Skip to content

Commit 1601215

Browse files
hanno-beckermkannwischer
hanno-becker
authored and
mkannwischer
committed
HOL-Light: Make dump_bytecode work in interactive shell
Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>
1 parent 9ab3e4b commit 1601215

File tree

8 files changed

+41
-41
lines changed

8 files changed

+41
-41
lines changed

‎proofs/hol_light/arm/Makefile‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -144,7 +144,7 @@ run_proofs: build_proofs $(PROOF_LOGS);
144144
proofs: run_proofs ; $(SRC)/tools/count-proofs.sh .
145145

146146
dump_bytecode: proofs/dump_bytecode.native
147-
./$<
147+
cd .. ; ./arm/$<
148148

149149
.PHONY: proofs build_proofs run_proofs sematest clean dump_bytecode
150150

‎proofs/hol_light/arm/proofs/dump_bytecode.ml‎

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

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

8-
print_string "=== bytecode start: mlkem/keccak_f1600_x1_v84a.o ===\n";;
9-
print_literal_from_elf "mlkem/keccak_f1600_x1_v84a.o";;
8+
print_string "=== bytecode start: arm/mlkem/keccak_f1600_x1_v84a.o ===\n";;
9+
print_literal_from_elf "arm/mlkem/keccak_f1600_x1_v84a.o";;
1010
print_string "==== bytecode end =====================================\n\n";;
1111

12-
print_string "=== bytecode start: mlkem/keccak_f1600_x1_scalar.o ===\n";;
13-
print_literal_from_elf "mlkem/keccak_f1600_x1_scalar.o";;
12+
print_string "=== bytecode start: arm/mlkem/keccak_f1600_x1_scalar.o ===\n";;
13+
print_literal_from_elf "arm/mlkem/keccak_f1600_x1_scalar.o";;
1414
print_string "==== bytecode end =====================================\n\n";;
1515

16-
print_string "=== bytecode start: mlkem/keccak_f1600_x2_v84a.o ===\n";;
17-
print_literal_from_elf "mlkem/keccak_f1600_x2_v84a.o";;
16+
print_string "=== bytecode start: arm/mlkem/keccak_f1600_x2_v84a.o ===\n";;
17+
print_literal_from_elf "arm/mlkem/keccak_f1600_x2_v84a.o";;
1818
print_string "==== bytecode end =====================================\n\n";;
1919

20-
print_string "=== bytecode start: mlkem/keccak_f1600_x4_v8a_scalar.o \n";;
21-
print_literal_from_elf "mlkem/keccak_f1600_x4_v8a_scalar.o";;
20+
print_string "=== bytecode start: arm/mlkem/keccak_f1600_x4_v8a_scalar.o \n";;
21+
print_literal_from_elf "arm/mlkem/keccak_f1600_x4_v8a_scalar.o";;
2222
print_string "==== bytecode end =====================================\n\n";;
2323

24-
print_string "=== bytecode start: mlkem/keccak_f1600_x4_v8a_v84a_scalar.o ===\n";;
25-
print_literal_from_elf "mlkem/keccak_f1600_x4_v8a_v84a_scalar.o";;
24+
print_string "=== bytecode start: arm/mlkem/keccak_f1600_x4_v8a_v84a_scalar.o ===\n";;
25+
print_literal_from_elf "arm/mlkem/keccak_f1600_x4_v8a_v84a_scalar.o";;
2626
print_string "==== bytecode end =====================================\n\n";;
2727

28-
print_string "=== bytecode start: mlkem/mlkem_intt.o ===============\n";;
29-
print_literal_from_elf "mlkem/mlkem_intt.o";;
28+
print_string "=== bytecode start: arm/mlkem/mlkem_intt.o ===============\n";;
29+
print_literal_from_elf "arm/mlkem/mlkem_intt.o";;
3030
print_string "==== bytecode end =====================================\n\n";;
3131

32-
print_string "=== bytecode start: mlkem/mlkem_ntt.o ================\n";;
33-
print_literal_from_elf "mlkem/mlkem_ntt.o";;
32+
print_string "=== bytecode start: arm/mlkem/mlkem_ntt.o ================\n";;
33+
print_literal_from_elf "arm/mlkem/mlkem_ntt.o";;
3434
print_string "==== bytecode end =====================================\n\n";;
3535

