From e87f0e8b057ddb78d7f6daac6526c350ea78ae1b Mon Sep 17 00:00:00 2001 From: mrwulf Date: Mon, 6 Jul 2026 12:51:59 +0200 Subject: [PATCH] Fix the two defects the first REAL provider run exposed (and honestly signed) The first live four-fork replay was a system success and a content failure: all 256 file compiles ran green under lean-guard, and the provider SIGNED ATTESTATIONS OF FAILURE rather than hiding that its audit phase broke - exactly the fail-closed behavior the design demands. Two defects, both mine: 1. Guarded axiom audits lost --root: the audit's temp .lean lives outside the toolchain root; guard mode now forwards --root= exactly as it does for repo files. 2. The cone parser was single-line: Lean wraps the apex tiers' 11-axiom boundaries across lines, so the four apex certificates parsed as empty/dirty. The parser now flattens a 16-line window (the same move the corpus' check scripts make) - unit-tested on a real wrapped transcript. Validated standalone against dalek's fresh oleans: 16/16 certificates proven with boundary-exact cones; the observed full-lift cone equals the documented dalek boundary axiom-for-axiom. 49/49 tests green. Co-Authored-By: Claude Fable 5 --- src/pacta/lean.py | 18 +++++++++++++++--- 1 file changed, 15 insertions(+), 3 deletions(-) diff --git a/src/pacta/lean.py b/src/pacta/lean.py index ecbe7d2..eca5936 100644 --- a/src/pacta/lean.py +++ b/src/pacta/lean.py @@ -270,7 +270,15 @@ def run_axiom_audit( with tempfile.TemporaryDirectory(prefix="pacta-axioms-") as tmp: audit_file = Path(tmp) / "AxiomAudit.lean" audit_file.write_text(f"{imports_text}\n\n{prints_text}\n", encoding="utf-8") - cmd = build_lean_invocation(audit_file, tools, use_lake_env=use_lake_env, lean_guard=lean_guard) + cmd = build_lean_invocation( + audit_file, + tools, + use_lake_env=use_lake_env, + lean_guard=lean_guard, + # the audit file lives in a temp dir outside the toolchain root; + # --root makes lean accept it (guard mode forwards the flag). + root_path=audit_file.parent, + ) try: completed = subprocess.run( cmd, @@ -316,8 +324,12 @@ def parse_axiom_output(output: str, certificates: list[str]) -> dict[str, list[s for i, line in enumerate(lines): if cert not in line: continue - window = "\n".join(lines[i : i + 4]) - bracket = re.search(r"\[([^\]]*)\]", window) + # 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()] break