# EARS requirements

<!-- Derived from the board report (C:/emurgoaudit/latex/board_report.pdf) and the source audit (C:/proof/audit). Cardano ZK recovery contract; research+spec pass; 2026-06-25. -->

## Consolidated EARS requirements (de-duplicated, grouped by domain)

Duplicates across the raw set are merged into one canonical requirement and the superseded ids are noted. New requirements surfaced by the threat model are marked [HARDENING].

### D1 — Proof statement (legitimacy relation, public inputs, ZK)
- **REQ-D1-01 (ubiquitous)** — Private witness is exactly (master_xprv 96B = kL||kR||chaincode, CIP-1852 path, merkle_path, entitlement_preimage, D address bytes); the standalone leaf scalar a is never a sufficient input. *Acc:* a witness lacking master_xprv or supplying a soft/leaf key fails proof generation. *Cite:* audit F3 (58-60,89-91); CIP-3.
- **REQ-D1-02 (ubiquitous)** — Circuit computes ONLY steps 3-4 (CIP-1852 V2 CKD, A=aB, C=Blake2b-224(A)); it computes NO BIP-39 decode and NO Icarus PBKDF2. *Acc:* R1CS shows CKD + 1 base mult + per-soft point mult + 1 Blake2b-224, zero PBKDF2 iterations. *Cite:* audit F3 (61-91); rust-ed25519-bip32 mod.rs:44-57.
- **REQ-D1-03 (ubiquitous)** — master_xprv is derived CLIENT-SIDE (BIP-39 + PBKDF2-HMAC-SHA512, 4096 iter, 96B, clamp) and supplied as a plaintext witness consistent with `XPrv::normalize_bytes_force3rd`. *Cite:* audit F3 (58-60); CIP-3.
- **REQ-D1-04 (complex)** — On proof generation, attest knowledge of a witness s.t. C=Blake2b-224(A) derived from master_xprv along path equals the leaf authenticated by merkle_path under public merkle_root (the credential→entitlement snapshot). *Acc:* off-snapshot C ⇒ no satisfying path ⇒ generation fails. *Cite:* audit F3 (68-69); CIP-19.
- **REQ-D1-05 (ubiquitous)** — One `role` signal (∈{0,1,2}) drives both the role-level CKD index and the bound public commitment, so a payment proof cannot claim staking. *Defends* T1-9. *Cite:* CIP-1852.
- **REQ-D1-06 (ubiquitous) [REVISED]** — Public input is exactly ONE aggregated field element committing to (domain_sep, scriptHash, snapshot_version, merkle_root, C, entitlement, D, role); the on-chain verifier reconstructs it solely from datum + tx outputs + recorded nullifier. *Supersedes* the four-input form. *Defends* T4-1, T4-6. *Cite:* CIP-381; CIP-19.
- **REQ-D1-07 (event-driven)** — A claim binds the FULL destination address D into the public commitment; any alteration of D invalidates the proof. *Defends* T2-8, T5-5. *Cite:* Cardano mempool front-running.

  **Destination-binding scope (frozen 2026-07-02, CL-004):** binding covers
  the full destination output address only — not ref-script or other
  spendability-affecting datum fields; `docs/SPEC.md`'s broader phrasing is
  corrected to match this EARS requirement, not the reverse (EARS is
  normative for implementers). **Address form:** both 29-byte enterprise
  addresses and 57-byte base addresses are valid destinations; the encoded
  byte length is read from the address's own CIP-19 header byte, not assumed
  fixed-width — a cleanroom implementer must branch on the Cardano
  address-header tag, not hardcode one width. This corrects, rather than
  documents, current production behavior: the deployed circuit
  (`proto/circuit/derivation/drv/params.go`, `AddrLen=57`) hardcodes a single
  57-byte destination width today, so 29-byte enterprise destinations are
  silently unusable in production even though the on-chain validator's
  `encodeAddr` (`proto/onchain/redemption/src/RedemptionValidator.hs`)
  already encodes both widths (`audit/25-design-spec-assurance-review.md`
  ADV-2). A cleanroom v2 implementation MUST support both widths from the
  start rather than carry ADV-2's completeness gap forward.
