Updates to sym_one tactic

Eliding use of `update_invariants` for now.
leanprover · Mar 3, 2024 · aafe462 · aafe462
1 parent d2bd408
commit aafe462
Show file tree

Hide file tree

Showing 38 changed files with 299 additions and 799 deletions.
diff --git a/Arm/Attr.lean b/Arm/Attr.lean
@@ -1,9 +1,14 @@
 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
 
+/-
 syntax "state_simp" : tactic
 macro_rules
   | `(tactic| state_simp) => `(tactic| simp only [state_simp_rules])
@@ -19,3 +24,4 @@ macro_rules
 syntax "state_simp_all?" : tactic
 macro_rules
   | `(tactic| state_simp_all?) => `(tactic| simp_all? only [state_simp_rules])
+-/
diff --git a/Arm/BitVec.lean b/Arm/BitVec.lean
@@ -8,10 +8,20 @@ Author(s): Shilpi Goel
 
 ----------------------------------------------------------------------
 
+import Arm.Attr
+
 namespace BitVec
 
 open BitVec
 
+-- Adding some useful simp lemmas to `bitvec_rules`:
+attribute [bitvec_rules] BitVec.ofFin_eq_ofNat
+attribute [minimal_theory] BitVec.extractLsb_ofFin
+attribute [minimal_theory] zeroExtend_eq 
+attribute [minimal_theory] add_ofFin
+attribute [minimal_theory] ofFin.injEq 
+attribute [minimal_theory] Fin.mk.injEq
+
 ----------------------------------------------------------------------
 -- Some BitVec definitions
 

diff --git a/Arm/Exec.lean b/Arm/Exec.lean
@@ -112,7 +112,6 @@ def run (n : Nat) (s : ArmState) : ArmState :=
     let s' := stepi s
     run n' s'
 
-@[simp]
 theorem run_opener_zero (s : ArmState) :
   run 0 s = s := by
   rfl
@@ -128,7 +127,7 @@ theorem run_opener_general
 theorem run_plus (n1 : Nat) (n2 : Nat) (s : ArmState) :
   run (n1 + n2) s = run n2 (run n1 s) := by
   induction n1 generalizing s with
-  | zero => simp
+  | zero => simp only [run_opener_zero, minimal_theory]
   | succ n n_ih =>
     simp [run_opener_general]
     conv =>
@@ -140,3 +139,11 @@ theorem run_plus (n1 : Nat) (n2 : Nat) (s : ArmState) :
       unfold run
     simp
     exact n_ih (stepi s)
