Remove fastpath for Zcast in absint

Yet another premature optimization

After     | File Name                                                            | Before    || Change    | % Change
--------------------------------------------------------------------------------------------------------------------
17m43.04s | Total                                                                | 17m43.59s || -0m00.55s | -0.05%
--------------------------------------------------------------------------------------------------------------------
0m21.28s  | p384_32.c                                                            | 0m22.70s  || -0m01.41s | -6.25%
5m51.41s  | Experiments/NewPipeline/SlowPrimeSynthesisExamples                   | 5m50.56s  || +0m00.84s | +0.24%
4m31.08s  | Experiments/NewPipeline/Toplevel1                                    | 4m31.11s  || -0m00.03s | -0.01%
1m34.67s  | Experiments/NewPipeline/Toplevel2                                    | 1m34.92s  || -0m00.25s | -0.26%
0m45.41s  | Experiments/NewPipeline/AbstractInterpretationProofs                 | 0m45.86s  || -0m00.45s | -0.98%
0m38.24s  | p521_32.c                                                            | 0m37.64s  || +0m00.60s | +1.59%
0m37.06s  | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery      | 0m37.39s  || -0m00.32s | -0.88%
0m34.56s  | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery    | 0m35.06s  || -0m00.50s | -1.42%
0m31.74s  | p521_64.c                                                            | 0m31.42s  || +0m00.31s | +1.01%
0m20.95s  | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas        | 0m20.43s  || +0m00.51s | +2.54%
0m18.93s  | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas          | 0m18.77s  || +0m00.16s | +0.85%
0m13.72s  | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas          | 0m13.65s  || +0m00.07s | +0.51%
0m12.63s  | Experiments/NewPipeline/CStringification                             | 0m12.67s  || -0m00.03s | -0.31%
0m10.71s  | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas            | 0m10.43s  || +0m00.28s | +2.68%
0m08.56s  | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery.ml   | 0m08.58s  || -0m00.01s | -0.23%
0m08.12s  | p384_64.c                                                            | 0m08.36s  || -0m00.24s | -2.87%
0m05.48s  | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery.hs | 0m05.42s  || +0m00.06s | +1.10%
0m05.48s  | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas.ml       | 0m05.58s  || -0m00.09s | -1.79%
0m04.01s  | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.hs     | 0m03.95s  || +0m00.05s | +1.51%
0m03.80s  | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas.ml         | 0m03.94s  || -0m00.14s | -3.55%
0m03.35s  | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas.hs       | 0m03.28s  || +0m00.07s | +2.13%
0m03.21s  | p256_32.c                                                            | 0m03.26s  || -0m00.04s | -1.53%
0m03.21s  | secp256k1_32.c                                                       | 0m03.26s  || -0m00.04s | -1.53%
0m01.95s  | curve25519_32.c                                                      | 0m01.91s  || +0m00.04s | +2.09%
0m01.91s  | p224_32.c                                                            | 0m01.80s  || +0m00.10s | +6.11%
0m01.51s  | secp256k1_64.c                                                       | 0m01.54s  || -0m00.03s | -1.94%
0m01.43s  | p224_64.c                                                            | 0m01.44s  || -0m00.01s | -0.69%
0m01.41s  | p256_64.c                                                            | 0m01.46s  || -0m00.05s | -3.42%
0m01.33s  | Experiments/NewPipeline/CLI                                          | 0m01.36s  || -0m00.03s | -2.20%
0m01.33s  | curve25519_64.c                                                      | 0m01.30s  || +0m00.03s | +2.30%
0m01.24s  | Experiments/NewPipeline/StandaloneOCamlMain                          | 0m01.15s  || +0m00.09s | +7.82%
0m01.23s  | Experiments/NewPipeline/StandaloneHaskellMain                        | 0m01.22s  || +0m00.01s | +0.81%
0m01.06s  | Experiments/NewPipeline/CompilersTestCases                           | 0m01.03s  || +0m00.03s | +2.91%
0m01.03s  | Experiments/NewPipeline/AbstractInterpretation                       | 0m01.15s  || -0m00.11s | -10.43%

2 files changed, 4 insertions, 37 deletions

