adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

arch_split: skeleton arch files for AInvs

This commit is contained in:
Daniel Matichuk 2016-05-11 12:29:46 +10:00 committed by Alejandro Gomez-Londono
parent 3b54eb8f70
commit 9f62622532
24 changed files with 549 additions and 71 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

34
proof/invariant-abstract/ARM/ArchArch_AI.thy Normal file
View File

@ -0,0 +1,34 @@
(*
* 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 ArchArch_AI
imports "../Arch_AI"
begin
context Arch begin
named_theorems Arch_AI_asms
definition "Arch_AI_dummy_const \<equiv> (1 :: nat)"
lemma Arch_AI_trivial_result[Arch_AI_asms]:
"Arch_AI_dummy_const > 0"
by (simp add: Arch_AI_dummy_const_def)
end
interpretation Arch_AI?: Arch_AI
where Arch_AI_dummy_const = Arch.Arch_AI_dummy_const
proof goal_cases
interpret Arch .
case 1 show ?case by (intro_locales; (unfold_locales, fact Arch_AI_asms)?)
qed
end

34
proof/invariant-abstract/ARM/ArchCNodeInv_AI.thy Normal file
View File

@ -0,0 +1,34 @@
(*
* 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 ArchCNodeInv_AI
imports "../CNodeInv_AI"
begin
context Arch begin
named_theorems CNodeInv_AI_asms
definition "CNodeInv_AI_dummy_const \<equiv> (1 :: nat)"
lemma CNodeInv_AI_trivial_result[CNodeInv_AI_asms]:
"CNodeInv_AI_dummy_const > 0"
by (simp add: CNodeInv_AI_dummy_const_def)
end
interpretation CNodeInv_AI?: CNodeInv_AI
where CNodeInv_AI_dummy_const = Arch.CNodeInv_AI_dummy_const
proof goal_cases
interpret Arch .
case 1 show ?case by (intro_locales; (unfold_locales, fact CNodeInv_AI_asms)?)
qed
end

34
proof/invariant-abstract/ARM/ArchDetype_AI.thy Normal file
View File

@ -0,0 +1,34 @@
(*
* 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 ArchDetype_AI
imports "../Detype_AI"
begin
context Arch begin
named_theorems Detype_AI_asms
definition "Detype_AI_dummy_const \<equiv> (1 :: nat)"
lemma Detype_AI_trivial_result[Detype_AI_asms]:
"Detype_AI_dummy_const > 0"
by (simp add: Detype_AI_dummy_const_def)
end
interpretation Detype_AI?: Detype_AI
where Detype_AI_dummy_const = Arch.Detype_AI_dummy_const
proof goal_cases
interpret Arch .
case 1 show ?case by (intro_locales; (unfold_locales, fact Detype_AI_asms)?)
qed
end

34
proof/invariant-abstract/ARM/ArchFinalise_AI.thy Normal file
View File

@ -0,0 +1,34 @@
(*
* 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 ArchFinalise_AI
imports "../Finalise_AI"
begin
context Arch begin
named_theorems Finalise_AI_asms
definition "Finalise_AI_dummy_const \<equiv> (1 :: nat)"
lemma Finalise_AI_trivial_result[Finalise_AI_asms]:
"Finalise_AI_dummy_const > 0"
by (simp add: Finalise_AI_dummy_const_def)
end
interpretation Finalise_AI?: Finalise_AI
where Finalise_AI_dummy_const = Arch.Finalise_AI_dummy_const
proof goal_cases
interpret Arch .
case 1 show ?case by (intro_locales; (unfold_locales, fact Finalise_AI_asms)?)
qed
end

34
proof/invariant-abstract/ARM/ArchInterrupt_AI.thy Normal file
View File

@ -0,0 +1,34 @@
(*
* 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 ArchInterrupt_AI
imports "../Interrupt_AI"
begin
context Arch begin
named_theorems Interrupt_AI_asms
definition "Interrupt_AI_dummy_const \<equiv> (1 :: nat)"
lemma Interrupt_AI_trivial_result[Interrupt_AI_asms]:
"Interrupt_AI_dummy_const > 0"
by (simp add: Interrupt_AI_dummy_const_def)
end
interpretation Interrupt_AI?: Interrupt_AI
where Interrupt_AI_dummy_const = Arch.Interrupt_AI_dummy_const
proof goal_cases
interpret Arch .
case 1 show ?case by (intro_locales; (unfold_locales, fact Interrupt_AI_asms)?)
qed
end

33
proof/invariant-abstract/ARM/ArchIpcCancel_AI.thy Normal file
View File

@ -0,0 +1,33 @@
(*
* 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 ArchIpcCancel_AI
imports "../IpcCancel_AI"
begin
context Arch begin
named_theorems IpcCancel_AI_asms
definition "IpcCancel_AI_dummy_const \<equiv> (1 :: nat)"
lemma IpcCancel_AI_trivial_result[IpcCancel_AI_asms]:
"IpcCancel_AI_dummy_const > 0"
by (simp add: IpcCancel_AI_dummy_const_def)
end
interpretation IpcCancel_AI: IpcCancel_AI
where IpcCancel_AI_dummy_const = Arch.IpcCancel_AI_dummy_const proof goal_cases
interpret Arch .
case 1 show ?case by (intro_locales; (unfold_locales, fact IpcCancel_AI_asms)?)
qed
end

34
proof/invariant-abstract/ARM/ArchIpc_AI.thy Normal file
View File

@ -0,0 +1,34 @@
(*
* 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 ArchIpc_AI
imports "../Ipc_AI"
begin
context Arch begin
named_theorems Ipc_AI_asms
definition "Ipc_AI_dummy_const \<equiv> (1 :: nat)"
lemma Ipc_AI_trivial_result[Ipc_AI_asms]:
"Ipc_AI_dummy_const > 0"
by (simp add: Ipc_AI_dummy_const_def)
end
interpretation Ipc_AI?: Ipc_AI
where Ipc_AI_dummy_const = Arch.Ipc_AI_dummy_const
proof goal_cases
interpret Arch .
case 1 show ?case by (intro_locales; (unfold_locales, fact Ipc_AI_asms)?)
qed
end

78
proof/invariant-abstract/ARM/ArchRetype_AI.thy Normal file
View File

@ -0,0 +1,78 @@
(*
* 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)
*)
(*
Arch-specific retype invariants
*)
theory ArchRetype_AI
imports "../Retype_AI"
begin
context Arch begin
named_theorems Retype_AI_asms
lemma clearMemoryVM_return[simp, Retype_AI_asms]:
"clearMemoryVM a b = return ()"
by (simp add: clearMemoryVM_def)
end
interpretation Retype_AI?: Retype_AI
proof goal_cases
interpret Arch .
case 1 show ?case by (intro_locales; (unfold_locales, fact Retype_AI_asms)?)
qed
context Arch begin global_naming ARM
lemma retype_region_plain_invs:
"\<lbrace>invs and caps_no_overlap ptr sz and pspace_no_overlap ptr sz
and caps_overlap_reserved {ptr..ptr + of_nat n * 2 ^ obj_bits_api ty us - 1}
and region_in_kernel_window {ptr .. (ptr &&~~ mask sz) + 2 ^ sz - 1}
and K (ty = Structures_A.CapTableObject \<longrightarrow> 0 < us)
and K (range_cover ptr sz (obj_bits_api ty us) n)
and K (ty \<noteq> ArchObject PageDirectoryObj)\<rbrace>
retype_region ptr n us ty \<lbrace>\<lambda>rv. invs\<rbrace>"
apply (rule hoare_gen_asm)
apply (rule hoare_strengthen_post[OF retype_region_post_retype_invs])
apply (simp add: post_retype_invs_def)
done
lemma storeWord_um_eq_0:
"\<lbrace>\<lambda>m. underlying_memory m p = 0\<rbrace>
storeWord x 0
\<lbrace>\<lambda>_ m. underlying_memory m p = 0\<rbrace>"
by (simp add: storeWord_def word_rsplit_0 | wp)+
lemma clearMemory_um_eq_0:
"\<lbrace>\<lambda>m. underlying_memory m p = 0\<rbrace>
clearMemory ptr bits
\<lbrace>\<lambda>_ m. underlying_memory m p = 0\<rbrace>"
apply (clarsimp simp: clearMemory_def)
apply (wp mapM_x_wp_inv | simp)+
apply (rule hoare_pre)
apply (wp hoare_drop_imps storeWord_um_eq_0)
apply (fastforce simp: ignore_failure_def split: split_if_asm)
done
lemma cleanCacheRange_PoU_um_inv[wp]:
"\<lbrace>\<lambda>m. P (underlying_memory m)\<rbrace>
cleanCacheRange_PoU ptr w p
\<lbrace>\<lambda>_ m. P (underlying_memory m)\<rbrace>"
by (simp add: cleanCacheRange_PoU_def cleanByVA_PoU_def machine_op_lift_def machine_rest_lift_def
split_def | wp)+
end
end

34
proof/invariant-abstract/ARM/ArchSchedule_AI.thy Normal file
View File

@ -0,0 +1,34 @@
(*
* 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 ArchSchedule_AI
imports "../Schedule_AI"
begin
context Arch begin
named_theorems Schedule_AI_asms
definition "Schedule_AI_dummy_const \<equiv> (1 :: nat)"
lemma Schedule_AI_trivial_result[Schedule_AI_asms]:
"Schedule_AI_dummy_const > 0"
by (simp add: Schedule_AI_dummy_const_def)
end
interpretation Schedule_AI: Schedule_AI
where Schedule_AI_dummy_const = Arch.Schedule_AI_dummy_const
proof goal_cases
interpret Arch .
case 1 show ?case by (intro_locales; (unfold_locales, fact Schedule_AI_asms)?)
qed
end

34
proof/invariant-abstract/ARM/ArchTcb_AI.thy Normal file
View File

@ -0,0 +1,34 @@
(*
* 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 ArchTcb_AI
imports "../Tcb_AI"
begin
context Arch begin
named_theorems Tcb_AI_asms
definition "Tcb_AI_dummy_const \<equiv> (1 :: nat)"
lemma Tcb_AI_trivial_result[Tcb_AI_asms]:
"Tcb_AI_dummy_const > 0"
by (simp add: Tcb_AI_dummy_const_def)
end
interpretation Tcb_AI?: Tcb_AI
where Tcb_AI_dummy_const = Arch.Tcb_AI_dummy_const
proof goal_cases
interpret Arch .
case 1 show ?case by (intro_locales; (unfold_locales, fact Tcb_AI_asms)?)
qed
end

34
proof/invariant-abstract/ARM/ArchUntyped_AI.thy Normal file
View File

@ -0,0 +1,34 @@
(*
* 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 ArchUntyped_AI
imports "../Untyped_AI"
begin
context Arch begin
named_theorems Untyped_AI_asms
definition "Untyped_AI_dummy_const \<equiv> (1 :: nat)"
lemma Untyped_AI_trivial_result[Untyped_AI_asms]:
"Untyped_AI_dummy_const > 0"
by (simp add: Untyped_AI_dummy_const_def)
end
interpretation Untyped_AI?: Untyped_AI
where Untyped_AI_dummy_const = Arch.Untyped_AI_dummy_const
proof goal_cases
interpret Arch .
case 1 show ?case by (intro_locales; (unfold_locales, fact Untyped_AI_asms)?)
qed
end

10
proof/invariant-abstract/Arch_AI.thy
View File

@ -13,9 +13,17 @@ Top level architecture related proofs.
*)
theory Arch_AI
imports Untyped_AI Finalise_AI
imports "./$L4V_ARCH/ArchUntyped_AI" "./$L4V_ARCH/ArchFinalise_AI"
begin
locale Arch_AI begin
extend_locale
fixes Arch_AI_dummy_const :: nat
assumes Arch_AI_trivial_asm: "Arch_AI_dummy_const > 0"
end
context Arch begin global_naming ARM (*FIXME: arch_split*)
definition

2
proof/invariant-abstract/BCorres2_AI.thy
View File

@ -12,7 +12,7 @@ theory BCorres2_AI
imports
EmptyFail_AI
"../../lib/BCorres_UL"
CNodeInv_AI
"./$L4V_ARCH/ArchCNodeInv_AI"
begin
definition all_but_exst where

10
proof/invariant-abstract/CNodeInv_AI.thy
View File

@ -14,9 +14,17 @@ recursive revoke and delete operations.
*)
theory CNodeInv_AI
imports Ipc_AI
imports "./$L4V_ARCH/ArchIpc_AI"
begin
locale CNodeInv_AI begin
extend_locale
fixes CNodeInv_AI_dummy_const :: nat
assumes CNodeInv_AI_trivial_asm: "CNodeInv_AI_dummy_const > 0"
end
primrec
valid_cnode_inv :: "cnode_invocation \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
where

10
proof/invariant-abstract/Detype_AI.thy
View File

@ -9,9 +9,17 @@
*)
theory Detype_AI
imports Retype_AI
imports "./$L4V_ARCH/ArchRetype_AI"
begin
locale Detype_AI begin
extend_locale
fixes Detype_AI_dummy_const :: nat
assumes Detype_AI_trivial_asm: "Detype_AI_dummy_const > 0"
end
lemma obj_at_detype[simp]:
"obj_at P p (detype S s) = (p \<notin> S \<and> obj_at P p s)"
by (clarsimp simp: obj_at_def detype_def)

12
proof/invariant-abstract/Finalise_AI.thy
View File

@ -10,11 +10,19 @@
theory Finalise_AI
imports
IpcCancel_AI
"./$L4V_ARCH/ArchIpcCancel_AI"
InterruptAcc_AI
Retype_AI
"./$L4V_ARCH/ArchRetype_AI"
begin
locale Finalise_AI begin
extend_locale
fixes Finalise_AI_dummy_const :: nat
assumes Finalise_AI_trivial_asm: "Finalise_AI_dummy_const > 0"
end
context begin interpretation Arch .
requalify_consts

10
proof/invariant-abstract/Interrupt_AI.thy
View File

@ -13,9 +13,17 @@ Refinement for interrupt controller operations
*)
theory Interrupt_AI
imports Ipc_AI
imports "./$L4V_ARCH/ArchIpc_AI"
begin
locale Interrupt_AI begin
extend_locale
fixes Interrupt_AI_dummy_const :: nat
assumes Interrupt_AI_trivial_asm: "Interrupt_AI_dummy_const > 0"
end
context begin interpretation Arch .
requalify_consts
maxIRQ

10
proof/invariant-abstract/IpcCancel_AI.thy
View File

@ -9,9 +9,17 @@
*)
theory IpcCancel_AI
imports Schedule_AI
imports "./$L4V_ARCH/ArchSchedule_AI"
begin
locale IpcCancel_AI begin
extend_locale
fixes IpcCancel_AI_dummy_const :: nat
assumes IpcCancel_AI_trivial_asm: "IpcCancel_AI_dummy_const > 0"
end
lemma blocked_cancel_ipc_simple:
"\<lbrace>tcb_at t\<rbrace> blocked_cancel_ipc ts t \<lbrace>\<lambda>rv. st_tcb_at simple t\<rbrace>"
by (simp add: blocked_cancel_ipc_def | wp sts_st_tcb_at')+

10
proof/invariant-abstract/Ipc_AI.thy
View File

@ -9,9 +9,17 @@
*)
theory Ipc_AI
imports Finalise_AI
imports "./$L4V_ARCH/ArchFinalise_AI"
begin
locale Ipc_AI begin
extend_locale
fixes Ipc_AI_dummy_const :: nat
assumes Ipc_AI_trivial_asm: "Ipc_AI_dummy_const > 0"
end
declare if_cong[cong del]
lemmas lookup_slot_wrapper_defs[simp] =

94
proof/invariant-abstract/Retype_AI.thy
View File

@ -20,10 +20,14 @@ context begin interpretation Arch .
requalify_facts
global_refs_kheap
requalify_consts clearMemoryVM
end
declare global_refs_kheap[simp]
locale Retype_AI begin
lemma upto_enum_inc_1:
"a < 2^word_bits - 1 \<Longrightarrow> [(0::machine_word).e.1 + a] = [0.e.a] @ [(1+a)]"
apply (simp add:upto_enum_word)
@ -83,17 +87,12 @@ proof -
done
qed
context Arch begin global_naming ARM (*FIXME: arch_split*)
lemma clearMemoryVM_return [simp]:
extend_locale
assumes clearMemoryVM_return [simp]:
"clearMemoryVM a b = return ()"
by (simp add: clearMemoryVM_def storeWordVM_def)
lemma clearMemoryVM_return_raw:
"clearMemoryVM = (\<lambda>x y. return ())"
apply (rule ext)+
by (simp add: clearMemoryVM_def storeWordVM_def)
end
lemmas clearMemoryVM_return_raw = clearMemoryVM_return[abs_def]
lemma unat_of_nat_minus_1:
"\<lbrakk>n < 2^len_of TYPE('a);n\<noteq> 0\<rbrakk> \<Longrightarrow> (unat (((of_nat n):: 'a :: len word) - 1)) = n - 1"
@ -468,12 +467,12 @@ lemma word_plus_mono_right_split:
done
lemmas word32_plus_mono_right_split = word_plus_mono_right_split[where 'a=32, folded word_bits_def]
end
(* range_cover locale:
proves properties when a small range is inside in a large range
*)
locale range_cover =
locale range_cover = Retype_AI +
fixes ptr :: "'a :: len word"
and sz sbit n
assumes aligned: "is_aligned ptr sbit"
@ -641,6 +640,11 @@ lemma range_cover_base_le:
end
context Retype_AI begin
lemmas range_cover_def =
range_cover_def[simplified range_cover_axioms_def Retype_AI_axioms, simplified]
lemma range_cover_subset:
fixes ptr :: "'a :: len word"
assumes cover: "range_cover ptr sz sbit n"
@ -959,6 +963,8 @@ lemma shiftr_mask_cmp:
apply (simp add:le_mask_iff shiftr_shiftr)
done
end
context Arch begin global_naming ARM (*FIXME: arch_split*)
definition
"no_gs_types \<equiv> UNIV - {Structures_A.CapTableObject,
@ -1000,6 +1006,7 @@ lemma range_cover_not_zero:
apply simp
done
context Retype_AI begin
lemma range_cover_not_zero_shift:
"\<lbrakk>n \<noteq> 0; range_cover (ptr :: 'a :: len word) sz bits n; gbits \<le> bits\<rbrakk>
@ -1206,6 +1213,7 @@ done
crunch valid_pspace: do_machine_op "valid_pspace"
end
context Arch begin global_naming ARM (*FIXME: arch_split*)
declare store_pde_state_refs_of [wp]
@ -1863,6 +1871,8 @@ lemma init_arch_objects_invs_from_restricted:
done
end
context Retype_AI begin
lemma retype_region_aligned_for_init[wp]:
"\<lbrace>\<lambda>s. range_cover ptr sz (obj_bits_api new_type obj_sz) n\<rbrace>
retype_region ptr n obj_sz new_type
@ -2363,6 +2373,8 @@ lemma valid_arch_obj_default:
apply (simp add: valid_arch_obj_default')
done
end
context Arch begin global_naming ARM (*FIXME: arch_split*)
lemma vs_lookup_trans_sub2:
assumes ko: "\<And>ko p. \<lbrakk> ko_at ko p s; vs_refs ko \<noteq> {} \<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko'. vs_refs ko \<subseteq> vs_refs ko') p s'"
@ -2440,7 +2452,7 @@ lemma usable_range_emptyD:
done
context begin interpretation Arch . (*FIXME: arch_split*)
context Retype_AI begin interpretation Arch . (*FIXME: arch_split*)
lemma valid_untyped_helper:
assumes valid_c : "s \<turnstile> c"
and cte_at : "cte_wp_at (op = c) q s"
@ -2518,7 +2530,7 @@ end
locale retype_region_proofs_gen =
locale retype_region_proofs_gen = Retype_AI +
fixes s ty us ptr sz n ps s'
assumes vp: "valid_pspace s"
and vm: "valid_mdb s"
@ -3257,7 +3269,11 @@ lemma post_retype_invs:
end
end
context begin interpretation Arch . (*FIXME: arch_split*)
context Retype_AI begin interpretation Arch . (*FIXME: arch_split*)
lemmas retype_region_proofs_gen_intro =
retype_region_proofs_gen.intro[simplified Retype_AI_axioms retype_region_proofs_gen_axioms_def]
lemma use_retype_region_proofs':
assumes x: "\<And>s. \<lbrakk> retype_region_proofs s ty us ptr sz n; P s \<rbrakk>
\<Longrightarrow> Q (retype_addrs ptr ty n us) (s\<lparr>kheap :=
@ -3278,12 +3294,14 @@ lemma use_retype_region_proofs':
foldr_upd_app_if fun_upd_def[symmetric])
apply safe
apply (rule x)
apply (rule retype_region_proofs.intro[OF retype_region_proofs_gen.intro], simp_all)[1]
apply (simp add: range_cover_def obj_bits_api_def
apply (rule retype_region_proofs.intro[OF retype_region_proofs_gen_intro], simp_all)[1]
apply (clarsimp simp add: range_cover_def obj_bits_api_def
slot_bits_def word_bits_def cte_level_bits_def)+
done
end
context Retype_AI begin
lemmas use_retype_region_proofs
= use_retype_region_proofs'[where Q="\<lambda>_. Q" and P=Q, simplified]
for Q
@ -3408,50 +3426,10 @@ lemma retype_region_post_retype_invs:
done
context Arch begin global_naming ARM (*FIXME: arch_split*)
lemma retype_region_plain_invs:
"\<lbrace>invs and caps_no_overlap ptr sz and pspace_no_overlap ptr sz
and caps_overlap_reserved {ptr..ptr + of_nat n * 2 ^ obj_bits_api ty us - 1}
and region_in_kernel_window {ptr .. (ptr &&~~ mask sz) + 2 ^ sz - 1}
and K (ty = Structures_A.CapTableObject \<longrightarrow> 0 < us)
and K (range_cover ptr sz (obj_bits_api ty us) n)
and K (ty \<noteq> ArchObject PageDirectoryObj)\<rbrace>
retype_region ptr n us ty \<lbrace>\<lambda>rv. invs\<rbrace>"
apply (rule hoare_gen_asm)
apply (rule hoare_strengthen_post[OF retype_region_post_retype_invs])
apply (simp add: post_retype_invs_def)
done
end
lemma subset_not_le_trans: "\<lbrakk>\<not> A \<subset> B; C \<subseteq> B\<rbrakk> \<Longrightarrow> \<not> A \<subset> C" by auto
context Arch begin global_naming ARM (*FIXME: arch_split*)
lemma storeWord_um_eq_0:
"\<lbrace>\<lambda>m. underlying_memory m p = 0\<rbrace>
storeWord x 0
\<lbrace>\<lambda>_ m. underlying_memory m p = 0\<rbrace>"
by (simp add: storeWord_def word_rsplit_0 | wp)+
lemma clearMemory_um_eq_0:
"\<lbrace>\<lambda>m. underlying_memory m p = 0\<rbrace>
clearMemory ptr bits
\<lbrace>\<lambda>_ m. underlying_memory m p = 0\<rbrace>"
apply (clarsimp simp: clearMemory_def)
apply (wp mapM_x_wp_inv | simp)+
apply (rule hoare_pre)
apply (wp hoare_drop_imps storeWord_um_eq_0)
apply (fastforce simp: ignore_failure_def split: split_if_asm)
done
lemma cleanCacheRange_PoU_um_inv[wp]:
"\<lbrace>\<lambda>m. P (underlying_memory m)\<rbrace>
cleanCacheRange_PoU ptr w p
\<lbrace>\<lambda>_ m. P (underlying_memory m)\<rbrace>"
by (simp add: cleanCacheRange_PoU_def cleanByVA_PoU_def machine_op_lift_def machine_rest_lift_def
split_def | wp)+
end
lemma cte_wp_at_trans_state[simp]: "cte_wp_at P ptr (kheap_update f (trans_state f' s)) =
cte_wp_at P ptr (kheap_update f s)"
apply (simp add: trans_state_update[symmetric] del: trans_state_update)
@ -3542,3 +3520,5 @@ lemma no_cap_to_obj_with_diff_ref_more_update[simp]:
no_cap_to_obj_with_diff_ref cap sl s"
by (simp add: no_cap_to_obj_with_diff_ref_def)
end
end

8
proof/invariant-abstract/Schedule_AI.thy
View File

@ -12,6 +12,14 @@ theory Schedule_AI
imports VSpace_AI
begin
locale Schedule_AI begin
extend_locale
fixes Schedule_AI_dummy_const :: nat
assumes Schedule_AI_trivial_asm: "Schedule_AI_dummy_const > 0"
end
context begin interpretation Arch .
(* FIXME arch_split: some of these could be moved to generic theories
so they don't need to be unqualified. *)

6
proof/invariant-abstract/Syscall_AI.thy
View File

@ -15,9 +15,9 @@ Refinement for handleEvent and syscalls
theory Syscall_AI
imports
BCorres2_AI
Tcb_AI
Arch_AI
Interrupt_AI
"./$L4V_ARCH/ArchTcb_AI"
"./$L4V_ARCH/ArchArch_AI"
"./$L4V_ARCH/ArchInterrupt_AI"
begin
lemma schedule_invs[wp]: "\<lbrace>invs\<rbrace> (Schedule_A.schedule :: (unit,det_ext) s_monad) \<lbrace>\<lambda>rv. invs\<rbrace>"

10
proof/invariant-abstract/Tcb_AI.thy
View File

@ -9,8 +9,16 @@
*)
theory Tcb_AI
imports CNodeInv_AI
imports "./$L4V_ARCH/ArchCNodeInv_AI"
begin
locale Tcb_AI begin
extend_locale
fixes Tcb_AI_dummy_const :: nat
assumes Tcb_AI_trivial_asm: "Tcb_AI_dummy_const > 0"
end
lemma ct_in_state_weaken:
"\<lbrakk> ct_in_state Q s; \<And>st. Q st \<Longrightarrow> P st \<rbrakk> \<Longrightarrow> ct_in_state P s"

11
proof/invariant-abstract/Untyped_AI.thy
View File

@ -11,8 +11,17 @@
(* Proofs about untyped invocations. *)
theory Untyped_AI
imports Detype_AI
imports "./$L4V_ARCH/ArchDetype_AI"
begin
locale Untyped_AI begin
extend_locale
fixes Untyped_AI_dummy_const :: nat
assumes Untyped_AI_trivial_asm: "Untyped_AI_dummy_const > 0"
end
context begin interpretation Arch .
requalify_consts