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/repos.yaml
mrwulf 0f5906cf94 examples/repos.yaml: ltl-accumulator-verified entry (entry-13 attestation config) 
Rehearsed end-to-end 2026-07-16 (throwaway key + throwaway log):
compile via the corpus's lean-guard, 61/61 certificates proven with
byte-exact cones (post parser fix 34a0457), append, publish,
witness-audit ok. kind merkle_accumulator uses the generic profile —
everything comes from this entry: the 61 fully-qualified certificates
with per-certificate cones (generated from the corpus's CONES table),
the nine Proofs.* axiom_imports (required — without them the generated
audit file has no imports and lean-guard rejects it), and known_status
carrying the REQUIRED scoped attestation wording (runbook B2 gate /
round-4 GPT §11): the mechanized model is verified; deployed
consistency correspondence relies on the unmechanized authentic-pair
invariant (KNOWN-GAPS 14/15).

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-16 11:08:01 +02:00

223 lines
9.9 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
- 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"]
Reference in a new issue View git blame Copy permalink