Remove admits, fill templates, copy bounds

1 files changed, 50 insertions, 0 deletions

diff --git a/src/SpecificGen/GF25519_32BoundedCommon.v b/src/SpecificGen/GF25519_32BoundedCommon.v
index 1695681c4..6751390ee 100644
--- a/src/SpecificGen/GF25519_32BoundedCommon.v
+++ b/src/SpecificGen/GF25519_32BoundedCommon.v
@@ -186,6 +186,25 @@ Section generic_destructuring.
     intros. cbv [appify2].
     etransitivity; apply app_fe25519_32W_correct.
   Qed.
+
+  Definition appify9 {T} (op : fe25519_32W -> fe25519_32W -> fe25519_32W -> fe25519_32W -> fe25519_32W -> fe25519_32W -> fe25519_32W -> fe25519_32W -> fe25519_32W -> T) (x0 x1 x2 x3 x4 x5 x6 x7 x8 : fe25519_32W) :=
+    app_fe25519_32W x0 (fun x0' =>
+    app_fe25519_32W x1 (fun x1' =>
+    app_fe25519_32W x2 (fun x2' =>
+    app_fe25519_32W x3 (fun x3' =>
+    app_fe25519_32W x4 (fun x4' =>
+    app_fe25519_32W x5 (fun x5' =>
+    app_fe25519_32W x6 (fun x6' =>
+    app_fe25519_32W x7 (fun x7' =>
+    app_fe25519_32W x8 (fun x8' =>
+                       op x0' x1' x2' x3' x4' x5' x6' x7' x8'))))))))).
+
+  Lemma appify9_correct : forall {T} op x0 x1 x2 x3 x4 x5 x6 x7 x8,
+      @appify9 T op x0 x1 x2 x3 x4 x5 x6 x7 x8 = op x0 x1 x2 x3 x4 x5 x6 x7 x8.
+  Proof.
+    intros. cbv [appify9].
+    repeat (etransitivity; [ apply app_fe25519_32W_correct | ]); reflexivity.
+  Qed.
 End generic_destructuring.
 
 Definition eta_fe25519_32W_sig (x : fe25519_32W) : { v : fe25519_32W | v = x }.
@@ -369,6 +388,22 @@ Definition uncurry_unop_wire_digitsW {T} (op : wire_digitsW -> T)
 Definition curry_unop_wire_digitsW {T} op : wire_digitsW -> T
   := Eval cbv (*-[word64]*) in fun f => app_wire_digitsW f (Tuple.curry (n:=length wire_widths) op).
 
+Definition uncurry_9op_fe25519_32W {T} (op : fe25519_32W -> fe25519_32W -> fe25519_32W -> fe25519_32W -> fe25519_32W -> fe25519_32W -> fe25519_32W -> fe25519_32W -> fe25519_32W -> T)
+  := Eval cbv (*-[word64]*) in
+      uncurry_unop_fe25519_32W (fun x0 =>
+      uncurry_unop_fe25519_32W (fun x1 =>
+      uncurry_unop_fe25519_32W (fun x2 =>
+      uncurry_unop_fe25519_32W (fun x3 =>
+      uncurry_unop_fe25519_32W (fun x4 =>
+      uncurry_unop_fe25519_32W (fun x5 =>
+      uncurry_unop_fe25519_32W (fun x6 =>
+      uncurry_unop_fe25519_32W (fun x7 =>
+      uncurry_unop_fe25519_32W (fun x8 =>
+                               op x0 x1 x2 x3 x4 x5 x6 x7 x8))))))))).
+Definition curry_9op_fe25519_32W {T} op : fe25519_32W -> fe25519_32W -> fe25519_32W -> fe25519_32W -> fe25519_32W -> fe25519_32W -> fe25519_32W -> fe25519_32W -> fe25519_32W -> T
+  := Eval cbv (*-[word64]*) in
+      appify9 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8
+               => curry_unop_fe25519_32W (curry_unop_fe25519_32W (curry_unop_fe25519_32W (curry_unop_fe25519_32W (curry_unop_fe25519_32W (curry_unop_fe25519_32W (curry_unop_fe25519_32W (curry_unop_fe25519_32W (curry_unop_fe25519_32W op x0) x1) x2) x3) x4) x5) x6) x7) x8).
 
 Definition proj1_fe25519_32W (x : fe25519_32) : fe25519_32W
   := Eval app_tuple_map in
@@ -708,5 +743,20 @@ Notation iunop_WireToFE_correct_and_bounded irop op
          wire_digits_is_bounded (wire_digitsWToZ x) = true
          -> fe25519_32WToZ (irop x) = op (wire_digitsWToZ x)
             /\ is_bounded (fe25519_32WToZ (irop x)) = true) (only parsing).
+Notation i9top_correct_and_bounded k irop op
+  := ((forall x0 x1 x2 x3 x4 x5 x6 x7 x8,
+          is_bounded (fe25519_32WToZ x0) = true
+          -> is_bounded (fe25519_32WToZ x1) = true
+          -> is_bounded (fe25519_32WToZ x2) = true
+          -> is_bounded (fe25519_32WToZ x3) = true
+          -> is_bounded (fe25519_32WToZ x4) = true
+          -> is_bounded (fe25519_32WToZ x5) = true
+          -> is_bounded (fe25519_32WToZ x6) = true
+          -> is_bounded (fe25519_32WToZ x7) = true
+          -> is_bounded (fe25519_32WToZ x8) = true
+          -> (Tuple.map (n:=k) fe25519_32WToZ (irop x0 x1 x2 x3 x4 x5 x6 x7 x8)
+              = op (fe25519_32WToZ x0) (fe25519_32WToZ x1) (fe25519_32WToZ x2) (fe25519_32WToZ x3) (fe25519_32WToZ x4) (fe25519_32WToZ x5) (fe25519_32WToZ x6) (fe25519_32WToZ x7) (fe25519_32WToZ x8))
+             * HList.hlist (fun v => is_bounded v = true) (Tuple.map (n:=k) fe25519_32WToZ (irop x0 x1 x2 x3 x4 x5 x6 x7 x8)))%type)
+       (only parsing).
 
 Definition prefreeze := GF25519_32.prefreeze.