diff --git a/src/Experiments/NewPipeline/AbstractInterpretation.v b/src/Experiments/NewPipeline/AbstractInterpretation.v
index 8f55400a3..e6ca7ebc8 100644
--- a/src/Experiments/NewPipeline/AbstractInterpretation.v
+++ b/src/Experiments/NewPipeline/AbstractInterpretation.v
@@ -913,25 +913,8 @@ Module Compilers.
           : @expr var t
           := @eta_expand_with_bound' base.type ident var abstract_domain' annotate bottom' t e st.
 
-        Section extract.
-          Local Notation bottom := (@bottom base.type abstract_domain' bottom').
-          Definition ident_extract {t} (idc : ident t) : abstract_domain t
-            := match idc in ident.ident t return abstract_domain t with
-               | ident.Literal _ _ as idc
-               | ident.nil _ as idc
-               | ident.cons _ as idc
-               | ident.pair _ _ as idc
-                 => abstract_interp_ident _ idc
-               | ident.Z_cast _ as idc
-               | ident.Z_cast2 _ as idc
-                 => (* fast-path for cast: don't bother with the abstract state of the argument *)
-                 fun _ => abstract_interp_ident _ idc (bottom' _)
-               | _ => bottom
-               end.
-
-          Definition extract {t} (e : @expr _ t) (bound : type.for_each_lhs_of_arrow abstract_domain t) : abstract_domain' (type.final_codomain t)
-            := @extract_gen base.type ident abstract_domain' (@ident_extract) t e bound.
-        End extract.
+        Definition extract {t} (e : @expr _ t) (bound : type.for_each_lhs_of_arrow abstract_domain t) : abstract_domain' (type.final_codomain t)
+          := @extract_gen base.type ident abstract_domain' abstract_interp_ident t e bound.
       End with_var.
     End ident.
 
@@ -999,9 +982,9 @@ Module Compilers.
       Definition EtaExpandWithListInfoFromBound {t} (e : Expr t) (bound : type.for_each_lhs_of_arrow abstract_domain t) : Expr t
         := EtaExpandWithBound e (type.map_for_each_lhs_of_arrow (@ZRange.type.option.strip_ranges) bound).
       Definition extract {t} (e : expr t) (bound : type.for_each_lhs_of_arrow abstract_domain t) : abstract_domain' (type.final_codomain t)
-        := @partial.ident.extract abstract_domain' bottom' abstract_interp_ident t e bound.
+        := @partial.ident.extract abstract_domain' abstract_interp_ident t e bound.
       Definition Extract {t} (e : Expr t) (bound : type.for_each_lhs_of_arrow abstract_domain t) : abstract_domain' (type.final_codomain t)
-        := @partial.ident.extract abstract_domain' bottom' abstract_interp_ident t (e _) bound.
+        := @partial.ident.extract abstract_domain' abstract_interp_ident t (e _) bound.
     End specialized.
   End partial.
 
diff --git a/src/Experiments/NewPipeline/AbstractInterpretationProofs.v b/src/Experiments/NewPipeline/AbstractInterpretationProofs.v
index f806aea25..8a5905d92 100644
--- a/src/Experiments/NewPipeline/AbstractInterpretationProofs.v
+++ b/src/Experiments/NewPipeline/AbstractInterpretationProofs.v
@@ -759,22 +759,6 @@ Module Compilers.
           Qed.
 
           Section extract.
-            Local Notation ident_extract := (@ident.ident_extract abstract_domain' bottom' abstract_interp_ident).
-            Global Instance ident_extract_Proper {t}
-              : Proper (eq ==> abstract_domain_R) (@ident_extract t).
-            Proof.
-              intros idc idc' ?; subst idc'.
-              destruct idc; cbn [ident.ident_extract];
-                repeat first [ refine (abstract_interp_ident_Proper _ _ _ eq_refl)
-                             | eapply bottom_Proper
-                             | eapply bottom'_Proper
-                             | progress cbn [type.related abstract_domain'_R]
-                             | progress cbv [respectful]
-                             | progress intros
-                             | refine (abstract_interp_ident_Proper (type.arrow (type.base _) (type.base _)) _ _ eq_refl _ _ _)
-                             | progress cbv [type.related abstract_domain_R] ].
-            Qed.
-
           (*
             Definition extract {t} (e : @expr _ t) (bound : type.for_each_lhs_of_arrow abstract_domain t) : abstract_domain' (type.final_codomain t)
               := @extract_gen base.type ident abstract_domain' (@ident_extract) t e bound.