diff options
| author |  jadep <jade.philipoom@gmail.com> | 2016-04-29 15:22:57 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2016-04-29 15:23:13 -0400 |
| commit | a82770a13960d214a76265620096d0f266ca00cd (patch) | |
| tree | 23f4adde871484b6eb6a26b96136939311ded33d | |
| parent | cd07805915328fd5ee8d41b6cdd4d0340aa156aa (diff) | |
Proved decode_point_eq in Ed25519 (comparing encodings is equivalent to
comparing points).
| -rw-r--r-- | src/Specific/Ed25519.v | 14 | ||||
| -rw-r--r-- | src/Util/WordUtil.v | 9 |
2 files changed, 21 insertions, 2 deletions
diff --git a/src/Specific/Ed25519.v b/src/Specific/Ed25519.v index d14e8ea30..5107c1468 100644 --- a/src/Specific/Ed25519.v +++ b/src/Specific/Ed25519.v @@ -9,7 +9,7 @@ Require Import Crypto.Encoding.PointEncodingPre. Require Import Crypto.Spec.Encoding Crypto.Spec.ModularWordEncoding Crypto.Spec.PointEncoding. Require Import Crypto.CompleteEdwardsCurve.ExtendedCoordinates. Require Import Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems. -Require Import Crypto.Util.IterAssocOp. +Require Import Crypto.Util.IterAssocOp Crypto.Util.WordUtil. Local Infix "++" := Word.combine. Local Notation " a '[:' i ']' " := (Word.split1 i _ a) (at level 40). @@ -110,7 +110,17 @@ Local Notation "'(' X ',' Y ',' Z ',' T ')'" := (mkExtended X Y Z T). Local Notation "2" := (ZToField 2) : F_scope. Local Existing Instance PointEncoding. -Axiom decode_point_eq : forall (P_ Q_ : word (S (b-1))) (P Q:E.point), dec P_ = Some P -> dec Q_ = Some Q -> weqb P_ Q_ = (P ==? Q)%E. +Lemma decode_point_eq : forall (P_ Q_ : word (S (b-1))) (P Q:E.point), + dec P_ = Some P -> + dec Q_ = Some Q -> + weqb P_ Q_ = (P ==? Q)%E. +Proof. + intros. + replace P_ with (enc P) in * by (auto using encoding_canonical). + replace Q_ with (enc Q) in * by (auto using encoding_canonical). + rewrite E.point_eqb_correct. + edestruct E.point_eq_dec; (apply weqb_true_iff || apply weqb_false_iff); congruence. +Qed. Lemma decode_test_encode_test : forall S_ X, option_rect (fun _ : option E.point => bool) (fun S : E.point => (S ==? X)%E) false (dec S_) = weqb S_ (enc X). diff --git a/src/Util/WordUtil.v b/src/Util/WordUtil.v index d655d046d..6a8831b14 100644 --- a/src/Util/WordUtil.v +++ b/src/Util/WordUtil.v @@ -46,6 +46,15 @@ Proof. rewrite pow2_id; assumption. Qed. +Lemma weqb_false_iff : forall sz (x y : word sz), weqb x y = false <-> x <> y. +Proof. + split; intros. + + intro eq_xy; apply weqb_true_iff in eq_xy; congruence. + + case_eq (weqb x y); intros weqb_xy; auto. + apply weqb_true_iff in weqb_xy. + congruence. +Qed. + Definition wfirstn n {m} (w : Word.word m) {H : n <= m} : Word.word n. refine (Word.split1 n (m - n) (match _ in _ = N return Word.word N with | eq_refl => w |