Compatibility endpoints for the stateful Fiat-Shamir CMA proof

The main stateful proof path uses the full CmaState game definitions from Stateful.Games and the full-state post-keygen normal form in Stateful.Bridge.

The generic SignatureAlg.unforgeableExp experiment is still a useful public API, but it interprets signing queries through a WriterT query log. Any theorem equating that legacy public experiment with the full-state CMA game necessarily relates two interpreters. Such theorems belong here, not in the main stateful bridge.

Public and stateful endpoints

noncomputable def FiatShamir.Stateful.publicUnforgeableAdvantage {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) [SampleableType Chal] (adv : SourceAdv σ hr M) : ENNReal

The legacy public EUF-CMA advantage exposed by SignatureAlg.

This endpoint uses SignatureAlg.unforgeableExp, which logs signing queries via WriterT. It is kept separate from the full-state stateful proof path.

noncomputable def FiatShamir.Stateful.statefulPostKeygenFreshAdvantage {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] (adv : SourceAdv σ hr M) : ENNReal

The full-state post-keygen CMA advantage used by the stateful proof path.

This is the key-generation wrapper around postKeygenFreshProb; the fixed-key body runs through cmaRealSourceFullSum on CmaState.

noncomputable def FiatShamir.Stateful.statefulCmaFreshExperiment {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] (adv : SourceAdv σ hr M) : ProbComp Bool

The full-state CMA run as a Boolean freshness experiment.

This packages cmaRealRun with the same final freshness predicate as the post-keygen normal form.

noncomputable def FiatShamir.Stateful.statefulCmaFreshAdvantage {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] (adv : SourceAdv σ hr M) : ENNReal

The full-state CMA advantage obtained directly from cmaRealRun.

This endpoint is equivalent to statefulPostKeygenFreshAdvantage by unfolding the public-key query in signedAdv; the equality is a stateful-game normal-form fact and does not mention SignatureAlg.unforgeableExp.

Compatibility boundary

def FiatShamir.Stateful.PublicCompatible {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] (adv : SourceAdv σ hr M) : Prop

Compatibility proposition between the legacy public experiment and the full-state stateful experiment.

The main stateful proof path should assume or prove facts about statefulCmaFreshAdvantage. If a caller needs the historical SignatureAlg.unforgeableAdv.advantage API, the required normalization theorem should target this proposition in this quarantined module.

theorem FiatShamir.Stateful.statefulCmaFreshAdvantage_eq_statefulPostKeygenFreshAdvantage {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] (adv : SourceAdv σ hr M) : statefulCmaFreshAdvantage σ hr M adv = statefulPostKeygenFreshAdvantage σ hr M adv

The direct cmaRealRun endpoint and the fixed-key post-keygen endpoint are the same full-state freshness experiment.

Public WriterT compatibility

theorem FiatShamir.Stateful.statefulPostKeygenFreshAdvantage_eq_cmaRealRunProb_signedFreshAdv {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] (adv : SourceAdv σ hr M) : statefulPostKeygenFreshAdvantage σ hr M adv = Pr[= true | (cmaReal M Commit Chal σ hr).runProb (cmaInit M Commit Chal Stmt Wit) (signedFreshAdv σ hr M adv)]

The post-keygen freshness endpoint is the same Boolean experiment as running signedFreshAdv in the direct stateful CMA game.

theorem FiatShamir.Stateful.publicUnforgeableAdvantage_eq_statefulPostKeygenFreshAdvantage {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] (adv : SourceAdv σ hr M) : publicUnforgeableAdvantage σ hr M adv = statefulPostKeygenFreshAdvantage σ hr M adv

Public EUF-CMA advantage in the shared fixed-key post-keygen normal form.

theorem FiatShamir.Stateful.publicCompatible {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] (adv : SourceAdv σ hr M) : PublicCompatible σ hr M adv

Public compatibility for the legacy SignatureAlg endpoint.

theorem FiatShamir.Stateful.publicUnforgeableAdvantage_le_statefulCmaFresh {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] (adv : SourceAdv σ hr M) (hCompat : PublicCompatible σ hr M adv) : SignatureAlg.unforgeableAdv.advantage (runtime M) adv ≤ statefulCmaFreshAdvantage σ hr M adv

Public compatibility, in inequality form, against the direct stateful freshness experiment.