Skip to content
GitLab
Menu
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Benoit Viguier
coq-verif-tweetnacl
Commits
e2379147
Commit
e2379147
authored
Jul 29, 2019
by
Benoit Viguier
Browse files
update readme
parent
a2f9c766
Changes
1
Show whitespace changes
Inline
Side-by-side
README.md
View file @
e2379147
...
@@ -8,90 +8,200 @@
...
@@ -8,90 +8,200 @@
[
Install OPAM
][
1
]
, e.g. for Debian:
[
Install OPAM
][
1
]
, e.g. for Debian:
```
bash
```
bash
sudo
apt-get
install
gcc opam
sudo
apt-get
install
gcc opam
opam init
opam init
eval
`
opam config
env
`
eval
$(
opam
env
)
opam update
```
```
**Verify that you are using OPAM 2.x.**
**Verify that you are using OPAM 2.x.**
```
bash
opam
--version
# 2.0.3
```
##### 2. Set OPAM for Tweetnacl so it does not pollute other projects.
##### 2. Set OPAM for Tweetnacl so it does not pollute other projects.
Because we use Coq 8.8.2, we are forced to use Ocaml 4.06.1.
Because we use Coq 8.8.2, we are forced to use Ocaml 4.06.1.
```
bash
```
bash
opam switch create Tweetnacl 4.06.1
opam switch create Tweetnacl 4.06.1
eval
$(
opam
env
)
eval
$(
opam
env
)
```
```
##### 3.
D
ependencies (coq 8.8.2, coqide, ssreflect, stdpp, coqprime, VST 2.0)
##### 3.
Set up general d
ependencies (coq 8.8.2, coqide, ssreflect, stdpp, coqprime, VST 2.0)
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.)
Add the repository by using the address:
```
bash
```
bash
opam repo add coq-released https://coq.inria.fr/opam/released
opam repo add tweetnacl git://gitlab.science.ru.nl/benoit/tweetnacl/
opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev
# check if this line is necessary and how to provide anonymity
opam repo add tweetnacl git://gitlab.science.ru.nl/benoit/tweetnacl/
opam update
# if you want coqide
opam
install
coqide.8.8.2
# install the two main repository
opam
install
coq-vst.2.0
opam
install
--deps-only
coq-verif-tweetnacl
```
```
##### 4. Install TweetNacl Mathematical model
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 .
```
To compil
e
m
an
ually:
#### 5. updat
e an
d install dependencies.
```
bash
```
bash
cd
proofs/spec/
opam update
# create a pin of coq-tweetnacl-spec
# if you want coqide
opam pin add
-n
coq-tweetnacl-spec
.
opam
install
coqide.8.8.2
./configure.sh
# install dependencies
make
-j
opam
install
--deps-only
coq-verif-tweetnacl
# if you want to compile the verification with VST
make
install
```
```
If you want to let opam do the job:
#### 6. Install the full Verification
Everything is compiled the following command:
```
bash
```
bash
cd
proofs/spec/
opam
install
coq-verif-tweetnacl
# create a pin of coq-tweetnacl-spec
opam pin add
-n
coq-tweetnacl-spec
.
opam
install
coq-tweetnacl-spec
```
```
##### 5. Install TweetNacl Verification
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
To compile manually:
To compile manually:
```
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:
```
bash
```
bash
cd
proofs/vst/
cd
proofs/spec/
# create a pin of coq-tweetnacl-vst
# create a pin of coq-tweetnacl-spec
opam pin add
-n
coq-tweetnacl-vst
.
opam pin add
-n
coq-tweetnacl-spec
.
./configure.sh
opam
install
coq-tweetnacl-spec
make
-j
```
```
If you want to let opam do the job:
##### 6.2 Install TweetNacl Verification
To compile manually:
```
bash
```
bash
cd
proofs/vst/
cd
proofs/vst/
# create a pin of coq-tweetnacl-vst
# create a pin of coq-tweetnacl-vst
opam pin add
-n
coq-tweetnacl-vst
.
opam pin add
-n
coq-tweetnacl-vst
.
opam
install
coq-tweetnacl-vst
./configure.sh
make
-j
# optional
make
install
```
```
##### Benchmarks
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
```
**NEED TO BE REDONE**
##### Benchmarks
```
```
Tweetnacl: make all -j 396.46s user 13.92s system 266% cpu 2:33.77 total
▶ time opam install coq-verif-tweetnacl
Tweetnacl_verif: make -j 2164.06s user 12.94s system 227% cpu 15:58.79 total
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
```
```
[
1
]:
https://opam.ocaml.org/doc/Install.html
[
1
]:
https://opam.ocaml.org/doc/Install.html
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment