Add more things to Reflective/Common

Preparation for reflective add_coordinates

1 files changed, 77 insertions, 11 deletions

diff --git a/src/Specific/GF25519Reflective/Common.v b/src/Specific/GF25519Reflective/Common.v
index 5ee903658..17fabd570 100644
--- a/src/Specific/GF25519Reflective/Common.v
+++ b/src/Specific/GF25519Reflective/Common.v
@@ -37,11 +37,34 @@ Definition ExprUnOpWireToFET : type base_type.
 Proof. make_type_from (uncurry_unop_wire_digits unpack). Defined.
 Definition ExprUnOpFEToWireT : type base_type.
 Proof. make_type_from (uncurry_unop_fe25519 pack). Defined.
+Definition ExprArgT : flat_type base_type
+  := Eval compute in remove_all_binders ExprUnOpT.
+Definition ExprArgWireT : flat_type base_type
+  := Eval compute in remove_all_binders ExprUnOpFEToWireT.
+Definition ExprArgRevT : flat_type base_type
+  := Eval compute in all_binders_for ExprUnOpT.
+Definition ExprArgWireRevT : flat_type base_type
+  := Eval compute in all_binders_for ExprUnOpWireToFET.
+Definition ExprZ : Type := Expr (Tbase TZ).
 Definition ExprBinOp : Type := Expr ExprBinOpT.
 Definition ExprUnOp : Type := Expr ExprUnOpT.
 Definition ExprUnOpFEToZ : Type := Expr ExprUnOpFEToZT.
 Definition ExprUnOpWireToFE : Type := Expr ExprUnOpWireToFET.
 Definition ExprUnOpFEToWire : Type := Expr ExprUnOpFEToWireT.
+Definition ExprArg : Type := Expr ExprArgT.
+Definition ExprArgWire : Type := Expr ExprArgWireT.
+Definition ExprArgRev : Type := Expr ExprArgRevT.
+Definition ExprArgWireRev : Type := Expr ExprArgWireRevT.
+Definition exprZ var : Type := expr base_type WordW.interp_base_type op (var:=var) (Tbase TZ).
+Definition exprBinOp var : Type := expr base_type WordW.interp_base_type op (var:=var) ExprBinOpT.
+Definition exprUnOp var : Type := expr base_type WordW.interp_base_type op (var:=var) ExprUnOpT.
+Definition exprUnOpFEToZ var : Type := expr base_type WordW.interp_base_type op (var:=var) ExprUnOpFEToZT.
+Definition exprUnOpWireToFE var : Type := expr base_type WordW.interp_base_type op (var:=var) ExprUnOpWireToFET.
+Definition exprUnOpFEToWire var : Type := expr base_type WordW.interp_base_type op (var:=var) ExprUnOpFEToWireT.
+Definition exprArg var : Type := expr base_type WordW.interp_base_type op (var:=var) ExprArgT.
+Definition exprArgWire var : Type := expr base_type WordW.interp_base_type op (var:=var) ExprArgWireT.
+Definition exprArgRev var : Type := expr base_type WordW.interp_base_type op (var:=var) ExprArgRevT.
+Definition exprArgWireRev var : Type := expr base_type WordW.interp_base_type op (var:=var) ExprArgWireRevT.
 
 Local Ltac bounds_from_list ls :=
   lazymatch (eval hnf in ls) with
@@ -224,6 +247,33 @@ Local Ltac get_len T :=
   | _ => constr:(1%nat)
   end.
 
+Ltac assoc_right_tuple x so_far :=
+  let t := type of x in
+  lazymatch (eval hnf in t) with
+  | prod _ _ => let so_far := assoc_right_tuple (snd x) so_far in
+                assoc_right_tuple (fst x) so_far
+  | _ => lazymatch so_far with
+         | @None => x
+         | _ => constr:((x, so_far))
+         end
+  end.
+
+Local Ltac make_args x :=
+  let x' := fresh "x'" in
+  compute in x |- *;
+  let t := match type of x with @expr _ _ _ _ (Tflat _ ?t) => t end in
+  let t' := match goal with |- @expr _ _ _ _ (Tflat _ ?t) => t end in
+  refine (LetIn (UnReturn x) _);
+  let x'' := fresh "x''" in
+  intro x'';
+  let xv := assoc_right_tuple x'' (@None) in
+  refine (SmartVarf (xv : interp_flat_type _ t')).
+
+Definition unop_make_args {var} (x : exprArg var) : exprArgRev var.
+Proof. make_args x. Defined.
+Definition unop_wire_make_args {var} (x : exprArgWire var) : exprArgWireRev var.
+Proof. make_args x. Defined.
+
 Local Ltac args_to_bounded x H :=
   let x' := fresh in
   set (x' := x);
@@ -256,17 +306,6 @@ Proof.
   exact v.
 Defined.
 
-Ltac assoc_right_tuple x so_far :=
-  let t := type of x in
-  lazymatch (eval hnf in t) with
-  | prod _ _ => let so_far := assoc_right_tuple (snd x) so_far in
-                assoc_right_tuple (fst x) so_far
-  | _ => lazymatch so_far with
-         | @None => x
-         | _ => constr:((x, so_far))
-         end
-  end.
-
 Local Ltac make_bounds_prop bounds orig_bounds :=
   let bounds' := fresh "bounds'" in
   let bounds_bad := fresh "bounds_bad" in
@@ -302,6 +341,33 @@ Proof.
   refine (let (l, u) := bounds in ((0 <=? l) && (u <=? 1))%Z%bool).
 Defined.
 
+Definition ApplyUnOp {var} (f : exprUnOp var) : exprArg var -> exprArg var
+  := fun x
+     => LetIn (UnReturn (unop_make_args x))
+              (fun k => UnReturn (Apply (n:=length_fe25519) f k)).
+Definition ApplyBinOp {var} (f : exprBinOp var) : exprArg var -> exprArg var -> exprArg var
+  := fun x y
+     => LetIn (UnReturn (unop_make_args x))
+              (fun x'
+               => LetIn (UnReturn (unop_make_args y))
+                        (fun y'
+                         => UnReturn (Apply (n:=length_fe25519)
+                                            (Apply (n:=length_fe25519)
+                                                   f x') y'))).
+Definition ApplyUnOpFEToWire {var} (f : exprUnOpFEToWire var) : exprArg var -> exprArgWire var
+  := fun x
+     => LetIn (UnReturn (unop_make_args x))
+              (fun k => UnReturn (Apply (n:=length_fe25519) f k)).
+Definition ApplyUnOpWireToFE {var} (f : exprUnOpWireToFE var) : exprArgWire var -> exprArg var
+  := fun x
+     => LetIn (UnReturn (unop_wire_make_args x))
+              (fun k => UnReturn (Apply (n:=List.length wire_widths) f k)).
+Definition ApplyUnOpFEToZ {var} (f : exprUnOpFEToZ var) : exprArg var -> exprZ var
+  := fun x
+     => LetIn (UnReturn (unop_make_args x))
+              (fun k => UnReturn (Apply (n:=length_fe25519) f k)).
+
+
 (* FIXME TODO(jgross): This is a horrible tactic.  We should unify the
     various kinds of correct and boundedness, and abstract in Gallina
     rather than Ltac *)