Finish reifying list lemmas

After     | File Name                                    | Before    || Change    | % Change
--------------------------------------------------------------------------------------------
22m23.84s | Total                                        | 21m34.63s || +0m49.21s | +3.80%
--------------------------------------------------------------------------------------------
1m52.62s  | RewriterRulesInterpGood.vo                   | 1m37.14s  || +0m15.48s | +15.93%
3m25.91s  | p384_32.c                                    | 3m14.24s  || +0m11.66s | +6.00%
1m32.94s  | RewriterRulesGood.vo                         | 1m42.36s  || -0m09.42s | -9.20%
0m33.72s  | RewriterWf1.vo                               | 0m24.30s  || +0m09.41s | +38.76%
1m17.31s  | Rewriter.vo                                  | 1m12.10s  || +0m05.21s | +7.22%
0m43.01s  | ExtractionHaskell/unsaturated_solinas        | 0m39.84s  || +0m03.16s | +7.95%
0m45.21s  | p521_32.c                                    | 0m42.86s  || +0m02.35s | +5.48%
1m46.30s  | Fancy/Barrett256.vo                          | 1m45.08s  || +0m01.21s | +1.16%
0m38.74s  | p521_64.c                                    | 0m37.49s  || +0m01.25s | +3.33%
0m23.16s  | ExtractionOCaml/word_by_word_montgomery      | 0m21.44s  || +0m01.71s | +8.02%
0m18.74s  | p256_32.c                                    | 0m16.88s  || +0m01.85s | +11.01%
0m15.00s  | ExtractionOCaml/unsaturated_solinas          | 0m13.98s  || +0m01.01s | +7.29%
0m11.92s  | ExtractionOCaml/saturated_solinas            | 0m10.13s  || +0m01.78s | +17.67%
0m07.82s  | ExtractionOCaml/saturated_solinas.ml         | 0m05.98s  || +0m01.83s | +30.76%
1m47.42s  | RewriterWf2.vo                               | 1m47.81s  || -0m00.39s | -0.36%
0m58.35s  | ExtractionHaskell/word_by_word_montgomery    | 0m57.41s  || +0m00.94s | +1.63%
0m45.47s  | RewriterInterpProofs1.vo                     | 0m45.67s  || -0m00.20s | -0.43%
0m37.34s  | Fancy/Montgomery256.vo                       | 0m37.09s  || +0m00.25s | +0.67%
0m36.14s  | PushButtonSynthesis/UnsaturatedSolinas.vo    | 0m36.52s  || -0m00.38s | -1.04%
0m29.91s  | ExtractionHaskell/saturated_solinas          | 0m29.70s  || +0m00.21s | +0.70%
0m26.77s  | PushButtonSynthesis/WordByWordMontgomery.vo  | 0m26.72s  || +0m00.05s | +0.18%
0m25.87s  | SlowPrimeSynthesisExamples.vo                | 0m25.49s  || +0m00.38s | +1.49%
0m18.72s  | p448_solinas_64.c                            | 0m19.16s  || -0m00.44s | -2.29%
0m16.94s  | secp256k1_32.c                               | 0m17.18s  || -0m00.23s | -1.39%
0m13.92s  | p434_64.c                                    | 0m13.08s  || +0m00.83s | +6.42%
0m13.15s  | ExtractionOCaml/word_by_word_montgomery.ml   | 0m12.58s  || +0m00.57s | +4.53%
0m08.97s  | ExtractionOCaml/unsaturated_solinas.ml       | 0m08.95s  || +0m00.02s | +0.22%
0m08.37s  | ExtractionHaskell/word_by_word_montgomery.hs | 0m08.51s  || -0m00.14s | -1.64%
0m08.35s  | p224_32.c                                    | 0m08.10s  || +0m00.25s | +3.08%
0m07.77s  | p384_64.c                                    | 0m07.29s  || +0m00.47s | +6.58%
0m06.92s  | BoundsPipeline.vo                            | 0m06.85s  || +0m00.07s | +1.02%
0m05.70s  | ExtractionHaskell/unsaturated_solinas.hs     | 0m06.14s  || -0m00.43s | -7.16%
0m05.12s  | ExtractionHaskell/saturated_solinas.hs       | 0m06.09s  || -0m00.96s | -15.92%
0m03.53s  | PushButtonSynthesis/Primitives.vo            | 0m03.55s  || -0m00.02s | -0.56%
0m03.38s  | PushButtonSynthesis/SmallExamples.vo         | 0m03.34s  || +0m00.04s | +1.19%
0m03.16s  | PushButtonSynthesis/BarrettReduction.vo      | 0m03.24s  || -0m00.08s | -2.46%
0m03.06s  | PushButtonSynthesis/SaturatedSolinas.vo      | 0m03.23s  || -0m00.16s | -5.26%
0m02.81s  | PushButtonSynthesis/MontgomeryReduction.vo   | 0m02.84s  || -0m00.02s | -1.05%
0m02.62s  | curve25519_32.c                              | 0m02.22s  || +0m00.39s | +18.01%
0m01.88s  | p224_64.c                                    | 0m01.47s  || +0m00.40s | +27.89%
0m01.68s  | curve25519_64.c                              | 0m02.19s  || -0m00.51s | -23.28%
0m01.32s  | CLI.vo                                       | 0m01.33s  || -0m00.01s | -0.75%
0m01.24s  | secp256k1_64.c                               | 0m01.30s  || -0m00.06s | -4.61%
0m01.22s  | p256_64.c                                    | 0m01.47s  || -0m00.25s | -17.00%
0m01.16s  | RewriterProofs.vo                            | 0m01.16s  || +0m00.00s | +0.00%
0m01.10s  | StandaloneHaskellMain.vo                     | 0m01.00s  || +0m00.10s | +10.00%
0m01.05s  | CompilersTestCases.vo                        | 0m01.09s  || -0m00.04s | -3.66%
0m01.04s  | StandaloneOCamlMain.vo                       | 0m01.04s  || +0m00.00s | +0.00%

