kings-crown/FVELER_Isabelle huggingface dataset:
theory CSpace_I

lemma isMDBParent_Null [simp]:
  "isMDBParentOf c (CTE NullCap m) = False"
  "isMDBParentOf (CTE NullCap m) c = False" unfolding isMDBParentOf_def by (auto split: cte.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isMDBParentOf c (CTE capability.NullCap m) = False &&& isMDBParentOf (CTE capability.NullCap m) c = False proof (prove)
goal (1 subgoal):
 1. (case (c, CTE capability.NullCap m) of (CTE a mdbA, CTE b mdbB) \<Rightarrow> if Not $ mdbRevocable mdbA then False else if Not $ a `~global.sameRegionAs~` b then False else if True then if isEndpointCap a \<and> capEPBadge a \<noteq> 0 then let badge = capEPBadge a in badge = capEPBadge b \<and> (Not $ mdbFirstBadged mdbB) else if isNotificationCap a \<and> capNtfnBadge a \<noteq> 0 then let badge = capNtfnBadge a in badge = capNtfnBadge b \<and> (Not $ mdbFirstBadged mdbB) else True else undefined) = False &&& (case (CTE capability.NullCap m, c) of (CTE a mdbA, CTE b mdbB) \<Rightarrow> if Not $ mdbRevocable mdbA then False else if Not $ a `~global.sameRegionAs~` b then False else if True then if isEndpointCap a \<and> capEPBadge a \<noteq> 0 then let badge = capEPBadge a in badge = capEPBadge b \<and> (Not $ mdbFirstBadged mdbB) else if isNotificationCap a \<and> capNtfnBadge a \<noteq> 0 then let badge = capNtfnBadge a in badge = capNtfnBadge b \<and> (Not $ mdbFirstBadged mdbB) else True else undefined) = False
theory CSpace_I

lemma capUntypedSize_simps [simp]:
  "capUntypedSize (ThreadCap r) = 1 << objBits (undefined::tcb)"
  "capUntypedSize (NotificationCap r badge a b) = 1 << objBits (undefined::Structures_H.notification)"
  "capUntypedSize (EndpointCap r badge a b c d) = 1 << objBits (undefined::endpoint)"
  "capUntypedSize (Zombie r zs n) = 1 << (zBits zs)"
  "capUntypedSize NullCap = 0"
  "capUntypedSize DomainCap = 1"
  "capUntypedSize (ArchObjectCap x) = Arch.capUntypedSize x"
  "capUntypedSize (UntypedCap d r n f) = 1 << n"
  "capUntypedSize (CNodeCap r n g n2) = 1 << (objBits (undefined::cte) + n)"
  "capUntypedSize (ReplyCap r m a) = 1 << objBits (undefined :: tcb)"
  "capUntypedSize IRQControlCap = 1"
  "capUntypedSize (IRQHandlerCap irq) = 1" by (auto simp add: capUntypedSize_def isCap_simps objBits_simps
              split: zombie_type.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((global.capUntypedSize (capability.ThreadCap r) = 1 << objBits undefined &&& global.capUntypedSize (capability.NotificationCap r badge a b) = 1 << objBits undefined &&& global.capUntypedSize (capability.EndpointCap r badge a b c d) = 1 << objBits undefined) &&& global.capUntypedSize (capability.Zombie r zs n) = 1 << zBits zs &&& global.capUntypedSize capability.NullCap = 0 &&& global.capUntypedSize capability.DomainCap = 1) &&& (global.capUntypedSize (capability.ArchObjectCap x) = Arch.capUntypedSize x &&& global.capUntypedSize (capability.UntypedCap d r n f) = 1 << n &&& global.capUntypedSize (capability.CNodeCap r n g n2) = 1 << objBits undefined + n) &&& global.capUntypedSize (capability.ReplyCap r m a) = 1 << objBits undefined &&& global.capUntypedSize capability.IRQControlCap = 1 &&& global.capUntypedSize (capability.IRQHandlerCap irq) = 1
theory CSpace_I

lemma sameRegionAs_classes:
  "\<lbrakk> sameRegionAs cap cap' \<rbrakk> \<Longrightarrow> capClass cap = capClass cap'" apply (erule sameRegionAsE) apply (rule master_eqI, rule capClass_Master) apply simp apply (simp add: capRange_def split: if_split_asm) apply (clarsimp simp: isCap_simps) apply (clarsimp simp: isCap_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. global.sameRegionAs cap cap' \<Longrightarrow> capClass cap = capClass cap' proof (prove)
goal (4 subgoals):
 1. \<lbrakk>capMasterCap cap = capMasterCap cap'; \<not> isNullCap cap; \<not> isZombie cap; \<not> isUntypedCap cap; \<not> isArchPageCap cap\<rbrakk> \<Longrightarrow> capClass cap = capClass cap'
 2. \<lbrakk>capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange cap; isUntypedCap cap\<rbrakk> \<Longrightarrow> capClass cap = capClass cap'
 3. \<lbrakk>capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange cap; isArchPageCap cap; isArchPageCap cap'\<rbrakk> \<Longrightarrow> capClass cap = capClass cap'
 4. \<lbrakk>isIRQControlCap cap; isIRQHandlerCap cap'\<rbrakk> \<Longrightarrow> capClass cap = capClass cap' proof (prove)
goal (4 subgoals):
 1. \<lbrakk>capMasterCap cap = capMasterCap cap'; \<not> isNullCap cap; \<not> isZombie cap; \<not> isUntypedCap cap; \<not> isArchPageCap cap\<rbrakk> \<Longrightarrow> capClass (capMasterCap cap) = capClass (capMasterCap cap')
 2. \<lbrakk>capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange cap; isUntypedCap cap\<rbrakk> \<Longrightarrow> capClass cap = capClass cap'
 3. \<lbrakk>capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange cap; isArchPageCap cap; isArchPageCap cap'\<rbrakk> \<Longrightarrow> capClass cap = capClass cap'
 4. \<lbrakk>isIRQControlCap cap; isIRQHandlerCap cap'\<rbrakk> \<Longrightarrow> capClass cap = capClass cap' proof (prove)
goal (3 subgoals):
 1. \<lbrakk>capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange cap; isUntypedCap cap\<rbrakk> \<Longrightarrow> capClass cap = capClass cap'
 2. \<lbrakk>capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange cap; isArchPageCap cap; isArchPageCap cap'\<rbrakk> \<Longrightarrow> capClass cap = capClass cap'
 3. \<lbrakk>isIRQControlCap cap; isIRQHandlerCap cap'\<rbrakk> \<Longrightarrow> capClass cap = capClass cap' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange cap; isArchPageCap cap; isArchPageCap cap'\<rbrakk> \<Longrightarrow> capClass cap = capClass cap'
 2. \<lbrakk>isIRQControlCap cap; isIRQHandlerCap cap'\<rbrakk> \<Longrightarrow> capClass cap = capClass cap' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isIRQControlCap cap; isIRQHandlerCap cap'\<rbrakk> \<Longrightarrow> capClass cap = capClass cap' proof (prove)
goal:
No subgoals!
theory CSpace_I

lemma capBadge_maskCapRights[simp]:
  "capBadge (maskCapRights msk cap)
    = capBadge cap" apply (cases cap;
         simp add: maskCapRights_def Let_def isCap_simps capBadge_def) apply (rename_tac arch_capability) apply (case_tac arch_capability;
         simp add: ARM_H.maskCapRights_def Let_def isCap_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. capBadge (global.maskCapRights msk cap) = capBadge cap proof (prove)
goal (1 subgoal):
 1. \<And>x8. cap = capability.ArchObjectCap x8 \<Longrightarrow> ((\<exists>v0 v1 v2 v3. Arch.maskCapRights msk x8 = capability.NotificationCap v0 v1 v2 v3) \<longrightarrow> (\<forall>v0 v1 v2 v3 v4 v5. Arch.maskCapRights msk x8 \<noteq> capability.EndpointCap v0 v1 v2 v3 v4 v5) \<and> (\<exists>v0 v1 v2 v3 v4 v5. Arch.maskCapRights msk x8 = capability.EndpointCap v0 v1 v2 v3 v4 v5)) \<and> ((\<forall>v0 v1 v2 v3. Arch.maskCapRights msk x8 \<noteq> capability.NotificationCap v0 v1 v2 v3) \<longrightarrow> (\<forall>v0 v1 v2 v3 v4 v5. Arch.maskCapRights msk x8 \<noteq> capability.EndpointCap v0 v1 v2 v3 v4 v5)) proof (prove)
goal (1 subgoal):
 1. \<And>arch_capability. cap = capability.ArchObjectCap arch_capability \<Longrightarrow> ((\<exists>v0 v1 v2 v3. Arch.maskCapRights msk arch_capability = capability.NotificationCap v0 v1 v2 v3) \<longrightarrow> (\<forall>v0 v1 v2 v3 v4 v5. Arch.maskCapRights msk arch_capability \<noteq> capability.EndpointCap v0 v1 v2 v3 v4 v5) \<and> (\<exists>v0 v1 v2 v3 v4 v5. Arch.maskCapRights msk arch_capability = capability.EndpointCap v0 v1 v2 v3 v4 v5)) \<and> ((\<forall>v0 v1 v2 v3. Arch.maskCapRights msk arch_capability \<noteq> capability.NotificationCap v0 v1 v2 v3) \<longrightarrow> (\<forall>v0 v1 v2 v3 v4 v5. Arch.maskCapRights msk arch_capability \<noteq> capability.EndpointCap v0 v1 v2 v3 v4 v5)) proof (prove)
goal:
No subgoals!
theory CSpace_I

lemma cte_wp_at_valid_objs_valid_cap':
  "\<lbrakk> cte_wp_at' P p s; valid_objs' s \<rbrakk> \<Longrightarrow> \<exists>cte. P cte \<and> s \<turnstile>' (cteCap cte)" apply (simp add: cte_wp_at_obj_cases') apply (elim disjE bexE conjE) apply (drule(1) obj_at_valid_objs') apply (clarsimp simp: projectKOs valid_obj'_def valid_cte'_def) apply (drule(1) obj_at_valid_objs') apply (clarsimp simp: projectKOs valid_obj'_def valid_cte'_def valid_tcb'_def) apply (fastforce dest: bspec [OF _ ranI]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at' P p s; valid_objs' s\<rbrakk> \<Longrightarrow> \<exists>cte. P cte \<and> valid_cap' (cteCap cte) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>obj_at' P p s \<or> (\<exists>n\<in>dom tcb_cte_cases. obj_at' (P \<circ> fst (the (tcb_cte_cases n))) (p - n) s); valid_objs' s\<rbrakk> \<Longrightarrow> \<exists>cte. P cte \<and> valid_cap' (cteCap cte) s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_objs' s; obj_at' P p s\<rbrakk> \<Longrightarrow> \<exists>cte. P cte \<and> valid_cap' (cteCap cte) s
 2. \<And>n. \<lbrakk>valid_objs' s; n \<in> dom tcb_cte_cases; obj_at' (P \<circ> fst (the (tcb_cte_cases n))) (p - n) s\<rbrakk> \<Longrightarrow> \<exists>cte. P cte \<and> valid_cap' (cteCap cte) s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_objs' s; \<exists>k. P k \<and> ((\<forall>ko. projectKO_opt ko = Some k \<longrightarrow> injectKO k = ko) \<longrightarrow> valid_obj' (injectKO k) s)\<rbrakk> \<Longrightarrow> \<exists>cte. P cte \<and> valid_cap' (cteCap cte) s
 2. \<And>n. \<lbrakk>valid_objs' s; n \<in> dom tcb_cte_cases; obj_at' (P \<circ> fst (the (tcb_cte_cases n))) (p - n) s\<rbrakk> \<Longrightarrow> \<exists>cte. P cte \<and> valid_cap' (cteCap cte) s proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>valid_objs' s; n \<in> dom tcb_cte_cases; obj_at' (P \<circ> fst (the (tcb_cte_cases n))) (p - n) s\<rbrakk> \<Longrightarrow> \<exists>cte. P cte \<and> valid_cap' (cteCap cte) s proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>valid_objs' s; n \<in> dom tcb_cte_cases; \<exists>k. (P \<circ> fst (the (tcb_cte_cases n))) k \<and> ((\<forall>ko. projectKO_opt ko = Some k \<longrightarrow> injectKO k = ko) \<longrightarrow> valid_obj' (injectKO k) s)\<rbrakk> \<Longrightarrow> \<exists>cte. P cte \<and> valid_cap' (cteCap cte) s proof (prove)
goal (1 subgoal):
 1. \<And>n k a b. \<lbrakk>valid_objs' s; tcb_cte_cases n = Some (a, b); P (a k); \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> valid_cap' (cteCap (getF k)) s; valid_tcb_state' (tcbState k) s; is_aligned (tcbIPCBuffer k) msg_align_bits; valid_bound_ntfn' (tcbBoundNotification k) s; tcbDomain k \<le> maxDomain; tcbPriority k \<le> maxPriority; tcbMCP k \<le> maxPriority\<rbrakk> \<Longrightarrow> \<exists>cte. P cte \<and> valid_cap' (cteCap cte) s proof (prove)
goal:
No subgoals!
theory CSpace_I

lemma ctes_of_valid_cap':
  "\<lbrakk> ctes_of s p = Some (CTE c n); valid_objs' s\<rbrakk> \<Longrightarrow> s \<turnstile>' c" apply (rule cte_wp_at_valid_objs_valid_cap'[where P="(=) (CTE c n)", simplified]) apply (simp add: cte_wp_at_ctes_of) apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctes_of s p = Some (CTE c n); valid_objs' s\<rbrakk> \<Longrightarrow> valid_cap' c s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ctes_of s p = Some (CTE c n); valid_objs' s\<rbrakk> \<Longrightarrow> cte_wp_at' ((=) (CTE c n)) ?p s
 2. \<lbrakk>ctes_of s p = Some (CTE c n); valid_objs' s\<rbrakk> \<Longrightarrow> valid_objs' s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctes_of s p = Some (CTE c n); valid_objs' s\<rbrakk> \<Longrightarrow> valid_objs' s proof (prove)
goal:
No subgoals!
theory CSpace_I

lemma valid_capAligned:
  "valid_cap' c s \<Longrightarrow> capAligned c" by (simp add: valid_cap'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_cap' c s \<Longrightarrow> capAligned c
theory CSpace_I

lemma init_next [simp]:
  "mdbNext initMDBNode = 0" by (simp add: initMDBNode_def nullPointer_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mdbNext initMDBNode = 0
theory CSpace_I

lemma untypedCapRange:
  "isUntypedCap cap \<Longrightarrow> capRange cap = untypedRange cap" by (clarsimp simp: isCap_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isUntypedCap cap \<Longrightarrow> capRange cap = untypedRange cap
theory CSpace_I

lemma no_direct_loop [simp]:
  "no_loops m \<Longrightarrow> m (mdbNext node) \<noteq> Some (CTE cap node)" by (fastforce simp: mdb_next_rel_def mdb_next_def no_loops_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_loops m \<Longrightarrow> m (mdbNext node) \<noteq> Some (CTE cap node)
theory CSpace_I

lemma no_loops_direct_simp:
  "no_loops m \<Longrightarrow> m \<turnstile> x \<leadsto> x = False" by (auto simp add: no_loops_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_loops m \<Longrightarrow> m \<turnstile> x \<leadsto> x = False
theory CSpace_I

lemma no_loops_trancl_simp:
  "no_loops m \<Longrightarrow> m \<turnstile> x \<leadsto>\<^sup>+ x = False" by (auto simp add: no_loops_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_loops m \<Longrightarrow> m \<turnstile> x \<leadsto>\<^sup>+ x = False
theory CSpace_I

lemma subtree_mdb_next:
  "m \<turnstile> a \<rightarrow> b \<Longrightarrow> m \<turnstile> a \<leadsto>\<^sup>+ b" by (erule subtree.induct) (auto simp: mdb_next_rel_def intro: trancl_into_trancl)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m \<turnstile> a \<rightarrow> b \<Longrightarrow> m \<turnstile> a \<leadsto>\<^sup>+ b
theory CSpace_I

lemma no_loops: "no_loops m" using chain no_0 by (rule mdb_chain_0_no_loops)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_loops m proof (prove)
using this:
mdb_chain_0 m
no_0 m

goal (1 subgoal):
 1. no_loops m
theory CSpace_I

lemma irrefl_direct_simp [iff]:
  "m \<turnstile> x \<leadsto> x = False" using no_loops by (rule no_loops_direct_simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m \<turnstile> x \<leadsto> x = False proof (prove)
using this:
no_loops m

goal (1 subgoal):
 1. m \<turnstile> x \<leadsto> x = False
theory CSpace_I

lemma irrefl_subtree [iff]:
  "m \<turnstile> x \<rightarrow> x = False" by (clarsimp dest!: subtree_mdb_next)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m \<turnstile> x \<rightarrow> x = False
theory CSpace_I

lemma no_loops_next_prev_0:
  fixes m :: cte_heap
  assumes "m src = Some (CTE src_cap src_node)"
  assumes "no_loops m"
  assumes "valid_dlist m"
  shows "(mdbNext src_node = mdbPrev src_node) =
         (mdbPrev src_node = 0 \<and> mdbNext src_node = 0)" apply (rule iffI) apply (drule sym) apply (simp add: no_loops_prev_next_0 [OF assms]) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (mdbNext src_node = mdbPrev src_node) = (mdbPrev src_node = 0 \<and> mdbNext src_node = 0) proof (prove)
goal (2 subgoals):
 1. mdbNext src_node = mdbPrev src_node \<Longrightarrow> mdbPrev src_node = 0 \<and> mdbNext src_node = 0
 2. mdbPrev src_node = 0 \<and> mdbNext src_node = 0 \<Longrightarrow> mdbNext src_node = mdbPrev src_node proof (prove)
goal (2 subgoals):
 1. mdbPrev src_node = mdbNext src_node \<Longrightarrow> mdbPrev src_node = 0 \<and> mdbNext src_node = 0
 2. mdbPrev src_node = 0 \<and> mdbNext src_node = 0 \<Longrightarrow> mdbNext src_node = mdbPrev src_node proof (prove)
goal (1 subgoal):
 1. mdbPrev src_node = 0 \<and> mdbNext src_node = 0 \<Longrightarrow> mdbNext src_node = mdbPrev src_node proof (prove)
goal:
No subgoals!
theory CSpace_I

lemma dlist [intro!]: "valid_dlist m" using valid by (simp add: valid_mdb_ctes_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_dlist m proof (prove)
using this:
valid_mdb_ctes m

goal (1 subgoal):
 1. valid_dlist m
theory CSpace_I

lemma prev_next_0_p:
  assumes "m p = Some (CTE cap node)"
  shows "(mdbPrev node = mdbNext node) =
         (mdbPrev node = 0 \<and> mdbNext node = 0)" using assms by (rule no_loops_prev_next_0) auto

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

goal (1 subgoal):
 1. (mdbPrev node = mdbNext node) = (mdbPrev node = 0 \<and> mdbNext node = 0)
theory CSpace_I

lemma next_prev_0_p:
  assumes "m p = Some (CTE cap node)"
  shows "(mdbNext node = mdbPrev node) =
         (mdbPrev node = 0 \<and> mdbNext node = 0)" using assms by (rule no_loops_next_prev_0) auto

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

goal (1 subgoal):
 1. (mdbNext node = mdbPrev node) = (mdbPrev node = 0 \<and> mdbNext node = 0)
theory CSpace_I

lemma subtree_not_0 [simp]:
  "\<not>m \<turnstile> p \<rightarrow> 0" apply clarsimp apply (erule subtree.cases) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> m \<turnstile> p \<rightarrow> 0 proof (prove)
goal (1 subgoal):
 1. m \<turnstile> p \<rightarrow> 0 \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>c'. \<lbrakk>0 = c'; m \<turnstile> p \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> False
 2. \<And>c' c''. \<lbrakk>0 = c''; m \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory CSpace_I

lemma not_0_subtree [simp]:
  "\<not>m \<turnstile> 0 \<rightarrow> p" apply clarsimp apply (erule subtree.induct) apply (auto simp: mdb_next_unfold) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> m \<turnstile> 0 \<rightarrow> p proof (prove)
goal (1 subgoal):
 1. m \<turnstile> 0 \<rightarrow> p \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>c'. \<lbrakk>m \<turnstile> 0 \<leadsto> c'; c' \<noteq> 0; m \<turnstile> 0 parentOf c'\<rbrakk> \<Longrightarrow> False
 2. \<And>c' c''. \<lbrakk>m \<turnstile> 0 \<rightarrow> c'; False; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> 0 parentOf c''\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory CSpace_I

lemma not_0_next [simp]:
  "\<not> m \<turnstile> 0 \<leadsto> p" by (clarsimp simp: mdb_next_unfold)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (0, p) \<notin> mdb_next_rel m
theory CSpace_I

lemma not_0_trancl [simp]:
  "\<not> m \<turnstile> 0 \<leadsto>\<^sup>+ p" by (clarsimp dest!: tranclD)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (0, p) \<notin> (mdb_next_rel m)\<^sup>+
theory CSpace_I

lemma rtrancl0 [simp]:
  "m \<turnstile> 0 \<leadsto>\<^sup>* p = (p = 0)" by (auto dest!: rtranclD)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m \<turnstile> 0 \<leadsto>\<^sup>* p = (p = 0)
theory CSpace_I

lemma valid_badges: "valid_badges m" using valid by (simp add: valid_mdb_ctes_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_badges m proof (prove)
using this:
valid_mdb_ctes m

goal (1 subgoal):
 1. valid_badges m
theory CSpace_I

lemma nullcaps: "valid_nullcaps m" using valid by (simp add: valid_mdb_ctes_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_nullcaps m proof (prove)
using this:
valid_mdb_ctes m

goal (1 subgoal):
 1. valid_nullcaps m
theory CSpace_I

lemma no_self_loop_next:
  assumes vmdb: "valid_mdb_ctes m"
  and     lup: "m ptr = Some cte"
  shows   "mdbNext (cteMDBNode cte) \<noteq> ptr" proof - from vmdb have "no_loops m" .. thus ?thesis by (rule no_self_loop_next_noloop) fact+ qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mdbNext (cteMDBNode cte) \<noteq> ptr proof (state)
goal (1 subgoal):
 1. mdbNext (cteMDBNode cte) \<noteq> ptr proof (chain)
picking this:
valid_mdb_ctes m proof (prove)
using this:
valid_mdb_ctes m

goal (1 subgoal):
 1. no_loops m proof (state)
this:
no_loops m

goal (1 subgoal):
 1. mdbNext (cteMDBNode cte) \<noteq> ptr proof (prove)
using this:
no_loops m

goal (1 subgoal):
 1. mdbNext (cteMDBNode cte) \<noteq> ptr proof (state)
this:
mdbNext (cteMDBNode cte) \<noteq> ptr

goal:
No subgoals!
theory CSpace_I

lemma no_self_loop_prev:
  assumes vmdb: "valid_mdb_ctes m"
  and     lup: "m ptr = Some cte"
  shows   "mdbPrev (cteMDBNode cte) \<noteq> ptr" proof assume prev: "mdbPrev (cteMDBNode cte) = ptr" from vmdb have "no_0 m" .. with lup have "ptr \<noteq> 0" by (rule no_0_neq) moreover have "mdbNext (cteMDBNode cte) \<noteq> ptr" by (rule no_self_loop_next) fact+ moreover from vmdb have "valid_dlist m" .. ultimately show False using lup prev by - (erule (1) valid_dlistEp, simp_all) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mdbPrev (cteMDBNode cte) \<noteq> ptr proof (state)
goal (1 subgoal):
 1. mdbPrev (cteMDBNode cte) = ptr \<Longrightarrow> False proof (state)
this:
mdbPrev (cteMDBNode cte) = ptr

goal (1 subgoal):
 1. mdbPrev (cteMDBNode cte) = ptr \<Longrightarrow> False proof (chain)
picking this:
valid_mdb_ctes m proof (prove)
using this:
valid_mdb_ctes m

goal (1 subgoal):
 1. no_0 m proof (state)
this:
no_0 m

goal (1 subgoal):
 1. mdbPrev (cteMDBNode cte) = ptr \<Longrightarrow> False proof (chain)
picking this:
m ptr = Some cte
no_0 m proof (prove)
using this:
m ptr = Some cte
no_0 m

goal (1 subgoal):
 1. ptr \<noteq> 0 proof (state)
this:
ptr \<noteq> 0

goal (1 subgoal):
 1. mdbPrev (cteMDBNode cte) = ptr \<Longrightarrow> False proof (state)
this:
ptr \<noteq> 0

goal (1 subgoal):
 1. mdbPrev (cteMDBNode cte) = ptr \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. mdbNext (cteMDBNode cte) \<noteq> ptr proof (state)
this:
mdbNext (cteMDBNode cte) \<noteq> ptr

goal (1 subgoal):
 1. mdbPrev (cteMDBNode cte) = ptr \<Longrightarrow> False proof (state)
this:
mdbNext (cteMDBNode cte) \<noteq> ptr

goal (1 subgoal):
 1. mdbPrev (cteMDBNode cte) = ptr \<Longrightarrow> False proof (chain)
picking this:
valid_mdb_ctes m proof (prove)
using this:
valid_mdb_ctes m

goal (1 subgoal):
 1. valid_dlist m proof (state)
this:
valid_dlist m

goal (1 subgoal):
 1. mdbPrev (cteMDBNode cte) = ptr \<Longrightarrow> False proof (chain)
picking this:
ptr \<noteq> 0
mdbNext (cteMDBNode cte) \<noteq> ptr
valid_dlist m proof (prove)
using this:
ptr \<noteq> 0
mdbNext (cteMDBNode cte) \<noteq> ptr
valid_dlist m

goal (1 subgoal):
 1. False proof (prove)
using this:
ptr \<noteq> 0
mdbNext (cteMDBNode cte) \<noteq> ptr
valid_dlist m
m ptr = Some cte
mdbPrev (cteMDBNode cte) = ptr

goal (1 subgoal):
 1. False proof (state)
this:
False

goal:
No subgoals!
theory CSpace_I

lemma p_not_next [simp]:
  "(p = mdbNext node) = False" using valid m_p by (fastforce dest: no_self_loop_next)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (p = mdbNext node) = False proof (prove)
using this:
valid_mdb_ctes m
m p = Some (CTE cap node)

goal (1 subgoal):
 1. (p = mdbNext node) = False
theory CSpace_I

lemma p_not_prev [simp]:
  "(p = mdbPrev node) = False" using valid m_p by (fastforce dest: no_self_loop_prev)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (p = mdbPrev node) = False proof (prove)
using this:
valid_mdb_ctes m
m p = Some (CTE cap node)

goal (1 subgoal):
 1. (p = mdbPrev node) = False
theory CSpace_I

lemma p_0 [simp]: "p \<noteq> 0" using m_p by clarsimp

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

goal (1 subgoal):
 1. p \<noteq> 0