kings-crown/FVELER_Isabelle huggingface dataset:
theory CSpace_I

lemma p_nextD:
  assumes p': "m p' = Some (CTE cap' node')"
  assumes eq: "mdbNext node = mdbNext node'"
  shows "p = p' \<or> mdbNext node = 0 \<and> mdbNext node' = 0" proof (cases "mdbNext node = 0") case True thus ?thesis using eq by simp next case False with eq have n': "mdbNext node' \<noteq> 0" by simp have "p = p'" apply (rule dlistEn [OF m_p, simplified, OF False]) apply (simp add: eq) apply (rule dlistEn [OF p', simplified, OF n']) apply clarsimp done thus ?thesis by blast qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. p = p' \<or> mdbNext node = 0 \<and> mdbNext node' = 0 proof (state)
goal (2 subgoals):
 1. mdbNext node = 0 \<Longrightarrow> p = p' \<or> mdbNext node = 0 \<and> mdbNext node' = 0
 2. mdbNext node \<noteq> 0 \<Longrightarrow> p = p' \<or> mdbNext node = 0 \<and> mdbNext node' = 0 proof (state)
this:
mdbNext node = 0

goal (2 subgoals):
 1. mdbNext node = 0 \<Longrightarrow> p = p' \<or> mdbNext node = 0 \<and> mdbNext node' = 0
 2. mdbNext node \<noteq> 0 \<Longrightarrow> p = p' \<or> mdbNext node = 0 \<and> mdbNext node' = 0 proof (prove)
using this:
mdbNext node = 0

goal (1 subgoal):
 1. p = p' \<or> mdbNext node = 0 \<and> mdbNext node' = 0 proof (prove)
using this:
mdbNext node = 0
mdbNext node = mdbNext node'

goal (1 subgoal):
 1. p = p' \<or> mdbNext node = 0 \<and> mdbNext node' = 0 proof (state)
this:
p = p' \<or> mdbNext node = 0 \<and> mdbNext node' = 0

goal (1 subgoal):
 1. mdbNext node \<noteq> 0 \<Longrightarrow> p = p' \<or> mdbNext node = 0 \<and> mdbNext node' = 0 proof (state)
goal (1 subgoal):
 1. mdbNext node \<noteq> 0 \<Longrightarrow> p = p' \<or> mdbNext node = 0 \<and> mdbNext node' = 0 proof (state)
this:
mdbNext node \<noteq> 0

goal (1 subgoal):
 1. mdbNext node \<noteq> 0 \<Longrightarrow> p = p' \<or> mdbNext node = 0 \<and> mdbNext node' = 0 proof (chain)
picking this:
mdbNext node = mdbNext node'
mdbNext node \<noteq> 0 proof (prove)
using this:
mdbNext node = mdbNext node'
mdbNext node \<noteq> 0

goal (1 subgoal):
 1. mdbNext node' \<noteq> 0 proof (state)
this:
mdbNext node' \<noteq> 0

goal (1 subgoal):
 1. mdbNext node \<noteq> 0 \<Longrightarrow> p = p' \<or> mdbNext node = 0 \<and> mdbNext node' = 0 proof (prove)
goal (1 subgoal):
 1. p = p' proof (prove)
goal (1 subgoal):
 1. \<And>cte'. \<lbrakk>m (mdbNext node) = Some cte'; mdbPrev (cteMDBNode cte') = p\<rbrakk> \<Longrightarrow> p = p' proof (prove)
goal (1 subgoal):
 1. \<And>cte'. \<lbrakk>m (mdbNext node') = Some cte'; mdbPrev (cteMDBNode cte') = p\<rbrakk> \<Longrightarrow> p = p' proof (prove)
goal (1 subgoal):
 1. \<And>cte' cte'a. \<lbrakk>m (mdbNext node') = Some cte'; mdbPrev (cteMDBNode cte') = p; m (mdbNext node') = Some cte'a; mdbPrev (cteMDBNode cte'a) = p'\<rbrakk> \<Longrightarrow> p = p' proof (prove)
goal:
No subgoals! proof (state)
this:
p = p'

