saymrwulf/proof-aware-crypto-tooling-agent
1
0
Fork 0
mirror of https://github.com/saymrwulf/proof-aware-crypto-tooling-agent.git synced 2026-09-03 19:53:43 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions
proof-aware-crypto-tooling-.../examples/dalek-ed25519.full.attestation.yaml
mrwulf caa864a749 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 10:04:43 +02:00

258 lines
5.7 KiB
YAML
Raw Blame History

schema_version: 1
provider: example-proof-checker.invalid
issued_at: '2026-07-06T00:00:00Z'
subject:
component: dalek-ed25519-verified
repo_url: https://github.com/saymrwulf/dalek-ed25519-verified.git
repo_commit: example-attested-commit
verification_dir: verification
kind: ed25519
verified_backend: serial/u64
environment:
lean_version: Lean v4.30.0-rc2
lake_version: pinned provider environment
certificates:
- name: CurveFieldProofs.fieldImplementation
status: proven
axiom_status: clean
observed_axioms:
- propext
- Classical.choice
- Quot.sound
expected_axioms:
- propext
- Classical.choice
- Quot.sound
- name: CurveFieldProofs.edwardsImplementation
status: proven
axiom_status: clean
observed_axioms:
- propext
- Classical.choice
- Quot.sound
expected_axioms:
- propext
- Classical.choice
- Quot.sound
- name: ScalarProofs.scalarImplementation
status: proven
axiom_status: clean
observed_axioms:
- propext
- Classical.choice
- Quot.sound
expected_axioms:
- propext
- Classical.choice
- Quot.sound
- name: CurveFieldProofs.verify_loop_full
status: proven
axiom_status: clean
observed_axioms:
- propext
- Classical.choice
- Quot.sound
expected_axioms:
- propext
- Classical.choice
- Quot.sound
- name: CurveFieldProofs.to_bytes_spec
status: proven
axiom_status: clean
observed_axioms:
- propext
- Classical.choice
- Quot.sound
expected_axioms:
- propext
- Classical.choice
- Quot.sound
- name: CurveFieldProofs.ed_compress_spec
status: proven
axiom_status: clean
observed_axioms:
- propext
- Classical.choice
- Quot.sound
expected_axioms:
- propext
- Classical.choice
- Quot.sound
- name: ScalarProofs.from_bytes_mod_order_wide_spec
status: proven
axiom_status: clean
observed_axioms:
- propext
- Classical.choice
- Quot.sound
expected_axioms:
- propext
- Classical.choice
- Quot.sound
- name: CurveFieldProofs.vartime_dsm_basepoint_spec
status: proven
axiom_status: clean
observed_axioms:
- propext
- Classical.choice
- Quot.sound
expected_axioms:
- propext
- Classical.choice
- Quot.sound
- name: CurveFieldProofs.enc_point_inj
status: proven
axiom_status: clean
observed_axioms:
- propext
- Classical.choice
- Quot.sound
expected_axioms:
- propext
- Classical.choice
- Quot.sound
- name: CurveFieldProofs.sqrt_ratio_i_sq_spec
status: proven
axiom_status: clean
observed_axioms:
- propext
- Classical.choice
- Quot.sound
expected_axioms:
- propext
- Classical.choice
- Quot.sound
- name: CurveFieldProofs.from_bytes_spec
status: proven
axiom_status: clean
observed_axioms:
- propext
- Classical.choice
- Quot.sound
expected_axioms:
- propext
- Classical.choice
- Quot.sound
- name: CurveFieldProofs.decompress_of_canonical
status: proven
axiom_status: clean
observed_axioms:
- propext
- Classical.choice
- Quot.sound
expected_axioms:
- propext
- Classical.choice
- Quot.sound
- name: CurveFieldProofs.verify_accepts_iff
status: proven
axiom_status: clean
observed_axioms:
- propext
- Classical.choice
- Quot.sound
- ed25519.Signature
- sha2.Sha512
- verifying.sha512_new
- verifying.sha512_update
- verifying.sha512_finalize_bytes
- ed25519.Signature.to_bytes
- signature.error.Error
- signature.error.Error.new
expected_axioms:
- propext
- Classical.choice
- Quot.sound
- ed25519.Signature
- sha2.Sha512
- verifying.sha512_new
- verifying.sha512_update
- verifying.sha512_finalize_bytes
- ed25519.Signature.to_bytes
- signature.error.Error
- signature.error.Error.new
- name: CurveFieldProofs.verify_accepts_iff_point
status: proven
axiom_status: clean
observed_axioms:
- propext
- Classical.choice
- Quot.sound
- ed25519.Signature
- sha2.Sha512
- verifying.sha512_new
- verifying.sha512_update
- verifying.sha512_finalize_bytes
- ed25519.Signature.to_bytes
- signature.error.Error
- signature.error.Error.new
expected_axioms:
- propext
- Classical.choice
- Quot.sound
- ed25519.Signature
- sha2.Sha512
- verifying.sha512_new
- verifying.sha512_update
- verifying.sha512_finalize_bytes
- ed25519.Signature.to_bytes
- signature.error.Error
- signature.error.Error.new
- name: CurveFieldProofs.verify_accepts_iff_point_eq
status: proven
axiom_status: clean
observed_axioms:
- propext
- Classical.choice
- Quot.sound
- ed25519.Signature
- sha2.Sha512
- verifying.sha512_new
- verifying.sha512_update
- verifying.sha512_finalize_bytes
- ed25519.Signature.to_bytes
- signature.error.Error
- signature.error.Error.new
expected_axioms:
- propext
- Classical.choice
- Quot.sound
- ed25519.Signature
- sha2.Sha512
- verifying.sha512_new
- verifying.sha512_update
- verifying.sha512_finalize_bytes
- ed25519.Signature.to_bytes
- signature.error.Error
- signature.error.Error.new
- name: CurveFieldProofs.verify_accepts_iff_decompress
status: proven
axiom_status: clean
observed_axioms:
- propext
- Classical.choice
- Quot.sound
- ed25519.Signature
- sha2.Sha512
- verifying.sha512_new
- verifying.sha512_update
- verifying.sha512_finalize_bytes
- ed25519.Signature.to_bytes
- signature.error.Error
- signature.error.Error.new
expected_axioms:
- propext
- Classical.choice
- Quot.sound
- ed25519.Signature
- sha2.Sha512
- verifying.sha512_new
- verifying.sha512_update
- verifying.sha512_finalize_bytes
- ed25519.Signature.to_bytes
- signature.error.Error
- signature.error.Error.new
signature:
status: not_implemented
identity: example schema only; a real provider signs with its Ed25519 key
log_url: https://example.invalid/proof-checks/dalek-ed25519
Reference in a new issue View git blame Copy permalink