harness/pybytecode_core/verify.py

#!/usr/bin/env python3
"""SELF-VERIFICATION — the check that lets the tool KNOW when it is right.

This is the measurement instrument behind the Phase-3 design proposal. It is NOT the product
(no CLI, no service, no retry loop is built here) -- it exists so the projected lift of a
best-of-k + verify loop can be grounded in a measured number instead of a guess.

THE KEY IDEA, and it is stronger than differential execution:

    RECOMPILE THE PREDICTION AND COMPARE THE BYTECODE TO THE ORIGINAL.

If `compile(predicted_source)` yields the same code object as the bytecode we were asked to
decompile, the prediction is CORRECT BY CONSTRUCTION -- it is a genuine inverse, not merely a
plausible one. This matters enormously for the product:

  * COVERAGE IS 100%. It needs no runnable environment, no fuzzing, no stubs, no imports. It works
    on framework-coupled code, on decorated code, on the 91% of real Python that neither the real
    nor the stubbed differential oracle can touch. The 5.43%/9% execution ceiling does not apply.
  * A POSITIVE IS A PROOF. Not evidence -- a proof. Identical code object => identical behaviour.
  * IT IS CHEAP AND DETERMINISTIC. One compile. Microseconds. No LLM judge, ever.

Its limit, stated honestly: it is STRICTER than semantic equivalence. A decompilation that is
correct but compiles differently (a `while` where the original had a `for`, a differently-ordered
but equivalent boolean) does NOT verify. So:

    verified   = PROVABLY correct    (sound; no false "verified")
    unverified = UNKNOWN, not wrong  (incomplete; false "unverified" is common)

That asymmetry is exactly the right one for a tool: it never lies about being right, and it is
honest about not knowing. Differential execution is then the SECOND-tier verifier that rescues the
semantically-equivalent-but-not-byte-identical cases where the code happens to be runnable.

NORMALISATION: we compare `disassemble_v2` of both code objects rather than the raw marshalled
bytes, because the latter embeds line numbers, filenames and a few interning artefacts that differ
without any semantic content.
"""
from __future__ import annotations
import argparse, json, re, sys, types
from pathlib import Path

sys.path.insert(0, str(Path(__file__).parent))
from rep import disassemble_v2  # noqa: E402


def strip_fences(text: str) -> str:
    m = re.search(r"```(?:python|py)?\s*\n(.*?)(?:```|\Z)", text, re.S)
    return (m.group(1) if m else text).strip()


def normalised_asm(src: str) -> str | None:
    """The offset-free, line-number-free disassembly of `src`. None if it does not compile."""
    try:
        return disassemble_v2(compile(src, "<v>", "exec"))
    except (SyntaxError, ValueError, RecursionError, MemoryError, TypeError):
        return None


UNORDERED_CONST = (set, frozenset)


def canon_const(c, depth: int = 0) -> str:
    """A CANONICAL, order-independent encoding of one non-code constant.

    This replaced a bare `repr(c)` on 2026-08-04, because `repr()` of a set/frozenset/dict follows
    the COMPILING PROCESS'S string hash seed, not anything about the program. That made the oracle
    NON-DETERMINISTIC on any input carrying such a constant: certifying the same 600 wild .pyc under
    PYTHONHASHSEED 0/1/2/3/4 gave 585/592/584/585/589 -- five different answers to one question.
    It was also the single largest cause of false rejection when verifying against a FOREIGN .pyc
    (13 of 15 failures on that corpus; in every case a set of EQUAL VALUES in a different order).

    Type tags are mandatory rather than cosmetic: without them `1`, `1.0` and `True` would collapse
    into one encoding, and those are behaviourally distinct. `repr()` is retained for scalars
    precisely because it already separates them, and keeps `-0.0` apart from `0.0`.

    LOSSLESS, and tested rather than asserted (see GATE-RESULT.md):
    mutation kill stayed 100% with 0 true survivors, false accepts stayed 0 across 2,190 effective
    mutants, all 18 blind-spot probes still behaved as required, and the published greedy scores were
    bit-identical before and after (335/400 CSN, 254/279 OOD).
    """
    if depth > 20:
        return "DEPTH"
    t = type(c).__name__
    if isinstance(c, UNORDERED_CONST):
        return f"{t}({','.join(sorted(canon_const(x, depth + 1) for x in c))})"
    if isinstance(c, dict):
        items = sorted(f"{canon_const(k, depth + 1)}:{canon_const(v, depth + 1)}"
                       for k, v in c.items())
        return f"dict({','.join(items)})"
    if isinstance(c, tuple):
        return f"tuple({','.join(canon_const(x, depth + 1) for x in c)})"
    if isinstance(c, list):
        return f"list({','.join(canon_const(x, depth + 1) for x in c)})"
    return f"{t}:{c!r}"


