# 15 — Alignment Reconciliation Map (2026-06-27)

Traceability-and-assurance map across the four representations of the recovery relation R — the
English/EARS **spec**, the gnark Groth16 **circuit**, the on-chain Plutus **contract**, and the
Lean **formal proofs**. Built per `docs/superpowers/specs/2026-06-27-alignment-reconciliation-map-design.md`
by multi-agent layered reconciliation (spec/circuit/contract/formal) + adversarial verification of
the high-severity seams, seeded from the code graph (`graphify-out/`). Spans two branches:
`feat/redemption-contract-v1` (contract + Lean Validator/UPLC + improved Ckd) and
`proto/preprod-experiments` (the full relation-R circuit `proto/circuit/derivation`).

## Bottom line

The reconciliation worked: it found one **Critical** and one **High** cross-layer defect that the
single-layer reviews had each reported as fine, plus confirmed several layers are genuinely sound.

- **M1 (Critical) — the public-input binding is NOT aligned.** The field *order* matches across
  all three layers, but the circuit and the contract compute `pub` over **different byte
  encodings** of `D` and `entitlement`. As written, an honest prover's circuit `pub` cannot equal
  the contract's `reconstructPub`. The on-chain scalar reduction is also unimplemented (the
  `groth16Verify` stub discards `pub`). This must be fixed before any end-to-end claim.
- **M2 (High) — the nullifier contradicts SPEC §3.4.** The contract, REQ-D1-08, and Lean V-NULL
  include `snapshot_version`; §3.4 mandates excluding it. Latent in single-snapshot v1; enables
  cross-version double-claim once the spent-map exists.
- **The circuit's free-input/hint ledger is clean** — no Orchard-class unbound signal. The CKD
  and credential gadgets are sound and complete (QA PASS, differential-clean). The CKD *relation*
  is faithfully formalized in Lean. The `pub`-binding **field order** is consistent (the `44a8a8f`
  reconciliation held).

The top assurance claim — *"the vending machine never releases ADA on an invalid proof"* — has
**open defeaters** (M1, the stub verifier, the deferred circuit/UPLC seams) and is therefore not
yet discharged. That is the honest current state.

## 1. Layered traceability matrix

