Native stateful Fiat-Shamir CMA game hops

The theorems here are stated directly over QueryImpl.Stateful handlers and the concrete CmaState product state.

H3 state invariants and per-query loss

@[reducible]

def FiatShamir.Stateful.cmaDataInit (M Commit Chal Stmt Wit : Type) : CmaData M Commit Chal Stmt Wit

Initial direct CMA data, without the trailing bad flag.

@[simp]

theorem FiatShamir.Stateful.cmaInit_eq_cmaDataInit (M Commit Chal : Type) {Stmt Wit : Type} : cmaInit M Commit Chal Stmt Wit = (cmaDataInit M Commit Chal Stmt Wit, false)

The direct CMA initial state is the initial data with bad unset.

def FiatShamir.Stateful.CmaData.Valid {M Commit Chal Stmt Wit : Type} {rel : Stmt → Wit → Bool} (s : CmaData M Commit Chal Stmt Wit) : Prop

Reachability invariant for the direct CMA data.

Cached keypairs, when present, must satisfy the relation generated by hr.gen. The invariant is intentionally phrased on CmaData, not heap cells.

@[implicit_reducible]

instance FiatShamir.Stateful.instDecidableValid {M Commit Chal Stmt Wit : Type} {rel : Stmt → Wit → Bool} (s : CmaData M Commit Chal Stmt Wit) : Decidable s.Valid

theorem FiatShamir.Stateful.cmaDataInit_valid (M Commit Chal : Type) {Stmt Wit : Type} {rel : Stmt → Wit → Bool} : (cmaDataInit M Commit Chal Stmt Wit).Valid

The initial direct CMA data has no cached keypair, hence satisfies the valid-keypair invariant.

noncomputable def FiatShamir.Stateful.cmaSignEpsCore (M Commit Chal : Type) {Stmt Wit : Type} (ζ_zk β : ENNReal) (s : CmaData M Commit Chal Stmt Wit) : ENNReal

Tight state-dependent per-signing-query loss for H3 on reachable states.

noncomputable def FiatShamir.Stateful.cmaSignEps (M Commit Chal : Type) {Stmt Wit : Type} {rel : Stmt → Wit → Bool} (ζ_zk β : ENNReal) (s : CmaData M Commit Chal Stmt Wit) : ENNReal

State-dependent per-signing-query loss for H3.

On reachable states this is ζ_zk + QueryCache.enncard · β. Invalid keypair states receive the conservative fallback cost 1, which is useful for ungated identical-until-bad statements.

H3 proof obligations

@[reducible, inline]

abbrev FiatShamir.Stateful.cmaH3Costly (M Commit Chal : Type) {Stmt Resp : Type} : (cmaSpec M Commit Chal Resp Stmt).Domain → Prop

Signing queries are the charged queries in the H3 hop.

@[reducible, inline]

noncomputable abbrev FiatShamir.Stateful.cmaH3Advantage (M : Type) [DecidableEq M] (Commit : Type) [DecidableEq Commit] (Chal : Type) [SampleableType Chal] {Stmt Wit : Type} {rel : Stmt → Wit → Bool} {Resp PrvState : Type} (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel) (hr : GenerableRelation Stmt Wit rel) (simT : Stmt → ProbComp (Commit × Chal × Resp)) (A : OracleComp (cmaSpec M Commit Chal Resp Stmt) Bool) : ℝ

Boolean distinguishing advantage for the native H3 pair from the direct initial CMA state.

@[reducible, inline]

noncomputable abbrev FiatShamir.Stateful.cmaH3ExpectedLoss (M : Type) [DecidableEq M] (Commit : Type) [DecidableEq Commit] (Chal : Type) [SampleableType Chal] {Stmt Wit : Type} {rel : Stmt → Wit → Bool} {Resp PrvState : Type} (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel) (hr : GenerableRelation Stmt Wit rel) (ζ_zk β : ENNReal) {α : Type} (A : OracleComp (cmaSpec M Commit Chal Resp Stmt) α) (qS : ℕ) : ENNReal

Expected accumulated H3 signing loss in the real game.

