Trappin' Binary Towers

F₂ is the smallest field there is, and until recently it was useless for proving anything. The reason is soundness. Every interactive proof depends on a random challenge, and the probability an adversarial prover survives one is bounded by the polynomial degree over the field size. Sampling challenges from F₂ creates an unfair advantage for the adversarial prover.

So proof systems used large prime fields. Early zkEVMs settled on the BN254 scalar field, mostly because Ethereum ships precompiles for BN254 pairings, which makes on-chain verification cheap. The word size was never the selling point; the EVM works in 256-bit words and the BN254 scalar field is roughly 254 bits. Almost, but not quite large enough for the 256 bit word. Every uint256 therefore decomposes into limbs, and every limb carries range checks.

The industry then shifted from proving the Ethereum virtual machine to proving any virtual machine, and the fields shrank to match. BabyBear is 31 bits, Goldilocks is 64, and both are sized so a 32-bit RISC-V word fits. Booleanity remained. If you want a variable in a prime-field R1CS to be a bit, you constrain x * (1 - x) == 0, one constraint per bit, before computing anything. For a workload made entirely of boolean logic, which describes every hash function, that cost lands on every wire.

Binary towers

The fix is a field that contains only bits. Wiedemann's tower construction builds F₂ ⊂ F₄ ⊂ F₁₆ ⊂ F₂₅₆ and onward, each level a degree-two extension of the one below. The small fields embed into the large ones as prefixes, so a value in F₂ is already a value in F₂¹²⁸ with zeros in the higher coefficients. Moving between levels costs nothing.

That enables a split. Commit to the witness in F₂, one bit per variable; draw the challenges from F₂¹²⁸, where Schwartz-Zippel gives a useful bound. Booleanity disappears, because the field contains only 0 and 1 and the constraint is vacuous. Commitments are hash-based, so the scheme is transparent and post-quantum secure, with no trusted setup and no toxic waste.

Reconciling the two field sizes is the actual work. Committing to bits and then handling each one embedded in a 128-bit element for the rest of the argument gives back the entire saving. Binius solves this with ring-switching, and the intermediate object is a tensor algebra, F₂¹²⁸ ⊗ F₂¹²⁸ over F₂. It has zero divisors, so it is a commutative ring and not a field. Picture a 128 by 128 grid of F₂ coefficients.

The mechanism is a reindexing. A message of 2^ℓ bits reads as 2^ℓ elements of F₂ or as 2^(ℓ-7) elements of F₂¹²⁸, packing 128 consecutive bits into each, so the variables of the multilinear split into an inner group naming the bit inside an element and an outer group naming which element. Ring-switching folds the inner variables away and reduces an evaluation claim about the bit-valued polynomial to one about the packed polynomial. The intermediate claim is an element of the tensor algebra for one step, and a random linear combination reduces it back to a field claim. I have not verified the exact split against Flock's specialization, only the general construction, so treat the seven as approximate.

Flock vendors this directly from Binius64, tensor_algebra.rs and the ring-switch verifier helper both. The lineage is visible in the file list.

Binius circuit 101

Binius64 provides CircuitBuilder, an API for writing circuits by hand, plus a gadget library covering SHA-256, ECDSA and the usual suspects. The unit is a 64-bit word, a deliberate move away from the original tower-field Binius, archived last September, toward something shaped like a CPU register.

The backend has one constraint type worth caring about, of the form (XOR-acc) AND (XOR-acc) == (XOR-acc), where each accumulation is an XOR of shifted witness words. Two things follow. XOR is linear over GF(2), so it folds into the operand slots of a neighboring constraint at compile time and costs nothing. AND is the only operation with a cost. Circuit design reduces to rewriting the function until the work sits in the free operations.

A full adder is the smallest interesting case. Written the standard way, the carry costs two ANDs. However, cout is majority-of-three, and majority has a one-AND form.

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 expressions have the same truth table over all eight inputs. The second has one fewer multiplication.

Rearranged into the constraint shape, with the outer XOR moved across because XOR is its own inverse, the carry becomes (a ^ b) & (a ^ cin) == (cout ^ a). One constraint.

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

