08eb78a5b2
This PR sets up the new integrated test/bench suite. It then migrates all benchmarks and some related tests to the new suite. There's also some documentation and some linting. For now, a lot of the old tests are left alone so this PR doesn't become even larger than it already is. Eventually, all tests should be migrated to the new suite though so there isn't a confusing mix of two systems.
39 lines
1.3 KiB
Text
39 lines
1.3 KiB
Text
import Std.Tactic.BVDecide
|
|
|
|
open BitVec
|
|
|
|
theorem cast_unit_1 (x : BitVec 64) : Nat.cast 0 &&& x = 0 := by
|
|
bv_decide
|
|
|
|
theorem cast_unit_2 (x : BitVec 64) : x.zeroExtend 32 = (x.zeroExtend 64).zeroExtend 32 := by
|
|
bv_decide
|
|
|
|
theorem cast_unit_3 (x : BitVec 64) : x.zeroExtend 128 = (x.zeroExtend 64).zeroExtend 128 := by
|
|
bv_decide
|
|
|
|
theorem cast_unit_3' (x : BitVec 64) : x.truncate 128 = (x.truncate 64).zeroExtend 128 := by
|
|
bv_decide
|
|
|
|
theorem cast_unit_4 (x y : BitVec 32) : (x.zeroExtend 64).extractLsb 32 0 = (y.zeroExtend 64).extractLsb 32 0 → x = y := by
|
|
bv_decide
|
|
|
|
theorem cast_unit_5 (x y : BitVec 64) : (x ++ y).extractLsb 63 0 = (y ++ x).extractLsb 127 64 := by
|
|
bv_decide
|
|
|
|
theorem cast_unit_5' (x y : BitVec 64) : (BitVec.append x y).extractLsb 63 0 = (y ++ x).extractLsb 127 64 := by
|
|
bv_decide
|
|
|
|
theorem cast_unit_6 (x : BitVec 64) : x.signExtend 32 = (x.signExtend 64).signExtend 32 := by
|
|
bv_decide
|
|
|
|
theorem cast_unit_7 (x : BitVec 64) : x.signExtend 128 = (x.signExtend 64).signExtend 128 := by
|
|
bv_decide
|
|
|
|
theorem cast_unit_8 (x : BitVec 64) : (x.signExtend 128 = x.zeroExtend 128) ↔ (x.msb = false) := by
|
|
bv_decide
|
|
|
|
theorem cast_unit_9 (x : BitVec 32) : (x.replicate 20).zeroExtend 32 = x := by
|
|
bv_decide
|
|
|
|
theorem cast_unit_10 (x : BitVec 32) : (x.replicate 20).getLsbD 40 = x.getLsbD 8 := by
|
|
bv_decide
|