Proof checker cannot collapse constant arithmetic

[fixermark]

Fact:

(outIdx + 2) < 400

What I expect:

outIdx < 400 is provable

Observed:

"cannot prove "outIdx < 400": failed at (...). Facts: [. . .] (outIdx + 2) < 400

[nigeltao]

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.

[Dawane9729]

What should the next step be

On Nov 27, 2017 5:42 PM, "Nigel Tao" [email protected] wrote:

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.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/google/puffs/issues/3#issuecomment-347353561, or mute the thread https://github.com/notifications/unsubscribe-auth/AgM_UM31pl3T2F4hCfi2eOoN5iMzn-Zqks5s6zrOgaJpZM4Qqd9q .

[Dawane9729]

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

[nigeltao]

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.