diff options
| -rw-r--r-- | src/Encoding/ModularWordEncodingTheorems.v | 27 | ||||
| -rw-r--r-- | src/Spec/Ed25519.v | 6 | ||||
| -rw-r--r-- | src/Spec/ModularWordEncoding.v | 6 | ||||
| -rw-r--r-- | src/Specific/Ed25519.v | 16 | ||||
| -rw-r--r-- | src/Util/WordUtil.v | 9 |
5 files changed, 37 insertions, 27 deletions
diff --git a/src/Encoding/ModularWordEncodingTheorems.v b/src/Encoding/ModularWordEncodingTheorems.v index a74ccb522..7251ac1e6 100644 --- a/src/Encoding/ModularWordEncodingTheorems.v +++ b/src/Encoding/ModularWordEncodingTheorems.v @@ -13,42 +13,29 @@ Local Open Scope F_scope. Section SignBit. Context {m : Z} {prime_m : prime m} {two_lt_m : (2 < m)%Z} {sz : nat} {bound_check : (Z.to_nat m < 2 ^ sz)%nat}. - Lemma m_pos : (0 < m)%Z. - Proof. - apply prime_ge_2 in prime_m; omega. - Qed. - - Arguments modular_word_encoding {m} {sz} m_pos bound_check. - Let Fm_encoding := modular_word_encoding m_pos bound_check. - - Definition sign_bit (x : F m) := - match (@enc _ _ Fm_encoding x) with - | Word.WO => false - | Word.WS b _ w' => b - end. - Lemma sign_bit_parity : forall x, sign_bit x = Z.odd x. + Lemma sign_bit_parity : forall x, @sign_bit m sz x = Z.odd x. Proof. - unfold sign_bit; intros. - unfold Fm_encoding, enc, modular_word_encoding, Fm_enc. + unfold sign_bit, Fm_enc; intros. pose proof (shatter_word (NToWord sz (Z.to_N x))) as shatter. case_eq sz; intros; subst; rewrite shatter. + pose proof (prime_ge_2 m prime_m). simpl in bound_check. assert (m < 1)%Z by (apply Z2Nat.inj_lt; try omega; assumption). omega. - + pose proof (FieldToZ_range x m_pos). + + assert (0 < m)%Z as m_pos by (pose proof prime_ge_2 m prime_m; omega). + pose proof (FieldToZ_range x m_pos). destruct (FieldToZ x); auto. - destruct p; auto. - pose proof (Pos2Z.neg_is_neg p); omega. Qed. - Lemma sign_bit_zero : sign_bit 0 = false. + Lemma sign_bit_zero : @sign_bit m sz 0 = false. Proof. rewrite sign_bit_parity; auto. Qed. - Lemma sign_bit_opp : forall (x : F m), x <> 0 -> negb (sign_bit x) = sign_bit (opp x). + Lemma sign_bit_opp : forall (x : F m), x <> 0 -> negb (@sign_bit m sz x) = @sign_bit m sz (opp x). Proof. intros. pose proof sign_bit_zero as sign_zero. @@ -56,7 +43,7 @@ Section SignBit. pose proof (F_opp_spec x) as opp_spec_x. apply F_eq in opp_spec_x. rewrite FieldToZ_add in opp_spec_x. - rewrite <-opp_spec_x, Z_odd_mod in sign_zero by omega. + rewrite <-opp_spec_x, Z_odd_mod in sign_zero by (pose proof prime_ge_2 m prime_m; omega). replace (Z.odd m) with true in sign_zero by (destruct (ZUtil.prime_odd_or_2 m prime_m); auto || omega). rewrite Z.odd_add, F_FieldToZ_add_opp, Z.div_same, Bool.xorb_true_r in sign_zero by assumption || omega. apply Bool.xorb_eq. diff --git a/src/Spec/Ed25519.v b/src/Spec/Ed25519.v index 9ae03dcd5..cddd72aaf 100644 --- a/src/Spec/Ed25519.v +++ b/src/Spec/Ed25519.v @@ -143,11 +143,9 @@ Proof. reflexivity. Qed. -Lemma b_minus1_nonzero : 0 < b - 1. Proof. cbv. omega. Qed. - Definition PointEncoding : encoding of E.point as (word b) := - (@point_encoding curve25519params (b - 1) q_5mod8 sqrt_minus1_valid FqEncoding - (@sign_bit _ prime_q two_lt_q (b - 1) b_valid) sign_bit_zero sign_bit_opp). + (@point_encoding curve25519params (b - 1) q_5mod8 sqrt_minus1_valid FqEncoding sign_bit + (@sign_bit_zero _ prime_q two_lt_q _ b_valid) (@sign_bit_opp _ prime_q two_lt_q _ b_valid)). Definition H : forall n : nat, word n -> word (b + b). Admitted. Definition B : E.point. Admitted. (* TODO: B = decodePoint (y=4/5, x="positive") *) diff --git a/src/Spec/ModularWordEncoding.v b/src/Spec/ModularWordEncoding.v index 262b1054d..7772a124c 100644 --- a/src/Spec/ModularWordEncoding.v +++ b/src/Spec/ModularWordEncoding.v @@ -22,6 +22,12 @@ Section ModularWordEncoding. else None . + Definition sign_bit (x : F m) := + match (Fm_enc x) with + | Word.WO => false + | Word.WS b _ w' => b + end. + Instance modular_word_encoding : encoding of F m as word sz := { enc := Fm_enc; dec := Fm_dec; diff --git a/src/Specific/Ed25519.v b/src/Specific/Ed25519.v index d14e8ea30..fa1c44d08 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). @@ -349,7 +359,7 @@ Proof. reflexivity. } Unfocus. - cbv iota beta delta [point_dec_coordinates ModularWordEncodingTheorems.sign_bit dec FqEncoding modular_word_encoding E.solve_for_x2 sqrt_mod_q]. + cbv iota beta delta [point_dec_coordinates sign_bit dec FqEncoding modular_word_encoding E.solve_for_x2 sqrt_mod_q]. etransitivity. Focus 2. { 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 |