diff --git a/ESTATE.md b/ESTATE.md new file mode 100644 index 0000000..d872905 --- /dev/null +++ b/ESTATE.md @@ -0,0 +1,157 @@ +# 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-07-19): log **13 leaves**, root `3488a2d0…`, key +fingerprint `874c8a00…`, paper **v0.9 camera-ready (23 pp)**, five +attested components, pacta suite 118 green. + +```mermaid +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"] + end + subgraph V["VERIFIED SUBJECTS"] + d["dalek-ed25519-verified
16 certs · leaf 8 · signer source"] + a["anza-ed25519-verified
16 certs · leaf 9"] + r["risc0-ed25519-verified
16 certs · leaf 10"] + b["betrusted-ed25519-verified
16 certs · leaf 11"] + p["pasta-pallas-verified
field layer only · NOT attested"] + c["ltl-accumulator-verified
61 certs · entry-13 subject · frozen 172a1d0"] + end + subgraph M["MACHINERY — pacta + operator-held"] + prov["provider service
check · append · publish · site code · templates (CI-pinned)"] + sig["dogfood signer
verified-dalek binary"] + lib["consumer library
receipts · pin store · R0–R5"] + wal["warden (code)
quorum wallet · MCP"] + pap["paper
v0.9 + v0.1/v0.2 archives"] + crs["course + llms.txt
14 notebooks"] + key["SIGNING KEY (offline)"] + ops["operational log state
the true accumulator"] + sd["SD archive
kits · stamps · correspondence"] + end + subgraph P["PUBLISHED FACES"] + mir["lean-transparency-log
GENERATED mirror · fail-closed verify.py + selftest"] + site["ltl.zkdefi.org
homepage · /v1 API · /paper"] + fj["Forgejo (droplet)
nightly full-account mirror"] + pcs["PersonalCloudServer (private)
droplet infra as code"] + book["verifying-crypto-with-lean
undergrad book (independent)"] + end + subgraph C2["CONSUMERS"] + cl["offline cloner
verify.py --all"] + wr["warden (runtime)"] + ag["agents
MCP · custody card"] + sw["swisspost-evoting-go-poc
prospective, family-level only"] + rev["external reviewers
GPT-5.6 + Claude"] + end + s1 --> d + s2 --> a + s3 --> r + s4 --> b + s5 --> p + 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 + pcs -->|infra| 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 entry 13"| 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 src + class d,a,r,b,p,c sub + class prov,sig,lib,wal,pap,crs mach + class key,ops,sd held + class mir,site,fj,pcs,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 **entry 13** — 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`, `litex-boards` context) | upstream | pinned inputs to extraction | **frozen — never modified** | +| `dalek-` / `anza-` / `risc0-` / `betrusted-ed25519-verified` | subject | Rust source + Lean proofs; 16 certs each; attested (leaves 8–11, generations at 0–7) | frozen at attested commits; branch moves only for docs | +| `pasta-pallas-verified` | subject | field layer proven; curve layer pending; **not attested** | changes freely | +| `ltl-accumulator-verified` | subject | 61-cert corpus about the log's accumulator model; **entry-13 subject**, frozen `172a1d0` | frozen; doc-only commits allowed | +| `proof-aware-crypto-tooling-agent` (this repo) | machinery | provider service, consumer library, warden, 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 | +| `PersonalCloudServer` (private) | published | droplet infrastructure as code | 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` (+`/v0.2`, `/v0.1`), key endpoint. Read-only; no key material on the server. | +| **Forgejo** (`cloud-forgejo-1`) | nightly (03:00) mirror of the entire saymrwulf GitHub account — disaster-recovery copy. | +| **Signing key** | offline, operator-only; fingerprint `874c8a00…`; sole copy + one encrypted SD backup; 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. | +| **SD archive** | review kits (rounds 1–15), stamped artifacts (`_timestamp_hash8`), evidence records, submission correspondence (never in git). | + +## 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. diff --git a/README.md b/README.md index d20c7f8..9df2b9b 100644 --- a/README.md +++ b/README.md @@ -1,5 +1,8 @@ # proof-aware-crypto-tooling-agent +> **Lost in the estate?** [ESTATE.md](ESTATE.md) is the one-page map of +> every repo, service, mirror, and loop, with the edge semantics. + `pacta` is a local CLI prototype for interpreting formal-verification evidence in cryptographic tooling. It is not a trading bot, does not move funds, and does not make financial decisions. The immediate corpus is the `saymrwulf/*-verified` family of repositories. The shipped Lean files are treated as the verification artifact. This project intentionally does not run Charon, Aeneas, extraction, or Rust-to-Lean regeneration. diff --git a/llms.txt b/llms.txt index dc9371d..b98ec5c 100644 --- a/llms.txt +++ b/llms.txt @@ -10,6 +10,8 @@ ## Start here +- [ESTATE.md](ESTATE.md): the map of the whole endeavour — every repo, service, mirror, operator-held entity, and the two self-referential loops. + - [README.md](README.md): what pacta is, the R0–R5 risk model, the dogfood loop. - [WALLET.md](WALLET.md): warden, the verified-custody wallet — the quorum boundary, the signing firewall, the R4 gate, the MCP surface. - [docs/agent-native.md](docs/agent-native.md): why the wallet is agent-native first (AX, MCP, A2A, AP2, x402, ERC-8004) and what each idea became.