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 <guard> <file> --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 <noreply@anthropic.com>

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

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,

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(

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"),
         )
 
 

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,

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: