mrwulf
922e87b024
Round-14 verdicts: the Claude reviewer CONCEDED its round-13 FORK
objection in writing ('I WAS WRONG', with the correct reasoning after
attempting the demanded counterexample) and passed everything
('nothing blocks x3') — but its 'chi genuinely encoded in the payload'
certification silently swapped pk out of the tuple, missing exactly
GPT's blocker 1. GPT verified the transport induction branch-by-branch
(sound) and found three real integration blockers, all independently
confirmed here before fixing:
- B1: chi contained pk and was claimed payload-encoded; the deployed
payload does NOT carry the key (it is an external verification
parameter) and the game fixed chi before KeyGen created pk. Now:
chi_enc = (log id, schema/type tags, hash-alg) is the encoded
context; chi = (chi_enc, pk) is set after KeyGen; all game texts
(syntax, injectivity lemma, HEAD, FORK/Ev) rescoped accordingly.
- B2: context scoping propagated to the three sites still stating the
cross-log-flawed form: Definition 2 clause (iii), Proposition 1
(statement + proof), and the Appendix A fork row — plus clause (i)
redefined as opening uniqueness under an authentic view (the
'position-bound' ambiguity), the App-A membership row aligned, and a
NEW App-A row for full-mirror recomputation (verify.py --all).
- B3: the security corollary no longer treats the epistemic
human-ignorance premise as a contradictable assumption. It is now
'Constructive security consequence': explicit feasible winner =>
explicitly given, equally feasible collision finder (stated costs);
HEAD/FORK => one EUF-CMA forgery, no loss; the human-ignorance
reading is an engineering judgment stated as such. Intro sentence
aligned.
Minor round-14 items adopted: kbelow citation corrected to the exact
corpus theorem kbelow_prefix_eq (Consistency.lean:48 — it EXISTS;
GPT's claim that no literally-named lemma exists was wrong, my memory
was right); payload-injectivity proof covers the timestamp string and
is scoped to the specified serializer; HIST chain re-termed
'head values, Merkle-level, authentication is HEAD's job'; transcript-
length cost sentence in Theorem 5; 'strong induction' clause;
DGHS-adaptation positioning sentence ('not a bespoke bar' — worded
'adapt', per GPT round 13's own caution against 'specialization').
21 pages, 0 overfull, suite 115 green.
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.