Laurel Language Enhancements by fabiomadge · Pull Request #385 · strata-org/Strata

fabiomadge · 2026-02-04T17:45:17Z

Summary

Expands the Laurel language with additional operators, data types, and verification constructs. Improves formatting across multiple dialects.

Key Changes

Laurel Grammar & Translator

New operators: -, *, /, %, /t, %t (truncating), ==>, !, unary -
Array support: Array<T> type, indexing, length
Sequence operations: Seq.From, Seq.Take, Seq.Drop, Seq.Contains
Constrained types with constraint injection into quantifiers
Quantifiers: forall, exists
Return statement works with postconditions
While loops with multiple invariants
Multiple requires clauses per procedure

Infrastructure

NewlineSepBy separator type for formatting preservation
Java codegen: list separator preservation, SourceRange overloads
Improved pretty printing for C_Simp, B3, Core

CLI Commands

laurelParse, laurelAnalyze, laurelToCore, laurelPrint

Bug Fixes

Fixed SMT encoding for multi-argument functions and Map type
Added substFvarLifting for proper de Bruijn index handling

Tests

Reorganized Laurel tests T01-T17
Added regression test for assignment lifting

…o laurelParsing

Resolve conflicts from c0409bb 'Add tactic for simplifying termination proofs': - Use term_by_mem where applicable in Laurel termination proofs - Keep manual proofs where term_by_mem can't handle the goal (HighType recursion, attach patterns)

keyboardDrummer · 2026-02-11T18:09:51Z

Strata/Languages/Laurel/Laurel.lean

  inputs : List Parameter
  outputs : List Parameter
-  precondition : WithMetadata StmtExpr
-  determinism : Determinism


What happened to determinism?

Intentionally removed in 67931730 — it was only ever set to .nondeterministic and never pattern-matched on.

I know it wasn't used but that doesn't mean it shouldn't be there. The whole AST wasn't used when it was first merged. Can you bring it back?

keyboardDrummer · 2026-02-11T18:10:15Z

Strata/Languages/Laurel/Laurel.lean


 theorem WithMetadata.sizeOf_val_lt {t : Type} [SizeOf t] (e : WithMetadata t) : sizeOf e.val < sizeOf e := by
-  cases e; grind
+  cases e <;> simp_wf <;> omega


Merge accident?

Intentional. omega is simpler and more predictable than grind here, and it proves the goal.

keyboardDrummer · 2026-02-11T18:14:35Z

Strata/Languages/Laurel/LaurelToCoreTranslator.lean

+  | _ => none
+
+/-- Collect Array.Get accesses with constrained element types -/
+def collectConstrainedArrayAccesses (env : TypeEnv) (tcMap : TranslatedConstraintMap) (e : StmtExprMd) : List (StmtExprMd × StmtExprMd × TranslatedConstraint) :=


Shouldn't the implementation of constraints be independent of the implementation of Arrays? If this is temporary code, can we mark it as such?

Added a TODO. Array.Get is special because it's a built-in (SMT select), not a procedure call, so there's no contract to assume from. Other constrained type sources (procedure returns, field reads) get their assumes via contracts. If more built-ins return constrained types in the future, this should be generalized.

keyboardDrummer · 2026-02-12T12:37:40Z

Strata/Languages/Laurel/LaurelToCoreTranslator.lean

+      let belse ← match elseBranch with
+                  | some e => do let (_, s) ← translateStmt ctMap tcMap env outputParams postconds e; pure s
+                  | none => pure []
+      pure (env, arrayElemAssumes ++ [Imperative.Stmt.ite bcond bthen belse stmt.md])


Why does the translation of IfThenElse refer to arrayElemAssumes? That can't be right

Good catch — fixed in fb9c7f60. Compound statements (Block, IfThenElse, While) no longer generate arrayElemAssumes at the top level. Their sub-statements handle their own assumes via recursive translateStmt calls.

keyboardDrummer · 2026-02-12T12:40:55Z

Strata/Languages/Laurel/LaurelToCoreTranslator.lean

