diff --git a/src/Rewriter/Rules.v b/src/Rewriter/Rules.v index dee627c7418..66eab705ef9 100644 --- a/src/Rewriter/Rules.v +++ b/src/Rewriter/Rules.v @@ -288,18 +288,35 @@ Definition arith_rewrite_rulesT (max_const_val : Z) : list (bool * Prop) ; (forall s y x, Z.add_get_carry_full s (- y) x = dlet vb := Z.sub_get_borrow_full s x y in (fst vb, - snd vb)) + ; (forall s y x k, + Z.add_get_carry_full s x (-y * k) + = dlet vb := Z.sub_get_borrow_full s x (y * k) in (fst vb, - snd vb)) + ; (forall s y x k, + Z.add_get_carry_full s (-y * k) x + = dlet vb := Z.sub_get_borrow_full s x (y * k) in (fst vb, - snd vb)) ; (forall s y x, Z.add_with_get_carry_full s 0 x (- y) = dlet vb := Z.sub_get_borrow_full s x y in (fst vb, - snd vb)) ; (forall s y x, Z.add_with_get_carry_full s 0 (- y) x = dlet vb := Z.sub_get_borrow_full s x y in (fst vb, - snd vb)) + + ; (forall s c x, + Z.add_with_get_carry_full s (- c) x 0 + = dlet vb := Z.sub_with_get_borrow_full s c x 0 in (fst vb, - snd vb)) + ; (forall s c y x, Z.add_with_get_carry_full s (- c) (- y) x = dlet vb := Z.sub_with_get_borrow_full s c x y in (fst vb, - snd vb)) ; (forall s c y x, Z.add_with_get_carry_full s (- c) x (- y) = dlet vb := Z.sub_with_get_borrow_full s c x y in (fst vb, - snd vb)) + ; (forall s c y x k, + Z.add_with_get_carry_full s c x (-y * k) + = dlet vb := Z.sub_with_get_borrow_full s (-c) x (y * k) in (fst vb, - snd vb)) + ; (forall s c y x k, + Z.add_with_get_carry_full s c (-y * k) x + = dlet vb := Z.sub_with_get_borrow_full s (-c) x (y * k) in (fst vb, - snd vb)) ; (forall b x, (* inline negation when the rewriter wouldn't already inline it *) ident.gets_inlined b x = false -> -x = dlet v := x in -v) @@ -395,6 +412,16 @@ Definition arith_with_casts_rewrite_rulesT (adc_no_carry_to_add : bool) : list ( y ∈ ry -> y = Z.ones (Z.succ (Z.log2 y)) -> cstZ rv (cstZ ry ('y) &' cstZ rx x) = cstZ rx x) ]%Z%zrange + ; mymap + do_again + [ (forall x y, cstZ r[0~>1] x * y = Z.zselect (cstZ r[0~>1] x) (cstZ r[0~>0] (' 0)) y) + ; (forall x y, y * cstZ r[0~>1] x = Z.zselect (cstZ r[0~>1] x) (cstZ r[0~>0] (' 0)) y) + ; (forall c M rv r0 rM, 0 ∈ r0 -> M ∈ rM -> M ∈ rv -> 2^Z.log2 (M+1) = M + 1 -> 1 <= M -> + cstZ rv (Z.zselect (cstZ r[0~>1] c) (cstZ r0 ('0)) (cstZ rM ('M))) + = (dlet vc := cstZZ rv r[0~>1] (Z.sub_with_get_borrow_full ('(M+1)) (cstZ r[0~>1] c) 0 0) in + cstZ rv (fst vc))) + ; (forall rv c x y, cstZ rv (Z.zselect c x y) = dlet v := cstZ rv (Z.zselect c x y) in cstZ rv v) + ] ; mymap do_again [ (* [do_again], so that we can trigger add/sub rules on the output *) @@ -415,6 +442,11 @@ Definition arith_with_casts_rewrite_rulesT (adc_no_carry_to_add : bool) : list ( adc_no_carry_to_add = true -> s ∈ rs -> (n rx - n ry - n rc <= r[0~>s-1])%zrange -> cstZZ rv r[0~>0] (Z.sub_with_get_borrow_full (cstZ rs ('s)) (cstZ rc c) (cstZ rx x) (cstZ ry y)) = (cstZ rv (cstZ rx x - cstZ ry y - cstZ rc c), (cstZ r[0~>0] ('0)))) + (* 0-0-c passes through the carry *) + ; (forall rv rs s c rx ry, + s ∈ rs -> 0 ∈ rx -> 0 ∈ ry -> -1 / s = -1 + -> cstZZ rv r[0~>1] (Z.sub_with_get_borrow_full (cstZ rs ('s)) (cstZ r[0~>1] c) (cstZ rx ('0)) (cstZ ry ('0))) + = (cstZ rv (-(cstZ r[0~>1]c) mod 's), (cstZ r[0~>1] c))) ]%Z%zrange ; mymap dont_do_again diff --git a/src/Rewriter/RulesProofs.v b/src/Rewriter/RulesProofs.v index 6e7cc2dddd6..688f9283dcc 100644 --- a/src/Rewriter/RulesProofs.v +++ b/src/Rewriter/RulesProofs.v @@ -258,6 +258,13 @@ Local Ltac interp_good_t_step_arith := => cbv [Z.ltz]; apply unfold_is_bounded_by_bool in Hx; apply unfold_is_bounded_by_bool in Hy + | [ H : is_bounded_by_bool _ (ZRange.normalize r[0 ~> 1]) = true |- _ ] + => change (ZRange.normalize r[0 ~> 1]) with r[0 ~> 1]%zrange in *; + cbv [is_bounded_by_bool] in H; cbn [upper lower] in H + | [ H : ?x <> ?a, H' : ?a <= ?x |- _ ] => assert (a < x) by lia; clear H H' + | [ H : 0 < ?x, H' : ?x <= 1 |- _ ] => assert (x = 1) by lia; clear H H' + | [ H : ?x <= 1, H' : 0 <= ?x |- _ ] => assert (x = 0 \/ x = 1) by lia; clear H H' + | [ H : ?x = Z.neg _ |- context[?x] ] => rewrite H | [ |- context[ident.cast r[0~>0] ?v] ] => rewrite (ident.platform_specific_cast_0_is_mod 0 v) by reflexivity | [ H : ?x = Z.ones _ |- context [Z.land _ ?x] ] => rewrite H @@ -283,6 +290,7 @@ Local Ltac interp_good_t_step_arith := | progress destruct_head'_and | progress Z.ltb_to_lt | progress split_andb + | progress change (0 - 1) with (-1) in * | match goal with | [ |- ?a mod ?b = ?a' mod ?b ] => apply f_equal2; lia | [ |- ?a / ?b = ?a' / ?b ] => apply f_equal2; lia @@ -394,6 +402,9 @@ Local Ltac interp_good_t_step_arith := => tryif constr_eq x x' then fail else replace x with x' by lia | [ |- _ = _ :> BinInt.Z ] => progress autorewrite with zsimplify_fast end + | match goal with + | [ |- context[(- _) mod _] ] => rewrite Z.mod_opp_small by lia + end | saturate_add_sub_bounds_step ]. Local Ltac remove_casts := @@ -598,9 +609,9 @@ Proof. -- rewrite <- Z.mod_divide_full. assumption. + rewrite H2. apply Ones.Z.ones_nonneg. remember (Z.log2_nonneg (upper)). lia. + lia. - + rewrite H2. apply Ones.Z.ones_nonneg. remember (Z.log2_nonneg (upper)). lia. + + rewrite H2. apply Ones.Z.ones_nonneg. remember (Z.log2_nonneg (upper)). lia. Qed. - + Lemma arith_with_relaxed_casts_rewrite_rules_proofs : PrimitiveHList.hlist (@snd bool Prop) arith_with_relaxed_casts_rewrite_rulesT. Proof using Type. @@ -608,7 +619,7 @@ Proof using Type. - apply relaxed_rules_work; assumption. - rewrite Z.land_comm. apply relaxed_rules_work; assumption. Qed. - + Lemma strip_literal_casts_rewrite_rules_proofs : PrimitiveHList.hlist (@snd bool Prop) strip_literal_casts_rewrite_rulesT. Proof using Type.