Module wide_int 

64-bit integers on a chip whose integer lanes are 32 bits wide.

An RDU computes integers in INT32 (super::rdu_chip::RduChipFacts::index_datatype), and some of what a model asks for needs 64 bits: Qwen3.8-Flash-Next’s n-gram hash multiplies a token by a multiplier below 2^45 and reduces the exclusive-or of such products by a prime (crate::model::ngram_hash), and an index past 2^31 needs a wider type. lower turns each 64-bit operation (Op64) into a LaneProgram: straight-line 32-bit lane operations (wrapping add and subtract, the low half of a product, bitwise operations, shifts by a constant), a 64-bit operand travelling as its low and its high lane.

The arithmetic lowerings keep every lane operation exact. An operand is cut into 16-bit limbs, so a limb product fits a lane; sums are carried limb by limb; and a value is only ever cut by a shift and a mask. A subtraction adds the complement plus one. The remainder by d is Barrett’s: the quotient estimate ⌊x · m / 2^64⌋ with m = ⌊2^64 / d⌋, the difference x − q·d, which lies in [0, 2d), and one conditional subtraction of d.

prove proves each lowering equal to its 64-bit definition. The arithmetic ones by their algebra: the program is evaluated symbolically over the integers, with an interval for every lane that shows no operation wraps; every cut v = h · 2^k + l keeps h as a symbol and writes l as v − h · 2^k; and what the outputs then are is a polynomial identity — the result equals the definition plus 2^64 times an integer polynomial — that the kernel checks by ring normalization (the first kernel’s try_ring reduced to DRingSolve and its conclusion, by infer_type). The second kernel re-checks each identity by exact evaluation at a Kronecker point where that fits its bound on slots (one per symbol at degree one: the add’s and subtract’s identities, not the multiply’s); it never disagrees, and a proof records which identities it decided (KernelVerdict). The remainder’s proof is a chain of such identities, the intervals that bound Barrett’s difference to [0, 2d), and the two cases of its correction. The bitwise lowerings and the shifts are wiring, proved by a certified equivalence check of their bit-blasted circuits (logicaffeine_proof::fraig, its LRAT derivation replayed).

Structs

LaneProgram

A straight-line program over 32-bit lanes computing one 64-bit operation: its inputs are each operand’s low and high lane, its two outputs the result’s.

Proof

A lowering’s proof: the program, and how it is proved equal to its 64-bit definition.

Enums

KernelVerdict

What the kernels say of one identity.

LaneOp

One operation of a 32-bit lane.

Op64

A 64-bit operation on unsigned integers; a shift carries its distance and a remainder its divisor.

ProofKind

How a lowering is proved.

Functions

lower

The program that computes op on 32-bit lanes.

needs_limbs

Whether a 64-bit integer needs limbs on target: its datapath stores no 64-bit integer.

prove

The lowering of op and its proof.

prove_program

A proof that program computes its operation, or why there is none. Proof::check accepts only a proof of the lowering itself; this is the prover any program can be put to.

Type Aliases

Identity

One identity the kernels check: lhs = rhs over the integers.

Reg

A register: the index of the operation that defines it.