[SamuelSchlesinger]

Part of #4817 (crypto readability, proofs lane P3). Follows #4956 (P2).

Micali's and BCS's ROM soundness proofs each carried their own copy of the same two-oracle plumbing: memoize the Merkle-hash and Fiat–Shamir sides in two lists, show this implements the lazy oracle on the sum, keep each list's invariant through a run, and transfer call budgets of one-sided programs to the sum. This PR proves it once, generically, and makes both proofs instances of it.

New shared API

• Languages/Probabilistic/RandomOracle/Sum.lean (extends refactor(Crypto/KEM): one lazy=eager random-oracle lemma for the FO-notbot chains (readability K4a) #4949's Cache.sum module): RandomOracle.memoizeSum, defined as sumHandler of two zoomStateT lenses over memoize; the one-call lemmas memoizeSum_inl/inr and support iffs mem_support_memoizeSum_inl/inr; run_interpret_memoizeSum (the two lists implement answer (sumHandler dist₁ dist₂) on Cache.sum); run_interpret_memoizeSum_liftLeft/Right; and the per-list invariant mem_support_run_interpret_memoizeSum.
• Languages/Probabilistic/QueryCount/Sum.lean: IsCostBounded.liftLeft/Right and liftLeft_of_cost_inl_eq_zero/liftRight_of_cost_inr_eq_zero.

Clients. micaliMemoize and bcsMemoize become abbreviations of memoizeSum. Removed: micaliOfTraces(_nil), run_interpret_micaliMemoize, bcsOfTraces(_nil), run_interpret_bcsMemoize, the six isCostBounded_{micali,bcs}{FS,MT}Cost_lift* lemmas and the private lift/invariant copies. The six bcsStickyMemoize support inversions in BCS/ROM use the support iffs instead of unfolding the handler. Net +417/−417 overall: MicaliSoundness −134 and BCS/ROM −186 lines, replaced by 235 lines of reusable API (163 in RandomOracle/Sum, 72 in QueryCount/Sum) with its own tests.

Unchanged: the statements and exact constants of micaliSoundness_bound and bcsROMSoundness_bound, and every other public theorem statement in MicaliSoundness and BCS/ROM. This is infrastructure/refactoring progress, not new mathematics.

Review history. infra reviewed the API design on the branch (board #657): the Cache.sum join, zoomStateT definition without @[expose], and support iffs are its requested changes.

Validation. Targeted --wfail --iofail build of MicaliSoundness, BCS/ROM, RandomOracle/Represented and its Fujisaki–Okamoto clients (NoCheck, NotBot, NotBot/Hybrids, NotBot/Lazy, Security), and the BCSROM/MicaliSoundness/RandomOracleSum/FujisakiOkamoto tests; lint-style; lint on the changed modules; hygiene; encoding readability and projection chain ratchets; mk_all --check; manual check (errors []). New tests in CslibFrontierTests/RandomOracleSum.lean: eager-table equivalence on a mixed program, a per-list invariant, cost transfer of an embedded hash program, and a hash call leaving the challenge list unchanged.

Manuals. Operator's Manual: probabilistic-workflows.md gains a "two independent random oracles as two lists" bullet naming run_interpret_memoizeSum and the one-call lemmas. Agent Operator's Manual: no change needed (no workflow or tooling change).

AI disclosure: Jetski worker proofs (session 7134127c), under the #4817 coordinator; agent review only.

[SamuelSchlesinger]

Agent review claim: coordinator agy-634bba4c (session 634bba4c-9d3c-4f80-8d5b-6097f495b913) is reviewing head a3946156b408ad83a1c61b766b5b39ab8ec4b814. This is agent review, not human review.

[SamuelSchlesinger]

Agent review (Jetski revc-1 session 81a99508-31d1-4fdd-ab77-42c5f3cab9e9), head a394615: APPROVE

This is the right consolidation. Both clients carried the same two-list memoization, the same cache representation and equivalence proof, the same lift inductions and per-list invariant, and six cost-lift lemmas; each is now a one-line instance or a call to the shared API.

• Statements and strength. In MicaliSoundness and BCS/ROM, the only declaration-header changes are the listed removals and micaliMemoize/bcsMemoize becoming abbrevs of memoizeSum. Both agree with the old pattern-matching handlers pointwise (memoizeSum_inl/inr hold by rfl on pair states). micaliSoundness_bound, bcsROMSoundness_bound and the other public statements are untouched. The old IsQueryBounded-hypothesis lifts are the cost₁ := fun _ => 1 instance of IsCostBounded.liftLeft/Right, so nothing is weakened.

• Removed names. No references remain in the library, tests, guide, manual or results, and there are no aliases. That's fine: the generic run_interpret_memoizeSum on Cache.sum supersedes run_interpret_{micali,bcs}Memoize with *OfTraces.

• Placement and reuse.

  • memoizeSum builds on refactor(Crypto/KEM): one lazy=eager random-oracle lemma for the FO-notbot chains (readability K4a) #4949's Cache.sum and the existing zoomStateT.
  • The invariant goes through run_interpret_invariant, and the equivalence through run_interpret_map_state.
  • QueryCount/Sum is a small leaf.
  • RandomOracle/Sum has 4 importers, so its new public Semantics import is cheap.

  I found no existing lift-cost lemma or other two-list copy in the tree. Probabilistic/Sum's interpret_sumHandler_liftLeft covers the stateless case only.

• Callers. The six bcsStickyMemoize inversions now use mem_support_memoizeSum_inl/inr instead of unfolding the handler. P4, or any other two-oracle ROM proof, gets the lazy-oracle equivalence, per-list invariants and per-oracle budgets without re-deriving them.

• Tests and docs.

  • The new RandomOracleSum tests exercise each API piece on a concrete program. They are not restatements, and check_changed_files --source-only passes.
  • The Operator's Manual bullet is accurate, and I agree the Agent Operator's Manual needs no change.
  • ROADMAP and results are unaffected, and the upstream markers are consistent.

There are no review threads. I'll queue once ci-checks and guide are green on this head and the CI notices are clean.

This is agent review, not human approval.

[SamuelSchlesinger]

Coordinator review (coordinator agy-634bba4c, session 634bba4c-9d3c-4f80-8d5b-6097f495b913) of head a3946156b408ad83a1c61b766b5b39ab8ec4b814: APPROVE.

Read the full 8-file diff (+417 / -417) and audited all callers and sibling ROM/query-count modules:

• Shared two-list random oracle (Languages/Probabilistic/RandomOracle/Sum.lean): RandomOracle.memoizeSum cleanly composes sumHandler + zoomStateT + memoize without exposing its body (public section), keeping structural/support/invariant lemmas (memoizeSum_inl/_inr, mem_support_memoizeSum_inl/_inr, run_interpret_memoizeSum_liftLeft/_liftRight, mem_support_run_interpret_memoizeSum) under [BEq ι₁] [BEq ι₂] only and introducing [LawfulBEq] [DecidableEq] only for run_interpret_memoizeSum and map_fst_run_interpret_memoizeSum_nil where answer / memoize_map_ofList require them.
• Sum-interface cost transfer (Languages/Probabilistic/QueryCount/Sum.lean): Universe-polymorphic IsCostBounded.liftLeft, liftRight, liftLeft_of_cost_inl_eq_zero, and liftRight_of_cost_inr_eq_zero live in a small leaf module rather than inflating QueryCount.lean (#569) and close in 2–3 lines from IsCostBounded.interpret and of_forall_cost_eq_zero.
• Client migrations & statements (MicaliSoundness.lean, BCS/ROM.lean, RandomOracleSum.lean): All soundness, knowledge-soundness, and honest-game theorems are preserved verbatim (micaliMemoize and bcsMemoize become abbrevs of RandomOracle.memoizeSum with private import of QueryCount.Sum), all superseded protocol-local trace/cost/invariant helpers are deleted, and CslibFrontierTests/RandomOracleSum.lean exercises adaptive mixed queries, eager PMF.pi simulation, asymmetric list invariants, and sum-cost transfers. Local hygiene, projection-chain ratchet, changed-file source lints, and check_operator_manual.py all pass (AGENT_OPERATORS.md needs no edit).

Optional non-blocking notes for a future pass: listing map_fst_run_interpret_memoizeSum_nil in RandomOracle/Sum.lean's ## Main results docstring and linking CslibFrontierTests/RandomOracleSum.lean from probabilistic-workflows.md alongside micaliMemoize/bcsMemoize.

Will check ci-checks, advisory notices, and the rendered probabilistic-workflows.md PDF page before queueing once CI completes.

This is agent review, not human review.

[SamuelSchlesinger]

Agent review (Jetski revc-1 session 81a99508-31d1-4fdd-ab77-42c5f3cab9e9), rendered-manual check, head a394615:

Rendered: I inspected p. 64 (the new "Two independent random oracles as two lists" bullet in probabilistic workflows) of cslib-frontier-operators-manual.pdf from run 43376320366. OK: no raw markdown, the link to RandomOracle/Sum.lean renders as text, and there is no overflow.

Agent Operator's Manual: no edit needed. The chapter isn't in the agent manual's source manifest, and no workflow changed. My approval of this head stands. This is agent review, not human approval.