saymrwulf/proof-aware-crypto-tooling-agent
1
0
Fork 0
mirror of https://github.com/saymrwulf/proof-aware-crypto-tooling-agent.git synced 2026-09-04 20:03:40 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions
proof-aware-crypto-tooling-.../AGENTS.md
mrwulf 37429335e6 docs: coherence + portability audit — clean-clone bootstrap proven 
Audit question: is the documentation coherent, and is the app portable
to a fresh machine (macOS) with proper isolation? Findings and fixes:

- README never mentioned the cockpit/deck/lab manual (three rounds of UI
  evolution invisible at the front door). Added: human-surface section
  with the one command, expanded Install (editable-from-clone is the
  supported mode — repo files are part of the product; zero-install
  PYTHONPATH=src alternative; fresh-machine skip behavior), macOS
  openssl/LibreSSL Ed25519 prerequisite with a one-line self-check,
  wallet commands in the command list.
- The lab manual violated the repo's own macOS law (AGENTS.md): GNU
  sha256sum -> shasum -a 256; GNU sed -i -> portable python3 -c
  one-liner (executed and output-matched before shipping: entry 0 hash
  mismatch, BROKEN, exit 1).
- Fresh-clone bootstrap was actually tested end to end in a scratch
  clone: zero-install suite 130 passed / 0 failed / 14 skipped after
  fixing the one unguarded test (test_ledger_is_hash_chained now skips
  like its siblings when the dogfood binary is absent - capability gap,
  not failure); venv + pip install -e . -> pacta console script serves
  bridge/deck/manual/sample-prefill/drift-tripwire with no PYTHONPATH.
- PYTHONPATH incantations simplified: cockpit needs src only (provider
  never imported by src/pacta); manual + cockpit.md updated.
- threat-model.md: cockpit attack-surface note (no mutating routes,
  no auth because nothing to operate, localhost-only disclosure risk,
  probe-only network I/O, fake-cockpit = host-compromise boundary).
- products.md: cockpit named as the shared human surface of all four
  profiles. AGENTS.md: doc-portability law + the cockpit's three laws
  added to the standing guidance.

Suite 144 green here; 130/0/14 on a bare clone.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-21 18:00:08 +02:00

4.6 KiB
Raw Blame History

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.
  • The same portability law applies to DOCUMENTATION: commands printed in docs, the cockpit, and the lab manual must run on macOS (BSD userland: shasum -a 256 not sha256sum; no GNU sed -i form; prefer portable python3 -c one-liners), and every printed command must be executed once before it ships.
  • The cockpit's three laws are load-bearing: renders-evidence-never-asserts (provenance lines, loud FAILED TO VERIFY), never-leave-a-human-in-the-dark (verdict in words, explainers, glossary links), and distinct-roles-with-handoffs (stations never melt). All three are test-enforced; keep them so.
  • 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.