adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

aarch64 ainvs+refine: proof updates for PT type ghost state 

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
Gerwin Klein 2023-05-24 18:05:24 +10:00
parent e0ae44a577
commit 064d102047
No known key found for this signature in database
GPG Key ID: 20A847CE6AB7F5F3
8 changed files with 267 additions and 214 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
proof/invariant-abstract/AARCH64/ArchRetype_AI.thy
View File

@ -32,14 +32,14 @@ lemma slot_bits_def2 [Retype_AI_assms]: "slot_bits = cte_level_bits"
definition
"no_gs_types \<equiv> UNIV - {CapTableObject,
ArchObject SmallPageObj, ArchObject LargePageObj, ArchObject HugePageObj}"
ArchObject SmallPageObj, ArchObject LargePageObj, ArchObject HugePageObj,
ArchObject PageTableObj, ArchObject VSpaceObj}"
lemma no_gs_types_simps [simp, Retype_AI_assms]:
"Untyped \<in> no_gs_types"
"TCBObject \<in> no_gs_types"
"EndpointObject \<in> no_gs_types"
"NotificationObject \<in> no_gs_types"
"ArchObject PageTableObj \<in> no_gs_types"
"ArchObject ASIDPoolObj \<in> no_gs_types"
by (simp_all add: no_gs_types_def)

49
proof/refine/AARCH64/CNodeInv_R.thy
View File

