Proof checker cannot collapse constant arithmetic about wuffs HOT 4 OPEN

Yeah, Puffs should be able to prove this. The question is whether this is done implicitly or explicitly. The explicit version would mean that you'd have to write something like

assert outIdx < 400 via "a < b: (a + c) < b; 0 <= c"(c:2)

There is already a very similar, existing explicit 'via' rule called "a < (b + c): a < c; 0 <= b", used in std/gif/decode_lzw.puffs.

Both of those could possibly become implicit, eventually, so you wouldn't have to write explicit assert lines in the program. But it's not obvious yet where to draw the line exactly between a fast-and-dumb proof checker and a full blown smart-and-slow SMT solver.

from wuffs.

from wuffs.

So how should one comment when placed in that spot, I agree fast and dumb is like being ones self like retardedly genius. Acronym

from wuffs.

What should the next step be

If you want to just play around with the built-in rules, edit lang/check/gen.go and run go generate and then go install.

If you want to push those rules upstream, that's a bigger conversation. For example, that would probably involve also taking the Puffs code that requires those new rules, and thus a discussion of whether whatever it is your Puffs code does belongs in the Puffs standard library.

So how should one comment when placed in that spot

Sorry, I don't understand your question.

from wuffs.