theory CSpace_R

lemma maskedAsFull_revokable_safe_parent:
  "\<lbrakk>is_simple_cap' c'; safe_parent_for' m p c'; m p = Some cte;
    cteCap cte = (maskedAsFull src_cap' a)\<rbrakk>
   \<Longrightarrow> revokable' (maskedAsFull src_cap' a) c' = revokable' src_cap' c'" apply (clarsimp simp:revokable'_def maskedAsFull_def split:if_splits capability.splits) apply (intro allI impI conjI) apply (clarsimp simp:isCap_simps is_simple_cap'_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_simple_cap' c'; safe_parent_for' m p c'; m p = Some cte; cteCap cte = maskedAsFull src_cap' a\<rbrakk> \<Longrightarrow> revokable' (maskedAsFull src_cap' a) c' = revokable' src_cap' c' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_simple_cap' c'; safe_parent_for' m p c'; m p = Some cte; isUntypedCap src_cap'; isUntypedCap a; capPtr src_cap' = capPtr a; capBlockSize src_cap' = capBlockSize a; cteCap cte = capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize a)) src_cap'\<rbrakk> \<Longrightarrow> (\<forall>x31 x32. (\<exists>x33 x34. c' = capability.NotificationCap x31 x32 x33 x34) \<longrightarrow> (x32 = capNtfnBadge (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize a)) src_cap')) = (x32 = capNtfnBadge src_cap')) \<and> ((\<exists>x4. c' = capability.IRQHandlerCap x4) \<longrightarrow> isIRQControlCap (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize a)) src_cap') = isIRQControlCap src_cap') \<and> (\<forall>x51 x52. (\<exists>x53 x54 x55 x56. c' = capability.EndpointCap x51 x52 x53 x54 x55 x56) \<longrightarrow> (x52 = capEPBadge (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize a)) src_cap')) = (x52 = capEPBadge src_cap'))
 2. \<lbrakk>is_simple_cap' c'; safe_parent_for' m p c'; m p = Some cte; capPtr (cteCap cte) = capPtr a \<longrightarrow> isUntypedCap a \<longrightarrow> isUntypedCap (cteCap cte) \<longrightarrow> capBlockSize (cteCap cte) \<noteq> capBlockSize a; src_cap' = cteCap cte\<rbrakk> \<Longrightarrow> (\<forall>x31 x32. (\<exists>x33 x34. c' = capability.NotificationCap x31 x32 x33 x34) \<longrightarrow> isUntypedCap (cteCap cte) \<and> isUntypedCap a \<and> capPtr (cteCap cte) = capPtr a \<and> capBlockSize (cteCap cte) = capBlockSize a \<longrightarrow> (x32 = capNtfnBadge (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize a)) (cteCap cte))) = (x32 = capNtfnBadge (cteCap cte))) \<and> ((\<exists>x4. c' = capability.IRQHandlerCap x4) \<longrightarrow> isUntypedCap (cteCap cte) \<and> isUntypedCap a \<and> capPtr (cteCap cte) = capPtr a \<and> capBlockSize (cteCap cte) = capBlockSize a \<longrightarrow> isIRQControlCap (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize a)) (cteCap cte)) = isIRQControlCap (cteCap cte)) \<and> (\<forall>x51 x52. (\<exists>x53 x54 x55 x56. c' = capability.EndpointCap x51 x52 x53 x54 x55 x56) \<longrightarrow> isUntypedCap (cteCap cte) \<and> isUntypedCap a \<and> capPtr (cteCap cte) = capPtr a \<and> capBlockSize (cteCap cte) = capBlockSize a \<longrightarrow> (x52 = capEPBadge (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize a)) (cteCap cte))) = (x52 = capEPBadge (cteCap cte))) proof (prove)
goal (4 subgoals):
 1. \<And>x31 x32. \<lbrakk>is_simple_cap' c'; safe_parent_for' m p c'; m p = Some cte; isUntypedCap src_cap'; isUntypedCap a; capPtr src_cap' = capPtr a; capBlockSize src_cap' = capBlockSize a; cteCap cte = capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize a)) src_cap'; \<exists>x33 x34. c' = capability.NotificationCap x31 x32 x33 x34\<rbrakk> \<Longrightarrow> (x32 = capNtfnBadge (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize a)) src_cap')) = (x32 = capNtfnBadge src_cap')
 2. \<lbrakk>is_simple_cap' c'; safe_parent_for' m p c'; m p = Some cte; isUntypedCap src_cap'; isUntypedCap a; capPtr src_cap' = capPtr a; capBlockSize src_cap' = capBlockSize a; cteCap cte = capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize a)) src_cap'; \<exists>x4. c' = capability.IRQHandlerCap x4\<rbrakk> \<Longrightarrow> isIRQControlCap (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize a)) src_cap') = isIRQControlCap src_cap'
 3. \<And>x51 x52. \<lbrakk>is_simple_cap' c'; safe_parent_for' m p c'; m p = Some cte; isUntypedCap src_cap'; isUntypedCap a; capPtr src_cap' = capPtr a; capBlockSize src_cap' = capBlockSize a; cteCap cte = capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize a)) src_cap'; \<exists>x53 x54 x55 x56. c' = capability.EndpointCap x51 x52 x53 x54 x55 x56\<rbrakk> \<Longrightarrow> (x52 = capEPBadge (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize a)) src_cap')) = (x52 = capEPBadge src_cap')
 4. \<lbrakk>is_simple_cap' c'; safe_parent_for' m p c'; m p = Some cte; capPtr (cteCap cte) = capPtr a \<longrightarrow> isUntypedCap a \<longrightarrow> isUntypedCap (cteCap cte) \<longrightarrow> capBlockSize (cteCap cte) \<noteq> capBlockSize a; src_cap' = cteCap cte\<rbrakk> \<Longrightarrow> (\<forall>x31 x32. (\<exists>x33 x34. c' = capability.NotificationCap x31 x32 x33 x34) \<longrightarrow> isUntypedCap (cteCap cte) \<and> isUntypedCap a \<and> capPtr (cteCap cte) = capPtr a \<and> capBlockSize (cteCap cte) = capBlockSize a \<longrightarrow> (x32 = capNtfnBadge (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize a)) (cteCap cte))) = (x32 = capNtfnBadge (cteCap cte))) \<and> ((\<exists>x4. c' = capability.IRQHandlerCap x4) \<longrightarrow> isUntypedCap (cteCap cte) \<and> isUntypedCap a \<and> capPtr (cteCap cte) = capPtr a \<and> capBlockSize (cteCap cte) = capBlockSize a \<longrightarrow> isIRQControlCap (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize a)) (cteCap cte)) = isIRQControlCap (cteCap cte)) \<and> (\<forall>x51 x52. (\<exists>x53 x54 x55 x56. c' = capability.EndpointCap x51 x52 x53 x54 x55 x56) \<longrightarrow> isUntypedCap (cteCap cte) \<and> isUntypedCap a \<and> capPtr (cteCap cte) = capPtr a \<and> capBlockSize (cteCap cte) = capBlockSize a \<longrightarrow> (x52 = capEPBadge (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize a)) (cteCap cte))) = (x52 = capEPBadge (cteCap cte))) proof (prove)
goal:
No subgoals!