packaging

.gitignore

@@ -38,7 +38,8 @@ Doc
 usenix*
 .coqdeps.d
 Makefile.conf
-Makefile
+proofs/*/Makefile
+.dist
 
 # Created by https://www.gitignore.io/api/latex,c++,coq,c,ocaml,sublimetext,vim,emacs
 
@@ -79,6 +80,7 @@ Makefile
 *.vrb
 *.xdy
 *.tdo
+coq-verif-tweetnacl*
 
 ### C++ ###
 # Compiled Object files

Makefile

+DIST=coq-verif-tweetnacl
+
+all: coq-tweetnacl-spec coq-tweetnacl-vst
+
+readme:
+	less README.md
+
+
+# DEFINE GENERIC ROUTINES (hidden via . prefix)
+.configure1 .configure2:
+	cd $P && $(SHELL) configure.sh
+
+.building1 .building2:
+	cd $P && $(MAKE) -j
+	cd $P && $(MAKE) install
+
+.dusting1 .dusting2:
+	cd $P && $(MAKE) clean
+	cd $P && rm _CoqProject
+	cd $P && rm Makefile
+	cd $P && rm Makefile.conf
+
+# DEFINE REAL TARGETS
+coq-tweetnacl-spec: P=proofs/spec
+coq-tweetnacl-spec: .configure1 .building1
+
+clean-spec: P=proofs/spec
+clean-spec: .configure1 .dusting1
+
+coq-tweetnacl-vst: P=proofs/vst
+coq-tweetnacl-vst: coq-tweetnacl-spec .configure2 .building2
+
+clean-vst: P=proofs/vst
+clean-vst: .configure2 .dusting2
+
+clean: clean-spec clean-vst clean-dist
+
+# build paper
+paper:
+	cd paper && $(MAKE)
+
+clean-paper:
+	cd paper && $(MAKE) clean
+
+# generate artefact
+$(DIST):
+	mkdir $(DIST)
+
+dist: $(DIST)
+	cp -r proofs $(DIST)
+	mkdir $(DIST)/packages
+	cp -r packages/coq-compcert $(DIST)/packages/
+	cp -r packages/coq-reciprocity $(DIST)/packages/
+	cp -r packages/coq-ssr-elliptic-curves $(DIST)/packages/
+	cp -r packages/coq-vst $(DIST)/packages/
+	cp repo $(DIST)/
+	cp version $(DIST)/
+	cp README.md $(DIST)/
+	cp Makefile $(DIST)/
+	tar -czvf $(DIST).tar.gz $(DIST)
+
+clean-dist: $(DIST)
+	rm -r $(DIST)
+	-rm $(DIST).tar.gz

README.md

@@ -39,14 +39,7 @@ 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
-opam repo add tweetnacl git://gitlab.science.ru.nl/benoit/tweetnacl/
-```
-
-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 .
 ```
@@ -55,12 +48,18 @@ opam repo add tweetnacl .
 
 ```bash
 opam update
-# if you want coqide
+# if you want coqide (may require additional dependencies)
 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 .
 # install dependencies
 opam install --deps-only coq-verif-tweetnacl
 ```
 
+
 ### 6. Install the full Verification
 
 Everything is compiled the following command:
@@ -71,12 +70,6 @@ opam install coq-verif-tweetnacl
 
 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:
@@ -122,7 +115,7 @@ opam install coq-tweetnacl-vst
 
 ### Benchmarks
 
-```
+```bash
 ▶ time opam install coq-verif-tweetnacl
 The following actions will be performed:
   ∗ install camlp5                    7.06.10-g84ce6cc4 [required by coq]

makefile

-all: coq-tweetnacl-spec coq-tweetnacl-vst
-
-coq-tweetnacl-spec:
-	cd proofs/spec ;\
-	./configure.sh ;\
-	$(MAKE) -j ;\
-	$(MAKE) install
-
-coq-tweetnacl-vst: coq-tweetnacl-spec
-	cd proofs/vst ;\
-	./configure.sh ;\
-	$(MAKE) -j ;\
-	$(MAKE) install

packages/coq-tweetnacl-spec/coq-tweetnacl-spec.dev/opam → opam

 opam-version: "2.0"
-name: "coq-tweetnacl-spec"
+name: "coq-verif-tweetnacl"
 maintainer: "benoit@cs.ru.nl"
 homepage: "https://gitlab.science.ru.nl/benoit/tweetnacl/"
 license: "MIT"
-build: [
-  ["./configure.sh"]
-  [make "-j%{jobs}%"]
-]
+build: []
 install: [
-  [make "install"]
+  [make "-j%{jobs}%" "all"]
 ]
-remove: ["rm" "-R" "%{lib}%/coq/user-contrib/Tweetnacl"]
+remove: []
 depends: [
   "coq" {>= "8.7.0" & < "8.9"}
   "coq-coqprime" {= "1.0.3"}
@@ -19,14 +16,14 @@ depends: [
   "coq-mathcomp-multinomials"
   "coq-mathcomp-ssreflect" {= "1.7.0"}
   "coq-reciprocity"
+  "coq-vst" {= "2.0"}
 ]
 author: [
   "benoit@cs.ru.nl"
-  "timmy@timmyweerwag.nl"
   ]
 description: """
-Verifying the Tweetnacl implementation: Specification
+Verifying the TweetNaCl implementation
 """
 url {
-  src: "git+https://github.com/ildyria/coq-tweetnacl-verif/tree/master/proofs/spec"
+  src: "git+https://gitlab.science.ru.nl/benoit/tweetnacl/"
 }

packages/coq-reciprocity/coq-reciprocity.dev/opam

@@ -22,5 +22,5 @@ description:"""
 Various proofs in Coq. As of now, only contains the proof of the theorem of quadratic reciprocity.
 """
 url {
-  src: "git+https://github.com/ildyria/coq-proofs.git"
+  src: "git+https://github.com/ildyria/coq-proofs.git#fork"
 }

packages/coq-tweetnacl-vst/coq-tweetnacl-vst.dev/opam

-opam-version: "2.0"
-name: "coq-tweetnacl-vst"
-maintainer: "benoit@cs.ru.nl"
-homepage: "https://gitlab.science.ru.nl/benoit/tweetnacl/"
-license: "MIT"
-build: [
-  ["./configure.sh"]
-  [make "-j%{jobs}%"]
-]
-install: [
-  [make "install"]
-]
-remove: ["rm" "-R" "%{lib}%/coq/user-contrib/Tweetnacl_verif"]
-depends: [
-  "coq" {>= "8.7.0" & < "8.9"}
-  "coq-coqprime" {= "1.0.3"}
-  "coq-stdpp" {= "1.1.0"}
-  "coq-ssr-elliptic-curves"
-  "coq-mathcomp-ssreflect"
-  "coq-vst" {= "2.0"}
-  "coq-tweetnacl-spec"
-]
-author: [
-  "benoit@cs.ru.nl"
-  ]
-description: """
-Verifying the Tweetnacl implementation: VST
-"""
-url {
-  src: "git+https://github.com/ildyria/coq-tweetnacl-verif/master/tree/proofs/vst"
-}

packages/coq-verif-tweetnacl/coq-verif-tweetnacl.dev/opam

 opam-version: "2.0"
-name: "coq-tweetnacl-verif"
+name: "coq-verif-tweetnacl"
 maintainer: "benoit@cs.ru.nl"
 homepage: "https://gitlab.science.ru.nl/benoit/tweetnacl/"
 license: "MIT"
@@ -22,7 +22,7 @@ author: [
   "benoit@cs.ru.nl"
   ]
 description: """
-Verifying the Tweetnacl implementation
+Verifying the TweetNaCl implementation
 """
 url {
   src: "git+https://gitlab.science.ru.nl/benoit/tweetnacl/"

proofs/spec/C/break.c

-#include <stdio.h>
-#include <stdbool.h>
-
-typedef long long i64;
-typedef i64 gf[16];
-
-
-#define BYTE_TO_BINARY_PATTERN "%c%c%c%c%c%c%c%c"
-#define BYTE_TO_BINARY(byte)  \
-  (byte & 0x80 ? '1' : '0'), \
-  (byte & 0x40 ? '1' : '0'), \
-  (byte & 0x20 ? '1' : '0'), \
-  (byte & 0x10 ? '1' : '0'), \
-  (byte & 0x08 ? '1' : '0'), \
-  (byte & 0x04 ? '1' : '0'), \
-  (byte & 0x02 ? '1' : '0'), \
-  (byte & 0x01 ? '1' : '0')
-
-
-static void print_bin64(i64 val)
-{
-	printf(" "BYTE_TO_BINARY_PATTERN" "BYTE_TO_BINARY_PATTERN" "BYTE_TO_BINARY_PATTERN" "BYTE_TO_BINARY_PATTERN,
-		BYTE_TO_BINARY(val>>56), BYTE_TO_BINARY(val>>48), BYTE_TO_BINARY(val>>40), BYTE_TO_BINARY(val >> 32));
-	printf(" "BYTE_TO_BINARY_PATTERN" "BYTE_TO_BINARY_PATTERN" "BYTE_TO_BINARY_PATTERN" "BYTE_TO_BINARY_PATTERN,
-		BYTE_TO_BINARY(val>>24), BYTE_TO_BINARY(val>>16), BYTE_TO_BINARY(val>>8), BYTE_TO_BINARY(val));
-	printf("\n");
-}
-
-static void print_o(gf o)
-{
-    for (int j = 0; j < 16; ++j)
-	{
-		printf("%2i: ", j);
-		print_bin64(o[j]);
-	}
-
-}
-
-static void car25519(gf o, bool b)
-{
-  int i;
-  i64 c;
-  for (i = 0;i < 16;++i) {
-    // o[i]+=(1LL<<16);
-    c=o[i]>>16;
-    // o[(i+1)*(i<15)]+=c-1+37*(c-1)*(i==15);
-    o[(i+1)*(i<15)]+=c+37*(c)*(i==15);
-    o[i]-=c<<16;
-
-    if(b){
-		// added to have a look at what is going on in there
-		printf("%2i : ---------------------------------------------\n",i);
-		for (int j = 0; j < 16; ++j)
-		{
-			printf("%2i: ", j);
-			print_bin64(o[j]);
-		}
-    }
-  }
-}
-
-int main(int argc, char const *argv[])
-{
-	gf o;
-	i64 val = 0xFFFF;
-	for (int i = 0; i < 16; ++i)
-	{
-		o[i] = val;
-	}
-
-	o[15] = val | (val << 32);
-	for (int i = 0; i < 16; ++i)
-	{
-		printf("%2i: ", i);
-		print_bin64(o[i]);
-	}
-
-
-	printf("#################################################### EXP: 2 carry is not enough\n");
-	printf("carry 1\n");
-	car25519(o,0);
-	printf("result carry 1:__________________________________________\n");
-	print_o(o);
-
-	printf("carry 2\n");
-	car25519(o,0);
-	printf("result carry 2:__________________________________________\n");
-	print_o(o);
-
-	printf("#################################################### EXP: -15, 1 step\n");
-
-	for (int i = 0; i < 16; ++i)
-	{
-		o[i] = 0;
-	}
-	o[0] = -15;
-	print_o(o);
-
-	print_bin64(o[0]);
-    o[0]+=(1LL<<16);
-    i64 c;
-    printf("o[0]+=(1LL<<16)\n");
-	print_bin64(o[0]);
-
-    c=o[0]>>16;
-    printf("c=o[0]>>16;\n");
-	print_bin64(c);
-
-    o[1]+=c-1;
-    printf("o[1]+=c-1;\n");
-	print_bin64(o[1]);
-
-    o[0]-=c<<16;
-    printf("o[0]-=c<<16;\n");
-	print_bin64(o[0]);
-
-	printf("result carry step 1:_____________________________________\n");
-	print_o(o);
-
-	printf("#################################################### EXP: -15 all steps\n");
-
-	for (int i = 0; i < 16; ++i)
-	{
-		o[i] = 0;
-	}
-	o[15] = -1;
-	print_o(o);
-
-	car25519(o,0);
-	printf("result carry 1:__________________________________________\n");
-	print_o(o);
-	car25519(o,0);
-	printf("result carry 2:__________________________________________\n");
-	print_o(o);
-	car25519(o,0);
-	printf("result carry 3:__________________________________________\n");
-	print_o(o);
-
-	printf("####################################################\n");
-
-	i64 t = -0xFFFFF;
-	printf("%li\n", t);
-	print_bin64(t);
-	t -= (t >> 16) << 16;
-	printf("%li\n", t);
-	print_bin64(t);
-
-	printf("####################################################\n");
-	t = -0xFFFC5;
-	printf("%li\n", t);
-	print_bin64(t);
-	i64 tt = t >> 16;
-	printf("%li\n", tt);
-	print_bin64(tt);
-	tt <<= 16;
-	printf("%li\n", tt);
-	print_bin64(tt);
-	t -= tt;
-	printf("%li\n", t);
-	print_bin64(t);
-
-
-	return 0;
-}

proofs/spec/configure.sh

 #!/bin/sh
 
-# remove _CoqProject if it alreqdy exists
+# remove _CoqProject if it already exists
 [ -e _CoqProject ] && rm _CoqProject
 
-while : ; do
-	case "$1" in
-	"")
-		break;;
-	--no-High|--no-high)
-		nohigh=true; shift;;
-	esac
-done
-
-if test "$nohigh" = "true"; then
-	echo "no-high"
-	filt='^C|^slides|^readings|^High|^gen'
-else
-	filt='^C|^slides|^readings|^gen'
-fi
-
 # generate the path for coqide and voqv
-for D in $(find * -maxdepth 1 -type d | egrep -v $filt); do
+for D in $(find * -maxdepth 1 -type d); do
 	echo "-Q $D Tweetnacl.$D" | sed 's/\//./2'>> _CoqProject
 done
 
 echo "" >> _CoqProject
 
 # generate the list of files for coq_makefile
-# ls */*.v | egrep -v $filt >> _CoqProject
-find * -name "*.v" -print | egrep -v $filt >> _CoqProject
- 
+find * -name "*.v" -print >> _CoqProject
 
 coq_makefile INSTALLDEFAULTROOT = Tweetnacl -f _CoqProject -o Makefile
