verification for IOAPIC PR seL4/seL4#896 #753
Conversation
lsf37
force-pushed
the
ioapic
branch
3 times, most recently
from
0d9a0a2
to
ad180ed
Compare
There was a problem hiding this comment.
Looks good to me (assuming that the Word_Lib failure is trivial)!
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.
It should be, I moved the lemma manually without checking dependencies, and that's what I get for my laziness :-)
I was also pretty impressed. AFAICS it works, because I managed to export the state dependency via abbreviation and therefore the lifting rule for |
lsf37
force-pushed
the
ioapic
branch
2 times, most recently
from
5175d01
to
4cae0a9
Compare
|
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. |
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. |
Separate IOAPICs can have different max numbers of IRQs. This PR adds the logic of seL4/seL4#896 for that to the specs. Signed-off-by: Gerwin Klein <[email protected]>
Slighly weaken arch_irq_control_inv_valid -- the condition `pin < ioapicIRQLines` was unused and would now require a new state invariant on x64_ioapic_nirqs to prove. Signed-off-by: Gerwin Klein <[email protected]>
Place constraints on the new IOPAPIC state components x64KSNumIOAPICs and x64KSIOAPICnIRQs to support CRefine arithmetic. Signed-off-by: Gerwin Klein <[email protected]>
Signed-off-by: Gerwin Klein <[email protected]>
Signed-off-by: Gerwin Klein <[email protected]>
seL4/seL4#896 changes IOAPIC-related decoding slightly and requires a few new small invariants on the Haskell level.
Test with: seL4/seL4#896