refactor(CryptoFoundations): derive replay forking from PolyFun contexts

[dtumad]

Summary

Recasts replay-based forking as a probability argument over PolyFun's typed Cursor occurrence contexts. Structural program decomposition, shared-prefix wiring, completion, and fixed/dynamic forking now live in PolyFun; VCVio retains the oracle-specific erasure bridge and the collision/probability estimates.

The former companion stack has merged:

• PolyFun Cursor: #43
• PolyFun occurrence/fork: #39
• exact PolyFun pin: 97a262ce2ba7513448b76635e1f6a07f61f40de5

This branch is rebased on current VCVio main and ports VCVio to Lean/Mathlib 4.32. It pins the validated Loom2 4.32 compatibility commit 2f65f311fae959c302586b07aa45390999b935d4.

Replay proof structure

• replayFirstPath exposes PolyFun execution paths while replayPathResult erases them to the output/query-log view used by cryptographic applications.
• PathCfReachable states reachability at the semantic path level and follows from the existing support-level reachability condition.
• contextForkWitness and contextFork use dynamically selected Cursor.ForkViews rather than replay cursors, flat-log indices, or a bespoke replay oracle.
• guarded pair and collision experiments isolate the direct probability comparison from the generic forking program.
• the square-minus-collision aggregation establishes the final forking bound.
• Fiat–Shamir reads the common occurrence prefix directly to prove target agreement and transfers the generic bound to the signature experiment.

This removes ReplayForkStdDo.lean and the remaining replay-oracle/pathway machinery. ReplayFork.lean is 1,332 lines and contains no replayOracle, forkReplay, replay cursor, or pathway definitions.

Lean 4.32 compatibility

• updates Lean and Mathlib to v4.32.0;
• pins merged PolyFun Cursor/Fork and Loom2 4.32 by exact commit;
• migrates the old Path/refork names to Cursor/fork;
• repairs the small number of Lean 4.32 elaboration and typeclass changes in existing examples, Merkle code, and query-counting instances;
• clears the repository's non-sorry warning budget without linter suppression;
• makes transformer and oracle universes explicit where Lean 4.32's universe linter exposed anonymous max metavariables.

No cryptographic theorem statement was weakened, and no sorry, admit, axiom, unsafe declaration, or new trust escape was added.

Review guide

1. VCVio/CryptoFoundations/ReplayFork.lean: structural erasure bridge and probability core.
2. VCVio/CryptoFoundations/FiatShamir/Sigma/Fork.lean: shared-prefix application to Fiat–Shamir.
3. VCVio/CryptoFoundations/FiatShamir/Sigma/Reductions.lean: final reduction call site.
4. Commit 01c57c0e: FreeM compatibility.
5. Commit d9d0ab68: proof cutover to typed occurrence contexts.
6. Commit fc7cda93: Lean 4.32, merged Cursor/Fork API, exact dependency pins, and compatibility cleanup.

Validation

• full lake build (2,979 jobs)
• exact CI warning-budget checker: no repository non-sorry warnings
• lake build VCVio.CryptoFoundations.ReplayFork
• lake build VCVio.CryptoFoundations.FiatShamir.Sigma.Fork VCVio.CryptoFoundations.FiatShamir.Sigma.Reductions
• lake env lean VCVioTest/Smoke.lean
• lake env lean VCVioTest/MerkleTreeBatch.lean
• lake exe slhdsa_kat
• lake exe slhdsa_c13_kat
• lake exe lint-style ToMathlib VCVio FFI LatticeCrypto Examples VCVioWidgets Interop
• all mk_all --check library-import gates
• agent documentation and Interop TCB-isolation checks
• git diff --check

The dormant Interop target remains excluded, as documented on main, pending independent Lean 4.32 ports of its upstream Hax/Aeneas dependencies.

[github-actions]

🤖 PR Summary

ℹ️ This PR modifies 2 file(s) under ToMathlib/ — consider whether a corresponding upstream PR is needed.

Refactor: Derive Replay Forking from PolyFun Contexts

This refactoring recasts replay‑based forking as a probability argument over PolyFun's typed Cursor occurrence contexts. The former ReplayForkStdDo.lean and its replay‑oracle/pathway machinery are removed; ReplayFork.lean (1,332 lines) now contains no replayOracle, forkReplay, replay cursor, or pathway definitions.

The core change concentrates in:

Mathematical Formalization

• VCVio/CryptoFoundations/ReplayFork.lean: Structural erasure bridge and probability core. Key definitions introduced:
  • replayFirstPath – exposes PolyFun execution paths.
  • replayPathResult – erases paths to the output/query‑log view.
  • PathCfReachable – states path‑level reachability, derived from support‑level reachability.
  • contextForkWitness, contextFork – use dynamically selected Cursor.ForkViews (not replay cursors, flat‑log indices, or bespoke replay oracle).
  • Guarded pair and collision experiments for probability comparison.
  • Square‑minus‑collision aggregation for the final forking bound.
• VCVio/CryptoFoundations/FiatShamir/Sigma/Fork.lean: Shared‑prefix application to Fiat–Shamir; reads common occurrence prefix directly to prove target agreement and transfers the generic bound.
• VCVio/CryptoFoundations/FiatShamir/Sigma/Reductions.lean: Final reduction call site.

Infrastructure / CI

• Lean 4.32 compatibility: Updated toolchain from v4.31.0 to v4.32.0 (lean-toolchain), Mathlib pin to v4.32.0 (lakefile.lean). PolyFun dependency pinned to commit 97a262ce2ba7513448b76635e1f6a07f61f40de5; Loom2 pinned to 2f65f311fae959c302586b07aa45390999b935d4.
• Dependency changes: ReplayForkStdDo module removed from VCVio.lean. VCVioTest/MerkleTreeBatch.lean converts six def declarations to theorems.
• CI updates: AGENTS.md bumps CI timed build to exclude Interop (dormant pending Lean 4.32 port of Hax/Aeneas). docs/agents/interop.md updated accordingly.
• No repository non‑sorry warnings remain; no sorry, admit, axiom, unsafe declaration, or new trust escape introduced.

Universe Polymorphism & Reducibility Tweaks

• LatticeCrypto/MLDSA/Arithmetic.lean: RoundingOps abbreviation pinned to explicit universe .{0, 0}.
• LatticeCrypto/Ring/Rounding.lean: RoundingOps structure made universe‑polymorphic (added universe u v).
• LatticeCrypto/MLDSA/Concrete/NTT.lean, LatticeCrypto/MLKEM/Concrete/NTT.lean: concreteNTTRingLaws changed from @[reducible] noncomputable def to bare theorem.
• LatticeCrypto/MLDSA/Concrete/Rounding.lean: BalancedDecomp.ofApproved changed from private def to private theorem.
• ToMathlib/Control/Monad/Commutative.lean: CommutativeAt.bind_comm made universe‑explicit; Set.monadComm changed from @[reducible] def to theorem.
• ToMathlib/OrderEnrichedCategory.lean: Explicit universe parameters added to MonoidalCategory (Preord) and PreordEnrichedCategory instances.

Proof Mechanics (Examples)

• Examples/: Proof‑mechanical adaptations to API changes (e.g., explicit (P := ...) argument in PFunctor.FreeM.lift calls; library lemma replacements; simplifications using new simp lemmas). No new sorry/admit.
• VCVioWidgets/OpenSyntax/Panel.lean: Renamed GraphDisplay to ForceGraphDisplay for ProofWidgets API consistency. No logical changes.

Note: The PR body is accurate and complete; per‑file summaries confirm no sorry/admit were added in any changed file. The cumulative diff aligns with the stated goal: removing bespoke replay‑forking machinery and replacing it with PolyFun Cursor‑based forking, while updating all dependencies and proofs for Lean 4.32 compatibility.

---

Statistics

Metric	Count
📝 Files Changed	65
✅ Lines Added	1719
❌ Lines Removed	3612

---

Lean Declarations

✏️ Removed: 99 declaration(s)

VCVio/CryptoFoundations/FiatShamir/Sigma/Fork.lean (1)

• lemma runTrace_target_eq_of_mem_forkReplay

VCVio/CryptoFoundations/ReplayFork.lean (89)

