U8 subtraction and less than

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
 

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

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) }

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

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
 

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],
   ]
 

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),

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)
+}

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<Vec<ValIdx>>),
 }
 

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<G>;
@@ -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(..) => (),
     }
   }

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) => {