feat: Correctness of Memcpy program (#138)

We add a manual proof of `memcpy` to understand just how complex a proof will be. The proof challenges `simp_mem`, due to, what we suspect, are `omega` scaling bottlenecks. This file will be used as a litmus test for improving automation. ### Testing: `make all` succeeds, nothing was change with regards to conformance. ### License: By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license. --------- Co-authored-by: Shilpi Goel <[email protected]>
leanprover · Sep 25, 2024 · bbd3075 · bbd3075
1 parent 26b5da0
commit bbd3075
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