From a651a3b58c93bf4567b909527d6a1f4a9edad2ec Mon Sep 17 00:00:00 2001 From: mrwulf Date: Mon, 6 Jul 2026 16:38:37 +0200 Subject: [PATCH] The LTL website: the accumulator drawn live, artifacts named unambiguously The /docs route is now a real landing site (still one self-contained HTML, inline CSS + inline SVG, zero external assets): - One-sentence definition up top: what the LTL is and the cost asymmetry it exists for (one signature + a few hashes in milliseconds vs hours of theorem proving). - THE GRAPHIC: the accumulator itself, rendered server-side from the LIVE log at page load - real leaf hashes, real internal nodes, the real root and signature. Green leaves are boundary-exact verified attestations; grey leaves are the historical audit-failure entries, labeled "kept forever - an append-only ledger does not erase its bad day". The signature box names the dogfood backend and the provider's self-inclusion check (the signature vouches for the code; the tree vouches for the signature's code). - "What do I download?" - exactly three artifacts, numbered, each with what-it-is and where: (1) provider.ed25519.pub, the sole trust anchor, cross-checkable between this site and the GitHub mirror; (2) the attestation = the claim; (3) the receipt = the proof of inclusion. Plus the maximal-benefit path: clone the mirror, run verify.py --all, become a witness. - Three usage lanes (quick check / zero-install audit / autonomous agent), the API, and the means / does-NOT-mean cards. Rendered against the real 8-leaf log and content-asserted in tests' presence. 54/54 green. Co-Authored-By: Claude Fable 5 --- provider/src/pacta_provider/webdocs.py | 255 ++++++++++++++++++------- 1 file changed, 188 insertions(+), 67 deletions(-) diff --git a/provider/src/pacta_provider/webdocs.py b/provider/src/pacta_provider/webdocs.py index 4f3c516..357e565 100644 --- a/provider/src/pacta_provider/webdocs.py +++ b/provider/src/pacta_provider/webdocs.py @@ -1,103 +1,224 @@ -"""Customer documentation served at the log's base path — self-contained -HTML, no external assets (the service must work air-gapped behind any -reverse proxy).""" +"""The LTL website, served at the log's base path — one self-contained HTML +page (inline CSS + inline SVG, no external assets: works air-gapped behind +any reverse proxy). Rendered from the LIVE log state, so the graphic and +every number on the page are the accumulator, not a brochure about it.""" from __future__ import annotations from html import escape +from typing import Any -from .transparency_log import TransparencyLog +from pacta.transparency import node_hash + +from .transparency_log import LogEntry, TransparencyLog _STYLE = """ - body{font-family:system-ui,sans-serif;max-width:60rem;margin:2rem auto;padding:0 1rem; - color:#1c2430;line-height:1.55;background:#f8f9fa} - h1{font-size:1.6rem} h2{font-size:1.15rem;margin-top:2rem} + :root{--ink:#1c2430;--ink2:#5a6675;--line:#dde2e9;--ok:#1e7f4f;--okbg:#e2f2e9; + --warn:#a86a10;--warnbg:#fdf0da;--accent:#3b4d8f;--accentbg:#eef0f7;--bg:#f8f9fa} + *{box-sizing:border-box} + body{font-family:system-ui,sans-serif;max-width:66rem;margin:0 auto;padding:2rem 1.2rem 4rem; + color:var(--ink);line-height:1.6;background:var(--bg)} + h1{font-size:2rem;margin:.2rem 0 0;letter-spacing:-.01em} + h2{font-size:1.2rem;margin-top:2.6rem;border-bottom:2px solid var(--line);padding-bottom:.3rem} + .tagline{font-size:1.05rem;color:var(--ink2);max-width:46rem} code,pre{font-family:ui-monospace,Menlo,Consolas,monospace;background:#eef0f3;border-radius:4px} - code{padding:.1rem .3rem} pre{padding:.8rem;overflow-x:auto} - table{border-collapse:collapse;width:100%;font-size:.92rem} - td,th{border-bottom:1px solid #dde2e9;padding:.4rem .6rem;text-align:left;vertical-align:top} - .pill{display:inline-block;background:#e2f2e9;color:#1e7f4f;border-radius:9px; - padding:.05rem .55rem;font-size:.8rem;font-weight:600} - .muted{color:#5a6675;font-size:.9rem} + code{padding:.1rem .3rem;font-size:.9em} pre{padding:.9rem;overflow-x:auto;font-size:.85rem} + table{border-collapse:collapse;width:100%;font-size:.93rem;background:#fff} + td,th{border:1px solid var(--line);padding:.5rem .7rem;text-align:left;vertical-align:top} + th{background:var(--accentbg)} + .pill{display:inline-block;border-radius:9px;padding:.08rem .6rem;font-size:.78rem;font-weight:600} + .ok{background:var(--okbg);color:var(--ok)} .warn{background:var(--warnbg);color:var(--warn)} + .acc{background:var(--accentbg);color:var(--accent)} + .muted{color:var(--ink2);font-size:.9rem} + .card{background:#fff;border:1px solid var(--line);border-radius:8px;padding:1rem 1.2rem;margin:.8rem 0} + .steps{counter-reset:s} .steps .card{position:relative;padding-left:3.2rem} + .steps .card::before{counter-increment:s;content:counter(s);position:absolute;left:1rem;top:1rem; + width:1.6rem;height:1.6rem;border-radius:50%;background:var(--accent);color:#fff; + display:flex;align-items:center;justify-content:center;font-weight:700;font-size:.9rem} + svg{max-width:100%;height:auto;display:block;margin:1rem auto;background:#fff; + border:1px solid var(--line);border-radius:8px} + a{color:var(--accent)} + .legend{display:flex;gap:1.4rem;flex-wrap:wrap;font-size:.85rem;color:var(--ink2);justify-content:center} + .sw{display:inline-block;width:.8rem;height:.8rem;border-radius:3px;vertical-align:-1px;margin-right:.3rem} """ +def _leaf_ok(entry: LogEntry) -> bool: + certificates = ((entry.leaf.get("attestation") or {}).get("certificates")) or [] + return bool(certificates) and all( + certificate.get("status") == "proven" and certificate.get("axiom_status") == "clean" + for certificate in certificates + ) + + +def _svg_tree(entries: list[LogEntry], root_hex: str, signing_backend: str) -> str: + """The accumulator, drawn from its real leaves.""" + if not entries: + return "

