Skip to content

Commit 8f2d5ba

Browse files
aqjune-awsaqjune-aws
committed
Use native OCaml compiler to build & run proofs
This patch compiles proofs using native OCaml compiler, and updates `make proofs` to run the newly created `*.native` executable files. The new `tools/build-proof.sh` script builds a specific `.ml` proof file. It inlines all loads/needs in the `.ml` file using HOL Light's `inline_load.ml`. Then, it collects all specifications in the original `.ml` file using already existing `tools/collect-specs.sh`, and adds a print statement at the end of the file, to make its standard output pass the proof checker script. It also adds timer and prints the running time of the proof. Then it is compiled with `ocamlopt.byte`. Building all proofs can be done with `make build_proofs`. This uses a lot of memory, so compared to the previous version `-j` number given to `make` must be reduced. This also makes the prerequisite lists tidier using the '*.native' items. Each '.native' file is considered as depending on the '.o' file.
1 parent efa579c commit 8f2d5ba

File tree

7 files changed

+202
-156
lines changed

7 files changed

+202
-156
lines changed

‎.gitignore

+1
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
11
*.a
22
*.correct
3+
*.native
34
*.o
45
*.obj
56
.vscode

‎arm/Makefile

+59-93
Large diffs are not rendered by default.

‎codebuild/proofs.yml

+4-2
Original file line numberDiff line numberDiff line change
@@ -18,11 +18,13 @@ phases:
1818
- eval $(opam env)
1919
- echo $(ocamlc -version)
2020
- echo $(camlp5 -v)
21-
- make
21+
- HOLLIGHT_USE_MODULE=1 make
2222
build:
2323
commands:
24-
- CORE_COUNT=45
24+
- BUILD_CORE_COUNT=15
25+
- CORE_COUNT=64
2526
- cd ${CODEBUILD_SRC_DIR}/${S2N_BIGNUM_ARCH}
2627
- export HOLDIR=${CODEBUILD_SRC_DIR_hol_light}
28+
- make -j ${BUILD_CORE_COUNT} build_proofs
2729
- make -j ${CORE_COUNT} proofs
2830
- ../tools/collect-times.sh ${S2N_BIGNUM_ARCH}

‎tools/build-proof.sh

