diff --git a/paper/check-paper.sh b/paper/check-paper.sh index 755fd94..4624af8 100755 --- a/paper/check-paper.sh +++ b/paper/check-paper.sh @@ -69,6 +69,14 @@ VERSION=$(grep -oP '\\date\{[^}]*---\s*\Kv[0-9.]+' ltl.tex || true) pdftotext -f 1 -l 1 ltl.pdf - | grep -q "$VERSION" || fail "title page does not carry $VERSION" ! pdftotext ltl.pdf - | grep -q '??' || fail "unresolved ?? reference in PDF" +# --- 5b. site claim binding: the webdocs paper card's page count --------- +WEBDOCS=../provider/src/pacta_provider/webdocs.py +if [[ -f "$WEBDOCS" ]]; then + STATED=$(grep -oP '\(PDF, \K[0-9]+(?= pages)' "$WEBDOCS" || true) + [[ -n "$STATED" ]] || fail "webdocs paper card lost its '(PDF, N pages' claim" + [[ "$STATED" -eq "$NPAGES" ]] || fail "webdocs says $STATED pages, PDF has $NPAGES" +fi + # --- 6. render for the mandatory eye pass -------------------------------- rm -rf "$PAGES_DIR"; mkdir -p "$PAGES_DIR" pdftoppm -png -r 110 ltl.pdf "$PAGES_DIR/p" diff --git a/paper/ltl.pdf b/paper/ltl.pdf index 1935968..6921d7d 100644 Binary files a/paper/ltl.pdf and b/paper/ltl.pdf differ diff --git a/provider/src/pacta_provider/webdocs.py b/provider/src/pacta_provider/webdocs.py index 394028e..f7a6080 100644 --- a/provider/src/pacta_provider/webdocs.py +++ b/provider/src/pacta_provider/webdocs.py @@ -138,16 +138,16 @@ proof subject of leaf 18.

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 +authenticates that these statements were made by the operator (the same party the artifacts call “the provider”). It does not, by itself, make 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 +extraction and toolchain assumptions stated in that leaf (one signed entry of the tree below). Every tree head and attestation is signature-checked against this key. -Pin it, and compare this copy byte-for-byte with the independently hosted -mirror copy; they must be identical.

+Pin it (save your own copy; from then on trust only what checks against that copy), and compare this copy byte-for-byte with the independently hosted +mirror copy; they must be identical. The first fetch is trust-on-first-use; the two-host byte-comparison is what bounds it.

{pem}

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

+ ·  curl -s https://ltl.zkdefi.org/log-public-key