• def ReplayPrefixInvariant [spec.DecidableEq] (i : ι) (st : ReplayForkState spec i) : Prop
• def ReplayReplacementInvariant [spec.DecidableEq] (i : ι) (st : ReplayForkState spec i) :
• def forkReplay [spec.DecidableEq] (main : OracleComp spec α)
• def forkReplayWithTraceValue [spec.DecidableEq] (main : OracleComp spec α)
• def inputAt? (log : QueryLog spec) (n : Nat) : Option ι
• def markMismatch (st : ReplayForkState spec i) : ReplayForkState spec i
• def nextEntry? (st : ReplayForkState spec i) :
• def noteObserved (st : ReplayForkState spec i) (t : ι) (u : spec.Range t) :
• def replayOracle [spec.DecidableEq] (i : ι) :
• def replayRunWithTraceValue [spec.DecidableEq] (main : OracleComp spec α) (i : ι)
• def takeBeforeForkAt [spec.DecidableEq] :
• lemma ReplayForkState.noteObserved_live_iff {i : ι}
• lemma countQ_takeBeforeForkAt_eq [spec.DecidableEq] (log : QueryLog spec) (i : ι) (s : ℕ)
• lemma countQ_takeBeforeForkAt_le [spec.DecidableEq]
• lemma evalDist_fst_map_simulateQ_replayOracle_of_live [spec.DecidableEq] [IsUniformSpec spec]
• lemma forkReplayWithTraceValue_eq_none_of_cf_none
• lemma fst_map_replayFirstRun (main : OracleComp spec α) :
• lemma fst_map_simulateQ_replayOracle_of_live [spec.DecidableEq]
• lemma getQueryValue?_takeBeforeForkAt_self [spec.DecidableEq]
• lemma init (trace : QueryLog spec) (forkQuery : Nat) (replacement : spec.Range i) :
• lemma inputAt?_logQuery_of_lt (log : QueryLog spec) (t : ι) (u : spec.Range t) {n : Nat}
• lemma inputAt?_logQuery_self (log : QueryLog spec) (t : ι) (u : spec.Range t) :
• lemma probEvent_fst_replayFirstRun [IsUniformSpec spec]
• lemma probOutput_fst_map_replayFirstRun [IsUniformSpec spec]
• lemma replayRunWithTraceValue_forkConsumed_imp_last_input [IsUniformSpec spec] [spec.DecidableEq]
• lemma replayRunWithTraceValue_forkConsumed_imp_prefix_count [IsUniformSpec spec] [spec.DecidableEq]
• lemma replayRunWithTraceValue_forkQuery_eq [spec.DecidableEq] [IsUniformSpec spec]
• lemma replayRunWithTraceValue_getQueryValue?_observed_eq_replacement
• lemma replayRunWithTraceValue_prefix_getElem?_eq [spec.DecidableEq] [IsUniformSpec spec]
• lemma replayRunWithTraceValue_prefix_input_eq [IsUniformSpec spec] [spec.DecidableEq]
• lemma replayRunWithTraceValue_replacement_eq [spec.DecidableEq] [IsUniformSpec spec]
• lemma replayRunWithTraceValue_trace_eq [spec.DecidableEq] [IsUniformSpec spec]
• lemma takeBeforeForkAt_cons_of_ne [spec.DecidableEq]
• lemma takeBeforeForkAt_cons_self_succ [spec.DecidableEq]
• lemma takeBeforeForkAt_cons_self_zero [spec.DecidableEq]
• lemma takeBeforeForkAt_nil [spec.DecidableEq] (i : ι) (s : ℕ) :
• lemma takeBeforeForkAt_of_getQ_length_le [spec.DecidableEq] (log : QueryLog spec) (i : ι) (s : ℕ)
• lemma takeBeforeForkAt_prefix [spec.DecidableEq]
• private lemma drop_cursor_succ_aux (i : ι) (st : ReplayForkState spec i) :
• private lemma evalDist_uniform_bind_fst_replayRunWithTraceValue_takeBeforeForkAt
• private lemma fst_map_replayOracle_run_live_bind_aux [spec.DecidableEq]
• private lemma nextEntry?_eq_drop_head_aux (i : ι) (st : ReplayForkState spec i) :
• private lemma noGuardReplayComp_le_forkReplay_add_collisionReplay [IsUniformSpec spec]
• private lemma probOutput_bind_liftComp_const [IsUniformSpec spec] {β : Type}
• private lemma probOutput_collisionReplay_le_main_div [IsUniformSpec spec]
• private lemma probOutput_map_fst_bind_liftComp_congr [IsUniformSpec spec] {β σ : Type}
• private lemma probOutput_uniformGuard_le_aux [IsUniformSpec spec] (qb : ι → ℕ) (i : ι)
• private lemma probOutput_uniform_bind_fst_replayRunWithTraceValue_takeBeforeForkAt
• private lemma replayOracle_observed_eq_logQuery [spec.DecidableEq]
• private lemma replayOracle_preservesConsumed
• private lemma replayOracle_preservesPrefixInvariant_markMismatch_aux [spec.DecidableEq]
• private lemma replayOracle_run_fork_fires [spec.DecidableEq]
• private lemma replayOracle_run_lockstep_i_pre_fork [spec.DecidableEq]
• private lemma replayOracle_run_lockstep_ne_i [spec.DecidableEq]
• private lemma replayOracle_run_mismatch_ne [spec.DecidableEq]
• private lemma replayOracle_run_nextEntry_none [spec.DecidableEq]
• private lemma replayOracle_step_isTotalQueryBound
• private lemma replayReplacementInvariant_markMismatch_noteObserved_aux [spec.DecidableEq]
• private lemma replayRunWithTraceValue_immutable_params [spec.DecidableEq] [IsUniformSpec spec]
• private lemma sq_probOutput_main_le_noGuardReplayComp [IsUniformSpec spec]
• private lemma sum_probEvent_forkReplay_le_tsum_some [IsUniformSpec spec]
• private lemma tsum_probOutput_replayFirstRun_weight_takeBeforeForkAt [IsUniformSpec spec]
• private noncomputable def collisionReplayComp
• private noncomputable def noGuardReplayComp
• private theorem cf_eq_of_mem_support_forkReplay
• private theorem evalDist_uniform_bind_fst_simulateQ_replayOracle_run_coupled_aux
• private theorem forkReplay_precondition_le_one [IsUniformSpec spec]
• private theorem fst_map_replayRunWithTraceValue_nil [spec.DecidableEq]
• private theorem fst_map_replayRunWithTraceValue_query_bind_cons_ne [spec.DecidableEq]
• private theorem fst_map_replayRunWithTraceValue_query_bind_cons_self_succ
• private theorem fst_map_simulateQ_replayOracle_both_noteObserved_aux [spec.DecidableEq]
• private theorem fst_map_simulateQ_replayOracle_state_equiv [spec.DecidableEq]
• private theorem isTotalQueryBound_replayRunWithTraceValue [IsUniformSpec spec]
• private theorem le_probOutput_forkReplay [IsUniformSpec spec]
• private theorem probEvent_forkReplay_fst_eq_probEvent_pair [IsUniformSpec spec]
• private theorem probOutput_none_forkReplay_le [IsUniformSpec spec]
• private theorem replayRun_mem_support_replayFirstRun_append [spec.DecidableEq]
• private theorem replayRun_preservesConsumed
• private theorem replayRun_state_correct_aux
• protected lemma replayOracle_immutable_params [spec.DecidableEq]
• protected lemma replayOracle_preservesPrefixInvariant [spec.DecidableEq]
• protected lemma replayOracle_preservesReplacementInvariant [spec.DecidableEq]
• theorem forkReplay_propertyTransfer [IsUniformSpec spec]
• theorem forkReplay_success_log_props [IsUniformSpec spec]
• theorem le_probEvent_isSome_forkReplay [IsUniformSpec spec]
• theorem replayRunWithTraceValue_mem_support_replayFirstRun [spec.DecidableEq]
• theorem replayRunWithTraceValue_preservesPrefixInvariant [spec.DecidableEq] [IsUniformSpec spec]
• theorem replayRunWithTraceValue_preservesReplacementInvariant
• theorem replayRunWithTraceValue_state_correct

