diff options
| -rw-r--r-- | _CoqProject | 1 | ||||
| -rw-r--r-- | src/ModularArithmetic/ZBoundedZ.v | 85 |
2 files changed, 86 insertions, 0 deletions
diff --git a/_CoqProject b/_CoqProject index c328c0f08..d19f66259 100644 --- a/_CoqProject +++ b/_CoqProject @@ -80,6 +80,7 @@ src/ModularArithmetic/PseudoMersenneBaseParamProofs.v src/ModularArithmetic/PseudoMersenneBaseParams.v src/ModularArithmetic/Tutorial.v src/ModularArithmetic/ZBounded.v +src/ModularArithmetic/ZBoundedZ.v src/ModularArithmetic/BarrettReduction/Z.v src/ModularArithmetic/BarrettReduction/ZBounded.v src/ModularArithmetic/BarrettReduction/ZGeneralized.v diff --git a/src/ModularArithmetic/ZBoundedZ.v b/src/ModularArithmetic/ZBoundedZ.v new file mode 100644 index 000000000..38032ec58 --- /dev/null +++ b/src/ModularArithmetic/ZBoundedZ.v @@ -0,0 +1,85 @@ +(*** ℤ can be a bounded ℤ-Like type *) +Require Import Coq.ZArith.ZArith Coq.micromega.Psatz. +Require Import Crypto.ModularArithmetic.ZBounded. +Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.Tactics. +Require Import Crypto.Util.Notations. + +Local Open Scope Z_scope. + +Global Instance ZZLikeOps small_bound_exp smaller_bound_exp modulus : ZLikeOps (2^small_bound_exp) (2^smaller_bound_exp) modulus + := { LargeT := Z; + SmallT := Z; + modulus_digits := modulus; + decode_large x := x; + decode_small x := x; + Mod_SmallBound x := Z.pow2_mod x small_bound_exp; + DivBy_SmallBound x := Z.shiftr x small_bound_exp; + DivBy_SmallerBound x := Z.shiftr x smaller_bound_exp; + Mul x y := (x * y)%Z; + CarryAdd x y := ((2^small_bound_exp * 2^small_bound_exp <=? x + y), Z.pow2_mod (x + y) (2 * small_bound_exp)); + CarrySubSmall x y := (x - y <? 0, Z.pow2_mod (x - y) small_bound_exp); + ConditionalSubtract b x := if b then Z.pow2_mod (x - modulus) small_bound_exp else x; + ConditionalSubtractModulus x := if x <? modulus then x else x - modulus }. + +Local Arguments Z.mul !_ !_. + +Class cls_is_true (x : bool) := build_is_true : x = true. +Hint Extern 1 (cls_is_true ?b) => vm_compute; reflexivity : typeclass_instances. + +Local Ltac pre_t := + unfold cls_is_true in *; Z.ltb_to_lt; + match goal with + | [ H : ?smaller_bound_exp <= ?small_bound_exp |- _ ] + => is_var smaller_bound_exp; is_var small_bound_exp; + assert (2^smaller_bound_exp <= 2^small_bound_exp) by auto with zarith; + assert (2^small_bound_exp * 2^smaller_bound_exp <= 2^small_bound_exp * 2^small_bound_exp) by auto with zarith + end. + +Local Ltac t_step := + first [ progress simpl in * + | progress intros + | progress autorewrite with push_Zpow Zshift_to_pow in * + | rewrite Z.pow2_mod_spec by omega + | progress Z.ltb_to_lt + | solve [ auto with zarith ] + | nia + | progress break_match ]. +Local Ltac t := pre_t; repeat t_step. + +Global Instance ZZLikeProperties {small_bound_exp smaller_bound_exp modulus} + {Hss : cls_is_true (0 <=? smaller_bound_exp)} + {Hs : cls_is_true (0 <=? small_bound_exp)} + {Hs_ss : cls_is_true (smaller_bound_exp <=? small_bound_exp)} + {Hmod0 : cls_is_true (0 <=? modulus)} + {Hmod1 : cls_is_true (modulus <? 2^small_bound_exp)} + : ZLikeProperties (@ZZLikeOps small_bound_exp smaller_bound_exp modulus) + := { large_valid x := 0 <= x < 2^(2*small_bound_exp); + medium_valid x := 0 <= x < 2^(small_bound_exp + smaller_bound_exp); + small_valid x := 0 <= x < 2^small_bound_exp }. +Proof. + { abstract t. } + { abstract t. } + { abstract t. } + { abstract t. } + { abstract t. } + { abstract t. } + { abstract t. } + { abstract t. } + { abstract t. } + { abstract t. } + { abstract t. } + { abstract t. } + { abstract t. } + { abstract t. } + { abstract t. } + { abstract t. } + { abstract t. } + { abstract t. } + { abstract t. } + { abstract t. } + { abstract t. } + { abstract t. } + { abstract t. } + { abstract t. } +Defined. |