Zero-Knowledge Validity Proofs

This document specifies the ZK validity-proof layer for the ENC protocol: a succinct proof that an SMT state transition produced by the node is valid under the RBAC rules, verifiable by a client in O(1) without replaying the event log or trusting the node.

It complements the Merkle proofs in proof.md (which prove inclusion against a root the client already trusts) by proving the root transition itself is well-formed.

Table of Contents

1. Motivation
2. Proving System
3. SMT Hash: Poseidon2 over BN254
4. The Transition Circuit
5. Multi-Leaf Transitions
6. Folding (Incremental Verifiable Computation)
7. Out of Circuit
8. Verification Flow
9. Status

Motivation

In the base protocol the node is an untrusted sequencer: it orders events, applies them to the Enclave State SMT (see smt.md), and publishes roots committed via Certificate Transparency. A client that wants to trust a new state_hash otherwise has to either re-execute every event or trust the node.

A ZK validity proof removes that choice. For each state-changing AC event the node (acting as prover) emits a proof that

old_root --[valid RBAC transition for this event]--> new_root

The client (acting as verifier) checks the proof against the public roots and is convinced the transition obeys every authorization rule — semiring evaluation, rank, state preconditions, leaf deletion — without seeing the witness or recomputing the tree. This makes ENC a validity rollup for RBAC state.

The same transition relation is proven in two complementary forms: a bounded Groth16 proof of one transition (or a fixed-size batch), and a single folded proof over the entire transition history (Nova IVC — see Folding). The folded form gives O(1) verification of an unbounded chain, which the bounded form cannot.

Proving System

The validity relation old_root → new_root MUST be proven in two complementary modes, both over BN254; implementations MUST use the choices in the following table:

Both modes use the BN254 scalar field Fr (p = 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001) as the field over which the SMT's Poseidon2 hash is defined, so SMT membership is proven natively in-circuit.

The bounded Groth16 verifier is pairing-based and on-chain-friendly (EIP-196/197); the unbounded path folds each transition with Nova and compresses the final instance to one succinct proof.

Trusted setup: Groth16 (and the optional KZG-based folding decider) require a per-circuit / universal setup; the transparent folding path (IPA/Pedersen commitments) requires none.

Verifying keys are published and pinned by clients; a proof is valid only against the pinned key.

SMT Hash: Poseidon2 over BN254

The Enclave State SMT leaf and node hashing use Poseidon2 over BN254 (a SNARK-native hash), so the prover can prove SMT membership inside the circuit cheaply.

The canonical instance is normative:

The round structure is the Poseidon2 form (distinct from Poseidon v1): an initial external linear layer, R_F/2 external rounds, R_P internal rounds, R_F/2 external rounds.

R_F, R_P, d, and M_int match the official Poseidon2 BN256 reference (HorizenLabs/poseidon2).

The round constants are an intentional NUMS deviation from the reference Grain-LFSR — a nothing-up-my-sleeve choice for trivial cross-implementation reproducibility; security rests on the (matching) round structure and matrices, not on the specific constants.

The full instance, including the materialized constants, is the cross-language contract and MUST be embedded, never re-derived per implementation.

Hash modes

Implementations MUST compute each hash mode per the following equations:

compress(cap, l, r) = Poseidon2_permute([cap, l, r])[0]
 
leaf_hash(key, value) = compress(DOMAIN_LEAF, F(key), F(value))
node_hash(left, right) = compress(DOMAIN_NODE, F(left), F(right))

Where F(b) interprets a 32-byte big-endian string as an Fr (reduced mod p), and the capacity element carries the domain constant.

This replaces the SHA-256 prefix-byte domain separation of smt.md:

Unchanged from smt.md

• Tree depth stays 168 bits, MSB-first traversal, namespaced fixed-depth sparse tree.

• Key derivation stays namespace || sha256(raw)[0:160 bits] — SHA-256, not Poseidon2.

  The in-circuit identity→key derivation (derive_key(ns, id) = poseidon2(...)) is deliberately not adopted: the circuit takes the SMT key as a public input and the binding to identity is enforced out-of-circuit (see Identity Binding), which is sound and avoids a second SMT migration plus ~30k constraints of in-circuit SHA-256.

