From b054d896a31ab00683d8d648482e2e45197f9def Mon Sep 17 00:00:00 2001 From: ashandoak Date: Wed, 11 Mar 2026 20:53:23 -0700 Subject: [PATCH 1/3] chore: remove excess space --- VerifiedCommitments/Pedersen.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/VerifiedCommitments/Pedersen.lean b/VerifiedCommitments/Pedersen.lean index 4cacd65..69a0b88 100644 --- a/VerifiedCommitments/Pedersen.lean +++ b/VerifiedCommitments/Pedersen.lean @@ -7,7 +7,6 @@ import Mathlib.Algebra.Field.ZMod import VerifiedCommitments.MapPMFBijection import VerifiedCommitments.cryptolib import Mathlib.Tactic - namespace Pedersen /- ======================================== From aa44ab8bf138f432c025d15916e51649f038d2b5 Mon Sep 17 00:00:00 2001 From: ashandoak Date: Wed, 11 Mar 2026 20:53:37 -0700 Subject: [PATCH 2/3] chore: reduce imports --- VerifiedCommitments/CommitmentScheme.lean | 4 ---- 1 file changed, 4 deletions(-) diff --git a/VerifiedCommitments/CommitmentScheme.lean b/VerifiedCommitments/CommitmentScheme.lean index d918a01..3b51bb8 100644 --- a/VerifiedCommitments/CommitmentScheme.lean +++ b/VerifiedCommitments/CommitmentScheme.lean @@ -1,8 +1,4 @@ -import Mathlib.Probability.ProbabilityMassFunction.Basic -import Mathlib.Probability.ProbabilityMassFunction.Monad -import Mathlib.Probability.ProbabilityMassFunction.Constructions import Mathlib.Probability.Distributions.Uniform -import Mathlib.Data.ZMod.Defs /-- A CommitmentScheme is a structure over four spaces: M: Message space From 893dd8ddb20cb5aaa5276668b7f1a5f355cd1fa0 Mon Sep 17 00:00:00 2001 From: ashandoak Date: Thu, 12 Mar 2026 20:58:52 -0700 Subject: [PATCH 3/3] wip: add oracle tag to adversary names --- VerifiedCommitments/ElgamalCommitments.lean | 14 +++++++------- VerifiedCommitments/Pedersen.lean | 8 ++++---- 2 files changed, 11 insertions(+), 11 deletions(-) diff --git a/VerifiedCommitments/ElgamalCommitments.lean b/VerifiedCommitments/ElgamalCommitments.lean index 3fbf5d4..439b2c8 100644 --- a/VerifiedCommitments/ElgamalCommitments.lean +++ b/VerifiedCommitments/ElgamalCommitments.lean @@ -87,7 +87,7 @@ end DDH HIDING PROPERTY ======================================== -/ -noncomputable def D_from_adversary +noncomputable def DDHOracleDistinguisher (A : TwoStageAdversary G G (G × G)) : G → G → G → PMF (ZMod 2) := fun gx gy gz => do let ((m₀, m₁), state) ← A.stage1 gx @@ -129,8 +129,8 @@ noncomputable def Game2 theorem ComputationalHidingGame_DDH0 (A : TwoStageAdversary G G (G × G)) : Commitment.comp_hiding_game scheme A = - DDH.experiment0 (D_from_adversary A) := by - simp only [Commitment.comp_hiding_game, DDH.experiment0, bind, scheme, setup, commit, D_from_adversary] + DDH.experiment0 (DDHOracleDistinguisher A) := by + simp only [Commitment.comp_hiding_game, DDH.experiment0, bind, scheme, setup, commit, DDHOracleDistinguisher] simp_rw [PMF.bind_bind (PMF.uniformOfFintype (ZMod params.q))] apply bind_skip' intro x @@ -149,8 +149,8 @@ theorem ComputationalHidingGame_DDH0 winning Game1 (i.e. guessing the correct bit) is equal to the probability of D winning the game DDH1. -/ -theorem Game1_DDH1 (A : TwoStageAdversary G G (G × G)) : @Game1 G params A = DDH.experiment1 (D_from_adversary A) := by - simp only [DDH.experiment1, Game1, bind, D_from_adversary] +theorem Game1_DDH1 (A : TwoStageAdversary G G (G × G)) : @Game1 G params A = DDH.experiment1 (DDHOracleDistinguisher A) := by + simp only [DDH.experiment1, Game1, bind, DDHOracleDistinguisher] simp only [PMF.bind_bind, mul_ite] apply bind_skip' intro x @@ -353,7 +353,7 @@ variable (ε : ENNReal) theorem hiding_from_ddh_single_adversary (A : TwoStageAdversary G G (G × G)) - (DDH_assumption : DDH.Assumption (D_from_adversary A) ε) : + (DDH_assumption : DDH.Assumption (DDHOracleDistinguisher A) ε) : Commitment.comp_hiding_game scheme A 1 - 1/2 ≤ ε := by rw [ComputationalHidingGame_DDH0] have h : ((PMF.uniformOfFintype (ZMod 2)) 1) = 1/2 := by @@ -371,7 +371,7 @@ theorem computational_hiding_from_ddh (ε : ENNReal) unfold Commitment.computational_hiding intro hA apply hiding_from_ddh_single_adversary - exact DDH_hard (D_from_adversary hA) + exact DDH_hard (DDHOracleDistinguisher hA) /- ======================================== diff --git a/VerifiedCommitments/Pedersen.lean b/VerifiedCommitments/Pedersen.lean index 69a0b88..511a38b 100644 --- a/VerifiedCommitments/Pedersen.lean +++ b/VerifiedCommitments/Pedersen.lean @@ -123,7 +123,7 @@ noncomputable def DLogExperiment (A h).bind fun x' => pure <| if params.g^x'.val = params.g^(x).val then 1 else 0 -noncomputable def constructDLogAdversary +noncomputable def DLogOracleAdversary (A : G → PMF (BindingGuess (ZMod params.q) G (ZMod params.q))) (h : G) : PMF (ZMod params.q) := PMF.bind (A h) fun guess => @@ -381,8 +381,8 @@ lemma gpow_eq_of_two_valid_openings lemma binding_reduction_to_dlog (A : G → PMF (BindingGuess (ZMod params.q) G (ZMod params.q))) : -- Pedersen adversary Commitment.comp_binding_game (scheme) A 1 ≤ - DLogExperiment (constructDLogAdversary A) 1 := by - unfold Commitment.comp_binding_game DLogExperiment constructDLogAdversary + DLogExperiment (DLogOracleAdversary A) 1 := by + unfold Commitment.comp_binding_game DLogExperiment DLogOracleAdversary simp only [Pedersen.scheme, Pedersen.setup, Pedersen.verify] @@ -496,7 +496,7 @@ theorem computational_binding : ∀ (A : G → PMF (BindingGuess (ZMod params.q) G (ZMod params.q))), Commitment.comp_binding_game (@scheme G params) A 1 ≤ ε := by intro ε A' A - exact le_trans (binding_reduction_to_dlog A) (A' (constructDLogAdversary A)) + exact le_trans (binding_reduction_to_dlog A) (A' (DLogOracleAdversary A)) end Binding