(log is empty)

" + hashes = [bytes.fromhex(entry.leaf_hash) for entry in entries] + levels: list[list[bytes]] = [hashes] + while len(levels[-1]) > 1: + level = levels[-1] + nxt = [node_hash(level[i], level[i + 1]) for i in range(0, len(level) - 1, 2)] + if len(level) % 2: + nxt.append(level[-1]) + levels.append(nxt) + width, level_gap = 1000, 86 + height = 150 + level_gap * len(levels) + out = [f''] + positions: dict[tuple[int, int], tuple[float, float]] = {} + for level_index, level in enumerate(levels): + y = height - 56 - level_index * level_gap + span = width / (len(level) + 1) + for node_index, node in enumerate(level): + x = span * (node_index + 1) + positions[(level_index, node_index)] = (x, y) + if level_index == 0: + entry = entries[node_index] + ok = _leaf_ok(entry) + component = (((entry.leaf.get("attestation") or {}).get("subject")) or {}).get("component", "?") + fill, stroke = ("#e2f2e9", "#1e7f4f") if ok else ("#f4f4f6", "#8a93a0") + out.append(f'') + out.append(f'leaf {node_index}') + short = escape(str(component).replace("-ed25519-verified", "")) + label = short if ok else f"{short} ✗" + out.append(f'{label}') + out.append(f'{node.hex()[:10]}…') + else: + is_root = level_index == len(levels) - 1 + out.append(f'') + out.append(f'{"ROOT" if is_root else "node"}') + out.append(f'{node.hex()[:10]}…') + for child in (2 * node_index, 2 * node_index + 1): + if (level_index - 1, child) in positions: + cx, cy = positions[(level_index - 1, child)] + out.append(f'') + root_x, root_y = positions[(len(levels) - 1, 0)] + out.append(f'') + out.append(f'Signed Tree Head — Ed25519({root_hex[:12]}…)') + out.append(f'signed by: {escape(signing_backend)} (the proof-attested library itself)') + out.append(f'') + out.append("") + return "".join(out) + + def render_docs(log: TransparencyLog, base_path: str) -> str: base = "/" + base_path.strip("/") metadata = log.metadata() history = log.sth_history() - latest = history[-1] if history else {} + latest: dict[str, Any] = history[-1] if history else {} entries = log.entries() + ed = (latest.get("signatures") or {}).get("ed25519") or {} + provenance = ed.get("signing_provenance") or {} + signing_backend = str(ed.get("signing_backend", "openssl")) components = sorted({ component for entry in entries - if (component := ((entry.leaf.get("attestation") or {}).get("subject") or {}).get("component")) + if _leaf_ok(entry) + and (component := ((entry.leaf.get("attestation") or {}).get("subject") or {}).get("component")) }) - provenance = ((latest.get("signatures") or {}).get("ed25519") or {}).get("signing_provenance") or {} + mirror = "https://github.com/saymrwulf/lean-transparency-log" rows = "".join( - f"{escape(component)}" - f"attestation" - f"inclusion proof" - for component in components + f"{escape(c)}" + f"attestation" + f"inclusion proof" + f"16/16 proven" + for c in components ) - return f""" -Lean Transparency Log -

