Stateful Fiat-Shamir CMA games

Direct QueryImpl.Stateful versions of the Fiat-Shamir CMA/NMA games. These handlers use ordinary product states rather than heap packages.

nma: no-message-attack game

noncomputable def FiatShamir.Stateful.nmaPublic (M : Type) [DecidableEq M] (Commit : Type) [DecidableEq Commit] (Chal : Type) [SampleableType Chal] {Stmt Wit : Type} {rel : Stmt → Wit → Bool} (hr : GenerableRelation Stmt Wit rel) : QueryImpl.Stateful unifSpec (cmaPublicSpec M Commit Chal Stmt) (NmaState M Commit Chal Stmt Wit)

Public part of the no-message-attack game.

State: random-oracle cache, lazily sampled keypair, and bad flag.

noncomputable def FiatShamir.Stateful.nmaProgram (M : Type) [DecidableEq M] (Commit : Type) [DecidableEq Commit] (Chal : Type) {Stmt Wit : Type} : QueryImpl.Stateful unifSpec (progSpec M Commit Chal) (NmaState M Commit Chal Stmt Wit)

Programmable random-oracle part of the no-message-attack game.

noncomputable def FiatShamir.Stateful.nma (M : Type) [DecidableEq M] (Commit : Type) [DecidableEq Commit] (Chal : Type) [SampleableType Chal] {Stmt Wit : Type} {rel : Stmt → Wit → Bool} (hr : GenerableRelation Stmt Wit rel) : QueryImpl.Stateful unifSpec (nmaSpec M Commit Chal Stmt) (NmaState M Commit Chal Stmt Wit)

The no-message-attack game as a direct stateful handler.

cmaToNma: CMA-to-NMA reduction

noncomputable def FiatShamir.Stateful.cmaPublicForward (M Commit Chal : Type) {Stmt : Type} : QueryImpl.Stateful (nmaSpec M Commit Chal Stmt) (cmaPublicSpec M Commit Chal Stmt) PUnit.{1}

Forward the public, non-signing CMA queries to the shared NMA interface.

This component has no private state. Its imports are intentionally the same ambient nmaSpec used by the signing simulator, so adversarial RO queries and programming queries interact through one inner random-oracle cache.

noncomputable def FiatShamir.Stateful.cmaSignSim (M Commit Chal : Type) {Stmt Resp : Type} (simT : Stmt → ProbComp (Commit × Chal × Resp)) : QueryImpl.Stateful (nmaSpec M Commit Chal Stmt) (signSpec M Commit Resp) (OuterState M)

Signing part of the CMA-to-NMA reduction.

State: signed-message log. Signing queries sample the HVZK simulator and program the random oracle through the shared NMA interface.

noncomputable def FiatShamir.Stateful.cmaToNma (M Commit Chal : Type) {Stmt Resp : Type} (simT : Stmt → ProbComp (Commit × Chal × Resp)) : QueryImpl.Stateful (nmaSpec M Commit Chal Stmt) (cmaSpec M Commit Chal Resp Stmt) (OuterState M)

The CMA-to-NMA reduction as a direct stateful handler.

Public queries are forwarded to the NMA interface; signing queries are handled by the simulator component that owns the signed-message log. Both paths share the same nmaSpec imports on purpose.

cmaSim: simulated CMA game

@[reducible, inline]

noncomputable abbrev FiatShamir.Stateful.cmaSim (M : Type) [DecidableEq M] (Commit : Type) [DecidableEq Commit] (Chal : Type) [SampleableType Chal] {Stmt Wit : Type} {rel : Stmt → Wit → Bool} {Resp : Type} (hr : GenerableRelation Stmt Wit rel) (simT : Stmt → ProbComp (Commit × Chal × Resp)) : QueryImpl.Stateful unifSpec (cmaSpec M Commit Chal Resp Stmt) (CmaState M Commit Chal Stmt Wit)

The simulated CMA game, linked through the direct CMA frame.

cmaReal: real CMA game

@[reducible]

noncomputable def FiatShamir.Stateful.fsBaseImpl (M : Type) [DecidableEq M] (Commit : Type) [DecidableEq Commit] (Chal : Type) [SampleableType Chal] : QueryImpl (unifSpec + roSpec M Commit Chal) (StateT (RoCache M Commit Chal) ProbComp)

The public random-oracle runtime as an explicit cache-state QueryImpl.

This handler is shared by the fixed-key public post-keygen experiment and the direct named CMA game.

@[reducible]

noncomputable def FiatShamir.Stateful.cmaRealFixedSign (M : Type) [DecidableEq M] (Commit : Type) [DecidableEq Commit] (Chal : Type) [SampleableType Chal] {Stmt Wit : Type} {rel : Stmt → Wit → Bool} {Resp PrvState : Type} (sigma : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel) (hr : GenerableRelation Stmt Wit rel) (pk : Stmt) (sk : Wit) : QueryImpl (signSpec M Commit Resp) (StateT (RoCache M Commit Chal) ProbComp)

Fixed-key real Fiat-Shamir signing over the shared random-oracle cache.

noncomputable def FiatShamir.Stateful.cmaRealSourceFull (M : Type) [DecidableEq M] (Commit : Type) [DecidableEq Commit] (Chal : Type) [SampleableType Chal] {Stmt Wit : Type} {rel : Stmt → Wit → Bool} {Resp PrvState : Type} (sigma : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel) (hr : GenerableRelation Stmt Wit rel) : QueryImpl.Stateful unifSpec (cmaSourceSpec M Commit Chal Resp) (CmaState M Commit Chal Stmt Wit)

Source-query part of the real CMA game over the full direct CMA state.

noncomputable def FiatShamir.Stateful.cmaRealSourceFullSum (M : Type) [DecidableEq M] (Commit : Type) [DecidableEq Commit] (Chal : Type) [SampleableType Chal] {Stmt Wit : Type} {rel : Stmt → Wit → Bool} {Resp PrvState : Type} (sigma : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel) (hr : GenerableRelation Stmt Wit rel) : QueryImpl.Stateful unifSpec (unifSpec + roSpec M Commit Chal + signSpec M Commit Resp) (CmaState M Commit Chal Stmt Wit)

Source-query part of the real CMA game over the concrete sum interface used by SignatureAlg.unforgeableAdv.

noncomputable def FiatShamir.Stateful.cmaReal (M : Type) [DecidableEq M] (Commit : Type) [DecidableEq Commit] (Chal : Type) [SampleableType Chal] {Stmt Wit : Type} {rel : Stmt → Wit → Bool} {Resp PrvState : Type} (sigma : SigmaProtocol Stmt Wit Commit PrvState Chal Resp rel) (hr : GenerableRelation Stmt Wit rel) : QueryImpl.Stateful unifSpec (cmaSpec M Commit Chal Resp Stmt) (CmaState M Commit Chal Stmt Wit)

The real CMA game as a direct stateful handler.

On signing queries, this runs the real Sigma protocol and appends the message to the signed log. The bad flag is preserved and never set by real signing.