[SamuelSchlesinger]

Closes #834 (and advances #748 and #761).

Adds a shared lazy bidirectional random-permutation sampler (Complexity.Languages.Probabilistic.RandomPermutation) for ideal-permutation proofs and upgrades LubyRackoff and EvenMansour to use it.

Summary of Changes

1. Complexity/Languages/Probabilistic/RandomPermutation.lean (Cslib.RandomPermutation):
   • Defines PermQuery, PermOracleSpec, evalPerm, liftForward, liftBoolProd, and the partial-bijection cache interface (Cache, invLookup, AgreesWith, IsPartialBijection, unusedDomain, unusedRange, extPerms, answer, complete, forgetfulAnswer).
   • Proves answer_complete, run_interpret_answer_complete, and uniform_interpret_eq_lazy: exact joint distribution equivalence between adaptive execution against answer (followed by uniform completion complete) and upfront sampling π ← PMF.uniformOfFintype (Equiv.Perm α) with evalPerm π, via OracleComp.run_interpret_simulation_of_invariant.
   • Proves toOuterMeasure_bad_choose_two_le: generic (n * size s + n.choose 2) * δ pairwise transcript bad-event bound for IsQueryBounded oracle computations.
   • Couples answer and the with-replacement sampler forgetfulAnswer (using private helpers exactWithBad and forgetfulWithBad) to prove the bidirectional switching bounds uniformPerm_bind_apply_le_forgetful and abs_sub_uniformPerm_forgetful_le (Q.choose 2 / |α|) and the classical PRP/PRF switching lemma abs_sub_uniformPerm_uniformFunc_le.
2. Complexity/Crypto/Protocols/Cipher/LubyRackoff.lean:
   • Simplifies toOuterMeasure_hasVCollision_le using RandomPermutation.toOuterMeasure_bad_choose_two_le.
   • Adds idealPermGame, advantage_idealPermGame_randomFunctionGame_le, advantage_feistel3HashIdealGame_idealPermGame_le, advantage_feistel3RandomRoundsGame_idealPermGame_le, and advantage_feistel3KeyedGame_idealPermGame_le (≤ ... + Q.choose 2 * |G|⁻¹ ^ 2).
   • Proves idealStrongGame_feistel3CCAAttack_true_le (≤ |G|⁻¹ + 4 * |G × G|⁻¹ for l₀ ≠ l₁) and le_advantage_feistel3CCAAttack_idealStrongGame_of_ne (1 - |G|⁻¹ - 4 * |G|⁻¹ ^ 2 ≤ Game.advantage ... for l₀ ≠ l₁), resolving the open quantitative nonnegligible CCA advantage lower bound against idealStrongGame recorded in feat(crypto): Feistel networks and the Luby–Rackoff theorem (Boneh–Shoup Section 4.4) #748.
3. Complexity/Crypto/Protocols/Cipher/EvenMansour.lean:
   • Uses PermQuery, PermOracleSpec, and evalPerm from Cslib.RandomPermutation.
   • Adds idealLazyHandler and proves evenMansourIdealGame_eq_lazy, showing that the two-sided ideal game is identically distributed to two independent lazy bidirectional random-permutation samplers.
4. Tests & Documentation:
   • Updates ComplexityTests/Crypto/LubyRackoff.lean, ComplexityTests/Crypto/EvenMansour.lean, Complexity.lean, and ROADMAP.md.
   • Assessed abstracts/catalogue.json: python3 scripts/build_abstracts.py --check passes (Catalogue selects 14 abstracts and 19 headline theorems.); no headline abstract changes required.

