Blame for code/bugfind/bench/translate_kernels.py

#!/usr/bin/env python3 -I
"""Translate every kernel (pre AND post revision) with Charon -> Aeneas(Lean) and compile the Lean against the pinned
Aeneas library, by reusing translate_items.one() in whole-crate mode. SERIAL by design (host-safety rules); run under hostguard.
Output: JSONL, one line per (kernel, version), with sha256 of the generated Lean (ledger hash of translated definitions).
An item (kernel) is KEPT iff both revisions translate and compile (a pair is needed: pre = positive, post = negative control)."""
import hashlib, json, os, sys
HERE = os.path.dirname(os.path.abspath(__file__)); sys.path.insert(0, HERE)
import translate_items as T
OUTF = sys.argv[1] if len(sys.argv) > 1 else "/apps/development/rlhf/bugfind_data/out/kernel_translate.jsonl"
WORK = "/apps/development/rlhf/bugfind_data/work/kernels"
only = set(sys.argv[2].split(",")) if len(sys.argv) > 2 else None
os.makedirs(WORK, exist_ok=True)
done = {}
if os.path.exists(OUTF):
    for l in open(OUTF): r = json.loads(l); done[r["item"]] = r
with open(OUTF, "a") as f:
    for kid in sorted(os.listdir(f"{HERE}/kernels")):
        if only and kid not in only: continue
        for ver in ("pre", "post"):
            name = f"{kid}.{ver}"
            if name in done: continue
            d = f"{HERE}/kernels/{kid}/{ver}"
            r = T.one(dict(item_id=name, crate=kid, pre_dir=d, stage="diff_safe"), WORK, 600)
            r["kernel"], r["version"] = kid, ver
            if r.get("lean_file"):
                r["lean_sha256"] = hashlib.sha256(open(os.path.join(WORK, name, r["lean_file"]), "rb").read()).hexdigest()
            f.write(json.dumps(r) + "\n"); f.flush()
            print(name, "T" if r["translated"] else "-", r.get("error", "")[:100], r["seconds"], flush=True)