• Empty sentinel stays sha256("") (reduced into Fr for hashing). Empty subtree hashes are precomputed per level.

• Leaf value encoding: a 32-byte SMT leaf value is interpreted as a single Fr via F(b) = Fr::from_be_bytes_mod_order(b) (32-byte big-endian → Fr, reduced modulo p).

  RBAC bitmasks (State bits 0-7, trait bits 8+) fit directly in Fr (< 2^253) and the reduction is a no-op for them.

  Arbitrary 32-byte values (event-status ids, KV content hashes, SMT leaf hash outputs from a SHA-256 path) MAY exceed p by a small margin (2^254 ≤ x < 2^256); the modular reduction is sound by reduction to discrete-log hardness of the underlying 32-byte source — the collision probability between two SHA-256 outputs a, b with a ≡ b (mod p) is ~2^-254, indistinguishable from collision in SHA-256 itself.

The Transition Circuit

The circuit proves a single state-changing AC event drives old_root → new_root validly.

There is one circuit family parameterized by event shape; the single-leaf circuit is the core, and multi-leaf events chain it (see Multi-Leaf Transitions).

Public Inputs

A single-leaf transition exposes exactly these field elements as public inputs:

Everything else — the author's and target's leaf values (bitmasks), the Merkle siblings and presence bitmaps for both leaves, the action schema, the operator rank, the Move from-state, the Grant scope — is a private witness. The verifier learns only that some valid witness exists.

Enforced Constraints

The circuit enforces the complete node authorization pipeline (see rbac/events.md):

1. Membership binding (old). fold_membership(target_key, old_target_leaf, siblings, bitmap) recomputes to old_root. Same for the author leaf. This binds the witnessed pre-image leaves to the public old_root.

2. Authorization (semiring). The RBAC semiring verdict (deny-override via _op rows, Public/Any/ wildcard/Self columns) over the operator's traits MUST be allow for this event type and operation.

3. Rank. The operator's best rank MUST be strictly less than the target's (skipped for the no-traits and self cases per the spec rule).

4. Event-specific preconditions.

   • Move: current_state == from (else the transition is invalid), set the State enum and clear trait flags unless preserve.

   • Grant: the trait being granted MUST be in-scope for the current State.

   • Revoke / Transfer: clear/move the trait bit.

5. Mutation + leaf deletion. The new target leaf is the mutated bitmask, except a bitmask of 0 removes the leaf (substitutes the empty sentinel) — an identity with no roles is not in the tree.

6. Membership binding (new). Re-folding the mutated target leaf through the same siblings MUST recompute to new_root. (Single-leaf updates share siblings, so this is sound without a divergence-detection multiproof.)

A proof exists iff all of the above hold. A forged new_root (or any rule violation) is unsatisfiable.

Emptiness handling (bounded vs folding). This bounded circuit takes the per-level sibling-presence bitmap as a private witness (pinned by the old-root membership binding) and covers present-leaf update and deletion (bitmask→0). Insert from a non-membership old state, and the empty-subtree short-circuit generally, are provided by the folding step (see Folding), which derives emptiness in-circuit from the sibling values rather than from a witnessed flag.

Identity Binding

author_key and target_key are public 21-byte SMT keys, not raw identities. The verifier closes the identity binding out-of-circuit by checking

key == namespace || sha256(id_pub)[0:160 bits]

against the id_pub it already authenticated (e.g. from the Schnorr-signed commit). This is sound — the key→identity map is a single trivial SHA-256 the verifier already computes — and keeps the expensive SHA-256 out of R1CS. is_self is derived in-circuit from author_key == target_key, so the Self authorization path cannot be forged.

Multi-Leaf Transitions

Events that touch more than one leaf MUST be proven as chains of single-leaf transitions through intermediate roots, rather than with a single multi-leaf multiproof, with each multi-leaf event constructed per the following table:

For a bundle, old_root and every intermediate root are public inputs; the final root is the published new_root. Each link is the single-leaf circuit above, so atomicity is proven as "the whole chain verifies or none does." This avoids an in-circuit divergence-detection gadget: because each link is an independent single-leaf update with its own membership binding against the previous root, the chain is sound.

