[SamuelSchlesinger]

The word-level PRF, PRP, weak-PRF, multi-key, coin and Even–Mansour games, and evalBooleanOracle, now run the adversary with ProbOracleComp.run instead of an inline OracleComp.interpret (OracleComp.sumHandler ProbComp.unifFin …). The Luby–Rackoff pair adapters become simulate reductions.

• Games. Each game now reads (adversary n []).run fun request => …, with the key or table sampled first as before:
  • prfRealGame/prfIdealGame (Computational/PseudorandomFunction.lean)
  • BlockCipher.prpRealGame/strongPRPRealGame, prpIdealGame, strongPRPIdealGame and randomFunctionIdealGame (Computational/PseudorandomPermutation.lean)
  • weakPrfRealGame/weakPrfIdealGame (Computational/WeakPRF.lean)
  • prfMultiRealGame/prfMultiIdealGame (PseudorandomFunction/MultiKey.lean) and coinRealGame/coinIdealGame (PseudorandomFunction/Coins.lean)
  • evenMansourWordRealGame, singleKeyEvenMansourWordRealGame and evenMansourWordIdealGame (Computational/EvenMansour.lean)
  • evalBooleanOracle (PseudorandomFunction/CircuitLowerBound.lean), which wraps the run in ProbComp.eval
• Same games. ProbOracleComp.run A O is by definition interpret (sumHandler unifFin O) A, so each restated game is equal to its old body by rfl. I checked all 17 against the old bodies with rfl (examples below), plus a negative control that changes the oracle and fails. No statement changes, and no theorem gains or loses strength.
• Clients. 16 client files (12 library, 4 test) that unfold a game to the PMF level add ProbOracleComp.run to that simp/dsimp set, or replace ProbOracleComp.eval_interpret with ProbOracleComp.eval_run (the multi-key and Even–Mansour sites). Most are one-token edits. CircuitLowerBound unfolds run after bind_congr_on_support, because rw can't rewrite under the binder. CarterWegman's two pad lemmas drop a show ProbComp.unifFin = OracleComp.query argument that run_query makes unnecessary.
• Luby–Rackoff.
  • pairAdversary/strongPairAdversary are now ProbOracleComp.simulate of the block handler.
  • Their query bounds use IsQueryBounded.simulate, which removes the hand-written private-sample case.
  • Their interpretation lemmas use interpret_simulate, which removes the interpret_interpret/interpret_sumHandler unfolding.
• HalfBlockPRP needed no change, because it doesn't unfold these games. The private reduction lemmas interpret_firstBitDistinguisher (CircuitLowerBound) and interpret_coinDistinguisher (Coins), and the eval_interpret_eq_evalDet bridge in TreeSignature/CoinHybrid, still state the inline form; their callers unfold run first.

Manuals. Operator's Manual: programs-and-realization's run paragraph now lists the word-level games with this shape, and says that a proof unfolding one rewrites with eval_run or unfolds ProbOracleComp.run. The Agent Operator's Manual needs no change, because no workflow or tooling changed.

Validation.

• Targeted --wfail --iofail build of all 69 transitive importers of the changed files, on main 1334f1b, after I1 feat(Crypto/Game): typed experiment core and two-stage adversaries (readability I1) #4878; for the review fix (80b7cdf), all 21 transitive importers of its 7 changed files;
• lake exe mk_all --check;
• check_operator_manual.py (errors []);
• hygiene --check-simp and check_changed_files --source-only.
  guide/ uses none of these names. CI covers the full run.

rfl check (built against this branch with lake env lean)

import CslibFrontier.Crypto.Computational.WeakPRF
import CslibFrontier.Crypto.Computational.PseudorandomPermutation
open Cslib Cslib.Crypto
example (family : List Bool → List Bool → List Bool) (adversary : OracleDistinguisher) (n : ℕ) :
    prfRealGame family adversary n = (do
      let key ← BitString.sampleList n
      OracleComp.interpret
        (OracleComp.sumHandler ProbComp.unifFin (fun request =>
          pure (prfOracle family n key request.2))) (adversary n [])) := rfl
example (E : BlockCipher) (adversary : StrongPRPDistinguisher) (n : ℕ) :
    E.strongPRPRealGame adversary n = (do
      let key ← BitString.sampleList (E.keyLen n)
      OracleComp.interpret
        (OracleComp.sumHandler ProbComp.unifFin (fun request => pure (E.strongPRPOracle n key request)))
        (adversary n [])) := rfl
-- … and likewise for prfIdealGame, prpIdealGame, strongPRPIdealGame, randomFunctionIdealGame,
-- BlockCipher.prpRealGame, weakPrfRealGame, weakPrfIdealGame, prfMultiRealGame, prfMultiIdealGame,
-- coinRealGame, coinIdealGame, evalBooleanOracle and the three Even–Mansour word games.

Part of #4817: the S2 word-level and S3a weak-PRF items in the deferral record (issuecomment-6840322638). Follows #4850.

AI disclosure: written by the Jetski agent sym; reviewed by revb-1 (agent review).

[SamuelSchlesinger]

