README.md 7.01 KB
Newer Older
Benoit Viguier's avatar
Benoit Viguier committed
1
2
3
# TweetNaCl verification
-------------------------------

benoit's avatar
benoit committed
4
## dependencies: GCC and OPAM.
Benoit Viguier's avatar
Benoit Viguier committed
5
6

[Install OPAM][1], e.g. for Debian:
Benoit Viguier's avatar
Benoit Viguier committed
7

Benoit Viguier's avatar
Benoit Viguier committed
8
```bash
Benoit Viguier's avatar
Benoit Viguier committed
9
sudo apt-get install gcc opam
Benoit Viguier's avatar
Benoit Viguier committed
10
```
Benoit Viguier's avatar
Benoit Viguier committed
11

Benoit Viguier's avatar
Benoit Viguier committed
12
13
**Verify that you are using OPAM 2.x.**

Benoit Viguier's avatar
Benoit Viguier committed
14
15
```bash
opam --version
benoit's avatar
benoit committed
16
# 2.0.5
Benoit Viguier's avatar
Benoit Viguier committed
17
18
```

benoit's avatar
benoit committed
19
20
21
## Setting up your environment

### 1. Set OPAM for Tweetnacl so it does not pollute other projects.
Benoit Viguier's avatar
Benoit Viguier committed
22

Benoit Viguier's avatar
Benoit Viguier committed
23
Because we use Coq 8.8.2, we are forced to use Ocaml 4.06.1.
Benoit Viguier's avatar
Benoit Viguier committed
24

Benoit Viguier's avatar
Benoit Viguier committed
25
```bash
benoit's avatar
benoit committed
26
27
opam init
eval $(opam env)
Benoit Viguier's avatar
Benoit Viguier committed
28
29
opam switch create Tweetnacl 4.06.1
eval $(opam env)
Benoit Viguier's avatar
Benoit Viguier committed
30
31
```

benoit's avatar
benoit committed
32
### 2. Set up general dependencies (coq 8.8.2, coqide, ssreflect, stdpp, coqprime, VST 2.0)
Benoit Viguier's avatar
Benoit Viguier committed
33

Benoit Viguier's avatar
Benoit Viguier committed
34
Add the repository general dependencies:
Benoit Viguier's avatar
Benoit Viguier committed
35
```bash
Benoit Viguier's avatar
Benoit Viguier committed
36
37
38
cd coq-verif-tweetnacl
opam repo add tweetnacl .
```
Benoit Viguier's avatar
Benoit Viguier committed
39

benoit's avatar
benoit committed
40
### 3. update and install dependencies.
Benoit Viguier's avatar
Benoit Viguier committed
41

Benoit Viguier's avatar
Benoit Viguier committed
42
```bash
Benoit Viguier's avatar
Benoit Viguier committed
43
opam update
benoit's avatar
benoit committed
44
opam install coq.8.8.2
Benoit Viguier's avatar
Benoit Viguier committed
45
# if you want coqide (may require additional dependencies)
Benoit Viguier's avatar
Benoit Viguier committed
46
opam install coqide.8.8.2
Benoit Viguier's avatar
Benoit Viguier committed
47
48
49
50
```

Pin the current repository as an opam to be able to fetch the dependencies
```bash
Benoit Viguier's avatar
Benoit Viguier committed
51
opam pin add -yn coq-verif-tweetnacl .
Benoit Viguier's avatar
Benoit Viguier committed
52
53
# install dependencies
opam install --deps-only coq-verif-tweetnacl
Benoit Viguier's avatar
Benoit Viguier committed
54
55
```

Benoit Viguier's avatar
Benoit Viguier committed
56

benoit's avatar
benoit committed
57
### 4. Install the full Verification
Benoit Viguier's avatar
Benoit Viguier committed
58
59

Everything is compiled the following command:
Benoit Viguier's avatar
Benoit Viguier committed
60
61

```bash
Benoit Viguier's avatar
Benoit Viguier committed
62
opam install coq-verif-tweetnacl
Benoit Viguier's avatar
Benoit Viguier committed
63
```
Benoit Viguier's avatar
Benoit Viguier committed
64

Benoit Viguier's avatar
Benoit Viguier committed
65
66
However if you want to compile each part you can follow these steps:

