Guard exponentially slow bounds analysis with a flag

With `--fancy-and-powerful-but-exponentially-slow-bounds-analysis`

Idk how to implement a non-exponential PHOAS passe for this.

Author: JasonGross

src/AbstractInterpretation/AbstractInterpretation.v

@@ -0,0 +1,35 @@
+Require Import Rewriter.Language.Language.
+Require Import Rewriter.Language.Wf.
+Require Import Crypto.Language.API.
+Require Import Crypto.Language.WfExtra.
+Require Import Crypto.AbstractInterpretation.Bottomify.AbstractInterpretation.
+Require Import Crypto.AbstractInterpretation.Bottomify.Wf.
+
+Module Compilers.
+  Import Language.Compilers.
+  Import Language.Inversion.Compilers.
+  Import Language.Wf.Compilers.
+  Import Language.API.Compilers.
+  Import Language.WfExtra.Compilers.
+  Import AbstractInterpretation.Bottomify.AbstractInterpretation.Compilers.
+  Import AbstractInterpretation.Bottomify.Wf.Compilers.
+  Import Compilers.API.
+
+  Import AbstractInterpretation.Bottomify.AbstractInterpretation.Compilers.partial.
+  Import AbstractInterpretation.Bottomify.Wf.Compilers.partial.
+
+#[global]
+  Hint Resolve Wf_Eval Wf_EvalWithBound Wf_EtaExpandWithBound Wf_EtaExpandWithListInfoFromBound Wf_StripAnnotations Wf_StripAllAnnotations : wf_extra.
+#[global]
+  Hint Opaque partial.Eval EvalWithBound EtaExpandWithBound EtaExpandWithListInfoFromBound StripAnnotations StripAllAnnotations : wf_extra interp_extra.
+
+#[global]
+  Hint Resolve Wf_PartialEvaluateWithListInfoFromBounds : wf_extra.
+#[global]
+  Hint Opaque PartialEvaluateWithListInfoFromBounds : wf_extra interp_extra.
+
+#[global]
+  Hint Resolve Wf_PartialEvaluateWithBounds : wf_extra.
+#[global]
+  Hint Opaque PartialEvaluateWithBounds : wf_extra interp_extra.
+End Compilers.

src/AbstractInterpretation/Bottomify/AbstractInterpretation.v

@@ -0,0 +1,35 @@
+Require Import Rewriter.Language.Language.
+Require Import Rewriter.Language.Wf.
+Require Import Crypto.Language.API.
+Require Import Crypto.Language.WfExtra.
+Require Import Crypto.AbstractInterpretation.Fancy.AbstractInterpretation.
+Require Import Crypto.AbstractInterpretation.Fancy.Wf.
+
+Module Compilers.
+  Import Language.Compilers.
+  Import Language.Inversion.Compilers.
+  Import Language.Wf.Compilers.
+  Import Language.API.Compilers.
+  Import Language.WfExtra.Compilers.
+  Import AbstractInterpretation.Fancy.AbstractInterpretation.Compilers.
+  Import AbstractInterpretation.Fancy.Wf.Compilers.
+  Import Compilers.API.
+
+  Import AbstractInterpretation.Fancy.AbstractInterpretation.Compilers.partial.
+  Import AbstractInterpretation.Fancy.Wf.Compilers.partial.
+
+#[global]
+  Hint Resolve Wf_Eval Wf_EvalWithBound Wf_EtaExpandWithBound Wf_EtaExpandWithListInfoFromBound Wf_StripAnnotations Wf_StripAllAnnotations : wf_extra.
+#[global]
+  Hint Opaque partial.Eval EvalWithBound EtaExpandWithBound EtaExpandWithListInfoFromBound StripAnnotations StripAllAnnotations : wf_extra interp_extra.
+
+#[global]
+  Hint Resolve Wf_PartialEvaluateWithListInfoFromBounds : wf_extra.
+#[global]
+  Hint Opaque PartialEvaluateWithListInfoFromBounds : wf_extra interp_extra.
+
+#[global]
+  Hint Resolve Wf_PartialEvaluateWithBounds : wf_extra.
+#[global]
+  Hint Opaque PartialEvaluateWithBounds : wf_extra interp_extra.
+End Compilers.

src/AbstractInterpretation/Bottomify/Proofs.v

@@ -4,25 +4,27 @@ Require Import Crypto.Language.API.
 Require Import Crypto.Language.WfExtra.
 Require Import Crypto.AbstractInterpretation.AbstractInterpretation.
 Require Import Crypto.AbstractInterpretation.Wf.
+Require Import Crypto.AbstractInterpretation.Fancy.WfExtra.
+Require Import Crypto.AbstractInterpretation.Bottomify.WfExtra.
 
 Module Compilers.
