x64: refine: CSpace_R, TcbAcc_R done
This commit is contained in:
Joel Beeren
parent
1768779b90
commit
0c011df0ef
|
|
@ -900,6 +900,7 @@ lemma set_cap_not_quite_corres':
|
|||
using cr
|
||||
apply (fastforce simp: c p pspace_relations_def)+
|
||||
done
|
||||
|
||||
context begin interpretation Arch . (*FIXME: arch_split*)
|
||||
lemma cap_move_corres:
|
||||
assumes cr: "cap_relation cap cap'"
|
||||
|
|
@ -1097,7 +1098,7 @@ lemma cap_move_corres:
|
|||
apply fastforce
|
||||
apply fastforce
|
||||
apply clarsimp
|
||||
subgoal by (simp add: null_filter_def split: if_splits)
|
||||
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
|
||||
apply (rule mdb_move.intro)
|
||||
|
|
@ -1374,7 +1375,7 @@ lemma n_trancl_eq':
|
|||
apply clarsimp
|
||||
apply (insert n_src_dest)[1]
|
||||
apply (drule (1) next_single_value)
|
||||
apply (clarsimp simp: rtrancl_eq_or_trancl)
|
||||
subgoal by (clarsimp dest!: rtrancl_eq_or_trancl[THEN iffD1])
|
||||
apply (drule m_tranclD)
|
||||
apply clarsimp
|
||||
done
|
||||
|
|
@ -1384,15 +1385,19 @@ lemma n_trancl_eq:
|
|||
(if p' = dest then p = src \<or> m \<turnstile> p \<leadsto>\<^sup>+ src
|
||||
else if p = dest then m \<turnstile> src \<leadsto>\<^sup>+ p'
|
||||
else m \<turnstile> p \<leadsto>\<^sup>+ p')"
|
||||
by (auto simp add: n_trancl_eq' rtrancl_eq_or_trancl)
|
||||
by (safe; clarsimp simp: n_trancl_eq'
|
||||
dest!: rtrancl_eq_or_trancl[THEN iffD1]
|
||||
intro!: rtrancl_eq_or_trancl[THEN iffD2])
|
||||
|
||||
lemma n_rtrancl_eq:
|
||||
"n \<turnstile> p \<leadsto>\<^sup>* p' =
|
||||
(if p' = dest then p = dest \<or> p \<noteq> dest \<and> m \<turnstile> p \<leadsto>\<^sup>* src
|
||||
else if p = dest then p' \<noteq> src \<and> m \<turnstile> src \<leadsto>\<^sup>* p'
|
||||
else m \<turnstile> p \<leadsto>\<^sup>* p')"
|
||||
by (auto simp: n_trancl_eq rtrancl_eq_or_trancl)
|
||||
|
||||
apply clarsimp
|
||||
by (safe; clarsimp simp: n_trancl_eq'
|
||||
dest!: rtrancl_eq_or_trancl[THEN iffD1]
|
||||
intro!: rtrancl_eq_or_trancl[THEN iffD2])
|
||||
|
||||
lemma n_cap:
|
||||
"n p = Some (CTE cap node) \<Longrightarrow>
|
||||
|
|
@ -1493,9 +1498,10 @@ lemma chunked_n:
|
|||
apply (rule conjI)
|
||||
apply clarsimp
|
||||
apply (erule sameRegionAsE, simp_all add: sameRegionAs_def3)[1]
|
||||
apply blast
|
||||
apply blast
|
||||
apply blast
|
||||
apply (clarsimp simp: isCap_simps)
|
||||
apply (clarsimp simp: isCap_simps)
|
||||
apply (clarsimp simp: isCap_simps portRange_def)
|
||||
apply fastforce
|
||||
apply clarsimp
|
||||
apply (erule_tac x=p'' in allE)
|
||||
|
|
@ -1826,7 +1832,9 @@ lemma untyped_inc_prev_update:
|
|||
lemma is_derived_badge_derived':
|
||||
"is_derived' m src cap cap' \<Longrightarrow> badge_derived' cap cap'"
|
||||
by (simp add: is_derived'_def)
|
||||
|
||||
context begin interpretation Arch . (*FIXME: arch_split*)
|
||||
|
||||
lemma cteInsert_mdb_chain_0:
|
||||
"\<lbrace>valid_mdb' and pspace_aligned' and pspace_distinct' and (\<lambda>s. src \<noteq> dest) and
|
||||
(\<lambda>s. cte_wp_at' (is_derived' (ctes_of s) src cap \<circ> cteCap) src s)\<rbrace>
|
||||
|
|
@ -2992,8 +3000,7 @@ crunch inQ[wp]: cteInsert "\<lambda>s. P (obj_at' (inQ d p) t s)"
|
|||
lemma setCTE_it'[wp]:
|
||||
"\<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> setCTE c p \<lbrace>\<lambda>_ s. P (ksIdleThread s)\<rbrace>"
|
||||
apply (simp add: setCTE_def setObject_def split_def updateObject_cte)
|
||||
apply (wp|wpc|simp add: unless_def)+
|
||||
done
|
||||
by (wpsimp+; auto)
|
||||
|
||||
lemma setCTE_idle [wp]:
|
||||
"\<lbrace>valid_idle'\<rbrace> setCTE p cte \<lbrace>\<lambda>rv. valid_idle'\<rbrace>"
|
||||
|
|
@ -3038,7 +3045,7 @@ lemma cteInsert_idle'[wp]:
|
|||
lemma setCTE_arch [wp]:
|
||||
"\<lbrace>\<lambda>s. P (ksArchState s)\<rbrace> setCTE p c \<lbrace>\<lambda>_ s. P (ksArchState s)\<rbrace>"
|
||||
apply (simp add: setCTE_def setObject_def split_def updateObject_cte)
|
||||
apply (wp|wpc|simp add: unless_def)+
|
||||
apply (wpsimp+; auto)
|
||||
done
|
||||
|
||||
lemma setCTE_valid_arch[wp]:
|
||||
|
|
@ -3048,13 +3055,13 @@ lemma setCTE_valid_arch[wp]:
|
|||
lemma setCTE_global_refs[wp]:
|
||||
"\<lbrace>\<lambda>s. P (global_refs' s)\<rbrace> setCTE p c \<lbrace>\<lambda>_ s. P (global_refs' s)\<rbrace>"
|
||||
apply (simp add: setCTE_def setObject_def split_def updateObject_cte global_refs'_def)
|
||||
apply (wp|wpc|simp add: unless_def)+
|
||||
apply (wpsimp+; auto)
|
||||
done
|
||||
|
||||
lemma setCTE_gsMaxObjectSize[wp]:
|
||||
"\<lbrace>\<lambda>s. P (gsMaxObjectSize s)\<rbrace> setCTE p c \<lbrace>\<lambda>_ s. P (gsMaxObjectSize s)\<rbrace>"
|
||||
apply (simp add: setCTE_def setObject_def split_def updateObject_cte)
|
||||
apply (wp|wpc|simp add: unless_def)+
|
||||
apply (wpsimp+; auto)
|
||||
done
|
||||
|
||||
lemma setCTE_valid_globals[wp]:
|
||||
|
|
@ -4089,11 +4096,11 @@ lemma create_reply_master_corres:
|
|||
done
|
||||
|
||||
lemma cte_map_nat_to_cref:
|
||||
"\<lbrakk> n < 2 ^ b; b < 32 \<rbrakk> \<Longrightarrow>
|
||||
cte_map (p, nat_to_cref b n) = p + (of_nat n * 16)"
|
||||
"\<lbrakk> n < 2 ^ b; b < 64 \<rbrakk> \<Longrightarrow>
|
||||
cte_map (p, nat_to_cref b n) = p + (of_nat n * 32)"
|
||||
apply (clarsimp simp: cte_map_def nat_to_cref_def
|
||||
dest!: less_is_drop_replicate)
|
||||
apply (rule arg_cong [where f="\<lambda>x. x * 16"])
|
||||
apply (rule arg_cong [where f="\<lambda>x. x * 32"])
|
||||
apply (subst of_drop_to_bl)
|
||||
apply (simp add: word_bits_def)
|
||||
apply (subst mask_eq_iff_w2p)
|
||||
|
|
@ -4181,7 +4188,7 @@ lemma setup_reply_master_corres:
|
|||
apply (simp add: setupReplyMaster_def setup_reply_master_def)
|
||||
apply (simp add: locateSlot_conv tcbReplySlot_def objBits_def objBitsKO_def)
|
||||
apply (simp add: nullMDBNode_def, fold initMDBNode_def)
|
||||
apply (rule_tac F="t + 0x20 = cte_map (t, tcb_cnode_index 2)"
|
||||
apply (rule_tac F="t + 0x40 = cte_map (t, tcb_cnode_index 2)"
|
||||
in corres_req)
|
||||
apply (clarsimp simp: tcb_cnode_index_def2 cte_map_nat_to_cref)
|
||||
apply (clarsimp simp: cte_level_bits_def)
|
||||
|
|
@ -4488,7 +4495,10 @@ lemma mdb_next_trans_next_pres:
|
|||
lemma mdb_next_rtrans_next_pres:
|
||||
"\<lbrakk> m p = Some v; mdbNext (cteMDBNode x) = mdbNext (cteMDBNode v) \<rbrakk> \<Longrightarrow>
|
||||
m(p \<mapsto> x) \<turnstile> a \<leadsto>\<^sup>* b = m \<turnstile> a \<leadsto>\<^sup>* b"
|
||||
by (simp add: rtrancl_eq_or_trancl mdb_next_trans_next_pres)
|
||||
by (safe; clarsimp simp: mdb_next_trans_next_pres
|
||||
dest!: rtrancl_eq_or_trancl[THEN iffD1]
|
||||
intro!: rtrancl_eq_or_trancl[THEN iffD2] mdb_next_trans_next_pres[THEN iffD1])
|
||||
|
||||
|
||||
lemma arch_update_descendants':
|
||||
"\<lbrakk> is_arch_update' cap oldcte; m p = Some oldcte\<rbrakk> \<Longrightarrow>
|
||||
|
|
@ -4731,7 +4741,8 @@ definition
|
|||
\<not> isThreadCap cap \<and>
|
||||
\<not> isCNodeCap cap \<and>
|
||||
\<not> isZombie cap \<and>
|
||||
\<not> isArchPageCap cap"
|
||||
\<not> isArchPageCap cap \<and>
|
||||
\<not> isArchIOPortCap cap"
|
||||
end
|
||||
|
||||
(* FIXME: duplicated *)
|
||||
|
|
@ -4940,7 +4951,9 @@ done
|
|||
lemma is_simple_cap'_maskedAsFull[simp]:
|
||||
"is_simple_cap' (maskedAsFull src_cap' c') = is_simple_cap' src_cap'"
|
||||
by (auto simp: is_simple_cap'_def maskedAsFull_def isCap_simps split:if_splits)
|
||||
|
||||
context begin interpretation Arch . (*FIXME: arch_split*)
|
||||
|
||||
lemma cins_corres_simple:
|
||||
assumes "cap_relation c c'" "src' = cte_map src" "dest' = cte_map dest"
|
||||
notes trans_state_update'[symmetric,simp]
|
||||
|
|
@ -5215,14 +5228,20 @@ lemma cins_corres_simple:
|
|||
|
||||
declare if_split [split]
|
||||
|
||||
lemma capMaster_portRange:
|
||||
"capMasterCap c = capMasterCap c' \<Longrightarrow> portRange c = portRange c'"
|
||||
by (simp add: capMasterCap_def portRange_def isCap_simps split: capability.splits arch_capability.splits)
|
||||
|
||||
lemma sameRegion_capRange_sub:
|
||||
"sameRegionAs cap cap' \<Longrightarrow> capRange cap' \<subseteq> capRange cap"
|
||||
apply (clarsimp simp: sameRegionAs_def2 isCap_Master capRange_Master)
|
||||
apply (erule disjE)
|
||||
apply (clarsimp dest!: capMaster_capRange)
|
||||
apply (clarsimp dest!: capMaster_capRange simp: portRange_def)
|
||||
apply (erule disjE)
|
||||
apply fastforce
|
||||
apply (clarsimp simp: isCap_simps capRange_def)
|
||||
apply (erule disjE)
|
||||
apply (clarsimp simp: isCap_simps portRange_def capRange_def)
|
||||
apply (clarsimp simp: isCap_simps capRange_def portRange_def)
|
||||
done
|
||||
|
||||
lemma safe_parent_for_capRange_capBits:
|
||||
|
|
@ -5741,8 +5760,10 @@ lemma sameRegion_c_src':
|
|||
prefer 2
|
||||
apply clarsimp
|
||||
apply (erule disjE, blast)
|
||||
apply (erule disjE, clarsimp simp: isCap_simps portRange_def split: if_split_asm;
|
||||
clarsimp simp: capRange_def)
|
||||
apply (clarsimp simp: isCap_simps)
|
||||
apply (clarsimp simp: capRange_def)
|
||||
apply (clarsimp simp: capRange_def portRange_def isCap_simps split: if_split_asm)
|
||||
apply (elim conjE)
|
||||
apply (drule capMaster_capRange)
|
||||
apply simp
|
||||
|
|
@ -5996,6 +6017,11 @@ lemma notArchPage:
|
|||
using simple
|
||||
by (clarsimp simp: isCap_simps is_simple_cap'_def)
|
||||
|
||||
lemma notArchIOPort:
|
||||
"\<not> isArchIOPortCap c'"
|
||||
using simple
|
||||
by (clarsimp simp: isCap_simps is_simple_cap'_def)
|
||||
|
||||
lemma distinct_zombies[simp]:
|
||||
"distinct_zombies n'"
|
||||
using distinct_zombies_m
|
||||
|
|
@ -6011,10 +6037,12 @@ lemma distinct_zombies[simp]:
|
|||
apply (frule(3) untyped_rangefree)
|
||||
apply (simp add: capRange_def)
|
||||
apply (rule sameRegionAsE [OF sameRegion_src], simp_all)
|
||||
apply (erule distinct_zombies_copyMasterE, rule src)
|
||||
apply simp
|
||||
apply (simp add: notZomb)
|
||||
apply (simp add: notArchPage)
|
||||
apply (erule distinct_zombies_copyMasterE, rule src)
|
||||
apply simp
|
||||
apply (simp add: notZomb)
|
||||
apply (simp add: notArchPage)
|
||||
apply (simp add: notArchIOPort)
|
||||
apply (clarsimp simp: isCap_simps)
|
||||
apply (erule distinct_zombies_sameMasterE, rule dest)
|
||||
apply (clarsimp simp: isCap_simps)
|
||||
done
|
||||
|
|
@ -6087,7 +6115,9 @@ setUntypedCapAsFull (cteCap srcCTE) cap src
|
|||
apply wp
|
||||
apply clarsimp
|
||||
done
|
||||
|
||||
context begin interpretation Arch . (*FIXME: arch_split*)
|
||||
|
||||
lemma cteInsert_simple_mdb':
|
||||
"\<lbrace>valid_mdb' and pspace_aligned' and pspace_distinct' and (\<lambda>s. src \<noteq> dest) and K (capAligned cap) and
|
||||
(\<lambda>s. safe_parent_for' (ctes_of s) src cap) and K (is_simple_cap' cap) \<rbrace>
|
||||
|
|
@ -6183,7 +6213,7 @@ lemma cte_refs_maskCapRights[simp]:
|
|||
split: arch_capability.split)
|
||||
|
||||
lemma capASID_PageCap_None [simp]:
|
||||
"capASID (ArchObjectCap (PageCap d r R page_size None)) = None"
|
||||
"capASID (ArchObjectCap (PageCap r R mt page_size d None)) = None"
|
||||
by (simp add: capASID_def)
|
||||
|
||||
lemma getSlotCap_cap_to'[wp]:
|
||||
|
|
@ -6498,7 +6528,7 @@ lemma usableUntypedRange_mono2:
|
|||
|
||||
lemma updateFreeIndex_pspace':
|
||||
"\<lbrace>\<lambda>s. (capFreeIndex cap \<le> idx \<and> idx \<le> 2 ^ capBlockSize cap \<and>
|
||||
is_aligned (of_nat idx :: word32) 4 \<and> isUntypedCap cap) \<and>
|
||||
is_aligned (of_nat idx :: machine_word) 4 \<and> isUntypedCap cap) \<and>
|
||||
valid_pspace' s \<and> cte_wp_at' (\<lambda>c. cteCap c = cap) src s\<rbrace>
|
||||
updateCap src (capFreeIndex_update (\<lambda>_. idx) cap)
|
||||
\<lbrace>\<lambda>r s. valid_pspace' s\<rbrace>"
|
||||
|
|
@ -6537,7 +6567,7 @@ lemma ctes_of_cte_wpD:
|
|||
lemma updateFreeIndex_forward_valid_objs':
|
||||
"\<lbrace>\<lambda>s. valid_objs' s \<and> cte_wp_at' ((\<lambda>cap. isUntypedCap cap
|
||||
\<and> capFreeIndex cap \<le> idx \<and> idx \<le> 2 ^ capBlockSize cap
|
||||
\<and> is_aligned (of_nat idx :: word32) 4) o cteCap) src s\<rbrace>
|
||||
\<and> is_aligned (of_nat idx :: machine_word) 4) o cteCap) src s\<rbrace>
|
||||
updateFreeIndex src idx
|
||||
\<lbrace>\<lambda>r s. valid_objs' s\<rbrace>"
|
||||
apply (simp add: updateFreeIndex_def updateTrackedFreeIndex_def updateCap_def getSlotCap_def)
|
||||
|
|
@ -6576,7 +6606,7 @@ lemma updateFreeIndex_forward_valid_mdb':
|
|||
lemma updateFreeIndex_forward_invs':
|
||||
"\<lbrace>\<lambda>s. invs' s \<and> cte_wp_at' ((\<lambda>cap. isUntypedCap cap
|
||||
\<and> capFreeIndex cap \<le> idx \<and> idx \<le> 2 ^ capBlockSize cap
|
||||
\<and> is_aligned (of_nat idx :: word32) 4) o cteCap) src s\<rbrace>
|
||||
\<and> is_aligned (of_nat idx :: machine_word) 4) o cteCap) src s\<rbrace>
|
||||
updateFreeIndex src idx
|
||||
\<lbrace>\<lambda>r s. invs' s\<rbrace>"
|
||||
apply (clarsimp simp:invs'_def valid_state'_def)
|
||||
|
|
|
|||
|
|
@ -36,7 +36,7 @@ lemmas bitmap_fun_defs = addToBitmap_def removeFromBitmap_def
|
|||
|
||||
definition
|
||||
(* when in the middle of updates, a particular queue might not be entirely valid *)
|
||||
valid_queues_no_bitmap_except :: "word32 \<Rightarrow> kernel_state \<Rightarrow> bool"
|
||||
valid_queues_no_bitmap_except :: "machine_word \<Rightarrow> kernel_state \<Rightarrow> bool"
|
||||
where
|
||||
"valid_queues_no_bitmap_except t' \<equiv> \<lambda>s.
|
||||
(\<forall>d p. (\<forall>t \<in> set (ksReadyQueues s (d, p)). t \<noteq> t' \<longrightarrow> obj_at' (inQ d p and runnable' \<circ> tcbState) t s)
|
||||
|
|
@ -145,7 +145,7 @@ lemma doMachineOp_irq_states':
|
|||
apply wp
|
||||
apply clarsimp
|
||||
apply (drule use_valid)
|
||||
apply (rule_tac P="\<lambda>m. m = irq_masks (ksMachineState s)" in masks)
|
||||
apply (rule_tac P1="\<lambda>m. m = irq_masks (ksMachineState s)" in masks)
|
||||
apply simp
|
||||
apply simp
|
||||
done
|
||||
|
|
@ -161,7 +161,7 @@ lemma dmo_invs':
|
|||
apply clarsimp
|
||||
apply (subst invs'_machine)
|
||||
apply (drule use_valid)
|
||||
apply (rule_tac P="\<lambda>m. m = irq_masks (ksMachineState s)" in masks, simp+)
|
||||
apply (rule_tac P1="\<lambda>m. m = irq_masks (ksMachineState s)" in masks, simp+)
|
||||
apply (fastforce simp add: valid_machine_state'_def)
|
||||
apply assumption
|
||||
done
|
||||
|
|
@ -177,7 +177,7 @@ lemma dmo_invs_no_cicd':
|
|||
apply clarsimp
|
||||
apply (subst invs_no_cicd'_machine)
|
||||
apply (drule use_valid)
|
||||
apply (rule_tac P="\<lambda>m. m = irq_masks (ksMachineState s)" in masks, simp+)
|
||||
apply (rule_tac P1="\<lambda>m. m = irq_masks (ksMachineState s)" in masks, simp+)
|
||||
apply (fastforce simp add: valid_machine_state'_def)
|
||||
apply assumption
|
||||
done
|
||||
|
|
@ -390,7 +390,7 @@ proof -
|
|||
apply (rule e)
|
||||
apply (rule corres_noop [where P=\<top> and P'=\<top>])
|
||||
apply simp
|
||||
apply (rule no_fail_pre, wp)[1]
|
||||
apply (rule no_fail_pre, wpsimp+)[1]
|
||||
apply wp+
|
||||
apply simp
|
||||
apply (erule pspace_relation_tcb_at[rotated])
|
||||
|
|
@ -922,8 +922,8 @@ lemma threadSet_valid_queues:
|
|||
|
||||
definition
|
||||
addToQs :: "(Structures_H.tcb \<Rightarrow> Structures_H.tcb)
|
||||
\<Rightarrow> word32 \<Rightarrow> (domain \<times> priority \<Rightarrow> word32 list)
|
||||
\<Rightarrow> (domain \<times> priority \<Rightarrow> word32 list)"
|
||||
\<Rightarrow> machine_word \<Rightarrow> (domain \<times> priority \<Rightarrow> machine_word list)
|
||||
\<Rightarrow> (domain \<times> priority \<Rightarrow> machine_word list)"
|
||||
where
|
||||
"addToQs F t \<equiv> \<lambda>qs (qdom, prio). if (\<forall>ko. \<not> inQ qdom prio (F ko))
|
||||
then t # qs (qdom, prio)
|
||||
|
|
@ -1785,7 +1785,7 @@ lemma no_fail_setQueue [wp]:
|
|||
by (simp add: setQueue_def)
|
||||
|
||||
lemma in_magnitude_check':
|
||||
"\<lbrakk> is_aligned x n; (1 :: word32) < 2 ^ n; ksPSpace s x = Some y; ps = ksPSpace s \<rbrakk>
|
||||
"\<lbrakk> is_aligned x n; (1 :: machine_word) < 2 ^ n; ksPSpace s x = Some y; ps = ksPSpace s \<rbrakk>
|
||||
\<Longrightarrow> ((v, s') \<in> fst (magnitudeCheck x (snd (lookupAround2 x ps)) n s)) =
|
||||
(s' = s \<and> ps_clear x n s)"
|
||||
by (simp add: in_magnitude_check)
|
||||
|
|
@ -2719,13 +2719,13 @@ lemma prioToL1Index_max:
|
|||
by (insert unat_lt2p[where x=p], simp add: shiftr_div_2n')
|
||||
|
||||
lemma prioToL1Index_bit_set:
|
||||
"((2 :: 32 word) ^ prioToL1Index p) !! prioToL1Index p"
|
||||
"((2 :: machine_word) ^ prioToL1Index p) !! prioToL1Index p"
|
||||
using prioToL1Index_max[simplified wordRadix_def]
|
||||
by (fastforce simp: nth_w2p_same)
|
||||
|
||||
lemma prioL2Index_bit_set:
|
||||
fixes p :: priority
|
||||
shows "((2::32 word) ^ unat (ucast p && (mask wordRadix :: machine_word))) !! unat (p && mask wordRadix)"
|
||||
shows "((2::machine_word) ^ unat (ucast p && (mask wordRadix :: machine_word))) !! unat (p && mask wordRadix)"
|
||||
apply (simp add: nth_w2p wordRadix_def ucast_and_mask[symmetric] unat_ucast_upcast is_up)
|
||||
apply (rule unat_less_helper)
|
||||
apply (insert and_mask_less'[where w=p and n=wordRadix], simp add: wordRadix_def)
|
||||
|
|
@ -3451,15 +3451,15 @@ lemma tcbSchedDequeue_ksQ:
|
|||
lemma valid_ipc_buffer_ptr'D:
|
||||
assumes yv: "y < unat max_ipc_words"
|
||||
and buf: "valid_ipc_buffer_ptr' a s"
|
||||
shows "pointerInUserData (a + of_nat y * 4) s"
|
||||
shows "pointerInUserData (a + of_nat y * 8) s"
|
||||
using buf unfolding valid_ipc_buffer_ptr'_def pointerInUserData_def
|
||||
apply clarsimp
|
||||
apply (subgoal_tac
|
||||
"(a + of_nat y * 4) && ~~ mask pageBits = a && ~~ mask pageBits")
|
||||
"(a + of_nat y * 8) && ~~ mask pageBits = a && ~~ mask pageBits")
|
||||
apply simp
|
||||
apply (rule mask_out_first_mask_some [where n = msg_align_bits])
|
||||
apply (erule is_aligned_add_helper [THEN conjunct2])
|
||||
apply (rule word_less_power_trans_ofnat [where k = 2, simplified])
|
||||
apply (rule word_less_power_trans_ofnat [where k = 3, simplified])
|
||||
apply (rule order_less_le_trans [OF yv])
|
||||
apply (simp add: msg_align_bits max_ipc_words)
|
||||
apply (simp add: msg_align_bits)
|
||||
|
|
@ -3469,18 +3469,18 @@ lemma valid_ipc_buffer_ptr'D:
|
|||
lemma in_user_frame_eq:
|
||||
assumes y: "y < unat max_ipc_words"
|
||||
and al: "is_aligned a msg_align_bits"
|
||||
shows "in_user_frame (a + of_nat y * 4) s = in_user_frame a s"
|
||||
shows "in_user_frame (a + of_nat y * 8) s = in_user_frame a s"
|
||||
proof -
|
||||
have "\<And>sz. (a + of_nat y * 4) && ~~ mask (pageBitsForSize sz) =
|
||||
have "\<And>sz. (a + of_nat y * 8) && ~~ mask (pageBitsForSize sz) =
|
||||
a && ~~ mask (pageBitsForSize sz)"
|
||||
apply (rule mask_out_first_mask_some [where n = msg_align_bits])
|
||||
apply (rule is_aligned_add_helper [OF al, THEN conjunct2])
|
||||
apply (rule word_less_power_trans_ofnat [where k = 2, simplified])
|
||||
apply (rule word_less_power_trans_ofnat [where k = 3, simplified])
|
||||
apply (rule order_less_le_trans [OF y])
|
||||
apply (simp add: msg_align_bits max_ipc_words)
|
||||
apply (simp add: msg_align_bits)
|
||||
apply (simp add: msg_align_bits pageBits_def)
|
||||
apply (case_tac sz, simp_all add: msg_align_bits)
|
||||
apply (case_tac sz, simp_all add: msg_align_bits bit_simps)
|
||||
done
|
||||
|
||||
thus ?thesis by (simp add: in_user_frame_def)
|
||||
|
|
@ -3488,7 +3488,7 @@ qed
|
|||
|
||||
lemma load_word_offs_corres:
|
||||
assumes y: "y < unat max_ipc_words"
|
||||
shows "corres op = \<top> (valid_ipc_buffer_ptr' a) (load_word_offs a y) (loadWordUser (a + of_nat y * 4))"
|
||||
shows "corres op = \<top> (valid_ipc_buffer_ptr' a) (load_word_offs a y) (loadWordUser (a + of_nat y * 8))"
|
||||
unfolding loadWordUser_def
|
||||
apply (rule corres_stateAssert_assume [rotated])
|
||||
apply (erule valid_ipc_buffer_ptr'D[OF y])
|
||||
|
|
@ -3500,7 +3500,7 @@ lemma load_word_offs_corres:
|
|||
apply (rule no_fail_pre)
|
||||
apply wp
|
||||
apply (erule aligned_add_aligned)
|
||||
apply (rule is_aligned_mult_triv2 [where n = 2, simplified])
|
||||
apply (rule is_aligned_mult_triv2 [where n = 3, simplified])
|
||||
apply (simp add: word_bits_conv msg_align_bits)+
|
||||
apply (simp add: valid_ipc_buffer_ptr'_def msg_align_bits)
|
||||
done
|
||||
|
|
@ -3508,7 +3508,7 @@ lemma load_word_offs_corres:
|
|||
lemma store_word_offs_corres:
|
||||
assumes y: "y < unat max_ipc_words"
|
||||
shows "corres dc (in_user_frame a) (valid_ipc_buffer_ptr' a)
|
||||
(store_word_offs a y w) (storeWordUser (a + of_nat y * 4) w)"
|
||||
(store_word_offs a y w) (storeWordUser (a + of_nat y * 8) w)"
|
||||
apply (simp add: storeWordUser_def bind_assoc[symmetric]
|
||||
store_word_offs_def word_size_def)
|
||||
apply (rule corres_guard2_imp)
|
||||
|
|
@ -3521,7 +3521,7 @@ lemma store_word_offs_corres:
|
|||
apply (rule no_fail_pre)
|
||||
apply (wp no_fail_storeWord)
|
||||
apply (erule_tac n=msg_align_bits in aligned_add_aligned)
|
||||
apply (rule is_aligned_mult_triv2 [where n = 2, simplified])
|
||||
apply (rule is_aligned_mult_triv2 [where n = 3, simplified])
|
||||
apply (simp add: word_bits_conv msg_align_bits)+
|
||||
apply (simp add: stateAssert_def)
|
||||
apply (rule_tac r'=dc in corres_split)
|
||||
|
|
@ -3538,7 +3538,7 @@ lemma store_word_offs_corres:
|
|||
|
||||
lemma load_word_corres:
|
||||
"corres op= \<top>
|
||||
(typ_at' UserDataT (a && ~~ mask pageBits) and (\<lambda>s. is_aligned a 2))
|
||||
(typ_at' UserDataT (a && ~~ mask pageBits) and (\<lambda>s. is_aligned a word_size_bits))
|
||||
(do_machine_op (loadWord a)) (loadWordUser a)"
|
||||
unfolding loadWordUser_def
|
||||
apply (rule corres_gen_asm2)
|
||||
|
|
@ -3549,15 +3549,12 @@ lemma load_word_corres:
|
|||
apply (rule corres_machine_op)
|
||||
apply (rule corres_Id [OF refl refl])
|
||||
apply (rule no_fail_pre)
|
||||
apply wp
|
||||
apply assumption
|
||||
apply simp
|
||||
apply simp
|
||||
apply (wpsimp simp: word_size_bits_def)+
|
||||
done
|
||||
|
||||
lemma store_word_corres:
|
||||
"corres dc \<top>
|
||||
(typ_at' UserDataT (a && ~~ mask pageBits) and (\<lambda>s. is_aligned a 2))
|
||||
(typ_at' UserDataT (a && ~~ mask pageBits) and (\<lambda>s. is_aligned a word_size_bits))
|
||||
(do_machine_op (storeWord a w)) (storeWordUser a w)"
|
||||
unfolding storeWordUser_def
|
||||
apply (rule corres_gen_asm2)
|
||||
|
|
@ -3569,16 +3566,13 @@ lemma store_word_corres:
|
|||
apply (rule corres_Id [OF refl])
|
||||
apply simp
|
||||
apply (rule no_fail_pre)
|
||||
apply (wp no_fail_storeWord)
|
||||
apply assumption
|
||||
apply simp
|
||||
apply simp
|
||||
apply (wpsimp wp: no_fail_storeWord simp: word_size_bits_def)+
|
||||
done
|
||||
|
||||
lemmas msgRegisters_unfold
|
||||
= X64_H.msgRegisters_def
|
||||
msg_registers_def
|
||||
ARM.msgRegisters_def
|
||||
X64.msgRegisters_def
|
||||
[unfolded upto_enum_def, simplified,
|
||||
unfolded fromEnum_def enum_register, simplified,
|
||||
unfolded toEnum_def enum_register, simplified]
|
||||
|
|
@ -3702,10 +3696,6 @@ proof -
|
|||
have S: "\<And>xs ys n m. m - n \<ge> length xs \<Longrightarrow> (zip xs (drop n (take m ys))) = zip xs (drop n ys)"
|
||||
by (simp add: zip_take_triv2 drop_take)
|
||||
|
||||
have upto_enum_nth_assist4:
|
||||
"\<And>i. i < 116 \<Longrightarrow> [(5::machine_word).e.0x78] ! i * 4 = 0x14 + of_nat i * 4"
|
||||
by (subst upto_enum_word, subst upt_lhs_sub_map, simp)
|
||||
|
||||
note upt.simps[simp del] upt_rec_numeral[simp del]
|
||||
|
||||
show ?thesis using m
|
||||
|
|
@ -3734,7 +3724,7 @@ proof -
|
|||
apply (rule corres_guard_imp)
|
||||
apply (rule corres_split_nor [OF _ corres_as_user'])
|
||||
apply (rule corres_split_nor, rule corres_trivial, clarsimp simp: min.commute)
|
||||
apply (rule_tac S="{((x, y), (x', y')). y = y' \<and> x' = (a + (of_nat x * 4)) \<and> x < unat max_ipc_words}"
|
||||
apply (rule_tac S="{((x, y), (x', y')). y = y' \<and> x' = (a + (of_nat x * 8)) \<and> x < unat max_ipc_words}"
|
||||
in zipWithM_x_corres)
|
||||
apply (fastforce intro: store_word_offs_corres)
|
||||
apply wp+
|
||||
|
|
@ -3761,13 +3751,13 @@ lemma copy_mrs_corres:
|
|||
(copy_mrs s sb r rb n) (copyMRs s sb r rb n)"
|
||||
proof -
|
||||
have U: "unat n \<le> msg_max_length \<Longrightarrow>
|
||||
map (toEnum :: nat \<Rightarrow> word32) [7 ..< Suc (unat n)] = map of_nat [7 ..< Suc (unat n)]"
|
||||
map (toEnum :: nat \<Rightarrow> machine_word) [7 ..< Suc (unat n)] = map of_nat [7 ..< Suc (unat n)]"
|
||||
unfolding msg_max_length_def by auto
|
||||
note R'=msgRegisters_unfold[THEN meta_eq_to_obj_eq, THEN arg_cong[where f=length]]
|
||||
note R=R'[simplified]
|
||||
|
||||
have as_user_bit:
|
||||
"\<And>v :: word32. corres dc (tcb_at s and tcb_at r) (tcb_at' s and tcb_at' r)
|
||||
"\<And>v :: machine_word. corres dc (tcb_at s and tcb_at r) (tcb_at' s and tcb_at' r)
|
||||
(mapM
|
||||
(\<lambda>ra. do v \<leftarrow> as_user s (get_register ra);
|
||||
as_user r (set_register ra v)
|
||||
|
|
@ -3784,7 +3774,7 @@ proof -
|
|||
apply (wp | clarsimp simp: msg_registers_def msgRegisters_def)+
|
||||
done
|
||||
|
||||
have wordSize[simp]: "of_nat wordSize = 4"
|
||||
have wordSize[simp]: "of_nat wordSize = 8"
|
||||
by (simp add: wordSize_def wordBits_def word_size)
|
||||
|
||||
show ?thesis
|
||||
|
|
@ -3835,10 +3825,10 @@ proof -
|
|||
done
|
||||
qed
|
||||
|
||||
lemma cte_at_tcb_at_16':
|
||||
"tcb_at' t s \<Longrightarrow> cte_at' (t + 16) s"
|
||||
lemma cte_at_tcb_at_32':
|
||||
"tcb_at' t s \<Longrightarrow> cte_at' (t + 32) s"
|
||||
apply (simp add: cte_at'_obj_at')
|
||||
apply (rule disjI2, rule bexI[where x=16])
|
||||
apply (rule disjI2, rule bexI[where x=32])
|
||||
apply simp
|
||||
apply fastforce
|
||||
done
|
||||
|
|
@ -3888,7 +3878,7 @@ lemma pspace_dom_dom:
|
|||
apply (rule range_eqI [where x = 0], simp)+
|
||||
apply (rename_tac vmpage_size)
|
||||
apply (rule exI [where x = 0])
|
||||
apply (case_tac vmpage_size, simp_all add: pageBits_def)
|
||||
apply (case_tac vmpage_size, simp_all add: bit_simps)
|
||||
done
|
||||
|
||||
lemma no_0_obj_kheap:
|
||||
|
|
@ -3919,33 +3909,34 @@ lemma lipcb_corres':
|
|||
apply (simp add: getThreadBufferSlot_def locateSlot_conv)
|
||||
apply (rule corres_split [OF _ getSlotCap_corres])
|
||||
apply (rule_tac F="valid_ipc_buffer_cap rv buffer_ptr"
|
||||
in corres_gen_asm)
|
||||
in corres_gen_asm)
|
||||
apply (rule_tac P="valid_cap rv" and Q="no_0_obj'"
|
||||
in corres_assume_pre)
|
||||
in corres_assume_pre)
|
||||
apply (simp add: Let_def split: cap.split arch_cap.split
|
||||
split del: if_split cong: if_cong)
|
||||
split del: if_split cong: if_cong)
|
||||
apply (safe, simp_all add: isCap_simps valid_ipc_buffer_cap_simps split:bool.split_asm)[1]
|
||||
apply (rename_tac word rights vmpage_size option)
|
||||
apply (rename_tac word rights mt vmpage_size option)
|
||||
apply (subgoal_tac "word + (buffer_ptr &&
|
||||
mask (pageBitsForSize vmpage_size)) \<noteq> 0")
|
||||
apply (simp add: cap_aligned_def
|
||||
valid_ipc_buffer_cap_def
|
||||
vmrights_map_def vm_read_only_def vm_read_write_def)
|
||||
apply auto[1]
|
||||
apply auto[1]
|
||||
apply (subgoal_tac "word \<noteq> 0")
|
||||
apply (subgoal_tac "word \<le> word + (buffer_ptr &&
|
||||
mask (pageBitsForSize vmpage_size))")
|
||||
apply fastforce
|
||||
apply (rule_tac b="2 ^ (pageBitsForSize vmpage_size) - 1"
|
||||
in word_plus_mono_right2)
|
||||
in word_plus_mono_right2)
|
||||
apply (clarsimp simp: valid_cap_def cap_aligned_def
|
||||
intro!: is_aligned_no_overflow')
|
||||
apply (clarsimp simp: word_bits_def
|
||||
apply (clarsimp simp: word_bits_def bit_simps
|
||||
intro!: word_less_sub_1 and_mask_less')
|
||||
apply (case_tac vmpage_size, simp_all)[1]
|
||||
apply (drule state_relation_pspace_relation)
|
||||
apply (clarsimp simp: valid_cap_def obj_at_def no_0_obj_kheap
|
||||
obj_relation_cuts_def3 no_0_obj'_def split:if_split_asm)
|
||||
apply (case_tac vmpage_size, simp_all add: bit_simps)[1]
|
||||
apply (drule state_relation_pspace_relation)
|
||||
apply (clarsimp simp: valid_cap_def obj_at_def no_0_obj_kheap
|
||||
obj_relation_cuts_def3 no_0_obj'_def
|
||||
split: if_split_asm)
|
||||
apply (simp add: cte_map_def tcb_cnode_index_def cte_level_bits_def tcbIPCBufferSlot_def)
|
||||
apply (wp get_cap_valid_ipc get_cap_aligned)+
|
||||
apply (simp add: tcb_relation_def)
|
||||
|
|
@ -3963,6 +3954,7 @@ lemma lipcb_corres:
|
|||
|
||||
|
||||
crunch inv'[wp]: lookupIPCBuffer P
|
||||
(wp: crunch_wps simp: crunch_simps)
|
||||
|
||||
crunch pred_tcb_at'[wp]: rescheduleRequired "pred_tcb_at' proj P t"
|
||||
(wp: threadSet_pred_tcb_no_state simp: unless_def ignore: threadSet)
|
||||
|
|
@ -4849,23 +4841,23 @@ lemma storeWord_invs'[wp]:
|
|||
"\<lbrace>pointerInUserData p and invs'\<rbrace> doMachineOp (storeWord p w) \<lbrace>\<lambda>rv. invs'\<rbrace>"
|
||||
proof -
|
||||
have aligned_offset_ignore:
|
||||
"\<And>l. l<4 \<Longrightarrow> p && mask 2 = 0 \<Longrightarrow> p + l && ~~ mask 12 = p && ~~ mask 12"
|
||||
"\<And>l. l<8 \<Longrightarrow> p && mask word_size_bits = 0 \<Longrightarrow> p + l && ~~ mask 12 = p && ~~ mask 12"
|
||||
proof -
|
||||
fix l
|
||||
assume al: "p && mask 2 = 0"
|
||||
assume "(l::word32) < 4" hence less: "l<2^2" by simp
|
||||
have le: "(2::nat) \<le> 12" by simp
|
||||
assume al: "p && mask word_size_bits = 0"
|
||||
assume "(l::machine_word) < 8" hence less: "l<2^word_size_bits" by (simp add: word_size_bits_def)
|
||||
have le: "(word_size_bits::nat) \<le> 12" by (simp add: word_size_bits_def)
|
||||
show "?thesis l"
|
||||
by (rule is_aligned_add_helper[simplified is_aligned_mask,
|
||||
THEN conjunct2, THEN mask_out_first_mask_some, OF al less le])
|
||||
qed
|
||||
|
||||
show ?thesis
|
||||
apply (wp dmo_invs' no_irq_storeWord no_irq)
|
||||
apply_trace (wp dmo_invs' no_irq_storeWord no_irq)
|
||||
apply (clarsimp simp: storeWord_def invs'_def valid_state'_def)
|
||||
apply (clarsimp simp: valid_machine_state'_def pointerInUserData_def
|
||||
assert_def simpler_modify_def fail_def bind_def return_def
|
||||
pageBits_def aligned_offset_ignore
|
||||
pageBits_def aligned_offset_ignore bit_simps upto0_7_def
|
||||
split: if_split_asm)
|
||||
done
|
||||
qed
|
||||
|
|
@ -4874,12 +4866,12 @@ lemma storeWord_invs_no_cicd'[wp]:
|
|||
"\<lbrace>pointerInUserData p and invs_no_cicd'\<rbrace> doMachineOp (storeWord p w) \<lbrace>\<lambda>rv. invs_no_cicd'\<rbrace>"
|
||||
proof -
|
||||
have aligned_offset_ignore:
|
||||
"\<And>l. l<4 \<Longrightarrow> p && mask 2 = 0 \<Longrightarrow> p + l && ~~ mask 12 = p && ~~ mask 12"
|
||||
"\<And>l. l<8 \<Longrightarrow> p && mask 3 = 0 \<Longrightarrow> p + l && ~~ mask 12 = p && ~~ mask 12"
|
||||
proof -
|
||||
fix l
|
||||
assume al: "p && mask 2 = 0"
|
||||
assume "(l::word32) < 4" hence less: "l<2^2" by simp
|
||||
have le: "(2::nat) \<le> 12" by simp
|
||||
assume al: "p && mask 3 = 0"
|
||||
assume "(l::machine_word) < 8" hence less: "l<2^3" by simp
|
||||
have le: "(3::nat) \<le> 12" by simp
|
||||
show "?thesis l"
|
||||
by (rule is_aligned_add_helper[simplified is_aligned_mask,
|
||||
THEN conjunct2, THEN mask_out_first_mask_some, OF al less le])
|
||||
|
|
@ -4890,7 +4882,7 @@ proof -
|
|||
apply (clarsimp simp: storeWord_def invs'_def valid_state'_def)
|
||||
apply (clarsimp simp: valid_machine_state'_def pointerInUserData_def
|
||||
assert_def simpler_modify_def fail_def bind_def return_def
|
||||
pageBits_def aligned_offset_ignore
|
||||
pageBits_def aligned_offset_ignore upto0_7_def
|
||||
split: if_split_asm)
|
||||
done
|
||||
qed
|
||||
|
|
@ -4994,7 +4986,8 @@ lemma set_eobject_corres':
|
|||
apply (clarsimp simp: aobj_relation_cuts_def split: X64_A.arch_kernel_obj.splits)
|
||||
apply (rename_tac arch_kernel_obj obj d p ts)
|
||||
apply (case_tac arch_kernel_obj; simp)
|
||||
apply (clarsimp simp: pte_relation_def pde_relation_def is_tcb_def
|
||||
apply (clarsimp simp: pte_relation_def pde_relation_def pdpte_relation_def pml4e_relation_def
|
||||
is_tcb_def
|
||||
split: if_split_asm)+
|
||||
apply (simp only: ekheap_relation_def dom_fun_upd2 simp_thms)
|
||||
apply (frule bspec, erule domI)
|
||||
|
|
|
|||
Loading…
Reference in New Issue