diff --git a/.github/workflows/ignored.yml b/.github/workflows/ignored.yml index cb0af803..c55af487 100644 --- a/.github/workflows/ignored.yml +++ b/.github/workflows/ignored.yml @@ -44,4 +44,4 @@ jobs: --errors-for-leak-kinds=definite \ --track-origins=yes \ --error-exitcode=1 \ - .lake/build/bin/IxTests -- --include-ignored aiur aiur-hashes ixvm + .lake/build/bin/IxTests -- --include-ignored aiur aiur-hashes ixvm rbtree-map diff --git a/Ix/Aiur/Bytecode.lean b/Ix/Aiur/Bytecode.lean index 78abfc95..d61a6708 100644 --- a/Ix/Aiur/Bytecode.lean +++ b/Ix/Aiur/Bytecode.lean @@ -34,6 +34,7 @@ inductive Op | u8And : ValIdx → ValIdx → Op | u8Or : ValIdx → ValIdx → Op | u8LessThan : ValIdx → ValIdx → Op + | u32LessThan : ValIdx → ValIdx → Op | debug : String → Option (Array ValIdx) → Op deriving Repr diff --git a/Ix/Aiur/Check.lean b/Ix/Aiur/Check.lean index 8a560e25..38690d83 100644 --- a/Ix/Aiur/Check.lean +++ b/Ix/Aiur/Check.lean @@ -116,6 +116,7 @@ partial def inferTerm (t : Term) : CheckM TypedTerm := match t with | .u8Add a b => inferBinop a b .u8Add (.tuple #[.field, .field]) | .u8Sub a b => inferBinop a b .u8Sub (.tuple #[.field, .field]) | .u8LessThan a b => inferBinop a b .u8LessThan .field + | .u32LessThan a b => inferBinop a b .u32LessThan .field | .ioGetInfo key => inferIoGetInfo key | .ioSetInfo key idx len ret => inferIoSetInfo key idx len ret | .ioRead idx len => inferIoRead idx len diff --git a/Ix/Aiur/Compile.lean b/Ix/Aiur/Compile.lean index db6ae047..ae911804 100644 --- a/Ix/Aiur/Compile.lean +++ b/Ix/Aiur/Compile.lean @@ -135,6 +135,11 @@ def opLayout : Bytecode.Op → LayoutM Unit pushDegree 1 bumpAuxiliaries 1 bumpLookups + | .u32LessThan .. => do + pushDegree 1 + bumpAuxiliaries 24 + modify fun stt => { stt with + functionLayout := { stt.functionLayout with lookups := stt.functionLayout.lookups + 8 } } | .debug .. => pure () partial def blockLayout (block : Bytecode.Block) : LayoutM Unit := do @@ -467,6 +472,10 @@ partial def toIndex let i ← expectIdx i let j ← expectIdx j pushOp (.u8LessThan i j) + | .u32LessThan i j => do + let i ← expectIdx i + let j ← expectIdx j + pushOp (.u32LessThan i j) | .debug label term ret => do let term ← term.mapM (toIndex layoutMap bindings) modify fun stt => { stt with ops := stt.ops.push (.debug label term) } diff --git a/Ix/Aiur/Meta.lean b/Ix/Aiur/Meta.lean index 40e8cb94..b0eaf280 100644 --- a/Ix/Aiur/Meta.lean +++ b/Ix/Aiur/Meta.lean @@ -132,6 +132,7 @@ syntax "u8_sub" "(" trm ", " trm ")" : trm syntax "u8_and" "(" trm ", " trm ")" : trm syntax "u8_or" "(" trm ", " trm ")" : trm syntax "u8_less_than" "(" trm ", " trm ")" : trm +syntax "u32_less_than" "(" trm ", " trm ")" : trm syntax "dbg!" "(" str (", " trm)? ")" ";" (trm)? : trm syntax trm "[" "@" noWs ident "]" : trm @@ -237,6 +238,8 @@ partial def elabTrm : ElabStxCat `trm mkAppM ``Term.u8Or #[← elabTrm i, ← elabTrm j] | `(trm| u8_less_than($i:trm, $j:trm)) => do mkAppM ``Term.u8LessThan #[← elabTrm i, ← elabTrm j] + | `(trm| u32_less_than($i:trm, $j:trm)) => do + mkAppM ``Term.u32LessThan #[← elabTrm i, ← elabTrm j] | `(trm| dbg!($label:str $[, $t:trm]?); $[$ret:trm]?) => do let t ← match t with | none => mkAppOptM ``Option.none #[some (mkConst ``Term)] @@ -394,6 +397,10 @@ where let i ← replaceToken old new i let j ← replaceToken old new j `(trm| u8_less_than($i, $j)) + | `(trm| u32_less_than($i:trm, $j:trm)) => do + let i ← replaceToken old new i + let j ← replaceToken old new j + `(trm| u32_less_than($i, $j)) | `(trm| dbg!($label:str $[, $t:trm]?); $[$ret:trm]?) => do let t' ← t.mapM $ replaceToken old new let ret' ← ret.mapM $ replaceToken old new diff --git a/Ix/Aiur/Term.lean b/Ix/Aiur/Term.lean index e6cb8e3d..ee662e79 100644 --- a/Ix/Aiur/Term.lean +++ b/Ix/Aiur/Term.lean @@ -100,6 +100,7 @@ inductive Term | u8And : Term → Term → Term | u8Or : Term → Term → Term | u8LessThan : Term → Term → Term + | u32LessThan : Term → Term → Term | debug : String → Option Term → Term → Term deriving Repr, BEq, Hashable, Inhabited @@ -147,6 +148,7 @@ inductive TypedTermInner | u8And : TypedTerm → TypedTerm → TypedTermInner | u8Or : TypedTerm → TypedTerm → TypedTermInner | u8LessThan : TypedTerm → TypedTerm → TypedTermInner + | u32LessThan : TypedTerm → TypedTerm → TypedTermInner | debug : String → Option TypedTerm → TypedTerm → TypedTermInner deriving Repr, Inhabited diff --git a/Ix/IxVM/RBTreeMap.lean b/Ix/IxVM/RBTreeMap.lean new file mode 100644 index 00000000..5bf64b36 --- /dev/null +++ b/Ix/IxVM/RBTreeMap.lean @@ -0,0 +1,159 @@ +module +public import Ix.Aiur.Meta + +public section + +namespace IxVM + +def rbTreeMap := ⟦ + enum RBTreeMap { + -- Color {0: red, 1: black}, key, value, left, right + Node(G, G, G, &RBTreeMap, &RBTreeMap), + Nil + } + + -- Okasaki-style balance: fixes red-red violations after insertion + fn rbtree_map_balance(color: G, key: G, value: G, left: RBTreeMap, right: RBTreeMap) -> RBTreeMap { + match (color, left, right) { + -- Case 1: left child red, left-left grandchild red + (1, RBTreeMap.Node(0, yk, yv, &RBTreeMap.Node(0, xk, xv, a, b), c), d) => + RBTreeMap.Node(0, yk, yv, + store(RBTreeMap.Node(1, xk, xv, a, b)), + store(RBTreeMap.Node(1, key, value, c, store(d)))), + -- Case 2: left child red, left-right grandchild red + (1, RBTreeMap.Node(0, xk, xv, a, &RBTreeMap.Node(0, yk, yv, b, c)), d) => + RBTreeMap.Node(0, yk, yv, + store(RBTreeMap.Node(1, xk, xv, a, b)), + store(RBTreeMap.Node(1, key, value, c, store(d)))), + -- Case 3: right child red, right-left grandchild red + (1, a, RBTreeMap.Node(0, zk, zv, &RBTreeMap.Node(0, yk, yv, b, c), d)) => + RBTreeMap.Node(0, yk, yv, + store(RBTreeMap.Node(1, key, value, store(a), b)), + store(RBTreeMap.Node(1, zk, zv, c, d))), + -- Case 4: right child red, right-right grandchild red + (1, a, RBTreeMap.Node(0, yk, yv, b, &RBTreeMap.Node(0, zk, zv, c, d))) => + RBTreeMap.Node(0, yk, yv, + store(RBTreeMap.Node(1, key, value, store(a), b)), + store(RBTreeMap.Node(1, zk, zv, c, d))), + -- No violation + _ => RBTreeMap.Node(color, key, value, store(left), store(right)), + } + } + + -- Internal insert (new nodes are red) + fn rbtree_map_ins(key: G, value: G, tree: RBTreeMap) -> RBTreeMap { + match tree { + RBTreeMap.Nil => + RBTreeMap.Node(0, key, value, store(RBTreeMap.Nil), store(RBTreeMap.Nil)), + RBTreeMap.Node(color, k, v, &left, &right) => + let lt = u32_less_than(key, k); + match lt { + 1 => rbtree_map_balance(color, k, v, rbtree_map_ins(key, value, left), right), + _ => + let gt = u32_less_than(k, key); + match gt { + 1 => rbtree_map_balance(color, k, v, left, rbtree_map_ins(key, value, right)), + _ => RBTreeMap.Node(color, key, value, store(left), store(right)), + }, + }, + } + } + + -- Public insert: inserts key-value pair, enforces black root + fn rbtree_map_insert(key: G, value: G, tree: RBTreeMap) -> RBTreeMap { + let result = rbtree_map_ins(key, value, tree); + match result { + RBTreeMap.Node(_, k, v, left, right) => RBTreeMap.Node(1, k, v, left, right), + } + } + + -- Lookup: returns the value associated with the key. + -- Fails if the key is not found (no Nil case). + fn rbtree_map_lookup(key: G, tree: RBTreeMap) -> G { + match tree { + RBTreeMap.Node(_, k, v, &left, &right) => + let lt = u32_less_than(key, k); + match lt { + 1 => rbtree_map_lookup(key, left), + _ => + let gt = u32_less_than(k, key); + match gt { + 1 => rbtree_map_lookup(key, right), + _ => v, + }, + }, + } + } + + /- # Test entrypoints -/ + + fn rbtree_map_test() -> [G; 22] { + -- Single insert and lookup + let tree = rbtree_map_insert(5, 42, RBTreeMap.Nil); + let r0 = rbtree_map_lookup(5, tree); + + -- Three inserts + let tree = rbtree_map_insert(10, 100, RBTreeMap.Nil); + let tree = rbtree_map_insert(20, 200, tree); + let tree = rbtree_map_insert(5, 50, tree); + let r1 = rbtree_map_lookup(5, tree); + let r2 = rbtree_map_lookup(10, tree); + let r3 = rbtree_map_lookup(20, tree); + + -- Overwrite + let tree = rbtree_map_insert(10, 100, RBTreeMap.Nil); + let tree = rbtree_map_insert(10, 999, tree); + let r4 = rbtree_map_lookup(10, tree); + + -- Ascending insertion order + let tree = rbtree_map_insert(1, 10, RBTreeMap.Nil); + let tree = rbtree_map_insert(2, 20, tree); + let tree = rbtree_map_insert(3, 30, tree); + let tree = rbtree_map_insert(4, 40, tree); + let tree = rbtree_map_insert(5, 50, tree); + let r5 = rbtree_map_lookup(1, tree); + let r6 = rbtree_map_lookup(2, tree); + let r7 = rbtree_map_lookup(3, tree); + let r8 = rbtree_map_lookup(4, tree); + let r9 = rbtree_map_lookup(5, tree); + + -- Descending insertion order + let tree = rbtree_map_insert(5, 50, RBTreeMap.Nil); + let tree = rbtree_map_insert(4, 40, tree); + let tree = rbtree_map_insert(3, 30, tree); + let tree = rbtree_map_insert(2, 20, tree); + let tree = rbtree_map_insert(1, 10, tree); + let r10 = rbtree_map_lookup(1, tree); + let r11 = rbtree_map_lookup(2, tree); + let r12 = rbtree_map_lookup(3, tree); + let r13 = rbtree_map_lookup(4, tree); + let r14 = rbtree_map_lookup(5, tree); + + -- Mixed insertion order + let tree = rbtree_map_insert(50, 500, RBTreeMap.Nil); + let tree = rbtree_map_insert(30, 300, tree); + let tree = rbtree_map_insert(70, 700, tree); + let tree = rbtree_map_insert(20, 200, tree); + let tree = rbtree_map_insert(40, 400, tree); + let tree = rbtree_map_insert(60, 600, tree); + let tree = rbtree_map_insert(80, 800, tree); + let r15 = rbtree_map_lookup(20, tree); + let r16 = rbtree_map_lookup(30, tree); + let r17 = rbtree_map_lookup(40, tree); + let r18 = rbtree_map_lookup(50, tree); + let r19 = rbtree_map_lookup(60, tree); + let r20 = rbtree_map_lookup(70, tree); + let r21 = rbtree_map_lookup(80, tree); + + [r0, + r1, r2, r3, + r4, + r5, r6, r7, r8, r9, + r10, r11, r12, r13, r14, + r15, r16, r17, r18, r19, r20, r21] + } +⟧ + +end IxVM + +end diff --git a/Tests/Aiur.lean b/Tests/Aiur.lean index 043a2ae0..70e4ddda 100644 --- a/Tests/Aiur.lean +++ b/Tests/Aiur.lean @@ -3,3 +3,4 @@ module public import Tests.Aiur.Common public import Tests.Aiur.Aiur public import Tests.Aiur.Hashes +public import Tests.Aiur.RBTreeMap diff --git a/Tests/Aiur/Aiur.lean b/Tests/Aiur/Aiur.lean index f49afee8..a5ac14f6 100644 --- a/Tests/Aiur/Aiur.lean +++ b/Tests/Aiur/Aiur.lean @@ -219,6 +219,10 @@ def toplevel := ⟦ u8_or(i, j) } + fn u32_less_than_function(x: G, y: G) -> G { + u32_less_than(x, y) + } + fn fold_matrix_sum(m: [[G; 2]; 2]) -> G { fold(0 .. 2, 0, |acc_outer, @i| fold(0 .. 2, acc_outer, |acc_inner, @j| @@ -270,6 +274,11 @@ def aiurTestCases : List AiurTestCase := [ .noIO `u8_and_function #[45, 131] #[1], .noIO `u8_or_function #[45, 131] #[175], .noIO `fold_matrix_sum #[1, 2, 3, 4] #[10], + { AiurTestCase.noIO `u32_less_than_function #[300, 500] #[1] with label := "u32_less_than(300,500)" }, + { AiurTestCase.noIO `u32_less_than_function #[500, 300] #[0] with label := "u32_less_than(500,300)" }, + { AiurTestCase.noIO `u32_less_than_function #[500, 500] #[0] with label := "u32_less_than(500,500)" }, + { AiurTestCase.noIO `u32_less_than_function #[0, 1] #[1] with label := "u32_less_than(0,1)" }, + { AiurTestCase.noIO `u32_less_than_function #[0, 0] #[0] with label := "u32_less_than(0,0)" }, ] end diff --git a/Tests/Aiur/RBTreeMap.lean b/Tests/Aiur/RBTreeMap.lean new file mode 100644 index 00000000..fa98e651 --- /dev/null +++ b/Tests/Aiur/RBTreeMap.lean @@ -0,0 +1,18 @@ +module + +public import Tests.Aiur.Common +public import Ix.IxVM.RBTreeMap + +public section + +public def rbTreeMapTestCases : List AiurTestCase := [ + .noIO `rbtree_map_test #[] #[ + 42, + 50, 100, 200, + 999, + 10, 20, 30, 40, 50, + 10, 20, 30, 40, 50, + 200, 300, 400, 500, 600, 700, 800], +] + +end diff --git a/Tests/Main.lean b/Tests/Main.lean index e57732a2..151a46f8 100644 --- a/Tests/Main.lean +++ b/Tests/Main.lean @@ -70,6 +70,11 @@ def ignoredRunners : List (String × IO UInt32) := [ return if r1 == 0 && r2 == 0 then 0 else 1), ("ixvm", do LSpec.lspecIO (.ofList [("ixvm", [mkAiurTests IxVM.ixVM [← serdeNatAddComm]])]) []), + ("rbtree-map", do + IO.println "rbtree-map" + match AiurTestEnv.build (pure IxVM.rbTreeMap) with + | .error e => IO.eprintln s!"RBTreeMap setup failed: {e}"; return 1 + | .ok env => LSpec.lspecEachIO rbTreeMapTestCases fun tc => pure (env.runTestCase tc)), ] def main (args : List String) : IO UInt32 := do diff --git a/src/aiur/bytecode.rs b/src/aiur/bytecode.rs index 1227d2f7..34ef80b1 100644 --- a/src/aiur/bytecode.rs +++ b/src/aiur/bytecode.rs @@ -57,6 +57,7 @@ pub enum Op { U8And(ValIdx, ValIdx), U8Or(ValIdx, ValIdx), U8LessThan(ValIdx, ValIdx), + U32LessThan(ValIdx, ValIdx), Debug(String, Option>), } diff --git a/src/aiur/constraints.rs b/src/aiur/constraints.rs index 46350844..695d27a6 100644 --- a/src/aiur/constraints.rs +++ b/src/aiur/constraints.rs @@ -448,6 +448,125 @@ impl Op { sel.clone(), state, ), + Op::U32LessThan(x_idx, y_idx) => { + // u32 less-than via byte decomposition and subtraction with borrow chain. + // + // Goal: constrain output = 1 if x < y, 0 otherwise, where x and y are + // u32 values (< 2^32) represented as Goldilocks field elements. + // + // Step 1 — Byte decomposition. Decompose x and y into 4 little-endian + // bytes each: + // x = Σ_{k=0}^{3} x_k · 256^k + // y = Σ_{k=0}^{3} y_k · 256^k + // Each byte is range-checked to [0, 255] by appearing as an operand in + // a u8_sub lookup against the Bytes2 preprocessed table. + // + // No canonicality check is needed. Since 2^32 < p, the 4- byte decomposition + // of any field element v is unique iff v < 2^32. If v ≥ 2^32, no 4-byte + // decomposition sums to v in the field, so the decomposition constraint + // is unsatisfiable and the prover simply cannot produce a valid witness. + // This means u32_less_than is only usable on values that actually fit in + // 32 bits; applying it to larger values will cause proof generation to fail. + // + // Step 2 — Borrow-chain subtraction. We compute + // y_int − x_int − 1 + // byte-by-byte using two u8_sub lookups per byte (8 total): + // u8_sub(y_k, x_k) → (t_k, b_k') + // u8_sub(t_k, c_k) → (r_k, b_k'') + // where c_0 = 1 (the −1 offset) and c_k = b_{k−1}' + b_{k−1}'' for k > 0. + // + // The algebraic identity across all 4 bytes gives: + // r_int − 2^32 · b_3 = y_int − x_int − 1 + // where r_int = Σ r_k · 256^k ∈ [0, 2^32−1] and b_3 = b_3' + b_3'' is + // the final borrow. + // + // Step 3 — Soundness of the final borrow. Since x, y < 2^32: + // • y − x − 1 ∈ [−(2^32−1), 2^32 − 2] ⊂ (−2^32, 2^32) + // • r_int ∈ [0, 2^32 − 1] + // So b_3 = (r_int − (y − x − 1)) / 2^32. If b_3 ≥ 2 then + // y − x − 1 = r_int − 2·2^32 ≤ 2^32−1 − 2^33 < −2^32, contradicting the + // lower bound. Hence b_3 ∈ {0, 1}: + // • b_3 = 0 ⟹ y − x − 1 ≥ 0 ⟹ x < y + // • b_3 = 1 ⟹ y − x − 1 < 0 ⟹ x ≥ y + // + // Output: 1 − b_3 = 1 − (b_3' + b_3''). + // + // Resources: 24 auxiliaries (8 bytes + 16 borrow chain), 8 lookups + // (all u8_sub), 2 polynomial constraints (decomposition only). + let x = state.map[*x_idx].0.clone(); + let y = state.map[*y_idx].0.clone(); + + // Byte decomposition: 4 byte auxiliaries per operand + let x_bytes: Vec = + (0..4).map(|_| state.next_auxiliary()).collect(); + let y_bytes: Vec = + (0..4).map(|_| state.next_auxiliary()).collect(); + + // Decomposition constraints: x = Σ xi * 256^i + let x_sum = x_bytes.iter().enumerate().fold( + Expr::Constant(G::ZERO), + |acc, (k, b)| { + acc + b.clone() * G::from_u64(256u64.pow(u32::try_from(k).unwrap())) + }, + ); + state.constraints.zeros.push(sel.clone() * (x - x_sum)); + + let y_sum = y_bytes.iter().enumerate().fold( + Expr::Constant(G::ZERO), + |acc, (k, b)| { + acc + b.clone() * G::from_u64(256u64.pow(u32::try_from(k).unwrap())) + }, + ); + state.constraints.zeros.push(sel.clone() * (y - y_sum)); + + // Borrow chain: y - x - 1 byte-by-byte + let sub_channel = u8_sub_channel(); + let mut prev_borrow: Option = None; + for k in 0..4 { + let t_k = state.next_auxiliary(); + let b_k_prime = state.next_auxiliary(); + let r_k = state.next_auxiliary(); + let b_k_double_prime = state.next_auxiliary(); + + // Lookup 1: u8_sub(y_k, x_k) -> (t_k, b_k') + let lookup = state.next_lookup(); + combine_lookup_args( + lookup, + vec![ + sel.clone() * sub_channel, + sel.clone() * y_bytes[k].clone(), + sel.clone() * x_bytes[k].clone(), + sel.clone() * t_k.clone(), + sel.clone() * b_k_prime.clone(), + ], + ); + lookup.multiplicity += sel.clone(); + + // Lookup 2: u8_sub(t_k, borrow_in) -> (r_k, b_k'') + let borrow_in = match prev_borrow { + None => Expr::Constant(G::ONE), + Some(prev_borrow) => prev_borrow.clone(), + }; + let lookup = state.next_lookup(); + combine_lookup_args( + lookup, + vec![ + sel.clone() * sub_channel, + sel.clone() * t_k, + sel.clone() * borrow_in, + sel.clone() * r_k, + sel.clone() * b_k_double_prime.clone(), + ], + ); + lookup.multiplicity += sel.clone(); + + prev_borrow = Some(b_k_prime + b_k_double_prime); + } + + // Output: 1 - (b_3' + b_3'') + let output = Expr::ONE - prev_borrow.unwrap(); + state.map.push((output, 1)); + }, Op::IOSetInfo(..) | Op::IOWrite(_) | Op::Debug(..) => (), } } diff --git a/src/aiur/execute.rs b/src/aiur/execute.rs index b3b105a8..95b4fb68 100644 --- a/src/aiur/execute.rs +++ b/src/aiur/execute.rs @@ -300,6 +300,35 @@ impl Function { bytes2_execute(*i, *j, &Bytes2Op::LessThan, &mut map, record); } }, + ExecEntry::Op(Op::U32LessThan(x_idx, y_idx)) => { + let x_val = map[*x_idx]; + let y_val = map[*y_idx]; + let x_u32 = + u32::try_from(x_val.as_canonical_u64()).expect("Out of range"); + let y_u32 = + u32::try_from(y_val.as_canonical_u64()).expect("Out of range"); + let result = G::from_bool(x_u32 < y_u32); + map.push(result); + if !unconstrained { + let x_bytes = x_u32.to_le_bytes(); + let y_bytes = y_u32.to_le_bytes(); + let mut prev_borrow: u8 = 0; + for k in 0..4 { + let yk = y_bytes[k]; + let xk = x_bytes[k]; + let (tk, bk_prime_bool) = yk.overflowing_sub(xk); + let bk_prime = u8::from(bk_prime_bool); + let borrow_in = if k == 0 { 1u8 } else { prev_borrow }; + let (_rk, bk_double_prime_bool) = tk.overflowing_sub(borrow_in); + let bk_double_prime = u8::from(bk_double_prime_bool); + record.bytes2_queries.bump_sub(&G::from_u8(yk), &G::from_u8(xk)); + record + .bytes2_queries + .bump_sub(&G::from_u8(tk), &G::from_u8(borrow_in)); + prev_borrow = bk_prime + bk_double_prime; + } + } + }, ExecEntry::Op(Op::Debug(label, idxs)) => match idxs { None => println!("{label}"), Some(idxs) => { diff --git a/src/aiur/gadgets/bytes2.rs b/src/aiur/gadgets/bytes2.rs index ff3b6b6a..ab3eda81 100644 --- a/src/aiur/gadgets/bytes2.rs +++ b/src/aiur/gadgets/bytes2.rs @@ -284,7 +284,7 @@ impl Bytes2Queries { self.bump_multiplicity_for(i, j, 1) } - fn bump_sub(&mut self, i: &G, j: &G) { + pub(crate) fn bump_sub(&mut self, i: &G, j: &G) { self.bump_multiplicity_for(i, j, 2) } diff --git a/src/aiur/trace.rs b/src/aiur/trace.rs index 0338bd61..4cc54520 100644 --- a/src/aiur/trace.rs +++ b/src/aiur/trace.rs @@ -413,6 +413,74 @@ impl Op { let lookup_args = vec![u8_less_than_channel(), i, j, less_than]; slice.push_lookup(index, Lookup::push(G::ONE, lookup_args)); }, + Op::U32LessThan(x_idx, y_idx) => { + let (x, _) = map[*x_idx]; + let (y, _) = map[*y_idx]; + let x_u32 = u32::try_from(x.as_canonical_u64()).unwrap(); + let y_u32 = u32::try_from(y.as_canonical_u64()).unwrap(); + let x_bytes: [u8; 4] = x_u32.to_le_bytes(); + let y_bytes: [u8; 4] = y_u32.to_le_bytes(); + + // Push 8 byte auxiliaries (x then y) + for &b in x_bytes.iter().chain(y_bytes.iter()) { + slice.push_auxiliary(index, G::from_u8(b)); + } + + // Borrow chain auxiliaries and lookups + let sub_channel = u8_sub_channel(); + let mut prev_borrow: u8 = 0; + for k in 0..4 { + let yk = y_bytes[k]; + let xk = x_bytes[k]; + let (tk, bk_prime_bool) = yk.overflowing_sub(xk); + let bk_prime = u8::from(bk_prime_bool); + let borrow_in = if k == 0 { 1u8 } else { prev_borrow }; + let (rk, bk_double_prime_bool) = tk.overflowing_sub(borrow_in); + let bk_double_prime = u8::from(bk_double_prime_bool); + + // Push 4 auxiliaries: t_k, b_k', r_k, b_k'' + slice.push_auxiliary(index, G::from_u8(tk)); + slice.push_auxiliary(index, G::from_bool(bk_prime_bool)); + slice.push_auxiliary(index, G::from_u8(rk)); + slice.push_auxiliary(index, G::from_bool(bk_double_prime_bool)); + + // Lookup 1: u8_sub(y_k, x_k) -> (t_k, b_k') + slice.push_lookup( + index, + Lookup::push( + G::ONE, + vec![ + sub_channel, + G::from_u8(yk), + G::from_u8(xk), + G::from_u8(tk), + G::from_bool(bk_prime_bool), + ], + ), + ); + + // Lookup 2: u8_sub(t_k, borrow_in) -> (r_k, b_k'') + slice.push_lookup( + index, + Lookup::push( + G::ONE, + vec![ + sub_channel, + G::from_u8(tk), + G::from_u8(borrow_in), + G::from_u8(rk), + G::from_bool(bk_double_prime_bool), + ], + ), + ); + + prev_borrow = bk_prime + bk_double_prime; + } + + // Output: 1 - final_borrow + let result = G::from_bool(x_u32 < y_u32); + map.push((result, 1)); + }, Op::AssertEq(..) | Op::IOSetInfo(..) | Op::IOWrite(_) | Op::Debug(..) => { }, } diff --git a/src/ffi/aiur/toplevel.rs b/src/ffi/aiur/toplevel.rs index 88c2d548..083cb147 100644 --- a/src/ffi/aiur/toplevel.rs +++ b/src/ffi/aiur/toplevel.rs @@ -115,6 +115,10 @@ fn decode_op(ctor: LeanCtor) -> Op { Op::U8LessThan(i, j) }, 22 => { + let [i, j] = ctor.objs::<2>().map(lean_unbox_nat_as_usize); + Op::U32LessThan(i, j) + }, + 23 => { let [label_obj, idxs_obj] = ctor.objs::<2>(); let label = label_obj.as_string().to_string(); let idxs = if idxs_obj.is_scalar() {