From 635575748b2cb688a7ae512b4d490c8a596ec2c8 Mon Sep 17 00:00:00 2001 From: Yan Peng Date: Wed, 25 Sep 2024 21:51:19 +0000 Subject: [PATCH] Fixing extractLsb to be extractLsb' --- Arm/Insts/BR/Cond_branch_imm.lean | 2 +- Arm/Insts/DPI/Logical_imm.lean | 2 +- Arm/Insts/DPR/Data_processing_one_source.lean | 8 +- Arm/Insts/DPR/Data_processing_two_source.lean | 2 +- Arm/Insts/DPSFP/Advanced_simd_copy.lean | 10 +- Arm/Insts/DPSFP/Advanced_simd_extract.lean | 4 +- .../Advanced_simd_modified_immediate.lean | 12 +-- .../DPSFP/Advanced_simd_scalar_copy.lean | 2 +- .../DPSFP/Conversion_between_FP_and_Int.lean | 11 +-- Arm/Insts/DPSFP/Crypto_aes.lean | 5 +- Arm/Insts/DPSFP/Crypto_three_reg_sha512.lean | 34 +++---- Arm/Insts/DPSFP/Crypto_two_reg_sha512.lean | 6 +- Arm/Insts/LDST/Reg_pair.lean | 11 +-- Arm/Insts/LDST/Reg_unscaled_imm.lean | 6 +- Arm/Memory/MemoryProofs.lean | 2 +- Specs/AESArm.lean | 4 +- Specs/AESCommon.lean | 99 +++++++++---------- Specs/AESV8.lean | 5 +- Specs/GCM.lean | 27 ++--- Specs/GCMV8.lean | 4 +- Tests/AES-GCM/AESV8ProgramTests.lean | 8 +- Tests/AES-GCM/GCMSpecTests.lean | 4 +- 22 files changed, 124 insertions(+), 144 deletions(-) diff --git a/Arm/Insts/BR/Cond_branch_imm.lean b/Arm/Insts/BR/Cond_branch_imm.lean index d15aa16b..33a0fdfb 100644 --- a/Arm/Insts/BR/Cond_branch_imm.lean +++ b/Arm/Insts/BR/Cond_branch_imm.lean @@ -29,7 +29,7 @@ def Cond_branch_imm_inst.condition_holds let N := read_flag PFlag.N s let V := read_flag PFlag.V s let result := - match (extractLsb 3 1 inst.cond) with + match (extractLsb' 1 3 inst.cond) with | 0b000#3 => Z = 1#1 | 0b001#3 => C = 1#1 | 0b010#3 => N = 1#1 diff --git a/Arm/Insts/DPI/Logical_imm.lean b/Arm/Insts/DPI/Logical_imm.lean index a2d4d8c8..0a1d7afb 100644 --- a/Arm/Insts/DPI/Logical_imm.lean +++ b/Arm/Insts/DPI/Logical_imm.lean @@ -63,7 +63,7 @@ def MoveWidePreferred (sf immN : BitVec 1) (imms immr : BitVec 6) : Bool := false -- NOTE: the second conjunct below is semantically equivalent to the ASL code -- !((immN:imms) IN {'00xxxxx'}) - else if sf = 0#1 ∧ ¬(immN = 0#1 ∧ imms.extractLsb 5 5 = 0#1) then + else if sf = 0#1 ∧ ¬(immN = 0#1 ∧ imms.extractLsb' 5 1 = 0#1) then false -- for MOVZ must contain no more than 16 ones diff --git a/Arm/Insts/DPR/Data_processing_one_source.lean b/Arm/Insts/DPR/Data_processing_one_source.lean index 36c6165c..145f004a 100644 --- a/Arm/Insts/DPR/Data_processing_one_source.lean +++ b/Arm/Insts/DPR/Data_processing_one_source.lean @@ -55,7 +55,7 @@ private theorem opc_and_sf_constraint (x : BitVec 2) (y : BitVec 1) @[state_simp_rules] def exec_data_processing_rev (inst : Data_processing_one_source_cls) (s : ArmState) : ArmState := - let opc : BitVec 2 := extractLsb 1 0 inst.opcode + let opc : BitVec 2 := extractLsb' 0 2 inst.opcode if H₁ : opc = 0b11#2 ∧ inst.sf = 0b0#1 then write_err (StateError.Illegal s!"Illegal {inst} encountered!") s else @@ -65,16 +65,16 @@ def exec_data_processing_rev let esize := 8 have opc_h₁ : opc.toNat ≥ 0 := by simp only [ge_iff_le, Nat.zero_le] have opc_h₂ : opc.toNat < 4 := by - refine BitVec.isLt (extractLsb 1 0 inst.opcode) + refine BitVec.isLt (extractLsb' 0 2 inst.opcode) have opc_sf_h : ¬(opc.toNat = 3 ∧ inst.sf.toNat = 0) := by - apply opc_and_sf_constraint (extractLsb 1 0 inst.opcode) inst.sf H₁ + apply opc_and_sf_constraint (extractLsb' 0 2 inst.opcode) inst.sf H₁ have h₀ : 0 < esize := by decide have h₁ : esize ≤ container_size := by apply shiftLeft_ge have h₂ : container_size ≤ datasize := by apply container_size_le_datasize opc.toNat inst.sf.toNat opc_h₁ opc_h₂ opc_sf_h have h₃ : esize ∣ container_size := by simp only [esize, container_size] - generalize BitVec.toNat (extractLsb 1 0 inst.opcode) = x + generalize BitVec.toNat (extractLsb' 0 2 inst.opcode) = x simp only [Nat.shiftLeft_eq] generalize 2 ^ x = n simp only [Nat.dvd_mul_right] diff --git a/Arm/Insts/DPR/Data_processing_two_source.lean b/Arm/Insts/DPR/Data_processing_two_source.lean index 22798d4e..a48ac981 100644 --- a/Arm/Insts/DPR/Data_processing_two_source.lean +++ b/Arm/Insts/DPR/Data_processing_two_source.lean @@ -19,7 +19,7 @@ open BitVec def exec_data_processing_shift (inst : Data_processing_two_source_cls) (s : ArmState) : ArmState := let datasize := 32 <<< inst.sf.toNat - let shift_type := decode_shift $ extractLsb 1 0 inst.opcode + let shift_type := decode_shift $ extractLsb' 0 2 inst.opcode let operand2 := read_gpr_zr datasize inst.Rm s let amount := BitVec.ofInt 6 (operand2.toInt % datasize) let operand := read_gpr_zr datasize inst.Rn s diff --git a/Arm/Insts/DPSFP/Advanced_simd_copy.lean b/Arm/Insts/DPSFP/Advanced_simd_copy.lean index bd4cf712..68870a52 100644 --- a/Arm/Insts/DPSFP/Advanced_simd_copy.lean +++ b/Arm/Insts/DPSFP/Advanced_simd_copy.lean @@ -32,7 +32,7 @@ def exec_dup_element (inst : Advanced_simd_copy_cls) (s : ArmState) : ArmState : if size > 3 ∨ (size = 3 ∧ inst.Q = 0) then write_err (StateError.Illegal s!"Illegal {inst} encountered!") s else - let index := (extractLsb 4 (size + 1) inst.imm5).toNat + let index := (extractLsb' (size + 1) (4 - size) inst.imm5).toNat let idxdsize := 64 <<< (lsb inst.imm5 4).toNat let esize := 8 <<< size let datasize := 64 <<< inst.Q.toNat @@ -69,8 +69,8 @@ def exec_ins_element (inst : Advanced_simd_copy_cls) (s : ArmState) : ArmState : if size > 3 then write_err (StateError.Illegal s!"Illegal {inst} encountered!") s else - let dst_index := (extractLsb 4 (size + 1) inst.imm5).toNat - let src_index := (extractLsb 3 size inst.imm4).toNat + let dst_index := (extractLsb' (size + 1) (4 - size) inst.imm5).toNat + let src_index := (extractLsb' size (4 - size) inst.imm4).toNat let idxdsize := 64 <<< (lsb inst.imm4 3).toNat let esize := 8 <<< size let operand := read_sfp idxdsize inst.Rn s @@ -89,7 +89,7 @@ def exec_ins_general (inst : Advanced_simd_copy_cls) (s : ArmState) : ArmState : if size > 3 then write_err (StateError.Illegal s!"Illegal {inst} encountered!") s else - let index := (extractLsb 4 (size + 1) inst.imm5).toNat + let index := (extractLsb' (size + 1) (4 - size) inst.imm5).toNat let esize := 8 <<< size let element := read_gpr esize inst.Rn s let result := read_sfp 128 inst.Rd s @@ -113,7 +113,7 @@ def exec_smov_umov (inst : Advanced_simd_copy_cls) (s : ArmState) (signed : Bool (datasize = 32 ∧ esize >= 64)) then write_err (StateError.Illegal s!"Illegal {inst} encountered!") s else - let index := (extractLsb 4 (size + 1) inst.imm5).toNat + let index := (extractLsb' (size + 1) (4 - size) inst.imm5).toNat let idxdsize := 64 <<< (lsb inst.imm5 4).toNat -- if index == 0 then CheckFPEnabled64 else CheckFPAdvSIMDEnabled64 let operand := read_sfp idxdsize inst.Rn s diff --git a/Arm/Insts/DPSFP/Advanced_simd_extract.lean b/Arm/Insts/DPSFP/Advanced_simd_extract.lean index cc52b4bb..ce48a09d 100644 --- a/Arm/Insts/DPSFP/Advanced_simd_extract.lean +++ b/Arm/Insts/DPSFP/Advanced_simd_extract.lean @@ -31,12 +31,12 @@ def exec_advanced_simd_extract let hi := read_sfp datasize inst.Rm s let lo := read_sfp datasize inst.Rn s let concat := hi ++ lo - let result := extractLsb (position + datasize - 1) position concat + 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 (BitVec.cast h result) s + 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_modified_immediate.lean b/Arm/Insts/DPSFP/Advanced_simd_modified_immediate.lean index cfec1f8f..a46404a8 100644 --- a/Arm/Insts/DPSFP/Advanced_simd_modified_immediate.lean +++ b/Arm/Insts/DPSFP/Advanced_simd_modified_immediate.lean @@ -52,7 +52,7 @@ def decode_immediate_op (inst : Advanced_simd_modified_immediate_cls) else (some ImmediateOp.MOVI, s) def AdvSIMDExpandImm (op : BitVec 1) (cmode : BitVec 4) (imm8 : BitVec 8) : BitVec 64 := - let cmode_high3 := extractLsb 3 1 cmode + let cmode_high3 := extractLsb' 1 3 cmode let cmode_low1 := lsb cmode 0 match cmode_high3 with | 0b000#3 => replicate 2 $ BitVec.zero 24 ++ imm8 @@ -82,13 +82,13 @@ def AdvSIMDExpandImm (op : BitVec 1) (cmode : BitVec 4) (imm8 : BitVec 8) : BitV else if cmode_low1 = 1 ∧ op = 0 then let imm32 := lsb imm8 7 ++ ~~~(lsb imm8 6) ++ (replicate 5 $ lsb imm8 6) ++ - extractLsb 5 0 imm8 ++ BitVec.zero 19 + extractLsb' 0 6 imm8 ++ BitVec.zero 19 replicate 2 imm32 else -- Assume not UsingAArch32() -- if UsingAArch32() then ReservedEncoding(); lsb imm8 7 ++ ~~~(lsb imm8 6) ++ - (replicate 8 $ lsb imm8 6) ++ extractLsb 5 0 imm8 ++ BitVec.zero 48 + (replicate 8 $ lsb imm8 6) ++ extractLsb' 0 6 imm8 ++ BitVec.zero 48 private theorem mul_div_norm_form_lemma (n m : Nat) (_h1 : 0 < m) (h2 : n ∣ m) : @@ -107,9 +107,9 @@ def exec_advanced_simd_modified_immediate let datasize := 64 <<< inst.Q.toNat let imm8 := inst.a ++ inst.b ++ inst.c ++ inst.d ++ inst.e ++ inst.f ++ inst.g ++ inst.h let imm16 : BitVec 16 := - extractLsb 7 7 imm8 ++ ~~~ (extractLsb 6 6 imm8) ++ - (replicate 2 $ extractLsb 6 6 imm8) ++ extractLsb 5 0 imm8 ++ - BitVec.zero 6 + extractLsb' 7 1 imm8 ++ ~~~ (extractLsb' 6 1 imm8) ++ + (replicate 2 $ extractLsb' 6 1 imm8) ++ + extractLsb' 0 6 imm8 ++ BitVec.zero 6 let imm64 := AdvSIMDExpandImm inst.op inst.cmode imm8 have h₁ : 16 * (datasize / 16) = datasize := by omega have h₂ : 64 * (datasize / 64) = datasize := by omega diff --git a/Arm/Insts/DPSFP/Advanced_simd_scalar_copy.lean b/Arm/Insts/DPSFP/Advanced_simd_scalar_copy.lean index 3f2b25c2..caa30639 100644 --- a/Arm/Insts/DPSFP/Advanced_simd_scalar_copy.lean +++ b/Arm/Insts/DPSFP/Advanced_simd_scalar_copy.lean @@ -23,7 +23,7 @@ def exec_advanced_simd_scalar_copy if size > 3 ∨ inst.imm4 ≠ 0b0000#4 ∨ inst.op ≠ 0 then write_err (StateError.Illegal s!"Illegal {inst} encountered!") s else - let index := extractLsb 4 (size + 1) inst.imm5 + let index := extractLsb' (size + 1) (4 - size) inst.imm5 let idxdsize := 64 <<< (lsb inst.imm5 4).toNat let esize := 8 <<< size let operand := read_sfp idxdsize inst.Rn s diff --git a/Arm/Insts/DPSFP/Conversion_between_FP_and_Int.lean b/Arm/Insts/DPSFP/Conversion_between_FP_and_Int.lean index b4a3642d..6e86c85c 100644 --- a/Arm/Insts/DPSFP/Conversion_between_FP_and_Int.lean +++ b/Arm/Insts/DPSFP/Conversion_between_FP_and_Int.lean @@ -32,10 +32,9 @@ def fmov_general_aux (intsize : Nat) (fltsize : Nat) (op : FPConvOp) s | FPConvOp.FPConvOp_MOV_ItoF => let intval := read_gpr intsize inst.Rn s - let fltval := extractLsb (fltsize - 1) 0 intval + let fltval := extractLsb' 0 fltsize intval -- State Update - have h₀ : fltsize - 1 - 0 + 1 = fltsize := by omega - let s := Vpart_write inst.Rd part fltsize (BitVec.cast h₀ fltval) s + let s := Vpart_write inst.Rd part fltsize fltval s let s := write_pc ((read_pc s) + 4#64) s s | _ => write_err (StateError.Other s!"fmov_general_aux called with non-FMOV op!") s @@ -51,7 +50,7 @@ def exec_fmov_general · decide · generalize BitVec.toNat (inst.ftype ^^^ 2#2) = x apply zero_lt_shift_left_pos (by decide) - match (extractLsb 2 1 inst.opcode) ++ inst.rmode with + match (extractLsb' 1 2 inst.opcode) ++ inst.rmode with | 1100 => -- FMOV if decode_fltsize ≠ 16 ∧ decode_fltsize ≠ intsize then write_err (StateError.Illegal s!"Illegal {inst} encountered!") s @@ -75,7 +74,7 @@ def exec_fmov_general @[state_simp_rules] def exec_conversion_between_FP_and_Int (inst : Conversion_between_FP_and_Int_cls) (s : ArmState) : ArmState := - if inst.ftype = 0b10#2 ∧ (extractLsb 2 1 inst.opcode) ++ inst.rmode ≠ 0b1101#4 then + if inst.ftype = 0b10#2 ∧ (extractLsb' 1 2 inst.opcode) ++ inst.rmode ≠ 0b1101#4 then write_err (StateError.Illegal s!"Illegal {inst} encountered!") s -- Assume IsFeatureImplemented(FEAT_FP16) is true else @@ -92,7 +91,7 @@ partial def Conversion_between_FP_and_Int_cls.fmov_general.rand : Cosim.CosimM ( let sf := ← BitVec.rand 1 let intsize := 32 <<< sf.toNat let decode_fltsize := if ftype == 0b10#2 then 64 else (8 <<< (ftype ^^^ 0b10#2).toNat) - if ftype == 0b10#2 && ((extractLsb 2 1 opcode) ++ rmode) != 0b1101#4 || + if ftype == 0b10#2 && ((extractLsb' 1 2 opcode) ++ rmode) != 0b1101#4 || decode_fltsize != 16 && decode_fltsize != intsize || intsize != 64 || ftype != 0b10#2 then Conversion_between_FP_and_Int_cls.fmov_general.rand diff --git a/Arm/Insts/DPSFP/Crypto_aes.lean b/Arm/Insts/DPSFP/Crypto_aes.lean index 99d99027..6c9b1493 100644 --- a/Arm/Insts/DPSFP/Crypto_aes.lean +++ b/Arm/Insts/DPSFP/Crypto_aes.lean @@ -53,7 +53,7 @@ def FFmul02 (b : BitVec 8) : BitVec 8 := ] let lo := b.toNat * 8 let hi := lo + 7 - BitVec.cast (by omega) $ extractLsb hi lo $ BitVec.flatten FFmul_02 + extractLsb' lo 8 $ BitVec.flatten FFmul_02 def FFmul03 (b : BitVec 8) : BitVec 8 := let FFmul_03 := @@ -76,8 +76,7 @@ def FFmul03 (b : BitVec 8) : BitVec 8 := 0x111217141D1E1B18090A0F0C05060300#128 -- 0 ] let lo := b.toNat * 8 - let hi := lo + 7 - BitVec.cast (by omega) $ extractLsb hi lo $ BitVec.flatten FFmul_03 + extractLsb' lo 8 $ BitVec.flatten FFmul_03 def AESMixColumns (op : BitVec 128) : BitVec 128 := AESCommon.MixColumns op FFmul02 FFmul03 diff --git a/Arm/Insts/DPSFP/Crypto_three_reg_sha512.lean b/Arm/Insts/DPSFP/Crypto_three_reg_sha512.lean index e0535d58..e62b4d8e 100644 --- a/Arm/Insts/DPSFP/Crypto_three_reg_sha512.lean +++ b/Arm/Insts/DPSFP/Crypto_three_reg_sha512.lean @@ -21,14 +21,14 @@ open BitVec def sha512h (x : BitVec 128) (y : BitVec 128) (w : BitVec 128) : BitVec 128 := open sha512_helpers in - let y_127_64 := extractLsb 127 64 y - let y_63_0 := extractLsb 63 0 y + let y_127_64 := extractLsb' 64 64 y + let y_63_0 := extractLsb' 0 64 y let msigma1 := sigma_big_1 y_127_64 - let x_63_0 := extractLsb 63 0 x - let x_127_64 := extractLsb 127 64 x + let x_63_0 := extractLsb' 0 64 x + let x_127_64 := extractLsb' 64 64 x let vtmp_127_64 := ch y_127_64 x_63_0 x_127_64 - let w_127_64 := extractLsb 127 64 w - let w_63_0 := extractLsb 63 0 w + let w_127_64 := extractLsb' 64 64 w + let w_63_0 := extractLsb' 0 64 w let vtmp_127_64 := vtmp_127_64 + msigma1 + w_127_64 let tmp := vtmp_127_64 + y_63_0 let msigma1 := sigma_big_1 tmp @@ -40,16 +40,16 @@ def sha512h (x : BitVec 128) (y : BitVec 128) (w : BitVec 128) def sha512h2 (x : BitVec 128) (y : BitVec 128) (w : BitVec 128) : BitVec 128 := open sha512_helpers in - let y_63_0 := extractLsb 63 0 y - let y_127_64 := extractLsb 127 64 y + let y_63_0 := extractLsb' 0 64 y + let y_127_64 := extractLsb' 64 64 y let nsigma0 := sigma_big_0 y_63_0 - let x_63_0 := extractLsb 63 0 x + let x_63_0 := extractLsb' 0 64 x let vtmp_127_64 := maj x_63_0 y_127_64 y_63_0 - let w_127_64 := extractLsb 127 64 w + let w_127_64 := extractLsb' 64 64 w let vtmp_127_64 := vtmp_127_64 + nsigma0 + w_127_64 let nsigma0 := sigma_big_0 vtmp_127_64 let vtmp_63_0 := maj vtmp_127_64 y_63_0 y_127_64 - let w_63_0 := extractLsb 63 0 w + let w_63_0 := extractLsb' 0 64 w let vtmp_63_0 := vtmp_63_0 + nsigma0 + w_63_0 let result := vtmp_127_64 ++ vtmp_63_0 result @@ -57,15 +57,15 @@ def sha512h2 (x : BitVec 128) (y : BitVec 128) (w : BitVec 128) : def sha512su1 (x : BitVec 128) (y : BitVec 128) (w : BitVec 128) : BitVec 128 := open sha512_helpers in - let x_127_64 := extractLsb 127 64 x + let x_127_64 := extractLsb' 64 64 x let sig1 := sigma_1 x_127_64 - let w_127_64 := extractLsb 127 64 w - let y_127_64 := extractLsb 127 64 y + let w_127_64 := extractLsb' 64 64 w + let y_127_64 := extractLsb' 64 64 y let vtmp_127_64 := w_127_64 + sig1 + y_127_64 - let x_63_0 := extractLsb 63 0 x + let x_63_0 := extractLsb' 0 64 x let sig1 := sigma_1 x_63_0 - let w_63_0 := extractLsb 63 0 w - let y_63_0 := extractLsb 63 0 y + let w_63_0 := extractLsb' 0 64 w + let y_63_0 := extractLsb' 0 64 y let vtmp_63_0 := w_63_0 + sig1 + y_63_0 let result := vtmp_127_64 ++ vtmp_63_0 result diff --git a/Arm/Insts/DPSFP/Crypto_two_reg_sha512.lean b/Arm/Insts/DPSFP/Crypto_two_reg_sha512.lean index 0fbe96e8..f3bbd1fa 100644 --- a/Arm/Insts/DPSFP/Crypto_two_reg_sha512.lean +++ b/Arm/Insts/DPSFP/Crypto_two_reg_sha512.lean @@ -19,10 +19,10 @@ open BitVec def sha512su0 (x : BitVec 128) (w : BitVec 128) : BitVec 128 := open sha512_helpers in - let w_127_64 := extractLsb 127 64 w - let w_63_0 := extractLsb 63 0 w + let w_127_64 := extractLsb' 64 64 w + let w_63_0 := extractLsb' 0 64 w let sig0 := sigma_0 w_127_64 - let x_63_0 := extractLsb 63 0 x + let x_63_0 := extractLsb' 0 64 x let vtmp_63_0 := w_63_0 + sig0 let sig0 := sigma_0 x_63_0 let vtmp_127_64 := w_127_64 + sig0 diff --git a/Arm/Insts/LDST/Reg_pair.lean b/Arm/Insts/LDST/Reg_pair.lean index 164a8b5d..b962eb09 100644 --- a/Arm/Insts/LDST/Reg_pair.lean +++ b/Arm/Insts/LDST/Reg_pair.lean @@ -64,18 +64,15 @@ def reg_pair_operation (inst : Reg_pair_cls) (inst_str : String) (signed : Bool) let full_data := data2 ++ data1 write_mem_bytes (2 * (datasize / 8)) address (BitVec.cast h3 full_data) s | _ => -- LOAD - have h4 : datasize - 1 - 0 + 1 = datasize := by - simp; apply Nat.sub_add_cancel H2 - have h5 : 2 * datasize - 1 - datasize + 1 = datasize := by omega let full_data := read_mem_bytes (2 * (datasize / 8)) address s - let data1 := extractLsb (datasize - 1) 0 full_data - let data2 := extractLsb ((2 * datasize) - 1) datasize full_data + let data1 := extractLsb' 0 datasize full_data + let data2 := extractLsb' datasize datasize full_data if not inst.SIMD? ∧ signed then let s := write_gpr 64 inst.Rt (signExtend 64 data1) s write_gpr 64 inst.Rt2 (signExtend 64 data2) s else - let s:= ldst_write inst.SIMD? datasize inst.Rt (BitVec.cast h4 data1) s - ldst_write inst.SIMD? datasize inst.Rt2 (BitVec.cast h5 data2) s + let s:= ldst_write inst.SIMD? datasize inst.Rt data1 s + ldst_write inst.SIMD? datasize inst.Rt2 data2 s if inst.wback then let address := if inst.postindex then address + offset else address write_gpr 64 inst.Rn address s diff --git a/Arm/Insts/LDST/Reg_unscaled_imm.lean b/Arm/Insts/LDST/Reg_unscaled_imm.lean index eca300cf..1e0db697 100644 --- a/Arm/Insts/LDST/Reg_unscaled_imm.lean +++ b/Arm/Insts/LDST/Reg_unscaled_imm.lean @@ -17,7 +17,7 @@ open BitVec @[state_simp_rules] def exec_ldstur (inst : Reg_unscaled_imm_cls) (s : ArmState) : ArmState := - let scale := (extractLsb 1 1 inst.opc ++ inst.size).toNat + let scale := (extractLsb' 1 1 inst.opc ++ inst.size).toNat if scale > 4 then write_err (StateError.Illegal s!"Illegal {inst} encountered!") s else @@ -44,9 +44,9 @@ def exec_ldstur @[state_simp_rules] def exec_reg_unscaled_imm (inst : Reg_unscaled_imm_cls) (s : ArmState) : ArmState := - if inst.VR = 0b1#1 then + if inst.VR = 0b1#1 then exec_ldstur inst s - else + else write_err (StateError.Unimplemented s!"Unsupported instruction {inst} encountered!") s end LDST diff --git a/Arm/Memory/MemoryProofs.lean b/Arm/Memory/MemoryProofs.lean index c3b048ff..6973512a 100644 --- a/Arm/Memory/MemoryProofs.lean +++ b/Arm/Memory/MemoryProofs.lean @@ -317,7 +317,7 @@ private theorem mem_subset_neq_first_addr_small_second_region cases h2 · rename_i h simp only [BitVec.add_sub_self_left_64] at h - have l1 : n' = 18446744073709551615 := by + have l1 : n' = 18446744073709551615 := by rw [BitVec.toNat_eq] at h simp only [toNat_ofNat, Nat.reducePow, Nat.reduceMod] at h omega diff --git a/Specs/AESArm.lean b/Specs/AESArm.lean index c549f8a6..5e36f677 100644 --- a/Specs/AESArm.lean +++ b/Specs/AESArm.lean @@ -112,9 +112,7 @@ protected def InitKey {Param : KBR} (i : Nat) (key : BitVec Param.key_len) (acc : KeySchedule) : KeySchedule := if h₀ : Param.Nk ≤ i then acc else - have h₁ : i * 32 + 32 - 1 - i * 32 + 1 = WordSize := by - simp only [WordSize]; omega - let wd := BitVec.cast h₁ $ extractLsb (i * 32 + 32 - 1) (i * 32) key + let wd := extractLsb' (i * 32) 32 key let (x:KeySchedule) := [wd] have _ : Param.Nk - (i + 1) < Param.Nk - i := by omega AESArm.InitKey (Param := Param) (i + 1) key (acc ++ x) diff --git a/Specs/AESCommon.lean b/Specs/AESCommon.lean index f36ae837..3c8a8ff0 100644 --- a/Specs/AESCommon.lean +++ b/Specs/AESCommon.lean @@ -33,84 +33,81 @@ def SBOX := ] def ShiftRows (op : BitVec 128) : BitVec 128 := - extractLsb 95 88 op ++ extractLsb 55 48 op ++ - extractLsb 15 8 op ++ extractLsb 103 96 op ++ - extractLsb 63 56 op ++ extractLsb 23 16 op ++ - extractLsb 111 104 op ++ extractLsb 71 64 op ++ - extractLsb 31 24 op ++ extractLsb 119 112 op ++ - extractLsb 79 72 op ++ extractLsb 39 32 op ++ - extractLsb 127 120 op ++ extractLsb 87 80 op ++ - extractLsb 47 40 op ++ extractLsb 7 0 op + extractLsb' 88 8 op ++ extractLsb' 48 8 op ++ + extractLsb' 8 8 op ++ extractLsb' 96 8 op ++ + extractLsb' 56 8 op ++ extractLsb' 16 8 op ++ + extractLsb' 104 8 op ++ extractLsb' 64 8 op ++ + extractLsb' 24 8 op ++ extractLsb' 112 8 op ++ + extractLsb' 72 8 op ++ extractLsb' 32 8 op ++ + extractLsb' 120 8 op ++ extractLsb' 80 8 op ++ + extractLsb' 40 8 op ++ extractLsb' 0 8 op def SubBytes_aux (i : Nat) (op : BitVec 128) (out : BitVec 128) : BitVec 128 := - if h₀ : 16 <= i then - out - else - let idx := (extractLsb (i * 8 + 7) (i * 8) op).toNat - let val := extractLsb (idx * 8 + 7) (idx * 8) $ BitVec.flatten SBOX - have h₁ : idx * 8 + 7 - idx * 8 + 1 = i * 8 + 7 - i * 8 + 1 := by omega + match i with + | 0 => out + | i' + 1 => + let i := 16 - i + let idx := (extractLsb' (i * 8) 8 op).toNat + let val := extractLsb' (idx * 8) 8 $ BitVec.flatten SBOX + have h₁ : 8 = i * 8 + 7 - i * 8 + 1 := by omega let out := BitVec.partInstall (i * 8 + 7) (i * 8) (BitVec.cast h₁ val) out - have _ : 15 - i < 16 - i := by omega - SubBytes_aux (i + 1) op out - termination_by (16 - i) + SubBytes_aux i' op out def SubBytes (op : BitVec 128) : BitVec 128 := - SubBytes_aux 0 op (BitVec.zero 128) + SubBytes_aux 16 op (BitVec.zero 128) def MixColumns_aux (c : Nat) (in0 : BitVec 32) (in1 : BitVec 32) (in2 : BitVec 32) (in3 : BitVec 32) (out0 : BitVec 32) (out1 : BitVec 32) (out2 : BitVec 32) (out3 : BitVec 32) (FFmul02 : BitVec 8 -> BitVec 8) (FFmul03 : BitVec 8 -> BitVec 8) : BitVec 32 × BitVec 32 × BitVec 32 × BitVec 32 := - if h₀ : 4 <= c then - (out0, out1, out2, out3) - else - let lo := c * 8 + match c with + | 0 => (out0, out1, out2, out3) + | c' + 1 => + let lo := (4 - c) * 8 let hi := lo + 7 - have h₁ : hi - lo + 1 = 8 := by omega - let in0_byte := BitVec.cast h₁ $ extractLsb hi lo in0 - let in1_byte := BitVec.cast h₁ $ extractLsb hi lo in1 - let in2_byte := BitVec.cast h₁ $ extractLsb hi lo in2 - let in3_byte := BitVec.cast h₁ $ extractLsb hi lo in3 - let val0 := BitVec.cast h₁.symm $ (FFmul02 in0_byte ^^^ FFmul03 in1_byte ^^^ in2_byte ^^^ in3_byte) + let in0_byte := extractLsb' lo 8 in0 + let in1_byte := extractLsb' lo 8 in1 + let in2_byte := extractLsb' lo 8 in2 + let in3_byte := extractLsb' lo 8 in3 + have h : 8 = hi - lo + 1 := by omega + let val0 := BitVec.cast h $ FFmul02 in0_byte ^^^ FFmul03 in1_byte ^^^ in2_byte ^^^ in3_byte let out0 := BitVec.partInstall hi lo val0 out0 - let val1 := BitVec.cast h₁.symm $ (FFmul02 in1_byte ^^^ FFmul03 in2_byte ^^^ in3_byte ^^^ in0_byte) + let val1 := BitVec.cast h $ FFmul02 in1_byte ^^^ FFmul03 in2_byte ^^^ in3_byte ^^^ in0_byte let out1 := BitVec.partInstall hi lo val1 out1 - let val2 := BitVec.cast h₁.symm $ (FFmul02 in2_byte ^^^ FFmul03 in3_byte ^^^ in0_byte ^^^ in1_byte) + let val2 := BitVec.cast h $ FFmul02 in2_byte ^^^ FFmul03 in3_byte ^^^ in0_byte ^^^ in1_byte let out2 := BitVec.partInstall hi lo val2 out2 - let val3 := BitVec.cast h₁.symm $ (FFmul02 in3_byte ^^^ FFmul03 in0_byte ^^^ in1_byte ^^^ in2_byte) + let val3 := BitVec.cast h $ FFmul02 in3_byte ^^^ FFmul03 in0_byte ^^^ in1_byte ^^^ in2_byte let out3 := BitVec.partInstall hi lo val3 out3 - have _ : 3 - c < 4 - c := by omega - MixColumns_aux (c + 1) in0 in1 in2 in3 out0 out1 out2 out3 FFmul02 FFmul03 - termination_by (4 - c) + MixColumns_aux c' in0 in1 in2 in3 out0 out1 out2 out3 FFmul02 FFmul03 def MixColumns (op : BitVec 128) (FFmul02 : BitVec 8 -> BitVec 8) (FFmul03 : BitVec 8 -> BitVec 8) : BitVec 128 := let in0 := - extractLsb 103 96 op ++ extractLsb 71 64 op ++ - extractLsb 39 32 op ++ extractLsb 7 0 op + extractLsb' 96 8 op ++ extractLsb' 64 8 op ++ + extractLsb' 32 8 op ++ extractLsb' 0 8 op let in1 := - extractLsb 111 104 op ++ extractLsb 79 72 op ++ - extractLsb 47 40 op ++ extractLsb 15 8 op + extractLsb' 104 8 op ++ extractLsb' 72 8 op ++ + extractLsb' 40 8 op ++ extractLsb' 8 8 op let in2 := - extractLsb 119 112 op ++ extractLsb 87 80 op ++ - extractLsb 55 48 op ++ extractLsb 23 16 op + extractLsb' 112 8 op ++ extractLsb' 80 8 op ++ + extractLsb' 48 8 op ++ extractLsb' 16 8 op let in3 := - extractLsb 127 120 op ++ extractLsb 95 88 op ++ - extractLsb 63 56 op ++ extractLsb 31 24 op + extractLsb' 120 8 op ++ extractLsb' 88 8 op ++ + extractLsb' 56 8 op ++ extractLsb' 24 8 op let (out0, out1, out2, out3) := (BitVec.zero 32, BitVec.zero 32, BitVec.zero 32, BitVec.zero 32) let (out0, out1, out2, out3) := - MixColumns_aux 0 in0 in1 in2 in3 out0 out1 out2 out3 FFmul02 FFmul03 - extractLsb 31 24 out3 ++ extractLsb 31 24 out2 ++ - extractLsb 31 24 out1 ++ extractLsb 31 24 out0 ++ - extractLsb 23 16 out3 ++ extractLsb 23 16 out2 ++ - extractLsb 23 16 out1 ++ extractLsb 23 16 out0 ++ - extractLsb 15 8 out3 ++ extractLsb 15 8 out2 ++ - extractLsb 15 8 out1 ++ extractLsb 15 8 out0 ++ - extractLsb 7 0 out3 ++ extractLsb 7 0 out2 ++ - extractLsb 7 0 out1 ++ extractLsb 7 0 out0 + MixColumns_aux 4 in0 in1 in2 in3 out0 out1 out2 out3 FFmul02 FFmul03 + extractLsb' 24 8 out3 ++ extractLsb' 24 8 out2 ++ + extractLsb' 24 8 out1 ++ extractLsb' 24 8 out0 ++ + extractLsb' 16 8 out3 ++ extractLsb' 16 8 out2 ++ + extractLsb' 16 8 out1 ++ extractLsb' 16 8 out0 ++ + extractLsb' 8 8 out3 ++ extractLsb' 8 8 out2 ++ + extractLsb' 8 8 out1 ++ extractLsb' 8 8 out0 ++ + extractLsb' 0 8 out3 ++ extractLsb' 0 8 out2 ++ + extractLsb' 0 8 out1 ++ extractLsb' 0 8 out0 end AESCommon diff --git a/Specs/AESV8.lean b/Specs/AESV8.lean index 75ecbf5d..44f9c7db 100644 --- a/Specs/AESV8.lean +++ b/Specs/AESV8.lean @@ -111,10 +111,7 @@ def AESHWCtr32EncryptBlocks_helper {Param : AESArm.KBR} (in_blocks : BitVec m) if i >= len then acc else let lo := m - (i + 1) * 128 - let hi := lo + 127 - have h5 : hi - lo + 1 = 128 := by omega - let curr_block : BitVec 128 := - BitVec.cast h5 $ BitVec.extractLsb hi lo in_blocks + let curr_block : BitVec 128 := BitVec.extractLsb' lo 128 in_blocks have h4 : 128 = Param.block_size := by cases h3 · rename_i h; simp only [h, AESArm.AES128KBR, AESArm.BlockSize] diff --git a/Specs/GCM.lean b/Specs/GCM.lean index 04f50184..17915aa4 100644 --- a/Specs/GCM.lean +++ b/Specs/GCM.lean @@ -23,15 +23,10 @@ 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 := - let msb_hi := l - 1 - let msb_lo := s - let lsb_hi := s - 1 - let lsb_lo := 0 - have h₁ : lsb_hi - lsb_lo + 1 = s := by omega - let upper := extractLsb msb_hi msb_lo X - let lower := BitVec.cast h₁ (extractLsb lsb_hi lsb_lo X) + 0b1#s - have h₂ : msb_hi - msb_lo + 1 + s = l := by omega - BitVec.cast h₂ (upper ++ lower) + let upper := extractLsb' s (l - s) X + let lower := (extractLsb' 0 s X) + 0b1#s + have h : l - s + s = l := by omega + (upper ++ lower).cast h def mul_aux (i : Nat) (X : BitVec 128) (Z : BitVec 128) (V : BitVec 128) : BitVec 128 := @@ -55,10 +50,8 @@ def GHASH_aux (i : Nat) (H : BitVec 128) (X : BitVec n) (Y : BitVec 128) Y else let lo := (n/128 - 1 - i) * 128 - let hi := lo + 127 - have h₀ : hi - lo + 1 = 128 := by omega - let Xi := extractLsb hi lo X - let res := Y ^^^ (BitVec.cast h₀ Xi) + let Xi := extractLsb' lo 128 X + let res := Y ^^^ Xi let Y := mul res H GHASH_aux (i + 1) H X Y h termination_by (n / 128 - i) @@ -75,10 +68,10 @@ def GCTR_aux (CIPH : Cipher (n := 128) (m := m)) else let lo := (n - i - 1) * 128 let hi := lo + 127 - have h : hi - lo + 1 = 128 := by omega - let Xi := extractLsb hi lo X - let Yi := BitVec.cast h Xi ^^^ CIPH ICB K - let Y := BitVec.partInstall hi lo (BitVec.cast h.symm Yi) Y + have h : 128 = hi - lo + 1 := by omega + 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) GCTR_aux CIPH (i + 1) n K ICB X Y termination_by (n - i) diff --git a/Specs/GCMV8.lean b/Specs/GCMV8.lean index 7483e332..8b51ae15 100644 --- a/Specs/GCMV8.lean +++ b/Specs/GCMV8.lean @@ -21,10 +21,10 @@ open BitVec ------------------------------------------------------------------------------ def hi (x : BitVec 128) : BitVec 64 := - extractLsb 127 64 x + extractLsb' 64 64 x def lo (x : BitVec 128) : BitVec 64 := - extractLsb 63 0 x + extractLsb' 0 64 x ------------------------------------------------------------------------------ -- Functions related to galois field operations diff --git a/Tests/AES-GCM/AESV8ProgramTests.lean b/Tests/AES-GCM/AESV8ProgramTests.lean index 4389d415..085fe7a2 100644 --- a/Tests/AES-GCM/AESV8ProgramTests.lean +++ b/Tests/AES-GCM/AESV8ProgramTests.lean @@ -360,28 +360,28 @@ def final_state1 : ArmState := aes_hw_ctr32_encrypt_blocks_test 88 1 in_block rounds key_schedule ivec def final_buf1 : BitVec 640 := read_mem_bytes 80 out_address final_state1 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 +example: final_buf1 = (BitVec.zero 512) ++ (extractLsb' 0 128 (revflat buf_res_128)) := by native_decide -- -- len = 2 def final_state2 : ArmState := aes_hw_ctr32_encrypt_blocks_test 89 2 in_block rounds key_schedule ivec def final_buf2 : BitVec 640 := read_mem_bytes 80 out_address final_state2 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 +example: final_buf2 = (BitVec.zero 384) ++ (extractLsb' 0 256 (revflat buf_res_128)) := by native_decide -- len = 3 def final_state3 : ArmState := aes_hw_ctr32_encrypt_blocks_test 128 3 in_block rounds key_schedule ivec def final_buf3 : BitVec 640 := read_mem_bytes 80 out_address final_state3 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 +example: final_buf3 = (BitVec.zero 256) ++ (extractLsb' 0 384 (revflat buf_res_128)) := by native_decide -- len = 4 def final_state4 : ArmState := aes_hw_ctr32_encrypt_blocks_test 190 4 in_block rounds key_schedule ivec def final_buf4 : BitVec 640 := read_mem_bytes 80 out_address final_state4 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 +example: final_buf4 = (BitVec.zero 128) ++ (extractLsb' 0 512 (revflat buf_res_128)) := by native_decide -- len = 5 def final_state5 : ArmState := diff --git a/Tests/AES-GCM/GCMSpecTests.lean b/Tests/AES-GCM/GCMSpecTests.lean index cf255810..2bd8598e 100644 --- a/Tests/AES-GCM/GCMSpecTests.lean +++ b/Tests/AES-GCM/GCMSpecTests.lean @@ -14,8 +14,8 @@ namespace GCMInitV8SpecTest def flatten_H := BitVec.flatten GCMProgramTestParams.H def spec_table := GCMV8.GCMInitV8 flatten_H -example : extractLsb (12 * 128) 0 (revflat spec_table) - = extractLsb (12 * 128) 0 (revflat GCMProgramTestParams.Htable) +example : extractLsb' 0 (12 * 128) (revflat spec_table) + = extractLsb' 0 (12 * 128) (revflat GCMProgramTestParams.Htable) := by native_decide end GCMInitV8SpecTest