-
Notifications
You must be signed in to change notification settings - Fork 0
/
Bits_AI.thy
114 lines (86 loc) · 3.72 KB
/
Bits_AI.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
(*
* 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 Bits_AI
imports Invariants_AI
begin
lemmas crunch_wps = hoare_drop_imps mapM_wp' mapM_x_wp'
lemmas crunch_simps = split_def whenE_def unlessE_def Let_def if_fun_split
assertE_def zipWithM_mapM zipWithM_x_mapM
lemma set_object_is_modify:
"set_object ptr obj = modify (\<lambda>s. s \<lparr> kheap := kheap s (ptr \<mapsto> obj) \<rparr>)"
unfolding set_object_def modify_def by simp
definition
intr :: "ExceptionTypes_A.interrupt \<Rightarrow> irq \<Rightarrow> bool" where
"intr x y \<equiv> (x = Interrupted y)"
lemma intr_simp[simp]:
"intr (Interrupted x) y = (x = y)"
by (simp add: intr_def)
lemma cap_fault_injection:
"cap_fault_on_failure addr b = injection_handler (ExceptionTypes_A.CapFault addr b)"
apply (rule ext)
apply (simp add: cap_fault_on_failure_def injection_handler_def o_def)
done
lemma lookup_error_injection:
"lookup_error_on_failure b = injection_handler (ExceptionTypes_A.FailedLookup b)"
apply (rule ext)
apply (simp add: lookup_error_on_failure_def injection_handler_def o_def)
done
lemmas cap_fault_wp[wp] = injection_wp[OF cap_fault_injection]
lemmas cap_fault_wp_E[wp] = injection_wp_E[OF cap_fault_injection]
lemmas cap_fault_bindE = injection_bindE[OF cap_fault_injection cap_fault_injection]
lemmas cap_fault_liftE[simp] = injection_liftE[OF cap_fault_injection]
lemmas lookup_error_wp[wp] = injection_wp[OF lookup_error_injection]
lemmas lookup_error_wp_E[wp] = injection_wp_E[OF lookup_error_injection]
lemmas lookup_error_bindE = injection_bindE[OF lookup_error_injection lookup_error_injection]
lemmas lookup_error_liftE[simp] = injection_liftE[OF lookup_error_injection]
lemma unify_failure_injection:
"unify_failure = injection_handler (\<lambda>x. ())"
by (intro ext, simp add: unify_failure_def injection_handler_def)
lemmas unify_failure_wp[wp] = injection_wp [OF unify_failure_injection]
lemmas unify_failure_wp_E[wp] = injection_wp_E [OF unify_failure_injection]
lemma ep_cases_weak_wp:
assumes "\<lbrace>P_A\<rbrace> a \<lbrace>Q\<rbrace>"
assumes "\<And>q. \<lbrace>P_B\<rbrace> b q \<lbrace>Q\<rbrace>"
assumes "\<And>q. \<lbrace>P_C\<rbrace> c q \<lbrace>Q\<rbrace>"
shows
"\<lbrace>P_A and P_B and P_C\<rbrace>
case ts of
Structures_A.IdleEP \<Rightarrow> a
| Structures_A.SendEP q \<Rightarrow> b q
| Structures_A.RecvEP q \<Rightarrow> c q \<lbrace>Q\<rbrace>"
apply (cases ts)
apply (simp, rule hoare_weaken_pre, rule assms, simp)+
done
lemma aep_cases_weak_wp:
assumes "\<lbrace>P_A\<rbrace> a \<lbrace>Q\<rbrace>"
assumes "\<And>q. \<lbrace>P_B\<rbrace> b q \<lbrace>Q\<rbrace>"
assumes "\<And>bdg msg. \<lbrace>P_C\<rbrace> c bdg msg \<lbrace>Q\<rbrace>"
shows
"\<lbrace>P_A and P_B and P_C\<rbrace>
case ts of
Structures_A.IdleAEP \<Rightarrow> a
| Structures_A.WaitingAEP q \<Rightarrow> b q
| Structures_A.ActiveAEP bdg msg \<Rightarrow> c bdg msg \<lbrace>Q\<rbrace>"
apply (cases ts)
apply (simp, rule hoare_weaken_pre, rule assms, simp)+
done
lemma NullCap_valid [simp]: "s \<turnstile> cap.NullCap"
by (simp add: valid_cap_def)
lemma empty_on_failure_wp[wp]:
"\<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>,\<lbrace>\<lambda>rv. Q []\<rbrace>
\<Longrightarrow> \<lbrace>P\<rbrace> empty_on_failure m \<lbrace>Q\<rbrace>"
apply (simp add: empty_on_failure_def)
apply wp
apply assumption
done
lemma pbfs_atleast_pageBits:
"pageBits \<le> pageBitsForSize sz"
by (cases sz) (auto simp: pageBits_def)
end