Folding (Incremental Verifiable Computation)

The bounded forms above prove a fixed-size batch: the circuit grows O(N) in the number of transitions, so there is a ceiling. But the Enclave State SMT also holds arbitrary application state (KV namespace 0x02, see smt.md), so the number of state transitions scales with app activity and is unbounded over an enclave's lifetime — no fixed batch can cover the whole history.

Folding (Incrementally Verifiable Computation, via the Nova folding scheme) closes this: each step folds one transition into a running instance, so the prover does O(1) work per step with constant memory, and a final compression SNARK yields one O(1)-verifiable proof of the entire chain.

Step relation. The IVC state is the two field elements z = [smt_root, schema_commitment]. The first moves each step (the SMT root); the second is constant across the chain — a commitment to the enclave's manifest schema, carried unchanged.

Each fold step proves the full per-transition authorization relation — membership of the old leaf in z[0], the RBAC semiring + rank rule on the author (with is_self derived in-circuit), the Move from-state precondition and Grant state-scope (Enforced Constraints item 4), the apply_op mutation, and the new root (including insert of a leaf into an empty slot and delete when a bitmask reaches 0) — and outputs the next root.

Universal step + witnessed op/schema. One circuit proves any single-leaf transition (RBAC, KV, or event-status), with is_ac (whether RBAC authorization applies) derived in-circuit from the target key's namespace byte — so one IVC chain covers an enclave's whole state across all namespaces. To make the constraint matrices identical for every transition (a precondition for a single shared PublicParams), both the event op (Grant/Revoke/Move of any trait) and the action schema (allow/deny flags + ranks, with trait positions fixed at bits 8+k) are witnessed circuit inputs rather than baked constants. So one PublicParams folds arbitrary ops under any enclave schema.

Schema binding. Because the schema is witnessed, the step also binds it: it hashes the witnessed schema in-circuit to schema_commitment = Poseidon2(0x53, flags_packed, ranks_packed) and enforces it equals z[1]. The verifier sets z[1] from the published manifest (the same hash), so a prover cannot fold under a forged, more-permissive schema — the proof is valid only for the manifest's schema. (This is stronger than the bounded circuit, where the schema is a trusted private witness.)

Folding N steps attests every transition in the chain from a trusted r_0 to a final r_n, with no replay; binding r_n to the node's published state_hash is the verifier's job (see Verification below).

Construction. The folding construction MUST follow the choices in the table below:

The empty-subtree short-circuit in the folding step is derived in-circuit from the sibling values (a parent of two empty children stays the sentinel) rather than taking a witnessed "sibling present" flag, so the emptiness check is bound to the actual sibling value (no free witness) — the basis for non-membership, insert, and delete, pending the external review noted under Status.

Because the step hash is the identical Poseidon2 instance, a folded root commits to state exactly as the node's root does, and the folding step enforces the same authorization relation as the bounded circuit. The one remaining difference is identity binding: the bounded circuit exposes the author/target keys as public inputs (so the verifier can bind them to signed events out-of-circuit), whereas the folding step witnesses the keys and derives is_self — the IVC state is [smt_root, schema_commitment], no per-step keys. So a folded proof attests the same per-transition validity, without exposing the per-step identities; the anchoring binds roots to the signed log (which is exactly what the folding path certifies: every transition between two log-anchored roots was valid).

Verification. Recompute schema_commitment from the published manifest. Obtain r_0 from a trusted genesis/checkpoint (or anchor it via CT + STH as in the bounded flow), then verify the compressed folding proof against z = [r_0, schema_commitment], checking the attested final state is [r_n, schema_commitment]. Success means every one of the (unboundedly many) intervening transitions was valid and folded under the manifest's schema — in O(1), with no replay. A reference implementation of this anchored verification (STH + CT inclusion + schema recompute + proof) lives in the impl-zk verifier/ crate.

Out of Circuit

The following checks MUST be performed out-of-circuit by the client with ordinary cryptography, and linked to the proof only by equality of the public field elements (the roots and keys). Putting SHA-256/CBOR/secp256k1 in-circuit would cost millions of constraints per event for no soundness gain.

