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

ainvs: Add itcb_arch to the itcb projection 

This allows us to more easily show that arch specific tcb fields are
preserved by many functions of the spec. For ARM_HYP we add a
projection for the tcb_vcpu field.
This commit is contained in:
Corey Lewis 2018-06-12 15:27:41 +10:00
parent d77d31a77c
commit 97c24b95c9
9 changed files with 143 additions and 69 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

18
proof/invariant-abstract/ARM/ArchInvariants_AI.thy
View File

@ -27,8 +27,26 @@ end_qualify
-- ---------------------------------------------------------------------------
section "ARM-specific invariant definitions"
qualify ARM_A (in Arch)
type_synonym iarch_tcb = unit
end_qualify
context Arch begin global_naming ARM
definition
arch_tcb_to_iarch_tcb :: "arch_tcb \<Rightarrow> iarch_tcb"
where
"arch_tcb_to_iarch_tcb arch_tcb \<equiv> ()"
lemma iarch_tcb_context_set[simp]:
"arch_tcb_to_iarch_tcb (arch_tcb_context_set p tcb) = arch_tcb_to_iarch_tcb tcb"
by (auto simp: arch_tcb_to_iarch_tcb_def arch_tcb_context_set_def)
lemma iarch_tcb_set_registers[simp]:
"arch_tcb_to_iarch_tcb (arch_tcb_set_registers regs arch_tcb)
= arch_tcb_to_iarch_tcb arch_tcb"
by (simp add: arch_tcb_set_registers_def)
(* These simplifications allows us to keep many arch-specific proofs unchanged. *)
lemma arch_cap_fun_lift_expand[simp]:

12
proof/invariant-abstract/ARM_HYP/ArchArch_AI.thy
View File

@ -1780,11 +1780,17 @@ lemma arch_decode_inv_wf[wp]:
declare word_less_sub_le [simp]
crunches associate_vcpu_tcb, vcpu_read_reg, vcpu_write_reg, invoke_vcpu_inject_irq
crunches associate_vcpu_tcb
for pred_tcb_at[wp_unsafe]: "pred_tcb_at proj P t"
(wp: crunch_wps simp: crunch_simps)
crunches vcpu_read_reg, vcpu_write_reg, invoke_vcpu_inject_irq
for pred_tcb_at[wp]: "pred_tcb_at proj P t"
lemma perform_vcpu_invocation_pred_tcb_at[wp]:
"\<lbrace>pred_tcb_at proj P t\<rbrace> perform_vcpu_invocation iv \<lbrace>\<lambda>_. pred_tcb_at proj P t\<rbrace>"
lemma perform_vcpu_invocation_pred_tcb_at[wp_unsafe]:
"\<lbrace>pred_tcb_at proj P t and K (proj_not_field proj tcb_arch_update)\<rbrace>
perform_vcpu_invocation iv
\<lbrace>\<lambda>_. pred_tcb_at proj P t\<rbrace>"
apply (simp add: perform_vcpu_invocation_def)
apply (rule hoare_pre)
apply (wp associate_vcpu_tcb_pred_tcb_at | wpc

5
proof/invariant-abstract/ARM_HYP/ArchCNodeInv_AI.thy
View File

@ -484,6 +484,7 @@ lemma zombie_is_cap_toE_pre[CNodeInv_AI_assms]:
done
crunch st_tcb_at_halted[wp]: prepare_thread_delete "st_tcb_at halted t"
(wp: dissociate_vcpu_tcb_pred_tcb_at)
lemma finalise_cap_makes_halted_proof:
"\<lbrace>invs and valid_cap cap and (\<lambda>s. ex = is_final_cap' cap s)
@ -513,8 +514,8 @@ lemmas finalise_cap_makes_halted = finalise_cap_makes_halted_proof
crunch emptyable[wp, CNodeInv_AI_assms]: finalise_cap "emptyable sl"
(simp: crunch_simps rule: emptyable_lift
wp: crunch_wps suspend_emptyable unbind_notification_invs unbind_maybe_notification_invs)
wp: crunch_wps suspend_emptyable unbind_notification_invs
unbind_maybe_notification_invs arch_finalise_cap_pred_tcb_at)
lemma finalise_cap_not_reply_master_unlifted [CNodeInv_AI_assms]:
"(rv, s') \<in> fst (finalise_cap cap sl s) \<Longrightarrow>

