Add inm_op_correct_and_bounded

1 files changed, 29 insertions, 0 deletions

diff --git a/src/Specific/GF25519BoundedCommon.v b/src/Specific/GF25519BoundedCommon.v
index 22c2edc4b..6167fec18 100644
--- a/src/Specific/GF25519BoundedCommon.v
+++ b/src/Specific/GF25519BoundedCommon.v
@@ -718,6 +718,35 @@ Definition div (f g : fe25519) : fe25519
 Definition eq (f g : fe25519) : Prop := eq (proj1_fe25519 f) (proj1_fe25519 g).
 
 
+Notation in_op_correct_and_bounded k irop op
+  := (((Tuple.map (n:=k) fe25519WToZ irop = op)
+       /\ HList.hlistP (fun v => is_bounded v = true) (Tuple.map (n:=k) fe25519WToZ irop))%type)
+       (only parsing).
+
+Fixpoint inm_op_correct_and_bounded' (count_in count_out : nat)
+  : forall (irop : Tower.tower_nd fe25519W (Tuple.tuple fe25519W count_out) count_in)
+           (op : Tower.tower_nd GF25519.fe25519 (Tuple.tuple GF25519.fe25519 count_out) count_in)
+           (cont : Prop -> Prop),
+    Prop
+  := match count_in return
+           forall (irop : Tower.tower_nd fe25519W (Tuple.tuple fe25519W count_out) count_in)
+                  (op : Tower.tower_nd GF25519.fe25519 (Tuple.tuple GF25519.fe25519 count_out) count_in)
+                  (cont : Prop -> Prop),
+             Prop
+     with
+     | O => fun irop op cont => cont (in_op_correct_and_bounded count_out irop op)
+     | S n => fun irop op cont
+              => forall x : fe25519W,
+                  @inm_op_correct_and_bounded'
+                    n count_out (irop x) (op (fe25519WToZ x))
+                    (fun P => cont (is_bounded (fe25519WToZ x) = true -> P))
+     end.
+Definition inm_op_correct_and_bounded count_in count_out irop op
+  := Eval cbv [inm_op_correct_and_bounded' Tower.tower_nd Tuple.tuple Tuple.tuple' HList.hlistP HList.hlistP'] in
+      inm_op_correct_and_bounded' count_in count_out irop op (fun P => P).
+Definition inm_op_correct_and_bounded1 count_in  irop op
+  := Eval cbv [inm_op_correct_and_bounded Tuple.map Tuple.to_list Tuple.to_list' Tuple.from_list Tuple.from_list' Tuple.on_tuple List.map] in
+      inm_op_correct_and_bounded count_in 1 irop op.
 Notation ibinop_correct_and_bounded irop op
   := (forall x y,
          is_bounded (fe25519WToZ x) = true