From 4e7e52ca4c92099961ad8c25a5f02f610d5778a8 Mon Sep 17 00:00:00 2001
From: Shilpi Goel <shigoel@gmail.com>
Date: Thu, 5 Sep 2024 15:13:09 -0700
Subject: [PATCH] Add StateEq theorems to Arm/State.lean (#141)

### Issues:

Resolves #134

### Description:

Prove `state_eq_iff_components_eq`, which says that two `ArmState`s are
equal iff their components, accessed via canonical accessor functions,
are equal.

### Testing:

`make all` succeeded locally.

### License:

By submitting this pull request, I confirm that my contribution is
made under the terms of the Apache 2.0 license.
---
 Arm/State.lean   | 100 ++++++++++++++++++++++++++++++++++-
 Arm/StateEq.lean | 133 -----------------------------------------------
 2 files changed, 98 insertions(+), 135 deletions(-)
 delete mode 100644 Arm/StateEq.lean

diff --git a/Arm/State.lean b/Arm/State.lean
index eaf7347c..dcff1083 100644
--- a/Arm/State.lean
+++ b/Arm/State.lean
@@ -1074,9 +1074,13 @@ by_cases h : ix < base
 
 end Memory
 
-/-! ## Helper lemma for `AxEffects` -/
 
-@[state_simp_rules]
+/-! ## Equality of `ArmState`s and their Components -/
+
+section StateEq
+
+/- Helper lemma for `AxEffects` -/
+
 theorem Memory.eq_of_read_mem_bytes_eq {m₁ m₂ : Memory}
     (h : ∀ n addr, m₁.read_bytes n addr = m₂.read_bytes n addr) :
     m₁ = m₂ := by
@@ -1103,3 +1107,95 @@ theorem read_mem_bytes_write_mem_bytes_of_read_mem_eq
   revert n₁ addr₁
   simp only [← mem_eq_iff_read_mem_bytes_eq] at h ⊢
   simp only [memory_rules, h]
+
+/- Helper lemma for `state_eq_iff_components_eq` -/
+
+private theorem reads_equal_implies_gpr_equal (s1 s2 : ArmState)
+  (h : ∀ (f : StateField), r f s1 = r f s2) :
+  ArmState.gpr s1 = ArmState.gpr s2 := by
+  funext i
+  simpa only [r, read_base_gpr, read_store] using h (.GPR i)
+
+private theorem reads_equal_implies_sfp_equal (s1 s2 : ArmState)
+  (h : ∀ (f : StateField), r f s1 = r f s2) :
+  ArmState.sfp s1 = ArmState.sfp s2 := by
+  funext i
+  simpa only [r, read_base_sfp, read_store] using h (.SFP i)
+
+private theorem reads_equal_implies_pc_equal (s1 s2 : ArmState)
+  (h : ∀ (f : StateField), r f s1 = r f s2) :
+  ArmState.pc s1 = ArmState.pc s2 := by
+  funext
+  simpa only [r, read_base_pc, read_store] using h (.PC)
+
+private theorem reads_equal_implies_pstate_equal (s1 s2 : ArmState)
+  (h : ∀ (f : StateField), r f s1 = r f s2) :
+  ArmState.pstate s1 = ArmState.pstate s2 := by
+  rw [@PState.ext_iff s1.pstate s2.pstate]
+  have h_n := by simpa only [r, read_base_flag, read_store] using h (.FLAG .N)
+  have h_z := by simpa only [r, read_base_flag, read_store] using h (.FLAG .Z)
+  have h_c := by simpa only [r, read_base_flag, read_store] using h (.FLAG .C)
+  have h_v := by simpa only [r, read_base_flag, read_store] using h (.FLAG .V)
+  simp_all only [and_true]
+
+private theorem reads_equal_implies_error_equal (s1 s2 : ArmState)
+  (h : ∀ (f : StateField), r f s1 = r f s2) :
+  ArmState.error s1 = ArmState.error s2 := by
+  funext
+  simpa only [r, read_base_error, read_store] using h (.ERR)
+
+private theorem read_mem_equal_implies_mem_equal (s1 s2 : ArmState)
+  (h_mem : ∀ (addr : BitVec 64), read_mem addr s1 = read_mem addr s2) :
+  s1.mem = s2.mem := by
+  funext i
+  simpa only [read_mem, read_store] using h_mem i
+
+private theorem read_mem_bytes_equal_implies_read_mem_equal (s1 s2 : ArmState)
+  (h_mem : ∀ (n : Nat) (addr : BitVec 64),
+              read_mem_bytes n addr s1 = read_mem_bytes n addr s2) :
+  ∀ (addr : BitVec 64), read_mem addr s1 = read_mem addr s2 := by
+  intro addr
+  have h_read_mem_bytes_all := h_mem 1 addr
+  simp only [read_mem_bytes, bitvec_rules] at h_read_mem_bytes_all
+  have h1 := @BitVec.empty_bitvector_append_left 8 (read_mem addr s1)
+  have h2 := @BitVec.empty_bitvector_append_left 8 (read_mem addr s2)
+  simp_all only
+
+private theorem read_mem_bytes_equal_implies_mem_equal (s1 s2 : ArmState)
+  (h_mem : ∀ (n : Nat) (addr : BitVec 64),
+              read_mem_bytes n addr s1 = read_mem_bytes n addr s2) :
+  s1.mem = s2.mem := by
+  funext i
+  rw [read_mem_equal_implies_mem_equal]
+  intro addr
+  rwa [read_mem_bytes_equal_implies_read_mem_equal]
+
+/--
+Two `ArmState`s are equal iff their components, accessed via canonical
+accessor functions, are equal.
+-/
+theorem state_eq_iff_components_eq {s1 s2 : ArmState} :
+  (s1 = s2) ↔
+  ((∀ (f : StateField), r f s1 = r f s2) ∧
+   (s1.program = s2.program) ∧
+   (∀ (n : Nat) (addr : BitVec 64),
+      read_mem_bytes n addr s1 = read_mem_bytes n addr s2)) := by
+  constructor
+  case mp =>
+    intro h
+    subst_vars
+    simp only [implies_true, and_self]
+  case mpr =>
+    intro h
+    obtain ⟨h_fields, h_program, h_mem⟩ := h
+    apply ArmState.ext
+    case gpr => rwa [reads_equal_implies_gpr_equal]
+    case sfp => rwa [reads_equal_implies_sfp_equal]
+    case pc  => rwa [reads_equal_implies_pc_equal]
+    case pstate => rwa [reads_equal_implies_pstate_equal]
+    case error => rwa [reads_equal_implies_error_equal]
+    case program => assumption
+    case mem => rwa [read_mem_bytes_equal_implies_mem_equal]
+  done
+
+end StateEq
diff --git a/Arm/StateEq.lean b/Arm/StateEq.lean
deleted file mode 100644
index e3f685c5..00000000
--- a/Arm/StateEq.lean
+++ /dev/null
@@ -1,133 +0,0 @@
-/-
-Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Author(s): Shilpi Goel
--/
-import Arm.State
-section StateEq
-
-open BitVec
-
-private theorem reads_equal_implies_gpr_equal (s1 s2 : ArmState)
-  (h : ∀ (f : StateField), r f s1 = r f s2) :
-  ArmState.gpr s1 = ArmState.gpr s2 := by
-  have h_gpr : ∀ (i : BitVec 5),
-    r (StateField.GPR i) s1 = r (StateField.GPR i) s2 := by
-    intro i; rw [h]
-  unfold r at h_gpr
-  simp only [read_base_gpr, read_store] at h_gpr
-  apply funext
-  assumption
-
-private theorem reads_equal_implies_sfp_equal (s1 s2 : ArmState)
-  (h : ∀ (f : StateField), r f s1 = r f s2) :
-  ArmState.sfp s1 = ArmState.sfp s2 := by
-  have h_sfp : ∀ (i : BitVec 5),
-    r (StateField.SFP i) s1 = r (StateField.SFP i) s2 := by
-    intro i; rw [h]
-  unfold r at h_sfp
-  simp only [read_base_sfp, read_store] at h_sfp
-  apply funext
-  assumption
-
-private theorem reads_equal_implies_pc_equal (s1 s2 : ArmState)
-  (h : ∀ (f : StateField), r f s1 = r f s2) :
-  ArmState.pc s1 = ArmState.pc s2 := by
-  have h_pc : r StateField.PC s1 = r StateField.PC s2 := by
-    rw [h]
-  unfold r at h_pc
-  simp only [read_base_pc, read_store] at h_pc
-  assumption
-
-private theorem reads_equal_implies_pstate_equal (s1 s2 : ArmState)
-  (h : ∀ (f : StateField), r f s1 = r f s2) :
-  ArmState.pstate s1 = ArmState.pstate s2 := by
-  have h_flag : ∀ (i : PFlag),
-    r (StateField.FLAG i) s1 = r (StateField.FLAG i) s2 := by
-    intro i; rw [h]
-  unfold r at h_flag
-  simp only [read_base_flag, read_store] at h_flag
-  have h_flag_n := h_flag PFlag.N
-  simp only at h_flag_n
-  have h_flag_z := h_flag PFlag.Z
-  simp only at h_flag_z
-  have h_flag_c := h_flag PFlag.C
-  simp only at h_flag_c
-  have h_flag_v := h_flag PFlag.V
-  simp only at h_flag_v
-  clear h_flag
-  rw [@PState.ext_iff s1.pstate s2.pstate]
-  simp only [*, minimal_theory]
-  done
-
-private theorem reads_equal_implies_error_equal (s1 s2 : ArmState)
-  (h : ∀ (f : StateField), r f s1 = r f s2) :
-  ArmState.error s1 = ArmState.error s2 := by
-  have h_err : r StateField.ERR s1 = r StateField.ERR s2 := by
-    rw [h]
-  unfold r at h_err
-  simp only [read_base_error, read_store] at h_err
-  assumption
-
-private theorem read_mem_and_mem_equal (s1 s2 : ArmState)
-  (h_mem : ∀ (addr : BitVec 64), read_mem addr s1 = read_mem addr s2) :
-  s1.mem = s2.mem := by
-  unfold read_mem read_store at h_mem
-  apply funext
-  simp_all only [minimal_theory]
-  done
-
-private theorem read_mem_bytes_and_read_mem (s1 s2 : ArmState)
-  (h_mem : ∀ (n : Nat) (addr : BitVec 64),
-      read_mem_bytes n addr s1 = read_mem_bytes n addr s2) :
-  ∀ (addr : BitVec 64), read_mem addr s1 = read_mem addr s2 := by
-  intro addr
-  have h_read_mem_bytes_all := h_mem 1 addr
-  simp [read_mem_bytes] at h_read_mem_bytes_all
-  have h1 := @BitVec.empty_bitvector_append_left 8 (read_mem addr s1)
-  have h2 := @BitVec.empty_bitvector_append_left 8 (read_mem addr s2)
-  simp_all only
-  done
-
-private theorem read_mem_equal_implies_mem_equal (s1 s2 : ArmState)
-  (h_mem : ∀ (n : Nat) (addr : BitVec 64),
-    read_mem_bytes n addr s1 = read_mem_bytes n addr s2) :
-  s1.mem = s2.mem := by
-  rw [read_mem_and_mem_equal]; intro addr
-  rwa [read_mem_bytes_and_read_mem]
-  done
-
-theorem reads_equal_implies_states_equal (s1 s2 : ArmState)
-  (h_fields : ∀ (f : StateField), r f s1 = r f s2)
-  (h_program : s1.program = s2.program)
-  (h_mem : ∀ (n : Nat) (addr : BitVec 64),
-    read_mem_bytes n addr s1 = read_mem_bytes n addr s2) :
-  s1 = s2 := by
-  apply ArmState.ext
-  case gpr => rwa [reads_equal_implies_gpr_equal]
-  case sfp => rwa [reads_equal_implies_sfp_equal]
-  case pc  => rwa [reads_equal_implies_pc_equal]
-  case pstate => rwa [reads_equal_implies_pstate_equal]
-  case error => rwa [reads_equal_implies_error_equal]
-  case program => assumption
-  case mem => rwa [read_mem_equal_implies_mem_equal]
-  done
-
-theorem r_of_w_general :
-  r fld1 (w fld2 v s) =
-    if h : fld1 = fld2 then
-      have h' : state_value fld1 = state_value fld2 := by
-        simp_all
-      h' ▸ v
-    else
-      r fld1 s := by
-  by_cases h : fld1 = fld2
-  case pos =>
-    rw [h]; simp only [r_of_w_same, ↓reduceDIte]
-  case neg =>
-    simp_all only [dite_false]
-    apply r_of_w_different
-    assumption
-  done
-
-end StateEq