Commit 65c956a2 authored by Benoit Viguier's avatar Benoit Viguier
Browse files

updated readme

parent 0c382f85
...@@ -35,52 +35,65 @@ eval $(opam env) ...@@ -35,52 +35,65 @@ eval $(opam env)
```bash ```bash
opam repo add coq-released https://coq.inria.fr/opam/released opam repo add coq-released https://coq.inria.fr/opam/released
opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev
opam repo add tweetnacl git://github.com/ildyria/opam-repository.git opam repo add tweetnacl git://gitlab.science.ru.nl/benoit/tweetnacl/
opam update opam update
# if you want coqide # if you want coqide
opam install coqide opam install coqide.8.8.2
# install the two main repository # install the two main repository
opam install coq-vst.2.0 opam install coq-vst.2.0
opam install --deps-only coq-tweetnacl opam install --deps-only coq-verif-tweetnacl
``` ```
##### 4. Install TweetNacl Mathematical model ##### 4. Install TweetNacl Mathematical model
To compile manually:
```bash ```bash
git clone https://gitlab.science.ru.nl/benoit/Tweetnacl.git Tweetnacl cd proofs/spec/
cd Tweetnacl # create a pin of coq-tweetnacl-spec
# create a pin of Tweetnacl opam pin add -n coq-tweetnacl-spec .
opam pin add -n coq-tweetnacl . ./configure.sh
make -j make -j
cd .. # if you want to compile the verification with VST
opam install coq-tweetnacl make install
``` ```
Another possibility is to use `opam source`. This will create a If you want to let opam do the job:
`coq-tweetnacl.dev` repo in your current directory
(equivalent of `git clone`). ```bash
cd proofs/spec/
# create a pin of coq-tweetnacl-spec
opam pin add -n coq-tweetnacl-spec .
opam install coq-tweetnacl-spec
```
##### 5. Install TweetNacl Verification
To compile manually:
```bash ```bash
opam source coq-tweetnacl --pin cd proofs/vst/
cd coq-tweetnacl.dev # create a pin of coq-tweetnacl-spec
opam pin add -n coq-tweetnacl-spec .
./configure.sh ./configure.sh
make -j make -j
cd .. # if you want to compile the verification with VST
opam install coq-tweetnacl make install
``` ```
##### 5. Install TweetNacl_verif (optional) If you want to let opam do the job:
```bash ```bash
git clone https://gitlab.science.ru.nl/benoit/Tweetnacl_verif.git Tweetnacl_verif cd proofs/spec/
cd Tweetnacl_verif # create a pin of coq-tweetnacl-vst
./configure.sh opam pin add -n coq-tweetnacl-vst .
make -j opam install coq-tweetnacl-vst
``` ```
##### Benchmarks ##### Benchmarks
**NEED TO BE REDONE**
``` ```
Tweetnacl: make all -j 396.46s user 13.92s system 266% cpu 2:33.77 total Tweetnacl: make all -j 396.46s user 13.92s system 266% cpu 2:33.77 total
Tweetnacl_verif: make -j 2164.06s user 12.94s system 227% cpu 15:58.79 total Tweetnacl_verif: make -j 2164.06s user 12.94s system 227% cpu 15:58.79 total
......
all: coq-tweetnacl-spec coq-tweetnacl-vst all: coq-tweetnacl-spec coq-tweetnacl-vst
coq-tweetnacl-spec: coq-tweetnacl-spec:
cd proofs/spec ;\ cd proofs/spec ;\
./configure.sh ;\ ./configure.sh ;\
......
...@@ -25,7 +25,7 @@ author: [ ...@@ -25,7 +25,7 @@ author: [
"timmy@timmyweerwag.nl" "timmy@timmyweerwag.nl"
] ]
description: """ description: """
Model to verify Tweetnacl Verifying the Tweetnacl implementation: Specification
""" """
url { url {
src: "git+https://github.com/ildyria/coq-tweetnacl-verif/tree/master/proofs/spec" src: "git+https://github.com/ildyria/coq-tweetnacl-verif/tree/master/proofs/spec"
......
opam-version: "2.0" opam-version: "2.0"
name: "coq-tweetnacl-vst" name: "coq-tweetnacl-vst"
maintainer: "benoit@cs.ru.nl" maintainer: "benoit@cs.ru.nl"
homepage: "https://gitlab.science.ru.nl/benoit/Tweetnacl_verif/" homepage: "https://gitlab.science.ru.nl/benoit/tweetnacl/"
license: "MIT" license: "MIT"
build: [ build: [
["./configure.sh"] ["./configure.sh"]
...@@ -12,9 +12,9 @@ install: [ ...@@ -12,9 +12,9 @@ install: [
] ]
remove: ["rm" "-R" "%{lib}%/coq/user-contrib/Tweetnacl_verif"] remove: ["rm" "-R" "%{lib}%/coq/user-contrib/Tweetnacl_verif"]
depends: [ depends: [
"coq" {>= "8.7.0"} "coq" {>= "8.7.0" & < "8.9"}
"coq-coqprime" "coq-coqprime" {= "1.0.3"}
"coq-stdpp" "coq-stdpp" {= "1.1.0"}
"coq-ssr-elliptic-curves" "coq-ssr-elliptic-curves"
"coq-mathcomp-ssreflect" "coq-mathcomp-ssreflect"
"coq-vst" {= "2.0"} "coq-vst" {= "2.0"}
...@@ -24,7 +24,7 @@ author: [ ...@@ -24,7 +24,7 @@ author: [
"benoit@cs.ru.nl" "benoit@cs.ru.nl"
] ]
description: """ description: """
Verifying the Tweetnacl implementation with VST Verifying the Tweetnacl implementation: VST
""" """
url { url {
src: "git+https://github.com/ildyria/coq-tweetnacl-verif/master/tree/proofs/vst" src: "git+https://github.com/ildyria/coq-tweetnacl-verif/master/tree/proofs/vst"
......
opam-version: "2.0" opam-version: "2.0"
name: "coq-tweetnacl-verif" name: "coq-tweetnacl-verif"
maintainer: "benoit@cs.ru.nl" maintainer: "benoit@cs.ru.nl"
homepage: "https://gitlab.science.ru.nl/benoit/Tweetnacl_verif/" homepage: "https://gitlab.science.ru.nl/benoit/tweetnacl/"
license: "MIT" license: "MIT"
build: [] build: []
install: [ install: [
...@@ -22,8 +22,8 @@ author: [ ...@@ -22,8 +22,8 @@ author: [
"benoit@cs.ru.nl" "benoit@cs.ru.nl"
] ]
description: """ description: """
Verifying the Tweetnacl implementation with VST Verifying the Tweetnacl implementation
""" """
url { url {
src: "git+https://github.com/ildyria/coq-tweetnacl-verif/" src: "git+https://gitlab.science.ru.nl/benoit/tweetnacl/"
} }
...@@ -25,7 +25,7 @@ author: [ ...@@ -25,7 +25,7 @@ author: [
"timmy@timmyweerwag.nl" "timmy@timmyweerwag.nl"
] ]
description: """ description: """
Model to verify Tweetnacl Verifying the Tweetnacl implementation: Specification
""" """
url { url {
src: "git+https://github.com/ildyria/coq-tweetnacl-verif/tree/master/proofs/spec" src: "git+https://github.com/ildyria/coq-tweetnacl-verif/tree/master/proofs/spec"
......
# PROOFS of correctness of Curve25519
1. Set up the environment as explained here:
[https://gitlab.science.ru.nl/benoit/tweetnacl](https://gitlab.science.ru.nl/benoit/tweetnacl).
2. Download that repo:
`git clone https://gitlab.science.ru.nl:benoit/Tweetnacl_verif.git`
3. Do `./configure.sh` followed by `make`.
```sh
make -j 2164.06s user 12.94s system 227% cpu 15:58.79 total
```
opam-version: "2.0" opam-version: "2.0"
name: "coq-tweetnacl-vst" name: "coq-tweetnacl-vst"
maintainer: "benoit@cs.ru.nl" maintainer: "benoit@cs.ru.nl"
homepage: "https://gitlab.science.ru.nl/benoit/Tweetnacl_verif/" homepage: "https://gitlab.science.ru.nl/benoit/tweetnacl/"
license: "MIT" license: "MIT"
build: [ build: [
["./configure.sh"] ["./configure.sh"]
...@@ -24,7 +24,7 @@ author: [ ...@@ -24,7 +24,7 @@ author: [
"benoit@cs.ru.nl" "benoit@cs.ru.nl"
] ]
description: """ description: """
Verifying the Tweetnacl implementation with VST Verifying the Tweetnacl implementation: VST
""" """
url { url {
src: "git+https://github.com/ildyria/coq-tweetnacl-verif/master/tree/proofs/vst" src: "git+https://github.com/ildyria/coq-tweetnacl-verif/master/tree/proofs/vst"
......
opam-version: "2.0" opam-version: "2.0"
upstream: "https://github.com/ildyria/coq-tweetnacl-verif/tree/master/" upstream: "https://gitlab.science.ru.nl/benoit/tweetnacl/"
browse: "" browse: ""
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment