proof-aware-crypto-tooling-agent/ESTATE.md

The estate map

One page holding the entire mental model of the Lean Transparency Log endeavour: every repository, service, mirror, and operator-held entity, and — most importantly — the typed relationships between them, including the two self-referential loops that make the estate hard to keep in one head. Maintained here in pacta because pacta is the machinery hub and the only repo that changes freely.

State snapshot (2026-08-16): log 19 leaves, root 7ee23940…, key fingerprint 874c8a00…, heads dual-signed (Ed25519 + SLH-DSA) since size 14, paper v0.15 (25 pp, revised August 2026; DOI 10.5281/zenodo.22057482), six attested components (SLH-DSA verify path = leaf 18, the first post-quantum entry), pacta suite 157 green.

flowchart LR
  subgraph S["UPSTREAM INPUTS (frozen clones)"]
    s1["curve25519-dalek-source"]
    s2["anza-cryptography-source"]
    s3["risc0-…-dalek-source"]
    s4["betrusted-…-dalek-source"]
    s5["pasta_curves-source"]
    s6["fips205-source"]
  end
  subgraph V["VERIFIED SUBJECTS"]
    d["dalek-ed25519-verified<br/>attested 44/44 (leaf 13 · signer source; earlier gens 0/4/8)"]
    a["anza-ed25519-verified<br/>attested 44/44 (leaf 14; earlier gens 1/5/9)"]
    r["risc0-ed25519-verified<br/>attested 44/44 (leaf 15; earlier gens 2/6/10)"]
    b["betrusted-ed25519-verified<br/>attested 44/44 (leaf 16; earlier gens 3/7/11)"]
    p["pasta-pallas-verified<br/>field layer only · NOT attested"]
    f["fips205-slhdsa-verified<br/>11 certs proven · attested — leaf 18 (first post-quantum)"]
    c["ltl-accumulator-verified<br/>61 certs · leaf 12 subject · re-attested leaf 17 (hardened)"]
  end
  subgraph M["MACHINERY — pacta + operator-held"]
    prov["provider service<br/>check · append · publish · site code · templates (CI-pinned)"]
    sig["dogfood signer<br/>verified-dalek binary"]
    lib["consumer library<br/>receipts · pin store · R0–R5"]
    wal["warden (code)<br/>quorum wallet · MCP · cockpit (local, read-only)"]
    pap["paper<br/>v0.15 + DOI (archives in git history)"]
    crs["course + llms.txt<br/>14 notebooks"]
    key["SIGNING KEY (offline)"]
    ops["operational log state<br/>the true accumulator"]
    sd["evidence archive (offline)<br/>kits · stamps"]
  end
  subgraph P["PUBLISHED FACES"]
    mir["lean-transparency-log<br/>GENERATED mirror · fail-closed verify.py + selftest"]
    site["ltl.zkdefi.org<br/>homepage · /v1 API · /paper"]
    fj["Forgejo (droplet)<br/>nightly full-account mirror"]
    book["verifying-crypto-with-lean<br/>undergrad book (independent)"]
  end
  subgraph C2["CONSUMERS"]
    cl["offline cloner<br/>verify.py --all"]
    wr["warden (runtime)"]
    ag["agents<br/>MCP · custody card"]
    sw["swisspost-evoting-go-poc<br/>prospective, family-level only"]
    rev["external reviewers<br/>GPT-5.6 + Claude"]
  end
  s1 --> d
  s2 --> a
  s3 --> r
  s4 --> b
  s5 --> p
  s6 --> f
  d -->|attest| prov
  a -->|attest| prov
  r -->|attest| prov
  b -->|attest| prov
  prov -->|append| ops
  key -->|signs heads| ops
  ops -->|publish| mir
  prov -.->|"templates (CI-pinned)"| mir
  prov -->|app code| site
  mir -->|published copy| site
  pap -->|/paper| site
  mir -.->|nightly| fj
  mir -->|clone + verify| cl
  site -->|API · custody card| ag
  mir -->|receipts · quorum| wr
  site -.->|prospective| sw
  sd -->|review kits| rev
  d ==>|"LOOP 1: built from"| sig
  sig ==>|"LOOP 1: signs the log"| ops
  mir ==>|"LOOP 1: contains the signer's own attestation (leaf 8)"| d
  c ==>|"LOOP 2: attested as leaf 12 (13th entry)"| prov
  mir ==>|"LOOP 2: carries proofs about its own accumulator"| c
  classDef src fill:#f1f3f5,stroke:#8a93a0,color:#1c2430
  classDef sub fill:#e2f2e9,stroke:#1e7f4f,color:#1c2430
  classDef mach fill:#eef0f7,stroke:#3b4d8f,color:#1c2430
  classDef held fill:#2b3442,stroke:#2b3442,color:#e8ecf2
  classDef pub fill:#efe9f5,stroke:#6d4a8f,color:#1c2430
  classDef cons fill:#fdf0da,stroke:#a86a10,color:#1c2430
  class s1,s2,s3,s4,s5,s6 src
  class d,a,r,b,p,c,f sub
  class prov,sig,lib,wal,pap,crs mach
  class key,ops,sd held
  class mir,site,fj,book pub
  class cl,wr,ag,sw,rev cons

The two loops (read these first)

Loop 1 — the dogfood signer. The log's tree heads are signed by verified-dalek-serial, a binary built from dalek-ed25519-verified — whose own attestation is leaf 8 inside the log it signs. Before signing, the provider re-checks inclusion of the signer's leaf. The signature vouches for the tree; the tree contains the proofs of the signer's source. (Execution provenance is reported, not proven — the paper says so explicitly.)

