From aee90845eec2475e1f2901d898b7f364272b6c71 Mon Sep 17 00:00:00 2001 From: jadep Date: Wed, 26 Oct 2016 20:08:10 -0400 Subject: Slightly loosen freeze preconditions (in particular, I had failed to properly account for the case when which [n] and [pred n] are BOTH out of bounds in my statement of initial bounds) --- src/ModularArithmetic/ModularBaseSystemOpt.v | 2 +- src/ModularArithmetic/ModularBaseSystemProofs.v | 71 ++++++++++++++++++++----- 2 files changed, 59 insertions(+), 14 deletions(-) (limited to 'src/ModularArithmetic') diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v index 89acd77f4..d2c73b57a 100644 --- a/src/ModularArithmetic/ModularBaseSystemOpt.v +++ b/src/ModularArithmetic/ModularBaseSystemOpt.v @@ -913,7 +913,7 @@ Section with_base. 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; + 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; diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v index 9a07e8ec0..f6efdfd87 100644 --- a/src/ModularArithmetic/ModularBaseSystemProofs.v +++ b/src/ModularArithmetic/ModularBaseSystemProofs.v @@ -525,7 +525,7 @@ Class FreezePreconditions `{prm : PseudoMersenneBaseParams} B := { lt_1_length_limb_widths : (1 < length limb_widths)%nat; B_pos : 0 < B; - B_compat : forall w, In w limb_widths -> w <= 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, @@ -666,8 +666,10 @@ Section CanonicalizationProofs. | |- _ => break_if; try omega | |- _ => progress simpl pred in * | |- _ => progress rewrite ?Z.add_0_r, ?Z.sub_0_r in * + | |- _ => rewrite nth_default_out_of_bounds by omega | |- _ => rewrite nth_default_carry_sequence_make_chain_full by auto | H : forall n, 0 <= _ [n] < _ |- appcontext [ _ [?n] ] => pose proof (H (pred n)); specialize (H n) + | H : forall n, (n < ?m)%nat -> 0 <= _ [n] < _ |- appcontext [ _ [?n] ] => pose proof (H (pred n)); specialize (H n); specialize_by omega | |- appcontext [make_chain 0] => simpl make_chain; rewrite carry_sequence_nil_l | |- 0 <= ?a + c * ?b < 2 * ?d => unique assert (c * b <= d); [ | solve [pose proof c_pos; rewrite <-Z.add_diag; split; zero_bounds] ] @@ -699,7 +701,7 @@ Section CanonicalizationProofs. Lemma bound_during_first_loop : forall us, length us = length limb_widths -> - (forall n, 0 <= us [n] < 2 ^ B - if eq_nat_dec n 0 then 0 else ((2 ^ B) >> (limb_widths [pred n]))) -> + (forall n, (n < length limb_widths)%nat -> 0 <= us [n] < 2 ^ B - if eq_nat_dec n 0 then 0 else ((2 ^ B) >> (limb_widths [pred n]))) -> forall i n, (i <= length limb_widths)%nat -> 0 <= us{{i}}[n] < if eq_nat_dec i 0 then us[n] + 1 else @@ -718,6 +720,30 @@ Section CanonicalizationProofs. induction i; bound_during_loop. Qed. + Lemma bound_after_loop_length_preconditions : forall us (Hlength : length us = length limb_widths) + {bound bound' bound'' : list Z -> nat -> Z} + {X Y : list Z -> nat -> nat -> Z} f, + (forall us, length us = length limb_widths + -> (forall n, (n < length limb_widths)%nat -> 0 <= us [n] < bound' us n) + -> forall i n, (i <= length limb_widths)%nat + -> 0 <= us{{i}}[n] < if eq_nat_dec i 0 then X us i n else + if lt_dec i (length limb_widths) + then Y us i n + else bound'' us n) -> + ((forall n, (n < length limb_widths)%nat -> 0 <= us [n] < bound us n) + -> forall n, (n < length limb_widths)%nat -> 0 <= (f us) [n] < bound' (f us) n) -> + length (f us) = length limb_widths -> + (forall n, (n < length limb_widths)%nat -> 0 <= us [n] < bound us n) + -> forall n, (n < length limb_widths)%nat -> 0 <= (carry_full (f us)) [n] < bound'' (f us) n. + Proof. + pose proof lt_1_length_limb_widths. + cbv [carry_full full_carry_chain]; intros ? ? ? ? ? ? ? ? Hloop Hfbound Hflength Hbound n. + specialize (Hfbound Hbound). + specialize (Hloop (f us) Hflength Hfbound (length limb_widths) n). + specialize_by omega. + repeat (break_if; try omega). + Qed. + Lemma bound_after_loop : forall us (Hlength : length us = length limb_widths) {bound bound' bound'' : list Z -> nat -> Z} {X Y : list Z -> nat -> nat -> Z} f, @@ -728,10 +754,10 @@ Section CanonicalizationProofs. if lt_dec i (length limb_widths) then Y us i n else bound'' us n) -> - ((forall n, 0 <= us [n] < bound us n) - -> forall n, 0 <= (f us) [n] < bound' (f us) n) -> - length (f us) = length limb_widths -> - (forall n, 0 <= us [n] < bound us n) + ((forall n, (n < length limb_widths)%nat -> 0 <= us [n] < bound us n) + -> forall n, 0 <= (f us) [n] < bound' (f us) n) + -> length (f us) = length limb_widths + -> (forall n, (n < length limb_widths)%nat -> 0 <= us [n] < bound us n) -> forall n, 0 <= (carry_full (f us)) [n] < bound'' (f us) n. Proof. pose proof lt_1_length_limb_widths. @@ -742,16 +768,35 @@ Section CanonicalizationProofs. repeat (break_if; try omega). Qed. + Lemma bound_after_first_loop_pre : forall us, + length us = length limb_widths -> + (forall n, (n < length limb_widths)%nat -> 0 <= us [n] < 2 ^ B - if eq_nat_dec n 0 then 0 else ((2 ^ B) >> (limb_widths [pred n]))) -> + forall n, (n < length limb_widths)%nat -> + 0 <= (carry_full us)[n] < + if eq_nat_dec n 0 + then 2 * 2 ^ limb_widths [n] + else 2 ^ limb_widths [n]. + Proof. + intros ? ?. + apply (bound_after_loop_length_preconditions us H id bound_during_first_loop); auto. + Qed. + Lemma bound_after_first_loop : forall us, length us = length limb_widths -> - (forall n, 0 <= us [n] < 2 ^ B - if eq_nat_dec n 0 then 0 else ((2 ^ B) >> (limb_widths [pred n]))) -> + (forall n, (n < length limb_widths)%nat -> 0 <= us [n] < 2 ^ B - if eq_nat_dec n 0 then 0 else ((2 ^ B) >> (limb_widths [pred n]))) -> forall n, 0 <= (carry_full us)[n] < if eq_nat_dec n 0 then 2 * 2 ^ limb_widths [n] else 2 ^ limb_widths [n]. Proof. - intros ? ?; apply (bound_after_loop us H id bound_during_first_loop); auto. + intros. + destruct (lt_dec n (length limb_widths)); + auto using bound_after_first_loop_pre. + rewrite !nth_default_out_of_bounds by (rewrite ?length_carry_full; omega). + autorewrite with zsimplify. + rewrite Z.pow_0_r. + break_if; omega. Qed. Lemma bound_during_second_loop : forall us, @@ -777,7 +822,7 @@ Section CanonicalizationProofs. Lemma bound_after_second_loop : forall us, length us = length limb_widths -> - (forall n, 0 <= us [n] < 2 ^ B - if eq_nat_dec n 0 then 0 else ((2 ^ B) >> (limb_widths [pred n]))) -> + (forall n, (n < length limb_widths)%nat -> 0 <= us [n] < 2 ^ B - if eq_nat_dec n 0 then 0 else ((2 ^ B) >> (limb_widths [pred n]))) -> forall n, 0 <= (carry_full (carry_full us)) [n] < if eq_nat_dec n 0 @@ -816,7 +861,7 @@ Section CanonicalizationProofs. Lemma bound_after_third_loop : forall us, length us = length limb_widths -> - (forall n, 0 <= us [n] < 2 ^ B - if eq_nat_dec n 0 then 0 else ((2 ^ B) >> (limb_widths [pred n]))) -> + (forall n, (n < length limb_widths)%nat -> 0 <= us [n] < 2 ^ B - if eq_nat_dec n 0 then 0 else ((2 ^ B) >> (limb_widths [pred n]))) -> forall n, 0 <= (carry_full (carry_full (carry_full us))) [n] < 2 ^ limb_widths [n]. Proof. @@ -826,7 +871,7 @@ Section CanonicalizationProofs. Qed. Local Notation initial_bounds u := - (forall n : nat, + (forall n : nat, (n < length limb_widths)%nat -> 0 <= to_list (length limb_widths) u [n] < 2 ^ B - (if eq_nat_dec n 0 @@ -907,7 +952,7 @@ Section CanonicalizationProofs. | |- _ => apply conditional_subtract_lt_modulus | |- _ => apply conditional_subtract_modulus_preserves_bounded | |- bounded _ (carry_full _) => apply bounded_iff - | |- _ => solve [auto using B_pos, B_compat, lt_1_length_limb_widths, length_carry_full, length_to_list] + | |- _ => solve [auto using Z.lt_le_incl, B_pos, B_compat, lt_1_length_limb_widths, length_carry_full, length_to_list] end. Qed. @@ -922,7 +967,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 B_pos, B_compat, lt_1_length_limb_widths, length_carry_full, length_to_list, ge_modulus_01 + auto using Z.lt_le_incl, B_pos, B_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]. -- cgit v1.2.3