+
+
+theorem run_onestep (s s': ArmState) (n : Nat) (h_nonneg : 0 < n):
+  (s' = run n s) ↔ ∃ s'', s'' = stepi s ∧ s' = run (n-1) s'' := by
+  cases n
+  · cases h_nonneg
+  · rename_i n
+    simp [run]
diff --git a/Arm/Insts/BR/Compare_branch.lean b/Arm/Insts/BR/Compare_branch.lean
@@ -19,13 +19,13 @@ open BitVec
 -- Compare_branch_inst.condition_holds are also used in control-flow
 -- analysis; see Arm/Cfg/Cfg.lean.
 
-@[simp]
+@[state_simp_rules]
 def Compare_branch_inst.branch_taken_pc (inst : Compare_branch_inst) (pc : BitVec 64) : BitVec 64 :=
   let offset := signExtend 64 (inst.imm19 <<< 2)
   let branch_taken_pc := pc + offset
   branch_taken_pc
 
-@[simp]
+@[state_simp_rules]
 def Compare_branch_inst.condition_holds (inst : Compare_branch_inst) (s : ArmState) : Bool :=
   let datasize := if inst.sf = 1#1 then 64 else 32
   let operand1 := read_gpr datasize inst.Rt s
@@ -37,7 +37,7 @@ def Compare_branch_inst.condition_holds (inst : Compare_branch_inst) (s : ArmSta
     -- CBNZ
     (not operand1_is_zero)
 
-@[simp]
+@[state_simp_rules]
 def exec_compare_branch (inst : Compare_branch_inst) (s : ArmState) : ArmState :=
     let orig_pc := read_pc s
     let branch_taken := Compare_branch_inst.condition_holds inst s

diff --git a/Arm/Insts/BR/Cond_branch_imm.lean b/Arm/Insts/BR/Cond_branch_imm.lean
@@ -15,12 +15,12 @@ namespace BR
 
 open BitVec
 
-@[simp]
+@[state_simp_rules]
 def Cond_branch_imm_inst.branch_taken_pc (inst : Cond_branch_imm_inst) (pc : BitVec 64) : BitVec 64 :=
   let offset := signExtend 64 (inst.imm19 <<< 2)
   pc + offset
 
-@[simp]
+@[state_simp_rules]
 def Cond_branch_imm_inst.condition_holds (inst : Cond_branch_imm_inst) (s : ArmState): Bool :=
   let Z := read_store PFlag.Z s.pstate
   let C := read_store PFlag.C s.pstate
@@ -42,7 +42,7 @@ def Cond_branch_imm_inst.condition_holds (inst : Cond_branch_imm_inst) (s : ArmS
     else result
   result
 
-@[simp]
+@[state_simp_rules]
 def exec_cond_branch_imm (inst : Cond_branch_imm_inst) (s : ArmState)
   : ArmState :=
   let orig_pc := read_pc s

diff --git a/Arm/Insts/BR/Uncond_branch_imm.lean b/Arm/Insts/BR/Uncond_branch_imm.lean
@@ -15,12 +15,12 @@ namespace BR
 
 open BitVec
 
-@[simp]
+@[state_simp_rules]
 def Uncond_branch_imm_inst.branch_taken_pc (inst : Uncond_branch_imm_inst) (pc : BitVec 64) : BitVec 64 :=
   let offset := signExtend 64 (inst.imm26 <<< 2)
   pc + offset
 
-@[simp]
+@[state_simp_rules]
 def exec_uncond_branch_imm (inst : Uncond_branch_imm_inst) (s : ArmState) : ArmState :=
     let orig_pc := read_pc s
     let next_pc := Uncond_branch_imm_inst.branch_taken_pc inst orig_pc

diff --git a/Arm/Insts/BR/Uncond_branch_reg.lean b/Arm/Insts/BR/Uncond_branch_reg.lean
@@ -17,7 +17,7 @@ open BitVec
 
 -- (FIXME) Extend Cfg.addToGraphs when more instructions in this
 -- category are implemented.
-@[simp]
+@[state_simp_rules]
 def exec_uncond_branch_reg (inst : Uncond_branch_reg_inst) (s : ArmState) : ArmState :=
     -- Only RET is implemented.
     if not (inst.opc == 0b0010#4 && inst.op2 = 0b11111#5 && 

diff --git a/Arm/Insts/Common.lean b/Arm/Insts/Common.lean
@@ -134,9 +134,6 @@ def invalid_bit_masks (immN : BitVec 1) (imms : BitVec 6) (immediate : Bool)
         let esize := 1 <<< len
         if esize * (M / esize) ≠ M then true else false
 
-theorem option_get_bang_of_some [Inhabited α] (v : α) :
-  Option.get! (some v) = v := by rfl
-
 theorem M_divisible_by_esize_of_valid_bit_masks (immN : BitVec 1) (imms : BitVec 6)
   (immediate : Bool) (M : Nat):
   ¬ invalid_bit_masks immN imms immediate M →
@@ -196,7 +193,7 @@ instance : ToString SIMDThreeSameLogicalType where toString a := toString (repr
 
 ----------------------------------------------------------------------
 
-@[simp]
+@[state_simp_rules]
 def Vpart_read (n : BitVec 5) (part width : Nat) (s : ArmState) (H : width > 0)
   : BitVec width :=
   -- assert n >= 0 && n <= 31;
@@ -211,7 +208,7 @@ def Vpart_read (n : BitVec 5) (part width : Nat) (s : ArmState) (H : width > 0)
     h2 ▸ extractLsb (width*2-1) width $ read_sfp 128 n s
 
 
-@[simp]
+@[state_simp_rules]
 def Vpart_write (n : BitVec 5) (part width : Nat) (val : BitVec width) (s : ArmState)
   : ArmState :=
   -- assert n >= 0 && n <= 31;
@@ -226,12 +223,12 @@ def Vpart_write (n : BitVec 5) (part width : Nat) (val : BitVec width) (s : ArmS
 
 ----------------------------------------------------------------------
 
-@[simp]
+@[state_simp_rules]
 def ldst_read (SIMD? : Bool) (width : Nat) (idx : BitVec 5) (s : ArmState)
   : BitVec width :=
   if SIMD? then read_sfp width idx s else read_gpr width idx s
 
-@[simp]
+@[state_simp_rules]
 def ldst_write (SIMD? : Bool) (width : Nat) (idx : BitVec 5) (val : BitVec width) (s : ArmState)
   : ArmState :=
   if SIMD? then write_sfp width idx val s else write_gpr width idx val s

diff --git a/Arm/Insts/DPI/Add_sub_imm.lean b/Arm/Insts/DPI/Add_sub_imm.lean
@@ -12,7 +12,7 @@ namespace DPI
 
 open BitVec
 
-@[simp]
+@[state_simp_rules]
 def exec_add_sub_imm (inst : Add_sub_imm_cls) (s : ArmState) : ArmState :=
     let sub_op        := inst.op == 1#1
     let setflags      := inst.S == 1#1

diff --git a/Arm/Insts/DPI/Bitfield.lean b/Arm/Insts/DPI/Bitfield.lean
@@ -13,7 +13,7 @@ namespace DPI
 
 open BitVec
 
-@[simp]
+@[state_simp_rules]
 def exec_bitfield (inst: Bitfield_cls) (s : ArmState) : ArmState :=
   if inst.opc != 0b10#2 then
     write_err (StateError.Unimplemented s!"Unsupported {inst} encountered!") s

diff --git a/Arm/Insts/DPI/Logical_imm.lean b/Arm/Insts/DPI/Logical_imm.lean
@@ -37,7 +37,7 @@ def exec_logical_imm_op (op : LogicalImmType) (op1 : BitVec n) (op2 : BitVec n)
     let result := op1 &&& op2
     (op1 &&& op2, some (update_logical_imm_pstate result))
 
-@[simp]
+@[state_simp_rules]
 def exec_logical_imm (inst : Logical_imm_cls) (s : ArmState) : ArmState :=
   if inst.sf = 0#1 ∧ inst.N ≠ 0 then
     write_err (StateError.Illegal s!"Illegal {inst} encountered!") s

diff --git a/Arm/Insts/DPI/PC_rel_addressing.lean b/Arm/Insts/DPI/PC_rel_addressing.lean
@@ -14,7 +14,7 @@ namespace DPI
 
 open BitVec
 
-@[simp]
+@[state_simp_rules]
 def exec_pc_rel_addressing (inst : PC_rel_addressing_cls) (s : ArmState) : ArmState :=
   let orig_pc := read_pc s
   let imm := if inst.op = 0#1 then

diff --git a/Arm/Insts/DPR/Add_sub_carry.lean b/Arm/Insts/DPR/Add_sub_carry.lean
@@ -12,7 +12,7 @@ namespace DPR
 
 open BitVec
 
-@[simp]
+@[state_simp_rules]
 def exec_add_sub_carry (inst : Add_sub_carry_cls) (s : ArmState) : ArmState :=
     let sub_op        := inst.op == 1#1
     let setflags      := inst.S == 1#1

diff --git a/Arm/Insts/DPR/Add_sub_shifted_reg.lean b/Arm/Insts/DPR/Add_sub_shifted_reg.lean
@@ -12,7 +12,7 @@ namespace DPR
 
 open BitVec
 
-@[simp]
+@[state_simp_rules]
 def exec_add_sub_shifted_reg (inst : Add_sub_shifted_reg_cls) (s : ArmState) : ArmState :=
   let datasize := 32 <<< inst.sf.toNat
   if inst.shift == 0b11#2 then

diff --git a/Arm/Insts/DPR/Conditional_select.lean b/Arm/Insts/DPR/Conditional_select.lean
@@ -14,7 +14,7 @@ namespace DPR
 
 open BitVec
 
-@[simp]
+@[state_simp_rules]
 def exec_conditional_select (inst : Conditional_select_cls) (s : ArmState) : ArmState :=
     let datasize := if inst.sf = 1#1 then 64 else 32
     let (unimplemented, result) :=

diff --git a/Arm/Insts/DPR/Data_processing_one_source.lean b/Arm/Insts/DPR/Data_processing_one_source.lean
@@ -51,7 +51,7 @@ private theorem opc_and_sf_constraint (x : BitVec 2) (y : BitVec 1)
   have h₁ : 3 < 2 ^ 2 := by decide
   simp [h₁]
 
-@[simp]
+@[state_simp_rules]
 def exec_data_processing_rev
   (inst : Data_processing_one_source_cls) (s : ArmState) : ArmState :=
   have H₀: 1 - 0 + 1 = 2 := by decide
@@ -86,7 +86,7 @@ def exec_data_processing_rev
     let s := write_pc ((read_pc s) + 4#64) s
     s
 
-@[simp]
+@[state_simp_rules]
 def exec_data_processing_one_source
   (inst : Data_processing_one_source_cls) (s : ArmState) : ArmState :=
   match inst.sf, inst.S, inst.opcode2, inst.opcode with

diff --git a/Arm/Insts/DPR/Logical_shifted_reg.lean b/Arm/Insts/DPR/Logical_shifted_reg.lean
@@ -47,7 +47,7 @@ def exec_logical_shifted_reg_op (op : LogicalShiftedRegType) (opd1 : BitVec n) (
     let result := opd1 &&& ~~~opd2
     (result, some (logical_shifted_reg_update_pstate result))
 
-@[simp]
+@[state_simp_rules]
 def exec_logical_shifted_reg (inst : Logical_shifted_reg_cls) (s : ArmState) : ArmState :=
   if inst.sf = 0#1 ∧ inst.imm6 &&& 32 ≠ 0 then
     write_err (StateError.Illegal s!"Illegal {inst} encountered!") s

diff --git a/Arm/Insts/DPSFP/Advanced_simd_copy.lean b/Arm/Insts/DPSFP/Advanced_simd_copy.lean
@@ -134,7 +134,7 @@ def exec_smov_umov (inst : Advanced_simd_copy_cls) (s : ArmState) (signed : Bool
     let s := write_gpr datasize inst.Rd result s
     s
 
-@[simp]
+@[state_simp_rules]
 def exec_advanced_simd_copy
   (inst : Advanced_simd_copy_cls) (s : ArmState) : ArmState :=
   match_bv inst.Q ++ inst.op ++ inst.imm5 ++ inst.imm4 with

diff --git a/Arm/Insts/DPSFP/Advanced_simd_extract.lean b/Arm/Insts/DPSFP/Advanced_simd_extract.lean
@@ -16,7 +16,7 @@ namespace DPSFP
 
 open BitVec
 
-@[simp]
+@[state_simp_rules]
 def exec_advanced_simd_extract
   (inst : Advanced_simd_extract_cls) (s : ArmState) : ArmState :=
   open BitVec in

diff --git a/Arm/Insts/DPSFP/Advanced_simd_modified_immediate.lean b/Arm/Insts/DPSFP/Advanced_simd_modified_immediate.lean
@@ -87,7 +87,7 @@ private theorem mul_div_norm_form_lemma  (n m : Nat) (_h1 : 0 < m) (h2 : n ∣ m
   rw [Nat.mul_div_assoc]
   simp only [h2]
 
-@[simp]
+@[state_simp_rules]
 -- Assumes CheckFPAdvSIMDEnabled64();
 def exec_advanced_simd_modified_immediate
   (inst : Advanced_simd_modified_immediate_cls) (s : ArmState) : ArmState :=

diff --git a/Arm/Insts/DPSFP/Advanced_simd_scalar_copy.lean b/Arm/Insts/DPSFP/Advanced_simd_scalar_copy.lean
@@ -15,7 +15,7 @@ namespace DPSFP
 
 open BitVec
 
-@[simp]
+@[state_simp_rules]
 def exec_advanced_simd_scalar_copy
   (inst : Advanced_simd_scalar_copy_cls) (s : ArmState) : ArmState :=
   let size := lowest_set_bit inst.imm5

diff --git a/Arm/Insts/DPSFP/Advanced_simd_three_different.lean b/Arm/Insts/DPSFP/Advanced_simd_three_different.lean
@@ -50,7 +50,7 @@ def pmull_op (e : Nat) (esize : Nat) (elements : Nat) (x : BitVec n)
     pmull_op (e + 1) esize elements x y result H
   termination_by (elements - e)
 
-@[simp]
+@[state_simp_rules]
 def exec_pmull (inst : Advanced_simd_three_different_cls) (s : ArmState) : ArmState :=
   -- This function assumes IsFeatureImplemented(FEAT_PMULL) is true
   if inst.size == 0b01#2 || inst.size == 0b10#2 then
@@ -70,7 +70,7 @@ def exec_pmull (inst : Advanced_simd_three_different_cls) (s : ArmState) : ArmSt
     let s := write_pc ((read_pc s) + 4#64) s
     s
 
-@[simp]
+@[state_simp_rules]
 def exec_advanced_simd_three_different
   (inst : Advanced_simd_three_different_cls) (s : ArmState) : ArmState :=
   match inst.U, inst.opcode with

diff --git a/Arm/Insts/DPSFP/Advanced_simd_three_same.lean b/Arm/Insts/DPSFP/Advanced_simd_three_same.lean
@@ -38,12 +38,12 @@ def binary_vector_op_aux (e : Nat) (elems : Nat) (esize : Nat)
 /--
   Perform pairwise op on esize-bit slices of x and y
 -/
-@[simp]
+@[state_simp_rules]
 def binary_vector_op (esize : Nat) (op : BitVec esize → BitVec esize → BitVec esize)
   (x : BitVec n) (y : BitVec n) (H : 0 < esize) : BitVec n :=
   binary_vector_op_aux 0 (n / esize) esize op x y (BitVec.zero n) H
 
-@[simp]
+@[state_simp_rules]
 def exec_binary_vector (inst : Advanced_simd_three_same_cls) (s : ArmState) : ArmState :=
   if inst.size == 0b11#2 && inst.Q == 0b0#1 then
     write_err (StateError.Illegal s!"Illegal {inst} encountered!") s
@@ -70,7 +70,7 @@ def decode_logical_op (U : BitVec 1) (size : BitVec 2) : SIMDThreeSameLogicalTyp
   | 1#1, 0b10#2 => SIMDThreeSameLogicalType.BIT
   | 1#1, 0b11#2 => SIMDThreeSameLogicalType.BIF
 
-@[simp]
+@[state_simp_rules]
 def logic_vector_op (op : SIMDThreeSameLogicalType) (opdn : BitVec n) (opdm : BitVec n) (opdd : BitVec n)
   : (BitVec n) :=
   match op with
@@ -83,7 +83,7 @@ def logic_vector_op (op : SIMDThreeSameLogicalType) (opdn : BitVec n) (opdm : Bi
   | SIMDThreeSameLogicalType.BIT => opdd ^^^ ((opdd ^^^ opdn) &&& opdm)
   | SIMDThreeSameLogicalType.BIF => opdd ^^^ ((opdd ^^^ opdn) &&& ~~~opdm)
 
-@[simp]
+@[state_simp_rules]
 def exec_logic_vector (inst : Advanced_simd_three_same_cls) (s : ArmState) : ArmState :=
   let datasize := if inst.Q = 1#1 then 128 else 64
   let operand1 := read_sfp datasize inst.Rn s
@@ -94,7 +94,7 @@ def exec_logic_vector (inst : Advanced_simd_three_same_cls) (s : ArmState) : Arm
   let s := write_sfp datasize inst.Rd result s
   s
 
-@[simp]
+@[state_simp_rules]
 def exec_advanced_simd_three_same
   (inst : Advanced_simd_three_same_cls) (s : ArmState) : ArmState :=
   open BitVec in
@@ -118,9 +118,9 @@ theorem pc_of_exec_advanced_simd_three_same
              ofNat_eq_ofNat, zero_eq, exec_logic_vector, 
              logic_vector_op]
   split
-  · split <;> state_simp
-  · state_simp
-  · state_simp
+  · split <;> simp only [state_simp_rules, minimal_theory]
+  · simp only [state_simp_rules, minimal_theory]
+  · simp only [state_simp_rules, minimal_theory]
 
 ----------------------------------------------------------------------
 

diff --git a/Arm/Insts/DPSFP/Advanced_simd_two_reg_misc.lean b/Arm/Insts/DPSFP/Advanced_simd_two_reg_misc.lean
@@ -74,7 +74,7 @@ theorem container_size_dvd_datasize (x : BitVec 2) (q : BitVec 1) :
     repeat trivial
     done
 
-@[simp]
+@[state_simp_rules]
 def exec_advanced_simd_two_reg_misc
   (inst : Advanced_simd_two_reg_misc_cls) (s : ArmState) : ArmState :=
   open BitVec in