Changes to enable communication with JVerify #308

keyboardDrummer · 2026-01-08T13:26:55Z

Changes

Move Laurel grammar from a .lean into a .st file, so it can be consumed by the javaGen command
Do not let the Laurel grammar use fn or type, since those are not needed and are not supported by javaGen
For source code positions, store byte code array offsets in the AST nodes, so that when parsing programs from Ion, these can be filled in without having access to original source files
Enable the Ion deserialization code to deserialize multiple files where each file has a filepath and a program AST.
Add a laurelAnalyze command to StrataMain that for now will serve as a root for Laurel related interactions. I can imagine that in the future we will introduce an analyze command that is agnostic to the dialect used.

Testing

Laurel pipeline changes (1-3) are covered by existing tests
(4) Added a test for the newly introduced Ion.fromIonFiles
(5) No test added, although I've successfully used this command from https://github.com/aws/jverify/pull/372

- Use writeJavaFiles helper in Test 11 (keyboardDrummer) - Document Test 12's dependency on comprehensive.ion (keyboardDrummer) - Fail if javac not found instead of skip (keyboardDrummer) - Use panic! for malformed SyntaxCat (joehendrix) - Add doc comments to GeneratedFiles and NameAssignments (joehendrix) - Collect warnings for unsupported type/function declarations (joehendrix)

PR strata-org#293 added dots to valid identifier characters, which broke qualified name resolution (e.g., 'Simple.Expr' was parsed as one identifier instead of dialect 'Simple' + name 'Expr'). Fix: In translateQualifiedIdent, split dotted identifiers on the first dot to extract dialect and name components. Also strip guillemets that the parser adds around special identifiers.

… lineoffsets when parsing Ion

- Fail on Init.TypeExpr (internal DDM machinery) - Fail on type/function declarations instead of warning - Remove warnings mechanism from GeneratedFiles - Fix cross-dialect category collision (A.Num vs B.Num) - Track QualifiedIdent instead of String for refs - Prefix with dialect name when names collide - Replace gradle with plain javac/java in regenerate script - Add test for cross-dialect name collision

joehendrix · 2026-01-14T00:10:53Z

Strata/DDM/AST.lean

+  | file (path: String)
+  deriving DecidableEq, Repr
+
+instance : ToFormat Uri where
+ format fr := match fr with | .file path => path
+
+structure FileRange where
+  file: Uri
+  range: Strata.SourceRange
+  deriving DecidableEq, Repr
+
+instance : ToFormat FileRange where
+ format fr := f!"{fr.file}:{fr.range}"
+
+structure File2dRange where
+  file: Uri
+  start: Lean.Position
+  ending: Lean.Position
+  deriving DecidableEq, Repr
+
+instance : ToFormat File2dRange where
+ format fr :=
+    let baseName := match fr.file with
+                    | .file path => (path.splitToList (· == '/')).getLast!
+    f!"{baseName}({fr.start.line}, {fr.start.column})-({fr.ending.line}, {fr.ending.column})"


These should not appear in between the definition of SourceRange and the methods in it's namespace.

joehendrix · 2026-01-14T00:11:34Z

Strata/DDM/Ion.lean

  | .mk (.list args) =>
    return .mk args (by simp; omega)
-  | _ => throw s!"Expected list"
+  | x => throw s!"Expected list but got {repr x}"


These values could be large. Repr may generate too much content.

Strata/DDM/Ion.lean

joscoh · 2026-01-14T15:11:58Z

Strata/DDM/Ion.lean

+    match Ion.deserialize bytes with
+    | .error (off, msg) => throw s!"Error reading Ion: {msg} (offset = {off})"
+    | .ok a =>
+      if p : a.size = 1 then


Do you use the p hypothesis anywhere?

If I remove p : then the next line with a[0] fails to prove. I don't know how Lean decides to use this fact implicitly.

Can you replace with _ : a.size = 1?

That's not valid syntactically 🤷

Note there is a if p : a.size = 1 then where the p is not used somewhere else in the codebase as well.

Weird, match _ : x with is fine but if _ : x then ... is not.

It's not short, but I frequently will handle this with a line like the following in monadic code.

let .isTrue p := inferInstanceAs (Decidable (a.size = 1)) | throw "blah blah blah"

This performs the checks, and subsequent code has access to the proof while the exception path is short.

Strata/DDM/Ion.lean

joehendrix · 2026-01-15T16:58:23Z

Strata/DDM/Ion.lean

      throw s!"{name} program found when {dialect} expected."
    fromIonFragment frag dialects dialect

+def filesFromIon (dialects : DialectMap) (bytes : ByteArray) : Except String (List StrataFile) := do


This seems like it shouldn't live in the Program namespace. Maybe move up one level and rename fileFromIon back?

Maybe this could be StrataFile.filesFromIon and appear below Program things.

I notice I have 0 intuition for what should be in what namespace. filesFromIon parses Ion into programs (nested in StrataFile), so why shouldn't it live in the Program namespace?

Maybe this could be StrataFile.filesFromIon

When do you decide to put things in a namespace? Can you give me any guidelines for how to decide to put things in a particular file or in a particular namespace?