Verification Flow

To accept a node-claimed state transition for an AC event:

1. Authenticate the event out-of-circuit: verify the commit signature per commit.alg (spec.md §Signature Schemes — Schnorr for the default path; ECDSA for the alg: "ecdsa" path; cosign cert validation for sub-key-authored commits per spec.md §Delegated Sub-keys). Recompute the CBOR event hash. In all cases, id_pub_author = commit.from and id_pub_target = content.target (when present); RBAC and the SMT key derivation are keyed to the parent identity, not the sub-key, so a cert-authorized commit produces the same author_key as a direct-signed commit by the same parent.

2. Derive the expected SMT keys namespace || sha256(id_pub)[0:160 bits] and check they equal the proof's public author_key / target_key. The hash input is the 32-byte x-only id_pub (the field-name used in spec.md §reg_identity — not id_pub_full or sub_pub). Sub-keys are not in the SMT and are never used as SMT-key material.

3. Establish that old_root is trusted — typically via a prior accepted transition, or via a CT inclusion proof + STH anchoring old_root to the signed log (proof.md).

4. Verify the proof against the pinned verifying key. Bounded mode: a Groth16 proof over public inputs (old_root, new_root, author_key, target_key) (plus any intermediate roots for multi-leaf events). Unbounded mode: the compressed folding (Spartan) proof over z = [r_0, schema_commitment] → [r_n, schema_commitment], where schema_commitment is recomputed from the published manifest — see Folding.

5. On success, new_root (bounded) / r_n (folded) is accepted as a valid successor reached by valid transition(s) — without replaying the SMT.

The proof certifies validity of the transition; the CT/STH layer certifies which transition the log commits to. Together a client trusts a fresh state_hash end-to-end with O(1) work.

Production Readiness

This layer is implemented and reference-tested but not yet production-locked:

• Bounded (Groth16). The validity proof verifies over a live node's real Poseidon2 SMT roots (real signed RBAC transition → Groth16 proof → client verify; a forged root is rejected). The single-leaf circuit is ~127k constraints; Transfer/AC_Bundle chain it; the Move precondition, Grant state-scope, rank rule, and leaf deletion are enforced.
• Unbounded (folding). The Nova IVC layer is implemented on the canonical Nova implementation: single-leaf membership-and-update, the full in-circuit RBAC authorization relation (semiring + rank + apply_op + Move from-state precondition + Grant state-scope), and structure-changing insert/delete are each folded and recursively verified. The universal step proves any single-leaf transition (RBAC/KV/event-status), and the op and schema are witnessed inputs — so one shared PublicParams folds arbitrary ops under any enclave schema, with the witnessed schema bound to a manifest commitment in z[1] (a prover cannot fold under a forged schema). A Spartan compression to one succinct proof is demonstrated end-to-end on the Poseidon2 fold chain. The folding step's Poseidon2 is gated byte-identical to the node (shared golden vectors). The full out-of-circuit verifier (impl-zk verifier/ crate) is implemented and run end-to-end against a live wrangler dev node: a real signed Grant is folded through the prover-service, and the client verifies the node's real STH (Schnorr) + CT inclusion proofs anchoring both r_0 and r_n to the signed log, then the compressed folding proof against [r_0, schema_commitment] — accepting r_n, and rejecting any tampering. It runs ceremony-free (transparent IPA commitments). The bounded circuit additionally exposes the keys as public inputs for identity binding; the folding step witnesses them (a by-design IVC difference). Each fold step is sizable (~1.5·10⁵ constraints); "O(1) per step" is asymptotic in chain length, not small.
• Poseidon2 is byte-identical across the JS node, the Rust node logic, the bounded circuit, and the folding step; the instance is validated against the official BN256 reference for R_F/R_P/d/ M_int (round constants an intentional NUMS deviation, above).
• Trusted setup. Groth16 (and the optional KZG folding decider) need a real setup ceremony before production; the transparent IPA folding path does not. Verifying keys MUST be published and pinned.

The reference implementation lives in the impl-zk circuit crate (bounded) and its folding/ crate (IVC).