mrwulf
fbe40c3dfe
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> |
||
|---|---|---|
| .. | ||
| src/pacta_provider | ||
| pyproject.toml | ||
| README.md | ||
PACTA Proof Check Provider
This nested project is a prototype third-party proof-checking service. It reuses host Lean/Aeneas infrastructure, runs portable PACTA replay/audit checks, and emits signed attestation certificates.
It does not modify anything outside this repository. It may read configured toolchains such as /Users/oho/GitClone/ClaudeCodeProjects/your-lean-project/aeneas-toolchain/env.sh.
It can also maintain a local transparency log. The log is an RFC 9162-style Merkle accumulator over signed attestations. It emits Signed Tree Heads with Ed25519 today and records an ML-DSA/FIPS 204 signature slot as unavailable unless a real backend is present. Agents that require both signatures must reject such receipts.
Commands
PYTHONPATH=src:provider/src python -m pacta_provider discover
PYTHONPATH=src:provider/src python -m pacta_provider init-key --key-dir provider/state/demo-provider
PYTHONPATH=src:provider/src python -m pacta_provider check \
--config examples/repos.yaml \
--repo-name dalek-ed25519-verified \
--repo repos/dalek-ed25519-verified \
--provider local-pacta-provider \
--private-key provider/state/demo-provider/provider.ed25519.key \
--public-key provider/state/demo-provider/provider.ed25519.pub \
--out provider/out/dalek.attestation.yaml
Transparency log:
PYTHONPATH=src:provider/src python -m pacta_provider log-init \
--log-dir provider/state/transparency-log \
--provider local-pacta-provider \
--public-key provider/state/demo-provider/provider.ed25519.pub
PYTHONPATH=src:provider/src python -m pacta_provider log-append \
--log-dir provider/state/transparency-log \
--attestation provider/out/dalek.attestation.yaml \
--private-key provider/state/demo-provider/provider.ed25519.key \
--public-key provider/state/demo-provider/provider.ed25519.pub \
--out provider/out/dalek.receipt.yaml
PYTHONPATH=src:provider/src python -m pacta_provider log-sth \
--log-dir provider/state/transparency-log \
--private-key provider/state/demo-provider/provider.ed25519.key \
--public-key provider/state/demo-provider/provider.ed25519.pub
The resulting certificate can be consumed by pacta with --attestation, --trust-attestation-provider, and --attestation-public-key.
The receipt can be consumed with --transparency-receipt, --transparency-log-public-key, and --require-transparency-receipt.
The private key must remain provider-side. Downstream agents only need the public key, the inclusion receipt, and a policy decision that the provider name/log key is trusted.