Correctness:
- ledger: single-flight fcntl lock over read-modify-append + fsync. Two
concurrent writers previously could fork the hash chain (read same tail,
same prev_hash). New test races 8 threads x6 appends; chain stays intact
with contiguous indices.
- small-order list: the order-8 encodings were hand-typed and unverifiable
and diverged from the canonical libsodium blocklist. A BOGUS entry is the
only dangerous direction (it down-grades a real tamper to a note, skipping
the latch), so the list is now the certain-low-order set only (y in
{0,1,-1}, reduced/non-reduced, both sign bits); order-8 edges escalate to
tamper until a derived list lands. Fail-safe asymmetry documented + tested.
- freshness: removed a tautological .
Non-functional:
- quorum members now run concurrently (ThreadPoolExecutor): a verify costs
one member's latency, not the sum (~17ms for 4 members, live).
- Wallet.quorum() memoized per state_dir: binary swap-detection hashes run
once at assembly, not on every verify; documented rationale.
85 tests green; live 4-fork wallet re-verified end-to-end.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
- web.py: /paper (and /paper/ltl.pdf) serve the committed PDF, loaded
once at startup from the repo checkout; listed in the 404 endpoint
index; covered by the web roundtrip test
- docs page: 'The paper' card linking the PDF
- DEPLOY.md: the second witness mirror belongs on a host the operator
does NOT control (a self-hosted mirror adds no equivocation defense)
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
- serve/webdocs/cli default to base_path='' (own subdomain, root serving)
- webdocs link builder handles the empty base like web.py already did
- all docs, paper, notebook 06b, and published-mirror README point at
https://ltl.zkdefi.org; DEPLOY.md rewritten for subdomain + redirect
- tests: root mount is the production shape; one test keeps exercising
the path-mounted variant
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Three synchronized faces of one log - transport orthogonal to trust:
- PUBLISHED GIT MIRROR: log-publish exports the public face (one file
per leaf so git history mirrors log history; the FULL STH history as
the witness channel; per-component attestations + receipts; the
provider public key; a standalone stdlib-only verify.py and customer
README). Live at github.com/saymrwulf/lean-transparency-log (genesis:
8 leaves incl. the honest failed-run entries, dogfood-signed head).
- ONLINE SERVICE (pacta_provider serve): read-only, zero-dependency
HTTP with CT-style endpoints under a base path for
zkdefi.org/lean-transparency-log - /v1/sth, /v1/sth-history,
/v1/sth-consistency?first=N, /v1/proof, /v1/attestation, /v1/entries,
/v1/metadata, /healthz - plus self-contained customer documentation
at /docs (current state, attested components, API, the verify-
without-trusting-this-site path, and the means/does-NOT-mean
boundary). The process never loads private keys: heads are signed
offline; a compromised server can withhold or replay (pinning +
freshness detect both) but never forge. STH history now recorded
append-only by the provider (with a backfill head signed for the
existing log).
- AGENT ONLINE CLIENT: pacta log-fetch (download evidence; explicitly
UNVERIFIED until receipt-verify runs - transport is not trust) and
pacta sth-refresh (fetch head, verify signature, advance the pin via
an online consistency proof from the pinned size; fail closed).
- WITNESSES: pacta witness-audit over a clone of the published mirror
recomputes every prefix root from the public leaves and checks every
historical head + signature - no consistency proofs needed when the
leaves are public. Tampering one published entry trips both the
leaf-hash check and the prefix-root check (tested). verify.py gives
customers the same audit with zero installation.
- DEPLOY.md: the complete server-session checklist for zkdefi.org -
reconstruct the servable log FROM the published mirror (the server
stays in witness trust-position), hardened systemd unit, nginx/Caddy
path routing, Forgejo mirror setup, the provider->world update
cycle, and remote smoke tests.
Validated end-to-end on the REAL log: all 10 endpoints, online-fetched
proof re-verified locally through the dogfood verifier with pinning,
online pin refresh, publish + witness audit green, tamper caught,
standalone verify.py green in the published clone. 54/54 tests.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The trust architecture has exactly two roles and the curriculum now
mirrors that split structurally - the conceptual burden is the design,
stated as such to the student:
- 06a THE PROVIDER'S SIDE (singleton). Domain banner in the provider's
voice. The full build pipeline run live in a scratch log made from
the REAL attestations: verify (Lean replay = the leaf-making step,
the only expensive one - the shipped evidence IS its output) -> leaf
(0x00 domain separation) -> tree -> STH signed via the MERKLEIZED
LIBRARY -> the self-inclusion check embedded in the signature block.
A generated SVG draws the student's own tree: leaves, internal
nodes, root, and the signature box, framed in the provider's domain
color. Closes with the singleton-vs-many justification table
(key/cost/obligation asymmetry) and exercises.
- 06b THE AGENT'S SIDE (one of many). Domain banner in the agent's
voice: you own the public key, the evidence files, ~25 lines of
hashing - and explicitly NO Lean. The COMPLETE RFC 9162 inclusion
verifier is implemented from scratch in one cell (hashlib only, no
pacta imports for the core) and run against the REAL dalek receipt
(leaf 4 of 8, three siblings, dogfood-signed root); then the STH
signature, the provider's signing_provenance read and interpreted
(why the agent still re-checks inclusion itself), the pin store, and
an SVG of the real log with the agent's path highlighted against the
grey leaves it never needs. Cost line: ~4 hashes + 1 signature.
- Lecture 06 now routes students into the pair and states the mirror
rule ("if you cannot say which notebook a step belongs to, you have
not understood the step"); lecture 09 records that dogfood now runs
in BOTH directions; course map + README updated.
Every cell of 06a/06b/09 executed against the real evidence before
commit (SVGs render in Jupyter, fail soft in plain exec). One
generation bug found and fixed: a single-backslash \\x00 in the
generator produced a literal NUL byte in a cell. 50/50 tests green
with the notebook inventory at twelve.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The dogfood principle now runs in BOTH directions. Agents already
verified signatures through the proven dalek path; now the provider
SIGNS with it too, and proves to itself that the signing code is in its
own log before every signature:
- dogfood binary gains a `sign` mode (seed over stdin, never argv;
ed25519_dalek::SigningKey from the same pinned merkleized workspace).
Honesty ledger unchanged: the library's VERIFY path is
certificate-covered; its signing path is declared trusted base - but
it is the ATTESTED artifact, not an un-attested third implementation.
- sign_payload_ed25519_detailed: signing dispatch mirroring the verify
dispatch; the backend that actually signed is recorded in every
attestation signature block and STH.
- THE SELF-REFERENTIAL CHECK: before signing any tree head, the
provider runs the SAME Merkle inclusion verification an agent runs -
against the very tree it is about to sign - for the newest leaf
attesting the signing library itself, and embeds the result in the
signature block:
signing_provenance:
signing_backend: verified-dalek-serial
signing_library_component: dalek-ed25519-verified
signing_library_source_commit: aa0f6ab...
self_inclusion: verified
signing_library_leaf_index: 4
signing_library_certificates_proven: 16/16
A root signature that names the leaf vouching for the code that
produced it. First-append chicken-and-egg is handled honestly
(self_inclusion: library_not_in_log).
- Evidence refreshed: all four receipts re-issued under dogfood-signed
STHs; the full agent verify loop re-run green.
50/50 tests (new signing roundtrip test, skip-safe where unbuilt).
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The notebooks now carry the same didactic contract as the companion book
(the "ratchet rule", stated in the course map): every load-bearing idea
runs twice - napkin scale, then real scale - and every pair is EXECUTABLE
in the notebook, not narrated.
- Lecture 1: the truth boundary updated to the proven four-tier apex,
with the what-is-still-NOT-proven list (SHA-512, parsers, signing,
wallets) given equal weight.
- Lecture 2: napkin/real scoring pair - a two-certificate toy card
scored in your head, then the shipped sixteen-certificate R4 fixture
through the same function, residual blockers and per-tier boundary
axioms printed.
- Lecture 6: new split-view section. A runnable equivocation drill:
pin a two-leaf view, grow it honestly with a consistency proof, then
present a forged same-size root and watch the pin store name the
attack. Real-scale pointers to --sth-store, log-consistency,
log-audit, and the freshness policy; a new exercise asks students to
construct the lie a size-only anchor check would miss.
- Lecture 7: the wallet gate now swings BOTH ways on real evidence -
a partial card denied at R3, the shipped R4 card allowed - both
runnable.
- Lecture 8 capstone: "design R4" became "audit R4": read the shipped
card like an auditor, then design the R5 discharge plan (parser
specs, verified SHA-512, signing-side, per-fork production-path
mapping).
- NEW Lecture 9, "Eat Your Own Dogfood": the honest coverage ledger of
the proven-path verifier; a napkin PEM decode (the fixed 12-byte
Ed25519 SPKI prefix, read with your eyes) paired with the mechanical
extraction; live backend dispatch; the fail-closed
--require-verified-verifier policy; and the hybrid-PQC section -
proven-classical Ed25519 plus a required-but-honest ML-DSA slot
("blockers get fixed; placeholders get trusted").
Every code cell of the changed notebooks was executed end-to-end before
committing (outputs stripped per house rules). 49/49 tests green with
the notebook inventory updated.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
"Eat your own dogfood": pacta consumes certificates about a verified
Ed25519 implementation while checking those certificates' signatures
with OpenSSL. Now it can use the object of its own evidence:
- dogfood/pacta-verified-verify: a ~90-line Rust binary built against
the PINNED proven source workspace (saymrwulf/curve25519-dalek-source
at the exact commit the dalek certificates pin - the build records it:
aa0f6ab...) with the serial backend pinned via RUSTFLAGS exactly as
the verified extraction pins it. Cargo.toml is committed as a template
({{SOURCE}} placeholder) so no machine path is hardcoded; the rendered
file, target/, and the built binary are gitignored.
- pacta dogfood-build --source <workspace>: renders, builds, installs
to dogfood/state/, and writes a provenance sidecar (source commit,
backend cfg, rustc, and an honest coverage note: the certificates
cover verify_sha512, the extraction-refactored image of this verify
path; SHA-512 and the wire glue remain the theorems' documented
boundary). pacta dogfood-status reports the active backend.
- signing.verify_payload_ed25519_detailed: dispatch - the dogfood
binary when present (backend "verified-dalek-serial"), OpenSSL
fallback otherwise, and the backend that ACTUALLY ran is recorded in
receipt signature statuses and attestation evidence. Fallback is
never silent.
- --require-verified-verifier (receipt-verify + agent): policy fails
closed when verification did not run on the certificate-covered
path.
- ML-DSA is deliberately unchanged: no proven implementation exists,
so the slot stays fail-closed "unavailable" - the honest hybrid-PQC
posture is one proven-classical signature plus one required-but-
unproven PQC slot, never a pretend backend.
Validated live: receipt verification through the proven verifier
(backend recorded), a corrupted signature bit rejected BY the proven
binary, tampered attestations rejected, and the policy failing closed
when the binary is absent. 49/49 tests green (incl. PEM-SPKI raw-key
cross-check against openssl, dispatch/backend recording with a stub,
and a real-binary roundtrip that skips gracefully where unbuilt).
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
A transparency log without split-view defense is just a signature with
extra steps: the provider could serve one tree to the agent and another
to the world, or roll the log back, and standalone receipt verification
would never notice. The primitives (RFC 9162 consistency proofs) were
already implemented and correct; this closes the loop on the AGENT side.
- src/pacta/sthstore.py: a local STH pin store. Unknown log -> pin
(trust-on-first-use, recorded as such). Same tree size -> the root
must match the pin byte-for-byte; a mismatch is named EQUIVOCATION
and is a hard rejection. Larger tree -> a consistency proof FROM THE
PINNED SIZE is required and verified before the pin advances
(receipts already embed a from-previous anchor; the anchor's root is
itself checked against the pin so a lying anchor cannot bridge a
split view). Smaller tree -> LOG ROLLBACK, hard rejection.
- Freshness policy: --max-sth-age-seconds rejects stale (or
future-dated) tree heads - an old-but-valid STH can hide later
entries.
- Wired into receipt-verify, claims, and agent (--sth-store,
--consistency-proof, --max-sth-age-seconds); evidence records the
pin action; any accountability failure fails the receipt closed.
- Provider: log-consistency --from-size N (serve proofs for pinning
agents whose pin is older than the receipt's embedded anchor) and
log-audit (monitor self-check: recompute the tree, verify the stored
STH and per-entry leaf hashes).
Live drill in this commit's validation: pin-on-first-use -> matched ->
grown-with-proof advance -> a real forged same-size split view REJECTED
with the equivocation diagnostic -> freshness rejection -> clean
self-audit. tests/test_sthstore.py covers pin/match/equivocation,
growth-without-proof, lying consistency anchors, rollback, freshness.
45/45 tests green.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The verified corpus completed its phase 2 on 2026-07-06: every ed25519
fork now carries FOUR button-enforced apex tiers up to the full lift
(accept <=> decompress(R) = [k](-A)+[s]B as points), the complete scalar
layer, and the constructive encoding/decoding chain. pacta was calibrated
to the pre-apex corpus and - worse - had no vocabulary for
boundary-audited certificates: its axiom audit knew only "clean = exactly
the three standard axioms", so the apex tiers would have scored dirty.
New vocabulary:
- Profile.certificate_axioms: per-certificate ALLOWED axiom sets;
expected_axioms_for(cert) resolves each certificate's own boundary.
- RepoConfig.apex_boundary: a simple per-fork key (dalek-wrappers /
hash3 / anza) expanded by the ed25519 profile into the exact
per-tier allowed sets. AUTHORITY NOTE in profiles/ed25519.py: each
repo's check.sh Phase 3b is the enforcement point; if the button and
this table disagree, the button wins.
- run_axiom_audit compares each certificate against ITS allowed set;
deviation in EITHER direction (extra axiom or missing boundary
axiom) is dirty.
New risk reality:
- R4 is now reachable: full four-tier apex + constructive chain +
scalar arithmetic, all proven with cones pinned to their documented
boundaries. R4 always carries explicit residual blockers (SHA-512
oracle, hypothesis-parametric wire parses, translation faithfulness,
no side-channel/build assurance - those gate R5).
- R3 unchanged (arithmetic pair) and now explains exactly which apex
certificates are missing for R4.
Attestation trust model hardened:
- The provider is trusted for its OBSERVATION, never its VERDICT:
axiom_status is re-derived locally from observed_axioms against the
agent's own boundary policy. A provider that labels a dirty cone
"clean" gains nothing; "proven" with no observed axioms is
"unverifiable".
- Partial attestations degrade instead of being rejected: uncovered
certificates stay unproven and the score caps accordingly (an
arithmetic-only attestation still authorizes an R3 library capsule,
never a wallet).
Also: scripts/mini_pytest.py - a dependency-free test runner (tmp_path,
raises, monkeypatch, capsys) for hosts without pytest; examples
regenerated FROM the tool (dalek/anza fixtures now R4, 16 certs; new
full four-tier attestation example); tests updated + new
tests/test_boundaries.py (lying-provider, missing-boundary-axiom,
partial-coverage cases). 40/40 tests green.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
