Skip to content

Commit a327ee0

Browse files
hanno-beckerhanno-becker
authored
Merge pull request #1202 from pq-code-package/hol_light_bytecode
HOL-Light: Add target to update byte code in proof scripts
2 parents c918885 + 9df17e2 commit a327ee0

20 files changed

+958
-752
lines changed

‎.github/workflows/hol_light.yml‎

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -32,7 +32,25 @@ concurrency:
3232
cancel-in-progress: true
3333

3434
jobs:
35+
# The proofs also check that the byte code is up to date,
36+
# but we use this as a fast path to not even start the proofs
37+
# if the byte code needs updating.
38+
hol_light_bytecode:
39+
name: HOL-Light bytecode check
40+
runs-on: pqcp-arm64
41+
if: github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork
42+
steps:
43+
- uses: actions/checkout@08c6903cd8c0fde910a37f88322edcfb5dd907a8 # v5.0.0
44+
with:
45+
fetch-depth: 0
46+
- uses: ./.github/actions/setup-shell
47+
with:
48+
gh_token: ${{ secrets.GITHUB_TOKEN }}
49+
nix-shell: 'hol_light'
50+
script: |
51+
autogen --update-hol-light-bytecode --dry-run
3552
hol_light_proofs:
53+
needs: [ hol_light_bytecode ]
3654
strategy:
3755
fail-fast: false
3856
matrix:

‎flake.nix‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -84,7 +84,7 @@
8484

