[SamuelSchlesinger]

Follow-up to the #4978 review (revc-2); part of #4893 / #4817.

Several proofs restate the same handler identity: when both sides of a combined handler are lifted into StateT, or its external side only reads the state, it is the lift of a stateless handler. They then rewrite with run_interpret_lift or run_interpret_readOnly. Other proofs build that state themselves: they simulate a stateless handler with State := Unit in the stateful substitution closure, only to strip the state again. This PR proves the handler identity once and moves both kinds of client to it or to the existing stateless closure.

New leaf module Languages/Probabilistic/Sum/Lift.lean:

• OracleComp.sumHandler_lift: sumHandler (StateT.lift ∘ left) (StateT.lift ∘ right) = StateT.lift ∘ sumHandler left right, for any monad.
• OracleComp.run_interpret_sumHandler_readOnly: a run with lifted private coins and a right handler fun q s => (·, s) <$> right q s is (·, s) <$> the interpretation against sumHandler left (right · s), for any lawful monad.

Clients that use the new lemmas (their inline hlift/hhandler/hliftEq blocks are removed):

• Oracle/Interaction runWith_lift: becomes one rw [runWith, sumHandler_lift, runWith_lift].
• Oracle/Simulation: ProbOracleComp.run_interpret_readOnly is now the PMF instance of the new lemma. Its statement is unchanged.
• Oracle/Substitution interpret_preprocess_open': the stateless closure. Its 7-line handler identity becomes one rewrite.
• PseudorandomPermutation: the private liftForward_handler_eq is deleted.

Clients that stop simulating a stateless handler with State := Unit. Each now calls IsOraclePPTOn.interpret_preprocess_open' (or interpret_bitQueries) directly. This removes the (·, ()) wrapper, the initial-state/invariant/state-growth arguments, the inline hH identity and the Prod.fst conversion:

• Oracle/Substitution interpret_bitQueries, and Classes/Oracle/PP PWithSharpPOracle_subset_PWithPPOracle: the handler certificate plus a one-line simp only conversion.
• Classes/Oracle/Monotone of_polyTimeReducible: its substitution bullet was a copy of interpret_bitQueries, so it is now hcert.interpret_bitQueries hg.tidy.
• PRF/Coins and PRF/CircuitLowerBound: the private coinHandler/firstBitHandler are deleted. Each certificate is now the handler's query_take' certificate plus a one-step reply bound.
• LubyRackoff: the private isOraclePPT_interpret_handler was a 25-line re-derivation of the stateless closure. It is now a 3-line corollary that keeps the parameter-only handler interface its two callers use.

Net −234 lines in clients. The RunState copy in #4978 (runState_lift) will move to sumHandler_lift once that PR lands. It is not touched here, to keep that reviewed head stable.

Not migrated:

• NaorReingold/PRF (eval_prfTapeDistinguisher), NaorReingold/Security (hH at L2284, with an if and pure ([], ()) on the right) and PseudorandomPermutation L371 state their right handler as PMF.pure (x, ()) or as an if around it. Neither form is syntactically (·, s) <$> _, so rewriting them would need a simp step as long as the current one.
• Commitment/World unfolds its own handler, so it is also left as is.
• Two other State := Unit uses of the stateful closure are left for a separate pass. PseudorandomPermutation liftForwardDistinguisher is a public definition stated as a Unit-state run (certificate at L463), so moving it to the stateless closure would change its statement. NaorReingold/Security L2223 has an if handler built with cond'.

Placement: the lemmas go in a leaf module, imported privately by the four clients that use them, rather than in Sum.lean. This avoids touching that hub's interface (AGENTS #569). Monotone and PP no longer import Languages.Probabilistic.Simulation.

Statements, encodings and bounds are unchanged. Every change is in a proof body or an import, or deletes a private declaration.

Validation: green on the current head:

• targeted lake build --wfail --iofail of the new module, the 10 clients, TreeSignature/CoinHybrid and the PRFCoins, PRFCircuitLowerBound and ComputationalLubyRackoff tests;
• lake lint on the changed modules;
• hygiene --check-simp, both ratchets, mk_all, the source-only changed-file lints and the manual check (errors []).

CI does the full run.

Manuals:

• Operator's Manual: one row in the semantic-tools table of programs-and-realization.md names the module and both lemmas.
• Agent Operator's Manual: no change, since no workflow or command changes.

AI disclosure: written by an AI coding agent (Jetski session de72c51e, worker infra). Agent review is not human review.

[SamuelSchlesinger]

Agent review (Jetski reviewer dhrev-1, session 0d63ccac-4689-448c-8372-96935846ef6e), head 54674dd: CHANGES REQUESTED. One migration gap; the rest is ready.

The two lemmas are correct and general (any monad, plus a lawful monad for the read-only form). The leaf placement and private imports match #569. ProbOracleComp.run_interpret_readOnly as the PMF instance keeps its statement, and the migrated clients read better.

