Repository navigation
refactor(Probability/PMF): share point-hit and bind-comparison lemmas (readability PD) - #4976
Queued
SamuelSchlesinger wants to merge 57 commits into
Queued
SamuelSchlesinger wants to merge 57 commits into
SamuelSchlesinger wants to merge 57 commits into
Conversation
Refs #4678. Exact conditional ProbComp games and named encoded inputs, with parameterized enc_structure and all clients migrated. Authored with Codex assistance for Samuel Schlesinger.
Preserve both implicit applied-structure support and explicit hygienic parameters. Retain both regression sets and manual guidance. All files outside the 18-file PR scope are identical to main.
Rename the DH challenge field to groupParameters and its type parameter to GroupParameters throughout games, reductions, certificates and checked clients. Explain F.Desc and Schnorr parameters (p, q, g) in source and the manual. Preserve challenge encodings, sampling laws and resource contracts. Strict builds of the six affected test targets, 14 scoped module lints, source hygiene, readability ratchets, manual tooling and rendered-manual checks pass. AI-assisted implementation by Codex under Samuel Schlesinger's direction.
State Boneh–Shoup Attack Games 10.4, 10.5 and 10.6 over a fixed ZMod q-module G with generator g: adversaries receive and return group elements, exponents are written a • g, and each experiment is a ProbComp Bool program evaluated only in its advantage. Add the elementary reductions dlToCDH and cdhToDDH. The superseded DDH.realGame/randomGame/advantage stay until DDH-OT migrates (#4678). Co-authored-by: Karn Seth <karn@google.com>
dlAdvantage_le_cdhAdvantage_dlToCDH holds in every group. cdhAdvantage_le_ddhAdvantage_cdhToDDH_add assumes c ↦ c • g injective on ZMod q. Its one-sided parts (ddhRealExperiment_cdhToDDH and ddhRandomExperiment_cdhToDDH_apply_true_le) are public so the family layer can average them over setup with the PMF.bind_apply_* lemmas (#4678).
DDH-OT now uses a • g with [Module (ZMod q) G] throughout, in place of a.val • g with the hypothesis ∀ y, q • y = 0. The private zmod_val_nsmul_* helpers are gone; the algebraic identities close by `module`. ddhOTReduction takes the DDH triple as three group elements. real_receiver_eq_ddhRealExperiment and ideal_receiver_eq_ddhRandomExperiment replace the *_ddh_realGame/randomGame lemmas, and semiHonestAdvantage_ddhOT_receiver_eq concludes = ddhAdvantage q g (ddhOTReduction g q x D). The sender-privacy theorems no longer need hq. The superseded Cslib.Crypto.DDH tuple games are removed, with no wrappers. New CslibFrontierTests/Crypto/DiffieHellmanFinite.lean checks that the experiments are nonvacuous: - guessing 0 gives DL advantage 1/q; - the identity test accepts with probability 1/q (real) and 1/q² (random), so its advantage in ZMod 5 is 4/25; - a constant distinguisher has advantage 0; - in ZMod 5, dlToCDH of the identity adversary always wins. Refs #4678. Co-authored-by: Karn Seth <karn@google.com>
Stage 1b of the typed Diffie–Hellman redesign. Family games now run core's fixed-group experiments in `F.Carrier d` after an arbitrary setup draw, and adversaries receive and return group elements: - `CDHInput`/`DDHInput` records with `words` views; `encCDHInput`/`encDDHInput` are byte-identical to the previous layout (`encCDHInput_apply`, `encDDHInput_apply`). - `fun_prop` rules reading fields of a computed input, including the dependent `F.encode x.groupParameters x.leftPublic`. - `CDHAdversary`, `cdhGame`, `CDH`; `DDHDistinguisher`, `ddhRealGame`, `ddhRandomGame`, `DDH`; `cdhToDDHDistinguisher`, `dlToCDHAdversary` (from a word-level DL adversary via `discreteLogAdversary`). - `CDH.discreteLog`, `DDH.cdh`, `DDH.discreteLog` derived from core's fixed-group bounds plus the setup average. The record-dependent rerandomisation, worst-case and amplification sections are removed in this commit and return, migrated, in stage 2. Clients do not compile until stage 3. AI-assisted (spike worker, Jetski swarm).
…oup masks Add `Probability/PMF/UniformPoint.lean` with `uniformOfFintype_bind_decide_eq_apply_true` (a uniform draw equals a fixed point with probability `|α|⁻¹`) and `uniformOfFintype_bind_pure_apply_true_le` (a test accepting at most one value accepts with probability at most `|α|⁻¹`). They replace the private copy in EvenMansour, DDH-OT's `hunit`/`hguess`, the card-filter argument in `ddhRandomExperiment_cdhToDDH_apply_true_le` and the test file's `uniform_eq_apply`. Make the fixed-group masks public in `DiffieHellman/Finite.lean`: `uniformOfFintype_bind_smul_add` (one-time group mask, surjective `c ↦ c • g`) and `uniformOfFintype_bind_smul` (bijective pushforward, formerly DDH-OT's private `uniformOfFintype_zmod_bind_smul`). `PrimeOrderGroupFamily.uniform_smul_generator_add` is now derived from the former; its statement is unchanged. Refs #4678
…teLog Move the encoding-based `DecidableEq (F.Carrier d)` instance from SchnorrProtocol.lean into DiscreteLog.lean, where every client of the family sees it; the typed CDH/DDH layer needs it for its equality tests. Refs #4678
Typed family-level CDH/DDH games (spike). The duplicate encoding-based DecidableEq (F.Carrier d) instance is dropped; it now lives in DiscreteLog.lean. Refs #4678
The key-exchange reduction now builds an F.DDHDistinguisher that encodes the group elements at the call site. Its certificate is hA.preprocess with the DDHInput field rules (fun_prop). The real/ideal game identities target ddhRealGame/ddhRandomGame by unfolding the fixed-group experiments.
…istinguishers Order.lean's identity test is now a typed F.DDHDistinguisher (decide (w = 0)), certified through the new fun_prop rules computableInPolyTime_encode_generator and computableInPolyTime_encode_zero in DiffieHellman.lean. Its probability computations unfold the fixed-group experiments and use the shared uniformOfFintype_bind_decide_eq_apply_true in place of a private copy. AI-assisted (spike worker, Jetski swarm).
Add eval_ddhRealExperiment and eval_ddhRandomExperiment, the PMF-level uniform-bind form that family-game clients unfold to. Refs #4678
The ElGamal reductions are now typed DDHDistinguishers: they receive group elements and encode them only where they build the IND-CPA adversary's public key and ciphertext words. The IND-CPA games keep their encodings. Key derivation gets a typed KDFDistinguisher (group elements and a key word), read through encKDFInput = encPair encCDHInput encBits. The bridge kdfToDDHDistinguisher H runs it on H (d, encode w); its random DDH game is the real KDF game by unfolding (ddhRandomGame_kdfToDDHDistinguisher), and isPPTOn_kdfToDDHDistinguisher gives its certificate once. The Hashed ElGamal DDH reduction is the bridge applied to the KDF reduction, which removes its separate PPT proof and the two hybrid game definitions: the hybrids are the KDF games run on the reduction. KDF.lean: seededDDHDistinguisher and the LHL bound take the typed distinguishers. Refs #4678
… KEM kemToKDFDistinguisher is a typed KDFDistinguisher and kemToDDHDistinguisher runs it through kdfToDDHDistinguisher, so the random-DDH/real-KDF bridge and the DDH PPT proof come from the shared Hashed ElGamal lemmas. Refs #4678
…hed ElGamal The per-bit and hidden-bit KDF reductions are typed KDFDistinguishers and the DDH reductions run them through kdfToDDHDistinguisher, so each DDH PPT proof and random-DDH bridge comes from the shared lemmas. Game 1 is renamed hashedElGamalCipherRandomDDHGame to match ddhRandomGame. Refs #4678
…esc-level construction The two Naor–Reingold DDH distinguishers repeated one body. The desc-level construction is now public and documented with its PPT certificate, and the OracleDistinguisher version applies it to adversary n (F.encDesc d).
Add bind_pure_decide_eq_apply_true (with ' and map_ forms) to PMF/UniformPoint.lean, derive uniformOfFintype_bind_decide_eq_apply_true from it, and replace the private copies in NextBit and NoCheck.
…nguisher.IsPPT
isPPT_{elGamalMsgToDDH,elGamalToDDH,kdfToDDH,seededDDH}Distinguisher replace
the isPPTOn_ versions and conclude (...).IsPPT; the seeded certificate takes
distinguisher.IsPPT.
…guisher.IsPPT
KeyExchange, Cramer-Shoup and Naor-Reingold DDH reduction certificates now
conclude `(F.reduction ...).IsPPT` instead of restating the IsPPTOn
F.encDDHInput body, and are renamed isPPTOn_ -> isPPT_ (isPPT_dhEavToDDH,
isPPT_cramerShoup{Msg,AD,}ToDDHDistinguisher,
isPPT_naorReingold{Desc,}ToDDHDistinguisher). Tests state the same.
… DH inputs on it enc_structure now accepts a parent's fields in place of toParent, flattening them into the tuple, and a field whose type depends on earlier fields as `f : w using hw`, encoded as the word `w f` in an encBits slot. Existing declarations generate the same statements and proofs. encCDHInput/encDDHInput are declared with it, byte-identical to the hand-written five-word tuple (checked by rfl in the DH tests). This deletes CDHInput.words/DDHInput.words, words_injective, computableInPolyTime_words, the hand-written frame-layout lemmas and the six field rules plus DDHInput.computableInPolyTime_mk; DDHInput.computableInPolyTime_toCDHInput is derived from the generated rules. NaorReingold length bounds use the generated encDDHInput_apply. Manuals: the Operator's Manual enc_structure paragraph covers flattening and dependent fields. Agent Operator's Manual: no edit needed (no agent workflow changes).
…_structure encKDFInput is now the flat layout of main's KDF reading (unary n, desc, u, v, key), pinned by rfl next to new CDH and DDH layout pins. KDFDistinguisher.IsPPT reads named fields, and KDFDistinguisher.IsPPT.comp mirrors DDHDistinguisher.IsPPT.comp; isPPT_kdfToDDHDistinguisher becomes one application of it. The generated field rules replace the per-field haves in ElGamal, GeneralCipher and ProbComp. Addresses dhrev-1 B2 and dhrev-2 nit 4.
…mes; record typed CDH (#4783) - ddh_iff_encoded: F.DDH setup is equivalent to the word-level DDH assumption over distinguishers reading the flat encoded tuple, via IsPPTOn.exists_extension (dhrev-1 B1, DDH half). - Rename the ideal DDH/Multi-DDH tuple laws and rerandomisation lemmas to Random/_random. - Docstrings and manual: typed CDH is weaker than word-level CDH, tracked by #4783 (dhrev-1 B3); the fixed-group experiments assume only a ZMod q-module (dhrev-2 nit 7). - Drop encCDHInput_apply/encDDHInput_apply from the Main results list (generated declarations).
Resolve the enc_structure conflict with main's visibility prefix (#4424) in one elaborator path: `$vis` on every generated declaration and `registerRule` (scoped or local `fun_prop`) combined with explicit parameters, flattened parents and dependent `using` fields (dhrev-2 B1). Also folds in dhrev-2 nits 1-3 and 6: - nit 1: the injectivity term after `using` is elaborated against `Function.Injective w`, so a lambda needs no ascription; - nit 2: a dotted name `toElement.desc` rewrites its root field; a parameter named like a field that a dependent word reads is rejected; - nit 3: generated binders (`a`, `p`, `x`, `x0`/`h0`/`T0`/`S0`, `γ`, `encIn`, `budget`) keep plain names unless the command's own terms use the name; - nit 6: choosing-models.md paragraphs reordered and one line each. Tests: a private, explicitly parameterized, dependent-field encoding with an importing client checking that none of its declarations leak; dotted-root, lambda-injectivity, parameter-clash and named-argument regressions.
Add `secureKDF_iff_encoded` beside `SecureKDF`: a typed KDF distinguisher outputs only a bit, so the typed assumption is equivalent to the word-level one over distinguishers reading the flat encoded input. Both it and `ddh_iff_encoded` now use the new `IsPPTOn.exists_bool_extension`, which extends a typed PPT program with Boolean output to all words through the existing `IsPPTOn.exists_extension`. Review nits (dhrev-1, dhrev-2): - drop the redundant `[DecidableEq (F.Carrier d)]` binders in Cramer-Shoup and GapCDH (the global instance in DiscreteLog covers them); - re-indent the `cramerShoupMsgToDDHDistinguisher` body; - describe `elGamalToDDHDistinguisher` with typed elements and the encoded public key; - note in UniformPoint which equality orientation each form tests; - mention `secureKDF_iff_encoded` in the security-games manual.
…process Replace the hand-unpacked IsPPTOn witnesses in ddh_iff_encoded and secureKDF_iff_encoded with IsPPTOn.preprocess, so the crypto layer no longer depends on the machine model (dhrev-1 review of #4874).
# Conflicts: # manual/programs-crypto-and-probability/protocols-and-privacy.md
Add PMF.toOuterMeasure_uniformOfFintype_le_of_subsingleton (UniformPoint) and the new topic module PMF/BindCompare.lean (bind_apply_add_of_forall, bind_apply_add_eq_on_support, bind_apply_le_add_of_ne, bind_apply_eq_of_good), moved from NextBit, CCA, WeakPRF and FO/NotBot/Challenge. MAC, CTRMode, CRTOW, EvenMansour, FO/NoCheck and DH/Finite use the shared lemmas instead of local re-derivations.
…mp, DEMCCA and the DH test
Collaborator
Author
|
Agent review (Jetski reviewer rev-2, session ef349cc4-931b-4d20-b996-c6b2afd6e998), head 371defd: APPROVE I checked the full diff against main (merge base 72a0132).
Non-blocking, optional:
I'll queue once ci-checks and guide are green and there are 0 open threads. This is agent review, not human approval. |
This was referenced Nov 13, 2026
# Conflicts: # CslibFrontier/Crypto/Computational/Encryption/CCA/Interleaved.lean
Collaborator
Author
|
|
Collaborator
Author
|
Agent review (Jetski reviewer rev-2, session ef349cc4-931b-4d20-b996-c6b2afd6e998), head b1f23c6: APPROVE The main merge resolves its only conflict, the CCA/Interleaved import line, by keeping both This is agent review, not human approval. |
SamuelSchlesinger
added this pull request to the merge queue
Nov 13, 2026
Any commits made after this event will not be merged.
Collaborator
Author
|
Agent review follow-up (Jetski reviewer rev-2, session ef349cc4-931b-4d20-b996-c6b2afd6e998), head b1f23c6, rendered-manual check: Rendered: inspected p. 36 (printed 28) of cslib-frontier-operators-manual.pdf from run 43376310472: OK.
Agent Operator's Manual: no edit needed. The PR adds probability lemmas and Operator's Manual guidance only, with no agent workflow change. This is agent review, not human approval. |
This branch has not been deployed
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.
Change
Part of #4817 (PD wave). Jetski session facts-encoding (helper of facts), branch
readability/facts-pd, withmainmerged after #4874 and #4904.Several crypto proofs re-derived the same two kinds of PMF fact locally: that a uniform sample hits one point, or a set with at most one point, with probability at most
1/|α|, and that two binds compare pointwise when their continuations do. This PR states each fact once and makes those files call the shared lemma.Probability/PMF/UniformPoint.leangainstoOuterMeasure_uniformOfFintype_le_of_subsingleton. CTRMode's privatetoOuterMeasure_eq_val_of_inj(25 lines) and MAC'suniformOfFintype_bitString_beq_true_leare deleted; both now apply the shared lemma, or the existinguniformOfFintype_bind_pure_apply_true_le, to an injective map. CRTOW'sbind_pure_beq_apply, EvenMansour'stoOuterMeasure_uniformOfFintype_singleton_predand NoCheck'sbind_pure_apply_eq_toOuterMeasureare reproved from or replaced by UniformPoint's decide/map lemmas. NoCheck's sum-to-onehaveusestoReal_true_add_toReal_false.Probability/PMF/BindCompare.leancollects four lemmas that were proved privately in single files. Each keeps its statement and a "Moved from" note:bind_apply_add_of_forall(from PRG/NextBit)bind_apply_add_eq_on_support(from Encryption/CCA, where it was public asCslib.Crypto.Encryption.bind_apply_add_eq_of_support; CCA/Interleaved used it too)bind_apply_le_add_of_ne(from WeakPRF)bind_apply_eq_of_good(from FO/NotBot/Challenge)uniformOfFintype_bind_smulis now a one-line instance ofPMF.uniformOfFintype_bind_bijective.unframe_encPair_encBits/dropFrame_encPair_encBitscopies are deleted in favor of refactor(Encodings): share encPair projection lemmas and delete their copies #4904's shared lemmas. One site applies them toencodeElGamalEncrypt …, so it unfolds that pair first. DEMCCA'shneusesunframe_encPair_encBitsinstead of asimpaunfoldingencPair_apply. tests/DiffieHellman'sdropFrame_dropFrame_unframe_encPair_encDescnow reads the nestedencPairlayout ofencDescwithunframe_encPair/dropFrame_encPairinstead of a hand-written frame word.What callers no longer repeat. For example,
CTRMode.toOuterMeasure_exists_ctr_mem_leused to call a private lemma that split on whether the injective counter hitsyand computed{iv | f iv = y}as a singleton or∅. It now passesSet.subsingleton_singleton.preimage hinjto the shared lemma.Placement.
PMF/Bind.leanhas 227 importers, so the bind comparisons get their own small module that only the five clients import.-- upstream: candidate (addition to Cslib/Probability/PMF.lean).Renamed public declaration:
Cslib.Crypto.Encryption.bind_apply_add_eq_of_support→Cslib.Probability.PMF.bind_apply_add_eq_on_support. Every other statement and name in the clients is unchanged.Left as they are. EvenMansour's
toOuterMeasure_any_any_toReal_le, a real-valued conversion with three local callers and no shared duplicate. NoCheck'spi_toOuterMeasure_*collision helpers, which have one client. NaorReingold, GroupHash and the sigmaextractNatrows, which other lanes own.Authors of new files: Samuel Schlesinger, Karn Seth.
Manual impact
PMF/BindCompare.lean.Validation
371defd2, a targetedlake build --wfail --iofailpasses for the 15 changed library modules, all their direct importers, and the client tests (CCA, CCAInterleaved, CTRMode, MAC, EvenMansour, FujisakiOkamoto{,NoCheck,NotBot}, CramerShoup, DiffieHellman, DiffieHellmanFinite, HybridDEMCCA, HybridEncryption, WeakPRFAndPolyMAC, SigmaLWECCANonvacuity, AssumptionNonvacuity, CollisionResistantToOneWay, ProgramCertificateDiagnostics): 50 targets.lake linton the changed modules,lake exe mk_all --check,check_hygiene.py --check-simp,check_changed_files.py --source-only, the encoding readability and projection chain ratchets, and the manual checker all pass.parallel_defs.py --theoremson the five new declarations finds no duplicate statement. Coverage was partial because modules without local build outputs were skipped; CI's notice covers the full library.AI assistance
Written by an AI agent (Jetski, swarm worker
facts-encoding) under the direction of Samuel Schlesinger: it moved the lemmas, migrated the clients, edited the manual and ran the checks. No human has reviewed this PR yet.