fix(intent): address bugbot and codex review findings

root · claude · root · commit b4f31da11137 · 2026-04-04T10:05:54.000+02:00
- evalIntent: reject non-void binding functions (Codex #4) - Eval eq/ne: return none for cross-type comparisons (Bugbot #5) - Circom: unique signal prefixes for repeated helper calls (Bugbot #13) - isUint256Expr: check constant value instead of assuming uint256 (Bugbot #10) - dedup: preserve first-occurrence order for Poseidon inputs (Bugbot #11) - Remove dead code: remapCtx, countEmitsExpr (Bugbot #12, #30) - compileStmts .call: skip non-void functions (Codex #24) - compileExpr .call: emit error comment for missing/bodyless fns (Codex #7) - validateParams: enforce positional order matching ABI (Codex #21) - evalConstInt: fuel-bounded to prevent cycles (Codex #22) - Update E2E test Poseidon orderings to match new dedup behavior Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
diff --git a/Compiler/Circom.lean b/Compiler/Circom.lean
@@ -63,14 +63,19 @@ def EmitState.addLine (st : EmitState) (line : String) : EmitState :=
 
 /-! ## Constant Folding -/
 
-/-- Try to evaluate a constant expression to an integer value at compile time. -/
-partial def evalConstInt (consts : List ConstDef) : Expr → Option Int
-  | .intLit n => some n
-  | .param name =>
-    match consts.find? (fun c => c.name == name) with
-    | some c => evalConstInt consts c.value
-    | none => none
-  | _ => none
+/-- Try to evaluate a constant expression to an integer value at compile time.
+    Uses fuel bounded by the number of constants to guard against cycles. -/
+def evalConstInt (consts : List ConstDef) (expr : Expr) : Option Int :=
+  go consts (consts.length + 1) expr
+where
+  go (consts : List ConstDef) : Nat → Expr → Option Int
+    | _, .intLit n => some n
+    | 0, _ => none  -- fuel exhausted (cycle in constants)
+    | fuel + 1, .param name =>
+      match consts.find? (fun c => c.name == name) with
+      | some c => go consts fuel c.value
+      | none => none
+    | _, _ => none
 
 /-- Split a 256-bit integer into lo/hi 128-bit limbs (as Nat). -/
 def splitUint256 (n : Int) : Nat × Nat :=
@@ -116,11 +121,6 @@ def remapStmtParams (fnPfx : String) (paramNames : List String) : Stmt → Stmt
   | .call fn args =>
     .call fn (args.map (remapParams fnPfx paramNames))
 
-/-- Remap a ParamCtx: add function prefix to param names. -/
-def remapCtx (fnPfx : String) (paramNames : List String) (ctx : ParamCtx) : ParamCtx :=
-  ctx.map (fun (n, t) =>
-    if paramNames.contains n then (s!"{fnPfx}_{n}", t) else (n, t))
-
 /-! ## Helpers for uint256 signal resolution -/
 
 /-- Check if an expression refers to a uint256 value. -/
@@ -129,8 +129,9 @@ def isUint256Expr (ctx : ParamCtx) (consts : List ConstDef) : Expr → Bool
     match ctx.findType name with
     | some .uint256 | some .int256 => true
     | _ =>
-      match consts.find? (fun c => c.name == name) with
-      | some _ => true  -- constants are typically uint256
+      -- Check if it's a constant whose value needs uint256 (lo/hi) treatment
+      match evalConstInt consts (.param name) with
+      | some n => n > (2 ^ 128 : Nat) || n < 0
       | none => false
   | .intLit n => n > (2 ^ 128 : Nat) || n < 0
   | _ => false
@@ -300,14 +301,19 @@ partial def compileExpr (st : EmitState) (ctx : ParamCtx)
     | some fn =>
       match fn.expr with
       | some body =>
-        -- Type-aware argument binding: uint256 params need lo/hi signals
-        let st := bindFnArgs st ctx fns consts fnName fn.params args
-        let fnCtx : ParamCtx := fn.params.map (fun (n, t) => (s!"{fnName}_{n}", t))
+        -- Use a unique prefix to avoid duplicate signals when the same helper is called twice
+        let (uniquePfx, st) := st.fresh fnName
+        let st := bindFnArgs st ctx fns consts uniquePfx fn.params args
+        let fnCtx : ParamCtx := fn.params.map (fun (n, t) => (s!"{uniquePfx}_{n}", t))
         let paramNames := fn.params.map (·.1)
-        let remappedBody := remapParams fnName paramNames body
+        let remappedBody := remapParams uniquePfx paramNames body
         compileExpr st (fnCtx ++ ctx) fns consts remappedBody
-      | none => ("0", st)
-    | none => ("0", st)
+      | none =>
+        let st := st.addLine s!"    // ERROR: function '{fnName}' has no expression body"
+        ("0", st)
+    | none =>
+      let st := st.addLine s!"    // ERROR: undefined function '{fnName}'"
+      ("0", st)
   -- index and length are not directly compilable to circuits in general;
   -- they are resolved during forEach unrolling. If reached here, emit 0.
   | .index _ _ => ("0", st)
@@ -389,13 +395,19 @@ partial def compileStmts (st : EmitState) (ctx : ParamCtx)
     | .call fnName args =>
       match fns.find? (fun f => f.name == fnName) with
       | some fn =>
-        let st := bindFnArgs st ctx fns consts fnName fn.params args
-        let fnCtx : ParamCtx := fn.params.map (fun (n, t) => (s!"{fnName}_{n}", t))
-        let paramNames := fn.params.map (·.1)
-        let remappedBody := fn.body.map (remapStmtParams fnName paramNames)
-        let (st, callPaths, nextIdx) := compileStmts st (fnCtx ++ ctx) fns consts remappedBody condSig nextTemplateIdx
-        let (st, restPaths, nextIdx) := compileStmts st ctx fns consts rest condSig nextIdx
-        (st, callPaths ++ restPaths, nextIdx)
+        -- Only inline void functions; non-void helpers are expression-level
+        if fn.returnKind != .void then
+          compileStmts st ctx fns consts rest condSig nextTemplateIdx
+        else
+          -- Use a unique prefix to avoid duplicate signals when the same helper is called twice
+          let (uniquePfx, st) := st.fresh fnName
+          let st := bindFnArgs st ctx fns consts uniquePfx fn.params args
+          let fnCtx : ParamCtx := fn.params.map (fun (n, t) => (s!"{uniquePfx}_{n}", t))
+          let paramNames := fn.params.map (·.1)
+          let remappedBody := fn.body.map (remapStmtParams uniquePfx paramNames)
+          let (st, callPaths, nextIdx) := compileStmts st (fnCtx ++ ctx) fns consts remappedBody condSig nextTemplateIdx
+          let (st, restPaths, nextIdx) := compileStmts st ctx fns consts rest condSig nextIdx
+          (st, callPaths ++ restPaths, nextIdx)
       | none =>
         compileStmts st ctx fns consts rest condSig nextTemplateIdx
 
@@ -414,9 +426,13 @@ private def indexed (xs : List α) : List (Nat × α) :=
     | i, x :: rest => (i, x) :: go (i + 1) rest
   go 0 xs
 
-private def dedup : List String → List String
-  | [] => []
-  | x :: xs => if xs.contains x then dedup xs else x :: dedup xs
+private def dedup (xs : List String) : List String :=
+  let rec go : List String → List String → List String
+    | [], _ => []
+    | x :: rest, seen =>
+      if seen.contains x then go rest seen
+      else x :: go rest (x :: seen)
+  go xs []
 
 /-- Generate Circom source for a single intent binding.
     `selectorHex` is the 4-byte selector as a hex string (e.g. "0xa9059cbb").
diff --git a/Verity/Intent/Eval.lean b/Verity/Intent/Eval.lean
@@ -104,11 +104,21 @@ def evalExpr (fns : List FnDecl) (consts : List ConstDef) (env : Env)
     | Expr.eq a b => do
       let va ← evalExpr fns consts env fuel' a
       let vb ← evalExpr fns consts env fuel' b
-      some (.bool (va == vb))
+      match va, vb with
+      | .int x, .int y => some (.bool (x == y))
+      | .str x, .str y => some (.bool (x == y))
+      | .bool x, .bool y => some (.bool (x == y))
+      | .addr x, .addr y => some (.bool (x == y))
+      | _, _ => none  -- cross-type equality is undefined
     | Expr.ne a b => do
       let va ← evalExpr fns consts env fuel' a
       let vb ← evalExpr fns consts env fuel' b
-      some (.bool (va != vb))
+      match va, vb with
+      | .int x, .int y => some (.bool (x != y))
+      | .str x, .str y => some (.bool (x != y))
+      | .bool x, .bool y => some (.bool (x != y))
+      | .addr x, .addr y => some (.bool (x != y))
+      | _, _ => none  -- cross-type inequality is undefined
     | Expr.lt a b => do
       let va ← evalExpr fns consts env fuel' a
       let vb ← evalExpr fns consts env fuel' b
@@ -259,7 +269,9 @@ def evalIntent (spec : IntentSpec) (binding : IntentBinding)
     (params : List (String × Value)) (fuel : Nat := defaultFuel)
     : Option (List EmittedTemplate) := do
   let fn ← findFn spec.fns binding.intentFn
-  if fn.params.length != params.length then none
+  -- Only void functions emit templates; non-void (bool/string) are helpers
+  if fn.returnKind != .void then none
+  else if fn.params.length != params.length then none
   else
     let env : Env := params
     evalStmts spec.fns spec.constants env fuel fn.body
@@ -324,9 +336,13 @@ def paramCircuitValues (env : Env) (paramName : String) (ty : ParamType) : Optio
       | _ => none
 
 /-- Dedup preserving first-occurrence order (same as Circom.dedup). -/
-private def dedup : List String → List String
-  | [] => []
-  | x :: xs => if xs.contains x then dedup xs else x :: dedup xs
+private def dedup (xs : List String) : List String :=
+  let rec go : List String → List String → List String
+    | [], _ => []
+    | x :: rest, seen =>
+      if seen.contains x then go rest seen
+      else x :: go rest (x :: seen)
+  go xs []
 
 /-- Circuit output: the values that the Circom circuit commits to. -/
 structure CircuitOutput where
@@ -337,54 +353,27 @@ structure CircuitOutput where
   holeValues : List Nat
   deriving Repr
 
-mutual
-
-/-- Count total emit paths in an expression (for void function calls).
-    Same traversal as Circom's compileStmts — needed for index agreement. -/
-def countEmitsExpr (fns : List FnDecl) (consts : List ConstDef)
-    (fuel : Nat) (expr : Expr) : Nat :=
-  match fuel with
-  | 0 => 0
-  | fuel' + 1 =>
-    match expr with
-    | .call fnName _args =>
-      match findFn fns fnName with
-      | some fn =>
-        match fn.returnKind with
-        | .void => countEmitsStmts fns consts fuel' fn.body
-        | _ => 0
-      | none => 0
-    | _ => 0
-
 /-- Count total emit paths in a statement list (same traversal as Circom's compileStmts).
     Counts ALL paths, not just the one taken — needed for consistent index assignment. -/
-def countEmitsStmts (fns : List FnDecl) (consts : List ConstDef)
-    (fuel : Nat) : List Stmt → Nat
+partial def countEmitsStmts (fns : List FnDecl) (consts : List ConstDef)
+    : List Stmt → Nat
   | [] => 0
-  | stmts =>
-    match fuel with
-    | 0 => 0
-    | fuel' + 1 =>
-      match stmts with
-      | [] => 0
-      | .emit _ :: rest => 1 + countEmitsStmts fns consts fuel' rest
-      | .ite _cond thenBr elseBr :: rest =>
-        countEmitsStmts fns consts fuel' thenBr +
-        countEmitsStmts fns consts fuel' elseBr +
-        countEmitsStmts fns consts fuel' rest
-      | .forEach _var _array body :: rest =>
-        -- forEach emits are counted once (for the body pattern);
-        -- actual unrolling happens at runtime/circuit compile time
-        countEmitsStmts fns consts fuel' body +
-        countEmitsStmts fns consts fuel' rest
-      | .call fnName _args :: rest =>
-        match findFn fns fnName with
-        | some fn =>
-          countEmitsStmts fns consts fuel' fn.body +
-          countEmitsStmts fns consts fuel' rest
-        | none => countEmitsStmts fns consts fuel' rest
-
-end
+  | .emit _ :: rest => 1 + countEmitsStmts fns consts rest
+  | .ite _cond thenBr elseBr :: rest =>
+    countEmitsStmts fns consts thenBr +
+    countEmitsStmts fns consts elseBr +
+    countEmitsStmts fns consts rest
+  | .forEach _var _array body :: rest =>
+    -- forEach emits are counted once (for the body pattern);
+    -- actual unrolling happens at runtime/circuit compile time
+    countEmitsStmts fns consts body +
+    countEmitsStmts fns consts rest
+  | .call fnName _args :: rest =>
+    match findFn fns fnName with
+    | some fn =>
+      countEmitsStmts fns consts fn.body +
+      countEmitsStmts fns consts rest
+    | none => countEmitsStmts fns consts rest
 
 /-- Evaluate an intent and return the circuit-compatible output.
     This computes the same `(templateId, holeValues)` that the Circom
@@ -434,8 +423,8 @@ where
             findEmitIndex spec fn env fuel' rest target (startIdx + 1)
         | none => findEmitIndex spec fn env fuel' rest target (startIdx + 1)
       | .ite cond thenBranch elseBranch :: rest =>
-        let thenCount := countEmitsStmts spec.fns spec.constants fuel' thenBranch
-        let elseCount := countEmitsStmts spec.fns spec.constants fuel' elseBranch
+        let thenCount := countEmitsStmts spec.fns spec.constants thenBranch
+        let elseCount := countEmitsStmts spec.fns spec.constants elseBranch
         match evalExpr spec.fns spec.constants env fuel' cond with
         | some (.bool true) =>
           match findEmitIndex spec fn env fuel' thenBranch target startIdx with
@@ -447,7 +436,7 @@ where
           | none => findEmitIndex spec fn env fuel' rest target (startIdx + thenCount + elseCount)
         | _ => none
       | .forEach _var _array body :: rest =>
-        let bodyCount := countEmitsStmts spec.fns spec.constants fuel' body
+        let bodyCount := countEmitsStmts spec.fns spec.constants body
         -- forEach circuit output not yet supported — skip the body emits
         findEmitIndex spec fn env fuel' rest target (startIdx + bodyCount)
       | .call fnName args :: rest =>
@@ -457,7 +446,7 @@ where
           match argVals with
           | some vals =>
             let callEnv := List.zipWith (fun (name, _) val => (name, val)) calledFn.params vals
-            let callCount := countEmitsStmts spec.fns spec.constants fuel' calledFn.body
+            let callCount := countEmitsStmts spec.fns spec.constants calledFn.body
             match findEmitIndex spec calledFn callEnv fuel' calledFn.body target startIdx with
             | some idx => some idx
             | none => findEmitIndex spec fn env fuel' rest target (startIdx + callCount)
diff --git a/Verity/Intent/Example.lean b/Verity/Intent/Example.lean
@@ -330,7 +330,8 @@ test (`test_circom_e2e.sh`) hard-codes as Poseidon inputs.
 
 private def max128 : Nat := (2 ^ 128) - 1
 
--- Test: transfer(to=0xdead, amount=1000) → templateIdx=1 (else branch), holes=[1000, 0, 57005]
+-- Test: transfer(to=0xdead, amount=1000) → templateIdx=1 (else branch), holes=[57005, 1000, 0]
+-- Hole order: dedup first-occurrence of [to] ++ [amount, to] = [to, amount] → [to, amount_lo, amount_hi]
 #eval do
   let spec := erc20IntentSpec
   match getBinding spec 0 with
@@ -343,13 +344,14 @@ private def max128 : Nat := (2 ^ 128) - 1
     | some co =>
       unless co.templateIdx == 1 do
         throw (IO.userError s!"expected templateIdx=1, got {co.templateIdx}")
-      unless co.holeValues == [1000, 0, 57005] do
-        throw (IO.userError s!"expected holeValues=[1000, 0, 57005], got {repr co.holeValues}")
+      unless co.holeValues == [57005, 1000, 0] do
+        throw (IO.userError s!"expected holeValues=[57005, 1000, 0], got {repr co.holeValues}")
       IO.println s!"✓ Circuit output: transfer(1000) → templateIdx={co.templateIdx}, holes={repr co.holeValues}"
     | none => throw (IO.userError "evalIntentCircuitOutput returned none")
   | none => throw (IO.userError "binding not found")
 
--- Test: transfer(to=0xdead, amount=MAX) → templateIdx=0 (then branch), holes=[max128, max128, 57005]
+-- Test: transfer(to=0xdead, amount=MAX) → templateIdx=0 (then branch), holes=[57005, max128, max128]
+-- Hole order: [to, amount_lo, amount_hi]
 #eval do
   let spec := erc20IntentSpec
   match getBinding spec 0 with
@@ -362,8 +364,8 @@ private def max128 : Nat := (2 ^ 128) - 1
     | some co =>
       unless co.templateIdx == 0 do
         throw (IO.userError s!"expected templateIdx=0, got {co.templateIdx}")
-      unless co.holeValues == [max128, max128, 57005] do
-        throw (IO.userError s!"expected holeValues=[max128, max128, 57005], got {repr co.holeValues}")
+      unless co.holeValues == [57005, max128, max128] do
+        throw (IO.userError s!"expected holeValues=[57005, max128, max128], got {repr co.holeValues}")
       IO.println s!"✓ Circuit output: transfer(MAX) → templateIdx={co.templateIdx}, holes match"
     | none => throw (IO.userError "evalIntentCircuitOutput returned none")
   | none => throw (IO.userError "binding not found")
@@ -388,9 +390,9 @@ private def max128 : Nat := (2 ^ 128) - 1
   | none => throw (IO.userError "binding not found")
 
 -- Test: transferFrom(fromAddr=0xcafe, to=0xdead, amount=2000)
---   → templateIdx=1 (else branch), holes=[2000, 0, 51966, 57005]
---   Hole order: dedup of [fromAddr, to] ++ [amount, fromAddr, to] = [amount, fromAddr, to]
---   Values: amount_lo=2000, amount_hi=0, fromAddr=0xcafe=51966, to=0xdead=57005
+--   → templateIdx=1 (else branch), holes=[51966, 57005, 2000, 0]
+--   Hole order: dedup first-occurrence of [fromAddr, to] ++ [amount, fromAddr, to] = [fromAddr, to, amount]
+--   Values: fromAddr=0xcafe=51966, to=0xdead=57005, amount_lo=2000, amount_hi=0
 #eval do
   let spec := erc20IntentSpec
   match getBinding spec 2 with
@@ -404,14 +406,15 @@ private def max128 : Nat := (2 ^ 128) - 1
     | some co =>
       unless co.templateIdx == 1 do
         throw (IO.userError s!"expected templateIdx=1, got {co.templateIdx}")
-      unless co.holeValues == [2000, 0, 51966, 57005] do
-        throw (IO.userError s!"expected holeValues=[2000, 0, 51966, 57005], got {repr co.holeValues}")
+      unless co.holeValues == [51966, 57005, 2000, 0] do
+        throw (IO.userError s!"expected holeValues=[51966, 57005, 2000, 0], got {repr co.holeValues}")
       IO.println s!"✓ Circuit output: transferFrom(2000) → templateIdx={co.templateIdx}, holes={repr co.holeValues}"
     | none => throw (IO.userError "evalIntentCircuitOutput returned none")
   | none => throw (IO.userError "binding not found")
 
 -- Test: transferFrom(fromAddr=0xcafe, to=0xdead, amount=MAX)
---   → templateIdx=0 (then branch), holes=[max128, max128, 51966, 57005]
+--   → templateIdx=0 (then branch), holes=[51966, 57005, max128, max128]
+--   Hole order: [fromAddr, to, amount_lo, amount_hi]
 #eval do
   let spec := erc20IntentSpec
   match getBinding spec 2 with
@@ -425,8 +428,8 @@ private def max128 : Nat := (2 ^ 128) - 1
     | some co =>
       unless co.templateIdx == 0 do
         throw (IO.userError s!"expected templateIdx=0, got {co.templateIdx}")
-      unless co.holeValues == [max128, max128, 51966, 57005] do
-        throw (IO.userError s!"expected holeValues=[max128, max128, 51966, 57005], got {repr co.holeValues}")
+      unless co.holeValues == [51966, 57005, max128, max128] do
+        throw (IO.userError s!"expected holeValues=[51966, 57005, max128, max128], got {repr co.holeValues}")
       IO.println s!"✓ Circuit output: transferFrom(MAX) → templateIdx={co.templateIdx}, holes match"
     | none => throw (IO.userError "evalIntentCircuitOutput returned none")
   | none => throw (IO.userError "binding not found")
diff --git a/Verity/Intent/Validate.lean b/Verity/Intent/Validate.lean
@@ -37,26 +37,26 @@ private def findFnDecl? (spec : IntentSpec) (name : String) : Option FnDecl :=
   spec.fns.find? (fun f => f.name == name)
 
 /-- Validate that intent function params match the ABI function params.
+    Checks name, type, count, and order (order matters for Poseidon commitment).
     Returns a list of error messages. -/
 private def validateParams
     (bindingName : String)
     (intentParams : List (String × ParamType))
     (abiParams : List Param) : List String :=
-  let intentByName := intentParams
   let abiByName := abiParams.map (fun p => (p.name, p.ty))
-  -- Check each intent param exists in ABI with compatible type
-  let paramErrors := intentByName.filterMap fun (name, intentTy) =>
-    match abiByName.find? (fun (n, _) => n == name) with
-    | none => some s!"Binding '{bindingName}': intent param '{name}' not found in ABI function"
-    | some (_, abiTy) =>
-      if typesCompatible intentTy abiTy then none
-      else some s!"Binding '{bindingName}': param '{name}' type mismatch — intent has {repr intentTy}, ABI has {repr abiTy}"
-  -- Check each ABI param is covered by the intent
-  let missingErrors := abiByName.filterMap fun (name, _) =>
-    match intentByName.find? (fun (n, _) => n == name) with
-    | none => some s!"Binding '{bindingName}': ABI param '{name}' missing from intent function"
-    | some _ => none
-  paramErrors ++ missingErrors
+  -- Check count matches
+  let countErrors :=
+    if intentParams.length != abiByName.length then
+      [s!"Binding '{bindingName}': param count mismatch — intent has {intentParams.length}, ABI has {abiByName.length}"]
+    else []
+  -- Check positional match: name, type, and order must all agree
+  let positionalErrors := (intentParams.zip abiByName).filterMap fun ((iName, iTy), (aName, aTy)) =>
+    if iName != aName then
+      some s!"Binding '{bindingName}': param order mismatch — intent has '{iName}' where ABI expects '{aName}'"
+    else if !typesCompatible iTy aTy then
+      some s!"Binding '{bindingName}': param '{iName}' type mismatch — intent has {repr iTy}, ABI has {repr aTy}"
+    else none
+  countErrors ++ positionalErrors
 
 /-- Collect all function names called in an expression. -/
 private def exprCallNames : Expr → List String
diff --git a/scripts/test_circom_e2e.sh b/scripts/test_circom_e2e.sh
