proof-zk-recovery

KO | EN

gitlite — search

#python #java #python3 #arduino #golang #machine-learning #rust #html #flask #javascript #seismology #nodejs

proof-zk-recovery

★ 17 Open GitHub ↗

ZK recovery contract: design, audits, and prototyping (private)

// repository documentation

Was this content helpful?

★ 0 (0 ratings)

# proof: zero-knowledge wallet recovery on Cardano

This repository builds one thing and proves it works: a way for someone who lost a wallet to get their exact funds back, on-chain, by handing the chain a zero-knowledge proof instead of a key. The funds were stolen because a wallet provider leaked the keys that sign transactions. The recovery does not use those keys. It uses the one secret the attacker never got, the master seed above them in the derivation tree, and it never reveals that secret to anyone, including the contract that pays out.

We did not stop at a design. We wrote the circuit, the prover, and the Plutus contract, deployed to the Cardano preview testnet, and watched a live node verify a real 3,450,403-constraint proof and release funds on the strength of it. The transaction hashes are in this README. If you want the readable version of the whole story, read [`product/zk-recovery-blog.md`](product/zk-recovery-blog.md); if you want the machine, keep reading here.

## What happened

A wallet provider got compromised, and what leaked was not seed phrases. It was the leaf signing scalars, the derived keys that actually sign transactions, for roughly 8,823 credentials. The cause was a deterministic-nonce bug: the shipped signer computed the EdDSA nonce as `r = H(M)` over the message alone, instead of `r = H(k_R ‖ M)` over the secret nonce prefix and the message. Two signatures over different messages then exposed the leaf scalar `a` by simple algebra. Once `a` is public, the account is anyone's, and no amount of "rotate your key" helps, because the key is the password and the password is on the internet now.

What did not leak is the whole reason recovery is possible: the recovery phrase, the BIP-39 entropy, the master seed, the secret nonce prefix `k_R`, and the chain code. In a hierarchical deterministic wallet, every leaf is derived from the master by a chain of one-way steps. You can walk down from the master to a leaf, but you cannot climb back up from a stolen leaf to the master. So the attacker holds leaves and no way up the tree, and the legitimate owner still holds the root. That asymmetry is the entire lever this project pulls.

## The idea

Recovery has to require something the attacker does not have, or it is just a footrace the attacker can win. The thing the attacker lacks is the master secret, so recovery means proving knowledge of the master that derives to an exposed credential. You obviously cannot hand the master to a contract; the moment it is on-chain it is public, and you have given the attacker the very thing you were protecting. So you prove you know it without showing it. That is a zero-knowledge proof, and it is the whole job.

One more property makes the proof safe to publish. The destination address, where the recovered money is allowed to land, is committed inside the proof itself. An attacker who sees your proof in the mempool and copies it cannot redirect the payout, because changing the destination invalidates the proof. The only address a recovery proof will ever pay is the one it was built for. You can broadcast it in the clear and not care who reads it.

## Architecture

The system is one relation `R` described four times over, and the discipline of the project is keeping those four descriptions saying the same thing. There is an English/EARS **specification** ([`docs/SPEC.md`](docs/SPEC.md), [`docs/04-ears-requirements.md`](docs/04-ears-requirements.md)), a gnark **circuit** that compiles `R` to constraints ([`proto/circuit/`](proto/circuit/)), a Plutus V3 **contract** that verifies a proof of `R` and releases funds ([`proto/onchain/redemption/`](proto/onchain/redemption/)), and **Lean proofs** that the contract's decision logic is sound ([`lean/`](lean/)). The reconciliation map in [`audit/15-alignment-reconciliation-map.md`](audit/15-alignment-reconciliation-map.md) tracks every place those four could disagree, and the review in [`audit/16-onchain-breakthrough-review.md`](audit/16-onchain-breakthrough-review.md) is the adversarial pass over the on-chain result.

Here is the whole system in one picture, from the victim's secret to funds landing in a fresh wallet:

```text
+==================================================================================================+
|         ZERO-KNOWLEDGE WALLET RECOVERY ON CARDANO  --  end-to-end design (top -> bottom)         |
+==================================================================================================+

##############################  TRUST BOUNDARY: VICTIM DEVICE (OFF-CHAIN)  #######################
  #  Secrets NEVER leave this box. Only a 336-byte proof + public address D cross the boundary.    #
  #                                                                                                 #
  #   +-------------------------------------+        +--------------------------------------+       #
  #   |  MASTER SEED  (24 words / mnemonic) |        |  FRESH NEW WALLET (clean keys)       |       #
  #   |  -> master XPrv                     |        |  -> destination address D (57 bytes) |       #
  #   +------------------+------------------+        +-------------------+------------------+       #
  #                      |                                               |                          #
  #   CIP-1852 / BIP32-Ed25519 derivation                               | (D is PUBLIC)            #
  #                      v                                               |                          #
  #   +-------------------------------------+                           |                          #
  #   |  leaf scalar kL                     |                           |                          #
  #   |  A   = compress(kL * B)             |                           |                          #
  #   |  C   = Blake2b-224(A)  (credential) |                           |                          #
  #   +------------------+------------------+                           |                          #
  #                      |                                              |                          #
  #                      v                                              v                          #
  #   +-----------------------------------------------------------------------------------+        #
  #   |  SINGLE PUBLIC INPUT                                                               |        #
  #   |  pub = Fr( Blake2b-256( domain_sep || scriptHash || snapshot_version              |        #
  #   |                         || root || C || entitlement || D || role ) )              |        #
  #   +------------------+----------------------------------------------------------------+        #
  #                      |        (master, path, Merkle siblings, entitlement = PRIVATE witness)    #
  #                      v                                                                          #
  #   +-----------------------------------------------------------------------------------+        #
  #   |  GROTH16 PROVER   (3,450,403 constraints, K = 22)                                  |        #
  #   |  proves: "I own a seed deriving C, C is in the snapshot at root, entitled to pay D"|        #
  #   |  output: 336-byte proof  (carries a BSB22 Pedersen commitment)                    |        #
  #   +------------------+----------------------------------------------------------------+        #
  ##########################|########################################################################
                            |   ONLY {  336-byte proof  +  public address D  }  leave the device
                            v
  +--------------------------------------------------+    +-------------------------------------+
  |  OPERATOR (OFF-CHAIN)                             |    |  CLAIM TRANSACTION (built by client)|
  |  - Eligibility snapshot:                         |    |  redeemer = ( proof_336B, D, role ) |
  |    Merkle tree depth 14 over (C, entitlement)    |    |  spends:   custody UTxO             |
  |    leaves  -> root pinned ON-CHAIN               |    |  CIP-30 wallet pays fee + collateral|
  |  - M-of-N governance: 3-of-5                     |    +------------------+------------------+
  |  - Custody funding: recovered funds locked at    |                       |
  |    the RedemptionValidator contract              |                       |
  +-----------------------+--------------------------+                       |
                          |  root, snapshot_version, scriptHash (params)     |
                          +-----------------------+--------------------------+
                                                  |  submit tx
                                                  v
  ###############################  TRUST BOUNDARY: CARDANO L1 (ON-CHAIN)  ###########################
  #   Plutus V3  RedemptionValidator   --  runs in consensus on a live Cardano node                #
  #                                                                                                 #
  #   STEP 1 - RECONSTRUCT pub FROM AUTHENTICATED CONTEXT (the client cannot forge it):             #
  #     custody datum (C, entitlement) + params (root, version, scriptHash) + redeemer (D, role)    #
  #                                       |                                                         #
  #                                       v                                                         #
  #   STEP 2 - groth16VerifyCommitted (the ZK verifier):                                            #
  #     (1) uncompress the commitment point                                                         #
  #     (2) Pedersen PoK pairing :  e(commitment, GSigmaNeg) . e(PoK, G) == 1                       #
  #     (3) challenge            :  e_cmt = expand_message_xmd(SHA-256, ...)                        #
  #     (4) fold vk_x            :  vk_x = K0 + pub*K1 + e_cmt*K2 + commitment                      #
  #     (5) final pairing        :  e(A,B) == e(alpha,beta) . e(vk_x,gamma) . e(C,delta)            #
  #                                       |  (proof valid)                                          #
  #                                       v                                                         #
  #   STEP 3 - PAYOUT CHECKS:                                                                        #
  #     encodeAddr(output) == D        (funds go to the proven fresh wallet)                        #
  #     encodeEntitlement(payVal) == entitlement   (exact owed amount, to the token)               #
  #     no self-pay                   (the operator cannot redirect to itself)                      #
  #                                       |  (all checks pass -> validator succeeds)                #
  #                                       v                                                         #
  #     RELEASE the exact entitlement from the custody UTxO  ==>  paid to address D                 #
  ##################################################################################################
                                          |
                                          v
  +--------------------------------------------------------------------------------------------+
  |  RESULT: funds arrive at the fresh wallet D.  The leaked / compromised key was NEVER used  |
  |          on-chain -- recovery is authorized purely by the zero-knowledge proof.            |
  +--------------------------------------------------------------------------------------------+
```

