Estate sync: boundary-axiom vocabulary + the four-tier apex reality (R4)
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>
2026-07-06 08:04:43 +00:00
|
|
|
component: pasta-pallas-verified
|
|
|
|
|
repo_url: https://github.com/saymrwulf/pasta-pallas-verified.git
|
|
|
|
|
local_path: repos/pasta-pallas-verified
|
|
|
|
|
repo_commit: null
|
|
|
|
|
verification_dir: verification
|
|
|
|
|
kind: pasta_pallas
|
|
|
|
|
verified_backend: null
|
|
|
|
|
certificates: []
|
|
|
|
|
guarantees:
|
|
|
|
|
- No configured certificate was replayed and axiom-clean in this run.
|
|
|
|
|
preconditions:
|
|
|
|
|
- Require explicit add, mul, reduce, square, and invert proof coverage before production
|
|
|
|
|
field claims.
|
|
|
|
|
- Require an aggregate fieldImplementation-style theorem before classifying the field
|
|
|
|
|
implementation as complete.
|
|
|
|
|
exclusions:
|
|
|
|
|
- Production-ready Pallas arithmetic is not assumed unless shipped certificates prove
|
|
|
|
|
it.
|
|
|
|
|
- Full protocol, wallet, proof-system, or transaction safety is out of scope.
|
|
|
|
|
- Compiler correctness, translation faithfulness, and side-channel resistance are
|
|
|
|
|
out of scope.
|
|
|
|
|
- full fieldImplementation certificate unless present and axiom-clean
|
|
|
|
|
- production-ready Pallas arithmetic unless add/mul/reduce/square/invert are proven
|
|
|
|
|
trusted_base:
|
|
|
|
|
- Lean kernel and standard library axioms.
|
|
|
|
|
- Correctness of the shipped translation artifact.
|
|
|
|
|
- Correct mapping from production code to checked routines.
|
|
|
|
|
evidence:
|
|
|
|
|
lean_version: Lean (version 4.30.0-rc2, x86_64-unknown-linux-gnu, commit 3dc1a088b6d2d8eafe25a7cd7ec7b58d731bd7cc,
|
|
|
|
|
Release)
|
|
|
|
|
lake_version: Lake version 5.0.0-src+3dc1a08 (Lean version 4.30.0-rc2)
|
|
|
|
|
check_log_path: null
|
|
|
|
|
axiom_log_path: null
|
|
|
|
|
replay_blockers: []
|
|
|
|
|
scanned_files: []
|
|
|
|
|
evidence_mode: local_or_fixture
|
|
|
|
|
risk:
|
|
|
|
|
level: R2
|
|
|
|
|
rationale: Pallas/Pasta foundation profile exists, but no aggregate production field
|
|
|
|
|
certificate was configured.
|
|
|
|
|
blockers:
|
|
|
|
|
- No configured aggregate certificate.
|
|
|
|
|
deployment_constraints:
|
|
|
|
|
- Do not classify as a complete production field implementation without aggregate
|
|
|
|
|
field coverage.
|
|
|
|
|
- Keep downstream protocol use behind independent tests and audits.
|
|
|
|
|
- foundation only unless aggregate field certificate is present
|
|
|
|
|
meta:
|
|
|
|
|
profile_axiom_imports:
|
|
|
|
|
- Proofs.FieldMain
|
|
|
|
|
r4_requirements: []
|
|
|
|
|
what_would_invalidate_this_evidence:
|
|
|
|
|
- Expected operation certificates are absent or fail replay.
|
|
|
|
|
- Unexpected axioms appear in certificate audits.
|
|
|
|
|
- Production code uses routines not covered by the shipped proof artifact.
|
|
|
|
|
next_proof_milestones:
|
|
|
|
|
- Prove add, mul, reduce, square, and invert.
|
|
|
|
|
- Add an aggregate fieldImplementation-style theorem.
|
|
|
|
|
- Map the checked theorem boundary to public production APIs.
|