✨ Count Zero Bytes

[Vectorized]

Description

Halmos seems to be unable to test equivalence, so here's the Python z3

from z3 import * 

def count_zero_bytes_original(x):
    zero = x * 0
    one = x * 0 + 1
    return (
        If((x & (0xff << (0 * 8))) == 0, one, zero) +
        If((x & (0xff << (1 * 8))) == 0, one, zero) +
        If((x & (0xff << (2 * 8))) == 0, one, zero) +
        If((x & (0xff << (3 * 8))) == 0, one, zero) +
        If((x & (0xff << (4 * 8))) == 0, one, zero) +
        If((x & (0xff << (5 * 8))) == 0, one, zero) +
        If((x & (0xff << (6 * 8))) == 0, one, zero) +
        If((x & (0xff << (7 * 8))) == 0, one, zero) +
        If((x & (0xff << (8 * 8))) == 0, one, zero) +
        If((x & (0xff << (9 * 8))) == 0, one, zero) +
        If((x & (0xff << (10 * 8))) == 0, one, zero) +
        If((x & (0xff << (11 * 8))) == 0, one, zero) +
        If((x & (0xff << (12 * 8))) == 0, one, zero) +
        If((x & (0xff << (13 * 8))) == 0, one, zero) +
        If((x & (0xff << (14 * 8))) == 0, one, zero) +
        If((x & (0xff << (15 * 8))) == 0, one, zero) +
        If((x & (0xff << (16 * 8))) == 0, one, zero) +
        If((x & (0xff << (17 * 8))) == 0, one, zero) +
        If((x & (0xff << (18 * 8))) == 0, one, zero) +
        If((x & (0xff << (19 * 8))) == 0, one, zero) +
        If((x & (0xff << (20 * 8))) == 0, one, zero) +
        If((x & (0xff << (21 * 8))) == 0, one, zero) +
        If((x & (0xff << (22 * 8))) == 0, one, zero) +
        If((x & (0xff << (23 * 8))) == 0, one, zero) +
        If((x & (0xff << (24 * 8))) == 0, one, zero) +
        If((x & (0xff << (25 * 8))) == 0, one, zero) +
        If((x & (0xff << (26 * 8))) == 0, one, zero) +
        If((x & (0xff << (27 * 8))) == 0, one, zero) +
        If((x & (0xff << (28 * 8))) == 0, one, zero) +
        If((x & (0xff << (29 * 8))) == 0, one, zero) +
        If((x & (0xff << (30 * 8))) == 0, one, zero) +
        If((x & (0xff << (31 * 8))) == 0, one, zero)
    )

def count_zero_bytes(x):
    m = BitVecVal(0x7f7f7f7f7f7f7f7f7f7f7f7f7f7f7f7f7f7f7f7f7f7f7f7f7f7f7f7f7f7f7f7f, 256)
    c = ~(((x & m) + m) | x | m)
    c = LShR(c, 7)  # logical right shift
    c = c * BitVecVal(0x0101010101010101010101010101010101010101010101010101010101010101, 256)
    c = c & BitVecVal((1 << 256) - 1, 256)
    c = LShR(c, 248)
    c = c & BitVecVal(0xff, 256)
    return c

x = BitVec('x', 256) 

solve(count_zero_bytes(x) != count_zero_bytes_original(x))

Checklist

Ensure you completed all of the steps below before submitting your pull request:

• Ran forge fmt?
• Ran forge test?

Pull requests with an incomplete checklist will be thrown out.

[github-actions]

Gas Snapshot Comparison Report

Generated at commit : f9ad2d2, Compared to commit : 92e647b

Contract Name	Test Name	Main Gas	PR Gas	Diff
LibBitTest	testAnd()	192744	192766	22
	testCLZ()	306404	306426	22
	testCommonBytePrefix()	1533	1555	22
	testCommonNibblePrefix()	407	429	22
	testFFS()	152877	152899	22
	testFLS()	254403	254337	-66
	testIsPo2()	57685	57707	22
	testPassInBool()	874	829	-45
	testPopCount()	63760	66842	3082
	testReverseBytes()	12514	12536	22
	test__codesize()	6774	7124	350
	testCountZeroBytes()	-	403	-

[Vectorized]

Dang, i have to fix the Natspec, and regen docs. Will do this in a separate PR.