Factor out some of the preglue synthesis code

This makes it a bit more uniform, and hopefully more automatable and
packageable.  Unfortunately, there's still no spec for this part of the
pipeline, so the tactics simply aggregate common patterns.

Alas, this also makes things a bit slower; I suspect that [Defined] is
the place where things are slower.

After     | File Name                                          | Before    || Change
---------------------------------------------------------------------------------------
13m51.14s | Total                                              | 12m59.29s || +0m51.84s
---------------------------------------------------------------------------------------
1m54.18s  | Specific/IntegrationTestKaratsubaMul               | 1m43.12s  || +0m11.06s
1m38.97s  | Specific/IntegrationTestLadderstep130              | 1m30.26s  || +0m08.70s
2m19.75s  | Specific/NISTP256/AMD64/femul                      | 2m14.08s  || +0m05.66s
0m39.90s  | Specific/IntegrationTestMontgomeryP256_128         | 0m34.21s  || +0m05.68s
0m21.95s  | Specific/NISTP256/AMD64/fesub                      | 0m19.23s  || +0m02.71s
0m21.37s  | Specific/NISTP256/AMD64/feadd                      | 0m18.82s  || +0m02.55s
0m21.02s  | Specific/X25519/C64/femul                          | 0m18.32s  || +0m02.69s
0m20.53s  | Specific/IntegrationTestFreeze                     | 0m23.26s  || -0m02.73s
0m18.28s  | Specific/IntegrationTestMontgomeryP256_128_Sub     | 0m15.32s  || +0m02.96s
0m18.20s  | Specific/IntegrationTestMontgomeryP256_128_Add     | 0m15.52s  || +0m02.67s
0m16.35s  | Specific/IntegrationTestMontgomeryP256_128_Opp     | 0m13.52s  || +0m02.83s
0m13.92s  | Specific/IntegrationTestMontgomeryP256_128_Nonzero | 0m11.84s  || +0m02.08s
0m18.23s  | Specific/NISTP256/AMD64/MontgomeryP256             | 0m16.62s  || +0m01.60s
0m15.54s  | Specific/IntegrationTestSub                        | 0m14.53s  || +0m01.00s
0m14.78s  | Specific/X25519/C64/fesquare                       | 0m13.13s  || +0m01.64s
0m13.71s  | Specific/NISTP256/AMD64/fenz                       | 0m12.69s  || +0m01.02s
3m14.34s  | Specific/X25519/C64/ladderstep                     | 3m14.32s  || +0m00.02s
0m16.54s  | Specific/NISTP256/AMD64/feopp                      | 0m16.48s  || +0m00.05s
0m12.21s  | Specific/MontgomeryP256_128                        | 0m12.70s  || -0m00.48s
0m00.73s  | Specific/IntegrationTestTemporaryMiscCommon        | 0m00.72s  || +0m00.01s
0m00.64s  | Specific/IntegrationTestDisplayCommon              | 0m00.60s  || +0m00.04s

1 files changed, 155 insertions, 49 deletions

