Constant-propogate 0+x and x+0 after bounds

After     | File Name                                    | Before    || Change    | % Change
--------------------------------------------------------------------------------------------
21m22.67s | Total                                        | 21m28.24s || -0m05.56s | -0.43%
--------------------------------------------------------------------------------------------
4m09.95s  | PushButtonSynthesis.vo                       | 4m14.76s  || -0m04.81s | -1.88%
3m07.95s  | p384_32.c                                    | 3m11.17s  || -0m03.21s | -1.68%
2m06.43s  | Rewriter.vo                                  | 2m06.15s  || +0m00.28s | +0.22%
1m55.83s  | RewriterWf2.vo                               | 1m56.15s  || -0m00.32s | -0.27%
1m52.36s  | RewriterRulesGood.vo                         | 1m52.34s  || +0m00.01s | +0.01%
1m46.52s  | RewriterRulesInterpGood.vo                   | 1m45.70s  || +0m00.82s | +0.77%
0m46.56s  | RewriterInterpProofs1.vo                     | 0m46.72s  || -0m00.15s | -0.34%
0m45.04s  | ExtractionHaskell/word_by_word_montgomery    | 0m45.33s  || -0m00.28s | -0.63%
0m39.17s  | p521_32.c                                    | 0m39.07s  || +0m00.10s | +0.25%
0m32.40s  | p521_64.c                                    | 0m32.64s  || -0m00.24s | -0.73%
0m31.13s  | ExtractionHaskell/unsaturated_solinas        | 0m30.88s  || +0m00.25s | +0.80%
0m24.20s  | ExtractionHaskell/saturated_solinas          | 0m24.27s  || -0m00.07s | -0.28%
0m23.72s  | RewriterWf1.vo                               | 0m23.42s  || +0m00.29s | +1.28%
0m17.52s  | ExtractionOCaml/word_by_word_montgomery      | 0m17.10s  || +0m00.41s | +2.45%
0m13.39s  | secp256k1_32.c                               | 0m13.29s  || +0m00.10s | +0.75%
0m13.08s  | p256_32.c                                    | 0m13.26s  || -0m00.17s | -1.35%
0m11.49s  | p484_64.c                                    | 0m11.18s  || +0m00.31s | +2.77%
0m10.68s  | ExtractionOCaml/unsaturated_solinas          | 0m10.64s  || +0m00.03s | +0.37%
0m10.11s  | ExtractionOCaml/word_by_word_montgomery.ml   | 0m10.10s  || +0m00.00s | +0.09%
0m07.96s  | ExtractionOCaml/saturated_solinas            | 0m07.95s  || +0m00.00s | +0.12%
0m06.81s  | ExtractionOCaml/unsaturated_solinas.ml       | 0m06.76s  || +0m00.04s | +0.73%
0m06.30s  | ExtractionHaskell/word_by_word_montgomery.hs | 0m06.26s  || +0m00.04s | +0.63%
0m06.07s  | p224_32.c                                    | 0m05.94s  || +0m00.12s | +2.18%
0m06.06s  | BoundsPipeline.vo                            | 0m06.08s  || -0m00.02s | -0.32%
0m05.46s  | p384_64.c                                    | 0m05.30s  || +0m00.16s | +3.01%
0m05.28s  | ExtractionOCaml/saturated_solinas.ml         | 0m05.18s  || +0m00.10s | +1.93%
0m04.97s  | ExtractionHaskell/unsaturated_solinas.hs     | 0m04.99s  || -0m00.02s | -0.40%
0m04.13s  | ExtractionHaskell/saturated_solinas.hs       | 0m04.10s  || +0m00.03s | +0.73%
0m02.34s  | curve25519_32.c                              | 0m02.21s  || +0m00.12s | +5.88%
0m01.59s  | curve25519_64.c                              | 0m01.47s  || +0m00.12s | +8.16%
0m01.46s  | CLI.vo                                       | 0m01.48s  || -0m00.02s | -1.35%
0m01.15s  | secp256k1_64.c                               | 0m01.03s  || +0m00.11s | +11.65%
0m01.14s  | RewriterProofs.vo                            | 0m01.13s  || +0m00.01s | +0.88%
0m01.14s  | StandaloneHaskellMain.vo                     | 0m01.09s  || +0m00.04s | +4.58%
0m01.14s  | StandaloneOCamlMain.vo                       | 0m01.12s  || +0m00.01s | +1.78%
0m01.09s  | p256_64.c                                    | 0m00.98s  || +0m00.11s | +11.22%
0m01.06s  | p224_64.c                                    | 0m01.00s  || +0m00.06s | +6.00%

