diff options
author | Andres Erbsen <andreser@mit.edu> | 2017-04-06 22:53:07 -0400 |
---|---|---|
committer | Andres Erbsen <andreser@mit.edu> | 2017-04-06 22:53:07 -0400 |
commit | c9fc5a3cdf1f5ea2d104c150c30d1b1a6ac64239 (patch) | |
tree | db7187f6984acff324ca468e7b33d9285806a1eb /src/Arithmetic/BarrettReduction | |
parent | 21198245dab432d3c0ba2bb8a02254e7d0594382 (diff) |
rename-everything
Diffstat (limited to 'src/Arithmetic/BarrettReduction')
-rw-r--r-- | src/Arithmetic/BarrettReduction/Generalized.v | 140 | ||||
-rw-r--r-- | src/Arithmetic/BarrettReduction/HAC.v | 158 | ||||
-rw-r--r-- | src/Arithmetic/BarrettReduction/Wikipedia.v | 122 |
3 files changed, 420 insertions, 0 deletions
diff --git a/src/Arithmetic/BarrettReduction/Generalized.v b/src/Arithmetic/BarrettReduction/Generalized.v new file mode 100644 index 000000000..76058463c --- /dev/null +++ b/src/Arithmetic/BarrettReduction/Generalized.v @@ -0,0 +1,140 @@ +(*** Barrett Reduction *) +(** This file implements a slightly-generalized version of Barrett + Reduction on [Z]. This version follows a middle path between the + Handbook of Applied Cryptography (Algorithm 14.42) and Wikipedia. + We split up the shifting and the multiplication so that we don't + need to store numbers that are quite so large, but we don't do + early reduction modulo [b^(k+offset)] (we generalize from HAC's [k + ± 1] to [k ± offset]). This leads to weaker conditions on the + base ([b]), exponent ([k]), and the [offset] than those given in + the HAC. *) +Require Import Coq.ZArith.ZArith Coq.micromega.Psatz. +Require Import Crypto.Util.ZUtil Crypto.Util.Tactics.BreakMatch. + +Local Open Scope Z_scope. + +Section barrett. + Context (n a : Z) + (n_reasonable : n <> 0). + (** Quoting Wikipedia <https://en.wikipedia.org/wiki/Barrett_reduction>: *) + (** In modular arithmetic, Barrett reduction is a reduction + algorithm introduced in 1986 by P.D. Barrett. A naive way of + computing *) + (** [c = a mod n] *) + (** would be to use a fast division algorithm. Barrett reduction is + an algorithm designed to optimize this operation assuming [n] is + constant, and [a < n²], replacing divisions by + multiplications. *) + + (** * General idea *) + Section general_idea. + (** Let [m = 1 / n] be the inverse of [n] as a floating point + number. Then *) + (** [a mod n = a - ⌊a m⌋ n] *) + (** where [⌊ x ⌋] denotes the floor function. The result is exact, + as long as [m] is computed with sufficient accuracy. *) + + (* [/] is [Z.div], which means truncated division *) + Local Notation "⌊am⌋" := (a / n) (only parsing). + + Theorem naive_barrett_reduction_correct + : a mod n = a - ⌊am⌋ * n. + Proof using n_reasonable. + apply Zmod_eq_full; assumption. + Qed. + End general_idea. + + (** * Barrett algorithm *) + Section barrett_algorithm. + (** Barrett algorithm is a fixed-point analog which expresses + everything in terms of integers. Let [k] be the smallest + integer such that [2ᵏ > n]. Think of [n] as representing the + fixed-point number [n 2⁻ᵏ]. We precompute [m] such that [m = + ⌊4ᵏ / n⌋]. Then [m] represents the fixed-point number + [m 2⁻ᵏ ≈ (n 2⁻ᵏ)⁻¹]. *) + (** N.B. We don't need [k] to be the smallest such integer. *) + (** N.B. We generalize to an arbitrary base. *) + (** N.B. We generalize from [k ± 1] to [k ± offset]. *) + Context (b : Z) + (base_good : 0 < b) + (k : Z) + (k_good : n < b ^ k) + (m : Z) + (m_good : m = b^(2*k) / n) (* [/] is [Z.div], which is truncated *) + (offset : Z) + (offset_nonneg : 0 <= offset). + (** Wikipedia neglects to mention non-negativity, but we need it. + It might be possible to do with a relaxed assumption, such as + the sign of [a] and the sign of [n] being the same; but I + figured it wasn't worth it. *) + Context (n_pos : 0 < n) (* or just [0 <= n], since we have [n <> 0] above *) + (a_nonneg : 0 <= a). + + Context (k_big_enough : offset <= k) + (a_small : a < b^(2*k)) + (** We also need that [n] is large enough; [n] larger than + [bᵏ⁻¹] works, but we ask for something more precise. *) + (n_large : a mod b^(k-offset) <= n). + + (** Now *) + + Let q := (m * (a / b^(k-offset))) / b^(k+offset). + Let r := a - q * n. + (** Because of the floor function (in Coq, because [/] means + truncated division), [q] is an integer and [r ≡ a mod n]. *) + Theorem barrett_reduction_equivalent + : r mod n = a mod n. + Proof using m_good offset. + subst r q m. + rewrite <- !Z.add_opp_r, !Zopp_mult_distr_l, !Z_mod_plus_full by assumption. + reflexivity. + Qed. + + Lemma qn_small + : q * n <= a. + Proof using a_nonneg a_small base_good k_big_enough m_good n_pos n_reasonable offset_nonneg. + subst q r m. + assert (0 < b^(k-offset)). zero_bounds. + assert (0 < b^(k+offset)) by zero_bounds. + assert (0 < b^(2 * k)) by zero_bounds. + Z.simplify_fractions_le. + autorewrite with pull_Zpow pull_Zdiv zsimplify; reflexivity. + Qed. + + Lemma q_nice : { b : bool * bool | q = a / n + (if fst b then -1 else 0) + (if snd b then -1 else 0) }. + Proof using a_nonneg a_small base_good k_big_enough m_good n_large n_pos n_reasonable offset_nonneg. + assert (0 < b^(k+offset)) by zero_bounds. + assert (0 < b^(k-offset)) by zero_bounds. + assert (a / b^(k-offset) <= b^(2*k) / b^(k-offset)) by auto with zarith lia. + assert (a / b^(k-offset) <= b^(k+offset)) by (autorewrite with pull_Zpow zsimplify in *; assumption). + subst q r m. + rewrite (Z.div_mul_diff_exact''' (b^(2*k)) n (a/b^(k-offset))) by auto with lia zero_bounds. + rewrite (Z_div_mod_eq (b^(2*k) * _ / n) (b^(k+offset))) by lia. + autorewrite with push_Zmul push_Zopp zsimplify zstrip_div zdiv_to_mod. + rewrite Z.div_sub_mod_cond, !Z.div_sub_small by auto with zero_bounds zarith. + eexists (_, _); reflexivity. + Qed. + + Lemma r_small : r < 3 * n. + Proof using a_nonneg a_small base_good k_big_enough m_good n_large n_pos n_reasonable offset_nonneg q. + Hint Rewrite (Z.mul_div_eq' a n) using lia : zstrip_div. + assert (a mod n < n) by auto with zarith lia. + unfold r; rewrite (proj2_sig q_nice); generalize (proj1_sig q_nice); intro; subst q m. + autorewrite with push_Zmul zsimplify zstrip_div. + break_match; auto with lia. + Qed. + + (** In that case, we have *) + Theorem barrett_reduction_small + : a mod n = let r := if r <? n then r else r-n in + let r := if r <? n then r else r-n in + r. + Proof using a_nonneg a_small base_good k_big_enough m_good n_large n_pos n_reasonable offset_nonneg q. + pose proof r_small. pose proof qn_small. cbv zeta. + destruct (r <? n) eqn:Hr, (r-n <? n) eqn:?; try rewrite Hr; Z.ltb_to_lt; try lia. + { symmetry; apply (Zmod_unique a n q); subst r; lia. } + { symmetry; apply (Zmod_unique a n (q + 1)); subst r; lia. } + { symmetry; apply (Zmod_unique a n (q + 2)); subst r; lia. } + Qed. + End barrett_algorithm. +End barrett. diff --git a/src/Arithmetic/BarrettReduction/HAC.v b/src/Arithmetic/BarrettReduction/HAC.v new file mode 100644 index 000000000..70661ee96 --- /dev/null +++ b/src/Arithmetic/BarrettReduction/HAC.v @@ -0,0 +1,158 @@ +(*** Barrett Reduction *) +(** This file implements a slightly-generalized version of Barrett + Reduction on [Z]. This version follows the Handbook of Applied + Cryptography (Algorithm 14.42) rather closely; the only deviations + are that we generalize from [k ± 1] to [k ± offset] for an + arbitrary offset, and we weaken the conditions on the base [b] in + [bᵏ] slightly. Contrasted with some other versions, this version + does reduction modulo [b^(k+offset)] early (ensuring that we don't + have to carry around extra precision), but requires more stringint + conditions on the base ([b]), exponent ([k]), and the [offset]. *) +Require Import Coq.ZArith.ZArith Coq.micromega.Psatz. +Require Import Crypto.Util.ZUtil Crypto.Util.Tactics.BreakMatch. + +Local Open Scope Z_scope. + +Section barrett. + (** Quoting the Handbook of Applied Cryptography <http://cacr.uwaterloo.ca/hac/about/chap14.pdf>: *) + (** Barrett reduction (Algorithm 14.42) computes [r = x mod m] given + [x] and [m]. The algorithm requires the precomputation of the + quantity [µ = ⌊b²ᵏ/m⌋]; it is advantageous if many reductions + are performed with a single modulus. For example, each RSA + encryption for one entity requires reduction modulo that + entity’s public key modulus. The precomputation takes a fixed + amount of work, which is negligible in comparison to modular + exponentiation cost. Typically, the radix [b] is chosen to be + close to the word-size of the processor. Hence, assume [b > 3] in + Algorithm 14.42 (see Note 14.44 (ii)). *) + + (** * Barrett modular reduction *) + Section barrett_modular_reduction. + Context (m b x k μ offset : Z) + (m_pos : 0 < m) + (base_pos : 0 < b) + (k_good : m < b^k) + (μ_good : μ = b^(2*k) / m) (* [/] is [Z.div], which is truncated *) + (x_nonneg : 0 <= x) + (offset_nonneg : 0 <= offset) + (k_big_enough : offset <= k) + (x_small : x < b^(2*k)) + (m_small : 3 * m <= b^(k+offset)) + (** We also need that [m] is large enough; [m] larger than + [bᵏ⁻¹] works, but we ask for something more precise. *) + (m_large : x mod b^(k-offset) <= m). + + Let q1 := x / b^(k-offset). Let q2 := q1 * μ. Let q3 := q2 / b^(k+offset). + Let r1 := x mod b^(k+offset). Let r2 := (q3 * m) mod b^(k+offset). + (** At this point, the HAC says "If [r < 0] then [r ← r + bᵏ⁺¹]". + This is equivalent to reduction modulo [b^(k+offset)], as we + prove below. The version involving modular reduction has the + benefit of being cheaper to implement, and making the proofs + simpler, so we primarily use that version. *) + Let r_mod_3m := (r1 - r2) mod b^(k+offset). + Let r_mod_3m_orig := let r := r1 - r2 in + if r <? 0 then r + b^(k+offset) else r. + + Lemma r_mod_3m_eq_orig : r_mod_3m = r_mod_3m_orig. + Proof using base_pos k_big_enough m_pos m_small offset_nonneg r1 r2. + assert (0 <= r1 < b^(k+offset)) by (subst r1; auto with zarith). + assert (0 <= r2 < b^(k+offset)) by (subst r2; auto with zarith). + subst r_mod_3m r_mod_3m_orig; cbv zeta. + break_match; Z.ltb_to_lt. + { symmetry; apply (Zmod_unique (r1 - r2) _ (-1)); lia. } + { symmetry; apply (Zmod_unique (r1 - r2) _ 0); lia. } + Qed. + + (** 14.43 Fact By the division algorithm (Definition 2.82), there + exist integers [Q] and [R] such that [x = Qm + R] and [0 ≤ R < + m]. In step 1 of Algorithm 14.42 (Barrett modular reduction), + the following inequality is satisfied: [Q - 2 ≤ q₃ ≤ Q]. *) + (** We prove this by providing a more useful form for [q₃]. *) + Let Q := x / m. + Let R := x mod m. + Lemma q3_nice : { b : bool * bool | q3 = Q + (if fst b then -1 else 0) + (if snd b then -1 else 0) }. + Proof using base_pos k_big_enough m_large m_pos m_small offset_nonneg x_nonneg x_small μ_good. + assert (0 < b^(k+offset)) by zero_bounds. + assert (0 < b^(k-offset)) by zero_bounds. + assert (x / b^(k-offset) <= b^(2*k) / b^(k-offset)) by auto with zarith lia. + assert (x / b^(k-offset) <= b^(k+offset)) by (autorewrite with pull_Zpow zsimplify in *; assumption). + subst q1 q2 q3 Q r_mod_3m r_mod_3m_orig r1 r2 R μ. + rewrite (Z.div_mul_diff_exact' (b^(2*k)) m (x/b^(k-offset))) by auto with lia zero_bounds. + rewrite (Z_div_mod_eq (_ * b^(2*k) / m) (b^(k+offset))) by lia. + autorewrite with push_Zmul push_Zopp zsimplify zstrip_div zdiv_to_mod. + rewrite Z.div_sub_mod_cond, !Z.div_sub_small; auto with zero_bounds zarith. + eexists (_, _); reflexivity. + Qed. + + Fact q3_in_range : Q - 2 <= q3 <= Q. + Proof using base_pos k_big_enough m_large m_pos m_small offset_nonneg q2 x_nonneg x_small μ_good. + rewrite (proj2_sig q3_nice). + break_match; lia. + Qed. + + (** 14.44 Note (partial justification of correctness of Barrett reduction) *) + (** (i) Algorithm 14.42 is based on the observation that [⌊x/m⌋] + can be written as [Q = + ⌊(x/bᵏ⁻¹)(b²ᵏ/m)(1/bᵏ⁺¹)⌋]. Moreover, [Q] can be + approximated by the quantity [q₃ = ⌊⌊x/bᵏ⁻¹⌋µ/bᵏ⁺¹⌋]. + Fact 14.43 guarantees that [q₃] is never larger than the + true quotient [Q], and is at most 2 smaller. *) + Lemma x_minus_q3_m_in_range : 0 <= x - q3 * m < 3 * m. + Proof using base_pos k_big_enough m_large m_pos m_small offset_nonneg q2 x_nonneg x_small μ_good. + pose proof q3_in_range. + assert (0 <= R < m) by (subst R; auto with zarith). + assert (0 <= (Q - q3) * m + R < 3 * m) by nia. + subst Q R; autorewrite with push_Zmul zdiv_to_mod in *; lia. + Qed. + + Lemma r_mod_3m_eq_alt : r_mod_3m = x - q3 * m. + Proof using base_pos k_big_enough m_large m_pos m_small offset_nonneg q2 x_nonneg x_small μ_good. + pose proof x_minus_q3_m_in_range. + subst r_mod_3m r_mod_3m_orig r1 r2. + autorewrite with pull_Zmod zsimplify; reflexivity. + Qed. + + (** This version uses reduction modulo [b^(k+offset)]. *) + Theorem barrett_reduction_equivalent + : r_mod_3m mod m = x mod m. + Proof using base_pos k_big_enough m_large m_pos m_small offset_nonneg r1 r2 x_nonneg x_small μ_good. + rewrite r_mod_3m_eq_alt. + autorewrite with zsimplify push_Zmod; reflexivity. + Qed. + + (** This version, which matches the original in the HAC, uses + conditional addition of [b^(k+offset)]. *) + Theorem barrett_reduction_orig_equivalent + : r_mod_3m_orig mod m = x mod m. + Proof using base_pos k_big_enough m_large m_pos m_small offset_nonneg r_mod_3m x_nonneg x_small μ_good. rewrite <- r_mod_3m_eq_orig; apply barrett_reduction_equivalent. Qed. + + Lemma r_small : 0 <= r_mod_3m < 3 * m. + Proof using Q R base_pos k_big_enough m_large m_pos m_small offset_nonneg q3 x_nonneg x_small μ_good. + pose proof x_minus_q3_m_in_range. + subst Q R r_mod_3m r_mod_3m_orig r1 r2. + autorewrite with pull_Zmod zsimplify; lia. + Qed. + + + (** This version uses reduction modulo [b^(k+offset)]. *) + Theorem barrett_reduction_small (r := r_mod_3m) + : x mod m = let r := if r <? m then r else r-m in + let r := if r <? m then r else r-m in + r. + Proof using base_pos k_big_enough m_large m_pos m_small offset_nonneg r1 r2 x_nonneg x_small μ_good. + pose proof r_small. cbv zeta. + destruct (r <? m) eqn:Hr, (r-m <? m) eqn:?; subst r; rewrite !r_mod_3m_eq_alt, ?Hr in *; Z.ltb_to_lt; try lia. + { symmetry; eapply (Zmod_unique x m q3); lia. } + { symmetry; eapply (Zmod_unique x m (q3 + 1)); lia. } + { symmetry; eapply (Zmod_unique x m (q3 + 2)); lia. } + Qed. + + (** This version, which matches the original in the HAC, uses + conditional addition of [b^(k+offset)]. *) + Theorem barrett_reduction_small_orig (r := r_mod_3m_orig) + : x mod m = let r := if r <? m then r else r-m in + let r := if r <? m then r else r-m in + r. + Proof using base_pos k_big_enough m_large m_pos m_small offset_nonneg r_mod_3m x_nonneg x_small μ_good. subst r; rewrite <- r_mod_3m_eq_orig; apply barrett_reduction_small. Qed. + End barrett_modular_reduction. +End barrett. diff --git a/src/Arithmetic/BarrettReduction/Wikipedia.v b/src/Arithmetic/BarrettReduction/Wikipedia.v new file mode 100644 index 000000000..69ce10c4b --- /dev/null +++ b/src/Arithmetic/BarrettReduction/Wikipedia.v @@ -0,0 +1,122 @@ +(*** Barrett Reduction *) +(** This file implements Barrett Reduction on [Z]. We follow Wikipedia. *) +Require Import Coq.ZArith.ZArith Coq.micromega.Psatz. +Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.Tactics.BreakMatch. + +Local Open Scope Z_scope. + +Section barrett. + Context (n a : Z) + (n_reasonable : n <> 0). + (** Quoting Wikipedia <https://en.wikipedia.org/wiki/Barrett_reduction>: *) + (** In modular arithmetic, Barrett reduction is a reduction + algorithm introduced in 1986 by P.D. Barrett. A naive way of + computing *) + (** [c = a mod n] *) + (** would be to use a fast division algorithm. Barrett reduction is + an algorithm designed to optimize this operation assuming [n] is + constant, and [a < n²], replacing divisions by + multiplications. *) + + (** * General idea *) + Section general_idea. + (** Let [m = 1 / n] be the inverse of [n] as a floating point + number. Then *) + (** [a mod n = a - ⌊a m⌋ n] *) + (** where [⌊ x ⌋] denotes the floor function. The result is exact, + as long as [m] is computed with sufficient accuracy. *) + + (* [/] is [Z.div], which means truncated division *) + Local Notation "⌊am⌋" := (a / n) (only parsing). + + Theorem naive_barrett_reduction_correct + : a mod n = a - ⌊am⌋ * n. + Proof using n_reasonable. + apply Zmod_eq_full; assumption. + Qed. + End general_idea. + + (** * Barrett algorithm *) + Section barrett_algorithm. + (** Barrett algorithm is a fixed-point analog which expresses + everything in terms of integers. Let [k] be the smallest + integer such that [2ᵏ > n]. Think of [n] as representing the + fixed-point number [n 2⁻ᵏ]. We precompute [m] such that [m = + ⌊4ᵏ / n⌋]. Then [m] represents the fixed-point number + [m 2⁻ᵏ ≈ (n 2⁻ᵏ)⁻¹]. *) + (** N.B. We don't need [k] to be the smallest such integer. *) + Context (k : Z) + (k_good : n < 2 ^ k) + (m : Z) + (m_good : m = 4^k / n). (* [/] is [Z.div], which is truncated *) + (** Wikipedia neglects to mention non-negativity, but we need it. + It might be possible to do with a relaxed assumption, such as + the sign of [a] and the sign of [n] being the same; but I + figured it wasn't worth it. *) + Context (n_pos : 0 < n) (* or just [0 <= n], since we have [n <> 0] above *) + (a_nonneg : 0 <= a). + + Lemma k_nonnegative : 0 <= k. + Proof using Type*. + destruct (Z_lt_le_dec k 0); try assumption. + rewrite !Z.pow_neg_r in * by lia; lia. + Qed. + + (** Now *) + Let q := (m * a) / 4^k. + Let r := a - q * n. + (** Because of the floor function (in Coq, because [/] means + truncated division), [q] is an integer and [r ≡ a mod n]. *) + Theorem barrett_reduction_equivalent + : r mod n = a mod n. + Proof using m_good. + subst r q m. + rewrite <- !Z.add_opp_r, !Zopp_mult_distr_l, !Z_mod_plus_full by assumption. + reflexivity. + Qed. + + Lemma qn_small + : q * n <= a. + Proof using a_nonneg k_good m_good n_pos n_reasonable. + pose proof k_nonnegative; subst q r m. + assert (0 <= 2^(k-1)) by zero_bounds. + Z.simplify_fractions_le. + Qed. + + (** Also, if [a < n²] then [r < 2n]. *) + (** N.B. It turns out that it is sufficient to assume [a < 4ᵏ]. *) + Context (a_small : a < 4^k). + Lemma q_nice : { b : bool | q = a / n + if b then -1 else 0 }. + Proof using a_nonneg a_small k_good m_good n_pos n_reasonable. + assert (0 <= (4 ^ k * a / n) mod 4 ^ k < 4 ^ k) by auto with zarith lia. + assert (0 <= a * (4 ^ k mod n) / n < 4 ^ k) by (auto with zero_bounds zarith lia). + subst q r m. + rewrite (Z.div_mul_diff_exact''' (4^k) n a) by lia. + rewrite (Z_div_mod_eq (4^k * _ / n) (4^k)) by lia. + autorewrite with push_Zmul push_Zopp zsimplify zstrip_div. + eexists; reflexivity. + Qed. + + Lemma r_small : r < 2 * n. + Proof using a_nonneg a_small k_good m_good n_pos n_reasonable q. + Hint Rewrite (Z.mul_div_eq' a n) using lia : zstrip_div. + assert (a mod n < n) by auto with zarith lia. + unfold r; rewrite (proj2_sig q_nice); generalize (proj1_sig q_nice); intro; subst q m. + autorewrite with push_Zmul zsimplify zstrip_div. + break_match; auto with lia. + Qed. + + (** In that case, we have *) + Theorem barrett_reduction_small + : a mod n = if r <? n + then r + else r - n. + Proof using a_nonneg a_small k_good m_good n_pos n_reasonable q. + pose proof r_small. pose proof qn_small. + destruct (r <? n) eqn:rlt; Z.ltb_to_lt. + { symmetry; apply (Zmod_unique a n q); subst r; lia. } + { symmetry; apply (Zmod_unique a n (q + 1)); subst r; lia. } + Qed. + End barrett_algorithm. +End barrett. |