From 6c65a537754e6c39478b559b6e2485a6b98ccf5b Mon Sep 17 00:00:00 2001 From: mrwulf Date: Sun, 16 Aug 2026 21:00:18 +0200 Subject: [PATCH] site rewrite: the trust ladder is the page's spine MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Operator order: coherent, precise, accessible — an undergraduate CS student must understand what the service provides, how to benefit, and what to DO from each trust angle. The page now opens in plain terms (what happened, why this site exists), keeps the precise one-sentence as the second voice, and replaces 'Three ways to use it' with the FIVE-rung trust ladder: (1) witness — hold the history honest, one minute; (2) trust the reports, bind the operator — milliseconds; (3) accept observations, reject judgment — re-derive verdicts from recorded cones against your own card, the rung most people miss; (4) replay the proofs yourself — ~30 min/library; (5) rebuild the whole path — weeks, floor named (kernel/extractors/compiler; no rung 6). Split-view comparison stated as orthogonal to all rungs. The API box is demoted to 'For your tooling — the raw API' at the bottom with its reason for existing stated (machine consumers; pacta builds on it). All content guards keep their exact phrases; suite 154 green. --- provider/src/pacta_provider/webdocs.py | 115 +++++++++++++++++++------ 1 file changed, 89 insertions(+), 26 deletions(-) diff --git a/provider/src/pacta_provider/webdocs.py b/provider/src/pacta_provider/webdocs.py index 1637f56..38c7ec4 100644 --- a/provider/src/pacta_provider/webdocs.py +++ b/provider/src/pacta_provider/webdocs.py @@ -221,13 +221,82 @@ def render_docs(log: TransparencyLog, base_path: str) -> str: · code · cv

LTL — the Lean Transparency Log

-

One sentence: a public, append-only Merkle -accumulator (a hash tree that only ever grows) of signed statements that the Lean 4 formal proofs of specific +

What happened here, in plain terms: we took real cryptographic +code — four production Ed25519 signature libraries and the verification path of +SLH-DSA (FIPS 205), the post-quantum signature standard — and machine-checked +mathematical proofs about it with the Lean 4 +proof assistant. Re-checking those proofs yourself takes a toolchain and about half +an hour of compute per library. This site is the shortcut that does not ask for +blind trust: a public, tamper-evident ledger of signed statements about every proof +check we ran — so you decide how much of our work you re-verify, from a millisecond +signature check to redoing everything.

+ +

The same thing, in one precise sentence: a public, append-only Merkle +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) and ~{max(1,(latest.get('tree_size') or 1).bit_length())} hashes in milliseconds, instead of running a theorem prover for hours.

+

Choose where you stand — the trust ladder

+

Every rung below is a legitimate place to stand. Each states what you still take +on trust, what you do, what it costs, and what you know afterwards. Climb one rung +at a time — the whole service is built so that you can.

+ +
+
“I just want the history held honest.” — anyone, one minute.
+Still trusted: everything — but lying becomes attributable. +
git clone https://github.com/saymrwulf/lean-transparency-log && cd lean-transparency-log && python3 verify.py --all
+Python plus the system openssl binary; fails closed without it. +Afterwards you hold every leaf and every Signed Tree Head (STH) ever issued. If the +operator ever shows anyone a conflicting history, your copy exposes it — you are a +witness. A split view (the operator showing different histories to different +consumers) survives only until two witnesses compare.
+ +
“I trust the operator’s reports; bind him to them.” — milliseconds.
+Still trusted: that the recorded observations are honest. +Download the three artifacts (key, claim, inclusion proof — table below), then: +
pacta receipt-verify --attestation … --receipt … --log-public-key provider.ed25519.pub
+The pacta CLI ships in the +pacta repository +(pip install . from a clone); a one-page Python core (the paper’s +Appendix C) does the same check without it. Add --sth-store pins.json to +remember every head you accept. Afterwards the exact claim — repository, commit, +theorems, assumptions — is cryptographically pinned to the operator’s key inside an +append-only history: he can never rewrite or deny it. What he observed, you +have not yet checked.
+ +
“I accept his observations — not his judgment.” — minutes; the rung most people miss.
+Still trusted: the recorded axiom lists; not the operator’s pass/fail labels. +Compare each attestation’s recorded assumption cones against a requirements card +you write yourself — pacta automates the comparison, and lecture 11 of the +Jupyter course +walks through it. +Afterwards every verdict is your verdict, re-derived from your +own ruler; operator labels can veto but never grant acceptance (details in +“You hold the ruler” below).
+ +
“I don’t trust his observations — I’ll run the proofs myself.” — about 30 minutes per library.
+Still trusted: the published Lean sources and the extraction that produced them; +not the operator’s execution. Clone the attested repository at its pinned +commit and press its check button (verification/check.sh) with a Lean 4 +toolchain: the kernel re-checks every certificate on your machine and the axiom +audit prints the exact assumption cones. +Afterwards the theorem prover accepted on your hardware — +the operator is out of the loop entirely.
+ +
“I trust none of it — I’ll rebuild the whole path.” — weeks.
+Still trusted: Lean’s kernel, the extraction tools, and your compiler — the floor, +which we name rather than hide. Pin the upstream Rust source yourself, extract it to +Lean with Charon/Aeneas (every repository ships its extract.sh, pinned +toolchain versions, and byte-pinned generated models for comparison), re-read the +theorem statements against FIPS 205 / RFC 9162 / the curve equations, and re-prove +or audit each certificate. +Afterwards you have reproduced the estate and no longer need us — +which is the point. There is no rung above this one: even here you trust a kernel, a +compiler, and your silicon. Anyone offering zero trust is selling something.
+
+

The trust anchors — pin these keys (one required, one additive)

{_trust_anchor_html(log, metadata, base, mirror)} @@ -284,30 +353,6 @@ consumers.)

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. 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, 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).
-
- -

API

-
GET {base}/v1/sth                      latest Signed Tree Head
-GET {base}/v1/sth-history              the published head history (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
-

What a verified inclusion means — and what it does not

means The provider whose key you hold attests: the Lean proofs of the named repository at the named git commit re-check with @@ -342,6 +387,24 @@ into this same log. If your ruler is stricter than our supply, your rule our roadmap. (The full walk-through is lecture 11 of the Jupyter course in the pacta repo.)
+

For your tooling — the raw API

+

Humans never need these directly; every link on this page already uses them. They +exist so that your software — a CI job, an autonomous agent, a package +resolver — can consume the log without scraping HTML. The pacta CLI +builds on them: STH pinning, freshness policy, risk scoring (R0–R5, six named +residual-risk classes) with policy-gated consequences, and optionally +--require-verified-verifier, which checks every signature through the +proof-attested Ed25519 code path itself.

+
GET {base}/v1/sth                      latest Signed Tree Head
+GET {base}/v1/sth-history              the published head history (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
+ +

The paper

Accountable Distribution of Machine-Checked Correctness Evidence: A Transparency Model and the Lean Transparency Log