verify.py: --all verifies every published receipt; binding fields required, not compare-if-present (round-12 GPT B4)

Round-12 review found two artifact-claim gaps: --all never touched
receipts, and receipt mode checked fingerprint/leaf_hash only when
present. Now:
- --all enumerates receipts/*.receipt.json and runs the full binding
  list on each (type tag, STH signature, REQUIRED key fingerprint,
  log_id vs log-metadata, STH membership in the published history,
  REQUIRED leaf_hash vs the named entry, tree_size agreement, receipt
  hash_algorithm + log_id consistency, inclusion proof).
- --receipt FILE routes through the same function.
- Malformed values (bad hex, missing sizes) are failures, not crashes.
- NEW verify_selftest.py: 11-case adversarial battery (mutated real
  receipts must be REJECTED: no fingerprint, no leaf_hash, wrong type,
  forged root, size mismatch, wrong log_id; honest controls pass;
  structural-only never claims full; no-openssl exits 2). GREEN.
One bug caught by the honest controls during development: the new
hash-algorithm check assumed 'sha256' but deployed heads carry
'RFC9162_SHA256' - fixed against reality, plus receipt-level
hash_algorithm/log_id binding added.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

README.md

@@ -2,8 +2,17 @@
 
 This repository is the **git-published face** of a transparency log of
 formal-verification attestations: signed statements that the Lean 4 proofs
-of specific cryptographic Rust libraries, at specific git commits,
-re-check with exactly their documented assumptions.
+of specific software, at specific git commits, re-check with exactly their
+documented assumptions. Its first twelve leaves attest four cryptographic
+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:
 
@@ -15,7 +24,8 @@ 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 standard library only |
+| `verify.py` | standalone verifier (Python stdlib + the `openssl` binary; fails closed without them; `--all` covers every published receipt) |
+| `verify_selftest.py` | adversarial self-test: proves the verifier's fail-closed paths reject mutated receipts |
 
 Verify everything locally, no installation:
 

verify.py

@@ -1,18 +1,31 @@
 #!/usr/bin/env python3
 """Standalone verifier for the published Lean Transparency Log.
 
-Python 3 standard library ONLY - no pacta, no pip. Verifies, from the
+Pure Python 3 standard library for hashing and structure; Ed25519
+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
-     (this is the witness check: a split view or tampered entry fails here),
-  3. every STH Ed25519 signature (via the openssl binary, if available),
-  4. any receipt's inclusion proof (--receipt FILE).
+     (a split view or tampered entry fails here),
+  3. every STH Ed25519 signature,
+  4. every published receipt under receipts/ (with --all), and any receipt
+     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
@@ -82,11 +95,21 @@ 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 "skipped (openssl or provider.ed25519.pub missing)"
+        return "UNAVAILABLE"
     signatures = head.get("signatures") or {}
     ed = signatures.get("ed25519") or {}
     payload = canonical_json({k: v for k, v in head.items() if k != "signatures"})
@@ -103,50 +126,152 @@ 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:
-        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 []
+        # log-wide checks (GPT §4.3): history internally consistent AND the
+        # published latest-sth.json is exactly the final history head.
         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}")
+                failures.append(f"STH #{position} prefix-root/monotonicity")
+            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":
-                failures.append(f"STH #{position} signature")
+            if signature == "INVALID" or (signature == "UNAVAILABLE" and not args.structural_only):
+                failures.append(f"STH #{position} signature {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:
-        receipt = json.loads(Path(args.receipt).read_text())
-        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")
+        failures += verify_receipt(json.loads(Path(args.receipt).read_text()),
+                                   heads, args.structural_only, Path(args.receipt).name)
 
-    print("RESULT:", "OK - the log is internally consistent" if not failures else f"FAILED ({len(failures)} problems)")
-    return 0 if not failures else 1
+    mode = "REDUCED (structural only, signatures NOT checked)" if args.structural_only else "full"
+    if failures:
+        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

@@ -0,0 +1,96 @@
+#!/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())