facts involving constants still need extra verbosity to work about wuffs HOT 3 CLOSED

If you want the real example: mvdan/zstd@1a75a15

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.

from wuffs.

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.

from wuffs.

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

from wuffs.