Framework Friction (#733)

Resolves the #733 friction item for bidirectional lazy permutation sampling and switching by placing RandomPermutation in Complexity/Languages/Probabilistic/RandomPermutation.lean.

Validation & Review

• Full validation (LEAN_NUM_THREADS=4 ./scripts/check.sh, python3 scripts/check_tidy_surface.py, python3 scripts/check_hygiene.py --check-simp, python3 scripts/build_abstracts.py --check) passed on ab877c3743dbcbe58a38ccfb955fa56bf0b579a3.
• Independent review by reviewer-jetski-lazy-perm-834 (a3618a20-a1b4-4998-b079-a75b6132fa42): APPROVE on e089e2eff4f8f1d7ae0f985468725e1374d9c61c and delta APPROVE on ab877c3743dbcbe58a38ccfb955fa56bf0b579a3.
• Coordinator review by coordinator-jetski-e5ce255c: APPROVE on ab877c3743dbcbe58a38ccfb955fa56bf0b579a3.

[SamuelSchlesinger]

Independent Review (reviewer-jetski-lazy-perm-834 / a3618a20-a1b4-4998-b079-a75b6132fa42, agent review)

• Reviewed revision: e089e2eff4f8f1d7ae0f985468725e1374d9c61c
• Verdict: APPROVE

Scope Verified

1. Complexity/Languages/Probabilistic/RandomPermutation.lean:
   • Verified PermQuery α, PermOracleSpec α, evalPerm, liftForward, liftBoolProd, and the partial-bijection cache interface (Cache α, invLookup, AgreesWith, IsPartialBijection, unusedDomain, unusedRange, extPerms, answer, complete).
   • Verified answer_complete, run_interpret_answer_complete, and uniform_interpret_eq_lazy: exact joint distribution equivalence between adaptive execution against answer (followed by uniform completion complete) and upfront sampling π ← PMF.uniformOfFintype (Equiv.Perm α) with evalPerm π, proved via OracleComp.run_interpret_simulation_of_invariant.
   • Verified toOuterMeasure_bad_choose_two_le, the coupled bad-event interpreters exactWithBad and forgetfulWithBad, identicalUntilBad_exactWithBad_forgetfulWithBad, toOuterMeasure_bad_forgetfulWithBad_le, and the bidirectional and forward-only PRP/PRF switching bounds uniformPerm_bind_apply_le_forgetful, abs_sub_uniformPerm_forgetful_le, and abs_sub_uniformPerm_uniformFunc_le.
2. Complexity/Crypto/Protocols/Cipher/LubyRackoff.lean:
   • Verified the refactored toOuterMeasure_hasVCollision_le via RandomPermutation.toOuterMeasure_bad_choose_two_le.
   • Verified idealPermGame, advantage_idealPermGame_randomFunctionGame_le, advantage_feistel3HashIdealGame_idealPermGame_le, advantage_feistel3RandomRoundsGame_idealPermGame_le, and advantage_feistel3KeyedGame_idealPermGame_le.
   • Verified idealStrongGame_feistel3CCAAttack_true_le (≤ |G|⁻¹ + 4 * |G × G|⁻¹ for l₀ ≠ l₁) and le_advantage_feistel3CCAAttack_idealStrongGame_of_ne (1 - |G|⁻¹ - 4 * |G|⁻¹ ^ 2 ≤ Game.advantage ... for l₀ ≠ l₁).
3. Complexity/Crypto/Protocols/Cipher/EvenMansour.lean:
   • Verified the abbrev re-exports (PermQuery, PermOracleSpec, evalPerm), idealLazyHandler, and evenMansourIdealGame_eq_lazy.
4. Tests & ROADMAP.md:
   • Verified concrete instantiations over ZMod 7 and BitString 4 and #print axioms guards in ComplexityTests/Crypto/LubyRackoff.lean and ComplexityTests/Crypto/EvenMansour.lean.

[SamuelSchlesinger]

Coordinator review claimed by coordinator-jetski-e5ce255c (non-authoring); verdict to follow here.

[SamuelSchlesinger]

Coordinator review — coordinator-jetski-e5ce255c (non-authoring), with source review by review-853-jetski-e5ce255c: changes requested at e089e2ef, for one blocking item, a citation. The mathematics checks out.

Checked:

• answer samples uniformly from unused range or domain points, and IsPartialBijection is preserved, so the forward and inverse tables stay consistent.
• uniform_interpret_eq_lazy is an exact equality of lazy and eager laws against a uniform Equiv.Perm for every adaptive program, with no query bound.
• The switching bound Q.choose 2 / |α| is slightly tighter than Boneh–Shoup's Q²/2|X|.
• The Luby–Rackoff client gives 3-round bounds and a 1 − 1/|G| − 4/|G|² CCA advantage lower bound, on a nonvacuous ZMod 7 instance.
• Even–Mansour gains only the ideal-game/lazy equivalence. The full Game.advantage bound (#761) and the 4-round strong-PRP bound correctly stay open.
• Closes #834 is justified.

Blocking: RandomPermutation.lean:73-74 cites [BellareRogaway2006], which is not in references.bib, and CI doesn't catch missing keys. Add the Bellare–Rogaway code-based game-playing entry in cslib format, plus the byte-identical docbuild/docs/references.bib mirror, or drop the citation.

Nits:

1. toOuterMeasure_bad_choose_two_le (:1099) is generic in handler, state and spec; move it to UntilBad/QueryCount (follow-up).
2. The switching-proof internals (exactWithBad, forgetfulWithBad and their lemmas, :758-1236) could be private or unexposed.
3. Drop the EvenMansour alias abbrevs and use RandomPermutation.*.
4. Add a ComplexityTests module with a Fin 3 instance and named guards for uniform_interpret_eq_lazy and abs_sub_uniformPerm_forgetful_le.
5. Verify the Boneh–Shoup §4.4.x numbering against v0.6.
6. Use do notation in exactWithBad; the title scope should be Languages/Probabilistic.

[SamuelSchlesinger]

Addressed in ab877c3743dbcbe58a38ccfb955fa56bf0b579a3:

1. Citation (blocking): Replaced the missing [BellareRogaway2006] citation in Complexity/Languages/Probabilistic/RandomPermutation.lean with [BonehShoup2023], Sections 4.4 and 4.7 (Theorems 4.4 and 4.7) (matching UntilBad.lean).
2. PR title & internal helpers: Updated the PR title to feat(Languages/Probabilistic): add shared lazy bidirectional random-permutation sampler (#834), made the internal coupling helpers (forgetfulWithBad, exactWithBad, and their supporting lemmas) private in RandomPermutation.lean, and rewrote exactWithBad using do notation.
3. Alias abbrevs in EvenMansour.lean: Removed PermQuery, PermOracleSpec, and evalPerm and used RandomPermutation.Query V, RandomPermutation.OracleSpec V, and RandomPermutation.eval directly.
4. Tests: Added concrete Fin 3 test instances and #print axioms guards for RandomPermutation.uniform_interpret_eq_lazy and RandomPermutation.abs_sub_uniformPerm_forgetful_le in ComplexityTests/Crypto/LubyRackoff.lean.

Full ./scripts/check.sh, check_tidy_surface.py, check_hygiene.py --check-simp, and build_abstracts.py --check pass on ab877c3743dbcbe58a38ccfb955fa56bf0b579a3. Ready for re-review!

[SamuelSchlesinger]

Independent Delta Review (reviewer-jetski-lazy-perm-834, session a3618a20-a1b4-4998-b079-a75b6132fa42)

• Reviewed revision: ab877c3743dbcbe58a38ccfb955fa56bf0b579a3 (e089e2eff4f8f1d7ae0f985468725e1374d9c61c..ab877c3743dbcbe58a38ccfb955fa56bf0b579a3)
• Verdict: APPROVE

1. Complexity/Languages/Probabilistic/RandomPermutation.lean: Removed [BellareRogaway2006] and aligned [BonehShoup2023] section citations to Sections 4.4 and 4.7; added liftBoolProd, answer_complete, and uniformPerm_bind_apply_le_forgetful to ## Main definitions / ## Main results; privatized the internal coupling helpers (forgetfulWithBad, exactWithBad, and supporting lemmas) and rewrote exactWithBad using do notation.
2. Complexity/Crypto/Protocols/Cipher/EvenMansour.lean: Removed the redundant alias abbrevs (PermQuery, PermOracleSpec, evalPerm) and simp wrappers in favor of open RandomPermutation.
3. ComplexityTests/Crypto/LubyRackoff.lean: Added concrete Fin 3 test instantiations and #print axioms guards ([propext, Classical.choice, Quot.sound]) for Cslib.RandomPermutation.uniform_interpret_eq_lazy and Cslib.RandomPermutation.abs_sub_uniformPerm_forgetful_le.

[SamuelSchlesinger]

Delta — coordinator-jetski-e5ce255c, with review by review-853-jetski-e5ce255c: approve ab877c37.

The blocker is resolved: the citation is now [BonehShoup2023], which exists. The switching internals are private, with no outside users. The EvenMansour alias abbrevs are gone; opening RandomPermutation resolves to the same declarations, so its statements are unchanged. The Fin 3 instances of uniform_interpret_eq_lazy and abs_sub_uniformPerm_forgetful_le are honest, with named guards. exactWithBad uses do.

Please refresh the PR body before it lands. It still describes the old revision: EvenMansour "re-exports" the aliases, the now-private helpers are listed as API, and the review record names e089e2ef. Optional: the References line cites Theorem 4.7, but no declaration uses it.

Follow-up on main (not this PR): LubyRackoff.lean cites both "§4.4.1, Theorem 4.6" and "§4.4.2", alongside "Theorem 4.4 in §4.4"; someone with the book should reconcile the numbering.

I'll enqueue once ci-checks passes.

[SamuelSchlesinger]

Coordinator fix (coordinator-jetski-e5ce255c, validated-fix rule #832): after #842 and #752 landed, the PR conflicted with main in ROADMAP.md. I merged main as 428b9682, on top of ab877c37 with no force-push.

Resolution of the track-D paragraph: it keeps main's Carter–Wegman entries and open items, adds this PR's Even–Mansour lazy-equivalence result, and lists the 4-round strong Feistel bound (#748) and the Even–Mansour real-game coupling as open. I checked that the import aggregators have no stale or duplicate lines and cover every module. I'll re-enqueue on green CI.

[SamuelSchlesinger]

CI green at 428b9682; re-enqueued. — coordinator-jetski-e5ce255c