Replay-Based Forking

This file adds an additive replay-based fork path beside the existing seed-based forking infrastructure in VCVio.CryptoFoundations.SeededFork.

The key idea is to record a first-run QueryLog, then replay that transcript exactly up to a selected fork point while changing one distinguished oracle answer. This is meant to support settings such as Fiat-Shamir where ambient randomness should be replayed by transcript rather than by pre-generated seed coverage.

def QueryLog.inputAt? {ι : Type} {spec : OracleSpec ι} (log : spec.QueryLog) (n : ℕ) : Option ι

The query input at position n in the full interleaved log, if it exists.

def QueryLog.getQueryValue? {ι : Type} {spec : OracleSpec ι} [spec.DecidableEq] (log : spec.QueryLog) (t : ι) (n : ℕ) : Option (spec.Range t)

The n-th answer in the log for queries to oracle t, if it exists.

@[simp]

theorem QueryLog.inputAt?_logQuery_of_lt {ι : Type} {spec : OracleSpec ι} (log : spec.QueryLog) (t : ι) (u : spec.Range t) {n : ℕ} (hn : n < List.length log) : inputAt? (log.logQuery t u) n = inputAt? log n

@[simp]

theorem QueryLog.inputAt?_logQuery_self {ι : Type} {spec : OracleSpec ι} (log : spec.QueryLog) (t : ι) (u : spec.Range t) : inputAt? (log.logQuery t u) (List.length log) = some t

theorem QueryLog.getQ_logQuery {ι : Type} {spec : OracleSpec ι} (log : spec.QueryLog) (t : ι) (u : spec.Range t) (p : ι → Prop) [DecidablePred p] : (log.logQuery t u).getQ p = log.getQ p ++ if p t then [⟨t, u⟩] else []

Decompose getQ across a logQuery step.

theorem QueryLog.getQ_getElem?_eq_of_getQueryValue?_eq_some {ι : Type} {spec : OracleSpec ι} [spec.DecidableEq] (log : spec.QueryLog) (t : ι) (n : ℕ) (u : spec.Range t) (h : getQueryValue? log t n = some u) : (log.getQ fun (x : spec.Domain) => x = t)[n]? = some ⟨t, u⟩

If getQueryValue? log t n = some u, then the n-th t-filtered entry of log is ⟨t, u⟩.

theorem QueryLog.getQueryValue?_eq_some_of_getQ_getElem? {ι : Type} {spec : OracleSpec ι} [spec.DecidableEq] (log : spec.QueryLog) (t : ι) (n : ℕ) (u : spec.Range t) (h : (log.getQ fun (x : spec.Domain) => x = t)[n]? = some ⟨t, u⟩) : getQueryValue? log t n = some u

Converse: if the n-th t-filtered entry is ⟨t, u⟩, then getQueryValue? log t n = some u.

