Facts involving constants don't propagate to bounds checks

[mvdan]

Apologies if this bug report is lacking any information or if I missed anything obvious. But I've been playing with this for over twenty minutes, and I cannot figure it out.

I have a piece of code:

pri const maxBlockSize u32 = 128 << 10 // 128KiB
[...]
var blockSize u32 = [...]
[...]
var i u32
while i < blockSize, inv blockSize <= maxBlockSize {
        assert i <= maxBlockSize via "a <= b: a <= c; c <= b"(c:blockSize)
        i += 1
}

And this gets an error:

check: assignment "i += 1" bounds [1..4294967296] is not within bounds [0..4294967295] at decode.wuffs:87. Facts:
        blockSize <= maxBlockSize
        i < blockSize
        i <= maxBlockSize

It seems to me like from those facts, I should be able to prove that i <= 131072, since 131072 == maxBlockSize and i <= maxBlockSize. However, I don't seem to be able to. I have tried multiple asserts, including assert maxBlockSize == 131072 and assert i <= 131072 via "a <= b: a <= c; c == b"(c:maxBlockSize).

Here's why I think this is a bug in Wuffs - if I replace all uses of maxBlockSize with 131072, the bounds error disappears.

[mvdan]

If you want to reproduce this:

git clone https://github.com/mvdan/zstd
git checkout tmp-break-inv
./build

The HEAD commit in that branch is what replaces the number with the constant name.

[mvdan]

Thanks for the fix!

[mvdan]

@nigeltao playing with this new feature, I hit a fun "cannot prove" error:

check: cannot prove "i <= 131072": cannot prove "block_size <= 131072": failed at decode.wuffs:86. Facts:
        max_block_size == 131072
        block_size <= max_block_size
        i < block_size

The code in question looks like:

var i u32
while i < block_size,
        inv max_block_size == 131072,
        inv block_size <= max_block_size {
        assert i <= max_block_size via "a <= b: a <= c; c <= b"(c:block_size)
        i += 1
}

Shouldn't this work? Or what am I missing?

[mvdan]

Ignore my comment above - I wasn't actually running the compiler on that assertion.