goal (1 subgoal):
 1. mdbNext node \<noteq> 0 \<Longrightarrow> p = p' \<or> mdbNext node = 0 \<and> mdbNext node' = 0 proof (prove)
using this:
p = p'

goal (1 subgoal):
 1. p = p' \<or> mdbNext node = 0 \<and> mdbNext node' = 0 proof (state)
this:
p = p' \<or> mdbNext node = 0 \<and> mdbNext node' = 0

goal:
No subgoals!
theory CSpace_I

lemma p_next_eq:
  assumes "m p' = Some (CTE cap' node')"
  shows "(mdbNext node = mdbNext node') =
         (p = p' \<or> mdbNext node = 0 \<and> mdbNext node' = 0)" using assms m_p apply - apply (rule iffI) apply (erule (1) p_nextD) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (mdbNext node = mdbNext node') = (p = p' \<or> mdbNext node = 0 \<and> mdbNext node' = 0) proof (prove)
using this:
m p' = Some (CTE cap' node')
m p = Some (CTE cap node)

goal (1 subgoal):
 1. (mdbNext node = mdbNext node') = (p = p' \<or> mdbNext node = 0 \<and> mdbNext node' = 0) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m p' = Some (CTE cap' node'); m p = Some (CTE cap node)\<rbrakk> \<Longrightarrow> (mdbNext node = mdbNext node') = (p = p' \<or> mdbNext node = 0 \<and> mdbNext node' = 0) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m p' = Some (CTE cap' node'); m p = Some (CTE cap node); mdbNext node = mdbNext node'\<rbrakk> \<Longrightarrow> p = p' \<or> mdbNext node = 0 \<and> mdbNext node' = 0
 2. \<lbrakk>m p' = Some (CTE cap' node'); m p = Some (CTE cap node); p = p' \<or> mdbNext node = 0 \<and> mdbNext node' = 0\<rbrakk> \<Longrightarrow> mdbNext node = mdbNext node' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m p' = Some (CTE cap' node'); m p = Some (CTE cap node); p = p' \<or> mdbNext node = 0 \<and> mdbNext node' = 0\<rbrakk> \<Longrightarrow> mdbNext node = mdbNext node' proof (prove)
goal:
No subgoals!
theory CSpace_I

lemma p_prevD:
  assumes p': "m p' = Some (CTE cap' node')"
  assumes eq: "mdbPrev node = mdbPrev node'"
  shows "p = p' \<or> mdbPrev node = 0 \<and> mdbPrev node' = 0" proof (cases "mdbPrev node = 0") case True thus ?thesis using eq by simp next case False with eq have n': "mdbPrev node' \<noteq> 0" by simp have "p = p'" apply (rule dlistEp [OF m_p, simplified, OF False]) apply (simp add: eq) apply (rule dlistEp [OF p', simplified, OF n']) apply clarsimp done thus ?thesis by blast qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. p = p' \<or> mdbPrev node = 0 \<and> mdbPrev node' = 0 proof (state)
goal (2 subgoals):
 1. mdbPrev node = 0 \<Longrightarrow> p = p' \<or> mdbPrev node = 0 \<and> mdbPrev node' = 0
 2. mdbPrev node \<noteq> 0 \<Longrightarrow> p = p' \<or> mdbPrev node = 0 \<and> mdbPrev node' = 0 proof (state)
this:
mdbPrev node = 0

goal (2 subgoals):
 1. mdbPrev node = 0 \<Longrightarrow> p = p' \<or> mdbPrev node = 0 \<and> mdbPrev node' = 0
 2. mdbPrev node \<noteq> 0 \<Longrightarrow> p = p' \<or> mdbPrev node = 0 \<and> mdbPrev node' = 0 proof (prove)
using this:
mdbPrev node = 0

goal (1 subgoal):
 1. p = p' \<or> mdbPrev node = 0 \<and> mdbPrev node' = 0 proof (prove)
using this:
mdbPrev node = 0
mdbPrev node = mdbPrev node'

goal (1 subgoal):
 1. p = p' \<or> mdbPrev node = 0 \<and> mdbPrev node' = 0 proof (state)
this:
p = p' \<or> mdbPrev node = 0 \<and> mdbPrev node' = 0

goal (1 subgoal):
 1. mdbPrev node \<noteq> 0 \<Longrightarrow> p = p' \<or> mdbPrev node = 0 \<and> mdbPrev node' = 0 proof (state)
goal (1 subgoal):
 1. mdbPrev node \<noteq> 0 \<Longrightarrow> p = p' \<or> mdbPrev node = 0 \<and> mdbPrev node' = 0 proof (state)
this:
mdbPrev node \<noteq> 0

goal (1 subgoal):
 1. mdbPrev node \<noteq> 0 \<Longrightarrow> p = p' \<or> mdbPrev node = 0 \<and> mdbPrev node' = 0 proof (chain)
picking this:
mdbPrev node = mdbPrev node'
mdbPrev node \<noteq> 0 proof (prove)
using this:
mdbPrev node = mdbPrev node'
mdbPrev node \<noteq> 0

goal (1 subgoal):
 1. mdbPrev node' \<noteq> 0 proof (state)
this:
mdbPrev node' \<noteq> 0

goal (1 subgoal):
 1. mdbPrev node \<noteq> 0 \<Longrightarrow> p = p' \<or> mdbPrev node = 0 \<and> mdbPrev node' = 0 proof (prove)
goal (1 subgoal):
 1. p = p' proof (prove)
goal (1 subgoal):
 1. \<And>cte'. \<lbrakk>m (mdbPrev node) = Some cte'; mdbNext (cteMDBNode cte') = p\<rbrakk> \<Longrightarrow> p = p' proof (prove)
goal (1 subgoal):
 1. \<And>cte'. \<lbrakk>m (mdbPrev node') = Some cte'; mdbNext (cteMDBNode cte') = p\<rbrakk> \<Longrightarrow> p = p' proof (prove)
goal (1 subgoal):
 1. \<And>cte' cte'a. \<lbrakk>m (mdbPrev node') = Some cte'; mdbNext (cteMDBNode cte') = p; m (mdbPrev node') = Some cte'a; mdbNext (cteMDBNode cte'a) = p'\<rbrakk> \<Longrightarrow> p = p' proof (prove)
goal:
No subgoals! proof (state)
this:
p = p'

goal (1 subgoal):
 1. mdbPrev node \<noteq> 0 \<Longrightarrow> p = p' \<or> mdbPrev node = 0 \<and> mdbPrev node' = 0 proof (prove)
using this:
p = p'

goal (1 subgoal):
 1. p = p' \<or> mdbPrev node = 0 \<and> mdbPrev node' = 0 proof (state)
this:
p = p' \<or> mdbPrev node = 0 \<and> mdbPrev node' = 0

goal:
No subgoals!
theory CSpace_I

lemma p_prev_eq:
  assumes "m p' = Some (CTE cap' node')"
  shows "(mdbPrev node = mdbPrev node') =
         (p = p' \<or> mdbPrev node = 0 \<and> mdbPrev node' = 0)" using assms m_p apply - apply (rule iffI) apply (erule (1) p_prevD) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (mdbPrev node = mdbPrev node') = (p = p' \<or> mdbPrev node = 0 \<and> mdbPrev node' = 0) proof (prove)
using this:
m p' = Some (CTE cap' node')
m p = Some (CTE cap node)

goal (1 subgoal):
 1. (mdbPrev node = mdbPrev node') = (p = p' \<or> mdbPrev node = 0 \<and> mdbPrev node' = 0) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m p' = Some (CTE cap' node'); m p = Some (CTE cap node)\<rbrakk> \<Longrightarrow> (mdbPrev node = mdbPrev node') = (p = p' \<or> mdbPrev node = 0 \<and> mdbPrev node' = 0) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m p' = Some (CTE cap' node'); m p = Some (CTE cap node); mdbPrev node = mdbPrev node'\<rbrakk> \<Longrightarrow> p = p' \<or> mdbPrev node = 0 \<and> mdbPrev node' = 0
 2. \<lbrakk>m p' = Some (CTE cap' node'); m p = Some (CTE cap node); p = p' \<or> mdbPrev node = 0 \<and> mdbPrev node' = 0\<rbrakk> \<Longrightarrow> mdbPrev node = mdbPrev node' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m p' = Some (CTE cap' node'); m p = Some (CTE cap node); p = p' \<or> mdbPrev node = 0 \<and> mdbPrev node' = 0\<rbrakk> \<Longrightarrow> mdbPrev node = mdbPrev node' proof (prove)
goal:
No subgoals!
theory CSpace_I

lemma m_p_prev [intro!]:
  "m \<turnstile> mdbPrev node \<leftarrow> p" using m_p by (clarsimp simp: mdb_prev_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m \<turnstile> mdbPrev node \<leftarrow> p proof (prove)
using this:
m p = Some (CTE cap node)

goal (1 subgoal):
 1. m \<turnstile> mdbPrev node \<leftarrow> p
theory CSpace_I

lemma next_p_prev:
  "mdbNext node \<noteq> 0 \<Longrightarrow> m \<turnstile> p \<leftarrow> mdbNext node" by (rule dlist_nextD0 [OF m_p_next])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mdbNext node \<noteq> 0 \<Longrightarrow> m \<turnstile> p \<leftarrow> mdbNext node
theory CSpace_I

lemma prev_p_next:
  "mdbPrev node \<noteq> 0 \<Longrightarrow> m \<turnstile> mdbPrev node \<leadsto> p" by (rule dlist_prevD0 [OF m_p_prev])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mdbPrev node \<noteq> 0 \<Longrightarrow> m \<turnstile> mdbPrev node \<leadsto> p
theory CSpace_I

lemma p_next:
  "(m \<turnstile> p \<leadsto> p') = (p' = mdbNext node)" using m_p by (auto simp: mdb_next_unfold)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m \<turnstile> p \<leadsto> p' = (p' = mdbNext node) proof (prove)
using this:
m p = Some (CTE cap node)

goal (1 subgoal):
 1. m \<turnstile> p \<leadsto> p' = (p' = mdbNext node)
theory CSpace_I

lemma no_mdb_not_target:
  "\<lbrakk> m \<turnstile> c \<leadsto> c'; m p = Some cte; no_mdb cte; valid_dlist m; no_0 m \<rbrakk>
  \<Longrightarrow> c' \<noteq> p" apply clarsimp apply (subgoal_tac "c \<noteq> 0") prefer 2 apply (clarsimp simp: mdb_next_unfold) apply (drule (3) vdlist_nextD) apply (clarsimp simp: mdb_prev_def) apply (simp add: no_mdb_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> c \<leadsto> c'; m p = Some cte; no_mdb cte; valid_dlist m; no_0 m\<rbrakk> \<Longrightarrow> c' \<noteq> p proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> c \<leadsto> p; m p = Some cte; no_mdb cte; valid_dlist m; no_0 m; c' = p\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> c \<leadsto> p; m p = Some cte; no_mdb cte; valid_dlist m; no_0 m; c' = p; c \<noteq> 0\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>m \<turnstile> c \<leadsto> p; m p = Some cte; no_mdb cte; valid_dlist m; no_0 m; c' = p\<rbrakk> \<Longrightarrow> c \<noteq> 0 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> c \<leadsto> p; m p = Some cte; no_mdb cte; valid_dlist m; no_0 m; c' = p\<rbrakk> \<Longrightarrow> c \<noteq> 0
 2. \<lbrakk>m \<turnstile> c \<leadsto> p; m p = Some cte; no_mdb cte; valid_dlist m; no_0 m; c' = p; c \<noteq> 0\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> c \<leadsto> p; m p = Some cte; no_mdb cte; valid_dlist m; no_0 m; c' = p; c \<noteq> 0\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m p = Some cte; no_mdb cte; valid_dlist m; no_0 m; c' = p; c \<noteq> 0; m \<turnstile> c \<leftarrow> p\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m p = Some cte; no_mdb cte; valid_dlist m; no_0 m; c' = p; mdbPrev (cteMDBNode cte) \<noteq> 0; c = mdbPrev (cteMDBNode cte)\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory CSpace_I

lemma valid_dlist_init:
  "\<lbrakk> valid_dlist m; m p = Some cte; no_mdb cte \<rbrakk> \<Longrightarrow>
  valid_dlist (m (p \<mapsto> CTE cap initMDBNode))" apply (simp add: initMDBNode_def Let_def nullPointer_def) apply (clarsimp simp: no_mdb_def valid_dlist_def Let_def) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_dlist m; m p = Some cte; no_mdb cte\<rbrakk> \<Longrightarrow> valid_dlist (m(p \<mapsto> CTE cap initMDBNode)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_dlist m; m p = Some cte; no_mdb cte\<rbrakk> \<Longrightarrow> valid_dlist (m(p \<mapsto> CTE cap (MDB 0 0 True True))) proof (prove)
goal (1 subgoal):
 1. \<And>pa ctea. \<lbrakk>\<forall>p cte. m p = Some cte \<longrightarrow> (mdbPrev (cteMDBNode cte) \<noteq> 0 \<longrightarrow> (\<exists>cte'. m (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p)) \<and> (mdbNext (cteMDBNode cte) \<noteq> 0 \<longrightarrow> (\<exists>cte'. m (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p)); m p = Some cte; mdbPrev (cteMDBNode cte) = 0; mdbNext (cteMDBNode cte) = 0; pa \<noteq> p\<rbrakk> \<Longrightarrow> (mdbPrev (cteMDBNode ctea) = p \<longrightarrow> m pa = Some ctea \<longrightarrow> p \<noteq> 0 \<longrightarrow> pa = 0) \<and> (mdbPrev (cteMDBNode ctea) \<noteq> p \<longrightarrow> mdbNext (cteMDBNode ctea) = p \<longrightarrow> m pa = Some ctea \<longrightarrow> p \<noteq> 0 \<longrightarrow> pa = 0) proof (prove)
goal:
No subgoals!
theory CSpace_I

lemma aligned_untypedRange_non_empty:
  "\<lbrakk>capAligned c; isUntypedCap c\<rbrakk> \<Longrightarrow> untypedRange c \<noteq> {}" apply (frule untypedCapRange) apply (drule capAligned_capUntypedPtr) apply (clarsimp simp: isCap_simps) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>capAligned c; isUntypedCap c\<rbrakk> \<Longrightarrow> untypedRange c \<noteq> {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>capAligned c; isUntypedCap c; capRange c = untypedRange c\<rbrakk> \<Longrightarrow> untypedRange c \<noteq> {} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>isUntypedCap c; capRange c = untypedRange c\<rbrakk> \<Longrightarrow> capClass c = PhysicalClass
 2. \<lbrakk>isUntypedCap c; capRange c = untypedRange c; global.capUntypedPtr c \<in> capRange c\<rbrakk> \<Longrightarrow> untypedRange c \<noteq> {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isUntypedCap c; capRange c = untypedRange c; global.capUntypedPtr c \<in> capRange c\<rbrakk> \<Longrightarrow> untypedRange c \<noteq> {} proof (prove)
goal:
No subgoals!
theory CSpace_I

lemma usableRange_subseteq:
  "\<lbrakk>capAligned c';isUntypedCap c'\<rbrakk> \<Longrightarrow> usableUntypedRange c' \<subseteq> untypedRange c'" apply (clarsimp simp:isCap_simps capAligned_def split:if_splits) apply (erule order_trans[OF is_aligned_no_wrap']) apply (erule of_nat_power) apply (simp add:word_bits_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>capAligned c'; isUntypedCap c'\<rbrakk> \<Longrightarrow> usableUntypedRange c' \<subseteq> untypedRange c' proof (prove)
goal (1 subgoal):
 1. \<And>x d v0 v1 f. \<lbrakk>c' = capability.UntypedCap d v0 v1 f; is_aligned v0 v1; v1 < word_bits; f < 2 ^ v1; v0 + word_of_nat f \<le> x; x \<le> v0 + 2 ^ v1 - 1\<rbrakk> \<Longrightarrow> v0 \<le> x proof (prove)
goal (2 subgoals):
 1. \<And>x d v0 v1 f. \<lbrakk>c' = capability.UntypedCap d v0 v1 f; v1 < word_bits; f < 2 ^ v1; v0 + word_of_nat f \<le> x; x \<le> v0 + 2 ^ v1 - 1\<rbrakk> \<Longrightarrow> ?off21 x d v0 v1 f < 2 ^ v1
 2. \<And>x d v0 v1 f. \<lbrakk>c' = capability.UntypedCap d v0 v1 f; v1 < word_bits; f < 2 ^ v1; v0 + word_of_nat f \<le> x; x \<le> v0 + 2 ^ v1 - 1\<rbrakk> \<Longrightarrow> v0 + ?off21 x d v0 v1 f \<le> x proof (prove)
goal (2 subgoals):
 1. \<And>x d v0 v1 f. \<lbrakk>c' = capability.UntypedCap d v0 v1 f; v1 < word_bits; v0 + word_of_nat f \<le> x; x \<le> v0 + 2 ^ v1 - 1\<rbrakk> \<Longrightarrow> v1 < LENGTH(32)
 2. \<And>x d v0 v1 f. \<lbrakk>c' = capability.UntypedCap d v0 v1 f; v1 < word_bits; f < 2 ^ v1; v0 + word_of_nat f \<le> x; x \<le> v0 + 2 ^ v1 - 1\<rbrakk> \<Longrightarrow> v0 + word_of_nat f \<le> x proof (prove)
goal:
No subgoals!
theory CSpace_I

lemma untypedRange_in_capRange: "untypedRange x \<subseteq> capRange x" by (case_tac x; simp add: capRange_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. untypedRange x \<subseteq> capRange x
theory CSpace_I

lemma valid_nullcaps_init:
  "\<lbrakk> valid_nullcaps m; cap \<noteq> NullCap \<rbrakk> \<Longrightarrow> valid_nullcaps (m(p \<mapsto> CTE cap initMDBNode))" by (simp add: valid_nullcaps_def initMDBNode_def nullPointer_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_nullcaps m; cap \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> valid_nullcaps (m(p \<mapsto> CTE cap initMDBNode))
theory CSpace_I

lemma capBits_Master:
  "capBits (capMasterCap cap) = capBits cap" by (clarsimp simp: capMasterCap_def split: capability.split arch_capability.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. capBits (capMasterCap cap) = capBits cap
theory CSpace_I

lemma capUntyped_Master:
  "capUntypedPtr (capMasterCap cap) = capUntypedPtr cap" by (clarsimp simp: capMasterCap_def split: capability.split arch_capability.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. global.capUntypedPtr (capMasterCap cap) = global.capUntypedPtr cap
theory CSpace_I

lemma isZombie_capClass: "isZombie cap \<Longrightarrow> capClass cap = PhysicalClass" by (clarsimp simp: isCap_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isZombie cap \<Longrightarrow> capClass cap = PhysicalClass
theory CSpace_I

lemma no_irqD':
  "\<lbrakk> m p = Some (CTE IRQControlCap n); no_irq' m \<rbrakk> \<Longrightarrow> False" unfolding no_irq'_def apply (erule allE, erule allE, erule (1) impE) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m p = Some (CTE capability.IRQControlCap n); no_irq' m\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m p = Some (CTE capability.IRQControlCap n); \<forall>p cte. m p = Some cte \<longrightarrow> cteCap cte \<noteq> capability.IRQControlCap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m p = Some (CTE capability.IRQControlCap n); cteCap (CTE capability.IRQControlCap n) \<noteq> capability.IRQControlCap\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory CSpace_I

lemma setCTE_state_refs_of'[wp]:
  "\<lbrace>\<lambda>s. P (state_refs_of' s)\<rbrace> setCTE p cte \<lbrace>\<lambda>rv s. P (state_refs_of' s)\<rbrace>" unfolding setCTE_def apply (rule setObject_state_refs_of_eq) apply (clarsimp simp: updateObject_cte in_monad typeError_def
                        in_magnitude_check objBits_simps
                 split: kernel_object.split_asm if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (state_refs_of' s)\<rbrace> setCTE p cte \<lbrace>\<lambda>rv s. P (state_refs_of' s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (state_refs_of' s)\<rbrace> setObject p cte \<lbrace>\<lambda>rv s. P (state_refs_of' s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s s' obj obj' ptr' ptr''. (obj', s') \<in> fst (updateObject cte obj p ptr' ptr'' s) \<Longrightarrow> refs_of' obj' = refs_of' obj proof (prove)
goal:
No subgoals!
theory CSpace_I

lemma setCTE_valid_mdb:
  fixes cap
  defines "cte \<equiv> CTE cap initMDBNode"
  shows
  "\<lbrace>\<lambda>s. valid_mdb' s \<and> cte_wp_at' no_mdb ptr s \<and>
        s \<turnstile>' cap \<and> valid_objs' s \<and> cap \<noteq> NullCap \<and>
        caps_no_overlap' (ctes_of s) (capRange cap) \<and>
        fresh_virt_cap_class (capClass cap) (ctes_of s) \<and>
        (cap = capability.IRQControlCap \<longrightarrow> no_irq' (ctes_of s))\<rbrace>
  setCTE ptr cte
  \<lbrace>\<lambda>r. valid_mdb'\<rbrace>" apply (simp add: valid_mdb'_def setCTE_def cte_def cte_wp_at_ctes_of) apply (wp ctes_of_setObject_cte) apply (clarsimp simp del: fun_upd_apply) apply (erule(8) valid_mdb_ctes_init [OF _ _ _ _ _ _ refl]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_mdb' s \<and> cte_wp_at' no_mdb ptr s \<and> valid_cap' cap s \<and> valid_objs' s \<and> cap \<noteq> capability.NullCap \<and> caps_no_overlap' (ctes_of s) (capRange cap) \<and> fresh_virt_cap_class (capClass cap) (ctes_of s) \<and> (cap = capability.IRQControlCap \<longrightarrow> no_irq' (ctes_of s))\<rbrace> setCTE ptr cte \<lbrace>\<lambda>r. valid_mdb'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_mdb_ctes (ctes_of s) \<and> (\<exists>cte. ctes_of s ptr = Some cte \<and> no_mdb cte) \<and> valid_cap' cap s \<and> valid_objs' s \<and> cap \<noteq> capability.NullCap \<and> caps_no_overlap' (ctes_of s) (capRange cap) \<and> fresh_virt_cap_class (capClass cap) (ctes_of s) \<and> (cap = capability.IRQControlCap \<longrightarrow> no_irq' (ctes_of s))\<rbrace> setObject ptr (CTE cap initMDBNode) \<lbrace>\<lambda>r s. valid_mdb_ctes (ctes_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_mdb_ctes (ctes_of s) \<and> (\<exists>cte. ctes_of s ptr = Some cte \<and> no_mdb cte) \<and> valid_cap' cap s \<and> valid_objs' s \<and> cap \<noteq> capability.NullCap \<and> caps_no_overlap' (ctes_of s) (capRange cap) \<and> fresh_virt_cap_class (capClass cap) (ctes_of s) \<and> (cap = capability.IRQControlCap \<longrightarrow> no_irq' (ctes_of s)) \<Longrightarrow> valid_mdb_ctes ((ctes_of s)(ptr \<mapsto> CTE cap initMDBNode)) proof (prove)
goal (1 subgoal):
 1. \<And>s cte. \<lbrakk>valid_mdb_ctes (ctes_of s); valid_cap' cap s; ctes_of s ptr = Some cte; no_mdb cte; valid_objs' s; cap \<noteq> capability.NullCap; caps_no_overlap' (ctes_of s) (capRange cap); fresh_virt_cap_class (capClass cap) (ctes_of s); cap = capability.IRQControlCap \<longrightarrow> no_irq' (ctes_of s)\<rbrakk> \<Longrightarrow> valid_mdb_ctes ((ctes_of s)(ptr \<mapsto> CTE cap initMDBNode)) proof (prove)
goal:
No subgoals!