diff options
author | Jason Gross <jgross@mit.edu> | 2016-10-16 19:38:39 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2016-10-16 19:38:39 -0400 |
commit | 55b5b72829f970f7b9180cc712351d54b7054130 (patch) | |
tree | 268be6845542cc8323d8174bbe23dce1e323ff0e /src | |
parent | 0f60b77ebbdcbc94197a2cf02665354303d3fdda (diff) |
Don't inline as much in ZBoundedZ
Diffstat (limited to 'src')
-rw-r--r-- | src/ModularArithmetic/ZBoundedZ.v | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/src/ModularArithmetic/ZBoundedZ.v b/src/ModularArithmetic/ZBoundedZ.v index 38032ec58..84508d2c7 100644 --- a/src/ModularArithmetic/ZBoundedZ.v +++ b/src/ModularArithmetic/ZBoundedZ.v @@ -3,6 +3,7 @@ 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.LetIn. Require Import Crypto.Util.Notations. Local Open Scope Z_scope. @@ -17,10 +18,11 @@ Global Instance ZZLikeOps small_bound_exp smaller_bound_exp modulus : ZLikeOps ( 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 }. + CarryAdd x y := dlet xpy := x + y in + ((2^small_bound_exp * 2^small_bound_exp <=? xpy), Z.pow2_mod xpy (2 * small_bound_exp)); + CarrySubSmall x y := dlet xmy := x - y in (xmy <? 0, Z.pow2_mod xmy small_bound_exp); + ConditionalSubtract b x := dlet x := x in if b then Z.pow2_mod (x - modulus) small_bound_exp else x; + ConditionalSubtractModulus x := dlet x := x in if x <? modulus then x else x - modulus }. Local Arguments Z.mul !_ !_. @@ -28,7 +30,7 @@ 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; + unfold cls_is_true, Let_In 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; |