Research proof index

Hash-query bound for simulatedNmaAdv: if the CMA adversary makes at most qS signing-oracle queries and qH random-oracle queries, the NMA reduction makes at most qH live hash queries. The qS signing queries are absorbed into the managed cache rather than issued live.

Native stateful top-level chain, assuming the H5 replay-forking boundary. This theorem carries the H1/H2/H3/H4 arithmetic directly in the stateful chain. The bound is in terms of the verify-wrapped adversary nmaAdvFromCmaWithFinalQuery at fork slot parameter qH.

Expected H3 loss from direct signing and hash query bounds. If the adversary makes at most qS signing queries and at most qH random oracle queries, the accumulated state-dependent signing slack is bounded by the standard qS * ζ + qS * (qS + qH) * β expression.

On a valid keypair state, the total-variation distance between the real and simulated signing oracle on a single signing query is bounded by cmaSignEpsCore.

Logging signing inputs while forwarding all queries preserves the joint signing/hash query bound.

H5 boundary in shifted-NMA form. This is the fork-side statement after the native H4 normalization has moved cmaSim to nma ∘ cmaToNma. The bound is in terms of the verify-wrapped adversary nmaAdvFromCmaWithFinalQuery at fork slot parameter qH (the framework's Fin (qH + 1) indexing accommodates the wrapper's verifier-point query).