Without understanding the context very well, my inclination would be to have a single namespace per file, so you wouldn't be able to have multiple definitions with the same name in a single file, but that seems fine to me. Why not put everything in this file in a Strata.DDM.Ion namespace?

In any case, right now I'm happy to name/move things in whatever way you prefer, but it wasn't entirely clear to me what you meant with "appear below Program things". If you're willing to move/name the things yourself, that could help speed-up the PR, since then I can approve your commit and @aqjune-aws can be the second approver and code-owner.

For me, I mostly keep things in the same top-level namespace except for three reasons:

I can use dot notation to access it (e.g., I'd put an operation like count (p : Program) : Nat in Program so I can write p.count.

It is closely coupled to a particular type and has a generic name (e.g., Program.fromIon). Instances follow this pattern even if their names are typically auto-generated.

If it is closely coupled to a method following pattern (1) and (2), and not intended for much use. e.g., an auxillary function needed to implementation some other methods.

I'm kind of slow at task switching and want to prioritize my regular work commitments.

I think I am fine with leaving this as is also; it doesn't matter that much if I don't see it as idiomatic.

fabiomadge and others added 30 commits December 23, 2025 03:33

feat(DDM): Java code generator for dialects

613fec6

Merge remote-tracking branch 'origin/main' into feat/java-codegen

e18f450

docs: update module docstring to mention builders

f99ea87

test: verify deserialized AST structure

780c78e

chore: remove redundant inline comments

e0b2bb5

refactor: use #load_dialect instead of inline dialect definition

da67291

fix: correct test 2 title

67c170d

test: use Simple dialect for compile test, include builders

8731075

fix: disambiguate builders filename to avoid collisions

98c3a4a

refactor: use get! and alter for cleaner lookups

b36929a

fix: escape builder method names for Java reserved words

1404ab0

Merge remote-tracking branch 'origin/main' into feat/java-codegen

be0acbf

Add LaurelGrammar.st file

22d07ed

Add laurelVerify command

cfc4a3a

Fixes

705cfb4

Fix namespace

28c581c

Fix concrete tree converter

b738175

Add missing files to run regenerate-testdata.sh, and enable including…

9e5a509

… lineoffsets when parsing Ion

Added filepaths as well

52e1f3f

Consume list of StrataFiles when consuming Laurel over ion

e2f5f47

Remove lineOffsets from StrataFile

ac9400b

Store source code byte offsets in the metadata instead of 2d positions

8d10e11

Fix printed filepath

e2715f1

Fixes

9e7994d

Merge branch 'main' into feat/java-codegen

a3e9ec9

Refactoring

46e0e58

Refactoring

44155c0

joehendrix reviewed Jan 14, 2026

View reviewed changes

keyboardDrummer added 3 commits January 14, 2026 09:37

Merge remote-tracking branch 'origin/main' into forJVerify

d15ab9a

Refactoring

9d40949

Merge remote-tracking branch 'origin/main' into forJVerify

6d7fc13

keyboardDrummer requested a review from joehendrix January 14, 2026 09:03

keyboardDrummer enabled auto-merge January 14, 2026 09:03

keyboardDrummer added 2 commits January 14, 2026 11:17

Fix merge error

a223c5d

Fix errors

84d86e7

keyboardDrummer mentioned this pull request Jan 14, 2026

Laurel fundamentals not supported #322

Draft

joscoh reviewed Jan 14, 2026

View reviewed changes

keyboardDrummer added 3 commits January 15, 2026 12:06

Cleanup

8da23f6

Merge remote-tracking branch 'origin/main' into forJVerify

2797281

Fix failing proof by adding ': h'

49bac76

keyboardDrummer requested a review from joscoh January 15, 2026 11:13

Fix merge mistakes

4b86292

joscoh previously approved these changes Jan 15, 2026

View reviewed changes

joehendrix reviewed Jan 15, 2026

View reviewed changes

Strata/DDM/Ion.lean Outdated Show resolved Hide resolved

joehendrix reviewed Jan 15, 2026

View reviewed changes

Remove repr usage

bafb7d2

keyboardDrummer dismissed joscoh’s stale review via 307f9a7 January 16, 2026 11:14

Merge remote-tracking branch 'origin/main' into forJVerify

79ee155

keyboardDrummer force-pushed the forJVerify branch from 307f9a7 to 79ee155 Compare January 16, 2026 11:20

keyboardDrummer requested a review from joehendrix January 16, 2026 11:20

keyboardDrummer added 4 commits January 16, 2026 12:39

Fix build error

8e20c05

Additional fix

a5b1e4b

Fix

39d7d71

Merge branch 'main' into forJVerify

da8413c

keyboardDrummer mentioned this pull request Jan 16, 2026

Mutable fields keyboardDrummer/Strata#3

Draft

joehendrix approved these changes Jan 16, 2026

View reviewed changes

Changes to enable communication with JVerify #308

Are you sure you want to change the base?

Changes to enable communication with JVerify #308

Uh oh!

Conversation

keyboardDrummer commented Jan 8, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Changes

Testing

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

keyboardDrummer Jan 16, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

keyboardDrummer commented Jan 8, 2026 •

edited

Loading

keyboardDrummer Jan 16, 2026 •

edited

Loading