Binary Fields and Binary Hashes
Plonky3 0.7 and 0.8 added a native characteristic-2 proving stack alongside the two-adic prime fields this repository is built on:
p3-binary-field: the towerGF(2) ⊂ GF(4) ⊂ … ⊂ GF(2^128)(Gf2,BinaryField8…BinaryField128),GF(2^128)in the GHASH polynomial basis (Ghash128), andBinaryChallenger, a Fiat-Shamir transcript over a byte hash.p3-binary-dft,p3-binary-pcs, WHIR over binary additive domains, andp3-multi-stark: multilinear commitments and a SuperSpartan-style prover over those fields.- Characteristic-2 AIRs for the bit-oriented hashes:
KeccakBinaryAir(p3-keccak-air) andBlake3BinaryAir(p3-blake3-air).
What this repository supports today
The repository supports complete native binary recursion for Tower128, and for
Poly64 with Poly192 challenges, using additive WHIR, product buses and native
Keccak or Blake3 hash tables.
The Tower128 owner also accepts Tower32 children. It separately verifies binary
PCS and additive-WHIR proofs inside prime-field circuits, including indexed
lookup variants. recursion/examples/native_binary_recursion.rs and
recursion/examples/native_poly_recursion.rs demonstrate binary-in/binary-out
proofs. recursion/examples/binary_prover.rs demonstrates the prime-field outer path.
-
Circuits over binary fields. The primitive circuit layer (constants, public and private inputs, ALU ops, connections, tags) needs only field arithmetic, and runs unchanged over every tower level and
Ghash128(circuit/tests/binary_fields.rs). Two things behave differently from a prime field:x - y = x + yand2 = 0. Integer constructors such asF::from_u64go throughGF(2), so they keep only the parity of their argument.- Gadgets that read field elements as integers are rejected, not silently wrong.
reconstruct_index_from_bitsreturnsCircuitBuilderError::CharacteristicTwoUnsupportedfor a characteristic-2 base field. The decomposition and recomposition gadgets requireBF: PrimeField64withF: ExtensionField<BF>, and the binary tower only extends its byte-aligned levels, so they cannot be instantiated over it at all. - The separate
binary_decompose_coordinates/binary_recompose_coordinatesAPIs use the field's raw basis throughBinaryCoordinateField. Every coordinate is constrained Boolean, and requesting fewer than the full width also constrains the omitted coordinates to zero. These APIs preserve each field's own basis; they do not reinterpret a polynomial element as a tower element.
-
Bit-oriented
BinaryField128arithmetic.BinaryTower128Targetrepresents the Wiedemann tower typep3_binary_field::BinaryField128as 128 Boolean coordinates in a prime or binary circuit field. It does not use the GHASH polynomial coordinates ofGhash128. At each level,a = a0 + a1 X_kstores the lower coefficient first and usesX_k² + X_(k-1) X_k + 1 = 0, withX_(-1) = 1. Bit 0 is one; bitjis the product of tower roots selected by the set bits ofj. Every 128-bit pattern is a valid tower element. The rawu128coordinates in native code come fromTowerLevel::from_repr/to_repr, or from little-endian bytes, notfrom_u128(which embeds throughGF(2)).- Import/export uses eight little-endian 16-bit limbs:
limb[j] = Σ_(i=0..15) bit[16j+i]·2^i. The base field must have order above 65535; both limb methods also reject characteristic two. Limb import constrains the range and base-field embedding, and raw-bit import asserts every input bit is Boolean. binary128_add,binary128_mul, andbinary128_squareuse the existing ALU relations for Boolean XOR/AND and recursive tower reduction.assert_binary128_inverse(value, candidate)constrains their product to tower one; the caller supplies the candidate, and zero has no satisfying inverse. There are no new tables, AIRs, or native-field hints.- All
ExprIds passed to these methods must come from the sameCircuitBuilderexpression graph. The target's read-only bits do not carry a builder identity. A circuit using this arithmetic can be proved with the compact circuit prover and carried into the next recursion layer over the supported prime host fields. Bits-only arithmetic also runs over binary fields; integer-limb import/export remains prime-only.
- Import/export uses eight little-endian 16-bit limbs:
-
Native primitive circuit proofs.
p3_circuit_prover::direct::DirectCircuitAirfreezes a circuit's primitive relation and binds public values in caller order. It accepts native binary carrier fields without integer witness addresses or count-based lookups.recursion/tests/native_binary_circuit.rsproves and verifies circuits over bothBinaryField128andPoly64(withPoly192challenges). The AIR repeats the entire assignment on every row, so its width and openings grow with the circuit's witness count. It is a non-hiding correctness baseline, rejects custom non-primitive tables, and does not yet provide an efficient recursive binary prover. -
Native challenge scalars.
NativeTower128Targetkeeps one expression per scalar and uses native addition, multiplication and squaring only onCircuitBuilder<BinaryField128>. Checked conversions materialize Boolean coordinates or raw words at serialization boundaries. It does not treat GHASH or polynomial carriers as the Wiedemann tower.NativePoly192Targetseparately represents the polynomial challenge as threePoly64scalars, with reduction byy³ = y + 1. -
Compact native primitive tables.
p3_circuit_prover::indexed::IndexedCircuitstores one canonical witness table and proves every gate operand and output with indexed reads. Trusted preprocessing pins the graph's positions, constants and selectors; public values bind in caller order, including aliases. No field-valued integer read counts or creator-role tags are used. Main and preprocessing PCS dimensions are computed from their complete stacked layouts. The native tower and polynomial tests inrecursion/tests/native_indexed_circuit.rsexercise real indexed proofs. This path remains non-hiding and rejects custom non-primitive tables. -
Native Keccak circuit tables.
p3_circuit_prover::native_binary::NativeBinaryCircuitextends the compact indexed relation with the explicitly enablednative_keccak_f1600operation.native_keccak256_bytesaccepts checked raw eight-coordinate bytes and returns 32 bytes in natural digest order. The default upstream binary Keccak AIR retains its Boolean constraints; fixed preprocessing pins each permutation's schedule, and indexed reads bind all 100 input and output limbs to canonical circuit witnesses. Other custom operations still fail closed.recursion/tests/native_keccak_circuit.rsexercises native proof verification and rejection of changed digest values and bridge payloads. The product-bus backend below also uses these hash tables. -
Native product-bus wiring.
p3_circuit_prover::native_bus::NativeBusCircuitbinds gates, public inputs and Keccak boundaries through fixed witness occurrences. Adjacent copies of each witness agree; native product buses authenticate their reads without sending a provider-sized pushforward vector. Each circuit requires a trusted, distinct bus namespace when composed with other circuits under one authority. The complete AIR/preprocessing bundle must be retained together.recursion/tests/native_bus_circuit.rschecks native tower and polynomial proofs, including rejection of cross-circuit public swaps and locally valid forged gate/hash payloads. This non-hiding backend proves the complete native recursive verifier described below. Its minimum-height constructor pads trusted inactive rows for larger initial PCS folds, without adding bus occurrences. Its Keccak table uses the upstream 1,625 bit columns and computes bus limbs from constrained bits, avoiding the indexed backend's 100 extra limb columns. -
Full native Tower128 recursion.
prepared::PreparedNativeBinaryWhirLayerbuilds a complete native scalar verifier for a trusted Tower32 or Tower128 additive-WHIR MultiStark authority, including product GKR, generic sumcheck, AIR evaluation and both main/preprocessing openings. It proves that verifier over Tower128 using native hash tables (Keccak or Blake3) and product buses, and verifies against independently supplied child public values. Checked child tokens must match the retained authority identity before packing or witness execution. The output authority can be used as the next layer's trusted child.recursion/examples/native_binary_recursion.rsdemonstrates one actual native outer proof; the prepared integration test covers wrong statements and foreign-authority rejection. Graph, trace and initial codeword limits are explicit; codeword counts exclude Merkle trees and proving workspaces. Dense Keccak openings currently cause substantial growth in later layers. These proofs are non-hiding. -
Full native folding recursion.
prepared::PreparedNativeBinaryLayerverifies a trusted tower MultiStark authority committed with the BaseFold folding PCS (BinaryNativeAuthority) in a Tower128 circuit and proves it with the same folding PCS, product buses and native Keccak. Each output PCS draws its derived query count plusquery_draw_slackcandidates in circuit. The output authority is the next layer's trusted child; grouped, indexed and BLAKE3-hashed children are rejected before graph construction. These proofs are non-hiding. -
Full native polynomial recursion.
prepared::PreparedNativeBinaryPolyWhirLayerverifies a trusted Poly64 additive-WHIR MultiStark proof in a Poly64 circuit, with Poly192 challenges represented by three coefficient cells. Product GKR, generic sumcheck, AIR evaluation, main openings and independently committed preprocessing openings all use native polynomial arithmetic. Base oracle rows serialize as eight bytes, while challenge oracle rows serialize as 24 coefficient-order bytes; base rows constrain the upper two coefficients to zero. Public values remain native Poly64 cells. The prepared owner checks authority identity, binds the caller's expected statement and exposes its output authority for another layer.recursion/examples/native_poly_recursion.rsproduces an actual native outer proof; integration tests also reject changed statements and foreign tokens. The same non-hiding and resource limits as the Tower128 path apply. -
Construction budgets for native owners. Both prepared owners expose
from_native_authority_with_construction_limits.CircuitConstructionLimitsbounds retained expression nodes, pending connections, non-primitive calls and their slots at periodic checkpoints. A checkpoint can exceed a bound by its local group of work; the final builder also checks before lowering. These counts are separate from final witness/operation limits, trace cells and initial codeword cells, and do not bound bytes or process memory. The examples expose--max-expression-nodesand apply all four entry budgets. -
Non-native binary byte-hash transcript.
BinaryTower128Challengerhas a separate, fallible inherent API (new,with_initial_limbs,observe,observe_slice,observe_digest,sample,sample_bits,check_witness). It matches nativeBinaryChallenger<BinaryField128, HashChallenger<u8, H, 32>>forH = Keccak256Hashorp3_blake3::Blake3, selected by the fixedByteHashpassed to its constructor. It is separate from the prime-fieldRecursiveChallengertrait.- The initial transcript is empty or an even number of raw bytes, supplied as low-byte-first
16-bit limbs. There is no length prefix or padding. A tower observation appends its eight
low-first limbs (the raw little-endian Wiedemann coordinates); a digest observation appends
all sixteen 16-bit limbs in natural byte order. External initial and digest limbs are
constrained to base-field integers at most 65535. The host base field must be an
odd-characteristic
PrimeField64with order above 65535. - An observation clears unread output bytes and appends to the next hash input. A refill
hashes that entire input; the resulting digest becomes both the forward input for the next
chained hash and the current output. Sampling draws bytes from the end of that digest,
retaining a short remainder across draws and refilling only when it is exhausted. Thus the
first sample from an empty transcript starts with the last byte of
H([]), while a refill after consuming its digest hashesH(previous_digest); later observations are appended to that digest in forward order before hashing. A field sample consumes 16 bytes and interprets them as raw little-endian tower coordinates, with no rejection sampling. sample_bits(bits)consumes eight bytes even whenbits == 0, returning Boolean targets for the requested low bits;bitsmust be belowusize::BITS. By contrast,check_witness(0, witness)leaves the transcript and builder untouched. For nonzero difficulty,check_witnessobserves the canonical witness, samples eight bytes and constrains the requested low bits to zero. This is witness checking; native grinding search is outside this API.- Every target and
ExprIdused with one challenger must belong to the sameCircuitBuildergraph; expression IDs do not enforce graph ownership. Enable the matching Keccak-f or BLAKE3 compression operation before a refill, and register its existing preprocessor, AIR builder and prover together with the statement table when proving. Bind dynamic transcript limbs, witnesses and returned samples throughStatementExport::Basein an agreed order. An error leaves the challenger's transcript state unchanged for retry, although expressions or constraints already added to the builder by a fallible gadget may remain.
- The initial transcript is empty or an even number of raw bytes, supplied as low-byte-first
16-bit limbs. There is no length prefix or padding. A tower observation appends its eight
low-first limbs (the raw little-endian Wiedemann coordinates); a digest observation appends
all sixteen 16-bit limbs in natural byte order. External initial and digest limbs are
constrained to base-field integers at most 65535. The host base field must be an
odd-characteristic
-
Native binary transcript hosts. The challenger's
_with_hostmethods share the same transcript implementation with an explicitBinaryCircuitHost.PrimeBinaryEncoding<BF>preserves integer words;NativeBinaryEncodinguses checked raw coordinates and native Keccak tables. Word packing, digest compression, refill order, partial samples and Poly192 coefficient serialization are tested across tower and polynomial carriers. Native BLAKE3 hashing is not yet available through this host. These APIs do not by themselves implement a complete binary-host proof verifier. -
Native byte Merkle verification.
verify_byte_hash_mmcs_opening_bytes_with_hostauthenticates serialized rows with the chosen host, sharing the prime API's mixed-height injection, index bounds and cap selection. Native tests cover odd-width rows, non-power-of-two heights, tower/polynomial carriers and a cap at the leaf layer. The caller still supplies trusted row widths, heights and serialization rules.verify_byte_hash_mmcs_opening_bytes_with_host_arity::<_, 4>opens trees whose nodes compress four digests, in the level order of p3'sMerkleTreeMmcs. Under Keccak a four-digest node hashes 128 bytes, one Keccak-f block like a pairwise node, so a path takes about half the Keccak-f calls. A native WHIR recursion layer chooses its output trees' arity inNativeBinaryRecursionOptions::arity; both native recursion examples use pairwise trees by default and four-digest trees under--hash keccak, and--merkle-arityoverrides the arity. -
Binary hash configurations.
p3_test_utils::binary_field_paramsprovides the configurationp3-binary-pcstests with, once per hash (keccakandblake3submodules with identical item names):- Merkle commitments over any tower level that serialize rows to bytes, hash with Keccak-256 or BLAKE3, and compress node pairs with the same hash;
BinaryChallengertranscripts over the same byte hash.
-
Binary hash AIRs.
test-utils/tests/binary_hashes.rschecks that the Keccak-f and BLAKE3 AIRs overGF(2^128)accept their generated traces and reject a non-bit cell or a flipped bit, and that the byte-hash commitments round-trip and reject tampering. -
In-circuit Keccak. Prime-field circuits can call Keccak-f[1600] as a non-primitive operation (
CircuitBuilder::enable_keccak_f1600/add_keccak_f1600).- State layout: the state is 100 little-endian 16-bit limbs (limb
4·i + kis limbkof lanei = x + 5·y), matchingp3-keccak-air. - Proving: the
KeccakF1600Airtable runsKeccakAirover 24 rows per call and ties the input and output limbs to the witness table throughWitnessCheckslookups.KeccakAir's bit decompositions keep every limb below2^16. - Registration: register it with
KeccakF1600Preprocessor,KeccakF1600AirBuilderandKeccakF1600Prover. - Merkle compression:
keccak256_compressbuilds on it. It computes Keccak-256 of two 32-byte digests in one call, matchingCompressionFunctionFromHasher<Keccak256Hash, 2, 32>, the node compression of a Keccak Merkle tree. - Keccak-256 sponge:
keccak256_limbshashes messages of any even byte length. The first block fills the zero state directly; later blocks are XORed in with a bitwise gadget. - Leaf hash:
keccak256_field_elementsmatchesSerializingHasher<Keccak256Hash>, the leaf hash of a Keccak Merkle tree. Elements are serialized exactly as Plonky3 does it (Montgomery fields such as BabyBear hashx·2^32 mod p). Each serialized value is decomposed into canonical bits, soy + pcannot stand in fory.
- State layout: the state is 100 little-endian 16-bit limbs (limb
-
In-circuit BLAKE3.
enable_blake3_compress/add_blake3_compressexpose one BLAKE3 compression per call.- Limb layout: 56 input limbs (block, chaining value, counter, block length, flags, each 32-bit word as a little-endian 16-bit pair) and 32 output limbs.
- Proving: the
Blake3CompressAirtable runsp3-blake3-air'sBlake3Air, one compression per row, with each call's real counter, length and flags. It exposes the limbs through dedicated columns tied toBlake3Air's bit columns. - Registration: register it with
Blake3CompressPreprocessor,Blake3CompressAirBuilderandBlake3CompressProver. - Gadgets: built on the compression are
blake3_limbs(messages of any even byte length, through the full chunk tree),blake3_compress_digests(CompressionFunctionFromHasher<Blake3, 2, 32>) andblake3_field_elements(SerializingHasher<Blake3>).
-
Merkle openings.
verify_byte_hash_mmcs_openingconstrains an opening of a Keccak-256 or BLAKE3MerkleTreeMmcsbatch commitment, mirroring the native binary-arityverify_batch:- Inputs: the opened rows of several matrices with their heights, the little-endian index bits, the sibling digests (bottom-up) and a cap of any power-of-two root count.
- Heights: as natively, they need not be powers of two, but each must be
ceil(max_height / 2^k). The index is constrained below the tallest height. - Injection: shorter matrices' rows are folded in at the level where their height is reached.
- Cap: the remaining index bits select the cap root.
- Shorthands:
verify_byte_hash_merkle_path,verify_keccak_merkle_pathandverify_blake3_merkle_pathcover the single-matrix, one-root case.
-
Recursion over hash tables. A batch proof whose circuit used Keccak-f or BLAKE3 can be verified by the next recursion layer.
- Low-level: pass
KeccakF1600Prover/Blake3CompressProveramong the input table provers ofverify_p3_batch_proof_circuitandreplay_batch_layer_transcript. - Built-in backends:
PcsRecursionBackend::input_table_proversadds these tables to the backend's own input provers in the input manifest's order, throughwith_hash_table_input_provers. The FRI and WHIR backends use it. - No relaxation: hash tables are only ever added. With its hash entries removed, the manifest must still list the backend's own tables exactly, as before.
- Low-level: pass
Not yet supported
- Native scalar recursion for indexed lookup relations or a BLAKE3 circuit host. The complete native Tower128 and Poly64 paths use product buses, Keccak and additive WHIR; those other input adapters still use prime hosts.
- Efficient bounded-size composition across many native layers. Output authorities can prepare subsequent layers, but dense Keccak oracle openings currently make those verifier circuits grow substantially.
- Folding-PCS MMCS trees of arity above two.