Support transparent procedures

Examples/expected/HeapReasoning.core.expected

@@ -2,7 +2,6 @@ Successfully parsed.
 HeapReasoning.core.st(98, 2) [modifiesFrameRef1]: ✅ pass
 HeapReasoning.core.st(103, 2) [modifiesFrameRef1]: ✅ pass
 HeapReasoning.core.st(108, 2) [modifiesFrameRef1]: ✅ pass
- [Container_ctor_ensures_4]: ✅ pass
 HeapReasoning.core.st(86, 2) [Container_ctor_ensures_7]: ✅ pass
 HeapReasoning.core.st(87, 2) [Container_ctor_ensures_8]: ✅ pass
 HeapReasoning.core.st(88, 2) [Container_ctor_ensures_9]: ✅ pass
@@ -12,7 +11,6 @@ HeapReasoning.core.st(169, 2) [modifiesFrameRef2]: ✅ pass
 HeapReasoning.core.st(172, 2) [modifiesFrameRef1Next]: ✅ pass
 HeapReasoning.core.st(177, 2) [modifiesFrameRef2Next]: ✅ pass
 HeapReasoning.core.st(132, 2) [UpdateContainers_ensures_5]: ✅ pass
- [UpdateContainers_ensures_6]: ✅ pass
 HeapReasoning.core.st(150, 2) [UpdateContainers_ensures_14]: ✅ pass
 HeapReasoning.core.st(151, 2) [UpdateContainers_ensures_15]: ✅ pass
 HeapReasoning.core.st(152, 2) [UpdateContainers_ensures_16]: ✅ pass
@@ -51,5 +49,4 @@ HeapReasoning.core.st(238, 2) [c2Pineapple0]: ✅ pass
 HeapReasoning.core.st(240, 2) [c1NextEqC2]: ✅ pass
 HeapReasoning.core.st(241, 2) [c2NextEqC1]: ✅ pass
 HeapReasoning.core.st(195, 2) [Main_ensures_1]: ✅ pass
- [Main_ensures_2]: ✅ pass
-All 53 goals passed.
+All 50 goals passed.

Strata/DL/Imperative/SMTUtils.lean

@@ -104,7 +104,9 @@ def getSMTId {Ident Ty} [ToFormat Ident]
   | (var, some ty) => do
     let (var', ty') ← typedVarToSMTFn var ty
     let key : Strata.SMT.UF := { id := var', args := [], out := ty' }
