#!/usr/bin/env python3
"""Build and run offline emulator proof tests from analyzer findings.

This tool is intentionally separate from the analyzer chain.  The analyzer emits
static findings and proof intents in a hlds-analyzer-proof-pack JSON/JSONC file;
this tool binds those proof intents to a concrete emulator session/device/media
profile and runs them offline through gdr_host_jsonl_bridge.py.

Expected ownership:
  * analyzer chain:       device profiles + analyzer proof packs
  * dumper/media tooling: media profiles
  * session builder:      session profiles
  * this tool:            offline proof scripts + proof reports
"""
from __future__ import annotations

import argparse
import hashlib
import json
import subprocess
import sys
from pathlib import Path
from typing import Any

from hlds_profiles import (
    load_json_or_jsonc,
    load_device_profile,
    load_media_profile,
    effective_session,
    write_json,
)

try:
    from hlds_lba_trace_validator import validate_lba_trace, write_md as write_lba_trace_md
except Exception:
    validate_lba_trace = None
    write_lba_trace_md = None


GOOD_STATUSES = {"good", "ok", "success", "passed"}
CHECK_STATUSES = {"check_condition", "check condition", "cc", "sense"}


def parse_hex_bytes(text: Any) -> bytes:
    if text is None:
        return b""
    if isinstance(text, (bytes, bytearray)):
        return bytes(text)
    s = str(text).strip()
    if not s:
        return b""
    s = s.replace("0x", "").replace("0X", "")
    s = "".join(ch for ch in s if ch in "0123456789abcdefABCDEF")
    if len(s) % 2:
        s = "0" + s
    return bytes.fromhex(s)


def hx(data: bytes) -> str:
    return " ".join(f"{b:02X}" for b in data)


def safe_name(text: Any) -> str:
    out = "".join(ch if ch.isalnum() or ch in "._-" else "_" for ch in str(text))
    out = out.strip("._-")
    return out or "proof"


def norm_hex(text: Any) -> str:
    return hx(parse_hex_bytes(text))


def sha256_file(path: Path) -> str:
    h = hashlib.sha256()
    with path.open("rb") as f:
        for chunk in iter(lambda: f.read(1024 * 1024), b""):
            h.update(chunk)
    return h.hexdigest()


def rel_or_abs(path_text: str | Path | None, base: Path | None) -> Path | None:
    if not path_text:
        return None
    p = Path(str(path_text))
    if not p.is_absolute() and base is not None:
        p = base / p
    return p


def load_context(args: argparse.Namespace) -> tuple[dict[str, Any], dict[str, Any], dict[str, Any], str | None, str | None]:
    session = effective_session(
        args.session_profile,
        device_profile=args.device_profile,
        media_profile=args.media_profile,
        firmware_image=args.firmware_image,
    ) if (args.session_profile or args.device_profile or args.media_profile or args.firmware_image) else {}
    device_path = args.device_profile or session.get("device_profile")
    media_path = args.media_profile or session.get("media_profile")
    device = load_device_profile(device_path) if device_path else {}
    media = load_media_profile(media_path) if media_path else {}
    return session, device, media, str(device_path) if device_path else None, str(media_path) if media_path else None


def proof_findings(proof_pack: dict[str, Any]) -> list[dict[str, Any]]:
    findings = proof_pack.get("findings") or proof_pack.get("proofs") or []
    if not isinstance(findings, list):
        raise SystemExit("proof pack 'findings' must be a list")
    return [dict(f) for f in findings]


def validate_proof_pack(doc: dict[str, Any]) -> None:
    fmt = doc.get("format")
    if fmt not in ("hlds-analyzer-proof-pack", "hlds-proof-pack"):
        raise SystemExit(f"proof pack has unexpected format: {fmt!r}")
    if not isinstance(doc.get("findings") or doc.get("proofs") or [], list):
        raise SystemExit("proof pack missing findings/proofs list")


def find_scsi_response_file(media: dict[str, Any], key: str) -> str | None:
    key_l = key.lower().replace("-", "_")
    for row in media.get("scsi_responses") or []:
        name = str(row.get("name") or "").lower().replace("-", "_")
        if key_l in name or (key_l == "ad_c0" and "xbox_control" in name):
            return row.get("response_file")
    return None


