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-04 20:03:40 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions
proof-aware-crypto-tooling-.../examples/repos.yaml
mrwulf ab629f34d8 replay: compile the certificate corpus, not the button's instruments; forks attest 44 
Closes the two halves of replay-pipeline-lags-hardened-forks.

(1) The generic replay compiled every .lean under verification/, including the
P1-b kernel-gate instruments (Proofs/Inventory*.lean) that read other modules'
object files via readModuleData and only run inside the button's environment;
it died with "object file does not exist". New RepoConfig.replay_exclude
(globs, per repo, in the config where a reviewer sees them) filters the
compile; every exclusion actually applied is recorded in the attestation's
replay.instruments_excluded, so the LEAF discloses what its replay did not
compile — a silent exclusion here would be the estate's oldest defect class.
The replay checks the certificates; the deeper self-auditing gates are the
repository's own and run there.

(2) The ed25519 profile's default list still carried the 16 pre-hardening
certificates, so a successful replay would have attested 16 and the whole
16->44 point of the re-attestation would have been lost silently. Each fork
entry now carries its own 44 — 27 main + 4 apex + 13 scalar — MEASURED from
the fork's two buttons (CERTS arrays; apex recovered by the same pattern
Phase 3c itself uses), never hand-typed. Correction to the plan on the way
through: the plan said 40; the apex tier makes it 44.

Suite: 152 passed, 0 failed, 0 skipped.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-08-07 10:24:35 +02:00

596 lines
25 KiB
YAML
Raw Blame History

repos:
- name: dalek-ed25519-verified
url: https://github.com/saymrwulf/dalek-ed25519-verified.git
kind: ed25519
verification_dir: verification
verified_backend: serial/u64
apex_boundary: dalek-wrappers
env_script: ~/aeneas-toolchain/env.sh
lean_project_dir: $AENEAS_HOME/backends/lean
lean_guard: verification/lean-guard
known_exclusions:
- SHA-512 implementation (opaque oracle in the apex theorems)
- wire parser/filter byte-level specs (hypothesis-parametric)
- signing-side correctness
- side-channel resistance
- compiler correctness
- SIMD/AVX/accelerator paths
# 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"
- name: anza-ed25519-verified
url: https://github.com/saymrwulf/anza-ed25519-verified.git
kind: ed25519
verification_dir: verification
verified_backend: serial/u64
apex_boundary: anza
env_script: ~/aeneas-toolchain/env.sh
lean_project_dir: $AENEAS_HOME/backends/lean
lean_guard: verification/lean-guard
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
known_exclusions:
- Solana runtime semantics
- Solana transaction construction
- the default HEEA/Zebra verify() path
- accelerator paths
# 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"
- name: risc0-ed25519-verified
url: https://github.com/saymrwulf/risc0-ed25519-verified.git
kind: ed25519
verification_dir: verification
verified_backend: serial/u64
apex_boundary: hash3
env_script: ~/aeneas-toolchain/env.sh
lean_project_dir: $AENEAS_HOME/backends/lean
lean_guard: verification/lean-guard
backend_warning: pure Rust path only; do not treat zkVM accelerator/syscall path as verified
# 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"
- name: betrusted-ed25519-verified
url: https://github.com/saymrwulf/betrusted-ed25519-verified.git
kind: ed25519
verification_dir: verification
verified_backend: serial/u64
apex_boundary: hash3
env_script: ~/aeneas-toolchain/env.sh
lean_project_dir: $AENEAS_HOME/backends/lean
lean_guard: verification/lean-guard
backend_warning: pure Rust path only; do not treat Engine25519/hardware accelerator as verified
# 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"
- name: pasta-pallas-verified
url: https://github.com/saymrwulf/pasta-pallas-verified.git
kind: pasta_pallas
verification_dir: verification
env_script: ~/aeneas-toolchain/env.sh
lean_project_dir: $AENEAS_HOME/backends/lean
lean_guard: verification/lean-guard
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
- 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"]
- 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"]
Reference in a new issue View git blame Copy permalink