tweetnacl.diff is now directly generated from source ../proofs/vst/c/

paper/Makefile

@@ -37,6 +37,15 @@ depend:
 
 .PHONY: clean FORCE
 
+tweetnacl.diff:
+	@echo $(BOLD)$(YELLOW)"Generating tweetnacl.diff"$(NO_COLOR)$(DARKGRAY)
+	diff -u ../proofs/vst/c/tweetnacl.c ../proofs/vst/c/tweetnaclVerifiableC.c > tweetnacl.diff.tmp; [ $$? -eq 1 ]
+	sed -i -e 1,2d tweetnacl.diff.tmp
+	echo '--- tweetnacl.c' >> tweetnacl.diff
+	echo '+++ tweetnaclVerifiableC.c' >> tweetnacl.diff
+	cat tweetnacl.diff.tmp >> tweetnacl.diff
+	rm tweetnacl.diff.tmp
+
 clean:
 	@echo $(BOLD)$(RED)"cleaning..."$(NO_COLOR)
 	@rm -fr latex.out 2> /dev/null || true
@@ -54,6 +63,7 @@ clean:
 	@rm *.bak 2> /dev/null || true
 	@rm */*.aux 2> /dev/null || true
 	@rm tweetverif.tex 2> /dev/null || true
+	@rm tweetnacl.diff 2> /dev/null || true
 
 spell:
 	@for f in $(TEX) ; do \

paper/tweetnacl.diff

---- tweetnacl.c
-+++ tweetnaclVerifiableC.c
-@@ -6,5 +6,5 @@
- typedef unsigned long u32;
- typedef unsigned long long u64;
--typedef long long i64;
-+typedef long long i64 __attribute__((aligned(8)));
- typedef i64 gf[16];
- extern void randombytes(u8 *,u64);
-@@ -274,16 +274,14 @@
- {
-   int i;
--  i64 c;
-   FOR(i,16) {
--    o[i]+=(1LL<<16);
--    c=o[i]>>16;
--    o[(i+1)*(i<15)]+=c-1+37*(c-1)*(i==15);
--    o[i]-=c<<16;
-+    o[(i+1)%16]+=(i<15?1:38)*(o[i]>>16);
-+    o[i]&=0xffff;
-   }
- }
- 
--sv sel25519(gf p,gf q,int b)
-+sv sel25519(gf p,gf q,i64 b)
- {
--  i64 t,i,c=~(b-1);
-+  int i;
-+  i64 t,c=~(b-1);
-   FOR(i,16) {
-     t= c&(p[i]^q[i]);
-@@ -295,7 +293,8 @@
- sv pack25519(u8 *o,const gf n)
- {
--  int i,j,b;
--  gf m,t;
--  FOR(i,16) t[i]=n[i];
-+  int i,j;
-+  i64 b;
-+  gf t,m={0};
-+  set25519(t,n);
-   car25519(t);
-   car25519(t);
-@@ -310,5 +309,6 @@
-     b=(m[15]>>16)&1;
-     m[14]&=0xffff;
--    sel25519(t,m,1-b);
-+    b=1-b;
-+    sel25519(t,m,b);
-   }
-   FOR(i,16) {
-@@ -354,5 +354,6 @@
- sv M(gf o,const gf a,const gf b)
- {
--  i64 i,j,t[31];
-+  int i,j;
-+  i64 t[31];
-   FOR(i,31) t[i]=0;
-   FOR(i,16) FOR(j,16) t[i+j]+=a[i]*b[j];
-@@ -372,5 +373,5 @@
-   gf c;
-   int a;
--  FOR(a,16) c[a]=i[a];
-+  set25519(c,i);
-   for(a=253;a>=0;a--) {
-     S(c,c);
-@@ -395,6 +396,7 @@
- {
-   u8 z[32];
--  i64 x[80],r,i;
--  gf a,b,c,d,e,f;
-+  i64 r;
-+  int i;
-+  gf x,a,b,c,d,e,f;
-   FOR(i,31) z[i]=n[i];
-   z[31]=(n[31]&127)|64;
-@@ -431,13 +433,7 @@
-     sel25519(c,d,r);
-   }
--  FOR(i,16) {
--    x[i+16]=a[i];
--    x[i+32]=c[i];
--    x[i+48]=b[i];
--    x[i+64]=d[i];
--  }
--  inv25519(x+32,x+32);
--  M(x+16,x+16,x+32);
--  pack25519(q,x+16);
-+  inv25519(c,c);
-+  M(a,a,c);
-+  pack25519(q,a);
-   return 0;
- }