Remove functions

Strata/Backends/CBMC/GOTO/InstToJson.lean

@@ -236,9 +236,8 @@ def instructionToJson (inst : Instruction) : Except String Json := do
     ("instructionId", Json.str (toString inst.type)),
     ("locationNumber", Json.num inst.locationNum)
   ]
-  let guardField ← if inst.type == .GOTO || !Expr.beq inst.guard Expr.true then do
+  let guardField ← do
     pure [("guard", ← exprToJsonWithNamedFields inst.guard)]
-  else pure []
   let codeField ← if inst.code == Code.skip then pure [] else do
     pure [("code", ← codeToJson inst.code)]
   let targetsField := match inst.type, inst.target with

Strata/Backends/CBMC/GOTO/LambdaToCProverGOTO.lean

@@ -255,6 +255,36 @@ def LExprT.toGotoExpr {TBase: LExprParamsT} [ToString TBase.base.IDMeta] (e : LE
     let e1g ← toGotoExpr e1
     let e2g ← toGotoExpr e2
     return { id := .binary .Equal, type := .Boolean, operands := [e1g, e2g] }
+  -- Quaternary Functions (4 arguments)
+  | .app m (.app _ (.app _ (.app _ (.op _ fn _) e1) e2) e3) e4 =>
+    let op ← fnToGotoID (toString fn)
+    let gty ← m.type.toGotoType
+    let e1g ← toGotoExpr e1
+    let e2g ← toGotoExpr e2
+    let e3g ← toGotoExpr e3
+    let e4g ← toGotoExpr e4
+    return { id := op, type := gty, operands := [e1g, e2g, e3g, e4g] }
+  -- Quinary Functions (5 arguments)
+  | .app m (.app _ (.app _ (.app _ (.app _ (.op _ fn _) e1) e2) e3) e4) e5 =>
+    let op ← fnToGotoID (toString fn)
+    let gty ← m.type.toGotoType
+    let e1g ← toGotoExpr e1
+    let e2g ← toGotoExpr e2
+    let e3g ← toGotoExpr e3
+    let e4g ← toGotoExpr e4
+    let e5g ← toGotoExpr e5
+    return { id := op, type := gty, operands := [e1g, e2g, e3g, e4g, e5g] }
+  -- Senary Functions (6 arguments)
+  | .app m (.app _ (.app _ (.app _ (.app _ (.app _ (.op _ fn _) e1) e2) e3) e4) e5) e6 =>
+    let op ← fnToGotoID (toString fn)
+    let gty ← m.type.toGotoType
+    let e1g ← toGotoExpr e1
+    let e2g ← toGotoExpr e2
+    let e3g ← toGotoExpr e3
+    let e4g ← toGotoExpr e4
+    let e5g ← toGotoExpr e5
+    let e6g ← toGotoExpr e6
+    return { id := op, type := gty, operands := [e1g, e2g, e3g, e4g, e5g, e6g] }
   | _ => .error f!"[toGotoExpr] Not yet implemented: {e}"
 
 /--
@@ -354,6 +384,41 @@ def LExpr.toGotoExprCtx {TBase: LExprParams} [ToString $ LExpr TBase.mono]
     let tg ← toGotoExprCtx bvars t
     let eg ← toGotoExprCtx bvars e
     return (Expr.ite cg tg eg)
+  -- N-ary Functions (4+ arguments) — handles function applications with more
+  -- than 3 arguments that aren't caught by the ternary/binary/unary cases.
+  -- Pattern: .app _ (.app _ (.app _ (.app _ (.op _ fn ty) e1) e2) e3) e4
+  | .app _ (.app _ (.app _ (.app _ (.op _ fn (some ty)) e1) e2) e3) e4 =>
+    let op ← fnToGotoID (toString fn)
+    let retty := ty.destructArrow.getLast!
+    let gty ← retty.toGotoType
+    let e1g ← toGotoExprCtx bvars e1
+    let e2g ← toGotoExprCtx bvars e2
+    let e3g ← toGotoExprCtx bvars e3
+    let e4g ← toGotoExprCtx bvars e4
+    return { id := op, type := gty, operands := [e1g, e2g, e3g, e4g] }
+  -- Quinary (5 arguments)
+  | .app _ (.app _ (.app _ (.app _ (.app _ (.op _ fn (some ty)) e1) e2) e3) e4) e5 =>
+    let op ← fnToGotoID (toString fn)
+    let retty := ty.destructArrow.getLast!
+    let gty ← retty.toGotoType
+    let e1g ← toGotoExprCtx bvars e1
+    let e2g ← toGotoExprCtx bvars e2
+    let e3g ← toGotoExprCtx bvars e3
+    let e4g ← toGotoExprCtx bvars e4
+    let e5g ← toGotoExprCtx bvars e5
+    return { id := op, type := gty, operands := [e1g, e2g, e3g, e4g, e5g] }
+  -- Senary (6 arguments)
+  | .app _ (.app _ (.app _ (.app _ (.app _ (.app _ (.op _ fn (some ty)) e1) e2) e3) e4) e5) e6 =>
+    let op ← fnToGotoID (toString fn)
+    let retty := ty.destructArrow.getLast!
+    let gty ← retty.toGotoType
+    let e1g ← toGotoExprCtx bvars e1
+    let e2g ← toGotoExprCtx bvars e2
+    let e3g ← toGotoExprCtx bvars e3
+    let e4g ← toGotoExprCtx bvars e4
+    let e5g ← toGotoExprCtx bvars e5
+    let e6g ← toGotoExprCtx bvars e6
+    return { id := op, type := gty, operands := [e1g, e2g, e3g, e4g, e5g, e6g] }
   | _ => .error f!"[toGotoExprCtx] Not yet implemented: {toString e}"
 
 /--

Strata/Cli/VerifyOptions.lean

@@ -158,7 +158,9 @@ def parseVerifyOptions (pflags : ParsedFlags)
 def laurelTranslateFlags : List Flag := [
   { name := "keep-all-files",
     help := "Store intermediate Laurel and Core programs in <dir>.",
-    takesArg := .arg "dir" }
+    takesArg := .arg "dir" },
+  { name := "always-call-core-functions",
+    help := "Redirect calls to single-output procedures to their pure $asFunction versions (keeps them constant-foldable during symbolic evaluation)." }
 ]
 
 /-- All CLI flags accepted by Laurel verify commands. -/

