BigInt

zisklib arbitrary-precision integer routines. Operands are slices of \1 limbs (little-endian: limb 0 is least significant). Division and remainder hint the result and verify Euclid's lemma in-circuit; modular exponentiation uses left-to-right square-and-multiply over a hinted binary decomposition of the exponent.

Overview

Arbitrary-precision integer arithmetic over slices of \1 limbs, used by higher-level layers (curve field reductions for bn254 / bls12_381, RSA-style modexp, hash precomputations). Operands are little-endian limb slices, and \1 is #[repr(transparent)] over [u64; 4], so &[U256] is just &[u64] in groups of four. Most operations come in _short (second operand fits in one U256, skipping the schoolbook loop) and _long (two arbitrary slices) variants. Division and remainder hint the quotient and verify a = q·b + r, r < b in-circuit; scratch types (\1, \1, \1) hold the reusable witness buffers.

The page is organized bottom-up:

Section	Provides	Depends on
Types	U256, ShortScratch, RemLongScratch, LongScratch	—
Addition	add_agtb, add_short	U256
Multiplication	mul_short, mul_long	U256
Squaring	square_short, square_long	U256
Division	div_short, div_long	U256, multiplication, scratch types
Remainder	rem_short, rem_long	U256, multiplication, scratch types
Modular exponentiation	modexp	Multiplication, division, remainder

note

Inputs must be normalized, non-empty and free of leading-zero limbs (a[len-1] != 0) unless the value itself is zero. Prefer the _short variants whenever the second operand fits in a single U256.

---

Types

The core element type plus the three reusable scratch buffers threaded through division and remainder. \1 is the single-limb building block — a 256-bit unsigned value laid out as four little-endian u64 limbs — and the scratch types hold the hinted quotient, remainder, and witness limbs that the in-circuit Euclid check consumes. Sizing depends on whether the divisor is single-limb or multi-limb.

256-bit unsigned integer stored as four little-endian 64-bit limbs. The struct is #[repr(transparent)], so &[U256] and &[u64] share a layout and can be converted with slice_to_flat / flat_to_slice.

#[repr(transparent)]
#[derive(Clone, Copy)]
pub struct U256([u64; 4]);

impl U256 {
    pub const ZERO: Self;
    pub const ONE: Self;
    pub const TWO: Self;
    pub const MAX: Self;

    pub const fn from_u64s(a: &[u64; 4]) -> Self;
    pub const fn from_u64(a: u64) -> Self;
    pub fn as_limbs(&self) -> &[u64; 4];
    pub fn as_limbs_mut(&mut self) -> &mut [u64; 4];
    pub fn is_zero(&self) -> bool;
    pub fn is_one(&self) -> bool;
    pub fn lt(&self, other: &Self) -> bool;
    pub fn gt(&self, other: &Self) -> bool;
    pub fn compare(&self, other: &Self) -> core::cmp::Ordering;
    pub fn slice_to_flat(slice: &[U256]) -> &[u64];
    pub fn flat_to_slice(flat: &[u64]) -> &[U256];
}

Example

let one = zisklib::U256::ONE;
let n   = zisklib::U256::from_u64(42);

---

Addition

Multi-limb unsigned addition with carry propagation. Two variants cover the common shapes: \1 for two big-integer slices where a is at least as long as b, and \1 for the frequent case of adding a single U256 to a multi-limb operand. Both write the result into a caller- supplied buffer that must reserve room for a carry-out limb, and return the actual limb count of the sum.

Adds two normalized big integers a + b where len(a) >= len(b), writing the result into out and returning the limb count of the result.

pub fn add_agtb(a: &[U256], b: &[U256], out: &mut [U256]) -> usize

Parameters

Name	Type	Description
a	&[U256]	First operand, at least as long as b.
b	&[U256]	Second operand, non-empty, no leading zeros.
out	&mut [U256]	Destination buffer with at least len(a) + 1 limbs.

Returns

Type	Description
usize	The number of U256 limbs written to out (either len(a) or len(a) + 1).

Example

let mut out = vec![zisklib::U256::ZERO; a.len() + 1];
let len = zisklib::add_agtb(&a, &b, &mut out);

---

Multiplication

Schoolbook multiplication of normalized big integers. Use \1 when the second factor fits in a single U256 — it avoids the quadratic outer loop and runs in O(len(a)) limb operations. \1 handles arbitrary multi-limb factors and writes up to len(a) + len(b) limbs into the output. Output buffers must be sized for the maximum possible product width.