-    .ok (E.ufs[key]!)
+    match E.ufs[key]? with
+    | some id => .ok id
+    | none => .error f!"Variable {var} (SMT name: {var'}) not found in encoder state"
 
 def runSolver (solver : String) (args : Array String) : IO IO.Process.Output := do
   let output ← IO.Process.output {

Strata/DL/Lambda/TypeFactory.lean

@@ -509,10 +509,26 @@ def destructorConcreteEval {T: LExprParams} [BEq T.Identifier] (d: LDatatype T.I
         then a[idx]? else none)
     | _ => none
 
-def destructorFuncName {IDMeta} (d: LDatatype IDMeta) (name: Identifier IDMeta) := d.name ++ ".." ++ name.name
+def destructorSeparator := ".."
+
+def destructorFuncName {IDMeta} (d: LDatatype IDMeta) (name: Identifier IDMeta) := d.name ++ destructorSeparator ++ name.name
 
 def unsafeDestructorSuffix := "!"
 
+/-- Check whether a name is a destructor or tester name (contains the `..` separator). -/
+def isSelectorName (name : String) : Bool :=
+  (name.splitOn destructorSeparator).length == 2
+
+/-- Check whether a name is a tester name (e.g. `IntList..isCons`). -/
+def isTesterName (name : String) : Bool :=
+  match name.splitOn destructorSeparator with
+  | [_, suffix] => suffix.startsWith "is"
+  | _ => false
+
+/-- Check whether a name is a destructor name (e.g. `IntList..head` or `IntList..head!`). -/
+def isDestructorName (name : String) : Bool :=
+  isSelectorName name && !isTesterName name
+
 def unsafeDestructorFuncName {IDMeta} (d: LDatatype IDMeta)
   (name: Identifier IDMeta) :=
   destructorFuncName d name ++ unsafeDestructorSuffix

Strata/Languages/Core/ProcedureEval.lean

@@ -93,13 +93,13 @@ def eval (E : Env) (p : Procedure) : Env × Statistics :=
                 match check.attr with
                 | .Free =>
                     -- NOTE: A free postcondition is not checked.
-                    -- We simply change a free-postcondition to "true", but
+                    -- We simply change a free-postcondition to "assume true", but
                     -- keep a record in the metadata field.
                     -- TODO: Perhaps introduce an "opaque" expression construct
                     -- that hides the expression from the evaluator, allowing us
                     -- to retain the postcondition body instead of replacing it
                     -- with "true".
-                  (.assert label (.true ())
+                  (.assume label (.true ())
                                  ((Imperative.MetaData.pushElem
                                   #[]
                                   (.label label)

Strata/Languages/Laurel/CoreGroupingAndOrdering.lean

@@ -5,18 +5,17 @@
 -/
 
 module
-public import Strata.Languages.Laurel.Laurel
+public import Strata.Languages.Laurel.TransparencyPass
 import Strata.DL.Lambda.LExpr
 import Strata.DDM.Util.Graph.Tarjan
+import Strata.Languages.Laurel.Grammar.AbstractToConcreteTreeTranslator
 
 /-!
 ## Grouping and Ordering for Core Translation
 
 Utilities for computing the grouping and topological ordering of Laurel
 declarations before they are emitted as Strata Core declarations.
 
-- `groupDatatypesByScc` — groups mutually recursive datatypes into SCC groups
-  using Tarjan's SCC algorithm.
 - `computeSccDecls` — builds the procedure call graph, runs Tarjan's SCC
   algorithm, and returns each SCC as a list of procedures paired with a flag
   indicating whether the SCC is recursive. The result is in reverse topological
@@ -54,7 +53,7 @@ def collectStaticCallNames (expr : StmtExprMd) : List String :=
   match val with
   | .StaticCall callee args =>
       callee.text :: args.flatMap (fun a => collectStaticCallNames a)
-  | .PrimitiveOp _ args => args.flatMap (fun a => collectStaticCallNames a)
+  | .PrimitiveOp _ args _ => args.flatMap (fun a => collectStaticCallNames a)
   | .IfThenElse cond t e =>
       collectStaticCallNames cond ++
       collectStaticCallNames t ++
@@ -90,7 +89,7 @@ def collectStaticCallNames (expr : StmtExprMd) : List String :=
   | .InstanceCall t _ args =>
       collectStaticCallNames t ++ args.flatMap (fun a => collectStaticCallNames a)
   | .Old v | .Fresh v | .Assume v => collectStaticCallNames v
-  | .Assert ⟨cond, _summary⟩ => collectStaticCallNames cond
+  | .Assert ⟨cond, _summary, _⟩ => collectStaticCallNames cond
   | .ProveBy v p => collectStaticCallNames v ++ collectStaticCallNames p
   | .ReferenceEquals l r => collectStaticCallNames l ++ collectStaticCallNames r
   | .AsType t _ | .IsType t _ => collectStaticCallNames t
@@ -113,27 +112,24 @@ Build the procedure call graph, run Tarjan's SCC algorithm, and return each SCC
 as a list of procedures paired with a flag indicating whether the SCC is recursive.
 Results are in reverse topological order: dependencies before dependents.
 
-Procedures with an `invokeOn` trigger are placed as early as possible — before
-unrelated procedures without one — by stably partitioning them first before building
+Procedures with `invokeOn` are placed as early as possible — before
+unrelated procedures without them — by stably partitioning them first before building
 the graph. Tarjan then naturally assigns them lower indices, causing them to appear
 earlier in the output.
-
-External procedures are excluded.
 -/
-public def computeSccDecls (program : Program) : List (List Procedure × Bool) :=
-  -- External procedures are completely ignored (not translated to Core).
+public def computeSccDecls (program : UnorderedCoreWithLaurelTypes) : List (List Procedure × Bool) :=
   -- Stable partition: procedures with invokeOn come first, preserving relative
   -- order within each group. Tarjan then places them earlier in the topological output.
+  let allProcs := program.functions ++ program.coreProcedures
   let (withInvokeOn, withoutInvokeOn) :=
-    (program.staticProcedures.filter (fun p => !p.body.isExternal))
-    |>.partition (fun p => p.invokeOn.isSome)
-  let nonExternal : List Procedure := withInvokeOn ++ withoutInvokeOn
+    allProcs.partition (fun p => p.invokeOn.isSome)
+  let orderedProcs : List Procedure := withInvokeOn ++ withoutInvokeOn
 
-  -- Build a call-graph over all non-external procedures.
+  -- Build a call-graph over all procedures.
   -- An edge proc → callee means proc's body/contracts contain a StaticCall to callee.
-  let nonExternalArr : Array Procedure := nonExternal.toArray
+  let procsArr : Array Procedure := orderedProcs.toArray
   let nameToIdx : Std.HashMap String Nat :=
-    nonExternalArr.foldl (fun (acc : Std.HashMap String Nat × Nat) proc =>
+    procsArr.foldl (fun (acc : Std.HashMap String Nat × Nat) proc =>
       (acc.1.insert proc.name.text acc.2, acc.2 + 1)) ({}, 0) |>.1
 
   -- Collect all callee names from a procedure's body and contracts.
@@ -149,9 +145,9 @@ public def computeSccDecls (program : Program) : List (List Procedure × Bool) :
     (bodyExprs ++ contractExprs).flatMap collectStaticCallNames
 
   -- Build the OutGraph for Tarjan.
-  let n := nonExternalArr.size
+  let n := procsArr.size
   let graph : Strata.OutGraph n :=
-    nonExternalArr.foldl (fun (acc : Strata.OutGraph n × Nat) proc =>
+    procsArr.foldl (fun (acc : Strata.OutGraph n × Nat) proc =>
       let callerIdx := acc.2
       let g := acc.1
       let callees := procCallees proc
@@ -167,7 +163,7 @@ public def computeSccDecls (program : Program) : List (List Procedure × Bool) :
 
   sccs.toList.filterMap fun scc =>
     let procs := scc.toList.filterMap fun idx =>
-      nonExternalArr[idx.val]?
+      procsArr[idx.val]?
     if procs.isEmpty then none else
     let isRecursive := procs.length > 1 ||
       (match scc.toList.head? with
@@ -176,60 +172,85 @@ public def computeSccDecls (program : Program) : List (List Procedure × Bool) :
     some (procs, isRecursive)
 
 /--
-A single declaration in an ordered Laurel program. Declarations are in
+A single declaration in a CoreWithLaurelTypes program. Declarations are in
 dependency order (dependencies before dependents).
 -/
 public inductive OrderedDecl where
-  /-- A group of functions (single non-recursive, or mutually recursive). -/
-  | procs (procs : List Procedure) (isRecursive : Bool)
+  /-- A group of functions (single non-recursive, or mutually recursive).
+      Invariant: `funcs.length > 1 → isRecursive = true`. -/
+  | funcs (funcs : List Procedure) (isRecursive : Bool)
+  /-- A single (non-functional) procedure. -/
+  | procedure (procedure : Procedure)
   /-- A group of (possibly mutually recursive) datatypes. -/
   | datatypes (dts : List DatatypeDefinition)
   /-- A named constant. -/
   | constant (c : Constant)
 
 /--
-A Laurel program whose declarations have been grouped and topologically ordered.
-Produced by `orderProgram` from a `Program`.
+A program whose declarations have been grouped and topologically ordered,
+using Laurel types. Produced by `orderFunctionsAndProcedures` from a
+`UnorderedCoreWithLaurelTypes`.
 -/
-public structure OrderedLaurel where
+public structure CoreWithLaurelTypes where
   decls : List OrderedDecl
 
-/--
-Group mutually recursive datatypes into SCC groups using Tarjan's SCC algorithm.
-Returns groups in topological order (dependencies before dependents).
--/
-public def groupDatatypesByScc (program : Program) : List (List DatatypeDefinition) :=
-  let laurelDatatypes := program.types.filterMap fun td => match td with
-    | .Datatype dt => some dt
-    | _ => none
-  let n := laurelDatatypes.length
-  if n == 0 then [] else
-  let nameToIdx : Std.HashMap String Nat :=
-    laurelDatatypes.foldlIdx (fun m i dt => m.insert dt.name.text i) {}
-  let edges : List (Nat × Nat) :=
-    laurelDatatypes.foldlIdx (fun acc i dt =>
-      (datatypeRefs dt).filterMap nameToIdx.get? |>.foldl (fun acc j => (j, i) :: acc) acc) []
-  let g := OutGraph.ofEdges! n edges
-  let dtsArr := laurelDatatypes.toArray
-  OutGraph.tarjan g |>.toList.filterMap fun comp =>
-    let members := comp.toList.filterMap fun idx => dtsArr[idx]?
-    if members.isEmpty then none else some members
+open Std (Format ToFormat)
 
-/--
-Group procedures into SCC groups and wrap them as `OrderedDecl.procs`.
--/
-public def groupProcsByScc (program : Program) : List OrderedDecl :=
-  (computeSccDecls program).map fun (procs, isRecursive) =>
-    OrderedDecl.procs procs isRecursive
+public section
+
+def formatOrderedDecl : OrderedDecl → Format
+  | .funcs funcs _ => Format.joinSep (funcs.map ToFormat.format) "\n\n"
+  | .procedure proc => ToFormat.format proc
+  | .datatypes dts => Format.joinSep (dts.map ToFormat.format) "\n\n"
+  | .constant c => ToFormat.format c
+
+instance : ToFormat OrderedDecl where
+  format := formatOrderedDecl
+
+def formatCoreWithLaurelTypes (p : CoreWithLaurelTypes) : Format :=
+  Format.joinSep (p.decls.map formatOrderedDecl) "\n\n"
+
+instance : ToFormat CoreWithLaurelTypes where
+  format := formatCoreWithLaurelTypes
+
+end -- public section
 
 /--
-Produce an `OrderedLaurel` from a `Program` by grouping and ordering
-procedures via SCC, collecting datatypes, and constants.
+Produce a `CoreWithLaurelTypes` from a `UnorderedCoreWithLaurelTypes` by
+computing a combined ordering of functions and proofs using the call graph,
+then collecting datatypes and constants.
+
+Functions are grouped into SCCs (for mutual recursion). Proofs are emitted
+as individual `procedure` decls. Both participate in the topological ordering
+so that axioms are available to functions that need them.
 -/
-public def orderProgram (program : Program) : OrderedLaurel :=
-  let datatypeDecls := (groupDatatypesByScc program).map OrderedDecl.datatypes
+public def orderFunctionsAndProcedures (program : UnorderedCoreWithLaurelTypes) : CoreWithLaurelTypes :=
+  let datatypeDecls := (groupDatatypesByScc' program).map OrderedDecl.datatypes
   let constantDecls := program.constants.map OrderedDecl.constant
-  let procDecls := groupProcsByScc program
-  { decls := datatypeDecls ++ constantDecls ++ procDecls }
+  let funcNames : Std.HashSet String :=
+    program.functions.foldl (fun s p => s.insert p.name.text) {}
+  let orderedDecls := (computeSccDecls program).flatMap fun (procs, isRecursive) =>
+    -- Split the SCC into functions and proofs
+    let (funcs, proofs) := procs.partition (fun p => funcNames.contains p.name.text)
+    let funcDecl := if funcs.isEmpty then [] else [OrderedDecl.funcs funcs isRecursive]
+    let proofDecls := proofs.map OrderedDecl.procedure
+    funcDecl ++ proofDecls
+  { decls := datatypeDecls ++ constantDecls ++ orderedDecls }
+where
+  /-- Group datatypes from a UnorderedCoreWithLaurelTypes by SCC. -/
+  groupDatatypesByScc' (program : UnorderedCoreWithLaurelTypes) : List (List DatatypeDefinition) :=
+    let laurelDatatypes := program.datatypes
+    let n := laurelDatatypes.length
+    if n == 0 then [] else
+    let nameToIdx : Std.HashMap String Nat :=
+      laurelDatatypes.foldlIdx (fun m i dt => m.insert dt.name.text i) {}
+    let edges : List (Nat × Nat) :=
+      laurelDatatypes.foldlIdx (fun acc i dt =>
+        (datatypeRefs dt).filterMap nameToIdx.get? |>.foldl (fun acc j => (j, i) :: acc) acc) []
+    let g := OutGraph.ofEdges! n edges
+    let dtsArr := laurelDatatypes.toArray
+    OutGraph.tarjan g |>.toList.filterMap fun comp =>
+      let members := comp.toList.filterMap fun idx => dtsArr[idx]?
+      if members.isEmpty then none else some members
 
 end Strata.Laurel

Strata/Languages/Laurel/DesugarShortCircuit.lean

@@ -5,8 +5,9 @@
 -/
 module
 
-public import Strata.Languages.Laurel.MapStmtExpr
-public import Strata.Languages.Laurel.LiftImperativeExpressions
+public import Strata.Languages.Laurel.Resolution
+import Strata.Languages.Laurel.LiftImperativeExpressions
+import Strata.Languages.Laurel.MapStmtExpr
 
 /-!
 # Desugar Short-Circuit Operators
@@ -29,7 +30,7 @@ private def bare (v : StmtExpr) : StmtExprMd := ⟨v, none⟩
 private def desugarShortCircuitNode (model : SemanticModel) (expr : StmtExprMd) : StmtExprMd :=
   let source := expr.source
   match expr.val with
-  | .PrimitiveOp op args =>
+  | .PrimitiveOp op args _ =>
     match op, args with
     -- With bottom-up traversal, `a` and `b` are already desugared (nested
     -- short-circuits converted to IfThenElse). The check still works because

Strata/Languages/Laurel/FilterPrelude.lean

@@ -107,7 +107,7 @@ private partial def collectExprNames (expr : StmtExprMd) : CollectM Unit := do
   | .Var (.Declare param) => collectHighTypeNames param.type
   | .PureFieldUpdate target _ newVal =>
     collectExprNames target; collectExprNames newVal
-  | .PrimitiveOp _ args => args.forM collectExprNames
+  | .PrimitiveOp _ args _ => args.forM collectExprNames
   | .AsType target ty => collectExprNames target; collectHighTypeNames ty
   | .IsType target ty => collectExprNames target; collectHighTypeNames ty
   | .Quantifier _ param trigger body =>

Strata/Languages/Laurel/Grammar/AbstractToConcreteTreeTranslator.lean

@@ -133,11 +133,11 @@ where
       let calleeArg := laurelOp "identifier" #[ident callee.text]
       let argsArr := args.map stmtExprToArg |>.toArray
       laurelOp "call" #[calleeArg, commaSep argsArr]
-    | .PrimitiveOp op [a] =>
+    | .PrimitiveOp op [a] _skipProof =>
       laurelOp (operationName op) #[stmtExprToArg a]
-    | .PrimitiveOp op [a, b] =>
+    | .PrimitiveOp op [a, b] _skipProof =>
       laurelOp (operationName op) #[stmtExprToArg a, stmtExprToArg b]
-    | .PrimitiveOp op args =>
+    | .PrimitiveOp op args _skipProof =>
       -- Fallback for unusual arities
       let argsArr := args.map stmtExprToArg |>.toArray
       laurelOp (operationName op) argsArr

Strata/Languages/Laurel/HeapParameterization.lean

@@ -76,7 +76,7 @@ def collectExpr (expr : StmtExpr) : StateM AnalysisResult Unit := do
         | .Local _ | .Declare _ => pure ()
       collectExprMd v
   | .PureFieldUpdate t _ v => collectExprMd t; collectExprMd v
-  | .PrimitiveOp _ args => for a in args do collectExprMd a
+  | .PrimitiveOp _ args _ => for a in args do collectExprMd a
   | .New _ => modify fun s => { s with writesHeapDirectly := true }
   | .ReferenceEquals l r => collectExprMd l; collectExprMd r
   | .AsType t _ => collectExprMd t
@@ -85,7 +85,7 @@ def collectExpr (expr : StmtExpr) : StateM AnalysisResult Unit := do
   | .Assigned n => collectExprMd n
   | .Old v => collectExprMd v
   | .Fresh v => collectExprMd v
-  | .Assert ⟨c, _⟩ => collectExprMd c
+  | .Assert ⟨c, _, _⟩ => collectExprMd c
   | .Assume c => collectExprMd c
   | .ProveBy v p => collectExprMd v; collectExprMd p
   | .ContractOf _ f => collectExprMd f
@@ -399,7 +399,7 @@ where
       return newAssign :: suffixes
 
     | .PureFieldUpdate t f v => return [⟨ .PureFieldUpdate (← recurseOne t) f (← recurseOne v), source ⟩]
-    | .PrimitiveOp op args =>
+    | .PrimitiveOp op args _ =>
       let args' ← args.mapM (recurseOne ·)
       -- For == and != on Composite types, compare refs instead
       match op, args with
@@ -434,8 +434,8 @@ where
     | .Assigned n => return [⟨ .Assigned (← recurseOne n), source ⟩]
     | .Old v => return [⟨ .Old (← recurseOne v), source ⟩]
     | .Fresh v => return [⟨ .Fresh (← recurseOne v), source ⟩]
-    | .Assert ⟨condExpr, summary⟩ =>
-        return [⟨ .Assert { condition := ← recurseOne condExpr, summary }, source ⟩]
+    | .Assert ⟨condExpr, summary, free⟩ =>
+        return [⟨ .Assert { condition := ← recurseOne condExpr, summary, free }, source ⟩]
     | .Assume c => return [⟨ .Assume (← recurseOne c), source ⟩]
     | .ProveBy v p => return [⟨ .ProveBy (← recurseOne v) (← recurseOne p), source ⟩]
     | .ContractOf ty f => return [⟨ .ContractOf ty (← recurseOne f), source ⟩]