"""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 pacta.transparency import node_hash from .transparency_log import LogEntry, TransparencyLog _STYLE = """ :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;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'") return "".join(out) def render_docs(log: TransparencyLog, base_path: str) -> str: base = "/" + base_path.strip("/") if base_path.strip("/") else "" metadata = log.metadata() history = log.sth_history() 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 _leaf_ok(entry) and (component := ((entry.leaf.get("attestation") or {}).get("subject") or {}).get("component")) }) mirror = "https://github.com/saymrwulf/lean-transparency-log" rows = "".join( f"{escape(c)}zkdefi.org
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.
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])}….
To benefit from the accumulator you need exactly three files per library, plus optionally the whole mirror. Nothing else.
| # | Artifact | What it is | Where |
|---|---|---|---|
| 1 | provider.ed25519.pub |
The 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.json |
The 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.json |
The 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 clone | Maximal 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} |
| component | artifact 2 | artifact 3 | status |
|---|
pacta receipt-verify --attestation … --receipt … --log-public-key provider.ed25519.pub
--sth-store pins.json for split-view defense.git clone {mirror} && python3 verify.py --all
--require-verified-verifier).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 (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
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.
"""