Oracle interfaces and plain states for the stateful Fiat-Shamir CMA proof

This file contains the oracle interfaces and direct product-state shapes used by the QueryImpl.Stateful Fiat-Shamir CMA games. The games store their private data in ordinary product types.

The fs_simp simp attribute used to tag handler definitions, frames, lenses, and adversary wrappers throughout the stateful FS-CMA development is declared in Stateful/SimpAttr.lean and imported above.

Oracle specs

inductive FiatShamir.Stateful.CmaSourceQuery (M Commit : Type) : Type

Named query constructors for the source CMA adversary interface.

• unif {M Commit : Type} (n : ℕ) : CmaSourceQuery M Commit

  Uniform sampling query.

• ro {M Commit : Type} (mc : M × Commit) : CmaSourceQuery M Commit

  Random-oracle query.

• sign {M Commit : Type} (m : M) : CmaSourceQuery M Commit

  Signing query.

inductive FiatShamir.Stateful.CmaQuery (M Commit : Type) : Type

Named query constructors for the CMA adversary's oracle view.

• unif {M Commit : Type} (n : ℕ) : CmaQuery M Commit

  Uniform sampling query.

• ro {M Commit : Type} (mc : M × Commit) : CmaQuery M Commit

  Random-oracle query.

• sign {M Commit : Type} (m : M) : CmaQuery M Commit

  Signing query.

• pk {M Commit : Type} : CmaQuery M Commit

  Public-key query.

inductive FiatShamir.Stateful.CmaPublicQuery (M Commit : Type) : Type

Named query constructors for the public, non-signing portion of the CMA interface.

• unif {M Commit : Type} (n : ℕ) : CmaPublicQuery M Commit

  Uniform sampling query.

• ro {M Commit : Type} (mc : M × Commit) : CmaPublicQuery M Commit

  Random-oracle query.

• pk {M Commit : Type} : CmaPublicQuery M Commit

  Public-key query.

inductive FiatShamir.Stateful.NmaQuery (M Commit Chal : Type) : Type

Named query constructors for the NMA interface used internally by the CMA-to-NMA reduction.

• unif {M Commit Chal : Type} (n : ℕ) : NmaQuery M Commit Chal

  Uniform sampling query.

• ro {M Commit Chal : Type} (mc : M × Commit) : NmaQuery M Commit Chal

  Random-oracle query.

• pk {M Commit Chal : Type} : NmaQuery M Commit Chal

  Public-key query.

• prog {M Commit Chal : Type} (mch : M × Commit × Chal) : NmaQuery M Commit Chal

  Programmable-random-oracle query.

@[reducible]

def FiatShamir.Stateful.roSpec (M Commit Chal : Type) : OracleSpec (M × Commit)

Random-oracle interface for the Fiat-Shamir transform.

@[reducible]

def FiatShamir.Stateful.signSpec (M Commit Resp : Type) : OracleSpec M

Signing-oracle interface presented to the CMA adversary.

@[reducible]

def FiatShamir.Stateful.pkSpec (Stmt : Type) : OracleSpec Unit

Public-key oracle interface: a single GetPK query returning the challenger's public key.

@[reducible]

def FiatShamir.Stateful.progSpec (M Commit Chal : Type) : OracleSpec (M × Commit × Chal)

Programming interface for the programmable random oracle.

@[reducible]

def FiatShamir.Stateful.cmaSourceSpec (M Commit Chal Resp : Type) : OracleSpec (CmaSourceQuery M Commit)

Source CMA adversary interface: uniform sampling, RO, and signing.

@[reducible]

def FiatShamir.Stateful.cmaSpec (M Commit Chal Resp Stmt : Type) : OracleSpec (CmaQuery M Commit)

The CMA adversary's complete oracle view: uniform sampling, RO, signing, and public-key oracles.

@[reducible]

def FiatShamir.Stateful.cmaPublicSpec (M Commit Chal Stmt : Type) : OracleSpec (CmaPublicQuery M Commit)

The non-signing portion of the CMA adversary's oracle view.

@[reducible]