VCVio/CryptoFoundations/ReplayForkStdDo.lean (9)

• example (i t₁ t₂ : ι) :
• example (i t₁ t₂ t₃ : ι) :
• example {α : Type} (main : OracleComp spec α) (i : ι) (trace : QueryLog spec)
• theorem replayOracle_triple_immutable (i t : ι) (st₀ : ReplayForkState spec i) :
• theorem replayOracle_triple_prefix (i t : ι) :
• theorem replayOracle_triple_replacement (i t : ι) :
• theorem simulateQ_replayOracle_preserves_immutable {α : Type}
• theorem simulateQ_replayOracle_preserves_prefix {α : Type}
• theorem simulateQ_replayOracle_preserves_replacement {α : Type}

✏️ Added: 72 declaration(s)

VCVio/CryptoFoundations/FiatShamir/Sigma/Fork.lean (1)

• lemma runTrace_target_eq_of_mem_contextFork

VCVio/CryptoFoundations/FiatShamir/Sigma/Stateful/Hops.lean (4)

• private lemma cmaRealSignPublicDist_none
• private lemma cmaRealSignPublicDist_some
• private lemma cmaSimSignPublicDist_none
• private lemma cmaSimSignPublicDist_some

VCVio/CryptoFoundations/MerkleTree/Vector/Defs.lean (4)

• def Cache.base (leaves : List.Vector α 1) : Cache α 0
• lemma Cache.base_zero (leaves : List.Vector α 1) : Cache.base α leaves 0 = leaves
• theorem getRoot_base (leaves : List.Vector α 1) :
• theorem getRoot_zero {m : Type _ → Type _} [Monad m] [LawfulMonad m]

VCVio/CryptoFoundations/ReplayFork.lean (56)

• @[simp] private theorem acceptContextForkWitness_eq_some
• @[simp] private theorem classifyForkView_isSome
• @[simp] private theorem collideForkView_eq_some
• @[simp] theorem contextForkWitness_outputs (main : OracleComp spec α) (qb : ι → ℕ) (i : ι)
• @[simp] theorem map_output_replayFirstPath (main : OracleComp spec α) :
• @[simp] theorem replayFirstPath_query_bind (t : spec.Domain)
• abbrev ContextForkWitness (main : OracleComp spec α) (qb : ι → ℕ) (i : ι)
• def PathCfReachable (main : OracleComp spec α) (qb : ι → ℕ) (i : ι)
• def contextFork (main : OracleComp spec α) (qb : ι → ℕ) (i : ι)
• def contextForkView (main : OracleComp spec α) (i : ι) (s : Nat) :
• def contextForkWitness (main : OracleComp spec α) (qb : ι → ℕ) (i : ι)
• def guardedContextFork (main : OracleComp spec α) (qb : ι → ℕ) (i : ι)
• def replayFirstPath (main : OracleComp spec α) :
• def replayPathResult (main : OracleComp spec α)
• lemma countQ_eq_occurrences [spec.DecidableEq] (log : QueryLog spec) (t : ι) :
• lemma getQueryValue?_append_self_at_countQ [spec.DecidableEq]
• lemma getQueryValue?_completion_path_eq_answer [spec.DecidableEq]
• lemma mem_support_replayFirstPath (main : OracleComp spec α)
• lemma replayPathResult_mem_support_replayFirstRun
• noncomputable def contextForkCollision (main : OracleComp spec α) (qb : ι → ℕ) (i : ι)
• noncomputable def contextForkPair (main : OracleComp spec α) (qb : ι → ℕ) (i : ι)
• private def acceptContextForkWitness
• private def classifyForkView
• private def collideForkView (main : OracleComp spec α) (qb : ι → ℕ) (i : ι)
• private def contextForkViewCollision (main : OracleComp spec α) (qb : ι → ℕ) (i : ι)
• private lemma sum_probEvent_contextFork_component_le_tsum_some
• private lemma tsum_some_eq_probEvent_isSome_contextFork
• private theorem classifyForkView_component_iff
• private theorem classifyForkView_component_ne
• private theorem classifyForkView_eq_some_iff
• private theorem map_completeFork_found_oracleComp
• private theorem mem_support_freeM_bind_iff {β γ : Type} (mx : OracleComp spec β)
• private theorem mem_support_freeM_map_iff
• private theorem mem_support_freeM_pure_iff {β : Type} (x y : β) :
• private theorem probEvent_classifyForkView_component_ne_eq_zero
• private theorem probEvent_classifyForkView_isSome_eq_zero_of_first_ne
• private theorem probEvent_freeM_bind_eq_tsum [IsProbabilitySpec spec]
• private theorem probEvent_freeM_map [IsProbabilitySpec spec]
• private theorem probEvent_freeM_pure [IsProbabilitySpec spec]
• private theorem splitAtValid_bind_completeFork_oracleComp
• private theorem splitAtValid_bind_complete_oracleComp
• theorem CfReachable.toPathCfReachable
• theorem contextFork_propertyTransfer [IsUniformSpec spec]
• theorem contextFork_success
• theorem le_probEvent_isSome_contextFork [IsUniformSpec spec]
• theorem map_replayPathResult_replayFirstPath (main : OracleComp spec α) :
• theorem not_cf_eq_of_valid_missing
• theorem probEvent_guardedContextFork_eq_contextFork_component
• theorem probOutput_contextForkCollision_le_main_div [IsUniformSpec spec]
• theorem probOutput_contextForkPair_le_guarded_add_collision [IsUniformSpec spec]
• theorem probOutput_contextForkViewCollision_le_collision [IsUniformSpec spec]
• theorem probOutput_contextForkViewCollision_le_main_div [IsUniformSpec spec]
• theorem sq_probOutput_main_le_contextForkPair [IsUniformSpec spec]
• theorem sq_sub_div_le_probEvent_guardedContextFork [IsUniformSpec spec]
• theorem sum_probEvent_guardedContextFork_le_isSome
• theorem sum_sq_sub_div_le_probEvent_guardedContextFork

VCVio/OracleComp/OracleComp.lean (7)

• def ofFreeM {α : Type w} (oa : PFunctor.FreeM spec.toPFunctor α) :
• def toFreeM {α : Type w} (oa : OracleComp spec α) :
• theorem ofFreeM_bind {α β : Type v}
• theorem ofFreeM_map {α β : Type v}
• theorem ofFreeM_pure {α : Type v} (x : α) :
• theorem ofFreeM_toFreeM {α : Type w} (oa : OracleComp spec α) :
• theorem toFreeM_ofFreeM {α : Type w}

✏️ Affected: 39 declaration(s) (line number changed)

