mirror of
https://github.com/saymrwulf/anza-cryptography-source.git
synced 2026-09-04 20:24:04 +00:00
Patched source for Aeneas/Charon formal verification transpilation
mrwulf
d275613c37
Pure refactors for the Charon/Aeneas extraction pipeline; production behavior unchanged (both default and pinned configs cargo-check clean, pre-existing warnings only). - ed_sigs::sha512_hash3: single-call SHA-512 oracle, semantically Sha512(r || a || m); a monomorphic signature with no foreign types lets the extractor treat the hash as one opaque oracle (sha2-0.11 stack). - VerificationKey::verify_sha512 (+ recompute_r_sha512, a_bytes_nonzero, check_scalar_canonical, is_legacy_excluded_r): semantically identical to verify_dalek with each step spelled extractor-friendly - derived array PartialEq/contains as explicit index loops, and Scalar::from_canonical_bytes (subtle internals defeat the extractor) as an explicit s < l byte compare + from_bytes_mod_order (the identity on canonical bytes). Signature accessors each called exactly once. - SIMD gates: cfg(target_arch = "x86_64") becomes cfg(all(target_arch = "x86_64", not(curve25519_serial_only))). Default builds are identical (the new cfg is never set); extraction builds pass RUSTFLAGS=--cfg curve25519_serial_only so the AVX2 dispatch arm compiles out and backend selection is the real constant Serial - the same serial-pin mechanism upstream curve25519-dalek provides natively. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> |
||
|---|---|---|
| .github | ||
| curve25519 | ||
| experimental/ed25519-pokos | ||
| scripts | ||
| secp256r1 | ||
| syscall | ||
| .gitattributes | ||
| .gitignore | ||
| Cargo.lock | ||
| Cargo.toml | ||