DIV + REM - Githubissues

jasmin-lang / jasmin

Language for high-assurance and high-speed cryptography

MIT License

271 stars 55 forks source link

Closed eponier closed 1 week ago

eponier commented 1 week ago

Also:

reorder riscv_instr_decl.v for consistency
remove GP/TP from the formalization (according to the RISC-V ABI, they are "unallocatable")

eponier commented 1 week ago

I rebased on top of latest risc-v. Extraction to EC must be updated to take into account DIV and REM, but I don't know how to do that.

clebreto commented 1 week ago

@bgregoir We are in need of a double check regarding the EasyCrypt extraction of DIV and DIVU =)