• abbrev RoundingOps (alpha : ℕ) in LatticeCrypto/MLDSA/Arithmetic.lean moved from L131 to L131
• theorem concreteNTTRingLaws : NTTRingLaws concreteNTTRingOps where in LatticeCrypto/MLDSA/Concrete/NTT.lean moved from L270 to L270
• private theorem BalancedDecomp.ofApproved {p : Params} (hp : p.isApproved) : in LatticeCrypto/MLDSA/Concrete/Rounding.lean moved from L163 to L163
• theorem concreteNTTRingLaws : NTTRingLaws concreteNTTRingOps where in LatticeCrypto/MLKEM/Concrete/NTT.lean moved from L331 to L331
• @[simp] theorem CommutativeAt.bind_comm {m : Type u → Type v} [Monad m] [LawfulMonad m] in ToMathlib/Control/Monad/Commutative.lean moved from L64 to L64
• theorem Set.monadComm : Commutative Set where in ToMathlib/Control/Monad/Commutative.lean moved from L195 to L196
• abbrev PreordEnrichedCategory (C : Type u) in ToMathlib/OrderEnrichedCategory.lean moved from L144 to L144
• @[simp] theorem negligible_iff (f : ℕ → ℝ≥0∞) : in VCVio/CryptoFoundations/Asymptotics/Negligible.lean moved from L30 to L30
• private def incrementProcess : ProcessOver ℕ trivCtx in VCVio/Interaction/UC/StdDoBridge.lean moved from L177 to L177
• theorem ProcessOver.runSteps_succ {P : Type} (process : ProcessOver P Γ) in VCVio/Interaction/UC/StdDoBridge.lean moved from L109 to L109
• theorem ProcessOver.runSteps_zero {P : Type} (process : ProcessOver P Γ) in VCVio/Interaction/UC/StdDoBridge.lean moved from L104 to L104
• theorem runSteps_triple_preserves_invariant {P : Type} (process : ProcessOver P Γ) in VCVio/Interaction/UC/StdDoBridge.lean moved from L136 to L136
• protected theorem induction {α} {C : OracleComp spec α → Prop} in VCVio/OracleComp/OracleComp.lean moved from L169 to L206
• protected theorem inductionOn {α} {C : OracleComp spec α → Prop} in VCVio/OracleComp/OracleComp.lean moved from L145 to L182
• protected theorem inductionOnOptional {α} {C : OptionT (OracleComp spec) α → Prop} in VCVio/OracleComp/OracleComp.lean moved from L156 to L193
• protected theorem inductionOptional {α} {C : OptionT (OracleComp spec) α → Prop} in VCVio/OracleComp/OracleComp.lean moved from L177 to L214
• @[simp] lemma toPFunctor_add {ι : Type u} {ι' : Type u'} in VCVio/OracleComp/OracleSpec.lean moved from L100 to L100
• @[simp] lemma toPFunctor_mul {ι : Type u} {ι' : Type u'} in VCVio/OracleComp/OracleSpec.lean moved from L153 to L154
• protected theorem inductionOn {α} {C : ProbComp α → Prop} in VCVio/OracleComp/ProbComp.lean moved from L93 to L93
• def OracleSpec.loggingOracle {ι : Type u} {spec : OracleSpec.{u, u} ι} : in VCVio/OracleComp/QueryTracking/LoggingOracle.lean moved from L206 to L206
• def addReaderT {ι₁ : Type u} {ι₂ : Type v} in VCVio/OracleComp/SimSemantics/ReaderT/Basic.lean moved from L25 to L25
• def flattenReaderT {ι : Type u} {spec : OracleSpec.{u, v} ι} in VCVio/OracleComp/SimSemantics/ReaderT/Basic.lean moved from L47 to L47
• @[simp, grind =] lemma withBadFlag_apply_run {ι : Type u} {spec : OracleSpec.{u, v} ι} in VCVio/OracleComp/SimSemantics/StateT/Basic.lean moved from L119 to L119
• @[simp, grind =] lemma withBadUpdate_apply_run {ι : Type u} {spec : OracleSpec.{u, v} ι} in VCVio/OracleComp/SimSemantics/StateT/Basic.lean moved from L127 to L127
• def parallelStateT {ι₁ : Type u} {ι₂ : Type v} in VCVio/OracleComp/SimSemantics/StateT/Basic.lean moved from L61 to L61
• def piStateT {τ : Type} [DecidableEq τ] {ι : τ → Type v} in VCVio/OracleComp/SimSemantics/StateT/Basic.lean moved from L91 to L91
• def withBadFlag {ι : Type u} {spec : OracleSpec.{u, v} ι} in VCVio/OracleComp/SimSemantics/StateT/Basic.lean moved from L101 to L101
• def withBadUpdate {ι : Type u} {spec : OracleSpec.{u, v} ι} in VCVio/OracleComp/SimSemantics/StateT/Basic.lean moved from L110 to L110
• def parallelWriterT {ι₁ : Type u} {ι₂ : Type v} in VCVio/OracleComp/SimSemantics/WriterT/Basic.lean moved from L28 to L28
• def sigmaWriterT {τ : Type} [DecidableEq τ] {ι : τ → Type v} in VCVio/OracleComp/SimSemantics/WriterT/Basic.lean moved from L40 to L40
• theorem allNonempty : selectAll.anySelected = true in VCVioTest/MerkleTreeBatch.lean moved from L63 to L63
• theorem bothLeftSelected : selectBoth.get pairLeftIndex = true in VCVioTest/MerkleTreeBatch.lean moved from L149 to L149
• theorem firstNonempty : selectFirst.anySelected = true in VCVioTest/MerkleTreeBatch.lean moved from L53 to L53
• theorem firstSelected : selectFirst.get firstIndex = true in VCVioTest/MerkleTreeBatch.lean moved from L51 to L51
• theorem leftSelected : selectLeft.get pairLeftIndex = true in VCVioTest/MerkleTreeBatch.lean moved from L147 to L147
• theorem outerNonempty : selectOuter.anySelected = true in VCVioTest/MerkleTreeBatch.lean moved from L58 to L58
• theorem putativeRootsAgree : in VCVioTest/MerkleTreeBatch.lean moved from L159 to L159
• theorem selectedValuesDiffer : in VCVioTest/MerkleTreeBatch.lean moved from L154 to L154
• private def compTreeToGraph (tree : CompTree) : ForceGraphDisplay.Props in VCVioWidgets/OpenSyntax/Panel.lean moved from L262 to L262

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

Coverage Notes

• AI file summarization partially analyzed 1 file(s) because their individual diffs exceeded the per-file size budget. Statistics and Lean signal tracking still cover the full PR.

Partially Analyzed Files

• VCVio/CryptoFoundations/ReplayFork.lean (+1165/-2982)

---

📋 **Additional Analysis**

The diff upgrades the project from Lean 4.31 to 4.32, including updates to all dependencies (PolyFun, mathlib, loom2, batteries, proofwidgets, aesop, Qq, and several transitive deps), the toolchain, and various library configurations. It also contains many source-level adaptations to API changes that the dependencies' version bump entailed: rewrites from replayOracle/forkReplay to PolyFun's intrinsic contextFork/contextForkView in ReplayFork.lean, elimination of the per-file autoImplicit = false workaround, removal of the ReplayForkStdDo.lean file, and numerous small simp/rw adjustments across the codebase (e.g., bind_pure_comp → map_eq_bind_pure_comp, @[reducible] def … → theorem, universe annotations on QueryImpl combinators). The Interop target and its documentation remain dormant but are updated to reflect the new toolchain.

---

📄 **Per-File Summaries**