36-
print_string "=== bytecode start: mlkem/mlkem_poly_basemul_acc_montgomery_cached_k2.o ===\n";;
37-
print_literal_from_elf "mlkem/mlkem_poly_basemul_acc_montgomery_cached_k2.o";;
36+
print_string "=== bytecode start: arm/mlkem/mlkem_poly_basemul_acc_montgomery_cached_k2.o ===\n";;
37+
print_literal_from_elf "arm/mlkem/mlkem_poly_basemul_acc_montgomery_cached_k2.o";;
3838
print_string "==== bytecode end =====================================\n\n";;
3939

40-
print_string "=== bytecode start: mlkem/mlkem_poly_basemul_acc_montgomery_cached_k3.o ===\n";;
41-
print_literal_from_elf "mlkem/mlkem_poly_basemul_acc_montgomery_cached_k3.o";;
40+
print_string "=== bytecode start: arm/mlkem/mlkem_poly_basemul_acc_montgomery_cached_k3.o ===\n";;
41+
print_literal_from_elf "arm/mlkem/mlkem_poly_basemul_acc_montgomery_cached_k3.o";;
4242
print_string "==== bytecode end =====================================\n\n";;
4343

44-
print_string "=== bytecode start: mlkem/mlkem_poly_basemul_acc_montgomery_cached_k4.o ===\n";;
45-
print_literal_from_elf "mlkem/mlkem_poly_basemul_acc_montgomery_cached_k4.o";;
44+
print_string "=== bytecode start: arm/mlkem/mlkem_poly_basemul_acc_montgomery_cached_k4.o ===\n";;
45+
print_literal_from_elf "arm/mlkem/mlkem_poly_basemul_acc_montgomery_cached_k4.o";;
4646
print_string "==== bytecode end =====================================\n\n";;
4747

48-
print_string "=== bytecode start: mlkem/mlkem_poly_mulcache_compute.o ===\n";;
49-
print_literal_from_elf "mlkem/mlkem_poly_mulcache_compute.o";;
48+
print_string "=== bytecode start: arm/mlkem/mlkem_poly_mulcache_compute.o ===\n";;
49+
print_literal_from_elf "arm/mlkem/mlkem_poly_mulcache_compute.o";;
5050
print_string "==== bytecode end =====================================\n\n";;
5151

52-
print_string "=== bytecode start: mlkem/mlkem_poly_reduce.o ========\n";;
53-
print_literal_from_elf "mlkem/mlkem_poly_reduce.o";;
52+
print_string "=== bytecode start: arm/mlkem/mlkem_poly_reduce.o ========\n";;
53+
print_literal_from_elf "arm/mlkem/mlkem_poly_reduce.o";;
5454
print_string "==== bytecode end =====================================\n\n";;
5555

56-
print_string "=== bytecode start: mlkem/mlkem_poly_tobytes.o =======\n";;
57-
print_literal_from_elf "mlkem/mlkem_poly_tobytes.o";;
56+
print_string "=== bytecode start: arm/mlkem/mlkem_poly_tobytes.o =======\n";;
57+
print_literal_from_elf "arm/mlkem/mlkem_poly_tobytes.o";;
5858
print_string "==== bytecode end =====================================\n\n";;
5959

60-
print_string "=== bytecode start: mlkem/mlkem_poly_tomont.o ========\n";;
61-
print_literal_from_elf "mlkem/mlkem_poly_tomont.o";;
60+
print_string "=== bytecode start: arm/mlkem/mlkem_poly_tomont.o ========\n";;
61+
print_literal_from_elf "arm/mlkem/mlkem_poly_tomont.o";;
6262
print_string "==== bytecode end =====================================\n\n";;
6363

64-
print_string "=== bytecode start: mlkem/mlkem_rej_uniform.o ========\n";;
65-
print_literal_from_elf "mlkem/mlkem_rej_uniform.o";;
64+
print_string "=== bytecode start: arm/mlkem/mlkem_rej_uniform.o ========\n";;
65+
print_literal_from_elf "arm/mlkem/mlkem_rej_uniform.o";;
6666
print_string "==== bytecode end =====================================\n\n";;