2
proof/invariant-abstract/ARM_HYP/ArchDetSchedSchedule_AI.thy
View File

@ -327,7 +327,7 @@ crunch cur_thread[wp]: arch_thread_set "\<lambda>s. P (cur_thread s)"
lemma arch_thread_set_valid_sched[wp]:
"\<lbrace>valid_sched\<rbrace> arch_thread_set f t \<lbrace>\<lambda>_. valid_sched\<rbrace>"
by (rule valid_sched_lift; wp)
by (rule valid_sched_lift; wpsimp wp: arch_thread_set_pred_tcb_at)
crunch ct_not_in_q [wp, DetSchedSchedule_AI_assms]:
arch_finalise_cap, prepare_thread_delete ct_not_in_q

23
proof/invariant-abstract/ARM_HYP/ArchFinalise_AI.thy
View File

@ -528,18 +528,20 @@ lemma arch_thread_set_valid_reply_masters[wp]:
"\<lbrace>valid_reply_masters\<rbrace> arch_thread_set p v \<lbrace>\<lambda>rv. valid_reply_masters\<rbrace>"
by (rule valid_reply_masters_cte_lift) wp
lemma arch_thread_set_pred_tcb_at[wp]:
"\<lbrace>pred_tcb_at proj P t\<rbrace> arch_thread_set p v \<lbrace>\<lambda>rv. pred_tcb_at proj P t\<rbrace>"
lemma arch_thread_set_pred_tcb_at[wp_unsafe]:
"\<lbrace>pred_tcb_at proj P t and K (proj_not_field proj tcb_arch_update)\<rbrace>
arch_thread_set p v
\<lbrace>\<lambda>rv. pred_tcb_at proj P t\<rbrace>"
apply (simp add: arch_thread_set_def set_object_def)
apply wp
apply (clarsimp simp: pred_tcb_at_def obj_at_def get_tcb_rev
tcb_to_itcb_def
dest!: get_tcb_SomeD)
done
lemma arch_thread_set_valid_reply_caps[wp]:
"\<lbrace>valid_reply_caps\<rbrace> arch_thread_set p v \<lbrace>\<lambda>rv. valid_reply_caps\<rbrace>"
by (rule valid_reply_caps_st_cte_lift) wp+
by (rule valid_reply_caps_st_cte_lift)
(wpsimp wp: arch_thread_set_pred_tcb_at)+
lemma arch_thread_set_if_unsafe_then_cap[wp]:
"\<lbrace>if_unsafe_then_cap\<rbrace> arch_thread_set p v \<lbrace>\<lambda>rv. if_unsafe_then_cap\<rbrace>"
@ -556,11 +558,12 @@ lemma arch_thread_set_if_unsafe_then_cap[wp]:
lemma arch_thread_set_only_idle[wp]:
"\<lbrace>only_idle\<rbrace> arch_thread_set p v \<lbrace>\<lambda>rv. only_idle\<rbrace>"
by (wp only_idle_lift set_asid_pool_typ_at)
by (wpsimp wp: only_idle_lift set_asid_pool_typ_at
arch_thread_set_pred_tcb_at)
lemma arch_thread_set_valid_idle[wp]:
"\<lbrace>valid_idle\<rbrace> arch_thread_set p v \<lbrace>\<lambda>rv. valid_idle\<rbrace>"
by (wp valid_idle_lift)
by (wpsimp wp: valid_idle_lift arch_thread_set_pred_tcb_at)
lemma arch_thread_set_valid_ioc[wp]:
"\<lbrace>valid_ioc\<rbrace> arch_thread_set p v \<lbrace>\<lambda>rv. valid_ioc\<rbrace>"
@ -1380,9 +1383,13 @@ crunch irq_node[Finalise_AI_asms,wp]: prepare_thread_delete "\<lambda>s. P (inte
crunch irq_node[wp]: arch_finalise_cap "\<lambda>s. P (interrupt_irq_node s)"
(simp: crunch_simps wp: crunch_wps)
crunch pred_tcb_at[wp]: arch_finalise_cap "pred_tcb_at proj P t"
(simp: crunch_simps wp: crunch_wps)
crunch pred_tcb_at[wp]:
delete_asid_pool, delete_asid, unmap_page_table, unmap_page, vcpu_invalidate_active
"pred_tcb_at proj P t"
(simp: crunch_simps wp: crunch_wps test)
crunch pred_tcb_at[wp_unsafe]: arch_finalise_cap "pred_tcb_at proj P t"
(simp: crunch_simps wp: crunch_wps)
lemma tcb_cap_valid_pagetable:
"tcb_cap_valid (ArchObjectCap (PageTableCap word (Some v))) slot

