From 908bb6fc69c5318985016db505375044366355ca Mon Sep 17 00:00:00 2001 From: Gabriel Barreto Date: Sun, 15 Feb 2026 19:07:48 -0300 Subject: [PATCH 1/2] u8 subtraction and less than --- Ix/Aiur/Bytecode.lean | 2 + Ix/Aiur/Check.lean | 2 + Ix/Aiur/Compile.lean | 14 ++- Ix/Aiur/Meta.lean | 14 +++ Ix/Aiur/Term.lean | 4 + src/aiur.rs | 14 ++- src/aiur/bytecode.rs | 2 + src/aiur/constraints.rs | 19 +++- src/aiur/execute.rs | 15 ++++ src/aiur/gadgets/bytes2.rs | 160 ++++++++++++++++++++++++++-------- src/aiur/trace.rs | 25 +++++- src/lean/ffi/aiur/toplevel.rs | 12 ++- 12 files changed, 237 insertions(+), 46 deletions(-) diff --git a/Ix/Aiur/Bytecode.lean b/Ix/Aiur/Bytecode.lean index 69abff49..7fbbec8e 100644 --- a/Ix/Aiur/Bytecode.lean +++ b/Ix/Aiur/Bytecode.lean @@ -27,8 +27,10 @@ inductive Op | u8ShiftRight : ValIdx → Op | u8Xor : ValIdx → ValIdx → Op | u8Add : ValIdx → ValIdx → Op + | u8Sub : ValIdx → ValIdx → Op | u8And : ValIdx → ValIdx → Op | u8Or : ValIdx → ValIdx → Op + | u8LessThan : ValIdx → ValIdx → Op | debug : String → Option (Array ValIdx) → Op deriving Repr diff --git a/Ix/Aiur/Check.lean b/Ix/Aiur/Check.lean index 83e33a51..0b76c57d 100644 --- a/Ix/Aiur/Check.lean +++ b/Ix/Aiur/Check.lean @@ -111,6 +111,8 @@ partial def inferTerm (t : Term) : CheckM TypedTerm := match t with | .u8And a b => inferBinop a b .u8And .field | .u8Or a b => inferBinop a b .u8Or .field | .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 | .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 ffe6a1c4..ef1469f5 100644 --- a/Ix/Aiur/Compile.lean +++ b/Ix/Aiur/Compile.lean @@ -124,10 +124,14 @@ def opLayout : Bytecode.Op → LayoutM Unit pushDegree 1 bumpAuxiliaries 1 bumpLookups - | .u8Add .. => do + | .u8Add .. | .u8Sub .. => do pushDegrees #[1, 1] bumpAuxiliaries 2 bumpLookups + | .u8LessThan .. => do + pushDegree 1 + bumpAuxiliaries 1 + bumpLookups | .debug .. => pure () partial def blockLayout (block : Bytecode.Block) : LayoutM Unit := do @@ -421,6 +425,10 @@ partial def toIndex let i ← expectIdx i let j ← expectIdx j pushOp (.u8Add i j) 2 + | .u8Sub i j => do + let i ← expectIdx i + let j ← expectIdx j + pushOp (.u8Sub i j) 2 | .u8And i j => do let i ← expectIdx i let j ← expectIdx j @@ -429,6 +437,10 @@ partial def toIndex let i ← expectIdx i let j ← expectIdx j pushOp (.u8Or i j) + | .u8LessThan i j => do + let i ← expectIdx i + let j ← expectIdx j + pushOp (.u8LessThan 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 48ad07c5..c68470b2 100644 --- a/Ix/Aiur/Meta.lean +++ b/Ix/Aiur/Meta.lean @@ -123,8 +123,10 @@ syntax "u8_shift_left" "(" trm ")" : trm syntax "u8_shift_right" "(" trm ")" : trm syntax "u8_xor" "(" trm ", " trm ")" : trm syntax "u8_add" "(" trm ", " trm ")" : trm +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 "dbg!" "(" str (", " trm)? ")" ";" (trm)? : trm syntax trm "[" "@" noWs ident "]" : trm @@ -221,10 +223,14 @@ partial def elabTrm : ElabStxCat `trm mkAppM ``Term.u8Xor #[← elabTrm i, ← elabTrm j] | `(trm| u8_add($i:trm, $j:trm)) => do mkAppM ``Term.u8Add #[← elabTrm i, ← elabTrm j] + | `(trm| u8_sub($i:trm, $j:trm)) => do + mkAppM ``Term.u8Sub #[← elabTrm i, ← elabTrm j] | `(trm| u8_and($i:trm, $j:trm)) => do mkAppM ``Term.u8And #[← elabTrm i, ← elabTrm j] | `(trm| u8_or($i:trm, $j:trm)) => do mkAppM ``Term.u8Or #[← elabTrm i, ← elabTrm j] + | `(trm| u8_less_than($i:trm, $j:trm)) => do + mkAppM ``Term.u8LessThan #[← 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)] @@ -366,6 +372,10 @@ where let i ← replaceToken old new i let j ← replaceToken old new j `(trm| u8_add($i, $j)) + | `(trm| u8_sub($i:trm, $j:trm)) => do + let i ← replaceToken old new i + let j ← replaceToken old new j + `(trm| u8_sub($i, $j)) | `(trm| u8_and($i:trm, $j:trm)) => do let i ← replaceToken old new i let j ← replaceToken old new j @@ -374,6 +384,10 @@ where let i ← replaceToken old new i let j ← replaceToken old new j `(trm| u8_or($i, $j)) + | `(trm| u8_less_than($i:trm, $j:trm)) => do + let i ← replaceToken old new i + let j ← replaceToken old new j + `(trm| u8_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 83302c79..71061824 100644 --- a/Ix/Aiur/Term.lean +++ b/Ix/Aiur/Term.lean @@ -93,8 +93,10 @@ inductive Term | u8ShiftRight : Term → Term | u8Xor : Term → Term → Term | u8Add : Term → Term → Term + | u8Sub : Term → Term → Term | u8And : Term → Term → Term | u8Or : Term → Term → Term + | u8LessThan : Term → Term → Term | debug : String → Option Term → Term → Term deriving Repr, BEq, Hashable, Inhabited @@ -138,8 +140,10 @@ inductive TypedTermInner | u8ShiftRight : TypedTerm → TypedTermInner | u8Xor : TypedTerm → TypedTerm → TypedTermInner | u8Add : TypedTerm → TypedTerm → TypedTermInner + | u8Sub : TypedTerm → TypedTerm → TypedTermInner | u8And : TypedTerm → TypedTerm → TypedTermInner | u8Or : TypedTerm → TypedTerm → TypedTermInner + | u8LessThan : TypedTerm → TypedTerm → TypedTermInner | debug : String → Option TypedTerm → TypedTerm → TypedTermInner deriving Repr, Inhabited diff --git a/src/aiur.rs b/src/aiur.rs index 26e49bb9..afe02ffe 100644 --- a/src/aiur.rs +++ b/src/aiur.rs @@ -46,11 +46,21 @@ pub fn u8_add_channel() -> G { } #[inline] -pub fn u8_and_channel() -> G { +pub fn u8_sub_channel() -> G { G::from_u8(7) } #[inline] -pub fn u8_or_channel() -> G { +pub fn u8_and_channel() -> G { G::from_u8(8) } + +#[inline] +pub fn u8_or_channel() -> G { + G::from_u8(9) +} + +#[inline] +pub fn u8_less_than_channel() -> G { + G::from_u8(10) +} diff --git a/src/aiur/bytecode.rs b/src/aiur/bytecode.rs index 43331947..1227d2f7 100644 --- a/src/aiur/bytecode.rs +++ b/src/aiur/bytecode.rs @@ -53,8 +53,10 @@ pub enum Op { U8ShiftRight(ValIdx), U8Xor(ValIdx, ValIdx), U8Add(ValIdx, ValIdx), + U8Sub(ValIdx, ValIdx), U8And(ValIdx, ValIdx), U8Or(ValIdx, ValIdx), + U8LessThan(ValIdx, ValIdx), Debug(String, Option>), } diff --git a/src/aiur/constraints.rs b/src/aiur/constraints.rs index 9c1252dd..46350844 100644 --- a/src/aiur/constraints.rs +++ b/src/aiur/constraints.rs @@ -17,7 +17,8 @@ use crate::aiur::{ bytes2::{Bytes2, Bytes2Op}, }, memory_channel, u8_add_channel, u8_and_channel, u8_bit_decomposition_channel, - u8_or_channel, u8_shift_left_channel, u8_shift_right_channel, u8_xor_channel, + u8_less_than_channel, u8_or_channel, u8_shift_left_channel, + u8_shift_right_channel, u8_sub_channel, u8_xor_channel, }; type Expr = SymbolicExpression; @@ -415,6 +416,14 @@ impl Op { sel.clone(), state, ), + Op::U8Sub(i, j) => bytes2_constraints( + *i, + *j, + &Bytes2Op::Sub, + u8_sub_channel(), + sel.clone(), + state, + ), Op::U8And(i, j) => bytes2_constraints( *i, *j, @@ -431,6 +440,14 @@ impl Op { sel.clone(), state, ), + Op::U8LessThan(i, j) => bytes2_constraints( + *i, + *j, + &Bytes2Op::LessThan, + u8_less_than_channel(), + sel.clone(), + state, + ), Op::IOSetInfo(..) | Op::IOWrite(_) | Op::Debug(..) => (), } } diff --git a/src/aiur/execute.rs b/src/aiur/execute.rs index 8030f5b0..b3b105a8 100644 --- a/src/aiur/execute.rs +++ b/src/aiur/execute.rs @@ -271,6 +271,14 @@ impl Function { bytes2_execute(*i, *j, &Bytes2Op::Add, &mut map, record); } }, + ExecEntry::Op(Op::U8Sub(i, j)) => { + if unconstrained { + let (r, u) = Bytes2::sub(&map[*i], &map[*j]); + map.extend([r, u]); + } else { + bytes2_execute(*i, *j, &Bytes2Op::Sub, &mut map, record); + } + }, ExecEntry::Op(Op::U8And(i, j)) => { if unconstrained { map.push(Bytes2::and(&map[*i], &map[*j])); @@ -285,6 +293,13 @@ impl Function { bytes2_execute(*i, *j, &Bytes2Op::Or, &mut map, record); } }, + ExecEntry::Op(Op::U8LessThan(i, j)) => { + if unconstrained { + map.push(Bytes2::less_than(&map[*i], &map[*j])); + } else { + bytes2_execute(*i, *j, &Bytes2Op::LessThan, &mut map, record); + } + }, 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 03a39a23..ff3b6b6a 100644 --- a/src/aiur/gadgets/bytes2.rs +++ b/src/aiur/gadgets/bytes2.rs @@ -8,15 +8,17 @@ use multi_stark::{ use crate::aiur::{ G, execute::QueryRecord, gadgets::AiurGadget, u8_add_channel, u8_and_channel, - u8_or_channel, u8_xor_channel, + u8_less_than_channel, u8_or_channel, u8_sub_channel, u8_xor_channel, }; /// Number of columns in the trace with multiplicities for /// - xor /// - overflowing add +/// - overflowing sub /// - and /// - or -const TRACE_WIDTH: usize = 4; +/// - less_than +const TRACE_WIDTH: usize = 6; /// Number of columns in the preprocessed trace: /// - first raw byte value @@ -24,9 +26,12 @@ const TRACE_WIDTH: usize = 4; /// - xor result /// - add result /// - add overflow +/// - sub result +/// - sub underflow /// - and result /// - or result -const PREPROCESSED_TRACE_WIDTH: usize = 7; +/// - less_than result +const PREPROCESSED_TRACE_WIDTH: usize = 10; /// AIR implementer for arity 2 byte-related lookups. pub(crate) struct Bytes2; @@ -34,8 +39,10 @@ pub(crate) struct Bytes2; pub(crate) enum Bytes2Op { Xor, Add, + Sub, And, Or, + LessThan, } impl BaseAir for Bytes2 { @@ -61,11 +68,19 @@ impl BaseAir for Bytes2 { trace_values.push(G::from_u8(r)); trace_values.push(G::from_bool(o)); + // Overflowing sub + let (r, u) = i.overflowing_sub(j); + trace_values.push(G::from_u8(r)); + trace_values.push(G::from_bool(u)); + // And trace_values.push(G::from_u8(i & j)); // Or trace_values.push(G::from_u8(i | j)); + + // Less than + trace_values.push(G::from_bool(i < j)); } } Some(RowMajorMatrix::new(trace_values, PREPROCESSED_TRACE_WIDTH)) @@ -82,8 +97,8 @@ impl AiurGadget for Bytes2 { fn output_size(&self, op: &Bytes2Op) -> usize { match op { - Bytes2Op::Xor | Bytes2Op::And | Bytes2Op::Or => 1, - Bytes2Op::Add => 2, + Bytes2Op::Xor | Bytes2Op::And | Bytes2Op::Or | Bytes2Op::LessThan => 1, + Bytes2Op::Add | Bytes2Op::Sub => 2, } } @@ -105,6 +120,11 @@ impl AiurGadget for Bytes2 { let (r, o) = Self::add(i, j); vec![r, o] }, + Bytes2Op::Sub => { + record.bytes2_queries.bump_sub(i, j); + let (r, u) = Self::sub(i, j); + vec![r, u] + }, Bytes2Op::And => { record.bytes2_queries.bump_and(i, j); vec![Self::and(i, j)] @@ -113,6 +133,10 @@ impl AiurGadget for Bytes2 { record.bytes2_queries.bump_or(i, j); vec![Self::or(i, j)] }, + Bytes2Op::LessThan => { + record.bytes2_queries.bump_less_than(i, j); + vec![Self::less_than(i, j)] + }, } } @@ -120,14 +144,18 @@ impl AiurGadget for Bytes2 { // Channels let xor_channel = u8_xor_channel().into(); let add_channel = u8_add_channel().into(); + let sub_channel = u8_sub_channel().into(); let and_channel = u8_and_channel().into(); let or_channel = u8_or_channel().into(); + let less_than_channel = u8_less_than_channel().into(); // Multiplicity columns let xor_multiplicity = var(0); let add_multiplicity = var(1); - let and_multiplicity = var(2); - let or_multiplicity = var(3); + let sub_multiplicity = var(2); + let and_multiplicity = var(3); + let or_multiplicity = var(4); + let less_than_multiplicity = var(5); // Preprocessed columns let i = preprocessed_var(0); @@ -135,8 +163,11 @@ impl AiurGadget for Bytes2 { let xor = preprocessed_var(2); let add_r = preprocessed_var(3); let add_o = preprocessed_var(4); - let and = preprocessed_var(5); - let or = preprocessed_var(6); + let sub_r = preprocessed_var(5); + let sub_u = preprocessed_var(6); + let and = preprocessed_var(7); + let or = preprocessed_var(8); + let less_than = preprocessed_var(9); let pull_xor = Lookup::pull( xor_multiplicity, @@ -148,14 +179,25 @@ impl AiurGadget for Bytes2 { vec![add_channel, i.clone(), j.clone(), add_r, add_o], ); + let pull_sub = Lookup::pull( + sub_multiplicity, + vec![sub_channel, i.clone(), j.clone(), sub_r, sub_u], + ); + let pull_and = Lookup::pull( and_multiplicity, vec![and_channel, i.clone(), j.clone(), and], ); - let pull_or = Lookup::pull(or_multiplicity, vec![or_channel, i, j, or]); + let pull_or = + Lookup::pull(or_multiplicity, vec![or_channel, i.clone(), j.clone(), or]); - vec![pull_xor, pull_add, pull_and, pull_or] + let pull_less_than = Lookup::pull( + less_than_multiplicity, + vec![less_than_channel, i, j, less_than], + ); + + vec![pull_xor, pull_add, pull_sub, pull_and, pull_or, pull_less_than] } fn witness_data( @@ -169,39 +211,58 @@ impl AiurGadget for Bytes2 { let xor_channel = u8_xor_channel(); let add_channel = u8_add_channel(); + let sub_channel = u8_sub_channel(); let and_channel = u8_and_channel(); let or_channel = u8_or_channel(); + let less_than_channel = u8_less_than_channel(); rows .chunks_exact_mut(TRACE_WIDTH) .enumerate() .zip(&record.bytes2_queries.0) .zip(&mut lookups) - .for_each(|(((row_idx, row), &[xor, add, and, or]), row_lookups)| { - let i = G::from_usize(row_idx / 256); - let j = G::from_usize(row_idx % 256); - - row[0] = xor; - row[1] = add; - row[2] = and; - row[3] = or; - - // Pull xor. - row_lookups[0] = - Lookup::pull(xor, vec![xor_channel, i, j, Self::xor(&i, &j)]); - - // Pull add. - let (r, o) = Self::add(&i, &j); - row_lookups[1] = Lookup::pull(add, vec![add_channel, i, j, r, o]); - - // Pull and. - row_lookups[2] = - Lookup::pull(and, vec![and_channel, i, j, Self::and(&i, &j)]); - - // Pull or. - row_lookups[3] = - Lookup::pull(or, vec![or_channel, i, j, Self::or(&i, &j)]); - }); + .for_each( + |( + ((row_idx, row), &[xor, add, sub, and, or, less_than]), + row_lookups, + )| { + let i = G::from_usize(row_idx / 256); + let j = G::from_usize(row_idx % 256); + + row[0] = xor; + row[1] = add; + row[2] = sub; + row[3] = and; + row[4] = or; + row[5] = less_than; + + // Pull xor. + row_lookups[0] = + Lookup::pull(xor, vec![xor_channel, i, j, Self::xor(&i, &j)]); + + // Pull add. + let (r, o) = Self::add(&i, &j); + row_lookups[1] = Lookup::pull(add, vec![add_channel, i, j, r, o]); + + // Pull sub. + let (r, u) = Self::sub(&i, &j); + row_lookups[2] = Lookup::pull(sub, vec![sub_channel, i, j, r, u]); + + // Pull and. + row_lookups[3] = + Lookup::pull(and, vec![and_channel, i, j, Self::and(&i, &j)]); + + // Pull or. + row_lookups[4] = + Lookup::pull(or, vec![or_channel, i, j, Self::or(&i, &j)]); + + // Pull less_than. + row_lookups[5] = Lookup::pull( + less_than, + vec![less_than_channel, i, j, Self::less_than(&i, &j)], + ); + }, + ); (RowMajorMatrix::new(rows, TRACE_WIDTH), lookups) } } @@ -223,14 +284,22 @@ impl Bytes2Queries { self.bump_multiplicity_for(i, j, 1) } - fn bump_and(&mut self, i: &G, j: &G) { + fn bump_sub(&mut self, i: &G, j: &G) { self.bump_multiplicity_for(i, j, 2) } - fn bump_or(&mut self, i: &G, j: &G) { + fn bump_and(&mut self, i: &G, j: &G) { self.bump_multiplicity_for(i, j, 3) } + fn bump_or(&mut self, i: &G, j: &G) { + self.bump_multiplicity_for(i, j, 4) + } + + fn bump_less_than(&mut self, i: &G, j: &G) { + self.bump_multiplicity_for(i, j, 5) + } + fn bump_multiplicity_for(&mut self, i: &G, j: &G, col: usize) { let i = usize::try_from(i.as_canonical_u64()).unwrap(); let j = usize::try_from(j.as_canonical_u64()).unwrap(); @@ -268,4 +337,19 @@ impl Bytes2 { let j: u8 = j.as_canonical_u64().try_into().unwrap(); G::from_u8(i | j) } + + #[inline] + pub(crate) fn sub(i: &G, j: &G) -> (G, G) { + let i: u8 = i.as_canonical_u64().try_into().unwrap(); + let j: u8 = j.as_canonical_u64().try_into().unwrap(); + let (r, u) = i.overflowing_sub(j); + (G::from_u8(r), G::from_bool(u)) + } + + #[inline] + pub(crate) fn less_than(i: &G, j: &G) -> G { + let i: u8 = i.as_canonical_u64().try_into().unwrap(); + let j: u8 = j.as_canonical_u64().try_into().unwrap(); + G::from_bool(i < j) + } } diff --git a/src/aiur/trace.rs b/src/aiur/trace.rs index 239b7862..0338bd61 100644 --- a/src/aiur/trace.rs +++ b/src/aiur/trace.rs @@ -17,8 +17,9 @@ use crate::aiur::{ function_channel, gadgets::{bytes1::Bytes1, bytes2::Bytes2}, memory::Memory, - u8_add_channel, u8_and_channel, u8_bit_decomposition_channel, u8_or_channel, - u8_shift_left_channel, u8_shift_right_channel, u8_xor_channel, + u8_add_channel, u8_and_channel, u8_bit_decomposition_channel, + u8_less_than_channel, u8_or_channel, u8_shift_left_channel, + u8_shift_right_channel, u8_sub_channel, u8_xor_channel, }; struct ColumnIndex { @@ -374,6 +375,17 @@ impl Op { let lookup_args = vec![u8_add_channel(), i, j, r, o]; slice.push_lookup(index, Lookup::push(G::ONE, lookup_args)); }, + Op::U8Sub(i, j) => { + let (i, _) = map[*i]; + let (j, _) = map[*j]; + let (r, u) = Bytes2::sub(&i, &j); + map.push((r, 1)); + map.push((u, 1)); + slice.push_auxiliary(index, r); + slice.push_auxiliary(index, u); + let lookup_args = vec![u8_sub_channel(), i, j, r, u]; + slice.push_lookup(index, Lookup::push(G::ONE, lookup_args)); + }, Op::U8And(i, j) => { let (i, _) = map[*i]; let (j, _) = map[*j]; @@ -392,6 +404,15 @@ impl Op { let lookup_args = vec![u8_or_channel(), i, j, or]; slice.push_lookup(index, Lookup::push(G::ONE, lookup_args)); }, + Op::U8LessThan(i, j) => { + let (i, _) = map[*i]; + let (j, _) = map[*j]; + let less_than = Bytes2::less_than(&i, &j); + map.push((less_than, 1)); + slice.push_auxiliary(index, less_than); + let lookup_args = vec![u8_less_than_channel(), i, j, less_than]; + slice.push_lookup(index, Lookup::push(G::ONE, lookup_args)); + }, Op::AssertEq(..) | Op::IOSetInfo(..) | Op::IOWrite(_) | Op::Debug(..) => { }, } diff --git a/src/lean/ffi/aiur/toplevel.rs b/src/lean/ffi/aiur/toplevel.rs index 8789665e..96c8d27b 100644 --- a/src/lean/ffi/aiur/toplevel.rs +++ b/src/lean/ffi/aiur/toplevel.rs @@ -118,13 +118,21 @@ fn lean_ptr_to_op(ptr: *const c_void) -> Op { }, 18 => { let [i, j] = ctor.objs().map(lean_unbox_nat_as_usize); - Op::U8And(i, j) + Op::U8Sub(i, j) }, 19 => { let [i, j] = ctor.objs().map(lean_unbox_nat_as_usize); - Op::U8Or(i, j) + Op::U8And(i, j) }, 20 => { + let [i, j] = ctor.objs().map(lean_unbox_nat_as_usize); + Op::U8Or(i, j) + }, + 21 => { + let [i, j] = ctor.objs().map(lean_unbox_nat_as_usize); + Op::U8LessThan(i, j) + }, + 22 => { let [label_ptr, idxs_ptr] = ctor.objs(); let label_str: &LeanStringObject = as_ref_unsafe(label_ptr.cast()); let label = label_str.as_string(); From cb5fa9c68757b4bc4d4f800467e4fa5cda1f8088 Mon Sep 17 00:00:00 2001 From: Gabriel Barreto Date: Sun, 15 Feb 2026 19:19:14 -0300 Subject: [PATCH 2/2] aiur tests --- Tests/Aiur.lean | 18 ++++++++++++++---- Tests/Main.lean | 2 ++ 2 files changed, 16 insertions(+), 4 deletions(-) diff --git a/Tests/Aiur.lean b/Tests/Aiur.lean index 7a1aa741..130cba67 100644 --- a/Tests/Aiur.lean +++ b/Tests/Aiur.lean @@ -199,11 +199,19 @@ def toplevel := ⟦ (u8_add(i_xor_j, i), u8_add(i_xor_j, j)) } - fn u8_add_and(i: G, j: G) -> G { + fn u8_sub_function(i: G, j: G) -> (G, G) { + u8_sub(i, j) + } + + fn u8_less_than_function(i: G, j: G) -> G { + u8_less_than(i, j) + } + + fn u8_and_function(i: G, j: G) -> G { u8_and(i, j) } - fn u8_add_or(i: G, j: G) -> G { + fn u8_or_function(i: G, j: G) -> G { u8_or(i, j) } @@ -253,8 +261,10 @@ def aiurTestCases : List AiurTestCase := [ ⟨#[1, 2, 3, 4, 1, 2, 3, 4], .ofList [(#[0], ⟨0, 4⟩), (#[1], ⟨0, 8⟩)]⟩⟩, .noIO `shr_shr_shl_decompose #[87] #[0, 1, 0, 1, 0, 1, 0, 0], .noIO `u8_add_xor #[45, 131] #[219, 0, 49, 1], - .noIO `u8_add_and #[45, 131] #[1], - .noIO `u8_add_or #[45, 131] #[175], + .noIO `u8_sub_function #[45, 131] #[170, 1], + .noIO `u8_less_than_function #[45, 131] #[1], + .noIO `u8_and_function #[45, 131] #[1], + .noIO `u8_or_function #[45, 131] #[175], .noIO `fold_matrix_sum #[1, 2, 3, 4] #[10], ] diff --git a/Tests/Main.lean b/Tests/Main.lean index e25300a8..d7f574ee 100644 --- a/Tests/Main.lean +++ b/Tests/Main.lean @@ -1,3 +1,4 @@ +import Tests.Aiur import Tests.ByteArray import Tests.Ix.Ixon import Tests.Ix.Claim @@ -22,6 +23,7 @@ opaque tmpDecodeConstMap : @& List (Lean.Name × Lean.ConstantInfo) → USize /-- Primary test suites - run by default -/ def primarySuites : Std.HashMap String (List LSpec.TestSeq) := .ofList [ + ("aiur", Tests.Aiur.suite), ("ffi", Tests.FFI.suite), ("byte-array", Tests.ByteArray.suite), ("ixon", Tests.Ixon.suite),