diff --git a/ESTATE.md b/ESTATE.md index 7ae7346..57ecb24 100644 --- a/ESTATE.md +++ b/ESTATE.md @@ -7,10 +7,11 @@ 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-22): log **13 leaves**, root `3488a2d0…`, key -fingerprint `874c8a00…`, paper **v0.9 camera-ready (23 pp)**, five -attested components, one campaign open (SLH-DSA — **eleven -certificates**), pacta suite 144 green. +State snapshot (2026-08-16): log **19 leaves**, root `7ee23940…`, key +fingerprint `874c8a00…`, heads dual-signed (Ed25519 + SLH-DSA) since +size 14, paper **v0.11 (25 pp, revised August 2026)**, six attested +components (SLH-DSA verify path = leaf 18, the first post-quantum +entry), pacta suite 153 green. ```mermaid flowchart LR @@ -23,20 +24,20 @@ flowchart LR s6["fips205-source"] end subgraph V["VERIFIED SUBJECTS"] - d["dalek-ed25519-verified
44 certs today · attested at 16 (leaf 8 · signer source)"] - a["anza-ed25519-verified
44 certs today · attested at 16 (leaf 9)"] - r["risc0-ed25519-verified
44 certs today · attested at 16 (leaf 10)"] - b["betrusted-ed25519-verified
44 certs today · attested at 16 (leaf 11)"] + d["dalek-ed25519-verified
attested 44/44 (leaf 13 · signer source; earlier gens 0/4/8)"] + a["anza-ed25519-verified
attested 44/44 (leaf 14; earlier gens 1/5/9)"] + r["risc0-ed25519-verified
attested 44/44 (leaf 15; earlier gens 2/6/10)"] + b["betrusted-ed25519-verified
attested 44/44 (leaf 16; earlier gens 3/7/11)"] p["pasta-pallas-verified
field layer only · NOT attested"] - f["fips205-slhdsa-verified
11 certs proven · reviewer attest-with-conditions · NOT in the log"] - c["ltl-accumulator-verified
61 certs · entry-13 subject · frozen 172a1d0"] + f["fips205-slhdsa-verified
11 certs proven · attested — leaf 18 (first post-quantum)"] + c["ltl-accumulator-verified
61 certs · leaf 12 subject · re-attested leaf 17 (hardened)"] 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 · cockpit (local, read-only)"] - pap["paper
v0.9 + v0.1/v0.2 archives"] + pap["paper
v0.11 (archives in git history)"] crs["course + llms.txt
14 notebooks"] key["SIGNING KEY (offline)"] ops["operational log state
the true accumulator"] @@ -81,7 +82,7 @@ flowchart LR 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 + 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 @@ -110,7 +111,7 @@ 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 +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). @@ -120,10 +121,10 @@ deployed verifier; see the corpus KNOWN-GAPS ledger). |---|---|---|---| | `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** | | `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 today (27 main + 4 apex + 13 scalar; 16 at the leaf 8–11 attestations, generations at 0–7) | attested commits fixed; branches carry substantial post-attestation proof work (scalar layer, apex tier, hardening rounds), staged for re-attestation | +| `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 layer proven; 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, outside-reviewer attest-with-conditions**; not appended to the log | changes freely — campaign | -| `ltl-accumulator-verified` | subject | 61-cert corpus about the log's accumulator model; **entry-13 subject**, frozen `172a1d0` | frozen; doc-only commits allowed | +| `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 | diff --git a/README.md b/README.md index d18ae74..8bdd577 100644 --- a/README.md +++ b/README.md @@ -324,7 +324,9 @@ The log has three synchronized faces, transport being orthogonal to trust: 2. **Git mirror** ([saymrwulf/lean-transparency-log](https://github.com/saymrwulf/lean-transparency-log), mirrored on Forgejo): every leaf, every signed tree head (the WITNESS CHANNEL - all cloners see the same heads), per-component receipts, the provider public key, - and a standalone stdlib-only `verify.py`. Anyone: `python3 verify.py --all`. + and a standalone `verify.py` (Python stdlib + the system `openssl` + binary; fails closed without it). Anyone, from inside a clone: + `python3 verify.py --all`. 3. **HTTP service** (deployed at `ltl.zkdefi.org`, see `DEPLOY.md`): read-only CT-style endpoints + customer docs. The web process never touches private keys - heads are signed offline; a diff --git a/docs/security-2026-07-23-consistency-terminal-check.md b/docs/security-2026-07-23-consistency-terminal-check.md index 0ec8d64..8c81f83 100644 --- a/docs/security-2026-07-23-consistency-terminal-check.md +++ b/docs/security-2026-07-23-consistency-terminal-check.md @@ -68,14 +68,14 @@ return old_hash == old_root_hash and new_hash == new_root_hash and sn == 0 This defect is the corpus's Known Gap 14: the project's own fidelity harness **found** the divergence (3,867 deployed-accepts-only cases in a pinned -73,573-case family) and recorded it in public log entry 13. What the two-way +73,573-case family) and recorded it in public log leaf 12 (the thirteenth entry). What the two-way harness could not do was assign blame — with only the deployed verifier and the Lean model disagreeing, and both labelled "RFC 9162", the divergence was filed as a scoped gap rather than a conformance bug. A post-appeal review round added the missing third oracle (a faithful RFC verifier), which showed the deployed side was the deviant one, and traced it to the omitted Step 7. -Public log entry 13 and the attested accumulator commit are unchanged: the +Public log leaf 12 and the attested accumulator commit are unchanged: the historical experiment remains truthfully recorded and reproducible at the tagged pre-fix commit. The IACR submission PDF is unchanged. The corpus Known-Gaps ledger records this closure. diff --git a/docs/warden-lab-manual.md b/docs/warden-lab-manual.md index 31b951f..270e9f2 100644 --- a/docs/warden-lab-manual.md +++ b/docs/warden-lab-manual.md @@ -705,7 +705,7 @@ tripwire that screams when the map forks from itself. Ed25519 implementation that is itself verified and attested *inside the log it signs* (leaf 8). The tool guards the evidence; the evidence covers the tool. - - **Loop 2, the self-attesting mechanization:** entry 13 of the log is the + - **Loop 2, the self-attesting mechanization:** leaf 12 of the log (its thirteenth entry) is the kernel-checked mechanization of the very soundness arguments the log's accumulator relies on. The proofs about the machinery live inside the ledger the machinery protects — scoped honestly, with a published list @@ -975,7 +975,7 @@ boolean. **6.1** Loop 1: the log's signing machinery runs on an Ed25519 implementation that is itself verified and attested inside the log it -signs (leaf 8). Loop 2: entry 13 is the kernel-checked mechanization of +signs (leaf 8). Loop 2: leaf 12 is the kernel-checked mechanization of the accumulator arguments the log itself relies on — the proofs about the machinery live in the ledger the machinery protects. **6.2** Because "what is running" is invisible from any single machine and diff --git a/evidence/README.md b/evidence/README.md index 764df3c..3502684 100644 --- a/evidence/README.md +++ b/evidence/README.md @@ -17,10 +17,11 @@ today's full state. | `log-metadata.json`, `latest-sth.yaml` | Log identity and the Signed Tree Head at capture time (tree size 8) | | `log-audit.txt` | Monitor self-check output (recomputed root matches the signed root) | -The log holds EIGHT leaves: entries 0-3 are the first run's attestations, +At the time of this capture (2026-07) the log held eight leaves: entries 0-3 are the first run's attestations, which honestly record an AUDIT FAILURE (two bugs in pacta's audit step, -since fixed - see the commit history); entries 4-7 are the definitive -16/16-proven attestations. An append-only trust ledger keeps its bad day. +since fixed - see the commit history); entries 4-7 are that run's +16/16-proven attestations (the forks were later re-attested at 44/44 as +leaves 13-16; the live log now holds nineteen leaves). An append-only trust ledger keeps its bad day. Re-verify everything yourself (signature via the proven-path verifier if built, STH pinning, freshness): diff --git a/llms.txt b/llms.txt index 3ded030..8bc8520 100644 --- a/llms.txt +++ b/llms.txt @@ -19,8 +19,8 @@ ## Live evidence -- Transparency log (RFC 9162): https://ltl.zkdefi.org — signed replay attestations of the Lean proofs. Thirteen leaves: three replay generations over four Ed25519 forks, plus entry 13 attesting the Lean mechanization of the log's own accumulator model. The mirror ships a fail-closed offline verifier (verify.py --all covers every leaf, signed head, and receipt) with an adversarial self-test. -- The paper: https://ltl.zkdefi.org/paper — "Accountable Distribution of Machine-Checked Correctness Evidence: A Transparency Model and the Lean Transparency Log" (23 pages: trust decomposition, scheme-level accountability games with explicit reductions, live deployment, and the measured model/deployment divergence reported as a result). Earlier versions archived at /paper/v0.2 (19 pages) and /paper/v0.1 (4 pages). +- Transparency log (RFC 9162): https://ltl.zkdefi.org — signed replay attestations of the Lean proofs. Nineteen leaves: three replay generations over four Ed25519 forks (newest at 44/44 certificates, leaves 13-16), the Lean mechanization of the log's own accumulator model (leaves 12 and 17), and the first post-quantum leaf - the SLH-DSA (FIPS 205) verify path (leaf 18); heads dual-signed (Ed25519 + SLH-DSA) since size 14. The mirror ships a fail-closed offline verifier (verify.py --all covers every leaf, signed head, and receipt) with an adversarial self-test. +- The paper: https://ltl.zkdefi.org/paper — "Accountable Distribution of Machine-Checked Correctness Evidence: A Transparency Model and the Lean Transparency Log" (25 pages, v0.11, revised August 2026: trust decomposition, scheme-level accountability games with explicit reductions, live deployment, and the measured model/deployment divergence reported as a result). Superseded drafts remain retrievable from the repository git history. ## For agents diff --git a/provider/README.md b/provider/README.md index 2ec9b40..1a5572d 100644 --- a/provider/README.md +++ b/provider/README.md @@ -2,7 +2,7 @@ This nested project is a prototype third-party proof-checking service. It reuses host Lean/Aeneas infrastructure, runs portable PACTA replay/audit checks, and emits signed attestation certificates. -It does not modify anything outside this repository. It may read configured toolchains such as `/Users/oho/GitClone/ClaudeCodeProjects/your-lean-project/aeneas-toolchain/env.sh`. +It does not modify anything outside this repository. It may read configured toolchains such as `~/aeneas-toolchain/env.sh`. It can also maintain a local transparency log. The log is an RFC 9162-style Merkle accumulator over signed attestations. It emits Signed Tree Heads with Ed25519 today; heads are dual-sign capable with an additive SLH-DSA-SHA2-128s slot (proven verify path), and the ML-DSA/FIPS 204 slot stays honestly `not_configured`/`unavailable` — never silently filled. Agents that require both signatures must reject such receipts. diff --git a/provider/src/pacta_provider/published_assets.py b/provider/src/pacta_provider/published_assets.py index 4db2f2b..018210b 100644 --- a/provider/src/pacta_provider/published_assets.py +++ b/provider/src/pacta_provider/published_assets.py @@ -498,7 +498,7 @@ This repository is the **git-published face** of a transparency log of formal-verification attestations: signed statements that the Lean 4 proofs of specific software, at specific git commits, re-check with exactly their documented assumptions. Its first twelve leaves attest four cryptographic -Rust libraries (Ed25519 implementations); as of **entry 13 (2026-07-16)** +Rust libraries (Ed25519 implementations); as of **its thirteenth entry (leaf index 12, 2026-07-16)** the log also attests **its own accumulator machinery** — a kernel-checked mechanization of the log's security analysis, so the log carries kernel-checked proofs *about the accumulator model* underlying its own @@ -506,7 +506,7 @@ inclusion and consistency reasoning, as one of its own entries (subject [`ltl-accumulator-verified`](https://github.com/saymrwulf/ltl-accumulator-verified); scoped to the mechanized model — it does not prove operator honesty, signing, or execution provenance). As of **2026-08** the log also attests -the **SLH-DSA (FIPS 205) verify-path proofs** +the **SLH-DSA (FIPS 205) verify-path proofs** (leaf 18) ([`fips205-slhdsa-verified`](https://github.com/saymrwulf/fips205-slhdsa-verified)) and its heads carry an **additive post-quantum SLH-DSA-SHA2-128s signature** beside the required Ed25519 one. The current head is `latest-sth.json` —