facts involving constants still need extra verbosity to work

[mvdan]

Take this piece of code:

packageid "xxxx"

pri const four u32 = 4

pub func foo(a u32)() {
        if in.a >= four {
                return
        }
        assert in.a < 4 via "a < b: a < c; c == b"(c:four)
}

As it is, it generates with wuffs-c gen -package_name xxxx foo.wuffs just fine.

However, none of the alternative assert lines below work - when I would expect every single one of them to work.

• Reasoning that 4 == four instead of four == 4: assert in.a < 4 via "a < b: a < c; b == c"(c:four). Note, however, that a lone assert 4 == four works just as fine as an assert four == 4, so it seems to be a bug in these assert reason expressions.

check: cannot prove "in.a < 4": no such reason "a < b: a < c; b == c" at foo.wuffs:9. Facts:
        in.a < four

• Asserting assert in.a < 4. In other words, if this works:

if in.a >= 4 {
        return
}
assert in.a < 4

I would expect this to work too, yet it doesn't (at least not without the extra reasoning in the original code):

if in.a >= four {
        return
}
assert in.a < 4

check: cannot prove "in.a < 4" at foo.wuffs:9. Facts:
        in.a < four

I'm also confused by how four == 4 doesn't appear in the error above. It only appears if I'm explicit with an assertion or invariant beforehand:

assert four == 4
assert in.a < 4

check: cannot prove "in.a < 4" at foo.wuffs:10. Facts:
        in.a < four
        four == 4

[mvdan]

If you want the real example: https://github.com/mvdan/zstd/commit/1a75a15a7625e9394fa2ac0f42f563084f854178

In particular, these two lines:

// TODO: hopefully clean up once this issue is
// fixed: https://github.com/google/wuffs/issues/11
assert i <= max_block_size via "a <= b: a <= c; c <= b"(c:block_size)
assert i <= 131072 via "a <= b: a <= c; c == b"(c: max_block_size)

I believe that my simpler examples above are the same underlying issue, but I might be wrong.

[nigeltao]

Yeah, there's more work to do with respect to facts and constants. There's probably some short term, ad hoc, tactical work to make your immediate problems disappear. There's probably also some long term, deeper thinking required about explicit versus implicit facts. In general, having more implicit facts (like your 'obvious' four == 4) makes for shorter Wuffs code, but might make the proof-of-safety or compile times longer, especially so if some of the algorithmic costs are super-linear.

[mvdan]

Thanks for looking into this. Please update this issue if this progresses or changes in any way in the future.