aboutsummaryrefslogtreecommitdiff
path: root/src/SpecificGen/GF2213_32BoundedCommon.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/SpecificGen/GF2213_32BoundedCommon.v')
-rw-r--r--src/SpecificGen/GF2213_32BoundedCommon.v29
1 files changed, 29 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