diff options
| -rw-r--r-- | _CoqProject | 3 | ||||
| -rw-r--r-- | src/Encoding/ModularWordEncodingPre.v | 53 | ||||
| -rw-r--r-- | src/Encoding/PointEncodingPre.v | 352 | ||||
| -rw-r--r-- | src/Encoding/PointEncodingTheorems.v | 189 | ||||
| -rw-r--r-- | src/Spec/Ed25519.v | 6 | ||||
| -rw-r--r-- | src/Spec/Encoding.v | 56 | ||||
| -rw-r--r-- | src/Spec/ModularWordEncoding.v | 31 | ||||
| -rw-r--r-- | src/Spec/PointEncoding.v | 226 | ||||
| -rw-r--r-- | src/Specific/Ed25519.v | 5 |
9 files changed, 671 insertions, 250 deletions
diff --git a/_CoqProject b/_CoqProject index 7d5b37863..b6f056b3e 100644 --- a/_CoqProject +++ b/_CoqProject @@ -7,6 +7,8 @@ src/CompleteEdwardsCurve/DoubleAndAdd.v src/CompleteEdwardsCurve/ExtendedCoordinates.v src/CompleteEdwardsCurve/Pre.v src/Encoding/EncodingTheorems.v +src/Encoding/ModularWordEncodingPre.v +src/Encoding/PointEncodingPre.v src/ModularArithmetic/ExtendedBaseVector.v src/ModularArithmetic/FField.v src/ModularArithmetic/FNsatz.v @@ -25,6 +27,7 @@ src/Spec/Ed25519.v src/Spec/EdDSA.v src/Spec/Encoding.v src/Spec/ModularArithmetic.v +src/Spec/ModularWordEncoding.v src/Spec/PointEncoding.v src/Specific/Ed25519.v src/Specific/GF25519.v diff --git a/src/Encoding/ModularWordEncodingPre.v b/src/Encoding/ModularWordEncodingPre.v new file mode 100644 index 000000000..272748103 --- /dev/null +++ b/src/Encoding/ModularWordEncodingPre.v @@ -0,0 +1,53 @@ +Require Import Coq.ZArith.ZArith. +Require Import Coq.Numbers.Natural.Peano.NPeano. +Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. +Require Import Bedrock.Word. +Require Import Crypto.Tactics.VerdiTactics. +Require Import Crypto.Util.NatUtil. +Require Import Crypto.Util.WordUtil. +Require Import Crypto.Spec.Encoding. + +Local Open Scope nat_scope. + +Section ModularWordEncodingPre. + Context {m : Z} {sz : nat} {m_pos : (0 < m)%Z} {bound_check : Z.to_nat m < 2 ^ sz}. + + Let Fm_enc (x : F m) : word sz := NToWord sz (Z.to_N (FieldToZ x)). + + Let Fm_dec (x_ : word sz) : option (F m) := + let z := Z.of_N (wordToN (x_)) in + if Z_lt_dec z m + then Some (ZToField z) + else None + . + + (* TODO : move to ZUtil *) + Lemma bound_check_N : forall x : F m, (Z.to_N x < Npow2 sz)%N. + Proof. + intro. + pose proof (FieldToZ_range x m_pos) as x_range. + rewrite <- Nnat.N2Nat.id. + rewrite Npow2_nat. + replace (Z.to_N x) with (N.of_nat (Z.to_nat x)) by apply Z_nat_N. + apply (Nat2N_inj_lt _ (pow2 sz)). + rewrite Zpow_pow2. + destruct x_range as [x_low x_high]. + apply Z2Nat.inj_lt in x_high; try omega. + rewrite <- ZUtil.pow_Z2N_Zpow by omega. + replace (Z.to_nat 2) with 2%nat by auto. + omega. + Qed. + + Lemma Fm_encoding_valid : forall x, Fm_dec (Fm_enc x) = Some x. + Proof. + unfold Fm_dec, Fm_enc; intros. + pose proof (FieldToZ_range x m_pos). + rewrite wordToN_nat, NToWord_nat. + rewrite wordToNat_natToWord_idempotent by + (rewrite Nnat.N2Nat.id; apply bound_check_N). + rewrite Nnat.N2Nat.id, Z2N.id by omega. + rewrite ZToField_idempotent. + break_if; auto; omega. + Qed. + +End ModularWordEncodingPre. diff --git a/src/Encoding/PointEncodingPre.v b/src/Encoding/PointEncodingPre.v new file mode 100644 index 000000000..9eb5118bd --- /dev/null +++ b/src/Encoding/PointEncodingPre.v @@ -0,0 +1,352 @@ +Require Import Coq.ZArith.ZArith Coq.ZArith.Znumtheory. +Require Import Coq.Numbers.Natural.Peano.NPeano. +Require Import Coq.Program.Equality. +Require Import Crypto.Encoding.EncodingTheorems. +Require Import Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems. +Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. +Require Import Bedrock.Word. +Require Import Crypto.Tactics.VerdiTactics. + +Require Import Crypto.Spec.Encoding Crypto.Spec.ModularArithmetic. + +Local Open Scope F_scope. + +Section PointEncoding. + Context {prm: TwistedEdwardsParams} {sz : nat} {sz_nonzero : (0 < sz)%nat} + {FqEncoding : encoding of F q as word sz} {q_5mod8 : (q mod 8 = 5)%Z} + {sqrt_minus1_valid : (@ZToField q 2 ^ Z.to_N (q / 4)) ^ 2 = opp 1}. + Existing Instance prime_q. + + Add Field Ffield : (@Ffield_theory q _) + (morphism (@Fring_morph q), + preprocess [Fpreprocess], + postprocess [Fpostprocess; try exact Fq_1_neq_0; try assumption], + constants [Fconstant], + div (@Fmorph_div_theory q), + power_tac (@Fpower_theory q) [Fexp_tac]). + + Definition sqrt_valid (a : F q) := ((sqrt_mod_q a) ^ 2 = a)%F. + + Lemma solve_sqrt_valid : forall p, onCurve p -> + sqrt_valid (solve_for_x2 (snd p)). + Proof. + intros ? onCurve_xy. + destruct p as [x y]; simpl. + rewrite (solve_correct x y) in onCurve_xy. + rewrite <- onCurve_xy. + unfold sqrt_valid. + eapply sqrt_mod_q_valid; eauto. + unfold isSquare; eauto. + Grab Existential Variables. eauto. + Qed. + + Lemma solve_onCurve: forall (y : F q), sqrt_valid (solve_for_x2 y) -> + onCurve (sqrt_mod_q (solve_for_x2 y), y). + Proof. + intros. + unfold sqrt_valid in *. + apply solve_correct; auto. + Qed. + + Lemma solve_opp_onCurve: forall (y : F q), sqrt_valid (solve_for_x2 y) -> + onCurve (opp (sqrt_mod_q (solve_for_x2 y)), y). + Proof. + intros y sqrt_valid_x2. + unfold sqrt_valid in *. + apply solve_correct. + rewrite <- sqrt_valid_x2 at 2. + ring. + Qed. + + Let sign_bit (x : F CompleteEdwardsCurve.q) := + match (enc x) with + | Word.WO => false + | Word.WS b _ w' => b + end. + + Definition point_enc_coordinates (p : (F q * F q)) : Word.word (S sz) := let '(x,y) := p in + Word.WS (sign_bit x) (enc y). + + Let point_enc (p : CompleteEdwardsCurve.point) : Word.word (S sz) := let '(x,y) := proj1_sig p in + Word.WS (sign_bit x) (enc y). + + Definition point_dec_coordinates (sign_bit : F q -> bool) (w : Word.word (S sz)) : option (F q * F q) := + match dec (Word.wtl w) with + | None => None + | Some y => let x2 := solve_for_x2 y in + let x := sqrt_mod_q x2 in + if F_eq_dec (x ^ 2) x2 + then + let p := (if Bool.eqb (whd w) (sign_bit x) then x else opp x, y) in + if (andb (F_eqb x 0) (whd w)) + then None (* special case for 0, since its opposite has the same sign; if the sign bit of 0 is 1, produce None.*) + else Some p + else None + end. + + Ltac inversion_Some_eq := match goal with [H: Some ?x = Some ?y |- _] => inversion H; subst end. + + Lemma point_dec_coordinates_onCurve : forall w p, point_dec_coordinates sign_bit w = Some p -> onCurve p. + Proof. + unfold point_dec_coordinates; intros. + edestruct dec; [ | congruence]. + break_if; [ | congruence]. + break_if; [ congruence | ]. + break_if; inversion_Some_eq; auto using solve_onCurve, solve_opp_onCurve. + Qed. +(* + Definition point_dec (w : word (S sz)) : option point. + case_eq (point_dec_coordinates w); intros; [ | apply None]. + apply Some. + eapply mkPoint. + eapply point_dec_coordinates_onCurve; eauto. + Defined. +*) + Lemma option_eq_dec : forall {A} (x y : option A), {x = y} + {x <> y}. + Proof. + decide equality. + Admitted. + + + Definition point_dec' w p : option point := + match (option_eq_dec (point_dec_coordinates sign_bit w) (Some p)) with + | left EQ => Some (mkPoint p (point_dec_coordinates_onCurve w p EQ)) + | right _ => None (* this case is never reached *) + end. + + Definition point_dec (w : word (S sz)) : option point := + match (point_dec_coordinates sign_bit w) with + | Some p => point_dec' w p + | None => None + end. + + Lemma enc_first_bit_opp : forall (x : F q), x <> 0 -> + match enc x with + | WO => True + | WS b n w => match enc (opp x) with + | WO => False + | WS b' _ _ => b' = negb b + end + end. + Proof. + Admitted. + + Lemma first_bit_zero : match enc 0 with + | WO => False + | WS b _ _ => b = false + end. + Admitted. + + Lemma sign_bit_opp_negb : forall x, x <> 0 -> negb (sign_bit x) = sign_bit (opp x). + Proof. + intros x x_nonzero. + unfold sign_bit. + pose proof (enc_first_bit_opp x x_nonzero). + pose proof (shatter_word (enc x)) as shatter_enc_x. + pose proof (shatter_word (enc (opp x))) as shatter_enc_opp. + destruct sz; try omega. + rewrite shatter_enc_x, shatter_enc_opp in *. + auto. + Qed. + + Lemma Fq_encoding_canonical : forall w (n : F q), dec w = Some n -> enc n = w. + Admitted. + + (* TODO : move *) + Lemma sqrt_mod_q_0 : forall x : F q, sqrt_mod_q x = 0 -> x = 0. + Proof. + unfold sqrt_mod_q; intros. + break_if. + - match goal with [ H : ?sqrt_x ^ 2 = x, H' : ?sqrt_x = 0 |- _ ] => rewrite <-H, H' end. + ring. + - match goal with + | [H : sqrt_minus1 * _ = 0 |- _ ]=> + apply Fq_mul_zero_why in H; destruct H as [sqrt_minus1_zero | ? ]; + [ | eapply Fq_root_zero; eauto ] + end. + unfold sqrt_minus1 in sqrt_minus1_zero. + rewrite sqrt_minus1_zero in sqrt_minus1_valid. + exfalso. + pose proof (@F_opp_spec q 1) as opp_spec_1. + rewrite <-sqrt_minus1_valid in opp_spec_1. + assert (((1 + 0 ^ 2) : F q) = (1 : F q)) as ring_subst by ring. + rewrite ring_subst in *. + apply Fq_1_neq_0; assumption. + Qed. + + Lemma sign_bit_zero : sign_bit 0 = false. + Proof. + unfold sign_bit. + pose proof first_bit_zero. + destruct sz; try omega. + pose proof (shatter_word (enc 0)) as shatter_enc0. + simpl in shatter_enc0; rewrite shatter_enc0 in *; assumption. + Qed. + + Lemma point_coordinates_encoding_canonical : forall w p, + point_dec_coordinates sign_bit w = Some p -> point_enc_coordinates p = w. + Proof. + unfold point_dec_coordinates, point_enc_coordinates; intros ? ? coord_dec_Some. + case_eq (dec (wtl w)); [ intros ? dec_Some | intros dec_None; rewrite dec_None in *; congruence ]. + destruct p. + rewrite (shatter_word w). + f_equal; rewrite dec_Some in *; + do 2 (break_if; try congruence); inversion coord_dec_Some; subst. + + destruct (F_eq_dec (sqrt_mod_q (solve_for_x2 f1)) 0%F) as [sqrt_0 | ?]. + - rewrite sqrt_0 in *. + apply sqrt_mod_q_0 in sqrt_0. + rewrite sqrt_0 in *. + break_if; [symmetry; auto using Bool.eqb_prop | ]. + rewrite sign_bit_zero in *. + simpl in Heqb; rewrite Heqb in *. + discriminate. + - break_if. + symmetry; auto using Bool.eqb_prop. + rewrite <- sign_bit_opp_negb by auto. + destruct (whd w); inversion Heqb0; break_if; auto. + + inversion coord_dec_Some; subst. + auto using Fq_encoding_canonical. +Qed. + + Lemma point_encoding_canonical : forall w x, point_dec w = Some x -> point_enc x = w. + Proof. + (* + unfold point_enc; intros. + unfold point_dec in *. + assert (point_dec_coordinates w = Some (proj1_sig x)). { + set (y := point_dec_coordinates w) in *. + revert H. + dependent destruction y. intros. + rewrite H0 in H. + *) + Admitted. + +Lemma point_dec_coordinates_correct w + : option_map (@proj1_sig _ _) (point_dec w) = point_dec_coordinates sign_bit w. +Proof. + unfold point_dec, option_map. + do 2 break_match; try congruence; unfold point_dec' in *; + break_match; try congruence. + inversion_Some_eq. + reflexivity. +Qed. + +Lemma y_decode : forall p, dec (wtl (point_enc_coordinates p)) = Some (snd p). +Proof. + intros. + destruct p as [x y]; simpl. + exact (encoding_valid y). +Qed. + + +Lemma wordToN_enc_neq_opp : forall x, x <> 0 -> (wordToN (enc (opp x)) <> wordToN (enc x))%N. +Proof. + intros x x_nonzero. + intro false_eq. + apply x_nonzero. + apply F_eq_opp_zero; try apply two_lt_q. + apply wordToN_inj in false_eq. + apply encoding_inj in false_eq. + auto. +Qed. + +Lemma sign_bit_opp : forall x y, y <> 0 -> + (sign_bit x <> sign_bit y <-> sign_bit x = sign_bit (opp y)). +Proof. + split; intro sign_mismatch; case_eq (sign_bit x); case_eq (sign_bit y); + try congruence; intros y_sign x_sign; rewrite <- sign_bit_opp_negb in * by auto; + rewrite y_sign, x_sign in *; reflexivity || discriminate. +Qed. + +Lemma sign_bit_squares : forall x y, y <> 0 -> x ^ 2 = y ^ 2 -> + sign_bit x = sign_bit y -> x = y. +Proof. + intros ? ? y_nonzero squares_eq sign_match. + destruct (sqrt_solutions _ _ squares_eq) as [? | eq_opp]; auto. + assert (sign_bit x = sign_bit (opp y)) as sign_mismatch by (f_equal; auto). + apply sign_bit_opp in sign_mismatch; auto. + congruence. +Qed. + +Lemma sign_bit_match : forall x x' y : F q, onCurve (x, y) -> onCurve (x', y) -> + sign_bit x = sign_bit x' -> x = x'. +Proof. + intros ? ? ? onCurve_x onCurve_x' sign_match. + apply solve_correct in onCurve_x. + apply solve_correct in onCurve_x'. + destruct (F_eq_dec x' 0). + + subst. + rewrite Fq_pow_zero in onCurve_x' by congruence. + rewrite <- onCurve_x' in *. + eapply Fq_root_zero; eauto. + + apply sign_bit_squares; auto. + rewrite onCurve_x, onCurve_x'. + reflexivity. +Qed. +(* +Lemma blah : forall x y, (F_eqb (sqrt_mod_q (solve_for_x2 y)) 0 && sign_bit x)%bool = true. +*) + +Lemma point_encoding_coordinates_valid : forall p, onCurve p -> + point_dec_coordinates sign_bit (point_enc_coordinates p) = Some p. +Proof. + intros p onCurve_p. + unfold point_dec_coordinates. + rewrite y_decode. + pose proof (solve_sqrt_valid p onCurve_p) as solve_sqrt_valid_p. + unfold sqrt_valid in *. + destruct p as [x y]. + simpl in *. + destruct (F_eq_dec ((sqrt_mod_q (solve_for_x2 y)) ^ 2) (solve_for_x2 y)); intuition. + break_if; f_equal. + + case_eq (F_eqb (sqrt_mod_q (solve_for_x2 y)) 0); intros eqb_0. +(* + SearchAbout F_eqb. + + [ | simpl in *; congruence]. + + + + rewrite Bool.eqb_true_iff in Heqb. + pose proof (solve_onCurve y solve_sqrt_valid_p). + f_equal. + apply (sign_bit_match _ _ y); auto. + + rewrite Bool.eqb_false_iff in Heqb. + pose proof (solve_opp_onCurve y solve_sqrt_valid_p). + f_equal. + apply sign_bit_opp in Heqb. + apply (sign_bit_match _ _ y); auto. + intro eq_zero. + apply solve_correct in onCurve_p. + rewrite eq_zero in *. + rewrite Fq_pow_zero in solve_sqrt_valid_p by congruence. + rewrite <- solve_sqrt_valid_p in onCurve_p. + apply Fq_root_zero in onCurve_p. + rewrite onCurve_p in Heqb; auto. +*) +Admitted. + +Lemma point_dec'_valid : forall p, + point_dec' (point_enc_coordinates (proj1_sig p)) (proj1_sig p) = Some p. +Proof. + unfold point_dec'; intros. + break_match. + + f_equal. + destruct p. + apply point_eq. + reflexivity. + + rewrite point_encoding_coordinates_valid in n by apply (proj2_sig p). + congruence. +Qed. + +Lemma point_encoding_valid : forall p, point_dec (point_enc p) = Some p. +Proof. + intros. + unfold point_dec. + replace (point_enc p) with (point_enc_coordinates (proj1_sig p)) by reflexivity. + break_match; rewrite point_encoding_coordinates_valid in * by apply (proj2_sig p); try congruence. + inversion_Some_eq. + eapply point_dec'_valid. +Qed. + +End PointEncoding. diff --git a/src/Encoding/PointEncodingTheorems.v b/src/Encoding/PointEncodingTheorems.v new file mode 100644 index 000000000..7bf207c88 --- /dev/null +++ b/src/Encoding/PointEncodingTheorems.v @@ -0,0 +1,189 @@ + +Section PointEncoding. + Context {prm: CompleteEdwardsCurve.TwistedEdwardsParams} {sz : nat} + {FqEncoding : encoding of ModularArithmetic.F (CompleteEdwardsCurve.q) as Word.word sz} + {q_5mod8 : (CompleteEdwardsCurve.q mod 8 = 5)%Z} + {sqrt_minus1_valid : (@ZToField CompleteEdwardsCurve.q 2 ^ BinInt.Z.to_N (CompleteEdwardsCurve.q / 4)) ^ 2 = opp 1}. + Existing Instance CompleteEdwardsCurve.prime_q. + + Add Field Ffield : (@PrimeFieldTheorems.Ffield_theory CompleteEdwardsCurve.q _) + (morphism (@ModularArithmeticTheorems.Fring_morph CompleteEdwardsCurve.q), + preprocess [ModularArithmeticTheorems.Fpreprocess], + postprocess [ModularArithmeticTheorems.Fpostprocess; try exact PrimeFieldTheorems.Fq_1_neq_0; try assumption], + constants [ModularArithmeticTheorems.Fconstant], + div (@ModularArithmeticTheorems.Fmorph_div_theory CompleteEdwardsCurve.q), + power_tac (@ModularArithmeticTheorems.Fpower_theory CompleteEdwardsCurve.q) [ModularArithmeticTheorems.Fexp_tac]). + + Definition sqrt_valid (a : F q) := ((sqrt_mod_q a) ^ 2 = a)%F. + + Lemma solve_sqrt_valid : forall (p : point), + sqrt_valid (solve_for_x2 (snd (proj1_sig p))). + Proof. + intros. + destruct p as [[x y] onCurve_xy]; simpl. + rewrite (solve_correct x y) in onCurve_xy. + rewrite <- onCurve_xy. + unfold sqrt_valid. + eapply sqrt_mod_q_valid; eauto. + unfold isSquare; eauto. + Grab Existential Variables. eauto. + Qed. + + Lemma solve_onCurve: forall (y : F q), sqrt_valid (solve_for_x2 y) -> + onCurve (sqrt_mod_q (solve_for_x2 y), y). + Proof. + intros. + unfold sqrt_valid in *. + apply solve_correct; auto. + Qed. + + Lemma solve_opp_onCurve: forall (y : F q), sqrt_valid (solve_for_x2 y) -> + onCurve (opp (sqrt_mod_q (solve_for_x2 y)), y). + Proof. + intros y sqrt_valid_x2. + unfold sqrt_valid in *. + apply solve_correct. + rewrite <- sqrt_valid_x2 at 2. + ring. + Qed. + +Definition sign_bit (x : F q) := (wordToN (enc (opp x)) <? wordToN (enc x))%N. +Definition point_enc (p : point) : word (S sz) := let '(x,y) := proj1_sig p in + WS (sign_bit x) (enc y). +Definition point_dec_coordinates (w : word (S sz)) : option (F q * F q) := + match dec (wtl w) with + | None => None + | Some y => let x2 := solve_for_x2 y in + let x := sqrt_mod_q x2 in + if F_eq_dec (x ^ 2) x2 + then + let p := (if Bool.eqb (whd w) (sign_bit x) then x else opp x, y) in + Some p + else None + end. + +Definition point_dec (w : word (S sz)) : option point := + match dec (wtl w) with + | None => None + | Some y => let x2 := solve_for_x2 y in + let x := sqrt_mod_q x2 in + match (F_eq_dec (x ^ 2) x2) with + | right _ => None + | left EQ => if Bool.eqb (whd w) (sign_bit x) + then Some (mkPoint (x, y) (solve_onCurve y EQ)) + else Some (mkPoint (opp x, y) (solve_opp_onCurve y EQ)) + end + end. + +Lemma point_dec_coordinates_correct w + : option_map (@proj1_sig _ _) (point_dec w) = point_dec_coordinates w. +Proof. + unfold point_dec, point_dec_coordinates. + edestruct dec; [ | reflexivity ]. + edestruct @F_eq_dec; [ | reflexivity ]. + edestruct @Bool.eqb; reflexivity. +Qed. + +Lemma y_decode : forall p, dec (wtl (point_enc p)) = Some (snd (proj1_sig p)). +Proof. + intros. + destruct p as [[x y] onCurve_p]; simpl. + exact (encoding_valid y). +Qed. + + +Lemma wordToN_enc_neq_opp : forall x, x <> 0 -> (wordToN (enc (opp x)) <> wordToN (enc x))%N. +Proof. + intros x x_nonzero. + intro false_eq. + apply x_nonzero. + apply F_eq_opp_zero; try apply two_lt_q. + apply wordToN_inj in false_eq. + apply encoding_inj in false_eq. + auto. +Qed. + +Lemma sign_bit_opp_negb : forall x, x <> 0 -> negb (sign_bit x) = sign_bit (opp x). +Proof. + intros x x_nonzero. + unfold sign_bit. + rewrite <- N.leb_antisym. + rewrite N.ltb_compare, N.leb_compare. + rewrite F_opp_involutive. + case_eq (wordToN (enc x) ?= wordToN (enc (opp x)))%N; auto. + intro wordToN_enc_eq. + pose proof (wordToN_enc_neq_opp x x_nonzero). + apply N.compare_eq_iff in wordToN_enc_eq. + congruence. +Qed. + +Lemma sign_bit_opp : forall x y, y <> 0 -> + (sign_bit x <> sign_bit y <-> sign_bit x = sign_bit (opp y)). +Proof. + split; intro sign_mismatch; case_eq (sign_bit x); case_eq (sign_bit y); + try congruence; intros y_sign x_sign; rewrite <- sign_bit_opp_negb in * by auto; + rewrite y_sign, x_sign in *; reflexivity || discriminate. +Qed. + +Lemma sign_bit_squares : forall x y, y <> 0 -> x ^ 2 = y ^ 2 -> + sign_bit x = sign_bit y -> x = y. +Proof. + intros ? ? y_nonzero squares_eq sign_match. + destruct (sqrt_solutions _ _ squares_eq) as [? | eq_opp]; auto. + assert (sign_bit x = sign_bit (opp y)) as sign_mismatch by (f_equal; auto). + apply sign_bit_opp in sign_mismatch; auto. + congruence. +Qed. + +Lemma sign_bit_match : forall x x' y : F q, onCurve (x, y) -> onCurve (x', y) -> + sign_bit x = sign_bit x' -> x = x'. +Proof. + intros ? ? ? onCurve_x onCurve_x' sign_match. + apply solve_correct in onCurve_x. + apply solve_correct in onCurve_x'. + destruct (F_eq_dec x' 0). + + subst. + rewrite Fq_pow_zero in onCurve_x' by congruence. + rewrite <- onCurve_x' in *. + eapply Fq_root_zero; eauto. + + apply sign_bit_squares; auto. + rewrite onCurve_x, onCurve_x'. + reflexivity. +Qed. + +Lemma point_encoding_valid : forall p, point_dec (point_enc p) = Some p. +Proof. + intros. + unfold point_dec. + rewrite y_decode. + pose proof solve_sqrt_valid p as solve_sqrt_valid_p. + unfold sqrt_valid in *. + destruct p as [[x y] onCurve_p]. + simpl in *. + destruct (F_eq_dec ((sqrt_mod_q (solve_for_x2 y)) ^ 2) (solve_for_x2 y)); intuition. + break_if; f_equal; apply point_eq. + + rewrite Bool.eqb_true_iff in Heqb. + pose proof (solve_onCurve y solve_sqrt_valid_p). + f_equal. + apply (sign_bit_match _ _ y); auto. + + rewrite Bool.eqb_false_iff in Heqb. + pose proof (solve_opp_onCurve y solve_sqrt_valid_p). + f_equal. + apply sign_bit_opp in Heqb. + apply (sign_bit_match _ _ y); auto. + intro eq_zero. + apply solve_correct in onCurve_p. + rewrite eq_zero in *. + rewrite Fq_pow_zero in solve_sqrt_valid_p by congruence. + rewrite <- solve_sqrt_valid_p in onCurve_p. + apply Fq_root_zero in onCurve_p. + rewrite onCurve_p in Heqb; auto. +Qed. + +Instance point_encoding : encoding of point as (word (S sz)) := { + enc := point_enc; + dec := point_dec; + encoding_valid := point_encoding_valid +}. + +End PointEncoding. diff --git a/src/Spec/Ed25519.v b/src/Spec/Ed25519.v index 6ab47e8e5..30892c006 100644 --- a/src/Spec/Ed25519.v +++ b/src/Spec/Ed25519.v @@ -1,6 +1,6 @@ Require Import Coq.ZArith.ZArith Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.ZArith.Znumtheory. Require Import Coq.Numbers.Natural.Peano.NPeano Coq.NArith.NArith. -Require Import Crypto.Spec.Encoding Crypto.Spec.PointEncoding. +Require Import Crypto.Spec.PointEncoding Crypto.Spec.ModularWordEncoding. Require Import Crypto.Spec.EdDSA. Require Import Crypto.Spec.CompleteEdwardsCurve Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems. Require Import Crypto.ModularArithmetic.PrimeFieldTheorems Crypto.ModularArithmetic.ModularArithmeticTheorems. @@ -114,6 +114,8 @@ Proof. compute; omega. Qed. +Require Import Crypto.Spec.Encoding. + Lemma q_pos : (0 < q)%Z. q_bound. Qed. Definition FqEncoding : encoding of (F q) as word (b-1) := @modular_word_encoding q (b - 1) q_pos b_valid. @@ -140,7 +142,7 @@ Proof. reflexivity. Qed. -Definition PointEncoding := @point_encoding curve25519params (b - 1) FqEncoding q_5mod8 sqrt_minus1_valid. +Definition PointEncoding := @point_encoding curve25519params (b - 1) FqEncoding. Definition H : forall n : nat, word n -> word (b + b). Admitted. Definition B : point. Admitted. (* TODO: B = decodePoint (y=4/5, x="positive") *) diff --git a/src/Spec/Encoding.v b/src/Spec/Encoding.v index 14cf9d9d9..9a2d5e5ed 100644 --- a/src/Spec/Encoding.v +++ b/src/Spec/Encoding.v @@ -1,61 +1,7 @@ -Require Import Coq.ZArith.ZArith Coq.ZArith.Zpower Coq.ZArith.ZArith. -Require Import Coq.Numbers.Natural.Peano.NPeano. -Require Import Crypto.ModularArithmetic.PrimeFieldTheorems Crypto.ModularArithmetic.ModularArithmeticTheorems. -Require Import Bedrock.Word. -Require Import Crypto.Tactics.VerdiTactics. -Require Import Crypto.Util.NatUtil. -Require Import Crypto.Util.WordUtil. - Class Encoding (T B:Type) := { enc : T -> B ; dec : B -> option T ; encoding_valid : forall x, dec (enc x) = Some x }. -Notation "'encoding' 'of' T 'as' B" := (Encoding T B) (at level 50). - -Local Open Scope nat_scope. - -Section ModularWordEncoding. - Context {m : Z} {sz : nat} {m_pos : (0 < m)%Z} {bound_check : Z.to_nat m < 2 ^ sz}. - - Definition Fm_enc (x : F m) : word sz := natToWord sz (Z.to_nat (FieldToZ x)). - - Definition Fm_dec (x_ : word sz) : option (F m) := - let z := Z.of_nat (wordToNat (x_)) in - if Z_lt_dec z m - then Some (ZToField z) - else None - . - - Lemma bound_check_N : forall x : F m, (N.of_nat (Z.to_nat x) < Npow2 sz)%N. - Proof. - intro. - pose proof (FieldToZ_range x m_pos) as x_range. - rewrite <- Nnat.N2Nat.id. - rewrite Npow2_nat. - apply (Nat2N_inj_lt (Z.to_nat x) (pow2 sz)). - rewrite Zpow_pow2. - destruct x_range as [x_low x_high]. - apply Z2Nat.inj_lt in x_high; try omega. - rewrite <- ZUtil.pow_Z2N_Zpow by omega. - replace (Z.to_nat 2) with 2%nat by auto. - omega. - Qed. - - Lemma Fm_encoding_valid : forall x, Fm_dec (Fm_enc x) = Some x. - Proof. - unfold Fm_dec, Fm_enc; intros. - pose proof (FieldToZ_range x m_pos). - rewrite wordToNat_natToWord_idempotent by apply bound_check_N. - rewrite Z2Nat.id by omega. - rewrite ZToField_idempotent. - break_if; auto; omega. - Qed. - - Instance modular_word_encoding : encoding of F m as word sz := { - enc := Fm_enc; - dec := Fm_dec; - encoding_valid := Fm_encoding_valid - }. -End ModularWordEncoding. +Notation "'encoding' 'of' T 'as' B" := (Encoding T B) (at level 50).
\ No newline at end of file diff --git a/src/Spec/ModularWordEncoding.v b/src/Spec/ModularWordEncoding.v new file mode 100644 index 000000000..9f7e3340b --- /dev/null +++ b/src/Spec/ModularWordEncoding.v @@ -0,0 +1,31 @@ +Require Import Coq.ZArith.ZArith. +Require Import Coq.Numbers.Natural.Peano.NPeano. +Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. +Require Import Bedrock.Word. +Require Import Crypto.Tactics.VerdiTactics. +Require Import Crypto.Util.NatUtil. +Require Import Crypto.Util.WordUtil. +Require Import Crypto.Spec.Encoding. +Require Crypto.Encoding.ModularWordEncodingPre. + +Local Open Scope nat_scope. + +Section ModularWordEncoding. + Context {m : Z} {sz : nat} {m_pos : (0 < m)%Z} {bound_check : Z.to_nat m < 2 ^ sz}. + + Definition Fm_enc (x : F m) : word sz := NToWord sz (Z.to_N (FieldToZ x)). + + Definition Fm_dec (x_ : word sz) : option (F m) := + let z := Z.of_N (wordToN (x_)) in + if Z_lt_dec z m + then Some (ZToField z) + else None + . + + Instance modular_word_encoding : encoding of F m as word sz := { + enc := Fm_enc; + dec := Fm_dec; + encoding_valid := @ModularWordEncodingPre.Fm_encoding_valid m sz m_pos bound_check + }. + +End ModularWordEncoding. diff --git a/src/Spec/PointEncoding.v b/src/Spec/PointEncoding.v index 251e50414..38b4b4224 100644 --- a/src/Spec/PointEncoding.v +++ b/src/Spec/PointEncoding.v @@ -1,196 +1,42 @@ -Require Import Coq.ZArith.ZArith Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.ZArith.Znumtheory. -Require Import Coq.Numbers.Natural.Peano.NPeano Coq.NArith.NArith. -Require Import Crypto.Spec.Encoding Crypto.Encoding.EncodingTheorems. -Require Import Crypto.Spec.CompleteEdwardsCurve Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems. -Require Import Crypto.ModularArithmetic.PrimeFieldTheorems Crypto.ModularArithmetic.ModularArithmeticTheorems. -Require Import Crypto.Util.NatUtil Crypto.Util.ZUtil Crypto.Util.NumTheoryUtil. -Require Import Bedrock.Word. -Require Import Crypto.Tactics.VerdiTactics. +Require Coq.ZArith.ZArith Coq.ZArith.Znumtheory. +Require Coq.Numbers.Natural.Peano.NPeano. +Require Crypto.Encoding.EncodingTheorems. +Require Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems. +Require Crypto.ModularArithmetic.PrimeFieldTheorems. +Require Bedrock.Word. +Require Crypto.Tactics.VerdiTactics. +Require Crypto.Encoding.PointEncodingPre. +Obligation Tactic := eauto using PointEncodingPre.point_encoding_canonical. + +Require Import Crypto.Spec.Encoding Crypto.Spec.ModularArithmetic. +Require Import Crypto.Spec.CompleteEdwardsCurve. Local Open Scope F_scope. Section PointEncoding. - Context {prm:TwistedEdwardsParams} {sz : nat} {FqEncoding : encoding of F q as word sz} {q_5mod8 : q mod 8 = 5} {sqrt_minus1_valid : (@ZToField q 2 ^ Z.to_N (q / 4)) ^ 2 = opp 1}. - Existing Instance prime_q. - - Add Field Ffield : (@Ffield_theory q _) - (morphism (@Fring_morph q), - preprocess [Fpreprocess], - postprocess [Fpostprocess; try exact Fq_1_neq_0; try assumption], - constants [Fconstant], - div (@Fmorph_div_theory q), - power_tac (@Fpower_theory q) [Fexp_tac]). - - Definition sqrt_valid (a : F q) := ((sqrt_mod_q a) ^ 2 = a)%F. - - Lemma solve_sqrt_valid : forall (p : point), - sqrt_valid (solve_for_x2 (snd (proj1_sig p))). - Proof. - intros. - destruct p as [[x y] onCurve_xy]; simpl. - rewrite (solve_correct x y) in onCurve_xy. - rewrite <- onCurve_xy. - unfold sqrt_valid. - eapply sqrt_mod_q_valid; eauto. - unfold isSquare; eauto. - Grab Existential Variables. eauto. - Qed. - - Lemma solve_onCurve: forall (y : F q), sqrt_valid (solve_for_x2 y) -> - onCurve (sqrt_mod_q (solve_for_x2 y), y). - Proof. - intros. - unfold sqrt_valid in *. - apply solve_correct; auto. - Qed. - - Lemma solve_opp_onCurve: forall (y : F q), sqrt_valid (solve_for_x2 y) -> - onCurve (opp (sqrt_mod_q (solve_for_x2 y)), y). - Proof. - intros y sqrt_valid_x2. - unfold sqrt_valid in *. - apply solve_correct. - rewrite <- sqrt_valid_x2 at 2. - ring. - Qed. - -Definition sign_bit (x : F q) := (wordToN (enc (opp x)) <? wordToN (enc x))%N. -Definition point_enc (p : point) : word (S sz) := let '(x,y) := proj1_sig p in - WS (sign_bit x) (enc y). -Definition point_dec_coordinates (w : word (S sz)) : option (F q * F q) := - match dec (wtl w) with - | None => None - | Some y => let x2 := solve_for_x2 y in - let x := sqrt_mod_q x2 in - if F_eq_dec (x ^ 2) x2 - then - let p := (if Bool.eqb (whd w) (sign_bit x) then x else opp x, y) in - Some p - else None - end. - -Definition point_dec (w : word (S sz)) : option point := - match dec (wtl w) with - | None => None - | Some y => let x2 := solve_for_x2 y in - let x := sqrt_mod_q x2 in - match (F_eq_dec (x ^ 2) x2) with - | right _ => None - | left EQ => if Bool.eqb (whd w) (sign_bit x) - then Some (mkPoint (x, y) (solve_onCurve y EQ)) - else Some (mkPoint (opp x, y) (solve_opp_onCurve y EQ)) - end - end. - -Lemma point_dec_coordinates_correct w - : option_map (@proj1_sig _ _) (point_dec w) = point_dec_coordinates w. -Proof. - unfold point_dec, point_dec_coordinates. - edestruct dec; [ | reflexivity ]. - edestruct @F_eq_dec; [ | reflexivity ]. - edestruct @Bool.eqb; reflexivity. -Qed. - -Lemma y_decode : forall p, dec (wtl (point_enc p)) = Some (snd (proj1_sig p)). -Proof. - intros. - destruct p as [[x y] onCurve_p]; simpl. - exact (encoding_valid y). -Qed. - - -Lemma wordToN_enc_neq_opp : forall x, x <> 0 -> (wordToN (enc (opp x)) <> wordToN (enc x))%N. -Proof. - intros x x_nonzero. - intro false_eq. - apply x_nonzero. - apply F_eq_opp_zero; try apply two_lt_q. - apply wordToN_inj in false_eq. - apply encoding_inj in false_eq. - auto. -Qed. - -Lemma sign_bit_opp_negb : forall x, x <> 0 -> negb (sign_bit x) = sign_bit (opp x). -Proof. - intros x x_nonzero. - unfold sign_bit. - rewrite <- N.leb_antisym. - rewrite N.ltb_compare, N.leb_compare. - rewrite F_opp_involutive. - case_eq (wordToN (enc x) ?= wordToN (enc (opp x)))%N; auto. - intro wordToN_enc_eq. - pose proof (wordToN_enc_neq_opp x x_nonzero). - apply N.compare_eq_iff in wordToN_enc_eq. - congruence. -Qed. - -Lemma sign_bit_opp : forall x y, y <> 0 -> - (sign_bit x <> sign_bit y <-> sign_bit x = sign_bit (opp y)). -Proof. - split; intro sign_mismatch; case_eq (sign_bit x); case_eq (sign_bit y); - try congruence; intros y_sign x_sign; rewrite <- sign_bit_opp_negb in * by auto; - rewrite y_sign, x_sign in *; reflexivity || discriminate. -Qed. - -Lemma sign_bit_squares : forall x y, y <> 0 -> x ^ 2 = y ^ 2 -> - sign_bit x = sign_bit y -> x = y. -Proof. - intros ? ? y_nonzero squares_eq sign_match. - destruct (sqrt_solutions _ _ squares_eq) as [? | eq_opp]; auto. - assert (sign_bit x = sign_bit (opp y)) as sign_mismatch by (f_equal; auto). - apply sign_bit_opp in sign_mismatch; auto. - congruence. -Qed. - -Lemma sign_bit_match : forall x x' y : F q, onCurve (x, y) -> onCurve (x', y) -> - sign_bit x = sign_bit x' -> x = x'. -Proof. - intros ? ? ? onCurve_x onCurve_x' sign_match. - apply solve_correct in onCurve_x. - apply solve_correct in onCurve_x'. - destruct (F_eq_dec x' 0). - + subst. - rewrite Fq_pow_zero in onCurve_x' by congruence. - rewrite <- onCurve_x' in *. - eapply Fq_root_zero; eauto. - + apply sign_bit_squares; auto. - rewrite onCurve_x, onCurve_x'. - reflexivity. -Qed. - -Lemma point_encoding_valid : forall p, point_dec (point_enc p) = Some p. -Proof. - intros. - unfold point_dec. - rewrite y_decode. - pose proof solve_sqrt_valid p as solve_sqrt_valid_p. - unfold sqrt_valid in *. - destruct p as [[x y] onCurve_p]. - simpl in *. - destruct (F_eq_dec ((sqrt_mod_q (solve_for_x2 y)) ^ 2) (solve_for_x2 y)); intuition. - break_if; f_equal; apply point_eq. - + rewrite Bool.eqb_true_iff in Heqb. - pose proof (solve_onCurve y solve_sqrt_valid_p). - f_equal. - apply (sign_bit_match _ _ y); auto. - + rewrite Bool.eqb_false_iff in Heqb. - pose proof (solve_opp_onCurve y solve_sqrt_valid_p). - f_equal. - apply sign_bit_opp in Heqb. - apply (sign_bit_match _ _ y); auto. - intro eq_zero. - apply solve_correct in onCurve_p. - rewrite eq_zero in *. - rewrite Fq_pow_zero in solve_sqrt_valid_p by congruence. - rewrite <- solve_sqrt_valid_p in onCurve_p. - apply Fq_root_zero in onCurve_p. - rewrite onCurve_p in Heqb; auto. -Qed. - -Instance point_encoding : encoding of point as (word (S sz)) := { - enc := point_enc; - dec := point_dec; - encoding_valid := point_encoding_valid -}. + Context {prm: CompleteEdwardsCurve.TwistedEdwardsParams} {sz : nat} + {FqEncoding : encoding of ModularArithmetic.F (CompleteEdwardsCurve.q) as Word.word sz}. + + Definition sign_bit (x : F CompleteEdwardsCurve.q) := + match (enc x) with + | Word.WO => false + | Word.WS b _ w' => b + end. + + Definition point_enc (p : CompleteEdwardsCurve.point) : Word.word (S sz) := let '(x,y) := proj1_sig p in + Word.WS (sign_bit x) (enc y). + + Program Definition point_dec_with_spec : + {point_dec : Word.word (S sz) -> option CompleteEdwardsCurve.point + | forall w x, point_dec w = Some x -> (point_enc x = w) + } := PointEncodingPre.point_dec. + + Definition point_dec := Eval hnf in (proj1_sig point_dec_with_spec). + + Instance point_encoding : encoding of CompleteEdwardsCurve.point as (Word.word (S sz)) := { + enc := point_enc; + dec := point_dec; + encoding_valid := PointEncodingPre.point_encoding_valid + }. End PointEncoding. diff --git a/src/Specific/Ed25519.v b/src/Specific/Ed25519.v index 2bafd4c8a..8ff80ebb9 100644 --- a/src/Specific/Ed25519.v +++ b/src/Specific/Ed25519.v @@ -5,7 +5,8 @@ Require Import BinNat BinInt NArith Crypto.Spec.ModularArithmetic. Require Import ModularArithmetic.ModularArithmeticTheorems. Require Import ModularArithmetic.PrimeFieldTheorems. Require Import Crypto.Spec.CompleteEdwardsCurve. -Require Import Crypto.Spec.Encoding Crypto.Spec.PointEncoding. +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. @@ -465,8 +466,6 @@ Proof. set_evars. rewrite !FRepOpp_correct. - rewrite <-!enc_rep2F_correct. - rewrite <-wltu_correct. rewrite (if_map rep2F). lazymatch goal with |- ?e = Let_In (rep2F ?x, rep2F ?y) (fun p => @?r p) => |