Issue 924 contract and proof pass

Examples/StringTest.laurel.st

@@ -1,6 +1,7 @@
 procedure testString()
 returns (result: string)
 requires true
+  opaque
 {
   var message: string := "Hello, World!";
   return message
@@ -9,6 +10,7 @@ requires true
 procedure testStringConcat()
 returns (result: string)
 requires true
+  opaque
 {
   var hello: string := "Hello";
   var world: string := "World";

Strata/Languages/Laurel/ConstrainedTypeElim.lean

@@ -92,8 +92,8 @@ def resolveExprNode (ptMap : ConstrainedTypeMap) (expr : StmtExprMd) : StmtExprM
   let source := expr.source
   let md := expr.md
   match expr.val with
-  | .LocalVariable n ty init =>
-    ⟨.LocalVariable n (resolveType ptMap ty) init, source, md⟩
+  | .LocalVariable params init =>
+    ⟨.LocalVariable (params.map fun p => { p with type := resolveType ptMap p.type }) init, source, md⟩
   | .Forall param trigger body =>
     let param' := { param with type := resolveType ptMap param.type }
     -- With bottom-up traversal, `body` is already recursed into. The newly
@@ -127,15 +127,18 @@ def elimStmt (ptMap : ConstrainedTypeMap)
   let source := stmt.source
   let md := stmt.md
   match _h : stmt.val with
-  | .LocalVariable name ty init =>
-    let callOpt := constraintCallFor ptMap ty.val name md (src := source)
-    if callOpt.isSome then modify fun pv => pv.insert name.text ty.val
+  | .LocalVariable params init =>
+    for p in params do
+      let callOpt := constraintCallFor ptMap p.type.val p.name md (src := source)
+      if callOpt.isSome then modify fun pv => pv.insert p.name.text p.type.val
     let (init', check) : Option StmtExprMd × List StmtExprMd := match init with
-      | none => match callOpt with
-        | some c => (none, [⟨.Assume c, source, md⟩])
-        | none => (none, [])
-      | some _ => (init, callOpt.toList.map fun c => ⟨.Assert c, source, md⟩)
-    pure ([⟨.LocalVariable name ty init', source, md⟩] ++ check)
+      | none =>
+        let calls := params.filterMap fun p => constraintCallFor ptMap p.type.val p.name md (src := source)
+        (none, calls.map fun c => ⟨.Assume c, source, md⟩)
+      | some _ =>
+        let calls := params.filterMap fun p => constraintCallFor ptMap p.type.val p.name md (src := source)
+        (init, calls.map fun c => ⟨.Assert c, source, md⟩)
+    pure ([⟨.LocalVariable params init', source, md⟩] ++ check)
 
   | .Assign [target] _ => match target.val with
     | .Identifier name => do
@@ -209,13 +212,13 @@ private def mkWitnessProc (ptMap : ConstrainedTypeMap) (ct : ConstrainedType) :
   let md := ct.witness.md
   let witnessId : Identifier := mkId "$witness"
   let witnessInit : StmtExprMd :=
-    ⟨.LocalVariable witnessId (resolveType ptMap ct.base) (some ct.witness), src, md⟩
+    ⟨.LocalVariable [{ name := witnessId, type := resolveType ptMap ct.base }] (some ct.witness), src, md⟩
   let assert : StmtExprMd :=
     ⟨.Assert (constraintCallFor ptMap (.UserDefined ct.name) witnessId md (src := src)).get!, src, md⟩
   { name := mkId s!"$witness_{ct.name.text}"
     inputs := []
     outputs := []
-    body := .Transparent ⟨.Block [witnessInit, assert] none, src, md⟩
+    body := .Opaque [] (some ⟨.Block [witnessInit, assert] none, src, md⟩) []
     preconditions := []
     isFunctional := false
     decreases := none }

Strata/Languages/Laurel/ContractPass.lean

@@ -0,0 +1,328 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+module
+
+public import Strata.Languages.Laurel.MapStmtExpr
+
+/-!
+## Contract Pass (Laurel → Laurel)
+
+Removes pre- and postconditions from all procedures and replaces them with
+explicit precondition/postcondition helper procedures, assumptions, and
+assertions.
+
+For each procedure with contracts:
+- Generate a precondition procedure (`foo$pre`) returning the conjunction of preconditions.
+- Generate a postcondition procedure (`foo$post`) that takes only the *input*
+  parameters, internally calls the original procedure to obtain the outputs,
+  and returns the conjunction of postconditions.
+- Insert `assume foo$pre(inputs)` at the start of the body.
+- Insert `assert foo$post(inputs)` at the end of the body.
+
+For each call to a contracted procedure:
+- Insert `assert foo$pre(args)` before the call (precondition check).
+- Insert `assume foo$post(args)` after the call (postcondition assumption).
+
+The postcondition procedure calls the original procedure internally so that
+the `assume` at call sites only references pre-call arguments. This avoids
+a soundness issue where mutable variables (e.g. `$heap`) are overwritten by
+the call's result destructuring before the `assume` is evaluated.
+-/
+
+namespace Strata.Laurel
+
+public section
+
+private def emptyMd : MetaData := .empty
+
+private def mkMd (e : StmtExpr) : StmtExprMd := { val := e, source := none }
+
+/-- Create a `StmtExprMd` with a property summary in its metadata. -/
+private def mkMdWithSummary (e : StmtExpr) (summary : String) : StmtExprMd :=
+  ⟨e, none, emptyMd.withPropertySummary summary⟩
+
+/-- Build a conjunction of expressions. Returns `LiteralBool true` for an empty list. -/
+private def conjoin (exprs : List StmtExprMd) : StmtExprMd :=
+  match exprs with
+  | [] => mkMd (.LiteralBool true)
+  | [e] => e
+  | e :: rest => rest.foldl (fun acc x =>
+      mkMd (.PrimitiveOp .And [acc, x])) e
+
+/-- Name for the precondition helper procedure. -/
+def preCondProcName (procName : String) : String := s!"{procName}$pre"
+
+/-- Name for the postcondition helper procedure. -/
+def postCondProcName (procName : String) : String := s!"{procName}$post"
+
+/-- Get postconditions from a procedure body. -/
+private def getPostconditions (body : Body) : List StmtExprMd :=
+  match body with
+  | .Opaque postconds _ _ => postconds
+  | .Abstract postconds => postconds
+  | _ => []
+
+/-- Build a call expression. -/
+private def mkCall (callee : String) (args : List StmtExprMd) : StmtExprMd :=
+  mkMd (.StaticCall (mkId callee) args)
+
+/-- Convert parameters to identifier expressions. -/
+private def paramsToArgs (params : List Parameter) : List StmtExprMd :=
+  params.map fun p => mkMd (.Identifier p.name)
+
+/-- Build a helper function that returns the conjunction of the given conditions. -/
+private def mkConditionProc (name : String) (params : List Parameter)
+    (conditions : List StmtExprMd) : Procedure :=
+  -- Use "$result" as the output name to avoid clashing with user-defined
+  -- parameter names (user names cannot contain '$').
+  { name := mkId name
+    inputs := params
+    outputs := [⟨mkId "$result", { val := .TBool, source := none }⟩] -- TODO, enable anonymous output parameters
+    preconditions := []
+    decreases := none
+    isFunctional := true
+    body := .Transparent (conjoin conditions) }
+
+/-- Build a postcondition procedure that takes only the *input* parameters
+    and internally calls the original procedure to obtain the outputs.
+
+    For a procedure `foo(a, b) returns (x, y)` with postcondition `P(a, b, x, y)`,
+    generates:
+    ```
+    procedure foo$post(a, b) returns ($result : bool) {
+      var x, y : Tx := foo(a, b);
+      P(a, b, x, y)
+    }
+    ```
+
+    This ensures the `assume` at call sites only references pre-call arguments,
+    avoiding a soundness issue where mutable variables (e.g. `$heap`) are
+    overwritten by the call's result destructuring before the `assume` is
+    evaluated. -/
+private def mkPostConditionProc (name : String) (originalProcName : String)
+    (inputParams : List Parameter) (outputParams : List Parameter)
+    (conditions : List StmtExprMd) : Procedure :=
+  let inputArgs := paramsToArgs inputParams
+  let callExpr := mkMd (.StaticCall (mkId originalProcName) inputArgs)
+  let localVarStmt := mkMd (.LocalVariable outputParams (some callExpr))
+  -- Body: single initialized local variable, then postcondition conjunction
+  let bodyStmts := [localVarStmt, conjoin conditions]
+  let body := mkMd (.Block bodyStmts none)
+  { name := mkId name
+    inputs := inputParams
+    outputs := [⟨mkId "$result", { val := .TBool, source := none }⟩]
+    preconditions := []
+    decreases := none
+    isFunctional := false
+    body := .Transparent body }
+
+/-- Extract a combined summary from a list of contract clauses. -/
+private def combinedSummary (clauses : List StmtExprMd) : Option String :=
+  let summaries := clauses.filterMap fun c => c.md.getPropertySummary
+  match summaries with
+  | [] => none
+  | [s] => some s
+  | ss => some (String.intercalate ", " ss)
+
+/-- Information about a procedure's contracts. -/
+private structure ContractInfo where
+  hasPreCondition : Bool
+  hasPostCondition : Bool
+  preName : String
+  postName : String
+  preSummary : Option String
+  postSummary : Option String
+  /-- The original procedure's input parameters (needed for postcondition generation). -/
+  inputParams : List Parameter
+  /-- The original procedure's output parameters (needed for postcondition generation). -/
+  outputParams : List Parameter
+
+/-- Collect contract info for all procedures with contracts. -/
+private def collectContractInfo (procs : List Procedure) : Std.HashMap String ContractInfo :=
+  procs.foldl (fun m proc =>
+    let postconds := getPostconditions proc.body
+    let hasPre := !proc.preconditions.isEmpty
+    let hasPost := !postconds.isEmpty
+    if hasPre || hasPost then
+      m.insert proc.name.text {
+        hasPreCondition := hasPre
+        hasPostCondition := hasPost
+        preName := preCondProcName proc.name.text
+        postName := postCondProcName proc.name.text
+        preSummary := combinedSummary proc.preconditions
+        postSummary := combinedSummary postconds
+        inputParams := proc.inputs
+        outputParams := proc.outputs
+      }
+    else m) {}
+
+/-- Transform a procedure body to add assume/assert for its own contracts. -/
+private def transformProcBody (proc : Procedure) (info : ContractInfo) : Body :=
+  let inputArgs := paramsToArgs proc.inputs
+  let postconds := getPostconditions proc.body
+  -- Use the source location from the first precondition for the assume node
+  let preAssume : List StmtExprMd :=
+    if info.hasPreCondition then
+      let (preSrc, preMd) := match proc.preconditions.head? with
+        | some pc => (pc.source, pc.md)
+        | none => (none, emptyMd)
+      [⟨.Assume (mkCall info.preName inputArgs), preSrc, preMd⟩]
+    else []
+  let postAssert : List StmtExprMd :=
+    if info.hasPostCondition then
+      -- Use the source location and metadata from the first postcondition so
+      -- the diagnostic carries the source location of the `ensures` clause.
+      let (baseSrc, baseMd) := match postconds.head? with
+        | some pc => (pc.source, pc.md)
+        | none => (none, emptyMd)
+      let summary := info.postSummary.getD "postcondition"
+      -- Directly assert the postcondition conjunction rather than calling $post.
+      -- The $post procedure re-invokes the original (opaque) procedure to obtain
+      -- outputs, which is correct at *call sites* but wrong inside the body:
+      -- here the output variables (e.g. $heap) are already in scope with their
+      -- actual values, so we assert the postcondition directly.
+      [⟨.Assert (conjoin postconds),
+        baseSrc, baseMd.withPropertySummary summary⟩]
+    else []
+  match proc.body with
+  | .Transparent body =>
+    .Transparent ⟨.Block (preAssume ++ [body] ++ postAssert) none, body.source, emptyMd ⟩
+  | .Opaque _ (some impl) _ =>
+    .Opaque [] (some ⟨.Block (preAssume ++ [impl] ++ postAssert) none, impl.source, emptyMd⟩)  []
+  | .Opaque _ none _ | .Abstract _ =>
+    .Opaque [] (some ⟨ .Block [] none, none, emptyMd⟩)  []
+  | b => b
+
+/-- Rewrite a single statement that may be a call to a contracted procedure.
+    Returns a list of statements (the original plus any inserted assert/assume).
+    Uses the call site's metadata for generated assert/assume nodes.
+    The postcondition assume passes only the call arguments (not the results),
+    since the $post procedure internally calls the original to obtain outputs. -/
+private def rewriteStmt (contractInfoMap : Std.HashMap String ContractInfo)
+    (e : StmtExprMd) : List StmtExprMd :=
+  let md := e.md
+  let src := e.source
+  let mkWithMd (se : StmtExpr) : StmtExprMd := ⟨se, src, md⟩
+  let mkWithMdSummary (se : StmtExpr) (summary : String) : StmtExprMd :=
+    ⟨se, src, md.withPropertySummary summary⟩
+  match e.val with
+  | .Assign _targets (.mk (.StaticCall callee args) ..) =>
+    match contractInfoMap.get? callee.text with
+    | some info =>
+      let preAssert := if info.hasPreCondition
+        then [mkWithMdSummary (.Assert (mkCall info.preName args)) (info.preSummary.getD "precondition")] else []
+      -- Assume $post *before* the assignment so that args still reference
+      -- pre-call values (e.g. $heap before it is overwritten by the call result).
+      -- The $post procedure internally calls the original to obtain outputs.
+      let postAssume := if info.hasPostCondition
+        then [mkWithMd (.Assume (mkCall info.postName args))] else []
+      preAssert ++ postAssume ++ [e]
+    | none => [e]
+  | .LocalVariable _params (some (.mk (.StaticCall callee args) ..)) =>
+    match contractInfoMap.get? callee.text with
+    | some info =>
+      let preAssert := if info.hasPreCondition
+        then [mkWithMdSummary (.Assert (mkCall info.preName args)) (info.preSummary.getD "precondition")] else []
+      -- Assume $post *before* the local variable binding so that args still
+      -- reference pre-call values.  The $post procedure internally calls the
+      -- original to obtain outputs.
+      let postAssume := if info.hasPostCondition
+        then [mkWithMd (.Assume (mkCall info.postName args))] else []
+      preAssert ++ postAssume ++ [e]
+    | none => [e]
+  | .StaticCall callee args =>
+    match contractInfoMap.get? callee.text with
+    | some info =>
+      let preAssert := if info.hasPreCondition
+        then [mkWithMdSummary (.Assert (mkCall info.preName args)) (info.preSummary.getD "precondition")] else []
+      preAssert ++ [e]
+    | none => [e]
+  | _ => [e]
+
+/-- Rewrite call sites in a statement/expression tree. Processes Block children
+    at the statement level to avoid interfering with expression-level calls.
+    For each statement-level call to a contracted procedure, inserts
+    `assert pre(args)` before and `assume post(args)` after. -/
+private def rewriteCallSites (contractInfoMap : Std.HashMap String ContractInfo)
+    (expr : StmtExprMd) : StmtExprMd :=
+  let result := mapStmtExpr (fun e =>
+    match e.val with
+    | .Block stmts label =>
+      let stmts' := stmts.flatMap (rewriteStmt contractInfoMap)
+      if stmts'.length == stmts.length then e
+      else ⟨.Block stmts' label, e.source, e.md⟩
+    | _ => e) expr
+  -- Handle top-level non-Block statements (e.g., bare Assign or StaticCall)
+  let expanded := rewriteStmt contractInfoMap result
+  match expanded with
+  | [single] => single
+  | many => mkMd (.Block many none)
+
+/-- Rewrite call sites in all bodies of a procedure. -/
+private def rewriteCallSitesInProc (contractInfoMap : Std.HashMap String ContractInfo)
+    (proc : Procedure) : Procedure :=
+  let rw := rewriteCallSites contractInfoMap
+  match proc.body with
+  | .Transparent body =>
+    { proc with body := .Transparent (rw body) }
+  | .Opaque posts impl mods =>
+    let body := Body.Opaque (posts.map rw) (impl.map rw) (mods.map rw)
+    { proc with body := body }
+  | _ => proc
+
+/-- Build an axiom expression from `invokeOn` trigger and ensures clauses.
+    Produces `∀ p1, ∀ p2, ..., ∀ pn :: { trigger } (ensures1 && ensures2 && ...)`. -/
+private def mkInvokeOnAxiom (params : List Parameter) (trigger : StmtExprMd)
+    (postconds : List StmtExprMd) : StmtExprMd :=
+  let body := conjoin postconds
+  -- Wrap in nested Forall from last param (innermost) to first (outermost).
+  -- The trigger is placed on the innermost quantifier.
+  params.foldr (init := (body, true)) (fun p (acc, isInnermost) =>
+    let trig := if isInnermost then some trigger else none
+    (mkMd (.Forall p trig acc), false)) |>.1
+
+/-- Run the contract pass on a Laurel program.
+    All procedures with contracts are transformed. -/
+def contractPass (program : Program) : Program :=
+  let contractInfoMap := collectContractInfo program.staticProcedures
+
+  -- Generate helper procedures for all procedures with contracts
+  let helperProcs := program.staticProcedures.flatMap fun proc =>
+    let postconds := getPostconditions proc.body
+    let preProc :=
+      if proc.preconditions.isEmpty then []
+      else [mkConditionProc (preCondProcName proc.name.text) proc.inputs proc.preconditions]
+    let postProc :=
+      if postconds.isEmpty then []
+      else [mkPostConditionProc (postCondProcName proc.name.text) proc.name.text
+              proc.inputs proc.outputs postconds]
+    preProc ++ postProc
+
+  -- Transform procedures: strip contracts, add assume/assert, rewrite call sites
+  let transformedProcs := program.staticProcedures.map fun proc =>
+    -- Build axioms from invokeOn + ensures BEFORE transforming the body
+    -- (transformProcBody strips postconditions from the body)
+    let proc := match proc.invokeOn with
+      | some trigger =>
+        let postconds := getPostconditions proc.body
+        if postconds.isEmpty then { proc with invokeOn := none }
+        else { proc with
+          axioms := [mkInvokeOnAxiom proc.inputs trigger postconds]
+          invokeOn := none }
+      | none => proc
+    let proc := match contractInfoMap.get? proc.name.text with
+      | some info =>
+        { proc with
+          preconditions := []
+          body := transformProcBody proc info }
+      | none => proc
+    -- Rewrite call sites in the procedure body
+    rewriteCallSitesInProc contractInfoMap proc
+
+  { program with staticProcedures := helperProcs ++ transformedProcs }
+
+end -- public section
+end Strata.Laurel