From f022b9c4e96d68269700e062cf2a469e07ded612 Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Wed, 25 Feb 2026 04:29:14 +0100 Subject: [PATCH 1/3] =?UTF-8?q?Laurel=20API:=20precondition=20=E2=86=92=20?= =?UTF-8?q?preconditions,=20postcondition=20=E2=86=92=20postconditions?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - Laurel.lean: precondition (single) → preconditions (list), postcondition → postconditions in Body.Abstract, Parameter struct reorder, add Repr instances - ConcreteToAbstractTreeTranslator: adapt to list preconditions - LaurelToCoreTranslator: iterate over preconditions list - HeapParameterization: iterate over preconditions/postconditions lists - LaurelFormat: format preconditions list, restore formatDeterminism - LaurelEval: adapt While invariant handling - LiftExpressionAssignments: simplify block ordering - LaurelTypes: reorder operator match - PythonToLaurel, Specs/ToLaurel: adapt to new field names --- .../ConcreteToAbstractTreeTranslator.lean | 14 ++-- .../Laurel/HeapParameterization.lean | 26 +++---- Strata/Languages/Laurel/Laurel.lean | 31 +++++---- Strata/Languages/Laurel/LaurelEval.lean | 4 +- Strata/Languages/Laurel/LaurelFormat.lean | 20 +++--- .../Laurel/LaurelToCoreTranslator.lean | 12 ++-- .../Laurel/LiftExpressionAssignments.lean | 34 ++-------- Strata/Languages/Python/PythonToLaurel.lean | 6 +- Strata/Languages/Python/Specs/ToLaurel.lean | 2 +- .../Laurel/LiftExpressionAssignmentsTest.lean | 68 +++++++++++++++++++ 10 files changed, 135 insertions(+), 82 deletions(-) create mode 100644 StrataTest/Languages/Laurel/LiftExpressionAssignmentsTest.lean diff --git a/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean b/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean index 19285d20e..f28fdf534 100644 --- a/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean +++ b/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean @@ -126,7 +126,7 @@ instance : Inhabited Procedure where name := "" inputs := [] outputs := [] - precondition := mkStmtExprMdEmpty <| .LiteralBool true + preconditions := [] determinism := .deterministic none decreases := none body := .Transparent ⟨.LiteralBool true, #[]⟩ @@ -343,12 +343,14 @@ def parseProcedure (arg : Arg) : TransM Procedure := do | .option _ none => pure [] | _ => TransM.error s!"Expected returnParameters operation, got {repr returnParamsArg}" | _ => TransM.error s!"Expected optionalReturnType operation, got {repr returnTypeArg}" - -- Parse precondition (requires clause) - let precondition ← match requiresArg with + -- Parse preconditions (requires clause) + let preconditions ← match requiresArg with | .option _ (some (.op requiresOp)) => match requiresOp.name, requiresOp.args with - | q`Laurel.optionalRequires, #[exprArg] => translateStmtExpr exprArg + | q`Laurel.optionalRequires, #[exprArg] => do + let precond ← translateStmtExpr exprArg + pure [precond] | _, _ => TransM.error s!"Expected optionalRequires operation, got {repr requiresOp.name}" - | .option _ none => pure (mkStmtExprMdEmpty <| .LiteralBool true) + | .option _ none => pure [] | _ => TransM.error s!"Expected optionalRequires operation, got {repr requiresArg}" -- Parse postconditions (ensures clauses - zero or more) let postconditions ← translateEnsuresClauses ensuresArg @@ -370,7 +372,7 @@ def parseProcedure (arg : Arg) : TransM Procedure := do name := name inputs := parameters outputs := returnParameters - precondition := precondition + preconditions := preconditions determinism := .deterministic none decreases := none body := procBody diff --git a/Strata/Languages/Laurel/HeapParameterization.lean b/Strata/Languages/Laurel/HeapParameterization.lean index 4dd620f90..b920addc0 100644 --- a/Strata/Languages/Laurel/HeapParameterization.lean +++ b/Strata/Languages/Laurel/HeapParameterization.lean @@ -111,9 +111,9 @@ def analyzeProc (proc : Procedure) : AnalysisResult := { readsHeapDirectly := r1.readsHeapDirectly || r2.readsHeapDirectly, writesHeapDirectly := r1.writesHeapDirectly || r2.writesHeapDirectly, callees := r1.callees ++ r2.callees } - | .Abstract postcond => (collectExprMd postcond).run {} |>.2 - -- Also analyze precondition - let precondResult := (collectExprMd proc.precondition).run {} |>.2 + | .Abstract postconds => postconds.foldl (fun (acc : AnalysisResult) p => let r := (collectExprMd p).run {} |>.2; { readsHeapDirectly := acc.readsHeapDirectly || r.readsHeapDirectly, writesHeapDirectly := acc.writesHeapDirectly || r.writesHeapDirectly, callees := acc.callees ++ r.callees }) {} + -- Also analyze preconditions + let precondResult := proc.preconditions.foldl (fun (acc : AnalysisResult) p => let r := (collectExprMd p).run {} |>.2; { readsHeapDirectly := acc.readsHeapDirectly || r.readsHeapDirectly, writesHeapDirectly := acc.writesHeapDirectly || r.writesHeapDirectly, callees := acc.callees ++ r.callees }) {} { readsHeapDirectly := bodyResult.readsHeapDirectly || precondResult.readsHeapDirectly, writesHeapDirectly := bodyResult.writesHeapDirectly || precondResult.writesHeapDirectly, callees := bodyResult.callees ++ precondResult.callees } @@ -341,7 +341,7 @@ def heapTransformProcedure (proc : Procedure) : TransformM Procedure := do let outputs' := heapOutParam :: proc.outputs -- Precondition uses heap_in (the input state) - let precondition' ← heapTransformExpr heapInName proc.precondition + let preconditions' ← proc.preconditions.mapM (heapTransformExpr heapInName) let bodyValueIsUsed := !proc.outputs.isEmpty let body' ← match proc.body with @@ -360,14 +360,14 @@ def heapTransformProcedure (proc : Procedure) : TransformM Procedure := do pure (some (mkMd (.Block [assignHeapOut, implExpr'] none))) | none => pure none let modif' ← modif.mapM (heapTransformExpr heapOutName) - pure (.Opaque postconds' impl' modif') | .Abstract postcond => - let postcond' ← heapTransformExpr heapOutName postcond - pure (.Abstract postcond') + pure (.Opaque postconds' impl' modif') | .Abstract postconds => + let postconds' ← postconds.mapM (heapTransformExpr heapOutName) + pure (.Abstract postconds') return { proc with inputs := inputs', outputs := outputs', - precondition := precondition', + preconditions := preconditions', body := body' } else if readsHeap then @@ -375,7 +375,7 @@ def heapTransformProcedure (proc : Procedure) : TransformM Procedure := do let heapInParam : Parameter := { name := heapInName, type := ⟨.THeap, #[]⟩ } let inputs' := heapInParam :: proc.inputs - let precondition' ← heapTransformExpr heapInName proc.precondition + let preconditions' ← proc.preconditions.mapM (heapTransformExpr heapInName) let body' ← match proc.body with | .Transparent bodyExpr => @@ -386,13 +386,13 @@ def heapTransformProcedure (proc : Procedure) : TransformM Procedure := do let impl' ← impl.mapM (heapTransformExpr heapInName) let modif' ← modif.mapM (heapTransformExpr heapInName) pure (.Opaque postconds' impl' modif') - | .Abstract postcond => - let postcond' ← heapTransformExpr heapInName postcond - pure (.Abstract postcond') + | .Abstract postconds => + let postconds' ← postconds.mapM (heapTransformExpr heapInName) + pure (.Abstract postconds') return { proc with inputs := inputs', - precondition := precondition', + preconditions := preconditions', body := body' } else diff --git a/Strata/Languages/Laurel/Laurel.lean b/Strata/Languages/Laurel/Laurel.lean index 49f0c3876..e18fdcc4f 100644 --- a/Strata/Languages/Laurel/Laurel.lean +++ b/Strata/Languages/Laurel/Laurel.lean @@ -66,6 +66,9 @@ inductive Operation : Type where | Geq deriving Repr +-- Explicit instance needed for deriving Repr in the mutual block +instance : Repr (Imperative.MetaData Core.Expression) := inferInstance + /-- A wrapper that pairs a value with source-level metadata such as source locations and annotations. All Laurel AST nodes are wrapped in @@ -77,6 +80,7 @@ structure WithMetadata (t : Type) : Type where val : t /-- Source-level metadata (locations, annotations). -/ md : Imperative.MetaData Core.Expression + deriving Repr /-- The type system for Laurel programs. @@ -115,6 +119,7 @@ inductive HighType : Type where /-- Temporary construct meant to aid the migration of Python->Core to Python->Laurel. Type "passed through" from Core. Intended to allow translations to Laurel to refer directly to Core. -/ | TCore (s: String) + deriving Repr mutual @@ -130,8 +135,8 @@ structure Procedure : Type where inputs : List Parameter /-- Output parameters with their types. Multiple outputs are supported. -/ outputs : List Parameter - /-- The precondition that callers must satisfy. -/ - precondition : WithMetadata StmtExpr + /-- The preconditions that callers must satisfy. -/ + preconditions : List (WithMetadata StmtExpr) /-- Whether the procedure is deterministic or nondeterministic. -/ determinism : Determinism /-- Optional termination measure for recursive procedures. -/ @@ -141,6 +146,15 @@ structure Procedure : Type where /-- Source-level metadata. -/ md : Imperative.MetaData Core.Expression +/-- +A typed parameter for a procedure. +-/ +structure Parameter where + /-- The parameter name. -/ + name : Identifier + /-- The parameter type. -/ + type : WithMetadata HighType + /-- Specifies whether a procedure is deterministic or nondeterministic. @@ -153,15 +167,6 @@ inductive Determinism where /-- A nondeterministic procedure. They can read from the heap but there is no benefit from specifying a reads clause. -/ | nondeterministic -/-- -A typed parameter for a procedure. --/ -structure Parameter where - /-- The parameter name. -/ - name : Identifier - /-- The parameter type. -/ - type : WithMetadata HighType - /-- The body of a procedure. A body can be transparent (with a visible implementation), opaque (with a postcondition and optional implementation), @@ -172,11 +177,11 @@ inductive Body where | Transparent (body : WithMetadata StmtExpr) /-- An opaque body with a postcondition, optional implementation, and modifies clause. Without an implementation the postcondition is assumed. -/ | Opaque - (postcondition : List (WithMetadata StmtExpr)) + (postconditions : List (WithMetadata StmtExpr)) (implementation : Option (WithMetadata StmtExpr)) (modifies : List (WithMetadata StmtExpr)) /-- An abstract body that must be overridden in extending types. A type containing any members with abstract bodies cannot be instantiated. -/ - | Abstract (postcondition : WithMetadata StmtExpr) + | Abstract (postconditions : List (WithMetadata StmtExpr)) /-- The unified statement-expression type for Laurel programs. diff --git a/Strata/Languages/Laurel/LaurelEval.lean b/Strata/Languages/Laurel/LaurelEval.lean index 44b6a8704..46f4e0dbc 100644 --- a/Strata/Languages/Laurel/LaurelEval.lean +++ b/Strata/Languages/Laurel/LaurelEval.lean @@ -226,8 +226,8 @@ partial def eval (expr : StmtExpr) : Eval TypedValue := withResult <| EvalResult.TypeError s!"Static invocation of {callee} with wrong return type" else pure transparantResult - | Body.Opaque (postcondition: StmtExpr) _ _ => panic! "not implemented: opaque body" - | Body.Abstract (postcondition: StmtExpr) => panic! "not implemented: opaque body" + | Body.Opaque _ _ _ => panic! "not implemented: opaque body" + | Body.Abstract _ => panic! "not implemented: abstract body" popStack pure result diff --git a/Strata/Languages/Laurel/LaurelFormat.lean b/Strata/Languages/Laurel/LaurelFormat.lean index f7ace1cda..bb3063cfd 100644 --- a/Strata/Languages/Laurel/LaurelFormat.lean +++ b/Strata/Languages/Laurel/LaurelFormat.lean @@ -142,11 +142,6 @@ end def formatParameter (p : Parameter) : Format := Format.text p.name ++ ": " ++ formatHighType p.type -def formatDeterminism : Determinism → Format - | .deterministic none => "deterministic" - | .deterministic (some reads) => "deterministic reads " ++ formatStmtExpr reads - | .nondeterministic => "nondeterministic" - def formatBody : Body → Format | .Transparent body => formatStmtExpr body | .Opaque postconds impl modif => @@ -156,13 +151,21 @@ def formatBody : Body → Format match impl with | none => Format.nil | some e => " := " ++ formatStmtExpr e - | .Abstract post => "abstract ensures " ++ formatStmtExpr post + | .Abstract posts => "abstract" ++ Format.join (posts.map (fun p => " ensures " ++ formatStmtExpr p)) + +def formatDeterminism : Determinism → Format + | .deterministic none => "deterministic" + | .deterministic (some reads) => "deterministic reads " ++ formatStmtExpr reads + | .nondeterministic => "nondeterministic" + +instance : Std.ToFormat Determinism where + format := formatDeterminism def formatProcedure (proc : Procedure) : Format := "procedure " ++ Format.text proc.name ++ "(" ++ Format.joinSep (proc.inputs.map formatParameter) ", " ++ ") returns " ++ Format.line ++ "(" ++ Format.joinSep (proc.outputs.map formatParameter) ", " ++ ")" ++ Format.line ++ - "requires " ++ formatStmtExpr proc.precondition ++ Format.line ++ + Format.join (proc.preconditions.map (fun p => "requires " ++ formatStmtExpr p ++ Format.line)) ++ formatDeterminism proc.determinism ++ Format.line ++ formatBody proc.body @@ -206,9 +209,6 @@ instance : Std.ToFormat StmtExpr where instance : Std.ToFormat Parameter where format := formatParameter -instance : Std.ToFormat Determinism where - format := formatDeterminism - instance : Std.ToFormat Body where format := formatBody diff --git a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean b/Strata/Languages/Laurel/LaurelToCoreTranslator.lean index 0d6434be9..57e0ac405 100644 --- a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean +++ b/Strata/Languages/Laurel/LaurelToCoreTranslator.lean @@ -316,13 +316,13 @@ def translateProcedure (constants : List Constant) (funcNames : FunctionNames) ( let initEnv : TypeEnv := proc.inputs.map (fun p => (p.name, p.type)) ++ proc.outputs.map (fun p => (p.name, p.type)) ++ constants.map (fun c => (c.name, c.type)) - -- Translate precondition if it's not just LiteralBool true + -- Translate preconditions let preconditions : ListMap Core.CoreLabel Core.Procedure.Check := - match proc.precondition with - | ⟨ .LiteralBool true, _ ⟩ => [] - | precond => + let (_, result) := proc.preconditions.foldl (fun (i, acc) precond => + let label := if proc.preconditions.length == 1 then "requires" else s!"requires_{i}" let check : Core.Procedure.Check := { expr := translateExpr constants initEnv precond, md := precond.md } - [("requires", check)] + (i + 1, acc ++ [(label, check)])) (0, []) + result -- Translate postconditions for Opaque bodies let postconditions : ListMap Core.CoreLabel Core.Procedure.Check := match proc.body with @@ -408,7 +408,7 @@ def canBeBoogieFunction (proc : Procedure) : Bool := match proc.body with | .Transparent bodyExpr => isPureExpr bodyExpr && - (match proc.precondition.val with | .LiteralBool true => true | _ => false) && + proc.preconditions.isEmpty && proc.outputs.length == 1 | _ => false diff --git a/Strata/Languages/Laurel/LiftExpressionAssignments.lean b/Strata/Languages/Laurel/LiftExpressionAssignments.lean index 3b9f1f375..cfa6d4486 100644 --- a/Strata/Languages/Laurel/LiftExpressionAssignments.lean +++ b/Strata/Languages/Laurel/LiftExpressionAssignments.lean @@ -261,9 +261,12 @@ def transformExpr (expr : StmtExprMd) : LiftM StmtExprMd := do match val with | .LocalVariable name ty _ => addToEnv name ty | _ => pure () - -- Process all-but-last right to left using transformExprDiscarded - for nonLastStatement in stmts.dropLast.reverse.attach do - transformExprDiscarded nonLastStatement + -- Process all-but-last as statements and prepend them in order + let mut blockStmts : List StmtExprMd := [] + for nonLastStatement in stmts.dropLast.attach do + have := List.dropLast_subset stmts nonLastStatement.property + blockStmts := blockStmts ++ (← transformStmt nonLastStatement) + for s in blockStmts.reverse do addPrepend s -- Last element is the expression value transformExpr last @@ -289,31 +292,6 @@ def transformExpr (expr : StmtExprMd) : LiftM StmtExprMd := do termination_by (sizeOf expr, 0) decreasing_by all_goals (simp_all; try term_by_mem) - have := List.dropLast_subset stmts - have stmtInStmts : nonLastStatement.val ∈ stmts := by grind - -- term_by_mem gets a type error here, so we do it manually - have xSize := List.sizeOf_lt_of_mem stmtInStmts - omega - -/-- -Transform an expression whose result value is discarded (e.g. non-last elements in a block). All side-effects in Laurel are represented as assignments, so we only need to lift assignments, anything else can be forgotten. --/ -def transformExprDiscarded (expr2 : StmtExprMd) : LiftM Unit := do - match _hExpr: expr2 with - | WithMetadata.mk val md => - match _h: val with - | .Assign targets value => - -- Transform value to process nested assignments (side-effect only), - -- but use original value for the prepended assignment (no substitutions needed). - let _ ← transformExpr value - liftAssignExpr targets value md - | _ => - let result ← transformExpr expr2 - addPrepend result - termination_by (sizeOf expr2, 1) - decreasing_by - simp_all; omega - rw [<- _hExpr]; omega /-- Process a statement, handling any assignments in its sub-expressions. diff --git a/Strata/Languages/Python/PythonToLaurel.lean b/Strata/Languages/Python/PythonToLaurel.lean index 5f65eda1f..60b52fcda 100644 --- a/Strata/Languages/Python/PythonToLaurel.lean +++ b/Strata/Languages/Python/PythonToLaurel.lean @@ -551,7 +551,7 @@ def translateFunction (ctx : TranslationContext) (f : Python.stmt SourceRange) name := funcName inputs := inputs outputs := outputs - precondition := mkStmtExprMd (StmtExpr.LiteralBool true) + preconditions := [] determinism := .deterministic none -- TODO: need to set reads decreases := none body := Body.Transparent bodyBlock @@ -634,9 +634,9 @@ def pythonToLaurel (prelude: Core.Program) name := "__main__", inputs := [], outputs := [], - precondition := mkStmtExprMd (StmtExpr.LiteralBool true), + preconditions := [], + determinism := .deterministic none, --TODO: need to set reads decreases := none, - determinism := .deterministic none --TODO: need to set reads body := .Transparent bodyBlock md := default } diff --git a/Strata/Languages/Python/Specs/ToLaurel.lean b/Strata/Languages/Python/Specs/ToLaurel.lean index 686d7dd81..5c22f6e74 100644 --- a/Strata/Languages/Python/Specs/ToLaurel.lean +++ b/Strata/Languages/Python/Specs/ToLaurel.lean @@ -268,7 +268,7 @@ def funcDeclToLaurel (procName : String) (func : FunctionDecl) name := procName inputs := inputs.toList outputs := outputs - precondition := ⟨.LiteralBool true, .empty⟩ + preconditions := [] determinism := .nondeterministic decreases := none body := .Opaque [] none [] diff --git a/StrataTest/Languages/Laurel/LiftExpressionAssignmentsTest.lean b/StrataTest/Languages/Laurel/LiftExpressionAssignmentsTest.lean new file mode 100644 index 000000000..ea03e304a --- /dev/null +++ b/StrataTest/Languages/Laurel/LiftExpressionAssignmentsTest.lean @@ -0,0 +1,68 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +/- +Tests that the expression lifter correctly handles statement constructs +(heap-updating assignments) in non-last positions of block expressions, +by comparing the lifted Laurel against expected output. +-/ + +import Strata.DDM.Elab +import Strata.DDM.BuiltinDialects.Init +import Strata.Languages.Laurel.Grammar.LaurelGrammar +import Strata.Languages.Laurel.Grammar.ConcreteToAbstractTreeTranslator +import Strata.Languages.Laurel.LaurelToCoreTranslator + +open Strata +open Strata.Elab (parseStrataProgramFromDialect) + +namespace Strata.Laurel + +def blockStmtLiftingProgram : String := r" +composite Box { + var value: int +} + +procedure heapUpdateInBlockExpr(b: Box) +{ + var x: int := { b#value := b#value + 1; b#value }; + assert x == b#value; +} + +procedure assertInBlockExpr() +{ + var x: int := 0; + var y: int := { assert x == 0; x := 1; x }; + assert y == 1; +} +" + +def parseLaurelAndLift (input : String) : IO Program := do + let inputCtx := Strata.Parser.stringInputContext "test" input + let dialects := Strata.Elab.LoadedDialects.ofDialects! #[initDialect, Laurel] + let strataProgram ← parseStrataProgramFromDialect dialects Laurel.name inputCtx + let uri := Strata.Uri.file "test" + match Laurel.TransM.run uri (Laurel.parseProgram strataProgram) with + | .error e => throw (IO.userError s!"Translation errors: {e}") + | .ok program => pure (liftExpressionAssignments program) + +/-- +info: procedure heapUpdateInBlockExpr(b: Box) returns +() +deterministic +{ b#value := b#value + 1; var x: int := b#value; assert x == b#value } +procedure assertInBlockExpr() returns +() +deterministic +{ var x: int := 0; assert x == 0; x := 1; var y: int := x; assert y == 1 } +-/ +#guard_msgs in +#eval! do + let program ← parseLaurelAndLift blockStmtLiftingProgram + for proc in program.staticProcedures do + IO.println (toString (Std.Format.pretty (Std.ToFormat.format proc))) + +end Laurel From 1fccd3a84020eaa86522ccaae355c31aab30d961 Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Thu, 26 Feb 2026 18:29:55 +0100 Subject: [PATCH 2/3] Address review: remove LaurelGrammar.lean artifact, clean up analyzeProc with forM --- Strata/Languages/Laurel/Grammar/LaurelGrammar.lean | 3 --- Strata/Languages/Laurel/HeapParameterization.lean | 4 ++-- 2 files changed, 2 insertions(+), 5 deletions(-) diff --git a/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean b/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean index 1266020c1..d6664abec 100644 --- a/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean +++ b/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean @@ -5,11 +5,8 @@ -/ -- Laurel dialect definition, loaded from LaurelGrammar.st --- NOTE: Changes to LaurelGrammar.st are not automatically tracked by the build system. --- Update this file (e.g. this comment) to trigger a recompile after modifying LaurelGrammar.st. import Strata.DDM.Integration.Lean namespace Strata.Laurel #load_dialect "./LaurelGrammar.st" - diff --git a/Strata/Languages/Laurel/HeapParameterization.lean b/Strata/Languages/Laurel/HeapParameterization.lean index bb95f8daf..ef8041ca9 100644 --- a/Strata/Languages/Laurel/HeapParameterization.lean +++ b/Strata/Languages/Laurel/HeapParameterization.lean @@ -111,9 +111,9 @@ def analyzeProc (proc : Procedure) : AnalysisResult := { readsHeapDirectly := r1.readsHeapDirectly || r2.readsHeapDirectly, writesHeapDirectly := r1.writesHeapDirectly || r2.writesHeapDirectly, callees := r1.callees ++ r2.callees } - | .Abstract postconds => postconds.foldl (fun (acc : AnalysisResult) p => let r := (collectExprMd p).run {} |>.2; { readsHeapDirectly := acc.readsHeapDirectly || r.readsHeapDirectly, writesHeapDirectly := acc.writesHeapDirectly || r.writesHeapDirectly, callees := acc.callees ++ r.callees }) {} + | .Abstract postconds => (postconds.forM collectExprMd).run {} |>.2 -- Also analyze preconditions - let precondResult := proc.preconditions.foldl (fun (acc : AnalysisResult) p => let r := (collectExprMd p).run {} |>.2; { readsHeapDirectly := acc.readsHeapDirectly || r.readsHeapDirectly, writesHeapDirectly := acc.writesHeapDirectly || r.writesHeapDirectly, callees := acc.callees ++ r.callees }) {} + let precondResult := (proc.preconditions.forM collectExprMd).run {} |>.2 { readsHeapDirectly := bodyResult.readsHeapDirectly || precondResult.readsHeapDirectly, writesHeapDirectly := bodyResult.writesHeapDirectly || precondResult.writesHeapDirectly, callees := bodyResult.callees ++ precondResult.callees } From 79c3868411b30824ae2f64a9478f9a3510913df0 Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Thu, 26 Feb 2026 18:44:45 +0100 Subject: [PATCH 3/3] Restore LaurelGrammar.lean build tracking comment --- Strata/Languages/Laurel/Grammar/LaurelGrammar.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean b/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean index d6664abec..632e0a69b 100644 --- a/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean +++ b/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean @@ -5,6 +5,8 @@ -/ -- Laurel dialect definition, loaded from LaurelGrammar.st +-- NOTE: Changes to LaurelGrammar.st are not automatically tracked by the build system. +-- Update this file (e.g. this comment) to trigger a recompile after modifying LaurelGrammar.st. import Strata.DDM.Integration.Lean namespace Strata.Laurel