mirror of
https://github.com/saymrwulf/proof-aware-crypto-tooling-agent.git
synced 2026-09-04 20:03:40 +00:00
mrwulf
bde0f87558
README: truth boundary rewritten to the proven four-tier reality (with the still-unproven list at equal weight); risk expectations state the R4 path and the now-openable wallet gate; new sections for the STH pin store / split-view defense and the dogfood verifier; notebook course list gains lecture 9 and the ratchet rule; test-runner note. AGENTS.md gains the operating rules the new subsystems depend on: boundary tables mirror the repos' buttons (the button is the authority); observation-vs-verdict for providers; degradation semantics for partial attestations; the pinning rules (equivocation, growth-needs-proof, rollback, anchor-root checking); dogfood provenance/fallback-visibility rules; ML-DSA stays fail-closed; the mini runner must keep covering the whole suite. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
29 lines
4 KiB
Markdown
29 lines
4 KiB
Markdown
# AGENTS.md
|
|
|
|
Guidance for future Codex runs in this repository:
|
|
|
|
- Do not add Charon or Aeneas transpilation flows.
|
|
- Do not regenerate Lean from Rust. Treat shipped Lean files in verified repos as the artifact.
|
|
- Do not claim end-to-end verification unless theorem coverage actually exists.
|
|
- Keep macOS and Apple Silicon portability. Do not rely on GNU `timeout`, `free`, `taskset`, Docker, Nix, or x86_64 assumptions.
|
|
- Prefer explicit theorem-boundary language over marketing language.
|
|
- Update tests with every behavior change.
|
|
- Do not silently lower risk ratings. A lower score must explain the failed or missing evidence.
|
|
- Do not hide proof failures behind warnings.
|
|
- Keep claim cards machine-readable and reports explicit about proven claims, preconditions, exclusions, trusted base, and residual risk.
|
|
- Consequence-producing commands must be policy gated. Do not build wallet or trading-agent artifacts from `R3` arithmetic evidence.
|
|
- Distinguish verifier capability failures from proof failures. Missing `Mathlib`, missing `Aeneas`, or a missing pinned env script means local replay is unavailable; do not treat it as a clean proof.
|
|
- Third-party proof-checking attestations are allowed only as an explicit trust transformation. They must identify the provider, subject repo/commit, theorem names, observed axioms, and signature status. Untrusted attestations must not authorize builds.
|
|
- Transparency receipts must be verified against the exact attestation bytes, Signed Tree Head, log public key, and inclusion proof before they can authorize consequences.
|
|
- Keep the Merkle log RFC 9162-style unless a new standard is deliberately adopted and documented. Do not replace it with an ad hoc hash chain.
|
|
- Do not pretend ML-DSA exists. If no real ML-DSA backend is available, record the signature slot as unavailable and fail closed for policies that require both Ed25519 and ML-DSA.
|
|
- Provider private keys and transparency log state belong under ignored `provider/state/` or `provider/out/` paths. Do not commit local trust state.
|
|
- Curriculum notebooks are generated by `scripts/build_curriculum_notebooks.py`. Update the generator, regenerate `notebooks/`, and keep notebook code cells output-free. Execute every changed code cell before committing. Keep the ratchet rule: each load-bearing idea gets a napkin-scale AND a real-scale runnable pair.
|
|
- The per-fork apex boundary axiom sets in `profiles/ed25519.py` MIRROR each verified repo's check.sh Phase 3b; the button is the authority. When a repo's enforced boundary changes, update the table in the same change set and say so.
|
|
- Apex-tier certificates are judged against their fork's documented boundary, standard certificates against the three standard axioms; deviation in EITHER direction is dirty. Never widen an allowed set to make a cone pass.
|
|
- Trust providers for OBSERVATIONS, never VERDICTS: axiom_status of attested certificates is re-derived locally from observed_axioms. Do not bypass `_normalize_certificate`.
|
|
- Partial attestations degrade (uncovered certificates stay unproven; the score caps); they are not rejected. Identity, signature, and receipt failures still reject.
|
|
- STH pinning: same size means same root (EQUIVOCATION otherwise), growth requires a verified consistency proof from the pinned size, shrinkage is rollback. Never accept growth without proof, and always check the consistency anchor's ROOT against the pin, not just its size.
|
|
- Dogfood verifier: never hardcode a machine path in committed files (Cargo.toml stays a template); always write the provenance sidecar; record the backend that actually verified each signature; OpenSSL fallback must be visible in evidence and must fail `--require-verified-verifier` policies.
|
|
- ML-DSA stays fail-closed until a real, configured backend exists. The dogfood loop does NOT extend to it: there is no proven ML-DSA, and the hybrid posture depends on saying so.
|
|
- `scripts/mini_pytest.py` must keep running the whole suite on a bare python3; if a test needs a new pytest fixture, extend the shim in the same change.
|