2026-07-03 08:51:03 +00:00
repos :
- name : dalek-ed25519-verified
url : https://github.com/saymrwulf/dalek-ed25519-verified.git
kind : ed25519
verification_dir : verification
verified_backend : serial/u64
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
apex_boundary : dalek-wrappers
2026-07-03 09:24:13 +00:00
env_script : ~/aeneas-toolchain/env.sh
lean_project_dir : $AENEAS_HOME/backends/lean
2026-07-06 08:42:59 +00:00
lean_guard : verification/lean-guard
2026-07-03 08:51:03 +00:00
known_exclusions :
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
- SHA-512 implementation (opaque oracle in the apex theorems)
- wire parser/filter byte-level specs (hypothesis-parametric)
- signing-side correctness
2026-07-03 08:51:03 +00:00
- side-channel resistance
- compiler correctness
- SIMD/AVX/accelerator paths
2026-08-07 08:24:35 +00:00
# certificates + imports MEASURED from the two buttons (CERTS arrays;
# apex recovered the way Phase 3c itself recovers it). replay_exclude:
# the button-owned audit instruments the replay does not compile —
# disclosed per-leaf in replay.instruments_excluded.
certificates :
- CurveFieldProofs.fieldImplementation
- CurveFieldProofs.edwardsImplementation
- CurveFieldProofs.naf_table_spec
- CurveFieldProofs.naf_select_spec
- CurveFieldProofs.proj_double_law
- CurveFieldProofs.compl_as_projective_law
- CurveFieldProofs.dsm_step_p_law
- CurveFieldProofs.dsm_step_b_law
- CurveFieldProofs.dsm_loop_spec
- CurveFieldProofs.naf_load_spec
- CurveFieldProofs.naf_exit
- CurveFieldProofs.naf_digit_loop_spec
- CurveFieldProofs.non_adjacent_form_spec
- CurveFieldProofs.run_basepoint
- CurveFieldProofs.vartime_double_base_mul_spec
- CurveFieldProofs.verify_loop_full
- CurveFieldProofs.to_bytes_spec
- CurveFieldProofs.ed_compress_spec
- ScalarProofs.from_bytes_mod_order_wide_spec
- CurveFieldProofs.vartime_dsm_basepoint_spec
- CurveFieldProofs.enc_point_inj
- CurveFieldProofs.pow_p58_spec
- CurveFieldProofs.fe_ct_eq_spec
- CurveFieldProofs.sqrt_core
- CurveFieldProofs.sqrt_ratio_i_sq_spec
- CurveFieldProofs.from_bytes_spec
- CurveFieldProofs.decompress_of_canonical
- CurveFieldProofs.verify_accepts_iff
- CurveFieldProofs.verify_accepts_iff_decompress
- CurveFieldProofs.verify_accepts_iff_point
- CurveFieldProofs.verify_accepts_iff_point_eq
- ScalarProofs.L_val
- ScalarProofs.sub_loop_spec
- ScalarProofs.cond_add_l_one_spec
- ScalarProofs.sub_val_spec
- ScalarProofs.add_val_spec
- ScalarProofs.mul_internal_spec
- ScalarProofs.part1_spec
- ScalarProofs.montgomery_reduce_spec
- ScalarProofs.mul_spec
- ScalarProofs.scalarImplementation
- ScalarProofs.montgomery_mul_spec
- ScalarProofs.bytes_unpack_spec
- ScalarProofs.from_bytes_wide_spec
axiom_imports :
- Proofs.FieldMain
- Proofs.EdMain
- Proofs.ScalarMain
- Proofs.ToBytesSpec
- Proofs.CompressSpec
- Proofs.ScalarPackSpec
- Proofs.DsmMulSpec
- Proofs.SigApexSpec
- Proofs.PointLiftSpec
- Proofs.PointEqSpec
- Proofs.DecompressSpec
- Proofs.FromBytesSpec
- Proofs.DecompressMain
- Proofs.ScalarDenote
- Proofs.ScalarLoop
- Proofs.ScalarSubSpec
- Proofs.ScalarAddSpec
- Proofs.ScalarMulSpec
- Proofs.ScalarMontSpec
- Proofs.ScalarReduceSpec
- Proofs.ScalarFullMulSpec
- Proofs.ScalarWideSpec
- Proofs.ScalarBytesSpec
- Proofs.ScalarUnpackSpec
- Proofs.ScalarFromBytesSpec
replay_exclude :
- "Proofs/Audit.lean"
- "Proofs/ScalarAudit.lean"
- "Proofs/AxiomCheck.lean"
- "Proofs/Inventory*.lean"
2026-07-03 08:51:03 +00:00
- name : anza-ed25519-verified
url : https://github.com/saymrwulf/anza-ed25519-verified.git
kind : ed25519
verification_dir : verification
verified_backend : serial/u64
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
apex_boundary : anza
2026-07-03 09:24:13 +00:00
env_script : ~/aeneas-toolchain/env.sh
lean_project_dir : $AENEAS_HOME/backends/lean
2026-07-06 08:42:59 +00:00
lean_guard : verification/lean-guard
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
backend_warning : verified entry point is verify_sha512 = verify_dalek (canonical-R incl. legacy filters); the crate's default HEEA/Zebra verify() is a DIFFERENT acceptance criterion and is not covered
2026-07-03 08:51:03 +00:00
known_exclusions :
- Solana runtime semantics
- Solana transaction construction
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
- the default HEEA/Zebra verify() path
2026-07-03 08:51:03 +00:00
- accelerator paths
2026-08-07 08:24:35 +00:00
# certificates + imports MEASURED from the two buttons (CERTS arrays;
# apex recovered the way Phase 3c itself recovers it). replay_exclude:
# the button-owned audit instruments the replay does not compile —
# disclosed per-leaf in replay.instruments_excluded.
certificates :
- CurveFieldProofs.fieldImplementation
- CurveFieldProofs.edwardsImplementation
- CurveFieldProofs.naf_table_spec
- CurveFieldProofs.naf_select_spec
- CurveFieldProofs.proj_double_law
- CurveFieldProofs.compl_as_projective_law
- CurveFieldProofs.dsm_step_p_law
- CurveFieldProofs.dsm_step_b_law
- CurveFieldProofs.dsm_loop_spec
- CurveFieldProofs.naf_load_spec
- CurveFieldProofs.naf_exit
- CurveFieldProofs.naf_digit_loop_spec
- CurveFieldProofs.non_adjacent_form_spec
- CurveFieldProofs.run_basepoint
- CurveFieldProofs.vartime_double_base_mul_spec
- CurveFieldProofs.verify_loop_full
- CurveFieldProofs.to_bytes_spec
- CurveFieldProofs.ed_compress_spec
- ScalarProofs.from_bytes_mod_order_wide_spec
- CurveFieldProofs.vartime_dsm_basepoint_spec
- CurveFieldProofs.enc_point_inj
- CurveFieldProofs.pow_p58_spec
- CurveFieldProofs.fe_ct_eq_spec
- CurveFieldProofs.sqrt_core
- CurveFieldProofs.sqrt_ratio_i_sq_spec
- CurveFieldProofs.from_bytes_spec
- CurveFieldProofs.decompress_of_canonical
- CurveFieldProofs.verify_accepts_iff
- CurveFieldProofs.verify_accepts_iff_decompress
- CurveFieldProofs.verify_accepts_iff_point
- CurveFieldProofs.verify_accepts_iff_point_eq
- ScalarProofs.L_val
- ScalarProofs.sub_loop_spec
- ScalarProofs.cond_add_l_one_spec
- ScalarProofs.sub_val_spec
- ScalarProofs.add_val_spec
- ScalarProofs.mul_internal_spec
- ScalarProofs.part1_spec
- ScalarProofs.montgomery_reduce_spec
- ScalarProofs.mul_spec
- ScalarProofs.scalarImplementation
- ScalarProofs.montgomery_mul_spec
- ScalarProofs.bytes_unpack_spec
- ScalarProofs.from_bytes_wide_spec
axiom_imports :
- Proofs.FieldMain
- Proofs.EdMain
- Proofs.ScalarMain
- Proofs.ToBytesSpec
- Proofs.CompressSpec
- Proofs.ScalarPackSpec
- Proofs.DsmMulSpec
- Proofs.SigApexSpec
- Proofs.PointLiftSpec
- Proofs.PointEqSpec
- Proofs.DecompressSpec
- Proofs.FromBytesSpec
- Proofs.DecompressMain
- Proofs.ScalarDenote
- Proofs.ScalarLoop
- Proofs.ScalarSubSpec
- Proofs.ScalarAddSpec
- Proofs.ScalarMulSpec
- Proofs.ScalarMontSpec
- Proofs.ScalarReduceSpec
- Proofs.ScalarFullMulSpec
- Proofs.ScalarWideSpec
- Proofs.ScalarBytesSpec
- Proofs.ScalarUnpackSpec
- Proofs.ScalarFromBytesSpec
replay_exclude :
- "Proofs/Audit.lean"
- "Proofs/ScalarAudit.lean"
- "Proofs/AxiomCheck.lean"
- "Proofs/Inventory*.lean"
2026-07-03 08:51:03 +00:00
- name : risc0-ed25519-verified
url : https://github.com/saymrwulf/risc0-ed25519-verified.git
kind : ed25519
verification_dir : verification
verified_backend : serial/u64
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
apex_boundary : hash3
2026-07-03 09:24:13 +00:00
env_script : ~/aeneas-toolchain/env.sh
lean_project_dir : $AENEAS_HOME/backends/lean
2026-07-06 08:42:59 +00:00
lean_guard : verification/lean-guard
2026-07-03 08:51:03 +00:00
backend_warning : pure Rust path only; do not treat zkVM accelerator/syscall path as verified
2026-08-07 08:24:35 +00:00
# certificates + imports MEASURED from the two buttons (CERTS arrays;
# apex recovered the way Phase 3c itself recovers it). replay_exclude:
# the button-owned audit instruments the replay does not compile —
# disclosed per-leaf in replay.instruments_excluded.
certificates :
- CurveFieldProofs.fieldImplementation
- CurveFieldProofs.edwardsImplementation
- CurveFieldProofs.naf_table_spec
- CurveFieldProofs.naf_select_spec
- CurveFieldProofs.proj_double_law
- CurveFieldProofs.compl_as_projective_law
- CurveFieldProofs.dsm_step_p_law
- CurveFieldProofs.dsm_step_b_law
- CurveFieldProofs.dsm_loop_spec
- CurveFieldProofs.naf_load_spec
- CurveFieldProofs.naf_exit
- CurveFieldProofs.naf_digit_loop_spec
- CurveFieldProofs.non_adjacent_form_spec
- CurveFieldProofs.run_basepoint
- CurveFieldProofs.vartime_double_base_mul_spec
- CurveFieldProofs.verify_loop_full
- CurveFieldProofs.to_bytes_spec
- CurveFieldProofs.ed_compress_spec
- ScalarProofs.from_bytes_mod_order_wide_spec
- CurveFieldProofs.vartime_dsm_basepoint_spec
- CurveFieldProofs.enc_point_inj
- CurveFieldProofs.pow_p58_spec
- CurveFieldProofs.fe_ct_eq_spec
- CurveFieldProofs.sqrt_core
- CurveFieldProofs.sqrt_ratio_i_sq_spec
- CurveFieldProofs.from_bytes_spec
- CurveFieldProofs.decompress_of_canonical
- CurveFieldProofs.verify_accepts_iff
- CurveFieldProofs.verify_accepts_iff_decompress
- CurveFieldProofs.verify_accepts_iff_point
- CurveFieldProofs.verify_accepts_iff_point_eq
- ScalarProofs.L_val
- ScalarProofs.sub_loop_spec
- ScalarProofs.sub_loop1_one_spec
- ScalarProofs.sub_val_spec
- ScalarProofs.add_val_spec
- ScalarProofs.mul_internal_spec
- ScalarProofs.part1_spec
- ScalarProofs.montgomery_reduce_spec
- ScalarProofs.mul_spec
- ScalarProofs.scalarImplementation
- ScalarProofs.montgomery_mul_spec
- ScalarProofs.bytes_unpack_spec
- ScalarProofs.from_bytes_wide_spec
axiom_imports :
- Proofs.FieldMain
- Proofs.EdMain
- Proofs.ScalarMain
- Proofs.ToBytesSpec
- Proofs.CompressSpec
- Proofs.ScalarPackSpec
- Proofs.DsmMulSpec
- Proofs.SigApexSpec
- Proofs.PointLiftSpec
- Proofs.PointEqSpec
- Proofs.DecompressSpec
- Proofs.FromBytesSpec
- Proofs.DecompressMain
- Proofs.ScalarDenote
- Proofs.ScalarLoop
- Proofs.ScalarSubSpec
- Proofs.ScalarAddSpec
- Proofs.ScalarMulSpec
- Proofs.ScalarMontSpec
- Proofs.ScalarReduceSpec
- Proofs.ScalarFullMulSpec
- Proofs.ScalarWideSpec
- Proofs.ScalarBytesSpec
- Proofs.ScalarUnpackSpec
- Proofs.ScalarFromBytesSpec
replay_exclude :
- "Proofs/Audit.lean"
- "Proofs/ScalarAudit.lean"
- "Proofs/AxiomCheck.lean"
- "Proofs/Inventory*.lean"
2026-07-03 08:51:03 +00:00
- name : betrusted-ed25519-verified
url : https://github.com/saymrwulf/betrusted-ed25519-verified.git
kind : ed25519
verification_dir : verification
verified_backend : serial/u64
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
apex_boundary : hash3
2026-07-03 09:24:13 +00:00
env_script : ~/aeneas-toolchain/env.sh
lean_project_dir : $AENEAS_HOME/backends/lean
2026-07-06 08:42:59 +00:00
lean_guard : verification/lean-guard
2026-07-03 08:51:03 +00:00
backend_warning : pure Rust path only; do not treat Engine25519/hardware accelerator as verified
2026-08-07 08:24:35 +00:00
# certificates + imports MEASURED from the two buttons (CERTS arrays;
# apex recovered the way Phase 3c itself recovers it). replay_exclude:
# the button-owned audit instruments the replay does not compile —
# disclosed per-leaf in replay.instruments_excluded.
certificates :
- CurveFieldProofs.fieldImplementation
- CurveFieldProofs.edwardsImplementation
- CurveFieldProofs.naf_table_spec
- CurveFieldProofs.naf_select_spec
- CurveFieldProofs.proj_double_law
- CurveFieldProofs.compl_as_projective_law
- CurveFieldProofs.dsm_step_p_law
- CurveFieldProofs.dsm_step_b_law
- CurveFieldProofs.dsm_loop_spec
- CurveFieldProofs.naf_load_spec
- CurveFieldProofs.naf_exit
- CurveFieldProofs.naf_digit_loop_spec
- CurveFieldProofs.non_adjacent_form_spec
- CurveFieldProofs.run_basepoint
- CurveFieldProofs.vartime_double_base_mul_spec
- CurveFieldProofs.verify_loop_full
- CurveFieldProofs.to_bytes_spec
- CurveFieldProofs.ed_compress_spec
- ScalarProofs.from_bytes_mod_order_wide_spec
- CurveFieldProofs.vartime_dsm_basepoint_spec
- CurveFieldProofs.enc_point_inj
- CurveFieldProofs.pow_p58_spec
- CurveFieldProofs.fe_ct_eq_spec
- CurveFieldProofs.sqrt_core
- CurveFieldProofs.sqrt_ratio_i_sq_spec
- CurveFieldProofs.from_bytes_spec
- CurveFieldProofs.decompress_of_canonical
- CurveFieldProofs.verify_accepts_iff
- CurveFieldProofs.verify_accepts_iff_decompress
- CurveFieldProofs.verify_accepts_iff_point
- CurveFieldProofs.verify_accepts_iff_point_eq
- ScalarProofs.L_val
- ScalarProofs.sub_loop_spec
- ScalarProofs.sub_loop1_one_spec
- ScalarProofs.sub_val_spec
- ScalarProofs.add_val_spec
- ScalarProofs.mul_internal_spec
- ScalarProofs.part1_spec
- ScalarProofs.montgomery_reduce_spec
- ScalarProofs.mul_spec
- ScalarProofs.scalarImplementation
- ScalarProofs.montgomery_mul_spec
- ScalarProofs.bytes_unpack_spec
- ScalarProofs.from_bytes_wide_spec
axiom_imports :
- Proofs.FieldMain
- Proofs.EdMain
- Proofs.ScalarMain
- Proofs.ToBytesSpec
- Proofs.CompressSpec
- Proofs.ScalarPackSpec
- Proofs.DsmMulSpec
- Proofs.SigApexSpec
- Proofs.PointLiftSpec
- Proofs.PointEqSpec
- Proofs.DecompressSpec
- Proofs.FromBytesSpec
- Proofs.DecompressMain
- Proofs.ScalarDenote
- Proofs.ScalarLoop
- Proofs.ScalarSubSpec
- Proofs.ScalarAddSpec
- Proofs.ScalarMulSpec
- Proofs.ScalarMontSpec
- Proofs.ScalarReduceSpec
- Proofs.ScalarFullMulSpec
- Proofs.ScalarWideSpec
- Proofs.ScalarBytesSpec
- Proofs.ScalarUnpackSpec
- Proofs.ScalarFromBytesSpec
replay_exclude :
- "Proofs/Audit.lean"
- "Proofs/ScalarAudit.lean"
- "Proofs/AxiomCheck.lean"
- "Proofs/Inventory*.lean"
2026-07-03 08:51:03 +00:00
- name : pasta-pallas-verified
url : https://github.com/saymrwulf/pasta-pallas-verified.git
kind : pasta_pallas
verification_dir : verification
2026-07-03 09:24:13 +00:00
env_script : ~/aeneas-toolchain/env.sh
lean_project_dir : $AENEAS_HOME/backends/lean
2026-07-06 08:42:59 +00:00
lean_guard : verification/lean-guard
2026-07-03 08:51:03 +00:00
known_status : foundation only unless aggregate field certificate is present
known_exclusions :
- full fieldImplementation certificate unless present and axiom-clean
- production-ready Pallas arithmetic unless add/mul/reduce/square/invert are proven
2026-07-16 09:08:01 +00:00
- name : ltl-accumulator-verified
url : https://github.com/saymrwulf/ltl-accumulator-verified.git
kind : merkle_accumulator
verification_dir : verification
verified_backend : rfc9162-sha256/lean-model
env_script : ~/aeneas-toolchain/env.sh
lean_project_dir : $AENEAS_HOME/backends/lean
lean_guard : verification/lean-guard
known_status : >-
Attestation scope : this corpus kernel-checks the listed theorems about
the mechanized recursive accumulator model. Correspondence with the
deployed inclusion verifier is supported by finite differential testing
over the pinned families. The deployed consistency verifier is not
extensionally equal to the model; applying the mechanized soundness
result to the deployed consumer flow additionally relies on an
unmechanized authentic-size/root invariant (KNOWN-GAPS 14/15).
known_exclusions :
- SHA-256 collision resistance (the single opaque boundary axiom; soundness theorems CONSTRUCT collisions)
- deployed-verifier extensional equality (KNOWN-GAPS 14/15 - lied-size divergence, one-sided; refinement invariant unmechanized)
- signature/STH layer and evidence transferability (gap 4)
- asymptotic cost claims (gap 9)
axiom_imports :
- Proofs.Basic
- Proofs.Completeness
- Proofs.Extract
- Proofs.Descent
- Proofs.Consistency
- Proofs.Binding3
- Proofs.Refactor
- Proofs.Theorem3
- Proofs.PinStore
certificates :
- LTLAcc.ConsRec
- LTLAcc.Hash
- LTLAcc.IsCollision
- LTLAcc.MTH
- LTLAcc.MTH_single
- LTLAcc.MTH_split
- LTLAcc.Path
- LTLAcc.Root
- LTLAcc.Root_left
- LTLAcc.Root_one
- LTLAcc.Root_one_cons
- LTLAcc.Root_right
- LTLAcc.acceptCons
- LTLAcc.acceptCons_sound
- LTLAcc.acceptIncl
- LTLAcc.acceptIncl_complete
- LTLAcc.acceptIncl_sound
- LTLAcc.consRecBinding
- LTLAcc.consRec_base_false_eq
- LTLAcc.consRec_base_true_eq
- LTLAcc.consRec_some_le
- LTLAcc.domsep
- LTLAcc.eq_dropLast_append_of_getLast?
- LTLAcc.exists_singleton_of_length_one
- LTLAcc.extractCons
- LTLAcc.extractConsNode
- LTLAcc.extractCons_correct
- LTLAcc.extractCons_correct_paper
- LTLAcc.extractCons_nonvacuous
- LTLAcc.extractIncl
- LTLAcc.extractIncl_correct
- LTLAcc.extractIncl_nonvacuous
- LTLAcc.extractMTH
- LTLAcc.extractMTH_correct
- LTLAcc.extractMTH_nonvacuous
- LTLAcc.fork_distinct
- LTLAcc.getD_drop
- LTLAcc.getD_take
- LTLAcc.hleaf
- LTLAcc.hnode
- LTLAcc.hnode_preimage_inj
- LTLAcc.incl_complete
- LTLAcc.instDecidableEqHash
- LTLAcc.instInhabitedHash
- LTLAcc.kbelow
- LTLAcc.kbelow_eq_of_pow2_between
- LTLAcc.kbelow_lt
- LTLAcc.kbelow_pos
- LTLAcc.kbelow_pow2
- LTLAcc.kbelow_prefix_eq
- LTLAcc.le_two_kbelow
- LTLAcc.pinAccept
- LTLAcc.pinAccept_monotone
- LTLAcc.pinExtract
- LTLAcc.pin_prefix_correct
- LTLAcc.pin_prefix_nonvacuous
- LTLAcc.pow2_exp_unique
- LTLAcc.take_all
- LTLAcc.take_append_drop
- LTLAcc.take_drop_prefix
- LTLAcc.take_take_le
certificate_axioms :
LTLAcc.ConsRec : [ "propext" , "LTLAcc.sha256" , "Quot.sound" ]
LTLAcc.Hash : [ ]
LTLAcc.IsCollision : [ "LTLAcc.sha256" ]
LTLAcc.MTH : [ "propext" , "LTLAcc.sha256" , "Quot.sound" ]
LTLAcc.MTH_single : [ "propext" , "LTLAcc.sha256" , "Quot.sound" ]
LTLAcc.MTH_split : [ "propext" , "LTLAcc.sha256" , "Quot.sound" ]
LTLAcc.Path : [ "propext" , "LTLAcc.sha256" , "Quot.sound" ]
LTLAcc.Root : [ "propext" , "LTLAcc.sha256" , "Quot.sound" ]
LTLAcc.Root_left : [ "propext" , "LTLAcc.sha256" , "Quot.sound" ]
LTLAcc.Root_one : [ "propext" , "LTLAcc.sha256" , "Quot.sound" ]
LTLAcc.Root_one_cons : [ "propext" , "LTLAcc.sha256" , "Quot.sound" ]
LTLAcc.Root_right : [ "propext" , "LTLAcc.sha256" , "Quot.sound" ]
LTLAcc.acceptCons : [ "propext" , "LTLAcc.sha256" , "Quot.sound" ]
LTLAcc.acceptCons_sound : [ "propext" , "Classical.choice" , "LTLAcc.sha256" , "Quot.sound" ]
LTLAcc.acceptIncl : [ "propext" , "LTLAcc.sha256" , "Quot.sound" ]
LTLAcc.acceptIncl_complete : [ "propext" , "Classical.choice" , "LTLAcc.sha256" , "Quot.sound" ]
LTLAcc.acceptIncl_sound : [ "propext" , "Classical.choice" , "LTLAcc.sha256" , "Quot.sound" ]
LTLAcc.consRecBinding : [ "propext" , "Classical.choice" , "LTLAcc.sha256" , "Quot.sound" ]
LTLAcc.consRec_base_false_eq : [ "propext" , "Classical.choice" , "Quot.sound" ]
LTLAcc.consRec_base_true_eq : [ "propext" ]
LTLAcc.consRec_some_le : [ "propext" , "LTLAcc.sha256" , "Quot.sound" ]
LTLAcc.domsep : [ ]
LTLAcc.eq_dropLast_append_of_getLast? : [ "propext" ]
LTLAcc.exists_singleton_of_length_one : [ "propext" , "Classical.choice" , "Quot.sound" ]
LTLAcc.extractCons : [ "propext" , "LTLAcc.sha256" , "Quot.sound" ]
LTLAcc.extractConsNode : [ "propext" , "LTLAcc.sha256" , "Quot.sound" ]
LTLAcc.extractCons_correct : [ "propext" , "Classical.choice" , "LTLAcc.sha256" , "Quot.sound" ]
LTLAcc.extractCons_correct_paper : [ "propext" , "Classical.choice" , "LTLAcc.sha256" , "Quot.sound" ]
LTLAcc.extractCons_nonvacuous : [ "propext" , "LTLAcc.sha256" , "Quot.sound" ]
LTLAcc.extractIncl : [ "propext" , "LTLAcc.sha256" , "Quot.sound" ]
LTLAcc.extractIncl_correct : [ "propext" , "Classical.choice" , "LTLAcc.sha256" , "Quot.sound" ]
LTLAcc.extractIncl_nonvacuous : [ "propext" , "LTLAcc.sha256" , "Quot.sound" ]
LTLAcc.extractMTH : [ "propext" , "LTLAcc.sha256" , "Quot.sound" ]
LTLAcc.extractMTH_correct : [ "propext" , "Classical.choice" , "LTLAcc.sha256" , "Quot.sound" ]
LTLAcc.extractMTH_nonvacuous : [ "propext" , "LTLAcc.sha256" , "Quot.sound" ]
LTLAcc.fork_distinct : [ "propext" , "LTLAcc.sha256" , "Quot.sound" ]
LTLAcc.getD_drop : [ "propext" , "Quot.sound" ]
LTLAcc.getD_take : [ "propext" , "Quot.sound" ]
LTLAcc.hleaf : [ "LTLAcc.sha256" ]
LTLAcc.hnode : [ "LTLAcc.sha256" ]
LTLAcc.hnode_preimage_inj : [ "propext" ]
LTLAcc.incl_complete : [ "propext" , "Classical.choice" , "LTLAcc.sha256" , "Quot.sound" ]
LTLAcc.instDecidableEqHash : [ ]
LTLAcc.instInhabitedHash : [ "propext" ]
LTLAcc.kbelow : [ "propext" , "Quot.sound" ]
LTLAcc.kbelow_eq_of_pow2_between : [ "propext" , "Quot.sound" ]
LTLAcc.kbelow_lt : [ "propext" , "Quot.sound" ]
LTLAcc.kbelow_pos : [ "propext" , "Quot.sound" ]
LTLAcc.kbelow_pow2 : [ "propext" , "Quot.sound" ]
LTLAcc.kbelow_prefix_eq : [ "propext" , "Quot.sound" ]
LTLAcc.le_two_kbelow : [ "propext" , "Quot.sound" ]
LTLAcc.pinAccept : [ "propext" , "LTLAcc.sha256" , "Quot.sound" ]
LTLAcc.pinAccept_monotone : [ "propext" , "LTLAcc.sha256" , "Quot.sound" ]
LTLAcc.pinExtract : [ "propext" , "LTLAcc.sha256" , "Quot.sound" ]
LTLAcc.pin_prefix_correct : [ "propext" , "Classical.choice" , "LTLAcc.sha256" , "Quot.sound" ]
LTLAcc.pin_prefix_nonvacuous : [ "propext" , "LTLAcc.sha256" , "Quot.sound" ]
LTLAcc.pow2_exp_unique : [ "propext" , "Quot.sound" ]
LTLAcc.take_all : [ "propext" ]
LTLAcc.take_append_drop : [ ]
LTLAcc.take_drop_prefix : [ "propext" , "Classical.choice" , "Quot.sound" ]
LTLAcc.take_take_le : [ "propext" , "Quot.sound" ]
2026-08-07 07:22:58 +00:00
- name : fips205-slhdsa-verified
url : https://github.com/saymrwulf/fips205-slhdsa-verified.git
kind : slh_dsa
verification_dir : verification
verified_backend : verify-mono/sha2-128s
env_script : ~/aeneas-toolchain/env.sh
lean_project_dir : $AENEAS_HOME/backends/lean
lean_guard : verification/lean-guard
backend_warning : >-
proved subject is the private verify_mono facade; the bridge to the
deployed generic pk.verify() is a 137-case differential test, not a
machine-checked refinement (TRUSTED-BASE item 9)
known_exclusions :
- the five verify-path hash oracles h_msg/f/h/t_l/t_len (assumed, not proven against FIPS 180-4)
- signing and key generation (out of extraction scope entirely)
- "everything above the extraction root: M' assembly, the pure/prehash domain-separator byte, ctx length bound, deserialization (TRUSTED-BASE item 10)"
- the base_2b inner loop (threaded opaquely, no certificate)
- parameter sets other than SLH-DSA-SHA2-128s
- compiler correctness and side channels
axiom_imports :
- Proofs.ApexSpec
- Proofs.ChainSpec
- Proofs.ForsInnerSpec
- Proofs.ForsOuterSpec
- Proofs.HtSpec
- Proofs.InputPrepSpec
- Proofs.WotsSpec
- Proofs.XmssSpec
certificates :
- fips205.base2b_outer_loop_eq
- fips205.chain_free_loop_eq
- fips205.fors_inner_loop_eq
- fips205.fors_outer_loop_eq
- fips205.ht_loop_eq
- fips205.slh_verify_128s_accepts_iff
- fips205.to_byte_loop_eq
- fips205.to_int_loop_eq
- fips205.wots_csum_loop_eq
- fips205.wots_loop1_eq
- fips205.xmss_loop_eq
certificate_axioms :
fips205.base2b_outer_loop_eq : [ "Classical.choice" , "Quot.sound" , "propext" ]
fips205.chain_free_loop_eq : [ "Classical.choice" , "Quot.sound" , "propext" , "verify_mono.oracle.f" ]
fips205.fors_inner_loop_eq : [ "Classical.choice" , "Quot.sound" , "propext" , "verify_mono.oracle.h" ]
fips205.fors_outer_loop_eq : [ "Classical.choice" , "Quot.sound" , "propext" , "verify_mono.oracle.f" , "verify_mono.oracle.h" ]
fips205.ht_loop_eq : [ "Classical.choice" , "Quot.sound" , "propext" , "verify_mono.oracle.f" , "verify_mono.oracle.h" , "verify_mono.oracle.t_l" ]
fips205.slh_verify_128s_accepts_iff : [ "Classical.choice" , "Quot.sound" , "propext" , "verify_mono.oracle.f" , "verify_mono.oracle.h" , "verify_mono.oracle.h_msg" , "verify_mono.oracle.t_l" , "verify_mono.oracle.t_len" ]
fips205.to_byte_loop_eq : [ "Classical.choice" , "Quot.sound" , "propext" ]
fips205.to_int_loop_eq : [ "Classical.choice" , "Quot.sound" , "propext" ]
fips205.wots_csum_loop_eq : [ "Classical.choice" , "Quot.sound" , "propext" ]
fips205.wots_loop1_eq : [ "Classical.choice" , "Quot.sound" , "propext" , "verify_mono.oracle.f" ]
fips205.xmss_loop_eq : [ "Classical.choice" , "Quot.sound" , "propext" , "verify_mono.oracle.h" ]
