[SamuelSchlesinger]

The block-mode CPA hybrid now runs its experiments on the typed oracle API from #4850. CTR and OFB no longer unfold the reduction by hand.

• Block-mode experiments. In RandomFunctionHybrid, blockModeCpaGame/blockModeIdealGame become blockModeCpaExperiment/blockModeIdealExperiment : ProbComp Bool, which run the adversary with adversary.run. blockModeReduction is now ProbOracleComp.simulate (blockModeQueryProgram keystream ℓ b) adversary. As a result:
  • blockModeCpaExperiment_eq_realExperiment holds before evaluation;
  • isQueryBounded_blockModeReduction is a single isCostBounded_simulate call.
• runWith_simulate. It is in the new Oracle/Substitution/RunWith.lean. A stateful run of simulate handler A is a run of A against the oracle that runs each handler q. CTR, OFB, RFH and the DEM CCA simulation lemma (Hybrid/DEMCCA) use it in place of the runWith_interpret_sumHandler rewrites.
  • Substitution (94 transitive importers) and Interaction (1150) don't import each other. So the lemma goes in a leaf module that imports both, as Substitution/QueryCount.lean does. It is imported only by its four clients.
• CTR/OFB. ctrCpaGame/ofbCpaGame stay Game-valued as the law of the typed experiment, so their security statements are unchanged. The lift lemmas are now congrArg ProbComp.eval of the experiment equation.
• CCR. CCR.Arithmetic.idealGame runs the adversary with ProbOracleComp.run, as revc-1 raised in refactor(Crypto): typed finite PRF/PRP experiments and ProbOracleComp.run #4850. It answers every query with a fresh uniform label, so it stays separate from PRF.idealExperiment.

No theorem statement changes strength. The only renames are the two block-mode experiments above, and no references to the old names remain.

Caller check. The identical-until-bad bound in CTR (toOuterMeasure_bad_fresh_le, and its OFB counterpart) opens with rw [ctrReduction, blockModeReduction, ProbOracleComp.runWith_simulate]. It no longer unfolds simulate into runWith_interpret_sumHandler, and ctrCpaGame_eq_realExperiment is a one-line congrArg ProbComp.eval of the experiment equation. The RFH query bound no longer re-proves the handler's private-sample case.

Manuals. In the Operator's Manual:

• security-games-and-primitives describes the typed block-mode experiments;
• probabilistic-workflows ("Substitute an oracle") adds runWith_simulate next to the QueryCount paragraph.

The Agent Operator's Manual needs no change because no workflow or tooling changed.

Validation.

• Targeted --wfail --iofail build of every transitive importer of the changed modules (15 targets, including the CTR, OFB, garbling and half-gates tests);
• lake exe mk_all --check;
• scripts/check_operator_manual.py (errors []).
  CI covers the full run.

Part of #4817: the S2 block-mode and CCR items in the deferral record (issuecomment-6840322638). Follows #4850, which has landed.

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

[SamuelSchlesinger]

Agent review (Jetski revc-1 session 81a99508-31d1-4fdd-ab77-42c5f3cab9e9), head 01733bf: CHANGES REQUESTED (one small migration and a doc nit; the main change is correct)

What checks out:

• Same laws. The definitions match the old ones definitionally:

  • ProbOracleComp.run A O unfolds to interpret (sumHandler unifFin O) A.
  • simulate h A unfolds to interpret (sumHandler (sample ∘ unifFin) h) A.

  So blockModeCpaExperiment/blockModeIdealExperiment, blockModeReduction and CCR.Arithmetic.idealGame are the replaced terms with names. Every Game the statements use is ProbComp.eval of the corresponding experiment.

• Strength.

  • ctrCpaGame/ofbCpaGame keep their type.
  • The CTR/OFB idealization and CPA bounds and isQueryBounded_blockModeReduction change only by the definitional rename.
  • blockModeCpaExperiment_eq_realExperiment now holds before evaluation, which is stronger.

• Old names. No references to the old names remain anywhere in the tree (library, tests, results, guide, manual).

• Placement. runWith_simulate belongs in a leaf: Substitution and Interaction don't import each other, the same reason Substitution/QueryCount is a leaf. The upstream marker matches its sibling.

• Manuals. I agree with the manual assessment for both manuals.

• Lints. check_changed_files.py --source-only passes.

Requested:

1. Encryption/Hybrid/DEMCCA.lean:210 is the one other library proof that does what this PR removes. It unfolds simulate and then rewrites with runWith_interpret_sumHandler:
   rw [ProbOracleComp.simulate, ProbOracleComp.eval_run_interpret_eq_runWith, ProbOracleComp.runWith_interpret_sumHandler, ← hsim, …].
   Please migrate it with the other callers:
   rw [ProbOracleComp.eval_run_interpret_eq_runWith, ProbOracleComp.runWith_simulate, ← hsim, ProbOracleComp.eval_run_interpret_eq_runWith], plus import CslibFrontier.Languages.Probabilistic.Oracle.Substitution.RunWith.
   This is an unbuilt sketch. The rewrite order matches the current proof, which already depends on the first eval_run_interpret_eq_runWith hitting the left-hand side.
   refactor(Probability/PMF): share point-hit and bind-comparison lemmas (readability PD) #4976 also edits DEMCCA, at the imports and L173. Put the new import after Oracle.Simulation so the hunks don't touch.
   The other runWith_interpret_sumHandler users are fine as they are:
   • MACThenEncrypt, which inlines its handler and doesn't use simulate;
   • Signature/RandomOracle (liftProver);
   • the OracleRepresentation test of the general lemma.
2. RandomFunctionHybrid.lean:34: the module doc still says "block-mode query/cost/ideal-game interface". CTR, OFB and the manual now say "ideal-experiment".

This is agent review, not human approval.

[SamuelSchlesinger]

Agent review (Jetski revc-1 session 81a99508-31d1-4fdd-ab77-42c5f3cab9e9), head 00d06c3: APPROVE

The delta since 01733bf (2 files) resolves both requested items:

• DEMCCA.lean:211 now rewrites the substituted phase with runWith_simulate instead of unfolding simulate and using runWith_interpret_sumHandler. The new import sits after Oracle.Simulation, clear of refactor(Probability/PMF): share point-hit and bind-comparison lemmas (readability PD) #4976's import hunk.
• The RandomFunctionHybrid module doc now says "ideal-experiment interface".

Statements are unchanged, the head still merges cleanly with main, and there are no review threads. My review of the rest of the PR stands (issuecomment-6844723008). I'll queue once ci-checks and guide are green on this head.

This is agent review, not human approval.

[SamuelSchlesinger]

Agent review (Jetski revc-1 session 81a99508-31d1-4fdd-ab77-42c5f3cab9e9), rendered-manual check, head 00d06c3:

Rendered: I inspected pp. 445–446 (the block-mode interface paragraph and the CTR/OFB paragraphs that now name blockModeIdealExperiment) and p. 59 (the runWith_simulate paragraph in probabilistic workflows) of cslib-frontier-operators-manual.pdf from run 43370238829. All OK: no raw markdown, the links resolve to text, there is no overflow, and ℓ/2^n are typeset correctly.

Agent Operator's Manual: no edit needed. Neither changed chapter is in the agent manual's source manifest, and no workflow or convention changed. My approval of this head stands. This is agent review, not human approval.