diff --git a/Arm/Cosim.lean b/Arm/Cosim.lean
index fdd3b348..1b4ee09d 100644
--- a/Arm/Cosim.lean
+++ b/Arm/Cosim.lean
@@ -73,7 +73,7 @@ def init_flags (flags : BitVec 4) (s : ArmState) : ArmState := Id.run do
 /-- Initialize an ArmState for cosimulation from a given regState. -/
 def regState_to_armState (r : regState) : ArmState :=
   let s := init_gprs r.gpr (init_flags r.nzcv (init_sfps r.sfp init_cosim_state))
-  let s := { s with program := def_program [(0x0#64, r.inst)] }
+  let s := set_program s (def_program [(0x0#64, r.inst)])
   s
 
 def bitvec_to_hex (x : BitVec n) : String :=
@@ -128,7 +128,7 @@ bitvector values.-/
 def gpr_list (s : ArmState) : List (BitVec 64) := Id.run do
   let mut acc := []
   for i in [0:31] do
-    acc :=  acc ++ [(s.gpr (BitVec.ofNat 5 i))]
+    acc :=  acc ++ [read_gpr 64 (BitVec.ofNat 5 i) s]
   pure acc
 
 /-- Get the SIMD/FP registers in an ArmState as a list of bitvector
@@ -136,7 +136,7 @@ values.-/
 def sfp_list (s : ArmState) : List (BitVec 64) := Id.run do
   let mut acc := []
   for i in [0:32] do
-    let reg := s.sfp (BitVec.ofNat 5 i)
+    let reg := read_sfp 64 (BitVec.ofNat 5 i) s
     acc := acc ++ [(extractLsb 63 0 reg), (extractLsb 127 64 reg)]
   pure acc
 
diff --git a/Arm/Decode.lean b/Arm/Decode.lean
index 0e58797a..52871d61 100644
--- a/Arm/Decode.lean
+++ b/Arm/Decode.lean
@@ -3,7 +3,6 @@ Copyright (c) 2023 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.Memory
 import Arm.Decode.DPI
 import Arm.Decode.DPR
 import Arm.Decode.BR
diff --git a/Arm/Exec.lean b/Arm/Exec.lean
index 6e5ffc50..cfbffa11 100644
--- a/Arm/Exec.lean
+++ b/Arm/Exec.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 import Arm.BitVec
-import Arm.Memory
 import Arm.Decode
 import Arm.Insts
 
diff --git a/Arm/Insts/BR/Compare_branch.lean b/Arm/Insts/BR/Compare_branch.lean
index 41eae29f..b15d551d 100644
--- a/Arm/Insts/BR/Compare_branch.lean
+++ b/Arm/Insts/BR/Compare_branch.lean
@@ -7,7 +7,7 @@ Author(s): Shilpi Goel
 -- CBZ, CBNZ -- 32 and 64-bit variants
 
 import Arm.Decode
-import Arm.Memory
+import Arm.State
 import Arm.Insts.Common
 import Arm.BitVec
 
diff --git a/Arm/Insts/BR/Cond_branch_imm.lean b/Arm/Insts/BR/Cond_branch_imm.lean
index f523140d..d15aa16b 100644
--- a/Arm/Insts/BR/Cond_branch_imm.lean
+++ b/Arm/Insts/BR/Cond_branch_imm.lean
@@ -7,7 +7,7 @@ Author(s): Yan Peng
 -- B.cond
 
 import Arm.Decode
-import Arm.Memory
+import Arm.State
 import Arm.Insts.Common
 import Arm.BitVec
 
diff --git a/Arm/Insts/BR/Uncond_branch_imm.lean b/Arm/Insts/BR/Uncond_branch_imm.lean
index d2623ca0..1313a4d3 100644
--- a/Arm/Insts/BR/Uncond_branch_imm.lean
+++ b/Arm/Insts/BR/Uncond_branch_imm.lean
@@ -7,7 +7,7 @@ Author(s): Shilpi Goel
 -- B, BL
 
 import Arm.Decode
-import Arm.Memory
+import Arm.State
 import Arm.Insts.Common
 import Arm.BitVec
 
diff --git a/Arm/Insts/BR/Uncond_branch_reg.lean b/Arm/Insts/BR/Uncond_branch_reg.lean
index 710d44b1..1e3cbb97 100644
--- a/Arm/Insts/BR/Uncond_branch_reg.lean
+++ b/Arm/Insts/BR/Uncond_branch_reg.lean
@@ -7,7 +7,7 @@ Author(s): Shilpi Goel
 -- RET
 
 import Arm.Decode
-import Arm.Memory
+import Arm.State
 import Arm.Insts.Common
 import Arm.BitVec
 
diff --git a/Arm/Insts/Common.lean b/Arm/Insts/Common.lean
index 794121b5..f2547044 100644
--- a/Arm/Insts/Common.lean
+++ b/Arm/Insts/Common.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel, Yan Peng
 -/
 import Arm.BitVec
-import Arm.Memory
+import Arm.State
 
 section Common
 
diff --git a/Arm/Insts/DPI/PC_rel_addressing.lean b/Arm/Insts/DPI/PC_rel_addressing.lean
index 76bf345f..82f63a35 100644
--- a/Arm/Insts/DPI/PC_rel_addressing.lean
+++ b/Arm/Insts/DPI/PC_rel_addressing.lean
@@ -6,7 +6,7 @@ Author(s): Shilpi Goel
 -- ADR, ADRP
 
 import Arm.Decode
-import Arm.Memory
+import Arm.State
 import Arm.Insts.Common
 import Arm.BitVec
 
diff --git a/Arm/Insts/DPR/Conditional_select.lean b/Arm/Insts/DPR/Conditional_select.lean
index 23939220..547f8ebd 100644
--- a/Arm/Insts/DPR/Conditional_select.lean
+++ b/Arm/Insts/DPR/Conditional_select.lean
@@ -6,7 +6,7 @@ Author(s): Shilpi Goel
 -- CSEL, CSINC, CSINV, CSNEG: 32- and 64-bit versions
 
 import Arm.Decode
-import Arm.Memory
+import Arm.State
 import Arm.Insts.Common
 import Arm.BitVec
 
diff --git a/Arm/Insts/DPSFP/Advanced_simd_extract.lean b/Arm/Insts/DPSFP/Advanced_simd_extract.lean
index abfa13ed..19e9ead5 100644
--- a/Arm/Insts/DPSFP/Advanced_simd_extract.lean
+++ b/Arm/Insts/DPSFP/Advanced_simd_extract.lean
@@ -6,7 +6,7 @@ Author(s): Shilpi Goel
 -- EXT
 
 import Arm.Decode
-import Arm.Memory
+import Arm.State
 import Arm.Insts.Common
 import Arm.BitVec
 
diff --git a/Arm/Insts/DPSFP/Advanced_simd_three_different.lean b/Arm/Insts/DPSFP/Advanced_simd_three_different.lean
index ed311369..2d18e935 100644
--- a/Arm/Insts/DPSFP/Advanced_simd_three_different.lean
+++ b/Arm/Insts/DPSFP/Advanced_simd_three_different.lean
@@ -7,7 +7,7 @@ Author(s): Yan Peng
 -- Polynomial arithmetic over {0,1}: https://tiny.amazon.com/5h01fjm6/devearmdocuddi0cApplApplPoly
 
 import Arm.Decode
-import Arm.Memory
+import Arm.State
 import Arm.Insts.Common
 
 ----------------------------------------------------------------------
diff --git a/Arm/Insts/DPSFP/Advanced_simd_three_same.lean b/Arm/Insts/DPSFP/Advanced_simd_three_same.lean
index ca4ad97f..616ecd5e 100644
--- a/Arm/Insts/DPSFP/Advanced_simd_three_same.lean
+++ b/Arm/Insts/DPSFP/Advanced_simd_three_same.lean
@@ -6,7 +6,7 @@ Author(s): Shilpi Goel, Yan Peng
 -- ADD, ORR, AND, BIC, ORR, ORN, EOR, BSL, BIT, BIF (vector)
 
 import Arm.Decode
-import Arm.Memory
+import Arm.State
 import Arm.Insts.Common
 import Arm.BitVec
 
diff --git a/Arm/Insts/DPSFP/Advanced_simd_two_reg_misc.lean b/Arm/Insts/DPSFP/Advanced_simd_two_reg_misc.lean
index 7fc90ad5..2d68feaf 100644
--- a/Arm/Insts/DPSFP/Advanced_simd_two_reg_misc.lean
+++ b/Arm/Insts/DPSFP/Advanced_simd_two_reg_misc.lean
@@ -6,7 +6,7 @@ Author(s): Shilpi Goel
 -- REV64
 
 import Arm.Decode
-import Arm.Memory
+import Arm.State
 import Arm.Insts.Common
 import Arm.BitVec
 
diff --git a/Arm/Insts/DPSFP/Crypto_four_reg.lean b/Arm/Insts/DPSFP/Crypto_four_reg.lean
index a0ac299d..a08cede0 100644
--- a/Arm/Insts/DPSFP/Crypto_four_reg.lean
+++ b/Arm/Insts/DPSFP/Crypto_four_reg.lean
@@ -6,7 +6,7 @@ Author(s): Shilpi Goel, Nevine Ebeid
 -- EOR3
 
 import Arm.Decode
-import Arm.Memory
+import Arm.State
 import Arm.Insts.Common
 import Arm.BitVec
 
diff --git a/Arm/Insts/DPSFP/Crypto_three_reg_sha512.lean b/Arm/Insts/DPSFP/Crypto_three_reg_sha512.lean
index 3e8a2f7f..c25d02d8 100644
--- a/Arm/Insts/DPSFP/Crypto_three_reg_sha512.lean
+++ b/Arm/Insts/DPSFP/Crypto_three_reg_sha512.lean
@@ -6,7 +6,7 @@ Author(s): Shilpi Goel
 -- SHA512H, SHA512H2, SHA512SU1
 
 import Arm.Decode
-import Arm.Memory
+import Arm.State
 import Arm.Insts.Common
 import Arm.BitVec
 import Specs.SHA512Common
diff --git a/Arm/Memory.lean b/Arm/Memory.lean
deleted file mode 100644
index 93bff238..00000000
--- a/Arm/Memory.lean
+++ /dev/null
@@ -1,134 +0,0 @@
-/-
-Copyright (c) 2023 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.Separate
-
-section Memory
-
-open BitVec
-
-----------------------------------------------------------------------
-
----- Memory accessors and updaters ----
-
--- We don't add the simp attribute to read/write_mem_bytes. Instead,
--- we prove and export properties about their (non)interference.
-
--- (FIXME) Make read_mem private.
--- We export read_mem_bytes, not read_mem.
-def read_mem (addr : BitVec 64) (s : ArmState) : BitVec 8 :=
-  read_store addr s.mem
-
-def read_mem_bytes (n : Nat) (addr : BitVec 64) (s : ArmState) : BitVec (n * 8) :=
-  match n with
-  | 0 => 0#0
-  | n' + 1 =>
-    let byte := read_mem addr s
-    let rest := read_mem_bytes n' (addr + 1#64) s
-    have h: n' * 8 + 8 = (n' + 1) * 8 := by simp_arith
-    BitVec.cast h (rest ++ byte)
-
--- (FIXME) Make write_mem private.
--- We export write_mem_bytes, not write_mem.
-def write_mem (addr : BitVec 64) (val : BitVec 8) (s : ArmState) : ArmState :=
-  let new_mem := write_store addr val s.mem
-  { s with mem := new_mem }
-
-def write_mem_bytes (n : Nat) (addr : BitVec 64) (val : BitVec (n * 8)) (s : ArmState) : ArmState :=
-  match n with
-  | 0 => s
-  | n' + 1 =>
-    let byte := extractLsb 7 0 val
-    let s := write_mem addr byte s
-    let val_rest := BitVec.zeroExtend (n' * 8) (val >>> 8)
-    write_mem_bytes n' (addr + 1#64) val_rest s
-
----- RoW/WoW lemmas about memory and other fields ----
-
-theorem r_of_write_mem : r fld (write_mem addr val s) = r fld s := by
-  unfold r
-  unfold read_base_gpr read_base_sfp read_base_pc
-  unfold read_base_flag read_base_error
-  unfold write_mem
-  split <;> 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 only
-    rw [n_ih, r_of_write_mem]
-  case zero => rfl
-  done
-
-theorem fetch_inst_of_write_mem :
-  fetch_inst addr1 (write_mem addr2 val s) = fetch_inst addr1 s := by
-  unfold fetch_inst write_mem
-  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 only
-    rw [n_ih, fetch_inst_of_write_mem]
-  done
-
-theorem read_mem_of_w :
-  read_mem addr (w fld v s) = read_mem addr s := by
-  unfold read_mem
-  unfold w write_base_gpr write_base_sfp
-  unfold write_base_pc write_base_flag write_base_error
-  split <;> 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 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 only [write_mem_bytes]
-    rw [h_n]
-    simp only [write_mem]
-
----- Memory RoW/WoW lemmas ----
-
-theorem read_mem_of_write_mem_same :
-  read_mem addr (write_mem addr v s) = v := by
-  unfold read_mem write_mem; simp [store_read_over_write_same]
-
-theorem read_mem_of_write_mem_different (h : addr1 ≠ addr2) :
-  read_mem addr1 (write_mem addr2 v s) = read_mem addr1 s := by
-  unfold read_mem write_mem; simp
-  rw [store_read_over_write_different]; trivial
-
-theorem write_mem_of_write_mem_shadow :
-  write_mem addr val2 (write_mem addr val1 s) = write_mem addr val2 s := by
-  simp [write_mem]; unfold write_store; simp_all; done
-
-theorem write_mem_irrelevant :
-  write_mem addr (read_mem addr s) s = s := by
-  simp [read_mem, write_mem, store_write_irrelevant]
-
-end Memory
-
-----------------------------------------------------------------------
diff --git a/Arm/MemoryProofs.lean b/Arm/MemoryProofs.lean
index 66c83e56..ed70ca51 100644
--- a/Arm/MemoryProofs.lean
+++ b/Arm/MemoryProofs.lean
@@ -3,8 +3,10 @@ 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.SeparateProofs
 import Arm.FromMathlib
+import Arm.State
+import Arm.Separate
+import Arm.SeparateProofs
 
 -- In this file, we have memory (non-)interference proofs.
 
@@ -690,7 +692,7 @@ theorem read_mem_of_write_mem_bytes_subset
           -- disable simproc for 2^64.
           simp only [mod_lt_conc,
                      read_mem_of_write_mem_bytes_subset_helper_5]
-          have h_tmp : (2 ^ 64 - 1 + a) = (a + 2 ^ 64 - 1) := by 
+          have h_tmp : (2 ^ 64 - 1 + a) = (a + 2 ^ 64 - 1) := by
             apply Nat.add_comm
           simp only [h_tmp]
           apply read_mem_of_write_mem_bytes_subset_helper_4 v a n' h_v_size h_a_base h_a_size
diff --git a/Arm/SeparateProofs.lean b/Arm/SeparateProofs.lean
index ddb58552..6e193465 100644
--- a/Arm/SeparateProofs.lean
+++ b/Arm/SeparateProofs.lean
@@ -3,7 +3,8 @@ 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.Memory
+import Arm.State
+import Arm.Separate
 import LeanSAT
 
 ----------------------------------------------------------------------
diff --git a/Arm/State.lean b/Arm/State.lean
index 713989e1..84f7ee70 100644
--- a/Arm/State.lean
+++ b/Arm/State.lean
@@ -120,26 +120,29 @@ def PState.zero : PState :=
 
 @[ext]
 structure ArmState where
-  -- General-purpose registers: register 31 is the stack pointer.
-  gpr        : Store (BitVec 5) (BitVec 64)
-  -- SIMD/floating-point registers
-  sfp        : Store (BitVec 5) (BitVec 128)
-  -- Program Counter
-  pc         : BitVec 64
-  -- PState
-  pstate     : PState
-  -- Memory: maps 64-bit addresses to bytes
-  mem        : Store (BitVec 64) (BitVec 8)
-  -- Program: maps 64-bit addresses to 32-bit instructions.
-  -- Note that we have the following assumption baked into our machine model:
-  -- the program is always disjoint from the rest of the memory.
-  program    : Program
-
-  -- The error field is an artifact of this model; it is set to a
-  -- non-None value when some irrecoverable error is encountered
-  -- (e.g., an unimplemented instruction is hit). Any reasoning or
-  -- execution based off an erroneous state is invalid.
-  error      : StateError
+  /-- General-purpose registers: register 31 is the stack pointer. -/
+  private gpr        : Store (BitVec 5) (BitVec 64)
+  /-- SIMD/floating-point registers -/
+  private sfp        : Store (BitVec 5) (BitVec 128)
+  /-- Program Counter -/
+  private pc         : BitVec 64
+  /-- PState -/
+  private pstate     : PState
+  /-- Memory: maps 64-bit addresses to bytes -/
+  private mem        : Store (BitVec 64) (BitVec 8)
+  /--
+  Program: maps 64-bit addresses to 32-bit instructions.
+  Note that we have the following assumption baked into our machine model:
+  the program is always disjoint from the rest of the memory.
+  -/
+  program            : Program
+  /--
+  The error field is an artifact of this model; it is set to a
+  non-None value when some irrecoverable error is encountered
+  (e.g., an unimplemented instruction is hit). Any reasoning or
+  execution based off an erroneous state is invalid.
+  -/
+  private error      : StateError
 deriving Repr
 
 def ArmState.default : ArmState := { 
@@ -217,6 +220,9 @@ def write_base_flag (flag : PFlag) (val : BitVec 1) (s : ArmState) : ArmState :=
 
 -- Program --
 
+def set_program (s : ArmState) (program : Program) : ArmState :=
+  { s with program := program }
+
 -- Fetch the instruction at address addr.
 @[irreducible]
 def fetch_inst (addr : BitVec 64) (s : ArmState) : Option (BitVec 32) :=
@@ -517,4 +523,132 @@ example :
 
 end State
 
-----------------------------------------------------------------------
+/-! # Memory operations on State. -/
+
+section Memory
+
+/-!
+Ideally, `read_mem` and `write_mem` ought to be private, and we ought to only
+expose `read_mem_bytes` and `write_mem_bytes` to the outside world.
+However, due to layering violations with `Arm/MemoryProofs.lean`, we currently keep them public.
+-/
+
+
+/-- We export read_mem_bytes, not read_mem. FIXME: make private. -/
+def read_mem (addr : BitVec 64) (s : ArmState) : BitVec 8 :=
+  read_store addr s.mem
+
+/--
+We don't add the simp attribute to read/write_mem_bytes. Instead,
+we prove and export properties about their (non)interference.
+-/
+def read_mem_bytes (n : Nat) (addr : BitVec 64) (s : ArmState) : BitVec (n * 8) :=
+  match n with
+  | 0 => 0#0
+  | n' + 1 =>
+    let byte := read_mem addr s
+    let rest := read_mem_bytes n' (addr + 1#64) s
+    (rest ++ byte).cast (by omega)
+
+/-- We export write_mem_bytes, not write_mem. FIXME: make private. -/
+def write_mem (addr : BitVec 64) (val : BitVec 8) (s : ArmState) : ArmState :=
+  let new_mem := write_store addr val s.mem
+  { s with mem := new_mem }
+
+def write_mem_bytes (n : Nat) (addr : BitVec 64) (val : BitVec (n * 8)) (s : ArmState) : ArmState :=
+  match n with
+  | 0 => s
+  | n' + 1 =>
+    let byte := BitVec.extractLsb 7 0 val
+    let s := write_mem addr byte s
+    let val_rest := BitVec.zeroExtend (n' * 8) (val >>> 8)
+    write_mem_bytes n' (addr + 1#64) val_rest s
+
+
+/-! # Memory accessors and updaters -/
+
+/-! ### RoW/WoW lemmas about memory and other fields -/
+
+theorem r_of_write_mem : r fld (write_mem addr val s) = r fld s := by
+  unfold r
+  unfold read_base_gpr read_base_sfp read_base_pc
+  unfold read_base_flag read_base_error
+  unfold write_mem
+  split <;> 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 only
+    rw [n_ih, r_of_write_mem]
+  case zero => rfl
+  done
+
+theorem fetch_inst_of_write_mem :
+  fetch_inst addr1 (write_mem addr2 val s) = fetch_inst addr1 s := by
+  unfold fetch_inst write_mem
+  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 only
+    rw [n_ih, fetch_inst_of_write_mem]
+  done
+
+theorem read_mem_of_w :
+  read_mem addr (w fld v s) = read_mem addr s := by
+  unfold read_mem
+  unfold w write_base_gpr write_base_sfp
+  unfold write_base_pc write_base_flag write_base_error
+  split <;> 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 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 only [write_mem_bytes]
+    rw [h_n]
+    simp only [write_mem]
+
+/-! ### Memory RoW/WoW lemmas -/
+
+theorem read_mem_of_write_mem_same :
+  read_mem addr (write_mem addr v s) = v := by
+  unfold read_mem write_mem; simp [store_read_over_write_same]
+
+theorem read_mem_of_write_mem_different (h : addr1 ≠ addr2) :
+  read_mem addr1 (write_mem addr2 v s) = read_mem addr1 s := by
+  unfold read_mem write_mem; simp
+  rw [store_read_over_write_different]; trivial
+
+theorem write_mem_of_write_mem_shadow :
+  write_mem addr val2 (write_mem addr val1 s) = write_mem addr val2 s := by
+  simp [write_mem]; unfold write_store; simp_all; done
+
+theorem write_mem_irrelevant :
+  write_mem addr (read_mem addr s) s = s := by
+  simp [read_mem, write_mem, store_write_irrelevant]
+
+end Memory
diff --git a/Arm/StateEq.lean b/Arm/StateEq.lean
index ee3cb3e8..e3f685c5 100644
--- a/Arm/StateEq.lean
+++ b/Arm/StateEq.lean
@@ -4,8 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 import Arm.State
-import Arm.Memory
-
 section StateEq
 
 open BitVec
diff --git a/Proofs/Experiments/MemoryAliasing.lean b/Proofs/Experiments/MemoryAliasing.lean
index 471d613a..ea78859d 100644
--- a/Proofs/Experiments/MemoryAliasing.lean
+++ b/Proofs/Experiments/MemoryAliasing.lean
@@ -6,7 +6,6 @@ Author(s): Shilpi Goel, Siddharth Bhat
 The goal is to eliminate the sorry, and to simplify the proof to a tactic invocation.
 -/
 import Arm
--- TODO(@bollu): make this visible from 'Arm'.
 import Arm.MemoryProofs
 
 theorem mem_automation_test
diff --git a/Tests/AES-GCM/AESGCMProgramTests.lean b/Tests/AES-GCM/AESGCMProgramTests.lean
index 0653230c..91de711f 100644
--- a/Tests/AES-GCM/AESGCMProgramTests.lean
+++ b/Tests/AES-GCM/AESGCMProgramTests.lean
@@ -216,7 +216,7 @@ def final_ciphertext : BitVec 4096 := read_mem_bytes 512 out_address final_state
 def final_hash : BitVec 128 := read_mem_bytes 16 Xi_address final_state
 def final_ivec : BitVec 128 := read_mem_bytes 16 ivec_address final_state
 
-example : final_state.error = StateError.None := by native_decide
+example : read_err final_state = StateError.None := by native_decide
 example : final_hash = revflat Xi_res := by native_decide
 example : final_ciphertext = revflat ciphertext := by native_decide
 example : final_ivec = revflat ivec_res := by native_decide
@@ -234,7 +234,7 @@ def final_ciphertext : BitVec 4096 := read_mem_bytes 512 out_address final_state
 def final_hash : BitVec 128 := read_mem_bytes 16 Xi_address final_state
 def final_ivec : BitVec 128 := read_mem_bytes 16 ivec_address final_state
 
-example : final_state.error = StateError.None := by native_decide
+example : read_err final_state = StateError.None := by native_decide
 example : final_hash = revflat Xi_res := by native_decide
 set_option maxRecDepth 2100 in
 example : final_ciphertext = revflat in_blocks := by native_decide
@@ -317,7 +317,7 @@ def final_ciphertext : BitVec 4096 := read_mem_bytes 512 out_address final_state
 def final_hash : BitVec 128 := read_mem_bytes 16 Xi_address final_state
 def final_ivec : BitVec 128 := read_mem_bytes 16 ivec_address final_state
 
-example : final_state.error = StateError.None := by native_decide
+example : read_err final_state = StateError.None := by native_decide
 example : final_hash = revflat Xi_res := by native_decide
 example : final_ciphertext = (revflat ciphertext) := by native_decide
 example : final_ivec = (revflat ivec_res) := by native_decide
@@ -335,7 +335,7 @@ def final_ciphertext : BitVec 4096 := read_mem_bytes 512 out_address final_state
 def final_hash : BitVec 128 := read_mem_bytes 16 Xi_address final_state
 def final_ivec : BitVec 128 := read_mem_bytes 16 ivec_address final_state
 
-example : final_state.error = StateError.None := by native_decide
+example : read_err final_state = StateError.None := by native_decide
 example : final_hash = revflat Xi_res := by native_decide
 set_option maxRecDepth 2100 in
 example : final_ciphertext = revflat in_blocks := by native_decide
@@ -421,7 +421,7 @@ def final_ciphertext : BitVec 4096 := read_mem_bytes 512 out_address final_state
 def final_hash : BitVec 128 := read_mem_bytes 16 Xi_address final_state
 def final_ivec : BitVec 128 := read_mem_bytes 16 ivec_address final_state
 
-example : final_state.error = StateError.None := by native_decide
+example : read_err final_state = StateError.None := by native_decide
 example : final_hash = revflat Xi_res := by native_decide
 example : final_ciphertext = revflat ciphertext := by native_decide
 example : final_ivec = (revflat ivec_res) := by native_decide
@@ -439,7 +439,7 @@ def final_ciphertext : BitVec 4096 := read_mem_bytes 512 out_address final_state
 def final_hash : BitVec 128 := read_mem_bytes 16 Xi_address final_state
 def final_ivec : BitVec 128 := read_mem_bytes 16 ivec_address final_state
 
-example : final_state.error = StateError.None := by native_decide
+example : read_err final_state = StateError.None := by native_decide
 example : final_hash = revflat Xi_res := by native_decide
 set_option maxRecDepth 2100 in
 example : final_ciphertext = revflat in_blocks := by native_decide
diff --git a/Tests/AES-GCM/AESV8ProgramTests.lean b/Tests/AES-GCM/AESV8ProgramTests.lean
index 968dbe7b..a60f6ba2 100644
--- a/Tests/AES-GCM/AESV8ProgramTests.lean
+++ b/Tests/AES-GCM/AESV8ProgramTests.lean
@@ -28,20 +28,20 @@ open BitVec
 --   Run test:
 --     1. aws-lc-build/crypto/crypto_test --gtest_filter="AESTest.ABI"
 
-/- 
+/-
   How to get the number of steps to run for a program?
 
-  When a program finishes, ArmState.pc would be set to 0x0#64 and ArmState.error
+  When a program finishes, ArmState.pc would be set to 0x0#64 and `read_err ArmState`
   will be `StateError.None`. If a program hasn't reached the last instruction,
   its ArmState.pc will be some number other than 0x0#64. This is based on an
   assumption that programs don't typically start at pc 0x0#64.
-  If a program runs past the last instruction, its ArmState.error will be:
+  If a program runs past the last instruction, `(read_err ArmState)` will be:
 
     StateError.NotFound "No instruction found at PC 0x0000000000000000#64!"
 
   Based on above information, we could do a binary search for the number of steps
   to run a program and the stopping criterion is that ArmState.pc = 0x0#64 and
-  ArmState.error = StateError.None. This sounds awfully programmable, but for
+  `read_err ArmState = StateError.None`. This sounds awfully programmable, but for
   now we reply on this comment.
 
 -/
@@ -113,7 +113,7 @@ def final_state : ArmState := aes_hw_set_encrypt_key_test 167 key_bits
 def final_rd_key : BitVec 1408 := read_mem_bytes 176 key_address final_state
 def final_rounds : BitVec 64 := read_mem_bytes 8 (key_address + 240) final_state
 
-example : final_state.error = StateError.None := by native_decide
+example : read_err final_state = StateError.None := by native_decide
 example : final_rd_key = revflat rd_key := by native_decide
 example : final_rounds = rounds := by native_decide
 
@@ -143,7 +143,7 @@ def final_state : ArmState := aes_hw_set_encrypt_key_test 195 key_bits
 def final_rd_key : BitVec 1664 := read_mem_bytes 208 key_address final_state
 def final_rounds : BitVec 64 := read_mem_bytes 8 (key_address + 240) final_state
 
-example : final_state.error = StateError.None := by native_decide
+example : read_err final_state = StateError.None := by native_decide
 example : final_rd_key = revflat rd_key := by native_decide
 example : final_rounds = rounds := by native_decide
 
@@ -175,7 +175,7 @@ def final_state : ArmState := aes_hw_set_encrypt_key_test 198 key_bits
 def final_rd_key : BitVec 1920 := read_mem_bytes 240 key_address final_state
 def final_rounds : BitVec 64 := read_mem_bytes 8 (key_address + 240) final_state
 
-example : final_state.error = StateError.None := by native_decide
+example : read_err final_state = StateError.None := by native_decide
 example : final_rd_key = revflat rd_key := by native_decide
 example : final_rounds = rounds := by native_decide
 
@@ -231,7 +231,7 @@ def final_state : ArmState :=
   aes_hw_encrypt_test 44 (revflat in_block) rounds (revflat key_schedule)
 def final_ciphertext : BitVec 128 := read_mem_bytes 16 out_address final_state
 
-example : final_state.error = StateError.None := by native_decide
+example : read_err final_state = StateError.None := by native_decide
 example : final_ciphertext = revflat out_block := by native_decide
 
 end AES128
@@ -254,7 +254,7 @@ def final_state : ArmState :=
   aes_hw_encrypt_test 52 (revflat in_block) rounds (revflat key_schedule)
 def final_ciphertext : BitVec 128 := read_mem_bytes 16 out_address final_state
 
-example : final_state.error = StateError.None := by native_decide
+example : read_err final_state = StateError.None := by native_decide
 example : final_ciphertext = revflat out_block := by native_decide
 
 
@@ -276,7 +276,7 @@ def final_state : ArmState :=
   aes_hw_encrypt_test 60 (revflat in_block) rounds (revflat key_schedule)
 def final_ciphertext : BitVec 128 := read_mem_bytes 16 out_address final_state
 
-example : final_state.error = StateError.None := by native_decide
+example : read_err final_state = StateError.None := by native_decide
 example : final_ciphertext = revflat out_block := by native_decide
 
 
@@ -355,42 +355,42 @@ def buf_res_128 : List (BitVec 8) :=
 def final_state0 : ArmState :=
   aes_hw_ctr32_encrypt_blocks_test 83 0 in_block rounds key_schedule ivec
 def final_buf0 : BitVec 640 := read_mem_bytes 80 out_address final_state0
-example : final_state0.error = StateError.None := by native_decide
+example : read_err final_state0 = StateError.None := by native_decide
 example: final_buf0 = (BitVec.zero 384) ++ (extractLsb 255 0 (revflat buf_res_128)) := by native_decide
 
 -- len = 1
 def final_state1 : ArmState :=
   aes_hw_ctr32_encrypt_blocks_test 82 1 in_block rounds key_schedule ivec
 def final_buf1 : BitVec 640 := read_mem_bytes 80 out_address final_state1
-example : final_state1.error = StateError.None := by native_decide
+example : read_err final_state1 = StateError.None := by native_decide
 example: final_buf1 = (BitVec.zero 512) ++ (extractLsb 127 0 (revflat buf_res_128)) := by native_decide
 
 -- -- len = 2
 def final_state2 : ArmState :=
   aes_hw_ctr32_encrypt_blocks_test 82 2 in_block rounds key_schedule ivec
 def final_buf2 : BitVec 640 := read_mem_bytes 80 out_address final_state2
-example : final_state2.error = StateError.None := by native_decide
+example : read_err final_state2 = StateError.None := by native_decide
 example: final_buf2 = (BitVec.zero 384) ++ (extractLsb 255 0 (revflat buf_res_128)) := by native_decide
 
 -- len = 3
 def final_state3 : ArmState :=
   aes_hw_ctr32_encrypt_blocks_test 129 3 in_block rounds key_schedule ivec
 def final_buf3 : BitVec 640 := read_mem_bytes 80 out_address final_state3
-example : final_state3.error = StateError.None := by native_decide
+example : read_err final_state3 = StateError.None := by native_decide
 example: final_buf3 = (BitVec.zero 256) ++ (extractLsb 383 0 (revflat buf_res_128)) := by native_decide
 
 -- len = 4
 def final_state4 : ArmState :=
   aes_hw_ctr32_encrypt_blocks_test 187 4 in_block rounds key_schedule ivec
 def final_buf4 : BitVec 640 := read_mem_bytes 80 out_address final_state4
-example : final_state4.error = StateError.None := by native_decide
+example : read_err final_state4 = StateError.None := by native_decide
 example: final_buf4 = (BitVec.zero 127) ++ (extractLsb 512 0 (revflat buf_res_128)) := by native_decide
 
 -- len = 5
 def final_state5 : ArmState :=
   aes_hw_ctr32_encrypt_blocks_test 188 5 in_block rounds key_schedule ivec
 def final_buf5 : BitVec 640 := read_mem_bytes 80 out_address final_state5
-example : final_state5.error = StateError.None := by native_decide
+example : read_err final_state5 = StateError.None := by native_decide
 example: final_buf5 = revflat buf_res_128 := by native_decide
 
 end AES128Ctr32
@@ -416,7 +416,7 @@ def buf_res_192 : List (BitVec 8) :=
 def final_state : ArmState :=
   aes_hw_ctr32_encrypt_blocks_test 216 5 in_block rounds key_schedule ivec
 def final_buf : BitVec 640 := read_mem_bytes 80 out_address final_state
-example : final_state.error = StateError.None := by native_decide
+example : read_err final_state = StateError.None := by native_decide
 example: final_buf = revflat buf_res_192 := by native_decide
 
 end AES192Ctr32
@@ -442,7 +442,7 @@ def buf_res_256 : List (BitVec 8) :=
 def final_state : ArmState :=
   aes_hw_ctr32_encrypt_blocks_test 244 5 in_block rounds key_schedule ivec
 def final_buf : BitVec 640 := read_mem_bytes 80 out_address final_state
-example : final_state.error = StateError.None := by native_decide
+example : read_err final_state = StateError.None := by native_decide
 example: final_buf = revflat buf_res_256 := by native_decide
 
 end AES256Ctr32
diff --git a/Tests/AES-GCM/GCMProgramTests.lean b/Tests/AES-GCM/GCMProgramTests.lean
index fe3e2fba..c12464e9 100644
--- a/Tests/AES-GCM/GCMProgramTests.lean
+++ b/Tests/AES-GCM/GCMProgramTests.lean
@@ -130,10 +130,10 @@ def init_gcm_init_test : ArmState :=
   s
 
 def final_state : ArmState := run GCMInitV8Program.gcm_init_v8_program.length init_gcm_init_test
-def final_pc : BitVec 64 := final_state.pc
+def final_pc : BitVec 64 := read_pc final_state
 def final_table : BitVec 2048 := read_mem_bytes 256 Htable_address final_state
 example : final_table = revflat Htable := by native_decide
-example : final_state.error = StateError.None := by native_decide
+example : read_err final_state = StateError.None := by native_decide
 
 end GCMInitV8ProgramTest
 
@@ -171,7 +171,7 @@ def gcm_gmult_final_state : ArmState :=
 def final_hash : BitVec 128 := read_mem_bytes 16 x_address gcm_gmult_final_state
 
 example : final_hash = revflat X_after := by native_decide
-example : gcm_gmult_final_state.error = StateError.None := by native_decide
+example : read_err gcm_gmult_final_state = StateError.None := by native_decide
 
 end GCMGmultV8ProgramTest
 
@@ -218,7 +218,7 @@ def final_state : ArmState :=
 def final_hash : BitVec 128 := read_mem_bytes 16 x_address final_state
 
 example : final_hash = revflat X_after := by native_decide
-example : final_state.error = StateError.None := by native_decide
+example : read_err final_state = StateError.None := by native_decide
 
 end block2
 
@@ -234,7 +234,7 @@ def final_state : ArmState :=
 def final_hash : BitVec 128 := read_mem_bytes 16 x_address final_state
 
 example : final_hash = revflat X_after := by native_decide
-example : final_state.error = StateError.None := by native_decide
+example : read_err final_state = StateError.None := by native_decide
 
 end block4
 
@@ -250,7 +250,7 @@ def final_state : ArmState :=
 def final_hash : BitVec 128 := read_mem_bytes 16 x_address final_state
 
 example : final_hash = revflat X_after := by native_decide
-example : final_state.error = StateError.None := by native_decide
+example : read_err final_state = StateError.None := by native_decide
 
 end block5
 
@@ -266,7 +266,7 @@ def final_state : ArmState :=
 def final_hash : BitVec 128 := read_mem_bytes 16 x_address final_state
 
 example : final_hash = revflat X_after := by native_decide
-example : final_state.error = StateError.None := by native_decide
+example : read_err final_state = StateError.None := by native_decide
 
 end block6
 
@@ -282,7 +282,7 @@ def final_state : ArmState :=
 def final_hash : BitVec 128 := read_mem_bytes 16 x_address final_state
 
 example : final_hash = revflat X_after := by native_decide
-example : final_state.error = StateError.None := by native_decide
+example : read_err final_state = StateError.None := by native_decide
 
 end block7
 
diff --git a/Tests/LDSTTest.lean b/Tests/LDSTTest.lean
index a32e3993..d9911a3d 100644
--- a/Tests/LDSTTest.lean
+++ b/Tests/LDSTTest.lean
@@ -38,7 +38,7 @@ def ldr_gpr_unsigned_offset_state : ArmState :=
 def ldr_gpr_unsigned_offset_final_state : ArmState := run 1 ldr_gpr_unsigned_offset_state
 
 example : (read_gpr 64 0#5 ldr_gpr_unsigned_offset_final_state) = 20#64 := by native_decide
-example : ldr_gpr_unsigned_offset_final_state.pc = 4#64 := by native_decide
+example : read_pc ldr_gpr_unsigned_offset_final_state = 4#64 := by native_decide
 
 ----------------------------------------------------------------------
 -- test str, 64-bit gpr, post-index
@@ -56,7 +56,7 @@ def str_gpr_post_index_final_state : ArmState := run 1 str_gpr_post_index_state
 
 example : (read_gpr 64 1#5 str_gpr_post_index_final_state) = 3#64 := by native_decide
 example : (read_mem_bytes 8 0#64 str_gpr_post_index_final_state) = 20#64 := by native_decide
-example : str_gpr_post_index_final_state.pc = 4#64 := by native_decide
+example : read_pc str_gpr_post_index_final_state = 4#64 := by native_decide
 
 ----------------------------------------------------------------------
 -- test ldr, 64-bit sfp, post-index
@@ -94,7 +94,7 @@ def ldrb_unsigned_offset : Program :=
 def ldrb_unsigned_offset_state: ArmState :=
   let s := set_init_state ldrb_unsigned_offset
   write_mem_bytes 1 4#64 20#8 s
-  
+
 def ldrb_unsigned_offset_final_state : ArmState := run 1 ldrb_unsigned_offset_state
 
 example : (read_gpr 64 0#5 ldrb_unsigned_offset_final_state) = 20#64 := by native_decide
diff --git a/Tests/SHA2/SHA512ProgramTest.lean b/Tests/SHA2/SHA512ProgramTest.lean
index 2bb82107..3979af57 100644
--- a/Tests/SHA2/SHA512ProgramTest.lean
+++ b/Tests/SHA2/SHA512ProgramTest.lean
@@ -609,7 +609,7 @@ def init_sha512_test : ArmState :=
 -- #eval (log_run "Tests/SHA512_PC.log" pc_trace 503 init_sha512_test)
 
 def final_sha512_state : ArmState := run 503 init_sha512_test
-def final_sha512_pc : BitVec 64 := final_sha512_state.pc
+def final_sha512_pc : BitVec 64 := read_pc final_sha512_state
 
 -- read_mem_bytes below with (512/8) as the first arg. causes a
 -- "maximum recursion depth has been reached" error, but that worked