From 241c5981715fced69e38b394efed2a70dc193a53 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 23 Feb 2026 15:24:00 +0000 Subject: [PATCH 01/28] Introduce pure property for procedures --- .../ConcreteToAbstractTreeTranslator.lean | 7 +- .../Languages/Laurel/Grammar/LaurelGrammar.st | 9 ++ Strata/Languages/Laurel/Laurel.lean | 1 + Strata/Languages/Laurel/LaurelFormat.lean | 1 + .../Laurel/LaurelToCoreTranslator.lean | 46 ++++++---- .../Laurel/LiftExpressionAssignments.lean | 90 +++++++++++++++---- Strata/Languages/Python/PythonToLaurel.lean | 2 + .../T5_ProcedureCallsStrataCore.lean | 2 +- 8 files changed, 121 insertions(+), 37 deletions(-) diff --git a/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean b/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean index 19285d20e..d338547d3 100644 --- a/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean +++ b/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean @@ -129,6 +129,7 @@ instance : Inhabited Procedure where precondition := mkStmtExprMdEmpty <| .LiteralBool true determinism := .deterministic none decreases := none + isPure := false body := .Transparent ⟨.LiteralBool true, #[]⟩ md := .empty } @@ -322,6 +323,8 @@ def parseProcedure (arg : Arg) : TransM Procedure := do match op.name, op.args with | q`Laurel.procedure, #[nameArg, paramArg, returnTypeArg, returnParamsArg, + requiresArg, ensuresArg, modifiesArg, bodyArg] + | q`Laurel.pureProcedure, #[nameArg, paramArg, returnTypeArg, returnParamsArg, requiresArg, ensuresArg, modifiesArg, bodyArg] => let name ← translateIdent nameArg let nameMd ← getArgMetaData nameArg @@ -373,10 +376,12 @@ def parseProcedure (arg : Arg) : TransM Procedure := do precondition := precondition determinism := .deterministic none decreases := none + isPure := op.name == q`Laurel.pureProcedure body := procBody md := nameMd } - | q`Laurel.procedure, args => + | q`Laurel.procedure, args + | q`Laurel.pureProcedure, args => TransM.error s!"parseProcedure expects 8 arguments, got {args.size}" | _, _ => TransM.error s!"parseProcedure expects procedure, got {repr op.name}" diff --git a/Strata/Languages/Laurel/Grammar/LaurelGrammar.st b/Strata/Languages/Laurel/Grammar/LaurelGrammar.st index 2569ad818..b12db3d9d 100644 --- a/Strata/Languages/Laurel/Grammar/LaurelGrammar.st +++ b/Strata/Languages/Laurel/Grammar/LaurelGrammar.st @@ -126,6 +126,15 @@ op procedure (name : Ident, parameters: CommaSepBy Parameter, body : Option OptionalBody) : Procedure => "procedure " name "(" parameters ")" returnType returnParameters requires ensures modifies body; +op pureProcedure (name : Ident, parameters: CommaSepBy Parameter, + returnType: Option OptionalReturnType, + returnParameters: Option ReturnParameters, + requires: Option OptionalRequires, + ensures: Seq EnsuresClause, + modifies: Seq ModifiesClause, + body : Option OptionalBody) : Procedure => + "pure procedure " name "(" parameters ")" returnType returnParameters requires ensures modifies body; + category TopLevel; op topLevelComposite(composite: Composite): TopLevel => composite; op topLevelProcedure(procedure: Procedure): TopLevel => procedure; diff --git a/Strata/Languages/Laurel/Laurel.lean b/Strata/Languages/Laurel/Laurel.lean index ab66066a9..f4818e75f 100644 --- a/Strata/Languages/Laurel/Laurel.lean +++ b/Strata/Languages/Laurel/Laurel.lean @@ -93,6 +93,7 @@ structure Procedure : Type where precondition : WithMetadata StmtExpr determinism : Determinism decreases : Option (WithMetadata StmtExpr) -- optionally prove termination + isPure : Bool := false body : Body md : Imperative.MetaData Core.Expression diff --git a/Strata/Languages/Laurel/LaurelFormat.lean b/Strata/Languages/Laurel/LaurelFormat.lean index f7ace1cda..446e88c99 100644 --- a/Strata/Languages/Laurel/LaurelFormat.lean +++ b/Strata/Languages/Laurel/LaurelFormat.lean @@ -159,6 +159,7 @@ def formatBody : Body → Format | .Abstract post => "abstract ensures " ++ formatStmtExpr post def formatProcedure (proc : Procedure) : Format := + (if proc.isPure then "pure " else "") ++ "procedure " ++ Format.text proc.name ++ "(" ++ Format.joinSep (proc.inputs.map formatParameter) ", " ++ ") returns " ++ Format.line ++ "(" ++ Format.joinSep (proc.outputs.map formatParameter) ", " ++ ")" ++ Format.line ++ diff --git a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean b/Strata/Languages/Laurel/LaurelToCoreTranslator.lean index 0d6434be9..8b2c572de 100644 --- a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean +++ b/Strata/Languages/Laurel/LaurelToCoreTranslator.lean @@ -379,7 +379,7 @@ Check if a StmtExpr is a pure expression (can be used as a Core function body). Pure expressions don't contain statements like assignments, loops, or local variables. A Block with a single pure expression is also considered pure. -/ -def isPureExpr(expr: StmtExprMd): Bool := +private def isPureExpr(expr: StmtExprMd): Bool := match _h : expr.val with | .LiteralBool _ => true | .LiteralInt _ => true @@ -396,15 +396,9 @@ def isPureExpr(expr: StmtExprMd): Bool := termination_by sizeOf expr decreasing_by all_goals (have := WithMetadata.sizeOf_val_lt expr; term_by_mem) - -/-- -Check if a procedure can be translated as a Core function. -A procedure can be a function if: -- It has a transparent body that is a pure expression -- It has no precondition (or just `true`) -- It has exactly one output parameter (the return type) --/ -def canBeBoogieFunction (proc : Procedure) : Bool := +/-- Check if a pure-marked procedure can actually be represented as a Core function: + transparent body that is a pure expression, no precondition, exactly one output. -/ +private def canBeCoreFunctionBody (proc : Procedure) : Bool := match proc.body with | .Transparent bodyExpr => isPureExpr bodyExpr && @@ -432,6 +426,21 @@ def translateProcedureToFunction (constants : List Constant) (proc : Procedure) body := body } +/-- +Try to translate a Laurel Procedure marked `isPure` to a Core Function. +Returns `.error` with a diagnostic if the procedure cannot be represented as a Core function +(e.g. it has a non-pure body, a precondition, or multiple outputs). +-/ +def tryTranslatePureToFunction (constants : List Constant) (proc : Procedure) + : Except DiagnosticModel Core.Decl := + let fileRange := (Imperative.getFileRange proc.md).getD FileRange.unknown + if !canBeCoreFunctionBody proc then + .error (DiagnosticModel.withRange fileRange + s!"Pure procedure '{proc.name}' cannot be translated to a Core function. \ + It must have a transparent pure body, no precondition, and exactly one output.") + else + .ok (translateProcedureToFunction constants proc) + /-- Translate Laurel Program to Core Program -/ @@ -445,16 +454,21 @@ def translate (program : Program) : Except (Array DiagnosticModel) (Core.Program -- dbg_trace "=== Program after heapParameterization + modifiesClausesTransform + liftExpressionAssignments ===" -- dbg_trace (toString (Std.Format.pretty (Std.ToFormat.format program))) -- dbg_trace "=================================" - -- Separate procedures that can be functions from those that must be procedures - let (funcProcs, procProcs) := program.staticProcedures.partition canBeBoogieFunction - -- Build the set of function names for use during translation - let funcNames : FunctionNames := funcProcs.map (·.name) + -- Procedures marked isPure are translated to Core functions; all others become Core procedures. + let (markedPure, procProcs) := program.staticProcedures.partition (·.isPure) + -- Try to translate each isPure procedure to a Core function, collecting errors for failures + let (pureErrors, pureFuncDecls) := markedPure.foldl (fun (errs, decls) p => + match tryTranslatePureToFunction program.constants p with + | .error e => (errs.push e, decls) + | .ok d => (errs, decls.push d)) (#[], #[]) + if !pureErrors.isEmpty then + .error pureErrors + let funcNames : FunctionNames := markedPure.map (·.name) let procedures := procProcs.map (translateProcedure program.constants funcNames) let procDecls := procedures.map (fun p => Core.Decl.proc p .empty) - let laurelFuncDecls := funcProcs.map (translateProcedureToFunction program.constants) let constDecls := program.constants.map translateConstant let preludeDecls := corePrelude.decls - pure ({ decls := preludeDecls ++ constDecls ++ laurelFuncDecls ++ procDecls }, modifiesDiags) + pure ({ decls := preludeDecls ++ constDecls ++ pureFuncDecls.toList ++ procDecls }, modifiesDiags) /-- Verify a Laurel program using an SMT solver diff --git a/Strata/Languages/Laurel/LiftExpressionAssignments.lean b/Strata/Languages/Laurel/LiftExpressionAssignments.lean index 3b9f1f375..09273aa44 100644 --- a/Strata/Languages/Laurel/LiftExpressionAssignments.lean +++ b/Strata/Languages/Laurel/LiftExpressionAssignments.lean @@ -78,6 +78,8 @@ structure LiftState where types : List TypeDefinition := [] /-- Global counter for fresh conditional variables -/ condCounter : Nat := 0 + /-- Names of non-pure procedures whose calls must be lifted from expression position -/ + nonPureNames : List Identifier := [] abbrev LiftM := StateM LiftState @@ -129,18 +131,21 @@ private def computeType (expr : StmtExprMd) : LiftM HighTypeMd := do let s ← get return computeExprType s.env s.types expr -/-- Check if an expression contains any assignments (recursively). -/ -private def containsAssignment (expr : StmtExprMd) : Bool := +/-- Check if an expression contains any assignments or non-pure calls (recursively). -/ +private def containsAssignmentOrNonPureCall (nonPureNames : List Identifier) (expr : StmtExprMd) : Bool := match expr with | WithMetadata.mk val _ => match val with | .Assign .. => true - | .StaticCall _ args1 => args1.attach.any (fun x => containsAssignment x.val) - | .PrimitiveOp _ args2 => args2.attach.any (fun x => containsAssignment x.val) - | .Block stmts _ => stmts.attach.any (fun x => containsAssignment x.val) + | .StaticCall name args1 => + nonPureNames.contains name || + args1.attach.any (fun x => containsAssignmentOrNonPureCall nonPureNames x.val) + | .PrimitiveOp _ args2 => args2.attach.any (fun x => containsAssignmentOrNonPureCall nonPureNames x.val) + | .Block stmts _ => stmts.attach.any (fun x => containsAssignmentOrNonPureCall nonPureNames x.val) | .IfThenElse cond th el => - containsAssignment cond || containsAssignment th || - match el with | some e => containsAssignment e | none => false + containsAssignmentOrNonPureCall nonPureNames cond || + containsAssignmentOrNonPureCall nonPureNames th || + match el with | some e => containsAssignmentOrNonPureCall nonPureNames e | none => false | _ => false termination_by expr decreasing_by @@ -200,13 +205,26 @@ def transformExpr (expr : StmtExprMd) : LiftM StmtExprMd := do return ⟨.PrimitiveOp op seqArgs.reverse, md⟩ | .StaticCall name args => + let nonPure := (← get).nonPureNames let seqArgs ← args.reverse.mapM transformExpr - return ⟨.StaticCall name seqArgs.reverse, md⟩ + let seqCall := ⟨.StaticCall name seqArgs.reverse, md⟩ + if nonPure.contains name then + -- Non-pure call in expression position: lift it like an assignment + -- Order matters: assign must be prepended first (it's newest-first), + -- so that when reversed the var declaration comes before the call. + let callResultVar ← freshCondVar + let callResultType ← computeType expr + addPrepend (⟨.Assign [bare (.Identifier callResultVar)] seqCall, md⟩) + addPrepend (bare (.LocalVariable callResultVar callResultType none)) + return bare (.Identifier callResultVar) + else + return seqCall | .IfThenElse cond thenBranch elseBranch => - let thenHasAssign := containsAssignment thenBranch + let nonPure := (← get).nonPureNames + let thenHasAssign := containsAssignmentOrNonPureCall nonPure thenBranch let elseHasAssign := match elseBranch with - | some e => containsAssignment e + | some e => containsAssignmentOrNonPureCall nonPure e | none => false if thenHasAssign || elseHasAssign then -- Lift the entire if-then-else. Introduce a fresh variable for the result. @@ -341,18 +359,51 @@ def transformStmt (stmt : StmtExprMd) : LiftM (List StmtExprMd) := do addToEnv name ty match initializer with | some initExpr => - let seqInit ← transformExpr initExpr - let prepends ← takePrepends - modify fun s => { s with subst := [] } - return prepends ++ [⟨.LocalVariable name ty (some seqInit), md⟩] + -- If the initializer is a direct non-pure StaticCall, don't lift it — + -- translateStmt handles LocalVariable + StaticCall directly as a call statement. + match initExpr.val with + | .StaticCall callee args => + let nonPure := (← get).nonPureNames + if nonPure.contains callee then + -- Pass through as-is; translateStmt will emit init + call + let seqArgs ← args.mapM transformExpr + let argPrepends ← takePrepends + modify fun s => { s with subst := [] } + return argPrepends ++ [⟨.LocalVariable name ty (some ⟨.StaticCall callee seqArgs, initExpr.md⟩), md⟩] + else + let seqInit ← transformExpr initExpr + let prepends ← takePrepends + modify fun s => { s with subst := [] } + return prepends ++ [⟨.LocalVariable name ty (some seqInit), md⟩] + | _ => + let seqInit ← transformExpr initExpr + let prepends ← takePrepends + modify fun s => { s with subst := [] } + return prepends ++ [⟨.LocalVariable name ty (some seqInit), md⟩] | none => return [stmt] | .Assign targets value => - let seqValue ← transformExpr value - let prepends ← takePrepends - modify fun s => { s with subst := [] } - return prepends ++ [⟨.Assign targets seqValue, md⟩] + -- If the RHS is a direct non-pure StaticCall, don't lift it — + -- translateStmt handles Assign + StaticCall directly as a call statement. + match value.val with + | .StaticCall callee args => + let nonPure := (← get).nonPureNames + if nonPure.contains callee then + let seqArgs ← args.mapM transformExpr + let argPrepends ← takePrepends + modify fun s => { s with subst := [] } + return argPrepends ++ [⟨.Assign targets ⟨.StaticCall callee seqArgs, value.md⟩, md⟩] + else + let seqValue ← transformExpr value + let prepends ← takePrepends + modify fun s => { s with subst := [] } + return prepends ++ [⟨.Assign targets seqValue, md⟩] + | _ => + let seqValue ← transformExpr value + let prepends ← takePrepends + modify fun s => { s with subst := [] } + return prepends ++ [⟨.Assign targets seqValue, md⟩] | .IfThenElse cond thenBranch elseBranch => let seqCond ← transformExpr cond @@ -412,7 +463,8 @@ def transformProcedure (proc : Procedure) : LiftM Procedure := do Transform a program to lift all assignments that occur in an expression context. -/ def liftExpressionAssignments (program : Program) : Program := - let initState : LiftState := { types := program.types } + let nonPureNames := program.staticProcedures.filter (fun p => !p.isPure) |>.map (·.name) + let initState : LiftState := { types := program.types, nonPureNames := nonPureNames } let (seqProcedures, _) := (program.staticProcedures.mapM transformProcedure).run initState { program with staticProcedures := seqProcedures } diff --git a/Strata/Languages/Python/PythonToLaurel.lean b/Strata/Languages/Python/PythonToLaurel.lean index 284e73dbe..02f95622e 100644 --- a/Strata/Languages/Python/PythonToLaurel.lean +++ b/Strata/Languages/Python/PythonToLaurel.lean @@ -501,6 +501,7 @@ def translateFunction (ctx : TranslationContext) (f : Python.stmt SourceRange) precondition := mkStmtExprMd (StmtExpr.LiteralBool true) determinism := .deterministic none -- TODO: need to set reads decreases := none + isPure := false body := Body.Transparent bodyBlock md := default } @@ -579,6 +580,7 @@ def pythonToLaurel (prelude: Core.Program) (pyModule : Python.Command SourceRang precondition := mkStmtExprMd (StmtExpr.LiteralBool true), decreases := none, determinism := .deterministic none --TODO: need to set reads + isPure := false body := .Transparent bodyBlock md := default } diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T5_ProcedureCallsStrataCore.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T5_ProcedureCallsStrataCore.lean index 685e824d5..abf570483 100644 --- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T5_ProcedureCallsStrataCore.lean +++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T5_ProcedureCallsStrataCore.lean @@ -19,7 +19,7 @@ open Strata namespace Strata.Laurel def program := r" -procedure syntacticallyABoogieFunction(x: int): int { +pure procedure syntacticallyABoogieFunction(x: int): int { x + 1 } From 079f5da8efa7ddd70fa37f8e0748c8bfb3fff233 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 23 Feb 2026 15:32:46 +0000 Subject: [PATCH 02/28] Rename --- .../Laurel/LaurelToCoreTranslator.lean | 6 +-- ...nments.lean => LiftImpureExpressions.lean} | 50 +++++++++---------- 2 files changed, 28 insertions(+), 28 deletions(-) rename Strata/Languages/Laurel/{LiftExpressionAssignments.lean => LiftImpureExpressions.lean} (91%) diff --git a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean b/Strata/Languages/Laurel/LaurelToCoreTranslator.lean index 8b2c572de..21ba24c4b 100644 --- a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean +++ b/Strata/Languages/Laurel/LaurelToCoreTranslator.lean @@ -10,7 +10,7 @@ import Strata.Languages.Core.Statement import Strata.Languages.Core.Procedure import Strata.Languages.Core.Options import Strata.Languages.Laurel.Laurel -import Strata.Languages.Laurel.LiftExpressionAssignments +import Strata.Languages.Laurel.LiftImpureExpressions import Strata.Languages.Laurel.HeapParameterization import Strata.Languages.Laurel.LaurelTypes import Strata.Languages.Laurel.ModifiesClauses @@ -450,8 +450,8 @@ def translate (program : Program) : Except (Array DiagnosticModel) (Core.Program dbg_trace "=== Program after heapParameterization + modifiesClausesTransform ===" dbg_trace (toString (Std.Format.pretty (Std.ToFormat.format program))) dbg_trace "=================================" - let program := liftExpressionAssignments program - -- dbg_trace "=== Program after heapParameterization + modifiesClausesTransform + liftExpressionAssignments ===" + let program := liftImpureExpressions program + -- dbg_trace "=== Program after heapParameterization + modifiesClausesTransform + liftImpureExpressions ===" -- dbg_trace (toString (Std.Format.pretty (Std.ToFormat.format program))) -- dbg_trace "=================================" -- Procedures marked isPure are translated to Core functions; all others become Core procedures. diff --git a/Strata/Languages/Laurel/LiftExpressionAssignments.lean b/Strata/Languages/Laurel/LiftImpureExpressions.lean similarity index 91% rename from Strata/Languages/Laurel/LiftExpressionAssignments.lean rename to Strata/Languages/Laurel/LiftImpureExpressions.lean index 09273aa44..a84c686a2 100644 --- a/Strata/Languages/Laurel/LiftExpressionAssignments.lean +++ b/Strata/Languages/Laurel/LiftImpureExpressions.lean @@ -78,8 +78,8 @@ structure LiftState where types : List TypeDefinition := [] /-- Global counter for fresh conditional variables -/ condCounter : Nat := 0 - /-- Names of non-pure procedures whose calls must be lifted from expression position -/ - nonPureNames : List Identifier := [] + /-- Names of impure procedures whose calls must be lifted from expression position -/ + impureNames : List Identifier := [] abbrev LiftM := StateM LiftState @@ -131,21 +131,21 @@ private def computeType (expr : StmtExprMd) : LiftM HighTypeMd := do let s ← get return computeExprType s.env s.types expr -/-- Check if an expression contains any assignments or non-pure calls (recursively). -/ -private def containsAssignmentOrNonPureCall (nonPureNames : List Identifier) (expr : StmtExprMd) : Bool := +/-- Check if an expression contains any assignments or impure calls (recursively). -/ +private def containsAssignmentOrImpureCall (impureNames : List Identifier) (expr : StmtExprMd) : Bool := match expr with | WithMetadata.mk val _ => match val with | .Assign .. => true | .StaticCall name args1 => - nonPureNames.contains name || - args1.attach.any (fun x => containsAssignmentOrNonPureCall nonPureNames x.val) - | .PrimitiveOp _ args2 => args2.attach.any (fun x => containsAssignmentOrNonPureCall nonPureNames x.val) - | .Block stmts _ => stmts.attach.any (fun x => containsAssignmentOrNonPureCall nonPureNames x.val) + impureNames.contains name || + args1.attach.any (fun x => containsAssignmentOrImpureCall impureNames x.val) + | .PrimitiveOp _ args2 => args2.attach.any (fun x => containsAssignmentOrImpureCall impureNames x.val) + | .Block stmts _ => stmts.attach.any (fun x => containsAssignmentOrImpureCall impureNames x.val) | .IfThenElse cond th el => - containsAssignmentOrNonPureCall nonPureNames cond || - containsAssignmentOrNonPureCall nonPureNames th || - match el with | some e => containsAssignmentOrNonPureCall nonPureNames e | none => false + containsAssignmentOrImpureCall impureNames cond || + containsAssignmentOrImpureCall impureNames th || + match el with | some e => containsAssignmentOrImpureCall impureNames e | none => false | _ => false termination_by expr decreasing_by @@ -205,11 +205,11 @@ def transformExpr (expr : StmtExprMd) : LiftM StmtExprMd := do return ⟨.PrimitiveOp op seqArgs.reverse, md⟩ | .StaticCall name args => - let nonPure := (← get).nonPureNames + let impure := (← get).impureNames let seqArgs ← args.reverse.mapM transformExpr let seqCall := ⟨.StaticCall name seqArgs.reverse, md⟩ - if nonPure.contains name then - -- Non-pure call in expression position: lift it like an assignment + if impure.contains name then + -- Impure call in expression position: lift it like an assignment -- Order matters: assign must be prepended first (it's newest-first), -- so that when reversed the var declaration comes before the call. let callResultVar ← freshCondVar @@ -221,10 +221,10 @@ def transformExpr (expr : StmtExprMd) : LiftM StmtExprMd := do return seqCall | .IfThenElse cond thenBranch elseBranch => - let nonPure := (← get).nonPureNames - let thenHasAssign := containsAssignmentOrNonPureCall nonPure thenBranch + let impure := (← get).impureNames + let thenHasAssign := containsAssignmentOrImpureCall impure thenBranch let elseHasAssign := match elseBranch with - | some e => containsAssignmentOrNonPureCall nonPure e + | some e => containsAssignmentOrImpureCall impure e | none => false if thenHasAssign || elseHasAssign then -- Lift the entire if-then-else. Introduce a fresh variable for the result. @@ -363,8 +363,8 @@ def transformStmt (stmt : StmtExprMd) : LiftM (List StmtExprMd) := do -- translateStmt handles LocalVariable + StaticCall directly as a call statement. match initExpr.val with | .StaticCall callee args => - let nonPure := (← get).nonPureNames - if nonPure.contains callee then + let impure := (← get).impureNames + if impure.contains callee then -- Pass through as-is; translateStmt will emit init + call let seqArgs ← args.mapM transformExpr let argPrepends ← takePrepends @@ -384,12 +384,12 @@ def transformStmt (stmt : StmtExprMd) : LiftM (List StmtExprMd) := do return [stmt] | .Assign targets value => - -- If the RHS is a direct non-pure StaticCall, don't lift it — + -- If the RHS is a direct impure StaticCall, don't lift it — -- translateStmt handles Assign + StaticCall directly as a call statement. match value.val with | .StaticCall callee args => - let nonPure := (← get).nonPureNames - if nonPure.contains callee then + let impure := (← get).impureNames + if impure.contains callee then let seqArgs ← args.mapM transformExpr let argPrepends ← takePrepends modify fun s => { s with subst := [] } @@ -462,9 +462,9 @@ def transformProcedure (proc : Procedure) : LiftM Procedure := do /-- Transform a program to lift all assignments that occur in an expression context. -/ -def liftExpressionAssignments (program : Program) : Program := - let nonPureNames := program.staticProcedures.filter (fun p => !p.isPure) |>.map (·.name) - let initState : LiftState := { types := program.types, nonPureNames := nonPureNames } +def liftImpureExpressions (program : Program) : Program := + let impureNames := program.staticProcedures.filter (fun p => !p.isPure) |>.map (·.name) + let initState : LiftState := { types := program.types, impureNames := impureNames } let (seqProcedures, _) := (program.staticProcedures.mapM transformProcedure).run initState { program with staticProcedures := seqProcedures } From 4a9dad21661dab0a7c327659f04f5532e456231c Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 23 Feb 2026 15:38:33 +0000 Subject: [PATCH 03/28] Add additinal tests --- .../Fundamentals/T2_ImpureExpressions.lean | 28 +++++++++++++++++++ 1 file changed, 28 insertions(+) diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean index fd839edf7..d37b7e0ee 100644 --- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean +++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean @@ -66,6 +66,34 @@ procedure nestedImpureStatementsAndOpaque() //^^^^^^^^^^^^^^ error: assertion does not hold assert z == y; } + +-- An impure procedure call in expression position is lifted before the +-- surrounding expression is evaluated. +procedure impureProc(x: int) returns (r: int) { + r := r + 1; + return; +} + +procedure impureCallInExpressionPosition() { + var x: int := 0; + -- impureProc(x) is lifted out; its argument is evaluated before the call, + -- so the result is 1 (impureProc(0)), and x is still 0 afterwards. + var y: int := impureProc(x) + x; + assert y == 1; + assert x == 0; +} + +-- An impure call inside a conditional expression is also lifted. +procedure impureCallInConditionalExpression(b: bool) { + var counter: int := 0; + -- The impure call in the then-branch is lifted out of the expression. + var result: int := (if (b) { impureProc(counter); } else { 0 }) + counter; + if (b) { + assert result == 1; + } else { + assert result == 0; + } +} " #guard_msgs (error, drop all) in From 6b2d31f155ecf2e391d977e081db8d99f199647e Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 23 Feb 2026 16:15:11 +0000 Subject: [PATCH 04/28] Parser stuck fix --- Strata/DDM/Elab.lean | 5 ++ .../Laurel/LaurelToCoreTranslator.lean | 6 +-- ...ns.lean => LiftImperativeExpressions.lean} | 52 +++++++++---------- .../Fundamentals/T2_ImpureExpressions.lean | 22 ++++---- 4 files changed, 45 insertions(+), 40 deletions(-) rename Strata/Languages/Laurel/{LiftImpureExpressions.lean => LiftImperativeExpressions.lean} (90%) diff --git a/Strata/DDM/Elab.lean b/Strata/DDM/Elab.lean index a14f09015..5c7f97612 100644 --- a/Strata/DDM/Elab.lean +++ b/Strata/DDM/Elab.lean @@ -71,6 +71,11 @@ private partial def runCommand (leanEnv : Lean.Environment) (commands : Array Op return commands let (some tree, true) ← runChecked <| elabCommand leanEnv | return commands + -- Prevent infinite loop if parser makes no progress + let newPos := (←get).pos + if newPos <= iniPos then + logError { start := iniPos, stop := iniPos } "Syntax error: unrecognized syntax or unexpected token" + return commands let cmd := tree.info.asOp!.op let dialects := (← read).loader.dialects modify fun s => { s with diff --git a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean b/Strata/Languages/Laurel/LaurelToCoreTranslator.lean index 21ba24c4b..cd6dbd8e5 100644 --- a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean +++ b/Strata/Languages/Laurel/LaurelToCoreTranslator.lean @@ -10,7 +10,7 @@ import Strata.Languages.Core.Statement import Strata.Languages.Core.Procedure import Strata.Languages.Core.Options import Strata.Languages.Laurel.Laurel -import Strata.Languages.Laurel.LiftImpureExpressions +import Strata.Languages.Laurel.LiftImperativeExpressions import Strata.Languages.Laurel.HeapParameterization import Strata.Languages.Laurel.LaurelTypes import Strata.Languages.Laurel.ModifiesClauses @@ -450,8 +450,8 @@ def translate (program : Program) : Except (Array DiagnosticModel) (Core.Program dbg_trace "=== Program after heapParameterization + modifiesClausesTransform ===" dbg_trace (toString (Std.Format.pretty (Std.ToFormat.format program))) dbg_trace "=================================" - let program := liftImpureExpressions program - -- dbg_trace "=== Program after heapParameterization + modifiesClausesTransform + liftImpureExpressions ===" + let program := liftImperativeExpressions program + -- dbg_trace "=== Program after heapParameterization + modifiesClausesTransform + liftImperativeExpressions ===" -- dbg_trace (toString (Std.Format.pretty (Std.ToFormat.format program))) -- dbg_trace "=================================" -- Procedures marked isPure are translated to Core functions; all others become Core procedures. diff --git a/Strata/Languages/Laurel/LiftImpureExpressions.lean b/Strata/Languages/Laurel/LiftImperativeExpressions.lean similarity index 90% rename from Strata/Languages/Laurel/LiftImpureExpressions.lean rename to Strata/Languages/Laurel/LiftImperativeExpressions.lean index a84c686a2..0985147ff 100644 --- a/Strata/Languages/Laurel/LiftImpureExpressions.lean +++ b/Strata/Languages/Laurel/LiftImperativeExpressions.lean @@ -78,8 +78,8 @@ structure LiftState where types : List TypeDefinition := [] /-- Global counter for fresh conditional variables -/ condCounter : Nat := 0 - /-- Names of impure procedures whose calls must be lifted from expression position -/ - impureNames : List Identifier := [] + /-- Names of imperative procedures whose calls must be lifted from expression position -/ + imperativeNames : List Identifier := [] abbrev LiftM := StateM LiftState @@ -131,21 +131,21 @@ private def computeType (expr : StmtExprMd) : LiftM HighTypeMd := do let s ← get return computeExprType s.env s.types expr -/-- Check if an expression contains any assignments or impure calls (recursively). -/ -private def containsAssignmentOrImpureCall (impureNames : List Identifier) (expr : StmtExprMd) : Bool := +/-- Check if an expression contains any assignments or imperative calls (recursively). -/ +private def containsAssignmentOrImperativeCall (imperativeNames : List Identifier) (expr : StmtExprMd) : Bool := match expr with | WithMetadata.mk val _ => match val with | .Assign .. => true | .StaticCall name args1 => - impureNames.contains name || - args1.attach.any (fun x => containsAssignmentOrImpureCall impureNames x.val) - | .PrimitiveOp _ args2 => args2.attach.any (fun x => containsAssignmentOrImpureCall impureNames x.val) - | .Block stmts _ => stmts.attach.any (fun x => containsAssignmentOrImpureCall impureNames x.val) + imperativeNames.contains name || + args1.attach.any (fun x => containsAssignmentOrImperativeCall imperativeNames x.val) + | .PrimitiveOp _ args2 => args2.attach.any (fun x => containsAssignmentOrImperativeCall imperativeNames x.val) + | .Block stmts _ => stmts.attach.any (fun x => containsAssignmentOrImperativeCall imperativeNames x.val) | .IfThenElse cond th el => - containsAssignmentOrImpureCall impureNames cond || - containsAssignmentOrImpureCall impureNames th || - match el with | some e => containsAssignmentOrImpureCall impureNames e | none => false + containsAssignmentOrImperativeCall imperativeNames cond || + containsAssignmentOrImperativeCall imperativeNames th || + match el with | some e => containsAssignmentOrImperativeCall imperativeNames e | none => false | _ => false termination_by expr decreasing_by @@ -205,11 +205,11 @@ def transformExpr (expr : StmtExprMd) : LiftM StmtExprMd := do return ⟨.PrimitiveOp op seqArgs.reverse, md⟩ | .StaticCall name args => - let impure := (← get).impureNames + let imperative := (← get).imperativeNames let seqArgs ← args.reverse.mapM transformExpr let seqCall := ⟨.StaticCall name seqArgs.reverse, md⟩ - if impure.contains name then - -- Impure call in expression position: lift it like an assignment + if imperative.contains name then + -- Imperative call in expression position: lift it like an assignment -- Order matters: assign must be prepended first (it's newest-first), -- so that when reversed the var declaration comes before the call. let callResultVar ← freshCondVar @@ -221,10 +221,10 @@ def transformExpr (expr : StmtExprMd) : LiftM StmtExprMd := do return seqCall | .IfThenElse cond thenBranch elseBranch => - let impure := (← get).impureNames - let thenHasAssign := containsAssignmentOrImpureCall impure thenBranch + let imperative := (← get).imperativeNames + let thenHasAssign := containsAssignmentOrImperativeCall imperative thenBranch let elseHasAssign := match elseBranch with - | some e => containsAssignmentOrImpureCall impure e + | some e => containsAssignmentOrImperativeCall imperative e | none => false if thenHasAssign || elseHasAssign then -- Lift the entire if-then-else. Introduce a fresh variable for the result. @@ -359,12 +359,12 @@ def transformStmt (stmt : StmtExprMd) : LiftM (List StmtExprMd) := do addToEnv name ty match initializer with | some initExpr => - -- If the initializer is a direct non-pure StaticCall, don't lift it — + -- If the initializer is a direct imperative StaticCall, don't lift it — -- translateStmt handles LocalVariable + StaticCall directly as a call statement. match initExpr.val with | .StaticCall callee args => - let impure := (← get).impureNames - if impure.contains callee then + let imperative := (← get).imperativeNames + if imperative.contains callee then -- Pass through as-is; translateStmt will emit init + call let seqArgs ← args.mapM transformExpr let argPrepends ← takePrepends @@ -384,12 +384,12 @@ def transformStmt (stmt : StmtExprMd) : LiftM (List StmtExprMd) := do return [stmt] | .Assign targets value => - -- If the RHS is a direct impure StaticCall, don't lift it — + -- If the RHS is a direct imperative StaticCall, don't lift it — -- translateStmt handles Assign + StaticCall directly as a call statement. match value.val with | .StaticCall callee args => - let impure := (← get).impureNames - if impure.contains callee then + let imperative := (← get).imperativeNames + if imperative.contains callee then let seqArgs ← args.mapM transformExpr let argPrepends ← takePrepends modify fun s => { s with subst := [] } @@ -462,9 +462,9 @@ def transformProcedure (proc : Procedure) : LiftM Procedure := do /-- Transform a program to lift all assignments that occur in an expression context. -/ -def liftImpureExpressions (program : Program) : Program := - let impureNames := program.staticProcedures.filter (fun p => !p.isPure) |>.map (·.name) - let initState : LiftState := { types := program.types, impureNames := impureNames } +def liftImperativeExpressions (program : Program) : Program := + let imperativeNames := program.staticProcedures.filter (fun p => !p.isPure) |>.map (·.name) + let initState : LiftState := { types := program.types, imperativeNames := imperativeNames } let (seqProcedures, _) := (program.staticProcedures.mapM transformProcedure).run initState { program with staticProcedures := seqProcedures } diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean index d37b7e0ee..5fec3367d 100644 --- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean +++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean @@ -67,27 +67,27 @@ procedure nestedImpureStatementsAndOpaque() assert z == y; } --- An impure procedure call in expression position is lifted before the +-- An imperative procedure call in expression position is lifted before the -- surrounding expression is evaluated. -procedure impureProc(x: int) returns (r: int) { +procedure imperativeProc(x: int) returns (r: int) { r := r + 1; - return; + r } -procedure impureCallInExpressionPosition() { +procedure imperativeCallInExpressionPosition() { var x: int := 0; - -- impureProc(x) is lifted out; its argument is evaluated before the call, - -- so the result is 1 (impureProc(0)), and x is still 0 afterwards. - var y: int := impureProc(x) + x; + -- imperativeProc(x) is lifted out; its argument is evaluated before the call, + -- so the result is 1 (imperativeProc(0)), and x is still 0 afterwards. + var y: int := imperativeProc(x) + x; assert y == 1; assert x == 0; } --- An impure call inside a conditional expression is also lifted. -procedure impureCallInConditionalExpression(b: bool) { +-- An imperative call inside a conditional expression is also lifted. +procedure imperativeCallInConditionalExpression(b: bool) { var counter: int := 0; - -- The impure call in the then-branch is lifted out of the expression. - var result: int := (if (b) { impureProc(counter); } else { 0 }) + counter; + -- The imperative call in the then-branch is lifted out of the expression. + var result: int := (if (b) { imperativeProc(counter); } else { 0 }) + counter; if (b) { assert result == 1; } else { From fd5fdf1d5dd6fe0a45c9058ff38ec5145534db44 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 23 Feb 2026 16:25:46 +0000 Subject: [PATCH 05/28] Fixes --- Strata/Languages/Laurel/LaurelTypes.lean | 24 +++++++++++-------- .../Laurel/LiftImperativeExpressions.lean | 7 ++++-- .../Fundamentals/T2_ImpureExpressions.lean | 14 +++++------ 3 files changed, 26 insertions(+), 19 deletions(-) diff --git a/Strata/Languages/Laurel/LaurelTypes.lean b/Strata/Languages/Laurel/LaurelTypes.lean index dfa68c563..4645193ff 100644 --- a/Strata/Languages/Laurel/LaurelTypes.lean +++ b/Strata/Languages/Laurel/LaurelTypes.lean @@ -31,11 +31,12 @@ def lookupFieldInTypes (types : List TypeDefinition) (typeName : Identifier) (fi | _ => none /-- -Compute the HighType of a StmtExpr given a type environment and type definitions. +Compute the HighType of a StmtExpr given a type environment, type definitions, and procedure list. No inference is performed — all types are determined by annotations on parameters and variable declarations. -/ -def computeExprType (env : TypeEnv) (types : List TypeDefinition) (expr : StmtExprMd) : HighTypeMd := +def computeExprType (env : TypeEnv) (types : List TypeDefinition) (expr : StmtExprMd) + (procedures : List Procedure := []) : HighTypeMd := match expr with | WithMetadata.mk val md => match val with @@ -50,16 +51,19 @@ def computeExprType (env : TypeEnv) (types : List TypeDefinition) (expr : StmtEx | none => panic s!"Could not find variable {name} in environment" -- Field access | .FieldSelect target fieldName => - match computeExprType env types target with + match computeExprType env types target procedures with | WithMetadata.mk (.UserDefined typeName) _ => match lookupFieldInTypes types typeName fieldName with | some ty => ty | none => panic s!"Could not find field in type" | _ => panic s!"Selecting from a type that's not a composite" -- Pure field update returns the same type as the target - | .PureFieldUpdate target _ _ => computeExprType env types target - -- Calls — we don't track return types here, so fall back to TVoid - | .StaticCall _ _ => panic "Not supported StaticCall" + | .PureFieldUpdate target _ _ => computeExprType env types target procedures + -- Calls — look up return type from first output of matching procedure + | .StaticCall name _ => + match procedures.find? (·.name == name) with + | some proc => proc.outputs.head?.map (·.type) |>.getD ⟨ .TVoid, md ⟩ + | none => ⟨ .TVoid, md ⟩ | .InstanceCall _ _ _ => panic "Not supported InstanceCall" -- Operators | .PrimitiveOp op _ => @@ -67,11 +71,11 @@ def computeExprType (env : TypeEnv) (types : List TypeDefinition) (expr : StmtEx | .Eq | .Neq | .And | .Or | .Not | .Implies | .Lt | .Leq | .Gt | .Geq => ⟨ .TBool, md ⟩ | .Neg | .Add | .Sub | .Mul | .Div | .Mod | .DivT | .ModT => ⟨ .TInt, md ⟩ -- Control flow - | .IfThenElse _ thenBranch _ => computeExprType env types thenBranch + | .IfThenElse _ thenBranch _ => computeExprType env types thenBranch procedures | .Block stmts _ => match _blockGetLastResult: stmts.getLast? with | some last => have := List.mem_of_getLast? _blockGetLastResult - computeExprType env types last + computeExprType env types last procedures | none => ⟨ .TVoid, md ⟩ -- Statements (void-typed) | .LocalVariable _ _ _ => ⟨ .TVoid, md ⟩ @@ -91,10 +95,10 @@ def computeExprType (env : TypeEnv) (types : List TypeDefinition) (expr : StmtEx | .Forall _ _ _ => ⟨ .TBool, md ⟩ | .Exists _ _ _ => ⟨ .TBool, md ⟩ | .Assigned _ => ⟨ .TBool, md ⟩ - | .Old v => computeExprType env types v + | .Old v => computeExprType env types v procedures | .Fresh _ => ⟨ .TBool, md ⟩ -- Proof related - | .ProveBy v _ => computeExprType env types v + | .ProveBy v _ => computeExprType env types v procedures | .ContractOf _ _ => panic "Not supported" -- Special | .Abstract => panic "Not supported" diff --git a/Strata/Languages/Laurel/LiftImperativeExpressions.lean b/Strata/Languages/Laurel/LiftImperativeExpressions.lean index 0985147ff..8affc8489 100644 --- a/Strata/Languages/Laurel/LiftImperativeExpressions.lean +++ b/Strata/Languages/Laurel/LiftImperativeExpressions.lean @@ -80,6 +80,8 @@ structure LiftState where condCounter : Nat := 0 /-- Names of imperative procedures whose calls must be lifted from expression position -/ imperativeNames : List Identifier := [] + /-- All procedures in the program, used to look up return types of imperative calls -/ + procedures : List Procedure := [] abbrev LiftM := StateM LiftState @@ -129,7 +131,7 @@ private def setSubst (varName : Identifier) (value : Identifier) : LiftM Unit := private def computeType (expr : StmtExprMd) : LiftM HighTypeMd := do let s ← get - return computeExprType s.env s.types expr + return computeExprType s.env s.types expr s.procedures /-- Check if an expression contains any assignments or imperative calls (recursively). -/ private def containsAssignmentOrImperativeCall (imperativeNames : List Identifier) (expr : StmtExprMd) : Bool := @@ -214,6 +216,7 @@ def transformExpr (expr : StmtExprMd) : LiftM StmtExprMd := do -- so that when reversed the var declaration comes before the call. let callResultVar ← freshCondVar let callResultType ← computeType expr + addToEnv callResultVar callResultType addPrepend (⟨.Assign [bare (.Identifier callResultVar)] seqCall, md⟩) addPrepend (bare (.LocalVariable callResultVar callResultType none)) return bare (.Identifier callResultVar) @@ -464,7 +467,7 @@ Transform a program to lift all assignments that occur in an expression context. -/ def liftImperativeExpressions (program : Program) : Program := let imperativeNames := program.staticProcedures.filter (fun p => !p.isPure) |>.map (·.name) - let initState : LiftState := { types := program.types, imperativeNames := imperativeNames } + let initState : LiftState := { types := program.types, imperativeNames := imperativeNames, procedures := program.staticProcedures } let (seqProcedures, _) := (program.staticProcedures.mapM transformProcedure).run initState { program with staticProcedures := seqProcedures } diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean index 5fec3367d..b42c4ab6e 100644 --- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean +++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean @@ -67,8 +67,8 @@ procedure nestedImpureStatementsAndOpaque() assert z == y; } --- An imperative procedure call in expression position is lifted before the --- surrounding expression is evaluated. +// An imperative procedure call in expression position is lifted before the +// surrounding expression is evaluated. procedure imperativeProc(x: int) returns (r: int) { r := r + 1; r @@ -76,18 +76,18 @@ procedure imperativeProc(x: int) returns (r: int) { procedure imperativeCallInExpressionPosition() { var x: int := 0; - -- imperativeProc(x) is lifted out; its argument is evaluated before the call, - -- so the result is 1 (imperativeProc(0)), and x is still 0 afterwards. + // imperativeProc(x) is lifted out; its argument is evaluated before the call, + // so the result is 1 (imperativeProc(0)), and x is still 0 afterwards. var y: int := imperativeProc(x) + x; assert y == 1; assert x == 0; } --- An imperative call inside a conditional expression is also lifted. +// An imperative call inside a conditional expression is also lifted. procedure imperativeCallInConditionalExpression(b: bool) { var counter: int := 0; - -- The imperative call in the then-branch is lifted out of the expression. - var result: int := (if (b) { imperativeProc(counter); } else { 0 }) + counter; + // The imperative call in the then-branch is lifted out of the expression. + var result: int := (if (b) { imperativeProc(counter) } else { 0 }) + counter; if (b) { assert result == 1; } else { From 2defa7cb503a6abcffa816926dac304d18f60a94 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 23 Feb 2026 16:29:14 +0000 Subject: [PATCH 06/28] Fix test --- .../Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean index b42c4ab6e..227e8f7b5 100644 --- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean +++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean @@ -69,8 +69,11 @@ procedure nestedImpureStatementsAndOpaque() // An imperative procedure call in expression position is lifted before the // surrounding expression is evaluated. -procedure imperativeProc(x: int) returns (r: int) { - r := r + 1; +procedure imperativeProc(x: int) returns (r: int) + // ensures clause requires because Core does not support transparent proceduces yet + ensures r == x + 1 +{ + r := x + 1; r } From 2cd09afc3ca564255d48d4c33578973335778a5d Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Tue, 24 Feb 2026 10:00:08 +0000 Subject: [PATCH 07/28] Use function instead of pure procedure --- .../Grammar/ConcreteToAbstractTreeTranslator.lean | 10 +++++----- Strata/Languages/Laurel/Grammar/LaurelGrammar.st | 4 ++-- Strata/Languages/Laurel/Laurel.lean | 2 +- Strata/Languages/Laurel/LaurelFormat.lean | 3 +-- Strata/Languages/Laurel/LaurelToCoreTranslator.lean | 8 ++++---- Strata/Languages/Laurel/LiftImperativeExpressions.lean | 2 +- Strata/Languages/Python/PythonToLaurel.lean | 4 ++-- .../Fundamentals/T5_ProcedureCallsStrataCore.lean | 4 ++-- 8 files changed, 18 insertions(+), 19 deletions(-) diff --git a/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean b/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean index d338547d3..51588466f 100644 --- a/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean +++ b/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean @@ -129,7 +129,7 @@ instance : Inhabited Procedure where precondition := mkStmtExprMdEmpty <| .LiteralBool true determinism := .deterministic none decreases := none - isPure := false + isFunctional := false body := .Transparent ⟨.LiteralBool true, #[]⟩ md := .empty } @@ -324,7 +324,7 @@ def parseProcedure (arg : Arg) : TransM Procedure := do match op.name, op.args with | q`Laurel.procedure, #[nameArg, paramArg, returnTypeArg, returnParamsArg, requiresArg, ensuresArg, modifiesArg, bodyArg] - | q`Laurel.pureProcedure, #[nameArg, paramArg, returnTypeArg, returnParamsArg, + | q`Laurel.function, #[nameArg, paramArg, returnTypeArg, returnParamsArg, requiresArg, ensuresArg, modifiesArg, bodyArg] => let name ← translateIdent nameArg let nameMd ← getArgMetaData nameArg @@ -376,15 +376,15 @@ def parseProcedure (arg : Arg) : TransM Procedure := do precondition := precondition determinism := .deterministic none decreases := none - isPure := op.name == q`Laurel.pureProcedure + isFunctional := op.name == q`Laurel.function body := procBody md := nameMd } | q`Laurel.procedure, args - | q`Laurel.pureProcedure, args => + | q`Laurel.function, args => TransM.error s!"parseProcedure expects 8 arguments, got {args.size}" | _, _ => - TransM.error s!"parseProcedure expects procedure, got {repr op.name}" + TransM.error s!"parseProcedure expects procedure or function, got {repr op.name}" def parseField (arg : Arg) : TransM Field := do let .op op := arg diff --git a/Strata/Languages/Laurel/Grammar/LaurelGrammar.st b/Strata/Languages/Laurel/Grammar/LaurelGrammar.st index b12db3d9d..96178de45 100644 --- a/Strata/Languages/Laurel/Grammar/LaurelGrammar.st +++ b/Strata/Languages/Laurel/Grammar/LaurelGrammar.st @@ -126,14 +126,14 @@ op procedure (name : Ident, parameters: CommaSepBy Parameter, body : Option OptionalBody) : Procedure => "procedure " name "(" parameters ")" returnType returnParameters requires ensures modifies body; -op pureProcedure (name : Ident, parameters: CommaSepBy Parameter, +op function (name : Ident, parameters: CommaSepBy Parameter, returnType: Option OptionalReturnType, returnParameters: Option ReturnParameters, requires: Option OptionalRequires, ensures: Seq EnsuresClause, modifies: Seq ModifiesClause, body : Option OptionalBody) : Procedure => - "pure procedure " name "(" parameters ")" returnType returnParameters requires ensures modifies body; + "function " name "(" parameters ")" returnType returnParameters requires ensures modifies body; category TopLevel; op topLevelComposite(composite: Composite): TopLevel => composite; diff --git a/Strata/Languages/Laurel/Laurel.lean b/Strata/Languages/Laurel/Laurel.lean index 648127bcc..630fa9925 100644 --- a/Strata/Languages/Laurel/Laurel.lean +++ b/Strata/Languages/Laurel/Laurel.lean @@ -137,7 +137,7 @@ structure Procedure : Type where /-- Optional termination measure for recursive procedures. -/ decreases : Option (WithMetadata StmtExpr) -- optionally prove termination /-- If true, the body may only have functional constructs, so no destructive assignments or loops. -/ - isPure : Bool := false + isFunctional : Bool := false /-- The procedure body: transparent, opaque, or abstract. -/ body : Body /-- Source-level metadata. -/ diff --git a/Strata/Languages/Laurel/LaurelFormat.lean b/Strata/Languages/Laurel/LaurelFormat.lean index 446e88c99..35383f563 100644 --- a/Strata/Languages/Laurel/LaurelFormat.lean +++ b/Strata/Languages/Laurel/LaurelFormat.lean @@ -159,8 +159,7 @@ def formatBody : Body → Format | .Abstract post => "abstract ensures " ++ formatStmtExpr post def formatProcedure (proc : Procedure) : Format := - (if proc.isPure then "pure " else "") ++ - "procedure " ++ Format.text proc.name ++ + (if proc.isFunctional then "function " else "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 ++ diff --git a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean b/Strata/Languages/Laurel/LaurelToCoreTranslator.lean index cd6dbd8e5..b106cb86e 100644 --- a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean +++ b/Strata/Languages/Laurel/LaurelToCoreTranslator.lean @@ -427,7 +427,7 @@ def translateProcedureToFunction (constants : List Constant) (proc : Procedure) } /-- -Try to translate a Laurel Procedure marked `isPure` to a Core Function. +Try to translate a Laurel Procedure marked `isFunctional` to a Core Function. Returns `.error` with a diagnostic if the procedure cannot be represented as a Core function (e.g. it has a non-pure body, a precondition, or multiple outputs). -/ @@ -454,9 +454,9 @@ def translate (program : Program) : Except (Array DiagnosticModel) (Core.Program -- dbg_trace "=== Program after heapParameterization + modifiesClausesTransform + liftImperativeExpressions ===" -- dbg_trace (toString (Std.Format.pretty (Std.ToFormat.format program))) -- dbg_trace "=================================" - -- Procedures marked isPure are translated to Core functions; all others become Core procedures. - let (markedPure, procProcs) := program.staticProcedures.partition (·.isPure) - -- Try to translate each isPure procedure to a Core function, collecting errors for failures + -- Procedures marked isFunctional are translated to Core functions; all others become Core procedures. + let (markedPure, procProcs) := program.staticProcedures.partition (·.isFunctional) + -- Try to translate each isFunctional procedure to a Core function, collecting errors for failures let (pureErrors, pureFuncDecls) := markedPure.foldl (fun (errs, decls) p => match tryTranslatePureToFunction program.constants p with | .error e => (errs.push e, decls) diff --git a/Strata/Languages/Laurel/LiftImperativeExpressions.lean b/Strata/Languages/Laurel/LiftImperativeExpressions.lean index 8affc8489..838dd454f 100644 --- a/Strata/Languages/Laurel/LiftImperativeExpressions.lean +++ b/Strata/Languages/Laurel/LiftImperativeExpressions.lean @@ -466,7 +466,7 @@ def transformProcedure (proc : Procedure) : LiftM Procedure := do Transform a program to lift all assignments that occur in an expression context. -/ def liftImperativeExpressions (program : Program) : Program := - let imperativeNames := program.staticProcedures.filter (fun p => !p.isPure) |>.map (·.name) + let imperativeNames := program.staticProcedures.filter (fun p => !p.isFunctional) |>.map (·.name) let initState : LiftState := { types := program.types, imperativeNames := imperativeNames, procedures := program.staticProcedures } let (seqProcedures, _) := (program.staticProcedures.mapM transformProcedure).run initState { program with staticProcedures := seqProcedures } diff --git a/Strata/Languages/Python/PythonToLaurel.lean b/Strata/Languages/Python/PythonToLaurel.lean index 02f95622e..948c95af8 100644 --- a/Strata/Languages/Python/PythonToLaurel.lean +++ b/Strata/Languages/Python/PythonToLaurel.lean @@ -501,7 +501,7 @@ def translateFunction (ctx : TranslationContext) (f : Python.stmt SourceRange) precondition := mkStmtExprMd (StmtExpr.LiteralBool true) determinism := .deterministic none -- TODO: need to set reads decreases := none - isPure := false + isFunctional := false body := Body.Transparent bodyBlock md := default } @@ -580,7 +580,7 @@ def pythonToLaurel (prelude: Core.Program) (pyModule : Python.Command SourceRang precondition := mkStmtExprMd (StmtExpr.LiteralBool true), decreases := none, determinism := .deterministic none --TODO: need to set reads - isPure := false + isFunctional := false body := .Transparent bodyBlock md := default } diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T5_ProcedureCallsStrataCore.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T5_ProcedureCallsStrataCore.lean index abf570483..a77b6777b 100644 --- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T5_ProcedureCallsStrataCore.lean +++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T5_ProcedureCallsStrataCore.lean @@ -19,7 +19,7 @@ open Strata namespace Strata.Laurel def program := r" -pure procedure syntacticallyABoogieFunction(x: int): int { +function aFunction(x: int): int { x + 1 } @@ -35,7 +35,7 @@ procedure noFunctionBecauseStatements(): int { } procedure caller() { - assert syntacticallyABoogieFunction(1) == 2; + assert aFunction(1) == 2; var x: int := noFunctionBecauseContract(); assert x > 0; var y: int := noFunctionBecauseStatements(); From ffa62ed325c61efb1d07faae0b4e30e31ce04d92 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Tue, 24 Feb 2026 10:15:56 +0000 Subject: [PATCH 08/28] Fix docs --- docs/verso/LaurelDoc.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/verso/LaurelDoc.lean b/docs/verso/LaurelDoc.lean index 889a9f64e..b1abaa274 100644 --- a/docs/verso/LaurelDoc.lean +++ b/docs/verso/LaurelDoc.lean @@ -10,7 +10,7 @@ import Strata.Languages.Laurel.Laurel import Strata.Languages.Laurel.LaurelTypes import Strata.Languages.Laurel.LaurelToCoreTranslator import Strata.Languages.Laurel.HeapParameterization -import Strata.Languages.Laurel.LiftExpressionAssignments +import Strata.Languages.Laurel.LiftImperativeExpressions import Strata.Languages.Laurel.ModifiesClauses import Strata.Languages.Laurel.CorePrelude From 65082fac8b4635d6153c84cb110a7fbf719932d3 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 25 Feb 2026 12:00:00 +0000 Subject: [PATCH 09/28] Add more checks to LaurelToCoreTranslator.lean --- .../Laurel/LaurelToCoreTranslator.lean | 292 +++++++++++------- .../Fundamentals/T2_ImpureExpressions.lean | 2 +- .../T2_ImpureExpressionsError.lean | 55 ++++ 3 files changed, 239 insertions(+), 110 deletions(-) create mode 100644 StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressionsError.lean diff --git a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean b/Strata/Languages/Laurel/LaurelToCoreTranslator.lean index b106cb86e..b6ac5587b 100644 --- a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean +++ b/Strata/Languages/Laurel/LaurelToCoreTranslator.lean @@ -68,43 +68,70 @@ def isCoreFunction (funcNames : FunctionNames) (name : Identifier) : Bool := funcNames.contains name /-- -Translate Laurel StmtExpr to Core Expression. +Translate Laurel StmtExpr to Core Expression, also returning any diagnostics for disallowed +constructs (assignments, loops, procedure calls) that are not valid in expression position. + +`isPureContext` should be `true` when translating function bodies or contract expressions. +In that case, disallowed constructs emit `DiagnosticModel` +errors. When `false` (inside a procedure body statement), disallowed constructs `panic!` +because `liftImperativeExpressions` should have already removed them. `boundVars` tracks names bound by enclosing Forall/Exists quantifiers (innermost first). When an Identifier matches a bound name at index `i`, it becomes `bvar i` (de Bruijn index) instead of `fvar`. -/ -def translateExpr (constants : List Constant) (env : TypeEnv) (expr : StmtExprMd) - (boundVars : List Identifier := []) : Core.Expression.Expr := +def translateExpr (constants : List Constant) (funcNames : FunctionNames) (env : TypeEnv) (expr : StmtExprMd) + (boundVars : List Identifier := []) (isPureContext : Bool := false) + : Core.Expression.Expr × List DiagnosticModel := + -- Dummy expression used as placeholder when an error is emitted in pure context + let dummy := .fvar () (Core.CoreIdent.locl s!"DUMMY_VAR_{env.length}") none + -- Emit an error in pure context; panic in impure context (lifting invariant violated) + let disallowed (e : StmtExprMd) (msg : String) : Core.Expression.Expr × List DiagnosticModel := + if isPureContext then + (dummy, [e.md.toDiagnostic msg]) + else + panic! s!"translateExpr: {msg} (should have been lifted): {Std.Format.pretty (Std.ToFormat.format e)}" + -- Helper: combine diagnostics from two translated sub-expressions + let combine2 (r1 r2 : Core.Expression.Expr × List DiagnosticModel) + (f : Core.Expression.Expr → Core.Expression.Expr → Core.Expression.Expr) + : Core.Expression.Expr × List DiagnosticModel := + (f r1.1 r2.1, r1.2 ++ r2.2) match h: expr.val with - | .LiteralBool b => .const () (.boolConst b) - | .LiteralInt i => .const () (.intConst i) - | .LiteralString s => .const () (.strConst s) + | .LiteralBool b => (.const () (.boolConst b), []) + | .LiteralInt i => (.const () (.intConst i), []) + | .LiteralString s => (.const () (.strConst s), []) | .Identifier name => -- First check if this name is bound by an enclosing quantifier match boundVars.findIdx? (· == name) with | some idx => -- Bound variable: use de Bruijn index - .bvar () idx + (.bvar () idx, []) | none => -- Check if this is a constant (field constant) or local variable if isConstant constants name then let ident := Core.CoreIdent.unres name - .op () ident none + (.op () ident none, []) else let ident := Core.CoreIdent.locl name - .fvar () ident (some (lookupType env name)) + (.fvar () ident (some (lookupType env name)), []) | .PrimitiveOp op [e] => match op with - | .Not => .app () boolNotOp (translateExpr constants env e boundVars) - | .Neg => .app () intNegOp (translateExpr constants env e boundVars) + | .Not => + let (re, ds) := translateExpr constants funcNames env e boundVars isPureContext + (.app () boolNotOp re, ds) + | .Neg => + let (re, ds) := translateExpr constants funcNames env e boundVars isPureContext + (.app () intNegOp re, ds) | _ => panic! s!"translateExpr: Invalid unary op: {repr op}" | .PrimitiveOp op [e1, e2] => - let binOp (bop : Core.Expression.Expr): Core.Expression.Expr := - LExpr.mkApp () bop [translateExpr constants env e1 boundVars, translateExpr constants env e2 boundVars] + let (re1, ds1) := translateExpr constants funcNames env e1 boundVars isPureContext + let (re2, ds2) := translateExpr constants funcNames env e2 boundVars isPureContext + let ds := ds1 ++ ds2 + let binOp (bop : Core.Expression.Expr) : Core.Expression.Expr × List DiagnosticModel := + (LExpr.mkApp () bop [re1, re2], ds) match op with - | .Eq => .eq () (translateExpr constants env e1 boundVars) (translateExpr constants env e2 boundVars) - | .Neq => .app () boolNotOp (.eq () (translateExpr constants env e1 boundVars) (translateExpr constants env e2 boundVars)) + | .Eq => (.eq () re1 re2, ds) + | .Neq => (.app () boolNotOp (.eq () re1 re2), ds) | .And => binOp boolAndOp | .Or => binOp boolOrOp | .Implies => binOp boolImpliesOp @@ -123,32 +150,72 @@ def translateExpr (constants : List Constant) (env : TypeEnv) (expr : StmtExprMd | .PrimitiveOp op args => panic! s!"translateExpr: PrimitiveOp {repr op} with {args.length} args" | .IfThenElse cond thenBranch elseBranch => - let bcond := translateExpr constants env cond boundVars - let bthen := translateExpr constants env thenBranch boundVars - let belse := match elseBranch with - | some e => translateExpr constants env e boundVars - | none => .const () (.intConst 0) - .ite () bcond bthen belse - | .Assign _ value => translateExpr constants env value boundVars + let (bcond, ds0) := translateExpr constants funcNames env cond boundVars isPureContext + let (bthen, ds1) := translateExpr constants funcNames env thenBranch boundVars isPureContext + let (belse, ds2) : Core.Expression.Expr × List DiagnosticModel := + match elseBranch with + | none => panic "if-then without else expression not yet implemented" + | some e => + have : sizeOf e < sizeOf expr := by + have := WithMetadata.sizeOf_val_lt expr + cases expr; simp_all; omega + translateExpr constants funcNames env e boundVars isPureContext + (.ite () bcond bthen belse, ds0 ++ ds1 ++ ds2) | .StaticCall name args => - let ident := Core.CoreIdent.unres name - let fnOp := .op () ident none - args.foldl (fun acc arg => .app () acc (translateExpr constants env arg boundVars)) fnOp - | .Block [single] _ => translateExpr constants env single boundVars + -- In a pure context, only Core functions (not procedures) are allowed + if isPureContext && !isCoreFunction funcNames name then + disallowed expr "calls to procedures are not supported in functions or contracts" + else + let ident := Core.CoreIdent.unres name + let fnOp := .op () ident none + let (result, ds) := args.attach.foldl (fun (acc, accDs) ⟨arg, _⟩ => + let (re, ds) := translateExpr constants funcNames env arg boundVars isPureContext + (.app () acc re, accDs ++ ds)) (fnOp, []) + (result, ds) + | .Block [single] _ => translateExpr constants funcNames env single boundVars isPureContext + | .Block _ _ => panic "block expression not yet implemented" + | .LocalVariable _ _ _ => panic "local variable expression not yet implemented" + | .Return _ => disallowed expr "return expression not yet implemented" + | .Forall name ty body => let coreTy := translateType ty - let coreBody := translateExpr constants env body (name :: boundVars) - LExpr.all () (some coreTy) coreBody + let (coreBody, ds) := translateExpr constants funcNames env body (name :: boundVars) isPureContext + (LExpr.all () (some coreTy) coreBody, ds) | .Exists name ty body => let coreTy := translateType ty - let coreBody := translateExpr constants env body (name :: boundVars) - LExpr.exist () (some coreTy) coreBody + let (coreBody, ds) := translateExpr constants funcNames env body (name :: boundVars) isPureContext + (LExpr.exist () (some coreTy) coreBody, ds) + | .Hole => (dummy, []) + | .ReferenceEquals e1 e2 => + combine2 (translateExpr constants funcNames env e1 boundVars isPureContext) + (translateExpr constants funcNames env e2 boundVars isPureContext) + (fun l r => .eq () l r) + | .Assign _ _ => + disallowed expr "destructive assignments are not supported in functions or contracts" + | .While _ _ _ _ => + disallowed expr "loops are not supported in functions or contracts" + | .Exit _ => disallowed expr "exit is not supported in expression position" + + | .IsType _ _ => panic "IsType should have been lowered" | .FieldSelect target fieldName => -- Field selects should have been eliminated by heap parameterization -- If we see one here, it's an error in the pipeline panic! s!"FieldSelect should have been eliminated by heap parameterization: {Std.ToFormat.format target}#{fieldName}" - | .Hole => .fvar () (Core.CoreIdent.locl s!"DUMMY_VAR_{env.length}") none -- TODO: don't do this - | _ => panic! Std.Format.pretty (Std.ToFormat.format expr) + + | .AsType target _ => panic "AsType expression not implemented" + | .Assigned _ => panic "assigned expression not implemented" + | .Old value => panic "old expression not implemented" + | .Fresh _ => panic "fresh expression not implemented" + | .Assert _ => panic "assert expression not implemented" + | .Assume _ => panic "assume expression not implemented" + | .ProveBy value _ => panic "proveBy expression not implemented" + | .ContractOf _ _ => panic "contractOf expression not implemented" + | .Abstract => panic "abstract expression not implemented" + | .All => panic "all expression not implemented" + | .InstanceCall _ _ _ => panic "InstanceCall not implemented" + | .PureFieldUpdate _ _ _ => panic "This expression not implemented" + | .New _ => panic "New expression not implemented" + | .This => panic "This expression not implemented" termination_by expr decreasing_by all_goals (have := WithMetadata.sizeOf_val_lt expr; term_by_mem) @@ -173,19 +240,20 @@ def defaultExprForType (ty : HighTypeMd) : Core.Expression.Expr := Translate Laurel StmtExpr to Core Statements Takes the constants list, type environment, output parameter names, and set of function names -/ -def translateStmt (constants : List Constant) (funcNames : FunctionNames) (env : TypeEnv) +def translateStmt (constants : List Constant) (functionNames : FunctionNames) (env : TypeEnv) (outputParams : List Parameter) (stmt : StmtExprMd) : TypeEnv × List Core.Statement := let md := stmt.md match h : stmt.val with | @StmtExpr.Assert cond => - let boogieExpr := translateExpr constants env cond - (env, [Core.Statement.assert ("assert" ++ getNameFromMd md) boogieExpr md]) + -- Assert/assume bodies must be pure expressions (no assignments, loops, or procedure calls) + let (coreExpr, _) := translateExpr constants functionNames env cond [] (isPureContext := true) + (env, [Core.Statement.assert ("assert" ++ getNameFromMd md) coreExpr md]) | @StmtExpr.Assume cond => - let boogieExpr := translateExpr constants env cond - (env, [Core.Statement.assume ("assume" ++ getNameFromMd md) boogieExpr md]) + let (coreExpr, _) := translateExpr constants functionNames env cond [] (isPureContext := true) + (env, [Core.Statement.assume ("assume" ++ getNameFromMd md) coreExpr md]) | .Block stmts _ => let (env', stmtsList) := stmts.attach.foldl (fun (e, acc) ⟨s, _hs⟩ => - let (e', ss) := translateStmt constants funcNames e outputParams s + let (e', ss) := translateStmt constants functionNames e outputParams s (e', acc ++ ss)) (env, []) (env', stmtsList) | .LocalVariable name ty initializer => @@ -196,20 +264,20 @@ def translateStmt (constants : List Constant) (funcNames : FunctionNames) (env : match initializer with | some (⟨ .StaticCall callee args, callMd⟩) => -- Check if this is a function or a procedure call - if isCoreFunction funcNames callee then + if isCoreFunction functionNames callee then -- Translate as expression (function application) - let boogieExpr := translateExpr constants env (⟨ .StaticCall callee args, callMd ⟩) + let (boogieExpr, _) := translateExpr constants functionNames env (⟨ .StaticCall callee args, callMd ⟩) (env', [Core.Statement.init ident boogieType (some boogieExpr) md]) else -- Translate as: var name; call name := callee(args) - let boogieArgs := args.map (translateExpr constants env) + let coreArgs := args.map (fun a => (translateExpr constants functionNames env a).1) let defaultExpr := defaultExprForType ty let initStmt := Core.Statement.init ident boogieType (some defaultExpr) - let callStmt := Core.Statement.call [ident] callee boogieArgs + let callStmt := Core.Statement.call [ident] callee coreArgs (env', [initStmt, callStmt]) | some initExpr => - let boogieExpr := translateExpr constants env initExpr - (env', [Core.Statement.init ident boogieType (some boogieExpr)]) + let (coreExpr, _) := translateExpr constants functionNames env initExpr + (env', [Core.Statement.init ident boogieType (some coreExpr)]) | none => let defaultExpr := defaultExprForType ty (env', [Core.Statement.init ident boogieType (some defaultExpr)]) @@ -220,51 +288,51 @@ def translateStmt (constants : List Constant) (funcNames : FunctionNames) (env : -- Check if RHS is a procedure call (not a function) match value.val with | .StaticCall callee args => - if isCoreFunction funcNames callee then + if isCoreFunction functionNames callee then -- Functions are translated as expressions - let boogieExpr := translateExpr constants env value + let (boogieExpr, _) := translateExpr constants functionNames env value (env, [Core.Statement.set ident boogieExpr]) else -- Procedure calls need to be translated as call statements - let boogieArgs := args.map (translateExpr constants env) - (env, [Core.Statement.call [ident] callee boogieArgs]) + let coreArgs := args.map (fun a => (translateExpr constants functionNames env a).1) + (env, [Core.Statement.call [ident] callee coreArgs]) | _ => - let boogieExpr := translateExpr constants env value + let (boogieExpr, _) := translateExpr constants functionNames env value (env, [Core.Statement.set ident boogieExpr]) | _ => -- Parallel assignment: (var1, var2, ...) := expr -- Example use is heap-modifying procedure calls: (result, heap) := f(heap, args) match value.val with | .StaticCall callee args => - let boogieArgs := args.map (translateExpr constants env) + let coreArgs := args.map (fun a => (translateExpr constants functionNames env a).1) let lhsIdents := targets.filterMap fun t => match t.val with | .Identifier name => some (Core.CoreIdent.locl name) | _ => none - (env, [Core.Statement.call lhsIdents callee boogieArgs value.md]) + (env, [Core.Statement.call lhsIdents callee coreArgs value.md]) | _ => panic "Assignments with multiple target but without a RHS call should not be constructed" | .IfThenElse cond thenBranch elseBranch => - let bcond := translateExpr constants env cond - let (_, bthen) := translateStmt constants funcNames env outputParams thenBranch + let (bcond, _) := translateExpr constants functionNames env cond + let (_, bthen) := translateStmt constants functionNames env outputParams thenBranch let belse := match elseBranch with - | some e => (translateStmt constants funcNames env outputParams e).2 + | some e => (translateStmt constants functionNames env outputParams e).2 | none => [] (env, [Imperative.Stmt.ite bcond bthen belse .empty]) | .StaticCall name args => -- Check if this is a function or procedure - if isCoreFunction funcNames name then + if isCoreFunction functionNames name then -- Functions as statements have no effect (shouldn't happen in well-formed programs) (env, []) else - let boogieArgs := args.map (translateExpr constants env) + let boogieArgs := args.map (fun a => (translateExpr constants functionNames env a).1) (env, [Core.Statement.call [] name boogieArgs]) | .Return valueOpt => match valueOpt, outputParams.head? with | some value, some outParam => let ident := Core.CoreIdent.locl outParam.name - let boogieExpr := translateExpr constants env value - let assignStmt := Core.Statement.set ident boogieExpr + let (coreExpr, _) := translateExpr constants functionNames env value + let assignStmt := Core.Statement.set ident coreExpr let noFallThrough := Core.Statement.assume "return" (.const () (.boolConst false)) .empty (env, [assignStmt, noFallThrough]) | none, _ => @@ -273,15 +341,15 @@ def translateStmt (constants : List Constant) (funcNames : FunctionNames) (env : | some _, none => panic! "Return statement with value but procedure has no output parameters" | .While cond invariants decreasesExpr body => - let condExpr := translateExpr constants env cond + let (condExpr, _) := translateExpr constants functionNames env cond -- Combine multiple invariants with && for Core (which expects single invariant) - let translatedInvariants := invariants.map (translateExpr constants env) + let translatedInvariants := invariants.map (fun inv => (translateExpr constants functionNames env inv).1) let invExpr := match translatedInvariants with | [] => none | [single] => some single | first :: rest => some (rest.foldl (fun acc inv => LExpr.mkApp () boolAndOp [acc, inv]) first) - let decreasingExprCore := decreasesExpr.map (translateExpr constants env) - let (_, bodyStmts) := translateStmt constants funcNames env outputParams body + let decreasingExprCore := decreasesExpr.map (fun d => (translateExpr constants functionNames env d).1) + let (_, bodyStmts) := translateStmt constants functionNames env outputParams body (env, [Imperative.Stmt.loop condExpr decreasingExprCore invExpr bodyStmts md]) | _ => (env, []) termination_by sizeOf stmt @@ -299,9 +367,11 @@ def translateParameterToCore (param : Parameter) : (Core.CoreIdent × LMonoTy) : (ident, ty) /-- -Translate Laurel Procedure to Core Procedure +Translate Laurel Procedure to Core Procedure, also returning any diagnostics from +disallowed constructs in preconditions or postconditions. -/ -def translateProcedure (constants : List Constant) (funcNames : FunctionNames) (proc : Procedure) : Core.Procedure := +def translateProcedure (constants : List Constant) (funcNames : FunctionNames) (proc : Procedure) + : Core.Procedure × List DiagnosticModel := let inputPairs := proc.inputs.map translateParameterToCore let inputs := inputPairs @@ -317,42 +387,40 @@ def translateProcedure (constants : List Constant) (funcNames : FunctionNames) ( 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 - let preconditions : ListMap Core.CoreLabel Core.Procedure.Check := + let (preconditions, precondDiags) : ListMap Core.CoreLabel Core.Procedure.Check × List DiagnosticModel := match proc.precondition with - | ⟨ .LiteralBool true, _ ⟩ => [] + | ⟨ .LiteralBool true, _ ⟩ => ([], []) | precond => - let check : Core.Procedure.Check := { expr := translateExpr constants initEnv precond, md := precond.md } - [("requires", check)] + let (e, ds) := translateExpr constants funcNames initEnv precond [] (isPureContext := true) + let check : Core.Procedure.Check := { expr := e, md := precond.md } + ([("requires", check)], ds) -- Translate postconditions for Opaque bodies - let postconditions : ListMap Core.CoreLabel Core.Procedure.Check := + let (postconditions, postcondDiags) : ListMap Core.CoreLabel Core.Procedure.Check × List DiagnosticModel := match proc.body with | .Opaque postconds _ _ => - let (_, result) := postconds.foldl (fun (i, acc) postcond => + let (_, result, diags) := postconds.foldl (fun (i, acc, accDs) postcond => let label := if postconds.length == 1 then "postcondition" else s!"postcondition_{i}" - let check : Core.Procedure.Check := { expr := translateExpr constants initEnv postcond, md := postcond.md } - (i + 1, acc ++ [(label, check)])) (0, []) - result - | _ => [] + let (e, ds) := translateExpr constants funcNames initEnv postcond [] (isPureContext := true) + let check : Core.Procedure.Check := { expr := e, md := postcond.md } + (i + 1, acc ++ [(label, check)], accDs ++ ds)) (0, [], []) + (result, diags) + | _ => ([], []) let modifies : List Core.Expression.Ident := [] - -- For bodyless opaque procedures (no implementation), we use `assume false` - -- so postcondition asserts are vacuously true. The postconditions are kept in - -- the spec so they are assumed at call sites via call elimination. let body : List Core.Statement := match proc.body with | .Transparent bodyExpr => (translateStmt constants funcNames initEnv proc.outputs bodyExpr).2 | .Opaque _postconds (some impl) _ => (translateStmt constants funcNames initEnv proc.outputs impl).2 - -- because Core does not support procedures without a body, we add an assume false | _ => [Core.Statement.assume "no_body" (.const () (.boolConst false)) .empty] let spec : Core.Procedure.Spec := { modifies, preconditions, postconditions, } - { + ({ header := header spec := spec body := body - } + }, precondDiags ++ postcondDiags) def translateConstant (c : Constant) : Core.Decl := match c.type.val with @@ -397,49 +465,53 @@ private def isPureExpr(expr: StmtExprMd): Bool := decreasing_by all_goals (have := WithMetadata.sizeOf_val_lt expr; term_by_mem) /-- Check if a pure-marked procedure can actually be represented as a Core function: - transparent body that is a pure expression, no precondition, exactly one output. -/ + transparent body that is a pure expression and has exactly one output. -/ private def canBeCoreFunctionBody (proc : Procedure) : Bool := match proc.body with | .Transparent bodyExpr => isPureExpr bodyExpr && - (match proc.precondition.val with | .LiteralBool true => true | _ => false) && + proc.outputs.length == 1 + | .Opaque _ bodyExprOption _ => + (bodyExprOption.map isPureExpr).getD true && proc.outputs.length == 1 | _ => false /-- -Translate a Laurel Procedure to a Core Function (when applicable) +Translate a Laurel Procedure to a Core Function (when applicable), also returning any +diagnostics emitted for disallowed constructs in the function body. -/ -def translateProcedureToFunction (constants : List Constant) (proc : Procedure) : Core.Decl := +def translateProcedureToFunction (constants : List Constant) (funcNames : FunctionNames) (proc : Procedure) + : Core.Decl × List DiagnosticModel := let inputs := proc.inputs.map translateParameterToCore let outputTy := match proc.outputs.head? with | some p => translateType p.type | none => LMonoTy.int let initEnv : TypeEnv := proc.inputs.map (fun p => (p.name, p.type)) - let body := match proc.body with - | .Transparent bodyExpr => some (translateExpr constants initEnv bodyExpr) - | _ => none - .func { + let (body, bodyDiags) := match proc.body with + | .Transparent bodyExpr => + let (e, ds) := translateExpr constants funcNames initEnv bodyExpr [] (isPureContext := true) + (some e, ds) + | _ => (none, []) + (.func { name := Core.CoreIdent.unres proc.name typeArgs := [] inputs := inputs output := outputTy body := body - } + }, bodyDiags) /-- Try to translate a Laurel Procedure marked `isFunctional` to a Core Function. -Returns `.error` with a diagnostic if the procedure cannot be represented as a Core function -(e.g. it has a non-pure body, a precondition, or multiple outputs). +Returns `.error` with diagnostics if the procedure body contains disallowed constructs +(destructive assignments, loops, or procedure calls). -/ -def tryTranslatePureToFunction (constants : List Constant) (proc : Procedure) - : Except DiagnosticModel Core.Decl := - let fileRange := (Imperative.getFileRange proc.md).getD FileRange.unknown - if !canBeCoreFunctionBody proc then - .error (DiagnosticModel.withRange fileRange - s!"Pure procedure '{proc.name}' cannot be translated to a Core function. \ - It must have a transparent pure body, no precondition, and exactly one output.") +def tryTranslatePureToFunction (constants : List Constant) (funcNames : FunctionNames) (proc : Procedure) + : Except (Array DiagnosticModel) Core.Decl := + let (decl, diags) := translateProcedureToFunction constants funcNames proc + if diags.isEmpty then + .ok decl else - .ok (translateProcedureToFunction constants proc) + .error diags.toArray /-- Translate Laurel Program to Core Program @@ -451,20 +523,22 @@ def translate (program : Program) : Except (Array DiagnosticModel) (Core.Program dbg_trace (toString (Std.Format.pretty (Std.ToFormat.format program))) dbg_trace "=================================" let program := liftImperativeExpressions program - -- dbg_trace "=== Program after heapParameterization + modifiesClausesTransform + liftImperativeExpressions ===" - -- dbg_trace (toString (Std.Format.pretty (Std.ToFormat.format program))) - -- dbg_trace "=================================" -- Procedures marked isFunctional are translated to Core functions; all others become Core procedures. let (markedPure, procProcs) := program.staticProcedures.partition (·.isFunctional) -- Try to translate each isFunctional procedure to a Core function, collecting errors for failures - let (pureErrors, pureFuncDecls) := markedPure.foldl (fun (errs, decls) p => - match tryTranslatePureToFunction program.constants p with - | .error e => (errs.push e, decls) - | .ok d => (errs, decls.push d)) (#[], #[]) - if !pureErrors.isEmpty then - .error pureErrors let funcNames : FunctionNames := markedPure.map (·.name) - let procedures := procProcs.map (translateProcedure program.constants funcNames) + let (pureErrors, pureFuncDecls) := markedPure.foldl (fun (errs, decls) p => + match tryTranslatePureToFunction program.constants funcNames p with + | .error es => (errs ++ es.toList, decls) + | .ok d => (errs, decls.push d)) ([], #[]) + -- Translate procedures, collecting any diagnostics from preconditions/postconditions + let (procedures, procDiags) := procProcs.foldl (fun (procs, diags) p => + let (proc, ds) := translateProcedure program.constants funcNames p + (procs ++ [proc], diags ++ ds)) ([], []) + -- Collect ALL errors from both functions and procedures before deciding whether to fail + let allErrors := pureErrors ++ procDiags + if !allErrors.isEmpty then + .error allErrors.toArray let procDecls := procedures.map (fun p => Core.Decl.proc p .empty) let constDecls := program.constants.map translateConstant let preludeDecls := corePrelude.decls diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean index 227e8f7b5..b85e998e4 100644 --- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean +++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean @@ -70,7 +70,7 @@ procedure nestedImpureStatementsAndOpaque() // An imperative procedure call in expression position is lifted before the // surrounding expression is evaluated. procedure imperativeProc(x: int) returns (r: int) - // ensures clause requires because Core does not support transparent proceduces yet + // ensures clause required because Core does not support transparent proceduces yet ensures r == x + 1 { r := x + 1; diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressionsError.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressionsError.lean new file mode 100644 index 000000000..388c38ddd --- /dev/null +++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressionsError.lean @@ -0,0 +1,55 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import StrataTest.Util.TestDiagnostics +import StrataTest.Languages.Laurel.TestExamples + +open StrataTest.Util +open Strata + +namespace Strata.Laurel + +def program: String := r" +procedure impure(): int { + var x: int := 0; + x := x + 1; + x +} + +function impureFunction(x: int): int +{ + var y: int := x; + y := y + 1; +//^^^^^^^^^^ error: destructive assignments are not supported in functions or contracts + while(false) {} +//^^^^^ error: loops are not supported in functions or contracts + var z: int := impure(); +// ^^^^^^^^ error: calls to procedures are not supported in functions or contracts + y +} + +procedure impureContractIsNotLegal1(x: int) + requires x == impure() +// ^^^^^^^^ error: calls to procedures are not supported in functions or contracts +{ + assert impure() == 1; +// ^^^^^^^^ error: calls to procedures are not supported in functions or contracts +} + +procedure impureContractIsNotLegal2(x: int) + requires (var y: iInt := 1;) (y := 2;) == 2 +// ^^^^^^^ error: destructive assignments are not supported in functions or contracts +{ + assert (var z: int := 1;) (z := 2;) == 2; +// ^^^^^^^ error: destructive assignments are not supported in functions or contracts +} +" + +#guard_msgs in -- (error, drop all) in +#eval! testInputWithOffset "NestedImpureStatements" program 14 processLaurelFile + + +end Laurel From 82dd95c16f0aff7185fd518289dfd64585aba9de Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 25 Feb 2026 12:08:45 +0000 Subject: [PATCH 10/28] Use a monad to make the code more readable --- .../Laurel/LaurelToCoreTranslator.lean | 340 +++++++++--------- 1 file changed, 173 insertions(+), 167 deletions(-) diff --git a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean b/Strata/Languages/Laurel/LaurelToCoreTranslator.lean index b6ac5587b..4e092b193 100644 --- a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean +++ b/Strata/Languages/Laurel/LaurelToCoreTranslator.lean @@ -67,129 +67,139 @@ def isCoreFunction (funcNames : FunctionNames) (name : Identifier) : Bool := name == "Box..intVal" || name == "Box..boolVal" || name == "Box..float64Val" || name == "Box..compositeVal" || funcNames.contains name +/-- State threaded through expression and statement translation -/ +structure TranslateState where + /-- Diagnostics accumulated during translation -/ + diagnostics : List DiagnosticModel := [] + /-- Constants known to the program (field constants, etc.) -/ + constants : List Constant := [] + /-- Names of procedures that are translated as Core functions -/ + funcNames : FunctionNames := [] + +/-- The translation monad: state over Id -/ +abbrev TranslateM := StateT TranslateState Id + +/-- Emit a diagnostic into the translation state -/ +def emitDiagnostic (d : DiagnosticModel) : TranslateM Unit := + modify fun s => { s with diagnostics := s.diagnostics ++ [d] } + +/-- Run a `TranslateM` action, returning the result and final state -/ +def runTranslateM (s : TranslateState) (m : TranslateM α) : α × TranslateState := + m s + /-- -Translate Laurel StmtExpr to Core Expression, also returning any diagnostics for disallowed -constructs (assignments, loops, procedure calls) that are not valid in expression position. +Translate Laurel StmtExpr to Core Expression using the `TranslateM` monad. +Diagnostics for disallowed constructs are emitted into the monad state. `isPureContext` should be `true` when translating function bodies or contract expressions. -In that case, disallowed constructs emit `DiagnosticModel` -errors. When `false` (inside a procedure body statement), disallowed constructs `panic!` +In that case, disallowed constructs emit `DiagnosticModel` errors into the state. +When `false` (inside a procedure body statement), disallowed constructs `panic!` because `liftImperativeExpressions` should have already removed them. `boundVars` tracks names bound by enclosing Forall/Exists quantifiers (innermost first). When an Identifier matches a bound name at index `i`, it becomes `bvar i` (de Bruijn index) instead of `fvar`. -/ -def translateExpr (constants : List Constant) (funcNames : FunctionNames) (env : TypeEnv) (expr : StmtExprMd) +def translateExpr (env : TypeEnv) (expr : StmtExprMd) (boundVars : List Identifier := []) (isPureContext : Bool := false) - : Core.Expression.Expr × List DiagnosticModel := + : TranslateM Core.Expression.Expr := do + let s ← get + let constants := s.constants + let funcNames := s.funcNames -- Dummy expression used as placeholder when an error is emitted in pure context let dummy := .fvar () (Core.CoreIdent.locl s!"DUMMY_VAR_{env.length}") none -- Emit an error in pure context; panic in impure context (lifting invariant violated) - let disallowed (e : StmtExprMd) (msg : String) : Core.Expression.Expr × List DiagnosticModel := + let disallowed (e : StmtExprMd) (msg : String) : TranslateM Core.Expression.Expr := do if isPureContext then - (dummy, [e.md.toDiagnostic msg]) + emitDiagnostic (e.md.toDiagnostic msg) + return dummy else panic! s!"translateExpr: {msg} (should have been lifted): {Std.Format.pretty (Std.ToFormat.format e)}" - -- Helper: combine diagnostics from two translated sub-expressions - let combine2 (r1 r2 : Core.Expression.Expr × List DiagnosticModel) - (f : Core.Expression.Expr → Core.Expression.Expr → Core.Expression.Expr) - : Core.Expression.Expr × List DiagnosticModel := - (f r1.1 r2.1, r1.2 ++ r2.2) match h: expr.val with - | .LiteralBool b => (.const () (.boolConst b), []) - | .LiteralInt i => (.const () (.intConst i), []) - | .LiteralString s => (.const () (.strConst s), []) + | .LiteralBool b => return .const () (.boolConst b) + | .LiteralInt i => return .const () (.intConst i) + | .LiteralString s => return .const () (.strConst s) | .Identifier name => -- First check if this name is bound by an enclosing quantifier match boundVars.findIdx? (· == name) with | some idx => -- Bound variable: use de Bruijn index - (.bvar () idx, []) + return .bvar () idx | none => -- Check if this is a constant (field constant) or local variable if isConstant constants name then - let ident := Core.CoreIdent.unres name - (.op () ident none, []) + return .op () (Core.CoreIdent.unres name) none else - let ident := Core.CoreIdent.locl name - (.fvar () ident (some (lookupType env name)), []) + return .fvar () (Core.CoreIdent.locl name) (some (lookupType env name)) | .PrimitiveOp op [e] => match op with | .Not => - let (re, ds) := translateExpr constants funcNames env e boundVars isPureContext - (.app () boolNotOp re, ds) + let re ← translateExpr env e boundVars isPureContext + return .app () boolNotOp re | .Neg => - let (re, ds) := translateExpr constants funcNames env e boundVars isPureContext - (.app () intNegOp re, ds) + let re ← translateExpr env e boundVars isPureContext + return .app () intNegOp re | _ => panic! s!"translateExpr: Invalid unary op: {repr op}" | .PrimitiveOp op [e1, e2] => - let (re1, ds1) := translateExpr constants funcNames env e1 boundVars isPureContext - let (re2, ds2) := translateExpr constants funcNames env e2 boundVars isPureContext - let ds := ds1 ++ ds2 - let binOp (bop : Core.Expression.Expr) : Core.Expression.Expr × List DiagnosticModel := - (LExpr.mkApp () bop [re1, re2], ds) + let re1 ← translateExpr env e1 boundVars isPureContext + let re2 ← translateExpr env e2 boundVars isPureContext + let binOp (bop : Core.Expression.Expr) : Core.Expression.Expr := + LExpr.mkApp () bop [re1, re2] match op with - | .Eq => (.eq () re1 re2, ds) - | .Neq => (.app () boolNotOp (.eq () re1 re2), ds) - | .And => binOp boolAndOp - | .Or => binOp boolOrOp - | .Implies => binOp boolImpliesOp - | .Add => binOp intAddOp - | .Sub => binOp intSubOp - | .Mul => binOp intMulOp - | .Div => binOp intDivOp - | .Mod => binOp intModOp - | .DivT => binOp intDivTOp - | .ModT => binOp intModTOp - | .Lt => binOp intLtOp - | .Leq => binOp intLeOp - | .Gt => binOp intGtOp - | .Geq => binOp intGeOp + | .Eq => return .eq () re1 re2 + | .Neq => return .app () boolNotOp (.eq () re1 re2) + | .And => return binOp boolAndOp + | .Or => return binOp boolOrOp + | .Implies => return binOp boolImpliesOp + | .Add => return binOp intAddOp + | .Sub => return binOp intSubOp + | .Mul => return binOp intMulOp + | .Div => return binOp intDivOp + | .Mod => return binOp intModOp + | .DivT => return binOp intDivTOp + | .ModT => return binOp intModTOp + | .Lt => return binOp intLtOp + | .Leq => return binOp intLeOp + | .Gt => return binOp intGtOp + | .Geq => return binOp intGeOp | _ => panic! s!"translateExpr: Invalid binary op: {repr op}" | .PrimitiveOp op args => panic! s!"translateExpr: PrimitiveOp {repr op} with {args.length} args" | .IfThenElse cond thenBranch elseBranch => - let (bcond, ds0) := translateExpr constants funcNames env cond boundVars isPureContext - let (bthen, ds1) := translateExpr constants funcNames env thenBranch boundVars isPureContext - let (belse, ds2) : Core.Expression.Expr × List DiagnosticModel := - match elseBranch with + let bcond ← translateExpr env cond boundVars isPureContext + let bthen ← translateExpr env thenBranch boundVars isPureContext + let belse ← match elseBranch with | none => panic "if-then without else expression not yet implemented" | some e => have : sizeOf e < sizeOf expr := by have := WithMetadata.sizeOf_val_lt expr cases expr; simp_all; omega - translateExpr constants funcNames env e boundVars isPureContext - (.ite () bcond bthen belse, ds0 ++ ds1 ++ ds2) + translateExpr env e boundVars isPureContext + return .ite () bcond bthen belse | .StaticCall name args => -- In a pure context, only Core functions (not procedures) are allowed if isPureContext && !isCoreFunction funcNames name then disallowed expr "calls to procedures are not supported in functions or contracts" else - let ident := Core.CoreIdent.unres name - let fnOp := .op () ident none - let (result, ds) := args.attach.foldl (fun (acc, accDs) ⟨arg, _⟩ => - let (re, ds) := translateExpr constants funcNames env arg boundVars isPureContext - (.app () acc re, accDs ++ ds)) (fnOp, []) - (result, ds) - | .Block [single] _ => translateExpr constants funcNames env single boundVars isPureContext - | .Block _ _ => panic "block expression not yet implemented" - | .LocalVariable _ _ _ => panic "local variable expression not yet implemented" - | .Return _ => disallowed expr "return expression not yet implemented" + let fnOp : Core.Expression.Expr := .op () (Core.CoreIdent.unres name) none + args.attach.foldlM (fun acc ⟨arg, _⟩ => do + let re ← translateExpr env arg boundVars isPureContext + return .app () acc re) fnOp + | .Block [single] _ => translateExpr env single boundVars isPureContext | .Forall name ty body => let coreTy := translateType ty - let (coreBody, ds) := translateExpr constants funcNames env body (name :: boundVars) isPureContext - (LExpr.all () (some coreTy) coreBody, ds) + let coreBody ← translateExpr env body (name :: boundVars) isPureContext + return LExpr.all () (some coreTy) coreBody | .Exists name ty body => let coreTy := translateType ty - let (coreBody, ds) := translateExpr constants funcNames env body (name :: boundVars) isPureContext - (LExpr.exist () (some coreTy) coreBody, ds) - | .Hole => (dummy, []) + let coreBody ← translateExpr env body (name :: boundVars) isPureContext + return LExpr.exist () (some coreTy) coreBody + | .Hole => return dummy | .ReferenceEquals e1 e2 => - combine2 (translateExpr constants funcNames env e1 boundVars isPureContext) - (translateExpr constants funcNames env e2 boundVars isPureContext) - (fun l r => .eq () l r) + let re1 ← translateExpr env e1 boundVars isPureContext + let re2 ← translateExpr env e2 boundVars isPureContext + return .eq () re1 re2 | .Assign _ _ => disallowed expr "destructive assignments are not supported in functions or contracts" | .While _ _ _ _ => @@ -202,6 +212,10 @@ def translateExpr (constants : List Constant) (funcNames : FunctionNames) (env : -- If we see one here, it's an error in the pipeline panic! s!"FieldSelect should have been eliminated by heap parameterization: {Std.ToFormat.format target}#{fieldName}" + | .Block _ _ => panic "block expression not yet implemented" + | .LocalVariable _ _ _ => panic "local variable expression not yet implemented" + | .Return _ => disallowed expr "return expression not yet implemented" + | .AsType target _ => panic "AsType expression not implemented" | .Assigned _ => panic "assigned expression not implemented" | .Old value => panic "old expression not implemented" @@ -237,25 +251,27 @@ def defaultExprForType (ty : HighTypeMd) : Core.Expression.Expr := .fvar () (Core.CoreIdent.locl "$default") (some coreTy) /-- -Translate Laurel StmtExpr to Core Statements -Takes the constants list, type environment, output parameter names, and set of function names +Translate Laurel StmtExpr to Core Statements using the `TranslateM` monad. +Diagnostics are emitted into the monad state. -/ -def translateStmt (constants : List Constant) (functionNames : FunctionNames) (env : TypeEnv) - (outputParams : List Parameter) (stmt : StmtExprMd) : TypeEnv × List Core.Statement := +def translateStmt (env : TypeEnv) (outputParams : List Parameter) (stmt : StmtExprMd) + : TranslateM (TypeEnv × List Core.Statement) := do + let s ← get + let functionNames := s.funcNames let md := stmt.md - match h : stmt.val with + match _h : stmt.val with | @StmtExpr.Assert cond => -- Assert/assume bodies must be pure expressions (no assignments, loops, or procedure calls) - let (coreExpr, _) := translateExpr constants functionNames env cond [] (isPureContext := true) - (env, [Core.Statement.assert ("assert" ++ getNameFromMd md) coreExpr md]) + let coreExpr ← translateExpr env cond [] (isPureContext := true) + return (env, [Core.Statement.assert ("assert" ++ getNameFromMd md) coreExpr md]) | @StmtExpr.Assume cond => - let (coreExpr, _) := translateExpr constants functionNames env cond [] (isPureContext := true) - (env, [Core.Statement.assume ("assume" ++ getNameFromMd md) coreExpr md]) + let coreExpr ← translateExpr env cond [] (isPureContext := true) + return (env, [Core.Statement.assume ("assume" ++ getNameFromMd md) coreExpr md]) | .Block stmts _ => - let (env', stmtsList) := stmts.attach.foldl (fun (e, acc) ⟨s, _hs⟩ => - let (e', ss) := translateStmt constants functionNames e outputParams s - (e', acc ++ ss)) (env, []) - (env', stmtsList) + let (env', stmtsList) ← stmts.attach.foldlM (fun (e, acc) ⟨s, _hs⟩ => do + let (e', ss) ← translateStmt e outputParams s + return (e', acc ++ ss)) (env, []) + return (env', stmtsList) | .LocalVariable name ty initializer => let env' := (name, ty) :: env let boogieMonoType := translateType ty @@ -266,21 +282,21 @@ def translateStmt (constants : List Constant) (functionNames : FunctionNames) (e -- Check if this is a function or a procedure call if isCoreFunction functionNames callee then -- Translate as expression (function application) - let (boogieExpr, _) := translateExpr constants functionNames env (⟨ .StaticCall callee args, callMd ⟩) - (env', [Core.Statement.init ident boogieType (some boogieExpr) md]) + let boogieExpr ← translateExpr env (⟨ .StaticCall callee args, callMd ⟩) + return (env', [Core.Statement.init ident boogieType (some boogieExpr) md]) else -- Translate as: var name; call name := callee(args) - let coreArgs := args.map (fun a => (translateExpr constants functionNames env a).1) + let coreArgs ← args.mapM (fun a => translateExpr env a) let defaultExpr := defaultExprForType ty let initStmt := Core.Statement.init ident boogieType (some defaultExpr) let callStmt := Core.Statement.call [ident] callee coreArgs - (env', [initStmt, callStmt]) + return (env', [initStmt, callStmt]) | some initExpr => - let (coreExpr, _) := translateExpr constants functionNames env initExpr - (env', [Core.Statement.init ident boogieType (some coreExpr)]) + let coreExpr ← translateExpr env initExpr + return (env', [Core.Statement.init ident boogieType (some coreExpr)]) | none => let defaultExpr := defaultExprForType ty - (env', [Core.Statement.init ident boogieType (some defaultExpr)]) + return (env', [Core.Statement.init ident boogieType (some defaultExpr)]) | .Assign targets value => match targets with | [⟨ .Identifier name, _ ⟩] => @@ -290,68 +306,68 @@ def translateStmt (constants : List Constant) (functionNames : FunctionNames) (e | .StaticCall callee args => if isCoreFunction functionNames callee then -- Functions are translated as expressions - let (boogieExpr, _) := translateExpr constants functionNames env value - (env, [Core.Statement.set ident boogieExpr]) + let boogieExpr ← translateExpr env value + return (env, [Core.Statement.set ident boogieExpr]) else -- Procedure calls need to be translated as call statements - let coreArgs := args.map (fun a => (translateExpr constants functionNames env a).1) - (env, [Core.Statement.call [ident] callee coreArgs]) + let coreArgs ← args.mapM (fun a => translateExpr env a) + return (env, [Core.Statement.call [ident] callee coreArgs]) | _ => - let (boogieExpr, _) := translateExpr constants functionNames env value - (env, [Core.Statement.set ident boogieExpr]) + let boogieExpr ← translateExpr env value + return (env, [Core.Statement.set ident boogieExpr]) | _ => -- Parallel assignment: (var1, var2, ...) := expr -- Example use is heap-modifying procedure calls: (result, heap) := f(heap, args) match value.val with | .StaticCall callee args => - let coreArgs := args.map (fun a => (translateExpr constants functionNames env a).1) + let coreArgs ← args.mapM (fun a => translateExpr env a) let lhsIdents := targets.filterMap fun t => match t.val with | .Identifier name => some (Core.CoreIdent.locl name) | _ => none - (env, [Core.Statement.call lhsIdents callee coreArgs value.md]) + return (env, [Core.Statement.call lhsIdents callee coreArgs value.md]) | _ => panic "Assignments with multiple target but without a RHS call should not be constructed" | .IfThenElse cond thenBranch elseBranch => - let (bcond, _) := translateExpr constants functionNames env cond - let (_, bthen) := translateStmt constants functionNames env outputParams thenBranch - let belse := match elseBranch with - | some e => (translateStmt constants functionNames env outputParams e).2 - | none => [] - (env, [Imperative.Stmt.ite bcond bthen belse .empty]) + let bcond ← translateExpr env cond + let (_, bthen) ← translateStmt env outputParams thenBranch + let belse ← match elseBranch with + | some e => (·.2) <$> translateStmt env outputParams e + | none => pure [] + return (env, [Imperative.Stmt.ite bcond bthen belse .empty]) | .StaticCall name args => -- Check if this is a function or procedure if isCoreFunction functionNames name then -- Functions as statements have no effect (shouldn't happen in well-formed programs) - (env, []) + return (env, []) else - let boogieArgs := args.map (fun a => (translateExpr constants functionNames env a).1) - (env, [Core.Statement.call [] name boogieArgs]) + let boogieArgs ← args.mapM (fun a => translateExpr env a) + return (env, [Core.Statement.call [] name boogieArgs]) | .Return valueOpt => match valueOpt, outputParams.head? with | some value, some outParam => let ident := Core.CoreIdent.locl outParam.name - let (coreExpr, _) := translateExpr constants functionNames env value + let coreExpr ← translateExpr env value let assignStmt := Core.Statement.set ident coreExpr let noFallThrough := Core.Statement.assume "return" (.const () (.boolConst false)) .empty - (env, [assignStmt, noFallThrough]) + return (env, [assignStmt, noFallThrough]) | none, _ => let noFallThrough := Core.Statement.assume "return" (.const () (.boolConst false)) .empty - (env, [noFallThrough]) + return (env, [noFallThrough]) | some _, none => panic! "Return statement with value but procedure has no output parameters" | .While cond invariants decreasesExpr body => - let (condExpr, _) := translateExpr constants functionNames env cond + let condExpr ← translateExpr env cond -- Combine multiple invariants with && for Core (which expects single invariant) - let translatedInvariants := invariants.map (fun inv => (translateExpr constants functionNames env inv).1) + let translatedInvariants ← invariants.mapM (fun inv => translateExpr env inv) let invExpr := match translatedInvariants with | [] => none | [single] => some single | first :: rest => some (rest.foldl (fun acc inv => LExpr.mkApp () boolAndOp [acc, inv]) first) - let decreasingExprCore := decreasesExpr.map (fun d => (translateExpr constants functionNames env d).1) - let (_, bodyStmts) := translateStmt constants functionNames env outputParams body - (env, [Imperative.Stmt.loop condExpr decreasingExprCore invExpr bodyStmts md]) - | _ => (env, []) + let decreasingExprCore ← decreasesExpr.mapM (fun d => translateExpr env d) + let (_, bodyStmts) ← translateStmt env outputParams body + return (env, [Imperative.Stmt.loop condExpr decreasingExprCore invExpr bodyStmts md]) + | _ => return (env, []) termination_by sizeOf stmt decreasing_by all_goals @@ -367,16 +383,16 @@ def translateParameterToCore (param : Parameter) : (Core.CoreIdent × LMonoTy) : (ident, ty) /-- -Translate Laurel Procedure to Core Procedure, also returning any diagnostics from -disallowed constructs in preconditions or postconditions. +Translate Laurel Procedure to Core Procedure using `TranslateM`. +Diagnostics from disallowed constructs in preconditions, postconditions, and body +are emitted into the monad state. -/ -def translateProcedure (constants : List Constant) (funcNames : FunctionNames) (proc : Procedure) - : Core.Procedure × List DiagnosticModel := +def translateProcedure (proc : Procedure) : TranslateM Core.Procedure := do + let s ← get + let constants := s.constants let inputPairs := proc.inputs.map translateParameterToCore let inputs := inputPairs - let outputs := proc.outputs.map translateParameterToCore - let header : Core.Procedure.Header := { name := proc.name typeArgs := [] @@ -387,40 +403,31 @@ def translateProcedure (constants : List Constant) (funcNames : FunctionNames) ( 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 - let (preconditions, precondDiags) : ListMap Core.CoreLabel Core.Procedure.Check × List DiagnosticModel := + let preconditions : ListMap Core.CoreLabel Core.Procedure.Check ← match proc.precondition with - | ⟨ .LiteralBool true, _ ⟩ => ([], []) + | ⟨ .LiteralBool true, _ ⟩ => pure [] | precond => - let (e, ds) := translateExpr constants funcNames initEnv precond [] (isPureContext := true) + let e ← translateExpr initEnv precond [] (isPureContext := true) let check : Core.Procedure.Check := { expr := e, md := precond.md } - ([("requires", check)], ds) + pure [("requires", check)] -- Translate postconditions for Opaque bodies - let (postconditions, postcondDiags) : ListMap Core.CoreLabel Core.Procedure.Check × List DiagnosticModel := + let postconditions : ListMap Core.CoreLabel Core.Procedure.Check ← match proc.body with | .Opaque postconds _ _ => - let (_, result, diags) := postconds.foldl (fun (i, acc, accDs) postcond => + postconds.mapIdxM (fun i postcond => do let label := if postconds.length == 1 then "postcondition" else s!"postcondition_{i}" - let (e, ds) := translateExpr constants funcNames initEnv postcond [] (isPureContext := true) + let e ← translateExpr initEnv postcond [] (isPureContext := true) let check : Core.Procedure.Check := { expr := e, md := postcond.md } - (i + 1, acc ++ [(label, check)], accDs ++ ds)) (0, [], []) - (result, diags) - | _ => ([], []) + pure (label, check)) + | _ => pure [] let modifies : List Core.Expression.Ident := [] - let body : List Core.Statement := + let body : List Core.Statement ← match proc.body with - | .Transparent bodyExpr => (translateStmt constants funcNames initEnv proc.outputs bodyExpr).2 - | .Opaque _postconds (some impl) _ => (translateStmt constants funcNames initEnv proc.outputs impl).2 - | _ => [Core.Statement.assume "no_body" (.const () (.boolConst false)) .empty] - let spec : Core.Procedure.Spec := { - modifies, - preconditions, - postconditions, - } - ({ - header := header - spec := spec - body := body - }, precondDiags ++ postcondDiags) + | .Transparent bodyExpr => (·.2) <$> translateStmt initEnv proc.outputs bodyExpr + | .Opaque _postconds (some impl) _ => (·.2) <$> translateStmt initEnv proc.outputs impl + | _ => pure [Core.Statement.assume "no_body" (.const () (.boolConst false)) .empty] + let spec : Core.Procedure.Spec := { modifies, preconditions, postconditions } + return { header, spec, body } def translateConstant (c : Constant) : Core.Decl := match c.type.val with @@ -477,41 +484,38 @@ private def canBeCoreFunctionBody (proc : Procedure) : Bool := | _ => false /-- -Translate a Laurel Procedure to a Core Function (when applicable), also returning any -diagnostics emitted for disallowed constructs in the function body. +Translate a Laurel Procedure to a Core Function (when applicable) using `TranslateM`. +Diagnostics for disallowed constructs in the function body are emitted into the monad state. -/ -def translateProcedureToFunction (constants : List Constant) (funcNames : FunctionNames) (proc : Procedure) - : Core.Decl × List DiagnosticModel := +def translateProcedureToFunction (proc : Procedure) : TranslateM Core.Decl := do let inputs := proc.inputs.map translateParameterToCore let outputTy := match proc.outputs.head? with | some p => translateType p.type | none => LMonoTy.int let initEnv : TypeEnv := proc.inputs.map (fun p => (p.name, p.type)) - let (body, bodyDiags) := match proc.body with - | .Transparent bodyExpr => - let (e, ds) := translateExpr constants funcNames initEnv bodyExpr [] (isPureContext := true) - (some e, ds) - | _ => (none, []) - (.func { + let body ← match proc.body with + | .Transparent bodyExpr => some <$> translateExpr initEnv bodyExpr [] (isPureContext := true) + | _ => pure none + return .func { name := Core.CoreIdent.unres proc.name typeArgs := [] inputs := inputs output := outputTy body := body - }, bodyDiags) + } /-- Try to translate a Laurel Procedure marked `isFunctional` to a Core Function. Returns `.error` with diagnostics if the procedure body contains disallowed constructs (destructive assignments, loops, or procedure calls). -/ -def tryTranslatePureToFunction (constants : List Constant) (funcNames : FunctionNames) (proc : Procedure) +def tryTranslatePureToFunction (proc : Procedure) (initState : TranslateState) : Except (Array DiagnosticModel) Core.Decl := - let (decl, diags) := translateProcedureToFunction constants funcNames proc - if diags.isEmpty then + let (decl, finalState) := runTranslateM initState (translateProcedureToFunction proc) + if finalState.diagnostics.isEmpty then .ok decl else - .error diags.toArray + .error finalState.diagnostics.toArray /-- Translate Laurel Program to Core Program @@ -525,16 +529,18 @@ def translate (program : Program) : Except (Array DiagnosticModel) (Core.Program let program := liftImperativeExpressions program -- Procedures marked isFunctional are translated to Core functions; all others become Core procedures. let (markedPure, procProcs) := program.staticProcedures.partition (·.isFunctional) - -- Try to translate each isFunctional procedure to a Core function, collecting errors for failures + -- Build the shared initial state with constants and function names let funcNames : FunctionNames := markedPure.map (·.name) + let initState : TranslateState := { constants := program.constants, funcNames } + -- Try to translate each isFunctional procedure to a Core function, collecting errors for failures let (pureErrors, pureFuncDecls) := markedPure.foldl (fun (errs, decls) p => - match tryTranslatePureToFunction program.constants funcNames p with + match tryTranslatePureToFunction p initState with | .error es => (errs ++ es.toList, decls) | .ok d => (errs, decls.push d)) ([], #[]) - -- Translate procedures, collecting any diagnostics from preconditions/postconditions - let (procedures, procDiags) := procProcs.foldl (fun (procs, diags) p => - let (proc, ds) := translateProcedure program.constants funcNames p - (procs ++ [proc], diags ++ ds)) ([], []) + -- Translate procedures using the monad, collecting diagnostics from the final state + let (procedures, procState) := runTranslateM initState do + procProcs.mapM translateProcedure + let procDiags := procState.diagnostics -- Collect ALL errors from both functions and procedures before deciding whether to fail let allErrors := pureErrors ++ procDiags if !allErrors.isEmpty then From b1472a0ea44b8abb989793da9d39080b228bbdc9 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 25 Feb 2026 12:09:04 +0000 Subject: [PATCH 11/28] Update panic --- Strata/Languages/Laurel/LaurelToCoreTranslator.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean b/Strata/Languages/Laurel/LaurelToCoreTranslator.lean index 4e092b193..2f2012b90 100644 --- a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean +++ b/Strata/Languages/Laurel/LaurelToCoreTranslator.lean @@ -212,9 +212,9 @@ def translateExpr (env : TypeEnv) (expr : StmtExprMd) -- If we see one here, it's an error in the pipeline panic! s!"FieldSelect should have been eliminated by heap parameterization: {Std.ToFormat.format target}#{fieldName}" - | .Block _ _ => panic "block expression not yet implemented" - | .LocalVariable _ _ _ => panic "local variable expression not yet implemented" - | .Return _ => disallowed expr "return expression not yet implemented" + | .Block _ _ => panic "block expression not yet implemented (should be lowered in a separate pass)" + | .LocalVariable _ _ _ => panic "local variable expression not yet implemented (should be lowered in a separate pass)" + | .Return _ => disallowed expr "return expression not yet implemented (should be lowered in a separate pass)" | .AsType target _ => panic "AsType expression not implemented" | .Assigned _ => panic "assigned expression not implemented" From 40a28ad589b03ddf834114e1309f7b8ff284f95f Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 25 Feb 2026 13:52:20 +0000 Subject: [PATCH 12/28] Fix --- .../Laurel/LiftImperativeExpressions.lean | 11 +++---- .../T2_ImpureExpressionsError.lean | 31 +++++++++++-------- 2 files changed, 23 insertions(+), 19 deletions(-) diff --git a/Strata/Languages/Laurel/LiftImperativeExpressions.lean b/Strata/Languages/Laurel/LiftImperativeExpressions.lean index 838dd454f..4cb595d32 100644 --- a/Strata/Languages/Laurel/LiftImperativeExpressions.lean +++ b/Strata/Languages/Laurel/LiftImperativeExpressions.lean @@ -345,14 +345,13 @@ def transformStmt (stmt : StmtExprMd) : LiftM (List StmtExprMd) := do | WithMetadata.mk val md => match val with | .Assert cond => - let seqCond ← transformExpr cond - let prepends ← takePrepends - return prepends ++ [⟨.Assert seqCond, md⟩] + -- Do not transform assert conditions: impure expressions inside contracts + -- must be rejected by the translator, not silently lifted. + return [stmt] | .Assume cond => - let seqCond ← transformExpr cond - let prepends ← takePrepends - return prepends ++ [⟨.Assume seqCond, md⟩] + -- Do not transform assume conditions: same reasoning as assert. + return [stmt] | .Block stmts metadata => let seqStmts ← stmts.mapM transformStmt diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressionsError.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressionsError.lean index 388c38ddd..422f4d265 100644 --- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressionsError.lean +++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressionsError.lean @@ -19,16 +19,21 @@ procedure impure(): int { x } -function impureFunction(x: int): int +function impureFunction1(x: int): int +{ + x := x + 1; +//^^^^^^^^^^^ error: destructive assignments are not supported in functions or contracts +} + +function impureFunction2(x: int): int { - var y: int := x; - y := y + 1; -//^^^^^^^^^^ error: destructive assignments are not supported in functions or contracts while(false) {} -//^^^^^ error: loops are not supported in functions or contracts - var z: int := impure(); -// ^^^^^^^^ error: calls to procedures are not supported in functions or contracts - y +//^^^^^^^^^^^^^^^ error: loops are not supported in functions or contracts +} +function impureFunction3(x: int): int +{ + impure() +//^^^^^^^^ error: calls to procedures are not supported in functions or contracts } procedure impureContractIsNotLegal1(x: int) @@ -40,15 +45,15 @@ procedure impureContractIsNotLegal1(x: int) } procedure impureContractIsNotLegal2(x: int) - requires (var y: iInt := 1;) (y := 2;) == 2 -// ^^^^^^^ error: destructive assignments are not supported in functions or contracts + requires (x := 2;) == 2 +// ^^^^^^^ error: destructive assignments are not supported in functions or contracts { - assert (var z: int := 1;) (z := 2;) == 2; -// ^^^^^^^ error: destructive assignments are not supported in functions or contracts + assert (x := 2;) == 2; +// ^^^^^^^ error: destructive assignments are not supported in functions or contracts } " -#guard_msgs in -- (error, drop all) in +#guard_msgs (error, drop all) in #eval! testInputWithOffset "NestedImpureStatements" program 14 processLaurelFile From c9ed9fa2d2bf3b34a6ac588577d6a3c5ba1e2a48 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 25 Feb 2026 14:19:54 +0000 Subject: [PATCH 13/28] Add more test cases --- .../Fundamentals/T5_ProcedureCalls.lean | 56 +++++++------------ .../T5_ProcedureCallsStrataCore.lean | 48 ---------------- .../Fundamentals/T8_Postconditions.lean | 24 +++++++- 3 files changed, 44 insertions(+), 84 deletions(-) delete mode 100644 StrataTest/Languages/Laurel/Examples/Fundamentals/T5_ProcedureCallsStrataCore.lean diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T5_ProcedureCalls.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T5_ProcedureCalls.lean index 3ba48f00f..d45d911cc 100644 --- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T5_ProcedureCalls.lean +++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T5_ProcedureCalls.lean @@ -10,56 +10,42 @@ import StrataTest.Languages.Laurel.TestExamples open StrataTest.Util open Strata -namespace Laurel +namespace Strata.Laurel def program := r" procedure fooReassign(): int { - var x = 0; - x = x + 1; + var x: int := 0; + x := x + 1; assert x == 1; - x = x + 1; + x := x + 1; x } procedure fooSingleAssign(): int { - var x = 0 - var x2 = x + 1; - var x3 = x2 + 1; + var x: int := 0; + var x2: int := x + 1; + var x3: int := x2 + 1; x3 } procedure fooProof() { - assert fooReassign() == fooSingleAssign(); -} -" - --- Not working yet --- #eval! testInput "ProcedureCalls" program processLaurelFile - -/- -Translation towards SMT: - -function fooReassign(): int { - var x0 = 0; - var x1 = x0 + 1; - var x2 = x1 + 1; - x2 + var x: int := fooReassign(); + var y: int := fooSingleAssign(); +// The following assertions fails while it should succeed, +// because Core does not yet support transparent procedures +// assert x == y; } -proof fooReassign_body { - var x = 0; - x = x + 1; - assert x == 1; +function aFunction(x: int): int +{ + x } -function fooSingleAssign(): int { - var x = 0; - var x2 = x + 1; - var x3 = x2 + 1; - x3 +procedure aFunctionCaller() { + var x: int := aFunction(3); + assert x == 3; } +" -proof fooProof_body { - assert fooReassign() == fooSingleAssign(); -} --/ +#guard_msgs (drop info, error) in +#eval testInputWithOffset "ProcedureCalls" program 14 processLaurelFile diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T5_ProcedureCallsStrataCore.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T5_ProcedureCallsStrataCore.lean deleted file mode 100644 index a77b6777b..000000000 --- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T5_ProcedureCallsStrataCore.lean +++ /dev/null @@ -1,48 +0,0 @@ -/- - Copyright Strata Contributors - - SPDX-License-Identifier: Apache-2.0 OR MIT --/ - -/- -The purpose of this test is to ensure we're using functions and procedures as well as -Strata Core supports them. When Strata Core makes procedures more powerful, so we -won't need functions any more, then this test can be merged into other tests. --/ - -import StrataTest.Util.TestDiagnostics -import StrataTest.Languages.Laurel.TestExamples - -open StrataTest.Util -open Strata - -namespace Strata.Laurel - -def program := r" -function aFunction(x: int): int { - x + 1 -} - -procedure noFunctionBecauseContract() returns (r: int) - ensures r > 0 -{ - return 10; -} - -procedure noFunctionBecauseStatements(): int { - var x: int := 3; - x + 1 -} - -procedure caller() { - assert aFunction(1) == 2; - var x: int := noFunctionBecauseContract(); - assert x > 0; - var y: int := noFunctionBecauseStatements(); - assert y == 4; -//. ^^^^^^^^^^^^^^ error: assertion does not hold -} -" - -#guard_msgs(drop info, error) in -#eval! testInputWithOffset "T5_ProcedureCallsStrataCore" program 20 processLaurelFile diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T8_Postconditions.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T8_Postconditions.lean index 6b7802446..769611336 100644 --- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T8_Postconditions.lean +++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T8_Postconditions.lean @@ -15,17 +15,39 @@ namespace Strata.Laurel def program := r" procedure opaqueBody(x: int) returns (r: int) // the presence of the ensures make the body opaque. we can consider more explicit syntax. - ensures (r >= 0) + ensures r > 0 { if (x > 0) { r := x; } else { r := 1; } } +procedure callerOfOpaqueProcedure() { + var x: int := opaqueBody(3); + assert x > 0; + assert x == 3; +//^^^^^^^^^^^^^^ error: assertion does not hold +} + procedure invalidPostcondition(x: int) ensures false // ^^^^^ error: assertion does not hold { } + +function opaqueFunction(x: int) returns (r: int) + requires x > 0 + ensures r > 0 +{ + x +} + +procedure callerOfOpaqueFunction() { + var x: int := opaqueFunction(3); + assert x > 0; +// The following assert should fail but it does not, +// because Core does not support opaque functions +// assert x == 3; +} " #guard_msgs (drop info, error) in From 64a5ad8729bde9e9c36618662f52d49d903baed5 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 25 Feb 2026 14:39:04 +0000 Subject: [PATCH 14/28] Test updated and extra diagnostics --- .../Laurel/LaurelToCoreTranslator.lean | 11 ++++++ .../Fundamentals/T6_Preconditions.lean | 11 ++++++ .../Fundamentals/T8_Postconditions.lean | 15 -------- .../Fundamentals/T8_PostconditionsErrors.lean | 37 +++++++++++++++++++ 4 files changed, 59 insertions(+), 15 deletions(-) create mode 100644 StrataTest/Languages/Laurel/Examples/Fundamentals/T8_PostconditionsErrors.lean diff --git a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean b/Strata/Languages/Laurel/LaurelToCoreTranslator.lean index 2f2012b90..beee4497d 100644 --- a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean +++ b/Strata/Languages/Laurel/LaurelToCoreTranslator.lean @@ -493,8 +493,18 @@ def translateProcedureToFunction (proc : Procedure) : TranslateM Core.Decl := do | some p => translateType p.type | none => LMonoTy.int let initEnv : TypeEnv := proc.inputs.map (fun p => (p.name, p.type)) + -- Translate precondition to FuncPrecondition (skip trivial `true`) + let preconditions : List (Lambda.FuncPrecondition Core.Expression.Expr Core.ExpressionMetadata) ← + match proc.precondition with + | ⟨ .LiteralBool true, _ ⟩ => pure [] + | precond => + let e ← translateExpr initEnv precond [] (isPureContext := true) + pure [{ expr := e, md := () }] let body ← match proc.body with | .Transparent bodyExpr => some <$> translateExpr initEnv bodyExpr [] (isPureContext := true) + | .Opaque _ (some bodyExpr) _ => + emitDiagnostic (proc.md.toDiagnostic "functions with postconditions are not yet supported") + some <$> translateExpr initEnv bodyExpr [] (isPureContext := true) | _ => pure none return .func { name := Core.CoreIdent.unres proc.name @@ -502,6 +512,7 @@ def translateProcedureToFunction (proc : Procedure) : TranslateM Core.Decl := do inputs := inputs output := outputTy body := body + preconditions := preconditions } /-- diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T6_Preconditions.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T6_Preconditions.lean index 5853047f8..8be84a361 100644 --- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T6_Preconditions.lean +++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T6_Preconditions.lean @@ -29,6 +29,17 @@ procedure caller() { var x: int := hasRequires(1); var y: int := hasRequires(3); } + +function aFunctionWithPrecondition(x: int): int + requires x == 10 +{ + x +} + +procedure aFunctionWithPreconditionCaller() { + var x: int := aFunctionWithPrecondition(0); +//^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: assertion does not hold +} " #guard_msgs (drop info, error) in diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T8_Postconditions.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T8_Postconditions.lean index 769611336..88c32eed2 100644 --- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T8_Postconditions.lean +++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T8_Postconditions.lean @@ -33,21 +33,6 @@ procedure invalidPostcondition(x: int) // ^^^^^ error: assertion does not hold { } - -function opaqueFunction(x: int) returns (r: int) - requires x > 0 - ensures r > 0 -{ - x -} - -procedure callerOfOpaqueFunction() { - var x: int := opaqueFunction(3); - assert x > 0; -// The following assert should fail but it does not, -// because Core does not support opaque functions -// assert x == 3; -} " #guard_msgs (drop info, error) in diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T8_PostconditionsErrors.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T8_PostconditionsErrors.lean new file mode 100644 index 000000000..dc141e223 --- /dev/null +++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T8_PostconditionsErrors.lean @@ -0,0 +1,37 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import StrataTest.Util.TestDiagnostics +import StrataTest.Languages.Laurel.TestExamples + +open StrataTest.Util +open Strata + +namespace Strata.Laurel + +def program := r" + +function opaqueFunction(x: int) returns (r: int) +// ^^^^^^^^^^^^^^ error: functions with postconditions are not yet supported +// The above limitation is because Core does not yet support functions with postconditions + requires x > 0 + ensures r > 0 +// The above limitation is because functions in Core do not support postconditions +{ + x +} + +procedure callerOfOpaqueFunction() { + var x: int := opaqueFunction(3); + assert x > 0; +// The following assertion should fail but does not +// Because Core does not support opaque functions + assert x == 3; +} +" + +#guard_msgs (drop info, error) in +#eval testInputWithOffset "Postconditions" program 14 processLaurelFile From f02d1dcc62a41c6a48aed9c5ced8a88f9345333e Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 25 Feb 2026 14:40:34 +0000 Subject: [PATCH 15/28] Fix warnings --- Strata/Languages/Laurel/LiftImperativeExpressions.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Strata/Languages/Laurel/LiftImperativeExpressions.lean b/Strata/Languages/Laurel/LiftImperativeExpressions.lean index 4cb595d32..88957b9ca 100644 --- a/Strata/Languages/Laurel/LiftImperativeExpressions.lean +++ b/Strata/Languages/Laurel/LiftImperativeExpressions.lean @@ -344,12 +344,12 @@ def transformStmt (stmt : StmtExprMd) : LiftM (List StmtExprMd) := do match stmt with | WithMetadata.mk val md => match val with - | .Assert cond => + | .Assert _ => -- Do not transform assert conditions: impure expressions inside contracts -- must be rejected by the translator, not silently lifted. return [stmt] - | .Assume cond => + | .Assume _ => -- Do not transform assume conditions: same reasoning as assert. return [stmt] From 21dcb9b073dcad8f9fab67ee32ea994addd86b4d Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 25 Feb 2026 16:56:40 +0000 Subject: [PATCH 16/28] Hit cache --- Strata/Languages/Laurel/Grammar/LaurelGrammar.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean b/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean index d6664abec..b81925ddd 100644 --- a/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean +++ b/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean @@ -9,4 +9,5 @@ import Strata.DDM.Integration.Lean namespace Strata.Laurel + #load_dialect "./LaurelGrammar.st" From 52ba56ee4c59758d8a994bdbd0df221e4f8bbf8b Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 26 Feb 2026 09:11:50 +0000 Subject: [PATCH 17/28] Updated comment --- .../Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean index b85e998e4..f021f823b 100644 --- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean +++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean @@ -70,7 +70,7 @@ procedure nestedImpureStatementsAndOpaque() // An imperative procedure call in expression position is lifted before the // surrounding expression is evaluated. procedure imperativeProc(x: int) returns (r: int) - // ensures clause required because Core does not support transparent proceduces yet + // ensures clause required because Core's symbolic verification does not support transparent proceduces yet ensures r == x + 1 { r := x + 1; From 616a6a0379dd4fb36cf7be9a36511ef1aa62755e Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 26 Feb 2026 09:56:11 +0000 Subject: [PATCH 18/28] Improve error reporting for functions --- .../ConcreteToAbstractTreeTranslator.lean | 4 +- Strata/Languages/Laurel/Laurel.lean | 4 +- .../Laurel/LaurelToCoreTranslator.lean | 24 ++++++--- .../Examples/Fundamentals/T3_ControlFlow.lean | 53 +++++-------------- .../Fundamentals/T3_ControlFlowError.lean | 27 ++++++++++ 5 files changed, 62 insertions(+), 50 deletions(-) create mode 100644 StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlowError.lean diff --git a/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean b/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean index 96057b74d..df9355132 100644 --- a/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean +++ b/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean @@ -74,8 +74,8 @@ def translateBool (arg : Arg) : TransM Bool := do instance : Inhabited Parameter where default := { name := "", type := ⟨.TVoid, #[]⟩ } -def mkHighTypeMd (t : HighType) (md : MetaData Core.Expression) : HighTypeMd := ⟨t, md⟩ -def mkStmtExprMd (e : StmtExpr) (md : MetaData Core.Expression) : StmtExprMd := ⟨e, md⟩ +def mkHighTypeMd (t : HighType) (md : MetaData) : HighTypeMd := ⟨t, md⟩ +def mkStmtExprMd (e : StmtExpr) (md : MetaData) : StmtExprMd := ⟨e, md⟩ def mkStmtExprMdEmpty (e : StmtExpr) : StmtExprMd := ⟨e, #[]⟩ partial def translateHighType (arg : Arg) : TransM HighTypeMd := do diff --git a/Strata/Languages/Laurel/Laurel.lean b/Strata/Languages/Laurel/Laurel.lean index 81b25de52..41315265a 100644 --- a/Strata/Languages/Laurel/Laurel.lean +++ b/Strata/Languages/Laurel/Laurel.lean @@ -68,6 +68,8 @@ inductive Operation : Type where | StrConcat deriving Repr +abbrev MetaData := Imperative.MetaData Core.Expression + /-- A wrapper that pairs a value with source-level metadata such as source locations and annotations. All Laurel AST nodes are wrapped in @@ -78,7 +80,7 @@ structure WithMetadata (t : Type) : Type where /-- The wrapped value. -/ val : t /-- Source-level metadata (locations, annotations). -/ - md : Imperative.MetaData Core.Expression + md : MetaData /-- The type system for Laurel programs. diff --git a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean b/Strata/Languages/Laurel/LaurelToCoreTranslator.lean index 1ba05f709..c818f7e26 100644 --- a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean +++ b/Strata/Languages/Laurel/LaurelToCoreTranslator.lean @@ -116,12 +116,12 @@ def translateExpr (env : TypeEnv) (expr : StmtExprMd) -- Dummy expression used as placeholder when an error is emitted in pure context let dummy := .fvar () (Core.CoreIdent.locl s!"DUMMY_VAR_{env.length}") none -- Emit an error in pure context; panic in impure context (lifting invariant violated) - let disallowed (e : StmtExprMd) (msg : String) : TranslateM Core.Expression.Expr := do + let disallowed (md : MetaData) (msg : String) : TranslateM Core.Expression.Expr := do if isPureContext then - emitDiagnostic (e.md.toDiagnostic msg) + emitDiagnostic (md.toDiagnostic msg) return dummy else - panic! s!"translateExpr: {msg} (should have been lifted): {Std.Format.pretty (Std.ToFormat.format e)}" + panic! s!"translateExpr: {msg} (should have been lifted): {Std.Format.pretty (Std.ToFormat.format md)}" match h: expr.val with | .LiteralBool b => return .const () (.boolConst b) | .LiteralInt i => return .const () (.intConst i) @@ -188,7 +188,7 @@ def translateExpr (env : TypeEnv) (expr : StmtExprMd) | .StaticCall name args => -- In a pure context, only Core functions (not procedures) are allowed if isPureContext && !isCoreFunction funcNames name then - disallowed expr "calls to procedures are not supported in functions or contracts" + disallowed expr.md "calls to procedures are not supported in functions or contracts" else let fnOp : Core.Expression.Expr := .op () (Core.CoreIdent.unres name) none args.attach.foldlM (fun acc ⟨arg, _⟩ => do @@ -210,10 +210,17 @@ def translateExpr (env : TypeEnv) (expr : StmtExprMd) let re2 ← translateExpr env e2 boundVars isPureContext return .eq () re1 re2 | .Assign _ _ => - disallowed expr "destructive assignments are not supported in functions or contracts" + disallowed expr.md "destructive assignments are not supported in functions or contracts" | .While _ _ _ _ => - disallowed expr "loops are not supported in functions or contracts" - | .Exit _ => disallowed expr "exit is not supported in expression position" + disallowed expr.md "loops are not supported in functions or contracts" + | .Exit _ => disallowed expr.md "exit is not supported in expression position" + + | .Block (⟨ .Assert _, md⟩ :: rest) label => do + _ ← disallowed md "asserts are not YET supported in functions or contracts" + translateExpr env ⟨ StmtExpr.Block rest label, md ⟩ boundVars isPureContext + | .Block (⟨ .Assume _, md⟩ :: rest) label => + _ ← disallowed md "assumes are not YET supported in functions or contracts" + translateExpr env ⟨ StmtExpr.Block rest label, md ⟩ boundVars isPureContext | .IsType _ _ => panic "IsType should have been lowered" | .New _ => panic! s!"New should have been eliminated by typeHierarchyTransform" @@ -222,9 +229,10 @@ def translateExpr (env : TypeEnv) (expr : StmtExprMd) -- If we see one here, it's an error in the pipeline panic! s!"FieldSelect should have been eliminated by heap parameterization: {Std.ToFormat.format target}#{fieldName}" + | .Block _ _ => panic "block expression not yet implemented (should be lowered in a separate pass)" | .LocalVariable _ _ _ => panic "local variable expression not yet implemented (should be lowered in a separate pass)" - | .Return _ => disallowed expr "return expression not yet implemented (should be lowered in a separate pass)" + | .Return _ => disallowed expr.md "return expression not yet implemented (should be lowered in a separate pass)" | .AsType target _ => panic "AsType expression not implemented" | .Assigned _ => panic "assigned expression not implemented" diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlow.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlow.lean index 0ec84f449..ea08002ce 100644 --- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlow.lean +++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlow.lean @@ -10,8 +10,7 @@ import StrataTest.Languages.Laurel.TestExamples open StrataTest.Util open Strata -namespace Strata -namespace Laurel +namespace Strata.Laurel def program := r" procedure guards(a: int) returns (r: int) @@ -32,6 +31,19 @@ procedure guards(a: int) returns (r: int) return e; } +function letsInFunction() returns (r: int) { + var x: int := 0; + var y: int := x + 1; + var z: int := y + 1; + z +} + +procedure testFunctions() { + assert letsInFunction() == 2; + assert letsInFunction() == 3; +//^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: assertion does not hold +} + procedure dag(a: int) returns (r: int) { var b: int; @@ -48,40 +60,3 @@ procedure dag(a: int) returns (r: int) #guard_msgs (error, drop all) in #eval! testInputWithOffset "ControlFlow" program 14 processLaurelFile - -/- -Translation towards expression form: - -function guards(a: int): int { - var b = a + 2; - if (b > 2) { - var c = b + 3; - if (c > 3) { - c + 4; - } else { - var d = c + 5; - d + 6; - } - } else { - var e = b + 1; - e - } -} - -To translate towards SMT we only need to apply something like WP calculus. - Here's an example of what that looks like: - -function dag(a: int): int { - ( - assume a > 0; - assume b == 1; - b; - ) - OR - ( - assume a <= 0; - assume b == 2; - b; - ) -} --/ diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlowError.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlowError.lean new file mode 100644 index 000000000..7e112e50f --- /dev/null +++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlowError.lean @@ -0,0 +1,27 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import StrataTest.Util.TestDiagnostics +import StrataTest.Languages.Laurel.TestExamples + +open StrataTest.Util +open Strata + +namespace Strata.Laurel + +def program := r" +function assertAndAssumeInFunctions(a: int) returns (r: int) +{ + assert 2 == 3; +//^^^^^^^^^^^^^^ error: asserts are not YET supported in functions or contracts + assume true; +//^^^^^^^^^^^^ error: assumes are not YET supported in functions or contracts + a +} +" + +#guard_msgs (error, drop all) in +#eval! testInputWithOffset "ControlFlowError" program 14 processLaurelFile From 6db50c915446533d66fd42b1c4789d217490b5e7 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 26 Feb 2026 10:04:35 +0000 Subject: [PATCH 19/28] Attempt at supporting lettish locals in functions --- .../Laurel/LaurelToCoreTranslator.lean | 20 ++++++++++++------- .../Laurel/LiftImperativeExpressions.lean | 5 +++-- 2 files changed, 16 insertions(+), 9 deletions(-) diff --git a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean b/Strata/Languages/Laurel/LaurelToCoreTranslator.lean index c818f7e26..4bd9e0a1d 100644 --- a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean +++ b/Strata/Languages/Laurel/LaurelToCoreTranslator.lean @@ -221,6 +221,12 @@ def translateExpr (env : TypeEnv) (expr : StmtExprMd) | .Block (⟨ .Assume _, md⟩ :: rest) label => _ ← disallowed md "assumes are not YET supported in functions or contracts" translateExpr env ⟨ StmtExpr.Block rest label, md ⟩ boundVars isPureContext + | .Block (⟨ .LocalVariable name ty (some initializer), md⟩ :: rest) label => do + let env' := (name, ty) :: env + let coreMonoType := translateType ty + let valueExpr ← translateExpr env initializer boundVars isPureContext + let bodyExpr ← translateExpr env ⟨ StmtExpr.Block rest label, md ⟩ (name :: boundVars) isPureContext + return .app () (.abs () (some coreMonoType) bodyExpr) valueExpr | .IsType _ _ => panic "IsType should have been lowered" | .New _ => panic! s!"New should have been eliminated by typeHierarchyTransform" @@ -291,29 +297,29 @@ def translateStmt (env : TypeEnv) (outputParams : List Parameter) (stmt : StmtEx return (env', stmtsList) | .LocalVariable name ty initializer => let env' := (name, ty) :: env - let boogieMonoType := translateType ty - let boogieType := LTy.forAll [] boogieMonoType + let coreMonoType := translateType ty + let coreType := LTy.forAll [] coreMonoType let ident := Core.CoreIdent.locl name match initializer with | some (⟨ .StaticCall callee args, callMd⟩) => -- Check if this is a function or a procedure call if isCoreFunction functionNames callee then -- Translate as expression (function application) - let boogieExpr ← translateExpr env (⟨ .StaticCall callee args, callMd ⟩) - return (env', [Core.Statement.init ident boogieType (some boogieExpr) md]) + let coreExpr ← translateExpr env (⟨ .StaticCall callee args, callMd ⟩) + return (env', [Core.Statement.init ident coreType (some coreExpr) md]) else -- Translate as: var name; call name := callee(args) let coreArgs ← args.mapM (fun a => translateExpr env a) let defaultExpr := defaultExprForType ty - let initStmt := Core.Statement.init ident boogieType (some defaultExpr) + let initStmt := Core.Statement.init ident coreType (some defaultExpr) let callStmt := Core.Statement.call [ident] callee coreArgs return (env', [initStmt, callStmt]) | some initExpr => let coreExpr ← translateExpr env initExpr - return (env', [Core.Statement.init ident boogieType (some coreExpr)]) + return (env', [Core.Statement.init ident coreType (some coreExpr)]) | none => let defaultExpr := defaultExprForType ty - return (env', [Core.Statement.init ident boogieType (some defaultExpr)]) + return (env', [Core.Statement.init ident coreType (some defaultExpr)]) | .Assign targets value => match targets with | [⟨ .Identifier name, _ ⟩] => diff --git a/Strata/Languages/Laurel/LiftImperativeExpressions.lean b/Strata/Languages/Laurel/LiftImperativeExpressions.lean index 88957b9ca..1b0d70a17 100644 --- a/Strata/Languages/Laurel/LiftImperativeExpressions.lean +++ b/Strata/Languages/Laurel/LiftImperativeExpressions.lean @@ -467,7 +467,8 @@ Transform a program to lift all assignments that occur in an expression context. def liftImperativeExpressions (program : Program) : Program := let imperativeNames := program.staticProcedures.filter (fun p => !p.isFunctional) |>.map (·.name) let initState : LiftState := { types := program.types, imperativeNames := imperativeNames, procedures := program.staticProcedures } - let (seqProcedures, _) := (program.staticProcedures.mapM transformProcedure).run initState - { program with staticProcedures := seqProcedures } + let (imperativeProcs, functionalProcs) := program.staticProcedures.partition (fun p => !p.isFunctional) + let (seqProcedures, _) := (imperativeProcs.mapM transformProcedure).run initState + { program with staticProcedures := seqProcedures ++ functionalProcs } end Laurel From 13a9aee3f6e943e8b43adef1561c9a96f960e6a3 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 26 Feb 2026 11:01:17 +0000 Subject: [PATCH 20/28] Support guard pattern --- .../Laurel/LaurelToCoreTranslator.lean | 2 ++ .../Examples/Fundamentals/T3_ControlFlow.lean | 29 ++++++++++++++----- 2 files changed, 23 insertions(+), 8 deletions(-) diff --git a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean b/Strata/Languages/Laurel/LaurelToCoreTranslator.lean index 4bd9e0a1d..daced76cc 100644 --- a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean +++ b/Strata/Languages/Laurel/LaurelToCoreTranslator.lean @@ -11,6 +11,7 @@ import Strata.Languages.Core.Procedure import Strata.Languages.Core.Options import Strata.Languages.Laurel.Laurel import Strata.Languages.Laurel.LiftImperativeExpressions +import Strata.Languages.Laurel.GuardReturnElim import Strata.Languages.Laurel.HeapParameterization import Strata.Languages.Laurel.TypeHierarchy import Strata.Languages.Laurel.LaurelTypes @@ -587,6 +588,7 @@ def translate (program : Program) : Except (Array DiagnosticModel) (Core.Program dbg_trace (toString (Std.Format.pretty (Std.ToFormat.format program))) dbg_trace "=================================" let program := liftImperativeExpressions program + let program := guardReturnElim program -- Collect field names from the Field datatype (generated by heapParameterization) let fieldNames : List Identifier := program.types.foldl (fun acc td => match td with diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlow.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlow.lean index ea08002ce..5a804729e 100644 --- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlow.lean +++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlow.lean @@ -31,17 +31,30 @@ procedure guards(a: int) returns (r: int) return e; } -function letsInFunction() returns (r: int) { - var x: int := 0; - var y: int := x + 1; - var z: int := y + 1; - z +// Lettish bindings in functions not yet supported +// because Core expressions do not support let bindings +// function letsInFunction() returns (r: int) { +// var x: int := 0; +// var y: int := x + 1; +// var z: int := y + 1; +// z +// } + +function guardInFunction(x: int) returns (r: int) { + if (x > 0) { + return 1; + } + + return 2; } procedure testFunctions() { - assert letsInFunction() == 2; - assert letsInFunction() == 3; -//^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: assertion does not hold + // assert letsInFunction() == 2; + // assert letsInFunction() == 3; error: assertion does not hold + + assert guardInFunction(5) == 1; + assert guardInFunction(5) == 2; +//^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: assertion does not hold } procedure dag(a: int) returns (r: int) From 525f25cfc2a5413102cab91e3c45b6e4db056086 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 26 Feb 2026 12:20:08 +0000 Subject: [PATCH 21/28] Improve algorithm and fix test --- .../Laurel/EliminateReturnsInExpression.lean | 116 ++++++++++++++++++ .../Laurel/LaurelToCoreTranslator.lean | 4 +- .../Laurel/LiftImperativeExpressions.lean | 4 +- .../Examples/Fundamentals/T3_ControlFlow.lean | 28 ++++- 4 files changed, 143 insertions(+), 9 deletions(-) create mode 100644 Strata/Languages/Laurel/EliminateReturnsInExpression.lean diff --git a/Strata/Languages/Laurel/EliminateReturnsInExpression.lean b/Strata/Languages/Laurel/EliminateReturnsInExpression.lean new file mode 100644 index 000000000..be476fa22 --- /dev/null +++ b/Strata/Languages/Laurel/EliminateReturnsInExpression.lean @@ -0,0 +1,116 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import Strata.Languages.Laurel.Laurel +import Strata.Util.Tactics + +/-! +# Eliminate Returns in Expression Position + +Rewrites functional procedure bodies so that `return` statements are removed +and early-return guard patterns become if-then-else expressions. This makes +the body a pure expression tree suitable for translation to a Core function. + +The algorithm walks a block backwards (from last statement to first), +accumulating a result expression: + +- The last statement is converted via `lastStmtToExpr` which strips `return`, + recurses into blocks, and handles if-then-else. +- Each preceding statement wraps around the accumulated result via `stmtsToExpr`: + - `if (cond) { body }` (no else) becomes `if cond then lastStmtToExpr(body) else acc` + - Other statements are kept in a two-element block with the accumulator. + +-/ + +namespace Strata.Laurel + +/-- Appending a singleton strictly increases `sizeOf`. -/ +private theorem List.sizeOf_lt_append_singleton [SizeOf α] (xs : List α) (y : α) : + sizeOf xs < sizeOf (xs ++ [y]) := by + induction xs with + | nil => simp_all; omega + | cons hd tl ih => simp_all [List.cons_append] + +/-- `dropLast` of a non-empty list has strictly smaller `sizeOf`. -/ +private theorem List.sizeOf_dropLast_lt [SizeOf α] {l : List α} (h_ne : l ≠ []) : + sizeOf l.dropLast < sizeOf l := by + have h_concat := List.dropLast_concat_getLast h_ne + have : sizeOf l = sizeOf (l.dropLast ++ [l.getLast h_ne]) := by rw [h_concat] + rw [this] + exact List.sizeOf_lt_append_singleton l.dropLast (l.getLast h_ne) + +mutual + +/-- +Fold a list of preceding statements (right-to-left) around an accumulator +expression. Each `if-then` (no else) guard wraps as +`if cond then lastStmtToExpr(body) else acc`; other statements produce +`Block [stmt, acc]`. +-/ +def stmtsToExpr (stmts : List StmtExprMd) (acc : StmtExprMd) (blockMd : MetaData) + : StmtExprMd := + match stmts with + | [] => acc + | s :: rest => + let acc' := stmtsToExpr rest acc blockMd + match s with + | ⟨.IfThenElse cond thenBr none, smd⟩ => + ⟨.IfThenElse cond (lastStmtToExpr thenBr) (some acc'), smd⟩ + | _ => + ⟨.Block [s, acc'] none, blockMd⟩ + termination_by (sizeOf stmts, 1) + +/-- +Convert the last statement of a block into an expression. +- `return expr` → `expr` +- A non-empty block → process last element, fold preceding statements +- `if cond then A else B` → recurse into both branches +- Anything else → kept as-is +-/ +def lastStmtToExpr (stmt : StmtExprMd) : StmtExprMd := + match stmt with + | ⟨.Return (some val), _⟩ => val + | ⟨.Block stmts _, md⟩ => + match h_last : stmts.getLast? with + | some last => + have := List.mem_of_getLast? h_last + let lastExpr := lastStmtToExpr last + let dropped := stmts.dropLast + -- have := List.dropLast_subset stmts + have h : sizeOf stmts.dropLast < sizeOf stmts := + List.sizeOf_dropLast_lt (by intro h; simp [h] at h_last) + stmtsToExpr dropped lastExpr md + | none => stmt + | ⟨.IfThenElse cond thenBr (some elseBr), md⟩ => + ⟨.IfThenElse cond (lastStmtToExpr thenBr) (some (lastStmtToExpr elseBr)), md⟩ + | _ => stmt + termination_by (sizeOf stmt, 0) + decreasing_by + all_goals (simp_all; term_by_mem) + +end + +/-- +Apply return elimination to a functional procedure's body. +The entire body is treated as an expression to be converted. +-/ +def eliminateReturnsInExpression (proc : Procedure) : Procedure := + if !proc.isFunctional then proc + else + match proc.body with + | .Transparent bodyExpr => + { proc with body := .Transparent (lastStmtToExpr bodyExpr) } + | .Opaque postconds (some impl) modif => + { proc with body := .Opaque postconds (some (lastStmtToExpr impl)) modif } + | _ => proc + +/-- +Transform a program by eliminating returns in all functional procedure bodies. +-/ +def eliminateReturnsInExpressionTransform (program : Program) : Program := + { program with staticProcedures := program.staticProcedures.map eliminateReturnsInExpression } + +end Laurel diff --git a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean b/Strata/Languages/Laurel/LaurelToCoreTranslator.lean index daced76cc..04703c4fe 100644 --- a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean +++ b/Strata/Languages/Laurel/LaurelToCoreTranslator.lean @@ -11,7 +11,7 @@ import Strata.Languages.Core.Procedure import Strata.Languages.Core.Options import Strata.Languages.Laurel.Laurel import Strata.Languages.Laurel.LiftImperativeExpressions -import Strata.Languages.Laurel.GuardReturnElim +import Strata.Languages.Laurel.EliminateReturnsInExpression import Strata.Languages.Laurel.HeapParameterization import Strata.Languages.Laurel.TypeHierarchy import Strata.Languages.Laurel.LaurelTypes @@ -588,7 +588,7 @@ def translate (program : Program) : Except (Array DiagnosticModel) (Core.Program dbg_trace (toString (Std.Format.pretty (Std.ToFormat.format program))) dbg_trace "=================================" let program := liftImperativeExpressions program - let program := guardReturnElim program + let program := eliminateReturnsInExpressionTransform program -- Collect field names from the Field datatype (generated by heapParameterization) let fieldNames : List Identifier := program.types.foldl (fun acc td => match td with diff --git a/Strata/Languages/Laurel/LiftImperativeExpressions.lean b/Strata/Languages/Laurel/LiftImperativeExpressions.lean index 1b0d70a17..60f1ab9f4 100644 --- a/Strata/Languages/Laurel/LiftImperativeExpressions.lean +++ b/Strata/Languages/Laurel/LiftImperativeExpressions.lean @@ -312,9 +312,7 @@ def transformExpr (expr : StmtExprMd) : LiftM StmtExprMd := do 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 + term_by_mem /-- 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. diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlow.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlow.lean index 5a804729e..235f7350b 100644 --- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlow.lean +++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlow.lean @@ -40,20 +40,40 @@ procedure guards(a: int) returns (r: int) // z // } +function returnAtEnd(x: int) returns (r: int) { + if (x > 0) { + if (x == 1) { + return 1; + } else { + return 2; + } + } else { + return 3; + } +} + function guardInFunction(x: int) returns (r: int) { if (x > 0) { - return 1; + if (x == 1) { + return 1; + } else { + return 2; + } } - return 2; + return 3; } procedure testFunctions() { // assert letsInFunction() == 2; // assert letsInFunction() == 3; error: assertion does not hold - assert guardInFunction(5) == 1; - assert guardInFunction(5) == 2; + assert returnAtEnd(1) == 1; + assert returnAtEnd(1) == 2; +//^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: assertion does not hold + + assert guardInFunction(1) == 1; + assert guardInFunction(1) == 2; //^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: assertion does not hold } From a7fe1fcfcd4e9b4d3532d5bd1f74d66797da8c4f Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 26 Feb 2026 19:31:37 +0000 Subject: [PATCH 22/28] Fixes --- .../Laurel/LaurelToCoreTranslator.lean | 42 ++++++++++--------- .../Laurel/LiftImperativeExpressions.lean | 4 +- .../Fundamentals/T6_Preconditions.lean | 2 +- .../Laurel/LiftExpressionAssignmentsTest.lean | 6 +-- 4 files changed, 28 insertions(+), 26 deletions(-) diff --git a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean b/Strata/Languages/Laurel/LaurelToCoreTranslator.lean index 8f5b2a83e..640599c04 100644 --- a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean +++ b/Strata/Languages/Laurel/LaurelToCoreTranslator.lean @@ -368,16 +368,28 @@ def translateStmt (env : TypeEnv) (outputParams : List Parameter) (stmt : StmtEx | .While cond invariants decreasesExpr body => let condExpr ← translateExpr env cond let invExprs ← invariants.mapM (translateExpr env) - let decreasingExprCore ← decreasesExpr.map (translateExpr env) + let decreasingExprCore ← decreasesExpr.mapM (translateExpr env) let (_, bodyStmts) ← translateStmt env outputParams body - (env, [Imperative.Stmt.loop condExpr decreasingExprCore invExprs bodyStmts md]) - | _ => (env, []) + return (env, [Imperative.Stmt.loop condExpr decreasingExprCore invExprs bodyStmts md]) + | _ => return (env, []) termination_by sizeOf stmt decreasing_by all_goals have hlt := WithMetadata.sizeOf_val_lt stmt cases stmt; term_by_mem +/-- +Translate a list of checks (preconditions or postconditions) to Core checks. +Each check gets a label like `"requires"` or `"requires_0"`, `"requires_1"`, etc. +-/ +private def translateChecks (env : TypeEnv) (checks : List StmtExprMd) (labelBase : String) + : TranslateM (ListMap Core.CoreLabel Core.Procedure.Check) := + checks.mapIdxM (fun i check => do + let label := if checks.length == 1 then labelBase else s!"{labelBase}_{i}" + let checkExpr ← translateExpr env check [] (isPureContext := true) + let c : Core.Procedure.Check := { expr := checkExpr, md := check.md } + return (label, c)) + /-- Translate Laurel Parameter to Core Signature entry -/ @@ -404,21 +416,13 @@ def translateProcedure (proc : Procedure) : TranslateM Core.Procedure := do let initEnv : TypeEnv := proc.inputs.map (fun p => (p.name, p.type)) ++ proc.outputs.map (fun p => (p.name, p.type)) -- Translate preconditions - let preconditions : ListMap Core.CoreLabel Core.Procedure.Check := - 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 initEnv precond, md := precond.md } - (i + 1, acc ++ [(label, check)])) (0, []) - result + let preconditions ← translateChecks initEnv proc.preconditions "requires" + -- Translate postconditions for Opaque bodies let postconditions : ListMap Core.CoreLabel Core.Procedure.Check ← match proc.body with | .Opaque postconds _ _ => - postconds.mapIdxM (fun i postcond => do - let label := if postconds.length == 1 then "postcondition" else s!"postcondition_{i}" - let e ← translateExpr initEnv postcond [] (isPureContext := true) - let check : Core.Procedure.Check := { expr := e, md := postcond.md } - pure (label, check)) + translateChecks initEnv postconds "postcondition" | _ => pure [] let modifies : List Core.Expression.Ident := [] let body : List Core.Statement ← @@ -501,12 +505,10 @@ def translateProcedureToFunction (proc : Procedure) : TranslateM Core.Decl := do | none => LMonoTy.int let initEnv : TypeEnv := proc.inputs.map (fun p => (p.name, p.type)) -- Translate precondition to FuncPrecondition (skip trivial `true`) - let preconditions : List (Lambda.FuncPrecondition Core.Expression.Expr Core.ExpressionMetadata) ← - match proc.precondition with - | ⟨ .LiteralBool true, _ ⟩ => pure [] - | precond => - let e ← translateExpr initEnv precond [] (isPureContext := true) - pure [{ expr := e, md := () }] + let preconditions ← proc.preconditions.mapM (fun precondition => do + let checkExpr ← translateExpr initEnv precondition [] true + return { expr := checkExpr, md := () }) + let body ← match proc.body with | .Transparent bodyExpr => some <$> translateExpr initEnv bodyExpr [] (isPureContext := true) | .Opaque _ (some bodyExpr) _ => diff --git a/Strata/Languages/Laurel/LiftImperativeExpressions.lean b/Strata/Languages/Laurel/LiftImperativeExpressions.lean index eb6404490..027eb3380 100644 --- a/Strata/Languages/Laurel/LiftImperativeExpressions.lean +++ b/Strata/Languages/Laurel/LiftImperativeExpressions.lean @@ -369,7 +369,7 @@ def transformStmt (stmt : StmtExprMd) : LiftM (List StmtExprMd) := do -- If the RHS is a direct imperative StaticCall, don't lift it — -- translateStmt handles Assign + StaticCall directly as a call statement. match _:value with - | WithMetadata.mk val md => + | WithMetadata.mk val valueMd => match _:val with | .StaticCall callee args => let imperative := (← get).imperativeNames @@ -377,7 +377,7 @@ def transformStmt (stmt : StmtExprMd) : LiftM (List StmtExprMd) := do let seqArgs ← args.mapM transformExpr let argPrepends ← takePrepends modify fun s => { s with subst := [] } - return argPrepends ++ [⟨.Assign targets ⟨.StaticCall callee seqArgs, value.md⟩, md⟩] + return argPrepends ++ [⟨.Assign targets ⟨.StaticCall callee seqArgs, valueMd⟩, md⟩] else let seqValue ← transformExpr value let prepends ← takePrepends diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T6_Preconditions.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T6_Preconditions.lean index 8be84a361..45c9a982a 100644 --- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T6_Preconditions.lean +++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T6_Preconditions.lean @@ -38,7 +38,7 @@ function aFunctionWithPrecondition(x: int): int procedure aFunctionWithPreconditionCaller() { var x: int := aFunctionWithPrecondition(0); -//^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: assertion does not hold +// ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: assertion does not hold } " diff --git a/StrataTest/Languages/Laurel/LiftExpressionAssignmentsTest.lean b/StrataTest/Languages/Laurel/LiftExpressionAssignmentsTest.lean index ea03e304a..dc486f7de 100644 --- a/StrataTest/Languages/Laurel/LiftExpressionAssignmentsTest.lean +++ b/StrataTest/Languages/Laurel/LiftExpressionAssignmentsTest.lean @@ -47,14 +47,14 @@ def parseLaurelAndLift (input : String) : IO Program := do 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) + | .ok program => pure (liftImperativeExpressions program) /-- -info: procedure heapUpdateInBlockExpr(b: Box) returns +info: procedure heapUpdateInBlockExpr(b: Box) returns ⏎ () deterministic { b#value := b#value + 1; var x: int := b#value; assert x == b#value } -procedure assertInBlockExpr() returns +procedure assertInBlockExpr() returns ⏎ () deterministic { var x: int := 0; assert x == 0; x := 1; var y: int := x; assert y == 1 } From 6b36544cbf48787f72bbf072fac9ed4ada56b367 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 4 Mar 2026 12:37:29 +0000 Subject: [PATCH 23/28] Fixes and cleanup --- .../Laurel/LaurelToCoreTranslator.lean | 75 +++---------------- .../Examples/Fundamentals/T3_ControlFlow.lean | 9 --- .../Fundamentals/T3_ControlFlowError.lean | 18 +++++ 3 files changed, 27 insertions(+), 75 deletions(-) diff --git a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean b/Strata/Languages/Laurel/LaurelToCoreTranslator.lean index 2db4eb026..7b432851d 100644 --- a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean +++ b/Strata/Languages/Laurel/LaurelToCoreTranslator.lean @@ -221,11 +221,15 @@ def translateExpr (env : TypeEnv) (expr : StmtExprMd) _ ← disallowed md "assumes are not YET supported in functions or contracts" translateExpr env ⟨ StmtExpr.Block rest label, md ⟩ boundVars isPureContext | .Block (⟨ .LocalVariable name ty (some initializer), md⟩ :: rest) label => do - let env' := (name, ty) :: env - let coreMonoType := translateType ty - let valueExpr ← translateExpr env initializer boundVars isPureContext - let bodyExpr ← translateExpr env ⟨ StmtExpr.Block rest label, md ⟩ (name :: boundVars) isPureContext - return .app () (.abs () (some coreMonoType) bodyExpr) valueExpr + let env' := (name, ty) :: env + let valueExpr ← translateExpr env initializer boundVars isPureContext + let bodyExpr ← translateExpr env' ⟨ StmtExpr.Block rest label, md ⟩ (name :: boundVars) isPureContext + disallowed md "local variables in functions are not YET supported" + -- This doesn't work because of a limitation in Core. + -- let coreMonoType := translateType ty + -- return .app () (.abs () (some coreMonoType) bodyExpr) valueExpr + | .Block (⟨ .LocalVariable name ty none, md⟩ :: rest) label => + disallowed md "local variables in functions must have initializers" | .IsType _ _ => panic "IsType should have been lowered" | .New _ => panic! s!"New should have been eliminated by typeHierarchyTransform" @@ -444,67 +448,6 @@ def translateProcedure (proc : Procedure) : TranslateM Core.Procedure := do let spec : Core.Procedure.Spec := { modifies, preconditions, postconditions } return { header, spec, body } -/-- -Check if a Laurel expression is pure (contains no side effects). -Used to determine if a procedure can be translated as a Core function. --/ -private def isPureExpr(expr: StmtExprMd): Bool := - match _h : expr.val with - | .LiteralBool _ => true - | .LiteralInt _ => true - | .LiteralString _ => true - | .Identifier _ => true - | .PrimitiveOp _ args => args.attach.all (fun ⟨a, _⟩ => isPureExpr a) - | .IfThenElse c t none => isPureExpr c && isPureExpr t - | .IfThenElse c t (some e) => isPureExpr c && isPureExpr t && isPureExpr e - | .StaticCall _ args => args.attach.all (fun ⟨a, _⟩ => isPureExpr a) - | .New _ => false - | .ReferenceEquals e1 e2 => isPureExpr e1 && isPureExpr e2 - | .Block [single] _ => isPureExpr single - | .Block _ _ => false - -- Statement-like - | .LocalVariable .. => true - | .While .. => false - | .Exit .. => false - | .Return .. => false - -- Expression-like - | .Assign .. => false - | .FieldSelect .. => true - | .PureFieldUpdate .. => true - -- Instance related - | .This => panic s!"isPureExpr not implemented for This" - | .AsType .. => panic s!"isPureExpr not supported for AsType" - | .IsType .. => panic s!"isPureExpr not supported for IsType" - | .InstanceCall .. => panic s!"isPureExpr not implemented for InstanceCall" - -- Verification specific - | .Forall .. => panic s!"isPureExpr not implemented for Forall" - | .Exists .. => panic s!"isPureExpr not implemented for Exists" - | .Assigned .. => panic s!"isPureExpr not supported for AsType" - | .Old .. => panic s!"isPureExpr not supported for AsType" - | .Fresh .. => panic s!"isPureExpr not supported for AsType" - | .Assert .. => panic s!"isPureExpr not implemented for Assert" - | .Assume .. => panic s!"isPureExpr not implemented for Assume" - | .ProveBy .. => panic s!"isPureExpr not implemented for ProveBy" - | .ContractOf .. => panic s!"isPureExpr not implemented for ContractOf" - | .Abstract => panic s!"isPureExpr not implemented for Abstract" - | .All => panic s!"isPureExpr not implemented for All" - -- Dynamic / closures - | .Hole => true - termination_by sizeOf expr - decreasing_by all_goals (have := WithMetadata.sizeOf_val_lt expr; term_by_mem) - -/-- Check if a pure-marked procedure can actually be represented as a Core function: - transparent body that is a pure expression and has exactly one output. -/ -private def canBeCoreFunctionBody (proc : Procedure) : Bool := - match proc.body with - | .Transparent bodyExpr => - isPureExpr bodyExpr && - proc.outputs.length == 1 - | .Opaque _ bodyExprOption _ => - (bodyExprOption.map isPureExpr).getD true && - proc.outputs.length == 1 - | _ => false - /-- Translate a Laurel Procedure to a Core Function (when applicable) using `TranslateM`. Diagnostics for disallowed constructs in the function body are emitted into the monad state. diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlow.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlow.lean index 235f7350b..8f9b55a22 100644 --- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlow.lean +++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlow.lean @@ -31,15 +31,6 @@ procedure guards(a: int) returns (r: int) return e; } -// Lettish bindings in functions not yet supported -// because Core expressions do not support let bindings -// function letsInFunction() returns (r: int) { -// var x: int := 0; -// var y: int := x + 1; -// var z: int := y + 1; -// z -// } - function returnAtEnd(x: int) returns (r: int) { if (x > 0) { if (x == 1) { diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlowError.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlowError.lean index 7e112e50f..8e26f000b 100644 --- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlowError.lean +++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlowError.lean @@ -21,6 +21,24 @@ function assertAndAssumeInFunctions(a: int) returns (r: int) //^^^^^^^^^^^^ error: assumes are not YET supported in functions or contracts a } + +// Lettish bindings in functions not yet supported +// because Core expressions do not support let bindings +function letsInFunction() returns (r: int) { + var x: int := 0; +//^^^^^^^^^^^^^^^^ error: local variables in functions are not YET supported + var y: int := x + 1; +//^^^^^^^^^^^^^^^^^^^^ error: local variables in functions are not YET supported + var z: int := y + 1; +//^^^^^^^^^^^^^^^^^^^^ error: local variables in functions are not YET supported + z +} + +function localVariableWithoutInitializer(): int { + var x: int; +//^^^^^^^^^^^ error: local variables in functions must have initializers + 3 +} " #guard_msgs (error, drop all) in From b57985764f88c06588a8d18f3b627b40da75042e Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 4 Mar 2026 12:45:53 +0000 Subject: [PATCH 24/28] Fail gracefully when having an if-then-else as a non-last statement in a function block --- Strata/Languages/Laurel/LaurelToCoreTranslator.lean | 4 +++- .../Laurel/Examples/Fundamentals/T3_ControlFlowError.lean | 6 ++++++ 2 files changed, 9 insertions(+), 1 deletion(-) diff --git a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean b/Strata/Languages/Laurel/LaurelToCoreTranslator.lean index 7b432851d..6f729d5a2 100644 --- a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean +++ b/Strata/Languages/Laurel/LaurelToCoreTranslator.lean @@ -230,6 +230,8 @@ def translateExpr (env : TypeEnv) (expr : StmtExprMd) -- return .app () (.abs () (some coreMonoType) bodyExpr) valueExpr | .Block (⟨ .LocalVariable name ty none, md⟩ :: rest) label => disallowed md "local variables in functions must have initializers" + | .Block (⟨ .IfThenElse cond thenBranch (some elseBranch), md⟩ :: rest) label => + disallowed md "if-then-else only supported as the last statement in a block" | .IsType _ _ => panic "IsType should have been lowered" | .New _ => panic! s!"New should have been eliminated by typeHierarchyTransform" @@ -237,7 +239,7 @@ def translateExpr (env : TypeEnv) (expr : StmtExprMd) -- Field selects should have been eliminated by heap parameterization -- If we see one here, it's an error in the pipeline panic! s!"FieldSelect should have been eliminated by heap parameterization: {Std.ToFormat.format target}#{fieldName}" - | .Block _ _ => panic "block expression not yet implemented (should be lowered in a separate pass)" + | .Block _ _ => panic! "block expression should have been lowered in a separate pass" | .LocalVariable _ _ _ => panic "local variable expression not yet implemented (should be lowered in a separate pass)" | .Return _ => disallowed expr.md "return expression not yet implemented (should be lowered in a separate pass)" diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlowError.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlowError.lean index 8e26f000b..b9a5ebe37 100644 --- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlowError.lean +++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlowError.lean @@ -39,6 +39,12 @@ function localVariableWithoutInitializer(): int { //^^^^^^^^^^^ error: local variables in functions must have initializers 3 } + +function deadCodeAfterIfElse(x: int) returns (r: int) { + if (x > 0) { return 1; } else { return 2; } +//^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: if-then-else only supported as the last statement in a block + return 3; +} " #guard_msgs (error, drop all) in From 97153bf70833008df29a3e5de7d477a51eae90d1 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 5 Mar 2026 09:51:12 +0000 Subject: [PATCH 25/28] Update CodeOwners file --- .github/CODEOWNERS | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index 33f0e40ea..92eebe582 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -3,7 +3,8 @@ * @strata-org/reviewers # Laurel language -Strata/Languages/Laurel/ @strata-org/reviewers @keyboardDrummer @fabiomadge -StrataTest/Languages/Laurel/ @strata-org/reviewers @keyboardDrummer @fabiomadge -Strata/Languages/Python/ @strata-org/reviewers @keyboardDrummer @fabiomadge -StrataTest/Languages/Python/ @strata-org/reviewers @keyboardDrummer @fabiomadge \ No newline at end of file +/Strata/Languages/Laurel @strata-org/reviewers @keyboardDrummer @fabiomadge +/StrataTest/Languages/Laurel @strata-org/reviewers @keyboardDrummer @fabiomadge +/Strata/Languages/Python @strata-org/reviewers @keyboardDrummer @fabiomadge +/StrataTest/Languages/Python @strata-org/reviewers @keyboardDrummer @fabiomadge +/docs/verso @strata-org/reviewers @keyboardDrummer @fabiomadge \ No newline at end of file From 258762c9e9955fe0cacda037822a0c78288e3727 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 6 Mar 2026 08:33:49 +0000 Subject: [PATCH 26/28] Move test-case --- .../Examples/Fundamentals/T3_ControlFlow.lean | 36 +++++++++---------- 1 file changed, 18 insertions(+), 18 deletions(-) diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlow.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlow.lean index d211ad4ae..124a64c56 100644 --- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlow.lean +++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlow.lean @@ -13,24 +13,6 @@ open Strata namespace Strata.Laurel def program := r" -procedure guards(a: int) returns (r: int) -{ - var b: int := a + 2; - if (b > 2) { - var c: int := b + 3; - if (c > 3) { - return c + 4; - } - var d: int := c + 5; - return d + 6; - } - var e: int := b + 1; - assert e <= 3; - assert e < 3; -// ^^^^^^^^^^^^^ error: assertion does not hold - return e; -} - function returnAtEnd(x: int) returns (r: int) { if (x > 0) { if (x == 1) { @@ -68,6 +50,24 @@ procedure testFunctions() { //^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: assertion does not hold } +procedure guards(a: int) returns (r: int) +{ + var b: int := a + 2; + if (b > 2) { + var c: int := b + 3; + if (c > 3) { + return c + 4; + } + var d: int := c + 5; + return d + 6; + } + var e: int := b + 1; + assert e <= 3; + assert e < 3; +// ^^^^^^^^^^^^^ error: assertion does not hold + return e; +} + procedure dag(a: int) returns (r: int) { var b: int; From 7a0530c92ffaa1e70f34f78bb67316bbbcb1bbef Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 9 Mar 2026 14:54:53 +0100 Subject: [PATCH 27/28] Fix variable capture bug --- Strata/Languages/Laurel/LiftImperativeExpressions.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Strata/Languages/Laurel/LiftImperativeExpressions.lean b/Strata/Languages/Laurel/LiftImperativeExpressions.lean index 6e5520a40..3ab2a2042 100644 --- a/Strata/Languages/Laurel/LiftImperativeExpressions.lean +++ b/Strata/Languages/Laurel/LiftImperativeExpressions.lean @@ -321,7 +321,7 @@ def transformStmt (stmt : StmtExprMd) : LiftM (List StmtExprMd) := do -- If the initializer is a direct imperative StaticCall, don't lift it — -- translateStmt handles LocalVariable + StaticCall directly as a call statement. match _: initExprMd with - | WithMetadata.mk initExpr md => + | WithMetadata.mk initExpr _ => match _: initExpr with | .StaticCall callee args => let model := (← get).model From 151348170ea082f7ac4d35df2b7559dbf9215757 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 9 Mar 2026 23:14:56 +0100 Subject: [PATCH 28/28] Fix test expect files --- StrataTest/Languages/Laurel/DivisionByZeroCheckTest.lean | 7 +++++-- .../Laurel/Examples/Fundamentals/T6_Preconditions.lean | 3 ++- 2 files changed, 7 insertions(+), 3 deletions(-) diff --git a/StrataTest/Languages/Laurel/DivisionByZeroCheckTest.lean b/StrataTest/Languages/Laurel/DivisionByZeroCheckTest.lean index 55717ef66..2d8eb89ec 100644 --- a/StrataTest/Languages/Laurel/DivisionByZeroCheckTest.lean +++ b/StrataTest/Languages/Laurel/DivisionByZeroCheckTest.lean @@ -26,9 +26,11 @@ procedure safeDivision() { assert z == 5; } +// Error ranges are too wide because Core does not use expression locations procedure unsafeDivision(x: int) { var z: int := 10 / x; -// ^^^^^^ error: assertion does not hold +//^^^^^^^^^^^^^^^^^^^^^ error: assertion does not hold +// Error ranges are too wide because Core does not use expression locations } function pureDiv(x: int, y: int): int @@ -44,7 +46,8 @@ procedure callPureDivSafe() { procedure callPureDivUnsafe(x: int) { var z: int := pureDiv(10, x); -// ^^^^^^^^^^^^^^ error: assertion does not hold +//^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: assertion does not hold +// Error ranges are too wide because Core does not use expression locations } " diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T6_Preconditions.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T6_Preconditions.lean index 45c9a982a..8132a6864 100644 --- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T6_Preconditions.lean +++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T6_Preconditions.lean @@ -38,7 +38,8 @@ function aFunctionWithPrecondition(x: int): int procedure aFunctionWithPreconditionCaller() { var x: int := aFunctionWithPrecondition(0); -// ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: assertion does not hold +//^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: assertion does not hold +// Error ranges are too wide because Core does not use expression locations } "