Update proofs for AArch64 seL4 PR #663
Conversation
lsf37
added
seL4-PR
| @@ -2332,6 +2332,9 @@ definition | |||
| | ARM_HYP_H.PageDirectoryObject \<Rightarrow> scast seL4_ARM_PageDirectoryObject | |||
| | ARM_HYP_H.VCPUObject \<Rightarrow> scast seL4_ARM_VCPUObject" | |||
|
|
|||
| (* always unfold StrictC'_mode_object_defs together with api_object_defs *) | |||
| lemmas api_object_defs = api_object_defs StrictC'_mode_object_defs | |||
There was a problem hiding this comment.
I'm not 100% on whether having this kind of def override so far into CRefine is a risky approach. Should be ok here, but made me stop and think.
There was a problem hiding this comment.
In this case I think it's fine for ARM/ARM_HYP, because it recreates the old situation before it matters the first time. But generally I agree, it's a bit risky.
There was a problem hiding this comment.
The changes themselves look fine to me but I'm a bit confused. Isn't the C change generally getting rid of the PageDirectoryObj and using PageTableObj instead?
Otherwise, a very minor comment is that I think the more standard commit tag would be arm abstract+design instead of arm abstract/design.
It doesn't actually get rid of
👍 |
AArch64 C code changes now designate PageDirectoryObj as the VSpace object type, which comes first in the enum. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Update proofs for the changes in seL4/seL4#801, in particular commit seL4/seL4@b3cc852