# 16 — On-chain Breakthrough Review (2026-06-27c)

Review of the milestone: a real client-generated 3,450,403-constraint Groth16 recovery proof
verified by a live Cardano Preview node and funds released. Six-agent review (verifier soundness,
on-chain evidence, contract integration, prover/commitment, spec reconciliation, formal/Lean) +
an adversarial refutation pass on the two high findings. Raw findings:
`scratchpad/review2/{R1..R6,RB-A,RB-B}.md`.

## Bottom line

**The breakthrough is real and independently verified — and it is a verify-only gate, not bound
redemption.** Both halves of that sentence are load-bearing.

- **Verified (R2, via Koios):** lock tx `168b4de3…` and spend tx `7f7f41e0…` are real on Preview.
  The spend consumed the gate UTxO, executed a PlutusV3 script whose hash is exactly the repo's
  compiled `gate.plutus` (`bb6a2410…`), the redeemer is **byte-for-byte** the repo's `proof_c.hex`,
  the script **succeeded**, and 3.5 tADA was released. The on-chain commitment-aware verifier
  accepted a genuine BSB22-committed proof.
- **Cryptographically sound on the main path (R1, R4):** the commitment-aware verifier matches
  gnark's BSB22 verify (PoK pairing, `e_cmt` challenge, fold `vk_x = K0 + pub·K1 + e_cmt·K2 +
  commitment`, final Groth16). The prover↔verifier wire format and the `e_cmt` challenge are
  **byte-exact** (14/14 fields; `ecmt_test.go` cross-checks gnark `fr.Hash`). No honest proof is
  rejected; the main pairing resists forgery.
- **But (R3, RB-A CONFIRMED):** the deployed script (`Gate.hs::mkGate`) is **verify-only** — it
  binds no destination, entitlement, value, or self-pay, so a proof revealed in the mempool can be
  spent to any address (front-runnable). The full `RedemptionValidator` (which *does* bind D +
  entitlement + no-self-pay) wires the **vanilla** `groth16Verify` and would therefore **reject**
  the real committed proof. No single deployable script both verifies the committed proof and binds
  the payout. The live demo proves the verifier integration; it does **not** exercise bound redemption.

## Findings (severity-ranked, post-refutation)

| # | Sev | Finding | Status |
|---|---|---|---|
| **F1 (R3-01/R6-02)** | **High** | **Verifier/binding split.** `mkValidator` uses vanilla verify (rejects real proofs); deployed `mkGate` uses the committed verifier but binds nothing (front-runnable). Fix: wire `groth16VerifyCommitted` into `mkValidator`, deploy that, retire `Gate` as a redemption path. | open (integration) |
| **F2 (R5)** | **High (prod)** | **Throwaway trusted setup.** `test.md`: single-party local `groth16.Setup` (12m, WSL). Retained toxic waste forges any proof; satisfies zero of REQ-TS-01..14. Fine for testnet; hard mainnet blocker — needs a real MPC ceremony. | open (production) |
| **F3 (R6-01)** | **High (fidelity)** | **Lean lags the impl.** `Validator.lean` still models the pre-M1 `payAddr == r.destination` CBOR equality that M1 deleted, and lacks `payoutOk` + len-57. `v_cons` now proves a check the contract no longer performs. Fix: add V-PAYOUT (`payoutMatchesDestination`), restate `v_cons`. | open |
| **F4 (R1-01/R4-04/RB-B)** | **Low–Med** | **Commitment `Y` not bound to the point.** `e_cmt` hashes the raw prover `Y` bytes; the point uses only X+sign (no `Y<p`/on-curve/`Y==Y_P` check). Diverges from gnark's canonical `Marshal()`. Malleability (~2^383 encodings/point), not forgery (the main pairing pins `e_cmt`). Fix: hash the canonical reconstructed point, or enforce canonical Y. | open |
| **F5 (R2)** | Med | **Tampered-rejection not chain-evidenced.** Tx3 `0279ff4c…` is absent from chain (a pre-submission rejection leaves no artifact), so "tampered rejected on-chain" is asserted, not third-party verifiable. (`RecoveryVerifySpec` does reject tampered A and tampered-Y off-chain.) | scope note |
| **F6 (R5)** | Med | **Spec describes only vanilla Groth16.** SPEC §3/§6 + REQ-V-02/05/08/D1-12 specify a 192B-proof/432B-VK vanilla verify; the implemented/verified path is commitment-aware (336B/672B). GAP-1: add §3.x + REQ-V-14 (DST `bsb22-commitment`, expand_message_xmd SHA-256, LE-mod-r, PoK, fold). GAP-2: REQ-TS-16 (throwaway-setup demo = non-production). GAP-3: no REQ-D-E2E for the on-chain milestone. | open (doc) |
| **F7 (R3-02)** | Med | **Nullifier is dead code; no spent-map.** Single-use rests entirely on EUTXO consumption + the unenforced "one custody UTxO per (C,entitlement,snapshot)" assumption. The version-dependent nullifier + §8 migration are unimplemented. | known/deferred |
| **R4-02/R4-03** | Low | Setup is single-party (covered by F2); the Haskell `expandMsgXmd48` is only indirectly tested — add a direct assertion vs `ecmt.hex`. | minor |

## What the review CONFIRMED sound

- The commitment-aware verifier is cryptographically correct on the main verification path and
  byte-exact with the prover (R1, R4); fail-closed on any parse/uncompress error.
- The on-chain redemption is real and reproducible from the repo artifacts (R2).
- Inside `mkValidator`, the `validateClaim` conjunction is sound against the five claim-fraud vectors
  (R3); `reconstructPub` binds authenticated context; `payoutMatchesDestination` (the M1 fix) is sound.
- **C1 is CLOSED** — the commitment-aware verifier that was the dominant `audit/15` defeater is
  implemented and on-chain verified (R5).
- Axiom hygiene intact: proved theorems ⊆ `{propext, Classical.choice, Quot.sound}`, one isolated
  seam `sorry` (R6). The deferred R1CS/UPLC seams are unchanged by the on-chain win.

## Prioritized next steps

1. **[High] Close F1** — wire `groth16VerifyCommitted` into `RedemptionValidator.mkValidator`, redeploy
   the *bound* validator, and run a Preview claim that binds D + entitlement (not the verify-only gate).
   This is the gap between "the verifier works on-chain" and "bound recovery works on-chain."
2. **[High, prod] F2** — plan the trusted-setup MPC ceremony before any value-bearing deployment.
3. **[High] F3** — bring the Lean Validator model up to the M1 impl (V-PAYOUT).
4. **[Med] F6** — fill the SPEC commitment-scheme gap (§3.x + REQ-V-14, REQ-TS-16, REQ-D-E2E).
5. **[Low–Med] F4** — canonicalize the commitment-Y binding.
6. **[Med] F7** — implement the spent-map / nullifier recording for multi-claim/replay safety.

The on-chain milestone genuinely closes C1 and proves the hardest piece (a real commitment-carrying
proof verifying on a live node). The remaining work is integration (F1), production hardening (F2),
and keeping the spec + Lean caught up (F3, F6).