-  Import Language.Compilers.
-  Import Language.Inversion.Compilers.
-  Import Language.Wf.Compilers.
-  Import Language.API.Compilers.
-  Import Language.WfExtra.Compilers.
+  Export AbstractInterpretation.Fancy.WfExtra.Compilers.
+  Export AbstractInterpretation.Bottomify.WfExtra.Compilers.
   Import AbstractInterpretation.AbstractInterpretation.Compilers.
   Import AbstractInterpretation.Wf.Compilers.
   Import Compilers.API.
 
+  (*
   Import AbstractInterpretation.AbstractInterpretation.Compilers.partial.
   Import AbstractInterpretation.Wf.Compilers.partial.
+   *)
 
+  (*
 #[global]
   Hint Resolve Wf_Eval Wf_EvalWithBound Wf_EtaExpandWithBound Wf_EtaExpandWithListInfoFromBound Wf_StripAnnotations Wf_StripAllAnnotations : wf_extra.
 #[global]
   Hint Opaque partial.Eval EvalWithBound EtaExpandWithBound EtaExpandWithListInfoFromBound StripAnnotations StripAllAnnotations : wf_extra interp_extra.
-
+*)
 #[global]
   Hint Resolve Wf_PartialEvaluateWithListInfoFromBounds : wf_extra.
 #[global]

src/AbstractInterpretation/Bottomify/Wf.v

@@ -20,18 +20,30 @@ Module Compilers.
       Class shiftr_avoid_uint1_opt := shiftr_avoid_uint1 : bool.
 #[global]
       Typeclasses Opaque shiftr_avoid_uint1_opt.
+      Class fancy_and_powerful_but_exponentially_slow_bounds_analysis_opt := fancy_and_powerful_but_exponentially_slow_bounds_analysis : bool.
+      #[global]
+      Typeclasses Opaque fancy_and_powerful_but_exponentially_slow_bounds_analysis_opt.
       Module AbstractInterpretation.
         Local Set Primitive Projections.
         Class Options
           := { shiftr_avoid_uint1 : shiftr_avoid_uint1_opt
+             ; fancy_and_powerful_but_exponentially_slow_bounds_analysis : fancy_and_powerful_but_exponentially_slow_bounds_analysis_opt
              }.
         Definition default_Options : Options
-          := {| shiftr_avoid_uint1 := false |}.
+          := {| shiftr_avoid_uint1 := false
+             ; fancy_and_powerful_but_exponentially_slow_bounds_analysis := false
+             |}.
         Module Export Exports.
           Global Existing Instance Build_Options.
           Global Existing Instance shiftr_avoid_uint1.
-          Global Hint Cut [ ( _ * ) shiftr_avoid_uint1 ( _ * ) Build_Options ] : typeclass_instances.
+          Global Existing Instance fancy_and_powerful_but_exponentially_slow_bounds_analysis.
+          Global Hint Cut [ ( _ * )
+                              ( shiftr_avoid_uint1
+                              | fancy_and_powerful_but_exponentially_slow_bounds_analysis
+                              )
+                              ( _ * ) Build_Options ] : typeclass_instances.
           Global Coercion shiftr_avoid_uint1 : Options >-> shiftr_avoid_uint1_opt.
+          Global Coercion fancy_and_powerful_but_exponentially_slow_bounds_analysis : Options >-> fancy_and_powerful_but_exponentially_slow_bounds_analysis_opt.
         End Exports.
       End AbstractInterpretation.
       Export AbstractInterpretation.Exports.

src/AbstractInterpretation/Bottomify/WfExtra.v

@@ -1375,7 +1375,7 @@ Module Pipeline.
               let e' := fresh "e" in
               destruct v as [e'|e'] eqn:H;
               cbv beta iota in Hrv;
