paper rigor pass: fix three claims that failed verification; serve the trust anchor

Socratic audit findings, all verified against artifacts:
- 'zero lines between structurally identical forks' was FALSE: risc0 vs
  betrusted differ by 27 lines (all annotation, documenting the risc0
  fork's black_box trusted-base entry). Corrected to the true number.
- '~64 Lean files per fork' over-rounded anza's 58. Now '58-64'.
- completeness parenthetical now states both hypotheses (a=-1 square, d
  non-square), not just d.
- 'key published in two independent locations' was ASPIRATIONAL: the
  site served only a fingerprint. New /log-public-key endpoint serves
  the key bytes; docs-page artifact-1 row links both copies; test added.
Verified exactly and kept: 215-line parser diff (FromBytesSpec), 121-line
signature-glue diff (SigApexSpec), byte-identical x4 math files incl. the
carry-telescope file, 11-axiom upstream boundary, 16 certs/leaf, 153-line
mirror verifier, leaf fields (toolchain + machine_protection), all 17 refs.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

paper/ltl.tex

@@ -97,8 +97,9 @@ $E : -x^2+y^2 = 1+d\,x^2y^2$ over $\mathbb{F}_p$,
 \Bigl(\tfrac{x_1y_2+x_2y_1}{1+d\,x_1x_2y_1y_2},\;
 \tfrac{y_1y_2+x_1x_2}{1-d\,x_1x_2y_1y_2}\Bigr),
 \end{equation*}
-including the completeness fact that makes it branch-free ($d$ is a
+including the completeness fact that makes it branch-free ($a=-1$ is a
-non-square, so the denominators never vanish~\cite{bernsteinlange}).
+square and $d$ a non-square in $\mathbb{F}_p$, so the denominators never
+vanish~\cite{bernsteinlange}).
 At the apex, writing $\code{accept}(A,m,R,s)$ for ``the extracted
 verifier returns \code{ok}'', with $k$ the scalar produced by the hash
 oracle $H(R,A,m)$ and no properties assumed of $H$, the byte-level tier
@@ -287,7 +288,7 @@ Operator/consumer tooling and a twelve-lecture course:
 underlying proof corpora are in the \code{saymrwulf/*-ed25519-verified}
 repositories; every claim in this paper is re-checkable from these
 artifacts.} with eight leaves: one attestation per fork from each of two
-full replay runs ($\approx$64 Lean files and $\approx$1{,}800\,s per
+full replay runs (58--64 Lean files and $\approx$1{,}800\,s per
 fork, under hard memory caps and core pinning). In the second run all
 four forks reported 16/16 certificates proven with boundary-exact cones,
 pinned to exact commits. The first run is deliberately still in the log: its audit step
@@ -328,9 +329,11 @@ lemma file) are byte-identical across all four; extraction-facing proof
 scripts diverge sharply where the forks' code or the extractor's naming
 differs (e.g., 215 changed lines for the byte-parser proofs on the two
 forks whose extraction produces a closure-based loader; 121 lines for
-the signature-glue proofs on the same-crate fork; zero lines between
+the signature-glue proofs on the same-crate fork; 27 lines---all
-structurally identical forks). Per-target verification, in other words,
+annotation---between the two structurally closest forks, documenting the
-is doing measurable work exactly where the targets actually differ.
+one fork's \code{black\_box} optimization barrier). Per-target
+verification, in other words, is doing measurable work exactly where the
+targets actually differ.
 
 \section{Related work}
 \label{sec:related}

provider/src/pacta_provider/web.py

@@ -54,6 +54,20 @@ def make_handler(log: TransparencyLog, base_path: str, docs_html: str, paper_pdf
                 self.send_header("Content-Length", str(len(paper_pdf)))
                 self.end_headers()
                 self.wfile.write(paper_pdf)
+            elif route == "/log-public-key":
+                # TOFU mitigation depends on the key being published in two
+                # independent locations; this is the site's copy (the mirror
+                # carries the other). Serving only a fingerprint would not do.
+                key_path = Path(log.log_dir) / "provider.ed25519.pub"
+                if not key_path.is_file():
+                    self._send(404, {"error": "log public key not present in this log directory"})
+                    return
+                body = key_path.read_bytes()
+                self.send_response(200)
+                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)
             elif route == "/healthz":
                 self._send(200, {"ok": True, "tree_size": len(log.entries())})
             elif route == f"/{API_VERSION}/metadata":
@@ -124,6 +138,7 @@ def make_handler(log: TransparencyLog, base_path: str, docs_html: str, paper_pdf
                     "endpoints": [
                         f"{base}/docs",
                         f"{base}/paper",
+                        f"{base}/log-public-key",
                         f"{base}/healthz",
                         f"{base}/{API_VERSION}/metadata",
                         f"{base}/{API_VERSION}/sth",

provider/src/pacta_provider/webdocs.py

@@ -164,9 +164,9 @@ library, plus optionally the whole mirror. Nothing else.</p>
 <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 trust anchor.</strong> 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
+take on trust, once. Fetch it from BOTH independent locations and compare; the copies
 must be identical.</td>
-<td><a href="{mirror}/blob/main/provider.ed25519.pub">mirror</a></td></tr>
+<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,
 which observed axiom cones, what machine protection — signed by the provider.</td>

tests/test_web_and_witness.py

@@ -59,6 +59,12 @@ def test_web_endpoints_and_online_proof_roundtrip(tmp_path):
         with urllib.request.urlopen(base + "/paper", timeout=10) as r:
             assert r.headers["Content-Type"] == "application/pdf"
             assert r.read(5) == b"%PDF-"
+        # the site's copy of the trust anchor (TOFU: two independent locations)
+        import shutil
+
+        shutil.copy2(tmp_path / "k.pub", tmp_path / "log" / "provider.ed25519.pub")
+        with urllib.request.urlopen(base + "/log-public-key", timeout=10) as r:
+            assert r.read() == (tmp_path / "k.pub").read_bytes()
     finally:
         server.shutdown()