Native stateful Fiat-Shamir CMA-to-NMA chain

This file assembles the non-heap Fiat-Shamir EUF-CMA chain. The top-level statement is factored so the H1/H2/H3 arithmetic is native immediately, while the H5 replay-forking boundary can be ported as a focused lemma.

Tag the CMA-to-NMA simulator handler family from Sigma/CmaToNma.lean into the local fs_simp simp set. These defs live upstream (not under Sigma/Stateful/), so we attach the FS-stateful local attribute here rather than at the definition sites.

CMA-to-NMA adversary

noncomputable def FiatShamir.Stateful.nmaAdvFromCma {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 Chal] [Finite Chal] [Inhabited Chal] (adv : SourceAdv σ hr M) (simT : Stmt → ProbComp (Commit × Chal × Resp)) : (SourceSigAlg σ hr M).managedRoNmaAdv

The CMA-to-NMA reduction at the managed random-oracle interface.

theorem FiatShamir.Stateful.nmaAdvFromCma_nmaHashQueryBound {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 Chal] [Finite Chal] [Inhabited Chal] (adv : SourceAdv σ hr M) (simT : Stmt → ProbComp (Commit × Chal × Resp)) (qS qH : ℕ) (hQ : ∀ (pk : Stmt), signHashQueryBound M (adv.main pk) qS qH) (pk : Stmt) : nmaHashQueryBound M ((nmaAdvFromCma σ hr M adv simT).main pk) qH

Hash-query bound for nmaAdvFromCma.

noncomputable def FiatShamir.Stateful.nmaAdvFromCmaWithFinalQuery {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 Chal] [Finite Chal] [Inhabited Chal] (adv : SourceAdv σ hr M) (simT : Stmt → ProbComp (Commit × Chal × Resp)) : (SourceSigAlg σ hr M).managedRoNmaAdv

Wrapper around nmaAdvFromCma that issues one explicit live random-oracle query for the forgery's hash point (msg, commit) after the source adversary returns. The extra query makes the verification challenge part of the forkable transcript: Fork.runTrace always sees (msg, commit) in the live queryLog, so the replay-forking lemma can rewind at the verification position without any auxiliary "fresh challenge accepts" assumption on the verifier.

