diff --git a/telperion/src/telperion/cli.py b/telperion/src/telperion/cli.py index 9a7195ce4..b0b1fa04f 100644 --- a/telperion/src/telperion/cli.py +++ b/telperion/src/telperion/cli.py @@ -1507,17 +1507,100 @@ def cmd_mission_comparator_record(args) -> int: if not art.exists(): print(f"{slug}: artifact {node.proof.artifact!r} does not exist") return 1 - second = "nanoda" - if getattr(args, "lean_kernel_only", False): - second = "none: heavy_certificates" - elif node.heavy_certificates: + lean_only = bool(getattr(args, "lean_kernel_only", False)) + if not lean_only and node.heavy_certificates: print(f"{slug}: node declares heavy_certificates = true, so the judge config had " "enable_nanoda = false; pass --lean-kernel-only to record that honestly.") return 1 + + # Read the verdict out of the judge's own job log rather than trusting the arguments. + # The JOB, never the run's conclusion: pushing this record to the same pull request + # supersedes the run that validated the artifact, so the run can read "cancelled" while + # the judging job succeeded (cl/kwin, 2026-09-25). + from .missions.judge_log import check as _check_log + run_id = str(args.run_id).strip() + theorem = args.theorem.strip() + job_id = str(getattr(args, "job_id", "") or "").strip() + job_url = str(getattr(args, "job_url", "") or "").strip() + head_sha = str(getattr(args, "head_sha", "") or "").strip() + kernel_mode, log_check, head_check = "", "skipped", "skipped" + log_text = None + if getattr(args, "log", None): + log_text = Path(args.log).read_text(errors="replace") + log_check = "verified-offline" + # When `gh` is reachable the caller's --head-sha is not taken on trust either. + api_sha = _job_head_sha(job_id) if job_id else None + if api_sha and head_sha and not (api_sha == head_sha or api_sha.startswith(head_sha)): + print(f"{slug}: --head-sha {head_sha} is not the head of job {job_id}, which the " + f"API says is {api_sha}.") + return 1 + if not head_sha: + print(f"{slug}: --log needs --head-sha, the commit the judging job checked out, or " + "the artifact-at-that-commit check silently does not happen. Find it with " + f"`gh api repos///actions/jobs/ --jq .head_sha`.") + return 1 + elif not getattr(args, "no_verify", False): + found = _fetch_judge_job(run_id, slug) + if found is None: + print(f"{slug}: could not read the judge logs for run {run_id} (is `gh` installed and " + "authenticated?). Pass --log FILE with the job log and --head-sha, or " + "--no-verify to record without checking -- which the record will then say.") + return 1 + job, errs = found + if errs: + for e in errs: + print(f"{slug}: {e}") + return 1 + job_id, job_url, head_sha, log_text = job.job_id, job.job_url, job.head_sha, job.log + log_check = "verified" + if log_text is not None: + errs = _check_log(log_text, node=slug, theorem=theorem, run_id=run_id, + expect_lean_kernel_only=lean_only) + if errs: + for e in errs: + print(f"{slug}: {e}") + return 1 + from .missions.judge_log import parse_verdicts as _pv + kernel_mode = _pv(log_text)[slug].kernel + # The judge saw the artifact as of the job's own head commit, which is not necessarily + # the working tree. Hash the blob there and require it to match, so a PASS on an older + # version of the artifact cannot be cited for the current one. + at_head = _blob_sha256(head_sha, art) + if at_head is None: + _try_fetch(art, head_sha) # a PR head is normally fetchable + at_head = _blob_sha256(head_sha, art) + # Store the FULL 40-hex commit: a provenance field must not leave a verifier + # disambiguating an abbreviation years later. + head_sha = _full_sha(art, head_sha) or head_sha + here = sha256_file(art) + if at_head is None: + if not getattr(args, "allow_unresolved_head", False): + print(f"{slug}: cannot resolve {art.name} at the judged commit {head_sha[:9]} " + "even after fetching it, so nothing here confirms the judge saw THIS " + "version of the artifact. Fetch that commit, or pass " + "--allow-unresolved-head, which records head_check = \"unresolved\".") + return 1 + print(f"{slug}: NOTE recording with head_check = \"unresolved\": {art.name} could not " + f"be resolved at {head_sha[:9]}, so the hash below is the working tree's.") + head_check = "unresolved" + elif at_head != here: + print(f"{slug}: the judge saw {art.name} at {at_head[:16]}... but the working " + f"tree has {here[:16]}...; that PASS is for a different version of the " + "artifact and must not be recorded for this one.") + return 1 + else: + head_check = "matched" + else: + print(f"{slug}: WARNING --no-verify: recording without reading the judge log, so the " + "theorem name and the kernel mode are unchecked. The record says " + "log_check = \"skipped\".") + second = "none: heavy_certificates" if lean_only else "nanoda" rec = ComparatorRecord( - run_id=str(args.run_id).strip(), date=_date.today().isoformat(), - artifact_sha256=sha256_file(art), theorem=args.theorem.strip(), + run_id=run_id, date=_date.today().isoformat(), + artifact_sha256=sha256_file(art), theorem=theorem, run_url=(args.run_url or "").strip(), second_kernel=second, + job_id=job_id, job_url=job_url, kernel_mode=kernel_mode, + judged_head_sha=head_sha, log_check=log_check, head_check=head_check, ) new_node = _dc.replace(node, comparator=rec, updated=rec.date) save_node(new_node, camp_root / "nodes" / f"{slug}.toml") @@ -1526,6 +1609,143 @@ def cmd_mission_comparator_record(args) -> int: return 0 + + +def _fetch_judge_job(run_id: str, slug: str): + """((the job to cite), errors) for `slug` in this run, or None when `gh` cannot be used. + + Reads EVERY job of the run, not the first one that mentions the node: a job whose log we + could not download is not a job that said nothing, and a node judged by two shards could + pass in one and fail in the other. `judge_log.choose` applies those rules. + """ + import json + import subprocess + + from .missions.judge_log import JobVerdict, choose, failed_nodes, parse_verdicts + + def gh(*a): + r = _run_ok(["gh", *a], text=True) + return r.stdout if r is not None else None + + out = gh("api", f"repos/{_gh_repo()}/actions/runs/{run_id}/jobs?per_page=100") + if out is None: + return None + try: + jobs = json.loads(out).get("jobs", []) + except json.JSONDecodeError: + return None + seen = [] + for job in jobs: + log = gh("api", f"repos/{_gh_repo()}/actions/jobs/{job['id']}/logs") + jid = str(job["id"]) + if log is None: + seen.append(JobVerdict(jid, job.get("html_url", ""), str(job.get("head_sha", "")), + None, False, False)) + continue + v = parse_verdicts(log).get(slug) + failed = slug in failed_nodes(log) + if v is None and not failed: + continue # this shard simply did not judge the node + seen.append(JobVerdict(jid, job.get("html_url", ""), str(job.get("head_sha", "")), + v, failed, True, log)) + return choose(seen, slug) + + + + +def _run_ok(cmd, **kw): + """subprocess.run that returns None when the tool is absent or fails. + + A missing `gh` or `git` must surface as "cannot check", which callers turn into a clean + refusal; a traceback out of a provenance command helps nobody. + """ + import subprocess + + try: + r = subprocess.run(cmd, capture_output=True, **kw) + except (FileNotFoundError, OSError): + return None + return r if r.returncode == 0 else None + +def _full_sha(path: Path, commit: str): + """`commit` as a full 40-hex commit id in the artifact's repository, or None.""" + import subprocess + + if not commit: + return None + top = _run_ok(["git", "-C", str(path.resolve().parent), "rev-parse", "--show-toplevel"], + text=True) + if top is None: + return None + r = _run_ok(["git", "-C", top.stdout.strip(), "rev-parse", f"{commit}^{{commit}}"], text=True) + out = r.stdout.strip() if r is not None else "" + return out if len(out) == 40 else None + + +def _job_head_sha(job_id: str): + """The head commit GitHub reports for a job, or None when `gh` cannot answer.""" + import json + import subprocess + + r = _run_ok(["gh", "api", f"repos/{_gh_repo()}/actions/jobs/{job_id}"], text=True) + if r is None: + return None + try: + return str(json.loads(r.stdout).get("head_sha") or "") or None + except json.JSONDecodeError: + return None + +def _try_fetch(path: Path, commit: str) -> None: + """Best-effort `git fetch origin `, so an unfetched PR head stops being a dead end.""" + import subprocess + + if not commit: + return + top = _run_ok(["git", "-C", str(path.resolve().parent), "rev-parse", "--show-toplevel"], + text=True) + if top is None: + return + _run_ok(["git", "-C", top.stdout.strip(), "fetch", "--quiet", "origin", commit]) + + +def _gh_repo() -> str: + """owner/name of the origin remote, for the GitHub API.""" + import os + import re + import subprocess + + env = os.environ.get("GITHUB_REPOSITORY") + if env: + return env + r = _run_ok(["git", "remote", "get-url", "origin"], text=True) + m = re.search(r"github\.com[:/](?P[^/]+/[^/.]+)", (r.stdout if r else "") or "") + return m.group("repo") if m else "DrMurphyIsIn/Arda" + + + +def _blob_sha256(commit: str, path: Path): + """sha256 of `path` as of `commit`, or None when it cannot be resolved here.""" + import hashlib + import subprocess + + # Resolve the repository from the ARTIFACT's own location, not the process's cwd: the + # registry and the artifact can live in a different checkout than the one we run in + # (e.g. `mission --missions-root `), and a cwd-based lookup would then + # silently report "cannot check". + art = path.resolve() + top = _run_ok(["git", "-C", str(art.parent), "rev-parse", "--show-toplevel"], text=True) + if top is None: + return None + root = Path(top.stdout.strip()).resolve() + try: + rel = art.relative_to(root) + except ValueError: + return None + blob = _run_ok(["git", "-C", str(root), "cat-file", "blob", f"{commit}:{rel.as_posix()}"]) + if blob is None: + return None + return hashlib.sha256(blob.stdout).hexdigest() + def cmd_mission_verify(args) -> int: from .missions.verify import verify_campaign @@ -1536,7 +1756,8 @@ def cmd_mission_verify(args) -> int: seen_warnings: set[str] = set() for camp_root in roots: deep = getattr(args, "deep_lean", False) - report = verify_campaign(camp_root, deep_lean=deep) + report = verify_campaign(camp_root, deep_lean=deep, + strict_provenance=getattr(args, 'strict_provenance', False)) if report.errors: for e in report.errors: print(f"ERROR [{camp_root.name}]: {e}") @@ -1962,6 +2183,22 @@ def _wsopt(p): p.add_argument("--lean-kernel-only", action="store_true", dest="lean_kernel_only", help="the judge ran with enable_nanoda = false for this node " "(heavy_certificates = true); the record says so") + p.add_argument("--job-id", default=None, dest="job_id", + help="the shard job that printed the PASS line (found automatically when the " + "log is fetched; required with --log to make the record point at a job)") + p.add_argument("--job-url", default=None, dest="job_url") + p.add_argument("--log", default=None, + help="read the judge verdict from this file instead of fetching it (offline); " + "requires --head-sha") + p.add_argument("--head-sha", default=None, dest="head_sha", + help="the commit the judging job checked out (with --log); the artifact is " + "hashed at that commit and must match") + p.add_argument("--allow-unresolved-head", action="store_true", dest="allow_unresolved_head", + help="record even when the judged commit cannot be resolved here; the record " + "then says head_check = \"unresolved\"") + p.add_argument("--no-verify", action="store_true", dest="no_verify", + help="record WITHOUT reading the judge log: the theorem name and the kernel " + "mode are then unchecked. Last resort; say why in the commit message") p.set_defaults(mission_fn=cmd_mission_comparator_record) # ci-record SLUG [--campaign C] --workflow W --job J --run-id N [--head-sha S] [--conclusion C] @@ -1988,6 +2225,10 @@ def _wsopt(p): p.add_argument("campaign", nargs="?", default=None) p.add_argument("--deep-lean", action="store_true", dest="deep_lean", help="run lake build in lean/") + p.add_argument("--strict-provenance", action="store_true", dest="strict_provenance", + help="treat a weakly checked Comparator record (written with --no-verify, " + "from a supplied log, or without the artifact check at the judged " + "commit) as an ERROR rather than a warning") p.set_defaults(mission_fn=cmd_mission_verify) # graph [CAMPAIGN] diff --git a/telperion/src/telperion/missions/judge_log.py b/telperion/src/telperion/missions/judge_log.py new file mode 100644 index 000000000..bc2bce1ba --- /dev/null +++ b/telperion/src/telperion/missions/judge_log.py @@ -0,0 +1,156 @@ +"""Read the independent judge's verdict out of a CI job log. + +`mission comparator-record` used to take the run id, the theorem name and the kernel mode +on trust: it wrote whatever string it was handed, and nothing checked that the cited run +had actually passed on that node, let alone with that theorem. The convention ("the island +theorem's fully-qualified name, exactly as the PASS line prints it") lived only in reviewers' +heads. These functions turn it into a check. + +The judge prints one line per node: + + COMPARATOR PASS island=rvm_bridge node= theorem= run= kernel= + +with `kernel` either `nanoda` (both kernels replayed the export) or `lean-kernel-only` (the +node declares `heavy_certificates = true`, so only the Lean kernel and the axiom whitelist +ran). A failure prints `::error::COMPARATOR FAIL island=... node=... theorem=...`. + +Two details matter when reading a log: + +* The job log also contains the workflow's own `echo` of those templates, with the shell + variables unexpanded (`node=$slug`). Those are not verdicts and are skipped. +* Verdicts must be read from the JOB, never from the run's conclusion. Pushing the record + commit to the same pull request supersedes the run that validated the artifact, so the + run's overall conclusion can be `cancelled` while the shard that judged this node passed + (seen 2026-09-25 on cl/kwin: run 36169770951 cancelled, job 108204239961 successful). +""" +from __future__ import annotations + +import re +from dataclasses import dataclass +from typing import Dict, List, Optional + +#: `kernel=` values the judge is allowed to print, mapped to the second kernel that ran. +KERNEL_MODES = { + "nanoda": "nanoda", + "lean-kernel-only": "none: heavy_certificates", +} + +_PASS = re.compile( + r"COMPARATOR PASS\s+island=(?P\S+)\s+node=(?P\S+)\s+" + r"theorem=(?P\S+)\s+run=(?P\S+)\s+kernel=(?P\S+)") +_FAIL = re.compile(r"COMPARATOR FAIL\s+island=(?P\S+)\s+node=(?P\S+)") +_UNEXPANDED = re.compile(r"\$\{?[A-Za-z_]") + + +@dataclass(frozen=True) +class Verdict: + """One judged node, as the log states it.""" + island: str + node: str + theorem: str + run: str + kernel: str + + @property + def second_kernel(self) -> str: + """The `second_kernel` string this verdict implies, or "" for an unknown mode.""" + return KERNEL_MODES.get(self.kernel, "") + + +def parse_verdicts(text: str) -> Dict[str, Verdict]: + """Every PASS verdict in a job log, by node slug. Unexpanded templates are skipped.""" + out: Dict[str, Verdict] = {} + for line in text.splitlines(): + if _UNEXPANDED.search(line): + continue # the workflow echoing its own `echo "COMPARATOR PASS ... node=$slug ..."` + m = _PASS.search(line) + if m: + out[m.group("node")] = Verdict(m.group("island"), m.group("node"), + m.group("theorem"), m.group("run"), m.group("kernel")) + return out + + +def failed_nodes(text: str) -> List[str]: + """Nodes the log reports as FAIL (templates skipped).""" + return [m.group("node") for line in text.splitlines() + if not _UNEXPANDED.search(line) for m in [_FAIL.search(line)] if m] + + +def check(text: str, *, node: str, theorem: str, run_id: str = "", + expect_lean_kernel_only: Optional[bool] = None) -> List[str]: + """Problems with recording `node`/`theorem` against this log. Empty list means OK. + + `expect_lean_kernel_only` is what the caller believes (from the node's + `heavy_certificates` flag and the `--lean-kernel-only` switch); when given, the log must + agree, so a record can neither claim both kernels ran when only Lean did, nor the reverse. + """ + errs: List[str] = [] + if node in failed_nodes(text): + errs.append(f"the log reports COMPARATOR FAIL for {node}: a failing run must never be recorded") + verdicts = parse_verdicts(text) + v = verdicts.get(node) + if v is None: + others = ", ".join(sorted(verdicts)[:4]) or "none" + errs.append(f"no COMPARATOR PASS line for {node} in this log " + f"(nodes judged here: {others}) -- wrong run, wrong shard, or it never passed") + return errs + if v.theorem != theorem: + errs.append(f"the log says the judge asserted {v.theorem!r} for {node}, " + f"not {theorem!r}; record the theorem exactly as the PASS line prints it") + if run_id and v.run != str(run_id): + errs.append(f"the PASS line for {node} cites run {v.run}, not {run_id}") + if v.kernel not in KERNEL_MODES: + errs.append(f"unknown kernel mode {v.kernel!r} for {node}; expected one of " + f"{sorted(KERNEL_MODES)}") + elif expect_lean_kernel_only is not None: + lean_only = (v.kernel == "lean-kernel-only") + if lean_only and not expect_lean_kernel_only: + errs.append(f"the log says {node} was judged with kernel={v.kernel} (nanoda did NOT " + f"run), so the record must say so: pass --lean-kernel-only") + if expect_lean_kernel_only and not lean_only: + errs.append(f"--lean-kernel-only was given but the log says {node} was judged with " + f"kernel={v.kernel}, i.e. the second kernel DID run; drop the switch") + return errs + + +@dataclass(frozen=True) +class JobVerdict: + """What one shard job of a run says about a node.""" + job_id: str + job_url: str = "" + head_sha: str = "" + verdict: Optional[Verdict] = None + failed: bool = False + #: False when the job's log could not be downloaded. A job we could not read is not a + #: job that said nothing: it may be the one holding the FAIL. + readable: bool = True + #: The log itself, so the caller can re-check the chosen job without downloading it twice. + log: str = "" + + +def choose(jobs: List[JobVerdict], node: str): + """(the job to cite, errors). Scans EVERY job: silence from one is not consent. + + Refuses when any job reports the node as failed, when no job passed it, when two jobs + disagree about the theorem or the kernel mode (a shard-split change or a matrix bug could + judge one node twice), or when any job's log was unreadable -- that job could be the one + with the FAIL. + """ + errs: List[str] = [] + unreadable = [j.job_id for j in jobs if not j.readable] + if unreadable: + errs.append(f"could not read the log of job(s) {', '.join(unreadable)} in this run; one of " + "them may hold a FAIL for this node, so the run cannot be certified from here") + failed = [j.job_id for j in jobs if j.failed] + if failed: + errs.append(f"job(s) {', '.join(failed)} report COMPARATOR FAIL for {node}: " + "a failing run must never be recorded") + hits = [j for j in jobs if j.verdict is not None] + if not hits: + errs.append(f"no job in this run printed a COMPARATOR PASS for {node}") + return None, errs + shapes = {(j.verdict.theorem, j.verdict.kernel) for j in hits} + if len(shapes) > 1: + errs.append(f"{node} was judged by {len(hits)} jobs with disagreeing verdicts " + f"({sorted(shapes)}); refusing to pick one") + return (None if errs else hits[0]), errs diff --git a/telperion/src/telperion/missions/provenance.py b/telperion/src/telperion/missions/provenance.py index 6acd632f9..0c28a85cf 100644 --- a/telperion/src/telperion/missions/provenance.py +++ b/telperion/src/telperion/missions/provenance.py @@ -297,6 +297,9 @@ class ProvenanceRow: comparator_run: str # "" when no passing run is recorded comparator_stale: bool lean_kernel_only: bool + #: How the record was checked when written ("" for records predating the checks). + log_check: str + head_check: str has_grant: bool @property @@ -328,6 +331,8 @@ def provenance_rows(campaign) -> List[ProvenanceRow]: comparator_stale=bool(comparator_staleness(campaign.root, n)), lean_kernel_only=bool(n.comparator and n.comparator.second_kernel != "nanoda"), has_grant=n.grant is not None, + log_check=(n.comparator.log_check if n.comparator else ""), + head_check=(n.comparator.head_check if n.comparator else ""), )) return rows @@ -352,4 +357,27 @@ def render_provenance_report(campaign) -> str: for r in lko: lines.append(f" {r.slug:<48} comparator={r.comparator_run} Lean kernel only " "(heavy_certificates: nanoda not run)") + for r in covered: + weak = weak_record_reasons(r) + if weak: + lines.append(f" {r.slug:<48} comparator={r.comparator_run} " + f"WEAKLY CHECKED: {'; '.join(weak)}") return "\n".join(lines) + "\n" + + +#: A Comparator record whose own checks were skipped or could not complete. Not an error -- +#: the record may be perfectly true -- but it must never read like a fully checked one. +def weak_record_reasons(row) -> List[str]: + out = [] + if row.log_check == "skipped": + out.append("written with --no-verify, so no judge log confirmed the theorem or kernel") + elif row.log_check == "verified-offline": + out.append("verified against a supplied log file; the job id is the recorder's word") + if row.head_check == "unresolved": + out.append("the artifact could not be hashed at the judged commit, so only the grant " + "pins the artifact") + elif row.head_check == "skipped": + out.append("the artifact was not checked at the judged commit") + if row.comparator_run and not row.log_check and not row.head_check: + out.append("predates the record checks (no log_check/head_check)") + return out diff --git a/telperion/src/telperion/missions/schema.py b/telperion/src/telperion/missions/schema.py index b167bc784..80e633103 100644 --- a/telperion/src/telperion/missions/schema.py +++ b/telperion/src/telperion/missions/schema.py @@ -249,6 +249,30 @@ class ComparatorRecord: #: the Lean kernel replay and the axiom whitelist still ran). Surfaced by #: `mission provenance-report` as "Lean kernel only". second_kernel: str = "nanoda" + #: The shard JOB that printed the PASS line, and its url. A record pushed onto the same + #: pull request supersedes the run that validated the artifact (missions-comparator cancels + #: in-progress runs on pull_request), so the RUN's conclusion can be "cancelled" while the + #: judging job succeeded -- seen 2026-09-25 on cl/kwin. The job is what a verifier should + #: open, so record it. + job_id: str = "" + job_url: str = "" + #: The literal `kernel=` token from the PASS line ("nanoda" or "lean-kernel-only"), as + #: observed rather than inferred from the node's flag. `second_kernel` is its reading. + kernel_mode: str = "" + #: The commit the judging job checked out. Recorded so any later verifier can re-hash the + #: artifact blob at that commit without asking the API what the job's head was. + judged_head_sha: str = "" + #: How thoroughly this record was checked when written. A degraded check must leave a mark + #: in the RECORD, not only in the terminal of whoever ran the command: + #: log_check "verified" the judge's own job logs were read and agreed + #: "verified-offline" a supplied log file agreed; the job id is the caller's word + #: "skipped" --no-verify: nothing confirmed this record + #: head_check "matched" the artifact blob at `judged_head_sha` equals the recorded hash + #: "unresolved" that commit could not be resolved, so the hash is the + #: working tree's and only the grant still pins the artifact + #: "skipped" not attempted (--no-verify) + log_check: str = "" + head_check: str = "" def __post_init__(self): for f in ("run_id", "date", "artifact_sha256", "theorem", "second_kernel"): @@ -450,6 +474,10 @@ def _node_to_doc(node: Node) -> dict: doc["comparator"]["run_url"] = node.comparator.run_url if node.comparator.second_kernel != "nanoda": doc["comparator"]["second_kernel"] = node.comparator.second_kernel + for _f in ("job_id", "job_url", "kernel_mode", "judged_head_sha", "log_check", + "head_check"): + if getattr(node.comparator, _f): + doc["comparator"][_f] = getattr(node.comparator, _f) if node.ci_record is not None: c = node.ci_record doc["ci_record"] = { @@ -505,6 +533,10 @@ def _doc_to_node(doc: dict, path: Path) -> Node: artifact_sha256=c["artifact_sha256"], theorem=c["theorem"], run_url=c.get("run_url", ""), second_kernel=c.get("second_kernel", "nanoda"), + job_id=str(c.get("job_id", "")), job_url=c.get("job_url", ""), + kernel_mode=c.get("kernel_mode", ""), + judged_head_sha=c.get("judged_head_sha", ""), + log_check=c.get("log_check", ""), head_check=c.get("head_check", ""), ) ci_record = None if "ci_record" in doc: diff --git a/telperion/src/telperion/missions/verify.py b/telperion/src/telperion/missions/verify.py index 6fe56a699..2cc0a6c14 100644 --- a/telperion/src/telperion/missions/verify.py +++ b/telperion/src/telperion/missions/verify.py @@ -678,6 +678,7 @@ def verify_campaign( deep_lean: bool = False, runner: Optional[Callable] = None, universe=None, + strict_provenance: bool = False, ) -> VerifyReport: """Full invariant battery (read-only). Returns VerifyReport(errors, warnings, ok). @@ -799,6 +800,19 @@ def verify_campaign( stale = comparator_staleness(root, node) if stale: warnings.append(f"Node {sl!r}: {stale}") + # A Comparator record whose own checks were skipped or could not complete is not + # wrong, but it must not read like a fully checked one. `--strict-provenance` turns + # that into a failure, so a campaign can require fully checked records. + if node.comparator is not None: + from .provenance import ProvenanceRow, weak_record_reasons + row = ProvenanceRow( + campaign=root.name, slug=sl, status=node.status, independence="", + self_audit=False, comparator_run=node.comparator.run_id, + comparator_stale=bool(stale), lean_kernel_only=False, has_grant=True, + log_check=node.comparator.log_check, head_check=node.comparator.head_check) + for why in weak_record_reasons(row): + msg = f"Node {sl!r}: Comparator record is weakly checked -- {why}" + (errors if strict_provenance else warnings).append(msg) ci = required_ci_problem(root, node) if ci and node.status == "proved": errors.append(f"Node {sl!r}: status is 'proved' but it {ci}") diff --git a/telperion/tests/test_comparator_record_verify.py b/telperion/tests/test_comparator_record_verify.py new file mode 100644 index 000000000..3abbd9cb2 --- /dev/null +++ b/telperion/tests/test_comparator_record_verify.py @@ -0,0 +1,86 @@ +"""`_blob_sha256`: the artifact as the judge saw it, not as the working tree has it. + +A Comparator record pins `artifact_sha256`. Computing it from the working tree is only right +when the artifact has not moved since the judged commit, which is the common case but not a +guarantee: a PASS on an older version of the artifact must never be citable for the current +one. So `comparator-record` hashes the artifact blob at the judged job's own head commit and +requires the two to agree. + +These tests use a throwaway git repository, so they need neither network nor the real history. +""" +import hashlib +import shutil +import subprocess +from pathlib import Path + +import pytest + +_CLI_SRC = Path(__file__).resolve().parents[1] / "src" + + +@pytest.fixture(scope="module") +def blob_sha256(): + import sys + sys.path.insert(0, str(_CLI_SRC)) + from telperion.cli import _blob_sha256 + return _blob_sha256 + + +def _git(cwd, *args): + r = subprocess.run(["git", *args], cwd=cwd, capture_output=True, text=True) + assert r.returncode == 0, f"git {' '.join(args)} failed: {r.stderr}" + return r.stdout.strip() + + +@pytest.fixture +def repo(tmp_path): + if shutil.which("git") is None: # pragma: no cover + pytest.skip("git is not available") + d = tmp_path / "r" + (d / "lean").mkdir(parents=True) + _git(d, "init", "-q") + _git(d, "config", "user.email", "t@example.com") + _git(d, "config", "user.name", "t") + art = d / "lean" / "Artifact.lean" + art.write_text("theorem old : True := trivial\n") + _git(d, "add", "-A") + _git(d, "commit", "-q", "-m", "first") + return d, art, _git(d, "rev-parse", "HEAD") + + +def test_hashes_the_committed_blob(repo, blob_sha256): + d, art, sha = repo + want = hashlib.sha256(art.read_bytes()).hexdigest() + assert blob_sha256(sha, art) == want + + +def test_sees_the_judged_version_not_the_working_tree(repo, blob_sha256): + """The case the check exists for: the artifact changed after the judged commit.""" + d, art, sha = repo + committed = blob_sha256(sha, art) + art.write_text("theorem changed : True := trivial\n") + assert blob_sha256(sha, art) == committed, "must still hash the judged commit" + assert hashlib.sha256(art.read_bytes()).hexdigest() != committed, "fixture did not change" + + +def test_short_sha_resolves(repo, blob_sha256): + d, art, sha = repo + assert blob_sha256(sha[:9], art) == blob_sha256(sha, art) + + +def test_unknown_commit_is_none_not_an_exception(repo, blob_sha256): + """Unresolvable means "cannot check here", which the caller reports rather than failing.""" + d, art, _ = repo + assert blob_sha256("0" * 40, art) is None + + +def test_path_outside_the_repository_is_none(repo, blob_sha256, tmp_path): + d, _, sha = repo + outside = tmp_path / "elsewhere.lean" + outside.write_text("x\n") + assert blob_sha256(sha, outside) is None + + +def test_missing_path_in_that_commit_is_none(repo, blob_sha256): + d, _, sha = repo + assert blob_sha256(sha, d / "lean" / "NeverCommitted.lean") is None diff --git a/telperion/tests/test_judge_log.py b/telperion/tests/test_judge_log.py new file mode 100644 index 000000000..7eee531b8 --- /dev/null +++ b/telperion/tests/test_judge_log.py @@ -0,0 +1,148 @@ +"""Reading the independent judge's verdict out of a job log, and refusing to record a lie. + +`mission comparator-record` used to write whatever theorem name and kernel mode it was given. +Nothing checked that the cited run had judged that node at all, so the convention -- record +the island theorem exactly as the PASS line prints it -- was enforced only by reviewers +noticing. These tests pin the parser and the checks that replace that trust. +""" +import importlib.util +import sys +from pathlib import Path + +import pytest + +_SRC = Path(__file__).resolve().parents[1] / "src" / "telperion" / "missions" / "judge_log.py" +_spec = importlib.util.spec_from_file_location("judge_log", _SRC) +jl = importlib.util.module_from_spec(_spec) +# Register before exec: @dataclass resolves annotations through sys.modules[cls.__module__]. +sys.modules["judge_log"] = jl +_spec.loader.exec_module(jl) + +# A real shard log, trimmed: the workflow's own unexpanded echo of both templates, then +# verdicts for a heavy node (Lean kernel only) and an ordinary one (both kernels). +LOG = """ +2026-09-25T19:20:04Z [36;1m echo "COMPARATOR PASS island=rvm_bridge node=$slug theorem=$thm run=36169770951 kernel=$kernel"[0m +2026-09-25T19:20:04Z [36;1m echo "::error::COMPARATOR FAIL island=rvm_bridge node=$slug theorem=$thm"[0m +2026-09-25T20:05:11Z COMPARATOR PASS island=rvm_bridge node=MM_weil_positivity_prime_free_window theorem=weil_positivity_prime_free_window run=36169770951 kernel=lean-kernel-only +2026-09-25T20:05:12Z COMPARATOR PASS island=rvm_bridge node=RH_corridor_bound theorem=RvMBridge3.corridor_bound run=36169770951 kernel=nanoda +""" + +FAIL_LOG = LOG + ( + "2026-09-25T20:06:00Z ::error::COMPARATOR FAIL island=rvm_bridge " + "node=MM_weil_positivity_window_two_fifths theorem=weil_positivity_window_two_fifths\n") + +HEAVY = "MM_weil_positivity_prime_free_window" + + +def test_parses_both_verdicts_and_skips_the_unexpanded_templates(): + v = jl.parse_verdicts(LOG) + assert set(v) == {HEAVY, "RH_corridor_bound"}, "a template echo was read as a verdict" + assert v[HEAVY].theorem == "weil_positivity_prime_free_window" + assert v[HEAVY].kernel == "lean-kernel-only" + assert v[HEAVY].second_kernel == "none: heavy_certificates" + assert v["RH_corridor_bound"].second_kernel == "nanoda" + assert v[HEAVY].run == "36169770951" + + +def test_failed_nodes_skips_templates_too(): + assert jl.failed_nodes(LOG) == [] + assert jl.failed_nodes(FAIL_LOG) == ["MM_weil_positivity_window_two_fifths"] + + +def test_a_good_record_passes(): + assert jl.check(LOG, node=HEAVY, theorem="weil_positivity_prime_free_window", + run_id="36169770951", expect_lean_kernel_only=True) == [] + + +def test_wrong_theorem_is_refused(): + errs = jl.check(LOG, node=HEAVY, theorem="KWin_Bridge.weil_positivity_prime_free_window", + run_id="36169770951", expect_lean_kernel_only=True) + assert errs and "not" in errs[0] and "PASS line prints" in errs[0] + + +def test_node_absent_from_the_log_is_refused(): + errs = jl.check(LOG, node="MM_weil_positivity_window_two_fifths", + theorem="weil_positivity_window_two_fifths", run_id="36169770951") + assert errs and "no COMPARATOR PASS line" in errs[0] + assert "nodes judged here" in errs[0], "say which nodes the log does cover" + + +def test_a_failing_node_is_refused_even_though_others_passed(): + errs = jl.check(FAIL_LOG, node="MM_weil_positivity_window_two_fifths", + theorem="weil_positivity_window_two_fifths", run_id="36169770951") + assert any("COMPARATOR FAIL" in e for e in errs) + + +def test_wrong_run_id_is_refused(): + errs = jl.check(LOG, node=HEAVY, theorem="weil_positivity_prime_free_window", + run_id="99999999", expect_lean_kernel_only=True) + assert any("cites run 36169770951" in e for e in errs) + + +def test_claiming_both_kernels_when_only_lean_ran_is_refused(): + """The dangerous direction: a record that overstates what was checked.""" + errs = jl.check(LOG, node=HEAVY, theorem="weil_positivity_prime_free_window", + run_id="36169770951", expect_lean_kernel_only=False) + assert any("--lean-kernel-only" in e and "nanoda did NOT run" in e for e in errs) + + +def test_claiming_lean_only_when_nanoda_also_ran_is_refused(): + errs = jl.check(LOG, node="RH_corridor_bound", theorem="RvMBridge3.corridor_bound", + run_id="36169770951", expect_lean_kernel_only=True) + assert any("drop the switch" in e for e in errs) + + +def test_unknown_kernel_mode_is_refused(): + log = LOG.replace("kernel=lean-kernel-only", "kernel=something-new") + errs = jl.check(log, node=HEAVY, theorem="weil_positivity_prime_free_window") + assert any("unknown kernel mode" in e for e in errs) + + +def test_kernel_modes_cover_what_the_workflow_can_print(): + """If the judge learns a new mode, this test is the reminder to map it.""" + wf = Path(__file__).resolve().parents[2] / ".github" / "workflows" / "missions-comparator.yml" + text = wf.read_text() + for mode in jl.KERNEL_MODES: + assert mode in text, f"{mode} is mapped here but the workflow never prints it" + + +def _jv(job_id, **kw): + return jl.JobVerdict(job_id, **kw) + + +def test_choose_picks_the_job_that_judged_the_node(): + v = jl.parse_verdicts(LOG)[HEAVY] + job, errs = jl.choose([_jv("1"), _jv("2", verdict=v)], HEAVY) + assert errs == [] and job.job_id == "2" + + +def test_choose_refuses_when_another_job_failed_the_node(): + """A PASS in one shard must not paper over a FAIL in another.""" + v = jl.parse_verdicts(LOG)[HEAVY] + job, errs = jl.choose([_jv("1", verdict=v), _jv("2", failed=True)], HEAVY) + assert job is None and any("COMPARATOR FAIL" in e for e in errs) + + +def test_choose_refuses_when_a_log_could_not_be_read(): + """Silence from an unreadable job is not consent: it may hold the FAIL.""" + v = jl.parse_verdicts(LOG)[HEAVY] + job, errs = jl.choose([_jv("1", verdict=v), _jv("2", readable=False)], HEAVY) + assert job is None and any("could not read the log" in e for e in errs) + + +def test_choose_refuses_disagreeing_duplicate_verdicts(): + a = jl.parse_verdicts(LOG)[HEAVY] + b = jl.Verdict(a.island, a.node, a.theorem, a.run, "nanoda") + job, errs = jl.choose([_jv("1", verdict=a), _jv("2", verdict=b)], HEAVY) + assert job is None and any("disagreeing verdicts" in e for e in errs) + + +def test_choose_accepts_agreeing_duplicate_verdicts(): + v = jl.parse_verdicts(LOG)[HEAVY] + job, errs = jl.choose([_jv("1", verdict=v), _jv("2", verdict=v)], HEAVY) + assert errs == [] and job.job_id == "1" + + +def test_choose_refuses_when_no_job_passed_the_node(): + job, errs = jl.choose([_jv("1"), _jv("2")], HEAVY) + assert job is None and any("no job in this run" in e for e in errs) diff --git a/telperion/tests/test_missions_provenance.py b/telperion/tests/test_missions_provenance.py index c229dfd4f..c50a4fac8 100644 --- a/telperion/tests/test_missions_provenance.py +++ b/telperion/tests/test_missions_provenance.py @@ -327,8 +327,9 @@ def test_verify_warns_when_comparator_record_is_stale(tmp_path): stmt = "theorem v_cmp : 1 = 1" _open_with_proof(croot, "V_cmp", stmt, f"{stmt} := by rfl\n") grant_status(load_campaign(croot), "V_cmp", **GATE) + # --no-verify: this test is about staleness, not about reading a judge log. rc = _cli(mroot, "comparator-record", "V_cmp", "--campaign", "demo", - "--run-id", "12345", "--theorem", "v_cmp") + "--run-id", "12345", "--theorem", "v_cmp", "--no-verify") assert rc == 0 node = load_node(croot / "nodes" / "V_cmp.toml") assert node.comparator.run_id == "12345" @@ -452,9 +453,12 @@ def test_heavy_node_record_must_say_lean_kernel_only(tmp_path, capsys): assert "heavy_certificates" in capsys.readouterr().out assert load_node(croot / "nodes" / "HV_one.toml").comparator is None assert _cli(mroot, "comparator-record", "HV_one", "--campaign", "demo", - "--run-id", "9", "--theorem", "hv", "--lean-kernel-only") == 0 + "--run-id", "9", "--theorem", "hv", "--lean-kernel-only", "--no-verify") == 0 n = load_node(croot / "nodes" / "HV_one.toml") assert n.comparator.second_kernel == "none: heavy_certificates" + # --no-verify must leave a mark in the RECORD, not only in the terminal + assert n.comparator.log_check == "skipped" + assert 'log_check = "skipped"' in (croot / "nodes" / "HV_one.toml").read_text() assert 'second_kernel = "none: heavy_certificates"' in (croot / "nodes" / "HV_one.toml").read_text() assert n.heavy_certificates is True capsys.readouterr() @@ -524,7 +528,7 @@ def test_provenance_report_lists_unverified_and_self_audits_only_when_proved(tmp _open_with_proof(croot, "R_cmp", stmt3, f"{stmt3} := by rfl\n") grant_status(load_campaign(croot), "R_cmp", **GATE) assert _cli(mroot, "comparator-record", "R_cmp", "--campaign", "demo", - "--run-id", "777", "--theorem", "r_cmp") == 0 + "--run-id", "777", "--theorem", "r_cmp", "--no-verify") == 0 prov.migrate_unverified(croot) capsys.readouterr() @@ -621,3 +625,38 @@ def test_live_registry_every_readback_is_labelled_and_no_grant_digest_is_stale() f"{camp_dir.name}/{sl}: read-back has no independence label (run provenance-migrate)" assert not prov.readback_is_self_audit(node), f"{camp_dir.name}/{sl} is a self-audit" assert prov.grant_digest_errors(camp_dir, node) == [], f"{camp_dir.name}/{sl}" + + +def test_comparator_record_refuses_rather_than_skipping_the_check_silently(tmp_path, capsys, + monkeypatch): + """Without a log and without --no-verify, the command must NOT quietly record. + + The whole point of the checks is that a record nobody verified cannot look like one that + was verified, so an unusable `gh` has to be a refusal, not a silent pass. + """ + mroot, croot = _demo(tmp_path) + stmt = "theorem n_cmp : 5 = 5" + _open_with_proof(croot, "N_cmp", stmt, f"{stmt} := by rfl\n") + grant_status(load_campaign(croot), "N_cmp", **GATE) + monkeypatch.setenv("PATH", str(tmp_path)) # no `gh` on PATH + rc = _cli(mroot, "comparator-record", "N_cmp", "--campaign", "demo", + "--run-id", "42", "--theorem", "n_cmp") + assert rc == 1 + out = capsys.readouterr().out + assert "--no-verify" in out and "could not read the judge logs" in out + assert load_node(croot / "nodes" / "N_cmp.toml").comparator is None + + +def test_log_path_requires_the_judged_commit(tmp_path, capsys): + """--log without --head-sha used to skip the artifact check with no message at all.""" + mroot, croot = _demo(tmp_path) + stmt = "theorem l_cmp : 6 = 6" + _open_with_proof(croot, "L_cmp", stmt, f"{stmt} := by rfl\n") + grant_status(load_campaign(croot), "L_cmp", **GATE) + log = tmp_path / "job.log" + log.write_text("COMPARATOR PASS island=demo node=L_cmp theorem=l_cmp run=42 kernel=nanoda\n") + rc = _cli(mroot, "comparator-record", "L_cmp", "--campaign", "demo", + "--run-id", "42", "--theorem", "l_cmp", "--log", str(log)) + assert rc == 1 + assert "--head-sha" in capsys.readouterr().out + assert load_node(croot / "nodes" / "L_cmp.toml").comparator is None diff --git a/telperion/tests/test_weak_comparator_records.py b/telperion/tests/test_weak_comparator_records.py new file mode 100644 index 000000000..668a41062 --- /dev/null +++ b/telperion/tests/test_weak_comparator_records.py @@ -0,0 +1,81 @@ +"""A Comparator record must say how thoroughly it was checked, and that must be visible. + +`comparator-record` can write a record under a weaker check than the full one: with +`--no-verify` (nothing read the judge log), from a supplied log file (the job id is the +recorder's word), or without hashing the artifact at the judged commit (that commit could +not be resolved). Those records may be perfectly true, but they must never read like a +fully checked one, so `provenance-report` lists them and `mission verify` warns -- or fails +under `--strict-provenance`. + +Records written before the checks existed carry neither field, and are flagged as such +rather than assumed good. +""" +import importlib.util +import sys +from pathlib import Path + +import pytest + +_SRC = Path(__file__).resolve().parents[1] / "src" +sys.path.insert(0, str(_SRC)) + + +def _load(): + spec = importlib.util.spec_from_file_location( + "prov", _SRC / "telperion" / "missions" / "provenance.py") + m = importlib.util.module_from_spec(spec) + sys.modules["prov"] = m + try: + spec.loader.exec_module(m) + except ImportError as exc: # pragma: no cover - relative imports need the package + pytest.skip(f"provenance.py needs its package: {exc}") + return m + + +prov = pytest.importorskip("telperion.missions.provenance") + + +def _row(**kw): + base = dict(campaign="c", slug="N", status="proved", independence="unverified", + self_audit=False, comparator_run="1", comparator_stale=False, + lean_kernel_only=False, has_grant=True, log_check="verified", + head_check="matched") + base.update(kw) + return prov.ProvenanceRow(**base) + + +def test_a_fully_checked_record_is_not_flagged(): + assert prov.weak_record_reasons(_row()) == [] + + +def test_no_verify_is_flagged(): + why = prov.weak_record_reasons(_row(log_check="skipped", head_check="skipped")) + assert any("--no-verify" in w for w in why) + assert any("not checked at the judged commit" in w for w in why) + + +def test_offline_verification_is_flagged_as_the_recorders_word(): + why = prov.weak_record_reasons(_row(log_check="verified-offline")) + assert why and "recorder's word" in why[0] + + +def test_unresolved_head_is_flagged(): + why = prov.weak_record_reasons(_row(head_check="unresolved")) + assert any("only the grant" in w for w in why) + + +def test_a_record_predating_the_checks_is_flagged_not_assumed_good(): + why = prov.weak_record_reasons(_row(log_check="", head_check="")) + assert why == ["predates the record checks (no log_check/head_check)"] + + +def test_a_node_without_a_comparator_record_is_not_flagged_here(): + """Absence of a record is the job of the `flagged` property, not of this check.""" + assert prov.weak_record_reasons(_row(comparator_run="", log_check="", head_check="")) == [] + + +def test_report_lists_weak_records(tmp_path): + """The reasons reach the rendered report, not just the data structure.""" + rows = [_row(slug="Weak", log_check="skipped", head_check="skipped")] + line = "; ".join(prov.weak_record_reasons(rows[0])) + assert "no judge log confirmed" in line