From 13c218f6a5e43d307958f95adfbea3e5fb45eaac Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 25 Nov 2016 13:12:01 -0500 Subject: Add inm_op_correct_and_bounded --- src/SpecificGen/GF2213_32BoundedCommon.v | 29 +++++++++++++++++++++++++++++ src/SpecificGen/GF2519_32BoundedCommon.v | 29 +++++++++++++++++++++++++++++ src/SpecificGen/GF25519_32BoundedCommon.v | 29 +++++++++++++++++++++++++++++ src/SpecificGen/GF25519_64BoundedCommon.v | 29 +++++++++++++++++++++++++++++ src/SpecificGen/GF41417_32BoundedCommon.v | 29 +++++++++++++++++++++++++++++ src/SpecificGen/GF5211_32BoundedCommon.v | 29 +++++++++++++++++++++++++++++ 6 files changed, 174 insertions(+) (limited to 'src/SpecificGen') 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 -- cgit v1.2.3