CMA-to-NMA reduction for Fiat-Shamir on Σ-protocols

This file contains the managed-RO NMA adversary construction used by the stateful Fiat-Shamir theorem chain and the public Sigma security theorem.

The construction is the standard "simulated CMA" adversary: run the CMA adversary's main computation, replace signing queries with simulator transcripts, program the managed random-oracle cache on each simulated signature, and return the final forgery together with that cache. The query bound below shows that live NMA random-oracle queries are exactly the source adversary's live hash queries; simulator-programmed signing queries are absorbed into the managed cache.

The quantitative CMA-to-NMA theorem itself lives in Sigma/Stateful/Chain.lean, so the public proof path has a single stateful source of truth.

Simulator handler components

@[reducible, inline]

abbrev FiatShamir.fsRoSpec (M Commit Chal : Type) : OracleSpec (ℕ ⊕ M × Commit)

@[reducible, inline]

abbrev FiatShamir.cmaOracleSpec (M Commit Chal Resp : Type) : OracleSpec ((ℕ ⊕ M × Commit) ⊕ M)

noncomputable def FiatShamir.simulatedNmaFwd {Commit Chal : Type} (M : Type) [DecidableEq M] [DecidableEq Commit] : QueryImpl (fsRoSpec M Commit Chal) (StateT (fsRoSpec M Commit Chal).QueryCache (OracleComp (fsRoSpec M Commit Chal)))

noncomputable def FiatShamir.simulatedNmaUnifSim {Commit Chal : Type} (M : Type) [DecidableEq M] [DecidableEq Commit] : QueryImpl unifSpec (StateT (fsRoSpec M Commit Chal).QueryCache (OracleComp (fsRoSpec M Commit Chal)))

noncomputable def FiatShamir.simulatedNmaRoSim {Commit Chal : Type} (M : Type) [DecidableEq M] [DecidableEq Commit] : QueryImpl (OracleSpec.ofFn fun (x : M × Commit) => Chal) (StateT (fsRoSpec M Commit Chal).QueryCache (OracleComp (fsRoSpec M Commit Chal)))

noncomputable def FiatShamir.simulatedNmaBaseSim {Commit Chal : Type} (M : Type) [DecidableEq M] [DecidableEq Commit] : QueryImpl (fsRoSpec M Commit Chal) (StateT (fsRoSpec M Commit Chal).QueryCache (OracleComp (fsRoSpec M Commit Chal)))

noncomputable def FiatShamir.simulatedNmaSigSim {Stmt Commit Chal Resp : Type} (M : Type) [DecidableEq M] [DecidableEq Commit] [Finite Chal] [Inhabited Chal] [SampleableType Chal] (simTranscript : Stmt → ProbComp (Commit × Chal × Resp)) (pk : Stmt) : QueryImpl (OracleSpec.ofFn fun (x : M) => Commit × Resp) (StateT (fsRoSpec M Commit Chal).QueryCache (OracleComp (fsRoSpec M Commit Chal)))

noncomputable def FiatShamir.simulatedNmaImpl {Stmt Commit Chal Resp : Type} (M : Type) [DecidableEq M] [DecidableEq Commit] [Finite Chal] [Inhabited Chal] [SampleableType Chal] (simTranscript : Stmt → ProbComp (Commit × Chal × Resp)) (pk : Stmt) : QueryImpl (cmaOracleSpec M Commit Chal Resp) (StateT (fsRoSpec M Commit Chal).QueryCache (OracleComp (fsRoSpec M Commit Chal)))

noncomputable def FiatShamir.simulatedNmaAdv {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)) (adv : (FiatShamir σ hr M).unforgeableAdv) : (FiatShamir σ hr M).managedRoNmaAdv

CMA-to-NMA reduction at the managed-RO interface.

Builds a managedRoNmaAdv from a CMA adversary adv and an HVZK simulator simTranscript: runs adv.main pk under a handler that forwards live RO queries (with cache side-effects), handles signing queries by sampling from simTranscript and programming the cache, and returns the final cache together with the forgery.

This is the concrete-interface reduction entering the replay-forking lemma.

theorem FiatShamir.simulatedNmaAdv_hashQueryBound {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)) (adv : (FiatShamir σ hr M).unforgeableAdv) (qS qH : ℕ) (hQ : ∀ (pk : Stmt), signHashQueryBound M (adv.main pk) qS qH) (pk : Stmt) : nmaHashQueryBound M ((simulatedNmaAdv σ hr M simTranscript adv).main pk) qH

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.