max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: BitVec benchmark after renaming of getLsb (#5217)

Browse source 
fallout from https://github.com/leanprover/lean4/pull/5200
This commit is contained in:
Henrik Böving 2024-08-30 11:08:24 +02:00 • committed by GitHub
parent a50ed83560
commit 648239c6ec
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
tests/bench/bv_decide_realworld.lean
View file

@ -28,7 +28,7 @@ def parity32_spec_rec (i : Nat) (x : BitVec 32) : Bool :=
match i with
| 0 => false
| i' + 1 =>
let bit_idx := BitVec.getLsb x i'
let bit_idx := BitVec.getLsbD x i'
Bool.xor bit_idx (parity32_spec_rec i' x)
def parity32_spec (x : BitVec 32) : Bool :=
@ -42,6 +42,6 @@ def parity32_impl (x : BitVec 32) : BitVec 32 :=
(0x00006996#32 >>> x4) &&& 1#32
theorem parity32_correct (x : BitVec 32) :
(parity32_spec x) = ((parity32_impl x).getLsb 0) := by
(parity32_spec x) = ((parity32_impl x).getLsbD 0) := by
dsimp only [parity32_spec, parity32_impl, parity32_spec_rec]
bv_decide