Lean Transparency Log read-only

-

This service publishes signed attestations of formal (Lean 4) proof -verification for cryptographic Rust libraries, bound into an append-only -RFC 9162-style Merkle log. Customers verify a signature and a -≈{max(1, (latest.get('tree_size') or 1).bit_length())}-hash inclusion proof in milliseconds -— the hours of Lean kernel re-checking happened once, on the provider's side, -under memory-capped guards.

+ tree_svg = _svg_tree(entries, str(latest.get("root_hash", "")), signing_backend) -

Current state

+ return f""" + +LTL — Lean Transparency Log + +

zkdefi.org

+

LTL — the Lean Transparency Log

+

One sentence: a public, append-only Merkle +accumulator of signed statements that the Lean 4 formal proofs of specific +cryptographic Rust libraries, at specific git commits, machine-re-check with exactly +their documented assumptions — so that you can trust a proof result by checking +one signature and ~{max(1,(latest.get('tree_size') or 1).bit_length())} hashes in +milliseconds, instead of running a theorem prover for hours.

+ +

The accumulator, live

+{tree_svg} +

+verified attestation (all certificates proven, axiom cones boundary-exact) +historical audit-failure attestation — kept forever; an append-only ledger does not erase its bad day +

+

Every box above is computed from the live log at page render — leaf hashes, +internal nodes, the root, and the signature are the real ones. Before signing this +root, the provider Merkle-verified its own signing library's leaf +(index {provenance.get('signing_library_leaf_index','?')}, +certificates {escape(str(provenance.get('signing_library_certificates_proven','?')))}) +against this very tree — the signature vouches for the code that produced it, and +the tree vouches for the signature's code. Tree size {latest.get('tree_size',0)}, +log id {escape(str(metadata.get('log_id',''))[:16])}….

+ +

What do I download? — the three artifacts, unambiguously

+

To benefit from the accumulator you need exactly three files per +library, plus optionally the whole mirror. Nothing else.

- - - - - + + + + + + + + + + + + +
log id{escape(str(metadata.get('log_id', ''))[:32])}…
tree size{latest.get('tree_size', 0)} leaves
latest root{escape(str(latest.get('root_hash', ''))[:32])}…
root signed by{escape(str(((latest.get('signatures') or {}).get('ed25519') or {}).get('signing_backend', 'n/a')))} - — the merkleized, proof-attested Ed25519 library itself; before signing, the provider - Merkle-verified that library's own leaf (index {provenance.get('signing_library_leaf_index', '?')}, - certificates {escape(str(provenance.get('signing_library_certificates_proven', '?')))}) against this very tree
attested components{len(components)}
#ArtifactWhat it isWhere
1provider.ed25519.pubThe trust anchor. The provider's public key — the only thing you +take on trust, once. Compare the copy here with the copy in the GitHub mirror; they +must be identical.mirror
2<library>.attestation.jsonThe claim. Which repo, which exact git commit, which theorems, +which observed axiom cones, what machine protection — signed by the provider.table above, or mirror entries/
3<library>.receipt.jsonThe proof of inclusion. Binds artifact 2 into the signed tree: +leaf index, sibling hashes, the Signed Tree Head. ~25 lines of stdlib Python verify it.table above, or mirror receipts/
+the full mirror cloneMaximal benefit: become a witness. Every leaf + every signed head +ever issued + verify.py (stdlib-only). python3 verify.py --all +recomputes the entire tree and every historical head — you then hold proof the log +never equivocated within your clone.git clone {mirror}

Attested libraries

-{rows}
componentclaim documentproof of inclusion
-

Each attestation names the exact git commit it covers, every certificate -with its observed axiom cone, and the machine-protection used during replay. The log -also retains earlier leaves that honestly record a failed audit run — an -append-only trust ledger keeps its history.

+{rows}
componentartifact 2artifact 3status
+ +

Three ways to use it

+
+
Quick check (any machine, milliseconds): download +artifacts 1–3, then
+pacta receipt-verify --attestation … --receipt … --log-public-key provider.ed25519.pub +
No Lean, no Rust, no account. Add --sth-store pins.json for split-view defense.
+
Zero-install audit: git clone {mirror} && python3 verify.py --all +
Standard-library Python only. You become a witness of the whole history.
+
Autonomous agent: the pacta +tool adds STH pinning, freshness policy, online refresh from this service, risk scoring +(R0–R5) with policy-gated consequences, and optionally verifies every signature through +the proof-attested Ed25519 code path itself (--require-verified-verifier).
+

API

GET {base}/v1/sth                      latest Signed Tree Head
 GET {base}/v1/sth-history              every head ever signed (witness material)
 GET {base}/v1/sth-consistency?first=N  consistency proof from your pinned size
-GET {base}/v1/proof?component=NAME     inclusion proof for the newest attestation
-GET {base}/v1/attestation?component=NAME
-GET {base}/v1/entries?start=N&end=M
+GET {base}/v1/proof?component=NAME     inclusion proof (artifact 3, freshly issued)
+GET {base}/v1/attestation?component=NAME   the claim (artifact 2)
+GET {base}/v1/entries?start=N&end=M    raw leaves
 GET {base}/v1/metadata                 log identity
 GET {base}/healthz
-

Verify without trusting this site

-

Everything is verifiable offline. Clone the mirror repository (published on GitHub -and on this Forgejo), which contains every leaf, every signed tree head, the provider -public key, and a standalone verify.py (Python standard library only, -≈100 lines). It recomputes the entire tree from the leaves, checks every historical -head against its prefix, verifies the signatures, and checks any inclusion proof:

-
git clone <mirror-url>/lean-transparency-log
-python3 verify.py --all
-

For agents: the pacta tool adds pinning (split-view defense), -freshness policy, and the option to verify signatures through the -proof-attested Ed25519 code path itself -(pacta receipt-verify … --sth-store … --require-verified-verifier).

+

What a verified inclusion means — and what it does not

+
means The provider whose key you hold +attests: the Lean proofs of the named repository at the named git commit re-check with +exactly the documented assumptions — and that statement is irrevocably part of the log +every other customer and witness sees.
+
does not mean A verified binary. The +proofs cover Rust source; clone the attested commit (the git hash is +the content hash) and build it yourself — compiler and build are declared trusted base +until the reproducible-builds program (R5) lands. Every attestation carries its full +residual-risk list. Honesty about the boundary is the product.
-

What a verified inclusion means — and what it does not

-

Means: the provider whose key you hold attests that the Lean proofs -of the named repository at the named commit re-check with exactly the documented -assumptions, and this attestation is irrevocably part of the log everyone sees.

-

Does not mean: a verified binary. The proofs cover Rust source; -you clone the attested commit (the git hash is the content hash) and build it -yourself — compiler and build remain declared trusted base until the R5 -program (reproducible builds) lands. Every attestation carries the full residual-risk -list; honesty about the boundary is the product.

+

Log heads are signed offline; this service is read-only and holds no +key material. Provider tooling, agent tooling, and the full course (12 Jupyter +lectures) live in the pacta repository.

"""