mrwulf
caa864a749
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> |
||
|---|---|---|
| .. | ||
| 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.