The relation itself is short to state and expensive to prove. I know a master extended private key. Run it down the standard Cardano path (CIP-1852 over BIP32-Ed25519) to a leaf scalar `kL`. Multiply the base point by it and compress, `A = compress(kL·B)`, and hash that, `C = Blake2b-224(A)`, and you have the credential sitting inside the compromised address. `C` is one leaf in a fixed-depth-14 eligibility Merkle tree whose root the contract holds, so membership is a cheap inclusion check. Every part of it folds into a single field element:

```
pub = Fr(Blake2b-256(domain_sep ‖ scriptHash ‖ snapshot_version ‖ root ‖ C ‖ entitlement ‖ D ‖ role))
```

That one number is the only public input. The master key, the derivation path, the Merkle siblings, and the entitlement all stay private witness; the verifier never sees them. The entitlement is encoded as a fixed 553-byte, up-to-eight-asset bundle, sorted and padded, so the contract repays the exact tokens that were held and the circuit and the contract never disagree about what they are looking at.

The proof is generated entirely on the client. The master seed never leaves the machine that holds it; only the 336-byte proof and the public destination ever go on-chain. The circuit is built from gadgets that were each audited on their own, the HMAC-SHA512 derivation chain, the Ed25519 scalar multiplication, the Blake2b core, because the point was never new cryptography. It was wiring proven parts together so that the word "correctly" actually holds, which is exactly where this class of system breaks.

On-chain, the verifier is the part with teeth. Cardano exposes the BLS12-381 pairing operations as Plutus built-ins under CIP-381, so a contract can run a Groth16 verifier with its own hands. The wrinkle is that the circuit uses lookup tables to make hashing cheap, and the moment the proving system sees lookups it staples an extra object onto the proof, a single gnark BSB22 Pedersen commitment, that a textbook verifier ignores. So our on-chain verifier ([`Recovery/Verify.hs`](proto/onchain/redemption/src/Recovery/Verify.hs)) reproduces the proving library's full procedure: reconstruct the commitment point, run a pairing check that the prover knows what it committed to, hash the commitment to a challenge with `expand_message_xmd` over SHA-256 byte-for-byte against gnark's own `fr.Hash`, fold it into the public-input term as `vk_x = K0 + pub·K1 + e_cmt·K2 + commitment`, and run the final pairing. One byte off in that challenge and nothing matches, so "byte-for-byte" is the literal spec.

Verifying the proof is necessary but not the finish line. The full claim path ([`RedemptionValidator.hs`](proto/onchain/redemption/src/RedemptionValidator.hs)) does more: it rebuilds `pub` from context it already trusts, the credential and entitlement in the custody datum, the root and version and script hash in its parameters, plus the destination and role from the redeemer, so a prover cannot supply their own public input. It checks the payout equals the committed entitlement to the token, checks the money goes to the bound destination `D` and nowhere else, and refuses to pay itself. Money leaves custody through this claim path or through governance, and through no other branch.

Two roles operate the system, and you can see both as working strawman web apps in [`product/`](product/). The **redeemer** is the victim: they hold the master seed, prove ownership in the browser without it ever leaving the device, generate a fresh recovery wallet, and submit the claim through a connected CIP-30 wallet. The **operator** is a three-of-five M-of-N governance multisig plus permissionless reference services. It publishes the eligibility snapshot, funds custody, and runs a public accounting dashboard. The trust model is honest about itself: the operator can move custody, so the protection for people who were already robbed once is not cryptographic non-custody but radical transparency. Every inflow, every vend, and every governance action is public, and the snapshot is independently reproducible.

## What we built and deployed

This is the part that matters, so I will be plain about it: this is not a paper. We deployed real Plutus V3 scripts to the Cardano preview testnet and moved real (testnet) funds with them, twice, with negative controls. Two milestones.

**E1, the node verifies the proof.** A minimal gate script ([`Gate.hs`](proto/onchain/redemption/src/Gate.hs)), parameterized by `(vk, pub)`, spendable only if the on-chain commitment-aware verifier returns true. We locked 5 tADA behind it and spent it with the real 336-byte proof in the redeemer; the node ran the verifier and released the funds. Then we flipped one byte of the proof and resubmitted, and the node rejected it at the exact step where the bad byte became an invalid curve point.

| # | Tx hash | Action |
|---|---------|--------|
| Lock | `168b4de3c9b63eae48722af2992db8881b7f0a1d5343fa90dc1ec5e03cfcb4ef` | Lock 5 tADA at the gate |
| Verify | `7f7f41e0db53892ce2c216732fad1ad78a5b795fa2d50fd297dd7518bcda82af` | Real proof verified on-chain, funds released |
| Tampered | `0279ff4c1e220a2b1ce314db77e32f956489c0acb306dba4ae4a83e7186a07c7` | One byte flipped, rejected by the node |

Gate script (`bb6a2410…`): `addr_test1wzak5fqsa8ztaatzrfrqcfcqnrlrpjmdhqajn394pvc2h9sdyqte3`. Evidence: [`test.md`](test.md).

**E2, the full recovery runs on-chain.** The gate only proves the node can check a proof. The full `RedemptionValidator` does the whole job, proof verification plus the entitlement check plus the destination binding plus no-self-pay. We locked 5 tADA in custody with an inline `CustodyDatum(C, entitlement)`, generated a clean wallet that had never held anything, re-proved the circuit with that wallet as the destination, and claimed. The contract verified the proof, matched the 5 tADA entitlement, confirmed the payout went to the bound destination, and paid out. Five tADA landed in a fresh UTxO put there by nothing but a proof of knowledge of a master secret.

| # | Tx hash | Action |
|---|---------|--------|
| Lock | `09664cd27de2d64f30db788ff9457b27b6ebd82dc9e7c4acb767a4c79ae9314e` | Lock 5 tADA in custody at the full validator |
| Claim | `ababcda39b11f37ca490fa80a02a09b69225a2d7dfa2bd170f90c8cb34856d16` | Full validator runs, 5 tADA recovered to the fresh wallet `D` |

