#!/usr/bin/env python3 -I
"""Replay ONE arm-reported witness on the unmodified Rust of a kernel (pre and post) and emit a ledger line.
Usage (under hostguard): replay_flag.py KERNEL 'RUST_ARGS' [--arm NAME] [--claim TEXT] >> bench/ledger/flag_ledger.jsonl
A flag is credited iff replay.pre misbehaves (PANIC/HANG, or a value that violates a bank property) and replay.post does not.
Here `discriminating` is the mechanical part (outcomes differ); property-violation judging is done by the scorer."""
import argparse, json, os, subprocess, sys
HERE = os.path.dirname(os.path.abspath(__file__)); sys.path.insert(0, HERE)
import witness_replay as W
ap = argparse.ArgumentParser(); ap.add_argument("kernel"); ap.add_argument("args"); ap.add_argument("--arm", default="manual"); ap.add_argument("--claim", default="")
a = ap.parse_args()
m = json.load(open(f"{W.KER}/{a.kernel}/meta.json")); os.makedirs(W.WORK, exist_ok=True)
src = f"{W.WORK}/flag_{a.kernel}.rs"; binp = f"{W.WORK}/flag_{a.kernel}.bin"
open(src, "w").write(W.TPL.format(pre=f"{W.KER}/{a.kernel}/pre/src/lib.rs", post=f"{W.KER}/{a.kernel}/post/src/lib.rs", fn=m["function"], args=a.args))
c = subprocess.run(["rustc", *W.FLAGS, "-o", binp, src], capture_output=True, text=True, timeout=120)
if c.returncode: sys.exit("compile error: " + c.stderr[-300:])
pre, post = W.run(binp, "pre"), W.run(binp, "post")
print(json.dumps(dict(item_id=m["item_id"], kind="flag_replay", arm=a.arm, claim=a.claim, witness_call=f'{m["function"]}({a.args})',
                      toolchain=subprocess.run(["rustc", "--version"], capture_output=True, text=True).stdout.strip(), flags=" ".join(W.FLAGS),
                      replay=dict(pre=pre, post=post), discriminating=pre != post,
                      src_sha256=dict(pre=W.sha(f"{W.KER}/{a.kernel}/pre/src/lib.rs"), post=W.sha(f"{W.KER}/{a.kernel}/post/src/lib.rs")))))