From 5b0158ecefa7f0f8832879fea3d3ed768b6c276a Mon Sep 17 00:00:00 2001 From: mrwulf Date: Mon, 6 Jul 2026 10:42:59 +0200 Subject: [PATCH] Machine protection: route all pacta Lean compiles through lean-guard pacta's replay invoked `lake env lean` bare - on the reference machine that is exactly the pattern that once OOM-crashed the host (see the corpus' POSTMORTEM). New RepoConfig.lean_guard (set for all five repos in examples/repos.yaml: verification/lean-guard): when configured, every compile and axiom audit runs `lake env --root=...` instead of bare lean - hard memory cap via systemd scope + lean -M, core pinning, timeout, single-flight lock, free-RAM preflight with the Guard-3a retry ladder, all tuned via LEAN_MEM_MB / LEAN_MIN_FREE_MB / LEAN_MEM_WAIT_SEC / LEAN_TIMEOUT / LEAN_MAX_CORES. Provider attestations now record a machine_protection block naming the guard (or "UNGUARDED"). Smoke-tested live on the real dalek repo: clamping trace visible, compile green. 49/49 tests green. Co-Authored-By: Claude Fable 5 --- examples/repos.yaml | 5 +++++ provider/src/pacta_provider/service.py | 9 ++++++++- src/pacta/cli.py | 8 +++++++- src/pacta/config.py | 2 ++ src/pacta/lean.py | 21 ++++++++++++++++++++- src/pacta/repo.py | 11 +++++++++++ 6 files changed, 53 insertions(+), 3 deletions(-) diff --git a/examples/repos.yaml b/examples/repos.yaml index ddc0830..f59a6a1 100644 --- a/examples/repos.yaml +++ b/examples/repos.yaml @@ -7,6 +7,7 @@ repos: apex_boundary: dalek-wrappers env_script: ~/aeneas-toolchain/env.sh lean_project_dir: $AENEAS_HOME/backends/lean + lean_guard: verification/lean-guard known_exclusions: - SHA-512 implementation (opaque oracle in the apex theorems) - wire parser/filter byte-level specs (hypothesis-parametric) @@ -23,6 +24,7 @@ repos: apex_boundary: anza env_script: ~/aeneas-toolchain/env.sh lean_project_dir: $AENEAS_HOME/backends/lean + lean_guard: verification/lean-guard backend_warning: verified entry point is verify_sha512 = verify_dalek (canonical-R incl. legacy filters); the crate's default HEEA/Zebra verify() is a DIFFERENT acceptance criterion and is not covered known_exclusions: - Solana runtime semantics @@ -38,6 +40,7 @@ repos: apex_boundary: hash3 env_script: ~/aeneas-toolchain/env.sh lean_project_dir: $AENEAS_HOME/backends/lean + lean_guard: verification/lean-guard backend_warning: pure Rust path only; do not treat zkVM accelerator/syscall path as verified - name: betrusted-ed25519-verified @@ -48,6 +51,7 @@ repos: apex_boundary: hash3 env_script: ~/aeneas-toolchain/env.sh lean_project_dir: $AENEAS_HOME/backends/lean + lean_guard: verification/lean-guard backend_warning: pure Rust path only; do not treat Engine25519/hardware accelerator as verified - name: pasta-pallas-verified @@ -56,6 +60,7 @@ repos: verification_dir: verification env_script: ~/aeneas-toolchain/env.sh lean_project_dir: $AENEAS_HOME/backends/lean + lean_guard: verification/lean-guard known_status: foundation only unless aggregate field certificate is present known_exclusions: - full fieldImplementation certificate unless present and axiom-clean diff --git a/provider/src/pacta_provider/service.py b/provider/src/pacta_provider/service.py index 265089a..e940d51 100644 --- a/provider/src/pacta_provider/service.py +++ b/provider/src/pacta_provider/service.py @@ -11,7 +11,7 @@ from pacta.config import RepoConfig from pacta.lean import LeanCheckResult, build_lean_env, detect_tools, lean_check_files, resolve_lean_project_dir, run_axiom_audit from pacta.manifest import discover_layout from pacta.profiles import get_profile -from pacta.repo import git_commit +from pacta.repo import git_commit, resolve_lean_guard from pacta.signing import sign_attestation @@ -29,6 +29,7 @@ def build_attestation( path = Path(repo_path) profile = get_profile(repo.kind, repo) layout = discover_layout(path, repo.verification_dir) + lean_guard = resolve_lean_guard(repo.lean_guard, path) check = lean_check_files( layout.compile_order, layout.verification_dir, @@ -36,6 +37,7 @@ def build_attestation( log_dir=log_dir, env_script=env_script or repo.env_script, lean_project_dir=lean_project_dir or repo.lean_project_dir, + lean_guard=lean_guard, ) axiom = None if check.attempted and check.ok: @@ -49,6 +51,7 @@ def build_attestation( env_script=env_script or repo.env_script, lean_project_dir=lean_project_dir or repo.lean_project_dir, certificate_axioms=profile.certificate_axioms, + lean_guard=lean_guard, ) certs = [ { @@ -72,6 +75,10 @@ def build_attestation( "schema_version": 1, "provider": provider, "issued_at": datetime.now(timezone.utc).replace(microsecond=0).isoformat().replace("+00:00", "Z"), + "machine_protection": { + "lean_guard": lean_guard or "UNGUARDED", + "note": "All Lean compiles route through the repo's lean-guard (memory cap, core pinning, timeout, single-flight lock) when configured.", + }, "subject": { "component": repo.name, "repo_url": repo.url, diff --git a/src/pacta/cli.py b/src/pacta/cli.py index 3754c5b..e427f77 100644 --- a/src/pacta/cli.py +++ b/src/pacta/cli.py @@ -21,7 +21,7 @@ from .lean import ( ) from .manifest import discover_layout from .profiles import get_profile -from .repo import clone_or_fetch, status_for +from .repo import clone_or_fetch, status_for, resolve_lean_guard from .report import render_markdown from .risk import score_claim_card from .sthstore import check_sth_against_store, check_sth_freshness @@ -276,6 +276,7 @@ def cmd_axioms(args: argparse.Namespace) -> int: log_dir=args.log_dir, env_script=env_script, lean_project_dir=lean_project_dir, + lean_guard=resolve_lean_guard(repo.lean_guard, args.repo), ) if check_result.log_path: print(f"check log: {check_result.log_path}") @@ -294,6 +295,7 @@ def cmd_axioms(args: argparse.Namespace) -> int: env_script=env_script, lean_project_dir=lean_project_dir, certificate_axioms=profile.certificate_axioms, + lean_guard=resolve_lean_guard(repo.lean_guard, args.repo), ) for cert in result.certificates: print(f"{cert.name}: {cert.status}, axioms={cert.axiom_status}, observed={cert.observed_axioms}") @@ -326,6 +328,7 @@ def cmd_claims(args: argparse.Namespace) -> int: log_dir=args.log_dir, env_script=env_script, lean_project_dir=lean_project_dir, + lean_guard=resolve_lean_guard(repo.lean_guard, local_path), ) axiom_result = run_axiom_audit( local_path / repo.verification_dir, @@ -337,6 +340,7 @@ def cmd_claims(args: argparse.Namespace) -> int: env_script=env_script, lean_project_dir=lean_project_dir, certificate_axioms=profile.certificate_axioms, + lean_guard=resolve_lean_guard(repo.lean_guard, local_path), ) attestation = _attestation_for_args(args, repo) card = build_claim_card( @@ -542,6 +546,7 @@ def _card_for_agent(args: argparse.Namespace) -> dict[str, Any]: log_dir=args.log_dir, env_script=env_script, lean_project_dir=lean_project_dir, + lean_guard=resolve_lean_guard(repo.lean_guard, local_path), ) axiom_result = run_axiom_audit( local_path / repo.verification_dir, @@ -553,6 +558,7 @@ def _card_for_agent(args: argparse.Namespace) -> dict[str, Any]: env_script=env_script, lean_project_dir=lean_project_dir, certificate_axioms=profile.certificate_axioms, + lean_guard=resolve_lean_guard(repo.lean_guard, local_path), ) attestation = _attestation_for_args(args, repo) return build_claim_card( diff --git a/src/pacta/config.py b/src/pacta/config.py index e90c1d6..a531c1f 100644 --- a/src/pacta/config.py +++ b/src/pacta/config.py @@ -27,6 +27,7 @@ class RepoConfig: certificate_axioms: dict[str, list[str]] = field(default_factory=dict) env_script: str | None = None lean_project_dir: str | None = None + lean_guard: str | None = None @classmethod def from_dict(cls, raw: dict[str, Any]) -> "RepoConfig": @@ -51,6 +52,7 @@ class RepoConfig: }, env_script=raw.get("env_script"), lean_project_dir=raw.get("lean_project_dir"), + lean_guard=raw.get("lean_guard"), ) diff --git a/src/pacta/lean.py b/src/pacta/lean.py index e1fd0b0..ecbe7d2 100644 --- a/src/pacta/lean.py +++ b/src/pacta/lean.py @@ -99,7 +99,23 @@ def build_lean_invocation( use_lake_env: bool = False, output_path: str | Path | None = None, root_path: str | Path | None = None, + lean_guard: str | Path | None = None, ) -> list[str]: + if lean_guard: + # MACHINE PROTECTION: route the compile through the repo's lean-guard + # (hard memory cap via systemd scope + lean -M, core pinning, timeout, + # single-flight lock, free-RAM preflight with a retry ladder). The + # guard replaces the bare `lean` binary entirely and computes its own + # olean output path; caps are tuned via LEAN_MEM_MB, LEAN_MIN_FREE_MB, + # LEAN_MEM_WAIT_SEC, LEAN_TIMEOUT, LEAN_MAX_CORES in the environment. + guarded = [str(lean_guard), str(file_path)] + if root_path is not None: + # lean-guard forwards extra args to lean after the file; --root + # lets absolute file paths live outside the toolchain project dir. + guarded.append(f"--root={root_path}") + if use_lake_env and tools.lake: + return [tools.lake, "env", *guarded] + return guarded args = ["lean"] if root_path is not None: args.append(f"--root={root_path}") @@ -120,6 +136,7 @@ def lean_check_files( log_dir: str | Path | None = None, env_script: str | Path | None = None, lean_project_dir: str | Path | None = None, + lean_guard: str | Path | None = None, ) -> LeanCheckResult: if not files: return LeanCheckResult( @@ -172,6 +189,7 @@ def lean_check_files( use_lake_env=use_lake_env, output_path=path.with_suffix(".olean"), root_path=_lean_root_for_file(path, verification), + lean_guard=lean_guard, ) log.write("$ " + " ".join(cmd) + "\n") try: @@ -218,6 +236,7 @@ def run_axiom_audit( env_script: str | Path | None = None, lean_project_dir: str | Path | None = None, certificate_axioms: dict[str, list[str]] | None = None, + lean_guard: str | Path | None = None, ) -> AxiomAuditResult: expected = expected_axioms or STANDARD_LEAN_AXIOMS per_cert = certificate_axioms or {} @@ -251,7 +270,7 @@ 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) + cmd = build_lean_invocation(audit_file, tools, use_lake_env=use_lake_env, lean_guard=lean_guard) try: completed = subprocess.run( cmd, diff --git a/src/pacta/repo.py b/src/pacta/repo.py index 62c9295..6d19593 100644 --- a/src/pacta/repo.py +++ b/src/pacta/repo.py @@ -37,6 +37,17 @@ def status_for(repo: RepoConfig, base_dir: str | Path = "repos", explicit_path: ) +def resolve_lean_guard(lean_guard: str | None, repo_path: str | Path) -> str | None: + """Resolve a repo-relative lean-guard path; None when unset or missing + (callers then run unguarded, which is only acceptable for tiny fixtures).""" + if not lean_guard: + return None + candidate = Path(lean_guard).expanduser() + if not candidate.is_absolute(): + candidate = Path(repo_path) / candidate + return str(candidate.resolve()) if candidate.exists() else None + + def git_commit(path: str | Path) -> str | None: git = shutil.which("git") if not git: