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/ModularArithmetic/ModularBaseSystem.v | 16 ++++++------- src/ModularArithmetic/ModularBaseSystemOpt.v | 26 +++++--------------- src/ModularArithmetic/ModularBaseSystemProofs.v | 32 +++++++++++++++---------- 3 files changed, 34 insertions(+), 40 deletions(-) (limited to 'src/ModularArithmetic') diff --git a/src/ModularArithmetic/ModularBaseSystem.v b/src/ModularArithmetic/ModularBaseSystem.v index 6df49173e..9d7ce7c1f 100644 --- a/src/ModularArithmetic/ModularBaseSystem.v +++ b/src/ModularArithmetic/ModularBaseSystem.v @@ -83,10 +83,10 @@ Section ModularBaseSystem. Definition eq (x y : digits) : Prop := decode x = decode y. - Definition freeze B (x : digits) : digits := - from_list (freeze B [[x]]) (length_freeze length_to_list). + Definition freeze int_width (x : digits) : digits := + from_list (freeze int_width [[x]]) (length_freeze length_to_list). - Definition eqb B (x y : digits) : bool := fieldwiseb Z.eqb (freeze B x) (freeze B y). + Definition eqb int_width (x y : digits) : bool := fieldwiseb Z.eqb (freeze int_width x) (freeze int_width y). (* Note : both of the following square root definitions will produce garbage output if the input is not square mod [modulus]. The caller should either provably only call them with square input, @@ -95,10 +95,10 @@ Section ModularBaseSystem. (chain_correct : fold_chain 0%N N.add chain (1%N :: nil) = Z.to_N (modulus / 4 + 1)) (x : digits) : digits := pow x chain. - Definition sqrt_5mod8 B powx powx_squared (chain : list (nat * nat)) + Definition sqrt_5mod8 int_width powx powx_squared (chain : list (nat * nat)) (chain_correct : fold_chain 0%N N.add chain (1%N :: nil) = Z.to_N (modulus / 8 + 1)) (sqrt_minus1 x : digits) : digits := - if eqb B powx_squared x then powx else mul sqrt_minus1 powx. + if eqb int_width powx_squared x then powx else mul sqrt_minus1 powx. Import Morphisms. Global Instance eq_Equivalence : Equivalence eq. @@ -106,9 +106,9 @@ Section ModularBaseSystem. split; cbv [eq]; repeat intro; congruence. Qed. - Definition select B (b : Z) (x y : digits) := - add (map (Z.land (neg B b)) x) - (map (Z.land (neg B (Z.lxor b 1))) x). + Definition select int_width (b : Z) (x y : digits) := + add (map (Z.land (neg int_width b)) x) + (map (Z.land (neg int_width (Z.lxor b 1))) x). Context {target_widths} (target_widths_nonneg : forall x, In x target_widths -> 0 <= x) (bits_eq : sum_firstn limb_widths (length limb_widths) = diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v index d302f83a8..155698e56 100644 --- a/src/ModularArithmetic/ModularBaseSystemOpt.v +++ b/src/ModularArithmetic/ModularBaseSystemOpt.v @@ -905,30 +905,15 @@ Section Conversion. End Conversion. -Section with_base. - Context {modulus} (prm : PseudoMersenneBaseParams modulus). - Local Notation base := (Pow2Base.base_from_limb_widths limb_widths). - Local Notation log_cap i := (nth_default 0 limb_widths i). - - Record freezePreconditions int_width := - mkFreezePreconditions { - lt_1_length_base : (1 < length base)%nat; - int_width_pos : 0 < int_width; - int_width_compat : forall w, In w limb_widths -> w < int_width; - c_pos : 0 < c; - c_reduce1 : c * (Z.ones (int_width - log_cap (pred (length base)))) < 2 ^ log_cap 0; - c_reduce2 : c < 2 ^ log_cap 0 - c; - two_pow_k_le_2modulus : 2 ^ k <= 2 * modulus - }. -End with_base. -Local Hint Resolve lt_1_length_base int_width_pos int_width_compat c_pos - c_reduce1 c_reduce2 two_pow_k_le_2modulus. +Local Hint Resolve lt_1_length_limb_widths int_width_pos B_pos B_compat + c_reduce1 c_reduce2. Section Canonicalization. Context `{prm : PseudoMersenneBaseParams} {sc : SubtractionCoefficient} (* allows caller to precompute k and c *) (k_ c_ : Z) (k_subst : k = k_) (c_subst : c = c_) - {int_width} (preconditions : freezePreconditions prm int_width). + {int_width freeze_input_bound} + (preconditions : FreezePreconditions freeze_input_bound int_width). Local Notation digits := (tuple Z (length limb_widths)). Definition carry_full_3_opt_cps_sig @@ -1072,7 +1057,8 @@ Section SquareRoots. Section SquareRoot5mod8. Context {ec : ExponentiationChain (modulus / 8 + 1)}. Context (sqrt_m1 : digits) (sqrt_m1_correct : rep (mul sqrt_m1 sqrt_m1) (F.opp 1%F)). - Context {int_width} (preconditions : freezePreconditions prm int_width). + Context {int_width freeze_input_bound} + (preconditions : FreezePreconditions freeze_input_bound int_width). Definition sqrt_5mod8_opt_sig (powx powx_squared us : digits) : { vs : digits | diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v index 59a6f33db..197a0dca6 100644 --- a/src/ModularArithmetic/ModularBaseSystemProofs.v +++ b/src/ModularArithmetic/ModularBaseSystemProofs.v @@ -521,16 +521,18 @@ End CarryProofs. Hint Rewrite @length_carry_and_reduce @length_carry : distr_length. -Class FreezePreconditions `{prm : PseudoMersenneBaseParams} B := +Class FreezePreconditions `{prm : PseudoMersenneBaseParams} B int_width := { lt_1_length_limb_widths : (1 < length limb_widths)%nat; + int_width_pos : 0 < int_width; + B_le_int_width : B <= int_width; B_pos : 0 < B; B_compat : forall w, In w limb_widths -> w < B; (* on the first reduce step, we add at most one bit of width to the first digit *) c_reduce1 : c * ((2 ^ B) >> nth_default 0 limb_widths (pred (length limb_widths))) <= 2 ^ (nth_default 0 limb_widths 0); (* on the second reduce step, we add at most one bit of width to the first digit, and leave room to carry c one more time after the highest bit is carried *) - c_reduce2 : c <= 2 ^ (nth_default 0 limb_widths 0) - c + c_reduce2 : c <= 2 ^ (nth_default 0 limb_widths 0) - c; }. Section CanonicalizationProofs. @@ -940,8 +942,14 @@ Section CanonicalizationProofs. congruence. Qed. + Lemma int_width_compat : forall x, In x limb_widths -> x < int_width. + Proof. + intros. apply B_compat in H. + eapply Z.lt_le_trans; eauto using B_le_int_width. + Qed. + Lemma minimal_rep_freeze : forall u, initial_bounds u -> - minimal_rep (freeze B u). + minimal_rep (freeze int_width u). Proof. repeat match goal with | |- _ => progress (cbv [freeze ModularBaseSystemList.freeze]) @@ -952,12 +960,12 @@ Section CanonicalizationProofs. | |- _ => apply conditional_subtract_lt_modulus | |- _ => apply conditional_subtract_modulus_preserves_bounded | |- bounded _ (carry_full _) => apply bounded_iff - | |- _ => solve [auto using Z.lt_le_incl, B_pos, B_compat, lt_1_length_limb_widths, length_carry_full, length_to_list] + | |- _ => solve [auto using Z.lt_le_incl, int_width_pos, int_width_compat, lt_1_length_limb_widths, length_carry_full, length_to_list] end. Qed. Lemma freeze_decode : forall u, - BaseSystem.decode base (to_list _ (freeze B u)) mod modulus = + BaseSystem.decode base (to_list _ (freeze int_width u)) mod modulus = BaseSystem.decode base (to_list _ u) mod modulus. Proof. repeat match goal with @@ -967,7 +975,7 @@ Section CanonicalizationProofs. | |- _ => rewrite Z.mod_add by (pose proof prime_modulus; prime_bound) | |- _ => rewrite to_list_from_list | |- _ => rewrite conditional_subtract_modulus_spec by - auto using Z.lt_le_incl, B_pos, B_compat, lt_1_length_limb_widths, length_carry_full, length_to_list, ge_modulus_01 + (auto using Z.lt_le_incl, int_width_pos, int_width_compat, lt_1_length_limb_widths, length_carry_full, length_to_list, ge_modulus_01) end. rewrite !decode_mod_Fdecode by auto using length_carry_full, length_to_list. cbv [carry_full]. @@ -986,7 +994,7 @@ Section CanonicalizationProofs. rewrite from_list_to_list; reflexivity. Qed. - Lemma freeze_rep : forall u x, rep u x -> rep (freeze B u) x. + Lemma freeze_rep : forall u x, rep u x -> rep (freeze int_width u) x. Proof. cbv [rep]; intros. apply F.eq_to_Z_iff. @@ -997,7 +1005,7 @@ Section CanonicalizationProofs. Lemma freeze_canonical : forall u v x y, rep u x -> rep v y -> initial_bounds u -> initial_bounds v -> - (x = y <-> fieldwise Logic.eq (freeze B u) (freeze B v)). + (x = y <-> fieldwise Logic.eq (freeze int_width u) (freeze int_width v)). Proof. intros; apply bounded_canonical; auto using freeze_rep, minimal_rep_freeze. Qed. @@ -1022,7 +1030,7 @@ Section SquareRootProofs. Lemma eqb_true_iff : forall u v x y, bounded_by u freeze_input_bounds -> bounded_by v freeze_input_bounds -> - u ~= x -> v ~= y -> (x = y <-> eqb B u v = true). + u ~= x -> v ~= y -> (x = y <-> eqb int_width u v = true). Proof. cbv [eqb freeze_input_bounds]. intros. rewrite fieldwiseb_fieldwise by (apply Z.eqb_eq). @@ -1031,10 +1039,10 @@ Section SquareRootProofs. Lemma eqb_false_iff : forall u v x y, bounded_by u freeze_input_bounds -> bounded_by v freeze_input_bounds -> - u ~= x -> v ~= y -> (x <> y <-> eqb B u v = false). + u ~= x -> v ~= y -> (x <> y <-> eqb int_width u v = false). Proof. intros. - case_eq (eqb B u v). + case_eq (eqb int_width u v). + rewrite <-eqb_true_iff by eassumption; split; intros; congruence || contradiction. + split; intros; auto. @@ -1069,7 +1077,7 @@ Section SquareRootProofs. bounded_by powx_squared freeze_input_bounds -> ModularBaseSystem.eq powx (pow u chain) -> ModularBaseSystem.eq powx_squared (mul powx powx) -> - (sqrt_5mod8 B powx powx_squared chain chain_correct sqrt_m1 u) ~= F.sqrt_5mod8 (decode sqrt_m1) x. + (sqrt_5mod8 int_width powx powx_squared chain chain_correct sqrt_m1 u) ~= F.sqrt_5mod8 (decode sqrt_m1) x. Proof. cbv [sqrt_5mod8 F.sqrt_5mod8]. intros. -- cgit v1.2.3