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
8e299cd0f5
Pure refactor, semantics identical (cargo check green): - from_bytes_wide_parts(bytes) -> (Scalar52, Scalar52): the byte-unpack loops + the 52-bit lo/hi split, as a named prefix - split_words_lo / split_words_hi: the two split halves, built with Scalar52([...]) struct literals instead of per-index mutation - from_bytes_wide: parts -> montgomery_mul(lo, R) -> montgomery_mul(hi, RR) -> add Why: the verification side measured that (a) a WP walk whose motives contain a montgomery_mul call replays its whole body at every kernel step, and (b) straight-line chains of IndexMut closure back-functions make kernel defeq exponential in chain depth. Named prefix functions fix (a); struct-literal construction eliminates the closures and fixes (b). With this shape the full from_bytes_wide certificate kernel-checks in 77 seconds (was: aborted after 30+ minutes). |
||
|---|---|---|
| .github | ||
| curve25519 | ||
| experimental/ed25519-pokos | ||
| scripts | ||
| secp256r1 | ||
| syscall | ||
| .gitattributes | ||
| .gitignore | ||
| Cargo.lock | ||
| Cargo.toml | ||