Strata/Languages/Core/CoreOp.lean

@@ -199,7 +199,7 @@ inductive MapOpKind where
   deriving Repr, DecidableEq, Inhabited, BEq, Hashable
 
 def MapOpKind.names : List (MapOpKind × String) :=
-  [(.Const, "const"), (.Select, "select"), (.Update, "update")]
+  [(.Const, "mapConst"), (.Select, "select"), (.Update, "update")]
 
 def MapOpKind.toString (k : MapOpKind) : String := lookupName names k
 instance : ToString MapOpKind := ⟨MapOpKind.toString⟩

Strata/Languages/Core/DDMTransform/FormatCore.lean

@@ -689,9 +689,26 @@ partial def lappToExpr {M} [Inhabited M]
     : ToCSTM M (CoreDDM.Expr M) := do
   let (head, args) := Lambda.getLFuncCall e
   match head with
-  | .op _ fn _ =>
-    let argExprs ← args.mapM (lexprToExpr · qLevel)
-    lopToExpr fn.name argExprs
+  | .op _ fn ty =>
+    -- `mapConst` (the constant-map builtin) has no inferable key type, so it is
+    -- emitted with an explicit key-type annotation `mapConst<K>(v)`. Recover `K`
+    -- from the op's function type `V → Map K V`.
+    if fn.name == "mapConst" then
+      match args with
+      | [valArg] =>
+        let valCST ← lexprToExpr valArg qLevel
+        let kCST ← match ty with
+          | some (.tcons "arrow" [_, .tcons "Map" [k, _]]) => lmonoTyToCoreType k
+          | some (.tcons "Map" [k, _]) => lmonoTyToCoreType k
+          | _ => pure (CoreType.tvar default unknownTypeVar)
+        -- The value type is inferred from `v` on re-parse, so a placeholder is fine.
+        pure (.map_const default kCST (CoreType.tvar default unknownTypeVar) valCST)
+      | _ =>
+        let argExprs ← args.mapM (lexprToExpr · qLevel)
+        lopToExpr fn.name argExprs
+    else
+      let argExprs ← args.mapM (lexprToExpr · qLevel)
+      lopToExpr fn.name argExprs
   | .app _ fn arg =>
     -- getLFuncCall couldn't decompose further (fn is not .app or .op)
     let fnCST ← lexprToExpr fn qLevel

