diff options
| author |  Jason Gross <jgross@mit.edu> | 2019-03-12 22:55:21 -0400 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2019-03-31 14:54:24 -0400 |
| commit | bacfa270c0c492ef8518d360d87e46cee292474f (patch) | |
| tree | c022e6e54a514f277ea395f44774aee8f762de6c | |
| parent | 31d31d23fbb6c9b3b7f01bd270cf72328f754594 (diff) | |
Factor out rewriter rules
Move rewrite rule definitions, and the proofs about them, into separate
files.
We don't yet make use of the separate interp proofs of rewrite rules;
the next step is to refactor the interp proof machinery so that we can
easily prove the relevant interp relations, given the equality proofs in
`src/RewriterRulesProofs.v`
After | File Name | Before || Change | % Change
--------------------------------------------------------------------------------------------
23m01.93s | Total | 22m37.08s || +0m24.84s | +1.83%
--------------------------------------------------------------------------------------------
0m24.10s | RewriterRulesProofs.vo | N/A || +0m24.10s | ∞
1m12.13s | Rewriter.vo | 1m20.61s || -0m08.48s | -10.51%
0m41.17s | ExtractionHaskell/unsaturated_solinas | 0m37.57s || +0m03.60s | +9.58%
1m42.40s | Fancy/Barrett256.vo | 1m40.22s || +0m02.18s | +2.17%
0m45.56s | p521_32.c | 0m48.16s || -0m02.59s | -5.39%
0m14.48s | ExtractionOCaml/word_by_word_montgomery.ml | 0m12.47s || +0m02.00s | +16.11%
1m48.48s | RewriterWf2.vo | 1m46.70s || +0m01.77s | +1.66%
0m15.06s | ExtractionOCaml/unsaturated_solinas | 0m14.06s || +0m01.00s | +7.11%
0m06.26s | ExtractionHaskell/unsaturated_solinas.hs | 0m07.29s || -0m01.03s | -14.12%
0m04.71s | ExtractionHaskell/saturated_solinas.hs | 0m06.05s || -0m01.33s | -22.14%
3m22.17s | p384_32.c | 3m23.06s || -0m00.88s | -0.43%
1m57.31s | RewriterRulesInterpGood.vo | 1m56.61s || +0m00.70s | +0.60%
1m35.20s | RewriterRulesGood.vo | 1m35.80s || -0m00.59s | -0.62%
0m57.50s | ExtractionHaskell/word_by_word_montgomery | 0m56.53s || +0m00.96s | +1.71%
0m45.71s | RewriterInterpProofs1.vo | 0m46.13s || -0m00.42s | -0.91%
0m39.66s | p521_64.c | 0m38.90s || +0m00.75s | +1.95%
0m36.22s | PushButtonSynthesis/UnsaturatedSolinas.vo | 0m36.42s || -0m00.20s | -0.54%
0m34.39s | Fancy/Montgomery256.vo | 0m34.45s || -0m00.06s | -0.17%
0m33.16s | RewriterWf1.vo | 0m32.96s || +0m00.19s | +0.60%
0m32.21s | ExtractionHaskell/saturated_solinas | 0m31.53s || +0m00.67s | +2.15%
0m26.94s | PushButtonSynthesis/WordByWordMontgomery.vo | 0m27.20s || -0m00.25s | -0.95%
0m25.89s | SlowPrimeSynthesisExamples.vo | 0m25.59s || +0m00.30s | +1.17%
0m23.37s | ExtractionOCaml/word_by_word_montgomery | 0m22.90s || +0m00.47s | +2.05%
0m21.19s | PushButtonSynthesis/BarrettReduction.vo | 0m20.79s || +0m00.40s | +1.92%
0m18.30s | p256_32.c | 0m18.54s || -0m00.23s | -1.29%
0m18.29s | p448_solinas_64.c | 0m18.58s || -0m00.28s | -1.56%
0m17.92s | secp256k1_32.c | 0m18.41s || -0m00.48s | -2.66%
0m14.06s | p434_64.c | 0m13.92s || +0m00.14s | +1.00%
0m11.61s | ExtractionOCaml/saturated_solinas | 0m11.57s || +0m00.03s | +0.34%
0m08.90s | p224_32.c | 0m09.12s || -0m00.21s | -2.41%
0m08.49s | ExtractionOCaml/unsaturated_solinas.ml | 0m08.85s || -0m00.35s | -4.06%
0m08.45s | ExtractionHaskell/word_by_word_montgomery.hs | 0m08.62s || -0m00.16s | -1.97%
0m08.02s | p384_64.c | 0m07.04s || +0m00.97s | +13.92%
0m07.01s | ExtractionOCaml/saturated_solinas.ml | 0m06.57s || +0m00.43s | +6.69%
0m06.67s | BoundsPipeline.vo | 0m06.87s || -0m00.20s | -2.91%
0m03.39s | PushButtonSynthesis/Primitives.vo | 0m03.44s || -0m00.04s | -1.45%
0m03.36s | PushButtonSynthesis/SmallExamples.vo | 0m03.38s || -0m00.02s | -0.59%
0m03.23s | PushButtonSynthesis/SaturatedSolinas.vo | 0m03.21s || +0m00.02s | +0.62%
0m03.04s | curve25519_32.c | 0m02.68s || +0m00.35s | +13.43%
0m02.74s | PushButtonSynthesis/MontgomeryReduction.vo | 0m02.55s || +0m00.19s | +7.45%
0m02.19s | curve25519_64.c | 0m01.81s || +0m00.37s | +20.99%
0m01.72s | secp256k1_64.c | 0m01.46s || +0m00.26s | +17.80%
0m01.56s | p256_64.c | 0m01.22s || +0m00.34s | +27.86%
0m01.49s | p224_64.c | 0m01.56s || -0m00.07s | -4.48%
0m01.32s | CLI.vo | 0m01.32s || +0m00.00s | +0.00%
0m01.14s | StandaloneHaskellMain.vo | 0m01.08s || +0m00.05s | +5.55%
0m01.06s | CompilersTestCases.vo | 0m01.04s || +0m00.02s | +1.92%
0m01.06s | StandaloneOCamlMain.vo | 0m01.12s || -0m00.06s | -5.35%
0m01.00s | RewriterProofs.vo | 0m01.13s || -0m00.12s | -11.50%
0m00.64s | RewriterRules.vo | N/A || +0m00.64s | ∞
| -rw-r--r-- | _CoqProject | 2 | ||||
| -rw-r--r-- | src/Rewriter.v | 822 | ||||
| -rw-r--r-- | src/RewriterRules.v | 788 | ||||
| -rw-r--r-- | src/RewriterRulesProofs.v | 485 |
4 files changed, 1286 insertions, 811 deletions
diff --git a/_CoqProject b/_CoqProject index 8fadf2f12..8c26d122b 100644 --- a/_CoqProject +++ b/_CoqProject @@ -37,8 +37,10 @@ src/MiscCompilerPassesProofs.v src/Rewriter.v src/RewriterInterpProofs1.v src/RewriterProofs.v +src/RewriterRules.v src/RewriterRulesGood.v src/RewriterRulesInterpGood.v +src/RewriterRulesProofs.v src/RewriterWf1.v src/RewriterWf2.v src/SlowPrimeSynthesisExamples.v diff --git a/src/Rewriter.v b/src/Rewriter.v index 3ca65c2bf..1d4910a5f 100644 --- a/src/Rewriter.v +++ b/src/Rewriter.v @@ -13,6 +13,7 @@ Require Import Crypto.Util.ZUtil.Notations. Require Import Crypto.Util.Tactics.ConstrFail. Require Crypto.Util.PrimitiveProd. Require Crypto.Util.PrimitiveHList. +Require Import Crypto.RewriterRules. Require Import Crypto.Language. Require Import Crypto.UnderLets. Require Import Crypto.GENERATEDIdentifiersWithoutTypes. @@ -2026,7 +2027,7 @@ Module Compilers. Ltac reify_list ident reify_ident pident pident_arg_types pident_type_of_list_arg_types_beq pident_of_typed_ident pident_arg_types_of_typed_ident reflect_ident_iota var lems := let reify' := reify ident reify_ident pident pident_arg_types pident_type_of_list_arg_types_beq pident_of_typed_ident pident_arg_types_of_typed_ident reflect_ident_iota var in let reify_list_rec := reify_list ident reify_ident pident pident_arg_types pident_type_of_list_arg_types_beq pident_of_typed_ident pident_arg_types_of_typed_ident reflect_ident_iota var in - lazymatch lems with + lazymatch (eval hnf in lems) with | (?b, ?lem) :: ?lems => let rlem := reify' b lem in let rlems := reify_list_rec lems in @@ -2400,498 +2401,30 @@ Module Compilers. Local Notation list := pattern.base.type.list. Local Notation "' x" := (ident.literal x). - (* - Local Arguments Make.interp_rewrite_rules / . - *) - (** - The follow are rules for rewriting expressions. On the left is a pattern to match: - ??: any expression whose type contains no arrows. - ??{x}: any expression whose type is x. - ??{list '1}: for example, a list with elements of a type variable '1. - x @ y: x applied to y. - #?x: a value, know at compile time, with type x. (Where x is one of {ℕ or N (nat), 𝔹 or B (bool), ℤ or Z (integers)}.) - #x: the identifer x. - - A matched expression is replaced with the right-hand-side, which is a function that returns a syntax tree, or None to indicate that the match didn't really match. The syntax tree is under two monads: option, and custom UnderLets monad. - - The function takes first any types that appeared as type variables (e.g., '1, '2, etc), and then the elements that where matched on the LHS as arguments. The arguments are given in the same order as on the LHS. - - In the RHS, the follow notation applies: - ##x: the literal value x - #x: the identifier x - x @ y: x applied to y - $x: PHOAS variable named x - λ: PHOAS abstraction / functions - - On the RHS, since we're returning a value under three monads, there's some fun notion for dealing with different levels of the monad stack in a single expression: - <-: bind, under the Option monad. - <--: bind, under the UnderLets monad - <---: bind, under the UnderLets+List monad. - <----: bind+ret, under the Option monad. - - There are eight choices for kinds of rewrite rules: - - [make_rewrite] for rules returning [expr] - - [make_rewriteo] for rules returning [option expr] - - [make_rewritel] for rules returning [UnderLets expr] - - [make_rewriteol] for rules returning [option (UnderLets expr)] - - [make_rewrite*_step] as [make_rewrite*] above, but indicating that rewriting should happen again in the result of rewriting with this rule. - - If stuck, email Jason. - *) Local Arguments pattern.anypattern : clear implicits. Local Arguments Make.interp_rewrite_rules / . Let myapp {A} := Eval cbv [List.app] in @List.app A. Let myflatten {A} := Eval cbv in List.fold_right myapp (@nil A). - Local Notation do_again P := (true, P) (only parsing). - Local Notation cstZ := (ident.cast ident.cast_outside_of_range). - Local Notation cstZZ := (ident.cast2 ident.cast_outside_of_range). - (* N.B. [ident.eagerly] does not play well with [do_again] *) Definition nbe_rewrite_rules : rewrite_rulesT := Eval cbv [Make.interp_rewrite_rules myapp myflatten] in - myapp - Make.interp_rewrite_rules - (myflatten - [reify - [(forall A B x y, @fst A B (x, y) = x) - ; (forall A B x y, @snd A B (x, y) = y) - ; (forall P t f, @ident.Thunked.bool_rect P t f true = t tt) - ; (forall P t f, @ident.Thunked.bool_rect P t f false = f tt) - ; (forall A B C f x y, @prod_rect A B (fun _ => C) f (x, y) = f x y) - - ; (forall A x n, - @List.repeat A x ('n) - = ident.eagerly (@nat_rect) _ nil (fun k repeat_k => x :: repeat_k) ('n)) - ; (forall A xs ys, - xs ++ ys - = ident.eagerly (@list_rect) A _ ys (fun x xs app_xs_ys => x :: app_xs_ys) xs) - ; (forall A B f a ls, - @fold_right A B f a ls - = (ident.eagerly (@list_rect) _ _) - a - (fun x xs fold_right_xs => f x fold_right_xs) - ls) - ; (forall A P N C ls, - @ident.Thunked.list_rect A P N C ls - = ident.eagerly (@ident.Thunked.list_rect) A P N C ls) - ; (forall A P Q N C ls v, - @list_rect A (fun _ => P -> Q) N C ls v - = ident.eagerly (@list_rect) A (fun _ => P -> Q) N C ls v) - ; (forall A P N C, @ident.Thunked.list_case A P N C nil = N tt) - ; (forall A P N C x xs, @ident.Thunked.list_case A P N C (x :: xs) = C x xs) - ; (forall A B f ls, - @List.map A B f ls - = (ident.eagerly (@list_rect) _ _) - nil - (fun x xs map_f_xs => f x :: map_f_xs) - ls) - ; (forall P O_case S_case n, - @ident.Thunked.nat_rect P O_case S_case ('n) - = (ident.eagerly (@ident.Thunked.nat_rect) _) - O_case - S_case - ('n)) - ; (forall P Q O_case S_case n v, - @nat_rect (fun _ => P -> Q) O_case S_case ('n) v - = (ident.eagerly (@nat_rect) _) - O_case - S_case - ('n) - v) - ; (forall A default ls n, - @List.nth_default A default ls ('n) - = ident.eagerly (@List.nth_default) _ default ls ('n)) - ] - ; reify - [do_again - (forall A B xs ys, - @List.combine A B xs ys - = (list_rect _) - (fun _ => nil) - (fun x xs combine_xs ys - => match ys with - | nil => nil - | y :: ys => (x, y) :: combine_xs ys - end) - xs - ys) - ; do_again - (forall A n ls, - @List.firstn A ('n) ls - = (nat_rect _) - (fun _ => nil) - (fun n' firstn_n' ls - => match ls with - | nil => nil - | cons x xs => x :: firstn_n' xs - end) - ('n) - ls) - ; do_again - (forall A n ls, - @List.skipn A ('n) ls - = (nat_rect _) - (fun ls => ls) - (fun n' skipn_n' ls - => match ls with - | nil => nil - | cons x xs => skipn_n' xs - end) - ('n) - ls) - ; do_again - (forall A xs, - @List.length A xs - = (list_rect _) - 0%nat - (fun _ xs length_xs => S length_xs) - xs) - ; do_again - (forall A xs, - @List.rev A xs - = (list_rect _) - nil - (fun x xs rev_xs => rev_xs ++ [x]) - xs) - ; do_again - (forall A B f xs, - @List.flat_map A B f xs - = (list_rect _) - nil - (fun x _ flat_map_tl => f x ++ flat_map_tl) - xs) - ; do_again - (forall A f xs, - @List.partition A f xs - = (list_rect _) - ([], []) - (fun x tl partition_tl - => let '(g, d) := partition_tl in - if f x then (x :: g, d) else (g, x :: d)) - xs) - ; do_again - (forall A n f xs, - @update_nth A ('n) f xs - = (nat_rect _) - (fun xs => match xs with - | nil => nil - | x' :: xs' => f x' :: xs' - end) - (fun n' update_nth_n' xs - => match xs with - | nil => nil - | x' :: xs' => x' :: update_nth_n' xs' - end) - ('n) - xs) - ] - ]). + myflatten + [Make.interp_rewrite_rules + ; reify nbe_rewrite_rulesT + ]. Definition arith_rewrite_rules (max_const_val : Z) : rewrite_rulesT := Eval cbv [Make.interp_rewrite_rules myapp myflatten] in myflatten - [reify - [(forall A B x y, @fst A B (x, y) = x) - ; (forall A B x y, @snd A B (x, y) = y) - ; (forall v, 0 + v = v) - ; (forall v, v + 0 = v) - ; (forall x y, (-x) + (-y) = -(x + y)) - ; (forall x y, (-x) + y = y - x) - ; (forall x y, x + (-y) = x - y) - - ; (forall v, 0 - (-v) = v) - ; (forall v, 0 - v = -v) - ; (forall v, v - 0 = v) - ; (forall x y, (-x) - (-y) = y - x) - ; (forall x y, (-x) - y = -(x + y)) - ; (forall x y, x - (-y) = x + y) - - ; (forall v, 0 * v = 0) - ; (forall v, v * 0 = 0) - ; (forall v, 1 * v = v) - ; (forall v, v * 1 = v) - ; (forall v, (-1) * (-v) = v) - ; (forall v, (-v) * (-1) = v) - ; (forall v, (-1) * v = -v) - ; (forall v, v * (-1) = -v) - ; (forall x y, (-x) * (-y) = x * y) - ; (forall x y, (-x) * y = -(x * y)) - ; (forall x y, x * (-y) = -(x * y)) - - ; (forall x, x &' 0 = 0) - - ; (forall x, x / 1 = x) - ; (forall x, x mod 1 = 0) - - ; (forall v, -(-v) = v) - - ; (forall z v, z > 0 -> 'z + (-v) = 'z - v) - ; (forall z v, z > 0 -> (-v) + 'z = 'z - v) - ; (forall z v, z < 0 -> 'z + (-v) = -('(-z) + v)) - ; (forall z v, z < 0 -> (-v) + 'z = -(v + '(-z))) - - ; (forall z v, z > 0 -> 'z - (-v) = 'z + v) - ; (forall z v, z < 0 -> 'z - (-v) = v - '(-z)) - ; (forall z v, z < 0 -> 'z - v = -('(-z) + v)) - ; (forall z v, z > 0 -> (-v) - 'z = -(v + 'z)) - ; (forall z v, z < 0 -> (-v) - 'z = '(-z) - v) - ; (forall z v, z < 0 -> v - 'z = v + '(-z)) - - ; (forall x y, 'x * 'y = '(x*y)) - ; (forall z v, z < 0 -> 'z * v = -('(-z) * v)) - ; (forall z v, z < 0 -> v * 'z = -(v * '(-z))) - - ; (forall x y, y = 2^Z.log2 y -> y <> 2 -> x * 'y = x << '(Z.log2 y)) - ; (forall x y, y = 2^Z.log2 y -> y <> 2 -> 'y * x = x << '(Z.log2 y)) - - ; (forall x y, y = 2^Z.log2 y -> x / 'y = x >> '(Z.log2 y)) - ; (forall x y, y = 2^Z.log2 y -> x mod 'y = x &' '(y-1)) - - (* We reassociate some multiplication of small constants *) - ; (forall c1 c2 x y, - Z.abs c1 <= Z.abs max_const_val - -> Z.abs c2 <= Z.abs max_const_val - -> 'c1 * ('c2 * (x * y)) = (x * (y * ('c1 * 'c2)))) - ; (forall c1 c2 x y, - Z.abs c1 <= Z.abs max_const_val - -> Z.abs c2 <= Z.abs max_const_val - -> 'c1 * (x * (y * 'c2)) = (x * (y * ('c1 * 'c2)))) - ; (forall c x y, - Z.abs c <= Z.abs max_const_val - -> 'c * (x * y) = x * (y * 'c)) - ; (forall c x, - Z.abs c <= Z.abs max_const_val - -> 'c * x = x * 'c) - - (* transform +- to + *) - ; (forall s y x, - Z.add_get_carry_full s x (- y) - = dlet vb := Z.sub_get_borrow_full s x y in (fst vb, - snd vb)) - ; (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, - 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 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)) - ] - ; reify - [ (* [do_again], so that if one of the arguments is concrete, we automatically get the rewrite rule for [Z_cast] applying to it *) - do_again (forall r x y, cstZZ r (x, y) = (cstZ (fst r) x, cstZ (snd r) y)) - ] - + [reify (arith_rewrite_rulesT max_const_val) ; [ make_rewriteol (-??) (fun e => (llet v := e in -$v) when negb (SubstVarLike.is_var_fst_snd_pair_opp_cast e)) (* inline negation when the rewriter wouldn't already inline it *) ] ]. - Let cst {var} (r : zrange) (e : @expr.expr _ _ var _) := (#(ident.Z_cast r) @ e)%expr. - Let cst' {var} (r : zrange) (e : @expr.expr _ _ var _) := (#(ident.Z_cast (-r)) @ e)%expr. - Let cst2 {var} (r : zrange * zrange) (e : @expr.expr _ _ var _) := (#(ident.Z_cast2 r) @ e)%expr. - - Let llet2_opp2 (rvc : zrange * zrange) e - := (let rvc' := (fst rvc, -snd rvc)%zrange in - let cst' e := #(ident.Z_cast2 rvc') @ e in - let cst1 e := #(ident.Z_cast (fst rvc)) @ e in - let cst2 e := #(ident.Z_cast (snd rvc)) @ e in - let cst2' e := #(ident.Z_cast (-snd rvc)) @ e in - (llet vc := cst' e in - (cst1 (#ident.fst @ (cst' ($vc))), cst2 (-(cst2' (#ident.snd @ (cst' ($vc))))))))%expr. - - Let llet2 (rvc : zrange * zrange) e - := ((llet vc := cst2 rvc e in - (cst (fst rvc) (#ident.fst @ (cst2 rvc ($vc))), - cst (snd rvc) (#ident.snd @ (cst2 rvc ($vc))))))%expr. - - Local Notation "'plet' x := y 'in' z" - := (match y return _ with x => z end). - - Local Notation dlet2_opp2 rvc e - := (plet rvc' := (fst rvc, -snd rvc)%zrange in - plet cst' := cstZZ rvc' in - plet cst1 := cstZ (fst rvc%zrange%zrange) in - plet cst2 := cstZ (snd rvc%zrange%zrange) in - plet cst2' := cstZ (-snd rvc%zrange%zrange) in - (dlet vc := cst' e in - (cst1 (fst (cst' vc)), cst2 (-(cst2' (snd (cst' vc))))))). - - Local Notation dlet2 rvc e - := (dlet vc := cstZZ rvc e in - (cstZ (fst rvc) (fst (cstZZ rvc vc)), - cstZ (snd rvc) (snd (cstZZ rvc vc)))). - - - Local Notation "x '\in' y" := (is_bounded_by_bool x (ZRange.normalize y) = true) : zrange_scope. - Local Notation "x ∈ y" := (is_bounded_by_bool x (ZRange.normalize y) = true) : zrange_scope. - Local Notation "x <= y" := (is_tighter_than_bool (ZRange.normalize x) y = true) : zrange_scope. - Local Notation litZZ x := (ident.literal (fst x), ident.literal (snd x)) (only parsing). - Local Notation n r := (ZRange.normalize r) (only parsing). - Definition arith_with_casts_rewrite_rules : rewrite_rulesT - := Eval cbv [Make.interp_rewrite_rules myapp myflatten] in - myflatten - [reify - [(forall A B x y, @fst A B (x, y) = x) - ; (forall A B x y, @snd A B (x, y) = y) - ; (forall r v, lower r = upper r -> cstZ r v = cstZ r ('(lower r))) - ; (forall r0 v, 0 ∈ r0 -> cstZ r0 0 + v = v) - ; (forall r0 v, 0 ∈ r0 -> v + cstZ r0 0 = v) - ; (forall r0 v, 0 ∈ r0 -> cstZ r0 0 - v = -v) - ; (forall r0 v, 0 ∈ r0 -> cstZ r0 0 << v = 0) - ; (forall r0 rnv rv v, - (rv <= -n rnv)%zrange -> 0 ∈ r0 - -> cstZ r0 0 - cstZ rnv (-(cstZ rv v)) = cstZ rv v) - ; (forall rnv rv v, - (rv <= -n rnv)%zrange - -> -(cstZ rnv (-(cstZ rv v))) = cstZ rv v) - - ; (forall s r0 y, 0 ∈ r0 -> Z.mul_split s (cstZ r0 0) y = (cstZ r[0~>0] 0, cstZ r[0~>0] 0)) - ; (forall s r0 y, 0 ∈ r0 -> Z.mul_split s y (cstZ r0 0) = (cstZ r[0~>0] 0, cstZ r[0~>0] 0)) - ; (forall rs s r1 ry y, - 1 ∈ r1 -> s ∈ rs -> (ry <= r[0~>s-1])%zrange - -> Z.mul_split (cstZ rs ('s)) (cstZ r1 1) (cstZ ry y) - = (cstZ ry y, cstZ r[0~>0] 0)) - ; (forall rs s r1 ry y, - 1 ∈ r1 -> s ∈ rs -> (ry <= r[0~>s-1])%zrange - -> Z.mul_split (cstZ rs ('s)) (cstZ ry y) (cstZ r1 1) - = (cstZ ry y, cstZ r[0~>0] 0)) - - ; (forall rvc s rny ry y x, - (ry <= -n rny)%zrange - -> cstZZ rvc (Z.add_get_carry_full s (cstZ rny (-cstZ ry y)) x) - = dlet2_opp2 rvc (Z.sub_get_borrow_full s x (cstZ ry y))) - ; (forall rvc s rny ry y x, - (ry <= -n rny)%zrange - -> cstZZ rvc (Z.add_get_carry_full s x (cstZ rny (-cstZ ry y))) - = dlet2_opp2 rvc (Z.sub_get_borrow_full s x (cstZ ry y))) - ; (forall rvc s ryy yy x, - yy ∈ ryy -> yy < 0 - -> cstZZ rvc (Z.add_get_carry_full s (cstZ ryy ('yy)) x) - = dlet2_opp2 rvc (Z.sub_get_borrow_full s x (cstZ (-ryy) ('(-yy))))) - ; (forall rvc s ryy yy x, - yy ∈ ryy -> yy < 0 - -> cstZZ rvc (Z.add_get_carry_full s x (cstZ ryy ('yy))) - = dlet2_opp2 rvc (Z.sub_get_borrow_full s x (cstZ (-ryy) ('(-yy))))) - ; (forall rvc s rnc rc c rny ry y x, - (ry <= -n rny)%zrange -> (rc <= -n rnc)%zrange - -> cstZZ rvc (Z.add_with_get_carry_full s (cstZ rnc (-cstZ rc c)) (cstZ rny (-cstZ ry y)) x) - = dlet2_opp2 rvc (Z.sub_with_get_borrow_full s (cstZ rc c) x (cstZ ry y))) - ; (forall rvc s rnc rc c rny ry y x, - (ry <= -n rny)%zrange -> (rc <= -n rnc)%zrange - -> cstZZ rvc (Z.add_with_get_carry_full s (cstZ rnc (-cstZ rc c)) x (cstZ rny (-cstZ ry y))) - = dlet2_opp2 rvc (Z.sub_with_get_borrow_full s (cstZ rc c) x (cstZ ry y))) - ; (forall rvc s r0 rny ry y x, - 0 ∈ r0 -> (ry <= -n rny)%zrange - -> cstZZ rvc (Z.add_with_get_carry_full s (cstZ r0 0) (cstZ rny (-cstZ ry y)) x) - = dlet2_opp2 rvc (Z.sub_get_borrow_full s x (cstZ ry y))) - ; (forall rvc s rcc cc rny ry y x, - cc < 0 -> cc ∈ rcc -> (ry <= -n rny)%zrange - -> cstZZ rvc (Z.add_with_get_carry_full s (cstZ rcc ('cc)) (cstZ rny (-cstZ ry y)) x) - = dlet2_opp2 rvc (Z.sub_with_get_borrow_full s (cstZ (-rcc) ('(-cc))) x (cstZ ry y))) - ; (forall rvc s r0 rny ry y x, - 0 ∈ r0 -> (ry <= -n rny)%zrange - -> cstZZ rvc (Z.add_with_get_carry_full s (cstZ r0 0) x (cstZ rny (-cstZ ry y))) - = dlet2_opp2 rvc (Z.sub_get_borrow_full s x (cstZ ry y))) - ; (forall rvc s rcc cc rny ry y x, - cc < 0 -> cc ∈ rcc -> (ry <= -n rny)%zrange - -> cstZZ rvc (Z.add_with_get_carry_full s (cstZ rcc ('cc)) x (cstZ rny (-cstZ ry y))) - = dlet2_opp2 rvc (Z.sub_with_get_borrow_full s (cstZ (-rcc) ('(-cc))) x (cstZ ry y))) - ; (forall rvc s rnc rc c ryy yy x, - yy <= 0 -> yy ∈ ryy -> (rc <= -n rnc)%zrange - -> cstZZ rvc (Z.add_with_get_carry_full s (cstZ rnc (-cstZ rc c)) (cstZ ryy ('yy)) x) - = dlet2_opp2 rvc (Z.sub_with_get_borrow_full s (cstZ rc c) x (cstZ (-ryy) ('(-yy))))) - ; (forall rvc s rnc rc c ryy yy x, - yy <= 0 -> yy ∈ ryy -> (rc <= -n rnc)%zrange - -> cstZZ rvc (Z.add_with_get_carry_full s (cstZ rnc (-cstZ rc c)) x (cstZ ryy ('yy))) - = dlet2_opp2 rvc (Z.sub_with_get_borrow_full s (cstZ rc c) x (cstZ (-ryy) ('(-yy))))) - ; (forall rvc s rcc cc ryy yy x, - yy <= 0 -> cc <= 0 -> yy + cc < 0 (* at least one must be strictly negative *) -> yy ∈ ryy -> cc ∈ rcc - -> cstZZ rvc (Z.add_with_get_carry_full s (cstZ rcc ('cc)) (cstZ ryy ('yy)) x) - = dlet2_opp2 rvc (Z.sub_with_get_borrow_full s (cstZ (-rcc) ('(-cc))) x (cstZ (-ryy) ('(-yy))))) - ; (forall rvc s rcc cc ryy yy x, - yy <= 0 -> cc <= 0 -> yy + cc < 0 (* at least one must be strictly negative *) -> yy ∈ ryy -> cc ∈ rcc - -> cstZZ rvc (Z.add_with_get_carry_full s (cstZ rcc ('cc)) x (cstZ ryy ('yy))) - = dlet2_opp2 rvc (Z.sub_with_get_borrow_full s (cstZ (-rcc) ('(-cc))) x (cstZ (-ryy) ('(-yy))))) - - - ; (forall rs s rxx xx ryy yy, - s ∈ rs -> xx ∈ rxx -> yy ∈ ryy - -> Z.add_get_carry_full (cstZ rs ('s)) (cstZ rxx ('xx)) (cstZ ryy ('yy)) - = litZZ (Z.add_get_carry_full s xx yy)) - ; (forall rs s r0 ry y, - s ∈ rs -> 0 ∈ r0 -> (ry <= r[0~>s-1])%zrange - -> Z.add_get_carry_full (cstZ rs ('s)) (cstZ r0 0) (cstZ ry y) - = (cstZ ry y, cstZ r[0~>0] 0)) - ; (forall rs s r0 ry y, - s ∈ rs -> 0 ∈ r0 -> (ry <= r[0~>s-1])%zrange - -> Z.add_get_carry_full (cstZ rs ('s)) (cstZ ry y) (cstZ r0 0) - = (cstZ ry y, cstZ r[0~>0] 0)) - - ; (forall r0 x y, 0 ∈ r0 -> Z.add_with_carry (cstZ r0 0) x y = x + y) - - ; (forall rs s rcc cc rxx xx ryy yy, - s ∈ rs -> cc ∈ rcc -> xx ∈ rxx -> yy ∈ ryy - -> Z.add_with_get_carry_full (cstZ rs ('s)) (cstZ rcc ('cc)) (cstZ rxx ('xx)) (cstZ ryy ('yy)) - = litZZ (Z.add_with_get_carry_full s cc xx yy)) - ; (forall rs s r0c r0x ry y, - s ∈ rs -> 0 ∈ r0c -> 0 ∈ r0x -> (ry <= r[0~>s-1])%zrange - -> Z.add_with_get_carry_full (cstZ rs ('s)) (cstZ r0c 0) (cstZ r0x 0) (cstZ ry y) - = (cstZ ry y, cstZ r[0~>0] 0)) - ; (forall rs s r0c r0x ry y, - s ∈ rs -> 0 ∈ r0c -> 0 ∈ r0x -> (ry <= r[0~>s-1])%zrange - -> Z.add_with_get_carry_full (cstZ rs ('s)) (cstZ r0c 0) (cstZ ry y) (cstZ r0x 0) - = (cstZ ry y, cstZ r[0~>0] 0)) - - ; (forall rvc s r0 x y, (* carry = 0: ADC x y -> ADD x y *) - 0 ∈ r0 - -> cstZZ rvc (Z.add_with_get_carry_full s (cstZ r0 0) x y) - = dlet2 rvc (Z.add_get_carry_full s x y)) - ; (forall rvc rs s rc c r0x r0y, (* ADC 0 0 -> (ADX 0 0, 0) *) (* except we don't do ADX, because C stringification doesn't handle it *) - 0 ∈ r0x -> 0 ∈ r0y -> (rc <= r[0~>s-1])%zrange -> 0 ∈ snd rvc -> s ∈ rs - -> cstZZ rvc (Z.add_with_get_carry_full (cstZ rs ('s)) (cstZ rc c) (cstZ r0x 0) (cstZ r0y 0)) - = (dlet vc := (cstZZ rvc (Z.add_with_get_carry_full (cstZ rs ('s)) (cstZ rc c) (cstZ r0x 0) (cstZ r0y 0))) in - (cstZ (fst rvc) (fst (cstZZ rvc vc)), - cstZ r[0~>0] 0))) - - (* let-bind any adc/sbb/mulx *) - ; (forall rvc s c x y, - cstZZ rvc (Z.add_with_get_carry_full s c x y) - = dlet2 rvc (Z.add_with_get_carry_full s c x y)) - ; (forall rv c x y, - cstZ rv (Z.add_with_carry c x y) - = (dlet vc := cstZ rv (Z.add_with_carry c x y) in - cstZ rv vc)) - ; (forall rvc s x y, - cstZZ rvc (Z.add_get_carry_full s x y) - = dlet2 rvc (Z.add_get_carry_full s x y)) - ; (forall rvc s c x y, - cstZZ rvc (Z.sub_with_get_borrow_full s c x y) - = dlet2 rvc (Z.sub_with_get_borrow_full s c x y)) - ; (forall rvc s x y, - cstZZ rvc (Z.sub_get_borrow_full s x y) - = dlet2 rvc (Z.sub_get_borrow_full s x y)) - ; (forall rvc s x y, - cstZZ rvc (Z.mul_split s x y) - = dlet2 rvc (Z.mul_split s x y)) - ]%Z%zrange - ; reify - [ (* [do_again], so that if one of the arguments is concrete, we automatically get the rewrite rule for [Z_cast] applying to it *) - do_again (forall r x y, cstZZ r (x, y) = (cstZ (fst r) x, cstZ (snd r) y)) - ] - ; reify - [(forall r1 r2 x, (r2 <= n r1)%zrange -> cstZ r1 (cstZ r2 x) = cstZ r2 x) - ]%Z%zrange - ]. + := reify arith_with_casts_rewrite_rulesT. Definition strip_literal_casts_rewrite_rules : rewrite_rulesT - := reify - [(forall rx x, x ∈ rx -> cstZ rx ('x) = 'x)]%Z%zrange. + := reify strip_literal_casts_rewrite_rulesT. Definition nbe_dtree' @@ -2959,343 +2492,10 @@ Module Compilers. Context (invert_low invert_high : Z (*log2wordmax*) -> Z -> option Z) (value_range flag_range : zrange). Definition fancy_rewrite_rules : rewrite_rulesT - := []. - - Local Notation pcst v := (#pattern.ident.Z_cast @ v)%pattern. - Local Notation pcst2 v := (#pattern.ident.Z_cast2 @ v)%pattern. - - Local Coercion ZRange.constant : Z >-> zrange. (* for ease of use with sanity-checking bounds *) - Local Notation bounds1_good f - := (fun (output x_bs : zrange) - => is_tighter_than_bool (f (ZRange.normalize x_bs)) (ZRange.normalize output) = true). - Local Notation bounds2_good f - := (fun (output x_bs y_bs : zrange) - => is_tighter_than_bool (f (ZRange.normalize x_bs) (ZRange.normalize y_bs)) (ZRange.normalize output) = true). - Local Notation range_in_bitwidth r s - := (is_tighter_than_bool (ZRange.normalize r) r[0~>s-1]%zrange = true). - Local Notation shiftl_good := (bounds2_good ZRange.shiftl). - Local Notation shiftr_good := (bounds2_good ZRange.shiftr). - Local Notation land_good := (bounds2_good ZRange.land). - Local Notation mul_good := (bounds2_good ZRange.mul). - Local Notation cc_m_good output s := (bounds1_good (ZRange.cc_m s) output). - Local Notation lit_good x rx := (is_bounded_by_bool x (ZRange.normalize rx)). + := reify fancy_rewrite_rulesT. Definition fancy_with_casts_rewrite_rules : rewrite_rulesT - := Eval cbv [Make.interp_rewrite_rules myapp myflatten] in - myflatten - [reify - [(* -(Z.add_get_carry_concrete 2^256) @@ (?x, ?y << 128) --> (add 128) @@ (x, y) -(Z.add_get_carry_concrete 2^256) @@ (?x << 128, ?y) --> (add 128) @@ (y, x) -(Z.add_get_carry_concrete 2^256) @@ (?x, ?y >> 128) --> (add (- 128)) @@ (x, y) -(Z.add_get_carry_concrete 2^256) @@ (?x >> 128, ?y) --> (add (- 128)) @@ (y, x) -(Z.add_get_carry_concrete 2^256) @@ (?x, ?y) --> (add 0) @@ (y, x) - *) - (forall r rs s rx x rshiftl rland ry y rmask mask roffset offset, - s = 2^Z.log2 s -> s ∈ rs -> offset ∈ roffset -> mask ∈ rmask -> shiftl_good rshiftl rland offset -> land_good rland ry mask -> range_in_bitwidth rshiftl s -> (mask = Z.ones (Z.log2 s - offset)) -> (0 <= offset <= Z.log2 s) - -> cstZZ r (Z.add_get_carry_full (cstZ rs ('s)) (cstZ rx x) (cstZ rshiftl ((cstZ rland (cstZ ry y &' cstZ rmask ('mask))) << cstZ roffset ('offset)))) - = cstZZ r (ident.interp (ident.fancy_add (Z.log2 s) (offset)) (cstZ rx x, cstZ ry y))) - ; (forall r rs s rx x rshiftl rland ry y rmask mask roffset offset, - (s = 2^Z.log2 s) -> (mask = Z.ones (Z.log2 s - offset)) -> (0 <= offset <= Z.log2 s) -> s ∈ rs -> mask ∈ rmask -> offset ∈ roffset -> shiftl_good rshiftl rland offset -> land_good rland ry mask -> range_in_bitwidth rshiftl s - -> cstZZ r (Z.add_get_carry_full (cstZ rs ('s)) (cstZ rx x) (cstZ rshiftl (cstZ rland (cstZ ry y &' cstZ rmask ('mask)) << cstZ roffset ('offset)))) - = cstZZ r (ident.interp (ident.fancy_add (Z.log2 s) offset) (cstZ rx x, cstZ ry y))) - - ; (forall r rs s rshiftl rland ry y rmask mask roffset offset rx x, - s ∈ rs -> mask ∈ rmask -> offset ∈ roffset -> (s = 2^Z.log2 s) -> shiftl_good rshiftl rland offset -> land_good rland ry mask -> range_in_bitwidth rshiftl s -> (mask = Z.ones (Z.log2 s - offset)) -> (0 <= offset <= Z.log2 s) - -> cstZZ r (Z.add_get_carry_full (cstZ rs ('s)) (cstZ rshiftl (Z.shiftl (cstZ rland (Z.land (cstZ ry y) (cstZ rmask ('mask)))) (cstZ roffset ('offset)))) (cstZ rx x)) - = cstZZ r (ident.interp (ident.fancy_add (Z.log2 s) offset) (cstZ rx x, cstZ ry y))) - - ; (forall r rs s rx x rshiftr ry y roffset offset, - s ∈ rs -> offset ∈ roffset -> (s = 2^Z.log2 s) -> shiftr_good rshiftr ry offset -> range_in_bitwidth rshiftr s - -> cstZZ r (Z.add_get_carry_full (cstZ rs ('s)) (cstZ rx x) (cstZ rshiftr (Z.shiftr (cstZ ry y) (cstZ roffset ('offset))))) - = cstZZ r (ident.interp (ident.fancy_add (Z.log2 s) (-offset)) (cstZ rx x, cstZ ry y))) - - ; (forall r rs s rshiftr ry y roffset offset rx x, - s ∈ rs -> offset ∈ roffset -> (s = 2^Z.log2 s) -> shiftr_good rshiftr ry offset -> range_in_bitwidth rshiftr s - -> cstZZ r (Z.add_get_carry_full (cstZ rs ('s)) (cstZ rshiftr (Z.shiftr (cstZ ry y) (cstZ roffset ('offset)))) (cstZ rx x)) - = cstZZ r (ident.interp (ident.fancy_add (Z.log2 s) (-offset)) (cstZ rx x, cstZ ry y))) - - ; (forall r rs s rx x ry y, - s ∈ rs -> (s = 2^Z.log2 s) -> range_in_bitwidth ry s - -> cstZZ r (Z.add_get_carry_full (cstZ rs ('s)) (cstZ rx x) (cstZ ry y)) - = cstZZ r (ident.interp (ident.fancy_add (Z.log2 s) 0) (cstZ rx x, cstZ ry y))) - - (* -(Z.add_with_get_carry_concrete 2^256) @@ (?c, ?x, ?y << 128) --> (addc 128) @@ (c, x, y) -(Z.add_with_get_carry_concrete 2^256) @@ (?c, ?x << 128, ?y) --> (addc 128) @@ (c, y, x) -(Z.add_with_get_carry_concrete 2^256) @@ (?c, ?x, ?y >> 128) --> (addc (- 128)) @@ (c, x, y) -(Z.add_with_get_carry_concrete 2^256) @@ (?c, ?x >> 128, ?y) --> (addc (- 128)) @@ (c, y, x) -(Z.add_with_get_carry_concrete 2^256) @@ (?c, ?x, ?y) --> (addc 0) @@ (c, y, x) - *) - ; (forall r rs s rc c rx x rshiftl rland ry y rmask mask roffset offset, - s ∈ rs -> mask ∈ rmask -> offset ∈ roffset -> (s = 2^Z.log2 s) -> shiftl_good rshiftl rland offset -> land_good rland ry mask -> range_in_bitwidth rshiftl s -> (mask = Z.ones (Z.log2 s - offset)) -> (0 <= offset <= Z.log2 s) - -> cstZZ r (Z.add_with_get_carry_full (cstZ rs ('s)) (cstZ rc c) (cstZ rx x) (cstZ rshiftl (Z.shiftl (cstZ rland (Z.land (cstZ ry y) (cstZ rmask ('mask)))) (cstZ roffset ('offset))))) - = cstZZ r (ident.interp (ident.fancy_addc (Z.log2 s) offset) (cstZ rc c, cstZ rx x, cstZ ry y))) - - ; (forall r rs s rc c rshiftl rland ry y rmask mask roffset offset rx x, - s ∈ rs -> mask ∈ rmask -> offset ∈ roffset -> (s = 2^Z.log2 s) -> shiftl_good rshiftl rland offset -> range_in_bitwidth rshiftl s -> land_good rland ry mask -> (mask = Z.ones (Z.log2 s - offset)) -> (0 <= offset <= Z.log2 s) - -> cstZZ r (Z.add_with_get_carry_full (cstZ rs ('s)) (cstZ rc c) (cstZ rshiftl (Z.shiftl (cstZ rland (Z.land (cstZ ry y) (cstZ rmask ('mask)))) (cstZ roffset ('offset)))) (cstZ rx x)) - = cstZZ r (ident.interp (ident.fancy_addc (Z.log2 s) offset) (cstZ rc c, cstZ rx x, cstZ ry y))) - - ; (forall r rs s rc c rx x rshiftr ry y roffset offset, - s ∈ rs -> offset ∈ roffset -> (s = 2^Z.log2 s) -> shiftr_good rshiftr ry offset -> range_in_bitwidth rshiftr s - -> cstZZ r (Z.add_with_get_carry_full (cstZ rs ('s)) (cstZ rc c) (cstZ rx x) (cstZ rshiftr (Z.shiftr (cstZ ry y) (cstZ roffset ('offset))))) - = cstZZ r (ident.interp (ident.fancy_addc (Z.log2 s) (-offset)) (cstZ rc c, cstZ rx x, cstZ ry y))) - - ; (forall r rs s rc c rshiftr ry y roffset offset rx x, - s ∈ rs -> offset ∈ roffset -> (s = 2^Z.log2 s) -> shiftr_good rshiftr ry offset -> range_in_bitwidth rshiftr s - -> cstZZ r (Z.add_with_get_carry_full (cstZ rs ('s)) (cstZ rc c) (cstZ rshiftr (Z.shiftr (cstZ ry y) (cstZ roffset ('offset)))) (cstZ rx x)) - = cstZZ r (ident.interp (ident.fancy_addc (Z.log2 s) (-offset)) (cstZ rc c, cstZ rx x, cstZ ry y))) - - ; (forall r rs s rc c rx x ry y, - s ∈ rs -> (s = 2^Z.log2 s) -> range_in_bitwidth ry s - -> cstZZ r (Z.add_with_get_carry_full (cstZ rs ('s)) (cstZ rc c) (cstZ rx x) (cstZ ry y)) - = cstZZ r (ident.interp (ident.fancy_addc (Z.log2 s) 0) (cstZ rc c, cstZ rx x, cstZ ry y))) - - (* -(Z.sub_get_borrow_concrete 2^256) @@ (?x, ?y << 128) --> (sub 128) @@ (x, y) -(Z.sub_get_borrow_concrete 2^256) @@ (?x, ?y >> 128) --> (sub (- 128)) @@ (x, y) -(Z.sub_get_borrow_concrete 2^256) @@ (?x, ?y) --> (sub 0) @@ (y, x) - *) - - ; (forall r rs s rx x rshiftl rland ry y rmask mask roffset offset, - s ∈ rs -> mask ∈ rmask -> offset ∈ roffset -> (s = 2^Z.log2 s) -> shiftl_good rshiftl rland offset -> range_in_bitwidth rshiftl s -> land_good rland ry mask -> (mask = Z.ones (Z.log2 s - offset)) -> (0 <= offset <= Z.log2 s) - -> cstZZ r (Z.sub_get_borrow_full (cstZ rs ('s)) (cstZ rx x) (cstZ rshiftl (Z.shiftl (cstZ rland (Z.land (cstZ ry y) (cstZ rmask ('mask)))) (cstZ roffset ('offset))))) - = cstZZ r (ident.interp (ident.fancy_sub (Z.log2 s) offset) (cstZ rx x, cstZ ry y))) - - ; (forall r rs s rx x rshiftr ry y roffset offset, - s ∈ rs -> offset ∈ roffset -> (s = 2^Z.log2 s) -> shiftr_good rshiftr ry offset -> range_in_bitwidth rshiftr s - -> cstZZ r (Z.sub_get_borrow_full (cstZ rs ('s)) (cstZ rx x) (cstZ rshiftr (Z.shiftr (cstZ ry y) (cstZ roffset ('offset))))) - = cstZZ r (ident.interp (ident.fancy_sub (Z.log2 s) (-offset)) (cstZ rx x, cstZ ry y))) - - ; (forall r rs s rx x ry y, - s ∈ rs -> (s = 2^Z.log2 s) -> range_in_bitwidth ry s - -> cstZZ r (Z.sub_get_borrow_full (cstZ rs ('s)) (cstZ rx x) (cstZ ry y)) - = cstZZ r (ident.interp (ident.fancy_sub (Z.log2 s) 0) (cstZ rx x, cstZ ry y))) - - (* -(Z.sub_with_get_borrow_concrete 2^256) @@ (?c, ?x, ?y << 128) --> (subb 128) @@ (c, x, y) -(Z.sub_with_get_borrow_concrete 2^256) @@ (?c, ?x, ?y >> 128) --> (subb (- 128)) @@ (c, x, y) -(Z.sub_with_get_borrow_concrete 2^256) @@ (?c, ?x, ?y) --> (subb 0) @@ (c, y, x) - *) - - ; (forall r rs s rb b rx x rshiftl rland ry y rmask mask roffset offset, - s ∈ rs -> mask ∈ rmask -> offset ∈ roffset -> (s = 2^Z.log2 s) -> shiftl_good rshiftl rland offset -> range_in_bitwidth rshiftl s -> land_good rland ry mask -> (mask = Z.ones (Z.log2 s - offset)) -> (0 <= offset <= Z.log2 s) - -> cstZZ r (Z.sub_with_get_borrow_full (cstZ rs ('s)) (cstZ rb b) (cstZ rx x) (cstZ rshiftl (Z.shiftl (cstZ rland (Z.land (cstZ ry y) (cstZ rmask ('mask)))) (cstZ roffset ('offset))))) - = cstZZ r (ident.interp (ident.fancy_subb (Z.log2 s) offset) (cstZ rb b, cstZ rx x, cstZ ry y))) - - ; (forall r rs s rb b rx x rshiftr ry y roffset offset, - s ∈ rs -> offset ∈ roffset -> (s = 2^Z.log2 s) -> shiftr_good rshiftr ry offset -> range_in_bitwidth rshiftr s - -> cstZZ r (Z.sub_with_get_borrow_full (cstZ rs ('s)) (cstZ rb b) (cstZ rx x) (cstZ rshiftr (Z.shiftr (cstZ ry y) (cstZ roffset ('offset))))) - = cstZZ r (ident.interp (ident.fancy_subb (Z.log2 s) (-offset)) (cstZ rb b, cstZ rx x, cstZ ry y))) - - ; (forall r rs s rb b rx x ry y, - s ∈ rs -> (s = 2^Z.log2 s) -> range_in_bitwidth ry s - -> cstZZ r (Z.sub_with_get_borrow_full (cstZ rs ('s)) (cstZ rb b) (cstZ rx x) (cstZ ry y)) - = cstZZ r (ident.interp (ident.fancy_subb (Z.log2 s) 0) (cstZ rb b, cstZ rx x, cstZ ry y))) - - (*(Z.rshi_concrete 2^256 ?n) @@ (?c, ?x, ?y) --> (rshi n) @@ (x, y)*) - - ; (forall r rs s rx x ry y rn n, - s ∈ rs -> n ∈ rn -> (s = 2^Z.log2 s) - -> cstZ r (Z.rshi (cstZ rs ('s)) (cstZ rx x) (cstZ ry y) (cstZ rn ('n))) - = cstZ r (ident.interp (ident.fancy_rshi (Z.log2 s) n) (cstZ rx x, cstZ ry y))) - - (* -Z.zselect @@ (Z.cc_m_concrete 2^256 ?c, ?x, ?y) --> selm @@ (c, x, y) -Z.zselect @@ (?c &' 1, ?x, ?y) --> sell @@ (c, x, y) -Z.zselect @@ (?c, ?x, ?y) --> selc @@ (c, x, y) - *) - ; (forall r rccm rs s rc c rx x ry y, - s ∈ rs -> (s = 2^Z.log2 s) -> cc_m_good rccm s rc - -> cstZ r (Z.zselect (cstZ rccm (Z.cc_m (cstZ rs ('s)) (cstZ rc c))) (cstZ rx x) (cstZ ry y)) - = cstZ r (ident.interp (ident.fancy_selm (Z.log2 s)) (cstZ rc c, cstZ rx x, cstZ ry y))) - - ; (forall r rland r1 rc c rx x ry y, - 1 ∈ r1 -> land_good rland 1 rc - -> cstZ r (Z.zselect (cstZ rland (cstZ r1 1 &' cstZ rc c)) (cstZ rx x) (cstZ ry y)) - = cstZ r (ident.interp ident.fancy_sell (cstZ rc c, cstZ rx x, cstZ ry y))) - - ; (forall r rland rc c r1 rx x ry y, - 1 ∈ r1 -> land_good rland rc 1 - -> cstZ r (Z.zselect (cstZ rland (cstZ rc c &' cstZ r1 1)) (cstZ rx x) (cstZ ry y)) - = cstZ r (ident.interp ident.fancy_sell (cstZ rc c, cstZ rx x, cstZ ry y))) - - ; (forall r c x y, - cstZ r (Z.zselect c x y) - = cstZ r (ident.interp ident.fancy_selc (c, x, y))) - - (*Z.add_modulo @@ (?x, ?y, ?m) --> addm @@ (x, y, m)*) - ; (forall x y m, - Z.add_modulo x y m - = ident.interp ident.fancy_addm (x, y, m)) - - (* -Z.mul @@ (?x &' (2^128-1), ?y &' (2^128-1)) --> mulll @@ (x, y) -Z.mul @@ (?x &' (2^128-1), ?y >> 128) --> mullh @@ (x, y) -Z.mul @@ (?x >> 128, ?y &' (2^128-1)) --> mulhl @@ (x, y) -Z.mul @@ (?x >> 128, ?y >> 128) --> mulhh @@ (x, y) - *) - (* literal on left *) - ; (forall r rx x rland ry y rmask mask, - plet s := (2*Z.log2_up mask)%Z in - plet xo := invert_low s x in - plet xv := match xo with Some x => x | None => 0 end in - xo <> None -> x ∈ rx -> mask ∈ rmask -> (mask = 2^(s/2)-1) -> land_good rland ry mask - -> cstZ r (cstZ rx ('x) * cstZ rland (Z.land (cstZ ry y) (cstZ rmask ('mask)))) - = cstZ r (ident.interp (ident.fancy_mulll s) ('xv, cstZ ry y))) - - ; (forall r rx x rland rmask mask ry y, - plet s := (2*Z.log2_up mask)%Z in - plet xo := invert_low s x in - plet xv := match xo with Some x => x | None => 0 end in - xo <> None -> x ∈ rx -> mask ∈ rmask -> (mask = 2^(s/2)-1) -> land_good rland mask ry - -> cstZ r (cstZ rx ('x) * cstZ rland (Z.land (cstZ rmask ('mask)) (cstZ ry y))) - = cstZ r (ident.interp (ident.fancy_mulll s) ('xv, cstZ ry y))) - - ; (forall r rx x rshiftr ry y roffset offset, - plet s := (2*offset)%Z in - plet xo := invert_low s x in - plet xv := match xo with Some x => x | None => 0 end in - xo <> None -> x ∈ rx -> offset ∈ roffset -> shiftr_good rshiftr ry offset - -> cstZ r (cstZ rx ('x) * cstZ rshiftr (Z.shiftr (cstZ ry y) (cstZ roffset ('offset)))) - = cstZ r (ident.interp (ident.fancy_mullh s) ('xv, cstZ ry y))) - - ; (forall r rx x rland rmask mask ry y, - plet s := (2*Z.log2_up mask)%Z in - plet xo := invert_high s x in - plet xv := match xo with Some x => x | None => 0 end in - xo <> None -> x ∈ rx -> mask ∈ rmask -> (mask = 2^(s/2)-1) -> land_good rland mask ry - -> cstZ r (cstZ rx ('x) * cstZ rland (Z.land (cstZ rmask ('mask)) (cstZ ry y))) - = cstZ r (ident.interp (ident.fancy_mulhl s) ('xv, cstZ ry y))) - - ; (forall r rx x rland ry y rmask mask, - plet s := (2*Z.log2_up mask)%Z in - plet xo := invert_high s x in - plet xv := match xo with Some x => x | None => 0 end in - xo <> None -> x ∈ rx -> mask ∈ rmask -> (mask = 2^(s/2)-1) -> land_good rland ry mask - -> cstZ r (cstZ rx ('x) * cstZ rland (Z.land (cstZ ry y) (cstZ rmask ('mask)))) - = cstZ r (ident.interp (ident.fancy_mulhl s) ('xv, cstZ ry y))) - - ; (forall r rx x rshiftr ry y roffset offset, - plet s := (2*offset)%Z in - plet xo := invert_high s x in - plet xv := match xo with Some x => x | None => 0 end in - xo <> None -> x ∈ rx -> offset ∈ roffset -> shiftr_good rshiftr ry offset - -> cstZ r (cstZ rx ('x) * cstZ rshiftr (Z.shiftr (cstZ ry y) (cstZ roffset ('offset)))) - = cstZ r (ident.interp (ident.fancy_mulhh s) ('xv, cstZ ry y))) - - (* literal on right *) - ; (forall r rland rmask mask rx x ry y, - plet s := (2*Z.log2_up mask)%Z in - plet yo := invert_low s y in - plet yv := match yo with Some y => y | None => 0 end in - yo <> None -> y ∈ ry -> mask ∈ rmask -> (mask = 2^(s/2)-1) -> land_good rland mask rx - -> cstZ r (cstZ rland (Z.land (cstZ rmask ('mask)) (cstZ rx x)) * cstZ ry ('y)) - = cstZ r (ident.interp (ident.fancy_mulll s) (cstZ rx x, 'yv))) - - ; (forall r rland rx x rmask mask ry y, - plet s := (2*Z.log2_up mask)%Z in - plet yo := invert_low s y in - plet yv := match yo with Some y => y | None => 0 end in - yo <> None -> y ∈ ry -> mask ∈ rmask -> (mask = 2^(s/2)-1) -> land_good rland rx mask - -> cstZ r (cstZ rland (Z.land (cstZ rx x) (cstZ rmask ('mask))) * cstZ ry ('y)) - = cstZ r (ident.interp (ident.fancy_mulll s) (cstZ rx x, 'yv))) - - ; (forall r rland rmask mask rx x ry y, - plet s := (2*Z.log2_up mask)%Z in - plet yo := invert_high s y in - plet yv := match yo with Some y => y | None => 0 end in - yo <> None -> y ∈ ry -> mask ∈ rmask -> (mask = 2^(s/2)-1) -> land_good rland mask rx - -> cstZ r (cstZ rland (Z.land (cstZ rmask ('mask)) (cstZ rx x)) * cstZ ry ('y)) - = cstZ r (ident.interp (ident.fancy_mullh s) (cstZ rx x, 'yv))) - - ; (forall r rland rx x rmask mask ry y, - plet s := (2*Z.log2_up mask)%Z in - plet yo := invert_high s y in - plet yv := match yo with Some y => y | None => 0 end in - yo <> None -> y ∈ ry -> mask ∈ rmask -> (mask = 2^(s/2)-1) -> land_good rland rx mask - -> cstZ r (cstZ rland (Z.land (cstZ rx x) (cstZ rmask ('mask))) * cstZ ry ('y)) - = cstZ r (ident.interp (ident.fancy_mullh s) (cstZ rx x, 'yv))) - - ; (forall r rshiftr rx x roffset offset ry y, - plet s := (2*offset)%Z in - plet yo := invert_low s y in - plet yv := match yo with Some y => y | None => 0 end in - yo <> None -> y ∈ ry -> offset ∈ roffset -> shiftr_good rshiftr rx offset - -> cstZ r (cstZ rshiftr (Z.shiftr (cstZ rx x) (cstZ roffset ('offset))) * cstZ ry ('y)) - = cstZ r (ident.interp (ident.fancy_mulhl s) (cstZ rx x, 'yv))) - - ; (forall r rshiftr rx x roffset offset ry y, - plet s := (2*offset)%Z in - plet yo := invert_high s y in - plet yv := match yo with Some y => y | None => 0 end in - yo <> None -> y ∈ ry -> offset ∈ roffset -> shiftr_good rshiftr rx offset - -> cstZ r (cstZ rshiftr (Z.shiftr (cstZ rx x) (cstZ roffset ('offset))) * cstZ ry ('y)) - = cstZ r (ident.interp (ident.fancy_mulhh s) (cstZ rx x, 'yv))) - - (* no literal *) - ; (forall r rland1 rmask1 mask1 rx x rland2 rmask2 mask2 ry y, - plet s := (2*Z.log2_up mask1)%Z in - mask1 ∈ rmask1 -> mask2 ∈ rmask2 -> (mask1 = 2^(s/2)-1) -> (mask2 = 2^(s/2)-1) -> land_good rland1 mask1 rx -> land_good rland2 mask2 ry - -> cstZ r (cstZ rland1 (Z.land (cstZ rmask1 ('mask1)) (cstZ rx x)) * cstZ rland2 (Z.land (cstZ rmask2 ('mask2)) (cstZ ry y))) - = cstZ r (ident.interp (ident.fancy_mulll s) (cstZ rx x, cstZ ry y))) - - ; (forall r rland1 rx x rmask1 mask1 rland2 rmask2 mask2 ry y, - plet s := (2*Z.log2_up mask1)%Z in - mask1 ∈ rmask1 -> mask2 ∈ rmask2 -> (mask1 = 2^(s/2)-1) -> (mask2 = 2^(s/2)-1) -> land_good rland1 rx mask1 -> land_good rland2 mask2 ry - -> cstZ r (cstZ rland1 (Z.land (cstZ rx x) (cstZ rmask1 ('mask1))) * cstZ rland2 (Z.land (cstZ rmask2 ('mask2)) (cstZ ry y))) - = cstZ r (ident.interp (ident.fancy_mulll s) (cstZ rx x, cstZ ry y))) - - ; (forall r rland1 rmask1 mask1 rx x rland2 ry y rmask2 mask2, - plet s := (2*Z.log2_up mask1)%Z in - mask1 ∈ rmask1 -> mask2 ∈ rmask2 -> (mask1 = 2^(s/2)-1) -> (mask2 = 2^(s/2)-1) -> land_good rland1 mask1 rx -> land_good rland2 ry mask2 - -> cstZ r (cstZ rland1 (Z.land (cstZ rmask1 ('mask1)) (cstZ rx x)) * cstZ rland2 (Z.land (cstZ ry y) (cstZ rmask2 ('mask2)))) - = cstZ r (ident.interp (ident.fancy_mulll s) (cstZ rx x, cstZ ry y))) - - ; (forall r rland1 rx x rmask1 mask1 rland2 ry y rmask2 mask2, - plet s := (2*Z.log2_up mask1)%Z in - mask1 ∈ rmask1 -> mask2 ∈ rmask2 -> (mask1 = 2^(s/2)-1) -> (mask2 = 2^(s/2)-1) -> land_good rland1 rx mask1 -> land_good rland2 ry mask2 - -> cstZ r (cstZ rland1 (Z.land (cstZ rx x) (cstZ rmask1 ('mask1))) * cstZ rland2 (Z.land (cstZ ry y) (cstZ rmask2 ('mask2)))) - = cstZ r (ident.interp (ident.fancy_mulll s) (cstZ rx x, cstZ ry y))) - - ; (forall r rland1 rmask mask rx x rshiftr2 ry y roffset offset, - plet s := (2*offset)%Z in - mask ∈ rmask -> offset ∈ roffset -> (mask = 2^(s/2)-1) -> land_good rland1 mask rx -> shiftr_good rshiftr2 ry offset - -> cstZ r (cstZ rland1 (Z.land (cstZ rmask ('mask)) (cstZ rx x)) * cstZ rshiftr2 (Z.shiftr (cstZ ry y) (cstZ roffset ('offset)))) - = cstZ r (ident.interp (ident.fancy_mullh s) (cstZ rx x, cstZ ry y))) - - ; (forall r rland1 rx x rmask mask rshiftr2 ry y roffset offset, - plet s := (2*offset)%Z in - mask ∈ rmask -> offset ∈ roffset -> (mask = 2^(s/2)-1) -> land_good rland1 rx mask -> shiftr_good rshiftr2 ry offset - -> cstZ r (cstZ rland1 (Z.land (cstZ rx x) (cstZ rmask ('mask))) * cstZ rshiftr2 (Z.shiftr (cstZ ry y) (cstZ roffset ('offset)))) - = cstZ r (ident.interp (ident.fancy_mullh s) (cstZ rx x, cstZ ry y))) - - ; (forall r rshiftr1 rx x roffset offset rland2 rmask mask ry y, - plet s := (2*offset)%Z in - mask ∈ rmask -> offset ∈ roffset -> (mask = 2^(s/2)-1) -> shiftr_good rshiftr1 rx offset -> land_good rland2 mask ry - -> cstZ r (cstZ rshiftr1 (Z.shiftr (cstZ rx x) (cstZ roffset ('offset))) * cstZ rland2 (Z.land (cstZ rmask ('mask)) (cstZ ry y))) - = cstZ r (ident.interp (ident.fancy_mulhl s) (cstZ rx x, cstZ ry y))) - - ; (forall r rshiftr1 rx x roffset offset rland2 ry y rmask mask, - plet s := (2*offset)%Z in - mask ∈ rmask -> offset ∈ roffset -> (mask = 2^(s/2)-1) -> shiftr_good rshiftr1 rx offset -> land_good rland2 ry mask - -> cstZ r (cstZ rshiftr1 (Z.shiftr (cstZ rx x) (cstZ roffset ('offset))) * cstZ rland2 (Z.land (cstZ ry y) (cstZ rmask ('mask)))) - = cstZ r (ident.interp (ident.fancy_mulhl s) (cstZ rx x, cstZ ry y))) - - ; (forall r rshiftr1 rx x roffset1 offset1 rshiftr2 ry y roffset2 offset2, - plet s := (2*offset1)%Z in - offset1 ∈ roffset1 -> offset2 ∈ roffset2 -> (offset1 = offset2) -> shiftr_good rshiftr1 rx offset1 -> shiftr_good rshiftr2 ry offset2 - -> cstZ r (cstZ rshiftr1 (Z.shiftr (cstZ rx x) (cstZ roffset1 ('offset1))) * cstZ rshiftr2 (Z.shiftr (cstZ ry y) (cstZ roffset2 ('offset2)))) - = cstZ r (ident.interp (ident.fancy_mulhh s) (cstZ rx x, cstZ ry y))) - - (** Dummy rule to make sure we use the two value ranges; this can be removed *) - ; (forall rx x, - ((is_tighter_than_bool rx value_range = true) - \/ (is_tighter_than_bool rx flag_range = true)) - -> cstZ rx x = cstZ rx x) - ]%Z%zrange - ]. + := reify (fancy_with_casts_rewrite_rulesT invert_low invert_high value_range flag_range). Definition fancy_dtree' := Eval compute in @compile_rewrites ident var pattern.ident (@pattern.ident.arg_types) pattern.Raw.ident (@pattern.ident.strip_types) pattern.Raw.ident.ident_beq 100 fancy_rewrite_rules. diff --git a/src/RewriterRules.v b/src/RewriterRules.v new file mode 100644 index 000000000..4ded9846f --- /dev/null +++ b/src/RewriterRules.v @@ -0,0 +1,788 @@ +Require Import Coq.ZArith.ZArith. +Require Import Crypto.Util.ListUtil Coq.Lists.List Crypto.Util.ListUtil.FoldBool. +Require Import Crypto.Util.ZRange. +Require Import Crypto.Util.ZRange.Operations. +Require Import Crypto.Util.ZUtil.Definitions. +Require Import Crypto.Util.ZUtil.Notations. +Require Import Crypto.Util.ZRange. +Require Import Crypto.Util.ZRange.Operations. +Require Import Crypto.Language. +Require Import Crypto.Util.LetIn. +Require Import Crypto.Util.Notations. +Import ListNotations. Local Open Scope bool_scope. Local Open Scope Z_scope. + +Local Definition mymap {A B} := Eval cbv in @List.map A B. +Local Definition myapp {A} := Eval cbv in @List.app A. +Local Definition myflatten {A} := Eval cbv in List.fold_right myapp (@nil A). +Local Notation dont_do_again := (pair false) (only parsing). +Local Notation do_again := (pair true) (only parsing). + +Import Language.Compilers. + +Local Notation "' x" := (ident.literal x). +Local Notation cstZ := (ident.cast ident.cast_outside_of_range). +Local Notation cstZZ := (ident.cast2 ident.cast_outside_of_range). +Local Notation "'plet' x := y 'in' z" + := (match y return _ with x => z end). + +Local Notation dlet2_opp2 rvc e + := (plet rvc' := (fst rvc, -snd rvc)%zrange in + plet cst' := cstZZ rvc' in + plet cst1 := cstZ (fst rvc%zrange%zrange) in + plet cst2 := cstZ (snd rvc%zrange%zrange) in + plet cst2' := cstZ (-snd rvc%zrange%zrange) in + (dlet vc := cst' e in + (cst1 (fst (cst' vc)), cst2 (-(cst2' (snd (cst' vc))))))). + +Local Notation dlet2 rvc e + := (dlet vc := cstZZ rvc e in + (cstZ (fst rvc) (fst (cstZZ rvc vc)), + cstZ (snd rvc) (snd (cstZZ rvc vc)))). + + +Local Notation "x '\in' y" := (is_bounded_by_bool x (ZRange.normalize y) = true) : zrange_scope. +Local Notation "x ∈ y" := (is_bounded_by_bool x (ZRange.normalize y) = true) : zrange_scope. +Local Notation "x <= y" := (is_tighter_than_bool (ZRange.normalize x) y = true) : zrange_scope. +Local Notation litZZ x := (ident.literal (fst x), ident.literal (snd x)) (only parsing). +Local Notation n r := (ZRange.normalize r) (only parsing). + +(* N.B. [ident.eagerly] does not play well with [do_again] *) +Definition nbe_rewrite_rulesT : list (bool * Prop) + := Eval cbv [myapp mymap myflatten] in + myflatten + [mymap + dont_do_again + [(forall A B x y, @fst A B (x, y) = x) + ; (forall A B x y, @snd A B (x, y) = y) + ; (forall P t f, @ident.Thunked.bool_rect P t f true = t tt) + ; (forall P t f, @ident.Thunked.bool_rect P t f false = f tt) + ; (forall A B C f x y, @prod_rect A B (fun _ => C) f (x, y) = f x y) + + ; (forall A x n, + @List.repeat A x ('n) + = ident.eagerly (@nat_rect) _ nil (fun k repeat_k => x :: repeat_k) ('n)) + ; (forall A xs ys, + xs ++ ys + = ident.eagerly (@list_rect) A _ ys (fun x xs app_xs_ys => x :: app_xs_ys) xs) + ; (forall A B f a ls, + @fold_right A B f a ls + = (ident.eagerly (@list_rect) _ _) + a + (fun x xs fold_right_xs => f x fold_right_xs) + ls) + ; (forall A P N C ls, + @ident.Thunked.list_rect A P N C ls + = ident.eagerly (@ident.Thunked.list_rect) A P N C ls) + ; (forall A P Q N C ls v, + @list_rect A (fun _ => P -> Q) N C ls v + = ident.eagerly (@list_rect) A (fun _ => P -> Q) N C ls v) + ; (forall A P N C, @ident.Thunked.list_case A P N C nil = N tt) + ; (forall A P N C x xs, @ident.Thunked.list_case A P N C (x :: xs) = C x xs) + ; (forall A B f ls, + @List.map A B f ls + = (ident.eagerly (@list_rect) _ _) + nil + (fun x xs map_f_xs => f x :: map_f_xs) + ls) + ; (forall P O_case S_case n, + @ident.Thunked.nat_rect P O_case S_case ('n) + = (ident.eagerly (@ident.Thunked.nat_rect) _) + O_case + S_case + ('n)) + ; (forall P Q O_case S_case n v, + @nat_rect (fun _ => P -> Q) O_case S_case ('n) v + = (ident.eagerly (@nat_rect) _) + O_case + S_case + ('n) + v) + ; (forall A default ls n, + @List.nth_default A default ls ('n) + = ident.eagerly (@List.nth_default) _ default ls ('n)) + ] + ; mymap + do_again + [(forall A B xs ys, + @List.combine A B xs ys + = (list_rect _) + (fun _ => nil) + (fun x xs combine_xs ys + => match ys with + | nil => nil + | y :: ys => (x, y) :: combine_xs ys + end) + xs + ys) + ; (forall A n ls, + @List.firstn A ('n) ls + = (nat_rect _) + (fun _ => nil) + (fun n' firstn_n' ls + => match ls with + | nil => nil + | cons x xs => x :: firstn_n' xs + end) + ('n) + ls) + ; (forall A n ls, + @List.skipn A ('n) ls + = (nat_rect _) + (fun ls => ls) + (fun n' skipn_n' ls + => match ls with + | nil => nil + | cons x xs => skipn_n' xs + end) + ('n) + ls) + ; (forall A xs, + @List.length A xs + = (list_rect _) + 0%nat + (fun _ xs length_xs => S length_xs) + xs) + ; (forall A xs, + @List.rev A xs + = (list_rect _) + nil + (fun x xs rev_xs => rev_xs ++ [x]) + xs) + ; (forall A B f xs, + @List.flat_map A B f xs + = (list_rect _) + nil + (fun x _ flat_map_tl => f x ++ flat_map_tl) + xs) + ; (forall A f xs, + @List.partition A f xs + = (list_rect _) + ([], []) + (fun x tl partition_tl + => let '(g, d) := partition_tl in + if f x then (x :: g, d) else (g, x :: d)) + xs) + ; (forall A n f xs, + @update_nth A ('n) f xs + = (nat_rect _) + (fun xs => match xs with + | nil => nil + | x' :: xs' => f x' :: xs' + end) + (fun n' update_nth_n' xs + => match xs with + | nil => nil + | x' :: xs' => x' :: update_nth_n' xs' + end) + ('n) + xs) + ] + ]. + +Definition arith_rewrite_rulesT (max_const_val : Z) : list (bool * Prop) + := Eval cbv [myapp mymap myflatten] in + myflatten + [mymap + dont_do_again + [(forall A B x y, @fst A B (x, y) = x) + ; (forall A B x y, @snd A B (x, y) = y) + ; (forall v, 0 + v = v) + ; (forall v, v + 0 = v) + ; (forall x y, (-x) + (-y) = -(x + y)) + ; (forall x y, (-x) + y = y - x) + ; (forall x y, x + (-y) = x - y) + + ; (forall v, 0 - (-v) = v) + ; (forall v, 0 - v = -v) + ; (forall v, v - 0 = v) + ; (forall x y, (-x) - (-y) = y - x) + ; (forall x y, (-x) - y = -(x + y)) + ; (forall x y, x - (-y) = x + y) + + ; (forall v, 0 * v = 0) + ; (forall v, v * 0 = 0) + ; (forall v, 1 * v = v) + ; (forall v, v * 1 = v) + ; (forall v, (-1) * (-v) = v) + ; (forall v, (-v) * (-1) = v) + ; (forall v, (-1) * v = -v) + ; (forall v, v * (-1) = -v) + ; (forall x y, (-x) * (-y) = x * y) + ; (forall x y, (-x) * y = -(x * y)) + ; (forall x y, x * (-y) = -(x * y)) + + ; (forall x, x &' 0 = 0) + + ; (forall x, x / 1 = x) + ; (forall x, x mod 1 = 0) + + ; (forall v, -(-v) = v) + + ; (forall z v, z > 0 -> 'z + (-v) = 'z - v) + ; (forall z v, z > 0 -> (-v) + 'z = 'z - v) + ; (forall z v, z < 0 -> 'z + (-v) = -('(-z) + v)) + ; (forall z v, z < 0 -> (-v) + 'z = -(v + '(-z))) + + ; (forall z v, z > 0 -> 'z - (-v) = 'z + v) + ; (forall z v, z < 0 -> 'z - (-v) = v - '(-z)) + ; (forall z v, z < 0 -> 'z - v = -('(-z) + v)) + ; (forall z v, z > 0 -> (-v) - 'z = -(v + 'z)) + ; (forall z v, z < 0 -> (-v) - 'z = '(-z) - v) + ; (forall z v, z < 0 -> v - 'z = v + '(-z)) + + ; (forall x y, 'x * 'y = '(x*y)) + ; (forall z v, z < 0 -> 'z * v = -('(-z) * v)) + ; (forall z v, z < 0 -> v * 'z = -(v * '(-z))) + + ; (forall x y, y = 2^Z.log2 y -> y <> 2 -> x * 'y = x << '(Z.log2 y)) + ; (forall x y, y = 2^Z.log2 y -> y <> 2 -> 'y * x = x << '(Z.log2 y)) + + ; (forall x y, y = 2^Z.log2 y -> x / 'y = x >> '(Z.log2 y)) + ; (forall x y, y = 2^Z.log2 y -> x mod 'y = x &' '(y-1)) + + (* We reassociate some multiplication of small constants *) + ; (forall c1 c2 x y, + Z.abs c1 <= Z.abs max_const_val + -> Z.abs c2 <= Z.abs max_const_val + -> 'c1 * ('c2 * (x * y)) = (x * (y * ('c1 * 'c2)))) + ; (forall c1 c2 x y, + Z.abs c1 <= Z.abs max_const_val + -> Z.abs c2 <= Z.abs max_const_val + -> 'c1 * (x * (y * 'c2)) = (x * (y * ('c1 * 'c2)))) + ; (forall c x y, + Z.abs c <= Z.abs max_const_val + -> 'c * (x * y) = x * (y * 'c)) + ; (forall c x, + Z.abs c <= Z.abs max_const_val + -> 'c * x = x * 'c) + + (* transform +- to + *) + ; (forall s y x, + Z.add_get_carry_full s x (- y) + = dlet vb := Z.sub_get_borrow_full s x y in (fst vb, - snd vb)) + ; (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, + 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 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)) + ] + ; mymap + do_again + [ (* [do_again], so that if one of the arguments is concrete, we automatically get the rewrite rule for [Z_cast] applying to it *) + (forall r x y, cstZZ r (x, y) = (cstZ (fst r) x, cstZ (snd r) y)) + ] + ]. + +Definition arith_with_casts_rewrite_rulesT : list (bool * Prop) + := Eval cbv [myapp mymap myflatten] in + myflatten + [mymap + dont_do_again + [(forall A B x y, @fst A B (x, y) = x) + ; (forall A B x y, @snd A B (x, y) = y) + ; (forall r v, lower r = upper r -> cstZ r v = cstZ r ('(lower r))) + ; (forall r0 v, 0 ∈ r0 -> cstZ r0 0 + v = v) + ; (forall r0 v, 0 ∈ r0 -> v + cstZ r0 0 = v) + ; (forall r0 v, 0 ∈ r0 -> cstZ r0 0 - v = -v) + ; (forall r0 v, 0 ∈ r0 -> cstZ r0 0 << v = 0) + ; (forall r0 rnv rv v, + (rv <= -n rnv)%zrange -> 0 ∈ r0 + -> cstZ r0 0 - cstZ rnv (-(cstZ rv v)) = cstZ rv v) + ; (forall rnv rv v, + (rv <= -n rnv)%zrange + -> -(cstZ rnv (-(cstZ rv v))) = cstZ rv v) + + ; (forall s r0 y, 0 ∈ r0 -> Z.mul_split s (cstZ r0 0) y = (cstZ r[0~>0] 0, cstZ r[0~>0] 0)) + ; (forall s r0 y, 0 ∈ r0 -> Z.mul_split s y (cstZ r0 0) = (cstZ r[0~>0] 0, cstZ r[0~>0] 0)) + ; (forall rs s r1 ry y, + 1 ∈ r1 -> s ∈ rs -> (ry <= r[0~>s-1])%zrange + -> Z.mul_split (cstZ rs ('s)) (cstZ r1 1) (cstZ ry y) + = (cstZ ry y, cstZ r[0~>0] 0)) + ; (forall rs s r1 ry y, + 1 ∈ r1 -> s ∈ rs -> (ry <= r[0~>s-1])%zrange + -> Z.mul_split (cstZ rs ('s)) (cstZ ry y) (cstZ r1 1) + = (cstZ ry y, cstZ r[0~>0] 0)) + + ; (forall rvc s rny ry y x, + (ry <= -n rny)%zrange + -> cstZZ rvc (Z.add_get_carry_full s (cstZ rny (-cstZ ry y)) x) + = dlet2_opp2 rvc (Z.sub_get_borrow_full s x (cstZ ry y))) + ; (forall rvc s rny ry y x, + (ry <= -n rny)%zrange + -> cstZZ rvc (Z.add_get_carry_full s x (cstZ rny (-cstZ ry y))) + = dlet2_opp2 rvc (Z.sub_get_borrow_full s x (cstZ ry y))) + ; (forall rvc s ryy yy x, + yy ∈ ryy -> yy < 0 + -> cstZZ rvc (Z.add_get_carry_full s (cstZ ryy ('yy)) x) + = dlet2_opp2 rvc (Z.sub_get_borrow_full s x (cstZ (-ryy) ('(-yy))))) + ; (forall rvc s ryy yy x, + yy ∈ ryy -> yy < 0 + -> cstZZ rvc (Z.add_get_carry_full s x (cstZ ryy ('yy))) + = dlet2_opp2 rvc (Z.sub_get_borrow_full s x (cstZ (-ryy) ('(-yy))))) + ; (forall rvc s rnc rc c rny ry y x, + (ry <= -n rny)%zrange -> (rc <= -n rnc)%zrange + -> cstZZ rvc (Z.add_with_get_carry_full s (cstZ rnc (-cstZ rc c)) (cstZ rny (-cstZ ry y)) x) + = dlet2_opp2 rvc (Z.sub_with_get_borrow_full s (cstZ rc c) x (cstZ ry y))) + ; (forall rvc s rnc rc c rny ry y x, + (ry <= -n rny)%zrange -> (rc <= -n rnc)%zrange + -> cstZZ rvc (Z.add_with_get_carry_full s (cstZ rnc (-cstZ rc c)) x (cstZ rny (-cstZ ry y))) + = dlet2_opp2 rvc (Z.sub_with_get_borrow_full s (cstZ rc c) x (cstZ ry y))) + ; (forall rvc s r0 rny ry y x, + 0 ∈ r0 -> (ry <= -n rny)%zrange + -> cstZZ rvc (Z.add_with_get_carry_full s (cstZ r0 0) (cstZ rny (-cstZ ry y)) x) + = dlet2_opp2 rvc (Z.sub_get_borrow_full s x (cstZ ry y))) + ; (forall rvc s rcc cc rny ry y x, + cc < 0 -> cc ∈ rcc -> (ry <= -n rny)%zrange + -> cstZZ rvc (Z.add_with_get_carry_full s (cstZ rcc ('cc)) (cstZ rny (-cstZ ry y)) x) + = dlet2_opp2 rvc (Z.sub_with_get_borrow_full s (cstZ (-rcc) ('(-cc))) x (cstZ ry y))) + ; (forall rvc s r0 rny ry y x, + 0 ∈ r0 -> (ry <= -n rny)%zrange + -> cstZZ rvc (Z.add_with_get_carry_full s (cstZ r0 0) x (cstZ rny (-cstZ ry y))) + = dlet2_opp2 rvc (Z.sub_get_borrow_full s x (cstZ ry y))) + ; (forall rvc s rcc cc rny ry y x, + cc < 0 -> cc ∈ rcc -> (ry <= -n rny)%zrange + -> cstZZ rvc (Z.add_with_get_carry_full s (cstZ rcc ('cc)) x (cstZ rny (-cstZ ry y))) + = dlet2_opp2 rvc (Z.sub_with_get_borrow_full s (cstZ (-rcc) ('(-cc))) x (cstZ ry y))) + ; (forall rvc s rnc rc c ryy yy x, + yy <= 0 -> yy ∈ ryy -> (rc <= -n rnc)%zrange + -> cstZZ rvc (Z.add_with_get_carry_full s (cstZ rnc (-cstZ rc c)) (cstZ ryy ('yy)) x) + = dlet2_opp2 rvc (Z.sub_with_get_borrow_full s (cstZ rc c) x (cstZ (-ryy) ('(-yy))))) + ; (forall rvc s rnc rc c ryy yy x, + yy <= 0 -> yy ∈ ryy -> (rc <= -n rnc)%zrange + -> cstZZ rvc (Z.add_with_get_carry_full s (cstZ rnc (-cstZ rc c)) x (cstZ ryy ('yy))) + = dlet2_opp2 rvc (Z.sub_with_get_borrow_full s (cstZ rc c) x (cstZ (-ryy) ('(-yy))))) + ; (forall rvc s rcc cc ryy yy x, + yy <= 0 -> cc <= 0 -> yy + cc < 0 (* at least one must be strictly negative *) -> yy ∈ ryy -> cc ∈ rcc + -> cstZZ rvc (Z.add_with_get_carry_full s (cstZ rcc ('cc)) (cstZ ryy ('yy)) x) + = dlet2_opp2 rvc (Z.sub_with_get_borrow_full s (cstZ (-rcc) ('(-cc))) x (cstZ (-ryy) ('(-yy))))) + ; (forall rvc s rcc cc ryy yy x, + yy <= 0 -> cc <= 0 -> yy + cc < 0 (* at least one must be strictly negative *) -> yy ∈ ryy -> cc ∈ rcc + -> cstZZ rvc (Z.add_with_get_carry_full s (cstZ rcc ('cc)) x (cstZ ryy ('yy))) + = dlet2_opp2 rvc (Z.sub_with_get_borrow_full s (cstZ (-rcc) ('(-cc))) x (cstZ (-ryy) ('(-yy))))) + + + ; (forall rs s rxx xx ryy yy, + s ∈ rs -> xx ∈ rxx -> yy ∈ ryy + -> Z.add_get_carry_full (cstZ rs ('s)) (cstZ rxx ('xx)) (cstZ ryy ('yy)) + = litZZ (Z.add_get_carry_full s xx yy)) + ; (forall rs s r0 ry y, + s ∈ rs -> 0 ∈ r0 -> (ry <= r[0~>s-1])%zrange + -> Z.add_get_carry_full (cstZ rs ('s)) (cstZ r0 0) (cstZ ry y) + = (cstZ ry y, cstZ r[0~>0] 0)) + ; (forall rs s r0 ry y, + s ∈ rs -> 0 ∈ r0 -> (ry <= r[0~>s-1])%zrange + -> Z.add_get_carry_full (cstZ rs ('s)) (cstZ ry y) (cstZ r0 0) + = (cstZ ry y, cstZ r[0~>0] 0)) + + ; (forall r0 x y, 0 ∈ r0 -> Z.add_with_carry (cstZ r0 0) x y = x + y) + + ; (forall rs s rcc cc rxx xx ryy yy, + s ∈ rs -> cc ∈ rcc -> xx ∈ rxx -> yy ∈ ryy + -> Z.add_with_get_carry_full (cstZ rs ('s)) (cstZ rcc ('cc)) (cstZ rxx ('xx)) (cstZ ryy ('yy)) + = litZZ (Z.add_with_get_carry_full s cc xx yy)) + ; (forall rs s r0c r0x ry y, + s ∈ rs -> 0 ∈ r0c -> 0 ∈ r0x -> (ry <= r[0~>s-1])%zrange + -> Z.add_with_get_carry_full (cstZ rs ('s)) (cstZ r0c 0) (cstZ r0x 0) (cstZ ry y) + = (cstZ ry y, cstZ r[0~>0] 0)) + ; (forall rs s r0c r0x ry y, + s ∈ rs -> 0 ∈ r0c -> 0 ∈ r0x -> (ry <= r[0~>s-1])%zrange + -> Z.add_with_get_carry_full (cstZ rs ('s)) (cstZ r0c 0) (cstZ ry y) (cstZ r0x 0) + = (cstZ ry y, cstZ r[0~>0] 0)) + + ; (forall rvc s r0 x y, (* carry = 0: ADC x y -> ADD x y *) + 0 ∈ r0 + -> cstZZ rvc (Z.add_with_get_carry_full s (cstZ r0 0) x y) + = dlet2 rvc (Z.add_get_carry_full s x y)) + ; (forall rvc rs s rc c r0x r0y, (* ADC 0 0 -> (ADX 0 0, 0) *) (* except we don't do ADX, because C stringification doesn't handle it *) + 0 ∈ r0x -> 0 ∈ r0y -> (rc <= r[0~>s-1])%zrange -> 0 ∈ snd rvc -> s ∈ rs + -> cstZZ rvc (Z.add_with_get_carry_full (cstZ rs ('s)) (cstZ rc c) (cstZ r0x 0) (cstZ r0y 0)) + = (dlet vc := (cstZZ rvc (Z.add_with_get_carry_full (cstZ rs ('s)) (cstZ rc c) (cstZ r0x 0) (cstZ r0y 0))) in + (cstZ (fst rvc) (fst (cstZZ rvc vc)), + cstZ r[0~>0] 0))) + + (* let-bind any adc/sbb/mulx *) + ; (forall rvc s c x y, + cstZZ rvc (Z.add_with_get_carry_full s c x y) + = dlet2 rvc (Z.add_with_get_carry_full s c x y)) + ; (forall rv c x y, + cstZ rv (Z.add_with_carry c x y) + = (dlet vc := cstZ rv (Z.add_with_carry c x y) in + cstZ rv vc)) + ; (forall rvc s x y, + cstZZ rvc (Z.add_get_carry_full s x y) + = dlet2 rvc (Z.add_get_carry_full s x y)) + ; (forall rvc s c x y, + cstZZ rvc (Z.sub_with_get_borrow_full s c x y) + = dlet2 rvc (Z.sub_with_get_borrow_full s c x y)) + ; (forall rvc s x y, + cstZZ rvc (Z.sub_get_borrow_full s x y) + = dlet2 rvc (Z.sub_get_borrow_full s x y)) + ; (forall rvc s x y, + cstZZ rvc (Z.mul_split s x y) + = dlet2 rvc (Z.mul_split s x y)) + ]%Z%zrange + ; mymap + do_again + [ (* [do_again], so that if one of the arguments is concrete, we automatically get the rewrite rule for [Z_cast] applying to it *) + (forall r x y, cstZZ r (x, y) = (cstZ (fst r) x, cstZ (snd r) y)) + ] + ; mymap + dont_do_again + [(forall r1 r2 x, (r2 <= n r1)%zrange -> cstZ r1 (cstZ r2 x) = cstZ r2 x) + ]%Z%zrange + ]. + +Definition strip_literal_casts_rewrite_rulesT : list (bool * Prop) + := [dont_do_again (forall rx x, x ∈ rx -> cstZ rx ('x) = 'x)]%Z%zrange. + +Section fancy. + Context (invert_low invert_high : Z (*log2wordmax*) -> Z -> option Z) + (value_range flag_range : zrange). + + Definition fancy_rewrite_rulesT : list (bool * Prop) + := []. + + Local Coercion ZRange.constant : Z >-> zrange. (* for ease of use with sanity-checking bounds *) + Local Notation bounds1_good f + := (fun (output x_bs : zrange) + => is_tighter_than_bool (f (ZRange.normalize x_bs)) (ZRange.normalize output) = true). + Local Notation bounds2_good f + := (fun (output x_bs y_bs : zrange) + => is_tighter_than_bool (f (ZRange.normalize x_bs) (ZRange.normalize y_bs)) (ZRange.normalize output) = true). + Local Notation range_in_bitwidth r s + := (is_tighter_than_bool (ZRange.normalize r) r[0~>s-1]%zrange = true). + Local Notation shiftl_good := (bounds2_good ZRange.shiftl). + Local Notation shiftr_good := (bounds2_good ZRange.shiftr). + Local Notation land_good := (bounds2_good ZRange.land). + Local Notation mul_good := (bounds2_good ZRange.mul). + Local Notation cc_m_good output s := (bounds1_good (ZRange.cc_m s) output). + Local Notation lit_good x rx := (is_bounded_by_bool x (ZRange.normalize rx)). + + Definition fancy_with_casts_rewrite_rulesT : list (bool * Prop) + := Eval cbv [myapp mymap myflatten] in + myflatten + [mymap + dont_do_again + [(* +(Z.add_get_carry_concrete 2^256) @@ (?x, ?y << 128) --> (add 128) @@ (x, y) +(Z.add_get_carry_concrete 2^256) @@ (?x << 128, ?y) --> (add 128) @@ (y, x) +(Z.add_get_carry_concrete 2^256) @@ (?x, ?y >> 128) --> (add (- 128)) @@ (x, y) +(Z.add_get_carry_concrete 2^256) @@ (?x >> 128, ?y) --> (add (- 128)) @@ (y, x) +(Z.add_get_carry_concrete 2^256) @@ (?x, ?y) --> (add 0) @@ (y, x) + *) + (forall r rs s rx x rshiftl rland ry y rmask mask roffset offset, + s = 2^Z.log2 s -> s ∈ rs -> offset ∈ roffset -> mask ∈ rmask -> shiftl_good rshiftl rland offset -> land_good rland ry mask -> range_in_bitwidth rshiftl s -> (mask = Z.ones (Z.log2 s - offset)) -> (0 <= offset <= Z.log2 s) + -> cstZZ r (Z.add_get_carry_full (cstZ rs ('s)) (cstZ rx x) (cstZ rshiftl ((cstZ rland (cstZ ry y &' cstZ rmask ('mask))) << cstZ roffset ('offset)))) + = cstZZ r (ident.interp (ident.fancy_add (Z.log2 s) (offset)) (cstZ rx x, cstZ ry y))) + ; (forall r rs s rx x rshiftl rland ry y rmask mask roffset offset, + (s = 2^Z.log2 s) -> (mask = Z.ones (Z.log2 s - offset)) -> (0 <= offset <= Z.log2 s) -> s ∈ rs -> mask ∈ rmask -> offset ∈ roffset -> shiftl_good rshiftl rland offset -> land_good rland ry mask -> range_in_bitwidth rshiftl s + -> cstZZ r (Z.add_get_carry_full (cstZ rs ('s)) (cstZ rx x) (cstZ rshiftl (cstZ rland (cstZ ry y &' cstZ rmask ('mask)) << cstZ roffset ('offset)))) + = cstZZ r (ident.interp (ident.fancy_add (Z.log2 s) offset) (cstZ rx x, cstZ ry y))) + + ; (forall r rs s rshiftl rland ry y rmask mask roffset offset rx x, + s ∈ rs -> mask ∈ rmask -> offset ∈ roffset -> (s = 2^Z.log2 s) -> shiftl_good rshiftl rland offset -> land_good rland ry mask -> range_in_bitwidth rshiftl s -> (mask = Z.ones (Z.log2 s - offset)) -> (0 <= offset <= Z.log2 s) + -> cstZZ r (Z.add_get_carry_full (cstZ rs ('s)) (cstZ rshiftl (Z.shiftl (cstZ rland (Z.land (cstZ ry y) (cstZ rmask ('mask)))) (cstZ roffset ('offset)))) (cstZ rx x)) + = cstZZ r (ident.interp (ident.fancy_add (Z.log2 s) offset) (cstZ rx x, cstZ ry y))) + + ; (forall r rs s rx x rshiftr ry y roffset offset, + s ∈ rs -> offset ∈ roffset -> (s = 2^Z.log2 s) -> shiftr_good rshiftr ry offset -> range_in_bitwidth rshiftr s + -> cstZZ r (Z.add_get_carry_full (cstZ rs ('s)) (cstZ rx x) (cstZ rshiftr (Z.shiftr (cstZ ry y) (cstZ roffset ('offset))))) + = cstZZ r (ident.interp (ident.fancy_add (Z.log2 s) (-offset)) (cstZ rx x, cstZ ry y))) + + ; (forall r rs s rshiftr ry y roffset offset rx x, + s ∈ rs -> offset ∈ roffset -> (s = 2^Z.log2 s) -> shiftr_good rshiftr ry offset -> range_in_bitwidth rshiftr s + -> cstZZ r (Z.add_get_carry_full (cstZ rs ('s)) (cstZ rshiftr (Z.shiftr (cstZ ry y) (cstZ roffset ('offset)))) (cstZ rx x)) + = cstZZ r (ident.interp (ident.fancy_add (Z.log2 s) (-offset)) (cstZ rx x, cstZ ry y))) + + ; (forall r rs s rx x ry y, + s ∈ rs -> (s = 2^Z.log2 s) -> range_in_bitwidth ry s + -> cstZZ r (Z.add_get_carry_full (cstZ rs ('s)) (cstZ rx x) (cstZ ry y)) + = cstZZ r (ident.interp (ident.fancy_add (Z.log2 s) 0) (cstZ rx x, cstZ ry y))) + + (* +(Z.add_with_get_carry_concrete 2^256) @@ (?c, ?x, ?y << 128) --> (addc 128) @@ (c, x, y) +(Z.add_with_get_carry_concrete 2^256) @@ (?c, ?x << 128, ?y) --> (addc 128) @@ (c, y, x) +(Z.add_with_get_carry_concrete 2^256) @@ (?c, ?x, ?y >> 128) --> (addc (- 128)) @@ (c, x, y) +(Z.add_with_get_carry_concrete 2^256) @@ (?c, ?x >> 128, ?y) --> (addc (- 128)) @@ (c, y, x) +(Z.add_with_get_carry_concrete 2^256) @@ (?c, ?x, ?y) --> (addc 0) @@ (c, y, x) + *) + ; (forall r rs s rc c rx x rshiftl rland ry y rmask mask roffset offset, + s ∈ rs -> mask ∈ rmask -> offset ∈ roffset -> (s = 2^Z.log2 s) -> shiftl_good rshiftl rland offset -> land_good rland ry mask -> range_in_bitwidth rshiftl s -> (mask = Z.ones (Z.log2 s - offset)) -> (0 <= offset <= Z.log2 s) + -> cstZZ r (Z.add_with_get_carry_full (cstZ rs ('s)) (cstZ rc c) (cstZ rx x) (cstZ rshiftl (Z.shiftl (cstZ rland (Z.land (cstZ ry y) (cstZ rmask ('mask)))) (cstZ roffset ('offset))))) + = cstZZ r (ident.interp (ident.fancy_addc (Z.log2 s) offset) (cstZ rc c, cstZ rx x, cstZ ry y))) + + ; (forall r rs s rc c rshiftl rland ry y rmask mask roffset offset rx x, + s ∈ rs -> mask ∈ rmask -> offset ∈ roffset -> (s = 2^Z.log2 s) -> shiftl_good rshiftl rland offset -> range_in_bitwidth rshiftl s -> land_good rland ry mask -> (mask = Z.ones (Z.log2 s - offset)) -> (0 <= offset <= Z.log2 s) + -> cstZZ r (Z.add_with_get_carry_full (cstZ rs ('s)) (cstZ rc c) (cstZ rshiftl (Z.shiftl (cstZ rland (Z.land (cstZ ry y) (cstZ rmask ('mask)))) (cstZ roffset ('offset)))) (cstZ rx x)) + = cstZZ r (ident.interp (ident.fancy_addc (Z.log2 s) offset) (cstZ rc c, cstZ rx x, cstZ ry y))) + + ; (forall r rs s rc c rx x rshiftr ry y roffset offset, + s ∈ rs -> offset ∈ roffset -> (s = 2^Z.log2 s) -> shiftr_good rshiftr ry offset -> range_in_bitwidth rshiftr s + -> cstZZ r (Z.add_with_get_carry_full (cstZ rs ('s)) (cstZ rc c) (cstZ rx x) (cstZ rshiftr (Z.shiftr (cstZ ry y) (cstZ roffset ('offset))))) + = cstZZ r (ident.interp (ident.fancy_addc (Z.log2 s) (-offset)) (cstZ rc c, cstZ rx x, cstZ ry y))) + + ; (forall r rs s rc c rshiftr ry y roffset offset rx x, + s ∈ rs -> offset ∈ roffset -> (s = 2^Z.log2 s) -> shiftr_good rshiftr ry offset -> range_in_bitwidth rshiftr s + -> cstZZ r (Z.add_with_get_carry_full (cstZ rs ('s)) (cstZ rc c) (cstZ rshiftr (Z.shiftr (cstZ ry y) (cstZ roffset ('offset)))) (cstZ rx x)) + = cstZZ r (ident.interp (ident.fancy_addc (Z.log2 s) (-offset)) (cstZ rc c, cstZ rx x, cstZ ry y))) + + ; (forall r rs s rc c rx x ry y, + s ∈ rs -> (s = 2^Z.log2 s) -> range_in_bitwidth ry s + -> cstZZ r (Z.add_with_get_carry_full (cstZ rs ('s)) (cstZ rc c) (cstZ rx x) (cstZ ry y)) + = cstZZ r (ident.interp (ident.fancy_addc (Z.log2 s) 0) (cstZ rc c, cstZ rx x, cstZ ry y))) + + (* +(Z.sub_get_borrow_concrete 2^256) @@ (?x, ?y << 128) --> (sub 128) @@ (x, y) +(Z.sub_get_borrow_concrete 2^256) @@ (?x, ?y >> 128) --> (sub (- 128)) @@ (x, y) +(Z.sub_get_borrow_concrete 2^256) @@ (?x, ?y) --> (sub 0) @@ (y, x) + *) + + ; (forall r rs s rx x rshiftl rland ry y rmask mask roffset offset, + s ∈ rs -> mask ∈ rmask -> offset ∈ roffset -> (s = 2^Z.log2 s) -> shiftl_good rshiftl rland offset -> range_in_bitwidth rshiftl s -> land_good rland ry mask -> (mask = Z.ones (Z.log2 s - offset)) -> (0 <= offset <= Z.log2 s) + -> cstZZ r (Z.sub_get_borrow_full (cstZ rs ('s)) (cstZ rx x) (cstZ rshiftl (Z.shiftl (cstZ rland (Z.land (cstZ ry y) (cstZ rmask ('mask)))) (cstZ roffset ('offset))))) + = cstZZ r (ident.interp (ident.fancy_sub (Z.log2 s) offset) (cstZ rx x, cstZ ry y))) + + ; (forall r rs s rx x rshiftr ry y roffset offset, + s ∈ rs -> offset ∈ roffset -> (s = 2^Z.log2 s) -> shiftr_good rshiftr ry offset -> range_in_bitwidth rshiftr s + -> cstZZ r (Z.sub_get_borrow_full (cstZ rs ('s)) (cstZ rx x) (cstZ rshiftr (Z.shiftr (cstZ ry y) (cstZ roffset ('offset))))) + = cstZZ r (ident.interp (ident.fancy_sub (Z.log2 s) (-offset)) (cstZ rx x, cstZ ry y))) + + ; (forall r rs s rx x ry y, + s ∈ rs -> (s = 2^Z.log2 s) -> range_in_bitwidth ry s + -> cstZZ r (Z.sub_get_borrow_full (cstZ rs ('s)) (cstZ rx x) (cstZ ry y)) + = cstZZ r (ident.interp (ident.fancy_sub (Z.log2 s) 0) (cstZ rx x, cstZ ry y))) + + (* +(Z.sub_with_get_borrow_concrete 2^256) @@ (?c, ?x, ?y << 128) --> (subb 128) @@ (c, x, y) +(Z.sub_with_get_borrow_concrete 2^256) @@ (?c, ?x, ?y >> 128) --> (subb (- 128)) @@ (c, x, y) +(Z.sub_with_get_borrow_concrete 2^256) @@ (?c, ?x, ?y) --> (subb 0) @@ (c, y, x) + *) + + ; (forall r rs s rb b rx x rshiftl rland ry y rmask mask roffset offset, + s ∈ rs -> mask ∈ rmask -> offset ∈ roffset -> (s = 2^Z.log2 s) -> shiftl_good rshiftl rland offset -> range_in_bitwidth rshiftl s -> land_good rland ry mask -> (mask = Z.ones (Z.log2 s - offset)) -> (0 <= offset <= Z.log2 s) + -> cstZZ r (Z.sub_with_get_borrow_full (cstZ rs ('s)) (cstZ rb b) (cstZ rx x) (cstZ rshiftl (Z.shiftl (cstZ rland (Z.land (cstZ ry y) (cstZ rmask ('mask)))) (cstZ roffset ('offset))))) + = cstZZ r (ident.interp (ident.fancy_subb (Z.log2 s) offset) (cstZ rb b, cstZ rx x, cstZ ry y))) + + ; (forall r rs s rb b rx x rshiftr ry y roffset offset, + s ∈ rs -> offset ∈ roffset -> (s = 2^Z.log2 s) -> shiftr_good rshiftr ry offset -> range_in_bitwidth rshiftr s + -> cstZZ r (Z.sub_with_get_borrow_full (cstZ rs ('s)) (cstZ rb b) (cstZ rx x) (cstZ rshiftr (Z.shiftr (cstZ ry y) (cstZ roffset ('offset))))) + = cstZZ r (ident.interp (ident.fancy_subb (Z.log2 s) (-offset)) (cstZ rb b, cstZ rx x, cstZ ry y))) + + ; (forall r rs s rb b rx x ry y, + s ∈ rs -> (s = 2^Z.log2 s) -> range_in_bitwidth ry s + -> cstZZ r (Z.sub_with_get_borrow_full (cstZ rs ('s)) (cstZ rb b) (cstZ rx x) (cstZ ry y)) + = cstZZ r (ident.interp (ident.fancy_subb (Z.log2 s) 0) (cstZ rb b, cstZ rx x, cstZ ry y))) + + (*(Z.rshi_concrete 2^256 ?n) @@ (?c, ?x, ?y) --> (rshi n) @@ (x, y)*) + + ; (forall r rs s rx x ry y rn n, + s ∈ rs -> n ∈ rn -> (s = 2^Z.log2 s) + -> cstZ r (Z.rshi (cstZ rs ('s)) (cstZ rx x) (cstZ ry y) (cstZ rn ('n))) + = cstZ r (ident.interp (ident.fancy_rshi (Z.log2 s) n) (cstZ rx x, cstZ ry y))) + + (* +Z.zselect @@ (Z.cc_m_concrete 2^256 ?c, ?x, ?y) --> selm @@ (c, x, y) +Z.zselect @@ (?c &' 1, ?x, ?y) --> sell @@ (c, x, y) +Z.zselect @@ (?c, ?x, ?y) --> selc @@ (c, x, y) + *) + ; (forall r rccm rs s rc c rx x ry y, + s ∈ rs -> (s = 2^Z.log2 s) -> cc_m_good rccm s rc + -> cstZ r (Z.zselect (cstZ rccm (Z.cc_m (cstZ rs ('s)) (cstZ rc c))) (cstZ rx x) (cstZ ry y)) + = cstZ r (ident.interp (ident.fancy_selm (Z.log2 s)) (cstZ rc c, cstZ rx x, cstZ ry y))) + + ; (forall r rland r1 rc c rx x ry y, + 1 ∈ r1 -> land_good rland 1 rc + -> cstZ r (Z.zselect (cstZ rland (cstZ r1 1 &' cstZ rc c)) (cstZ rx x) (cstZ ry y)) + = cstZ r (ident.interp ident.fancy_sell (cstZ rc c, cstZ rx x, cstZ ry y))) + + ; (forall r rland rc c r1 rx x ry y, + 1 ∈ r1 -> land_good rland rc 1 + -> cstZ r (Z.zselect (cstZ rland (cstZ rc c &' cstZ r1 1)) (cstZ rx x) (cstZ ry y)) + = cstZ r (ident.interp ident.fancy_sell (cstZ rc c, cstZ rx x, cstZ ry y))) + + ; (forall r c x y, + cstZ r (Z.zselect c x y) + = cstZ r (ident.interp ident.fancy_selc (c, x, y))) + + (*Z.add_modulo @@ (?x, ?y, ?m) --> addm @@ (x, y, m)*) + ; (forall x y m, + Z.add_modulo x y m + = ident.interp ident.fancy_addm (x, y, m)) + + (* +Z.mul @@ (?x &' (2^128-1), ?y &' (2^128-1)) --> mulll @@ (x, y) +Z.mul @@ (?x &' (2^128-1), ?y >> 128) --> mullh @@ (x, y) +Z.mul @@ (?x >> 128, ?y &' (2^128-1)) --> mulhl @@ (x, y) +Z.mul @@ (?x >> 128, ?y >> 128) --> mulhh @@ (x, y) + *) + (* literal on left *) + ; (forall r rx x rland ry y rmask mask, + plet s := (2*Z.log2_up mask)%Z in + plet xo := invert_low s x in + plet xv := match xo with Some x => x | None => 0 end in + xo <> None -> x ∈ rx -> mask ∈ rmask -> (mask = 2^(s/2)-1) -> land_good rland ry mask + -> cstZ r (cstZ rx ('x) * cstZ rland (Z.land (cstZ ry y) (cstZ rmask ('mask)))) + = cstZ r (ident.interp (ident.fancy_mulll s) ('xv, cstZ ry y))) + + ; (forall r rx x rland rmask mask ry y, + plet s := (2*Z.log2_up mask)%Z in + plet xo := invert_low s x in + plet xv := match xo with Some x => x | None => 0 end in + xo <> None -> x ∈ rx -> mask ∈ rmask -> (mask = 2^(s/2)-1) -> land_good rland mask ry + -> cstZ r (cstZ rx ('x) * cstZ rland (Z.land (cstZ rmask ('mask)) (cstZ ry y))) + = cstZ r (ident.interp (ident.fancy_mulll s) ('xv, cstZ ry y))) + + ; (forall r rx x rshiftr ry y roffset offset, + plet s := (2*offset)%Z in + plet xo := invert_low s x in + plet xv := match xo with Some x => x | None => 0 end in + xo <> None -> x ∈ rx -> offset ∈ roffset -> shiftr_good rshiftr ry offset + -> cstZ r (cstZ rx ('x) * cstZ rshiftr (Z.shiftr (cstZ ry y) (cstZ roffset ('offset)))) + = cstZ r (ident.interp (ident.fancy_mullh s) ('xv, cstZ ry y))) + + ; (forall r rx x rland rmask mask ry y, + plet s := (2*Z.log2_up mask)%Z in + plet xo := invert_high s x in + plet xv := match xo with Some x => x | None => 0 end in + xo <> None -> x ∈ rx -> mask ∈ rmask -> (mask = 2^(s/2)-1) -> land_good rland mask ry + -> cstZ r (cstZ rx ('x) * cstZ rland (Z.land (cstZ rmask ('mask)) (cstZ ry y))) + = cstZ r (ident.interp (ident.fancy_mulhl s) ('xv, cstZ ry y))) + + ; (forall r rx x rland ry y rmask mask, + plet s := (2*Z.log2_up mask)%Z in + plet xo := invert_high s x in + plet xv := match xo with Some x => x | None => 0 end in + xo <> None -> x ∈ rx -> mask ∈ rmask -> (mask = 2^(s/2)-1) -> land_good rland ry mask + -> cstZ r (cstZ rx ('x) * cstZ rland (Z.land (cstZ ry y) (cstZ rmask ('mask)))) + = cstZ r (ident.interp (ident.fancy_mulhl s) ('xv, cstZ ry y))) + + ; (forall r rx x rshiftr ry y roffset offset, + plet s := (2*offset)%Z in + plet xo := invert_high s x in + plet xv := match xo with Some x => x | None => 0 end in + xo <> None -> x ∈ rx -> offset ∈ roffset -> shiftr_good rshiftr ry offset + -> cstZ r (cstZ rx ('x) * cstZ rshiftr (Z.shiftr (cstZ ry y) (cstZ roffset ('offset)))) + = cstZ r (ident.interp (ident.fancy_mulhh s) ('xv, cstZ ry y))) + + (* literal on right *) + ; (forall r rland rmask mask rx x ry y, + plet s := (2*Z.log2_up mask)%Z in + plet yo := invert_low s y in + plet yv := match yo with Some y => y | None => 0 end in + yo <> None -> y ∈ ry -> mask ∈ rmask -> (mask = 2^(s/2)-1) -> land_good rland mask rx + -> cstZ r (cstZ rland (Z.land (cstZ rmask ('mask)) (cstZ rx x)) * cstZ ry ('y)) + = cstZ r (ident.interp (ident.fancy_mulll s) (cstZ rx x, 'yv))) + + ; (forall r rland rx x rmask mask ry y, + plet s := (2*Z.log2_up mask)%Z in + plet yo := invert_low s y in + plet yv := match yo with Some y => y | None => 0 end in + yo <> None -> y ∈ ry -> mask ∈ rmask -> (mask = 2^(s/2)-1) -> land_good rland rx mask + -> cstZ r (cstZ rland (Z.land (cstZ rx x) (cstZ rmask ('mask))) * cstZ ry ('y)) + = cstZ r (ident.interp (ident.fancy_mulll s) (cstZ rx x, 'yv))) + + ; (forall r rland rmask mask rx x ry y, + plet s := (2*Z.log2_up mask)%Z in + plet yo := invert_high s y in + plet yv := match yo with Some y => y | None => 0 end in + yo <> None -> y ∈ ry -> mask ∈ rmask -> (mask = 2^(s/2)-1) -> land_good rland mask rx + -> cstZ r (cstZ rland (Z.land (cstZ rmask ('mask)) (cstZ rx x)) * cstZ ry ('y)) + = cstZ r (ident.interp (ident.fancy_mullh s) (cstZ rx x, 'yv))) + + ; (forall r rland rx x rmask mask ry y, + plet s := (2*Z.log2_up mask)%Z in + plet yo := invert_high s y in + plet yv := match yo with Some y => y | None => 0 end in + yo <> None -> y ∈ ry -> mask ∈ rmask -> (mask = 2^(s/2)-1) -> land_good rland rx mask + -> cstZ r (cstZ rland (Z.land (cstZ rx x) (cstZ rmask ('mask))) * cstZ ry ('y)) + = cstZ r (ident.interp (ident.fancy_mullh s) (cstZ rx x, 'yv))) + + ; (forall r rshiftr rx x roffset offset ry y, + plet s := (2*offset)%Z in + plet yo := invert_low s y in + plet yv := match yo with Some y => y | None => 0 end in + yo <> None -> y ∈ ry -> offset ∈ roffset -> shiftr_good rshiftr rx offset + -> cstZ r (cstZ rshiftr (Z.shiftr (cstZ rx x) (cstZ roffset ('offset))) * cstZ ry ('y)) + = cstZ r (ident.interp (ident.fancy_mulhl s) (cstZ rx x, 'yv))) + + ; (forall r rshiftr rx x roffset offset ry y, + plet s := (2*offset)%Z in + plet yo := invert_high s y in + plet yv := match yo with Some y => y | None => 0 end in + yo <> None -> y ∈ ry -> offset ∈ roffset -> shiftr_good rshiftr rx offset + -> cstZ r (cstZ rshiftr (Z.shiftr (cstZ rx x) (cstZ roffset ('offset))) * cstZ ry ('y)) + = cstZ r (ident.interp (ident.fancy_mulhh s) (cstZ rx x, 'yv))) + + (* no literal *) + ; (forall r rland1 rmask1 mask1 rx x rland2 rmask2 mask2 ry y, + plet s := (2*Z.log2_up mask1)%Z in + mask1 ∈ rmask1 -> mask2 ∈ rmask2 -> (mask1 = 2^(s/2)-1) -> (mask2 = 2^(s/2)-1) -> land_good rland1 mask1 rx -> land_good rland2 mask2 ry + -> cstZ r (cstZ rland1 (Z.land (cstZ rmask1 ('mask1)) (cstZ rx x)) * cstZ rland2 (Z.land (cstZ rmask2 ('mask2)) (cstZ ry y))) + = cstZ r (ident.interp (ident.fancy_mulll s) (cstZ rx x, cstZ ry y))) + + ; (forall r rland1 rx x rmask1 mask1 rland2 rmask2 mask2 ry y, + plet s := (2*Z.log2_up mask1)%Z in + mask1 ∈ rmask1 -> mask2 ∈ rmask2 -> (mask1 = 2^(s/2)-1) -> (mask2 = 2^(s/2)-1) -> land_good rland1 rx mask1 -> land_good rland2 mask2 ry + -> cstZ r (cstZ rland1 (Z.land (cstZ rx x) (cstZ rmask1 ('mask1))) * cstZ rland2 (Z.land (cstZ rmask2 ('mask2)) (cstZ ry y))) + = cstZ r (ident.interp (ident.fancy_mulll s) (cstZ rx x, cstZ ry y))) + + ; (forall r rland1 rmask1 mask1 rx x rland2 ry y rmask2 mask2, + plet s := (2*Z.log2_up mask1)%Z in + mask1 ∈ rmask1 -> mask2 ∈ rmask2 -> (mask1 = 2^(s/2)-1) -> (mask2 = 2^(s/2)-1) -> land_good rland1 mask1 rx -> land_good rland2 ry mask2 + -> cstZ r (cstZ rland1 (Z.land (cstZ rmask1 ('mask1)) (cstZ rx x)) * cstZ rland2 (Z.land (cstZ ry y) (cstZ rmask2 ('mask2)))) + = cstZ r (ident.interp (ident.fancy_mulll s) (cstZ rx x, cstZ ry y))) + + ; (forall r rland1 rx x rmask1 mask1 rland2 ry y rmask2 mask2, + plet s := (2*Z.log2_up mask1)%Z in + mask1 ∈ rmask1 -> mask2 ∈ rmask2 -> (mask1 = 2^(s/2)-1) -> (mask2 = 2^(s/2)-1) -> land_good rland1 rx mask1 -> land_good rland2 ry mask2 + -> cstZ r (cstZ rland1 (Z.land (cstZ rx x) (cstZ rmask1 ('mask1))) * cstZ rland2 (Z.land (cstZ ry y) (cstZ rmask2 ('mask2)))) + = cstZ r (ident.interp (ident.fancy_mulll s) (cstZ rx x, cstZ ry y))) + + ; (forall r rland1 rmask mask rx x rshiftr2 ry y roffset offset, + plet s := (2*offset)%Z in + mask ∈ rmask -> offset ∈ roffset -> (mask = 2^(s/2)-1) -> land_good rland1 mask rx -> shiftr_good rshiftr2 ry offset + -> cstZ r (cstZ rland1 (Z.land (cstZ rmask ('mask)) (cstZ rx x)) * cstZ rshiftr2 (Z.shiftr (cstZ ry y) (cstZ roffset ('offset)))) + = cstZ r (ident.interp (ident.fancy_mullh s) (cstZ rx x, cstZ ry y))) + + ; (forall r rland1 rx x rmask mask rshiftr2 ry y roffset offset, + plet s := (2*offset)%Z in + mask ∈ rmask -> offset ∈ roffset -> (mask = 2^(s/2)-1) -> land_good rland1 rx mask -> shiftr_good rshiftr2 ry offset + -> cstZ r (cstZ rland1 (Z.land (cstZ rx x) (cstZ rmask ('mask))) * cstZ rshiftr2 (Z.shiftr (cstZ ry y) (cstZ roffset ('offset)))) + = cstZ r (ident.interp (ident.fancy_mullh s) (cstZ rx x, cstZ ry y))) + + ; (forall r rshiftr1 rx x roffset offset rland2 rmask mask ry y, + plet s := (2*offset)%Z in + mask ∈ rmask -> offset ∈ roffset -> (mask = 2^(s/2)-1) -> shiftr_good rshiftr1 rx offset -> land_good rland2 mask ry + -> cstZ r (cstZ rshiftr1 (Z.shiftr (cstZ rx x) (cstZ roffset ('offset))) * cstZ rland2 (Z.land (cstZ rmask ('mask)) (cstZ ry y))) + = cstZ r (ident.interp (ident.fancy_mulhl s) (cstZ rx x, cstZ ry y))) + + ; (forall r rshiftr1 rx x roffset offset rland2 ry y rmask mask, + plet s := (2*offset)%Z in + mask ∈ rmask -> offset ∈ roffset -> (mask = 2^(s/2)-1) -> shiftr_good rshiftr1 rx offset -> land_good rland2 ry mask + -> cstZ r (cstZ rshiftr1 (Z.shiftr (cstZ rx x) (cstZ roffset ('offset))) * cstZ rland2 (Z.land (cstZ ry y) (cstZ rmask ('mask)))) + = cstZ r (ident.interp (ident.fancy_mulhl s) (cstZ rx x, cstZ ry y))) + + ; (forall r rshiftr1 rx x roffset1 offset1 rshiftr2 ry y roffset2 offset2, + plet s := (2*offset1)%Z in + offset1 ∈ roffset1 -> offset2 ∈ roffset2 -> (offset1 = offset2) -> shiftr_good rshiftr1 rx offset1 -> shiftr_good rshiftr2 ry offset2 + -> cstZ r (cstZ rshiftr1 (Z.shiftr (cstZ rx x) (cstZ roffset1 ('offset1))) * cstZ rshiftr2 (Z.shiftr (cstZ ry y) (cstZ roffset2 ('offset2)))) + = cstZ r (ident.interp (ident.fancy_mulhh s) (cstZ rx x, cstZ ry y))) + + (** Dummy rule to make sure we use the two value ranges; this can be removed *) + ; (forall rx x, + ((is_tighter_than_bool rx value_range = true) + \/ (is_tighter_than_bool rx flag_range = true)) + -> cstZ rx x = cstZ rx x) + ]%Z%zrange + ]. +End fancy. diff --git a/src/RewriterRulesProofs.v b/src/RewriterRulesProofs.v new file mode 100644 index 000000000..0b6317167 --- /dev/null +++ b/src/RewriterRulesProofs.v @@ -0,0 +1,485 @@ +Require Import Coq.micromega.Lia. +Require Import Coq.ZArith.ZArith. +Require Import Crypto.Util.ListUtil Coq.Lists.List Crypto.Util.ListUtil.FoldBool. +(* +Require Import Crypto.Util.Option. +Require Import Crypto.Util.OptionList. +Require Import Crypto.Util.CPSNotations. +Require Import Crypto.Util.Bool.Reflect. + *) +Require Import Crypto.Util.ZRange. +Require Import Crypto.Util.ZRange.Operations. +Require Import Crypto.Util.ZUtil.Definitions. +Require Import Crypto.Util.ZUtil.Notations. +Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. +Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem. +Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo. +Require Import Crypto.Util.ZUtil.Hints. +Require Import Crypto.Util.ZUtil.Hints.Core. +Require Import Crypto.Util.ZUtil.ZSimplify.Core. +Require Import Crypto.Util.ZUtil.ZSimplify. +Require Import Crypto.Util.ZUtil.ZSimplify.Simple. +Require Import Crypto.Util.ZUtil.Definitions. +Require Import Crypto.Util.ZUtil.AddGetCarry. +Require Import Crypto.Util.ZUtil.MulSplit. +Require Import Crypto.Util.ZUtil.Zselect. +Require Import Crypto.Util.ZUtil.Div. +Require Import Crypto.Util.ZUtil.Modulo. +Require Import Crypto.Util.ZRange. +Require Import Crypto.Util.ZRange.Operations. +Require Import Crypto.Util.ZRange.BasicLemmas. +Require Import Crypto.Util.ZRange.OperationsBounds. +Require Import Crypto.Util.Tactics.NormalizeCommutativeIdentifier. +Require Import Crypto.Util.Tactics.BreakMatch. +Require Import Crypto.Util.Tactics.SplitInContext. +Require Import Crypto.Util.Tactics.SpecializeAllWays. +Require Import Crypto.Util.Tactics.SpecializeBy. +Require Import Crypto.Util.Tactics.RewriteHyp. +Require Import Crypto.Util.Tactics.Head. +Require Import Crypto.Util.Tactics.SetEvars. +Require Import Crypto.Util.Tactics.SubstEvars. +Require Import Crypto.Util.Prod. +Require Import Crypto.Util.Bool. +Require Import Crypto.Util.ListUtil. +Require Import Crypto.Util.ListUtil.Forall. +Require Import Crypto.Util.ListUtil.ForallIn. +Require Import Crypto.Util.NatUtil. +Require Import Crypto.Util.Option. +Require Import Crypto.Util.CPSNotations. +Require Import Crypto.Util.HProp. +Require Import Crypto.Util.Decidable. +Require Crypto.Util.PrimitiveProd. +Require Crypto.Util.PrimitiveHList. +Require Import Crypto.Language. +Require Import Crypto.LanguageWf. +Require Import Crypto.RewriterRules. +Require Import Crypto.Util.LetIn. +Require Import Crypto.Util.Tactics.Head. +Require Import Crypto.Util.Notations. +Import ListNotations. Local Open Scope bool_scope. Local Open Scope Z_scope. + +Local Definition mymap {A B} := Eval cbv in @List.map A B. +Local Definition myapp {A} := Eval cbv in @List.app A. +Local Definition myflatten {A} := Eval cbv in List.fold_right myapp (@nil A). +Local Notation dont_do_again := (pair false) (only parsing). +Local Notation do_again := (pair true) (only parsing). + +Import Language.Compilers. +Import LanguageWf.Compilers. + +Local Ltac start_proof := + cbv [snd]; hnf; cbv [PrimitiveHList.hlist ident.eagerly ident.literal ident.interp ident.fancy.interp ident.fancy.interp_with_wordmax Let_In ident.to_fancy invert_Some ident.cast2]; + repeat apply PrimitiveProd.Primitive.pair; try exact tt. + +Local Hint Resolve + eq_repeat_nat_rect + eq_app_list_rect + eq_combine_list_rect + eq_firstn_nat_rect + eq_skipn_nat_rect + eq_update_nth_nat_rect + : core. + +Lemma nbe_rewrite_rules_proofs + : PrimitiveHList.hlist (@snd bool Prop) nbe_rewrite_rulesT. +Proof using Type. start_proof; auto. Qed. + +Definition nbe_rewrite_rules_with_proofs + := Eval cbv [PrimitiveHList.combine_hlist nbe_rewrite_rulesT] in + PrimitiveHList.combine_hlist _ nbe_rewrite_rules_proofs. + +Local Ltac interp_good_t_step_related := + first [ lazymatch goal with + | [ |- ?x = ?x ] => reflexivity + | [ |- True ] => exact I + | [ H : ?x = true, H' : ?x = false |- _ ] => exfalso; clear -H H'; congruence + | [ |- ?G ] => has_evar G; reflexivity + | [ |- context[expr.interp_related_gen _ _ _ _] ] => reflexivity + | [ |- context[_ == _] ] => reflexivity + (*| [ |- context[(fst ?x, snd ?x)] ] => progress eta_expand + | [ |- context[match ?x with pair a b => _ end] ] => progress eta_expand*) + end + | progress cbn [fst snd] in * + | match goal with + | [ H : zrange * zrange |- _ ] => destruct H + end + | progress intros + | progress subst + | assumption + | progress inversion_option + | progress destruct_head'_and + | progress destruct_head'_unit + | progress split_andb + | match goal with + | [ H : ?x = ?x -> _ |- _ ] => specialize (H eq_refl) + | [ H : forall v : unit, _ |- _ ] => specialize (H tt) + | [ H : negb ?b = true |- _ ] => rewrite (@Bool.negb_true_iff b) in H + | [ |- context[Z.mul_split ?a ?b ?c] ] + => rewrite (surjective_pairing (Z.mul_split a b c)), Z.mul_split_div, Z.mul_split_mod + | [ |- context[Z.zselect] ] => rewrite Z.zselect_correct + | [ |- context[Z.sub_get_borrow_full ?a ?b ?c] ] + => rewrite (surjective_pairing (Z.sub_get_borrow_full a b c)), Z.sub_get_borrow_full_div, Z.sub_get_borrow_full_mod + | [ |- context[Z.sub_with_get_borrow_full ?a ?b ?c ?d] ] + => rewrite (surjective_pairing (Z.sub_with_get_borrow_full a b c d)), Z.sub_with_get_borrow_full_div, Z.sub_with_get_borrow_full_mod + | [ |- context[Z.add_get_carry_full ?a ?b ?c] ] + => rewrite (surjective_pairing (Z.add_get_carry_full a b c)), Z.add_get_carry_full_div, Z.add_get_carry_full_mod + | [ |- context[Z.add_with_get_carry_full ?a ?b ?c ?d] ] + => rewrite (surjective_pairing (Z.add_with_get_carry_full a b c d)), Z.add_with_get_carry_full_div, Z.add_with_get_carry_full_mod + | [ |- pair _ _ = pair _ _ ] => apply f_equal2 + | [ |- ?a mod ?b = ?a' mod ?b ] => apply f_equal2; lia + | [ |- ?a / ?b = ?a' / ?b ] => apply f_equal2; lia + | [ |- Z.opp _ = Z.opp _ ] => apply f_equal + end + | break_innermost_match_step + | break_innermost_match_hyps_step + | progress destruct_head'_or ]. + +Lemma arith_rewrite_rules_proofs (max_const_val : Z) + : PrimitiveHList.hlist (@snd bool Prop) (arith_rewrite_rulesT max_const_val). +Proof using Type. + start_proof; auto; intros; try lia. + all: autorewrite with zsimplify_const; try reflexivity. + all: repeat first [ reflexivity + | match goal with + | [ |- context[Z.shiftl] ] => rewrite Z.shiftl_mul_pow2 by auto with zarith + | [ |- context[Z.shiftr] ] => rewrite Z.shiftr_div_pow2 by auto with zarith + | [ H : ?x = 2^?n |- context[Z.land _ (?x - 1)] ] + => rewrite !Z.sub_1_r, H, <- Z.ones_equiv, Z.land_ones by auto with zarith + end + | Z.div_mod_to_quot_rem; nia + | interp_good_t_step_related ]. +Qed. + +Local Ltac interp_good_t_step_arith := + first [ lazymatch goal with + | [ |- ?x = ?x ] => reflexivity + | [ |- True ] => exact I + | [ H : ?x = true, H' : ?x = false |- _ ] => exfalso; clear -H H'; congruence + | [ H : true = false |- _ ]=> exfalso; clear -H; congruence + | [ H : false = true |- _ ]=> exfalso; clear -H; congruence + end + | progress cbv [option_beq] in * + | match goal with + | [ H : context[ZRange.normalize (ZRange.normalize _)] |- _ ] + => rewrite ZRange.normalize_idempotent in H + | [ |- context[ZRange.normalize (ZRange.normalize _)] ] + => rewrite ZRange.normalize_idempotent + | [ |- context[ident.cast (ZRange.normalize ?r)] ] + => rewrite ident.cast_normalize + | [ H : context[ident.cast (ZRange.normalize ?r)] |- _ ] + => rewrite ident.cast_normalize in H + | [ H : ?T, H' : ?T |- _ ] => clear H' + | [ H : context[is_bounded_by_bool _ (ZRange.normalize (-_))] |- _ ] + => rewrite ZRange.is_bounded_by_bool_move_opp_normalize in H + | [ |- context[is_bounded_by_bool _ (ZRange.normalize (-_))] ] + => rewrite ZRange.is_bounded_by_bool_move_opp_normalize + | [ H : is_bounded_by_bool ?v (ZRange.normalize ?r) = true |- context[ident.cast _ ?r ?v] ] + => rewrite (@ident.cast_in_normalized_bounds _ r v) by exact H + | [ H : is_bounded_by_bool ?v (ZRange.normalize ?r) = true |- context[ident.cast _ (-?r) (-?v)] ] + => rewrite (@ident.cast_in_normalized_bounds _ (-r) (-v)); + [ | clear -H ] + | [ |- context[ident.cast _ ?r (-ident.cast _ (-?r) ?v)] ] + => rewrite (ident.cast_in_normalized_bounds r (-ident.cast _ (-r) v)) + by (rewrite <- ZRange.is_bounded_by_bool_move_opp_normalize; apply ident.cast_always_bounded) + | [ |- context[ident.cast _ ?r (ident.cast _ ?r _)] ] + => rewrite (@ident.cast_idempotent _ _ r) + | [ H : is_bounded_by_bool _ ?r = true |- _] + => is_var r; unique pose proof (ZRange.is_bounded_by_normalize _ _ H) + | [ H : lower ?x = upper ?x |- _ ] => is_var x; destruct x; cbn [upper lower] in * + | [ H : is_bounded_by_bool ?x (ZRange.normalize r[?y~>?y]) = true |- _ ] + => apply ZRange.is_bounded_by_bool_normalize_constant_iff in H + | [ H : is_bounded_by_bool ?x r[?y~>?y] = true |- _ ] + => apply ZRange.is_bounded_by_bool_constant_iff in H + end + | progress intros + | progress subst + | assumption + | progress destruct_head'_and + | progress Z.ltb_to_lt + | progress split_andb + | match goal with + | [ |- ?a mod ?b = ?a' mod ?b ] => apply f_equal2; lia + | [ |- ?a / ?b = ?a' / ?b ] => apply f_equal2; lia + | [ |- Z.opp _ = Z.opp _ ] => apply f_equal + end + | break_innermost_match_step + | break_innermost_match_hyps_step + | progress destruct_head'_or + | match goal with + | [ |- context[-ident.cast _ (-?r) (-?v)] ] => rewrite (ident.cast_opp' r v) + | [ |- context[ident.cast ?coor ?r ?v] ] + => is_var v; + pose proof (@ident.cast_always_bounded coor r v); + generalize dependent (ident.cast coor r v); clear v; intro v; intros + | [ |- context[ident.cast ?coor ?r ?v] ] + => is_var v; is_var coor; + pose proof (@ident.cast_cases coor r v); + generalize dependent (ident.cast coor r v); intros + | [ H : is_bounded_by_bool ?v ?r = true, H' : is_tighter_than_bool ?r ?r' = true |- _ ] + => unique assert (is_bounded_by_bool v r' = true) by (eauto 2 using ZRange.is_bounded_by_of_is_tighter_than) + | [ H : is_bounded_by_bool (-?v) ?r = true, H' : (-?r <=? ?r')%zrange = true |- _ ] + => unique assert (is_bounded_by_bool v r' = true) + by (apply (@ZRange.is_bounded_by_of_is_tighter_than _ _ H'); + rewrite <- ZRange.is_bounded_by_bool_opp, ZRange.opp_involutive; exact H) + | [ H : is_bounded_by_bool ?v (-?r) = true |- _ ] + => is_var v; + unique assert (is_bounded_by_bool (-v) r = true) + by now rewrite <- ZRange.is_bounded_by_bool_move_opp_normalize, ZRange.normalize_opp + | [ H : is_bounded_by_bool ?x r[0~>?v-1] = true |- _ ] + => progress (try unique assert (0 <= x); try unique assert (x <= v - 1)); + [ clear -H; cbv [is_bounded_by_bool] in H; cbn [lower upper] in H; Bool.split_andb; Z.ltb_to_lt; lia.. + | ] + end + | progress cbn [expr.interp_related_gen] in * + | match goal with + | [ |- context[Z.shiftl] ] => rewrite Z.shiftl_mul_pow2 by auto with zarith + | [ |- context[Z.shiftr] ] => rewrite Z.shiftr_div_pow2 by auto with zarith + | [ |- context[Z.shiftl _ (-_)] ] => rewrite Z.shiftl_opp_r + | [ |- context[Z.land _ (Z.ones _)] ] => rewrite Z.land_ones by auto using Z.log2_nonneg + | [ |- context[- - _] ] => rewrite Z.opp_involutive + | [ H : ?x = 2^Z.log2 ?x |- context[2^Z.log2 ?x] ] => rewrite <- H + | [ H : ?x = 2^?n |- context[Z.land _ (?x - 1)] ] + => rewrite !Z.sub_1_r, H, <- Z.ones_equiv, Z.land_ones by auto with zarith + | [ |- _ = _ :> BinInt.Z ] => progress normalize_commutative_identifier Z.land Z.land_comm + | [ H : ?x = ?y, H' : ?x <> ?y |- _ ] => exfalso; apply H', H + | [ H : ?x = 2^Z.log2_up ?x - 1 |- context[2^Z.log2_up ?x - 1] ] => rewrite <- H + | [ H : ?x = 2^Z.log2 ?x, H' : context[2^Z.log2 ?x] |- _ = _ :> BinInt.Z ] + => rewrite <- H in H' + | [ |- _ = _ :> BinInt.Z ] => progress autorewrite with zsimplify_const + | [ H : 0 <= ?x, H' : ?x <= ?r - 1 |- context[?x mod ?r] ] + => rewrite (Z.mod_small x r) by (clear -H H'; lia) + | [ H : 0 <= ?x, H' : ?x <= ?y - 1 |- context[?x / ?y] ] + => rewrite (Z.div_small x y) by (clear -H H'; lia) + | [ H : ?x = 2^Z.log2 ?x |- _ ] + => unique assert (0 <= x) by (rewrite H; auto with zarith) + | [ |- _ mod ?x = _ mod ?x ] + => progress (push_Zmod; pull_Zmod) + | [ |- ?f (_ mod ?x) = ?f (_ mod ?x) ] + => progress (push_Zmod; pull_Zmod) + | [ |- _ mod ?x = _ mod ?x ] + => apply f_equal2; (lia + nia) + | _ => rewrite !Z.shiftl_mul_pow2 in * by auto using Z.log2_nonneg + | _ => rewrite !Z.land_ones in * by auto using Z.log2_nonneg + | H : ?x mod ?b * ?y <= _ + |- context [ (?x * ?y) mod ?b ] => + rewrite (PullPush.Z.mul_mod_l x y b); + rewrite (Z.mod_small (x mod b * y) b) by omega + | [ |- context[_ - ?x + ?x] ] => rewrite !Z.sub_add + | [ |- context[_ mod (2^_) * 2^_] ] => rewrite <- !Z.mul_mod_distr_r_full + | [ |- context[Z.land _ (Z.ones _)] ] => rewrite !Z.land_ones by lia + | [ |- context[2^?a * 2^?b] ] => rewrite <- !Z.pow_add_r by lia + | [ |- context[-?x + ?y] ] => rewrite !Z.add_opp_l + | [ |- context[?n + - ?m] ] => rewrite !Z.add_opp_r + | [ |- context[?n - - ?m] ] => rewrite !Z.sub_opp_r + | [ |- context[Zpos ?p * ?x / Zpos ?p] ] + => rewrite (@Z.div_mul' x (Zpos p)) in * by (clear; lia) + | [ H : context[Zpos ?p * ?x / Zpos ?p] |- _ ] + => rewrite (@Z.div_mul' x (Zpos p)) in * by (clear; lia) + | [ |- ?f (?a mod ?r) = ?f (?b mod ?r) ] => apply f_equal; apply f_equal2; lia + | [ |- context[-?a - ?b + ?c] ] => replace (-a - b + c) with (c - a - b) by (clear; lia) + | [ |- context[?x - ?y + ?z] ] + => lazymatch goal with + | [ |- context[z - y + x] ] + => progress replace (z - y + x) with (x - y + z) by (clear; lia) + end + | [ |- context[?x - ?y - ?z] ] + => lazymatch goal with + | [ |- context[x - z - y] ] + => progress replace (x - z - y) with (x - y - z) by (clear; lia) + end + | [ |- context[?x + ?y] ] + => lazymatch goal with + | [ |- context[y + x] ] + => progress replace (y + x) with (x + y) by (clear; lia) + end + | [ |- context[?x + ?y + ?z] ] + => lazymatch goal with + | [ |- context[x + z + y] ] + => progress replace (x + z + y) with (x + y + z) by (clear; lia) + | [ |- context[z + x + y] ] + => progress replace (z + x + y) with (x + y + z) by (clear; lia) + | [ |- context[z + y + x] ] + => progress replace (z + y + x) with (x + y + z) by (clear; lia) + | [ |- context[y + x + z] ] + => progress replace (y + x + z) with (x + y + z) by (clear; lia) + | [ |- context[y + z + x] ] + => progress replace (y + z + x) with (x + y + z) by (clear; lia) + end + | [ |- - ident.cast _ (-?r) (- (?x / ?y)) = ident.cast _ ?r (?x' / ?y) ] + => tryif constr_eq x x' then fail else replace x with x' by lia + | [ |- _ = _ :> BinInt.Z ] => progress autorewrite with zsimplify_fast + end ]. + +Local Ltac remove_casts := + repeat match goal with + | [ |- context[ident.cast _ r[?x~>?x] ?x] ] + => rewrite (ident.cast_in_bounds r[x~>x] x) by apply ZRange.is_bounded_by_bool_constant + | [ |- context[ident.cast _ ?r (ident.cast _ ?r _)] ] + => rewrite ident.cast_idempotent + | [ H : context[ident.cast _ ?r (ident.cast _ ?r _)] |- _ ] + => rewrite ident.cast_idempotent in H + | [ |- context[ident.cast ?coor ?r ?v] ] + => is_var v; + pose proof (@ident.cast_always_bounded coor r v); + generalize dependent (ident.cast coor r v); + clear v; intro v; intros + | [ H : context[ident.cast ?coor ?r ?v] |- _ ] + => is_var v; + pose proof (@ident.cast_always_bounded coor r v); + generalize dependent (ident.cast coor r v); + clear v; intro v; intros + | [ H : context[ZRange.constant ?v] |- _ ] => unique pose proof (ZRange.is_bounded_by_bool_normalize_constant v) + | [ H : is_tighter_than_bool (?ZRf ?r1 ?r2) (ZRange.normalize ?rs) = true, + H1 : is_bounded_by_bool ?v1 ?r1 = true, + H2 : is_bounded_by_bool ?v2 ?r2 = true + |- _ ] + => let cst := multimatch goal with + | [ |- context[ident.cast ?coor rs (?Zf v1 v2)] ] => constr:(ident.cast coor rs (Zf v1 v2)) + | [ H : context[ident.cast ?coor rs (?Zf v1 v2)] |- _ ] => constr:(ident.cast coor rs (Zf v1 v2)) + end in + lazymatch cst with + | ident.cast ?coor rs (?Zf v1 v2) + => let lem := lazymatch constr:((ZRf, Zf)%core) with + | (ZRange.shiftl, Z.shiftl)%core => constr:(@ZRange.is_bounded_by_bool_shiftl v1 r1 v2 r2 H1 H2) + | (ZRange.shiftr, Z.shiftr)%core => constr:(@ZRange.is_bounded_by_bool_shiftr v1 r1 v2 r2 H1 H2) + | (ZRange.land, Z.land)%core => constr:(@ZRange.is_bounded_by_bool_land v1 r1 v2 r2 H1 H2) + end in + try unique pose proof (@ZRange.is_bounded_by_of_is_tighter_than _ _ H _ lem); + clear H; + rewrite (@ident.cast_in_normalized_bounds coor rs (Zf v1 v2)) in * by assumption + end + | [ H : is_tighter_than_bool (?ZRf ?r1) (ZRange.normalize ?rs) = true, + H1 : is_bounded_by_bool ?v1 ?r1 = true + |- _ ] + => let cst := multimatch goal with + | [ |- context[ident.cast ?coor rs (?Zf v1)] ] => constr:(ident.cast coor rs (Zf v1)) + | [ H : context[ident.cast ?coor rs (?Zf v1)] |- _ ] => constr:(ident.cast coor rs (Zf v1)) + end in + lazymatch cst with + | ident.cast ?coor rs (?Zf v1) + => let lem := lazymatch constr:((ZRf, Zf)%core) with + | (ZRange.cc_m ?s, Z.cc_m ?s)%core => constr:(@ZRange.is_bounded_by_bool_cc_m s v1 r1 H1) + end in + try unique pose proof (@ZRange.is_bounded_by_of_is_tighter_than _ _ H _ lem); + clear H; + rewrite (@ident.cast_in_normalized_bounds coor rs (Zf v1)) in * by assumption + end + | [ H : is_bounded_by_bool ?v (ZRange.normalize ?r) = true |- context[ident.cast ?coor ?r ?v] ] + => rewrite (@ident.cast_in_normalized_bounds coor r v) in * by assumption + | [ H : is_bounded_by_bool ?v (ZRange.normalize ?r) = true, H' : context[ident.cast ?coor ?r ?v] |- _ ] + => rewrite (@ident.cast_in_normalized_bounds coor r v) in * by assumption + | [ H : is_bounded_by_bool ?v ?r = true, + H' : is_tighter_than_bool ?r r[0~>?x-1]%zrange = true, + H'' : Z.eqb ?x ?m = true + |- context[?v mod ?m] ] + => unique assert (is_bounded_by_bool v r[0~>x-1] = true) + by (eapply ZRange.is_bounded_by_of_is_tighter_than; eassumption) + | _ => progress Z.ltb_to_lt + | _ => progress subst + end. + +Local Lemma unfold_is_bounded_by_bool v r + : is_bounded_by_bool v r = true -> lower r <= v <= upper r. +Proof using Type. + cbv [is_bounded_by_bool]; intro; split_andb; Z.ltb_to_lt; split; assumption. +Qed. + +Local Lemma unfold_is_tighter_than_bool r1 r2 + : is_tighter_than_bool r1 r2 = true -> lower r2 <= lower r1 /\ upper r1 <= upper r2. +Proof using Type. + cbv [is_tighter_than_bool]; intro; split_andb; Z.ltb_to_lt; split; assumption. +Qed. + +Local Ltac unfold_cast_lemmas := + repeat match goal with + | [ H : context[ZRange.normalize (ZRange.constant _)] |- _ ] + => rewrite ZRange.normalize_constant in H + | [ H : is_bounded_by_bool _ (ZRange.normalize ?r) = true |- _ ] + => is_var r; generalize dependent (ZRange.normalize r); clear r; intro r; intros + | [ H : is_bounded_by_bool ?x (ZRange.constant ?x) = true |- _ ] + => clear H + | [ H : is_bounded_by_bool ?x ?r = true |- _ ] + => is_var r; apply unfold_is_bounded_by_bool in H + | [ H : is_bounded_by_bool ?x r[_~>_] = true |- _ ] + => apply unfold_is_bounded_by_bool in H + | [ H : is_tighter_than_bool r[_~>_] r[_~>_] = true |- _ ] + => apply unfold_is_tighter_than_bool in H + | _ => progress cbn [lower upper] in * + | [ H : context[lower ?r] |- _ ] + => is_var r; let l := fresh "l" in let u := fresh "u" in destruct r as [l u] + | [ H : context[upper ?r] |- _ ] + => is_var r; let l := fresh "l" in let u := fresh "u" in destruct r as [l u] + | _ => progress Z.ltb_to_lt + end. + +Local Ltac clear_useless_hyps := + repeat match goal with + | [ H : True |- _ ] => clear H + | [ H : unit |- _ ] => clear H + | [ H : nat |- _ ] => clear H + | [ H : Z |- _ ] => clear H + | [ H : zrange |- _ ] => clear H + | [ H : ?x = ?x |- _ ] => clear H + | [ H : ?x <= ?y <= ?z |- _ ] + => is_var x; is_var z; clear x z H + | [ H : ?x <= ?x' /\ ?y' <= ?y, H' : ?x' <= ?z <= ?y' |- _ ] + => is_var x'; is_var y'; + let H'' := fresh in + assert (H'' : x <= z <= y) by (clear -H H'; lia); + clear x' y' H H' + end. + +Local Ltac systematically_handle_casts := + remove_casts; unfold_cast_lemmas; clear_useless_hyps. + + +Local Ltac fin_with_nia := + lazymatch goal with + | [ |- ident.cast _ ?r _ = ident.cast _ ?r _ ] => apply f_equal; Z.div_mod_to_quot_rem; nia + | _ => reflexivity || (Z.div_mod_to_quot_rem; (lia + nia)) + end. + +Lemma arith_with_casts_rewrite_rules_proofs + : PrimitiveHList.hlist (@snd bool Prop) arith_with_casts_rewrite_rulesT. +Proof using Type. + start_proof; auto; intros; try lia. + all: repeat interp_good_t_step_related. + all: repeat interp_good_t_step_arith. + all: remove_casts; try fin_with_nia. +Qed. + +Lemma strip_literal_casts_rewrite_rules_proofs + : PrimitiveHList.hlist (@snd bool Prop) strip_literal_casts_rewrite_rulesT. +Proof using Type. + start_proof; auto; intros; remove_casts; reflexivity. +Qed. + +Section fancy. + Context (invert_low invert_high : Z (*log2wordmax*) -> Z -> option Z) + (value_range flag_range : zrange). + + Lemma fancy_rewrite_rules_proofs + : PrimitiveHList.hlist (@snd bool Prop) fancy_rewrite_rulesT. + Proof using Type. start_proof. Qed. + + Local Ltac fancy_local_t := + repeat match goal with + | [ H : forall s v v', ?invert_low s v = Some v' -> v = _, + H' : ?invert_low _ _ = Some _ |- _ ] => apply H in H' + | [ H : forall s v v', ?invert_low s v = Some v' -> v = _ |- _ ] + => clear invert_low H + | [ H : None <> None |- _ ] => exfalso; exact (H eq_refl) + end. + Local Ltac more_fancy_arith_t := repeat autorewrite with zsimplify in *. + + Lemma fancy_with_casts_rewrite_rules_proofs + (Hlow : forall s v v', invert_low s v = Some v' -> v = Z.land v' (2^(s/2)-1)) + (Hhigh : forall s v v', invert_high s v = Some v' -> v = Z.shiftr v' (s/2)) + : PrimitiveHList.hlist (@snd bool Prop) (@fancy_with_casts_rewrite_rulesT invert_low invert_high value_range flag_range). + Proof using Type. + start_proof; auto; intros; try lia. + Time all: repeat interp_good_t_step_related. + Time all: fancy_local_t. + Time all: try solve [ systematically_handle_casts; repeat interp_good_t_step_arith ]. + Qed. +End fancy. |