def resolve_media_payload_ref(media: dict[str, Any], media_path: str | None, ref: str) -> Path | None:
    """Resolve refs like media.dvd_structures.ad_c0 or payload:ad_c0."""
    if not ref:
        return None
    base = Path(media_path).resolve().parent if media_path else None
    ref = str(ref)
    key = ref.split(":", 1)[-1].split(".")[-1]
    key = key.lower()

    dvd = media.get("dvd_structures") or {}
    value = dvd.get(key)
    if isinstance(value, dict):
        value = value.get("file") or value.get("path") or value.get("response_file")
    if not value:
        value = find_scsi_response_file(media, key)
    if not value and key == "xbox_control_block_ad_c0":
        value = find_scsi_response_file(media, "ad_c0")
    return rel_or_abs(value, base) if value else None


def expected_sha_for_ref(media: dict[str, Any], media_path: str | None, ref: str) -> tuple[str | None, str | None]:
    p = resolve_media_payload_ref(media, media_path, ref)
    if not p:
        return None, f"payload_ref not found in media profile: {ref}"
    if not p.exists():
        return None, f"payload_ref file does not exist: {p}"
    return sha256_file(p), None


def request_from_step(finding: dict[str, Any], step: dict[str, Any], step_index: int) -> tuple[dict[str, Any] | None, dict[str, Any]]:
    fid = str(finding.get("finding_id") or finding.get("id") or f"finding_{step_index}")
    tag = str(step.get("tag") or step.get("name") or f"{safe_name(fid)}_step{step_index:02d}")
    row: dict[str, Any]
    if step.get("op"):
        row = {"op": step.get("op"), "tag": tag}
        for k in ("stage", "force", "reset_auth", "xdvd_json", "iso", "log", "unlocked"):
            if k in step:
                row[k] = step[k]
    else:
        cdb = step.get("cdb_hex") or step.get("cdb")
        if not cdb:
            return None, {"blocked": True, "reason": "step has neither op nor cdb_hex", "tag": tag}
        row = {"tag": tag, "cdb_hex": cdb}
        if step.get("data_out_hex") is not None:
            row["data_out_hex"] = step.get("data_out_hex")
        elif step.get("data_out") is not None:
            row["data_out_hex"] = step.get("data_out")
        if step.get("reset_auth_stage"):
            row["reset_auth_stage"] = step.get("reset_auth_stage")
        if step.get("title"):
            row["title"] = step.get("title")
    row["proof_id"] = fid
    row["proof_step_index"] = step_index

    exp = dict(step.get("expectation") or step.get("expect") or {})
    # Allow shorthand step-level expectation fields.
    for k, v in step.items():
        if k.startswith("expect_") or k.startswith("expected_"):
            exp[k] = v
    return row, exp


def command_cdb_by_name(name: str) -> str | None:
    key = name.lower().replace(" ", "_").replace("-", "_")
    table = {
        "test_unit_ready": "00 00 00 00 00 00",
        "inquiry": "12 00 00 00 24 00",
        "request_sense": "03 00 00 00 12 00",
        "read_capacity_10": "25 00 00 00 00 00 00 00 00 00",
        "get_configuration": "46 02 00 00 00 00 00 00 40 00",
        "read_disc_information": "51 00 00 00 00 00 00 00 22 00",
        "read_track_information": "52 01 00 00 00 01 00 00 24 00",
        "write_buffer": "3B 05 00 00 00 00 00 00 40 00",
        "write_10": "2A 00 00 00 00 00 00 00 01 00",
        "write_12": "AA 00 00 00 00 01 00 00 00 01 00 00",
        "blank": "A1 00 00 00 00 00 00 00 00 00 00 00",
        "format_unit": "04 11 00 00 00 00",
        "reserve_track": "53 00 00 00 00 00 00 00 10 00",
        "close_track_session": "5B 00 02 00 00 00 00 00 00 00",
        "synchronize_cache_10": "35 00 00 00 00 00 00 00 00 00",
    }
    return table.get(key)


