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

Benoit Viguier's avatar
Benoit Viguier committed
4
## Setting up your environment
Benoit Viguier's avatar
Benoit Viguier committed
5

Benoit Viguier's avatar
Benoit Viguier committed
6
7
8
##### 1. download & install GCC and OPAM.

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

Benoit Viguier's avatar
Benoit Viguier committed
10
```bash
Benoit Viguier's avatar
Benoit Viguier committed
11
12
13
sudo apt-get install gcc opam
opam init
eval $(opam env)
Benoit Viguier's avatar
Benoit Viguier committed
14
```
Benoit Viguier's avatar
Benoit Viguier committed
15

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

Benoit Viguier's avatar
Benoit Viguier committed
18
19
20
21
22
```bash
opam --version
# 2.0.3
```

Benoit Viguier's avatar
Benoit Viguier committed
23
24
##### 2. Set OPAM for Tweetnacl so it does not pollute other projects.

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

Benoit Viguier's avatar
Benoit Viguier committed
27
```bash
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 Viguier's avatar
Benoit Viguier committed
32
##### 3. 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
35
36
37
38
39
40
Add the repository general dependencies:
```bash
opam repo add coq-released https://coq.inria.fr/opam/released
opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev
```

#### 4. Set up project related dependencies (dependencies at specific commit number.)
Benoit Viguier's avatar
Benoit Viguier committed
41

Benoit Viguier's avatar
Benoit Viguier committed
42
Add the repository by using the address:
Benoit Viguier's avatar
Benoit Viguier committed
43
```bash
Benoit Viguier's avatar
Benoit Viguier committed
44
opam repo add tweetnacl git://gitlab.science.ru.nl/benoit/tweetnacl/
Benoit Viguier's avatar
Benoit Viguier committed
45
```
Benoit Viguier's avatar
Benoit Viguier committed
46

Benoit Viguier's avatar
Benoit Viguier committed
47
48
49
50
51
52
Or by cloning it:
```bash
git clone https://gitlab.science.ru.nl/benoit/tweetnacl/ coq-verif-tweetnacl
cd coq-verif-tweetnacl
opam repo add tweetnacl .
```
Benoit Viguier's avatar
Benoit Viguier committed
53

Benoit Viguier's avatar
Benoit Viguier committed
54
#### 5. update and install dependencies.
Benoit Viguier's avatar
Benoit Viguier committed
55

Benoit Viguier's avatar
Benoit Viguier committed
56
```bash
Benoit Viguier's avatar
Benoit Viguier committed
57
58
59
60
61
opam update
# if you want coqide
opam install coqide.8.8.2
# install dependencies
opam install --deps-only coq-verif-tweetnacl
Benoit Viguier's avatar
Benoit Viguier committed
62
63
```

Benoit Viguier's avatar
Benoit Viguier committed
64
65
66
#### 6. Install the full Verification

Everything is compiled the following command:
Benoit Viguier's avatar
Benoit Viguier committed
67
68

```bash
Benoit Viguier's avatar
Benoit Viguier committed
69
opam install coq-verif-tweetnacl
Benoit Viguier's avatar
Benoit Viguier committed
70
```
Benoit Viguier's avatar
Benoit Viguier committed
71

Benoit Viguier's avatar
Benoit Viguier committed
72
73
74
75
76
77
78
79
80
However if you want to compile each part you can follow these steps:

Clone the repository:
```bash
git clone https://gitlab.science.ru.nl/benoit/tweetnacl/ coq-verif-tweetnacl
cd coq-verif-tweetnacl
```

##### 6.1 Install TweetNacl Mathematical Model and Specification
Benoit Viguier's avatar
Benoit Viguier committed
81
82

To compile manually:
Benoit Viguier's avatar
Benoit Viguier committed
83
84
85
86
87
88
89
90
91
92
93
```bash
cd proofs/spec/
# create a pin of coq-tweetnacl-spec
opam pin add -n coq-tweetnacl-spec .
./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
94

Benoit Viguier's avatar
Benoit Viguier committed
95
```bash
Benoit Viguier's avatar
Benoit Viguier committed
96
97
98
99
cd proofs/spec/
# create a pin of coq-tweetnacl-spec
opam pin add -n coq-tweetnacl-spec .
opam install coq-tweetnacl-spec
Benoit Viguier's avatar
Benoit Viguier committed
100
101
```

Benoit Viguier's avatar
Benoit Viguier committed
102
##### 6.2 Install TweetNacl Verification
Benoit Viguier's avatar
Benoit Viguier committed
103

Benoit Viguier's avatar
Benoit Viguier committed
104
To compile manually:
Benoit Viguier's avatar
Benoit Viguier committed
105
```bash
Benoit Viguier's avatar
Benoit Viguier committed
106
107
108
109
110
111
112
cd proofs/vst/
# create a pin of coq-tweetnacl-vst
opam pin add -n coq-tweetnacl-vst .
./configure.sh
make -j
# optional
make install
Benoit Viguier's avatar
Benoit Viguier committed
113
```
Benoit Viguier's avatar
Benoit Viguier committed
114

Benoit Viguier's avatar
Benoit Viguier committed
115
116
117
118
119
120
121
If you want to let opam do the job:
```bash
cd proofs/vst/
# create a pin of coq-tweetnacl-vst
opam pin add -n coq-tweetnacl-vst .
opam install coq-tweetnacl-vst
```
Benoit Viguier's avatar
Benoit Viguier committed
122

Benoit Viguier's avatar
Benoit Viguier committed
123
##### Benchmarks
Benoit Viguier's avatar
Benoit Viguier committed
124

Benoit Viguier's avatar
Benoit Viguier committed
125
```
Benoit Viguier's avatar
Benoit Viguier committed
126
127
128
129
130
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
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
▶ 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]
  ∗ install coq-mathcomp-algebra      1.7.0             [required by coq-mathcomp-multinomials,
                                                        coq-ssr-elliptic-curves]
  ∗ 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
205
206
```

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