From e094a3f049444dd4db93b0862b2b9ff847677aa8 Mon Sep 17 00:00:00 2001 From: jadep Date: Thu, 3 Nov 2016 14:23:41 -0400 Subject: Make [freeze] proofs consider machine integer width and hard input bounds separately --- src/Experiments/Ed25519.v | 92 +++++++++++++++++++++++------------------------ 1 file changed, 46 insertions(+), 46 deletions(-) (limited to 'src/Experiments') diff --git a/src/Experiments/Ed25519.v b/src/Experiments/Ed25519.v index aa5c5c5ca..84b8cb113 100644 --- a/src/Experiments/Ed25519.v +++ b/src/Experiments/Ed25519.v @@ -31,14 +31,6 @@ Definition feSign (f : GF25519BoundedCommon.fe25519) : bool := let '(x9, x8, x7, x6, x5, x4, x3, x2, x1, x0) := (x : GF25519.fe25519) in BinInt.Z.testbit x0 0. -Definition freezePre : - @ModularBaseSystemProofs.FreezePreconditions - GF25519.modulus GF25519.params25519 GF25519.int_width. -Proof. - pose proof GF25519.freezePreconditions25519 as A. - inversion A; econstructor; eauto. -Defined. - Definition a : GF25519BoundedCommon.fe25519 := Eval vm_compute in GF25519BoundedCommon.encode a. Definition d : GF25519BoundedCommon.fe25519 := @@ -399,24 +391,34 @@ Proof. f_equal. Qed. -Lemma nth_default_B_compat : forall i, +Lemma nth_default_freeze_input_bound_compat : forall i, + (nth_default 0 PseudoMersenneBaseParams.limb_widths i < + GF25519.freeze_input_bound)%Z. +Proof. + pose proof GF25519.freezePreconditions25519. + intros. + destruct (lt_dec i (length PseudoMersenneBaseParams.limb_widths)). + { apply ModularBaseSystemProofs.B_compat. + rewrite nth_default_eq. + auto using nth_In. } + { rewrite nth_default_out_of_bounds by omega. + cbv; congruence. } +Qed. +(* +Lemma nth_default_int_width_compat : forall i, (nth_default 0 PseudoMersenneBaseParams.limb_widths i < GF25519.int_width)%Z. Proof. - assert (@ModularBaseSystemProofs.FreezePreconditions - GF25519.modulus GF25519.params25519 - GF25519.int_width) by - (let A := fresh "H" in - pose proof GF25519.freezePreconditions25519 as A; - inversion A; econstructor; eauto). - intros. - destruct (lt_dec i (length PseudoMersenneBaseParams.limb_widths)). - { apply ModularBaseSystemProofs.B_compat. - rewrite nth_default_eq. - auto using nth_In. } - { rewrite nth_default_out_of_bounds by omega. - cbv; congruence. } + pose proof GF25519.freezePreconditions25519. + intros. + destruct (lt_dec i (length PseudoMersenneBaseParams.limb_widths)). + { apply ModularBaseSystemProofs.int_width_compat. + rewrite nth_default_eq. + auto using nth_In. } + { rewrite nth_default_out_of_bounds by omega. + cbv; congruence. } Qed. +*) Lemma minrep_freeze : forall x, Pow2Base.bounded @@ -436,12 +438,7 @@ Lemma minrep_freeze : forall x, (ModularBaseSystem.encode x))) = 0%Z. Proof. - assert (@ModularBaseSystemProofs.FreezePreconditions - GF25519.modulus GF25519.params25519 - GF25519.int_width) - by (let A := fresh "H" in - pose proof GF25519.freezePreconditions25519 as A; - inversion A; econstructor; eauto). + pose proof GF25519.freezePreconditions25519. intros. match goal with |- appcontext [ModularBaseSystem.freeze _ ?x] => @@ -455,15 +452,17 @@ Proof. eapply Z.lt_le_trans; [ solve [intuition eauto] | ]. match goal with |- appcontext [if ?a then _ else _] => destruct a end. { apply Z.pow_le_mono_r; try omega. - apply Z.lt_le_incl, nth_default_B_compat. } - { transitivity (2 ^ (Z.pred GF25519.int_width))%Z. + apply Z.lt_le_incl. + apply nth_default_freeze_input_bound_compat. } + { transitivity (2 ^ (Z.pred GF25519.freeze_input_bound))%Z. { apply Z.pow_le_mono; try omega. - apply Z.lt_le_pred. - apply nth_default_B_compat. } + apply Z.lt_le_pred. + apply nth_default_freeze_input_bound_compat. } { rewrite Z.shiftr_div_pow2 by (auto using Pow2BaseProofs.nth_default_limb_widths_nonneg, PseudoMersenneBaseParamProofs.limb_widths_nonneg). - rewrite <- Z.pow_sub_r by (try omega; split; auto using Pow2BaseProofs.nth_default_limb_widths_nonneg, PseudoMersenneBaseParamProofs.limb_widths_nonneg, Z.lt_le_incl, nth_default_B_compat). - replace (2 ^ GF25519.int_width)%Z - with (2 ^ (Z.pred GF25519.int_width + 1))%Z by (f_equal; omega). + rewrite <- Z.pow_sub_r by (try omega; split; auto using Pow2BaseProofs.nth_default_limb_widths_nonneg, PseudoMersenneBaseParamProofs.limb_widths_nonneg, Z.lt_le_incl, nth_default_freeze_input_bound_compat). + replace (2 ^ GF25519.freeze_input_bound)%Z + with (2 ^ (Z.pred GF25519.freeze_input_bound + 1))%Z + by (f_equal; omega). rewrite Z.pow_add_r by (omega || (cbv; congruence)). rewrite <-Zplus_diag_eq_mult_2. match goal with |- (?a <= ?a + ?b - ?c)%Z => @@ -561,7 +560,7 @@ Proof. { cbv [ZNWord]. do 2 apply f_equal. subst w. - pose proof freezePre. + pose proof GF25519.freezePreconditions25519. match goal with |- appcontext [GF25519.freeze ?x ] => let A := fresh "H" in @@ -625,11 +624,11 @@ Lemma initial_bounds : forall x n, nth_default 0 (Tuple.to_list (length PseudoMersenneBaseParams.limb_widths) (GF25519BoundedCommon.proj1_fe25519 x)) n < - 2 ^ GF25519.int_width - + 2 ^ GF25519.freeze_input_bound - (if eq_nat_dec n 0%nat then 0 else - Z.shiftr (2 ^ GF25519.int_width) + Z.shiftr (2 ^ GF25519.freeze_input_bound) (nth_default 0 PseudoMersenneBaseParams.limb_widths (pred n))))%Z. Proof. @@ -673,7 +672,7 @@ Proof. rewrite !Z.bit0_odd. rewrite <-@Pow2BaseProofs.parity_decode with (limb_widths := PseudoMersenneBaseParams.limb_widths) by (auto using PseudoMersenneBaseParamProofs.limb_widths_nonneg, Tuple.length_to_list; cbv; congruence). - pose proof freezePre. + pose proof GF25519.freezePreconditions25519. match goal with H : _ = GF25519.freeze ?u |- _ => let A := fresh "H" in let B := fresh "H" in pose proof (ModularBaseSystemProofs.freeze_rep u x) as A; @@ -702,14 +701,14 @@ Proof. repeat match goal with |- appcontext[GF25519.freeze ?x] => remember (GF25519.freeze x) end. assert (Tuple.fieldwise (n := 10) eq f f0). - { pose proof freezePre. + { pose proof GF25519.freezePreconditions25519. match goal with H1 : _ = GF25519.freeze ?u, H2 : _ = GF25519.freeze ?v |- _ => let A := fresh "H" in let HP := fresh "H" in let HQ := fresh "H" in pose proof (ModularBaseSystemProofs.freeze_canonical - (freeze_pre := freezePre) u v _ _ eq_refl eq_refl); + (freeze_pre := GF25519.freezePreconditions25519) u v _ _ eq_refl eq_refl); match type of A with ?P -> ?Q -> _ => assert P as HP by apply initial_bounds; assert Q as HQ by apply initial_bounds end; @@ -748,7 +747,7 @@ Qed. Lemma Proper_feEnc : Proper (GF25519BoundedCommon.eq ==> eq) feEnc. Proof. - pose proof freezePre. + pose proof GF25519.freezePreconditions25519. repeat intro; cbv [feEnc]. rewrite !GF25519Bounded.pack_correct, !GF25519Bounded.freeze_correct. rewrite !GF25519.freeze_correct, !ModularBaseSystemOpt.freeze_opt_correct @@ -760,7 +759,8 @@ Proof. let HP := fresh "H" in let HQ := fresh "H" in pose proof (ModularBaseSystemProofs.freeze_canonical - (freeze_pre := freezePre) x y (ModularBaseSystem.decode x) + (freeze_pre := GF25519.freezePreconditions25519) + x y (ModularBaseSystem.decode x) (ModularBaseSystem.decode y) eq_refl eq_refl); match type of A with ?P -> ?Q -> _ => assert P as HP by apply initial_bounds; @@ -1258,14 +1258,14 @@ Qed. Lemma bounded_by_encode_freeze : forall x, ModularBaseSystemProofs.bounded_by (ModularBaseSystem.encode x) - (ModularBaseSystemProofs.freeze_input_bounds (B := GF25519.int_width)). + (ModularBaseSystemProofs.freeze_input_bounds (B := GF25519.freeze_input_bound)). Proof. Admitted. Lemma bounded_by_freeze : forall x, ModularBaseSystemProofs.bounded_by (GF25519BoundedCommon.fe25519WToZ x) - (ModularBaseSystemProofs.freeze_input_bounds (B := GF25519.int_width)). + (ModularBaseSystemProofs.freeze_input_bounds (B := GF25519.freeze_input_bound)). Admitted. Lemma sqrt_correct : forall x : ModularArithmetic.F.F q, @@ -1288,7 +1288,7 @@ Proof. rewrite ModularBaseSystemProofs.encode_rep. symmetry. eapply @ModularBaseSystemProofs.sqrt_5mod8_correct; - eauto using freezePre, ModularBaseSystemProofs.encode_rep, bounded_by_freeze, bounded_by_encode_freeze; + eauto using GF25519.freezePreconditions25519, ModularBaseSystemProofs.encode_rep, bounded_by_freeze, bounded_by_encode_freeze; match goal with | |- appcontext[GF25519Bounded.powW ?a ?ch] => let A := fresh "H" in -- cgit v1.2.3