Try out the new Strata Ion framework

[keyboardDrummer]

Update the strata submodule to the commit from this PR: keyboardDrummer/Strata#7

And then use the changes from that PR to update the Laurel AST and the Laurel backend in this repository.

[keyboardDrummer-bot]

I've analyzed the Strata PR (keyboardDrummer/Strata#7) and the current jverify codebase. I have a few questions before proceeding:

Understanding the scope of changes:

The Strata PR introduces two things:

1. A new getIonSerializer% elaborator that generates Java from Lean types (simpler output: no SourceRange, Node, IonSerializer, or builder class — just records/interfaces with toIon(IonSystem ion))
2. The old DDM-based generator is preserved but moved to Strata.Java.DDM.generateDialect (in GenDDM.lean)

The current Laurel AST in jverify is generated via make generate-laurel-ast, which runs lake exe strata javaGen Laurel ... — this uses the DDM-based generator. The generated code is deeply integrated into the backend:

• JavaToLaurelCompiler uses Laurel.* builder methods, SourceRange, Node, IonSerializer
• LaurelDriver uses IonSerializer for serialization to Ion binary format
• All AST nodes implement Node with sourceRange(), operationName(), toIon(IonSerializer $s)

Questions:

1. Which generator should the Laurel AST use? Should I switch the Laurel AST to use the new getIonSerializer% elaborator, or keep using the DDM-based generator (now at Strata.Java.DDM)? Switching to getIonSerializer% would require substantial changes to JavaToLaurelCompiler and LaurelDriver since the generated API is fundamentally different (no SourceRange, no Node interface, no IonSerializer, no builder class).

2. What does "update the Laurel AST" mean concretely? If we keep the DDM-based generator, the only change needed is updating the submodule and regenerating (since javaGen now calls Strata.Java.DDM.generateDialect). If we switch to getIonSerializer%, we'd need to define the Laurel AST as Lean types and generate Java from those, plus rewrite the backend to use the new API.

3. What does "update the Laurel backend" mean? Is this about adapting LaurelDriver/JavaToLaurelCompiler to work with whatever new AST is generated, or something else?

The simplest path is: update the submodule, regenerate the Laurel AST (which should produce identical output since the DDM generator was just moved to a new namespace), and verify the build still works. But I want to confirm that's the intent before proceeding, since the issue mentions "use the changes from that PR" which could imply adopting the new getIonSerializer% approach.

[keyboardDrummer]

Which generator should the Laurel AST use? Should I switch the Laurel AST to use the new getIonSerializer% elaborator

Yes

[keyboardDrummer-bot]

I'll switch the Laurel AST to use the new getIonSerializer% elaborator. Here's my plan:

1. Update the Strata submodule to the commit from Add getIonDeserializer% elaborator for generic Ion deserialization keyboardDrummer/Strata#7
2. Define the Laurel AST as Lean types that can be used with getIonSerializer%
3. Replace the generated Java files with what getIonSerializer% produces (records/interfaces with toIon(IonSystem ion) instead of Node/SourceRange/IonSerializer/builder class)
4. Update JavaToLaurelCompiler to construct the new AST types directly (no more Laurel.* static factory methods, no more SourceRange on every node)
5. Update LaurelDriver to serialize using the new toIon(IonSystem) API instead of IonSerializer
6. Update the Makefile generation command

Key API changes:

• SourceRange is removed from AST nodes (source ranges will need to be tracked separately or embedded differently)
• Node interface is removed
• IonSerializer class is removed
• Laurel builder class is removed
• Each type gets toIon(IonSystem ion) directly
• Optional<T> → nullable T
• List<T> → java.util.List<T> (same)

Starting implementation now.