Resolve Laurel in Python pipeline

Strata/DDM/Format.lean

@@ -30,9 +30,12 @@ Check if a character is valid for continuing a regular identifier.
 Includes @ and $ which are valid in SMT-LIB 2.6 simple symbols and
 used by the encoder for disambiguated names (e.g. x@1) and generated
 names (e.g. $__bv0).
+Note: `'` (apostrophe) is intentionally excluded. Although SMT-LIB 2.6 allows
+it in simple symbols, both cvc5 and Z3 reject it as an unquoted character.
+Names containing `'` (e.g. Lean's `v'`) will be pipe-quoted instead.
 -/
 private def isIdContinue (c : Char) : Bool :=
-  c.isAlphanum || c == '_' || c == '\'' || c == '.' || c == '?' || c == '!' || c == '@' || c == '$'
+  c.isAlphanum || c == '_' || c == '.' || c == '?' || c == '!' || c == '@' || c == '$'
 
 /--
 Check if a string needs pipe delimiters when formatted as an identifier.

Strata/Languages/Laurel/CoreGroupingAndOrdering.lean

@@ -0,0 +1,200 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+
+module
+public import Strata.Languages.Laurel.Laurel
+import Strata.DL.Lambda.LExpr
+import Strata.DDM.Util.Graph.Tarjan
+
+/-!
+## 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.
+
+- `groupDatatypes` — groups mutually recursive datatypes into a single `.data`
+  declaration 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
+  order (dependencies before dependents), which is the order required by Core.
+-/
+
+namespace Strata.Laurel
+
+open Lambda (LMonoTy LExpr)
+
+/-- Collect all `UserDefined` type names referenced in a `HighType`, including nested ones. -/
+def collectTypeRefs : HighTypeMd → List String
+  | ⟨.UserDefined name, _⟩ => [name.text]
+  | ⟨.TSet elem, _⟩ => collectTypeRefs elem
+  | ⟨.TMap k v, _⟩ => collectTypeRefs k ++ collectTypeRefs v
+  | ⟨.TTypedField vt, _⟩ => collectTypeRefs vt
+  | ⟨.Applied base args, _⟩ =>
+      collectTypeRefs base ++ args.flatMap collectTypeRefs
+  | ⟨.Pure base, _⟩ => collectTypeRefs base
+  | ⟨.Intersection ts, _⟩ => ts.flatMap collectTypeRefs
+  | ⟨.TCore name, _⟩ => [name]
+  | _ => []
+
+/-- Get all datatype names that a `DatatypeDefinition` references in its constructor args. -/
+def datatypeRefs (dt : DatatypeDefinition) : List String :=
+  dt.constructors.flatMap fun c => c.args.flatMap fun p => collectTypeRefs p.type
+
+/--
+Group `LDatatype Unit` values by strongly connected components of their direct type references.
+Datatypes in the same SCC (mutually recursive) share a single `.data` declaration.
+Non-recursive datatypes each get their own singleton `.data` declaration.
+The returned groups are in topological order: leaves (no dependencies) first, roots last.
+-/
+public def groupDatatypes (dts : List DatatypeDefinition)
+    (ldts : List (Lambda.LDatatype Unit)) : List (List (Lambda.LDatatype Unit)) :=
+  let n := dts.length
+  if n = 0 then [] else
+  let nameToIdx : Std.HashMap String Nat :=
+    dts.foldlIdx (fun m i dt => m.insert dt.name.text i) {}
+  -- dt[i] references dt[j] means i depends on j (j must be declared first).
+  -- tarjan guarantees: if there's a path A→B, B appears after A in the output.
+  -- So we add edge j→i (j has a path to i), ensuring i (the dependent) appears after j (the dependency).
+  let edges : List (Nat × Nat) :=
+    dts.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 ldtMap : Std.HashMap String (Lambda.LDatatype Unit) :=
+    ldts.foldl (fun m ldt => m.insert ldt.name ldt) {}
+  let dtsArr := dts.toArray
+  OutGraph.tarjan g |>.toList.filterMap fun comp =>
+    let members := comp.toList.filterMap fun idx =>
+      dtsArr[idx]? |>.bind fun dt => ldtMap.get? dt.name.text
+    if members.isEmpty then none else some members
+
+/--
+Collect all `StaticCall` callee names referenced anywhere in a `StmtExpr`.
+Used to build the call graph for SCC-based procedure ordering.
+-/
+def collectStaticCallNames (expr : StmtExprMd) : List String :=
+  match expr with
+  | WithMetadata.mk val _ =>
+  match val with
+  | .StaticCall callee args =>
+      callee.text :: args.flatMap (fun a => collectStaticCallNames a)
+  | .PrimitiveOp _ args => args.flatMap (fun a => collectStaticCallNames a)
+  | .IfThenElse cond t e =>
+      collectStaticCallNames cond ++
+      collectStaticCallNames t ++
+      match e with
+      | some eelse => collectStaticCallNames eelse
+      | none => []
+  | .Block stmts _ => stmts.flatMap (fun s => collectStaticCallNames s)
+  | .Assign targets v =>
+      targets.flatMap (fun t => collectStaticCallNames t) ++
+      collectStaticCallNames v
+  | .LocalVariable _ _ initOption =>
+      match initOption with
+      | some init => collectStaticCallNames init
+      | none => []
+  | .Return v =>
+      match v with
+      | some x => collectStaticCallNames x
+      | none => []
+  | .While cond invs dec body =>
+      collectStaticCallNames cond ++
+      invs.flatMap (fun i => collectStaticCallNames i) ++
+      (match dec with
+      | some d => collectStaticCallNames d
+      | none => []) ++
+      collectStaticCallNames body
+  | .Forall _ trig body =>
+      (match trig with
+      | some t => collectStaticCallNames t
+      | none => []) ++
+      collectStaticCallNames body
+  | .Exists _ trig body =>
+      (match trig with
+      | some t => collectStaticCallNames t
+      | none => []) ++
+      collectStaticCallNames body
+  | .FieldSelect t _ => collectStaticCallNames t
+  | .PureFieldUpdate t _ v => collectStaticCallNames t ++ collectStaticCallNames v
+  | .InstanceCall t _ args =>
+      collectStaticCallNames t ++ args.flatMap (fun a => collectStaticCallNames a)
+  | .Old v | .Fresh v | .Assert v | .Assume v => collectStaticCallNames v
+  | .ProveBy v p => collectStaticCallNames v ++ collectStaticCallNames p
+  | .ReferenceEquals l r => collectStaticCallNames l ++ collectStaticCallNames r
+  | .AsType t _ | .IsType t _ => collectStaticCallNames t
+  | .ContractOf _ f => collectStaticCallNames f
+  | .Assigned v => collectStaticCallNames v
+  | _ => []
+termination_by sizeOf expr
+
+/--
+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
+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
+  -- 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
+
+  -- Build a call-graph over all non-external procedures.
+  -- An edge proc → callee means proc's body/contracts contain a StaticCall to callee.
+  let nonExternalArr : Array Procedure := nonExternal.toArray
+  let nameToIdx : Std.HashMap String Nat :=
+    nonExternalArr.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.
+  let procCallees (proc : Procedure) : List String :=
+    let bodyExprs : List StmtExprMd := match proc.body with
+      | .Transparent b => [b]
+      | .Opaque postconds (some impl) _ => postconds ++ [impl]
+      | .Opaque postconds none _ => postconds
+      | _ => []
+    let contractExprs : List StmtExprMd :=
+      proc.preconditions ++
+      proc.invokeOn.toList
+    (bodyExprs ++ contractExprs).flatMap collectStaticCallNames
+
+  -- Build the OutGraph for Tarjan.
+  let n := nonExternalArr.size
+  let graph : Strata.OutGraph n :=
+    nonExternalArr.foldl (fun (acc : Strata.OutGraph n × Nat) proc =>
+      let callerIdx := acc.2
+      let g := acc.1
+      let callees := procCallees proc
+      let g' := callees.foldl (fun g callee =>
+        match nameToIdx.get? callee with
+        | some calleeIdx => g.addEdge! calleeIdx callerIdx
+        | none => g) g
+      (g', callerIdx + 1)) (Strata.OutGraph.empty n, 0) |>.1
+
+  -- Run Tarjan's SCC algorithm. Results are in reverse topological order
+  -- (a node appears after all nodes that have paths to it).
+  let sccs := Strata.OutGraph.tarjan graph
+
+  sccs.toList.filterMap fun scc =>
+    let procs := scc.toList.filterMap fun idx =>
+      nonExternalArr[idx.val]?
+    if procs.isEmpty then none else
+    let isRecursive := procs.length > 1 ||
+      (match scc.toList.head? with
+        | some node => (graph.nodesOut node).contains node
+        | none => false)
+    some (procs, isRecursive)
+
+end Strata.Laurel

Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean

@@ -77,7 +77,7 @@ def translateBool (arg : Arg) : TransM Bool := do
   | x => TransM.error s!"translateBool expects expression or operation, got {repr x}"
 
 instance : Inhabited Parameter where
-  default := { name := "" , type := ⟨.TVoid, #[]⟩ }
+  default := { name := "" , type := ⟨.Unknown, #[]⟩ }
 
 def mkHighTypeMd (t : HighType) (md : MetaData) : HighTypeMd := ⟨t, md⟩
 def mkStmtExprMd (e : StmtExpr) (md : MetaData) : StmtExprMd := ⟨e, md⟩
@@ -146,6 +146,7 @@ instance : Inhabited Procedure where
     determinism := .deterministic none
     decreases := none
     isFunctional := false
+    invokeOn := none
     body := .Transparent ⟨.LiteralBool true, #[]⟩
     md := .empty
   }
@@ -426,9 +427,9 @@ def parseProcedure (arg : Arg) : TransM Procedure := do
 
   match op.name, op.args with
   | q`Laurel.procedure, #[nameArg, paramArg, returnTypeArg, returnParamsArg,
-      requiresArg, ensuresArg, modifiesArg, bodyArg]
+      requiresArg, invokeOnArg, ensuresArg, modifiesArg, bodyArg]
   | q`Laurel.function, #[nameArg, paramArg, returnTypeArg, returnParamsArg,
-      requiresArg, ensuresArg, modifiesArg, bodyArg] =>
+      requiresArg, invokeOnArg, ensuresArg, modifiesArg, bodyArg] =>
     let name ← translateIdent nameArg
     let nameMd ← getArgMetaData nameArg
     let parameters ← translateParameters paramArg
@@ -451,6 +452,14 @@ def parseProcedure (arg : Arg) : TransM Procedure := do
       | _ => TransM.error s!"Expected optionalReturnType operation, got {repr returnTypeArg}"
     -- Parse preconditions (requires clauses - zero or more)
     let preconditions ← translateRequiresClauses requiresArg
+    -- Parse optional invokeOn clause
+    let invokeOn ← match invokeOnArg with
+      | .option _ (some (.op invokeOnOp)) => match invokeOnOp.name, invokeOnOp.args with
+        | q`Laurel.invokeOnClause, #[triggerExprArg] =>
+          translateStmtExpr triggerExprArg >>= (pure ∘ some)
+        | _, _ => TransM.error s!"Expected invokeOnClause operation, got {repr invokeOnOp.name}"
+      | .option _ none => pure none
+      | _ => pure none
     -- Parse postconditions (ensures clauses - zero or more)
     let postconditions ← translateEnsuresClauses ensuresArg
     -- Parse modifies clauses (zero or more)