def code_fingerprint(co) -> tuple:
    """A STRUCTURAL fingerprint of the real code object — recursively, including the EXCEPTION TABLE.

    The verifier must NOT compare my textual disassembly. It did, and that made it UNSOUND: the
    v2.0 rep omitted the exception table's `end`, so a `try: A; B; C` and a `try: A ... else: B; C`
    rendered identically, and a behaviourally WRONG prediction was stamped VERIFIED (a false proof,
    caught at n=279). A proof of correctness must rest on the code object itself, not on my
    rendering of it -- otherwise every bug in the rendering silently becomes a bug in the proof.

    Constants are encoded by canon_const(), NOT by repr() -- see that function for why.
    """
    kids = tuple(code_fingerprint(c) for c in co.co_consts if isinstance(c, types.CodeType))
    consts = tuple(canon_const(c) for c in co.co_consts if not isinstance(c, types.CodeType))
    return (
        co.co_code,                 # the instruction bytes
        co.co_exceptiontable,       # <- the field whose omission caused the false proof
        consts, co.co_names, co.co_varnames, co.co_freevars, co.co_cellvars,
        co.co_argcount, co.co_posonlyargcount, co.co_kwonlyargcount, co.co_flags,
        kids,
    )


def compiles_to(src: str):
    try:
        return compile(src, "<v>", "exec")
    except (SyntaxError, ValueError, RecursionError, MemoryError, TypeError):
        return None


def verify(prediction: str, reference_src: str) -> tuple[bool, str]:
    """Does the prediction RECOMPILE to the SAME CODE OBJECT as the original?

    At inference the reference is the .pyc itself (we hold the real code object). Here, in
    measurement, we reconstruct it by compiling the reference source -- which yields exactly the
    code object the model was asked to invert.

    Compared STRUCTURALLY on the code object (instructions + EXCEPTION TABLE + consts + names +
    flags, recursively), never on my textual disassembly. See code_fingerprint().
    """
    src = strip_fences(prediction)
    if not src.strip():
        return False, "empty prediction"
    got = compiles_to(src)
    if got is None:
        return False, "prediction does not compile"
    want = compiles_to(reference_src)
    if want is None:
        return False, "REFERENCE does not compile — cannot verify"
    if code_fingerprint(got) == code_fingerprint(want):
        return True, "VERIFIED: recompiles to an identical code object (proof of correctness)"
    return False, "compiles, but to a different code object (unverified — may still be correct)"


def main() -> None:
    ap = argparse.ArgumentParser()
    ap.add_argument("--results", required=True, help="the --out json from grade_outputs.py")
    ap.add_argument("--out", required=True, help="PERSIST the verification report here")
    ap.add_argument("--label", default="")
    a = ap.parse_args()
    samples = json.loads(Path(a.results).read_text())["samples"]

    n = len(samples)
    vflag = [verify(s["got"], s["expected"])[0] for s in samples]
    verified = sum(vflag)
    behav = sum(1 for s in samples if s["verdict"]["pass"])
    # the interesting cell: verified is a PROOF, so it must never exceed behavioural truth
    verified_and_behav = sum(1 for s, v in zip(samples, vflag) if v and s["verdict"]["pass"])
    verified_but_failed = verified - verified_and_behav

    # a false proof is the one result that would sink the whole thesis, so name the offenders
    false_proofs = [{"i": s.get("i"), "note": s["verdict"].get("note", "")[:160],
                     "expected": s["expected"][:400], "got": s["got"][:400]}
                    for s, v in zip(samples, vflag) if v and not s["verdict"]["pass"]]

    rep = {
        "label": a.label,
        "results_file": a.results,
        "n": n,
        "behaviourally_correct": behav,
        "behaviourally_correct_pct": round(100 * behav / max(1, n), 1),
        "VERIFIED_by_recompile": verified,
        "VERIFIED_by_recompile_pct": round(100 * verified / max(1, n), 1),
        "verified_AND_behaviourally_correct": verified_and_behav,
        "VERIFIED_BUT_BEHAVIOURALLY_WRONG": verified_but_failed,
        "soundness_note": ("a recompile-verified prediction that FAILS differential execution would "
                           "mean the verifier is unsound. Expect exactly 0. Any non-zero is a bug."),
        "false_proof_cases": false_proofs,
        "unverified_but_correct": behav - verified_and_behav,
        "incompleteness_note": ("these are correct decompilations the recompile check cannot PROVE "
                                "(equivalent source, different bytecode). Differential execution is "
                                "the second-tier verifier that rescues them where code is runnable."),
    }
    print(json.dumps({k: v for k, v in rep.items() if k != "false_proof_cases"}, indent=2))
    Path(a.out).write_text(json.dumps(rep, indent=2))
    print(f"artifact -> {a.out}", file=sys.stderr)


if __name__ == "__main__":
    main()