Refactor program logic (Loom + pRHL-like) and prove ElGamal IND-CPA via DDH

[quangvdao]

Summary

Two interlocking workstreams:

1. Program logic refactor — monad-algebra foundation

• Cut over unary Hoare triples (HoareTriple.lean) from the old OracleComp.StateM-specific formulation to a generic ordered-monad-algebra framework adapted from Loom (POPL 2026).
• New StdDoBridge.lean: bridges Lean 4's Std.Do monad notation to the program-logic layer, with examples in StdDoExamples.lean.
• Relational logic (Relational/Basic.lean, Relational/Examples.lean): RelTriple for relational pre/post reasoning over OracleComp, proved via SPMF couplings.
• ToMathlib/Control/Monad/RelationalAlgebra.lean: standalone relational monad-algebra theory (359 lines, new file).
• ToMathlib/Control/Monad/Algebra.lean: expanded ordered-monad-algebra infrastructure (+244 lines).
• ToMathlib/ProbabilityTheory/Coupling.lean: renamed coupling API to RelTriple, cleaned up.
• New EvalDist lemmas in SPMF.lean and Monad/Basic.lean (probOutput_map_injective, probEvent_bind_bind_swap, probEvent_map, probOutput_bind_congr', etc.) — used extensively in the ElGamal proof.
• README: added Loom attribution in Acknowledgments section.

2. ElGamal multi-query IND-CPA security via DDH

Complete rewrite of Examples/HHS_Elgamal.lean (was fully commented-out old-API code → 929 lines of live proof):

1. ElGamal definition over AddTorsor G P (hard homogeneous space) and perfect correctness proof.
2. Hybrid game family: IND_CPA_HybridGame adversary i answers the first i fresh LR queries with real ElGamal, the rest with random masking (uniform group element + uniform point).
3. All-random hybrid = 1/2 (IND_CPA_allRandomHalf): proved via simulateQ_hybrid0_bdistrib_eq — the adversary's view is b-independent when all queries are randomly masked, using RelTriple from the relational logic layer.
4. Per-hop DDH reduction (IND_CPA_stepDDHReduction): DDH adversary that embeds the DDH challenge into the k-th fresh query.
5. DDH decomposition (ddhExp_stepDDHReduction_decomp): decomposes DDH advantage into difference of hybrid success probabilities.
6. Main theorem (IND_CPA_advantage_le_sum_DDH): IND-CPA advantage ≤ Σ per-hop DDH advantages, using telescoping and triangle inequality from AsymmEncAlg.lean.

Remaining sorrys: IND_CPA_stepDDH_hopBound (connecting per-hop DDH decomposition to the hybrid bound — the core identity is proved in ddhExp_stepDDHReduction_decomp but the final wiring needs equating stepDDH_realBranchGame / stepDDH_randBranchGame with the adjacent hybrids).

3. AsymmEncAlg.lean cleanup

• Added generic telescoping/hybrid infrastructure (trueProbReal, signedAdvantageReal, advantage_le_sum_hops) for any AsymmEncAlg.
• Removed one-time-specific definitions that were incorrectly added by a previous AI session.

Test plan

• lake build passes (all files compile; the only sorrys are in IND_CPA_stepDDH_hopBound and the main theorem which depends on it)
• Verify no import cycles introduced (new files respect the module DAG)
• Spot-check IND_CPA_allRandomHalf proof compiles without sorry

Made with Cursor

[github-actions]

🤖 AI-Generated PR Summary

Files Changed:

• Examples/HHS_Elgamal.lean
• README.md
• ToMathlib.lean
• ToMathlib/Control/Monad/Algebra.lean
• ToMathlib/Control/Monad/RelationalAlgebra.lean
• ToMathlib/ProbabilityTheory/Coupling.lean
• VCVio.lean
• VCVio/CryptoFoundations/AsymmEncAlg.lean
• VCVio/EvalDist/Defs/SPMF.lean
• VCVio/EvalDist/Monad/Basic.lean
• VCVio/ProgramLogic/Relational/Basic.lean
• VCVio/ProgramLogic/Relational/Examples.lean
• VCVio/ProgramLogic/Unary/Examples.lean
• VCVio/ProgramLogic/Unary/HoareTriple.lean
• VCVio/ProgramLogic/Unary/StdDoBridge.lean
• VCVio/ProgramLogic/Unary/StdDoExamples.lean

Overview of Changes:
This diff introduces a comprehensive formal proof of multi-query IND-CPA security for ElGamal encryption and builds out a powerful program logic framework to support it.

Here is a summary of the key changes:

• New ElGamal IND-CPA Security Proof: The central change is a complete replacement of a simple ElGamal sketch with a detailed formal proof. The new implementation proves multi-query IND-CPA security for ElGamal over hard homogeneous spaces via a q-step hybrid argument, reducing its security to the Decisional Diffie-Hellman (DDH) assumption.

• Introduction of a Quantitative Program Logic Framework: To enable this complex proof, a new program logic framework inspired by the Loom project was added:

  • A unary logic based on ordered monad algebras (MAlgOrdered) provides a quantitative weakest precondition (wp) calculus for OracleComp.
  • A relational logic (MAlgRelOrdered, RelTriple) is introduced for reasoning about pairs of programs using coupling semantics, a crucial technique for cryptographic proofs.
  • This framework includes lifting instances for standard monad transformers (StateT, OptionT, etc.), making it broadly applicable.

• Generic Infrastructure for Security Proofs: The foundations for asymmetric encryption (AsymmEncAlg) have been enhanced with generic tools for structuring security arguments, such as lemmas for analyzing hybrid games (game-hopping) and lifting simple adversaries to more complex models.

• Integration with Proof Automation: A new bridge connects the program logic to Lean's Std.Do tactic (mvcgen), enabling automated reasoning for almost-sure properties within do blocks in OracleComp.

New 'sorry's: 1

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: da3f8e1d46

ℹ️ 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".

[chatgpt-codex-connector]

Prove per-hop DDH bound instead of using placeholder

The theorem IND_CPA_stepDDH_hopBound is left as sorry, which turns this result into an axiom and makes downstream security claims (including ElGamal_IND_CPA_bound_toReal, which applies this lemma at line 896) non-verified in the formal sense. This is especially problematic for a cryptography proof file because the main IND-CPA bound now depends on an unproven assumption rather than a checked reduction.

Useful? React with 👍 / 👎.