1(*
2 * Copyright 2014, NICTA
3 *
4 * This software may be distributed and modified according to the terms of
5 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
6 * See "LICENSE_BSD2.txt" for details.
7 *
8 * @TAG(NICTA_BSD)
9 *)
10
11(*
12 * Theorems linking the L4.verified proofs to our own framework;
13 * typically showing that we prove equivalent results as a sanity
14 * check.
15 *)
16
17theory L4VerifiedLinks
18imports
19  "AutoCorres.AutoCorres"
20  "CLib.Corres_UL_C"
21begin
22
23(*
24 * The ccorresE framework implies the ccorres framework.
25 *)
26lemma ccorresE_ccorres_underlying:
27  "\<lbrakk> ccorresE st check_termination \<Gamma> G G' A B; \<not> exceptions_thrown B \<rbrakk> \<Longrightarrow>
28  ccorres_underlying {(s', s). s' = st s} \<Gamma> dc (\<lambda>_. ()) dc (\<lambda>_. ()) G G' [] A B"
29  apply (clarsimp simp: ccorres_underlying_def dc_def)
30  apply (clarsimp simp: ccorresE_def)
31  apply (erule allE, erule impE, force)
32  apply (erule exec_handlers.cases, simp_all)
33   apply clarsimp
34   apply (frule exceptions_thrown_not_abrupt, simp_all)[1]
35  apply (clarsimp split: xstate.splits)
36  apply (erule allE, erule conjE, erule impE, assumption)
37  apply (clarsimp simp: unif_rrel_def isAbr_def split: xstate.splits)
38  apply (case_tac ta, simp_all)
39  apply (rule bexI [rotated], assumption)
40  apply simp
41  done
42
43(*
44 * The ccorresE framework implies the ccorres framework.
45 *)
46lemma ccorresE_ccorres_underlying':
47  "\<lbrakk> ccorresE st check_termination \<Gamma> G G' A B; no_throw G A \<rbrakk> \<Longrightarrow>
48  ccorres_underlying {(s', s). s' = st s} \<Gamma> dc (\<lambda>_. ()) dc (\<lambda>_. ()) G G' [] A B"
49  apply (clarsimp simp: ccorres_underlying_def dc_def)
50  apply (clarsimp simp: ccorresE_def)
51  apply (erule allE, erule impE, force)
52  apply (erule exec_handlers.cases, simp_all)
53   apply clarsimp
54   apply (erule_tac allE, erule (1) impE)
55   apply clarsimp
56   apply (drule (1) no_throw_Inr)
57    apply fastforce
58   apply fastforce
59  apply (clarsimp split: xstate.splits)
60  apply (erule allE, erule conjE, erule impE, assumption)
61  apply (clarsimp simp: unif_rrel_def isAbr_def split: xstate.splits)
62  apply (case_tac ta, simp_all)
63  apply (rule bexI [rotated], assumption)
64  apply simp
65  done
66
67lemma ac_corres_ccorres_underlying:
68  "ac_corres st check_termination \<Gamma> rx G A B \<Longrightarrow>
69   ccorres_underlying {(a, b). a = st b} \<Gamma> ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = rx s)) Inr ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = rx s)) Inr (\<lambda>_. True) (Collect G) [] A B"
70  apply (clarsimp simp: ac_corres_def ccorres_underlying_def)
71  apply (erule allE, erule impE, force)
72  apply clarsimp
73  apply (erule exec_handlers.cases)
74    apply clarsimp
75    apply (erule allE, erule (1) impE)
76    apply clarsimp
77   apply (case_tac hs)
78    apply clarsimp
79    apply (erule allE, erule (1) impE)
80    apply (clarsimp split: xstate.splits)
81    apply (erule bexI [rotated])
82    apply (clarsimp simp: unif_rrel_def)
83   apply clarsimp
84  apply clarsimp
85  done
86
87(*
88 * The definition of corresXF and corres_underlying are equivalent,
89 * assuming we don't use the extraction functions.
90 *)
91lemma corres_impl_corresXF:
92  "corres_underlying {(a, b). a = st b} nf True (dc \<oplus> dc) \<top> P G G' \<Longrightarrow>
93   corresXF st (\<lambda>_ _. ()) (\<lambda>_ _. ()) P G G'"
94  apply (rule corresXF_I)
95    apply (clarsimp simp: corres_underlying_def corresXF_def)
96    apply (erule allE, erule (1) impE)
97    apply force
98   apply (clarsimp simp: corres_underlying_def corresXF_def)
99   apply (erule allE, erule (1) impE)
100   apply force
101  apply (clarsimp simp: corres_underlying_def corresXF_def)
102  done
103
104lemma corresXF_impl_corres:
105  "\<lbrakk> corresXF st (\<lambda>_ _. ()) (\<lambda>_ _. ()) P G G'; no_fail \<top> G \<rbrakk> \<Longrightarrow>
106   corres_underlying {(a, b). a = st b} nf True (dc \<oplus> dc) \<top> P G G'"
107  apply (clarsimp simp: corres_underlying_def corresXF_def no_fail_def)
108  apply (erule allE, erule (1) impE)
109  apply clarsimp
110  apply (erule (1) my_BallE)
111  apply (force split: sum.splits)
112  done
113
114end
115