{slh_block}
""" @@ -197,11 +197,10 @@ def render_docs(log: TransparencyLog, base_path: str) -> str: · cv

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 +accumulator (a hash tree that only ever grows) of signed statements that the Lean 4 formal proofs of specific +cryptographic Rust libraries, at specific git commits, re-check by machine with exactly their documented assumptions — so that you can trust a proof result by checking -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 +one required signature (Ed25519) 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

@@ -211,10 +210,10 @@ milliseconds, instead of running a theorem prover for hours.

{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 +historical audit-failure attestation — kept forever; an append-only ledger does not erase its bad day (leaves 0–3: an early audit round that failed; leaves 4–7 re-attest the same four libraries cleanly)

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 +internal nodes, the root, and the signature are the real ones. The code that signs the log is itself an entry in the log — and checks its own entry before signing. In detail: 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','?')))}) @@ -237,12 +236,12 @@ identical. this site · 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/ +which observed axiom cones (the exact set of assumptions each proof ultimately rests on), what machine protection — signed by the provider. +table below, 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 Python verify it (stdlib hashing; signature checks shell out to the openssl binary). -table above, or mirror receipts/ +leaf index, sibling hashes, the Signed Tree Head (STH). A one-page Python core verifies it — printed as Appendix C of the paper; the shipped verify.py wraps that core with full fail-closed binding checks (stdlib hashing; signature checks shell out to the openssl binary). +table below, or mirror receipts/ +the full mirror clone Maximal benefit: become a witness. Every leaf + every signed head ever issued + verify.py (Python stdlib + the openssl binary for @@ -257,17 +256,19 @@ consumers.)

Attested libraries

{rows}
componentartifact 2artifact 3status
+

One certificate = one machine-checked theorem together with its exact assumption set (its axiom cone).

+

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.
+
No Lean, no Rust, no account. The pacta CLI ships in the pacta repository (pip install . from a clone). Add --sth-store pins.json to remember every Signed Tree Head (STH) you accept — your defense against a split view (the operator showing different histories to different consumers).
+
Zero-install audit: git clone {mirror} && cd lean-transparency-log && python3 verify.py --all +
Standard-library Python plus the system openssl binary (signature checks fail closed without it). 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 +(R0–R5, six named residual-risk classes) with policy-gated consequences, and optionally verifies every signature through the proof-attested Ed25519 code path itself (--require-verified-verifier).
@@ -290,19 +291,19 @@ view.
does not mean A verified binary. The proofs cover Rust source; clone the attested commit (the commit id identifies the committed git tree — not external dependencies, toolchain downloads, or generated artifacts) 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.
+build it yourself — compiler and build are declared trusted base (assumed, not proven) +until the reproducible-builds program lands and retires risk class R5. Every attestation carries its full +residual-risk list — the enumerated assumptions inside its attestation.json. Honesty about the boundary is the product.

You hold the ruler

The list of assumptions a certificate is allowed to rest on is not something this site hands you at verification time — it is a requirements card that lives in your tooling, on your disk, and that you can read in five minutes or rewrite from first -principles: Lean's three foundational axioms, plus — for the signature tiers only — +principles: Lean's three foundational axioms, plus — for the signature tiers only (the top proof layers, where full signature verification is proven) — named placeholders for SHA-512 and the wire format. Your tooling ignores this operator's pass/fail labels entirely and re-derives every verdict by comparing the -attestation's observed axiom list against your card, name by name. +attestation's observed axiom list (its cone) against your card, name by name. The operator is trusted to copy down what the proof kernel printed — never to interpret it.
A card you write yourself will match this log's supply @@ -312,13 +313,13 @@ shrunk until every remaining axiom justifies its existence. If your card is negotiate — the gap is itemized, never blurred, and you have three honest options: accept a named line item, walk away, or prove the missing piece and enter it into this same log. If your ruler is stricter than our supply, your ruler is -our roadmap. (The full walk-through is lecture 11 in the -course.)
+our roadmap. (The full walk-through is lecture 11 of the Jupyter course in the +pacta repo.)

The paper

Accountable Distribution of Machine-Checked Correctness Evidence: A Transparency Model and the Lean Transparency Log -(PDF, 23 pages, v0.11 — revised August 2026; the version is printed on the +(PDF, 25 pages, v0.11 — revised August 2026; the version is printed on the title page) — 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 @@ -334,14 +335,12 @@ instantiation section for the SLH-DSA (FIPS 205) verify path — eleven cer five uninterpreted hash oracles, exact cones — and a certificate appendix mirroring the Ed25519 tiers.
-
The paper's snapshot vs. today's log. The paper analyses -the log's 16 July 2026 snapshot — thirteen leaves, still leaves 0–12 today, -byte-identical, its pinned head still head #5 of sth-history.jsonl. Everything -since is additive: the four Ed25519 corpora re-attested at 44 certificates each -(leaves 13–16), the accumulator's hardened model (leaf 17), the first post-quantum -subject (leaf 18), and dual-signed heads from tree 14 on. -python3 verify.py --all re-verifies the paper-era prefix together with everything -after it.
+
Paper and log, one story. Since v0.11 the paper +describes this deployment as it runs — nineteen leaves, dual-signed heads, the +post-quantum verify path as leaf 18 with its own certificate appendix. The log is +append-only and keeps growing past any paper revision; every number the paper states +stays checkable against the retained history: python3 verify.py --all +re-verifies all of it, paper-era and after, from a clone of the mirror.

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

diff --git a/tests/test_web_and_witness.py b/tests/test_web_and_witness.py index 30995e4..27870a5 100644 --- a/tests/test_web_and_witness.py +++ b/tests/test_web_and_witness.py @@ -159,3 +159,25 @@ def test_standalone_verify_py_runs(tmp_path): assert result.returncode == 0, result.stdout + result.stderr # hardened verifier: full mode (signatures verified) must report exactly this assert "RESULT: OK [full]" in result.stdout + + +def test_webdocs_source_carries_no_stale_paper_claims(): + # Regression for the 2026-08-16 operator finding: the paper card said + # "23 pages" and the July-snapshot card survived a silently failed + # replace (an invisible NBSP defeated the pattern). Guard the shipped + # STRINGS, not just version markers. + from pathlib import Path + + source = Path(__file__).resolve().parents[1] / "provider" / "src" / "pacta_provider" / "webdocs.py" + text = source.read_text(encoding="utf-8") + for stale in ("snapshot", "thirteen leaves", "16 July", "16 July", + "16\xa0July", "v0.9", "v0.10", "23 pages"): + assert stale not in text, f"stale marker {stale!r} in webdocs" + # printed commands must work as printed: curl needs the scheme + # (http->https redirect yields empty output), the clone one-liner + # needs the cd into the cloned directory + assert "curl -s ltl.zkdefi.org" not in text + assert "cd lean-transparency-log" in text + # first-use glosses the page promised: STH and axiom cones + assert "Signed Tree Head (STH)" in text + assert "axiom cones (the exact set of assumptions" in text