diff --git a/provider/src/pacta_provider/webdocs.py b/provider/src/pacta_provider/webdocs.py index 1a18135..66e97e5 100644 --- a/provider/src/pacta_provider/webdocs.py +++ b/provider/src/pacta_provider/webdocs.py @@ -115,8 +115,11 @@ def _trust_anchor_html(log: TransparencyLog, metadata: dict[str, Any], base: str ) pem = escape(key_path.read_text(encoding="utf-8").strip()) return f"""
-

This key is the only thing you take on trust, once. -Everything else on this page - every attestation, every tree head - is verified against it. +

This key is the sole cryptographic identity anchor: it +authenticates that these statements were made by the operator. 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 +signature-checked against this key. Pin it, and compare this copy byte-for-byte with the independently hosted mirror copy; they must be identical.

{pem}
@@ -135,18 +138,27 @@ 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")) - components = sorted({ - component - for entry in entries - if _leaf_ok(entry) - and (component := ((entry.leaf.get("attestation") or {}).get("subject") or {}).get("component")) - }) + # newest entry per component, with its real proven/total from the leaf + newest: dict[str, Any] = {} + for entry in entries: + if not _leaf_ok(entry): + continue + 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"{escape(c)}" f"attestation" f"inclusion proof" - f"16/16 proven" + f"{escape(_counts(newest[c]))}" for c in components ) tree_svg = _svg_tree(entries, str(latest.get("root_hash", "")), signing_backend) @@ -181,8 +193,10 @@ 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 — the signature vouches for the code that produced it, and -the tree vouches for the signature's code. Tree size {latest.get('tree_size',0)}, +against this very tree — so the signed tree contains an attestation of the source the +operator reports its signing binary was built from. (An Ed25519 signature cannot by itself prove +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 {escape(str(metadata.get('log_id',''))[:16])}….

What do I download? — the three artifacts, unambiguously

@@ -191,9 +205,10 @@ library, plus optionally the whole mirror. Nothing else.

- + +recomputes the entire tree and every historical head — you then hold a retained view that can +later EXPOSE a conflicting head shown to someone else. (A single clone cannot by itself prove the +log never split its view toward another consumer; that requires comparing heads across +consumers.)
#ArtifactWhat it isWhere
1provider.ed25519.pubThe trust anchor. The provider's public key — the only thing you -take on trust, once. Fetch it from BOTH independent locations and compare; the copies -must be identical.The identity anchor. The provider's public key — the sole cryptographic +identity you pin. It authenticates the operator's statements; their truth rests on each leaf's +stated assumptions. Fetch it from BOTH independent locations and compare; the copies must be +identical. this site · mirror
2<library>.attestation.json The claim. Which repo, which exact git commit, which theorems, @@ -206,8 +221,10 @@ leaf index, sibling hashes, the Signed Tree Head. ~25 lines of stdlib Python ver
+the full mirror clone Maximal benefit: become a witness. Every leaf + every signed head ever issued + verify.py (stdlib-only). python3 verify.py --all -recomputes the entire tree and every historical head — you then hold proof the log -never equivocated within your clone. git clone {mirror}
@@ -241,11 +258,13 @@ 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 -exactly the documented assumptions — and that statement is irrevocably part of the log -every other customer and witness sees.
+exactly the documented assumptions — and this signed head irrevocably commits that statement to +this view. Consumers who compare heads, or retain the public mirror, can expose any conflicting +view.
does not mean A verified binary. The -proofs cover Rust source; clone the attested commit (the git hash is -the content hash) and build it yourself — compiler and build are declared trusted base +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.
@@ -276,7 +295,7 @@ Kernel-Checked Correctness Evidence for Deployed Ed25519 ImplementationsPrevious version: v0.1 (4 pages).