fix: fail-closed certificate classification + record-scoped axiom parsing (review round 6)

R6-B1 (Claude, executed end-to-end): provenness was decided by a
WHOLE-OUTPUT 'no axioms' sentence, so an axiom-free certificate whose
line was entirely absent still scored proven+clean ([]==[]). The
reviewer drove a doctored 60-line output through the real gate and got
61/61 with domsep never audited. Classification is now extracted into
classify_certificates(): proven iff the certificate's OWN anchor was
parsed (axiom-free anchors populate []); absent certs are
unknown/failed + not_checked — never clean. This also fail-closes the
typo'd-future-cert case (R6-C2).

GPT §6: parse_axiom_output is now RECORD-scoped — anchors delimit
records, a cone bracket is accepted only inside its own record, missing
or truncated brackets yield MISSING (fail closed) instead of borrowing
the next certificate's bracket, and cones may wrap arbitrarily (the
old fixed 16-line window was a latent overflow for the 11-axiom
ed25519 apex cones on this estate). Anchor names are captured between
the exact quotes Lean prints.

Six new regression tests (absent-axiom-free-not-clean, missing-bracket
no-steal, truncated cone, >16-line wrap, duplicate anchor, interleaved
diagnostics). Suite: 114 passed / 0 failed.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

src/pacta/lean.py