def synthetic_payload(blocks: int = 1, sector_size: int = 2048, seed: int = 0x42) -> str:
    data = bytes(((i + seed) & 0xFF for i in range(max(1, blocks) * max(1, sector_size))))
    return hx(data)


def steps_from_dynamic_expectation(finding: dict[str, Any], media: dict[str, Any]) -> tuple[list[dict[str, Any]], dict[str, Any] | None]:
    dyn = dict(finding.get("dynamic_expectation") or finding.get("dynamic_test") or {})
    if not dyn:
        return [], {"blocked": True, "reason": "finding has no dynamic_expectation/dynamic_test"}

    # Explicit dynamic_test.steps wins.
    steps = dyn.get("steps")
    if isinstance(steps, list):
        return [dict(s) for s in steps], None

    # A single CDB expectation.
    if dyn.get("cdb_hex") or dyn.get("cdb"):
        step = {
            "name": dyn.get("name") or finding.get("finding_id") or "proof_cdb",
            "cdb_hex": dyn.get("cdb_hex") or dyn.get("cdb"),
            "expectation": {k: v for k, v in dyn.items() if k.startswith("expected_") or k.startswith("expect_") or k in ("direction", "data_len", "payload_ref")},
        }
        if dyn.get("data_out_hex"):
            step["data_out_hex"] = dyn.get("data_out_hex")
        return [step], None

    # Command list expectation, useful for write/firmware-update surfaces.
    commands = dyn.get("commands") or []
    if isinstance(commands, list) and commands:
        out: list[dict[str, Any]] = []
        for i, c in enumerate(commands):
            c = dict(c)
            name = str(c.get("name") or c.get("command") or f"cmd{i:02d}")
            cdb = c.get("cdb_hex") or command_cdb_by_name(name)
            if not cdb:
                continue
            row: dict[str, Any] = {"name": name, "cdb_hex": cdb}
            if c.get("data_out") or c.get("data_out_hex"):
                row["data_out_hex"] = c.get("data_out_hex") or synthetic_payload()
            row["expectation"] = {k: v for k, v in c.items() if k.startswith("expected_") or k.startswith("expect_") or k in ("expected_status", "expected_policy")}
            out.append(row)
        return out, None if out else {"blocked": True, "reason": "no commands could be resolved to CDBs"}

    return [], {"blocked": True, "reason": "dynamic expectation had no supported test shape"}


def generate_finding_script(finding: dict[str, Any], media: dict[str, Any]) -> tuple[list[dict[str, Any]], list[dict[str, Any]], dict[str, Any] | None]:
    steps, blocked = steps_from_dynamic_expectation(finding, media)
    if blocked:
        return [], [], blocked

    rows: list[dict[str, Any]] = []
    expectations: list[dict[str, Any]] = []
    # Optional setup stage at finding level.
    stage = (finding.get("dynamic_expectation") or {}).get("requires_auth_stage") or finding.get("requires_auth_stage")
    if stage:
        rows.append({"op": "reset_auth", "stage": stage, "tag": f"{safe_name(finding.get('finding_id','finding'))}_reset_{stage}", "proof_id": finding.get("finding_id")})
        expectations.append({"tag": rows[-1]["tag"], "control": True, "expected_status": "GOOD"})

    for idx, step in enumerate(steps):
        row, exp = request_from_step(finding, step, idx)
        if row is None:
            return [], [], exp
        rows.append(row)
        exp = dict(exp)
        exp.setdefault("tag", row.get("tag"))
        expectations.append(exp)
    return rows, expectations, None



def make_read10_cdb_hex(lba: int, blocks: int = 1) -> str:
    cdb = bytearray(10)
    cdb[0] = 0x28
    cdb[2:6] = int(lba).to_bytes(4, "big", signed=False)
    cdb[7:9] = int(blocks).to_bytes(2, "big", signed=False)
    return hx(bytes(cdb))


