Bridge helpers for the stateful Fiat-Shamir CMA games

This file contains the adversary wrappers and query-bound bookkeeping that connect the public SignatureAlg.unforgeableAdv interface to the direct QueryImpl.Stateful CMA games.

Local type abbreviations

@[reducible, inline]

abbrev FiatShamir.Stateful.SourceSigAlg {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) : SignatureAlg (OracleComp (unifSpec + OracleSpec.ofFn fun (x : M × Commit) => Chal)) M Stmt Wit (Commit × Resp)

Fiat-Shamir signature scheme over the public random-oracle interface used by the source CMA adversary.

@[reducible, inline]

abbrev FiatShamir.Stateful.SourceAdv {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) : Type

Source EUF-CMA adversary type for the Fiat-Shamir signature scheme.

@[reducible, inline]

abbrev FiatShamir.Stateful.SourceCmaSpec {Commit Chal Resp : Type} (M : Type) : OracleSpec ((ℕ ⊕ M × Commit) ⊕ M)

Source post-keygen CMA oracle interface: public Fiat-Shamir queries plus signing queries.

@[reducible, inline]

abbrev FiatShamir.Stateful.SourceCmaComp {Commit Chal Resp : Type} (M α : Type) : Type

Computations over the source post-keygen CMA oracle interface.

Adversary wrappers

@[reducible]

noncomputable def FiatShamir.Stateful.postKeygenCandidateAdv {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) (adv : SourceAdv σ hr M) (pk : Stmt) : OracleComp (cmaSpec M Commit Chal Resp Stmt) (M × Commit × Resp)

Candidate-producing part of the CMA adversary after the public key is fixed.

@[reducible]

noncomputable def FiatShamir.Stateful.candidateAdv {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) (adv : SourceAdv σ hr M) : OracleComp (cmaSpec M Commit Chal Resp Stmt) (Stmt × M × Commit × Resp)

Candidate-producing adversary with the public key fetched from the game.

@[reducible]

noncomputable def FiatShamir.Stateful.signedAdv {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) (adv : SourceAdv σ hr M) : OracleComp (cmaSpec M Commit Chal Resp Stmt) ((M × Commit × Resp) × Bool)

Lift a CMA-style Fiat-Shamir adversary into the named CMA game interface.

@[reducible]

noncomputable def FiatShamir.Stateful.cmaSignLogImpl {Stmt Commit Chal Resp : Type} (M : Type) : QueryImpl (cmaSpec M Commit Chal Resp Stmt) (StateT (List M) (OracleComp (cmaSpec M Commit Chal Resp Stmt)))

Log signing queries while forwarding every query to the surrounding CMA interface.

@[reducible]

noncomputable def FiatShamir.Stateful.signedCandidateAdv {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) (adv : SourceAdv σ hr M) : OracleComp (cmaSpec M Commit Chal Resp Stmt) ((Stmt × M × Commit × Resp) × List M)

Log signing queries while producing the final candidate, before verification.

@[reducible]

noncomputable def FiatShamir.Stateful.verifyFreshComp {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] (p : (Stmt × M × Commit × Resp) × List M) : OracleComp (cmaSpec M Commit Chal Resp Stmt) Bool

Freshness and verification check attached after candidate production.

@[reducible]

noncomputable def FiatShamir.Stateful.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] (adv : SourceAdv σ hr M) : OracleComp (cmaSpec M Commit Chal Resp Stmt) Bool

Freshness-preserving Boolean adversary for the direct stateful CMA chain.

Fixed-key post-keygen runtime

noncomputable def FiatShamir.Stateful.postKeygenAdvBase {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) (adv : SourceAdv σ hr M) (pk : Stmt) : SourceCmaComp M ((M × Commit × Resp) × Bool)

The public post-keygen adversary/verification computation before it is interpreted by the explicit random-oracle cache runtime.

noncomputable def FiatShamir.Stateful.postVerifyComp {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) (pk : Stmt) (x : M × Commit × Resp) : OracleComp (cmaSpec M Commit Chal Resp Stmt) ((M × Commit × Resp) × Bool)

Verification suffix attached after the fixed-key adversary produces a candidate.

noncomputable def FiatShamir.Stateful.postKeygenAdv {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) (adv : SourceAdv σ hr M) (pk : Stmt) : OracleComp (cmaSpec M Commit Chal Resp Stmt) ((M × Commit × Resp) × Bool)

Fixed-key adversary and verification computation over the named CMA interface.

