Open fixermark opened 6 years ago
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.
What should the next step be
On Nov 27, 2017 5:42 PM, "Nigel Tao" notifications@github.com 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 .
So how should one comment when placed in that spot, I agree fast and dumb is like being ones self like retardedly genius. Acronym
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.
Fact:
(outIdx + 2) < 400
What I expect:
outIdx < 400 is provable
Observed:
"cannot prove "outIdx < 400": failed at (...). Facts: [. . .] (outIdx + 2) < 400