aiur: verify u32 addition from hinted sum

Ix/Aiur/Compiler/Check.lean

@@ -802,6 +802,20 @@ def inferTerm (t : Term) : CheckM Typed.Term := match t with
     let a' ← checkNoEscape a .field
     let b' ← checkNoEscape b .field
     pure (Typed.Term.u32LessThan .field false a' b')
+  | .unconstrainedU32Add a b => do
+    let word : Typ := .array .u8 4
+    let a' ← checkNoEscape a word
+    let b' ← checkNoEscape b word
+    pure (Typed.Term.unconstrainedU32Add (.tuple #[.array .field 4, .field]) false a' b')
+  | .unconstrainedU32Add3 a b c => do
+    let word : Typ := .array .u8 4
+    let a' ← checkNoEscape a word
+    let b' ← checkNoEscape b word
+    let c' ← checkNoEscape c word
+    pure (Typed.Term.unconstrainedU32Add3 (.tuple #[.array .field 4, .field]) false a' b' c')
+  | .u32ToField a => do
+    let a' ← checkNoEscape a (.array .u8 4)
+    pure (Typed.Term.u32ToField .field false a')
   | .u8Lit n => do
     if n ≥ 256 then throw (.u8LitOutOfRange n)
     pure (Typed.Term.field .u8 false (G.ofNat n))
@@ -1010,6 +1024,13 @@ def zonkTypedTerm (t : Typed.Term) : CheckM Typed.Term := match t with
       pure (.unconstrainedGToBytes (← zonkTyp τ) e (← zonkTypedTerm a))
   | .unconstrainedGInverse τ e a => do
       pure (.unconstrainedGInverse (← zonkTyp τ) e (← zonkTypedTerm a))
+  | .unconstrainedU32Add τ e a b => do
+      pure (.unconstrainedU32Add (← zonkTyp τ) e (← zonkTypedTerm a) (← zonkTypedTerm b))
+  | .unconstrainedU32Add3 τ e a b c => do
+      pure (.unconstrainedU32Add3 (← zonkTyp τ) e (← zonkTypedTerm a) (← zonkTypedTerm b)
+        (← zonkTypedTerm c))
+  | .u32ToField τ e a => do
+      pure (.u32ToField (← zonkTyp τ) e (← zonkTypedTerm a))
   | .toField τ e a => do pure (.toField (← zonkTyp τ) e (← zonkTypedTerm a))
   | .u8FromFieldUnsafe τ e a => do
       pure (.u8FromFieldUnsafe (← zonkTyp τ) e (← zonkTypedTerm a))

Ix/Aiur/Compiler/Concretize.lean

@@ -361,6 +361,14 @@ def termToConcrete
   | .u32LessThan τ e a b => do
       pure (.u32LessThan (← typToConcrete mono τ) e
                          (← termToConcrete mono a) (← termToConcrete mono b))
+  | .unconstrainedU32Add τ e a b => do
+      pure (.unconstrainedU32Add (← typToConcrete mono τ) e
+        (← termToConcrete mono a) (← termToConcrete mono b))
+  | .unconstrainedU32Add3 τ e a b c => do
+      pure (.unconstrainedU32Add3 (← typToConcrete mono τ) e
+        (← termToConcrete mono a) (← termToConcrete mono b) (← termToConcrete mono c))
+  | .u32ToField τ e a => do
+      pure (.u32ToField (← typToConcrete mono τ) e (← termToConcrete mono a))
   | .u8RangeCheck τ e a b => do
       pure (.u8RangeCheck (← typToConcrete mono τ) e
                           (← termToConcrete mono a) (← termToConcrete mono b))
@@ -576,6 +584,13 @@ def rewriteTypedTerm (decls : Typed.Decls)
       (rewriteTypedTerm decls subst mono a) (rewriteTypedTerm decls subst mono b)
   | .u32LessThan τ e a b => .u32LessThan (rewriteTyp subst mono τ) e
       (rewriteTypedTerm decls subst mono a) (rewriteTypedTerm decls subst mono b)
+  | .unconstrainedU32Add τ e a b => .unconstrainedU32Add (rewriteTyp subst mono τ) e
+      (rewriteTypedTerm decls subst mono a) (rewriteTypedTerm decls subst mono b)
+  | .unconstrainedU32Add3 τ e a b c => .unconstrainedU32Add3 (rewriteTyp subst mono τ) e
+      (rewriteTypedTerm decls subst mono a) (rewriteTypedTerm decls subst mono b)
+      (rewriteTypedTerm decls subst mono c)
+  | .u32ToField τ e a => .u32ToField (rewriteTyp subst mono τ) e
+      (rewriteTypedTerm decls subst mono a)
   | .u8RangeCheck τ e a b => .u8RangeCheck (rewriteTyp subst mono τ) e
       (rewriteTypedTerm decls subst mono a) (rewriteTypedTerm decls subst mono b)
   | .unconstrainedBigUintDivMod τ e a b => .unconstrainedBigUintDivMod (rewriteTyp subst mono τ) e
@@ -658,11 +673,14 @@ def collectInTypedTerm (seen : Std.HashSet (Global × Array Typ)) :
   | .u8ChainRotr7 τ _ a b | .u8ChainRotr4 τ _ a b | .u8RangeCheck τ _ a b
   | .unconstrainedBigUintDivMod τ _ a b
   | .u8And τ _ a b | .u8Or τ _ a b
-  | .u8LessThan τ _ a b | .u32LessThan τ _ a b =>
+  | .u8LessThan τ _ a b | .u32LessThan τ _ a b | .unconstrainedU32Add τ _ a b =>
     collectInTypedTerm (collectInTypedTerm (collectInTyp seen τ) a) b
+  | .unconstrainedU32Add3 τ _ a b c =>
+    collectInTypedTerm (collectInTypedTerm (collectInTypedTerm (collectInTyp seen τ) a) b) c
   | .eqZero τ _ a | .store τ _ a | .load τ _ a | .ptrVal τ _ a | .toField τ _ a
   | .u8FromFieldUnsafe τ _ a
   | .unconstrainedGToBytes τ _ a | .unconstrainedGInverse τ _ a
+  | .u32ToField τ _ a
   | .u8BitDecomposition τ _ a | .u8ShiftLeft τ _ a | .u8ShiftRight τ _ a =>
     collectInTypedTerm (collectInTyp seen τ) a
   | .ioGetInfo τ _ c k =>
@@ -730,11 +748,14 @@ def collectCalls (decls : Typed.Decls)
   | .u8ChainRotr7 _ _ a b | .u8ChainRotr4 _ _ a b | .u8RangeCheck _ _ a b
   | .unconstrainedBigUintDivMod _ _ a b
   | .u8And _ _ a b | .u8Or _ _ a b
-  | .u8LessThan _ _ a b | .u32LessThan _ _ a b =>
+  | .u8LessThan _ _ a b | .u32LessThan _ _ a b | .unconstrainedU32Add _ _ a b =>
     collectCalls decls (collectCalls decls seen a) b
+  | .unconstrainedU32Add3 _ _ a b c =>
+    collectCalls decls (collectCalls decls (collectCalls decls seen a) b) c
   | .eqZero _ _ a | .store _ _ a | .load _ _ a | .ptrVal _ _ a | .toField _ _ a
   | .u8FromFieldUnsafe _ _ a
   | .unconstrainedGToBytes _ _ a | .unconstrainedGInverse _ _ a
+  | .u32ToField _ _ a
   | .u8BitDecomposition _ _ a | .u8ShiftLeft _ _ a | .u8ShiftRight _ _ a =>
     collectCalls decls seen a
   | .ioGetInfo _ _ c k =>
@@ -846,6 +867,11 @@ def substInTypedTerm (subst : Global → Option Typ) : Typed.Term → Typed.Term
       (substInTypedTerm subst a) (substInTypedTerm subst b)
   | .u32LessThan τ e a b => .u32LessThan (Typ.instantiate subst τ) e
       (substInTypedTerm subst a) (substInTypedTerm subst b)
+  | .unconstrainedU32Add τ e a b => .unconstrainedU32Add (Typ.instantiate subst τ) e
+      (substInTypedTerm subst a) (substInTypedTerm subst b)
+  | .unconstrainedU32Add3 τ e a b c => .unconstrainedU32Add3 (Typ.instantiate subst τ) e
+      (substInTypedTerm subst a) (substInTypedTerm subst b) (substInTypedTerm subst c)
+  | .u32ToField τ e a => .u32ToField (Typ.instantiate subst τ) e (substInTypedTerm subst a)
   | .u8RangeCheck τ e a b => .u8RangeCheck (Typ.instantiate subst τ) e
       (substInTypedTerm subst a) (substInTypedTerm subst b)
   | .unconstrainedBigUintDivMod τ e a b => .unconstrainedBigUintDivMod (Typ.instantiate subst τ) e

Ix/Aiur/Compiler/Layout.lean

@@ -201,6 +201,19 @@ def opLayout : Bytecode.Op → LayoutM Unit
   | .u8ChainRotr7 .. | .u8ChainRotr4 .. => do pushDegrees #[1, 1, 1]; bumpAuxiliaries 3; bumpLookups
   | .u8LessThan .. => do pushDegree 1; bumpAuxiliaries; bumpLookups
   | .u32LessThan .. => do pushDegree 1; bumpAuxiliaries 12; bumpLookups 6
+  | .unconstrainedU32Add a b => do
+    let degrees ← (a ++ b).mapM getDegree
+    pushDegrees $ .replicate 4 1
+    pushDegree (degrees.foldl Nat.max 1)
+    bumpAuxiliaries 4
+  | .unconstrainedU32Add3 a b c => do
+    let degrees ← (a ++ b ++ c).mapM getDegree
+    pushDegrees $ .replicate 4 1
+    pushDegree (degrees.foldl Nat.max 1)
+    bumpAuxiliaries 4
+  | .u32ToField a => do
+    let degrees ← a.mapM getDegree
+    pushDegree (degrees.foldl Nat.max 0)
   -- Pure range-check lookup: no output columns/degrees, just one lookup.
   | .u8RangeCheck .. => bumpLookups
   -- Unconstrained hint: two fresh auxiliary witness columns (q_ptr, r_ptr).

Ix/Aiur/Compiler/Lower.lean

@@ -319,6 +319,18 @@ def toIndex
   | .u8Or _ _ i j => do let i ← expectIdx layoutMap bindings i; let j ← expectIdx layoutMap bindings j; pushOp (.u8Or i j)
   | .u8LessThan _ _ i j => do let i ← expectIdx layoutMap bindings i; let j ← expectIdx layoutMap bindings j; pushOp (.u8LessThan i j)
   | .u32LessThan _ _ i j => do let i ← expectIdx layoutMap bindings i; let j ← expectIdx layoutMap bindings j; pushOp (.u32LessThan i j)
+  | .unconstrainedU32Add _ _ a b => do
+    let a ← toIndex layoutMap bindings a
+    let b ← toIndex layoutMap bindings b
+    pushOp (.unconstrainedU32Add a b) 5
+  | .unconstrainedU32Add3 _ _ a b c => do
+    let a ← toIndex layoutMap bindings a
+    let b ← toIndex layoutMap bindings b
+    let c ← toIndex layoutMap bindings c
+    pushOp (.unconstrainedU32Add3 a b c) 5
+  | .u32ToField _ _ a => do
+    let a ← toIndex layoutMap bindings a
+    pushOp (.u32ToField a)
   | .u8RangeCheck _ _ i j => do
     -- Side-effecting lookup; the two `u8` outputs alias the inputs, so no new
     -- value slots are allocated (cf. `.assertEq`).

Ix/Aiur/Compiler/Match.lean

@@ -390,6 +390,9 @@ def typedToSimple : Term → Simple.Term
   | .u8Or τ e a b => .u8Or τ e (typedToSimple a) (typedToSimple b)
   | .u8LessThan τ e a b => .u8LessThan τ e (typedToSimple a) (typedToSimple b)
   | .u32LessThan τ e a b => .u32LessThan τ e (typedToSimple a) (typedToSimple b)
+  | .unconstrainedU32Add τ e a b => .unconstrainedU32Add τ e (typedToSimple a) (typedToSimple b)
+  | .unconstrainedU32Add3 τ e a b c => .unconstrainedU32Add3 τ e (typedToSimple a) (typedToSimple b) (typedToSimple c)
+  | .u32ToField τ e a => .u32ToField τ e (typedToSimple a)
   | .u8RangeCheck τ e a b => .u8RangeCheck τ e (typedToSimple a) (typedToSimple b)
   | .unconstrainedBigUintDivMod τ e a b => .unconstrainedBigUintDivMod τ e (typedToSimple a) (typedToSimple b)
   | .unconstrainedGToBytes τ e a => .unconstrainedGToBytes τ e (typedToSimple a)

Ix/Aiur/Compiler/Simple.lean

@@ -139,6 +139,13 @@ def simplifyTypedTerm (decls : Source.Decls) : Term → Except CheckError Term
   | .unconstrainedGToBytes τ e a => do
       let a' ← simplifyTypedTerm decls a
       pure (.unconstrainedGToBytes τ e a')
+  | .unconstrainedU32Add τ e a b => do
+      pure (.unconstrainedU32Add τ e (← simplifyTypedTerm decls a) (← simplifyTypedTerm decls b))
+  | .unconstrainedU32Add3 τ e a b c => do
+      pure (.unconstrainedU32Add3 τ e (← simplifyTypedTerm decls a) (← simplifyTypedTerm decls b)
+        (← simplifyTypedTerm decls c))
+  | .u32ToField τ e a => do
+      pure (.u32ToField τ e (← simplifyTypedTerm decls a))
   | .unconstrainedGInverse τ e a => do
       let a' ← simplifyTypedTerm decls a
       pure (.unconstrainedGInverse τ e a')

Ix/Aiur/Interpret.lean

@@ -469,6 +469,30 @@ partial def interp (decls : Decls) (bindings : Bindings) : Term → InterpM Valu
       | .field a, .field b =>
           return .field (if a.val.toUInt32 < b.val.toUInt32 then 1 else 0)
       | _, _ => throwErr "u32LessThan: expected field values"
+  | .unconstrainedU32Add t1 t2 => do
+      match (← interp decls bindings t1), (← interp decls bindings t2) with
+      | .array a, .array b =>
+        let pack (xs : Array Value) := xs.toList.zipIdx.foldl
+          (fun n (v, i) => match v with | .field g => n + g.val.toNat * 256 ^ i | _ => n) 0
+        let sum := pack a + pack b
+        return .tuple #[.array (#[0, 1, 2, 3].map fun i => .field (.ofNat ((sum / 256 ^ i) % 256))),
+          .field (.ofNat (sum / 0x100000000))]
+      | _, _ => throwErr "unconstrainedU32Add: expected byte arrays"
+  | .unconstrainedU32Add3 t1 t2 t3 => do
+      match (← interp decls bindings t1), (← interp decls bindings t2),
+          (← interp decls bindings t3) with
+      | .array a, .array b, .array c =>
+        let pack (xs : Array Value) := xs.toList.zipIdx.foldl
+          (fun n (v, i) => match v with | .field g => n + g.val.toNat * 256 ^ i | _ => n) 0
+        let sum := pack a + pack b + pack c
+        return .tuple #[.array (#[0, 1, 2, 3].map fun i => .field (.ofNat ((sum / 256 ^ i) % 256))),
+          .field (.ofNat (sum / 0x100000000))]
+      | _, _, _ => throwErr "unconstrainedU32Add3: expected byte arrays"
+  | .u32ToField t => do
+      match ← interp decls bindings t with
+      | .array a => return .field (.ofNat (a.toList.zipIdx.foldl
+          (fun n (v, i) => match v with | .field g => n + g.val.toNat * 256 ^ i | _ => n) 0))
+      | _ => throwErr "u32ToField: expected byte array"
   | .u8RangeCheck t1 t2 => do
       match (← interp decls bindings t1), (← interp decls bindings t2) with
       | .field a, .field b =>

Ix/Aiur/Meta.lean

@@ -203,6 +203,9 @@ syntax "u8_and" "(" aiur_trm ", " aiur_trm ")"                              : ai
 syntax "u8_or" "(" aiur_trm ", " aiur_trm ")"                               : aiur_trm
 syntax "u8_less_than" "(" aiur_trm ", " aiur_trm ")"                        : aiur_trm
 syntax "u32_less_than" "(" aiur_trm ", " aiur_trm ")"                       : aiur_trm
+syntax "unconstrained_u32_add" "(" aiur_trm ", " aiur_trm ")"               : aiur_trm
+syntax "unconstrained_u32_add3" "(" aiur_trm ", " aiur_trm ", " aiur_trm ")" : aiur_trm
+syntax "u32_to_field" "(" aiur_trm ")"                                      : aiur_trm
 syntax "u8_range_check" "(" aiur_trm ", " aiur_trm ")"                      : aiur_trm
 syntax "unconstrained_big_uint_div_mod" "(" aiur_trm ", " aiur_trm ")"           : aiur_trm
 syntax "unconstrained_g_to_bytes" "(" aiur_trm ")"                          : aiur_trm
@@ -352,6 +355,12 @@ partial def elabTrm : ElabStxCat `aiur_trm
     mkAppM ``Source.Term.u8LessThan #[← elabTrm i, ← elabTrm j]
   | `(aiur_trm| u32_less_than($i:aiur_trm, $j:aiur_trm)) => do
     mkAppM ``Source.Term.u32LessThan #[← elabTrm i, ← elabTrm j]
+  | `(aiur_trm| unconstrained_u32_add($i:aiur_trm, $j:aiur_trm)) => do
+    mkAppM ``Source.Term.unconstrainedU32Add #[← elabTrm i, ← elabTrm j]
+  | `(aiur_trm| unconstrained_u32_add3($i:aiur_trm, $j:aiur_trm, $k:aiur_trm)) => do
+    mkAppM ``Source.Term.unconstrainedU32Add3 #[← elabTrm i, ← elabTrm j, ← elabTrm k]
+  | `(aiur_trm| u32_to_field($a:aiur_trm)) => do
+    mkAppM ``Source.Term.u32ToField #[← elabTrm a]
   | `(aiur_trm| u8_range_check($i:aiur_trm, $j:aiur_trm)) => do
     mkAppM ``Source.Term.u8RangeCheck #[← elabTrm i, ← elabTrm j]
   | `(aiur_trm| unconstrained_big_uint_div_mod($a:aiur_trm, $b:aiur_trm)) => do
@@ -580,6 +589,18 @@ where
       let i ← replaceToken old new i
       let j ← replaceToken old new j
       `(aiur_trm| u32_less_than($i, $j))
+    | `(aiur_trm| unconstrained_u32_add($i:aiur_trm, $j:aiur_trm)) => do
+      let i ← replaceToken old new i
+      let j ← replaceToken old new j
+      `(aiur_trm| unconstrained_u32_add($i, $j))
+    | `(aiur_trm| unconstrained_u32_add3($i:aiur_trm, $j:aiur_trm, $k:aiur_trm)) => do
+      let i ← replaceToken old new i
+      let j ← replaceToken old new j
+      let k ← replaceToken old new k
+      `(aiur_trm| unconstrained_u32_add3($i, $j, $k))
+    | `(aiur_trm| u32_to_field($a:aiur_trm)) => do
+      let a ← replaceToken old new a
+      `(aiur_trm| u32_to_field($a))
     | `(aiur_trm| u8_range_check($i:aiur_trm, $j:aiur_trm)) => do
       let i ← replaceToken old new i
       let j ← replaceToken old new j

Ix/Aiur/Semantics/BytecodeEval.lean

@@ -342,6 +342,22 @@ def evalOp (t : Bytecode.Toplevel) (fuel : Nat) (op : Op) (st : EvalState) :
   | .u32LessThan a b => do
     let x ← readIdx st a; let y ← readIdx st b
     pure (pushMap st (if x.val.toUInt32 < y.val.toUInt32 then 1 else 0))
+  | .unconstrainedU32Add a b => do
+    let pack (idxs : Array Nat) := idxs.toList.zipIdx.foldl
+      (fun n (idx, i) => n + (st.map[idx]?.getD 0).val.toNat * 256 ^ i) 0
+    let sum := pack a + pack b
+    let bytes := #[0, 1, 2, 3].map fun i => G.ofNat ((sum / 256 ^ i) % 256)
+    pure (pushMap (appendMap st bytes) (.ofNat (sum / 0x100000000)))
+  | .unconstrainedU32Add3 a b c => do
+    let pack (idxs : Array Nat) := idxs.toList.zipIdx.foldl
+      (fun n (idx, i) => n + (st.map[idx]?.getD 0).val.toNat * 256 ^ i) 0
+    let sum := pack a + pack b + pack c
+    let bytes := #[0, 1, 2, 3].map fun i => G.ofNat ((sum / 256 ^ i) % 256)
+    pure (pushMap (appendMap st bytes) (.ofNat (sum / 0x100000000)))
+  | .u32ToField bytes => do
+    let word := bytes.toList.zipIdx.foldl
+      (fun n (idx, i) => n + (st.map[idx]?.getD 0).val.toNat * 256 ^ i) 0
+    pure (pushMap st (.ofNat word))
   | .u8RangeCheck a b => do
     -- No value pushed: the `u8` results alias the inputs. Fails if either is
     -- outside `[0, 256)` (exactly what the byte-chip lookup enforces).

Ix/Aiur/Semantics/SourceEval.lean

@@ -551,6 +551,40 @@ def interp (decls : Decls) (fuel : Nat) (bindings : Bindings)
       combineFieldsResult (fun a b => .field (if a.val.toUInt32 < b.val.toUInt32 then 1 else 0))
         (interp decls fuel bindings t1 st)
         (fun st1 => interp decls fuel bindings t2 st1)
+  | .unconstrainedU32Add t1 t2 =>
+      match interp decls fuel bindings t1 st with
+      | .error e => .error e
+      | .ok (v1, st1) => match interp decls fuel bindings t2 st1 with
+        | .error e => .error e
+        | .ok (v2, st2) => match v1, v2 with
+          | .array a, .array b =>
+            let pack (xs : Array Value) := xs.toList.zipIdx.foldl
+              (fun n (v, i) => match v with | .field g => n + g.val.toNat * 256 ^ i | _ => n) 0
+            let sum := pack a + pack b
+            .ok (.tuple #[.array (#[0, 1, 2, 3].map fun i => .field (.ofNat ((sum / 256 ^ i) % 256))),
+              .field (.ofNat (sum / 0x100000000))], st2)
+          | _, _ => .error (.typeMismatch "unconstrainedU32Add")
+  | .unconstrainedU32Add3 t1 t2 t3 =>
+      match interp decls fuel bindings t1 st with
+      | .error e => .error e
+      | .ok (v1, st1) => match interp decls fuel bindings t2 st1 with
+        | .error e => .error e
+        | .ok (v2, st2) => match interp decls fuel bindings t3 st2 with
+          | .error e => .error e
+          | .ok (v3, st3) => match v1, v2, v3 with
+            | .array a, .array b, .array c =>
+              let pack (xs : Array Value) := xs.toList.zipIdx.foldl
+                (fun n (v, i) => match v with | .field g => n + g.val.toNat * 256 ^ i | _ => n) 0
+              let sum := pack a + pack b + pack c
+              .ok (.tuple #[.array (#[0, 1, 2, 3].map fun i => .field (.ofNat ((sum / 256 ^ i) % 256))),
+                .field (.ofNat (sum / 0x100000000))], st3)
+            | _, _, _ => .error (.typeMismatch "unconstrainedU32Add3")
+  | .u32ToField t =>
+      match interp decls fuel bindings t st with
+      | .error e => .error e
+      | .ok (.array a, st') => .ok (.field (.ofNat (a.toList.zipIdx.foldl
+          (fun n (v, i) => match v with | .field g => n + g.val.toNat * 256 ^ i | _ => n) 0)), st')
+      | .ok _ => .error (.typeMismatch "u32ToField")
   | .u8RangeCheck t1 t2 =>
       match interp decls fuel bindings t1 st with
       | .error e => .error e

Ix/Aiur/Stages/Bytecode.lean

@@ -65,6 +65,13 @@ inductive Op
   auxiliary value, no constraint relation; the caller must pin it via
   multiply-and-assert. Appended last (tag 30). -/
   | unconstrainedGInverse : ValIdx → Op
+  /-- Native wrapping u32 addition. Four result bytes are advice columns; the
+  carry is a fifth logical output represented by a compound expression. -/
+  | unconstrainedU32Add : Array ValIdx → Array ValIdx → Op
+  /-- Native wrapping three-input u32 addition, with virtual carry output. -/
+  | unconstrainedU32Add3 : Array ValIdx → Array ValIdx → Array ValIdx → Op
+  /-- Virtual LE-byte packing expression; allocates no auxiliary column. -/
+  | u32ToField : Array ValIdx → Op
   deriving Repr, BEq, Hashable
 
 mutual