Update ARM Access for det_ext changes #840
Conversation
|
|
|
|
||
| lemma thread_set_time_slice_pas_refined[wp]: | ||
| "thread_set_time_slice tptr time \<lbrace>pas_refined aag\<rbrace>" | ||
| by (simp add: thread_set_time_slice_def | wp)+ | ||
| "\<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state\<rbrace> |
There was a problem hiding this comment.
This precondition (and those of several similar lemmas) could be weakened using the changes from 357ccc9. I'll do so once that commit is either in master or is able to be cherry-picked into this branch.
There was a problem hiding this comment.
does this also apply to lemma pas_refined?
corlewis
force-pushed
the
det_ext_state_arm
branch
from
9788c54 to
6f4d440
Compare
|
Is the plan to rebase this over #844? |
I think it already is. This PR has 3 commits, but only one is new, and the second one is the same as in 844 (currently) |
| apply (clarsimp simp: etcbs_of'_def split: if_split_asm kernel_object.splits) | ||
| apply (clarsimp simp: default_object_def default_tcb_def tyunt split: apiobject_type.splits) | ||
| defer | ||
| apply (force intro: domtcbs) |
There was a problem hiding this comment.
is this copied from elsewhere? post-defer indent is wrong, and probably there's no need to split obj and aobj separately anyway, and on top of that force can probably finish it after the erule, or maybe even do the whole lemma if we're lucky
Signed-off-by: Corey Lewis <[email protected]>
corlewis
force-pushed
the
det_ext_state_arm
branch
from
6f4d440 to
b4bd341
Compare
corlewis
changed the title
Following on from #824 and #844, this PR additionally updates the Access Control proofs for the changes to det_ext and the scheduler state.