Code

RISC-V backlifting and examples#174

Code

Merged

didriklundberg merged 15 commits intomasterkth-step/HolBA:masterfrom holmake+riscvkth-step/HolBA:holmake+riscvCopy head branch name to clipboardMar 15, 2024

+1,873-188

Commits

Commits on Mar 10, 2024

• mod2 riscv example

  palmskog

  committed
  4084d60

  Copy full SHA for 4084d60

• riscv backlifting WIP

  palmskog

  committed
  46db8ab

  Copy full SHA for 46db8ab

• riscv state backlifting WIP

  palmskog

  committed
  816c142

  Copy full SHA for 816c142

Commits on Mar 11, 2024

• prove default_riscv_bir_state_satisfies_rel_thm

  palmskog

  committed
  8c4442c

  Copy full SHA for 8c4442c

• finish initial proof of riscv_lift_contract_thm

  palmskog

  committed
  8d78fbb

  Copy full SHA for 8d78fbb

• add get_riscv_contract_sing function to bir_backlifterLib

  palmskog

  committed
  a8aa9ee

  Copy full SHA for a8aa9ee

Commits on Mar 13, 2024

• boilerplate for using riscv_lift_contract_thm for swap example

  palmskog

  committed
  9990c28

  Copy full SHA for 9990c28

• WIP swap properties

  palmskog

  committed
  5bf39db

  Copy full SHA for 5bf39db

• fix some backlifting issues

  palmskog

  committed
  b7bfed4

  Copy full SHA for b7bfed4

Commits on Mar 14, 2024

• fix bir_backlifterLib magic constant, bir_cont proof generation for swap RISC-V example

  palmskog

  committed
  9f5a368

  Copy full SHA for 9f5a368

• get rid of most cheats

  palmskog

  committed
  b5c54c8

  Copy full SHA for b5c54c8

• rename bir_backlifterScript.sml to bir_arm8_backlifterScript.sml to better reflect content

  palmskog

  committed
  fbdb454

  Copy full SHA for fbdb454

• factor definitions to make riscv backlifter proofs faster

  palmskog

  committed
  fc53cdc

  Copy full SHA for fc53cdc

• reorganize backlifter theories to split off ISA-independent results

  palmskog

  committed
  dc58c6f

  Copy full SHA for dc58c6f

Commits on Mar 15, 2024

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

  palmskog

  committed
  714996c

  Copy full SHA for 714996c