def is_lba_transform_finding(finding: dict[str, Any]) -> bool:
    ftype = str(finding.get("type") or "").lower()
    dyn = finding.get("dynamic_expectation") or finding.get("dynamic_test") or {}
    run_mode = str(dyn.get("run_mode") or "").lower()
    goal = str(dyn.get("proof_goal") or "").lower()
    return (
        "lba_transform" in ftype
        or "lba_window" in ftype
        or run_mode == "offline_cpu_trace"
        or "lba" in goal and "translation" in goal
    )


def generate_lba_bridge_probe_script(finding: dict[str, Any]) -> list[dict[str, Any]]:
    """Generate a bridge-level READ probe script for an LBA transform finding.

    These probes are not a firmware proof by themselves. They are useful context:
    they show what the current high-level bridge model serves for each host LBA.
    A PROVEN firmware result still requires CPU/MMIO evidence.
    """
    dyn = dict(finding.get("dynamic_expectation") or finding.get("dynamic_test") or {})
    fid = str(finding.get("finding_id") or finding.get("id") or "lba_transform")
    rows: list[dict[str, Any]] = []
    stage = dyn.get("requires_auth_state") or dyn.get("requires_auth_stage") or "unlocked"
    rows.append({"op": "reset_auth", "stage": stage, "tag": f"{safe_name(fid)}_reset_{stage}", "proof_id": fid})
    rows.append({"op": "firmware_lba_state", "tag": f"{safe_name(fid)}_state_before_reads", "proof_id": fid})
    probes = dyn.get("probe_reads") or []
    if not isinstance(probes, list) or not probes:
        probes = [{"host_lba": 0}, {"host_lba": 32}, {"host_lba": 33}]
    for i, probe in enumerate(probes):
        if isinstance(probe, dict):
            lba = int(probe.get("host_lba") or probe.get("lba") or 0)
            blocks = int(probe.get("blocks") or 1)
            expected = probe.get("expected_current_bridge_iso_lba")
        else:
            lba = int(probe)
            blocks = 1
            expected = None
        row = {
            "tag": f"{safe_name(fid)}_read_lba{lba}_blocks{blocks}",
            "cdb_hex": make_read10_cdb_hex(lba, blocks),
            "proof_id": fid,
            "proof_step_index": i,
            "lba_probe": True,
            "expected_current_bridge_iso_lba": expected,
        }
        rows.append(row)
    rows.append({"op": "firmware_lba_state", "tag": f"{safe_name(fid)}_state_after_reads", "proof_id": fid})
    return rows