benoit's avatar
benoit committed
67
##### 4.1 Install TweetNacl Mathematical Model and Specification
Benoit Viguier's avatar
Benoit Viguier committed
68
69

To compile manually:
Benoit Viguier's avatar
Benoit Viguier committed
70
71
72
```bash
cd proofs/spec/
# create a pin of coq-tweetnacl-spec
Benoit Viguier's avatar
Benoit Viguier committed
73
opam pin add -yn coq-tweetnacl-spec .
Benoit Viguier's avatar
Benoit Viguier committed
74
75
76
77
78
79
80
./configure.sh
make -j
# if you want to compile the verification with VST
make install
```

Or you can let opam do the job:
Benoit Viguier's avatar
Benoit Viguier committed
81

Benoit Viguier's avatar
Benoit Viguier committed
82
```bash
Benoit Viguier's avatar
Benoit Viguier committed
83
84
cd proofs/spec/
# create a pin of coq-tweetnacl-spec
Benoit Viguier's avatar
Benoit Viguier committed
85
opam pin add -y coq-tweetnacl-spec .
Benoit Viguier's avatar
Benoit Viguier committed
86
87
```

benoit's avatar
benoit committed
88
##### 4.2 Install TweetNacl Verification
Benoit Viguier's avatar
Benoit Viguier committed
89

Benoit Viguier's avatar
Benoit Viguier committed
90
To compile manually:
Benoit Viguier's avatar
Benoit Viguier committed
91
```bash
Benoit Viguier's avatar
Benoit Viguier committed
92
93
cd proofs/vst/
# create a pin of coq-tweetnacl-vst
Benoit Viguier's avatar
Benoit Viguier committed
94
opam pin add -yn coq-tweetnacl-vst .
Benoit Viguier's avatar
Benoit Viguier committed
95
96
97
98
./configure.sh
make -j
# optional
make install
Benoit Viguier's avatar
Benoit Viguier committed
99
```
Benoit Viguier's avatar
Benoit Viguier committed
100

Benoit Viguier's avatar
Benoit Viguier committed
101
102
103
104
If you want to let opam do the job:
```bash
cd proofs/vst/
# create a pin of coq-tweetnacl-vst
Benoit Viguier's avatar
Benoit Viguier committed
105
opam pin add -y coq-tweetnacl-vst .
Benoit Viguier's avatar
Benoit Viguier committed
106
```
Benoit Viguier's avatar
Benoit Viguier committed
107

Benoit Viguier's avatar
Benoit Viguier committed
108
### Benchmarks
Benoit Viguier's avatar
Benoit Viguier committed
109

