leanprover/LNSym

Issues

• Prove mem_separate_of_mem_separate'

  #137 opened 4 months ago by bollu
  0

• Update StateEq.lean

  #134 opened 4 months ago by shigoel
  1

• Teach CSE to ignore Bitvector literals

  #127 opened 4 months ago by bollu
  0

• Cache Target Triple Information for Random Instruction Generation

  #97 opened 4 months ago by bollu
  0

• Elab and delab for ARM instructions

  #121 opened 4 months ago by bollu
  0

• memory: add zero byte read/write theorems

  #117 opened 4 months ago by bollu
  0

• memory: zero width subsets

  #116 opened 4 months ago by bollu
  0

• memory: overlapping_read_test_4 hangs at bv_omega.

  #115 opened 4 months ago by bollu
  0

• Rethink Memory accessors for ArmState

  #112 opened 4 months ago by bollu
  0

• Switch back to using leanprover/lean-action once MacOS runner is fixed

  #82 opened 4 months ago by bollu
  0

• ELF Parser in Lean

  #18 opened 10 months ago by shigoel
  32

• Experiment: Use r for accessing the program field, which solves program being public.

  #55 opened 5 months ago by bollu
  0