23
proof/invariant-abstract/ARM_HYP/ArchInvariants_AI.thy
View File

@ -27,8 +27,31 @@ end_qualify
-- ---------------------------------------------------------------------------
section "ARM-specific invariant definitions"
qualify ARM_HYP_A (in Arch)
record iarch_tcb =
itcb_vcpu :: "obj_ref option"
end_qualify
context Arch begin global_naming ARM
definition
arch_tcb_to_iarch_tcb :: "arch_tcb \<Rightarrow> iarch_tcb"
where
"arch_tcb_to_iarch_tcb arch_tcb \<equiv> \<lparr> itcb_vcpu = tcb_vcpu arch_tcb \<rparr>"
(* Need one of these simp rules for each field in 'iarch_tcb' *)
lemma arch_tcb_to_iarch_tcb_simps[simp]:
"itcb_vcpu (arch_tcb_to_iarch_tcb arch_tcb) = tcb_vcpu arch_tcb"
by (auto simp: arch_tcb_to_iarch_tcb_def)
lemma iarch_tcb_context_set[simp]:
"arch_tcb_to_iarch_tcb (arch_tcb_context_set p tcb) = arch_tcb_to_iarch_tcb tcb"
by (auto simp: arch_tcb_to_iarch_tcb_def arch_tcb_context_set_def)
lemma iarch_tcb_set_registers[simp]:
"arch_tcb_to_iarch_tcb (arch_tcb_set_registers regs arch_tcb)
= arch_tcb_to_iarch_tcb arch_tcb"
by (simp add: arch_tcb_set_registers_def)
lemmas vspace_bits_defs = pd_bits_def pde_bits_def pt_bits_def pte_bits_def pageBits_def

106
proof/invariant-abstract/Invariants_AI.thy
View File

