Files reorganization

Arm/Decode/BR.lean

@@ -3,7 +3,7 @@ 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, Yan Peng
 -/
-import Arm.BitVec
+import Data.BitVec
 
 ------------------------------------------------------------------------------
 

Arm/Decode/DPI.lean

@@ -3,7 +3,7 @@ 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.BitVec
+import Data.BitVec
 
 ------------------------------------------------------------------------------
 

Arm/Decode/DPR.lean

@@ -3,7 +3,7 @@ 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, Yan Peng
 -/
-import Arm.BitVec
+import Data.BitVec
 
 ------------------------------------------------------------------------------
 

Arm/Decode/DPSFP.lean

@@ -3,7 +3,7 @@ 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.BitVec
+import Data.BitVec
 
 ------------------------------------------------------------------------------
 

Arm/Decode/LDST.lean

@@ -3,7 +3,7 @@ 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, Yan Peng
 -/
-import Arm.BitVec
+import Data.BitVec
 
 ------------------------------------------------------------------------------
 

Arm/Exec.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.BitVec
 import Arm.Decode
 import Arm.Insts
 

Arm/Insts/BR/Compare_branch.lean

@@ -9,7 +9,6 @@ Author(s): Shilpi Goel
 import Arm.Decode
 import Arm.State
 import Arm.Insts.Common
-import Arm.BitVec
 
 namespace BR
 

Arm/Insts/BR/Cond_branch_imm.lean

@@ -9,7 +9,6 @@ Author(s): Yan Peng
 import Arm.Decode
 import Arm.State
 import Arm.Insts.Common
-import Arm.BitVec
 
 namespace BR
 

Arm/Insts/BR/Uncond_branch_imm.lean

@@ -9,7 +9,6 @@ Author(s): Shilpi Goel
 import Arm.Decode
 import Arm.State
 import Arm.Insts.Common
-import Arm.BitVec
 
 namespace BR
 

Arm/Insts/BR/Uncond_branch_reg.lean

@@ -9,7 +9,6 @@ Author(s): Shilpi Goel
 import Arm.Decode
 import Arm.State
 import Arm.Insts.Common
-import Arm.BitVec
 
 namespace BR
 

Arm/Insts/Common.lean

@@ -5,7 +5,6 @@ Author(s): Shilpi Goel, Yan Peng, Nathan Wetzler
 -/
 
 import LeanSAT
-import Arm.BitVec
 import Arm.State
 
 section Common

Arm/Insts/DPI/PC_rel_addressing.lean

@@ -8,7 +8,6 @@ Author(s): Shilpi Goel
 import Arm.Decode
 import Arm.State
 import Arm.Insts.Common
-import Arm.BitVec
 
 namespace DPI
 

Arm/Insts/DPR/Conditional_select.lean

@@ -8,7 +8,6 @@ Author(s): Shilpi Goel
 import Arm.Decode
 import Arm.State
 import Arm.Insts.Common
-import Arm.BitVec
 
 namespace DPR
 

Arm/Insts/DPSFP/Advanced_simd_copy.lean

@@ -7,7 +7,6 @@ Author(s): Yan Peng
 
 import Arm.Decode
 import Arm.Insts.Common
-import Arm.BitVec
 
 ----------------------------------------------------------------------
 

Arm/Insts/DPSFP/Advanced_simd_extract.lean

@@ -8,7 +8,6 @@ Author(s): Shilpi Goel
 import Arm.Decode
 import Arm.State
 import Arm.Insts.Common
-import Arm.BitVec
 
 ----------------------------------------------------------------------
 

Arm/Insts/DPSFP/Advanced_simd_modified_immediate.lean

@@ -8,7 +8,6 @@ Author(s): Yan Peng
 
 import Arm.Decode
 import Arm.Insts.Common
-import Arm.BitVec
 
 ----------------------------------------------------------------------
 

Arm/Insts/DPSFP/Advanced_simd_scalar_copy.lean

@@ -7,7 +7,6 @@ Author(s): Yan Peng
 
 import Arm.Decode
 import Arm.Insts.Common
-import Arm.BitVec
 
 ----------------------------------------------------------------------
 

Arm/Insts/DPSFP/Advanced_simd_three_same.lean

@@ -8,7 +8,6 @@ Author(s): Shilpi Goel, Yan Peng
 import Arm.Decode
 import Arm.State
 import Arm.Insts.Common
-import Arm.BitVec
 
 ----------------------------------------------------------------------
 

Arm/Insts/DPSFP/Advanced_simd_two_reg_misc.lean

