adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
lh-l4v/proof/infoflow/FinalCaps.thy

3281 lines
136 KiB
Plaintext
Raw Normal View History

Import release snapshot.
2014-07-14 19:32:44 +00:00
(*
* Copyright 2014, NICTA
*
* 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(NICTA_GPL)
*)
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
text {*
The InfoFlow theorem needs that caps shared between labels cannot be deleted.
In order to do that, this file introduces a dummy label, SilcLabel that will
own all those caps. It then proves all the properties needed about SilcLabel
doing its job.
*}
Import release snapshot.
2014-07-14 19:32:44 +00:00
theory FinalCaps
imports InfoFlow
begin
arch_split: requalify abstract theories
2016-04-27 06:48:03 +00:00
context begin interpretation Arch . (*FIXME: arch_split*)
arch_split: InfoFlow checking
2016-04-24 05:44:40 +00:00
Genericise deletion actions that occur after empty_slot This patch adds a generic "post_cap_deletion" step that is called by finalise_slot. Previous to this, the only caps which had actions required at this stage were IRQHandlerCaps -- it was required that the IRQ bitmap be updated after the cap itself was removed (as the invariants state that for any existing IRQHandlerCap, the corresponding bit in the IRQ bitmap must be set). By genericising this, we add the capacity for new, arch-specific post cap deletion actions to occur in the future.
2018-02-07 04:08:43 +00:00
declare arch_gen_obj_refs_def[simp]
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
definition cap_points_to_label
where
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
"cap_points_to_label aag cap l \<equiv>
Import release snapshot.
2014-07-14 19:32:44 +00:00
(\<forall> x \<in> Structures_A.obj_refs cap. (pasObjectAbs aag x = l))
\<and> (\<forall> x \<in> cap_irqs cap. (pasIRQAbs aag x = l))"
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
definition intra_label_cap
where
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
"intra_label_cap aag slot s \<equiv>
Isabelle2018: new "op x" syntax; now is "(x)" (result of "isabelle update_op -m <dir>")
2018-06-09 08:30:53 +00:00
(\<forall> cap. cte_wp_at ((=) cap) slot s \<longrightarrow>
Import release snapshot.
2014-07-14 19:32:44 +00:00
(cap_points_to_label aag cap (pasObjectAbs aag (fst slot))))"
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
definition slots_holding_overlapping_caps :: "cap \<Rightarrow> ('z::state_ext) state \<Rightarrow> cslot_ptr set"
Import release snapshot.
2014-07-14 19:32:44 +00:00
where
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
"slots_holding_overlapping_caps cap s \<equiv>
Import release snapshot.
2014-07-14 19:32:44 +00:00
{cref. \<exists>cap'. fst (get_cap cref s) = {(cap', s)} \<and>
(Structures_A.obj_refs cap \<inter> Structures_A.obj_refs cap' \<noteq> {} \<or>
Genericise deletion actions that occur after empty_slot This patch adds a generic "post_cap_deletion" step that is called by finalise_slot. Previous to this, the only caps which had actions required at this stage were IRQHandlerCaps -- it was required that the IRQ bitmap be updated after the cap itself was removed (as the invariants state that for any existing IRQHandlerCap, the corresponding bit in the IRQ bitmap must be set). By genericising this, we add the capacity for new, arch-specific post cap deletion actions to occur in the future.
2018-02-07 04:08:43 +00:00
cap_irqs cap \<inter> cap_irqs cap' \<noteq> {} \<or>
arch_gen_refs cap \<inter> arch_gen_refs cap' \<noteq> {})}"
Import release snapshot.
2014-07-14 19:32:44 +00:00
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
text {* We introduce a new label. The name 'silc' here stands for 'safe inter-label caps',
Import release snapshot.
2014-07-14 19:32:44 +00:00
since the domain with this label holds copies of all inter-label caps to ensure that
any others remain 'safe' by never becoming final caps, which would otherwise introduce
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
a potential covert storage channel *}
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
datatype 'a subject_label = OrdinaryLabel 'a | SilcLabel
Import release snapshot.
2014-07-14 19:32:44 +00:00
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
text{* We need to introduce an equivalence on the dummy domain, and add
Import release snapshot.
2014-07-14 19:32:44 +00:00
it to the state that the current subject can read from (i.e.
effectively add it to the current subject's domain), to complete
the proof for is_final_cap. This will necessitate showing that
the dummy domain's state is never affected, but this should be
relatively easy. The annoying part is that now we end up proving
a different property; it will take some finesse to avoid having
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
to do a search/replace on @{term reads_respects} \<rightarrow> reads_respects_f *}
definition silc_dom_equiv
where
Import release snapshot.
2014-07-14 19:32:44 +00:00
"silc_dom_equiv aag \<equiv>
equiv_for (\<lambda> x. pasObjectAbs aag x = SilcLabel) kheap"
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
text{* This is an invariant that ensures that the info leak due to is_final_cap doesn't
arise. Silc stands for 'safe inter label caps'.
We include a condition that the contents of SilcLabel wrt the kheap are unchanged from
some fixed reference state, since we invariably use this fact to reason that the
Import release snapshot.
2014-07-14 19:32:44 +00:00
invariant is preserved anyway. Including it here saves duplicating essentially identical
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
reasoning. *}
Import release snapshot.
2014-07-14 19:32:44 +00:00
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
definition silc_inv :: "'a subject_label PAS \<Rightarrow> det_ext state \<Rightarrow> det_ext state \<Rightarrow> bool"
where
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
"silc_inv aag st s \<equiv>
Import release snapshot.
2014-07-14 19:32:44 +00:00
(SilcLabel \<noteq> pasSubject aag) \<and>
(\<forall> x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists> sz. cap_table_at sz x s)) \<and>
(\<forall> y auth. (y,auth,SilcLabel) \<in> pasPolicy aag \<longrightarrow> y = SilcLabel) \<and>
Isabelle2018: new "op x" syntax; now is "(x)" (result of "isabelle update_op -m <dir>")
2018-06-09 08:30:53 +00:00
(\<forall> slot cap. cte_wp_at ((=) cap) slot s \<and>
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
\<not> intra_label_cap aag slot s \<longrightarrow>
Import release snapshot.
2014-07-14 19:32:44 +00:00
(\<exists> lslot. lslot \<in> slots_holding_overlapping_caps cap s \<and>
(pasObjectAbs aag (fst lslot) = SilcLabel))) \<and>
all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s) \<and>
silc_dom_equiv aag st s"
lemma silc_inv_exst[simp]:
"silc_inv aag st (trans_state f s) = silc_inv aag st s"
apply(auto simp: silc_inv_def intra_label_cap_def slots_holding_overlapping_caps_def silc_dom_equiv_def equiv_for_def)
done
arch_split: InfoFlow checking
2016-04-24 05:44:40 +00:00
end
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
lemma (in is_extended') silc_inv[wp]: "I (silc_inv aag st)" by (rule lift_inv,simp)
Import release snapshot.
2014-07-14 19:32:44 +00:00
arch_split: requalify abstract theories
2016-04-27 06:48:03 +00:00
context begin interpretation Arch . (*FIXME: arch_split*)
arch_split: InfoFlow checking
2016-04-24 05:44:40 +00:00
Import release snapshot.
2014-07-14 19:32:44 +00:00
lemma get_cap_cte_wp_at':
Isabelle2018: new "op x" syntax; now is "(x)" (result of "isabelle update_op -m <dir>")
2018-06-09 08:30:53 +00:00
"(fst (get_cap p s) = {(r,s)}) = cte_wp_at ((=) r) p s"
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(auto simp: cte_wp_at_def)
done
lemma silc_invD:
"\<lbrakk>silc_inv aag st s;
Isabelle2018: new "op x" syntax; now is "(x)" (result of "isabelle update_op -m <dir>")
2018-06-09 08:30:53 +00:00
cte_wp_at ((=) cap) slot s;
Import release snapshot.
2014-07-14 19:32:44 +00:00
\<not> intra_label_cap aag slot s\<rbrakk> \<Longrightarrow>
(\<exists> lslot. lslot \<in> slots_holding_overlapping_caps cap s \<and>
(pasObjectAbs aag (fst lslot) = SilcLabel))"
apply(clarsimp simp: silc_inv_def)
apply(drule_tac x="fst slot" in spec, drule_tac x="snd slot" in spec, fastforce)
done
lemma is_final_cap'_def4:
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
"is_final_cap' cap s \<equiv>
Import release snapshot.
2014-07-14 19:32:44 +00:00
\<exists> a b. slots_holding_overlapping_caps cap s = {(a,b)}"
Genericise deletion actions that occur after empty_slot This patch adds a generic "post_cap_deletion" step that is called by finalise_slot. Previous to this, the only caps which had actions required at this stage were IRQHandlerCaps -- it was required that the IRQ bitmap be updated after the cap itself was removed (as the invariants state that for any existing IRQHandlerCap, the corresponding bit in the IRQ bitmap must be set). By genericising this, we add the capacity for new, arch-specific post cap deletion actions to occur in the future.
2018-02-07 04:08:43 +00:00
apply(simp add: is_final_cap'_def slots_holding_overlapping_caps_def gen_obj_refs_Int)
Import release snapshot.
2014-07-14 19:32:44 +00:00
done
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
(* I think this property is strong enough to give us a sane
Import release snapshot.
2014-07-14 19:32:44 +00:00
confidentiality rule for is_final_cap. This is true, so long as
we include the dummy domain l in what the current subject can
read *)
lemma silc_inv:
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
"silc_inv aag st s \<Longrightarrow>
Isabelle2018: new "op x" syntax; now is "(x)" (result of "isabelle update_op -m <dir>")
2018-06-09 08:30:53 +00:00
(\<forall> cap slot. cte_wp_at ((=) cap) slot s \<and> is_final_cap' cap s \<longrightarrow>
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
(intra_label_cap aag slot s \<or> (pasObjectAbs aag (fst slot) = SilcLabel)))"
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply clarsimp
apply(erule contrapos_np)
apply(drule (2) silc_invD)
apply(subgoal_tac "(a,b) \<in> slots_holding_overlapping_caps cap s")
apply(clarsimp simp: is_final_cap'_def4 cte_wp_at_def)
apply(auto simp: slots_holding_overlapping_caps_def cte_wp_at_def)
done
lemma cte_wp_at_pspace':
"kheap s (fst p) = kheap s' (fst p) \<Longrightarrow> cte_wp_at P p s = cte_wp_at P p s'"
apply(rule iffI)
apply(erule cte_wp_atE)
apply(auto intro: cte_wp_at_cteI dest: sym)[1]
apply(auto intro: cte_wp_at_tcbI dest: sym)[1]
apply(erule cte_wp_atE)
apply(auto intro: cte_wp_at_cteI dest: sym)[1]
apply(auto intro: cte_wp_at_tcbI dest: sym)[1]
done
lemma cte_wp_at_intra_label_cap:
Isabelle2018: new "op x" syntax; now is "(x)" (result of "isabelle update_op -m <dir>")
2018-06-09 08:30:53 +00:00
"\<lbrakk>cte_wp_at ((=) cap) slot s; cte_wp_at ((=) cap) slot t;
Import release snapshot.
2014-07-14 19:32:44 +00:00
intra_label_cap aag slot s\<rbrakk> \<Longrightarrow> intra_label_cap aag slot t"
apply(clarsimp simp: intra_label_cap_def)
apply(auto dest: cte_wp_at_eqD2)
done
lemma not_is_final_cap_cte_wp_at:
Isabelle2018: new "op x" syntax; now is "(x)" (result of "isabelle update_op -m <dir>")
2018-06-09 08:30:53 +00:00
"\<lbrakk>\<not> is_final_cap' cap s; cte_wp_at ((=) cap) slot s;
Genericise deletion actions that occur after empty_slot This patch adds a generic "post_cap_deletion" step that is called by finalise_slot. Previous to this, the only caps which had actions required at this stage were IRQHandlerCaps -- it was required that the IRQ bitmap be updated after the cap itself was removed (as the invariants state that for any existing IRQHandlerCap, the corresponding bit in the IRQ bitmap must be set). By genericising this, we add the capacity for new, arch-specific post cap deletion actions to occur in the future.
2018-02-07 04:08:43 +00:00
Structures_A.obj_refs cap \<noteq> {} \<or> cap_irqs cap \<noteq> {} \<or> arch_gen_refs cap \<noteq> {}\<rbrakk> \<Longrightarrow>
Import release snapshot.
2014-07-14 19:32:44 +00:00
\<exists> slot'. slot' \<noteq> slot \<and> slot' \<in> slots_holding_overlapping_caps cap s"
apply(simp add: is_final_cap'_def4)
apply(subgoal_tac "slot \<in> slots_holding_overlapping_caps cap s")
apply(drule_tac x="fst slot" in spec, drule_tac x="snd slot" in spec)
apply simp
apply fastforce
apply(auto simp: slots_holding_overlapping_caps_def get_cap_cte_wp_at')
done
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
Import release snapshot.
2014-07-14 19:32:44 +00:00
lemma is_final_then_nonempty_refs:
"is_final_cap' cap s \<Longrightarrow>
Genericise deletion actions that occur after empty_slot This patch adds a generic "post_cap_deletion" step that is called by finalise_slot. Previous to this, the only caps which had actions required at this stage were IRQHandlerCaps -- it was required that the IRQ bitmap be updated after the cap itself was removed (as the invariants state that for any existing IRQHandlerCap, the corresponding bit in the IRQ bitmap must be set). By genericising this, we add the capacity for new, arch-specific post cap deletion actions to occur in the future.
2018-02-07 04:08:43 +00:00
Structures_A.obj_refs cap \<noteq> {} \<or> cap_irqs cap \<noteq> {} \<or> arch_gen_refs cap \<noteq> {}"
apply(auto simp add: is_final_cap'_def gen_obj_refs_def)
Import release snapshot.
2014-07-14 19:32:44 +00:00
done
lemma caps_ref_single_objects:
"\<lbrakk>x \<in> Structures_A.obj_refs cap;
y \<in> Structures_A.obj_refs cap\<rbrakk> \<Longrightarrow>
x = y"
apply(case_tac cap)
apply(simp_all)
done
lemma caps_ref_single_irqs:
"\<lbrakk>x \<in> cap_irqs cap;
y \<in> cap_irqs cap\<rbrakk> \<Longrightarrow>
x = y"
apply(case_tac cap)
apply(simp_all)
done
Genericise deletion actions that occur after empty_slot This patch adds a generic "post_cap_deletion" step that is called by finalise_slot. Previous to this, the only caps which had actions required at this stage were IRQHandlerCaps -- it was required that the IRQ bitmap be updated after the cap itself was removed (as the invariants state that for any existing IRQHandlerCap, the corresponding bit in the IRQ bitmap must be set). By genericising this, we add the capacity for new, arch-specific post cap deletion actions to occur in the future.
2018-02-07 04:08:43 +00:00
lemma caps_ref_single_arch_gen_refs:
"\<lbrakk>x \<in> arch_gen_refs cap; y \<in> arch_gen_refs cap\<rbrakk> \<Longrightarrow> x = y"
apply (case_tac cap)
apply simp_all
done
Import release snapshot.
2014-07-14 19:32:44 +00:00
lemma not_is_final_cap:
Isabelle2018: new "op x" syntax; now is "(x)" (result of "isabelle update_op -m <dir>")
2018-06-09 08:30:53 +00:00
"\<lbrakk>slot' \<noteq> slot; cte_wp_at ((=) cap) slot t;
cte_wp_at ((=) cap') slot' t;
Import release snapshot.
2014-07-14 19:32:44 +00:00
Structures_A.obj_refs cap \<inter> Structures_A.obj_refs cap' =
Genericise deletion actions that occur after empty_slot This patch adds a generic "post_cap_deletion" step that is called by finalise_slot. Previous to this, the only caps which had actions required at this stage were IRQHandlerCaps -- it was required that the IRQ bitmap be updated after the cap itself was removed (as the invariants state that for any existing IRQHandlerCap, the corresponding bit in the IRQ bitmap must be set). By genericising this, we add the capacity for new, arch-specific post cap deletion actions to occur in the future.
2018-02-07 04:08:43 +00:00
{} \<longrightarrow> cap_irqs cap \<inter> cap_irqs cap' = {} \<longrightarrow>
arch_gen_refs cap \<inter> arch_gen_refs cap' \<noteq> {}\<rbrakk> \<Longrightarrow>
Import release snapshot.
2014-07-14 19:32:44 +00:00
\<not> is_final_cap' cap t"
apply(rule ccontr)
Genericise deletion actions that occur after empty_slot This patch adds a generic "post_cap_deletion" step that is called by finalise_slot. Previous to this, the only caps which had actions required at this stage were IRQHandlerCaps -- it was required that the IRQ bitmap be updated after the cap itself was removed (as the invariants state that for any existing IRQHandlerCap, the corresponding bit in the IRQ bitmap must be set). By genericising this, we add the capacity for new, arch-specific post cap deletion actions to occur in the future.
2018-02-07 04:08:43 +00:00
apply(clarsimp simp: is_final_cap'_def get_cap_cte_wp_at' gen_obj_refs_def)
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(erule_tac B="{(a,b)}" in equalityE)
apply(frule_tac c=slot in subsetD)
apply fastforce
apply(drule_tac c=slot' in subsetD)
Genericise deletion actions that occur after empty_slot This patch adds a generic "post_cap_deletion" step that is called by finalise_slot. Previous to this, the only caps which had actions required at this stage were IRQHandlerCaps -- it was required that the IRQ bitmap be updated after the cap itself was removed (as the invariants state that for any existing IRQHandlerCap, the corresponding bit in the IRQ bitmap must be set). By genericising this, we add the capacity for new, arch-specific post cap deletion actions to occur in the future.
2018-02-07 04:08:43 +00:00
subgoal by fastforce
by fastforce
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
Import release snapshot.
2014-07-14 19:32:44 +00:00
lemma caps_ref_either_an_object_or_irq:
"ref \<in> Structures_A.obj_refs cap' \<Longrightarrow>
Genericise deletion actions that occur after empty_slot This patch adds a generic "post_cap_deletion" step that is called by finalise_slot. Previous to this, the only caps which had actions required at this stage were IRQHandlerCaps -- it was required that the IRQ bitmap be updated after the cap itself was removed (as the invariants state that for any existing IRQHandlerCap, the corresponding bit in the IRQ bitmap must be set). By genericising this, we add the capacity for new, arch-specific post cap deletion actions to occur in the future.
2018-02-07 04:08:43 +00:00
(cap_irqs cap' = {} \<and> arch_gen_refs cap' = {})"
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(case_tac cap', simp_all)
done
lemma caps_ref_either_an_object_or_irq':
"ref \<in> cap_irqs cap' \<Longrightarrow>
Genericise deletion actions that occur after empty_slot This patch adds a generic "post_cap_deletion" step that is called by finalise_slot. Previous to this, the only caps which had actions required at this stage were IRQHandlerCaps -- it was required that the IRQ bitmap be updated after the cap itself was removed (as the invariants state that for any existing IRQHandlerCap, the corresponding bit in the IRQ bitmap must be set). By genericising this, we add the capacity for new, arch-specific post cap deletion actions to occur in the future.
2018-02-07 04:08:43 +00:00
(Structures_A.obj_refs cap' = {} \<and> arch_gen_refs cap' = {})"
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(case_tac cap', simp_all)
done
Genericise deletion actions that occur after empty_slot This patch adds a generic "post_cap_deletion" step that is called by finalise_slot. Previous to this, the only caps which had actions required at this stage were IRQHandlerCaps -- it was required that the IRQ bitmap be updated after the cap itself was removed (as the invariants state that for any existing IRQHandlerCap, the corresponding bit in the IRQ bitmap must be set). By genericising this, we add the capacity for new, arch-specific post cap deletion actions to occur in the future.
2018-02-07 04:08:43 +00:00
lemma caps_ref_either_an_object_or_irq'':
"ref \<in> arch_gen_refs cap' \<Longrightarrow>
(Structures_A.obj_refs cap' = {} \<and> cap_irqs cap' = {})"
apply(case_tac cap', simp_all)
done
Import release snapshot.
2014-07-14 19:32:44 +00:00
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
definition reads_equiv_f
where
Import release snapshot.
2014-07-14 19:32:44 +00:00
"reads_equiv_f aag s s' \<equiv> reads_equiv aag s s' \<and> silc_dom_equiv aag s s'"
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
abbreviation reads_respects_f
where
Import release snapshot.
2014-07-14 19:32:44 +00:00
"reads_respects_f aag l P f \<equiv> equiv_valid_inv (reads_equiv_f aag) (affects_equiv aag l) P f"
lemma intra_label_capD:
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
"\<lbrakk>intra_label_cap aag slot s;
Isabelle2018: new "op x" syntax; now is "(x)" (result of "isabelle update_op -m <dir>")
2018-06-09 08:30:53 +00:00
cte_wp_at ((=) cap) slot s\<rbrakk> \<Longrightarrow>
Import release snapshot.
2014-07-14 19:32:44 +00:00
(cap_points_to_label aag cap (pasObjectAbs aag (fst slot)))"
by(auto simp: intra_label_cap_def)
lemma is_subject_kheap_eq:
"\<lbrakk>reads_equiv aag s t; is_subject aag ptr\<rbrakk> \<Longrightarrow> kheap s ptr = kheap t ptr"
apply(clarsimp simp: reads_equiv_def2)
apply(erule states_equiv_forE_kheap)
apply(blast intro: aag_can_read_self)
done
Genericise deletion actions that occur after empty_slot This patch adds a generic "post_cap_deletion" step that is called by finalise_slot. Previous to this, the only caps which had actions required at this stage were IRQHandlerCaps -- it was required that the IRQ bitmap be updated after the cap itself was removed (as the invariants state that for any existing IRQHandlerCap, the corresponding bit in the IRQ bitmap must be set). By genericising this, we add the capacity for new, arch-specific post cap deletion actions to occur in the future.
2018-02-07 04:08:43 +00:00
lemma arch_gen_refs_no_intersection[simp]:
"arch_gen_refs c \<inter> arch_gen_refs c' = {}"
by (cases c; auto)
Import release snapshot.
2014-07-14 19:32:44 +00:00
lemma is_final_cap_reads_respects_helper:
Isabelle2018: new "op x" syntax; now is "(x)" (result of "isabelle update_op -m <dir>")
2018-06-09 08:30:53 +00:00
"\<lbrakk>silc_inv aag st s; cte_wp_at ((=) cap) slot s;
silc_inv aag st t; cte_wp_at ((=) cap) slot t;
Import release snapshot.
2014-07-14 19:32:44 +00:00
is_subject aag (fst slot); reads_equiv aag s t;
silc_dom_equiv aag s t; affects_equiv aag l s t;
kheap s (fst slot) = kheap t (fst slot);
Isabelle2018: new "op x" syntax; now is "(x)" (result of "isabelle update_op -m <dir>")
2018-06-09 08:30:53 +00:00
cte_wp_at ((=) cap) slot s =
cte_wp_at ((=) cap) slot t;
Import release snapshot.
2014-07-14 19:32:44 +00:00
is_final_cap' cap s\<rbrakk>
\<Longrightarrow> is_final_cap' cap t"
apply(frule_tac s=s in silc_inv)
apply(drule_tac x=cap in spec, drule_tac x="slot" in spec, simp)
apply(erule disjE)
prefer 2
apply(simp add: silc_inv_def)
apply(frule_tac s=s and t=t in cte_wp_at_intra_label_cap, assumption+)
apply(rule ccontr)
apply(drule not_is_final_cap_cte_wp_at)
apply assumption
apply(erule is_final_then_nonempty_refs)
apply(elim exE conjE, rename_tac slot')
apply(simp add: slots_holding_overlapping_caps_def get_cap_cte_wp_at')
apply(elim exE conjE, rename_tac cap')
apply(case_tac "is_subject aag (fst slot')")
(* this case is easy, since the new cap in question must also exist
in s too, and so the original cap in s is not final, creating
a clear contradiction *)
apply(drule_tac ptr="fst slot'" in is_subject_kheap_eq, assumption)
Isabelle2018: new "op x" syntax; now is "(x)" (result of "isabelle update_op -m <dir>")
2018-06-09 08:30:53 +00:00
apply(cut_tac p="slot'"and s=s and s'=t and P="(=) cap'" in cte_wp_at_pspace', assumption)
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(subgoal_tac "\<not> is_final_cap' cap s")
apply blast
apply(rule not_is_final_cap)
apply assumption
apply assumption
apply simp
Genericise deletion actions that occur after empty_slot This patch adds a generic "post_cap_deletion" step that is called by finalise_slot. Previous to this, the only caps which had actions required at this stage were IRQHandlerCaps -- it was required that the IRQ bitmap be updated after the cap itself was removed (as the invariants state that for any existing IRQHandlerCap, the corresponding bit in the IRQ bitmap must be set). By genericising this, we add the capacity for new, arch-specific post cap deletion actions to occur in the future.
2018-02-07 04:08:43 +00:00
apply clarsimp
Import release snapshot.
2014-07-14 19:32:44 +00:00
(* on the other hand, the new cap in t is now clearly not
intra_label. So SilcLabel must have an overlapping cap.
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
This overlapping cap will overlap the original one,
Import release snapshot.
2014-07-14 19:32:44 +00:00
since caps reference only a single object. It will be
present in s as well, and so the original one won't be final;
this creates a clear contradiction *)
apply(subgoal_tac "\<not> intra_label_cap aag slot' t")
apply(drule_tac s=t and cap=cap' and slot=slot' in silc_invD)
apply assumption
apply assumption
apply(erule exE, rename_tac lslot)
apply(erule conjE)
apply(simp add: slots_holding_overlapping_caps_def get_cap_cte_wp_at')
apply(elim exE conjE, rename_tac lcap)
apply(subgoal_tac "\<not> is_final_cap' cap s")
apply blast
apply(rule_tac slot=slot and slot'=lslot in not_is_final_cap)
apply(fastforce simp: silc_inv_def)
apply assumption
apply(rule_tac s1=t in cte_wp_at_pspace'[THEN iffD1])
apply(fastforce simp: silc_dom_equiv_def elim: equiv_forE)
apply assumption
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
apply(simp add: intra_label_cap_def)
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(elim exE conjE)
apply(drule (1) cte_wp_at_eqD2, simp)
apply(simp add: cap_points_to_label_def)
apply(erule disjE)
apply(erule bexE, rename_tac ref)
apply(frule caps_ref_either_an_object_or_irq)
apply(subgoal_tac "ref \<in> Structures_A.obj_refs cap \<and> ref \<in> Structures_A.obj_refs lcap")
apply blast
apply(blast dest: caps_ref_single_objects)
apply(erule bexE, rename_tac ref)
apply(frule caps_ref_either_an_object_or_irq')
apply(subgoal_tac "ref \<in> cap_irqs cap \<and> ref \<in> cap_irqs lcap")
apply blast
apply(blast dest: caps_ref_single_irqs)
(* we have to show that cap' at slot' is not intra_label.
If it were intra_label, then it would exist in s too.
And so cap would not be final, creating a contradiction *)
apply(rule notI)
apply(drule_tac s=t and slot=slot' in intra_label_capD)
apply assumption
apply(simp add: cap_points_to_label_def)
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
apply(subgoal_tac "is_subject aag (fst slot')")
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(subgoal_tac "\<not> is_final_cap' cap s", blast)
apply(rule_tac slot=slot and slot'=slot' in not_is_final_cap)
apply assumption
apply assumption
apply(rule_tac s1=t in cte_wp_at_pspace'[THEN iffD1])
apply(rule sym)
apply(fastforce elim: is_subject_kheap_eq)
apply assumption
Genericise deletion actions that occur after empty_slot This patch adds a generic "post_cap_deletion" step that is called by finalise_slot. Previous to this, the only caps which had actions required at this stage were IRQHandlerCaps -- it was required that the IRQ bitmap be updated after the cap itself was removed (as the invariants state that for any existing IRQHandlerCap, the corresponding bit in the IRQ bitmap must be set). By genericising this, we add the capacity for new, arch-specific post cap deletion actions to occur in the future.
2018-02-07 04:08:43 +00:00
apply clarsimp
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(case_tac "\<exists> ref. ref \<in> Structures_A.obj_refs cap'")
apply(erule exE, frule caps_ref_either_an_object_or_irq)
apply(elim conjE)
apply(drule_tac x=ref in bspec, assumption)
apply(drule_tac s=t in intra_label_capD)
apply assumption
apply(simp add: cap_points_to_label_def)
apply(erule conjE, drule_tac x=ref in bspec)
apply(blast dest: caps_ref_single_objects)
apply fastforce
apply(subgoal_tac "\<exists> ref. ref \<in> cap_irqs cap'")
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
apply clarsimp
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(drule_tac x=ref in bspec, assumption)
apply(drule_tac s=t in intra_label_capD)
apply assumption
apply(simp add: cap_points_to_label_def)
apply(erule conjE, drule_tac x=ref in bspec)
apply(blast dest: caps_ref_single_irqs)
apply fastforce
apply blast
done
lemma is_final_cap_reads_respects:
Isabelle2018: new "op x" syntax; now is "(x)" (result of "isabelle update_op -m <dir>")
2018-06-09 08:30:53 +00:00
"reads_respects_f aag l (silc_inv aag st and ( \<lambda> s. cte_wp_at ((=) cap) slot s \<and>
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
is_subject aag (fst slot)))
(is_final_cap cap)"
Import release snapshot.
2014-07-14 19:32:44 +00:00
unfolding is_final_cap_def
apply(clarsimp simp: equiv_valid_def2 equiv_valid_2_def in_monad reads_equiv_f_def)
apply(frule (1) is_subject_kheap_eq)
Isabelle2018: new "op x" syntax; now is "(x)" (result of "isabelle update_op -m <dir>")
2018-06-09 08:30:53 +00:00
apply(cut_tac p="slot" and s=s and s'=t and P="(=) cap" in cte_wp_at_pspace', simp)
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(rule iffI)
apply(blast intro: is_final_cap_reads_respects_helper)
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
apply(rule_tac s=t and t=s in is_final_cap_reads_respects_helper,
Import release snapshot.
2014-07-14 19:32:44 +00:00
(simp add: silc_dom_equiv_def
|erule reads_equiv_sym
|erule affects_equiv_sym
|erule equiv_for_sym)+)
done
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
Import release snapshot.
2014-07-14 19:32:44 +00:00
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
definition ctes_wp_at
where
Import release snapshot.
2014-07-14 19:32:44 +00:00
"ctes_wp_at P s \<equiv> {ptr. cte_wp_at P ptr s}"
lemma slots_holding_overlapping_caps_def2:
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
"slots_holding_overlapping_caps cap s =
ctes_wp_at (\<lambda> c. (Structures_A.obj_refs cap \<inter> Structures_A.obj_refs c \<noteq> {}) \<or>
(cap_irqs cap \<inter> cap_irqs c \<noteq> {}) \<or>
(arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {})) s"
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(simp add: slots_holding_overlapping_caps_def ctes_wp_at_def cte_wp_at_def)
done
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
Import release snapshot.
2014-07-14 19:32:44 +00:00
lemma intra_label_cap_pres:
assumes cte: "\<And> P. \<lbrace>\<lambda> s. \<not> (cte_wp_at P slot s)\<rbrace> f \<lbrace>\<lambda> _ s. \<not> (cte_wp_at P slot s)\<rbrace>"
shows "\<lbrace>\<lambda> s. (intra_label_cap aag slot s) \<rbrace> f \<lbrace>\<lambda> _s. (intra_label_cap aag slot s) \<rbrace>"
apply(clarsimp simp: valid_def intra_label_cap_def)
apply(drule_tac x=cap in spec)
Isabelle2018: new "op x" syntax; now is "(x)" (result of "isabelle update_op -m <dir>")
2018-06-09 08:30:53 +00:00
apply(case_tac "cte_wp_at ((=) cap) slot s")
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply blast
apply(drule_tac use_valid[OF _ cte])
apply assumption
apply blast
done
lemma not_intra_label_cap_pres:
assumes cte: "\<And>P. \<lbrace>\<lambda> s. (cte_wp_at P slot s)\<rbrace> f \<lbrace>\<lambda> _ s. (cte_wp_at P slot s)\<rbrace>"
shows "\<lbrace>\<lambda> s. \<not> (intra_label_cap aag slot s) \<rbrace> f \<lbrace>\<lambda> _s. \<not> (intra_label_cap aag slot s) \<rbrace>"
apply(clarsimp simp: valid_def intra_label_cap_def)
apply(rule_tac x=cap in exI)
apply(drule_tac use_valid[OF _ cte], assumption)
apply blast
done
lemma cte_wp_at_pres_from_kheap':
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
assumes l:
"\<And> ptr P.
\<lbrace> R and (\<lambda> s. P (kheap s ptr)) and K (pasObjectAbs aag ptr = l)\<rbrace>
f
\<lbrace>\<lambda> _ s. P (kheap s ptr)\<rbrace>"
shows
"\<lbrace>(\<lambda> s. Q (cte_wp_at P slot s)) and R and K (pasObjectAbs aag (fst slot) = l)\<rbrace>
f
\<lbrace>( \<lambda> _ s. Q (cte_wp_at P slot s))\<rbrace>"
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(rule hoare_gen_asm)
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
apply(simp add: valid_def | intro allI impI ballI)+
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(rename_tac x, case_tac x, simp, rename_tac rv s')
apply(subgoal_tac "\<exists> x. kheap s (fst slot) = x")
apply(erule exE, rename_tac x)
apply(drule use_valid)
apply(rule_tac ptr="fst slot" and P="\<lambda> y. y = x" in l)
apply simp
apply(drule trans, erule sym)
apply(drule_tac P=P in cte_wp_at_pspace')
apply simp
apply blast
done
lemmas cte_wp_at_pres_from_kheap = cte_wp_at_pres_from_kheap'[where R="\<top>", simplified]
lemma hoare_contrapositive:
"\<lbrakk>\<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>; \<not> Q r s'; (r, s') \<in> fst (f s)\<rbrakk> \<Longrightarrow>
\<not> P s"
apply(case_tac "P s")
apply(blast dest: use_valid)
apply assumption
done
lemma allI': "\<forall>x y. P x y \<Longrightarrow> \<forall> y x. P x y"
by simp
lemma silc_inv_pres:
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
assumes l:
"\<And> ptr P.
\<lbrace> silc_inv aag st and (\<lambda> s. P (kheap s ptr)) and K (pasObjectAbs aag ptr = SilcLabel)\<rbrace>
f
\<lbrace>\<lambda> _ s. P (kheap s ptr)\<rbrace>"
Import release snapshot.
2014-07-14 19:32:44 +00:00
assumes c: "\<And>P. \<lbrace>\<lambda>s. P (cdt s) \<rbrace> f \<lbrace>\<lambda> _ s. P (cdt s)\<rbrace>"
assumes ncte: "\<And> P slot. \<lbrace> \<lambda> s. \<not> (cte_wp_at P slot s) \<rbrace> f \<lbrace> \<lambda> _ s. \<not> (cte_wp_at P slot s) \<rbrace>"
shows
"\<lbrace> silc_inv aag st \<rbrace> f \<lbrace> \<lambda>_. silc_inv aag st\<rbrace>"
apply(clarsimp simp: valid_def silc_inv_def)
apply(clarsimp simp: slots_holding_overlapping_caps_def2 ctes_wp_at_def)
apply(rule conjI)
apply(intro allI impI)
apply(frule_tac x=x in spec, erule (1) impE)
apply(erule exE, rename_tac sz, rule_tac x=sz in exI)
apply(simp add: obj_at_def)
apply(elim exE conjE, rename_tac ko)
apply(rule_tac x=ko in exI, simp)
apply(erule use_valid[OF _ l])
apply simp
apply(clarsimp simp: silc_inv_def obj_at_def slots_holding_overlapping_caps_def2 ctes_wp_at_def)
apply(rule conjI)
apply clarsimp
apply(frule_tac x=aa in spec, drule_tac x=ba in spec, drule_tac x=cap in spec)
Isabelle2018: new "op x" syntax; now is "(x)" (result of "isabelle update_op -m <dir>")
2018-06-09 08:30:53 +00:00
apply(subgoal_tac "cte_wp_at ((=) cap) (aa, ba) s \<and> \<not> intra_label_cap aag (aa,ba) s")
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(erule (1) impE)
apply (elim exE conjE)+
apply (rule_tac x=ab in exI, rule conjI, rule_tac x=bb in exI)
apply (erule use_valid[OF _ cte_wp_at_pres_from_kheap'[where R="silc_inv aag st"]])
apply(rule l)
apply simp
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
apply(clarsimp simp: silc_inv_def tcb_at_typ obj_at_def
slots_holding_overlapping_caps_def2 ctes_wp_at_def)
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply assumption
apply(rule conjI)
apply(erule (1) hoare_contrapositive[OF ncte, simplified])
apply(rule hoare_contrapositive[OF intra_label_cap_pres, simplified, OF ncte], assumption+)
apply (rule conjI)
apply (erule use_valid[OF _ c])
apply simp
apply(simp add: silc_dom_equiv_def)
apply(rule equiv_forI)
apply(erule use_valid[OF _ l])
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
apply(fastforce simp: silc_inv_def obj_at_def slots_holding_overlapping_caps_def2
ctes_wp_at_def silc_dom_equiv_def
elim: equiv_forE)
Import release snapshot.
2014-07-14 19:32:44 +00:00
done
(* if we don't touch any caps or modify any object-types, then
silc_inv is preserved *)
lemma silc_inv_triv:
assumes kheap: "\<And> P x. \<lbrace>\<lambda> s. P (kheap s x) \<rbrace> f \<lbrace> \<lambda>_ s. P (kheap s x) \<rbrace>"
assumes c: "\<And>P. \<lbrace>\<lambda>s. P (cdt s) \<rbrace> f \<lbrace>\<lambda> _ s. P (cdt s)\<rbrace>"
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
assumes cte: "\<And> Q P slot. \<lbrace>\<lambda> s. Q (cte_wp_at P slot s)\<rbrace> f \<lbrace>\<lambda> _ s. Q (cte_wp_at P slot s)\<rbrace>"
Import release snapshot.
2014-07-14 19:32:44 +00:00
assumes typ_at: "\<And> P T p. \<lbrace> \<lambda> s. P (typ_at T p s) \<rbrace> f \<lbrace> \<lambda> _ s. P (typ_at T p s) \<rbrace>"
shows
"\<lbrace> silc_inv aag st \<rbrace> f \<lbrace> \<lambda>_. silc_inv aag st \<rbrace>"
apply(clarsimp simp: valid_def silc_inv_def)
apply(rule conjI)
apply(intro allI impI)
apply(erule use_valid)
apply(rule hoare_vcg_ex_lift)
apply(rule cap_table_at_lift_valid[OF typ_at])
apply blast
apply(rule conjI)
apply(clarsimp simp: slots_holding_overlapping_caps_def2 ctes_wp_at_def)
apply(drule_tac x=aa in spec, drule_tac x=ba in spec, drule_tac x=cap in spec)
Isabelle2018: new "op x" syntax; now is "(x)" (result of "isabelle update_op -m <dir>")
2018-06-09 08:30:53 +00:00
apply(subgoal_tac "cte_wp_at ((=) cap) (aa, ba) s \<and> \<not> intra_label_cap aag (aa,ba) s")
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(elim exE conjE | simp)+
apply (rule_tac x=ab in exI, rule conjI, rule_tac x=bb in exI)
apply (erule (1) use_valid[OF _ cte])
apply(assumption)
apply(rule conjI)
Isabelle2018: new "op x" syntax; now is "(x)" (result of "isabelle update_op -m <dir>")
2018-06-09 08:30:53 +00:00
apply(case_tac "cte_wp_at ((=) cap) (aa, ba) s")
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply assumption
apply(drule use_valid[OF _ cte[where Q="\<lambda> x. \<not> x"]])
apply assumption
apply blast
apply(case_tac "intra_label_cap aag (aa, ba) s")
apply(drule_tac use_valid[OF _ intra_label_cap_pres[OF cte]])
apply assumption
apply blast
apply assumption
apply(simp add: silc_dom_equiv_def)
apply (rule conjI)
apply (erule use_valid[OF _ c])
apply simp
apply(rule equiv_forI)
apply(erule use_valid[OF _ kheap])
apply(fastforce elim: equiv_forE)
done
lemma set_object_wp:
"\<lbrace> \<lambda> s. P (s\<lparr>kheap := kheap s(ptr \<mapsto> obj)\<rparr>) \<rbrace>
set_object ptr obj
\<lbrace> \<lambda>_. P \<rbrace>"
unfolding set_object_def
apply (wp)
done
lemma set_cap_well_formed_cnode_helper:
"\<lbrakk>well_formed_cnode_n x xa; xa (snd slot) = Some y\<rbrakk> \<Longrightarrow>
well_formed_cnode_n x
(\<lambda>a. if a = snd slot then Some cap else xa a)"
apply(simp add: well_formed_cnode_n_def)
apply(rule equalityI)
apply(drule equalityD1)
apply(fastforce dest: subsetD split: if_splits)
apply(drule equalityD2)
apply(fastforce dest: subsetD split: if_splits)
done
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
Import release snapshot.
2014-07-14 19:32:44 +00:00
lemma set_cap_slots_holding_overlapping_caps_helper:
"\<lbrakk>x \<in> slots_holding_overlapping_caps cap s; fst x \<noteq> fst slot;
ko_at (TCB tcb) (fst slot) s;
Structures_A.obj_refs cap = {} \<longrightarrow> cap_irqs cap \<noteq> {};
tcb_cap_cases (snd slot) = Some (getF, setF, blah)\<rbrakk>
\<Longrightarrow> x \<in> slots_holding_overlapping_caps cap
(s\<lparr>kheap := kheap s(fst slot \<mapsto>
TCB (setF (\<lambda> x. capa) tcb))\<rparr>)"
apply(clarsimp simp: slots_holding_overlapping_caps_def)
apply(rule_tac x=cap' in exI)
apply(clarsimp simp: get_cap_cte_wp_at')
apply(erule (1) upd_other_cte_wp_at)
done
lemma set_cap_slots_holding_overlapping_caps_other:
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
"\<lbrace> \<lambda> s. x \<in> slots_holding_overlapping_caps capa s \<and>
pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag (fst slot) \<rbrace>
Import release snapshot.
2014-07-14 19:32:44 +00:00
set_cap cap slot
\<lbrace> \<lambda> rv s. x \<in> slots_holding_overlapping_caps capa s \<rbrace>"
unfolding set_cap_def
wp: update the proofs for the new wp/wpc/wpsimp
2017-03-13 16:37:32 +00:00
apply (wpsimp wp: set_object_wp get_object_wp)+
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(case_tac "Structures_A.obj_refs capa = {} \<and> cap_irqs capa = {}")
apply(clarsimp simp: slots_holding_overlapping_caps_def)
apply(subgoal_tac "fst x \<noteq> fst slot")
apply(intro allI impI conjI)
apply(clarsimp simp: slots_holding_overlapping_caps_def)
apply(rule_tac x=cap' in exI)
apply clarsimp
apply(subst get_cap_cte_wp_at')
apply(rule upd_other_cte_wp_at)
apply(simp add: cte_wp_at_def)
apply assumption
wp: update the proofs for the new wp/wpc/wpsimp
2017-03-13 16:37:32 +00:00
apply((drule set_cap_slots_holding_overlapping_caps_helper[where slot=slot], simp+)+)[5]
apply clarsimp
Import release snapshot.
2014-07-14 19:32:44 +00:00
done
lemma set_cap_cte_wp_at_triv:
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
"\<lbrace>\<top>\<rbrace> set_cap cap slot
Isabelle2018: new "op x" syntax; now is "(x)" (result of "isabelle update_op -m <dir>")
2018-06-09 08:30:53 +00:00
\<lbrace>\<lambda>_. cte_wp_at ((=) cap) slot\<rbrace>"
Import release snapshot.
2014-07-14 19:32:44 +00:00
unfolding set_cap_def
wp: update the proofs for the new wp/wpc/wpsimp
2017-03-13 16:37:32 +00:00
apply (wpsimp wp: set_object_wp get_object_wp)
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(intro impI conjI allI)
apply(rule cte_wp_at_cteI)
apply fastforce
apply clarsimp
wp: update the proofs for the new wp/wpc/wpsimp
2017-03-13 16:37:32 +00:00
apply(drule set_cap_well_formed_cnode_helper[where slot=slot], simp+)
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(fastforce intro: cte_wp_at_tcbI simp: tcb_cap_cases_def)+
done
lemma set_cap_neg_cte_wp_at_other_helper':
"\<lbrakk>oslot \<noteq> slot;
ko_at (TCB x) (fst oslot) s;
tcb_cap_cases (snd oslot) = Some (ogetF, osetF, orestr);
kheap
(s\<lparr>kheap := kheap s(fst oslot \<mapsto>
TCB (osetF (\<lambda> x. cap) x))\<rparr>)
(fst slot) =
Some (TCB tcb);
tcb_cap_cases (snd slot) = Some (getF, setF, restr);
P (getF tcb)\<rbrakk> \<Longrightarrow>
cte_wp_at P slot s"
apply(case_tac "fst oslot = fst slot")
apply(rule cte_wp_at_tcbI)
apply(fastforce split: if_splits simp: obj_at_def)
apply assumption
apply(fastforce split: if_splits simp: tcb_cap_cases_def dest: prod_eqI)
apply(rule cte_wp_at_tcbI)
apply(fastforce split: if_splits simp: obj_at_def)
apply assumption
apply assumption
done
lemma set_cap_neg_cte_wp_at_other_helper:
"\<lbrakk>\<not> cte_wp_at P slot s; oslot \<noteq> slot; ko_at (TCB x) (fst oslot) s;
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
tcb_cap_cases (snd oslot) = Some (getF, setF, restr)\<rbrakk> \<Longrightarrow>
Import release snapshot.
2014-07-14 19:32:44 +00:00
\<not> cte_wp_at P slot (s\<lparr>kheap := kheap s(fst oslot \<mapsto> TCB (setF (\<lambda> x. cap) x))\<rparr>)"
apply(rule notI)
apply(erule cte_wp_atE)
apply(fastforce elim: notE intro: cte_wp_at_cteI split: if_splits)
apply(fastforce elim: notE intro: set_cap_neg_cte_wp_at_other_helper')
done
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
Import release snapshot.
2014-07-14 19:32:44 +00:00
lemma set_cap_neg_cte_wp_at_other:
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
"oslot \<noteq> slot \<Longrightarrow>
\<lbrace>\<lambda>s. \<not> (cte_wp_at P slot s)\<rbrace>
set_cap cap oslot
\<lbrace>\<lambda>rv s. \<not> (cte_wp_at P slot s) \<rbrace>"
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(rule hoare_pre)
unfolding set_cap_def
apply(wp set_object_wp get_object_wp | wpc | simp add: split_def)+
apply(intro allI impI conjI)
apply(rule notI)
apply(erule cte_wp_atE)
apply (fastforce split: if_splits dest: prod_eqI elim: notE intro: cte_wp_at_cteI simp: obj_at_def)
apply(fastforce split: if_splits elim: notE intro: cte_wp_at_tcbI)
apply(auto dest: set_cap_neg_cte_wp_at_other_helper)
done
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
Import release snapshot.
2014-07-14 19:32:44 +00:00
lemma set_cap_silc_inv:
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
"\<lbrace>(\<lambda>s. \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow>
(\<exists> lslot. lslot \<in> slots_holding_overlapping_caps cap s \<and>
pasObjectAbs aag (fst lslot) = SilcLabel))
and silc_inv aag st and K (pasObjectAbs aag (fst slot) \<noteq> SilcLabel)\<rbrace>
set_cap cap slot
\<lbrace>\<lambda>rv. silc_inv aag st\<rbrace>"
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(rule hoare_gen_asm)
apply(clarsimp simp: valid_def silc_inv_def)
apply(intro conjI impI allI)
apply(erule use_valid)
apply(rule hoare_vcg_ex_lift)
apply(rule cap_table_at_lift_valid[OF set_cap_typ_at])
apply blast
apply(case_tac "slot = (a,ba)")
apply(subgoal_tac "cap = capa")
apply (simp)
apply(erule impE)
apply(simp add: intra_label_cap_def)
apply(elim conjE exE)
apply(blast dest: cte_wp_at_eqD2)
apply(elim exE conjE)
apply(rule_tac x=aa in exI, simp)
apply(rule_tac x=bb in exI)
apply(erule use_valid[OF _ set_cap_slots_holding_overlapping_caps_other[where aag=aag]])
apply fastforce
apply(rule cte_wp_at_eqD2)
apply blast
apply(drule_tac s=slot in sym, simp)
apply(erule use_valid[OF _ set_cap_cte_wp_at_triv], rule TrueI)
apply(drule_tac x=a in spec, drule_tac x=ba in spec, drule_tac x= capa in spec)
apply(erule impE, rule conjI)
apply(fastforce elim!: hoare_contrapositive[OF set_cap_neg_cte_wp_at_other, simplified])
apply(rule_tac P="\<lambda> s. intra_label_cap aag (a, ba) s" in hoare_contrapositive)
apply(rule intra_label_cap_pres)
apply(erule set_cap_neg_cte_wp_at_other)
apply(erule conjE, assumption)
apply assumption
apply clarsimp
apply(rule_tac x=aa in exI, simp)
apply(rule_tac x=bb in exI)
apply(erule use_valid[OF _ set_cap_slots_holding_overlapping_caps_other[where aag=aag]])
apply fastforce
Proof update for crunch changes
2018-03-14 00:48:48 +00:00
apply (erule use_valid[OF _ set_cap_rvk_cdt_ct_ms(4)],simp)
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(simp add: silc_dom_equiv_def)
apply(rule equiv_forI)
apply(erule use_valid)
unfolding set_cap_def
apply(wp set_object_wp get_object_wp static_imp_wp | simp add: split_def | wpc)+
apply clarsimp
apply(rule conjI)
apply fastforce
apply (fastforce elim: equiv_forE)
done
lemma weak_derived_overlaps':
"\<lbrakk>weak_derived cap cap';
Structures_A.obj_refs cap \<noteq> {} \<or> cap_irqs cap \<noteq> {}\<rbrakk> \<Longrightarrow>
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
Structures_A.obj_refs cap \<inter> Structures_A.obj_refs cap' \<noteq> {} \<or>
Import release snapshot.
2014-07-14 19:32:44 +00:00
cap_irqs cap \<inter> cap_irqs cap' \<noteq> {}"
apply(simp add: weak_derived_def)
apply(erule disjE)
prefer 2
apply simp
Isabelle2016-1: update references to renamed constants and facts
2016-10-25 06:01:30 +00:00
apply(simp add: copy_of_def split: if_split_asm add: same_object_as_def split: cap.splits)
infoflow: 2015 update (apart from C refinement)
2015-05-16 08:14:59 +00:00
apply((case_tac cap; simp)+)[5]
arch_split: Access and InfoFlow now build
2016-01-25 07:40:30 +00:00
subgoal for arch1 arch2 by (cases arch1; cases arch2; simp)
Import release snapshot.
2014-07-14 19:32:44 +00:00
done
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
Import release snapshot.
2014-07-14 19:32:44 +00:00
lemma weak_derived_overlaps:
"\<lbrakk>cte_wp_at (weak_derived cap) slot s;
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
Structures_A.obj_refs cap \<noteq> {} \<or> cap_irqs cap \<noteq> {}\<rbrakk> \<Longrightarrow>
Import release snapshot.
2014-07-14 19:32:44 +00:00
slot \<in> slots_holding_overlapping_caps cap s"
apply(simp add: slots_holding_overlapping_caps_def get_cap_cte_wp_at')
apply(drule cte_wp_at_eqD)
apply(erule exE, rename_tac cap')
apply(rule_tac x=cap' in exI)
apply(blast dest: weak_derived_overlaps')
done
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
Import release snapshot.
2014-07-14 19:32:44 +00:00
lemma not_cap_points_to_label_transfers_across_overlapping_caps:
"\<lbrakk>\<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot));
slot \<in> slots_holding_overlapping_caps cap s\<rbrakk>
\<Longrightarrow> \<not> intra_label_cap aag slot s"
apply(simp add: slots_holding_overlapping_caps_def get_cap_cte_wp_at')
apply(elim exE conjE, rename_tac cap')
apply(simp add: intra_label_cap_def)
apply(rule_tac x=cap' in exI)
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
apply(auto simp: cap_points_to_label_def
dest: caps_ref_single_objects caps_ref_single_irqs caps_ref_either_an_object_or_irq)
Import release snapshot.
2014-07-14 19:32:44 +00:00
done
lemma overlapping_transfers_across_overlapping_caps:
"\<lbrakk>slot \<in> FinalCaps.slots_holding_overlapping_caps cap s;
Isabelle2018: new "op x" syntax; now is "(x)" (result of "isabelle update_op -m <dir>")
2018-06-09 08:30:53 +00:00
cte_wp_at ((=) cap') slot s;
Import release snapshot.
2014-07-14 19:32:44 +00:00
lslot \<in> FinalCaps.slots_holding_overlapping_caps cap' s\<rbrakk> \<Longrightarrow>
lslot \<in> FinalCaps.slots_holding_overlapping_caps cap s"
apply(simp add: slots_holding_overlapping_caps_def get_cap_cte_wp_at')
apply(elim exE conjE)
apply(drule (1) cte_wp_at_eqD2)+
apply clarsimp
apply(rename_tac lcap)
apply(rule_tac x=lcap in exI)
apply(auto dest: caps_ref_single_objects caps_ref_single_irqs caps_ref_either_an_object_or_irq)
done
lemma slots_holding_overlapping_caps_hold_caps:
"slot \<in> slots_holding_overlapping_caps cap s \<Longrightarrow>
Isabelle2018: new "op x" syntax; now is "(x)" (result of "isabelle update_op -m <dir>")
2018-06-09 08:30:53 +00:00
\<exists> cap'. cte_wp_at ((=) cap') slot s"
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(fastforce simp: slots_holding_overlapping_caps_def get_cap_cte_wp_at')
done
lemma overlapping_slots_have_labelled_overlapping_caps:
"\<lbrakk>slot \<in> slots_holding_overlapping_caps cap s; silc_inv aag st s;
\<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot))\<rbrakk> \<Longrightarrow>
(\<exists> lslot. lslot \<in> slots_holding_overlapping_caps cap s \<and>
pasObjectAbs aag (fst lslot) = SilcLabel)"
apply(drule not_cap_points_to_label_transfers_across_overlapping_caps)
apply assumption
apply(frule slots_holding_overlapping_caps_hold_caps)
apply(erule exE, rename_tac cap')
apply(drule silc_invD)
apply assumption
apply assumption
apply(blast dest: overlapping_transfers_across_overlapping_caps)
done
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
Import release snapshot.
2014-07-14 19:32:44 +00:00
crunch silc_inv[wp]: set_original "silc_inv aag st"
(wp: silc_inv_triv)
lemma nonempty_refs:
"\<not> cap_points_to_label aag cap l \<Longrightarrow> Structures_A.obj_refs cap \<noteq> {} \<or> cap_irqs cap \<noteq> {}"
apply(simp add: cap_points_to_label_def)
apply auto
done
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
lemma set_cdt_silc_inv:
"\<lbrace>silc_inv aag st and K(all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) m)\<rbrace>
set_cdt m
\<lbrace>\<lambda>_. silc_inv aag st\<rbrace>"
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply (simp add: set_cdt_def)
apply wp
apply (simp add: silc_inv_def intra_label_cap_def slots_holding_overlapping_caps_def silc_dom_equiv_def equiv_for_def)
done
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
lemma update_cdt_silc_inv:
"\<lbrace>silc_inv aag st and (\<lambda>s. all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (f (cdt s)))\<rbrace>
update_cdt f
\<lbrace>\<lambda>_. silc_inv aag st\<rbrace>"
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply (simp add: update_cdt_def)
apply (wp set_cdt_silc_inv | simp)+
done
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
lemma silc_inv_all_children:
"silc_inv aag st s \<Longrightarrow> all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s)"
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply (simp add: silc_inv_def)
done
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
Import release snapshot.
2014-07-14 19:32:44 +00:00
lemma cap_swap_silc_inv:
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
"\<lbrace>silc_inv aag st and cte_wp_at (weak_derived cap) slot and
cte_wp_at (weak_derived cap') slot' and
K(pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot') \<and>
pasObjectAbs aag (fst slot') \<noteq> SilcLabel)\<rbrace>
cap_swap cap slot cap' slot'
\<lbrace>\<lambda>_. silc_inv aag st\<rbrace>"
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(rule hoare_gen_asm)
unfolding cap_swap_def
apply(rule hoare_pre)
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
apply (wp set_cap_silc_inv hoare_vcg_ex_lift static_imp_wp
set_cap_slots_holding_overlapping_caps_other[where aag=aag] set_cdt_silc_inv
| simp split del: if_split)+
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(rule conjI)
apply(rule impI, elim conjE)
apply(drule weak_derived_overlaps)
apply(erule nonempty_refs)
apply(drule overlapping_slots_have_labelled_overlapping_caps)
apply assumption
apply simp
apply fastforce
apply (rule conjI)
apply(rule impI, elim conjE)
apply(drule weak_derived_overlaps, erule nonempty_refs)
apply(drule overlapping_slots_have_labelled_overlapping_caps)
apply assumption
apply simp
apply fastforce
apply (elim conjE)
apply (drule silc_inv_all_children)
apply simp
apply (intro impI conjI)
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
apply (fastforce simp: all_children_def simp del: split_paired_All
| simp add: all_children_def del: split_paired_All)+ (*slow*)
Import release snapshot.
2014-07-14 19:32:44 +00:00
done
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
Import release snapshot.
2014-07-14 19:32:44 +00:00
lemma cap_move_silc_inv:
"\<lbrace> silc_inv aag st and cte_wp_at (weak_derived cap) slot and
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
K(pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot') \<and>
pasObjectAbs aag (fst slot') \<noteq> SilcLabel) \<rbrace>
cap_move cap slot slot'
Import release snapshot.
2014-07-14 19:32:44 +00:00
\<lbrace> \<lambda>_. silc_inv aag st \<rbrace>"
apply(rule hoare_gen_asm)
unfolding cap_move_def
apply(rule hoare_pre)
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
apply (wp set_cap_silc_inv hoare_vcg_ex_lift
set_cap_slots_holding_overlapping_caps_other[where aag=aag]
set_cdt_silc_inv static_imp_wp
| simp)+
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(rule conjI)
apply(fastforce simp: cap_points_to_label_def)
apply (rule conjI)
apply(rule impI, elim conjE)
apply(drule weak_derived_overlaps)
apply(erule nonempty_refs)
apply(drule overlapping_slots_have_labelled_overlapping_caps)
apply assumption
apply simp
apply fastforce
apply (elim conjE)
apply (drule silc_inv_all_children)
apply (fastforce simp: all_children_def simp del: split_paired_All)
done
lemma cap_irqs_max_free_index_update[simp]:
"cap_irqs (max_free_index_update cap) = cap_irqs cap"
apply(case_tac cap, simp_all add: free_index_update_def)
done
lemma cap_points_to_label_max_free_index_update[simp]:
"cap_points_to_label aag (max_free_index_update cap) l = cap_points_to_label aag cap l"
apply(simp add: cap_points_to_label_def)
done
lemma slots_holding_overlapping_caps_max_free_index_update[simp]:
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
"slots_holding_overlapping_caps (max_free_index_update cap) s =
slots_holding_overlapping_caps cap s"
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(simp add: slots_holding_overlapping_caps_def)
done
crunch silc_inv': set_untyped_cap_as_full "silc_inv aag st"
(wp: set_cap_silc_inv)
lemmas set_untyped_cap_as_full_silc_inv[wp] = set_untyped_cap_as_full_silc_inv'[simplified]
lemma set_untyped_cap_as_full_slots_holding_overlapping_caps_other:
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
"\<lbrace> \<lambda> s. x \<in> slots_holding_overlapping_caps capa s \<and>
pasObjectAbs aag (fst x) \<noteq> pasObjectAbs aag (fst slot) \<rbrace>
Import release snapshot.
2014-07-14 19:32:44 +00:00
set_untyped_cap_as_full src_cap cap slot
\<lbrace> \<lambda> rv s. x \<in> slots_holding_overlapping_caps capa s \<rbrace>"
unfolding set_untyped_cap_as_full_def
apply(rule hoare_pre)
apply(wp set_cap_slots_holding_overlapping_caps_other[where aag=aag])
apply clarsimp
done
lemma is_derived_overlaps':
"\<lbrakk>is_derived (cdt s) slot cap cap';
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
(Structures_A.obj_refs cap' \<noteq> {} \<or> cap_irqs cap' \<noteq> {}) \<or>
Import release snapshot.
2014-07-14 19:32:44 +00:00
(Structures_A.obj_refs cap \<noteq> {} \<or> cap_irqs cap \<noteq> {})\<rbrakk> \<Longrightarrow>
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
Structures_A.obj_refs cap \<inter> Structures_A.obj_refs cap' \<noteq> {} \<or>
Import release snapshot.
2014-07-14 19:32:44 +00:00
cap_irqs cap \<inter> cap_irqs cap' \<noteq> {}"
apply(simp add: is_derived_def)
apply(case_tac cap', simp_all add: cap_master_cap_def split: cap.splits arch_cap.splits)
done
lemma is_derived_overlaps:
"\<lbrakk>cte_wp_at (is_derived (cdt s) slot cap) slot s;
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
Structures_A.obj_refs cap \<noteq> {} \<or> cap_irqs cap \<noteq> {}\<rbrakk> \<Longrightarrow>
Import release snapshot.
2014-07-14 19:32:44 +00:00
slot \<in> slots_holding_overlapping_caps cap s"
apply(simp add: slots_holding_overlapping_caps_def get_cap_cte_wp_at')
apply(drule cte_wp_at_eqD)
apply(erule exE, rename_tac cap')
apply(rule_tac x=cap' in exI)
apply(blast dest: is_derived_overlaps')
done
lemma is_derived_overlaps2:
Isabelle2018: new "op x" syntax; now is "(x)" (result of "isabelle update_op -m <dir>")
2018-06-09 08:30:53 +00:00
"\<lbrakk>cte_wp_at ((=) cap') slot s;
Import release snapshot.
2014-07-14 19:32:44 +00:00
is_derived (cdt s) slot cap cap';
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
Structures_A.obj_refs cap' \<noteq> {} \<or> cap_irqs cap' \<noteq> {}\<rbrakk> \<Longrightarrow>
Import release snapshot.
2014-07-14 19:32:44 +00:00
slot \<in> slots_holding_overlapping_caps cap' s"
apply(simp add: slots_holding_overlapping_caps_def get_cap_cte_wp_at')
infoflow: 2015 update (apart from C refinement)
2015-05-16 08:14:59 +00:00
apply(blast dest: cte_wp_at_eqD is_derived_overlaps')
Import release snapshot.
2014-07-14 19:32:44 +00:00
done
lemma disj_dup: "A \<and> B \<and> C \<and> C'\<Longrightarrow> A \<and> B \<and> C \<and> A \<and> B \<and> C'"
apply simp
done
lemma cap_insert_silc_inv:
"\<lbrace> silc_inv aag st and (\<lambda>s. cte_wp_at (is_derived (cdt s) slot cap) slot s) and
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
K (pasObjectAbs aag (fst slot) = pasObjectAbs aag (fst slot') \<and>
pasObjectAbs aag (fst slot') \<noteq> SilcLabel) \<rbrace>
Import release snapshot.
2014-07-14 19:32:44 +00:00
cap_insert cap slot slot'
\<lbrace> \<lambda>_. silc_inv aag st \<rbrace>"
unfolding cap_insert_def
(* The order here matters. The first two need to be first. *)
apply (wp assert_wp static_imp_conj_wp set_cap_silc_inv hoare_vcg_ex_lift
set_untyped_cap_as_full_slots_holding_overlapping_caps_other[where aag=aag]
get_cap_wp update_cdt_silc_inv | simp | wp_once hoare_drop_imps)+
apply clarsimp
apply (rule disj_dup)
apply(rule conjI)
apply(rule impI)
apply(drule is_derived_overlaps)
apply(erule nonempty_refs)
apply(drule overlapping_slots_have_labelled_overlapping_caps)
apply assumption
apply simp
apply fastforce
apply (rule conjI)
apply(rule impI)
apply(drule cte_wp_at_eqD)
apply(elim conjE exE)
apply(drule (1) cte_wp_at_eqD2)
apply simp
apply(drule_tac cap'=capa in is_derived_overlaps2)
apply assumption
apply(erule nonempty_refs)
apply(drule overlapping_slots_have_labelled_overlapping_caps)
apply assumption
apply simp
apply fastforce
apply (drule silc_inv_all_children)
apply (rule conjI)
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
apply (fastforce simp: all_children_def simp del: split_paired_All)+
Import release snapshot.
2014-07-14 19:32:44 +00:00
done
lemma cte_wp_at_eq:
Isabelle2018: new "op x" syntax; now is "(x)" (result of "isabelle update_op -m <dir>")
2018-06-09 08:30:53 +00:00
assumes a: "\<And> cap. \<lbrace> cte_wp_at ((=) cap) slot \<rbrace> f \<lbrace> \<lambda>_. cte_wp_at ((=) cap) slot \<rbrace>"
Import release snapshot.
2014-07-14 19:32:44 +00:00
shows "\<lbrace> cte_wp_at P slot \<rbrace> f \<lbrace> \<lambda>_. cte_wp_at P slot \<rbrace>"
apply(clarsimp simp: valid_def)
apply(drule cte_wp_at_eqD)
apply(elim exE conjE, rename_tac cap)
apply(drule use_valid)
apply(rule a)
apply assumption
apply(simp add: cte_wp_at_def)
done
arm: update for simple_ko getter/setter
2017-11-27 04:59:58 +00:00
lemma set_simple_ko_silc_inv[wp]:
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
"\<lbrace> silc_inv aag st \<rbrace>
arm: update for simple_ko getter/setter
2017-11-27 04:59:58 +00:00
set_simple_ko f ptr ep
Import release snapshot.
2014-07-14 19:32:44 +00:00
\<lbrace> \<lambda> _. silc_inv aag st \<rbrace>"
arm: update for simple_ko getter/setter
2017-11-27 04:59:58 +00:00
unfolding set_simple_ko_def
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(rule silc_inv_pres)
apply(wp set_object_wp get_object_wp)
apply (simp split: kernel_object.splits)
apply(rule impI | simp)+
apply(fastforce simp: silc_inv_def obj_at_def is_cap_table_def)
apply(wp set_object_wp get_object_wp | simp)+
apply(case_tac "ptr = fst slot")
arm: update for simple_ko getter/setter
2017-11-27 04:59:58 +00:00
apply(clarsimp simp: a_type_def partial_inv_def split: kernel_object.splits)
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(fastforce elim: cte_wp_atE simp: obj_at_def)
apply(fastforce elim: cte_wp_atE intro: cte_wp_at_cteI cte_wp_at_tcbI)
done
crunch kheap[wp]: deleted_irq_handler "\<lambda>s. P (kheap s x)"
crunch silc_inv[wp]: deleted_irq_handler "silc_inv aag st"
(wp: silc_inv_triv)
arch_split: InfoFlow checking
2016-04-24 05:44:40 +00:00
end
Import release snapshot.
2014-07-14 19:32:44 +00:00
lemma (in is_extended') not_cte_wp_at[wp]: "I (\<lambda>s. \<not> cte_wp_at P t s)" by (rule lift_inv,simp)
arch_split: requalify abstract theories
2016-04-27 06:48:03 +00:00
context begin interpretation Arch . (*FIXME: arch_split*)
arch_split: InfoFlow checking
2016-04-24 05:44:40 +00:00
Import release snapshot.
2014-07-14 19:32:44 +00:00
lemma set_thread_state_silc_inv[wp]:
"\<lbrace>silc_inv aag st\<rbrace>
set_thread_state tptr ts
\<lbrace>\<lambda>_. silc_inv aag st\<rbrace>"
unfolding set_thread_state_def
apply(rule silc_inv_pres)
Isabelle2016-1: update references to renamed constants and facts
2016-10-25 06:01:30 +00:00
apply(wp set_object_wp|simp split del: if_split)+
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply (simp split: kernel_object.splits)
apply(rule impI | simp)+
apply(fastforce simp: silc_inv_def dest: get_tcb_SomeD simp: obj_at_def is_cap_table_def)
apply(wp set_object_wp | simp)+
apply(case_tac "tptr = fst slot")
apply(clarsimp split: kernel_object.splits)
apply(erule notE)
apply(erule cte_wp_atE)
apply(fastforce simp: obj_at_def)
apply(drule get_tcb_SomeD)
apply(rule cte_wp_at_tcbI)
apply(simp)
apply assumption
apply (fastforce simp: tcb_cap_cases_def split: if_splits)
apply(fastforce elim: cte_wp_atE intro: cte_wp_at_cteI cte_wp_at_tcbI)
done
add arch_tcb object to C, rename aep -> ntfn
2015-11-02 00:00:32 +00:00
lemma set_bound_notification_silc_inv[wp]:
history squashed patch for aep-binding
2015-09-02 05:43:39 +00:00
"\<lbrace>silc_inv aag st\<rbrace>
add arch_tcb object to C, rename aep -> ntfn
2015-11-02 00:00:32 +00:00
set_bound_notification tptr ntfn
history squashed patch for aep-binding
2015-09-02 05:43:39 +00:00
\<lbrace>\<lambda>_. silc_inv aag st\<rbrace>"
add arch_tcb object to C, rename aep -> ntfn
2015-11-02 00:00:32 +00:00
unfolding set_bound_notification_def
history squashed patch for aep-binding
2015-09-02 05:43:39 +00:00
apply(rule silc_inv_pres)
Isabelle2016-1: update references to renamed constants and facts
2016-10-25 06:01:30 +00:00
apply(wp set_object_wp|simp split del: if_split)+
history squashed patch for aep-binding
2015-09-02 05:43:39 +00:00
apply (simp split: kernel_object.splits)
apply(rule impI | simp)+
apply(fastforce simp: silc_inv_def dest: get_tcb_SomeD simp: obj_at_def is_cap_table_def)
apply(wp set_object_wp | simp)+
apply(case_tac "tptr = fst slot")
apply(clarsimp split: kernel_object.splits)
apply(erule notE)
apply(erule cte_wp_atE)
apply(fastforce simp: obj_at_def)
apply(drule get_tcb_SomeD)
apply(rule cte_wp_at_tcbI)
apply(simp)
apply assumption
apply (fastforce simp: tcb_cap_cases_def split: if_splits)
apply(fastforce elim: cte_wp_atE intro: cte_wp_at_cteI cte_wp_at_tcbI)
done
Import release snapshot.
2014-07-14 19:32:44 +00:00
add arch_tcb object to C, rename aep -> ntfn
2015-11-02 00:00:32 +00:00
crunch silc_inv[wp]: fast_finalise, unbind_notification "silc_inv aag st"
Import release snapshot.
2014-07-14 19:32:44 +00:00
(ignore: set_object wp: crunch_wps simp: crunch_simps)
lemma slots_holding_overlapping_caps_lift:
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
assumes a: "\<And> P Q slot. \<lbrace>\<lambda>s. Q (cte_wp_at P slot s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (cte_wp_at P slot s)\<rbrace>"
shows
"\<lbrace>\<lambda>s. P (slots_holding_overlapping_caps cap s)\<rbrace>
f
\<lbrace>\<lambda>_ s. P (slots_holding_overlapping_caps cap s)\<rbrace>"
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(clarsimp simp: valid_def)
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
apply(subgoal_tac "slots_holding_overlapping_caps cap b = slots_holding_overlapping_caps cap s",
simp)
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(clarsimp simp: slots_holding_overlapping_caps_def2 ctes_wp_at_def)
apply(rule Collect_cong)
apply(erule use_valid[OF _ a])
apply(rule refl)
done
crunch cte_wp_at'[wp]: set_original "\<lambda> s. Q (cte_wp_at P slot s)"
lemma slots_holding_overlapping_caps_exst_update[simp]:
"slots_holding_overlapping_caps cap (trans_state f s) =
slots_holding_overlapping_caps cap s"
apply(simp add: slots_holding_overlapping_caps_def2 ctes_wp_at_def)
done
crunch cte_wp_at'[wp]: set_cdt "\<lambda> s. Q (cte_wp_at P slot s)"
lemma slots_holding_overlapping_caps_is_original_cap_update[simp]:
"slots_holding_overlapping_caps cap (s\<lparr>is_original_cap := X\<rparr>) =
slots_holding_overlapping_caps cap s"
apply(simp add: slots_holding_overlapping_caps_def2 ctes_wp_at_def)
done
lemma intra_label_cap_is_original_cap[simp]:
"intra_label_cap aag slot (s\<lparr>is_original_cap := X\<rparr>) = intra_label_cap aag slot s"
apply(simp add: intra_label_cap_def)
done
lemma silc_inv_is_original_cap[simp]:
"silc_inv aag st (s\<lparr>is_original_cap := X\<rparr>) = silc_inv aag st s"
apply(simp add: silc_inv_def silc_dom_equiv_def equiv_for_def)
done
lemma empty_slot_silc_inv:
"\<lbrace>silc_inv aag st and K (pasObjectAbs aag (fst slot) \<noteq> SilcLabel)\<rbrace>
empty_slot slot free_irq
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
\<lbrace>\<lambda>_. silc_inv aag st\<rbrace>"
Import release snapshot.
2014-07-14 19:32:44 +00:00
unfolding empty_slot_def
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
apply(wp set_cap_silc_inv hoare_vcg_all_lift hoare_vcg_ex_lift
Import release snapshot.
2014-07-14 19:32:44 +00:00
slots_holding_overlapping_caps_lift get_cap_wp
Genericise deletion actions that occur after empty_slot This patch adds a generic "post_cap_deletion" step that is called by finalise_slot. Previous to this, the only caps which had actions required at this stage were IRQHandlerCaps -- it was required that the IRQ bitmap be updated after the cap itself was removed (as the invariants state that for any existing IRQHandlerCap, the corresponding bit in the IRQ bitmap must be set). By genericising this, we add the capacity for new, arch-specific post cap deletion actions to occur in the future.
2018-02-07 04:08:43 +00:00
set_cdt_silc_inv dxo_wp_weak hoare_drop_imps
Import release snapshot.
2014-07-14 19:32:44 +00:00
| wpc | simp del: empty_slot_extended.dxo_eq)+
apply(clarsimp simp: cap_points_to_label_def)
apply (drule silc_inv_all_children)
apply (fastforce simp: all_children_def simp del: split_paired_All)
done
lemma cap_delete_one_silc_inv:
"\<lbrace>silc_inv aag st and K (is_subject aag (fst slot)) \<rbrace>
cap_delete_one slot
\<lbrace>\<lambda>_. silc_inv aag st\<rbrace>"
unfolding cap_delete_one_def
apply (wp hoare_unless_wp empty_slot_silc_inv get_cap_wp | simp)+
apply (clarsimp simp: silc_inv_def)
done
SELFOUR-276: Finish proofs for maximum controlled priority (MCP) To finish the proof of refinement to C, the specification for checkPrio needed strengthening: the checkPrio spec now takes a machine word argument. In the spec, priorities are still stored as 8-bit quantities, however. Once the spec was strenthened, it was possible to remove some redundant checks and mask operations from the C code. A thread's maximum controlled priority (MCP) determines the maximum thread priority or MCP it can assign to another thread (or itself).
2016-10-04 00:58:33 +00:00
lemma thread_set_silc_inv:
assumes cap_inv: "\<And>tcb. \<forall>(getF, v) \<in> ran tcb_cap_cases. getF (f tcb) = getF tcb"
shows "\<lbrace>silc_inv aag st\<rbrace> thread_set f t \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>"
apply (rule silc_inv_pres)
apply (subst thread_set_def)
apply (wp set_object_wp)
apply (simp split: kernel_object.splits)
apply (rule impI | simp)+
apply (fastforce simp: silc_inv_def dest: get_tcb_SomeD simp: obj_at_def is_cap_table_def)
apply (rule thread_set_Pmdb)
apply (rule thread_set_cte_wp_at_trivial[OF cap_inv])
done
Import release snapshot.
2014-07-14 19:32:44 +00:00
lemma thread_set_tcb_fault_update_silc_inv[wp]:
"\<lbrace>silc_inv aag st\<rbrace>
thread_set (tcb_fault_update blah) t
\<lbrace>\<lambda>_. silc_inv aag st\<rbrace>"
SELFOUR-276: Finish proofs for maximum controlled priority (MCP) To finish the proof of refinement to C, the specification for checkPrio needed strengthening: the checkPrio spec now takes a machine word argument. In the spec, priorities are still stored as 8-bit quantities, however. Once the spec was strenthened, it was possible to remove some redundant checks and mask operations from the C code. A thread's maximum controlled priority (MCP) determines the maximum thread priority or MCP it can assign to another thread (or itself).
2016-10-04 00:58:33 +00:00
by (rule thread_set_silc_inv; simp add: tcb_cap_cases_def)
Import release snapshot.
2014-07-14 19:32:44 +00:00
add arch_tcb object to C, rename aep -> ntfn
2015-11-02 00:00:32 +00:00
lemma reply_cancel_ipc_silc_inv:
Import release snapshot.
2014-07-14 19:32:44 +00:00
"\<lbrace>silc_inv aag st and pas_refined aag and K (is_subject aag t) \<rbrace>
add arch_tcb object to C, rename aep -> ntfn
2015-11-02 00:00:32 +00:00
reply_cancel_ipc t
Import release snapshot.
2014-07-14 19:32:44 +00:00
\<lbrace>\<lambda>_. silc_inv aag st\<rbrace>"
wp_cleanup: update proofs for new wp behaviour The things that usually go wrong: - wp fall through: add +, e.g. apply (wp select_wp) -> apply (wp select_wp)+ - precondition: you can remove most hoare_pre, but wpc still needs it, and sometimes the wp instance relies on being able to fit a rule to the current non-schematic precondition. In that case, use "including no_pre" to switch off the automatic hoare_pre application. - very rarely there is a schematic postcondition that interferes with the new trivial cleanup rules, because the rest of the script assumes some specific state afterwards (shouldn't happen in a reasonable proof, but not all proofs are reasonable..). In that case, (wp_once ...)+ should emulate the old behaviour precisely.
2017-01-13 12:58:40 +00:00
unfolding reply_cancel_ipc_def including no_pre
apply ((wp cap_delete_one_silc_inv select_wp hoare_vcg_if_lift)+ | simp)+
Import release snapshot.
2014-07-14 19:32:44 +00:00
(* there must be a better way to do this... *)
apply (clarsimp simp: valid_def)
apply (rule conjI)
apply clarsimp
apply(rule conjI)
apply(erule use_valid)
apply wp
apply assumption
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
apply(subgoal_tac "descendants_of (t, tcb_cnode_index 2) (cdt b) =
descendants_of (t, tcb_cnode_index 2) (cdt s)")
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(drule descendants_of_owned)
apply fastforce
apply simp
apply simp
apply(erule use_valid[OF _ thread_set_Pmdb])
apply(rule refl)
apply(fastforce elim: use_valid[OF _ thread_set_tcb_fault_update_silc_inv])
done
add arch_tcb object to C, rename aep -> ntfn
2015-11-02 00:00:32 +00:00
crunch silc_inv[wp]: cancel_signal "silc_inv aag st"
Import release snapshot.
2014-07-14 19:32:44 +00:00
add arch_tcb object to C, rename aep -> ntfn
2015-11-02 00:00:32 +00:00
lemma cancel_ipc_silc_inv:
Import release snapshot.
2014-07-14 19:32:44 +00:00
"\<lbrace>silc_inv aag st and pas_refined aag and K (is_subject aag t) \<rbrace>
add arch_tcb object to C, rename aep -> ntfn
2015-11-02 00:00:32 +00:00
cancel_ipc t
Import release snapshot.
2014-07-14 19:32:44 +00:00
\<lbrace> \<lambda>_. silc_inv aag st \<rbrace>"
add arch_tcb object to C, rename aep -> ntfn
2015-11-02 00:00:32 +00:00
unfolding cancel_ipc_def
arm: update for simple_ko getter/setter
2017-11-27 04:59:58 +00:00
apply(wp get_simple_ko_wp reply_cancel_ipc_silc_inv get_thread_state_inv hoare_vcg_all_lift
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
| wpc
add arch_tcb object to C, rename aep -> ntfn
2015-11-02 00:00:32 +00:00
| simp(no_asm) add: blocked_cancel_ipc_def get_ep_queue_def
get_blocking_object_def
Import release snapshot.
2014-07-14 19:32:44 +00:00
| wp_once hoare_drop_imps)+
apply auto
done
add arch_tcb object to C, rename aep -> ntfn
2015-11-02 00:00:32 +00:00
lemma cancel_ipc_indirect_silc_inv:
history squashed patch for aep-binding
2015-09-02 05:43:39 +00:00
"\<lbrace>silc_inv aag st and st_tcb_at receive_blocked t \<rbrace>
add arch_tcb object to C, rename aep -> ntfn
2015-11-02 00:00:32 +00:00
cancel_ipc t
history squashed patch for aep-binding
2015-09-02 05:43:39 +00:00
\<lbrace>\<lambda>_. silc_inv aag st\<rbrace>"
add arch_tcb object to C, rename aep -> ntfn
2015-11-02 00:00:32 +00:00
unfolding cancel_ipc_def
history squashed patch for aep-binding
2015-09-02 05:43:39 +00:00
apply (rule hoare_seq_ext[OF _ gts_sp])
apply (rule hoare_name_pre_state)
apply (clarsimp simp: st_tcb_def2 receive_blocked_def)
add arch_tcb object to C, rename aep -> ntfn
2015-11-02 00:00:32 +00:00
apply (simp add: blocked_cancel_ipc_def split: thread_state.splits)
history squashed patch for aep-binding
2015-09-02 05:43:39 +00:00
apply (wp)
apply simp
done
Import release snapshot.
2014-07-14 19:32:44 +00:00
lemma intra_label_cap_machine_state[simp]:
"intra_label_cap aag slot (s\<lparr>machine_state := X\<rparr>) = intra_label_cap aag slot s"
apply(simp add: intra_label_cap_def)
done
lemma slots_holding_overlapping_caps_machine_state[simp]:
"slots_holding_overlapping_caps cap (s\<lparr>machine_state := X\<rparr>) = slots_holding_overlapping_caps cap s"
apply(simp add: slots_holding_overlapping_caps_def2 ctes_wp_at_def)
done
lemma silc_inv_machine_state[simp]:
"silc_inv aag st (s\<lparr>machine_state := X\<rparr>) = silc_inv aag st s"
apply(simp add: silc_inv_def silc_dom_equiv_def equiv_for_def)
done
lemma intra_label_cap_arch_state[simp]:
"intra_label_cap aag slot (s\<lparr>arch_state := X\<rparr>) = intra_label_cap aag slot s"
apply(simp add: intra_label_cap_def)
done
lemma slots_holding_overlapping_caps_arch_state[simp]:
"slots_holding_overlapping_caps cap (s\<lparr>arch_state := X\<rparr>) = slots_holding_overlapping_caps cap s"
apply(simp add: slots_holding_overlapping_caps_def2 ctes_wp_at_def)
done
lemma silc_inv_arch_state[simp]:
"silc_inv aag st (s\<lparr>arch_state := X\<rparr>) = silc_inv aag st s"
apply(simp add: silc_inv_def silc_dom_equiv_def equiv_for_def)
done
lemma set_pt_silc_inv[wp]:
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
"\<lbrace> silc_inv aag st \<rbrace>
Import release snapshot.
2014-07-14 19:32:44 +00:00
set_pt ptr pt
\<lbrace> \<lambda> _. silc_inv aag st \<rbrace>"
unfolding set_pt_def
apply(rule silc_inv_pres)
apply(wp set_object_wp get_object_wp)
apply (simp split: kernel_object.splits)
apply(rule impI | simp)+
apply(fastforce simp: silc_inv_def obj_at_def is_cap_table_def)
apply(wp set_object_wp get_object_wp | simp)+
apply(case_tac "ptr = fst slot")
apply(clarsimp split: kernel_object.splits)
apply(fastforce elim: cte_wp_atE simp: obj_at_def)
apply(fastforce elim: cte_wp_atE intro: cte_wp_at_cteI cte_wp_at_tcbI)
done
lemma set_pd_silc_inv[wp]:
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
"\<lbrace> silc_inv aag st \<rbrace>
Import release snapshot.
2014-07-14 19:32:44 +00:00
set_pd ptr pt
\<lbrace> \<lambda> _. silc_inv aag st \<rbrace>"
unfolding set_pd_def
apply(rule silc_inv_pres)
apply(wp set_object_wp get_object_wp)
apply (simp split: kernel_object.splits)
apply(rule impI | simp)+
apply(fastforce simp: silc_inv_def obj_at_def is_cap_table_def)
apply(wp set_object_wp get_object_wp | simp)+
apply(case_tac "ptr = fst slot")
apply(clarsimp split: kernel_object.splits)
apply(fastforce elim: cte_wp_atE simp: obj_at_def)
apply(fastforce elim: cte_wp_atE intro: cte_wp_at_cteI cte_wp_at_tcbI)
done
lemma set_asid_pool_silc_inv[wp]:
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
"\<lbrace> silc_inv aag st \<rbrace>
Import release snapshot.
2014-07-14 19:32:44 +00:00
set_asid_pool ptr pt
\<lbrace> \<lambda> _. silc_inv aag st \<rbrace>"
unfolding set_asid_pool_def
apply(rule silc_inv_pres)
apply(wp set_object_wp get_object_wp)
apply (simp split: kernel_object.splits)
apply(rule impI | simp)+
apply(fastforce simp: silc_inv_def obj_at_def is_cap_table_def)
apply(wp set_object_wp get_object_wp | simp)+
apply(case_tac "ptr = fst slot")
apply(clarsimp split: kernel_object.splits)
apply(fastforce elim: cte_wp_atE simp: obj_at_def)
apply(fastforce elim: cte_wp_atE intro: cte_wp_at_cteI cte_wp_at_tcbI)
done
Access and InfoFlow fix for prepare_thread_delete
2017-02-17 04:48:50 +00:00
crunch silc_inv[wp]: arch_finalise_cap,prepare_thread_delete "silc_inv aag st"
Import release snapshot.
2014-07-14 19:32:44 +00:00
(wp: crunch_wps modify_wp simp: crunch_simps ignore: set_object)
lemma finalise_cap_silc_inv:
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
"\<lbrace>silc_inv aag st and pas_refined aag and K (pas_cap_cur_auth aag cap)\<rbrace>
finalise_cap cap final
\<lbrace>\<lambda>_. silc_inv aag st\<rbrace>"
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(case_tac cap)
Isabelle2016-1: update references to renamed constants and facts
2016-10-25 06:01:30 +00:00
apply(wp cancel_ipc_silc_inv | simp split del: if_split add: suspend_def| clarsimp)+
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(clarsimp simp: aag_cap_auth_Thread)
Isabelle2016-1: update references to renamed constants and facts
2016-10-25 06:01:30 +00:00
apply(wp | simp split del: if_split | clarsimp split del: if_split)+
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(rule hoare_pre)
apply (wp cap_delete_one_silc_inv | simp add: deleting_irq_handler_def)+
apply (fastforce simp: aag_cap_auth_def cap_links_irq_def elim: aag_Control_into_owns_irq)
Isabelle2016-1: update references to renamed constants and facts
2016-10-25 06:01:30 +00:00
apply(wp | simp split del: if_split)+
Import release snapshot.
2014-07-14 19:32:44 +00:00
done
SELFOUR-553: rebase and fix styles and comments
2016-11-21 07:37:54 +00:00
Import release snapshot.
2014-07-14 19:32:44 +00:00
lemma validE_validE_R':
"\<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>,\<lbrace> R \<rbrace> \<Longrightarrow> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>,-"
apply(rule validE_validE_R)
apply(erule hoare_post_impErr)
by auto
lemma finalise_cap_ret_subset_cap_irqs:
"\<lbrace>\<lambda> s. (cap_irqs cap) = X\<rbrace> finalise_cap cap blah \<lbrace>\<lambda>rv s. (cap_irqs (fst rv)) \<subseteq> X\<rbrace>"
apply(case_tac cap)
Isabelle2016-1: update references to renamed constants and facts
2016-10-25 06:01:30 +00:00
apply(wp | simp add: o_def split del: if_split)+
apply(simp split: if_split)
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(wp | simp add: o_def | safe)+
apply(simp add: arch_finalise_cap_def)
apply(rule hoare_pre)
apply(wpc | wp | simp)+
done
lemma finalise_cap_ret_subset_obj_refs:
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
"\<lbrace>\<lambda>s. (Structures_A.obj_refs cap) = X\<rbrace>
finalise_cap cap blah
\<lbrace>\<lambda>rv s. (Structures_A.obj_refs (fst rv)) \<subseteq> X\<rbrace>"
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(case_tac cap)
Isabelle2016-1: update references to renamed constants and facts
2016-10-25 06:01:30 +00:00
apply(wp | simp add: o_def split del: if_split)+
apply(simp split: if_split)
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(wp | simp add: o_def | safe)+
apply(simp add: arch_finalise_cap_def)
apply(rule hoare_pre)
apply(wpc | wp | simp)+
done
lemma finalise_cap_ret_intra_label_cap:
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
"\<lbrace>\<lambda> s. cap_points_to_label aag cap l\<rbrace>
finalise_cap cap blah
\<lbrace>\<lambda>rv s. cap_points_to_label aag (fst rv) l\<rbrace>"
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(clarsimp simp: cap_points_to_label_def valid_def)
apply(rule conjI)
apply(erule ball_subset)
apply(drule use_valid[OF _ finalise_cap_ret_subset_obj_refs])
apply(rule refl)
apply simp
apply(erule ball_subset)
apply(drule use_valid[OF _ finalise_cap_ret_subset_cap_irqs])
apply(rule refl)
by simp
lemma silc_inv_preserves_silc_dom_caps:
"\<lbrakk>silc_inv aag st s; silc_inv aag st s';
pasObjectAbs aag (fst lslot) = SilcLabel;
lslot \<in> FinalCaps.slots_holding_overlapping_caps cap s\<rbrakk> \<Longrightarrow>
lslot \<in> FinalCaps.slots_holding_overlapping_caps cap s'"
apply(clarsimp simp: slots_holding_overlapping_caps_def get_cap_cte_wp_at')
apply(rule_tac x=cap' in exI)
apply simp
apply(subst (asm) cte_wp_at_pspace'[where s'=s'])
apply(fastforce simp: silc_inv_def silc_dom_equiv_def equiv_for_def)
apply assumption
done
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
Import release snapshot.
2014-07-14 19:32:44 +00:00
lemma finalise_cap_ret_is_silc:
Isabelle2018: new "op x" syntax; now is "(x)" (result of "isabelle update_op -m <dir>")
2018-06-09 08:30:53 +00:00
"\<lbrace>silc_inv aag st and cte_wp_at ((=) cap) slot and
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
pas_refined aag and K (pas_cap_cur_auth aag cap)\<rbrace>
finalise_cap cap blah
Import release snapshot.
2014-07-14 19:32:44 +00:00
\<lbrace>\<lambda>rvb s. (\<not> cap_points_to_label aag (fst rvb) (pasObjectAbs aag (fst slot)) \<longrightarrow>
(\<exists> lslot. lslot
\<in> FinalCaps.slots_holding_overlapping_caps (fst rvb) s \<and>
pasObjectAbs aag (fst lslot) = SilcLabel))\<rbrace>"
apply(clarsimp simp: valid_def)
apply(rename_tac a b s')
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
apply(cut_tac aag1=aag and r="(a,b)" and l1="pasObjectAbs aag (fst slot)"
in hoare_contrapositive[OF finalise_cap_ret_intra_label_cap])
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply simp
apply assumption
apply(frule use_valid[OF _ finalise_cap_silc_inv[where aag=aag and st=st]])
apply simp
apply(frule_tac s=s in silc_invD)
apply assumption
apply(fastforce simp: intra_label_cap_def)
apply(simp, elim exE conjE)
apply(rename_tac la lb)
apply(rule_tac x=la in exI, simp)
apply(rule_tac x=lb in exI)
apply(drule_tac lslot="(la,lb)" in silc_inv_preserves_silc_dom_caps, simp+)
apply(drule nonempty_refs)+
apply(erule disjE[where P="Structures_A.obj_refs cap \<noteq> {}"])
apply(subgoal_tac "cap_irqs cap = {} \<and> cap_irqs a = {}")
apply(clarsimp simp: slots_holding_overlapping_caps_def get_cap_cte_wp_at')
apply(rename_tac cap'a)
apply(rule_tac x=cap'a in exI)
apply simp
apply(subgoal_tac "\<exists> x. Structures_A.obj_refs cap = {x} \<and> Structures_A.obj_refs a = {x}")
apply blast
apply(erule nonemptyE)
apply(rename_tac x)
apply(rule_tac x=x in exI)
apply(subgoal_tac "Structures_A.obj_refs a \<subseteq> Structures_A.obj_refs cap")
apply(drule (1) subsetD)
apply(blast dest: caps_ref_single_objects)
apply(fastforce dest: use_valid[OF _ finalise_cap_ret_subset_obj_refs])
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
apply(fastforce dest: caps_ref_either_an_object_or_irq
use_valid[OF _ finalise_cap_ret_subset_cap_irqs])
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(subgoal_tac "Structures_A.obj_refs cap = {} \<and> Structures_A.obj_refs a = {}")
apply(clarsimp simp: slots_holding_overlapping_caps_def get_cap_cte_wp_at')
apply(rename_tac cap'a)
apply(rule_tac x=cap'a in exI)
apply simp
apply(subgoal_tac "\<exists> x. cap_irqs cap = {x} \<and> cap_irqs a = {x}")
apply blast
apply(erule nonemptyE)
apply(rename_tac x)
apply(rule_tac x=x in exI)
apply(subgoal_tac "cap_irqs a \<subseteq> cap_irqs cap")
apply(drule (1) subsetD)
apply(blast dest: caps_ref_single_irqs)
apply(fastforce dest: use_valid[OF _ finalise_cap_ret_subset_cap_irqs])
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
apply(fastforce dest: caps_ref_either_an_object_or_irq'
use_valid[OF _ finalise_cap_ret_subset_obj_refs])
Import release snapshot.
2014-07-14 19:32:44 +00:00
done
lemma arch_finalise_cap_ret:
Genericise deletion actions that occur after empty_slot This patch adds a generic "post_cap_deletion" step that is called by finalise_slot. Previous to this, the only caps which had actions required at this stage were IRQHandlerCaps -- it was required that the IRQ bitmap be updated after the cap itself was removed (as the invariants state that for any existing IRQHandlerCap, the corresponding bit in the IRQ bitmap must be set). By genericising this, we add the capacity for new, arch-specific post cap deletion actions to occur in the future.
2018-02-07 04:08:43 +00:00
"(rv, s') \<in> fst (arch_finalise_cap arch_cap final s) \<Longrightarrow> rv = (NullCap, NullCap)"
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(erule use_valid)
unfolding arch_finalise_cap_def
apply(wp | wpc | simp)+
done
lemma finalise_cap_ret:
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
"(rv, s') \<in> fst (finalise_cap cap final s)
\<Longrightarrow> case (fst rv) of NullCap \<Rightarrow> True | Zombie ptr bits n \<Rightarrow> True | _ \<Rightarrow> False"
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(case_tac cap, simp_all add: return_def)
Isabelle2016-1: update references to renamed constants and facts
2016-10-25 06:01:30 +00:00
apply(fastforce simp: liftM_def when_def bind_def return_def split: if_split_asm)+
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(drule arch_finalise_cap_ret)
apply(simp)
done
lemma finalise_cap_ret_is_subject:
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
"\<lbrace>K ((is_cnode_cap cap \<or> is_thread_cap cap \<or> is_zombie cap) \<longrightarrow> is_subject aag (obj_ref_of cap))\<rbrace>
finalise_cap cap is_final
\<lbrace>\<lambda>rv _. case (fst rv) of Zombie ptr bits n \<Rightarrow> is_subject aag (obj_ref_of (fst rv)) | _ \<Rightarrow> True\<rbrace>"
wp_cleanup: update proofs for new wp behaviour The things that usually go wrong: - wp fall through: add +, e.g. apply (wp select_wp) -> apply (wp select_wp)+ - precondition: you can remove most hoare_pre, but wpc still needs it, and sometimes the wp instance relies on being able to fit a rule to the current non-schematic precondition. In that case, use "including no_pre" to switch off the automatic hoare_pre application. - very rarely there is a schematic postcondition that interferes with the new trivial cleanup rules, because the rest of the script assumes some specific state afterwards (shouldn't happen in a reasonable proof, but not all proofs are reasonable..). In that case, (wp_once ...)+ should emulate the old behaviour precisely.
2017-01-13 12:58:40 +00:00
including no_pre
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(case_tac cap, simp_all add: is_zombie_def)
apply(wp | simp add: comp_def | rule impI | rule conjI)+
apply(fastforce simp: valid_def dest: arch_finalise_cap_ret)
done
lemma finalise_cap_ret_is_subject':
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
"\<lbrace>K(is_cnode_cap rv \<or> is_thread_cap rv \<or> is_zombie rv \<longrightarrow> is_subject aag (obj_ref_of rv))\<rbrace>
finalise_cap rv rva
\<lbrace>\<lambda>rv s. (is_zombie (fst rv) \<longrightarrow> is_subject aag (obj_ref_of (fst rv)))\<rbrace>"
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(clarsimp simp: valid_def)
apply(drule use_valid[OF _ finalise_cap_ret_is_subject[where aag=aag]])
apply simp
apply(case_tac a, simp_all add: is_zombie_def)
done
lemma get_cap_weak_derived[wp]:
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
"\<lbrace>\<top>\<rbrace>
get_cap slot
Import release snapshot.
2014-07-14 19:32:44 +00:00
\<lbrace>\<lambda>rv s. cte_wp_at (weak_derived rv) slot s\<rbrace>"
unfolding get_cap_def
apply(wp get_object_wp | simp add: split_def | wpc)+
apply safe
apply(rule cte_wp_at_cteI)
apply(fastforce simp: obj_at_def)
apply assumption
apply assumption
apply simp
apply(clarsimp simp: tcb_cnode_map_tcb_cap_cases)
apply(rule cte_wp_at_tcbI)
apply(fastforce simp: obj_at_def)
apply assumption
apply simp
done
crunch silc_inv: cap_swap_for_delete "silc_inv aag st"
(simp: crunch_simps)
lemma get_thread_cap_ret_is_subject:
"\<lbrace>(pas_refined aag) and K (is_subject aag (fst slot))\<rbrace>
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
get_cap slot
Import release snapshot.
2014-07-14 19:32:44 +00:00
\<lbrace>\<lambda>rv s. is_thread_cap rv \<longrightarrow> (is_subject aag (obj_ref_of rv))\<rbrace>"
apply(clarsimp simp: valid_def)
apply(frule get_cap_det)
apply(drule_tac f=fst in arg_cong)
apply(subst (asm) fst_conv)
apply(drule in_get_cap_cte_wp_at[THEN iffD1])
apply(clarsimp simp: cte_wp_at_caps_of_state)
apply(rule caps_of_state_pasObjectAbs_eq)
apply(blast intro: sym)
apply(fastforce simp: cap_auth_conferred_def split: cap.split)
apply assumption+
apply(case_tac a, simp_all)
done
lemma get_zombie_ret_is_subject:
"\<lbrace>(pas_refined aag) and K (is_subject aag (fst slot))\<rbrace>
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
get_cap slot
Import release snapshot.
2014-07-14 19:32:44 +00:00
\<lbrace>\<lambda>rv s. is_zombie rv \<longrightarrow> (is_subject aag (obj_ref_of rv))\<rbrace>"
apply(clarsimp simp: valid_def is_zombie_def)
apply(frule get_cap_det)
apply(drule_tac f=fst in arg_cong)
apply(subst (asm) fst_conv)
apply(drule in_get_cap_cte_wp_at[THEN iffD1])
apply(clarsimp simp: cte_wp_at_caps_of_state)
apply(rule caps_of_state_pasObjectAbs_eq)
apply(blast intro: sym)
apply(fastforce simp: cap_auth_conferred_def split: cap.split)
apply assumption+
apply(case_tac a, simp_all)
done
lemma ran_caps_of_state_cte_wp_at:
"(\<forall>cap\<in>ran (caps_of_state s). P cap) \<Longrightarrow>
Isabelle2018: new "op x" syntax; now is "(x)" (result of "isabelle update_op -m <dir>")
2018-06-09 08:30:53 +00:00
(\<forall>cap. cte_wp_at ((=) cap) slot s \<longrightarrow> P cap)"
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(simp add: cte_wp_at_caps_of_state)
apply(fastforce)
done
declare if_weak_cong[cong]
lemma rec_del_pas_refined:
notes drop_spec_valid[wp_split del] drop_spec_validE[wp_split del]
drop_spec_ev[wp_split del] rec_del.simps[simp del]
shows
"s \<turnstile> \<lbrace>pas_refined aag and K (case call of
CTEDeleteCall slot exposed \<Rightarrow> is_subject aag (fst slot) |
FinaliseSlotCall slot exposed \<Rightarrow> is_subject aag (fst slot) |
ReduceZombieCall cap slot exposed \<Rightarrow> is_subject aag (fst slot) \<and>
is_subject aag (obj_ref_of cap))\<rbrace>
rec_del call \<lbrace>K (pas_refined aag)\<rbrace>, \<lbrace>K (pas_refined aag)\<rbrace>"
proof (induct rule: rec_del.induct, simp_all only: rec_del_fails hoare_fail_any)
case (1 slot exposed s) show ?case
apply(simp add: split_def rec_del.simps)
apply(rule hoare_pre_spec_validE)
apply(wp)
apply(rule drop_spec_validE, wp)
apply(rule drop_spec_validE, wp)
apply(simp)
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
apply(rule_tac Q'="\<lambda>_ s. pas_refined aag s \<and> is_subject aag (fst slot)"
and E="\<lambda>_. pas_refined aag" in spec_strengthen_postE)
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(rule spec_valid_conj_liftE2)
apply(wp)
apply(rule "1.hyps"[simplified])
apply(simp)+
done
next
case (2 slot exposed s) show ?case
apply(simp add: rec_del.simps)
apply(rule hoare_pre_spec_validE)
apply(wp)
wp_cleanup: update proofs for new wp behaviour The things that usually go wrong: - wp fall through: add +, e.g. apply (wp select_wp) -> apply (wp select_wp)+ - precondition: you can remove most hoare_pre, but wpc still needs it, and sometimes the wp instance relies on being able to fit a rule to the current non-schematic precondition. In that case, use "including no_pre" to switch off the automatic hoare_pre application. - very rarely there is a schematic postcondition that interferes with the new trivial cleanup rules, because the rest of the script assumes some specific state afterwards (shouldn't happen in a reasonable proof, but not all proofs are reasonable..). In that case, (wp_once ...)+ should emulate the old behaviour precisely.
2017-01-13 12:58:40 +00:00
apply(rule drop_spec_validE, wp+)
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(simp add: split_def)
apply(rule conjI | rule impI)+
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
apply(rule_tac P="pas_refined aag and
K (is_subject aag (fst slot) \<and>
(is_zombie (fst rvb) \<longrightarrow> is_subject aag (obj_ref_of (fst rvb)) \<and>
aag_cap_auth aag (pasObjectAbs aag (fst slot)) (fst rvb)))"
in hoare_pre_spec_validE)
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(rule drop_spec_validE, wp)
apply(simp)
apply(wp | simp | rule impI | rule conjI)+
apply(rule drop_spec_validE, wp)
apply(rule drop_spec_validE, wp)
apply(clarsimp simp: is_zombie_def)
apply(simp)
apply(wp | simp | rule impI | rule conjI)+
apply(rule drop_spec_validE, wp)
apply(simp)
apply(rule impI, wp)
apply(rule "2.hyps"[simplified])
apply(simp)+
apply(rule drop_spec_validE, (wp preemption_point_inv'|simp)+)
apply(rule spec_valid_conj_liftE2)
apply(wp)
apply(rule "2.hyps"[simplified])
apply(simp)+
apply(wp drop_spec_validE | simp | clarsimp)+
apply(drule finalise_cap_ret)
apply(case_tac "fst (a,b)")
apply(simp add: is_zombie_def)+
apply(wp drop_spec_validE)
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
apply (rule_tac Q="\<lambda>rv s. pas_refined aag s \<and> is_subject aag (fst slot) \<and>
(case (fst rv) of Zombie ptr bits n \<Rightarrow>
is_subject aag (obj_ref_of (fst rv))
| _ \<Rightarrow> True) \<and>
pas_cap_cur_auth aag (fst rv) \<and>
(is_zombie (fst rv) \<or> fst rv = NullCap)"
in hoare_strengthen_post)
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(wp finalise_cap_ret_is_subject)
apply(wp finalise_cap_auth')
apply(simp add: valid_def)
apply(clarsimp)
apply(drule_tac rv="(a,b)" in finalise_cap_ret)
apply(clarsimp simp: is_zombie_def)
apply(case_tac a)
apply(clarsimp)+
apply(simp split: cap.splits)
apply(wp drop_spec_validE)
apply(simp)
apply(wp)
apply(simp)
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
apply(rule_tac Q'="\<lambda>rva s. pas_refined aag s \<and> pas_cap_cur_auth aag rv \<and>
is_subject aag (fst slot) \<and>
(is_cnode_cap rv \<longrightarrow> is_subject aag (obj_ref_of rv)) \<and>
(is_thread_cap rv \<longrightarrow> is_subject aag (obj_ref_of rv)) \<and>
(is_zombie rv \<longrightarrow> is_subject aag (obj_ref_of rv))"
in hoare_post_imp_R)
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(wp)
apply(simp)
apply(simp)
apply(wp drop_spec_validE hoare_drop_imps)
apply(rule_tac Q="\<lambda>s. pas_refined aag s \<and> is_subject aag (fst slot) \<and>
Isabelle2018: new "op x" syntax; now is "(x)" (result of "isabelle update_op -m <dir>")
2018-06-09 08:30:53 +00:00
(\<forall>cap. cte_wp_at ((=) cap) slot s \<longrightarrow> pas_cap_cur_auth aag cap)"
Import release snapshot.
2014-07-14 19:32:44 +00:00
in hoare_weaken_pre)
apply(rule hoare_conjI)
apply(rule hoare_weaken_pre, rule get_cap_wp, simp)
apply(wp get_cap_ret_is_subject get_thread_cap_ret_is_subject get_zombie_ret_is_subject)
apply(simp | clarsimp)+
apply(simp add: cte_wp_at_caps_of_state)
apply(frule cap_cur_auth_caps_of_state)
apply(simp)+
done
next
case (3 ptr bits n slot s) show ?case
apply(simp add: rec_del.simps)
Initial proof updates for combinator changes.
2018-03-15 03:45:48 +00:00
apply(wp drop_spec_validE)+
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(clarsimp)
done
next
case (4 ptr bits n slot s) show ?case
apply(simp add: rec_del.simps)
apply(wp)
apply(wp drop_spec_validE | simp)+
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
apply(rule_tac Q="\<lambda>rv s. pas_refined aag s \<and> is_subject aag (fst slot) \<and>
(ptr = obj_ref_of rv \<longrightarrow> is_zombie rv \<longrightarrow> is_subject aag (obj_ref_of rv)) \<and>
(rv = Zombie ptr bits (Suc n) \<longrightarrow> pas_cap_cur_auth aag rv)"
in hoare_strengthen_post)
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(rule_tac Q="\<lambda>s. pas_refined aag s \<and> is_subject aag (fst slot)" in hoare_weaken_pre)
apply(rule hoare_conjI, wp, simp)
apply(rule hoare_conjI, wp, simp)
apply(rule hoare_conjI)
apply(rule hoare_drop_imps)
apply(wp get_zombie_ret_is_subject)
apply(simp)
apply(rule hoare_weaken_pre)
apply(rule get_cap_wp)
apply(clarsimp)
apply(simp add: cte_wp_at_caps_of_state)
apply(frule cap_cur_auth_caps_of_state)
apply(simp)+
apply(clarsimp)
apply(simp add: aag_cap_auth_def)
apply(simp add: cap_auth_conferred_def)
apply(simp add: cap_links_asid_slot_def cap_links_irq_def)
apply(simp)
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
apply(rule_tac P'="\<lambda>s. (pas_refined aag s \<and> is_subject aag (fst slot) \<and> is_subject aag ptr) \<and>
pas_refined aag s \<and> is_subject aag (fst slot) \<and> is_subject aag ptr"
in hoare_pre_spec_validE)
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(rule spec_valid_conj_liftE2)
apply(wp, simp)
apply(rule hoare_pre_spec_validE)
apply(rule "4.hyps"[simplified])
apply(simp add: returnOk_def return_def)+
done
qed
lemma rec_del_pas_refined':
"\<lbrace>pas_refined aag and K (case call of
CTEDeleteCall slot exposed \<Rightarrow> is_subject aag (fst slot) |
FinaliseSlotCall slot exposed \<Rightarrow> is_subject aag (fst slot) |
ReduceZombieCall cap slot exposed \<Rightarrow> is_subject aag (fst slot) \<and>
is_subject aag (obj_ref_of cap))\<rbrace>
rec_del call \<lbrace>K (pas_refined aag)\<rbrace>, \<lbrace>K (pas_refined aag)\<rbrace>"
apply(rule use_spec)
apply(rule rec_del_pas_refined)
done
lemma finalise_cap_ret':
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
"\<lbrace>\<top>\<rbrace> finalise_cap cap final
Import release snapshot.
2014-07-14 19:32:44 +00:00
\<lbrace>\<lambda>rv s. (is_zombie (fst rv) \<or> fst rv = NullCap)\<rbrace>"
apply(auto simp: valid_def dest!: finalise_cap_ret split: cap.splits simp: is_zombie_def)
done
lemma silc_inv_irq_state_independent_A[simp, intro!]:
"irq_state_independent_A (silc_inv aag st)"
apply(simp add: silc_inv_def irq_state_independent_A_def silc_dom_equiv_def equiv_for_def)
done
lemma rec_del_silc_inv':
notes drop_spec_valid[wp_split del] drop_spec_validE[wp_split del]
drop_spec_ev[wp_split del] rec_del.simps[simp del]
shows
"s \<turnstile> \<lbrace> silc_inv aag st and pas_refined aag and K (case call of
CTEDeleteCall slot exposed \<Rightarrow> is_subject aag (fst slot) |
FinaliseSlotCall slot exposed \<Rightarrow> is_subject aag (fst slot) |
ReduceZombieCall cap slot exposed \<Rightarrow> is_subject aag (fst slot) \<and>
is_subject aag (obj_ref_of cap))\<rbrace>
(rec_del call)
\<lbrace>\<lambda>_. silc_inv aag st\<rbrace>,\<lbrace>\<lambda>_. silc_inv aag st\<rbrace>"
proof (induct s arbitrary: rule: rec_del.induct, simp_all only: rec_del_fails hoare_fail_any)
case (1 slot exposed s) show ?case
apply(simp add: split_def rec_del.simps)
apply(rule hoare_pre_spec_validE)
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
apply(wp empty_slot_silc_inv drop_spec_validE[OF returnOk_wp] drop_spec_validE[OF liftE_wp]
| simp)+
apply(rule_tac Q'="\<lambda>_ s. silc_inv aag st s \<and> is_subject aag (fst slot)"
and E="\<lambda>_. silc_inv aag st"
in spec_strengthen_postE)
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(rule spec_valid_conj_liftE2)
apply(wp)
apply(rule "1.hyps"[simplified])
apply(simp | fastforce simp: silc_inv_def)+
done
next
case (2 slot exposed s) show ?case
Isabelle2016-1: update references to renamed constants and facts
2016-10-25 06:01:30 +00:00
apply(simp add: rec_del.simps split del: if_split)
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(rule hoare_pre_spec_validE)
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
apply(wp drop_spec_validE[OF returnOk_wp] drop_spec_validE[OF liftE_wp] set_cap_silc_inv
Import release snapshot.
2014-07-14 19:32:44 +00:00
"2.hyps"
Isabelle2016-1: update references to renamed constants and facts
2016-10-25 06:01:30 +00:00
|simp add: split_def split del: if_split)+
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(rule drop_spec_validE, (wp preemption_point_inv'| simp)+)[1]
apply simp
apply(rule spec_valid_conj_liftE2)
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
apply(wp validE_validE_R'[OF rec_del_pas_refined'[simplified]] "2.hyps"
Import release snapshot.
2014-07-14 19:32:44 +00:00
drop_spec_validE[OF liftE_wp] set_cap_silc_inv
Isabelle2016-1: update references to renamed constants and facts
2016-10-25 06:01:30 +00:00
|simp add: without_preemption_def split del: if_split)+
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
Import release snapshot.
2014-07-14 19:32:44 +00:00
(* where the action is *)
fewer warnings
2015-05-16 09:52:49 +00:00
apply(simp cong: conj_cong add: conj_comms)
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(rule_tac Q="\<lambda> rvb s. pas_refined aag s \<and>
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
silc_inv aag st s \<and>
pasSubject aag \<noteq> SilcLabel \<and>
pas_cap_cur_auth aag (fst rvb) \<and>
is_subject aag (fst slot) \<and>
(is_zombie (fst rvb) \<or> fst rvb = NullCap) \<and>
(is_zombie (fst rvb) \<longrightarrow> is_subject aag (obj_ref_of (fst rvb))) \<and>
(\<not> cap_points_to_label aag (fst rvb) (pasObjectAbs aag (fst slot)) \<longrightarrow>
(\<exists>slot. slot \<in> FinalCaps.slots_holding_overlapping_caps (fst rvb) s
\<and> pasObjectAbs aag (fst slot) = SilcLabel))"
in hoare_strengthen_post)
Import release snapshot.
2014-07-14 19:32:44 +00:00
prefer 2
apply (fastforce)
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
apply(wp finalise_cap_pas_refined finalise_cap_silc_inv finalise_cap_auth' finalise_cap_ret'
finalise_cap_ret_is_subject' finalise_cap_ret_is_silc[where st=st])[1]
apply(wp drop_spec_validE[OF liftE_wp] get_cap_auth_wp[where aag=aag]
| simp add: without_preemption_def)+
fewer warnings
2015-05-16 09:52:49 +00:00
apply (clarsimp simp: conj_comms cong: conj_cong simp: caps_of_state_cteD)
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply (rule conjI, clarsimp simp: silc_inv_def)
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
apply(case_tac cap;
simp add: is_zombie_def aag_cap_auth_CNode aag_cap_auth_Thread aag_cap_auth_Zombie)
Import release snapshot.
2014-07-14 19:32:44 +00:00
done
next
case (3 ptr bits n slot s) show ?case
apply(simp add: rec_del.simps)
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
apply (wp drop_spec_validE[OF returnOk_wp] drop_spec_validE[OF liftE_wp]
cap_swap_for_delete_silc_inv)
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(simp add: pred_conj_def)
apply(rule hoare_pre_spec_validE)
apply(rule spec_valid_conj_liftE2)
apply (wp | simp)+
apply (wp drop_spec_validE[OF assertE_wp])
apply(fastforce simp: silc_inv_def)
done
next
case (4 ptr bits n slot s) show ?case
apply(simp add: rec_del.simps)
apply (wp drop_spec_validE[OF returnOk_wp] drop_spec_validE[OF liftE_wp] set_cap_silc_inv
drop_spec_validE[OF assertE_wp] get_cap_wp | simp add: without_preemption_def)+
apply (rule_tac Q'="\<lambda> _. silc_inv aag st and
K (pasObjectAbs aag (fst slot) \<noteq> SilcLabel)" in spec_strengthen_postE)
prefer 2
apply (clarsimp)
apply (drule silc_invD)
apply assumption
apply(simp add: intra_label_cap_def)
apply(rule exI)
apply(rule conjI)
apply assumption
apply(fastforce simp: cap_points_to_label_def)
apply(clarsimp simp: slots_holding_overlapping_caps_def2 ctes_wp_at_def)
apply (simp add: pred_conj_def)
apply (rule hoare_pre_spec_validE)
apply(wp spec_valid_conj_liftE2 "4.hyps")
apply(simp add: in_monad)
apply(fastforce simp: silc_inv_def)
done
qed
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
Import release snapshot.
2014-07-14 19:32:44 +00:00
lemma rec_del_silc_inv:
"\<lbrace> silc_inv aag st and pas_refined aag and K (case call of
CTEDeleteCall slot exposed \<Rightarrow> is_subject aag (fst slot) |
FinaliseSlotCall slot exposed \<Rightarrow> is_subject aag (fst slot) |
ReduceZombieCall cap slot exposed \<Rightarrow> is_subject aag (fst slot) \<and>
is_subject aag (obj_ref_of cap))\<rbrace>
(rec_del call)
\<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>"
apply(rule use_spec)
apply(rule rec_del_silc_inv')
done
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
Import release snapshot.
2014-07-14 19:32:44 +00:00
lemma cap_delete_silc_inv:
"\<lbrace> silc_inv aag st and pas_refined aag and K (is_subject aag (fst slot)) \<rbrace>
cap_delete slot
\<lbrace> \<lambda>_. silc_inv aag st \<rbrace>"
unfolding cap_delete_def
apply(wp rec_del_silc_inv | simp)+
done
crunch_ignore (valid) (add: getActiveIRQ)
crunch silc_inv[wp]: preemption_point "silc_inv aag st"
(ignore: wrap_ext_bool OR_choiceE simp: OR_choiceE_def crunch_simps wp: crunch_wps)
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
crunch tcb_domain_map_wellformed[wp]: update_work_units, reset_work_units
"tcb_domain_map_wellformed aag"
Import release snapshot.
2014-07-14 19:32:44 +00:00
crunch pas_refined[wp]: preemption_point "pas_refined aag"
(ignore: wrap_ext_bool OR_choiceE simp: OR_choiceE_def crunch_simps wp: crunch_wps)
lemma cap_revoke_silc_inv':
notes drop_spec_valid[wp_split del] drop_spec_validE[wp_split del]
drop_spec_ev[wp_split del] rec_del.simps[simp del]
shows
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
"s \<turnstile> \<lbrace> silc_inv aag st and pas_refined aag and einvs and simple_sched_action and
K (is_subject aag (fst slot)) \<rbrace>
cap_revoke slot
Import release snapshot.
2014-07-14 19:32:44 +00:00
\<lbrace> \<lambda>_. silc_inv aag st \<rbrace>, \<lbrace> \<lambda>_. silc_inv aag st \<rbrace>"
proof(induct rule: cap_revoke.induct[where ?a1.0=s])
case (1 slot s)
show ?case
apply(subst cap_revoke.simps)
apply(rule hoare_pre_spec_validE)
wp_cleanup: update proofs for new wp behaviour The things that usually go wrong: - wp fall through: add +, e.g. apply (wp select_wp) -> apply (wp select_wp)+ - precondition: you can remove most hoare_pre, but wpc still needs it, and sometimes the wp instance relies on being able to fit a rule to the current non-schematic precondition. In that case, use "including no_pre" to switch off the automatic hoare_pre application. - very rarely there is a schematic postcondition that interferes with the new trivial cleanup rules, because the rest of the script assumes some specific state afterwards (shouldn't happen in a reasonable proof, but not all proofs are reasonable..). In that case, (wp_once ...)+ should emulate the old behaviour precisely.
2017-01-13 12:58:40 +00:00
apply (wp "1.hyps")
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(wp spec_valid_conj_liftE2 | simp)+
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
apply(wp drop_spec_validE[OF valid_validE[OF preemption_point_silc_inv]]
cap_delete_silc_inv preemption_point_inv' | simp)+
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(rule spec_valid_conj_liftE1)
apply(rule validE_validE_R'[OF valid_validE[OF cap_delete_pas_refined]])
apply(rule spec_valid_conj_liftE1, (wp | simp)+)
apply(rule spec_valid_conj_liftE1, (wp | simp)+)
apply(rule spec_valid_conj_liftE1, (wp | simp)+)
apply(rule spec_valid_conj_liftE1, (wp | simp)+)
apply(rule spec_valid_conj_liftE1, (wp | simp)+)
apply(rule drop_spec_validE[OF valid_validE[OF cap_delete_silc_inv]])
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
apply (wp drop_spec_validE[OF assertE_wp] drop_spec_validE[OF without_preemption_wp]
get_cap_wp select_wp drop_spec_validE[OF returnOk_wp])+
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply clarsimp
fewer warnings
2015-05-16 09:52:49 +00:00
apply (clarsimp cong: conj_cong simp: conj_comms)
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply (subst conj_commute)
apply (rule conjI)
apply(fastforce dest: descendants_of_owned split: if_splits)
apply (case_tac "next_revoke_cap slot s")
apply (auto simp: emptyable_def dest!: reply_slot_not_descendant split: if_splits)
done
qed
lemma cap_revoke_silc_inv:
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
"\<lbrace> silc_inv aag st and pas_refined aag and einvs and simple_sched_action and
K (is_subject aag (fst slot)) \<rbrace>
cap_revoke slot
Import release snapshot.
2014-07-14 19:32:44 +00:00
\<lbrace> \<lambda>_. silc_inv aag st \<rbrace>, \<lbrace> \<lambda>_. silc_inv aag st \<rbrace>"
apply(rule use_spec)
apply(rule cap_revoke_silc_inv')
done
lemma thread_set_tcb_registers_caps_merge_default_tcb_silc_inv[wp]:
"\<lbrace>silc_inv aag st\<rbrace>
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
thread_set (tcb_registers_caps_merge default_tcb) word
Import release snapshot.
2014-07-14 19:32:44 +00:00
\<lbrace>\<lambda>xa. silc_inv aag st\<rbrace>"
SELFOUR-276: Finish proofs for maximum controlled priority (MCP) To finish the proof of refinement to C, the specification for checkPrio needed strengthening: the checkPrio spec now takes a machine word argument. In the spec, priorities are still stored as 8-bit quantities, however. Once the spec was strenthened, it was possible to remove some redundant checks and mask operations from the C code. A thread's maximum controlled priority (MCP) determines the maximum thread priority or MCP it can assign to another thread (or itself).
2016-10-04 00:58:33 +00:00
by (rule thread_set_silc_inv; simp add: tcb_cap_cases_def tcb_registers_caps_merge_def)
Import release snapshot.
2014-07-14 19:32:44 +00:00
SELFOUR-64: Remove general Recycle operation This removes the RecycleCap CNodeInvocation, whilst retaining recycle behaviour for Endpoints -- now renamed CNodeCancelBadgedSends.
2016-11-07 06:02:50 +00:00
crunch silc_inv[wp]: cancel_badged_sends "silc_inv aag st"
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
( wp: crunch_wps hoare_unless_wp simp: crunch_simps ignore: filterM set_object thread_set
simp: filterM_mapM)
Import release snapshot.
2014-07-14 19:32:44 +00:00
lemma finalise_slot_silc_inv:
"\<lbrace> silc_inv aag st and pas_refined aag and K (is_subject aag (fst slot))\<rbrace>
finalise_slot slot blah
\<lbrace> \<lambda>_. silc_inv aag st \<rbrace>"
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
unfolding finalise_slot_def
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(rule validE_valid)
apply(rule hoare_pre)
apply(rule rec_del_silc_inv)
apply simp
done
lemma invoke_cnode_silc_inv:
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
"\<lbrace> silc_inv aag st and einvs and simple_sched_action and pas_refined aag and
valid_cnode_inv i and authorised_cnode_inv aag i and is_subject aag \<circ> cur_thread \<rbrace>
invoke_cnode i
Import release snapshot.
2014-07-14 19:32:44 +00:00
\<lbrace> \<lambda>_. silc_inv aag st \<rbrace>"
unfolding invoke_cnode_def
apply(case_tac i)
apply(wp cap_insert_silc_inv | simp)+
apply(fastforce simp: silc_inv_def authorised_cnode_inv_def)
apply(wp cap_move_silc_inv | simp)+
apply(fastforce simp: silc_inv_def authorised_cnode_inv_def)
apply(wp cap_revoke_silc_inv | simp)+
apply(fastforce simp: authorised_cnode_inv_def)
apply(wp cap_delete_silc_inv | simp)+
apply(fastforce simp: authorised_cnode_inv_def)
apply(rule hoare_pre)
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
apply(wp cap_move_silc_inv cap_swap_silc_inv cap_move_cte_wp_at_other
| simp split del: if_split)+
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(fastforce simp: silc_inv_def authorised_cnode_inv_def)
apply(wp cap_move_silc_inv get_cap_wp | wpc | simp)+
apply(clarsimp simp: silc_inv_def authorised_cnode_inv_def)
apply(erule cte_wp_at_weak_derived_ReplyCap)
SELFOUR-64: Remove general Recycle operation This removes the RecycleCap CNodeInvocation, whilst retaining recycle behaviour for Endpoints -- now renamed CNodeCancelBadgedSends.
2016-11-07 06:02:50 +00:00
apply(wp cancel_badged_sends_silc_inv | simp | wpc | rule hoare_pre)+
Import release snapshot.
2014-07-14 19:32:44 +00:00
done
lemma set_cap_default_cap_silc_inv:
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
"\<lbrace>silc_inv aag st and K (is_subject aag (fst slot) \<and> is_subject aag oref)\<rbrace>
SELFOUR-421: infoflow and infoflow_c builds
2016-08-10 02:13:35 +00:00
set_cap (default_cap a oref b dev) slot
Import release snapshot.
2014-07-14 19:32:44 +00:00
\<lbrace>\<lambda>_. silc_inv aag st\<rbrace>"
apply(rule hoare_pre)
apply(rule set_cap_silc_inv)
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
apply (auto simp: cap_points_to_label_def
Import release snapshot.
2014-07-14 19:32:44 +00:00
dest: subsetD[OF obj_refs_default_cap] simp: default_cap_irqs silc_inv_def)
done
lemma create_cap_silc_inv:
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
"\<lbrace> silc_inv aag st and K (is_subject aag (fst (fst ref)) \<and> is_subject aag (snd ref) \<and>
is_subject aag (fst c))\<rbrace>
create_cap a b c dev ref
Import release snapshot.
2014-07-14 19:32:44 +00:00
\<lbrace> \<lambda>_. silc_inv aag st \<rbrace>"
unfolding create_cap_def
apply(rule hoare_gen_asm)
apply(wp set_cap_default_cap_silc_inv set_cdt_silc_inv | simp add: split_def)+
apply (subgoal_tac "pasObjectAbs aag (fst c) \<noteq> SilcLabel")
apply (drule silc_inv_all_children)
apply (simp add: all_children_def del: split_paired_All)
apply (clarsimp simp: silc_inv_def)
done
crunch silc_inv[wp]: init_arch_objects "silc_inv aag st"
SELFOUR-421: infoflow and infoflow_c builds
2016-08-10 02:13:35 +00:00
(wp: crunch_wps hoare_unless_wp simp: crunch_simps)
Import release snapshot.
2014-07-14 19:32:44 +00:00
lemma retype_region_silc_inv:
"\<lbrace>silc_inv aag st and K (range_cover ptr sz (obj_bits_api type o_bits) num_objects \<and>
(\<forall>x\<in>{ptr..(ptr && ~~ mask sz) + (2 ^ sz - 1)}. is_subject aag x)) \<rbrace>
SELFOUR-421: infoflow and infoflow_c builds
2016-08-10 02:13:35 +00:00
retype_region ptr num_objects o_bits type dev
Import release snapshot.
2014-07-14 19:32:44 +00:00
\<lbrace>\<lambda>_. silc_inv aag st \<rbrace>"
apply(rule hoare_gen_asm)+
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
apply(simp only: retype_region_def retype_addrs_def
Import release snapshot.
2014-07-14 19:32:44 +00:00
foldr_upd_app_if fun_app_def K_bind_def)
apply(wp modify_wp dxo_wp_weak | simp)+
apply (simp add: trans_state_update[symmetric] del: trans_state_update)
wp_cleanup: update proofs for new wp behaviour The things that usually go wrong: - wp fall through: add +, e.g. apply (wp select_wp) -> apply (wp select_wp)+ - precondition: you can remove most hoare_pre, but wpc still needs it, and sometimes the wp instance relies on being able to fit a rule to the current non-schematic precondition. In that case, use "including no_pre" to switch off the automatic hoare_pre application. - very rarely there is a schematic postcondition that interferes with the new trivial cleanup rules, because the rest of the script assumes some specific state afterwards (shouldn't happen in a reasonable proof, but not all proofs are reasonable..). In that case, (wp_once ...)+ should emulate the old behaviour precisely.
2017-01-13 12:58:40 +00:00
apply wp+
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply (clarsimp simp: not_less)
apply (clarsimp simp add: silc_inv_def)
apply (intro conjI impI allI)
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
apply (fastforce simp: obj_at_def silc_inv_def
dest: retype_addrs_subset_ptr_bits[simplified retype_addrs_def]
simp: image_def p_assoc_help power_sub)
Import release snapshot.
2014-07-14 19:32:44 +00:00
defer
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
apply (fastforce simp: silc_dom_equiv_def equiv_for_def silc_inv_def
dest: retype_addrs_subset_ptr_bits[simplified retype_addrs_def]
simp: image_def p_assoc_help power_sub)
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(case_tac "a \<in> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) `
{0..<num_objects}")
apply clarsimp
apply(subgoal_tac "cap = NullCap")
apply(clarsimp simp: intra_label_cap_def cap_points_to_label_def)
apply(drule (1) cte_wp_at_eqD2)
apply fastforce
apply(erule cte_wp_atE)
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
subgoal by (fastforce simp: default_object_def empty_cnode_def
split: apiobject_type.splits if_splits)
subgoal by (clarsimp simp: default_object_def default_tcb_def tcb_cap_cases_def
split: apiobject_type.splits if_splits)
Isabelle2018: new "op x" syntax; now is "(x)" (result of "isabelle update_op -m <dir>")
2018-06-09 08:30:53 +00:00
apply(subgoal_tac "cte_wp_at ((=) cap) (a,b) s \<and> \<not> intra_label_cap aag (a,b) s")
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(drule_tac x=a in spec, drule_tac x=b in spec, drule_tac x=cap in spec, simp)
apply(elim exE conjE, rename_tac la lb)
apply(rule_tac x=la in exI, simp, rule_tac x=lb in exI)
apply(simp add: slots_holding_overlapping_caps_def2 ctes_wp_at_def)
apply(subgoal_tac "la \<notin> (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) `
{0..<num_objects}")
apply(erule_tac t="(la,lb)" in cte_wp_atE)
apply(rule cte_wp_at_cteI)
apply fastforce
apply assumption
apply assumption
apply assumption
apply(rule cte_wp_at_tcbI)
apply fastforce
apply assumption
apply assumption
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
subgoal by (fastforce simp: silc_inv_def
dest: retype_addrs_subset_ptr_bits[simplified retype_addrs_def]
simp: image_def p_assoc_help power_sub)
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(rule conjI)
Merge branch 'master' into aep-merge This commit should at least remove merge conflict markers, and the idea is that at least refine, crefine, drefine, and infoflow (with sorrys) build. Subsequent commits may be required to fix build issues that I have not picked up.
2015-09-10 07:06:45 +00:00
subgoal by (fastforce elim: cte_wp_atE intro: cte_wp_at_cteI cte_wp_at_tcbI)
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(clarsimp simp: intra_label_cap_def cap_points_to_label_def)
apply(drule (1) cte_wp_at_eqD2)
apply(rule_tac x=capa in exI)
apply clarsimp
Merge branch 'master' into aep-merge This commit should at least remove merge conflict markers, and the idea is that at least refine, crefine, drefine, and infoflow (with sorrys) build. Subsequent commits may be required to fix build issues that I have not picked up.
2015-09-10 07:06:45 +00:00
by (fastforce elim: cte_wp_atE intro: cte_wp_at_cteI cte_wp_at_tcbI)
Import release snapshot.
2014-07-14 19:32:44 +00:00
lemma slots_holding_overlapping_caps_from_silc_inv:
assumes a: "\<lbrace> silc_inv aag st and P \<rbrace> f \<lbrace>\<lambda>_. silc_inv aag st \<rbrace>"
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
shows
"\<lbrace> silc_inv aag st and (\<lambda> s. slot \<in> (slots_holding_overlapping_caps cap s) \<and>
pasObjectAbs aag (fst slot) = SilcLabel) and P \<rbrace>
f
\<lbrace> \<lambda>_ s. slot \<in> (slots_holding_overlapping_caps cap s) \<rbrace>"
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(simp add: valid_def split_def | intro impI allI ballI | elim conjE)+
apply(simp add: slots_holding_overlapping_caps_def2 ctes_wp_at_def)
apply(erule subst[rotated], rule cte_wp_at_pspace')
apply(case_tac x, simp)
apply(drule use_valid[OF _ a])
apply simp
Merge branch 'master' into aep-merge This commit should at least remove merge conflict markers, and the idea is that at least refine, crefine, drefine, and infoflow (with sorrys) build. Subsequent commits may be required to fix build issues that I have not picked up.
2015-09-10 07:06:45 +00:00
by (fastforce simp: silc_inv_def silc_dom_equiv_def elim: equiv_forE)
Import release snapshot.
2014-07-14 19:32:44 +00:00
lemma slots_holding_overlapping_caps_eq:
assumes "Structures_A.obj_refs cap = Structures_A.obj_refs cap'"
assumes "cap_irqs cap = cap_irqs cap'"
shows
"slots_holding_overlapping_caps cap s = slots_holding_overlapping_caps cap' s"
using assms
apply(fastforce simp: slots_holding_overlapping_caps_def)
done
lemma detype_silc_inv:
"\<lbrace> silc_inv aag st and (K (\<forall>p\<in>S. is_subject aag p))\<rbrace>
modify (detype S)
\<lbrace>\<lambda>_. silc_inv aag st\<rbrace>"
apply(wp modify_wp)
apply(clarsimp simp: silc_inv_def)
apply(rule conjI, fastforce)
apply(rule conjI)
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
apply (clarsimp simp: slots_holding_overlapping_caps_def intra_label_cap_def
cap_points_to_label_def get_cap_cte_wp_at')
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(drule (1) cte_wp_at_eqD2)
apply clarsimp
apply(drule_tac x=a in spec, drule_tac x=b in spec, drule_tac x=cap in spec)
apply simp
apply(erule impE)
apply fastforce
apply(elim exE conjE, rename_tac la lb lcap)
apply(rule_tac x=la in exI, simp, rule_tac x=lb in exI, rule_tac x=lcap in exI)
apply simp
apply fastforce
apply(clarsimp simp: silc_dom_equiv_def equiv_for_def detype_def)
done
lemma delete_objects_silc_inv:
"\<lbrace> silc_inv aag st and (K (\<forall>p\<in>ptr_range ptr bits. is_subject aag p))\<rbrace>
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
delete_objects ptr bits
Import release snapshot.
2014-07-14 19:32:44 +00:00
\<lbrace>\<lambda>_. silc_inv aag st\<rbrace>"
apply(rule hoare_gen_asm)
unfolding delete_objects_def
apply (wp detype_silc_inv | simp add: ptr_range_def)+
done
SELFOUR-444: Finished InfoFlow and DRefine.
2016-05-26 07:51:53 +00:00
lemma set_cap_silc_inv_simple:
"\<lbrace> silc_inv aag st and cte_wp_at (\<lambda>cp. cap_irqs cp = cap_irqs cap
\<and> Structures_A.obj_refs cp = Structures_A.obj_refs cap) slot
and K (is_subject aag (fst slot))\<rbrace>
set_cap cap slot
\<lbrace>\<lambda>_. silc_inv aag st\<rbrace>"
apply (wp set_cap_silc_inv)
apply (clarsimp simp: cte_wp_at_caps_of_state)
apply (rule conjI; clarsimp)
apply (drule caps_of_state_cteD)
apply (frule(1) silc_invD)
apply (clarsimp simp: intra_label_cap_def)
apply (rule exI, rule conjI, assumption)
apply (simp add: cap_points_to_label_def)
apply (simp add: slots_holding_overlapping_caps_def)
apply (simp add: silc_inv_def)
done
lemma reset_untyped_cap_silc_inv:
"\<lbrace> silc_inv aag st and cte_wp_at is_untyped_cap slot
and invs and pas_refined aag
and (\<lambda>s. descendants_of slot (cdt s) = {})
and K (is_subject aag (fst slot))\<rbrace>
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
reset_untyped_cap slot
SELFOUR-444: Finished InfoFlow and DRefine.
2016-05-26 07:51:53 +00:00
\<lbrace>\<lambda>_. silc_inv aag st\<rbrace>"
apply (rule hoare_gen_asm)
SELFOUR-444: Avoid unnecessary cache clears. Adjust both specs and propagate the changes.
2016-06-05 13:06:26 +00:00
apply (simp add: reset_untyped_cap_def cong: if_cong)
apply (rule validE_valid, rule hoare_pre)
SELFOUR-444: Repair InfoFlow.
2016-10-17 13:56:47 +00:00
apply (wp set_cap_silc_inv_simple | simp add: unless_def)+
SELFOUR-444: Avoid unnecessary cache clears. Adjust both specs and propagate the changes.
2016-06-05 13:06:26 +00:00
apply (rule valid_validE, rule_tac Q="\<lambda>_. cte_wp_at is_untyped_cap slot
and silc_inv aag st" in hoare_strengthen_post)
apply (rule validE_valid, rule mapME_x_inv_wp, rule hoare_pre)
apply (wp mapME_x_inv_wp preemption_point_inv set_cap_cte_wp_at
set_cap_silc_inv_simple | simp)+
apply (clarsimp simp: cte_wp_at_caps_of_state is_cap_simps)
apply simp
apply (wp hoare_vcg_const_imp_lift delete_objects_silc_inv get_cap_wp
set_cap_silc_inv_simple
Many proof repairs.
2018-02-26 01:58:43 +00:00
| simp add: if_apply_def2)+
SELFOUR-444: Finished InfoFlow and DRefine.
2016-05-26 07:51:53 +00:00
apply (clarsimp simp: cte_wp_at_caps_of_state is_cap_simps bits_of_def)
apply (frule(1) cap_auth_caps_of_state)
apply (clarsimp simp: aag_cap_auth_def aag_has_Control_iff_owns
ptr_range_def[symmetric])
apply (frule if_unsafe_then_capD[OF caps_of_state_cteD], clarsimp+)
apply (drule ex_cte_cap_protects[OF _ _ _ _ order_refl], erule caps_of_state_cteD)
apply (clarsimp simp: descendants_range_def2 empty_descendants_range_in)
apply clarsimp+
done
lemma reset_untyped_cap_untyped_cap:
"\<lbrace>cte_wp_at (\<lambda>cp. is_untyped_cap cp \<and> P True (untyped_range cp)) slot
and invs
and (\<lambda>s. descendants_of slot (cdt s) = {})\<rbrace>
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
reset_untyped_cap slot
SELFOUR-444: Finished InfoFlow and DRefine.
2016-05-26 07:51:53 +00:00
\<lbrace>\<lambda>rv. cte_wp_at (\<lambda>cp. P (is_untyped_cap cp) (untyped_range cp)) slot\<rbrace>"
SELFOUR-444: Avoid unnecessary cache clears. Adjust both specs and propagate the changes.
2016-06-05 13:06:26 +00:00
apply (simp add: reset_untyped_cap_def cong: if_cong)
SELFOUR-444: Finished InfoFlow and DRefine.
2016-05-26 07:51:53 +00:00
apply (rule hoare_pre)
apply (wp set_cap_cte_wp_at | simp add: unless_def)+
apply (rule valid_validE, rule_tac Q="\<lambda>rv. cte_wp_at (\<lambda>cp. is_untyped_cap cp
\<and> is_untyped_cap cap
\<and> untyped_range cp = untyped_range cap
\<and> P True (untyped_range cp)) slot"
in hoare_strengthen_post)
apply (wp mapME_x_inv_wp preemption_point_inv set_cap_cte_wp_at
Many proof repairs.
2018-02-26 01:58:43 +00:00
| simp add: if_apply_def2
| clarsimp simp: cte_wp_at_caps_of_state is_cap_simps bits_of_def
SELFOUR-444: Finished InfoFlow and DRefine.
2016-05-26 07:51:53 +00:00
ptr_range_def[symmetric])+
apply (wp get_cap_wp)
apply (clarsimp simp: cte_wp_at_caps_of_state is_cap_simps ptr_range_def[symmetric])
apply (frule if_unsafe_then_capD[OF caps_of_state_cteD], clarsimp+)
apply (drule ex_cte_cap_protects[OF _ _ _ _ order_refl], erule caps_of_state_cteD)
apply (clarsimp simp: descendants_range_def2 empty_descendants_range_in)
apply clarsimp+
done
Import release snapshot.
2014-07-14 19:32:44 +00:00
lemma invoke_untyped_silc_inv:
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
"\<lbrace> silc_inv aag st and invs and pas_refined aag
SELFOUR-444: Finished InfoFlow and DRefine.
2016-05-26 07:51:53 +00:00
and ct_active and valid_untyped_inv ui
and K (authorised_untyped_inv aag ui)\<rbrace>
Import release snapshot.
2014-07-14 19:32:44 +00:00
invoke_untyped ui
\<lbrace> \<lambda>_. silc_inv aag st \<rbrace>"
apply(rule hoare_gen_asm)
SELFOUR-444: Finished InfoFlow and DRefine.
2016-05-26 07:51:53 +00:00
apply (rule hoare_pre)
apply (rule_tac Q="\<lambda>_. silc_inv aag st
and cte_wp_at (\<lambda>cp. is_untyped_cap cp \<longrightarrow> (\<forall>x \<in> untyped_range cp.
is_subject aag x)) (case ui of Invocations_A.Retype src_slot _ _ _ _ _ _ _ \<Rightarrow>
src_slot)" in hoare_strengthen_post)
apply (rule invoke_untyped_Q)
apply (rule hoare_pre, wp create_cap_silc_inv create_cap_pas_refined)
apply (clarsimp simp: authorised_untyped_inv_def)
apply (auto simp: cte_wp_at_caps_of_state)[1]
apply ((wp | simp)+)[1]
apply (rule hoare_pre)
apply (wp retype_region_silc_inv retype_cte_wp_at | simp)+
apply clarsimp
apply (strengthen range_cover_le[mk_strg I E])
apply (clarsimp simp: cte_wp_at_caps_of_state)
apply (simp add: invs_valid_pspace)
apply (erule ball_subset)
apply (simp add: word_and_le2 field_simps)
apply (rule hoare_pre)
apply (wp set_cap_silc_inv_simple set_cap_cte_wp_at)
apply (cases ui, clarsimp simp: cte_wp_at_caps_of_state is_cap_simps
Isabelle2016-1: update references to renamed constants and facts
2016-10-25 06:01:30 +00:00
split del: if_split cong: if_cong)
SELFOUR-444: Finished InfoFlow and DRefine.
2016-05-26 07:51:53 +00:00
apply (clarsimp simp: authorised_untyped_inv_def)
apply (wp reset_untyped_cap_silc_inv reset_untyped_cap_untyped_cap)
apply simp
apply (cases ui, clarsimp simp: cte_wp_at_caps_of_state
authorised_untyped_inv_def)
apply (frule(1) cap_auth_caps_of_state)
apply (clarsimp simp: aag_cap_auth_def aag_has_Control_iff_owns)
done
Import release snapshot.
2014-07-14 19:32:44 +00:00
lemma perform_page_table_invocation_silc_ionv_get_cap_helper:
"\<lbrace>silc_inv aag st and cte_wp_at (is_pt_cap or is_pg_cap) xa\<rbrace>
get_cap xa
\<lbrace>(\<lambda>capa s.
(\<not> cap_points_to_label aag
(ArchObjectCap $ update_map_data capa None)
(pasObjectAbs aag (fst xa)) \<longrightarrow>
(\<exists>lslot.
lslot
\<in> FinalCaps.slots_holding_overlapping_caps
(ArchObjectCap $ update_map_data capa None)
s \<and>
pasObjectAbs aag (fst lslot) = SilcLabel))) \<circ> the_arch_cap\<rbrace>"
apply(wp get_cap_wp)
apply clarsimp
apply(drule cte_wp_at_eqD)
apply(clarify)
apply(drule (1) cte_wp_at_eqD2)
apply(case_tac cap, simp_all add: is_pg_cap_def is_pt_cap_def)
apply(clarsimp simp: cap_points_to_label_def update_map_data_def split: arch_cap.splits)
apply(drule silc_invD)
apply assumption
apply(fastforce simp: intra_label_cap_def cap_points_to_label_def)
apply(fastforce simp: slots_holding_overlapping_caps_def2 ctes_wp_at_def)
apply(drule silc_invD)
apply assumption
apply(fastforce simp: intra_label_cap_def cap_points_to_label_def)
apply(fastforce simp: slots_holding_overlapping_caps_def2 ctes_wp_at_def)
done
lemmas perform_page_table_invocation_silc_inv_get_cap_helper' =
perform_page_table_invocation_silc_ionv_get_cap_helper
[simplified o_def fun_app_def]
lemma mapM_x_swp_store_pte_silc_inv[wp]:
"\<lbrace>silc_inv aag st\<rbrace> mapM_x (swp store_pte A) slots
\<lbrace>\<lambda>_. silc_inv aag st\<rbrace>"
apply(wp mapM_x_wp[OF _ subset_refl] | simp add: swp_def)+
done
lemma is_arch_diminished_pt_is_pt_or_pg_cap:
"cte_wp_at (is_arch_diminished (ArchObjectCap (PageTableCap xa xb))) slot s
\<Longrightarrow> cte_wp_at (\<lambda>a. is_pt_cap a \<or> is_pg_cap a) slot s"
apply(erule cte_wp_at_weakenE)
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
apply (clarsimp simp: is_arch_diminished_def diminished_def mask_cap_def cap_rights_update_def
split: cap.splits arch_cap.splits
simp: acap_rights_update_def acap_rights_def)
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(case_tac c, simp_all)[1]
infoflow: 2015 update (apart from C refinement)
2015-05-16 08:14:59 +00:00
apply(rename_tac arch_cap)
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(drule_tac x=arch_cap in spec)
apply(case_tac arch_cap, simp_all add: is_pt_cap_def)[1]
done
lemma is_arch_diminished_pg_is_pt_or_pg_cap:
SELFOUR-421: infoflow and infoflow_c builds
2016-08-10 02:13:35 +00:00
"cte_wp_at (is_arch_diminished (ArchObjectCap (PageCap dev x xa xb xc))) slot s
Import release snapshot.
2014-07-14 19:32:44 +00:00
\<Longrightarrow> cte_wp_at (\<lambda>a. is_pt_cap a \<or> is_pg_cap a) slot s"
apply(erule cte_wp_at_weakenE)
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
apply (clarsimp simp: is_arch_diminished_def diminished_def mask_cap_def cap_rights_update_def
split: cap.splits arch_cap.splits
simp: acap_rights_update_def acap_rights_def)
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(case_tac c, simp_all)[1]
infoflow: 2015 update (apart from C refinement)
2015-05-16 08:14:59 +00:00
apply(rename_tac arch_cap)
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(drule_tac x=arch_cap in spec)
apply(case_tac arch_cap, simp_all add: is_pg_cap_def)[1]
done
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
Import release snapshot.
2014-07-14 19:32:44 +00:00
lemma is_arch_update_overlaps:
"\<lbrakk>cte_wp_at (\<lambda>c. is_arch_update cap c) slot s;
\<not> cap_points_to_label aag cap l\<rbrakk>
\<Longrightarrow> slot \<in> slots_holding_overlapping_caps cap s"
apply(clarsimp simp: slots_holding_overlapping_caps_def2 ctes_wp_at_def)
apply(erule cte_wp_at_weakenE)
apply(clarsimp simp: is_arch_update_def)
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
apply(clarsimp simp: cap_master_cap_def split: cap.splits arch_cap.splits
simp: cap_points_to_label_def)
Import release snapshot.
2014-07-14 19:32:44 +00:00
done
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
Import release snapshot.
2014-07-14 19:32:44 +00:00
lemma perform_page_table_invocation_silc_inv:
"\<lbrace>silc_inv aag st and valid_pti blah and K (authorised_page_table_inv aag blah)\<rbrace>
perform_page_table_invocation blah
\<lbrace>\<lambda>_. silc_inv aag st\<rbrace>"
unfolding perform_page_table_invocation_def
apply(rule hoare_pre)
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
apply(wp set_cap_silc_inv
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
perform_page_table_invocation_silc_inv_get_cap_helper'[where st=st]
mapM_x_wp[OF _ subset_refl]
Import release snapshot.
2014-07-14 19:32:44 +00:00
| wpc | simp only: o_def fun_app_def K_def swp_def)+
apply clarsimp
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
apply(clarsimp simp: valid_pti_def authorised_page_table_inv_def
split: page_table_invocation.splits)
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(rule conjI)
apply(clarsimp)
defer
apply(fastforce simp: silc_inv_def)
apply(fastforce dest: is_arch_diminished_pt_is_pt_or_pg_cap simp: silc_inv_def)
apply(drule_tac slot="(aa,ba)" in overlapping_slots_have_labelled_overlapping_caps[rotated])
apply(fastforce)
apply(fastforce elim: is_arch_update_overlaps[rotated] cte_wp_at_weakenE)
apply fastforce
done
lemma perform_page_directory_invocation_silc_inv:
"\<lbrace>silc_inv aag st\<rbrace>
perform_page_directory_invocation blah
\<lbrace>\<lambda>_. silc_inv aag st\<rbrace>"
unfolding perform_page_directory_invocation_def
apply (cases blah)
apply (wp | simp)+
done
Updates for getpaddr system call (by Joel Beeren)
2014-07-18 15:21:34 +00:00
lemma as_user_silc_inv[wp]:
"\<lbrace>silc_inv aag st\<rbrace>
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
as_user t f
Updates for getpaddr system call (by Joel Beeren)
2014-07-18 15:21:34 +00:00
\<lbrace>\<lambda>_. silc_inv aag st\<rbrace>"
unfolding as_user_def
apply(rule silc_inv_pres)
apply(wp set_object_wp | simp add: split_def)+
apply (clarsimp)
apply(fastforce simp: silc_inv_def dest: get_tcb_SomeD simp: obj_at_def is_cap_table_def)
apply(wp set_object_wp | simp add: split_def)+
apply(case_tac "t = fst slot")
apply(clarsimp split: kernel_object.splits)
apply(erule notE)
apply(erule cte_wp_atE)
apply(fastforce simp: obj_at_def)
apply(drule get_tcb_SomeD)
apply(rule cte_wp_at_tcbI)
apply(simp)
apply assumption
apply (fastforce simp: tcb_cap_cases_def split: if_splits)
apply(fastforce elim: cte_wp_atE intro: cte_wp_at_cteI cte_wp_at_tcbI)
done
crunch silc_inv[wp]: store_word_offs "silc_inv aag st"
crunch kheap[wp]: store_word_offs "\<lambda> s. P (kheap s x)"
crunch cte_wp_at'[wp]: store_word_offs "\<lambda> s. Q (cte_wp_at P slot s)"
(wp: crunch_wps simp: crunch_simps)
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
Updates for getpaddr system call (by Joel Beeren)
2014-07-18 15:21:34 +00:00
lemma set_mrs_silc_inv[wp]:
"\<lbrace>silc_inv aag st\<rbrace>
set_mrs a b c
\<lbrace>\<lambda>_. silc_inv aag st\<rbrace>"
unfolding set_mrs_def
apply(rule silc_inv_pres)
Isabelle2016-1: update references to renamed constants and facts
2016-10-25 06:01:30 +00:00
apply(wp crunch_wps set_object_wp | wpc | simp add: crunch_simps split del: if_split)+
Updates for getpaddr system call (by Joel Beeren)
2014-07-18 15:21:34 +00:00
apply (clarsimp)
apply(fastforce simp: silc_inv_def dest: get_tcb_SomeD simp: obj_at_def is_cap_table_def)
Isabelle2016-1: update references to renamed constants and facts
2016-10-25 06:01:30 +00:00
apply(wp crunch_wps set_object_wp | wpc | simp add: crunch_simps split del: if_split)+
Updates for getpaddr system call (by Joel Beeren)
2014-07-18 15:21:34 +00:00
apply(case_tac "a = fst slot")
apply(clarsimp split: kernel_object.splits cong: conj_cong)
apply(erule notE)
apply(erule cte_wp_atE)
apply(fastforce simp: obj_at_def)
apply(drule get_tcb_SomeD)
apply(rule cte_wp_at_tcbI)
apply(simp)
apply assumption
apply (fastforce simp: tcb_cap_cases_def split: if_splits)
apply(fastforce elim: cte_wp_atE intro: cte_wp_at_cteI cte_wp_at_tcbI)
done
SELFOUR-64: Remove general Recycle operation This removes the RecycleCap CNodeInvocation, whilst retaining recycle behaviour for Endpoints -- now renamed CNodeCancelBadgedSends.
2016-11-07 06:02:50 +00:00
crunch silc_inv[wp]: update_waiting_ntfn, set_message_info, invalidate_tlb_by_asid "silc_inv aag st"
Updates for getpaddr system call (by Joel Beeren)
2014-07-18 15:21:34 +00:00
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
lemma send_signal_silc_inv[wp]:
add arch_tcb object to C, rename aep -> ntfn
2015-11-02 00:00:32 +00:00
"\<lbrace>silc_inv aag st\<rbrace> send_signal param_a param_b \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>"
unfolding send_signal_def
arm: update for simple_ko getter/setter
2017-11-27 04:59:58 +00:00
apply (wp get_simple_ko_wp gts_wp cancel_ipc_indirect_silc_inv | wpc | simp)+
Merge branch 'master' into aep-merge This commit should at least remove merge conflict markers, and the idea is that at least refine, crefine, drefine, and infoflow (with sorrys) build. Subsequent commits may be required to fix build issues that I have not picked up.
2015-09-10 07:06:45 +00:00
apply (clarsimp simp: receive_blocked_def pred_tcb_at_def obj_at_def)
done
Updates for getpaddr system call (by Joel Beeren)
2014-07-18 15:21:34 +00:00
Import release snapshot.
2014-07-14 19:32:44 +00:00
lemma perform_page_invocation_silc_inv:
"\<lbrace>silc_inv aag st and valid_page_inv blah and K (authorised_page_inv aag blah)\<rbrace>
perform_page_invocation blah
\<lbrace>\<lambda>_. silc_inv aag st\<rbrace>"
unfolding perform_page_invocation_def
apply(rule hoare_pre)
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
apply(wp mapM_wp[OF _ subset_refl] set_cap_silc_inv
mapM_x_wp[OF _ subset_refl]
Import release snapshot.
2014-07-14 19:32:44 +00:00
perform_page_table_invocation_silc_inv_get_cap_helper'[where st=st]
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
hoare_vcg_all_lift hoare_vcg_if_lift static_imp_wp
| wpc
| simp only: swp_def o_def fun_app_def K_def
|wp_once hoare_drop_imps)+
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply (clarsimp simp: valid_page_inv_def authorised_page_inv_def
split: page_invocation.splits)
apply(intro allI impI conjI)
apply(drule_tac slot="(aa,bb)" in overlapping_slots_have_labelled_overlapping_caps[rotated])
apply(fastforce)
apply(fastforce elim: is_arch_update_overlaps[rotated] cte_wp_at_weakenE)
apply fastforce
apply(fastforce simp: silc_inv_def)
apply(drule_tac slot="(aa,bb)" in overlapping_slots_have_labelled_overlapping_caps[rotated])
apply(fastforce)
apply(fastforce elim: is_arch_update_overlaps[rotated] cte_wp_at_weakenE)
apply fastforce
apply(fastforce simp: silc_inv_def)
apply(fastforce dest: is_arch_diminished_pg_is_pt_or_pg_cap simp: silc_inv_def)
done
lemma cap_insert_silc_inv':
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
"\<lbrace>silc_inv aag st and K (is_subject aag (fst dest) \<and> is_subject aag (fst src) \<and>
cap_points_to_label aag cap (pasSubject aag))\<rbrace>
Import release snapshot.
2014-07-14 19:32:44 +00:00
cap_insert cap src dest
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
\<lbrace>\<lambda>_. silc_inv aag st\<rbrace>"
Import release snapshot.
2014-07-14 19:32:44 +00:00
unfolding cap_insert_def
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
apply (wp set_cap_silc_inv hoare_vcg_ex_lift
set_untyped_cap_as_full_slots_holding_overlapping_caps_other[where aag=aag]
get_cap_wp update_cdt_silc_inv set_cap_caps_of_state2
set_untyped_cap_as_full_cdt_is_original_cap static_imp_wp
| simp split del: if_split)+
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply (intro allI impI conjI)
apply clarsimp
apply(fastforce dest: silc_invD simp: intra_label_cap_def)
apply(clarsimp simp: silc_inv_def)
apply (fastforce dest!: silc_inv_all_children simp: all_children_def simp del: split_paired_All)
done
lemma intra_label_cap_pres':
assumes cte: "\<And> P. \<lbrace> \<lambda> s. cte_wp_at P slot s \<and> R s \<rbrace> f \<lbrace>\<lambda> _. cte_wp_at P slot \<rbrace>"
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
shows
"\<lbrace> intra_label_cap aag slot and cte_wp_at Q slot and R \<rbrace>
f
\<lbrace>\<lambda> _s. (intra_label_cap aag slot s) \<rbrace>"
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(clarsimp simp: valid_def intra_label_cap_def)
apply(drule cte_wp_at_eqD)
apply(elim exE conjE, rename_tac cap')
apply(subgoal_tac "cap' = cap", blast)
apply(drule use_valid[OF _ cte], fastforce)
apply(rule_tac s=b in cte_wp_at_eqD2, auto)
done
lemma max_free_index_update_intra_label_cap[wp]:
Isabelle2018: new "op x" syntax; now is "(x)" (result of "isabelle update_op -m <dir>")
2018-06-09 08:30:53 +00:00
"\<lbrace>intra_label_cap aag slot and cte_wp_at ((=) cap) slot\<rbrace>
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
set_cap (max_free_index_update cap) slot
Import release snapshot.
2014-07-14 19:32:44 +00:00
\<lbrace>\<lambda>rv s. intra_label_cap aag slot s\<rbrace>"
unfolding set_cap_def
apply (wp set_object_wp get_object_wp | wpc| simp add: split_def)+
apply(clarsimp simp: intra_label_cap_def cap_points_to_label_def)
apply(fastforce elim: cte_wp_atE)
done
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
Import release snapshot.
2014-07-14 19:32:44 +00:00
lemma get_cap_slots_holding_overlapping_caps:
"\<lbrace>silc_inv aag st\<rbrace> get_cap slot
\<lbrace>\<lambda>cap s. (\<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<longrightarrow>
(\<exists>a. (\<exists>b. (a, b) \<in> FinalCaps.slots_holding_overlapping_caps cap s) \<and>
pasObjectAbs aag a = SilcLabel))\<rbrace>"
apply(wp get_cap_wp)
apply(fastforce dest: silc_invD simp: intra_label_cap_def)
done
lemma get_cap_cte_wp_at_triv:
Isabelle2018: new "op x" syntax; now is "(x)" (result of "isabelle update_op -m <dir>")
2018-06-09 08:30:53 +00:00
"\<lbrace> \<top> \<rbrace> get_cap slot \<lbrace>\<lambda> rv s. cte_wp_at ((=) rv) slot s \<rbrace>"
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(wp get_cap_wp, simp)
done
lemma get_cap_valid_max_free_index_update:
Isabelle2018: new "op x" syntax; now is "(x)" (result of "isabelle update_op -m <dir>")
2018-06-09 08:30:53 +00:00
"\<lbrace> \<lambda> s. \<exists> cap. cte_wp_at ((=) cap) slot s \<and> valid_cap cap s \<and> is_untyped_cap cap \<rbrace>
Import release snapshot.
2014-07-14 19:32:44 +00:00
get_cap slot
\<lbrace>\<lambda>rv s. s \<turnstile> max_free_index_update rv\<rbrace>"
apply(wp get_cap_wp)
apply clarsimp
apply(drule (1) cte_wp_at_eqD2, clarsimp)
done
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
lemma get_cap_perform_asid_control_invocation_helper:
Isabelle2018: new "op x" syntax; now is "(x)" (result of "isabelle update_op -m <dir>")
2018-06-09 08:30:53 +00:00
"\<lbrace>\<lambda> s. (\<exists> cap. cte_wp_at ((=) cap) x2 s \<and> valid_cap cap s \<and> is_untyped_cap cap) \<and> R\<rbrace>
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
get_cap x2
Import release snapshot.
2014-07-14 19:32:44 +00:00
\<lbrace>\<lambda>rv s. free_index_of rv \<le> max_free_index (untyped_sz_bits rv) \<and>
is_untyped_cap rv \<and>
max_free_index (untyped_sz_bits rv) \<le> 2 ^ cap_bits rv \<and> R\<rbrace>"
apply(wp get_cap_wp)
apply clarsimp
apply(drule (1) cte_wp_at_eqD2)
apply(case_tac capa, simp_all add: max_free_index_def free_index_of_def valid_cap_simps)
done
lemma retype_region_cte_wp_at_other':
"\<lbrace> cte_wp_at P slot and K ((fst slot) \<notin> set (retype_addrs ptr ty n us)) \<rbrace>
SELFOUR-421: infoflow and infoflow_c builds
2016-08-10 02:13:35 +00:00
retype_region ptr n us ty dev
Import release snapshot.
2014-07-14 19:32:44 +00:00
\<lbrace> \<lambda>_. cte_wp_at P slot \<rbrace>"
apply(rule hoare_gen_asm)
apply(clarsimp simp: valid_def)
apply(subst cte_wp_at_pspace')
prefer 2
apply assumption
apply(erule use_valid)
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
apply(simp only: retype_region_def retype_addrs_def
Import release snapshot.
2014-07-14 19:32:44 +00:00
foldr_upd_app_if fun_app_def K_bind_def)
apply(wp modify_wp | simp)+
apply (clarsimp simp: not_less retype_addrs_def)
done
lemma untyped_caps_are_intra_label:
"\<lbrakk>cte_wp_at is_untyped_cap slot s\<rbrakk>
\<Longrightarrow> intra_label_cap aag slot s"
apply(clarsimp simp: intra_label_cap_def cap_points_to_label_def)
apply(drule (1) cte_wp_at_eqD2)
apply(case_tac cap, simp_all)
done
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
Import release snapshot.
2014-07-14 19:32:44 +00:00
lemma perform_asid_control_invocation_silc_inv:
notes blah[simp del] = atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff
shows
"\<lbrace>silc_inv aag st and valid_aci blah and invs and K (authorised_asid_control_inv aag blah)\<rbrace>
perform_asid_control_invocation blah
\<lbrace>\<lambda>_. silc_inv aag st\<rbrace>"
apply(rule hoare_gen_asm)
unfolding perform_asid_control_invocation_def
apply(rule hoare_pre)
apply (wp modify_wp cap_insert_silc_inv' retype_region_silc_inv[where sz=pageBits]
set_cap_silc_inv get_cap_slots_holding_overlapping_caps[where st=st]
delete_objects_silc_inv static_imp_wp
| wpc | simp )+
apply (clarsimp simp: authorised_asid_control_inv_def silc_inv_def valid_aci_def ptr_range_def page_bits_def)
apply(rule conjI)
apply(clarsimp simp: range_cover_def obj_bits_api_def default_arch_object_def asid_bits_def pageBits_def)
apply(rule of_nat_inverse)
apply simp
apply(drule is_aligned_neg_mask_eq'[THEN iffD1, THEN sym])
apply(erule_tac t=x in ssubst)
apply(simp add: mask_AND_NOT_mask)
apply simp
Fix up proofs after word lemma moves
2018-09-17 06:17:28 +00:00
apply(simp add: p_assoc_help)
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(clarsimp simp: cap_points_to_label_def)
apply(erule bspec)
Fix up proofs after word lemma moves
2018-09-17 06:17:28 +00:00
apply(fastforce intro: is_aligned_no_wrap' simp: blah)
Import release snapshot.
2014-07-14 19:32:44 +00:00
done
lemma perform_asid_pool_invocation_silc_inv:
"\<lbrace>silc_inv aag st and K (authorised_asid_pool_inv aag blah)\<rbrace>
perform_asid_pool_invocation blah
\<lbrace>\<lambda>_. silc_inv aag st\<rbrace>"
apply(rule hoare_gen_asm)
unfolding perform_asid_pool_invocation_def
apply(rule hoare_pre)
apply(wp set_cap_silc_inv get_cap_wp | wpc)+
apply clarsimp
apply(rule conjI, intro impI)
apply(drule silc_invD)
apply assumption
apply(fastforce simp: intra_label_cap_def simp: cap_points_to_label_def)
apply(clarsimp simp: slots_holding_overlapping_caps_def)
apply(fastforce simp: authorised_asid_pool_inv_def silc_inv_def)
done
lemma arch_perform_invocation_silc_inv:
"\<lbrace>silc_inv aag st and invs and valid_arch_inv ai and K (authorised_arch_inv aag ai)\<rbrace>
arch_perform_invocation ai
\<lbrace>\<lambda>_. silc_inv aag st\<rbrace>"
unfolding arch_perform_invocation_def
apply(rule hoare_pre)
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
apply(wp perform_page_table_invocation_silc_inv
perform_page_directory_invocation_silc_inv
Import release snapshot.
2014-07-14 19:32:44 +00:00
perform_page_invocation_silc_inv
perform_asid_control_invocation_silc_inv
perform_asid_pool_invocation_silc_inv
| wpc)+
apply(clarsimp simp: authorised_arch_inv_def valid_arch_inv_def split: arch_invocation.splits)
done
add arch_tcb object to C, rename aep -> ntfn
2015-11-02 00:00:32 +00:00
lemma interrupt_derived_ntfn_cap_identical_refs:
"\<lbrakk>interrupt_derived cap cap'; is_ntfn_cap cap\<rbrakk> \<Longrightarrow>
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
Structures_A.obj_refs cap = Structures_A.obj_refs cap' \<and>
Import release snapshot.
2014-07-14 19:32:44 +00:00
cap_irqs cap = cap_irqs cap'"
apply(case_tac cap)
apply(simp_all add: interrupt_derived_def cap_master_cap_def split: cap.splits)
done
lemma subject_not_silc: "is_subject aag x \<Longrightarrow> silc_inv aag st s \<Longrightarrow> pasObjectAbs aag x \<noteq> SilcLabel"
apply (clarsimp simp add: silc_inv_def)
done
lemma cap_insert_silc_inv'':
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
"\<lbrace>silc_inv aag st and (\<lambda> s. \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst dest)) \<longrightarrow>
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
(\<exists> lslot. lslot \<in> slots_holding_overlapping_caps cap s \<and>
pasObjectAbs aag (fst lslot) = SilcLabel)) and
K (is_subject aag (fst src) \<and> is_subject aag (fst dest))\<rbrace>
cap_insert cap src dest
\<lbrace>\<lambda>_. silc_inv aag st\<rbrace>"
Import release snapshot.
2014-07-14 19:32:44 +00:00
unfolding cap_insert_def
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
apply (wp set_cap_silc_inv hoare_vcg_ex_lift
set_untyped_cap_as_full_slots_holding_overlapping_caps_other[where aag=aag]
get_cap_wp update_cdt_silc_inv set_cap_caps_of_state2
set_untyped_cap_as_full_cdt_is_original_cap static_imp_wp
| simp split del: if_split)+
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply (intro impI conjI allI)
apply clarsimp
apply(fastforce simp: silc_inv_def)
apply clarsimp
apply(drule_tac cap=capa in silc_invD)
apply assumption
apply(fastforce simp: intra_label_cap_def)
apply fastforce
apply(fastforce simp: silc_inv_def)
apply (elim conjE)
apply (drule(1) subject_not_silc)+
apply (subgoal_tac "\<forall>b. all_children
(\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel)
(\<lambda>a. if a = dest
then if b
then Some src else cdt s src
else cdt s a)")
apply simp
apply (intro allI)
apply (drule silc_inv_all_children)
apply (simp add: all_children_def del: split_paired_All)
apply fastforce
done
lemma cap_delete_one_cte_wp_at_other:
"\<lbrace> cte_wp_at P slot and K (slot \<noteq> irq_slot) \<rbrace>
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
cap_delete_one irq_slot
Import release snapshot.
2014-07-14 19:32:44 +00:00
\<lbrace>\<lambda>rv s. cte_wp_at P slot s \<rbrace>"
unfolding cap_delete_one_def
apply(wp hoare_unless_wp empty_slot_cte_wp_elsewhere get_cap_wp | simp)+
done
lemma invoke_irq_handler_silc_inv:
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
"\<lbrace>silc_inv aag st and pas_refined aag and irq_handler_inv_valid blah and
K (authorised_irq_hdl_inv aag blah) \<rbrace>
invoke_irq_handler blah
\<lbrace>\<lambda>_. silc_inv aag st\<rbrace>"
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(rule hoare_gen_asm)
apply(case_tac blah)
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
apply(wp cap_insert_silc_inv'' cap_delete_one_silc_inv cap_delete_one_cte_wp_at_other
static_imp_wp hoare_vcg_ex_lift
slots_holding_overlapping_caps_from_silc_inv[where aag=aag and st=st]
fewer warnings
2015-05-16 09:52:49 +00:00
| simp add: authorised_irq_hdl_inv_def get_irq_slot_def conj_comms)+
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply (clarsimp simp: pas_refined_def irq_map_wellformed_aux_def)
apply (drule cte_wp_at_eqD)
apply (elim exE conjE, rename_tac cap')
apply (drule_tac cap=cap' in silc_invD)
apply assumption
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
apply(fastforce simp: intra_label_cap_def cap_points_to_label_def
interrupt_derived_ntfn_cap_identical_refs)
apply(fastforce simp: slots_holding_overlapping_caps_def2 ctes_wp_at_def
interrupt_derived_ntfn_cap_identical_refs)
apply(wp cap_delete_one_silc_inv
| simp add: pas_refined_def irq_map_wellformed_aux_def authorised_irq_hdl_inv_def)+
Import release snapshot.
2014-07-14 19:32:44 +00:00
done
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
Import release snapshot.
2014-07-14 19:32:44 +00:00
lemma new_irq_handler_caps_are_intra_label:
Isabelle2018: new "op x" syntax; now is "(x)" (result of "isabelle update_op -m <dir>")
2018-06-09 08:30:53 +00:00
"\<lbrakk>cte_wp_at ((=) (IRQControlCap)) slot s; pas_refined aag s; is_subject aag (fst slot)\<rbrakk>
Import release snapshot.
2014-07-14 19:32:44 +00:00
\<Longrightarrow> cap_points_to_label aag (IRQHandlerCap irq) (pasSubject aag)"
apply(clarsimp simp: cap_points_to_label_def)
apply(frule cap_cur_auth_caps_of_state[rotated])
apply assumption
apply(simp add: cte_wp_at_caps_of_state)
apply(clarsimp simp: aag_cap_auth_def cap_links_irq_def)
apply(blast intro: aag_Control_into_owns_irq)
done
Genericise deletion actions that occur after empty_slot This patch adds a generic "post_cap_deletion" step that is called by finalise_slot. Previous to this, the only caps which had actions required at this stage were IRQHandlerCaps -- it was required that the IRQ bitmap be updated after the cap itself was removed (as the invariants state that for any existing IRQHandlerCap, the corresponding bit in the IRQ bitmap must be set). By genericising this, we add the capacity for new, arch-specific post cap deletion actions to occur in the future.
2018-02-07 04:08:43 +00:00
crunch silc_inv[wp]: set_irq_state "silc_inv aag st"
(wp: silc_inv_triv)
Updated specs and proofs for SELFOUR-1491: control IRQ triggering on ARM.
2018-08-14 00:25:22 +00:00
lemma arch_invoke_irq_control_silc_inv:
"\<lbrace>silc_inv aag st and pas_refined aag and arch_irq_control_inv_valid arch_irq_cinv and
K (arch_authorised_irq_ctl_inv aag arch_irq_cinv) \<rbrace>
arch_invoke_irq_control arch_irq_cinv
\<lbrace>\<lambda>_. silc_inv aag st\<rbrace>"
unfolding arch_authorised_irq_ctl_inv_def
apply(rule hoare_gen_asm)
apply(case_tac arch_irq_cinv)
apply(wp cap_insert_silc_inv'' hoare_vcg_ex_lift slots_holding_overlapping_caps_lift
| simp add: authorised_irq_ctl_inv_def arch_irq_control_inv_valid_def)+
apply(fastforce dest: new_irq_handler_caps_are_intra_label)
done
Import release snapshot.
2014-07-14 19:32:44 +00:00
lemma invoke_irq_control_silc_inv:
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
"\<lbrace>silc_inv aag st and pas_refined aag and irq_control_inv_valid blah and
K (authorised_irq_ctl_inv aag blah) \<rbrace>
invoke_irq_control blah
\<lbrace>\<lambda>_. silc_inv aag st\<rbrace>"
Updated specs and proofs for SELFOUR-1491: control IRQ triggering on ARM.
2018-08-14 00:25:22 +00:00
unfolding authorised_irq_ctl_inv_def
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(case_tac blah)
Updated specs and proofs for SELFOUR-1491: control IRQ triggering on ARM.
2018-08-14 00:25:22 +00:00
apply(rule hoare_gen_asm)
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(wp cap_insert_silc_inv'' hoare_vcg_ex_lift slots_holding_overlapping_caps_lift
Updated specs and proofs for SELFOUR-1491: control IRQ triggering on ARM.
2018-08-14 00:25:22 +00:00
| simp add: authorised_irq_ctl_inv_def)+
wp_cleanup: update proofs for new wp behaviour The things that usually go wrong: - wp fall through: add +, e.g. apply (wp select_wp) -> apply (wp select_wp)+ - precondition: you can remove most hoare_pre, but wpc still needs it, and sometimes the wp instance relies on being able to fit a rule to the current non-schematic precondition. In that case, use "including no_pre" to switch off the automatic hoare_pre application. - very rarely there is a schematic postcondition that interferes with the new trivial cleanup rules, because the rest of the script assumes some specific state afterwards (shouldn't happen in a reasonable proof, but not all proofs are reasonable..). In that case, (wp_once ...)+ should emulate the old behaviour precisely.
2017-01-13 12:58:40 +00:00
apply(fastforce dest: new_irq_handler_caps_are_intra_label)
Updated specs and proofs for SELFOUR-1491: control IRQ triggering on ARM.
2018-08-14 00:25:22 +00:00
apply (simp, rule arch_invoke_irq_control_silc_inv[simplified])
Import release snapshot.
2014-07-14 19:32:44 +00:00
done
add arch_tcb object to C, rename aep -> ntfn
2015-11-02 00:00:32 +00:00
crunch silc_inv[wp]: receive_signal "silc_inv aag st"
Import release snapshot.
2014-07-14 19:32:44 +00:00
lemma setup_caller_cap_silc_inv:
"\<lbrace>silc_inv aag st and K (is_subject aag sender \<and> is_subject aag receiver)\<rbrace>
setup_caller_cap sender receiver
\<lbrace>\<lambda>_. silc_inv aag st\<rbrace>"
unfolding setup_caller_cap_def
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
apply(wp cap_insert_silc_inv'' hoare_vcg_imp_lift hoare_vcg_ex_lift
Import release snapshot.
2014-07-14 19:32:44 +00:00
slots_holding_overlapping_caps_from_silc_inv[where aag=aag and st=st and P="\<top>"] | simp)+
apply(rule disjI1)
apply(auto simp: cap_points_to_label_def)
done
crunch silc_inv[wp]: set_extra_badge "silc_inv aag st"
lemma imp_ball_lemma:
"(R y \<longrightarrow> (\<forall>x\<in>S. P y x)) = (\<forall>x\<in>S. R y \<longrightarrow> P y x)"
apply auto
done
lemma derive_cap_silc:
"\<lbrace> \<lambda> s. (\<not> cap_points_to_label aag cap l) \<longrightarrow> (R (slots_holding_overlapping_caps cap s)) \<rbrace>
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
derive_cap slot cap
Import release snapshot.
2014-07-14 19:32:44 +00:00
\<lbrace> \<lambda> cap' s. (\<not> cap_points_to_label aag cap' l) \<longrightarrow> (R (slots_holding_overlapping_caps cap' s)) \<rbrace>,-"
apply(rule hoare_pre)
apply(simp add: derive_cap_def)
apply(wp | wpc | simp add: split_def arch_derive_cap_def)+
apply(clarsimp simp: cap_points_to_label_def)
apply (auto simp: slots_holding_overlapping_caps_def)
done
lemma transfer_caps_silc_inv:
"\<lbrace>silc_inv aag st and valid_objs and valid_mdb and pas_refined aag
and (\<lambda> s. (\<forall>x\<in>set caps.
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
s \<turnstile> fst x) \<and>
Import release snapshot.
2014-07-14 19:32:44 +00:00
(\<forall>x\<in>set caps.
cte_wp_at
(\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow>
cp = fst x)
(snd x) s \<and>
real_cte_at (snd x) s)) and
K (is_subject aag receiver \<and> (\<forall>cap\<in>set caps.
is_subject aag (fst (snd cap))))\<rbrace>
SELFOUR-56: Remove diminish rights from IPC
2016-02-10 03:11:09 +00:00
transfer_caps mi caps endpoint receiver receive_buffer
Import release snapshot.
2014-07-14 19:32:44 +00:00
\<lbrace>\<lambda>_. silc_inv aag st\<rbrace>"
apply (rule hoare_gen_asm)
apply (simp add: transfer_caps_def)
apply (wpc | wp)+
wp_cleanup: update proofs for new wp behaviour The things that usually go wrong: - wp fall through: add +, e.g. apply (wp select_wp) -> apply (wp select_wp)+ - precondition: you can remove most hoare_pre, but wpc still needs it, and sometimes the wp instance relies on being able to fit a rule to the current non-schematic precondition. In that case, use "including no_pre" to switch off the automatic hoare_pre application. - very rarely there is a schematic postcondition that interferes with the new trivial cleanup rules, because the rest of the script assumes some specific state afterwards (shouldn't happen in a reasonable proof, but not all proofs are reasonable..). In that case, (wp_once ...)+ should emulate the old behaviour precisely.
2017-01-13 12:58:40 +00:00
apply (rule_tac P = "\<forall>x \<in> set dest_slots. is_subject aag (fst x)" in hoare_gen_asm)
apply (wp transfer_caps_loop_pres_dest cap_insert_silc_inv)
apply(fastforce simp: silc_inv_def)
apply(wp get_receive_slots_authorised hoare_vcg_all_lift hoare_vcg_imp_lift | simp)+
apply(fastforce elim: cte_wp_at_weakenE)
Import release snapshot.
2014-07-14 19:32:44 +00:00
done
history squashed patch for aep-binding
2015-09-02 05:43:39 +00:00
crunch silc_inv[wp]: copy_mrs, set_message_info "silc_inv aag st"
Import release snapshot.
2014-07-14 19:32:44 +00:00
(wp: crunch_wps)
lemma do_normal_transfer_silc_inv:
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
"\<lbrace>silc_inv aag st and valid_objs and valid_mdb and pas_refined aag and
Import release snapshot.
2014-07-14 19:32:44 +00:00
K (grant \<longrightarrow> is_subject aag sender \<and> is_subject aag receiver)\<rbrace>
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
do_normal_transfer sender send_buffer ep badge grant receiver recv_buffer
Import release snapshot.
2014-07-14 19:32:44 +00:00
\<lbrace>\<lambda>_. silc_inv aag st\<rbrace>"
unfolding do_normal_transfer_def
apply(case_tac grant)
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
apply ((wp transfer_caps_silc_inv copy_mrs_cte_wp_at hoare_vcg_ball_lift lec_valid_cap'
lookup_extra_caps_authorised
Import release snapshot.
2014-07-14 19:32:44 +00:00
| simp)+)[1]
apply simp
apply(wp transfer_caps_empty_inv | simp)+
done
add arch_tcb object to C, rename aep -> ntfn
2015-11-02 00:00:32 +00:00
crunch silc_inv[wp]: do_fault_transfer, complete_signal "silc_inv aag st"
Import release snapshot.
2014-07-14 19:32:44 +00:00
(* doesn't need sym_refs *)
lemma valid_ep_recv_dequeue':
"\<lbrakk> ko_at (Endpoint (Structures_A.endpoint.RecvEP (t # ts))) epptr s;
valid_objs s\<rbrakk>
\<Longrightarrow> valid_ep (case ts of [] \<Rightarrow> Structures_A.endpoint.IdleEP
| b # bs \<Rightarrow> Structures_A.endpoint.RecvEP ts) s"
unfolding valid_objs_def valid_obj_def valid_ep_def obj_at_def
apply (drule bspec)
apply (auto split: list.splits)
done
lemma do_ipc_transfer_silc_inv:
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
"\<lbrace>silc_inv aag st and valid_objs and valid_mdb and pas_refined aag and
Import release snapshot.
2014-07-14 19:32:44 +00:00
K (grant \<longrightarrow> is_subject aag sender \<and> is_subject aag receiver)\<rbrace>
SELFOUR-56: Remove diminish rights from IPC
2016-02-10 03:11:09 +00:00
do_ipc_transfer sender ep badge grant receiver
Import release snapshot.
2014-07-14 19:32:44 +00:00
\<lbrace>\<lambda>_. silc_inv aag st\<rbrace>"
unfolding do_ipc_transfer_def
apply (wp do_normal_transfer_silc_inv hoare_vcg_all_lift | wpc | wp_once hoare_drop_imps)+
apply clarsimp
done
lemma send_ipc_silc_inv:
"\<lbrace>silc_inv aag st and valid_objs and valid_mdb and pas_refined aag and
sym_refs \<circ> state_refs_of and
(\<lambda>s. \<exists>ep. ko_at (Endpoint ep) epptr s \<and>
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
(can_grant \<longrightarrow>
Import release snapshot.
2014-07-14 19:32:44 +00:00
(\<forall>x\<in>ep_q_refs_of ep. (\<lambda>(t, rt). rt = EPRecv \<longrightarrow> is_subject aag t) x)))
and K (can_grant \<longrightarrow> is_subject aag thread)\<rbrace>
send_ipc block call badge can_grant thread epptr
\<lbrace>\<lambda>_. silc_inv aag st\<rbrace>"
unfolding send_ipc_def
apply (wp setup_caller_cap_silc_inv | wpc | simp)+
wp_cleanup: update proofs for new wp behaviour The things that usually go wrong: - wp fall through: add +, e.g. apply (wp select_wp) -> apply (wp select_wp)+ - precondition: you can remove most hoare_pre, but wpc still needs it, and sometimes the wp instance relies on being able to fit a rule to the current non-schematic precondition. In that case, use "including no_pre" to switch off the automatic hoare_pre application. - very rarely there is a schematic postcondition that interferes with the new trivial cleanup rules, because the rest of the script assumes some specific state afterwards (shouldn't happen in a reasonable proof, but not all proofs are reasonable..). In that case, (wp_once ...)+ should emulate the old behaviour precisely.
2017-01-13 12:58:40 +00:00
apply(rename_tac xs word ys recv_state)
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
apply(rule_tac Q="\<lambda> r s. (can_grant \<longrightarrow> is_subject aag thread \<and> is_subject aag (hd xs)) \<and>
silc_inv aag st s"
in hoare_strengthen_post)
wp_cleanup: update proofs for new wp behaviour The things that usually go wrong: - wp fall through: add +, e.g. apply (wp select_wp) -> apply (wp select_wp)+ - precondition: you can remove most hoare_pre, but wpc still needs it, and sometimes the wp instance relies on being able to fit a rule to the current non-schematic precondition. In that case, use "including no_pre" to switch off the automatic hoare_pre application. - very rarely there is a schematic postcondition that interferes with the new trivial cleanup rules, because the rest of the script assumes some specific state afterwards (shouldn't happen in a reasonable proof, but not all proofs are reasonable..). In that case, (wp_once ...)+ should emulate the old behaviour precisely.
2017-01-13 12:58:40 +00:00
apply simp
apply(wp do_ipc_transfer_silc_inv | wpc | simp)+
apply(wp_once hoare_drop_imps)
arm: update for simple_ko getter/setter
2017-11-27 04:59:58 +00:00
apply (wp get_simple_ko_wp)+
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply clarsimp
apply(rule conjI)
apply(fastforce simp: obj_at_def ep_q_refs_of_def)
apply(clarsimp simp: valid_ep_recv_dequeue' obj_at_def)
done
history squashed patch for aep-binding
2015-09-02 05:43:39 +00:00
lemma receive_ipc_base_silc_inv:
Wait -> Recv: update proofs
2015-11-10 15:25:02 +00:00
notes do_nbrecv_failed_transfer_def[simp]
poll: added non blocking sync wait
2015-10-21 02:34:22 +00:00
shows "\<lbrace>silc_inv aag st and valid_objs and valid_mdb and pas_refined aag and
history squashed patch for aep-binding
2015-09-02 05:43:39 +00:00
sym_refs \<circ> state_refs_of and ko_at (Endpoint ep) epptr and
K (is_subject aag receiver \<and> (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag)\<rbrace>
poll: added non blocking sync wait
2015-10-21 02:34:22 +00:00
receive_ipc_base aag receiver ep epptr rights is_blocking
Import release snapshot.
2014-07-14 19:32:44 +00:00
\<lbrace>\<lambda>_. silc_inv aag st\<rbrace>"
history squashed patch for aep-binding
2015-09-02 05:43:39 +00:00
apply (clarsimp simp: thread_get_def get_thread_state_def cong: endpoint.case_cong)
apply (rule hoare_pre)
apply (wp setup_caller_cap_silc_inv
Isabelle2016-1: update references to renamed constants and facts
2016-10-25 06:01:30 +00:00
| wpc | simp split del: if_split)+
Merge branch 'master' into aep-merge This commit should at least remove merge conflict markers, and the idea is that at least refine, crefine, drefine, and infoflow (with sorrys) build. Subsequent commits may be required to fix build issues that I have not picked up.
2015-09-10 07:06:45 +00:00
apply (rename_tac list tcb data)
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
apply(rule_tac Q="\<lambda> r s. (sender_can_grant data \<longrightarrow> is_subject aag receiver
\<and> is_subject aag (hd list))
\<and> silc_inv aag st s"
in hoare_strengthen_post)
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(wp do_ipc_transfer_silc_inv hoare_vcg_all_lift | wpc | simp)+
arm: update for simple_ko getter/setter
2017-11-27 04:59:58 +00:00
apply(wp hoare_vcg_imp_lift [OF set_simple_ko_get_tcb, unfolded disj_not1]
hoare_vcg_all_lift get_simple_ko_wp
poll: added non blocking sync wait
2015-10-21 02:34:22 +00:00
| wpc)+
infoflow: 2015 update (apart from C refinement)
2015-05-16 08:14:59 +00:00
apply (clarsimp simp: conj_comms)
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(rule conjI)
defer
apply(drule valid_objsE)
apply(fastforce simp: obj_at_def)
prefer 2
apply assumption
apply(clarsimp simp: valid_obj_def)
apply(clarsimp simp: valid_ep_def split: list.splits)
apply(rule conjI)
apply(erule bspec)
apply(fastforce intro: hd_tl_in_set)
apply(rule conjI)
apply(fastforce dest: subsetD[OF set_tl_subset])
apply(case_tac x, auto)[1]
(* clagged from Ipc_AC.receive_ipc_integrity_autarch *)
history squashed patch for aep-binding
2015-09-02 05:43:39 +00:00
apply (subgoal_tac "epptr = xa")
Import release snapshot.
2014-07-14 19:32:44 +00:00
prefer 2
history squashed patch for aep-binding
2015-09-02 05:43:39 +00:00
apply (frule_tac p = epptr in sym_refs_obj_atD, assumption)
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply (clarsimp)
apply (drule (1) bspec [OF _ hd_in_set])
history squashed patch for aep-binding
2015-09-02 05:43:39 +00:00
apply (clarsimp simp: obj_at_def tcb_bound_refs_def2 dest!: get_tcb_SomeD)
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply clarsimp
apply (subgoal_tac "aag_has_auth_to aag Control (hd x)")
apply (fastforce simp add: pas_refined_refl dest!: aag_Control_into_owns)
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
apply (rule_tac ep = "pasObjectAbs aag epptr"
in aag_wellformed_grant_Control_to_send [OF _ _ pas_refined_wellformed])
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply (rule_tac s = s in pas_refined_mem [OF sta_ts])
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
apply (clarsimp simp: tcb_at_def thread_states_def tcb_states_of_state_def
dest!: st_tcb_at_tcb_at)
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply assumption+
done
history squashed patch for aep-binding
2015-09-02 05:43:39 +00:00
lemma receive_ipc_silc_inv:
"\<lbrace>silc_inv aag st and valid_objs and valid_mdb and pas_refined aag and
sym_refs \<circ> state_refs_of and
K (is_subject aag receiver \<and>
(\<forall>epptr\<in>Access.obj_refs cap.
(pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag))\<rbrace>
poll: added non blocking sync wait
2015-10-21 02:34:22 +00:00
receive_ipc receiver cap is_blocking
history squashed patch for aep-binding
2015-09-02 05:43:39 +00:00
\<lbrace>\<lambda>_. silc_inv aag st\<rbrace>"
unfolding receive_ipc_def
apply (rule hoare_gen_asm)
apply (simp del: AllowSend_def split: cap.splits)
apply clarsimp
arm: update for simple_ko getter/setter
2017-11-27 04:59:58 +00:00
apply (rule hoare_seq_ext[OF _ get_simple_ko_sp])
add arch_tcb object to C, rename aep -> ntfn
2015-11-02 00:00:32 +00:00
apply (rule hoare_seq_ext[OF _ gbn_sp])
apply (case_tac ntfnptr, simp_all)
history squashed patch for aep-binding
2015-09-02 05:43:39 +00:00
(* old receive case, not bound *)
apply (rule hoare_pre, wp receive_ipc_base_silc_inv, clarsimp)
arm: update for simple_ko getter/setter
2017-11-27 04:59:58 +00:00
apply (rule hoare_seq_ext[OF _ get_simple_ko_sp])
add arch_tcb object to C, rename aep -> ntfn
2015-11-02 00:00:32 +00:00
apply (case_tac "isActive ntfn", simp_all)
(* new ntfn-binding case *)
history squashed patch for aep-binding
2015-09-02 05:43:39 +00:00
apply (rule hoare_pre, wp, clarsimp)
add arch_tcb object to C, rename aep -> ntfn
2015-11-02 00:00:32 +00:00
(* old receive case, bound ntfn not active *)
history squashed patch for aep-binding
2015-09-02 05:43:39 +00:00
apply (rule hoare_pre, wp receive_ipc_base_silc_inv, clarsimp)
done
Import release snapshot.
2014-07-14 19:32:44 +00:00
lemma send_fault_ipc_silc_inv:
"\<lbrace>pas_refined aag and valid_objs and sym_refs \<circ> state_refs_of and valid_mdb and
silc_inv aag st and
K (valid_fault fault) and
K (is_subject aag thread)\<rbrace>
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
send_fault_ipc thread fault
Import release snapshot.
2014-07-14 19:32:44 +00:00
\<lbrace>\<lambda>rv. silc_inv aag st\<rbrace>"
apply(rule hoare_gen_asm)+
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
unfolding send_fault_ipc_def
apply(wp send_ipc_silc_inv thread_set_valid_objs thread_set_tcb_fault_update_valid_mdb
Import release snapshot.
2014-07-14 19:32:44 +00:00
thread_set_fault_pas_refined thread_set_refs_trivial thread_set_obj_at_impossible
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
hoare_vcg_ex_lift
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
| wpc
| simp add: Let_def split_def lookup_cap_def valid_tcb_fault_update
split del: if_split)+
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(rule_tac Q="\<lambda> handler_cap s. silc_inv aag st s \<and>
valid_objs s \<and> valid_mdb s \<and>
pas_refined aag s \<and>
sym_refs (state_refs_of s) \<and>
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
(\<forall>x xa xb. handler_cap = EndpointCap x xa xb \<longrightarrow>
(AllowWrite \<in> xb \<and> AllowGrant \<in> xb \<longrightarrow>
(\<exists>xa. ko_at (Endpoint xa) x s \<and>
(\<forall>x\<in>ep_q_refs_of xa.
snd x = EPRecv \<longrightarrow> is_subject aag (fst x)))))"
in hoare_strengthen_post)
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(wp get_cap_inv get_cap_auth_wp[where aag=aag])
apply fastforce
(* clagged from Ipc_AC.send_fault_ipc_pas_refined *)
apply wp
Minor adjustments caused by Strengthen changes.
2015-10-29 00:22:21 +00:00
apply (rule_tac Q'="\<lambda>rv s. silc_inv aag st s \<and> pas_refined aag s
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
\<and> valid_objs s \<and> sym_refs (state_refs_of s)
\<and> valid_mdb s
Import release snapshot.
2014-07-14 19:32:44 +00:00
\<and> is_subject aag (fst (fst rv))"
Minor adjustments caused by Strengthen changes.
2015-10-29 00:22:21 +00:00
in hoare_post_imp_R[rotated])
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply clarsimp
apply (frule caps_of_state_valid_cap, assumption)
apply (clarsimp simp: valid_cap_simps obj_at_def is_ep)
apply (subgoal_tac "\<forall>auth. aag_has_auth_to aag auth x")
apply (erule (3) owns_ep_owns_receivers', simp add: obj_at_def, assumption)
apply (auto dest!: pas_refined_mem[OF sta_caps]
simp: cap_auth_conferred_def cap_rights_to_auth_def)[1]
apply (wp get_cap_auth_wp[where aag=aag] lookup_slot_for_thread_authorised
| simp add: add: lookup_cap_def split_def)+
done
crunch silc_inv[wp]: handle_fault "silc_inv aag st"
crunch silc_inv[wp]: do_reply_transfer "silc_inv aag st"
(wp: thread_set_tcb_fault_update_silc_inv crunch_wps ignore: set_object thread_set)
crunch silc_inv[wp]: reply_from_kernel "silc_inv aag st"
(wp: crunch_wps simp: crunch_simps)
lemma setup_reply_master_silc_inv:
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
"\<lbrace>silc_inv aag st and K (is_subject aag thread)\<rbrace>
setup_reply_master thread
\<lbrace>\<lambda>_. silc_inv aag st\<rbrace>"
Import release snapshot.
2014-07-14 19:32:44 +00:00
unfolding setup_reply_master_def
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
apply (wp set_cap_silc_inv hoare_vcg_ex_lift
slots_holding_overlapping_caps_from_silc_inv[where aag=aag and st=st and P="\<top>"]
get_cap_wp static_imp_wp
| simp)+
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(clarsimp simp: cap_points_to_label_def silc_inv_def)
done
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
crunch silc_inv: restart "silc_inv aag st"
Import release snapshot.
2014-07-14 19:32:44 +00:00
(wp: crunch_wps simp: crunch_simps)
crunch silc_inv: suspend "silc_inv aag st"
lemma same_object_as_cap_points_to_label:
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
"\<lbrakk>same_object_as a cap;
Import release snapshot.
2014-07-14 19:32:44 +00:00
\<not> cap_points_to_label aag a (pasSubject aag)\<rbrakk>
\<Longrightarrow> \<not> cap_points_to_label aag cap (pasSubject aag)"
apply(simp add: same_object_as_def cap_points_to_label_def split: cap.splits)
apply(case_tac cap, simp_all)
apply(case_tac cap, simp_all)
apply(case_tac cap, simp_all)
apply(case_tac cap, simp_all)
arch_split: Access and InfoFlow now build
2016-01-25 07:40:30 +00:00
subgoal for arch1 arch2 by (cases arch1; cases arch2; simp)
Import release snapshot.
2014-07-14 19:32:44 +00:00
done
lemma same_object_as_slots_holding_overlapping_caps:
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
"\<lbrakk>same_object_as a cap;
Import release snapshot.
2014-07-14 19:32:44 +00:00
\<not> cap_points_to_label aag a (pasSubject aag)\<rbrakk> \<Longrightarrow>
slots_holding_overlapping_caps cap s = slots_holding_overlapping_caps a s"
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
apply(simp add: same_object_as_def slots_holding_overlapping_caps_def2 ctes_wp_at_def
split: cap.splits)
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(case_tac cap, simp_all)
apply(case_tac cap, simp_all)
apply(case_tac cap, simp_all)
apply(case_tac cap, simp_all)
apply(case_tac cap, simp_all)
arch_split: Access and InfoFlow now build
2016-01-25 07:40:30 +00:00
subgoal for arch1 arch2 by (cases arch1; cases arch2; simp)
Import release snapshot.
2014-07-14 19:32:44 +00:00
done
lemma checked_cap_insert_silc_inv:
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
"\<lbrace>silc_inv aag st and K (is_subject aag (fst b) \<and> is_subject aag (fst e))\<rbrace>
Import release snapshot.
2014-07-14 19:32:44 +00:00
check_cap_at a b (check_cap_at c d (cap_insert a b e))
\<lbrace>\<lambda>_. silc_inv aag st\<rbrace>"
apply(wp cap_insert_silc_inv'' get_cap_wp | simp add: check_cap_at_def)+
apply clarsimp
apply(drule_tac cap=cap in silc_invD)
apply assumption
apply(clarsimp simp: intra_label_cap_def)
apply(fastforce dest: same_object_as_cap_points_to_label)
apply(fastforce dest: same_object_as_slots_holding_overlapping_caps)
done
lemma thread_set_tcb_ipc_buffer_update_silc_inv[wp]:
"\<lbrace>silc_inv aag st\<rbrace>
thread_set (tcb_ipc_buffer_update blah) t
\<lbrace>\<lambda>_. silc_inv aag st\<rbrace>"
SELFOUR-276: Finish proofs for maximum controlled priority (MCP) To finish the proof of refinement to C, the specification for checkPrio needed strengthening: the checkPrio spec now takes a machine word argument. In the spec, priorities are still stored as 8-bit quantities, however. Once the spec was strenthened, it was possible to remove some redundant checks and mask operations from the C code. A thread's maximum controlled priority (MCP) determines the maximum thread priority or MCP it can assign to another thread (or itself).
2016-10-04 00:58:33 +00:00
by (rule thread_set_silc_inv; simp add: tcb_cap_cases_def)
Import release snapshot.
2014-07-14 19:32:44 +00:00
lemma thread_set_tcb_fault_handler_update_silc_inv[wp]:
"\<lbrace>silc_inv aag st\<rbrace>
thread_set (tcb_fault_handler_update blah) t
\<lbrace>\<lambda>_. silc_inv aag st\<rbrace>"
SELFOUR-276: Finish proofs for maximum controlled priority (MCP) To finish the proof of refinement to C, the specification for checkPrio needed strengthening: the checkPrio spec now takes a machine word argument. In the spec, priorities are still stored as 8-bit quantities, however. Once the spec was strenthened, it was possible to remove some redundant checks and mask operations from the C code. A thread's maximum controlled priority (MCP) determines the maximum thread priority or MCP it can assign to another thread (or itself).
2016-10-04 00:58:33 +00:00
by (rule thread_set_silc_inv; simp add: tcb_cap_cases_def)
Import release snapshot.
2014-07-14 19:32:44 +00:00
lemma thread_set_tcb_fault_handler_update_invs:
"\<lbrace>invs and K (length a = word_bits)\<rbrace>
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
thread_set (tcb_fault_handler_update (\<lambda>y. a)) word
Import release snapshot.
2014-07-14 19:32:44 +00:00
\<lbrace>\<lambda>rv s. invs s\<rbrace>"
apply(rule hoare_gen_asm)
apply(wp itr_wps | simp)+
done
SELFOUR-276: Finish proofs for maximum controlled priority (MCP) To finish the proof of refinement to C, the specification for checkPrio needed strengthening: the checkPrio spec now takes a machine word argument. In the spec, priorities are still stored as 8-bit quantities, however. Once the spec was strenthened, it was possible to remove some redundant checks and mask operations from the C code. A thread's maximum controlled priority (MCP) determines the maximum thread priority or MCP it can assign to another thread (or itself).
2016-10-04 00:58:33 +00:00
lemma set_mcpriority_silc_inv[wp]:
"\<lbrace>silc_inv aag st\<rbrace> set_mcpriority t mcp \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>"
unfolding set_mcpriority_def
by (rule thread_set_silc_inv; simp add: tcb_cap_cases_def)
trivial: remove some uses of find_theorems
2016-11-13 23:03:58 +00:00
add arch_tcb object to C, rename aep -> ntfn
2015-11-02 00:00:32 +00:00
crunch silc_inv[wp]: bind_notification "silc_inv aag st"
history squashed patch for aep-binding
2015-09-02 05:43:39 +00:00
Import release snapshot.
2014-07-14 19:32:44 +00:00
lemma invoke_tcb_silc_inv:
notes static_imp_wp [wp]
static_imp_conj_wp [wp]
shows
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
"\<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and
arch-split: Tcb_AI.thy done
2016-06-29 06:21:23 +00:00
Tcb_AI.tcb_inv_wf tinv and K (authorised_tcb_inv aag tinv)\<rbrace>
Import release snapshot.
2014-07-14 19:32:44 +00:00
invoke_tcb tinv
\<lbrace>\<lambda>_. silc_inv aag st\<rbrace>"
apply(case_tac tinv)
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
apply((wp restart_silc_inv hoare_vcg_if_lift suspend_silc_inv mapM_x_wp[OF _ subset_refl]
static_imp_wp
Import release snapshot.
2014-07-14 19:32:44 +00:00
| wpc
Isabelle2016-1: update references to renamed constants and facts
2016-10-25 06:01:30 +00:00
| simp split del: if_split add: authorised_tcb_inv_def check_cap_at_def
Import release snapshot.
2014-07-14 19:32:44 +00:00
| clarsimp)+)[3]
wp_cleanup: update proofs for new wp behaviour The things that usually go wrong: - wp fall through: add +, e.g. apply (wp select_wp) -> apply (wp select_wp)+ - precondition: you can remove most hoare_pre, but wpc still needs it, and sometimes the wp instance relies on being able to fit a rule to the current non-schematic precondition. In that case, use "including no_pre" to switch off the automatic hoare_pre application. - very rarely there is a schematic postcondition that interferes with the new trivial cleanup rules, because the rest of the script assumes some specific state afterwards (shouldn't happen in a reasonable proof, but not all proofs are reasonable..). In that case, (wp_once ...)+ should emulate the old behaviour precisely.
2017-01-13 12:58:40 +00:00
defer
apply((wp suspend_silc_inv restart_silc_inv | simp add: authorised_tcb_inv_def)+)[2]
add arch_tcb object to C, rename aep -> ntfn
2015-11-02 00:00:32 +00:00
(* NotificationControl *)
wp_cleanup: update proofs for new wp behaviour The things that usually go wrong: - wp fall through: add +, e.g. apply (wp select_wp) -> apply (wp select_wp)+ - precondition: you can remove most hoare_pre, but wpc still needs it, and sometimes the wp instance relies on being able to fit a rule to the current non-schematic precondition. In that case, use "including no_pre" to switch off the automatic hoare_pre application. - very rarely there is a schematic postcondition that interferes with the new trivial cleanup rules, because the rest of the script assumes some specific state afterwards (shouldn't happen in a reasonable proof, but not all proofs are reasonable..). In that case, (wp_once ...)+ should emulate the old behaviour precisely.
2017-01-13 12:58:40 +00:00
apply (rename_tac option)
apply (case_tac option)
apply ((wp | simp)+)[2]
Import release snapshot.
2014-07-14 19:32:44 +00:00
(* just ThreadControl left *)
apply (simp add: split_def cong: option.case_cong)
wp_cleanup: update proofs for new wp behaviour The things that usually go wrong: - wp fall through: add +, e.g. apply (wp select_wp) -> apply (wp select_wp)+ - precondition: you can remove most hoare_pre, but wpc still needs it, and sometimes the wp instance relies on being able to fit a rule to the current non-schematic precondition. In that case, use "including no_pre" to switch off the automatic hoare_pre application. - very rarely there is a schematic postcondition that interferes with the new trivial cleanup rules, because the rest of the script assumes some specific state afterwards (shouldn't happen in a reasonable proof, but not all proofs are reasonable..). In that case, (wp_once ...)+ should emulate the old behaviour precisely.
2017-01-13 12:58:40 +00:00
apply (wp checked_cap_insert_silc_inv hoare_vcg_all_lift_R
Import release snapshot.
2014-07-14 19:32:44 +00:00
hoare_vcg_all_lift hoare_vcg_const_imp_lift_R
cap_delete_silc_inv itr_wps(19) cap_insert_pas_refined
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
cap_delete_pas_refined cap_delete_deletes
cap_delete_valid_cap cap_delete_cte_at itr_wps(12)
Import release snapshot.
2014-07-14 19:32:44 +00:00
itr_wps(14)
check_cap_inv2[where Q="\<lambda>_. valid_list"]
check_cap_inv2[where Q="\<lambda>_. valid_sched"]
check_cap_inv2[where Q="\<lambda>_. simple_sched_action"]
|wpc
|simp add: emptyable_def tcb_cap_cases_def tcb_cap_valid_def
tcb_at_st_tcb_at
|strengthen use_no_cap_to_obj_asid_strg)+
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
apply (rule hoare_pre)
Fix up proofs after word lemma moves
2018-09-17 06:17:28 +00:00
(* This can take up to several minutes *)
apply (simp add: option_update_thread_def tcb_cap_cases_def
|wp hoare_vcg_all_lift thread_set_tcb_fault_handler_update_invs
thread_set_pas_refined thread_set_emptyable thread_set_valid_cap
thread_set_not_state_valid_sched thread_set_cte_at
thread_set_no_cap_to_trivial
|wpc)+
apply (clarsimp simp: authorised_tcb_inv_def emptyable_def)
apply (clarsimp simp: is_cap_simps is_cnode_or_valid_arch_def is_valid_vtable_root_def
|intro impI
|rule conjI)+
Import release snapshot.
2014-07-14 19:32:44 +00:00
done
lemma perform_invocation_silc_inv:
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
"\<lbrace>silc_inv aag st and valid_invocation iv and
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
authorised_invocation aag iv and einvs and simple_sched_action
and pas_refined aag and is_subject aag \<circ> cur_thread\<rbrace>
perform_invocation block call iv
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
\<lbrace>\<lambda>_. silc_inv aag st\<rbrace>"
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(case_tac iv)
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
apply(wp invoke_untyped_silc_inv send_ipc_silc_inv
invoke_tcb_silc_inv invoke_cnode_silc_inv
invoke_irq_control_silc_inv
Import release snapshot.
2014-07-14 19:32:44 +00:00
invoke_irq_handler_silc_inv
arch_perform_invocation_silc_inv
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
| simp add: authorised_invocation_def invs_valid_objs
invs_mdb invs_sym_refs
Initial proof updates for combinator changes.
2018-03-15 03:45:48 +00:00
split_def invoke_domain_def
Import release snapshot.
2014-07-14 19:32:44 +00:00
| blast)+
done
lemma handle_invocation_silc_inv:
"\<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
is_subject aag \<circ> cur_thread and ct_active and domain_sep_inv (pasMaySendIrqs aag) st'\<rbrace>
handle_invocation calling blocking
Import release snapshot.
2014-07-14 19:32:44 +00:00
\<lbrace>\<lambda>_. silc_inv aag st\<rbrace>"
apply (simp add: handle_invocation_def ts_Restart_case_helper split_def
liftE_liftM_liftME liftME_def bindE_assoc
Isabelle2016-1: update references to renamed constants and facts
2016-10-25 06:01:30 +00:00
split del: if_split)
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(wp syscall_valid perform_invocation_silc_inv set_thread_state_runnable_valid_sched
set_thread_state_pas_refined decode_invocation_authorised
Isabelle2016-1: update references to renamed constants and facts
2016-10-25 06:01:30 +00:00
| simp split del: if_split)+
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(rule_tac E="\<lambda>ft. silc_inv aag st and pas_refined aag and
valid_objs and
sym_refs \<circ> state_refs_of and
valid_mdb and
(\<lambda>y. valid_fault ft) and
infoflow: 2015 update (apart from C refinement)
2015-05-16 08:14:59 +00:00
(\<lambda>y. is_subject aag thread)" and R="Q" and Q=Q for Q in hoare_post_impErr)
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply(wp lookup_extra_caps_authorised lookup_extra_caps_auth
| simp)+
apply(rule_tac E="\<lambda>ft. silc_inv aag st and pas_refined aag and
valid_objs and
sym_refs \<circ> state_refs_of and
valid_mdb and
(\<lambda>y. valid_fault (CapFault x False ft)) and
infoflow: 2015 update (apart from C refinement)
2015-05-16 08:14:59 +00:00
(\<lambda>y. is_subject aag thread)" and R="Q" and Q=Q for Q in hoare_post_impErr)
Import release snapshot.
2014-07-14 19:32:44 +00:00
apply (wp lookup_cap_and_slot_authorised
lookup_cap_and_slot_cur_auth
| simp)+
apply (auto intro: st_tcb_ex_cap simp: ct_in_state_def runnable_eq_active)
done
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
lemmas handle_send_silc_inv =
handle_invocation_silc_inv[where calling=False, folded handle_send_def]
Import release snapshot.
2014-07-14 19:32:44 +00:00
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
lemmas handle_call_silc_inv =
handle_invocation_silc_inv[where calling=True and blocking=True, folded handle_call_def]
Import release snapshot.
2014-07-14 19:32:44 +00:00
lemma cte_wp_at_caps_of_state':
Isabelle2018: new "op x" syntax; now is "(x)" (result of "isabelle update_op -m <dir>")
2018-06-09 08:30:53 +00:00
"cte_wp_at ((=) c) slot s \<Longrightarrow> caps_of_state s slot = Some c"
Import release snapshot.
2014-07-14 19:32:44 +00:00
by(simp add: caps_of_state_def cte_wp_at_def)
lemma handle_reply_silc_inv:
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
"\<lbrace>silc_inv aag st and invs and pas_refined aag and
Import release snapshot.
2014-07-14 19:32:44 +00:00
is_subject aag \<circ> cur_thread\<rbrace>
handle_reply
\<lbrace>\<lambda>_. silc_inv aag st\<rbrace>"
apply(simp add: handle_reply_def)
apply (wp hoare_vcg_all_lift get_cap_wp | wpc )+
apply(clarsimp simp: invs_valid_objs invs_mdb)
apply(subst aag_cap_auth_Reply[symmetric], assumption)
apply(rule cap_cur_auth_caps_of_state)
apply(subst cte_wp_at_caps_of_state')
apply assumption
apply (rule refl)
apply assumption
by simp
crunch silc_inv: delete_caller_cap "silc_inv aag st"
Wait -> Recv: update proofs
2015-11-10 15:25:02 +00:00
lemma handle_recv_silc_inv:
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
"\<lbrace>silc_inv aag st and invs and pas_refined aag and
Import release snapshot.
2014-07-14 19:32:44 +00:00
is_subject aag \<circ> cur_thread\<rbrace>
Wait -> Recv: update proofs
2015-11-10 15:25:02 +00:00
handle_recv is_blocking
Import release snapshot.
2014-07-14 19:32:44 +00:00
\<lbrace>\<lambda>_. silc_inv aag st\<rbrace>"
Wait -> Recv: update proofs
2015-11-10 15:25:02 +00:00
apply (simp add: handle_recv_def Let_def lookup_cap_def split_def)
arm: update for simple_ko getter/setter
2017-11-27 04:59:58 +00:00
apply (wp hoare_vcg_all_lift get_simple_ko_wp delete_caller_cap_silc_inv
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
receive_ipc_silc_inv
Import release snapshot.
2014-07-14 19:32:44 +00:00
lookup_slot_for_thread_authorised
lookup_slot_for_thread_cap_fault
get_cap_auth_wp[where aag=aag]
SELFOUR-220: When calling handleWait, only delete the TCB's ReplyCap when actually waiting on a synchronous endpoint.
2015-07-15 07:13:06 +00:00
| wpc | simp
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
| rule_tac Q="\<lambda>rv s. invs s \<and> pas_refined aag s \<and> is_subject aag thread
SELFOUR-220: When calling handleWait, only delete the TCB's ReplyCap when actually waiting on a synchronous endpoint.
2015-07-15 07:13:06 +00:00
\<and> (pasSubject aag, Receive, pasObjectAbs aag x31) \<in> pasPolicy aag"
in hoare_strengthen_post, wp, clarsimp simp: invs_valid_objs invs_sym_refs)+
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
apply (rule_tac Q'="\<lambda>r s. silc_inv aag st s \<and> invs s \<and> pas_refined aag s
\<and> is_subject aag thread \<and> tcb_at thread s
SELFOUR-220: When calling handleWait, only delete the TCB's ReplyCap when actually waiting on a synchronous endpoint.
2015-07-15 07:13:06 +00:00
\<and> cur_thread s = thread" in hoare_post_imp_R)
apply wp
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
apply ((clarsimp simp add: invs_valid_objs invs_sym_refs
Import release snapshot.
2014-07-14 19:32:44 +00:00
| intro impI allI conjI
| rule cte_wp_valid_cap caps_of_state_cteD
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
| fastforce simp: aag_cap_auth_def cap_auth_conferred_def
Import release snapshot.
2014-07-14 19:32:44 +00:00
cap_rights_to_auth_def valid_fault_def
)+)[1]
SELFOUR-220: When calling handleWait, only delete the TCB's ReplyCap when actually waiting on a synchronous endpoint.
2015-07-15 07:13:06 +00:00
apply (wp delete_caller_cap_silc_inv | simp add: split_def cong: conj_cong)+
apply(wp | simp add: invs_valid_objs invs_mdb invs_sym_refs tcb_at_invs)+
Import release snapshot.
2014-07-14 19:32:44 +00:00
done
lemma handle_interrupt_silc_inv:
"\<lbrace>silc_inv aag st\<rbrace> handle_interrupt irq \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>"
unfolding handle_interrupt_def
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
apply (rule hoare_if)
Updating remaining proofs for tcb_arch reserved_irq and arch_fault changes * tcb_context rephrasing to (tcb_context o tcb_arch) and respectively for set operations * unfolding of reserved_irq for trivially solving most lemmas * Changes to the inductive definition of integrity_obj to account for tcb_arch and tcb_context new location * Changes to the tcb examples in ExampleSystem to include tcb_arch * Rephrasing of domain_sep_inv to accommodate the ReservedIRQ case * Mostly rephrasing of tcb_context to (some form of) (tcb_context o tcb_arch) * Trivial unfolding of handle_reserved_irq for hoare rules * Examples in Example_Valid_State.thy were updated * Nothing remarkable, mostly rephrasing of tcb_context and ReservedIRQ handling * Fun fact, some proofs are now shorter tags: [VER-623][SELFOUR-413]
2016-11-10 05:12:16 +00:00
apply(wp | wpc | simp add: handle_reserved_irq_def | wp_once hoare_drop_imps)+
Import release snapshot.
2014-07-14 19:32:44 +00:00
done
lemma handle_vm_fault_silc_inv:
"\<lbrace>silc_inv aag st\<rbrace> handle_vm_fault thread vmfault_type
\<lbrace>\<lambda>_. silc_inv aag st\<rbrace>"
apply(case_tac vmfault_type)
apply(wp | simp)+
done
Bisim / Access / InfoFlow: updates for Hypervisor stub
2017-02-21 23:49:35 +00:00
crunch silc_inv: handle_hypervisor_fault "silc_inv aag st"
Import release snapshot.
2014-07-14 19:32:44 +00:00
lemma handle_event_silc_inv:
"\<lbrace> silc_inv aag st and einvs and simple_sched_action and
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
(\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> ct_active s) and
pas_refined aag and (\<lambda>s. ct_active s \<longrightarrow> is_subject aag (cur_thread s)) and
domain_sep_inv (pasMaySendIrqs aag) st'\<rbrace>
handle_event ev
Import release snapshot.
2014-07-14 19:32:44 +00:00
\<lbrace> \<lambda>_. silc_inv aag st\<rbrace>"
apply(case_tac ev, simp_all)
apply(rule hoare_pre)
Removes all trailing whitespaces
2017-07-12 05:13:51 +00:00
apply(wpc
Import release snapshot.
2014-07-14 19:32:44 +00:00
| wp handle_send_silc_inv[where st'=st'] handle_call_silc_inv[where st'=st']
Wait -> Recv: update proofs
2015-11-10 15:25:02 +00:00
handle_recv_silc_inv handle_reply_silc_inv
Import release snapshot.
2014-07-14 19:32:44 +00:00
handle_interrupt_silc_inv handle_vm_fault_silc_inv hy_inv
| simp add: invs_valid_objs invs_mdb invs_sym_refs)+
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
apply(rule_tac E="\<lambda>rv s. silc_inv aag st s \<and> invs s \<and> valid_fault rv \<and> is_subject aag thread"
and R="Q" and Q=Q for Q
in hoare_post_impErr)
apply(wp handle_vm_fault_silc_inv handle_hypervisor_fault_silc_inv
| simp add: invs_valid_objs invs_mdb invs_sym_refs)+
Import release snapshot.
2014-07-14 19:32:44 +00:00
done
crunch silc_inv[wp]: activate_thread "silc_inv aag st"
lemma intra_label_cap_cur_thread[simp]:
"intra_label_cap aag slot (s\<lparr>cur_thread := X\<rparr>) = intra_label_cap aag slot s"
apply(simp add: intra_label_cap_def)
done
lemma slots_holding_overlapping_caps_cur_thread[simp]:
"slots_holding_overlapping_caps cap (s\<lparr>cur_thread := X\<rparr>) = slots_holding_overlapping_caps cap s"
apply(simp add: slots_holding_overlapping_caps_def2 ctes_wp_at_def)
done
lemma silc_inv_cur_thread[simp]:
"silc_inv aag st (s\<lparr>cur_thread := X\<rparr>) = silc_inv aag st s"
apply(simp add: silc_inv_def silc_dom_equiv_def equiv_for_def)
done
crunch silc_inv[wp]: schedule "silc_inv aag st"
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
( wp: alternative_wp OR_choice_weak_wp select_wp crunch_wps
ignore: set_scheduler_action ARM.clearExMonitor
simp: crunch_simps
ignore: set_scheduler_action ARM.clearExMonitor)
Import release snapshot.
2014-07-14 19:32:44 +00:00
lemma call_kernel_silc_inv:
"\<lbrace> silc_inv aag st and einvs and simple_sched_action and
infoflow: Clean up infoflow, comment, wrap lines, ...
2018-07-02 05:34:21 +00:00
(\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> ct_active s) and
pas_refined aag and is_subject aag \<circ> cur_thread and domain_sep_inv (pasMaySendIrqs aag) st'\<rbrace>
call_kernel ev
Import release snapshot.
2014-07-14 19:32:44 +00:00
\<lbrace> \<lambda>_. silc_inv aag st\<rbrace>"
apply (simp add: call_kernel_def getActiveIRQ_def)
apply (wp handle_interrupt_silc_inv handle_event_silc_inv[where st'=st'] | simp)+
done
arch_split: InfoFlow checking
2016-04-24 05:44:40 +00:00
end
SELFOUR-444: Finished InfoFlow and DRefine.
2016-05-26 07:51:53 +00:00
end