Multiplies a big integer by a single-limb operand a · b, writing the result into out.

pub fn mul_short(a: &[U256], b: &U256, out: &mut [U256]) -> usize

Parameters

Name	Type	Description
a	&[U256]	Multi-limb factor, non-empty, no leading zeros.
b	&U256	Single-limb factor.
out	&mut [U256]	Destination buffer with at least len(a) + 1 limbs.

Returns

Type	Description
usize	The number of U256 limbs written.

Example

let mut out = vec![zisklib::U256::ZERO; a.len() + 1];
let len = zisklib::mul_short(&a, &b, &mut out);

---

Squaring

Dedicated a² paths that exploit the symmetry of the schoolbook product — diagonal terms plus doubled cross-terms — to roughly halve the multiplications versus a generic mul_long(a, a). \1 handles a single-limb operand and returns a fixed-size 2-limb buffer; \1 covers arbitrary multi-limb operands and writes up to 2 · len(a) limbs.

Squares a single-limb integer a², returning a 2-limb buffer and the number of limbs used.

pub fn square_short(a: &U256) -> ([U256; 2], usize)

Parameters

Name	Type	Description
a	&U256	Non-zero single-limb operand.

Returns

Type	Description
([U256; 2], usize)	The squared value and the number of U256 limbs used (1 or 2).

Example

let (sq, len) = zisklib::square_short(&a);

---

Division

Quotient-and-remainder division for normalized big integers. The quotient is hinted out of circuit and Euclid's lemma (a = q·b + r, r < b) is verified in-circuit, so the verifier cost scales with the limb-by-limb multiplication and compare rather than with a long-division loop. The divisor must be non-zero; use \1 for single-limb divisors and \1 for multi-limb divisors.

Divides a big integer by a single-limb divisor. Hints the quotient and remainder, then verifies a = q·b + r and r < b in-circuit.

pub fn div_short(a: &[U256], b: &U256) -> (Vec<U256>, U256)

Parameters

Name	Type	Description
a	&[U256]	Dividend, non-empty, no leading zeros.
b	&U256	Non-zero single-limb divisor.

Returns

Type	Description
(Vec<U256>, U256)	Tuple of (quotient, remainder) with a = q·b + r.

Example

let (quo, rem) = zisklib::div_short(&a, &b);

---

Remainder

Remainder-only variants for callers that don't need the quotient, matching the same hint-and-verify structure as the division functions but reusing caller-owned scratch buffers (\1 or \1) across repeated reductions against the same modulus. The divisor must be non-zero. These are the hot-path primitives for modular reduction in \1 and curve-field code.

Computes a mod b for a single-limb divisor, reusing the supplied \1 buffers across calls.

pub fn rem_short(
    a: &[U256],
    b: &U256,
    scratch: &mut ShortScratch,
) -> U256

Parameters

Name	Type	Description
a	&[U256]	Dividend, non-empty, no leading zeros.
b	&U256	Non-zero single-limb modulus.
scratch	&mut ShortScratch	Reusable scratch space.

Returns

Type	Description
U256	The remainder a mod b.

Example

let mut scratch = zisklib::ShortScratch::new();
let r = zisklib::rem_short(&a, &b, &mut scratch);

---

Modular exponentiation

Arbitrary-precision base^exp mod modulus via left-to-right square-and-multiply over a hinted binary decomposition of the exponent. EVM-style edge cases (modulus ∈ {0, 1}, exp == 0, base ∈ {0, 1}) are handled explicitly, and the implementation dispatches between single-limb and multi-limb reduction paths based on the modulus width. This is the routine that backs the RSA-style MODEXP precompile.

Computes base^exp (mod modulus) over arbitrary-length operands. Handles the EVM-style edge cases — modulus == 0, modulus == 1, exp == 0, base ∈ {0, 1} — explicitly. Internally dispatches to a single-limb or multi-limb implementation based on the modulus size and verifies the binary decomposition of the exponent in circuit.

pub fn modexp(
    base: &[U256],
    exp: &[u64],
    modulus: &[U256],
) -> Vec<U256>

Parameters

Name	Type	Description
base	&[U256]	Base, non-empty, no leading zeros.
exp	&[u64]	Exponent as little-endian u64 limbs, non-empty, no leading zeros.
modulus	&[U256]	Modulus, non-empty, no leading zeros.

Returns

Type	Description
Vec<U256>	base^exp mod modulus.

Example

let result = zisklib::modexp(&base, &exp, &modulus);