@ -17,6 +17,7 @@ context begin interpretation Arch .
requalify_types
vs_chain
vs_ref
iarch_tcb
requalify_consts
not_kernel_window
@ -64,6 +65,7 @@ requalify_consts
tcb_arch_ref
valid_arch_mdb
arch_tcb_to_iarch_tcb
requalify_facts
valid_arch_sizes
@ -112,6 +114,8 @@ lemmas [simp] =
tcb_bits_def
endpoint_bits_def
ntfn_bits_def
iarch_tcb_context_set
iarch_tcb_set_registers
end
@ -154,20 +158,21 @@ abbreviation
(*
* sseefried: 'itcb' is projection of the "mostly preserved" fields of 'tcb'. Many functions
* in the spec will leave these fields of a TCB unchanged. The 'crunch' tool is easily able
* to ascertain this from the types of the fields.
*
* The 'itcb' record is closely associated with the 'pred_tcb_at' definition.
* 'pred_tcb_at' is used to assert an arbitrary predicate over the fields in 'itcb' for a TCB
* Before the introduction of this data structure 'st_tcb_at' was defined directly. It is
* now an abbreviation of a partial application of the 'pred_tcb_at' function, specifically
* a partial application to the projection function 'itcb_state'.
*
* The advantage of this approach is that we an assert 'pred_tcb_at proj P t' is preserved
* across calls to many functions. We get "for free" that 'st_tcb_at P t' is also preserved.
* In the future we may introduce other abbreviations that assert preservation over other
* fields in the TCB record.
'itcb' is a projection of the "mostly preserved" fields of 'tcb'. Many
functions in the spec will leave these fields of a TCB unchanged. The 'crunch'
tool is easily able to ascertain this from the types of the fields.
The 'itcb' record is closely associated with the 'pred_tcb_at' definition.
'pred_tcb_at' is used to assert an arbitrary predicate over the fields in
'itcb' for a TCB. Before the introduction of this data structure 'st_tcb_at'
was defined directly. It is now an abbreviation of a partial application of
the 'pred_tcb_at' function, specifically a partial application to the
projection function 'itcb_state'.
The advantage of this approach is that we an assert 'pred_tcb_at proj P t' is
preserved across calls to many functions. We get "for free" that 'st_tcb_at P
t' is also preserved. In the future we may introduce other abbreviations that
assert preservation over other fields in the TCB record.
*)
record itcb =
itcb_state :: thread_state
@ -176,49 +181,48 @@ record itcb =
itcb_fault :: "fault option"
itcb_bound_notification :: "obj_ref option"
itcb_mcpriority :: priority
itcb_arch :: iarch_tcb
definition
tcb_to_itcb :: "tcb \<Rightarrow> itcb"
where
"tcb_to_itcb tcb \<equiv>
\<lparr> itcb_state = tcb_state tcb,
itcb_fault_handler = tcb_fault_handler tcb,
itcb_ipc_buffer = tcb_ipc_buffer tcb,
itcb_fault = tcb_fault tcb,
itcb_bound_notification = tcb_bound_notification tcb,
itcb_mcpriority = tcb_mcpriority tcb,
itcb_arch = arch_tcb_to_iarch_tcb (tcb_arch tcb) \<rparr>"
definition "tcb_to_itcb tcb \<equiv> \<lparr> itcb_state = tcb_state tcb,
itcb_fault_handler = tcb_fault_handler tcb,
itcb_ipc_buffer = tcb_ipc_buffer tcb,
itcb_fault = tcb_fault tcb,
itcb_bound_notification = tcb_bound_notification tcb,
itcb_mcpriority = tcb_mcpriority tcb\<rparr>"
(*
The simplification rules below are used to help produce lemmas that talk about
fields of the 'tcb' data structure rather than the 'itcb' data structure when
the lemma refers to a predicate of the form 'pred_tcb_at proj P t'.
(* sseefried: The simplification rules below are used to help produce
* lemmas that talk about fields of the 'tcb' data structure rather than
* the 'itcb' data structure when the lemma refers to a predicate of the
* form 'pred_tcb_at proj P t'.
*
* e.g. You might have a lemma that has an assumption
* \<And>tcb. itcb_state (tcb_to_itcb (f tcb)) = itcb_state (tcb_to_itcb tcb)
*
* This simplifies to:
* \<And>tcb. tcb_state (f tcb) = tcb_state tcb
*)
e.g. You might have a lemma that has an assumption
\<And>tcb. itcb_state (tcb_to_itcb (f tcb)) = itcb_state (tcb_to_itcb tcb)
This simplifies to:
\<And>tcb. tcb_state (f tcb) = tcb_state tcb
*)
(* Need one of these simp rules for each field in 'itcb' *)
lemma [simp]: "itcb_state (tcb_to_itcb tcb) = tcb_state tcb"
lemma tcb_to_itcb_simps[simp]:
"itcb_state (tcb_to_itcb tcb) = tcb_state tcb"
"itcb_fault_handler (tcb_to_itcb tcb) = tcb_fault_handler tcb"
"itcb_ipc_buffer (tcb_to_itcb tcb) = tcb_ipc_buffer tcb"
"itcb_fault (tcb_to_itcb tcb) = tcb_fault tcb"
"itcb_bound_notification (tcb_to_itcb tcb) = tcb_bound_notification tcb"
"itcb_mcpriority (tcb_to_itcb tcb) = tcb_mcpriority tcb"
"itcb_arch (tcb_to_itcb tcb) = arch_tcb_to_iarch_tcb (tcb_arch tcb)"
by (auto simp: tcb_to_itcb_def)
(* Need one of these simp rules for each field in 'itcb' *)
lemma [simp]: "itcb_fault_handler (tcb_to_itcb tcb) = tcb_fault_handler tcb"
by (auto simp: tcb_to_itcb_def)
(* Need one of these simp rules for each field in 'itcb' *)
lemma [simp]: "itcb_ipc_buffer (tcb_to_itcb tcb) = tcb_ipc_buffer tcb"
by (auto simp: tcb_to_itcb_def)
(* Need one of these simp rules for each field in 'itcb' *)
lemma [simp]: "itcb_fault (tcb_to_itcb tcb) = tcb_fault tcb"
by (auto simp: tcb_to_itcb_def)
(* Need one of these simp rules for each field in 'itcb' *)
lemma [simp]: "itcb_bound_notification (tcb_to_itcb tcb) = tcb_bound_notification tcb"
by (auto simp: tcb_to_itcb_def)
lemma [simp]: "itcb_mcpriority (tcb_to_itcb tcb) = tcb_mcpriority tcb"
by (auto simp: tcb_to_itcb_def)
(* This is used to assert whether an itcb projection is affected by a tcb
field update, such as tcb_arch_update. *)
abbreviation
"proj_not_field proj field_upd \<equiv>
\<forall>f tcb. proj (tcb_to_itcb ((field_upd f) tcb)) = proj (tcb_to_itcb tcb)"
definition
pred_tcb_at :: "(itcb \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> machine_word \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
@ -233,10 +237,8 @@ abbreviation "mcpriority_tcb_at \<equiv> pred_tcb_at itcb_mcpriority"
lemma st_tcb_at_def: "st_tcb_at test \<equiv> obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> test (tcb_state tcb))"
by (simp add: pred_tcb_at_def)
text {* cte with property at *}
definition
cte_wp_at :: "(cap \<Rightarrow> bool) \<Rightarrow> cslot_ptr \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
where

