diff --git a/Arm/Cosim.lean b/Arm/Cosim.lean index 13ddb6a6..b910b9e9 100644 --- a/Arm/Cosim.lean +++ b/Arm/Cosim.lean @@ -205,13 +205,15 @@ def nzcv_mismatch (x1 x2 : BitVec 4) : IO String := do acc := acc ++ s!"Flag{flag} machine {f1} model {f2}" pure acc -def regStates_match (input o1 o2 : regState) : IO Bool := do +def regStates_match (uniqueBaseName : String) (input o1 o2 : regState) : + IO Bool := do if o1 == o2 then pure true else let gpr_mismatch ← gpr_mismatch o1.gpr o2.gpr let nzcv_mismatch ← nzcv_mismatch o1.nzcv o2.nzcv let sfp_mismatch ← sfp_mismatch o1.sfp o2.sfp + IO.println s!"ID: {uniqueBaseName}" IO.println s!"Instruction: {decode_raw_inst input.inst}" IO.println s!"input: {toString input}" IO.println s!"Mismatch found: {gpr_mismatch} {nzcv_mismatch} {sfp_mismatch}" @@ -224,7 +226,7 @@ def one_test (inst : BitVec 32) (uniqueBaseName : String) : IO Bool := do let machine_st := machine_to_regState inst machine let model := run 1 (regState_to_armState input) let model_st := model_to_regState inst model - regStates_match input machine_st model_st + regStates_match uniqueBaseName input machine_st model_st /-- Make a task for running a single test. diff --git a/Arm/Memory/Separate.lean b/Arm/Memory/Separate.lean index 1012aaf9..09c3fb20 100644 --- a/Arm/Memory/Separate.lean +++ b/Arm/Memory/Separate.lean @@ -582,7 +582,7 @@ theorem read_mem_bytes_write_mem_bytes_eq_extract_LsB_of_mem_subset rw [BitVec.le_def] at hstart omega · simp only [h₁, bitvec_rules, minimal_theory] - intros h + intros apply BitVec.getLsb_ge omega diff --git a/Arm/MinTheory.lean b/Arm/MinTheory.lean index 7bddcda6..3b7fcc9c 100644 --- a/Arm/MinTheory.lean +++ b/Arm/MinTheory.lean @@ -94,6 +94,8 @@ attribute [minimal_theory] bne_iff_ne attribute [minimal_theory] Bool.false_eq attribute [minimal_theory] Bool.and_eq_false_imp +attribute [minimal_theory] Decidable.not_not + attribute [minimal_theory] Nat.le_zero_eq attribute [minimal_theory] Nat.zero_add attribute [minimal_theory] Nat.zero_eq diff --git a/Correctness/ArmSpec.lean b/Correctness/ArmSpec.lean index 9c730055..76e54fa9 100644 --- a/Correctness/ArmSpec.lean +++ b/Correctness/ArmSpec.lean @@ -1,3 +1,12 @@ +/- +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 + +Specializing the Correctness module for use with our specification of the Arm +ISA. +-/ + import Arm.Exec import Correctness.Correctness @@ -18,4 +27,20 @@ theorem arm_run (n : Nat) (s : ArmState) : simp only [Sys.run, Sys.next, run] rw [h] +-- (TODO) Move to Arm/BitVec.lean? +/-- Unexpander to represent bitvector literals in hexadecimal -- this overrides + the unexpander in the Lean BitVec library. -/ +@[app_unexpander BitVec.ofNat] def unexpandBitVecOfNatToHex : Lean.PrettyPrinter.Unexpander + | `($(_) $n:num $i:num) => + let i' := i.getNat + let n' := n.getNat + let trimmed_hex := -- Remove leading zeroes... + String.dropWhile (BitVec.ofNat n' i').toHex + (fun c => c = '0') + -- ... but keep one if the literal is all zeros. + let trimmed_hex := if trimmed_hex.isEmpty then "0" else trimmed_hex + let bv := Lean.Syntax.mkNumLit s!"0x{trimmed_hex}#{n'}" + `($bv:num) + | _ => throw () + end Correctness diff --git a/Correctness/Correctness.lean b/Correctness/Correctness.lean index 98220d96..7b6ef2c4 100644 --- a/Correctness/Correctness.lean +++ b/Correctness/Correctness.lean @@ -142,7 +142,8 @@ theorem partial_correctness_from_verification_conditions [Sys σ] [Spec' σ] (v1 : ∀ s0 : σ, pre s0 → assert s0 s0) (v2 : ∀ sf : σ, exit sf → cut sf) (v3 : ∀ s0 sf : σ, assert s0 sf → exit sf → post s0 sf) - (v4 : ∀ s0 si : σ, assert s0 si → ¬ exit si → assert s0 (nextc (next si))) + -- We prefer to use `run` instead of `step`. + (v4 : ∀ s0 si : σ, assert s0 si → ¬ exit si → assert s0 (nextc (run si 1))) : PartialCorrectness σ := fun s0 n hp hexit => let rec find (i : Nat) (h : assert s0 (run s0 i)) (hle : i ≤ n) : diff --git a/Proofs/Experiments/AbsVCG.lean b/Proofs/Experiments/AbsVCG.lean index 64db3d40..7313cd36 100644 --- a/Proofs/Experiments/AbsVCG.lean +++ b/Proofs/Experiments/AbsVCG.lean @@ -12,7 +12,6 @@ import Arm import Tactics.StepThms import Tactics.Sym import Correctness.ArmSpec -import Lean namespace AbsVCG @@ -29,7 +28,10 @@ def program : Program := def abs_pre (s : ArmState) : Prop := read_pc s = 0x4005d0#64 ∧ s.program = program ∧ - read_err s = StateError.None + read_err s = StateError.None ∧ + -- (FIXME) We don't really need the stack pointer to be aligned, but the + -- `sym_n` tactic expects this. Can we make this optional? + CheckSPAlignment s /-- Specification of the absolute value computation for a 32-bit bitvector. -/ def spec (x : BitVec 32) : BitVec 32 := @@ -46,7 +48,9 @@ def spec (x : BitVec 32) : BitVec 32 := /-- Postcondition for the correctness of the `Abs` program. -/ def abs_post (s0 sf : ArmState) : Prop := read_gpr 32 0#5 sf = spec (read_gpr 32 0#5 s0) ∧ - read_err sf = StateError.None + read_pc sf = 0x4005e0#64 ∧ + read_err sf = StateError.None ∧ + CheckSPAlignment sf /-- Function identifying the exit state(s) of the program. -/ def abs_exit (s : ArmState) : Prop := @@ -79,207 +83,155 @@ instance : Spec' ArmState where theorem Abs.csteps_eq (s : ArmState) (i : Nat) : Correctness.csteps s i = if abs_cut s then i - else Correctness.csteps (stepi s) (i + 1) := by + else Correctness.csteps (run 1 s) (i + 1) := by rw [Correctness.csteps_eq] - simp only [Sys.next, Spec'.cut] + simp only [Sys.next, Spec'.cut, run] done ------------------------------------------------------------------------------- -- Generating the program effects and non-effects -- set_option trace.gen_step.print_names true in -#genStepTheorems program thmType:="fetch" --- set_option trace.gen_step.print_names true in -#genStepTheorems program thmType:="decodeExec" --- set_option trace.gen_step.print_names true in -#genStepTheorems program thmType:="step" `state_simp_rules +#genStepEqTheorems program -- (FIXME) Obtain *_cut theorems for each instruction automatically. -theorem abs_stepi_0x4005d0_cut (s : ArmState) +theorem program.stepi_0x4005d0_cut (s sn : ArmState) (h_program : s.program = program) (h_pc : r StateField.PC s = 0x4005d0#64) - (h_err : r StateField.ERR s = StateError.None) : - abs_cut (stepi s) = false := by - have := program.stepi_0x4005d0 s (stepi s) h_program h_pc h_err + (h_err : r StateField.ERR s = StateError.None) + (h_sp_aligned : CheckSPAlignment s) + (h_step : sn = run 1 s) : + abs_cut sn = false ∧ + r StateField.PC sn = 0x4005d4#64 ∧ + r StateField.ERR sn = .None ∧ + sn.program = program ∧ + CheckSPAlignment sn := by + have := program.stepi_eq_0x4005d0 h_program h_pc h_err simp only [minimal_theory] at this - simp only [abs_cut, this, state_simp_rules, bitvec_rules, minimal_theory] + simp_all only [run, abs_cut, this, + state_simp_rules, bitvec_rules, minimal_theory] done -theorem abs_stepi_0x4005d4_cut (s : ArmState) +theorem program.stepi_0x4005d4_cut (s sn : ArmState) (h_program : s.program = program) (h_pc : r StateField.PC s = 0x4005d4#64) - (h_err : r StateField.ERR s = StateError.None) : - abs_cut (stepi s) = false := by - have := program.stepi_0x4005d4 s (stepi s) h_program h_pc h_err + (h_err : r StateField.ERR s = StateError.None) + (h_sp_aligned : CheckSPAlignment s) + (h_step : sn = run 1 s) : + abs_cut sn = false ∧ + r StateField.PC sn = 0x4005d8#64 ∧ + r StateField.ERR sn = .None ∧ + sn.program = program ∧ + CheckSPAlignment sn := by + have := program.stepi_eq_0x4005d4 h_program h_pc h_err simp only [minimal_theory] at this - simp only [abs_cut, this, state_simp_rules, bitvec_rules, minimal_theory] + simp_all only [run, abs_cut, this, + state_simp_rules, bitvec_rules, minimal_theory] done -theorem abs_stepi_0x4005d8_cut (s : ArmState) +theorem program.stepi_0x4005d8_cut (s sn : ArmState) (h_program : s.program = program) (h_pc : r StateField.PC s = 0x4005d8#64) - (h_err : r StateField.ERR s = StateError.None) : - abs_cut (stepi s) = false := by - have := program.stepi_0x4005d8 s (stepi s) h_program h_pc h_err + (h_err : r StateField.ERR s = StateError.None) + (h_sp_aligned : CheckSPAlignment s) + (h_step : sn = run 1 s) : + abs_cut sn = false ∧ + r StateField.PC sn = 0x4005dc#64 ∧ + r StateField.ERR sn = .None ∧ + sn.program = program ∧ + CheckSPAlignment sn := by + have := program.stepi_eq_0x4005d8 h_program h_pc h_err simp only [minimal_theory] at this - simp only [abs_cut, this, state_simp_rules, bitvec_rules, minimal_theory] + simp_all only [run, abs_cut, this, + state_simp_rules, bitvec_rules, minimal_theory] done -theorem abs_stepi_0x4005dc_cut (s : ArmState) +theorem program.stepi_0x4005dc_cut (s sn : ArmState) (h_program : s.program = program) (h_pc : r StateField.PC s = 0x4005dc#64) - (h_err : r StateField.ERR s = StateError.None) : - abs_cut (stepi s) = true := by - have := program.stepi_0x4005dc s (stepi s) h_program h_pc h_err + (h_err : r StateField.ERR s = StateError.None) + (h_sp_aligned : CheckSPAlignment s) + (h_step : sn = run 1 s) : + abs_cut sn = true ∧ + r StateField.PC sn = 0x4005e0#64 ∧ + r StateField.ERR sn = .None ∧ + sn.program = program ∧ + CheckSPAlignment sn := by + have := program.stepi_eq_0x4005dc h_program h_pc h_err simp only [minimal_theory] at this - simp only [abs_cut, this, state_simp_rules, bitvec_rules, minimal_theory] + simp_all only [run, abs_cut, this, + state_simp_rules, bitvec_rules, minimal_theory] done -/-- -(FIXME) This was tedious: we need to prove helper lemmas/build automation to -generate these effects theorems, but the good news is that we see a -pattern here to exploit. Our main workhorse here is symbolic -simulation, but the interesting part is that we are symbolically simulating -as well as determining the number of steps to simulate in tandem. --/ -theorem program_effects_lemma (h_pre : abs_pre s0) - (h_run : sf = run (Correctness.csteps (stepi s0) 0) (stepi s0)) : - r (StateField.GPR 0#5) sf = BitVec.truncate 64 - (BitVec.zeroExtend 32 - (BitVec.zeroExtend 64 - (AddWithCarry (BitVec.zeroExtend 32 (BitVec.zeroExtend 64 (BitVec.zeroExtend 32 (r (StateField.GPR 0#5) s0)))) - (BitVec.zeroExtend 32 - (BitVec.truncate 64 - (BitVec.replicate 32 - (BitVec.extractLsb 31 31 (BitVec.zeroExtend 32 (r (StateField.GPR 0#5) s0)))) &&& - BitVec.truncate 64 (~~~1#32) ||| - (BitVec.truncate 64 (BitVec.zero 32) &&& BitVec.truncate 64 (~~~4294967295#32) ||| - BitVec.truncate 64 ((BitVec.zeroExtend 32 (r (StateField.GPR 0#5) s0)).rotateRight 31) &&& - BitVec.truncate 64 4294967295#32) &&& - BitVec.truncate 64 1#32)) - 0#1).fst)) ^^^ - BitVec.truncate 64 - (BitVec.zeroExtend 32 - (BitVec.truncate 64 - (BitVec.replicate 32 (BitVec.extractLsb 31 31 (BitVec.zeroExtend 32 (r (StateField.GPR 0#5) s0)))) &&& - BitVec.truncate 64 (~~~1#32) ||| - (BitVec.truncate 64 (BitVec.zero 32) &&& BitVec.truncate 64 (~~~4294967295#32) ||| - BitVec.truncate 64 ((BitVec.zeroExtend 32 (r (StateField.GPR 0#5) s0)).rotateRight 31) &&& - BitVec.truncate 64 4294967295#32) &&& - BitVec.truncate 64 1#32)) ∧ - r StateField.PC sf = 0x4005e0#64 ∧ - r StateField.ERR sf = StateError.None := by - - simp only [abs_pre, state_simp_rules] at h_pre - have ⟨h_s0_pc, h_s0_program, h_s0_err⟩ := h_pre; clear h_pre - - -- Instruction 1 - rw [Abs.csteps_eq, abs_stepi_0x4005d0_cut s0 h_s0_program h_s0_pc h_s0_err] at h_run - simp only [minimal_theory, Nat.reduceAdd] at h_run - generalize h_step_1 : stepi s0 = s1 at h_run - have h_s1 : s1 = run 1 s0 := by - simp only [run, h_step_1] - replace h_step_1 : s1 = stepi s0 := h_step_1.symm - rw [program.stepi_0x4005d0 s0 s1 h_s0_program h_s0_pc h_s0_err] at h_step_1 - have h_s1_program : s1.program = program := by - simp only [h_step_1, h_s0_program, - state_simp_rules, minimal_theory, bitvec_rules] - have h_s1_err : r StateField.ERR s1 = StateError.None := by - simp only [h_step_1, h_s0_err, - state_simp_rules, minimal_theory, bitvec_rules] - have h_s1_pc : r StateField.PC s1 = 0x4005d4#64 := by - simp only [h_step_1, h_s0_pc, - state_simp_rules, minimal_theory, bitvec_rules] - - -- Instruction 2 - rw [Abs.csteps_eq, abs_stepi_0x4005d4_cut s1 h_s1_program h_s1_pc h_s1_err] at h_run - simp only [minimal_theory, Nat.reduceAdd] at h_run - generalize h_step_2 : stepi s1 = s2 at h_run - have h_s2 : s2 = run 1 s1 := by - simp only [run, h_step_2] - replace h_step_2 : s2 = stepi s1 := h_step_2.symm - rw [program.stepi_0x4005d4 s1 s2 h_s1_program h_s1_pc h_s1_err] at h_step_2 - have h_s2_program : s2.program = program := by - simp only [h_step_2, h_s1_program, - state_simp_rules, minimal_theory, bitvec_rules] - have h_s2_err : r StateField.ERR s2 = StateError.None := by - simp only [h_step_2, h_s1_err, - state_simp_rules, minimal_theory, bitvec_rules] - have h_s2_pc : r StateField.PC s2 = 0x4005d8#64 := by - simp only [h_step_2, h_s1_pc, - state_simp_rules, minimal_theory, bitvec_rules] +theorem nextc_to_run_from_0x4005d0 (h : abs_pre s0) : + (Correctness.nextc (Sys.run s0 1)) = run 4 s0 := by + simp only [abs_pre, state_simp_rules] at h + obtain ⟨h_s0_pc, h_s0_program, h_s0_err, h_s0_sp_aligned⟩ := h + simp only + [Correctness.nextc, Correctness.arm_run, + Spec'.cut, minimal_theory] - -- Instruction 3 - rw [Abs.csteps_eq, abs_stepi_0x4005d8_cut s2 h_s2_program h_s2_pc h_s2_err] at h_run - simp only [minimal_theory, Nat.reduceAdd] at h_run - generalize h_step_3 : stepi s2 = s3 at h_run - have h_s3 : s3 = run 1 s2 := by - simp only [run, h_step_3] - replace h_step_3 : s3 = stepi s2 := h_step_3.symm - rw [program.stepi_0x4005d8 s2 s3 h_s2_program h_s2_pc h_s2_err] at h_step_3 - have h_s3_program : s3.program = program := by - simp only [h_step_3, h_s2_program, - state_simp_rules, minimal_theory, bitvec_rules] - have h_s3_err : r StateField.ERR s3 = StateError.None := by - simp only [h_step_3, h_s2_err, - state_simp_rules, minimal_theory, bitvec_rules] - have h_s3_pc : r StateField.PC s3 = 0x4005dc#64 := by - simp only [h_step_3, h_s2_pc, - state_simp_rules, minimal_theory, bitvec_rules] + rw [Abs.csteps_eq] + have h_step_1 := program.stepi_0x4005d0_cut s0 (run 1 s0) + simp_all only [minimal_theory, bitvec_rules] + generalize h_s1 : run 1 s0 = s1 at h_step_1 - -- Instruction 4 - rw [Abs.csteps_eq, abs_stepi_0x4005dc_cut s3 h_s3_program h_s3_pc h_s3_err] at h_run - simp only [minimal_theory, Nat.reduceAdd] at h_run - generalize h_step_4 : stepi s3 = s4 at h_run - have h_s4 : s4 = run 1 s3 := by - simp only [run, h_step_4] - replace h_step_4 : s4 = stepi s3 := h_step_4.symm - rw [program.stepi_0x4005dc s3 s4 h_s3_program h_s3_pc h_s3_err] at h_step_4 - have _h_s4_program : s4.program = program := by - simp only [h_step_4, h_s3_program, - state_simp_rules, minimal_theory, bitvec_rules] - have h_s4_err : r StateField.ERR s4 = StateError.None := by - simp only [h_step_4, h_s3_err, - state_simp_rules, minimal_theory, bitvec_rules] - have h_s4_pc : r StateField.PC s4 = 0x4005e0#64 := by - simp only [h_step_4, h_s3_pc, - state_simp_rules, minimal_theory, bitvec_rules] + rw [Abs.csteps_eq] + have h_step_2 := program.stepi_0x4005d4_cut s1 (run 1 s1) + simp_all only [minimal_theory, bitvec_rules] + generalize h_s2 : run 1 s1 = s2 at h_step_2 - have h_s4_gpr0 : r (StateField.GPR 0#5) s4 = - BitVec.truncate 64 - (BitVec.zeroExtend 32 - (BitVec.zeroExtend 64 - (AddWithCarry (BitVec.zeroExtend 32 (BitVec.zeroExtend 64 (BitVec.zeroExtend 32 (r (StateField.GPR 0#5) s0)))) - (BitVec.zeroExtend 32 - (BitVec.truncate 64 - (BitVec.replicate 32 - (BitVec.extractLsb 31 31 (BitVec.zeroExtend 32 (r (StateField.GPR 0#5) s0)))) &&& - BitVec.truncate 64 (~~~1#32) ||| - (BitVec.truncate 64 (BitVec.zero 32) &&& BitVec.truncate 64 (~~~4294967295#32) ||| - BitVec.truncate 64 ((BitVec.zeroExtend 32 (r (StateField.GPR 0#5) s0)).rotateRight 31) &&& - BitVec.truncate 64 4294967295#32) &&& - BitVec.truncate 64 1#32)) - 0#1).fst)) ^^^ - BitVec.truncate 64 - (BitVec.zeroExtend 32 - (BitVec.truncate 64 - (BitVec.replicate 32 (BitVec.extractLsb 31 31 (BitVec.zeroExtend 32 (r (StateField.GPR 0#5) s0)))) &&& - BitVec.truncate 64 (~~~1#32) ||| - (BitVec.truncate 64 (BitVec.zero 32) &&& BitVec.truncate 64 (~~~4294967295#32) ||| - BitVec.truncate 64 ((BitVec.zeroExtend 32 (r (StateField.GPR 0#5) s0)).rotateRight 31) &&& - BitVec.truncate 64 4294967295#32) &&& - BitVec.truncate 64 1#32)) := by - simp (config := {decide := true}) only [h_step_4, h_step_3, h_step_2, h_step_1, - state_simp_rules, bitvec_rules] + rw [Abs.csteps_eq] + have h_step_3 := program.stepi_0x4005d8_cut s2 (run 1 s2) + simp_all only [minimal_theory, bitvec_rules] + generalize h_s3 : run 1 s2 = s3 at h_step_3 - have h_sf_s4 : sf = s4 := by - simp only [h_run, h_s4, h_s3, h_s2, h_s1, run] + rw [Abs.csteps_eq] + have h_step_4 := program.stepi_0x4005dc_cut s3 (run 1 s3) + simp_all only [minimal_theory, bitvec_rules] + generalize h_s4 : run 1 s3 = s4 at h_step_4 - simp only [h_sf_s4, h_s4_gpr0, h_s4_pc, h_s4_err, minimal_theory] + have h_s4_s1 : s4 = run 3 s1 := by + simp only [←h_s4, ←h_s3, ←h_s2, ←run_plus] + simp only [←h_s4_s1, h_step_4, minimal_theory] + simp only [h_s4_s1, ←h_s1, ←run_plus] done -------------------------------------------------------------------------------- +theorem effects_of_nextc_from_0x4005d0 (h_pre : abs_pre s0) + (_h_pc : read_pc s0 = 0x4005d0#64) + (h_run : sn = Correctness.nextc (Sys.run s0 1)) : + r StateField.PC sn = 0x4005e0#64 ∧ + r (StateField.GPR 0#5) sn = + BitVec.zeroExtend 64 + (AddWithCarry (BitVec.zeroExtend 32 (r (StateField.GPR 0x0#5) s0)) + (BitVec.replicate 32 (BitVec.extractLsb 31 31 (BitVec.zeroExtend 32 (r (StateField.GPR 0x0#5) s0))) &&& + 0xfffffffe#32 ||| + (BitVec.zeroExtend 32 (r (StateField.GPR 0x0#5) s0)).rotateRight 31 &&& 0xffffffff#32 &&& 0x1#32) + 0x0#1).fst ^^^ + (BitVec.zeroExtend 64 + (BitVec.replicate 32 (BitVec.extractLsb 31 31 (BitVec.zeroExtend 32 (r (StateField.GPR 0x0#5) s0)))) &&& + 0xfffffffe#64 ||| + BitVec.zeroExtend 64 ((BitVec.zeroExtend 32 (r (StateField.GPR 0x0#5) s0)).rotateRight 31) &&& 0xffffffff#64 &&& + 0x1#64) ∧ + r StateField.ERR sn = .None ∧ + sn.program = program ∧ + CheckSPAlignment sn := by + rw [nextc_to_run_from_0x4005d0 h_pre] at h_run + obtain ⟨h_pc, h_program, h_err, h_sp_aligned⟩ := h_pre + simp only [state_simp_rules] at * + -- Symbolic simulation + -- (FIXME) Why do we need `try assumption` below? + sym_n 4 at s0 <;> try assumption + -- Aggregate the effects + simp only [run] at h_run + subst sn + simp only [abs_cut, + h_s4_err, h_s4_pc, h_s4_program, h_s4_sp_aligned, + state_simp_rules, minimal_theory] + simp only [h_step_4, h_step_3, h_step_2, h_step_1, + state_simp_rules, bitvec_rules, minimal_theory] + done theorem partial_correctness : PartialCorrectness ArmState := by @@ -306,15 +258,18 @@ theorem partial_correctness : have ⟨h_assert1, h_assert2, h_assert3⟩ := h_assert subst si clear h_exit h_assert - generalize h_run : (run (Correctness.csteps (stepi s0) 0) (stepi s0)) = sf - have effects := @program_effects_lemma s0 sf h_assert1 h_run.symm - simp only [Sys.next, Spec'.assert, abs_assert, h_assert1, - Correctness.nextc, Correctness.arm_run, - h_run, effects, Spec'.cut, abs_cut, - Spec'.assert, abs_assert, abs_post, - AddWithCarry, spec, + generalize h_run : (Correctness.nextc (Sys.run s0 1)) = sf + have h_effects := @effects_of_nextc_from_0x4005d0 s0 sf + simp only [*, minimal_theory] at h_effects + simp only [*, Spec'.assert, abs_assert, abs_post, state_simp_rules, bitvec_rules, minimal_theory] - split <;> bv_decide + simp only [spec, AddWithCarry, bitvec_rules] + generalize h_x0 : (r (StateField.GPR 0x0#5) s0) = x0 + simp only [state_value] at x0 + clear h_effects h_run h_assert1 h_assert2 sf h_x0 s0 + split + case isTrue => bv_decide + case isFalse => bv_decide done theorem termination : @@ -322,10 +277,17 @@ theorem termination : simp [Termination, Spec.pre, Spec.exit, abs_exit, state_simp_rules, bitvec_rules, minimal_theory] intro s h_pre - have h_effects := @program_effects_lemma s - simp only [h_pre, minimal_theory] at h_effects - apply Exists.intro ((Correctness.csteps (Sys.next s) 0) + 1) - simp only [Correctness.arm_run, Sys.next, run_succ, h_effects] + have h_clock := @nextc_to_run_from_0x4005d0 s h_pre + have h_effects := @effects_of_nextc_from_0x4005d0 + s (run 4 s) h_pre + simp only [abs_pre, state_simp_rules] at h_pre + simp only [h_pre, h_clock, state_simp_rules, minimal_theory] + at h_effects + obtain ⟨h_effects_pc, h_effects⟩ := h_effects + -- Clearing h_effects for readability. + clear h_effects + apply Exists.intro 4 + simp only [Correctness.arm_run, h_effects_pc] done end AbsVCG diff --git a/Proofs/Experiments/AddLoop.lean b/Proofs/Experiments/AddLoop.lean new file mode 100644 index 00000000..c343d847 --- /dev/null +++ b/Proofs/Experiments/AddLoop.lean @@ -0,0 +1,651 @@ +/- +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 + +Experimental: Use the Correctness module to prove that this program computes the +following via a naive loop that iterates over `x0`: +`x0 := x0 + x1` +-/ +import Arm +import Tactics.StepThms +import Tactics.Sym +import Correctness.ArmSpec + +namespace AddLoop + +/- +Here is a C snippet that describes this program's behavior. + +while (x0 != 0) { + x1 := x1 + 1 + x0 := x0 - 1 +} +x0 := x1 +-/ +def program : Program := + def_program + [ + /- 00000000004005a4 : -/ + (0x4005a4#64, 0x14000003#32), /- b 4005b0 -/ + + /- 00000000004005a8 : -/ + (0x4005a8#64, 0x91000421#32), /- add x1, x1, #0x1 -/ + (0x4005ac#64, 0xd1000400#32), /- sub x0, x0, #0x1 -/ + + /- 00000000004005b0 : -/ + (0x4005b0#64, 0xf100001f#32), /- cmp x0, #0x0 -/ + (0x4005b4#64, 0x54ffffa1#32), /- b.ne 4005a8 -/ + (0x4005b8#64, 0xaa0103e0#32), /- mov x0, x1 -/ + (0x4005bc#64, 0xd65f03c0#32) /- ret -/ + ] + +/-- Precondition for the correctness of the Add program. -/ +def pre (s : ArmState) : Prop := + read_pc s = 0x4005a4#64 ∧ + s.program = program ∧ + read_err s = StateError.None ∧ + -- (FIXME) We don't really need the stack pointer to be aligned, but the + -- `sym_n` tactic expects this. Can we make this optional? + CheckSPAlignment s + +/-- Specification function. -/ +def spec (x0 x1 : BitVec 64) : BitVec 64 := + x0 + x1 + +def post (s0 sf : ArmState) : Prop := + read_gpr 64 0#5 sf = spec (read_gpr 64 0#5 s0) (read_gpr 64 1#5 s0) ∧ + read_pc sf = 0x4005bc#64 ∧ + read_err sf = StateError.None ∧ + sf.program = program ∧ + -- (FIXME) We don't really need the stack pointer to be aligned, but the + -- `sym_n` tactic expects this. Can we make this optional? + CheckSPAlignment sf + +def exit (s : ArmState) : Prop := + -- (FIXME) Let's consider the state where we are poised to execute `ret` as an + -- exit state for now. + read_pc s = 0x4005bc#64 + +def cut (s : ArmState) : Bool := + -- First instruction + read_pc s = 0x4005a4#64 || + -- Loop guard (branch instruction) + read_pc s = 0x4005b4#64 || + -- First instruction following the loop + read_pc s = 0x4005b8#64 || + -- Last instruction + read_pc s = 0x4005bc#64 + +def loop_inv (s0 si : ArmState) : Prop := + let x0 := read_gpr 64 0#5 s0 + let x1 := read_gpr 64 1#5 s0 + let curr_x0 := read_gpr 64 0#5 si + let curr_x1 := read_gpr 64 1#5 si + let curr_zf := r (StateField.FLAG PFlag.Z) si + (curr_x0 <= x0) ∧ + ((curr_zf = 1#1) ↔ (curr_x0 = 0#64)) ∧ + (curr_x1 = x1 + (x0 - curr_x0)) ∧ + read_err si = .None ∧ + si.program = program ∧ + -- (FIXME) We don't really need the stack pointer to be aligned, but the + -- `sym_n` tactic expects this. Can we make this optional? + CheckSPAlignment si + +def loop_post (s0 si : ArmState) : Prop := + read_gpr 64 1#5 si = spec (read_gpr 64 0#5 s0) (read_gpr 64 1#5 s0) ∧ + read_err si = .None ∧ + si.program = program ∧ + -- (FIXME) We don't really need the stack pointer to be aligned, but the + -- `sym_n` tactic expects this. Can we make this optional? + CheckSPAlignment si + +def assert (s0 si : ArmState) : Prop := + pre s0 ∧ + -- Using `match` is preferable to `if` for the `split` tactic (and for + -- readability). + match (read_pc si) with + | 0x4005a4#64 => + -- First instruction + si = s0 + | 0x4005b4#64 => + -- Loop guard + loop_inv s0 si + | 0x4005b8#64 => + -- First instruction following the loop + loop_post s0 si + | 0x4005bc#64 => + -- Last instruction + post s0 si + | _ => False + +instance : Spec' ArmState where + pre := pre + post := post + exit := exit + cut := cut + assert := assert + +theorem AddLoop.csteps_eq (s : ArmState) (i : Nat) : + Correctness.csteps s i = if cut s then i + else Correctness.csteps (run 1 s) (i + 1) := by + rw [Correctness.csteps_eq] + simp only [Sys.next, Spec'.cut, run] + done + +------------------------------------------------------------------------------- +-- Generating the program effects and non-effects + +-- (FIXME) Print names of generated theorems. +-- set_option trace.gen_step.debug true in +#genStepEqTheorems program + +-- (FIXME) Obtain *_cut theorems for each instruction automatically. + +theorem program.stepi_0x4005a4_cut (s sn : ArmState) + (h_program : s.program = program) + (h_pc : r StateField.PC s = 0x4005a4#64) + (h_err : r StateField.ERR s = StateError.None) + (h_sp_aligned : CheckSPAlignment s) + (h_step : sn = run 1 s) : + cut sn = false ∧ + r StateField.PC sn = 0x4005b0#64 ∧ + r StateField.ERR sn = .None ∧ + sn.program = program ∧ + CheckSPAlignment sn := by + have := program.stepi_eq_0x4005a4 h_program h_pc h_err + simp only [minimal_theory] at this + simp_all only [run, cut, this, + state_simp_rules, bitvec_rules, minimal_theory] + done + +theorem program.stepi_0x4005a8_cut (s sn : ArmState) + (h_program : s.program = program) + (h_pc : r StateField.PC s = 0x4005a8#64) + (h_err : r StateField.ERR s = StateError.None) + (h_sp_aligned : CheckSPAlignment s) + (h_step : sn = run 1 s) : + cut sn = false ∧ + r StateField.PC sn = 0x4005ac#64 ∧ + r StateField.ERR sn = .None ∧ + sn.program = program ∧ + CheckSPAlignment sn := by + have := program.stepi_eq_0x4005a8 h_program h_pc h_err + simp only [minimal_theory, bitvec_rules] at this + simp_all only [run, cut, this, state_simp_rules, bitvec_rules, minimal_theory] + done + +theorem program.stepi_0x4005ac_cut (s sn : ArmState) + (h_program : s.program = program) + (h_pc : r StateField.PC s = 0x4005ac#64) + (h_err : r StateField.ERR s = StateError.None) + (h_sp_aligned : CheckSPAlignment s) + (h_step : sn = run 1 s) : + cut sn = false ∧ + r StateField.PC sn = 0x4005b0#64 ∧ + r StateField.ERR sn = .None ∧ + sn.program = program ∧ + CheckSPAlignment sn := by + have := program.stepi_eq_0x4005ac h_program h_pc h_err + simp only [minimal_theory] at this + simp_all only [run, cut, this, state_simp_rules, bitvec_rules, minimal_theory] + done + +theorem program.stepi_0x4005b0_cut (s sn : ArmState) + (h_program : s.program = program) + (h_pc : r StateField.PC s = 0x4005b0#64) + (h_err : r StateField.ERR s = StateError.None) + (h_sp_aligned : CheckSPAlignment s) + (h_step : sn = run 1 s) : + cut sn = true ∧ + r StateField.PC sn = 0x4005b4#64 ∧ + r StateField.ERR sn = .None ∧ + sn.program = program ∧ + CheckSPAlignment sn := by + have := program.stepi_eq_0x4005b0 h_program h_pc h_err + simp only [minimal_theory] at this + simp_all only [run, cut, this, state_simp_rules, bitvec_rules, minimal_theory] + done + +-- Branch instruction! +theorem program.stepi_0x4005b4_cut (s sn : ArmState) + (h_program : s.program = program) + (h_pc : r StateField.PC s = 0x4005b4#64) + (h_err : r StateField.ERR s = StateError.None) + (h_sp_aligned : CheckSPAlignment s) + (h_step : sn = run 1 s) : + cut sn = (r (StateField.FLAG PFlag.Z) s = 1#1) ∧ + r StateField.PC sn = (if (r (StateField.FLAG PFlag.Z) s = 1#1) then + 0x4005b8#64 + else + 0x4005a8#64) ∧ + r StateField.ERR sn = .None ∧ + sn.program = program ∧ + CheckSPAlignment sn := by + have := program.stepi_eq_0x4005b4 h_program h_pc h_err + simp only [minimal_theory] at this + simp_all only [run, cut, this, state_simp_rules, bitvec_rules, minimal_theory] + split + · rename_i h + simp_all only [state_simp_rules, bitvec_rules, minimal_theory] + · rename_i h; simp only [minimal_theory] at h + simp_all only [state_simp_rules, minimal_theory] + done + +theorem program.stepi_eq_0x4005b8_cut (s sn : ArmState) + (h_program : s.program = program) + (h_pc : r StateField.PC s = 0x4005b8#64) + (h_err : r StateField.ERR s = StateError.None) + (h_sp_aligned : CheckSPAlignment s) + (h_step : sn = run 1 s) : + cut sn = true ∧ + r StateField.PC sn = 0x4005bc#64 ∧ + r StateField.ERR sn = .None ∧ + sn.program = program ∧ + CheckSPAlignment sn := by + have := program.stepi_eq_0x4005b8 h_program h_pc h_err + simp only [minimal_theory] at this + simp_all only [run, cut, this, state_simp_rules, bitvec_rules, minimal_theory] + done + +-- (TODO) program.stepi_0x4005bc_cut elided. + +------------------------------------------------------------------------------- + +private theorem AddWithCarry.all_ones_identity_64 (x : BitVec 64) : + (AddWithCarry x 0xffffffffffffffff#64 0x1#1).fst = x := by + simp only [AddWithCarry] + bv_decide + +private theorem AddWithCarry.all_ones_zero_flag_64 (x : BitVec 64) : + ((AddWithCarry x 0xffffffffffffffff#64 0x1#1).snd.z = 1#1) ↔ + (x = 0#64) := by + simp only [AddWithCarry, bitvec_rules, state_simp_rules] + repeat split + · bv_decide + · bv_decide + done + +theorem nextc_to_run_from_0x4005a4 (h : pre s0) : + (Correctness.nextc (Sys.run s0 1)) = run 2 s0 := by + simp only [pre, state_simp_rules] at h + obtain ⟨h_s0_pc, h_s0_program, h_s0_err⟩ := h + simp only + [Correctness.nextc, Correctness.arm_run, + Spec'.cut, minimal_theory] + + rw [AddLoop.csteps_eq] + have h_step_1 := program.stepi_0x4005a4_cut s0 (run 1 s0) + simp_all only [minimal_theory, bitvec_rules] + generalize h_s1 : run 1 s0 = s1 at h_step_1 + + -- Stop when the *_cut theorem says (cut ) = true. + rw [AddLoop.csteps_eq] + have h_step_2 := program.stepi_0x4005b0_cut s1 (run 1 s1) + simp_all only [minimal_theory] + generalize h_s2 : run 1 s1 = s2 at h_step_2 + + simp only [←h_s2, ←h_s1, ←run_plus] + done + +theorem effects_of_nextc_from_0x4005a4 + (h_pre : pre s0) + (_h_pc : r StateField.PC s0 = 0x4005a4#64) + (h_run : sf = (Correctness.nextc (Sys.run s0 1))) : + -- I've elided irrelevant effects and non-effects for now. + sf.program = program ∧ + r StateField.PC sf = 0x4005b4#64 ∧ + r StateField.ERR sf = .None ∧ + ((r (StateField.FLAG PFlag.Z) sf = 1#1) ↔ + (r (StateField.GPR 0x0#5) s0 = 0x0#64)) ∧ + r (StateField.GPR 0#5) sf = r (StateField.GPR 0#5) s0 ∧ + r (StateField.GPR 1#5) sf = r (StateField.GPR 1#5) s0 ∧ + CheckSPAlignment sf := by + -- Prelude + rw [nextc_to_run_from_0x4005a4 h_pre] at h_run + -- TODO: Tactic to "explode" conjunctions? + obtain ⟨h_s0_pc, h_s0_program, h_s0_err, h_s0_sp_aligned⟩ := h_pre + -- Symbolic simulation + -- (FIXME) sym_n doesn't play well with unconditional branches. + /- + application type mismatch + program.stepi_0x4005a8 s1 s2 h_s1_program h_s1_pc + argument + h_s1_pc + has type + r StateField.PC s1 = 0x4005b0#64 : Prop + but is expected to have type + r StateField.PC s1 = 0x4005a8#64 : Prop + -/ + -- sym_n 2 + sym_n 1 at s0 + sym_n 1 at s1 + -- (FIXME) better stepi lemma generation + simp (config := {ground := true}) only at h_step_2 + -- Aggregate block effects + -- explode_step h_step_1 + -- explode_step h_step_2 + simp only [run] at h_run + subst h_run + simp only [*, state_simp_rules, bitvec_rules, minimal_theory] + rw [AddWithCarry.all_ones_zero_flag_64] + done + +------------------------------------------------------------------------------- + +theorem nextc_to_run_from_0x4005b4_cond_holds_true (_h_pre : pre s0) + (h_pc : r StateField.PC si = 0x4005b4#64) + (h_cond_holds_true : r (StateField.FLAG PFlag.Z) si = 0#1) + (h_inv : loop_inv s0 si) : + (Correctness.nextc (Sys.run si 1)) = run 4 si := by + simp only [pre, loop_inv, state_simp_rules] at * + obtain ⟨_h_inv_x0_le, h_inv_z, h_inv_x1, h_inv_err, + h_inv_program, h_inv_sp_aligned⟩ := h_inv + simp only + [Correctness.nextc, Correctness.arm_run, + Spec'.cut, minimal_theory] + + rw [AddLoop.csteps_eq] + have h_step_1 := program.stepi_0x4005b4_cut si (run 1 si) + simp_all only [minimal_theory, bitvec_rules] + -- (FIXME) Why do we need this decide? + simp (config := {decide := true}) only [*, minimal_theory] at h_inv_z + simp_all only [h_inv_z, minimal_theory] + -- + generalize h_s1 : run 1 si = s1 at h_step_1 + + rw [AddLoop.csteps_eq] + have h_step_2 := program.stepi_0x4005a8_cut s1 (run 1 s1) + simp_all only [minimal_theory, bitvec_rules] + generalize h_s2 : run 1 s1 = s2 at h_step_2 + + rw [AddLoop.csteps_eq] + have h_step_3 := program.stepi_0x4005ac_cut s2 (run 1 s2) + simp_all only [minimal_theory, bitvec_rules] + generalize h_s3 : run 1 s2 = s3 at h_step_3 + + -- Stop when the *_cut theorem says (cut ) = true. + rw [AddLoop.csteps_eq] + have h_step_4 := program.stepi_0x4005b0_cut s3 (run 1 s3) + simp_all only [minimal_theory, bitvec_rules] + generalize h_s4 : run 1 s3 = s4 at h_step_4 + + -- (FIXME): Ugh, obtaining the intermediate states in terms of each other and + -- the initial states is such a pain! + have h_s4_s1 : s4 = run 3 s1 := by + simp only [←h_s4, ←h_s3, ←run_plus, ←h_s2, + minimal_theory, bitvec_rules] + simp only [←h_s4_s1, h_step_4, + bitvec_rules, minimal_theory] + simp only [h_s4_s1, ←h_s1, ←run_plus] + done + +private theorem non_zero_one_bit_is_one (x : BitVec 1) + (h : ¬ x = 0#1) : + x = 1#1 := by + bv_decide + +theorem nextc_to_run_from_0x4005b4_cond_holds_false (_h_pre : pre s0) + (h_pc : r StateField.PC si = 0x4005b4#64) + (h_cond_holds_false : ¬ (r (StateField.FLAG PFlag.Z) si = 0#1)) + (h_inv : loop_inv s0 si) : + (Correctness.nextc (Sys.run si 1)) = run 1 si := by + simp only [pre, loop_inv, state_simp_rules] at * + obtain ⟨_h_inv_x0_le, h_inv_z, h_inv_x1, h_inv_err, + h_inv_program, h_inv_sp_aligned⟩ := h_inv + simp only + [Correctness.nextc, Correctness.arm_run, + Spec'.cut, minimal_theory] + + -- Stop when the *_cut theorem says (cut ) = true. + rw [AddLoop.csteps_eq] + have h_step_1 := program.stepi_0x4005b4_cut si (run 1 si) + simp_all only [non_zero_one_bit_is_one, minimal_theory, bitvec_rules] + generalize _h_s1 : run 1 si = s1 at h_step_1 + + simp only [run, h_step_1, minimal_theory] + done + +private theorem AddWithCarry.sub_one_64 (x : BitVec 64) : + (AddWithCarry x 0xfffffffffffffffe#64 0x1#1).fst = x - 1#64 := by + simp only [AddWithCarry] + bv_decide + +theorem effects_of_nextc_from_0x4005b4_cond_holds_true + (h_pre : pre s0) + (h_pc : r StateField.PC si = 0x4005b4#64) + (h_cond_holds_true : r (StateField.FLAG PFlag.Z) si = 0#1) + (h_inv : loop_inv s0 si) + (h_run : sf = (Correctness.nextc (Sys.run si 1))) : + r (StateField.GPR 0#5) sf = r (StateField.GPR 0x0#5) si - 0x1#64 ∧ + r (StateField.GPR 1#5) sf = + (AddWithCarry (r (StateField.GPR 0x1#5) s0 + + (r (StateField.GPR 0x0#5) s0 - + r (StateField.GPR 0x0#5) si)) + 0x1#64 + 0x0#1).fst ∧ + r (StateField.FLAG PFlag.Z) sf = + (AddWithCarry (r (StateField.GPR 0x0#5) si - 0x1#64) + 0xffffffffffffffff#64 0x1#1).snd.z ∧ + r StateField.PC sf = 0x4005b4#64 ∧ + r StateField.ERR sf = .None ∧ + sf.program = program ∧ + CheckSPAlignment sf := by + -- Prelude + rw [nextc_to_run_from_0x4005b4_cond_holds_true + h_pre h_pc h_cond_holds_true h_inv] at h_run + simp only [state_simp_rules, loop_inv] at h_inv + obtain ⟨_h_inv_x0_le, h_inv_z, h_inv_x1, h_inv_err, + h_inv_program, h_inv_sp_aligned⟩ := h_inv + simp (config := {decide := true}) only + [h_cond_holds_true, minimal_theory] at h_inv_z + -- Symbolic simulation + -- (TODO) Better handling for branch instructions. + init_next_step h_run h_step_1 s1 + rw [program.stepi_eq_0x4005b4] at h_step_1 + simp only [*, bitvec_rules, minimal_theory] at h_step_1 + (intro_fetch_decode_lemmas h_step_1 h_inv_program "h_inv"; + all_goals (try assumption)) + -- + sym_n 3 at s1 + -- Aggregating the effects + simp (config := {ground := true}) only + at h_step_2 h_step_3 h_step_4 + simp only [run] at h_run + simp only [*, AddWithCarry.sub_one_64, + state_simp_rules, bitvec_rules, minimal_theory] + done + +theorem effects_of_nextc_from_0x4005b4_cond_holds_false + (h_pre : pre s0) + (h_pc : r StateField.PC si = 0x4005b4#64) + (h_cond_holds_false : ¬ (r (StateField.FLAG PFlag.Z) si = 0#1)) + (h_inv : loop_inv s0 si) + (h_run : sf = (Correctness.nextc (Sys.run si 1))) : + r (StateField.GPR 0#5) sf = 0#64 ∧ + r (StateField.GPR 1#5) sf = + r (StateField.GPR 0x1#5) s0 + r (StateField.GPR 0x0#5) s0 ∧ + r (StateField.FLAG PFlag.Z) sf = 1#1 ∧ + r StateField.PC sf = 0x4005b8#64 ∧ + r StateField.ERR sf = .None ∧ + sf.program = program ∧ + CheckSPAlignment sf := by + -- Prelude + rw [nextc_to_run_from_0x4005b4_cond_holds_false + h_pre h_pc h_cond_holds_false h_inv] at h_run + simp only [state_simp_rules, loop_inv] at h_inv + obtain ⟨_h_inv_x0_le, h_inv_z, h_inv_x1, h_inv_err, + h_inv_program, h_inv_sp_aligned⟩ := h_inv + simp (config := {decide := true}) only + [non_zero_one_bit_is_one, h_cond_holds_false, minimal_theory] at h_inv_z + -- Symbolic simulation + -- sym_n 1 at si + -- (TODO) Better handling for branch instructions. + init_next_step h_run h_step_1 s1 + rw [program.stepi_eq_0x4005b4] at h_step_1 + simp only [*, non_zero_one_bit_is_one, bitvec_rules, minimal_theory] + at h_step_1 + (intro_fetch_decode_lemmas h_step_1 h_inv_program "h_inv"; + all_goals (try assumption)) + -- Aggregating the effects + simp only [run] at h_run + simp only [*, non_zero_one_bit_is_one, + state_simp_rules, bitvec_rules, minimal_theory] + done + +------------------------------------------------------------------------------- + +theorem nextc_to_run_from_0x4005b8 (_h_pre : pre s0) + (h_pc : r StateField.PC si = 0x4005b8#64) + (h_assert : loop_post s0 si) : + Correctness.nextc (Sys.run si 1) = run 1 si := by + simp only [pre, loop_post, state_simp_rules] at * + obtain ⟨_h_inv_x0, h_inv_err, h_inv_program, h_inv_sp_aligned⟩ := h_assert + + simp only + [Correctness.nextc, Correctness.arm_run, + Spec'.cut, minimal_theory] + + -- Stop when the *_cut theorem says (cut ) = true. + rw [AddLoop.csteps_eq] + have h_step_1 := program.stepi_eq_0x4005b8_cut si (run 1 si) + simp_all only [minimal_theory, bitvec_rules] + generalize _h_s1 : run 1 si = s1 at h_step_1 + + simp only [run_opener_zero, h_step_1, minimal_theory] + done + +theorem effects_of_nextc_from_0x4005b8 (_h_pre : pre s0) + (h_pc : r StateField.PC si = 0x4005b8#64) + (h_assert : loop_post s0 si) + (h_run : sf = Correctness.nextc (Sys.run si 1)) : + r (StateField.GPR 0#5) sf = r (StateField.GPR 1#5) si ∧ + r StateField.PC sf = 0x4005bc#64 ∧ + r StateField.ERR sf = .None ∧ + sf.program = program ∧ + CheckSPAlignment sf := by + -- Prelude + rw [nextc_to_run_from_0x4005b8 _h_pre h_pc h_assert] at h_run + -- TODO: Tactic to "explode" conjunctions? + obtain ⟨_h_inv_x0, h_inv_err, h_inv_program, h_inv_sp_aligned⟩ := h_assert + -- Symbolic simulation + -- TODO: Why do we need `try assumption` here? + sym_n 1 at si <;> try assumption + -- Aggregate effects. + simp only [run] at h_run + subst h_run + simp only [*, state_simp_rules, bitvec_rules, minimal_theory] + done + +------------------------------------------------------------------------------- + +-- TODO: Upstream? +@[bitvec_rules] +theorem BitVec.le_refl (x : BitVec n) : + x <= x := by + exact BitVec.le_of_eq x x rfl + +private theorem loop_inv_x0_le (x y : BitVec 64) + (h_assert_x0 : x ≤ y) + (h_assert_x0_nz : ¬x = 0x0#64) : + x - 0x1#64 ≤ y := by + bv_omega + +private theorem AddWithCarry.add_one_64 (x : BitVec 64) : + (AddWithCarry x 0x1#64 0x0#1).fst = x + 0x1#64 := by + simp only [AddWithCarry, bitvec_rules] + bv_omega + +private theorem crock_lemma (x y z : BitVec 64) : + x + (y - z) + 1#64 = x + (y - (z - 1#64)) := by + -- (FIXME) Without this apply below, bv_omega crashes my editor. + apply BitVec.eq_sub_iff_add_eq.mp + bv_omega + +theorem partial_correctness : + PartialCorrectness ArmState := by + apply Correctness.partial_correctness_from_verification_conditions + case v1 => + intro s0 h_pre + simp_all only [Spec.pre, pre, Spec'.assert, assert, + minimal_theory] + case v2 => + intro sf h_exit + simp_all only [Spec.exit, exit, Spec'.cut, cut, + state_simp_rules, minimal_theory] + case v3 => + intro s0 sf h_assert h_exit + -- (FIXME) Remove Spec.post to replicate bug where simp_all somehow + -- aggressively makes the goal unprovable. + simp_all only [Spec'.assert, Spec.exit, assert, exit, Spec.post] + case v4 => + intro s0 si h_assert h_exit + simp_all only [Spec'.assert, Spec.exit, assert, exit, + minimal_theory, state_simp_rules] + obtain ⟨h_pre, h_assert⟩ := h_assert + split at h_assert + · -- Next cutpoint from 0x4005a4#64 (first instruction) + generalize h_sn : (Correctness.nextc (Sys.run si 1)) = sn + subst h_assert + simp_all only [bitvec_rules, minimal_theory] + have h_effects := @effects_of_nextc_from_0x4005a4 si sn + simp only [*, minimal_theory] at h_effects + simp only [h_effects, loop_inv, + state_simp_rules, bitvec_rules, minimal_theory] + done + · -- Next cutpoint from 0x4005b4#64 (loop guard) + generalize h_sn : (Correctness.nextc (Sys.run si 1)) = sn + by_cases h_cond_holds : r (StateField.FLAG PFlag.Z) si = 0x0#1 + case pos => + have h_effects := + @effects_of_nextc_from_0x4005b4_cond_holds_true s0 si sn + simp only [*, minimal_theory] at h_effects + simp only [*, loop_inv, + state_simp_rules, bitvec_rules, minimal_theory] + simp (config := {decide := true}) only + [loop_inv, h_cond_holds, non_zero_one_bit_is_one, + state_simp_rules, bitvec_rules, minimal_theory] + at h_assert + obtain ⟨h_assert_x0, h_assert_x0_nz, _h_assert_x1, _, _, _⟩ := h_assert + apply And.intro + · apply loop_inv_x0_le + (r (StateField.GPR 0x0#5) si) (r (StateField.GPR 0x0#5) s0) + h_assert_x0 h_assert_x0_nz + · apply And.intro + · apply AddWithCarry.all_ones_zero_flag_64 + · simp only [AddWithCarry.add_one_64] + rw [crock_lemma] + case neg => + have h_effects := + @effects_of_nextc_from_0x4005b4_cond_holds_false s0 si sn + simp only [*, minimal_theory] at h_effects + simp only [*, loop_post, spec, + minimal_theory, bitvec_rules, state_simp_rules] + ac_rfl + done + · -- Next cutpoint from 0x4005b8#64 (first instruction after loop) + generalize h_sn : (Correctness.nextc (Sys.run si 1)) = sn + have h_effects := @effects_of_nextc_from_0x4005b8 s0 si sn + simp only [*, minimal_theory] at h_effects + simp only [h_effects, post, + state_simp_rules, bitvec_rules, minimal_theory] + simp only [loop_post, + state_simp_rules, bitvec_rules, minimal_theory] + at h_assert + simp_all only + done + · -- Next cutpoint from 0x4005bc#64 (last instruction) + -- No such cutpoint exists: + contradiction + · -- No further cutpoints exist. + simp_all only + done + +theorem termination : + Termination ArmState := by + simp [Termination, Spec.pre, Spec.exit, exit, + state_simp_rules, bitvec_rules, minimal_theory] + intro s h_pre + sorry + +end AddLoop diff --git a/Proofs/Experiments/SHA512MemoryAliasing.lean b/Proofs/Experiments/SHA512MemoryAliasing.lean index 552e52b5..da4ec22f 100644 --- a/Proofs/Experiments/SHA512MemoryAliasing.lean +++ b/Proofs/Experiments/SHA512MemoryAliasing.lean @@ -7,7 +7,7 @@ import Arm.Exec import Arm.Memory.MemoryProofs import Specs.SHA512 -- import Tactics.Sym --- import Proofs.SHA512.Sha512StepLemmas +-- import Proofs.SHA512.SHA512StepLemmas open BitVec /- The memory aliasing proof obligations in diff --git a/Proofs/Proofs.lean b/Proofs/Proofs.lean index 01ee77b7..a7132a87 100644 --- a/Proofs/Proofs.lean +++ b/Proofs/Proofs.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author(s): Shilpi Goel, Siddharth Bhat -/ import «Proofs».MultiInsts -import «Proofs».«SHA512».Sha512 +import «Proofs».«SHA512».SHA512 import Proofs.«AES-GCM».GCM import Proofs.Popcount32 @@ -15,4 +15,5 @@ import Proofs.Experiments.SHA512MemoryAliasing import Proofs.Experiments.Max import Proofs.Experiments.Abs import Proofs.Experiments.AbsVCG +import Proofs.Experiments.AddLoop import Proofs.Experiments.MemCpyVCG diff --git a/Proofs/SHA512/SHA512.lean b/Proofs/SHA512/SHA512.lean new file mode 100644 index 00000000..3695135f --- /dev/null +++ b/Proofs/SHA512/SHA512.lean @@ -0,0 +1,3 @@ +import Proofs.SHA512.SHA512_block_armv8_rules +import Proofs.SHA512.SHA512_block_armv8 +import Proofs.SHA512.SHA512Sym diff --git a/Proofs/SHA512/SHA512StepLemmas.lean b/Proofs/SHA512/SHA512StepLemmas.lean new file mode 100644 index 00000000..ee35149a --- /dev/null +++ b/Proofs/SHA512/SHA512StepLemmas.lean @@ -0,0 +1,21 @@ +/- +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): Alex Keizer, Shilpi Goel +-/ + +import Tests.SHA2.SHA512Program +import Tactics.StepThms + +-- set_option trace.gen_step.debug.heartBeats true in +-- set_option trace.gen_step.print_names true in +set_option maxHeartbeats 2000000 in +#genStepEqTheorems SHA512.program + +/-- +info: SHA512.program.stepi_eq_0x126c90 {s : ArmState} (h_program : s.program = SHA512.program) + (h_pc : r StateField.PC s = 1207440#64) (h_err : r StateField.ERR s = StateError.None) : + stepi s = w StateField.PC (if ¬r (StateField.GPR 2#5) s = 0#64 then 1205504#64 else 1207444#64) s +-/ +#guard_msgs in +#check SHA512.program.stepi_eq_0x126c90 diff --git a/Proofs/SHA512/Sha512Sym.lean b/Proofs/SHA512/SHA512Sym.lean similarity index 90% rename from Proofs/SHA512/Sha512Sym.lean rename to Proofs/SHA512/SHA512Sym.lean index 50b2699e..76a00d1f 100644 --- a/Proofs/SHA512/Sha512Sym.lean +++ b/Proofs/SHA512/SHA512Sym.lean @@ -6,11 +6,11 @@ Author(s): Shilpi Goel import Arm.Exec import Arm.Util import Tactics.Sym -import Proofs.SHA512.Sha512StepLemmas +import Proofs.SHA512.SHA512StepLemmas import Lean open BitVec -section SHA512_Proof +namespace SHA512 -- set_option debug.skipKernelTC true in -- set_option profiler true in @@ -20,7 +20,7 @@ theorem sha512_block_armv8_test_4_sym (s0 s_final : ArmState) (h_s0_err : read_err s0 = StateError.None) (h_s0_sp_aligned : CheckSPAlignment s0) (h_s0_pc : read_pc s0 = 0x1264c4#64) - (h_s0_program : s0.program = sha512_program) + (h_s0_program : s0.program = program) (h_run : s_final = run 11 s0) : read_err s_final = StateError.None := by -- Prelude @@ -45,4 +45,4 @@ theorem sha512_block_armv8_test_4_sym (s0 s_final : ArmState) -- clear h_s0_x31 -/ -end SHA512_Proof +end SHA512 diff --git a/Proofs/SHA512/Sha512_block_armv8.lean b/Proofs/SHA512/SHA512_block_armv8.lean similarity index 100% rename from Proofs/SHA512/Sha512_block_armv8.lean rename to Proofs/SHA512/SHA512_block_armv8.lean diff --git a/Proofs/SHA512/Sha512_block_armv8_rules.lean b/Proofs/SHA512/SHA512_block_armv8_rules.lean similarity index 100% rename from Proofs/SHA512/Sha512_block_armv8_rules.lean rename to Proofs/SHA512/SHA512_block_armv8_rules.lean diff --git a/Proofs/SHA512/Sha512.lean b/Proofs/SHA512/Sha512.lean deleted file mode 100644 index dd1cc482..00000000 --- a/Proofs/SHA512/Sha512.lean +++ /dev/null @@ -1,3 +0,0 @@ -import Proofs.SHA512.Sha512_block_armv8_rules -import Proofs.SHA512.Sha512_block_armv8 -import Proofs.SHA512.Sha512Sym diff --git a/Proofs/SHA512/Sha512DecodeExecLemmas.lean b/Proofs/SHA512/Sha512DecodeExecLemmas.lean deleted file mode 100644 index 91c6aece..00000000 --- a/Proofs/SHA512/Sha512DecodeExecLemmas.lean +++ /dev/null @@ -1,33 +0,0 @@ -import Tactics.StepThms -import Proofs.SHA512.Sha512Program --- import Tests.SHA2.SHA512ProgramTest - --- set_option trace.gen_step.debug.heartBeats true in --- set_option trace.gen_step.print_names true in -set_option maxHeartbeats 1002500 in -#genStepTheorems sha512_program thmType:="decodeExec" - -/-- -info: sha512_program.decode_0x1264e8 : - decode_raw_inst 1310722675#32 = - some - (ArmInst.DPSFP - (DataProcSFPInst.Advanced_simd_two_reg_misc - { _fixed1 := 0#1, Q := 1#1, U := 0#1, _fixed2 := 14#5, size := 0#2, _fixed3 := 16#5, opcode := 0#5, - _fixed4 := 2#2, Rn := 19#5, Rd := 19#5 })) --/ -#guard_msgs in -#check sha512_program.decode_0x1264e8 - -/-- -info: sha512_program.exec_0x126c90 (s : ArmState) : - exec_inst - (ArmInst.BR (BranchInst.Compare_branch { sf := 1#1, _fixed := 26#5, op := 1#1, imm19 := 523804#19, Rt := 2#5 })) - s = - w StateField.PC - (if ¬r (StateField.GPR 2#5) s = 0#64 then r StateField.PC s + 18446744073709549680#64 - else r StateField.PC s + 4#64) - s --/ -#guard_msgs in -#check sha512_program.exec_0x126c90 diff --git a/Proofs/SHA512/Sha512FetchLemmas.lean b/Proofs/SHA512/Sha512FetchLemmas.lean deleted file mode 100644 index 98d5fe95..00000000 --- a/Proofs/SHA512/Sha512FetchLemmas.lean +++ /dev/null @@ -1,15 +0,0 @@ -import Tactics.StepThms -import Proofs.SHA512.Sha512Program --- import Tests.SHA2.SHA512ProgramTest - --- set_option trace.gen_step.debug.heartBeats true in --- set_option trace.gen_step.print_names true in -set_option maxHeartbeats 1000000 in -#genStepTheorems sha512_program thmType:="fetch" - -/-- -info: sha512_program.fetch_0x1264e8 (s : ArmState) (h : s.program = sha512_program) : - fetch_inst (1205480#64) s = some 1310722675#32 --/ -#guard_msgs in -#check sha512_program.fetch_0x1264e8 diff --git a/Proofs/SHA512/Sha512StepLemmas.lean b/Proofs/SHA512/Sha512StepLemmas.lean deleted file mode 100644 index 4b246fbd..00000000 --- a/Proofs/SHA512/Sha512StepLemmas.lean +++ /dev/null @@ -1,15 +0,0 @@ -import Proofs.SHA512.Sha512Program -import Tactics.StepThms - --- set_option trace.gen_step.debug.heartBeats true in --- set_option trace.gen_step.print_names true in -set_option maxHeartbeats 2000000 in -#genStepEqTheorems sha512_program - -/-- -info: sha512_program.stepi_eq_0x126c90 {s : ArmState} (h_program : s.program = sha512_program) - (h_pc : r StateField.PC s = 1207440#64) (h_err : r StateField.ERR s = StateError.None) : - stepi s = w StateField.PC (if ¬r (StateField.GPR 2#5) s = 0#64 then 1205504#64 else 1207444#64) s --/ -#guard_msgs in -#check sha512_program.stepi_eq_0x126c90 diff --git a/Tactics/StepThms.lean b/Tactics/StepThms.lean index 3f9eb8df..710e0940 100644 --- a/Tactics/StepThms.lean +++ b/Tactics/StepThms.lean @@ -224,321 +224,6 @@ elab "#genStepEqTheorems" program:term : command => liftTermElabM do SymM.run name (persist := true) <| genStepEqTheorems - -/- Generate and prove a fetch theorem of the following form: -``` -theorem .("fetch_0x" ++
) (s : ArmState) - (h : s.program = ) : fetch_inst
s = some -``` --/ -def genFetchTheorem (program_name : Name) (address_str : String) - (orig_map address_expr raw_inst_expr : Expr) - : MetaM Unit := do - let startHB ← IO.getNumHeartbeats - trace[gen_step.debug.heartBeats] "[genFetchTheorem] Start heartbeats: {startHB}" - let declName := Name.str program_name ("fetch_0x" ++ address_str) - let s_program_hyp_fn := - fun s => -- (s.program = ) - (mkAppN (mkConst ``Eq [1]) - #[(mkConst ``Program), - (mkAppN (mkConst ``ArmState.program) #[s]), - orig_map]) - let fetch_inst_fn := fun s => -- (fetch_inst ) - (mkAppN (mkConst ``fetch_inst) #[address_expr, s]) - let bitvec32 := (mkAppN (mkConst ``BitVec) #[mkRawNatLit 32]) - let opt_bitvec32 := (mkAppN (mkConst ``Option [0]) #[bitvec32]) - let raw_inst_rhs := (mkAppN (mkConst ``Option.some [0]) #[bitvec32, raw_inst_expr]) - let orig_thm := -- ∀ (s : ArmState), (h : s.program = ) : - -- fetch_inst s = some - forallE `s (mkConst ``ArmState) - (forallE (Name.mkSimple "h") - (s_program_hyp_fn (bvar 0)) - (mkAppN (mkConst ``Eq [1]) - #[opt_bitvec32, (fetch_inst_fn (bvar 1)), raw_inst_rhs]) - Lean.BinderInfo.default) - Lean.BinderInfo.default - trace[gen_step.debug] "[genFetchTheorem] Statement of the theorem: {orig_thm}" - withLocalDeclD `s (mkConst ``ArmState) fun s => do - withLocalDeclD `h (s_program_hyp_fn s) fun _h => do - let lhs := fetch_inst_fn s - trace[gen_step.debug] "[genFetchTheorem] lhs: {lhs}" - let (ctx, simprocs) ← LNSymSimpContext (config := {ground := false}) - (simp_attrs := #[`minimal_theory]) - (thms := #[``fetch_inst_from_program]) - (simprocs := #[``reduceMapFind?]) - -- Adding local declarations to the context. - let mut simpTheorems := ctx.simpTheorems - let hs ← getPropHyps - for h in hs do - trace[gen_step.debug] "[genFetchTheorem] Prop. in Local Context: {← h.getType}" - unless simpTheorems.isErased (.fvar h) do - simpTheorems ← simpTheorems.addTheorem (.fvar h) (← h.getDecl).toExpr - let ctx := { ctx with simpTheorems } - let (result, _) ← simp lhs ctx simprocs - trace[gen_step.debug] "[genFetchTheorem] Simp result: result: {result.expr}" - trace[gen_step.debug] "[genFetchTheorem] result.proof?: {result.proof?}" - -- FIXME: Is this DefEq check necessary? - -- if ! (← isDefEq result.expr raw_inst_rhs) then - -- throwError "[genFetchTheorem] {lhs} simplified to {result.expr}, which is not \ - -- the expected term, {raw_inst_rhs}" - -- Why do we need to add s explicitly here? - let args := #[s] ++ (hs.map (fun f => (.fvar f))) - let value ← mkLambdaFVars args result.proof?.get! (usedOnly := true) (usedLetOnly := true) - trace[gen_step.debug] "[genFetchTheorem] Proof: {value}" - let decl := Declaration.thmDecl { - name := declName, - -- TODO: Compute levelParams instead of hard-coding it? - levelParams := [], - type := orig_thm, - value := value - } - addDecl decl - -- addAndCompile decl - trace[gen_step.print_names] "[Proved theorem {declName}.]" - let stopHB ← IO.getNumHeartbeats - trace[gen_step.debug.heartBeats] "[genFetchTheorem]: Stop heartbeats: {stopHB}" - trace[gen_step.debug.heartBeats] "[genFetchTheorem]: HeartBeats used: {stopHB - startHB}" - -/- Generate and prove an exec theorem of the following form: -``` -theorem .("exec_0x" ++ ) (s : ArmState) : - exec_inst s = -``` --/ -def genExecTheorem (program_name : Name) (address_str : String) - (decoded_inst : Expr) : MetaM Unit := do - let startHB ← IO.getNumHeartbeats - trace[gen_step.debug.heartBeats] "[genExecTheorem] Start heartbeats: {startHB}" - let declName := Name.str program_name ("exec_0x" ++ address_str) - withLocalDeclD `s (mkConst ``ArmState) fun s => do - let exec_inst_expr := (mkAppN (mkConst ``exec_inst) #[decoded_inst, s]) - trace[gen_step.debug] "[Exec_inst Expression: {exec_inst_expr}]" - -- let sp_aligned ← (mkAppM ``Eq #[(← mkAppM ``CheckSPAlignment #[s]), (mkConst ``true)]) - -- logInfo m!"sp_aligned: {sp_aligned}" - -- withLocalDeclD `h_sp_aligned sp_aligned fun _h_sp_aligned => do - let (ctx, simprocs) ← - LNSymSimpContext - -- Unfortunately, using `ground := true` exposes a lot of internal BitVec - -- structure in terms of Fin. - (config := {decide := true, ground := false}) - (simp_attrs := #[`minimal_theory, `bitvec_rules, `state_simp_rules]) - (decls_to_unfold := #[``exec_inst]) - -- Adding local declarations to the context. - let mut simpTheorems := ctx.simpTheorems - let hs ← getPropHyps - for h in hs do - trace[gen_step.debug] "[genExecTheorem] Prop. in Local Context: {← h.getType}" - unless simpTheorems.isErased (.fvar h) do - simpTheorems ← simpTheorems.addTheorem (.fvar h) (← h.getDecl).toExpr - let ctx := { ctx with simpTheorems } - let (exec_inst_result, _) ← simp exec_inst_expr ctx simprocs - trace[gen_step.debug] "[Exec_inst Simplified Expression: {exec_inst_result.expr}]" - let hs ← getPropHyps - let args := #[s] ++ (hs.map (fun f => (.fvar f))) - let thm ← mkAppM ``Eq #[exec_inst_expr, exec_inst_result.expr] - let type ← mkForallFVars args thm -- (usedOnly := true) (usedLetOnly := false) - trace[gen_step.debug] "[Exec_inst Theorem: {type}.]" - let value ← mkLambdaFVars args exec_inst_result.proof?.get! - -- (usedOnly := true) (usedLetOnly := false) - let decl := Declaration.thmDecl - -- TODO: Compute levelParams instead of hard-coding it? - { name := declName, levelParams := [], - type := type, value := value } - addDecl decl - trace[gen_step.print_names] "[Proved theorem {declName}.]" - let stopHB ← IO.getNumHeartbeats - trace[gen_step.debug.heartBeats] "[genExecTheorem]: Stop heartbeats: {stopHB}" - trace[gen_step.debug.heartBeats] "[genExecTheorem]: HeartBeats used: {stopHB - startHB}" - -/- Generate and prove a decode theorem of the following form: -``` -theorem ( ++ "decode_0x" ++ ) (s : ArmState) : - decode_raw_inst = -``` - -The is then used as an input to `genExecTheorem` to generate -an exec theorem. --/ -def genDecodeAndExecTheorems (program_name : Name) (address_str : String) - (raw_inst : Expr) : - MetaM Unit := do - let startHB ← IO.getNumHeartbeats - trace[gen_step.debug.heartBeats] "[genDecodeTheorem] Start heartbeats: {startHB}" - let declName := Name.str program_name ("decode_0x" ++ address_str) - let lhs := (mkAppN (Expr.const ``decode_raw_inst []) #[raw_inst]) - -- reduce and whnfD do too much and expose the internal Fin structure of the - -- BitVecs below. whnfR does not do enough and leaves the decode_raw_inst term - -- unsimplified. So we use simp for this simplification. - -- let rhs ← reduce lhs -- whnfD or whnfR? - let (ctx, simprocs) ← LNSymSimpContext (config := {ground := true}) - let (rhs, _) ← simp lhs ctx simprocs - let opt_arminst := (mkAppN (mkConst ``Option [0]) #[(mkConst ``ArmInst [])]) - let type := mkAppN (Expr.const ``Eq [1]) #[opt_arminst, lhs, rhs.expr] - let value := mkAppN (Expr.const ``Eq.refl [1]) #[opt_arminst, lhs] - let decl := Declaration.thmDecl { - name := declName, - -- TODO: Compute levelParams instead of hard-coding it? - levelParams := [], - type := type, - value := value - } - addDecl decl - trace[gen_step.print_names] "[Proved theorem {declName}.]" - let_expr Option.some _ decoded_inst ← rhs.expr | - throwError "[genDecodeTheorem] Instruction {raw_inst} could not be decoded!" - let stopHB ← IO.getNumHeartbeats - trace[gen_step.debug.heartBeats] "[genDecodeTheorem]: Stop heartbeats: {stopHB}" - trace[gen_step.debug.heartBeats] "[genDecodeTheorem]: HeartBeats used: {stopHB - startHB}" - genExecTheorem program_name address_str decoded_inst - -/- Generate and prove a step theorem, using pre-existing fetch, decode, and exec -theorems. The step theorem looks like the following: -``` -theorem ( ++ "stepi_0x" ++ ) (s sn : ArmState) - (h_program : s.program = ) - (h_pc : r StateField.PC s = ) - (h_err : r StateField.ERR s = StateError.None) : - (sn = stepi s) = - (sn = ) -``` --/ -def genStepTheorem (program_name : Name) (address_str : String) - (orig_map address_expr : Expr) (simpExt : Option Name) : MetaM Unit := do - let startHB ← IO.getNumHeartbeats - trace[gen_step.debug.heartBeats] "[genStepTheorem] Start heartbeats: {startHB}" - let declName := Name.str program_name ("stepi_0x" ++ address_str) - let s_program_hyp_fn := - fun s => -- (s.program = ) - (mkAppN (mkConst ``Eq [1]) - #[(mkConst ``Program), - (mkAppN (mkConst ``ArmState.program) #[s]), - orig_map]) - let bitvec64 := (mkAppN (mkConst ``BitVec) #[mkRawNatLit 64]) - let s_pc_hyp_fn := - fun s => -- (r StateField.PC s = ) - (mkAppN (Expr.const ``Eq [1]) - #[bitvec64, - (mkAppN (Expr.const ``r []) #[mkConst ``StateField.PC, s]), - address_expr]) - let s_err_hyp_fn := - fun s => -- (r StateField.ERR s = StateError.None) - (mkAppN (Expr.const ``Eq [1]) - #[mkConst ``StateError, - (mkAppN (Expr.const ``r []) #[mkConst ``StateField.ERR, s]), - (mkConst ``StateError.None)]) - let stepi_fn := fun sn s => -- (sn = stepi s) - (mkAppN (mkConst ``Eq [1]) - #[mkConst ``ArmState, sn, (mkAppN (mkConst ``stepi) #[s])]) - let helper_thms := - -- We assume that the necessary fetch, decode, and exec theorems already exist. - Array.map - (fun str => Name.str program_name (str ++ address_str)) - #["fetch_0x", "decode_0x", "exec_0x"] - withLocalDeclD `sn (mkConst ``ArmState) fun sn => do - withLocalDeclD `s (mkConst ``ArmState) fun s => do - withLocalDeclD `h_program (s_program_hyp_fn s) fun _h_program => do - withLocalDeclD `h_pc (s_pc_hyp_fn s) fun _h_program => do - withLocalDeclD `h_err (s_err_hyp_fn s) fun _h_err => do - let lhs := stepi_fn sn s - trace[gen_step.debug] "[genStepTheorem] lhs: {lhs}" - let (ctx, simprocs) ← LNSymSimpContext (config := {ground := false, decide := false}) - (simp_attrs := #[`minimal_theory, `bitvec_rules]) - (decls_to_unfold := #[``stepi, ``read_pc, ``read_err]) - (thms := helper_thms) - (simprocs := #[]) - -- Adding local declarations to the context. - let mut simpTheorems := ctx.simpTheorems - let hs ← getPropHyps - for h in hs do - trace[gen_step.debug] "[genStepTheorem] Prop. in Local Context: {← h.getType}" - unless simpTheorems.isErased (.fvar h) do - simpTheorems ← simpTheorems.addTheorem (.fvar h) (← h.getDecl).toExpr - let ctx := { ctx with simpTheorems } - let (result, _) ← simp lhs ctx simprocs - trace[gen_step.debug] "[genStepTheorem] Simp result: result: {result.expr}" - trace[gen_step.debug] "[genStepTheorem] result.proof?: {result.proof?}" - -- Why do we need to add s explicitly here? - let args := #[s, sn] ++ (hs.map (fun f => (.fvar f))) - let thm ← mkAppM ``Eq #[lhs, result.expr] - -- let (_, changed_expr, unchanged_expr) ← getChangedUnchangedExprs result.expr - -- let thm ← mkAppM ``Iff #[lhs, (mkAnd changed_expr unchanged_expr)] - let type ← mkForallFVars args thm -- (usedOnly := true) (usedLetOnly := false) - trace[gen_step.debug] "[genStepTheorem] type: {type}" - let value ← mkLambdaFVars args result.proof?.get! (usedOnly := true) (usedLetOnly := true) - trace[gen_step.debug] "[genStepTheorem] Proof: {value}" - let decl := Declaration.thmDecl { - name := declName, - -- TODO: Compute levelParams instead of hard-coding it? - levelParams := [], - type := type, - value := value -- (← mkSorry type (synthetic := true)) - } - addDecl decl - -- Unlike the fetch, decode, and exec theorems, which we view as ephemeral, - -- the step theorems are added to the simpset `simpExt`. - -- TODO: We should erase the fetch, decode, and exec theorems once we - -- prove the corresponding step theorem. - if simpExt.isSome then - addToSimpExt declName simpExt.get! - trace[gen_step.print_names] "[Proved theorem {declName}.]" - let stopHB ← IO.getNumHeartbeats - trace[gen_step.debug.heartBeats] "[genStepTheorem]: Stop heartbeats: {stopHB}" - trace[gen_step.debug.heartBeats] "[genStepTheorem]: HeartBeats used: {stopHB - startHB}" - -partial def genStepTheorems (program map : Expr) (program_name : Name) - (thm_type : String) (simpExt : Option Name) : MetaM Unit := do - trace[gen_step.debug] "[genStepTheorems: Poised to run whnfD on the map: {map}]" - let map ← whnfD map - trace[gen_step.debug] "[genStepTheorems: after whnfD: {map}]" - match_expr map with - | List.cons _ hd tl => - let hd ← whnfD hd - let_expr Prod.mk _ _ address_expr raw_inst_expr ← hd | - throwError "Unexpected program map entry! {hd}" - let address_expr ← whnfR address_expr -- whnfR vs whnfD? - let raw_inst_expr ← whnfR raw_inst_expr - let some address_string ← getBitVecString? address_expr (hex := true) - | throwError "We expect program addresses to be concrete. \ - Found this instead: {address_expr}." - trace[gen_step.debug] "[genStepTheorems: address_expr {address_expr} \ - raw_inst_expr {raw_inst_expr}]" - if thm_type == "fetch" then - genFetchTheorem program_name address_string program address_expr raw_inst_expr - if thm_type == "decodeExec" then - genDecodeAndExecTheorems program_name address_string raw_inst_expr - if thm_type == "step" then - genStepTheorem program_name address_string program address_expr simpExt - genStepTheorems program tl program_name thm_type simpExt - | List.nil _ => return - | _ => - throwError "Unexpected program map term! {map}" - --- TODO: --- The arguments of this command are pretty clunky. For instance, they are sort --- of named, but we still expect them to appear in the same order. --- Also, it'd be nice to not have `thmType` as a string, but an inductive type --- of legal values. --- Maybe elaborate a StepTheorems object here? See, e.g., declare_config_elab. -elab "#genStepTheorems " arg:term - "thmType:="thmType:str - ext:(name)? : command => liftTermElabM do - let ty := mkConst `Program [] - let arg ← Term.elabTermAndSynthesize arg ty - let arg ← Term.ensureHasType ty arg - - -- Abort if there are any metavariables or free variables in arg. - if arg.hasExprMVar || arg.hasFVar then - throwError "No meta-variable(s) or free variable(s) allowed in arg: {arg}" - else - let .const program_name _ := arg - | throwError "Expected a constant, found:\n\t{arg} - -Tip: you can always introduce an abbreviation, as in: -\tabbrev myProgram : Program := {arg}" - - genStepTheorems arg arg program_name thmType.getString - (if ext.isSome then ext.get!.getName else Option.none) - ----------------------------------------------------------------------------- section StepThmsExample @@ -552,49 +237,6 @@ def test_program : Program := #genStepEqTheorems test_program -#genStepTheorems test_program thmType:="fetch" -/-- -info: test_program.fetch_0x126510 (s : ArmState) (h : s.program = test_program) : - fetch_inst (1205520#64) s = some 1319181371#32 --/ -#guard_msgs in -#check test_program.fetch_0x126510 - -#genStepTheorems test_program thmType:="decodeExec" -/-- -info: test_program.decode_0x126510 : - decode_raw_inst 1319181371#32 = - some - (ArmInst.DPSFP - (DataProcSFPInst.Advanced_simd_three_same - { _fixed1 := 0#1, Q := 1#1, U := 0#1, _fixed2 := 14#5, size := 2#2, _fixed3 := 1#1, Rm := 1#5, opcode := 3#5, - _fixed4 := 1#1, Rn := 1#5, Rd := 27#5 })) --/ -#guard_msgs in -#check test_program.decode_0x126510 - -/-- -info: test_program.exec_0x126510 (s : ArmState) : - exec_inst - (ArmInst.DPSFP - (DataProcSFPInst.Advanced_simd_three_same - { _fixed1 := 0#1, Q := 1#1, U := 0#1, _fixed2 := 14#5, size := 2#2, _fixed3 := 1#1, Rm := 1#5, opcode := 3#5, - _fixed4 := 1#1, Rn := 1#5, Rd := 27#5 })) - s = - w StateField.PC (r StateField.PC s + 4#64) (w (StateField.SFP 27#5) (r (StateField.SFP 1#5) s) s) --/ -#guard_msgs in -#check test_program.exec_0x126510 - -#genStepTheorems test_program thmType:="step" `state_simp_rules -/-- -info: test_program.stepi_0x126510 (s sn : ArmState) (h_program : s.program = test_program) - (h_pc : r StateField.PC s = 1205520#64) (h_err : r StateField.ERR s = StateError.None) : - (sn = stepi s) = (sn = w StateField.PC (1205524#64) (w (StateField.SFP 27#5) (r (StateField.SFP 1#5) s) s)) --/ -#guard_msgs in -#check test_program.stepi_0x126510 - /-- info: test_program.stepi_eq_0x126510 {s : ArmState} (h_program : s.program = test_program) (h_pc : r StateField.PC s = 1205520#64) (h_err : r StateField.ERR s = StateError.None) : @@ -604,7 +246,8 @@ info: test_program.stepi_eq_0x126510 {s : ArmState} (h_program : s.program = tes #check test_program.stepi_eq_0x126510 -- Here's the theorem that we'd actually like to obtain instead of the --- erstwhile test_stepi_0x126510. +-- erstwhile test_program.stepi_eq_0x126510, provided that this +-- enables better aggregation of the effects of a basic block. theorem test_stepi_0x126510_desired (s sn : ArmState) (h_program : s.program = test_program) (h_pc : r StateField.PC s = 1205520#64) @@ -616,7 +259,7 @@ theorem test_stepi_0x126510_desired (s sn : ArmState) -- Non-Effects (∀ (f : StateField), f ≠ StateField.PC ∧ f ≠ StateField.SFP 27#5 → r f sn = r f s) ∧ (∀ (n : Nat) (addr : BitVec 64), read_mem_bytes n addr sn = read_mem_bytes n addr s) := by - simp_all only [minimal_theory, state_simp_rules, bitvec_rules, test_program.stepi_0x126510] + simp_all only [minimal_theory, state_simp_rules, bitvec_rules, test_program.stepi_eq_0x126510] done end StepThmsExample diff --git a/Proofs/SHA512/Sha512Program.lean b/Tests/SHA2/SHA512Program.lean similarity index 98% rename from Proofs/SHA512/Sha512Program.lean rename to Tests/SHA2/SHA512Program.lean index 6f6f0084..112ad34a 100644 --- a/Proofs/SHA512/Sha512Program.lean +++ b/Tests/SHA2/SHA512Program.lean @@ -1,11 +1,19 @@ +/- +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.State +namespace SHA512 + open BitVec -def sha512_program : Program := +-- sha512_block_armv8 +-- Source: https://github.com/aws/aws-lc/blob/main/crypto/fipsmodule/sha/asm/sha512-armv8.pl#L454 +def program : Program := def_program - [ - -- (0x1264c0#64 , 0xa9bf7bfd#32), -- stp x29, x30, [sp, #-16]! + [(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 @@ -507,6 +515,7 @@ def sha512_program : Program := (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) -- ret - ] + (0x126c98#64 , 0xf84107fd#32), -- ldr x29, [sp], #16 + (0x126c9c#64 , 0xd65f03c0#32)] -- ret + +end SHA512 diff --git a/Tests/SHA2/SHA512ProgramTest.lean b/Tests/SHA2/SHA512ProgramTest.lean index f98a6d25..29c0cb86 100644 --- a/Tests/SHA2/SHA512ProgramTest.lean +++ b/Tests/SHA2/SHA512ProgramTest.lean @@ -7,520 +7,12 @@ import Arm.Exec import Arm.Cfg.Cfg import Specs.SHA512 import Tests.Debug +import Tests.SHA2.SHA512Program section SHA512ProgramTest open BitVec --- sha512_block_armv8 --- Source: https://github.com/aws/aws-lc/blob/main/crypto/fipsmodule/sha/asm/sha512-armv8.pl#L454 -def sha512_program_map : Program := - def_program - [(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)] -- ret - /-- info: #[(0, { guard := 0x0000000000126c90#64, @@ -528,7 +20,7 @@ info: #[(0, next := 0x0000000000126c94#64 })] -/ #guard_msgs in -#eval (do let cfg ← (Cfg.create sha512_program_map) +#eval (do let cfg ← (Cfg.create SHA512.program) IO.println s!"{cfg.loops_info}") -- Initial hash value, with the most-significant word first. @@ -595,7 +87,7 @@ def init_sha512_test : ArmState := pc := 0x1264c0#64, pstate := PState.zero, mem := (fun (_ : BitVec 64) => 0#8), - program := sha512_program_map, + program := SHA512.program, error := StateError.None } have h_input : 1024 = 1024 / 8 * 8 := by decide let s := write_mem_bytes (1024 / 8) input_address (BitVec.cast h_input asm_input) s @@ -624,7 +116,7 @@ def final_sha512_hash : BitVec 512 := read_mem_bytes 64 ctx_address final_sha512 example : final_sha512_pc = -- Get the address (first element of the pair) from the -- max. element of sha512_program_map. - sha512_program_map.max!.1 := by + SHA512.program.max!.1 := by native_decide -- The final hash computed by the program is this bitvector below. diff --git a/Tests/Tactics/ReduceFetchInst.lean b/Tests/Tactics/ReduceFetchInst.lean index baebefa8..630bcbbc 100644 --- a/Tests/Tactics/ReduceFetchInst.lean +++ b/Tests/Tactics/ReduceFetchInst.lean @@ -5,7 +5,7 @@ Author(s): Alex Keizer -/ import Tactics.Reflect.FetchAndDecode import Tests.«AES-GCM».GCMGmultV8Program -import Tests.SHA2.SHA512ProgramTest +import Tests.SHA2.SHA512Program /-! ## Tests for `refuceFetchInst` simproc -/ @@ -13,10 +13,10 @@ example (h : s.program = GCMGmultV8Program.gcm_gmult_v8_program) : fetch_inst 0x7d8800#64 s = (some 1279294481#32) := by simp (config := {ground := false}) only [reduceFetchInst] -example (h : s.program = sha512_program_map) : +example (h : s.program = SHA512.program) : fetch_inst 0x1264c0#64 s = (some 0xa9bf7bfd#32) := by simp (config := {ground := false}) only [reduceFetchInst] -example (h : s.program = sha512_program_map) : +example (h : s.program = SHA512.program) : fetch_inst 0x126c98#64 s = (some 0xf84107fd#32) := by simp (config := {ground := false}) only [reduceFetchInst]