def handle_lba_transform_finding(args: argparse.Namespace, finding: dict[str, Any], scripts_dir: Path, runs_dir: Path) -> tuple[dict[str, Any], dict[str, Any]]:
    """Special handling for firmware LBA transform proof targets.

    This deliberately refuses to mark a firmware LBA proof as PROVEN from the
    sidecar/bridge model alone. If --allow-bridge-model-lba-proof is supplied,
    it can run the generated bridge probe and report MODEL_ONLY when the current
    high-level mapping matches expectations. Otherwise it reports BLOCKED and
    points at the missing CPU/MMIO trace surface.
    """
    fid = str(finding.get("finding_id") or finding.get("id") or "lba_transform")
    ftype = str(finding.get("type") or "firmware_lba_transform")
    rows = generate_lba_bridge_probe_script(finding)
    script_path = scripts_dir / f"{safe_name(fid)}.bridge_lba_probe.jsonl"
    write_jsonl(script_path, rows)
    base_entry: dict[str, Any] = {
        "finding_id": fid,
        "type": ftype,
        "confidence": finding.get("confidence"),
        "requests": len(rows),
        "script": str(script_path),
        "trace_required": True,
        "trace_kind": "cpu_mmio_packet_dma",
    }

    dyn = dict(finding.get("dynamic_expectation") or finding.get("dynamic_test") or {})
    if args.cpu_trace_csv:
        entry = dict(base_entry)
        if validate_lba_trace is None:
            entry.update({
                "outcome": "BLOCKED",
                "notes": [
                    "cpu trace path was supplied but hlds_lba_trace_validator.py could not be imported",
                    f"cpu_trace_csv={args.cpu_trace_csv}",
                ],
            })
            return base_entry, entry
        try:
            # Validate this single finding against the supplied CPU/MMIO trace.
            pp = {"format": "hlds-analyzer-proof-pack", "version": 1, "findings": [finding]}
            trace_report = validate_lba_trace(args.cpu_trace_csv, pp)
            out_base = Path(args.cpu_trace_csv).with_suffix("")
            trace_json = out_base.parent / f"{out_base.name}.{safe_name(fid)}.proof.json"
            trace_md = out_base.parent / f"{out_base.name}.{safe_name(fid)}.proof.md"
            write_json(trace_json, trace_report)
            if write_lba_trace_md is not None:
                write_lba_trace_md(trace_md, trace_report)
            f_reports = trace_report.get("findings") or []
            outcome = f_reports[0].get("outcome") if f_reports else "BLOCKED"
            entry.update({
                "outcome": outcome,
                "cpu_trace_csv": args.cpu_trace_csv,
                "cpu_trace_proof_json": str(trace_json),
                "cpu_trace_proof_md": str(trace_md),
                "notes": ["validated supplied CPU/MMIO trace with hlds_lba_trace_validator.py"],
            })
        except Exception as e:
            entry.update({
                "outcome": "BLOCKED",
                "notes": [f"cpu trace validation failed: {e}", f"cpu_trace_csv={args.cpu_trace_csv}"],
            })
        return base_entry, entry

    if args.run_jsonl and args.allow_bridge_model_lba_proof:
        rc, responses = run_finding(args, fid, script_path, runs_dir)
        problems: list[str] = []
        resp_by_tag = {str(r.get("tag")): r for r in responses}
        for row in rows:
            if not row.get("lba_probe"):
                continue
            tag = str(row.get("tag"))
            resp = resp_by_tag.get(tag)
            if not resp:
                problems.append(f"missing bridge probe response for {tag}")
                continue
            expected = row.get("expected_current_bridge_iso_lba")
            if expected is not None:
                got = resp.get("iso_lba")
                try:
                    got_i = int(got)
                except Exception:
                    problems.append(f"{tag}: missing/invalid iso_lba in response: {got!r}")
                    continue
                if got_i != int(expected):
                    problems.append(f"{tag}: current bridge iso_lba expected {expected}, got {got_i}")
            source = str(resp.get("firmware_state_source") or "")
            if "pending_mmio" in source or "bridge_instrumentation" in source:
                # This is expected: it is why the result is MODEL_ONLY.
                pass
        entry = dict(base_entry)
        if problems or rc not in (0, 2):
            if rc not in (0, 2):
                problems.append(f"runner return code {rc}")
            entry.update({"returncode": rc, "responses": len(responses), "outcome": "CONTRADICTED", "problems": problems})
        else:
            entry.update({
                "returncode": rc,
                "responses": len(responses),
                "outcome": "MODEL_ONLY",
                "notes": [
                    "current high-level bridge LBA model matched expectations",
                    "not a firmware proof: CPU/MMIO packet-DMA trace is still required",
                ],
            })
        return base_entry, entry

    entry = dict(base_entry)
    entry.update({
        "outcome": "BLOCKED",
        "notes": [
            "firmware LBA transform proof requires CPU/MMIO packet-DMA trace; sidecar/bridge mapping alone is not sufficient",
            "bridge-level probe script was generated for context only",
            "rerun with --run-jsonl --allow-bridge-model-lba-proof only if you intentionally want MODEL_ONLY evidence",
        ],
    })
    return base_entry, entry


def normalize_expected_status(value: Any) -> str | None:
    if value is None:
        return None
    s = str(value).strip().lower().replace("-", "_")
    if s in GOOD_STATUSES:
        return "GOOD"
    if s in CHECK_STATUSES:
        return "CHECK CONDITION"
    if s in ("good", "check condition"):
        return s.upper()
    return str(value).upper()


