refine: speed up CSpace1_R+CSpace_R proofs
Three main thrusts:
- speed up the `updateMDB_the_lot` chain by using more targeted
proof methods
- drastically reduce goal size by removing unused assumptions when
that becomes possible (this is the largest overall speed win)
- use `subgoal` to unblock interactive proof progress
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
Gerwin Klein
Gerwin Klein
parent
0aaeb868ce
commit
954b42cdd9
|
|
@ -6565,13 +6565,22 @@ lemma cteSwap_corres:
|
|||
| rule refl | clarsimp simp: put_def simp del: fun_upd_apply )+
|
||||
apply (simp cong: option.case_cong)
|
||||
apply (drule updateCap_stuff, elim conjE, erule(1) impE)
|
||||
apply (drule (2) updateMDB_the_lot', fastforce, fastforce, simp, clarsimp)
|
||||
apply (drule (2) updateMDB_the_lot', fastforce, fastforce, simp, clarsimp)
|
||||
apply (drule in_getCTE, clarsimp)
|
||||
apply (drule (2) updateMDB_the_lot', fastforce, fastforce, simp, clarsimp)
|
||||
apply (drule (2) updateMDB_the_lot', fastforce, fastforce, simp, clarsimp)
|
||||
apply (drule (2) updateMDB_the_lot', fastforce, fastforce, simp, clarsimp)
|
||||
apply (drule (2) updateMDB_the_lot', fastforce, fastforce, simp, clarsimp)
|
||||
apply (drule (2) updateMDB_the_lot')
|
||||
apply (erule (1) impE, assumption)
|
||||
apply (fastforce simp only: no_0_modify_map)
|
||||
apply assumption
|
||||
apply (elim conjE TrueE, simp only:)
|
||||
apply (drule (2) updateMDB_the_lot', fastforce, simp only: no_0_modify_map, assumption)
|
||||
apply (drule in_getCTE, elim conjE, simp only:)
|
||||
apply (drule (2) updateMDB_the_lot', fastforce, simp only: no_0_modify_map, assumption)
|
||||
apply (elim conjE TrueE, simp only:)
|
||||
apply (drule (2) updateMDB_the_lot', fastforce, simp only: no_0_modify_map, assumption)
|
||||
apply (elim conjE TrueE, simp only:)
|
||||
apply (drule (2) updateMDB_the_lot', fastforce, simp only: no_0_modify_map, assumption)
|
||||
apply (elim conjE TrueE, simp only:)
|
||||
apply (drule (2) updateMDB_the_lot', fastforce, simp only: no_0_modify_map, assumption)
|
||||
apply (simp only: pspace_relations_def refl)
|
||||
apply (rule conjI, rule TrueI)+
|
||||
apply (thin_tac "ksMachineState t = p" for t p)+
|
||||
apply (thin_tac "ksCurThread t = p" for t p)+
|
||||
apply (thin_tac "ksReadyQueues t = p" for t p)+
|
||||
|
|
@ -6582,7 +6591,8 @@ lemma cteSwap_corres:
|
|||
apply (thin_tac "ksDomSchedule t = p" for t p)+
|
||||
apply (thin_tac "ksCurDomain t = p" for t p)+
|
||||
apply (thin_tac "ksDomainTime t = p" for t p)+
|
||||
apply (clarsimp simp: cte_wp_at_ctes_of in_set_cap_cte_at_swp cong: if_cong)
|
||||
apply (simp only: simp_thms no_0_modify_map)
|
||||
apply (clarsimp simp: cte_wp_at_ctes_of cong: if_cong)
|
||||
apply (thin_tac "ctes_of x = y" for x y)+
|
||||
apply (case_tac cte1)
|
||||
apply (rename_tac src_cap src_node)
|
||||
|
|
@ -6603,24 +6613,49 @@ lemma cteSwap_corres:
|
|||
apply (erule weak_derived_sym')
|
||||
apply (erule weak_derived_sym')
|
||||
apply assumption
|
||||
apply (clarsimp simp: pspace_relations_def)
|
||||
apply (rule conjI)
|
||||
apply (clarsimp simp: ghost_relation_typ_at set_cap_a_type_inv ARM.data_at_def)
|
||||
subgoal by (simp only: simp_thms ghost_relation_typ_at set_cap_a_type_inv ARM.data_at_def)
|
||||
apply (thin_tac "ksMachineState t = p" for t p)+
|
||||
apply (thin_tac "ksCurThread t = p" for t p)+
|
||||
apply (thin_tac "ksReadyQueues t = p" for t p)+
|
||||
apply (thin_tac "ksSchedulerAction t = p" for t p)+
|
||||
apply (thin_tac "ready_queues t = p" for t p)+
|
||||
apply (thin_tac "cur_domain t = p" for t p)+
|
||||
apply (thin_tac "ksDomScheduleIdx t = p" for t p)+
|
||||
apply (thin_tac "ksDomSchedule t = p" for t p)+
|
||||
apply (thin_tac "ksCurDomain t = p" for t p)+
|
||||
apply (thin_tac "ksDomainTime t = p" for t p)+
|
||||
apply (thin_tac "idle_thread t = p" for t p)+
|
||||
apply (thin_tac "work_units_completed t = p" for t p)+
|
||||
apply (thin_tac "domain_index t = p" for t p)+
|
||||
apply (thin_tac "domain_list t = p" for t p)+
|
||||
apply (thin_tac "domain_time t = p" for t p)+
|
||||
apply (thin_tac "ekheap t = p" for t p)+
|
||||
apply (thin_tac "scheduler_action t = p" for t p)+
|
||||
apply (thin_tac "ksArchState t = p" for t p)+
|
||||
apply (thin_tac "gsCNodes t = p" for t p)+
|
||||
apply (thin_tac "ksWorkUnitsCompleted t = p" for t p)+
|
||||
apply (thin_tac "ksInterruptState t = p" for t p)+
|
||||
apply (thin_tac "ksIdleThread t = p" for t p)+
|
||||
apply (thin_tac "gsUserPages t = p" for t p)+
|
||||
apply (thin_tac "pspace_relation s s'" for s s')+
|
||||
apply (thin_tac "ekheap_relation e p" for e p)+
|
||||
apply (thin_tac "interrupt_state_relation n s s'" for n s s')+
|
||||
apply (thin_tac "(s,s') \<in> arch_state_relation" for s s')+
|
||||
apply(subst conj_assoc[symmetric])
|
||||
apply (rule conjI)
|
||||
prefer 2
|
||||
apply (clarsimp simp add: revokable_relation_def in_set_cap_cte_at
|
||||
simp del: split_paired_All)
|
||||
apply (drule set_cap_caps_of_state_monad)+
|
||||
apply (thin_tac "pspace_relation s t" for s t)+
|
||||
apply (simp del: split_paired_All split: if_split)
|
||||
apply (rule conjI)
|
||||
apply (clarsimp simp: cte_wp_at_caps_of_state simp del: split_paired_All)
|
||||
apply (drule(1) mdb_swap.revokable)
|
||||
apply (erule_tac x="dest" in allE)
|
||||
apply (erule impE)
|
||||
apply (clarsimp simp: null_filter_def weak_derived_Null split: if_splits)
|
||||
apply simp
|
||||
subgoal by (clarsimp simp: null_filter_def weak_derived_Null split: if_splits)
|
||||
subgoal by simp
|
||||
apply (clarsimp simp del: split_paired_All)
|
||||
apply (rule conjI)
|
||||
apply (clarsimp simp: cte_wp_at_caps_of_state simp del: split_paired_All)
|
||||
|
|
@ -6629,19 +6664,19 @@ lemma cteSwap_corres:
|
|||
apply (simp del: split_paired_All)
|
||||
apply (erule_tac x="src" in allE)
|
||||
apply (erule impE)
|
||||
apply (clarsimp simp: null_filter_def weak_derived_Null split: if_splits)
|
||||
apply simp
|
||||
subgoal by (clarsimp simp: null_filter_def weak_derived_Null split: if_splits)
|
||||
subgoal by simp
|
||||
apply (drule caps_of_state_cte_at)+
|
||||
apply (erule (5) cte_map_inj)
|
||||
apply (clarsimp simp: cte_wp_at_caps_of_state simp del: split_paired_All)
|
||||
apply (drule (1) mdb_swap.revokable)
|
||||
apply (subgoal_tac "null_filter (caps_of_state a) (aa,bb) \<noteq> None")
|
||||
prefer 2
|
||||
apply (clarsimp simp: null_filter_def split: if_splits)
|
||||
subgoal by (clarsimp simp: null_filter_def split: if_splits)
|
||||
apply clarsimp
|
||||
apply (subgoal_tac "cte_map (aa,bb) \<noteq> cte_map src")
|
||||
apply (subgoal_tac "cte_map (aa,bb) \<noteq> cte_map dest")
|
||||
apply (clarsimp simp del: split_paired_All)
|
||||
subgoal by (clarsimp simp del: split_paired_All)
|
||||
apply (drule caps_of_state_cte_at)+
|
||||
apply (drule null_filter_caps_of_stateD)+
|
||||
apply (erule cte_map_inj, erule cte_wp_cte_at, assumption+)
|
||||
|
|
@ -6650,7 +6685,7 @@ lemma cteSwap_corres:
|
|||
apply (erule cte_map_inj, erule cte_wp_cte_at, assumption+)
|
||||
apply (subgoal_tac "no_loops (ctes_of b)")
|
||||
prefer 2
|
||||
apply (simp add: valid_mdb_ctes_def mdb_chain_0_no_loops)
|
||||
subgoal by (simp add: valid_mdb_ctes_def mdb_chain_0_no_loops)
|
||||
apply (subgoal_tac "mdb_swap_abs (cdt a) src dest a")
|
||||
prefer 2
|
||||
apply (erule mdb_swap_abs.intro)
|
||||
|
|
@ -6660,7 +6695,7 @@ lemma cteSwap_corres:
|
|||
apply assumption
|
||||
apply (frule mdb_swap_abs''.intro)
|
||||
apply (drule_tac t="cdt_list (a)" in mdb_swap_abs'.intro)
|
||||
apply (simp add: mdb_swap_abs'_axioms_def)
|
||||
subgoal by (simp add: mdb_swap_abs'_axioms_def)
|
||||
apply (thin_tac "modify_map m f p p' = t" for m f p p' t)
|
||||
apply(rule conjI)
|
||||
apply (simp add: cdt_relation_def del: split_paired_All)
|
||||
|
|
@ -6712,7 +6747,7 @@ lemma cteSwap_corres:
|
|||
apply (erule (3) inj_on_descendants_cte_map)
|
||||
apply (rule subset_refl)
|
||||
apply clarsimp
|
||||
apply auto[1]
|
||||
subgoal by auto
|
||||
apply clarsimp
|
||||
apply (rule conjI, clarsimp)
|
||||
apply (rule conjI, clarsimp)
|
||||
|
|
@ -6891,9 +6926,7 @@ lemma cteSwap_corres:
|
|||
apply(rule cte_at_next_slot')
|
||||
apply(simp_all)[9]
|
||||
apply(erule cte_wp_at_weakenE, simp)
|
||||
apply(rule cte_at_next_slot)
|
||||
apply(simp_all)
|
||||
done
|
||||
by (rule cte_at_next_slot; simp)
|
||||
|
||||
|
||||
lemma capSwapForDelete_corres:
|
||||
|
|
|
|||
|
|
@ -101,7 +101,7 @@ lemma src_no_parent [iff]:
|
|||
lemma no_0_n: "no_0 n" by (simp add: n_def no_0)
|
||||
lemma no_0': "no_0 m'" by (simp add: m'_def no_0_n)
|
||||
|
||||
lemma next_neq_dest [simp]:
|
||||
lemma next_neq_dest [iff]:
|
||||
"mdbNext src_node \<noteq> dest"
|
||||
using dlist src dest prev dest_0 no_0
|
||||
by (fastforce simp add: valid_dlist_def no_0_def Let_def)
|
||||
|
|
@ -201,26 +201,10 @@ proof -
|
|||
thus ?thesis by (simp add: m'_def)
|
||||
qed
|
||||
|
||||
lemma [iff]:
|
||||
lemma dest_not_parent [iff]:
|
||||
"m \<turnstile> dest parentOf c = False"
|
||||
using dest by (simp add: parentOf_def)
|
||||
|
||||
lemma [iff]:
|
||||
"mdbNext src_node \<noteq> dest"
|
||||
proof
|
||||
assume "mdbNext src_node = dest"
|
||||
moreover have "dest \<noteq> 0" ..
|
||||
ultimately
|
||||
have "mdbPrev old_dest_node = src"
|
||||
using src dest dlist
|
||||
by (fastforce elim: valid_dlistEn)
|
||||
with prev
|
||||
show False by (simp add: src_0)
|
||||
qed
|
||||
|
||||
lemmas no_loops_simps [simp] =
|
||||
no_loops_direct_simp [OF no_loops] no_loops_trancl_simp [OF no_loops]
|
||||
|
||||
lemma dest_source [iff]:
|
||||
"(m \<turnstile> dest \<leadsto> x) = (x = 0)"
|
||||
using dest nxt by (simp add: next_unfold')
|
||||
|
|
@ -883,10 +867,12 @@ lemma cteMove_corres:
|
|||
apply (drule (4) updateMDB_the_lot, elim conjE)
|
||||
apply (drule (4) updateMDB_the_lot, elim conjE)
|
||||
apply (drule updateCap_stuff, elim conjE, erule (1) impE)
|
||||
apply (drule updateCap_stuff, clarsimp)
|
||||
apply (drule updateCap_stuff)
|
||||
apply (subgoal_tac "pspace_distinct' b \<and> pspace_aligned' b")
|
||||
prefer 2
|
||||
subgoal by fastforce
|
||||
apply (elim valid_pspaceE' conjE)
|
||||
apply (rule conjI; assumption)
|
||||
apply (simp only: )
|
||||
apply (thin_tac "ctes_of t = s" for t s)+
|
||||
apply (thin_tac "ksMachineState t = p" for t p)+
|
||||
apply (thin_tac "ksCurThread t = p" for t p)+
|
||||
|
|
@ -895,7 +881,7 @@ lemma cteMove_corres:
|
|||
apply (thin_tac "ksSchedulerAction t = p" for t p)+
|
||||
apply (subgoal_tac "\<forall>p. cte_at p ta = cte_at p a")
|
||||
prefer 2
|
||||
apply (simp add: set_cap_cte_eq)
|
||||
subgoal by (simp add: set_cap_cte_eq)
|
||||
apply (clarsimp simp add: swp_def cte_wp_at_ctes_of simp del: split_paired_All)
|
||||
apply (subgoal_tac "cte_at ptr' a")
|
||||
prefer 2
|
||||
|
|
@ -909,6 +895,36 @@ lemma cteMove_corres:
|
|||
apply (clarsimp simp: pspace_relations_def)
|
||||
apply (rule conjI)
|
||||
apply (clarsimp simp: ghost_relation_typ_at set_cap_a_type_inv data_at_def)
|
||||
apply (thin_tac "gsCNodes t = p" for t p)+
|
||||
apply (thin_tac "ksMachineState t = p" for t p)+
|
||||
apply (thin_tac "ksCurThread t = p" for t p)+
|
||||
apply (thin_tac "ksWorkUnitsCompleted t = p" for t p)+
|
||||
apply (thin_tac "ksIdleThread t = p" for t p)+
|
||||
apply (thin_tac "ksReadyQueues t = p" for t p)+
|
||||
apply (thin_tac "ksSchedulerAction t = p" for t p)+
|
||||
apply (thin_tac "cur_thread t = p" for t p)+
|
||||
apply (thin_tac "domain_index t = p" for t p)+
|
||||
apply (thin_tac "domain_time t = p" for t p)+
|
||||
apply (thin_tac "cur_domain t = p" for t p)+
|
||||
apply (thin_tac "scheduler_action t = p" for t p)+
|
||||
apply (thin_tac "ready_queues t = p" for t p)+
|
||||
apply (thin_tac "idle_thread t = p" for t p)+
|
||||
apply (thin_tac "machine_state t = p" for t p)+
|
||||
apply (thin_tac "work_units_completed t = p" for t p)+
|
||||
apply (thin_tac "ksArchState t = p" for t p)+
|
||||
apply (thin_tac "gsUserPages t = p" for t p)+
|
||||
apply (thin_tac "ksCurDomain t = p" for t p)+
|
||||
apply (thin_tac "ksInterruptState t = p" for t p)+
|
||||
apply (thin_tac "ksDomScheduleIdx t = p" for t p)+
|
||||
apply (thin_tac "ksDomainTime t = p" for t p)+
|
||||
apply (thin_tac "ksDomSchedule t = p" for t p)+
|
||||
apply (thin_tac "ctes_of t = p" for t p)+
|
||||
apply (thin_tac "ekheap_relation t p" for t p)+
|
||||
apply (thin_tac "pspace_relation t p" for t p)+
|
||||
apply (thin_tac "interrupt_state_relation s t p" for s t p)+
|
||||
apply (thin_tac "ghost_relation s t p" for s t p)+
|
||||
apply (thin_tac "sched_act_relation t p" for t p)+
|
||||
apply (thin_tac "ready_queues_relation t p" for t p)+
|
||||
apply (subst conj_assoc[symmetric])
|
||||
apply (rule conjI)
|
||||
defer
|
||||
|
|
@ -986,7 +1002,7 @@ lemma cteMove_corres:
|
|||
apply (subgoal_tac "descendants_of' (cte_map (aa, bb)) (ctes_of b) =
|
||||
cte_map ` descendants_of (aa, bb) (cdt a)")
|
||||
prefer 2
|
||||
apply (simp add: cdt_relation_def del: split_paired_All)
|
||||
subgoal by (simp add: cdt_relation_def del: split_paired_All)
|
||||
apply simp
|
||||
apply (rule conjI)
|
||||
apply clarsimp
|
||||
|
|
@ -997,8 +1013,8 @@ lemma cteMove_corres:
|
|||
apply fastforce
|
||||
apply fastforce
|
||||
apply (rule subset_refl)
|
||||
apply simp
|
||||
apply simp
|
||||
subgoal by simp
|
||||
subgoal by simp
|
||||
apply clarsimp
|
||||
apply (drule (1) cte_map_inj_eq)
|
||||
apply (erule descendants_of_cte_at)
|
||||
|
|
@ -1017,7 +1033,7 @@ lemma cteMove_corres:
|
|||
apply(intro allI impI)
|
||||
apply(rule mdb_move_abs'.next_slot)
|
||||
apply(simp, fastforce, simp)
|
||||
apply(fastforce split: option.splits)
|
||||
subgoal by(fastforce split: option.splits)
|
||||
apply(case_tac "ctes_of b (cte_map (aa, bb))")
|
||||
subgoal by (clarsimp simp: modify_map_def split: if_split_asm)
|
||||
apply(case_tac ab)
|
||||
|
|
@ -4755,12 +4771,41 @@ lemma cteInsert_simple_corres:
|
|||
apply (clarsimp simp: put_def state_relation_def simp del: fun_upd_apply)
|
||||
apply (drule updateCap_stuff)
|
||||
apply clarsimp
|
||||
apply (drule (3) updateMDB_the_lot', simp, simp, elim conjE)
|
||||
apply (drule (3) updateMDB_the_lot', simp, simp, elim conjE)
|
||||
apply (drule (3) updateMDB_the_lot', simp, simp, elim conjE)
|
||||
apply (drule (3) updateMDB_the_lot', simp only: no_0_modify_map, simp only:, elim conjE)
|
||||
apply (drule (3) updateMDB_the_lot', simp only: no_0_modify_map, simp only:, elim conjE)
|
||||
apply (drule (3) updateMDB_the_lot', simp only: no_0_modify_map, simp only:, elim conjE)
|
||||
apply (clarsimp simp: pspace_relations_def)
|
||||
apply (thin_tac "gsCNodes t = p" for t p)+
|
||||
apply (thin_tac "ksMachineState t = p" for t p)+
|
||||
apply (thin_tac "ksCurThread t = p" for t p)+
|
||||
apply (thin_tac "ksWorkUnitsCompleted t = p" for t p)+
|
||||
apply (thin_tac "ksIdleThread t = p" for t p)+
|
||||
apply (thin_tac "ksReadyQueues t = p" for t p)+
|
||||
apply (thin_tac "ksSchedulerAction t = p" for t p)+
|
||||
apply (thin_tac "cur_thread t = p" for t p)+
|
||||
apply (thin_tac "domain_index t = p" for t p)+
|
||||
apply (thin_tac "domain_time t = p" for t p)+
|
||||
apply (thin_tac "cur_domain t = p" for t p)+
|
||||
apply (thin_tac "scheduler_action t = p" for t p)+
|
||||
apply (thin_tac "ready_queues t = p" for t p)+
|
||||
apply (thin_tac "idle_thread t = p" for t p)+
|
||||
apply (thin_tac "machine_state t = p" for t p)+
|
||||
apply (thin_tac "work_units_completed t = p" for t p)+
|
||||
apply (thin_tac "ksArchState t = p" for t p)+
|
||||
apply (thin_tac "gsUserPages t = p" for t p)+
|
||||
apply (thin_tac "ksCurDomain t = p" for t p)+
|
||||
apply (thin_tac "ksInterruptState t = p" for t p)+
|
||||
apply (thin_tac "ksDomScheduleIdx t = p" for t p)+
|
||||
apply (thin_tac "ksDomainTime t = p" for t p)+
|
||||
apply (thin_tac "ksDomSchedule t = p" for t p)+
|
||||
apply (thin_tac "ctes_of t = p" for t p)+
|
||||
apply (thin_tac "ekheap_relation t p" for t p)+
|
||||
apply (thin_tac "pspace_relation t p" for t p)+
|
||||
apply (thin_tac "interrupt_state_relation s t p" for s t p)+
|
||||
apply (thin_tac "sched_act_relation t p" for t p)+
|
||||
apply (thin_tac "ready_queues_relation t p" for t p)+
|
||||
apply (rule conjI)
|
||||
apply (clarsimp simp: ghost_relation_typ_at set_cap_a_type_inv data_at_def)
|
||||
subgoal by (clarsimp simp: ghost_relation_typ_at set_cap_a_type_inv data_at_def)
|
||||
apply (clarsimp simp: cte_wp_at_ctes_of nullPointer_def prev_update_modify_mdb_relation)
|
||||
apply (subgoal_tac "cte_map dest \<noteq> 0")
|
||||
prefer 2
|
||||
|
|
@ -4770,11 +4815,6 @@ lemma cteInsert_simple_corres:
|
|||
prefer 2
|
||||
apply (clarsimp simp: valid_mdb'_def
|
||||
valid_mdb_ctes_def no_0_def)
|
||||
apply (thin_tac "ksMachineState t = p" for t p)+
|
||||
apply (thin_tac "ksCurThread t = p" for t p)+
|
||||
apply (thin_tac "ksIdleThread t = p" for t p)+
|
||||
apply (thin_tac "ksReadyQueues t = p" for t p)+
|
||||
apply (thin_tac "ksSchedulerAction t = p" for t p)+
|
||||
apply (subgoal_tac "should_be_parent_of src_cap (is_original_cap a src) c (revokable src_cap c) = True")
|
||||
prefer 2
|
||||
apply (subst should_be_parent_of_masked_as_full[symmetric])
|
||||
|
|
@ -4783,7 +4823,6 @@ lemma cteInsert_simple_corres:
|
|||
apply (subst conj_assoc[symmetric])
|
||||
apply (rule conjI)
|
||||
defer
|
||||
apply (thin_tac "ctes_of t = t'" for t t')+
|
||||
apply (clarsimp simp: modify_map_apply)
|
||||
apply (clarsimp simp: revokable_relation_def simp del: fun_upd_apply)
|
||||
apply (simp split: if_split)
|
||||
|
|
@ -4798,7 +4837,7 @@ lemma cteInsert_simple_corres:
|
|||
apply (subst same_region_as_relation [symmetric])
|
||||
prefer 3
|
||||
apply (rule safe_parent_same_region)
|
||||
apply (simp add: cte_wp_at_caps_of_state safe_parent_for_masked_as_full)
|
||||
apply (simp add: cte_wp_at_caps_of_state)
|
||||
apply assumption
|
||||
apply assumption
|
||||
apply (clarsimp simp: cte_wp_at_def is_simple_cap_def)
|
||||
|
|
@ -4835,9 +4874,6 @@ lemma cteInsert_simple_corres:
|
|||
apply clarsimp
|
||||
subgoal by (fastforce elim: cte_wp_at_weakenE)
|
||||
subgoal by (clarsimp simp: cte_wp_at'_def)
|
||||
apply (thin_tac "ctes_of s = t" for s t)+
|
||||
apply (thin_tac "pspace_relation s t" for s t)+
|
||||
apply (thin_tac "machine_state t = s" for t s)+
|
||||
apply (case_tac "srcCTE")
|
||||
apply (rename_tac src_cap' src_node)
|
||||
apply (case_tac "rv'")
|
||||
|
|
@ -4845,7 +4881,7 @@ lemma cteInsert_simple_corres:
|
|||
apply (clarsimp simp: in_set_cap_cte_at_swp)
|
||||
apply (subgoal_tac "cte_at src a \<and> safe_parent_for (cdt a) src c src_cap")
|
||||
prefer 2
|
||||
subgoal by (fastforce simp: cte_wp_at_def safe_parent_for_masked_as_full)
|
||||
subgoal by (fastforce simp: cte_wp_at_def)
|
||||
apply (erule conjE)
|
||||
|
||||
apply (subgoal_tac "mdb_insert (ctes_of b) (cte_map src) (maskedAsFull src_cap' c') src_node
|
||||
|
|
|
|||
|
|
@ -2460,15 +2460,15 @@ lemma updateCap_corres:
|
|||
apply (unfold cdt_list_relation_def)[1]
|
||||
apply (intro allI impI)
|
||||
apply (erule_tac x=c in allE)
|
||||
apply (auto elim!: modify_map_casesE)[1]
|
||||
subgoal by (auto elim!: modify_map_casesE)[1]
|
||||
apply (unfold revokable_relation_def)[1]
|
||||
apply (drule set_cap_caps_of_state_monad)
|
||||
apply (simp add: cte_wp_at_caps_of_state del: split_paired_All)
|
||||
apply (intro allI impI)
|
||||
apply (erule_tac x=c in allE)
|
||||
apply (erule impE[where P="\<exists>y. v = Some y" for v])
|
||||
apply (clarsimp simp: null_filter_def is_zombie_def split: if_split_asm)
|
||||
apply (auto elim!: modify_map_casesE del: disjE)[1]
|
||||
subgoal by (clarsimp simp: null_filter_def is_zombie_def split: if_split_asm)
|
||||
subgoal by (auto elim!: modify_map_casesE del: disjE)[1]
|
||||
apply (case_tac "ctes_of b (cte_map slot)")
|
||||
apply (simp add: modify_map_None)
|
||||
apply (simp add: modify_map_apply)
|
||||
|
|
@ -2477,7 +2477,7 @@ lemma updateCap_corres:
|
|||
apply (rule use_update_ztc_one [OF descendants_of_update_ztc])
|
||||
apply simp
|
||||
apply assumption
|
||||
apply (auto simp: is_cap_simps isCap_simps)[1]
|
||||
subgoal by (auto simp: is_cap_simps isCap_simps)[1]
|
||||
apply (frule(3) is_final_untyped_ptrs [OF _ _ not_sym], clarsimp+)
|
||||
apply (clarsimp simp: cte_wp_at_caps_of_state)
|
||||
apply (simp add: is_cap_simps, elim disjE exE, simp_all)[1]
|
||||
|
|
@ -2862,9 +2862,8 @@ lemma capBadge_ordering_relation:
|
|||
"\<lbrakk> cap_relation c c'; cap_relation d d' \<rbrakk> \<Longrightarrow>
|
||||
((capBadge c', capBadge d') \<in> capBadge_ordering f) =
|
||||
((cap_badge c, cap_badge d) \<in> capBadge_ordering f)"
|
||||
apply (cases c)
|
||||
apply (auto simp add: cap_badge_def capBadge_ordering_def split: cap.splits)
|
||||
done
|
||||
by (cases c)
|
||||
(auto simp add: cap_badge_def capBadge_ordering_def split: cap.splits)
|
||||
|
||||
lemma is_reply_cap_relation:
|
||||
"cap_relation c c' \<Longrightarrow> is_reply_cap c = (isReplyCap c' \<and> \<not> capReplyMaster c')"
|
||||
|
|
@ -5238,34 +5237,52 @@ lemma cteInsert_corres:
|
|||
apply (clarsimp simp: put_def state_relation_def)
|
||||
apply (drule updateCap_stuff)
|
||||
apply clarsimp
|
||||
apply (drule (3) updateMDB_the_lot', simp, simp, elim conjE)
|
||||
apply (drule (3) updateMDB_the_lot', simp, simp, elim conjE)
|
||||
apply (drule (3) updateMDB_the_lot', simp, simp, elim conjE)
|
||||
apply (drule (3) updateMDB_the_lot', simp only: no_0_modify_map, simp only:, elim conjE)
|
||||
apply (drule (3) updateMDB_the_lot', simp only: no_0_modify_map, simp only:, elim conjE)
|
||||
apply (drule (3) updateMDB_the_lot', simp only: no_0_modify_map, simp only:, elim conjE)
|
||||
apply (clarsimp simp: cte_wp_at_ctes_of nullPointer_def
|
||||
prev_update_modify_mdb_relation)
|
||||
apply (subgoal_tac "cte_map dest \<noteq> 0")
|
||||
prefer 2
|
||||
apply (clarsimp simp: valid_mdb'_def
|
||||
valid_mdb_ctes_def no_0_def)
|
||||
subgoal by (clarsimp simp: valid_mdb'_def valid_mdb_ctes_def no_0_def)
|
||||
apply (subgoal_tac "cte_map src \<noteq> 0")
|
||||
prefer 2
|
||||
apply (clarsimp simp: valid_mdb'_def
|
||||
valid_mdb_ctes_def no_0_def)
|
||||
subgoal by (clarsimp simp: valid_mdb'_def valid_mdb_ctes_def no_0_def)
|
||||
apply (thin_tac "ksMachineState t = p" for p t)+
|
||||
apply (thin_tac "ksCurThread t = p" for p t)+
|
||||
apply (thin_tac "ksIdleThread t = p" for p t)+
|
||||
apply (thin_tac "ksReadyQueues t = p" for p t)+
|
||||
apply (thin_tac "ksSchedulerAction t = p" for p t)+
|
||||
apply (clarsimp simp: pspace_relations_def)
|
||||
|
||||
apply (rule conjI)
|
||||
apply (clarsimp simp: ghost_relation_typ_at set_cap_a_type_inv data_at_def)
|
||||
subgoal by (clarsimp simp: ghost_relation_typ_at set_cap_a_type_inv data_at_def)
|
||||
apply (thin_tac "gsCNodes t = p" for t p)+
|
||||
apply (thin_tac "ksWorkUnitsCompleted t = p" for t p)+
|
||||
apply (thin_tac "cur_thread t = p" for t p)+
|
||||
apply (thin_tac "domain_index t = p" for t p)+
|
||||
apply (thin_tac "domain_time t = p" for t p)+
|
||||
apply (thin_tac "cur_domain t = p" for t p)+
|
||||
apply (thin_tac "scheduler_action t = p" for t p)+
|
||||
apply (thin_tac "ready_queues t = p" for t p)+
|
||||
apply (thin_tac "idle_thread t = p" for t p)+
|
||||
apply (thin_tac "machine_state t = p" for t p)+
|
||||
apply (thin_tac "work_units_completed t = p" for t p)+
|
||||
apply (thin_tac "ksArchState t = p" for t p)+
|
||||
apply (thin_tac "gsUserPages t = p" for t p)+
|
||||
apply (thin_tac "ksCurDomain t = p" for t p)+
|
||||
apply (thin_tac "ksInterruptState t = p" for t p)+
|
||||
apply (thin_tac "ksDomScheduleIdx t = p" for t p)+
|
||||
apply (thin_tac "ksDomainTime t = p" for t p)+
|
||||
apply (thin_tac "ksDomSchedule t = p" for t p)+
|
||||
apply (thin_tac "ctes_of t = p" for t p)+
|
||||
apply (thin_tac "ekheap_relation t p" for t p)+
|
||||
apply (thin_tac "pspace_relation t p" for t p)+
|
||||
apply (thin_tac "interrupt_state_relation s t p" for s t p)+
|
||||
apply (thin_tac "sched_act_relation t p" for t p)+
|
||||
apply (thin_tac "ready_queues_relation t p" for t p)+
|
||||
apply (rule conjI)
|
||||
defer
|
||||
apply(rule conjI)
|
||||
apply (thin_tac "ctes_of s = t" for s t)+
|
||||
apply (thin_tac "pspace_relation s t" for s t)+
|
||||
apply (thin_tac "machine_state t = s" for s t)+
|
||||
apply (case_tac "srcCTE")
|
||||
apply (rename_tac src_cap' src_node)
|
||||
apply (case_tac "rv'")
|
||||
|
|
@ -5550,7 +5567,6 @@ lemma cteInsert_corres:
|
|||
apply(simp_all)[2]
|
||||
apply(erule_tac x="(aa, bb)" in allE)+
|
||||
subgoal by(fastforce)
|
||||
apply (thin_tac "ctes_of t = t'" for t t')+
|
||||
apply (clarsimp simp: modify_map_apply)
|
||||
apply (clarsimp simp: revokable_relation_def split: if_split)
|
||||
apply (rule conjI)
|
||||
|
|
@ -5605,9 +5621,6 @@ lemma cteInsert_corres:
|
|||
apply clarsimp
|
||||
subgoal by (fastforce elim: cte_wp_at_weakenE)
|
||||
apply (clarsimp simp: cte_wp_at'_def)
|
||||
apply (thin_tac "ctes_of s = t" for s t)+
|
||||
apply (thin_tac "pspace_relation s t" for s t)+
|
||||
apply (thin_tac "machine_state t = s" for s t)+
|
||||
apply (case_tac "srcCTE")
|
||||
apply (rename_tac src_cap' src_node)
|
||||
apply (case_tac "rv'")
|
||||
|
|
@ -5641,7 +5654,7 @@ lemma cteInsert_corres:
|
|||
apply (subgoal_tac "descendants_of dest (cdt a) = {}")
|
||||
prefer 2
|
||||
apply (drule mdb_insert.dest_no_descendants)
|
||||
subgoal by (fastforce simp add: cdt_relation_def simp del: split_paired_All)
|
||||
subgoal by (fastforce simp add: cdt_relation_def)
|
||||
apply (subgoal_tac "mdb_insert_abs (cdt a) src dest")
|
||||
prefer 2
|
||||
apply (erule mdb_insert_abs.intro)
|
||||
|
|
@ -5676,7 +5689,7 @@ lemma cteInsert_corres:
|
|||
dest!:cap_master_cap_eqDs)
|
||||
apply (subgoal_tac "is_original_cap a src = mdbRevocable src_node")
|
||||
prefer 2
|
||||
apply (simp add: revokable_relation_def del: split_paired_All)
|
||||
apply (simp add: revokable_relation_def)
|
||||
apply (erule_tac x=src in allE)
|
||||
apply (erule impE)
|
||||
apply (clarsimp simp: null_filter_def cte_wp_at_caps_of_state cap_master_cap_simps
|
||||
|
|
@ -5690,7 +5703,7 @@ lemma cteInsert_corres:
|
|||
prefer 2
|
||||
apply assumption
|
||||
apply (simp_all)[6]
|
||||
apply (simp add: cdt_relation_def split: if_split del: split_paired_All)
|
||||
apply (simp add: cdt_relation_def split: if_split)
|
||||
apply clarsimp
|
||||
apply (drule (5) cte_map_inj)+
|
||||
apply simp
|
||||
|
|
@ -5718,7 +5731,7 @@ lemma cteInsert_corres:
|
|||
dest!:cap_master_cap_eqDs)
|
||||
apply (subgoal_tac "is_original_cap a src = mdbRevocable src_node")
|
||||
subgoal by simp
|
||||
apply (simp add: revokable_relation_def del: split_paired_All)
|
||||
apply (simp add: revokable_relation_def)
|
||||
apply (erule_tac x=src in allE)
|
||||
apply (erule impE)
|
||||
apply (clarsimp simp: null_filter_def cte_wp_at_caps_of_state split: if_splits)
|
||||
|
|
@ -5728,9 +5741,9 @@ lemma cteInsert_corres:
|
|||
apply (frule_tac p="(aa, bb)" in in_set_cap_cte_at)
|
||||
apply (rule conjI)
|
||||
apply (clarsimp simp: descendants_of_eq')
|
||||
subgoal by (simp add: cdt_relation_def del: split_paired_All)
|
||||
subgoal by (simp add: cdt_relation_def)
|
||||
apply (clarsimp simp: descendants_of_eq')
|
||||
subgoal by (simp add: cdt_relation_def del: split_paired_All)
|
||||
subgoal by (simp add: cdt_relation_def)
|
||||
done
|
||||
|
||||
|
||||
|
|
@ -6734,13 +6747,22 @@ lemma cteSwap_corres:
|
|||
| rule refl | clarsimp simp: put_def simp del: fun_upd_apply )+
|
||||
apply (simp cong: option.case_cong)
|
||||
apply (drule updateCap_stuff, elim conjE, erule(1) impE)
|
||||
apply (drule (2) updateMDB_the_lot', fastforce, fastforce, simp, clarsimp)
|
||||
apply (drule (2) updateMDB_the_lot', fastforce, fastforce, simp, clarsimp)
|
||||
apply (drule in_getCTE, clarsimp)
|
||||
apply (drule (2) updateMDB_the_lot', fastforce, fastforce, simp, clarsimp)
|
||||
apply (drule (2) updateMDB_the_lot', fastforce, fastforce, simp, clarsimp)
|
||||
apply (drule (2) updateMDB_the_lot', fastforce, fastforce, simp, clarsimp)
|
||||
apply (drule (2) updateMDB_the_lot', fastforce, fastforce, simp, clarsimp)
|
||||
apply (drule (2) updateMDB_the_lot')
|
||||
apply (erule (1) impE, assumption)
|
||||
apply (fastforce simp only: no_0_modify_map)
|
||||
apply assumption
|
||||
apply (elim conjE TrueE, simp only:)
|
||||
apply (drule (2) updateMDB_the_lot', fastforce, simp only: no_0_modify_map, assumption)
|
||||
apply (drule in_getCTE, elim conjE, simp only:)
|
||||
apply (drule (2) updateMDB_the_lot', fastforce, simp only: no_0_modify_map, assumption)
|
||||
apply (elim conjE TrueE, simp only:)
|
||||
apply (drule (2) updateMDB_the_lot', fastforce, simp only: no_0_modify_map, assumption)
|
||||
apply (elim conjE TrueE, simp only:)
|
||||
apply (drule (2) updateMDB_the_lot', fastforce, simp only: no_0_modify_map, assumption)
|
||||
apply (elim conjE TrueE, simp only:)
|
||||
apply (drule (2) updateMDB_the_lot', fastforce, simp only: no_0_modify_map, assumption)
|
||||
apply (simp only: pspace_relations_def refl)
|
||||
apply (rule conjI, rule TrueI)+
|
||||
apply (thin_tac "ksMachineState t = p" for t p)+
|
||||
apply (thin_tac "ksCurThread t = p" for t p)+
|
||||
apply (thin_tac "ksReadyQueues t = p" for t p)+
|
||||
|
|
@ -6751,7 +6773,8 @@ lemma cteSwap_corres:
|
|||
apply (thin_tac "ksDomSchedule t = p" for t p)+
|
||||
apply (thin_tac "ksCurDomain t = p" for t p)+
|
||||
apply (thin_tac "ksDomainTime t = p" for t p)+
|
||||
apply (clarsimp simp: cte_wp_at_ctes_of in_set_cap_cte_at_swp cong: if_cong)
|
||||
apply (simp only: simp_thms no_0_modify_map)
|
||||
apply (clarsimp simp: cte_wp_at_ctes_of cong: if_cong)
|
||||
apply (thin_tac "ctes_of x = y" for x y)+
|
||||
apply (case_tac cte1)
|
||||
apply (rename_tac src_cap src_node)
|
||||
|
|
@ -6772,23 +6795,48 @@ lemma cteSwap_corres:
|
|||
apply (erule weak_derived_sym')
|
||||
apply (erule weak_derived_sym')
|
||||
apply assumption
|
||||
apply (clarsimp simp: pspace_relations_def)
|
||||
apply (rule conjI)
|
||||
apply (clarsimp simp: ghost_relation_typ_at set_cap_a_type_inv ARM_HYP.data_at_def)
|
||||
subgoal by (simp only: simp_thms ghost_relation_typ_at set_cap_a_type_inv ARM_HYP.data_at_def)
|
||||
apply (thin_tac "ksMachineState t = p" for t p)+
|
||||
apply (thin_tac "ksCurThread t = p" for t p)+
|
||||
apply (thin_tac "ksReadyQueues t = p" for t p)+
|
||||
apply (thin_tac "ksSchedulerAction t = p" for t p)+
|
||||
apply (thin_tac "ready_queues t = p" for t p)+
|
||||
apply (thin_tac "cur_domain t = p" for t p)+
|
||||
apply (thin_tac "ksDomScheduleIdx t = p" for t p)+
|
||||
apply (thin_tac "ksDomSchedule t = p" for t p)+
|
||||
apply (thin_tac "ksCurDomain t = p" for t p)+
|
||||
apply (thin_tac "ksDomainTime t = p" for t p)+
|
||||
apply (thin_tac "idle_thread t = p" for t p)+
|
||||
apply (thin_tac "work_units_completed t = p" for t p)+
|
||||
apply (thin_tac "domain_index t = p" for t p)+
|
||||
apply (thin_tac "domain_list t = p" for t p)+
|
||||
apply (thin_tac "domain_time t = p" for t p)+
|
||||
apply (thin_tac "ekheap t = p" for t p)+
|
||||
apply (thin_tac "scheduler_action t = p" for t p)+
|
||||
apply (thin_tac "ksArchState t = p" for t p)+
|
||||
apply (thin_tac "gsCNodes t = p" for t p)+
|
||||
apply (thin_tac "ksWorkUnitsCompleted t = p" for t p)+
|
||||
apply (thin_tac "ksInterruptState t = p" for t p)+
|
||||
apply (thin_tac "ksIdleThread t = p" for t p)+
|
||||
apply (thin_tac "gsUserPages t = p" for t p)+
|
||||
apply (thin_tac "pspace_relation s s'" for s s')+
|
||||
apply (thin_tac "ekheap_relation e p" for e p)+
|
||||
apply (thin_tac "interrupt_state_relation n s s'" for n s s')+
|
||||
apply (thin_tac "(s,s') \<in> arch_state_relation" for s s')+
|
||||
apply(subst conj_assoc[symmetric])
|
||||
apply (rule conjI)
|
||||
prefer 2
|
||||
apply (clarsimp simp add: revokable_relation_def in_set_cap_cte_at
|
||||
simp del: split_paired_All)
|
||||
apply (drule set_cap_caps_of_state_monad)+
|
||||
apply (thin_tac "pspace_relation s t" for s t)+
|
||||
apply (simp del: split_paired_All split: if_split)
|
||||
apply (rule conjI)
|
||||
apply (clarsimp simp: cte_wp_at_caps_of_state simp del: split_paired_All)
|
||||
apply (drule(1) mdb_swap.revokable)
|
||||
apply (erule_tac x="dest" in allE)
|
||||
apply (erule impE)
|
||||
apply (clarsimp simp: null_filter_def weak_derived_Null split: if_splits)
|
||||
subgoal by (clarsimp simp: null_filter_def weak_derived_Null split: if_splits)
|
||||
apply simp
|
||||
apply (clarsimp simp del: split_paired_All)
|
||||
apply (rule conjI)
|
||||
|
|
@ -6798,19 +6846,19 @@ lemma cteSwap_corres:
|
|||
apply (simp del: split_paired_All)
|
||||
apply (erule_tac x="src" in allE)
|
||||
apply (erule impE)
|
||||
apply (clarsimp simp: null_filter_def weak_derived_Null split: if_splits)
|
||||
apply simp
|
||||
subgoal by (clarsimp simp: null_filter_def weak_derived_Null split: if_splits)
|
||||
subgoal by simp
|
||||
apply (drule caps_of_state_cte_at)+
|
||||
apply (erule (5) cte_map_inj)
|
||||
apply (clarsimp simp: cte_wp_at_caps_of_state simp del: split_paired_All)
|
||||
apply (drule (1) mdb_swap.revokable)
|
||||
apply (subgoal_tac "null_filter (caps_of_state a) (aa,bb) \<noteq> None")
|
||||
prefer 2
|
||||
apply (clarsimp simp: null_filter_def split: if_splits)
|
||||
subgoal by (clarsimp simp: null_filter_def split: if_splits)
|
||||
apply clarsimp
|
||||
apply (subgoal_tac "cte_map (aa,bb) \<noteq> cte_map src")
|
||||
apply (subgoal_tac "cte_map (aa,bb) \<noteq> cte_map dest")
|
||||
apply (clarsimp simp del: split_paired_All)
|
||||
subgoal by (clarsimp simp del: split_paired_All)
|
||||
apply (drule caps_of_state_cte_at)+
|
||||
apply (drule null_filter_caps_of_stateD)+
|
||||
apply (erule cte_map_inj, erule cte_wp_cte_at, assumption+)
|
||||
|
|
@ -6819,7 +6867,7 @@ lemma cteSwap_corres:
|
|||
apply (erule cte_map_inj, erule cte_wp_cte_at, assumption+)
|
||||
apply (subgoal_tac "no_loops (ctes_of b)")
|
||||
prefer 2
|
||||
apply (simp add: valid_mdb_ctes_def mdb_chain_0_no_loops)
|
||||
subgoal by (simp add: valid_mdb_ctes_def mdb_chain_0_no_loops)
|
||||
apply (subgoal_tac "mdb_swap_abs (cdt a) src dest a")
|
||||
prefer 2
|
||||
apply (erule mdb_swap_abs.intro)
|
||||
|
|
@ -6829,7 +6877,7 @@ lemma cteSwap_corres:
|
|||
apply assumption
|
||||
apply (frule mdb_swap_abs''.intro)
|
||||
apply (drule_tac t="cdt_list (a)" in mdb_swap_abs'.intro)
|
||||
apply (simp add: mdb_swap_abs'_axioms_def)
|
||||
subgoal by (simp add: mdb_swap_abs'_axioms_def)
|
||||
apply (thin_tac "modify_map m f p p' = t" for m f p p' t)
|
||||
apply(rule conjI)
|
||||
apply (simp add: cdt_relation_def del: split_paired_All)
|
||||
|
|
@ -6881,7 +6929,7 @@ lemma cteSwap_corres:
|
|||
apply (erule (3) inj_on_descendants_cte_map)
|
||||
apply (rule subset_refl)
|
||||
apply clarsimp
|
||||
apply auto[1]
|
||||
subgoal by auto
|
||||
apply clarsimp
|
||||
apply (rule conjI, clarsimp)
|
||||
apply (rule conjI, clarsimp)
|
||||
|
|
@ -7060,9 +7108,7 @@ lemma cteSwap_corres:
|
|||
apply(rule cte_at_next_slot')
|
||||
apply(simp_all)[9]
|
||||
apply(erule cte_wp_at_weakenE, simp)
|
||||
apply(rule cte_at_next_slot)
|
||||
apply(simp_all)
|
||||
done
|
||||
by (rule cte_at_next_slot; simp)
|
||||
|
||||
|
||||
lemma capSwapForDelete_corres:
|
||||
|
|
|
|||
|
|
@ -101,7 +101,7 @@ lemma src_no_parent [iff]:
|
|||
lemma no_0_n: "no_0 n" by (simp add: n_def no_0)
|
||||
lemma no_0': "no_0 m'" by (simp add: m'_def no_0_n)
|
||||
|
||||
lemma next_neq_dest [simp]:
|
||||
lemma next_neq_dest [iff]:
|
||||
"mdbNext src_node \<noteq> dest"
|
||||
using dlist src dest prev dest_0 no_0
|
||||
by (fastforce simp add: valid_dlist_def no_0_def Let_def)
|
||||
|
|
@ -201,26 +201,10 @@ proof -
|
|||
thus ?thesis by (simp add: m'_def)
|
||||
qed
|
||||
|
||||
lemma [iff]:
|
||||
lemma dest_not_parent [iff]:
|
||||
"m \<turnstile> dest parentOf c = False"
|
||||
using dest by (simp add: parentOf_def)
|
||||
|
||||
lemma [iff]:
|
||||
"mdbNext src_node \<noteq> dest"
|
||||
proof
|
||||
assume "mdbNext src_node = dest"
|
||||
moreover have "dest \<noteq> 0" ..
|
||||
ultimately
|
||||
have "mdbPrev old_dest_node = src"
|
||||
using src dest dlist
|
||||
by (fastforce elim: valid_dlistEn)
|
||||
with prev
|
||||
show False by (simp add: src_0)
|
||||
qed
|
||||
|
||||
lemmas no_loops_simps [simp] =
|
||||
no_loops_direct_simp [OF no_loops] no_loops_trancl_simp [OF no_loops]
|
||||
|
||||
lemma dest_source [iff]:
|
||||
"(m \<turnstile> dest \<leadsto> x) = (x = 0)"
|
||||
using dest nxt by (simp add: next_unfold')
|
||||
|
|
@ -883,10 +867,12 @@ lemma cteMove_corres:
|
|||
apply (drule (4) updateMDB_the_lot, elim conjE)
|
||||
apply (drule (4) updateMDB_the_lot, elim conjE)
|
||||
apply (drule updateCap_stuff, elim conjE, erule (1) impE)
|
||||
apply (drule updateCap_stuff, clarsimp)
|
||||
apply (drule updateCap_stuff)
|
||||
apply (subgoal_tac "pspace_distinct' b \<and> pspace_aligned' b")
|
||||
prefer 2
|
||||
subgoal by fastforce
|
||||
apply (elim valid_pspaceE' conjE)
|
||||
apply (rule conjI; assumption)
|
||||
apply (simp only: )
|
||||
apply (thin_tac "ctes_of t = s" for t s)+
|
||||
apply (thin_tac "ksMachineState t = p" for t p)+
|
||||
apply (thin_tac "ksCurThread t = p" for t p)+
|
||||
|
|
@ -895,7 +881,7 @@ lemma cteMove_corres:
|
|||
apply (thin_tac "ksSchedulerAction t = p" for t p)+
|
||||
apply (subgoal_tac "\<forall>p. cte_at p ta = cte_at p a")
|
||||
prefer 2
|
||||
apply (simp add: set_cap_cte_eq)
|
||||
subgoal by (simp add: set_cap_cte_eq)
|
||||
apply (clarsimp simp add: swp_def cte_wp_at_ctes_of simp del: split_paired_All)
|
||||
apply (subgoal_tac "cte_at ptr' a")
|
||||
prefer 2
|
||||
|
|
@ -908,7 +894,37 @@ lemma cteMove_corres:
|
|||
apply fastforce
|
||||
apply (clarsimp simp: pspace_relations_def)
|
||||
apply (rule conjI)
|
||||
apply (clarsimp simp: ghost_relation_typ_at set_cap_a_type_inv data_at_def)
|
||||
subgoal by (clarsimp simp: ghost_relation_typ_at set_cap_a_type_inv data_at_def)
|
||||
apply (thin_tac "gsCNodes t = p" for t p)+
|
||||
apply (thin_tac "ksMachineState t = p" for t p)+
|
||||
apply (thin_tac "ksCurThread t = p" for t p)+
|
||||
apply (thin_tac "ksWorkUnitsCompleted t = p" for t p)+
|
||||
apply (thin_tac "ksIdleThread t = p" for t p)+
|
||||
apply (thin_tac "ksReadyQueues t = p" for t p)+
|
||||
apply (thin_tac "ksSchedulerAction t = p" for t p)+
|
||||
apply (thin_tac "cur_thread t = p" for t p)+
|
||||
apply (thin_tac "domain_index t = p" for t p)+
|
||||
apply (thin_tac "domain_time t = p" for t p)+
|
||||
apply (thin_tac "cur_domain t = p" for t p)+
|
||||
apply (thin_tac "scheduler_action t = p" for t p)+
|
||||
apply (thin_tac "ready_queues t = p" for t p)+
|
||||
apply (thin_tac "idle_thread t = p" for t p)+
|
||||
apply (thin_tac "machine_state t = p" for t p)+
|
||||
apply (thin_tac "work_units_completed t = p" for t p)+
|
||||
apply (thin_tac "ksArchState t = p" for t p)+
|
||||
apply (thin_tac "gsUserPages t = p" for t p)+
|
||||
apply (thin_tac "ksCurDomain t = p" for t p)+
|
||||
apply (thin_tac "ksInterruptState t = p" for t p)+
|
||||
apply (thin_tac "ksDomScheduleIdx t = p" for t p)+
|
||||
apply (thin_tac "ksDomainTime t = p" for t p)+
|
||||
apply (thin_tac "ksDomSchedule t = p" for t p)+
|
||||
apply (thin_tac "ctes_of t = p" for t p)+
|
||||
apply (thin_tac "ekheap_relation t p" for t p)+
|
||||
apply (thin_tac "pspace_relation t p" for t p)+
|
||||
apply (thin_tac "interrupt_state_relation s t p" for s t p)+
|
||||
apply (thin_tac "ghost_relation s t p" for s t p)+
|
||||
apply (thin_tac "sched_act_relation t p" for t p)+
|
||||
apply (thin_tac "ready_queues_relation t p" for t p)+
|
||||
apply (subst conj_assoc[symmetric])
|
||||
apply (rule conjI)
|
||||
defer
|
||||
|
|
@ -946,7 +962,7 @@ lemma cteMove_corres:
|
|||
apply fastforce
|
||||
apply fastforce
|
||||
apply fastforce
|
||||
apply clarsimp
|
||||
subgoal by clarsimp
|
||||
subgoal by (simp add: null_filter_def split: if_splits)
|
||||
apply (subgoal_tac "mdb_move (ctes_of b) (cte_map ptr) src_cap src_node (cte_map ptr') cap' old_dest_node")
|
||||
prefer 2
|
||||
|
|
@ -970,8 +986,8 @@ lemma cteMove_corres:
|
|||
apply (rule mdb_move_abs.intro)
|
||||
apply fastforce
|
||||
apply (fastforce elim!: cte_wp_at_weakenE)
|
||||
apply simp
|
||||
apply simp
|
||||
subgoal by simp
|
||||
subgoal by simp
|
||||
apply (case_tac "(aa,bb) = ptr", simp)
|
||||
apply (subgoal_tac "cte_map (aa,bb) \<noteq> cte_map ptr")
|
||||
prefer 2
|
||||
|
|
@ -986,7 +1002,7 @@ lemma cteMove_corres:
|
|||
apply (subgoal_tac "descendants_of' (cte_map (aa, bb)) (ctes_of b) =
|
||||
cte_map ` descendants_of (aa, bb) (cdt a)")
|
||||
prefer 2
|
||||
apply (simp add: cdt_relation_def del: split_paired_All)
|
||||
subgoal by (simp add: cdt_relation_def del: split_paired_All)
|
||||
apply simp
|
||||
apply (rule conjI)
|
||||
apply clarsimp
|
||||
|
|
@ -997,8 +1013,8 @@ lemma cteMove_corres:
|
|||
apply fastforce
|
||||
apply fastforce
|
||||
apply (rule subset_refl)
|
||||
apply simp
|
||||
apply simp
|
||||
subgoal by simp
|
||||
subgoal by simp
|
||||
apply clarsimp
|
||||
apply (drule (1) cte_map_inj_eq)
|
||||
apply (erule descendants_of_cte_at)
|
||||
|
|
@ -1017,7 +1033,7 @@ lemma cteMove_corres:
|
|||
apply(intro allI impI)
|
||||
apply(rule mdb_move_abs'.next_slot)
|
||||
apply(simp, fastforce, simp)
|
||||
apply(fastforce split: option.splits)
|
||||
subgoal by(fastforce split: option.splits)
|
||||
apply(case_tac "ctes_of b (cte_map (aa, bb))")
|
||||
subgoal by (clarsimp simp: modify_map_def split: if_split_asm)
|
||||
apply(case_tac ab)
|
||||
|
|
@ -4812,12 +4828,41 @@ lemma cteInsert_simple_corres:
|
|||
apply (clarsimp simp: put_def state_relation_def simp del: fun_upd_apply)
|
||||
apply (drule updateCap_stuff)
|
||||
apply clarsimp
|
||||
apply (drule (3) updateMDB_the_lot', simp, simp, elim conjE)
|
||||
apply (drule (3) updateMDB_the_lot', simp, simp, elim conjE)
|
||||
apply (drule (3) updateMDB_the_lot', simp, simp, elim conjE)
|
||||
apply (drule (3) updateMDB_the_lot', simp only: no_0_modify_map, simp only:, elim conjE)
|
||||
apply (drule (3) updateMDB_the_lot', simp only: no_0_modify_map, simp only:, elim conjE)
|
||||
apply (drule (3) updateMDB_the_lot', simp only: no_0_modify_map, simp only:, elim conjE)
|
||||
apply (clarsimp simp: pspace_relations_def)
|
||||
apply (thin_tac "gsCNodes t = p" for t p)+
|
||||
apply (thin_tac "ksMachineState t = p" for t p)+
|
||||
apply (thin_tac "ksCurThread t = p" for t p)+
|
||||
apply (thin_tac "ksWorkUnitsCompleted t = p" for t p)+
|
||||
apply (thin_tac "ksIdleThread t = p" for t p)+
|
||||
apply (thin_tac "ksReadyQueues t = p" for t p)+
|
||||
apply (thin_tac "ksSchedulerAction t = p" for t p)+
|
||||
apply (thin_tac "cur_thread t = p" for t p)+
|
||||
apply (thin_tac "domain_index t = p" for t p)+
|
||||
apply (thin_tac "domain_time t = p" for t p)+
|
||||
apply (thin_tac "cur_domain t = p" for t p)+
|
||||
apply (thin_tac "scheduler_action t = p" for t p)+
|
||||
apply (thin_tac "ready_queues t = p" for t p)+
|
||||
apply (thin_tac "idle_thread t = p" for t p)+
|
||||
apply (thin_tac "machine_state t = p" for t p)+
|
||||
apply (thin_tac "work_units_completed t = p" for t p)+
|
||||
apply (thin_tac "ksArchState t = p" for t p)+
|
||||
apply (thin_tac "gsUserPages t = p" for t p)+
|
||||
apply (thin_tac "ksCurDomain t = p" for t p)+
|
||||
apply (thin_tac "ksInterruptState t = p" for t p)+
|
||||
apply (thin_tac "ksDomScheduleIdx t = p" for t p)+
|
||||
apply (thin_tac "ksDomainTime t = p" for t p)+
|
||||
apply (thin_tac "ksDomSchedule t = p" for t p)+
|
||||
apply (thin_tac "ctes_of t = p" for t p)+
|
||||
apply (thin_tac "ekheap_relation t p" for t p)+
|
||||
apply (thin_tac "pspace_relation t p" for t p)+
|
||||
apply (thin_tac "interrupt_state_relation s t p" for s t p)+
|
||||
apply (thin_tac "sched_act_relation t p" for t p)+
|
||||
apply (thin_tac "ready_queues_relation t p" for t p)+
|
||||
apply (rule conjI)
|
||||
apply (clarsimp simp: ghost_relation_typ_at set_cap_a_type_inv data_at_def)
|
||||
subgoal by (clarsimp simp: ghost_relation_typ_at set_cap_a_type_inv data_at_def)
|
||||
apply (clarsimp simp: cte_wp_at_ctes_of nullPointer_def prev_update_modify_mdb_relation)
|
||||
apply (subgoal_tac "cte_map dest \<noteq> 0")
|
||||
prefer 2
|
||||
|
|
@ -4827,11 +4872,6 @@ lemma cteInsert_simple_corres:
|
|||
prefer 2
|
||||
apply (clarsimp simp: valid_mdb'_def
|
||||
valid_mdb_ctes_def no_0_def)
|
||||
apply (thin_tac "ksMachineState t = p" for t p)+
|
||||
apply (thin_tac "ksCurThread t = p" for t p)+
|
||||
apply (thin_tac "ksIdleThread t = p" for t p)+
|
||||
apply (thin_tac "ksReadyQueues t = p" for t p)+
|
||||
apply (thin_tac "ksSchedulerAction t = p" for t p)+
|
||||
apply (subgoal_tac "should_be_parent_of src_cap (is_original_cap a src) c (revokable src_cap c) = True")
|
||||
prefer 2
|
||||
apply (subst should_be_parent_of_masked_as_full[symmetric])
|
||||
|
|
@ -4840,7 +4880,6 @@ lemma cteInsert_simple_corres:
|
|||
apply (subst conj_assoc[symmetric])
|
||||
apply (rule conjI)
|
||||
defer
|
||||
apply (thin_tac "ctes_of t = t'" for t t')+
|
||||
apply (clarsimp simp: modify_map_apply)
|
||||
apply (clarsimp simp: revokable_relation_def simp del: fun_upd_apply)
|
||||
apply (simp split: if_split)
|
||||
|
|
@ -4855,7 +4894,7 @@ lemma cteInsert_simple_corres:
|
|||
apply (subst same_region_as_relation [symmetric])
|
||||
prefer 3
|
||||
apply (rule safe_parent_same_region)
|
||||
apply (simp add: cte_wp_at_caps_of_state safe_parent_for_masked_as_full)
|
||||
apply (simp add: cte_wp_at_caps_of_state)
|
||||
apply assumption
|
||||
apply assumption
|
||||
apply (clarsimp simp: cte_wp_at_def is_simple_cap_def)
|
||||
|
|
@ -4892,9 +4931,6 @@ lemma cteInsert_simple_corres:
|
|||
apply clarsimp
|
||||
subgoal by (fastforce elim: cte_wp_at_weakenE)
|
||||
subgoal by (clarsimp simp: cte_wp_at'_def)
|
||||
apply (thin_tac "ctes_of s = t" for s t)+
|
||||
apply (thin_tac "pspace_relation s t" for s t)+
|
||||
apply (thin_tac "machine_state t = s" for t s)+
|
||||
apply (case_tac "srcCTE")
|
||||
apply (rename_tac src_cap' src_node)
|
||||
apply (case_tac "rv'")
|
||||
|
|
@ -4902,7 +4938,7 @@ lemma cteInsert_simple_corres:
|
|||
apply (clarsimp simp: in_set_cap_cte_at_swp)
|
||||
apply (subgoal_tac "cte_at src a \<and> safe_parent_for (cdt a) src c src_cap")
|
||||
prefer 2
|
||||
subgoal by (fastforce simp: cte_wp_at_def safe_parent_for_masked_as_full)
|
||||
subgoal by (fastforce simp: cte_wp_at_def)
|
||||
apply (erule conjE)
|
||||
|
||||
apply (subgoal_tac "mdb_insert (ctes_of b) (cte_map src) (maskedAsFull src_cap' c') src_node
|
||||
|
|
@ -4971,8 +5007,7 @@ lemma cteInsert_simple_corres:
|
|||
apply(simp)
|
||||
apply(simp add: valid_mdb'_def valid_mdb_ctes_def)
|
||||
apply(clarsimp)
|
||||
apply(drule cte_map_inj_eq)
|
||||
apply(simp_all)[6]
|
||||
subgoal by (drule cte_map_inj_eq; simp)
|
||||
apply(erule_tac x="fst src" in allE)
|
||||
apply(erule_tac x="snd src" in allE)
|
||||
apply(fastforce)
|
||||
|
|
@ -4982,12 +5017,10 @@ lemma cteInsert_simple_corres:
|
|||
apply(simp)
|
||||
apply(subgoal_tac "cte_at ca a")
|
||||
prefer 2
|
||||
apply(rule cte_at_next_slot)
|
||||
apply(simp_all)[5]
|
||||
subgoal by (rule cte_at_next_slot; simp)
|
||||
apply(clarsimp simp: modify_map_def const_def)
|
||||
apply(simp split: if_split_asm)
|
||||
apply(drule cte_map_inj_eq)
|
||||
apply(simp_all)[6]
|
||||
subgoal by (drule cte_map_inj_eq; simp)
|
||||
apply(drule_tac p="cte_map src" in valid_mdbD1')
|
||||
apply(simp)
|
||||
apply(simp add: valid_mdb'_def valid_mdb_ctes_def)
|
||||
|
|
@ -4997,12 +5030,9 @@ lemma cteInsert_simple_corres:
|
|||
apply(erule_tac x=aa in allE)
|
||||
apply(erule_tac x=bb in allE)
|
||||
apply(fastforce)
|
||||
apply(drule cte_map_inj_eq)
|
||||
apply(simp_all)[6]
|
||||
apply(drule cte_map_inj_eq)
|
||||
apply(simp_all)[6]
|
||||
apply(drule cte_map_inj_eq)
|
||||
apply(simp_all)[6]
|
||||
subgoal by (drule cte_map_inj_eq; simp)
|
||||
subgoal by (drule cte_map_inj_eq; simp)
|
||||
subgoal by (drule cte_map_inj_eq; simp)
|
||||
by(fastforce)
|
||||
|
||||
declare if_split [split]
|
||||
|
|
|
|||
|
|
@ -6694,13 +6694,22 @@ lemma cteSwap_corres:
|
|||
| rule refl | clarsimp simp: put_def simp del: fun_upd_apply )+
|
||||
apply (simp cong: option.case_cong)
|
||||
apply (drule updateCap_stuff, elim conjE, erule(1) impE)
|
||||
apply (drule (2) updateMDB_the_lot', fastforce, fastforce, simp, clarsimp)
|
||||
apply (drule (2) updateMDB_the_lot', fastforce, fastforce, simp, clarsimp)
|
||||
apply (drule in_getCTE, clarsimp)
|
||||
apply (drule (2) updateMDB_the_lot', fastforce, fastforce, simp, clarsimp)
|
||||
apply (drule (2) updateMDB_the_lot', fastforce, fastforce, simp, clarsimp)
|
||||
apply (drule (2) updateMDB_the_lot', fastforce, fastforce, simp, clarsimp)
|
||||
apply (drule (2) updateMDB_the_lot', fastforce, fastforce, simp, clarsimp)
|
||||
apply (drule (2) updateMDB_the_lot')
|
||||
apply (erule (1) impE, assumption)
|
||||
apply (fastforce simp only: no_0_modify_map)
|
||||
apply assumption
|
||||
apply (elim conjE TrueE, simp only:)
|
||||
apply (drule (2) updateMDB_the_lot', fastforce, simp only: no_0_modify_map, assumption)
|
||||
apply (drule in_getCTE, elim conjE, simp only:)
|
||||
apply (drule (2) updateMDB_the_lot', fastforce, simp only: no_0_modify_map, assumption)
|
||||
apply (elim conjE TrueE, simp only:)
|
||||
apply (drule (2) updateMDB_the_lot', fastforce, simp only: no_0_modify_map, assumption)
|
||||
apply (elim conjE TrueE, simp only:)
|
||||
apply (drule (2) updateMDB_the_lot', fastforce, simp only: no_0_modify_map, assumption)
|
||||
apply (elim conjE TrueE, simp only:)
|
||||
apply (drule (2) updateMDB_the_lot', fastforce, simp only: no_0_modify_map, assumption)
|
||||
apply (simp only: pspace_relations_def refl)
|
||||
apply (rule conjI, rule TrueI)+
|
||||
apply (thin_tac "ksMachineState t = p" for t p)+
|
||||
apply (thin_tac "ksCurThread t = p" for t p)+
|
||||
apply (thin_tac "ksReadyQueues t = p" for t p)+
|
||||
|
|
@ -6711,7 +6720,8 @@ lemma cteSwap_corres:
|
|||
apply (thin_tac "ksDomSchedule t = p" for t p)+
|
||||
apply (thin_tac "ksCurDomain t = p" for t p)+
|
||||
apply (thin_tac "ksDomainTime t = p" for t p)+
|
||||
apply (clarsimp simp: cte_wp_at_ctes_of in_set_cap_cte_at_swp cong: if_cong)
|
||||
apply (simp only: simp_thms no_0_modify_map)
|
||||
apply (clarsimp simp: cte_wp_at_ctes_of cong: if_cong)
|
||||
apply (thin_tac "ctes_of x = y" for x y)+
|
||||
apply (case_tac cte1)
|
||||
apply (rename_tac src_cap src_node)
|
||||
|
|
@ -6732,23 +6742,48 @@ lemma cteSwap_corres:
|
|||
apply (erule weak_derived_sym')
|
||||
apply (erule weak_derived_sym')
|
||||
apply assumption
|
||||
apply (clarsimp simp: pspace_relations_def)
|
||||
apply (thin_tac "ksMachineState t = p" for t p)+
|
||||
apply (thin_tac "ksCurThread t = p" for t p)+
|
||||
apply (thin_tac "ksReadyQueues t = p" for t p)+
|
||||
apply (thin_tac "ksSchedulerAction t = p" for t p)+
|
||||
apply (thin_tac "ready_queues t = p" for t p)+
|
||||
apply (thin_tac "cur_domain t = p" for t p)+
|
||||
apply (thin_tac "ksDomScheduleIdx t = p" for t p)+
|
||||
apply (thin_tac "ksDomSchedule t = p" for t p)+
|
||||
apply (thin_tac "ksCurDomain t = p" for t p)+
|
||||
apply (thin_tac "ksDomainTime t = p" for t p)+
|
||||
apply (thin_tac "idle_thread t = p" for t p)+
|
||||
apply (thin_tac "work_units_completed t = p" for t p)+
|
||||
apply (thin_tac "domain_index t = p" for t p)+
|
||||
apply (thin_tac "domain_list t = p" for t p)+
|
||||
apply (thin_tac "domain_time t = p" for t p)+
|
||||
apply (thin_tac "ekheap t = p" for t p)+
|
||||
apply (thin_tac "scheduler_action t = p" for t p)+
|
||||
apply (thin_tac "ksArchState t = p" for t p)+
|
||||
apply (thin_tac "gsCNodes t = p" for t p)+
|
||||
apply (thin_tac "ksWorkUnitsCompleted t = p" for t p)+
|
||||
apply (thin_tac "ksInterruptState t = p" for t p)+
|
||||
apply (thin_tac "ksIdleThread t = p" for t p)+
|
||||
apply (thin_tac "gsUserPages t = p" for t p)+
|
||||
apply (thin_tac "pspace_relation s s'" for s s')+
|
||||
apply (thin_tac "ekheap_relation e p" for e p)+
|
||||
apply (thin_tac "interrupt_state_relation n s s'" for n s s')+
|
||||
apply (thin_tac "(s,s') \<in> arch_state_relation" for s s')+
|
||||
apply (rule conjI)
|
||||
apply (clarsimp simp: ghost_relation_typ_at set_cap_a_type_inv RISCV64.data_at_def)
|
||||
subgoal by (clarsimp simp: ghost_relation_typ_at set_cap_a_type_inv RISCV64.data_at_def)
|
||||
apply(subst conj_assoc[symmetric])
|
||||
apply (rule conjI)
|
||||
prefer 2
|
||||
apply (clarsimp simp add: revokable_relation_def in_set_cap_cte_at
|
||||
simp del: split_paired_All)
|
||||
apply (drule set_cap_caps_of_state_monad)+
|
||||
apply (thin_tac "pspace_relation s t" for s t)+
|
||||
apply (simp del: split_paired_All split: if_split)
|
||||
apply (rule conjI)
|
||||
apply (clarsimp simp: cte_wp_at_caps_of_state simp del: split_paired_All)
|
||||
apply (drule(1) mdb_swap.revokable)
|
||||
apply (erule_tac x="dest" in allE)
|
||||
apply (erule impE)
|
||||
apply (clarsimp simp: null_filter_def weak_derived_Null split: if_splits)
|
||||
subgoal by (clarsimp simp: null_filter_def weak_derived_Null split: if_splits)
|
||||
apply simp
|
||||
apply (clarsimp simp del: split_paired_All)
|
||||
apply (rule conjI)
|
||||
|
|
@ -6758,19 +6793,19 @@ lemma cteSwap_corres:
|
|||
apply (simp del: split_paired_All)
|
||||
apply (erule_tac x="src" in allE)
|
||||
apply (erule impE)
|
||||
apply (clarsimp simp: null_filter_def weak_derived_Null split: if_splits)
|
||||
apply simp
|
||||
subgoal by (clarsimp simp: null_filter_def weak_derived_Null split: if_splits)
|
||||
subgoal by simp
|
||||
apply (drule caps_of_state_cte_at)+
|
||||
apply (erule (5) cte_map_inj)
|
||||
apply (clarsimp simp: cte_wp_at_caps_of_state simp del: split_paired_All)
|
||||
apply (drule (1) mdb_swap.revokable)
|
||||
apply (subgoal_tac "null_filter (caps_of_state a) (aa,bb) \<noteq> None")
|
||||
prefer 2
|
||||
apply (clarsimp simp: null_filter_def split: if_splits)
|
||||
subgoal by (clarsimp simp: null_filter_def split: if_splits)
|
||||
apply clarsimp
|
||||
apply (subgoal_tac "cte_map (aa,bb) \<noteq> cte_map src")
|
||||
apply (subgoal_tac "cte_map (aa,bb) \<noteq> cte_map dest")
|
||||
apply (clarsimp simp del: split_paired_All)
|
||||
subgoal by (clarsimp simp del: split_paired_All)
|
||||
apply (drule caps_of_state_cte_at)+
|
||||
apply (drule null_filter_caps_of_stateD)+
|
||||
apply (erule cte_map_inj, erule cte_wp_cte_at, assumption+)
|
||||
|
|
@ -6779,7 +6814,7 @@ lemma cteSwap_corres:
|
|||
apply (erule cte_map_inj, erule cte_wp_cte_at, assumption+)
|
||||
apply (subgoal_tac "no_loops (ctes_of b)")
|
||||
prefer 2
|
||||
apply (simp add: valid_mdb_ctes_def mdb_chain_0_no_loops)
|
||||
subgoal by (simp add: valid_mdb_ctes_def mdb_chain_0_no_loops)
|
||||
apply (subgoal_tac "mdb_swap_abs (cdt a) src dest a")
|
||||
prefer 2
|
||||
apply (erule mdb_swap_abs.intro)
|
||||
|
|
@ -6789,7 +6824,7 @@ lemma cteSwap_corres:
|
|||
apply assumption
|
||||
apply (frule mdb_swap_abs''.intro)
|
||||
apply (drule_tac t="cdt_list (a)" in mdb_swap_abs'.intro)
|
||||
apply (simp add: mdb_swap_abs'_axioms_def)
|
||||
subgoal by (simp add: mdb_swap_abs'_axioms_def)
|
||||
apply (thin_tac "modify_map m f p p' = t" for m f p p' t)
|
||||
apply(rule conjI)
|
||||
apply (simp add: cdt_relation_def del: split_paired_All)
|
||||
|
|
@ -6841,7 +6876,7 @@ lemma cteSwap_corres:
|
|||
apply (erule (3) inj_on_descendants_cte_map)
|
||||
apply (rule subset_refl)
|
||||
apply clarsimp
|
||||
apply auto[1]
|
||||
subgoal by auto
|
||||
apply clarsimp
|
||||
apply (rule conjI, clarsimp)
|
||||
apply (rule conjI, clarsimp)
|
||||
|
|
@ -7020,9 +7055,7 @@ lemma cteSwap_corres:
|
|||
apply(rule cte_at_next_slot')
|
||||
apply(simp_all)[9]
|
||||
apply(erule cte_wp_at_weakenE, simp)
|
||||
apply(rule cte_at_next_slot)
|
||||
apply(simp_all)
|
||||
done
|
||||
by (rule cte_at_next_slot; simp)
|
||||
|
||||
|
||||
lemma capSwapForDelete_corres:
|
||||
|
|
|
|||
|
|
@ -893,7 +893,31 @@ lemma cteMove_corres:
|
|||
apply fastforce
|
||||
apply (clarsimp simp: pspace_relations_def)
|
||||
apply (rule conjI)
|
||||
apply (clarsimp simp: ghost_relation_typ_at set_cap_a_type_inv data_at_def)
|
||||
subgoal by (clarsimp simp: ghost_relation_typ_at set_cap_a_type_inv data_at_def)
|
||||
apply (thin_tac "gsCNodes t = p" for t p)+
|
||||
apply (thin_tac "ksWorkUnitsCompleted t = p" for t p)+
|
||||
apply (thin_tac "cur_thread t = p" for t p)+
|
||||
apply (thin_tac "domain_index t = p" for t p)+
|
||||
apply (thin_tac "domain_time t = p" for t p)+
|
||||
apply (thin_tac "cur_domain t = p" for t p)+
|
||||
apply (thin_tac "scheduler_action t = p" for t p)+
|
||||
apply (thin_tac "ready_queues t = p" for t p)+
|
||||
apply (thin_tac "idle_thread t = p" for t p)+
|
||||
apply (thin_tac "machine_state t = p" for t p)+
|
||||
apply (thin_tac "work_units_completed t = p" for t p)+
|
||||
apply (thin_tac "ksArchState t = p" for t p)+
|
||||
apply (thin_tac "gsUserPages t = p" for t p)+
|
||||
apply (thin_tac "ksCurDomain t = p" for t p)+
|
||||
apply (thin_tac "ksInterruptState t = p" for t p)+
|
||||
apply (thin_tac "ksDomScheduleIdx t = p" for t p)+
|
||||
apply (thin_tac "ksDomainTime t = p" for t p)+
|
||||
apply (thin_tac "ksDomSchedule t = p" for t p)+
|
||||
apply (thin_tac "ekheap_relation t p" for t p)+
|
||||
apply (thin_tac "pspace_relation t p" for t p)+
|
||||
apply (thin_tac "interrupt_state_relation s t p" for s t p)+
|
||||
apply (thin_tac "ghost_relation s t p" for s t p)+
|
||||
apply (thin_tac "sched_act_relation t p" for t p)+
|
||||
apply (thin_tac "ready_queues_relation t p" for t p)+
|
||||
apply (subst conj_assoc[symmetric])
|
||||
apply (rule conjI)
|
||||
defer
|
||||
|
|
@ -945,7 +969,7 @@ lemma cteMove_corres:
|
|||
apply (simp add: nullPointer_def)
|
||||
apply (simp add: nullPointer_def)
|
||||
apply (erule weak_derived_sym')
|
||||
apply clarsimp
|
||||
subgoal by clarsimp
|
||||
apply assumption
|
||||
apply (rule conjI)
|
||||
apply (simp (no_asm) add: cdt_relation_def)
|
||||
|
|
@ -955,14 +979,14 @@ lemma cteMove_corres:
|
|||
apply (rule mdb_move_abs.intro)
|
||||
apply fastforce
|
||||
apply (fastforce elim!: cte_wp_at_weakenE)
|
||||
apply simp
|
||||
apply simp
|
||||
subgoal by simp
|
||||
subgoal by simp
|
||||
apply (case_tac "(aa,bb) = ptr", simp)
|
||||
apply (subgoal_tac "cte_map (aa,bb) \<noteq> cte_map ptr")
|
||||
prefer 2
|
||||
apply (erule (2) cte_map_inj, fastforce, fastforce, fastforce)
|
||||
apply (case_tac "(aa,bb) = ptr'")
|
||||
apply (simp add: cdt_relation_def del: split_paired_All)
|
||||
subgoal by (simp add: cdt_relation_def del: split_paired_All)
|
||||
apply (subgoal_tac "cte_map (aa,bb) \<noteq> cte_map ptr'")
|
||||
prefer 2
|
||||
apply (erule (2) cte_map_inj, fastforce, fastforce, fastforce)
|
||||
|
|
@ -982,7 +1006,7 @@ lemma cteMove_corres:
|
|||
apply fastforce
|
||||
apply fastforce
|
||||
apply (rule subset_refl)
|
||||
apply simp
|
||||
subgoal by simp
|
||||
apply simp
|
||||
apply clarsimp
|
||||
apply (drule (1) cte_map_inj_eq)
|
||||
|
|
@ -991,9 +1015,8 @@ lemma cteMove_corres:
|
|||
apply fastforce
|
||||
apply fastforce
|
||||
apply fastforce
|
||||
subgoal by clarsimp
|
||||
subgoal by simp
|
||||
apply(clarsimp simp: cdt_list_relation_def)
|
||||
|
||||
apply(subst next_slot_eq2)
|
||||
apply(simp split: option.splits)
|
||||
apply(intro conjI impI)
|
||||
|
|
@ -1002,7 +1025,7 @@ lemma cteMove_corres:
|
|||
apply(intro allI impI)
|
||||
apply(rule mdb_move_abs'.next_slot)
|
||||
apply(simp, fastforce, simp)
|
||||
apply(fastforce split: option.splits)
|
||||
subgoal by (fastforce split: option.splits)
|
||||
apply(case_tac "ctes_of b (cte_map (aa, bb))")
|
||||
subgoal by (clarsimp simp: modify_map_def split: if_split_asm)
|
||||
apply(case_tac ab)
|
||||
|
|
@ -4764,12 +4787,41 @@ lemma cteInsert_simple_corres:
|
|||
apply (clarsimp simp: put_def state_relation_def simp del: fun_upd_apply)
|
||||
apply (drule updateCap_stuff)
|
||||
apply clarsimp
|
||||
apply (drule (3) updateMDB_the_lot', simp, simp, elim conjE)
|
||||
apply (drule (3) updateMDB_the_lot', simp, simp, elim conjE)
|
||||
apply (drule (3) updateMDB_the_lot', simp, simp, elim conjE)
|
||||
apply (drule (3) updateMDB_the_lot', simp only: no_0_modify_map, simp only:, elim conjE)
|
||||
apply (drule (3) updateMDB_the_lot', simp only: no_0_modify_map, simp only:, elim conjE)
|
||||
apply (drule (3) updateMDB_the_lot', simp only: no_0_modify_map, simp only:, elim conjE)
|
||||
apply (clarsimp simp: pspace_relations_def)
|
||||
apply (rule conjI)
|
||||
apply (clarsimp simp: ghost_relation_typ_at set_cap_a_type_inv data_at_def)
|
||||
subgoal by (clarsimp simp: ghost_relation_typ_at set_cap_a_type_inv data_at_def)
|
||||
apply (thin_tac "gsCNodes t = p" for t p)+
|
||||
apply (thin_tac "ksMachineState t = p" for t p)+
|
||||
apply (thin_tac "ksCurThread t = p" for t p)+
|
||||
apply (thin_tac "ksWorkUnitsCompleted t = p" for t p)+
|
||||
apply (thin_tac "ksIdleThread t = p" for t p)+
|
||||
apply (thin_tac "ksReadyQueues t = p" for t p)+
|
||||
apply (thin_tac "ksSchedulerAction t = p" for t p)+
|
||||
apply (thin_tac "cur_thread t = p" for t p)+
|
||||
apply (thin_tac "domain_index t = p" for t p)+
|
||||
apply (thin_tac "domain_time t = p" for t p)+
|
||||
apply (thin_tac "cur_domain t = p" for t p)+
|
||||
apply (thin_tac "scheduler_action t = p" for t p)+
|
||||
apply (thin_tac "ready_queues t = p" for t p)+
|
||||
apply (thin_tac "idle_thread t = p" for t p)+
|
||||
apply (thin_tac "machine_state t = p" for t p)+
|
||||
apply (thin_tac "work_units_completed t = p" for t p)+
|
||||
apply (thin_tac "ksArchState t = p" for t p)+
|
||||
apply (thin_tac "gsUserPages t = p" for t p)+
|
||||
apply (thin_tac "ksCurDomain t = p" for t p)+
|
||||
apply (thin_tac "ksInterruptState t = p" for t p)+
|
||||
apply (thin_tac "ksDomScheduleIdx t = p" for t p)+
|
||||
apply (thin_tac "ksDomainTime t = p" for t p)+
|
||||
apply (thin_tac "ksDomSchedule t = p" for t p)+
|
||||
apply (thin_tac "ctes_of t = p" for t p)+
|
||||
apply (thin_tac "ekheap_relation t p" for t p)+
|
||||
apply (thin_tac "pspace_relation t p" for t p)+
|
||||
apply (thin_tac "interrupt_state_relation s t p" for s t p)+
|
||||
apply (thin_tac "sched_act_relation t p" for t p)+
|
||||
apply (thin_tac "ready_queues_relation t p" for t p)+
|
||||
apply (clarsimp simp: cte_wp_at_ctes_of nullPointer_def prev_update_modify_mdb_relation)
|
||||
apply (subgoal_tac "cte_map dest \<noteq> 0")
|
||||
prefer 2
|
||||
|
|
@ -4779,11 +4831,6 @@ lemma cteInsert_simple_corres:
|
|||
prefer 2
|
||||
apply (clarsimp simp: valid_mdb'_def
|
||||
valid_mdb_ctes_def no_0_def)
|
||||
apply (thin_tac "ksMachineState t = p" for t p)+
|
||||
apply (thin_tac "ksCurThread t = p" for t p)+
|
||||
apply (thin_tac "ksIdleThread t = p" for t p)+
|
||||
apply (thin_tac "ksReadyQueues t = p" for t p)+
|
||||
apply (thin_tac "ksSchedulerAction t = p" for t p)+
|
||||
apply (subgoal_tac "should_be_parent_of src_cap (is_original_cap a src) c (is_cap_revocable c src_cap) = True")
|
||||
prefer 2
|
||||
apply (subst should_be_parent_of_masked_as_full[symmetric])
|
||||
|
|
@ -4792,7 +4839,6 @@ lemma cteInsert_simple_corres:
|
|||
apply (subst conj_assoc[symmetric])
|
||||
apply (rule conjI)
|
||||
defer
|
||||
apply (thin_tac "ctes_of t = t'" for t t')+
|
||||
apply (clarsimp simp: modify_map_apply)
|
||||
apply (clarsimp simp: revokable_relation_def simp del: fun_upd_apply)
|
||||
apply (simp split: if_split)
|
||||
|
|
@ -4844,9 +4890,6 @@ lemma cteInsert_simple_corres:
|
|||
apply clarsimp
|
||||
subgoal by (fastforce elim: cte_wp_at_weakenE)
|
||||
subgoal by (clarsimp simp: cte_wp_at'_def)
|
||||
apply (thin_tac "ctes_of s = t" for s t)+
|
||||
apply (thin_tac "pspace_relation s t" for s t)+
|
||||
apply (thin_tac "machine_state t = s" for t s)+
|
||||
apply (case_tac "srcCTE")
|
||||
apply (rename_tac src_cap' src_node)
|
||||
apply (case_tac "rv'")
|
||||
|
|
@ -4884,7 +4927,7 @@ lemma cteInsert_simple_corres:
|
|||
apply (frule set_cap_caps_of_state_monad)
|
||||
apply (subgoal_tac "cte_at (aa,bb) a")
|
||||
prefer 2
|
||||
apply (clarsimp simp: cte_wp_at_caps_of_state split: if_split_asm)
|
||||
subgoal by (clarsimp simp: cte_wp_at_caps_of_state split: if_split_asm)
|
||||
apply (simp add: descendants_of_eq' cdt_relation_def split: if_split del: split_paired_All)
|
||||
apply clarsimp
|
||||
apply (drule (5) cte_map_inj)+
|
||||
|
|
@ -4934,12 +4977,10 @@ lemma cteInsert_simple_corres:
|
|||
apply(simp)
|
||||
apply(subgoal_tac "cte_at ca a")
|
||||
prefer 2
|
||||
apply(rule cte_at_next_slot)
|
||||
apply(simp_all)[5]
|
||||
subgoal by (rule cte_at_next_slot; simp)
|
||||
apply(clarsimp simp: modify_map_def const_def)
|
||||
apply(simp split: if_split_asm)
|
||||
apply(drule cte_map_inj_eq)
|
||||
apply(simp_all)[6]
|
||||
subgoal by (drule cte_map_inj_eq; simp)
|
||||
apply(drule_tac p="cte_map src" in valid_mdbD1')
|
||||
apply(simp)
|
||||
apply(simp add: valid_mdb'_def valid_mdb_ctes_def)
|
||||
|
|
@ -4949,12 +4990,9 @@ lemma cteInsert_simple_corres:
|
|||
apply(erule_tac x=aa in allE)
|
||||
apply(erule_tac x=bb in allE)
|
||||
apply(fastforce)
|
||||
apply(drule cte_map_inj_eq)
|
||||
apply(simp_all)[6]
|
||||
apply(drule cte_map_inj_eq)
|
||||
apply(simp_all)[6]
|
||||
apply(drule cte_map_inj_eq)
|
||||
apply(simp_all)[6]
|
||||
subgoal by (drule cte_map_inj_eq; simp)
|
||||
subgoal by (drule cte_map_inj_eq; simp)
|
||||
subgoal by (drule cte_map_inj_eq; simp)
|
||||
by(fastforce)
|
||||
|
||||
declare if_split [split]
|
||||
|
|
|
|||
|
|
@ -2461,15 +2461,15 @@ lemma updateCap_corres:
|
|||
apply (unfold cdt_list_relation_def)[1]
|
||||
apply (intro allI impI)
|
||||
apply (erule_tac x=c in allE)
|
||||
apply (auto elim!: modify_map_casesE)[1]
|
||||
subgoal by (auto elim!: modify_map_casesE)[1]
|
||||
apply (unfold revokable_relation_def)[1]
|
||||
apply (drule set_cap_caps_of_state_monad)
|
||||
apply (simp add: cte_wp_at_caps_of_state del: split_paired_All)
|
||||
apply (intro allI impI)
|
||||
apply (erule_tac x=c in allE)
|
||||
apply (erule impE[where P="\<exists>y. v = Some y" for v])
|
||||
apply (clarsimp simp: null_filter_def is_zombie_def split: if_split_asm)
|
||||
apply (auto elim!: modify_map_casesE del: disjE)[1] (* slow *)
|
||||
subgoal by (clarsimp simp: null_filter_def is_zombie_def split: if_split_asm)
|
||||
subgoal by (auto elim!: modify_map_casesE del: disjE)[1] (* slow *)
|
||||
apply (case_tac "ctes_of b (cte_map slot)")
|
||||
apply (simp add: modify_map_None)
|
||||
apply (simp add: modify_map_apply)
|
||||
|
|
@ -2478,10 +2478,10 @@ lemma updateCap_corres:
|
|||
apply (rule use_update_ztc_one [OF descendants_of_update_ztc])
|
||||
apply simp
|
||||
apply assumption
|
||||
apply (auto simp: is_cap_simps isCap_simps)[1]
|
||||
subgoal by (auto simp: is_cap_simps isCap_simps)[1]
|
||||
apply (frule(3) is_final_untyped_ptrs [OF _ _ not_sym], clarsimp+)
|
||||
apply (clarsimp simp: cte_wp_at_caps_of_state)
|
||||
apply (simp add: is_cap_simps, elim disjE exE, simp_all)[1]
|
||||
subgoal by (simp add: is_cap_simps, elim disjE exE, simp_all)[1]
|
||||
apply (simp add: eq_commute)
|
||||
apply (drule cte_wp_at_norm, clarsimp)
|
||||
apply (drule(1) pspace_relation_ctes_ofI, clarsimp+)
|
||||
|
|
@ -2492,15 +2492,10 @@ lemma updateCap_corres:
|
|||
apply clarsimp
|
||||
apply (drule cte_wp_at_norm, clarsimp)
|
||||
apply (drule(1) pspace_relation_ctes_ofI, clarsimp+)
|
||||
apply (simp add: is_cap_simps, elim disjE exE, simp_all add: isCap_simps)[1]
|
||||
subgoal by (simp add: is_cap_simps, elim disjE exE, simp_all add: isCap_simps)[1]
|
||||
apply clarsimp
|
||||
done
|
||||
|
||||
lemma exst_set_cap:
|
||||
"(x,s') \<in> fst (set_cap p c s) \<Longrightarrow> exst s' = exst s"
|
||||
by (clarsimp simp: set_cap_def in_monad split_def get_object_def set_object_def
|
||||
split: if_split_asm Structures_A.kernel_object.splits)
|
||||
|
||||
lemma updateMDB_eqs:
|
||||
assumes "(x, s'') \<in> fst (updateMDB p f s')"
|
||||
shows "ksMachineState s'' = ksMachineState s' \<and>
|
||||
|
|
@ -2551,8 +2546,8 @@ lemma updateMDB_pspace_relation:
|
|||
apply (subst map_upd_triv[symmetric, where t="kheap s"], assumption)
|
||||
apply (erule(2) pspace_relation_update_tcbs)
|
||||
apply (case_tac tcba)
|
||||
apply (simp add: tcb_cte_cases_def tcb_relation_def del: diff_neg_mask
|
||||
split: if_split_asm)
|
||||
subgoal by (simp add: tcb_cte_cases_def tcb_relation_def del: diff_neg_mask
|
||||
split: if_split_asm)
|
||||
apply (clarsimp simp: cte_wp_at_cases')
|
||||
apply (erule disjE)
|
||||
apply (rule pspace_dom_relatedE, assumption+)
|
||||
|
|
@ -2580,8 +2575,7 @@ lemma updateMDB_ekheap_relation:
|
|||
apply (drule(1) updateObject_cte_is_tcb_or_cte[OF _ refl, rotated])
|
||||
apply (drule_tac P="(=) s'" in use_valid [OF _ getCTE_sp], rule refl)
|
||||
apply (drule bspec, erule domI)
|
||||
apply (clarsimp simp: tcb_cte_cases_def lookupAround2_char1 split: if_split_asm)
|
||||
done
|
||||
by (clarsimp simp: tcb_cte_cases_def lookupAround2_char1 split: if_split_asm)
|
||||
|
||||
lemma updateMDB_pspace_relations:
|
||||
assumes "(x, s'') \<in> fst (updateMDB p f s')"
|
||||
|
|
@ -2645,24 +2639,17 @@ lemma is_cap_revocable_eq:
|
|||
"\<lbrakk> cap_relation c c'; cap_relation src_cap src_cap'; sameRegionAs src_cap' c';
|
||||
is_untyped_cap src_cap \<longrightarrow> \<not> is_ep_cap c \<and> \<not> is_ntfn_cap c\<rbrakk>
|
||||
\<Longrightarrow> is_cap_revocable c src_cap = isCapRevocable c' src_cap'"
|
||||
apply (clarsimp simp: isCap_simps objBits_simps bit_simps arch_is_cap_revocable_def
|
||||
bits_of_def is_cap_revocable_def Retype_H.isCapRevocable_def
|
||||
sameRegionAs_def3 isCapRevocable_def
|
||||
split: cap_relation_split_asm arch_cap.split_asm)
|
||||
done
|
||||
by (clarsimp simp: isCap_simps objBits_simps bit_simps arch_is_cap_revocable_def
|
||||
bits_of_def is_cap_revocable_def Retype_H.isCapRevocable_def
|
||||
sameRegionAs_def3 isCapRevocable_def
|
||||
split: cap_relation_split_asm arch_cap.split_asm)
|
||||
|
||||
lemma isMDBParentOf_prev_update [simp]:
|
||||
"isMDBParentOf (cteMDBNode_update (mdbPrev_update f) cte) cte' =
|
||||
isMDBParentOf cte cte'"
|
||||
"isMDBParentOf cte (cteMDBNode_update (mdbPrev_update f) cte') =
|
||||
isMDBParentOf cte cte'"
|
||||
apply (cases cte)
|
||||
apply (cases cte')
|
||||
apply (simp add: isMDBParentOf_def)
|
||||
apply (cases cte)
|
||||
apply (cases cte')
|
||||
apply (clarsimp simp: isMDBParentOf_def)
|
||||
done
|
||||
by (cases cte, cases cte', simp add: isMDBParentOf_def)+
|
||||
|
||||
lemma prev_update_subtree [simp]:
|
||||
"modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<rightarrow> b = m' \<turnstile> a \<rightarrow> b"
|
||||
|
|
@ -2905,32 +2892,25 @@ lemma is_derived_eq:
|
|||
apply (clarsimp simp: is_derived_def is_derived'_def badge_derived'_def)
|
||||
apply (rule conjI)
|
||||
apply (clarsimp simp: is_cap_simps isCap_simps)
|
||||
apply (cases c, auto simp: isCap_simps cap_master_cap_def capMasterCap_def)[1]
|
||||
apply (simp add:vsCapRef_def)
|
||||
apply (simp add:vs_cap_ref_def)
|
||||
subgoal by (cases c, auto simp: isCap_simps cap_master_cap_def capMasterCap_def vsCapRef_def
|
||||
vs_cap_ref_def)[1]
|
||||
apply (case_tac "isIRQControlCap d'")
|
||||
apply (frule(1) master_cap_relation)
|
||||
apply (clarsimp simp: isCap_simps cap_master_cap_def
|
||||
is_zombie_def is_reply_cap_def is_master_reply_cap_def
|
||||
split: cap_relation_split_asm arch_cap.split_asm)[1]
|
||||
subgoal by (clarsimp simp: isCap_simps cap_master_cap_def
|
||||
is_zombie_def is_reply_cap_def is_master_reply_cap_def
|
||||
split: cap_relation_split_asm arch_cap.split_asm)[1]
|
||||
apply (case_tac "isIOPortControlCap' d'")
|
||||
apply (frule(1) master_cap_relation)
|
||||
apply (clarsimp simp: isCap_simps cap_master_cap_def is_cap_simps is_zombie_def
|
||||
split: cap_relation_split_asm arch_cap.split_asm)
|
||||
subgoal by (clarsimp simp: isCap_simps cap_master_cap_def is_cap_simps is_zombie_def
|
||||
split: cap_relation_split_asm arch_cap.split_asm)
|
||||
apply (frule(1) master_cap_relation)
|
||||
apply (frule(1) cap_badge_relation)
|
||||
apply (frule cap_asid_cap_relation)
|
||||
apply (frule(1) capBadge_ordering_relation)
|
||||
apply (case_tac d)
|
||||
apply (simp_all add: isCap_simps is_cap_simps cap_master_cap_def
|
||||
vs_cap_ref_def vsCapRef_def capMasterCap_def
|
||||
split: cap_relation_split_asm arch_cap.split_asm)
|
||||
apply fastforce
|
||||
apply ((auto split:arch_cap.splits arch_capability.splits option.splits)[7])
|
||||
apply (clarsimp split:option.splits arch_cap.splits arch_capability.splits)
|
||||
apply (intro conjI|clarsimp)+
|
||||
apply fastforce
|
||||
done
|
||||
by (case_tac d; simp add: isCap_simps is_cap_simps cap_master_cap_def
|
||||
vs_cap_ref_def vsCapRef_def capMasterCap_def
|
||||
split: cap_relation_split_asm arch_cap.split_asm)
|
||||
(auto split:arch_cap.splits arch_capability.splits option.splits) (* slow *)
|
||||
end
|
||||
|
||||
locale masterCap =
|
||||
|
|
@ -4752,7 +4732,7 @@ lemma updateCap_cte_wp_at':
|
|||
updateCap ptr cap \<lbrace>\<lambda>rv s. Q (cte_wp_at' P' p s)\<rbrace>"
|
||||
apply (simp add:updateCap_def cte_wp_at_ctes_of)
|
||||
apply (wp setCTE_ctes_of_wp getCTE_wp)
|
||||
apply (clarsimp simp: cte_wp_at_ctes_of split del: if_split)
|
||||
apply (clarsimp simp: cte_wp_at_ctes_of)
|
||||
apply (case_tac cte, auto split: if_split)
|
||||
done
|
||||
|
||||
|
|
@ -5327,34 +5307,55 @@ lemma cteInsert_corres:
|
|||
apply (clarsimp simp: put_def state_relation_def)
|
||||
apply (drule updateCap_stuff)
|
||||
apply clarsimp
|
||||
apply (drule (3) updateMDB_the_lot', simp, simp, elim conjE)
|
||||
apply (drule (3) updateMDB_the_lot', simp, simp, elim conjE)
|
||||
apply (drule (3) updateMDB_the_lot', simp, simp, elim conjE)
|
||||
apply (clarsimp simp: cte_wp_at_ctes_of nullPointer_def
|
||||
prev_update_modify_mdb_relation)
|
||||
apply (drule (3) updateMDB_the_lot', simp only: no_0_modify_map, simp only:, elim conjE)
|
||||
apply (drule (3) updateMDB_the_lot', simp only: no_0_modify_map, simp only:, elim conjE)
|
||||
apply (drule (3) updateMDB_the_lot', simp only: no_0_modify_map, simp only:, elim conjE)
|
||||
apply (clarsimp simp: cte_wp_at_ctes_of nullPointer_def prev_update_modify_mdb_relation)
|
||||
apply (subgoal_tac "cte_map dest \<noteq> 0")
|
||||
prefer 2
|
||||
apply (clarsimp simp: valid_mdb'_def
|
||||
valid_mdb_ctes_def no_0_def)
|
||||
subgoal by (clarsimp simp: valid_mdb'_def valid_mdb_ctes_def no_0_def)
|
||||
apply (subgoal_tac "cte_map src \<noteq> 0")
|
||||
prefer 2
|
||||
apply (clarsimp simp: valid_mdb'_def
|
||||
valid_mdb_ctes_def no_0_def)
|
||||
subgoal by (clarsimp simp: valid_mdb'_def valid_mdb_ctes_def no_0_def)
|
||||
apply (thin_tac "ksMachineState t = p" for p t)+
|
||||
apply (thin_tac "ksCurThread t = p" for p t)+
|
||||
apply (thin_tac "ksIdleThread t = p" for p t)+
|
||||
apply (thin_tac "ksReadyQueues t = p" for p t)+
|
||||
apply (thin_tac "ksSchedulerAction t = p" for p t)+
|
||||
apply (clarsimp simp: pspace_relations_def)
|
||||
|
||||
apply (rule conjI)
|
||||
apply (clarsimp simp: ghost_relation_typ_at set_cap_a_type_inv data_at_def)
|
||||
subgoal by (simp only: simp_thms ghost_relation_typ_at set_cap_a_type_inv data_at_def)
|
||||
apply (thin_tac "ready_queues t = p" for t p)+
|
||||
apply (thin_tac "cur_domain t = p" for t p)+
|
||||
apply (thin_tac "ksDomScheduleIdx t = p" for t p)+
|
||||
apply (thin_tac "ksDomSchedule t = p" for t p)+
|
||||
apply (thin_tac "ksCurDomain t = p" for t p)+
|
||||
apply (thin_tac "ksDomainTime t = p" for t p)+
|
||||
apply (thin_tac "idle_thread t = p" for t p)+
|
||||
apply (thin_tac "work_units_completed t = p" for t p)+
|
||||
apply (thin_tac "domain_index t = p" for t p)+
|
||||
apply (thin_tac "domain_list t = p" for t p)+
|
||||
apply (thin_tac "domain_time t = p" for t p)+
|
||||
apply (thin_tac "ekheap t = p" for t p)+
|
||||
apply (thin_tac "scheduler_action t = p" for t p)+
|
||||
apply (thin_tac "ksArchState t = p" for t p)+
|
||||
apply (thin_tac "gsCNodes t = p" for t p)+
|
||||
apply (thin_tac "ksWorkUnitsCompleted t = p" for t p)+
|
||||
apply (thin_tac "ksInterruptState t = p" for t p)+
|
||||
apply (thin_tac "gsUserPages t = p" for t p)+
|
||||
apply (thin_tac "pspace_relation s s'" for s s')+
|
||||
apply (thin_tac "ekheap_relation e p" for e p)+
|
||||
apply (thin_tac "interrupt_state_relation n s s'" for n s s')+
|
||||
apply (thin_tac "sched_act_relation s s'" for s s')+
|
||||
apply (thin_tac "ready_queues_relation s s'" for s s')+
|
||||
apply (thin_tac "ghost_relation p s s'" for p s s')+
|
||||
apply (thin_tac "cur_thread t = p" for t p)+
|
||||
apply (thin_tac "(s,s') \<in> arch_state_relation" for s s')+
|
||||
apply (thin_tac "ctes_of s = t" for s t)+
|
||||
apply (thin_tac "machine_state t = s" for s t)+
|
||||
apply (rule conjI)
|
||||
defer
|
||||
apply(rule conjI)
|
||||
apply (thin_tac "ctes_of s = t" for s t)+
|
||||
apply (thin_tac "pspace_relation s t" for s t)+
|
||||
apply (thin_tac "machine_state t = s" for s t)+
|
||||
apply (case_tac "srcCTE")
|
||||
apply (rename_tac src_cap' src_node)
|
||||
apply (case_tac "rv'")
|
||||
|
|
@ -5416,7 +5417,7 @@ lemma cteInsert_corres:
|
|||
apply(case_tac "ca=src")
|
||||
apply(simp)
|
||||
apply(clarsimp simp: modify_map_def)
|
||||
apply(fastforce split: if_split_asm)
|
||||
subgoal by(fastforce split: if_split_asm)
|
||||
apply(case_tac "ca = dest")
|
||||
apply(simp)
|
||||
apply(rule impI)
|
||||
|
|
@ -5426,8 +5427,7 @@ lemma cteInsert_corres:
|
|||
subgoal by(simp)
|
||||
subgoal by(simp add: valid_mdb'_def valid_mdb_ctes_def)
|
||||
subgoal by(clarsimp)
|
||||
apply(drule cte_map_inj_eq')
|
||||
apply(simp_all)[2]
|
||||
subgoal by(drule cte_map_inj_eq'; simp)
|
||||
apply(erule_tac x=src in allE)+
|
||||
subgoal by(fastforce)
|
||||
apply(simp)
|
||||
|
|
@ -5438,8 +5438,7 @@ lemma cteInsert_corres:
|
|||
apply(simp_all)[4]
|
||||
apply(clarsimp simp: modify_map_def const_def)
|
||||
apply(simp split: if_split_asm)
|
||||
apply(drule cte_map_inj_eq')
|
||||
apply(simp_all)[2]
|
||||
apply(drule cte_map_inj_eq'; simp)
|
||||
apply(drule_tac p="cte_map src" in valid_mdbD1')
|
||||
subgoal by(simp)
|
||||
subgoal by(simp add: valid_mdb'_def valid_mdb_ctes_def)
|
||||
|
|
@ -5448,12 +5447,9 @@ lemma cteInsert_corres:
|
|||
apply(case_tac z)
|
||||
apply(erule_tac x="(aa, bb)" in allE)+
|
||||
subgoal by(fastforce)
|
||||
apply(drule cte_map_inj_eq')
|
||||
apply(simp_all)[2]
|
||||
apply(drule cte_map_inj_eq')
|
||||
apply(simp_all)[2]
|
||||
apply(drule cte_map_inj_eq')
|
||||
apply(simp_all)[2]
|
||||
apply(drule cte_map_inj_eq'; simp)
|
||||
apply(drule cte_map_inj_eq'; simp)
|
||||
apply(drule cte_map_inj_eq'; simp)
|
||||
apply(erule_tac x="(aa, bb)" in allE)+
|
||||
subgoal by(fastforce)
|
||||
|
||||
|
|
@ -5472,20 +5468,17 @@ lemma cteInsert_corres:
|
|||
subgoal by(simp)
|
||||
apply(simp add: valid_mdb'_def valid_mdb_ctes_def)
|
||||
subgoal by(clarsimp)
|
||||
apply(drule cte_map_inj_eq')
|
||||
apply(simp_all)[2]
|
||||
apply(drule cte_map_inj_eq'; simp)
|
||||
apply(erule_tac x=src in allE)+
|
||||
subgoal by(fastforce)
|
||||
apply(simp)
|
||||
apply(rule impI)
|
||||
apply(subgoal_tac "cte_at ca a")
|
||||
prefer 2
|
||||
apply(rule cte_at_next_slot)
|
||||
apply(simp_all)[4]
|
||||
subgoal by (rule cte_at_next_slot; simp)
|
||||
apply(clarsimp simp: modify_map_def const_def)
|
||||
apply(simp split: if_split_asm)
|
||||
apply(drule cte_map_inj_eq')
|
||||
apply(simp_all)[2]
|
||||
apply(drule cte_map_inj_eq'; simp)
|
||||
apply(drule_tac p="cte_map src" in valid_mdbD1')
|
||||
subgoal by(simp)
|
||||
subgoal by(simp add: valid_mdb'_def valid_mdb_ctes_def)
|
||||
|
|
@ -5494,17 +5487,15 @@ lemma cteInsert_corres:
|
|||
apply(case_tac z)
|
||||
apply(erule_tac x="(aa, bb)" in allE)+
|
||||
subgoal by(fastforce)
|
||||
apply(drule cte_map_inj_eq')
|
||||
apply(simp_all)[2]
|
||||
apply(drule cte_map_inj_eq')
|
||||
apply(simp_all)[2]
|
||||
apply(drule cte_map_inj_eq')
|
||||
apply(simp_all)[2]
|
||||
apply(drule cte_map_inj_eq'; simp)
|
||||
apply(drule cte_map_inj_eq'; simp)
|
||||
apply(drule cte_map_inj_eq'; simp)
|
||||
apply(erule_tac x="(aa, bb)" in allE)+
|
||||
subgoal by(fastforce)
|
||||
|
||||
apply(subgoal_tac "mdb_insert_sib (ctes_of b) (cte_map src) (maskedAsFull src_cap' c')
|
||||
src_node (cte_map dest) capability.NullCap dest_node c'")
|
||||
src_node (cte_map dest) capability.NullCap
|
||||
dest_node c'")
|
||||
prefer 2
|
||||
apply(simp add: mdb_insert_sib_def)
|
||||
apply(rule mdb_insert_sib_axioms.intro)
|
||||
|
|
@ -5517,8 +5508,7 @@ lemma cteInsert_corres:
|
|||
apply simp
|
||||
apply (subst (asm) is_cap_revocable_eq, assumption, assumption)
|
||||
apply (rule derived_sameRegionAs)
|
||||
apply (subst is_derived_eq[symmetric], assumption,
|
||||
assumption, assumption, assumption, assumption)
|
||||
apply (subst is_derived_eq[symmetric]; assumption)
|
||||
apply assumption
|
||||
subgoal by (clarsimp simp: cte_wp_at_def is_derived_def is_cap_simps cap_master_cap_simps
|
||||
dest!:cap_master_cap_eqDs)
|
||||
|
|
@ -5566,12 +5556,10 @@ lemma cteInsert_corres:
|
|||
apply(simp)
|
||||
apply(subgoal_tac "cte_at ca a")
|
||||
prefer 2
|
||||
apply(rule cte_at_next_slot)
|
||||
apply(simp_all)[4]
|
||||
subgoal by (rule cte_at_next_slot; simp)
|
||||
apply(clarsimp simp: modify_map_def const_def)
|
||||
apply(simp split: if_split_asm)
|
||||
apply(drule cte_map_inj_eq')
|
||||
apply(simp_all)[2]
|
||||
apply(drule cte_map_inj_eq'; simp)
|
||||
apply(drule_tac p="cte_map src" in valid_mdbD1')
|
||||
apply(simp)
|
||||
subgoal by(simp add: valid_mdb'_def valid_mdb_ctes_def)
|
||||
|
|
@ -5617,12 +5605,10 @@ lemma cteInsert_corres:
|
|||
apply(simp)
|
||||
apply(subgoal_tac "cte_at ca a")
|
||||
prefer 2
|
||||
apply(rule cte_at_next_slot)
|
||||
apply(simp_all)[4]
|
||||
subgoal by (rule cte_at_next_slot; simp)
|
||||
apply(clarsimp simp: modify_map_def const_def)
|
||||
apply(simp split: if_split_asm)
|
||||
apply(drule cte_map_inj_eq')
|
||||
apply(simp_all)[2]
|
||||
apply(drule cte_map_inj_eq'; simp)
|
||||
apply(drule_tac p="cte_map src" in valid_mdbD1')
|
||||
subgoal by(simp)
|
||||
subgoal by(simp add: valid_mdb'_def valid_mdb_ctes_def)
|
||||
|
|
@ -5631,15 +5617,11 @@ lemma cteInsert_corres:
|
|||
apply(case_tac z)
|
||||
apply(erule_tac x="(aa, bb)" in allE)+
|
||||
subgoal by(fastforce)
|
||||
apply(drule cte_map_inj_eq')
|
||||
apply(simp_all)[2]
|
||||
apply(drule cte_map_inj_eq')
|
||||
apply(simp_all)[2]
|
||||
apply(drule cte_map_inj_eq')
|
||||
apply(simp_all)[2]
|
||||
apply(drule cte_map_inj_eq'; simp)
|
||||
apply(drule cte_map_inj_eq'; simp)
|
||||
apply(drule cte_map_inj_eq'; simp)
|
||||
apply(erule_tac x="(aa, bb)" in allE)+
|
||||
subgoal by(fastforce)
|
||||
apply (thin_tac "ctes_of t = t'" for t t')+
|
||||
apply (clarsimp simp: modify_map_apply)
|
||||
apply (clarsimp simp: revokable_relation_def split: if_split)
|
||||
apply (rule conjI)
|
||||
|
|
@ -5684,19 +5666,15 @@ lemma cteInsert_corres:
|
|||
apply (erule (5) cte_map_inj)
|
||||
(* FIXME *)
|
||||
|
||||
apply (rule setUntypedCapAsFull_corres)
|
||||
apply simp+
|
||||
apply (rule setUntypedCapAsFull_corres; simp)
|
||||
apply (wp set_untyped_cap_full_valid_objs set_untyped_cap_as_full_valid_mdb
|
||||
set_untyped_cap_as_full_cte_wp_at setUntypedCapAsFull_valid_cap
|
||||
setUntypedCapAsFull_cte_wp_at | clarsimp simp: cte_wp_at_caps_of_state| wps)+
|
||||
set_untyped_cap_as_full_cte_wp_at setUntypedCapAsFull_valid_cap
|
||||
setUntypedCapAsFull_cte_wp_at | clarsimp simp: cte_wp_at_caps_of_state| wps)+
|
||||
apply (case_tac rv',clarsimp simp:cte_wp_at_ctes_of maskedAsFull_def)
|
||||
apply (wp getCTE_wp' get_cap_wp)+
|
||||
apply clarsimp
|
||||
subgoal by (fastforce elim: cte_wp_at_weakenE)
|
||||
apply (clarsimp simp: cte_wp_at'_def)
|
||||
apply (thin_tac "ctes_of s = t" for s t)+
|
||||
apply (thin_tac "pspace_relation s t" for s t)+
|
||||
apply (thin_tac "machine_state t = s" for s t)+
|
||||
apply (case_tac "srcCTE")
|
||||
apply (rename_tac src_cap' src_node)
|
||||
apply (case_tac "rv'")
|
||||
|
|
@ -5730,7 +5708,7 @@ lemma cteInsert_corres:
|
|||
apply (subgoal_tac "descendants_of dest (cdt a) = {}")
|
||||
prefer 2
|
||||
apply (drule mdb_insert.dest_no_descendants)
|
||||
subgoal by (fastforce simp add: cdt_relation_def simp del: split_paired_All)
|
||||
subgoal by (fastforce simp add: cdt_relation_def)
|
||||
apply (subgoal_tac "mdb_insert_abs (cdt a) src dest")
|
||||
prefer 2
|
||||
apply (erule mdb_insert_abs.intro)
|
||||
|
|
@ -5743,8 +5721,7 @@ lemma cteInsert_corres:
|
|||
apply (intro impI allI)
|
||||
apply (unfold const_def)
|
||||
apply (frule(4) iffD1[OF is_derived_eq])
|
||||
apply (drule_tac src_cap' = src_cap' in
|
||||
maskedAsFull_revokable[where a = c',symmetric])
|
||||
apply (drule_tac src_cap' = src_cap' in maskedAsFull_revokable[where a = c',symmetric])
|
||||
apply simp
|
||||
apply (subst mdb_insert_child.descendants)
|
||||
apply (rule mdb_insert_child.intro)
|
||||
|
|
@ -5765,11 +5742,11 @@ lemma cteInsert_corres:
|
|||
dest!:cap_master_cap_eqDs)
|
||||
apply (subgoal_tac "is_original_cap a src = mdbRevocable src_node")
|
||||
prefer 2
|
||||
apply (simp add: revokable_relation_def del: split_paired_All)
|
||||
apply (simp add: revokable_relation_def)
|
||||
apply (erule_tac x=src in allE)
|
||||
apply (erule impE)
|
||||
apply (clarsimp simp: null_filter_def cte_wp_at_caps_of_state cap_master_cap_simps
|
||||
split: if_splits dest!:cap_master_cap_eqDs)
|
||||
split: if_splits dest!:cap_master_cap_eqDs)
|
||||
subgoal by (clarsimp simp: masked_as_full_def is_cap_simps free_index_update_def split: if_splits)
|
||||
subgoal by simp
|
||||
subgoal by clarsimp
|
||||
|
|
@ -5779,7 +5756,7 @@ lemma cteInsert_corres:
|
|||
prefer 2
|
||||
apply assumption
|
||||
apply (simp_all)[6]
|
||||
apply (simp add: cdt_relation_def split: if_split del: split_paired_All)
|
||||
apply (simp add: cdt_relation_def split: if_split)
|
||||
apply clarsimp
|
||||
apply (drule (5) cte_map_inj)+
|
||||
apply simp
|
||||
|
|
@ -5807,7 +5784,7 @@ lemma cteInsert_corres:
|
|||
dest!:cap_master_cap_eqDs)
|
||||
apply (subgoal_tac "is_original_cap a src = mdbRevocable src_node")
|
||||
subgoal by simp
|
||||
apply (simp add: revokable_relation_def del: split_paired_All)
|
||||
apply (simp add: revokable_relation_def)
|
||||
apply (erule_tac x=src in allE)
|
||||
apply (erule impE)
|
||||
apply (clarsimp simp: null_filter_def cte_wp_at_caps_of_state split: if_splits)
|
||||
|
|
@ -5817,9 +5794,9 @@ lemma cteInsert_corres:
|
|||
apply (frule_tac p="(aa, bb)" in in_set_cap_cte_at)
|
||||
apply (rule conjI)
|
||||
apply (clarsimp simp: descendants_of_eq')
|
||||
subgoal by (simp add: cdt_relation_def del: split_paired_All)
|
||||
subgoal by (simp add: cdt_relation_def)
|
||||
apply (clarsimp simp: descendants_of_eq')
|
||||
subgoal by (simp add: cdt_relation_def del: split_paired_All)
|
||||
subgoal by (simp add: cdt_relation_def)
|
||||
done
|
||||
|
||||
|
||||
|
|
@ -6823,13 +6800,22 @@ lemma cteSwap_corres:
|
|||
| rule refl | clarsimp simp: put_def simp del: fun_upd_apply )+
|
||||
apply (simp cong: option.case_cong)
|
||||
apply (drule updateCap_stuff, elim conjE, erule(1) impE)
|
||||
apply (drule (2) updateMDB_the_lot', fastforce, fastforce, simp, clarsimp)
|
||||
apply (drule (2) updateMDB_the_lot', fastforce, fastforce, simp, clarsimp)
|
||||
apply (drule in_getCTE, clarsimp)
|
||||
apply (drule (2) updateMDB_the_lot', fastforce, fastforce, simp, clarsimp)
|
||||
apply (drule (2) updateMDB_the_lot', fastforce, fastforce, simp, clarsimp)
|
||||
apply (drule (2) updateMDB_the_lot', fastforce, fastforce, simp, clarsimp)
|
||||
apply (drule (2) updateMDB_the_lot', fastforce, fastforce, simp, clarsimp)
|
||||
apply (drule (2) updateMDB_the_lot')
|
||||
apply (erule (1) impE, assumption)
|
||||
apply (fastforce simp only: no_0_modify_map)
|
||||
apply assumption
|
||||
apply (elim conjE TrueE, simp only:)
|
||||
apply (drule (2) updateMDB_the_lot', fastforce, simp only: no_0_modify_map, assumption)
|
||||
apply (drule in_getCTE, elim conjE, simp only:)
|
||||
apply (drule (2) updateMDB_the_lot', fastforce, simp only: no_0_modify_map, assumption)
|
||||
apply (elim conjE TrueE, simp only:)
|
||||
apply (drule (2) updateMDB_the_lot', fastforce, simp only: no_0_modify_map, assumption)
|
||||
apply (elim conjE TrueE, simp only:)
|
||||
apply (drule (2) updateMDB_the_lot', fastforce, simp only: no_0_modify_map, assumption)
|
||||
apply (elim conjE TrueE, simp only:)
|
||||
apply (drule (2) updateMDB_the_lot', fastforce, simp only: no_0_modify_map, assumption)
|
||||
apply (simp only: pspace_relations_def refl)
|
||||
apply (rule conjI, rule TrueI)+
|
||||
apply (thin_tac "ksMachineState t = p" for t p)+
|
||||
apply (thin_tac "ksCurThread t = p" for t p)+
|
||||
apply (thin_tac "ksReadyQueues t = p" for t p)+
|
||||
|
|
@ -6840,7 +6826,28 @@ lemma cteSwap_corres:
|
|||
apply (thin_tac "ksDomSchedule t = p" for t p)+
|
||||
apply (thin_tac "ksCurDomain t = p" for t p)+
|
||||
apply (thin_tac "ksDomainTime t = p" for t p)+
|
||||
apply (clarsimp simp: cte_wp_at_ctes_of in_set_cap_cte_at_swp cong: if_cong)
|
||||
apply (thin_tac "ready_queues t = p" for t p)+
|
||||
apply (thin_tac "cur_domain t = p" for t p)+
|
||||
apply (thin_tac "idle_thread t = p" for t p)+
|
||||
apply (thin_tac "work_units_completed t = p" for t p)+
|
||||
apply (thin_tac "domain_index t = p" for t p)+
|
||||
apply (thin_tac "domain_list t = p" for t p)+
|
||||
apply (thin_tac "domain_time t = p" for t p)+
|
||||
apply (thin_tac "ekheap t = p" for t p)+
|
||||
apply (thin_tac "scheduler_action t = p" for t p)+
|
||||
apply (thin_tac "ksArchState t = p" for t p)+
|
||||
apply (thin_tac "gsCNodes t = p" for t p)+
|
||||
apply (thin_tac "ksWorkUnitsCompleted t = p" for t p)+
|
||||
apply (thin_tac "ksInterruptState t = p" for t p)+
|
||||
apply (thin_tac "ksIdleThread t = p" for t p)+
|
||||
apply (thin_tac "gsUserPages t = p" for t p)+
|
||||
apply (thin_tac "ekheap_relation e p" for e p)+
|
||||
apply (thin_tac "interrupt_state_relation n s s'" for n s s')+
|
||||
apply (thin_tac "(s,s') \<in> arch_state_relation" for s s')+
|
||||
apply (thin_tac "sched_act_relation s s'" for s s')+
|
||||
apply (thin_tac "ready_queues_relation s s'" for s s')+
|
||||
apply (simp only: simp_thms no_0_modify_map)
|
||||
apply (clarsimp simp: cte_wp_at_ctes_of cong: if_cong)
|
||||
apply (thin_tac "ctes_of x = y" for x y)+
|
||||
apply (case_tac cte1)
|
||||
apply (rename_tac src_cap src_node)
|
||||
|
|
@ -6861,24 +6868,39 @@ lemma cteSwap_corres:
|
|||
apply (erule weak_derived_sym')
|
||||
apply (erule weak_derived_sym')
|
||||
apply assumption
|
||||
apply (clarsimp simp: pspace_relations_def)
|
||||
apply (rule conjI)
|
||||
apply (clarsimp simp: ghost_relation_typ_at set_cap_a_type_inv X64.data_at_def)
|
||||
subgoal by (simp only: simp_thms ghost_relation_typ_at set_cap_a_type_inv X64.data_at_def)
|
||||
apply (thin_tac "ksArchState t = p" for t p)+
|
||||
apply (thin_tac "gsCNodes t = p" for t p)+
|
||||
apply (thin_tac "ksWorkUnitsCompleted t = p" for t p)+
|
||||
apply (thin_tac "ksInterruptState t = p" for t p)+
|
||||
apply (thin_tac "ksIdleThread t = p" for t p)+
|
||||
apply (thin_tac "gsUserPages t = p" for t p)+
|
||||
apply (thin_tac "ekheap_relation e p" for e p)+
|
||||
apply (thin_tac "ksMachineState t = p" for t p)+
|
||||
apply (thin_tac "ksCurThread t = p" for t p)+
|
||||
apply (thin_tac "ksReadyQueues t = p" for t p)+
|
||||
apply (thin_tac "ksSchedulerAction t = p" for t p)+
|
||||
apply (thin_tac "ksDomScheduleIdx t = p" for t p)+
|
||||
apply (thin_tac "ksDomSchedule t = p" for t p)+
|
||||
apply (thin_tac "ksCurDomain t = p" for t p)+
|
||||
apply (thin_tac "ksDomainTime t = p" for t p)+
|
||||
apply (thin_tac "pspace_relation s t" for s t)+
|
||||
apply (thin_tac "ghost_relation h s t" for h s t)+
|
||||
apply(subst conj_assoc[symmetric])
|
||||
apply (rule conjI)
|
||||
prefer 2
|
||||
apply (clarsimp simp add: revokable_relation_def in_set_cap_cte_at
|
||||
simp del: split_paired_All)
|
||||
apply (drule set_cap_caps_of_state_monad)+
|
||||
apply (thin_tac "pspace_relation s t" for s t)+
|
||||
apply (simp del: split_paired_All split: if_split)
|
||||
apply (rule conjI)
|
||||
apply (clarsimp simp: cte_wp_at_caps_of_state simp del: split_paired_All)
|
||||
apply (drule(1) mdb_swap.revokable)
|
||||
apply (erule_tac x="dest" in allE)
|
||||
apply (erule impE)
|
||||
apply (clarsimp simp: null_filter_def weak_derived_Null split: if_splits)
|
||||
apply simp
|
||||
subgoal by (clarsimp simp: null_filter_def weak_derived_Null split: if_splits)
|
||||
subgoal by simp
|
||||
apply (clarsimp simp del: split_paired_All)
|
||||
apply (rule conjI)
|
||||
apply (clarsimp simp: cte_wp_at_caps_of_state simp del: split_paired_All)
|
||||
|
|
@ -6887,19 +6909,19 @@ lemma cteSwap_corres:
|
|||
apply (simp del: split_paired_All)
|
||||
apply (erule_tac x="src" in allE)
|
||||
apply (erule impE)
|
||||
apply (clarsimp simp: null_filter_def weak_derived_Null split: if_splits)
|
||||
apply simp
|
||||
subgoal by (clarsimp simp: null_filter_def weak_derived_Null split: if_splits)
|
||||
subgoal by simp
|
||||
apply (drule caps_of_state_cte_at)+
|
||||
apply (erule (5) cte_map_inj)
|
||||
apply (clarsimp simp: cte_wp_at_caps_of_state simp del: split_paired_All)
|
||||
apply (drule (1) mdb_swap.revokable)
|
||||
apply (subgoal_tac "null_filter (caps_of_state a) (aa,bb) \<noteq> None")
|
||||
prefer 2
|
||||
apply (clarsimp simp: null_filter_def split: if_splits)
|
||||
subgoal by (clarsimp simp: null_filter_def split: if_splits)
|
||||
apply clarsimp
|
||||
apply (subgoal_tac "cte_map (aa,bb) \<noteq> cte_map src")
|
||||
apply (subgoal_tac "cte_map (aa,bb) \<noteq> cte_map dest")
|
||||
apply (clarsimp simp del: split_paired_All)
|
||||
subgoal by (clarsimp simp del: split_paired_All)
|
||||
apply (drule caps_of_state_cte_at)+
|
||||
apply (drule null_filter_caps_of_stateD)+
|
||||
apply (erule cte_map_inj, erule cte_wp_cte_at, assumption+)
|
||||
|
|
@ -6908,7 +6930,7 @@ lemma cteSwap_corres:
|
|||
apply (erule cte_map_inj, erule cte_wp_cte_at, assumption+)
|
||||
apply (subgoal_tac "no_loops (ctes_of b)")
|
||||
prefer 2
|
||||
apply (simp add: valid_mdb_ctes_def mdb_chain_0_no_loops)
|
||||
subgoal by (simp add: valid_mdb_ctes_def mdb_chain_0_no_loops)
|
||||
apply (subgoal_tac "mdb_swap_abs (cdt a) src dest a")
|
||||
prefer 2
|
||||
apply (erule mdb_swap_abs.intro)
|
||||
|
|
@ -6918,7 +6940,7 @@ lemma cteSwap_corres:
|
|||
apply assumption
|
||||
apply (frule mdb_swap_abs''.intro)
|
||||
apply (drule_tac t="cdt_list (a)" in mdb_swap_abs'.intro)
|
||||
apply (simp add: mdb_swap_abs'_axioms_def)
|
||||
subgoal by (simp add: mdb_swap_abs'_axioms_def)
|
||||
apply (thin_tac "modify_map m f p p' = t" for m f p p' t)
|
||||
apply(rule conjI)
|
||||
apply (simp add: cdt_relation_def del: split_paired_All)
|
||||
|
|
@ -6962,7 +6984,7 @@ lemma cteSwap_corres:
|
|||
apply (erule cte_wp_at_weakenE, rule TrueI)
|
||||
apply (erule (1) descendants_of_cte_at)
|
||||
apply assumption+
|
||||
apply simp
|
||||
subgoal by simp
|
||||
apply (subst insert_minus_eq, assumption)
|
||||
apply clarsimp
|
||||
apply (subst insert_minus_eq [where x="cte_map dest"], assumption)
|
||||
|
|
@ -6970,7 +6992,7 @@ lemma cteSwap_corres:
|
|||
apply (erule (3) inj_on_descendants_cte_map)
|
||||
apply (rule subset_refl)
|
||||
apply clarsimp
|
||||
apply auto[1]
|
||||
subgoal by auto
|
||||
apply clarsimp
|
||||
apply (rule conjI, clarsimp)
|
||||
apply (rule conjI, clarsimp)
|
||||
|
|
@ -7062,12 +7084,10 @@ lemma cteSwap_corres:
|
|||
cte_map (aa, bb) = mdbPrev src_node")
|
||||
apply(clarsimp)
|
||||
apply(rule conjI)
|
||||
apply(rule cte_map_inj)
|
||||
apply(simp_all)[6]
|
||||
apply(rule cte_map_inj; simp?)
|
||||
apply(erule cte_wp_at_weakenE, simp)
|
||||
apply(rule conjI)
|
||||
apply(rule cte_map_inj)
|
||||
apply(simp_all)[6]
|
||||
apply(rule cte_map_inj; simp?)
|
||||
apply(erule cte_wp_at_weakenE, simp)
|
||||
apply(frule mdb_swap.m_exists)
|
||||
apply(simp)
|
||||
|
|
@ -7076,8 +7096,7 @@ lemma cteSwap_corres:
|
|||
apply(clarsimp)
|
||||
apply(simp add: valid_mdb'_def)
|
||||
apply(clarsimp)
|
||||
apply(rule cte_at_next_slot)
|
||||
apply(simp_all)[4]
|
||||
subgoal by (rule cte_at_next_slot; simp)
|
||||
apply(case_tac "next_slot (aa, bb) (cdt_list (a)) (cdt a) = Some dest")
|
||||
apply(simp)
|
||||
apply(erule_tac x=aa in allE, erule_tac x=bb in allE)
|
||||
|
|
@ -7090,12 +7109,10 @@ lemma cteSwap_corres:
|
|||
apply(clarsimp)
|
||||
apply(clarsimp simp: mdb_swap.prev_dest_src)
|
||||
apply(rule conjI)
|
||||
apply(rule cte_map_inj)
|
||||
apply(simp_all)[6]
|
||||
apply(rule cte_map_inj; simp?)
|
||||
apply(erule cte_wp_at_weakenE, simp)
|
||||
apply(rule conjI)
|
||||
apply(rule cte_map_inj)
|
||||
apply(simp_all)[6]
|
||||
apply(rule cte_map_inj; simp?)
|
||||
apply(erule cte_wp_at_weakenE, simp)
|
||||
apply(frule mdb_swap.m_exists)
|
||||
apply(simp)
|
||||
|
|
@ -7104,8 +7121,7 @@ lemma cteSwap_corres:
|
|||
apply(clarsimp)
|
||||
apply(simp add: valid_mdb'_def)
|
||||
apply(clarsimp)
|
||||
apply(rule cte_at_next_slot)
|
||||
apply(simp_all)[4]
|
||||
subgoal by (rule cte_at_next_slot; simp)
|
||||
apply(simp)
|
||||
apply(case_tac "next_slot (aa, bb) (cdt_list (a)) (cdt a)")
|
||||
apply(simp)
|
||||
|
|
@ -7119,12 +7135,10 @@ lemma cteSwap_corres:
|
|||
cte_map (aa, bb) \<noteq> mdbPrev dest_node")
|
||||
apply(clarsimp)
|
||||
apply(rule conjI)
|
||||
apply(rule cte_map_inj)
|
||||
apply(simp_all)[6]
|
||||
apply(rule cte_map_inj; simp?)
|
||||
apply(erule cte_wp_at_weakenE, simp)
|
||||
apply(rule conjI)
|
||||
apply(rule cte_map_inj)
|
||||
apply simp_all[6]
|
||||
apply(rule cte_map_inj; simp?)
|
||||
apply(erule cte_wp_at_weakenE, simp)
|
||||
apply(rule conjI)
|
||||
apply(frule mdb_swap.m_exists)
|
||||
|
|
@ -7134,9 +7148,8 @@ lemma cteSwap_corres:
|
|||
subgoal by (clarsimp)
|
||||
apply(simp add: valid_mdb'_def)
|
||||
apply(clarsimp)
|
||||
apply(drule cte_map_inj_eq)
|
||||
apply(rule cte_at_next_slot')
|
||||
apply(simp_all)[9]
|
||||
apply(drule cte_map_inj_eq; simp?)
|
||||
subgoal by (rule cte_at_next_slot'; simp)
|
||||
apply(erule cte_wp_at_weakenE, simp)
|
||||
apply(frule mdb_swap.m_exists)
|
||||
apply(simp)
|
||||
|
|
@ -7145,13 +7158,10 @@ lemma cteSwap_corres:
|
|||
apply(clarsimp)
|
||||
apply(simp add: valid_mdb'_def)
|
||||
apply(clarsimp)
|
||||
apply(drule cte_map_inj_eq)
|
||||
apply(rule cte_at_next_slot')
|
||||
apply(simp_all)[9]
|
||||
apply(erule cte_wp_at_weakenE, simp)
|
||||
apply(rule cte_at_next_slot)
|
||||
apply(simp_all)
|
||||
done
|
||||
apply(drule cte_map_inj_eq; simp?)
|
||||
subgoal by (rule cte_at_next_slot'; simp)
|
||||
apply(erule cte_wp_at_weakenE, simp)
|
||||
by (rule cte_at_next_slot; simp)
|
||||
|
||||
|
||||
lemma capSwapForDelete_corres:
|
||||
|
|
|
|||
|
|
@ -776,8 +776,7 @@ lemma sameObjectAs_def2:
|
|||
split del: if_split cong: if_cong)
|
||||
apply (simp add: capRange_def isCap_simps
|
||||
split del: if_split)
|
||||
apply fastforce
|
||||
done
|
||||
by fastforce
|
||||
|
||||
lemmas sameRegionAs_def3 =
|
||||
sameRegionAs_def2 [simplified capClass_Master capRange_Master isCap_Master]
|
||||
|
|
|
|||
|
|
@ -101,7 +101,7 @@ lemma src_no_parent [iff]:
|
|||
lemma no_0_n: "no_0 n" by (simp add: n_def no_0)
|
||||
lemma no_0': "no_0 m'" by (simp add: m'_def no_0_n)
|
||||
|
||||
lemma next_neq_dest [simp]:
|
||||
lemma next_neq_dest [iff]:
|
||||
"mdbNext src_node \<noteq> dest"
|
||||
using dlist src dest prev dest_0 no_0
|
||||
by (fastforce simp add: valid_dlist_def no_0_def Let_def)
|
||||
|
|
@ -201,26 +201,10 @@ proof -
|
|||
thus ?thesis by (simp add: m'_def)
|
||||
qed
|
||||
|
||||
lemma [iff]:
|
||||
lemma dest_not_parent [iff]:
|
||||
"m \<turnstile> dest parentOf c = False"
|
||||
using dest by (simp add: parentOf_def)
|
||||
|
||||
lemma [iff]:
|
||||
"mdbNext src_node \<noteq> dest"
|
||||
proof
|
||||
assume "mdbNext src_node = dest"
|
||||
moreover have "dest \<noteq> 0" ..
|
||||
ultimately
|
||||
have "mdbPrev old_dest_node = src"
|
||||
using src dest dlist
|
||||
by (fastforce elim: valid_dlistEn)
|
||||
with prev
|
||||
show False by (simp add: src_0)
|
||||
qed
|
||||
|
||||
lemmas no_loops_simps [simp] =
|
||||
no_loops_direct_simp [OF no_loops] no_loops_trancl_simp [OF no_loops]
|
||||
|
||||
lemma dest_source [iff]:
|
||||
"(m \<turnstile> dest \<leadsto> x) = (x = 0)"
|
||||
using dest nxt by (simp add: next_unfold')
|
||||
|
|
@ -884,10 +868,12 @@ lemma cteMove_corres:
|
|||
apply (drule (4) updateMDB_the_lot, elim conjE)
|
||||
apply (drule (4) updateMDB_the_lot, elim conjE)
|
||||
apply (drule updateCap_stuff, elim conjE, erule (1) impE)
|
||||
apply (drule updateCap_stuff, clarsimp)
|
||||
apply (drule updateCap_stuff)
|
||||
apply (subgoal_tac "pspace_distinct' b \<and> pspace_aligned' b")
|
||||
prefer 2
|
||||
subgoal by fastforce
|
||||
apply (elim valid_pspaceE' conjE)
|
||||
apply (rule conjI; assumption)
|
||||
apply (simp only: )
|
||||
apply (thin_tac "ctes_of t = s" for t s)+
|
||||
apply (thin_tac "ksMachineState t = p" for t p)+
|
||||
apply (thin_tac "ksCurThread t = p" for t p)+
|
||||
|
|
@ -896,7 +882,7 @@ lemma cteMove_corres:
|
|||
apply (thin_tac "ksSchedulerAction t = p" for t p)+
|
||||
apply (subgoal_tac "\<forall>p. cte_at p ta = cte_at p a")
|
||||
prefer 2
|
||||
apply (simp add: set_cap_cte_eq)
|
||||
subgoal by (simp add: set_cap_cte_eq)
|
||||
apply (clarsimp simp add: swp_def cte_wp_at_ctes_of simp del: split_paired_All)
|
||||
apply (subgoal_tac "cte_at ptr' a")
|
||||
prefer 2
|
||||
|
|
@ -909,7 +895,37 @@ lemma cteMove_corres:
|
|||
apply fastforce
|
||||
apply (clarsimp simp: pspace_relations_def)
|
||||
apply (rule conjI)
|
||||
apply (clarsimp simp: ghost_relation_typ_at set_cap_a_type_inv data_at_def)
|
||||
subgoal by (clarsimp simp: ghost_relation_typ_at set_cap_a_type_inv data_at_def)
|
||||
apply (thin_tac "gsCNodes t = p" for t p)+
|
||||
apply (thin_tac "ksMachineState t = p" for t p)+
|
||||
apply (thin_tac "ksCurThread t = p" for t p)+
|
||||
apply (thin_tac "ksWorkUnitsCompleted t = p" for t p)+
|
||||
apply (thin_tac "ksIdleThread t = p" for t p)+
|
||||
apply (thin_tac "ksReadyQueues t = p" for t p)+
|
||||
apply (thin_tac "ksSchedulerAction t = p" for t p)+
|
||||
apply (thin_tac "cur_thread t = p" for t p)+
|
||||
apply (thin_tac "domain_index t = p" for t p)+
|
||||
apply (thin_tac "domain_time t = p" for t p)+
|
||||
apply (thin_tac "cur_domain t = p" for t p)+
|
||||
apply (thin_tac "scheduler_action t = p" for t p)+
|
||||
apply (thin_tac "ready_queues t = p" for t p)+
|
||||
apply (thin_tac "idle_thread t = p" for t p)+
|
||||
apply (thin_tac "machine_state t = p" for t p)+
|
||||
apply (thin_tac "work_units_completed t = p" for t p)+
|
||||
apply (thin_tac "ksArchState t = p" for t p)+
|
||||
apply (thin_tac "gsUserPages t = p" for t p)+
|
||||
apply (thin_tac "ksCurDomain t = p" for t p)+
|
||||
apply (thin_tac "ksInterruptState t = p" for t p)+
|
||||
apply (thin_tac "ksDomScheduleIdx t = p" for t p)+
|
||||
apply (thin_tac "ksDomainTime t = p" for t p)+
|
||||
apply (thin_tac "ksDomSchedule t = p" for t p)+
|
||||
apply (thin_tac "ctes_of t = p" for t p)+
|
||||
apply (thin_tac "ekheap_relation t p" for t p)+
|
||||
apply (thin_tac "pspace_relation t p" for t p)+
|
||||
apply (thin_tac "interrupt_state_relation s t p" for s t p)+
|
||||
apply (thin_tac "ghost_relation s t p" for s t p)+
|
||||
apply (thin_tac "sched_act_relation t p" for t p)+
|
||||
apply (thin_tac "ready_queues_relation t p" for t p)+
|
||||
apply (subst conj_assoc[symmetric])
|
||||
apply (rule conjI)
|
||||
defer
|
||||
|
|
@ -947,7 +963,7 @@ lemma cteMove_corres:
|
|||
apply fastforce
|
||||
apply fastforce
|
||||
apply fastforce
|
||||
apply clarsimp
|
||||
subgoal by clarsimp
|
||||
subgoal by (simp add: null_filter_def split: if_splits) (*long *)
|
||||
apply (subgoal_tac "mdb_move (ctes_of b) (cte_map ptr) src_cap src_node (cte_map ptr') cap' old_dest_node")
|
||||
prefer 2
|
||||
|
|
@ -972,13 +988,13 @@ lemma cteMove_corres:
|
|||
apply fastforce
|
||||
apply (fastforce elim!: cte_wp_at_weakenE)
|
||||
apply simp
|
||||
apply simp
|
||||
subgoal by simp
|
||||
apply (case_tac "(aa,bb) = ptr", simp)
|
||||
apply (subgoal_tac "cte_map (aa,bb) \<noteq> cte_map ptr")
|
||||
prefer 2
|
||||
apply (erule (2) cte_map_inj, fastforce, fastforce, fastforce)
|
||||
apply (case_tac "(aa,bb) = ptr'")
|
||||
apply (simp add: cdt_relation_def del: split_paired_All)
|
||||
subgoal by (simp add: cdt_relation_def del: split_paired_All)
|
||||
apply (subgoal_tac "cte_map (aa,bb) \<noteq> cte_map ptr'")
|
||||
prefer 2
|
||||
apply (erule (2) cte_map_inj, fastforce, fastforce, fastforce)
|
||||
|
|
@ -987,7 +1003,7 @@ lemma cteMove_corres:
|
|||
apply (subgoal_tac "descendants_of' (cte_map (aa, bb)) (ctes_of b) =
|
||||
cte_map ` descendants_of (aa, bb) (cdt a)")
|
||||
prefer 2
|
||||
apply (simp add: cdt_relation_def del: split_paired_All)
|
||||
subgoal by (simp add: cdt_relation_def del: split_paired_All)
|
||||
apply simp
|
||||
apply (rule conjI)
|
||||
apply clarsimp
|
||||
|
|
@ -998,8 +1014,8 @@ lemma cteMove_corres:
|
|||
apply fastforce
|
||||
apply fastforce
|
||||
apply (rule subset_refl)
|
||||
apply simp
|
||||
apply simp
|
||||
subgoal by simp
|
||||
subgoal by simp
|
||||
apply clarsimp
|
||||
apply (drule (1) cte_map_inj_eq)
|
||||
apply (erule descendants_of_cte_at)
|
||||
|
|
@ -1018,7 +1034,7 @@ lemma cteMove_corres:
|
|||
apply(intro allI impI)
|
||||
apply(rule mdb_move_abs'.next_slot)
|
||||
apply(simp, fastforce, simp)
|
||||
apply(fastforce split: option.splits)
|
||||
subgoal by(fastforce split: option.splits)
|
||||
apply(case_tac "ctes_of b (cte_map (aa, bb))")
|
||||
subgoal by (clarsimp simp: modify_map_def split: if_split_asm)
|
||||
apply(case_tac ab)
|
||||
|
|
@ -5004,12 +5020,41 @@ lemma cteInsert_simple_corres:
|
|||
apply (clarsimp simp: put_def state_relation_def simp del: fun_upd_apply)
|
||||
apply (drule updateCap_stuff)
|
||||
apply clarsimp
|
||||
apply (drule (3) updateMDB_the_lot', simp, simp, elim conjE)
|
||||
apply (drule (3) updateMDB_the_lot', simp, simp, elim conjE)
|
||||
apply (drule (3) updateMDB_the_lot', simp, simp, elim conjE)
|
||||
apply (drule (3) updateMDB_the_lot', simp only: no_0_modify_map, simp only:, elim conjE)
|
||||
apply (drule (3) updateMDB_the_lot', simp only: no_0_modify_map, simp only:, elim conjE)
|
||||
apply (drule (3) updateMDB_the_lot', simp only: no_0_modify_map, simp only:, elim conjE)
|
||||
apply (clarsimp simp: pspace_relations_def)
|
||||
apply (thin_tac "gsCNodes t = p" for t p)+
|
||||
apply (thin_tac "ksMachineState t = p" for t p)+
|
||||
apply (thin_tac "ksCurThread t = p" for t p)+
|
||||
apply (thin_tac "ksWorkUnitsCompleted t = p" for t p)+
|
||||
apply (thin_tac "ksIdleThread t = p" for t p)+
|
||||
apply (thin_tac "ksReadyQueues t = p" for t p)+
|
||||
apply (thin_tac "ksSchedulerAction t = p" for t p)+
|
||||
apply (thin_tac "cur_thread t = p" for t p)+
|
||||
apply (thin_tac "domain_index t = p" for t p)+
|
||||
apply (thin_tac "domain_time t = p" for t p)+
|
||||
apply (thin_tac "cur_domain t = p" for t p)+
|
||||
apply (thin_tac "scheduler_action t = p" for t p)+
|
||||
apply (thin_tac "ready_queues t = p" for t p)+
|
||||
apply (thin_tac "idle_thread t = p" for t p)+
|
||||
apply (thin_tac "machine_state t = p" for t p)+
|
||||
apply (thin_tac "work_units_completed t = p" for t p)+
|
||||
apply (thin_tac "ksArchState t = p" for t p)+
|
||||
apply (thin_tac "gsUserPages t = p" for t p)+
|
||||
apply (thin_tac "ksCurDomain t = p" for t p)+
|
||||
apply (thin_tac "ksInterruptState t = p" for t p)+
|
||||
apply (thin_tac "ksDomScheduleIdx t = p" for t p)+
|
||||
apply (thin_tac "ksDomainTime t = p" for t p)+
|
||||
apply (thin_tac "ksDomSchedule t = p" for t p)+
|
||||
apply (thin_tac "ctes_of t = p" for t p)+
|
||||
apply (thin_tac "ekheap_relation t p" for t p)+
|
||||
apply (thin_tac "pspace_relation t p" for t p)+
|
||||
apply (thin_tac "interrupt_state_relation s t p" for s t p)+
|
||||
apply (thin_tac "sched_act_relation t p" for t p)+
|
||||
apply (thin_tac "ready_queues_relation t p" for t p)+
|
||||
apply (rule conjI)
|
||||
apply (clarsimp simp: ghost_relation_typ_at set_cap_a_type_inv data_at_def)
|
||||
subgoal by (clarsimp simp: ghost_relation_typ_at set_cap_a_type_inv data_at_def)
|
||||
apply (clarsimp simp: cte_wp_at_ctes_of nullPointer_def prev_update_modify_mdb_relation)
|
||||
apply (subgoal_tac "cte_map dest \<noteq> 0")
|
||||
prefer 2
|
||||
|
|
@ -5017,13 +5062,7 @@ lemma cteInsert_simple_corres:
|
|||
valid_mdb_ctes_def no_0_def)
|
||||
apply (subgoal_tac "cte_map src \<noteq> 0")
|
||||
prefer 2
|
||||
apply (clarsimp simp: valid_mdb'_def
|
||||
valid_mdb_ctes_def no_0_def)
|
||||
apply (thin_tac "ksMachineState t = p" for t p)+
|
||||
apply (thin_tac "ksCurThread t = p" for t p)+
|
||||
apply (thin_tac "ksIdleThread t = p" for t p)+
|
||||
apply (thin_tac "ksReadyQueues t = p" for t p)+
|
||||
apply (thin_tac "ksSchedulerAction t = p" for t p)+
|
||||
apply (clarsimp simp: valid_mdb'_def valid_mdb_ctes_def no_0_def)
|
||||
apply (subgoal_tac "should_be_parent_of src_cap (is_original_cap a src) c (is_cap_revocable c src_cap) = True")
|
||||
prefer 2
|
||||
apply (subst should_be_parent_of_masked_as_full[symmetric])
|
||||
|
|
@ -5032,7 +5071,6 @@ lemma cteInsert_simple_corres:
|
|||
apply (subst conj_assoc[symmetric])
|
||||
apply (rule conjI)
|
||||
defer
|
||||
apply (thin_tac "ctes_of t = t'" for t t')+
|
||||
apply (clarsimp simp: modify_map_apply)
|
||||
apply (clarsimp simp: revokable_relation_def simp del: fun_upd_apply)
|
||||
apply (simp split: if_split)
|
||||
|
|
@ -5047,7 +5085,7 @@ lemma cteInsert_simple_corres:
|
|||
apply (subst same_region_as_relation [symmetric])
|
||||
prefer 3
|
||||
apply (rule safe_parent_same_region)
|
||||
apply (simp add: cte_wp_at_caps_of_state safe_parent_for_masked_as_full)
|
||||
apply (simp add: cte_wp_at_caps_of_state)
|
||||
apply assumption
|
||||
apply assumption
|
||||
apply (clarsimp simp: cte_wp_at_def is_simple_cap_def)
|
||||
|
|
@ -5076,17 +5114,14 @@ lemma cteInsert_simple_corres:
|
|||
apply (rule setUntypedCapAsFull_corres)
|
||||
apply simp+
|
||||
apply (wp set_untyped_cap_full_valid_objs set_untyped_cap_as_full_valid_mdb set_untyped_cap_as_full_valid_list
|
||||
set_untyped_cap_as_full_cte_wp_at setUntypedCapAsFull_valid_cap
|
||||
setUntypedCapAsFull_cte_wp_at setUntypedCapAsFull_safe_parent_for' | clarsimp | wps)+
|
||||
set_untyped_cap_as_full_cte_wp_at setUntypedCapAsFull_valid_cap
|
||||
setUntypedCapAsFull_cte_wp_at setUntypedCapAsFull_safe_parent_for' | clarsimp | wps)+
|
||||
apply (clarsimp simp:cte_wp_at_caps_of_state )
|
||||
apply (case_tac rv',clarsimp simp:cte_wp_at_ctes_of maskedAsFull_def)
|
||||
apply (wp getCTE_wp' get_cap_wp)+
|
||||
apply clarsimp
|
||||
subgoal by (fastforce elim: cte_wp_at_weakenE)
|
||||
subgoal by (clarsimp simp: cte_wp_at'_def)
|
||||
apply (thin_tac "ctes_of s = t" for s t)+
|
||||
apply (thin_tac "pspace_relation s t" for s t)+
|
||||
apply (thin_tac "machine_state t = s" for t s)+
|
||||
apply (case_tac "srcCTE")
|
||||
apply (rename_tac src_cap' src_node)
|
||||
apply (case_tac "rv'")
|
||||
|
|
@ -5094,7 +5129,7 @@ lemma cteInsert_simple_corres:
|
|||
apply (clarsimp simp: in_set_cap_cte_at_swp)
|
||||
apply (subgoal_tac "cte_at src a \<and> safe_parent_for (cdt a) src c src_cap")
|
||||
prefer 2
|
||||
subgoal by (fastforce simp: cte_wp_at_def safe_parent_for_masked_as_full)
|
||||
subgoal by (fastforce simp: cte_wp_at_def)
|
||||
apply (erule conjE)
|
||||
|
||||
apply (subgoal_tac "mdb_insert (ctes_of b) (cte_map src) (maskedAsFull src_cap' c') src_node
|
||||
|
|
@ -5163,8 +5198,7 @@ lemma cteInsert_simple_corres:
|
|||
apply(simp)
|
||||
apply(simp add: valid_mdb'_def valid_mdb_ctes_def)
|
||||
apply(clarsimp)
|
||||
apply(drule cte_map_inj_eq)
|
||||
apply(simp_all)[6]
|
||||
subgoal by(drule cte_map_inj_eq; simp)
|
||||
apply(erule_tac x="fst src" in allE)
|
||||
apply(erule_tac x="snd src" in allE)
|
||||
apply(fastforce)
|
||||
|
|
@ -5174,12 +5208,10 @@ lemma cteInsert_simple_corres:
|
|||
apply(simp)
|
||||
apply(subgoal_tac "cte_at ca a")
|
||||
prefer 2
|
||||
apply(rule cte_at_next_slot)
|
||||
apply(simp_all)[5]
|
||||
subgoal by (rule cte_at_next_slot; simp)
|
||||
apply(clarsimp simp: modify_map_def const_def)
|
||||
apply(simp split: if_split_asm)
|
||||
apply(drule cte_map_inj_eq)
|
||||
apply(simp_all)[6]
|
||||
subgoal by (drule cte_map_inj_eq; simp)
|
||||
apply(drule_tac p="cte_map src" in valid_mdbD1')
|
||||
apply(simp)
|
||||
apply(simp add: valid_mdb'_def valid_mdb_ctes_def)
|
||||
|
|
@ -5189,12 +5221,9 @@ lemma cteInsert_simple_corres:
|
|||
apply(erule_tac x=aa in allE)
|
||||
apply(erule_tac x=bb in allE)
|
||||
apply(fastforce)
|
||||
apply(drule cte_map_inj_eq)
|
||||
apply(simp_all)[6]
|
||||
apply(drule cte_map_inj_eq)
|
||||
apply(simp_all)[6]
|
||||
apply(drule cte_map_inj_eq)
|
||||
apply(simp_all)[6]
|
||||
subgoal by (drule cte_map_inj_eq; simp)
|
||||
subgoal by (drule cte_map_inj_eq; simp)
|
||||
subgoal by (drule cte_map_inj_eq; simp)
|
||||
by(fastforce)
|
||||
|
||||
declare if_split [split]
|
||||
|
|
@ -5310,7 +5339,7 @@ lemma n_direct_eq':
|
|||
"n' \<turnstile> p \<leadsto> p' = (if p = src then p' = dest else
|
||||
if p = dest then m \<turnstile> src \<leadsto> p'
|
||||
else m \<turnstile> p \<leadsto> p')"
|
||||
by (simp add: n'_def mdb_next_modify n_direct_eq)
|
||||
by (simp add: n'_def n_direct_eq)
|
||||
|
||||
lemma dest_no_next_p:
|
||||
"m p = Some cte \<Longrightarrow> mdbNext (cteMDBNode cte) \<noteq> dest"
|
||||
|
|
|
|||
|
|
@ -786,10 +786,7 @@ lemma tcb_cte_cases_change:
|
|||
"tcb_cte_cases x = Some (getF, setF) \<Longrightarrow>
|
||||
(\<exists>getF. (\<exists>setF. tcb_cte_cases y = Some (getF, setF)) \<and> getF (setF f tcb) \<noteq> getF tcb)
|
||||
= (x = y \<and> f (getF tcb) \<noteq> getF tcb)"
|
||||
apply (rule iffI)
|
||||
apply (clarsimp simp: tcb_cte_cases_def split: if_split_asm)
|
||||
apply (clarsimp simp: tcb_cte_cases_def split: if_split_asm)
|
||||
done
|
||||
by (rule iffI; clarsimp simp: tcb_cte_cases_def split: if_split_asm) (* long *)
|
||||
|
||||
lemma cte_level_bits_nonzero [simp]: "0 < cte_level_bits"
|
||||
by (simp add: cte_level_bits_def)
|
||||
|
|
@ -924,13 +921,12 @@ lemma obj_relation_cut_same_type:
|
|||
\<or> (\<exists>sz sz'. a_type ko = AArch (ADeviceData sz) \<and> a_type ko' = AArch (ADeviceData sz'))"
|
||||
apply (rule ccontr)
|
||||
apply (simp add: obj_relation_cuts_def2 a_type_def)
|
||||
apply (auto simp: other_obj_relation_def cte_relation_def
|
||||
pte_relation_def pde_relation_def
|
||||
pdpte_relation_def pml4e_relation_def
|
||||
split: Structures_A.kernel_object.split_asm if_split_asm
|
||||
Structures_H.kernel_object.split_asm
|
||||
X64_A.arch_kernel_obj.split_asm)
|
||||
done
|
||||
by (auto simp: other_obj_relation_def cte_relation_def
|
||||
pte_relation_def pde_relation_def
|
||||
pdpte_relation_def pml4e_relation_def
|
||||
split: Structures_A.kernel_object.split_asm if_split_asm
|
||||
Structures_H.kernel_object.split_asm
|
||||
X64_A.arch_kernel_obj.split_asm)
|
||||
|
||||
definition exst_same :: "Structures_H.tcb \<Rightarrow> Structures_H.tcb \<Rightarrow> bool"
|
||||
where
|
||||
|
|
@ -977,7 +973,7 @@ lemma setObject_other_corres:
|
|||
apply (erule_tac x=ptr in allE)+
|
||||
apply (clarsimp simp: obj_at_def a_type_def
|
||||
split: Structures_A.kernel_object.splits if_split_asm)
|
||||
apply (simp split: arch_kernel_obj.splits if_splits)
|
||||
subgoal by (simp split: arch_kernel_obj.splits if_splits)
|
||||
apply (fold fun_upd_def)
|
||||
apply (simp only: pspace_relation_def pspace_dom_update dom_fun_upd2 simp_thms)
|
||||
apply (elim conjE)
|
||||
|
|
@ -996,10 +992,8 @@ lemma setObject_other_corres:
|
|||
apply (insert t,
|
||||
clarsimp simp: is_other_obj_relation_type_CapTable a_type_def)
|
||||
apply (erule disjE)
|
||||
apply (insert t,
|
||||
clarsimp simp: is_other_obj_relation_type_UserData a_type_def)
|
||||
apply (insert t,
|
||||
clarsimp simp: is_other_obj_relation_type_DeviceData a_type_def)
|
||||
apply (insert t, clarsimp simp: is_other_obj_relation_type_UserData a_type_def)
|
||||
apply (insert t, clarsimp simp: is_other_obj_relation_type_DeviceData a_type_def)
|
||||
apply (simp only: ekheap_relation_def)
|
||||
apply (rule ballI, drule(1) bspec)
|
||||
apply (drule domD)
|
||||
|
|
@ -1011,15 +1005,15 @@ lemma setObject_other_corres:
|
|||
apply (case_tac ob;
|
||||
simp_all add: a_type_def other_obj_relation_def etcb_relation_def
|
||||
is_other_obj_relation_type t exst_same_def)
|
||||
apply (clarsimp simp: is_other_obj_relation_type t exst_same_def
|
||||
split: Structures_A.kernel_object.splits Structures_H.kernel_object.splits
|
||||
X64_A.arch_kernel_obj.splits)+
|
||||
done
|
||||
by (clarsimp simp: is_other_obj_relation_type t exst_same_def
|
||||
split: Structures_A.kernel_object.splits Structures_H.kernel_object.splits
|
||||
X64_A.arch_kernel_obj.splits)+
|
||||
|
||||
lemmas obj_at_simps = obj_at_def obj_at'_def projectKOs map_to_ctes_upd_other
|
||||
is_other_obj_relation_type_def
|
||||
a_type_def objBits_simps other_obj_relation_def
|
||||
archObjSize_def pageBits_def
|
||||
|
||||
lemma setEndpoint_corres:
|
||||
"ep_relation e e' \<Longrightarrow>
|
||||
corres dc (ep_at ptr) (ep_at' ptr)
|
||||
|
|
@ -1073,8 +1067,7 @@ lemma getNotification_corres:
|
|||
|
||||
lemma setObject_ko_wp_at:
|
||||
fixes v :: "'a :: pspace_storable"
|
||||
assumes R: "\<And>ko s x y n. (updateObject v ko p y n s)
|
||||
= (updateObject_default v ko p y n s)"
|
||||
assumes R: "\<And>ko s y n. (updateObject v ko p y n s) = (updateObject_default v ko p y n s)"
|
||||
assumes n: "\<And>v' :: 'a. objBits v' = n"
|
||||
assumes m: "(1 :: machine_word) < 2 ^ n"
|
||||
shows "\<lbrace>\<lambda>s. obj_at' (\<lambda>x :: 'a. True) p s \<longrightarrow>
|
||||
|
|
@ -2172,7 +2165,6 @@ lemma doMachineOp_invs_bits[wp]:
|
|||
| wp cur_tcb_lift sch_act_wf_lift tcb_in_cur_domain'_lift
|
||||
| fastforce elim: state_refs_of'_pspaceI)+
|
||||
|
||||
crunch cte_wp_at'[wp]: doMachineOp "\<lambda>s. P (cte_wp_at' P' p s)"
|
||||
crunch obj_at'[wp]: doMachineOp "\<lambda>s. P (obj_at' P' p s)"
|
||||
|
||||
crunch it[wp]: doMachineOp "\<lambda>s. P (ksIdleThread s)"
|
||||
|
|
|
|||
Loading…
Reference in New Issue