Full validator (Plutus V3, 5960 bytes): `addr_test1wq3xw4rlsavkfkrwmn5rgkds6uethg6q3naf65jefcp4d5qm46s4w`. Destination `D`: `addr_test1qpyrmar0p6rh94dvv7vlx060j359mvrfmyey2ezw4zhdhev8l5948m6weh72g4h3df2zleuyqyp30e0mm0ky72t8zeqsm0yae5`. Negatives reject as they should: tampered proof, wrong value, wrong destination. Evidence: [`proto/onchain/redemption/E2-FULL-CLAIM.md`](proto/onchain/redemption/E2-FULL-CLAIM.md).

## On-chain record (Preview, independently verified)

These are not numbers I am asking you to take on faith. They were pulled live from the public Koios Preview API, with the chain tip at block 4,422,889 at query time. All four settled transactions sit in epoch 1342 on 2026-06-28. The tampered-proof transaction (`0279ff4c…`) is absent from the chain, exactly as it should be: a transaction the node rejects never settles and leaves no record.

| Tx | What it did | Block | Slot | Time (UTC) | Fee | Conf. |
|----|-------------|-------|------|------------|-----|-------|
| [`168b4de3…`](https://preview.cexplorer.io/tx/168b4de3c9b63eae48722af2992db8881b7f0a1d5343fa90dc1ec5e03cfcb4ef) | E1, lock 5 tADA at the gate | 4,422,463 | 115,962,606 | 03:50:06 | 1.0 tADA | ~426 |
| [`7f7f41e0…`](https://preview.cexplorer.io/tx/7f7f41e0db53892ce2c216732fad1ad78a5b795fa2d50fd297dd7518bcda82af) | E1, real proof verified, funds released | 4,422,476 | 115,962,987 | 03:56:27 | 1.5 tADA | ~413 |
| [`09664cd2…`](https://preview.cexplorer.io/tx/09664cd27de2d64f30db788ff9457b27b6ebd82dc9e7c4acb767a4c79ae9314e) | E2, lock 5 tADA in custody | 4,422,656 | 115,968,747 | 05:32:27 | 1.0 tADA | ~233 |
| [`ababcda3…`](https://preview.cexplorer.io/tx/ababcda39b11f37ca490fa80a02a09b69225a2d7dfa2bd170f90c8cb34856d16) | E2, full validator runs, 5 tADA recovered to `D` | 4,422,688 | 115,969,788 | 05:49:48 | 2.0 tADA | ~201 |

Koios confirms the script executions directly: the E1 verify (`7f7f41e0…`) consumed the gate UTxO and ran Plutus V3 script `bb6a2410e9c4bef5…`; the E2 claim (`ababcda3…`) consumed a custody UTxO and ran the full `RedemptionValidator` script `2267547f875964d8…`. Both succeeded and moved funds. The on-chain execution cost, measured by CEK evaluation against the submitted budgets, was 3,236,238,137 ExCPU for E1 and 3,914,957,868 ExCPU (39.1% of the 10,000,000,000 per-tx budget) for the full E2 recovery. What the chain proves, plainly: a live Cardano node ran a contract that verified a real 3.45-million-constraint zero-knowledge proof and released funds to a fresh wallet, and rejected the same proof with one byte changed.

Those four transactions used a throwaway `groth16.Setup`. The setup has since been re-run as an MPC ceremony, with its own Preview lock and claim against the ceremony-produced verifying key. That deployment, its transactions, and the trust caveats are in the [MPC trusted-setup ceremony](#mpc-trusted-setup-ceremony) section.

**D ≠ C payout invariant (REQ-D1-15), re-minted and re-verified on-chain.** The circuit now enforces that a recovery payout can never return funds to the compromised claimed credential: the destination `D`'s payment credential must not equal the derived `C`, a hard in-circuit constraint (the proof is uncreatable otherwise) mirrored as a fail-closed check in the validator. Adding the gadget changed the R1CS from 3,450,403 to **3,450,487 constraints**, which invalidated the old keys, so the proving/verifying keys were re-minted and the `RedemptionValidator` redeployed to Preview at `addr_test1wz75hdz…q64qrqzgfz9r`. A full end-to-end claim against the re-minted keys — exercising the ticket-aware spent-state gate (custody + ticket locked, both spent, ticket burned) — settled on-chain: the node ran the complete validator (Groth16 verify + entitlement + destination binding + no-self-pay + `D ≠ C` + one-custody-input + ticket-burn) and released 5 tADA to the bound `D` in claim tx [`5f490bc5…`](https://preview.cexplorer.io/tx/5f490bc508c605611cfed7da4a3cd69c4a7234c522bb57ccbdbd3d14d4127cbc) (measured ~5.94e9 ExCPU / 10.95e6 ExMem, well inside the per-tx budget). The re-minted keys remain single-operator dev keys pending the production ceremony.

## Real numbers

Everything below is measured from the actual implementation, not estimated.

| Quantity | Value |
|----------|-------|
| Circuit constraints | 3,450,403 (K=22; 1 public input, 1,239 secret witnesses) |
| Setup / prove | 12m18s throwaway `groth16.Setup`, 43s prove, peak 7.3 GB RAM (local WSL, 24 GB box); the MPC ceremony replaces this setup and its timings are in the [MPC trusted-setup ceremony](#mpc-trusted-setup-ceremony) section |
| Verifying key (on-chain) | 672 B |
| Proof (on-chain) | 336 B (A‖B‖C 192 ‖ commitment 96 ‖ PoK 48) |
| Public input | 32 B (LE Blake2b-256 digest, reduced mod r on-chain) |
| Preview per-tx budget | 10,000,000,000 ExCPU / 16,500,000 ExMem |
| E1 verify cost (CEK) | 3,236,238,137 ExCPU (32.4%) / 35,242 ExMem (0.21%) |
| E2 full-claim cost | 3,914,957,868 ExCPU (39.1%) / 2,826,629 ExMem (17.1%) |
| Compromised credentials | ~8,823 |

The whole recovery fits comfortably inside a single Preview transaction, with room to spare. That number, a full zero-knowledge recovery at under 40% of one transaction's compute budget, is the one I did not expect to be able to write down.

## Test snapshot at scale

Testing the contract against one wallet proves the path; testing it against a realistic eligibility set proves the machine. The repository ships a committed, deterministic **16,384-wallet snapshot** — the full depth-14 Merkle capacity — as the canonical test fixture, at [`proto/vending/snapshot/testdata/`](proto/vending/snapshot/testdata/) (documented in [`proto/vending/snapshot/README.md`](proto/vending/snapshot/README.md)). Holdings are synthetic but realistic: a long-tail ADA distribution from a 2-ADA min-UTxO floor up to ~20M-ADA whales (median ≈ 357 ADA), with ~20% of wallets carrying native tokens so the multi-asset 553-byte entitlement is exercised at scale. The whole fixture is byte-for-byte reproducible — every wallet's holdings derive deterministically from its credential `C` (integer-only, no floating-point), so a regenerated snapshot reproduces the committed Merkle root (`348e02ee…`) and file hash exactly. A fast Go test recomputes the root from the committed credentials with no toolchain, and a `perf`-tagged test regenerates the entire pipeline from seeds (through the `e2-refgen` oracle) and checks it bit-for-bit. The snapshot itself carries no key material; a small `golden-claims.json` holds a few Preview-only, zero-value test wallets — with keys and inclusion paths — for driving end-to-end prover and validator tests against the real root.

## Property-based testing

Beyond the fixed-vector and differential tests, a property-based layer asserts the load-bearing invariants over randomized inputs. In Go (via `pgregory.net/rapid`, plus native fuzzing): Merkle inclusion-proof soundness and tamper-binding over random trees, the public-input aggregation's field-range and binding, the synthetic-holdings min-UTxO floor and determinism, and the wire-proof parser's never-panic robustness. In Haskell (`tasty-quickcheck`): the nullifier's spec formula and snapshot-version independence, and the `D ≠ C` rejection over random credentials — the validator-side mirror of the in-circuit constraint. Each property runs hundreds of cases per invocation and shrinks any counterexample to a minimal repro.

## The product and the writeup

- [`product/redeemer.html`](product/redeemer.html), the victim's recovery flow (eligibility check, CIP-30 connect, local proving, claim), as a self-contained strawman web app.
- [`product/operator.html`](product/operator.html), the operator dashboard: the solvency gauge, the M-of-N governance console, the snapshot builder, and the public accounting.
- [`product/zk-recovery-blog.md`](product/zk-recovery-blog.md) / [`.html`](product/zk-recovery-blog.html), the readable technical writeup of how the whole thing works.

## What's proven, and what's assumed

The Lean layer ([`lean/`](lean/)) proves the contract's decision logic is sound with the Groth16 verifier left opaque, which is the right boundary: the cryptographic soundness of the verifier lives in the gnark/BLS layer, not in Lean. Every proved theorem there depends only on `propext`, `Classical.choice`, and `Quot.sound`, no `sorryAx`, no `native_decide`. There is exactly one open seam, `circuit_models_relation` ([`lean/Ckd/OBLIGATIONS.md`](lean/Ckd/OBLIGATIONS.md)), the claim that the R1CS constraints model the relation over the canonical witness; it is deferred-blocked because discharging it means proving SHA-512 and Ed25519 R1CS soundness, and it is named honestly rather than hidden.

The honest gaps are not the cryptography. The trusted setup is the one everyone asks about, and it is not existential: the funds already sit under a three-of-five governance set that can move them, so a multi-party setup ceremony, sound as long as one honest participant discards their toxic waste, would ask for strictly less trust than the system already assumes. The ceremony framework is now built, and a single-operator ceremony has been run end-to-end on Preview against the deployed circuit, documented in the [MPC trusted-setup ceremony](#mpc-trusted-setup-ceremony) section. The deployed Preview keys are single-operator, so the 1-of-N guarantee does not yet apply to them; the multi-party production ceremony with an external beacon is still ahead. The design is in [`docs/trusted-setup-ceremony.md`](docs/trusted-setup-ceremony.md). The gaps that actually bite live upstream: the sweep race (the at-risk funds have to reach custody before the attacker drains them, and the eligibility snapshot has to be taken before the draining starts), and the governance question of who builds the eligibility list and is trusted to build it honestly. Those are operations and governance problems, not proving-system problems, and they are where the next attention should go.

## MPC trusted-setup ceremony

The ceremony produces Groth16 proving and verifying keys for the deployed `drv.Recovery` circuit over BLS12-381. It is split into a circuit-independent Powers of Tau (Phase 1) and a circuit-specific, commitment-aware Phase 2. The on-chain artifact is a 672-byte committed verifying key (`vk_c.hex`) baked into the `RedemptionValidator`. The `proto/ceremony` packages provide a verifiable multi-party framework that enforces the BGM17 soundness properties. The keys on Preview today came from a single operator, which this section states plainly and examines in [Trust posture](#trust-posture-testnet-today-what-production-needs).

### Why Groth16 needs a trusted setup, and what MPC buys

Groth16 gives constant-size proofs (336 bytes for this circuit) and constant-time verification regardless of circuit depth. Both properties are what make running the verifier inside a Plutus V3 script practical: the ExCPU cost is bounded and fixed. The cost is a structured reference string (SRS) whose generation involves secret random scalars. Anyone who retains those scalars can forge proofs for false statements. There is no way to eliminate the toxic waste; there is only a way to distribute it.

The BGM17 protocol (ePrint 2017/1050), implemented in gnark's `bls12-381/mpcsetup` backend, distributes the toxic waste across N participants. Each participant contributes fresh randomness on top of the current state and publishes a proof of knowledge of what they contributed. If at least one participant honestly discards their secret, the resulting SRS is as sound as one generated by an honest third party, under the discrete-logarithm assumption on BLS12-381. This is the 1-of-N guarantee: the adversary must corrupt every participant, not just one.

That guarantee is a property of the framework, not of the deployed keys. The verifying key on Preview came from a single-operator run with N=1. There is no 1-of-N protection on the currently deployed key.

Two verifying key formats are in use and must not be confused. The 432-byte vanilla VK carries `alpha|beta|gamma|delta|IC0|IC1`. The 672-byte committed VK appends three extra points (`K2`, `CK.G`, `CK.GSigmaNeg`) that the on-chain `groth16VerifyCommitted` needs for the BSB22 Pedersen commitment check. A validator built against the vanilla form ignores the sigma machinery and is susceptible to a sigma-degenerate forgery. The committed form is the only one deployed on-chain.

### The two phases

Phase 1 (Powers of Tau) is circuit-independent. It produces the `SrsCommons`: powers of a secret scalar tau at the curve generators, plus alpha and beta correction factors. Any circuit whose constraint count fits within the domain can reuse the same Phase-1 output. The framework design targets domain 2²³ as headroom over the deployed 2²² circuit. Each participant calls `Contribute`, which applies fresh randomness to every point and attaches a proof of knowledge. The phase closes when the coordinator calls `SealPhase1` with a public beacon.

Phase 2 is bound to one specific circuit's R1CS. The `drv.Recovery` circuit carries one gnark BSB22 Pedersen commitment, so Phase 2 has two secrets: delta and sigma. Gamma is fixed to 1 by gnark's design; this is correct, not a defect, and checking whether gamma equals 1 is not a meaningful security test. The secrets to protect are delta (which controls the Z and PKK polynomial evaluations) and sigma (which controls the Pedersen commitment key). A verifier that checks only the delta proof of knowledge, treating the circuit as vanilla Groth16, accepts a sigma-degenerate setup that allows proof forgery on the commitment branch.

| Dimension | Phase 1 (Powers of Tau) | Phase 2 (circuit-specific) |
|---|---|---|
| Circuit dependency | none; any circuit within the domain | bound to the `drv.Recovery` R1CS |
| Secrets generated | tau, alpha, beta | delta, sigma (gamma is fixed to 1 by gnark design) |
| Proof-of-knowledge scope | tau/alpha/beta ratio checks | delta PoK and sigma PoK |
| Seal output | `SrsCommons` | proving key, verifying key |
| If secrets are kept | any SRS for this domain can be rebuilt | any proof for this circuit can be forged |

### Architecture and end-to-end pipeline

The pipeline runs in six stages, from the gnark fork through Phase 1, Phase 2, the prover, deploy, and finally lock and claim on Preview.

| Stage | Entry points | Source |
|---|---|---|
| Phase 1: Powers of Tau | `InitPhase1`, `p1.Contribute()`, `SealPhase1` | `core/bgm17.go` |
| Phase 2: circuit-specific | `InitPhase2`, `p2.Contribute()`, `SealPhase2` | `core/bgm17.go` |
| Prove | `realprove` (load pk, skip `groth16.Setup`) | `proto/vending/prover/cmd/realprove` |
| Deploy | `redemption-deploy` (Haskell) | `proto/onchain/redemption/app-deploy/Main.hs` |
| Lock | `claim_lock.sh` | `proto/onchain/redemption/claim_lock.sh` |
| Claim | `claim_spend.sh` | `proto/onchain/redemption/claim_spend.sh` |

`InitPhase1(power)` creates the genesis `Phase1` object at domain size `1<<power`. After `SealPhase1` returns, its argument is invalid: a verify-before-seal must serialize with `Phase1Payload` and deserialize with `ReadPhase1` to get a fresh copy, not copy the struct. `InitPhase2(r, &commons)` compiles the `drv.Recovery` R1CS into the Phase 2 seed and returns the `Phase2Evaluations` needed by the seal. `realprove` detects `recovery.{pk,vk}` in `proto/vending/prover/work/keys/` and skips `groth16.Setup` entirely. Deploy uses `redemption-deploy`, not `proto/vending/scripts/deploy.sh`, which is a vanilla 432-byte dry-run printer and not the canonical path.

**End-to-end data flow**

```
  gnark fork
  (fix/1428-phase2-init-memory at C:\proof-deps\gnark)
       |
       v
  PHASE 1
  InitPhase1(22) -> p1.Contribute() -> SealPhase1(beacon)
       |
       v
  SrsCommons (in-process; not persisted to disk in the realceremony path)
       |
       v
  PHASE 2
  InitPhase2(r, &commons) -> p2.Contribute() -> SealPhase2(beacon)
       |
       +----------------------------------+
       |                                  |
       v                                  v
  recovery.pk (2.42 GB, gitignored)  recovery.vk (784 B, gitignored)
       |                                  |
       +----------------------------------+
       |
       v
  realprove
  (loads pk via UnsafeReadFrom; skips groth16.Setup;
   vk loaded via checked ReadFrom)
       |
       v
  testdata-recovery/
    vk_c.hex    (672 B, committed VK, on-chain artifact)
    proof_c.hex (336 B, on-chain proof)
    dom.hex     (722 B)
    pub.hex     ( 32 B)
       |
       +--- vk_c.hex + dom.hex
       |
       v
  redemption-deploy (Haskell, app-deploy/Main.hs)
       |
       v
  redemption.plutus (Plutus V3, 5960 B)
       |
       v
  cardano-cli address build
       |
       v
  Script address (MPC VK, Preview):
  addr_test1wrgkz5sdkqjy8qzyqu96dl5clx0ljlfj46ey5g8f0394dgqv86qr5
       |
       +-- lock tx af001550... -- claim tx 92738a5d...
       |
       v
  Preview node:
  groth16VerifyCommitted(MPC VK) + entitlement + dest bind -> ACCEPT
  5 tADA released to addr_test1qpyrmar0p6rh94...
```

**Component map**

proto/ceremony/* uses the PATCHED gnark fork.
  proto/vending uses STOCK gnark.

go.work at C:\proof-deps\realceremony unifies them:
    replace github.com/consensys/gnark
         => /mnt/c/proof-deps/gnark
  (branch: fix/1428-phase2-init-memory)
```

The gnark fork at `C:\proof-deps\gnark` (WSL: `/mnt/c/proof-deps/gnark`) carries two patches on branch `fix/1428-phase2-init-memory`. The first (#1428) rewrites `Phase2.Initialize` as four sequential single-array passes, reducing peak RSS by approximately 24% at power 22 while producing bit-for-bit identical output, gated by `TestPhase2InitGolden` (digest `f822fa15...`). The second parallelizes `SrsCommons.update` by precomputing the power vector serially and running the EC scalar-multiplication pass across all cores, gated by `TestPhase1UpdateGolden`. `proto/vending` uses stock gnark and is unaffected. The `go.work` in the `realceremony` scratch module unifies both for the ceremony binary. See [Performance](#performance) for the measured numbers.

### Soundness properties

| Property | Mechanism | Source |
|---|---|---|
| Subgroup and canonical-encoding checks on every contribution | `ReadFrom` (not `UnsafeReadFrom`) on the verify path | `core/bgm17.go`: `ReadPhase1`, `ReadPhase2` |
| tau/alpha/beta proof of knowledge (Phase 1) | `VerifyPhase1Step` calls gnark inner `Verify` | `core/bgm17.go` |
| delta and sigma proof of knowledge (Phase 2) | `VerifyPhase2Step` checks both | `core/bgm17.go` |
| sigma-degenerate rejection | commitment-aware verify rejects; a delta-only verify accepts the same transcript | `spec/sigma_degenerate_test.go` |
| Genesis recomputed, never trusted from bytes | `VerifyAll` calls `InitPhase1` and `InitPhase2` from a fresh R1CS compile; never reads genesis from the transcript | `core/bgm17.go` |
| gnark-drift canary and R1CS hash-pin | deterministic VK regenerated from the current gnark build and byte-diffed against `spec/testdata/golden_vk_c.bin` | `spec/drift_canary_test.go`, `core/r1cs.go` |
| Committed-VK structural invariants | `AssertCommitmentInvariants` checks one commitment key, three IC points, `PublicAndCommitmentCommitted == [[1]]` | `core/bgm17.go` |
| Transport integrity | `ValidateChain` checks BLAKE2b content addresses and Prev links for every step file | `core/chain.go` |
| Bounded-allocation decode | `ReadTranscript` caps declared lengths against `maxPayload` before allocating and rejects trailing bytes | `core/transcript.go` |

`ValidateChain` (BLAKE2b hash chain) is transport integrity only. `VerifyAll` is the cryptographic check. Both must pass; one does not substitute for the other.

`UnsafeReadFrom` is used only when `realprove` loads `recovery.pk` for proving from a locally produced file. The verifying key is always loaded with the checked reader. This call is not on any verify path.

`AssertCommitmentInvariants` checks the MiniCircuit's `[[1]]` shape. It must not be called on `drv.Recovery` VK output. The real circuit has `PublicAndCommitmentCommitted == [[]]`, so calling it on that VK would false-positive on a correct key. The real circuit's commitment binding is implicit in the Phase 2 sigma check. `VerifyAll` calls `AssertCommitmentInvariants` internally; it is correct for the MiniCircuit and must not be called independently on the production VK. VibeSec marked this PARTIALLY-CONFIRMED.

### Interface: packages, CLIs, file formats

#### Package reference

| Package | Role |
|---|---|
| `proto/ceremony/core` | I/O-free protocol library: BGM17 wrapper, TLV transcript, Prev-linked chain, committed-VK serializer, R1CS hash-pin, MiniCircuit definition |
| `proto/ceremony/coord` | Coordinator seam: `Client` interface, `LocalClient` (filesystem implementation), `HealthCheck` |
| `proto/ceremony/cmd/contributor` | Contributor CLI: `contribute` subcommand, airgap contribution with phase-override flag |
| `proto/ceremony/cmd/verify-go` | Verifier CLI for **MiniCircuit conformance ceremonies**: independent re-verification over a full transcript directory; emits the 672-byte committed VK (see the CLI scope note) |
| `proto/ceremony/spec` | Conformance vectors, frozen golden VK, sigma-degenerate anti-monoculture test, gnark-drift canary |

Key exported signatures from `core`:

```go
// Phase 1
func InitPhase1(power uint8) (*mpcsetup.Phase1, error)
func Phase1Payload(p *mpcsetup.Phase1) ([]byte, error)
func ReadPhase1(b []byte) (*mpcsetup.Phase1, error)          // checked ReadFrom only
func VerifyPhase1Step(prev, next *mpcsetup.Phase1) error
func SealPhase1(p *mpcsetup.Phase1, beacon []byte) mpcsetup.SrsCommons  // invalidates p

// Phase 2
func InitPhase2(r *cs.R1CS, commons *mpcsetup.SrsCommons) (*mpcsetup.Phase2, *mpcsetup.Phase2Evaluations)
func Phase2Payload(p *mpcsetup.Phase2) ([]byte, error)
func ReadPhase2(b []byte) (*mpcsetup.Phase2, error)          // checked ReadFrom only
func VerifyPhase2Step(prev, next *mpcsetup.Phase2) error
func SealPhase2(p *mpcsetup.Phase2, commons *mpcsetup.SrsCommons,
    evals *mpcsetup.Phase2Evaluations, beacon []byte) (groth16.ProvingKey, groth16.VerifyingKey)

// Full ceremony verification
func VerifyAll(cfg CeremonyConfig, beacon []byte, p1Steps, p2Steps [][]byte) (groth16.VerifyingKey, error)

// Chain
func AppendStep(dir string, phase Phase, payload []byte) (Transcript, error)
func LoadChain(dir string) (CeremonyConfig, []byte, [][]byte, [][]byte, error)
func ValidateChain(dir string) error

// VK serialization
func SerializeVKCommitment(vk groth16.VerifyingKey) ([]byte, [][]int, error)
func AssertCommitmentInvariants(vk groth16.VerifyingKey) error

// R1CS utilities
func DomainSize(r *cs.R1CS) uint64
func HashR1CS(r *cs.R1CS) (Hash, error)
func CompileMiniCircuit() (*cs.R1CS, error)
```

`coord.Client` interface:

```go
type Client interface {
    Register(identity string) (token string, err error)
    CurrentTranscript() (chainDir string, err error)
    SubmitContribution(stepFile string) (receipt string, err error)
    PublishAttestation(att Attestation) error
}
```

`coord.HealthCheck()` draws two 32-byte values from `crypto/rand` before a contribution and fails if either draw fails or both values are identical (stuck CSPRNG). The contributor CLI calls it automatically; callers using the package API must call it themselves.

#### CLI reference

**contributor**

```
contributor contribute --in <transcript-dir> --out <step-file> [--phase 0|1|2]
```

`--in` is the source transcript directory containing `manifest.json`. `--out` is the output TLV step file. `--phase 0` (default) auto-detects the active phase from the manifest head: Phase 2 if any Phase-2 step exists, Phase 1 otherwise. `--phase 1` or `--phase 2` overrides the auto-detection; the Prev hash and index always come from the manifest head regardless. The CLI calls `HealthCheck` before drawing entropy and writes the step file. It does not submit to the coordinator: that step goes through `LocalClient.SubmitContribution`. On success:

```
wrote <step-file>
```

**verify-go**

```
verify-go --transcript <transcript-dir>
```

`verify-go` re-verifies a **MiniCircuit conformance ceremony**. `VerifyAll` recompiles the MiniCircuit (`CompileMiniCircuit`) as genesis, so step (4) `AssertCommitmentInvariants` is valid for the MiniCircuit's `[[1]]` shape. The production `drv.Recovery` ceremony is run with the `realceremony` binary, which does not call `VerifyAll`; the real circuit has `PublicAndCommitmentCommitted == [[]]` and its binding is implicit (see [Soundness properties](#soundness-properties)). Do not run `verify-go` against a `drv.Recovery` transcript.

Runs five steps in order: (1) `ValidateChain` for transport integrity, (2) `LoadChain` to read the manifest and step payloads, (3) `VerifyAll` to recompute genesis and verify every step cryptographically, (4) `AssertCommitmentInvariants` on the output VK, (5) `SerializeVKCommitment` to emit the 672-byte hex. On success:

```
OK: ceremony verified (<n> phase-1, <m> phase-2 contributions)
VK (672-byte committed): <hex>
```

#### File formats

**TLV step file.** Four-byte magic `PZKT`, version `0x0001` (uint16 big-endian), phase (uint8), index (uint32 big-endian), Prev hash (32 bytes), payload as an 8-byte big-endian uint64 length prefix followed by the payload bytes, attestation in the same length-prefixed form. The content-address hash covers `DST || TLV(Version) || TLV(Phase) || TLV(Index) || TLV(Prev) || TLV(Payload)` via BLAKE2b-256 with domain-separation tag `proof-zk/ceremony/transcript/v1`. The attestation field is excluded from the hash. `ReadTranscript` rejects any version other than 1, caps declared lengths against `maxPayload` before allocating, and rejects trailing bytes after the structure.

**manifest.json.** JSON with keys `config` (a `CeremonyConfig` object: curve string, power uint8, phase, gnark version), `beacon_b64` (base64), and `steps` (ordered array of objects with `file`, `hash_b64`, `phase`, `index`). The manifest is the recoverable source of truth; both `LoadChain` and `ValidateChain` start from it.

**Committed VK (672 bytes).** Byte layout (BLS12-381, ZCash/IETF compressed-point encoding; G1 = 48 bytes, G2 = 96 bytes):

| Offset | Length | Field | Description |
|---|---|---|---|
| 0 | 48 | alpha | [alpha]_1 compressed G1 |
| 48 | 96 | beta | [beta]_2 compressed G2 |
| 144 | 96 | gamma | [gamma]_2 compressed G2 (fixed to G2 generator by gnark) |
| 240 | 96 | delta | [delta]_2 compressed G2 |
| 336 | 48 | IC0 | K[0] G1 (constant IC term) |
| 384 | 48 | IC1 | K[1] G1 (public input scalar) |
| 432 | 48 | K2 | K[2] G1 (commitment wire IC point) |
| 480 | 96 | CK.G | CommitmentKeys[0].G, G2 (Pedersen base) |
| 576 | 96 | CK.GSigmaNeg | CommitmentKeys[0].GSigmaNeg, G2 (negated sigma key) |

`VKCommitLen = 432 + 48 + 96 + 96 = 672`. The 432-byte vanilla prefix matches the layout `groth16VerifyCommitted` reads for the standard Groth16 check; the three extra points follow it for the commitment branch.

Constants from `core/vkcommit.go`: `VKLen = 432`, `K2Off = 432`, `CKGOff = 480`, `CKGSNOff = 576`, `VKCommitLen = 672`.

#### Known interface gaps

Four gaps are documented and must not be papered over:

1. There is no `submit` or `runFlow` CLI subcommand. Chain submission goes through `LocalClient.SubmitContribution` in the library. A network coordinator path is a future addition.
2. `AppendStep` is not crash-atomic. It writes the TLV step file and then rewrites `manifest.json`. A crash between the two leaves the manifest inconsistent with the directory.
3. `AssertCommitmentInvariants` must not be called on `drv.Recovery` VK output. The real circuit has `PublicAndCommitmentCommitted == [[]]`, not the MiniCircuit's `[[1]]`, so the assertion false-positives on a correct production key.
4. `SealPhase1` mutates and invalidates its `*Phase1` argument. A verify-before-seal flow must produce a deep copy via `Phase1Payload` plus `ReadPhase1`, not a struct copy.

#### Quick start

Build and run a contribution against a local transcript directory (WSL, Go 1.26):

```bash
# Build both CLIs
cd /mnt/c/proof/.claude/worktrees/mpc-ceremony/proto/ceremony
go build ./cmd/contributor ./cmd/verify-go

# Contribute (auto-detects phase from the manifest head)
./contributor contribute --in /path/to/transcript-dir --out my-step.tlv

# Submit via LocalClient (no submit CLI yet; call from Go directly)

# Re-verify the full chain
./verify-go --transcript /path/to/transcript-dir
```

For the real circuit (requires the gnark fork and the `realceremony` scratch module):

```bash
# Build and run the ceremony for drv.Recovery (2^22 domain, ~42 min)
cd /mnt/c/proof-deps/realceremony
go build . && ./realceremony
# Keys written to:
# .../proto/vending/prover/work/keys/recovery.pk  (2.42 GB, gitignored)
# .../proto/vending/prover/work/keys/recovery.vk  (784 B, gitignored)
```

### Performance

| Metric | Value |
|---|---|
| Full ceremony wall-clock | 2528 s (~42 min) |
| Phase-1 contribute: serial / parallel | 1251.6 s / 137.2 s (~9.1x) |
| Phase-1 seal: serial / parallel | 1332 s / 134 s (~10x) |
| Phase-1 overall speedup (2^22 real run) | ~9.5x |
| Isolated `update` benchmark (power 18) | 129.2 s / 9.17 s (~14x); design projection 18-22x on an idle box |
| Phase-2 duration | ~37.5 min |
| Key write (`recovery.pk`, 2.42 GB) | ~6 s (buffered ~224 MB/s; was ~0.13 MB/s unbuffered, ~1700x) |
| Phase-2 peak RSS | ~13 GB |
| #1428 peak heap reduction at power 18 | 142 MiB (~24%); projected ~2.4 GiB at 2^23 |
| `recovery.pk` | 2,422,768,145 bytes (gitignored) |
| `recovery.vk` | 784 bytes (gitignored) |
| `vk_c.hex` (on-chain committed VK) | 672 bytes |
| Vanilla VK (not deployed) | 432 bytes |
| `proof_c.hex` (on-chain proof) | 336 bytes |
| `pub.hex` | 32 bytes |

Phase rows are approximate; the 2528 s total also covers circuit compilation (about 8 s) and the buffered key write (about 6 s).

Phase 1 parallelizes because `SrsCommons.update` applies independent scalar multiplications to each SRS point. The only sequential dependency is the power recurrence `tau^i = tau^(i-1) * tauUpdate`, which the patch resolves by precomputing the power vector in a serial field-multiplication pass (cheap, approximately 1-2 s at 2^22) and then running the EC scalar-multiplication pass across all cores with no shared mutable state. `utils.Parallelize` (already used elsewhere in the gnark fork package) distributes the index range across workers; each worker uses its own scratch variables.

The buffered pk I/O improvement replaced point-by-point writes over a 9P filesystem mount with a `bufio.Writer`. The verifying key path was not changed; `recovery.vk` is small enough that the improvement is immaterial.

The #1428 memory patch splits the single four-array Lagrange allocation in `Phase2.Initialize` into four sequential single-array passes. At the 2^23 framework headroom domain the unpatched code holds approximately 4.0 GiB of Lagrange arrays simultaneously; the patched code holds at most 1.61 GiB. Full measurements at 2^23 are an open item in `proto/ceremony/PHASE0-REPORT.md`.

### Running a ceremony

#### Prerequisites

- WSL with Go 1.26; `PATH` includes `/usr/local/go/bin` and `$HOME/go/bin`.
- The gnark fork at `C:\proof-deps\gnark` (WSL: `/mnt/c/proof-deps/gnark`), branch `fix/1428-phase2-init-memory`. Both `TestPhase2InitGolden` (digest `f822fa15...`) and `TestPhase1UpdateGolden` must pass, and the full mpcsetup `TestAll` must be green under `-race`.
- The `realceremony` scratch module at `C:\proof-deps\realceremony` with the `go.work` and `main.go` from `docs/superpowers/CANONICAL-SETUP-HANDOFF.md` section 1.1. This module lives outside the repo because it unifies `proto/ceremony` (patched gnark fork) with `proto/vending` and the circuit modules (stock gnark). Placing it under `proto/ceremony` would break that module's build and tests.
- `cardano-cli` and `cabal` in the WSL PATH for the deploy and redeem steps.
- Koios Preview API access for lock and claim submission.

Two environment issues to resolve before running:

The claim scripts (`claim_lock.sh`, `claim_spend.sh`, `run_realclaim.sh`, `claim_env.sh`) hardcode `export PROOF=/mnt/c/proof`. Before using them from a worktree, set `PROOF` to the worktree path or edit `claim_env.sh` locally. Do not commit that edit.

The worktree's `.git` is a Windows-format path. WSL git fails inside it. Run all Go builds and ceremony steps via WSL. Run `git` commits via Windows: `git -C C:\proof\.claude\worktrees\mpc-ceremony <command>`.

#### Runbook

**Step 1: run the ceremony.**

```bash
wsl -e bash -lc '
  export PATH=$HOME/.local/bin:/usr/local/go/bin:$HOME/go/bin:$PATH
  cd /mnt/c/proof-deps/realceremony
  go build . && ./realceremony
'
```

Keys land at `proto/vending/prover/work/keys/recovery.{pk,vk}` (gitignored). The keys are not reproducible; re-running produces a fresh, equally valid setup. To check whether the keys already exist: `ls -la <worktree>/proto/vending/prover/work/keys/`.

**Step 2: prove** (loads ceremony keys, regenerates all on-chain fixtures).

```bash
wsl -e bash -lc '
  export PATH=$HOME/.local/bin:$HOME/.ghcup/bin:$HOME/.cabal/bin:/usr/local/go/bin:$HOME/go/bin:$PATH
  cd /mnt/c/proof/.claude/worktrees/mpc-ceremony/proto/vending
  go run ./prover/cmd/realprove
'
```

Writes to `proto/onchain/redemption/testdata-recovery/`: `vk_c.hex` (672 B), `proof_c.hex` (336 B), `dom.hex` (722 B), `pub.hex` (32 B). Compile takes approximately 10 s, prove approximately 43 s.

**Step 3: deploy** (bakes the committed VK into the validator, derives the script address).

```bash
cd /mnt/c/proof/.claude/worktrees/mpc-ceremony/proto/onchain/redemption
export PROOF=/mnt/c/proof/.claude/worktrees/mpc-ceremony
bash claim_serialize.sh
```

`claim_serialize.sh` calls `redemption-deploy testdata-recovery/vk_c.hex testdata-recovery/dom.hex redemption.plutus` and then `cardano-cli address build`. The result is `redemption.plutus` and its script address. Also emits `datum.json` and `redeemer.json`.

**Step 4: lock custody funds.**

```bash
bash claim_lock.sh
```

**Step 5: off-chain CEK dry-run** (recommended gate before submitting the live claim).

```bash
bash run_realclaim.sh
```

This calls `redemption-eval real-claim` and must print `ACCEPT` with ExBudget within 10,000,000,000 ExCPU and 16,500,000 ExMem.

**Step 6: claim.**

```bash
bash claim_spend.sh
```

Record the lock and claim transaction IDs as the canonical evidence. The pattern for recording them is `proto/onchain/redemption/CANONICAL-MPC-CLAIM.md`.

### Trust posture: testnet today, what production needs

The verifying key in the deployed Preview validator came from a single-operator setup. That is the operative trust boundary. The `realceremony` binary calls `InitPhase1`, `Contribute`, `SealPhase1`, `InitPhase2`, `Contribute`, `SealPhase2` directly and bypasses the `coord`/`contributor` framework and the TLV transcript chain entirely. The operator transiently held tau, alpha, beta, delta, and sigma. For a Preview testnet deployment carrying no real value, this is an accepted scope decision. It is not acceptable for any value-bearing deployment.

| Dimension | Deployed (Preview testnet) | Required for production |
|---|---|---|
| Participants | 1 operator | at least 3 independent contributors |
| Path | `realceremony` calls Init/Contribute/Seal directly; `coord` and transcript bypassed | `coord` + `contributor`, with `VerifyAll` over the full TLV chain |
| Toxic waste | operator transiently held tau, alpha, beta, delta, sigma | no participant holds all secrets; soundness holds if one is honest |
| Beacon | fixed ASCII string; no external entropy | public randomness (drand and Cardano epoch nonce), committed before contributions open |
| Transcript | none persisted | per-contribution TLV chain, published for independent verification |
| Plutus byte-identical guard | absent in this branch | present and pinned to the deployed artifact before merge |
| gnark fork | local-path replace; no commit-SHA pin | published fork pinned to a commit SHA |
| Network value | none (tADA) | real funds; all rows above are blocking |

Findings from the VibeSec gate (`docs/superpowers/2026-06-30-vibesec-session-gate.md`), with dispositions:

| # | Severity | Finding | Disposition |
|---|---|---|---|
| F1 | P1 | Single-operator setup; operator holds toxic waste; 1-of-N guarantee does not apply to the deployed key | Accepted for testnet; multi-party path required before mainnet |
| F5 | P1 | No in-branch byte-identical guard for `redemption.plutus` | Artifact independently verified (file sha256 `4942b869...`, cborHex sha256 `1b4fb0ce...`); guard must be added before merging to any guard-carrying branch |
| F2 | P2 | Fixed-text beacon; no external entropy | Scheduled; subsumed by F1; drand plus Cardano epoch nonce required for production |
| F4 | P3 | gnark fork pinned by local-path replace only; no commit-SHA | Scheduled backlog |
| F6 | P3 | Prover provenance manifest absent | Scheduled; pre-existing |

The parallelized `SrsCommons.update` and the buffered pk I/O drew no finding: the byte-identical golden gate passed, `-race` was clean, and the verifying key still uses the checked reader.

The sequence rule is unconditional: ceremony before VK, VK before script address, script address before funds. Locking funds at a script address before the ceremony completes, or deploying with any VK other than the post-ceremony output, voids the on-chain guarantees.

### Canonical Preview evidence

The MPC ceremony keys are the canonical setup for the `RedemptionValidator` on the address below. This address is derived from the ceremony-produced 672-byte committed VK (`vk_c.hex`) and is distinct from the E1 and E2 addresses described in [What we built and deployed](#what-we-built-and-deployed), which used a throwaway `groth16.Setup`.

| Item | Value |
|---|---|
| Script address (MPC VK, Preview) | [`addr_test1wrgkz5sdkqjy8qzyqu96dl5clx0ljlfj46ey5g8f0394dgqv86qr5`](https://preview.cexplorer.io/address/addr_test1wrgkz5sdkqjy8qzyqu96dl5clx0ljlfj46ey5g8f0394dgqv86qr5) |
| Lock tx | [`af00155008b74408c34f81722f3f7cbc935a8c0474d93f2ad2de89e362f93e2e`](https://preview.cexplorer.io/tx/af00155008b74408c34f81722f3f7cbc935a8c0474d93f2ad2de89e362f93e2e) |
| Claim tx | [`92738a5d5b7603f056c822bd15b309c29c967dc91ef3325137d236966910f896`](https://preview.cexplorer.io/tx/92738a5d5b7603f056c822bd15b309c29c967dc91ef3325137d236966910f896) |

The live Preview node ran the full `RedemptionValidator` against the ceremony VK and released 5 tADA to `addr_test1qpyrmar0p6rh94dvv7vlx060j359mvrfmyey2ezw4zhdhev8l5948m6weh72g4h3df2zleuyqyp30e0mm0ky72t8zeqsm0yae5`. The claim declared on-chain ex-units of 6,000,000,000 ExCPU and 4,000,000 ExMem, with headroom over the off-chain CEK measurement of 3,914,957,868 ExCPU and 2,826,629 ExMem (within the Preview per-tx budget of 10,000,000,000 ExCPU and 16,500,000 ExMem). That CEK measurement is identical to the E2 throwaway-setup claim in [Real numbers](#real-numbers): the Groth16 verifier cost depends on the circuit, not on the verifying key's contents. Full evidence is in [`proto/onchain/redemption/CANONICAL-MPC-CLAIM.md`](proto/onchain/redemption/CANONICAL-MPC-CLAIM.md).

## Repository layout

| Path | Contents |
|------|----------|
| `proto/circuit/` | gnark circuit for relation R (`derivation/`, `ckd/`), reference oracles, differential tests |
| `proto/vending/prover/` | Go prover: witness assembly, Groth16 setup/prove, wire serialization |
| `proto/vending/snapshot/` | Eligibility-snapshot builder + the committed 16,384-wallet at-scale test fixture (`testdata/`), deterministic generator, reproducibility tests |
| `proto/onchain/redemption/` | Plutus V3 contract: `RedemptionValidator`, `Recovery/Verify.hs` (committed verifier), `Gate.hs`, claim/deploy scripts, on-chain evidence |
| `proto/ceremony/` | MPC trusted-setup ceremony framework: `core` (BGM17 wrapper, TLV transcript, chain re-verification), `coord` (coordinator seam), `cmd/{contributor,verify-go}`, `spec` conformance vectors |
| `lean/` | Lean 4 proofs: `Ckd/`, `Validator/`, `ValidatorUPLC/` |
| `docs/` | `SPEC.md`, EARS requirements, `trusted-setup-ceremony.md`, design specs |
| `audit/` | Sixteen audit/review rounds, the alignment reconciliation map, the on-chain breakthrough review |
| `product/` | Redeemer and operator strawman web apps, the technical blog |
| `strategies/` | Onboarding docs for future sessions (formalization, code, graphify, sources) |
| `graphify-out/` | Code knowledge graph (1,200+ nodes) for navigation and context |
| `test.md` | E1 on-chain evidence (tx IDs, fund flow, ex-units) |

## TODO

The spine works. The road to something that can hold real money runs through these, roughly in order of how much they matter.

- [ ] **Run the multi-party trusted-setup ceremony.** A single-operator ceremony has been run on Preview (see the [MPC trusted-setup ceremony](#mpc-trusted-setup-ceremony) section); the production run is still open. Execute Phase 2 with the governance set, the white-hat, and unrelated external contributors over the `coord`/`contributor` path, seal on a public beacon (drand plus the Cardano epoch nonce), and publish the full transcript and the `verify-go` re-verification. This retires the single-operator caveat.
- [ ] **Close the sweep race.** Design and document the operational flow that moves at-risk funds into custody ahead of the attacker, including snapshot timing relative to the incident. This is the real-world hard part and it is currently named, not solved.
- [ ] **Eligibility-list governance.** Specify who builds the `(C, entitlement)` snapshot, how it is reproduced and challenged, and the solvency invariant (Σ entitlement ≤ custody, per asset) that gates every root commit.
- [ ] **Implement the spent-map / nullifier.** The version-dependent nullifier and the sharded sparse-Merkle spent-state (SPEC §8) are designed but not yet enforced on-chain; single-use currently rests on EUTXO structure. Needed for multi-claim and replay safety.
- [ ] **Discharge or formally defer the R1CS seam.** `circuit_models_relation` needs SHA-512/Ed25519 R1CS soundness; decide between a Picus/Ecne-class automated check and a scoped manual proof.
- [ ] **Re-prove the compiled validator (UPLC).** Carry the Lean app-logic proofs down to the compiled on-chain code via the PlutusCoreBlaster CEK formalization.
- [ ] **Harden the commitment-Y binding.** Bind the raw commitment `Y` bytes to the reconstructed point (canonical `Marshal`), closing the encoding-malleability gap noted in `audit/16` (F4).
- [ ] **Productionize the redeemer client.** Move the strawman to a real CIP-30 dApp with the WASM/native prover split and the relayer fallback.
- [ ] **Mainnet readiness review.** A full external audit of circuit, contract, and ceremony before any value-bearing deployment.

proof-zk-recovery

Explore Similar Repositories

Was this content helpful?

Recent Feedback

Download README