The wrapped adversary issues qH + 1 random-oracle queries (the source's qH plus the appended verifier-point query). The H5 chain calls Fork.advantage on this wrapper at slot parameter qH: Fork.forkPoint qH indexes Fin (qH + 1), which is exactly the right number of slots for qH + 1 queries (the framework's structural +1 is precisely the wrapper's verifier slot). The replay-forking denominator is therefore qH + 1, not qH + 2.

Shifted CMA-to-NMA normal forms

theorem FiatShamir.Stateful.cmaToNma_shiftLeft_signedFreshAdv_eq_bind {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] (adv : SourceAdv σ hr M) (simT : Stmt → ProbComp (Commit × Chal × Resp)) : (cmaToNma M Commit Chal simT).shiftLeft [] (signedFreshAdv σ hr M adv) = do let x ← (simulateQ (cmaToNma M Commit Chal simT) (signedCandidateAdv σ hr M adv)).run [] match x with | (p, log') => Prod.fst <$> (simulateQ (cmaToNma M Commit Chal simT) (verifyFreshComp σ hr M p)).run log'

The stateful shifted form of signedFreshAdv splits at the candidate/verifier boundary, preserving the cmaToNma signing log between the two pieces.

H5 fork-side infrastructure

theorem FiatShamir.Stateful.nma_runProb_shiftLeft_signedFreshAdv_le_fork {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 Chal] [Inhabited Chal] [Finite Chal] (adv : SourceAdv σ hr M) (simT : Stmt → ProbComp (Commit × Chal × Resp)) (qS qH : ℕ) (hQ : ∀ (pk : Stmt), signHashQueryBound M (adv.main pk) qS qH) : Pr[= true | (nma M Commit Chal hr).runProb (nmaInit M Commit Chal Stmt Wit) ((cmaToNma M Commit Chal simT).shiftLeft [] (signedFreshAdv σ hr M adv))] ≤ Fork.advantage σ hr M (nmaAdvFromCmaWithFinalQuery σ hr M adv simT) qH

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).

H3 cost factoring

Top-level chain factored over H5

H4: linked simulation as shifted NMA execution

theorem FiatShamir.Stateful.cmaSim_run_eq_nma_run_shiftLeft_cmaToNma {Stmt Wit Commit Chal Resp : Type} {rel : Stmt → Wit → Bool} (hr : GenerableRelation Stmt Wit rel) (M : Type) [DecidableEq M] [DecidableEq Commit] [SampleableType Chal] (simT : Stmt → ProbComp (Commit × Chal × Resp)) {α : Type} (A : OracleComp (cmaSpec M Commit Chal Resp Stmt) α) : (cmaSim M Commit Chal hr simT).run (cmaInit M Commit Chal Stmt Wit) A = (nma M Commit Chal hr).run (nmaInit M Commit Chal Stmt Wit) ((cmaToNma M Commit Chal simT).shiftLeft [] A)

Native H4 hop: running the linked simulated CMA game from the direct initial state is the same as running the NMA game on the cmaToNma-shifted adversary.

The initial direct CMA state decomposes into the empty signing log for cmaToNma and the initial NMA state for nma.

theorem FiatShamir.Stateful.cmaSim_runProb_eq_nma_runProb_shiftLeft_cmaToNma {Stmt Wit Commit Chal Resp : Type} {rel : Stmt → Wit → Bool} (hr : GenerableRelation Stmt Wit rel) (M : Type) [DecidableEq M] [DecidableEq Commit] [SampleableType Chal] (simT : Stmt → ProbComp (Commit × Chal × Resp)) (A : OracleComp (cmaSpec M Commit Chal Resp Stmt) Bool) : (cmaSim M Commit Chal hr simT).runProb (cmaInit M Commit Chal Stmt Wit) A = (nma M Commit Chal hr).runProb (nmaInit M Commit Chal Stmt Wit) ((cmaToNma M Commit Chal simT).shiftLeft [] A)

Native H4 hop in probability form.

theorem FiatShamir.Stateful.cmaSim_signedFreshAdv_le_fork_of_shifted_h5 {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 Chal] [Finite Chal] [Inhabited Chal] (adv : SourceAdv σ hr M) (simT : Stmt → ProbComp (Commit × Chal × Resp)) (qH : ℕ) (hH5 : Pr[= true | (nma M Commit Chal hr).runProb (nmaInit M Commit Chal Stmt Wit) ((cmaToNma M Commit Chal simT).shiftLeft [] (signedFreshAdv σ hr M adv))] ≤ Fork.advantage σ hr M (nmaAdvFromCmaWithFinalQuery σ hr M adv simT) qH) : Pr[= true | (cmaSim M Commit Chal hr simT).runProb (cmaInit M Commit Chal Stmt Wit) (signedFreshAdv σ hr M adv)] ≤ Fork.advantage σ hr M (nmaAdvFromCmaWithFinalQuery σ hr M adv simT) qH

Convert the shifted-NMA H5 boundary into the linked simulated-CMA form used by the top-level chain.

theorem FiatShamir.Stateful.cmaSim_signedFreshAdv_le_fork {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 Chal] [Inhabited Chal] [Finite Chal] (adv : SourceAdv σ hr M) (simT : Stmt → ProbComp (Commit × Chal × Resp)) (qS qH : ℕ) (hQ : ∀ (pk : Stmt), signHashQueryBound M (adv.main pk) qS qH) : Pr[= true | (cmaSim M Commit Chal hr simT).runProb (cmaInit M Commit Chal Stmt Wit) (signedFreshAdv σ hr M adv)] ≤ Fork.advantage σ hr M (nmaAdvFromCmaWithFinalQuery σ hr M adv simT) qH

Native H5 boundary in the linked simulated-CMA form used by the top-level chain.

theorem FiatShamir.Stateful.cma_advantage_le_fork_bound_of_h5 {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 Chal] [Finite Chal] [Inhabited Chal] (simT : Stmt → ProbComp (Commit × Chal × Resp)) (ζ_zk : ℝ) (hζ_zk : 0 ≤ ζ_zk) (hHVZK : σ.HVZK simT ζ_zk) (β : ENNReal) (hPredSim : σ.simCommitPredictability simT β) (adv : SourceAdv σ hr M) (qS qH : ℕ) (hQ : ∀ (pk : Stmt), signHashQueryBound M (adv.main pk) qS qH) (hH1H2 : SignatureAlg.unforgeableAdv.advantage (runtime M) adv ≤ Pr[= true | (cmaReal M Commit Chal σ hr).runProb (cmaInit M Commit Chal Stmt Wit) (signedFreshAdv σ hr M adv)]) (hH5 : Pr[= true | (cmaSim M Commit Chal hr simT).runProb (cmaInit M Commit Chal Stmt Wit) (signedFreshAdv σ hr M adv)] ≤ Fork.advantage σ hr M (nmaAdvFromCmaWithFinalQuery σ hr M adv simT) qH) : SignatureAlg.unforgeableAdv.advantage (runtime M) adv ≤ Fork.advantage σ hr M (nmaAdvFromCmaWithFinalQuery σ hr M adv simT) qH + ENNReal.ofReal (↑qS * ζ_zk) + ↑qS * (↑qS + ↑qH) * β

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.

theorem FiatShamir.Stateful.cma_advantage_le_fork_bound_of_h1h2 {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 Chal] [Finite Chal] [Inhabited Chal] (simT : Stmt → ProbComp (Commit × Chal × Resp)) (ζ_zk : ℝ) (hζ_zk : 0 ≤ ζ_zk) (hHVZK : σ.HVZK simT ζ_zk) (β : ENNReal) (hPredSim : σ.simCommitPredictability simT β) (adv : SourceAdv σ hr M) (qS qH : ℕ) (hQ : ∀ (pk : Stmt), signHashQueryBound M (adv.main pk) qS qH) (hH1H2 : SignatureAlg.unforgeableAdv.advantage (runtime M) adv ≤ Pr[= true | (cmaReal M Commit Chal σ hr).runProb (cmaInit M Commit Chal Stmt Wit) (signedFreshAdv σ hr M adv)]) : SignatureAlg.unforgeableAdv.advantage (runtime M) adv ≤ Fork.advantage σ hr M (nmaAdvFromCmaWithFinalQuery σ hr M adv simT) qH + ENNReal.ofReal (↑qS * ζ_zk) + ↑qS * (↑qS + ↑qH) * β

Native stateful chain with H5 discharged by the replay-forking boundary, leaving only the public-to-stateful H1/H2 compatibility premise.