Release with ARM support

jasmin-lang / jasmin

Language for high-assurance and high-speed cryptography

MIT License

250 stars 53 forks source link

Release with ARM support #373

Open vbgl opened 1 year ago

vbgl commented 1 year ago

This gathers things to happen before a release of Jasmin with ARM support can happen.

Required

[ ] Extraction to EasyCrypt (#366)
- Started: #417
- Continued: #460
[ ] Fix known bugs
[ ] Fix add sp & sub sp.
[ ] Support for flags with ?{ … } syntax
- Done: #594
[ ] Support for global variables
- Started: #428
[ ] Ensure stack-frame allocation emits valid code
- Started: #677

Maybe

[ ] Safety checker

Nice to have

[ ] EasyCrypt model of the ARM platform
[ ] Fix other issues

Out of scope

LibJade for ARM
Fancy instructions (LDM etc.)

sarranz commented 1 year ago

I tried to understand the add r, sp, #imm and sub r, sp #imm problem a bit better. It is simpler than what I explained earlier. The restriction is the following: If the output register r is sp, then imm needs to be a multiple of four. Since we need to do further computation with the value of sp, in Jasmin we don't use this case. So I believe that there is nothing to fix here. I will test more thoroughly now.