mechanical-refactor-verify

1"""Verify a whole mechanical-refactor chain: classification, proofs, and a full report.2 3Every commit in ``base..branch`` must classify itself by carrying exactly one of the two4words ``mechanical_provable`` or ``non_mechanical_provable`` anywhere in its message (the5rest of the message format is free). Every ``mechanical_provable`` commit must ship a6proof script in the proof folder (``<proof>/repro_scripts/<sha-prefix>.py`` or a flat7``<proof>/<sha-prefix>.py``), and running the proof must PASS -- reproduce the commit8byte-for-byte. A ``non_mechanical_provable`` commit carries no machine proof and is left9to human review.10 11The run prints a markdown report, writes it into the proof folder (``chain_report.md``),12and exits 0 iff the whole chain verifies. Normative contract: spec-reproduction-cli.md.13 14    python3 mechanical_refactor_reproduction_cli.py \15        --base <base-commit> --branch <pr-branch-name> --proof path/to/proof/folder16"""17 18import argparse19import hashlib20import json21import re22import subprocess23import sys24from concurrent.futures import ThreadPoolExecutor25from dataclasses import dataclass, field26from pathlib import Path27 28_DEFAULT_JOBS = 329_PASSED_CACHE_FILENAME = "mechanical_refactor_passed_proofs.json"30_CACHED_PASS_DETAIL = "reused this machine's earlier PASS (--skip-passed)"31 32KIND_MECHANICAL = "mechanical_provable"33KIND_NON_MECHANICAL = "non_mechanical_provable"34 35VERDICT_PASS = "PASS"36VERDICT_FAIL = "FAIL"37VERDICT_MISSING_PROOF = "MISSING_PROOF"38VERDICT_AMBIGUOUS_PROOF = "AMBIGUOUS_PROOF"39VERDICT_HUMAN_REVIEW = "HUMAN_REVIEW"40VERDICT_UNCLASSIFIED = "UNCLASSIFIED"41VERDICT_AMBIGUOUS_KIND = "AMBIGUOUS_KIND"42 43_OK_VERDICTS = (VERDICT_PASS, VERDICT_HUMAN_REVIEW)44 45# The words are matched standalone: delimited by any non-[0-9A-Za-z_] character or the46# string boundary, so `non_mechanical_provable` never also counts as the bare word.47_KIND_WORD_RE = re.compile(48    r"(?<![0-9A-Za-z_])(non_)?mechanical_provable(?![0-9A-Za-z_])"49)50 51# The arbiter's verdict line (Repro.run / verify_mechanical_refactor both print `PASS:`).52_PASS_LINE_RE = re.compile(r"^PASS:", re.MULTILINE)53 54_MIN_PROOF_STEM_LEN = 755_REPORT_FILENAME = "chain_report.md"56_FAIL_OUTPUT_TAIL_LINES = 6057 58 59class ChainVerificationError(Exception):60    """A setup problem (bad refs, non-linear range, missing proof folder): exit code 2."""61 62 63@dataclass(frozen=True)64class CommitVerdict:65    sha: str66    subject: str67    kind: "str | None"68    verdict: str69    detail: str = ""70    cached: bool = False71 72    @property73    def ok(self) -> bool:74        return self.verdict in _OK_VERDICTS75 76 77@dataclass(frozen=True)78class _PendingProof:79    sha: str80    subject: str81    kind: str82    script: Path83 84 85@dataclass(frozen=True)86class ChainResult:87    base: str88    branch: str89    base_sha: str90    branch_sha: str91    proof_dir: Path92    verdicts: "list[CommitVerdict]" = field(default_factory=list)93 94    @property95    def passed(self) -> bool:96        return bool(self.verdicts) and all(v.ok for v in self.verdicts)97 98 99def main(argv: "list[str]") -> int:100    parser = argparse.ArgumentParser(101        description="Verify a whole mechanical-refactor chain against its proof folder."102    )103    parser.add_argument("--base", required=True, help="base commit of the chain")104    parser.add_argument("--branch", required=True, help="PR branch name (chain tip)")105    parser.add_argument("--proof", required=True, help="proof folder path")106    parser.add_argument("--repo-root", default=None, help="repo root (default: cwd's)")107    parser.add_argument(108        "--report",109        default=None,110        help=f"report file path (default: <proof>/{_REPORT_FILENAME})",111    )112    parser.add_argument(113        "--jobs",114        type=int,115        default=_DEFAULT_JOBS,116        help=f"max concurrent proof runs (default {_DEFAULT_JOBS})",117    )118    parser.add_argument(119        "--skip-passed",120        action="store_true",121        help="reuse this machine's earlier PASS verdicts for unchanged proofs",122    )123    args = parser.parse_args(argv)124 125    try:126        result = verify_chain(127            base=args.base,128            branch=args.branch,129            proof=Path(args.proof),130            repo_root=args.repo_root,131            jobs=args.jobs,132            skip_passed=args.skip_passed,133        )134    except ChainVerificationError as exc:135        print(f"error: {exc}", file=sys.stderr)136        return 2137 138    report = render_report(result)139    report_path = (140        Path(args.report) if args.report else result.proof_dir / _REPORT_FILENAME141    )142    report_path.write_text(report)143    print(report)144    print(f"report written to: {report_path}")145    return 0 if result.passed else 1146 147 148def verify_chain(149    *,150    base: str,151    branch: str,152    proof: Path,153    repo_root: "str | None" = None,154    jobs: int = _DEFAULT_JOBS,155    skip_passed: bool = False,156) -> ChainResult:157    """Classify every commit in ``base..branch`` and run every provable commit's proof.158 159    Classification and proof resolution are sequential (cheap); the proof runs execute160    concurrently, up to ``jobs`` at a time — safe because each proof works in its own161    throwaway worktree. The verdict list keeps chain order. With ``skip_passed``, a162    pending proof whose (sha, script hash, utils hash) triple this machine already ran to163    a PASS is reused instead of re-executed; every fresh PASS is recorded either way."""164    root = repo_root or _repo_root()165    if not proof.is_dir():166        raise ChainVerificationError(f"proof folder does not exist: {proof}")167    base_sha = _rev_parse(base, root)168    branch_sha = _rev_parse(branch, root)169    commits = _linear_commits(base_sha=base_sha, branch_sha=branch_sha, root=root)170 171    resolved: "list[CommitVerdict | _PendingProof]" = []172    for sha in commits:173        subject = _git_output(["log", "-1", "--format=%s", sha], root).strip()174        message = _git_output(["log", "-1", "--format=%B", sha], root)175        resolved.append(176            _resolve_commit(sha=sha, subject=subject, message=message, proof=proof)177        )178 179    cache_path = _passed_cache_path(root)180    cache = _load_passed_cache(cache_path)181    if skip_passed:182        resolved = [_reuse_cached_pass(item, cache=cache) for item in resolved]183 184    pending_by_sha = {185        item.sha: item for item in resolved if isinstance(item, _PendingProof)186    }187    verdicts: "list[CommitVerdict]" = _run_pending_proofs(188        resolved=resolved, root=root, jobs=jobs189    )190    _record_passes(191        cache=cache,192        cache_path=cache_path,193        verdicts=verdicts,194        pending_by_sha=pending_by_sha,195    )196    return ChainResult(197        base=base,198        branch=branch,199        base_sha=base_sha,200        branch_sha=branch_sha,201        proof_dir=proof,202        verdicts=verdicts,203    )204 205 206def render_report(result: ChainResult) -> str:207    """The full chain report as markdown: header, per-commit table, failure details."""208    n_mech = sum(1 for v in result.verdicts if v.kind == KIND_MECHANICAL)209    n_non_mech = sum(1 for v in result.verdicts if v.kind == KIND_NON_MECHANICAL)210    n_unclassified = sum(1 for v in result.verdicts if v.kind is None)211    n_pass = sum(1 for v in result.verdicts if v.verdict == VERDICT_PASS)212    n_cached = sum(1 for v in result.verdicts if v.cached)213 214    lines = [215        "# Mechanical refactor chain report",216        "",217        f"- base: `{result.base}` (`{result.base_sha[:12]}`)",218        f"- branch: `{result.branch}` (`{result.branch_sha[:12]}`)",219        f"- proof folder: `{result.proof_dir}`",220        f"- chain verdict: **{'PASS' if result.passed else 'FAIL'}**",221        f"- commits: {len(result.verdicts)} total — {n_mech} {KIND_MECHANICAL}, "222        f"{n_non_mech} {KIND_NON_MECHANICAL}, {n_unclassified} classification error(s)",223        f"- proofs: {n_pass}/{n_mech} PASS",224        *(225            [f"- reused from the passed-proof cache (--skip-passed): {n_cached}"]226            if n_cached227            else []228        ),229        "",230        "| # | commit | kind | verdict | subject |",231        "|---|--------|------|---------|---------|",232    ]233    for i, v in enumerate(result.verdicts, start=1):234        kind = v.kind or "?"235        subject = v.subject.replace("|", "\\|")236        lines.append(f"| {i} | `{v.sha[:9]}` | {kind} | {v.verdict} | {subject} |")237 238    failures = [v for v in result.verdicts if not v.ok]239    if failures:240        lines += ["", "## Failure details"]241        for v in failures:242            lines += [243                "",244                f"### `{v.sha[:9]}` — {v.verdict}",245                "",246                v.detail or "(no detail)",247            ]248    return "\n".join(lines) + "\n"249 250 251def _reuse_cached_pass(252    item: "CommitVerdict | _PendingProof", *, cache: dict253) -> "CommitVerdict | _PendingProof":254    """Turn a pending proof into a cached PASS verdict on an exact cache-key match."""255    if not isinstance(item, _PendingProof):256        return item257    if cache.get("passed", {}).get(item.sha) != _proof_cache_key(item.script):258        return item259    print(f"proof {item.sha[:9]}  {VERDICT_PASS} (cached)", flush=True)260    return CommitVerdict(261        sha=item.sha,262        subject=item.subject,263        kind=item.kind,264        verdict=VERDICT_PASS,265        detail=_CACHED_PASS_DETAIL,266        cached=True,267    )268 269 270def _record_passes(271    *,272    cache: dict,273    cache_path: Path,274    verdicts: "list[CommitVerdict]",275    pending_by_sha: "dict[str, _PendingProof]",276) -> None:277    """Record every freshly-run PASS into the cache (a FAIL is never recorded)."""278    fresh = [279        v280        for v in verdicts281        if v.verdict == VERDICT_PASS and not v.cached and v.sha in pending_by_sha282    ]283    if not fresh:284        return285    for v in fresh:286        cache.setdefault("passed", {})[v.sha] = _proof_cache_key(287            pending_by_sha[v.sha].script288        )289    try:290        cache_path.write_text(json.dumps(cache, indent=2, sort_keys=True) + "\n")291    except OSError as exc:292        print(f"note: could not write passed-proof cache {cache_path}: {exc}")293 294 295def _proof_cache_key(script: Path) -> "dict[str, str]":296    """The cache key parts beyond the sha: hashes of the script and its utils module."""297    utils_sha256 = ""298    for directory in (script.parent, script.parent.parent):299        utils = directory / "mechanical_refactor_reproduction_utils.py"300        if utils.is_file():301            utils_sha256 = hashlib.sha256(utils.read_bytes()).hexdigest()302            break303    return {304        "script_sha256": hashlib.sha256(script.read_bytes()).hexdigest(),305        "utils_sha256": utils_sha256,306    }307 308 309def _passed_cache_path(root: str) -> Path:310    common_dir = _git_output(["rev-parse", "--git-common-dir"], root).strip()311    common = Path(common_dir)312    if not common.is_absolute():313        common = Path(root) / common314    return common / _PASSED_CACHE_FILENAME315 316 317def _load_passed_cache(path: Path) -> dict:318    """The cache is best-effort: missing, corrupt, or unreadable means empty."""319    try:320        data = json.loads(path.read_text())321    except (OSError, ValueError):322        return {"passed": {}}323    if not isinstance(data, dict) or not isinstance(data.get("passed"), dict):324        return {"passed": {}}325    return data326 327 328def _run_pending_proofs(329    *, resolved: "list[CommitVerdict | _PendingProof]", root: str, jobs: int330) -> "list[CommitVerdict]":331    """Execute the pending proofs on a bounded thread pool; keep chain order."""332    pending = [333        (i, item) for i, item in enumerate(resolved) if isinstance(item, _PendingProof)334    ]335    finished: "dict[int, CommitVerdict]" = {}336    if pending:337        with ThreadPoolExecutor(max_workers=max(1, jobs)) as pool:338            futures = {339                i: pool.submit(_proof_verdict, item, root=root) for i, item in pending340            }341            for i, future in futures.items():342                finished[i] = future.result()343    return [344        finished[i] if isinstance(item, _PendingProof) else item345        for i, item in enumerate(resolved)346    ]347 348 349def _proof_verdict(pending: _PendingProof, *, root: str) -> CommitVerdict:350    passed, output = _run_proof(script=pending.script, root=root)351    if passed:352        verdict = CommitVerdict(353            sha=pending.sha,354            subject=pending.subject,355            kind=pending.kind,356            verdict=VERDICT_PASS,357            detail="",358        )359    else:360        tail = "\n".join(output.splitlines()[-_FAIL_OUTPUT_TAIL_LINES:])361        verdict = CommitVerdict(362            sha=pending.sha,363            subject=pending.subject,364            kind=pending.kind,365            verdict=VERDICT_FAIL,366            detail=(367                f"proof `{pending.script}` did not PASS; output tail:\n\n"368                f"```\n{tail}\n```"369            ),370        )371    print(f"proof {pending.sha[:9]}  {verdict.verdict}", flush=True)372    return verdict373 374 375def _resolve_commit(376    *, sha: str, subject: str, message: str, proof: Path377) -> "CommitVerdict | _PendingProof":378    kind, classification_error = _classify(message)379    if kind is None:380        return CommitVerdict(381            sha=sha,382            subject=subject,383            kind=None,384            verdict=classification_error,385            detail=(386                f"the commit message must contain exactly one of the words "387                f"`{KIND_MECHANICAL}` or `{KIND_NON_MECHANICAL}`"388            ),389        )390    if kind == KIND_NON_MECHANICAL:391        return CommitVerdict(392            sha=sha,393            subject=subject,394            kind=kind,395            verdict=VERDICT_HUMAN_REVIEW,396            detail="declared non_mechanical_provable: no machine proof, review by hand",397        )398 399    scripts = _find_proof_scripts(proof=proof, sha=sha)400    if not scripts:401        return CommitVerdict(402            sha=sha,403            subject=subject,404            kind=kind,405            verdict=VERDICT_MISSING_PROOF,406            detail=(407                f"no proof script found; searched `{proof / 'repro_scripts'}` and "408                f"`{proof}` for `<sha-prefix>.py` (>= {_MIN_PROOF_STEM_LEN} hex chars)"409            ),410        )411    if len(scripts) > 1:412        listing = ", ".join(f"`{p}`" for p in scripts)413        return CommitVerdict(414            sha=sha,415            subject=subject,416            kind=kind,417            verdict=VERDICT_AMBIGUOUS_PROOF,418            detail=f"multiple proof scripts match this commit: {listing}",419        )420 421    return _PendingProof(sha=sha, subject=subject, kind=kind, script=scripts[0])422 423 424def _classify(message: str) -> "tuple[str | None, str]":425    """The commit's declared kind, or (None, error-verdict) when the word rule is broken.426 427    Exactly one of the two words must appear (any number of times, but only one of the428    two): zero occurrences is UNCLASSIFIED, both words present is AMBIGUOUS_KIND."""429    kinds = {430        KIND_NON_MECHANICAL if match.group(1) else KIND_MECHANICAL431        for match in _KIND_WORD_RE.finditer(message)432    }433    if not kinds:434        return None, VERDICT_UNCLASSIFIED435    if len(kinds) > 1:436        return None, VERDICT_AMBIGUOUS_KIND437    return kinds.pop(), ""438 439 440def _find_proof_scripts(*, proof: Path, sha: str) -> "list[Path]":441    """Proof scripts naming this commit: a ``<sha-prefix>.py`` (lowercase hex, >= 7 chars)442    under ``<proof>/repro_scripts/`` or flat in ``<proof>/``."""443    found: "list[Path]" = []444    for directory in (proof / "repro_scripts", proof):445        if not directory.is_dir():446            continue447        for path in sorted(directory.glob("*.py")):448            stem = path.stem449            is_sha_prefix = (450                len(stem) >= _MIN_PROOF_STEM_LEN451                and all(c in "0123456789abcdef" for c in stem)452                and sha.startswith(stem)453            )454            if is_sha_prefix:455                found.append(path)456    return found457 458 459def _run_proof(*, script: Path, root: str) -> "tuple[bool, str]":460    """Run one proof script from the repo root. A PASS is exit code 0 AND the arbiter's461    ``PASS:`` verdict line on stdout (an old-style script that exits 0 with a residual is462    therefore still a FAIL)."""463    result = subprocess.run(464        [sys.executable, str(script.resolve())],465        cwd=root,466        capture_output=True,467        text=True,468    )469    output = result.stdout + result.stderr470    passed = result.returncode == 0 and bool(_PASS_LINE_RE.search(result.stdout))471    return passed, output472 473 474def _linear_commits(*, base_sha: str, branch_sha: str, root: str) -> "list[str]":475    if not _is_ancestor(base_sha=base_sha, branch_sha=branch_sha, root=root):476        raise ChainVerificationError(477            f"base {base_sha[:12]} is not an ancestor of branch {branch_sha[:12]}"478        )479    commits = _git_output(480        ["rev-list", "--reverse", f"{base_sha}..{branch_sha}"], root481    ).split()482    if not commits:483        raise ChainVerificationError(484            f"no commits in {base_sha[:12]}..{branch_sha[:12]}"485        )486    merges = [487        sha488        for sha in commits489        if len(_git_output(["rev-list", "--parents", "-n", "1", sha], root).split()) > 2490    ]491    if merges:492        listing = ", ".join(sha[:9] for sha in merges)493        raise ChainVerificationError(494            f"the chain must be linear, but it contains merge commit(s): {listing}"495        )496    return commits497 498 499def _is_ancestor(*, base_sha: str, branch_sha: str, root: str) -> bool:500    result = subprocess.run(501        ["git", "merge-base", "--is-ancestor", base_sha, branch_sha],502        cwd=root,503        capture_output=True,504    )505    return result.returncode == 0506 507 508def _rev_parse(ref: str, root: str) -> str:509    result = subprocess.run(510        ["git", "rev-parse", "--verify", f"{ref}^{{commit}}"],511        cwd=root,512        capture_output=True,513        text=True,514    )515    if result.returncode != 0:516        raise ChainVerificationError(f"cannot resolve {ref!r}: {result.stderr.strip()}")517    return result.stdout.strip()518 519 520def _git_output(args: "list[str]", root: str) -> str:521    result = subprocess.run(522        ["git", *args], cwd=root, capture_output=True, text=True, check=True523    )524    return result.stdout525 526 527def _repo_root() -> str:528    return subprocess.run(529        ["git", "rev-parse", "--show-toplevel"],530        capture_output=True,531        text=True,532        check=True,533    ).stdout.strip()534 535 536if __name__ == "__main__":537    sys.exit(main(sys.argv[1:]))538