• AGENTS.md: The CI timed build list was updated to exclude the Interop library (now noted as 'dormant') while keeping VCVioWidgets in the set. The Lean toolchain and Mathlib version was bumped from v4.31.0 to v4.32.0.
• Examples/CommitmentScheme/Common.lean: In lemma probEvent_from_fresh_query_le_inv, the change tactic was updated to use an explicit P := (CMOracle M S C).toPFunctor argument when calling PFunctor.FreeM.lift, instead of passing (CMOracle M S C).query t directly. This adapts the proof to a change in the PFunctor.FreeM.lift API (likely requiring the parent functor to be specified as a named argument). No new definitions, theorems, or sorrys were introduced.
• Examples/CommitmentScheme/Hiding/LoggingBounds/Average.lean: The diff refactors run_simulateQ_hidingAvgComp_eq_bind lemma: replaces the earlier change block (which was a tautological equality stating two identical expressions are equal) with simp only [simulateQ_pure, StateT.run_pure, bind_pure_comp] followed by rfl. This simplifies the proof by applying the new rewrite rules simulateQ_pure, StateT.run_pure, and bind_pure_comp before concluding the goal. This change removes a dead (identity) equality and uses the existing simp lemmas to directly close the goal, aligning the proof with the library's current simplifier rules. No sorry or admit introduced.
• Examples/CommitmentScheme/Hiding/LoggingBounds/QuerySalt.lean: The diff updates four rw and change blocks in the proofs of wp_querySaltIndicator_prepend_eq_one, wp_querySaltIndicator_prepend_eq_of_ne, and wp_querySaltIndicator_cached_logging_cacheQuery_eq_of_no_other_salt_entrie. Two call sites of simulateQ_map now include an additional StateT.run_map rewrite. Two PFunctor.FreeM.lift calls are updated from the old (CMOracle M S C).query t argument to the new explicit syntax (P := (CMOracle M S C).toPFunctor) t, reflecting an API change in how the underlying PFunctor is passed.
• Examples/PRFTagReader/MultipleToHybrid/EagerSetup.lean: The proof of probOutput_uniformSample_fun_eval was restructured: the original rw chain using (probOutput_bind_eq_tsum _ _ _).symm followed by bind_pure and probOutput_uniformSample was replaced with a simpa block that applies bind_pure inside a call to probOutput_bind_eq_tsum with explicit arguments, then separately rewrites probOutput_uniformSample. The lemma's statement and the overall omit context remain unchanged.
• Examples/PRFTagReader/PRFReductions/IdealHandlers.lean: The proof of prfIdealExp_unlinkToMultiplePRFReduction_eq_run' was simplified by replacing a sequence of rw and change with simp on StateT.run'_eq, simulateQ_map, and StateT.run_map, followed by a single rw of simulateQ_multipleIdeal_collapse and a simp of Functor.map_map. Similarly, the proof of prfIdealExp_unlinkToSinglePRFReduction_eq_run' was simplified with the same pattern using simulateQ_singleIdeal_collapse. In simulateQ_prfIdeal_query_inr, the none case of the idealCacheStep case now additionally rewrites map_eq_bind_pure_comp after QueryImpl.withCaching_run_none.
• Examples/PRFTagReader/PRFReductions/Reductions.lean: In Reductions.lean, two theorems—prfRealExp_unlinkToMultiplePRFReduction_eq_unlinkMultipleExp and prfRealExp_unlinkToSinglePRFReduction_eq_unlinkSingleExp—were modified. Each proof previously ended with rfl; the diff replaces that with a block that rewrites using StateT.run'_eq, StateT.run'_eq, and map_eq_bind_pure_comp, then applies simp only [simulateQ_pure, bind_pure_comp] in place of the rfl step. No new theorems, definitions, or sorries are introduced; the change refines the closing reasoning of both existing equational proofs.
• Examples/PRGfromPRF.lean: The proof of lemma tvDist_seedOutputs_le_collision_gen is completed by adding three lines that fill the earlier rfl block. The new lines apply congr 1 to refine the goal, then use bind_congr and map_eq_bind_pure_comp to rewrite an equality between distributions, thereby closing the remaining subgoal.
• Examples/SimpleTwoServerPIR.lean: The proof of pirQuery'_eq_pirQuery is refactored to replace the custom List.forIn_mprod_yield_eq_foldlM bridge from ToMathlib.General with Lean's standard List.forIn_yield_eq_foldlM lemma. Two local lemmas ite_pure and ite_yield are added to normalize branchwise pure and ForInStep.yield terms into the form expected by that bridge. The comment above the theorem is updated to reflect these changes. The statement of the theorem itself is unchanged.
• LatticeCrypto/MLDSA/Arithmetic.lean: In LatticeCrypto/MLDSA/Arithmetic.lean, the RoundingOps abbreviation (line 131) was updated: the underlying LatticeCrypto.RoundingOps application now explicitly includes universe parameters .{0, 0} instead of relying on implicit universe inference. This change pins the abbreviation to the lowest universe, which can affect type‑checking by removing unwanted universe polymorphism.
• LatticeCrypto/MLDSA/Concrete/NTT.lean: The declaration concreteNTTRingLaws was changed from a @[reducible] noncomputable def to a theorem, with the same body. This modifies its reducibility and computational status: it will no longer be unfolded by simp and cannot be used where a computable definition is required, while still providing a proof of NTTRingLaws.
• LatticeCrypto/MLDSA/Concrete/Rounding.lean: In LatticeCrypto/MLDSA/Concrete/Rounding.lean, the BalancedDecomp.ofApproved constructor was changed from a private def to a private theorem (its signature remains otherwise identical). This change ensures the declaration is recognized by Lean as a theorem rather than a definition, which may affect how it is treated by the elaborator and in proofs, without altering its logical content or the statements it establishes.
• LatticeCrypto/MLKEM/Concrete/NTT.lean: The declaration concreteNTTRingLaws was changed from a @[reducible] noncomputable def to a bare theorem, removing the reducible and noncomputable attributes. This alters the reducibility and computational status of the proof bundle that asserts the concrete ML‑KEM NTT satisfies the NTTRingLaws abstract interface, though the actual proofs (invNTT_ntt, ntt_invNTT, etc.) remain unchanged.
• LatticeCrypto/Ring/Rounding.lean: The RoundingOps structure in LatticeCrypto/Ring/Rounding.lean was made universe-polymorphic: the Coeff parameter now uses an explicit universe variable u (was Type*), and the High and Hint fields now use universe variable v (were Type*). A universe u v declaration was added to support this. No other changes were made; no sorry or admit were introduced.
• ToMathlib/Control/Monad/Commutative.lean: This diff modifies ToMathlib/Control/Monad/Commutative.lean to fix three type-level issues. It changes the @[simp] theorem CommutativeAt.bind_comm declaration to give explicit universe variables (m : Type u → Type v, α β : Type u), ensuring the theorem's binder universe levels match the LawfulMonad typeclass expectation. It also changes Set.monadComm from a @[reducible] def to a plain theorem, which alters how the Commutative Set instance is elaborated and may affect when it is applied by typeclass search. Finally, it removes the @[reducible] attribute from Set.monadComm, so that the binder is no longer reducible (i.e., its definition is not unfolded automatically by simp or dsimp). No sorry or admit are present.
• ToMathlib/OrderEnrichedCategory.lean: The file ToMathlib/OrderEnrichedCategory.lean changes two explicit universe parameters in type class instances and an abbreviation. The MonoidalCategory instance for Preord is modified from MonoidalCategory (Preord) to MonoidalCategory (Preord.{u}), and the PreordEnrichedCategory abbreviation is adjusted from EnrichedCategory Preord C to EnrichedCategory (Preord.{v}) C. These changes ensure the use of explicit universe levels, aligning with the Preord category's universe-polymorphic definition.
• VCVio.lean: Removed the import of VCVio.CryptoFoundations.ReplayForkStdDo from VCVio.lean. This likely indicates that the module is no longer needed, possibly because its functionality was merged elsewhere, eliminated, or the dependency was removed.
• VCVio/CryptoFoundations/AsymmEncAlg/INDCPA/GenericLift.lean: In GenericLift.lean, the proof of IND_CPA_stepAdversary_game_eq_hybridBranch was repaired. The existing evalDist_ext block was missing the transformation of the right-hand side via StateT.run'_eq and an auxiliary lemma hmap (which rewrites (bit == ·) <$> mx as its bind/pure equivalent using map_eq_bind_pure_comp). Adding these steps now makes the subsequent applications of probOutput_map_eq_of_evalDist_eq and probOutput_bind_congr' type-check correctly.
• VCVio/CryptoFoundations/Asymptotics/Negligible.lean: Changed negligible_iff from a def to a theorem (retaining the @[simp] attribute). This refines the declaration's status from a definition to a proposition, which may affect reducibility and kernel treatment while preserving its role as a simp lemma.
• VCVio/CryptoFoundations/FiatShamir/Sigma/Fork.lean: The file has been refactored to replace forkReplay with contextFork throughout. The lemma runTrace_target_eq_of_mem_forkReplay is renamed to runTrace_target_eq_of_mem_contextFork and its proof is rewritten from a replayRunWithTraceValue-based argument to a direct PolyFun context decomposition using contextFork_success. The replayForkingBound theorem’s statement and proof are updated to use contextFork, le_probEvent_isSome_contextFork, and contextFork_propertyTransfer; its docstring is revised to describe the new proof approach. Comments referencing forkReplay are updated to reflect the new API, and an obsolete comment about typeclass requirements is removed from replayForkingBound’s docstring. No sorry or admit are introduced.
• VCVio/CryptoFoundations/FiatShamir/Sigma/Reductions.lean: Renamed the function forkReplay to contextFork throughout the file, including in the definition of nmaForkExtract, the theorem perPk_extraction_bound, and all associated docstrings and proof references. The lemma Fork.runTrace_target_eq_of_mem_forkReplay was also renamed to Fork.runTrace_target_eq_of_mem_contextFork. This is a purely mechanical API refactor that does not change the logic or behavior; it ensures consistency with an updated naming convention in the project's forking infrastructure.
• VCVio/CryptoFoundations/FiatShamir/Sigma/Stateful/Chain.lean: The proof of the private lemma nma_lift_unif_run was adjusted: the exact call to bind_congr was replaced with a refine block that uses simpa with additional rewriting (pure_bind, map_eq_bind_pure_comp, Function.comp_apply) to make the type alignment explicit. This fixes a proof that previously relied on an implicit conversion that is now disallowed or ambiguous.
• VCVio/CryptoFoundations/FiatShamir/Sigma/Stateful/Hops.lean: Added four private lemmas (cmaRealSignPublicDist_some, cmaSimSignPublicDist_some, cmaRealSignPublicDist_none, cmaSimSignPublicDist_none) that factor out the evaluation of cmaRealSignPublicDist and cmaSimSignPublicDist in the some and none cases. The existing lemmas cmaSignPublicDist_tv_le_hvzk and cmaSimSignPublicBad_prob_le_roCacheCount_mul were then refactored to use these new lemmas, eliminating redundant inline expansions and streamlining the proofs. A minor simplification using map_eq_bind_pure_comp was also applied in cmaSimSignStep_evalDist_eq_public. No sorry or admit were introduced.
• VCVio/CryptoFoundations/MacFromPRF.lean: The diff modifies two private theorems in MacFromPRF.lean. simulateQ_prfReal_macToPRFQueryImpl_run is rewritten to use QueryImpl.simulateQ_writerTMapBase_run and a cases split on the query tag, replacing a previously inductive proof. log_cache_invariant_step_unif is rewritten to (a) eliminate a use of erw by rewriting with simulateQ_map and a new lemma simulateQ_prfIdealQueryImpl_liftComp, and (b) restructure the case analysis so that the induction hypothesis ih returns a disjunction hcache' | hlog', which is now used to decide the overall conclusion (left or Or.inr hlog'). Both changes appear to be internal refactors of existing proofs; no new public theorems, definitions, or sorrys are introduced.
• VCVio/CryptoFoundations/MerkleTree/Inductive/Extractability.lean: Removed an unnecessary bind_pure lemma from a simp call in singleHash_withQueryLog, simplifying the proof without changing the theorem's statement. In probOutput_singleHash_eq_inv_card, replaced a bind_pure rewrite with simp [singleHash] to directly equate singleHash to the lifted query, making the bind_pure rewrite explicit and potentially easier to maintain.
• VCVio/CryptoFoundations/MerkleTree/Inductive/QueryBound.lean: The lemma singleHash_isTotalQueryBound is simplified by removing the rewrite rule isTotalQueryBound_query_bind_iff from its simp invocation. The proof now only expands the definitions and uses the simplified Nat inequality and the trivial condition.
• VCVio/CryptoFoundations/MerkleTree/Vector/Defs.lean: The diff introduces a new definition Cache.base (and its lemma Cache.base_zero) to represent the unique cache layer of a depth-zero Merkle tree, replacing ad-hoc Fin case splits in buildMerkleTree and buildMerkleTree_with_hash. It also adds the theorems getRoot_base and getRoot_zero, and refactors getRoot_trivial to use getRoot_zero and getRoot_single to remove an unused Fin.snoc reference. The getPutativeRoot function is simplified by removing a redundant h : n match. These changes unify the base-case handling and provide foundational lemmas for reasoning about depth-zero trees.
• VCVio/CryptoFoundations/ReplayFork.lean: The file replaces its previous replay-based forking infrastructure, which relied on takeBeforeForkAt (an explicit prefix-slicing operator on QueryLog) and inputAt?, with a new approach based on PolyFun's PFunctor.FreeM.Cursor.ForkView. This is reflected by removing inputAt?, inputAt?_logQuery_of_lt, inputAt?_logQuery_self, takeBeforeForkAt, and all its associated lemmas, and adding import PolyFun.PFunctor.Free.Cursor.Fork alongside a local reducibility setting for OracleSpec.toPFunctor and PFunctor.Idx. The new lemmas getQueryValue?_append_self_at_countQ and countQ_eq_occurrences connect QueryLog.countQ to PFunctor.TraceList.occurrences, establishing that query‑log counting is the specialization of PolyFun’s generic occurrence count. The module docstring is updated to state that the shared prefix and both suffixes are now intrinsic to PFunctor.FreeM.Cursor.ForkView, leaving the VCVio layer only responsible for probability and collision estimates.
• VCVio/CryptoFoundations/ReplayForkStdDo.lean: This commit deletes the file VCVio/CryptoFoundations/ReplayForkStdDo.lean, which contained Std.Do.Triple specifications for the replay fork oracle, including per-query theorems (replayOracle_triple_prefix, replayOracle_triple_replacement, replayOracle_triple_immutable) and whole-program corollaries (simulateQ_replayOracle_preserves_prefix, simulateQ_replayOracle_preserves_replacement, simulateQ_replayOracle_preserves_immutable) that lifted the replay invariants from OracleComp.replayOracle into a form consumable by mvcgen, along with worked examples showing their use. The file also included set_option mvcgen.warning false to suppress a known mvcgen warning and two example blocks demonstrating how to recover the support-based theorems from the new Std.Do infrastructure.
• VCVio/CryptoFoundations/SeededFork.lean: In VCVio/CryptoFoundations/SeededFork.lean, the proof block inside sq_tsum_seed_weighted_le_tsum_factored was refactored: three lines using simp and change were replaced with a single rw applying simulateQ_map and StateT.run'_map'. No new theorems or definitions were added, and no sorry or admit appear in the change.
• VCVio/Interaction/UC/AsyncRuntime.lean: Summary unavailable — error: Model 'deepseek/deepseek-v4-flash' hit the output token cap before producing complete structured output; increase max_tokens or lower the thinking budget.
• VCVio/Interaction/UC/AsyncSecurity.lean: The AsyncRun structure and its associated variable block now take an additional type parameter P, and the process field/parameter type changed from Concurrent.ProcessOver Γ to Concurrent.ProcessOver P Γ. This reflects a refactoring of Concurrent.ProcessOver to be parameterized by an extra type P, which propagates to all uses of AsyncRun.
• VCVio/Interaction/UC/Runtime.lean: This diff modifies VCVio/Interaction/UC/Runtime.lean in two ways. First, it adds a new binder {P : Type} to the ProcessOver.runSteps definition and changes its process argument type from ProcessOver Γ to ProcessOver P Γ, generalizing the function to work with processes over any type P rather than just the implicit context Γ. Second, it updates the processSemantics definition to call ProcessOver.runSteps explicitly (using the new qualified name and passing the process.toProcess argument), rather than relying on a method of process.toProcess directly, reflecting the refactored signature.
• VCVio/Interaction/UC/StdDoBridge.lean: Refactored ProcessOver to take an explicit index type P as a parameter, updating the signatures of ProcessOver.runSteps_zero, ProcessOver.runSteps_succ, and runSteps_triple_preserves_invariant to include {P : Type}; added a new ProcessOver.ofStep constructor in the definition of incrementProcess, replacing the former structure-literal syntax.
• VCVio/OracleComp/Coercions/SubSpec.lean: The proof of liftComp_bind_pure was rewritten to use liftComp_bind and map_eq_bind_pure_comp in place of the previous liftComp_map. The lemma's statement is unchanged.
• VCVio/OracleComp/OracleComp.lean: Added ofFreeM and toFreeM reducible definitions to expose the PFunctor.FreeM representation as an explicit abstraction boundary, with accompanying theorems ofFreeM_toFreeM and toFreeM_ofFreeM proving they are mutual inverses. Changed queryBind to use PFunctor.FreeM.liftBind instead of PFunctor.FreeM.roll and updated the liftM_def, liftM_ne_pure, and pure_ne_liftM lemmas to reference PFunctor.FreeM.liftObj and its associated theorems. Added three ofFreeM-monad interaction theorems (ofFreeM_pure, ofFreeM_bind, ofFreeM_map). Converted inductionOn, inductionOnOptional, induction, and inductionOptional from def to theorem, changing their underlying implementation from PFunctor.FreeM.inductionOn to PFunctor.FreeM.induction. Reimplemented construct using OracleComp.recOn instead of PFunctor.FreeM.construct, and changed defaultResult from PFunctor.FreeM.mapM to PFunctor.FreeM.liftM. No sorry or admit were introduced.
• VCVio/OracleComp/OracleSpec.lean: The toPFunctor_add and toPFunctor_mul lemmas were modified to include explicit universe parameters {ι : Type u} {ι' : Type u'} in their binder lists, making the universe levels explicit. The @[simp] attribute and rfl bodies remain unchanged.
• VCVio/OracleComp/ProbComp.lean: Changed ProbComp.inductionOn from a def to a theorem and updated its implementation to use PFunctor.FreeM.induction instead of PFunctor.FreeM.inductionOn. This aligns the induction principle with the current naming in the PFunctor.FreeM API.
• VCVio/OracleComp/QueryTracking/Birthday.lean: The private lemma run_simulateQ_cachingOracle_query_bind_of_miss is modified: in the change tactic block, the argument to PFunctor.FreeM.lift now explicitly supplies the PFunctor via (P := spec.toPFunctor) and passes t directly instead of (query t). This refactor corrects the type of the lifted term, likely to align with an API change or to resolve a type mismatch in the equality proof.
• VCVio/OracleComp/QueryTracking/CachingOracle.lean: The proof of withCacheOverlay_bind_pure was rewritten from a single-equation := to a calc block that first rewrites oa >>= pure ∘ f into f <$> oa using map_eq_bind_pure_comp, then applies the existing withCacheOverlay_map lemma. The statement of the lemma is unchanged; the refactor makes the reasoning explicit and easier to follow.
• VCVio/OracleComp/QueryTracking/Enforcement.lean: The proof of fst_map_run_simulateQ was updated to use simpa with map_eq_bind_pure_comp to rewrite the goal, likely to align with changes in the monad normalization lemmas.
• VCVio/OracleComp/QueryTracking/LoggingOracle.lean: The signature of OracleSpec.loggingOracle was made explicitly universe-polymorphic: the implicit {spec : OracleSpec ι} was replaced with {ι : Type u} {spec : OracleSpec.{u, u} ι}. This adds an explicit universe parameter u for the index type ι and specifies both universe levels in the OracleSpec type, enabling the definition to be used with oracles at different universe levels rather than being tied to a single implicit universe.
• VCVio/OracleComp/QueryTracking/QueryBound.lean: The proof of isQueryBound_query_iff has been refactored from a single call to PFunctor.FreeM.isRollBound_liftA_iff to an explicit simpa block that expands IsQueryBound, OracleSpec.query_def, OracleComp.liftM_def, and PFunctor.FreeM.liftObj before applying the renamed lemma PFunctor.FreeM.isRollBound_lift_iff (note the removal of the capital 'A' from liftA). This reflects a downstream API change in PFunctor.FreeM and ensures that isQueryBound_query_iff continues to reduce correctly under the new definitions.
• VCVio/OracleComp/QueryTracking/ResourceProfile.lean: Refactored the proofs of nsmul_zero and nsmul_succ in the AddMonoid instance for ResourceProfile ω κ so they no longer use simp-based ext-proofs. Instead, each proof now explicitly calls ResourceProfile.ext and then delegates to the corresponding AddMonoid law (AddMonoid.nsmul_zero / AddMonoid.nsmul_succ) on the intrinsic and usage fields separately. This makes the proofs more robust and directly verifies the component-wise equality.
• VCVio/OracleComp/QueryTracking/Structures.lean: Summary unavailable — error: 1 validation error for _ProseSummary
  Invalid JSON: expected value at line 1 column 1 [type=json_invalid, input_value='The Monoid (QueryCount ...admit` are introduced.', input_type=str]
  For further information visit https://errors.pydantic.dev/2.13/v/json_invalid
• VCVio/OracleComp/QueryTracking/Unpredictability.lean: In Unpredictability.lean, the proof of probEvent_cache_has_value_le_of_unique_preimage was modified: the change tactic on the line (StateT.lift (PFunctor.FreeM.lift (query t)) cache₀ >>= _) = _ was updated to (StateT.lift (PFunctor.FreeM.lift (P := spec.toPFunctor) t) cache₀ >>= _) = _. This adjusts the call to PFunctor.FreeM.lift to explicitly provide the P := spec.toPFunctor type argument, likely required by a change in the PFunctor.FreeM.lift API or to resolve type inference.
• VCVio/OracleComp/SimSemantics/Append.lean: In VCVio/OracleComp/SimSemantics/Append.lean, the equality proof hrun in the lemma simulateQ_optionT_liftM_run_eq_of_query was refactored from a rfl to an explicit by block that uses change and rw [map_eq_bind_pure_comp] before concluding with rfl. This change adjusts how the equality of OptionT.run (OptionT.lift ...) is proved, likely to accommodate a change in the representation or definition of OptionT.run or OptionT.lift elsewhere in the codebase. No sorry or admit were introduced.
• VCVio/OracleComp/SimSemantics/ReaderT/Basic.lean: This change generalizes the universe levels of type variables in addReaderT and flattenReaderT within ReaderT/Basic.lean. Specifically, ι₁ and ι₂ are now explicitly quantified with universe parameters u and v (previously Type _), and the OracleSpec types and the inner monad m have their universe parameters made explicit (e.g., OracleSpec.{u, w} ι₁, m : Type w → Type x). The same pattern is applied to flattenReaderT, where ι and the inner monad are given explicit universe parameters. No new theorems, definitions, or sorry/admit were introduced; the changes are purely to universe polymorphism, making the signatures more precise and potentially allowing use in a wider range of universe contexts.
• VCVio/OracleComp/SimSemantics/SimulateQ.lean: The lemma simulateQ and its supporting lemmas simulateQ_bind and simulateQ_def are refactored to replace PFunctor.FreeM.mapM / PFunctor.FreeM.mapMHom / PFunctor.FreeM.mapM_bind' with the corresponding PFunctor.FreeM.liftM / PFunctor.FreeM.liftMHom / PFunctor.FreeM.liftM_bind API. The change propagates through the definition of simulateQ, the proof of simulateQ_bind, and the equality in simulateQ_def (which now states simulateQ impl mx = PFunctor.FreeM.liftMHom impl mx). No other definitions or theorems are modified, and no sorry or admit is introduced.
• VCVio/OracleComp/SimSemantics/StateT/Basic.lean: This file modifies several definitions and lemmas in Basic.lean to make universe parameters explicit. The functions parallelStateT, piStateT, withBadFlag, and withBadUpdate, along with the lemmas withBadFlag_apply_run and withBadUpdate_apply_run, now have their universe variables u, v, w, x explicitly annotated on the type parameters, replacing previous implicit universe placeholders. Additionally, the universe constraint universe u v w was expanded to universe u v w x to accommodate the new explicit x universe parameter used for the codomain of the functor m. These changes improve universe polymorphism and compatibility across different universe levels without altering the logical content or behavior of the code.
• VCVio/OracleComp/SimSemantics/StateT/BundledSemantics.lean: The proof of withStateOracle_evalDist_bind_pure was refactored to use a calc block that explicitly rewrites mx >>= fun x => pure (f x) as f <$> mx using map_eq_bind_pure_comp before applying the existing lemma withStateOracle_evalDist_map. This makes the proof more explicit without altering the lemma's statement.
• VCVio/OracleComp/SimSemantics/WriterT/Basic.lean: The diff modifies parallelWriterT and sigmaWriterT in VCVio/OracleComp/SimSemantics/WriterT/Basic.lean to make their universe levels more precise. Specifically, the universe variables ι₁, ι₂, spec₁, spec₂, m, ω₁, and ω₂ in parallelWriterT are now explicitly constrained as Type u, Type v, OracleSpec.{u, w} ι₁, OracleSpec.{v, w} ι₂, Type w → Type x, and Type w respectively, instead of using Type _. Similarly, in sigmaWriterT, ι is changed to Type v, spec to OracleSpec.{v, w} (ι t), and ω to τ → Type w with m as Type w → Type x. A new universe variable x is also introduced in the universe declaration. These changes tighten the universe polymorphism to avoid universe unification issues in the surrounding project.
• VCVio/ProgramLogic/Tactics/Common/Core.lean: The import Lean.Elab.Tactic has been replaced with the more specific Lean.Elab.Tactic.Basic. This narrows the dependency to only the basic tactic elaboration infrastructure, which may improve compilation times and reduce namespace pollution by avoiding the broader Tactic module import.
• VCVio/ProgramLogic/Tactics/Common/WpStepDispatch.lean: The import Lean.Elab.Tactic was replaced with the more specific Lean.Elab.Tactic.Basic, likely to reduce dependency scope or align with updated module organization in the Lean metaprogramming framework.
• VCVio/ProgramLogic/Tactics/Handler.lean: The import Lean.Elab.Tactic was changed to the more specific Lean.Elab.Tactic.Basic, and no other definitions, theorems, or declarations were modified in the file.
• VCVio/ProgramLogic/Tactics/Relational/Internals.lean: In runRelBindBijRuleUsing, the simp normalization steps now use map_eq_bind_pure_comp instead of bind_pure_comp and OracleComp.bind_pure_comp. This adjustment updates the tactic’s best-effort normalization to reflect a lemma rename or reorganization in the library, ensuring that bind-on-both-sides shapes are still recognized after the underlying API change.
• VCVio/ProgramLogic/Unary/HandlerSpecs.lean: Removed references to the replay fork handler and its specification from the module documentation: the description of prefix/replacement chains for the replay fork in VCVio.CryptoFoundations.ReplayForkStdDo was deleted, and the entire "## Related" section (which noted the location of the replayOracle handler in VCVio.CryptoFoundations.ReplayFork and its Std.Do.Triple specifications in VCVio.CryptoFoundations.ReplayForkStdDo) was removed. This cleanup keeps the file's commentary focused on the handlers it actually documents, as those replay-fork specifics are now maintained elsewhere.
• VCVio/ProgramLogic/Unary/HoareTriple.lean: The proof of wp_map was refactored: the change tactic was replaced with rw [map_eq_bind_pure_comp], which directly rewrites the left-hand side using the standard lemma map_eq_bind_pure_comp instead of manually expanding the monadic map. This simplifies the proof without altering the theorem's statement or its logical content.
• VCVio/ProgramLogic/Unary/Loom/Quantitative.lean: The proof of wp_ExceptT_monadLift was rewritten: previously a single simp call, it now uses an explicit sequence of rw (map_eq_bind_pure_comp, MAlgOrdered.wp_bind), congr, funext, and a direct application of MAlgOrdered.wp_pure. The theorem's statement is unchanged.
• VCVioTest/MerkleTreeBatch.lean: Converts six def declarations with by decide or rfl proofs to theorems: firstSelected, firstNonempty, outerNonempty, allNonempty, leftSelected, bothLeftSelected. Also promotes two defs using native_decide or rfl into theorems: selectedValuesDiffer (proved by native_decide) and putativeRootsAgree (proved by rfl). These changes make the stated equalities and properties into formally named theorems, improving the test file's structure without altering computational content.
• VCVioWidgets/OpenSyntax/Panel.lean: This diff renames the GraphDisplay component and its associated types (Vertex, Edge, Props) to ForceGraphDisplay throughout the file, updating all references in the module documentation comments, the GraphState structure, the buildGraph function, the compTreeToGraph function, and the JSX rendering in renderOneDef. The change ensures consistency with the ProofWidgets library's current API naming. No theorems, definitions, or instances are added, removed, or modified beyond the renaming; no sorries or admits are introduced.
• docs/agents/interop.md: Updated docs/agents/interop.md to reflect that the project now targets Lean 4.32 (up from 4.31). The description of each integration's status was revised: Hax is now noted as not yet Lean 4.32‑compatible, and the Aeneas entry was changed from stating it publishes a Lean 4.31 build whose VCVio bridge must be revalidated, to stating it publishes a Lean 4.31 build whose bridge must instead be ported and then revalidated. The inline lakefile‑style comments were updated accordingly: the Hax element now says it does not build under Lean 4.32, and the Aeneas element now says it is disabled pending a Lean 4.32 port (rather than pending bridge validation).
• lakefile.lean: Updates lakefile.lean to require Lean 4.32 (from 4.31) as the project baseline, bumping the Mathlib pin to v4.32.0, the PolyFun dependency to commit 97a262ce2ba7513448b76635e1f6a07f61f40de5, and the Loom2 dependency to commit 2f65f311fae959c302586b07aa45390999b935d4. The Loom2 comment is revised to reflect that Lean 4.32 now includes stable Std.Do foundations, while Loom2's Std.Do' layer maintains the three-parameter PredTrans, EPost, and relational APIs that VCVio currently consumes; migrating to the redesigned PostShape API is deferred. The comment regarding the Hax interop backend is updated to state that its pinned revision still targets Lean 4.29.0-rc1 and is not part of the Lean 4.32 build. The Interop library comment is updated to confirm it remains excluded from the 4.32 baseline build.
• lean-toolchain: The lean-toolchain file was updated from leanprover/lean4:v4.31.0 to leanprover/lean4:v4.32.0, changing the project's Lean 4 compiler version.
• 1 file(s) filtered as noise (lockfiles, generated, or trivial): lake-manifest.json

---

Last updated: 2026-07-15 17:43 UTC.

[github-actions]

Build Timing Report

• Commit: f5eeecd
• Message: Merge bc5a244 into 4bba755
• Ref: refactor/polyfun-replay-fork
• Comparison baseline: 4bba755 from the latest successful main run.
• Measured on ubuntu-latest with /usr/bin/time -p.
• Commands: clean build rm -rf .lake/build && lake build ToMathlib VCVio FFI LatticeCrypto HashSig Examples VCVioWidgets; warm rebuild lake build ToMathlib VCVio FFI LatticeCrypto HashSig Examples VCVioWidgets; smoke test lake env lean VCVioTest/Smoke.lean.

Measurement	Baseline (s)	Current (s)	Delta (s)	Status
Clean build	721.20	770.18	+48.98	ok
Warm rebuild	5.61	6.65	+1.04	ok
Smoke test	2.88	2.99	+0.11	ok

Incremental Rebuild Signal

• Warm rebuild saved 763.53s vs clean (115.82x faster).

This compares a clean project build against an incremental rebuild in the same CI job; it is a lightweight variability signal, not a full cross-run benchmark.

Slowest Current Clean-Build Files

Showing 20 slowest current targets, with comparison against the selected baseline when available.

Current (s)	Baseline (s)	Delta (s)	Path
65.00	68.00	-3.00	LatticeCrypto/MLKEM/Concrete/NTT.lean
65.00	69.00	-4.00	LatticeCrypto/MLDSA/Concrete/NTT.lean
41.00	36.00	+5.00	VCVio/ProgramLogic/Relational/Loom/Probabilistic.lean
34.00	36.00	-2.00	VCVio/ProgramLogic/Relational/SimulateQ.lean
34.00	32.00	+2.00	VCVio/CryptoFoundations/FiatShamir/Sigma/Stateful/Chain.lean
29.00	29.00	+0.00	VCVio/CryptoFoundations/FiatShamir/Sigma/Stateful/Compatibility.lean
27.00	25.00	+2.00	VCVio/OracleComp/Coercions/Add.lean
25.00	26.00	-1.00	LatticeCrypto/MLKEM/Concrete/Encoding.lean
24.00	33.00	-9.00	VCVio/ProgramLogic/Tactics/Unary/Internals.lean
23.00	23.00	+0.00	VCVio/CryptoFoundations/SecExp.lean
23.00	23.00	+0.00	VCVio/CryptoFoundations/FiatShamir/Sigma/Fork.lean
22.00	21.00	+1.00	VCVio/CryptoFoundations/Fischlin/KnowledgeSoundness.lean
21.00	19.00	+2.00	VCVio/EvalDist/Defs/Basic.lean
21.00	20.00	+1.00	VCVio/CryptoFoundations/FiatShamir/Sigma/Stateful/Hops.lean
20.00	21.00	-1.00	VCVio/OracleComp/QueryTracking/Birthday.lean
20.00	22.00	-2.00	VCVio/ProgramLogic/Tactics/Relational/Internals.lean
20.00	26.00	-6.00	Examples/SimpleTwoServerPIR.lean
17.00	16.00	+1.00	VCVio/EvalDist/Monad/Basic.lean
17.00	18.00	-1.00	VCVio/CryptoFoundations/Fischlin/Completeness.lean
17.00	14.00	+3.00	Examples/CommitmentScheme/Hiding/CountBounds.lean