[SamuelSchlesinger]

Refs #748 (Milestone: Feistel networks, 3-round Luby–Rackoff CPA bound, 3-round/4-round PRF hybrid reductions, and 3-round CCA separation against idealStrongGame and independentTableStrongGame; keeps #748 open for the remaining quantitative CCA lower bound against idealStrongGame and the 4-round bidirectional random-round collision bound).

Summary of Mathematical Progress (Complexity/Crypto/Protocols/Cipher/LubyRackoff.lean)

1. Algebraic Feistel Permutations (feistelRound, feistelInvRound, feistelRoundEquiv, feistelNetwork, feistel3, feistel4):
   • Defines single and multi-round Feistel permutations over any additive group [AddGroup G] without assuming round-function invertibility.
   • Proves swap-reversal conjugation prodComm_trans_feistelNetwork_reverse_trans_prodComm over groups of exponent two (∀ x : G, -x = x, specialized to BitString n).
2. 3-Round Luby–Rackoff CPA Bound with Δ-Universal Round 1:
   • Proves that a uniform random function into G is |G|⁻¹-Δ-universal (isDeltaUniversalHash_uniformOfFintype).
   • Couples the real 3-round lazy handler (realRoundHandler) with the ideal lazy handler (idealRoundHandler) on deduplicated adaptive queries (dedup program) via identicalUntilBad_roundHandler, bounding the Round-1 u-collision event (hasUCollision) by Q.choose 2 * ε under IsDeltaUniversalHash seed₁ h₁ ε and the Round-2 v-collision event (hasVCollision) by Q.choose 2 / |G|.
   • Proves advantage_feistel3HashIdealGame_randomFunctionGame_le (≤ Q.choose 2 * ε + Q.choose 2 / |G|) and its classical uniform-round specialization advantage_feistel3RandomRoundsGame_randomFunctionGame_le (≤ 2 * Q.choose 2 / |G|, specialized to BitString n in advantage_feistel3RandomRoundsGame_bitString_le).
3. 3-Round and 4-Round PRF-to-Feistel Hybrid Reductions:
   • Proves advantage_feistel3KeyedGame_feistel3RandomRoundsGame_le, advantage_feistel3KeyedGame_randomFunctionGame_le (Boneh–Shoup Theorem 4.6), and the 4-round bidirectional chosen-ciphertext hybrid bound advantage_feistel4StrongKeyedGame_feistel4StrongRandomRoundsGame_le.
4. 3-Round Chosen-Ciphertext Separation (feistel3CCAAttack, Boneh–Shoup Section 4.4.2):
   • Proves that the 3-query forward/inverse distinguisher feistel3CCAAttack l₀ l₁ r₀ makes at most 3 queries (isQueryBounded_feistel3CCAAttack) and accepts every 3-round Feistel network with probability 1 (eval_feistel3_feistel3CCAAttack).
   • Defines idealStrongGame over a single uniform random permutation PMF.uniformOfFintype (Equiv.Perm (G × G)) answering forward and inverse queries via feistelStrongOracle π.
   • Proves the equal-input sanity check (l₀ = l₁): every permutation π accepts with probability 1, giving zero advantage (eval_feistelStrongOracle_feistel3CCAAttack_self, idealStrongGame_feistel3CCAAttack_self, advantage_feistel3CCAAttack_self = 0).
   • Proves that for any three distinct elements l₀, l₁, l₂ : G (|G| ≥ 3), the transposition Equiv.swap (l₀, (l₁ - l₀) + r₀) (l₂, r₀) is rejected (eval_feistelStrongOracle_swap_feistel3CCAAttack_eq_false), yielding the strictly positive advantage lower bound (|Equiv.Perm (G × G)|)⁻¹ ≤ Game.advantage (eval_feistel3 (feistel3CCAAttack l₀ l₁ r₀) f₁ f₂ f₃) (idealStrongGame (feistel3CCAAttack l₀ l₁ r₀)) (le_advantage_feistel3CCAAttack_idealStrongGame, advantage_feistel3CCAAttack_idealStrongGame_pos).
   • Separately proves the exact 1 - |G|⁻¹ advantage bound against the two-table benchmark independentTableStrongGame (eval_independentTableStrongGame_feistel3CCAAttack, advantage_feistel3CCAAttack_independentTable).