a[i], b[i] and cin[i] are 64-bit words, and every bit position in them is an independent adder. The three bxor calls do not each become a constraint; they are linear, so the compiler fuses them into the operand slots of the band between them. What reaches the backend is a single AND row covering all 64 lanes. One adder and sixty-four adders cost the same :)

The sum is a ^ b ^ cin, pure XOR, free. Binding it to a declared output wire is a purely linear assertion with no multiplication in it, and whether the compiler discharges that for free or emits a row to hold it is worth measuring. Check n_bitand in the prove trace; one per word means free, two means the binding costs a constraint.

Flock circuit 101

Flock has no frontend, no builder and no gadget library. The provers it ships are hand-written encoders for BLAKE3, SHA-256 and Keccak-f[1600]. Its public surface is R1CS over GF(2), so writing a full adder for Flock means writing the constraint matrices directly.

An R1CS row over GF(2) is (A·z) * (B·z) == (C·z), where z is the witness with z[0] pinned to 1, each dot product is an XOR-sum of the selected entries, and the multiplication is GF(2) multiplication, which is AND. That is the same object as the Binius64 constraint. Binius64 documents its own constraint system as building on R1CS and CCS, so the resemblance is inheritance.

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

a, b, cin and cout are indices into z, each holding a single GF(2) element instead of a word. The three slices are the A, B and C selectors for one row, and the row is satisfied when the XOR of the A entries, ANDed with the XOR of the B entries, equals the XOR of the C entries. The selectors must be sorted and pair-cancelled, because a variable appearing twice in the same selector cancels to zero over GF(2).

Same identity, same single constraint, different unit. Binius64's row operates on a 64-bit word and covers 64 instances. Flock's operates on a scalar and covers one, and the parallelism moves into the batch dimension that its zerocheck runs over.

Flock's Ligerito PCS layer has a minimum size. The smallest batch the binding would accept was 65,536 adder instances at m = 22. You cannot prove one full adder in Flock; the smallest thing it will prove is sixty-five thousand of them. I do not know whether 22 is the true floor or the value I reused from Flock's own test suite without pushing lower.

What actually differs

A million adders is 16,384 AND constraints in Binius64 and a million rows in Flock. That ratio is a packing artifact. Flock recovers it through ring-switching and its batch structure, which is the subject of its paper. Wall clock is the only thing that settles the comparison, and the full adder does not settle it either, because one nonlinear constraint means the measurement is circuit build, prover setup and the Merkle commitment of a witness that is almost entirely padding.

The real comparison is BLAKE3, and Flock's own benchmarks put it around 14x ahead of Binius64 there. I have not run that sweep, so the number belongs to their repository. What it buys and what it costs is visible in the source. Flock is specialized to batches of one fixed boolean circuit, its optimized kernels are NEON and gated to ARM64 with scalar fallbacks elsewhere, and its authors describe it as a research prototype and recommend against production use. Binius64 proves arbitrary circuits over 64-bit words, ships gadgets, and supports an application today.

If you run the comparison yourself, match the thread counts explicitly, because Binius64's rayon is off by default. Pin both revisions, since Flock is a handful of commits old and Binius64's main moves fast enough that performance moves with it. Report proof size and verify time next to prove time; they move differently and a prove-only table hides the trade. Irreducible has published corrections to their own earlier benchmarks over a CPU and GPU instance mismatch.

Why I spend time here

Sereel is capital markets infrastructure, and the interesting problems in it involve proving something about a portfolio without publishing the portfolio. Compliance attestations, reserve proofs, eligibility checks against a rule set a regulator wrote and an investor cannot see. Those are boolean-heavy workloads, and boolean-heavy is where binary fields change what is affordable.

I am not shipping Binius in production this quarter. I do want to know, before I need it, which of these systems is general enough to build on and which one is a specialist offering 14x on one workload. Reading two implementations of the same six-line circuit answered that faster than reading either paper.

The repo is at github.com/lancenonce/binius-flock. The full adder is in crates/binius64-adder and crates/flock-adder, the algebra is checked independently in scripts/model.py so the identity verifies without a Rust toolchain, and docs/CONSTRAINTS.md walks the comparison in more detail. Clone it, break it, tell me where I am wrong.

Check it out under Projects.