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
b912c25f
Commit
b912c25f
authored
Jul 29, 2019
by
Benoit Viguier
Browse files
remove warnings, anonymize
parent
c35e31b1
Changes
5
Hide whitespace changes
Inline
Side-by-side
README.md
View file @
b912c25f
...
...
@@ -54,7 +54,7 @@ opam install coqide.8.8.2
Pin the current repository as an opam to be able to fetch the dependencies
```
bash
opam pin add
-n
coq-verif-tweetnacl
.
opam pin add
-
y
n
coq-verif-tweetnacl
.
# install dependencies
opam
install
--deps-only
coq-verif-tweetnacl
```
...
...
@@ -76,7 +76,7 @@ To compile manually:
```
bash
cd
proofs/spec/
# create a pin of coq-tweetnacl-spec
opam pin add
-n
coq-tweetnacl-spec
.
opam pin add
-
y
n
coq-tweetnacl-spec
.
./configure.sh
make
-j
# if you want to compile the verification with VST
...
...
@@ -88,8 +88,7 @@ Or you can let opam do the job:
```
bash
cd
proofs/spec/
# create a pin of coq-tweetnacl-spec
opam pin add
-n
coq-tweetnacl-spec
.
opam
install
coq-tweetnacl-spec
opam pin add
-y
coq-tweetnacl-spec .
```
##### 6.2 Install TweetNacl Verification
...
...
@@ -98,7 +97,7 @@ To compile manually:
```
bash
cd
proofs/vst/
# create a pin of coq-tweetnacl-vst
opam pin add
-n
coq-tweetnacl-vst
.
opam pin add
-
y
n
coq-tweetnacl-vst
.
./configure.sh
make
-j
# optional
...
...
@@ -109,8 +108,7 @@ 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
opam pin add
-y
coq-tweetnacl-vst .
```
### Benchmarks
...
...
opam
View file @
b912c25f
opam-version: "2.0"
name: "coq-verif-tweetnacl"
maintainer: "benoit@cs.ru.nl"
homepage: "https://gitlab.science.ru.nl/benoit/tweetnacl/"
maintainer: "anonym"
homepage: "https://github.com/"
bug-reports: "https://github.com/"
dev-repo: "git+https://github.com/"
license: "MIT"
build: []
install: [
...
...
@@ -18,12 +20,10 @@ depends: [
"coq-reciprocity"
"coq-vst" {= "2.0"}
]
author: [
"benoit@cs.ru.nl"
]
authors: [
"anonym"
]
synopsis: "Verifying the TweetNaCl implementation"
description: """
Verifying the TweetNaCl implementation
Verifying the TweetNaCl implementation
.
"""
url {
src: "git+https://gitlab.science.ru.nl/benoit/tweetnacl/"
}
packages/coq-verif-tweetnacl/coq-verif-tweetnacl.dev/opam
deleted
100644 → 0
View file @
c35e31b1
opam-version: "2.0"
name: "coq-verif-tweetnacl"
maintainer: "benoit@cs.ru.nl"
homepage: "https://gitlab.science.ru.nl/benoit/tweetnacl/"
license: "MIT"
build: []
install: [
[make "-j%{jobs}%"]
]
remove: []
depends: [
"coq" {>= "8.7.0" & < "8.9"}
"coq-coqprime" {= "1.0.3"}
"coq-stdpp" {= "1.1.0"}
"coq-ssr-elliptic-curves"
"coq-mathcomp-multinomials"
"coq-mathcomp-ssreflect" {= "1.7.0"}
"coq-reciprocity"
"coq-vst" {= "2.0"}
]
author: [
"benoit@cs.ru.nl"
]
description: """
Verifying the TweetNaCl implementation
"""
url {
src: "git+https://gitlab.science.ru.nl/benoit/tweetnacl/"
}
proofs/spec/opam
View file @
b912c25f
opam-version: "2.0"
name: "coq-tweetnacl-spec"
maintainer: "benoit@cs.ru.nl"
homepage: "https://gitlab.science.ru.nl/benoit/tweetnacl/"
maintainer: "anonym"
homepage: "https://github.com/"
bug-reports: "https://github.com/"
dev-repo: "git+https://github.com/"
license: "MIT"
build: [
["./configure.sh"]
...
...
@@ -21,12 +23,9 @@ depends: [
"coq-reciprocity"
]
author: [
"benoit@cs.ru.nl"
"timmy@timmyweerwag.nl"
"anonym"
]
synopsis: "Verifying the TweetNaCl implementation: Spec"
description: """
Verifying the Tweetnacl implementation: Specification
"""
url {
src: "git+https://github.com/ildyria/coq-tweetnacl-verif/tree/master/proofs/spec"
}
proofs/vst/opam
View file @
b912c25f
opam-version: "2.0"
name: "coq-tweetnacl-vst"
maintainer: "benoit@cs.ru.nl"
homepage: "https://gitlab.science.ru.nl/benoit/tweetnacl/"
maintainer: "anonym"
homepage: "https://github.com/"
bug-reports: "https://github.com/"
dev-repo: "git+https://github.com/"
license: "MIT"
build: [
["./configure.sh"]
...
...
@@ -21,11 +23,9 @@ depends: [
"coq-tweetnacl-spec"
]
author: [
"
benoit@cs.ru.nl
"
"
anonym
"
]
synopsis: "Verifying the TweetNaCl implementation: VST"
description: """
Verifying the Tweetnacl implementation: VST
"""
url {
src: "git+https://github.com/ildyria/coq-tweetnacl-verif/master/tree/proofs/vst"
}
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Attach a 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