Phase 2b+3 of the step-3 rehearsal, under the four operator decisions of
2026-08-06: deterministic signing, separate slh_dsa block, additive posture,
keygen executed same day (key in provider state, 0600, git-ignored — verified
before generation, not after).
src/pacta/slhdsa.py — the module that did not exist (register:
pq-slot-names-unproven-algorithm). Parameter set LOCKED to SLH-DSA-SHA2-128s:
every entry point asserts the key's reported algorithm and refuses anything
else, because any other set sits outside all eleven certificates while looking
like dogfood. Deterministic via -pkeyopt deterministic:1, so the byte-level
reproducibility check that caught a real defect on the Ed25519 side survives
here. Verification runs two ways: OpenSSL, and pacta-verify-slhdsa built from
the pinned proven source — the one signature check in the estate performed by
code whose verify path the certificates cover. The proven-verifier path is
package-anchored, not cwd-relative: the lesson of signer-backend-depends-on-cwd
applied on day one, not retrofitted.
make_signed_tree_head grows optional slhdsa key parameters. With them, the head
carries a signed slh_dsa block; without, an honest not-configured slot exactly
as ml_dsa always has. ml_dsa itself is untouched. Signatures stay outside the
signed payload for both algorithms — tested by asserting the payload is
byte-identical with and without the slh_dsa key.
Honesty carried in the artifact: signing_backend says "openssl" because no
proven signer exists for any algorithm; the module docstring states that
nothing here is Lean-proven and that the certificates cover the verify path of
the extracted model only.
Tests: 7 new, suite 152 passed, 0 failed, 0 skipped — including determinism
(two signings, identical bytes), the foreign-key refusal (Ed25519 key raises),
corruption rejected by both verifiers, and the proven/OpenSSL agreement.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
DEFAULT_STATE_DIR was Path("dogfood")/"state" -- a relative path, so
locate_verifier() resolved against whatever directory the process started in.
The consequence was not a crash but something quieter: run the provider from
the repository root and it signs with the attested dalek build; run it from
anywhere else and the binary is not found, signing falls back to OpenSSL, and
the head records `signing_backend: openssl`. Which implementation signs the
transparency log was an accident of the current directory.
Found by re-signing published head 13 as a reproducibility check. The byte
comparison passed -- the reconstructed payload re-signed to signature_base64
exactly -- but the backend came back `openssl` while head 13 records
`verified-dalek-serial`. The swap is invisible precisely BECAUSE Ed25519 is
deterministic: both implementations emit identical bytes, nothing downstream
differs, no test fails. A silent substitution that changes no output is one
nobody notices until the outputs differ, which for a signing key is late.
(The byte-identity is also a good result in its own right: independent
cross-implementation agreement on the SIGNING side, alongside the five-way
agreement already demonstrated on the verifying side.)
Fix: anchor to the package via Path(__file__).resolve().parents[2]. Resolution
no longer depends on cwd -- demonstrated from /, /tmp and the repo root, all
three now select verified-dalek where before only the repo root did.
Added PACTA_REQUIRE_VERIFIED_SIGNER. Recording a downgrade truthfully, which
this code already did, tells you afterwards which implementation signed; it
does not let you DECIDE which one will. For signing a transparency-log head
that choice should be stated up front and enforced, not discovered in a
provenance field once the head exists. Set it and signing raises instead of
substituting OpenSSL. Off by default: every existing caller keeps the
fall-back-and-record behaviour.
Negative-tested both ways (refuses, naming the path it searched; default still
records `openssl`). Suite: 145 passed, 0 failed, 0 skipped.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
The /estate page was hand-written prose inside estateview.py: 32 hard-coded
fact arrays and zero places reading live data, last edited 2026-07-22. It
cannot go stale by accident — it can only go stale, because nothing connected
it to the repositories it describes. For eight days it told the operator:
· SLH-DSA "campaign in progress", "check.sh exits non-green by design"
— while it had 11 proven certificates, a green button, an 18-attack
self-test and an outside reviewer's attest-with-conditions;
· ed25519 "16 reviewed certificates"
— while they had 31 bound certificates and 3022 inventoried constants;
· nothing at all about five audit phases and five self-tests per repo,
none of which existed on the day the page was last touched.
Those four claims are corrected. More importantly the page now carries a
MEASURED panel rendered from formal-verification-control's
tools/estate-progress.py, which derives every figure from the repositories at
generation time. The panel states three things a reader would otherwise have
to assume:
· WHEN it was measured, and by what;
· WHETHER the repositories have moved since — the snapshot records the HEADs
it was taken against, and the panel compares them live, naming any repo
that has moved rather than quietly showing old numbers as current;
· WHICH PART OF THE PAGE IS MEASURED AT ALL. Everything above the panel is
labelled, in the page itself, as hand-written prose that can be out of
date. That label is the honest part: the map is still prose, and a reader
should know which half is which.
If the snapshot is absent the panel says NOT MEASURED in words and prints the
command to produce one. It never renders nothing, and never falls back to
prose — a blank space and a confident-looking stale figure are the same
failure, and the second is worse.
Two numbers, never one, per PROGRESS-METRIC.md: a single figure is what let
the old metric report 100% for work nobody had attacked.
All three paths tested: current, moved-since, and absent. 145/145 tests pass,
including the sync test guarding drift between this page and ESTATE.md.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
The deployed consistency verifier implemented the RFC 9162 2.1.4.2
bit-navigation loop but its final return checked only the two
reconstructed roots, omitting the terminal condition that the new-size
navigation counter reach zero. That condition couples the consumed proof
length to the claimed tree sizes; without it, a valid proof for one
transition verifies under a lied (power-of-two) old size. Flagship: a
valid 2->3 proof is accepted under the false claim 1->3 with the size-2
root.
Fix: add `and sn == 0` to the final return.
This is the corpus's Known Gap 14 (3,867 deployed-accepts-only cases in a
pinned 73,573-case family, recorded in public log entry 13). It was
found by the project's own differential harness; a post-appeal review
round added a faithful RFC oracle as a third comparison, which showed
the deployed verifier — not the mechanized model — was the one deviating
from RFC 9162, and traced it to the missing terminal check.
Scope: verify_consistency's only production caller is the consumer-side
pin store, reached only behind a verified head signature. Generation is
RFC-correct and unaffected; the live provider service does not run this
verifier; the published standalone verify.py has no consistency verifier.
An empirical search found 0 realizable pin-advance poisons against an
honestly pinned consumer, consistent with Known Gap 14's non-claim.
Verification:
- New fail-first three-way regression test
test_consistency_lied_size_three_way_agreement (deployed / recursive
ConsRec model / independent faithful RFC 9162 transliteration) over the
honest AND lied-size families; fails pre-fix, passes post-fix.
- Historical differential tests (164,479 inclusion; 164,224 consistency)
unchanged — the fix rejects nothing honest.
- Full suite: 145 passed, 0 failed.
Public log entry 13, the attested accumulator commit, and the IACR
submission PDF are all unchanged. Vulnerable state tagged
vulnerable/sn0-consistency-fd2f6ba. See
docs/security-2026-07-23-consistency-terminal-check.md.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Two repos joined the estate on 2026-07-22; both renderings (ESTATE.md +
cockpit /estate) gain their cards, with every fact recomputed from the
repos themselves:
- fips205-source (upstream lane): verbatim snapshot of
integritychain/fips205 (pure-Rust FIPS 205 / SLH-DSA), upstream pin
30bac08, snapshot head 5dca0db — single deviation: upstream CI
workflows stripped, documented in-commit. Aeneas-compat patches land
there as transparent, individually-justified commits; nothing is
proposed upstream.
- fips205-slhdsa-verified (subject lane): SLH-DSA-SHA2-128s verify-path
campaign, marked exactly as its own check.sh says — CAMPAIGN IN
PROGRESS, zero certificates, non-green by design. NOT attested; the
map does not imply otherwise.
Also:
- liveness board now probes fips205-slhdsa-verified (a sibling under
the default repos root). fips205-source is deliberately NOT probed:
the upstream-source shelf lives outside that root, like the five
existing source clones (comment documents the decision).
- drift tripwire (test_estate_view_and_estate_md_do_not_drift) extended
with both new sentinel names.
- stale fact chip refreshed in both renderings: pacta suite 135 → 144
green (the suite grew during the cockpit era; chip was never bumped).
- estateview's pasta dossier no longer calls the curve layer "the one
open verification task in the estate" — the campaign is a second.
Suite 144 green.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Operator asked for a real big fat user manual: read on one monitor with
the deck on the other, worked like a lab from beginning to end, with
highest didactical skill — the goal being to educate ONE person in ALL
roles, as if to BECOME each role. Shipped as a full course:
- docs/warden-lab-manual.md (canonical, ~7100 words): 8 sessions +
capstone. Fixed didactic ritual per role-session: why the role exists
-> the mind of the role -> concepts -> LAB (numbered machine exercises
with checkpoint rails) -> never-list with whys + thought experiment ->
handoff artifact -> self-test -> recap card. Notation: do / checkpoint
/ write / optional. Capstone 'incident day': one incident walked
through all six chairs producing seven written artifacts; graduation
session maps the path to a real wallet; Appendix A command reference
by chair, Appendix B full self-test answers.
- Session 4's tamper drill: copy the demo wallet, flip one character of
ledger history, watch verify-ledger AND a second cockpit catch it.
Every checkpoint in the manual was executed by the author before
commit: status fields, intact-chain exit 0, tampered-chain 'entry 0:
hash mismatch / BROKEN' exit 1, CUSTODY EVIDENCE BROKEN banner.
- src/pacta/mdlite.py: deliberately small stdlib Markdown renderer
(headings/anchors+TOC, bold/italic/code with placeholder stashing,
fences, lists, quotes, tables, links); tested against the real manual
for zero artifact leaks.
- /manual route with syllabus TOC; manual typography (checkpoint boxes,
session borders); nav tab, deck wizard cross-link, cli hint.
Suite 142 -> 144 green; read-only sweep covers /manual.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Operator asked for a tmux-type panes grid in the browser (one pane per
role, all acting in parallel, like real life) with a wizard on the right
that takes a newcomer by the hand through every role's actions, each
instruction camouflaged in that role's color.
- /deck: CSS-grid of six live panes (2-col, 3-col on wide screens),
one per station, each an iframe onto /station/<id>?pane=1. tmux
controls per pane: reload, single-pane zoom, open-full. Narrow
screens: wizard first, panes stacked.
- pane mode (?pane=1): chrome-stripped shell (no h1/banner/nav), same
station content, READ-ONLY label kept; an 8-line shim re-carries
pane=1 on every same-origin link and form submit, so probes, incident
browsing, and inspect verdicts all happen inside the pane.
- the wizard: a 10-step guided first watch across all six roles on the
live demo wallet. Each step card wears the role's hue with a 'YOU ARE
THE <ROLE>' chip, the matching pane glows, and every step states what
success looks like + what was just learned. Step remembered per
session (sessionStorage).
- /inspect?sample=1 pre-fills examples/wallet-evidence so the
cryptographer step verifies (then deliberately breaks) real evidence.
- verified in a real browser: step navigation moves the glow, panes
load their stations, Probe-now inside the pane probed live inside the
pane (log head tree_size 13), sample flow prefilled the key in-pane.
Suite 139 -> 142 green. Read-only guarantee unchanged; byte sweep
covers /deck and pane routes.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Operator verdict on round two: better, but 'still no coherent
application'. The cockpit must provide everything a human crew would
need if no AI were around — as distinct roles that cooperate through
handoffs and never melt into each other. This rebuilds the IA as a
bridge with six stations over shared instruments, in the control-room
tradition (overview -> station -> instrument -> raw files/CLI), with
maker-checker separation of duties encoded in the UI itself.
- / is now the Bridge: whole-system verdict strip, six crew cards with
live data, and the dispatch (andon) board 'if this happens, who acts'
- /station/{proposer,quorum,operator,cryptographer,architect,newcomer}:
each console has a fixed anatomy: Mission -> Duties (every duty a
runnable, verified-real CLI command - the no-AI drill) -> embedded
live instruments -> 'This station never...' (separation of duties) ->
Handoffs (receives/delivers)
- Operator gets a real liveness board: on-demand parallel probes (HTTP
GET on log head/paper/blog/mirror with observed facts + latency; git
HEAD/cleanliness on all 9 local repos). Never probes on ordinary page
loads. Verified live: caught this very repo as 'alive, dirty' while
building it, and confirmed log 13/3488a2d0 + paper 7f140356
- Architect gets the live drift tripwire (ESTATE.md vs estate view)
- modularized per the standing separation-of-concerns order:
uikit.py (primitives+style), stations.py (role model, pure),
liveness.py (probes), walletui.py (collectors, instruments, routes)
- crew law test-enforced: bridge crew+dispatch, per-station role
contract, station distinctness (signature phrases must not bleed
across roles), explicit-probe semantics; read-only byte sweep now
covers all 13 routes incl. the probe route
- narrow-viewport fix: breakany for unbreakable paths in headings
Suite 135 -> 139 green. Read-only guarantee unchanged: no mutating
routes; every custody act is a printed command, never a button.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Operator verdict on the first cockpit: unusable, jargon-walled. The
evidence layer was honest but the presentation assumed the reader
already lived inside warden's head. This rebuilds the presentation
layer around a testable UX contract, additive to the design law:
- every page: verdict IN WORDS first (CUSTODY HEALTHY / CUSTODY FROZEN
(LATCHED) / CUSTODY EVIDENCE BROKEN), then evidence, then provenance
- every page: plain-language lead saying what the page answers
- every panel: 'How to read this panel' expander interpreting every
column and pill; jargon carries a ? linking to the glossary
- new /guide view: what warden is, how to read any page, color code,
five-minute tour, 12-term glossary, honest 'what this cockpit cannot
tell you'
- navigation: two-line tabs stating the question each view answers,
present on every page; /estate gets a back-to-cockpit chip
- explained empty states (incidents: 'empty is the good state')
- narrow-viewport fix: tables/pre scroll in their own containers
- estate fact chip updated 130->135 green (both renderings)
UX contract is test-enforced (guide terms, lead+nav+explainers on every
view, empty states); read-only byte-guarantee sweep now covers /guide.
Verified by looking: served --demo, walked all six views in a browser.
Suite 131 -> 135 green.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The operator ran the documented command and hit the fail-fast (no
wallet exists on a fresh machine) — correct behavior, useless
instruction. seal_demo_wallet() now seals a throwaway DEMO wallet
(fake shell-stub members, DEMO-labeled fields, temp dir named
warden-DEMO-*, sample incident/refusal/airgap so every view has
content); 'pacta wallet cockpit --demo' serves it. Exactly one of
--wallet/--demo required. Verified by running the literal command:
all five views 200, demo quorum renders. Suite 130 -> 131.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Operator questions answered in code: (1) the estate map now lives IN the
cockpit too — /estate serves the interactive map (lanes, typed edges,
loops, clickable dossiers) to the same human audience the cockpit
serves; ESTATE.md remains the canonical committed version (renders on
GitHub, reachable by agents via llms.txt, needs no running process), and
a name-level sync test guards drift between the two renderings — the
published_assets lesson applied preemptively. (2) 'What is RUNNING?' is
now answered everywhere: an operations strip on the map (ALWAYS ON:
caddy + the LTL read-only container + Forgejo with its single 03:00
mirror cron, all droplet; ON-DEMAND: append/publish/sign ceremonies,
cockpit, MCP, operator machine only; NOT RUNNING: warden — prototype,
no deployed instance, no funds watched; everything else: static files
or external parties), a per-entity Runtime line in every dossier, and a
verified What-is-running table in ESTATE.md (container commands, :ro
mounts and read_only:true on the LTL service, and the crontab checked
on the droplet 2026-07-20, not recalled).
Suite 128 -> 130 (estate route + drift guard). Local-only as before:
nothing deployed, live estate untouched.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Operator-ordered milestone, built under an explicit no-risk constraint
while the paper application is in flight: strictly ADDITIVE (one new
module + one CLI subcommand; zero changes to wallet semantics, the
public site, or anything the paper describes), LOCAL-ONLY (never
deployed; binds 127.0.0.1), and READ-ONLY in v1 (human approve/deny is
deliberately deferred — that is a custody-semantics change belonging to
a separately reviewed milestone).
New: src/pacta/walletui.py — four views over an existing wallet:
- Posture: latch state, ledger head with FULL hash-chain
re-verification, pinned quorum members, spending policy verbatim.
- Signature queue: airgap outbox/inbox, observed never operated.
- Incidents & refusals: verbatim records, newest first.
- Receipt inspector: paste attestation + receipt + log key; verdict,
per-signature results, and diagnostics come verbatim from
transparency.verify_receipt — the deployed verifier itself, reused
not reimplemented.
Design law, stated in the module and enforced by tests: THE COCKPIT
RENDERS EVIDENCE, IT NEVER ASSERTS IT. Every panel recomputes at
request time and carries a provenance line (function + timestamp);
anything unverifiable renders a loud FAILED-TO-VERIFY panel — no cached
green, no neutral gray. Panels state what they do NOT prove (e.g.
binary pinning vs source-to-binary correspondence).
CLI: pacta wallet cockpit --wallet DIR [--host --port].
Tests (10 new, suite 118 -> 128 green): recomputed-evidence rendering,
CHAIN BROKEN on tampered ledger, loud failure on collector error,
latched-state rendering, airgap queue states, verbatim incident/refusal
rendering, fail-closed inspector on garbage, real-evidence roundtrip
(skips if example evidence absent), full-sweep BYTE-LEVEL read-only
guarantee (wallet dir hash-identical after all GETs + a POST), and
fail-fast on non-wallet dirs. Rendering additionally verified visually
against a live demo wallet (posture, quorum table, incidents).
Docs: docs/cockpit.md; WALLET.md section; ESTATE.md + llms.txt updated.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Its last two callers vanished in the round-6 hardening (parse anchors
on the exact phrase via regex; classification is membership-based).
Dead code in an audited producer invites misreading. Suite 115.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
R6-B1 (Claude, executed end-to-end): provenness was decided by a
WHOLE-OUTPUT 'no axioms' sentence, so an axiom-free certificate whose
line was entirely absent still scored proven+clean ([]==[]). The
reviewer drove a doctored 60-line output through the real gate and got
61/61 with domsep never audited. Classification is now extracted into
classify_certificates(): proven iff the certificate's OWN anchor was
parsed (axiom-free anchors populate []); absent certs are
unknown/failed + not_checked — never clean. This also fail-closes the
typo'd-future-cert case (R6-C2).
GPT §6: parse_axiom_output is now RECORD-scoped — anchors delimit
records, a cone bracket is accepted only inside its own record, missing
or truncated brackets yield MISSING (fail closed) instead of borrowing
the next certificate's bracket, and cones may wrap arbitrarily (the
old fixed 16-line window was a latent overflow for the 11-axiom
ed25519 apex cones on this estate). Anchor names are captured between
the exact quotes Lean prints.
Six new regression tests (absent-axiom-free-not-clean, missing-bracket
no-steal, truncated cone, >16-line wrap, duplicate anchor, interleaved
diagnostics). Suite: 114 passed / 0 failed.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Found by the entry-13 rehearsal (the accumulator corpus is the first
subject with axiom-free certificates — every fork certificate carries
at least the boundary axiom, so this path was never exercised):
- an axiom-free certificate ('X' does not depend on any axioms) was
parsed by opening a 16-line window and taking the first bracket in
it — which belongs to the NEXT certificate. domsep/Hash/
instDecidableEqHash/take_append_drop were reported with their
neighbors' cones and flagged dirty.
- certificate names were matched as bare substrings, so 'Foo' could
anchor on the line for 'Foo_bar'. Now anchored on the exact quoted
name Lean prints.
The no-axioms decision is now made on the anchor line itself, before
any window. Two regression tests added (steal-next-cone, exact-name);
suite 108 passed / 0 failed.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
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>
Makes the paper's pin-store safety proposition true in the deployed code:
- the full signed STH is retained at pin and at each advance (not just
size+root), so on equivocation both conflicting heads are transferable,
signature-verifiable evidence;
- any equivocation (same-size root mismatch, or a consistency anchor
disagreeing with the pin) persists poisoned=true with both signed
heads and refuses ALL further operations for that log, restart-proof
and independent of the update flag;
- rollback unchanged. 102 tests (was 100): poison persistence, evidence
transferability, full-head retention.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Correctness:
- ledger: single-flight fcntl lock over read-modify-append + fsync. Two
concurrent writers previously could fork the hash chain (read same tail,
same prev_hash). New test races 8 threads x6 appends; chain stays intact
with contiguous indices.
- small-order list: the order-8 encodings were hand-typed and unverifiable
and diverged from the canonical libsodium blocklist. A BOGUS entry is the
only dangerous direction (it down-grades a real tamper to a note, skipping
the latch), so the list is now the certain-low-order set only (y in
{0,1,-1}, reduced/non-reduced, both sign bits); order-8 edges escalate to
tamper until a derived list lands. Fail-safe asymmetry documented + tested.
- freshness: removed a tautological .
Non-functional:
- quorum members now run concurrently (ThreadPoolExecutor): a verify costs
one member's latency, not the sum (~17ms for 4 members, live).
- Wallet.quorum() memoized per state_dir: binary swap-detection hashes run
once at assembly, not on every verify; documented rationale.
85 tests green; live 4-fork wallet re-verified end-to-end.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
pacta wallet init/status/card/verify-ledger and the stdio MCP server
all confirmed working end-to-end against the four-fork R4 wallet.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
- walletmcp.py: stdlib stdio JSON-RPC MCP server; 7 outcome-first tools
with strict schemas; errors are structured (code/missing/remediation),
never prose; results carry evidence (structuredContent)
- custodycard.py: A2A-style card sharpened to self-proving - embeds each
member's LTL inclusion proof + STH so a counterparty recomputes trust
instead of believing it; proof-of-posture nonce challenge returns a
firewalled, signed posture attestation with the full quorum trail
- cli.py:
- verified end-to-end on the live wallet: all 7 MCP tools, structured
refusal on bad input, and a counterparty recomputing all 4 inclusion
proofs + STH signatures from the card alone (no operator trust)
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
- Wallet.init is the R4 gate in executable form: per member, the built
binary's source commit must match an attestation whose verdicts are
re-derived locally, scored >= R4, and Merkle-bound to a verified STH
under the log key (explicit --trusted-provider required, never inferred)
- append-only hash-chained ledger; latch semantics (tamper => custody
frozen; unlatch is a deliberate operator act recorded with a note)
- outbound: intent envelope bound to payload bytes -> signer (local
dogfood or airgap/Precursor-style outbox) -> quorum firewall; a
rejected self-signature is quarantined, never released, and latches
- refusal receipts: signed machine-actionable artifacts (code, missing,
remediation); unsigned-by-design while latched
- live end-to-end against ltl.zkdefi.org: 4 members R4 (leaves 4-7),
release firewall unanimous-accept, inbound unanimous-accept, refusal
signed, ledger chain verified
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
- dogfood/quorum/verify-{dalek,anza,risc0,betrusted}: verify-only crates
built from the pinned proven source workspaces (serial backends pinned
per fork; anza entry is the certificate-covered verify_sha512, not the
default Zebra-lineage verify())
- src/pacta/quorum.py: unanimity-required acceptance, divergence
taxonomy (semantic-edge vs unexplained/tamper), small-order/canonicity
edge flags, per-member provenance sidecars with binary hashes
- live smoke: 4/4 members agree on accept and reject
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
- serve/webdocs/cli default to base_path='' (own subdomain, root serving)
- webdocs link builder handles the empty base like web.py already did
- all docs, paper, notebook 06b, and published-mirror README point at
https://ltl.zkdefi.org; DEPLOY.md rewritten for subdomain + redirect
- tests: root mount is the production shape; one test keeps exercising
the path-mounted variant
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Three synchronized faces of one log - transport orthogonal to trust:
- PUBLISHED GIT MIRROR: log-publish exports the public face (one file
per leaf so git history mirrors log history; the FULL STH history as
the witness channel; per-component attestations + receipts; the
provider public key; a standalone stdlib-only verify.py and customer
README). Live at github.com/saymrwulf/lean-transparency-log (genesis:
8 leaves incl. the honest failed-run entries, dogfood-signed head).
- ONLINE SERVICE (pacta_provider serve): read-only, zero-dependency
HTTP with CT-style endpoints under a base path for
zkdefi.org/lean-transparency-log - /v1/sth, /v1/sth-history,
/v1/sth-consistency?first=N, /v1/proof, /v1/attestation, /v1/entries,
/v1/metadata, /healthz - plus self-contained customer documentation
at /docs (current state, attested components, API, the verify-
without-trusting-this-site path, and the means/does-NOT-mean
boundary). The process never loads private keys: heads are signed
offline; a compromised server can withhold or replay (pinning +
freshness detect both) but never forge. STH history now recorded
append-only by the provider (with a backfill head signed for the
existing log).
- AGENT ONLINE CLIENT: pacta log-fetch (download evidence; explicitly
UNVERIFIED until receipt-verify runs - transport is not trust) and
pacta sth-refresh (fetch head, verify signature, advance the pin via
an online consistency proof from the pinned size; fail closed).
- WITNESSES: pacta witness-audit over a clone of the published mirror
recomputes every prefix root from the public leaves and checks every
historical head + signature - no consistency proofs needed when the
leaves are public. Tampering one published entry trips both the
leaf-hash check and the prefix-root check (tested). verify.py gives
customers the same audit with zero installation.
- DEPLOY.md: the complete server-session checklist for zkdefi.org -
reconstruct the servable log FROM the published mirror (the server
stays in witness trust-position), hardened systemd unit, nginx/Caddy
path routing, Forgejo mirror setup, the provider->world update
cycle, and remote smoke tests.
Validated end-to-end on the REAL log: all 10 endpoints, online-fetched
proof re-verified locally through the dogfood verifier with pinning,
online pin refresh, publish + witness audit green, tamper caught,
standalone verify.py green in the published clone. 54/54 tests.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The dogfood principle now runs in BOTH directions. Agents already
verified signatures through the proven dalek path; now the provider
SIGNS with it too, and proves to itself that the signing code is in its
own log before every signature:
- dogfood binary gains a `sign` mode (seed over stdin, never argv;
ed25519_dalek::SigningKey from the same pinned merkleized workspace).
Honesty ledger unchanged: the library's VERIFY path is
certificate-covered; its signing path is declared trusted base - but
it is the ATTESTED artifact, not an un-attested third implementation.
- sign_payload_ed25519_detailed: signing dispatch mirroring the verify
dispatch; the backend that actually signed is recorded in every
attestation signature block and STH.
- THE SELF-REFERENTIAL CHECK: before signing any tree head, the
provider runs the SAME Merkle inclusion verification an agent runs -
against the very tree it is about to sign - for the newest leaf
attesting the signing library itself, and embeds the result in the
signature block:
signing_provenance:
signing_backend: verified-dalek-serial
signing_library_component: dalek-ed25519-verified
signing_library_source_commit: aa0f6ab...
self_inclusion: verified
signing_library_leaf_index: 4
signing_library_certificates_proven: 16/16
A root signature that names the leaf vouching for the code that
produced it. First-append chicken-and-egg is handled honestly
(self_inclusion: library_not_in_log).
- Evidence refreshed: all four receipts re-issued under dogfood-signed
STHs; the full agent verify loop re-run green.
50/50 tests (new signing roundtrip test, skip-safe where unbuilt).
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The provider ran its full honest replay against the four verified
repositories on this machine - every Lean compile and axiom audit routed
through lean-guard (memory-capped, core-pinned, single-flight, ~30 min
per fork) - and the results are now shipped under evidence/:
- 16/16 certificates proven per fork, every axiom cone boundary-exact
(the four apex tiers carry their fork's documented SHA-512/wire
boundary axiom-for-axiom), each attestation pinned to the exact repo
commit (dalek 8ded7bc, anza 673c15e, risc0 98a13a6, betrusted
81f614a) and Ed25519-signed.
- All four appended to the persistent transparency log. The log holds
EIGHT leaves: the first four are the initial run's attestations,
which honestly recorded an AUDIT FAILURE (the two pacta bugs fixed in
e87f0e8) - an append-only trust ledger keeps its bad day, and the
fixed run's leaves sit beside it.
- Every receipt re-verified through the FULL stack: dogfood verifier
(backend verified-dalek-serial recorded), STH pin store, freshness
policy. Receipts are freshly issued against the final tree (a stale
mid-run receipt tripped the pin store's rollback defense exactly as
designed; the rollback diagnostic now hints at idempotent re-issue).
- The capstone consequence ran for real: pacta agent with trusted
provider + signature via the proven path + required receipt + pin
store + --require-verified-verifier built the R4-gated library
capsule from ATTESTED evidence (no local Lean replay needed by the
consuming agent).
Docs and teaching updated against the real artifacts: evidence/README
(inventory + re-verify instructions), README "Real Evidence" section,
lecture 5 now re-derives 16/16 verdicts from the REAL dalek attestation
(signature checked on the proven path, provider labels ignored), and
lecture 6 verifies all four REAL receipts and walks a fresh pin store
over them. Every changed notebook cell executed before commit. 49/49
tests green.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The first live four-fork replay was a system success and a content
failure: all 256 file compiles ran green under lean-guard, and the
provider SIGNED ATTESTATIONS OF FAILURE rather than hiding that its
audit phase broke - exactly the fail-closed behavior the design
demands. Two defects, both mine:
1. Guarded axiom audits lost --root: the audit's temp .lean lives
outside the toolchain root; guard mode now forwards
--root=<temp dir> exactly as it does for repo files.
2. The cone parser was single-line: Lean wraps the apex tiers'
11-axiom boundaries across lines, so the four apex certificates
parsed as empty/dirty. The parser now flattens a 16-line window
(the same move the corpus' check scripts make) - unit-tested on a
real wrapped transcript.
Validated standalone against dalek's fresh oleans: 16/16 certificates
proven with boundary-exact cones; the observed full-lift cone equals
the documented dalek boundary axiom-for-axiom. 49/49 tests green.
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>
"Eat your own dogfood": pacta consumes certificates about a verified
Ed25519 implementation while checking those certificates' signatures
with OpenSSL. Now it can use the object of its own evidence:
- dogfood/pacta-verified-verify: a ~90-line Rust binary built against
the PINNED proven source workspace (saymrwulf/curve25519-dalek-source
at the exact commit the dalek certificates pin - the build records it:
aa0f6ab...) with the serial backend pinned via RUSTFLAGS exactly as
the verified extraction pins it. Cargo.toml is committed as a template
({{SOURCE}} placeholder) so no machine path is hardcoded; the rendered
file, target/, and the built binary are gitignored.
- pacta dogfood-build --source <workspace>: renders, builds, installs
to dogfood/state/, and writes a provenance sidecar (source commit,
backend cfg, rustc, and an honest coverage note: the certificates
cover verify_sha512, the extraction-refactored image of this verify
path; SHA-512 and the wire glue remain the theorems' documented
boundary). pacta dogfood-status reports the active backend.
- signing.verify_payload_ed25519_detailed: dispatch - the dogfood
binary when present (backend "verified-dalek-serial"), OpenSSL
fallback otherwise, and the backend that ACTUALLY ran is recorded in
receipt signature statuses and attestation evidence. Fallback is
never silent.
- --require-verified-verifier (receipt-verify + agent): policy fails
closed when verification did not run on the certificate-covered
path.
- ML-DSA is deliberately unchanged: no proven implementation exists,
so the slot stays fail-closed "unavailable" - the honest hybrid-PQC
posture is one proven-classical signature plus one required-but-
unproven PQC slot, never a pretend backend.
Validated live: receipt verification through the proven verifier
(backend recorded), a corrupted signature bit rejected BY the proven
binary, tampered attestations rejected, and the policy failing closed
when the binary is absent. 49/49 tests green (incl. PEM-SPKI raw-key
cross-check against openssl, dispatch/backend recording with a stub,
and a real-binary roundtrip that skips gracefully where unbuilt).
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
A transparency log without split-view defense is just a signature with
extra steps: the provider could serve one tree to the agent and another
to the world, or roll the log back, and standalone receipt verification
would never notice. The primitives (RFC 9162 consistency proofs) were
already implemented and correct; this closes the loop on the AGENT side.
- src/pacta/sthstore.py: a local STH pin store. Unknown log -> pin
(trust-on-first-use, recorded as such). Same tree size -> the root
must match the pin byte-for-byte; a mismatch is named EQUIVOCATION
and is a hard rejection. Larger tree -> a consistency proof FROM THE
PINNED SIZE is required and verified before the pin advances
(receipts already embed a from-previous anchor; the anchor's root is
itself checked against the pin so a lying anchor cannot bridge a
split view). Smaller tree -> LOG ROLLBACK, hard rejection.
- Freshness policy: --max-sth-age-seconds rejects stale (or
future-dated) tree heads - an old-but-valid STH can hide later
entries.
- Wired into receipt-verify, claims, and agent (--sth-store,
--consistency-proof, --max-sth-age-seconds); evidence records the
pin action; any accountability failure fails the receipt closed.
- Provider: log-consistency --from-size N (serve proofs for pinning
agents whose pin is older than the receipt's embedded anchor) and
log-audit (monitor self-check: recompute the tree, verify the stored
STH and per-entry leaf hashes).
Live drill in this commit's validation: pin-on-first-use -> matched ->
grown-with-proof advance -> a real forged same-size split view REJECTED
with the equivocation diagnostic -> freshness rejection -> clean
self-audit. tests/test_sthstore.py covers pin/match/equivocation,
growth-without-proof, lying consistency anchors, rollback, freshness.
45/45 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>
