feat(ProgramLogic): program logic overhaul — eRHL, simulateQ rules, and ElGamal all-random proof#116
Open
feat(ProgramLogic): program logic overhaul — eRHL, simulateQ rules, and ElGamal all-random proof#116
Conversation
…ative relational logic, and ElGamal wiring Add the complete program logic overhaul skeleton: - Unary/SimulateQ: wp rules for simulateQ, liftComp, stateful oracle impls - Relational/Quantitative: eRHL (ℝ≥0∞-valued) with pRHL and apRHL as special cases - Relational/SimulateQ: relational simulateQ coupling and identical-until-bad lemma - Notation: GameEquiv, AdvBound, game_wp/game_rel tactic macros - Basic: query coupling rules (identity + bijection/rnd) - RelationalAlgebra: two-sided StateT instance - SampleableType: bijective map + uniform bool guessing lemmas - HoareTriple: wp_ite rule - ElGamal: helper lemma statements for allRandomHalf and DDH step All proofs are either completed or sorry'd for parallel proof-filling. Made-with: Cursor
…l/SimulateQ Fill in proofs for relational coupling rules and simulateQ theorems: - Basic.lean: relTriple_query, relTriple_query_bij (bijection/"rnd" rule), plus relTriple_refl, relTriple_post_mono, relTriple_bind, and evalDist/probOutput equivalence bridges - SimulateQ.lean: relTriple_simulateQ_run (stateful oracle coupling by induction on OracleComp), relTriple_simulateQ_run' (output-only projection), and helper relTriple_map Made-with: Cursor
Unary/SimulateQ: all sorry's resolved — wp_simulateQ_eq, wp_liftComp, wp_simulateQ_run'_eq now fully proven. Relational/SimulateQ: fix "identical until bad" theorem signature — add required monotonicity hypotheses (h_mono₁, h_mono₂) without which the theorem is false. All helper lemmas fully proven; one sorry remains in the final tvDist bound (ENNReal algebra). Made-with: Cursor
Resolve three sorry's in the IND-CPA game-hopping proof: - randomMaskedCipher_dist_indep: left-multiplication bijection argument - IND_CPA_hybridOracle_allRandom_eqDist: relational coupling via evalDist equality - IND_CPA_allRandomHalf: uniform bit guessing reduces to probOutput_decide_eq_uniformBool_half Also add helper lemmas (evalDist_simulateQ_run_eq_of_impl_evalDist_eq, hybridChallengeOracle_allRandom_evalDist_eq) used in the coupling proof. Made-with: Cursor
🤖 AI-Generated PR SummaryFiles Changed:
Overview of Changes: Here is a summary of the key changes:
New 'sorry's: 11 |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 8b32f36d81
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| /-- `game_wp` decomposes unary WP goals by repeatedly applying WP rules. -/ | ||
| macro "game_wp" : tactic => | ||
| `(tactic| ( | ||
| simp only [game_rule] |
There was a problem hiding this comment.
game_rule references in game tactics
game_wp/game_rel both call simp with game_rule, but there is no game_rule lemma anywhere in the repository (a repo-wide rg "\bgame_rule\b" only finds these macro lines). As a result, the macros elaborate but fail when invoked with an unknown-constant error, so the new user-facing game-hopping tactics are not actually usable.
Useful? React with 👍 / 👎.
…d program logic tactics Rename `SigmaAlg` → `SigmaProtocol` with security property definitions (completeness, special soundness, HVZK). Add `game_rule` simp attribute, extend `game_wp`/`game_rel`/`coupling`/`game_hop` tactics, and wire up Schnorr sigma protocol and Fiat-Shamir examples. Made-with: Cursor
…l equivalence Fill the three Part A sorry's in HHS_Elgamal.lean: - hybridChallengeOracle_allRandom_evalDist_eq: the challenge oracle produces equal distributions for b=true vs b=false when realUntil=0, via StateT/liftM unfolding and randomMaskedCipher_dist_indep. - evalDist_monadLift_self: identity lift simplification using simulateQ_id'. - Minor SubSpec.lean comment fix. Made-with: Cursor
…ij, tvDist_simulateQ bound Fill sorry's in three program logic files: - wp_uniformSample via μ_bind_eq_tsum decomposition - relTriple_uniformSample_bij via relWP coupling with bijection - tvDist_simulateQ_le_probEvent_bad via fundamental lemma of game playing Made-with: Cursor
… and OptimalCoupling - Generalize IsQueryBound to arbitrary budget types; recover classical per-index bound as IsPerIndexQueryBound - Prove Schnorr sigma protocol completeness, special soundness, and HVZK - Fill eRelTriple_pure, relTriple'_bind, and backward direction of relTriple'_iff_couplingPost - Add OptimalCoupling.lean with compactness infrastructure for coupling space - Inline trueProbReal, weaken IND_CPA hybrid theorem hypotheses - Remove unused DecidableEq constraints from DDH/HHS definitions Made-with: Cursor
🤖 Gemini PR SummaryComprehensive program logic framework for cryptographic game-hopping proofs, focusing on quantitative relational logic and its application to ElGamal IND-CPA security. Core Program Logic (eRHL & WP)
Mathematical & Supporting Library
ElGamal IND-CPA Proof
Critical: Sorry InventoryCRITICAL: This PR contains several
Note on DiscrepanciesThere are significant discrepancies between the provided PR body and the draft summary derived from the code changes:
Statistics
Lean Declarations ✏️ **Removed:** 4 declaration(s)
✏️ **Added:** 67 declaration(s)
✏️ **Affected:** 15 declaration(s) (line number changed)
✅ **Removed:** 2 `sorry`(s)
❌ **Added:** 8 `sorry`(s)
📄 **Per-File Summaries**
Last updated: 2026-03-06 23:26 UTC. |
…ain) Define IND_CPA_allRealChallengeOracle / IND_CPA_queryImpl_allReal and the lemma chain (allReal_eq_hybrid_on_bounded, hybrid_q_probOutput_eq_allReal, allReal_evalDist_proj_eq_real, hybrid_q_run'_evalDist_eq_real) that proves IND_CPA_HybridGame_q_eq_game: hybrid game at q equals the real IND-CPA game when the adversary MakesAtMostQueries q. Land ElGamal_IND_CPA_le_q_mul_ddh with the locked-in statement using MakesAtMostQueries. Remove unused ddh_decomp_two_games, inline trueProbReal, tighten longFile limit. Four sorry's remain in the allReal simulation lemmas (term-matching issues, not logical gaps). Made-with: Cursor
Match upstream mathlib PR #35826 review feedback: remove [DecidableEq β] from type signatures where it is only needed in the proof, and use `classical` instead. Made-with: Cursor
Complete the final allReal and projection lemmas so the HHS ElGamal IND-CPA proof closes without remaining sorries. Made-with: Cursor
Establish the finite-support projection and coupling reconstruction lemmas so the compactness argument yields an actual maximizing coupling. Made-with: Cursor
Prove the remaining Wave 1 eRHL bridge lemmas so the quantitative relational logic file builds cleanly except for the intended Wave 2 placeholders. Made-with: Cursor
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
1 participant
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.
Summary
Adds the core program-logic infrastructure for game-hopping proofs and applies it to advance the ElGamal IND-CPA security proof.
Program Logic (
VCVio/ProgramLogic/)wp_simulateQ_eq,wp_liftComp,wp_simulateQ_run'_eq) that let unary Hoare-logic proofs pass throughsimulateQboundaries. All proofs complete (no sorry).RelTriple) coupling rules for oracle queries — identity coupling (relTriple_query) and bijection/rnd rule (relTriple_query_bij), plusrelTriple_bind,relTriple_refl, postcondition monotonicity, and bridges toevalDist/probOutput. All proofs complete.simulateQby induction onOracleComp, and the fundamental lemma of game playing (tvDist_simulateQ_le_probEvent_bad) — "identical until bad" with required monotonicity hypotheses. All helper lemmas proven; 1 sorry remains in the finaltvDistbound (ENNReal algebra step).GameEquiv,AdvBound, bridge lemmas fromRelTripleto game equivalence. 1 sorry in a convenience bridge.wp_iterule added.Supporting Library
StateTMAlgRelOrderedinstance (instStateTBoth) for relational reasoning with independent state on each side.probOutput_map_bijective_uniformSample(bijective map preserves uniform distribution) andprobOutput_decide_eq_uniformBool_half(bit-guessing with distribution-independent oracle has probability 1/2).ElGamal IND-CPA (
Examples/HHS_Elgamal.lean)randomMaskedCipher_dist_indep(left-multiplication bijection),IND_CPA_hybridOracle_allRandom_eqDist(relational coupling via evalDist equality), andIND_CPA_allRandomHalf(the all-random hybrid has success probability exactly 1/2).IND_CPA_stepDDH_real_branch_eqandIND_CPA_stepDDH_random_branch_eq— the per-hop DDH reduction correctness lemmas (3 sorry's total in this file).Sorry inventory
Relational/Quantitative.leanRelational/SimulateQ.leanNotation.leanExamples/HHS_Elgamal.leanTest plan
lake buildpasses (all new files compile, sorry's are explicit)Made with Cursor