ABCDEF.v 2.44 KB
Newer Older
Benoit Viguier's avatar
Benoit Viguier committed
1
From Tweetnacl.Gen Require Import AMZubSqSel.
Benoit Viguier's avatar
Benoit Viguier committed
2

Benoit Viguier's avatar
Benoit Viguier committed
3
4
Module Gen.

Benoit Viguier's avatar
Benoit Viguier committed
5
Section ABCDEF.
Benoit Viguier's avatar
Benoit Viguier committed
6

Benoit Viguier's avatar
Benoit Viguier committed
7
Context {T : Type}.
Benoit Viguier's avatar
Benoit Viguier committed
8
Context {T' : Type}.
Benoit Viguier's avatar
Benoit Viguier committed
9
10
Context {Mod : T -> T}.
Context {O : @Ops T T' Mod}.
Benoit Viguier's avatar
Benoit Viguier committed
11

Benoit Viguier's avatar
Benoit Viguier committed
12
Definition fa r (a b c d e f x:T) :=
Benoit Viguier's avatar
Benoit Viguier committed
13
14
15
16
17
18
19
20
21
  Sel25519 r
     (M (Sq (A (Sel25519 r a b) (Sel25519 r c d)))
        (Sq (Zub (Sel25519 r a b) (Sel25519 r c d))))
     (Sq
        (A
           (M (A (Sel25519 r b a) (Sel25519 r d c))
              (Zub (Sel25519 r a b) (Sel25519 r c d)))
           (M (Zub (Sel25519 r b a) (Sel25519 r d c))
              (A (Sel25519 r a b) (Sel25519 r c d))))).
Benoit Viguier's avatar
Benoit Viguier committed
22
Definition fb r (a b c d e f x:T) :=
Benoit Viguier's avatar
Benoit Viguier committed
23
24
25
26
27
28
29
30
31
  Sel25519 r
     (Sq
        (A
           (M (A (Sel25519 r b a) (Sel25519 r d c))
              (Zub (Sel25519 r a b) (Sel25519 r c d)))
           (M (Zub (Sel25519 r b a) (Sel25519 r d c))
              (A (Sel25519 r a b) (Sel25519 r c d)))))
     (M (Sq (A (Sel25519 r a b) (Sel25519 r c d)))
        (Sq (Zub (Sel25519 r a b) (Sel25519 r c d)))).
Benoit Viguier's avatar
Benoit Viguier committed
32
Definition fc r (a b c d e f x:T) :=
Benoit Viguier's avatar
Benoit Viguier committed
33
34
35
36
37
38
39
Sel25519 r
  (M
     (Zub (Sq (A (Sel25519 r a b) (Sel25519 r c d)))
        (Sq (Zub (Sel25519 r a b) (Sel25519 r c d))))
     (A
        (M
           (Zub (Sq (A (Sel25519 r a b) (Sel25519 r c d)))
Benoit Viguier's avatar
Benoit Viguier committed
40
              (Sq (Zub (Sel25519 r a b) (Sel25519 r c d)))) C_121665)
Benoit Viguier's avatar
Benoit Viguier committed
41
42
43
44
45
46
47
48
        (Sq (A (Sel25519 r a b) (Sel25519 r c d)))))
  (M
     (Sq
        (Zub
           (M (A (Sel25519 r b a) (Sel25519 r d c))
              (Zub (Sel25519 r a b) (Sel25519 r c d)))
           (M (Zub (Sel25519 r b a) (Sel25519 r d c))
              (A (Sel25519 r a b) (Sel25519 r c d))))) x).
Benoit Viguier's avatar
Benoit Viguier committed
49
Definition fd r (a b c d e f x:T) :=
Benoit Viguier's avatar
Benoit Viguier committed
50
51
52
53
54
55
56
57
58
59
60
61
62
63
Sel25519 r
  (M
     (Sq
        (Zub
           (M (A (Sel25519 r b a) (Sel25519 r d c))
              (Zub (Sel25519 r a b) (Sel25519 r c d)))
           (M (Zub (Sel25519 r b a) (Sel25519 r d c))
              (A (Sel25519 r a b) (Sel25519 r c d))))) x)
  (M
     (Zub (Sq (A (Sel25519 r a b) (Sel25519 r c d)))
        (Sq (Zub (Sel25519 r a b) (Sel25519 r c d))))
     (A
        (M
           (Zub (Sq (A (Sel25519 r a b) (Sel25519 r c d)))
Benoit Viguier's avatar
Benoit Viguier committed
64
              (Sq (Zub (Sel25519 r a b) (Sel25519 r c d)))) C_121665)
Benoit Viguier's avatar
Benoit Viguier committed
65
        (Sq (A (Sel25519 r a b) (Sel25519 r c d))))).
Benoit Viguier's avatar
Benoit Viguier committed
66
Definition fe r (a b c d e f x:T) :=
Benoit Viguier's avatar
Benoit Viguier committed
67
68
69
70
71
A
  (M (A (Sel25519 r b a) (Sel25519 r d c))
     (Zub (Sel25519 r a b) (Sel25519 r c d)))
  (M (Zub (Sel25519 r b a) (Sel25519 r d c))
     (A (Sel25519 r a b) (Sel25519 r c d))).
Benoit Viguier's avatar
Benoit Viguier committed
72
Definition ff r (a b c d e f x:T) :=
Benoit Viguier's avatar
Benoit Viguier committed
73
74
  Sq (Zub (Sel25519 r a b) (Sel25519 r c d)).

Benoit Viguier's avatar
Benoit Viguier committed
75
76
77
End ABCDEF.

End Gen.