diff options
Diffstat (limited to 'src/SpecificGen/GF25519_32BoundedCommon.v')
| -rw-r--r-- | src/SpecificGen/GF25519_32BoundedCommon.v | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/src/SpecificGen/GF25519_32BoundedCommon.v b/src/SpecificGen/GF25519_32BoundedCommon.v index f28608623..43fc1be36 100644 --- a/src/SpecificGen/GF25519_32BoundedCommon.v +++ b/src/SpecificGen/GF25519_32BoundedCommon.v @@ -871,5 +871,21 @@ Notation i9top_correct_and_bounded k irop op = op (fe25519_32WToZ x0) (fe25519_32WToZ x1) (fe25519_32WToZ x2) (fe25519_32WToZ x3) (fe25519_32WToZ x4) (fe25519_32WToZ x5) (fe25519_32WToZ x6) (fe25519_32WToZ x7) (fe25519_32WToZ x8)) * HList.hlist (fun v => is_bounded v = true) (Tuple.map (n:=k) fe25519_32WToZ (irop x0 x1 x2 x3 x4 x5 x6 x7 x8)))%type) (only parsing). +Notation i10top_correct_and_bounded k irop op + := ((forall x0 x1 x2 x3 x4 x5 x6 x7 x8 x9, + is_bounded (fe25519_32WToZ x0) = true + -> is_bounded (fe25519_32WToZ x1) = true + -> is_bounded (fe25519_32WToZ x2) = true + -> is_bounded (fe25519_32WToZ x3) = true + -> is_bounded (fe25519_32WToZ x4) = true + -> is_bounded (fe25519_32WToZ x5) = true + -> is_bounded (fe25519_32WToZ x6) = true + -> is_bounded (fe25519_32WToZ x7) = true + -> is_bounded (fe25519_32WToZ x8) = true + -> is_bounded (fe25519_32WToZ x9) = true + -> (Tuple.map (n:=k) fe25519_32WToZ (irop x0 x1 x2 x3 x4 x5 x6 x7 x8 x9) + = op (fe25519_32WToZ x0) (fe25519_32WToZ x1) (fe25519_32WToZ x2) (fe25519_32WToZ x3) (fe25519_32WToZ x4) (fe25519_32WToZ x5) (fe25519_32WToZ x6) (fe25519_32WToZ x7) (fe25519_32WToZ x8) (fe25519_32WToZ x9)) + * HList.hlist (fun v => is_bounded v = true) (Tuple.map (n:=k) fe25519_32WToZ (irop x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)))%type) + (only parsing). Definition prefreeze := GF25519_32.prefreeze. |