Add inm_op_correct_and_bounded

6 files changed, 174 insertions, 0 deletions

diff --git a/src/SpecificGen/GF2213_32BoundedCommon.v b/src/SpecificGen/GF2213_32BoundedCommon.v
index 268b0be56..02216323a 100644
--- a/src/SpecificGen/GF2213_32BoundedCommon.v
+++ b/src/SpecificGen/GF2213_32BoundedCommon.v
@@ -718,6 +718,35 @@ Definition div (f g : fe2213_32) : fe2213_32
 Definition eq (f g : fe2213_32) : Prop := eq (proj1_fe2213_32 f) (proj1_fe2213_32 g).
 
 
+Notation in_op_correct_and_bounded k irop op
+  := (((Tuple.map (n:=k) fe2213_32WToZ irop = op)
+       /\ HList.hlistP (fun v => is_bounded v = true) (Tuple.map (n:=k) fe2213_32WToZ irop))%type)
+       (only parsing).
+
+Fixpoint inm_op_correct_and_bounded' (count_in count_out : nat)
+  : forall (irop : Tower.tower_nd fe2213_32W (Tuple.tuple fe2213_32W count_out) count_in)
+           (op : Tower.tower_nd GF2213_32.fe2213_32 (Tuple.tuple GF2213_32.fe2213_32 count_out) count_in)
+           (cont : Prop -> Prop),
+    Prop
+  := match count_in return
+           forall (irop : Tower.tower_nd fe2213_32W (Tuple.tuple fe2213_32W count_out) count_in)
+                  (op : Tower.tower_nd GF2213_32.fe2213_32 (Tuple.tuple GF2213_32.fe2213_32 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 : fe2213_32W,
+                  @inm_op_correct_and_bounded'
+                    n count_out (irop x) (op (fe2213_32WToZ x))
+                    (fun P => cont (is_bounded (fe2213_32WToZ 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 (fe2213_32WToZ x) = true
diff --git a/src/SpecificGen/GF2519_32BoundedCommon.v b/src/SpecificGen/GF2519_32BoundedCommon.v
index 330f738cd..a9f1a75c8 100644
--- a/src/SpecificGen/GF2519_32BoundedCommon.v
+++ b/src/SpecificGen/GF2519_32BoundedCommon.v
@@ -718,6 +718,35 @@ Definition div (f g : fe2519_32) : fe2519_32
 Definition eq (f g : fe2519_32) : Prop := eq (proj1_fe2519_32 f) (proj1_fe2519_32 g).
 
 
+Notation in_op_correct_and_bounded k irop op
+  := (((Tuple.map (n:=k) fe2519_32WToZ irop = op)
+       /\ HList.hlistP (fun v => is_bounded v = true) (Tuple.map (n:=k) fe2519_32WToZ irop))%type)
+       (only parsing).
+
+Fixpoint inm_op_correct_and_bounded' (count_in count_out : nat)
+  : forall (irop : Tower.tower_nd fe2519_32W (Tuple.tuple fe2519_32W count_out) count_in)
+           (op : Tower.tower_nd GF2519_32.fe2519_32 (Tuple.tuple GF2519_32.fe2519_32 count_out) count_in)
+           (cont : Prop -> Prop),
+    Prop
+  := match count_in return
+           forall (irop : Tower.tower_nd fe2519_32W (Tuple.tuple fe2519_32W count_out) count_in)
+                  (op : Tower.tower_nd GF2519_32.fe2519_32 (Tuple.tuple GF2519_32.fe2519_32 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 : fe2519_32W,
+                  @inm_op_correct_and_bounded'
+                    n count_out (irop x) (op (fe2519_32WToZ x))
+                    (fun P => cont (is_bounded (fe2519_32WToZ 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 (fe2519_32WToZ x) = true
diff --git a/src/SpecificGen/GF25519_32BoundedCommon.v b/src/SpecificGen/GF25519_32BoundedCommon.v
index 6751390ee..ec4b042c9 100644
--- a/src/SpecificGen/GF25519_32BoundedCommon.v
+++ b/src/SpecificGen/GF25519_32BoundedCommon.v
@@ -718,6 +718,35 @@ Definition div (f g : fe25519_32) : fe25519_32
 Definition eq (f g : fe25519_32) : Prop := eq (proj1_fe25519_32 f) (proj1_fe25519_32 g).
 
 
+Notation in_op_correct_and_bounded k irop op
+  := (((Tuple.map (n:=k) fe25519_32WToZ irop = op)
+       /\ HList.hlistP (fun v => is_bounded v = true) (Tuple.map (n:=k) fe25519_32WToZ irop))%type)
+       (only parsing).
+
+Fixpoint inm_op_correct_and_bounded' (count_in count_out : nat)
+  : forall (irop : Tower.tower_nd fe25519_32W (Tuple.tuple fe25519_32W count_out) count_in)
+           (op : Tower.tower_nd GF25519_32.fe25519_32 (Tuple.tuple GF25519_32.fe25519_32 count_out) count_in)
+           (cont : Prop -> Prop),
+    Prop
+  := match count_in return
+           forall (irop : Tower.tower_nd fe25519_32W (Tuple.tuple fe25519_32W count_out) count_in)
+                  (op : Tower.tower_nd GF25519_32.fe25519_32 (Tuple.tuple GF25519_32.fe25519_32 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 : fe25519_32W,
+                  @inm_op_correct_and_bounded'
+                    n count_out (irop x) (op (fe25519_32WToZ x))
+                    (fun P => cont (is_bounded (fe25519_32WToZ 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 (fe25519_32WToZ x) = true
diff --git a/src/SpecificGen/GF25519_64BoundedCommon.v b/src/SpecificGen/GF25519_64BoundedCommon.v
index b9608811d..99a023a48 100644
--- a/src/SpecificGen/GF25519_64BoundedCommon.v
+++ b/src/SpecificGen/GF25519_64BoundedCommon.v
@@ -718,6 +718,35 @@ Definition div (f g : fe25519_64) : fe25519_64
 Definition eq (f g : fe25519_64) : Prop := eq (proj1_fe25519_64 f) (proj1_fe25519_64 g).
 
 
+Notation in_op_correct_and_bounded k irop op
+  := (((Tuple.map (n:=k) fe25519_64WToZ irop = op)
+       /\ HList.hlistP (fun v => is_bounded v = true) (Tuple.map (n:=k) fe25519_64WToZ irop))%type)
+       (only parsing).
+
+Fixpoint inm_op_correct_and_bounded' (count_in count_out : nat)
+  : forall (irop : Tower.tower_nd fe25519_64W (Tuple.tuple fe25519_64W count_out) count_in)
+           (op : Tower.tower_nd GF25519_64.fe25519_64 (Tuple.tuple GF25519_64.fe25519_64 count_out) count_in)
+           (cont : Prop -> Prop),
+    Prop
+  := match count_in return
+           forall (irop : Tower.tower_nd fe25519_64W (Tuple.tuple fe25519_64W count_out) count_in)
+                  (op : Tower.tower_nd GF25519_64.fe25519_64 (Tuple.tuple GF25519_64.fe25519_64 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 : fe25519_64W,
+                  @inm_op_correct_and_bounded'
+                    n count_out (irop x) (op (fe25519_64WToZ x))
+                    (fun P => cont (is_bounded (fe25519_64WToZ 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 (fe25519_64WToZ x) = true
diff --git a/src/SpecificGen/GF41417_32BoundedCommon.v b/src/SpecificGen/GF41417_32BoundedCommon.v
index 1ec733cc6..02873665f 100644
--- a/src/SpecificGen/GF41417_32BoundedCommon.v
+++ b/src/SpecificGen/GF41417_32BoundedCommon.v
@@ -718,6 +718,35 @@ Definition div (f g : fe41417_32) : fe41417_32
 Definition eq (f g : fe41417_32) : Prop := eq (proj1_fe41417_32 f) (proj1_fe41417_32 g).
 
 
+Notation in_op_correct_and_bounded k irop op
+  := (((Tuple.map (n:=k) fe41417_32WToZ irop = op)
+       /\ HList.hlistP (fun v => is_bounded v = true) (Tuple.map (n:=k) fe41417_32WToZ irop))%type)
+       (only parsing).
+
+Fixpoint inm_op_correct_and_bounded' (count_in count_out : nat)
+  : forall (irop : Tower.tower_nd fe41417_32W (Tuple.tuple fe41417_32W count_out) count_in)
+           (op : Tower.tower_nd GF41417_32.fe41417_32 (Tuple.tuple GF41417_32.fe41417_32 count_out) count_in)
+           (cont : Prop -> Prop),
+    Prop
+  := match count_in return
+           forall (irop : Tower.tower_nd fe41417_32W (Tuple.tuple fe41417_32W count_out) count_in)
+                  (op : Tower.tower_nd GF41417_32.fe41417_32 (Tuple.tuple GF41417_32.fe41417_32 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 : fe41417_32W,
+                  @inm_op_correct_and_bounded'
+                    n count_out (irop x) (op (fe41417_32WToZ x))
+                    (fun P => cont (is_bounded (fe41417_32WToZ 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 (fe41417_32WToZ x) = true
diff --git a/src/SpecificGen/GF5211_32BoundedCommon.v b/src/SpecificGen/GF5211_32BoundedCommon.v
index 395e6c6f2..7dd04370e 100644
--- a/src/SpecificGen/GF5211_32BoundedCommon.v
+++ b/src/SpecificGen/GF5211_32BoundedCommon.v
@@ -718,6 +718,35 @@ Definition div (f g : fe5211_32) : fe5211_32
 Definition eq (f g : fe5211_32) : Prop := eq (proj1_fe5211_32 f) (proj1_fe5211_32 g).
 
 
+Notation in_op_correct_and_bounded k irop op
+  := (((Tuple.map (n:=k) fe5211_32WToZ irop = op)
+       /\ HList.hlistP (fun v => is_bounded v = true) (Tuple.map (n:=k) fe5211_32WToZ irop))%type)
+       (only parsing).
+
+Fixpoint inm_op_correct_and_bounded' (count_in count_out : nat)
+  : forall (irop : Tower.tower_nd fe5211_32W (Tuple.tuple fe5211_32W count_out) count_in)
+           (op : Tower.tower_nd GF5211_32.fe5211_32 (Tuple.tuple GF5211_32.fe5211_32 count_out) count_in)
+           (cont : Prop -> Prop),
+    Prop
+  := match count_in return
+           forall (irop : Tower.tower_nd fe5211_32W (Tuple.tuple fe5211_32W count_out) count_in)
+                  (op : Tower.tower_nd GF5211_32.fe5211_32 (Tuple.tuple GF5211_32.fe5211_32 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 : fe5211_32W,
+                  @inm_op_correct_and_bounded'
+                    n count_out (irop x) (op (fe5211_32WToZ x))
+                    (fun P => cont (is_bounded (fe5211_32WToZ 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 (fe5211_32WToZ x) = true