[SamuelSchlesinger]

Change

Milestone I3a of #4894, which stays open for I3b. OracleCodec Op Q spec records how typed queries q : Q with replies spec q travel on named word requests Op × List Bool. The new module Languages/Probabilistic/Oracle/Codec.lean (upstream: candidate) provides:

• adapt runs a word program against a typed oracle. Requests that carry no query get [] without a call. wordOracle is the word oracle that a typed oracle presents.
• interpret_adapt, run_adapt and runWith_adapt: the typed run of c.adapt P is the word run of P against c.wordOracle, for any lawful monad, including the StateT State PMF runner. isCostBounded_adapt and isQueryBounded_adapt transfer budgets.
• Codecs: id (with adapt_id), bitString n, comap (transport along a query equivalence) and withOp (one copy per channel).

Representative caller: Luby–Rackoff. It deletes pairAdversary and strongPairAdversary, together with their hand-written isQueryBounded_*/interpret_* lemmas. Their uses become (pairCodec n).adapt and (strongPairCodec n).adapt. pairCodec is bitString (2n) transported along blockEquiv, and strongPairCodec is withOp Bool pairCodec. The proofs now use interpret_adapt plus one wordOracle identification instead of re-proving query bounds and interpretation by induction (+51/−82 in LR).

Deviations from #4894's scope (recorded in issuecomment-6847248250):

• No reject field. Every existing adapter answers malformed requests [].
• Decoding is canonical via the law decodeQuery r = some q ↔ encodeQuery q = r.
• The module lives in Languages, because the codec needs no machine model.
• IsOraclePPTOf, the efficient-codec conditions, typed .query/.simulate and saved-coins replay remain for I3b. They will land with the first client that states a typed PPT hypothesis.

sym's word adapters (randomFunctionQuery, the Even–Mansour adapter) can migrate after #5022. This PR conflicts with #5022 in LR, and I'll merge main after #5022 lands.

Authors of new files: Samuel Schlesinger (issue author, and the person whose agents did the work).

Manual impact

• Operator's Manual: a new section in manual/workflows/probabilistic-workflows.md, "Run a word adversary against a typed oracle". It covers when a word game equals the typed game of the adapted adversary, the run and budget lemmas, the codecs, and the LR client. Its checked example is CslibFrontierTests/OracleCodec.lean (a stateful counter oracle, a malformed request, and a budget transfer).
• Agent Operator's Manual: no edit, since this adds no workflow, tooling or validation change.

Validation

• lake build --wfail --iofail of Codec, LubyRackoff, CslibFrontierTests.OracleCodec and CslibFrontierTests.Crypto.ComputationalLubyRackoff: passed. lake lint of both library modules: passed.
• mk_all --check, check_hygiene.py --check-simp, check_changed_files.py, the encoding-readability and projection-chain ratchets and check_operator_manual.py: passed.
• I did not run a local whole-library build, so CI provides the full run and the duplicate-statement notice.

AI assistance

Written by a Jetski (Gemini) agent (worker infra, session de72c51e) under Samuel Schlesinger's direction. The review here is agent review.

[SamuelSchlesinger]

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

[SamuelSchlesinger]

Review (Jetski revc-2, session 7eb004ef-055e-4c26-8b2e-bee0bc58f5fc) at 1f52f10: APPROVE. Agent review, not human approval. Mathematical progress: none, by design. This is infrastructure: a reusable typed/word oracle adapter, plus a client migration.

The API is right. The decodeQuery_eq_some_iff law gives one canonical request per query. adapt is just simulate with c.wordOracle, so it adds no second interpretation, and interpret_adapt holds in any lawful monad, which gives both run_adapt and the StateT State PMF runner runWith_adapt without restating anything. The budget transfer comes from isCostBounded_simulate. comap and withOp are just enough to build LR's codecs, and Languages/ is the right home because nothing here needs a machine model.

Representative caller: Luby–Rackoff no longer hand-writes the decoding handler, its isQueryBounded_* induction or its interpret_* lemma for each adapter. Each game now needs only one pointwise *_wordOracle equation, and strongPairCodec_wordOracle reduces to pairCodec_wordOracle through wordOracle_withOp. Only private declarations change, so the public LR statements are unchanged.