theorem FiatShamir.Stateful.runtimeWithCache_evalDist_eq_fsBaseImpl {Commit Chal : Type} (M : Type) [DecidableEq M] [DecidableEq Commit] [SampleableType Chal] (cache : (OracleSpec.ofFn fun (x : M × Commit) => Chal).QueryCache) {α : Type} (oa : OracleComp (unifSpec + OracleSpec.ofFn fun (x : M × Commit) => Chal) α) : (runtimeWithCache M cache).evalDist oa = 𝒟[(simulateQ (fsBaseImpl M Commit Chal) oa).run' cache]

The Fiat-Shamir runtime-with-cache semantics is the explicit cache-state implementation fsBaseImpl, observed from the chosen initial cache.

Fixed-key post-keygen probability normal form

noncomputable def FiatShamir.Stateful.postKeygenFreshProb {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) (pk : Stmt) (sk : Wit) : ProbComp Bool

Fixed-key post-keygen experiment in the full direct CMA state.

The keypair is installed before the adversary runs, and the final freshness check reads the signed-message log from the resulting CmaState. This is the canonical normal form used by the stateful CMA chain.

Joint output of cmaReal

noncomputable def FiatShamir.Stateful.cmaRealRun {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 ((M × Commit × Resp) × Bool × List M)

Run the direct stateful cmaReal game against signedAdv and pack the forgery, verification bit, and signed-message log into one probability computation.

theorem FiatShamir.Stateful.cmaRealRun_eq_keygen_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] [DecidableEq Commit] [SampleableType Chal] (adv : SourceAdv σ hr M) : cmaRealRun σ hr M adv = do let ps ← hr.gen let p ← (cmaReal M Commit Chal σ hr).runState (([], ∅, some (ps.1, ps.2)), false) (postKeygenAdv σ hr M adv ps.1) pure (p.1.1, p.1.2, p.2.1.1)

The initial public-key query in signedAdv factors cmaRealRun through the key generator and a fixed-key post-keygen run.

Joint signing/hash query bounds

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

A named CMA query is costly for H3 exactly when it targets the signing oracle.

@[implicit_reducible]

instance FiatShamir.Stateful.instDecidablePredDomainCmaQueryCmaSpecIsCostlyQuery {Stmt Commit Chal Resp : Type} (M : Type) : DecidablePred (IsCostlyQuery M)

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

A named CMA query is a hash query exactly when it targets the random oracle.

@[implicit_reducible]

instance FiatShamir.Stateful.instDecidablePredDomainCmaQueryCmaSpecIsHashQuery {Stmt Commit Chal Resp : Type} (M : Type) : DecidablePred (IsHashQuery M)

def FiatShamir.Stateful.cmaSignHashQueryBound {Stmt Commit Chal Resp : Type} (M : Type) {α : Type} (oa : OracleComp (cmaSpec M Commit Chal Resp Stmt) α) (qS qH : ℕ) : Prop

Joint signing/hash query bound for computations over the named CMA interface.

theorem FiatShamir.Stateful.cmaSignLogImpl_cmaSignHashQueryBound {Stmt Commit Chal Resp : Type} (M : Type) {α : Type} (A : OracleComp (cmaSpec M Commit Chal Resp Stmt) α) (signed : List M) (qS qH : ℕ) (hA : cmaSignHashQueryBound M A qS qH) : cmaSignHashQueryBound M ((simulateQ (cmaSignLogImpl M) A).run signed) qS qH

Logging signing inputs while forwarding all queries preserves the joint signing/hash query bound.

theorem FiatShamir.Stateful.signedCandidateAdv_cmaSignHashQueryBound {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) (adv : SourceAdv σ hr M) (qS qH : ℕ) (hQ : ∀ (pk : Stmt), signHashQueryBound M (adv.main pk) qS qH) : cmaSignHashQueryBound M (signedCandidateAdv σ hr M adv) qS qH

Candidate production, with signing queries logged before final verification, preserves the source adversary signing/hash query budget.

theorem FiatShamir.Stateful.signedFreshAdv_cmaSignHashQueryBound {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) (qS qH : ℕ) (hQ : ∀ (pk : Stmt), signHashQueryBound M (adv.main pk) qS qH) : cmaSignHashQueryBound M (signedFreshAdv σ hr M adv) qS (qH + 1)

The final freshness-preserving Boolean adversary is bounded by the source adversary budget plus one verifier hash query.

theorem FiatShamir.Stateful.signedFreshAdv_isQueryBoundP_costly {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) (qS qH : ℕ) (hQ : ∀ (pk : Stmt), signHashQueryBound M (adv.main pk) qS qH) : (signedFreshAdv σ hr M adv).IsQueryBoundP (IsCostlyQuery M) qS

Predicate-targeted signing-query bound for the final freshness-preserving CMA adversary.

theorem FiatShamir.Stateful.signedCandidateAdv_isQueryBoundP_costly {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) (adv : SourceAdv σ hr M) (qS qH : ℕ) (hQ : ∀ (pk : Stmt), signHashQueryBound M (adv.main pk) qS qH) : (signedCandidateAdv σ hr M adv).IsQueryBoundP (IsCostlyQuery M) qS

Predicate-targeted signing-query bound for candidate production before the final verification suffix.

theorem FiatShamir.Stateful.signedCandidateAdv_isQueryBoundP_hash {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) (adv : SourceAdv σ hr M) (qS qH : ℕ) (hQ : ∀ (pk : Stmt), signHashQueryBound M (adv.main pk) qS qH) : (signedCandidateAdv σ hr M adv).IsQueryBoundP (IsHashQuery M) qH

Predicate-targeted hash-query bound for candidate production before the final verification suffix.

theorem FiatShamir.Stateful.signedFreshAdv_isQueryBoundP_hash {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) (qS qH : ℕ) (hQ : ∀ (pk : Stmt), signHashQueryBound M (adv.main pk) qS qH) : (signedFreshAdv σ hr M adv).IsQueryBoundP (IsHashQuery M) (qH + 1)

Predicate-targeted hash-query bound for the final freshness-preserving CMA adversary. The extra query is the final Fiat-Shamir verification.