-        (e', acc ++ ss)) (env, [])
-      (env', stmtsList)
-  | .LocalVariable name ty initializer =>
+def translateStmt (ctMap : ConstrainedTypeMap) (tcMap : TranslatedConstraintMap) (env : TypeEnv) (outputParams : List Parameter) (postconds : List (String × Core.Expression.Expr)) (stmt : StmtExprMd) : Except String (TypeEnv × List Core.Statement) := do


Why would you introduce assert statements related to postconditions? Core will already check that procedure bodies adhere to the postconditions of that procedure.

These asserts are needed for early returns. Laurel's return is translated to result := value; assert postconditions; assume false. The assume false prevents fall-through but also makes the path vacuously true, so Core's VCG won't check postconditions on it.

Without the asserts, a postcondition-violating early return passes verification silently. I verified this by writing a Core program where the early return path sets result := -x (violating ensures result >= 0):

Without the assert before assume false: ✅ pass (unsound)

With the assert before assume false: ❌ fail (correct)

Laurel's return is translated to result := value; assert postconditions; assume false

Is that new? It's not mentioned in the PR. I think it would be better to encode a return using a jump than an assume false. With the assume false it would be incorrect when executing the code, since then the assume is ignored, and having to assert the postconditions introduces a lot of duplication.

You're right that goto would be better. I tried implementing it (return value → result := value; goto "\$return" with \$return: {} at the end of the body), and it works correctly for individual procedures.

However, I found a Core VCG issue: when a procedure has a goto inside an if branch, processIteBranches produces multiple EnvWithNext results, and these multiply across procedures via ProgramEval.flatMap. A second procedure's assertions get checked N times instead of once.

Filed as #419 with a proposed fix (merge paths by nextLabel in processIteBranches). Keeping assume false for now until that's resolved.

However, I found a Core VCG issue

Nice find! How did you find that?

I'm hesitant to merge the assert+assume solution for reasons that I think you identified as well:

It works with an analysis that respects assume false but not one that ignores it, like concrete execution.

It duplicates the postconditions for each return so it breaks our goal of having transformations that are linear in size.

The current PythonToCore translation uses the goto approach, so to support moving that over to Laurel, we could use the goto approach as well.

I'm also ok with using the assert+assume approach if we sufficiently document that it is a temporary solution.

…ules

…aints - Don't generate arrayElemAssumes for compound statements (Block, IfThenElse, While). Their sub-statements handle their own assumes via recursive translateStmt calls. Previously, assumes for array accesses inside branches were incorrectly hoisted before the if/while statement. - Add TODO comment explaining why constraint injection is array-specific: Array.Get is a built-in (SMT select), not a procedure call, so there's no contract to assume from.

Strata/DDM/Parser.lean

Strata/DDM/Integration/Java/Gen.lean

Strata/DDM/Format.lean

Strata/DDM/Integration/Java/Gen.lean

joehendrix

I added a few suggestions, but this looks reasonable to me. I'll approve this if you don't like the suggestions.

- Parser.lean: use Id.run do + early return for comment parsing, replace startsWith with utf8ByteSize check (comment 6) - Java/Gen.lean: match on DDM category name (Init.Num/Init.Decimal) instead of Java type string for builder parameter generation (comment 7) - Format.lean: collapse comma/space/newline seq formatting into single sepBy arm, eliminating duplication (comment 8) - Java/Gen.lean: consolidate getSeparator with SepFormat.toIonName by adding fromCategoryName? and moving Ion-specific functions to Strata.DDM.Ion (comment 9)

keyboardDrummer · 2026-02-14T12:28:02Z

StrataTest/Languages/Laurel/Examples/Fundamentals/T03_Variables.lean

@@ -1 +1 @@
 /-


Why the rename of this test?

keyboardDrummer · 2026-02-16T08:43:57Z

Strata/Languages/Laurel/LaurelToCoreTranslator.lean

    body := body
+  }) .empty
+
+def arrayTypeSynonym : Core.Decl := .type (.syn { name := "Array", typeArgs := ["T"], type := .tcons "Map" [.int, .ftvar "T"] })


Can you move these static Core definition to CorePrelude.lean ?

keyboardDrummer · 2026-02-16T08:44:41Z

Strata/Languages/Laurel/LaurelToCoreTranslator.lean