structure FiatShamir.Stateful.CmaH3StepFacts (M : Type) [DecidableEq M] (Commit : Type) [DecidableEq Commit] (Chal : Type) [SampleableType Chal] {Stmt Wit : Type} {rel : Stmt → Wit → Bool} {Resp PrvState : Type} (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel) (hr : GenerableRelation Stmt Wit rel) (simT : Stmt → ProbComp (Commit × Chal × Resp)) (ζ_zk β : ENNReal) : Prop

Per-query facts for the native H3 hop.

• preservesValid : (cmaReal M Commit Chal σ hr).PreservesNoBadInvariant CmaData.Valid

  The real game preserves keypair validity while bad is false.

• stepTvCostly (t : (cmaSpec M Commit Chal Resp Stmt).Domain) : cmaH3Costly M Commit Chal t → ∀ (s : CmaData M Commit Chal Stmt Wit), s.Valid → ENNReal.ofReal (tvDist ((cmaReal M Commit Chal σ hr t).run (s, false)) ((cmaSim M Commit Chal hr simT t).run (s, false))) ≤ cmaSignEpsCore M Commit Chal ζ_zk β s

  Signing queries are close by the state-dependent H3 loss.

• stepEqFree (t : (cmaSpec M Commit Chal Resp Stmt).Domain) : ¬cmaH3Costly M Commit Chal t → ∀ (p : CmaState M Commit Chal Stmt Wit), (cmaReal M Commit Chal σ hr t).run p = (cmaSim M Commit Chal hr simT t).run p

  Non-signing queries agree pointwise.

• badMono (t : (cmaSpec M Commit Chal Resp Stmt).Domain) (p : CmaState M Commit Chal Stmt Wit) : p.2 = true → ∀ z ∈ support ((cmaReal M Commit Chal σ hr t).run p), z.2.2 = true

  Once the real bad flag is true, it stays true.

structure FiatShamir.Stateful.CmaH3RunFacts (M : Type) [DecidableEq M] (Commit : Type) [DecidableEq Commit] (Chal : Type) [SampleableType Chal] {Stmt Wit : Type} {rel : Stmt → Wit → Bool} {Resp PrvState : Type} (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel) (hr : GenerableRelation Stmt Wit rel) (ζ_zk β : ENNReal) (A : OracleComp (cmaSpec M Commit Chal Resp Stmt) Bool) (qS : ℕ) (εBound : ENNReal) : Prop

Computation-specific facts for applying the native H3 hop.

• queryBound : A.IsQueryBoundP (cmaH3Costly M Commit Chal) qS

  The adversary issues at most qS signing queries.

• badZero : (probEvent ((simulateQ (cmaReal M Commit Chal σ hr) A).run (cmaInit M Commit Chal Stmt Wit)) fun (z : Bool × CmaState M Commit Chal Stmt Wit) => z.2.2 = true) = 0

  The real game never reaches bad from the initial state.

• expectedLossLe : cmaH3ExpectedLoss M Commit Chal σ hr ζ_zk β A qS ≤ εBound

  The expected accumulated signing loss is at most the requested bound.

Real-game bad flag facts

theorem FiatShamir.Stateful.simulateQ_bad_preserved_of_step {ι ι' : Type} {spec : OracleSpec ι} {spec' : OracleSpec ι'} {σ α : Type} (impl : QueryImpl spec (StateT (σ × Bool) (OracleComp spec'))) (hstep : ∀ (t : spec.Domain) (p : σ × Bool), ∀ z ∈ support ((impl t).run p), z.2.2 = p.2) (oa : OracleComp spec α) (p : σ × Bool) {z : α × σ × Bool} (hz : z ∈ support ((simulateQ impl oa).run p)) : z.2.2 = p.2

Stepwise preservation of a trailing Boolean flag lifts through simulateQ.

theorem FiatShamir.Stateful.cmaReal_bad_preserved (M : Type) [DecidableEq M] (Commit : Type) [DecidableEq Commit] (Chal : Type) [SampleableType Chal] {Stmt Wit : Type} {rel : Stmt → Wit → Bool} {Resp PrvState : Type} (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel) (hr : GenerableRelation Stmt Wit rel) (t : (cmaSpec M Commit Chal Resp Stmt).Domain) (p : CmaState M Commit Chal Stmt Wit) (z : (cmaSpec M Commit Chal Resp Stmt).Range t × CmaState M Commit Chal Stmt Wit) (hz : z ∈ support ((cmaReal M Commit Chal σ hr t).run p)) : z.2.2 = p.2