Loop 2 — the self-attestation. ltl-accumulator-verified is a Lean corpus proving soundness of the log's own accumulator model (extractors, consistency binding, per-step pin safety). It was attested into the log as leaf 12 (the log's thirteenth entry) — the log carries kernel-checked proofs about its own machinery, scoped honestly (recursive model, not the deployed verifier; see the corpus KNOWN-GAPS ledger).

Repository inventory

Repository	Lane	Role	Mutability
curve25519-dalek-source, anza-cryptography-source, risc0-…-source, betrusted-…-source, pasta_curves-source (+ xous-core context)	upstream	pinned inputs to extraction	frozen — never modified
fips205-source	upstream	verbatim snapshot of integritychain/fips205 (pure-Rust FIPS 205 / SLH-DSA); upstream pin 30bac08, snapshot head a3ce8e8 — deviations: CI workflows stripped + the documented Aeneas-compat/de-plumbing patch series (each commit individually justified)	pinned; moves only for transparent, individually-justified Aeneas-compat patches (nothing proposed upstream)
dalek- / anza- / risc0- / betrusted-ed25519-verified	subject	Rust source + Lean proofs; 44 certs each, attested 44/44 as leaves 13–16 (2026-08-08); earlier 16-cert generations at leaves 8–11, first generations at 0–7	attested commits fixed
pasta-pallas-verified	subject	field foundation proven (sub/neg, helpers, constants, primality, denotation); field completion and curve layer pending; not attested	changes freely
fips205-slhdsa-verified	subject	SLH-DSA (FIPS 205) verify-path campaign, parameter set SLH-DSA-SHA2-128s; 11 certificates proven, check.sh green with an 18-attack self-test; attested — leaf 18 (2026-08-08), the log's first post-quantum entry	attested commit fixed
ltl-accumulator-verified	subject	61-cert corpus about the log's accumulator model; leaf 12 subject, frozen 172a1d0; hardened model re-attested as leaf 17 (2026-08-08)	frozen; doc-only commits allowed
proof-aware-crypto-tooling-agent (this repo)	machinery	provider service, consumer library, warden (+ local read-only cockpit), dogfood signer, paper, course, tests	changes freely — the hub
lean-transparency-log	published	the public mirror: leaves, heads, receipts, fail-closed verify.py + selftest	generated by publish — canonical files here, templates in pacta, CI-pinned
verifying-crypto-with-lean	published	undergraduate book; zero coupling to log state	changes freely
swisspost-evoting-go-poc	consumer	operator's PoC; prospective consumer (family-level dalek match only)	independent

Services, infra, operator-held

Entity	What it is
ltl.zkdefi.org	droplet (caddy → docker cloud-ltl-1): homepage rendered from live leaves, /v1 API, /paper, key endpoint. Read-only; no key material on the server. Deployment configuration is maintained privately.
Forgejo (cloud-forgejo-1)	nightly (03:00) mirror of the entire saymrwulf GitHub account — disaster-recovery copy.
Signing key	offline, operator-only; fingerprint 874c8a00…; never on the server; public half published in two independent locations.
Operational log state	provider/state/transparency-log-main — the true accumulator. Appends happen here; the mirror is its projection.
Evidence archive (offline)	review kits and stamped artifacts (_timestamp_hash8 convention); never in git.

What is running (operations, verified 2026-07-20; campaign rows 2026-07-22)

Entity	Runtime	Where	Starts / stops
caddy (TLS, static blog)	always on	droplet container	docker compose, restart-unless-stopped
LTL web service (ltl.zkdefi.org)	always on	droplet container	pacta_provider serve with read-only mounts and read_only: true — it cannot write, sign, or append
Forgejo mirror	always on	droplet container	plus exactly one cron: 03:00 daily mirror reconcile
provider write side (check / append / publish / sign)	on demand	operator machine	runs only during an append ceremony, minutes at a time; the signing key is offline otherwise
warden (the financial agent)	not running	nowhere	implemented prototype: a wallet directory plus CLI/MCP/cockpit processes that exist only while explicitly started; no deployed instance, no funds watched
custody cockpit	on demand	operator machine, localhost	pacta wallet cockpit, stops with Ctrl-C; read-only
SLH-DSA campaign (fips205-source + fips205-slhdsa-verified)	no process	—	static repos, 11 certificates; extraction/proof sessions are episodic operator-machine runs under lean-guard
everything else (repos, paper, book, mirror, SD)	no process	—	static files; consumers and reviewers are external and episodic

The human-facing interactive rendering of this whole map, runtime dimension included, is the cockpit's Estate map view (pacta wallet cockpit → /estate); this file remains the canonical committed version, and tests/test_walletui.py guards name-level drift between the two.

Edge glossary

Edge	Meaning
extract	pinned source → Lean model (Aeneas/Charon)
attest	subject at pinned commit → provider check → signed leaf
append / publish	leaf → operational state → generated mirror
templates (CI-pinned)	pacta published_assets → mirror's verify.py/selftest/README; guarded by tests/test_published_assets.py since 2026-07-19
serve	pacta app + mirror copy + paper → droplet → site
consume	mirror/site → cloners, warden, agents (receipts recomputed, never trusted)

Maintenance

Update this file when: a leaf is appended or a head signed (snapshot line), the paper version changes, a repo/service/consumer is added or retired, or a loop-relevant mechanism changes. Rules that keep the map honest: generated artifacts are fixed at their source (mirror files → pacta templates); subject repos move only for docs; the three operator-held entities are never expanded into detail here, and the private infrastructure layer is deliberately unnamed — this map lists only entities whose existence is already public or must be public for trust.