+    explicitPreconditions := explicitPreconditions ++ [(s!"{proc.name}_pre_{i}", check)]
+  let preconditions := inputConstraints ++ arrayLenConstraints ++ explicitPreconditions
+  -- Generate constraint checks for output parameters with constrained types
+  let outputConstraints : List (Core.CoreLabel × Core.Procedure.Check) ←


Can you generate the implicit pre and postconditions in a separate pass in a separate file?

keyboardDrummer · 2026-02-16T08:46:48Z

Strata/Languages/Laurel/LaurelToCoreTranslator.lean

+      | some expr => pure (some (s!"{proc.name}_input_{p.name}_constraint", { expr, md := p.type.md }))
+      | none => pure none)
+  -- Array lengths are implicitly >= 0
+  let arrayLenConstraints : List (Core.CoreLabel × Core.Procedure.Check) :=


Can you move everything related to arrays to a separate file? Can you elaborate on the design of Array support? How come it's not a Laurel library? The length constraint seems like a type invariant or constrained type.

keyboardDrummer · 2026-02-16T09:14:50Z

Strata/Languages/Laurel/LaurelToCoreTranslator.lean

+
+/-- Extract sequence bounds from Seq.From/Take/Drop chain.
+    Note: Seq.From only works with simple Identifier arguments; complex expressions are not supported. -/
+def translateSeqBounds (env : TypeEnv) (expr : StmtExprMd) : Except String SeqBounds :=


Can everything related to sequences be in a separate file? Can it be a separate pass?

keyboardDrummer · 2026-02-16T09:17:03Z

StrataTest/Languages/Laurel/Examples/Fundamentals/T10_Arrays.lean

@@ -0,0 +1,42 @@
+/-


Can you move and Sequence support tests into a separate folder?

keyboardDrummer · 2026-02-16T09:21:12Z

Can you add Laurel test Idiomaticity.lean that compares it's expectation against the generated Core code? That way it'll be easier to see how idiomatic the generated code is. I'm asking for this in this PR because some of the changes are pretty complicated and it's difficult for me to see from the translations what the end result is.

keyboardDrummer · 2026-02-16T09:31:18Z

Strata/Languages/Laurel/LaurelToCoreTranslator.lean

+      match outputParams.head? with
+      | some _ => do
+          let coreExpr ← translateExpr ctMap tcMap env stmt
+          mkReturnStmts (some coreExpr)


Is this the scenario where we return "naturally" because we reach the end of a block? Since this is not a jump, should we not call something different than mkReturnStmt which does do a jump?

keyboardDrummer · 2026-02-16T10:09:16Z

Strata/Languages/Laurel/Grammar/LaurelGrammar.st

 op assume (cond : StmtExpr) : StmtExpr => "assume " cond ";";
 op return (value : StmtExpr) : StmtExpr => "return " value ";";
-op block (stmts : Seq StmtExpr) : StmtExpr => @[prec(1000)] "{" stmts "}";
+op block (stmts : NewlineSepBy StmtExpr) : StmtExpr => @[prec(1000)] "{" indent(2, "\n" stmts) "\n}";