def response_matches_expectation(row: dict[str, Any], exp: dict[str, Any], media: dict[str, Any], media_path: str | None) -> tuple[bool, list[str]]:
    problems: list[str] = []
    status = normalize_expected_status(exp.get("expected_status") or exp.get("expect_status") or exp.get("scsi_status"))
    if status and str(row.get("scsi_status") or "").upper() != status:
        problems.append(f"status expected {status}, got {row.get('scsi_status')}")

    direction = exp.get("expected_direction") or exp.get("expect_direction") or exp.get("direction")
    if direction and str(row.get("direction") or "").lower() != str(direction).lower():
        problems.append(f"direction expected {direction}, got {row.get('direction')}")

    exact_len = exp.get("expected_exact_len") or exp.get("expect_exact_len") or exp.get("expected_data_len")
    if exact_len is not None and int(row.get("data_len") or 0) != int(exact_len):
        problems.append(f"data_len expected {exact_len}, got {row.get('data_len')}")

    min_len = exp.get("expected_min_len") or exp.get("expect_min_len")
    if min_len is not None and int(row.get("data_len") or 0) < int(min_len):
        problems.append(f"data_len expected >= {min_len}, got {row.get('data_len')}")

    prefix = exp.get("expected_data_prefix_hex") or exp.get("expect_data_prefix_hex") or exp.get("expected_prefix_hex")
    if prefix:
        got = parse_hex_bytes(row.get("data_hex") or row.get("data_preview_hex") or "")
        want = parse_hex_bytes(prefix)
        if not got.startswith(want):
            problems.append(f"data prefix expected {hx(want)}, got {hx(got[:len(want)])}")

    contains = exp.get("expected_contains_hex") or exp.get("expect_contains_hex")
    if contains:
        got = parse_hex_bytes(row.get("data_hex") or "")
        want = parse_hex_bytes(contains)
        if want not in got:
            problems.append(f"data did not contain {hx(want)}")

    expected_sha = exp.get("expected_payload_sha256") or exp.get("expect_payload_sha256") or exp.get("expected_data_sha256")
    if not expected_sha and (exp.get("expected_payload_ref") or exp.get("expect_payload_ref") or exp.get("payload_ref") or exp.get("requires_media_payload")):
        ref = exp.get("expected_payload_ref") or exp.get("expect_payload_ref") or exp.get("payload_ref") or exp.get("requires_media_payload")
        expected_sha, err = expected_sha_for_ref(media, media_path, str(ref))
        if err:
            problems.append(err)
    if expected_sha and str(row.get("data_sha256") or "") != str(expected_sha):
        problems.append(f"data_sha256 expected {expected_sha}, got {row.get('data_sha256')}")

    policy = exp.get("expected_policy") or exp.get("expect_policy")
    if policy:
        # Capture-only commands may be GOOD or CHECK CONDITION depending on device policy;
        # require only that data-out was observed or the row carries a capture/policy hint.
        if str(policy) == "capture_only":
            captured = bool(row.get("captured_data_out") or row.get("data_out_len") or row.get("direction") == "out" or row.get("data_len"))
            if not captured:
                problems.append("expected capture_only evidence, but no data-out/capture marker was present")

    return not problems, problems


def run_cmd(cmd: list[str], cwd: Path | None, log_path: Path | None = None) -> int:
    print("[RUN]", " ".join(str(x) for x in cmd))
    proc = subprocess.run(cmd, cwd=str(cwd) if cwd else None, text=True, stdout=subprocess.PIPE, stderr=subprocess.STDOUT)
    if log_path:
        log_path.parent.mkdir(parents=True, exist_ok=True)
        log_path.write_text(proc.stdout, encoding="utf-8")
    sys.stdout.write(proc.stdout)
    return int(proc.returncode)


def write_jsonl(path: Path, rows: list[dict[str, Any]]) -> None:
    path.parent.mkdir(parents=True, exist_ok=True)
    path.write_text("# hlds offline proof JSONL; keep comment so single-row files are not mistaken for JSON objects\n" + "".join(json.dumps(r, separators=(",", ":")) + "\n" for r in rows), encoding="utf-8")


