Skip to content

Aiur kernel: u8_mul gadget + multiplication/arithmetic cleanups #410

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
arthurpaulino wants to merge 5 commits into
base: main
Choose a base branch
from
Open

Aiur kernel: u8_mul gadget + multiplication/arithmetic cleanups #410

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
7d28c2e
perf(kernel): boolean-inversion opt + dedup u64_add
arthurpaulino May 15, 2026
6cae736
feat(aiur): add u8_mul gadget
arthurpaulino May 15, 2026
091881b
perf(kernel): use u8_mul gadget in u64_mul, shrink divmod_256
arthurpaulino May 15, 2026
2152020
perf(kernel): u64_mul via unconstrained carry witness
arthurpaulino May 16, 2026
11f6f45
perf(kernel): klimbs_from_g via unconstrained byte witness
arthurpaulino May 16, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 5 additions & 0 deletions Ix/Aiur/Compiler/Check.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -735,6 +735,10 @@ def inferTerm (t : Term) : CheckM Typed.Term := match t with
let a' ← checkNoEscape a .field
let b' ← checkNoEscape b .field
pure (Typed.Term.u8Add (.tuple #[.field, .field]) false a' b')
| .u8Mul a b => do
let a' ← checkNoEscape a .field
let b' ← checkNoEscape b .field
pure (Typed.Term.u8Mul (.tuple #[.field, .field]) false a' b')
| .u8Sub a b => do
let a' ← checkNoEscape a .field
let b' ← checkNoEscape b .field
Expand Down Expand Up @@ -900,6 +904,7 @@ def zonkTypedTerm (t : Typed.Term) : CheckM Typed.Term := match t with
| .u8ShiftRight τ e a => do pure (.u8ShiftRight (← zonkTyp τ) e (← zonkTypedTerm a))
| .u8Xor τ e a b => do pure (.u8Xor (← zonkTyp τ) e (← zonkTypedTerm a) (← zonkTypedTerm b))
| .u8Add τ e a b => do pure (.u8Add (← zonkTyp τ) e (← zonkTypedTerm a) (← zonkTypedTerm b))
| .u8Mul τ e a b => do pure (.u8Mul (← zonkTyp τ) e (← zonkTypedTerm a) (← zonkTypedTerm b))
| .u8Sub τ e a b => do pure (.u8Sub (← zonkTyp τ) e (← zonkTypedTerm a) (← zonkTypedTerm b))
| .u8And τ e a b => do pure (.u8And (← zonkTyp τ) e (← zonkTypedTerm a) (← zonkTypedTerm b))
| .u8Or τ e a b => do pure (.u8Or (← zonkTyp τ) e (← zonkTypedTerm a) (← zonkTypedTerm b))
Expand Down
11 changes: 9 additions & 2 deletions Ix/Aiur/Compiler/Concretize.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -325,6 +325,9 @@ def termToConcrete
| .u8Add τ e a b => do
pure (.u8Add (← typToConcrete mono τ) e
(← termToConcrete mono a) (← termToConcrete mono b))
| .u8Mul τ e a b => do
pure (.u8Mul (← typToConcrete mono τ) e
(← termToConcrete mono a) (← termToConcrete mono b))
| .u8Sub τ e a b => do
pure (.u8Sub (← typToConcrete mono τ) e
(← termToConcrete mono a) (← termToConcrete mono b))
Expand Down Expand Up @@ -521,6 +524,8 @@ def rewriteTypedTerm (decls : Typed.Decls)
(rewriteTypedTerm decls subst mono a) (rewriteTypedTerm decls subst mono b)
| .u8Add τ e a b => .u8Add (rewriteTyp subst mono τ) e
(rewriteTypedTerm decls subst mono a) (rewriteTypedTerm decls subst mono b)
| .u8Mul τ e a b => .u8Mul (rewriteTyp subst mono τ) e
(rewriteTypedTerm decls subst mono a) (rewriteTypedTerm decls subst mono b)
| .u8Sub τ e a b => .u8Sub (rewriteTyp subst mono τ) e
(rewriteTypedTerm decls subst mono a) (rewriteTypedTerm decls subst mono b)
| .u8And τ e a b => .u8And (rewriteTyp subst mono τ) e
Expand Down Expand Up @@ -597,7 +602,7 @@ def collectInTypedTerm (seen : Std.HashSet (Global × Array Typ)) :
let seen := tArgs.foldl collectInTyp seen
args.attach.foldl (fun s ⟨a, _⟩ => collectInTypedTerm s a) seen
| .add τ _ a b | .sub τ _ a b | .mul τ _ a b
| .u8Xor τ _ a b | .u8Add τ _ a b | .u8Sub τ _ a b
| .u8Xor τ _ a b | .u8Add τ _ a b | .u8Mul τ _ a b | .u8Sub τ _ a b
| .u8And τ _ a b | .u8Or τ _ a b
| .u8LessThan τ _ a b | .u32LessThan τ _ a b =>
collectInTypedTerm (collectInTypedTerm (collectInTyp seen τ) a) b
Expand Down Expand Up @@ -659,7 +664,7 @@ def collectCalls (decls : Typed.Decls)
let seen := collectCalls decls seen scrut
bs.attach.foldl (fun s ⟨(_, b), _⟩ => collectCalls decls s b) seen
| .add _ _ a b | .sub _ _ a b | .mul _ _ a b
| .u8Xor _ _ a b | .u8Add _ _ a b | .u8Sub _ _ a b
| .u8Xor _ _ a b | .u8Add _ _ a b | .u8Mul _ _ a b | .u8Sub _ _ a b
| .u8And _ _ a b | .u8Or _ _ a b
| .u8LessThan _ _ a b | .u32LessThan _ _ a b =>
collectCalls decls (collectCalls decls seen a) b
Expand Down Expand Up @@ -749,6 +754,8 @@ def substInTypedTerm (subst : Global → Option Typ) : Typed.Term → Typed.Term
(substInTypedTerm subst a) (substInTypedTerm subst b)
| .u8Add τ e a b => .u8Add (Typ.instantiate subst τ) e
(substInTypedTerm subst a) (substInTypedTerm subst b)
| .u8Mul τ e a b => .u8Mul (Typ.instantiate subst τ) e
(substInTypedTerm subst a) (substInTypedTerm subst b)
| .u8Sub τ e a b => .u8Sub (Typ.instantiate subst τ) e
(substInTypedTerm subst a) (substInTypedTerm subst b)
| .u8And τ e a b => .u8And (Typ.instantiate subst τ) e
Expand Down
2 changes: 1 addition & 1 deletion Ix/Aiur/Compiler/Layout.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -185,7 +185,7 @@ def opLayout : Bytecode.Op → LayoutM Unit
| .u8BitDecomposition _ => do pushDegrees $ .replicate 8 1; bumpAuxiliaries 8; bumpLookups
| .u8ShiftLeft _ | .u8ShiftRight _ | .u8Xor .. | .u8And .. | .u8Or .. => do
pushDegree 1; bumpAuxiliaries; bumpLookups
| .u8Add .. | .u8Sub .. => do pushDegrees #[1, 1]; bumpAuxiliaries 2; bumpLookups
| .u8Add .. | .u8Mul .. | .u8Sub .. => do pushDegrees #[1, 1]; bumpAuxiliaries 2; bumpLookups
| .u8LessThan .. => do pushDegree 1; bumpAuxiliaries; bumpLookups
| .u32LessThan .. => do pushDegree 1; bumpAuxiliaries 12; bumpLookups 6
| .debug .. => pure ()
Expand Down
3 changes: 3 additions & 0 deletions Ix/Aiur/Compiler/Lower.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -283,6 +283,9 @@ def toIndex
| .u8Add _ _ i j => do
let i ← expectIdx layoutMap bindings i; let j ← expectIdx layoutMap bindings j
pushOp (.u8Add i j) 2
| .u8Mul _ _ i j => do
let i ← expectIdx layoutMap bindings i; let j ← expectIdx layoutMap bindings j
pushOp (.u8Mul i j) 2
| .u8Sub _ _ i j => do
let i ← expectIdx layoutMap bindings i; let j ← expectIdx layoutMap bindings j
pushOp (.u8Sub i j) 2
Expand Down
1 change: 1 addition & 0 deletions Ix/Aiur/Compiler/Match.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -380,6 +380,7 @@ def typedToSimple : Term → Simple.Term
| .u8ShiftRight τ e a => .u8ShiftRight τ e (typedToSimple a)
| .u8Xor τ e a b => .u8Xor τ e (typedToSimple a) (typedToSimple b)
| .u8Add τ e a b => .u8Add τ e (typedToSimple a) (typedToSimple b)
| .u8Mul τ e a b => .u8Mul τ e (typedToSimple a) (typedToSimple b)
| .u8Sub τ e a b => .u8Sub τ e (typedToSimple a) (typedToSimple b)
| .u8And τ e a b => .u8And τ e (typedToSimple a) (typedToSimple b)
| .u8Or τ e a b => .u8Or τ e (typedToSimple a) (typedToSimple b)
Expand Down
4 changes: 4 additions & 0 deletions Ix/Aiur/Goldilocks.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -56,6 +56,10 @@ def G.u8LessThan (a b : G) : G := if a.n < b.n then 1 else 0
def G.u8Add (a b : G) : G × G :=
(G.ofNat ((a.n + b.n) % 256), G.ofNat ((a.n + b.n) / 256))

/-- u8 multiplication returns `(low byte, high byte)`. -/
def G.u8Mul (a b : G) : G × G :=
(G.ofNat ((a.n * b.n) % 256), G.ofNat ((a.n * b.n) / 256))

/-- u8 subtraction returns `(result % 256, borrow)`. -/
def G.u8Sub (a b : G) : G × G :=
(G.ofNat ((a.n + 256 - b.n) % 256), if a.n < b.n then 1 else 0)
Expand Down
8 changes: 8 additions & 0 deletions Ix/Aiur/Interpret.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -326,6 +326,14 @@ partial def interp (decls : Decls) (bindings : Bindings) : Term → InterpM Valu
let overflow : Value := .field (if x >= 256 then 1 else 0)
return .tuple #[sum, overflow]
| _, _ => throwErr "u8Add: expected field values"
| .u8Mul t1 t2 => do
match (← interp decls bindings t1), (← interp decls bindings t2) with
| .field a, .field b =>
let x := a.val.toUInt8.toNat * b.val.toUInt8.toNat
let lo : Value := .field (G.ofUInt8 x.toUInt8)
let hi : Value := .field (G.ofUInt8 (x / 256).toUInt8)
return .tuple #[lo, hi]
| _, _ => throwErr "u8Mul: expected field values"
| .u8Sub t1 t2 => do
match (← interp decls bindings t1), (← interp decls bindings t2) with
| .field a, .field b =>
Expand Down
7 changes: 7 additions & 0 deletions Ix/Aiur/Meta.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -173,6 +173,7 @@ syntax "u8_shift_left" "(" aiur_trm ")" : a
syntax "u8_shift_right" "(" aiur_trm ")" : aiur_trm
syntax "u8_xor" "(" aiur_trm ", " aiur_trm ")" : aiur_trm
syntax "u8_add" "(" aiur_trm ", " aiur_trm ")" : aiur_trm
syntax "u8_mul" "(" aiur_trm ", " aiur_trm ")" : aiur_trm
syntax "u8_sub" "(" aiur_trm ", " aiur_trm ")" : aiur_trm
syntax "u8_and" "(" aiur_trm ", " aiur_trm ")" : aiur_trm
syntax "u8_or" "(" aiur_trm ", " aiur_trm ")" : aiur_trm
Expand Down Expand Up @@ -292,6 +293,8 @@ partial def elabTrm : ElabStxCat `aiur_trm
mkAppM ``Source.Term.u8Xor #[← elabTrm i, ← elabTrm j]
| `(aiur_trm| u8_add($i:aiur_trm, $j:aiur_trm)) => do
mkAppM ``Source.Term.u8Add #[← elabTrm i, ← elabTrm j]
| `(aiur_trm| u8_mul($i:aiur_trm, $j:aiur_trm)) => do
mkAppM ``Source.Term.u8Mul #[← elabTrm i, ← elabTrm j]
| `(aiur_trm| u8_sub($i:aiur_trm, $j:aiur_trm)) => do
mkAppM ``Source.Term.u8Sub #[← elabTrm i, ← elabTrm j]
| `(aiur_trm| u8_and($i:aiur_trm, $j:aiur_trm)) => do
Expand Down Expand Up @@ -480,6 +483,10 @@ where
let i ← replaceToken old new i
let j ← replaceToken old new j
`(aiur_trm| u8_add($i, $j))
| `(aiur_trm| u8_mul($i:aiur_trm, $j:aiur_trm)) => do
let i ← replaceToken old new i
let j ← replaceToken old new j
`(aiur_trm| u8_mul($i, $j))
| `(aiur_trm| u8_sub($i:aiur_trm, $j:aiur_trm)) => do
let i ← replaceToken old new i
let j ← replaceToken old new j
Expand Down
5 changes: 5 additions & 0 deletions Ix/Aiur/Semantics/BytecodeEval.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -247,6 +247,11 @@ def evalOp (t : Bytecode.Toplevel) (fuel : Nat) (op : Op) (st : EvalState) :
let sum := x.val.toUInt8.toNat + y.val.toUInt8.toNat
let st1 := pushMap st (G.ofUInt8 sum.toUInt8)
pure (pushMap st1 (if sum ≥ 256 then 1 else 0))
| .u8Mul a b => do
let x ← readIdx st a; let y ← readIdx st b
let prod := x.val.toUInt8.toNat * y.val.toUInt8.toNat
let st1 := pushMap st (G.ofUInt8 prod.toUInt8)
pure (pushMap st1 (G.ofUInt8 (prod / 256).toUInt8))
| .u8Sub a b => do
let x ← readIdx st a; let y ← readIdx st b
let i := x.val.toUInt8; let j := y.val.toUInt8
Expand Down
8 changes: 8 additions & 0 deletions Ix/Aiur/Semantics/SourceEval.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -382,6 +382,14 @@ def interp (decls : Decls) (fuel : Nat) (bindings : Bindings)
.field (if x >= 256 then 1 else 0)])
(interp decls fuel bindings t1 st)
(fun st1 => interp decls fuel bindings t2 st1)
| .u8Mul t1 t2 =>
combineFieldsResult
(fun a b =>
let x := a.val.toUInt8.toNat * b.val.toUInt8.toNat
.tuple #[.field (G.ofUInt8 x.toUInt8),
.field (G.ofUInt8 (x / 256).toUInt8)])
(interp decls fuel bindings t1 st)
(fun st1 => interp decls fuel bindings t2 st1)
| .u8Sub t1 t2 =>
combineFieldsResult
(fun a b =>
Expand Down
1 change: 1 addition & 0 deletions Ix/Aiur/Stages/Bytecode.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -37,6 +37,7 @@ inductive Op
| u8ShiftRight : ValIdx → Op
| u8Xor : ValIdx → ValIdx → Op
| u8Add : ValIdx → ValIdx → Op
| u8Mul : ValIdx → ValIdx → Op
| u8Sub : ValIdx → ValIdx → Op
| u8And : ValIdx → ValIdx → Op
| u8Or : ValIdx → ValIdx → Op
Expand Down
5 changes: 3 additions & 2 deletions Ix/Aiur/Stages/Concrete.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -78,6 +78,7 @@ inductive Term : Type where
| u8ShiftRight (typ : Typ) (escapes : Bool) (a : Term) : Term
| u8Xor (typ : Typ) (escapes : Bool) (a : Term) (b : Term) : Term
| u8Add (typ : Typ) (escapes : Bool) (a : Term) (b : Term) : Term
| u8Mul (typ : Typ) (escapes : Bool) (a : Term) (b : Term) : Term
| u8Sub (typ : Typ) (escapes : Bool) (a : Term) (b : Term) : Term
| u8And (typ : Typ) (escapes : Bool) (a : Term) (b : Term) : Term
| u8Or (typ : Typ) (escapes : Bool) (a : Term) (b : Term) : Term
Expand All @@ -98,7 +99,7 @@ def Term.typ : Term → Typ
| .assertEq t _ _ _ _ | .ioGetInfo t _ _ | .ioSetInfo t _ _ _ _ _
| .ioRead t _ _ _ | .ioWrite t _ _ _
| .u8BitDecomposition t _ _ | .u8ShiftLeft t _ _ | .u8ShiftRight t _ _
| .u8Xor t _ _ _ | .u8Add t _ _ _ | .u8Sub t _ _ _
| .u8Xor t _ _ _ | .u8Add t _ _ _ | .u8Mul t _ _ _ | .u8Sub t _ _ _
| .u8And t _ _ _ | .u8Or t _ _ _ | .u8LessThan t _ _ _ | .u32LessThan t _ _ _
| .debug t _ _ _ _ => t

Expand All @@ -114,7 +115,7 @@ def Term.escapes : Term → Bool
| .assertEq _ e _ _ _ | .ioGetInfo _ e _ | .ioSetInfo _ e _ _ _ _
| .ioRead _ e _ _ | .ioWrite _ e _ _
| .u8BitDecomposition _ e _ | .u8ShiftLeft _ e _ | .u8ShiftRight _ e _
| .u8Xor _ e _ _ | .u8Add _ e _ _ | .u8Sub _ e _ _
| .u8Xor _ e _ _ | .u8Add _ e _ _ | .u8Mul _ e _ _ | .u8Sub _ e _ _
| .u8And _ e _ _ | .u8Or _ e _ _ | .u8LessThan _ e _ _ | .u32LessThan _ e _ _
| .debug _ e _ _ _ => e

Expand Down
5 changes: 3 additions & 2 deletions Ix/Aiur/Stages/Simple.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -74,6 +74,7 @@ inductive Term : Type where
| u8ShiftRight (typ : Typ) (escapes : Bool) (a : Term) : Term
| u8Xor (typ : Typ) (escapes : Bool) (a : Term) (b : Term) : Term
| u8Add (typ : Typ) (escapes : Bool) (a : Term) (b : Term) : Term
| u8Mul (typ : Typ) (escapes : Bool) (a : Term) (b : Term) : Term
| u8Sub (typ : Typ) (escapes : Bool) (a : Term) (b : Term) : Term
| u8And (typ : Typ) (escapes : Bool) (a : Term) (b : Term) : Term
| u8Or (typ : Typ) (escapes : Bool) (a : Term) (b : Term) : Term
Expand All @@ -93,7 +94,7 @@ def Term.typ : Term → Typ
| .assertEq t _ _ _ _ | .ioGetInfo t _ _ | .ioSetInfo t _ _ _ _ _
| .ioRead t _ _ _ | .ioWrite t _ _ _
| .u8BitDecomposition t _ _ | .u8ShiftLeft t _ _ | .u8ShiftRight t _ _
| .u8Xor t _ _ _ | .u8Add t _ _ _ | .u8Sub t _ _ _
| .u8Xor t _ _ _ | .u8Add t _ _ _ | .u8Mul t _ _ _ | .u8Sub t _ _ _
| .u8And t _ _ _ | .u8Or t _ _ _ | .u8LessThan t _ _ _ | .u32LessThan t _ _ _
| .debug t _ _ _ _ => t

Expand All @@ -108,7 +109,7 @@ def Term.escapes : Term → Bool
| .assertEq _ e _ _ _ | .ioGetInfo _ e _ | .ioSetInfo _ e _ _ _ _
| .ioRead _ e _ _ | .ioWrite _ e _ _
| .u8BitDecomposition _ e _ | .u8ShiftLeft _ e _ | .u8ShiftRight _ e _
| .u8Xor _ e _ _ | .u8Add _ e _ _ | .u8Sub _ e _ _
| .u8Xor _ e _ _ | .u8Add _ e _ _ | .u8Mul _ e _ _ | .u8Sub _ e _ _
| .u8And _ e _ _ | .u8Or _ e _ _ | .u8LessThan _ e _ _ | .u32LessThan _ e _ _
| .debug _ e _ _ _ => e

Expand Down
1 change: 1 addition & 0 deletions Ix/Aiur/Stages/Source.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -382,6 +382,7 @@ inductive Term
| u8ShiftRight : Term → Term
| u8Xor : Term → Term → Term
| u8Add : Term → Term → Term
| u8Mul : Term → Term → Term
| u8Sub : Term → Term → Term
| u8And : Term → Term → Term
| u8Or : Term → Term → Term
Expand Down
5 changes: 3 additions & 2 deletions Ix/Aiur/Stages/Typed.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -50,6 +50,7 @@ inductive Term : Type where
| u8ShiftRight (typ : Typ) (escapes : Bool) (a : Term) : Term
| u8Xor (typ : Typ) (escapes : Bool) (a : Term) (b : Term) : Term
| u8Add (typ : Typ) (escapes : Bool) (a : Term) (b : Term) : Term
| u8Mul (typ : Typ) (escapes : Bool) (a : Term) (b : Term) : Term
| u8Sub (typ : Typ) (escapes : Bool) (a : Term) (b : Term) : Term
| u8And (typ : Typ) (escapes : Bool) (a : Term) (b : Term) : Term
| u8Or (typ : Typ) (escapes : Bool) (a : Term) (b : Term) : Term
Expand All @@ -69,7 +70,7 @@ def Term.typ : Term → Typ
| .assertEq t _ _ _ _ | .ioGetInfo t _ _ | .ioSetInfo t _ _ _ _ _
| .ioRead t _ _ _ | .ioWrite t _ _ _
| .u8BitDecomposition t _ _ | .u8ShiftLeft t _ _ | .u8ShiftRight t _ _
| .u8Xor t _ _ _ | .u8Add t _ _ _ | .u8Sub t _ _ _
| .u8Xor t _ _ _ | .u8Add t _ _ _ | .u8Mul t _ _ _ | .u8Sub t _ _ _
| .u8And t _ _ _ | .u8Or t _ _ _ | .u8LessThan t _ _ _ | .u32LessThan t _ _ _
| .debug t _ _ _ _ => t

Expand All @@ -84,7 +85,7 @@ def Term.escapes : Term → Bool
| .assertEq _ e _ _ _ | .ioGetInfo _ e _ | .ioSetInfo _ e _ _ _ _
| .ioRead _ e _ _ | .ioWrite _ e _ _
| .u8BitDecomposition _ e _ | .u8ShiftLeft _ e _ | .u8ShiftRight _ e _
| .u8Xor _ e _ _ | .u8Add _ e _ _ | .u8Sub _ e _ _
| .u8Xor _ e _ _ | .u8Add _ e _ _ | .u8Mul _ e _ _ | .u8Sub _ e _ _
| .u8And _ e _ _ | .u8Or _ e _ _ | .u8LessThan _ e _ _ | .u32LessThan _ e _ _
| .debug _ e _ _ _ => e

Expand Down
12 changes: 7 additions & 5 deletions Ix/IxVM/ByteStream.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -99,8 +99,9 @@ def byteStream := ⟦
}
}

-- `u64` addition with carry propagation (little-endian bytes)
fn u64_add(a: U64, b: U64) -> U64 {
-- `u64` addition with carry propagation (little-endian bytes).
-- Returns the sum together with the final carry-out.
fn u64_add(a: U64, b: U64) -> (U64, G) {
let [a0, a1, a2, a3, a4, a5, a6, a7] = a;
let [b0, b1, b2, b3, b4, b5, b6, b7] = b;
let (s0, c1) = u8_add(a0, b0);
Expand All @@ -122,9 +123,10 @@ def byteStream := ⟦
let (t6, o6) = u8_add(a6, b6);
let (s6, c6a) = u8_add(t6, c6);
let c7 = u8_xor(o6, c6a);
let (t7, _) = u8_add(a7, b7);
let (s7, _) = u8_add(t7, c7);
[s0, s1, s2, s3, s4, s5, s6, s7]
let (t7, o7) = u8_add(a7, b7);
let (s7, c7a) = u8_add(t7, c7);
let final_carry = u8_xor(o7, c7a);
([s0, s1, s2, s3, s4, s5, s6, s7], final_carry)
}

-- `u64` subtraction via repeated decrement (correct for small b)
Expand Down
6 changes: 1 addition & 5 deletions Ix/IxVM/Kernel/Check.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -59,11 +59,7 @@ def check := ⟦
KExprNode.Srt(_) => 1,
KExprNode.Const(idx, _) =>
let ci = load(list_lookup(top, idx));
let u = is_unsafe_ci(ci);
match u {
0 => 1,
1 => 0,
},
1 - is_unsafe_ci(ci),
KExprNode.App(f, a) =>
safe_refs_only(f, top) * safe_refs_only(a, top),
KExprNode.Lam(t, b) =>
Expand Down
Loading