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"]