So, I was just starting to work through analyzing these right before everything blew up, so partially I'm piecing this together from notes I don't remember writing--trusting myself that I wrote down correct stuff.
The recent failures can be viewed at: https://reports.makerfoundation.com/k-dss/2addb6a7692db7ba72ef/
I went through the error logs for these previously. Most of them "exploded"--some intimidatingly abstruse stderr.
I tried to replicate Vow_cage-surplus_pass_rough locally; its stderr from the server was an explosion, but locally
it just got "stuck" (no progress being made when viewing the trace in klab debug).
I klab fetched a few of these "exploded" proofs, klab debug just crashes, probably the stuff it actually needs to
consume is missing.
I think the way to move forward is to just pick one at a time, figure out what's going wrong with it, and see how many more proofs that same methodology can be applied to.
To this end, there is one proof that I've spent significant time on that's probably a good place to start.
That would be End_skim_fail_rough.
This one has been broken for a while. Originally, after an exhaustive analysis, I found it was taking a branch that
contradicted conditions it had already assumed, but K wasn't noticing this contradiction. (And it's still doing this
in the latest runs AFAICT, I can't debug it but klab status-js is printing the tell-tale deep branching with one
acceptance).
I had talked to Daejun about a proof that was exhibiting similar behavior before, and he said that the form of the
constraint for fail specs that klab uses (the negation of the conjunction of all iff constraints) is very hard for
K to reason about. He told me about an alternative approach used by RV: break these "failure" specs into a series of
specs as follows:
- determine the conditions that can cause reversion in the function and their sequence, calls the conditions A, B, C etc. So if !A is true, the function reverts, whether B and C are true or not. If A holds, but not B, the function reverts regardless of the valence of C, and so on.
- make a separate spec for each possible reversion, e.g. one with (!A), then one with (A && !B), then (A && B && !C), etc
So I started doing this for End_skim_fail_rough. You can accomplish the above procedure in klab by using
failure in place of behavior (this means "just generate the fail spec"), putting the one thing you want to
falsify in an iff block, and putting the thing you want to hold in an if block.
That's what End_skim-A_fail_rough, End_skim-B_fail_rough, etc are.
When I was originally doing these, all was well up until "H", at which point I got a failure I didn't understand. Since
then, changes in klab and the underlying binaries like K itself have made "C" and "F" start "exploding".
This is actually great news, because End_skim-C_fail_rough is a really simple spec and gives us an excellent place
to start. I can reporduce the "explosion" locally with the latest klab and debug it...nothing is clear from that of
course, because it's not a normal rejection, but rather some sort of crash in the K binary.
stderr
stdout