@@ -8,7 +8,6 @@ Author(s): Shilpi Goel
 import Arm.Decode
 import Arm.State
 import Arm.Insts.Common
-import Arm.BitVec
 
 ----------------------------------------------------------------------
 

Arm/Insts/DPSFP/Conversion_between_FP_and_Int.lean

@@ -7,7 +7,6 @@ Author(s): Yan Peng
 
 import Arm.Decode
 import Arm.Insts.Common
-import Arm.BitVec
 
 ----------------------------------------------------------------------
 

Arm/Insts/DPSFP/Crypto_aes.lean

@@ -7,7 +7,6 @@ Author(s): Shilpi Goel, Yan Peng
 
 import Arm.Decode
 import Arm.Insts.Common
-import Arm.BitVec
 import Specs.AESCommon
 
 ----------------------------------------------------------------------

Arm/Insts/DPSFP/Crypto_four_reg.lean

@@ -8,7 +8,6 @@ Author(s): Shilpi Goel, Nevine Ebeid
 import Arm.Decode
 import Arm.State
 import Arm.Insts.Common
-import Arm.BitVec
 
 ----------------------------------------------------------------------
 

Arm/Insts/DPSFP/Crypto_three_reg_sha512.lean

@@ -8,7 +8,6 @@ Author(s): Shilpi Goel
 import Arm.Decode
 import Arm.State
 import Arm.Insts.Common
-import Arm.BitVec
 import Specs.SHA512Common
 
 ----------------------------------------------------------------------

Arm/State.lean

@@ -4,10 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 import Lean.Data.Format
-import Arm.BitVec
-import Arm.Map
-import Arm.Attr
-import Arm.MinTheory
+import Data.BitVec
+import Data.Map
+import Data.MinTheory
+import Data.Attr
 
 ------------------------------------------------------------------------------
 ------------------------------------------------------------------------------

Data/Attr.lean

@@ -0,0 +1,9 @@
+import Lean
+
+-- A minimal theory, safe for all LNSym proofs
+register_simp_attr minimal_theory
+-- Non-interference lemmas for simplifying terms involving state
+-- accessors and updaters.
+register_simp_attr state_simp_rules
+-- Rules for bitvector lemmas
+register_simp_attr bitvec_rules

Arm/BitVec.lean → Data/BitVec.lean

@@ -8,7 +8,7 @@ Author(s): Shilpi Goel
 
 ----------------------------------------------------------------------
 
-import Arm.Attr
+import Data.Attr
 
 namespace BitVec
 
@@ -261,6 +261,11 @@ protected def flatten {n : Nat} (xs : List (BitVec n)) : BitVec (n * xs.length)
       omega
     BitVec.cast h (x ++ (BitVec.flatten rest))
 
+/-- Reverse `x` and then flatten it. -/
+def revflat (x : List (BitVec n)) : BitVec (n * x.length) := 
+  have h : n * x.reverse.length = n * x.length := by simp only [List.length_reverse]
+  BitVec.cast h $ BitVec.flatten (List.reverse x)
+
 /-- Generate a random bitvector of width n. The range of the values
 can also be specified using lo and hi arguments, which default to 0
 and 2^n - 1 (inclusive), respectively. -/

Arm/MinTheory.lean → Data/MinTheory.lean

@@ -1,6 +1,14 @@
-import Arm.Attr
+/-
+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
+-/
 
--- These lemmas are from lean/Init/SimpLemmas.lean.
+-- A minimal theory, safe for all LNSym proofs
+
+import Data.Attr
+
+-- Source: lean/Init/SimpLemmas.lean.
 attribute [minimal_theory] eq_self
 attribute [minimal_theory] ne_eq
 attribute [minimal_theory] ite_true

Proofs/Experiments/Max.lean

@@ -6,7 +6,6 @@ Author(s): Shilpi Goel, Siddharth Bhat
 The goal is to prove that this program implements max correctly.
 -/
 import Arm
-import Arm.BitVec
 
 namespace Max
 

Proofs/MultiInsts.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 import Arm.Exec
-import Arm.Util
 import Tactics.Sym
 
 namespace multi_insts_proofs

Proofs/Popcount32.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Nathan Wetzler
 -/
 import Arm.Exec
-import Arm.Util
 import Tactics.Sym
 import Tactics.StepThms
 

Proofs/SHA512/Sha512Sym.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 import Arm.Exec
-import Arm.Util
 import Tactics.Sym
 import Proofs.SHA512.Sha512StepLemmas
 import Lean