- **REQ-D1-08 (ubiquitous)** — nullifier = Blake2b(domain_sep || scriptHash || C), a pure function of C and instance identity with no free witness input. snapshot_version is deliberately EXCLUDED from the nullifier (including it would give the same leaked C a distinct nullifier per snapshot version, allowing a double claim); snapshot_version is bound in `pub` for eligibility instead. Matches SPEC §3.4. *Merges* CE-07, TXB-05 nullifier clauses. *Defends* T1-3, T2-3, T2-5.
- **REQ-D1-09 (unwanted)** — A claim whose nullifier is already recorded spent is rejected and releases nothing. *Merges* CE-08, TXB-06.
- **REQ-D1-10 (unwanted)** — A witness anchored below the hardened levels (account-/role-level XPrv, or a alone) is inadmissible; ≥1 hardened CKD must be recomputed in-circuit. *Defends* T1-6. *Cite:* audit F3 (93-99); mod.rs:69-76.
- **REQ-D1-11 (ubiquitous)** — Zero-knowledge: master_xprv, kL, kR, chaincode, intermediate keys, a, and the mnemonic never appear in public input, redeemer, or datum; a documented simulator argument accompanies the Groth16 instantiation. *Defends* T5-1.
- **REQ-D1-12 (ubiquitous)** — Verify as Groth16 over BLS12-381 via Plutus V3 `bls12_381_millerLoop`/`finalVerify` with G1/G2 add/scalarMul, binding reconstructed public inputs to the equation. *Cite:* CIP-381.
- **REQ-D1-13 (ubiquitous) [HARDENED]** — domain_sep is a genuine PUBLIC INPUT reconstructed on-chain from the validator's scriptHash and snapshot_version (NOT a circuit constant), so proofs/nullifiers cannot replay across instances or versions. *Defends* T2-5, T4-12.
- **REQ-D1-14 (ubiquitous)** — Reconstruct A=scalarmult_base(leaf scalar) and C=Blake2b-224(A) byte-identically to the ledger keyhash construction. *Acc:* in-circuit Blake2b-224(aB) == ledger keyhash on vectors. *Cite:* CIP-19; audit F3 (68-69).
- **REQ-D1-15 (unwanted)** — The circuit MUST reject any witness whose destination `D` pays back to the claimed credential: the payment credential of `D` (bytes `[1:29]` of the 57-byte Shelley base address) MUST NOT equal `C`, so a valid proof is uncreatable when recovery would return funds to the (compromised) claimed key. Scope: the *claimed* credential only; the staking credential is unconstrained (it does not gate spending). Enforced in-circuit, not via client UX. *Acc:* `test.IsSolved` rejects an otherwise-valid witness with `D[1:29]==C` (`drv.AssertDestinationNotClaimed`). *Defends* T2-10 (compounds T5-5/T5-6). *Cite:* CIP-19.

