-
Notifications
You must be signed in to change notification settings - Fork 0
/
SubMonad_R.thy
143 lines (125 loc) · 5.67 KB
/
SubMonad_R.thy
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
(*
* Copyright 2014, General Dynamics C4 Systems
*
* This software may be distributed and modified according to the terms of
* the GNU General Public License version 2. Note that NO WARRANTY is provided.
* See "LICENSE_GPLv2.txt" for details.
*
* @TAG(GD_GPL)
*)
theory SubMonad_R
imports KHeap_R EmptyFail
begin
(* SubMonadLib *)
lemma submonad_doMachineOp:
"submonad ksMachineState (ksMachineState_update \<circ> K) \<top> doMachineOp"
apply (unfold_locales)
apply (clarsimp simp: ext stateAssert_def doMachineOp_def o_def gets_def
get_def bind_def return_def submonad_fn_def)+
done
interpretation submonad_doMachineOp:
submonad ksMachineState "(ksMachineState_update \<circ> K)" \<top> doMachineOp
by (rule submonad_doMachineOp)
lemma corres_machine_op:
assumes P: "corres_underlying Id True r \<top> \<top> x x'"
shows "corres r \<top> \<top> (do_machine_op x) (doMachineOp x')"
apply (rule corres_submonad [OF submonad_do_machine_op submonad_doMachineOp _ _ P])
apply (simp_all add: state_relation_def swp_def)
done
lemma doMachineOp_mapM:
assumes "\<And>x. empty_fail (m x)"
shows "doMachineOp (mapM m l) = mapM (doMachineOp \<circ> m) l"
apply (rule submonad_mapM [OF submonad_doMachineOp submonad_doMachineOp,
simplified])
apply (rule assms)
done
lemma doMachineOp_mapM_x:
assumes "\<And>x. empty_fail (m x)"
shows "doMachineOp (mapM_x m l) = mapM_x (doMachineOp \<circ> m) l"
apply (rule submonad_mapM_x [OF submonad_doMachineOp submonad_doMachineOp,
simplified])
apply (rule assms)
done
lemma submonad_args_ksPSpace:
"submonad_args ksPSpace (ksPSpace_update o (\<lambda>x _. x)) \<top>"
by (simp add: submonad_args_def K_def)
definition
"asUser_fetch \<equiv> \<lambda>t s. case (ksPSpace s t) of
Some (KOTCB tcb) \<Rightarrow> tcbContext tcb
| None \<Rightarrow> undefined"
definition
"asUser_replace \<equiv> \<lambda>t uc s.
let obj = case (ksPSpace s t) of
Some (KOTCB tcb) \<Rightarrow> Some (KOTCB (tcb \<lparr>tcbContext := uc\<rparr>))
| obj \<Rightarrow> obj
in s \<lparr> ksPSpace := (ksPSpace s) (t := obj) \<rparr>"
lemma threadGet_stateAssert_gets_asUser:
"threadGet tcbContext t = do stateAssert (tcb_at' t) []; gets (asUser_fetch t) od"
apply (rule is_stateAssert_gets [OF _ _ empty_fail_threadGet no_fail_threadGet])
apply (clarsimp simp: threadGet_def liftM_def, wp)
apply (simp add: threadGet_def liftM_def, wp getObject_tcb_at')
apply (simp add: threadGet_def liftM_def, wp)
apply (rule hoare_strengthen_post, wp getObject_obj_at')
apply (simp add: objBits_def objBitsKO_def)+
apply (clarsimp simp: obj_at'_def asUser_fetch_def projectKOs)
done
lemma threadSet_modify_asUser:
"tcb_at' t st \<Longrightarrow>
threadSet (tcbContext_update (\<lambda>_. uc)) t st = modify (asUser_replace t uc) st"
apply (rule is_modify [OF _ empty_fail_threadSet no_fail_threadSet])
apply (clarsimp simp: threadSet_def setObject_def split_def
updateObject_default_def)
apply wp
apply (rule_tac Q="\<lambda>rv. obj_at' (op = rv) t and (op = st)" in hoare_post_imp)
apply (clarsimp simp: asUser_replace_def Let_def obj_at'_def
projectKOs fun_upd_def
split: option.split kernel_object.split)
apply (wp getObject_obj_at' | clarsimp simp: objBits_def objBitsKO_def)+
done
lemma submonad_asUser:
"submonad (asUser_fetch t) (asUser_replace t) (tcb_at' t) (asUser t)"
apply (unfold_locales)
apply (clarsimp simp: asUser_fetch_def asUser_replace_def
Let_def obj_at'_def projectKOs
split: kernel_object.split option.split)
apply (clarsimp simp: asUser_replace_def Let_def
split: kernel_object.split option.split)
apply (case_tac tcb, simp)
apply (clarsimp simp: asUser_fetch_def asUser_replace_def Let_def
fun_upd_idem
split: kernel_object.splits option.splits)
apply (case_tac tcb, simp add: map_upd_triv)
apply (clarsimp simp: obj_at'_def asUser_replace_def Let_def projectKOs
split: kernel_object.splits option.splits)
apply (case_tac tcb, simp add: objBitsKO_def ps_clear_def)
apply (rule ext)
apply (clarsimp simp: submonad_fn_def asUser_def bind_assoc split_def)
apply (subst threadGet_stateAssert_gets_asUser, simp add: bind_assoc, rule ext)
apply (rule bind_apply_cong [OF refl])+
apply (rule bind_apply_cong [OF threadSet_modify_asUser])
apply (clarsimp simp: in_monad stateAssert_def select_f_def)
apply (rule refl)
done
interpretation submonad_asUser:
submonad "asUser_fetch t" "asUser_replace t" "tcb_at' t" "asUser t"
by (rule submonad_asUser)
lemma asUser_doMachineOp_comm:
"\<lbrakk> empty_fail m; empty_fail m' \<rbrakk> \<Longrightarrow>
do x \<leftarrow> asUser t m; y \<leftarrow> doMachineOp m'; n x y od =
do y \<leftarrow> doMachineOp m'; x \<leftarrow> asUser t m; n x y od"
apply (rule submonad_comm [OF submonad.axioms(1) [OF submonad_asUser]
submonad.axioms(1) [OF submonad_doMachineOp]])
apply (simp add: submonad.fn_is_sm [OF submonad_asUser])
apply (simp add: submonad.fn_is_sm [OF submonad_doMachineOp])
apply (simp add: asUser_replace_def Let_def)
apply simp
apply (rule refl)
apply assumption+
done
lemma doMachineOp_nosch [wp]:
"\<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> doMachineOp m \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace>"
apply (simp add: doMachineOp_def split_def)
apply (wp select_f_wp)
apply simp
done
end