search

seL4 / l4v

seL4 specification and proofs
https://sel4.systems
Other
504 stars 105 forks source link

Prove `awaken_ccorres` #796

Closed michaelmcinerney closed 2 months ago

Xaphiosis commented 2 months ago

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 commented 2 months ago

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...