One step of the real CMA game preserves the bad flag exactly.

theorem FiatShamir.Stateful.cmaReal_bad_mono (M : Type) [DecidableEq M] (Commit : Type) [DecidableEq Commit] (Chal : Type) [SampleableType Chal] {Stmt Wit : Type} {rel : Stmt → Wit → Bool} {Resp PrvState : Type} (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel) (hr : GenerableRelation Stmt Wit rel) (t : (cmaSpec M Commit Chal Resp Stmt).Domain) (p : CmaState M Commit Chal Stmt Wit) : p.2 = true → ∀ z ∈ support ((cmaReal M Commit Chal σ hr t).run p), z.2.2 = true

Once the real CMA bad flag is true, one real step keeps it true.

theorem FiatShamir.Stateful.cmaReal_probEvent_bad_eq_zero (M : Type) [DecidableEq M] (Commit : Type) [DecidableEq Commit] (Chal : Type) [SampleableType Chal] {Stmt Wit : Type} {rel : Stmt → Wit → Bool} {Resp PrvState : Type} (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel) (hr : GenerableRelation Stmt Wit rel) {α : Type} (A : OracleComp (cmaSpec M Commit Chal Resp Stmt) α) : (probEvent ((simulateQ (cmaReal M Commit Chal σ hr) A).run (cmaInit M Commit Chal Stmt Wit)) fun (z : α × CmaState M Commit Chal Stmt Wit) => z.2.2 = true) = 0

The real CMA game never reaches bad from the initial state.

theorem FiatShamir.Stateful.cmaReal_valid_preserved (M : Type) [DecidableEq M] (Commit : Type) [DecidableEq Commit] (Chal : Type) [SampleableType Chal] {Stmt Wit : Type} {rel : Stmt → Wit → Bool} {Resp PrvState : Type} (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel) (hr : GenerableRelation Stmt Wit rel) (t : (cmaSpec M Commit Chal Resp Stmt).Domain) (p : CmaState M Commit Chal Stmt Wit) (hpvalid : p.1.Valid) (z : (cmaSpec M Commit Chal Resp Stmt).Range t × CmaState M Commit Chal Stmt Wit) (hz : z ∈ support ((cmaReal M Commit Chal σ hr t).run p)) : z.2.1.Valid

One real CMA step preserves keypair validity.

theorem FiatShamir.Stateful.cmaReal_preserves_valid (M : Type) [DecidableEq M] (Commit : Type) [DecidableEq Commit] (Chal : Type) [SampleableType Chal] {Stmt Wit : Type} {rel : Stmt → Wit → Bool} {Resp PrvState : Type} (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel) (hr : GenerableRelation Stmt Wit rel) : (cmaReal M Commit Chal σ hr).PreservesNoBadInvariant CmaData.Valid

The real CMA handler preserves keypair validity while bad is false.

theorem FiatShamir.Stateful.cmaReal_roCacheCount_step_le (M : Type) [DecidableEq M] (Commit : Type) [DecidableEq Commit] (Chal : Type) [SampleableType Chal] {Stmt Wit : Type} {rel : Stmt → Wit → Bool} {Resp PrvState : Type} (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel) (hr : GenerableRelation Stmt Wit rel) (t : (cmaSpec M Commit Chal Resp Stmt).Domain) (p : CmaState M Commit Chal Stmt Wit) (z : (cmaSpec M Commit Chal Resp Stmt).Range t × CmaState M Commit Chal Stmt Wit) (hz : z ∈ support ((cmaReal M Commit Chal σ hr t).run p)) : OracleSpec.QueryCache.enncard z.2.1.2.1 ≤ OracleSpec.QueryCache.enncard p.1.2.1 + if cmaH3Costly M Commit Chal t ∨ IsHashQuery M t then 1 else 0

One real CMA step grows the direct random-oracle cache by at most one on signing or hash queries, and does not grow it on other queries.

