Lance Ato Nathaniel Davis - Personal Website

The same full adder written twice, once as a Binius64 circuit and once as an R1CS-over-GF(2) instance for Flock, so the two constraint systems can be read side by side. Binary fields let you commit to the witness in F₂ and draw challenges from F₂¹²⁸, which makes booleanity constraints vacuous. What remains is a question of what a single row buys you, and the cheapest circuit that still has a multiplication in it is the place to look.

The identity

A full adder's carry out is majority-of-three, and majority has a one-AND form. Written the usual way it costs two multiplications; rearranged, it costs one.

cout = (a AND b) XOR (cin AND (a XOR b))     two ANDs
cout = a XOR ((a XOR b) AND (a XOR cin))     one AND

Both have the same truth table over all eight inputs. Moving the outer XOR across, which is free because XOR is its own inverse, puts the carry in the shape both backends want: (a ^ b) & (a ^ cin) == (cout ^ a). One constraint. The sum, a ^ b ^ cin, is pure XOR and costs nothing. The algebra is checked independently in scripts/model.py, so the identity verifies without a Rust toolchain.

Binius64 side

Binius64's backend takes constraints of the form (XOR-acc) AND (XOR-acc) == (XOR-acc). XOR is linear over GF(2), so it folds into the operand slots at compile time; AND is the only operation with a cost.

let a_xor_b    = builder.bxor(a[i], b[i]);
let a_xor_cin  = builder.bxor(a[i], cin[i]);
let carry_term = builder.band(a_xor_b, a_xor_cin);
let cout_xor_a = builder.bxor(cout[i], a[i]);
builder.assert_eq("full_adder_carry", carry_term, cout_xor_a);

The operands are 64-bit words and every bit position is an independent adder, so the three bxor calls fuse into the band between them and what reaches the backend is a single AND row covering all 64 lanes. One adder and sixty-four adders cost the same.

Flock side

Flock has no frontend and no gadget library. Its public surface is R1CS over GF(2), so the adder is written as constraint matrices directly. A row is (A·z) * (B·z) == (C·z), where each dot product is an XOR-sum of the selected witness entries and the multiplication is AND.

// (a + b) * (a + cin) == (cout + a)
rows.push(Row::new(&[a, b], &[a, cin], &[cout, a]));

Same identity, same single constraint, different unit: Flock's row holds scalars and covers one instance, and the parallelism moves into the batch dimension its zerocheck runs over. The Ligerito PCS layer has a floor. The smallest batch the binding would accept was 65,536 adder instances at m = 22, so the smallest thing Flock will prove here is sixty-five thousand adders.

What's in the repo

crates/binius64-adder — the circuit, with a sweep mode and CSV output
crates/flock-adder — the R1CS rows and the Ligerito binding
scripts/model.py — the truth-table check, no toolchain required
docs/CONSTRAINTS.md — the comparison in more detail
PINNED.md — the revisions both sides were built against

Run it

python3 scripts/model.py

cargo run --release -p binius64-adder -- --adders 65536 --runs 3
cargo run --release -p binius64-adder -- --sweep --csv results/binius64.csv

cargo test -p flock-adder --features flock --release -- \
  --ignored --nocapture real_ligerito_proof_of_a_batched_adder_verifies

./scripts/bench_blake3.sh both

What the adder does not settle

A million adders is 16,384 AND constraints in Binius64 and a million rows in Flock, and that ratio is a packing artifact rather than a verdict. One nonlinear constraint means a wall-clock measurement is mostly circuit build, prover setup and the Merkle commitment of a witness that is almost entirely padding. The real comparison is BLAKE3, where Flock's own benchmarks put it around 14x ahead; that number belongs to their repository, not to mine.