[SamuelSchlesinger]

Part of #4893 (I2a). Builds on ProbOracleComp.run from #4850.

This PR adds Languages/Probabilistic/Oracle/RunState.lean, which runs an oracle program against a challenger oracle that keeps state or a log. It is meant to replace the inline sum handlers and the per-lane runners.

• A.runState O: each query q runs a StateT σ ProbComp program O q, and private draws stay uniform. The simp laws are runState_pure/bind/map/query/sample. eval_runState gives its law as runWith, and runState_lift says that a memoryless oracle reduces to run with the state unchanged.
• A.runLog O and A.runLogWith O return the result together with the chronological log of answered queries. In runLogWith, the oracle can read the log and refuse a query: O log q = none answers default and logs nothing. This is the form of one-time and no-repeat signing and MAC oracles. logOracle_run is the one-call equation that sig asked for.
• IsQueryBounded.length_runLog_le and length_runLogWith_le bound the log length by the query budget. They come from measure_runState_le, the stateful form of OracleComp.IsCostBounded.measure_le, so the counting argument is made once.

This is infrastructure, not new mathematics. Limitations: there is no library client in this PR. I2b (stacked, opens next) puts UntilBad's runStatelessOracle/runFinderOracle on runState and adds the IsOraclePPT certificate. The enc runAgainst, mac and sig runners move when their lanes type their oracles (#4817 infra row). The checked examples are in CslibFrontierTests/OracleRunState.lean.

Manuals. In the Operator's Manual, programs-and-realization.md gets a paragraph after the run paragraph covering runState, runLog, runLogWith and the log bound. The Agent Operator's Manual needs no change, since agent workflow, tooling and validation are unaffected. ROADMAP and the results inventory are unaffected. The new module carries -- upstream: candidate.

Validation. At this head (main merged; #4850's files taken from main):

• lake build --wfail --iofail of the module and its test
• lake lint on the module
• check_hygiene.py --check-simp, mk_all --check, check_operator_manual.py
• the source @[expose]/new-test checks

The full run is on CI.

AI disclosure: written by the Jetski agent infra (conversation de72c51e) for Samuel Schlesinger; agent self-reviewed, awaiting independent review.

[SamuelSchlesinger]

Agent review (Jetski revc-2 session 7eb004ef-055e-4c26-8b2e-bee0bc58f5fc), head 0f06d7e: APPROVE.

runState gives a name to the interpret (sumHandler (fun n => StateT.lift (ProbComp.unifFin n)) O) pattern that games now write out inline. The module is a small leaf under Oracle/, so it does not grow a hub. Its laws come from existing results instead of new proofs: eval_runState is eval_run_interpret_eq_runWith, and measure_runState_le is IsCostBounded.measure_le for this handler. Both log-length bounds use that one counting lemma. @[expose] is needed here, because the test checks runLogWith_some and logOracle_run by rfl from another module. The new paragraph in the Operator's Manual matches the API, and no Agent Operator's Manual change is needed.

Optional, not blocking: the hlift step in runState_lift (L115–118) is the fifth copy of "sumHandler of StateT.lifts is StateT.lift of the sumHandler". The others are at Interaction:106, LubyRackoff:546, NaorReingold/PRF:589 and PseudorandomPermutation:373/484. A sumHandler_lift lemma in Probabilistic/Sum.lean could replace all of them later. Moving the inline StateT.lift (ProbComp.unif…) sites over to runState is follow-up work for I2b and the per-lane PRs, as the Limitations section says.

Checked locally at this head: lake build --wfail --iofail of Oracle.RunState and CslibFrontierTests.OracleRunState (no other importers yet), runLinter on the module, check_hygiene.py, the source @[expose] and new-test checks, and check_operator_manual.py (no errors). There are 0 unresolved threads.

This is an agent review, not human approval.

[SamuelSchlesinger]

Rendered-manual check for the approved head 0f06d7e. Rendered: inspected PDF p. 414 (printed p. 406) of cslib-frontier-operators-manual.pdf from run 43369525874: OK. This is the new runState/runLog/runLogWith paragraph in programs-and-realization. Long identifiers break at underscores or dots, which is the book's normal style.

I checked the page's text layer, link annotations and word bounding boxes: no raw markdown, every word stays inside the 72pt margins, and the new links point to this head. Agent review (Jetski revc-2, session 7eb004ef-055e-4c26-8b2e-bee0bc58f5fc), not human approval.

Agent Operator's Manual: no edit needed. Its manifest takes only AGENT_OPERATORS.md as input, and this PR doesn't change workflow policy.