| |
| """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) |
|
|