theorem FiatShamir.Stateful.cmaH3ExpectedLoss_le_queryBounds (M : Type) [DecidableEq M] (Commit : Type) [DecidableEq Commit] (Chal : Type) [SampleableType Chal] {Stmt Wit : Type} {rel : Stmt → Wit → Bool} {Resp PrvState : Type} (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel) (hr : GenerableRelation Stmt Wit rel) (ζ_zk β : ENNReal) {α : Type} (A : OracleComp (cmaSpec M Commit Chal Resp Stmt) α) {qS qH : ℕ} (h_qS : A.IsQueryBoundP (cmaH3Costly M Commit Chal) qS) (h_qH : A.IsQueryBoundP (IsHashQuery M) qH) : cmaH3ExpectedLoss M Commit Chal σ hr ζ_zk β A qS ≤ ↑qS * ζ_zk + ↑qS * (↑qS + ↑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.

theorem FiatShamir.Stateful.cmaH3RunFacts_of_queryBound_expectedLoss (M : Type) [DecidableEq M] (Commit : Type) [DecidableEq Commit] (Chal : Type) [SampleableType Chal] {Stmt Wit : Type} {rel : Stmt → Wit → Bool} {Resp PrvState : Type} (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel) (hr : GenerableRelation Stmt Wit rel) (ζ_zk β : ENNReal) (A : OracleComp (cmaSpec M Commit Chal Resp Stmt) Bool) (qS : ℕ) (εBound : ENNReal) (h_queryBound : A.IsQueryBoundP (cmaH3Costly M Commit Chal) qS) (h_expectedLoss : cmaH3ExpectedLoss M Commit Chal σ hr ζ_zk β A qS ≤ εBound) : CmaH3RunFacts M Commit Chal σ hr ζ_zk β A qS εBound

Build the native H3 run facts from the query bound and expected-loss bound.

Non-signing step equality

theorem FiatShamir.Stateful.cmaReal_eq_cmaSim_of_not_costly (M : Type) [DecidableEq M] (Commit : Type) [DecidableEq Commit] (Chal : Type) [SampleableType Chal] {Stmt Wit : Type} {rel : Stmt → Wit → Bool} {Resp PrvState : Type} (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel) (hr : GenerableRelation Stmt Wit rel) (simT : Stmt → ProbComp (Commit × Chal × Resp)) (t : (cmaSpec M Commit Chal Resp Stmt).Domain) (ht : ¬cmaH3Costly M Commit Chal t) (p : CmaState M Commit Chal Stmt Wit) : (cmaReal M Commit Chal σ hr t).run p = (cmaSim M Commit Chal hr simT t).run p

The real and simulated CMA handlers agree on every non-signing query.

Native signing-step TV ingredients

theorem FiatShamir.Stateful.cmaReal_cmaSim_tv_sign_le_cmaSignEpsCore_of_valid (M : Type) [DecidableEq M] (Commit : Type) [DecidableEq Commit] (Chal : Type) [SampleableType Chal] {Stmt Wit : Type} {rel : Stmt → Wit → Bool} {Resp PrvState : Type} (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel) (hr : GenerableRelation Stmt Wit rel) (simT : Stmt → ProbComp (Commit × Chal × Resp)) (ζ_zk β : ENNReal) (hζ_zk : ζ_zk < ⊤) (hHVZK : σ.HVZK simT ζ_zk.toReal) (hCommit : σ.simCommitPredictability simT β) (m : M) (s : CmaData M Commit Chal Stmt Wit) (hvalid : s.Valid) : ENNReal.ofReal (tvDist ((cmaReal M Commit Chal σ hr (CmaQuery.sign m)).run (s, false)) ((cmaSim M Commit Chal hr simT (CmaQuery.sign m)).run (s, false))) ≤ cmaSignEpsCore M Commit Chal ζ_zk β s

theorem FiatShamir.Stateful.cmaReal_cmaSim_tv_costly_le_cmaSignEpsCore_of_valid (M : Type) [DecidableEq M] (Commit : Type) [DecidableEq Commit] (Chal : Type) [SampleableType Chal] {Stmt Wit : Type} {rel : Stmt → Wit → Bool} {Resp PrvState : Type} (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel) (hr : GenerableRelation Stmt Wit rel) (simT : Stmt → ProbComp (Commit × Chal × Resp)) (ζ_zk β : ENNReal) (hζ_zk : ζ_zk < ⊤) (hHVZK : σ.HVZK simT ζ_zk.toReal) (hCommit : σ.simCommitPredictability simT β) (t : (cmaSpec M Commit Chal Resp Stmt).Domain) (ht : cmaH3Costly M Commit Chal t) (s : CmaData M Commit Chal Stmt Wit) (hvalid : s.Valid) : ENNReal.ofReal (tvDist ((cmaReal M Commit Chal σ hr t).run (s, false)) ((cmaSim M Commit Chal hr simT t).run (s, false))) ≤ cmaSignEpsCore M Commit Chal ζ_zk β s

theorem FiatShamir.Stateful.cmaH3StepFacts_of_hvzk_predictability (M : Type) [DecidableEq M] (Commit : Type) [DecidableEq Commit] (Chal : Type) [SampleableType Chal] {Stmt Wit : Type} {rel : Stmt → Wit → Bool} {Resp PrvState : Type} (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel) (hr : GenerableRelation Stmt Wit rel) (simT : Stmt → ProbComp (Commit × Chal × Resp)) (ζ_zk β : ENNReal) (hζ_zk : ζ_zk < ⊤) (hHVZK : σ.HVZK simT ζ_zk.toReal) (hCommit : σ.simCommitPredictability simT β) : CmaH3StepFacts M Commit Chal σ hr simT ζ_zk β

Build the native H3 step facts from HVZK and simulator commit predictability.

Native H3 factoring theorem

theorem FiatShamir.Stateful.cmaReal_cmaSim_advantage_le_H3_bound_of_expectedQuerySlack (M : Type) [DecidableEq M] (Commit : Type) [DecidableEq Commit] (Chal : Type) [SampleableType Chal] {Stmt Wit : Type} {rel : Stmt → Wit → Bool} {Resp PrvState : Type} (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel) (hr : GenerableRelation Stmt Wit rel) (simT : Stmt → ProbComp (Commit × Chal × Resp)) (ζ_zk β : ENNReal) (A : OracleComp (cmaSpec M Commit Chal Resp Stmt) Bool) (qS : ℕ) (εBound : ENNReal) (stepFacts : CmaH3StepFacts M Commit Chal σ hr simT ζ_zk β) (runFacts : CmaH3RunFacts M Commit Chal σ hr ζ_zk β A qS εBound) : ENNReal.ofReal (cmaH3Advantage M Commit Chal σ hr simT A) ≤ εBound

Native H3 bridge with caller-supplied expected-cost bound.

This is the direct QueryImpl.Stateful replacement for the old H3 identical-until-bad instantiation. The hypotheses are factored into per-query step facts and computation-specific run facts; no heap package or state projection appears in the statement.

theorem FiatShamir.Stateful.cmaReal_cmaSim_advantage_le_H3_bound (M : Type) [DecidableEq M] (Commit : Type) [DecidableEq Commit] (Chal : Type) [SampleableType Chal] {Stmt Wit : Type} {rel : Stmt → Wit → Bool} {Resp PrvState : Type} (σ : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel) (hr : GenerableRelation Stmt Wit rel) (simT : Stmt → ProbComp (Commit × Chal × Resp)) (ζ_zk β : ENNReal) (hζ_zk : ζ_zk < ⊤) (hHVZK : σ.HVZK simT ζ_zk.toReal) (hCommit : σ.simCommitPredictability simT β) (A : OracleComp (cmaSpec M Commit Chal Resp Stmt) Bool) {qS qH : ℕ} (h_qS : A.IsQueryBoundP (cmaH3Costly M Commit Chal) qS) (h_qH : A.IsQueryBoundP (IsHashQuery M) qH) : ENNReal.ofReal (cmaH3Advantage M Commit Chal σ hr simT A) ≤ ↑qS * ζ_zk + ↑qS * (↑qS + ↑qH) * β

Fully assembled native H3 bound from HVZK, simulator commit predictability, and adversary signing/hash query budgets.