README.md

@@ -2,17 +2,8 @@
 
 This repository is the **git-published face** of a transparency log of
 formal-verification attestations: signed statements that the Lean 4 proofs
-of specific software, at specific git commits, re-check with exactly their
+of specific cryptographic Rust libraries, at specific git commits,
-documented assumptions. Its first twelve leaves attest four cryptographic
+re-check with exactly their documented assumptions.
-Rust libraries (Ed25519 implementations); as of **entry 13 (2026-07-16)**
-the log also attests **its own accumulator machinery** — a kernel-checked
-mechanization of the log's security analysis, so the log carries
-kernel-checked proofs *about the accumulator model* underlying its own
-inclusion and consistency reasoning, as one of its own entries (subject
-[`ltl-accumulator-verified`](https://github.com/saymrwulf/ltl-accumulator-verified);
-scoped to the mechanized model — it does not prove operator honesty,
-signing, or execution provenance). Current head: tree size 13, root
-`3488a2d0…`.
 
 Layout:
 
@@ -24,8 +15,7 @@ Layout:
 | `sth-history.jsonl` | **every** Signed Tree Head ever issued — the witness channel: all cloners see the same heads |
 | `latest-sth.json` | the current head |
 | `provider.ed25519.pub` | the provider's public key (the sole trust anchor) |
-| `verify.py` | standalone verifier (Python stdlib + the `openssl` binary; fails closed without them; `--all` covers every published receipt) |
+| `verify.py` | standalone verifier, Python standard library only |
-| `verify_selftest.py` | adversarial self-test: proves the verifier's fail-closed paths reject mutated receipts |
 
 Verify everything locally, no installation:
 

verify.py

@@ -1,31 +1,18 @@
 #!/usr/bin/env python3
 """Standalone verifier for the published Lean Transparency Log.
 
-Pure Python 3 standard library for hashing and structure; Ed25519
+Python 3 standard library ONLY - no pacta, no pip. Verifies, from the
-signature checking shells out to the `openssl` binary. Verifies, from the
 files in this repository alone:
 
   1. every entry's leaf hash,
   2. every historical Signed Tree Head against the recomputed prefix root
-     (a split view or tampered entry fails here),
+     (this is the witness check: a split view or tampered entry fails here),
-  3. every STH Ed25519 signature,
+  3. every STH Ed25519 signature (via the openssl binary, if available),
-  4. every published receipt under receipts/ (with --all), and any receipt
+  4. any receipt's inclusion proof (--receipt FILE).
-     supplied via --receipt FILE, as a FULL transparency receipt: type tag,
-     STH signature, REQUIRED key fingerprint, log id, presence of its STH
-     in the published history, REQUIRED leaf hash matching the named entry,
-     tree-size agreement, and the inclusion proof. Binding fields are
-     required, never compare-if-present.
-
-FAIL-CLOSED: if signature checking is unavailable (no `openssl`, or the
-public key is missing), the run FAILS — signatures are load-bearing and a
-"couldn't check" is not a pass. Use --structural-only to explicitly ask
-for hashes/structure without signatures (it prints, and exits, as a
-reduced check, never as full verification).
 
 Usage:
   python3 verify.py --all
   python3 verify.py --receipt receipts/dalek-ed25519-verified.receipt.json
-  python3 verify.py --all --structural-only   # explicit reduced check
 """
 import argparse
 import base64
@@ -95,21 +82,11 @@ def load_leaves():
     return leaves, problems
 
 
-def signatures_available() -> bool:
-    return bool(shutil.which("openssl")) and (HERE / "provider.ed25519.pub").exists()
-
-
-def key_fingerprint() -> str:
-    return hashlib.sha256((HERE / "provider.ed25519.pub").read_bytes()).hexdigest()
-
-
 def check_sth_signature(head) -> str:
-    """VALID / INVALID / UNAVAILABLE. UNAVAILABLE is a FAILURE at the
-    caller unless the run is explicitly --structural-only."""
     openssl = shutil.which("openssl")
     key = HERE / "provider.ed25519.pub"
     if not openssl or not key.exists():
-        return "UNAVAILABLE"
+        return "skipped (openssl or provider.ed25519.pub missing)"
     signatures = head.get("signatures") or {}
     ed = signatures.get("ed25519") or {}
     payload = canonical_json({k: v for k, v in head.items() if k != "signatures"})
@@ -126,152 +103,50 @@ def check_sth_signature(head) -> str:
     return "VALID" if result.returncode == 0 else "INVALID"
 
 
-RECEIPT_TYPE = "pacta.transparency.receipt.v1"
-
-
-def verify_receipt(receipt, heads, structural_only: bool, label: str):
-    """Full binding checks for one receipt. Every binding field is REQUIRED;
-    a missing field is a failure, never a skip. Returns failure strings."""
-    problems = []
-    if receipt.get("type") != RECEIPT_TYPE:
-        problems.append(f"{label}: type is {receipt.get('type')!r}, expected {RECEIPT_TYPE!r}")
-    sth = receipt.get("sth") or {}
-    if sth.get("hash_algorithm") != "RFC9162_SHA256":
-        problems.append(f"{label}: STH hash_algorithm is not RFC9162_SHA256")
-    if receipt.get("hash_algorithm") != "RFC9162_SHA256":
-        problems.append(f"{label}: receipt hash_algorithm is not RFC9162_SHA256")
-    if receipt.get("log_id") != sth.get("log_id"):
-        problems.append(f"{label}: receipt log_id != its STH log_id")
-    try:
-        index = int(receipt.get("leaf_index"))
-    except (TypeError, ValueError):
-        index = -1
-    entry_path = HERE / "entries" / f"{index:06d}.json" if index >= 0 else None
-    if entry_path is None or not entry_path.exists():
-        problems.append(f"{label}: leaf_index {receipt.get('leaf_index')!r} names no published entry")
-        return problems
-    entry = json.loads(entry_path.read_text())
-    leaf_bytes = canonical_json(entry["leaf"])
-    # (a) the receipt's STH must be signed by THIS log's key ...
-    rsig = check_sth_signature(sth)
-    if rsig == "INVALID" or (rsig == "UNAVAILABLE" and not structural_only):
-        problems.append(f"{label}: STH signature {rsig}")
-    # (b) ... the named key fingerprint is REQUIRED and must be this key ...
-    fp = (sth.get("signatures", {}).get("ed25519", {}) or {}).get("public_key_fingerprint_sha256")
-    if not fp:
-        problems.append(f"{label}: STH lacks public_key_fingerprint_sha256 (required)")
-    elif (HERE / "provider.ed25519.pub").exists() and fp != key_fingerprint():
-        problems.append(f"{label}: STH signed by a different key than provider.ed25519.pub")
-    # (c) ... its log_id must be present and match the log ...
-    meta_path = HERE / "log-metadata.json"
-    if meta_path.exists():
-        meta_log_id = json.loads(meta_path.read_text()).get("log_id")
-        if meta_log_id and sth.get("log_id") != meta_log_id:
-            problems.append(f"{label}: STH log_id missing or not this log's")
-    # (d) ... the receipt's STH must appear in the published history ...
-    if heads and canonical_json(sth) not in {canonical_json(h) for h in heads}:
-        problems.append(f"{label}: STH not present in sth-history.jsonl")
-    # (e) ... the leaf_hash is REQUIRED and must match the named entry ...
-    if not receipt.get("leaf_hash"):
-        problems.append(f"{label}: leaf_hash missing (required)")
-    elif receipt["leaf_hash"] != leaf_hash(leaf_bytes).hex():
-        problems.append(f"{label}: leaf_hash does not match the named entry")
-    # (f) ... tree_size agreement ...
-    try:
-        size_agree = int(receipt.get("tree_size")) == int(sth.get("tree_size"))
-    except (TypeError, ValueError):
-        size_agree = False
-    if not size_agree:
-        problems.append(f"{label}: tree_size != its STH tree_size")
-    # (g) ... and finally the inclusion proof itself.
-    try:
-        ok = verify_inclusion(
-            leaf_bytes, index, int(receipt.get("tree_size") or 0),
-            [bytes.fromhex(h) for h in receipt.get("inclusion_proof") or []],
-            bytes.fromhex(sth.get("root_hash") or ""),
-        )
-    except (TypeError, ValueError):
-        ok = False
-    if not ok:
-        problems.append(f"{label}: inclusion proof INVALID")
-    print(f"receipt {label}: leaf {index} of {receipt.get('tree_size')} "
-          f"STH-sig:{rsig} bindings+inclusion:{'OK' if not problems else 'FAIL'}")
-    return problems
-
-
 def main() -> int:
     parser = argparse.ArgumentParser()
     parser.add_argument("--all", action="store_true")
     parser.add_argument("--receipt")
-    parser.add_argument("--structural-only", action="store_true",
-                        help="skip Ed25519 signature checks explicitly; the run reports a "
-                             "REDUCED check and can never print full verification.")
     args = parser.parse_args()
-
-    sigs_ok = signatures_available()
-    if not args.structural_only and not sigs_ok:
-        # Fail closed: a verifier that cannot check signatures must not
-        # imply it did. Do not silently continue.
-        print("FATAL: signature checking unavailable (need the `openssl` binary and "
-              "provider.ed25519.pub). Install openssl / fetch the key, or pass "
-              "--structural-only to run an explicit hashes-and-structure check.")
-        return 2
-
     leaves, problems = load_leaves()
     print(f"entries: {len(leaves)}")
     failures = list(problems)
     for problem in problems:
         print("PROBLEM:", problem)
 
-    history_path = HERE / "sth-history.jsonl"
-    heads = [json.loads(line) for line in history_path.read_text().splitlines() if line.strip()] if history_path.exists() else []
-
     if args.all or not args.receipt:
-        # log-wide checks (GPT §4.3): history internally consistent AND the
+        history_path = HERE / "sth-history.jsonl"
-        # published latest-sth.json is exactly the final history head.
+        heads = [json.loads(line) for line in history_path.read_text().splitlines() if line.strip()] if history_path.exists() else []
         previous = -1
-        log_id = None
         for position, head in enumerate(heads):
             size = int(head["tree_size"])
-            if size > len(leaves):
-                failures.append(f"STH #{position} claims size {size} > {len(leaves)} leaves")
             expected = merkle_root(leaves[:size]).hex()
             structural = "OK" if head["root_hash"] == expected and size >= previous else "MISMATCH"
             if structural != "OK":
-                failures.append(f"STH #{position} prefix-root/monotonicity")
+                failures.append(f"STH #{position}")
-            if log_id is None:
-                log_id = head.get("log_id")
-            elif head.get("log_id") != log_id:
-                failures.append(f"STH #{position} log_id changed mid-history")
             signature = check_sth_signature(head)
-            if signature == "INVALID" or (signature == "UNAVAILABLE" and not args.structural_only):
+            if signature == "INVALID":
-                failures.append(f"STH #{position} signature {signature}")
+                failures.append(f"STH #{position} signature")
             print(f"STH #{position} size={size} root={head['root_hash'][:16]}… prefix-root:{structural} signature:{signature}")
             previous = max(previous, size)
-        latest_path = HERE / "latest-sth.json"
-        if latest_path.exists() and heads:
-            latest = json.loads(latest_path.read_text())
-            if canonical_json(latest) != canonical_json(heads[-1]):
-                failures.append("latest-sth.json is not the final sth-history head")
-            elif int(latest["tree_size"]) != len(leaves):
-                failures.append(f"latest-sth tree_size {latest['tree_size']} != {len(leaves)} leaves")
-            else:
-                print(f"latest-sth: size {latest['tree_size']} == leaf count, and == final history head  OK")
-        for receipt_path in sorted((HERE / "receipts").glob("*.receipt.json")):
-            failures += verify_receipt(json.loads(receipt_path.read_text()),
-                                       heads, args.structural_only, receipt_path.name)
 
     if args.receipt:
-        failures += verify_receipt(json.loads(Path(args.receipt).read_text()),
+        receipt = json.loads(Path(args.receipt).read_text())
-                                   heads, args.structural_only, Path(args.receipt).name)
+        index = int(receipt["leaf_index"])
+        entry = json.loads((HERE / "entries" / f"{index:06d}.json").read_text())
+        ok = verify_inclusion(
+            canonical_json(entry["leaf"]),
+            index,
+            int(receipt["tree_size"]),
+            [bytes.fromhex(h) for h in receipt["inclusion_proof"]],
+            bytes.fromhex(receipt["sth"]["root_hash"]),
+        )
+        print(f"receipt leaf {index} of {receipt['tree_size']}: inclusion {'VALID' if ok else 'INVALID'}")
+        if not ok:
+            failures.append("receipt inclusion")
 
-    mode = "REDUCED (structural only, signatures NOT checked)" if args.structural_only else "full"
+    print("RESULT:", "OK - the log is internally consistent" if not failures else f"FAILED ({len(failures)} problems)")
-    if failures:
+    return 0 if not failures else 1
-        print(f"RESULT: FAILED ({len(failures)} problems) [{mode}]")
-        return 1
-    print(f"RESULT: OK [{mode}]"
-          + ("" if not args.structural_only else " — signatures were NOT verified; this is not full verification"))
-    return 0
 
 
 if __name__ == "__main__":

verify_selftest.py

@@ -1,96 +0,0 @@
-#!/usr/bin/env python3
-"""Adversarial self-test for verify.py — proves the fail-closed paths fail.
-
-Each case mutates a real published receipt (or the environment) and asserts
-the verifier REJECTS it; plus the honest controls. Exit 0 only if every case
-behaves. Run from a clone: python3 verify_selftest.py
-"""
-import copy
-import json
-import os
-import subprocess
-import sys
-import tempfile
-from pathlib import Path
-
-HERE = Path(__file__).resolve().parent
-
-
-def run(*args, env=None):
-    result = subprocess.run(
-        [sys.executable, str(HERE / "verify.py"), *args],
-        capture_output=True, text=True, env=env,
-    )
-    return result.returncode, result.stdout
-
-
-def base_receipt():
-    path = sorted((HERE / "receipts").glob("*.receipt.json"))[0]
-    return json.loads(path.read_text())
-
-
-def mutated(**changes):
-    receipt = copy.deepcopy(base_receipt())
-    for dotted, value in changes.items():
-        target, keys = receipt, dotted.split(".")
-        for key in keys[:-1]:
-            target = target[key]
-        if value is None:
-            target.pop(keys[-1], None)
-        else:
-            target[keys[-1]] = value
-    return receipt
-
-
-def check_receipt(receipt) -> int:
-    with tempfile.NamedTemporaryFile("w", suffix=".json", delete=False) as handle:
-        json.dump(receipt, handle)
-        path = handle.name
-    try:
-        code, _ = run("--receipt", path)
-        return code
-    finally:
-        os.unlink(path)
-
-
-def main() -> int:
-    cases = []
-
-    code, out = run("--all")
-    cases.append(("honest --all passes (full)", code == 0 and "RESULT: OK [full]" in out))
-    cases.append(("--all covers every published receipt",
-                  out.count("receipt ") == len(list((HERE / "receipts").glob("*.receipt.json")))))
-
-    cases.append(("honest receipt passes", check_receipt(base_receipt()) == 0))
-    cases.append(("missing key fingerprint REJECTED",
-                  check_receipt(mutated(**{"sth.signatures.ed25519.public_key_fingerprint_sha256": None})) == 1))
-    cases.append(("missing leaf_hash REJECTED", check_receipt(mutated(leaf_hash=None)) == 1))
-    cases.append(("wrong receipt type REJECTED", check_receipt(mutated(type="forged.v0")) == 1))
-    cases.append(("forged (unsigned) root REJECTED",
-                  check_receipt(mutated(**{"sth.root_hash": "ff" * 32})) == 1))
-    cases.append(("tree_size mismatch REJECTED",
-                  check_receipt(mutated(tree_size=int(base_receipt()["tree_size"]) + 1)) == 1))
-    cases.append(("wrong log_id REJECTED",
-                  check_receipt(mutated(**{"sth.log_id": "00" * 32})) == 1))
-
-    code, out = run("--all", "--structural-only")
-    cases.append(("--structural-only is explicit, never claims full",
-                  code == 0 and "REDUCED" in out and "[full]" not in out))
-
-    with tempfile.TemporaryDirectory() as tmp:
-        os.symlink(sys.executable, Path(tmp) / Path(sys.executable).name)
-        code, out = run("--all", env={"PATH": tmp})
-        cases.append(("no openssl -> FAIL CLOSED (exit 2)", code == 2))
-
-    width = max(len(name) for name, _ in cases)
-    for name, ok in cases:
-        print(f"{'PASS' if ok else 'FAIL'}  {name:<{width}}")
-    if all(ok for _, ok in cases):
-        print(f"SELFTEST GREEN ({len(cases)} cases)")
-        return 0
-    print("SELFTEST RED")
-    return 1
-
-
-if __name__ == "__main__":
-    sys.exit(main())