Skip to content

Commit

Permalink
x64 crefine: update to Isabelle2023 mapsto syntax
Browse files Browse the repository at this point in the history 
Signed-off-by: Gerwin Klein <[email protected]>
  • Loading branch information
@lsf37
lsf37 committed Sep 29, 2023
1 parent 29f3c35 commit 1f3d1f6
Show file tree
Hide file tree
Showing 11 changed files with 142 additions and 141 deletions.
8 changes: 4 additions & 4 deletions proof/crefine/X64/Finalise_C.thy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1283,7 +1283,7 @@ lemma deleteASID_ccorres:

lemma setObject_ccorres_lemma:
fixes val :: "'a :: pspace_storable" shows
"\<lbrakk> \<And>s. \<Gamma> \<turnstile> (Q s) c {s'. (s \<lparr> ksPSpace := ksPSpace s (ptr \<mapsto> injectKO val) \<rparr>, s') \<in> rf_sr},{};
"\<lbrakk> \<And>s. \<Gamma> \<turnstile> (Q s) c {s'. (s \<lparr> ksPSpace := (ksPSpace s)(ptr \<mapsto> injectKO val) \<rparr>, s') \<in> rf_sr},{};
\<And>s s' val (val' :: 'a). \<lbrakk> ko_at' val' ptr s; (s, s') \<in> rf_sr \<rbrakk>
\<Longrightarrow> s' \<in> Q s;
\<And>val :: 'a. updateObject val = updateObject_default val;
Expand Down Expand Up @@ -1730,7 +1730,7 @@ lemma option_to_ctcb_ptr_not_0:
done

lemma update_tcb_map_to_tcb:
"map_to_tcbs (ksPSpace s(p \<mapsto> KOTCB tcb))
"map_to_tcbs ((ksPSpace s)(p \<mapsto> KOTCB tcb))
= (map_to_tcbs (ksPSpace s))(p \<mapsto> tcb)"
by (rule ext, clarsimp simp: projectKOs map_comp_def split: if_split)

Expand Down Expand Up @@ -1770,7 +1770,7 @@ lemma sched_queue_relation_shift:

lemma cendpoint_relation_udpate_arch:
"\<lbrakk> cslift x p = Some tcb ; cendpoint_relation (cslift x) v v' \<rbrakk>
\<Longrightarrow> cendpoint_relation (cslift x(p \<mapsto> tcbArch_C_update f tcb)) v v'"
\<Longrightarrow> cendpoint_relation ((cslift x)(p \<mapsto> tcbArch_C_update f tcb)) v v'"
apply (clarsimp simp: cendpoint_relation_def Let_def tcb_queue_relation'_def
split: endpoint.splits)
apply (subst ep_queue_relation_shift2; simp add: fun_eq_iff)
Expand All @@ -1781,7 +1781,7 @@ lemma cendpoint_relation_udpate_arch:

