diff options
author | Jason Gross <jgross@mit.edu> | 2016-10-16 19:20:22 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2016-10-16 19:20:22 -0400 |
commit | 0f60b77ebbdcbc94197a2cf02665354303d3fdda (patch) | |
tree | 99507e46a004d056d41adf1b04955a0243a2d0ce /src/ModularArithmetic | |
parent | 3f631a2d6bfcc8c67ec9991c6c5a74abe098eaa5 (diff) |
Add Z as ZBounded
Diffstat (limited to 'src/ModularArithmetic')
-rw-r--r-- | src/ModularArithmetic/ZBoundedZ.v | 85 |
1 files changed, 85 insertions, 0 deletions
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. |