mirror of
https://github.com/saymrwulf/proof-aware-crypto-tooling-agent.git
synced 2026-09-03 19:53:43 +00:00
mrwulf
3a7a56c4e5
First slh_dsa-kind repo. The 11 certificate names and every per-certificate cone are GENERATED from the repositorys own pinned AUDIT-MANIFEST.txt, not hand-typed; the apex resolves to kernel-3 plus the five verify-path oracles. Exclusions carry TRUSTED-BASE items 2/9/10 into the leaf: hash oracles assumed, signing/keygen out of scope, everything above the extraction root (including the pure/prehash domain-separator byte) uncovered, the deployed bridge a 137-case differential test. Dry-run green: 11/11 proven+clean at d44b70d8, attestation signed verified-dalek-serial. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
276 lines
13 KiB
YAML
276 lines
13 KiB
YAML
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
|
|
|
|
- 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
|
|
|
|
- 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
|
|
|
|
- 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
|
|
|
|
- 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"]
|