mirror of
https://github.com/saymrwulf/proof-aware-crypto-tooling-agent.git
synced 2026-09-04 20:03:40 +00:00
mrwulf
5b0158ecef
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>
67 lines
2.7 KiB
YAML
67 lines
2.7 KiB
YAML
repos:
|
|
- name: dalek-ed25519-verified
|
|
url: https://github.com/saymrwulf/dalek-ed25519-verified.git
|
|
kind: ed25519
|
|
verification_dir: verification
|
|
verified_backend: serial/u64
|
|
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)
|
|
- signing-side correctness
|
|
- side-channel resistance
|
|
- compiler correctness
|
|
- SIMD/AVX/accelerator paths
|
|
|
|
- name: anza-ed25519-verified
|
|
url: https://github.com/saymrwulf/anza-ed25519-verified.git
|
|
kind: ed25519
|
|
verification_dir: verification
|
|
verified_backend: serial/u64
|
|
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
|
|
- Solana transaction construction
|
|
- the default HEEA/Zebra verify() path
|
|
- accelerator paths
|
|
|
|
- name: risc0-ed25519-verified
|
|
url: https://github.com/saymrwulf/risc0-ed25519-verified.git
|
|
kind: ed25519
|
|
verification_dir: verification
|
|
verified_backend: serial/u64
|
|
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
|
|
url: https://github.com/saymrwulf/betrusted-ed25519-verified.git
|
|
kind: ed25519
|
|
verification_dir: verification
|
|
verified_backend: serial/u64
|
|
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
|
|
url: https://github.com/saymrwulf/pasta-pallas-verified.git
|
|
kind: pasta_pallas
|
|
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
|
|
- production-ready Pallas arithmetic unless add/mul/reduce/square/invert are proven
|