Add a simp attribute to control the lemmas used to simplify terms inv…

…olving state accessors and updaters.
leanprover · Mar 1, 2024 · 6b0d380 · 6b0d380
1 parent 5a39086
commit 6b0d380
Show file tree

Hide file tree

Showing 9 changed files with 137 additions and 59 deletions.
diff --git a/Arm/Attr.lean b/Arm/Attr.lean
@@ -0,0 +1,21 @@
+import Lean
+
+-- Non-interference lemmas for simplifying terms involving state
+-- accessors and updaters.
+register_simp_attr state_simp_rules
+
+syntax "state_simp" : tactic
+macro_rules
+  | `(tactic| state_simp) => `(tactic| simp only [state_simp_rules])
+
+syntax "state_simp?" : tactic
+macro_rules
+  | `(tactic| state_simp?) => `(tactic| simp? only [state_simp_rules])
+
+syntax "state_simp_all" : tactic
+macro_rules
+  | `(tactic| state_simp_all) => `(tactic| simp_all only [state_simp_rules])
+
+syntax "state_simp_all?" : tactic
+macro_rules
+  | `(tactic| state_simp_all?) => `(tactic| simp_all? only [state_simp_rules])
diff --git a/Arm/Insts/DPSFP/Advanced_simd_three_same.lean b/Arm/Insts/DPSFP/Advanced_simd_three_same.lean
@@ -113,11 +113,14 @@ theorem pc_of_exec_advanced_simd_three_same
   -- (r StateField.PC s) + 4#64 -- TODO: How do I use + here?
   (BitVec.add (r StateField.PC s) 4#64) := by
   simp_all!
-  simp [exec_advanced_simd_three_same, exec_binary_vector, exec_logic_vector]
+  simp only [exec_advanced_simd_three_same, exec_binary_vector, 
+             Bool.and_eq_true, beq_iff_eq, binary_vector_op,
+             ofNat_eq_ofNat, zero_eq, exec_logic_vector, 
+             logic_vector_op]
   split
-  · split <;> simp
-  · simp
-  · simp
+  · split <;> state_simp
+  · state_simp
+  · state_simp
 
 ----------------------------------------------------------------------
 

diff --git a/Arm/Map.lean b/Arm/Map.lean
@@ -115,8 +115,17 @@ def Map.size (m : Map α β) : Nat :=
 @[simp] theorem Map.size_erase_le [DecidableEq α] (m : Map α β) (a : α) : (m.erase a).size ≤ m.size := by
   induction m <;> simp [erase, size] at *
   split
-  next => omega
-  next => simp; omega
+  next => 
+    -- (FIXME) This could be discharged by omega in
+    -- leanprover/lean4:nightly-2024-02-24, but not in
+    -- leanprover/lean4:nightly-2024-03-01.
+    exact Nat.le_succ_of_le (by assumption)
+  next => 
+    simp; 
+    -- (FIXME) This could be discharged by omega in
+    -- leanprover/lean4:nightly-2024-02-24, but not in
+    -- leanprover/lean4:nightly-2024-03-01.  
+    exact Nat.succ_le_succ (by assumption)
 
 @[simp] theorem Map.size_erase_eq [DecidableEq α] (m : Map α β) (a : α) : m.contains a = false → (m.erase a).size = m.size := by
   induction m <;> simp [erase, size] at *
@@ -127,5 +136,13 @@ def Map.size (m : Map α β) : Nat :=
   induction m <;> simp [erase, size, contains, find?] at *
   next head tail ih =>
   split
-  next => have := Map.size_erase_le tail a; omega
-  next he => simp [he] at h; simp [h] at ih; simp; omega
+  next => have := Map.size_erase_le tail a; 
+          -- (FIXME) This could be discharged by omega in
+          -- leanprover/lean4:nightly-2024-02-24, but not in
+          -- leanprover/lean4:nightly-2024-03-01.
+          exact Nat.lt_succ_of_le this
+  next he => simp [he] at h; simp [h] at ih; simp; 
+          -- (FIXME) This could be discharged by omega in
+          -- leanprover/lean4:nightly-2024-02-24, but not in
+          -- leanprover/lean4:nightly-2024-03-01.
+             exact Nat.succ_lt_succ ih
diff --git a/Arm/Memory.lean b/Arm/Memory.lean
@@ -54,13 +54,13 @@ theorem r_of_write_mem : r fld (write_mem addr val s) = r fld s := by
   unfold write_mem
   split <;> simp
 
-@[simp]
+@[state_simp_rules]
 theorem r_of_write_mem_bytes :
   r fld (write_mem_bytes n addr val s) = r fld s := by
   induction n generalizing addr s
   case succ =>
     rename_i n n_ih
-    unfold write_mem_bytes; simp
+    unfold write_mem_bytes; simp only
     rw [n_ih, r_of_write_mem]
   case zero => rfl
   done
@@ -70,14 +70,14 @@ theorem fetch_inst_of_write_mem :
   unfold fetch_inst write_mem
   simp
 
-@[simp]
+@[state_simp_rules]
 theorem fetch_inst_of_write_mem_bytes :
   fetch_inst addr1 (write_mem_bytes n addr2 val s) = fetch_inst addr1 s := by
   induction n generalizing addr2 s
   case zero => rfl
   case succ =>
     rename_i n n_ih
-    unfold write_mem_bytes; simp
+    unfold write_mem_bytes; simp only
     rw [n_ih, fetch_inst_of_write_mem]
   done
 
@@ -88,26 +88,27 @@ theorem read_mem_of_w :
   unfold write_base_pc write_base_flag write_base_error
   split <;> simp
 
-@[simp]
+@[state_simp_rules]
 theorem read_mem_bytes_of_w :
   read_mem_bytes n addr (w fld v s) = read_mem_bytes n addr s := by
   induction n generalizing addr s
   case zero => rfl
   case succ =>
     rename_i n n_ih
-    unfold read_mem_bytes; simp [read_mem_of_w]
+    unfold read_mem_bytes; simp only [read_mem_of_w]
     rw [n_ih]
   done
 
+@[state_simp_rules]
 theorem write_mem_bytes_program {n : Nat} (addr : BitVec 64) (bytes : BitVec (n * 8)):
     (write_mem_bytes n addr bytes s).program = s.program := by
   intros
   induction n generalizing addr s
   · simp [write_mem_bytes]
   · rename_i n h_n
-    simp [write_mem_bytes]
+    simp only [write_mem_bytes]
     rw [h_n]
-    simp [write_mem]
+    simp only [write_mem]
 
 ---- Memory RoW/WoW lemmas ----
 

diff --git a/Arm/MemoryProofs.lean b/Arm/MemoryProofs.lean
@@ -82,7 +82,7 @@ theorem append_byte_of_extract_rest_same_cast (n : Nat) (v : BitVec ((n + 1) * 8
   · omega
   done
 
-@[simp]
+@[state_simp_rules]
 theorem read_mem_bytes_of_write_mem_bytes_same (hn1 : n <= 2^64) :
   read_mem_bytes n addr (write_mem_bytes n addr v s) = v := by
   by_cases hn0 : n = 0
@@ -127,7 +127,7 @@ theorem read_mem_bytes_of_write_mem_bytes_same (hn1 : n <= 2^64) :
 ----------------------------------------------------------------------
 -- Key theorem: read_mem_bytes_of_write_mem_bytes_different
 
-@[simp]
+@[state_simp_rules]
 theorem read_mem_bytes_of_write_mem_bytes_different
   (hn1 : n1 <= 2^64) (hn2 : n2 <= 2^64)
   (h : mem_separate addr1 (addr1 + (n1 - 1)#64) addr2 (addr2 + (n2 - 1)#64)) :
@@ -208,7 +208,7 @@ theorem write_mem_of_write_mem_bytes_commute
       · omega
   done
 
-@[simp]
+@[state_simp_rules]
 theorem write_mem_bytes_of_write_mem_bytes_commute
   (h1 : n1 <= 2^64) (h2 : n2 <= 2^64)
   (h3 : mem_separate addr2 (addr2 + (n2 - 1)#64) addr1 (addr1 + (n1 - 1)#64)) :
@@ -247,7 +247,7 @@ theorem write_mem_bytes_of_write_mem_bytes_commute
 -- Key theorems: write_mem_bytes_of_write_mem_bytes_shadow_same_region
 -- and write_mem_bytes_of_write_mem_bytes_shadow_general
 
-@[simp]
+@[state_simp_rules]
 theorem write_mem_bytes_of_write_mem_bytes_shadow_same_region
   (h : n <= 2^64) :
   write_mem_bytes n addr val2 (write_mem_bytes n addr val1 s) =
@@ -473,7 +473,7 @@ private theorem write_mem_bytes_of_write_mem_bytes_shadow_general_n2_eq
           · omega
         · exact h₁
 
-@[simp]
+@[state_simp_rules]
 theorem write_mem_bytes_of_write_mem_bytes_shadow_general
   (h1u : n1 <= 2^64) (h2l : 0 < n2) (h2u : n2 <= 2^64)
   (h3 : mem_subset addr1 (addr1 + (n1 - 1)#64) addr2 (addr2 + (n2 - 1)#64)) :
@@ -803,7 +803,7 @@ private theorem read_mem_bytes_of_write_mem_bytes_subset_n2_lt
     (extractLsb ((((addr2 - addr1).toNat + n2) * 8) - 1) ((addr2 - addr1).toNat * 8) val) := by
   induction n2, h2 using Nat.le_induction generalizing addr1 addr2 val s
   case base =>
-    simp only [Nat.reduceSucc, Nat.succ_sub_succ_eq_sub, 
+    simp only [Nat.reduceSucc, Nat.succ_sub_succ_eq_sub,
                Nat.sub_self, BitVec.add_zero] at h4
     simp_all only [read_mem_bytes, BitVec.cast_eq]
     have h' : (BitVec.toNat (addr2 - addr1) + 1) * 8 - 1 - BitVec.toNat (addr2 - addr1) * 8 + 1 = 8 := by
@@ -832,7 +832,7 @@ private theorem read_mem_bytes_of_write_mem_bytes_subset_n2_lt
         · have l0 := @mem_subset_trans (addr2 + 1#64) (addr2 + n#64) addr2 (addr2 + n#64)
                    addr1 (addr1 + (n1 - 1)#64)
           simp only [h4] at l0
-          rw [first_addresses_add_one_is_subset_of_region_general 
+          rw [first_addresses_add_one_is_subset_of_region_general
               (by omega) (by omega) (by omega)] at l0
           · simp_all only [Nat.succ_sub_succ_eq_sub, Nat.sub_zero, forall_const]
           · simp only [mem_subset_refl]
@@ -939,7 +939,7 @@ private theorem read_mem_bytes_of_write_mem_bytes_subset_n2_eq_alt
       simp [my_pow_2_gt_zero]
     · unfold my_pow; decide
 
-@[simp]
+@[state_simp_rules]
 theorem read_mem_bytes_of_write_mem_bytes_subset
   (h0 : 0 < n1) (h1 : n1 <= 2^64) (h2 : 0 < n2) (h3 : n2 <= 2^64)
   (h4 : mem_subset addr2 (addr2 + (n2 - 1)#64) addr1 (addr1 + (n1 - 1)#64))
@@ -1009,7 +1009,7 @@ private theorem extract_byte_of_read_mem_bytes_succ (n : Nat) :
   rw [l0, Nat.mod_eq_of_lt y.isLt]
   done
 
-@[simp]
+@[state_simp_rules]
 theorem write_mem_bytes_irrelevant :
   write_mem_bytes n addr (read_mem_bytes n addr s) s = s := by
   induction n generalizing addr s
@@ -1028,6 +1028,17 @@ theorem write_mem_bytes_irrelevant :
     exact n_ih'
     done
 
+-- set_option pp.deepTerms false in
+-- set_option pp.deepTerms.threshold 1000 in
+-- theorem write_mem_bytes_irrelevant :
+--   write_mem_bytes n addr (read_mem_bytes n addr s) s = s := by
+--   induction n generalizing addr s
+--   case zero => simp only [write_mem_bytes]
+--   case succ =>
+--     rename_i n n_ih
+--     simp only [read_mem_bytes, write_mem_bytes]
+--     sorry
+
 ----------------------------------------------------------------------
 
 end MemoryProofs