diff --git a/provider/src/pacta_provider/webdocs.py b/provider/src/pacta_provider/webdocs.py index 6884285..18a7030 100644 --- a/provider/src/pacta_provider/webdocs.py +++ b/provider/src/pacta_provider/webdocs.py @@ -50,7 +50,7 @@ def _leaf_ok(entry: LogEntry) -> bool: ) -def _svg_tree(entries: list[LogEntry], root_hex: str, signing_backend: str) -> str: +def _svg_tree(entries: list[LogEntry], root_hex: str, signing_backend: str, head_label: str = "Ed25519") -> str: """The accumulator, drawn from its real leaves.""" if not entries: return "

(log is empty)

" @@ -94,7 +94,7 @@ def _svg_tree(entries: list[LogEntry], root_hex: str, signing_backend: str) -> s 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 Tree Head — {escape(head_label)}({root_hex[:12]}…)') out.append(f'signed by: {escape(signing_backend)} (the proof-attested library itself)') out.append(f'') out.append("") @@ -114,6 +114,28 @@ def _trust_anchor_html(log: TransparencyLog, metadata: dict[str, Any], base: str f'mirror instead.' ) pem = escape(key_path.read_text(encoding="utf-8").strip()) + # The SLH-DSA verification key (additive post-quantum head signature, + # 2026-08) is published THE SAME WAY: full PEM on the page, raw endpoint, + # mirror comparison. Heads before tree 14 carry no SLH-DSA signature and + # verify.py reports them ABSENT — allowed; an append-only log keeps its + # history. + slh_path = log.log_dir / "provider.slhdsa.pub" + if slh_path.is_file(): + import hashlib as _h + slh_pem = escape(slh_path.read_text(encoding="utf-8").strip()) + slh_fp = _h.sha256(slh_path.read_bytes()).hexdigest() + slh_block = f"""
+

Second, additive anchor — post-quantum. Heads from +tree 14 on additionally carry a deterministic SLH-DSA-SHA2-128s (FIPS 205) +signature over the same payload. The Ed25519 signature above remains the one every consumer must +check; this one is checked where tooling allows (OpenSSL ≥ 3.5). Its verify path is the +proof subject of leaf 18.

+
{slh_pem}
+

SHA-256 fingerprint {slh_fp} + ·  raw: {base or ''}/log-slhdsa-public-key + ·  mirror: provider.slhdsa.pub

""" + else: + slh_block = "" return f"""

This key is the sole cryptographic identity anchor: it authenticates that these statements were made by the operator. It does not, by itself, make @@ -126,7 +148,7 @@ Pin it, and compare this copy byte-for-byte with the independently hosted

SHA-256 fingerprint {escape(fingerprint)}  ·  raw: {base or ''}/log-public-key  ·  curl -s ltl.zkdefi.org/log-public-key

-
""" +{slh_block}""" def render_docs(log: TransparencyLog, base_path: str) -> str: @@ -161,7 +183,9 @@ def render_docs(log: TransparencyLog, base_path: str) -> str: f"{escape(_counts(newest[c]))}" for c in components ) - tree_svg = _svg_tree(entries, str(latest.get("root_hash", "")), signing_backend) + slh_signed = ((latest.get("signatures") or {}).get("slh_dsa") or {}).get("status") == "signed" + head_label = "Ed25519 + SLH-DSA" if slh_signed else "Ed25519" + tree_svg = _svg_tree(entries, str(latest.get("root_hash", "")), signing_backend, head_label) return f""" @@ -176,7 +200,8 @@ def render_docs(log: TransparencyLog, base_path: str) -> str: 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 +one required signature (Ed25519; heads from tree 14 add an additive post-quantum +SLH-DSA signature) and ~{max(1,(latest.get('tree_size') or 1).bit_length())} hashes in milliseconds, instead of running a theorem prover for hours.

The trust anchor — pin this key

@@ -216,11 +241,12 @@ 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. +leaf index, sibling hashes, the Signed Tree Head. ~25 lines of Python verify it (stdlib hashing; signature checks shell out to the openssl binary). 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 +ever issued + verify.py (Python stdlib + the openssl binary for +signatures; fails closed without them). python3 verify.py --all recomputes the entire tree and every historical head — you then hold a retained view that can later EXPOSE a conflicting head shown to someone else. (A single clone cannot by itself prove the log never split its view toward another consumer; that requires comparing heads across @@ -292,19 +318,39 @@ our roadmap. (The full walk-through is lecture 11 in the

The paper

Accountable Distribution of Machine-Checked Correctness Evidence: A Transparency Model and the Lean Transparency Log -(PDF, 23 pages, v0.9) — the trust decomposition (expensive verification produces an +(PDF, 23 pages, v0.9 — frozen while under journal review; it describes the +log as of its 16 July 2026 snapshot) — 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, the live thirteen-leaf deployment +operator labels can veto but never grant acceptance, the then-thirteen-leaf deployment whose entry 13 attests the accumulator's own mechanized model, and the measured model/deployment divergence (3,867 lied-size cases, every one accepted only by the deployed verifier) reported as a result rather than hidden. Previous versions: v0.2 (19 pages, the system report) · v0.1 (4 pages).
+
Reading the paper against today's log. The paper is frozen +under review; the log is append-only and has kept moving. Nothing the paper describes was +altered, so every number in it remains checkable against the live history: the thirteen leaves +it analyses are still leaves 0–12, byte-identical, and the head it pins (tree 13, root +3488a2d0…) is still head #5 of sth-history.jsonl — +python3 verify.py --all re-verifies the paper-era prefix together with everything +after it. What has moved since the snapshot is additive: leaves 13–16 re-attest the four +Ed25519 libraries at 44 certificates each (the paper's sixteen-certificate corpora describe the +leaf 8–11 generation, which those leaves still record); leaf 17 re-attests the +accumulator's mechanized model at its hardened state; and leaf 18 is the log's first +post-quantum subject, the SLH-DSA-SHA2-128s verify path. Heads from tree 14 on carry an +additive SLH-DSA signature beside the Ed25519 signature the paper describes; earlier heads have +none, by design, and the verifier reports them as ABSENT rather than failing them. +One result has changed in the good direction: the 3,867-case model/deployment divergence the +paper honestly reports was closed on 23 July 2026 (the sn==0 fix); the +current pinned divergence count is 0, and both the divergence and its fix are part of the +retained record. Where the paper and the live log disagree on a number, the paper is describing +its snapshot — and the log's history contains that snapshot, unchanged, inside it.
+

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.