From 46cb41b734d877a1a62c4e4101eaa06561440f48 Mon Sep 17 00:00:00 2001 From: jadep Date: Wed, 15 Jun 2016 14:37:46 -0400 Subject: Added canonicalization to ModularBaseSystemOpt. --- src/ModularArithmetic/ModularBaseSystem.v | 6 +- src/ModularArithmetic/ModularBaseSystemOpt.v | 111 +++++++++++++++++++++++- src/ModularArithmetic/ModularBaseSystemProofs.v | 23 +++-- 3 files changed, 124 insertions(+), 16 deletions(-) (limited to 'src') diff --git a/src/ModularArithmetic/ModularBaseSystem.v b/src/ModularArithmetic/ModularBaseSystem.v index c25f89785..7989d641d 100644 --- a/src/ModularArithmetic/ModularBaseSystem.v +++ b/src/ModularArithmetic/ModularBaseSystem.v @@ -89,7 +89,7 @@ Section Canonicalization. | S i' => isFull' us (andb (Z.eqb (max_bound i) (nth_default 0 us i)) full) i' end. - Definition isFull us := isFull' us true (length us - 1)%nat. + Definition isFull us := isFull' us true (length base - 1)%nat. Fixpoint modulus_digits' i := match i with @@ -108,10 +108,12 @@ Section Canonicalization. | b :: lb' => f a b :: map2 f la' lb' end end. + + Definition and_term us := if isFull us then max_ones else 0. Definition freeze us := let us' := carry_full (carry_full (carry_full us)) in - let and_term := if isFull us' then max_ones else 0 in + let and_term := and_term us' in (* [and_term] is all ones if us' is full, so the subtractions subtract q overall. Otherwise, it's all zeroes, and the subtractions do nothing. *) map2 (fun x y => x - y) us' (map (Z.land and_term) modulus_digits). diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v index 981680b4a..71841d871 100644 --- a/src/ModularArithmetic/ModularBaseSystemOpt.v +++ b/src/ModularArithmetic/ModularBaseSystemOpt.v @@ -460,4 +460,113 @@ Section Multiplication. change (carry_mul_opt _ _ _) with (carry_sequence_opt_cps c_ is (mul_opt us vs)). apply carry_sequence_opt_cps_rep, mul_opt_rep; auto. Qed. -End Multiplication. \ No newline at end of file +End Multiplication. + +Section Canonicalization. + Context `{prm : PseudoMersenneBaseParams} {sc : SubtractionCoefficient modulus prm} + (* allows caller to precompute k and c *) + (k_ c_ : Z) (k_subst : k = k_) (c_subst : c = c_) + (lt_1_length_base : (1 < length base)%nat) + {int_width} (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)))) < max_bound 0 + 1) + (c_reduce2 : c <= max_bound 0 - c) + (two_pow_k_le_2modulus : 2 ^ k <= 2 * modulus). + + Print freeze. + Definition max_ones_opt := Eval compute in max_ones. + Definition max_bound_opt := Eval compute in max_bound. + Definition full_carry_chain_opt := Eval compute in full_carry_chain. + Definition length_opt := Eval compute in length. + Definition minus_opt := Eval compute in minus. + + Definition isFull'_opt_sig (us : T) full i : + { b : bool | b = isFull' us full i }. + Proof. + eexists. + cbv [isFull']. + change max_bound with max_bound_opt. + reflexivity. + Defined. + + Definition isFull'_opt (us : T) full i: bool + := Eval cbv [proj1_sig isFull'_opt_sig] in proj1_sig (isFull'_opt_sig us full i). + + Definition isFull'_opt_correct us full i: isFull'_opt us full i = isFull' us full i := + proj2_sig (isFull'_opt_sig us full i). + + Lemma full_carry_chain_bounds : forall i, In i full_carry_chain -> (i < length base)%nat. + Proof. + unfold full_carry_chain; rewrite <-base_length; intros. + apply make_chain_lt; auto. + Qed. + + Definition carry_full_opt_sig (us : T) : { b : digits | b = carry_full us }. + Proof. + eexists. + cbv [carry_full]. + change full_carry_chain with full_carry_chain_opt. + rewrite <-(carry_sequence_opt_cps_correct c_) by (auto; apply full_carry_chain_bounds). + reflexivity. + Defined. + + Definition carry_full_opt (us : T) : digits + := Eval cbv [proj1_sig carry_full_opt_sig] in proj1_sig (carry_full_opt_sig us). + + Definition carry_full_opt_correct us : carry_full_opt us = carry_full us := + proj2_sig (carry_full_opt_sig us). + + Definition and_term_opt_sig (us : T) : { b : Z | b = and_term us }. + Proof. + eexists. + cbv [and_term isFull]. + change length with length_opt. + rewrite <-isFull'_opt_correct. + change max_ones with max_ones_opt. + reflexivity. + Defined. + + Definition and_term_opt (us : T) : Z + := Eval cbv [proj1_sig and_term_opt_sig] in proj1_sig (and_term_opt_sig us). + + Definition and_term_opt_correct us : and_term_opt us = and_term us := + proj2_sig (and_term_opt_sig us). + + Definition freeze_opt_sig (us : T) : + { b : digits | b = freeze us }. + Proof. + eexists. + cbv beta iota delta [freeze map2]. + repeat rewrite <-carry_full_opt_correct. + change (@carry_full modulus prm) with @carry_full_opt. + change and_term with and_term_opt. + change @map with @map_opt. + reflexivity. + Defined. + + Definition freeze_opt (us : T) : digits + := Eval cbv [proj1_sig freeze_opt_sig] in proj1_sig (freeze_opt_sig us). + + Definition freeze_opt_correct us + : freeze_opt us = freeze us + := proj2_sig (freeze_opt_sig us). + + Lemma freeze_opt_canonical: forall us vs x, + @pre_carry_bounds _ _ int_width us -> (length us = length base) -> rep us x -> + @pre_carry_bounds _ _ int_width vs -> (length vs = length base) -> rep vs x -> + freeze_opt us = freeze_opt vs. + Proof. + intros. + rewrite !freeze_opt_correct. + eapply freeze_canonical with (B := int_width); eauto. + Qed. + + Lemma freeze_opt_preserves_rep : forall us x, (length us = length base) -> + rep us x -> rep (freeze_opt us) x. + Proof. + intros. + rewrite freeze_opt_correct. + eauto using freeze_preserves_rep. + Qed. + +End Canonicalization. \ No newline at end of file diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v index 350660323..8ac3a0faa 100644 --- a/src/ModularArithmetic/ModularBaseSystemProofs.v +++ b/src/ModularArithmetic/ModularBaseSystemProofs.v @@ -1229,9 +1229,6 @@ Section CanonicalizationProofs. right. apply IHl; auto using in_cons. Qed. - (* - Local Hint Resolve max_ones_nonneg. *) - Lemma land_max_ones_noop : forall x i, 0 <= x < 2 ^ log_cap i -> Z.land max_ones x = x. Proof. @@ -1343,7 +1340,7 @@ Section CanonicalizationProofs. Proof. destruct ls1; reflexivity. Qed. - Hint Resolve map2_nil_r map2_nil_l. + Local Hint Resolve map2_nil_r map2_nil_l. Opaque map2. @@ -1651,7 +1648,7 @@ Section CanonicalizationProofs. Proof. unfold rep; intros. intuition; rewrite ?freeze_length; auto. - unfold freeze. + unfold freeze, and_term. break_if. + apply decode_mod with (us := carry_full (carry_full (carry_full us))). - rewrite carry_full_3_length; auto. @@ -1679,14 +1676,14 @@ Section CanonicalizationProofs. Lemma isFull_true_iff : forall us, (length us = length base) -> (isFull us = true <-> max_bound 0 - c < nth_default 0 us 0 - /\ (forall i, (0 < i <= length us - 1)%nat -> nth_default 0 us i = max_bound i)). + /\ (forall i, (0 < i <= length base - 1)%nat -> nth_default 0 us i = max_bound i)). Proof. unfold isFull; intros; auto using isFull'_true_iff. Qed. - + Definition minimal_rep us := BaseSystem.decode base us = (BaseSystem.decode base us) mod modulus. - Fixpoint compare' us vs i := + Fixpoint compare' us vs i := match i with | O => Eq | S i' => if Z_eq_dec (nth_default 0 us i') (nth_default 0 vs i') @@ -1695,7 +1692,7 @@ Section CanonicalizationProofs. end. (* Lexicographically compare two vectors of equal length, starting from the END of the list - (in our context, this is the most significant end). *) + (in our context, this is the most significant end). NOT constant time. *) Definition compare us vs := compare' us vs (length us). Lemma compare'_Eq : forall us vs i, (length us = length vs) -> @@ -2012,7 +2009,7 @@ Section CanonicalizationProofs. pre_carry_bounds us -> (length us = length base) -> carry_done (freeze us). Proof. - unfold freeze; intros ? PCB lengths_eq. + unfold freeze, and_term; intros ? PCB lengths_eq. rewrite carry_done_bounds by simpl_lengths; intro i. rewrite nth_default_map2 with (d1 := 0) (d2 := 0). simpl_lengths. @@ -2030,7 +2027,7 @@ Section CanonicalizationProofs. rewrite carry_done_bounds in cf3_done by simpl_lengths. specialize (cf3_done 0%nat). omega. - - assert ((0 < i <= length (carry_full (carry_full (carry_full us))) - 1)%nat) as i_range by + - assert ((0 < i <= length base - 1)%nat) as i_range by (simpl_lengths; apply lt_min_l in l; omega). specialize (high_digits i i_range). clear first_digit i_range. @@ -2054,7 +2051,7 @@ Section CanonicalizationProofs. Lemma freeze_minimal_rep : forall us, pre_carry_bounds us -> (length us = length base) -> minimal_rep (freeze us). Proof. - unfold minimal_rep, freeze. + unfold minimal_rep, freeze, and_term. intros. symmetry. apply Z.mod_small. split; break_if; rewrite decode_map2_sub; simpl_lengths. @@ -2106,4 +2103,4 @@ Section CanonicalizationProofs. intros; eapply minimal_rep_unique; eauto; rewrite freeze_length; assumption. Qed. -End CanonicalizationProofs. +End CanonicalizationProofs. \ No newline at end of file -- cgit v1.2.3