Commit 84663369 authored by Benoit Viguier's avatar Benoit Viguier
Browse files

clean unused Lemma in High

parent d55757a2
......@@ -61,16 +61,6 @@ Definition p := locked (2^255 - 19).
Fact Hp_gt0 : p > 0.
Proof. by unlock p; rewrite Z.gt_lt_iff; apply/Z.ltb_spec0. Qed.
Fact Z_of_nat_to_nat_p : Z.of_nat (Z.to_nat p) = p.
Proof. have := Hp_gt0 ; unlock p => Hp; apply Z2Nat.id => //. Qed.
(* Faster proof:
unlock p.
rewrite Z.gt_lt_iff Z.lt_0_sub.
apply: (@Z.lt_trans _ (2^5)); first by apply/Z.ltb_spec0.
by apply: Z.pow_lt_mono_r; do [apply/Z.ltb_spec0 | apply/Z.leb_spec0].
*)
Lemma Hp_neq0 : p <> 0.
Proof. move: Hp_gt0=> ?; omega. Qed.
......@@ -128,7 +118,7 @@ Proof. apply: val_inj. apply: modZp. Qed.
Lemma piK (x : Z) : betweenb 0 p x -> repr (pi x) = x.
Proof. by move/betweenbP=> Hx /=; apply: Zmod_small. Qed.
Lemma x_eq_0 : forall x:Z,
(* Lemma x_eq_0 : forall x:Z,
0 <= x < p -> x <> 0 -> x mod p <> 0.
Proof.
move=> x Hx Hx' Hx''.
......@@ -138,18 +128,7 @@ rewrite Z.mod_divide; last by rewrite /p -lock.
move => Hx'.
rewrite -(Zmod_small x p Hx).
by apply Zdivide_mod.
Qed.
Lemma oppZ (x:Z) : betweenb 0 p x -> repr (pi (-x)) = (- (pi x)) mod p.
Proof. move/betweenbP=> Hx /=.
have := Z.eq_dec x 0.
move => [].
+ move => -> //=.
+ move => Hx'.
rewrite Z_mod_nz_opp_full ; last by apply x_eq_0 => //=.
rewrite Z_mod_nz_opp_full ; last by rewrite Zmod_mod; apply x_eq_0 => //=.
rewrite Zmod_mod //.
Qed.
Qed. *)
Module Zmodp_finite.
......@@ -232,20 +211,6 @@ Import Zmodp_zmod.Exports.
Module Refl.
Lemma eqb_Zeqb x y : eqb x y -> Z.eqb x y.
Proof.
move=> H.
rewrite -(reprK x).
rewrite -(reprK y).
apply/Z.eqb_spec.
move: H.
simpl.
rewrite /eqb.
case_eq y => yi Hyi Heqyi.
case_eq x => xi Hxi Heqxi /=.
by move/Z.eqb_spec ->.
Qed.
Lemma eqb_spec (x y: type) : reflect (x = y) (eqb x y).
Proof.
apply Bool.iff_reflect.
......@@ -453,37 +418,7 @@ apply Zmodp_zmod.add_sub.
move => x. rewrite Zmodp_zmod.add_comm Zmodp_zmod.add_left_inv //.
Defined.
Lemma Zmodp_ringTypeR : @ring_theory Zmodp_ringType zero one add mul sub opp eq.
Proof.
apply mk_rt.
apply Zmodp_zmod.add_left_id.
apply Zmodp_zmod.add_comm.
apply Zmodp_zmod.add_assoc.
apply Zmodp_ring.mul_left_id.
apply Zmodp_ring.mul_comm.
apply Zmodp_ring.mul_assoc.
apply Zmodp_ring.mul_left_distr.
apply Zmodp_zmod.add_sub.
move => x. rewrite Zmodp_zmod.add_comm Zmodp_zmod.add_left_inv //.
Defined.
Lemma Zmodp_GRingSort_ringType : @ring_theory (GRing.Zmodule.sort Zmodp_ringType) zero one add mul sub opp eq.
Proof.
apply mk_rt.
apply Zmodp_zmod.add_left_id.
apply Zmodp_zmod.add_comm.
apply Zmodp_zmod.add_assoc.
apply Zmodp_ring.mul_left_id.
apply Zmodp_ring.mul_comm.
apply Zmodp_ring.mul_assoc.
apply Zmodp_ring.mul_left_distr.
apply Zmodp_zmod.add_sub.
move => x. rewrite Zmodp_zmod.add_comm Zmodp_zmod.add_left_inv //.
Defined.
Add Ring Zmodp_ring : Zmodp_ring.
Add Ring Zmodp_ringType : Zmodp_ringTypeR.
Add Ring Zmodp_GRingSort_ringType : Zmodp_GRingSort_ringType.
Lemma eq_inv_2 : forall (x m:Zmodp.type), (m = (Zmodp.pi 28948022309329048855892746252171976963317496166410141009864396001978282409975%Z) * x)%R -> ((Zmodp.pi 2) * m = x)%R.
Proof.
......@@ -522,18 +457,3 @@ Lemma mult_xy_eq_0: forall (x y: Zmodp.type),
Proof. by move => x y/eqP; rewrite mulf_eq0 ; move/orP => []/eqP -> ; [left|right]. Qed.
Close Scope ring_scope.
(* Lemma eq_inv_2' : forall (x m:Zmodp.type), ((Zmodp.pi 2) * m = x)%R -> (m = (Zmodp.pi 28948022309329048855892746252171976963317496166410141009864396001978282409975%Z) * x)%R.
Proof.
move => m x <-.
apply val_inj => /=.
rewrite Z.mul_mod_idemp_l ; last apply Hp_neq0.
rewrite Z.mul_mod_idemp_l ; last apply Hp_neq0.
rewrite Z.mul_mod_idemp_r ; last apply Hp_neq0.
rewrite Z.mul_assoc.
rewrite -Z.mul_mod_idemp_l ; last apply Hp_neq0.
have ->: (28948022309329048855892746252171976963317496166410141009864396001978282409975 * 2) mod p = 1.
rewrite /p -lock //.
rewrite Z.mul_1_l.
symmetry ;
apply modZp.
Qed. *)
\ No newline at end of file
......@@ -287,11 +287,6 @@ Inductive Zinv_spec (x : type) : Type :=
| Zinv_spec_zero : x = zero -> Zinv_spec x
| Zinv_spec_unit : x <> zero -> forall y, (y * x)%R = one -> Zinv_spec x.
Fixpoint pow (n:nat) (x:type) := match n with
| 0%nat => one
| S n => (x * pow n x)%R
end.
Local Lemma pi_2 : Zmodp.pi 2 = 2%:R.
Proof. by apply/eqP ; zmodp_compute. Qed.
Local Lemma pi_3 : Zmodp.pi 3 = 3%:R.
......
......@@ -32,8 +32,6 @@ end.
Lemma pi_2 : Zmodp.pi 2 = 2%:R.
Proof. by apply/eqP ; zmodp_compute. Qed.
Lemma pi_3 : Zmodp.pi 3 = 3%:R.
Proof. by apply/eqP ; zmodp_compute. Qed.
Ltac ringify := repeat match goal with
| [ |- context[Zmodp.pi 2]] => rewrite pi_2
......@@ -93,12 +91,6 @@ rewrite Zmodp2_mul_Zmodp_a0 GRing.mulfV //.
by apply/eqP.
Qed.
Lemma Zmodp2_div_Zmodp_a0 a b : (Zmodp2 a 0) / (Zmodp2 b 0) = Zmodp2 (a/b) 0.
Proof.
by rewrite Zmodp2_inv_Zmodp_a0 Zmodp2_mul_Zmodp_a0.
Qed.
(*
* Operations of the form (a , 0) op (b , 0)
*)
......@@ -186,7 +178,6 @@ Ltac Zmodpify := repeat match goal with
| _ => rewrite Zmodp2_mul_Zmodp_a0
| _ => rewrite Zmodp2_pow_Zmodp_a0
| _ => rewrite Zmodp2_inv_Zmodp_a0
| _ => rewrite Zmodp2_div_Zmodp_a0
| _ => rewrite Zmodp2_mul_Zmodp_0a
| _ => rewrite Zmodp2_mul_Zmodp_ab1
| _ => rewrite Zmodp2_mul_Zmodp_ab2
......
......@@ -58,9 +58,6 @@ Canonical Structure curve25519_Fp2_ecuFieldType :=
Canonical Structure curve25519_Fp2_finECUFieldType :=
Eval hnf in [finECUFieldType of Zmodp2.type].
Definition curve25519_Fp2_ladder n x :=
@opt_montgomery curve25519_Fp2_finECUFieldType curve25519_Fp2_mcuType n 255 x.
Local Notation "p '#x0'" := (point_x0 p) (at level 30).
Lemma oncurve_0_0: oncurve curve25519_Fp2_mcuType (|0%:R ,0%:R|).
......@@ -88,31 +85,6 @@ Proof.
by rewrite mulf_eq0; move /orP => []/eqP ->.
Qed.
Lemma n_inf : forall n p,
p = MC oncurve_inf ->
p *+ n = MC oncurve_inf.
Proof.
move => n p.
have ->: MC (M:=curve25519_Fp2_mcuType) (p:=) oncurve_inf = 0.
by rewrite /0 => /= ; apply mc_eq.
move => ->.
apply mul0rn.
Qed.
Lemma eq_0_0_0_0_inf : forall x y z,
x = MC oncurve_0_0 ->
y = MC oncurve_0_0 ->
z = MC oncurve_inf ->
x + y = z.
Proof. by move => x y z -> -> ->; rewrite /GRing.add /= ; apply mc_eq. Qed.
Lemma eq_0_0_inf_0_0 : forall x y z,
x = MC oncurve_0_0 ->
y = MC oncurve_inf ->
z = MC oncurve_0_0 ->
x + y = z.
Proof. by move => x y z -> -> ->; rewrite /GRing.add /= ; apply mc_eq. Qed.
Lemma p_x0_0_eq_0 : forall (n:nat) (p: mc curve25519_Fp2_mcuType),
p #x0 = 0%:R ->
(p *+ n) #x0 = 0%R.
......@@ -125,19 +97,4 @@ Proof.
all: move/p_x0_0_impl:Hp.
all: move => [] ->.
all: rewrite /GRing.add //=.
Qed.
(*
Theorem curve25519_Fp2_ladder_ok (n : nat) (x : Zmodp.type) :
(n < 2^255)%nat -> x != 0 ->
forall (p : mc curve25519_Fp2_mcuType), p#x0 = Zmodp2.pi (x, Zmodp.zero) -> curve25519_Fp2_ladder n (Zmodp2.pi (x, Zmodp.zero)) = (p *+ n)#x0.
Proof.
move => Hn Hx p Hp.
rewrite /curve25519_Fp2_ladder.
apply opt_montgomery_ok=> //=.
2: by apply/eqP => H ; inversion H ; subst.
Admitted.
*)
(* apply curve25519_residute. *)
(* Qed. *)
Qed.
\ No newline at end of file
......@@ -82,27 +82,6 @@ Proof.
case_eq ((yp == yq) && (yp != 0)) => -> //=.
Qed.
(* Local Lemma on_curve_add_Fp_to_Fp2 : forall (p q: point Zmodp_ringType),
oncurve curve25519_mcuType p ->
oncurve curve25519_mcuType q ->
oncurve curve25519_Fp2_mcuType (curve_Fp_to_Fp2 (MCGroup.add curve25519_mcuType p q)).
Proof.
move=> p q Hp Hq.
pose p' := curve_Fp_to_Fp2 p.
pose q' := curve_Fp_to_Fp2 q.
rewrite -(curve_add_Fp_to_Fp2 p q p' q') => //.
have OCp' : oncurve curve25519_Fp2_mcuType p' by subst p' ; apply on_curve_Fp_to_Fp2.
have OCq' : oncurve curve25519_Fp2_mcuType q' by subst q' ; apply on_curve_Fp_to_Fp2.
by apply MCGroup.addO'.
Qed.
*)
(* Lemma on_curve25519_add_Fp_to_Fp2: forall (p q: mc curve25519_mcuType),
oncurve curve25519_Fp2_mcuType (curve25519_Fp_to_Fp2 (p + q)).
Proof.
by move => [p Hp] [q Hq] => /=; apply on_curve_add_Fp_to_Fp2.
Qed.
*)
Local Lemma curve25519_add_Fp_to_Fp2' : forall (p q: mc curve25519_mcuType) (p' q': mc curve25519_Fp2_mcuType),
p' = curve25519_Fp_to_Fp2 p ->
q' = curve25519_Fp_to_Fp2 q ->
......
......@@ -24,9 +24,6 @@ Import GRing.Theory.
Local Notation "p '#x0'" := (point_x0 p) (at level 30).
Lemma oncurve_inf : oncurve curve25519_Fp2_mcuType (EC_Inf Zmodp2.type).
Proof. done. Defined.
Local Lemma oncurve_00 : (oncurve curve25519_Fp2_mcuType (EC_In 0 0)).
Proof.
simpl; rewrite /a /b ; apply/eqP.
......@@ -75,10 +72,6 @@ Definition Fp_to_Fp2 p := match p with
| Zmodp2.Zmodp2 x y => x
end.
Lemma Fp_to_Fp2_t : forall p:mc twist25519_mcuType, p#x0 = Fp_to_Fp2 ((twist25519_Fp_to_Fp2 p)#x0).
Proof. by case; case. Qed.
Lemma Fp_to_Fp2_c : forall p:mc curve25519_mcuType, p#x0 = Fp_to_Fp2 ((curve25519_Fp_to_Fp2 p)#x0).
Proof. by case; case. Qed.
Lemma Fp_to_Fp2_eq_C: Fp_to_Fp2 = cFp_to_Fp2.
Proof. reflexivity. Qed.
......
......@@ -472,12 +472,6 @@ Module MCGroup.
by apply addO'.
Qed.
Lemma add0o_check : {in (oncurve M), left_id add_check}.
Proof.
move=> p; rewrite /in_mem /= => oncve_p //.
by rewrite /add_check /= oncve_p.
Qed.
Lemma add0o : {in (oncurve M), left_id add}.
Proof. done. Qed.
......
......@@ -283,7 +283,7 @@ Section MontgomerysHomFormulas.
by move/eqP; case.
Qed.
Lemma point_x0_neq0_point_x x z p : p#x0 != 0 ->
(* Lemma point_x0_neq0_point_x x z p : p#x0 != 0 ->
p#x = inf_div x z -> p#x0 = x / z.
Proof.
move=> Hneq0 Hp.
......@@ -294,7 +294,7 @@ Section MontgomerysHomFormulas.
have z_neq0 : z != 0 by apply: inf_div_K_Fin; apply/sym_eq; exact: H.
by have : false by apply: contra_eqT => [_|]; first by exact: z_neq0.
+ by case: p Hneq0 Hp; first by rewrite eq_refl.
Qed.
Qed. *)
Definition hom_ok (x z : K) := (x != 0) || (z != 0).
......
......@@ -154,7 +154,7 @@ Section OptimizedLadder.
- by apply: point_x0_neq0_fin; rewrite p_x_eqx.
Qed.
Lemma neg_x : forall (p : mc M),
(* Lemma neg_x : forall (p : mc M),
p#x0 = (-p)#x0.
Proof.
move=> [[|xp yp] Hp] //=.
......@@ -167,7 +167,7 @@ Section OptimizedLadder.
rewrite GRing.mulNrn.
apply neg_x.
Qed.
*)
Local Ltac ring_simplify_this :=
repeat match goal with
| _ => rewrite expr2
......
......@@ -82,27 +82,6 @@ Proof.
case_eq ((yp == yq) && (yp != 0)) => -> //=.
Qed.
(* Local Lemma on_twist_add_Fp_to_Fp2 : forall (p q: point Zmodp_ringType),
oncurve twist25519_mcuType p ->
oncurve twist25519_mcuType q ->
oncurve curve25519_Fp2_mcuType (twist_Fp_to_Fp2 (MCGroup.add twist25519_mcuType p q)).
Proof.
move=> p q Hp Hq.
pose p' := twist_Fp_to_Fp2 p.
pose q' := twist_Fp_to_Fp2 q.
rewrite -(twist_add_Fp_to_Fp2 p q p' q') => //.
have OCp' : oncurve curve25519_Fp2_mcuType p' by subst p' ; apply on_twist_Fp_to_Fp2.
have OCq' : oncurve curve25519_Fp2_mcuType q' by subst q' ; apply on_twist_Fp_to_Fp2.
by apply MCGroup.addO'.
Qed.
Lemma on_twist25519_add_Fp_to_Fp2: forall (p q: mc twist25519_mcuType),
oncurve curve25519_Fp2_mcuType (twist25519_Fp_to_Fp2 (p + q)).
Proof.
by move => [p Hp] [q Hq] => /=; apply on_twist_add_Fp_to_Fp2.
Qed.
*)
Local Lemma twist25519_add_Fp_to_Fp2_ : forall (p q: mc twist25519_mcuType) (p' q': mc curve25519_Fp2_mcuType),
p' = twist25519_Fp_to_Fp2 p ->
q' = twist25519_Fp_to_Fp2 q ->
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment