Don't fuse annotations

It was causing issues with proving things, and isn't really needed.

Instead, we just check if the current annotation is exactly the state
we're attempting to annotate with; if it is, then we don't double up on
identical annotations.

After     | File Name                                                            | Before    || Change    | % Change
--------------------------------------------------------------------------------------------------------------------
17m54.46s | Total                                                                | 17m52.24s || +0m02.21s | +0.20%
--------------------------------------------------------------------------------------------------------------------
5m55.78s  | Experiments/NewPipeline/SlowPrimeSynthesisExamples                   | 5m55.41s  || +0m00.37s | +0.10%
4m32.97s  | Experiments/NewPipeline/Toplevel1                                    | 4m33.59s  || -0m00.62s | -0.22%
1m35.89s  | Experiments/NewPipeline/Toplevel2                                    | 1m35.77s  || +0m00.11s | +0.12%
0m39.24s  | p521_32.c                                                            | 0m38.50s  || +0m00.74s | +1.92%
0m38.16s  | Experiments/NewPipeline/AbstractInterpretationWf                     | 0m38.52s  || -0m00.36s | -0.93%
0m37.42s  | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery      | 0m37.34s  || +0m00.07s | +0.21%
0m34.59s  | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery    | 0m34.58s  || +0m00.01s | +0.02%
0m32.58s  | p521_64.c                                                            | 0m31.97s  || +0m00.60s | +1.90%
0m23.66s  | p384_32.c                                                            | 0m23.63s  || +0m00.03s | +0.12%
0m21.02s  | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas        | 0m20.88s  || +0m00.14s | +0.67%
0m18.92s  | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas          | 0m18.84s  || +0m00.08s | +0.42%
0m13.91s  | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas          | 0m13.99s  || -0m00.08s | -0.57%
0m12.56s  | Experiments/NewPipeline/CStringification                             | 0m12.61s  || -0m00.04s | -0.39%
0m10.51s  | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas            | 0m10.66s  || -0m00.15s | -1.40%
0m08.55s  | p384_64.c                                                            | 0m08.46s  || +0m00.08s | +1.06%
0m08.51s  | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery.ml   | 0m08.61s  || -0m00.09s | -1.16%
0m05.59s  | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery.hs | 0m05.56s  || +0m00.03s | +0.53%
0m05.43s  | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas.ml       | 0m05.34s  || +0m00.08s | +1.68%
0m04.00s  | Experiments/NewPipeline/AbstractInterpretationProofs                 | 0m03.07s  || +0m00.93s | +30.29%
0m04.00s  | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.hs     | 0m04.04s  || -0m00.04s | -0.99%
0m03.91s  | secp256k1_32.c                                                       | 0m03.93s  || -0m00.02s | -0.50%
0m03.87s  | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas.ml         | 0m03.84s  || +0m00.03s | +0.78%
0m03.84s  | p256_32.c                                                            | 0m03.78s  || +0m00.06s | +1.58%
0m03.33s  | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas.hs       | 0m03.32s  || +0m00.01s | +0.30%
0m02.12s  | p224_32.c                                                            | 0m02.10s  || +0m00.02s | +0.95%
0m02.11s  | curve25519_32.c                                                      | 0m02.03s  || +0m00.08s | +3.94%
0m01.56s  | p256_64.c                                                            | 0m01.55s  || +0m00.01s | +0.64%
0m01.53s  | p224_64.c                                                            | 0m01.55s  || -0m00.02s | -1.29%
0m01.50s  | secp256k1_64.c                                                       | 0m01.51s  || -0m00.01s | -0.66%
0m01.44s  | curve25519_64.c                                                      | 0m01.51s  || -0m00.07s | -4.63%
0m01.38s  | Experiments/NewPipeline/CLI                                          | 0m01.22s  || +0m00.15s | +13.11%
0m01.30s  | Experiments/NewPipeline/StandaloneHaskellMain                        | 0m01.16s  || +0m00.14s | +12.06%
0m01.25s  | Experiments/NewPipeline/StandaloneOCamlMain                          | 0m01.25s  || +0m00.00s | +0.00%
0m01.04s  | Experiments/NewPipeline/CompilersTestCases                           | 0m01.08s  || -0m00.04s | -3.70%
0m01.00s  | Experiments/NewPipeline/AbstractInterpretation                       | 0m01.05s  || -0m00.05s | -4.76%

1 files changed, 28 insertions, 25 deletions

