Update ARM Access for det_ext changes #840
Conversation
|
|
proof/access-control/Syscall_AC.thy
Outdated
|
|
||
| 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?
There was a problem hiding this comment.
There was a problem hiding this comment.
does this also apply to
lemma pas_refined?
If I'm looking at the right lemma then no. This was specifically for preconditions where I'd had to add pspace_aligned and valid_vspace_objs and valid_arch_state
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) |
proof/access-control/Retype_AC.thy
Outdated
| 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
There was a problem hiding this comment.
I have to admit that I don't remember but it doesn't look like my style so I assume that I copied it from somewhere.
It's actually even weirder than you thought, the post-defer indent is correct, because the defer is done when there is only one subgoal. I've changed it like you suggested and moved everything into the force.
corlewis
force-pushed
the
det_ext_state_arm
branch
from
6f4d440 to
b4bd341
Compare
corlewis
changed the title
-Remove various instances of pspace_aligned, valid_vspace_objs, and valid_asid_table/valid_arch_state from preconditions -Relax the is_subject predicate in various Syscall_AC lemmas Signed-off-by: Ryan Barry <ryan.barry@proofcraft.systems>
Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>
Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>
Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>
corlewis
force-pushed
the
det_ext_state_arm
branch
from
d4dbc96 to
e3797a8
Compare
| @@ -138,6 +143,7 @@ abbreviation integrity_asids_aux :: | |||
| pp_opt = pp_opt' \<or> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of asid | |||
| \<longrightarrow> pasASIDAbs aag asid' \<in> subjects)" | |||
|
|
|||
| \<comment> \<open>FIXME: could we define integrity_asids to operate on arch_state only?\<close> | |||
There was a problem hiding this comment.
Unfortunately not, we use asid_pools_of in RISCV64
| @@ -33,12 +33,25 @@ end | |||
|
|
|||
| context retype_region_proofs' begin interpretation Arch . | |||
|
|
|||
| \<comment> \<open>FIXME: move to pas_refined_state_objs_to_policy_subset?\<close> | |||
There was a problem hiding this comment.
If the proof impact is minimal, that would be ideal. Curious what case you ran into where the subset relation was too strong.
Following on from #824 and #844, this PR additionally updates the Access Control proofs for the changes to det_ext and the scheduler state.