proof-aware-crypto-tooling-.../examples
mrwulf 5b0158ecef 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>
2026-07-06 10:42:59 +02:00
..
anza-ed25519.claims.yaml Estate sync: boundary-axiom vocabulary + the four-tier apex reality (R4) 2026-07-06 10:04:43 +02:00
dalek-ed25519.attestation.yaml add verifier bootstrap and attestation lane 2026-07-03 11:24:13 +02:00
dalek-ed25519.claims.yaml Estate sync: boundary-axiom vocabulary + the four-tier apex reality (R4) 2026-07-06 10:04:43 +02:00
dalek-ed25519.full.attestation.yaml Estate sync: boundary-axiom vocabulary + the four-tier apex reality (R4) 2026-07-06 10:04:43 +02:00
pasta-pallas.claims.yaml Estate sync: boundary-axiom vocabulary + the four-tier apex reality (R4) 2026-07-06 10:04:43 +02:00
repos.yaml Machine protection: route all pacta Lean compiles through lean-guard 2026-07-06 10:42:59 +02:00