1 files changed, 121 insertions, 2 deletions

diff --git a/src/arith_with_casts_rewrite_head.out b/src/arith_with_casts_rewrite_head.out
index 053110d89..a179fff11 100644
--- a/src/arith_with_casts_rewrite_head.out
+++ b/src/arith_with_casts_rewrite_head.out
@@ -950,6 +950,126 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
            | None => None
            end
        | @expr.App _ _ _ s _
+         (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc)
+          (@expr.Ident _ _ _ t0 idc0))
+         (@expr.App _ _ _ s1 _ (@expr.Ident _ _ _ t1 idc1) x2) =>
+           args <- invert_bind_args idc1 Raw.ident.Z_cast;
+           args0 <- invert_bind_args idc0 Raw.ident.Literal;
+           _ <- invert_bind_args idc Raw.ident.Z_add;
+           match
+             pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype
+               ((projT1 args0) -> s1)%ptype option (fun x3 : option => x3)
+           with
+           | Some (_, _)%zrange =>
+               if
+                type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
+                  ((projT1 args0) -> s1)%ptype
+               then
+                xv <- ident.unify pattern.ident.Literal ##(projT2 args0);
+                v <- type.try_make_transport_cps s1 ℤ;
+                fv <- (x3 <- (if
+                               ((let (x3, _) := xv in x3) =? 0) &&
+                               (ZRange.normalize args <=?
+                                ZRange.normalize range)%zrange
+                              then
+                               Some
+                                 (#(Z_cast args)%expr @
+                                  v (Compile.reflect x2))%expr_pat
+                              else None);
+                       Some (Base x3));
+                Some (fv0 <-- fv;
+                      Base fv0)%under_lets
+               else None
+           | None => None
+           end
+       | @expr.App _ _ _ s _
+         (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc)
+          (@expr.Ident _ _ _ t0 idc0)) (@expr.App _ _ _ s1 _ ($_)%expr _) |
+         @expr.App _ _ _ s _
+         (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc)
+          (@expr.Ident _ _ _ t0 idc0))
+         (@expr.App _ _ _ s1 _ (@expr.Abs _ _ _ _ _ _) _) | @expr.App _ _ _ s
+         _
+         (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc)
+          (@expr.Ident _ _ _ t0 idc0))
+         (@expr.App _ _ _ s1 _ (_ @ _)%expr_pat _) | @expr.App _ _ _ s _
+         (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc)
+          (@expr.Ident _ _ _ t0 idc0))
+         (@expr.App _ _ _ s1 _ (@expr.LetIn _ _ _ _ _ _ _) _) => None
+       | @expr.App _ _ _ s _
+         (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc)
+          (@expr.Ident _ _ _ t0 idc0)) #(_)%expr_pat | @expr.App _ _ _ s _
+         (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc)
+          (@expr.Ident _ _ _ t0 idc0)) ($_)%expr | @expr.App _ _ _ s _
+         (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc)
+          (@expr.Ident _ _ _ t0 idc0)) (@expr.Abs _ _ _ _ _ _) | @expr.App _
+         _ _ s _
+         (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc)
+          (@expr.Ident _ _ _ t0 idc0)) (@expr.LetIn _ _ _ _ _ _ _) => None
+       | @expr.App _ _ _ s _
+         (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc)
+          (@expr.App _ _ _ s1 _ (@expr.Ident _ _ _ t0 idc0) x2))
+         (@expr.Ident _ _ _ t1 idc1) =>
+           args <- invert_bind_args idc1 Raw.ident.Literal;
+           args0 <- invert_bind_args idc0 Raw.ident.Z_cast;
+           _ <- invert_bind_args idc Raw.ident.Z_add;
+           match
+             pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype
+               (s1 -> (projT1 args))%ptype option (fun x3 : option => x3)
+           with
+           | Some (_, _)%zrange =>
+               if
+                type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
+                  (s1 -> (projT1 args))%ptype
+               then
+                v <- type.try_make_transport_cps s1 ℤ;
+                xv <- ident.unify pattern.ident.Literal ##(projT2 args);
+                fv <- (x3 <- (if
+                               ((let (x3, _) := xv in x3) =? 0) &&
+                               (ZRange.normalize args0 <=?
+                                ZRange.normalize range)%zrange
+                              then
+                               Some
+                                 (#(Z_cast args0)%expr @
+                                  v (Compile.reflect x2))%expr_pat
+                              else None);
+                       Some (Base x3));
+                Some (fv0 <-- fv;
+                      Base fv0)%under_lets
+               else None
+           | None => None
+           end
+       | @expr.App _ _ _ s _
+         (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc)
+          (@expr.App _ _ _ s1 _ (@expr.Ident _ _ _ t0 idc0) x2)) ($_)%expr |
+         @expr.App _ _ _ s _
+         (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc)
+          (@expr.App _ _ _ s1 _ (@expr.Ident _ _ _ t0 idc0) x2))
+         (@expr.Abs _ _ _ _ _ _) | @expr.App _ _ _ s _
+         (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc)
+          (@expr.App _ _ _ s1 _ (@expr.Ident _ _ _ t0 idc0) x2))
+         (_ @ _)%expr_pat | @expr.App _ _ _ s _
+         (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc)
+          (@expr.App _ _ _ s1 _ (@expr.Ident _ _ _ t0 idc0) x2))
+         (@expr.LetIn _ _ _ _ _ _ _) => None
+       | @expr.App _ _ _ s _
+         (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc)
+          (@expr.App _ _ _ s1 _ ($_)%expr _)) _ | @expr.App _ _ _ s _
+         (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc)
+          (@expr.App _ _ _ s1 _ (@expr.Abs _ _ _ _ _ _) _)) _ | @expr.App _ _
+         _ s _
+         (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc)
+          (@expr.App _ _ _ s1 _ (_ @ _)%expr_pat _)) _ | @expr.App _ _ _ s _
+         (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc)
+          (@expr.App _ _ _ s1 _ (@expr.LetIn _ _ _ _ _ _ _) _)) _ => None
+       | @expr.App _ _ _ s _
+         (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc) ($_)%expr) _ |
+         @expr.App _ _ _ s _
+         (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc)
+          (@expr.Abs _ _ _ _ _ _)) _ | @expr.App _ _ _ s _
+         (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc)
+          (@expr.LetIn _ _ _ _ _ _ _)) _ => None
+       | @expr.App _ _ _ s _
          (@expr.App _ _ _ s0 _
           (@expr.App _ _ _ s1 _ (@expr.Ident _ _ _ t idc) x2) x1) x0 =>
            _ <- invert_bind_args idc Raw.ident.Z_add_with_carry;
@@ -985,8 +1105,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
          _ | @expr.App _ _ _ s _
          (@expr.App _ _ _ s0 _
           (@expr.App _ _ _ s1 _ (@expr.LetIn _ _ _ _ _ _ _) _) _) _ => None
-       | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ #(_)%expr_pat _) _ |
-         @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ ($_)%expr _) _ | @expr.App
+       | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ ($_)%expr _) _ | @expr.App
          _ _ _ s _ (@expr.App _ _ _ s0 _ (@expr.Abs _ _ _ _ _ _) _) _ |
          @expr.App _ _ _ s _
          (@expr.App _ _ _ s0 _ (@expr.LetIn _ _ _ _ _ _ _) _) _ => None