Repository navigation
refactor(crypto): share pointwise and mixture advantage bounds - #804
Merged
Merged
Conversation
Extract Game.advantage_le_of_apply_le and Game.advantage_bind_le byte-identically from 31bbf19 by worker-jetski-5950b838 (#752), preserving original source author credit. Reuse existing coe_succProbability. Focused GameBounds client checks pass strictly (6100 jobs); full required gates pending. No Feistel client/model changes or CCA completion claim. Refs #802, #733.
Collaborator
Author
|
Peer Both advantage-lemma statements and proofs are byte-identical to reviewed #752 head Exact-head CI 40099285502 is SUCCESS: all six gates and the tidy-statement ratchet passed, with the full head SHA verified. No fresh full build or Feistel/CCA audit is claimed. Ready for enqueue at this head; #752 must consume the actual support squash and retain its separate model/quantitative-scope holds. |
SamuelSchlesinger
added a commit
that referenced
this pull request
Oct 24, 2026
Formalize multi-round Feistel networks (`feistelRound`, `feistelInvRound`, `feistelRoundEquiv`, `feistelNetwork`, `feistel3`, `feistel4`, `feistelNetwork_reverse_conj_prodComm`) over arbitrary additive groups (`[AddGroup G]`) and the Luby-Rackoff theorem (Boneh-Shoup Section 4.4, Luby-Rackoff 1988) in `Complexity/Crypto/Protocols/Cipher/LubyRackoff.lean`. Address coordinator review (#752): - Rebase onto `origin/main` (`0193eb0b`) and reuse `Game.advantage_le_of_apply_le`, `Game.advantage_bind_le` (#802/#804), and `Game.coe_succProbability` directly from `Complexity.Crypto.Game` with zero changes to `Game.lean`. - Prove `map_fst_interpret_dedup_pure` in 11 lines directly from `RandomOracle.interpret_eq_memoize`, removing the private `run_interpret_memoize_pure` copy. - Define `idealStrongGame` over a uniform random permutation `PMF.uniformOfFintype (Equiv.Perm (G × G))` evaluated through `feistelStrongOracle`, and prove both the equal-input (`l₀ = l₁`) zero-advantage sanity check (`advantage_feistel3CCAAttack_self = 0`) and the finite positive advantage lower bound `(|Equiv.Perm (G × G)|)⁻¹ ≤ advantage` against `idealStrongGame` for `|G| ≥ 3` (`le_advantage_feistel3CCAAttack_idealStrongGame`, `advantage_feistel3CCAAttack_idealStrongGame_pos`). Rename the two-table benchmark to `independentTableStrongGame` / `advantage_feistel3CCAAttack_independentTable`, and record the remaining quantitative CCA and 4-round bidirectional information-theoretic bounds as open in #748. Refs #748
orbitingflea
pushed a commit
to orbitingflea/complexitylib2
that referenced
this pull request
Oct 24, 2026
…mmunity#748) (cslib-community#752) Formalize multi-round Feistel networks (`feistelRound`, `feistelInvRound`, `feistelRoundEquiv`, `feistelNetwork`, `feistel3`, `feistel4`, `feistelNetwork_reverse_conj_prodComm`) over arbitrary additive groups (`[AddGroup G]`) and the Luby-Rackoff theorem (Boneh-Shoup Section 4.4, Luby-Rackoff 1988) in `Complexity/Crypto/Protocols/Cipher/LubyRackoff.lean`. Address coordinator review (cslib-community#752): - Rebase onto `origin/main` (`0193eb0b`) and reuse `Game.advantage_le_of_apply_le`, `Game.advantage_bind_le` (cslib-community#802/cslib-community#804), and `Game.coe_succProbability` directly from `Complexity.Crypto.Game` with zero changes to `Game.lean`. - Prove `map_fst_interpret_dedup_pure` in 11 lines directly from `RandomOracle.interpret_eq_memoize`, removing the private `run_interpret_memoize_pure` copy. - Define `idealStrongGame` over a uniform random permutation `PMF.uniformOfFintype (Equiv.Perm (G × G))` evaluated through `feistelStrongOracle`, and prove both the equal-input (`l₀ = l₁`) zero-advantage sanity check (`advantage_feistel3CCAAttack_self = 0`) and the finite positive advantage lower bound `(|Equiv.Perm (G × G)|)⁻¹ ≤ advantage` against `idealStrongGame` for `|G| ≥ 3` (`le_advantage_feistel3CCAAttack_idealStrongGame`, `advantage_feistel3CCAAttack_idealStrongGame_pos`). Rename the two-table benchmark to `independentTableStrongGame` / `advantage_feistel3CCAAttack_independentTable`, and record the remaining quantitative CCA and 4-round bidirectional information-theoretic bounds as open in cslib-community#748. Refs cslib-community#748
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Extract
Game.advantage_le_of_apply_leandGame.advantage_bind_leunchanged from reviewed #752 at31bbf19finto the existing shared Game API, reusingcoe_succProbability. The first bounds real advantage from mutual finite acceptance-probability bounds; the second preserves a uniform bound across a common first-stage distribution, with no finite-type restriction. Original Jetski source/proof and author credit are retained.Framework friction
These are the two general game bounds #752 was asked to split under #733. Clients can compose probability inequalities and nested shared mixtures without repeating the real/ENNReal conversion and summation proofs. #752 must reuse the actual shared-support squash. No Feistel source, security model or quantitative CCA objective is changed.
Validation at
9fd1fdf06a1c9a4ff23ab86df57e3797eddfa340: all six required gates pass; strict S3 matches the unchanged baseline (1903 statements /401 modules). Focused strict clients pass: composition of both APIs, zero advantage for an arbitrary sampler over ℕ, and a counterexample showing why the finite-error premise matters. Catalogue/hygiene pass; no abstract meaning, scope, headline or rendering impact.Prepared with Codex; extracted code by
worker-jetski-5950b838is preserved byte-identically. Independent final review is required; authors do not enqueue or approve this PR.Closes #802. Refs #733, #748, #752.