This repository has been archived by the owner on Mar 7, 2024. It is now read-only.
-
Notifications
You must be signed in to change notification settings - Fork 43
/
typecheck_examples.sh
executable file
·88 lines (85 loc) · 3.37 KB
/
typecheck_examples.sh
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
#!/usr/bin/env bash
set -e
function typecheck {
echo "Typechecking $1 ..."
if [ "$2" == "ec" ];
then
echo " extracting EC ..."
mkdir -p ../target/easycrypt
cargo hacspec -e ec --dir ../target/easycrypt/ $1
else
cargo hacspec $1
fi
if [ -z "$6" ];
then
mkdir -p ../target/fstar
fstar_dir=../target/fstar/
else
fstar_dir=../fstar/
fi
if [ "$3" == "fst" ];
then
echo " extracting F* ..."
cargo hacspec -e fst --dir $fstar_dir $1
fi
if [ "$4" == "json" ];
then
echo " extracting JSON ..."
mkdir -p ../target/json
cargo hacspec -e json --dir ../target/json/ $1
fi
if [ "$5" == "coq" ];
then
echo " extracting coq ..."
mkdir -p ../target/coq
cratename=$1
prefix="hacspec-"
outname=${cratename#"$prefix"}
# capitalize first letter - macOS safe version (bash <= 3.2)
outname=$(tr '[:lower:]' '[:upper:]' <<<"${outname:0:1}")${outname:1}
cargo hacspec -e v --dir ../target/coq/ -o ${outname} $1
fi
}
cwd=$(cd $(dirname $0); pwd -P)
cd $cwd/../
cargo clean
cargo build
cargo install --path language
cd $cwd
cargo clean
cargo build
# Examples:
typecheck hacspec-chacha20 ec fst json coq
typecheck hacspec-chacha20poly1305 no-ec fst json coq
typecheck hacspec-poly1305 ec fst json coq
typecheck hacspec-curve25519 ec fst json coq
typecheck hacspec-hkdf no-ec fst json no-coq
typecheck hacspec-hmac no-ec fst json coq
typecheck hacspec-sha256 no-ec fst json coq
typecheck hacspec-ntru-prime ec fst json no-coq
typecheck hacspec-p256 no-ec fst json coq
typecheck hacspec-riot-bootloader ec fst json no-coq
typecheck hacspec-riot-runqueue no-ec fst no-json no-coq
typecheck hacspec-sha3 no-ec fst json no-coq
typecheck hacspec-gimli ec fst json no-coq
typecheck hacspec-bls12-381 no-ec no-fst json coq
typecheck hacspec-ecdsa-p256-sha256 no-ec no-fst json coq
typecheck hacspec-aes no-ec fst json no-coq
typecheck hacspec-gf128 no-ec fst json coq
typecheck hacspec-aes128-gcm no-ec fst json no-coq
typecheck hacspec-bls12-381-hash no-ec no-fst json coq
typecheck hacspec-sha512 no-ec no-fst json coq
typecheck hacspec-ed25519 no-ec no-fst json coq
typecheck hacspec-linalg no-ec no-fst json coq
typecheck hacspec-ristretto no-ec no-fst json coq
typecheck hacspec-merlin no-ec fst json coq
typecheck hacspec-edwards25519 no-ec no-fst json coq
typecheck hacspec-edwards25519-hash no-ec no-fst json coq
typecheck hacspec-edwards25519-ecvrf no-ec no-fst json coq
typecheck hacspec-linalg no-ec no-fst json coq
typecheck hacspec-rsa-pkcs1 no-ec no-fst json coq
typecheck hacspec-rsa-fdh-vrf no-ec no-fst json coq
typecheck hacspec-bip-340 no-ec no-fst json coq
typecheck hacspec-sha1 ec fst json coq
# Protocols:
typecheck tls_cryptolib no-ec fst json coq