chore: Make ArmState fields private to ensure that every field access…

… is written in terms of r/w and read/write_mem_bytes (#51) This cleans up our definitions, and forces us to correctly the `read_*` and `write_*` methods. This is important to allow us to reduce all (non)interference reasoning into the `r/w` functions. --------- Co-authored-by: Shilpi Goel <[email protected]>
leanprover · Aug 2, 2024 · 453e343 · 453e343
1 parent 8879666
commit 453e343
Show file tree

Hide file tree

Showing 27 changed files with 213 additions and 215 deletions.
diff --git 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,15 +128,15 @@ 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
 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
diff --git 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
@@ -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
 
 ----------------------------------------------------------------------