From 1576d3ee03709f9eac8c7c24b3323a8b8fc1e4f7 Mon Sep 17 00:00:00 2001 From: "Matthias J. Kannwischer" Date: Sun, 25 Oct 2026 22:00:18 +0800 Subject: [PATCH] HOL Light: Fail bytecode update if a proof's bytecode is not dumped The AArch64 dump_bytecode.ml did not dump the five Keccak objects, so `autogen --update-hol-light-bytecode` silently skipped their proofs. Add the missing entries, and make autogen require, for every assembly file in proofs/hol_light//mldsa, a proof file with BYTECODE START/END markers and matching bytecode in the dump. This isn't a soundness risk as outdated bytecode is caught when the proof itself runs, but it is still desirable to also catch outdated bytecode earlier. Signed-off-by: Matthias J. Kannwischer --- .../hol_light/aarch64/proofs/dump_bytecode.ml | 20 +++++++++++++++++++ scripts/autogen | 14 ++++++++++--- 2 files changed, 31 insertions(+), 3 deletions(-) diff --git a/proofs/hol_light/aarch64/proofs/dump_bytecode.ml b/proofs/hol_light/aarch64/proofs/dump_bytecode.ml index 8eb3edefa2..137f95ae40 100644 --- a/proofs/hol_light/aarch64/proofs/dump_bytecode.ml +++ b/proofs/hol_light/aarch64/proofs/dump_bytecode.ml @@ -73,3 +73,23 @@ print_string "==== bytecode end =====================================\n\n";; print_string "=== bytecode start: aarch64/mldsa/mldsa_rej_uniform_eta4_aarch64_asm.o ===\n";; print_literal_from_elf "aarch64/mldsa/mldsa_rej_uniform_eta4_aarch64_asm.o";; print_string "==== bytecode end =====================================\n\n";; + +print_string "=== bytecode start: aarch64/mldsa/keccak_f1600_x1_scalar_aarch64_asm.o ===\n";; +print_literal_from_elf "aarch64/mldsa/keccak_f1600_x1_scalar_aarch64_asm.o";; +print_string "==== bytecode end =====================================\n\n";; + +print_string "=== bytecode start: aarch64/mldsa/keccak_f1600_x1_v84a_aarch64_asm.o ===\n";; +print_literal_from_elf "aarch64/mldsa/keccak_f1600_x1_v84a_aarch64_asm.o";; +print_string "==== bytecode end =====================================\n\n";; + +print_string "=== bytecode start: aarch64/mldsa/keccak_f1600_x2_v84a_aarch64_asm.o ===\n";; +print_literal_from_elf "aarch64/mldsa/keccak_f1600_x2_v84a_aarch64_asm.o";; +print_string "==== bytecode end =====================================\n\n";; + +print_string "=== bytecode start: aarch64/mldsa/keccak_f1600_x4_v8a_scalar_hybrid_aarch64_asm.o ===\n";; +print_literal_from_elf "aarch64/mldsa/keccak_f1600_x4_v8a_scalar_hybrid_aarch64_asm.o";; +print_string "==== bytecode end =====================================\n\n";; + +print_string "=== bytecode start: aarch64/mldsa/keccak_f1600_x4_v8a_v84a_scalar_hybrid_aarch64_asm.o ===\n";; +print_literal_from_elf "aarch64/mldsa/keccak_f1600_x4_v8a_v84a_scalar_hybrid_aarch64_asm.o";; +print_string "==== bytecode end =====================================\n\n";; diff --git a/scripts/autogen b/scripts/autogen index 6f783c32a8..d4581ddb5f 100755 --- a/scripts/autogen +++ b/scripts/autogen @@ -4145,9 +4145,17 @@ def update_hol_light_bytecode_for_arch(arch, force_cross=()): bytecode_dict = extract_bytecode_from_output(output_text) # Update each .ml file - for obj_name, bytecode in bytecode_dict.items(): - ml_file = "proofs/hol_light/" + arch + "/proofs/" + obj_name + ".ml" - update_bytecode_in_proof_script(ml_file, bytecode) + proof_dir = "proofs/hol_light/" + arch + "/proofs" + asm_dir = "proofs/hol_light/" + arch + "/mldsa" + for asm_file in sorted(pathlib.Path(asm_dir).glob("*.S")): + ml_file = f"{proof_dir}/{asm_file.stem}.ml" + if not os.path.isfile(ml_file): + raise Exception(f"{asm_file} has no proof {ml_file}") + if asm_file.stem not in bytecode_dict: + raise Exception( + f"{proof_dir}/dump_bytecode.ml does not dump {asm_file.stem}.o" + ) + update_bytecode_in_proof_script(ml_file, bytecode_dict[asm_file.stem]) def update_hol_light_bytecode(force_cross=()):