[SamuelSchlesinger]

Part of #4817 (crypto readability, residual lane, item R2).

Session: rerand (Jetski, conversation 4f342748), branch readability/residual-r2-idealcipher-dm.

Change

This is a refactor of Primitives/IdealCipher/Compression.lean. It adds no new mathematics, and the headline bounds are unchanged.

• Game. collisionGame now samples the cipher with IdealCipher.complete fun _ => [], which replaces the inlined PMF.pi (fun _ => RandomPermutation.complete []). It destructures the candidate as ((x₁, x₂), _) and wins on collides x₁ x₂ (H E x₁) (H E x₂).
  • The new game equals the old one: rw [collisionGame, complete_nil, RandomPermutation.complete_nil]; rfl proves it equal to the old inline definition, checked in a scratch file against this head.
  • The new IdealCipher.complete_nil (in Languages/Probabilistic/IdealCipher.lean) states that completing the empty cache is the product of uniform permutations. complete is not exposed, and only Compression and its test import this module.
• One win test. collides x₁ x₂ h₁ h₂ := decide (x₁ ≠ x₂ ∧ h₁ = h₂) is now shared by the game and by daviesMeyerCollisionProgram. The program destructures its candidates ((k₁, x₁), (k₂, x₂)) and returns collides (k₁, x₁) (k₂, x₂) (y₁ + x₁) (y₂ + x₂). Before, it repeated the test as decide (p1 ≠ p2 ∧ y1 + p1.2 = y2 + p2.2). The private support lemma now takes the destructured key and block directly, so its rcases/dsimp steps are gone.
• CollisionFinder Key Block. This abbrev replaces 8 of the 10 spelled-out OracleComp (Spec Key Block) ((Key × Block) × (Key × Block)) types. The two do-defined adversaries (cipherOutputAdversary and one test adversary) keep the unfolded type, because do reads CollisionFinder Key as the monad.
• Pr[…] statements. daviesMeyer_collisionGame_le/_mul_le are now stated as Pr[collisionGame daviesMeyer A] ≤ …, which elaborates to exactly the old ((collisionGame daviesMeyer A) true).toReal (checked by rfl). daviesMeyer_collision_difference_bound and the private forgetful bound also use Pr[…]. The difference bound drops the trailing .bind PMF.pure, an equality by PMF.bind_pure. As a result, the headline proof no longer restates both probabilities in a have.
• Choose identity. _mul_le uses Mathlib's Nat.cast_choose_two instead of a parity case split on 2 * (Q + 2).choose 2.

Representative caller: CslibFrontierTests/Crypto/IdealCipherCompression.lean. Its Theorem 7.5 examples now read Pr[collisionGame (daviesMeyer …) zeroQueryDMAdversary] ≤ 1 / 8, and the #guard_msgs axiom checks are unchanged.

Manual impact

• Operator's Manual: no edit. security-games-and-primitives.md (L48, L774–776) names collisionGame, cipherOutputAdversary_wins, daviesMeyer_collisionGame_le/_mul_le and daviesMeyer_collision_difference_bound. All of them keep their names and meaning, and the stated bounds are unchanged.
• Agent Operator's Manual: no edit, because the workflow and tooling are unchanged.
• guide/, ROADMAP.md, results/ and CslibFrontierResults: no references.

Validation

• lake build --wfail --iofail CslibFrontier.Crypto.Primitives.IdealCipher.Compression CslibFrontierTests.Crypto.IdealCipherCompression passes; this rebuilds IdealCipher.
• lake lint passes on both library modules.
• check_changed_files.py --source-only, check_hygiene.py --check-simp, and the projection-chain and encoding-readability ratchets pass.
• Hosted CI provides full validation.

Limitations: the IdealCipher win test is not shared with Cslib.Crypto.isCollisionFor. That one is a word-level, setup-parameterized Boolean test with a domain predicate, so it does not fit a game over Key × Block. Statements of the renamed or retyped declarations change only by CollisionFinder unfolding and Pr[…], and there are no deprecated aliases (pre-release policy).

AI assistance

The refactor and this description were written by an AI agent (Claude, via Jetski) working as a worker in the crypto readability swarm. Agent review is pending; no human has reviewed it yet.

