search

seL4 / l4v

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

Several sorries in `IpcCancel_C` #789

Closed michaelmcinerney closed 2 months ago

michaelmcinerney commented 2 months ago

Please see the commit message

michaelmcinerney commented 2 months ago

Cool. Happy to see more sorries melting away and somehow even Refine seems to have a lot of removed lines with this change.

Refine does seem to shrink most of the time I have to touch it. I often do add asserts and might need to strengthen an abstract guard as a result, but I am often able to remove lines by making proofs that were forwards backwards instead, or removing Hoare triples about properties that we no longer need, like valid_idle' or in this case, things about the scheduler action not being resume current thread. I also weakened weak_sch_act_wf, so some of the Hoare triples could just be crunched, now. Hopefully the trend continues.