Commit 67cb7145 authored by Benoit Viguier's avatar Benoit Viguier
Browse files

Hello World

parents
*.bck
bin
Debug
ipch
.idea
*.pdf
Doc
*.sublime-project
# Created by https://www.gitignore.io/api/latex,c++,coq,c,ocaml,sublimetext,vim,emacs
### LaTeX ###
*.acn
*.acr
*.alg
*.aux
*.bbl
*.bcf
*.blg
*.dvi
*.fdb_latexmk
*.fls
*.glg
*.glo
*.gls
*.idx
*.ilg
*.ind
*.ist
*.lof
*.log
*.lot
*.maf
*.mtc
*.mtc0
*.nav
*.nlo
*.out
*.pdfsync
*.ps
*.run.xml
*.snm
*.synctex.gz
*.toc
*.vrb
*.xdy
*.tdo
### C++ ###
# Compiled Object files
*.slo
*.lo
*.o
*.obj
# Precompiled Headers
*.gch
*.pch
# Compiled Dynamic libraries
*.so
*.dylib
*.dll
# Fortran module files
*.mod
# Compiled Static libraries
*.lai
*.la
*.a
*.lib
# Executables
*.exe
*.out
*.app
### Coq ###
*.vo
*.glob
*.v.d
*.vio
*.crashcoqide
### C ###
# Object files
*.o
*.ko
*.obj
*.elf
# Precompiled Headers
*.gch
*.pch
# Libraries
*.lib
*.a
*.la
*.lo
# Shared objects (inc. Windows DLLs)
*.dll
*.so
*.so.*
*.dylib
# Executables
*.exe
*.out
*.app
*.i*86
*.x86_64
*.hex
# Debug files
*.dSYM/
### OCaml ###
*.annot
*.cmo
*.cma
*.cmi
*.a
*.o
*.cmx
*.cmxs
*.cmxa
*.cmt
# ocamlbuild working directory
_build/
# ocamlbuild targets
*.byte
*.native
# oasis generated files
setup.data
setup.log
### SublimeText ###
# cache files for sublime text
*.tmlanguage.cache
*.tmPreferences.cache
*.stTheme.cache
# workspace files are user-specific
*.sublime-workspace
# project files should be checked into the repository, unless a significant
# proportion of contributors will probably not be using SublimeText
# *.sublime-project
# sftp configuration file
sftp-config.json
### Vim ###
[._]*.s[a-w][a-z]
[._]s[a-w][a-z]
*.un~
Session.vim
.netrwhist
*~
### Emacs ###
# -*- mode: gitignore; -*-
*~
\#*\#
/.emacs.desktop
/.emacs.desktop.lock
*.elc
auto-save-list
tramp
.\#*
# Org-mode
.org-id-locations
*_archive
# flymake-mode
*_flymake.*
# eshell files
/eshell/history
/eshell/lastdir
# elpa packages
/elpa/
# reftex files
*.rel
# AUCTeX auto folder
/auto/
# cask packages
.cask/
# server auth directory
/server/
# TweetNaCl verification
-------------------------------
## Setting up your environment (Debian 8.5)
##### 1. download & install GCC and OPAM and initialize it.
````bash
sudo apt-get install gcc
sudo apt-get install opam
opam init
opam switch 4.03.0
````
##### 2. install coq 8.5.2 + coqide + ssreflect
````bash
opam install coq.8.5.2
opam install coqide.8.5.2
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-mathcomp-ssreflect
opam install menhir
````
##### 3. Get VST from Princeton and Compcert
````bash
git clone git@github.com:PrincetonUniversity/VST.git
# go into VST folder and delete compcert folder: this version doesn't compile for some reasons
cd VST
rm -fr compcert
# while we are at it, replace it with a working version
wget http://compcert.inria.fr/release/compcert-2.7.1.tgz
tar zxvf compcert-2.7.1.tgz
rm compcert-2.7.1.tgz
# and rename the folder as initially expected
mv CompCert-2.7.1 compcert
# time to compile compcert
cd compcert
# -clightgen is required for the VST. Also verify you need this architecture...
./configure -clightgen ia32-linux
# I compile with 3 of my 4 cores, if you have 8 cores, you can try with -j 5
make -j 3
# install compcert so it is accessible through cli
sudo make install
# compcert is installed, we can install VST.
cd ..
# I compile with 3 of my 4 cores, if you have 8 cores, you can try with -j 5
make -j 3
````
##### 4. launch coqide from THIS folder (VST) so it uses `.loadpath`
````bash
coqide
# or if you use ProofGeneral
./pg
````
echo "
list of commands that you might want to know
git add -A : add all files
git add --all : add all files
git add -u : update modified files
git commit -m <msg> : commit some changes with <msg>
git commit -am <msg> : git add -u + git commit -m
git mv <source> <destination> : move a file/folder
git status : check local status
git fetch : check for changes online
git pull : check for changes online and update local
git push : push your commited changes online
REVERT CHANGES :
git checkout -- <file> : reset your file/folder to the last commit
git stash : reset your local repo to the last commit
git reset --hard : complete reset to the last commit
/!\ your changes will be destroyed
IN CASE OF CONFLICT :
git fetch --all
git reset --hard origin/master
/!\ your changes will be destroyed
TO MERGE IN CASE OF CONFLICT :
git fetch : parse the last modifications
git difftool : merge the files
Edit the files (chose the right parts), commit and push.
MORE ADVANCED STUFF :
git stash save <message> : save temporarly your changes and revert
git stash list : show the list of the previous \"stash\"
git stash clear : clear the previous list
git stash pop : return to your working state
BRANCHES
git checkout -b <branch name> : create a branch <branch name>
git checkout <branch name> : switch to branch <branch name>
git push -u --all
git checkout <commit number> : switch to this commit /!\ DANGEROUS
MERGE /!\ DANGEROUS
git merge <branch name> merges ROOT BRANCH (the one you are on, see git status) with <branch name>.
The changes are done on ROOT BRANCH.
alias gtree='git log --oneline --decorate --all --graph'
Add this to .git/config in order to have a nice output on ''git log''
[log]
date = short
[format]
pretty = format:%C(yellow)%h %>(10)%Cred%ad %<(13)%C(cyan)%an %Cgreen%d %Creset%s"
#include "tweetnacl.h"
#define FOR(i,n) for (i = 0;i < n;++i)
#define sv static void
typedef unsigned char u8;
typedef unsigned long u32;
typedef unsigned long long u64;
typedef long long i64;
typedef i64 gf[16];
extern void randombytes(u8 *,u64);
static const u8
_0[16],
_9[32] = {9};
static const gf
gf0,
gf1 = {1},
_121665 = {0xDB41,1},
D = {0x78a3, 0x1359, 0x4dca, 0x75eb, 0xd8ab, 0x4141, 0x0a4d, 0x0070, 0xe898, 0x7779, 0x4079, 0x8cc7, 0xfe73, 0x2b6f, 0x6cee, 0x5203},
D2 = {0xf159, 0x26b2, 0x9b94, 0xebd6, 0xb156, 0x8283, 0x149a, 0x00e0, 0xd130, 0xeef3, 0x80f2, 0x198e, 0xfce7, 0x56df, 0xd9dc, 0x2406},
X = {0xd51a, 0x8f25, 0x2d60, 0xc956, 0xa7b2, 0x9525, 0xc760, 0x692c, 0xdc5c, 0xfdd6, 0xe231, 0xc0a4, 0x53fe, 0xcd6e, 0x36d3, 0x2169},
Y = {0x6658, 0x6666, 0x6666, 0x6666, 0x6666, 0x6666, 0x6666, 0x6666, 0x6666, 0x6666, 0x6666, 0x6666, 0x6666, 0x6666, 0x6666, 0x6666},
I = {0xa0b0, 0x4a0e, 0x1b27, 0xc4ee, 0xe478, 0xad2f, 0x1806, 0x2f43, 0xd7a7, 0x3dfb, 0x0099, 0x2b4d, 0xdf0b, 0x4fc1, 0x2480, 0x2b83};
static u32 L32(u32 x,int c) { return (x << c) | ((x&0xffffffff) >> (32 - c)); }
static u32 ld32(const u8 *x)
{
u32 u = x[3];
u = (u<<8)|x[2];
u = (u<<8)|x[1];
return (u<<8)|x[0];
}
static u64 dl64(const u8 *x)
{
u64 i,u=0;
FOR(i,8) u=(u<<8)|x[i];
return u;
}
sv st32(u8 *x,u32 u)
{
int i;
FOR(i,4) { x[i] = u; u >>= 8; }
}
sv ts64(u8 *x,u64 u)
{
int i;
for (i = 7;i >= 0;--i) { x[i] = u; u >>= 8; }
}
static int vn(const u8 *x,const u8 *y,int n)
{
u32 i,d = 0;
FOR(i,n) d |= x[i]^y[i];
return (1 & ((d - 1) >> 8)) - 1;
}
int crypto_verify_16(const u8 *x,const u8 *y)
{
return vn(x,y,16);
}
int crypto_verify_32(const u8 *x,const u8 *y)
{
return vn(x,y,32);
}
sv core(u8 *out,const u8 *in,const u8 *k,const u8 *c,int h)
{
u32 w[16],x[16],y[16],t[4];
int i,j,m;
FOR(i,4) {
x[5*i] = ld32(c+4*i);
x[1+i] = ld32(k+4*i);
x[6+i] = ld32(in+4*i);
x[11+i] = ld32(k+16+4*i);
}
FOR(i,16) y[i] = x[i];
FOR(i,20) {
FOR(j,4) {
FOR(m,4) t[m] = x[(5*j+4*m)%16];
t[1] ^= L32(t[0]+t[3], 7);
t[2] ^= L32(t[1]+t[0], 9);
t[3] ^= L32(t[2]+t[1],13);
t[0] ^= L32(t[3]+t[2],18);
FOR(m,4) w[4*j+(j+m)%4] = t[m];
}
FOR(m,16) x[m] = w[m];
}
if (h) {
FOR(i,16) x[i] += y[i];
FOR(i,4) {
x[5*i] -= ld32(c+4*i);
x[6+i] -= ld32(in+4*i);
}
FOR(i,4) {
st32(out+4*i,x[5*i]);
st32(out+16+4*i,x[6+i]);
}
} else
FOR(i,16) st32(out + 4 * i,x[i] + y[i]);
}
int crypto_core_salsa20(u8 *out,const u8 *in,const u8 *k,const u8 *c)
{
core(out,in,k,c,0);
return 0;
}
int crypto_core_hsalsa20(u8 *out,const u8 *in,const u8 *k,const u8 *c)
{
core(out,in,k,c,1);
return 0;
}
static const u8 sigma[16] = "expand 32-byte k";
int crypto_stream_salsa20_xor(u8 *c,const u8 *m,u64 b,const u8 *n,const u8 *k)
{
u8 z[16],x[64];
u32 u,i;
if (!b) return 0;
FOR(i,16) z[i] = 0;
FOR(i,8) z[i] = n[i];
while (b >= 64) {
crypto_core_salsa20(x,z,k,sigma);
FOR(i,64) c[i] = (m?m[i]:0) ^ x[i];
u = 1;
for (i = 8;i < 16;++i) {
u += (u32) z[i];
z[i] = u;
u >>= 8;
}
b -= 64;
c += 64;
if (m) m += 64;
}
if (b) {
crypto_core_salsa20(x,z,k,sigma);
FOR(i,b) c[i] = (m?m[i]:0) ^ x[i];
}
return 0;
}
int crypto_stream_salsa20(u8 *c,u64 d,const u8 *n,const u8 *k)
{
return crypto_stream_salsa20_xor(c,0,d,n,k);
}
int crypto_stream(u8 *c,u64 d,const u8 *n,const u8 *k)
{
u8 s[32];
crypto_core_hsalsa20(s,n,k,sigma);
return crypto_stream_salsa20(c,d,n+16,s);
}
int crypto_stream_xor(u8 *c,const u8 *m,u64 d,const u8 *n,const u8 *k)
{
u8 s[32];
crypto_core_hsalsa20(s,n,k,sigma);
return crypto_stream_salsa20_xor(c,m,d,n+16,s);
}
sv add1305(u32 *h,const u32 *c)
{
u32 j,u = 0;
FOR(j,17) {
u += h[j] + c[j];
h[j] = u & 255;
u >>= 8;
}
}
static const u32 minusp[17] = {
5, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 252
} ;
int crypto_onetimeauth(u8 *out,const u8 *m,u64 n,const u8 *k)
{
u32 s,i,j,u,x[17],r[17],h[17],c[17],g[17];
FOR(j,17) r[j]=h[j]=0;
FOR(j,16) r[j]=k[j];
r[3]&=15;
r[4]&=252;
r[7]&=15;
r[8]&=252;
r[11]&=15;
r[12]&=252;
r[15]&=15;
while (n > 0) {
FOR(j,17) c[j] = 0;
for (j = 0;(j < 16) && (j < n);++j) c[j] = m[j];
c[j] = 1;
m += j; n -= j;
add1305(h,c);
FOR(i,17) {
x[i] = 0;
FOR(j,17) x[i] += h[j] * ((j <= i) ? r[i - j] : 320 * r[i + 17 - j]);
}
FOR(i,17) h[i] = x[i];
u = 0;
FOR(j,16) {
u += h[j];
h[j] = u & 255;
u >>= 8;
}
u += h[16]; h[16] = u & 3;
u = 5 * (u >> 2);
FOR(j,16) {
u += h[j];
h[j] = u & 255;
u >>= 8;
}
u += h[16]; h[16] = u;
}
FOR(j,17) g[j] = h[j];
add1305(h,minusp);
s = -(h[16] >> 7);
FOR(j,17) h[j] ^= s & (g[j] ^ h[j]);
FOR(j,16) c[j] = k[j + 16];
c[16] = 0;
add1305(h,c);
FOR(j,16) out[j] = h[j];
return 0;
}
int crypto_onetimeauth_verify(const u8 *h,const u8 *m,u64 n,const u8 *k)
{
u8 x[16];
crypto_onetimeauth(x,m,n,k);
return crypto_verify_16(h,x);
}
int crypto_secretbox(u8 *c,const u8 *m,u64 d,const u8 *n,const u8 *k)
{
int i;
if (d < 32) return -1;
crypto_stream_xor(c,m,d,n,k);
crypto_onetimeauth(c + 16,c + 32,d - 32,c);
FOR(i,16) c[i] = 0;
return 0;
}
int crypto_secretbox_open(u8 *m,const u8 *c,u64 d,const u8 *n,const u8 *k)
{
int i;
u8 x[32];
if (d < 32) return -1;
crypto_stream(x,32,n,k);
if (crypto_onetimeauth_verify(c + 16,c + 32,d - 32,x) != 0) return -1;
crypto_stream_xor(m,c,d,n,k);
FOR(i,32) m[i] = 0;
return 0;
}
sv set25519(gf r, const gf a)
{
int i;
FOR(i,16) r[i]=a[i];
}
sv car25519(gf o)
{
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;
}
}
sv sel25519(gf p,gf q,int b)
{
i64 t,i,c=~(b-1);
FOR(i,16) {
t= c&(p[i]^q[i]);
p[i]^=t;
q[i]^=t;
}
}
sv pack25519(u8 *o,const gf n)
{
int i,j,b;
gf m,t;
FOR(i,16) t[i]=n[i];
car25519(t);
car25519(t);
car25519(t);
FOR(j,2) {
m[0]=t[0]-0xffed;
for(i=1;i<15;i++)