‎proofs/hol_light/arm/proofs/keccak_f1600_x1_scalar.ml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@
1010
needs "arm/proofs/base.ml";;
1111
needs "arm/proofs/keccak_spec.ml";;
1212

13-
(**** print_literal_from_elf "mlkem/keccak_f1600_x1_scalar.o";;
13+
(**** print_literal_from_elf "arm/mlkem/keccak_f1600_x1_scalar.o";;
1414
****)
1515

1616
let keccak_f1600_x1_scalar_mc = define_assert_from_elf

‎proofs/hol_light/arm/proofs/keccak_f1600_x4_v8a_scalar.ml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@
1010
needs "arm/proofs/base.ml";;
1111
needs "arm/proofs/keccak_spec.ml";;
1212

13-
(**** print_literal_from_elf "mlkem/keccak_f1600_x4_v8a_scalar.o";;
13+
(**** print_literal_from_elf "arm/mlkem/keccak_f1600_x4_v8a_scalar.o";;
1414
****)
1515

1616
let keccak_f1600_x4_v8a_scalar_mc = define_assert_from_elf

‎proofs/hol_light/arm/proofs/keccak_f1600_x4_v8a_v84a_scalar.ml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@
1010
needs "arm/proofs/base.ml";;
1111
needs "arm/proofs/keccak_spec.ml";;
1212

13-
(**** print_literal_from_elf "mlkem/keccak_f1600_x4_v8a_v84a_scalar.o";;
13+
(**** print_literal_from_elf "arm/mlkem/keccak_f1600_x4_v8a_v84a_scalar.o";;
1414
****)
1515

1616
let keccak_f1600_x4_v8a_v84a_scalar_mc = define_assert_from_elf

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@ needs "common/mlkem_specs.ml";;
99
needs "arm/proofs/mlkem_utils.ml";;
1010
needs "arm/proofs/mlkem_zetas.ml";;
1111

12-
(**** print_literal_from_elf "mlkem/poly_mulcache_compute.o";;
12+
(**** print_literal_from_elf "arm/mlkem/poly_mulcache_compute.o";;
1313
****)
1414

1515

‎proofs/hol_light/x86/Makefile‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -122,7 +122,7 @@ run_proofs: build_proofs $(PROOF_LOGS);
122122
proofs: run_proofs ; $(SRC)/tools/count-proofs.sh .
123123

124124
dump_bytecode: proofs/dump_bytecode.native
125-
./$<
125+
cd .. ; ./x86/$<
126126

127127
.PHONY: proofs build_proofs run_proofs sematest clean dump_bytecode
128128

‎proofs/hol_light/x86/proofs/dump_bytecode.ml‎

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

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

8-
print_string "=== bytecode start: mlkem/mlkem_poly_basemul_acc_montgomery_cached_k2.o ===\n";;
9-
print_literal_from_elf "mlkem/mlkem_poly_basemul_acc_montgomery_cached_k2.o";;
8+
print_string "=== bytecode start: x86/mlkem/mlkem_poly_basemul_acc_montgomery_cached_k2.o ===\n";;
9+
print_literal_from_elf "x86/mlkem/mlkem_poly_basemul_acc_montgomery_cached_k2.o";;
1010
print_string "==== bytecode end =====================================\n\n";;
1111

12-
print_string "=== bytecode start: mlkem/mlkem_poly_basemul_acc_montgomery_cached_k3.o ===\n";;
13-
print_literal_from_elf "mlkem/mlkem_poly_basemul_acc_montgomery_cached_k3.o";;
12+
print_string "=== bytecode start: x86/mlkem/mlkem_poly_basemul_acc_montgomery_cached_k3.o ===\n";;
13+
print_literal_from_elf "x86/mlkem/mlkem_poly_basemul_acc_montgomery_cached_k3.o";;
1414
print_string "==== bytecode end =====================================\n\n";;
1515

1616
print_string "=== bytecode start: /mlkem/mlkem_poly_basemul_acc_montgomery_cached_k4.o ===\n";;
17-
print_literal_from_elf "mlkem/mlkem_poly_basemul_acc_montgomery_cached_k4.o";;
17+
print_literal_from_elf "x86/mlkem/mlkem_poly_basemul_acc_montgomery_cached_k4.o";;
1818
print_string "==== bytecode end =====================================\n\n";;

0 commit comments

Comments
 (0)