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
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
|
#!/usr/bin/env bash
#
# Use this script to update the HACL generated hash algorithm implementation
# code from a local checkout of the upstream hacl-star repository.
#
set -e
set -o pipefail
if [[ "${BASH_VERSINFO[0]}" -lt 4 ]]; then
echo "A bash version >= 4 required. Got: $BASH_VERSION" >&2
exit 1
fi
if [[ $1 == "" ]]; then
echo "Usage: $0 path-to-hacl-directory"
echo ""
echo " path-to-hacl-directory should be a local git checkout of a"
echo " https://github.com/hacl-star/hacl-star/ repo."
exit 1
fi
# Update this when updating to a new version after verifying that the changes
# the update brings in are good.
expected_hacl_star_rev=4ef25b547b377dcef855db4289c6a00580e7221c
hacl_dir="$(realpath "$1")"
cd "$(dirname "$0")"
actual_rev=$(cd "$hacl_dir" && git rev-parse HEAD)
if [[ "$actual_rev" != "$expected_hacl_star_rev" ]]; then
echo "WARNING: HACL* in '$hacl_dir' is at revision:" >&2
echo " $actual_rev" >&2
echo "but expected revision:" >&2
echo " $expected_hacl_star_rev" >&2
echo "Edit the expected rev if the changes pulled in are what you want."
fi
# Step 1: copy files
declare -a dist_files
dist_files=(
Hacl_Streaming_Types.h
internal/Hacl_Streaming_Types.h
# Cryptographic Hash Functions (headers)
Hacl_Hash_MD5.h
Hacl_Hash_SHA1.h
Hacl_Hash_SHA2.h
Hacl_Hash_SHA3.h
Hacl_Hash_Blake2b.h
Hacl_Hash_Blake2s.h
Hacl_Hash_Blake2b_Simd256.h
Hacl_Hash_Blake2s_Simd128.h
# Cryptographic Primitives (headers)
Hacl_HMAC.h
Hacl_Streaming_HMAC.h
# Cryptographic Hash Functions (internal headers)
internal/Hacl_Hash_MD5.h
internal/Hacl_Hash_SHA1.h
internal/Hacl_Hash_SHA2.h
internal/Hacl_Hash_SHA3.h
internal/Hacl_Hash_Blake2b.h
internal/Hacl_Hash_Blake2s.h
internal/Hacl_Hash_Blake2b_Simd256.h
internal/Hacl_Hash_Blake2s_Simd128.h
internal/Hacl_Impl_Blake2_Constants.h
# Cryptographic Primitives (internal headers)
internal/Hacl_HMAC.h
internal/Hacl_Streaming_HMAC.h
# Cryptographic Hash Functions (sources)
Hacl_Hash_MD5.c
Hacl_Hash_SHA1.c
Hacl_Hash_SHA2.c
Hacl_Hash_SHA3.c
Hacl_Hash_Blake2b.c
Hacl_Hash_Blake2s.c
Hacl_Hash_Blake2b_Simd256.c
Hacl_Hash_Blake2s_Simd128.c
# Cryptographic Primitives (sources)
Hacl_HMAC.c
Hacl_Streaming_HMAC.c
# Miscellaneous
libintvector.h
libintvector-shim.h
lib_memzero0.h
Lib_Memzero0.c
)
declare -a include_files
include_files=(
include/krml/lowstar_endianness.h
include/krml/internal/compat.h
include/krml/internal/target.h
include/krml/internal/types.h
)
declare -a lib_files
lib_files=(
krmllib/dist/minimal/FStar_UInt_8_16_32_64.h
krmllib/dist/minimal/fstar_uint128_struct_endianness.h
krmllib/dist/minimal/FStar_UInt128_Verified.h
)
# C files for the algorithms themselves: current directory
(cd "$hacl_dir/dist/gcc-compatible" && tar cf - "${dist_files[@]}") | tar xf -
# Support header files (e.g. endianness macros): stays in include/
(cd "$hacl_dir/dist/karamel" && tar cf - "${include_files[@]}") | tar xf -
# Special treatment: we don't bother with an extra directory and move krmllib
# files to the same include directory
for f in "${lib_files[@]}"; do
cp "$hacl_dir/dist/karamel/$f" include/krml/
done
# Step 2: some in-place modifications to keep things simple and minimal
# This is basic, but refreshes of the vendored HACL code are infrequent, so
# let's not over-engineer this.
if [[ $(uname) == "Darwin" ]]; then
# You're already running with homebrew or macports to satisfy the
# bash>=4 requirement, so requiring GNU sed is entirely reasonable.
sed=gsed
else
sed=sed
fi
readarray -t all_files < <(find . -name '*.h' -or -name '*.c')
# Adjust the include path to reflect the local directory structure
$sed -i 's!#include "FStar_UInt128_Verified.h"!#include "krml/FStar_UInt128_Verified.h"!g' include/krml/internal/types.h
$sed -i 's!#include "fstar_uint128_struct_endianness.h"!#include "krml/fstar_uint128_struct_endianness.h"!g' include/krml/internal/types.h
# use KRML_VERIFIED_UINT128
$sed -i -z 's!#define KRML_TYPES_H!#define KRML_TYPES_H\n#define KRML_VERIFIED_UINT128!g' include/krml/internal/types.h
# This contains static inline prototypes that are defined in
# FStar_UInt_8_16_32_64; they are by default repeated for safety of separate
# compilation, but this is not necessary.
$sed -i 's!#include.*Hacl_Krmllib.h"!!g' "${all_files[@]}"
# Use globally unique names for the Hacl_ C APIs to avoid linkage conflicts.
$sed -i -z 's!#include <string.h>!#include <string.h>\n#include "python_hacl_namespaces.h"!' \
Hacl_Hash_*.h \
Hacl_HMAC.h \
Hacl_Streaming_HMAC.h
$sed -i -z 's!#include <inttypes.h>!#include <inttypes.h>\n#include "python_hacl_namespaces.h"!' \
lib_memzero0.h
# Step 3: trim whitespace (for the linter)
find . -name '*.c' -or -name '*.h' | xargs $sed -i 's![[:space:]]\+$!!'
echo "Updated; verify all is okay using git diff and git status."
|
