Merge functions and procedures in Laurel

Strata/Languages/Core/Factory.lean

@@ -42,6 +42,7 @@ def KnownLTys : LTys :=
    t[real],
    t[Triggers],
    t[TriggerGroup],
+   t[errorVoid],
    -- Note: t[bv<n>] elaborates to (.forAll [] .tcons "bitvec" <n>).
    -- We can simply add the following here.
    t[∀n. bitvec n],

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/Core/SMTEncoder.lean

@@ -236,7 +236,12 @@ def LMonoTy.toSMTType (E: Env) (ty : LMonoTy) (ctx : SMT.Context) (useArrayTheor
   | .ftvar tyv => match ctx.tySubst.find? tyv with
                     | .some termTy =>
                       .ok (termTy, ctx)
-                    | _ => .error f!"Unimplemented encoding for type var {tyv}"
+                    | _ =>
+                      -- Unresolved type variables can arise from polymorphic
+                      -- precondition assertions (PrecondElim) where the element
+                      -- type is unconstrained. Default to `int` since the
+                      -- assertion's semantics are independent of the type.
+                      .ok (.int, ctx)
 
 def LMonoTys.toSMTType (E: Env) (args : LMonoTys) (ctx : SMT.Context) (useArrayTheory : Bool := false) :
     Except Format ((List TermType) × SMT.Context) := do

Strata/Languages/Laurel/CoreDefinitionsForLaurel.lean

@@ -27,16 +27,21 @@ program Laurel;
 
 datatype LaurelResolutionErrorPlaceholder {}
 datatype Float64IsNotSupportedYet {}
+datatype LaurelUnit { MkLaurelUnit() }
 
 // The types for these Map functions are incorrect.
 // We'll fix them when Laurel supports polymorphism
-function select(map: int, key: int) : int
+// And then we can remove the datatype Box as well
+// And remove the hacky filter in HeapParameterization
+datatype Box { MkBox() }
+
+function select(map: int, key: int) : Box
   external;
 
-function update(map: int, key: int, value: int) : int
+function update(map: int, key: int, value: int) : Box
   external;
 
-function const(value: int) : int
+function const(value: int) : Box
   external;
 
 #end

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
@@ -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 axioms 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).
-  -- Stable partition: procedures with invokeOn come first, preserving relative
+public def computeSccDecls (program : UnorderedCoreWithLaurelTypes) : List (List Procedure × Bool) :=
+  -- Stable partition: procedures with axioms come first, preserving relative
   -- order within each group. Tarjan then places them earlier in the topological output.
-  let (withInvokeOn, withoutInvokeOn) :=
-    (program.staticProcedures.filter (fun p => !p.body.isExternal))
-    |>.partition (fun p => p.invokeOn.isSome)
-  let nonExternal : List Procedure := withInvokeOn ++ withoutInvokeOn
+  let allProcs := program.functions ++ program.coreProcedures
+  let (withAxioms, withoutAxioms) :=
+    allProcs.partition (fun p => !p.axioms.isEmpty)
+  let orderedProcs : List Procedure := withAxioms ++ withoutAxioms
 
-  -- 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.
@@ -145,13 +141,14 @@ public def computeSccDecls (program : Program) : List (List Procedure × Bool) :
       | _ => []
     let contractExprs : List StmtExprMd :=
       proc.preconditions.map (·.condition) ++
-      proc.invokeOn.toList
+      proc.invokeOn.toList ++
+      proc.axioms
     (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 +164,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 +173,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 `orderFunctionsAndProofs` 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 orderFunctionsAndProofs (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/DatatypeTesters.lean

@@ -0,0 +1,54 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+module
+
+public import Strata.Languages.Laurel.Laurel
+
+/-!
+## Datatype Tester Generation
+
+For each constructor of a datatype, generate an external testing function.
+The tester function takes a single argument of the datatype's type and returns
+`bool`. Its name is determined by `DatatypeDefinition.testerName`.
+
+This pass runs at the start of the Laurel pipeline, before resolution, so that
+the tester functions are available as normal static procedures.
+-/
+
+namespace Strata.Laurel
+
+public section
+
+/-- Generate an external tester function for a single constructor of a datatype. -/
+private def mkTesterFunction (dt : DatatypeDefinition) (ctor : DatatypeConstructor) : Procedure :=
+  let testerName := dt.testerName ctor
+  let inputParam : Parameter := {
+    name := mkId "value"
+    type := { val := .UserDefined dt.name, source := none }
+  }
+  let outputParam : Parameter := {
+    name := mkId "$result"
+    type := { val := .TBool, source := none }
+  }
+  { name := mkId testerName
+    inputs := [inputParam]
+    outputs := [outputParam]
+    preconditions := []
+    decreases := none
+    isFunctional := true
+    body := .External }
+
+/-- Generate external tester functions for all constructors of all datatypes in the program. -/
+def generateDatatypeTesters (program : Program) : Program :=
+  let testers := program.types.flatMap fun td =>
+    match td with
+    | .Datatype dt => dt.constructors.map (mkTesterFunction dt)
+    | _ => []
+  { program with staticProcedures := testers ++ program.staticProcedures }
+
+end -- public section
+
+end Strata.Laurel

Strata/Languages/Laurel/DesugarShortCircuit.lean

@@ -23,32 +23,33 @@ namespace Strata.Laurel
 
 public section
 
-private def bare (v : StmtExpr) : StmtExprMd := ⟨v, none⟩
 
 /-- Local rewrite of a single short-circuit node. Recursion is handled by `mapStmtExpr`. -/
-private def desugarShortCircuitNode (model : SemanticModel) (expr : StmtExprMd) : StmtExprMd :=
+private def desugarShortCircuitNode (imperativeCallees : List String) (expr : StmtExprMd) : StmtExprMd :=
   let source := expr.source
+  let wrap (v : StmtExpr) : StmtExprMd := ⟨v, source⟩
   match expr.val with
   | .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
     -- `containsAssignmentOrImperativeCall` recurses into IfThenElse.
     | .AndThen, [a, b] | .Implies, [a, b] =>
-      if containsAssignmentOrImperativeCall model b then
+      if containsAssignmentOrImperativeCall imperativeCallees b then
         let elseVal := match op with | .AndThen => false | _ => true
-        ⟨.IfThenElse a b (some (bare (.LiteralBool elseVal))), source⟩
+        ⟨.IfThenElse a b (some (wrap (.LiteralBool elseVal))), source⟩
       else expr
     | .OrElse, [a, b] =>
-      if containsAssignmentOrImperativeCall model b then
-        ⟨.IfThenElse a (bare (.LiteralBool true)) (some b), source⟩
+      if containsAssignmentOrImperativeCall imperativeCallees b then
+        ⟨.IfThenElse a (wrap (.LiteralBool true)) (some b), source⟩
       else expr
     | _, _ => expr
   | _ => expr
 
 /-- Desugar short-circuit operators in a program. -/
-def desugarShortCircuit (model : SemanticModel) (program : Program) : Program :=
-  mapProgram (mapStmtExpr (desugarShortCircuitNode model)) program
+def desugarShortCircuit (program : Program) : Program :=
+  let imperativeCallees := program.staticProcedures.map (fun p => p.name.text)
+  mapProgram (mapStmtExpr (desugarShortCircuitNode imperativeCallees)) program
 
 end -- public section
 end Strata.Laurel