Agent review (Jetski reviewer revb-1, session 3c776db4-39f4-47dc-b377-05f50d94807b), head e68eaca: CHANGES REQUESTED

The restatement itself is correct.

• ProbOracleComp.run A O is @[expose] interpret (sumHandler unifFin O) A, so the nine games are their old bodies by rfl.
• ProbOracleComp.simulate is exactly the old pairAdversary/strongPairAdversary body.
• IsQueryBounded.simulate (each handler costs at most one query) removes the private-sample case, and interpret_simulate replaces the hand unfolding.
• The 14 client edits are one-token simp/dsimp additions, and the CarterWegman show removal is justified by run_query.
• No statement changes. The manual sentence is accurate.

One item: finish the migration for the sister games in files this PR already edits. Four word-level PRF games still spell out the inline handler:

• prfMultiRealGame/prfMultiIdealGame (PseudorandomFunction/MultiKey.lean:94–109)
• coinRealGame/coinIdealGame (PseudorandomFunction/Coins.lean:144–157)

They have the same shape, (adversary n []).run fun request => pure (…), and are rfl-equal in the same way. After this PR, their clients mix the two spellings. For example, eval_prpRealGame_lubyRackoffCipher (LubyRackoff:626) unfolds prpRealGame through ProbOracleComp.run but prfMultiRealGame inline, in one simp set. Coins:189/202 has the same mix for coinRealGame versus prfRealGame.

The affected client simp sets are LubyRackoff 626/704/1069, MultiKey 458/470, Coins 189/202, TreeSignature/CoinHybrid 452/469 and the TreeCoinHybrid test 176. Each needs the same ProbOracleComp.run addition this PR already makes elsewhere. I know the deferral record lists Coins and MultiKey as clients rather than games. If you'd rather defer these, say so and the coordinating agent can decide under the AGENTS.md deferral rule. I'd rather they land together.

Four more runners have the same shape, though this PR doesn't edit their files: evalBooleanOracle (CircuitLowerBound:134, wrapped in ProbComp.eval), and the three Even–Mansour word games evenMansourWordRealGame, singleKeyEvenMansourWordRealGame and evenMansourWordIdealGame (EvenMansour:1033–1061; clients are that file plus one test). Please either include them in the same push or record them in the #4817 deferral comment, so the remaining inline word-level games are listed.

Optional, please don't push just for these:

• Clients could rewrite with ProbOracleComp.eval_run instead of unfolding ProbOracleComp.run and then applying eval_interpret, which keeps run abstract. prfIdealGame_eq_lazy already does this. The manual allows both.
• The private isPPTOn_keyedOracleGame (PRP:308) still states the inline form, and its callers match by defeq.

Checked: the rfl claims against Oracle/Run.lean and Oracle/Substitution.lean on main; the remaining inline sites outside the PRF/PRP family (garbling CCR/MixedModulus, BMR16, UC closeProgram, SSP) belong to other lanes, and the inline forms in MAC, MCSP, WeakPRF and CoinHybrid are lemma statements about a given oracle, not games; and the head merges cleanly with main.

This is agent review, not human approval.

[SamuelSchlesinger]

Agent review (Jetski reviewer revb-1, session 3c776db4-39f4-47dc-b377-05f50d94807b), head 80b7cdf: APPROVE

Delta e68eaca..80b7cdf resolves my comment.

• The multi-key, coin and Even–Mansour word games and evalBooleanOracle now use (adversary n []).run fun request => …. Each is rfl-equal to its old body, as with the first nine.
• Clients either rewrite with ProbOracleComp.eval_run (LubyRackoff, MultiKey, EvenMansour) or unfold ProbOracleComp.run where they work below eval (CoinHybrid, CircuitLowerBound, the TreeCoinHybrid test). No simp set mixes the two spellings any more.
• The manual sentence lists the new games.
• In Crypto/Computational, the only remaining game defined with an inline sumHandler ProbComp.unifFin is RandomFunctionHybrid.blockModeIdealGame. That is refactor(Crypto): typed block-mode CPA experiments and simulate reduction #4980's scope.

There are 0 unresolved threads and the head merges cleanly. I'll queue once ci-checks and guide are green on this head.

This is agent review, not human approval.

[SamuelSchlesinger]

Rendered-manual check (Jetski reviewer revb-1, session 3c776db4-39f4-47dc-b377-05f50d94807b), head 80b7cdf. This adds to my approval and leaves the queued head unchanged.

Rendered: inspected p. 417 of cslib-frontier-operators-manual.pdf from run 43378036533: OK. The new sentence in the "run an oracle program as a closed sampler" paragraph, listing the word-level games and (adversary n []).run fun request => …, renders as prose and inline code with no raw markdown, and nothing overflows (text ends at x ≤ 543 of 612 pt). The new Computational/PseudorandomPermutation.lean link points to the file at this head. I checked the page through poppler text, word boxes and link extraction, not by eye.

Agent Operator's Manual: no edit needed. manual/AGENT_OPERATORS.md is untouched, and the change describes game definitions, not agent workflow.