Status per cell uses **S**(ound)/**C**(omplete) where both apply. ✅ established · ◐ partial ·
✗ gap · ⚠ mismatch · ⟂ deferred.

| # | Component | Spec (anchor) | Circuit (gnark, preprod) | Contract (Plutus, feat) | Proof (Lean, feat) |
|---|---|---|---|---|---|
| R1 | CKD leaf `kL` | SPEC §3.3; REQ-CKD-S/F/VR-* | `ckd/chain,step,adder,encoding` — S✅ C✅ | — (witness) | `Rckd`+S-01..06+`adder_exact_chain`+`ckd_rejects_bit255` — C✅, rejection ◐ (bit255 only; tag/canon/clamp ⟂ seam) |
| R2 | leaf `A`, `C=Blake2b-224(A)` | SPEC §3.3; REQ-D-LEAF | `credential.go` (same KLbits, F1/F2 closed) — S✅ C✅ | — | not formalized ⟂ (opaque) |
| R3 | entitlement (EntLen 553, ≤8 assets) | SPEC §3.3; REQ-D-ENT; REQ-B-06/07 | `entitlement.go` well-formedness S✅ C✅; **ordering ✗ by design** | `CustodyDatum.entitlement` (CBOR `Value`) — see M1 | `v_cons` per-claim ✅; global Σ ⟂ Blaster |
| R4 | Merkle inclusion depth-14 | SPEC §3.3; REQ-D-MERKLE | `merkle.go` (range-checked siblings, 0x00/0x01 tags) — S✅ C✅ | `merkleRoot` (Params) | not formalized ⟂ (opaque root) |
| R5 | **pub binding** `pub=Fr(Blake2b-256(DOM))` | SPEC §3.1; REQ-D-PUB; V-PUB | `binding.go` (722-byte DOM, LE mod r) — S✅ C✅ | `reconstructPub` (`Logic.hs`) — **⚠ M1** | `v_pub_reconstructed` (pub = reconstructPub) ✅ app-logic; UPLC ⟂ |
| R6 | Groth16/BLS12-381 gate | REQ-V-*, REQ-TS-* | proof system, K=22; full prove/verify ⟂ (N1) | `mkValidator`/`groth16Verify` — **stub** ⚠ | `v_pub` proves the gate; soundness assumed (opaque) ⟂ |
| R7 | nullifier | SPEC §3.4 (version-independent) | not in circuit (by design) | `nullifier` (`Logic.hs`) — **⚠ M2** | `v_null` credential-determinism ✅ — but certifies the wrong formula |

## 2. Free-input / hint ledger (circuit) — CLEAN

Every prover witness (MasterKL/KR/CC, account/role/index, Ent, Version, ScriptHash, D, Root,
Path.Siblings/Dirs, Pub, per-column lo/carry) has an explicit binding constraint. The single gnark
hint `splitByteHint` (adder.go) is bound by `v == lo + 256·carry` + two range checks; its value is
never trusted. `role` is one shared wire across `DeriveChain` and `Bind` (role coherence holds).
**No unbound signal — no Zcash-Orchard-class soundness hole on the circuit side.** Residual trust:
the `std/math/uints` range-check primitives (vetted boundary) and the deferred full proving run.

## 3. Mismatch register

### M1 (Critical) — pub-binding encoding mismatch  ⟶ defeater on the top claim
Confirmed by adversarial verification (`scratchpad/align/RB-pubdom.md`).
- **Order:** ALIGNED — `domainSep ‖ scriptHash ‖ version ‖ root ‖ C ‖ entitlement ‖ D ‖ role`
  in SPEC §3.1, `binding.go:48`, and `Logic.hs:28-36`. (The Haskell test certifies order only,
  with placeholder strings.)
- **`D` width/encoding:** MISMATCH — circuit binds a 57-byte canonical Shelley address
  (`ref.go AddrLen=57`); contract folds `serialiseData(toBuiltinData Address)` (PlutusData/CBOR).
  Different bytes ⇒ different Blake2b preimage.
- **`entitlement`:** MISMATCH — circuit uses the fixed 553-byte `EntLen` layout (`params.go`);
  contract folds `serialiseData(toBuiltinData Value)` (CBOR map). Structurally unrelated.
- **Digest→scalar reduction:** NOT IMPLEMENTED on-chain — circuit commits `LE(Blake2b256(DOM)) mod r`;
  contract emits the raw 32 digest bytes, deferring reduction to `groth16Verify`, which is a stub
  (`Verify.hs:19`) that discards `_pub`. LE-vs-BE / mod-r cannot be confirmed.
- **`domainSep`:** unpinned — circuit hardcodes `"CKD-RECOVERY-v1"` (15 B); contract uses a
  deploy-time `pDomainSep` param with no literal pin.
- **Impact:** as written the off-chain prover (circuit `pub`) and the on-chain `reconstructPub`
  bind different preimages, so a legitimate proof would not verify (completeness break); forcing
  them to "match" without fixing the encodings would open a soundness gap. **The whole E2E rests
  on this.** Fix: pin one canonical byte encoding of `D` and `entitlement` (and the reduction +
  domainSep literal) and prove the circuit, contract, and snapshot tooling all use it.

### M2 (High) — nullifier `snapshot_version` contradiction  ⟶ defeater (latent)
Confirmed (`scratchpad/align/RA-nullifier.md`). SPEC §3.4: `nullifier = Blake2b(domain_sep ‖
scriptHash ‖ C)`, version-independent, "MUST NOT include snapshot_version." Contract `Logic.hs:42`,
REQ-D1-08, and Lean `Validator.lean:40`/`v_null` all **include** `snapshotVersion`. Impl-bug +
requirements-bug vs the §3.4 anchor (not a spec bug). Harmless in single-snapshot v1 (EUTXO
single-use); at multi-snapshot with the global spent-map (REQ-B-09) the same `C` yields a different
nullifier per version → cross-version double-claim (threat BT-ST-6). `v_null` only proves
credential-determinism, so it silently certifies the version-dependent formula. (Nuance: §8 /
REQ-B-13 permit a version-dependent branch *only* with a verified cross-version spent-state
migration, which does not exist; the layers are inconsistent either way.)

### Residual cross-checks (cannot be closed from code alone)
The real `groth16Verify` must apply LE+mod-r; the off-chain prover must hash the exact `D`/
entitlement bytes the contract folds in; deploy must set `pDomainSep="CKD-RECOVERY-v1"` and the
snapshot tooling must emit the 28/8/32/28 widths. Each needs a translation-validation certificate.

## 4. Gap register — eliminative-argumentation assurance case

**Top claim G0:** *the vending machine never releases ADA on an invalid proof.* Discharged only if
every failure vector is eliminated. Current state:

| Vector | Eliminated by | Status |
|---|---|---|
| Circuit under-constrained (forge) | free-input ledger (§2) + circuit QA PASS | ✅ eliminated (circuit side); automated Picus/Ecne/AC4 re-check recommended |
| `pub` not bound to context / wrong preimage | `v_pub_reconstructed` + **M1** | ✗ **OPEN defeater (M1)** |
| On-chain verifier doesn't actually verify | real CIP-381 `groth16Verify` | ✗ **OPEN — stub verifier** |
| Plutus app-logic bug | `v_*` proofs (app-logic) + Blaster UPLC | ◐ app-logic ✅; UPLC re-proof ⟂ |
| Nullifier re-randomization / cross-version | `v_null` + **M2** | ◐ v1 ok; ✗ **OPEN defeater (M2)** at multi-snapshot |
| Circuit ≠ relation R (R1CS) | `circuit_models_relation` | ⟂ **deferred-blocked** (defeater recorded) |
| Trusted-setup fault | ceremony evidence | ⟂ out of scope (defeater recorded) |

**G0 is NOT discharged** — open defeaters M1, the stub verifier, and the deferred seams. A
companion **liveness** claim (*any legitimate victim can recover*) is also blocked by M1
(completeness break) until the encodings align.

**VLF (contract):** Validity ◐ (per-claim binding sound; "at most once" rests on EUTXO single-use,
v1 single-claim, no spent-map); Liquidity ◐ (no lock-up; gated by stub verifier); Fidelity ◐
(matches spec except M2; global Σ-conservation/batch-AON/spent-map deferred).

## 5. Branch-divergence register (`feat` is canonical for Lean)

1. **Circuit** (full relation R, `proto/circuit/derivation`) exists **only on preprod**; contract +
   `Validator.lean` + `ValidatorUPLC` exist **only on feat**. The two must converge on one branch.
2. **lean/Ckd theorem sets differ:** feat-only `adder_exact_chain`/`ckd_rejects_bit255`/
   `ckd_bit255_unsat` (typed-subtype model, no axiom); preprod-only `adder_exact_soft`/
   `no_mod_L_alias_soft`/`bit255_invariant_perhop`/`*_wellFormed`. Neither is a superset — re-land
   preprod's soft/per-hop theorems onto feat's typed model.
3. **V-PUB DOM order agrees** across branches (the `44a8a8f` reconciliation held); only loose `vk`
   prose remains.
4. REQ-B numbering drift and stale `Seam.lean` line refs (doc-only, low).

## 6. Axiom/build ground truth (formal layer)

Proved theorems ⊆ `{propext, Classical.choice, Quot.sound}` (Validator = `{propext}`); zero
`axiom`/`native_decide`; exactly one isolated `sorry` (`circuit_models_relation`, REQ-CKD-VR-03,
deferred-blocked on ~2.77M opaque HMAC/Ed25519 constraints), a true non-propagating leaf.

## 7. Prioritized punch-list (the phased program that follows)

1. **[Critical] Close M1** — define one canonical byte encoding for `D` and `entitlement`, pin
   `domainSep` and the LE-mod-r reduction; make the circuit, the contract `reconstructPub`, and the
   snapshot/prover tooling provably agree; add a translation-validation certificate at the
   prover↔contract boundary. Nothing E2E is sound until this lands.
2. **[High] Resolve M2** — decide version-independent (per §3.4: fix `Logic.hs`, REQ-D1-08, Lean)
   vs version-dependent-with-migration (per §8: build the verified migration); correct V-NULL so it
   actually tests version-independence.
3. **[High] Replace the `groth16Verify` stub** with the real CIP-381 BLS12-381 verifier and prove
   it matches the verification equation (the Lean Groth16-soundness spec; the Blaster UPLC path).
4. **[Med] Entitlement ordering** — add a REQ-V requirement + validator check (the circuit excludes
   it by design; currently no layer enforces canonical ordering on-chain).
5. **[Med] Branch convergence** — bring the circuit and the Lean Validator/UPLC onto one branch;
   re-land preprod's soft/per-hop CKD theorems onto feat's typed model.
6. **[Med] Automated under-constraint re-check** — run Picus/Ecne/AC4 on the gnark R1CS export as a
   standing gate, even though the manual ledger is clean.
7. **[Track] Deferred seams** — R1CS `circuit_models_relation`, the UPLC invariant re-proofs
   (Blaster Phase 3+), the full Groth16 proving run; each carries a recorded defeater.
8. **[Infra] CI-gate this map** so it re-checks on each change and flags drift.

Raw per-workstream findings: `scratchpad/align/W1..W4` + `RA`/`RB`.

---

## Update (post-merge with `feat/vending-machine`, 2026-06-27b)

Re-examined the map against the merged vending-machine integration (real Groth16 verifier, canonical
entitlement encoder, full circuit + contract in one tree). Status of each finding:

| Finding | Before | Now | Note |
|---|---|---|---|
| M1 · entitlement encoding | ✗ CBOR `Value` vs 553B `EntLen` | ✅ **FIXED** | `Recovery/Entitlement.hs` `encodeEntitlement` → canonical 553B (ada‖count‖8×(policy28‖name32‖qty8)), sorts assets ASC; `validateClaim` checks `encodeEntitlement payVal == cdEntitlement` |
| R3 · entitlement ordering | ✗ not enforced on-chain | ✅ **FIXED** | the canonical encoder sorts, so the on-chain check enforces canonical order |
| M1 · LE-mod-r reduction | ✗ unimplemented (stub) | ✅ **FIXED** | `Recovery/Verify.hs` is the REAL BLS12-381 verifier; reads the 32-byte digest LITTLE-ENDIAN and reduces mod r, matching `bytesToFieldLE`/`RefPub` |
| M1 · `groth16Verify` stub | ✗ `p=="VALID_PROOF_STUB"` | ◐ **REAL but vanilla** | real pairing check via CIP-381 builtins — but see C1 below |
| **M1 · `D` encoding** | ✗ CBOR vs 57-byte raw | ✗ **STILL OPEN** | `RedemptionValidator.hs:29` `addrBytes = serialiseData . toBuiltinData` (CBOR PlutusData) vs circuit `ref.go AddrLen=57` raw Shelley (`header ‖ payment28 ‖ stake28`, per `prover/cmd/realprove`). Contract `pub` preimage ≠ circuit `pub` preimage → proof cannot verify. |
| M1 · `domainSep` pin | ✗ unpinned | ✗ **OPEN** | circuit hardcodes `"CKD-RECOVERY-v1"`; contract uses deploy-time `pDomainSep` param (must be pinned or hardcoded) |
| **C1 · commitment-aware verifier** | (new) | ✗ **PENDING** | the real gnark proof carries a Pedersen COMMITMENT (`nbCommitments=1`, from lookup-table hashing) that the current vanilla A‖B‖C verifier drops; `RecoveryVerifySpec` marks the real proof as currently rejected on-chain until a commitment-aware verifier (commitment parse + PoK + folding) lands |
| **M2 · nullifier version** | ✗ open | ✗ **OPEN — design fork** | SPEC §3.4: `Blake2b(domain_sep ‖ scriptHash ‖ C)`, version-INDEPENDENT, "MUST NOT include snapshot_version". Contract `Logic.hs`, Lean `Validator.lean`, AND REQ-D1-08/D1-13 all INCLUDE `snapshotVersion`; §8/REQ-TS-15 design version-dependent nullifiers + cross-version migration. Three impl layers vs §3.4 disagree on a soundness property. Moot in single-snapshot v1; load-bearing at multi-snapshot. |
| Free-input/hint ledger | ✅ clean | ✅ clean | unchanged |
| Branch convergence | ✗ split | ✅ **converged** | circuit + contract + vending now in one tree; this merge also brings the analysis layer + ValidatorUPLC alongside |

**Net:** the update closed the entitlement, ordering, and reduction parts of M1, converged the branches,
and stood up the real verifier. Remaining: M1 `D`-encoding (concrete fix), `domainSep` pin (minor), C1
commitment-aware verifier (the active crypto front), and M2 (a design fork the spec contradicts itself on).

### Resolutions applied (2026-06-27b)

- **M2 — RESOLVED (design decision: version-dependent is canonical).** SPEC §3.4 reconciled to the
  implemented version-dependent nullifier `Blake2b(domain_sep ‖ scriptHash ‖ snapshot_version ‖ C)`,
  with the §8 / REQ-TS-15 cross-version spent-state migration REQUIRED for multi-version deployments
  (so a credential cannot be claimed once per version). The contract, the Lean model (`v_null`), and
  REQ-D1-08/D1-13 were already consistent; SPEC §3.4 was the stale outlier and is now fixed. This
  also inverts the `audit/14 §6` "V-NULL prose drift" note — the Lean was correct.
- **`domainSep` — deploy-pin invariant (no code bug).** The circuit hardcodes `"CKD-RECOVERY-v1"`
  (`ref.go`); the contract's `pDomainSep` Param MUST be deployed equal to it. The prover fixtures
  already use that constant, so it is consistent in practice; flagged as a deploy invariant (assert
  `pDomainSep == "CKD-RECOVERY-v1"` at deploy / in the conformance test). REQ-D1-13's
  "domain_sep reconstructed from scriptHash+version" is a DIFFERENT, unimplemented design — recorded.
- **M1 `D`-encoding — FIXED contract-side (credential-comparison).** The validator now binds the
  payout to `D` by comparing the output's payment/stake credential hashes against the 57-byte
  `crDestination` (`header ‖ payment28 ‖ stake28`), replacing the wrong CBOR `serialiseData`. This is
  robust to the header convention. **Coordination required:** the prover/snapshot (the active vending
  front) currently uses a STUB address (`makeAddr` = `0x60 ‖ 28×02 ‖ 28×03`); the real claim flow must
  emit `crDestination` as the real 57-byte base address and pay to it. The contract side is now correct;
  the end-to-end closes once the prover emits matching 57-byte `D`.
- **C1 commitment-aware verifier — OPEN (owner's active front).** The dominant remaining work: the real
  gnark proof carries a Pedersen commitment (`nbCommitments=1`) the vanilla on-chain verifier drops.
  Implementing the commitment-aware verification equation on-chain is tracked separately.

**Updated top-claim status:** G0 ("never release ADA on an invalid proof") still has open defeaters —
now narrowed to C1 (commitment-aware verifier) + the prover-side `D`-format finalization + the deferred
R1CS/UPLC seams. The entitlement, reduction, ordering, and contract-side `D`-binding defeaters are closed.

---

## Update (on-chain breakthrough, 2026-06-27c) — see `audit/16` for the full review

A real 3.45M-constraint commitment-carrying Groth16 recovery proof was **verified on a live Cardano
Preview node and released funds** (tx `7f7f41e0…`, independently confirmed via Koios). Six-agent
review + refutation: `audit/16-onchain-breakthrough-review.md`.

- **C1 (commitment-aware verifier) — CLOSED.** `Recovery/Verify.hs::groth16VerifyCommitted` (gnark
  BSB22: commitment uncompress, Pedersen PoK, `e_cmt` RFC-9380 challenge, fold, Groth16) is real,
  byte-exact with the prover, and on-chain verified. The dominant defeater is eliminated.
- **New F1 (High) — verifier/binding split.** The deployed gate (`mkGate`) is verify-only (no D /
  entitlement / self-pay binding → front-runnable); `mkValidator` (which binds those) wires the
  *vanilla* verifier and would reject the real committed proof. The live win exercises the verifier,
  **not** bound redemption. Fix: wire `groth16VerifyCommitted` into `mkValidator`.
- **New F2 (High, production) — throwaway trusted setup** (single-party local). Mainnet blocker.
- **New F3 (High, fidelity) — Lean lags M1.** `Validator.lean` still has the deleted CBOR
  `payAddr == r.destination`; needs V-PAYOUT.
- **REQ-V-15 Lean mirror — DONE.** `Validator.lean` now models the PR #10 `payCredOf D ≠ C`
  conjunct in `validateClaim` and proves it (`v_dest_not_claimed`), keeping the Lean
  re-statement in step with the shipped Haskell. INDEPENDENT of F3 above: it does not touch the
  `payAddr == r.destination` / V-PAYOUT encoding lag, which stays OPEN. Source-level fidelity
  only; the compiled `redemption.plutus` UPLC regen is a separate item.
- **F4 (Low–Med) — commitment-`Y` not bound** (malleability, not forgery).
- **Spec gaps (F6)** — SPEC describes only vanilla Groth16; add the commitment-scheme §/REQ-V-14,
  REQ-TS-16 (non-production setup), REQ-D-E2E.

**Updated G0:** the top claim is **substantially discharged for the testnet verifier-integration
demo**, with named open defeaters: F1 (bound-redemption integration), F2 (trusted setup), the
deferred R1CS/UPLC seams. M1/M2 and C1 are closed.