+70
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,70 @@
1+
#!/bin/bash
2+
if [ "$#" -ne 3 ]; then
3+
echo "../tools/build-proof.sh <.ml file path> <hol.sh> <output .native path>"
4+
echo "This script builds HOL Light proof using OCaml native compiler and puts the "
5+
echo "output binary at <output .native path>."
6+
exit 1
7+
fi
8+
9+
# Return the exit code if any statement fails
10+
set -e
11+
12+
s2n_bignum_arch=$(basename "$(pwd)")
13+
14+
cd ..
15+
16+
ml_path_noarch=$1
17+
ml_path=${s2n_bignum_arch}/${ml_path_noarch}
18+
hol_sh_cmd=$2
19+
output_path=${s2n_bignum_arch}/$3
20+
21+
export HOLLIGHT_DIR="$(dirname ${hol_sh_cmd})"
22+
if [ ! -f "${HOLLIGHT_DIR}/hol_lib.cmxa" ]; then
23+
echo "hol_lib.cmxa does not exist in HOLLIGHT_DIR('${HOLLIGHT_DIR}')."
24+
echo "Did you compile HOL Light with HOLLIGHT_USE_MODULE set to 1?"
25+
exit 1
26+
fi
27+
28+
29+
template_ml="$(mktemp).ml"
30+
echo "Generating a template .ml that loads the file...: ${template_ml}"
31+
32+
(echo 'let s2n_bignum_build_proof_start_time = Unix.time();;'; \
33+
echo "loadt \"${ml_path}\";;"; \
34+
echo "check_axioms ();;") >> ${template_ml}
35+
36+
spec_found=0
37+
for spec in $(./tools/collect-specs.sh ${s2n_bignum_arch} $(basename ${ml_path})) ; do
38+
echo "Printf.printf \"val ${spec} : thm = %s\n\" (string_of_thm ${spec});;"
39+
spec_found=1
40+
done >> ${template_ml}
41+
42+
if [ $spec_found -eq 0 ]; then
43+
echo "Could not find any specification from ${ml_path}."
44+
exit 1
45+
fi
46+
47+
(echo 'let s2n_bignum_build_proof_end_time = Unix.time();;'; \
48+
echo 'Printf.printf "Running time: %f sec, Start unixtime: %f, End unixtime: %f\n" (s2n_bignum_build_proof_end_time -. s2n_bignum_build_proof_start_time) s2n_bignum_build_proof_start_time s2n_bignum_build_proof_end_time;;') >> ${template_ml}
49+
50+
51+
if [ -d "${HOLLIGHT_DIR}/_opam" ]; then
52+
# To use inline_load.ml ... If OCaml version is too old, otherwise, a few String functions fail.
53+
eval $(opam env --switch "${HOLLIGHT_DIR}/" --set-switch)
54+
fi
55+
56+
inlined_prefix="$(mktemp)"
57+
inlined_ml="${inlined_prefix}.ml"
58+
inlined_cmx="${inlined_prefix}.cmx"
59+
ocaml ${HOLLIGHT_DIR}/inline_load.ml ${template_ml} ${inlined_ml}
60+
61+
# Give a large stack size.
62+
OCAMLRUNPARAM=l=2000000000 \
63+
ocamlopt.byte -pp "$(${hol_sh_cmd} -pp)" -I "${HOLLIGHT_DIR}" -I +unix -c \
64+
hol_lib.cmxa ${inlined_ml} -o ${inlined_cmx} -w -a
65+
ocamlfind ocamlopt -package zarith,unix -linkpkg hol_lib.cmxa \
66+
-I "${HOLLIGHT_DIR}" ${inlined_cmx} \
67+
-o "${output_path}"
68+
69+
# Remove the intermediate files to save disk space
70+
rm ${inlined_cmx} ${template_ml} ${inlined_ml}

‎tools/collect-specs.sh

+8-3
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,19 @@
11
#!/bin/bash
2-
if [ "$#" -ne 1 ]; then
3-
echo "collect-specs.sh <dir (e.g., arm)>"
2+
if [ "$#" -ne 1 ] && [ "$#" -ne 2 ]; then
3+
echo "collect-specs.sh <dir (e.g., arm)> <.ml file (optional)>"
44
echo "This script collects the names of HOL Light theorems that are"
55
echo "specifications of correctness of assembly functions."
66
exit 1
77
fi
88

99
s2n_bignum_arch=$1
10+
if [ "$#" -eq 2 ]; then
11+
filepat="$2"
12+
else
13+
filepat="*.ml"
14+
fi
1015
cd $s2n_bignum_arch
1116

