Merge branch 'main' into cleanup-popcount

leanprover · Sep 25, 2024 · 8f7799d · 8f7799d
2 parents 2d5a84b + bbd3075
commit 8f7799d
Show file tree

Hide file tree

Showing 5 changed files with 797 additions and 178 deletions.
diff --git a/Arm/State.lean b/Arm/State.lean
@@ -820,6 +820,7 @@ A variant of `write_mem` that directly talks about writes to memory, instead of
 def Memory.write (addr : BitVec 64) (val : BitVec 8) (m : Memory) : Memory :=
   write_store addr val m
 
+@[state_simp_rules]
 theorem ArmState.write_mem_eq_mem_write :  (write_mem addr val s).mem = s.mem.write addr val := rfl
 
 namespace Memory

diff --git a/Proofs/Experiments/MemCpyVCG.lean b/Proofs/Experiments/MemCpyVCG.lean