RISC-V backlifting and examples #174

palmskog · 2024-03-14T10:20:03Z

This PR contains:

backlifting results for RISC-V, following those for ARMv8
fixes to the backlifting proof generation for ARMv8 (and proper name for the theory)
more RISC-V examples and results for those examples (testing backlifting)

Currently a draft because a final cheat in a test case needs to be addressed.

…wap RISC-V example

…etter reflect content

palmskog · 2024-03-15T09:41:43Z

No cheat anymore, can we please merge this before #173 @didriklundberg?

palmskog added 13 commits March 10, 2024 18:40

mod2 riscv example

4084d60

riscv backlifting WIP

46db8ab

riscv state backlifting WIP

816c142

prove default_riscv_bir_state_satisfies_rel_thm

8c4442c

finish initial proof of riscv_lift_contract_thm

8d78fbb

add get_riscv_contract_sing function to bir_backlifterLib

a8aa9ee

boilerplate for using riscv_lift_contract_thm for swap example

9990c28

WIP swap properties

5bf39db

fix some backlifting issues

b7bfed4

fix bir_backlifterLib magic constant, bir_cont proof generation for s…

9f5a368

…wap RISC-V example

get rid of most cheats

b5c54c8

rename bir_backlifterScript.sml to bir_arm8_backlifterScript.sml to b…

fbdb454

…etter reflect content

factor definitions to make riscv backlifter proofs faster

fc53cdc

palmskog requested a review from didriklundberg March 14, 2024 12:14

reorganize backlifter theories to split off ISA-independent results

dc58c6f

palmskog mentioned this pull request Mar 15, 2024

Update to modern syntax #173

Merged

get a vacuous swap contract to RISC-V level to test workflow

714996c

palmskog marked this pull request as ready for review March 15, 2024 09:41

didriklundberg approved these changes Mar 15, 2024

View reviewed changes

didriklundberg merged commit 01abd3b into master Mar 15, 2024
4 checks passed

palmskog deleted the holmake+riscv branch March 15, 2024 15:44

Provide feedback