(log is empty)
" + hashes = [bytes.fromhex(entry.leaf_hash) for entry in entries] + levels: list[list[bytes]] = [hashes] + while len(levels[-1]) > 1: + level = levels[-1] + nxt = [node_hash(level[i], level[i + 1]) for i in range(0, len(level) - 1, 2)] + if len(level) % 2: + nxt.append(level[-1]) + levels.append(nxt) + width, level_gap = 1000, 86 + height = 150 + level_gap * len(levels) + out = [f'") + return "".join(out) + + def render_docs(log: TransparencyLog, base_path: str) -> str: base = "/" + base_path.strip("/") metadata = log.metadata() history = log.sth_history() - latest = history[-1] if history else {} + latest: dict[str, Any] = history[-1] if history else {} entries = log.entries() + 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 (component := ((entry.leaf.get("attestation") or {}).get("subject") or {}).get("component")) + if _leaf_ok(entry) + and (component := ((entry.leaf.get("attestation") or {}).get("subject") or {}).get("component")) }) - provenance = ((latest.get("signatures") or {}).get("ed25519") or {}).get("signing_provenance") or {} + mirror = "https://github.com/saymrwulf/lean-transparency-log" rows = "".join( - f"{escape(component)}{escape(c)}This service publishes signed attestations of formal (Lean 4) proof -verification for cryptographic Rust libraries, bound into an append-only -RFC 9162-style Merkle log. Customers verify a signature and a -≈{max(1, (latest.get('tree_size') or 1).bit_length())}-hash inclusion proof in milliseconds -— the hours of Lean kernel re-checking happened once, on the provider's side, -under memory-capped guards.
+ tree_svg = _svg_tree(entries, str(latest.get("root_hash", "")), signing_backend) -zkdefi.org
+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 +their documented assumptions — so that you can trust a proof result by checking +one signature and ~{max(1,(latest.get('tree_size') or 1).bit_length())} hashes in +milliseconds, instead of running a theorem prover for hours.
+ ++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 +
+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
+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)},
+log id {escape(str(metadata.get('log_id',''))[:16])}….
To benefit from the accumulator you need exactly three files per +library, plus optionally the whole mirror. Nothing else.
| log id | {escape(str(metadata.get('log_id', ''))[:32])}… | ||
|---|---|---|---|
| tree size | {latest.get('tree_size', 0)} leaves | ||
| latest root | {escape(str(latest.get('root_hash', ''))[:32])}… | ||
| root signed by | {escape(str(((latest.get('signatures') or {}).get('ed25519') or {}).get('signing_backend', 'n/a')))}
- — the merkleized, proof-attested Ed25519 library itself; before signing, the provider
- Merkle-verified that library's own leaf (index {provenance.get('signing_library_leaf_index', '?')},
- certificates {escape(str(provenance.get('signing_library_certificates_proven', '?')))}) against this very tree | ||
| attested components | {len(components)} | ||
| # | Artifact | What it is | Where |
| 1 | provider.ed25519.pub |
+The trust anchor. 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 +must be identical. | +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/ |
| 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 stdlib Python verify it. | +table above, or mirror receipts/ |
| + | 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} |
| component | claim document | proof of inclusion |
|---|
Each attestation names the exact git commit it covers, every certificate -with its observed axiom cone, and the machine-protection used during replay. The log -also retains earlier leaves that honestly record a failed audit run — an -append-only trust ledger keeps its history.
+| component | artifact 2 | artifact 3 | status |
|---|
pacta receipt-verify --attestation … --receipt … --log-public-key provider.ed25519.pub
+--sth-store pins.json for split-view defense.git clone {mirror} && python3 verify.py --all
+--require-verified-verifier).GET {base}/v1/sth latest Signed Tree Head
GET {base}/v1/sth-history every head ever signed (witness material)
GET {base}/v1/sth-consistency?first=N consistency proof from your pinned size
-GET {base}/v1/proof?component=NAME inclusion proof for the newest attestation
-GET {base}/v1/attestation?component=NAME
-GET {base}/v1/entries?start=N&end=M
+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
-Everything is verifiable offline. Clone the mirror repository (published on GitHub
-and on this Forgejo), which contains every leaf, every signed tree head, the provider
-public key, and a standalone verify.py (Python standard library only,
-≈100 lines). It recomputes the entire tree from the leaves, checks every historical
-head against its prefix, verifies the signatures, and checks any inclusion proof:
git clone <mirror-url>/lean-transparency-log -python3 verify.py --all-
For agents: the pacta tool adds pinning (split-view defense),
-freshness policy, and the option to verify signatures through the
-proof-attested Ed25519 code path itself
-(pacta receipt-verify … --sth-store … --require-verified-verifier).
Means: the provider whose key you hold attests that the Lean proofs -of the named repository at the named commit re-check with exactly the documented -assumptions, and this attestation is irrevocably part of the log everyone sees.
-Does not mean: a verified binary. The proofs cover Rust source; -you clone the attested commit (the git hash is the content hash) and build it -yourself — compiler and build remain declared trusted base until the R5 -program (reproducible builds) lands. Every attestation carries the full residual-risk -list; honesty about the boundary is the product.
+Log heads are signed offline; this service is read-only and holds no +key material. Provider tooling, agent tooling, and the full course (12 Jupyter +lectures) live in the pacta repository.
"""