def FiatShamir.Stateful.nmaSpec (M Commit Chal Stmt : Type) : OracleSpec (NmaQuery M Commit Chal)

The NMA-game oracle interface used internally by the CMA-to-NMA reduction. Includes uniform sampling, RO, programmable RO, and public-key queries.

def FiatShamir.Stateful.cmaRoute (M Commit Chal Resp Stmt : Type) : QueryImpl.Stateful.ExportRouteEquiv (cmaSpec M Commit Chal Resp Stmt) (cmaPublicSpec M Commit Chal Stmt) (signSpec M Commit Resp)

Route named CMA queries to the public-forwarding component or the signing component of the CMA-to-NMA reduction.

@[implicit_reducible]

instance FiatShamir.Stateful.subSpec_unif_nmaSpec (M Commit Chal Stmt : Type) : unifSpec ⊂ₒ nmaSpec M Commit Chal Stmt

instance FiatShamir.Stateful.lawfulSubSpec_unif_nmaSpec (M Commit Chal Stmt : Type) : unifSpec.LawfulSubSpec (nmaSpec M Commit Chal Stmt)

@[implicit_reducible]

instance FiatShamir.Stateful.subSpec_unif_cmaSpec (M Commit Chal Resp Stmt : Type) : unifSpec ⊂ₒ cmaSpec M Commit Chal Resp Stmt

instance FiatShamir.Stateful.lawfulSubSpec_unif_cmaSpec (M Commit Chal Resp Stmt : Type) : unifSpec.LawfulSubSpec (cmaSpec M Commit Chal Resp Stmt)

@[implicit_reducible]

instance FiatShamir.Stateful.subSpec_ro_cmaSpec (M Commit Chal Resp Stmt : Type) : roSpec M Commit Chal ⊂ₒ cmaSpec M Commit Chal Resp Stmt

instance FiatShamir.Stateful.lawfulSubSpec_ro_cmaSpec (M Commit Chal Resp Stmt : Type) : (roSpec M Commit Chal).LawfulSubSpec (cmaSpec M Commit Chal Resp Stmt)

@[implicit_reducible]

instance FiatShamir.Stateful.subSpec_sign_cmaSpec (M Commit Chal Resp Stmt : Type) : signSpec M Commit Resp ⊂ₒ cmaSpec M Commit Chal Resp Stmt

instance FiatShamir.Stateful.lawfulSubSpec_sign_cmaSpec (M Commit Chal Resp Stmt : Type) : (signSpec M Commit Resp).LawfulSubSpec (cmaSpec M Commit Chal Resp Stmt)

@[implicit_reducible]

instance FiatShamir.Stateful.subSpec_pk_cmaSpec (M Commit Chal Resp Stmt : Type) : pkSpec Stmt ⊂ₒ cmaSpec M Commit Chal Resp Stmt

instance FiatShamir.Stateful.lawfulSubSpec_pk_cmaSpec (M Commit Chal Resp Stmt : Type) : (pkSpec Stmt).LawfulSubSpec (cmaSpec M Commit Chal Resp Stmt)

@[implicit_reducible]

instance FiatShamir.Stateful.subSpec_fsRo_cmaSpec (M Commit Chal Resp Stmt : Type) : unifSpec + roSpec M Commit Chal ⊂ₒ cmaSpec M Commit Chal Resp Stmt

The Fiat-Shamir public random-oracle interface embeds into the named CMA interface by routing uniform and random-oracle queries to their named constructors.

instance FiatShamir.Stateful.lawfulSubSpec_fsRo_cmaSpec (M Commit Chal Resp Stmt : Type) : (unifSpec + roSpec M Commit Chal).LawfulSubSpec (cmaSpec M Commit Chal Resp Stmt)

@[implicit_reducible]

instance FiatShamir.Stateful.subSpec_sourceCma_cmaSpec (M Commit Chal Resp Stmt : Type) : unifSpec + roSpec M Commit Chal + signSpec M Commit Resp ⊂ₒ cmaSpec M Commit Chal Resp Stmt

