Skip to content

Commit 71f93e0

Browse files
dkosticdkostic
committed
Make the interactive HOL Light shell work for Arm and x86
Signed-off-by: Dusan Kostic <[email protected]>
1 parent eacdb7e commit 71f93e0

18 files changed

+55
-55
lines changed

‎flake.nix‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -101,8 +101,8 @@
101101
}).overrideAttrs (old: {
102102
shellHook = ''
103103
export PATH=$PWD/scripts:$PATH
104-
# Set PROOF_DIR_ARM based on where we entered the shell
105-
export PROOF_DIR_ARM="$PWD/proofs/hol_light/arm"
104+
# Set PROOF_DIR based on where we entered the shell
105+
export PROOF_DIR="$PWD/proofs/hol_light"
106106
'';
107107
});
108108
devShells.ci = util.mkShell {

‎nix/hol_light/0005-Configure-hol-sh-for-mlkem-native.patch‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -21,10 +21,10 @@ index 1311255..8b2bc36 100755
2121
+SITELIB=$(dirname $(ocamlfind query findlib 2>/dev/null) 2>/dev/null)
2222
+
2323
+# Set HOLLIGHT_LOAD_PATH to include S2N_BIGNUM_DIR and mlkem-native proofs
24-
+export HOLLIGHT_LOAD_PATH="${S2N_BIGNUM_DIR}:${PROOF_DIR_ARM}:${HOLLIGHT_LOAD_PATH}"
24+
+export HOLLIGHT_LOAD_PATH="${S2N_BIGNUM_DIR}:${PROOF_DIR}:${HOLLIGHT_LOAD_PATH}"
2525
+
2626
+# Change to mlkem-native proofs directory if set, so define_from_elf can find object files
27-
+[ -n "${PROOF_DIR_ARM}" ] && cd "${PROOF_DIR_ARM}"
27+
+[ -n "${PROOF_DIR}" ] && cd "${PROOF_DIR}"
2828
+
2929
+${LINE_EDITOR} ${HOLLIGHT_DIR}/ocaml-hol -init ${HOL_ML_PATH} -I ${HOLLIGHT_DIR} ${SITELIB:+-I "$SITELIB"}
3030
diff --git a/hol_4.sh b/hol_4.sh

‎proofs/hol_light/arm/proofs/build-proof.sh‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,7 @@
1616
# - Removal of s2n-bignum specific code that is not relevant for
1717
# the mlkem-native proofs.
1818

19-
ROOT="$(realpath "$(dirname "$0")"/../)"
19+
ROOT="$(realpath "$(dirname "$0")"/../../)"
2020

2121
if [ "$#" -ne 3 ]; then
2222
echo "${ROOT}/build-proof.sh <.ml file path> <hol.sh> <output .native path>"

‎proofs/hol_light/arm/proofs/mlkem_intt.ml‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -9,15 +9,15 @@
99

1010
needs "arm/proofs/base.ml";;
1111

12-
needs "../common/mlkem_specs.ml";;
13-
needs "proofs/mlkem_utils.ml";;
14-
needs "proofs/mlkem_zetas.ml";;
12+
needs "common/mlkem_specs.ml";;
13+
needs "arm/proofs/mlkem_utils.ml";;
14+
needs "arm/proofs/mlkem_zetas.ml";;
1515

16-
(**** print_literal_from_elf "mlkem/mlkem_intt.o";;
16+
(**** print_literal_from_elf "arm/mlkem/mlkem_intt.o";;
1717
****)
1818

1919
let mlkem_intt_mc = define_assert_from_elf
20-
"mlkem_intt_mc" "mlkem/mlkem_intt.o"
20+
"mlkem_intt_mc" "arm/mlkem/mlkem_intt.o"
2121
(*** BYTECODE START ***)
2222
[
2323
0xd10103ff; (* arm_SUB SP SP (rvalue (word 64)) *)

‎proofs/hol_light/arm/proofs/mlkem_ntt.ml‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -9,15 +9,15 @@
99

1010
needs "arm/proofs/base.ml";;
1111

12-
needs "../common/mlkem_specs.ml";;
13-
needs "proofs/mlkem_utils.ml";;
14-
needs "proofs/mlkem_zetas.ml";;
12+
needs "common/mlkem_specs.ml";;
13+
needs "arm/proofs/mlkem_utils.ml";;
14+
needs "arm/proofs/mlkem_zetas.ml";;
1515

16-
(**** print_literal_from_elf "mlkem/mlkem_ntt.o";;
16+
(**** print_literal_from_elf "arm/mlkem/mlkem_ntt.o";;
1717
****)
1818

1919
let mlkem_ntt_mc = define_assert_from_elf
20-
"mlkem_ntt_mc" "mlkem/mlkem_ntt.o"
20+
"mlkem_ntt_mc" "arm/mlkem/mlkem_ntt.o"
2121
(*** BYTECODE START ***)
2222
[
2323
0xd10103ff; (* arm_SUB SP SP (rvalue (word 64)) *)

‎proofs/hol_light/arm/proofs/mlkem_poly_basemul_acc_montgomery_cached_k2.ml‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -5,15 +5,15 @@
55

66
needs "arm/proofs/base.ml";;
77

8-
needs "../common/mlkem_specs.ml";;
9-
needs "proofs/mlkem_utils.ml";;
8+
needs "common/mlkem_specs.ml";;
9+
needs "arm/proofs/mlkem_utils.ml";;
1010

11-
(**** print_literal_from_elf "mlkem/mlkem_poly_basemul_acc_montgomery_cached_k2.o";;
11+
(**** print_literal_from_elf "arm/mlkem/mlkem_poly_basemul_acc_montgomery_cached_k2.o";;
1212
****)
1313

1414

1515
let poly_basemul_acc_montgomery_cached_k2_mc = define_assert_from_elf
16-
"poly_basemul_acc_montgomery_cached_k2_mc" "mlkem/mlkem_poly_basemul_acc_montgomery_cached_k2.o"
16+
"poly_basemul_acc_montgomery_cached_k2_mc" "arm/mlkem/mlkem_poly_basemul_acc_montgomery_cached_k2.o"
1717
(*** BYTECODE START ***)
1818
[
1919
0xd10103ff; (* arm_SUB SP SP (rvalue (word 64)) *)

‎proofs/hol_light/arm/proofs/mlkem_poly_basemul_acc_montgomery_cached_k3.ml‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -5,15 +5,15 @@
55

66
needs "arm/proofs/base.ml";;
77

8-
needs "../common/mlkem_specs.ml";;
9-
needs "proofs/mlkem_utils.ml";;
8+
needs "common/mlkem_specs.ml";;
9+
needs "arm/proofs/mlkem_utils.ml";;
1010

11-
(**** print_literal_from_elf "mlkem/mlkem_poly_basemul_acc_montgomery_cached_k3.o";;
11+
(**** print_literal_from_elf "arm/mlkem/mlkem_poly_basemul_acc_montgomery_cached_k3.o";;
1212
****)
1313

1414

1515
let poly_basemul_acc_montgomery_cached_k3_mc = define_assert_from_elf
16-
"poly_basemul_acc_montgomery_cached_k3_mc" "mlkem/mlkem_poly_basemul_acc_montgomery_cached_k3.o"
16+
"poly_basemul_acc_montgomery_cached_k3_mc" "arm/mlkem/mlkem_poly_basemul_acc_montgomery_cached_k3.o"
1717
(*** BYTECODE START ***)
1818
[
1919
0xd10103ff; (* arm_SUB SP SP (rvalue (word 64)) *)

‎proofs/hol_light/arm/proofs/mlkem_poly_basemul_acc_montgomery_cached_k4.ml‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -5,14 +5,14 @@
55

66
needs "arm/proofs/base.ml";;
77

8-
needs "../common/mlkem_specs.ml";;
9-
needs "proofs/mlkem_utils.ml";;
8+
needs "common/mlkem_specs.ml";;
9+
needs "arm/proofs/mlkem_utils.ml";;
1010

11-
(**** print_literal_from_elf "mlkem/mlkem_poly_basemul_acc_montgomery_cached_k4.o";;
11+
(**** print_literal_from_elf "arm/mlkem/mlkem_poly_basemul_acc_montgomery_cached_k4.o";;
1212
****)
1313

1414
let poly_basemul_acc_montgomery_cached_k4_mc = define_assert_from_elf
15-
"poly_basemul_acc_montgomery_cached_k4_mc" "mlkem/mlkem_poly_basemul_acc_montgomery_cached_k4.o"
15+
"poly_basemul_acc_montgomery_cached_k4_mc" "arm/mlkem/mlkem_poly_basemul_acc_montgomery_cached_k4.o"
1616
(*** BYTECODE START ***)
1717
[
1818
0xd10103ff; (* arm_SUB SP SP (rvalue (word 64)) *)

‎proofs/hol_light/arm/proofs/mlkem_poly_mulcache_compute.ml‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -5,16 +5,16 @@
55

66
needs "arm/proofs/base.ml";;
77

8-
needs "../common/mlkem_specs.ml";;
9-
needs "proofs/mlkem_utils.ml";;
10-
needs "proofs/mlkem_zetas.ml";;
8+
needs "common/mlkem_specs.ml";;
9+
needs "arm/proofs/mlkem_utils.ml";;
10+
needs "arm/proofs/mlkem_zetas.ml";;
1111

1212
(**** print_literal_from_elf "mlkem/poly_mulcache_compute.o";;
1313
****)
1414

1515

1616
let poly_mulcache_compute_mc = define_assert_from_elf
17-
"poly_mulcache_compute_mc" "mlkem/mlkem_poly_mulcache_compute.o"
17+
"poly_mulcache_compute_mc" "arm/mlkem/mlkem_poly_mulcache_compute.o"
1818
(*** BYTECODE START ***)
1919
[
2020
0x5281a025; (* arm_MOV W5 (rvalue (word 3329)) *)

‎proofs/hol_light/arm/proofs/mlkem_poly_reduce.ml‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -9,14 +9,14 @@
99

1010
needs "arm/proofs/base.ml";;
1111

12-
needs "../common/mlkem_specs.ml";;
13-
needs "proofs/mlkem_utils.ml";;
12+
needs "common/mlkem_specs.ml";;
13+
needs "arm/proofs/mlkem_utils.ml";;
1414

15-
(**** print_literal_from_elf "mlkem/mlkem_poly_reduce.o";;
15+
(**** print_literal_from_elf "arm/mlkem/mlkem_poly_reduce.o";;
1616
****)
1717

1818
let mlkem_poly_reduce_mc = define_assert_from_elf
19-
"mlkem_poly_reduce_mc" "mlkem/mlkem_poly_reduce.o"
19+
"mlkem_poly_reduce_mc" "arm/mlkem/mlkem_poly_reduce.o"
2020
(*** BYTECODE START ***)
2121
[
2222
0x5281a022; (* arm_MOV W2 (rvalue (word 3329)) *)

0 commit comments

Comments
 (0)