spec: bind each member's SpendRecord.nullifiers to its committed input_nullifiers_root

[TaprootFreak]

Why (soundness — fork double-spend / inflation)

Same class as the coin-amount binding (#81/#82), applied to the anti-double-spend commitment itself. The nf values inserted into the global nullifier accumulator come from the free-witness SpendRecord.nullifiers list — §2.2 clause 3 sets batch_nullifiers = the multiset union of member lists — but no clause bound that list to the input_nullifiers_root (inr) each per-account proof committed. Clause 1 binds only the root inr to ProofData (root-to-root) and never opens it to the individual nf; clause 9 keeps the nf private to C.

The attack

1. Malicious spender owns coin C (amount 100), true nullifier nf_C.
2. Build an honest per-account proof: spend C → pay Bob 100; inr = NullifiersRoot([nf_C]); sign message = inr ‖ ocr, S2C over H(ProofData). Verifies.
3. In the SpendRecord handed to the publisher, set nullifiers = [], k = 0, leaving the signed message untouched.
4. C_batch verifies (clause 3 union = [], clause 4 empty insert), batch admitted — nf_C never inserted. Bob credits 100 (clause 10(d) never inspects the list).
5. In a fork (§1.6 allows forks — no global account registry), re-spend C: nf_C is still absent from the live accumulator → passes → pay Carol 100.
6. Coin C (100) spent once, 200 delivered. Unbounded by repetition.

Found by an adversarial soundness sweep (three attack lenses converged on it independently; the verify pass confirmed no in-circuit or receive-side check catches it).

Fix

§2.2 clause 3 now requires, for each member:

NullifiersRoot(SpendRecordⱼ.nullifiers) == ProofDataⱼ.input_nullifiers_root   (= messageⱼ.inr)
SpendRecordⱼ.k == |SpendRecordⱼ.nullifiers|

using the §1.7.5 NullifiersRoot construction (tag, L_⊥ padding). C_batch cannot re-derive the nf from nk (private to C), but it can open the committed root to the declared list — both inr (in ProofData) and the list (in the SpendRecord) are available, no nk needed. Since C already guarantees inr = NullifiersRoot(correctly-derived nf), NullifiersRoot(list) == inr proves the inserted list is the opening of each member's committed root — no nf can be dropped or substituted. NullifiersRoot([]) = L_⊥ ≠ inr makes the nullifiers=[] proof unsatisfiable; the empty-list case (mint/receive, inr = L_⊥, k = 0) passes trivially.

The binding is also anchored at the operative insertion site (§2.5 leaf mode, now clauses 1–3), and the §2.1 clause 4 cross-reference and the §2.4 / §3.6 step 7-8 prose are hardened to state the opening rather than merely assert "correctly derived".

Scope

6 line-level edits in specification.md; no test vectors affected (pure normative addition over the existing inr definition and k field). Reviewed adversarially for residual vectors (inr forgery, 2nd-preimage, k consistency, padding, mint case, interaction with #82) — all closed.

[TaprootFreak]

Ready for review. Found by an adversarial soundness sweep (six attack lenses over the current spec — the follow-up to the #81/#82 fix, applying the same 'is every value-bearing field bound to a verifier-checked commitment?' question to the rest of the protocol). Three lenses converged on this one independently; the verify pass confirmed no in-circuit or receive-side check catches it.

Two review passes (soundness + consistency in parallel each round). Pass 1 confirmed the core is sound but found the §2.5 leaf-mode enumeration still listed clauses 1–2 — the operative insertion site where the new opening check must live — plus two minors (an m symbol overload in clause 3, a tense slip in §3.6 step 8). Pass 2: both lenses clean, residual vectors (inr forgery, 2nd-preimage, k-consistency, padding, the mint/empty-list case, interaction with #82) all checked and closed.

Wording/normative only, no test vectors affected.