1(*
2 * Copyright 2017, Data61
3 * Commonwealth Scientific and Industrial Research Organisation (CSIRO)
4 * ABN 41 687 119 230.
5 *
6 * This software may be distributed and modified according to the terms of
7 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
8 * See "LICENSE_BSD2.txt" for details.
9 *
10 * @TAG(DATA61_BSD)
11 *)
12
13chapter \<open>Extending C refinement proofs using AutoCorres\<close>
14
15theory AutoCorres_C
16imports
17  Corres_C
18  AutoCorresModifiesProofs
19begin
20
21text \<open>
22This theory provides some tools for extending existing collections of C refinement proofs,
23which use the @{term ccorresG} framework, with new proofs using the higher-level
24@{term corres_underlying} framework. We use AutoCorres to move between the frameworks.
25
26See AutoCorresTest for examples.
27\<close>
28
29section \<open>Setup\<close>
30
31text \<open>
32The imports for this theory cause a merge between AutoCorres and the preamble for CRefine.
33AutoCorres both adds to and deletes from various rule sets, such that the merge produces
34an entirely new theory context, which is unfamiliar to any previous CRefine or AutoCorres
35development. In particular, rules which were deleted in AutoCorres may reappear in this
36theory, but in a different place in the rule set than they appeared in Corres_C.
37
38The following setup restores the ordering from @{theory CRefine.Corres_C} for the crucial
39@{attribute wp_comb} rule set, and places new rules introduced by @{theory AutoCorres.AutoCorres} at
40the end of the @{attribute wp_comb} set.
41
42To ensure that we only have to do this once, we are careful to ensure that there is only
43one theory merge between AutoCorres and CRefine. We import @{theory CRefine.L4VerifiedLinks} into
44@{theory CRefine.AutoCorresModifiesProofs}, and import the latter here. This satisfies the
45dependencies from @{theory CRefine.AutoCorresModifiesProofs} to @{theory AutoCorres.AutoCorres}, and from
46this theory to @{theory CRefine.L4VerifiedLinks} and @{theory CRefine.Corres_C}, without duplicating
47theory merges. Finally, we list @{theory CRefine.L4VerifiedLinks} as a top-level theory in the
48CBaseRefine session, so that @{theory AutoCorres.AutoCorres} need not be processed in a CRefine
49session, but do not import @{theory AutoCorres.AutoCorres} into @{text CBaseRefine.Include_C}, since that would
50cause a redundant theory merge.
51\<close>
52
53setup \<open>
54  fn thy => let
55    fun get_combs thy = #combs (WeakestPre.get_rules (Proof_Context.init_global thy) [])
56    val corres_c_combs = get_combs (Context.get_theory {long=true} thy "CRefine.Corres_C")
57    val accorres_combs = get_combs thy
58    val subtract_thms = subtract (fn (a,b) => Thm.prop_of a = Thm.prop_of b)
59    val accorres_extra = subtract_thms corres_c_combs accorres_combs
60    fun upd attr = fold_rev (snd oo Thm.apply_attribute attr)
61    val add = upd WeakestPre.combs_add
62    val del = upd WeakestPre.combs_del
63    val upd_gen = add corres_c_combs o add accorres_extra o del accorres_combs
64  in Context.theory_of (upd_gen (Context.Theory thy)) end
65\<close>
66
67text \<open>
68AutoCorres adds some rules about @{term whenE} to the @{attribute wp} set, which don't always
69behave nicely. They introduce @{term If} expressions into pre and post conditions, where they
70don't always simplify as one might expect. We replace them with a rule that does allow the
71conditional to simplify away more often.
72
73FIXME: Move this change into AutoCorres itself, or the underlying VCG library.
74\<close>
75
76lemmas [wp del] =
77  NonDetMonadEx.validE_whenE
78  NonDetMonadVCG.hoare_whenE_wps
79
80lemmas hoare_whenE_wp2 [wp] =
81  NonDetMonadVCG.hoare_whenE_wps[simplified if_apply_def2]
82
83section \<open>Rules for proving @{term ccorres_underlying} goals\<close>
84
85text \<open>
86Following are rules for converting a @{term ccorresG} goal to a @{term corres_underlying}
87goal, by making use of an automatically generated @{term ac_corres} fact about the procedure.
88
89For the first two of these, the user is expected to specify the return-value relation for the
90resulting @{term corres_underlying} goal, and will be required to prove that it implies the
91return-value relation of the original @{term ccorresG} goal.
92
93In the general case, the C can return some extra information via global variables.
94\<close>
95
96(* FIXME: provide a way to use this rule, and its rv_spec version, in ac_init. *)
97lemma corres_to_ccorres_extra_globals:
98  assumes rf_sr_def: "rf_sr \<equiv> {(s,s'). cstate_relation s (globals s')}"
99  assumes acc: "ac_corres globals check_term \<Gamma> ret_xf G (liftE ac) c"
100  assumes cac: "corres_underlying {(s,s'). cstate_relation s s'} True True
101                                  R P Q a (do x \<leftarrow> ac; y \<leftarrow> gets g; return (x,y) od)"
102  assumes pre: "\<And>s s'. cstate_relation s (globals s') \<Longrightarrow> P' s \<and> s' \<in> Q' \<Longrightarrow> P s \<and> Q (globals s')"
103  assumes p_g: "\<And>s s'. cstate_relation s (globals s') \<Longrightarrow> P' s \<and> s' \<in> Q' \<Longrightarrow> G s'"
104  assumes ret: "\<And>r s'. R r (ret_xf s', g (globals s')) \<longrightarrow> R' r (ret_xf' s')"
105  shows "ccorresG rf_sr \<Gamma> R' ret_xf' P' Q' [] a c"
106  unfolding rf_sr_def using ac_corres_ccorres_underlying[OF acc]
107  apply (clarsimp intro!: ccorresI')
108  apply (frule corres_underlyingD[OF cac, simplified], (simp add: pre)+)
109  apply (clarsimp simp: bind_def return_def simpler_gets_def)
110  apply (erule ccorresE, simp+, erule p_g, simp+)
111    apply (simp add: liftE_def)
112   apply assumption
113  apply (fastforce simp: unif_rrel_def dest: mp[OF ret] split: xstate.splits)
114  done
115
116text \<open>
117In the case where there is no extra information returned via global variables, the rule is simpler.
118\<close>
119
120lemma corres_to_ccorres:
121  assumes rf_sr_def: "rf_sr \<equiv> {(s,s'). cstate_relation s (globals s')}"
122  assumes acc: "ac_corres globals check_term \<Gamma> ret_xf G (liftE ac) c"
123  assumes cac: "corres_underlying {(s,s'). cstate_relation s s'} True True R P Q a ac"
124  assumes pre: "\<And>s s'. cstate_relation s (globals s') \<Longrightarrow> P' s \<and> s' \<in> Q' \<Longrightarrow> P s \<and> Q (globals s')"
125  assumes p_g: "\<And>s s'. cstate_relation s (globals s') \<Longrightarrow> P' s \<and> s' \<in> Q' \<Longrightarrow> G s'"
126  assumes ret: "\<And>r s'. R r (ret_xf s') \<longrightarrow> R' r (ret_xf' s')"
127  shows "ccorresG rf_sr \<Gamma> R' ret_xf' P' Q' [] a c"
128  apply (rule corres_to_ccorres_extra_globals[OF rf_sr_def acc, where g="K ()" and R="\<lambda>v. R v o fst"])
129     apply (simp add: liftM_def[symmetric])
130     apply (rule corres_rel_imp, rule cac)
131     apply (auto simp: pre p_g ret)
132  done
133
134text \<open>
135In the following versions of the above rules, the return-value relation for the resulting
136@{term corres_underlying} goal is fixed to a reasonably general relation. In cases where this
137return-value relation is good enough, it saves the effort of explicitly specifying a return-value
138relation.
139\<close>
140
141lemma corres_to_ccorres_extra_globals_rv_spec:
142  assumes "rf_sr \<equiv> {(s,s'). cstate_relation s (globals s')}"
143  assumes "ac_corres globals check_term \<Gamma> ret_xf G (liftE ac) c"
144  assumes "corres_underlying {(s,s'). cstate_relation s s'} True True
145                             (\<lambda>r (x,y). \<forall>s'. x = ret_xf s' \<and> y = g (globals s') \<longrightarrow> R' r (ret_xf' s'))
146                             P Q a (do x \<leftarrow> ac; y \<leftarrow> gets g; return (x, y) od)"
147  assumes "\<And>s s'. cstate_relation s (globals s') \<Longrightarrow> P' s \<and> s' \<in> Q' \<Longrightarrow> P s \<and> Q (globals s')"
148  assumes "\<And>s s'. cstate_relation s (globals s') \<Longrightarrow> P' s \<and> s' \<in> Q' \<Longrightarrow> G s'"
149  shows "ccorresG rf_sr \<Gamma> R' ret_xf' P' Q' [] a c"
150  using assms by (auto intro: corres_to_ccorres_extra_globals)
151
152lemma corres_to_ccorres_rv_spec:
153  assumes "rf_sr \<equiv> {(s,s'). cstate_relation s (globals s')}"
154  assumes "ac_corres globals check_term \<Gamma> ret_xf G (liftE ac) c"
155  assumes "corres_underlying {(s,s'). cstate_relation s s'} True True
156                             (\<lambda>r r'. \<forall>s'. r' = ret_xf s' \<longrightarrow> R' r (ret_xf' s')) P Q a ac"
157  assumes "\<And>s s'. cstate_relation s (globals s') \<Longrightarrow> P' s \<and> s' \<in> Q' \<Longrightarrow> P s \<and> Q (globals s')"
158  assumes "\<And>s s'. cstate_relation s (globals s') \<Longrightarrow> P' s \<and> s' \<in> Q' \<Longrightarrow> G s'"
159  shows "ccorresG rf_sr \<Gamma> R' ret_xf' P' Q' [] a c"
160  using assms by (auto intro: corres_to_ccorres)
161
162section \<open>Rules for importing @{term ccorresG} facts\<close>
163
164text \<open>
165While proving a @{term corres_underlying} goal which was obtained from a @{term ccorresG} goal,
166we might want to make use of existing @{term ccorresG} facts about called procedures. Following
167are rules for converting existing @{term ccorresG} facts to suitable @{term corres_underlying}
168facts.
169\<close>
170
171lemma in_AC_call_simpl:
172  fixes r s s' arg_pred ret_xf \<Gamma> f_'proc
173  shows "(r, s') \<in> fst (AC_call_L1 arg_pred globals ret_xf (L1_call_simpl check_term \<Gamma> f_'proc) s) \<Longrightarrow>
174         \<exists>cs cs'. s = globals cs \<and> arg_pred cs \<and>
175                  (check_term \<longrightarrow> \<Gamma> \<turnstile> Call f_'proc \<down> Normal cs) \<and>
176                  \<Gamma> \<turnstile> \<langle>Call f_'proc, Normal cs\<rangle> \<Rightarrow> Normal cs' \<and>
177                  s' = globals cs' \<and> r = ret_xf cs'"
178  apply (clarsimp simp: AC_call_L1_def L2_call_L1_def L1_call_simpl_def
179                        in_monad liftM_def select_def select_f_def
180                 split: xstate.splits sum.splits)
181  apply (rename_tac cs cs' status; case_tac status; fastforce)
182  done
183
184text \<open>
185Given a @{term ccorresG} fact, we need to process its preconditions to obtain a
186@{term corres_underlying} fact in a usable form. The following definition, rules and method
187provide some machinery for this processing.
188
189For a @{term ccorresG} rule about a procedure call, the concrete precondition typically
190describes how local variables in the C state relate to the arguments of the abstract procedure
191call. In some cases, it might also talk about the global C state.
192
193For the conversion from @{term ccorresG} to @{term corres_underlying}, we will use AutoCorres
194to generate an abstract wrapper around the C call. The wrapper will also have a precondition
195describing the relationship between local variables in the C state, and arguments to the
196wrapper.
197
198The purpose of this machinery, then, is to partition the components of the @{term ccorresG}
199precondition. Preconditions concerning function arguments are matched between the @{term ccorresG}
200fact and the AutoCorres-generated wrapper, and need not appear in the preconditions of the
201resulting @{term ccorres_underlying} rule. On the other hand, preconditions concerning global
202state must appear in the resulting @{term ccorres_underlying} rule.
203\<close>
204
205definition
206  "ccorres_to_corres_pre Q E Q' s' \<equiv> Q (globals s') \<longrightarrow> E s' \<and> s' \<in> Q'"
207
208text \<open>
209In @{term ccorres_to_corres_pre}, parameter @{term Q'} is the @{term ccorresG} precondition
210begin analysed; parameter @{term Q} is a schematic variable for what will become the precondition
211of the resulting @{term ccorres_underlying} rule, and therefore only concerns global state; and
212parameter @{term E} accumulates equalities between arguments to the AutoCorres-generated wrapper
213and the arguments to the abstract function call in the @{term ccorresG} fact.
214\<close>
215
216text \<open>
217Preconditions concerning global variables are incorporated into the precondition of the
218resulting @{term ccorres_underlying} fact.
219\<close>
220lemma ccorres_to_corres_pre_globals_Int:
221  assumes "ccorres_to_corres_pre Q E Q' s'"
222  shows "ccorres_to_corres_pre (P and Q) E ({s'. P (globals s')} \<inter> Q') s'"
223  using assms by (simp add: ccorres_to_corres_pre_def)
224
225lemmas ccorres_to_corres_pre_globals_base
226  = ccorres_to_corres_pre_globals_Int[where Q'=UNIV, simplified Int_UNIV_right]
227
228text \<open>
229For preconditions concerning function arguments, we can eliminate any mention of C local
230variable state, and are left with a predicate on the argument to AutoCorres-generated
231wrapper. Typically, this will be a relation to an argument to the abstract call in the
232@{term ccorresG} fact.
233\<close>
234lemma ccorres_to_corres_pre_local_Int:
235  assumes "f s' = x"
236  assumes "ccorres_to_corres_pre Q (K (P x) and E) Q' s'"
237  shows "ccorres_to_corres_pre Q E ({s'. P (f s')} \<inter> Q') s'"
238  using assms by (simp add: ccorres_to_corres_pre_def)
239
240lemmas ccorres_to_corres_pre_local_base
241  = ccorres_to_corres_pre_local_Int[where Q'=UNIV, simplified Int_UNIV_right]
242
243lemma ccorres_to_corres_pre_UNIV_Int:
244  assumes "ccorres_to_corres_pre Q E Q' s'"
245  shows "ccorres_to_corres_pre Q E (UNIV \<inter> Q') s'"
246  using assms by (simp add: ccorres_to_corres_pre_def)
247
248lemmas ccorres_to_corres_pre_intros =
249  ccorres_to_corres_pre_UNIV_Int
250  ccorres_to_corres_pre_globals_Int
251  ccorres_to_corres_pre_globals_base
252
253lemmas ccorres_to_corres_pre_elims =
254  ccorres_to_corres_pre_local_Int
255  ccorres_to_corres_pre_local_base
256
257lemma ccorres_to_corres_pre_finalise:
258  "E s' \<Longrightarrow> ccorres_to_corres_pre \<top> E UNIV s'"
259  by (simp add: ccorres_to_corres_pre_def)
260
261method ccorres_to_corres_pre_step =
262  (rule ccorres_to_corres_pre_intros | erule ccorres_to_corres_pre_elims)
263
264method ccorres_to_corres_pre_process = (
265  (elim pred_andE)?,
266  (simp only: Int_assoc)?,
267  (ccorres_to_corres_pre_step+)?,
268  (rule ccorres_to_corres_pre_finalise),
269  (intro pred_andI TrueI; clarsimp)
270)
271
272text \<open>
273We can easily obtain a partial @{term corres_underlying} fact from a @{term ccorresG} fact.
274However, this is not strong enough to prove @{term ccorresG} goals of the form produced by
275@{thm corres_to_ccorres} above.
276\<close>
277
278lemma ccorres_to_corres_partial:
279  assumes rf_sr_def: "rf_sr \<equiv> {(s,s'). cstate_relation s (globals s')}"
280  assumes ac_def: "ac_f \<equiv> AC_call_L1 G globals ret_xf (L1_call_simpl check_term \<Gamma> f_'proc)"
281  assumes ccorres: "ccorresG rf_sr \<Gamma> R' ret_xf' P Q' [] dspec_f (Call f_'proc)"
282  assumes pre: "\<And>s'. G s' \<Longrightarrow> ccorres_to_corres_pre Q \<top> Q' s'"
283  assumes ret: "\<And>r s'. R r (ret_xf s') \<longleftrightarrow> R' r (ret_xf' s')"
284  shows "corres_underlying {(s, s'). cstate_relation s s'} True False R P Q dspec_f ac_f"
285  using ccorres ret pre unfolding ac_def ccorres_to_corres_pre_def
286  by (fastforce simp: unif_rrel_def corres_underlying_def ccorres_underlying_def rf_sr_def
287                intro: EHOther dest: in_AC_call_simpl)
288
289text \<open>
290If we are willing to prove termination of the C code, we can obtain a rule which can be used
291with or without the AutoCorres no_c_termination setting, and which is strong enough to prove
292goals obtained from @{thm corres_to_ccorres}.
293\<close>
294
295lemma ccorres_to_corres_with_termination:
296  assumes rf_sr_def: "rf_sr \<equiv> {(s,s'). cstate_relation s (globals s')}"
297  assumes ac_def: "ac_f \<equiv> AC_call_L1 G globals ret_xf (L1_call_simpl check_term \<Gamma> f_'proc)"
298  assumes ccorres: "ccorresG rf_sr \<Gamma> R' ret_xf' P Q' [] dspec_f (Call f_'proc)"
299  assumes pre: "\<And>s'. G s' \<Longrightarrow> ccorres_to_corres_pre Q \<top> Q' s'"
300  assumes ret: "\<And>r s'. R r (ret_xf s') \<longleftrightarrow> R' r (ret_xf' s')"
301  assumes terminates:
302    "\<And>s s'. \<lbrakk> cstate_relation s (globals s'); P s; \<not> snd (dspec_f s); G s' \<rbrakk> \<Longrightarrow>
303             \<Gamma> \<turnstile> Call f_'proc \<down> Normal s'"
304  shows "corres_underlying {(s, s'). cstate_relation s s'} True True R P Q dspec_f ac_f"
305  using ccorres ret pre unfolding ac_def ccorres_to_corres_pre_def
306  apply (clarsimp simp: corres_underlying_def ccorres_underlying_def rf_sr_def)
307  apply (rule conjI)
308   apply (fastforce simp: unif_rrel_def intro: EHOther dest: in_AC_call_simpl)
309  apply (clarsimp simp: AC_call_L1_def L2_call_L1_def L1_call_simpl_def)
310  apply (cases check_term;
311         clarsimp simp: select_f_def select_def snd_bind snd_assert get_def
312                 split: sum.splits prod.splits)
313    apply (erule impE, blast intro: terminates)
314    apply (erule disjE)
315     apply (monad_eq split: xstate.splits sum.splits)
316      apply (drule EHOther, fastforce)
317      apply blast
318     apply (drule EHOther, fastforce)
319     apply blast
320    apply (monad_eq split: xstate.splits)
321    apply (fastforce dest: EHAbrupt[OF _ EHEmpty])
322   apply (monad_eq split: xstate.splits sum.splits)
323    apply (drule EHOther, fastforce)
324    apply blast
325   apply (drule EHOther, fastforce)
326   apply blast
327  apply (monad_eq split: xstate.splits)
328  apply (fastforce dest: EHAbrupt[OF _ EHEmpty])
329  done
330
331text \<open>
332When using AutoCorres with the no_c_termination setting, we need not prove termination
333of the C code.
334\<close>
335
336lemma ccorres_to_corres_no_termination:
337  assumes rf_sr_def: "rf_sr \<equiv> {(s,s'). cstate_relation s (globals s')}"
338  assumes ac_def: "ac_f \<equiv> AC_call_L1 G globals ret_xf (L1_call_simpl False \<Gamma> f_'proc)"
339  assumes ccorres: "ccorresG rf_sr \<Gamma> R' ret_xf' P Q' [] dspec_f (Call f_'proc)"
340  assumes pre: "\<And>s'. G s' \<Longrightarrow> ccorres_to_corres_pre Q \<top> Q' s'"
341  assumes ret: "\<And>r s'. R r (ret_xf s') \<longleftrightarrow> R' r (ret_xf' s')"
342  shows "corres_underlying {(s, s'). cstate_relation s s'} True True R P Q dspec_f ac_f"
343  using ccorres ret pre unfolding ac_def ccorres_to_corres_pre_def
344  apply (clarsimp simp: ac_def corres_underlying_def ccorres_underlying_def rf_sr_def)
345  apply (rule conjI)
346   apply (fastforce simp: unif_rrel_def intro: EHOther dest: in_AC_call_simpl)
347  apply (clarsimp simp: AC_call_L1_def L2_call_L1_def L1_call_simpl_def)
348  apply (clarsimp simp: select_f_def select_def snd_bind snd_assert get_def
349                 split: sum.splits prod.splits)
350   apply (monad_eq split: xstate.splits sum.splits)
351    apply (drule EHOther, fastforce)
352    apply blast
353   apply (drule EHOther, fastforce)
354   apply blast
355  apply (monad_eq split: xstate.splits)
356  apply (fastforce dest: EHAbrupt[OF _ EHEmpty])
357  done
358
359section \<open>Proof automation\<close>
360
361text \<open>
362We now provide ML functions for constructing simple proof automation tools.
363
364The first implements a method which converts a @{term ccorresG} goal into a
365@{term corres_underlying} goal, using @{thm corres_to_ccorres}, and automatically
366solving some subgoals. In some cases, it will also guess an appropriate return-value
367relation.
368
369The second is an attribute which converts a @{term ccorresG} fact into a
370@{term corres_underlying} fact.
371
372The setup functions are parameterised over a state relation. We instantiate them
373for the C kernel below.
374\<close>
375
376ML \<open>
377signature AUTOCORRES_CREFINE = sig
378  val setup_ac_init : thm -> (Proof.context -> Proof.method) context_parser
379  val setup_ac_attr : thm -> attribute context_parser
380end
381
382structure AutoCorresCRefine : AUTOCORRES_CREFINE = struct
383
384  fun proc_base_name termerr qualified_'proc_name =
385    unsuffix "_'proc" (List.last (Long_Name.explode qualified_'proc_name))
386      handle Empty => raise termerr "empty proc name"
387      handle Fail _ => raise termerr "not a _'proc"
388
389  fun get_call_'proc_name termerr c = case c of
390      Const (@{const_name Call}, _) $ Const (qualified_'proc_name, _) => qualified_'proc_name
391    | _ => raise termerr "not a Call"
392
393  fun match_ccorres_term termerr ccorres_term = case ccorres_term of
394      @{term Trueprop} $
395        (Const (@{const_name ccorres_underlying}, _)
396          $ _ $ c_Gamma $ c_rel $ c_xf $ a_rel $ a_xf $ _ $ _ $ c_hs $ _ $ c_c) =>
397      let
398        val _ = if c_rel = a_rel orelse c_xf = a_xf then ()
399                  else raise termerr "not a ccorres goal"
400      in
401        { c_Gamma=c_Gamma, c_rel=c_rel, c_xf=c_xf, c_hs=c_hs, c_c=c_c }
402      end
403    | _ => raise termerr "not a ccorres goal"
404
405  fun match_ac_corres_term ac_corres_fact_name ac_corres_term = case ac_corres_term of
406      @{term Trueprop} $ (Const (@{const_name ac_corres}, _)
407        $ _ $ _ $ ac_Gamma $ ac_xf $ _ $ (Const (@{const_name liftE}, _) $ _) $ ac_c)
408        => { ac_Gamma=ac_Gamma, ac_xf=ac_xf, ac_c=ac_c }
409    | _ => error ("ac_init_tac: " ^ ac_corres_fact_name ^ " not an ac_corres fact")
410
411  fun match_ac_wrap_term ac_wrap_name ac_wrap_term = case ac_wrap_term of
412      Const (@{const_name Pure.eq}, _) $ _
413        $ (Const (@{const_name AC_call_L1}, _) $ _ $ Const (@{const_name globals}, _) $ ac_xf
414        $ (Const (@{const_name L1_call_simpl}, _) $ check_term $ ac_Gamma
415        $ (Const (ac_proc_name, _))))
416        => { ac_Gamma=ac_Gamma, ac_xf=ac_xf, check_term=check_term, ac_proc_name=ac_proc_name }
417    | _ => error ("ac_attr: " ^ ac_wrap_name ^ " wasn't in the expected form")
418
419  fun auto_rv_relation ctxt mk_imp ac_xf c_rel c_xf =
420    let
421      (* Find the types of return-value relations and extraction functions. *)
422      val ccorres_xf_ty = fastype_of c_xf
423      val c_state_ty = case ccorres_xf_ty of
424          Type("fun", [st_ty, _]) => st_ty
425        | _ => raise TYPE ("ac_init_tac'", [ccorres_xf_ty], [c_xf])
426      val ac_corres_xf_ty = fastype_of ac_xf
427      val ac_corres_ret_ty = case ac_corres_xf_ty of
428          Type("fun", [_, acr_ty]) => acr_ty
429        | _ => raise TYPE ("ac_init_tac'", [ac_corres_xf_ty], [ac_xf])
430      val ccorres_rrel_ty = fastype_of c_rel
431      val abstract_ret_ty = case ccorres_rrel_ty of
432          Type("fun", [ar_ty, Type("fun", [_, @{typ bool}])]) => ar_ty
433        | _ => raise TYPE("ac_init_tac'", [ccorres_rrel_ty], [c_rel])
434      val ac_corres_rrel_ty = abstract_ret_ty --> ac_corres_ret_ty --> @{typ bool}
435
436      (* A function for building implications between return-value relations,
437         of the form used in corres_to_ccorres. *)
438      fun mk_rv_prop rv_rel =
439        let
440          val r_var = Free ("r", abstract_ret_ty)
441          val state_var = Free ("s'", c_state_ty)
442          fun mk_rel r xf = r $ r_var $ (xf $ state_var)
443          val assm = mk_rel rv_rel ac_xf
444          val conc = mk_rel c_rel c_xf
445          val prop = HOLogic.mk_Trueprop (mk_imp (assm, conc))
446        in
447          Logic.all r_var (Logic.all state_var prop)
448        end
449
450      (* Try two strategies for guessing a simple return-value relation,
451         and proving a corresponding implication:
452         - If dc works, use that.
453         - If the types allow us to reuse the relation we were given, try that. *)
454      fun first _ [] = NONE
455        | first f (x::xs) = (if f x then SOME x else first f xs)
456      fun prove_rv rv_rel =
457          (Goal.prove ctxt [] [] (mk_rv_prop rv_rel) (fn _ => full_simp_tac ctxt 1); true)
458                handle ERROR _ => false
459    in
460      first prove_rv [Const (@{const_name dc}, ac_corres_rrel_ty), c_rel]
461        |> Option.map (Thm.cterm_of ctxt)
462    end
463
464  fun ac_init_tac corres_to_ccorres corres_to_ccorres_rv_spec ctxt (insts, fixes) ccorres_goal_t =
465    let
466      fun termerr msg = TERM ("ac_init_tac: " ^ msg, [ccorres_goal_t])
467
468      (* Find the arguments to ccorres in the goal. *)
469      val { c_Gamma, c_rel, c_xf, c_hs, c_c } = match_ccorres_term termerr ccorres_goal_t
470      val proc_name = proc_base_name termerr (get_call_'proc_name termerr c_c)
471
472      (* Check that the handler stack is empty. *)
473      val _ = case c_hs of Const (@{const_name Nil}, _) => ()
474                | _ => raise termerr "non-empty handler stack"
475
476      (* Find the AutoCorres-generated fact for that procedure. *)
477      val ac_corres_fact_name = proc_name ^ "'_ac_corres"
478      val ac_corres_fact = Proof_Context.get_thm ctxt ac_corres_fact_name
479            handle ERROR msg => error ("ac_init_tac: " ^ msg)
480
481      (* Find the arguments to ac_corres in the AutoCorres-generated fact. *)
482      val { ac_Gamma, ac_xf, ac_c } =
483          match_ac_corres_term ac_corres_fact_name (Thm.prop_of ac_corres_fact)
484
485      (* Check that AutoCorres-generated fact is as expected. *)
486      val _ = if ac_c = c_c andalso c_Gamma = ac_Gamma then ()
487              else error ("ac_init_tac: " ^ ac_corres_fact_name ^ " unexpected fact")
488
489      fun corres_to_ccorres_inst rv_rel =
490        Drule.infer_instantiate ctxt [(("R",0), rv_rel)] corres_to_ccorres
491
492      val auto_rv_relation_tac =
493        case auto_rv_relation ctxt HOLogic.mk_imp ac_xf c_rel c_xf of
494            SOME rv_rel =>
495              resolve_tac ctxt [corres_to_ccorres_inst rv_rel] 1 THEN
496              resolve_tac ctxt [ac_corres_fact] 1 THEN
497              SOLVED' (full_simp_tac ctxt) 4 THEN
498              TRY (SOLVED' (full_simp_tac ctxt) 3)
499          | NONE =>
500              resolve_tac ctxt [corres_to_ccorres_rv_spec] 1 THEN
501              resolve_tac ctxt [ac_corres_fact] 1 THEN
502              TRY (SOLVED' (full_simp_tac ctxt) 3)
503
504      fun spec_rv_relation_tac thm =
505        let
506          val init_thm = (ac_corres_fact RS corres_to_ccorres) RS thm
507          val inst_thm = Rule_Insts.where_rule ctxt insts fixes init_thm
508          val tac =
509            TRY (SOLVED' (full_simp_tac ctxt) 4) THEN
510            TRY (SOLVED' (full_simp_tac ctxt) 3)
511        in
512          tac inst_thm
513        end
514    in
515      if null insts andalso null fixes
516        then auto_rv_relation_tac
517        else spec_rv_relation_tac
518    end
519
520  fun ac_attr conv_with_term conv_no_term gen_ctxt insts fixes ccorres_thm =
521    let
522      val ctxt = Context.proof_of gen_ctxt
523      val ccorres_t = Thm.prop_of ccorres_thm
524
525      fun termerr msg = TERM ("ac_attr: " ^ msg, [ccorres_t])
526
527      (* Find the arguments to ccorres in the given fact. *)
528      val { c_Gamma, c_rel, c_xf, c_c, ... } = match_ccorres_term termerr ccorres_t
529
530      val qualified_'proc_name = get_call_'proc_name termerr c_c
531      val proc_name = proc_base_name termerr qualified_'proc_name
532
533      (* Find the AutoCorres-generated wrapper, and extract relevant arguments. *)
534      val ac_wrap_name = proc_name ^ "'_def"
535      val ac_wrap_def = Proof_Context.get_thm ctxt ac_wrap_name
536            handle ERROR msg => error ("ac_attr: " ^ msg)
537
538      val { ac_Gamma, ac_xf, check_term, ac_proc_name } =
539          match_ac_wrap_term ac_wrap_name (Thm.prop_of ac_wrap_def)
540
541      (* Check that AutoCorres-generated wrapper is as expected. *)
542      val _ = if ac_proc_name = qualified_'proc_name andalso ac_Gamma = c_Gamma then ()
543              else error ("ac_attr: " ^ ac_wrap_name ^ " wasn't in the expected form")
544
545      val ccorres_to_corres = case check_term of
546          @{term False} => conv_no_term | _ => conv_with_term
547
548      fun ccorres_to_corres_inst rv_rel =
549        Drule.infer_instantiate ctxt [(("R",0), rv_rel)] ccorres_to_corres
550
551      val (ccorres_to_corres', rv_tac) =
552        if null insts andalso null fixes then
553          case auto_rv_relation ctxt HOLogic.mk_eq ac_xf c_rel c_xf of
554              SOME rv_rel => (ccorres_to_corres_inst rv_rel, SOLVED' (full_simp_tac ctxt) 2)
555            | NONE => (ccorres_to_corres, all_tac)
556          else (Rule_Insts.where_rule ctxt insts fixes ccorres_to_corres, all_tac)
557
558      val ac_corres_init_thm = ccorres_thm RS (ac_wrap_def RS ccorres_to_corres')
559
560      val ccorres_to_corres_pre_process_tac = Method.NO_CONTEXT_TACTIC ctxt
561          (Method_Closure.apply_method ctxt @{method ccorres_to_corres_pre_process}
562                                       [] [] [] ctxt [])
563
564      val tac = rv_tac THEN ccorres_to_corres_pre_process_tac
565    in
566      Seq.hd (tac ac_corres_init_thm) |> asm_full_simplify ctxt
567    end
568
569  val where_for_parser =
570    Scan.lift
571      (Scan.optional
572        (Args.$$$ "where" |--
573          Parse.and_list
574            (Parse.position Args.var -- (Args.$$$ "=" |-- Parse.!!! Args.embedded_inner_syntax))
575          -- Parse.for_fixes)
576        ([],[]))
577
578  fun setup_ac_init rf_sr_def =
579    let
580      val corres_to_ccorres = rf_sr_def RS @{thm corres_to_ccorres}
581      val corres_to_ccorres_rv_spec = rf_sr_def RS @{thm corres_to_ccorres_rv_spec}
582      val tac = ac_init_tac corres_to_ccorres corres_to_ccorres_rv_spec
583    in
584      where_for_parser >>
585        (fn args => fn ctxt => fn facts =>
586          SIMPLE_METHOD (SUBGOAL (tac ctxt args o #1) 1) facts)
587    end
588
589  fun setup_ac_attr rf_sr_def =
590    let
591      val conv_with_term = rf_sr_def RS @{thm ccorres_to_corres_with_termination}
592      val conv_no_term = rf_sr_def RS @{thm ccorres_to_corres_no_termination}
593    in
594      where_for_parser >>
595        (fn (insts, fixes) => fn (ctxt, ccorres_thm) =>
596          (NONE, SOME (ac_attr conv_with_term conv_no_term ctxt insts fixes ccorres_thm)))
597    end
598end
599\<close>
600
601section \<open>Kernel instantiation\<close>
602
603text \<open>Here, we instantiate the proof automation for the C kernel.\<close>
604
605context kernel begin
606
607method_setup ac_init = \<open>AutoCorresCRefine.setup_ac_init @{thm rf_sr_def}\<close>
608attribute_setup ac = \<open>AutoCorresCRefine.setup_ac_attr @{thm rf_sr_def}\<close>
609
610text \<open>
611FIXME: It would be nice to have an abbreviation for the @{term corres_underlying} relation
612that comes out of @{method ac_init}. Unfortunately, this causes renumbering of metavariables
613produced in resolution, breaking many proofs, so we avoid this for now.
614\<close>
615(* abbreviation "corres_ac \<equiv> corres_underlying {(s, s'). cstate_relation s s'} True True" *)
616
617end
618
619section \<open>Experiments with transferring bitfield proofs\<close>
620
621text \<open>Generic transfer rules\<close>
622lemma autocorres_transfer_spec:
623  assumes ac_def:
624    "ac_f \<equiv> AC_call_L1 arg_rel globals ret_xf (L1_call_simpl check_termination \<Gamma> f_'proc)"
625  assumes c_spec:
626    "\<forall>s0. \<Gamma>\<turnstile> (Collect (\<lambda>s. s0 = s \<and> P s)) Call f_'proc (Collect (Q s0))"
627  assumes precond_deps:
628    "\<And>s t. \<lbrakk> arg_rel s; arg_rel t; globals s = globals t \<rbrakk> \<Longrightarrow> P s = P t"
629  assumes postcond_deps:
630    "\<And>s0 s0' s t. \<lbrakk> arg_rel s0; arg_rel s0'; globals s0 = globals s0';
631                    ret_xf s = ret_xf t; globals s = globals t \<rbrakk> \<Longrightarrow> Q s0 s = Q s0' t"
632  shows "\<lbrace>\<lambda>s. P cs \<and> s = globals cs \<and> arg_rel cs \<rbrace>
633           ac_f
634         \<lbrace>\<lambda>r s'. \<exists>cs'. s' = globals cs' \<and> r = ret_xf cs' \<and> Q cs cs' \<rbrace>"
635  apply (clarsimp simp: valid_def ac_def AC_call_L1_def L2_call_L1_def L1_call_simpl_def
636                        in_monad' in_liftM select_f_def in_select in_fail
637                  split: sum.splits xstate.splits)
638  apply (rename_tac r', case_tac r'; clarsimp)
639  apply (rename_tac xst, case_tac xst; clarsimp)
640  apply (drule_tac ?s0.1=s in exec_normal[OF _ _ c_spec[rule_format], rotated])
641   apply (blast dest: precond_deps)
642  apply (blast dest: postcond_deps)
643  done
644
645text \<open>This one is probably more useful\<close>
646lemma autocorres_transfer_spec_no_modifies:
647  assumes ac_def:
648    "ac_f \<equiv> AC_call_L1 arg_rel globals ret_xf (L1_call_simpl check_termination \<Gamma> f_'proc)"
649  assumes c_spec:
650    "\<forall>s0. hoarep \<Gamma> {} {} (P' s0) (Call f_'proc) (Collect (Q s0)) A" \<comment> \<open>syntax parser barfs...\<close>
651  assumes c_modifies:
652    "\<forall>\<sigma>. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {\<sigma>} Call f_'proc {t. t may_not_modify_globals \<sigma>}"
653  assumes c_spec_unify:
654    "\<And>s0. P' s0 = {s. s0 = s \<and> P s}"
655  assumes precond_deps:
656    "\<And>s0 s t. \<lbrakk> arg_rel s; arg_rel t; globals s = globals t \<rbrakk> \<Longrightarrow> P s = P t"
657  assumes postcond_deps:
658    "\<And>s0 s0' s t. \<lbrakk> arg_rel s0; arg_rel s0'; globals s0 = globals s0';
659                    ret_xf s = ret_xf t; globals s = globals t \<rbrakk> \<Longrightarrow> Q s0 s = Q s0' t"
660  shows "\<lbrace>\<lambda>s. s = globals cs \<and> P cs \<and> arg_rel cs \<rbrace>
661           ac_f
662         \<lbrace>\<lambda>r s'. s' = globals cs \<and> (\<exists>cs'. r = ret_xf cs' \<and> Q cs cs') \<rbrace>"
663  apply (clarsimp simp: valid_def ac_def AC_call_L1_def L2_call_L1_def L1_call_simpl_def
664                        in_monad' in_liftM select_f_def in_select in_fail
665                  split: sum.splits xstate.splits)
666  apply (rename_tac r', case_tac r'; clarsimp)
667  apply (rename_tac xst, case_tac xst; clarsimp)
668  apply (frule_tac ?s0.1=s in exec_normal[OF _ _ c_spec[rule_format], rotated])
669   apply (clarsimp simp: c_spec_unify)
670   apply (blast dest: precond_deps)
671  apply (frule exec_normal[OF singletonI _ c_modifies[rule_format]])
672  apply (clarsimp simp: meq_def)
673  apply (blast dest: postcond_deps)
674  done
675
676subsection \<open>Helpers\<close>
677
678lemma All_to_all':
679  "(\<forall>x. P x) \<Longrightarrow> (\<And>x. P x)"
680  by simp
681
682text \<open>
683  Convert references to global or local state variables, to the opposite one.
684  FIXME: surely this has been proven already.
685\<close>
686lemma collect_lift:
687  "Collect (\<lambda>s. s0 = s \<and> f s) = Collect (\<lambda>s. s0 = s \<and> f s0)"
688  by blast
689lemma collect_unlift:
690  "Collect (\<lambda>s. s0 = s \<and> f s0 s) = Collect (\<lambda>s. s0 = s \<and> f s s)"
691  by blast
692
693
694subsection \<open>Experiment with wrapping specs\<close>
695lemma exec_no_fault:
696  assumes asms: "s \<in> P"
697  and     ce: "Gamma \<turnstile> \<langle>c, Normal s\<rangle> \<Rightarrow> Fault f"
698  and  valid: "Gamma \<turnstile> P c Q, A"
699  shows   "False"
700  using valid ce asms
701  apply -
702  apply (frule hoare_sound)
703  apply (clarsimp simp: NonDetMonad.bind_def cvalid_def split_def HoarePartialDef.valid_def)
704  apply (drule spec, drule spec, drule (1) mp)
705  apply auto
706  done
707
708lemma exec_no_stuck:
709  assumes asms: "s \<in> P"
710  and     ce: "Gamma \<turnstile> \<langle>c, Normal s\<rangle> \<Rightarrow> Stuck"
711  and  valid: "Gamma \<turnstile> P c Q, A"
712  shows   "False"
713  using valid ce asms
714  apply -
715  apply (frule hoare_sound)
716  apply (clarsimp simp: NonDetMonad.bind_def cvalid_def split_def HoarePartialDef.valid_def)
717  apply (drule spec, drule spec, drule (1) mp)
718  apply auto
719  done
720
721definition L1_call_simpl_spec where
722  "L1_call_simpl_spec check_term Gamma proc precond postcond =
723     L1_spec (Collect (\<lambda>(s, t). precond s s \<and> postcond s t))"
724
725lemma L1corres_call_simpl_spec:
726  "\<lbrakk> \<forall>s0. Gamma\<turnstile> (Collect (precond s0)) (Call proc) (Collect (postcond s0));
727     \<And>s. ct \<Longrightarrow> Gamma\<turnstile>Call proc \<down> Normal s \<rbrakk> \<Longrightarrow>
728   L1corres ct Gamma (L1_call_simpl_spec ct Gamma proc precond postcond) (Call proc)"
729  apply (clarsimp simp: L1corres_def L1_call_simpl_spec_def L1_defs
730                        assert_def snd_select snd_liftE snd_spec
731                        in_monad' in_spec
732                  split: xstate.splits)
733  apply (case_tac t)
734     apply (blast dest: exec_normal[rotated])
735    apply (blast dest: exec_abrupt[rotated])
736   apply (blast intro: exec_no_fault[rotated])
737  apply (blast intro: exec_no_stuck[rotated])
738  done
739
740
741section \<open>Termination proofs\<close>
742text \<open>
743  Proving termination side conditions for @{thm ccorres_to_corres_with_termination}.
744
745  To begin with, we can automatically prove terminates for most
746  helper functions as they do not have recursion or loops.
747\<close>
748
749named_theorems terminates_trivial
750
751method_setup terminates_setup = \<open>
752  let
753    fun tac ctxt goal_t =
754        case Logic.strip_assums_concl goal_t of
755             @{term_pat "Trueprop (_ \<turnstile> Call ?f_'proc \<down> _)"} =>
756               let
757                 val f = dest_Const f_'proc |> fst |> Long_Name.base_name |> unsuffix "_'proc";
758                 val impl = Proof_Context.get_thm ctxt (f ^ "_impl");
759                 val body = Proof_Context.get_thm ctxt (f ^ "_body_def");
760               in
761                 EVERY [
762                   resolve_tac ctxt @{thms terminates.Call} 1,
763                   resolve_tac ctxt [impl] 1,
764                   simp_tac (ctxt addsimps (body :: @{thms return_C_def lvar_nondet_init_def})) 1
765                 ]
766               end
767  in
768    Scan.succeed (fn ctxt => Method.SIMPLE_METHOD (SUBGOAL (tac ctxt o #1) 1))
769  end
770\<close>
771
772method terminates_trivial declares terminates_trivial =
773  (terminates_setup; intro terminates_trivial)
774
775lemma [terminates_trivial]:
776  "\<lbrakk> \<And>s. \<Gamma> \<turnstile> c \<down> Normal s \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Guard F G c \<down> Normal s"
777  apply (blast intro: terminates.Guard terminates.GuardFault)
778  done
779lemma [terminates_trivial]:
780  "\<lbrakk> \<And>s. \<Gamma> \<turnstile> c1 \<down> Normal s; \<And>s. \<Gamma> \<turnstile> c2 \<down> Normal s \<rbrakk> \<Longrightarrow>
781   \<Gamma> \<turnstile> Cond C c1 c2 \<down> Normal s"
782  apply (blast intro: terminates.CondTrue terminates.CondFalse)
783  done
784lemma [terminates_trivial]:
785  "\<lbrakk> \<Gamma> \<turnstile> c1 \<down> Normal s; \<And>s. \<Gamma> \<turnstile> c2 \<down> Normal s \<rbrakk> \<Longrightarrow>
786   \<Gamma> \<turnstile> c1;;c2 \<down> Normal s"
787  apply (erule terminates.Seq)
788  apply clarsimp
789  apply (case_tac s'; auto)
790  done
791
792lemma [terminates_trivial]:
793  fixes \<Gamma> return init shows
794  "\<lbrakk> \<And>s. \<Gamma> \<turnstile> Call p \<down> Normal s; \<And>s t u. \<Gamma> \<turnstile> c s t \<down> Normal u \<rbrakk> \<Longrightarrow>
795   \<Gamma> \<turnstile> call init p return c \<down> Normal s"
796  apply (case_tac "\<Gamma> p")
797   apply (erule terminates_callUndefined)
798  apply (fastforce simp: terminates_Call_body intro: terminates_call)
799  done
800
801lemmas [terminates_trivial] =
802  terminates.Basic
803  terminates.Catch[rule_format]
804  terminates.Throw
805  terminates.Skip
806  terminates.Spec
807
808section \<open>Additional infrastructure\<close>
809
810(* FIXME: Needs reorganisation. Much of the following should be moved elsewhere. *)
811
812context kernel begin
813
814lemma wpc_helper_corres_final:
815  "corres_underlying sr nf nf' rv Q Q' f f'
816   \<Longrightarrow> wpc_helper (P, P') (Q, {s. Q' s}) (corres_underlying sr nf nf' rv P (\<lambda>s. s \<in> P') f f')"
817  apply (clarsimp simp: wpc_helper_def)
818  apply (erule corres_guard_imp)
819   apply auto
820  done
821
822wpc_setup "\<lambda>m. corres_underlying sr nf nf' rv P P' m f'" wpc_helper_corres_final
823wpc_setup "\<lambda>m. corres_underlying sr nf nf' rv P P' (m >>= f) f'" wpc_helper_corres_final
824
825lemma condition_const: "condition (\<lambda>_. P) L R = (if P then L else R)"
826  by (simp add: condition_def split: if_splits)
827
828definition
829  errglobals :: "globals \<Rightarrow> errtype"
830where
831  "errglobals s \<equiv> \<lparr> errfault = seL4_Fault_lift (current_fault_' s),
832                    errlookup_fault = lookup_fault_lift (current_lookup_fault_' s),
833                    errsyscall = current_syscall_error_' s \<rparr>"
834
835lemma errstate_errglobals:
836  "errstate s' = errglobals (globals s')"
837  by (auto simp: errstate_def errglobals_def)
838
839lemma errglobals_simps [simp]:
840  "errfault (errglobals s) = seL4_Fault_lift (current_fault_' s)"
841  "errlookup_fault (errglobals s) = lookup_fault_lift (current_lookup_fault_' s)"
842  "errsyscall (errglobals s) = current_syscall_error_' s"
843  by (auto simp: errglobals_def)
844
845definition
846  "lift_rv ef vf elf R E \<equiv>
847    \<lambda>r (r',e'). (case r of Inl e \<Rightarrow> ef r' \<noteq> scast EXCEPTION_NONE \<and> E e (ef r') (elf e')
848                         | Inr v \<Rightarrow> ef r' = scast EXCEPTION_NONE \<and> R v (vf r'))"
849
850(* FIXME: provide a way to use this rule (and derived versions below) in ac_init. *)
851lemma corres_to_ccorres_rv_spec_liftxf:
852  assumes ac: "ac_corres globals check_term \<Gamma> ret_xf G (liftE ac) c"
853  assumes cu:
854    "corres_underlying
855      {(s,s'). cstate_relation s s'} True True (lift_rv ef vf elf R' E)
856      P Q a (do r' \<leftarrow> ac; e' \<leftarrow> gets exf; return (r',e') od)"
857  assumes "\<And>s'. esf (errstate s') = elf (exf (globals s'))"
858  assumes "\<And>e f e'. E' e f e' = E e f (esf e')"
859  assumes "\<And>s s'. cstate_relation s (globals s') \<Longrightarrow> P' s \<and> s' \<in> Q' \<Longrightarrow> P s \<and> Q (globals s')"
860  assumes "\<And>s s'. cstate_relation s (globals s') \<Longrightarrow> P' s \<and> s' \<in> Q' \<Longrightarrow> G s'"
861  shows "ccorres (E' \<currency> R') (liftxf errstate ef vf ret_xf) P' Q' [] a c"
862  apply (rule corres_to_ccorres_extra_globals_rv_spec[OF _ _ corres_rel_imp, OF rf_sr_def ac cu])
863  apply (all \<open>clarsimp simp: assms(5-6) liftxf_def\<close>)
864  apply (clarsimp simp: lift_rv_def liftxf_def assms(3-4) split: sum.splits)
865  done
866
867lemmas corres_to_ccorres_rv_spec_errglobals =
868  corres_to_ccorres_rv_spec_liftxf
869    [where elf="\<lambda>e. e" and esf="\<lambda>e. e" and E=E' for E', OF _ _ errstate_errglobals]
870
871lemmas corres_to_ccorres_rv_spec_current_fault =
872  corres_to_ccorres_rv_spec_liftxf
873    [where elf=seL4_Fault_lift and esf=errfault, OF _ _ errfault_errstate]
874
875lemmas corres_to_ccorres_rv_spec_current_lookup_fault =
876  corres_to_ccorres_rv_spec_liftxf
877    [where elf=lookup_fault_lift and esf=errlookup_fault, OF _ _ errlookup_fault_errstate]
878
879lemmas corres_to_ccorres_rv_spec_current_syscall_error =
880  corres_to_ccorres_rv_spec_liftxf
881    [where elf="\<lambda>e. e" and esf=errsyscall, OF _ _ errsyscall_errstate]
882
883lemma lift_rv_returnOk:
884  assumes "ef r = scast EXCEPTION_NONE"
885  assumes "R rv (vf r)"
886  shows "corres_underlying
887           {(x, y). cstate_relation x y} True True (lift_rv ef vf elf R E) \<top> \<top>
888           (returnOk rv)
889           (do e' \<leftarrow> gets exf; return (r, e') od)"
890  apply (clarsimp simp: corres_underlying_def snd_bind snd_modify snd_gets in_monad)
891  apply (rule bexI[of _ "(Inr rv, s)" for s]; simp add: in_monad lift_rv_def assms)
892  done
893
894lemma lift_rv_throwError':
895  assumes "\<And>s s'. cstate_relation s s' \<longrightarrow> cstate_relation s (esu s')"
896  assumes "ef r \<noteq> scast EXCEPTION_NONE"
897  assumes "\<And>err'. E err (ef r) (elf (exf (esu err')))"
898  shows "corres_underlying
899           {(x, y). cstate_relation x y} True True (lift_rv ef vf elf R E) \<top> \<top>
900           (throwError err)
901           (do _ \<leftarrow> modify esu; e' \<leftarrow> gets exf; return (r, e') od)"
902  apply (clarsimp simp: corres_underlying_def snd_bind snd_modify snd_gets in_monad)
903  apply (rule bexI[of _ "(Inl err, s)" for s]; simp add: in_monad lift_rv_def assms)
904  done
905
906lemma cstate_relation_errglobals_updates:
907  "cstate_relation s s' \<longrightarrow> cstate_relation s (current_fault_'_update f s')"
908  "cstate_relation s s' \<longrightarrow> cstate_relation s (current_lookup_fault_'_update lf s')"
909  "cstate_relation s s' \<longrightarrow> cstate_relation s (current_syscall_error_'_update sce s')"
910  by (auto simp: cstate_relation_def carch_state_relation_def cmachine_state_relation_def)
911
912lemmas lift_rv_throwError =
913  cstate_relation_errglobals_updates[THEN lift_rv_throwError']
914
915lemma valid_spec_to_wp:
916  assumes "\<And>\<sigma>. \<lbrace> \<lambda>s. s = \<sigma> \<and> P s \<rbrace> f \<lbrace> \<lambda>r s. s = \<sigma> \<and> R r s \<rbrace>"
917  shows "\<lbrace> \<lambda>s. P s \<and> (\<forall>r. R r s \<longrightarrow> Q r s) \<rbrace> f \<lbrace> Q \<rbrace>"
918  using assms by (fastforce simp: valid_def)
919
920lemmas valid_spec_to_wp' = valid_spec_to_wp[where P=\<top>, simplified]
921
922lemma spec_result_Normal:
923  fixes \<Gamma>
924  assumes p_spec: "\<forall>s. \<Gamma>,{} \<turnstile> {s'. s = s' \<and> P s s'} p (Q s)"
925  shows "\<forall>s t. P s s \<longrightarrow> \<Gamma> \<turnstile> \<langle>p, Normal s\<rangle> \<Rightarrow> t \<longrightarrow> t \<in> range Normal"
926  by (rule all_forward[OF p_spec], drule hoare_sound)
927     (auto simp: cvalid_def HoarePartialDef.valid_def image_def)
928
929lemma terminates_spec_no_fail:
930  fixes \<Gamma>
931  assumes ac: "ac \<equiv> AC_call_L1 arg_rel globals ret_xf (L1_call_simpl check_termination \<Gamma> f_'proc)"
932  assumes p_spec: "\<forall>s. \<Gamma>,{} \<turnstile> {s'. s = s' \<and> P s s'} (Call f_'proc) (Q s)"
933  assumes terminates: "\<forall>s. P s s \<longrightarrow> \<Gamma> \<turnstile> Call f_'proc \<down> Normal s"
934  assumes nf_pre: "\<And>s. N (globals s) \<Longrightarrow> arg_rel s \<Longrightarrow> P s s"
935  shows "no_fail N ac"
936  proof -
937    have normal: "\<forall>s t. P s s \<longrightarrow> \<Gamma> \<turnstile> \<langle>Call f_'proc, Normal s\<rangle> \<Rightarrow> t \<longrightarrow> t \<in> range Normal"
938      using spec_result_Normal p_spec by simp
939    have L1_call_simpl_no_fail:
940      "no_fail (\<lambda>s. P s s) (L1_call_simpl check_termination \<Gamma> f_'proc)"
941      apply (wpsimp simp: L1_call_simpl_def wp: non_fail_select select_wp)
942      using terminates normal by auto
943    have select_f_L1_call_simpl_no_fail:
944      "\<And>s. no_fail (\<lambda>_. P s s) (select_f (L1_call_simpl check_termination \<Gamma> f_'proc s))"
945      using L1_call_simpl_no_fail[unfolded no_fail_def]
946      by wpsimp
947    have select_f_L1_call_simpl_rv:
948      "\<And>s. \<lbrace>\<lambda>_. P s s\<rbrace> select_f (L1_call_simpl check_termination \<Gamma> f_'proc s) \<lbrace>\<lambda>r s. fst r = Inr ()\<rbrace>"
949      apply (wp, clarsimp simp: L1_call_simpl_def in_monad in_select split: xstate.splits)
950      apply (match premises in "s \<noteq> Stuck" for s \<Rightarrow> \<open>cases s\<close>)
951      using normal by auto
952    show ?thesis
953      apply (clarsimp simp: ac AC_call_L1_def L2_call_L1_def)
954      apply (wpsimp wp: select_f_L1_call_simpl_no_fail non_fail_select
955                wp_del: select_f_wp)
956      apply (rule hoare_strengthen_post[OF select_f_L1_call_simpl_rv], fastforce)
957      apply (wpsimp wp: select_wp nf_pre)+
958      done
959  qed
960
961lemmas terminates_spec_no_fail' =
962  terminates_spec_no_fail[where P="\<top>\<top>", simplified]
963
964lemma valid_spec_to_corres_symb_exec_r:
965  assumes spec': "\<And>\<sigma>. \<lbrace> \<lambda>s. s = \<sigma> \<and> P' s \<rbrace> f \<lbrace> \<lambda>r s. s = \<sigma> \<and> Q' r s \<rbrace>"
966  assumes nf: "nf' \<Longrightarrow> no_fail N' f"
967  assumes corres_rv: "\<And>rv'. corres_underlying sr nf nf' r P (R' rv') a (c rv')"
968  shows "corres_underlying sr nf nf' r P (\<lambda>s. N' s \<and> P' s \<and> (\<forall>r. Q' r s \<longrightarrow> R' r s)) a (f >>= c)"
969  by (rule corres_symb_exec_r[OF corres_rv])
970     (wpsimp wp: valid_spec_to_wp[OF spec'] nf)+
971
972lemma valid_spec_to_corres_gen_symb_exec_r:
973  assumes spec': "\<And>\<sigma>. \<lbrace> \<lambda>s. s = \<sigma> \<and> P' s \<rbrace> f \<lbrace> \<lambda>r s. s = \<sigma> \<and> Q' r \<rbrace>"
974  assumes nf: "nf' \<Longrightarrow> no_fail N' f"
975  assumes corres_rv: "\<And>rv'. Q' rv' \<Longrightarrow> corres_underlying sr nf nf' r P (R' rv') a (c rv')"
976  shows "corres_underlying sr nf nf' r P (\<lambda>s. N' s \<and> P' s \<and> (\<forall>r. Q' r \<longrightarrow> R' r s)) a (f >>= c)"
977  by (rule corres_symb_exec_r, rule_tac F="Q' rv" in corres_gen_asm2, erule corres_rv)
978     (wpsimp wp: valid_spec_to_wp[OF spec'] nf)+
979
980lemmas valid_spec_to_corres_symb_exec_r' =
981  valid_spec_to_corres_symb_exec_r[where P'=\<top>, simplified]
982
983lemmas valid_spec_to_corres_gen_symb_exec_r' =
984  valid_spec_to_corres_gen_symb_exec_r[where P'=\<top>, simplified]
985
986abbreviation
987  "gslift (s :: globals) \<equiv> clift (t_hrs_' s)"
988
989abbreviation
990  "c_h_t_g_valid" :: "globals \<Rightarrow> 'a::c_type ptr \<Rightarrow> bool"  ("_ \<Turnstile>\<^sub>g _" [99,99] 100)
991where
992  "s \<Turnstile>\<^sub>g p == hrs_htd (t_hrs_' s),c_guard \<Turnstile>\<^sub>t p"
993
994(* Mirrors ccorres_symb_exec_l, to get access to what's known about the abstract return value
995   in the concrete precondition. Not sure if this is necessary, or even a good idea. *)
996lemma corres_symb_exec_l'':
997  assumes corres: "\<And>rv. corres_underlying sr nf nf' r (R rv) (R' rv) (x rv) y"
998  assumes no_upd: "\<And>s. P s \<Longrightarrow> \<lbrace>(=) s\<rbrace> m \<lbrace>\<lambda>r. (=) s\<rbrace>"
999  assumes result: "\<lbrace>Q\<rbrace> m \<lbrace>R\<rbrace>"
1000  assumes nofail: "\<not> nf \<longrightarrow> no_fail P m"
1001  assumes mtfail: "empty_fail m"
1002  shows "corres_underlying sr nf nf' r
1003                           (P and Q) (\<lambda>s'. \<forall>rv s. (s,s') \<in> sr \<and> R rv s \<longrightarrow> R' rv s')
1004                           (m >>= (\<lambda>rv. x rv)) y"
1005  using corres unfolding corres_underlying_def
1006  apply (clarsimp; rename_tac s s')
1007  apply (subgoal_tac "\<not> snd (m s)")
1008   prefer 2
1009   using nofail
1010   apply (cases nf; clarsimp simp: no_fail_def elim!: not_snd_bindI1)
1011  apply (erule empty_fail_not_snd [OF _ mtfail, THEN exE]; clarsimp; rename_tac rv t)
1012  apply (subgoal_tac "t = s")
1013   prefer 2
1014   apply (frule use_valid, rule no_upd, simp+)
1015  apply clarsimp
1016  apply (drule_tac x=rv in spec, drule_tac x=rv in meta_spec, drule (1) bspec, simp)
1017  apply (frule use_valid, rule result, assumption)
1018  apply (drule mp, rule_tac x=s in exI, simp_all)
1019  apply (subgoal_tac "nf \<longrightarrow> \<not> snd (x rv s)")
1020   prefer 2
1021   apply (cases nf; clarsimp simp: no_fail_def elim!: not_snd_bindI2)
1022  apply (clarsimp; rename_tac fv' t')
1023  apply (drule (1) bspec; clarsimp; rename_tac fv t)
1024  apply (rule_tac x="(fv,t)" in bexI; clarsimp simp: bind_def)
1025  apply (rule bexI[rotated], assumption, simp)
1026  done
1027
1028lemma corres_stateAssert_l:
1029  assumes "corres_underlying sr nf nf' r P P' (a ()) c"
1030  shows "corres_underlying sr nf nf' r
1031                           (\<lambda>s. (\<not> nf \<longrightarrow> Q s) \<and> (Q s \<longrightarrow> P s)) P'
1032                           (stateAssert Q bs >>= a) c"
1033  apply (rule corres_guard_imp[OF corres_symb_exec_l''[where P="\<lambda>s. nf \<or> Q s"]])
1034        using assms apply simp
1035       apply (wpsimp simp: stateAssert_def)+
1036  done
1037
1038lemma corres_guard_r:
1039  assumes "corres_underlying sr nf nf' r P P' a (c ())"
1040  shows "corres_underlying sr nf nf' r P (\<lambda>s. (nf' \<longrightarrow> f s) \<and> (f s \<longrightarrow> P' s))
1041                           a (guard f >>= c)"
1042  apply (rule corres_guard_imp[OF corres_symb_exec_r'[where R'="\<lambda>s. nf' \<longrightarrow> f s"]])
1043       using assms apply simp
1044      apply wpsimp+
1045  done
1046
1047lemma corres_cross_over_guard:
1048  assumes "corres_underlying sr nf nf' r P P' a c"
1049  shows "corres_underlying sr nf nf' r (P and Q) (\<lambda>s'. \<forall>s. (s,s') \<in> sr \<and> Q s \<longrightarrow> P' s') a c"
1050  by (rule stronger_corres_guard_imp[OF assms]) auto
1051
1052end
1053
1054end
1055