-# coq_makefile -f _CoqProject -o Makefile
-

proofs/vst/Makefile.local

@@ -4,9 +4,15 @@ ifeq (,$(wildcard ./c/tweetnaclVerifiableC.v))
 endif
 
 clean::
-	$(HIDE)echo "rm c/tweetnaclVerifiableC.v"
-	$(HIDE)rm c/tweetnaclVerifiableC.v 2> /dev/null || true
+	$(HIDE)rm .lia.cache 2> /dev/null || true
+	$(HIDE)rm .nia.cache 2> /dev/null || true
+	$(HIDE)rm */*.crashcoqide 2> /dev/null || true
+	$(HIDE)rm */.*.aux 2> /dev/null || true
+	$(HIDE)rm */*.glob 2> /dev/null || true
+	$(HIDE)rm */*.v.d 2> /dev/null || true
 	$(HIDE)rm *.dpd 2> /dev/null || true
+	$(HIDE)rm c/tweetnaclVerifiableC.v 2> /dev/null || true
+	$(HIDE)rm c/.tweetnaclVerifiableC.aux 2> /dev/null || true
 
 DPD = $(wildcard *.dpd)
 DOT = $(DPD:%.dpd=%.dot)

proofs/vst/configure.sh

 #!/bin/sh
 
-name=""
+cd c
 
-cd c;
 # generate the .v file of TweetnaclVerifiableC.c
 clightgen -normalize tweetnaclVerifiableC.c
+
 # set the proper path to compcert library
-sed -i 's/^Require Import/From compcert.exportclight Require Import/' tweetnaclVerifiableC.v 
+sed -i 's/^Require Import/From compcert.exportclight Require Import/' tweetnaclVerifiableC.v
+
 cd ..
 
 # remove _CoqProject if it alreqdy exists
 [ -e _CoqProject ] && rm _CoqProject
 
-# generate the path for coqide and voqv
+# generate the path for coqide and coqv
 for D in */; do
 	echo $D | sed 's/.$//' | echo "-R $(cat -) Tweetnacl_verif" >> _CoqProject
 done
@@ -21,5 +22,3 @@ done
 ls */*.v >> _CoqProject
 
 coq_makefile INSTALLDEFAULTROOT = Tweetnacl_verif -f _CoqProject -o Makefile
-# coq_makefile -f _CoqProject -o Makefile
-