Socratic pass over everything this public repo reveals, adversary-first:
- DEPLOY.md no longer names the hosting provider or the server's other
software inventory (that sentence was NEW public information - the
site's front page does not advertise it). It now states its own
redaction policy up front, leads with a Caddy proxy config (matching
what the target site actually fronts with), adds rate-limiting and
proxy timeouts for the stdlib backend, generalizes the second-mirror
section, and gains an explicit key-hygiene section (the signing key
never touches the public server; a compromised box has nothing to
rotate).
- Future attestations stop leaking provider-machine paths: the
machine_protection guard path is recorded repo-relative and the Lean
project dir is recorded in its configured env-var form, never
machine-resolved. (The 12 already-published leaves containing local
home paths are immutable by design - severity assessed low: a local
username on a non-addressable dev box, no credentials - and an
append-only log does not rewrite its history.)
Audited clean: no keys, tokens, or credential-named files anywhere in
git history; no public IPs; loopback-only binds; commit identity is the
owner's long-standing public one. 54/54 tests.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
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>
The verified corpus completed its phase 2 on 2026-07-06: every ed25519
fork now carries FOUR button-enforced apex tiers up to the full lift
(accept <=> decompress(R) = [k](-A)+[s]B as points), the complete scalar
layer, and the constructive encoding/decoding chain. pacta was calibrated
to the pre-apex corpus and - worse - had no vocabulary for
boundary-audited certificates: its axiom audit knew only "clean = exactly
the three standard axioms", so the apex tiers would have scored dirty.
New vocabulary:
- Profile.certificate_axioms: per-certificate ALLOWED axiom sets;
expected_axioms_for(cert) resolves each certificate's own boundary.
- RepoConfig.apex_boundary: a simple per-fork key (dalek-wrappers /
hash3 / anza) expanded by the ed25519 profile into the exact
per-tier allowed sets. AUTHORITY NOTE in profiles/ed25519.py: each
repo's check.sh Phase 3b is the enforcement point; if the button and
this table disagree, the button wins.
- run_axiom_audit compares each certificate against ITS allowed set;
deviation in EITHER direction (extra axiom or missing boundary
axiom) is dirty.
New risk reality:
- R4 is now reachable: full four-tier apex + constructive chain +
scalar arithmetic, all proven with cones pinned to their documented
boundaries. R4 always carries explicit residual blockers (SHA-512
oracle, hypothesis-parametric wire parses, translation faithfulness,
no side-channel/build assurance - those gate R5).
- R3 unchanged (arithmetic pair) and now explains exactly which apex
certificates are missing for R4.
Attestation trust model hardened:
- The provider is trusted for its OBSERVATION, never its VERDICT:
axiom_status is re-derived locally from observed_axioms against the
agent's own boundary policy. A provider that labels a dirty cone
"clean" gains nothing; "proven" with no observed axioms is
"unverifiable".
- Partial attestations degrade instead of being rejected: uncovered
certificates stay unproven and the score caps accordingly (an
arithmetic-only attestation still authorizes an R3 library capsule,
never a wallet).
Also: scripts/mini_pytest.py - a dependency-free test runner (tmp_path,
raises, monkeypatch, capsys) for hosts without pytest; examples
regenerated FROM the tool (dalek/anza fixtures now R4, 16 certs; new
full four-tier attestation example); tests updated + new
tests/test_boundaries.py (lying-provider, missing-boundary-axiom,
partial-coverage cases). 40/40 tests green.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
