Signed-off-by: Daira-Emma Hopwood <daira@jacaranda.org>
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Signed-off-by: Daira-Emma Hopwood <daira@jacaranda.org>
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Add a Terminology entry stating that in this ZIP's discussion sections we
abbreviate H^{rcm,Orchard} as H^{rcm} (and similarly for other Orchard-
specific hash function names). Spec changes and references to other ZIPs
use the full forms.

Drop the now-redundant local abbreviation sentence at the start of the
Cost section, since the convention is established globally in Terminology.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…eduction.

The previous argument enumerated specific attack classes (a per-input
bullet list of "this input goes through this hash") and incorrectly
modelled f and g — the Sinsemilla-base lift and the K^Orchard-linear g
— as random oracles. f and g are deterministic functions of their inputs.

Replace with a reduction-based argument: any classical adversary that
finds two valid Recovery Statement witnesses for distinct underlying
notes with colliding nullifiers succeeds with probability bounded by
q(q-1)/r_P (≤ 2^-94 for Pallas with q ≤ 2^80). The reduction simulates
H^{rcm} as a lazily-sampled random oracle, extracts the algebraic
identity H_1 + f_1 + g_1 ≡ ±(H_2 + f_2 + g_2) (mod r_P), and bounds the
probability that two independent uniform RO outputs satisfy a fixed
linear constraint.

The argument does not assume Commit^{ivk}-binding (which would not hold
against a discrete-log-breaking adversary on Pallas) or collision-
resistance of the key-derivation hashes; it uses only H^{rcm}-as-RO plus
the structural fact that f and g are deterministic.

Also: replace "pq-collision-resistant" with "collapsing" in the
rehashed-commitment-tree discussion — the precise post-quantum binding
notion per Unruh 2016.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Signed-off-by: Daira-Emma Hopwood <daira@jacaranda.org>

…ture; Spendability-proof refinements.

**Make the key-binding argument rigorous** (to support the ε_kb term in
the Spendability proof): hoist the binding-break definition, ε_kb
advantage, and a formal theorem statement into a Security argument for
key binding section, with a proof sketch that mirrors the Spendability
reduction structurally.

**Lift flags out of the Recovery Statement and key-binding witness.**
The use_qsk and is_internal_rivk flag information is now encoded in
the witness's null structure: (sk = ⊥) ≠ (qk = ⊥) replaces the use_qsk
flag, and rivk ∈ {rivk_ext, H^{rivk_int}_{rivk_ext}(ak, nk)} replaces
the is_internal_rivk flag. The witness-structure form is strictly
stronger than flag-based: cross-branch attacks (e.g., w_1 with qk ≠ ⊥
and w_2 with sk ≠ ⊥, both opening the same ivk) are now in scope.
Co-nullable witness components are grouped as tuples — (qk, σ_qsk) is
a single (T_1 × T_2) ∪ {(⊥, ⊥)} field rather than two independently-
nullable fields with a separate consistency constraint.

**Fix a pre-existing bug:** rk = SpendAuthSig.RandomizePublic(α, ak^P)
was conditioned on use_qsk = true in the original Recovery Statement;
it should hold unconditionally.

**Spendability-proof tightening:**

* Split the pinning lemma into ivk-pinning (unconditional, per-witness,
  via discrete-log on prime-order Pallas) and PRF^{nf}-pinning (pair-
  conditional, via key-binding break absence).
* Make F's partiality explicit: F is defined under the no-key-binding-
  break conditioning, with (rseed, ρ, ψ) as fields of notetuple and
  PRF^{nf}_{nk}(ρ) pinned via the PRF^{nf}-pinning lemma.
* Handle the F_i = 0 (identity) case via § 5.4.9.7 convention
  Extract_P(O) = 0, citing the new protocol-concreteextractorpallas
  reference.
* Justify K_R being well-defined and nonzero.
* State the non-querying constraint where it does work: deterministic
  shifts in F are independent of H^{rcm} oracle responses.
* Add a tightness paragraph citing Maurer's classical-RO collision
  bound k(k-1)/(2N), with the factor-of-2 derivation for the
  ±-equivalence in our win condition.
* Drop "or extracts from internal state" from the ε_{kb} definition.
* Rename ε_{Commit^{ivk}}(A) to ε_{kb}(A, q_{kb}) — parameterized by
  query count, scoped to "key-binding" rather than just Commit^{ivk}.
* Add the substituted concrete bound: by the key-binding theorem,
  ε_{kb}(A, q_{kb}) ≤ q_{kb}(q_{kb}-1)/r_P, so the overall Spendability
  bound is at most (q_{rcm}(q_{rcm}-1) + q_{kb}(q_{kb}-1))/r_P.

**Notation cleanup:**

* F → \mathsf{F} (function names sans-serif; F_1, F_2 stay italic as
  values).
* q → q_{rcm} / q_{kb} (subscripted by which RO is being counted).

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Signed-off-by: Daira-Emma Hopwood <daira@jacaranda.org>

Restructure the key-binding theorem's proof sketch around a "final
random oracle" formulation, absorbing the previous internal-IVK case
into the others; tighten each case's WLOG step to derive distinctness
from predicate determinism rather than from a vague witness-distinctness
claim. Correct the bound to 3 q_kb(q_kb-1)/(2 r_P) to account for the
upstream-RO collision residual in the both-internal sub-case, which the
previous bound q_kb(q_kb-1)/r_P missed; propagate the corrected constant
to the Spendability theorem's combined bound.

Update G notation (function mathsf, output values italic) to match
the F convention.

Update the high-level summary's binding-argument paragraph to describe
both branches symmetrically, matching the lifted formal statement.

Define the break event at the projection level (distinct
(qk, sk, ak, nk, rivk)), making explicit that the y-sign of ak^P is
intentionally not part of the binding equivalence class — consistent
with Orchard's existing design choice to use ak as a single
F_{q_P} element.

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Use BLAKE3.derive_key with context string "Zcash ZIP 2005 qk-derivation v1"
and 32-byte output. Requires one BLAKE3 compression in the SoK^{qsk}
circuit, with the derive_key context key precomputed as a constant.

Add a BLAKE3 reference.

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>