seL4
verification for IOAPIC PR seL4/seL4#896
seL4/seL4#896 changes IOAPIC-related decoding slightly and requires a few new small invariants on the Haskell level.
Test with: seL4/seL4#896
Looks good to me (assuming that the
Word_Libfailure is trivial)!
It should be, I moved the lemma manually without checking dependencies, and that's what I get for my laziness :-)
Did the new invariant in
valid_arch_state'really not need any proof updates to show that it's maintained? I'm actually pretty impressed if so, even with it only depending on such specific parts of the state, I would have thought that some of the higher level functions would need at least some manual steps to show it.
I was also pretty impressed. AFAICS it works, because I managed to export the state dependency via abbreviation and therefore the lifting rule for valid_arch_state' still works as before and anything that unfolds valid_arch_state' will simplify out the new parts trivially. It's nice to see those ideas actually fully working every once in a while.
The Word_Lib failure has drawn in a whole slate of word lemma movement from CRefine, so it's probably worth looking at this again before I merge.
I'm confused by the remaining failures but assuming that it's mostly unrelated then it still looks good to me.
They were because the seL4 PR was not rebased yet and didn't have some of the hyp related changes that happened in the meantime. I've pushed a rebased version of the PR and restarted the tests.