Circuits and layers

The SMT compiler translates one operation kind into a layered circuit whose output wires are constraint residuals. This page follows that translation: what the circuit checks, how the input vector is laid out, how Poseidon2 rounds become layers, and how the verifier evaluates the wiring. Each property is labeled as measured or as a consequence of the source structure.

Circuits are compiled per kind#

compiler::compile_with_hints(params, kind, strategy, template) builds the circuit for one SmtOpKind under one configuration. The structure depends only on the operation kind, the tree depth, the leaf bound and the layer strategy, never on a particular key, leaf or path. One compiled circuit therefore serves every request of its kind and configuration, which is what makes preparation reusable.

Key bits are circuit inputs. At each level a multiplexer built from Mul gates uses the key bit to choose the left and right order of the accumulator and the sibling, so the same circuit works for every key.

compile_with_hints also returns WiringHints, which the verifier uses to derive its wiring oracle. compile returns the same circuit without hints.

Acceptance is an all-zero output layer#

Every output wire of a compiled circuit is a residual: the difference between two values that must be equal. A witness is accepting when every output wire is zero, which compiler::is_accepting tests. The verifier always claims an all-zero output layer and never takes output values from the prover.

The residuals of one authentication path are:

1. Leaf binding: the leaf hash of the pre-image minus the first accumulator.
2. Level transitions: at every level, the compression of the accumulator and the sibling, in the order the key bit selects, minus the next accumulator.
3. Root: the last accumulator minus the root input.
4. Value digest: the first accumulator, which the leaf binding ties to the leaf hash, minus the value_digest input. For an update the new path's first accumulator is used, so the value digest names the new leaf.
5. Key bits: s * (s - 1) for every key bit s, which is zero only when s is 0 or 1.
6. Non-membership tag: for NonMembership only, tag * (tag - 2) on the leaf tag, which is zero only for Empty (0) and Tombstone (2).

An Update circuit contains a second path over the same siblings and key bits, bound to the new root. Together with the public-input checks the verifier performs, circuit acceptance is designed to agree with the native semantics of compiler::smt_valid_native. That agreement is proved for the compiler model in Isabelle/HOL, and the connection to the Rust code is partial; see Formal verification.

The input vector#

The circuit reads one input vector. The prover fills it during witness generation, and the verifier rebuilds it from the request with compiler::build_input_vector. For Membership and NonMembership the segments are, in order:

An Update layout holds two leaf pre-images, two accumulator chains, the shared siblings and key bits, the old and new roots and the value digest. The vector is padded with zeros to the next power of two. compiler::InputLayout exposes every offset.

Parallel path constraints#

A Merkle path is a sequential computation in which each accumulator depends on the previous one. The circuit does not reproduce that sequence layer by layer. The witness computes all accumulators in order, the input vector carries them, and the circuit checks every compression transition independently against the supplied intermediate values. The level transitions are identical sub-circuits placed side by side in the same layers.

A deeper tree therefore adds width, meaning more parallel sub-circuits per layer, rather than more layers. The longest chain in the circuit is the leaf hash: at the default leaf bound it absorbs its 32-lane pre-image in four sponge blocks, and each block is one 29-layer permutation. The builder carries shorter chains up to the output level with identity copies.

Cube gates and fused rounds#

A Poseidon2 round adds round constants, applies the x^3 S-box and multiplies the state by a fixed matrix. Written with a separate gate for each step, one round would take several layers. The builder's combine node instead accumulates into one output wire a sum of taps plus a constant. Each tap is either coeff * a (TapKind::Lin, emitted as a Lin gate) or coeff * a^3 (TapKind::Cube, emitted as a Pow3 gate), so one round becomes one layer:

out[z] = sum over lanes x of M[z][x] * sbox(u[x]) + next_rc[z]

External rounds cube all 16 lanes. Internal rounds cube lane 0 and pass the other 15 lanes through as linear taps. Because a Pow3 gate cubes its input wire directly, the round constant that has to be added before the next cube travels in the current layer's constant vector. A full permutation is one initial linear layer followed by 4 external, 20 internal and 4 external rounds: 29 layers.

Pow3 is an operation of the circuit representation, not a processor instruction. The benefit of fusion is structural, fewer and denser layers. No measurement of an unfused compiler exists, so there is no speed figure for it.

The layer schedule across tree depths#

Proof size grows slowly because it depends on the logarithm of the layer widths. The sumcheck of each layer has two rounds per bit of the width of the layer below it, so doubling a layer's width adds two round polynomials to one sumcheck. A fixed layer count with modest proof growth does not mean constant cost: total computation still grows with depth.

Wiring oracles at verification#

At the end check of each layer the verifier needs the wiring predicate MLEs at the sumcheck's random point. The gkr::WiringOracle trait abstracts that evaluation, and the engine ships three implementations:

DerivedRegularWiring::derive(circuit, hints) groups gates into data-parallel families: blocks of identical sub-circuits laid out at a power-of-two stride from an aligned base. The circuit builder emits a FamilyTag (family, block) for each gate and constant as a hint. Derivation re-checks every proposed progression gate by gate, and any gate that does not fit stays on an exact sparse path. Derivation is designed so that a wrong hint can only cost speed: each proposed progression is re-checked gate by gate, unmatched gates stay on the exact sparse path, and tests compare the derived oracle with TableWiring on the compiled circuits. expand_gates re-expands it for audit, and stats reports how much of the circuit the closed form covered. The Rust derivation itself is not formally verified; see Formal verification.

With the circuit, request and proof held fixed and only the wiring oracle changed, the complete prepared typed verification call was 10.80–23.68 times faster with the derived oracle across nine depth and operation profiles. Preparation is outside the timer; request validation and native leaf and path hashing are inside it. TableWiring already iterates a sparse gate list, so this comparison is separate from the Dense prover reference described in How GKR works.

Layer strategies#

LayerStrategy selects how tree levels map to GKR layers:

The inner-proof encoding accepts only the strategy identifier of A. See Configuration.

The full circuit commitment#

prepare computes a full circuit commitment for each compiled circuit: a Poseidon2 digest over the configuration and every gate and constant in compiler emission order. Equal circuits give equal commitments, and changing any gate gives a different one, barring a hash collision. Every proof transcript absorbs the commitment, and an encoded proof carries it. Verifiers take it from their own preparation, recomputed by prepare or taken from the crate-pinned anchor of the reviewed depth-24 membership material, and never accept a received value on trust. Wire format gives the exact preimage.

Next steps#

• Proof lifecycle shows where compilation, wiring derivation and the commitment run.
• Prepared execution explains how to reuse them across requests.
• Benchmark results lists the measurements with their conditions.