Boosted by soatok@furry.engineer ("Soatok Dreamseeker"):
pornin@infosec.exchange ("Thomas Pornin") wrote:
I made some variations on Montgomery multiplication with redundant representations. As an illustration, I made some codegolfed ECDSA signature verification (curve P-256) on 64-bit architectures (x86, Arm and RISC-V); I got that down to 848 bytes of code on x86 with a still usable runtime cost. Moreover, there is a comprehensive range analysis (automated) that proves that the computation cannot overflow.
AI was not used, but it was defeated.
Paper is here: https://github.com/pornin/small-ecdsa/blob/main/tex/mmul.pdf
More generally, the repository contains the paper, the code, and the proof (in Python): https://github.com/pornin/small-ecdsa