diff --git a/src/Experiments/NewPipeline/AbstractInterpretation.v b/src/Experiments/NewPipeline/AbstractInterpretation.v
index 10590c02b..b673d630f 100644
--- a/src/Experiments/NewPipeline/AbstractInterpretation.v
+++ b/src/Experiments/NewPipeline/AbstractInterpretation.v
@@ -790,31 +790,18 @@ Module Compilers.
                 (abstract_interp_ident : forall t, ident t -> type.interp abstract_domain' t)
                 (update_literal_with_state : forall A : base.type.base, abstract_domain' A -> base.interp A -> base.interp A)
                 (extract_list_state : forall A, abstract_domain' (base.type.list A) -> option (list (abstract_domain' A)))
-                (is_annotation : forall t, ident t -> bool)
-        (*(do_again : forall t : base.type, @expr var t -> UnderLets (@expr var t))*).
+                (is_annotated_for : forall t t', ident t -> abstract_domain' t' -> bool).
 
         (** TODO: Is it okay to commute annotations? *)
         Definition update_annotation {t} (st : abstract_domain' t) (e : @expr var t) : @expr var t
-          := match e with
-             | (#cst' @ e')
-               => if is_annotation _ cst'
-                 then match type.try_transport base.try_make_transport_cps ident _ (t -> t) cst', type.try_transport base.try_make_transport_cps _ _ _ e' with
-                      | Some cst'', Some e''
-                        => match annotate_ident _ (abstract_interp_ident _ cst'' st) with
-                          | Some cst''' => ###cst''' @ e''
-                          | None => e
-                          end%expr
-                      | _, _ => e
-                      end
-                 else match annotate_ident _ st with
-                      | Some cst => ###cst @ e
-                      | None => e
-                      end%expr
-             | _ => match annotate_ident _ st with
-                   | Some cst => ###cst @ e
-                   | None => e
-                   end%expr
-             end%expr_pat.
+          := match e, annotate_ident _ st with
+             | (#cst' @ e'), Some cst
+               => if is_annotated_for _ _ cst' st
+                  then e
+                  else ###cst @ e
+             | _, Some cst => ###cst @ e
+             | _, None => e
+             end%expr_pat%expr.
 
         Definition annotate_with_ident (is_let_bound : bool) {t}
                    (st : abstract_domain' t) (e : @expr var t)
@@ -934,6 +921,22 @@ Module Compilers.
              => fun '(sta, stb) => sta' <- sta; stb' <- stb; Some (ident.Z_cast2 (sta', stb'))
            | _ => fun _ => None
            end%option%etype.
+      Definition is_annotated_for t t' (idc : ident t) : abstract_domain' t' -> bool
+        := match idc, t' with
+           | ident.Z_cast r, base.type.type_base base.type.Z
+             => fun r'
+                => match r' with
+                   | Some r' => zrange_beq r r'
+                   | None => false
+                   end
+           | ident.Z_cast2 (r1, r2), base.type.prod (base.type.type_base base.type.Z) (base.type.type_base base.type.Z)
+             => fun '(r1', r2')
+                => match r1', r2' with
+                   | Some r1', Some r2' => zrange_beq r1 r1' && zrange_beq r2 r2'
+                   | _, _ => false
+                   end
+           | _, _ => fun _ => false
+           end.
       Definition is_annotation t (idc : ident t) : bool
         := match idc with
            | ident.Z_cast _
@@ -966,13 +969,13 @@ Module Compilers.
 
       Definition eval {var} {t} (e : @expr _ t) : expr t
         := (@partial.ident.eval)
-             var abstract_domain' annotate_ident bottom' abstract_interp_ident update_literal_with_state extract_list_state is_annotation t e.
+             var abstract_domain' annotate_ident bottom' abstract_interp_ident update_literal_with_state extract_list_state is_annotated_for t e.
       Definition eval_with_bound {var} {t} (e : @expr _ t) (bound : type.for_each_lhs_of_arrow abstract_domain t) : expr t
         := (@partial.ident.eval_with_bound)
-             var abstract_domain' annotate_ident bottom' abstract_interp_ident update_literal_with_state extract_list_state is_annotation t e bound.
+             var abstract_domain' annotate_ident bottom' abstract_interp_ident update_literal_with_state extract_list_state is_annotated_for t e bound.
       Definition eta_expand_with_bound {var} {t} (e : @expr _ t) (bound : type.for_each_lhs_of_arrow abstract_domain t) : expr t
         := (@partial.ident.eta_expand_with_bound)
-             var abstract_domain' annotate_ident bottom' abstract_interp_ident update_literal_with_state extract_list_state is_annotation t e bound.
+             var abstract_domain' annotate_ident bottom' abstract_interp_ident update_literal_with_state extract_list_state is_annotated_for t e bound.
       Definition Eval {t} (e : Expr t) : Expr t
         := fun var => eval (e _).
       Definition EvalWithBound {t} (e : Expr t) (bound : type.for_each_lhs_of_arrow abstract_domain t) : Expr t