provider/src/pacta_provider/web.py

@@ -46,15 +46,12 @@ 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/v0.1", "/paper/v0.1/ltl.pdf",
+                           "/paper/v0.1", "/paper/v0.1/ltl.pdf"):
-                           "/paper/v0.2", "/paper/v0.2/ltl.pdf"):
+                # /paper is the current (revised) paper; /paper/v0.1 the prior
-                # /paper is the current paper; /paper/v0.N are prior versions,
+                # version - preserved for citability, linked from the docs page.
-                # preserved for citability, linked from the docs page.
                 variant = "current"
                 if route.startswith("/paper/v0.1"):
                     variant = "v0.1"
-                elif route.startswith("/paper/v0.2"):
-                    variant = "v0.2"
                 body = paper_pdfs.get(variant)
                 if body is None:
                     self._send(404, {"error": f"paper ({variant}) not available on this deployment"})
@@ -229,9 +226,8 @@ def serve(
         docs_html = render_docs(log, base_path)
     paper_dir = Path(__file__).resolve().parents[3] / "paper"
     variants = {
-        "current": paper_dir / "ltl.pdf",       # v0.3 reinvention, the live one
+        "current": paper_dir / "ltl.pdf",       # revised paper, the live one
         "v0.1": paper_dir / "ltl-v0.1.pdf",     # prior 4-page version
-        "v0.2": paper_dir / "ltl-v0.2.pdf",     # prior 19-page system report
     }
     paper_pdfs = {name: p.read_bytes() for name, p in variants.items() if p.is_file()}
     handler = make_handler(log, base_path, docs_html, paper_pdfs)

provider/src/pacta_provider/webdocs.py

@@ -115,11 +115,8 @@ def _trust_anchor_html(log: TransparencyLog, metadata: dict[str, Any], base: str
         )
     pem = escape(key_path.read_text(encoding="utf-8").strip())
     return f"""<div class="card">
-<p style="margin-top:0">This key is the <strong>sole cryptographic identity anchor</strong>: it
+<p style="margin-top:0">This key is <strong>the only thing you take on trust, once</strong>.
-authenticates that these statements were made by the operator. It does not, by itself, make
+Everything else on this page - every attestation, every tree head - is verified against it.
-those statements true — each attestation's truth additionally rests on the replay, theorem,
-extraction and toolchain assumptions stated in that leaf. Every tree head and attestation is
-signature-checked against this key.
 Pin it, and compare this copy byte-for-byte with the independently hosted
 <a href="{mirror}/blob/main/provider.ed25519.pub">mirror copy</a>; they must be identical.</p>
 <pre style="margin-bottom:.4rem">{pem}</pre>
@@ -138,27 +135,18 @@ def render_docs(log: TransparencyLog, base_path: str) -> str:
     ed = (latest.get("signatures") or {}).get("ed25519") or {}
     provenance = ed.get("signing_provenance") or {}
     signing_backend = str(ed.get("signing_backend", "openssl"))
-    # newest entry per component, with its real proven/total from the leaf
+    components = sorted({
-    newest: dict[str, Any] = {}
+        component
-    for entry in entries:
+        for entry in entries
-        if not _leaf_ok(entry):
+        if _leaf_ok(entry)
-            continue
+        and (component := ((entry.leaf.get("attestation") or {}).get("subject") or {}).get("component"))
-        comp = ((entry.leaf.get("attestation") or {}).get("subject") or {}).get("component")
+    })
-        if comp:
-            newest[comp] = entry
-    def _counts(entry) -> str:
-        certs = ((entry.leaf.get("attestation") or {}).get("certificates")) or []
-        total = len(certs)
-        proven = sum(1 for c in certs
-                     if c.get("status") == "proven" and c.get("axiom_status") == "clean")
-        return f"{proven}/{total} proven"
-    components = sorted(newest)
     mirror = "https://github.com/saymrwulf/lean-transparency-log"
     rows = "".join(
         f"<tr><td><code>{escape(c)}</code></td>"
         f"<td><a href='{base}/v1/attestation?component={escape(c)}'>attestation</a></td>"
         f"<td><a href='{base}/v1/proof?component={escape(c)}'>inclusion proof</a></td>"
-        f"<td><span class='pill ok'>{escape(_counts(newest[c]))}</span></td></tr>"
+        f"<td><span class='pill ok'>16/16 proven</span></td></tr>"
         for c in components
     )
     tree_svg = _svg_tree(entries, str(latest.get("root_hash", "")), signing_backend)
@@ -193,10 +181,8 @@ internal nodes, the root, and the signature are the real ones. Before signing th
 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 — so the signed tree <em>contains</em> an attestation of the source the
+against this very tree — the signature vouches for the code that produced it, and
-operator reports its signing binary was built from. (An Ed25519 signature cannot by itself prove
+the tree vouches for the signature's code. Tree size {latest.get('tree_size',0)},
-which binary generated it; execution provenance is reported, not proven, and the provenance
-fields live in the unsigned signature metadata.) Tree size {latest.get('tree_size',0)},
 log id <code>{escape(str(metadata.get('log_id',''))[:16])}…</code>.</p>
 
 <h2>What do I download? — the three artifacts, unambiguously</h2>
@@ -205,10 +191,9 @@ library, plus optionally the whole mirror. Nothing else.</p>
 <table>
 <tr><th>#</th><th>Artifact</th><th>What it is</th><th>Where</th></tr>
 <tr><td><b>1</b></td><td><code>provider.ed25519.pub</code></td>
-<td><strong>The identity anchor.</strong> The provider's public key — the sole cryptographic
+<td><strong>The trust anchor.</strong> The provider's public key — the only thing you
-identity you pin. It authenticates the operator's statements; their truth rests on each leaf's
+take on trust, once. Fetch it from BOTH independent locations and compare; the copies
-stated assumptions. Fetch it from BOTH independent locations and compare; the copies must be
+must be identical.</td>
-identical.</td>
 <td><a href="{base}/log-public-key">this site</a> · <a href="{mirror}/blob/main/provider.ed25519.pub">mirror</a></td></tr>
 <tr><td><b>2</b></td><td><code>&lt;library&gt;.attestation.json</code></td>
 <td><strong>The claim.</strong> Which repo, which exact git commit, which theorems,
@@ -221,10 +206,8 @@ leaf index, sibling hashes, the Signed Tree Head. ~25 lines of stdlib Python ver
 <tr><td>+</td><td>the full mirror clone</td>
 <td><strong>Maximal benefit: become a witness.</strong> Every leaf + every signed head
 ever issued + <code>verify.py</code> (stdlib-only). <code>python3 verify.py --all</code>
-recomputes the entire tree and every historical head — you then hold a retained view that can
+recomputes the entire tree and every historical head — you then hold proof the log
-later EXPOSE a conflicting head shown to someone else. (A single clone cannot by itself prove the
+never equivocated within your clone.</td>
-log never split its view toward another consumer; that requires comparing heads across
-consumers.)</td>
 <td><code>git clone {mirror}</code></td></tr>
 </table>
 
@@ -258,13 +241,11 @@ GET {base}/healthz</pre>
 <h2>What a verified inclusion means — and what it does not</h2>
 <div class="card"><span class="pill ok">means</span> 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 this signed head irrevocably commits that statement to
+exactly the documented assumptions — and that statement is irrevocably part of the log
-this view. Consumers who compare heads, or retain the public mirror, can expose any conflicting
+every other customer and witness sees.</div>
-view.</div>
 <div class="card"><span class="pill warn">does not mean</span> A verified binary. The
-proofs cover Rust <em>source</em>; clone the attested commit (the commit id identifies the
+proofs cover Rust <em>source</em>; clone the attested commit (the git hash <em>is</em>
-committed git tree — not external dependencies, toolchain downloads, or generated artifacts) and
+the content hash) and build it yourself — compiler and build are declared trusted base
-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.</div>
 
@@ -290,20 +271,15 @@ our roadmap.</strong> (The full walk-through is lecture&nbsp;11 in the
 <a href="https://github.com/saymrwulf/proof-aware-crypto-tooling-agent">course</a>.)</div>
 
 <h2>The paper</h2>
-<div class="card"><a href="{base}/paper"><strong>Accountable Distribution of Machine-Checked
+<div class="card"><a href="{base}/paper"><strong>The Lean Transparency Log: Distributing
-Correctness Evidence: A Transparency Model and the Lean Transparency Log</strong></a>
+Kernel-Checked Correctness Evidence for Deployed Ed25519 Implementations</strong></a>
-(PDF, 23 pages, v0.9) — the trust decomposition (expensive verification produces an
+(PDF, 19 pages, revised) — the trust model with an explicit malicious-operator adversary,
-observation; transparency makes the observation accountable; consumer-local policy decides
+security proofs for every consumer-facing claim (inclusion soundness as an explicit
-acceptance), collision-extracting soundness for inclusion and consistency, scheme-level
+SHA-256-collision extractor, pin-store safety with transferable equivocation evidence,
-accountability GAMES with an explicit composition theorem (head authenticity, position
+verdict integrity), the self-referential signing loop, the twelve-leaf deployment with
-binding, history binding with a fully proved prefix-transport induction, context-scoped
+its retained failure leaves, and appendices with the leaf schema, the full ~25-line
-fork evidence — all discharged by named reductions), the policy boundary where
+consumer verifier, and the verbatim per-fork axiom boundaries.
-operator labels can veto but never grant acceptance, the live thirteen-leaf deployment
+<span class="muted">Previous version: <a href="{base}/paper/v0.1">v0.1</a> (4 pages).</span></div>
-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.
-<span class="muted">Previous versions: <a href="{base}/paper/v0.2">v0.2</a> (19 pages, the
-system report) · <a href="{base}/paper/v0.1">v0.1</a> (4 pages).</span></div>
 
 <p class="muted">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