1217
# An env. var for sorting
1318
export LC_ALL=C
14-
grep 'let [A-Z_0-9]*_SUBROUTINE_CORRECT' proofs/*.ml | cut -f2 -d' ' | sort
19+
grep 'let [A-Z_0-9]*_SUBROUTINE_CORRECT' proofs/${filepat} | cut -f2 -d' ' | sort

‎tools/run-proof.sh

+11-18
Original file line numberDiff line numberDiff line change
@@ -1,36 +1,29 @@
11
#!/bin/bash
2-
if [ "$#" -ne 4 ]; then
3-
echo "../tools/run-proof.sh <dir (arm/x86)>"
4-
echo " <asm filename without .S (e.g., bignum_copy)>"
5-
echo " <HOL Light command> <output log path>"
6-
echo "This script runs HOL Light proof at '<dir>/proofs/<asm filename>.ml', and".
7-
echo "inspects the log file to check whether all proofs are done successfully."
2+
if [ "$#" -ne 2 ]; then
3+
echo "../tools/run-proof.sh <.native file to run> <output log path>"
4+
echo "This script runs precompiled HOL Light proof '<.native file>', prints the output"
5+
echo "at <output log path>, and inspects the log file to check whether all proofs "
6+
echo "are done successfully."
87
exit 1
98
fi
109

1110
# Return the exit code if any statement fails
1211
set -e
1312

13+
s2n_bignum_arch=$(basename "$(pwd)")
14+
1415
cd ..
1516

16-
s2n_bignum_arch=$1
17-
asm_filename=$2
18-
hol_light_cmd=$3
19-
output_path=${s2n_bignum_arch}/$4
17+
native_path=${s2n_bignum_arch}/$1
18+
output_path=${s2n_bignum_arch}/$2
2019

21-
(echo 'Topdirs.dir_directory "+unix";;'; \
22-
echo 'Topdirs.dir_load Format.std_formatter "unix.cma";;'; \
23-
echo 'let start_time = Unix.time();;'; \
24-
echo "loadt \"${s2n_bignum_arch}/proofs/${asm_filename}.ml\";;"; \
25-
echo "check_axioms ();;"; \
26-
echo 'let end_time = Unix.time();;'; \
27-
echo 'Printf.printf "Running time: %f sec, Start unixtime: %f, End unixtime: %f\n" (end_time -. start_time) start_time end_time;;') | eval "$hol_light_cmd" 2>&1 > "$output_path"
20+
"$native_path" 2>&1 > "$output_path"
2821

2922
# Revert the exit code option since 'grep' may return non-zero.
3023
set +e
3124

3225
grep -r -i "error\|exception" --include "$output_path"
3326
if [ $? -eq 0 ]; then
34-
echo "${s2n_bignum_arch}/proofs/${asm_filename}.ml had error(s)"
27+
echo "${s2n_bignum_arch}/${native_path} had error(s)"
3528
exit 1
3629
fi

‎x86/Makefile

+49-40
Original file line numberDiff line numberDiff line change
@@ -407,7 +407,7 @@ libs2nbignum.a: $(OBJ) ; ar -rc libs2nbignum.a $(OBJ)
407407

408408
winobj: $(WINOBJ) ;
409409

410-
clean:; rm -f libs2nbignum.a */*.o */*.obj */*.correct
410+
clean:; rm -f libs2nbignum.a */*.o */*.obj */*.correct */*.native
411411

412412
# Dynamically regenerate or destroy the files recording which functions
413413
# use BMI and/or ADX instructions in the x86 versions. These won't run
@@ -444,48 +444,57 @@ clobber: clean ; rm -f yesbmi_functions nonbmi_functions
444444
HOLDIR?=$(HOME)/hol-light
445445
HOLLIGHT:=$(HOLDIR)/hol.sh
446446

447-
PROOFS = $(OBJ:.o=.correct)
447+
PROOF_BINS = $(OBJ:.o=.native)
448+
PROOF_LOGS = $(OBJ:.o=.correct)
449+
450+
# Build precompiled native binaries of HOL Light proofs
451+
452+
.SECONDEXPANSION:
453+
%.native: proofs/$$(*F).ml %.o %.obj ; ../tools/build-proof.sh "$<" "$(HOLLIGHT)" "$@"
454+
455+
# Run them and print the standard output+error at *.correct
456+
457+
%.correct: %.native ; ../tools/run-proof.sh "$<" "$@"
448458

449459
# Cases where a proof uses other proofs for lemmas and/or subroutines
450460