diff --git a/src/Specific/MontgomeryP256_128.v b/src/Specific/MontgomeryP256_128.v
index 9c0336503..b3df2a409 100644
--- a/src/Specific/MontgomeryP256_128.v
+++ b/src/Specific/MontgomeryP256_128.v
@@ -201,15 +201,16 @@ Proof.*)
 Definition montgomery_to_F (v : Z) : F m
   := (F.of_Z m v * F.of_Z m (r'^Z.of_nat sz)%Z)%F.
 
-Definition mulmod_256 : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz
-                        | let eval := MontgomeryAPI.eval (Z.pos r) in
-                          (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
-                                  (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
-                              montgomery_to_F (eval (f A B))
-                              = (montgomery_to_F (eval A) * montgomery_to_F (eval B))%F)
-                          /\ (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
-                                     (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
-                                 (eval B < eval p256 -> 0 <= eval (f A B) < eval p256)%Z) }.
+Definition mulmod_256_ext
+  : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz
+    | let eval := MontgomeryAPI.eval (Z.pos r) in
+      (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
+              (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
+          montgomery_to_F (eval (f A B))
+          = (montgomery_to_F (eval A) * montgomery_to_F (eval B))%F)
+      /\ (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
+                 (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
+             (eval B < eval p256 -> 0 <= eval (f A B) < eval p256)%Z) }.
 Proof.
   exists (proj1_sig mulmod_256'').
   abstract (
@@ -226,6 +227,26 @@ Proof.
     ).
 Defined.
 
+Definition mulmod_256
+  : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz
+    | let eval := MontgomeryAPI.eval (Z.pos r) in
+      forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
+             (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
+        montgomery_to_F (eval (f A B))
+        = (montgomery_to_F (eval A) * montgomery_to_F (eval B))%F }.
+Proof.
+  let v := (eval cbv [proj1_sig mulmod_256_ext mulmod_256'' mulmod_256' lift2_sig] in (proj1_sig mulmod_256_ext)) in
+  (exists v).
+  abstract apply (proj2_sig mulmod_256_ext).
+Defined.
+
+Lemma mulmod_256_bounded
+  : let eval := MontgomeryAPI.eval (Z.pos r) in
+    forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
+           (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
+      (eval B < eval p256 -> 0 <= eval (proj1_sig mulmod_256 A B) < eval p256)%Z.
+Proof. apply (proj2_sig mulmod_256_ext). Qed.
+
 Local Ltac t_fin :=
   [ > reflexivity
   | repeat match goal with
@@ -241,19 +262,20 @@ Local Ltac t_fin :=
            | [ |- (0 <= MontgomeryAPI.eval (Z.pos r) _)%Z ] => apply MontgomeryAPI.eval_small
            end.. ].
 
-Definition add : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz
-                 | let eval := MontgomeryAPI.eval (Z.pos r) in
-                   ((forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
-                            (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
-                        (eval A < eval p256
-                         -> eval B < eval p256
-                         -> montgomery_to_F (eval (f A B))
-                            = (montgomery_to_F (eval A) + montgomery_to_F (eval B))%F))
-                    /\ (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
-                               (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
-                           (eval A < eval p256
-                            -> eval B < eval p256
-                            -> 0 <= eval (f A B) < eval p256)))%Z }.
+Definition add_ext
+  : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz
+    | let eval := MontgomeryAPI.eval (Z.pos r) in
+      ((forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
+               (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
+           (eval A < eval p256
+            -> eval B < eval p256
+            -> montgomery_to_F (eval (f A B))
+               = (montgomery_to_F (eval A) + montgomery_to_F (eval B))%F))
+       /\ (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
+                  (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
+              (eval A < eval p256
+               -> eval B < eval p256
+               -> 0 <= eval (f A B) < eval p256)))%Z }.
 Proof.
   exists (proj1_sig add').
   abstract (
@@ -266,19 +288,20 @@ Proof.
     ).
 Defined.
 
-Definition sub : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz
-                 | let eval := MontgomeryAPI.eval (Z.pos r) in
-                   ((forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
-                            (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
-                        (eval A < eval p256
-                         -> eval B < eval p256
-                         -> montgomery_to_F (eval (f A B))
-                            = (montgomery_to_F (eval A) - montgomery_to_F (eval B))%F))
-                    /\ (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
-                            (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
-                        (eval A < eval p256
-                         -> eval B < eval p256
-                         -> 0 <= eval (f A B) < eval p256)))%Z }.
+Definition sub_ext
+  : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz
+    | let eval := MontgomeryAPI.eval (Z.pos r) in
+      ((forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
+               (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
+           (eval A < eval p256
+            -> eval B < eval p256
+            -> montgomery_to_F (eval (f A B))
+               = (montgomery_to_F (eval A) - montgomery_to_F (eval B))%F))
+       /\ (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
+                  (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
+              (eval A < eval p256
+               -> eval B < eval p256
+               -> 0 <= eval (f A B) < eval p256)))%Z }.
 Proof.
   exists (proj1_sig sub').
   abstract (
@@ -291,15 +314,16 @@ Proof.
     ).
 Defined.
 
-Definition opp : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz
-                 | let eval := MontgomeryAPI.eval (Z.pos r) in
-                   ((forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A),
-                        (eval A < eval p256
-                         -> montgomery_to_F (eval (f A))
-                            = (F.opp (montgomery_to_F (eval A)))%F))
-                    /\ (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A),
-                           (eval A < eval p256
-                            -> 0 <= eval (f A) < eval p256)))%Z }.
+Definition opp_ext
+  : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz
+    | let eval := MontgomeryAPI.eval (Z.pos r) in
+      ((forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A),
+           (eval A < eval p256
+            -> montgomery_to_F (eval (f A))
+               = (F.opp (montgomery_to_F (eval A)))%F))
+       /\ (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A),
+              (eval A < eval p256
+               -> 0 <= eval (f A) < eval p256)))%Z }.
 Proof.
   exists (proj1_sig opp').
   abstract (
@@ -312,11 +336,12 @@ Proof.
     ).
 Defined.
 
-Definition nonzero : { f:Tuple.tuple Z sz -> Z
-                     | let eval := MontgomeryAPI.eval (Z.pos r) in
-                       forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A),
-                         (eval A < eval p256
-                          -> f A = 0 <-> (montgomery_to_F (eval A) = F.of_Z m 0))%Z }.
+Definition nonzero_ext
+  : { f:Tuple.tuple Z sz -> Z
+    | let eval := MontgomeryAPI.eval (Z.pos r) in
+      forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A),
+        (eval A < eval p256
+         -> f A = 0 <-> (montgomery_to_F (eval A) = F.of_Z m 0))%Z }.
 Proof.
   exists (proj1_sig nonzero').
   abstract (
@@ -334,5 +359,86 @@ Proof.
     ).
 Defined.
 
+Definition add
+  : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz
+    | let eval := MontgomeryAPI.eval (Z.pos r) in
+      forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
+             (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
+        (eval A < eval p256
+         -> eval B < eval p256
+         -> montgomery_to_F (eval (f A B))
+            = (montgomery_to_F (eval A) + montgomery_to_F (eval B))%F)%Z }.
+Proof.
+  let v := (eval cbv [proj1_sig add_ext add' lift2_sig] in (proj1_sig add_ext)) in
+  (exists v).
+  abstract apply (proj2_sig add_ext).
+Defined.
+
+Lemma add_bounded
+  : let eval := MontgomeryAPI.eval (Z.pos r) in
+    (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
+            (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
+        (eval A < eval p256
+         -> eval B < eval p256
+         -> 0 <= eval (proj1_sig add A B) < eval p256))%Z.
+Proof. apply (proj2_sig add_ext). Qed.
+
+Definition sub
+  : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz
+    | let eval := MontgomeryAPI.eval (Z.pos r) in
+      forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
+             (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
+        (eval A < eval p256
+         -> eval B < eval p256
+         -> montgomery_to_F (eval (f A B))
+            = (montgomery_to_F (eval A) - montgomery_to_F (eval B))%F)%Z }.
+Proof.
+  let v := (eval cbv [proj1_sig sub_ext sub' lift2_sig] in (proj1_sig sub_ext)) in
+  (exists v).
+  abstract apply (proj2_sig sub_ext).
+Defined.
+
+Lemma sub_bounded
+  : let eval := MontgomeryAPI.eval (Z.pos r) in
+    (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A)
+            (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B),
+        (eval A < eval p256
+         -> eval B < eval p256
+         -> 0 <= eval (proj1_sig sub A B) < eval p256))%Z.
+Proof. apply (proj2_sig sub_ext). Qed.
+
+Definition opp
+  : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz
+    | let eval := MontgomeryAPI.eval (Z.pos r) in
+      forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A),
+        (eval A < eval p256
+         -> montgomery_to_F (eval (f A))
+            = (F.opp (montgomery_to_F (eval A)))%F)%Z }.
+Proof.
+  let v := (eval cbv [proj1_sig opp_ext opp' lift1_sig] in (proj1_sig opp_ext)) in
+  (exists v).
+  abstract apply (proj2_sig opp_ext).
+Defined.
+
+Lemma opp_bounded
+  : let eval := MontgomeryAPI.eval (Z.pos r) in
+    (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A),
+        (eval A < eval p256
+         -> 0 <= eval (proj1_sig opp A) < eval p256))%Z.
+Proof. apply (proj2_sig opp_ext). Qed.
+
+Definition nonzero
+  : { f:Tuple.tuple Z sz -> Z
+    | let eval := MontgomeryAPI.eval (Z.pos r) in
+      forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A),
+        (eval A < eval p256
+         -> f A = 0 <-> (montgomery_to_F (eval A) = F.of_Z m 0))%Z }.
+Proof.
+  let v := (eval cbv [proj1_sig nonzero_ext nonzero' lift1_sig] in (proj1_sig nonzero_ext)) in
+  (exists v).
+  abstract apply (proj2_sig nonzero_ext).
+Defined.
+
+
 Local Definition for_assumptions := (mulmod_256, add, sub, opp, nonzero).
 Print Assumptions for_assumptions.