saymrwulf/proof-aware-crypto-tooling-agent
1
0
Fork 0
mirror of https://github.com/saymrwulf/proof-aware-crypto-tooling-agent.git synced 2026-09-03 19:53:43 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Fix the two defects the first REAL provider run exposed (and honestly signed)

Browse source 
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:
mrwulf 2026-07-06 12:51:59 +02:00
parent 5b0158ecef
commit e87f0e8b05
1 changed files with 15 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
src/pacta/lean.py
View file

@ -270,7 +270,15 @@ def run_axiom_audit(
with tempfile.TemporaryDirectory(prefix="pacta-axioms-") as tmp: with tempfile.TemporaryDirectory(prefix="pacta-axioms-") as tmp:
audit_file = Path(tmp) / "AxiomAudit.lean" audit_file = Path(tmp) / "AxiomAudit.lean"
audit_file.write_text(f"{imports_text}\n\n{prints_text}\n", encoding="utf-8") 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: try:
completed = subprocess.run( completed = subprocess.run(
cmd, cmd,
@ -316,8 +324,12 @@ def parse_axiom_output(output: str, certificates: list[str]) -> dict[str, list[s
for i, line in enumerate(lines): for i, line in enumerate(lines):
if cert not in line: if cert not in line:
continue continue
window = "\n".join(lines[i : i + 4]) # Lean wraps long axiom lists (the apex tiers carry 11 axioms)
bracket = re.search(r"\[([^\]]*)\]", window) # 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: if bracket:
cert_results = [item.strip() for item in bracket.group(1).split(",") if item.strip()] cert_results = [item.strip() for item in bracket.group(1).split(",") if item.strip()]
break break