From f428b846f6cea343c7278d1f2db9c91aa3aa2f09 Mon Sep 17 00:00:00 2001 From: Alex Keizer Date: Fri, 11 Oct 2024 17:35:49 -0500 Subject: [PATCH] slight refactor of read_write_bytes_different --- Arm/Memory/MemoryProofs.lean | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/Arm/Memory/MemoryProofs.lean b/Arm/Memory/MemoryProofs.lean index b4539fc4..f7521a87 100644 --- a/Arm/Memory/MemoryProofs.lean +++ b/Arm/Memory/MemoryProofs.lean @@ -55,19 +55,19 @@ theorem mem_separate_preserved_second_start_addr_add_one apply BitVec.val_nat_le 1 m 64 h0 (_ : 1 < 2^64) h1 decide +set_option maxHeartbeats 0 in theorem Memory.read_write_bytes_different (h : mem_separate addr1 addr1 addr2 (addr2 + (BitVec.ofNat 64 (n - 1)))) : read addr1 (write_bytes n addr2 v mem) = read addr1 mem := by induction n generalizing mem addr1 addr2 case zero => simp only [write_bytes] case succ n ih => - rw [write_bytes, ih ?h_sep] - case h_sep => - show mem_separate addr1 addr1 (addr2 + 1#64) - (addr2 + 1#64 + BitVec.ofNat 64 (n - 1)) = true + have h_sep : mem_separate addr1 addr1 (addr2 + 1#64) + (addr2 + 1#64 + BitVec.ofNat 64 (n - 1)) := by sorry - rw [Memory.read_write_different] - sorry + have h_neq : addr1 ≠ addr2 := + mem_separate_starting_addresses_neq h + rw [write_bytes, ih h_sep, Memory.read_write_different h_neq] theorem read_mem_of_write_mem_bytes_different (hn1 : n <= 2^64) (h : mem_separate addr1 addr1 addr2 (addr2 + (BitVec.ofNat 64 (n - 1)))) :