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
58894a049a
Pure refactors (cargo check green under both feature sets), semantics of mul unchanged: - dsm_top_index / dsm_loop / dsm_step_p / dsm_step_b helpers: the main double-and-add loop becomes a strictly-decreasing while with a single-assignment body and parameter-rooted borrows (the original loop/break shape with match-updates fails Aeneas' loop fixed point); - the starting-index scan always returns 255: leading zero NAF digits double the identity (a no-op), so the result is unchanged - only the variable-time skip is dropped (constant-time behavior improves); - the downward break-scan (which failed Aeneas' symbolic join) is gone. With these, Charon+Aeneas extract the complete path - non_adjacent_form, NafLookupTable5::from/select, the affine basepoint table, the 256-step dsm_loop, and mul - with zero errors and zero sorries. This opens the double-scalar-multiplication verification campaign (the EdDSA verify equation's core). |
||
|---|---|---|
| .github | ||
| curve25519 | ||
| experimental/ed25519-pokos | ||
| scripts | ||
| secp256r1 | ||
| syscall | ||
| .gitattributes | ||
| .gitignore | ||
| Cargo.lock | ||
| Cargo.toml | ||