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
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
|
theory Prompt_monad_extras
imports Prompt_monad
begin
lemma All_bind_dom: "bind_dom (oc, f)"
by (induction oc) (auto intro: bind.domintros; blast intro: bind.domintros)+
termination bind using All_bind_dom by auto
lemma bind_induct[case_names Done Read_mem Read_reg Write_memv Excl_res Write_ea Barrier Footprint Write_reg Escape Fail Error Exception Internal]:
fixes m :: "('a, 'e) outcome" and f :: "'a \<Rightarrow> ('b, 'e) outcome"
assumes "\<And>a f. P (Done a) f"
and "\<And>rk addr sz k f. (\<And>v m' opt. (m', opt) = k v \<Longrightarrow> P m' f) \<Longrightarrow> P (Read_mem (rk, addr, sz) k) f"
and "\<And>reg k f. (\<And>v m' opt. (m', opt) = k v \<Longrightarrow> P m' f) \<Longrightarrow> P (Read_reg reg k) f"
and "\<And>val k f. (\<And>v m' opt. (m', opt) = k v \<Longrightarrow> P m' f) \<Longrightarrow> P (Write_memv val k) f"
and "\<And>k f. (\<And>v m' opt. (m', opt) = k v \<Longrightarrow> P m' f) \<Longrightarrow> P (Excl_res k) f"
and "\<And>wk addr sz m opt f. P m f \<Longrightarrow> P (Write_ea (wk, addr, sz) (m, opt)) f"
and "\<And>bk m opt f. P m f \<Longrightarrow> P (Barrier bk (m, opt)) f"
and "\<And>m opt f. P m f \<Longrightarrow> P (Footprint (m, opt)) f"
and "\<And>reg val m opt f. P m f \<Longrightarrow> P (Write_reg (reg, val) (m, opt)) f"
and "\<And>descr f. P (Escape descr) f"
and "\<And>descr f. P (Fail descr) f" and "\<And>descr f. P (Error descr) f" and "\<And>e f. P (Exception e) f"
and "\<And>i m opt f. P m f \<Longrightarrow> P (Internal i (m, opt)) f"
shows "P m f"
by (rule bind.induct[split_format (complete), OF assms]; blast)
datatype event =
(* Request to read memory *)
Read_mem read_kind address_lifted nat memory_value
(* Write is imminent, at address lifted, of size nat *)
| Write_ea write_kind address_lifted nat
(* Request the result of store-exclusive *)
| Excl_res bool
(* Request to write memory at last signalled address. Memory value should be 8
times the size given in ea signal *)
| Write_memv memory_value bool
(* Request a memory barrier *)
| Barrier " barrier_kind "
(* Tell the system to dynamically recalculate dependency footprint *)
| Footprint
(* Request to read register *)
| Read_reg reg_name register_value
(* Request to write register *)
| Write_reg reg_name register_value
| Internal " ( string option * (unit \<Rightarrow> string)option) "
inductive_set T :: "(('a, 'e)outcome \<times> event \<times> ('a, 'e)outcome) set" where
Read_mem: "\<exists>opt. k v = (m, opt) \<Longrightarrow> ((outcome.Read_mem (rk, addr, sz) k), Read_mem rk addr sz v, m) \<in> T"
| Write_ea: "\<exists>opt. k = (m, opt) \<Longrightarrow> ((outcome.Write_ea (rk, addr, sz) k), Write_ea rk addr sz, m) \<in> T"
| Excl_res: "\<exists>opt. k r = (m, opt) \<Longrightarrow> ((outcome.Excl_res k), Excl_res r, m) \<in> T"
| Write_memv: "\<exists>opt. k r = (m, opt) \<Longrightarrow> ((outcome.Write_memv v k), Write_memv v r, m) \<in> T"
| Barrier: "\<exists>opt. k = (m, opt) \<Longrightarrow> ((outcome.Barrier bk k), Barrier bk, m) \<in> T"
| Footprint: "\<exists>opt. k = (m, opt) \<Longrightarrow> ((outcome.Footprint k), Footprint, m) \<in> T"
| Read_reg: "\<exists>opt. k v = (m, opt) \<Longrightarrow> ((outcome.Read_reg r k), Read_reg r v, m) \<in> T"
| Write_reg: "\<exists>opt. k = (m, opt) \<Longrightarrow> ((outcome.Write_reg (r, v) k), Write_reg r v, m) \<in> T"
| Internal: "\<exists>opt. k = (m, opt) \<Longrightarrow> ((outcome.Internal descr k), Internal descr, m) \<in> T"
inductive_set Traces :: "(('a, 'r)outcome \<times> event list \<times> ('a, 'r)outcome) set" where
Nil: "(s, [], s) \<in> Traces"
| Step: "\<lbrakk>(s, e, s'') \<in> T; (s'', t, s') \<in> Traces\<rbrakk> \<Longrightarrow> (s, e # t, s') \<in> Traces"
declare Traces.intros[intro]
declare T.intros[intro]
declare prod.splits[split]
(* lemma fst_case_bind[simp]: "fst (case k of (o1, x) \<Rightarrow> (bind o1 f, x)) = bind (fst k) f"
by (cases k) auto *)
lemmas Traces_ConsI = T.intros[THEN Step, rotated]
inductive_cases Traces_NilE[elim]: "(s, [], s') \<in> Traces"
inductive_cases Traces_ConsE[elim]: "(s, e # t, s') \<in> Traces"
abbreviation Run :: "('a, 'r)outcome \<Rightarrow> event list \<Rightarrow> 'a \<Rightarrow> bool"
where "Run s t a \<equiv> (s, t, Done a) \<in> Traces"
lemma Run_appendI:
assumes "(s, t1, s') \<in> Traces"
and "Run s' t2 a"
shows "Run s (t1 @ t2) a"
proof (use assms in \<open>induction t1 arbitrary: s\<close>)
case (Cons e t1)
then show ?case by (elim Traces_ConsE) auto
qed auto
lemma bind_DoneE:
assumes "bind m f = outcome.Done a"
obtains a' where "m = outcome.Done a'" and "f a' = outcome.Done a"
using assms by (auto elim: bind.elims)
lemma bind_T_cases:
assumes "(bind m f, e, s') \<in> T"
obtains (Done) a where "m = Done a"
| (Bind) m' where "s' = bind m' f" and "(m, e, m') \<in> T"
proof cases
assume D: "\<forall>a. m \<noteq> Done a"
show thesis using assms proof cases
case (Read_mem k v rk addr sz)
then obtain k' where "m = outcome.Read_mem (rk, addr, sz) k'" using D by (cases m) auto
then show ?thesis using Read_mem by (intro Bind[of "fst (k' v)"]) auto
next
case (Write_ea k rk addr sz)
then obtain k' where "m = outcome.Write_ea (rk, addr, sz) k'" using D by (cases m) auto
then show ?thesis using Write_ea by (intro Bind[of "fst k'"]) auto
next
case (Excl_res k r)
then obtain k' where "m = outcome.Excl_res k'" using D by (cases m) auto
then show ?thesis using Excl_res by (intro Bind[of "fst (k' r)"]) auto
next
case (Write_memv k r v)
then obtain k' where "m = outcome.Write_memv v k'" using D by (cases m) auto
then show ?thesis using Write_memv by (intro Bind[of "fst (k' r)"]) auto
next
case (Barrier k bk)
then obtain k' where "m = outcome.Barrier bk k'" using D by (cases m) auto
then show ?thesis using Barrier by (intro Bind[of "fst k'"]) auto
next
case (Footprint k)
then obtain k' where "m = outcome.Footprint k'" using D by (cases m) auto
then show ?thesis using Footprint by (intro Bind[of "fst k'"]) auto
next
case (Read_reg k v r)
then obtain k' where "m = outcome.Read_reg r k'" using D by (cases m) auto
then show ?thesis using Read_reg by (intro Bind[of "fst (k' v)"]) (auto split: prod.splits)
next
case (Write_reg k r v)
then obtain k' where "m = outcome.Write_reg (r, v) k'" using D by (cases m) auto
then show ?thesis using Write_reg by (intro Bind[of "fst k'"]) auto
next
case (Internal k descr)
then obtain k' where "m = outcome.Internal descr k'" using D by (cases m) auto
then show ?thesis using Internal by (intro Bind[of "fst k'"]) auto
qed
qed auto
lemma Run_bindE:
fixes m :: "('b, 'r) outcome" and a :: 'a
assumes "Run (bind m f) t a"
obtains tm am tf where "t = tm @ tf" and "Run m tm am" and "Run (f am) tf a"
proof (use assms in \<open>induction "bind m f" t "Done a :: ('a,'r) outcome" arbitrary: m rule: Traces.induct\<close>)
case Nil
obtain am where "m = Done am" and "f am = Done a" using Nil(1) by (elim bind_DoneE)
then show ?case by (intro Nil(2)) auto
next
case (Step e s'' t m)
show thesis using Step(1)
proof (cases rule: bind_T_cases)
case (Done am)
then show ?thesis using Step(1,2) by (intro Step(4)[of "[]" "e # t" am]) auto
next
case (Bind m')
show ?thesis proof (rule Step(3)[OF Bind(1)])
fix tm tf am
assume "t = tm @ tf" and "Run m' tm am" and "Run (f am) tf a"
then show thesis using Bind by (intro Step(4)[of "e # tm" tf am]) auto
qed
qed
qed
lemma Run_DoneE:
assumes "Run (Done a) t a'"
obtains "t = []" and "a' = a"
using assms by (auto elim: Traces.cases T.cases)
lemma Run_Done_iff_Nil[simp]: "Run (Done a) t a' \<longleftrightarrow> t = [] \<and> a' = a"
by (auto elim: Run_DoneE)
lemma Run_BarrierE[elim!]:
assumes "Run (outcome.Barrier bk k) t a"
obtains t' where "t = Barrier bk # t'" and "Run (fst k) t' a"
using assms by cases (auto elim: T.cases)
lemma bind_cong[fundef_cong]:
assumes m: "m1 = m2"
and f: "\<And>t a. Run m2 t a \<Longrightarrow> f1 a = f2 a"
shows "bind m1 f1 = bind m2 f2"
proof (unfold m, use f in \<open>induction m2 f1 arbitrary: f2 rule: bind_induct\<close>)
case (Read_mem rk addr sz k f)
have "bind m' f = bind m' f2" if k: "k v = (m', opt)" for v m' opt
using k by (auto intro!: Read_mem.IH[of _ opt v] Read_mem.prems)
then show ?case by auto
next
case (Read_reg reg k f)
have "bind m' f = bind m' f2" if k: "k v = (m', opt)" for v m' opt
using k by (auto intro!: Read_reg.IH[of _ opt v] Read_reg.prems)
then show ?case by auto
next
case (Write_memv val k f)
have "bind m' f = bind m' f2" if k: "k v = (m', opt)" for v m' opt
using k by (auto intro!: Write_memv.IH[of _ opt v] Write_memv.prems)
then show ?case by auto
next
case (Excl_res k f)
have "bind m' f = bind m' f2" if k: "k v = (m', opt)" for v m' opt
using k by (auto intro!: Excl_res.IH[of _ opt v] Excl_res.prems)
then show ?case by auto
next
case (Write_ea wk addr sz m opt f)
show ?case by (auto intro!: Write_ea)
next
case (Barrier bk m opt f)
show ?case by (auto intro!: Barrier)
next
case (Footprint m opt f)
show ?case by (auto intro!: Footprint)
next
case (Write_reg reg val m opt f)
show ?case by (auto intro!: Write_reg)
next
case (Internal i m opt f)
show ?case by (auto intro!: Internal)
qed auto
end
|
