-
Notifications
You must be signed in to change notification settings - Fork 105
/
LevityCatch_AI.thy
78 lines (59 loc) · 2.44 KB
/
LevityCatch_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
(*
* Copyright 2022, Proofcraft Pty Ltd
* Copyright 2014, General Dynamics C4 Systems
*
* SPDX-License-Identifier: GPL-2.0-only
*)
theory LevityCatch_AI
imports
ArchLevityCatch_AI
begin
(* FIXME: eliminate mapM_UNIV_wp, use mapM_wp' directly *)
lemmas mapM_UNIV_wp = mapM_wp'
arch_requalify_consts
ptrFromPAddr addrFromPPtr
arch_requalify_facts
ptrFormPAddr_addFromPPtr
aobj_ref_arch_cap
arch_finalise_cap_bcorres
prepare_thread_delete_bcorres
lemmas aobj_ref_arch_cap_simps[simp] = aobj_ref_arch_cap
lemmas [wp] = arch_finalise_cap_bcorres prepare_thread_delete_bcorres
lemma detype_arch_state:
"arch_state (detype S s) = arch_state s"
by (simp add: detype_def)
lemma obj_ref_elemD:
"r \<in> obj_refs cap \<Longrightarrow> obj_refs cap = {r}"
by (cases cap; simp)
lemma get_cap_id:
"(v, s') \<in> fst (get_cap p s) \<Longrightarrow> (s' = s)"
by (clarsimp simp: get_cap_def get_object_def in_monad split_def
split: kernel_object.splits)
lemmas cap_irq_opt_simps[simp] =
cap_irq_opt_def [split_simps cap.split sum.split]
lemmas cap_irqs_simps[simp] =
cap_irqs_def [unfolded cap_irq_opt_def, split_simps cap.split sum.split, simplified option.simps]
declare liftE_wp[wp]
declare case_sum_True[simp]
crunch_ignore (add: do_extended_op)
lemma None_Some_strg:
"x = None \<Longrightarrow> x \<noteq> Some y"
by simp
(* Weakest precondition lemmas that need ASpec concepts: *)
lemma const_on_failure_wp:
"\<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>rv. Q n\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> const_on_failure n m \<lbrace>Q\<rbrace>"
by (wpsimp simp: const_on_failure_def)
(* Weaker wp rule for arguments "a" which do not take type det_ext state.
The stronger rule below will take precendence, because it is declared [wp]
later than this one. This rule here will fire when the stronger one does not
apply because of a looser type than det_ext state. The looser type tends to
happen in goals that are stated by crunch. *)
lemma select_ext_weak_wp[wp]:
"\<lbrace>\<lambda>s. \<forall>x\<in>S. Q x s\<rbrace> select_ext a S \<lbrace>Q\<rbrace>"
by (wpsimp simp: select_ext_def)
(* The "real" wp rule for select_ext, requires det_ext state: *)
lemma select_ext_wp[wp]:
"\<lbrace>\<lambda>s. a s \<in> S \<longrightarrow> Q (a s) s\<rbrace> select_ext a S \<lbrace>Q\<rbrace>"
unfolding select_ext_def unwrap_ext_det_ext_ext_def
by (wpsimp simp: select_switch_det_ext_ext_def)
end