1 files changed, 108 insertions, 0 deletions

diff --git a/src/SlowPrimeSynthesisExamples.v b/src/SlowPrimeSynthesisExamples.v
index 9bac61295..eb02d9ad6 100644
--- a/src/SlowPrimeSynthesisExamples.v
+++ b/src/SlowPrimeSynthesisExamples.v
@@ -25,6 +25,114 @@ Local Coercion Z.of_nat : nat >-> Z.
 Local Coercion QArith_base.inject_Z : Z >-> Q.
 Local Coercion Z.pos : positive >-> Z.
 
+Module debugging_rewriting.
+  Section __.
+    Context (n : nat := 2%nat)
+            (s : Z := 2^127)
+            (c : list (Z * Z) := [(1,1)])
+            (machine_wordsize : Z := 64).
+
+    Let limbwidth := (Z.log2_up (s - Associational.eval c) / Z.of_nat n)%Q.
+    Let idxs := (List.seq 0 n ++ [0; 1])%list%nat.
+
+    Definition possible_values_of_machine_wordsize
+      := [0; machine_wordsize; 2 * machine_wordsize]%Z.
+
+    Let possible_values := possible_values_of_machine_wordsize.
+
+
+    Let prime_upperbound_list : list Z
+      := encode_no_reduce (weight (Qnum limbwidth) (Qden limbwidth)) n (s-1).
+    Let tight_upperbounds : list Z
+      := List.map
+           (fun v : Z => Qceiling (11/10 * v))
+           prime_upperbound_list.
+    Definition tight_bounds : list (ZRange.type.option.interp base.type.Z)
+      := List.map (fun u => Some r[0~>u]%zrange) tight_upperbounds.
+    Definition loose_bounds : list (ZRange.type.option.interp base.type.Z)
+      := List.map (fun u => Some r[0 ~> 3*u]%zrange) tight_upperbounds.
+
+
+    Let limbwidth_num := Eval vm_compute in Qnum limbwidth.
+    Let limbwidth_den := Eval vm_compute in QDen limbwidth.
+
+    Compute
+      (Pipeline.BoundsPipeline
+         true None [64; 128]
+         ltac:(let r := Reify (fun f g
+                               => (  (addmod limbwidth_num limbwidth_den n f g)
+                              )) in
+               exact r)
+                (Some (repeat (@None _) n), (Some (repeat (@None _) n), tt))
+                ZRange.type.base.option.None).
+
+    Compute
+      (Pipeline.BoundsPipeline
+         true None [64; 128]
+         ltac:(let r := Reify (fun f g
+                               => (  (add (weight limbwidth_num limbwidth_den) n f g)
+                              )) in
+               exact r)
+                (Some (repeat (@None _) n), (Some (repeat (@None _) n), tt))
+                ZRange.type.base.option.None).
+
+    Compute
+      (Pipeline.BoundsPipeline
+         true None [64; 128]
+         ltac:(let r := Reify (fun f g
+                               => let a_a := to_associational (weight limbwidth_num limbwidth_den) n f in
+                                  let b_a := to_associational (weight limbwidth_num limbwidth_den) n g in from_associational (weight limbwidth_num limbwidth_den) n (a_a ++ b_a)
+                              ) in
+               exact r)
+                (Some (repeat (@None _) n), (Some (repeat (@None _) n), tt))
+                ZRange.type.base.option.None).
+
+    Compute
+      (Pipeline.BoundsPipeline
+         true None [64; 128]
+         ltac:(let r := Reify (fun f (g : list Z)
+                               => let a_a := to_associational (weight limbwidth_num limbwidth_den) n f in
+                                  a_a) in
+               exact r)
+                (Some (repeat (@None _) n), (Some (repeat (@None _) n), tt))
+                ZRange.type.base.option.None).
+
+    Compute
+      (Pipeline.BoundsPipeline
+         true None [64; 128]
+         ltac:(let r := Reify (fun (f g : list Z)
+                               => let a_a := combine (map (weight limbwidth_num limbwidth_den) (seq 0 n)) f in
+                                  a_a) in
+               exact r)
+                (Some (repeat (@None _) n), (Some (repeat (@None _) n), tt))
+                ZRange.type.base.option.None).
+
+    Definition foo := (Pipeline.BoundsPipeline
+                         true None [64; 128]
+                         ltac:(let r := Reify (combine [1; 2] [1; 2]) in
+                               exact r)
+                                tt
+                                ZRange.type.base.option.None).
+
+  (*
+  Goal True.
+    pose foo as X; cbv [foo] in X.
+    clear -X.
+    cbv [Pipeline.BoundsPipeline LetIn.Let_In] in X.
+    set (Y := (PartialEvaluateWithListInfoFromBounds _ _)) in (value of X).
+    vm_compute in Y.
+    subst Y; set (Y := (Rewriter.Compilers.PartialEvaluate _)) in (value of X).
+    cbv [Rewriter.Compilers.PartialEvaluate Rewriter.Compilers.RewriteRules.RewriteNBE Rewriter.Compilers.RewriteRules.Compile.Rewrite Rewriter.Compilers.RewriteRules.Compile.rewrite] in Y.
+    clear -Y.
+    change (Rewriter.Compilers.RewriteRules.nbe_default_fuel) with (S (pred Rewriter.Compilers.RewriteRules.nbe_default_fuel)) in (value of Y).
+    cbn [Rewriter.Compilers.RewriteRules.Compile.repeat_rewrite] in Y.
+    cbv [Rewriter.Compilers.RewriteRules.Compile.rewrite_bottomup] in Y.
+    Print Rewriter.Compilers.RewriteRules.nbe_rewrite_head.
+  Abort.
+   *)
+  End __.
+End debugging_rewriting.
+
 Section debugging_p448.
   Context (n : nat := 8%nat)
           (s : Z := 2^448)