diff options
author | Jason Gross <jagro@google.com> | 2016-08-05 19:30:44 -0700 |
---|---|---|
committer | Jason Gross <jagro@google.com> | 2016-08-09 16:47:33 -0700 |
commit | 7d3f54c975d24dc2f5fd8a0e31e004d74d7a3dd0 (patch) | |
tree | 854f1f859b1cfa8b60e4f62479fbb3d5bad174d4 /src/ModularArithmetic/BarrettReduction | |
parent | 97dd7cca1433f0cf42d28df671de54e4cfb746e0 (diff) |
Specify a type of bounded integers for mod arith
Also use it to implement Montgomery reduction and Barrett reduction.
Diffstat (limited to 'src/ModularArithmetic/BarrettReduction')
-rw-r--r-- | src/ModularArithmetic/BarrettReduction/ZBounded.v | 48 |
1 files changed, 48 insertions, 0 deletions
diff --git a/src/ModularArithmetic/BarrettReduction/ZBounded.v b/src/ModularArithmetic/BarrettReduction/ZBounded.v new file mode 100644 index 000000000..bcebd6ea7 --- /dev/null +++ b/src/ModularArithmetic/BarrettReduction/ZBounded.v @@ -0,0 +1,48 @@ +(*** Barrett Reduction *) +(** This file implements Barrett Reduction on [ZLikeOps]. We follow + [BarretReduction/ZHandbook.v]. *) +Require Import Coq.ZArith.ZArith Coq.Lists.List Coq.Classes.Morphisms Coq.micromega.Psatz. +Require Import Crypto.ModularArithmetic.BarrettReduction.ZHandbook. +Require Import Crypto.ModularArithmetic.Pow2Base. +Require Import Crypto.ModularArithmetic.ExtendedBaseVector. +Require Import Crypto.ModularArithmetic.ZBounded. +Require Import Crypto.BaseSystem. +Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.Tactics. +Require Import Crypto.Util.Notations. + +Local Open Scope small_zlike_scope. +Local Open Scope large_zlike_scope. +Local Open Scope Z_scope. + +Section barrett. + Context (m b 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 *) + (offset_nonneg : 0 <= offset) + (k_big_enough : offset <= k) + (m_small : 3 * m <= b^(k+offset)) + (m_large : b^(k-offset) <= m + 1). + Context {ops : ZLikeOps (b^(k+offset)) (b^(k-offset)) m} {props : ZLikeProperties ops} + (μ' : SmallT) + (μ'_good : small_valid μ') + (μ'_eq : decode_small μ' = μ). + + Definition barrett_reduce : forall x : LargeT, + { barrett_reduce : SmallT + | medium_valid x + -> decode_small barrett_reduce = (decode_large x) mod m + /\ small_valid barrett_reduce }. + Proof. + intro x. evar (pr : SmallT); exists pr. intros x_valid. + assert (0 <= decode_large x < b^(k+offset) * b^(k-offset)) by auto using decode_medium_valid. + assert (0 <= decode_large x < b^(2 * k)) by (autorewrite with pull_Zpow zsimplify in *; omega). + assert ((decode_large x) mod b^(k-offset) < b^(k-offset)) by auto with zarith omega. + rewrite (barrett_reduction_small m b (decode_large x) k μ offset) by omega. + rewrite <- μ'_eq. + pull_zlike_decode. + subst pr; split; [ reflexivity | exact _ ]. + Defined. +End barrett. |