diff options
author | Andres Erbsen <andreser@mit.edu> | 2017-07-07 00:18:13 -0400 |
---|---|---|
committer | Andres Erbsen <andreser@mit.edu> | 2017-07-07 00:18:13 -0400 |
commit | bf8572ea461758b8b66155ec6573d8f99c59065e (patch) | |
tree | 8f734b35ae6ae2cb7011df0bdeda20413ca394ee | |
parent | 18cb95257b2707cb3ead6f4f4de7ccb9f4e532e8 (diff) |
enforce use of [F.zero], [F.one]; prove Ed25519 admits
-rw-r--r-- | src/Arithmetic/ModularArithmeticTheorems.v | 4 | ||||
-rw-r--r-- | src/Arithmetic/PrimeFieldTheorems.v | 2 | ||||
-rw-r--r-- | src/Spec/Ed25519.v | 32 | ||||
-rw-r--r-- | src/Spec/ModularArithmetic.v | 4 |
4 files changed, 15 insertions, 27 deletions
diff --git a/src/Arithmetic/ModularArithmeticTheorems.v b/src/Arithmetic/ModularArithmeticTheorems.v index d634cc0ce..666dd54eb 100644 --- a/src/Arithmetic/ModularArithmeticTheorems.v +++ b/src/Arithmetic/ModularArithmeticTheorems.v @@ -15,7 +15,7 @@ Module F. Ltac unwrap_F := intros; repeat match goal with [ x : F _ |- _ ] => destruct x end; - lazy iota beta delta [F.add F.sub F.mul F.opp F.to_Z F.of_Z proj1_sig] in *; + lazy iota beta delta [F.one F.zero F.add F.sub F.mul F.opp F.to_Z F.of_Z proj1_sig] in *; try apply eqsig_eq; pull_Zmod. @@ -63,7 +63,7 @@ Module F. Proof using Type. intros Hrange Hnz. inversion Hnz. rewrite Zmod_small, Zmod_0_l in *; omega. Qed. Lemma to_Z_nonzero (x:F m) : x <> 0 -> F.to_Z x <> 0%Z. - Proof using Type. intros Hnz Hz. rewrite <- Hz, of_Z_to_Z in Hnz; auto. Qed. + Proof using Type. cbv [F.zero]. intros Hnz Hz. rewrite <- Hz, of_Z_to_Z in Hnz; auto. Qed. Lemma to_Z_range (x : F m) : 0 < m -> 0 <= F.to_Z x < m. Proof using Type. intros. rewrite <- mod_to_Z. apply Z.mod_pos_bound. trivial. Qed. diff --git a/src/Arithmetic/PrimeFieldTheorems.v b/src/Arithmetic/PrimeFieldTheorems.v index 2184d20c6..842313b93 100644 --- a/src/Arithmetic/PrimeFieldTheorems.v +++ b/src/Arithmetic/PrimeFieldTheorems.v @@ -33,7 +33,7 @@ Module F. | _ => solve [ solve_proper | apply F.commutative_ring_modulo | apply inv_nonzero - | cbv [not]; pose proof prime_ge_2 q prime_q; + | cbv [F.zero F.one not]; pose proof prime_ge_2 q prime_q; rewrite F.eq_to_Z_iff, !F.to_Z_of_Z, !Zmod_small; omega ] | _ => split end. diff --git a/src/Spec/Ed25519.v b/src/Spec/Ed25519.v index 1e9ef6faa..914692508 100644 --- a/src/Spec/Ed25519.v +++ b/src/Spec/Ed25519.v @@ -32,6 +32,13 @@ Section Ed25519. Context {SHA512: forall n : nat, Word.word n -> Word.word 512}. + Local Instance char_gt_e : + @Ring.char_ge (@F q) eq F.zero F.one F.opp F.add F.sub F.mul + (BinNat.N.succ_pos BinNat.N.two). + Proof. eapply Hierarchy.char_ge_weaken; + [apply (_:Ring.char_ge q)|Decidable.vm_decide]. Qed. + + Definition E : Type := E.point (F:=Fq) (Feq:=Logic.eq) (Fone:=F.one) (Fadd:=F.add) (Fmul:=F.mul) (a:=a) (d:=d). @@ -52,31 +59,12 @@ Section Ed25519. let '(x,y) := E.coordinates P in Fencode (len:=b-1) y ++ bit (sign x). Definition Senc : Fl -> Word.word b := Fencode (len:=b). - Local Instance char_gt_e : (* TODO: prove this in PrimeFieldTheorems *) - @Ring.char_ge (F.F q) (@eq (F.F q)) (F.of_Z q BinNums.Z0) - (F.of_Z q (BinNums.Zpos BinNums.xH)) (@F.opp q) - (@F.add q) (@F.sub q) (@F.mul q) (BinNat.N.succ_pos BinNat.N.two). - Proof. intros p ?. - edestruct (fun p:p = (BinNat.N.succ_pos BinNat.N.zero) \/ p = (BinNat.N.succ_pos BinNat.N.one) => p); subst. - { admit. (* - p : BinNums.positive - H : BinPos.Pos.le p (BinNat.N.succ_pos BinNat.N.one) - ============================ - p = BinNat.N.succ_pos BinNat.N.zero \/ p = BinNat.N.succ_pos BinNat.N.one *) } - { Crypto.Util.Decidable.vm_decide. } - { Crypto.Util.Decidable.vm_decide. } - Admitted. Lemma nonzero_a : a <> 0%F. - Proof using Type. - Crypto.Util.Decidable.vm_decide. Qed. + Proof using Type. Crypto.Util.Decidable.vm_decide. Qed. Lemma square_a : exists sqrt_a : Fq, (sqrt_a * sqrt_a)%F = a. - Proof using Type. - - pose (@PrimeFieldTheorems.F.Decidable_square q _ ltac:(Crypto.Util.Decidable.vm_decide) a); Crypto.Util.Decidable.vm_decide. Qed. + Proof using Type. pose (@PrimeFieldTheorems.F.Decidable_square q _ ltac:(Crypto.Util.Decidable.vm_decide) a); Crypto.Util.Decidable.vm_decide. Qed. Lemma nonsquare_d : forall x : Fq, (x * x)%F <> d. - Proof using Type. - - pose (@PrimeFieldTheorems.F.Decidable_square q _ ltac:(Crypto.Util.Decidable.vm_decide) d); Crypto.Util.Decidable.vm_decide. Qed. + Proof using Type. pose (@PrimeFieldTheorems.F.Decidable_square q _ ltac:(Crypto.Util.Decidable.vm_decide) d); Crypto.Util.Decidable.vm_decide. Qed. Let add := E.add(nonzero_a:=nonzero_a)(square_a:=square_a)(nonsquare_d:=nonsquare_d). Let zero := E.zero(nonzero_a:=nonzero_a)(d:=d). diff --git a/src/Spec/ModularArithmetic.v b/src/Spec/ModularArithmetic.v index cb57b4547..02c4dd742 100644 --- a/src/Spec/ModularArithmetic.v +++ b/src/Spec/ModularArithmetic.v @@ -81,5 +81,5 @@ Infix "*" := F.mul : F_scope. Infix "-" := F.sub : F_scope. Infix "/" := F.div : F_scope. Infix "^" := F.pow : F_scope. -Notation "0" := (F.of_Z _ 0) : F_scope. -Notation "1" := (F.of_Z _ 1) : F_scope. +Notation "0" := F.zero : F_scope. +Notation "1" := F.one : F_scope. |