5
proof/invariant-abstract/TcbAcc_AI.thy
View File

@ -754,8 +754,7 @@ lemma ct_in_state_thread_state_lift:
lemma as_user_ct_in_state:
"\<lbrace>ct_in_state x\<rbrace> as_user t f \<lbrace>\<lambda>_. ct_in_state x\<rbrace>"
by (rule ct_in_state_thread_state_lift) (wp as_user_ct)+
by (rule ct_in_state_thread_state_lift) (wpsimp wp: as_user_ct)+
lemma set_object_ntfn_at:
"\<lbrace> ntfn_at p and tcb_at r \<rbrace> set_object r obj \<lbrace> \<lambda>rv. ntfn_at p \<rbrace>"
@ -1853,7 +1852,7 @@ lemma set_mrs_thread_set_dmo:
apply (wpsimp wp: ts mapM_wp' dmo)
done
lemma set_mrs_st_tcb [wp]:
lemma set_mrs_pred_tcb_at [wp]:
"\<lbrace>pred_tcb_at proj P t\<rbrace> set_mrs r t' mrs \<lbrace>\<lambda>rv. pred_tcb_at proj P t\<rbrace>"
apply (rule set_mrs_thread_set_dmo)
apply (rule thread_set_no_change_tcb_pred)

18
proof/invariant-abstract/X64/ArchInvariants_AI.thy
View File

@ -29,8 +29,26 @@ end_qualify
-- ---------------------------------------------------------------------------
section "X64-specific invariant definitions"
qualify X64_A (in Arch)
type_synonym iarch_tcb = unit
end_qualify
context Arch begin global_naming X64
definition
arch_tcb_to_iarch_tcb :: "arch_tcb \<Rightarrow> iarch_tcb"
where
"arch_tcb_to_iarch_tcb arch_tcb \<equiv> ()"
lemma iarch_tcb_context_set[simp]:
"arch_tcb_to_iarch_tcb (arch_tcb_context_set p tcb) = arch_tcb_to_iarch_tcb tcb"
by (auto simp: arch_tcb_to_iarch_tcb_def arch_tcb_context_set_def)
lemma iarch_tcb_set_registers[simp]:
"arch_tcb_to_iarch_tcb (arch_tcb_set_registers regs arch_tcb)
= arch_tcb_to_iarch_tcb arch_tcb"
by (simp add: arch_tcb_set_registers_def)
(* These simplifications allows us to keep many arch-specific proofs unchanged. *)
lemma arch_cap_fun_lift_expand[simp]: