debugging...

src/AbstractInterpretation/AbstractInterpretation.v

@@ -1,3 +1,4 @@
+Require Import ReductionEffect.PrintingEffect.
 Require Import Coq.ZArith.ZArith.
 Require Import Crypto.Util.ListUtil Coq.Lists.List Crypto.Util.ListUtil.FoldBool.
 Require Import Crypto.Util.ZRange.
@@ -122,29 +123,57 @@ Module Compilers.
            | None => false
            end.
 
+      Definition invert_Base {base_type ident var T} (u : @UnderLets.UnderLets base_type ident var T) : option T :=
+        match u with
+        | Base v => Some v
+        | _ => None
+        end.
+
+      Definition invert_base_value {t} : value t -> option (abstract_domain t * @expr var t) :=
+        match t return value t -> option (abstract_domain t * expr t)
+        with type.base t => fun ve => Some (ve) | _ => fun _ => None end.
+
+      Notation invert_bounds x := (option_map (option_map fst) (option_map invert_base_value (invert_Base x))).
+      Notation invert_base_bounds x := (option_map fst (invert_base_value x)).
+
+      Import Coq.Strings.String.
       Fixpoint interp (annotate_with_state : bool) {t} (e : @expr value_with_lets t) : value_with_lets t
         := let annotate_with_state := annotate_with_state && negb (skip_annotations_for_App e) in
            match e in expr.expr t return value_with_lets t with
            | expr.Ident t idc => interp_ident annotate_with_state _ idc (* Base (reflect (###idc) (abstract_interp_ident _ idc))*)
            | expr.Var t v => v
-           | expr.Abs s d f => Base (fun x => @interp annotate_with_state d (f (Base x)))
+           | expr.Abs s d f => Base (fun x => let y := @interp annotate_with_state d (f (Base x)) in
+           (* let __ := print ("Abs", f, "^&", y) in *)
+                y)
            | expr.App (type.base s) d f x
              => (x' <-- @interp annotate_with_state _ x;
                    f' <-- @interp annotate_with_state (_ -> d)%etype f;
-                   f' x')
+                   let f'x' := f' x' in
+                   let __ :=
+                     match d, invert_AppIdent_curried e with
+                     | type.base d, Some (existT _ (idc, args)) =>
+                         print ("App bounds", idc, d, "!@", x, "@#", invert_base_bounds x', "!=", (invert_bounds f'x'))
+                     | _, Some (existT _ (idc, args)) =>
+                         print ("App bounds", idc, d, "!@", x, "@#", invert_base_bounds x', "!:")
+                     | _, _ => tt
+                     end in
+                   f'x')
            | expr.App (type.arrow s' d') d f x
              => (x' <-- @interp annotate_with_state (s' -> d')%etype x;
                    x'' <-- bottomify x';
                    f' <-- @interp annotate_with_state (_ -> d)%etype f;
-                   f' x'')
+                   let f'x'' := f' x'' in
+                   (* let __ := print ("App arrow", f, "^@", x, "^#", x'', "^=", f'x'') in *)
+                   f'x'')
            | expr.LetIn (type.arrow _ _) B x f
              => (x' <-- @interp annotate_with_state _ x;
                    @interp annotate_with_state _ (f (Base x')))
            | expr.LetIn (type.base A) B x f
              => (x' <-- @interp annotate_with_state _ x;
+                 let __ := print ("LetIn bounds for", x, "!%", invert_base_bounds x') in
                    x'' <-- reify annotate_with_state true (* this forces a let-binder here *) x' tt;
                    @interp annotate_with_state _ (f (Base (reflect annotate_with_state x'' (state_of_value x')))))
-           end%under_lets.
+           end%under_lets%string.
 
       Definition eval_with_bound' (annotate_with_state : bool) {t} (e : @expr value_with_lets t)
                  (st : type.for_each_lhs_of_arrow abstract_domain t)

src/AbstractInterpretation/ZRange.v

@@ -1,3 +1,4 @@
+Require Import ReductionEffect.PrintingEffect. Require Import Coq.Strings.String.
 Require Import Coq.micromega.Lia.
 Require Import Coq.ZArith.ZArith.
 Require Import Crypto.Util.ListUtil Coq.Lists.List Crypto.Util.ListUtil.FoldBool.
@@ -642,7 +643,7 @@ Module Compilers.
                => fun t f b
                  => match b with
                    | Some b => if b then t tt else f tt
-                   | None => type.base.option.union (t tt) (f tt)
+                   | None => type.base.option.union (let ttt := t tt in let __ := print ("LEFT"%string, ttt) in ttt) (let ftt := f tt in let __ := print ("RIGHT"%string, ftt) in ftt)
                    end
              | ident.bool_rect_nodep _
                => fun t f b

src/SlowPrimeSynthesisExamples.v

@@ -1,3 +1,6 @@
+Set Printing Width 3999999.
+Set Printing Depth 3999999.
+
 Require Import Coq.ZArith.ZArith.
 Require Import Coq.QArith.QArith.
 Require Import Coq.QArith.Qround.
@@ -73,7 +76,7 @@ Module debugging_sat_solinas_25519.
     Local Instance : no_select_size_opt := no_select_size_of_no_select machine_wordsize.
     Local Instance : split_mul_to_opt := split_mul_to_of_should_split_mul machine_wordsize possible_values.
     Local Instance : split_multiret_to_opt := split_multiret_to_of_should_split_multiret machine_wordsize possible_values.
-    Let n : nat := 4.
+    Let n : nat := 2.
     Let boundsn : list (ZRange.type.option.interp base.type.Z) := repeat (Some r[0 ~> (2^machine_wordsize - 1)]%zrange) n.
 
     Import IdentifiersBasicGENERATED.Compilers.
@@ -84,6 +87,136 @@ Module debugging_sat_solinas_25519.
 
     Definition bound (_ : Datatypes.nat) := Z.to_pos (2^64).
 
+    Local Instance : debug_rewriting_opt := false.
+    Local Instance : PHOAS.with_all_casts := true.
+
+    Import PrintingEffect.
+Eval compute in
+  let __ := PrintingEffect.print (1+1) in O.
+    Eval compute in
+         (Pipeline.BoundsPipelineToString
+            "fiat_" "fe4_mul_no_reduce"
+            false (* subst01 *)
+            false (* inline *)
+            possible_values
+            machine_wordsize
+            ltac:(let e := constr:(mul bound) in
+                  let e := eval cbv delta [mulmod mul add_mul add_mul_limb_ add_mul_limb reduce' add_mul_limb' stream.map weight stream.prefixes] in e in
+                  let r := Reify e in
+                  exact r)
+                   (fun _ _ => []) (* comment *)
+                   (Some boundsn, (Some boundsn, tt))
+                   (None)
+                   (None, (None, tt))
+                   (None)).
+
+
+  compute in e.
+
+    cbv [Pipeline.BoundsPipelineToString Pipeline.BoundsPipelineToStringWithDebug Pipeline.BoundsPipelineToStringsWithDebug Pipeline.BoundsPipelineToExtendedResult   Pipeline.BoundsPipelineWithDebug Pipeline.PreBoundsPipeline] in e.
+    cbv [Rewriter.Util.LetIn.Let_In DebugMonad.Debug.eval_result DebugMonad.Debug.sequence Pipeline.debug_after_rewrite DebugMonad.Debug.ret] in *.
+    cbv [Pipeline.wrap_debug_rewrite Pipeline.debug_after_rewrite Pipeline.debug_rewriting debug_rewriting_opt_instance_0] in *.
+    cbv [Rewriter.Util.LetIn.Let_In DebugMonad.Debug.eval_result DebugMonad.Debug.sequence Pipeline.debug_after_rewrite DebugMonad.Debug.ret] in *.
+    cbn [DebugMonad.Debug.bind fst snd] in *.
+    cbv [Pipeline.unfold_value_barrier].
+    set (PartialEvaluateWithListInfoFromBounds _ _) in (value of e).
+    set (CheckedPartialEvaluateWithBounds _ _  _ _ _ _ _) as cpe in (value of e) at 1.
+    clear -cpe.
+    set (GeneralizeVar.FromFlat _) as cve in (value of cpe).
+    vm_compute in cve.
+    clear -cpe.
+
+    cbv [CheckedPartialEvaluateWithBounds] in cpe.
+    Locate "dlet".
+    cbv [Rewriter.Util.LetIn.Let_In] in *.
+    vm_compute CheckCasts.GetUnsupportedCasts in (value of cpe); cbv match beta in cpe.
+    vm_compute ZRange.type.base.option.is_tighter_than in cpe; cbv match beta in cpe.
+    cbv [PartialEvaluateWithBounds partial.EvalWithBound partial.eval_with_bound ] in *.
+
+    set (fun var : _ => _) in (value of cpe) at 2.
+    epose _ as var; clearbody var.
+    epose (y var).
+    subst y.
+    clear cpe.
+    cbv beta in *.
+
+    set (GeneralizeVar.GeneralizeVar _ _) in (value of e).
+    vm_compute in e0; clear -e.
+    cbv [partial.ident.eval_with_bound partial.eval_with_bound' ] in e.
+
+    subst e0.
+
+    progress cbv beta zeta delta [partial.interp] in e.
+    cbv iota in e.
+    cbv beta in e.
+    cbv iota in e.
+    cbv beta in e.
+    cbv iota in e.
+    cbv beta in e.
+    cbv iota in e.
+    cbv beta in e.
+    cbv iota in e.
+    cbv beta in e.
+    set (fun _ => _) in (value of e) at 1.
+    cbn [partial.interp UnderLets.splice UnderLets.to_expr partial.reify andb] in e.
+
+    subst y.
+    cbv beta in e.
+
+    progress cbv beta delta [partial.interp] in e.
+    cbn [partial.interp UnderLets.splice UnderLets.to_expr partial.reify andb] in e.
+
+    set (fun var : _ => _) in (value of e0) at 7.
+    subst e0.
+    cbn [partial.interp UnderLets.splice UnderLets.to_expr partial.reify andb] in e.
+
+    set (fun var : _ => _) in (value of e) at 7.
+    epose (y0 _).
+    subst y0.
+    clear e.
+    cbv beta in *.
+
+    set (y _) in (value of e0).
+    subst y.
+    vm_compute partial.skip_annotations_for_App in (value of e0).
+    cbv beta in *.
+
+    clear -e0.
+
+    rename e into x.
+    rename e0 into e.
+    rename x into e0.
+
+
+    set (fun var : _ => _) in (value of e0) at 7.
+    subst e0.
+    cbn [partial.interp UnderLets.splice UnderLets.to_expr partial.reify andb] in e.
+
+    set (fun var : _ => _) in (value of e) at 7.
+    epose (y0 _).
+    subst y0.
+    clear e.
+    cbv beta in *.
+
+    set (y _) in (value of e0).
+    subst y.
+    vm_compute partial.skip_annotations_for_App in (value of e0).
+    clear cve.
+    revert e0.
+    repeat match goal with H : _ |- _ => clear H end.
+    intros.
+
+
+
+    cbv beta in e.
+
+
+    vm_compute in cpe.
+    clear -cpe.
+    cbv [tree.smart_app] in *.
+    clear e.
+    vm_compute in e0.
+
     (*
     Definition mulmod (c : BinNums.Z := 38) (a b : list BinNums.Z) :=
       let p := mul bound a b in
@@ -266,26 +399,6 @@ Module debugging_sat_solinas_25519.
                    (None, tt)
                    (None, None)).
 
-    Time Redirect "log"
-         Compute
-         Show.show (* [show] for pretty-printing of the AST without needing lots of imports *)
-         (Pipeline.BoundsPipelineToString
-            "fiat_" "fe4_mul_no_reduce"
-            false (* subst01 *)
-            false (* inline *)
-            possible_values
-            machine_wordsize
-            ltac:(let e := constr:(mul bound) in
-                  let e := eval cbv delta [mulmod mul add_mul add_mul_limb_ add_mul_limb reduce' add_mul_limb' stream.map weight stream.prefixes] in e in
-                  let r := Reify e in
-                  exact r)
-                   (fun _ _ => []) (* comment *)
-                   (Some boundsn, (Some boundsn, tt))
-                   (Some (boundsn++boundsn))
-                   (None, (None, tt))
-                   (None)
-          : Pipeline.ErrorT _).
-
     Time Redirect "log"
          Compute
          Show.show (* [show] for pretty-printing of the AST without needing lots of imports *)