Prove awaken_ccorres

[michaelmcinerney]

No description provided.

[Xaphiosis]

I think the approach and proofs look ok. I'm as always a bit worried about the tendency to not have any comments in the proofs to help separate things or guide a potential reader/victim.

For when this isn't a draft: the commit tags aren't right btw (no rt, RISCV64 only, etc)

[michaelmcinerney]

Now (finally) ready for review.

I have added rt to the commit message, but I wasn't sure what to do about adding riscv. We agreed that we wouldn't add riscv to the crefine tag, since RISCV is the only arch we're doing for MCS at the moment. I have still been adding riscv to refine, since we at one point had both ARM and RISCV working for Refine, but we're now just back to RISCV, and I wasn't sure how to add riscv refine without then mentioning the other half a dozen sessions I'm changing here...

[Xaphiosis]

I'm fine with this one. You're right about the commit message, rt does seem to have different standards and in this case I have no idea how they would hang together usefully.