Strata/Languages/Core/DDMTransform/Grammar.lean

@@ -103,6 +103,10 @@ fn old (tp : Type, v : tp) : tp => "old " v;
 fn map_get (K : Type, V : Type, m : Map K V, k : K) : V => m "[" k "]";
 fn map_set (K : Type, V : Type, m : Map K V, k : K, v : V) : Map K V =>
   m "[" k ":=" v "]";
+// map_const uses explicit key-type annotation syntax: the key type cannot be
+// inferred from the single value argument, so it is written `mapConst<K>(v)`.
+// The value type V is inferred from `v`.
+fn map_const (K : Type, V : Type, v : V) : Map K V => "mapConst" "<" K ">" "(" v ")";
 
 // seq_empty uses explicit type annotation syntax since there are no value
 // arguments to infer the type parameter from.

Strata/Languages/Core/DDMTransform/Translate.lean

@@ -977,6 +977,12 @@ partial def translateExpr (p : Program) (bindings : TransBindings) (arg : Arg) :
      let i ← translateExpr p bindings ia
      let x ← translateExpr p bindings xa
      return .mkApp () fn [m, i, x]
+  | .fn _ q`Core.map_const, [_ktp, _vtp, va] =>
+     let kty ← translateLMonoTy bindings _ktp
+     let vty ← translateLMonoTy bindings _vtp
+     let fn : LExpr Core.CoreLParams.mono := (Core.coreOpExpr (.map .Const) (.some (LMonoTy.mkArrow vty [Core.mapTy kty vty])))
+     let v ← translateExpr p bindings va
+     return .mkApp () fn [v]
   -- Seq operations
   | .fn _ q`Core.seq_length, [_atp, sa] =>
      let ety ← translateLMonoTy bindings _atp

Strata/Languages/Core/Factory.lean

@@ -363,18 +363,21 @@ def reNoneFunc : WFLFunc CoreLParams :=
   nullaryUneval "Re.None" mty[regex]
 
 /- A constant `Map` constructor with type `∀k, v. v → Map k v`.
-   `const(d)` returns a map where every key maps to the value `d`. -/
+   `mapConst(d)` returns a map where every key maps to the value `d`.
+   Named `mapConst` (not `const`) to avoid colliding with the `const`
+   declaration keyword in the Core grammar, which would otherwise make
+   pretty-printed programs fail to re-parse. -/
 def mapConstFunc : WFLFunc CoreLParams :=
-  polyUneval "const" ["k", "v"]
+  polyUneval "mapConst" ["k", "v"]
     [("d", mty[%v])]
     (mapTy mty[%k] mty[%v])
     (axioms := [
       esM[∀ (%v): -- %1 d
           (∀ (%k): -- %0 kk
             {(((~select : (Map %k %v) → %k → %v)
-                ((~const : %v → (Map %k %v)) %1)) %0)}
+                ((~mapConst : %v → (Map %k %v)) %1)) %0)}
             (((~select : (Map %k %v) → %k → %v)
-                ((~const : %v → (Map %k %v)) %1)) %0) == %1)]
+                ((~mapConst : %v → (Map %k %v)) %1)) %0) == %1)]
     ])
 
 /- A `Map` selection function with type `∀k, v. Map k v → k → v`. -/

Strata/Languages/Laurel/ConstrainedTypeElim.lean

@@ -71,9 +71,9 @@ def constraintCallFor (ptMap : ConstrainedTypeMap) (ty : HighType)
     (varName : Identifier) (src : Option FileRange := none) : Option StmtExprMd :=
   constraintCallForExpr ptMap ty ⟨.Var (.Local varName), src⟩ src
 
