proposition: Theorem PedersenComputionallyBinding : Pr[BindingCommit_G PedersenSetup _ PedersenReveal A] <= Pr[(@DLP_G _ groupOp _ _ _ g order B)].
proof: Proof. unfold BindingCommit_G, PedersenSetup, PedersenReveal, B, DLP_G. inline_first. comp_skip. inline_first. comp_skip. reflexivity. comp_simp. Local Opaque evalDist. case_eq (eqb n n1); intuition; simpl. rewrite evalDist_ret_0. eapply rat0_le_all. intuition. case_eq (eqb g0 (g ^ n * (g ^ x) ^ n0)); intuition. simpl. rewrite eqb_leibniz in H3. case_eq ( eqb g0 (g ^ n1 * (g ^ x) ^ n2)); intuition. rewrite eqb_leibniz in H4. subst. case_eq (eqb x (modNat ((n + modNatAddInverse n1 order) * multInverseModOrder (n2 + modNatAddInverse n0 order)) order)%nat); intuition. exfalso. eapply eqb_false_iff in H3. eapply H3. clear H3. repeat rewrite groupExp_mult in H4. repeat rewrite <- groupExp_plus in H4. apply groupExp_eq in H4. Local Open Scope nat_scope. apply (plus_add_same_r_if (modNatAddInverse n1 order)) in H4. eapply (modNat_eq_compat_gen order) in H4. repeat rewrite <- modNat_plus in H4. rewrite <- (Nat.add_comm (x * n2)) in H4. rewrite <- (Nat.add_assoc _ n1) in H4. rewrite (Nat.add_comm (x * n2)) in H4. symmetry in H4. rewrite modNat_plus in H4. rewrite modNatAddInverse_correct in H4. rewrite Nat.add_0_l in H4. symmetry in H4. rewrite (Nat.add_comm) in H4. rewrite Nat.add_assoc in H4. eapply (plus_add_same_r_if (modNatAddInverse (x * n0) order)) in H4. eapply (modNat_eq_compat_gen order) in H4. rewrite <- modNat_plus in H4. rewrite <- Nat.add_assoc in H4. rewrite Nat.add_comm in H4. rewrite modNat_plus in H4. rewrite modNatAddInverse_correct in H4. rewrite Nat.add_0_l in H4. rewrite <- modNat_plus in H4. symmetry in H4. rewrite (Nat.add_comm (x * n2)) in H4. rewrite modNat_plus in H4. rewrite modNatAddInverse_mult in H4. rewrite <- modNat_plus in H4. rewrite <- Nat.mul_add_distr_l in H4. apply (modNat_mult_same_r _ _ (multInverseModOrder (n2 + modNatAddInverse n0 order)))in H4. rewrite <- Nat.mul_assoc in H4. rewrite modNat_mult_eq in H4. rewrite (Nat.add_comm n2) in H4. rewrite multInverseCorrect in H4. rewrite Nat.mul_1_r in H4. rewrite modNat_eq in H4. rewrite H4. clear H4. rewrite (Nat.add_comm (modNatAddInverse n1 order)). rewrite (Nat.add_comm n2). trivial. eapply RndNat_support_lt; intuition. eapply H. rewrite evalDist_ret_0. eapply rat0_le_all. intuition. simpl. rewrite evalDist_ret_0. eapply rat0_le_all. intuition. Qed.
imports: FCF GroupTheory OTP RndNat RndGrpElem