theorem QueryLog.getQ_eq_mem {ι : Type} {spec : OracleSpec ι} [spec.DecidableEq] (log : spec.QueryLog) (t : ι) {entry : (t' : ι) × spec.Range t'} (h : entry ∈ log.getQ fun (x : spec.Domain) => x = t) : entry.fst = t

Every entry of log.getQ (· = t) has its first component equal to t.

theorem QueryLog.getQueryValue?_isSome_of_lt {ι : Type} {spec : OracleSpec ι} [spec.DecidableEq] (log : spec.QueryLog) (t : ι) (n : ℕ) (h : n < (log.getQ fun (x : spec.Domain) => x = t).length) : (getQueryValue? log t n).isSome = true

If the t-filtered log has at least n + 1 entries, then getQueryValue? log t n is some _.

theorem QueryLog.getQueryValue?_cons_of_ne {ι : Type} {spec : OracleSpec ι} [spec.DecidableEq] (entry : (t' : ι) × spec.Range t') (log : spec.QueryLog) (t : ι) (n : ℕ) (h : entry.fst ≠ t) : getQueryValue? (entry :: log) t n = getQueryValue? log t n

Prepending an entry whose oracle index does not match t leaves the t-indexed view of the log unchanged.

theorem QueryLog.getQueryValue?_cons_self_zero {ι : Type} {spec : OracleSpec ι} [spec.DecidableEq] (t : ι) (u : spec.Range t) (log : spec.QueryLog) : getQueryValue? (⟨t, u⟩ :: log) t 0 = some u

The first entry of getQueryValue? (⟨t, u⟩ :: log) t 0 is the prepended value.

theorem QueryLog.getQueryValue?_cons_self_succ {ι : Type} {spec : OracleSpec ι} [spec.DecidableEq] (t : ι) (u : spec.Range t) (log : spec.QueryLog) (n : ℕ) : getQueryValue? (⟨t, u⟩ :: log) t (n + 1) = getQueryValue? log t n

Prepending a matching ⟨t, _⟩ entry shifts later t-indexed lookups by one.

def QueryLog.takeBeforeForkAt {ι : Type} {spec : OracleSpec ι} [spec.DecidableEq] : spec.QueryLog → ι → ℕ → spec.QueryLog

The prefix of log up to (but not including) the s-th i-query.

If log has fewer than s + 1 queries to i, this returns the entire log. This is the replay analogue of QuerySeed.takeAtIndex and is the key slicing operator used in the Cauchy-Schwarz step of the replay forking bound.

@[simp]

theorem QueryLog.takeBeforeForkAt_nil {ι : Type} {spec : OracleSpec ι} [spec.DecidableEq] (i : ι) (s : ℕ) : takeBeforeForkAt [] i s = []

theorem QueryLog.takeBeforeForkAt_cons_of_ne {ι : Type} {spec : OracleSpec ι} [spec.DecidableEq] (t : ι) (u : spec.Range t) (tl : spec.QueryLog) (i : ι) (s : ℕ) (h : t ≠ i) : takeBeforeForkAt (⟨t, u⟩ :: tl) i s = ⟨t, u⟩ :: takeBeforeForkAt tl i s

theorem QueryLog.takeBeforeForkAt_cons_self_zero {ι : Type} {spec : OracleSpec ι} [spec.DecidableEq] (t : ι) (u : spec.Range t) (tl : spec.QueryLog) : takeBeforeForkAt (⟨t, u⟩ :: tl) t 0 = []

theorem QueryLog.takeBeforeForkAt_cons_self_succ {ι : Type} {spec : OracleSpec ι} [spec.DecidableEq] (t : ι) (u : spec.Range t) (tl : spec.QueryLog) (s : ℕ) : takeBeforeForkAt (⟨t, u⟩ :: tl) t (s + 1) = ⟨t, u⟩ :: takeBeforeForkAt tl t s

theorem QueryLog.countQ_takeBeforeForkAt_le {ι : Type} {spec : OracleSpec ι} [spec.DecidableEq] (log : spec.QueryLog) (i : ι) (s : ℕ) : ((takeBeforeForkAt log i s).countQ fun (x : spec.Domain) => x = i) ≤ s

The prefix takeBeforeForkAt log i s has at most s queries to i.

theorem QueryLog.countQ_takeBeforeForkAt_eq {ι : Type} {spec : OracleSpec ι} [spec.DecidableEq] (log : spec.QueryLog) (i : ι) (s : ℕ) (h : s < (log.getQ fun (x : spec.Domain) => x = i).length) : ((takeBeforeForkAt log i s).countQ fun (x : spec.Domain) => x = i) = s

If log contains at least s + 1 queries to i, then takeBeforeForkAt log i s has exactly s queries to i.

theorem QueryLog.takeBeforeForkAt_prefix {ι : Type} {spec : OracleSpec ι} [spec.DecidableEq] (log : spec.QueryLog) (i : ι) (s : ℕ) : takeBeforeForkAt log i s <+: log

takeBeforeForkAt log i s is a prefix of log.

theorem QueryLog.getQueryValue?_takeBeforeForkAt_self {ι : Type} {spec : OracleSpec ι} [spec.DecidableEq] (log : spec.QueryLog) (i : ι) (s : ℕ) : getQueryValue? (takeBeforeForkAt log i s) i s = none

getQueryValue? on the truncation at index i position s is none: the prefix has fewer than s + 1 entries at oracle i.

theorem QueryLog.takeBeforeForkAt_of_getQ_length_le {ι : Type} {spec : OracleSpec ι} [spec.DecidableEq] (log : spec.QueryLog) (i : ι) (s : ℕ) (h : (log.getQ fun (x : spec.Domain) => x = i).length ≤ s) : takeBeforeForkAt log i s = log

If log has at most s entries of type i, then truncating log at position s leaves it unchanged: there is no s-th i-entry to truncate before.

structure OracleComp.ReplayForkState {ι : Type} (spec : OracleSpec ι) (i : ι) : Type u_1

Replay state for the second run of a replay-based fork.

trace is the first-run transcript, cursor tracks how much of that transcript has been matched so far, distinguishedCount counts how many queries to the forked oracle family have already been replayed, and observed stores the actual second-run transcript.

• trace : spec.QueryLog
• cursor : ℕ
• distinguishedCount : ℕ
• forkQuery : ℕ
• replacement : spec.Range i
• forkConsumed : Bool
• mismatch : Bool
• observed : spec.QueryLog

def OracleComp.ReplayForkState.init {ι : Type} {spec : OracleSpec ι} {i : ι} (trace : spec.QueryLog) (forkQuery : ℕ) (replacement : spec.Range i) : ReplayForkState spec i

Initial replay state before the second run starts.

def OracleComp.ReplayForkState.nextEntry? {ι : Type} {spec : OracleSpec ι} {i : ι} (st : ReplayForkState spec i) : Option ((t : ι) × spec.Range t)

The next entry in the logged first-run transcript, if any.

def OracleComp.ReplayForkState.noteObserved {ι : Type} {spec : OracleSpec ι} {i : ι} (st : ReplayForkState spec i) (t : ι) (u : spec.Range t) : ReplayForkState spec i

Record an observed query-answer pair in the second-run log.

def OracleComp.ReplayForkState.markMismatch {ι : Type} {spec : OracleSpec ι} {i : ι} (st : ReplayForkState spec i) : ReplayForkState spec i

Mark the replay as having deviated from the first-run prefix.

def OracleComp.replayOracle {ι : Type} {spec : OracleSpec ι} [spec.DecidableEq] (i : ι) : QueryImpl spec (StateT (ReplayForkState spec i) (OracleComp spec))

Replay oracle for the second run of a replay-based fork.

Before the fork point, the oracle must match the logged first-run transcript exactly. At the selected distinguished query it returns the replacement answer. Once the fork point has been consumed, or once replay has mismatched the logged prefix, the oracle falls through to the live ambient oracle.

@[reducible]

def OracleComp.replayFirstRun {ι : Type} {spec : OracleSpec ι} {α : Type} (main : OracleComp spec α) : OracleComp spec (α × spec.QueryLog)

Run main with query logging. This is the first-run object for replay forks.

@[simp]

theorem OracleComp.fst_map_replayFirstRun {ι : Type} {spec : OracleSpec ι} {α : Type} (main : OracleComp spec α) : Prod.fst <$> main.replayFirstRun = main

@[simp]

theorem OracleComp.probEvent_fst_replayFirstRun {ι : Type} {spec : OracleSpec ι} {α : Type} [spec.Fintype] [spec.Inhabited] (main : OracleComp spec α) (p : α → Prop) : (probEvent main.replayFirstRun fun (z : α × spec.QueryLog) => p z.1) = probEvent main p

@[simp]

theorem OracleComp.probOutput_fst_map_replayFirstRun {ι : Type} {spec : OracleSpec ι} {α : Type} [spec.Fintype] [spec.Inhabited] (main : OracleComp spec α) (x : α) : Pr[= x | Prod.fst <$> main.replayFirstRun] = Pr[= x | main]

def OracleComp.replayRunWithTraceValue {ι : Type} {spec : OracleSpec ι} {α : Type} [spec.DecidableEq] (main : OracleComp spec α) (i : ι) (trace : spec.QueryLog) (forkQuery : ℕ) (replacement : spec.Range i) : OracleComp spec (α × ReplayForkState spec i)

Replay the second run against a fixed first-run log, fork point, and replacement answer, returning both the final output and replay state.

def OracleComp.forkReplayWithTraceValue {ι : Type} {spec : OracleSpec ι} {α : Type} [spec.DecidableEq] (main : OracleComp spec α) (qb : ι → ℕ) (i : ι) (cf : α → Option (Fin (qb i + 1))) (first : α × spec.QueryLog) (u : spec.Range i) : OracleComp spec (Option (α × α))

Deterministic replay-fork core with the first-run output and transcript fixed.

This mirrors seededForkWithSeedValue: the first-run result and replacement answer are inputs, while the second run may still make live oracle calls after the fork point.

def OracleComp.forkReplay {ι : Type} {spec : OracleSpec ι} {α : Type} [spec.DecidableEq] (main : OracleComp spec α) (qb : ι → ℕ) (i : ι) (cf : α → Option (Fin (qb i + 1))) [(j : ι) → SampleableType (spec.Range j)] [unifSpec ⊂ₒ spec] : OracleComp spec (Option (α × α))

Additive replay-based fork operation.

The first run is obtained via withQueryLog. The second run then replays that transcript exactly up to the selected distinguished query, replacing exactly one answer at that query.

@[simp]

theorem OracleComp.forkReplayWithTraceValue_eq_none_of_cf_none {ι : Type} {spec : OracleSpec ι} {α : Type} [spec.DecidableEq] (main : OracleComp spec α) (qb : ι → ℕ) (i : ι) (cf : α → Option (Fin (qb i + 1))) (first : α × spec.QueryLog) (u : spec.Range i) (h : cf first.1 = none) : main.forkReplayWithTraceValue qb i cf first u = pure none

Live-mode α-marginal

Once the replay oracle has transitioned into "live mode" (either forkConsumed = true after the fork fired, or mismatch = true after a trace mismatch or exhaustion), every subsequent query simply falls through to the ambient query t and records the answer in observed. In particular, the α-component of the simulated computation coincides with main itself: the state only records observations and does not influence the output.

These lemmas are used in the B1 faithfulness proofs (evalDist_uniform_bind_fst_replay RunWithTraceValue_takeBeforeForkAt and tsum_probOutput_replayFirstRun_weight_take BeforeForkAt): after the fork point on either side (full log vs. truncated log), both computations enter live mode, and the α-marginal collapses to evalDist main.

theorem OracleComp.ReplayForkState.noteObserved_live_iff {ι : Type} {spec : OracleSpec ι} {i : ι} (st : ReplayForkState spec i) (t : ι) (u : spec.Range t) : (st.noteObserved t u).forkConsumed = st.forkConsumed ∧ (st.noteObserved t u).mismatch = st.mismatch

Live mode is preserved by noteObserved: neither forkConsumed nor mismatch is touched by recording an observation.

theorem OracleComp.fst_map_simulateQ_replayOracle_of_live {ι : Type} {spec : OracleSpec ι} {α : Type} [spec.DecidableEq] (i : ι) (main : OracleComp spec α) (st : ReplayForkState spec i) : st.forkConsumed = true ∨ st.mismatch = true → Prod.fst <$> (simulateQ (replayOracle i) main).run st = main

Live-mode α-marginal. Starting from a replay state in live mode (forkConsumed = true or mismatch = true), the α-component of running the replay oracle on main equals main itself. The state only accumulates observations; it has no effect on the α-distribution.

theorem OracleComp.evalDist_fst_map_simulateQ_replayOracle_of_live {ι : Type} {spec : OracleSpec ι} {α : Type} [spec.DecidableEq] [spec.Fintype] [spec.Inhabited] (i : ι) (main : OracleComp spec α) (st : ReplayForkState spec i) (hst : st.forkConsumed = true ∨ st.mismatch = true) : evalDist (Prod.fst <$> (simulateQ (replayOracle i) main).run st) = evalDist main

α-marginal form of fst_map_simulateQ_replayOracle_of_live, specialized to the evalDist level. Once in live mode, the α-output distribution of the replay run is evalDist main.

def OracleComp.ReplayPrefixInvariant {ι : Type} {spec : OracleSpec ι} [spec.DecidableEq] (i : ι) (st : ReplayForkState spec i) : Prop

Prefix-style replay invariant: the consumed prefix of observed matches the consumed prefix of trace at the level of query inputs, and if the fork has not fired yet then observed has no extra suffix beyond that prefix.

The values clause additionally pins down values on the non-fork positions: for every position n strictly before the fork (or every position < cursor when the fork has not yet fired), observed[n]? = trace[n]?, i.e., both the input oracle and the stored response agree. At the fork position itself the value in observed is the replacement, so only the input agrees.

The distinguishedCount_eq and fork_position clauses pin down the position of the fork entry in the filtered i-log: while pre-fork with no mismatch, distinguishedCount counts the number of i-type entries in observed; once the fork has fired, the entry at position cursor - 1 in observed is exactly the forkQuery-th (0-indexed) i-type entry, i.e., the prefix observed.take (cursor - 1) contains exactly forkQuery entries of type i.

theorem OracleComp.ReplayPrefixInvariant.init {ι : Type} {spec : OracleSpec ι} [spec.DecidableEq] {i : ι} (trace : spec.QueryLog) (forkQuery : ℕ) (replacement : spec.Range i) : ReplayPrefixInvariant i (ReplayForkState.init trace forkQuery replacement)

theorem OracleComp.replayOracle_preservesPrefixInvariant {ι : Type} {spec : OracleSpec ι} [spec.DecidableEq] (i t : ι) {st : ReplayForkState spec i} {z : spec.Range t × ReplayForkState spec i} (hInv : ReplayPrefixInvariant i st) (hz : z ∈ support ((replayOracle i t).run st)) : ReplayPrefixInvariant i z.2

Per-query preservation of the replay prefix invariant: a single replayOracle i t step starting from any state satisfying ReplayPrefixInvariant produces a state still satisfying it.

Made protected (formerly private) so the Std.Do.Triple bridge in VCVio/CryptoFoundations/ReplayForkStdDo.lean can lift this to a per-query spec consumable by mvcgen.

theorem OracleComp.replayRunWithTraceValue_preservesPrefixInvariant {ι : Type} {spec : OracleSpec ι} {α : Type} [spec.DecidableEq] (main : OracleComp spec α) (i : ι) (trace : spec.QueryLog) (forkQuery : ℕ) (replacement : spec.Range i) {z : α × ReplayForkState spec i} (hz : z ∈ support (main.replayRunWithTraceValue i trace forkQuery replacement)) : ReplayPrefixInvariant i z.2

Every reachable replay state preserves the logged query-input prefix up to cursor.

theorem OracleComp.replayRunWithTraceValue_prefix_input_eq {ι : Type} {spec : OracleSpec ι} {α : Type} [spec.DecidableEq] (main : OracleComp spec α) (i : ι) (trace : spec.QueryLog) (forkQuery : ℕ) (replacement : spec.Range i) {z : α × ReplayForkState spec i} (hz : z ∈ support (main.replayRunWithTraceValue i trace forkQuery replacement)) {n : ℕ} (hn : n < z.2.cursor) : QueryLog.inputAt? z.2.observed n = QueryLog.inputAt? z.2.trace n

Support-level replay-prefix lemma: before cursor, the second run queries the same oracle inputs as the logged first-run transcript.

theorem OracleComp.replayRunWithTraceValue_prefix_getElem?_eq {ι : Type} {spec : OracleSpec ι} {α : Type} [spec.DecidableEq] (main : OracleComp spec α) (i : ι) (trace : spec.QueryLog) (forkQuery : ℕ) (replacement : spec.Range i) {z : α × ReplayForkState spec i} (hz : z ∈ support (main.replayRunWithTraceValue i trace forkQuery replacement)) {n : ℕ} (hn : n < if z.2.forkConsumed = true then z.2.cursor - 1 else z.2.cursor) : z.2.observed[n]? = z.2.trace[n]?

Support-level value-agreement lemma: before the effective fork position (i.e., before cursor - 1 once the fork has fired, or before cursor while it has not), the second-run observed log agrees with the first-run trace log on both the query input and the stored response. This strengthens replayRunWithTraceValue_prefix_input_eq and is the key lemma for arguing that the adversary's query transcript prior to the fork is identical across the two runs.

theorem OracleComp.replayRunWithTraceValue_forkConsumed_imp_prefix_count {ι : Type} {spec : OracleSpec ι} {α : Type} [spec.DecidableEq] (main : OracleComp spec α) (i : ι) (trace : spec.QueryLog) (forkQuery : ℕ) (replacement : spec.Range i) {z : α × ReplayForkState spec i} (hz : z ∈ support (main.replayRunWithTraceValue i trace forkQuery replacement)) (hfork : z.2.forkConsumed = true) : (OracleSpec.QueryLog.getQ (List.take (z.2.cursor - 1) z.2.observed) fun (x : spec.Domain) => x = i).length = z.2.forkQuery

Extract the "fork-position count" invariant: once the fork has fired, the prefix of observed up to the fork position contains exactly st.forkQuery entries of type i. This pins down where the replacement entry sits in the filtered i-log.

theorem OracleComp.replayRunWithTraceValue_forkConsumed_imp_last_input {ι : Type} {spec : OracleSpec ι} {α : Type} [spec.DecidableEq] (main : OracleComp spec α) (i : ι) (trace : spec.QueryLog) (forkQuery : ℕ) (replacement : spec.Range i) {z : α × ReplayForkState spec i} (hz : z ∈ support (main.replayRunWithTraceValue i trace forkQuery replacement)) (hfork : z.2.forkConsumed = true) : 0 < z.2.cursor ∧ QueryLog.inputAt? z.2.trace (z.2.cursor - 1) = some i ∧ QueryLog.inputAt? z.2.observed (z.2.cursor - 1) = some i

If replay has consumed the fork point, the last consumed log entry is the distinguished query input i. This is the pathwise "same target" fact used downstream.

theorem OracleComp.replayOracle_immutable_params {ι : Type} {spec : OracleSpec ι} [spec.DecidableEq] (i t : ι) {st : ReplayForkState spec i} {z : spec.Range t × ReplayForkState spec i} (hz : z ∈ support ((replayOracle i t).run st)) : z.2.forkQuery = st.forkQuery ∧ z.2.replacement = st.replacement ∧ z.2.trace = st.trace

The replay oracle never mutates the immutable parameters forkQuery, replacement, or trace.

Made protected (formerly private) so the Std.Do.Triple bridge in VCVio/CryptoFoundations/ReplayForkStdDo.lean can lift this to a per-query spec consumable by mvcgen.

theorem OracleComp.replayRunWithTraceValue_forkQuery_eq {ι : Type} {spec : OracleSpec ι} {α : Type} [spec.DecidableEq] (main : OracleComp spec α) (i : ι) (trace : spec.QueryLog) (forkQuery : ℕ) (replacement : spec.Range i) {z : α × ReplayForkState spec i} (hz : z ∈ support (main.replayRunWithTraceValue i trace forkQuery replacement)) : z.2.forkQuery = forkQuery

theorem OracleComp.replayRunWithTraceValue_replacement_eq {ι : Type} {spec : OracleSpec ι} {α : Type} [spec.DecidableEq] (main : OracleComp spec α) (i : ι) (trace : spec.QueryLog) (forkQuery : ℕ) (replacement : spec.Range i) {z : α × ReplayForkState spec i} (hz : z ∈ support (main.replayRunWithTraceValue i trace forkQuery replacement)) : z.2.replacement = replacement

theorem OracleComp.replayRunWithTraceValue_trace_eq {ι : Type} {spec : OracleSpec ι} {α : Type} [spec.DecidableEq] (main : OracleComp spec α) (i : ι) (trace : spec.QueryLog) (forkQuery : ℕ) (replacement : spec.Range i) {z : α × ReplayForkState spec i} (hz : z ∈ support (main.replayRunWithTraceValue i trace forkQuery replacement)) : z.2.trace = trace

def OracleComp.ReplayReplacementInvariant {ι : Type} {spec : OracleSpec ι} [spec.DecidableEq] (i : ι) (st : ReplayForkState spec i) : Prop

Second replay invariant: once the fork has fired, the forkQuery-th entry among distinguished-oracle queries in the observed log is exactly the replacement value.

Before the fork fires and before any mismatch, distinguishedCount exactly tracks the number of i-entries in observed. Once the fork fires, position forkQuery in the i-filtered observed log is permanently pinned to replacement.

theorem OracleComp.ReplayReplacementInvariant.init {ι : Type} {spec : OracleSpec ι} [spec.DecidableEq] {i : ι} (trace : spec.QueryLog) (forkQuery : ℕ) (replacement : spec.Range i) : ReplayReplacementInvariant i (ReplayForkState.init trace forkQuery replacement)

theorem OracleComp.replayOracle_preservesReplacementInvariant {ι : Type} {spec : OracleSpec ι} [spec.DecidableEq] (i t : ι) {st : ReplayForkState spec i} (hInv : ReplayReplacementInvariant i st) {z : spec.Range t × ReplayForkState spec i} (hz : z ∈ support ((replayOracle i t).run st)) : ReplayReplacementInvariant i z.2

Per-query preservation of the replay replacement invariant.

Made protected (formerly private) so the Std.Do.Triple bridge in VCVio/CryptoFoundations/ReplayForkStdDo.lean can lift this to a per-query spec consumable by mvcgen.

theorem OracleComp.replayRunWithTraceValue_preservesReplacementInvariant {ι : Type} {spec : OracleSpec ι} {α : Type} [spec.DecidableEq] (main : OracleComp spec α) (i : ι) (trace : spec.QueryLog) (forkQuery : ℕ) (replacement : spec.Range i) {z : α × ReplayForkState spec i} (hz : z ∈ support (main.replayRunWithTraceValue i trace forkQuery replacement)) : ReplayReplacementInvariant i z.2

Every reachable replay state preserves the replacement invariant.

theorem OracleComp.replayRunWithTraceValue_getQueryValue?_observed_eq_replacement {ι : Type} {spec : OracleSpec ι} {α : Type} [spec.DecidableEq] (main : OracleComp spec α) (i : ι) (trace : spec.QueryLog) (forkQuery : ℕ) (replacement : spec.Range i) {z : α × ReplayForkState spec i} (hz : z ∈ support (main.replayRunWithTraceValue i trace forkQuery replacement)) (hfork : z.2.forkConsumed = true) : QueryLog.getQueryValue? z.2.observed i forkQuery = some replacement

If the replay has consumed the fork and the fork point is forkQuery, then the forkQuery-th distinguished-oracle entry in the observed log is exactly the replacement.

theorem OracleComp.replayRunWithTraceValue_mem_support_replayFirstRun {ι : Type} {spec : OracleSpec ι} {α : Type} [spec.DecidableEq] (main : OracleComp spec α) (i : ι) (trace : spec.QueryLog) (forkQuery : ℕ) (replacement : spec.Range i) {z : α × ReplayForkState spec i} (hz : z ∈ support (main.replayRunWithTraceValue i trace forkQuery replacement)) : (z.1, z.2.observed) ∈ support main.replayFirstRun

Every replay run can be realized as a logged run with the same observed transcript.

theorem OracleComp.isTotalQueryBound_replayRunWithTraceValue {ι : Type} {spec : OracleSpec ι} {α : Type} [spec.DecidableEq] (main : OracleComp spec α) (n : ℕ) (hmain : main.IsTotalQueryBound n) (i : ι) (trace : spec.QueryLog) (forkQuery : ℕ) (replacement : spec.Range i) : (main.replayRunWithTraceValue i trace forkQuery replacement).IsTotalQueryBound n

Replay does not increase the total number of oracle queries. If main makes at most n queries, then replayRunWithTraceValue main i trace forkQuery replacement also makes at most n queries.

Reduces to IsTotalQueryBound.simulateQ_run_of_step with replayOracle_step_isTotalQueryBound supplying the per-step bound of 1.

theorem OracleComp.cf_eq_of_mem_support_forkReplay {ι : Type} {spec : OracleSpec ι} {α : Type} [spec.DecidableEq] [(i : ι) → SampleableType (spec.Range i)] [unifSpec ⊂ₒ spec] (main : OracleComp spec α) (qb : ι → ℕ) (i : ι) (cf : α → Option (Fin (qb i + 1))) (x₁ x₂ : α) (h : some (x₁, x₂) ∈ support (main.forkReplay qb i cf)) : ∃ (s : Fin (qb i + 1)), cf x₁ = some s ∧ cf x₂ = some s

If forkReplay succeeds, both runs agree on the selected fork index.

theorem OracleComp.probEvent_forkReplay_fst_eq_probEvent_pair {ι : Type} {spec : OracleSpec ι} {α : Type} [spec.DecidableEq] [spec.Fintype] [spec.Inhabited] [(i : ι) → SampleableType (spec.Range i)] [unifSpec ⊂ₒ spec] (main : OracleComp spec α) (qb : ι → ℕ) (i : ι) (cf : α → Option (Fin (qb i + 1))) (s : Fin (qb i + 1)) : (probEvent (main.forkReplay qb i cf) fun (r : Option (α × α)) => Option.map (cf ∘ Prod.fst) r = some (some s)) = probEvent (main.forkReplay qb i cf) fun (r : Option (α × α)) => Option.map (Prod.map cf cf) r = some (some s, some s)

On forkReplay support, first-projection success equals the pair-style success event. This mirrors probEvent_seededFork_fst_eq_probEvent_pair for the replay fork.

Helper lemmas for le_probOutput_forkReplay

The pointwise replay bound is proved by the same three-step decomposition used for le_probOutput_seededFork:

1. probOutput_collisionReplay_le_main_div (replay analogue of probOutput_collision_le_main_div): bounds the probability that the uniformly sampled replacement u collides with the logged answer at the s-th i-query of the first run. The bound is Pr[cf <$> main = some s] / h where h = |spec.Range i|. Proof is purely about the replayFirstRun marginal: for any fixed v, Pr[u = v | u ← uniform] = 1/h.

2. noGuardReplayComp_le_forkReplay_add_collisionReplay (replay analogue of hNoGuardLeAdd): a structural inequality saying that the unrestricted "no-guard" composition (which always runs the second pass and inspects both projections of cf) is dominated by the genuine forkReplay success event plus the collision event. Proof is pointwise on (x₁, log)-pairs from replayFirstRun.

3. sq_probOutput_main_le_noGuardReplayComp (replay analogue of sq_probOutput_main_le_noGuardComp): the Jensen / Cauchy-Schwarz step. Squares the probability that the first run satisfies cf x₁ = some s and bounds it by the no-guard joint success probability. This is the deepest piece: it requires a replay-side analogue of seededOracle.tsum_probOutput_generateSeed_weight_takeAtIndex, stating that averaging over the full first-run log is equal to averaging over the "log truncated at the s-th i-query, then completed with a fresh uniform answer plus live tail samples".

def OracleComp.CfReachable {ι : Type} {spec : OracleSpec ι} {α : Type} [spec.DecidableEq] (main : OracleComp spec α) (qb : ι → ℕ) (i : ι) (cf : α → Option (Fin (qb i + 1))) : Prop

Reachability hypothesis on the fork-index selector cf: whenever the first run of main outputs x and the recorded log is log, every selected fork index s = cf x actually corresponds to an i-query in log (i.e. the s-th i-query exists in the log). This is needed for the replay forking lemma because, unlike the seeded variant, forkReplay's second run cannot fork at a position the first run never reached. In FiatShamir-style applications cf extracts the index of a recorded query, so this property holds by construction.

Replay state-correctness invariant

The next group of lemmas establishes that when main is replayed against a log it itself produced and the fork index is reachable in that log, the second run reaches the fork query without mismatching the prefix. The proof has three parts:

1. replayOracle_preservesConsumed (per-step) and replayRun_preservesConsumed (full simulation): once forkConsumed = true ∧ mismatch = false holds at some point, both flags stay set for the remainder of the run.
2. replayRun_state_correct_aux: a coupled inductive invariant over main showing that, starting from a state coupled to a partial first run with enough remaining i-queries to hit the fork, the simulation reaches forkConsumed = true with mismatch = false.
3. replayRunWithTraceValue_state_correct: the user-facing corollary obtained by instantiating the auxiliary invariant at the initial replay state.

theorem OracleComp.replayRunWithTraceValue_state_correct {ι : Type} {spec : OracleSpec ι} {α : Type} [spec.DecidableEq] (main : OracleComp spec α) (qb : ι → ℕ) (i : ι) (cf : α → Option (Fin (qb i + 1))) {x₁ : α} {log : spec.QueryLog} (hlog : (x₁, log) ∈ support main.replayFirstRun) {s : Fin (qb i + 1)} (hcf : cf x₁ = some s) (hreach : main.CfReachable qb i cf) (u : spec.Range i) {q : α × ReplayForkState spec i} (hq : q ∈ support (main.replayRunWithTraceValue i log (↑s) u)) : q.2.mismatch = false ∧ q.2.forkConsumed = true

Replay correctness invariant: starting from a logged first run of main whose log already records an i-query at position ↑s, replaying main against that log with substitution at the fork query always reaches the fork (so forkConsumed = true and mismatch = false on every output state).

This is the user-facing corollary of replayRun_state_correct_aux, instantiated at the initial replay state produced by ReplayForkState.init. The invariant is used in the replay forking lemma to argue that the no-guard composition cannot succeed via a state-failure path that forkReplay would reject.

noncomputable def OracleComp.noGuardReplayComp {ι : Type} {spec : OracleSpec ι} {α : Type} [spec.DecidableEq] [(i : ι) → SampleableType (spec.Range i)] [unifSpec ⊂ₒ spec] (main : OracleComp spec α) (qb : ι → ℕ) (i : ι) (cf : α → Option (Fin (qb i + 1))) (s : Fin (qb i + 1)) : OracleComp spec (Option (Option (Fin (qb i + 1)) × Option (Fin (qb i + 1))))

The "no-guard" replay composition: run main with logging, sample u, then run main a second time with the replay oracle (replaying log up to the s-th i-query and substituting u there). Always returns the pair of cf-projections, with no guards. This is the replay analogue of the noGuardComp used in sq_probOutput_main_le_noGuardComp for the seeded fork.

noncomputable def OracleComp.collisionReplayComp {ι : Type} {spec : OracleSpec ι} {α : Type} [spec.DecidableEq] [(i : ι) → SampleableType (spec.Range i)] [unifSpec ⊂ₒ spec] (main : OracleComp spec α) (qb : ι → ℕ) (i : ι) (cf : α → Option (Fin (qb i + 1))) (s : Fin (qb i + 1)) : OracleComp spec (Option (Fin (qb i + 1)))

The "collision" replay composition: run main with logging, sample u, and return cf x₁ only when u coincides with the logged answer at the s-th i-query. This is the replay analogue of collisionComp used in the seeded forking proof.

theorem OracleComp.le_probOutput_forkReplay {ι : Type} {spec : OracleSpec ι} {α : Type} [spec.DecidableEq] [spec.Fintype] [spec.Inhabited] [(i : ι) → SampleableType (spec.Range i)] [unifSpec ⊂ₒ spec] [unifSpec.LawfulSubSpec spec] (main : OracleComp spec α) (qb : ι → ℕ) (i : ι) (cf : α → Option (Fin (qb i + 1))) (hreach : main.CfReachable qb i cf) (s : Fin (qb i + 1)) : have h := ↑(Fintype.card (spec.Range i)); Pr[= some s | cf <$> main] ^ 2 - Pr[= some s | cf <$> main] / h ≤ probEvent (main.forkReplay qb i cf) fun (r : Option (α × α)) => Option.map (cf ∘ Prod.fst) r = some (some s)

Key pointwise replay lower bound. This is the replay analogue of le_probOutput_seededFork.

The summed (aggregated) version is the replay analogue of Firsov-Janku's pr_fork_success in fsec/proof/Forking.ec:1175. The quantitative argument decomposes into:

1. pr_split [Forking.ec:410]: factor out the acc · h⁻¹ collision term.
2. pr_succ_resp_eq [Forking.ec:480]: exchange symmetry of the two replay answers.
3. pr_fork_specific [Forking.ec:1115]: pointwise Pr[success at s]² ≤ Pr[fork at s].
4. square_sum [Forking.ec:1148]: Jensen / Cauchy-Schwarz Σ aⱼ² ≥ (Σ aⱼ)² / Q.

In Lean the analogous pointwise bound corresponds to step (3) combined with (1) and is structurally similar to the seed-based le_probOutput_seededFork proof in VCVio/CryptoFoundations/SeededFork.lean, with replayFirstRun/replayRunWithTraceValue playing the role of generateSeed/seededOracle and QueryLog.takeBeforeFork-style slicing replacing QuerySeed.takeAtIndex.

The proof reduces to three helper lemmas: probOutput_collisionReplay_le_main_div, sq_probOutput_main_le_noGuardReplayComp, and noGuardReplayComp_le_forkReplay_add_collisionReplay.

The hreach hypothesis (CfReachable) is needed because, unlike the seed-based version (where cf x = some s always implies the s-th query value is well-defined in the seed), in the replay setting, cf is computed from x independently from the actual queries made by the run that produced it. The hypothesis captures the natural condition that the fork point s chosen by cf always corresponds to a query that was actually issued.

Currently conditional on the two prefix-faithfulness sorrys feeding sq_probOutput_main_le_noGuardReplayComp: evalDist_uniform_bind_fst_replayRunWithTraceValue_takeBeforeForkAt (induction on main) and tsum_probOutput_replayFirstRun_weight_takeBeforeForkAt (weighted-averaging induction). Downstream consumers (probOutput_none_forkReplay_le, le_probEvent_isSome_forkReplay, Fork.replayForkingBound, euf_nma_bound, euf_cma_bound) inherit this conditionality until both faithfulness lemmas are discharged.

theorem OracleComp.forkReplay_precondition_le_one {ι : Type} {spec : OracleSpec ι} {α : Type} [spec.Fintype] [spec.Inhabited] (main : OracleComp spec α) (qb : ι → ℕ) (i : ι) (cf : α → Option (Fin (qb i + 1))) : (have acc := ∑ s : Fin (qb i + 1), Pr[= some s | cf <$> main]; have h := ↑(Fintype.card (spec.Range i)); have q := qb i + 1; acc * (acc / ↑q - h⁻¹)) ≤ 1

The replay-fork precondition is itself bounded by 1. This mirrors seededFork_precondition_le_one; the statement is independent of the fork mechanism.

theorem OracleComp.probOutput_none_forkReplay_le {ι : Type} {spec : OracleSpec ι} {α : Type} [spec.DecidableEq] [spec.Fintype] [spec.Inhabited] [(i : ι) → SampleableType (spec.Range i)] [unifSpec ⊂ₒ spec] [unifSpec.LawfulSubSpec spec] (main : OracleComp spec α) (qb : ι → ℕ) (i : ι) (cf : α → Option (Fin (qb i + 1))) (hreach : main.CfReachable qb i cf) : have acc := ∑ s : Fin (qb i + 1), Pr[= some s | cf <$> main]; have h := ↑(Fintype.card (spec.Range i)); have q := qb i + 1; Pr[= none | main.forkReplay qb i cf] ≤ 1 - acc * (acc / ↑q - h⁻¹)

Replay fork failure probability bound. This mirrors probOutput_none_seededFork_le; the proof structure is identical, substituting the pointwise replay lower bound le_probOutput_forkReplay for its seed-based analogue. The hreach hypothesis is threaded through from le_probOutput_forkReplay.

Currently conditional on the two B1 prefix-faithfulness sorrys (transitively via le_probOutput_forkReplay → sq_probOutput_main_le_noGuardReplayComp).

theorem OracleComp.le_probEvent_isSome_forkReplay {ι : Type} {spec : OracleSpec ι} {α : Type} [spec.DecidableEq] [spec.Fintype] [spec.Inhabited] [(i : ι) → SampleableType (spec.Range i)] [unifSpec ⊂ₒ spec] [unifSpec.LawfulSubSpec spec] (main : OracleComp spec α) (qb : ι → ℕ) (i : ι) (cf : α → Option (Fin (qb i + 1))) (hreach : main.CfReachable qb i cf) : (have acc := ∑ s : Fin (qb i + 1), Pr[= some s | cf <$> main]; have h := ↑(Fintype.card (spec.Range i)); have q := qb i + 1; acc * (acc / ↑q - h⁻¹)) ≤ probEvent (main.forkReplay qb i cf) fun (r : Option (α × α)) => r.isSome = true

Packaged replay forking theorem. This is the replay analogue of le_probEvent_isSome_seededFork, derived from probOutput_none_forkReplay_le and forkReplay_precondition_le_one by the same 1 - · conversion used in le_probEvent_isSome_seededFork. The hreach hypothesis is threaded through.

Currently conditional on the two B1 prefix-faithfulness sorrys (transitively via probOutput_none_forkReplay_le → le_probOutput_forkReplay → sq_probOutput_main_le_noGuardReplayComp).

theorem OracleComp.forkReplay_success_log_props {ι : Type} {spec : OracleSpec ι} {α : Type} [spec.DecidableEq] [(i : ι) → SampleableType (spec.Range i)] [unifSpec ⊂ₒ spec] (main : OracleComp spec α) (qb : ι → ℕ) (i : ι) (cf : α → Option (Fin (qb i + 1))) {x₁ x₂ : α} (h : some (x₁, x₂) ∈ support (main.forkReplay qb i cf)) : ∃ (log₁ : spec.QueryLog) (log₂ : spec.QueryLog) (s : Fin (qb i + 1)), (x₁, log₁) ∈ support main.replayFirstRun ∧ (x₂, log₂) ∈ support main.replayFirstRun ∧ cf x₁ = some s ∧ cf x₂ = some s ∧ QueryLog.getQueryValue? log₁ i ↑s ≠ QueryLog.getQueryValue? log₂ i ↑s ∧ ∃ (replacement : spec.Range i) (st : ReplayForkState spec i), (x₂, st) ∈ support (main.replayRunWithTraceValue i log₁ (↑s) replacement) ∧ st.observed = log₂ ∧ st.mismatch = false ∧ st.forkConsumed = true ∧ ∀ n < st.cursor, QueryLog.inputAt? log₂ n = QueryLog.inputAt? log₁ n

Structural success facts for forkReplay: both outputs come from logged runs of main, share the same selected fork index, differ at the selected distinguished-oracle answer, and the second run is witnessed by a replay state whose observed log agrees with the first-run log on the replayed prefix.

This mirrors Firsov-Janku's success_log_props at fsec/proof/Forking.ec:1373. The Lean proof is library-native: it unfolds forkReplay with mem_support_bind_iff, then consumes the already-proved support-level lemmas replayRunWithTraceValue_mem_support_replayFirstRun, replayRunWithTraceValue_prefix_input_eq, and replayRunWithTraceValue_getQueryValue?_observed_eq_replacement. No procedural while-loop invariant is needed; the replacement invariant ReplayReplacementInvariant is established pointwise by induction on the replay oracle.

theorem OracleComp.forkReplay_propertyTransfer {ι : Type} {spec : OracleSpec ι} {α : Type} [spec.DecidableEq] [(i : ι) → SampleableType (spec.Range i)] [unifSpec ⊂ₒ spec] (main : OracleComp spec α) (qb : ι → ℕ) (i : ι) (cf : α → Option (Fin (qb i + 1))) (P_out : α → spec.QueryLog → Prop) (hP : ∀ {x : α} {log : spec.QueryLog}, (x, log) ∈ support main.replayFirstRun → P_out x log) {x₁ x₂ : α} (h : some (x₁, x₂) ∈ support (main.forkReplay qb i cf)) : ∃ (log₁ : spec.QueryLog) (log₂ : spec.QueryLog) (s : Fin (qb i + 1)), cf x₁ = some s ∧ cf x₂ = some s ∧ P_out x₁ log₁ ∧ P_out x₂ log₂ ∧ QueryLog.getQueryValue? log₁ i ↑s ≠ QueryLog.getQueryValue? log₂ i ↑s

Replay property transfer: any postcondition that holds for every logged run of main holds for both outputs of a successful replay fork, together with the common selected fork index and the fact that the distinguished answers differ at that index.

This mirrors Firsov-Janku's property_transfer at fsec/proof/Forking.ec:1351, combining fst_run_prop with the shared-prefix facts established by success_log_props.