Fiat-Shamir forking infrastructure

Wraps a managed-RO NMA adversary against FiatShamir into a single-oracle OracleComp (unifSpec + (Unit →ₒ Chal)) computation that ReplayFork can fork. Collects the forgery, the adversary's cache, the live query log, and a verified flag, and exposes a forkPoint that picks the index at which to rewind.

The main export is Fork.replayForkingBound: the Fiat-Shamir-specific analogue of Firsov-Janku's forking_lemma_ro, stated at the OracleComp level. Callers in FiatShamir.Sigma.Security compose it with ReplayFork.forkReplay_propertyTransfer to drive the NMA-to-extraction step of euf_nma_bound.

structure FiatShamir.Fork.Trace {Commit Chal Resp : Type} (M : Type) : Type

Trace used by the Fiat-Shamir forking reduction for managed-RO NMA adversaries.

Fields:

• forgery: the final (message, (commitment, response)) triple produced by the adversary.
• advCache: snapshot of the adversary's locally programmed random oracle. Only the reduction side reads from it: runTrace.verified and the forking bound treat it purely as bookkeeping. In the managed-RO model every adversary challenge query is routed through the live oracle, so programmed entries that ever actually influence a verified forgery also appear in roCache; this is the invariant that euf_cma_to_nma is responsible for establishing when it bridges advCache-only entries back to the live log.
• roCache: the live random-oracle cache populated by managed-RO queries during the run.
• queryLog: the list of (message, commitment) hash points actually queried (live). The forking lemma rewinds at a position of this list.
• verified: whether the forgery successfully verifies against a cached challenge for its target. runTrace consults only roCache for this flag (see its docstring).

• forgery : M × Commit × Resp
• advCache : (unifSpec + OracleSpec.ofFn fun (x : M × Commit) => Chal).QueryCache
• roCache : (OracleSpec.ofFn fun (x : M × Commit) => Chal).QueryCache
• queryLog : List (M × Commit)
• verified : Bool

def FiatShamir.Fork.Trace.target {Commit Chal Resp : Type} (M : Type) (trace : Trace M) : M × Commit

The hash point corresponding to the final forgery recorded in a fork trace.

def FiatShamir.Fork.forkPoint {Commit Chal Resp : Type} (M : Type) [DecidableEq M] [DecidableEq Commit] (qH : ℕ) (trace : Trace M) : Option (Fin (qH + 1))

Rewinding point extracted from a managed-RO fork trace. The fork is usable exactly when the final forgery verifies and its hash point appears in the live query log.

theorem FiatShamir.Fork.forkPoint_some_imp_verified {Commit Chal Resp : Type} (M : Type) [DecidableEq M] [DecidableEq Commit] {qH : ℕ} {trace : Trace M} {s : Fin (qH + 1)} (hs : forkPoint M qH trace = some s) : trace.verified = true

theorem FiatShamir.Fork.forkPoint_some_imp_mem {Commit Chal Resp : Type} (M : Type) [DecidableEq M] [DecidableEq Commit] {qH : ℕ} {trace : Trace M} {s : Fin (qH + 1)} (hs : forkPoint M qH trace = some s) : Trace.target M trace ∈ trace.queryLog

theorem FiatShamir.Fork.forkPoint_getElem?_eq_some_target {Commit Chal Resp : Type} (M : Type) [DecidableEq M] [DecidableEq Commit] {qH : ℕ} {trace : Trace M} {s : Fin (qH + 1)} (hs : forkPoint M qH trace = some s) : trace.queryLog[s]? = some (Trace.target M trace)

@[reducible, inline]

abbrev FiatShamir.Fork.wrappedSpec (Chal : Type) : OracleSpec (ℕ ⊕ Unit)

Wrapped oracle spec used by runTrace: uniform sampling plus a single counted challenge oracle exposing the random-oracle entropy.

@[reducible, inline]

abbrev FiatShamir.Fork.simSt (M Commit Chal : Type) [DecidableEq M] [DecidableEq Commit] : Type

