From aafe462959bab915c87b2f589305e1780574c428 Mon Sep 17 00:00:00 2001 From: Shilpi Goel Date: Sun, 3 Mar 2024 15:58:14 -0600 Subject: [PATCH] Updates to sym_one tactic Eliding use of `update_invariants` for now. --- Arm/Attr.lean | 6 + Arm/BitVec.lean | 10 + Arm/Exec.lean | 11 +- Arm/Insts/BR/Compare_branch.lean | 6 +- Arm/Insts/BR/Cond_branch_imm.lean | 6 +- Arm/Insts/BR/Uncond_branch_imm.lean | 4 +- Arm/Insts/BR/Uncond_branch_reg.lean | 2 +- Arm/Insts/Common.lean | 11 +- Arm/Insts/DPI/Add_sub_imm.lean | 2 +- Arm/Insts/DPI/Bitfield.lean | 2 +- Arm/Insts/DPI/Logical_imm.lean | 2 +- Arm/Insts/DPI/PC_rel_addressing.lean | 2 +- Arm/Insts/DPR/Add_sub_carry.lean | 2 +- Arm/Insts/DPR/Add_sub_shifted_reg.lean | 2 +- Arm/Insts/DPR/Conditional_select.lean | 2 +- Arm/Insts/DPR/Data_processing_one_source.lean | 4 +- Arm/Insts/DPR/Logical_shifted_reg.lean | 2 +- Arm/Insts/DPSFP/Advanced_simd_copy.lean | 2 +- Arm/Insts/DPSFP/Advanced_simd_extract.lean | 2 +- .../Advanced_simd_modified_immediate.lean | 2 +- .../DPSFP/Advanced_simd_scalar_copy.lean | 2 +- .../DPSFP/Advanced_simd_three_different.lean | 4 +- Arm/Insts/DPSFP/Advanced_simd_three_same.lean | 16 +- .../DPSFP/Advanced_simd_two_reg_misc.lean | 2 +- .../DPSFP/Conversion_between_FP_and_Int.lean | 6 +- Arm/Insts/DPSFP/Crypto_four_reg.lean | 2 +- Arm/Insts/DPSFP/Crypto_three_reg_sha512.lean | 2 +- Arm/Insts/DPSFP/Crypto_two_reg_sha512.lean | 2 +- .../LDST/Advanced_simd_multiple_struct.lean | 6 +- Arm/Insts/LDST/Reg_imm.lean | 12 +- Arm/Insts/LDST/Reg_pair.lean | 12 +- Arm/MinTheory.lean | 102 ++++ Arm/State.lean | 14 +- Proofs/Proofs.lean | 1 - Proofs/SHA512_AssocRepr.lean | 573 ------------------ Proofs/Sha512_block_armv8.lean | 109 +--- Tactics/Sym.lean | 149 ++--- lean-toolchain | 2 +- 38 files changed, 299 insertions(+), 799 deletions(-) create mode 100644 Arm/MinTheory.lean delete mode 100644 Proofs/SHA512_AssocRepr.lean diff --git a/Arm/Attr.lean b/Arm/Attr.lean index 4de079b3..b39055a1 100644 --- 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 index 00504a56..c7f42eef 100644 --- 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 index cf4cd455..08db1ee6 100644 --- 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 index 75599e85..42739e8c 100644 --- 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 index a7a27635..96993f4d 100644 --- 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 index cd3be358..c5ba8b2a 100644 --- 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 index ea341d67..9a738176 100644 --- 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 index 706e4871..1ff0068f 100644 --- 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 index ef65437c..5dba92b1 100644 --- 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 index 14d1fcd9..89f31fb1 100644 --- 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 index c83fe36f..f07931a5 100644 --- 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 index 3f436de1..e7630fd7 100644 --- 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 index f9de1dde..7d662604 100644 --- 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 index 7fc9e636..506c7453 100644 --- 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 index a8427ae2..739bbbe1 100644 --- 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 index 733e47f8..9251bdfd 100644 --- 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 index b65089fb..894a82b7 100644 --- 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 index 8e6c1615..2f39e204 100644 --- 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 index be3325a6..3fe45d6d 100644 --- 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 index ea10cb31..94ff8a4c 100644 --- 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 index e475483c..9bbf4b81 100644 --- 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 index 1fd1fb71..3c32b9fe 100644 --- 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 index 3d9bf265..4104ba9e 100644 --- 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 index 5ef00873..878f623c 100644 --- 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 diff --git a/Arm/Insts/DPSFP/Conversion_between_FP_and_Int.lean b/Arm/Insts/DPSFP/Conversion_between_FP_and_Int.lean index 45d554bb..32c55693 100644 --- a/Arm/Insts/DPSFP/Conversion_between_FP_and_Int.lean +++ b/Arm/Insts/DPSFP/Conversion_between_FP_and_Int.lean @@ -15,7 +15,7 @@ namespace DPSFP open BitVec -@[simp] +@[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) @@ -39,7 +39,7 @@ def fmov_general_aux (intsize : Nat) (fltsize : Nat) (op : FPConvOp) s | _ => write_err (StateError.Other s!"fmov_general_aux called with non-FMOV op!") s -@[simp] +@[state_simp_rules] def exec_fmov_general (inst : Conversion_between_FP_and_Int_cls) (s : ArmState): ArmState := let intsize := 32 <<< inst.sf.toNat @@ -71,7 +71,7 @@ def exec_fmov_general fmov_general_aux intsize decode_fltsize op part inst s H | _ => write_err (StateError.Other s!"exec_fmov_general called with non-FMOV instructions!") s -@[simp] +@[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 diff --git a/Arm/Insts/DPSFP/Crypto_four_reg.lean b/Arm/Insts/DPSFP/Crypto_four_reg.lean index ffb3a33c..52d577cd 100644 --- a/Arm/Insts/DPSFP/Crypto_four_reg.lean +++ b/Arm/Insts/DPSFP/Crypto_four_reg.lean @@ -16,7 +16,7 @@ namespace DPSFP open BitVec -@[simp] +@[state_simp_rules] def exec_crypto_four_reg (inst : Crypto_four_reg_cls) (s : ArmState) : ArmState := -- This function assumes IsFeatureImplemented(FEAT_SHA3) is true -- and that AArch64.CheckFPAdvSIMDEnabled() returns successfully diff --git a/Arm/Insts/DPSFP/Crypto_three_reg_sha512.lean b/Arm/Insts/DPSFP/Crypto_three_reg_sha512.lean index 2d135487..3e8a2f7f 100644 --- a/Arm/Insts/DPSFP/Crypto_three_reg_sha512.lean +++ b/Arm/Insts/DPSFP/Crypto_three_reg_sha512.lean @@ -69,7 +69,7 @@ def sha512su1 (x : BitVec 128) (y : BitVec 128) (w : BitVec 128) let result := vtmp_127_64 ++ vtmp_63_0 result -@[simp] +@[state_simp_rules] def exec_crypto_three_reg_sha512 (inst : Crypto_three_reg_sha512_cls) (s : ArmState) : ArmState := open BitVec in diff --git a/Arm/Insts/DPSFP/Crypto_two_reg_sha512.lean b/Arm/Insts/DPSFP/Crypto_two_reg_sha512.lean index 4c101727..d46a2be7 100644 --- a/Arm/Insts/DPSFP/Crypto_two_reg_sha512.lean +++ b/Arm/Insts/DPSFP/Crypto_two_reg_sha512.lean @@ -28,7 +28,7 @@ def sha512su0 (x : BitVec 128) (w : BitVec 128) let result := vtmp_127_64 ++ vtmp_63_0 result -@[simp] +@[state_simp_rules] def exec_crypto_two_reg_sha512 (inst : Crypto_two_reg_sha512_cls) (s : ArmState) : ArmState := open BitVec in diff --git a/Arm/Insts/LDST/Advanced_simd_multiple_struct.lean b/Arm/Insts/LDST/Advanced_simd_multiple_struct.lean index 11acc13a..8d9eb70c 100644 --- a/Arm/Insts/LDST/Advanced_simd_multiple_struct.lean +++ b/Arm/Insts/LDST/Advanced_simd_multiple_struct.lean @@ -24,7 +24,7 @@ structure Multiple_struct_inst_fields where Rt : BitVec 5 deriving DecidableEq, Repr -@[simp] +@[state_simp_rules] def ld1_st1_operation (wback : Bool) (inst : Multiple_struct_inst_fields) (inst_str : String) (s : ArmState) (H_opcode : inst.opcode ∈ @@ -127,7 +127,7 @@ def ld1_st1_operation (wback : Bool) (inst : Multiple_struct_inst_fields) let s := write_pc ((read_pc s) + 4#64) s s -@[simp] +@[state_simp_rules] def exec_advanced_simd_multiple_struct (inst : Advanced_simd_multiple_struct_cls) (s : ArmState) : ArmState := open BitVec in @@ -143,7 +143,7 @@ def exec_advanced_simd_multiple_struct (StateError.Unimplemented s!"Unsupported instruction {inst} encountered!") s -@[simp] +@[state_simp_rules] def exec_advanced_simd_multiple_struct_post_indexed (inst : Advanced_simd_multiple_struct_post_indexed_cls) (s : ArmState) : ArmState := open BitVec in diff --git a/Arm/Insts/LDST/Reg_imm.lean b/Arm/Insts/LDST/Reg_imm.lean index c8ac770b..118199be 100644 --- a/Arm/Insts/LDST/Reg_imm.lean +++ b/Arm/Insts/LDST/Reg_imm.lean @@ -28,7 +28,7 @@ deriving DecidableEq, Repr instance : ToString Reg_imm_cls where toString a := toString (repr a) -@[simp] +@[state_simp_rules] def reg_imm_operation (inst_str : String) (op : BitVec 1) (wback : Bool) (postindex : Bool) (SIMD? : Bool) (datasize : Nat) (regsize : Option Nat) (Rn : BitVec 5) @@ -59,12 +59,12 @@ def reg_imm_operation (inst_str : String) (op : BitVec 1) else s -@[simp] +@[state_simp_rules] def reg_imm_constrain_unpredictable (wback : Bool) (SIMD? : Bool) (Rn : BitVec 5) (Rt : BitVec 5) : Bool := if SIMD? then false else wback && Rn == Rt && Rn != 31#5 -@[simp] +@[state_simp_rules] def supported_reg_imm (size : BitVec 2) (opc : BitVec 2) (SIMD? : Bool) : Bool := match size, opc, SIMD? with | 0b00#2, 0b00#2, false => true -- STRB, 32-bit, GPR @@ -79,7 +79,7 @@ def supported_reg_imm (size : BitVec 2) (opc : BitVec 2) (SIMD? : Bool) : Bool : | 0b00#2, 0b11#2, true => true -- LDR, 128-bit, SIMD&FP | _, _, _ => false -- other instructions that are not supported or illegal -@[simp] +@[state_simp_rules] def exec_reg_imm_common (inst : Reg_imm_cls) (inst_str : String) (s : ArmState) : ArmState := let scale := @@ -112,7 +112,7 @@ def exec_reg_imm_common let s' := write_pc ((read_pc s) + 4#64) s' s' -@[simp] +@[state_simp_rules] def exec_reg_imm_unsigned_offset (inst : Reg_unsigned_imm_cls) (s : ArmState) : ArmState := let (extracted_inst : Reg_imm_cls) := @@ -126,7 +126,7 @@ def exec_reg_imm_unsigned_offset imm := Sum.inl inst.imm12 } exec_reg_imm_common extracted_inst s!"{inst}" s -@[simp] +@[state_simp_rules] def exec_reg_imm_post_indexed (inst : Reg_imm_post_indexed_cls) (s : ArmState) : ArmState := let (extracted_inst : Reg_imm_cls) := diff --git a/Arm/Insts/LDST/Reg_pair.lean b/Arm/Insts/LDST/Reg_pair.lean index 966ffb8b..1a3d85e4 100644 --- a/Arm/Insts/LDST/Reg_pair.lean +++ b/Arm/Insts/LDST/Reg_pair.lean @@ -28,7 +28,7 @@ deriving DecidableEq, Repr instance : ToString Reg_pair_cls where toString a := toString (repr a) -@[simp] +@[state_simp_rules] def reg_pair_constrain_unpredictable (wback : Bool) (inst : Reg_pair_cls) : Bool := match inst.SIMD?, inst.L? with | false, false => wback && ((inst.Rt == inst.Rn) || inst.Rt2 == inst.Rn) && inst.Rn != 31#5 @@ -37,7 +37,7 @@ def reg_pair_constrain_unpredictable (wback : Bool) (inst : Reg_pair_cls) : Bool | true, false => false | true, true => inst.Rt == inst.Rt2 -@[simp] +@[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 := @@ -82,7 +82,7 @@ def reg_pair_operation (inst : Reg_pair_cls) (inst_str : String) (signed : Bool) else s -@[simp] +@[state_simp_rules] def exec_reg_pair_common (inst : Reg_pair_cls) (inst_str : String) (s : ArmState) : ArmState := if -- UNDEFINED case for none-SIMD Reg Pair not inst.SIMD? && @@ -110,7 +110,7 @@ def exec_reg_pair_common (inst : Reg_pair_cls) (inst_str : String) (s : ArmState let s' := write_pc ((read_pc s) + 4#64) s' s' -@[simp] +@[state_simp_rules] def exec_reg_pair_pre_indexed (inst : Reg_pair_pre_indexed_cls) (s : ArmState) : ArmState := let (extracted_inst : Reg_pair_cls) := @@ -125,7 +125,7 @@ def exec_reg_pair_pre_indexed Rt := inst.Rt } exec_reg_pair_common extracted_inst s!"{inst}" s -@[simp] +@[state_simp_rules] def exec_reg_pair_post_indexed (inst : Reg_pair_post_indexed_cls) (s : ArmState) : ArmState := let (extracted_inst : Reg_pair_cls) := @@ -140,7 +140,7 @@ def exec_reg_pair_post_indexed Rt := inst.Rt } exec_reg_pair_common extracted_inst s!"{inst}" s -@[simp] +@[state_simp_rules] def exec_reg_pair_signed_offset (inst : Reg_pair_signed_offset_cls) (s : ArmState) : ArmState := let (extracted_inst : Reg_pair_cls) := diff --git a/Arm/MinTheory.lean b/Arm/MinTheory.lean new file mode 100644 index 00000000..89e870d1 --- /dev/null +++ b/Arm/MinTheory.lean @@ -0,0 +1,102 @@ +import Arm.Attr + +-- These lemmas are from lean/Init/SimpLemmas.lean. +attribute [minimal_theory] eq_self +attribute [minimal_theory] ne_eq +attribute [minimal_theory] ite_true +attribute [minimal_theory] ite_false +attribute [minimal_theory] dite_true +attribute [minimal_theory] dite_false +attribute [minimal_theory] ite_self +attribute [minimal_theory] and_true +attribute [minimal_theory] true_and +attribute [minimal_theory] and_false +attribute [minimal_theory] false_and +attribute [minimal_theory] and_self +attribute [minimal_theory] and_not_self +attribute [minimal_theory] not_and_self +attribute [minimal_theory] and_imp +attribute [minimal_theory] not_and +attribute [minimal_theory] or_self +attribute [minimal_theory] or_true +attribute [minimal_theory] true_or +attribute [minimal_theory] or_false +attribute [minimal_theory] false_or +attribute [minimal_theory] iff_self +attribute [minimal_theory] iff_true +attribute [minimal_theory] true_iff +attribute [minimal_theory] iff_false +attribute [minimal_theory] false_iff +attribute [minimal_theory] false_implies +attribute [minimal_theory] implies_true +attribute [minimal_theory] true_implies +attribute [minimal_theory] not_false_eq_true +attribute [minimal_theory] not_true_eq_false +attribute [minimal_theory] not_iff_self +attribute [minimal_theory] and_self_left +attribute [minimal_theory] and_self_right +attribute [minimal_theory] and_congr_right_iff +attribute [minimal_theory] and_congr_left_iff +attribute [minimal_theory] and_iff_left_iff_imp +attribute [minimal_theory] and_iff_right_iff_imp +attribute [minimal_theory] iff_self_and +attribute [minimal_theory] iff_and_self +attribute [minimal_theory] or_self_left +attribute [minimal_theory] or_self_right +attribute [minimal_theory] or_iff_right_of_imp +attribute [minimal_theory] or_iff_left_of_imp +attribute [minimal_theory] or_iff_left_iff_imp +attribute [minimal_theory] or_iff_right_iff_imp +attribute [minimal_theory] Bool.or_false +attribute [minimal_theory] Bool.or_true +attribute [minimal_theory] Bool.false_or +attribute [minimal_theory] Bool.true_or +attribute [minimal_theory] Bool.or_self +attribute [minimal_theory] Bool.or_eq_true +attribute [minimal_theory] Bool.and_false +attribute [minimal_theory] Bool.and_true +attribute [minimal_theory] Bool.false_and +attribute [minimal_theory] Bool.true_and +attribute [minimal_theory] Bool.and_self +attribute [minimal_theory] Bool.and_eq_true +attribute [minimal_theory] Bool.not_not +attribute [minimal_theory] Bool.not_true +attribute [minimal_theory] Bool.not_false +attribute [minimal_theory] Bool.not_beq_true +attribute [minimal_theory] Bool.not_beq_false +attribute [minimal_theory] Bool.not_eq_true' +attribute [minimal_theory] Bool.not_eq_false' +attribute [minimal_theory] Bool.beq_to_eq +attribute [minimal_theory] Bool.not_beq_to_not_eq +attribute [minimal_theory] Bool.not_eq_true +attribute [minimal_theory] Bool.not_eq_false +attribute [minimal_theory] decide_eq_true_eq +attribute [minimal_theory] decide_not +attribute [minimal_theory] not_decide_eq_true +attribute [minimal_theory] heq_eq_eq +attribute [minimal_theory] cond_true +attribute [minimal_theory] cond_false +attribute [minimal_theory] beq_self_eq_true +attribute [minimal_theory] beq_self_eq_true' +attribute [minimal_theory] bne_self_eq_false +attribute [minimal_theory] bne_self_eq_false' +attribute [minimal_theory] decide_False +attribute [minimal_theory] decide_True +attribute [minimal_theory] bne_iff_ne +attribute [minimal_theory] Nat.le_zero_eq + +attribute [minimal_theory] Nat.zero_add +attribute [minimal_theory] Nat.zero_eq +attribute [minimal_theory] Nat.succ.injEq +attribute [minimal_theory] Nat.succ_ne_zero +attribute [minimal_theory] Nat.sub_zero + +@[minimal_theory] +theorem option_get_bang_of_some [Inhabited α] (v : α) : + Option.get! (some v) = v := by rfl +attribute [minimal_theory] Option.isNone_some + +attribute [minimal_theory] Fin.isValue +attribute [minimal_theory] Fin.zero_eta + +-- attribute [minimal_theory] ↓reduceIte diff --git a/Arm/State.lean b/Arm/State.lean index e3582ce1..97cec7b9 100644 --- a/Arm/State.lean +++ b/Arm/State.lean @@ -7,6 +7,7 @@ import Lean.Data.Format import Arm.BitVec import Arm.Map import Arm.Attr +import Arm.MinTheory ------------------------------------------------------------------------------ ------------------------------------------------------------------------------ @@ -309,6 +310,7 @@ theorem fetch_inst_of_w (addr : BitVec 64) (fld : StateField) (val : (state_valu split <;> simp_all! -- There is no StateField that overwrites the program. +@[state_simp_rules] theorem w_program (sf : StateField) (v : state_value sf) (s : ArmState): (w sf v s).program = s.program := by intros @@ -362,7 +364,7 @@ def write_gpr_zr (n : Nat) (idx : BitVec 5) (val : BitVec n) (s : ArmState) example (n : Nat) (idx : BitVec 5) (val : BitVec n) (s : ArmState) : read_gpr n idx (write_gpr n idx val s) = BitVec.zeroExtend n (BitVec.zeroExtend 64 val) := by - state_simp + simp [state_simp_rules, minimal_theory] @[state_simp_rules] def read_sfp (width : Nat) (idx : BitVec 5) (s : ArmState) : BitVec width := @@ -463,21 +465,17 @@ end Load_program_and_fetch_inst ---------------------------------------------------------------------- --- Adding some basic simp lemmas to `state_simp_rules`: -attribute [state_simp_rules] ne_eq -attribute [state_simp_rules] not_false_eq_true - example : read_flag flag (write_flag flag val s) = val := by - state_simp + simp only [state_simp_rules, minimal_theory] example (h : flag1 ≠ flag2) : read_flag flag1 (write_flag flag2 val s) = read_flag flag1 s := by - state_simp_all + simp_all only [state_simp_rules, minimal_theory] example : read_gpr width idx (write_flag flag2 val s) = read_gpr width idx s := by - state_simp + simp only [state_simp_rules, minimal_theory] end State diff --git a/Proofs/Proofs.lean b/Proofs/Proofs.lean index e9c27759..4af1195b 100644 --- a/Proofs/Proofs.lean +++ b/Proofs/Proofs.lean @@ -7,5 +7,4 @@ import «Proofs».MultiInsts import «Proofs».Test import «Proofs».Sha512_block_armv8_rules import «Proofs».Sha512_block_armv8 -import «Proofs».SHA512_AssocRepr diff --git a/Proofs/SHA512_AssocRepr.lean b/Proofs/SHA512_AssocRepr.lean deleted file mode 100644 index 6847873d..00000000 --- a/Proofs/SHA512_AssocRepr.lean +++ /dev/null @@ -1,573 +0,0 @@ -/- -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.Exec -import Arm.MemoryProofs - -section SHA512_proof - -open BitVec - -def sha512_program : Map (BitVec 64) (BitVec 32) := - [(0x1264c0#64 , 0xa9bf7bfd#32), -- stp x29, x30, [sp, #-16]! - (0x1264c4#64 , 0x910003fd#32), -- mov x29, sp - (0x1264c8#64 , 0x4cdf2030#32), -- ld1 {v16.16b-v19.16b}, [x1], #64 - (0x1264cc#64 , 0x4cdf2034#32), -- ld1 {v20.16b-v23.16b}, [x1], #64 - (0x1264d0#64 , 0x4c402c00#32), -- ld1 {v0.2d-v3.2d}, [x0] - (0x1264d4#64 , 0xd0000463#32), -- adrp x3, 1b4000 - (0x1264d8#64 , 0x910c0063#32), -- add x3, x3, #0x300 - (0x1264dc#64 , 0x4e200a10#32), -- rev64 v16.16b, v16.16b - (0x1264e0#64 , 0x4e200a31#32), -- rev64 v17.16b, v17.16b - (0x1264e4#64 , 0x4e200a52#32), -- rev64 v18.16b, v18.16b - (0x1264e8#64 , 0x4e200a73#32), -- rev64 v19.16b, v19.16b - (0x1264ec#64 , 0x4e200a94#32), -- rev64 v20.16b, v20.16b - (0x1264f0#64 , 0x4e200ab5#32), -- rev64 v21.16b, v21.16b - (0x1264f4#64 , 0x4e200ad6#32), -- rev64 v22.16b, v22.16b - (0x1264f8#64 , 0x4e200af7#32), -- rev64 v23.16b, v23.16b - (0x1264fc#64 , 0x14000001#32), -- b 126500 - (0x126500#64 , 0x4cdf7c78#32), -- ld1 {v24.2d}, [x3], #16 - (0x126504#64 , 0xf1000442#32), -- subs x2, x2, #0x1 - (0x126508#64 , 0xd1020024#32), -- sub x4, x1, #0x80 - (0x12650c#64 , 0x4ea01c1a#32), -- mov v26.16b, v0.16b - (0x126510#64 , 0x4ea11c3b#32), -- mov v27.16b, v1.16b - (0x126514#64 , 0x4ea21c5c#32), -- mov v28.16b, v2.16b - (0x126518#64 , 0x4ea31c7d#32), -- mov v29.16b, v3.16b - (0x12651c#64 , 0x9a841021#32), -- csel x1, x1, x4, ne // ne = any - (0x126520#64 , 0x4ef08718#32), -- add v24.2d, v24.2d, v16.2d - (0x126524#64 , 0x4cdf7c79#32), -- ld1 {v25.2d}, [x3], #16 - (0x126528#64 , 0x6e184318#32), -- ext v24.16b, v24.16b, v24.16b, #8 - (0x12652c#64 , 0x6e034045#32), -- ext v5.16b, v2.16b, v3.16b, #8 - (0x126530#64 , 0x6e024026#32), -- ext v6.16b, v1.16b, v2.16b, #8 - (0x126534#64 , 0x4ef88463#32), -- add v3.2d, v3.2d, v24.2d - (0x126538#64 , 0xcec08230#32), -- sha512su0 v16.2d, v17.2d - (0x12653c#64 , 0x6e154287#32), -- ext v7.16b, v20.16b, v21.16b, #8 - (0x126540#64 , 0xce6680a3#32), -- sha512h q3, q5, v6.2d - (0x126544#64 , 0xce678af0#32), -- sha512su1 v16.2d, v23.2d, v7.2d - (0x126548#64 , 0x4ee38424#32), -- add v4.2d, v1.2d, v3.2d - (0x12654c#64 , 0xce608423#32), -- sha512h2 q3, q1, v0.2d - (0x126550#64 , 0x4ef18739#32), -- add v25.2d, v25.2d, v17.2d - (0x126554#64 , 0x4cdf7c78#32), -- ld1 {v24.2d}, [x3], #16 - (0x126558#64 , 0x6e194339#32), -- ext v25.16b, v25.16b, v25.16b, #8 - (0x12655c#64 , 0x6e024085#32), -- ext v5.16b, v4.16b, v2.16b, #8 - (0x126560#64 , 0x6e044006#32), -- ext v6.16b, v0.16b, v4.16b, #8 - (0x126564#64 , 0x4ef98442#32), -- add v2.2d, v2.2d, v25.2d - (0x126568#64 , 0xcec08251#32), -- sha512su0 v17.2d, v18.2d - (0x12656c#64 , 0x6e1642a7#32), -- ext v7.16b, v21.16b, v22.16b, #8 - (0x126570#64 , 0xce6680a2#32), -- sha512h q2, q5, v6.2d - (0x126574#64 , 0xce678a11#32), -- sha512su1 v17.2d, v16.2d, v7.2d - (0x126578#64 , 0x4ee28401#32), -- add v1.2d, v0.2d, v2.2d - (0x12657c#64 , 0xce638402#32), -- sha512h2 q2, q0, v3.2d - (0x126580#64 , 0x4ef28718#32), -- add v24.2d, v24.2d, v18.2d - (0x126584#64 , 0x4cdf7c79#32), -- ld1 {v25.2d}, [x3], #16 - (0x126588#64 , 0x6e184318#32), -- ext v24.16b, v24.16b, v24.16b, #8 - (0x12658c#64 , 0x6e044025#32), -- ext v5.16b, v1.16b, v4.16b, #8 - (0x126590#64 , 0x6e014066#32), -- ext v6.16b, v3.16b, v1.16b, #8 - (0x126594#64 , 0x4ef88484#32), -- add v4.2d, v4.2d, v24.2d - (0x126598#64 , 0xcec08272#32), -- sha512su0 v18.2d, v19.2d - (0x12659c#64 , 0x6e1742c7#32), -- ext v7.16b, v22.16b, v23.16b, #8 - (0x1265a0#64 , 0xce6680a4#32), -- sha512h q4, q5, v6.2d - (0x1265a4#64 , 0xce678a32#32), -- sha512su1 v18.2d, v17.2d, v7.2d - (0x1265a8#64 , 0x4ee48460#32), -- add v0.2d, v3.2d, v4.2d - (0x1265ac#64 , 0xce628464#32), -- sha512h2 q4, q3, v2.2d - (0x1265b0#64 , 0x4ef38739#32), -- add v25.2d, v25.2d, v19.2d - (0x1265b4#64 , 0x4cdf7c78#32), -- ld1 {v24.2d}, [x3], #16 - (0x1265b8#64 , 0x6e194339#32), -- ext v25.16b, v25.16b, v25.16b, #8 - (0x1265bc#64 , 0x6e014005#32), -- ext v5.16b, v0.16b, v1.16b, #8 - (0x1265c0#64 , 0x6e004046#32), -- ext v6.16b, v2.16b, v0.16b, #8 - (0x1265c4#64 , 0x4ef98421#32), -- add v1.2d, v1.2d, v25.2d - (0x1265c8#64 , 0xcec08293#32), -- sha512su0 v19.2d, v20.2d - (0x1265cc#64 , 0x6e1042e7#32), -- ext v7.16b, v23.16b, v16.16b, #8 - (0x1265d0#64 , 0xce6680a1#32), -- sha512h q1, q5, v6.2d - (0x1265d4#64 , 0xce678a53#32), -- sha512su1 v19.2d, v18.2d, v7.2d - (0x1265d8#64 , 0x4ee18443#32), -- add v3.2d, v2.2d, v1.2d - (0x1265dc#64 , 0xce648441#32), -- sha512h2 q1, q2, v4.2d - (0x1265e0#64 , 0x4ef48718#32), -- add v24.2d, v24.2d, v20.2d - (0x1265e4#64 , 0x4cdf7c79#32), -- ld1 {v25.2d}, [x3], #16 - (0x1265e8#64 , 0x6e184318#32), -- ext v24.16b, v24.16b, v24.16b, #8 - (0x1265ec#64 , 0x6e004065#32), -- ext v5.16b, v3.16b, v0.16b, #8 - (0x1265f0#64 , 0x6e034086#32), -- ext v6.16b, v4.16b, v3.16b, #8 - (0x1265f4#64 , 0x4ef88400#32), -- add v0.2d, v0.2d, v24.2d - (0x1265f8#64 , 0xcec082b4#32), -- sha512su0 v20.2d, v21.2d - (0x1265fc#64 , 0x6e114207#32), -- ext v7.16b, v16.16b, v17.16b, #8 - (0x126600#64 , 0xce6680a0#32), -- sha512h q0, q5, v6.2d - (0x126604#64 , 0xce678a74#32), -- sha512su1 v20.2d, v19.2d, v7.2d - (0x126608#64 , 0x4ee08482#32), -- add v2.2d, v4.2d, v0.2d - (0x12660c#64 , 0xce618480#32), -- sha512h2 q0, q4, v1.2d - (0x126610#64 , 0x4ef58739#32), -- add v25.2d, v25.2d, v21.2d - (0x126614#64 , 0x4cdf7c78#32), -- ld1 {v24.2d}, [x3], #16 - (0x126618#64 , 0x6e194339#32), -- ext v25.16b, v25.16b, v25.16b, #8 - (0x12661c#64 , 0x6e034045#32), -- ext v5.16b, v2.16b, v3.16b, #8 - (0x126620#64 , 0x6e024026#32), -- ext v6.16b, v1.16b, v2.16b, #8 - (0x126624#64 , 0x4ef98463#32), -- add v3.2d, v3.2d, v25.2d - (0x126628#64 , 0xcec082d5#32), -- sha512su0 v21.2d, v22.2d - (0x12662c#64 , 0x6e124227#32), -- ext v7.16b, v17.16b, v18.16b, #8 - (0x126630#64 , 0xce6680a3#32), -- sha512h q3, q5, v6.2d - (0x126634#64 , 0xce678a95#32), -- sha512su1 v21.2d, v20.2d, v7.2d - (0x126638#64 , 0x4ee38424#32), -- add v4.2d, v1.2d, v3.2d - (0x12663c#64 , 0xce608423#32), -- sha512h2 q3, q1, v0.2d - (0x126640#64 , 0x4ef68718#32), -- add v24.2d, v24.2d, v22.2d - (0x126644#64 , 0x4cdf7c79#32), -- ld1 {v25.2d}, [x3], #16 - (0x126648#64 , 0x6e184318#32), -- ext v24.16b, v24.16b, v24.16b, #8 - (0x12664c#64 , 0x6e024085#32), -- ext v5.16b, v4.16b, v2.16b, #8 - (0x126650#64 , 0x6e044006#32), -- ext v6.16b, v0.16b, v4.16b, #8 - (0x126654#64 , 0x4ef88442#32), -- add v2.2d, v2.2d, v24.2d - (0x126658#64 , 0xcec082f6#32), -- sha512su0 v22.2d, v23.2d - (0x12665c#64 , 0x6e134247#32), -- ext v7.16b, v18.16b, v19.16b, #8 - (0x126660#64 , 0xce6680a2#32), -- sha512h q2, q5, v6.2d - (0x126664#64 , 0xce678ab6#32), -- sha512su1 v22.2d, v21.2d, v7.2d - (0x126668#64 , 0x4ee28401#32), -- add v1.2d, v0.2d, v2.2d - (0x12666c#64 , 0xce638402#32), -- sha512h2 q2, q0, v3.2d - (0x126670#64 , 0x4ef78739#32), -- add v25.2d, v25.2d, v23.2d - (0x126674#64 , 0x4cdf7c78#32), -- ld1 {v24.2d}, [x3], #16 - (0x126678#64 , 0x6e194339#32), -- ext v25.16b, v25.16b, v25.16b, #8 - (0x12667c#64 , 0x6e044025#32), -- ext v5.16b, v1.16b, v4.16b, #8 - (0x126680#64 , 0x6e014066#32), -- ext v6.16b, v3.16b, v1.16b, #8 - (0x126684#64 , 0x4ef98484#32), -- add v4.2d, v4.2d, v25.2d - (0x126688#64 , 0xcec08217#32), -- sha512su0 v23.2d, v16.2d - (0x12668c#64 , 0x6e144267#32), -- ext v7.16b, v19.16b, v20.16b, #8 - (0x126690#64 , 0xce6680a4#32), -- sha512h q4, q5, v6.2d - (0x126694#64 , 0xce678ad7#32), -- sha512su1 v23.2d, v22.2d, v7.2d - (0x126698#64 , 0x4ee48460#32), -- add v0.2d, v3.2d, v4.2d - (0x12669c#64 , 0xce628464#32), -- sha512h2 q4, q3, v2.2d - (0x1266a0#64 , 0x4ef08718#32), -- add v24.2d, v24.2d, v16.2d - (0x1266a4#64 , 0x4cdf7c79#32), -- ld1 {v25.2d}, [x3], #16 - (0x1266a8#64 , 0x6e184318#32), -- ext v24.16b, v24.16b, v24.16b, #8 - (0x1266ac#64 , 0x6e014005#32), -- ext v5.16b, v0.16b, v1.16b, #8 - (0x1266b0#64 , 0x6e004046#32), -- ext v6.16b, v2.16b, v0.16b, #8 - (0x1266b4#64 , 0x4ef88421#32), -- add v1.2d, v1.2d, v24.2d - (0x1266b8#64 , 0xcec08230#32), -- sha512su0 v16.2d, v17.2d - (0x1266bc#64 , 0x6e154287#32), -- ext v7.16b, v20.16b, v21.16b, #8 - (0x1266c0#64 , 0xce6680a1#32), -- sha512h q1, q5, v6.2d - (0x1266c4#64 , 0xce678af0#32), -- sha512su1 v16.2d, v23.2d, v7.2d - (0x1266c8#64 , 0x4ee18443#32), -- add v3.2d, v2.2d, v1.2d - (0x1266cc#64 , 0xce648441#32), -- sha512h2 q1, q2, v4.2d - (0x1266d0#64 , 0x4ef18739#32), -- add v25.2d, v25.2d, v17.2d - (0x1266d4#64 , 0x4cdf7c78#32), -- ld1 {v24.2d}, [x3], #16 - (0x1266d8#64 , 0x6e194339#32), -- ext v25.16b, v25.16b, v25.16b, #8 - (0x1266dc#64 , 0x6e004065#32), -- ext v5.16b, v3.16b, v0.16b, #8 - (0x1266e0#64 , 0x6e034086#32), -- ext v6.16b, v4.16b, v3.16b, #8 - (0x1266e4#64 , 0x4ef98400#32), -- add v0.2d, v0.2d, v25.2d - (0x1266e8#64 , 0xcec08251#32), -- sha512su0 v17.2d, v18.2d - (0x1266ec#64 , 0x6e1642a7#32), -- ext v7.16b, v21.16b, v22.16b, #8 - (0x1266f0#64 , 0xce6680a0#32), -- sha512h q0, q5, v6.2d - (0x1266f4#64 , 0xce678a11#32), -- sha512su1 v17.2d, v16.2d, v7.2d - (0x1266f8#64 , 0x4ee08482#32), -- add v2.2d, v4.2d, v0.2d - (0x1266fc#64 , 0xce618480#32), -- sha512h2 q0, q4, v1.2d - (0x126700#64 , 0x4ef28718#32), -- add v24.2d, v24.2d, v18.2d - (0x126704#64 , 0x4cdf7c79#32), -- ld1 {v25.2d}, [x3], #16 - (0x126708#64 , 0x6e184318#32), -- ext v24.16b, v24.16b, v24.16b, #8 - (0x12670c#64 , 0x6e034045#32), -- ext v5.16b, v2.16b, v3.16b, #8 - (0x126710#64 , 0x6e024026#32), -- ext v6.16b, v1.16b, v2.16b, #8 - (0x126714#64 , 0x4ef88463#32), -- add v3.2d, v3.2d, v24.2d - (0x126718#64 , 0xcec08272#32), -- sha512su0 v18.2d, v19.2d - (0x12671c#64 , 0x6e1742c7#32), -- ext v7.16b, v22.16b, v23.16b, #8 - (0x126720#64 , 0xce6680a3#32), -- sha512h q3, q5, v6.2d - (0x126724#64 , 0xce678a32#32), -- sha512su1 v18.2d, v17.2d, v7.2d - (0x126728#64 , 0x4ee38424#32), -- add v4.2d, v1.2d, v3.2d - (0x12672c#64 , 0xce608423#32), -- sha512h2 q3, q1, v0.2d - (0x126730#64 , 0x4ef38739#32), -- add v25.2d, v25.2d, v19.2d - (0x126734#64 , 0x4cdf7c78#32), -- ld1 {v24.2d}, [x3], #16 - (0x126738#64 , 0x6e194339#32), -- ext v25.16b, v25.16b, v25.16b, #8 - (0x12673c#64 , 0x6e024085#32), -- ext v5.16b, v4.16b, v2.16b, #8 - (0x126740#64 , 0x6e044006#32), -- ext v6.16b, v0.16b, v4.16b, #8 - (0x126744#64 , 0x4ef98442#32), -- add v2.2d, v2.2d, v25.2d - (0x126748#64 , 0xcec08293#32), -- sha512su0 v19.2d, v20.2d - (0x12674c#64 , 0x6e1042e7#32), -- ext v7.16b, v23.16b, v16.16b, #8 - (0x126750#64 , 0xce6680a2#32), -- sha512h q2, q5, v6.2d - (0x126754#64 , 0xce678a53#32), -- sha512su1 v19.2d, v18.2d, v7.2d - (0x126758#64 , 0x4ee28401#32), -- add v1.2d, v0.2d, v2.2d - (0x12675c#64 , 0xce638402#32), -- sha512h2 q2, q0, v3.2d - (0x126760#64 , 0x4ef48718#32), -- add v24.2d, v24.2d, v20.2d - (0x126764#64 , 0x4cdf7c79#32), -- ld1 {v25.2d}, [x3], #16 - (0x126768#64 , 0x6e184318#32), -- ext v24.16b, v24.16b, v24.16b, #8 - (0x12676c#64 , 0x6e044025#32), -- ext v5.16b, v1.16b, v4.16b, #8 - (0x126770#64 , 0x6e014066#32), -- ext v6.16b, v3.16b, v1.16b, #8 - (0x126774#64 , 0x4ef88484#32), -- add v4.2d, v4.2d, v24.2d - (0x126778#64 , 0xcec082b4#32), -- sha512su0 v20.2d, v21.2d - (0x12677c#64 , 0x6e114207#32), -- ext v7.16b, v16.16b, v17.16b, #8 - (0x126780#64 , 0xce6680a4#32), -- sha512h q4, q5, v6.2d - (0x126784#64 , 0xce678a74#32), -- sha512su1 v20.2d, v19.2d, v7.2d - (0x126788#64 , 0x4ee48460#32), -- add v0.2d, v3.2d, v4.2d - (0x12678c#64 , 0xce628464#32), -- sha512h2 q4, q3, v2.2d - (0x126790#64 , 0x4ef58739#32), -- add v25.2d, v25.2d, v21.2d - (0x126794#64 , 0x4cdf7c78#32), -- ld1 {v24.2d}, [x3], #16 - (0x126798#64 , 0x6e194339#32), -- ext v25.16b, v25.16b, v25.16b, #8 - (0x12679c#64 , 0x6e014005#32), -- ext v5.16b, v0.16b, v1.16b, #8 - (0x1267a0#64 , 0x6e004046#32), -- ext v6.16b, v2.16b, v0.16b, #8 - (0x1267a4#64 , 0x4ef98421#32), -- add v1.2d, v1.2d, v25.2d - (0x1267a8#64 , 0xcec082d5#32), -- sha512su0 v21.2d, v22.2d - (0x1267ac#64 , 0x6e124227#32), -- ext v7.16b, v17.16b, v18.16b, #8 - (0x1267b0#64 , 0xce6680a1#32), -- sha512h q1, q5, v6.2d - (0x1267b4#64 , 0xce678a95#32), -- sha512su1 v21.2d, v20.2d, v7.2d - (0x1267b8#64 , 0x4ee18443#32), -- add v3.2d, v2.2d, v1.2d - (0x1267bc#64 , 0xce648441#32), -- sha512h2 q1, q2, v4.2d - (0x1267c0#64 , 0x4ef68718#32), -- add v24.2d, v24.2d, v22.2d - (0x1267c4#64 , 0x4cdf7c79#32), -- ld1 {v25.2d}, [x3], #16 - (0x1267c8#64 , 0x6e184318#32), -- ext v24.16b, v24.16b, v24.16b, #8 - (0x1267cc#64 , 0x6e004065#32), -- ext v5.16b, v3.16b, v0.16b, #8 - (0x1267d0#64 , 0x6e034086#32), -- ext v6.16b, v4.16b, v3.16b, #8 - (0x1267d4#64 , 0x4ef88400#32), -- add v0.2d, v0.2d, v24.2d - (0x1267d8#64 , 0xcec082f6#32), -- sha512su0 v22.2d, v23.2d - (0x1267dc#64 , 0x6e134247#32), -- ext v7.16b, v18.16b, v19.16b, #8 - (0x1267e0#64 , 0xce6680a0#32), -- sha512h q0, q5, v6.2d - (0x1267e4#64 , 0xce678ab6#32), -- sha512su1 v22.2d, v21.2d, v7.2d - (0x1267e8#64 , 0x4ee08482#32), -- add v2.2d, v4.2d, v0.2d - (0x1267ec#64 , 0xce618480#32), -- sha512h2 q0, q4, v1.2d - (0x1267f0#64 , 0x4ef78739#32), -- add v25.2d, v25.2d, v23.2d - (0x1267f4#64 , 0x4cdf7c78#32), -- ld1 {v24.2d}, [x3], #16 - (0x1267f8#64 , 0x6e194339#32), -- ext v25.16b, v25.16b, v25.16b, #8 - (0x1267fc#64 , 0x6e034045#32), -- ext v5.16b, v2.16b, v3.16b, #8 - (0x126800#64 , 0x6e024026#32), -- ext v6.16b, v1.16b, v2.16b, #8 - (0x126804#64 , 0x4ef98463#32), -- add v3.2d, v3.2d, v25.2d - (0x126808#64 , 0xcec08217#32), -- sha512su0 v23.2d, v16.2d - (0x12680c#64 , 0x6e144267#32), -- ext v7.16b, v19.16b, v20.16b, #8 - (0x126810#64 , 0xce6680a3#32), -- sha512h q3, q5, v6.2d - (0x126814#64 , 0xce678ad7#32), -- sha512su1 v23.2d, v22.2d, v7.2d - (0x126818#64 , 0x4ee38424#32), -- add v4.2d, v1.2d, v3.2d - (0x12681c#64 , 0xce608423#32), -- sha512h2 q3, q1, v0.2d - (0x126820#64 , 0x4ef08718#32), -- add v24.2d, v24.2d, v16.2d - (0x126824#64 , 0x4cdf7c79#32), -- ld1 {v25.2d}, [x3], #16 - (0x126828#64 , 0x6e184318#32), -- ext v24.16b, v24.16b, v24.16b, #8 - (0x12682c#64 , 0x6e024085#32), -- ext v5.16b, v4.16b, v2.16b, #8 - (0x126830#64 , 0x6e044006#32), -- ext v6.16b, v0.16b, v4.16b, #8 - (0x126834#64 , 0x4ef88442#32), -- add v2.2d, v2.2d, v24.2d - (0x126838#64 , 0xcec08230#32), -- sha512su0 v16.2d, v17.2d - (0x12683c#64 , 0x6e154287#32), -- ext v7.16b, v20.16b, v21.16b, #8 - (0x126840#64 , 0xce6680a2#32), -- sha512h q2, q5, v6.2d - (0x126844#64 , 0xce678af0#32), -- sha512su1 v16.2d, v23.2d, v7.2d - (0x126848#64 , 0x4ee28401#32), -- add v1.2d, v0.2d, v2.2d - (0x12684c#64 , 0xce638402#32), -- sha512h2 q2, q0, v3.2d - (0x126850#64 , 0x4ef18739#32), -- add v25.2d, v25.2d, v17.2d - (0x126854#64 , 0x4cdf7c78#32), -- ld1 {v24.2d}, [x3], #16 - (0x126858#64 , 0x6e194339#32), -- ext v25.16b, v25.16b, v25.16b, #8 - (0x12685c#64 , 0x6e044025#32), -- ext v5.16b, v1.16b, v4.16b, #8 - (0x126860#64 , 0x6e014066#32), -- ext v6.16b, v3.16b, v1.16b, #8 - (0x126864#64 , 0x4ef98484#32), -- add v4.2d, v4.2d, v25.2d - (0x126868#64 , 0xcec08251#32), -- sha512su0 v17.2d, v18.2d - (0x12686c#64 , 0x6e1642a7#32), -- ext v7.16b, v21.16b, v22.16b, #8 - (0x126870#64 , 0xce6680a4#32), -- sha512h q4, q5, v6.2d - (0x126874#64 , 0xce678a11#32), -- sha512su1 v17.2d, v16.2d, v7.2d - (0x126878#64 , 0x4ee48460#32), -- add v0.2d, v3.2d, v4.2d - (0x12687c#64 , 0xce628464#32), -- sha512h2 q4, q3, v2.2d - (0x126880#64 , 0x4ef28718#32), -- add v24.2d, v24.2d, v18.2d - (0x126884#64 , 0x4cdf7c79#32), -- ld1 {v25.2d}, [x3], #16 - (0x126888#64 , 0x6e184318#32), -- ext v24.16b, v24.16b, v24.16b, #8 - (0x12688c#64 , 0x6e014005#32), -- ext v5.16b, v0.16b, v1.16b, #8 - (0x126890#64 , 0x6e004046#32), -- ext v6.16b, v2.16b, v0.16b, #8 - (0x126894#64 , 0x4ef88421#32), -- add v1.2d, v1.2d, v24.2d - (0x126898#64 , 0xcec08272#32), -- sha512su0 v18.2d, v19.2d - (0x12689c#64 , 0x6e1742c7#32), -- ext v7.16b, v22.16b, v23.16b, #8 - (0x1268a0#64 , 0xce6680a1#32), -- sha512h q1, q5, v6.2d - (0x1268a4#64 , 0xce678a32#32), -- sha512su1 v18.2d, v17.2d, v7.2d - (0x1268a8#64 , 0x4ee18443#32), -- add v3.2d, v2.2d, v1.2d - (0x1268ac#64 , 0xce648441#32), -- sha512h2 q1, q2, v4.2d - (0x1268b0#64 , 0x4ef38739#32), -- add v25.2d, v25.2d, v19.2d - (0x1268b4#64 , 0x4cdf7c78#32), -- ld1 {v24.2d}, [x3], #16 - (0x1268b8#64 , 0x6e194339#32), -- ext v25.16b, v25.16b, v25.16b, #8 - (0x1268bc#64 , 0x6e004065#32), -- ext v5.16b, v3.16b, v0.16b, #8 - (0x1268c0#64 , 0x6e034086#32), -- ext v6.16b, v4.16b, v3.16b, #8 - (0x1268c4#64 , 0x4ef98400#32), -- add v0.2d, v0.2d, v25.2d - (0x1268c8#64 , 0xcec08293#32), -- sha512su0 v19.2d, v20.2d - (0x1268cc#64 , 0x6e1042e7#32), -- ext v7.16b, v23.16b, v16.16b, #8 - (0x1268d0#64 , 0xce6680a0#32), -- sha512h q0, q5, v6.2d - (0x1268d4#64 , 0xce678a53#32), -- sha512su1 v19.2d, v18.2d, v7.2d - (0x1268d8#64 , 0x4ee08482#32), -- add v2.2d, v4.2d, v0.2d - (0x1268dc#64 , 0xce618480#32), -- sha512h2 q0, q4, v1.2d - (0x1268e0#64 , 0x4ef48718#32), -- add v24.2d, v24.2d, v20.2d - (0x1268e4#64 , 0x4cdf7c79#32), -- ld1 {v25.2d}, [x3], #16 - (0x1268e8#64 , 0x6e184318#32), -- ext v24.16b, v24.16b, v24.16b, #8 - (0x1268ec#64 , 0x6e034045#32), -- ext v5.16b, v2.16b, v3.16b, #8 - (0x1268f0#64 , 0x6e024026#32), -- ext v6.16b, v1.16b, v2.16b, #8 - (0x1268f4#64 , 0x4ef88463#32), -- add v3.2d, v3.2d, v24.2d - (0x1268f8#64 , 0xcec082b4#32), -- sha512su0 v20.2d, v21.2d - (0x1268fc#64 , 0x6e114207#32), -- ext v7.16b, v16.16b, v17.16b, #8 - (0x126900#64 , 0xce6680a3#32), -- sha512h q3, q5, v6.2d - (0x126904#64 , 0xce678a74#32), -- sha512su1 v20.2d, v19.2d, v7.2d - (0x126908#64 , 0x4ee38424#32), -- add v4.2d, v1.2d, v3.2d - (0x12690c#64 , 0xce608423#32), -- sha512h2 q3, q1, v0.2d - (0x126910#64 , 0x4ef58739#32), -- add v25.2d, v25.2d, v21.2d - (0x126914#64 , 0x4cdf7c78#32), -- ld1 {v24.2d}, [x3], #16 - (0x126918#64 , 0x6e194339#32), -- ext v25.16b, v25.16b, v25.16b, #8 - (0x12691c#64 , 0x6e024085#32), -- ext v5.16b, v4.16b, v2.16b, #8 - (0x126920#64 , 0x6e044006#32), -- ext v6.16b, v0.16b, v4.16b, #8 - (0x126924#64 , 0x4ef98442#32), -- add v2.2d, v2.2d, v25.2d - (0x126928#64 , 0xcec082d5#32), -- sha512su0 v21.2d, v22.2d - (0x12692c#64 , 0x6e124227#32), -- ext v7.16b, v17.16b, v18.16b, #8 - (0x126930#64 , 0xce6680a2#32), -- sha512h q2, q5, v6.2d - (0x126934#64 , 0xce678a95#32), -- sha512su1 v21.2d, v20.2d, v7.2d - (0x126938#64 , 0x4ee28401#32), -- add v1.2d, v0.2d, v2.2d - (0x12693c#64 , 0xce638402#32), -- sha512h2 q2, q0, v3.2d - (0x126940#64 , 0x4ef68718#32), -- add v24.2d, v24.2d, v22.2d - (0x126944#64 , 0x4cdf7c79#32), -- ld1 {v25.2d}, [x3], #16 - (0x126948#64 , 0x6e184318#32), -- ext v24.16b, v24.16b, v24.16b, #8 - (0x12694c#64 , 0x6e044025#32), -- ext v5.16b, v1.16b, v4.16b, #8 - (0x126950#64 , 0x6e014066#32), -- ext v6.16b, v3.16b, v1.16b, #8 - (0x126954#64 , 0x4ef88484#32), -- add v4.2d, v4.2d, v24.2d - (0x126958#64 , 0xcec082f6#32), -- sha512su0 v22.2d, v23.2d - (0x12695c#64 , 0x6e134247#32), -- ext v7.16b, v18.16b, v19.16b, #8 - (0x126960#64 , 0xce6680a4#32), -- sha512h q4, q5, v6.2d - (0x126964#64 , 0xce678ab6#32), -- sha512su1 v22.2d, v21.2d, v7.2d - (0x126968#64 , 0x4ee48460#32), -- add v0.2d, v3.2d, v4.2d - (0x12696c#64 , 0xce628464#32), -- sha512h2 q4, q3, v2.2d - (0x126970#64 , 0x4ef78739#32), -- add v25.2d, v25.2d, v23.2d - (0x126974#64 , 0x4cdf7c78#32), -- ld1 {v24.2d}, [x3], #16 - (0x126978#64 , 0x6e194339#32), -- ext v25.16b, v25.16b, v25.16b, #8 - (0x12697c#64 , 0x6e014005#32), -- ext v5.16b, v0.16b, v1.16b, #8 - (0x126980#64 , 0x6e004046#32), -- ext v6.16b, v2.16b, v0.16b, #8 - (0x126984#64 , 0x4ef98421#32), -- add v1.2d, v1.2d, v25.2d - (0x126988#64 , 0xcec08217#32), -- sha512su0 v23.2d, v16.2d - (0x12698c#64 , 0x6e144267#32), -- ext v7.16b, v19.16b, v20.16b, #8 - (0x126990#64 , 0xce6680a1#32), -- sha512h q1, q5, v6.2d - (0x126994#64 , 0xce678ad7#32), -- sha512su1 v23.2d, v22.2d, v7.2d - (0x126998#64 , 0x4ee18443#32), -- add v3.2d, v2.2d, v1.2d - (0x12699c#64 , 0xce648441#32), -- sha512h2 q1, q2, v4.2d - (0x1269a0#64 , 0x4ef08718#32), -- add v24.2d, v24.2d, v16.2d - (0x1269a4#64 , 0x4cdf7c79#32), -- ld1 {v25.2d}, [x3], #16 - (0x1269a8#64 , 0x6e184318#32), -- ext v24.16b, v24.16b, v24.16b, #8 - (0x1269ac#64 , 0x6e004065#32), -- ext v5.16b, v3.16b, v0.16b, #8 - (0x1269b0#64 , 0x6e034086#32), -- ext v6.16b, v4.16b, v3.16b, #8 - (0x1269b4#64 , 0x4ef88400#32), -- add v0.2d, v0.2d, v24.2d - (0x1269b8#64 , 0xcec08230#32), -- sha512su0 v16.2d, v17.2d - (0x1269bc#64 , 0x6e154287#32), -- ext v7.16b, v20.16b, v21.16b, #8 - (0x1269c0#64 , 0xce6680a0#32), -- sha512h q0, q5, v6.2d - (0x1269c4#64 , 0xce678af0#32), -- sha512su1 v16.2d, v23.2d, v7.2d - (0x1269c8#64 , 0x4ee08482#32), -- add v2.2d, v4.2d, v0.2d - (0x1269cc#64 , 0xce618480#32), -- sha512h2 q0, q4, v1.2d - (0x1269d0#64 , 0x4ef18739#32), -- add v25.2d, v25.2d, v17.2d - (0x1269d4#64 , 0x4cdf7c78#32), -- ld1 {v24.2d}, [x3], #16 - (0x1269d8#64 , 0x6e194339#32), -- ext v25.16b, v25.16b, v25.16b, #8 - (0x1269dc#64 , 0x6e034045#32), -- ext v5.16b, v2.16b, v3.16b, #8 - (0x1269e0#64 , 0x6e024026#32), -- ext v6.16b, v1.16b, v2.16b, #8 - (0x1269e4#64 , 0x4ef98463#32), -- add v3.2d, v3.2d, v25.2d - (0x1269e8#64 , 0xcec08251#32), -- sha512su0 v17.2d, v18.2d - (0x1269ec#64 , 0x6e1642a7#32), -- ext v7.16b, v21.16b, v22.16b, #8 - (0x1269f0#64 , 0xce6680a3#32), -- sha512h q3, q5, v6.2d - (0x1269f4#64 , 0xce678a11#32), -- sha512su1 v17.2d, v16.2d, v7.2d - (0x1269f8#64 , 0x4ee38424#32), -- add v4.2d, v1.2d, v3.2d - (0x1269fc#64 , 0xce608423#32), -- sha512h2 q3, q1, v0.2d - (0x126a00#64 , 0x4ef28718#32), -- add v24.2d, v24.2d, v18.2d - (0x126a04#64 , 0x4cdf7c79#32), -- ld1 {v25.2d}, [x3], #16 - (0x126a08#64 , 0x6e184318#32), -- ext v24.16b, v24.16b, v24.16b, #8 - (0x126a0c#64 , 0x6e024085#32), -- ext v5.16b, v4.16b, v2.16b, #8 - (0x126a10#64 , 0x6e044006#32), -- ext v6.16b, v0.16b, v4.16b, #8 - (0x126a14#64 , 0x4ef88442#32), -- add v2.2d, v2.2d, v24.2d - (0x126a18#64 , 0xcec08272#32), -- sha512su0 v18.2d, v19.2d - (0x126a1c#64 , 0x6e1742c7#32), -- ext v7.16b, v22.16b, v23.16b, #8 - (0x126a20#64 , 0xce6680a2#32), -- sha512h q2, q5, v6.2d - (0x126a24#64 , 0xce678a32#32), -- sha512su1 v18.2d, v17.2d, v7.2d - (0x126a28#64 , 0x4ee28401#32), -- add v1.2d, v0.2d, v2.2d - (0x126a2c#64 , 0xce638402#32), -- sha512h2 q2, q0, v3.2d - (0x126a30#64 , 0x4ef38739#32), -- add v25.2d, v25.2d, v19.2d - (0x126a34#64 , 0x4cdf7c78#32), -- ld1 {v24.2d}, [x3], #16 - (0x126a38#64 , 0x6e194339#32), -- ext v25.16b, v25.16b, v25.16b, #8 - (0x126a3c#64 , 0x6e044025#32), -- ext v5.16b, v1.16b, v4.16b, #8 - (0x126a40#64 , 0x6e014066#32), -- ext v6.16b, v3.16b, v1.16b, #8 - (0x126a44#64 , 0x4ef98484#32), -- add v4.2d, v4.2d, v25.2d - (0x126a48#64 , 0xcec08293#32), -- sha512su0 v19.2d, v20.2d - (0x126a4c#64 , 0x6e1042e7#32), -- ext v7.16b, v23.16b, v16.16b, #8 - (0x126a50#64 , 0xce6680a4#32), -- sha512h q4, q5, v6.2d - (0x126a54#64 , 0xce678a53#32), -- sha512su1 v19.2d, v18.2d, v7.2d - (0x126a58#64 , 0x4ee48460#32), -- add v0.2d, v3.2d, v4.2d - (0x126a5c#64 , 0xce628464#32), -- sha512h2 q4, q3, v2.2d - (0x126a60#64 , 0x4ef48718#32), -- add v24.2d, v24.2d, v20.2d - (0x126a64#64 , 0x4cdf7c79#32), -- ld1 {v25.2d}, [x3], #16 - (0x126a68#64 , 0x6e184318#32), -- ext v24.16b, v24.16b, v24.16b, #8 - (0x126a6c#64 , 0x6e014005#32), -- ext v5.16b, v0.16b, v1.16b, #8 - (0x126a70#64 , 0x6e004046#32), -- ext v6.16b, v2.16b, v0.16b, #8 - (0x126a74#64 , 0x4ef88421#32), -- add v1.2d, v1.2d, v24.2d - (0x126a78#64 , 0xcec082b4#32), -- sha512su0 v20.2d, v21.2d - (0x126a7c#64 , 0x6e114207#32), -- ext v7.16b, v16.16b, v17.16b, #8 - (0x126a80#64 , 0xce6680a1#32), -- sha512h q1, q5, v6.2d - (0x126a84#64 , 0xce678a74#32), -- sha512su1 v20.2d, v19.2d, v7.2d - (0x126a88#64 , 0x4ee18443#32), -- add v3.2d, v2.2d, v1.2d - (0x126a8c#64 , 0xce648441#32), -- sha512h2 q1, q2, v4.2d - (0x126a90#64 , 0x4ef58739#32), -- add v25.2d, v25.2d, v21.2d - (0x126a94#64 , 0x4cdf7c78#32), -- ld1 {v24.2d}, [x3], #16 - (0x126a98#64 , 0x6e194339#32), -- ext v25.16b, v25.16b, v25.16b, #8 - (0x126a9c#64 , 0x6e004065#32), -- ext v5.16b, v3.16b, v0.16b, #8 - (0x126aa0#64 , 0x6e034086#32), -- ext v6.16b, v4.16b, v3.16b, #8 - (0x126aa4#64 , 0x4ef98400#32), -- add v0.2d, v0.2d, v25.2d - (0x126aa8#64 , 0xcec082d5#32), -- sha512su0 v21.2d, v22.2d - (0x126aac#64 , 0x6e124227#32), -- ext v7.16b, v17.16b, v18.16b, #8 - (0x126ab0#64 , 0xce6680a0#32), -- sha512h q0, q5, v6.2d - (0x126ab4#64 , 0xce678a95#32), -- sha512su1 v21.2d, v20.2d, v7.2d - (0x126ab8#64 , 0x4ee08482#32), -- add v2.2d, v4.2d, v0.2d - (0x126abc#64 , 0xce618480#32), -- sha512h2 q0, q4, v1.2d - (0x126ac0#64 , 0x4ef68718#32), -- add v24.2d, v24.2d, v22.2d - (0x126ac4#64 , 0x4cdf7c79#32), -- ld1 {v25.2d}, [x3], #16 - (0x126ac8#64 , 0x6e184318#32), -- ext v24.16b, v24.16b, v24.16b, #8 - (0x126acc#64 , 0x6e034045#32), -- ext v5.16b, v2.16b, v3.16b, #8 - (0x126ad0#64 , 0x6e024026#32), -- ext v6.16b, v1.16b, v2.16b, #8 - (0x126ad4#64 , 0x4ef88463#32), -- add v3.2d, v3.2d, v24.2d - (0x126ad8#64 , 0xcec082f6#32), -- sha512su0 v22.2d, v23.2d - (0x126adc#64 , 0x6e134247#32), -- ext v7.16b, v18.16b, v19.16b, #8 - (0x126ae0#64 , 0xce6680a3#32), -- sha512h q3, q5, v6.2d - (0x126ae4#64 , 0xce678ab6#32), -- sha512su1 v22.2d, v21.2d, v7.2d - (0x126ae8#64 , 0x4ee38424#32), -- add v4.2d, v1.2d, v3.2d - (0x126aec#64 , 0xce608423#32), -- sha512h2 q3, q1, v0.2d - (0x126af0#64 , 0x4ef78739#32), -- add v25.2d, v25.2d, v23.2d - (0x126af4#64 , 0x4cdf7c78#32), -- ld1 {v24.2d}, [x3], #16 - (0x126af8#64 , 0x6e194339#32), -- ext v25.16b, v25.16b, v25.16b, #8 - (0x126afc#64 , 0x6e024085#32), -- ext v5.16b, v4.16b, v2.16b, #8 - (0x126b00#64 , 0x6e044006#32), -- ext v6.16b, v0.16b, v4.16b, #8 - (0x126b04#64 , 0x4ef98442#32), -- add v2.2d, v2.2d, v25.2d - (0x126b08#64 , 0xcec08217#32), -- sha512su0 v23.2d, v16.2d - (0x126b0c#64 , 0x6e144267#32), -- ext v7.16b, v19.16b, v20.16b, #8 - (0x126b10#64 , 0xce6680a2#32), -- sha512h q2, q5, v6.2d - (0x126b14#64 , 0xce678ad7#32), -- sha512su1 v23.2d, v22.2d, v7.2d - (0x126b18#64 , 0x4ee28401#32), -- add v1.2d, v0.2d, v2.2d - (0x126b1c#64 , 0xce638402#32), -- sha512h2 q2, q0, v3.2d - (0x126b20#64 , 0x4cdf7c79#32), -- ld1 {v25.2d}, [x3], #16 - (0x126b24#64 , 0x4ef08718#32), -- add v24.2d, v24.2d, v16.2d - (0x126b28#64 , 0x4cdf7030#32), -- ld1 {v16.16b}, [x1], #16 - (0x126b2c#64 , 0x6e184318#32), -- ext v24.16b, v24.16b, v24.16b, #8 - (0x126b30#64 , 0x6e044025#32), -- ext v5.16b, v1.16b, v4.16b, #8 - (0x126b34#64 , 0x6e014066#32), -- ext v6.16b, v3.16b, v1.16b, #8 - (0x126b38#64 , 0x4ef88484#32), -- add v4.2d, v4.2d, v24.2d - (0x126b3c#64 , 0xce6680a4#32), -- sha512h q4, q5, v6.2d - (0x126b40#64 , 0x4e200a10#32), -- rev64 v16.16b, v16.16b - (0x126b44#64 , 0x4ee48460#32), -- add v0.2d, v3.2d, v4.2d - (0x126b48#64 , 0xce628464#32), -- sha512h2 q4, q3, v2.2d - (0x126b4c#64 , 0x4cdf7c78#32), -- ld1 {v24.2d}, [x3], #16 - (0x126b50#64 , 0x4ef18739#32), -- add v25.2d, v25.2d, v17.2d - (0x126b54#64 , 0x4cdf7031#32), -- ld1 {v17.16b}, [x1], #16 - (0x126b58#64 , 0x6e194339#32), -- ext v25.16b, v25.16b, v25.16b, #8 - (0x126b5c#64 , 0x6e014005#32), -- ext v5.16b, v0.16b, v1.16b, #8 - (0x126b60#64 , 0x6e004046#32), -- ext v6.16b, v2.16b, v0.16b, #8 - (0x126b64#64 , 0x4ef98421#32), -- add v1.2d, v1.2d, v25.2d - (0x126b68#64 , 0xce6680a1#32), -- sha512h q1, q5, v6.2d - (0x126b6c#64 , 0x4e200a31#32), -- rev64 v17.16b, v17.16b - (0x126b70#64 , 0x4ee18443#32), -- add v3.2d, v2.2d, v1.2d - (0x126b74#64 , 0xce648441#32), -- sha512h2 q1, q2, v4.2d - (0x126b78#64 , 0x4cdf7c79#32), -- ld1 {v25.2d}, [x3], #16 - (0x126b7c#64 , 0x4ef28718#32), -- add v24.2d, v24.2d, v18.2d - (0x126b80#64 , 0x4cdf7032#32), -- ld1 {v18.16b}, [x1], #16 - (0x126b84#64 , 0x6e184318#32), -- ext v24.16b, v24.16b, v24.16b, #8 - (0x126b88#64 , 0x6e004065#32), -- ext v5.16b, v3.16b, v0.16b, #8 - (0x126b8c#64 , 0x6e034086#32), -- ext v6.16b, v4.16b, v3.16b, #8 - (0x126b90#64 , 0x4ef88400#32), -- add v0.2d, v0.2d, v24.2d - (0x126b94#64 , 0xce6680a0#32), -- sha512h q0, q5, v6.2d - (0x126b98#64 , 0x4e200a52#32), -- rev64 v18.16b, v18.16b - (0x126b9c#64 , 0x4ee08482#32), -- add v2.2d, v4.2d, v0.2d - (0x126ba0#64 , 0xce618480#32), -- sha512h2 q0, q4, v1.2d - (0x126ba4#64 , 0x4cdf7c78#32), -- ld1 {v24.2d}, [x3], #16 - (0x126ba8#64 , 0x4ef38739#32), -- add v25.2d, v25.2d, v19.2d - (0x126bac#64 , 0x4cdf7033#32), -- ld1 {v19.16b}, [x1], #16 - (0x126bb0#64 , 0x6e194339#32), -- ext v25.16b, v25.16b, v25.16b, #8 - (0x126bb4#64 , 0x6e034045#32), -- ext v5.16b, v2.16b, v3.16b, #8 - (0x126bb8#64 , 0x6e024026#32), -- ext v6.16b, v1.16b, v2.16b, #8 - (0x126bbc#64 , 0x4ef98463#32), -- add v3.2d, v3.2d, v25.2d - (0x126bc0#64 , 0xce6680a3#32), -- sha512h q3, q5, v6.2d - (0x126bc4#64 , 0x4e200a73#32), -- rev64 v19.16b, v19.16b - (0x126bc8#64 , 0x4ee38424#32), -- add v4.2d, v1.2d, v3.2d - (0x126bcc#64 , 0xce608423#32), -- sha512h2 q3, q1, v0.2d - (0x126bd0#64 , 0x4cdf7c79#32), -- ld1 {v25.2d}, [x3], #16 - (0x126bd4#64 , 0x4ef48718#32), -- add v24.2d, v24.2d, v20.2d - (0x126bd8#64 , 0x4cdf7034#32), -- ld1 {v20.16b}, [x1], #16 - (0x126bdc#64 , 0x6e184318#32), -- ext v24.16b, v24.16b, v24.16b, #8 - (0x126be0#64 , 0x6e024085#32), -- ext v5.16b, v4.16b, v2.16b, #8 - (0x126be4#64 , 0x6e044006#32), -- ext v6.16b, v0.16b, v4.16b, #8 - (0x126be8#64 , 0x4ef88442#32), -- add v2.2d, v2.2d, v24.2d - (0x126bec#64 , 0xce6680a2#32), -- sha512h q2, q5, v6.2d - (0x126bf0#64 , 0x4e200a94#32), -- rev64 v20.16b, v20.16b - (0x126bf4#64 , 0x4ee28401#32), -- add v1.2d, v0.2d, v2.2d - (0x126bf8#64 , 0xce638402#32), -- sha512h2 q2, q0, v3.2d - (0x126bfc#64 , 0x4cdf7c78#32), -- ld1 {v24.2d}, [x3], #16 - (0x126c00#64 , 0x4ef58739#32), -- add v25.2d, v25.2d, v21.2d - (0x126c04#64 , 0x4cdf7035#32), -- ld1 {v21.16b}, [x1], #16 - (0x126c08#64 , 0x6e194339#32), -- ext v25.16b, v25.16b, v25.16b, #8 - (0x126c0c#64 , 0x6e044025#32), -- ext v5.16b, v1.16b, v4.16b, #8 - (0x126c10#64 , 0x6e014066#32), -- ext v6.16b, v3.16b, v1.16b, #8 - (0x126c14#64 , 0x4ef98484#32), -- add v4.2d, v4.2d, v25.2d - (0x126c18#64 , 0xce6680a4#32), -- sha512h q4, q5, v6.2d - (0x126c1c#64 , 0x4e200ab5#32), -- rev64 v21.16b, v21.16b - (0x126c20#64 , 0x4ee48460#32), -- add v0.2d, v3.2d, v4.2d - (0x126c24#64 , 0xce628464#32), -- sha512h2 q4, q3, v2.2d - (0x126c28#64 , 0x4cdf7c79#32), -- ld1 {v25.2d}, [x3], #16 - (0x126c2c#64 , 0x4ef68718#32), -- add v24.2d, v24.2d, v22.2d - (0x126c30#64 , 0x4cdf7036#32), -- ld1 {v22.16b}, [x1], #16 - (0x126c34#64 , 0x6e184318#32), -- ext v24.16b, v24.16b, v24.16b, #8 - (0x126c38#64 , 0x6e014005#32), -- ext v5.16b, v0.16b, v1.16b, #8 - (0x126c3c#64 , 0x6e004046#32), -- ext v6.16b, v2.16b, v0.16b, #8 - (0x126c40#64 , 0x4ef88421#32), -- add v1.2d, v1.2d, v24.2d - (0x126c44#64 , 0xce6680a1#32), -- sha512h q1, q5, v6.2d - (0x126c48#64 , 0x4e200ad6#32), -- rev64 v22.16b, v22.16b - (0x126c4c#64 , 0x4ee18443#32), -- add v3.2d, v2.2d, v1.2d - (0x126c50#64 , 0xce648441#32), -- sha512h2 q1, q2, v4.2d - (0x126c54#64 , 0xd10a0063#32), -- sub x3, x3, #0x280 - (0x126c58#64 , 0x4ef78739#32), -- add v25.2d, v25.2d, v23.2d - (0x126c5c#64 , 0x4cdf7037#32), -- ld1 {v23.16b}, [x1], #16 - (0x126c60#64 , 0x6e194339#32), -- ext v25.16b, v25.16b, v25.16b, #8 - (0x126c64#64 , 0x6e004065#32), -- ext v5.16b, v3.16b, v0.16b, #8 - (0x126c68#64 , 0x6e034086#32), -- ext v6.16b, v4.16b, v3.16b, #8 - (0x126c6c#64 , 0x4ef98400#32), -- add v0.2d, v0.2d, v25.2d - (0x126c70#64 , 0xce6680a0#32), -- sha512h q0, q5, v6.2d - (0x126c74#64 , 0x4e200af7#32), -- rev64 v23.16b, v23.16b - (0x126c78#64 , 0x4ee08482#32), -- add v2.2d, v4.2d, v0.2d - (0x126c7c#64 , 0xce618480#32), -- sha512h2 q0, q4, v1.2d - (0x126c80#64 , 0x4efa8400#32), -- add v0.2d, v0.2d, v26.2d - (0x126c84#64 , 0x4efb8421#32), -- add v1.2d, v1.2d, v27.2d - (0x126c88#64 , 0x4efc8442#32), -- add v2.2d, v2.2d, v28.2d - (0x126c8c#64 , 0x4efd8463#32), -- add v3.2d, v3.2d, v29.2d - (0x126c90#64 , 0xb5ffc382#32), -- cbnz x2, 126500 - (0x126c94#64 , 0x4c002c00#32), -- st1 {v0.2d-v3.2d}, [x0] - (0x126c98#64 , 0xf84107fd#32), -- ldr x29, [sp], #16 - (0x126c9c#64 , 0xd65f03c0#32)] - -theorem fetch_inst_from_assoclist - {address: BitVec 64} {program : Map (BitVec 64) (BitVec 32)} - (h_program : s.program = program.find?) : - fetch_inst address s = program.find? address := by - unfold fetch_inst read_store - simp_all! - -theorem sha512_block_armv8_new_program (s : ArmState) - (h_s_ok : read_err s = StateError.None) - (h_sp_aligned : CheckSPAlignment s = true) - (h_pc : read_pc s = 0x1264c0#64) - (h_program : s.program = sha512_program.find?) - (h_s' : s' = run 506 s) : - read_err s' = StateError.None := by - /- - -- (FIXME) simp_all below fails with a nested error: - -- maximum recursion depth has been reached (use `set_option maxRecDepth ` to increase limit) - -- simp_all - -- (WORKAROUND) I manually do subst and simp at individual hypotheses. - subst s' - simp at h_s_ok h_pc - unfold run - simp [stepi, h_pc] - rw [fetch_inst_from_assoclist h_program] - -- (FIXME) Wish this output from simp/ground wasn't so noisy. - FIXME - simp (config := {ground := true}) only - simp [exec_inst, *] - -- (FIXME) At this point, we have an if in the goal whose condition - -- is comprised of ground terms. However, simp/ground below fails - -- with a max. recursion depth error again. - -- simp (config := {ground := true}) only - -- (WORKAROUND) I manually split and attempt to make progress. - split - · rename_i h - simp (config := {ground := true}) at h - · rename_i h; simp (config := {ground := true}) at h - unfold run - simp [stepi] - rw [fetch_inst_from_assoclist h_program] - conv => - pattern find? .. - simp (config := {ground := true}) only - simp [*] - conv => - pattern decode_raw_inst .. - simp (config := {ground := true}) only - simp only - simp [exec_inst, *] - - - -/ - sorry - -end SHA512_proof diff --git a/Proofs/Sha512_block_armv8.lean b/Proofs/Sha512_block_armv8.lean index 9bc848f2..7c22cfcc 100644 --- a/Proofs/Sha512_block_armv8.lean +++ b/Proofs/Sha512_block_armv8.lean @@ -12,30 +12,6 @@ section SHA512_proof open BitVec -/- -The `sym1` tactic, defined in ../Tactics/Sym.lean, attempts to -symbolically simulate a single instruction -- it is pretty -straightforward right now and we expect it to radically change in the -near future. - -It unfolds the `run` function once, then -unfolds the `stepi` function, reduces -`fetch_inst
` -to a term like: -`Std.RBMap.find?
` -where `` and `
` are expected to be concrete. -We hope that `simp` is able to "evaluate" such ground terms during -proof so that the above gives us instruction located at -`
` in ``. Moreover, we also hope that `simp` -evaluates `decode_raw_inst ` to produce a concrete -`` and return an `exec_inst ` -term. - -`sym1` then applies some lemmas in its simpset, and finally we -capture the behavior of the instruction in terms of writes made to -the machine state (denoted by function `w`). --/ - ---------------------------------------------------------------------- -- Test 1: We have a 4 instruction program, and we attempt to simulate @@ -50,6 +26,7 @@ def sha512_program_test_1 : program := ] -- set_option profiler true in +-- set_option pp.deepTerms true in theorem sha512_program_test_1_sym (s0 s_final : ArmState) (h_s0_pc : read_pc s0 = 0x126538#64) (h_s0_sp_aligned : CheckSPAlignment s0 = true) @@ -57,19 +34,15 @@ theorem sha512_program_test_1_sym (s0 s_final : ArmState) (h_s0_ok : read_err s0 = StateError.None) (h_run : s_final = run 4 s0) : read_err s_final = StateError.None := by - -- iterate 4 (sym1 [h_s0_program]) - -- sym1 [h_s0_program] - (try simp_all (config := {decide := true, ground := true}) only [state_simp_rules]); - unfold run; - simp_all only [stepi, state_simp_rules]; - (try rw [fetch_inst_from_program h_s0_program]); - -- (try simp (config := {ground := true}) only); - -- simp only [exec_inst, state_simp_rules]; - -- (try simp_all (config := {decide := true, ground := true}) only [state_simp_rules]) - sorry - -- unfold read_pc at h_s0_pc - -- sym_n 4 0x126538 sha512_program_test_1 - -- rw [h_run,h_s4_ok] + -- Prelude + simp_all only [state_simp_rules, -h_run] + -- Symbolic simulation + sym_n 4 h_s0_program + -- Final steps + unfold run at h_run + subst s_final s_4 + simp_all only [state_simp_rules, minimal_theory, bitvec_rules] + done ---------------------------------------------------------------------- @@ -93,10 +66,15 @@ theorem sha512_program_test_2_sym (s0 s_final : ArmState) (h_s0_ok : read_err s0 = StateError.None) (h_run : s_final = run 4 s0) : read_err s_final = StateError.None := by - -- TODO: use sym_n. Using it causes an error at simp due to the - -- large formula size. - -- iterate 4 (sym1 [h_s0_program]) - sorry + -- Prelude + simp_all only [state_simp_rules, -h_run] + -- Symbolic simulation + sym_n 4 h_s0_program + -- Final steps + unfold run at h_run + subst s_final s_4 + simp_all only [state_simp_rules, minimal_theory, bitvec_rules] + done ---------------------------------------------------------------------- @@ -118,45 +96,12 @@ theorem sha512_block_armv8_test_3_sym (s0 s_final : ArmState) (h_s0_program : s0.program = sha512_program_test_3.find?) (h_run : s_final = run 4 s0) : read_err s_final = StateError.None := by - -- unfold read_pc at h_s0_pc - -- sym_n 4 0x1264c0 sha512_program_test_3 - -- rw [h_run,h_s4_ok] + -- Prelude + simp_all only [state_simp_rules, -h_run] + -- Symbolic simulation + -- sym_n 1 h_s0_program sorry --- A record that shows simp fails. -theorem sha512_block_armv8_test_3_sym_fail (s : ArmState) - (h_s_ok : read_err s = StateError.None) - (h_sp_aligned : CheckSPAlignment s = true) - (h_pc : read_pc s = 0x1264c0#64) - (h_program : s.program = sha512_program_test_3.find?) - (h_s' : s' = run 4 s) : - read_err s' = StateError.None := by - FIXME - -- Symbolically simulate one instruction. - (sym1 [h_program]) - -- - -- (FIXME) At this point, I get an `if` term as the second argument - -- of `run`. The if's condition consists of ground terms, and I - -- hoped the `if` would be "evaluated away" to the true branch. - -- However, the simp/ground below fails with a nested error: - -- "maximum recursion depth has been reached". - -- - -- (Aside: I also wish simp/ground didn't leave such a verbose - -- output. Anything I can do to fix it?) - -- - -- simp (config := {ground := true}) only - -- - -- (WOKRAROUND) I manually do a split here. - split - · rename_i h; simp (config := {ground := true}) at h - · unfold run - simp [stepi, *] - rw [fetch_inst_from_program h_program] - -- (FIXME) Here I run into a similar situation, where we are - -- matching on Std.RBMap.find? with ground terms and simp/ground - -- fails. - sorry - ---------------------------------------------------------------------- -- Test 4: sha512_block_armv8_test_4_sym --- this is a symbolic @@ -171,10 +116,10 @@ theorem sha512_block_armv8_test_4_sym (s0 s_final : ArmState) (h_s0_program : s0.program = sha512_program_map.find?) (h_run : s_final = run 32 s0) : read_err s_final = StateError.None := by - - unfold read_pc at h_s0_pc - -- sym_n 32 0x1264c0 - -- ^^ This raises the max recursion depth limit error because the program is too large. :/ + -- Prelude + simp_all only [state_simp_rules, -h_run] + -- Symbolic simulation + -- sym_n 1 h_s0_program sorry end SHA512_proof diff --git a/Tactics/Sym.lean b/Tactics/Sym.lean index 259c47d5..77a7c793 100644 --- a/Tactics/Sym.lean +++ b/Tactics/Sym.lean @@ -6,7 +6,7 @@ Author(s): Shilpi Goel import Arm.Exec import Arm.MemoryProofs -import Lean.Elab +import Lean.Elab import Lean.Expr open BitVec @@ -29,17 +29,6 @@ macro_rules -- (try simp only [ne_eq, r_of_w_different, r_of_w_same, w_of_w_shadow, w_irrelevant]) (try simp_all (config := {decide := true, ground := true}) only [state_simp_rules])) -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] - --- TODO: replace this with an upcoming new lemma in Std -theorem BitVec.foldCtor : { toFin := { val := a, isLt := h } : BitVec n } = BitVec.ofNat n a := by - simp [BitVec.ofNat, Fin.ofNat', h, Nat.mod_eq_of_lt] - -- init_next_step breaks 'h_s: s_next = run n s' into 'run (n-1) s' and one step. macro "init_next_step" h_s:ident : tactic => `(tactic| @@ -48,37 +37,54 @@ macro "init_next_step" h_s:ident : tactic => rename_i h_temp cases h_temp rename_i h_s' - simp at h_s')) + simp (config := {ground := true}) only at h_s')) -- Given 'h_step: s_next = stepi s', fetch_and_decode_inst unfolds stepi, -- simplifies fetch_inst and decode_raw_inst. -macro "fetch_and_decode_inst" h_step:ident h_s_ok:ident h_pc:ident h_program:ident : tactic => +macro "fetch_and_decode_inst" h_step:ident h_program:ident : tactic => `(tactic| - (unfold stepi at $h_step:ident - rw [$h_s_ok:ident] at $h_step:ident - dsimp at $h_step:ident -- reduce let and match - rw [$h_pc:ident] at $h_step:ident - rw [fetch_inst_from_program $h_program:ident] at $h_step:ident - -- Note: this often times out. It tries to evaluate, e.g., - -- Std.RBMap.find? sha512_program_test_2 1205560#64 - -- which easily becomes hard. - simp (config := {ground := true}) at $h_step:ident - repeat (rw [BitVec.foldCtor] at $h_step:ident) - )) + (-- unfold stepi at $h_step:ident + -- rw [$h_s_ok:ident] at $h_step:ident + -- dsimp at $h_step:ident -- reduce let and match + -- rw [$h_pc:ident] at $h_step:ident + -- rw [fetch_inst_from_program $h_program:ident] at $h_step:ident + -- -- Note: this often times out. It tries to evaluate, e.g., + -- -- Std.RBMap.find? sha512_program_test_2 1205560#64 + -- -- which easily becomes hard. + -- simp (config := {ground := true}) at $h_step:ident + -- repeat (rw [BitVec.ofFin_eq_ofNat] at $h_step:ident) + simp only [*, stepi, state_simp_rules, minimal_theory, bitvec_rules] at $h_step:ident + rw [fetch_inst_from_program $h_program:ident] at $h_step:ident + conv at $h_step:ident => + pattern Map.find? _ _ + simp (config := {ground := true}) only + -- simp/ground leaves bitvecs' structure exposed, so we use + -- BitVec.ofFin_eq_ofNat to fold them back into their canonical + -- form. + simp only [BitVec.ofFin_eq_ofNat] + (try dsimp only at $h_step:ident); + conv at $h_step:ident => + pattern decode_raw_inst _ + simp (config := {ground := true}) only + simp only [BitVec.ofFin_eq_ofNat] + (try dsimp only at $h_step:ident))) -- Given hstep which is the result of fetch_and_decode_inst, exec_inst executes -- an instruction and generates 's_next = w .. (w .. (... s))'. -macro "exec_inst" h_step:ident h_sp_aligned:ident st_next:ident: tactic => +macro "exec_inst" h_step:ident : tactic => `(tactic| - (unfold exec_inst at $h_step:ident - -- A simple case where simp works (e.g., Arm.DPI) - try (simp (config := {ground := true, decide := true}) at $h_step:ident) - -- A complicated case (e.g., Arm.LDST) - try (simp at $h_step:ident; (conv at $h_step:ident => - arg 2 - apply if_true - apply $st_next:ident); simp [$h_sp_aligned:ident] at $h_step:ident) - )) + (-- unfold exec_inst at $h_step:ident + -- -- A simple case where simp works (e.g., Arm.DPI) + -- try (simp (config := {ground := true, decide := true}) at $h_step:ident) + -- -- A complicated case (e.g., Arm.LDST) + -- try (simp at $h_step:ident; (conv at $h_step:ident => + -- arg 2 + -- apply if_true + -- apply $st_next:ident); simp [$h_sp_aligned:ident] at $h_step:ident) + simp only [exec_inst, state_simp_rules, minimal_theory, bitvec_rules] at $h_step:ident; + (try simp (config := {ground := true}) only [↓reduceIte, state_simp_rules, minimal_theory, bitvec_rules] at $h_step:ident) + -- Fold back any exposed bitvecs into canonical forms. + (try simp only [BitVec.ofFin_eq_ofNat]))) -- Given h_step wich is 's_next = w .. (w .. (... s))', it creates assumptions -- 'read .. s_next = value'. @@ -91,12 +97,12 @@ macro "update_invariants" st_next:ident progname:ident h_program_new:ident h_step:ident pc_next:term : tactic => `(tactic| - (have $h_s_ok_new:ident: read_err $st_next:ident = StateError.None := by + (have $h_s_ok_new:ident : r StateField.ERR $st_next:ident = StateError.None := by rw [$h_step:ident]; simp_all -- Q: How can we automatically infer the next PC? - have $h_pc_new:ident: r StateField.PC $st_next:ident = $pc_next:term := by + have $h_pc_new:ident : r StateField.PC $st_next:ident = $pc_next:term := by rw [$h_step:ident,$h_pc:ident]; simp; simp (config := {ground := true}) - have $h_sp_aligned_new:ident: CheckSPAlignment $st_next:ident = true := by + have $h_sp_aligned_new:ident : CheckSPAlignment $st_next:ident = true := by unfold CheckSPAlignment at * rw [$h_step:ident] simp @@ -116,62 +122,65 @@ macro "update_invariants" st_next:ident progname:ident -/ sorry have $h_program_new:ident : ($st_next:ident).program = - Std.RBMap.find? ($progname:ident) := by + Map.find? ($progname:ident) := by rw [$h_step:ident] try (repeat rw [w_program]) try (rw [write_mem_bytes_program]) assumption)) -def sym_one (curr_state_number : Nat) (pc_begin : Nat) (prog : Lean.Ident) : +def sym_one (curr_state_number : Nat) (prog : Lean.Ident) : Lean.Elab.Tactic.TacticM Unit := Lean.Elab.Tactic.withMainContext do let n_str := toString curr_state_number - let n'_str := toString (curr_state_number+1) - let pcexpr := Lean.mkNatLit (pc_begin + 4 * (curr_state_number + 1)) - let pcbv := ← (Lean.Elab.Term.exprToSyntax (Lean.mkApp2 (Lean.mkConst ``BitVec.ofNat) - (Lean.mkNatLit 64) - pcexpr)) + let n'_str := toString (curr_state_number + 1) + -- let pcexpr := Lean.mkNatLit (pc_begin + 4 * (curr_state_number + 1)) + -- let pcbv := ← (Lean.Elab.Term.exprToSyntax (Lean.mkApp2 (Lean.mkConst ``BitVec.ofNat) + -- (Lean.mkNatLit 64) + -- pcexpr)) -- let pcbv := ← (Lean.mkApp2 (Lean.mkConst ``BitVec.ofNat) (Lean.mkNatLit 64) -- pcexpr).toSyntax -- Question: how can I convert this pcbv into Syntax? - let mk_name (s:String): Lean.Name := + let mk_name (s : String) : Lean.Name := Lean.Name.append Lean.Name.anonymous s - -- The name of the next state + -- st': name of the next state let st' := Lean.mkIdent (mk_name ("s_" ++ n'_str)) - let h_st_ok := Lean.mkIdent (mk_name ("h_s" ++ n_str ++ "_ok")) - let h_st'_ok := Lean.mkIdent (mk_name ("h_s" ++ n'_str ++ "_ok")) - let h_st_pc := Lean.mkIdent (mk_name ("h_s" ++ n_str ++ "_pc")) - let h_st'_pc := Lean.mkIdent (mk_name ("h_s" ++ n'_str ++ "_pc")) - let h_st_program := Lean.mkIdent (mk_name ("h_s" ++ n_str ++ "_program")) - let h_st'_program := Lean.mkIdent (mk_name ("h_s" ++ n'_str ++ "_program")) - let h_st_sp_aligned := Lean.mkIdent (mk_name ("h_s" ++ n_str ++ "_sp_aligned")) - let h_st'_sp_aligned := Lean.mkIdent (mk_name ("h_s" ++ n'_str ++ "_sp_aligned")) + -- let h_st_ok := Lean.mkIdent (mk_name ("h_s" ++ n_str ++ "_ok")) + -- let h_st'_ok := Lean.mkIdent (mk_name ("h_s" ++ n'_str ++ "_ok")) + -- let h_st_pc := Lean.mkIdent (mk_name ("h_s" ++ n_str ++ "_pc")) + -- let h_st'_pc := Lean.mkIdent (mk_name ("h_s" ++ n'_str ++ "_pc")) + -- let h_st_program := Lean.mkIdent (mk_name ("h_s" ++ n_str ++ "_program")) + -- let h_st'_program := Lean.mkIdent (mk_name ("h_s" ++ n'_str ++ "_program")) + -- let h_st_sp_aligned := Lean.mkIdent (mk_name ("h_s" ++ n_str ++ "_sp_aligned")) + -- let h_st'_sp_aligned := Lean.mkIdent (mk_name ("h_s" ++ n'_str ++ "_sp_aligned")) -- Temporary hypotheses let h_run := Lean.mkIdent (mk_name "h_run") + let h_step_n := Lean.mkIdent (mk_name ("h_step_" ++ n_str)) + let h_step_n' := Lean.mkIdent (mk_name ("h_step_" ++ n'_str)) Lean.Elab.Tactic.evalTactic (← `(tactic| (init_next_step $h_run:ident - rename_i $st':ident h_step $h_run:ident + rename_i $st':ident $h_step_n':ident $h_run:ident -- Simulate one instruction - fetch_and_decode_inst h_step $h_st_ok:ident $h_st_pc:ident $h_st_program:ident - exec_inst h_step $h_st_sp_aligned:ident $st':ident - + fetch_and_decode_inst $h_step_n':ident $prog:ident + exec_inst $h_step_n':ident + (try clear $h_step_n:ident) -- Update invariants - update_invariants $st':ident $prog:ident - $h_st'_ok:ident - $h_st_pc:ident $h_st'_pc:ident - $h_st_sp_aligned $h_st'_sp_aligned:ident - $h_st'_program h_step $pcbv:term - clear $h_st_ok:ident $h_st_sp_aligned:ident $h_st_pc:ident h_step - $h_st_program:ident))) + -- update_invariants $st':ident $prog:ident + -- $h_st'_ok:ident + -- $h_st_pc:ident $h_st'_pc:ident + -- $h_st_sp_aligned $h_st'_sp_aligned:ident + -- $h_st'_program $h_step_n':ident $pcbv:term + -- clear $h_st_ok:ident $h_st_sp_aligned:ident $h_st_pc:ident $h_step_n':ident + -- $h_st_program:ident + ))) -- sym_n tactic symbolically simulates n instructions. -elab "sym_n" n:num pc:num prog:ident : tactic => do +elab "sym_n" n:num prog:ident : tactic => do for i in List.range n.getNat do - sym_one i pc.getNat prog + sym_one i prog -- sym_n tactic symbolically simulates n instructions from -- state number i. -elab "sym_i_n" i:num n:num pc:num prog:ident : tactic => do +elab "sym_i_n" i:num n:num prog:ident : tactic => do for j in List.range n.getNat do - sym_one (i.getNat + j) pc.getNat prog + sym_one (i.getNat + j) prog diff --git a/lean-toolchain b/lean-toolchain index f16b484e..6f6f7593 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2024-03-01 +leanprover/lean4:nightly-2024-03-02