diff options
| author |  Jason Gross <jgross@mit.edu> | 2019-01-22 17:18:09 -0500 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2019-02-11 17:34:58 -0800 |
| commit | 974bb6d7ac3a7f007dd3b8655693f38a54154c2a (patch) | |
| tree | a55756d600fd51c0ca4d20e1337eb0ccb992ff4a /src/Rewriter.v | |
| parent | 8708ece69c47a3b176ee5dcd5656a66f2c98b42d (diff) | |
Insert casts before literals during bounds analysis
Unless we explicitly say not to. The ability to explicitly say not to
is required for, e.g., eta-expansion where we want to replace variable
lists of known length with with cons cells indexing into the variable
list, but don't want to pollute the code with casts.
Uniformity in this way allows rewrite rules to not blow up exponentially
(in the number of wildcards); we previously required a separate rewrite
rule for each way of choosing between wildcard and literal.
To preserve output of the pipeline, we add another pass that just strips
the casts off of literals at the end.
After | File Name | Before || Change | % Change
--------------------------------------------------------------------------------------------
20m27.24s | Total | 22m39.70s || -2m12.46s | -9.74%
--------------------------------------------------------------------------------------------
0m44.27s | Rewriter.vo | 2m11.58s || -1m27.31s | -66.35%
1m15.23s | RewriterRulesInterpGood.vo | 1m50.28s || -0m35.04s | -31.78%
1m40.19s | RewriterRulesGood.vo | 1m58.05s || -0m17.85s | -15.12%
0m26.99s | AbstractInterpretationProofs.vo | 0m16.91s || +0m10.07s | +59.60%
3m15.98s | p384_32.c | 3m07.78s || +0m08.19s | +4.36%
0m42.52s | ExtractionHaskell/word_by_word_montgomery | 0m44.60s || -0m02.07s | -4.66%
0m28.63s | ExtractionHaskell/unsaturated_solinas | 0m31.38s || -0m02.75s | -8.76%
0m21.76s | ExtractionHaskell/saturated_solinas | 0m24.56s || -0m02.79s | -11.40%
0m09.87s | ExtractionOCaml/unsaturated_solinas | 0m11.28s || -0m01.41s | -12.50%
1m59.22s | RewriterWf2.vo | 2m00.09s || -0m00.87s | -0.72%
1m07.03s | Fancy/Montgomery256.vo | 1m07.31s || -0m00.28s | -0.41%
0m52.60s | Fancy/Barrett256.vo | 0m53.16s || -0m00.55s | -1.05%
0m48.17s | RewriterInterpProofs1.vo | 0m48.72s || -0m00.54s | -1.12%
0m40.16s | AbstractInterpretationWf.vo | 0m40.23s || -0m00.07s | -0.17%
0m38.35s | p521_32.c | 0m38.26s || +0m00.09s | +0.23%
0m31.56s | p521_64.c | 0m31.53s || +0m00.02s | +0.09%
0m24.64s | RewriterWf1.vo | 0m24.01s || +0m00.62s | +2.62%
0m23.54s | AbstractInterpretationZRangeProofs.vo | 0m23.64s || -0m00.10s | -0.42%
0m23.48s | PushButtonSynthesis/WordByWordMontgomery.vo | 0m23.26s || +0m00.21s | +0.94%
0m20.92s | SlowPrimeSynthesisExamples.vo | 0m20.62s || +0m00.30s | +1.45%
0m19.92s | PushButtonSynthesis/UnsaturatedSolinas.vo | 0m19.80s || +0m00.12s | +0.60%
0m16.60s | ExtractionOCaml/word_by_word_montgomery | 0m17.56s || -0m00.95s | -5.46%
0m14.72s | p448_solinas_64.c | 0m14.66s || +0m00.06s | +0.40%
0m13.70s | secp256k1_32.c | 0m13.45s || +0m00.25s | +1.85%
0m13.68s | p256_32.c | 0m13.33s || +0m00.34s | +2.62%
0m13.28s | CStringification.vo | 0m13.26s || +0m00.01s | +0.15%
0m11.88s | p484_64.c | 0m11.74s || +0m00.14s | +1.19%
0m09.96s | ExtractionOCaml/word_by_word_montgomery.ml | 0m10.24s || -0m00.27s | -2.73%
0m07.47s | ExtractionOCaml/saturated_solinas | 0m07.93s || -0m00.46s | -5.80%
0m06.78s | BoundsPipeline.vo | 0m05.96s || +0m00.82s | +13.75%
0m06.72s | ExtractionOCaml/unsaturated_solinas.ml | 0m07.03s || -0m00.31s | -4.40%
0m06.38s | p224_32.c | 0m06.54s || -0m00.16s | -2.44%
0m06.21s | ExtractionHaskell/word_by_word_montgomery.hs | 0m06.34s || -0m00.12s | -2.05%
0m05.45s | p384_64.c | 0m05.18s || +0m00.27s | +5.21%
0m04.82s | ExtractionHaskell/unsaturated_solinas.hs | 0m04.84s || -0m00.01s | -0.41%
0m04.80s | ExtractionOCaml/saturated_solinas.ml | 0m05.07s || -0m00.27s | -5.32%
0m03.83s | ExtractionHaskell/saturated_solinas.hs | 0m04.07s || -0m00.24s | -5.89%
0m03.30s | PushButtonSynthesis/Primitives.vo | 0m03.31s || -0m00.01s | -0.30%
0m03.26s | PushButtonSynthesis/SmallExamples.vo | 0m03.24s || +0m00.01s | +0.61%
0m03.08s | PushButtonSynthesis/SaturatedSolinas.vo | 0m02.96s || +0m00.12s | +4.05%
0m02.16s | curve25519_32.c | 0m02.16s || +0m00.00s | +0.00%
0m01.57s | curve25519_64.c | 0m01.47s || +0m00.10s | +6.80%
0m01.40s | CLI.vo | 0m01.32s || +0m00.07s | +6.06%
0m01.27s | PushButtonSynthesis/MontgomeryReduction.vo | 0m01.19s || +0m00.08s | +6.72%
0m01.26s | StandaloneHaskellMain.vo | 0m01.18s || +0m00.08s | +6.77%
0m01.22s | PushButtonSynthesis/BarrettReduction.vo | 0m01.29s || -0m00.07s | -5.42%
0m01.13s | RewriterProofs.vo | 0m01.10s || +0m00.02s | +2.72%
0m01.10s | secp256k1_64.c | 0m01.01s || +0m00.09s | +8.91%
0m01.08s | StandaloneOCamlMain.vo | 0m01.13s || -0m00.04s | -4.42%
0m01.06s | p256_64.c | 0m01.02s || +0m00.04s | +3.92%
0m01.05s | AbstractInterpretation.vo | 0m01.00s || +0m00.05s | +5.00%
0m01.00s | CompilersTestCases.vo | 0m01.08s || -0m00.08s | -7.40%
0m01.00s | p224_64.c | 0m01.00s || +0m00.00s | +0.00%
Diffstat (limited to 'src/Rewriter.v')
| -rw-r--r-- | src/Rewriter.v | 506 |
1 files changed, 193 insertions, 313 deletions
diff --git a/src/Rewriter.v b/src/Rewriter.v index 5f10869b2..a79bcb18f 100644 --- a/src/Rewriter.v +++ b/src/Rewriter.v @@ -359,6 +359,7 @@ Module Compilers. Notation "x 'mod' y" := (#ident.Z_modulo @ x @ y)%pattern : pattern_scope. Notation "- x" := (#ident.Z_opp @ x) : pattern_scope. + Notation "#?ℤ'" := (#ident.Z_cast @ #?ℤ) : pattern_scope. Notation "??'" := (#ident.Z_cast @ Wildcard _) : pattern_scope. Notation "x -' y" := (#ident.Z_cast @ (#ident.Z_sub @ x @ y)) : pattern_scope. Notation "x +' y" := (#ident.Z_cast @ (#ident.Z_add @ x @ y)) : pattern_scope. @@ -1747,34 +1748,34 @@ Module Compilers. Definition arith_with_casts_rewrite_rules : rewrite_rulesT := [make_rewrite (#(@pattern.ident.fst '1 '2) @ (??, ??)) (fun _ _ x y => x) - ; make_rewrite (#(@pattern.ident.snd '1 '2) @ (??, ??)) (fun _ x _ y => y) + ; make_rewrite (#(@pattern.ident.snd '1 '2) @ (??, ??)) (fun _ _ x y => y) - ; make_rewriteo (??') (fun r v => ##(lower r) when lower r =? upper r) + ; make_rewriteo (??') (fun r v => cst r (##(lower r)) when lower r =? upper r) ; make_rewriteo - (#?ℤ +' ??') - (fun rp z rv v => cst rv v when (z =? 0) && (ZRange.normalize rv <=? ZRange.normalize rp)%zrange) + (#?ℤ' + ?? ) + (fun rz z v => v when (z =? 0) && (is_bounded_by_bool z (ZRange.normalize rz))) ; make_rewriteo - (??' +' #?ℤ ) - (fun rp rv v z => cst rv v when (z =? 0) && (ZRange.normalize rv <=? ZRange.normalize rp)%zrange) + (?? + #?ℤ') + (fun v rz z => v when (z =? 0) && (is_bounded_by_bool z (ZRange.normalize rz))) ; make_rewriteo - (#?ℤ - (-'??')) - (fun z rnv rv v => cst rv v when (z =? 0) && (ZRange.normalize rv <=? -ZRange.normalize rnv)%zrange) - ; make_rewriteo (#?ℤ - ?? ) (fun z v => -v when z =? 0) + (#?ℤ' - (-'??')) + (fun rz z rnv rv v => cst rv v when (z =? 0) && (ZRange.normalize rv <=? -ZRange.normalize rnv)%zrange && (is_bounded_by_bool z rz)) + ; make_rewriteo (#?ℤ' - ?? ) (fun rz z v => -v when (z =? 0) && is_bounded_by_bool z (ZRange.normalize rz)) - ; make_rewriteo (#?ℤ << ??) (fun x y => ##0 when x =? 0) + ; make_rewriteo (#?ℤ' << ??) (fun rx x y => ##0 when (x =? 0) && is_bounded_by_bool x (ZRange.normalize rx)) ; make_rewriteo (-(-'??')) (fun rnv rv v => cst rv v when (ZRange.normalize rv <=? -ZRange.normalize rnv)%zrange) - ; make_rewriteo (#pattern.ident.Z_mul_split @ #?ℤ @ #?ℤ @ ??) (fun s xx y => (##0, ##0)%Z when xx =? 0) - ; make_rewriteo (#pattern.ident.Z_mul_split @ #?ℤ @ ?? @ #?ℤ) (fun s y xx => (##0, ##0)%Z when xx =? 0) + ; make_rewriteo (#pattern.ident.Z_mul_split @ ?? @ #?ℤ' @ ??) (fun s rxx xx y => (cst r[0~>0] ##0, cst r[0~>0] ##0)%Z when (xx =? 0) && is_bounded_by_bool xx (ZRange.normalize rxx)) + ; make_rewriteo (#pattern.ident.Z_mul_split @ ?? @ ?? @ #?ℤ') (fun s y rxx xx => (cst r[0~>0] ##0, cst r[0~>0] ##0)%Z when (xx =? 0) && is_bounded_by_bool xx (ZRange.normalize rxx)) ; make_rewriteo - (#pattern.ident.Z_mul_split @ #?ℤ @ #?ℤ @ ??') - (fun s xx ry y => (cst ry y, ##0)%Z when (xx =? 1) && (ZRange.normalize ry <=? r[0~>s-1])%zrange) + (#pattern.ident.Z_mul_split @ #?ℤ' @ #?ℤ' @ ??') + (fun rs s rxx xx ry y => (cst ry y, cst r[0~>0] ##0)%Z when (xx =? 1) && (ZRange.normalize ry <=? r[0~>s-1])%zrange && is_bounded_by_bool s (ZRange.normalize rs) && is_bounded_by_bool xx (ZRange.normalize rxx)) ; make_rewriteo - (#pattern.ident.Z_mul_split @ #?ℤ @ ??' @ #?ℤ) - (fun s ry y xx => (cst ry y, ##0)%Z when (xx =? 1) && (ZRange.normalize ry <=? r[0~>s-1])%zrange) + (#pattern.ident.Z_mul_split @ #?ℤ' @ ??' @ #?ℤ') + (fun rs s ry y rxx xx => (cst ry y, cst r[0~>0] ##0)%Z when (xx =? 1) && (ZRange.normalize ry <=? r[0~>s-1])%zrange && is_bounded_by_bool s (ZRange.normalize rs) && is_bounded_by_bool xx (ZRange.normalize rxx)) (* ; make_rewriteo (#pattern.ident.Z_mul_split @ #?ℤ @ #?ℤ @ ??') @@ -1796,14 +1797,14 @@ Module Compilers. => (llet2_opp2 rvc (#ident.Z_sub_get_borrow @ s @ x @ cst ry y)) when (ZRange.normalize ry <=? -ZRange.normalize rny)%zrange) ; make_rewriteol - (#pattern.ident.Z_cast2 @ (#pattern.ident.Z_add_get_carry @ ?? @ #?ℤ @ ??)) - (fun rvc s yy x - => (llet2_opp2 rvc (#ident.Z_sub_get_borrow @ s @ x @ ##(-yy)%Z)) - when yy <? 0) + (#pattern.ident.Z_cast2 @ (#pattern.ident.Z_add_get_carry @ ?? @ #?ℤ' @ ??)) + (fun rvc s ryy yy x + => (llet2_opp2 rvc (#ident.Z_sub_get_borrow @ s @ x @ cst (ZRange.opp ryy) ##(-yy)%Z)) + when (yy <? 0) && is_bounded_by_bool yy (ZRange.normalize ryy)) ; make_rewriteol - (#pattern.ident.Z_cast2 @ (#pattern.ident.Z_add_get_carry @ ?? @ ?? @ #?ℤ)) - (fun rvc s x yy => (llet2_opp2 rvc (#ident.Z_sub_get_borrow @ s @ x @ ##(-yy)%Z)) - when yy <? 0) + (#pattern.ident.Z_cast2 @ (#pattern.ident.Z_add_get_carry @ ?? @ ?? @ #?ℤ')) + (fun rvc s x ryy yy => (llet2_opp2 rvc (#ident.Z_sub_get_borrow @ s @ x @ cst (ZRange.opp ryy) ##(-yy)%Z)) + when (yy <? 0) && is_bounded_by_bool yy (ZRange.normalize ryy)) ; make_rewriteol @@ -1817,82 +1818,82 @@ Module Compilers. => (llet2_opp2 rvc (#ident.Z_sub_with_get_borrow @ s @ (cst rc c) @ x @ (cst ry y))) when ((ZRange.normalize ry <=? -ZRange.normalize rny) && (ZRange.normalize rc <=? -ZRange.normalize rnc))%zrange) ; make_rewriteol - (#pattern.ident.Z_cast2 @ (#pattern.ident.Z_add_with_get_carry @ ?? @ #?ℤ @ (-'??') @ ??)) - (fun rvc s cc rny ry y x + (#pattern.ident.Z_cast2 @ (#pattern.ident.Z_add_with_get_carry @ ?? @ #?ℤ' @ (-'??') @ ??)) + (fun rvc s rcc cc rny ry y x => (llet2_opp2 rvc (#ident.Z_sub_get_borrow @ s @ x @ cst ry y)) - when (cc =? 0) && (ZRange.normalize ry <=? -ZRange.normalize rny)%zrange) + when (cc =? 0) && (ZRange.normalize ry <=? -ZRange.normalize rny)%zrange && is_bounded_by_bool cc (ZRange.normalize rcc)) ; make_rewriteol - (#pattern.ident.Z_cast2 @ (#pattern.ident.Z_add_with_get_carry @ ?? @ #?ℤ @ (-'??') @ ??)) - (fun rvc s cc rny ry y x - => (llet2_opp2 rvc (#ident.Z_sub_with_get_borrow @ s @ ##(-cc)%Z @ x @ cst ry y)) - when (cc <? 0) && (ZRange.normalize ry <=? -ZRange.normalize rny)%zrange) + (#pattern.ident.Z_cast2 @ (#pattern.ident.Z_add_with_get_carry @ ?? @ #?ℤ' @ (-'??') @ ??)) + (fun rvc s rcc cc rny ry y x + => (llet2_opp2 rvc (#ident.Z_sub_with_get_borrow @ s @ cst (ZRange.opp rcc) ##(-cc)%Z @ x @ cst ry y)) + when (cc <? 0) && (ZRange.normalize ry <=? -ZRange.normalize rny)%zrange && is_bounded_by_bool cc (ZRange.normalize rcc)) ; make_rewriteol - (#pattern.ident.Z_cast2 @ (#pattern.ident.Z_add_with_get_carry @ ?? @ #?ℤ @ ?? @ (-'??'))) - (fun rvc s cc x rny ry y + (#pattern.ident.Z_cast2 @ (#pattern.ident.Z_add_with_get_carry @ ?? @ #?ℤ' @ ?? @ (-'??'))) + (fun rvc s rcc cc x rny ry y => (llet2_opp2 rvc (#ident.Z_sub_get_borrow @ s @ x @ cst ry y)) - when (cc =? 0) && (ZRange.normalize ry <=? -ZRange.normalize rny)%zrange) + when (cc =? 0) && (ZRange.normalize ry <=? -ZRange.normalize rny)%zrange && is_bounded_by_bool cc (ZRange.normalize rcc)) ; make_rewriteol - (#pattern.ident.Z_cast2 @ (#pattern.ident.Z_add_with_get_carry @ ?? @ #?ℤ @ ?? @ (-'??'))) - (fun rvc s cc x rny ry y - => (llet2_opp2 rvc (#ident.Z_sub_with_get_borrow @ s @ ##(-cc)%Z @ x @ cst ry y)) - when (cc <? 0) && (ZRange.normalize ry <=? -ZRange.normalize rny)%zrange) + (#pattern.ident.Z_cast2 @ (#pattern.ident.Z_add_with_get_carry @ ?? @ #?ℤ' @ ?? @ (-'??'))) + (fun rvc s rcc cc x rny ry y + => (llet2_opp2 rvc (#ident.Z_sub_with_get_borrow @ s @ cst (ZRange.opp rcc) ##(-cc)%Z @ x @ cst ry y) + when (cc <? 0) && (ZRange.normalize ry <=? -ZRange.normalize rny)%zrange && is_bounded_by_bool cc (ZRange.normalize rcc))) ; make_rewriteol - (#pattern.ident.Z_cast2 @ (#pattern.ident.Z_add_with_get_carry @ ?? @ (-'??') @ #?ℤ @ ??)) - (fun rvc s rnc rc c yy x - => (llet2_opp2 rvc (#ident.Z_sub_with_get_borrow @ s @ cst rc c @ x @ ##(-yy)%Z)) - when (yy <=? 0) && (ZRange.normalize rc <=? -ZRange.normalize rnc)%zrange) + (#pattern.ident.Z_cast2 @ (#pattern.ident.Z_add_with_get_carry @ ?? @ (-'??') @ #?ℤ' @ ??)) + (fun rvc s rnc rc c ryy yy x + => (llet2_opp2 rvc (#ident.Z_sub_with_get_borrow @ s @ cst rc c @ x @ cst (ZRange.opp ryy) ##(-yy)%Z)) + when (yy <=? 0) && (ZRange.normalize rc <=? -ZRange.normalize rnc)%zrange && is_bounded_by_bool yy (ZRange.normalize ryy)) ; make_rewriteol - (#pattern.ident.Z_cast2 @ (#pattern.ident.Z_add_with_get_carry @ ?? @ (-'??') @ ?? @ #?ℤ)) - (fun rvc s rnc rc c x yy - => (llet2_opp2 rvc (#ident.Z_sub_with_get_borrow @ s @ cst rc c @ x @ ##(-yy)%Z)) - when (yy <=? 0) && (ZRange.normalize rc <=? -ZRange.normalize rnc)%zrange) + (#pattern.ident.Z_cast2 @ (#pattern.ident.Z_add_with_get_carry @ ?? @ (-'??') @ ?? @ #?ℤ')) + (fun rvc s rnc rc c x ryy yy + => (llet2_opp2 rvc (#ident.Z_sub_with_get_borrow @ s @ cst rc c @ x @ cst (ZRange.opp ryy) ##(-yy)%Z)) + when (yy <=? 0) && (ZRange.normalize rc <=? -ZRange.normalize rnc)%zrange && is_bounded_by_bool yy (ZRange.normalize ryy)) ; make_rewriteol - (#pattern.ident.Z_cast2 @ (#pattern.ident.Z_add_with_get_carry @ ?? @ #?ℤ @ #?ℤ @ ??)) - (fun rvc s cc yy x - => (llet2_opp2 rvc (#ident.Z_sub_with_get_borrow @ s @ ##(-cc)%Z @ x @ ##(-yy)%Z)) - when (yy <=? 0) && (cc <=? 0) && ((yy + cc) <? 0)) (* at least one must be strictly negative *) + (#pattern.ident.Z_cast2 @ (#pattern.ident.Z_add_with_get_carry @ ?? @ #?ℤ' @ #?ℤ' @ ??)) + (fun rvc s rcc cc ryy yy x + => (llet2_opp2 rvc (#ident.Z_sub_with_get_borrow @ s @ cst (ZRange.opp rcc) ##(-cc)%Z @ x @ cst (ZRange.opp ryy) ##(-yy)%Z)) + when (yy <=? 0) && (cc <=? 0) && ((yy + cc) <? 0) && is_bounded_by_bool yy (ZRange.normalize ryy) && is_bounded_by_bool cc (ZRange.normalize rcc)) (* at least one must be strictly negative *) ; make_rewriteol - (#pattern.ident.Z_cast2 @ (#pattern.ident.Z_add_with_get_carry @ ?? @ #?ℤ @ ?? @ #?ℤ)) - (fun rvc s cc x yy - => (llet2_opp2 rvc (#ident.Z_sub_with_get_borrow @ s @ ##(-cc)%Z @ x @ ##(-yy)%Z)) - when (yy <=? 0) && (cc <=? 0) && ((yy + cc) <? 0)) (* at least one must be strictly negative *) + (#pattern.ident.Z_cast2 @ (#pattern.ident.Z_add_with_get_carry @ ?? @ #?ℤ' @ ?? @ #?ℤ')) + (fun rvc s rcc cc x ryy yy + => (llet2_opp2 rvc (#ident.Z_sub_with_get_borrow @ s @ cst (ZRange.opp rcc) ##(-cc)%Z @ x @ cst (ZRange.opp ryy) ##(-yy)%Z)) + when (yy <=? 0) && (cc <=? 0) && ((yy + cc) <? 0) && is_bounded_by_bool yy (ZRange.normalize ryy) && is_bounded_by_bool cc (ZRange.normalize rcc)) (* at least one must be strictly negative *) - ; make_rewrite - (#pattern.ident.Z_add_get_carry @ #?ℤ @ #?ℤ @ #?ℤ) - (fun s xx yy => ##(Z.add_get_carry_full s xx yy)) ; make_rewriteo - (#pattern.ident.Z_add_get_carry @ #?ℤ @ #?ℤ @ ??') - (fun s xx ry y => (cst ry y, ##0) when (xx =? 0) && (ZRange.normalize ry <=? r[0~>s-1])%zrange) + (#pattern.ident.Z_add_get_carry @ #?ℤ' @ #?ℤ' @ #?ℤ') + (fun rs s rxx xx ryy yy => ##(Z.add_get_carry_full s xx yy) when is_bounded_by_bool s (ZRange.normalize rs) && is_bounded_by_bool xx (ZRange.normalize rxx) && is_bounded_by_bool yy (ZRange.normalize ryy)) + ; make_rewriteo + (#pattern.ident.Z_add_get_carry @ #?ℤ' @ #?ℤ' @ ??') + (fun rs s rxx xx ry y => (cst ry y, cst r[0~>0] ##0) when (xx =? 0) && (ZRange.normalize ry <=? r[0~>s-1])%zrange && is_bounded_by_bool xx (ZRange.normalize rxx) && is_bounded_by_bool s (ZRange.normalize rs)) ; make_rewriteo - (#pattern.ident.Z_add_get_carry @ #?ℤ @ ??' @ #?ℤ) - (fun s ry y xx => (cst ry y, ##0) when (xx =? 0) && (ZRange.normalize ry <=? r[0~>s-1])%zrange) + (#pattern.ident.Z_add_get_carry @ #?ℤ' @ ??' @ #?ℤ') + (fun rs s ry y rxx xx => (cst ry y, cst r[0~>0] ##0) when (xx =? 0) && (ZRange.normalize ry <=? r[0~>s-1])%zrange && is_bounded_by_bool xx (ZRange.normalize rxx) && is_bounded_by_bool s (ZRange.normalize rs)) - ; make_rewriteo (#pattern.ident.Z_add_with_carry @ #?ℤ @ ?? @ ??) (fun cc x y => x + y when cc =? 0) + ; make_rewriteo (#pattern.ident.Z_add_with_carry @ #?ℤ' @ ?? @ ??) (fun rcc cc x y => x + y when (cc =? 0) && is_bounded_by_bool cc (ZRange.normalize rcc)) (*; make_rewrite_step (#pattern.ident.Z_add_with_carry @ ?? @ ?? @ ??) (fun x y z => $x + $y + $z)*) - ; make_rewrite - (#pattern.ident.Z_add_with_get_carry @ #?ℤ @ #?ℤ @ #?ℤ @ #?ℤ) - (fun s cc xx yy => ##(Z.add_with_get_carry_full s cc xx yy)) ; make_rewriteo - (#pattern.ident.Z_add_with_get_carry @ #?ℤ @ #?ℤ @ #?ℤ @ ??') - (fun s cc xx ry y => (cst ry y, ##0) when (cc =? 0) && (xx =? 0) && (ZRange.normalize ry <=? r[0~>s-1])%zrange) + (#pattern.ident.Z_add_with_get_carry @ #?ℤ' @ #?ℤ' @ #?ℤ' @ #?ℤ') + (fun rs s rcc cc rxx xx ryy yy => ##(Z.add_with_get_carry_full s cc xx yy) when is_bounded_by_bool s (ZRange.normalize rs) && is_bounded_by_bool cc (ZRange.normalize rcc) && is_bounded_by_bool xx (ZRange.normalize rxx) && is_bounded_by_bool yy (ZRange.normalize ryy)) ; make_rewriteo - (#pattern.ident.Z_add_with_get_carry @ #?ℤ @ #?ℤ @ ??' @ #?ℤ) - (fun s cc ry y xx => (cst ry y, ##0) when (cc =? 0) && (xx =? 0) && (ZRange.normalize ry <=? r[0~>s-1])%zrange) + (#pattern.ident.Z_add_with_get_carry @ #?ℤ' @ #?ℤ' @ #?ℤ' @ ??') + (fun rs s rcc cc rxx xx ry y => (cst ry y, cst r[0~>0] ##0) when (cc =? 0) && (xx =? 0) && (ZRange.normalize ry <=? r[0~>s-1])%zrange && is_bounded_by_bool s (ZRange.normalize rs) && is_bounded_by_bool cc (ZRange.normalize rcc) && is_bounded_by_bool xx (ZRange.normalize rxx)) + ; make_rewriteo + (#pattern.ident.Z_add_with_get_carry @ #?ℤ' @ #?ℤ' @ ??' @ #?ℤ') + (fun rs s rcc cc ry y rxx xx => (cst ry y, cst r[0~>0] ##0) when (cc =? 0) && (xx =? 0) && (ZRange.normalize ry <=? r[0~>s-1])%zrange && is_bounded_by_bool s (ZRange.normalize rs) && is_bounded_by_bool cc (ZRange.normalize rcc) && is_bounded_by_bool xx (ZRange.normalize rxx)) (*; make_rewriteo (#pattern.ident.Z_add_with_get_carry @ ?? @ ?? @ #?ℤ @ #?ℤ) (fun s c xx yy => (c, ##0) when (xx =? 0) && (yy =? 0))*) ; make_rewriteol (* carry = 0: ADC x y -> ADD x y *) - (#pattern.ident.Z_cast2 @ (#pattern.ident.Z_add_with_get_carry @ ?? @ #?ℤ @ ?? @ ??)) - (fun rvc s cc x y + (#pattern.ident.Z_cast2 @ (#pattern.ident.Z_add_with_get_carry @ ?? @ #?ℤ' @ ?? @ ??)) + (fun rvc s rcc cc x y => (llet2 rvc (#ident.Z_add_get_carry @ s @ x @ y)) - when cc =? 0) + when (cc =? 0) && is_bounded_by_bool cc (ZRange.normalize rcc)) ; make_rewriteol (* ADC 0 0 -> (ADX 0 0, 0) *) (* except we don't do ADX, because C stringification doesn't handle it *) - (#pattern.ident.Z_cast2 @ (#pattern.ident.Z_add_with_get_carry @ #?ℤ @ ??' @ #?ℤ @ #?ℤ)) - (fun rvc s rc c xx yy - => (llet vc := cst2 rvc (#ident.Z_add_with_get_carry @ ##s @ cst rc c @ ##xx @ ##yy) in - (cst (fst rvc) (#ident.fst @ cst2 rvc ($vc)), ##0)) - when (xx =? 0) && (yy =? 0) && (ZRange.normalize rc <=? r[0~>s-1])%zrange && is_bounded_by_bool 0 (snd rvc)) + (#pattern.ident.Z_cast2 @ (#pattern.ident.Z_add_with_get_carry @ #?ℤ' @ ??' @ #?ℤ' @ #?ℤ')) + (fun rvc rs s rc c rxx xx ryy yy + => (llet vc := cst2 rvc (#ident.Z_add_with_get_carry @ cst rs ##s @ cst rc c @ cst rxx ##xx @ cst ryy ##yy) in + (cst (fst rvc) (#ident.fst @ cst2 rvc ($vc)), cst r[0~>0] ##0)) + when (xx =? 0) && (yy =? 0) && (ZRange.normalize rc <=? r[0~>s-1])%zrange && is_bounded_by_bool 0 (snd rvc) && is_bounded_by_bool s (ZRange.normalize rs) && is_bounded_by_bool xx (ZRange.normalize rxx) && is_bounded_by_bool yy (ZRange.normalize ryy)) (* let-bind any adc/sbb/mulx *) @@ -1916,8 +1917,6 @@ Module Compilers. (#pattern.ident.Z_cast2 @ (#pattern.ident.Z_mul_split @ ?? @ ?? @ ??)) (fun rvc s x y => llet2 rvc (#ident.Z_mul_split @ s @ x @ y)) - ; make_rewriteo (#pattern.ident.Z_cast @ #?ℤ) (fun r v => ##v when is_bounded_by_bool v r) - ; make_rewrite_step (#pattern.ident.Z_cast2 @ (??, ??)) (fun r v1 v2 => (#(ident.Z_cast (fst r)) @ $v1, #(ident.Z_cast (snd r)) @ $v2)) ; make_rewriteo @@ -1925,22 +1924,31 @@ Module Compilers. (fun r1 r2 x => #(ident.Z_cast r2) @ x when ZRange.is_tighter_than_bool (ZRange.normalize r2) (ZRange.normalize r1)) ]. + Definition strip_literal_casts_rewrite_rules : rewrite_rulesT + := [make_rewriteo (#?ℤ') (fun rx x => ##x when is_bounded_by_bool x (ZRange.normalize rx))]. + + Definition nbe_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 nbe_rewrite_rules. Definition arith_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 (arith_rewrite_rules 0%Z (* dummy val *)). Definition arith_with_casts_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 arith_with_casts_rewrite_rules. + Definition strip_literal_casts_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 strip_literal_casts_rewrite_rules. Definition nbe_dtree : decision_tree := Eval compute in invert_Some nbe_dtree'. Definition arith_dtree : decision_tree := Eval compute in invert_Some arith_dtree'. Definition arith_with_casts_dtree : decision_tree := Eval compute in invert_Some arith_with_casts_dtree'. + Definition strip_literal_casts_dtree : decision_tree + := Eval compute in invert_Some strip_literal_casts_dtree'. Definition nbe_default_fuel := Eval compute in List.length nbe_rewrite_rules. Definition arith_default_fuel := Eval compute in List.length (arith_rewrite_rules 0%Z (* dummy val *)). Definition arith_with_casts_default_fuel := Eval compute in List.length arith_with_casts_rewrite_rules. + Definition strip_literal_casts_default_fuel := Eval compute in List.length strip_literal_casts_rewrite_rules. Import PrimitiveHList. (* N.B. The [combine_hlist] call MUST eta-expand @@ -1968,12 +1976,18 @@ Module Compilers. Definition arith_with_casts_pr1_rewrite_rules := Eval hnf in projT1 arith_with_casts_split_rewrite_rules. Definition arith_with_casts_pr2_rewrite_rules := Eval hnf in projT2 arith_with_casts_split_rewrite_rules. Definition arith_with_casts_all_rewrite_rules := combine_hlist (P:=rewrite_ruleTP) (arith_with_casts_pr1_rewrite_rules) arith_with_casts_pr2_rewrite_rules. + Definition strip_literal_casts_split_rewrite_rules := Eval cbv [split_list projT1 projT2 strip_literal_casts_rewrite_rules] in split_list strip_literal_casts_rewrite_rules. + Definition strip_literal_casts_pr1_rewrite_rules := Eval hnf in projT1 strip_literal_casts_split_rewrite_rules. + Definition strip_literal_casts_pr2_rewrite_rules := Eval hnf in projT2 strip_literal_casts_split_rewrite_rules. + Definition strip_literal_casts_all_rewrite_rules := combine_hlist (P:=rewrite_ruleTP) (strip_literal_casts_pr1_rewrite_rules) strip_literal_casts_pr2_rewrite_rules. Definition nbe_rewrite_head0 do_again {t} (idc : ident t) : value_with_lets t := @assemble_identifier_rewriters nbe_dtree nbe_all_rewrite_rules do_again t idc. Definition arith_rewrite_head0 max_const_val do_again {t} (idc : ident t) : value_with_lets t := @assemble_identifier_rewriters arith_dtree (arith_all_rewrite_rules max_const_val) do_again t idc. Definition arith_with_casts_rewrite_head0 do_again {t} (idc : ident t) : value_with_lets t := @assemble_identifier_rewriters arith_with_casts_dtree arith_with_casts_all_rewrite_rules do_again t idc. + Definition strip_literal_casts_rewrite_head0 do_again {t} (idc : ident t) : value_with_lets t + := @assemble_identifier_rewriters strip_literal_casts_dtree strip_literal_casts_all_rewrite_rules do_again t idc. Section fancy. Context (invert_low invert_high : Z (*log2wordmax*) -> Z -> option Z) @@ -1996,6 +2010,7 @@ Module Compilers. 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_rules : rewrite_rulesT := [ @@ -2007,42 +2022,24 @@ Module Compilers. (Z.add_get_carry_concrete 2^256) @@ (?x, ?y) --> (add 0) @@ (y, x) *) make_rewriteo - (pcst2 (#pattern.ident.Z_add_get_carry @ #?ℤ @ ??' @ (pcst (#pattern.ident.Z_shiftl @ (pcst (#pattern.ident.Z_land @ ??' @ #?ℤ)) @ #?ℤ)))) - (fun '((r1, r2)%core) s rx x rshiftl rland ry y mask offset => cst2 (r1, r2)%core (#(ident.fancy_add (Z.log2 s) offset) @ (cst rx x, cst ry y)) when (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) && (offset <=? Z.log2 s)) - ; make_rewriteo - (pcst2 (#pattern.ident.Z_add_get_carry @ #?ℤ @ #?ℤ @ (pcst (#pattern.ident.Z_shiftl @ (pcst (#pattern.ident.Z_land @ ??' @ #?ℤ)) @ #?ℤ)))) - (fun '((r1, r2)%core) s xx rshiftl rland ry y mask offset => cst2 (r1, r2)%core (#(ident.fancy_add (Z.log2 s) offset) @ (##xx, cst ry y)) when (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) && (offset <=? Z.log2 s)) + (pcst2 (#pattern.ident.Z_add_get_carry @ #?ℤ' @ ??' @ (pcst (#pattern.ident.Z_shiftl @ (pcst (#pattern.ident.Z_land @ ??' @ #?ℤ')) @ #?ℤ')))) + (fun '((r1, r2)%core) rs s rx x rshiftl rland ry y rmask mask roffset offset => cst2 (r1, r2)%core (#(ident.fancy_add (Z.log2 s) offset) @ (cst rx x, cst ry y)) when (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) && (offset <=? Z.log2 s) && lit_good s rs && lit_good mask rmask && lit_good offset roffset) ; make_rewriteo - (pcst2 (#pattern.ident.Z_add_get_carry @ #?ℤ @ (pcst (#pattern.ident.Z_shiftl @ (pcst (#pattern.ident.Z_land @ ??' @ #?ℤ)) @ #?ℤ)) @ ??')) - (fun '((r1, r2)%core) s rshiftl rland ry y mask offset rx x => cst2 (r1, r2)%core (#(ident.fancy_add (Z.log2 s) offset) @ (cst rx x, cst ry y)) when (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) && (offset <=? Z.log2 s)) - ; make_rewriteo - (pcst2 (#pattern.ident.Z_add_get_carry @ #?ℤ @ (pcst (#pattern.ident.Z_shiftl @ (pcst (#pattern.ident.Z_land @ ??' @ #?ℤ)) @ #?ℤ)) @ #?ℤ)) - (fun '((r1, r2)%core) s rshiftl rland ry y mask offset xx => cst2 (r1, r2)%core (#(ident.fancy_add (Z.log2 s) offset) @ (##xx, cst ry y)) when (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) && (offset <=? Z.log2 s)) + (pcst2 (#pattern.ident.Z_add_get_carry @ #?ℤ' @ (pcst (#pattern.ident.Z_shiftl @ (pcst (#pattern.ident.Z_land @ ??' @ #?ℤ')) @ #?ℤ')) @ ??')) + (fun '((r1, r2)%core) rs s rshiftl rland ry y rmask mask roffset offset rx x => cst2 (r1, r2)%core (#(ident.fancy_add (Z.log2 s) offset) @ (cst rx x, cst ry y)) when (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) && (offset <=? Z.log2 s) && lit_good s rs && lit_good mask rmask && lit_good offset roffset) ; make_rewriteo - (pcst2 (#pattern.ident.Z_add_get_carry @ #?ℤ @ ??' @ (pcst (#pattern.ident.Z_shiftr @ ??' @ #?ℤ)))) - (fun '((r1, r2)%core) s rx x rshiftr ry y offset => cst2 (r1, r2)%core (#(ident.fancy_add (Z.log2 s) (-offset)) @ (cst rx x, cst ry y)) when (s =? 2^Z.log2 s) && shiftr_good rshiftr ry offset && range_in_bitwidth rshiftr s) - ; make_rewriteo - (pcst2 (#pattern.ident.Z_add_get_carry @ #?ℤ @ #?ℤ @ (pcst (#pattern.ident.Z_shiftr @ ??' @ #?ℤ)))) - (fun '((r1, r2)%core) s xx rshiftr ry y offset => cst2 (r1, r2)%core (#(ident.fancy_add (Z.log2 s) (-offset)) @ (##xx, cst ry y)) when (s =? 2^Z.log2 s) && shiftr_good rshiftr ry offset && range_in_bitwidth rshiftr s) + (pcst2 (#pattern.ident.Z_add_get_carry @ #?ℤ' @ ??' @ (pcst (#pattern.ident.Z_shiftr @ ??' @ #?ℤ')))) + (fun '((r1, r2)%core) rs s rx x rshiftr ry y roffset offset => cst2 (r1, r2)%core (#(ident.fancy_add (Z.log2 s) (-offset)) @ (cst rx x, cst ry y)) when (s =? 2^Z.log2 s) && shiftr_good rshiftr ry offset && range_in_bitwidth rshiftr s && lit_good s rs && lit_good offset roffset) ; make_rewriteo - (pcst2 (#pattern.ident.Z_add_get_carry @ #?ℤ @ pcst (#pattern.ident.Z_shiftr @ ??' @ #?ℤ) @ ??')) - (fun '((r1, r2)%core) s rshiftr ry y offset rx x => cst2 (r1, r2)%core (#(ident.fancy_add (Z.log2 s) (-offset)) @ (cst rx x, cst ry y)) when (s =? 2^Z.log2 s) && shiftr_good rshiftr ry offset && range_in_bitwidth rshiftr s) - ; make_rewriteo - (pcst2 (#pattern.ident.Z_add_get_carry @ #?ℤ @ pcst (#pattern.ident.Z_shiftr @ ??' @ #?ℤ) @ #?ℤ)) - (fun '((r1, r2)%core) s rshiftr ry y offset xx => cst2 (r1, r2)%core (#(ident.fancy_add (Z.log2 s) (-offset)) @ (##xx, cst ry y)) when (s =? 2^Z.log2 s) && shiftr_good rshiftr ry offset && range_in_bitwidth rshiftr s) + (pcst2 (#pattern.ident.Z_add_get_carry @ #?ℤ' @ pcst (#pattern.ident.Z_shiftr @ ??' @ #?ℤ') @ ??')) + (fun '((r1, r2)%core) rs s rshiftr ry y roffset offset rx x => cst2 (r1, r2)%core (#(ident.fancy_add (Z.log2 s) (-offset)) @ (cst rx x, cst ry y)) when (s =? 2^Z.log2 s) && shiftr_good rshiftr ry offset && range_in_bitwidth rshiftr s && lit_good s rs && lit_good offset roffset) ; make_rewriteo - (pcst2 (#pattern.ident.Z_add_get_carry @ #?ℤ @ ??' @ ??')) - (fun '((r1, r2)%core) s rx x ry y => cst2 (r1, r2)%core (#(ident.fancy_add (Z.log2 s) 0) @ (cst rx x, cst ry y)) when (s =? 2^Z.log2 s) && range_in_bitwidth ry s) - ; make_rewriteo - (pcst2 (#pattern.ident.Z_add_get_carry @ #?ℤ @ ??' @ #?ℤ)) - (fun '((r1, r2)%core) s rx x yy => cst2 (r1, r2)%core (#(ident.fancy_add (Z.log2 s) 0) @ (cst rx x, ##yy)) when (s =? 2^Z.log2 s) && range_in_bitwidth yy s) - ; make_rewriteo - (pcst2 (#pattern.ident.Z_add_get_carry @ #?ℤ @ #?ℤ @ ??')) - (fun '((r1, r2)%core) s xx ry y => cst2 (r1, r2)%core (#(ident.fancy_add (Z.log2 s) 0) @ (##xx, cst ry y)) when (s =? 2^Z.log2 s) && range_in_bitwidth ry s) + (pcst2 (#pattern.ident.Z_add_get_carry @ #?ℤ' @ ??' @ ??')) + (fun '((r1, r2)%core) rs s rx x ry y => cst2 (r1, r2)%core (#(ident.fancy_add (Z.log2 s) 0) @ (cst rx x, cst ry y)) when (s =? 2^Z.log2 s) && range_in_bitwidth ry s && lit_good s rs) (* (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) @@ -2051,212 +2048,78 @@ Module Compilers. (Z.add_with_get_carry_concrete 2^256) @@ (?c, ?x, ?y) --> (addc 0) @@ (c, y, x) *) ; make_rewriteo - (pcst2 (#pattern.ident.Z_add_with_get_carry @ #?ℤ @ ??' @ ??' @ pcst (#pattern.ident.Z_shiftl @ (pcst (#pattern.ident.Z_land @ ??' @ #?ℤ)) @ #?ℤ))) - (fun '((r1, r2)%core) s rc c rx x rshiftl rland ry y mask offset => cst2 (r1, r2)%core (#(ident.fancy_addc (Z.log2 s) offset) @ (cst rc c, cst rx x, cst ry y)) when (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) && (offset <=? Z.log2 s)) - ; make_rewriteo - (pcst2 (#pattern.ident.Z_add_with_get_carry @ #?ℤ @ #?ℤ @ ??' @ pcst (#pattern.ident.Z_shiftl @ (pcst (#pattern.ident.Z_land @ ??' @ #?ℤ)) @ #?ℤ))) - (fun '((r1, r2)%core) s cc rx x rshiftl rland ry y mask offset => cst2 (r1, r2)%core (#(ident.fancy_addc (Z.log2 s) offset) @ (##cc, cst rx x, cst ry y)) when (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) && (offset <=? Z.log2 s)) - ; make_rewriteo - (pcst2 (#pattern.ident.Z_add_with_get_carry @ #?ℤ @ ??' @ #?ℤ @ pcst (#pattern.ident.Z_shiftl @ (pcst (#pattern.ident.Z_land @ ??' @ #?ℤ)) @ #?ℤ))) - (fun '((r1, r2)%core) s rc c xx rshiftl rland ry y mask offset => cst2 (r1, r2)%core (#(ident.fancy_addc (Z.log2 s) offset) @ (cst rc c, ##xx, cst ry y)) when (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) && (offset <=? Z.log2 s)) - ; make_rewriteo - (pcst2 (#pattern.ident.Z_add_with_get_carry @ #?ℤ @ #?ℤ @ #?ℤ @ pcst (#pattern.ident.Z_shiftl @ (pcst (#pattern.ident.Z_land @ ??' @ #?ℤ)) @ #?ℤ))) - (fun '((r1, r2)%core) s cc xx rshiftl rland ry y mask offset => cst2 (r1, r2)%core (#(ident.fancy_addc (Z.log2 s) offset) @ (##cc, ##xx, cst ry y)) when (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) && (offset <=? Z.log2 s)) + (pcst2 (#pattern.ident.Z_add_with_get_carry @ #?ℤ' @ ??' @ ??' @ pcst (#pattern.ident.Z_shiftl @ (pcst (#pattern.ident.Z_land @ ??' @ #?ℤ')) @ #?ℤ'))) + (fun '((r1, r2)%core) rs s rc c rx x rshiftl rland ry y rmask mask roffset offset => cst2 (r1, r2)%core (#(ident.fancy_addc (Z.log2 s) offset) @ (cst rc c, cst rx x, cst ry y)) when (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) && (offset <=? Z.log2 s) && lit_good s rs && lit_good mask rmask && lit_good offset roffset) ; make_rewriteo - (pcst2 (#pattern.ident.Z_add_with_get_carry @ #?ℤ @ ??' @ pcst (#pattern.ident.Z_shiftl @ (pcst (#pattern.ident.Z_land @ ??' @ #?ℤ)) @ #?ℤ) @ ??')) - (fun '((r1, r2)%core) s rc c rshiftl rland ry y mask offset rx x => cst2 (r1, r2)%core (#(ident.fancy_addc (Z.log2 s) offset) @ (cst rc c, cst rx x, cst ry y)) when (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) && (offset <=? Z.log2 s)) - ; make_rewriteo - (pcst2 (#pattern.ident.Z_add_with_get_carry @ #?ℤ @ #?ℤ @ pcst (#pattern.ident.Z_shiftl @ (pcst (#pattern.ident.Z_land @ ??' @ #?ℤ)) @ #?ℤ) @ ??')) - (fun '((r1, r2)%core) s cc rshiftl rland ry y mask offset rx x => cst2 (r1, r2)%core (#(ident.fancy_addc (Z.log2 s) offset) @ (##cc, cst rx x, cst ry y)) when (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) && (offset <=? Z.log2 s)) - ; make_rewriteo - (pcst2 (#pattern.ident.Z_add_with_get_carry @ #?ℤ @ ??' @ pcst (#pattern.ident.Z_shiftl @ (pcst (#pattern.ident.Z_land @ ??' @ #?ℤ)) @ #?ℤ) @ #?ℤ)) - (fun '((r1, r2)%core) s rc c rshiftl rland ry y mask offset xx => cst2 (r1, r2)%core (#(ident.fancy_addc (Z.log2 s) offset) @ (cst rc c, ##xx, cst ry y)) when (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) && (offset <=? Z.log2 s)) - ; make_rewriteo - (pcst2 (#pattern.ident.Z_add_with_get_carry @ #?ℤ @ #?ℤ @ pcst (#pattern.ident.Z_shiftl @ (pcst (#pattern.ident.Z_land @ ??' @ #?ℤ)) @ #?ℤ) @ #?ℤ)) - (fun '((r1, r2)%core) s cc rshiftl rland ry y mask offset xx => cst2 (r1, r2)%core (#(ident.fancy_addc (Z.log2 s) offset) @ (##cc, ##xx, cst ry y)) when (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) && (offset <=? Z.log2 s)) + (pcst2 (#pattern.ident.Z_add_with_get_carry @ #?ℤ' @ ??' @ pcst (#pattern.ident.Z_shiftl @ (pcst (#pattern.ident.Z_land @ ??' @ #?ℤ')) @ #?ℤ') @ ??')) + (fun '((r1, r2)%core) rs s rc c rshiftl rland ry y rmask mask roffset offset rx x => cst2 (r1, r2)%core (#(ident.fancy_addc (Z.log2 s) offset) @ (cst rc c, cst rx x, cst ry y)) when (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) && (offset <=? Z.log2 s) && lit_good s rs && lit_good mask rmask && lit_good offset roffset) ; make_rewriteo - (pcst2 (#pattern.ident.Z_add_with_get_carry @ #?ℤ @ ??' @ ??' @ pcst (#pattern.ident.Z_shiftr @ ??' @ #?ℤ))) - (fun '((r1, r2)%core) s rc c rx x rshiftr ry y offset => cst2 (r1, r2)%core (#(ident.fancy_addc (Z.log2 s) (-offset)) @ (cst rc c, cst rx x, cst ry y)) when (s =? 2^Z.log2 s) && shiftr_good rshiftr ry offset && range_in_bitwidth rshiftr s) - ; make_rewriteo - (pcst2 (#pattern.ident.Z_add_with_get_carry @ #?ℤ @ #?ℤ @ ??' @ pcst (#pattern.ident.Z_shiftr @ ??' @ #?ℤ))) - (fun '((r1, r2)%core) s cc rx x rshiftr ry y offset => cst2 (r1, r2)%core (#(ident.fancy_addc (Z.log2 s) (-offset)) @ (##cc, cst rx x, cst ry y)) when (s =? 2^Z.log2 s) && shiftr_good rshiftr ry offset && range_in_bitwidth rshiftr s) - ; make_rewriteo - (pcst2 (#pattern.ident.Z_add_with_get_carry @ #?ℤ @ ??' @ #?ℤ @ pcst (#pattern.ident.Z_shiftr @ ??' @ #?ℤ))) - (fun '((r1, r2)%core) s rc c xx rshiftr ry y offset => cst2 (r1, r2)%core (#(ident.fancy_addc (Z.log2 s) (-offset)) @ (cst rc c, ##xx, cst ry y)) when (s =? 2^Z.log2 s) && shiftr_good rshiftr ry offset && range_in_bitwidth rshiftr s) - ; make_rewriteo - (pcst2 (#pattern.ident.Z_add_with_get_carry @ #?ℤ @ #?ℤ @ #?ℤ @ pcst (#pattern.ident.Z_shiftr @ ??' @ #?ℤ))) - (fun '((r1, r2)%core) s cc xx rshiftr ry y offset => cst2 (r1, r2)%core (#(ident.fancy_addc (Z.log2 s) (-offset)) @ (##cc, ##xx, cst ry y)) when (s =? 2^Z.log2 s) && shiftr_good rshiftr ry offset && range_in_bitwidth rshiftr s) + (pcst2 (#pattern.ident.Z_add_with_get_carry @ #?ℤ' @ ??' @ ??' @ pcst (#pattern.ident.Z_shiftr @ ??' @ #?ℤ'))) + (fun '((r1, r2)%core) rs s rc c rx x rshiftr ry y roffset offset => cst2 (r1, r2)%core (#(ident.fancy_addc (Z.log2 s) (-offset)) @ (cst rc c, cst rx x, cst ry y)) when (s =? 2^Z.log2 s) && shiftr_good rshiftr ry offset && range_in_bitwidth rshiftr s && lit_good s rs && lit_good offset roffset) ; make_rewriteo - (pcst2 (#pattern.ident.Z_add_with_get_carry @ #?ℤ @ ??' @ pcst (#pattern.ident.Z_shiftr @ ??' @ #?ℤ) @ ??')) - (fun '((r1, r2)%core) s rc c rshiftr ry y offset rx x => cst2 (r1, r2)%core (#(ident.fancy_addc (Z.log2 s) (-offset)) @ (cst rc c, cst rx x, cst ry y)) when (s =? 2^Z.log2 s) && shiftr_good rshiftr ry offset && range_in_bitwidth rshiftr s) - ; make_rewriteo - (pcst2 (#pattern.ident.Z_add_with_get_carry @ #?ℤ @ #?ℤ @ pcst (#pattern.ident.Z_shiftr @ ??' @ #?ℤ) @ ??')) - (fun '((r1, r2)%core) s cc rshiftr ry y offset rx x => cst2 (r1, r2)%core (#(ident.fancy_addc (Z.log2 s) (-offset)) @ (##cc, cst rx x, cst ry y)) when (s =? 2^Z.log2 s) && shiftr_good rshiftr ry offset && range_in_bitwidth rshiftr s) - ; make_rewriteo - (pcst2 (#pattern.ident.Z_add_with_get_carry @ #?ℤ @ ??' @ pcst (#pattern.ident.Z_shiftr @ ??' @ #?ℤ) @ #?ℤ)) - (fun '((r1, r2)%core) s rc c rshiftr ry y offset xx => cst2 (r1, r2)%core (#(ident.fancy_addc (Z.log2 s) (-offset)) @ (cst rc c, ##xx, cst ry y)) when (s =? 2^Z.log2 s) && shiftr_good rshiftr ry offset && range_in_bitwidth rshiftr s) - ; make_rewriteo - (pcst2 (#pattern.ident.Z_add_with_get_carry @ #?ℤ @ #?ℤ @ pcst (#pattern.ident.Z_shiftr @ ??' @ #?ℤ) @ #?ℤ)) - (fun '((r1, r2)%core) s cc rshiftr ry y offset xx => cst2 (r1, r2)%core (#(ident.fancy_addc (Z.log2 s) (-offset)) @ (##cc, ##xx, cst ry y)) when (s =? 2^Z.log2 s) && shiftr_good rshiftr ry offset && range_in_bitwidth rshiftr s) + (pcst2 (#pattern.ident.Z_add_with_get_carry @ #?ℤ' @ ??' @ pcst (#pattern.ident.Z_shiftr @ ??' @ #?ℤ') @ ??')) + (fun '((r1, r2)%core) rs s rc c rshiftr ry y roffset offset rx x => cst2 (r1, r2)%core (#(ident.fancy_addc (Z.log2 s) (-offset)) @ (cst rc c, cst rx x, cst ry y)) when (s =? 2^Z.log2 s) && shiftr_good rshiftr ry offset && range_in_bitwidth rshiftr s && lit_good s rs && lit_good offset roffset) ; make_rewriteo - (pcst2 (#pattern.ident.Z_add_with_get_carry @ #?ℤ @ ??' @ ??' @ ??')) - (fun '((r1, r2)%core) s rc c rx x ry y => cst2 (r1, r2)%core (#(ident.fancy_addc (Z.log2 s) 0) @ (cst rc c, cst rx x, cst ry y)) when (s =? 2^Z.log2 s) && range_in_bitwidth ry s) - ; make_rewriteo - (pcst2 (#pattern.ident.Z_add_with_get_carry @ #?ℤ @ #?ℤ @ ??' @ ??')) - (fun '((r1, r2)%core) s cc rx x ry y => cst2 (r1, r2)%core (#(ident.fancy_addc (Z.log2 s) 0) @ (##cc, cst rx x, cst ry y)) when (s =? 2^Z.log2 s) && range_in_bitwidth ry s) - ; make_rewriteo - (pcst2 (#pattern.ident.Z_add_with_get_carry @ #?ℤ @ ??' @ #?ℤ @ ??')) - (fun '((r1, r2)%core) s rc c xx ry y => cst2 (r1, r2)%core (#(ident.fancy_addc (Z.log2 s) 0) @ (cst rc c, ##xx, cst ry y)) when (s =? 2^Z.log2 s) && range_in_bitwidth ry s) - ; make_rewriteo - (pcst2 (#pattern.ident.Z_add_with_get_carry @ #?ℤ @ ??' @ ??' @ #?ℤ)) - (fun '((r1, r2)%core) s rc c rx x yy => cst2 (r1, r2)%core (#(ident.fancy_addc (Z.log2 s) 0) @ (cst rc c, cst rx x, ##yy)) when (s =? 2^Z.log2 s) && range_in_bitwidth yy s) - ; make_rewriteo - (pcst2 (#pattern.ident.Z_add_with_get_carry @ #?ℤ @ #?ℤ @ #?ℤ @ ??')) - (fun '((r1, r2)%core) s cc xx ry y => cst2 (r1, r2)%core (#(ident.fancy_addc (Z.log2 s) 0) @ (##cc, ##xx, cst ry y)) when (s =? 2^Z.log2 s) && range_in_bitwidth ry s) - ; make_rewriteo - (pcst2 (#pattern.ident.Z_add_with_get_carry @ #?ℤ @ #?ℤ @ ??' @ #?ℤ)) - (fun '((r1, r2)%core) s cc rx x yy => cst2 (r1, r2)%core (#(ident.fancy_addc (Z.log2 s) 0) @ (##cc, cst rx x, ##yy)) when (s =? 2^Z.log2 s) && range_in_bitwidth yy s) - ; make_rewriteo - (pcst2 (#pattern.ident.Z_add_with_get_carry @ #?ℤ @ ??' @ #?ℤ @ #?ℤ)) - (fun '((r1, r2)%core) s rc c xx yy => cst2 (r1, r2)%core (#(ident.fancy_addc (Z.log2 s) 0) @ (cst rc c, ##xx, ##yy)) when (s =? 2^Z.log2 s) && range_in_bitwidth yy s) + (pcst2 (#pattern.ident.Z_add_with_get_carry @ #?ℤ' @ ??' @ ??' @ ??')) + (fun '((r1, r2)%core) rs s rc c rx x ry y => cst2 (r1, r2)%core (#(ident.fancy_addc (Z.log2 s) 0) @ (cst rc c, cst rx x, cst ry y)) when (s =? 2^Z.log2 s) && range_in_bitwidth ry s && lit_good s rs) + (* (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) *) ; make_rewriteo - (pcst2 (#pattern.ident.Z_sub_get_borrow @ #?ℤ @ ??' @ pcst (#pattern.ident.Z_shiftl @ (pcst (#pattern.ident.Z_land @ ??' @ #?ℤ)) @ #?ℤ))) - (fun '((r1, r2)%core) s rx x rshiftl rland ry y mask offset => cst2 (r1, r2)%core (#(ident.fancy_sub (Z.log2 s) offset) @ (cst rx x, cst ry y)) when (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) && (offset <=? Z.log2 s)) - ; make_rewriteo - (pcst2 (#pattern.ident.Z_sub_get_borrow @ #?ℤ @ #?ℤ @ pcst (#pattern.ident.Z_shiftl @ (pcst (#pattern.ident.Z_land @ ??' @ #?ℤ)) @ #?ℤ))) - (fun '((r1, r2)%core) s xx rshiftl rland ry y mask offset => cst2 (r1, r2)%core (#(ident.fancy_sub (Z.log2 s) offset) @ (##xx, cst ry y)) when (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) && (offset <=? Z.log2 s)) + (pcst2 (#pattern.ident.Z_sub_get_borrow @ #?ℤ' @ ??' @ pcst (#pattern.ident.Z_shiftl @ (pcst (#pattern.ident.Z_land @ ??' @ #?ℤ')) @ #?ℤ'))) + (fun '((r1, r2)%core) rs s rx x rshiftl rland ry y rmask mask roffset offset => cst2 (r1, r2)%core (#(ident.fancy_sub (Z.log2 s) offset) @ (cst rx x, cst ry y)) when (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) && (offset <=? Z.log2 s) && lit_good s rs && lit_good mask rmask && lit_good offset roffset) ; make_rewriteo - (pcst2 (#pattern.ident.Z_sub_get_borrow @ #?ℤ @ ??' @ pcst (#pattern.ident.Z_shiftr @ ??' @ #?ℤ))) - (fun '((r1, r2)%core) s rx x rshiftr ry y offset => cst2 (r1, r2)%core (#(ident.fancy_sub (Z.log2 s) (-offset)) @ (cst rx x, cst ry y)) when (s =? 2^Z.log2 s) && shiftr_good rshiftr ry offset && range_in_bitwidth rshiftr s) - ; make_rewriteo - (pcst2 (#pattern.ident.Z_sub_get_borrow @ #?ℤ @ #?ℤ @ pcst (#pattern.ident.Z_shiftr @ ??' @ #?ℤ))) - (fun '((r1, r2)%core) s xx rshiftr ry y offset => cst2 (r1, r2)%core (#(ident.fancy_sub (Z.log2 s) (-offset)) @ (##xx, cst ry y)) when (s =? 2^Z.log2 s) && shiftr_good rshiftr ry offset && range_in_bitwidth rshiftr s) + (pcst2 (#pattern.ident.Z_sub_get_borrow @ #?ℤ' @ ??' @ pcst (#pattern.ident.Z_shiftr @ ??' @ #?ℤ'))) + (fun '((r1, r2)%core) rs s rx x rshiftr ry y roffset offset => cst2 (r1, r2)%core (#(ident.fancy_sub (Z.log2 s) (-offset)) @ (cst rx x, cst ry y)) when (s =? 2^Z.log2 s) && shiftr_good rshiftr ry offset && range_in_bitwidth rshiftr s && lit_good s rs && lit_good offset roffset) ; make_rewriteo - (pcst2 (#pattern.ident.Z_sub_get_borrow @ #?ℤ @ ??' @ ??')) - (fun '((r1, r2)%core) s rx x ry y => cst2 (r1, r2)%core (#(ident.fancy_sub (Z.log2 s) 0) @ (cst rx x, cst ry y)) when (s =? 2^Z.log2 s) && range_in_bitwidth ry s) - ; make_rewriteo - (pcst2 (#pattern.ident.Z_sub_get_borrow @ #?ℤ @ #?ℤ @ ??')) - (fun '((r1, r2)%core) s xx ry y => cst2 (r1, r2)%core (#(ident.fancy_sub (Z.log2 s) 0) @ (##xx, cst ry y)) when (s =? 2^Z.log2 s) && range_in_bitwidth ry s) - ; make_rewriteo - (pcst2 (#pattern.ident.Z_sub_get_borrow @ #?ℤ @ ??' @ #?ℤ)) - (fun '((r1, r2)%core) s rx x yy => cst2 (r1, r2)%core (#(ident.fancy_sub (Z.log2 s) 0) @ (cst rx x, ##yy)) when (s =? 2^Z.log2 s) && range_in_bitwidth yy s) + (pcst2 (#pattern.ident.Z_sub_get_borrow @ #?ℤ' @ ??' @ ??')) + (fun '((r1, r2)%core) rs s rx x ry y => cst2 (r1, r2)%core (#(ident.fancy_sub (Z.log2 s) 0) @ (cst rx x, cst ry y)) when (s =? 2^Z.log2 s) && range_in_bitwidth ry s && lit_good s rs) (* (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) *) ; make_rewriteo - (pcst2 (#pattern.ident.Z_sub_with_get_borrow @ #?ℤ @ ??' @ ??' @ pcst (#pattern.ident.Z_shiftl @ (pcst (#pattern.ident.Z_land @ ??' @ #?ℤ)) @ #?ℤ))) - (fun '((r1, r2)%core) s rb b rx x rshiftl rland ry y mask offset => cst2 (r1, r2)%core (#(ident.fancy_subb (Z.log2 s) offset) @ (cst rb b, cst rx x, cst ry y)) when (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) && (offset <=? Z.log2 s)) - ; make_rewriteo - (pcst2 (#pattern.ident.Z_sub_with_get_borrow @ #?ℤ @ #?ℤ @ ??' @ pcst (#pattern.ident.Z_shiftl @ (pcst (#pattern.ident.Z_land @ ??' @ #?ℤ)) @ #?ℤ))) - (fun '((r1, r2)%core) s bb rx x rshiftl rland ry y mask offset => cst2 (r1, r2)%core (#(ident.fancy_subb (Z.log2 s) offset) @ (##bb, cst rx x, cst ry y)) when (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) && (offset <=? Z.log2 s)) - ; make_rewriteo - (pcst2 (#pattern.ident.Z_sub_with_get_borrow @ #?ℤ @ ??' @ #?ℤ @ pcst (#pattern.ident.Z_shiftl @ (pcst (#pattern.ident.Z_land @ ??' @ #?ℤ)) @ #?ℤ))) - (fun '((r1, r2)%core) s rb b xx rshiftl rland ry y mask offset => cst2 (r1, r2)%core (#(ident.fancy_subb (Z.log2 s) offset) @ (cst rb b, ##xx, cst ry y)) when (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) && (offset <=? Z.log2 s)) - ; make_rewriteo - (pcst2 (#pattern.ident.Z_sub_with_get_borrow @ #?ℤ @ #?ℤ @ #?ℤ @ pcst (#pattern.ident.Z_shiftl @ (pcst (#pattern.ident.Z_land @ ??' @ #?ℤ)) @ #?ℤ))) - (fun '((r1, r2)%core) s bb xx rshiftl rland ry y mask offset => cst2 (r1, r2)%core (#(ident.fancy_subb (Z.log2 s) offset) @ (##bb, ##xx, cst ry y)) when (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) && (offset <=? Z.log2 s)) + (pcst2 (#pattern.ident.Z_sub_with_get_borrow @ #?ℤ' @ ??' @ ??' @ pcst (#pattern.ident.Z_shiftl @ (pcst (#pattern.ident.Z_land @ ??' @ #?ℤ')) @ #?ℤ'))) + (fun '((r1, r2)%core) rs s rb b rx x rshiftl rland ry y rmask mask roffset offset => cst2 (r1, r2)%core (#(ident.fancy_subb (Z.log2 s) offset) @ (cst rb b, cst rx x, cst ry y)) when (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) && (offset <=? Z.log2 s) && lit_good s rs && lit_good mask rmask && lit_good offset roffset) ; make_rewriteo - (pcst2 (#pattern.ident.Z_sub_with_get_borrow @ #?ℤ @ ??' @ ??' @ pcst (#pattern.ident.Z_shiftr @ ??' @ #?ℤ))) - (fun '((r1, r2)%core) s rb b rx x rshiftr ry y offset => cst2 (r1, r2)%core (#(ident.fancy_subb (Z.log2 s) (-offset)) @ (cst rb b, cst rx x, cst ry y)) when (s =? 2^Z.log2 s) && shiftr_good rshiftr ry offset && range_in_bitwidth rshiftr s) - ; make_rewriteo - (pcst2 (#pattern.ident.Z_sub_with_get_borrow @ #?ℤ @ #?ℤ @ ??' @ pcst (#pattern.ident.Z_shiftr @ ??' @ #?ℤ))) - (fun '((r1, r2)%core) s bb rx x rshiftr ry y offset => cst2 (r1, r2)%core (#(ident.fancy_subb (Z.log2 s) (-offset)) @ (##bb, cst rx x, cst ry y)) when (s =? 2^Z.log2 s) && shiftr_good rshiftr ry offset && range_in_bitwidth rshiftr s) - ; make_rewriteo - (pcst2 (#pattern.ident.Z_sub_with_get_borrow @ #?ℤ @ ??' @ #?ℤ @ pcst (#pattern.ident.Z_shiftr @ ??' @ #?ℤ))) - (fun '((r1, r2)%core) s rb b xx rshiftr ry y offset => cst2 (r1, r2)%core (#(ident.fancy_subb (Z.log2 s) (-offset)) @ (cst rb b, ##xx, cst ry y)) when (s =? 2^Z.log2 s) && shiftr_good rshiftr ry offset && range_in_bitwidth rshiftr s) - ; make_rewriteo - (pcst2 (#pattern.ident.Z_sub_with_get_borrow @ #?ℤ @ #?ℤ @ #?ℤ @ pcst (#pattern.ident.Z_shiftr @ ??' @ #?ℤ))) - (fun '((r1, r2)%core) s bb xx rshiftr ry y offset => cst2 (r1, r2)%core (#(ident.fancy_subb (Z.log2 s) (-offset)) @ (##bb, ##xx, cst ry y)) when (s =? 2^Z.log2 s) && shiftr_good rshiftr ry offset && range_in_bitwidth rshiftr s) + (pcst2 (#pattern.ident.Z_sub_with_get_borrow @ #?ℤ' @ ??' @ ??' @ pcst (#pattern.ident.Z_shiftr @ ??' @ #?ℤ'))) + (fun '((r1, r2)%core) rs s rb b rx x rshiftr ry y roffset offset => cst2 (r1, r2)%core (#(ident.fancy_subb (Z.log2 s) (-offset)) @ (cst rb b, cst rx x, cst ry y)) when (s =? 2^Z.log2 s) && shiftr_good rshiftr ry offset && range_in_bitwidth rshiftr s && lit_good s rs && lit_good offset roffset) ; make_rewriteo - (pcst2 (#pattern.ident.Z_sub_with_get_borrow @ #?ℤ @ ??' @ ??' @ ??')) - (fun '((r1, r2)%core) s rb b rx x ry y => cst2 (r1, r2)%core (#(ident.fancy_subb (Z.log2 s) 0) @ (cst rb b, cst rx x, cst ry y)) when (s =? 2^Z.log2 s) && range_in_bitwidth ry s) - ; make_rewriteo - (pcst2 (#pattern.ident.Z_sub_with_get_borrow @ #?ℤ @ #?ℤ @ ??' @ ??')) - (fun '((r1, r2)%core) s bb rx x ry y => cst2 (r1, r2)%core (#(ident.fancy_subb (Z.log2 s) 0) @ (##bb, cst rx x, cst ry y)) when (s =? 2^Z.log2 s) && range_in_bitwidth ry s) - ; make_rewriteo - (pcst2 (#pattern.ident.Z_sub_with_get_borrow @ #?ℤ @ ??' @ #?ℤ @ ??')) - (fun '((r1, r2)%core) s rb b xx ry y => cst2 (r1, r2)%core (#(ident.fancy_subb (Z.log2 s) 0) @ (cst rb b, ##xx, cst ry y)) when (s =? 2^Z.log2 s) && range_in_bitwidth ry s) - ; make_rewriteo - (pcst2 (#pattern.ident.Z_sub_with_get_borrow @ #?ℤ @ ??' @ ??' @ #?ℤ)) - (fun '((r1, r2)%core) s rb b rx x yy => cst2 (r1, r2)%core (#(ident.fancy_subb (Z.log2 s) 0) @ (cst rb b, cst rx x, ##yy)) when (s =? 2^Z.log2 s) && range_in_bitwidth yy s) - ; make_rewriteo - (pcst2 (#pattern.ident.Z_sub_with_get_borrow @ #?ℤ @ #?ℤ @ #?ℤ @ ??')) - (fun '((r1, r2)%core) s bb xx ry y => cst2 (r1, r2)%core (#(ident.fancy_subb (Z.log2 s) 0) @ (##bb, ##xx, cst ry y)) when (s =? 2^Z.log2 s) && range_in_bitwidth ry s) - ; make_rewriteo - (pcst2 (#pattern.ident.Z_sub_with_get_borrow @ #?ℤ @ #?ℤ @ ??' @ #?ℤ)) - (fun '((r1, r2)%core) s bb rx x yy => cst2 (r1, r2)%core (#(ident.fancy_subb (Z.log2 s) 0) @ (##bb, cst rx x, ##yy)) when (s =? 2^Z.log2 s) && range_in_bitwidth yy s) - ; make_rewriteo - (pcst2 (#pattern.ident.Z_sub_with_get_borrow @ #?ℤ @ ??' @ #?ℤ @ #?ℤ)) - (fun '((r1, r2)%core) s rb b xx yy => cst2 (r1, r2)%core (#(ident.fancy_subb (Z.log2 s) 0) @ (cst rb b, ##xx, ##yy)) when (s =? 2^Z.log2 s) && range_in_bitwidth yy s) + (pcst2 (#pattern.ident.Z_sub_with_get_borrow @ #?ℤ' @ ??' @ ??' @ ??')) + (fun '((r1, r2)%core) rs s rb b rx x ry y => cst2 (r1, r2)%core (#(ident.fancy_subb (Z.log2 s) 0) @ (cst rb b, cst rx x, cst ry y)) when (s =? 2^Z.log2 s) && range_in_bitwidth ry s && lit_good s rs) (*(Z.rshi_concrete 2^256 ?n) @@ (?c, ?x, ?y) --> (rshi n) @@ (x, y)*) ; make_rewriteo - (pcst (#pattern.ident.Z_rshi @ #?ℤ @ ??' @ ??' @ #?ℤ)) - (fun r s rx x ry y n => cst r (#(ident.fancy_rshi (Z.log2 s) n) @ (cst rx x, cst ry y)) when (s =? 2^Z.log2 s)) - ; make_rewriteo - (pcst (#pattern.ident.Z_rshi @ #?ℤ @ #?ℤ @ ??' @ #?ℤ)) - (fun r s xx ry y n => cst r (#(ident.fancy_rshi (Z.log2 s) n) @ (##xx, cst ry y)) when (s =? 2^Z.log2 s)) - ; make_rewriteo - (pcst (#pattern.ident.Z_rshi @ #?ℤ @ ??' @ #?ℤ @ #?ℤ)) - (fun r s rx x yy n => cst r (#(ident.fancy_rshi (Z.log2 s) n) @ (cst rx x, ##yy)) when (s =? 2^Z.log2 s)) + (pcst (#pattern.ident.Z_rshi @ #?ℤ' @ ??' @ ??' @ #?ℤ')) + (fun r rs s rx x ry y rn n => cst r (#(ident.fancy_rshi (Z.log2 s) n) @ (cst rx x, cst ry y)) when (s =? 2^Z.log2 s) && lit_good s rs && lit_good n rn) (* 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) *) ; make_rewriteo - (pcst (#pattern.ident.Z_zselect @ pcst (#pattern.ident.Z_cc_m @ #?ℤ @ ??') @ ??' @ ??')) - (fun r rccm s rc c rx x ry y => cst r (#(ident.fancy_selm (Z.log2 s)) @ (cst rc c, cst rx x, cst ry y)) when (s =? 2^Z.log2 s) && cc_m_good rccm s rc) - ; make_rewriteo - (pcst (#pattern.ident.Z_zselect @ pcst (#pattern.ident.Z_cc_m @ #?ℤ @ ??') @ #?ℤ @ ??')) - (fun r rccm s rc c xx ry y => cst r (#(ident.fancy_selm (Z.log2 s)) @ (cst rc c, ##xx, cst ry y)) when (s =? 2^Z.log2 s) && cc_m_good rccm s rc) - ; make_rewriteo - (pcst (#pattern.ident.Z_zselect @ pcst (#pattern.ident.Z_cc_m @ #?ℤ @ ??') @ ??' @ #?ℤ)) - (fun r rccm s rc c rx x yy => cst r (#(ident.fancy_selm (Z.log2 s)) @ (cst rc c, cst rx x, ##yy)) when (s =? 2^Z.log2 s) && cc_m_good rccm s rc) - ; make_rewriteo - (pcst (#pattern.ident.Z_zselect @ pcst (#pattern.ident.Z_cc_m @ #?ℤ @ ??') @ #?ℤ @ #?ℤ)) - (fun r rccm s rc c xx yy => cst r (#(ident.fancy_selm (Z.log2 s)) @ (cst rc c, ##xx, ##yy)) when (s =? 2^Z.log2 s) && cc_m_good rccm s rc) + (pcst (#pattern.ident.Z_zselect @ pcst (#pattern.ident.Z_cc_m @ #?ℤ' @ ??') @ ??' @ ??')) + (fun r rccm rs s rc c rx x ry y => cst r (#(ident.fancy_selm (Z.log2 s)) @ (cst rc c, cst rx x, cst ry y)) when (s =? 2^Z.log2 s) && cc_m_good rccm s rc && lit_good s rs) ; make_rewriteo - (pcst (#pattern.ident.Z_zselect @ pcst (#pattern.ident.Z_land @ #?ℤ @ ??') @ ??' @ ??')) - (fun r rland mask rc c rx x ry y => cst r (#ident.fancy_sell @ (cst rc c, cst rx x, cst ry y)) when (mask =? 1) && land_good rland mask rc) - ; make_rewriteo - (pcst (#pattern.ident.Z_zselect @ pcst (#pattern.ident.Z_land @ #?ℤ @ ??') @ #?ℤ @ ??')) - (fun r rland mask rc c xx ry y => cst r (#ident.fancy_sell @ (cst rc c, ##xx, cst ry y)) when (mask =? 1) && land_good rland mask rc) - ; make_rewriteo - (pcst (#pattern.ident.Z_zselect @ pcst (#pattern.ident.Z_land @ #?ℤ @ ??') @ ??' @ #?ℤ)) - (fun r rland mask rc c rx x yy => cst r (#ident.fancy_sell @ (cst rc c, cst rx x, ##yy)) when (mask =? 1) && land_good rland mask rc) - ; make_rewriteo - (pcst (#pattern.ident.Z_zselect @ pcst (#pattern.ident.Z_land @ #?ℤ @ ??') @ #?ℤ @ #?ℤ)) - (fun r rland mask rc c xx yy => cst r (#ident.fancy_sell @ (cst rc c, ##xx, ##yy)) when (mask =? 1) && land_good rland mask rc) + (pcst (#pattern.ident.Z_zselect @ pcst (#pattern.ident.Z_land @ #?ℤ' @ ??') @ ??' @ ??')) + (fun r rland rmask mask rc c rx x ry y => cst r (#ident.fancy_sell @ (cst rc c, cst rx x, cst ry y)) when (mask =? 1) && land_good rland mask rc && lit_good mask rmask) ; make_rewriteo - (pcst (#pattern.ident.Z_zselect @ pcst (#pattern.ident.Z_land @ ??' @ #?ℤ) @ ??' @ ??')) - (fun r rland rc c mask rx x ry y => cst r (#ident.fancy_sell @ (cst rc c, cst rx x, cst ry y)) when (mask =? 1) && land_good rland rc mask) - ; make_rewriteo - (pcst (#pattern.ident.Z_zselect @ pcst (#pattern.ident.Z_land @ ??' @ #?ℤ) @ #?ℤ @ ??')) - (fun r rland rc c mask xx ry y => cst r (#ident.fancy_sell @ (cst rc c, ##xx, cst ry y)) when (mask =? 1) && land_good rland rc mask) - ; make_rewriteo - (pcst (#pattern.ident.Z_zselect @ pcst (#pattern.ident.Z_land @ ??' @ #?ℤ) @ ??' @ #?ℤ)) - (fun r rland rc c mask rx x yy => cst r (#ident.fancy_sell @ (cst rc c, cst rx x, ##yy)) when (mask =? 1) && land_good rland rc mask) - ; make_rewriteo - (pcst (#pattern.ident.Z_zselect @ pcst (#pattern.ident.Z_land @ ??' @ #?ℤ) @ #?ℤ @ #?ℤ)) - (fun r rland rc c mask xx yy => cst r (#ident.fancy_sell @ (cst rc c, ##xx, ##yy)) when (mask =? 1) && land_good rland rc mask) + (pcst (#pattern.ident.Z_zselect @ pcst (#pattern.ident.Z_land @ ??' @ #?ℤ') @ ??' @ ??')) + (fun r rland rc c rmask mask rx x ry y => cst r (#ident.fancy_sell @ (cst rc c, cst rx x, cst ry y)) when (mask =? 1) && land_good rland rc mask && lit_good mask rmask) ; make_rewrite (pcst (#pattern.ident.Z_zselect @ ?? @ ?? @ ??)) @@ -2274,70 +2137,70 @@ Z.mul @@ (?x >> 128, ?y >> 128) --> mulhh @@ (x, y) *) (* literal on left *) ; make_rewriteo - (#?ℤ *' pcst (#pattern.ident.Z_land @ ??' @ #?ℤ)) - (fun r x rland ry y mask => let s := (2*Z.log2_up mask)%Z in x <- invert_low s x; cst r (#(ident.fancy_mulll s) @ (##x, cst ry y)) when (mask =? 2^(s/2)-1) && land_good rland ry mask) + (#?ℤ' *' pcst (#pattern.ident.Z_land @ ??' @ #?ℤ')) + (fun r rx x rland ry y rmask mask => let s := (2*Z.log2_up mask)%Z in x <- invert_low s x; cst r (#(ident.fancy_mulll s) @ (##x, cst ry y)) when (mask =? 2^(s/2)-1) && land_good rland ry mask && lit_good x rx && lit_good mask rmask) ; make_rewriteo - (#?ℤ *' pcst (#pattern.ident.Z_land @ #?ℤ @ ??')) - (fun r x rland mask ry y => let s := (2*Z.log2_up mask)%Z in x <- invert_low s x; cst r (#(ident.fancy_mulll s) @ (##x, cst ry y)) when (mask =? 2^(s/2)-1) && land_good rland mask ry) + (#?ℤ' *' pcst (#pattern.ident.Z_land @ #?ℤ' @ ??')) + (fun r rx x rland rmask mask ry y => let s := (2*Z.log2_up mask)%Z in x <- invert_low s x; cst r (#(ident.fancy_mulll s) @ (##x, cst ry y)) when (mask =? 2^(s/2)-1) && land_good rland mask ry && lit_good x rx && lit_good mask rmask) ; make_rewriteo - (#?ℤ *' pcst (#pattern.ident.Z_shiftr @ ??' @ #?ℤ)) - (fun r x rshiftr ry y offset => let s := (2*offset)%Z in x <- invert_low s x; cst r (#(ident.fancy_mullh s) @ (##x, cst ry y)) when shiftr_good rshiftr ry offset) + (#?ℤ' *' pcst (#pattern.ident.Z_shiftr @ ??' @ #?ℤ')) + (fun r rx x rshiftr ry y roffset offset => let s := (2*offset)%Z in x <- invert_low s x; cst r (#(ident.fancy_mullh s) @ (##x, cst ry y)) when shiftr_good rshiftr ry offset && lit_good x rx && lit_good offset roffset) ; make_rewriteo - (#?ℤ *' pcst (#pattern.ident.Z_land @ #?ℤ @ ??')) - (fun r x rland mask ry y => let s := (2*Z.log2_up mask)%Z in x <- invert_high s x; cst r (#(ident.fancy_mulhl s) @ (##x, cst ry y)) when (mask =? 2^(s/2)-1) && land_good rland mask ry) + (#?ℤ' *' pcst (#pattern.ident.Z_land @ #?ℤ' @ ??')) + (fun r rx x rland rmask mask ry y => let s := (2*Z.log2_up mask)%Z in x <- invert_high s x; cst r (#(ident.fancy_mulhl s) @ (##x, cst ry y)) when (mask =? 2^(s/2)-1) && land_good rland mask ry && lit_good x rx && lit_good mask rmask) ; make_rewriteo - (#?ℤ *' pcst (#pattern.ident.Z_land @ ??' @ #?ℤ)) - (fun r x rland ry y mask => let s := (2*Z.log2_up mask)%Z in x <- invert_high s x; cst r (#(ident.fancy_mulhl s) @ (##x, cst ry y)) when (mask =? 2^(s/2)-1) && land_good rland ry mask) + (#?ℤ' *' pcst (#pattern.ident.Z_land @ ??' @ #?ℤ')) + (fun r rx x rland ry y rmask mask => let s := (2*Z.log2_up mask)%Z in x <- invert_high s x; cst r (#(ident.fancy_mulhl s) @ (##x, cst ry y)) when (mask =? 2^(s/2)-1) && land_good rland ry mask && lit_good x rx && lit_good mask rmask) ; make_rewriteo - (#?ℤ *' pcst (#pattern.ident.Z_shiftr @ ??' @ #?ℤ)) - (fun r x rshiftr ry y offset => let s := (2*offset)%Z in x <- invert_high s x; cst r (#(ident.fancy_mulhh s) @ (##x, cst ry y)) when shiftr_good rshiftr ry offset) + (#?ℤ' *' pcst (#pattern.ident.Z_shiftr @ ??' @ #?ℤ')) + (fun r rx x rshiftr ry y roffset offset => let s := (2*offset)%Z in x <- invert_high s x; cst r (#(ident.fancy_mulhh s) @ (##x, cst ry y)) when shiftr_good rshiftr ry offset && lit_good x rx && lit_good offset roffset) (* literal on right *) ; make_rewriteo - (pcst (#pattern.ident.Z_land @ #?ℤ @ ??') *' #?ℤ) - (fun r rland mask rx x y => let s := (2*Z.log2_up mask)%Z in y <- invert_low s y; cst r (#(ident.fancy_mulll s) @ (cst rx x, ##y)) when (mask =? 2^(s/2)-1) && land_good rland mask rx) + (pcst (#pattern.ident.Z_land @ #?ℤ' @ ??') *' #?ℤ') + (fun r rland rmask mask rx x ry y => let s := (2*Z.log2_up mask)%Z in y <- invert_low s y; cst r (#(ident.fancy_mulll s) @ (cst rx x, ##y)) when (mask =? 2^(s/2)-1) && land_good rland mask rx && lit_good y ry && lit_good mask rmask) ; make_rewriteo - (pcst (#pattern.ident.Z_land @ ??' @ #?ℤ) *' #?ℤ) - (fun r rland rx x mask y => let s := (2*Z.log2_up mask)%Z in y <- invert_low s y; cst r (#(ident.fancy_mulll s) @ (cst rx x, ##y)) when (mask =? 2^(s/2)-1) && land_good rland rx mask) + (pcst (#pattern.ident.Z_land @ ??' @ #?ℤ') *' #?ℤ') + (fun r rland rx x rmask mask ry y => let s := (2*Z.log2_up mask)%Z in y <- invert_low s y; cst r (#(ident.fancy_mulll s) @ (cst rx x, ##y)) when (mask =? 2^(s/2)-1) && land_good rland rx mask && lit_good y ry && lit_good mask rmask) ; make_rewriteo - (pcst (#pattern.ident.Z_land @ #?ℤ @ ??') *' #?ℤ) - (fun r rland mask rx x y => let s := (2*Z.log2_up mask)%Z in y <- invert_high s y; cst r (#(ident.fancy_mullh s) @ (cst rx x, ##y)) when (mask =? 2^(s/2)-1) && land_good rland mask rx) + (pcst (#pattern.ident.Z_land @ #?ℤ' @ ??') *' #?ℤ') + (fun r rland rmask mask rx x ry y => let s := (2*Z.log2_up mask)%Z in y <- invert_high s y; cst r (#(ident.fancy_mullh s) @ (cst rx x, ##y)) when (mask =? 2^(s/2)-1) && land_good rland mask rx && lit_good y ry && lit_good mask rmask) ; make_rewriteo - (pcst (#pattern.ident.Z_land @ ??' @ #?ℤ) *' #?ℤ) - (fun r rland rx x mask y => let s := (2*Z.log2_up mask)%Z in y <- invert_high s y; cst r (#(ident.fancy_mullh s) @ (cst rx x, ##y)) when (mask =? 2^(s/2)-1) && land_good rland rx mask) + (pcst (#pattern.ident.Z_land @ ??' @ #?ℤ') *' #?ℤ') + (fun r rland rx x rmask mask ry y => let s := (2*Z.log2_up mask)%Z in y <- invert_high s y; cst r (#(ident.fancy_mullh s) @ (cst rx x, ##y)) when (mask =? 2^(s/2)-1) && land_good rland rx mask && lit_good y ry && lit_good mask rmask) ; make_rewriteo - (pcst (#pattern.ident.Z_shiftr @ ??' @ #?ℤ) *' #?ℤ) - (fun r rshiftr rx x offset y => let s := (2*offset)%Z in y <- invert_low s y; cst r (#(ident.fancy_mulhl s) @ (cst rx x, ##y)) when shiftr_good rshiftr rx offset) + (pcst (#pattern.ident.Z_shiftr @ ??' @ #?ℤ') *' #?ℤ') + (fun r rshiftr rx x roffset offset ry y => let s := (2*offset)%Z in y <- invert_low s y; cst r (#(ident.fancy_mulhl s) @ (cst rx x, ##y)) when shiftr_good rshiftr rx offset && lit_good y ry && lit_good offset roffset) ; make_rewriteo - (pcst (#pattern.ident.Z_shiftr @ ??' @ #?ℤ) *' #?ℤ) - (fun r rshiftr rx x offset y => let s := (2*offset)%Z in y <- invert_high s y; cst r (#(ident.fancy_mulhh s) @ (cst rx x, ##y)) when shiftr_good rshiftr rx offset) + (pcst (#pattern.ident.Z_shiftr @ ??' @ #?ℤ') *' #?ℤ') + (fun r rshiftr rx x roffset offset ry y => let s := (2*offset)%Z in y <- invert_high s y; cst r (#(ident.fancy_mulhh s) @ (cst rx x, ##y)) when shiftr_good rshiftr rx offset && lit_good y ry && lit_good offset roffset) (* no literal *) ; make_rewriteo - (pcst (#pattern.ident.Z_land @ #?ℤ @ ??') *' pcst (#pattern.ident.Z_land @ #?ℤ @ ??')) - (fun r rland1 mask1 rx x rland2 mask2 ry y => let s := (2*Z.log2_up mask1)%Z in cst r (#(ident.fancy_mulll s) @ (cst rx x, cst ry y)) when (mask1 =? 2^(s/2)-1) && (mask2 =? 2^(s/2)-1) && land_good rland1 mask1 rx && land_good rland2 mask2 ry) + (pcst (#pattern.ident.Z_land @ #?ℤ' @ ??') *' pcst (#pattern.ident.Z_land @ #?ℤ' @ ??')) + (fun r rland1 rmask1 mask1 rx x rland2 rmask2 mask2 ry y => let s := (2*Z.log2_up mask1)%Z in cst r (#(ident.fancy_mulll s) @ (cst rx x, cst ry y)) when (mask1 =? 2^(s/2)-1) && (mask2 =? 2^(s/2)-1) && land_good rland1 mask1 rx && land_good rland2 mask2 ry && lit_good mask1 rmask1 && lit_good mask2 rmask2) ; make_rewriteo - (pcst (#pattern.ident.Z_land @ ??' @ #?ℤ) *' pcst (#pattern.ident.Z_land @ #?ℤ @ ??')) - (fun r rland1 rx x mask1 rland2 mask2 ry y => let s := (2*Z.log2_up mask1)%Z in cst r (#(ident.fancy_mulll s) @ (cst rx x, cst ry y)) when (mask1 =? 2^(s/2)-1) && (mask2 =? 2^(s/2)-1) && land_good rland1 rx mask1 && land_good rland2 mask2 ry) + (pcst (#pattern.ident.Z_land @ ??' @ #?ℤ') *' pcst (#pattern.ident.Z_land @ #?ℤ' @ ??')) + (fun r rland1 rx x rmask1 mask1 rland2 rmask2 mask2 ry y => let s := (2*Z.log2_up mask1)%Z in cst r (#(ident.fancy_mulll s) @ (cst rx x, cst ry y)) when (mask1 =? 2^(s/2)-1) && (mask2 =? 2^(s/2)-1) && land_good rland1 rx mask1 && land_good rland2 mask2 ry && lit_good mask1 rmask1 && lit_good mask2 rmask2) ; make_rewriteo - (pcst (#pattern.ident.Z_land @ #?ℤ @ ??') *' pcst (#pattern.ident.Z_land @ ??' @ #?ℤ)) - (fun r rland1 mask1 rx x rland2 ry y mask2 => let s := (2*Z.log2_up mask1)%Z in cst r (#(ident.fancy_mulll s) @ (cst rx x, cst ry y)) when (mask1 =? 2^(s/2)-1) && (mask2 =? 2^(s/2)-1) && land_good rland1 mask1 rx && land_good rland2 ry mask2) + (pcst (#pattern.ident.Z_land @ #?ℤ' @ ??') *' pcst (#pattern.ident.Z_land @ ??' @ #?ℤ')) + (fun r rland1 rmask1 mask1 rx x rland2 ry y rmask2 mask2 => let s := (2*Z.log2_up mask1)%Z in cst r (#(ident.fancy_mulll s) @ (cst rx x, cst ry y)) when (mask1 =? 2^(s/2)-1) && (mask2 =? 2^(s/2)-1) && land_good rland1 mask1 rx && land_good rland2 ry mask2 && lit_good mask1 rmask1 && lit_good mask2 rmask2) ; make_rewriteo - (pcst (#pattern.ident.Z_land @ ??' @ #?ℤ) *' pcst (#pattern.ident.Z_land @ ??' @ #?ℤ)) - (fun r rland1 rx x mask1 rland2 ry y mask2 => let s := (2*Z.log2_up mask1)%Z in cst r (#(ident.fancy_mulll s) @ (cst rx x, cst ry y)) when (mask1 =? 2^(s/2)-1) && (mask2 =? 2^(s/2)-1) && land_good rland1 rx mask1 && land_good rland2 ry mask2) + (pcst (#pattern.ident.Z_land @ ??' @ #?ℤ') *' pcst (#pattern.ident.Z_land @ ??' @ #?ℤ')) + (fun r rland1 rx x rmask1 mask1 rland2 ry y rmask2 mask2 => let s := (2*Z.log2_up mask1)%Z in cst r (#(ident.fancy_mulll s) @ (cst rx x, cst ry y)) when (mask1 =? 2^(s/2)-1) && (mask2 =? 2^(s/2)-1) && land_good rland1 rx mask1 && land_good rland2 ry mask2 && lit_good mask1 rmask1 && lit_good mask2 rmask2) ; make_rewriteo - (pcst (#pattern.ident.Z_land @ #?ℤ @ ??') *' pcst (#pattern.ident.Z_shiftr @ ??' @ #?ℤ)) - (fun r rland1 mask rx x rshiftr2 ry y offset => let s := (2*offset)%Z in cst r (#(ident.fancy_mullh s) @ (cst rx x, cst ry y)) when (mask =? 2^(s/2)-1) && land_good rland1 mask rx && shiftr_good rshiftr2 ry offset) + (pcst (#pattern.ident.Z_land @ #?ℤ' @ ??') *' pcst (#pattern.ident.Z_shiftr @ ??' @ #?ℤ')) + (fun r rland1 rmask mask rx x rshiftr2 ry y roffset offset => let s := (2*offset)%Z in cst r (#(ident.fancy_mullh s) @ (cst rx x, cst ry y)) when (mask =? 2^(s/2)-1) && land_good rland1 mask rx && shiftr_good rshiftr2 ry offset && lit_good mask rmask && lit_good offset roffset) ; make_rewriteo - (pcst (#pattern.ident.Z_land @ ??' @ #?ℤ) *' pcst (#pattern.ident.Z_shiftr @ ??' @ #?ℤ)) - (fun r rland1 rx x mask rshiftr2 ry y offset => let s := (2*offset)%Z in cst r (#(ident.fancy_mullh s) @ (cst rx x, cst ry y)) when (mask =? 2^(s/2)-1) && land_good rland1 rx mask && shiftr_good rshiftr2 ry offset) + (pcst (#pattern.ident.Z_land @ ??' @ #?ℤ') *' pcst (#pattern.ident.Z_shiftr @ ??' @ #?ℤ')) + (fun r rland1 rx x rmask mask rshiftr2 ry y roffset offset => let s := (2*offset)%Z in cst r (#(ident.fancy_mullh s) @ (cst rx x, cst ry y)) when (mask =? 2^(s/2)-1) && land_good rland1 rx mask && shiftr_good rshiftr2 ry offset && lit_good mask rmask && lit_good offset roffset) ; make_rewriteo - (pcst (#pattern.ident.Z_shiftr @ ??' @ #?ℤ) *' pcst (#pattern.ident.Z_land @ #?ℤ @ ??')) - (fun r rshiftr1 rx x offset rland2 mask ry y => let s := (2*offset)%Z in cst r (#(ident.fancy_mulhl s) @ (cst rx x, cst ry y)) when (mask =? 2^(s/2)-1) && shiftr_good rshiftr1 rx offset && land_good rland2 mask ry) + (pcst (#pattern.ident.Z_shiftr @ ??' @ #?ℤ') *' pcst (#pattern.ident.Z_land @ #?ℤ' @ ??')) + (fun r rshiftr1 rx x roffset offset rland2 rmask mask ry y => let s := (2*offset)%Z in cst r (#(ident.fancy_mulhl s) @ (cst rx x, cst ry y)) when (mask =? 2^(s/2)-1) && shiftr_good rshiftr1 rx offset && land_good rland2 mask ry && lit_good mask rmask && lit_good offset roffset) ; make_rewriteo - (pcst (#pattern.ident.Z_shiftr @ ??' @ #?ℤ) *' pcst (#pattern.ident.Z_land @ ??' @ #?ℤ)) - (fun r rshiftr1 rx x offset rland2 ry y mask => let s := (2*offset)%Z in cst r (#(ident.fancy_mulhl s) @ (cst rx x, cst ry y)) when (mask =? 2^(s/2)-1) && shiftr_good rshiftr1 rx offset && land_good rland2 ry mask) + (pcst (#pattern.ident.Z_shiftr @ ??' @ #?ℤ') *' pcst (#pattern.ident.Z_land @ ??' @ #?ℤ')) + (fun r rshiftr1 rx x roffset offset rland2 ry y rmask mask => let s := (2*offset)%Z in cst r (#(ident.fancy_mulhl s) @ (cst rx x, cst ry y)) when (mask =? 2^(s/2)-1) && shiftr_good rshiftr1 rx offset && land_good rland2 ry mask && lit_good mask rmask && lit_good offset roffset) ; make_rewriteo - (pcst (#pattern.ident.Z_shiftr @ ??' @ #?ℤ) *' pcst (#pattern.ident.Z_shiftr @ ??' @ #?ℤ)) - (fun r rshiftr1 rx x offset1 rshiftr2 ry y offset2 => let s := (2*offset1)%Z in cst r (#(ident.fancy_mulhh s) @ (cst rx x, cst ry y)) when (offset1 =? offset2) && shiftr_good rshiftr1 rx offset1 && shiftr_good rshiftr2 ry offset2) + (pcst (#pattern.ident.Z_shiftr @ ??' @ #?ℤ') *' pcst (#pattern.ident.Z_shiftr @ ??' @ #?ℤ')) + (fun r rshiftr1 rx x roffset1 offset1 rshiftr2 ry y roffset2 offset2 => let s := (2*offset1)%Z in cst r (#(ident.fancy_mulhh s) @ (cst rx x, cst ry y)) when (offset1 =? offset2) && shiftr_good rshiftr1 rx offset1 && shiftr_good rshiftr2 ry offset2 && lit_good offset1 roffset1 && lit_good offset2 roffset2) @@ -2595,12 +2458,29 @@ Z.mul @@ (?x >> 128, ?y >> 128) --> mulhh @@ (x, y) Redirect "arith_with_casts_rewrite_head" Print arith_with_casts_rewrite_head. End red_arith_with_casts. + Section red_strip_literal_casts. + Context {var : type.type base.type -> Type} + (do_again : forall t : base.type, @expr base.type ident (@Compile.value base.type ident var) (type.base t) + -> @UnderLets.UnderLets base.type ident var (@expr base.type ident var (type.base t))) + {t} (idc : ident t). + + Time Definition strip_literal_casts_rewrite_head + := make_rewrite_head (@strip_literal_casts_rewrite_head0 var do_again t idc) (@strip_literal_casts_pr2_rewrite_rules). + + Local Set Printing Depth 1000000. + Local Set Printing Width 200. + Import RewriterPrintingNotations. + Redirect "strip_literal_casts_rewrite_head" Print strip_literal_casts_rewrite_head. + End red_strip_literal_casts. + Definition RewriteNBE {t} (e : expr.Expr (ident:=ident) t) : expr.Expr (ident:=ident) t := @Compile.Rewrite (@nbe_rewrite_head) nbe_default_fuel t e. Definition RewriteArith (max_const_val : Z) {t} (e : expr.Expr (ident:=ident) t) : expr.Expr (ident:=ident) t := @Compile.Rewrite (@arith_rewrite_head max_const_val) arith_default_fuel t e. Definition RewriteArithWithCasts {t} (e : expr.Expr (ident:=ident) t) : expr.Expr (ident:=ident) t := @Compile.Rewrite (@arith_with_casts_rewrite_head) arith_with_casts_default_fuel t e. + Definition RewriteStripLiteralCasts {t} (e : expr.Expr (ident:=ident) t) : expr.Expr (ident:=ident) t + := @Compile.Rewrite (fun var do_again => @strip_literal_casts_rewrite_head var) strip_literal_casts_default_fuel t e. Definition RewriteToFancy (invert_low invert_high : Z (*log2wordmax*) -> Z -> @option Z) {t} (e : expr.Expr (ident:=ident) t) : expr.Expr (ident:=ident) t |