mirror of
https://github.com/saymrwulf/proof-aware-crypto-tooling-agent.git
synced 2026-09-04 20:03:40 +00:00
Compare commits
5 commits
469a962825
...
31a9dee10a
| Author | SHA1 | Date | |
|---|---|---|---|
| 31a9dee10a | |||
| 7e9e557187 | |||
| 7cc5982af3 | |||
| 57ac2095c0 | |||
| 03de38eaac |
8 changed files with 76 additions and 34 deletions
13
ESTATE.md
13
ESTATE.md
|
|
@ -9,9 +9,10 @@ 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.11 (25 pp, revised August 2026)**, six attested
|
||||
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 153 green.
|
||||
entry), pacta suite 157 green.
|
||||
|
||||
```mermaid
|
||||
flowchart LR
|
||||
|
|
@ -37,7 +38,7 @@ flowchart LR
|
|||
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.11 (archives in git history)"]
|
||||
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"]
|
||||
|
|
@ -119,10 +120,10 @@ deployed verifier; see the corpus KNOWN-GAPS ledger).
|
|||
|
||||
| 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** |
|
||||
| `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 layer proven; curve layer pending; **not attested** | changes freely |
|
||||
| `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** |
|
||||
|
|
@ -134,7 +135,7 @@ deployed verifier; see the corpus KNOWN-GAPS ledger).
|
|||
|
||||
| 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. Deployment configuration is maintained privately. |
|
||||
| **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. |
|
||||
|
|
|
|||
2
llms.txt
2
llms.txt
|
|
@ -20,7 +20,7 @@
|
|||
## Live evidence
|
||||
|
||||
- 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.
|
||||
- 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.15, revised August 2026, DOI 10.5281/zenodo.22057482: 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
|
||||
|
||||
|
|
|
|||
|
|
@ -17,7 +17,10 @@ two-sided dilemma explicitly in the introduction and aligns the
|
|||
introduction's question with the abstract (label, not verdict). The
|
||||
version submitted for review (July 17, 2026, sha256 `7f140356…`) is
|
||||
preserved unchanged in this repository's git history. The live copy at
|
||||
<https://ltl.zkdefi.org/paper> serves the current revision.
|
||||
<https://ltl.zkdefi.org/paper> serves the current revision; the v0.15
|
||||
revision is archived with DOI
|
||||
[10.5281/zenodo.22057482](https://doi.org/10.5281/zenodo.22057482)
|
||||
(CC BY 4.0).
|
||||
|
||||
Superseded early drafts (v0.1, v0.2) were removed from the working tree
|
||||
on 2026-08-15; like every prior state of this folder, they remain
|
||||
|
|
@ -25,4 +28,4 @@ retrievable from this repository's git history.
|
|||
|
||||
Revisions v0.3–v0.9 were successive overwrites of `ltl.tex`; they live in
|
||||
this repository's git history. v0.9 is the version that was submitted
|
||||
for review; v0.10 and v0.11 supersede it.
|
||||
for review; v0.10 through v0.15 supersede it (history above).
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
% Reconstructed directly from the 1344-line rejected ltl.tex and its PDF,
|
||||
% using reinvention-outline.md and the live 13-leaf deployment as factual patch.
|
||||
% Reinvented August 2026 from the round-11 review of the prior draft;
|
||||
% the full revision history lives in this folder's README.md.
|
||||
\documentclass[11pt]{article}
|
||||
\usepackage[a4paper,margin=1.02in]{geometry}
|
||||
\usepackage{amsmath,amssymb,amsthm,mathtools}
|
||||
|
|
|
|||
|
|
@ -508,7 +508,7 @@ 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** (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**
|
||||
and its heads carry a **second, post-quantum SLH-DSA-SHA2-128s signature**
|
||||
beside the required Ed25519 one. The current head is `latest-sth.json` —
|
||||
this README deliberately names no tree size, so it cannot go stale.
|
||||
|
||||
|
|
@ -536,6 +536,9 @@ python3 verify.py --receipt receipts/dalek-ed25519-verified.receipt.json
|
|||
The online service (same data, live endpoints + customer documentation):
|
||||
**https://ltl.zkdefi.org**
|
||||
|
||||
The design and its security analysis:
|
||||
**https://ltl.zkdefi.org/paper** (DOI [10.5281/zenodo.22057482](https://doi.org/10.5281/zenodo.22057482))
|
||||
|
||||
The provider tooling, agent tooling, and course materials:
|
||||
**https://github.com/saymrwulf/proof-aware-crypto-tooling-agent**
|
||||
|
||||
|
|
@ -548,7 +551,7 @@ trust ledger keeps its history. Tree heads are signed by the merkleized,
|
|||
proof-attested Ed25519 library itself, and each signature embeds the
|
||||
provider's own Merkle self-check of that library's leaf. Heads additionally
|
||||
carry a **deterministic SLH-DSA-SHA2-128s signature** over the same payload:
|
||||
additive, so Ed25519 remains the signature a consumer must check, and honest
|
||||
strictly additional, so Ed25519 remains the signature a consumer must check, and honest
|
||||
about scope — the estate's certificates cover the *verification* path of both
|
||||
algorithms; no signing operation is proven for either, and leaves themselves
|
||||
are Ed25519-signed at issuance only. Heads published before 2026-08 have no
|
||||
|
|
|
|||
|
|
@ -67,6 +67,16 @@ def make_handler(log: TransparencyLog, base_path: str, docs_html: str, paper_pdf
|
|||
except Exception as exc: # noqa: BLE001 - the service must not die on a bad request
|
||||
self._send(500, {"error": f"internal error: {type(exc).__name__}"})
|
||||
|
||||
def do_HEAD(self) -> None: # noqa: N802 - link checkers and mail/chat
|
||||
# unfurlers probe with HEAD; answer with the same headers as GET
|
||||
# and no body (a 501 here makes every link look broken to them).
|
||||
self._head_only = True
|
||||
self.do_GET()
|
||||
|
||||
def _body(self, body: bytes) -> None:
|
||||
if not getattr(self, "_head_only", False):
|
||||
self.wfile.write(body)
|
||||
|
||||
def _route(self) -> None:
|
||||
parsed = urlparse(self.path)
|
||||
path = parsed.path.rstrip("/")
|
||||
|
|
@ -79,7 +89,7 @@ def make_handler(log: TransparencyLog, base_path: str, docs_html: str, paper_pdf
|
|||
if route in ("/", "/docs"):
|
||||
self._send_html(docs_html)
|
||||
elif route in ("/paper", "/paper/ltl.pdf"):
|
||||
# /paper serves the current paper only (v0.11, revised
|
||||
# /paper serves the current paper only (v0.15, revised
|
||||
# August 2026). Superseded drafts were retired from the
|
||||
# site 2026-08-15; git history retains them.
|
||||
body = paper_pdfs.get("current")
|
||||
|
|
@ -91,7 +101,7 @@ def make_handler(log: TransparencyLog, base_path: str, docs_html: str, paper_pdf
|
|||
self.send_header("Content-Disposition", 'inline; filename="ltl.pdf"')
|
||||
self.send_header("Content-Length", str(len(body)))
|
||||
self.end_headers()
|
||||
self.wfile.write(body)
|
||||
self._body(body)
|
||||
elif route in ("/log-public-key", "/log-slhdsa-public-key"):
|
||||
# TOFU mitigation depends on the key being published in two
|
||||
# independent locations; this is the site's copy (the mirror
|
||||
|
|
@ -110,7 +120,7 @@ def make_handler(log: TransparencyLog, base_path: str, docs_html: str, paper_pdf
|
|||
self.send_header("Content-Type", "text/plain; charset=utf-8")
|
||||
self.send_header("Content-Length", str(len(body)))
|
||||
self.end_headers()
|
||||
self.wfile.write(body)
|
||||
self._body(body)
|
||||
elif route == "/openapi.json":
|
||||
self._send(200, _openapi_document(base))
|
||||
elif route == "/healthz":
|
||||
|
|
@ -222,7 +232,7 @@ def make_handler(log: TransparencyLog, base_path: str, docs_html: str, paper_pdf
|
|||
self.send_header("Content-Length", str(len(body)))
|
||||
self.send_header("X-Robots-Tag", "noindex, nofollow")
|
||||
self.end_headers()
|
||||
self.wfile.write(body)
|
||||
self._body(body)
|
||||
return True
|
||||
|
||||
def _send(self, code: int, payload: dict[str, Any], code_if_error: int | None = None) -> None:
|
||||
|
|
@ -234,7 +244,7 @@ def make_handler(log: TransparencyLog, base_path: str, docs_html: str, paper_pdf
|
|||
self.send_header("Content-Length", str(len(body)))
|
||||
self.send_header("Cache-Control", "no-store")
|
||||
self.end_headers()
|
||||
self.wfile.write(body)
|
||||
self._body(body)
|
||||
|
||||
def _send_html(self, html: str) -> None:
|
||||
body = html.encode("utf-8")
|
||||
|
|
@ -242,7 +252,7 @@ def make_handler(log: TransparencyLog, base_path: str, docs_html: str, paper_pdf
|
|||
self.send_header("Content-Type", "text/html; charset=utf-8")
|
||||
self.send_header("Content-Length", str(len(body)))
|
||||
self.end_headers()
|
||||
self.wfile.write(body)
|
||||
self._body(body)
|
||||
|
||||
def log_message(self, fmt: str, *args: Any) -> None: # quiet by default
|
||||
pass
|
||||
|
|
|
|||
|
|
@ -397,21 +397,16 @@ our roadmap.</strong> (The full walk-through is lecture 11 of the Jupyter c
|
|||
<h2>The paper</h2>
|
||||
<div class="card"><a href="{base}/paper"><strong>Accountable Distribution of Machine-Checked
|
||||
Correctness Evidence: A Transparency Model and the Lean Transparency Log</strong></a>
|
||||
(PDF, 25 pages, <strong>v0.15 — revised August 2026</strong>; the version is printed on the
|
||||
title page) — the trust decomposition (expensive verification produces an
|
||||
observation; transparency makes the observation accountable; consumer-local policy decides
|
||||
acceptance), collision-extracting soundness for inclusion and consistency, scheme-level
|
||||
accountability GAMES with an explicit composition theorem (head authenticity, position
|
||||
binding, history binding with a fully proved prefix-transport induction, context-scoped
|
||||
fork evidence — all discharged by named reductions), the policy boundary where
|
||||
operator labels can veto but never grant acceptance, and the measured model/deployment
|
||||
divergence reported as a result rather than hidden — now together with its closure: the
|
||||
divergence traced to one omitted RFC 9162 conjunct (Step 7's <code>sn = 0</code>),
|
||||
zero divergences after the one-line restoration, confirmed by a three-way regression.
|
||||
New in the August 2026 revisions: the deployment evaluated to its current nineteen-leaf, dual-signed state, an
|
||||
instantiation section for the SLH-DSA (FIPS 205) verify path — eleven certificates,
|
||||
five uninterpreted hash oracles, exact cones — and a certificate appendix mirroring the
|
||||
Ed25519 tiers.</div>
|
||||
(PDF, 25 pages · v0.15, August 2026 · DOI
|
||||
<a href="https://doi.org/10.5281/zenodo.22057482">10.5281/zenodo.22057482</a>).
|
||||
The full design and its security analysis: what the log guarantees, stated as
|
||||
precise games with proofs — and what it deliberately does not guarantee, with
|
||||
the same honesty discipline as this page, at referee depth. It also tells the
|
||||
project’s best war story: the mechanized model caught our own deployed
|
||||
verifier omitting a single condition of RFC 9162 — invisible to ordinary
|
||||
testing, 3,867 wrong acceptances across 73,573 adversarial cases, zero after
|
||||
the one-line fix. If you read one thing, read the claim matrix at the end:
|
||||
every promise, what establishes it, and what remains assumed.</div>
|
||||
|
||||
|
||||
<p class="muted">Log heads are signed offline; this service is read-only and holds no
|
||||
|
|
|
|||
|
|
@ -223,3 +223,33 @@ def test_openapi_document_served_and_valid():
|
|||
assert doc["openapi"].startswith("3.")
|
||||
assert "/v1/sth" in doc["paths"] and "/log-public-key" in doc["paths"]
|
||||
_json.dumps(doc) # serializable
|
||||
|
||||
|
||||
def test_head_requests_answer_like_get_without_body(tmp_path):
|
||||
# Link checkers and mail/chat unfurlers probe with HEAD; a 501 made
|
||||
# /paper look broken to them (found 2026-08-22 while verifying what
|
||||
# the paper link serves).
|
||||
import http.client
|
||||
import shutil
|
||||
|
||||
_make_log(tmp_path)
|
||||
shutil.copy2(tmp_path / "k.pub", tmp_path / "log" / "provider.ed25519.pub")
|
||||
server = serve(str(tmp_path / "log"), port=0)
|
||||
port = server.server_address[1]
|
||||
import threading
|
||||
|
||||
thread = threading.Thread(target=server.serve_forever, daemon=True)
|
||||
thread.start()
|
||||
try:
|
||||
conn = http.client.HTTPConnection("127.0.0.1", port, timeout=10)
|
||||
for route, ctype in [("/", "text/html"), ("/v1/sth", "application/json"),
|
||||
("/log-public-key", "text/plain")]:
|
||||
conn.request("HEAD", route)
|
||||
r = conn.getresponse()
|
||||
body = r.read()
|
||||
assert r.status == 200, (route, r.status)
|
||||
assert ctype in r.getheader("Content-Type", ""), route
|
||||
assert body == b"", (route, len(body))
|
||||
assert int(r.getheader("Content-Length", "0")) > 0, route
|
||||
finally:
|
||||
server.shutdown()
|
||||
|
|
|
|||
Loading…
Reference in a new issue