mirror of
https://github.com/saymrwulf/proof-aware-crypto-tooling-agent.git
synced 2026-09-04 20:03:40 +00:00
publish assets: sync the fail-open time bomb; llms/course/test docs refreshed (doc audit 2026-07-19)
REAL DEFECT found by the operator-ordered doc-freshness audit:
published_assets.py still carried the PRE-HARDENING fail-open verify.py
and the pre-Tier-2 README as the templates that log-publish drops into
the mirror — the next publish would have silently overwritten the
round-13-hardened fail-closed verifier and the corrected README with
the old versions. Fixed:
- published_assets.py regenerated from the canonical mirror files
(byte-identity verified by round-trip exec), now also carrying
verify_selftest.py; SYNC RULE documented in the module docstring.
- transparency_log.publish() now writes verify_selftest.py too.
- NEW tests/test_published_assets.py pins the security-critical markers
(fail-closed FATAL, RECEIPT_TYPE, verify_receipt, --all receipt
coverage, required fingerprint) so template drift fails CI instead of
shipping.
- test_web_and_witness updated to the hardened verifier's markers —
the published test log now passes FULL signature mode end to end
('RESULT: OK [full]'), a stronger assertion than the old string.
Doc refresh in the same pass:
- llms.txt: thirteen leaves + entry-13 self-attestation + fail-closed
verifier; paper line -> new title, 23 pages, v0.2/v0.1 archives.
- Course (generator + generated 06b notebook): 'the git hash IS the
content hash' -> 'the commit pins the exact source tree';
'irrevocably part of the log every other agent sees' -> 'committed to
the log's signed view, which any agent can compare' (the two Tier-2
scope corrections had never reached the teaching material).
- test_paper_verifiers.py docstring rescoped: its 164k counts are the
archived v0.2 report's citation; the current paper cites the corpus
harness and makes no extensional-equality claim.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
This commit is contained in:
parent
07302d9e66
commit
2587cc018b
8 changed files with 338 additions and 55 deletions
4
llms.txt
4
llms.txt
|
|
@ -17,8 +17,8 @@
|
||||||
|
|
||||||
## Live evidence
|
## Live evidence
|
||||||
|
|
||||||
- Transparency log (RFC 9162): https://ltl.zkdefi.org — signed replay attestations of the Lean proofs, one leaf per fork.
|
- Transparency log (RFC 9162): https://ltl.zkdefi.org — signed replay attestations of the Lean proofs. Thirteen leaves: three replay generations over four Ed25519 forks, plus entry 13 attesting the Lean mechanization of the log's own accumulator model. The mirror ships a fail-closed offline verifier (verify.py --all covers every leaf, signed head, and receipt) with an adversarial self-test.
|
||||||
- The paper: https://ltl.zkdefi.org/paper — "The Lean Transparency Log: Distributing Kernel-Checked Correctness Evidence for Deployed Ed25519 Implementations" (revised, with security proofs, 19 pages; prior version at /paper/v0.1).
|
- The paper: https://ltl.zkdefi.org/paper — "Accountable Distribution of Machine-Checked Correctness Evidence: A Transparency Model and the Lean Transparency Log" (23 pages: trust decomposition, scheme-level accountability games with explicit reductions, live deployment, and the measured model/deployment divergence reported as a result). Earlier versions archived at /paper/v0.2 (19 pages) and /paper/v0.1 (4 pages).
|
||||||
|
|
||||||
## For agents
|
## For agents
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -231,8 +231,8 @@
|
||||||
"After these cells pass, the agent knows: *the provider whose key I\n",
|
"After these cells pass, the agent knows: *the provider whose key I\n",
|
||||||
"pinned states that the Lean proofs of repository X at commit Y check\n",
|
"pinned states that the Lean proofs of repository X at commit Y check\n",
|
||||||
"out with exactly the documented assumptions, and that statement is\n",
|
"out with exactly the documented assumptions, and that statement is\n",
|
||||||
"irrevocably part of the log every other agent sees.* The agent then\n",
|
"committed to the log's signed view, which any agent can compare.* The agent then\n",
|
||||||
"clones commit Y (the git hash IS the content hash) and builds it -\n",
|
"clones commit Y (the commit pins the exact source tree) and builds it -\n",
|
||||||
"compiler and build remain declared trusted base until R5. Where a\n",
|
"compiler and build remain declared trusted base until R5. Where a\n",
|
||||||
"claim lives (this notebook) and why it is true (the provider's Lean\n",
|
"claim lives (this notebook) and why it is true (the provider's Lean\n",
|
||||||
"replay, lecture 6a) never blur.\n",
|
"replay, lecture 6a) never blur.\n",
|
||||||
|
|
|
||||||
|
|
@ -1,22 +1,45 @@
|
||||||
"""Static assets dropped into the git-published log repository: a
|
"""Static assets dropped into the git-published log repository: the
|
||||||
standalone stdlib-only verifier and the customer README. Kept as string
|
standalone fail-closed verifier, its adversarial self-test, and the
|
||||||
constants so the published repo is fully self-contained."""
|
customer README. Kept as string constants so the published repo is fully
|
||||||
|
self-contained.
|
||||||
|
|
||||||
VERIFY_PY = '''#!/usr/bin/env python3
|
SYNC RULE: these constants MUST stay byte-identical to the canonical
|
||||||
|
files in the published mirror (lean-transparency-log: verify.py,
|
||||||
|
verify_selftest.py, README.md). A publish overwrites the mirror copies
|
||||||
|
from here, so drift REGRESSES shipped fixes (found 2026-07-19: this file
|
||||||
|
still carried the pre-hardening fail-open verify.py and the pre-Tier-2
|
||||||
|
README). tests/test_published_assets.py pins the security-critical
|
||||||
|
markers; regenerate from the canonical files rather than hand-editing.
|
||||||
|
"""
|
||||||
|
|
||||||
|
VERIFY_PY = r'''#!/usr/bin/env python3
|
||||||
"""Standalone verifier for the published Lean Transparency Log.
|
"""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:
|
files in this repository alone:
|
||||||
|
|
||||||
1. every entry's leaf hash,
|
1. every entry's leaf hash,
|
||||||
2. every historical Signed Tree Head against the recomputed prefix root
|
2. every historical Signed Tree Head against the recomputed prefix root
|
||||||
(this is the witness check: a split view or tampered entry fails here),
|
(a split view or tampered entry fails here),
|
||||||
3. every STH Ed25519 signature (via the openssl binary, if available),
|
3. every STH Ed25519 signature,
|
||||||
4. any receipt's inclusion proof (--receipt FILE).
|
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:
|
Usage:
|
||||||
python3 verify.py --all
|
python3 verify.py --all
|
||||||
python3 verify.py --receipt receipts/dalek-ed25519-verified.receipt.json
|
python3 verify.py --receipt receipts/dalek-ed25519-verified.receipt.json
|
||||||
|
python3 verify.py --all --structural-only # explicit reduced check
|
||||||
"""
|
"""
|
||||||
import argparse
|
import argparse
|
||||||
import base64
|
import base64
|
||||||
|
|
@ -32,11 +55,11 @@ HERE = Path(__file__).resolve().parent
|
||||||
|
|
||||||
|
|
||||||
def leaf_hash(data: bytes) -> bytes:
|
def leaf_hash(data: bytes) -> bytes:
|
||||||
return hashlib.sha256(b"\\x00" + data).digest()
|
return hashlib.sha256(b"\x00" + data).digest()
|
||||||
|
|
||||||
|
|
||||||
def node_hash(left: bytes, right: bytes) -> bytes:
|
def node_hash(left: bytes, right: bytes) -> bytes:
|
||||||
return hashlib.sha256(b"\\x01" + left + right).digest()
|
return hashlib.sha256(b"\x01" + left + right).digest()
|
||||||
|
|
||||||
|
|
||||||
def merkle_root(leaves):
|
def merkle_root(leaves):
|
||||||
|
|
@ -86,11 +109,21 @@ def load_leaves():
|
||||||
return leaves, problems
|
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:
|
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")
|
openssl = shutil.which("openssl")
|
||||||
key = HERE / "provider.ed25519.pub"
|
key = HERE / "provider.ed25519.pub"
|
||||||
if not openssl or not key.exists():
|
if not openssl or not key.exists():
|
||||||
return "skipped (openssl or provider.ed25519.pub missing)"
|
return "UNAVAILABLE"
|
||||||
signatures = head.get("signatures") or {}
|
signatures = head.get("signatures") or {}
|
||||||
ed = signatures.get("ed25519") or {}
|
ed = signatures.get("ed25519") or {}
|
||||||
payload = canonical_json({k: v for k, v in head.items() if k != "signatures"})
|
payload = canonical_json({k: v for k, v in head.items() if k != "signatures"})
|
||||||
|
|
@ -107,62 +140,271 @@ def check_sth_signature(head) -> str:
|
||||||
return "VALID" if result.returncode == 0 else "INVALID"
|
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:
|
def main() -> int:
|
||||||
parser = argparse.ArgumentParser()
|
parser = argparse.ArgumentParser()
|
||||||
parser.add_argument("--all", action="store_true")
|
parser.add_argument("--all", action="store_true")
|
||||||
parser.add_argument("--receipt")
|
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()
|
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()
|
leaves, problems = load_leaves()
|
||||||
print(f"entries: {len(leaves)}")
|
print(f"entries: {len(leaves)}")
|
||||||
failures = list(problems)
|
failures = list(problems)
|
||||||
for problem in problems:
|
for problem in problems:
|
||||||
print("PROBLEM:", problem)
|
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:
|
if args.all or not args.receipt:
|
||||||
history_path = HERE / "sth-history.jsonl"
|
# log-wide checks (GPT §4.3): history internally consistent AND the
|
||||||
heads = [json.loads(line) for line in history_path.read_text().splitlines() if line.strip()] if history_path.exists() else []
|
# published latest-sth.json is exactly the final history head.
|
||||||
previous = -1
|
previous = -1
|
||||||
|
log_id = None
|
||||||
for position, head in enumerate(heads):
|
for position, head in enumerate(heads):
|
||||||
size = int(head["tree_size"])
|
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()
|
expected = merkle_root(leaves[:size]).hex()
|
||||||
structural = "OK" if head["root_hash"] == expected and size >= previous else "MISMATCH"
|
structural = "OK" if head["root_hash"] == expected and size >= previous else "MISMATCH"
|
||||||
if structural != "OK":
|
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)
|
signature = check_sth_signature(head)
|
||||||
if signature == "INVALID":
|
if signature == "INVALID" or (signature == "UNAVAILABLE" and not args.structural_only):
|
||||||
failures.append(f"STH #{position} signature")
|
failures.append(f"STH #{position} signature {signature}")
|
||||||
print(f"STH #{position} size={size} root={head['root_hash'][:16]}… prefix-root:{structural} signature:{signature}")
|
print(f"STH #{position} size={size} root={head['root_hash'][:16]}… prefix-root:{structural} signature:{signature}")
|
||||||
previous = max(previous, size)
|
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:
|
if args.receipt:
|
||||||
receipt = json.loads(Path(args.receipt).read_text())
|
failures += verify_receipt(json.loads(Path(args.receipt).read_text()),
|
||||||
index = int(receipt["leaf_index"])
|
heads, args.structural_only, Path(args.receipt).name)
|
||||||
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")
|
|
||||||
|
|
||||||
print("RESULT:", "OK - the log is internally consistent" if not failures else f"FAILED ({len(failures)} problems)")
|
mode = "REDUCED (structural only, signatures NOT checked)" if args.structural_only else "full"
|
||||||
return 0 if not failures else 1
|
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__":
|
if __name__ == "__main__":
|
||||||
sys.exit(main())
|
sys.exit(main())
|
||||||
'''
|
'''
|
||||||
|
|
||||||
README_MD = """# Lean Transparency Log — published mirror
|
VERIFY_SELFTEST_PY = r'''#!/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())
|
||||||
|
'''
|
||||||
|
|
||||||
|
README_MD = r'''# Lean Transparency Log — published mirror
|
||||||
|
|
||||||
This repository is the **git-published face** of a transparency log of
|
This repository is the **git-published face** of a transparency log of
|
||||||
formal-verification attestations: signed statements that the Lean 4 proofs
|
formal-verification attestations: signed statements that the Lean 4 proofs
|
||||||
of specific cryptographic Rust libraries, at specific git commits,
|
of specific software, at specific git commits, re-check with exactly their
|
||||||
re-check with exactly their documented assumptions.
|
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:
|
Layout:
|
||||||
|
|
||||||
|
|
@ -173,8 +415,9 @@ Layout:
|
||||||
| `receipts/<component>.receipt.json` | inclusion proof binding that attestation to the latest signed head |
|
| `receipts/<component>.receipt.json` | inclusion proof binding that attestation to the latest signed head |
|
||||||
| `sth-history.jsonl` | **every** Signed Tree Head ever issued — the witness channel: all cloners see the same heads |
|
| `sth-history.jsonl` | **every** Signed Tree Head ever issued — the witness channel: all cloners see the same heads |
|
||||||
| `latest-sth.json` | the current head |
|
| `latest-sth.json` | the current head |
|
||||||
| `provider.ed25519.pub` | the provider's public key (the sole trust anchor) |
|
| `provider.ed25519.pub` | the provider's public key — the sole cryptographic identity anchor; each statement's truth additionally rests on the assumptions stated in its leaf |
|
||||||
| `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 everything locally, no installation:
|
||||||
|
|
||||||
|
|
@ -190,10 +433,11 @@ The provider tooling, agent tooling, and course materials:
|
||||||
**https://github.com/saymrwulf/proof-aware-crypto-tooling-agent**
|
**https://github.com/saymrwulf/proof-aware-crypto-tooling-agent**
|
||||||
|
|
||||||
Honesty notes, always in force: attestations cover Rust **source** at a
|
Honesty notes, always in force: attestations cover Rust **source** at a
|
||||||
pinned commit (clone it — the git hash is the content hash — and build it
|
pinned commit (clone it — the commit identifies the committed git tree,
|
||||||
yourself; compilers are declared trusted base). The log deliberately
|
not dependencies or toolchains — and build it yourself; compilers are
|
||||||
|
declared trusted base). The log deliberately
|
||||||
retains early leaves recording a **failed** audit run: an append-only
|
retains early leaves recording a **failed** audit run: an append-only
|
||||||
trust ledger keeps its history. Tree heads are signed by the merkleized,
|
trust ledger keeps its history. Tree heads are signed by the merkleized,
|
||||||
proof-attested Ed25519 library itself, and each signature embeds the
|
proof-attested Ed25519 library itself, and each signature embeds the
|
||||||
provider's own Merkle self-check of that library's leaf.
|
provider's own Merkle self-check of that library's leaf.
|
||||||
"""
|
'''
|
||||||
|
|
|
||||||
|
|
@ -295,9 +295,10 @@ class TransparencyLog:
|
||||||
(out / "entries" / f"{component}.attestation.json").write_text(
|
(out / "entries" / f"{component}.attestation.json").write_text(
|
||||||
json.dumps(entry.leaf.get("attestation"), indent=2, sort_keys=True) + "\n", encoding="utf-8"
|
json.dumps(entry.leaf.get("attestation"), indent=2, sort_keys=True) + "\n", encoding="utf-8"
|
||||||
)
|
)
|
||||||
from .published_assets import README_MD, VERIFY_PY
|
from .published_assets import README_MD, VERIFY_PY, VERIFY_SELFTEST_PY
|
||||||
|
|
||||||
(out / "verify.py").write_text(VERIFY_PY, encoding="utf-8")
|
(out / "verify.py").write_text(VERIFY_PY, encoding="utf-8")
|
||||||
|
(out / "verify_selftest.py").write_text(VERIFY_SELFTEST_PY, encoding="utf-8")
|
||||||
(out / "README.md").write_text(README_MD, encoding="utf-8")
|
(out / "README.md").write_text(README_MD, encoding="utf-8")
|
||||||
if public_key_path is not None:
|
if public_key_path is not None:
|
||||||
(out / "provider.ed25519.pub").write_bytes(Path(public_key_path).read_bytes())
|
(out / "provider.ed25519.pub").write_bytes(Path(public_key_path).read_bytes())
|
||||||
|
|
|
||||||
|
|
@ -1560,8 +1560,8 @@ COURSE = {
|
||||||
After these cells pass, the agent knows: *the provider whose key I
|
After these cells pass, the agent knows: *the provider whose key I
|
||||||
pinned states that the Lean proofs of repository X at commit Y check
|
pinned states that the Lean proofs of repository X at commit Y check
|
||||||
out with exactly the documented assumptions, and that statement is
|
out with exactly the documented assumptions, and that statement is
|
||||||
irrevocably part of the log every other agent sees.* The agent then
|
committed to the log's signed view, which any agent can compare.* The agent then
|
||||||
clones commit Y (the git hash IS the content hash) and builds it -
|
clones commit Y (the commit pins the exact source tree) and builds it -
|
||||||
compiler and build remain declared trusted base until R5. Where a
|
compiler and build remain declared trusted base until R5. Where a
|
||||||
claim lives (this notebook) and why it is true (the provider's Lean
|
claim lives (this notebook) and why it is true (the provider's Lean
|
||||||
replay, lecture 6a) never blur.
|
replay, lecture 6a) never blur.
|
||||||
|
|
|
||||||
|
|
@ -1,11 +1,12 @@
|
||||||
"""The paper (ltl.tex, §5.3, App. B) claims the *recursive* inclusion and
|
"""Historical regression pin from the archived v0.2 system report
|
||||||
consistency verifiers it defines and proves about are equivalent to the
|
(hosted at /paper/v0.2), which cited these exact differential-testing
|
||||||
deployed iterative RFC 9162 verifiers, and cites exhaustive
|
counts (164,479 inclusion; 164,224 consistency) for its recursive forms
|
||||||
differential-testing counts. This test IS that verification, so the paper's
|
against the deployed iterative RFC 9162 verifiers over these families.
|
||||||
numbers cannot silently rot: it reproduces the exact recursive forms
|
The CURRENT paper makes no extensional-equality claim: it cites the
|
||||||
written in the paper and asserts full agreement with the deployed code over
|
accumulator corpus's fidelity harness instead (230,271 / 230,016 honest
|
||||||
all sizes up to 256, honest inputs plus adversarial mutations, and pins the
|
families, 73,573 lied-size cases with 3,867 divergences, every one
|
||||||
cited case counts (164,479 inclusion; 164,224 consistency).
|
accepted only by the deployed verifier). This test remains as a pinned
|
||||||
|
regression boundary for the pacta-internal recursive forms.
|
||||||
"""
|
"""
|
||||||
|
|
||||||
import hashlib
|
import hashlib
|
||||||
|
|
|
||||||
35
tests/test_published_assets.py
Normal file
35
tests/test_published_assets.py
Normal file
|
|
@ -0,0 +1,35 @@
|
||||||
|
"""The publish step overwrites the mirror's verify.py / verify_selftest.py /
|
||||||
|
README.md from the frozen constants in published_assets. A hardening
|
||||||
|
regression here silently fail-opens the PUBLIC verifier on the next publish
|
||||||
|
(exactly what the 2026-07-19 doc audit found: the constants still carried
|
||||||
|
the pre-hardening fail-open verify.py). These tests pin the
|
||||||
|
security-critical markers so that drift fails CI instead of shipping."""
|
||||||
|
|
||||||
|
from pacta_provider.published_assets import README_MD, VERIFY_PY, VERIFY_SELFTEST_PY
|
||||||
|
|
||||||
|
|
||||||
|
def test_verify_py_compiles_and_is_the_hardened_verifier():
|
||||||
|
compile(VERIFY_PY, "verify.py", "exec")
|
||||||
|
for marker in (
|
||||||
|
"FATAL: signature checking unavailable", # fail-closed exit 2
|
||||||
|
"RECEIPT_TYPE", # required type binding
|
||||||
|
"def verify_receipt", # full binding checks
|
||||||
|
"--structural-only", # explicit reduced mode
|
||||||
|
'glob("*.receipt.json")', # --all covers every receipt
|
||||||
|
"public_key_fingerprint_sha256", # required fingerprint
|
||||||
|
):
|
||||||
|
assert marker in VERIFY_PY, f"hardening marker missing: {marker}"
|
||||||
|
|
||||||
|
|
||||||
|
def test_selftest_compiles_and_covers_fail_closed():
|
||||||
|
compile(VERIFY_SELFTEST_PY, "verify_selftest.py", "exec")
|
||||||
|
for marker in ("FAIL CLOSED", "missing key fingerprint REJECTED",
|
||||||
|
"forged (unsigned) root REJECTED"):
|
||||||
|
assert marker in VERIFY_SELFTEST_PY, marker
|
||||||
|
|
||||||
|
|
||||||
|
def test_readme_is_the_corrected_template():
|
||||||
|
assert "identity anchor" in README_MD
|
||||||
|
assert "verify_selftest.py" in README_MD
|
||||||
|
assert "the git hash is the content hash" not in README_MD
|
||||||
|
assert "sole trust anchor" not in README_MD
|
||||||
|
|
@ -132,6 +132,7 @@ def test_publish_and_witness_audit_catches_tampering(tmp_path):
|
||||||
report = log.publish(published, public_key_path=tmp_path / "k.pub")
|
report = log.publish(published, public_key_path=tmp_path / "k.pub")
|
||||||
assert report["entries"] == 3
|
assert report["entries"] == 3
|
||||||
assert (published / "verify.py").exists() and (published / "README.md").exists()
|
assert (published / "verify.py").exists() and (published / "README.md").exists()
|
||||||
|
assert (published / "verify_selftest.py").exists()
|
||||||
|
|
||||||
clean = audit_published_log(published, tmp_path / "k.pub")
|
clean = audit_published_log(published, tmp_path / "k.pub")
|
||||||
assert clean.ok and clean.heads_checked == 3
|
assert clean.ok and clean.heads_checked == 3
|
||||||
|
|
@ -156,4 +157,5 @@ def test_standalone_verify_py_runs(tmp_path):
|
||||||
log.publish(published, public_key_path=tmp_path / "k.pub")
|
log.publish(published, public_key_path=tmp_path / "k.pub")
|
||||||
result = subprocess.run([sys.executable, "verify.py", "--all"], cwd=published, capture_output=True, text=True)
|
result = subprocess.run([sys.executable, "verify.py", "--all"], cwd=published, capture_output=True, text=True)
|
||||||
assert result.returncode == 0, result.stdout + result.stderr
|
assert result.returncode == 0, result.stdout + result.stderr
|
||||||
assert "OK - the log is internally consistent" in result.stdout
|
# hardened verifier: full mode (signatures verified) must report exactly this
|
||||||
|
assert "RESULT: OK [full]" in result.stdout
|
||||||
|
|
|
||||||
Loading…
Reference in a new issue