def run_finding(args: argparse.Namespace, finding_id: str, script_path: Path, out_dir: Path) -> tuple[int, list[dict[str, Any]]]:
    resp = out_dir / f"{safe_name(finding_id)}.responses.jsonl"
    payload_dir = out_dir / f"{safe_name(finding_id)}.payloads"
    verify = out_dir / f"{safe_name(finding_id)}.verify.md"
    log = out_dir / f"{safe_name(finding_id)}.run.log"
    cmd = [args.python, args.jsonl_bridge, "--script", str(script_path), "--out", str(resp), "--write-response-dir", str(payload_dir), "--verify-md", str(verify)]
    if args.session_profile:
        cmd += ["--session-profile", args.session_profile]
    else:
        if args.device_profile:
            cmd += ["--device-profile", args.device_profile]
        if args.media_profile:
            cmd += ["--media-profile", args.media_profile, args.media_profile]
        if args.iso:
            cmd += [args.iso]
    if args.read_map:
        cmd += ["--xdvd-read-map", args.read_map]
    if args.log:
        cmd += ["--log", args.log]
    rc = run_cmd(cmd, Path(args.cwd) if args.cwd else None, log)
    rows: list[dict[str, Any]] = []
    if resp.exists():
        rows = [json.loads(line) for line in resp.read_text(encoding="utf-8").splitlines() if line.strip()]
    return rc, rows


def write_proof_report(out_dir: Path, report: dict[str, Any]) -> None:
    lines: list[str] = []
    lines.append("# HLDS offline analyzer proof report")
    lines.append("")
    lines.append(f"stem={report.get('stem')}")
    lines.append(f"proof_pack={report.get('proof_pack')}")
    lines.append(f"session_profile={report.get('session_profile') or ''}")
    lines.append(f"device_profile={report.get('device_profile') or ''}")
    lines.append(f"media_profile={report.get('media_profile') or ''}")
    lines.append("")
    lines.append("| finding | type | outcome | requests | rc | notes |")
    lines.append("|---|---|---|---:|---:|---|")
    for item in report.get("findings") or []:
        notes = "; ".join(item.get("notes") or item.get("problems") or [])
        lines.append(f"| `{item.get('finding_id')}` | `{item.get('type','')}` | **{item.get('outcome')}** | {item.get('requests',0)} | {item.get('returncode','')} | {notes} |")
    lines.append("")
    lines.append("Outcome meanings: PROVEN = dynamic response matched expectation; MODEL_ONLY = current high-level bridge model matched but firmware code/MMIO source is not proven; CONTRADICTED = response ran but violated expectation; BLOCKED = proof needs a surface/data not available to this offline run; STATIC_ONLY = analyzer finding had no dynamic proof intent.")
    (out_dir / "proof_report.md").write_text("\n".join(lines) + "\n", encoding="utf-8")
    write_json(out_dir / "proof_report.json", report)


