# Consolidated design specification — ZK recovery contract (Cardano) > **This is the single normative document.** `docs/00-09` and `audit/01-05` are working > artifacts; where any of them differs from this file, this file governs. Corrections from > the third external audit (`audit/06`) are folded in here; the per-finding triage is in > `audit/07`. Status: research + specification. Target: **Groth16 over BLS12-381**, verified on-chain via Plutus V3 builtins (CIP-381), now with **van Rossem (Protocol v11)** batch verification. Custody: **contract-held funds with a committed credential→entitlement Merkle snapshot**. This document is normative; the detailed requirement and attack catalogues remain in `docs/04` (99 EARS) and `docs/03` (54 attacks), with corrections in `audit/03`–`audit/04`. ## 1. Problem and secret model The SecondFi/Yoroi defect derived the EdDSA nonce as `r = H(M)` instead of `r = H(k_R ‖ M)`, leaking the **leaf signing scalar** `a` of ~8,823 credentials (so `A = aB` and `C = Blake2b-224(A)` are public for every exposed credential). What did **not** leak (report §7.5): the 24-word phrase, BIP-39 entropy, master seed, the nonce prefix `k_R`, and the chain code. Therefore a victim **cannot** prove ownership by signing — `a` is public-recoverable. The only secret that distinguishes owner from thief is material **above the leaf** in the CIP-1852 tree. Recovery = a zero-knowledge proof of knowledge of such a secret that derives to an exposed credential `C` on the custody list, with payout bound to a fresh destination `D`, revealing nothing. ## 2. Architecture | Component | Role | |---|---| | **Eligibility snapshot** | Off-chain construction of a fixed-depth Merkle tree over `(C, entitlement, snapshot_version)` leaves (§3.3, §13 — `snapshot_version` is hashed into every leaf, not just pinned separately); root + `snapshot_version` are *additionally* pinned on-chain (immutable parameter / reference input) for eligibility binding independent of any Merkle path. | | **Client prover** | Fully offline. Takes the 24 words, derives the 96-byte master XPrv in plaintext (PBKDF2 outside the circuit), produces a Groth16 proof. The seed/XPrv never leave the device. | | **Recovery circuit** | Proves derivation `master XPrv → C` (steps 3–4 only), Merkle inclusion, destination binding, nullifier. | | **On-chain verifier** | Plutus V3 validator: verifies the proof (single or batched), reconstructs public inputs from authenticated context, enforces O(1) spent-state and the value delta. | | **Custody** | Sharded validator-held UTxOs (ADA + commingled tokens/NFTs); per-claim release of the snapshot-committed entitlement. | | **Aggregator (optional, van Rossem)** | Untrusted party that bundles many claims into one batched or aggregated proof for throughput. Cannot redirect or forge claims (§7.4). | ## 3. The proof statement ### 3.1 Public input (single aggregated field element) ``` pub = Fr( Blake2b-256( DOM ) ), DOM = domain_sep ‖ scriptHash ‖ snapshot_version ‖ merkle_root ‖ C ‖ entitlement_encoding ‖ D_full_address_bytes ‖ role ``` The validator **reconstructs** `pub` from authenticated context (root/vk/version/scriptHash from the immutable datum/parameter; `D` and entitlement from the actual output paying `D`) and never accepts a prover-supplied value (REQ-V-06). ### 3.2 Private witness ``` master_xprv = kL(32) ‖ kR(32) ‖ chaincode(32) // 96-byte Icarus master account_index, role ∈ {0,1,2}, address_index // 0=payment,1=change,2=staking; 1852',1815' constants merkle_path // fixed depth = ceil(log2 N) entitlement_preimage = (C, ada_amount, asset_bundle, snapshot_version) D_full_address_bytes ``` The leaf scalar `a` and any account-/role-level extended key are **inadmissible** standalone witnesses (REQ-D1-10). ### 3.3 Relation R (knowledge of witness s.t.) 1. **Clamp** on master `kL` (range-checked in-circuit, not assumed). 2. **Derivation, steps 3–4 only** (PBKDF2/BIP-39 explicitly out of circuit): 3 hardened then 2 soft DerivationScheme-V2 levels, top indices fixed to `1852+2³¹`, `1815+2³¹`, `role ∈ {0,1,2}`. Every output byte 8-bit range-checked, every carry exact-width, **no mod-L reduction**. 3. **Leaf key** `A = encode(scalarmult_base(kL_leaf))`, canonical RFC-8032. 4. **Credential** `C = Blake2b-224(A)`. 5. **Eligibility**: Merkle inclusion of `H(0x00 ‖ C ‖ entitlement ‖ snapshot_version)` (`H = Blake2b-256`, frozen §13) under domain-separated nodes at fixed depth, to `merkle_root`. 6. **Role coherence**: one `role` drives both the CKD index and the public commitment. 7. **Destination freshness**: the payout destination `D`'s payment credential (`D[1:29]` of the 57-byte base address) MUST NOT equal the claimed credential `C`, so recovery can never route funds back to the (compromised) claimed key. Enforced in-circuit — the proof is *uncreatable* otherwise — not left to client UX (REQ-D1-15; defends T2-10). Scope: the *claimed* credential only; the staking credential is unconstrained (it does not gate spending). ### 3.4 Nullifier and binding `nullifier = Blake2b(domain_sep ‖ scriptHash ‖ C)` — a pure function of the public credential `C` and the instance identity `(domain_sep, scriptHash)`, with no free witness input. **Version-stable by design (§8 option 1)**: the nullifier omits `snapshot_version`, so a credential's spent-state is keyed identically across snapshot versions at a given `scriptHash` — the same `C` yields one nullifier regardless of which snapshot version it claims under, and a credential already recorded spent stays spent if a later snapshot re-lists it (no per-version migration needed on the version axis). Eligibility remains version-scoped: `snapshot_version` is still bound into `pub` via `reconstructPub` (§3.1), so a proof only verifies against the committed version's root. The on-chain spent-state is enforced per credential via the §8 claim tickets (a pre-created ticket consumed on claim) — the §8 spent-state, now implemented. The cross-`scriptHash` redeploy migration — a different validator instance, hence a fresh nullifier namespace — remains the §8 / REQ-TS-15 concern, unchanged. This matches the implementation (`Recovery.Logic.nullifier`), the Lean model (`Validator.v_null`), and REQ-D1-08/REQ-D1-13. *(Reconciled 2026-06-29: SP2 adopted SPEC §8 option 1 — the version-stable nullifier with claim-ticket spent-state — superseding the prior version-dependent design and its cross-version §8 migration.)* No dependence on `a`/signature/proof bytes. Binding folds `D` (network id + payment + staking credential — the full destination address bytes, and *only* the address bytes; see `docs/04-ears-requirements.md` REQ-D1-07's frozen destination-binding-scope and address-form paragraph, CL-004, for the exact scope and the 29B/57B address-width rule) into `pub`, defeating mempool redirection. Separately, the circuit constrains `D`'s payment credential `≠ C` (REQ-D1-15): a claim can never return the recovered funds to the compromised claimed key — a hard, witness-independent invariant (the proof is uncreatable otherwise), with the validator re-checking it as a fail-closed mirror (REQ-V-15). ## 4. Minimal sound witness (load-bearing; `audit/03`, cross-checked GPT-5.5 `audit/04`) The witness must force **≥1 hardened CIP-1852 derivation to be recomputed in-circuit**. The leaked `a` is the wrong secret: soft CKD is additive over *public* parent material, so a soft-/leaf-anchored witness is forgeable by one linear solve when pubkey-binding or the carry-adder is weak (a real account-xpub being public suffices — no circuit bug needed); a flawlessly constrained soft circuit is instead HMAC-preimage-hard (~2²²⁴). Hardened anchoring is therefore required for **robust** soundness. Minimal sound anchor = coin_type `m/1852'/1815'`; **the design adopts the master XPrv** (3 hardened + 2 soft). **Sufficiency requires five further conditions** (each independently forgery-enabling if omitted): (i) hardcode hardened mode byte `0x00` and the hardened index constants; (ii) fully range/carry-constrain the no-mod-L adders; (iii) canonical limb/point encodings; (iv) exact 256-bit scalar handling incl. `s ≥ L` aliasing; (v) in-circuit clamp. ## 5. Circuit complexity In-circuit steps 3–4 ≈ **3.5–5.0M R1CS** (HMAC-SHA512 dominates ~2M; 3 fixed-base Ed25519 mults ~1.2M; Blake2b/Merkle ~0.4M; carry/range/clamp ~0.3M). Proving the full chain incl. Icarus PBKDF2 (~16k SHA-512 compressions ≈ 8×10⁸) is infeasible, which fixes the client-side/in-circuit boundary. ### 5.1 Circuit inventory and K-sizing Groth16 over R1CS uses an FFT domain of the next power of two ≥ the constraint count; the phase-1 Powers-of-Tau and the per-circuit phase-2 ceremony must both reach that **`K = ⌈log₂(constraints)⌉`**. | Circuit | Purpose | Constraints | **K (2ᴷ domain)** | Count | |---|---|---|---|---| | **Core recovery** (master XPrv → `C`: clamp + 3 hardened + 2 soft CKD-V2 + `A=aB` + `C=Blake2b-224(A)` + entitlement well-formedness + Blake2b-256 Merkle-14 inclusion + Blake2b-256 public-input binding) | production | **3,450,403** (full `Recovery` relation compile, `proto/circuit/derivation/REPORT.md` "Cost / K"; supersedes the earlier `~3.21M` simplified-harness figure in `FULL-CIRCUIT-K.md` §8, which omitted entitlement/version/domain-tag plumbing and used Blake2b-224 rather than Blake2b-256 for the Merkle hash — see §13 Merkle-hash-family entry) | **22** (2²²=4.19M, ~0.74M margin) | **1** | | Reduced bring-up (1 hardened + 2 soft) | E2 dev only | ~1.5–2.5M | 21 | 1 (dev, not deployed) | | Byron / V1 (HD-Random) derivation | only if legacy Byron credentials are in scope | ~similar | 22–23 | **0** (excluded unless required) | **How many: one production circuit.** It is the *only* SNARK circuit the system needs, because: - **`role ∈ {0,1,2}`, `account_index`, `address_index`, and the Merkle path are circuit inputs, not structure** — so a single circuit covers payment, change, and stake credentials and every address index. Merkle depth is fixed at `⌈log₂ 8823⌉ = 14`. - **Master-key-generation is client-side**, so the circuit consumes the 96-byte master XPrv and performs only the *common* ed25519-bip32 **V2** CIP-1852 derivation. It is therefore **master-generation-agnostic** across Icarus/Ledger/Trezor *given a compatible 96-byte root XPrv and matching V2 derivation semantics*, with one circuit. **Precise claim (audit/06 F-10):** the circuit proves knowledge of a *compatible master XPrv* that derives to `C`, not, in-circuit, that the XPrv came from a 24-word BIP-39 mnemonic — PBKDF2/BIP-39 run client-side and are out of circuit. This is sound for recovery because the master XPrv did not leak (only the leaf scalar did); user-facing materials must state it as "knowledge of the wallet's master key" rather than implying the phrase is proven inside the circuit. (Byron-era V1/HD-Random derivation differs and would be a second circuit; excluded unless legacy Byron recovery is required.) - **No circuit is added by batching.** Tier-1 RLC batches N proofs of *this same* circuit at the validator level; Tier-2 SnarkPack/TIPP-MIPP is an inner-pairing-product argument over an **SRS**, not a new R1CS circuit. (Only *recursive* aggregation would add a second, very large verifier-in-circuit — deliberately avoided.) **Ceremony consequence:** one phase-1 Powers-of-Tau at **K=23** (reusable; ~2²³ G1+G2 ≈ a few hundred MB; sourceable from an existing perpetual PoT ≥ 2²³) + **one** phase-2 per-circuit ceremony for the core circuit. The Tier-2 aggregation SRS is sized separately by the maximum aggregated batch length (a power of two ≥ N), not by K, with two independent commitment-key vectors (§9, REQ-B-06). **The core circuit is K=22** — the full `Recovery` relation compile measures **3,450,403** constraints < 2²² (4,194,304), with ~0.74M margin (`proto/circuit/derivation/REPORT.md` "Cost / K"; supersedes the earlier `~3.21M` simplified-harness figure in `FULL-CIRCUIT-K.md` §8, which omitted entitlement/version/domain-tag plumbing and used Blake2b-224 rather than Blake2b-256 for the Merkle hash — see §13's Merkle-hash-family entry). The earlier per-gadget sum (~5.5M, K=23) over-counted: gnark shares ONE range-check/lookup table across all gadgets, so each extra SHA-512 compression costs the ~63k marginal, not the 193k first-block, and summing 26 gadgets standalone re-counts that shared table. HMAC remains the dominant term (10 invocations, the majority of the total after amortization). Proof shape: the production (uints) circuit emits one Pedersen commitment, so it ships with a **commitment-aware verifier** (§8, §13, audit/12), not the vanilla 3-element path. ### 5.2 Circuit integration requirements (gadget audit, audit/08–09) The emulated Ed25519 scalar-mult gadget passed internal QA and external audit (SOUND after F1/F2). The audit converts into binding requirements for wiring the **full** circuit, where soundness now lives: - **One canonical `kL` bit vector.** Each `kL` (leaf and every soft-step parent) MUST be a single 256-bit little-endian vector that is BOTH the output of the no-mod-L CKD adder AND the input to `ScalarMulBaseBits`. No second decomposition or re-encoding anywhere. The point output cannot pin the scalar representative (`s·B = (s mod L)·B`), so `s`-vs-`s+L` aliases MUST be rejected at the derivation level — by constraining the exact CKD bytes and carries — not by the curve point (closes E25519-01; cf. `audit/03` condition iv). - **bit 255 pinned everywhere.** The gadget asserts `bits[255]=0` (F2); the full circuit's derived leaf/soft-parent scalars must satisfy this by construction (the master clamp + bounded V2 additions guarantee it) and be tested as such. - **Range-checked Compress→Blake2b handoff.** The 32 compressed-point bytes MUST enter the Blake2b-224 gadget through a range-checked byte API (`uints.U8`), never as raw field elements (E25519-04). - **Pinned proving stack.** Pin gnark **v0.15.0** for the ceremony circuit; re-audit `Field.Mux`/`Div`/`ToBitsCanonical` and 4×64-bit limb overflow before any gnark upgrade, with a regression test that detects a semantics change (E25519-05). - **Isolation tests.** Add an F1-isolating negative (call the gadget without caller-side booleanity; a non-boolean witness must be rejected by the gadget), and promote the QA probes (fresh oracle differential, cross-mismatch negative, `s∈{0,L,L+1}`) into committed CI (E25519-02/03). ## 6. On-chain verification — single proof (verified against live cost model E) | Step | CPU | |---|---| | Uncompress A,C (G1) + B (G2) | 180,594,716 | | IC (1 aggregated input): scalarMul + add | ~77,395,341 | | 4 millerLoop (or 3 if αβ precomputed to GT) | 1,016,025,092 | | 3 mulMlResult + finalVerify | 6,522,114 + 333,849,714 | | **Total** | **~1.36–1.61 × 10⁹ ≈ ~14–16% of the 10¹⁰ budget** | The table above is the **vanilla 3-element** baseline. The shipped circuit is the **uints** circuit (§5.1, §13), whose proof carries one Pedersen commitment, so the on-chain verifier is **commitment-aware** and adds a *measured* delta of **~1.03 × 10⁹ CPU** (`proto/onchain/COMMITMENT-VERIFIER-COST.md`, a Plutus prototype whose primitives reproduce this table to <0.2%): | Commitment-aware delta (per claim) | CPU | |---|---| | Opening pairing `e(D,[−σ]G)·e(π,G)=1` (dominant) | 844.6M | | Uncompress `D`, `π` (2× G1) | 106.0M | | Fold `Hash(D)·K_c + D` into `vk_x` | 78.7M | | Hash-to-field of `D` (Blake2b→Fr) | 4.2M | **Single-claim total = vanilla (1.36–1.61 × 10⁹) + delta (1.03 × 10⁹) ≈ 2.4–2.6 × 10⁹ ≈ 25–26% of the 10¹⁰ budget.** 192-byte vanilla proof + the commitment `D` and PoK `π` (2× G1). Conditions otherwise unchanged: single aggregated input, O(1) on-chain state, balanced fixed-depth tree. (Bit-decomposition — vanilla proof, no delta — was rejected: it is K=24–25 vs the uints K=22; see §13.) ## 7. Batch & aggregated verification (van Rossem / Protocol v11) van Rossem (live on preprod v11; mainnet pending) adds **BLS12-381 multi-scalar multiplication, CIP-133** (`G1_multiScalarMul = 321,837,444 + 25,087,669·n`) and `expModInteger` (CIP-109), built for on-chain ZK verification. Recovery must scale to ~8,823 credentials, so verification throughput is a first-class design axis. Two tiers. ### 7.1 Tier 1 — random-linear-combination (RLC) batch N proofs sharing one vk are checked together. With per-batch challenge scalars `rᵢ`: ``` Πᵢ e(rᵢAᵢ, Bᵢ) · e(−Σrᵢ·vk_xᵢ, γ) · e(−Σrᵢ·Cᵢ, δ) · e(−(Σrᵢ)·α, β) = 1 ``` `Σrᵢ·Cᵢ` and the `vk_x` aggregation are **MSMs (CIP-133)**; the `Bᵢ` are distinct in G2, so the `e(rᵢAᵢ,Bᵢ)` terms remain N separate miller loops — that is the inherent floor of RLC batching. Cost (live cost model E): - Per-proof marginal ≈ uncompress 180.6M + `rᵢAᵢ` scalarMul 76.4M + 1 millerLoop 254.0M + MSM slope 25.1M + mulMlResult 2.2M ≈ **0.538 × 10⁹**. - Fixed ≈ MSM intercept 321.8M + vk_x agg 153.8M + α scalarMul 76.4M + 3 millerLoop 762.0M + finalVerify 333.8M + overhead ≈ **1.66 × 10⁹**. - **Total ≈ 1.66 × 10⁹ + 0.538 × 10⁹ · N.** | N | CPU | % of 10¹⁰ budget | |---|---|---| | 1 | ~2.2B | ~22% (RLC overhead makes N=1 wasteful) | | 5 | ~4.35B | ~44% | | 10 | ~7.04B | ~70% | | 15 | ~9.73B | ~97% (CPU-bound ceiling) | So **~10–15 claims per transaction**, vs ~6 full single-verifies (~9.6B) unbatched — and the collapse of N finalVerifies/γ/δ pairings to one set is the saving MSM unlocks. **Caveat (audit/05):** this table excludes per-claim `pub`/entitlement reconstruction MSMs, the running-root sparse-Merkle non-membership/insert payloads, and the subgroup checks the soundness controls require; memory (16.5M) and `maxTxSize` (16,384 B) likely bind before CPU. The N ceiling MUST be re-derived on preprod v11 with all controls on — and a soundness control MUST NEVER be traded for throughput. RLC is the near-term, low-trust path: no extra setup beyond the base Groth16 ceremony. **Soundness invariants (Tier-1, normative).** The validator MUST compute exactly **N independent miller loops** `e(rᵢAᵢ,Bᵢ)`, each with that proof's own `Bᵢ`; the A-side MUST NOT be MSM-collapsed under a shared or prover-supplied `B`, and `Bᵢ` collisions are rejected (`Σrᵢ·Cᵢ` and the `vk_x` aggregation are the only MSMs, recomputed in-validator, never redeemer-supplied). The payout/nullifier loop MUST be a **single fused fold** over the same indexed set that enters the pairing, so no claim is paid whose `(rᵢAᵢ,Bᵢ)` term was not accumulated with `rᵢ≠0`. ### 7.2 Tier 2 — succinct proof aggregation (scaling endgame) An untrusted aggregator combines N Groth16 proofs into **one** O(log N) proof (SnarkPack-style TIPP/MIPP, inner-pairing-product arguments), verified on-chain with a **constant** number of pairings plus a few **log-N-sized MSMs (CIP-133)** — i.e. on-chain cost becomes ~flat in N for N in the thousands. This is the path to clearing all ~8,823 credentials in a handful of transactions rather than hundreds. Cost is approximately constant (a low single-digit billion CPU) for large N, dominated by a fixed pairing count and `O(log N)` MSM terms; the per-claim on-chain cost → ~0. The price is **new trust/soundness surface** (§7.4, REQ-B-06): TIPP/MIPP needs a structured reference string, and aggregation soundness must bind the exact ordered multiset of `(proof, public_input)` pairs. > **Status (audit/05): Tier-2 is UNSOUND as specified and stays off mainnet.** "Distinct > commitment keys" means **two independent secret exponents** (`a≠b`, neither derivable from > the other) — *not* two index ranges of one `τ`; a shared/related exponent collapses the > double-pairing binding. TIPP/MIPP recursion requires the batch length to be a power of two; > padding entries are a soundness-critical surface (REQ-B-06). Ship **Tier-1 RLC** > near-term; gate Tier-2 on a ceremony with base-Groth16 parity (§9). ### 7.3 Challenge derivation (mandatory soundness control) The RLC scalars `rᵢ` (Tier 1) and all aggregation challenges (Tier 2) **must** be derived by Fiat-Shamir from a Blake2b hash over the **full** batch contents — every `(Aᵢ,Bᵢ,Cᵢ,pubᵢ)`, the **true claim count**, the pinned **vk hash**, (Tier-2) the pinned **SRS hash**, and a per-tier **domain-separation tag** — in a byte-exact, length-prefixed, **ascending-by-`C`** canonical ordering, computed **in-validator**, never supplied in the redeemer. Each derived challenge MUST be mapped to `[1,q-1]` (explicitly nonzero); the validator MUST assert the nonzero-challenge cardinality equals the claim count and `Σrᵢ ≠ 0`. For Tier-2, `r`, all powers `rⁱ`, every TIPP/MIPP round challenge, and the final opening point `z` are all derived this way. A prover-chosen, zero, truncated, or padding-slot challenge lets an attacker craft proofs whose RLC cancels a forged term against a valid one while it is still nullified and paid. This is the central new requirement of the batch model. ### 7.4 New requirements introduced by batching > Normative; corrected by audit cycle 2 (`audit/05`). A faithful implementation of the > original six requirements was exploitable — see the BATCH-CONS findings. > SUPERSEDED FOR CITATIONS: `docs/07-batch-ears.md` refines and replaces REQ-B-01..06 > below, reusing the same identifiers with stronger definitions. Cite `docs/07` as the > authoritative source for all REQ-B-* requirements; the inline list below is retained for > narrative continuity only. - **REQ-B-01** Each batched/aggregated claim carries its own nullifier; the batch spends a distinct spent-map cell per claim, and the validator rejects intra-batch duplicate nullifiers (no two claims in one batch for the same `C`). - **REQ-B-02** The validator MUST subgroup- and on-curve-check **every** G1/G2/GT element before use — including in-validator-computed aggregates and (Tier-2) all aggregated A/B/C commitments, every GIPA round element, and opened commitment-key points — using explicit order-r/cofactor checks where an element is assembled on-chain rather than uncompressed; reject identity and small-order. - **REQ-B-03** Challenges derived in-validator by Fiat-Shamir over the entire ordered batch transcript (§7.3); each mapped to `[1,q-1]` with explicit nonzero check. - **REQ-B-04** (rewritten, critical) Each claim's payout output is matched 1:1 to a unique output index. The validator MUST **reconstruct each `pubᵢ` from authenticated context** (root/vk/version/scriptHash from the immutable datum; `Dᵢ` and `entitlementᵢ` from the actual paying output) and compute the challenge-weighted aggregate public-input term itself as a CIP-133 MSM — it MUST NEVER accept an aggregator-supplied `pubᵢ`, `vk_xᵢ`, or aggregated input (**REQ-V-06 applies per-claim**). The matched output MUST carry exactly the snapshot-committed entitlement reconstructed from the proven leaf; `Dᵢ` MUST NOT equal any custody/script address; outputs MUST be partitioned into disjoint index-ranged roles (continuing custody vs per-claim payout). The batch MUST satisfy `Σ(custody inputs) = Σ(payouts) + Σ(continuing custody) + fee`, payout delta equal to the sum of proven entitlements, fee drawn only from non-custody inputs. - **REQ-B-05** (replaced) If verification of an RLC or aggregated batch fails for any reason, the validator MUST reject the **entire** transaction, write no nullifier cell, and release no funds (**all-or-nothing**). The set of cells transitioned 0→1 MUST equal the set of claims paid MUST equal the FS-bound multiset — neither subset nor superset. (The earlier "invalidate only itself" clause is algebraically unsatisfiable: one GT bit in Tier-1, one O(log N) proof in Tier-2.) - **REQ-B-06** (rewritten, critical for Tier-2) The aggregated proof MUST be verified against the immutable on-chain-pinned **vk hash, circuit hash, AND aggregation-SRS hash**; the SRS hash MUST cover the entire commitment-key vectors plus the KZG verification elements (or a pinned sub-accumulator root with per-slot inclusion proofs); any reference-input SRS MUST be locked under an always-fails script. The SRS MUST come from a public reproducible ceremony deriving the two TIPP/MIPP commitment-key vectors from **two independent secret exponents** with a mandatory beacon/VDF. The validator MUST verify the KZG openings of `v_final`/`w_final` at the in-validator FS point in addition to the inner-pairing-product equations. The proof MUST bind the exact ordered multiset of `(C,pub)`; where `N` is padded to a power of two, the true count MUST be bound into the transcript and every padding slot constrained to a fixed non-identity unclaimable sentinel; padded `N > D_max` (pinned with the SRS hash) MUST be rejected. - **REQ-B-07** (economics) An explicit capped in-protocol aggregator fee, folded into each `pubᵢ` and the conservation equation (REQ-B-04). - **REQ-B-08** (economics) An aggregator bond, slashable only for attributable invalidity, never for ordering races. - **REQ-B-09** (liveness) A guaranteed permissionless, cheap, un-starvable **single-claim fallback** path with the same state/value rules, so no victim depends on an aggregator. ## 8. Custody and EUTXO state - **Sharded custody.** Funds are split across many validator UTxOs (by credential range / per-claim tickets), never one monolithic pot — a single multi-asset UTxO can exceed the `Value` size limit (commingled custody holds >1,000 victim tokens/NFTs) and serializes all claims. `MaryEraValue` (CIP-153) optimizes the multi-asset value handling. - **O(1) spent state.** A **global sharded sparse-Merkle spent map** (root in a state UTxO, flipped 0→1 with a non-membership/update proof) or **pre-created per-credential claim tickets**. A token merely *named* by the nullifier is **not** self-sufficient against double-mint. An in-datum spent list (~8,823×32 B) bricks the contract — forbidden. - **Double-satisfaction** is checked at transaction level: each claim consumes a unique ticket/state cell and proves an exact value delta to a unique payout (REQ-B-04). Removal of the same-tx-output spend restriction (later Dijkstra era) would further ease atomic settlement, but is not assumed here. - **Batch spent-state authority (audit/05).** Every batch claim MUST route its spent-cell update through the **single global spent-state authority**, with the consumed shard UTxO's committed index equal to `canonical_prefix(nullifier)` and non-membership verified against the **running intermediate root** (validator recomputes the final root). Shard width is pinned immutably. Two batches consuming disjoint custody UTxOs MUST NOT independently settle the same credential. - **Version/nullifier decoupling (audit/05).** The spent-map key MUST be stable across snapshot versions. **SP2 adopts option 1 (version-stable):** the nullifier is keyed as `Blake2b(domain_sep‖scriptHash‖C)` with `snapshot_version` bound into `pub` for eligibility (§3.4), so the spent-state is inherently stable across versions at a given `scriptHash` and no per-version migration is required. The alternative (option 2 — initialize each new-version shard from the prior version's accumulator root via a verified migration, empty re-init rejected) is thereby superseded on the version axis; the cross-`scriptHash` redeploy migration (REQ-TS-15) is unchanged. ## 9. Trusted setup Groth16 needs a per-circuit ceremony; retained toxic waste forges arbitrary claims. Required: reproducible circuit build, frozen constraint hash, independent circuit audit, public MPC transcript with contribution verification, on-chain pinning of **both** vk hash and circuit hash. **Shard custody so one setup/circuit failure cannot drain the whole pot.** Tier-2 aggregation introduces a **second trusted-setup surface co-equal with the Groth16 ceremony**: a retained or non-independent TIPP/MIPP trapdoor forges *every* aggregated claim. The aggregation SRS MUST receive the same controls as the Groth16 ceremony (independent contributors, mandatory beacon/VDF, public transcript, immutable on-chain pinning of the full keys), and custody MUST be sharded so one SRS failure cannot drain the pool. Tier-2 stays off mainnet until its ceremony reaches base-ceremony parity (REQ-B-06). ## 10. Client prover Fully offline, reproducible, audited builds. The 24 words and master XPrv never touch the network; the ZK proof protects on-chain privacy, **not** the seed during proving — UX must make master-XPrv exposure explicit and never route seeds through web apps (report's anti-seed-collection guidance). ## 11. Threat model (summary; full catalogue `docs/03`, corrections `audit/04`) Top residual risks, in priority order: (1) under-constrained foreign-field/carry/encoding gadgets injecting a leaf scalar downstream of the honest hardened anchor; (2) trusted setup (toxic waste, Sybil contributors, honest ceremony over a semantically weakened circuit, on-chain vk substitution); (3) EUTXO state (per-UTxO nullifiers → distributed double-claims; double-satisfaction; datum growth); (4) client/supply chain (plaintext seed outside every ZK guarantee). **Batch layer (audit cycle 2, verdict SOUND_WITH_REQUIRED_CHANGES for Tier-1, UNSOUND-as-specified for Tier-2; full catalogue `audit/05`):** the decisive findings were dropping per-claim `pubᵢ`/`Dᵢ` reconstruction at batch scale (aggregator redirect), single-sum value delta (entitlement swap/siphon), unsatisfiable partial-failure, and an under-pinned Tier-2 SRS. All are folded into REQ-B-01..09, §7.1–7.4, §8, §9 above. Tier-1 RLC ships with those changes; Tier-2 waits for ceremony parity. ## 12. Requirements and deployment Full EARS set: `docs/04` (99) plus REQ-B-01..06 here. Deploy and measure on **preprod v11** (van Rossem live there; mainnet pending) before any mainnet target; re-measure all costs against live preprod params, accounting for the van Rossem PCM re-costing of some primitives. ## 13. Open items - **Proof shape decision — RESOLVED** (audit/11, audit/12, `FULL-CIRCUIT-K.md`): ship the **uints circuit (K=23) with a commitment-aware verifier**, not bit-decomposition. Measurement (composed compile, `FULL-CIRCUIT-K.md` §8): uints **~3.21M → K=22** (fits, ~1M margin under 2²²; the per-gadget sum's ~5.5M/K=23 over-counted the shared lookup table); bit-decomposition ~10.5–26.7M → K=24–25 (does not fit; no shared-table amortization, and bit-decomposing the dominant hash gadgets costs ≥2 extra K). The uints proof carries one Pedersen commitment; commitment-batching is SOUND-WITH-CHANGES for the mainnet paths (single-claim + Tier-1 RLC; audit/12, 6 new commitment-path REQ-B in `docs/07`). **Flip condition:** revert to bit-decomposition at K=24 only if mainnet scaling is later made to depend on Tier-2 aggregation, which is unsound with commitments. Remaining build work: the commitment-aware Plutus verifier + its measured cost (§8), and the authoritative composed compile (confirmation only). - **Nullifier migration on validator upgrade** (audit/11 F-11): the nullifier is keyed on `scriptHash`, so a validator redeploy with a new hash creates a fresh nullifier namespace and could reset spent status. Define the migration rule: carry the spent map forward on upgrade, or add a stable, immutably-governed recovery-instance id to the domain so spent status survives script-hash changes. - **Soundness gate is not analyzer-certified** (audit/11): Picus/cvc5 do not decide these BLS12-381 circuits (even a 1-byte bit-decomp adder; `REPRO-picus.md`). The gate is named trust boundaries + differential + mutant + audit + Blaster (`docs/15`). Residual under-constraint risk is real; the current "negative" tests perturb public outputs (completeness), not constraints — true mutant testing (delete-a-constraint, adversarial witness) and a hand algebraic proof of the CKD adders are still owed. - **Build the full derivation circuit** (audit/06 P0): the emulated Ed25519 fixed-base scalar-mult (no gnark stdlib gadget — the critical path), SHA-512/HMAC-SHA512 ports, the exact no-mod-L carry adders, and canonical encodings, with a fail-closed negative-test suite for all five sufficiency conditions. No ceremony or mainnet path before this exists. - **Merkle hash family (FROZEN, 2026-07-02, corrected 2026-07-02 — see CL-002):** `H = Blake2b-256` (native 32-byte digest) for the Merkle leaf and internal-node hash — a distinct instantiation from the credential hash `C = Blake2b-224(A)` (28-byte digest) already fixed elsewhere in this document; `C` is only one *input* to the leaf preimage below, not the Merkle hash function itself. Both are the same underlying Blake2b compression core, generalized to a parameterized output length (`proto/circuit/derivation/hash/blake2b.go`), so this is one audited gadget family at two output-length parameterizations, not two hash primitives. Leaf: `H(0x00 ‖ C ‖ entitlement ‖ snapshot_version)` (matches §3.3's `entitlement`; same value as §3.1's `entitlement_encoding` and the `Ent` witness field in `proto/circuit/derivation/drv/circuit.go` — one field, three names in this document/codebase, noted here rather than silently disambiguated), where `C` is 28 bytes, `entitlement` is the 553-byte canonical encoding (`ada(8, LE) ‖ count(1) ‖ 8 × slot`, `slot = policy_id(28) ‖ asset_name(32) ‖ qty(8, LE)`; canonicity rules — zero-quantity rejection, sort order, dedup — and the full slot-field pinning now live in `docs/07-batch-ears.md`'s "Entitlement encoding" section, CL-005), and `snapshot_version` is 8 bytes little-endian. Internal node: `H(0x01 ‖ left ‖ right)`, each operand the full native 32-byte `Blake2b-256` digest of its child (leaf or node) — no truncation at any level. Merkle root is therefore 32 bytes. Depth fixed at 14 (already pinned elsewhere in this document). Decided over Poseidon2 because (a) both output-length parameterizations of Blake2b reuse one already-audited gadget (`Blake2b(uapi, in, outLen)`), so adopting Blake2b-256 for the Merkle hash alongside Blake2b-224 for the credential hash costs no new primitive, whereas Poseidon2 would add an arithmetic-hash gadget family with its own round-constant sourcing and audit burden; and (b) the K-budget objection that motivated considering Poseidon2 is stale. The full `Recovery` relation (`proto/circuit/derivation/drv/circuit.go`, the reference implementation of this document's §3.3) — clamp + 3 hardened + 2 soft CKD-V2 + `A=aB` + `C=Blake2b-224(A)` + entitlement well-formedness + Blake2b-256 Merkle-14 inclusion + Blake2b-256 public-input binding — measures **3,450,403 constraints, K=22** (`proto/circuit/derivation/REPORT.md` "Cost / K"), below both the ~5M/K=23 Blake2b-Merkle design estimate and even the ~3.98M/K=22 Poseidon2-swap estimate that motivated considering it; per that report, "swapping the Merkle hash to Poseidon2 would cut the Merkle term further but is not required to land at K=22." (An earlier, simplified measurement harness, `proto/circuit/fullcircuit/full.go` / `FULL-CIRCUIT-K.md` §8, used Blake2b-224 for the Merkle hash and omitted the entitlement/version/domain-tag plumbing; it predates and is superseded by the `proto/circuit/derivation` package for sizing purposes, though its K=22 headroom conclusion happens to still hold either way.) This decision is final for v2; changing it requires a new frozen-decision entry here, not a silent edit. - **Full Groth16 verifier on preprod** (audit/06 F-06/P1): the E0 lock+spend submit round-trip is now DONE for the HelloPairing pairing validator on Preview (lock `33b2125e…`, spend `ce784e6e…`, validator ran on-chain). STILL PENDING: a *full Groth16 verifier* (not just a pairing check) measured on-chain with live params. - **Deterministic proof randomness needs a formal ZK/linkability/subliminal-channel analysis** before it sits on any normative path (audit/06 F-09); until then it is a research item, not a requirement. - Independent verification of the batch/aggregation soundness claims. - Confirm `MaryEraValue` (CIP-153) builtin surface on the preprod v11 cost model. - Tier-2 aggregation SRS sourcing and its ceremony (hard-blocked from mainnet until parity). - Re-verify van Rossem live status + cost model against a live node immediately before any deployment (audit/06 F-12). - Sharded sparse-Merkle spent-map vs claim-ticket tradeoff, measured under nested-tx (future Dijkstra) vs current Conway settlement.