-/-- Generate a constraint function for a constrained type.
-    For nested types, the function calls the parent's constraint function. -/
-def mkConstraintFunc (ptMap : ConstrainedTypeMap) (ct : ConstrainedType) : Procedure :=
+/-- Generate a constraint procedure for a constrained type.
+    For nested types, the procedure calls the parent's constraint procedure. -/
+def mkConstraintProc (ptMap : ConstrainedTypeMap) (ct : ConstrainedType) : Procedure :=
   let baseType := resolveType ptMap ct.base
   let bodyExpr: StmtExprMd := match ct.base.val with
     | .UserDefined parent =>
@@ -90,7 +90,6 @@ def mkConstraintFunc (ptMap : ConstrainedTypeMap) (ct : ConstrainedType) : Proce
     inputs := [{ name := ct.valueName, type := baseType }]
     outputs := [{ name := mkId "result", type := { val := .TBool, source := none } }]
     body := .Transparent { val := .Return bodyExpr, source := none }
-    isFunctional := true
     decreases := none
     preconditions := [] }
 
@@ -166,16 +165,15 @@ def elimProc (ptMap : ConstrainedTypeMap) (model : SemanticModel) (proc : Proced
   let inputRequires : List Condition := proc.inputs.filterMap fun p =>
     (constraintCallFor ptMap p.type.val p.name (src := p.type.source)).map
       fun c => { condition := c }
-  let outputEnsures : List Condition := if proc.isFunctional then [] else proc.outputs.filterMap fun p =>
+  let outputEnsures : List Condition := proc.outputs.filterMap fun p =>
     (constraintCallFor ptMap p.type.val p.name (src := p.type.source)).map
       fun c => { condition := ⟨c.val, p.type.source⟩ }
   let body' := match proc.body with
   | .Transparent bodyExpr =>
     let body := elimStmts ptMap model bodyExpr
     if outputEnsures.isEmpty then .Transparent body
     else
-      let retBody := if proc.isFunctional then ⟨.Return (some body), bodyExpr.source⟩ else body
-      .Opaque outputEnsures (some retBody) []
+      .Opaque outputEnsures (some body) []
   | .Opaque postconds impl modif =>
     let impl' := impl.map (elimStmts ptMap model)
     .Opaque (postconds ++ outputEnsures) impl' modif
@@ -206,7 +204,6 @@ private def mkWitnessProc (ptMap : ConstrainedTypeMap) (ct : ConstrainedType) :
     outputs := []
     body := .Opaque [] (some ⟨.Block [witnessInit, assert] none, src⟩) []
     preconditions := []
-    isFunctional := false
     decreases := none }
 
 /-- Eliminate constrained types within a composite type definition: resolve
@@ -227,21 +224,17 @@ public def constrainedTypeElim (model : SemanticModel) (program : Program)
   let ptMap := buildConstrainedTypeMap program.types
   if ptMap.isEmpty then (program, []) else
   let constraintFuncs := program.types.filterMap fun
-    | .Constrained ct => some (mkConstraintFunc ptMap ct) | _ => none
+    | .Constrained ct => some (mkConstraintProc ptMap ct) | _ => none
   let witnessProcedures := program.types.filterMap fun
     | .Constrained ct => some (mkWitnessProc ptMap ct) | _ => none
-  let funcDiags := program.staticProcedures.foldl (init := []) fun acc proc =>
-    if proc.isFunctional && proc.outputs.any (fun p => isConstrainedType ptMap p.type.val) then
-      acc.cons (diagnosticFromSource proc.name.source "constrained return types on functions are not yet supported")
-    else acc
   ({ program with
     staticProcedures := constraintFuncs ++ program.staticProcedures.map (elimProc ptMap model)
                         ++ witnessProcedures
     types := program.types.filterMap fun
       | .Constrained _ => none
       | .Composite ct => some (.Composite (elimCompositeType ptMap model ct))
       | other => some other },
-   funcDiags)
+   [])
 
 /-- Pipeline pass: constrained type elimination. -/
 public def constrainedTypeElimPass : LoweringPass where