-
Notifications
You must be signed in to change notification settings - Fork 1
/
doc_cryptoasm.sh
130 lines (101 loc) · 3.39 KB
/
doc_cryptoasm.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
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
source ./doc_functions.sh
cryptoasm_cond () {
local i=$1
if [[ "$i" == *_prg.v ]] || [[ "$i" == *_termination.v ]] ||
[[ "$i" == *_triple.v ]] || [[ "$i" == *bbs* ]] ||
[[ "$i" == *goto* ]] || [[ "$i" == *compile* ]]; then
return 0
else
return 1
fi
}
print_function () {
echo "<li>"$2
echo "<ul>"
echo "<li>"
echo "<ul class=\"prg\">"
for i in *.v; do
if [[ "$i" == *"$3"*prg* ]]; then
echo "<li>"
print_filename $dir $i
echo "</li>"
fi
done
echo "</ul>"
echo "</li>"
echo "<li>"
echo "<ul class=\"triple\">"
for i in *.v; do
if [[ "$i" == *"$3"*triple* ]]; then
echo "<li>"
print_filename $dir $i
echo "</li>"
fi
done
echo "</ul>"
echo "</li>"
echo "<li>"
echo "<ul class=\"misc\">"
for i in *.v; do
if [[ "$i" == *"$3"* ]] && [[ "$i" != *"$3"*prg* ]] && [[ "$i" != *"$3"*triple* ]]; then
echo "<li>"
print_filename $dir $i
echo "</li>"
fi
done
echo "</ul>"
echo "</li>"
echo "</ul>"
echo "</li>"
}
echo "<title>TITLE</title>"
echo "</head>"
echo "<body>"
dir="cryptoasm"
cd $dir
echo "<dt class=\"dt_main\"><span class=\"bfont\">"$dir/"</span>: "
cat README.doc
echo "</dt>"
echo "<p class=\"sublib\">Separation logic for SmartMIPS:</p>"
for i in *.v; do
cryptoasm_cond $i
if [ $? -eq 1 ]; then
print_filename $dir $i
fi
done
echo "<p class=\"sublib\">Illustrative example of SGoto:</p>"
for i in *.v; do
if [[ "$i" == *goto* ]] || [[ "$i" == *compile* ]] ; then
print_filename $dir $i
fi
done
echo "<p class=\"sublib\">Formal verifications of cryptographic functions: <span class=\"prg\">program</span> <span class=\"triple\">functional correctness</span> <span class=\"misc\">other properties</span></p>"
echo "<div id=\"functions\">"
echo "<ul class=\"crypto_list\">"
echo "<div id=\"kamoku\">Multi-precision unsigned arithmetic</div>"
print_function $dir 'Initialization to 0 →' 'multi_zero_u'
print_function $dir 'Initialization to 1 →' 'multi_one_u'
print_function $dir 'Parity check →' 'multi_is_even_u'
print_function $dir 'Zero testing →' 'multi_is_zero_u'
print_function $dir 'Array copy →' 'copy_u_u'
print_function $dir 'Additions →' 'multi_add_u_u'
print_function $dir 'Subtractions →' 'multi_sub_u_u'
print_function $dir 'Multiplication →' 'multi_mul_u_u'
print_function $dir 'Halving →' 'multi_halve_u'
print_function $dir 'Doubling →' 'multi_double_u'
print_function $dir 'Comparison (<, >, =) →' 'multi_lt'
print_function $dir 'Montgomery multiplication →' 'mont_mul'
print_function $dir 'Montgomery squaring →' 'mont_square'
print_function $dir 'Montgomery exponentiation →' 'mont_exp'
print_function $dir 'BBS pseudorandom bit generator →' 'bbs'
echo "<div id=\"kamoku\">Multi-precision signed arithmetic</div>"
print_function $dir 'Initialization to 0 →' 'multi_zero_s'
print_function $dir 'Initialization to 1 →' 'multi_one_s'
print_function $dir 'Negation →' 'multi_negate'
print_function $dir 'Sign testing →' 'pick_sign'
print_function $dir 'Array copy →' 'copy_s_'
print_function $dir 'Signed addition →' 'multi_add_s_'
print_function $dir 'Signed subtractions →' 'multi_sub_s'
print_function $dir 'Signed halving →' 'multi_halve_s'
echo "</ul>"
echo "</div>"