Benoit Viguier's avatar
Benoit Viguier committed
110
```bash
Benoit Viguier's avatar
Benoit Viguier committed
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
time opam install coq-verif-tweetnacl
The following actions will be performed:
install camlp5                    7.06.10-g84ce6cc4 [required by coq]
install conf-m4                   1                 [required by ocamlfind]
install ocamlbuild                0.14.0            [required by menhir]
install ocamlfind                 1.8.0             [required by coq]
install num                       1.2               [required by coq]
install menhir                    20180528          [required by coq-compcert]
install coq                       8.8.2             [required by coq-verif-tweetnacl]
install coq-stdpp                 1.1.0             [required by coq-verif-tweetnacl]
install coq-reciprocity           dev               [required by coq-verif-tweetnacl]
install coq-mathcomp-ssreflect    1.7.0             [required by coq-verif-tweetnacl]
install coq-compcert              3.2.0             [required by coq-vst]
install coq-bignums               8.8.dev           [required by coq-coqprime]
install coq-mathcomp-finmap       1.0.0             [required by coq-mathcomp-multinomials]
install coq-mathcomp-fingroup     1.7.0             [required by coq-mathcomp-algebra]
install coq-mathcomp-bigenough    1.0.0             [required by coq-mathcomp-multinomials]
install coq-vst                   2.0               [required by coq-verif-tweetnacl]
install coq-coqprime              1.0.3             [required by coq-verif-tweetnacl]
Benoit Viguier's avatar
Benoit Viguier committed
130
install coq-mathcomp-algebra      1.7.0             [required by coq-mathcomp-multinomials, coq-ssr-elliptic-curves]
Benoit Viguier's avatar
Benoit Viguier committed
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
install coq-mathcomp-solvable     1.7.0             [required by coq-mathcomp-field]
install coq-mathcomp-multinomials 1.1               [required by coq-verif-tweetnacl]
install coq-mathcomp-field        1.7.0             [required by coq-ssr-elliptic-curves]
install coq-ssr-elliptic-curves   dev               [required by coq-verif-tweetnacl]
install coq-verif-tweetnacl       dev
===== ∗ 23 =====
Do you want to continue? [Y/n] Y

<><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
[camlp5.7.06.10-g84ce6cc4] downloaded from cache at https://opam.ocaml.org/cache
[coq.8.8.2] downloaded from cache at https://opam.ocaml.org/cache
[coq-bignums.8.8.dev] synchronised from git+https://github.com/coq/bignums.git#v8.8
[coq-coqprime.1.0.3] downloaded from https://github.com/thery/coqprime/archive/v8.8.zip
[coq-mathcomp-bigenough.1.0.0] downloaded from https://github.com/math-comp/bigenough/archive/1.0.0.tar.gz
[coq-mathcomp-algebra.1.7.0] downloaded from http://github.com/math-comp/math-comp/archive/mathcomp-1.7.0.tar.gz
[coq-mathcomp-field.1.7.0] found in cache
[coq-mathcomp-fingroup.1.7.0] found in cache
[coq-compcert.3.2.0] synchronised from git+https://github.com/ildyria/CompCert.git#v3.2WithVO
[coq-mathcomp-solvable.1.7.0] found in cache
[coq-mathcomp-finmap.1.0.0] downloaded from https://github.com/math-comp/finmap/archive/1.0.0.tar.gz
[coq-mathcomp-ssreflect.1.7.0] found in cache
[coq-mathcomp-multinomials.1.1] downloaded from https://github.com/math-comp/multinomials/archive/1.1.tar.gz
[coq-stdpp.1.1.0] downloaded from https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp/repository/coq-stdpp-1.1.0/archive.tar.gz
[coq-verif-tweetnacl.dev] synchronised from git+https://gitlab.science.ru.nl/benoit/tweetnacl/
[coq-reciprocity.dev] synchronised from git+https://github.com/ildyria/coq-proofs.git
[coq-ssr-elliptic-curves.dev] synchronised from git+https://github.com/strub/elliptic-curves-ssr.git#981ac368cddef9719e188101ae5068720771dd40
[menhir.20180528] downloaded from cache at https://opam.ocaml.org/cache
[num.1.2] downloaded from cache at https://opam.ocaml.org/cache
[ocamlbuild.0.14.0] downloaded from cache at https://opam.ocaml.org/cache
[ocamlfind.1.8.0] downloaded from cache at https://opam.ocaml.org/cache
[coq-vst.2.0] synchronised from git+https://github.com/ildyria/VST.git#v2.0_ssReflect_notation

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
∗ installed conf-m4.1
∗ installed ocamlfind.1.8.0
∗ installed num.1.2
∗ installed ocamlbuild.0.14.0
∗ installed menhir.20180528
∗ installed camlp5.7.06.10-g84ce6cc4
∗ installed coq.8.8.2
∗ installed coq-bignums.8.8.dev
∗ installed coq-mathcomp-ssreflect.1.7.0
∗ installed coq-coqprime.1.0.3
∗ installed coq-mathcomp-bigenough.1.0.0
∗ installed coq-reciprocity.dev
∗ installed coq-stdpp.1.1.0
∗ installed coq-mathcomp-finmap.1.0.0
∗ installed coq-mathcomp-fingroup.1.7.0
∗ installed coq-mathcomp-algebra.1.7.0
∗ installed coq-compcert.3.2.0
∗ installed coq-mathcomp-multinomials.1.1
∗ installed coq-mathcomp-solvable.1.7.0
∗ installed coq-mathcomp-field.1.7.0
∗ installed coq-ssr-elliptic-curves.dev
∗ installed coq-vst.2.0
∗ installed coq-verif-tweetnacl.dev
Done.
opam install coq-verif-tweetnacl  11668.44s user 727.58s system 266% cpu 1:17:36.39 total
Benoit Viguier's avatar
Benoit Viguier committed
189
190
```

Benoit Viguier's avatar
Benoit Viguier committed
191
[1]: https://opam.ocaml.org/doc/Install.html