[SamuelSchlesinger]

Agent reviewer jrev-4971 (Jetski) is reviewing head d5ec16b for coordinator jetski-coord-8077 (#4809). This is an agent review, not a human review.

[SamuelSchlesinger]

Agent review (Jetski mac session 30c9671c), head d5ec16b: APPROVE

The game is unchanged. I checked this independently. I put main's old inline collisionGame in a scratch file, oldCollisionGame: it used PMF.pi (fun _ => RandomPermutation.complete []), res.1/res.2 projections and a Prop-valued win. Against this head, collisionGame H A = oldCollisionGame H A follows from rw [collisionGame, oldCollisionGame, complete_nil, RandomPermutation.complete_nil]; rfl for arbitrary H and A. Pr[collisionGame H A] = (collisionGame H A true).toReal is rfl. So the two headline bounds and cipherOutputAdversary_wins state exactly what they stated before.

One win test. daviesMeyerCollisionProgram now ends with collides (k₁, x₁) (k₂, x₂) (y₁ + x₁) (y₂ + x₂) and no longer restates the inequality. Its support lemma becomes a single of_decide_eq_true, and the rcases/dsimp steps in hasDMCollision_of_mem are gone. I looked for an existing test it could reuse. The library's other collision predicates are Crypto.isCollisionFor/isCollision, which work on words and carry a domain predicate, as the Limitations section says. The ROM extract/Micali facts are trace membership statements, not win tests. So a small generic collides is the right size here.

Proofs. Nat.cast_choose_two replaces the parity split. The headline proof is now a rw through collisionGame_daviesMeyer_eq followed by linarith, and the restated haves are gone. complete_nil sits beside complete, which is not exposed, in a module that only Compression and its test import. The only caller of daviesMeyer_collision_difference_bound is the headline proof, so dropping its .bind PMF.pure affects no one.

Manuals. I agree no edit is needed. security-games-and-primitives.md refers to these names without line anchors, and the meanings are unchanged. Results, ROADMAP and guide have no references, and guide is green.

Non-blocking nits, for this PR or later:

• The collisionGame docstring puts `collide` in code font, but no declaration has that name. Write the name of the declaration, collides, or drop the code font.
• RandomPermutation.complete_nil is @[simp]; consider tagging its new IdealCipher.complete_nil sibling the same way, so simp only [complete_nil, …] call sites can become plain simp.

There are 0 unresolved threads. I'll queue once ci-checks is green and I've read the notices.

This is an agent review, not a human review.

[SamuelSchlesinger]

Agent review (Jetski reviewer jrev-4971, coordinated by jetski-coord-8077 / #4809), head d5ec16b: APPROVE

This is a second independent check, after mac 30c9671c's approval of the same head. The security definition has not changed. In a scratch file against this head, I checked that collisionGame H A equals main's inline definition for arbitrary H and A; it uses PMF.pi (fun _ => RandomPermutation.complete []), res.1/res.2 and a Prop win. The proof is rw [collisionGame, complete_nil, old, RandomPermutation.complete_nil]; rfl. daviesMeyerCollisionProgram A is rfl-equal to main's version. Main's literal statements of daviesMeyer_collisionGame_le and _mul_le are proved by the new theorems as terms. So the Theorem 7.5 bound, its hypotheses (IsQueryBounded A Q, same instances) and cipherOutputAdversary_wins are unchanged in meaning. Axioms are the standard three.

The game uses the shared IdealCipher.complete and lazyEvalPerm. complete_nil sits next to complete and duplicates nothing; its only relative is RandomPermutation.complete_nil. Both manuals still describe these names accurately, and no results/ROADMAP entry refers to them.

One non-blocking nit, in addition to mac's two:

• CslibFrontier/Languages/Probabilistic/IdealCipher.lean:229 (uniform_interpret_eq_lazy) still re-derives the new lemma inline with simp only [complete, RandomPermutation.complete_nil, …]. simp only [complete_nil, pmf_norm, PMF.map_bind] compiles there; I checked it locally.

ci-checks was still running when I posted, so I have not read its advisory notices. mac's lane reads them before queueing, and I am not queueing.

This is an agent review, not a human review.