Internal simulator state of runTrace: the cached random-oracle answers paired with the chronological list of cache-miss inputs (the trace's queryLog).

noncomputable def FiatShamir.Fork.unifFwd (M Commit Chal : Type) [DecidableEq M] [DecidableEq Commit] : QueryImpl unifSpec (StateT (simSt M Commit Chal) (OracleComp (wrappedSpec Chal)))

Forwards a uniform-spec query through to the wrapped spec's Sum.inl summand without touching the simulator state.

noncomputable def FiatShamir.Fork.roImpl (M Commit Chal : Type) [DecidableEq M] [DecidableEq Commit] : QueryImpl (OracleSpec.ofFn fun (x : M × Commit) => Chal) (StateT (simSt M Commit Chal) (OracleComp (wrappedSpec Chal)))

Caching random-oracle implementation: on a cache hit the recorded answer is returned, on a cache miss a fresh Sum.inr () query is issued, the answer is cached, and the miss input (msg, c) is appended to the trace's internal queryLog.

noncomputable def FiatShamir.Fork.runTrace {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] (nmaAdv : (FiatShamir σ hr M).managedRoNmaAdv) (pk : Stmt) : OracleComp (wrappedSpec Chal) (Trace M)

Replay a managed-RO NMA adversary against a single counted challenge oracle, keeping both the adversary-returned cache and the live query log that the forking lemma can rewind.

The verified flag is computed strictly from the live roCache so that a successful forkPoint extraction always pins the verifying challenge to the live random-oracle answer at the corresponding outer-log position. Forgeries whose verification depends only on programmed entries the adversary supplies in advCache are not counted: this is a strict strengthening over an advCache-fallback variant and strictly shrinks Fork.advantage. The residual obligation, "every advCache-only forgery that would have verified also has a corresponding live RO query", is a caller-side invariant that must be discharged by the managed-RO CMA→NMA reduction. Downstream, this is the role of euf_cma_to_nma in FiatShamir/Sigma/Security.lean, whose sigma→NMA simulation ensures that every advCache programming step is mirrored by a live query into roCache.

noncomputable def FiatShamir.Fork.exp {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] (nmaAdv : (FiatShamir σ hr M).managedRoNmaAdv) (qH : ℕ) : ProbComp Bool

Forkable managed-RO NMA experiment. Success means the final forged transcript verifies and the corresponding hash point appears in the live query log, so the forking lemma can rewind it.

noncomputable def FiatShamir.Fork.advantage {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] (nmaAdv : (FiatShamir σ hr M).managedRoNmaAdv) (qH : ℕ) : ENNReal

The forkable success probability of a managed-RO NMA adversary.

theorem FiatShamir.Fork.runTrace_queryLog_length_eq {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] (nmaAdv : (FiatShamir σ hr M).managedRoNmaAdv) (pk : Stmt) {x : Trace M} {outerLog : (wrappedSpec Chal).QueryLog} (hx : (x, outerLog) ∈ support (runTrace σ hr M nmaAdv pk).replayFirstRun) : x.queryLog.length = outerLog.countQ fun (x : (wrappedSpec Chal).Domain) => x = Sum.inr ()

Specialization of queryLog_length_eq_outer_inr_count to runTrace's initial state (∅, []): the trace's queryLog has the same length as the count of Sum.inr () outer queries in the recorded log.

theorem FiatShamir.Fork.runTrace_cache_outer_lockstep {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] [DecidableEq Chal] (nmaAdv : (FiatShamir σ hr M).managedRoNmaAdv) (pk : Stmt) {x : Trace M} {outerLog : (wrappedSpec Chal).QueryLog} (hx : (x, outerLog) ∈ support (runTrace σ hr M nmaAdv pk).replayFirstRun) (i : ℕ) (h_hi : i < x.queryLog.length) : ∃ (ω : (OracleSpec.ofFn fun (x : M × Commit) => Chal).Range x.queryLog[i]), x.roCache x.queryLog[i] = some ω ∧ QueryLog.getQueryValue? outerLog (Sum.inr ()) i = some ω

Specialization of queryLog_cache_outer_lockstep to runTrace's initial state (∅, []): the trace's queryLog[i] is cached in x.roCache, and the cached value matches the outer log's i-th Sum.inr () response.

theorem FiatShamir.Fork.runTrace_verified_imp_verify {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] (nmaAdv : (FiatShamir σ hr M).managedRoNmaAdv) (pk : Stmt) {x : Trace M} {outerLog : (wrappedSpec Chal).QueryLog} (hx : (x, outerLog) ∈ support (runTrace σ hr M nmaAdv pk).replayFirstRun) (hv : x.verified = true) : ∃ (ω : (OracleSpec.ofFn fun (x : M × Commit) => Chal).Range (Trace.target M x)), x.roCache (Trace.target M x) = some ω ∧ σ.verify pk (Trace.target M x).2 ω x.forgery.2.2 = true

Decoding the verified flag of a trace produced by runTrace. If the trace's verified field is true, then there is a cached challenge ω for x.target and the corresponding σ.verify succeeds. Used by forkSupportInvariant_of_mem_replayFirstRun.

theorem FiatShamir.Fork.runTrace_forkPoint_CfReachable {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] [DecidableEq Chal] [SampleableType Chal] (nmaAdv : (FiatShamir σ hr M).managedRoNmaAdv) (qH : ℕ) (pk : Stmt) : (runTrace σ hr M nmaAdv pk).CfReachable (fun (j : ℕ ⊕ Unit) => match j with | Sum.inl val => 0 | Sum.inr PUnit.unit => qH) (Sum.inr ()) (forkPoint M qH)

The forkPoint-based reachability invariant for runTrace: whenever forkPoint qH x = some s, the outer QueryLog of replayFirstRun (runTrace ...) has a Sum.inr () query at position ↑s. This holds because each cache miss in runTrace's roImpl issues exactly one Sum.inr () query and appends one entry to the trace's internal queryLog, so the trace's logical fork index s (an offset into trace.queryLog) always corresponds to a real outer-log query at the same position.

theorem FiatShamir.Fork.runTrace_queryLog_take_eq {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] (nmaAdv : (FiatShamir σ hr M).managedRoNmaAdv) (pk : Stmt) {x₁ x₂ : Trace M} {outerLog₁ outerLog₂ : (wrappedSpec Chal).QueryLog} (h₁ : (x₁, outerLog₁) ∈ support (runTrace σ hr M nmaAdv pk).replayFirstRun) (h₂ : (x₂, outerLog₂) ∈ support (runTrace σ hr M nmaAdv pk).replayFirstRun) (p : (wrappedSpec Chal).QueryLog) {v₁ v₂ : Chal} {rest₁ rest₂ : (wrappedSpec Chal).QueryLog} (hlog₁ : outerLog₁ = p ++ ⟨Sum.inr (), v₁⟩ :: rest₁) (hlog₂ : outerLog₂ = p ++ ⟨Sum.inr (), v₂⟩ :: rest₂) : List.take ((p.countQ fun (x : (wrappedSpec Chal).Domain) => x = Sum.inr ()) + 1) x₁.queryLog = List.take ((p.countQ fun (x : (wrappedSpec Chal).Domain) => x = Sum.inr ()) + 1) x₂.queryLog

Determinism of runTrace's inner queryLog from the outer-log prefix. If the outer logs of two runs of runTrace share a prefix p followed by a Sum.inr () query (whose response may differ across runs), then the traces' internal queryLogs coincide on the first p.countQ (· = Sum.inr ()) + 1 entries. This is the runTrace specialization of inner_prefix_det_one_more_inr, rephrased at the replayFirstRun-visible level.

theorem FiatShamir.Fork.replayForkingBound {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] [DecidableEq Chal] [SampleableType Chal] [Fintype Chal] [Inhabited Chal] (nmaAdv : (FiatShamir σ hr M).managedRoNmaAdv) (qH : ℕ) (pk : Stmt) (P_out : Trace M → (unifSpec + OracleSpec.ofFn fun (x : Unit) => Chal).QueryLog → Prop) (hP : ∀ {x : Trace M} {log : (wrappedSpec Chal).QueryLog}, (x, log) ∈ support (runTrace σ hr M nmaAdv pk).replayFirstRun → P_out x log) (hreach : (runTrace σ hr M nmaAdv pk).CfReachable (fun (j : ℕ ⊕ Unit) => match j with | Sum.inl val => 0 | Sum.inr PUnit.unit => qH) (Sum.inr ()) (forkPoint M qH)) : have wrappedMain := runTrace σ hr M nmaAdv pk; have cf := forkPoint M qH; let qb := fun (j : ℕ ⊕ Unit) => match j with | Sum.inl val => 0 | Sum.inr PUnit.unit => qH; have acc := probEvent wrappedMain fun (x : Trace M) => (cf x).isSome = true; acc * (acc / (↑qH + 1) - challengeSpaceInv Chal) ≤ probEvent (wrappedMain.forkReplay qb (Sum.inr ()) cf) fun (r : Option (Trace M × Trace M)) => ∃ (x₁ : Trace M) (x₂ : Trace M) (s : Fin (qH + 1)) (log₁ : (unifSpec + OracleSpec.ofFn fun (x : Unit) => Chal).QueryLog) (log₂ : (unifSpec + OracleSpec.ofFn fun (x : Unit) => Chal).QueryLog), r = some (x₁, x₂) ∧ cf x₁ = some s ∧ cf x₂ = some s ∧ QueryLog.getQueryValue? log₁ (Sum.inr ()) ↑s ≠ QueryLog.getQueryValue? log₂ (Sum.inr ()) ↑s ∧ P_out x₁ log₁ ∧ P_out x₂ log₂

Managed-RO replay-fork convenience theorem at a fixed public key, stated at the OracleComp (unifSpec + (Unit →ₒ Chal)) level.

This is the Fiat-Shamir-specific analogue of Firsov-Janku's forking_lemma_ro at fsec/proof/ForkingRO.ec:443. It packages the replay quantitative bound with the distinct-answer and postcondition-transfer facts for the wrapped managed random-oracle trace experiment, composing le_probEvent_isSome_forkReplay (quantitative bound) and forkReplay_propertyTransfer (postcondition transfer).

On the level of the statement. We state the bound at the OracleComp level rather than lifting through simulateQ to ProbComp. Each caller (e.g. euf_nma_bound) can bridge to ProbComp in one line using uniformSampleImpl.probEvent_simulateQ when needed, keeping this lemma focused on the forking-lemma content.

On the target-equality conjunct. A maximally-informative version would also conclude x₁.target = x₂.target (i.e. message-commit pair coincidence at the fork point), matching Firsov-Janku's forking_lemma_ro. In the Lean formalization this conjunct is consumed by the downstream reduction euf_nma_bound to align the cached challenges ω_i = x_i.roCache target. Since it relies on a value-level log-prefix invariant across replayRunWithTraceValue plus a correspondence between the adversary's internal queryLog and the outer QueryLog, it is extracted through the caller-provided P_out transfer predicate: the caller may choose P_out so that P_out x log pins x.target to a deterministic function of (log, cf x), and then derive target-equality from the distinct-answer disagreement on the outer log.

On the hreach hypothesis. CfReachable ensures that whenever forkPoint selects an index s for a trace x, the outer QueryLog actually has an i = Sum.inr () query at position ↑s. For the FiatShamir setting this follows from the correspondence between the trace's internal queryLog : List (M × Commit) and the outer QueryLog of Sum.inr () queries: each cache miss in roImpl appends to both simultaneously, so a logical index s into the trace's list corresponds to the same physical position in the outer log. Callers discharge hreach by establishing this correspondence at the level of runTrace.

On typeclass requirements. The wrappedSpec Chal oracle space is unifSpec + (Unit →ₒ Chal), and the quantitative section of ReplayFork.lean requires the typeclass [OracleSpec.LawfulSubSpec unifSpec spec] (to factor probOutput_uniformSample through liftComp on the forkReplay side). This instance is discharged by Mathlib automation at this call site.

Currently conditional on the two B1 prefix-faithfulness sorrys (transitively via le_probEvent_isSome_forkReplay → sq_probOutput_main_le_noGuardReplayComp → evalDist_uniform_bind_fst_replayRunWithTraceValue_takeBeforeForkAt and tsum_probOutput_replayFirstRun_weight_takeBeforeForkAt).