Two Fable-5 inventory agents cross-checked every empirical claim in the
paper against code/deployed log, and every external pointer against the
live internet. Fixes on both sides:
CODE (system brought up to the paper's claims):
- SECURITY: pin-store mutation (incl. permanent poisoning) was reachable
via receipts whose head signature FAILED verification in two of three
consumer paths (attestation.py, cli.py) - an unauthenticated forged
head at the pinned size could poison a consumer's pin forever and
pollute the equivocation-evidence pair with an unverifiable head,
contradicting SS5.4's 'validly signed' precondition and Prop 1.
Both paths now gate the store on a verified Ed25519 head signature
(logclient.py already did). Regression test added.
- Prop 2 made literally true: _normalize_certificate now derives the
cleanliness verdict purely from (observed cone, local allowed set) in
EVERY branch; the operator's axiom_status label is never copied (was
passed through for non-proven certs), missing cone => unverifiable
always. Labels can deny, never grant. Test added.
- webdocs: '/v1/sth-history: every head ever signed' -> 'the published
head history'.
PAPER (claims brought down to reality):
- 'every head ever signed' -> the signed head history since publication
began (heads for sizes 1-7 predate the mirror and were not retained).
- Run-3 bullet: 'independently checkable by diffing the two commit
trees' was no longer reproducible (pre-rewrite objects discarded);
now states the log-internal corroboration (identical cert lists and
cones across leaves 4-7 vs 8-11) and that tree diffs are not public.
- Appendix A leaf block now actually verbatim: scheme
openssl-ed25519, verified_backend serial/u64, real Lean version
(4.30.0-rc2) instead of 4.x.y placeholder, leaf's actual axiom order
(finalize/new/update), machine_protection note quoted, elisions
marked; preamble wording matches.
- Appendix C upstream boundary reordered to check.sh's verbatim order.
- '27 lines - all annotation' -> honest description (axiom-list entries
+ operation reordering from one fork's black_box barrier).
- Prop 2 proof + App A: status label consulted only negatively.
- SS7: provenance fields noted as outside the signed payload; consumer
chain relies on none of them.
- Bibliography: all 20 entries verified against DBLP/RFC-editor - zero
errors; added missing page numbers to 6 entries; thebibliography
width 19->20. All URLs verified public; no PlanetMacro leakage.
17 pages, 106 tests green, accumulator untouched (tree_size 12).
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>