@@ -296,16 +296,7 @@ def run_axiom_audit(
             return_code = 124
     logs.write_text(output, encoding="utf-8")
     parsed = parse_axiom_output(output, certificates)
-    cert_results: list[CertificateAxiomResult] = []
+    cert_results = classify_certificates(parsed, certificates, return_code, expected_for)
-    for cert in certificates:
-        observed = parsed.get(cert, [])
-        if return_code != 0 and not observed:
-            status = "failed"
-            axiom_status = "not_checked"
-        else:
-            status = "proven" if observed or _mentions_no_axioms(output) else "unknown"
-            axiom_status = "clean" if sorted(observed) == sorted(expected_for(cert)) else "dirty"
-        cert_results.append(CertificateAxiomResult(cert, status, axiom_status, observed, expected_for(cert)))
     return AxiomAuditResult(
         attempted=True,
         ok=return_code == 0 and all(cert.axiom_status == "clean" for cert in cert_results),
@@ -316,40 +307,79 @@ def run_axiom_audit(
     )
 
 
+# Anchor lines as Lean prints them: 'Name' depends on axioms: …  /
+# 'Name' does not depend on any axioms. The name is captured between the
+# first pair of quotes (an identifier that itself CONTAINS a quote, e.g.
+# Foo', would mis-capture — no such name exists on this estate; the old
+# substring matching was strictly worse).
+_AXIOM_ANCHOR = re.compile(r"'([^']+)'\s+(depends on axioms|does not depend on any axioms)")
+
+
 def parse_axiom_output(output: str, certificates: list[str]) -> dict[str, list[str]]:
-    results: dict[str, list[str]] = {}
+    """Record-scoped parsing (review round 6, GPT §6 / Claude R6-B).
+
+    The output is split into RECORDS: each anchor line starts one, the
+    next anchor line ends it. A cone bracket is accepted only inside its
+    own record; a record whose bracket is missing or truncated yields a
+    MISSING certificate (fail closed at the caller), never a bracket
+    borrowed from the next record. Cones may wrap arbitrarily many lines
+    (the ed25519 apex tiers carry 11 axioms — the old fixed 16-line
+    window was a latent overflow for them). Duplicate anchors: first one
+    wins, deterministically.
+    """
     lines = output.splitlines()
-    for cert in certificates:
+    anchors: list[tuple[int, str, bool]] = []  # (line index, name, axiom-free?)
-        # Anchor on the exact quoted name Lean prints ('X' depends on … /
-        # 'X' does not depend on any axioms). A bare substring match would
-        # let 'Foo' hit the line for 'Foo_bar' first.
-        needle = f"'{cert}'"
-        cert_results: list[str] | None = None
     for i, line in enumerate(lines):
-            if needle not in line:
+        m = _AXIOM_ANCHOR.search(line)
+        if m:
+            anchors.append((i, m.group(1), "does not depend" in m.group(2)))
+    wanted = set(certificates)
+    results: dict[str, list[str]] = {}
+    for k, (i, name, axiom_free) in enumerate(anchors):
+        if name not in wanted or name in results:
             continue
-            # Axiom-free certificates print a bracketless sentence. Decide
+        if axiom_free:
-            # on THIS line before opening any window: a window would reach
+            results[name] = []
-            # into the NEXT certificate's bracket and steal its cone (found
+            continue
-            # by the entry-13 rehearsal — the accumulator corpus is the
+        end = anchors[k + 1][0] if k + 1 < len(anchors) else len(lines)
-            # first subject with axiom-free certificates).
+        record = "\n".join(lines[i:end])
-            if _mentions_no_axioms(line):
+        bracket = re.search(r"\[([^\]]*)\]", record, re.DOTALL)
-                cert_results = []
-                break
-            # Lean wraps long axiom lists (the apex tiers carry 11 axioms)
-            # across many lines; take a window wide enough for the largest
-            # documented boundary and flatten it before matching, the same
-            # move the corpus' check scripts make (tr '\n' ' ').
-            window = "\n".join(lines[i : i + 16])
-            bracket = re.search(r"\[([^\]]*)\]", window, re.DOTALL)
         if bracket:
-                cert_results = [item.strip() for item in bracket.group(1).split(",") if item.strip()]
+            results[name] = [item.strip() for item in bracket.group(1).split(",") if item.strip()]
-                break
+        # else: no complete bracket before the next record — leave MISSING.
-        if cert_results is not None:
-            results[cert] = cert_results
     return results
 
 
+def classify_certificates(
+    parsed: dict[str, list[str]],
+    certificates: list[str],
+    return_code: int,
+    expected_for,
+) -> list[CertificateAxiomResult]:
+    """Fail-closed per-certificate classification (review round 6, R6-B1).
+
+    Provenness is decided by the certificate's OWN anchor having been
+    found (membership in `parsed` — which includes axiom-free certs as
+    []), never by a whole-output "no axioms" sentence: an ABSENT
+    axiom-free certificate previously scored proven+clean because some
+    OTHER certificate's bracketless sentence satisfied the global check
+    and [] == [] satisfied the cone comparison. Absent certificates are
+    never clean.
+    """
+    out: list[CertificateAxiomResult] = []
+    for cert in certificates:
+        if cert in parsed:
+            observed = parsed[cert]
+            status = "proven"
+            axiom_status = "clean" if sorted(observed) == sorted(expected_for(cert)) else "dirty"
+        else:
+            observed = []
+            status = "failed" if return_code != 0 else "unknown"
+            axiom_status = "not_checked"
+        out.append(CertificateAxiomResult(cert, status, axiom_status, observed, expected_for(cert)))
+    return out
+
+
 def _mentions_no_axioms(text: str) -> bool:
     lowered = text.lower()
     return "no axioms" in lowered or "does not depend on any axioms" in lowered

tests/test_lean.py

@@ -41,6 +41,79 @@ def test_parse_axiom_output_axiom_free_cert_does_not_steal_next_cone():
     assert parsed["LTLAcc.eq_dropLast_append_of_getLast?"] == ["propext"]
 
 
+def test_classify_absent_axiom_free_cert_is_not_clean():
+    # Regression (round-6 Claude R6-B1, executed end-to-end by the
+    # reviewer): domsep's line deleted from otherwise-pristine output
+    # still yielded 61/61 because a whole-output "no axioms" sentence +
+    # ([] == []) scored the ABSENT cert proven+clean. Provenness must be
+    # the cert's own anchor, i.e. membership in the parsed dict.
+    from pacta.lean import classify_certificates
+
+    output = (
+        "'LTLAcc.Hash' does not depend on any axioms\n"
+        "'LTLAcc.MTH' depends on axioms: [propext, LTLAcc.sha256, Quot.sound]\n"
+    )
+    certs = ["LTLAcc.Hash", "LTLAcc.domsep", "LTLAcc.MTH"]
+    parsed = parse_axiom_output(output, certs)
+    results = classify_certificates(parsed, certs, 0, lambda c: [])
+    by_name = {r.name: r for r in results}
+    assert by_name["LTLAcc.Hash"].status == "proven"
+    assert by_name["LTLAcc.domsep"].status == "unknown"
+    assert by_name["LTLAcc.domsep"].axiom_status == "not_checked"
+    assert not all(r.axiom_status == "clean" for r in results)
+
+
+def test_parse_missing_bracket_does_not_steal_next_record():
+    # GPT round-6 §6: a cone-bearing anchor with a MISSING bracket must
+    # not consume the next certificate's bracket.
+    output = (
+        "'A.a' depends on axioms:\n"
+        "'B.b' depends on axioms: [propext]\n"
+    )
+    parsed = parse_axiom_output(output, ["A.a", "B.b"])
+    assert "A.a" not in parsed
+    assert parsed["B.b"] == ["propext"]
+
+
+def test_parse_truncated_cone_is_missing():
+    output = "'A.a' depends on axioms: [propext, Classical.choice\n"
+    parsed = parse_axiom_output(output, ["A.a"])
+    assert "A.a" not in parsed
+
+
+def test_parse_long_wrapped_cone_beyond_old_window():
+    # The ed25519 apex tiers carry 11 axioms; the old fixed 16-line
+    # window was a latent overflow. Records now extend to the next
+    # anchor regardless of length.
+    items = [f"Ax{i}" for i in range(11)]
+    wrapped = "[\n" + ",\n".join(items) + "\n" * 10 + "]"
+    output = f"'A.a' depends on axioms: {wrapped}\n'B.b' does not depend on any axioms\n"
+    parsed = parse_axiom_output(output, ["A.a", "B.b"])
+    assert parsed["A.a"] == items
+    assert parsed["B.b"] == []
+
+
+def test_parse_duplicate_anchor_first_wins():
+    output = (
+        "'A.a' depends on axioms: [propext]\n"
+        "'A.a' depends on axioms: [Quot.sound]\n"
+    )
+    parsed = parse_axiom_output(output, ["A.a"])
+    assert parsed["A.a"] == ["propext"]
+
+
+def test_parse_interleaved_diagnostics_inside_record():
+    output = (
+        "'A.a' depends on axioms:\n"
+        "warning: something unrelated\n"
+        "[propext, Quot.sound]\n"
+        "'B.b' does not depend on any axioms\n"
+    )
+    parsed = parse_axiom_output(output, ["A.a", "B.b"])
+    assert parsed["A.a"] == ["propext", "Quot.sound"]
+    assert parsed["B.b"] == []
+
+
 def test_parse_axiom_output_exact_name_not_prefix():
     # 'LTLAcc.MTH' must not match the line for 'LTLAcc.MTH_single' even
     # when the latter comes first in the output.