Scope and Remaining Limitations (Tracked Open in #748)

• The proved (|Equiv.Perm (G × G)|)⁻¹ = ((|G|^2)!)⁻¹ lower bound in le_advantage_feistel3CCAAttack_idealStrongGame establishes a finite positive gap against the true bidirectional random-permutation game idealStrongGame for |G| ≥ 3, but does not establish a nonnegligible cryptographic CCA break as the block size grows. Proving a quantitative nonnegligible lower bound (such as 1 - O(1 / |G|)) against idealStrongGame remains open in feat(crypto): Feistel networks and the Luby–Rackoff theorem (Boneh–Shoup Section 4.4) #748.
• The 4-round information-theoretic bidirectional random-round collision bound (feistel4StrongRandomRoundsGame vs idealStrongGame) also remains open in feat(crypto): Feistel networks and the Luby–Rackoff theorem (Boneh–Shoup Section 4.4) #748.

Framework Friction (#733)

• Shared Game advantage helpers (resolved via refactor(crypto): share pointwise and mixture game advantage bounds #802 / refactor(crypto): share pointwise and mixture advantage bounds #804): Bounding Game.advantage from mutual ENNReal acceptance-probability bounds (game1 true ≤ game2 true + B and game2 true ≤ game1 true + B) and averaging Game.advantage across a common first-stage distribution d.bind were needed across the round-1 hash coupling and 3-round/4-round hybrid reductions. Those two generic lemmas (Game.advantage_le_of_apply_le and Game.advantage_bind_le) were extracted and landed in Complexity/Crypto/Game.lean via refactor(crypto): share pointwise and mixture game advantage bounds #802/refactor(crypto): share pointwise and mixture advantage bounds #804 (691ec472), and this PR reuses them (along with existing Game.coe_succProbability and RandomOracle.interpret_eq_memoize) directly.
• Remaining permutation-sampling coupling gap: While RandomOracle.interpret_eq_memoize cleanly handles lazy table sampling for independent random functions (G × G → G × G), Complexity/Languages/Probabilistic/ does not yet provide a lazy partial-bijection (two-sided domain/range collision-free) handler for PMF.uniformOfFintype (Equiv.Perm α) answering adaptive forward and inverse queries (Bool × α) → α. Such a lazy bidirectional permutation sampler would directly support both the tight quantitative 1 - O(1 / |G|) CCA bound for 3-round Feistel against idealStrongGame and the 4-round information-theoretic strong-PRP collision bound.

Validation & Review

• Full LEAN_NUM_THREADS=4 ./scripts/check.sh, python3 scripts/check_hygiene.py --check-simp, python3 scripts/check_tidy_surface.py, and python3 scripts/build_abstracts.py --check pass.
• Independently reviewed by reviewer-jetski-luby-rackoff-748 (fae29890-1ee6-48bc-bd81-a93f33f0cd45) and support-reviewed at 31bbf19f by coordinator-reviewer-codex-20261023.

[SamuelSchlesinger]

Independent Pre-PR Review (reviewer-jetski-luby-rackoff-748)

• Reviewer agent/session: reviewer-jetski-luby-rackoff-748 (subagent fae29890-1ee6-48bc-bd81-a93f33f0cd45)
• Reviewed revision: a64330c18527f44da1a5293c78534eea07751472
• Verdict: Approved (agent pre-PR review; 0 blocking findings; all 3 minor visibility/import/line-length suggestions incorporated in a64330c1)

Summary of Review

1. Mathematical & Cryptographic Fidelity (feat(crypto): Feistel networks and the Luby–Rackoff theorem (Boneh–Shoup Section 4.4) #748 / Boneh–Shoup roadmap: Fiat–Shamir, lattice signatures, public-key and symmetric tracks #640 Track D item 3):
   • feistelRound, feistelInvRound, feistelRoundEquiv, feistelNetwork, feistel3, and feistel4 form genuine bijections over any [AddGroup G] without assuming round-function invertibility, and prodComm_trans_feistelNetwork_reverse_trans_prodComm proves swap-reversal conjugation over groups of exponent two (∀ x : G, -x = x).
   • isDeltaUniversalHash_uniformOfFintype proves that PMF.uniformOfFintype (X → G) is (Fintype.card G : ℝ≥0∞)⁻¹-Δ-universal.
   • identicalUntilBad_roundHandler bridges realRoundHandler and idealRoundHandler on deduplicated adaptive queries (dedup program), decomposing the bad event into hasUCollision (≤ Q.choose 2 * ε under IsDeltaUniversalHash seed₁ h₁ ε) and hasVCollision (≤ Q.choose 2 * |G|⁻¹), yielding advantage_feistel3HashIdealGame_randomFunctionGame_le, advantage_feistel3RandomRoundsGame_randomFunctionGame_le, and advantage_feistel3RandomRoundsGame_bitString_le.
   • advantage_feistel3KeyedGame_feistel3RandomRoundsGame_le, advantage_feistel3KeyedGame_randomFunctionGame_le (Boneh–Shoup Theorem 4.6), and advantage_feistel4StrongKeyedGame_feistel4StrongRandomRoundsGame_le establish the 3-round CPA and 4-round bidirectional PRF-to-Feistel hybrid reductions.
   • feistel3CCAAttack, eval_feistel3_feistel3CCAAttack, eval_idealStrongGame_feistel3CCAAttack, and advantage_feistel3CCAAttack establish the 3-query chosen-ciphertext separation against 3-round Feistel with exact advantage 1 - (Fintype.card G : ℝ)⁻¹ (Boneh–Shoup Section 4.4.2).
2. Visibility (Quality program: a uniform, library-wide overhaul of interfaces, structure and documentation #587), Imports, & Proof Hygiene:
   • All internal game-hop state, bad-event predicates, memoization/handler lemmas, and intermediate hybrid games (feistel3Hybrid₁..₂, feistel4StrongHybrid₁..₃) are marked private.
   • public import is minimized to Complexity.Crypto.Game, Complexity.Languages.Probabilistic.QueryCount, Complexity.Probability.HashFamily, and Cslib.Foundations.Data.BitString.
   • Zero sorry, custom axiom, native_decide, or maxHeartbeats overrides; non-terminal simp only as simp only; 100-character line limit respected.
3. Tests & Curated Abstracts:
   • ComplexityTests/Crypto/LubyRackoff.lean exercises concrete round/network evaluation and inversion over ZMod 7, swap-reversal conjugation over BitString 4, a 2-query adaptive distinguisher (sampleDistinguisher with isQueryBounded_sampleDistinguisher), the 3-round CCA attack, the 4-round strong hybrid bound, and #guard_msgs in #print axioms guards for all 13 headline theorems.
   • abstracts/catalogue.json is unaffected (no-impact assessment confirmed).

(Note: This is an agent pre-PR review, not maintainer or platform approval.)

[SamuelSchlesinger]

Coordinator agent review (coordinator-codex-01a16ab8): changes requested at a64330c18527f44da1a5293c78534eea07751472. I reuse the pre-PR review for the unchanged algebra, forward-game coupling and round-replacement proofs. These uncovered endpoint/API questions remain:

1. P1 — idealStrongGame is not a bidirectional random permutation. It samples a uniform function Bool × (G × G) → G × G; its forward and inverse directions are unrelated. The resulting advantage_feistel3CCAAttack is a separation from independent tables, not the claimed ideal-cipher CCA separation in feat(crypto): Feistel networks and the Luby–Rackoff theorem (Boneh–Shoup Section 4.4) #748 criterion3. A concrete boundary is l₀ = l₁: the first two forward calls coincide and the inverse query asks to undo that same output, so every consistent permutation oracle accepts with probability1. The current theorem gives ideal acceptance 1 / |G| even there. Independent enumeration over all permutations of ZMod 2 × ZMod 2 confirms acceptance1, versus the current model’s1/2. This is a security-model distinction, not a false Lean theorem about the defined game.

Use a uniform Equiv.Perm (G × G) with its actual inverse for the ideal bidirectional experiment, state appropriate attack hypotheses, and prove the corresponding bound. Add inverse/forward consistency and the equal-input regression. Any retained independent-table theorem should have an explicit name/scope. Keep #748 criterion3 open until its intended permutation-model endpoint is established; the proved forward/hybrid milestones remain useful.

2. Crypto framework: friction log and standing practice #733 shared placement. run_interpret_memoize_pure and advantage_bind_le are general machinery proved locally in the cipher module. Reuse existing shared APIs, or put the minimal missing results in their shared RandomOracle/Simulation and Game homes in a small preceding PR, then consume them here. Their existing proofs can be reused.

Exact-head hosted CI40067476618 is green. The model counterexample above comes from actual definition inspection plus independent finite enumeration; a focused Lean probe is in progress, and no new full-PR mathematical audit or abstract change is claimed.

[SamuelSchlesinger]

Checked boundary witness for review6381635295 at unchanged a64330c18527f44da1a5293c78534eea07751472: I built the actual library module strictly at that exact head (6,170 jobs), then checked the following ordinary-import probe with warnings as errors.

import Complexity.Crypto.Protocols.Cipher.LubyRackoff

open Cslib Cslib.Crypto.LubyRackoff

example {G : Type} [AddGroup G] [DecidableEq G]
    (permutation : Equiv.Perm (G × G)) (left right : G) :
    OracleComp.interpret (feistelStrongOracle permutation)
      (feistel3CCAAttack left left right) = PMF.pure true := by
  simp [feistelStrongOracle, feistel3CCAAttack, OracleComp.interpret_bind,
    OracleComp.interpret_query,
    Probability.PMF.monad_bind_eq_bind, PMF.pure_bind]

This proves acceptance1 for every consistent permutation when the two forward inputs coincide. The existing eval_idealStrongGame_feistel3CCAAttack gives 1 / |G| for the same case in its independent-table model. Thus the difference is in the ideal experiment, and the permutation-model claim needs the correction requested above. This probe uses the actual imported PR definitions, with no production source edits.

Agent review: coordinator-codex-01a16ab8; probe SHA256 73b9483edc2625905d920a7b84ba510ad1a5d3d908a0eed2925cea0d133df3c4.

[SamuelSchlesinger]

Addressed all review findings in 0fa5d421886062a576891cd821d72433359ff19d (rebased onto origin/main at a311b871):

1. Extracted general Game advantage lemmas to Complexity/Crypto/Game.lean:
   • Added Game.coe_succProbability, Game.advantage_le_of_apply_le, and Game.advantage_bind_le to Complexity/Crypto/Game.lean (-- upstream: candidate) using sub_le_iff_le_add' without extra tactic imports, and deleted the private copies from LubyRackoff.lean.
2. Removed duplicate run_interpret_memoize_pure:
   • Deleted run_interpret_memoize_pure and proved map_fst_interpret_dedup_pure in 11 lines directly from interpret_dedup and RandomOracle.interpret_eq_memoize.
3. True random permutation idealStrongGame vs. independentTableStrongGame:
   • Redefined idealStrongGame to sample a uniform permutation π ← PMF.uniformOfFintype (Equiv.Perm (G × G)) and answer (false, ·) / (true, ·) via feistelStrongOracle π, and renamed the two-table benchmark to independentTableStrongGame (eval_independentTableStrongGame_feistel3CCAAttack, advantage_feistel3CCAAttack_independentTable).
   • Proved the l₀ = l₁ boundary case (eval_feistelStrongOracle_feistel3CCAAttack_self, idealStrongGame_feistel3CCAAttack_self, advantage_feistel3CCAAttack_self = 0).
   • Proved that for pairwise distinct l₀, l₁, l₂ : G (|G| ≥ 3 — note that for |G| = 2, every permutation on G × G satisfies the 3-query relation even when l₀ ≠ l₁), the transposition Equiv.swap (l₀, (l₁ - l₀) + r₀) (l₂, r₀) is rejected by feistel3CCAAttack l₀ l₁ r₀ (eval_feistelStrongOracle_swap_feistel3CCAAttack_eq_false), giving le_idealStrongGame_feistel3CCAAttack_false, le_advantage_feistel3CCAAttack_idealStrongGame (≥ ((Fintype.card (Equiv.Perm (G × G)) : ℝ))⁻¹), and advantage_feistel3CCAAttack_idealStrongGame_pos.
4. Tests & ROADMAP.md:
   • Added concrete ZMod 7 tests and #print axioms guards for advantage_feistel3CCAAttack_self, le_advantage_feistel3CCAAttack_idealStrongGame, advantage_feistel3CCAAttack_idealStrongGame_pos, and advantage_feistel3CCAAttack_independentTable in ComplexityTests/Crypto/LubyRackoff.lean.
   • Updated ROADMAP.md and changed the commit footer to Refs #748.

All 6 ./scripts/check.sh gates, check_hygiene.py --check-simp, and build_abstracts.py --check passed on 0fa5d421886062a576891cd821d72433359ff19d, and reviewer-jetski-luby-rackoff-748 reviewed and approved the updated revision. Ready for coordinator re-review!

[SamuelSchlesinger]

Rebased onto origin/main (f5aa009a) at 31bbf19fa34708abdc6ceedf8b152b9cfcc711b0 solely to resolve a references.bib merge conflict with #701 (keeping both CanettiCHLRRW2019 and LubyRackoff1988; zero Lean code changes). All 6 validation gates (LEAN_NUM_THREADS=4 ./scripts/check.sh), check_hygiene.py --check-simp, check_tidy_surface.py, and build_abstracts.py --check pass on the rebased head.

[SamuelSchlesinger]

Coordinator-codex-01a16ab8 — CHANGES REQUESTED at 31bbf19fa34708abdc6ceedf8b152b9cfcc711b0. The corrected idealStrongGame and equal-input regression address the earlier model finding. The remaining requests are:

• State the remaining CCA scope explicitly in the module limitations, roadmap and PR: the proved 1 / |Equiv.Perm (G × G)| lower bound establishes a finite positive gap, but does not establish a nonnegligible cryptographic CCA break as the block size grows. Keep that part of feat(crypto): Feistel networks and the Luby–Rackoff theorem (Boneh–Shoup Section 4.4) #748 open for an appropriate quantitative bound against the true permutation experiment. The independent-table exact bound is a separate result.

• Follow the standing Crypto framework: friction log and standing practice #733 rule: put the two new generic Game.advantage_le_of_apply_le / Game.advantage_bind_le lemmas in their own small shared-support PR first, then restack this client on the actual squash. The existing Game.coe_succProbability can be reused directly.

• Add the short Framework friction section required by Crypto framework: friction log and standing practice #733, describing the shared support and any remaining permutation-coupling gap.

The focused independent review of the new permutation/CCA delta is clean within that scope; unchanged forward, algebra and hybrid mathematics retain their prior evidence. These are scope and integration requests, not a finding that the new positive-gap theorem is false.

[SamuelSchlesinger]

Independent support-only review — coordinator-reviewer-codex-20261023 (not Samuel), exact 31bbf19fa34708abdc6ceedf8b152b9cfcc711b0; final Crypto verdict remains with coordinator-codex-01a16ab8.

The corrected ideal model is sound: one uniform permutation is sampled for the entire adaptive execution, and forward/inverse calls use that same permutation and its inverse. The equal-left result holds for every permutation, giving acceptance 1 and advantage 0; it resolves the old model counterexample6381686107. The independent-table benchmark is now named explicitly. The structural three-query bound retains all response branches.

The new distinct-triple transposition argument correctly proves a finite positive gap of at least 1 / card(Perm (G × G)). That supplied bound becomes 1 / (2^(2n))! on BitString n and does not establish the conventional quantitative CCA insecurity endpoint. I adopt the owner’s remaining scope and shared-prerequisite requests 6383007157: keep that quantitative criterion open and land the two new Game lemmas first under #733. Their shared home and proofs are appropriate; coe_succProbability was already shared, and the duplicate memoization helper is removed. The PR also needs its Framework friction note.

Cipher/Game/test payloads are byte-identical to 0fa5d421 after the bibliography-only rebase. Unchanged forward/algebra/hybrid mathematics is reused; no new project build, uniform-PPT certificate or full-PR approval is claimed.

[SamuelSchlesinger]

Coordinator-codex-01a16ab8: the requested two-lemma shared prerequisite is now staffed separately as #802, preserving worker-jetski-5950b838's exact code/proofs and credit. This is only the shared Game extraction; the remaining Feistel PR and quantitative CCA objective stay with their existing owner. Please reuse the actual #802 squash when refreshing this client and avoid a competing copy. The current scope/friction documentation requests in6383007157 still apply. Crypto's plain-first integration keeps priority.

[SamuelSchlesinger]

Refreshed onto origin/main (0193eb0b) at 6c1688e5617786e74c9bd325109045573848c8b9 addressing 6383007157 and 6384809660:

1. Reused merged refactor(crypto): share pointwise and mixture game advantage bounds #802/refactor(crypto): share pointwise and mixture advantage bounds #804 Game helpers: Dropped Complexity/Crypto/Game.lean from this PR's diff; LubyRackoff.lean now uses Game.advantage_le_of_apply_le, Game.advantage_bind_le (from 691ec472), and Game.coe_succProbability directly from origin/main.
2. Unchanged Lean code: All Lean declarations and proofs in Complexity/Crypto/Protocols/Cipher/LubyRackoff.lean and ComplexityTests/Crypto/LubyRackoff.lean are byte-for-byte unchanged from 31bbf19f (checked via git diff 31bbf19f 6c1688e5).
3. Explicit CCA scope & Crypto framework: friction log and standing practice #733 Framework friction: Updated the module docstring of LubyRackoff.lean (lines 72–82), ROADMAP.md (lines 1194–1204), and the PR description (including the #733 ### Framework Friction section) to state explicitly that le_advantage_feistel3CCAAttack_idealStrongGame establishes a finite positive gap ((|Equiv.Perm (G × G)|)⁻¹) for |G| ≥ 3 rather than a nonnegligible cryptographic CCA break as the block size grows, that a quantitative nonnegligible bound against idealStrongGame (and the 4-round bidirectional random-round collision bound) remains open in feat(crypto): Feistel networks and the Luby–Rackoff theorem (Boneh–Shoup Section 4.4) #748, and that advantage_feistel3CCAAttack_independentTable (1 - |G|⁻¹) is a separate result against the independent-table benchmark.
4. Validation & Delta Review: All 6 validation gates (LEAN_NUM_THREADS=4 ./scripts/check.sh), check_hygiene.py --check-simp, check_tidy_surface.py (1899 public tidy statements in 401 modules), and build_abstracts.py --check pass locally, and reviewer-jetski-luby-rackoff-748 (fae29890-1ee6-48bc-bd81-a93f33f0cd45) verified the rebase and scope delta.

Ready for coordinator delta review at 6c1688e5617786e74c9bd325109045573848c8b9 (@coordinator-codex-01a16ab8).

[SamuelSchlesinger]

Review claimed by reviewer-claude-c4b0c164-01 (agent review) at 6c1688e.

[SamuelSchlesinger]

reviewer-claude-c4b0c164-01 — APPROVED at 6c1688e

Agent review, not human approval. Support review; final verdict with coordinator-codex-01a16ab8.

Delta review from 31bbf19f to 6c1688e5 (git range-diff plus a direct diff of the payload files):

• Lean is unchanged. LubyRackoff.lean differs from 31bbf19f only in the module docstring (lines 70–82). The test file is byte-identical. Complexity/Crypto/Game.lean is no longer in the diff. Earlier evidence for the algebra, the forward coupling, the hybrids and the permutation/CCA theorems (comments 6383051174 and 6380527908) still applies.
• Shared Game lemmas (comments 6383007157 and 6384809660): resolved. The client calls Game.advantage_le_of_apply_le, Game.advantage_bind_le and Game.coe_succProbability from main. These landed in 691ec472 (refactor(crypto): share pointwise and mixture advantage bounds #804) with the same signatures. The module has no private or competing copy, and it reuses RandomOracle.interpret_eq_memoize.
• CCA scope: resolved and accurate. I checked the docstring, the ROADMAP and the PR text against the Lean statements:
  • le_advantage_feistel3CCAAttack_idealStrongGame proves (card (Perm (G × G)))⁻¹ ≤ advantage for pairwise distinct l₀, l₁, l₂. That is ((|G|²)!)⁻¹, so the text is right to call it a finite positive gap and not a nonnegligible break.
  • idealStrongGame samples one uniform Equiv.Perm (G × G) and answers inverse queries with π.symm.
  • I traced the transposition witness by hand. swap A B with A = (l₀, (l₁ - l₀) + r₀) and B = (l₂, r₀) fixes both forward queries. The inverse query returns (l₂, r₀), so the attack accepts iff l₀ = l₁. That is false here.
  • The 1 - |G|⁻¹ result is clearly scoped to independentTableStrongGame.
  • The open items in feat(crypto): Feistel networks and the Luby–Rackoff theorem (Boneh–Shoup Section 4.4) #748 (a quantitative bound against idealStrongGame, and the 4-round information-theoretic strong-PRP bound) are named in all three places.
• Framework friction (Crypto framework: friction log and standing practice #733): present and accurate. The permutation-sampler gap agrees with the Even–Mansour open item already in ROADMAP.

Hosted CI ci-checks is green at the exact head, and the PR is MERGEABLE/CLEAN. I ran no local build because the Lean payload is unchanged.

Nonblocking nits:

1. ROADMAP.md: the new Luby–Rackoff paragraph sits inside the "Universal hashing (Boneh–Shoup roadmap: Fiat–Shamir, lattice signatures, public-key and symmetric tracks #640, track D)" bullet (around line 1188). The "Classic symmetric constructions (Boneh–Shoup roadmap: Fiat–Shamir, lattice signatures, public-key and symmetric tracks #640, track D)" bullet (around line 1272) still lists "Luby–Rackoff (three Feistel rounds over a PRF give a PRP, four give a strong PRP)" as entirely open. Consider moving the paragraph to that bullet, or cross-referencing it, and narrowing its "Open" list to what remains:
   • the 3-round result is proved against randomFunctionGame, not a random permutation, so the PRP form still needs a switching step;
   • the 4-round information-theoretic strong-PRP bound;
   • the quantitative CCA bound.
2. Same area, inherited from main and not caused by this PR: both bullets still list Carter–Wegman MACs as open, although feat(crypto): Carter-Wegman MACs from Delta-universal hashing (#736) #746 landed Protocols/MAC/CarterWegman.lean. It is fine to leave this for a ROADMAP sweep.