theory Finalise_R

lemma cteDeleteOne_reply_pred_tcb_at:
  "\<lbrace>\<lambda>s. pred_tcb_at' proj P t s \<and> (\<exists>t' r. cte_wp_at' (\<lambda>cte. cteCap cte = ReplyCap t' False r) slot s)\<rbrace>
    cteDeleteOne slot
   \<lbrace>\<lambda>rv. pred_tcb_at' proj P t\<rbrace>" apply (simp add: cteDeleteOne_def unless_def isFinalCapability_def) apply (rule hoare_seq_ext [OF _ getCTE_sp]) apply (rule hoare_assume_pre) apply (clarsimp simp: cte_wp_at_ctes_of when_def isCap_simps
                        Let_def finaliseCapTrue_standin_def) apply (intro impI conjI, (wp | simp)+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. pred_tcb_at' proj P t s \<and> (\<exists>t' r. cte_wp_at' (\<lambda>cte. cteCap cte = capability.ReplyCap t' False r) slot s)\<rbrace> cteDeleteOne slot \<lbrace>\<lambda>rv. pred_tcb_at' proj P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. pred_tcb_at' proj P t s \<and> (\<exists>t' r. cte_wp_at' (\<lambda>cte. cteCap cte = capability.ReplyCap t' False r) slot s)\<rbrace> do cte <- getCTE slot;
when (cteCap cte \<noteq> capability.NullCap) (do final <- let mdb = cteMDBNode cte in do prevIsSameObject <- if mdbPrev mdb = nullPointer then return False else do prev <- getCTE (mdbPrev mdb);
return (global.sameObjectAs (cteCap prev) (cteCap cte))
od;
if prevIsSameObject then return False else if mdbNext mdb = nullPointer then return True else do next <- getCTE (mdbNext mdb);
return (\<not> global.sameObjectAs (cteCap cte) (cteCap next))
od
od;
(remainder, info) <- finaliseCapTrue_standin (cteCap cte) final;
y <- assert (capRemovable remainder slot \<and> info = capability.NullCap);
emptySlot slot capability.NullCap
od)
od \<lbrace>\<lambda>rv. pred_tcb_at' proj P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>cte. \<lbrace>cte_wp_at' (\<lambda>c. c = cte) slot and (\<lambda>s. pred_tcb_at' proj P t s \<and> (\<exists>t' r. cte_wp_at' (\<lambda>cte. cteCap cte = capability.ReplyCap t' False r) slot s))\<rbrace> when (cteCap cte \<noteq> capability.NullCap) (do final <- let mdb = cteMDBNode cte in do prevIsSameObject <- if mdbPrev mdb = nullPointer then return False else do prev <- getCTE (mdbPrev mdb);
return (global.sameObjectAs (cteCap prev) (cteCap cte))
od;
if prevIsSameObject then return False else if mdbNext mdb = nullPointer then return True else do next <- getCTE (mdbNext mdb);
return (\<not> global.sameObjectAs (cteCap cte) (cteCap next))
od
od;
(remainder, info) <- finaliseCapTrue_standin (cteCap cte) final;
y <- assert (capRemovable remainder slot \<and> info = capability.NullCap);
emptySlot slot capability.NullCap
od) \<lbrace>\<lambda>rv. pred_tcb_at' proj P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>cte s. (cte_wp_at' (\<lambda>c. c = cte) slot and (\<lambda>s. pred_tcb_at' proj P t s \<and> (\<exists>t' r. cte_wp_at' (\<lambda>cte. cteCap cte = capability.ReplyCap t' False r) slot s))) s \<Longrightarrow> \<lbrace>cte_wp_at' (\<lambda>c. c = cte) slot and (\<lambda>s. pred_tcb_at' proj P t s \<and> (\<exists>t' r. cte_wp_at' (\<lambda>cte. cteCap cte = capability.ReplyCap t' False r) slot s))\<rbrace> when (cteCap cte \<noteq> capability.NullCap) (do final <- let mdb = cteMDBNode cte in do prevIsSameObject <- if mdbPrev mdb = nullPointer then return False else do prev <- getCTE (mdbPrev mdb);
return (global.sameObjectAs (cteCap prev) (cteCap cte))
od;
if prevIsSameObject then return False else if mdbNext mdb = nullPointer then return True else do next <- getCTE (mdbNext mdb);
return (\<not> global.sameObjectAs (cteCap cte) (cteCap next))
od
od;
(remainder, info) <- finaliseCapTrue_standin (cteCap cte) final;
y <- assert (capRemovable remainder slot \<and> info = capability.NullCap);
emptySlot slot capability.NullCap
od) \<lbrace>\<lambda>rv. pred_tcb_at' proj P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>cte s t' r. \<lbrakk>pred_tcb_at' proj P t s; ctes_of s slot = Some cte; cteCap cte = capability.ReplyCap t' False r\<rbrakk> \<Longrightarrow> (mdbNext (cteMDBNode cte) = nullPointer \<longrightarrow> (mdbPrev (cteMDBNode cte) = nullPointer \<longrightarrow> \<lbrace>cte_wp_at' (\<lambda>c. c = cte) slot and (\<lambda>s. pred_tcb_at' proj P t s \<and> (\<exists>t' r cte. ctes_of s slot = Some cte \<and> cteCap cte = capability.ReplyCap t' False r))\<rbrace> do y <- assert (capRemovable capability.NullCap slot);
emptySlot slot capability.NullCap
od \<lbrace>\<lambda>rv. pred_tcb_at' proj P t\<rbrace>) \<and> (mdbPrev (cteMDBNode cte) \<noteq> nullPointer \<longrightarrow> \<lbrace>cte_wp_at' (\<lambda>c. c = cte) slot and (\<lambda>s. pred_tcb_at' proj P t s \<and> (\<exists>t' r cte. ctes_of s slot = Some cte \<and> cteCap cte = capability.ReplyCap t' False r))\<rbrace> do final <- do prev <- getCTE (mdbPrev (cteMDBNode cte));
if global.sameObjectAs (cteCap prev) (capability.ReplyCap t' False r) then return False else return True
od;
y <- assert (capRemovable capability.NullCap slot);
emptySlot slot capability.NullCap
od \<lbrace>\<lambda>rv. pred_tcb_at' proj P t\<rbrace>)) \<and> (mdbNext (cteMDBNode cte) \<noteq> nullPointer \<longrightarrow> (mdbPrev (cteMDBNode cte) = nullPointer \<longrightarrow> \<lbrace>cte_wp_at' (\<lambda>c. c = cte) slot and (\<lambda>s. pred_tcb_at' proj P t s \<and> (\<exists>t' r cte. ctes_of s slot = Some cte \<and> cteCap cte = capability.ReplyCap t' False r))\<rbrace> do next <- getCTE (mdbNext (cteMDBNode cte));
y <- assert (capRemovable capability.NullCap slot);
emptySlot slot capability.NullCap
od \<lbrace>\<lambda>rv. pred_tcb_at' proj P t\<rbrace>) \<and> (mdbPrev (cteMDBNode cte) \<noteq> nullPointer \<longrightarrow> \<lbrace>cte_wp_at' (\<lambda>c. c = cte) slot and (\<lambda>s. pred_tcb_at' proj P t s \<and> (\<exists>t' r cte. ctes_of s slot = Some cte \<and> cteCap cte = capability.ReplyCap t' False r))\<rbrace> do final <- do prev <- getCTE (mdbPrev (cteMDBNode cte));
if global.sameObjectAs (cteCap prev) (capability.ReplyCap t' False r) then return False else do next <- getCTE (mdbNext (cteMDBNode cte));
return (\<not> global.sameObjectAs (capability.ReplyCap t' False r) (cteCap next))
od
od;
y <- assert (capRemovable capability.NullCap slot);
emptySlot slot capability.NullCap
od \<lbrace>\<lambda>rv. pred_tcb_at' proj P t\<rbrace>)) \<and> ((\<forall>v1. v1) \<longrightarrow> (mdbNext (cteMDBNode cte) = nullPointer \<longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> nullPointer \<longrightarrow> \<lbrace>cte_wp_at' (\<lambda>c. c = cte) slot and (\<lambda>s. pred_tcb_at' proj P t s \<and> (\<exists>t' r cte. ctes_of s slot = Some cte \<and> cteCap cte = capability.ReplyCap t' False r))\<rbrace> do final <- do prev <- getCTE (mdbPrev (cteMDBNode cte));
if global.sameObjectAs (cteCap prev) (capability.ReplyCap t' False r) then return False else return True
od;
fail
od \<lbrace>\<lambda>rv. pred_tcb_at' proj P t\<rbrace>) \<and> (mdbNext (cteMDBNode cte) \<noteq> nullPointer \<longrightarrow> (mdbPrev (cteMDBNode cte) = nullPointer \<longrightarrow> \<lbrace>cte_wp_at' (\<lambda>c. c = cte) slot and (\<lambda>s. pred_tcb_at' proj P t s \<and> (\<exists>t' r cte. ctes_of s slot = Some cte \<and> cteCap cte = capability.ReplyCap t' False r))\<rbrace> do next <- getCTE (mdbNext (cteMDBNode cte));
fail
od \<lbrace>\<lambda>rv. pred_tcb_at' proj P t\<rbrace>) \<and> (mdbPrev (cteMDBNode cte) \<noteq> nullPointer \<longrightarrow> \<lbrace>cte_wp_at' (\<lambda>c. c = cte) slot and (\<lambda>s. pred_tcb_at' proj P t s \<and> (\<exists>t' r cte. ctes_of s slot = Some cte \<and> cteCap cte = capability.ReplyCap t' False r))\<rbrace> do final <- do prev <- getCTE (mdbPrev (cteMDBNode cte));
if global.sameObjectAs (cteCap prev) (capability.ReplyCap t' False r) then return False else do next <- getCTE (mdbNext (cteMDBNode cte));
return (\<not> global.sameObjectAs (capability.ReplyCap t' False r) (cteCap next))
od
od;
fail
od \<lbrace>\<lambda>rv. pred_tcb_at' proj P t\<rbrace>))) \<and> ((\<forall>v2. r = (\<not> v2)) \<longrightarrow> (mdbNext (cteMDBNode cte) = nullPointer \<longrightarrow> r \<longrightarrow> \<lbrace>cte_wp_at' (\<lambda>c. c = cte) slot and (\<lambda>s. pred_tcb_at' proj P t s \<and> (\<exists>t' r cte. ctes_of s slot = Some cte \<and> cteCap cte = capability.ReplyCap t' False r))\<rbrace> do final <- do prev <- getCTE (mdbPrev (cteMDBNode cte));
if global.sameObjectAs (cteCap prev) (capability.ReplyCap t' False True) then return False else return True
od;
fail
od \<lbrace>\<lambda>rv. pred_tcb_at' proj P t\<rbrace>) \<and> (r \<longrightarrow> (mdbPrev (cteMDBNode cte) = nullPointer \<longrightarrow> \<lbrace>cte_wp_at' (\<lambda>c. c = cte) slot and (\<lambda>s. pred_tcb_at' proj P t s \<and> (\<exists>t' r cte. ctes_of s slot = Some cte \<and> cteCap cte = capability.ReplyCap t' False r))\<rbrace> do next <- getCTE (mdbNext (cteMDBNode cte));
fail
od \<lbrace>\<lambda>rv. pred_tcb_at' proj P t\<rbrace>) \<and> \<lbrace>cte_wp_at' (\<lambda>c. c = cte) slot and (\<lambda>s. pred_tcb_at' proj P t s \<and> (\<exists>t' r cte. ctes_of s slot = Some cte \<and> cteCap cte = capability.ReplyCap t' False r))\<rbrace> do final <- do prev <- getCTE (mdbPrev (cteMDBNode cte));
if global.sameObjectAs (cteCap prev) (capability.ReplyCap t' False True) then return False else do next <- getCTE (mdbNext (cteMDBNode cte));
return True
od
od;
fail
od \<lbrace>\<lambda>rv. pred_tcb_at' proj P t\<rbrace>)) proof (prove)
goal:
No subgoals!