mirror of
https://github.com/saymrwulf/proof-aware-crypto-tooling-agent.git
synced 2026-09-03 19:53:43 +00:00
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=<temp dir> 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 <noreply@anthropic.com>
This commit is contained in:
parent
5b0158ecef
commit
e87f0e8b05
1 changed files with 15 additions and 3 deletions
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Reference in a new issue