-              [ apply CheckedPartialEvaluateWithBounds_Correct_first_order in H;
+              [ apply CheckedPartialEvaluateWithBounds_Correct in H;
                 [ let Hwf' := fresh "Hwf" in
                   rewrite (correct_of_final_iff_correct_of_initial Hinterp) in H by assumption;
                   destruct H as [? Hwf']; split_and;

src/AbstractInterpretation/Fancy/AbstractInterpretation.v

@@ -417,6 +417,10 @@ Module ForExtraction.
     := ([Arg.long_key "cmovznz-by-mul"], Arg.Unit, ["Use an alternative implementation of cmovznz using multiplication rather than bitwise-and with -1."]).
   Definition shiftr_avoid_uint1_spec : named_argT
     := ([Arg.long_key "shiftr-avoid-uint1"], Arg.Unit, ["Avoid uint1 types at the output of (>>) operations."]).
+  Definition fancy_and_powerful_but_exponentially_slow_bounds_analysis_spec : named_argT
+    := ([Arg.long_key "fancy-and-powerful-but-exponentially-slow-bounds-analysis"],
+         Arg.Unit,
+         ["Use a more powerful bound analysis implementation that is unfortunately exponentially slow in the number of lines of code. If you know how to implement PHOAS passes of type [expr var -> var * expr var] or if you want to reimplement our bounds analysis pass in a first-order expression representation instead of PHOAS, please contact us! See https://github.com/mit-plv/fiat-crypto/pull/1761 for more details."]).
   Definition tight_bounds_multiplier_default := default_tight_upperbound_fraction.
   Definition tight_bounds_multiplier_spec : named_argT
     := ([Arg.long_key "tight-bounds-mul-by"],
@@ -712,6 +716,7 @@ Module ForExtraction.
         ; relax_primitive_carry_to_bitwidth_spec
         ; cmovznz_by_mul_spec
         ; shiftr_avoid_uint1_spec
+        ; fancy_and_powerful_but_exponentially_slow_bounds_analysis_spec
         ; only_signed_spec
         ; hint_file_spec
         ; output_file_spec
@@ -769,6 +774,7 @@ Module ForExtraction.
              , relax_primitive_carry_to_bitwidthv
              , cmovznz_by_mulv
              , shiftr_avoid_uint1v
+             , fancy_and_powerful_but_exponentially_slow_bounds_analysisv
              , only_signedv
              , hint_file_namesv
              , output_file_namev
@@ -849,6 +855,7 @@ Module ForExtraction.
                   ; use_mul_for_cmovznz := to_bool cmovznz_by_mulv
                   ; abstract_interpretation_options :=
                       {| AbstractInterpretation.shiftr_avoid_uint1 := to_bool shiftr_avoid_uint1v
+                      ; AbstractInterpretation.fancy_and_powerful_but_exponentially_slow_bounds_analysis := to_bool fancy_and_powerful_but_exponentially_slow_bounds_analysisv
                       |}
                   ; emit_primitives := negb (to_bool no_primitivesv)
                   ; output_options :=

src/AbstractInterpretation/Fancy/Proofs.v

@@ -468,13 +468,15 @@ Module debugging_21271_from_bytes.
       vm_compute in e.
       set (k'' := CheckedPartialEvaluateWithBounds _ _ _ _ _ _ _) in (value of k).
       cbv [CheckedPartialEvaluateWithBounds] in k''.
+      cbv [AbstractInterpretation.fancy_and_powerful_but_exponentially_slow_bounds_analysis Pipeline.AbstractInterpretation_opts Primitives.Options.absint_opts Primitives.Options.default_PipelineOptions Pipeline.AbstractInterpretation_opts Pipeline.default_BoundsPipelineOptions AbstractInterpretation.default_Options] in k''.
+      cbv [Bottomify.AbstractInterpretation.Compilers.CheckedPartialEvaluateWithBounds] in k''.
       clear -k''.
       cbv [Rewriter.Util.LetIn.Let_In] in k''.
       set (e' := (GeneralizeVar.FromFlat (GeneralizeVar.ToFlat e))) in (value of k'').
       vm_compute in e'; clear e; rename e' into e.
-      set (b := (partial.Extract _ _ _)) in (value of k'').
+      set (b := (Bottomify.AbstractInterpretation.Compilers.partial.Extract _ _ _)) in (value of k'').
       clear -b.
-      cbv [partial.Extract partial.ident.extract partial.extract_gen type.app_curried partial.extract] in b.
+      cbv [Bottomify.AbstractInterpretation.Compilers.partial.Extract partial.ident.extract partial.extract_gen type.app_curried partial.extract] in b.
       subst e.
       cbv beta iota zeta in b.
       Import Rewriter.Util.LetIn.
@@ -1961,6 +1963,8 @@ Module debugging_p256_uint1.
         => set (k' := e) in (value of k)
       end; vm_compute in k'; subst k'.
       cbv [CheckedPartialEvaluateWithBounds] in k.
+      cbv [AbstractInterpretation.fancy_and_powerful_but_exponentially_slow_bounds_analysis Pipeline.AbstractInterpretation_opts Primitives.Options.absint_opts Primitives.Options.default_PipelineOptions Pipeline.AbstractInterpretation_opts Pipeline.default_BoundsPipelineOptions AbstractInterpretation.default_Options] in k.
+      cbv [Bottomify.AbstractInterpretation.Compilers.CheckedPartialEvaluateWithBounds] in k.
       cbv [Rewriter.Util.LetIn.Let_In] in k.
       set (k' := GeneralizeVar.FromFlat (GeneralizeVar.ToFlat _)) in (value of k).
       vm_compute in k'.
@@ -1987,7 +1991,7 @@ Module debugging_p256_uint1.
       cbv [split_multiret_to should_split_multiret should_split_multiret_opt_instance_0] in k.
       vm_compute ZRange.type.base.option.is_tighter_than in k.
       cbv beta iota zeta in k.
-      set (k' := PartialEvaluateWithBounds _ _ _ _ _ _) in (value of k) at 1.
+      set (k' := Bottomify.AbstractInterpretation.Compilers.PartialEvaluateWithBounds _ _ _ _ _ _) in (value of k) at 1.
       vm_compute in k'.
     Abort.
   End __.