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