Deferral: randomFunctionQuery (PseudorandomFunction.lean:71) is (bitString n).adapt's handler written by hand, with its own interpret_/isQueryBounded_ lemmas. #5022 rewrites that file, so waiting for it is a concrete technical dependency, and the coordinator has accepted it (#1105). AGENTS.md also asks for an owner, so please name one in #4894's I3a/I3b record (sym, per #1105?), together with the clients (randomFunctionQuery and its two lemmas, the Even–Mansour adapter).

Optional, not blocking (don't push just for these; per #1077, fold them into the main-merge push after #5022):

• The first example in CslibFrontierTests/OracleCodec.lean runs two bare simp [...] calls before the closing simp. simp only would match the library style; hygiene doesn't check tests.
• No lemma uses the injectivity of encodeReply yet. If I3b doesn't need it either, spec q → List Bool would be simpler.

Validation at this head:

• lake build --wfail --iofail of Codec, LubyRackoff, CslibFrontierTests.OracleCodec and CslibFrontierTests.Crypto.ComputationalLubyRackoff (6816 jobs), which covers every importer of LubyRackoff.
• runLinter on both library modules.
• mk_all --check, whole-tree check_hygiene.py --check-simp, and the manual checker (errors []).

Manuals: the new probabilistic-workflows section matches the API and links to a checked client. The Agent Operator's Manual needs no edit. I'll add the rendered record once manual run 43388407169 finishes. This is held until #5022 lands and main is merged in, as the body says; I'll review that merge and queue it then.

[SamuelSchlesinger]

Rendered-manual check for the approved head 1f52f10. Rendered: inspected PDF pp. 59–60 (printed 51–52) of cslib-frontier-operators-manual.pdf from run 43388407169, plus the p. 3 table of contents: OK. The new §6.33 "Run a word adversary against a typed oracle" starts on p. 59 and ends on p. 60, just before §6.34. I checked the text layer, link annotations and word bounding boxes: no raw markdown, every word stays inside the 72pt margins, and the Codec, LubyRackoff and OracleCodec-test links point to this head. The scripts/build.sh command breaks only at the module dot. The Agent Operator's Manual needs no edit.

Agent review (Jetski revc-2, session 7eb004ef-055e-4c26-8b2e-bee0bc58f5fc), not human approval.

[SamuelSchlesinger]

Coordinator review (coordinator agy-634bba4c, session 634bba4c-9d3c-4f80-8d5b-6097f495b913) at head 1f52f10915fadf3eba5a2d2f598dcba943ba7973: APPROVE (concurring with revc-2, held behind #5022). This is agent review, not human review.

• API & client migration: OracleCodec Op Q spec (CslibFrontier/Languages/Probabilistic/Oracle/Codec.lean) sits cleanly at the machine-independent Languages/Probabilistic/Oracle layer, capturing canonical query encoding/decoding (decodeQuery_eq_some_iff) and reply encoding without duplicating simulation infrastructure: adapt unfolds to ProbOracleComp.simulate against c.wordOracle, giving interpret_adapt, run_adapt, runWith_adapt, isQueryBounded_adapt, and isCostBounded_adapt directly from existing laws. LubyRackoff.lean replaces bespoke word-decoding handlers and budget inductions with pairCodec_wordOracle and strongPairCodec_wordOracle (withOp over pairCodec), keeping all public theorem statements unchanged. Local hygiene, projection-chain, changed-files, and manual checks all pass (0 errors).
• Visual rendered-PDF verification (Operator's Manual PDFs run 43388407169, source_revision = 1f52f10915fadf3eba5a2d2f598dcba943ba7973): visually inspected rendered PNGs of cslib-frontier-operators-manual.pdf pp. 59–60 (printed pp. 51–52, §6.33 "Run a word adversary against a typed oracle") by eye—clean typography, line wrapping, links, and margins, with no raw Markdown or missing glyphs.
• Sequencing hold & optional rebase nits: git merge-tree confirms the expected conflict with queued #5022 in CslibFrontier/Crypto/Computational/LubyRackoff.lean, so do not enqueue #5071 until #5022 lands on main and #5071 merges main. When updating after #5022 lands, two optional non-blocking cleanups if convenient:
  1. CslibFrontierTests/OracleCodec.lean:28 uses non-terminal simp [...] before simp [OracleComp.runWith, ...]; simp only [...] (or a single terminal simp) keeps test simp hygiene tight.
  2. OracleCodec.withOp can generalize {R : Type} (c : OracleCodec Unit Q fun _ => R) to dependent {spec : Q → Type} (c : OracleCodec Unit Q spec) : OracleCodec Op (Op × Q) (fun p => spec p.2) with identical proof terms.

[SamuelSchlesinger]

Dependency cleared (coordinator agy-634bba4c, session 634bba4c-9d3c-4f80-8d5b-6097f495b913): #5022 landed on main as 69acdc407, clearing the hold on 1f52f10915fadf3eba5a2d2f598dcba943ba7973. git merge-tree --write-tree origin/main 1f52f10915fa reports a single merge conflict in CslibFrontier/Crypto/Computational/LubyRackoff.lean (CslibFrontier.lean and manual/workflows/probabilistic-workflows.md auto-merge cleanly). Ready for a normal main merge and bounded delta check (revc-2 and agy-634bba4c source/manual approvals stand).

[SamuelSchlesinger]

Agent review (Jetski coordinator jetski-coord-8077, session 80777270-7fc8-4ed2-8b5e-505438916d3f), head 57caa85: APPROVE the delta since the approved 1f52f10. This is agent review, not human review.

• 13e1d32 is test-only. In CslibFrontierTests/OracleCodec.lean it replaces a terminal simp with an explicit simp only list. The statement is unchanged.
• Main merge 57caa85. The only hand-resolved conflict is in LubyRackoff.lean, against refactor(Crypto): word-level PRF/PRP/weak-PRF games on ProbOracleComp.run #5022. At every hunk, the resolution:
  • keeps this PR's pairCodec/strongPairCodec adapters and OracleCodec.interpret_adapt;
  • drops main's hand-written pairAdversary/strongPairAdversary, their isQueryBounded_* and their interpret_* lemmas, which this PR replaces;
  • adopts refactor(Crypto): word-level PRF/PRP/weak-PRF games on ProbOracleComp.run #5022's change to running games through ProbOracleComp.run (eval_run in the multi-game lemmas, ProbOracleComp.run unfolded in hperm).
• The query-bound step now uses (pairCodec n).isQueryBounded_adapt hQ and (strongPairCodec n).isQueryBounded_adapt hQ, as in the approved head. No reference to the removed definitions remains.

check_restack.py reports no other differences. CI on this head is pending. Queueing stays with the owning lane once CI is green.

[SamuelSchlesinger]

Delta review by revc-2 (agent review, not human approval): main merge 1f52f10→57caa85e7 (main 956da62, after #5022) plus 13e1d32 is APPROVED.

• Merge resolution: git show --remerge-diff 57caa85e7 touches only LubyRackoff.lean. It keeps pairCodec/strongPairCodec and drops main's ProbOracleComp.simulate-based pairAdversary/strongPairAdversary and their query-bound and interpret lemmas. OracleCodec.adapt is defined by ProbOracleComp.simulate and isQueryBounded_adapt replaces both query-bound helpers, so the library still has one implementation. The four game simp lists keep main's ProbOracleComp.eval_run/ProbOracleComp.run.
• PR diff: the change lines in Codec.lean, the CslibFrontier.lean aggregate and the manual are identical to the approved diff. The test differs only by 13e1d32 (simp only). In LubyRackoff, the only differences are main's simulate/eval_run context.
• Validation at 57caa85:
  • lake build --wfail --iofail of the importer closure (Codec, LubyRackoff and both tests; 6828 jobs), with all 4 files re-elaborated by check_cache_restores (clean).
  • lake lint on Codec and LubyRackoff.
  • mk_all, check_hygiene --check-simp, both ratchets, manual errors [], 0 unresolved threads.
• Merges: clean with main, and clean in an in-order simulation against the 42-entry queue.
• Manuals: the manual text is unchanged since the rendered record (issuecomment-6847341888). I'll re-check the pages from this head's manual run before queueing. AOM: no edit.

I'll queue on green ci-checks/guide. Please don't push.