From 908256076000f0cae579e5318627898ad65142a9 Mon Sep 17 00:00:00 2001 From: Yan Peng Date: Mon, 30 Sep 2024 18:43:46 +0000 Subject: [PATCH] Remove unused variables --- Arm/Insts/Common.lean | 6 +++--- Arm/Insts/DPSFP/Advanced_simd_copy.lean | 1 - Arm/Insts/DPSFP/Advanced_simd_extract.lean | 4 ---- Arm/Insts/DPSFP/Advanced_simd_scalar_copy.lean | 1 - Arm/Insts/DPSFP/Advanced_simd_three_different.lean | 5 ++--- Arm/Insts/DPSFP/Conversion_between_FP_and_Int.lean | 13 +++---------- Arm/Insts/DPSFP/Crypto_aes.lean | 1 - Arm/Insts/LDST/Reg_pair.lean | 7 ++----- Specs/GCM.lean | 8 ++++---- 9 files changed, 14 insertions(+), 32 deletions(-) diff --git a/Arm/Insts/Common.lean b/Arm/Insts/Common.lean index aae5ff4a..25ee05e5 100644 --- a/Arm/Insts/Common.lean +++ b/Arm/Insts/Common.lean @@ -496,7 +496,7 @@ instance : ToString SIMDThreeSameLogicalType where toString a := toString (repr ---------------------------------------------------------------------- @[state_simp_rules] -def Vpart_read (n : BitVec 5) (part width : Nat) (s : ArmState) (H : width > 0) +def Vpart_read (n : BitVec 5) (part width : Nat) (s : ArmState) : BitVec width := -- assert n >= 0 && n <= 31; -- assert part IN {0, 1}; @@ -656,7 +656,7 @@ deriving DecidableEq, Repr export ShiftInfo (esize elements shift unsigned round accumulate) @[state_simp_rules] -def RShr (unsigned : Bool) (value : Int) (shift : Nat) (round : Bool) (h : n > 0) +def RShr (unsigned : Bool) (value : Int) (shift : Nat) (round : Bool) : BitVec n := -- assert shift > 0 let fn := if unsigned then ushiftRight else sshiftRight @@ -679,7 +679,7 @@ def shift_right_common_aux result else let elem := Int_with_unsigned info.unsigned $ elem_get operand e info.esize - let shift_elem := RShr info.unsigned elem info.shift info.round info.h + let shift_elem := RShr info.unsigned elem info.shift info.round let acc_elem := elem_get operand2 e info.esize + shift_elem let result := elem_set result e info.esize acc_elem info.h have _ : info.elements - (e + 1) < info.elements - e := by omega diff --git a/Arm/Insts/DPSFP/Advanced_simd_copy.lean b/Arm/Insts/DPSFP/Advanced_simd_copy.lean index a9c2b35b..ffd077a1 100644 --- a/Arm/Insts/DPSFP/Advanced_simd_copy.lean +++ b/Arm/Insts/DPSFP/Advanced_simd_copy.lean @@ -117,7 +117,6 @@ def exec_smov_umov (inst : Advanced_simd_copy_cls) (s : ArmState) (signed : Bool let idxdsize := 64 <<< (lsb inst.imm5 4).toNat -- if index == 0 then CheckFPEnabled64 else CheckFPAdvSIMDEnabled64 let operand := read_sfp idxdsize inst.Rn s - have h₀ : esize > 0 := by apply zero_lt_shift_left_pos (by decide) let element := elem_get operand index esize let result := if signed then signExtend datasize element else zeroExtend datasize element -- State Updates diff --git a/Arm/Insts/DPSFP/Advanced_simd_extract.lean b/Arm/Insts/DPSFP/Advanced_simd_extract.lean index ce48a09d..9ec571cd 100644 --- a/Arm/Insts/DPSFP/Advanced_simd_extract.lean +++ b/Arm/Insts/DPSFP/Advanced_simd_extract.lean @@ -32,10 +32,6 @@ def exec_advanced_simd_extract let lo := read_sfp datasize inst.Rn s let concat := hi ++ lo let result := extractLsb' position datasize concat - have h_datasize : 1 <= datasize := by simp_all! [datasize]; split <;> decide - have h : (position + datasize - 1 - position + 1) = datasize := by - rw [Nat.add_sub_assoc, Nat.add_sub_self_left] - exact Nat.sub_add_cancel h_datasize; trivial let s := write_sfp datasize inst.Rd result s let s := write_pc ((read_pc s) + 4#64) s s diff --git a/Arm/Insts/DPSFP/Advanced_simd_scalar_copy.lean b/Arm/Insts/DPSFP/Advanced_simd_scalar_copy.lean index a28b8c99..47a1c98d 100644 --- a/Arm/Insts/DPSFP/Advanced_simd_scalar_copy.lean +++ b/Arm/Insts/DPSFP/Advanced_simd_scalar_copy.lean @@ -27,7 +27,6 @@ def exec_advanced_simd_scalar_copy let idxdsize := 64 <<< (lsb inst.imm5 4).toNat let esize := 8 <<< size let operand := read_sfp idxdsize inst.Rn s - have h : esize > 0 := by apply zero_lt_shift_left_pos (by decide) let result := elem_get operand index.toNat esize -- State Updates let s := write_pc ((read_pc s) + 4#64) s diff --git a/Arm/Insts/DPSFP/Advanced_simd_three_different.lean b/Arm/Insts/DPSFP/Advanced_simd_three_different.lean index 5a64fe3f..87dede23 100644 --- a/Arm/Insts/DPSFP/Advanced_simd_three_different.lean +++ b/Arm/Insts/DPSFP/Advanced_simd_three_different.lean @@ -58,9 +58,8 @@ def exec_pmull (inst : Advanced_simd_three_different_cls) (s : ArmState) : ArmSt let datasize := 64 let part := inst.Q.toNat let elements := datasize / esize - have h₁ : datasize > 0 := by decide - let operand1 := Vpart_read inst.Rn part datasize s h₁ - let operand2 := Vpart_read inst.Rm part datasize s h₁ + let operand1 := Vpart_read inst.Rn part datasize s + let operand2 := Vpart_read inst.Rm part datasize s let result := pmull_op 0 esize elements operand1 operand2 (BitVec.zero (2*datasize)) h₀ let s := write_sfp (datasize*2) inst.Rd result s diff --git a/Arm/Insts/DPSFP/Conversion_between_FP_and_Int.lean b/Arm/Insts/DPSFP/Conversion_between_FP_and_Int.lean index 6e86c85c..b1f60918 100644 --- a/Arm/Insts/DPSFP/Conversion_between_FP_and_Int.lean +++ b/Arm/Insts/DPSFP/Conversion_between_FP_and_Int.lean @@ -19,12 +19,11 @@ open BitVec @[state_simp_rules] def fmov_general_aux (intsize : Nat) (fltsize : Nat) (op : FPConvOp) (part : Nat) (inst : Conversion_between_FP_and_Int_cls) (s : ArmState) - (H : 0 < fltsize) : ArmState := -- Assume CheckFPEnabled64() match op with | FPConvOp.FPConvOp_MOV_FtoI => - let fltval := Vpart_read inst.Rn part fltsize s H + let fltval := Vpart_read inst.Rn part fltsize s let intval := zeroExtend intsize fltval -- State Update let s := write_gpr intsize inst.Rd intval s @@ -44,12 +43,6 @@ def exec_fmov_general (inst : Conversion_between_FP_and_Int_cls) (s : ArmState): ArmState := let intsize := 32 <<< inst.sf.toNat let decode_fltsize := if inst.ftype = 0b10#2 then 64 else (8 <<< (inst.ftype ^^^ 0b10#2).toNat) - have H: 0 < decode_fltsize := by - simp only [decode_fltsize, beq_iff_eq] - split - · decide - · generalize BitVec.toNat (inst.ftype ^^^ 2#2) = x - apply zero_lt_shift_left_pos (by decide) match (extractLsb' 1 2 inst.opcode) ++ inst.rmode with | 1100 => -- FMOV if decode_fltsize ≠ 16 ∧ decode_fltsize ≠ intsize then @@ -59,7 +52,7 @@ def exec_fmov_general then FPConvOp.FPConvOp_MOV_ItoF else FPConvOp.FPConvOp_MOV_FtoI let part := 0 - fmov_general_aux intsize decode_fltsize op part inst s H + fmov_general_aux intsize decode_fltsize op part inst s | 1101 => -- FMOV D[1] if intsize ≠ 64 ∨ inst.ftype ≠ 0b10#2 then write_err (StateError.Illegal s!"Illegal {inst} encountered!") s @@ -68,7 +61,7 @@ def exec_fmov_general then FPConvOp.FPConvOp_MOV_ItoF else FPConvOp.FPConvOp_MOV_FtoI let part := 1 - fmov_general_aux intsize decode_fltsize op part inst s H + fmov_general_aux intsize decode_fltsize op part inst s | _ => write_err (StateError.Other s!"exec_fmov_general called with non-FMOV instructions!") s @[state_simp_rules] diff --git a/Arm/Insts/DPSFP/Crypto_aes.lean b/Arm/Insts/DPSFP/Crypto_aes.lean index 6c9b1493..e58e3f73 100644 --- a/Arm/Insts/DPSFP/Crypto_aes.lean +++ b/Arm/Insts/DPSFP/Crypto_aes.lean @@ -52,7 +52,6 @@ def FFmul02 (b : BitVec 8) : BitVec 8 := 0x1E1C1A18161412100E0C0A0806040200#128 -- 0 ] let lo := b.toNat * 8 - let hi := lo + 7 extractLsb' lo 8 $ BitVec.flatten FFmul_02 def FFmul03 (b : BitVec 8) : BitVec 8 := diff --git a/Arm/Insts/LDST/Reg_pair.lean b/Arm/Insts/LDST/Reg_pair.lean index b962eb09..5c0c6263 100644 --- a/Arm/Insts/LDST/Reg_pair.lean +++ b/Arm/Insts/LDST/Reg_pair.lean @@ -40,7 +40,7 @@ def reg_pair_constrain_unpredictable (wback : Bool) (inst : Reg_pair_cls) : Bool @[state_simp_rules] def reg_pair_operation (inst : Reg_pair_cls) (inst_str : String) (signed : Bool) (datasize : Nat) (offset : BitVec 64) (s : ArmState) - (H1 : 8 ∣ datasize) (H2 : 0 < datasize) : ArmState := + (H1 : 8 ∣ datasize): ArmState := -- Note: we do not need to model the ASL function -- "CreateAccDescGPR" here, given the simplicity of our memory -- model @@ -99,11 +99,8 @@ def exec_reg_pair_common (inst : Reg_pair_cls) (inst_str : String) (s : ArmState let offset := (signExtend 64 inst.imm7) <<< scale have H1 : 8 ∣ datasize := by simp_all! only [gt_iff_lt, Nat.shiftLeft_eq, Nat.dvd_mul_right, datasize] - have H2 : 0 < datasize := by - simp_all! only [datasize] - apply zero_lt_shift_left_pos (by decide) -- State Updates - let s' := reg_pair_operation inst inst_str signed datasize offset s H1 H2 + let s' := reg_pair_operation inst inst_str signed datasize offset s H1 let s' := write_pc ((read_pc s) + 4#64) s' s' diff --git a/Specs/GCM.lean b/Specs/GCM.lean index 17915aa4..b7496b62 100644 --- a/Specs/GCM.lean +++ b/Specs/GCM.lean @@ -22,7 +22,7 @@ def R : (BitVec 128) := 0b11100001#8 ++ 0b0#120 abbrev Cipher {n : Nat} {m : Nat} := BitVec n → BitVec m → BitVec n /-- The s-bit incrementing function -/ -def inc_s (s : Nat) (X : BitVec l) (H₀ : 0 < s) (H₁ : s < l) : BitVec l := +def inc_s (s : Nat) (X : BitVec l) (H₀ : s < l) : BitVec l := let upper := extractLsb' s (l - s) X let lower := (extractLsb' 0 s X) + 0b1#s have h : l - s + s = l := by omega @@ -72,7 +72,7 @@ def GCTR_aux (CIPH : Cipher (n := 128) (m := m)) let Xi := extractLsb' lo 128 X let Yi := Xi ^^^ CIPH ICB K let Y := BitVec.partInstall hi lo (BitVec.cast h Yi) Y - let ICB := inc_s 32 ICB (by omega) (by omega) + let ICB := inc_s 32 ICB (by omega) GCTR_aux CIPH (i + 1) n K ICB X Y termination_by (n - i) @@ -130,7 +130,7 @@ def GCM_AE (CIPH : Cipher (n := 128) (m := m)) : (BitVec p) × (BitVec t) := let H := CIPH (BitVec.zero 128) K let J0 : BitVec 128 := GCM.initialize_J0 H IV - let ICB := inc_s 32 J0 (by decide) (by decide) + let ICB := inc_s 32 J0 (by decide) let C := GCTR (m := m) CIPH K ICB P let u := GCM.ceiling_in_bits p - p let v := GCM.ceiling_in_bits a - a @@ -165,7 +165,7 @@ def GCM_AD (CIPH : Cipher (n := 128) (m := m)) else let H := CIPH (BitVec.zero 128) K let J0 := GCM.initialize_J0 H IV - let ICB := inc_s 32 J0 (by decide) (by decide) + let ICB := inc_s 32 J0 (by decide) let P := GCTR (m := m) CIPH K ICB C let u := GCM.ceiling_in_bits c - c let v := GCM.ceiling_in_bits a - a