Add dump bytecode to autogen

Signed-off-by: Jake Massimo <[email protected]>

Author: jakemas

proofs/hol_light/x86_64/proofs/mldsa_ntt.ml

@@ -11,9 +11,11 @@ needs "x86/proofs/base.ml";;
 needs "proofs/mldsa_specs.ml";;
 needs "proofs/mldsa_utils.ml";;
 
-print_literal_from_elf "mldsa/mldsa_ntt.o";;
+(*** print_literal_from_elf "mldsa/mldsa_ntt.o";;
+ ***)
 
 let mldsa_ntt_mc = define_assert_from_elf "mldsa_ntt_mc" "mldsa/mldsa_ntt.o"
+(*** BYTECODE START ***)
 [
   0xf3; 0x0f; 0x1e; 0xfa;  (* ENDBR64 *)
   0xc5; 0xfd; 0x6f; 0x06;  (* VMOVDQA (%_% ymm0) (Memop Word256 (%% (rsi,0))) *)
@@ -4411,6 +4413,7 @@ let mldsa_ntt_mc = define_assert_from_elf "mldsa_ntt_mc" "mldsa/mldsa_ntt.o"
                            (* VMOVDQA (Memop Word256 (%% (rdi,992))) (%_% ymm11) *)
   0xc3                     (* RET *)
 ];;
+(*** BYTECODE END ***)
 
 let mldsa_ntt_tmc = define_trimmed "mldsa_ntt_tmc" mldsa_ntt_mc;;
 let MLDSA_NTT_TMC_EXEC = X86_MK_CORE_EXEC_RULE mldsa_ntt_tmc;;

scripts/autogen

@@ -27,6 +27,7 @@ montgomery_factor = pow(2, 32, modulus)
 _RE_DEFINED = re.compile(r"defined\(([^)]+)\)")
 _RE_MARKDOWN_CITE = re.compile(r"\[\^(?P<id>\w+)\]")
 _RE_C_CITE = re.compile(r"@\[(?P<id>\w+)")
+_RE_BYTECODE_START = re.compile(r"=== bytecode start: mldsa/([^/\s]+?)\.o")
 _RE_DEFINE = re.compile(r"^\s*#define\s+(\w+)")
 
 
@@ -2363,11 +2364,86 @@ def gen_test_configs():
         gen_test_config(config_spec["path"], config_spec, default_config)
 
 
+def extract_bytecode_from_output(output_text):
+    """Convert output of proofs/hol_light/x86_64/proofs/dump_bytecode.native
+    into a dictionary mapping function names to byte code strings."""
+    bytecode_dict = {}
+
+    lines = output_text.split("\n")
+    i = 0
+
+    while i < len(lines):
+        line = lines[i]
+        match = _RE_BYTECODE_START.search(line)
+        if match:
+            filename = match.group(1)
+
+            # Collect bytecode until end marker
+            bytecode_lines = []
+            i += 1
+            while i < len(lines) and "==== bytecode end" not in lines[i]:
+                bytecode_lines.append(lines[i])
+                i += 1
+
+            bytecode = "\n".join(bytecode_lines).strip()
+            bytecode_dict[filename] = bytecode
+        i += 1
+
+    return bytecode_dict
+
+
+def update_bytecode_in_proof_script(filepath, bytecode):
+    content = read_file(filepath)
+
+    # Check if markers exist
+    start_marker = "(*** BYTECODE START ***)"
+    end_marker = "(*** BYTECODE END ***)"
+
+    if start_marker not in content or end_marker not in content:
+        raise Exception(f"Could not find BYTECODE START/END markers in {filepath}")
+
+    # Replace content between markers
+    pattern = rf"{re.escape(start_marker)}.*?{re.escape(end_marker)}"
+    replacement = f"{start_marker}\n{bytecode}\n{end_marker}"
+
+    updated_content = re.sub(pattern, replacement, content, flags=re.DOTALL)
+
+    update_file(filepath, updated_content)
+
+
+def update_hol_light_bytecode(dry_run):
+    """Update HOL Light proof files with bytecode from make dump_bytecode."""
+    status_update(
+        "HOL Light bytecode",
+        "Running make dump_bytecode ... (this may take a few minutes)",
+    )
+
+    # Run make to get bytecode output
+    result = subprocess.run(
+        ["make", "-C", "proofs/hol_light/x86_64", "dump_bytecode"],
+        capture_output=True,
+        text=True,
+        check=True,
+    )
+    output_text = result.stdout
+
+    # Extract bytecode
+    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/x86_64/proofs/" + obj_name + ".ml"
+        update_bytecode_in_proof_script(ml_file, bytecode)
+
+
 def _main():
     parser = argparse.ArgumentParser(
         formatter_class=argparse.ArgumentDefaultsHelpFormatter
     )
     parser.add_argument("--dry-run", default=False, action="store_true")
+    parser.add_argument(
+        "--update-hol-light-bytecode", default=False, action="store_true"
+    )
     parser.add_argument("--aarch64-clean", default=True, action="store_true")
     parser.add_argument("--no-simplify", default=False, action="store_true")
     parser.add_argument("--force-cross", default=False, action="store_true")
@@ -2423,6 +2499,10 @@ def _main():
     gen_test_configs()
     high_level_status("Generated test configs")
 
+    if args.update_hol_light_bytecode:
+        update_hol_light_bytecode(args.dry_run)
+        high_level_status("Updated HOL Light bytecode")
+
     gen_preprocessor_comments()
     high_level_status("Generated preprocessor comments")