The source CMA adversary interface embeds into the named CMA interface.

instance FiatShamir.Stateful.lawfulSubSpec_sourceCma_cmaSpec (M Commit Chal Resp Stmt : Type) : (unifSpec + roSpec M Commit Chal + signSpec M Commit Resp).LawfulSubSpec (cmaSpec M Commit Chal Resp Stmt)

Plain state shapes

@[reducible, inline]

abbrev FiatShamir.Stateful.RoCache (M Commit Chal : Type) : Type

Random-oracle cache state.

@[reducible, inline]

abbrev FiatShamir.Stateful.OuterState (M : Type) : Type

Outer CMA-to-NMA state: the signed-message log.

@[reducible, inline]

abbrev FiatShamir.Stateful.NmaState (M Commit Chal Stmt Wit : Type) : Type

Inner NMA state: RO cache, optional keypair, and bad flag.

@[reducible, inline]

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

Direct CMA state without the bad flag: signed log, RO cache, keypair.

@[reducible, inline]

abbrev FiatShamir.Stateful.CmaState (M Commit Chal Stmt Wit : Type) : Type

Direct CMA state with the bad flag as the final component.

@[reducible]

def FiatShamir.Stateful.nmaInit (M Commit Chal Stmt Wit : Type) : NmaState M Commit Chal Stmt Wit

Initial NMA state: empty RO cache, no keypair, bad unset.

@[reducible]

def FiatShamir.Stateful.cmaInit (M Commit Chal Stmt Wit : Type) : CmaState M Commit Chal Stmt Wit

Initial CMA state: empty signed log, empty RO cache, no keypair, bad unset.

Frame for linking CMA-to-NMA over direct CMA state

def FiatShamir.Stateful.cmaOuterLens (M Commit Chal Stmt Wit : Type) : PFunctor.Lens.State (CmaState M Commit Chal Stmt Wit) (OuterState M)

Lens selecting the signed-message log from direct CMA state.

def FiatShamir.Stateful.cmaNmaLens (M Commit Chal Stmt Wit : Type) : PFunctor.Lens.State (CmaState M Commit Chal Stmt Wit) (NmaState M Commit Chal Stmt Wit)

Lens selecting the NMA state from direct CMA state.

instance FiatShamir.Stateful.cmaOuterLens_isVeryWellBehaved (M Commit Chal Stmt Wit : Type) : (cmaOuterLens M Commit Chal Stmt Wit).IsVeryWellBehaved

instance FiatShamir.Stateful.cmaNmaLens_isVeryWellBehaved (M Commit Chal Stmt Wit : Type) : (cmaNmaLens M Commit Chal Stmt Wit).IsVeryWellBehaved

instance FiatShamir.Stateful.cmaOuterLens_cmaNmaLens_isSeparated (M Commit Chal Stmt Wit : Type) : (cmaOuterLens M Commit Chal Stmt Wit).IsSeparated (cmaNmaLens M Commit Chal Stmt Wit)

def FiatShamir.Stateful.cmaFrame (M Commit Chal Stmt Wit : Type) : QueryImpl.Stateful.Frame (CmaState M Commit Chal Stmt Wit) (OuterState M) (NmaState M Commit Chal Stmt Wit)

The direct CMA frame used by cmaToNma.linkWith nma.

Frame for routing the CMA-to-NMA reduction

def FiatShamir.Stateful.unitLens (σ : Type) : PFunctor.Lens.State σ PUnit.{1}

Trivial lens into a PUnit component.

instance FiatShamir.Stateful.unitLens_isVeryWellBehaved (σ : Type) : (unitLens σ).IsVeryWellBehaved

instance FiatShamir.Stateful.unitLens_id_isSeparated (σ : Type) : (unitLens σ).IsSeparated (PFunctor.Lens.State.id σ)

def FiatShamir.Stateful.cmaToNmaFrame (M : Type) : QueryImpl.Stateful.Frame (OuterState M) PUnit.{1} (OuterState M)

Frame used to compose the stateless forwarding part of cmaToNma with the stateful signing simulator while keeping only the signing log as state.