v7next F0: the transplant proof gains teeth the audit showed it lacked

The 15:03 audit proved a false-green: byte_identical was computed but never
gated ok (token equality is blind to inter-token whitespace - 'x  + y' and
'x + y' tokenize identically), and the verifier checked only the requested
symbols, so an extra top-level definition or an import-time side effect in a
leaf rode an ok=true proof. Now: (1) the byte round trip is MANDATORY per
symbol, failing with the first divergent offset; (2) every top-level node of
the leaf must be attributable - requested symbol, docstring, imports, the
handle def, or a deliberate leaf-owned assignment allowlist - anything else
fails named with its line. Four mutation tests pin exactly the classes the
audit named (whitespace edit, smuggled def, import-time side effect) plus the
allowlisted-preamble pass. 32 tests, exit 0 preserved and shown.

scripts/v7next_transplant.py

@@ -802,18 +802,82 @@ def verify_transplant(upstream_source: str, leaf_source: str, symbols: List[str]
             if not ok:
                 problems.append(why or "token mismatch")
             entry["byte_identical"] = recovered == up.text
+            if not entry["byte_identical"] and not problems:
+                # MANDATORY (audit 2026-08-30): token equality alone is blind to
+                # inter-token whitespace (`x  + y` == `x + y` as tokens). The
+                # round trip must reproduce the upstream span BYTE-exactly.
+                for k, (a, b) in enumerate(zip(recovered, up.text)):
+                    if a != b:
+                        problems.append(
+                            "inverse-normalized span is not byte-identical to "
+                            f"upstream (first divergence at offset {k}: "
+                            f"{recovered[k:k+20]!r} != {up.text[k:k+20]!r})")
+                        break
+                else:
+                    problems.append(
+                        "inverse-normalized span is not byte-identical to "
+                        "upstream (length differs: "
+                        f"{len(recovered)} != {len(up.text)})")
         entry["handle_reads"] = sorted({s.attr for s in sites})
         reads.update(s.attr for s in sites)
         if problems:
             entry["detail"] = "; ".join(problems)
             report["ok"] = False
-        elif not (entry["ast_equal"] and entry["tokens_equal"]):
+        elif not (entry["ast_equal"] and entry["tokens_equal"]
+                  and entry["byte_identical"]):
             report["ok"] = False
     report["handle_reads"] = sorted(reads)
     report["unread_declared"] = sorted(declared - reads)
+    _flag_undeclared_top_level(leaf_source, symbols, handle, report)
     return report
 
 
+_PREAMBLE_OK_ASSIGN_DEFAULT = frozenset({"log"})
+
+
+def _flag_undeclared_top_level(leaf_source: str, symbols: List[str], handle: str,
+                               report: Dict[str, Any],
+                               leaf_owned: Optional[Set[str]] = None) -> None:
+    """MANDATORY (audit 2026-08-30): a leaf must contain NOTHING at top level
+    beyond the verified symbol spans and a recognizable preamble — otherwise an
+    extra definition or an import-time side effect rides an ok=true proof.
+    Allowed outside the requested symbols: the module docstring, __future__ and
+    ordinary imports, the handle def itself, and simple assignments to
+    leaf-owned names (default: {'log'}; extend deliberately, never silently).
+    """
+    owned = set(leaf_owned or _PREAMBLE_OK_ASSIGN_DEFAULT) | {handle}
+    requested = set(symbols)
+    extras: List[str] = []
+    tree = ast.parse(leaf_source)
+    for idx, node in enumerate(tree.body):
+        if idx == 0 and isinstance(node, ast.Expr) and isinstance(
+                getattr(node, "value", None), ast.Constant) and isinstance(
+                node.value.value, str):
+            continue  # module docstring
+        if isinstance(node, (ast.Import, ast.ImportFrom)):
+            continue
+        if isinstance(node, (ast.FunctionDef, ast.AsyncFunctionDef, ast.ClassDef)):
+            if node.name in requested or node.name in owned:
+                continue
+            extras.append(f"{type(node).__name__} {node.name!r} (line {node.lineno})")
+            continue
+        if isinstance(node, (ast.Assign, ast.AnnAssign)):
+            targets = node.targets if isinstance(node, ast.Assign) else [node.target]
+            names = {t.id for t in targets if isinstance(t, ast.Name)}
+            if names and names <= (requested | owned):
+                continue
+            extras.append(f"assignment to {sorted(names) or '<complex target>'} "
+                          f"(line {node.lineno})")
+            continue
+        if isinstance(node, ast.If) and isinstance(node.test, ast.Name) \
+                and node.test.id == "TYPE_CHECKING":
+            continue
+        extras.append(f"{type(node).__name__} (line {node.lineno})")
+    report["undeclared_top_level"] = extras
+    if extras:
+        report["ok"] = False
+
+
 # ---------------------------------------------------------------------------
 # CLI
 

tests/test_v7next_transplant.py

@@ -556,3 +556,48 @@ def test_cli_emit_and_check_roundtrip(tmp_path):
     leaf.write_text(corrupted, encoding="utf-8")
     check = subprocess.run(check_argv, capture_output=True, text=True)
     assert check.returncode == 2
+
+
+# ---------------------------------------------------------------------------
+# Mutation tests (audit 2026-08-30): the proof must FAIL on what tokens miss.
+# ---------------------------------------------------------------------------
+
+_MUT_UP = "def f(a, b):\n    return a  +  b + PARENT\n"
+_MUT_LEAF_OK = "def f(a, b):\n    return a  +  b + _h().PARENT\n"
+
+
+def test_mutation_whitespace_change_fails_byte_proof():
+    """Inter-token whitespace edits are invisible to the token proof; the
+    mandatory byte round trip must catch them."""
+    from scripts.v7next_transplant import verify_transplant
+    leaf_ws = "def f(a, b):\n    return a + b + _h().PARENT\n"  # collapsed spaces
+    rep = verify_transplant(_MUT_UP, leaf_ws, ["f"], {"PARENT"}, "_h")
+    assert rep["ok"] is False
+    assert "byte-identical" in (rep["symbols"]["f"]["detail"] or "")
+    rep_ok = verify_transplant(_MUT_UP, _MUT_LEAF_OK, ["f"], {"PARENT"}, "_h")
+    assert rep_ok["ok"] is True and rep_ok["symbols"]["f"]["byte_identical"] is True
+
+
+def test_mutation_extra_top_level_def_fails():
+    leaf = _MUT_LEAF_OK + "\n\ndef smuggled():\n    return 1\n"
+    from scripts.v7next_transplant import verify_transplant
+    rep = verify_transplant(_MUT_UP, leaf, ["f"], {"PARENT"}, "_h")
+    assert rep["ok"] is False
+    assert any("smuggled" in e for e in rep["undeclared_top_level"])
+
+
+def test_mutation_import_time_side_effect_fails():
+    leaf = "import os\n" + _MUT_LEAF_OK + "\nprint('boom')\n"
+    from scripts.v7next_transplant import verify_transplant
+    rep = verify_transplant(_MUT_UP, leaf, ["f"], {"PARENT"}, "_h")
+    assert rep["ok"] is False
+    assert any("Expr" in e or "line" in e for e in rep["undeclared_top_level"])
+
+
+def test_preamble_allowlist_still_passes():
+    leaf = ('"""doc"""\nfrom __future__ import annotations\nimport os\n'
+            "log = None\n\ndef _h():\n    return os\n\n" + _MUT_LEAF_OK)
+    from scripts.v7next_transplant import verify_transplant
+    rep = verify_transplant(_MUT_UP, leaf, ["f"], {"PARENT"}, "_h")
+    assert rep["undeclared_top_level"] == []
+    assert rep["ok"] is True