From 88b16da7c72095787882b06953745a2c17c1b70a Mon Sep 17 00:00:00 2001 From: Shilpi Goel Date: Thu, 1 Feb 2024 17:48:43 -0600 Subject: [PATCH] Bump to leanprover/lean4:v4.5.0 --- Arm/Insts/Common.lean | 2 +- Proofs/SHA512_AssocRepr.lean | 4 ++-- lean-toolchain | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/Arm/Insts/Common.lean b/Arm/Insts/Common.lean index 1f843bc5..2e8b0611 100644 --- a/Arm/Insts/Common.lean +++ b/Arm/Insts/Common.lean @@ -145,7 +145,7 @@ theorem M_divisible_by_esize_of_valid_bit_masks (immN : BitVec 1) (imms : BitVec . simp done --- Resouces on Arm bitmask immediate: +-- Resources on Arm bitmask immediate: -- https://developer.arm.com/documentation/dui0802/b/A64-General-Instructions/MOV--bitmask-immediate- -- https://kddnewton.com/2022/08/11/aarch64-bitmask-immediates.html -- Arm Implementation: diff --git a/Proofs/SHA512_AssocRepr.lean b/Proofs/SHA512_AssocRepr.lean index 986f6ead..579d1d41 100644 --- a/Proofs/SHA512_AssocRepr.lean +++ b/Proofs/SHA512_AssocRepr.lean @@ -565,8 +565,8 @@ theorem sha512_block_armv8_new_program (s : ArmState) simp only simp [exec_inst, *] - unfold run - simp [stepi, h_pc] + + sorry end SHA512_proof diff --git a/lean-toolchain b/lean-toolchain index 3f21e50b..bd59abf4 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.5.0-rc1 +leanprover/lean4:v4.5.0