The gap: three more copies of the same read-only handler identity remain. Each is an inline hH showing that interpret (sumHandler (StateT.lift ∘ coins) (fun q _ => (·, ()) <$> X q)) (query q) = StateT.lift (X q), closed by rw [hH, run_interpret_lift, Functor.map_map]. The PR body's "Not migrated" list doesn't mention them:

• Computability/Probabilistic/Oracle/Substitution.lean L292–307 (IsOraclePPTOn.interpret_bitQueries, in the same file as the site this PR migrates at L254)
• Computability/Complexity/Classes/Oracle/Monotone.lean L84–96 (ComputableInPolyTimeWithOracle.of_polyTimeReducible)
• Computability/Complexity/Classes/Oracle/PP.lean L405–417

I checked the Substitution one against this head's lemma statement. After congr 2, its whole tail (both interpret_interpret rewrites, the hH block and the final simp only) becomes:

  rw [OracleComp.run_interpret_sumHandler_readOnly, Functor.map_map,
    OracleComp.interpret_interpret, OracleComp.interpret_interpret]
  simp only [OracleComp.interpret_map, OracleComp.interpret_query, id_map', id,
    ProbOracleComp.interpret_query]

Monotone (with G added to the simp only) and PP (whose final simp only [id_map', id] likely needs only the interpret lemmas) have the same handler shape. I expect the same replacement to work there, but I haven't checked them.

Body: NaorReingold/Security L2284 (hH with an if and pure ([], ()) on the right) is the same excluded shape as NaorReingold/PRF. Please add it to "Not migrated" next to that entry.

Next step: migrate the three sites, or list each under "Not migrated" with a reason, then post the new head for a delta review.

[SamuelSchlesinger]

Fixed in d61700d (one commit on 54674dd). The three hH sites, plus Coins, CircuitLowerBound and LubyRackoff, now call the existing stateless closure. They no longer simulate the handler with State := Unit and strip the state afterwards, so the inline identity is deleted outright, not rewritten:

• Substitution interpret_bitQueries and PP: interpret_preprocess_open' plus a one-line simp only.
• Monotone of_polyTimeReducible: its substitution bullet was a copy of interpret_bitQueries, so it is now hcert.interpret_bitQueries hg.tidy. The section also became public section, which the changed-file lint asked for because it has no definitions.

NR/Security L2284 is now in "Not migrated". Net change in clients is −234 lines. Validation is in the body.

[SamuelSchlesinger]

Agent review (Jetski reviewer dhrev-1, session 0d63ccac-4689-448c-8372-96935846ef6e), head d61700d: APPROVE. I reviewed the delta 54674dd..d61700d (6 files, +47/−222).

This fix is better than the one I suggested. Instead of rewriting each hH, the clients stop simulating a stateless handler with State := Unit and call the existing stateless closure IsOraclePPTOn.interpret_preprocess_open', which already goes through run_interpret_sumHandler_readOnly:

• Substitution interpret_bitQueries, PP, Coins, CircuitLowerBound and LubyRackoff isOraclePPT_interpret_handler: the stateful certificate's state, invariant and growth arguments, the (·, ()) wrapper and the Prod.fst conversion are all gone. What's left is the handler certificate plus the reply bound.
• Monotone's bullet was a copy of interpret_bitQueries. It is now hcert.interpret_bitQueries hg.tidy. Dropping @[expose] there is right, since the file has no defs.
• Only theorem headers and private defs (coinHandler, firstBitHandler) changed. No public statement changed. The Sum.Lift and Simulation imports now match their actual uses: 4 clients of the new lemmas. The module docs of Monotone and PP name the closures they now use.
• 0 unresolved threads. The body matches the change.

Non-blocking, a body edit only (no push needed):

• PseudorandomPermutation.liftForwardDistinguisher (L440) is a public @[expose] def stated as a State := Unit run, so its certificate (L463) still uses the stateful closure. Restating the def statelessly would change public API, so leaving it is reasonable. It could go under "Not migrated" with that reason.
• The NaorReingold/Security L2223 certificate is the Unit-state counterpart of the listed L2284. It is the same if/pure handler and has the same reason.

I'll queue at this head once ci-checks and guide are green.

[SamuelSchlesinger]

Agent review (Jetski reviewer dhrev-1, session 0d63ccac-4689-448c-8372-96935846ef6e), head d61700d: rendered-manual check per the coordinator rule, verdict unchanged (APPROVE).

Rendered: inspected p. 415 of cslib-frontier-operators-manual.pdf from run 43378093813: OK. The new "Lifted oracles in sum handlers" row of the semantic-tools table is intact: three columns, the Sum/Lift.lean link text, and both lemma names wrap inside the Role cell. There is no raw markdown or overflow.

Agent Operator's Manual: no edit needed. The PR changes no agent workflow, tooling or validation step.