Bump to leanprover/lean4:v4.5.0

leanprover · Feb 1, 2024 · 88b16da · 88b16da
1 parent 3a761c8
commit 88b16da
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 4 deletions.
diff --git 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
@@ -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
@@ -1 +1 @@
-leanprover/lean4:v4.5.0-rc1
+leanprover/lean4:v4.5.0
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		leanprover/lean4:v4.5.0-rc1
		leanprover/lean4:v4.5.0