### D2 — Derivation circuit (the in-circuit gadget contract)
- **REQ-DC-01 (ubiquitous)** — Root witness is the 96B master XPrv (kL||kR||cc); no PBKDF2/BIP-39 sub-circuit; derivation-path constraint count in low millions. *Cite:* key.rs:18,44-48; CIP-3.
- **REQ-DC-02 (ubiquitous)** — Enforce Icarus clamp: kL[0]&0xF8==kL[0], kL[31]&0xC0==0x40, kL[31]&0x20==0 (range-checked, not assumed). *Cite:* key.rs:53-59,143-156.
- **REQ-DC-03 (ubiquitous)** — Path shape hardcoded: 3 hardened (indices 0,1 = 0x8000073C, 0x80000717; account' ≥2^31) + 2 soft (role∈{0,1,2}, index <2^31); no wire selects level mode. *Defends* T1-5. *Cite:* CIP-1852; common.rs:14-22.
- **REQ-DC-04 (event)** — Hardened level: Z=HMAC-SHA512(cc_par, 0x00||kL_par||kR_par||le32(i)), I=(0x01||…). *Cite:* mod.rs:41-77.
- **REQ-DC-05 (event)** — Soft level: A_par=encode(scalarmult_base(kL_par)); Z=HMAC-SHA512(cc_par,0x02||A_par||le32(i)), I=(0x03||…). *Cite:* mod.rs:59-68; key.rs:425-427.
- **REQ-DC-06 (event)** — Index serialized as 32-bit little-endian le32(i). *Cite:* v2.rs:29-31.
- **REQ-DC-07 (event) [HARDENED]** — kL_child = add_28_mul8(kL_par, zL): per-byte arithmetic with 16-bit carry, no mod-L; **every output byte 8-bit range-checked and every carry constrained to its exact bit width**. *Defends* T1-1 (critical). *Cite:* v2.rs:1-16; mod.rs:84-92.
- **REQ-DC-08 (event) [HARDENED]** — kR_child = add_256bits(kR_par, zR), 256-bit LE sum, carry-out discarded, no mod-L; output bytes and the final carry range-checked. *Defends* T1-1. *Cite:* v2.rs:18-27.
- **REQ-DC-09 (event)** — cc_child = I[32..64] for both modes. *Cite:* mod.rs:94-99.
- **REQ-DC-10 (ubiquitous)** — Each HMAC-SHA512 is RFC-2104 over SHA-512: 32B chaincode key zero-padded to the 128B block (not pre-hashed), ipad 0x36/opad 0x5C, 64B tag; SHA-512 padding/length are compile-time constants for the fixed 37/69-byte preimages. *Defends* T1-8. *Cite:* mod.rs:56-57; RFC 4231; FIPS 180-4.
- **REQ-DC-11 (event)** — Leaf A=encode(scalarmult_base(s)), s the full 256-bit literal LE scalar, no mod-L; bit-identical to cryptoxide incl. s≥L and s≡0. *Defends* T1-7. *Cite:* cryptoxide ed25519.rs:92-105; scalar64.rs:92-118.
- **REQ-DC-12 (ubiquitous) [HARDENED]** — RFC-8032 compressed encoding: LE y in 0..31 with x-sign in MSB of byte 31; **y forced canonical (y<p, 19-value correction) and y=0 sign fixed to 0** before serialization; same encoding for soft parent points and leaf A. *Defends* T1-3. *Cite:* cryptoxide ed25519.rs:103-104; RFC 8032 §5.1.2.
- **REQ-DC-13 (ubiquitous)** — C=Blake2b-224(A): unkeyed, no salt/personalization, 28B digest over the 32B compressed key. *Cite:* CSL crypto.rs:3-7; CIP-19.
- **REQ-DC-14 (ubiquitous)** — Derived C is bound to equal the credential field inside the authenticated Merkle leaf (no free credential). *Defends* T4-1.
- **REQ-DC-15 (ubiquitous) [HARDENED]** — All Curve25519 base-field (p=2^255-19) and 256-bit scalar/key arithmetic emulated as foreign-field ops over Fr with EVERY limb canonically range-checked; reduction applied where the reference reduces and omitted where it does not (DC-07/08/11). Treated as a hard, negative-tested obligation. *Defends* T1-1, T1-2. *Cite:* CIP-381; audit F3.
- **REQ-DC-16 (unwanted)** — A soft-anchored (account-/role-level) root witness is rejected; the circuit always evaluates ≥1 hardened CKD level. *Defends* T1-6. *Cite:* audit F3 (93-99); mod.rs:69-76.
- **REQ-DC-17 (ubiquitous)** — Consistent little-endian/canonical byte interpretation across HMAC preimages, scalar loads, point encodings, and Blake2b input; one witness ⇒ one derivation; end-to-end C byte-matches the reference CSL/ed25519-bip32 pipeline. *Cite:* v2.rs:1-31; scalar64.rs:92-140; CSL derive.rs:13.

### D3 — On-chain verifier
- **REQ-V-01 (ubiquitous) [HARDENED]** — Datum carries the snapshot Merkle root and binds the SINGLE authorized VK as an IMMUTABLE script parameter (preferred) or its Blake2b-256 hash; never per-claim. *Defends* T3-5, T3-7. *Cite:* CIP-35.
- **REQ-V-02 (superseded 2026-07-02, CL-003).** The on-chain-verified proof is
  the **commitment-aware Groth16 form**, 336 bytes total, matching
  `README.md`'s deployed layout and `Recovery/Verify.hs`'s wire-format doc
  comment: the 192-byte vanilla prefix `A` (G1, compressed, 48B) ‖ `B` (G2,
  compressed, 96B) ‖ `C` (G1, compressed, 48B), followed by `commitment` (G1,
  **UNCOMPRESSED** `X‖Y`, 96B — the BSB22 Pedersen commitment point, carried
  uncompressed so the validator reconstructs the ZCash compression flag bits
  from `Y`'s sign itself rather than trusting a redeemer-supplied flag) ‖
  `PoK` (G1, compressed, 48B, the knowledge-of-opening proof). `192 + 96 + 48
  = 336` bytes. Redeemer parsing is total and size-bounded; the Merkle path
  and reconstruction values are separate redeemer fields, not part of the
  336-byte proof. The verifying key is 672 bytes: the 432-byte vanilla prefix
  (`alpha`(G1,48B) ‖ `beta`(G2,96B) ‖ `gamma`(G2,96B) ‖ `delta`(G2,96B) ‖
  `IC0`(G1,48B) ‖ `IC1`(G1,48B)) plus the commitment-key extension `K2`
  (G1,48B) ‖ `CK.G` (G2,96B) ‖ `CK.GSigmaNeg` (G2,96B) = `432 + 48 + 96 + 96
  = 672` bytes. See `docs/commitment-groth16-protocol.md` (Task 3 of this
  plan) for the exact prover-side construction and byte order. *Supersedes*
  the prior vanilla-proof (`A`‖`B`‖`C` only) wording of this requirement.
  *Cite:* CIP-381; `Recovery/Verify.hs` (`groth16VerifyCommitted`);
  `README.md` "Real numbers" / "Committed VK (672 bytes)".
- **REQ-V-03 (unwanted)** — Any VK (or α,β,γ,δ,IC) presented through the redeemer or any untrusted field ⇒ reject. *Defends* T3-7. *Cite:* audit (93-99).
- **REQ-V-04 (event)** — Ingest every point via `bls12_381_G1/G2_uncompress`; any failure (malformed or non-prime-order) ⇒ reject. *Cite:* CIP-381; Builtins.hs:115,126.
- **REQ-V-05 (event)** — Accept only if e(A,B)=e(α,β)·e(L,γ)·e(C,δ) holds via millerLoop/mulMlResult/finalVerify, L the IC linear combination. *Cite:* CIP-381.
- **REQ-V-06 (complex)** — Reconstruct the public input SOLELY from authoritative state (datum-proven leaf + tx-output D); any redeemer-supplied free public input ⇒ reject. *Defends* T4-1. *Cite:* audit (37-47).
- **REQ-V-07 (unwanted)** — If D is not bound as a public input (proof valid for a different paid D) ⇒ reject. *Merges* TXB-01/03. *Defends* T2-8.
- **REQ-V-08 (unwanted)** — Reject if #public-inputs ≠ |IC|−1 or any input ≥ group order r (validator enforces scalar canonicity; the builtin does not). *Cite:* CIP-381; Builtins.hs:623-624,666-667.
- **REQ-V-09 (event) [HARDENED]** — On success, single-spend is enforced via a GLOBAL authority (one-shot state-thread NFT every claim consumes+recreates, or deterministic shard), not a per-UTxO local set. *Defends* T2-1, T2-6. *Cite:* per-claim release; commingled custody.
- **REQ-V-10 (ubiquitous)** — Full per-claim execution (uncompress, IC muls, 4 pairings, mulMlResult, finalVerify, Merkle check) fits mem ≤14,000,000 and steps ≤10,000,000,000 with documented margin. *Defends* T4-6. *Cite:* Cardano param guide; CIP-9.
- **REQ-V-11 (ubiquitous)** — Minimize Groth16 public inputs to ONE aggregated field element so IC G1 scalar-mul count is bounded. *Defends* T4-6. *Cite:* CIP-381.
- **REQ-V-12 (ubiquitous)** — Redeemer (≈192B proof + aggregated input + max-depth Merkle path) + tx ≤ 16,384B; on-chain DATUM is O(1) in #credentials. *Defends* T4-5. *Cite:* Cardano param guide.
- **REQ-V-13 (unwanted) [HARDENED]** — Deploy/parameterize only with a VK bound (via a published conformance suite that the VK MUST pass, including a leaked-a forgery that MUST be rejected) to the exact hardened-anchored steps-3-4 circuit. *Defends* T3-3, T4-7. *Cite:* audit (93-99).
- **REQ-V-15 (unwanted)** — The validator MUST reject a claim whose bound destination `D` pays back to the claimed credential: the payment credential of `D` (its first 28 address bytes after the header) MUST NOT equal `cdCredential` (`C`). This is a fail-closed mirror of the in-circuit REQ-D1-15 — the proof is already uncreatable in that case; the on-chain check keeps the two layers in agreement and holds if a future circuit/VK regression drops the constraint. *Acc:* `validateClaim` returns False when `payCredOf D == C` (`Recovery.Logic`). *Defends* T2-10. *Cite:* CIP-19.

### D4 — Custody and entitlement
- **REQ-CE-01 (ubiquitous)** — Datum holds ONE Merkle root committing credential→entitlement (ADA + asset bundle) leaves. *Cite:* CIP-1852.
- **REQ-CE-02 (ubiquitous) [HARDENED, corrected 2026-07-02 — see `audit/33` AUD-04]** — Each leaf = `H(0x00 || C || entitlement || snapshot_version)`; internal node = `H(0x01 || left || right)`; `H` = Blake2b-256 (native 32-byte digest, no truncation); ONE hash family, domain-separated, fixed depth 14, injective encoding. `entitlement` is the fixed-width 553-byte canonical encoding (`ada(8, LE) || count(1) || 8 × slot`, `slot = policy_id(28) || asset_name(32) || qty(8, LE)`) — **not** a length-prefixed/TLV encoding; there is no length-prefix byte anywhere in the leaf preimage, and field widths are fixed, not variable. See `docs/SPEC.md` §13 (the frozen Merkle-leaf/hash-family note) for the leaf/node hash freeze, and `docs/07-batch-ears.md`'s "Entitlement encoding" section (CL-005) for the exact entitlement byte layout and its canonicity rules (zero-quantity rejection, sort order, dedup). *Defends* T1-4, T4-3. *Cite:* CIP-55.
- **REQ-CE-03 (event)** — Accept only if the proof's public credential is a leaf of the DATUM-committed root (not a caller-supplied root). *Cite:* recovery problem.
- **REQ-CE-04 (event)** — Authorize release iff (a) Groth16 verifies under the pinned VK, (b) C in committed root, (c) C's nullifier unspent, (d) requested sub-bundle ≤ residual. *Cite:* CIP-381.
- **REQ-CE-05 (unwanted)** — Reject unless an output pays the claimed sub-bundle to the proof-bound D. *Defends* T2-2.
- **REQ-CE-06 (unwanted)** — Reject if released-so-far + requested exceeds committed entitlement in any asset. *Defends* T4-2.
- **REQ-CE-07 → merged into REQ-D1-08** (nullifier deterministic from C, independent of a). 
- **REQ-CE-08 → merged into REQ-D1-09** (spent-nullifier ⇒ reject).
- **REQ-CE-09 (event) [REVISED]** — Track a monotonic released-so-far per credential in the global state; record the nullifier when residual reaches zero in every asset; cap by the MIN committed across all versions paid under. *Defends* T4-8.
- **REQ-CE-10 (unwanted)** — Reject fractional or >1 quantity of any quantity-1 NFT; allow partial release of divisible assets. *Cite:* CIP-55.
- **REQ-CE-11 (event) [HARDENED]** — On consuming custody UTxO(s), produce a continuing output under the same script carrying forward root + global state, with Σinputs = Σpayout(to bound D) + Σcontinuing (fee funded from NON-custody inputs only — see REQ-CE-12a); create/destroy no asset. *Defends* T2-2, T2-4. *Cite:* CIP-55.
- **REQ-CE-12 (ubiquitous)** — Every output (payout and continuing) meets min-ADA = (160 + |serialized output|)·coinsPerUTxOByte over full value + datum. *Cite:* CIP-55.
- **REQ-CE-12a (unwanted) [HARDENING]** — Reject if the transaction fee draws on consumed custody value; fee must come from a claimant-supplied non-custody input. *Defends* T2-4.
- **REQ-CE-13 (unwanted) [HARDENED]** — Setting/replacing the Merkle root requires the designated threshold AND must satisfy an append-only/monotone, solvency-bounded, publicly-reproducible constraint (REQ-CE-17); the VK is NOT governance-mutable (REQ-V-01). *Defends* T4-4, T4-7.
- **REQ-CE-14 (complex)** — On a governed root replacement, increment a strictly monotonic snapshot-version and carry forward the spent set and released-so-far unchanged. *Defends* T4-8, T4-12.
- **REQ-CE-15 (unwanted)** — Reject a proof whose snapshot_version differs from the committed version (version bound inside the proof per REQ-D1-13). *Defends* T4-9.
- **REQ-CE-16 (ubiquitous)** — Custody value leaves ONLY via the REQ-CE-04 claim path or the REQ-CE-13 governance path; no other spend branch. *Defends* T3-5, T4-7.
- **REQ-CE-17 (ubiquitous) [HARDENING]** — At root-commit time enforce an on-chain/governance solvency invariant Σada ≤ custody ADA and Σqty ≤ custody qty per asset, against the actual custody UTxOs, with a published independently-reproducible derivation. *Defends* T4-2.
- **REQ-CE-18 (ubiquitous) [HARDENING]** — Provide a bonded on-chain challenge/dispute path for omitted/understated credentials and an explicit published tie-break (pro-rata) rule for ambiguous commingled NFTs; root inclusion is append-only with an immutable audit trail. *Defends* T4-11.

### D5 — Trusted setup
- **REQ-TS-01 (ubiquitous)** — Per-circuit VK from a two-phase MPC: BLS12-381 Powers-of-Tau (Phase-1) + circuit-specific Phase-2. *Cite:* CIP-381.
- **REQ-TS-02 (ubiquitous) [HARDENED]** — Phase-2 has ≥3 independent sequential contributions AND terminates in a public-randomness beacon/VDF applied after the last human contribution, so soundness does not rest on any human and survives full human collusion. *Defends* T3-1, T3-2.
- **REQ-TS-03 (ubiquitous) [HARDENED]** — Contributors mutually independent across org/jurisdiction/toolchain, anchored to hard-to-Sybil public identities (live/in-person, identity proofs), each publishing a signed toxic-waste-destruction attestation. *Defends* T3-2.
- **REQ-TS-04 (event)** — On completion, publish the full Phase-1/Phase-2 transcripts, R1CS, compiler+version, proving key, and VK at an immutable content-addressed location referenced on-chain.
- **REQ-TS-05 (ubiquitous)** — Each transcript lets any third party verify every contribution and recompute the VK without trusting the coordinator.
- **REQ-TS-06 (ubiquitous)** — Bind each VK to a hash of the exact R1CS + compiler version; publish the (circuitHash, vkHash) manifest. *Defends* T3-3.
- **REQ-TS-07 (ubiquitous) [HARDENED]** — Pin the active VK as an IMMUTABLE script parameter; if a reference input carries VK bytes, that UTxO is under an always-fails script AND the validator asserts Blake2b-256(VK)==committed immutable hash before any pairing. *Defends* T3-5, T3-7.
- **REQ-TS-08 (event) [HARDENED]** — ≥3 independent reviewers (distinct orgs/toolchains), ≥1 auditing R1CS SEMANTICS against this spec, recompute the VK byte-for-byte before pinning, within a public time-boxed open-verification window; absence blocks pinning. *Defends* T3-3, T3-10.
- **REQ-TS-09 (unwanted)** — If the transcript fails, contributions < required, or recomputed VK ≠ proposed, do not pin and release no funds.
- **REQ-TS-10 (event) [HARDENED]** — Accept a proof only under the immutably pinned VK; any circuitHash retained is derived on-chain from the pinned VK and used only for off-chain provenance, never for VK selection. *Defends* T3-9.
- **REQ-TS-11 (event)** — Any R1CS change ⇒ new circuitHash, fresh Phase-2, new VK; the prior VK does not verify the upgraded circuit; migration is a constrained op carrying forward the spent-state accumulator (REQ-CE-14, REQ-TS-15). *Defends* T4-12.
- **REQ-TS-12 (unwanted) [HARDENED]** — VK change (if ever permitted) requires a quorum strictly larger and more independent than the fund-release quorum, a timelock, an independent veto set, and a republished binding + recompute report; the fund-release key may never rotate the VK. *Defends* T3-5.
- **REQ-TS-13 (unwanted)** — Reject proofs for a superseded circuit/VK; versioning is strictly monotonic and irreversible, with an on-chain revoked-VK set forbidding re-pinning any superseded VK. *Defends* T3-6.
- **REQ-TS-14 (ubiquitous) [HARDENED — was optional]** — Reuse a large public BLS12-381 Powers-of-Tau as Phase-1; MANDATORY verification of its transcript and that powers ≥ circuit constraint count before Phase-2; never run a bespoke low-participation Phase-1. *Defends* T3-8.
- **REQ-TS-15 (event) [HARDENING]** — Circuit migration initializes the new instance's datum from the verified prior-instance final accumulator (on-chain checked), conserves total value (Σin=Σout), and keys nullifier domain so already-claimed credentials remain spent across instances. *Defends* T4-12.

### D6 — Client prover
- **REQ-CP-01 (ubiquitous)** — Compute master_xprv and the full witness only in volatile local RAM; no remote/co-processor witness step. *Defends* T5-1. *Cite:* audit F3 (87-91); CIP-3.
- **REQ-CP-02 (ubiquitous)** — Mnemonic, entropy, seed, XPrv, chaincode, k_R, and intermediate scalars never written to disk/swap/logs/telemetry/crash dumps. *Defends* T5-3, T5-6.
- **REQ-CP-03 (state-driven)** — While any secret is loaded, all network interfaces closed, no network I/O. *Defends* T4-9.
- **REQ-CP-04 (unwanted)** — If a routable interface is up at secret entry, refuse the mnemonic and instruct air-gap.
- **REQ-CP-05 (event)** — On completion/abort/error, zeroize every secret buffer (non-elidable wipe) before release/exit; stream-derive and wipe each child scalar. *Defends* T5-4.
- **REQ-CP-06 (ubiquitous) [HARDENED]** — Lock secret pages (mlock/VirtualLock), disable core/crash dumps, AND explicitly wipe accelerator (GPU/FPGA) memory; prefer CPU-only on dedicated bare-metal with no DMA ports. *Defends* T5-4.
- **REQ-CP-07 (ubiquitous)** — Deterministic reproducible build; released digest re-derivable from pinned audited sources AND across ≥2 independent toolchains. *Defends* T3-4, T5-2, T5-3.
- **REQ-CP-08 (event) [HARDENED]** — Replace self-integrity check with EXTERNAL pre-run verification (pre-incident hardware-key signature via multiple channels, transparency log, OS notarization) gating secret entry. *Defends* T5-2.
- **REQ-CP-09 (ubiquitous)** — Derive via CIP-1852 V2 (3 hardened + 2 soft), A=aB, Blake2b-224, bit-exact with the on-chain circuit; prover keyhash == reference CSL keyhash on vectors. *Cite:* CIP-1852; mod.rs:44-57; CSL derive.rs:13.
- **REQ-CP-10 (unwanted)** — Reject a soft-only (account/role/index) anchored witness; only master/hardened-anchored accepted. *Defends* T1-6.
- **REQ-CP-11 (ubiquitous) [HARDENED]** — Emitted artifacts leak no secret and bind D; proof randomness (r,s) is derived DETERMINISTICALLY and an independent second tool recomputes the proof byte-for-byte before it leaves the air-gap. *Defends* T5-1, T5-5.
- **REQ-CP-12 (ubiquitous) [AMENDED 2026-07-13]** — Mnemonic captured only via the prover's own offline input control, with a persistent anti-disclosure warning; no web/remote seed path, with exactly one exception: delegated proving MAY transport the master XPrv to a remote prover whose SEV-SNP attestation has been Warden-verified against the measurements registered for the configured DappID AND whose TLS session is channel-bound to the attested enclave CA (`docs/temenos-recovery-integration-feasibility.md` §5.3/§6). Unverified or staging transports carrying real seeds remain prohibited — the client fails closed without an explicit staging opt-in. *Defends* T5-2, T5-6 (delegated-path analysis in the feasibility doc's §6 threat table).
- **REQ-CP-13 (ubiquitous)** — Never place mnemonic/entropy/XPrv on the clipboard or any IPC channel. *Defends* T5-6.
- **REQ-CP-14 (event)** — Direct the user to the signature-verifiable distribution and display the expected digest before any secret entry. *Defends* T5-2.
- **REQ-CP-15 (ubiquitous) [HARDENING]** — destination_commitment = published recomputable H(domain || full D address bytes); an independent tool / hardware wallet recomputes from the user-entered D and asserts equality, with full-D on-device confirmation, before signing. *Defends* T5-5.

### D7 — Transaction binding (merged with D3/D4 where overlapping)
- **REQ-TXB-01 → merged into REQ-D1-07 / REQ-V-07** (D a public input).
- **REQ-TXB-02 (event)** — The spend must create an output paying exactly the snapshot entitlement for C to the bound D. *Defends* T2-2. *Cite:* CIP-69.
- **REQ-TXB-03 → merged into REQ-V-07** (any released value to a non-bound payment credential ⇒ fail).
- **REQ-TXB-04 (unwanted) [HARDENED]** — Any consumed custody value other than the entitlement to D and the continuing output ⇒ fail; fee from non-custody inputs only (REQ-CE-12a). *Defends* T2-4.
- **REQ-TXB-05 → merged into REQ-D1-08 / REQ-V-09** (nullifier recorded in the GLOBAL state thread, not a per-UTxO datum).
- **REQ-TXB-06 → merged into REQ-D1-09**.
- **REQ-TXB-07 (unwanted)** — Replay-uniqueness keyed solely on the credential nullifier; never on (re-randomizable) proof bytes. *Defends* T2-3. *Cite:* Groth16 malleability.
- **REQ-TXB-08 (unwanted)** — The proof's public-input merkle_root must equal the root in the spent custody UTxO's datum. *Defends* T2-5. *Cite:* CIP-69.
- **REQ-TXB-09 (unwanted) [HARDENED]** — Reject an unbounded or post-deadline validity upper bound (read from txInfoValidRange); the deadline is generous and extend-only, never reachable downward by governance, with post-deadline residue routed to a victim-favoring escrow. *Defends* T4-9. *Cite:* CIP-69.
- **REQ-TXB-10 → merged into REQ-D1-07** (full address bytes incl. staking credential, no normalization). *Defends* T2-8.
- **REQ-TXB-11 (event)** — Release only after finalVerify against the pinned VK on the reconstructed aggregated public input. *Cite:* CIP-381.
- **REQ-TXB-12 (ubiquitous) [HARDENING]** — At most one recovery-claim script input per transaction, OR a single global value-conservation equation over the whole tx with each claim bound to a unique output index; no two claims share a payout output. *Defends* T2-2, T4-6.

### D8 — Cross-cutting (recovery intent vs cryptographic soundness)
- **REQ-X-01 (ubiquitous) [HARDENING]** — Where a credential's effective mnemonic entropy may be low, gate payout on out-of-band ownership evidence (pre-incident timestamped signed message, exchange/KYC linkage) and a manual-review/dispute window for high-value entitlements, because a sound proof alone cannot distinguish a lucky grinder from the owner. *Defends* T4-13.
- **REQ-X-02 (ubiquitous) [HARDENING]** — Support batched/aggregated claims and/or a fee-sponsoring relayer reimbursed from released value so small entitlements are not priced out by per-claim verification cost. *Defends* T4-10 economics, small-claim viability.