def main() -> int:
    ap = argparse.ArgumentParser(description="Generate and run offline emulator proof tests from analyzer proof packs")
    ap.add_argument("--proof-pack", required=True, help="hlds-analyzer-proof-pack JSON/JSONC emitted by analyzer")
    ap.add_argument("--session-profile", default=None, help="session profile generated by hlds_session_builder.py")
    ap.add_argument("--device-profile", default=None, help="device profile generated by analyzer chain")
    ap.add_argument("--media-profile", default=None, help="media profile / XDVD sidecar generated by dumper/media tooling")
    ap.add_argument("--firmware-image", default=None)
    ap.add_argument("--iso", default=None)
    ap.add_argument("--log", default=None)
    ap.add_argument("--stem", default=None)
    ap.add_argument("--out-dir", default=None)
    ap.add_argument("--run-jsonl", action="store_true", help="run generated proof scripts offline through gdr_host_jsonl_bridge.py")
    ap.add_argument("--python", default=sys.executable)
    ap.add_argument("--jsonl-bridge", default="gdr_host_jsonl_bridge.py")
    ap.add_argument("--cwd", default=None)
    ap.add_argument("--read-map", default=None)
    ap.add_argument("--cpu-trace-csv", default=None, help="future CPU/MMIO trace CSV for firmware LBA transform proofs")
    ap.add_argument("--allow-bridge-model-lba-proof", action="store_true", help="allow LBA transform findings to run current bridge model probes and report MODEL_ONLY; never reports PROVEN")
    ap.add_argument("--include-static-only", action="store_true", help="include static-only findings in report instead of silently skipping")
    args = ap.parse_args()

    session, device, media, device_path, media_path = load_context(args)
    proof_pack = load_json_or_jsonc(args.proof_pack)
    validate_proof_pack(proof_pack)
    stem = safe_name(args.stem or proof_pack.get("proof_pack_id") or proof_pack.get("device_profile_id") or "hlds_offline_proofs")
    out_dir = Path(args.out_dir or (Path("emutests") / stem))
    scripts_dir = out_dir / "scripts"
    runs_dir = out_dir / "runs"
    out_dir.mkdir(parents=True, exist_ok=True)

    manifest: dict[str, Any] = {
        "format": "hlds-offline-proof-test-manifest",
        "version": 1,
        "stem": stem,
        "proof_pack": args.proof_pack,
        "session_profile": args.session_profile,
        "device_profile": args.device_profile or device_path,
        "media_profile": args.media_profile or media_path,
        "run_mode": "offline_jsonl",
        "findings": [],
    }
    report: dict[str, Any] = dict(manifest)
    report["findings"] = []

    for finding in proof_findings(proof_pack):
        fid = str(finding.get("finding_id") or finding.get("id") or f"finding_{len(manifest['findings']):03d}")
        ftype = str(finding.get("type") or "unknown")
        if is_lba_transform_finding(finding):
            manifest_entry, report_entry = handle_lba_transform_finding(args, finding, scripts_dir, runs_dir)
            manifest["findings"].append(manifest_entry)
            report["findings"].append(report_entry)
            continue

        rows, expectations, blocked = generate_finding_script(finding, media)
        entry: dict[str, Any] = {"finding_id": fid, "type": ftype, "confidence": finding.get("confidence"), "requests": len(rows)}
        if blocked:
            entry.update({"outcome": "BLOCKED", "notes": [blocked.get("reason", "blocked")]})
            manifest["findings"].append(entry)
            report["findings"].append(entry)
            continue
        if not rows:
            entry.update({"outcome": "STATIC_ONLY", "notes": ["no dynamic proof steps"]})
            if args.include_static_only:
                manifest["findings"].append(entry)
                report["findings"].append(entry)
            continue
        script_path = scripts_dir / f"{safe_name(fid)}.jsonl"
        write_jsonl(script_path, rows)
        entry.update({"script": str(script_path), "expectations": expectations})
        manifest["findings"].append(entry)

        if args.run_jsonl:
            rc, responses = run_finding(args, fid, script_path, runs_dir)
            response_by_tag = {str(r.get("tag")): r for r in responses}
            problems: list[str] = []
            for exp in expectations:
                tag = str(exp.get("tag"))
                row = response_by_tag.get(tag)
                if not row:
                    problems.append(f"missing response for tag {tag}")
                    continue
                ok, p = response_matches_expectation(row, exp, media, media_path)
                if not ok:
                    problems += [f"{tag}: {x}" for x in p]
            if rc not in (0, 2):
                problems.append(f"runner return code {rc}")
            outcome = "PROVEN" if not problems else "CONTRADICTED"
            r_entry = dict(entry)
            r_entry.update({"returncode": rc, "responses": len(responses), "outcome": outcome, "problems": problems})
            report["findings"].append(r_entry)
        else:
            gen_entry = dict(entry)
            gen_entry.update({"outcome": "GENERATED", "notes": ["not run; pass --run-jsonl to prove offline"]})
            report["findings"].append(gen_entry)

    write_json(out_dir / "manifest.json", manifest)
    write_proof_report(out_dir, report)
    print(f"[OK] wrote offline proof manifest: {out_dir / 'manifest.json'}")
    print(f"[OK] wrote offline proof report: {out_dir / 'proof_report.md'}")

    # Return nonzero only for tool/runtime failures, not analyzer contradictions.
    runner_failures = [f for f in report.get("findings") or [] if int(f.get("returncode") or 0) not in (0, 2)]
    return 1 if runner_failures else 0


if __name__ == "__main__":
    raise SystemExit(main())