The indent(2, is never used anywhere, right? I don't think we're ever printing Laurel through the DDM. Why did you add this?

keyboardDrummer · 2026-02-16T11:56:38Z

Strata/DDM/Elab.lean

    return commands
  let (some tree, true) ← runChecked <| elabCommand leanEnv
    | return commands
+  -- Prevent infinite loop if parser makes no progress


This is great!!

keyboardDrummer · 2026-02-16T11:57:12Z

Strata/DDM/Integration/Lean/Gen.lean

  | q`Init.SpacePrefixSepBy, 1 =>
    let inner := mkCApp ``Array #[args[0]]
    return if addAnn then mkCApp ``Ann #[inner, annType] else inner
+  | q`Init.NewlineSepBy, 1 =>


Can you say more about this NewlineSepBy operator? What is it for?

Contains a subset of the changes from #385 ### Changes - Fix to Strata/DDM/Parser.lean so it can handle parsing comments `//` in languages that have a division operator - New operators: `-`, `*`, `/`, `%`, `/t`, `%t` (truncating), `==>`, `!`, unary `-` - Quantifiers: `forall`, `exists` - While loops with multiple invariants ### Testing - Added tests for the new features --------- Co-authored-by: Andrew Wells <130512013+andrewmwells-amazon@users.noreply.github.com>

keyboardDrummer and others added 30 commits December 16, 2025 14:40

Fix warning

125bf17

Renames

fd1374f

T2_NestedImpureStatements.lean

cd77f34

Restructure files

de4e4a4

Improvements

110fc87

Updates

0104e5a

Updates to the grammar

a7562b5

Updates

d530725

Add panics

d37c57a

Translate all operators

871b27e

Merge branch 'main' into moveExamples

8ddbaa3

Progress with T3

5624f00

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

02c5cdd

Undo bad changes

9efa44a

Merge branch 'laurelParsing' into laurelMoreStmtExpr

853aa4d

Merge branch 'moveExamples' into laurelMoreStmtExpr

088816c

T3 passes now

f0454dd

Added failing assertion

b70f84d

Add breaking comment

6b0c417

Test update

67f4b31

Test passes now

333fc61

Merge branch 'main' into laurelParsing

eae1536

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

7e16741

Merge branch 'laurelParsing' of github.com:keyboardDrummer/Strata int…

f711bdc

…o laurelParsing

Merge branch 'laurelParsing' into laurelMoreStmtExpr

fbb9a07

Add missing file

0d964e3

Fix

b3c66a3

Improve testing output and fix some issues

f75ed44

Use dbg_trace instead of IO

c6c8d5c

Cleanup

f878398

keyboardDrummer requested changes Feb 12, 2026

View reviewed changes

fabiomadge and others added 5 commits February 12, 2026 21:06

Merge origin/main: cvc5 default solver, app builtin, Python specs mod…

313de3a

…ules

Merge origin/main: mutually recursive types in Core concrete syntax

fd3dc37

Merge branch 'main' into jverify-strata-backend

affc789

Fix MutualDatatypes test: update expected output for new formatting

f530354

joehendrix reviewed Feb 13, 2026

View reviewed changes

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

joehendrix reviewed Feb 13, 2026

View reviewed changes

Strata/DDM/Integration/Java/Gen.lean Outdated Show resolved Hide resolved

joehendrix reviewed Feb 13, 2026

View reviewed changes

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

joehendrix reviewed Feb 13, 2026

View reviewed changes

Strata/DDM/Integration/Java/Gen.lean Outdated Show resolved Hide resolved

joehendrix reviewed Feb 13, 2026

View reviewed changes

fabiomadge force-pushed the jverify-strata-backend branch from 80b2cc2 to 88d1a43 Compare February 13, 2026 02:21

keyboardDrummer added 5 commits February 13, 2026 17:54

Merge remote-tracking branch 'origin/main' into jverify-strata-backend

9e235df

Merge branch 'main' into jverify-strata-backend

ec98083

Merge remote-tracking branch 'origin/main' into jverify-strata-backend

11e3ad1

Remove obsolete stuff

69b57c0

Fix merge mistake

3dd3889

keyboardDrummer requested changes Feb 16, 2026

View reviewed changes

keyboardDrummer reviewed Feb 16, 2026

View reviewed changes

keyboardDrummer mentioned this pull request Feb 16, 2026

Add more operators, while statement and quantifiers #428

Merged

keyboardDrummer reviewed Feb 16, 2026

View reviewed changes

Cleanup

738c051

aqjune-aws self-requested a review February 16, 2026 16:29

keyboardDrummer mentioned this pull request Feb 16, 2026

Infrastructure changes from PR 385 #426

Open

Merge branch 'main' into jverify-strata-backend

6067f88

Conversation

fabiomadge commented Feb 4, 2026 • edited by keyboardDrummer Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary

Key Changes

Laurel Grammar & Translator

Infrastructure

CLI Commands

Bug Fixes

Tests

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!

fabiomadge Feb 12, 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!

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!

keyboardDrummer Feb 13, 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!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

joehendrix left a comment

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!

keyboardDrummer commented Feb 16, 2026

Uh oh!

Choose a reason for hiding this comment

Uh oh!

keyboardDrummer Feb 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

fabiomadge commented Feb 4, 2026 •

edited by keyboardDrummer

Loading

fabiomadge Feb 12, 2026 •

edited

Loading

keyboardDrummer Feb 13, 2026 •

edited

Loading

keyboardDrummer Feb 16, 2026 •

edited

Loading