lemma cnotification_relation_udpate_arch:
"\<lbrakk> cslift x p = Some tcb ; cnotification_relation (cslift x) v v' \<rbrakk>
\<Longrightarrow> cnotification_relation (cslift x(p \<mapsto> tcbArch_C_update f tcb)) v v'"
\<Longrightarrow> cnotification_relation ((cslift x)(p \<mapsto> tcbArch_C_update f tcb)) v v'"
apply (clarsimp simp: cnotification_relation_def Let_def tcb_queue_relation'_def
split: notification.splits ntfn.splits)
apply (subst ep_queue_relation_shift2; simp add: fun_eq_iff)
Expand Down
14 changes: 7 additions & 7 deletions proof/crefine/X64/IpcCancel_C.thy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2824,8 +2824,8 @@ lemma cpspace_relation_ep_update_an_ep:
and pal: "pspace_aligned' s" "pspace_distinct' s"
and others: "\<And>epptr' ep'. \<lbrakk> ko_at' ep' epptr' s; epptr' \<noteq> epptr; ep' \<noteq> IdleEP \<rbrakk>
\<Longrightarrow> set (epQueue ep') \<inter> (ctcb_ptr_to_tcb_ptr ` S) = {}"
shows "cmap_relation (map_to_eps (ksPSpace s(epptr \<mapsto> KOEndpoint ep')))
(cslift t(Ptr epptr \<mapsto> endpoint)) Ptr (cendpoint_relation mp')"
shows "cmap_relation (map_to_eps ((ksPSpace s)(epptr \<mapsto> KOEndpoint ep')))
((cslift t)(Ptr epptr \<mapsto> endpoint)) Ptr (cendpoint_relation mp')"
using cp koat pal rel unfolding cmap_relation_def
apply -
apply (clarsimp elim!: obj_atE' simp: map_comp_update projectKO_opts_defs)
Expand All @@ -2847,8 +2847,8 @@ lemma cpspace_relation_ep_update_ep:
and cp: "cmap_relation (map_to_eps (ksPSpace s)) (cslift t) Ptr (cendpoint_relation mp)"
and rel: "cendpoint_relation mp' ep' endpoint"
and mpeq: "(mp' |` (- (tcb_ptr_to_ctcb_ptr ` qs))) = (mp |` (- (tcb_ptr_to_ctcb_ptr ` qs)))"
shows "cmap_relation (map_to_eps (ksPSpace s(epptr \<mapsto> KOEndpoint ep')))
(cslift t(Ptr epptr \<mapsto> endpoint)) Ptr (cendpoint_relation mp')"
shows "cmap_relation (map_to_eps ((ksPSpace s)(epptr \<mapsto> KOEndpoint ep')))
((cslift t)(Ptr epptr \<mapsto> endpoint)) Ptr (cendpoint_relation mp')"
using invs
apply (intro cpspace_relation_ep_update_an_ep[OF koat cp rel mpeq])
apply clarsimp+
Expand All @@ -2860,15 +2860,15 @@ lemma cpspace_relation_ep_update_ep':
fixes ep :: "endpoint" and ep' :: "endpoint"
and epptr :: "machine_word" and s :: "kernel_state"
defines "qs \<equiv> if (isSendEP ep' \<or> isRecvEP ep') then set (epQueue ep') else {}"
defines "s' \<equiv> s\<lparr>ksPSpace := ksPSpace s(epptr \<mapsto> KOEndpoint ep')\<rparr>"
defines "s' \<equiv> s\<lparr>ksPSpace := (ksPSpace s)(epptr \<mapsto> KOEndpoint ep')\<rparr>"
assumes koat: "ko_at' ep epptr s"
and vp: "valid_pspace' s"
and cp: "cmap_relation (map_to_eps (ksPSpace s)) (cslift t) Ptr (cendpoint_relation mp)"
and srs: "sym_refs (state_refs_of' s')"
and rel: "cendpoint_relation mp' ep' endpoint"
and mpeq: "(mp' |` (- (tcb_ptr_to_ctcb_ptr ` qs))) = (mp |` (- (tcb_ptr_to_ctcb_ptr ` qs)))"
shows "cmap_relation (map_to_eps (ksPSpace s(epptr \<mapsto> KOEndpoint ep')))
(cslift t(Ptr epptr \<mapsto> endpoint)) Ptr (cendpoint_relation mp')"
shows "cmap_relation (map_to_eps ((ksPSpace s)(epptr \<mapsto> KOEndpoint ep')))
((cslift t)(Ptr epptr \<mapsto> endpoint)) Ptr (cendpoint_relation mp')"
proof -
from koat have koat': "ko_at' ep' epptr s'"
by (clarsimp simp: obj_at'_def s'_def objBitsKO_def ps_clear_def projectKOs)
Expand Down
21 changes: 11 additions & 10 deletions proof/crefine/X64/Ipc_C.thy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4820,12 +4820,12 @@ lemma sendIPC_enqueue_ccorres_helper:
apply (simp add: cendpoint_relation_def Let_def)
apply (case_tac ep, simp_all add: init_def valid_ep'_def)[1]
apply (subgoal_tac "sym_refs (state_refs_of' (\<sigma>\<lparr>ksPSpace :=
ksPSpace \<sigma>(epptr \<mapsto> KOEndpoint (SendEP queue))\<rparr>))")
(ksPSpace \<sigma>)(epptr \<mapsto> KOEndpoint (SendEP queue))\<rparr>))")
prefer 2
apply (clarsimp simp: state_refs_of'_upd ko_wp_at'_def
obj_at'_def projectKOs objBitsKO_def)
apply (subgoal_tac "ko_at' (SendEP queue) epptr (\<sigma>\<lparr>ksPSpace :=
ksPSpace \<sigma>(epptr \<mapsto> KOEndpoint (SendEP queue))\<rparr>)")
(ksPSpace \<sigma>)(epptr \<mapsto> KOEndpoint (SendEP queue))\<rparr>)")
prefer 2
apply (clarsimp simp: obj_at'_def projectKOs objBitsKO_def ps_clear_upd)
apply (intro conjI impI allI)
Expand Down Expand Up @@ -5241,12 +5241,12 @@ lemma receiveIPC_enqueue_ccorres_helper:
apply (simp add: cendpoint_relation_def Let_def)
apply (case_tac ep, simp_all add: init_def valid_ep'_def)[1]
apply (subgoal_tac "sym_refs (state_refs_of' (\<sigma>\<lparr>ksPSpace :=
ksPSpace \<sigma>(epptr \<mapsto> KOEndpoint (RecvEP queue))\<rparr>))")
(ksPSpace \<sigma>)(epptr \<mapsto> KOEndpoint (RecvEP queue))\<rparr>))")
prefer 2
apply (clarsimp simp: state_refs_of'_upd ko_wp_at'_def
obj_at'_def projectKOs objBitsKO_def)
apply (subgoal_tac "ko_at' (RecvEP queue) epptr (\<sigma>\<lparr>ksPSpace :=
ksPSpace \<sigma>(epptr \<mapsto> KOEndpoint (RecvEP queue))\<rparr>)")
(ksPSpace \<sigma>)(epptr \<mapsto> KOEndpoint (RecvEP queue))\<rparr>)")
prefer 2
apply (clarsimp simp: obj_at'_def projectKOs objBitsKO_def ps_clear_upd)
apply (intro conjI impI allI)
Expand Down Expand Up @@ -6291,16 +6291,17 @@ lemma cpspace_relation_ntfn_update_ntfn':
fixes ntfn :: "Structures_H.notification" and ntfn' :: "Structures_H.notification"
and ntfnptr :: "machine_word" and s :: "kernel_state"
defines "qs \<equiv> if isWaitingNtfn (ntfnObj ntfn') then set (ntfnQueue (ntfnObj ntfn')) else {}"
defines "s' \<equiv> s\<lparr>ksPSpace := ksPSpace s(ntfnptr \<mapsto> KONotification ntfn')\<rparr>"
defines "s' \<equiv> s\<lparr>ksPSpace := (ksPSpace s)(ntfnptr \<mapsto> KONotification ntfn')\<rparr>"
assumes koat: "ko_at' ntfn ntfnptr s"
and vp: "valid_pspace' s"
and cp: "cmap_relation (map_to_ntfns (ksPSpace s)) (cslift t) Ptr (cnotification_relation (cslift t))"
and srs: "sym_refs (state_refs_of' s')"
and rel: "cnotification_relation (cslift t') ntfn' notification"
and mpeq: "(cslift t' |` (- (tcb_ptr_to_ctcb_ptr ` qs))) = (cslift t |` (- (tcb_ptr_to_ctcb_ptr ` qs)))"
shows "cmap_relation (map_to_ntfns (ksPSpace s(ntfnptr \<mapsto> KONotification ntfn')))
(cslift t(Ptr ntfnptr \<mapsto> notification)) Ptr
(cnotification_relation (cslift t'))"
shows "cmap_relation (map_to_ntfns ((ksPSpace s)(ntfnptr \<mapsto> KONotification ntfn')))
((cslift t)(Ptr ntfnptr \<mapsto> notification))
Ptr
(cnotification_relation (cslift t'))"
proof -
from koat have koat': "ko_at' ntfn' ntfnptr s'"
by (clarsimp simp: obj_at'_def s'_def objBitsKO_def ps_clear_def projectKOs)
Expand Down Expand Up @@ -6376,12 +6377,12 @@ lemma receiveSignal_enqueue_ccorres_helper:
apply (simp add: cnotification_relation_def Let_def)
apply (case_tac "ntfnObj ntfn", simp_all add: init_def valid_ntfn'_def)[1]
apply (subgoal_tac "sym_refs (state_refs_of' (\<sigma>\<lparr>ksPSpace :=
ksPSpace \<sigma>(ntfnptr \<mapsto> KONotification (NTFN (WaitingNtfn queue) (ntfnBoundTCB ntfn)))\<rparr>))")
(ksPSpace \<sigma>)(ntfnptr \<mapsto> KONotification (NTFN (WaitingNtfn queue) (ntfnBoundTCB ntfn)))\<rparr>))")
prefer 2
apply (clarsimp simp: state_refs_of'_upd ko_wp_at'_def ntfnBound_state_refs_equivalence
obj_at'_def projectKOs objBitsKO_def)
apply (subgoal_tac "ko_at' (NTFN (WaitingNtfn queue) (ntfnBoundTCB ntfn)) ntfnptr (\<sigma>\<lparr>ksPSpace :=
ksPSpace \<sigma>(ntfnptr \<mapsto> KONotification (NTFN (WaitingNtfn queue) (ntfnBoundTCB ntfn)))\<rparr>)")
(ksPSpace \<sigma>)(ntfnptr \<mapsto> KONotification (NTFN (WaitingNtfn queue) (ntfnBoundTCB ntfn)))\<rparr>)")
prefer 2
apply (clarsimp simp: obj_at'_def projectKOs objBitsKO_def ps_clear_upd)
apply (intro conjI impI allI)
Expand Down
2 changes: 1 addition & 1 deletion proof/crefine/X64/PSpace_C.thy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -47,7 +47,7 @@ lemma setObject_ccorres_helper:
fixes ko :: "'a :: pspace_storable"
assumes valid: "\<And>\<sigma> (ko' :: 'a).
\<Gamma> \<turnstile> {s. (\<sigma>, s) \<in> rf_sr \<and> P \<sigma> \<and> s \<in> P' \<and> ko_at' ko' p \<sigma>}
c {s. (\<sigma>\<lparr>ksPSpace := ksPSpace \<sigma> (p \<mapsto> injectKO ko)\<rparr>, s) \<in> rf_sr}"
c {s. (\<sigma>\<lparr>ksPSpace := (ksPSpace \<sigma>)(p \<mapsto> injectKO ko)\<rparr>, s) \<in> rf_sr}"
shows "\<lbrakk> \<And>ko :: 'a. updateObject ko = updateObject_default ko;
\<And>ko :: 'a. (1 :: machine_word) < 2 ^ objBits ko \<rbrakk>
\<Longrightarrow> ccorres dc xfdc P P' hs (setObject p ko) c"
Expand Down
6 changes: 3 additions & 3 deletions proof/crefine/X64/Recycle_C.thy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -454,7 +454,7 @@ lemma mapM_x_store_memset_ccorres_assist:
"\<And>ko :: 'a. (1 :: machine_word) < 2 ^ objBits ko"
assumes restr: "set slots \<subseteq> S"
assumes worker: "\<And>ptr s s' (ko :: 'a). \<lbrakk> (s, s') \<in> rf_sr; ko_at' ko ptr s; ptr \<in> S \<rbrakk>
\<Longrightarrow> (s \<lparr> ksPSpace := ksPSpace s (ptr \<mapsto> injectKO val)\<rparr>,
\<Longrightarrow> (s \<lparr> ksPSpace := (ksPSpace s)(ptr \<mapsto> injectKO val)\<rparr>,
globals_update (t_hrs_'_update (hrs_mem_update
(heap_update_list ptr
(replicateHider (2 ^ objBits val) (ucast c))))) s') \<in> rf_sr"
Expand Down Expand Up @@ -793,8 +793,8 @@ lemma cpspace_relation_ep_update_ep2:
(cslift t) ep_Ptr (cendpoint_relation (cslift t));
cendpoint_relation (cslift t') ep' endpoint;
(cslift t' :: tcb_C ptr \<rightharpoonup> tcb_C) = cslift t \<rbrakk>
\<Longrightarrow> cmap_relation (map_to_eps (ksPSpace s(epptr \<mapsto> KOEndpoint ep')))
(cslift t(ep_Ptr epptr \<mapsto> endpoint))
\<Longrightarrow> cmap_relation (map_to_eps ((ksPSpace s)(epptr \<mapsto> KOEndpoint ep')))
((cslift t)(ep_Ptr epptr \<mapsto> endpoint))
ep_Ptr (cendpoint_relation (cslift t'))"
apply (rule cmap_relationE1, assumption, erule ko_at_projectKO_opt)
apply (rule_tac P="\<lambda>a. cmap_relation a b c d" for b c d in rsubst,
Expand Down
2 changes: 1 addition & 1 deletion proof/crefine/X64/Retype_C.thy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6121,7 +6121,7 @@ lemma gsCNodes_update_ccorres:

(* FIXME: move *)
lemma map_to_tcbs_upd:
"map_to_tcbs (ksPSpace s(t \<mapsto> KOTCB tcb')) = map_to_tcbs (ksPSpace s)(t \<mapsto> tcb')"
"map_to_tcbs ((ksPSpace s)(t \<mapsto> KOTCB tcb')) = (map_to_tcbs (ksPSpace s))(t \<mapsto> tcb')"
apply (rule ext)
apply (clarsimp simp: map_comp_def projectKOs split: option.splits if_splits)
done
Expand Down
Loading

0 comments on commit 1f3d1f6

Please sign in to comment.