@ -8632,33 +8632,34 @@ lemma corres_null_cap_update:
(invs' and cte_at' (cte_map slot))
(set_cap cap slot) (updateCap (cte_map slot) cap')"
apply (rule corres_caps_decomposition[rotated])
apply (wp updateCap_ctes_of_wp)+
apply (clarsimp simp: cte_wp_at_ctes_of modify_map_apply
fun_upd_def[symmetric])
apply (frule state_relation_pspace_relation)
apply (frule(1) pspace_relation_ctes_ofI, clarsimp+)
apply (drule(1) cap_relation_same)
apply (case_tac cte)
apply (clarsimp simp: cte_wp_at_caps_of_state fun_upd_idem)
apply (clarsimp simp: state_relation_def)
apply (erule_tac P="\<lambda>caps. cdt_relation caps m ctes" for m ctes in rsubst)
apply (rule ext, clarsimp simp: cte_wp_at_caps_of_state eq_commute)
apply(clarsimp simp: cdt_list_relation_def state_relation_def)
apply(case_tac "next_slot (a, b) (cdt_list s) (cdt s)")
apply (wp updateCap_ctes_of_wp)+
apply (clarsimp simp: cte_wp_at_ctes_of modify_map_apply
fun_upd_def[symmetric])
apply (frule state_relation_pspace_relation)
apply (frule(1) pspace_relation_ctes_ofI, clarsimp+)
apply (drule(1) cap_relation_same)
apply (case_tac cte)
apply (clarsimp simp: cte_wp_at_caps_of_state fun_upd_idem)
apply (clarsimp simp: state_relation_def)
apply (erule_tac P="\<lambda>caps. cdt_relation caps m ctes" for m ctes in rsubst)
apply (rule ext, clarsimp simp: cte_wp_at_caps_of_state eq_commute)
apply(clarsimp simp: cdt_list_relation_def state_relation_def)
apply(case_tac "next_slot (a, b) (cdt_list s) (cdt s)")
apply(simp)
apply(clarsimp)
apply(erule_tac x=a in allE, erule_tac x=b in allE)
apply(simp)
apply(clarsimp)
apply(erule_tac x=a in allE, erule_tac x=b in allE)
apply(simp)
apply(clarsimp simp: modify_map_def split: if_split_asm)
apply(case_tac z)
apply(clarsimp)
apply(clarsimp simp: modify_map_def split: if_split_asm)
apply(case_tac z)
apply(clarsimp)
apply (simp add: state_relation_def)
apply (simp add: state_relation_def)
apply (simp add: state_relation_def)
apply (clarsimp simp: state_relation_def fun_upd_def[symmetric]
cte_wp_at_caps_of_state fun_upd_idem)
apply (clarsimp simp: state_relation_def)
apply (clarsimp simp: state_relation_def fun_upd_def[symmetric]
cte_wp_at_caps_of_state fun_upd_idem)
apply (clarsimp simp: state_relation_def)
apply (clarsimp simp: state_relation_def ghost_relation_of_heap)
apply (clarsimp simp: state_relation_def ghost_relation_of_heap)
apply (clarsimp simp: state_relation_def ghost_relation_of_heap)
apply (clarsimp simp: state_relation_def ghost_relation_of_heap pt_types_of_heap_eq o_def)
apply (subst return_bind[where x="()", symmetric], subst updateCap_def,
rule corres_split_forwards')
apply (rule corres_guard_imp, rule getCTE_symb_exec_r, simp+)

192
proof/refine/AARCH64/CSpace_R.thy
View File

@ -916,7 +916,7 @@ lemma cteMove_corres:
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 "ghost_relation s t p q" for s t p q)+
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])
@ -3571,9 +3571,21 @@ lemma setCTE_corres:
apply fastforce
done
locale_abbrev
"pt_types_of s \<equiv> pts_of s ||> pt_type"
(* oldish-style, but still needed for the heap-only form below *)
definition pt_types_of_heap :: "(obj_ref \<rightharpoonup> Structures_A.kernel_object) \<Rightarrow> obj_ref \<rightharpoonup> pt_type" where
"pt_types_of_heap h \<equiv> h |> aobj_of |> pt_of ||> pt_type"
lemma pt_types_of_heap_eq:
"pt_types_of_heap (kheap s) = pt_types_of s"
by (simp add: pt_types_of_heap_def)
(* FIXME: move to StateRelation *)
lemma ghost_relation_of_heap:
"ghost_relation h ups cns \<longleftrightarrow> ups_of_heap h = ups \<and> cns_of_heap h = cns"
"ghost_relation h ups cns pt_types \<longleftrightarrow>
ups_of_heap h = ups \<and> cns_of_heap h = cns \<and> pt_types_of_heap h = pt_types"
apply (rule iffI)
apply (rule conjI)
apply (rule ext)
@ -3582,23 +3594,32 @@ lemma ghost_relation_of_heap:
apply (auto simp: ghost_relation_def ups_of_heap_def
split: option.splits Structures_A.kernel_object.splits
arch_kernel_obj.splits)[1]
subgoal for x dev sz
subgoal for x dev sz
by (drule_tac x = sz in spec,simp)
apply (rule conjI)
apply (rule ext)
apply (clarsimp simp add: ghost_relation_def cns_of_heap_def)
apply (drule_tac x=x in spec)+
apply (rule ccontr)
apply (simp split: option.splits Structures_A.kernel_object.splits
arch_kernel_obj.splits)[1]
apply (simp split: if_split_asm)
apply force
apply (drule not_sym)
apply clarsimp
apply (erule_tac x=y in allE)
apply simp
apply (rule ext)
apply (clarsimp simp add: ghost_relation_def cns_of_heap_def)
apply (drule_tac x=x in spec)+
apply (rule ccontr)
apply (simp split: option.splits Structures_A.kernel_object.splits
arch_kernel_obj.splits)[1]
apply (simp split: if_split_asm)
apply force
apply (drule not_sym)
apply clarsimp
apply (erule_tac x=y in allE)
apply simp
apply (auto simp add: ghost_relation_def ups_of_heap_def cns_of_heap_def
apply (clarsimp simp: ghost_relation_def cns_of_heap_def)
apply (thin_tac P for P) \<comment> \<open>DataPages\<close>
apply (thin_tac P for P) \<comment> \<open>CNodes\<close>
apply (simp add: pt_types_of_heap_def)
apply (clarsimp simp: opt_map_def split: option.splits)
apply (clarsimp?, rule conjI, clarsimp, rule sym, rule ccontr, force)+
apply force
apply (auto simp: ghost_relation_def ups_of_heap_def cns_of_heap_def pt_types_of_heap_def in_omonad
split: option.splits Structures_A.kernel_object.splits
arch_kernel_obj.splits if_split_asm)
arch_kernel_obj.splits if_split_asm)[1]
done
lemma corres_caps_decomposition:
@ -3625,6 +3646,7 @@ lemma corres_caps_decomposition:
"\<And>P. \<lbrace>\<lambda>s. P (new_ups' s)\<rbrace> g \<lbrace>\<lambda>rv s. P (gsUserPages s)\<rbrace>"
"\<And>P. \<lbrace>\<lambda>s. P (new_cns s)\<rbrace> f \<lbrace>\<lambda>rv s. P (cns_of_heap (kheap s))\<rbrace>"
"\<And>P. \<lbrace>\<lambda>s. P (new_cns' s)\<rbrace> g \<lbrace>\<lambda>rv s. P (gsCNodes s)\<rbrace>"
"\<And>P. \<lbrace>\<lambda>s. P (new_pt_types s)\<rbrace> f \<lbrace>\<lambda>rv s. P (pt_types_of s)\<rbrace>"
"\<And>P. \<lbrace>\<lambda>s. P (new_queues s)\<rbrace> f \<lbrace>\<lambda>rv s. P (ready_queues s)\<rbrace>"
"\<And>P. \<lbrace>\<lambda>s. P (new_action s)\<rbrace> f \<lbrace>\<lambda>rv s. P (scheduler_action s)\<rbrace>"
"\<And>P. \<lbrace>\<lambda>s. P (new_sa' s)\<rbrace> g \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace>"
@ -3657,6 +3679,8 @@ lemma corres_caps_decomposition:
\<Longrightarrow> new_ups s = new_ups' s'"
"\<And>s s'. \<lbrakk> P s; P' s'; (s, s') \<in> state_relation \<rbrakk>
\<Longrightarrow> new_cns s = new_cns' s'"
"\<And>s s'. \<lbrakk> P s; P' s'; (s, s') \<in> state_relation \<rbrakk>
\<Longrightarrow> new_pt_types s = gsPTTypes (new_as' s')"
shows "corres r P P' f g"
proof -
have all_ext: "\<And>f f'. (\<forall>p. f p = f' p) = (f = f')"
@ -3711,7 +3735,7 @@ proof -
apply (subst pspace_relations_def[symmetric])
apply (rule corres_underlying_decomposition [OF x])
apply (simp add: ghost_relation_of_heap)
apply (wp hoare_vcg_conj_lift mdb_wp rvk_wp list_wp u abs_irq_together)+
apply (wpsimp wp: hoare_vcg_conj_lift mdb_wp rvk_wp list_wp u abs_irq_together simp: pt_types_of_heap_eq)+
apply (intro z[simplified o_def] conjI | simp add: state_relation_def pspace_relations_def swp_cte_at
| (clarsimp, drule (1) z(6), simp add: state_relation_def pspace_relations_def swp_cte_at))+
done
@ -3764,46 +3788,17 @@ lemma revokable_relation_simp:
\<Longrightarrow> mdbRevocable node = is_original_cap s p"
by (cases p, clarsimp simp: state_relation_def revokable_relation_def)
lemma setCTE_gsUserPages[wp]:
"\<lbrace>\<lambda>s. P (gsUserPages s)\<rbrace> setCTE p v \<lbrace>\<lambda>rv s. P (gsUserPages s)\<rbrace>"
apply (simp add: setCTE_def setObject_def split_def)
apply (wp updateObject_cte_inv crunch_wps | simp)+
done
lemma setCTE_gsCNodes[wp]:
"\<lbrace>\<lambda>s. P (gsCNodes s)\<rbrace> setCTE p v \<lbrace>\<lambda>rv s. P (gsCNodes s)\<rbrace>"
apply (simp add: setCTE_def setObject_def split_def)
apply (wp updateObject_cte_inv crunch_wps | simp)+
done
crunches setCTE
for gsUserPages[wp]: "\<lambda>s. P (gsUserPages s)"
and gsCNodes[wp]: "\<lambda>s. P (gsCNodes s)"
and domain_time[wp]: "\<lambda>s. P (ksDomainTime s)"
and work_units_completed[wp]: "\<lambda>s. P (ksWorkUnitsCompleted s)"
(simp: setObject_def wp: updateObject_cte_inv)
lemma set_original_symb_exec_l':
"corres_underlying {(s, s'). f (ekheap s) (kheap s) s'} False nf' dc P P' (set_original p b) (return x)"
by (simp add: corres_underlying_def return_def set_original_def in_monad Bex_def)
lemma setCTE_schedule_index[wp]:
"\<lbrace>\<lambda>s. P (ksDomScheduleIdx s)\<rbrace> setCTE p v \<lbrace>\<lambda>rv s. P (ksDomScheduleIdx s)\<rbrace>"
apply (simp add: setCTE_def setObject_def split_def)
apply (wp updateObject_cte_inv crunch_wps | simp)+
done
lemma setCTE_schedule[wp]:
"\<lbrace>\<lambda>s. P (ksDomSchedule s)\<rbrace> setCTE p v \<lbrace>\<lambda>rv s. P (ksDomSchedule s)\<rbrace>"
apply (simp add: setCTE_def setObject_def split_def)
apply (wp updateObject_cte_inv crunch_wps | simp)+
done
lemma setCTE_domain_time[wp]:
"\<lbrace>\<lambda>s. P (ksDomainTime s)\<rbrace> setCTE p v \<lbrace>\<lambda>rv s. P (ksDomainTime s)\<rbrace>"
apply (simp add: setCTE_def setObject_def split_def)
apply (wp updateObject_cte_inv crunch_wps | simp)+
done
lemma setCTE_work_units_completed[wp]:
"\<lbrace>\<lambda>s. P (ksWorkUnitsCompleted s)\<rbrace> setCTE p v \<lbrace>\<lambda>_ s. P (ksWorkUnitsCompleted s)\<rbrace>"
apply (simp add: setCTE_def setObject_def split_def)
apply (wp updateObject_cte_inv crunch_wps | simp)+
done
lemma create_reply_master_corres:
"\<lbrakk> sl' = cte_map sl ; AllowGrant \<in> rights \<rbrakk> \<Longrightarrow>
corres dc
@ -3817,56 +3812,56 @@ lemma create_reply_master_corres:
(setCTE sl' (CTE (capability.ReplyCap thread True True) initMDBNode))"
apply clarsimp
apply (rule corres_caps_decomposition)
defer
apply (wp|simp)+
apply (clarsimp simp: o_def cdt_relation_def cte_wp_at_ctes_of
defer
apply (wp|simp)+
apply (clarsimp simp: o_def cdt_relation_def cte_wp_at_ctes_of
split del: if_split cong: if_cong simp del: id_apply)
apply (case_tac cte, clarsimp)
apply (fold fun_upd_def)
apply (subst descendants_of_Null_update')
apply fastforce
apply fastforce
apply assumption
apply assumption
apply (simp add: nullPointer_def)
apply (subgoal_tac "cte_at (a, b) s")
prefer 2
apply (drule not_sym, clarsimp simp: cte_wp_at_caps_of_state
split: if_split_asm)
apply (simp add: state_relation_def cdt_relation_def)
apply (clarsimp simp: o_def cdt_list_relation_def cte_wp_at_ctes_of
split del: if_split cong: if_cong simp del: id_apply)
apply (case_tac cte, clarsimp)
apply (fold fun_upd_def)
apply (subst descendants_of_Null_update')
apply fastforce
apply fastforce
apply assumption
apply assumption
apply (simp add: nullPointer_def)
apply (subgoal_tac "cte_at (a, b) s")
prefer 2
apply (drule not_sym, clarsimp simp: cte_wp_at_caps_of_state
split: if_split_asm)
apply (simp add: state_relation_def cdt_relation_def)
apply (clarsimp simp: o_def cdt_list_relation_def cte_wp_at_ctes_of
split del: if_split cong: if_cong simp del: id_apply)
apply (case_tac cte, clarsimp)
apply (clarsimp simp: state_relation_def cdt_list_relation_def)
apply (simp split: if_split_asm)
apply (erule_tac x=a in allE, erule_tac x=b in allE)
apply clarsimp
apply(case_tac "next_slot (a, b) (cdt_list s) (cdt s)")
apply (clarsimp simp: state_relation_def cdt_list_relation_def)
apply (simp split: if_split_asm)
apply (erule_tac x=a in allE, erule_tac x=b in allE)
apply clarsimp
apply(case_tac "next_slot (a, b) (cdt_list s) (cdt s)")
apply(simp)
apply(simp)
apply(simp)
apply(fastforce simp: valid_mdb'_def valid_mdb_ctes_def valid_nullcaps_def)
apply(fastforce simp: valid_mdb'_def valid_mdb_ctes_def valid_nullcaps_def)
apply (clarsimp simp: state_relation_def)
apply (clarsimp simp: state_relation_def)
apply (clarsimp simp: state_relation_def)
apply (clarsimp simp add: revokable_relation_def cte_wp_at_ctes_of
split del: if_split)
apply simp
apply (rule conjI)
apply (clarsimp simp: initMDBNode_def)
apply clarsimp
apply (subgoal_tac "null_filter (caps_of_state s) (a, b) \<noteq> None")
prefer 2
apply (clarsimp simp: null_filter_def cte_wp_at_caps_of_state
split: if_split_asm)
apply (subgoal_tac "cte_at (a,b) s")
prefer 2
apply (clarsimp simp add: revokable_relation_def cte_wp_at_ctes_of
split del: if_split)
apply simp
apply (rule conjI)
apply (clarsimp simp: initMDBNode_def)
apply clarsimp
apply (drule null_filter_caps_of_stateD)
apply (erule cte_wp_cte_at)
apply (clarsimp split: if_split_asm cong: conj_cong
simp: cte_map_eq_subst revokable_relation_simp
cte_wp_at_cte_at valid_pspace_def)
apply (clarsimp simp: state_relation_def)
apply (clarsimp elim!: state_relationE simp: ghost_relation_of_heap)+
apply (subgoal_tac "null_filter (caps_of_state s) (a, b) \<noteq> None")
prefer 2
apply (clarsimp simp: null_filter_def cte_wp_at_caps_of_state
split: if_split_asm)
apply (subgoal_tac "cte_at (a,b) s")
prefer 2
apply clarsimp
apply (drule null_filter_caps_of_stateD)
apply (erule cte_wp_cte_at)
apply (clarsimp split: if_split_asm cong: conj_cong
simp: cte_map_eq_subst revokable_relation_simp
cte_wp_at_cte_at valid_pspace_def)
apply (clarsimp simp: state_relation_def)
apply (clarsimp elim!: state_relationE simp: ghost_relation_of_heap pt_types_of_heap_eq o_def)+
apply (rule corres_guard_imp)
apply (rule corres_underlying_symb_exec_l [OF set_original_symb_exec_l'])
apply (rule setCTE_corres)
@ -6040,6 +6035,9 @@ lemma updateCap_same_master:
apply (frule use_valid[OF _ setCTE_gsCNodes])
prefer 2
apply simp+
apply (rule use_valid[OF _ setCTE_arch])
prefer 2
apply simp+
apply (subst conj_assoc[symmetric])
apply (rule conjI)
prefer 2

47
proof/refine/AARCH64/Detype_R.thy
View File

@ -123,10 +123,14 @@ lemma deleteObjects_def2:
gsUserPages := \<lambda>x. if x \<in> mask_range ptr bits
then None else gsUserPages s x,
gsCNodes := \<lambda>x. if x \<in> mask_range ptr bits
then None else gsCNodes s x \<rparr>);
then None else gsCNodes s x,
ksArchState := gsPTTypes_update (\<lambda>_ x. if x && - mask bits - 1 = ptr
then Nothing
else gsPTTypes (ksArchState s) x)
(ksArchState s)\<rparr>);
stateAssert ksASIDMapSafe []
od"
apply (simp add: deleteObjects_def is_aligned_mask[symmetric] unless_def)
apply (simp add: deleteObjects_def is_aligned_mask[symmetric] unless_def deleteGhost_def o_def)
apply (rule bind_eqI, rule ext)
apply (rule bind_eqI, rule ext)
apply (simp add: bind_assoc[symmetric])
@ -136,13 +140,14 @@ lemma deleteObjects_def2:
NOT_eq[symmetric] neg_mask_in_mask_range)
apply (clarsimp simp: simpler_modify_def)
apply (simp add: data_map_filterWithKey_def split: if_split_asm)
sorry (* FIXME AARCH64
apply (rule arg_cong2[where f=gsCNodes_update])
apply (simp add: NOT_eq[symmetric] mask_in_range ext)
apply (rule arg_cong2[where f=gsUserPages_update])
apply (simp add: NOT_eq[symmetric] mask_in_range ext)
apply (rule arg_cong[where f="\<lambda>f. ksPSpace_update f s" for s])
apply (simp add: NOT_eq[symmetric] mask_in_range ext split: option.split)
done
done *)
lemma deleteObjects_def3:
"deleteObjects ptr bits =
@ -156,7 +161,11 @@ lemma deleteObjects_def3:
gsUserPages := \<lambda>x. if x \<in> mask_range ptr bits
then None else gsUserPages s x,
gsCNodes := \<lambda>x. if x \<in> mask_range ptr bits
then None else gsCNodes s x \<rparr>);
then None else gsCNodes s x,
ksArchState := gsPTTypes_update (\<lambda>_ x. if x && - mask bits - 1 = ptr
then Nothing
else gsPTTypes (ksArchState s) x)
(ksArchState s) \<rparr>);
stateAssert ksASIDMapSafe []
od"
apply (cases "is_aligned ptr bits")
@ -648,13 +657,18 @@ lemma deleteObjects_corres:
detype_def)
apply (drule_tac t="gsUserPages s'" in sym)
apply (drule_tac t="gsCNodes s'" in sym)
apply (auto simp add: ups_of_heap_def cns_of_heap_def ext add_mask_fold
apply (drule_tac t="gsPTTypes (ksArchState s')" in sym)
apply (auto simp add: ups_of_heap_def cns_of_heap_def ext pt_types_of_heap_def add_mask_fold opt_map_def
split: option.splits kernel_object.splits)[1]
apply (rule ext)
apply (auto simp add: ups_of_heap_def cns_of_heap_def ext pt_types_of_heap_def add_mask_fold opt_map_def
split: option.splits kernel_object.splits)[1]
apply (simp add: valid_mdb_def)
apply (wp hoare_vcg_ex_lift hoare_vcg_ball_lift | wps |
simp add: invs_def valid_state_def valid_pspace_def
descendants_range_def | wp (once) hoare_drop_imps)+
done
sorry (* FIXME AARCH64: ghost state update in deleteObjects *)
text \<open>Invariant preservation across concrete deletion\<close>
@ -1594,14 +1608,15 @@ proof -
apply (simp cong: if_cong)
apply (subgoal_tac "is_aligned ptr bits \<and> 3 \<le> bits \<and> bits < word_bits",simp)
apply clarsimp
apply (frule(2) delete_locale.intro, simp_all)[1]
apply (frule(2) delete_locale.intro, simp_all)[1] thm delete_locale.delete_invs'
apply (rule subst[rotated, where P=invs'], erule delete_locale.delete_invs')
apply (simp add: field_simps mask_def)
sorry (* FIXME AARCH64
apply clarsimp
apply (drule invs_valid_objs')
apply (drule (1) cte_wp_at_valid_objs_valid_cap')
apply (clarsimp simp add: valid_cap'_def capAligned_def untypedBits_defs)
done
done *)
qed
lemma deleteObjects_st_tcb_at':
@ -1696,9 +1711,10 @@ lemma deleteObject_no_overlap[wp]:
ksMachineState_update (\<lambda>_. b)
(s\<lparr>ksPSpace := ksPSpace s |` (- mask_range ptr bits)\<rparr>)", simp)
apply (case_tac s, simp)
sorry (* FIXME AARCH64
apply (rule ext)
apply simp
done
done *)
lemma deleteObjects_cte_wp_at':
"\<lbrace>\<lambda>s. cte_wp_at' P p s \<and> p \<notin> mask_range ptr bits
@ -2158,7 +2174,7 @@ lemma createObject_cte_wp_at':
unless_def placeNewObject_def2 objBits_simps range_cover_full
curDomain_def bit_simps
getObjSize_simps apiGetObjectSize_def tcbBlockSizeBits_def
epSizeBits_def ntfnSizeBits_def cteSizeBits_def
epSizeBits_def ntfnSizeBits_def cteSizeBits_def updatePTType_def
| intro conjI impI | clarsimp dest!: arch_toAPIType_simps)+
done
@ -3160,7 +3176,7 @@ lemma createObject_gsUntypedZeroRanges_commute:
threadSet_gsUntypedZeroRanges_commute'[THEN commute_commute]
split: option.split prod.split cong: if_cong)+
apply (simp add: curDomain_def monad_commute_def exec_modify exec_gets)
done
sorry (* FIXME AARCH64: updatePTTYpes *)
lemma monad_commute_If_rhs:
"monad_commute P a b \<Longrightarrow> monad_commute Q a c
@ -3557,6 +3573,7 @@ lemma createNewCaps_pspace_no_overlap':
| assumption)+
apply (intro conjI range_cover_le[where n = "Suc n"] | simp)+
apply ((simp add:objBits_simps pageBits_def range_cover_def word_bits_def)+)[5]
sorry (* FIXME AARCH64
by ((clarsimp simp: apiGetObjectSize_def bit_simps toAPIType_def
getObjectSize_def objBits_simps objBits_defs
createObjects_def Arch_createNewCaps_def unless_def
@ -3565,7 +3582,7 @@ lemma createNewCaps_pspace_no_overlap':
createObjects'_psp_aligned createObjects'_psp_distinct
mapM_x_wp_inv
| assumption | clarsimp simp: word_bits_def
| intro conjI range_cover_le[where n = "Suc n"] range_cover.aligned)+)
| intro conjI range_cover_le[where n = "Suc n"] range_cover.aligned)+) *)
lemma objSize_eq_capBits:
"Types_H.getObjectSize ty us = APIType_capBits ty us"
@ -4490,13 +4507,14 @@ lemma createObject_def2:
placeNewObject_def2 objBits_simps bind_assoc
clearMemory_def clearMemoryVM_def fun_upd_def[symmetric]
word_size mapM_x_singleton storeWordVM_def)+)[6]
sorry (* FIXME AARCH64: needs update in Intermediate_H
apply (rename_tac apiobject_type)
apply (case_tac apiobject_type)
apply (clarsimp simp: Arch_createNewCaps_def createObjects_def shiftL_nat
AARCH64_H.createObject_def placeNewObject_def2 objBits_simps bind_assoc
clearMemory_def clearMemoryVM_def word_size mapM_x_singleton
storeWordVM_def)+
done
done *)
lemma createNewObjects_def2:
@ -4712,7 +4730,7 @@ lemma ArchCreateObject_pspace_no_overlap':
field_simps split del: if_split
| clarsimp simp add: add.assoc[symmetric],wp createObjects'_pspace_no_overlap2[where n =0 and sz = sz,simplified]
| clarsimp simp add: APIType_capBits_def objBits_simps pageBits_def)+
sorry (* FIXME AARCH64: updatePTType pspace_no_overlap'
apply (clarsimp simp: conj_comms)
apply (frule(1) range_cover_no_0[where p = n])
apply simp
@ -4742,7 +4760,6 @@ lemma ArchCreateObject_pspace_no_overlap':
apply (clarsimp simp: field_simps word_bits_conv
APIType_capBits_def shiftl_t2n objBits_simps bit_simps
| rule conjI | erule range_cover_le,simp)+
sorry (* FIXME AARCH64 we're getting undefined here for something PT-related
done *)
lemma to_from_apiTypeD: "toAPIType ty = Some x \<Longrightarrow> ty = fromAPIType x"

159
proof/refine/AARCH64/Retype_R.thy
View File

@ -302,70 +302,74 @@ lemma cte_at_next_slot'':
lemma state_relation_null_filterE:
"\<lbrakk> (s, s') \<in> state_relation; t = kheap_update f (ekheap_update ef s);
\<exists>f' g' h'.
\<exists>f' g' h' pt_fn'.
t' = s'\<lparr>ksPSpace := f' (ksPSpace s'), gsUserPages := g' (gsUserPages s'),
gsCNodes := h' (gsCNodes s')\<rparr>;
gsCNodes := h' (gsCNodes s'),
ksArchState := (ksArchState s') \<lparr>gsPTTypes := pt_fn' (gsPTTypes (ksArchState s'))\<rparr>\<rparr>;
null_filter (caps_of_state t) = null_filter (caps_of_state s);
null_filter' (ctes_of t') = null_filter' (ctes_of s');
pspace_relation (kheap t) (ksPSpace t');
ekheap_relation (ekheap t) (ksPSpace t');
ghost_relation (kheap t) (gsUserPages t') (gsCNodes t'); valid_list s;
ghost_relation (kheap t) (gsUserPages t') (gsCNodes t') (gsPTTypes (ksArchState t'));
valid_list s;
pspace_aligned' s'; pspace_distinct' s'; valid_objs s; valid_mdb s;
pspace_aligned' t'; pspace_distinct' t';
mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s) \<rbrakk>
\<Longrightarrow> (t, t') \<in> state_relation"
apply (clarsimp simp: state_relation_def)
apply (intro conjI)
apply (simp add: cdt_relation_def cte_wp_at_caps_of_state)
apply (elim allEI)
apply clarsimp
apply (erule(1) across_null_filter_eq)
apply (simp add: cdt_relation_def cte_wp_at_caps_of_state)
apply (elim allEI)
apply clarsimp
apply (erule(1) across_null_filter_eq)
apply simp
apply (rule null_filter_descendants_of', simp)
apply simp
apply (rule null_filter_descendants_of', simp)
apply simp
apply (case_tac "cdt s (a, b)")
apply (subst mdb_cte_at_no_descendants, assumption)
apply (simp add: cte_wp_at_caps_of_state swp_def)
apply (cut_tac s="kheap_update f (ekheap_update ef s)" and
s'="s'\<lparr>ksPSpace := f' (ksPSpace s'),
gsUserPages := g' (gsUserPages s'),
gsCNodes := h' (gsCNodes s')\<rparr>"
in pspace_relation_ctes_ofI, simp_all)[1]
apply (simp add: trans_state_update[symmetric] del: trans_state_update)
apply (erule caps_of_state_cteD)
apply (clarsimp simp: descendants_of'_def)
apply (case_tac cte)
apply (erule Null_not_subtree[rotated])
apply simp
apply (drule(1) mdb_cte_atD)
apply (clarsimp simp: cte_wp_at_caps_of_state)
apply(simp add: cdt_list_relation_def cte_wp_at_caps_of_state)
apply(elim allEI)
apply(clarsimp)
apply(case_tac "next_slot (a, b) (cdt_list (s)) (cdt s)")
apply(simp)
apply(subgoal_tac "cte_wp_at (\<lambda>c. c \<noteq> cap.NullCap) (a, b) s")
apply(drule_tac f="\<lambda>cs. cs (a, b)" in arg_cong)
apply(clarsimp simp: cte_wp_at_caps_of_state)
apply(clarsimp simp: null_filter_def split: if_split_asm)
apply(drule_tac f="\<lambda>ctes. ctes (cte_map (a, b))" in arg_cong)
apply(simp add: null_filter'_def cte_wp_at_ctes_of split: if_split_asm)
apply(frule pspace_relation_cte_wp_at)
apply(simp add: cte_wp_at_caps_of_state)
apply(simp)
apply (case_tac "cdt s (a, b)")
apply (subst mdb_cte_at_no_descendants, assumption)
apply (simp add: cte_wp_at_caps_of_state swp_def)
apply (cut_tac s="kheap_update f (ekheap_update ef s)" and
s'="s'\<lparr>ksPSpace := f' (ksPSpace s'),
gsUserPages := g' (gsUserPages s'),
gsCNodes := h' (gsCNodes s'),
ksArchState := ksArchState s' \<lparr>gsPTTypes := pt_fn' (gsPTTypes (ksArchState s'))\<rparr>\<rparr>"
in pspace_relation_ctes_ofI, simp_all)[1]
apply (simp add: trans_state_update[symmetric] del: trans_state_update)
apply (erule caps_of_state_cteD)
apply (clarsimp simp: descendants_of'_def)
apply (case_tac cte)
apply (erule Null_not_subtree[rotated])
apply simp
apply (drule(1) mdb_cte_atD)
apply (clarsimp simp: cte_wp_at_caps_of_state)
apply(simp add: cdt_list_relation_def cte_wp_at_caps_of_state)
apply(elim allEI)
apply(clarsimp)
apply(case_tac "next_slot (a, b) (cdt_list (s)) (cdt s)")
apply(simp)
apply(simp add: cte_wp_at_ctes_of)
apply (simp add: mdb_cte_at_def)
apply(frule finite_depth)
apply(frule(3) cte_at_next_slot'')
apply simp
apply (simp add: revokable_relation_def)
apply (elim allEI, rule impI, drule(1) mp, elim allEI)
apply (clarsimp elim!: null_filterE)
apply (drule(3) pspace_relation_cte_wp_at [OF _ caps_of_state_cteD])
apply (drule_tac f="\<lambda>ctes. ctes (cte_map (a, b))" in arg_cong)
apply (clarsimp simp: null_filter'_def cte_wp_at_ctes_of
split: if_split_asm)
apply(subgoal_tac "cte_wp_at (\<lambda>c. c \<noteq> cap.NullCap) (a, b) s")
apply(drule_tac f="\<lambda>cs. cs (a, b)" in arg_cong)
apply(clarsimp simp: cte_wp_at_caps_of_state)
apply(clarsimp simp: null_filter_def split: if_split_asm)
apply(drule_tac f="\<lambda>ctes. ctes (cte_map (a, b))" in arg_cong)
apply(simp add: null_filter'_def cte_wp_at_ctes_of split: if_split_asm)
apply(frule pspace_relation_cte_wp_at)
apply(simp add: cte_wp_at_caps_of_state)
apply(simp)
apply(simp)
apply(simp add: cte_wp_at_ctes_of)
apply (simp add: mdb_cte_at_def)
apply(frule finite_depth)
apply(frule(3) cte_at_next_slot'')
apply simp
apply (simp add: revokable_relation_def)
apply (elim allEI, rule impI, drule(1) mp, elim allEI)
apply (clarsimp elim!: null_filterE)
apply (drule(3) pspace_relation_cte_wp_at [OF _ caps_of_state_cteD])
apply (drule_tac f="\<lambda>ctes. ctes (cte_map (a, b))" in arg_cong)
apply (clarsimp simp: null_filter'_def cte_wp_at_ctes_of
split: if_split_asm)
apply (simp add: arch_state_relation_def)
done
lemma lookupAround2_pspace_no:
@ -1154,6 +1158,10 @@ where
(\<lambda>ups x. if x \<in> ptrs then Some ARMLargePage else ups x)
| ArchObject HugePageObj \<Rightarrow> gsUserPages_update
(\<lambda>ups x. if x \<in> ptrs then Some ARMHugePage else ups x)
| ArchObject PageTableObj \<Rightarrow> ksArchState_update
(\<lambda>as. gsPTTypes_update (\<lambda>pt_types x. if x \<in> ptrs then Some NormalPT_T else pt_types x) as)
| ArchObject VSpaceObj \<Rightarrow> ksArchState_update
(\<lambda>as. gsPTTypes_update (\<lambda>pt_types x. if x \<in> ptrs then Some VSRootPT_T else pt_types x) as)
| _ \<Rightarrow> id"
lemma ksPSpace_update_gs_eq[simp]:
@ -1193,6 +1201,10 @@ lemma update_gs_simps[simp]:
gsUserPages_update (\<lambda>ups x. if x \<in> ptrs then Some ARMLargePage else ups x)"
"update_gs (ArchObject HugePageObj) us ptrs =
gsUserPages_update (\<lambda>ups x. if x \<in> ptrs then Some ARMHugePage else ups x)"
"update_gs (ArchObject PageTableObj) us ptrs = ksArchState_update
(\<lambda>as. gsPTTypes_update (\<lambda>pt_types x. if x \<in> ptrs then Some NormalPT_T else pt_types x) as)"
"update_gs (ArchObject VSpaceObj) us ptrs = ksArchState_update
(\<lambda>as. gsPTTypes_update (\<lambda>pt_types x. if x \<in> ptrs then Some VSRootPT_T else pt_types x) as)"
by (simp_all add: update_gs_def)
lemma retype_state_relation:
@ -1298,14 +1310,15 @@ lemma retype_state_relation:
have pn2: "\<forall>a\<in>set ?al. kheap s a = None"
by (rule ccontr) (clarsimp simp: pspace_no_overlapD1[OF pn _ cover vs(1)])
from sr have gr: "ghost_relation (kheap s) (gsUserPages s') (gsCNodes s')"
from sr
have gr: "ghost_relation (kheap s) (gsUserPages s') (gsCNodes s') (gsPTTypes (ksArchState s'))"
by (rule state_relationE)
show "ghost_relation ?ps (gsUserPages ?t') (gsCNodes ?t')"
show "ghost_relation ?ps (gsUserPages ?t') (gsCNodes ?t') (gsPTTypes (ksArchState ?t'))"
proof (cases ?tp)
case Untyped thus ?thesis by (simp add: not_unt)
next
note data_map_insert_def[simp]
note data_map_insert_def[simp]
case TCBObject
from pn2
@ -1316,6 +1329,8 @@ lemma retype_state_relation:
have [simp]: "cns_of_heap ?ps = cns_of_heap (kheap s)"
by - (rule ext, induct (?al),
simp_all add: cns_of_heap_def default_object_def TCBObject)
have [simp]: "pt_types_of_heap ?ps = pt_types_of_heap (kheap s)"
sorry (* FIXME AARCH64 *)
note data_map_insert_def[simp del]
from gr show ?thesis
by (simp add: ghost_relation_of_heap, simp add: TCBObject update_gs_def)
@ -1329,11 +1344,13 @@ lemma retype_state_relation:
have [simp]: "cns_of_heap ?ps = cns_of_heap (kheap s)"
by - (rule ext, induct (?al),
simp_all add: cns_of_heap_def default_object_def data_map_insert_def EndpointObject)
have [simp]: "pt_types_of_heap ?ps = pt_types_of_heap (kheap s)"
sorry (* FIXME AARCH64 *)
from gr show ?thesis
by (simp add: ghost_relation_of_heap,
simp add: EndpointObject update_gs_def)
next
note data_map_insert_def[simp]
note data_map_insert_def[simp]
case NotificationObject
from pn2
have [simp]: "ups_of_heap ?ps = ups_of_heap (kheap s)"
@ -1343,7 +1360,9 @@ lemma retype_state_relation:
have [simp]: "cns_of_heap ?ps = cns_of_heap (kheap s)"
by - (rule ext, induct (?al), simp_all add: cns_of_heap_def
default_object_def NotificationObject)
note data_map_insert_def[simp del]
have [simp]: "pt_types_of_heap ?ps = pt_types_of_heap (kheap s)"
sorry (* FIXME AARCH64 *)
note data_map_insert_def[simp del]
from gr show ?thesis
by (simp add: ghost_relation_of_heap,
simp add: NotificationObject update_gs_def)
@ -1358,6 +1377,8 @@ lemma retype_state_relation:
else cns_of_heap (kheap s) x)"
by (rule ext, induct (?al),
simp_all add: cns_of_heap_def wf_empty_bits wf_unique default_object_def CapTableObject)
have [simp]: "pt_types_of_heap ?ps = pt_types_of_heap (kheap s)"
sorry (* FIXME AARCH64 *)
note data_map_insert_def[simp del]
from gr show ?thesis
by (simp add: ghost_relation_of_heap,
@ -1370,6 +1391,7 @@ lemma retype_state_relation:
default_object_def ArchObject)
from pn2 gr show ?thesis
apply (clarsimp simp add: ghost_relation_of_heap)
sorry (* FIXME AARCH64
apply (rule conjI[rotated])
apply (simp add: ArchObject update_gs_def split: aobject_type.splits)
apply (thin_tac "cns_of_heap h = g" for h g)
@ -1381,14 +1403,16 @@ lemma retype_state_relation:
default_arch_object_def ups_of_heap_def
data_map_insert_def
split: aobject_type.splits)
done
done *)
qed
show "\<exists>f' g' h'. ?t' =
show "\<exists>f' g' h' pt_fn'. ?t' =
s'\<lparr>ksPSpace := f' (ksPSpace s'), gsUserPages := g' (gsUserPages s'),
gsCNodes := h' (gsCNodes s')\<rparr>"
gsCNodes := h' (gsCNodes s'),
ksArchState := (ksArchState s') \<lparr>gsPTTypes := pt_fn' (gsPTTypes (ksArchState s'))\<rparr>\<rparr>"
apply (clarsimp simp: update_gs_def
split: Structures_A.apiobject_type.splits)
sorry (* FIXME AARCH64
apply (intro conjI impI)
apply (subst ex_comm, rule_tac x=id in exI,
subst ex_comm, rule_tac x=id in exI, fastforce)+
@ -1411,7 +1435,7 @@ lemma retype_state_relation:
apply (rule_tac x="\<lambda>cns x. if x \<in> set ?al then Some ARMHugePage
else cns x" in exI, simp)
apply (rule_tac x=id in exI, simp)+
done
done *)
qed
lemma new_cap_addrs_fold':
@ -4068,8 +4092,9 @@ lemma createNewCaps_idle'[wp]:
sorry (* FIXME AARCH64 issue: range_cover ptr sz 13 n does not imply range_cover ptr sz 12 n ?
done *)
(* FIXME AARCH64: this is no longer true, createNewCaps does update the ghost state inside the arch state
crunch ksArch[wp]: createNewCaps "\<lambda>s. P (ksArchState s)"
(simp: crunch_simps unless_def wp: crunch_wps)
(simp: crunch_simps unless_def wp: crunch_wps) *)
crunch gsMaxObjectSize[wp]: createNewCaps "\<lambda>s. P (gsMaxObjectSize s)"
(simp: crunch_simps unless_def wp: crunch_wps updateObject_default_inv)
@ -4087,6 +4112,7 @@ lemma createNewCaps_global_refs':
apply (auto simp: cte_wp_at_ctes_of linorder_not_less elim!: ranE)[1]
apply (rule hoare_pre)
apply (simp add: global_refs'_def)
sorry (* FIXME AARCH64: needs new crunch for parts of ksArchState
apply (rule hoare_use_eq [where f=ksArchState, OF createNewCaps_ksArch])
apply (rule hoare_use_eq [where f=ksIdleThread, OF createNewCaps_it])
apply (rule hoare_use_eq [where f=irq_node', OF createNewCaps_ksInterrupt])
@ -4095,7 +4121,7 @@ lemma createNewCaps_global_refs':
apply (clarsimp simp: cte_wp_at_ctes_of global_refs'_def
makeObject_cte)
apply (auto simp: linorder_not_less ball_ran_eq)
done
done *)
lemma koTypeOf_eq_UserDataT:
"(koTypeOf ko = UserDataT)
@ -4110,11 +4136,12 @@ lemma createNewCaps_valid_arch_state:
\<lbrace>\<lambda>rv. valid_arch_state'\<rbrace>"
unfolding valid_arch_state'_def valid_asid_table'_def vspace_table_at'_defs
apply (simp add: typ_at_to_obj_at_arches option_case_all_conv)
sorry (* FIXME AARCH64: needs new crunch for parts of ksArchState
apply (wpsimp wp: hoare_vcg_const_Ball_lift createNewCaps_obj_at'
createNewCaps_ko_wp_at' hoare_vcg_all_lift
hoare_vcg_imp_lift')
apply (fastforce simp: pred_conj_def valid_pspace'_def o_def is_vcpu'_def)
done
done *)
lemma valid_irq_node_lift_asm:
assumes x: "\<And>P. \<lbrace>\<lambda>s. P (irq_node' s)\<rbrace> f \<lbrace>\<lambda>rv s. P (irq_node' s)\<rbrace>"
@ -4703,6 +4730,7 @@ lemma createObjects_no_cte_valid_global:
apply (auto simp: cte_wp_at_ctes_of linorder_not_less elim!: ranE)[1]
apply (rule hoare_pre)
apply (simp add: global_refs'_def)
sorry (* FIXME AARCH64: needs new crunch for parts of ksArchState
apply (rule hoare_use_eq [where f=ksArchState, OF createObjects_ksArch])
apply (rule hoare_use_eq [where f=ksIdleThread, OF createObjects_it])
apply (rule hoare_use_eq [where f=irq_node', OF createObjects_ksInterrupt])
@ -4713,7 +4741,7 @@ lemma createObjects_no_cte_valid_global:
apply (simp add: split_def cte_wp_at_ctes_of split: option.splits)
apply (clarsimp simp: global_refs'_def)
apply (auto simp: ball_ran_eq linorder_not_less[symmetric])
done
done *)
lemma createObjects'_typ_at:
"\<lbrace>\<lambda>s. n \<noteq> 0 \<and>
@ -4768,8 +4796,9 @@ lemma createObjects_valid_arch:
apply (wpsimp wp: hoare_vcg_const_Ball_lift createNewCaps_obj_at' createObjects_orig_ko_wp_at2'
createNewCaps_ko_wp_at' hoare_vcg_all_lift
hoare_vcg_imp_lift')
sorry (* FIXME AARCH64: needs new crunch for parts of ksArchState
apply (fastforce simp: pred_conj_def valid_pspace'_def o_def is_vcpu'_def)
done
done *)
lemma createObjects_irq_state:
"\<lbrace>\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and>

21
proof/refine/AARCH64/StateRelation.thy
View File

@ -325,10 +325,11 @@ definition ready_queues_relation ::
"ready_queues_relation qs qs' \<equiv> \<forall>d p. (qs d p = qs' (d, p))"
definition ghost_relation ::
"Structures_A.kheap \<Rightarrow> (machine_word \<rightharpoonup> vmpage_size) \<Rightarrow> (machine_word \<rightharpoonup> nat) \<Rightarrow> bool" where
"ghost_relation h ups cns \<equiv>
"Structures_A.kheap \<Rightarrow> (machine_word \<rightharpoonup> vmpage_size) \<Rightarrow> (machine_word \<rightharpoonup> nat) \<Rightarrow> (machine_word \<rightharpoonup> pt_type) \<Rightarrow> bool" where
"ghost_relation h ups cns pt_types \<equiv>
(\<forall>a sz. (\<exists>dev. h a = Some (ArchObj (DataPage dev sz))) \<longleftrightarrow> ups a = Some sz) \<and>
(\<forall>a n. (\<exists>cs. h a = Some (CNode n cs) \<and> well_formed_cnode_n n cs) \<longleftrightarrow> cns a = Some n)"
(\<forall>a n. (\<exists>cs. h a = Some (CNode n cs) \<and> well_formed_cnode_n n cs) \<longleftrightarrow> cns a = Some n) \<and>
(\<forall>a pt_t. (\<exists>pt. h a = Some (ArchObj (PageTable pt)) \<and> pt_t = pt_type pt) \<longleftrightarrow> pt_types a = Some pt_t)"
definition cdt_relation :: "(cslot_ptr \<Rightarrow> bool) \<Rightarrow> cdt \<Rightarrow> cte_heap \<Rightarrow> bool" where
"cdt_relation \<equiv> \<lambda>cte_at m m'.
@ -461,7 +462,7 @@ definition state_relation :: "(det_state \<times> kernel_state) set" where
\<and> ekheap_relation (ekheap s) (ksPSpace s')
\<and> sched_act_relation (scheduler_action s) (ksSchedulerAction s')
\<and> ready_queues_relation (ready_queues s) (ksReadyQueues s')
\<and> ghost_relation (kheap s) (gsUserPages s') (gsCNodes s')
\<and> ghost_relation (kheap s) (gsUserPages s') (gsCNodes s') (gsPTTypes (ksArchState s'))
\<and> cdt_relation (swp cte_at s) (cdt s) (ctes_of s')
\<and> cdt_list_relation (cdt_list s) (cdt s) (ctes_of s')
\<and> revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s')
@ -496,7 +497,7 @@ lemma state_relationD:
ekheap_relation (ekheap s) (ksPSpace s') \<and>
sched_act_relation (scheduler_action s) (ksSchedulerAction s') \<and>
ready_queues_relation (ready_queues s) (ksReadyQueues s') \<and>
ghost_relation (kheap s) (gsUserPages s') (gsCNodes s') \<and>
ghost_relation (kheap s) (gsUserPages s') (gsCNodes s') (gsPTTypes (ksArchState s')) \<and>
cdt_relation (swp cte_at s) (cdt s) (ctes_of s') \<and>
cdt_list_relation (cdt_list s) (cdt s) (ctes_of s') \<and>
revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s') \<and>
@ -518,7 +519,7 @@ lemma state_relationE [elim?]:
ekheap_relation (ekheap s) (ksPSpace s');
sched_act_relation (scheduler_action s) (ksSchedulerAction s');
ready_queues_relation (ready_queues s) (ksReadyQueues s');
ghost_relation (kheap s) (gsUserPages s') (gsCNodes s');
ghost_relation (kheap s) (gsUserPages s') (gsCNodes s') (gsPTTypes (ksArchState s'));
cdt_relation (swp cte_at s) (cdt s) (ctes_of s') \<and>
revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s');
cdt_list_relation (cdt_list s) (cdt s) (ctes_of s');
@ -585,13 +586,13 @@ lemma pspace_dom_relatedE:
done
lemma ghost_relation_typ_at:
"ghost_relation (kheap s) ups cns \<equiv>
"ghost_relation (kheap s) ups cns pt_types \<equiv>
(\<forall>a sz. data_at sz a s = (ups a = Some sz)) \<and>
(\<forall>a n. typ_at (ACapTable n) a s = (cns a = Some n))"
(\<forall>a n. typ_at (ACapTable n) a s = (cns a = Some n)) \<and>
(\<forall>a pt_t. pt_at pt_t a s = (pt_types a = Some pt_t))"
apply (rule eq_reflection)
apply (clarsimp simp: ghost_relation_def typ_at_eq_kheap_obj data_at_def)
apply (intro conjI impI iffI allI; force)
done
by (intro conjI impI iffI allI; force)
end

6
proof/refine/AARCH64/Untyped_R.thy
View File

@ -1494,7 +1494,7 @@ shows
apply (elim modify_map_casesE)
apply (clarsimp split: if_split_asm cong: conj_cong
simp: cte_map_eq_subst cte_wp_at_cte_at revokable_relation_simp)+
apply (clarsimp simp: state_relation_def ghost_relation_of_heap)+
apply (clarsimp simp: state_relation_def ghost_relation_of_heap pt_types_of_heap_eq o_def)+
apply wp+
apply (rule corres_guard_imp)
apply (rule corres_underlying_symb_exec_l [OF gets_symb_exec_l])
@ -4046,6 +4046,8 @@ lemma idx_le_new_offs:
end
context begin interpretation Arch . (*FIXME: arch_split*)
lemma valid_sched_etcbs[elim!]: "valid_sched_2 queues ekh sa cdom kh ct it \<Longrightarrow> valid_etcbs_2 ekh kh"
by (simp add: valid_sched_def)
@ -4608,6 +4610,8 @@ lemma whenE_reset_resetUntypedCap_invs_etc:
crunch ksCurDomain[wp]: updateFreeIndex "\<lambda>s. P (ksCurDomain s)"
end
lemma (in range_cover) funky_aligned:
"is_aligned ((ptr && foo) + v * 2 ^ sbit) sbit"
apply (rule aligned_add_aligned)

3
spec/haskell/src/SEL4/Model/PSpace/AARCH64.hs
View File

@ -11,8 +11,11 @@ module SEL4.Model.PSpace.AARCH64(deleteGhost) where
import Prelude hiding (Word)
import SEL4.Model.StateData
import SEL4.Model.StateData.AARCH64
import SEL4.Machine.RegisterSet
import Data.Bits
deleteGhost :: PPtr a -> Int -> Kernel ()
deleteGhost ptr bits = do
let inRange = (\x -> x .&. ((- mask bits) - 1) == fromPPtr ptr)