8585
devShells.hol_light = util.mkShell {
8686
packages = builtins.attrValues {
87-
inherit (config.packages) hol_light s2n_bignum;
87+
inherit (config.packages) linters hol_light s2n_bignum;
8888
};
8989
};
9090
devShells.ci = util.mkShell {

‎proofs/hol_light/arm/Makefile‎

Lines changed: 11 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -92,6 +92,9 @@ $(OBJ): %.o : %.S
9292
cat $< | $(PREPROCESS) | $(SPLIT) | grep -v -E '^\s+.quad\s+0x[0-9a-f]+$$' | $(ASSEMBLE) -o $@ -
9393
$(OBJDUMP) $@ | ( ( ! grep --ignore-case -E 'w18|[^0]x18' ) || ( rm $@ ; exit 1 ) )
9494
cat $< | $(PREPROCESS) | $(SPLIT) | $(ASSEMBLE) -o $@ -
95+
# MacOS may generate relocations in non-text sections that break
96+
# the object file parser in HOL-Light
97+
strip $@
9598

9699
clean:; rm -f */*.o */*/*.o */*.correct */*.native
97100

@@ -115,6 +118,10 @@ BASE?=$(shell dirname $(realpath $(firstword $(MAKEFILE_LIST))))
115118
PROOF_BINS = $(OBJ:.o=.native)
116119
PROOF_LOGS = $(OBJ:.o=.correct)
117120

121+
# Build precompiled binary for dumping bytecodes
122+
proofs/dump_bytecode.native: proofs/dump_bytecode.ml $(OBJ)
123+
./proofs/build-proof.sh $(BASE)/$< "$(HOLLIGHT)" "$@"
124+
118125
# Build precompiled native binaries of HOL Light proofs
119126

120127
.SECONDEXPANSION:
@@ -135,7 +142,10 @@ run_proofs: build_proofs $(PROOF_LOGS);
135142

136143
proofs: run_proofs ; $(SRC)/tools/count-proofs.sh .
137144

138-
.PHONY: proofs build_proofs run_proofs sematest clean
145+
dump_bytecode: proofs/dump_bytecode.native
146+
./$<
147+
148+
.PHONY: proofs build_proofs run_proofs sematest clean dump_bytecode
139149

140150
# Always run sematest regardless of dependency check
141151
FORCE: ;

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

Lines changed: 66 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,66 @@
1+
(*
2+
* Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
3+
* SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT-0
4+
*)
5+
6+
needs "arm/proofs/base.ml";;
7+
8+
print_string "=== bytecode start: mlkem/keccak_f1600_x1_v84a.o ===\n";;
9+
print_literal_from_elf "mlkem/keccak_f1600_x1_v84a.o";;
10+
print_string "==== bytecode end =====================================\n\n";;
11+
12+
print_string "=== bytecode start: mlkem/keccak_f1600_x1_scalar.o ===\n";;
13+
print_literal_from_elf "mlkem/keccak_f1600_x1_scalar.o";;
14+
print_string "==== bytecode end =====================================\n\n";;
15+
16+
print_string "=== bytecode start: mlkem/keccak_f1600_x2_v84a.o ===\n";;
17+
print_literal_from_elf "mlkem/keccak_f1600_x2_v84a.o";;
18+
print_string "==== bytecode end =====================================\n\n";;
19+
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";;
22+
print_string "==== bytecode end =====================================\n\n";;
23+
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";;
26+
print_string "==== bytecode end =====================================\n\n";;
27+
28+
print_string "=== bytecode start: mlkem/mlkem_intt.o ===============\n";;
29+
print_literal_from_elf "mlkem/mlkem_intt.o";;
30+
print_string "==== bytecode end =====================================\n\n";;
31+
32+
print_string "=== bytecode start: mlkem/mlkem_ntt.o ================\n";;
33+
print_literal_from_elf "mlkem/mlkem_ntt.o";;
34+
print_string "==== bytecode end =====================================\n\n";;
35+
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";;
38+
print_string "==== bytecode end =====================================\n\n";;
39+
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";;
42+
print_string "==== bytecode end =====================================\n\n";;
43+
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";;
46+
print_string "==== bytecode end =====================================\n\n";;
47+
48+
print_string "=== bytecode start: mlkem/mlkem_poly_mulcache_compute.o ===\n";;
49+
print_literal_from_elf "mlkem/mlkem_poly_mulcache_compute.o";;
50+
print_string "==== bytecode end =====================================\n\n";;
51+
52+
print_string "=== bytecode start: mlkem/mlkem_poly_reduce.o ========\n";;
53+
print_literal_from_elf "mlkem/mlkem_poly_reduce.o";;
54+
print_string "==== bytecode end =====================================\n\n";;
55+
56+
print_string "=== bytecode start: mlkem/mlkem_poly_tobytes.o =======\n";;
57+
print_literal_from_elf "mlkem/mlkem_poly_tobytes.o";;
58+
print_string "==== bytecode end =====================================\n\n";;
59+
60+
print_string "=== bytecode start: mlkem/mlkem_poly_tomont.o ========\n";;
61+
print_literal_from_elf "mlkem/mlkem_poly_tomont.o";;
62+
print_string "==== bytecode end =====================================\n\n";;
63+
64+
print_string "=== bytecode start: mlkem/mlkem_rej_uniform.o ========\n";;
65+
print_literal_from_elf "mlkem/mlkem_rej_uniform.o";;
66+
print_string "==== bytecode end =====================================\n\n";;

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

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@ needs "proofs/keccak_spec.ml";;
1515

1616
let keccak_f1600_x1_scalar_mc = define_assert_from_elf
1717
"keccak_f1600_x1_scalar_mc" "mlkem/keccak_f1600_x1_scalar.o"
18+
(*** BYTECODE START ***)
1819
[
1920
0xd10203ff; (* arm_SUB SP SP (rvalue (word 128)) *)
2021
0xa90253f3; (* arm_STP X19 X20 SP (Immediate_Offset (iword (&32))) *)
@@ -305,6 +306,7 @@ let keccak_f1600_x1_scalar_mc = define_assert_from_elf
305306
0x910203ff; (* arm_ADD SP SP (rvalue (word 128)) *)
306307
0xd65f03c0 (* arm_RET X30 *)
307308
];;
309+
(*** BYTECODE END ***)
308310

309311
let KECCAK_F1600_X1_SCALAR_EXEC = ARM_MK_EXEC_RULE keccak_f1600_x1_scalar_mc;;
310312

‎proofs/hol_light/arm/proofs/keccak_f1600_x1_v84a.ml‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@ needs "proofs/keccak_spec.ml";;
1515

1616
let keccak_f1600_x1_v84a_mc = define_assert_from_elf
1717
"keccak_f1600_x1_v84a_mc" "mlkem/keccak_f1600_x1_v84a.o"
18+
(*** BYTECODE START ***)
1819
[
1920
0xd10103ff; (* arm_SUB SP SP (rvalue (word 64)) *)
2021
0x6d0027e8; (* arm_STP D8 D9 SP (Immediate_Offset (iword (&0))) *)
@@ -124,6 +125,7 @@ let keccak_f1600_x1_v84a_mc = define_assert_from_elf
124125
0x910103ff; (* arm_ADD SP SP (rvalue (word 64)) *)
125126
0xd65f03c0 (* arm_RET X30 *)
126127
];;
128+
(*** BYTECODE END ***)
127129

128130
let KECCAK_F1600_X1_V84A_EXEC = ARM_MK_EXEC_RULE keccak_f1600_x1_v84a_mc;;
129131

‎proofs/hol_light/arm/proofs/keccak_f1600_x2_v84a.ml‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@ needs "proofs/keccak_spec.ml";;
1515

1616
let keccak_f1600_x2_v84a_mc = define_assert_from_elf
1717
"keccak_f1600_x2_v84a_mc" "mlkem/keccak_f1600_x2_v84a.o"
18+
(*** BYTECODE START ***)
1819
[
1920
0xd10103ff; (* arm_SUB SP SP (rvalue (word 64)) *)
2021
0x6d0027e8; (* arm_STP D8 D9 SP (Immediate_Offset (iword (&0))) *)
@@ -178,6 +179,7 @@ let keccak_f1600_x2_v84a_mc = define_assert_from_elf
178179
0x910103ff; (* arm_ADD SP SP (rvalue (word 64)) *)
179180
0xd65f03c0 (* arm_RET X30 *)
180181
];;
182+
(*** BYTECODE END ***)
181183

182184
let KECCAK_F1600_X2_V84A_EXEC = ARM_MK_EXEC_RULE keccak_f1600_x2_v84a_mc;;
183185

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

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@ needs "proofs/keccak_spec.ml";;
1515

1616
let keccak_f1600_x4_v8a_scalar_mc = define_assert_from_elf
1717
"keccak_f1600_x4_v8a_scalar_mc" "mlkem/keccak_f1600_x4_v8a_scalar.o"
18+
(*** BYTECODE START ***)
1819
[
1920
0xd10383ff; (* arm_SUB SP SP (rvalue (word 224)) *)
2021
0xa90353f3; (* arm_STP X19 X20 SP (Immediate_Offset (iword (&48))) *)
@@ -985,6 +986,7 @@ let keccak_f1600_x4_v8a_scalar_mc = define_assert_from_elf
985986
0x910383ff; (* arm_ADD SP SP (rvalue (word 224)) *)
986987
0xd65f03c0 (* arm_RET X30 *)
987988
];;
989+
(*** BYTECODE END ***)
988990

989991
let KECCAK_F1600_X4_V8A_SCALAR_EXEC = ARM_MK_EXEC_RULE keccak_f1600_x4_v8a_scalar_mc;;
990992

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

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@ needs "proofs/keccak_spec.ml";;
1515

1616
let keccak_f1600_x4_v8a_v84a_scalar_mc = define_assert_from_elf
1717
"keccak_f1600_x4_v8a_v84a_scalar_mc" "mlkem/keccak_f1600_x4_v8a_v84a_scalar.o"
18+
(*** BYTECODE START ***)
1819
[
1920
0xd10383ff; (* arm_SUB SP SP (rvalue (word 224)) *)
2021
0xa90353f3; (* arm_STP X19 X20 SP (Immediate_Offset (iword (&48))) *)
@@ -891,6 +892,7 @@ let keccak_f1600_x4_v8a_v84a_scalar_mc = define_assert_from_elf
891892
0x910383ff; (* arm_ADD SP SP (rvalue (word 224)) *)
892893
0xd65f03c0 (* arm_RET X30 *)
893894
];;
895+
(*** BYTECODE END ***)
894896

895897
let KECCAK_F1600_X4_V8A_V84A_SCALAR_EXEC = ARM_MK_EXEC_RULE keccak_f1600_x4_v8a_v84a_scalar_mc;;
896898

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

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,7 @@ needs "proofs/mlkem_zetas.ml";;
1818

1919
let mlkem_intt_mc = define_assert_from_elf
2020
"mlkem_intt_mc" "mlkem/mlkem_intt.o"
21+
(*** BYTECODE START ***)
2122
[
2223
0xd10103ff; (* arm_SUB SP SP (rvalue (word 64)) *)
2324
0x6d0027e8; (* arm_STP D8 D9 SP (Immediate_Offset (iword (&0))) *)
@@ -542,6 +543,7 @@ let mlkem_intt_mc = define_assert_from_elf
542543
0x910103ff; (* arm_ADD SP SP (rvalue (word 64)) *)
543544
0xd65f03c0 (* arm_RET X30 *)
544545
];;
546+
(*** BYTECODE END ***)
545547

546548
let MLKEM_INTT_EXEC = ARM_MK_EXEC_RULE mlkem_intt_mc;;
547549

0 commit comments

Comments
 (0)