451-
curve25519/curve25519_x25519.correct: curve25519/bignum_inv_p25519.o curve25519/bignum_inv_p25519.obj proofs/curve25519_x25519.ml curve25519/curve25519_x25519.o curve25519/curve25519_x25519.obj ; ../tools/run-proof.sh x86 curve25519_x25519 "$(HOLLIGHT)" $@
452-
curve25519/curve25519_x25519_alt.correct: curve25519/bignum_inv_p25519.o curve25519/bignum_inv_p25519.obj proofs/curve25519_x25519_alt.ml curve25519/curve25519_x25519_alt.o curve25519/curve25519_x25519_alt.obj ; ../tools/run-proof.sh x86 curve25519_x25519_alt "$(HOLLIGHT)" $@
453-
curve25519/curve25519_x25519_byte.correct: curve25519/bignum_inv_p25519.o curve25519/bignum_inv_p25519.obj proofs/curve25519_x25519_byte.ml curve25519/curve25519_x25519_byte.o curve25519/curve25519_x25519_byte.obj ; ../tools/run-proof.sh x86 curve25519_x25519_byte "$(HOLLIGHT)" $@
454-
curve25519/curve25519_x25519_byte_alt.correct: curve25519/bignum_inv_p25519.o curve25519/bignum_inv_p25519.obj proofs/curve25519_x25519_byte_alt.ml curve25519/curve25519_x25519_byte_alt.o curve25519/curve25519_x25519_byte_alt.obj ; ../tools/run-proof.sh x86 curve25519_x25519_byte_alt "$(HOLLIGHT)" $@
455-
curve25519/curve25519_x25519base.correct: curve25519/bignum_inv_p25519.o curve25519/bignum_inv_p25519.obj proofs/curve25519_x25519base.ml curve25519/curve25519_x25519base.o curve25519/curve25519_x25519base.obj ; ../tools/run-proof.sh x86 curve25519_x25519base "$(HOLLIGHT)" $@
456-
curve25519/curve25519_x25519base_alt.correct: curve25519/bignum_inv_p25519.o curve25519/bignum_inv_p25519.obj proofs/curve25519_x25519base_alt.ml curve25519/curve25519_x25519base_alt.o curve25519/curve25519_x25519base_alt.obj ; ../tools/run-proof.sh x86 curve25519_x25519base_alt "$(HOLLIGHT)" $@
457-
curve25519/curve25519_x25519base_byte.correct: curve25519/bignum_inv_p25519.o curve25519/bignum_inv_p25519.obj proofs/curve25519_x25519base_byte.ml curve25519/curve25519_x25519base_byte.o curve25519/curve25519_x25519base_byte.obj ; ../tools/run-proof.sh x86 curve25519_x25519base_byte "$(HOLLIGHT)" $@
458-
curve25519/curve25519_x25519base_byte_alt.correct: curve25519/bignum_inv_p25519.o curve25519/bignum_inv_p25519.obj proofs/curve25519_x25519base_byte_alt.ml curve25519/curve25519_x25519base_byte_alt.o curve25519/curve25519_x25519base_byte_alt.obj ; ../tools/run-proof.sh x86 curve25519_x25519base_byte_alt "$(HOLLIGHT)" $@
459-
curve25519/edwards25519_scalarmulbase.correct: curve25519/bignum_inv_p25519.o curve25519/bignum_inv_p25519.obj proofs/edwards25519_scalarmulbase.ml curve25519/edwards25519_scalarmulbase.o curve25519/edwards25519_scalarmulbase.obj ; ../tools/run-proof.sh x86 edwards25519_scalarmulbase "$(HOLLIGHT)" $@
460-
curve25519/edwards25519_scalarmulbase_alt.correct: curve25519/bignum_inv_p25519.o curve25519/bignum_inv_p25519.obj proofs/edwards25519_scalarmulbase_alt.ml curve25519/edwards25519_scalarmulbase_alt.o curve25519/edwards25519_scalarmulbase_alt.obj ; ../tools/run-proof.sh x86 edwards25519_scalarmulbase_alt "$(HOLLIGHT)" $@
461-
curve25519/edwards25519_scalarmuldouble.correct: curve25519/bignum_inv_p25519.o curve25519/bignum_inv_p25519.obj proofs/edwards25519_scalarmuldouble.ml curve25519/edwards25519_scalarmuldouble.o curve25519/edwards25519_scalarmuldouble.obj ; ../tools/run-proof.sh x86 edwards25519_scalarmuldouble "$(HOLLIGHT)" $@
462-
curve25519/edwards25519_scalarmuldouble_alt.correct: curve25519/bignum_inv_p25519.o curve25519/bignum_inv_p25519.obj proofs/edwards25519_scalarmuldouble_alt.ml curve25519/edwards25519_scalarmuldouble_alt.o curve25519/edwards25519_scalarmuldouble_alt.obj ; ../tools/run-proof.sh x86 edwards25519_scalarmuldouble_alt "$(HOLLIGHT)" $@
463-
generic/bignum_modexp.correct: generic/bignum_amontifier.correct generic/bignum_amontmul.correct generic/bignum_demont.correct generic/bignum_mux.correct proofs/bignum_modexp.ml generic/bignum_modexp.o generic/bignum_modexp.obj ; ../tools/run-proof.sh x86 bignum_modexp "$(HOLLIGHT)" $@
464-
p256/p256_montjscalarmul.correct: proofs/p256_montjadd.ml p256/p256_montjadd.o p256/p256_montjadd.obj proofs/p256_montjdouble.ml p256/p256_montjdouble.o p256/p256_montjdouble.obj proofs/p256_montjscalarmul.ml p256/p256_montjscalarmul.o p256/p256_montjscalarmul.obj ; ../tools/run-proof.sh x86 p256_montjscalarmul "$(HOLLIGHT)" $@
465-
p256/p256_montjscalarmul_alt.correct: proofs/p256_montjadd_alt.ml p256/p256_montjadd_alt.o p256/p256_montjadd_alt.obj proofs/p256_montjdouble_alt.ml p256/p256_montjdouble_alt.o p256/p256_montjdouble_alt.obj proofs/p256_montjscalarmul_alt.ml p256/p256_montjscalarmul_alt.o p256/p256_montjscalarmul_alt.obj ; ../tools/run-proof.sh x86 p256_montjscalarmul_alt "$(HOLLIGHT)" $@
466-
p256/p256_scalarmul.correct: proofs/bignum_demont_p256.ml p256/bignum_demont_p256.o p256/bignum_demont_p256.obj proofs/bignum_inv_p256.ml p256/bignum_inv_p256.o p256/bignum_inv_p256.obj proofs/bignum_montmul_p256.ml p256/bignum_montmul_p256.o p256/bignum_montmul_p256.obj proofs/bignum_montsqr_p256.ml p256/bignum_montsqr_p256.o p256/bignum_montsqr_p256.obj proofs/bignum_tomont_p256.ml p256/bignum_tomont_p256.o p256/bignum_tomont_p256.obj proofs/p256_montjadd.ml p256/p256_montjadd.o p256/p256_montjadd.obj proofs/p256_montjdouble.ml p256/p256_montjdouble.o p256/p256_montjdouble.obj proofs/p256_montjmixadd.ml p256/p256_montjmixadd.o p256/p256_montjmixadd.obj proofs/p256_scalarmul.ml p256/p256_scalarmul.o p256/p256_scalarmul.obj ; ../tools/run-proof.sh x86 p256_scalarmul "$(HOLLIGHT)" $@
467-
p256/p256_scalarmul_alt.correct: proofs/bignum_demont_p256_alt.ml p256/bignum_demont_p256_alt.o p256/bignum_demont_p256_alt.obj proofs/bignum_inv_p256.ml p256/bignum_inv_p256.o p256/bignum_inv_p256.obj proofs/bignum_montmul_p256_alt.ml p256/bignum_montmul_p256_alt.o p256/bignum_montmul_p256_alt.obj proofs/bignum_montsqr_p256_alt.ml p256/bignum_montsqr_p256_alt.o p256/bignum_montsqr_p256_alt.obj proofs/bignum_tomont_p256_alt.ml p256/bignum_tomont_p256_alt.o p256/bignum_tomont_p256_alt.obj proofs/p256_montjadd_alt.ml p256/p256_montjadd_alt.o p256/p256_montjadd_alt.obj proofs/p256_montjdouble_alt.ml p256/p256_montjdouble_alt.o p256/p256_montjdouble_alt.obj proofs/p256_montjmixadd_alt.ml p256/p256_montjmixadd_alt.o p256/p256_montjmixadd_alt.obj proofs/p256_scalarmul_alt.ml p256/p256_scalarmul_alt.o p256/p256_scalarmul_alt.obj ; ../tools/run-proof.sh x86 p256_scalarmul_alt "$(HOLLIGHT)" $@
468-
p256/p256_scalarmulbase.correct: proofs/bignum_demont_p256.ml p256/bignum_demont_p256.o p256/bignum_demont_p256.obj proofs/bignum_inv_p256.ml p256/bignum_inv_p256.o p256/bignum_inv_p256.obj proofs/bignum_montmul_p256.ml p256/bignum_montmul_p256.o p256/bignum_montmul_p256.obj proofs/bignum_montsqr_p256.ml p256/bignum_montsqr_p256.o p256/bignum_montsqr_p256.obj proofs/p256_montjmixadd.ml p256/p256_montjmixadd.o p256/p256_montjmixadd.obj proofs/p256_scalarmulbase.ml p256/p256_scalarmulbase.o p256/p256_scalarmulbase.obj ; ../tools/run-proof.sh x86 p256_scalarmulbase "$(HOLLIGHT)" $@
469-
p256/p256_scalarmulbase_alt.correct: proofs/bignum_demont_p256_alt.ml p256/bignum_demont_p256_alt.o p256/bignum_demont_p256_alt.obj proofs/bignum_inv_p256.ml p256/bignum_inv_p256.o p256/bignum_inv_p256.obj proofs/bignum_montmul_p256_alt.ml p256/bignum_montmul_p256_alt.o p256/bignum_montmul_p256_alt.obj proofs/bignum_montsqr_p256_alt.ml p256/bignum_montsqr_p256_alt.o p256/bignum_montsqr_p256_alt.obj proofs/p256_montjmixadd_alt.ml p256/p256_montjmixadd_alt.o p256/p256_montjmixadd_alt.obj proofs/p256_scalarmulbase_alt.ml p256/p256_scalarmulbase_alt.o p256/p256_scalarmulbase_alt.obj ; ../tools/run-proof.sh x86 p256_scalarmulbase_alt "$(HOLLIGHT)" $@
470-
p384/p384_montjscalarmul.correct: proofs/p384_montjadd.ml p384/p384_montjadd.o p384/p384_montjadd.obj proofs/p384_montjdouble.ml p384/p384_montjdouble.o p384/p384_montjdouble.obj proofs/p384_montjscalarmul.ml p384/p384_montjscalarmul.o p384/p384_montjscalarmul.obj ; ../tools/run-proof.sh x86 p384_montjscalarmul "$(HOLLIGHT)" $@
471-
p384/p384_montjscalarmul_alt.correct: proofs/p384_montjadd_alt.ml p384/p384_montjadd_alt.o p384/p384_montjadd_alt.obj proofs/p384_montjdouble_alt.ml p384/p384_montjdouble_alt.o p384/p384_montjdouble_alt.obj proofs/p384_montjscalarmul_alt.ml p384/p384_montjscalarmul_alt.o p384/p384_montjscalarmul_alt.obj ; ../tools/run-proof.sh x86 p384_montjscalarmul_alt "$(HOLLIGHT)" $@
472-
p521/p521_jscalarmul.correct: proofs/bignum_mod_n521_9.ml p521/bignum_mod_n521_9.o p521/bignum_mod_n521_9.obj proofs/bignum_mod_p521_9.ml p521/bignum_mod_p521_9.o p521/bignum_mod_p521_9.obj proofs/p521_jscalarmul.ml p521/p521_jscalarmul.o p521/p521_jscalarmul.obj ; ../tools/run-proof.sh x86 p521_jscalarmul "$(HOLLIGHT)" $@
473-
p521/p521_jscalarmul_alt.correct: proofs/bignum_mod_n521_9_alt.ml p521/bignum_mod_n521_9_alt.o p521/bignum_mod_n521_9_alt.obj proofs/bignum_mod_p521_9.ml p521/bignum_mod_p521_9.o p521/bignum_mod_p521_9.obj proofs/p521_jscalarmul_alt.ml p521/p521_jscalarmul_alt.o p521/p521_jscalarmul_alt.obj ; ../tools/run-proof.sh x86 p521_jscalarmul_alt "$(HOLLIGHT)" $@
474-
sm2/sm2_montjscalarmul.correct: proofs/sm2_montjadd.ml sm2/sm2_montjadd.o sm2/sm2_montjadd.obj proofs/sm2_montjdouble.ml sm2/sm2_montjdouble.o sm2/sm2_montjdouble.obj proofs/sm2_montjscalarmul.ml sm2/sm2_montjscalarmul.o sm2/sm2_montjscalarmul.obj ; ../tools/run-proof.sh x86 sm2_montjscalarmul "$(HOLLIGHT)" $@
475-
sm2/sm2_montjscalarmul_alt.correct: proofs/sm2_montjadd_alt.ml sm2/sm2_montjadd_alt.o sm2/sm2_montjadd_alt.obj proofs/sm2_montjdouble_alt.ml sm2/sm2_montjdouble_alt.o sm2/sm2_montjdouble_alt.obj proofs/sm2_montjscalarmul_alt.ml sm2/sm2_montjscalarmul_alt.o sm2/sm2_montjscalarmul_alt.obj ; ../tools/run-proof.sh x86 sm2_montjscalarmul_alt "$(HOLLIGHT)" $@
476-
477-
# All other other instances are standalone
478-
479-
curve25519/%.correct: proofs/%.ml curve25519/%.o curve25519/%.obj ; ../tools/run-proof.sh x86 "$*" "$(HOLLIGHT)" $@
480-
fastmul/%.correct: proofs/%.ml fastmul/%.o fastmul/%.obj ; ../tools/run-proof.sh x86 "$*" "$(HOLLIGHT)" $@
481-
generic/%.correct: proofs/%.ml generic/%.o generic/%.obj ; ../tools/run-proof.sh x86 "$*" "$(HOLLIGHT)" $@
482-
p256/%.correct: proofs/%.ml p256/%.o p256/%.obj ; ../tools/run-proof.sh x86 "$*" "$(HOLLIGHT)" $@
483-
p384/%.correct: proofs/%.ml p384/%.o p384/%.obj ; ../tools/run-proof.sh x86 "$*" "$(HOLLIGHT)" $@
484-
p521/%.correct: proofs/%.ml p521/%.o p521/%.obj ; ../tools/run-proof.sh x86 "$*" "$(HOLLIGHT)" $@
485-
secp256k1/%.correct: proofs/%.ml secp256k1/%.o secp256k1/%.obj ; ../tools/run-proof.sh x86 "$*" "$(HOLLIGHT)" $@
486-
sm2/%.correct: proofs/%.ml sm2/%.o sm2/%.obj ; ../tools/run-proof.sh x86 "$*" "$(HOLLIGHT)" $@
487-
488-
run_proofs: $(PROOFS);
461+
curve25519/curve25519_x25519.native: curve25519/bignum_inv_p25519.native
462+
curve25519/curve25519_x25519_alt.native: curve25519/bignum_inv_p25519.native
463+
curve25519/curve25519_x25519_byte.native: curve25519/bignum_inv_p25519.native
464+
curve25519/curve25519_x25519_byte_alt.native: curve25519/bignum_inv_p25519.native
465+
curve25519/curve25519_x25519base.native: curve25519/bignum_inv_p25519.native
466+
curve25519/curve25519_x25519base_alt.native: curve25519/bignum_inv_p25519.native
467+
curve25519/curve25519_x25519base_byte.native: curve25519/bignum_inv_p25519.native
468+
curve25519/curve25519_x25519base_byte_alt.native: curve25519/bignum_inv_p25519.native
469+
curve25519/edwards25519_scalarmulbase.native: curve25519/bignum_inv_p25519.native
470+
curve25519/edwards25519_scalarmulbase_alt.native: curve25519/bignum_inv_p25519.native
471+
curve25519/edwards25519_scalarmuldouble.native: curve25519/bignum_inv_p25519.native
472+
curve25519/edwards25519_scalarmuldouble_alt.native: curve25519/bignum_inv_p25519.native
473+
generic/bignum_modexp.native: generic/bignum_amontifier.native generic/bignum_amontmul.native generic/bignum_demont.native generic/bignum_mux.native
474+
p256/p256_montjadd.native: p256/bignum_montsqr_p256.native p256/bignum_montmul_p256.native p256/bignum_sub_p256.native
475+
p256/p256_montjdouble.native: p256/bignum_montsqr_p256.native p256/bignum_montmul_p256.native p256/bignum_sub_p256.native p256/bignum_add_p256.native
476+
p256/p256_montjscalarmul.native: p256/p256_montjadd.native p256/p256_montjdouble.native
477+
p256/p256_montjscalarmul_alt.native: p256/p256_montjadd_alt.native p256/p256_montjdouble_alt.native
478+
p256/p256_scalarmul.native: p256/bignum_demont_p256.native p256/bignum_inv_p256.native p256/bignum_tomont_p256.native p256/p256_montjadd.native p256/p256_montjdouble.native p256/p256_montjmixadd.native
479+
p256/p256_scalarmul_alt.native: p256/bignum_demont_p256.native p256/bignum_inv_p256.native p256/p256_montjadd_alt.native p256/p256_montjdouble_alt.native p256/p256_montjmixadd_alt.native
480+
p256/p256_scalarmulbase.native: p256/bignum_demont_p256.native p256/bignum_inv_p256.native p256/p256_montjmixadd.native
481+
p256/p256_scalarmulbase_alt.native: p256/bignum_demont_p256.native p256/bignum_inv_p256.native p256/p256_montjmixadd_alt.native
482+
p384/p384_montjadd.native: p384/bignum_montsqr_p384.native p384/bignum_montmul_p384.native p384/bignum_sub_p384.native
483+
p384/p384_montjdouble.native: p384/bignum_montsqr_p384.native p384/bignum_montmul_p384.native p384/bignum_sub_p384.native p384/bignum_add_p384.native
484+
p384/p384_montjscalarmul.native: \
485+
p384/p384_montjadd.native p384/p384_montjdouble.native \
486+
p384/bignum_sub_p384.native p384/bignum_add_p384.native
487+
p384/p384_montjscalarmul_alt.native: p384/p384_montjadd_alt.native p384/p384_montjdouble_alt.native
488+
p521/p521_jadd.native: p521/bignum_mul_p521.native p521/bignum_sqr_p521.native
489+
p521/p521_jdouble.native: p521/bignum_mul_p521.native p521/bignum_sqr_p521.native
490+
p521/p521_jscalarmul.native: p521/bignum_mod_n521_9.native p521/p521_jadd.native p521/p521_jdouble.native
491+
p521/p521_jscalarmul_alt.native: p521/bignum_mod_n521_9.native
492+
sm2/sm2_montjscalarmul.native: sm2/sm2_montjadd.native sm2/sm2_montjdouble.native
493+
sm2/sm2_montjscalarmul_alt.native: sm2/sm2_montjadd_alt.native sm2/sm2_montjdouble_alt.native
494+
495+
496+
build_proofs: $(PROOF_BINS);
497+
run_proofs: build_proofs $(PROOF_LOGS);
489498

490499
proofs: run_proofs ; ../tools/count-proofs.sh .
491500

0 commit comments

Comments
 (0)