From 4b45ece97b28b9f4d80c52424cf24f1d091b228f Mon Sep 17 00:00:00 2001 From: mrwulf Date: Mon, 17 Aug 2026 10:58:56 +0200 Subject: [PATCH] =?UTF-8?q?site:=20the=20term-coherence=20pass=20=E2=80=94?= =?UTF-8?q?=20every=20word=20defined=20before=20use,=20every=20table=20sel?= =?UTF-8?q?f-describing?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Operator-caught: 'certificate' used before any definition, 'requirements card' undefined, and the Attested-libraries table headed 'artifact 2 / artifact 3' — numbers pointing at a DIFFERENT table. Fixed: certificates defined in the Merkle intro (each leaf = one proof run, a batch of certificates: one machine-checked theorem with its assumption list); the requirements card is now 'a short plain-text file listing, by name, the assumptions you accept'; table headers are self-describing (library / claim (attestation) / proof of inclusion (receipt) / certificates proven); redundant gloss under the table dropped (say it once). My own fresh re-read on top: 'head' glossed at first use, keys card says 'entry 18' (leaf comes later, at the Merkle mapping), 'Binds artifact 2' de-numbered, 'become a witness' now plain ('hold the complete history yourself, rung 1'), 'risk class R5' dropped from prose, the legend says 'every assumption list exactly as declared' instead of 'boundary-exact'. --- provider/src/pacta_provider/webdocs.py | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) diff --git a/provider/src/pacta_provider/webdocs.py b/provider/src/pacta_provider/webdocs.py index 7fccc29..2026252 100644 --- a/provider/src/pacta_provider/webdocs.py +++ b/provider/src/pacta_provider/webdocs.py @@ -150,7 +150,7 @@ def _trust_anchor_html(log: TransparencyLog, metadata: dict[str, Any], base: str

Key 2 — SLH-DSA (FIPS 205), post-quantum. Heads from tree size 14 on carry a second signature from this key; older heads legitimately have none — an append-only log keeps its history. Check it where your tooling allows (OpenSSL ≥ 3.5). The kind of code that verifies such signatures is itself -a proof subject of this log (leaf 18).

+a proof subject of this log (entry 18).

{slh_pem}

SHA-256 fingerprint {slh_fp}  ·  raw: {base or ''}/log-slhdsa-public-key @@ -239,7 +239,8 @@ You still trust: the content of every claim. You defeat: silent rewriting.
You need: Python 3 and the openssl command (preinstalled on most Linux and macOS systems). 

git clone https://github.com/saymrwulf/lean-transparency-log && cd lean-transparency-log && python3 verify.py --all
This fetches the log’s public mirror — a git repository holding every entry -and every signed head ever issued — and re-computes every hash and signature in it. A green +and every signed head ever issued (a head is the signed root fingerprint of the tree at a +given size) — and re-computes every hash and signature in it. A green result means the history you now hold is internally consistent and signed. Keep the folder: if the operator ever shows a different history to anyone else, your copy proves it. A log that shows different histories to different people (a “split view”) survives only until @@ -294,7 +295,9 @@ compiler, and your hardware.

The accumulator, live

The log is a Merkle tree: every entry (“leaf”) is hashed, hashes pair up level by level, and a single 32-byte root fingerprints the entire history; the operator signs -that root. Changing any past entry would change the root — that is the tamper evidence. This +that root. Changing any past entry would change the root — that is the tamper evidence. Each leaf +records one proof run: a batch of certificates — one machine-checked theorem +each, together with its exact assumption list. This picture is computed from the live log at page render — the leaf hashes, nodes, root, and signature are the real ones:

{tree_svg} @@ -346,9 +349,8 @@ consumers.)

Attested libraries

-{rows}
componentartifact 2artifact 3status
+{rows}
libraryclaim (attestation)proof of inclusion (receipt)certificates proven
-

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

What a verified inclusion means — and what it does not

means The provider whose key you hold @@ -366,7 +368,8 @@ residual-risk list — the enumerated assumptions inside its attestation.j

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 +requirements card — a short plain-text file listing, by name, the +assumptions you accept — 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 (the top proof layers, where full signature verification is proven) — named placeholders for SHA-512 (the hash function Ed25519 uses internally —