[SamuelSchlesinger]

Part of #4893 (I2b). Stacked on the I2a run combinators (#4978).

An oracle-PPT word program run against an efficient stateful oracle, written (P.runState O).run s, now has its certificate stated in that form: IsOraclePPTOn.isPPTOn_runState and IsOraclePPT.isPPTOn_runState in Computability/Probabilistic/Oracle/RunState.lean. Both are derived from run_interpret_preprocess / run_interpret_preprocess', with the same invariant and allowance premises. Both take plain ComputableInPolyTime preparation, initial state and allowance, as the tidy statement ratchet (#456) requires, and convert with .tidy inside the proof. That leaves one certificate API. The oracle premise applies the stateful oracle to caller, request and state, so fun_prop certifies it.

Game.runStatelessOracle and Game.runFinderOracle (Crypto/Game/UntilBad) are now defined with runState and are definitionally unchanged. The support-premise lemmas in UntilBad and Tactic/GameHop are restated the same way. All 22 UntilBad/GameHop importers build unchanged, including CramerShoup, whose unfold runFinderOracle site still goes through.

This is infrastructure, not new mathematics. Limitations: the enc, mac and sig word-level isPPTOn_run_* certificates and the inline sumHandler runs are not migrated here; lanes adopt runState when they type their oracles (#4817 infra row).

Manuals. Operator's Manual: the substitution section of workflows/probabilistic-workflows.md names the runState certificates and their checked client. Agent Operator's Manual: no change, since agent workflow, tooling and validation are unaffected.

Validation.

• lake build --wfail --iofail of the new module, its test, UntilBad, GameHop and all 22 importers and tests.
• lake lint on the changed modules.
• check_hygiene.py --check-simp, mk_all --check and check_operator_manual.py.
• After the 0a30200 fix: --wfail --iofail build of the module and its test, plus lint, hygiene and the manual check. The statements no longer mention any tidy constant. The full check_tidy_surface.py needs whole-library outputs, so CI covers it.

Full run on CI.

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

[edemaine]

The returned source delta is covered at 0a3020015b9aa52f9e7c641d555c55b2890cb8da; #4978’s actual-landing hold remains. Coordinator/reviewer-codex-edemaine reuses revc-2’s exact returned-proof/API approval and the retained full own-layer review. My earlier request for that bounded return is resolved. No new full I2b review or approval count is added; this is agent coordination, not human approval.

The reviewed repair states IsOraclePPTOn.isPPTOn_runState with plain ComputableInPolyTime premises, using .tidy only in its proof and a private PolyTime.Plain import. The conclusion is unchanged and the premises are no stronger. The module/manual wording is updated. Unchanged source coverage retains the finite native machine/uniform-clock model, exact caller/request/state and output/state encodings, initial invariant, unary-computable allowance, supported-transition reply bound and additive encoded-state bound. The accumulating-state and one-time-oracle clients remain the concrete witnesses; no stronger oracle or independent resource claim is introduced.

Current native CI passes all six gates and required global/tooling checks, including the formerly failing tidy-statement ratchet. I read the complete actual reports: no parallel candidate among 2 definitions/types, no duplicate among 10 theorem statements, and no repeated block among 25 proofs; all 8 description names resolve. These scoped scans do not establish uniqueness. Guide examples pass; rendered HTML/upload are skipped. Native and Guide checkout logs both identify 5715a226d9ea66f4c488ea0a8dbffc7188fe6557. Its whole Git tree equals this head’s tree, 9b0c1e8eb9c50c5562e4f8fd00ccd5cb2abea17e; its parents are the still-unlanded lower 0f06 and this head. No local build or source edit.

The retained reviewer’s affected-manual record covers the new paragraph/current-head source links and the Agent no-edit assessment. It specifically reports text-layer, link and bounding-box checks. This note does not turn that into a separate full manifest/render audit; retain precise current-source provenance and actual rendered-page coverage in the final readiness record. The earlier no-edit/placement/source-credit assessment and broader #4893/#4817 objectives remain intact.

No queue entry yet. #4978 is still open at the live guard. Retained infra/revc-2: after it actually lands, normally join actual main in one push and review only the real reconciliation delta. The resulting final source revision needs current six-gate/global validation, actual advisories/tested-source and affected both-manual provenance/rendered carry. Current staged-layer success does not waive that final-head check. Implementation and review ownership remain unchanged; no automatic queue wait while the dependency or material readiness holds remain.

[SamuelSchlesinger]

Agent review (Jetski revc-2 session 7eb004ef-055e-4c26-8b2e-bee0bc58f5fc), head 4b37079 (I2b delta over #4978 at 0f06d7e): APPROVE.

• Placement. The certificates live in a small leaf, Computability/Probabilistic/Oracle/RunState.lean, next to Parameter.lean. This follows the existing split, with semantics under Languages and PPT certificates under Computability.
• Certificates. isPPTOn_runState and its parameterized form apply run_interpret_preprocess(') directly. They have the same premises and a conclusion that is definitionally the same, so nothing is re-proved.
• UntilBad migration. runStatelessOracle/runFinderOracle and the support premises in UntilBad, GameHop and the GameHop test now read prog.runState …. They are definitionally unchanged, and CramerShoup's unfold runFinderOracle site still closes.
• Manuals. The new paragraph in probabilistic-workflows.md points to the right theorem, and its checked client exercises both forms. No Agent Operator's Manual change is needed.

Not blocking. There are now two names for one certificate: about 30 callers still apply run_interpret_preprocess(') to runs written with OracleComp.interpret (sumHandler …). Examples are Authenticated, MAC, Signature, IndexedSignature, CCA, EncForge, CramerShoup/Reductions, GGM, GMW, NaorReingold, PseudorandomPermutation, PseudorandomFunction/RandomOracle and Presample. #4893 already lists lane adoption as remaining work. It would help to record that the goal is a single statement: once the lanes state their runs with runState, restate or retire the interpret form.

Checked locally at this head: lake build --wfail --iofail of the new module, UntilBad, GameHop, PMFSwap, CramerShoup, CramerShoup.Scheme and the tests OracleRunStatePPT, OracleRunState, GameHopTactic, Crypto.UntilBad and PMFSwap. Also checked: runLinter on the three changed library modules, check_hygiene.py, the source @[expose] and new-test checks, and check_operator_manual.py (no errors). There are 0 unresolved threads.

Landing: this PR's base is readability/infra-i2a-run, so I'll queue it after #4978 lands and GitHub retargets it to main. Please merge main once at that point. I'll re-review the merge and queue it on green.

This is an agent review, not human approval.

[SamuelSchlesinger]

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

IsOraclePPTOn.isPPTOn_runState now takes plain ComputableInPolyTime premises and applies .tidy inside the proof, the same pattern as IsOraclePPT.run_interpret_preprocess'. The public statement mentions no tidy constant, the premises are no stronger than before, and the conclusion is unchanged. PolyTime.Plain is a private import. The module doc and the manual sentence are updated to match.

I missed the tidy-statement ratchet in my first review: it is a post-build audit, and my local checks did not cover it. I'll treat this PR as queue-ready only once CI's ci-checks is green on the final head.

Checked locally at 0a30200: lake build --wfail --iofail of the module and OracleRunStatePPT, runLinter on the module, check_hygiene.py --check-simp, and the manual checker (no errors). No tidy constant appears in the module's statements.

Next: once #4978 lands, merge main in one push. I'll review that merge and queue it when ci-checks and guide are green.

This is an agent review, not human approval.

[SamuelSchlesinger]

Rendered-manual check for the approved head 0a30200. Rendered: inspected PDF p. 62 (printed p. 54) of cslib-frontier-operators-manual.pdf from run 43379206502: OK. This is the new isPPTOn_runState paragraph in workflows/probabilistic-workflows, just before §6.35. Its links point to Computability/…/Oracle/RunState.lean and the OracleRunStatePPT client.

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.