Fiat-Shamir reductions for Sigma protocols

This file exposes the CMA-to-NMA reduction used by the public Sigma security theorem. The proof is discharged by the direct stateful game chain; callers depend only on the reduction statement here.

theorem FiatShamir.cma_to_nma_advantage_bound {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel) (hr : GenerableRelation Stmt Wit rel) (M : Type) [DecidableEq M] [DecidableEq Commit] [Finite Chal] [Inhabited Chal] [SampleableType Chal] (simTranscript : Stmt → ProbComp (Commit × Chal × Resp)) (ζ_zk : ℝ) (hζ_zk : 0 ≤ ζ_zk) (hHVZK : σ.HVZK simTranscript ζ_zk) (β : ENNReal) (hPredSim : σ.simCommitPredictability simTranscript β) (adv : (FiatShamir σ hr M).unforgeableAdv) (qS qH : ℕ) (hQ : ∀ (pk : Stmt), signHashQueryBound M (adv.main pk) qS qH) : ∃ (nmaAdv : (FiatShamir σ hr M).managedRoNmaAdv), SignatureAlg.unforgeableAdv.advantage (runtime M) adv ≤ Fork.advantage σ hr M nmaAdv qH + ENNReal.ofReal (↑qS * ζ_zk) + ↑qS * (↑qS + ↑qH) * β

CMA-to-NMA reduction for Fiat-Shamir signatures built from a Sigma protocol.

The reduction runs the CMA adversary with simulated signing transcripts and a managed random oracle, then appends a single explicit live random-oracle query for the forgery's hash point so that the verification challenge is part of the forkable transcript (the nmaAdvFromCmaWithFinalQuery wrapper). The quantitative loss is the HVZK simulation cost plus the programming-collision term from simulator commit predictability; no separate verifier-guessing slack is needed.

The bound is stated against Fork.advantage σ hr M nmaAdv qH: the wrapped adversary issues qH + 1 random-oracle queries, and Fork.forkPoint qH indexes Fin (qH + 1), which is exactly the right number of forkable slots (the framework's structural +1 in Fin (qH + 1) is precisely the wrapper's verifier slot). The replay-forking denominator is therefore qH + 1.

theorem FiatShamir.nma_to_hard_relation_bound {Stmt Wit Commit PrvState Chal Resp : Type} {rel : Stmt → Wit → Bool} (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel) (hr : GenerableRelation Stmt Wit rel) (M : Type) [DecidableEq M] [DecidableEq Commit] [SampleableType Wit] [SampleableType Chal] (hss : σ.SpeciallySound) (hss_nf : ∀ (ω₁ : Chal) (p₁ : Resp) (ω₂ : Chal) (p₂ : Resp), Pr[⊥ | σ.extract ω₁ p₁ ω₂ p₂] = 0) [Fintype Chal] [Inhabited Chal] (nmaAdv : (FiatShamir σ hr M).managedRoNmaAdv) (qH : ℕ) : ∃ (reduction : Stmt → ProbComp Wit), Fork.advantage σ hr M nmaAdv qH * (Fork.advantage σ hr M nmaAdv qH / (↑qH + 1) - challengeSpaceInv Chal) ≤ Pr[= true | hardRelationExp hr reduction]

NMA-to-extraction via the forking lemma and special soundness.

The parameter qH is the fork slot parameter passed to Fork.forkPoint qH, i.e., the number of Fin (qH + 1) candidate target positions over which the replay-forking lemma sums. It is not required to be a valid query bound on the adversary: callers may supply a wrapped adversary with up to qH + 1 queries (the framework's structural +1 in Fin (qH + 1) accommodates the extra slot).