@@ -483,12 +492,13 @@ def parseProcedure (arg : Arg) : TransM Procedure := do
       determinism := .deterministic none
       decreases := none
       isFunctional := op.name == q`Laurel.function
+      invokeOn := invokeOn
       body := procBody
       md := nameMd
     }
   | q`Laurel.procedure, args
   | q`Laurel.function, args =>
-    TransM.error s!"parseProcedure expects 8 arguments, got {args.size}"
+    TransM.error s!"parseProcedure expects 9 arguments, got {args.size}"
   | _, _ =>
     TransM.error s!"parseProcedure expects procedure or function, got {repr op.name}"
 

Strata/Languages/Laurel/Grammar/LaurelGrammar.lean

@@ -9,7 +9,7 @@ module
 -- Laurel dialect definition, loaded from LaurelGrammar.st
 -- NOTE: Changes to LaurelGrammar.st are not automatically tracked by the build system.
 -- Update this file (e.g. this comment) to trigger a recompile after modifying LaurelGrammar.st.
--- Last grammar change: replaced regexType with general coreType
+-- Last grammar change: added invokeOn clause before ensures in procedure/function ops.
 public import Strata.DDM.Integration.Lean
 public meta import Strata.DDM.Integration.Lean
 

Strata/Languages/Laurel/Grammar/LaurelGrammar.st

@@ -90,7 +90,7 @@ category ElseBranch;
 op elseBranch(stmts : StmtExpr) : ElseBranch => @[prec(0)] "else" stmts;
 
 op ifThenElse (cond: StmtExpr, thenBranch: StmtExpr, elseBranch: Option ElseBranch): StmtExpr =>
-  @[prec(20)] "if (" cond ") " thenBranch:0 elseBranch:0;
+  @[prec(20)] "if " cond " then " thenBranch:0 elseBranch:0;
 
 op assert (cond : StmtExpr, errorMessage: Option ErrorSummary) : StmtExpr => @[prec(0)] "assert " cond:0 errorMessage:0;
 op assume (cond : StmtExpr) : StmtExpr => @[prec(0)] "assume " cond:0;
@@ -145,6 +145,9 @@ op datatype (name: Ident, constructors: DatatypeConstructorList): Datatype => "d
 category ReturnType;
 op returnType(returnType: LaurelType): ReturnType => ":" returnType;
 
+category InvokeOnClause;
+op invokeOnClause(trigger: StmtExpr): InvokeOnClause => "invokeOn" trigger:0;
+
 category RequiresClause;
 op requiresClause(cond: StmtExpr, errorMessage: Option ErrorSummary): RequiresClause => "requires" cond:0 errorMessage;
 
@@ -166,19 +169,21 @@ op procedure (name : Ident, parameters: CommaSepBy Parameter,
   returnType: Option ReturnType,
   returnParameters: Option ReturnParameters,
   requires: Seq RequiresClause,
+  invokeOn: Option InvokeOnClause,
   ensures: Seq EnsuresClause,
   modifies: Seq ModifiesClause,
   body : Option Body) : Procedure =>
-  "procedure " name "(" parameters ")" returnType returnParameters requires ensures modifies body ";";
+  "procedure " name "(" parameters ")" returnType returnParameters requires invokeOn ensures modifies body ";";
 
 op function (name : Ident, parameters: CommaSepBy Parameter,
   returnType: Option ReturnType,
   returnParameters: Option ReturnParameters,
   requires: Seq RequiresClause,
+  invokeOn: Option InvokeOnClause,
   ensures: Seq EnsuresClause,
   modifies: Seq ModifiesClause,
   body : Option Body) : Procedure =>
-  "function " name "(" parameters ")" returnType returnParameters requires ensures modifies body ";";
+  "function " name "(" parameters ")" returnType returnParameters requires invokeOn ensures modifies body ";";
 
 op composite (name: Ident, extending: Option Extends, fields: Seq Field, procedures: Seq Procedure): Composite => "composite " name extending "{" fields procedures "}";