[Heapster] Prove mbox_randomize_spec_ref

[m-yac]

This PR finishes what #1478 started by proving spec refinement for mbox_randomize.

In English, the spec I used says:

• If m is non-null, the function returns SUCCESS and m->data is set to some data' such that m->data[i] = data'[i] for all i such that i < m->strt or i >= m->len.
• Otherwise, the function returns MBOX_NULL_ERROR.

[eddywestbrook]

Looks like you proved it! There are some Admitteds for lemmas in SAWCoreBitvectors.v, and although it would be nice to prove these eventually, they are pretty obviously true, so I'm not that worried about it.

My one concern going forwards (just food for thought, no need to address it now) is that the main proof does seem rather long and involved. How hard was this to write? Is the proof just long because there are a lot of rote steps, or are they difficult and involved? Keep in mind that the goal here is not really to prove that our mbox example is correct as much as it is to develop the tools and techniques needed to prove other functions like these correct in the future.

[m-yac]

Is the proof just long because there are a lot of rote steps, or are they difficult and involved?

With the exception of lines 192-196 and 216-220, everything is just bitvector fiddling. I did have to spend some time thinking about how to prove these things (you can see I had to add a few more lemmas too) but if we had some Coq tactic that could prove bitvector inequalities automatically, all these lines would vanish.

As for the SAWCoreBitvectors lemmas, I agree these need to get proven someday, but I don't think it would be worth the time doing that with the current bitvector library we're using. There are other libraries that have already done the work of proving most of these things – plus if we end up using SMTCoq, we would just send everything to an SMT solver anyway. We should probably coordinate with the other users of saw-core-coq before switching bitvector libraries though?

[eddywestbrook]

Yeah, you are right, it would be useful to hook up to an SMT solver for proving some of the bitvector propositions. OTOH, SAW already has a bunch of support for interfacing with SMT solvers, so all this stuff could get sorted out simply by figuring out how to do some or all of this work inside SAW using MRSolver. Or maybe that approach won't be nearly as useful as the manual proof control you get in Coq? Or maybe we will figure some sort of combination of the two?