theory IsolatedThreadAction

lemma cteInsert_isolatable:
  "thread_actions_isolatable idx (cteInsert cap src dest)" supply if_split[split del] if_cong[cong] apply (simp add: cteInsert_def updateCap_def updateMDB_def
                   Let_def setUntypedCapAsFull_def) apply (intro thread_actions_isolatable_bind[OF _ _ hoare_pre(1)]
               thread_actions_isolatable_if
               thread_actions_isolatable_returns assert_isolatable
               getCTE_isolatable setCTE_isolatable) apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. thread_actions_isolatable idx (cteInsert cap src dest) proof (prove)
goal (1 subgoal):
 1. thread_actions_isolatable idx (cteInsert cap src dest) proof (prove)
goal (1 subgoal):
 1. thread_actions_isolatable idx (do srcCTE <- getCTE src;
oldCTE <- getCTE dest;
y <- assert (cteCap oldCTE = capability.NullCap);
y <- assert (mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer);
y <- if isUntypedCap (cteCap srcCTE) \<and> isUntypedCap cap \<and> capPtr (cteCap srcCTE) = capPtr cap \<and> capBlockSize (cteCap srcCTE) = capBlockSize cap then do cte <- getCTE src;
setCTE src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) (cteCap srcCTE)) cte)
od else return ();
y <- do cte <- getCTE dest;
setCTE dest (cteCap_update (\<lambda>_. cap) cte)
od;
y <- if dest = 0 then return () else do cte <- getCTE dest;
setCTE dest (cteMDBNode_update (\<lambda>_. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap srcCTE) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap srcCTE) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode srcCTE)))) cte)
od;
y <- if src = 0 then return () else do cte <- getCTE src;
setCTE src (cteMDBNode_update (\<lambda>_. mdbNext_update (\<lambda>_. dest) (cteMDBNode cte)) cte)
od;
if mdbNext (cteMDBNode srcCTE) = 0 then return () else do cte <- getCTE (mdbNext (cteMDBNode srcCTE));
setCTE (mdbNext (cteMDBNode srcCTE)) (cteMDBNode_update (\<lambda>_. mdbPrev_update (\<lambda>_. dest) (cteMDBNode cte)) cte)
od
od) proof (prove)
goal (26 subgoals):
 1. \<And>x xa xb xc t. isUntypedCap (cteCap x) \<and> isUntypedCap cap \<and> capPtr (cteCap x) = capPtr cap \<and> capBlockSize (cteCap x) = capBlockSize cap \<Longrightarrow> \<lbrace>?Q74 x xa xb xc t\<rbrace> getCTE src \<lbrace>\<lambda>rv. tcb_at' t\<rbrace>
 2. \<And>x xa xb xc t s. \<lbrakk>isUntypedCap (cteCap x) \<and> isUntypedCap cap \<and> capPtr (cteCap x) = capPtr cap \<and> capBlockSize (cteCap x) = capBlockSize cap; tcb_at' t s\<rbrakk> \<Longrightarrow> ?Q74 x xa xb xc t s
 3. \<And>x xa xb xc xd t. \<lbrace>?Q66 x xa xb xc xd t\<rbrace> getCTE dest \<lbrace>\<lambda>rv. tcb_at' t\<rbrace>
 4. \<And>x xa xb xc xd t s. tcb_at' t s \<Longrightarrow> ?Q66 x xa xb xc xd t s
 5. \<And>x xa xb xc xd xe t. dest \<noteq> 0 \<Longrightarrow> \<lbrace>?Q59 x xa xb xc xd xe t\<rbrace> getCTE dest \<lbrace>\<lambda>rv. tcb_at' t\<rbrace>
 6. \<And>x xa xb xc xd xe t s. \<lbrakk>dest \<noteq> 0; tcb_at' t s\<rbrakk> \<Longrightarrow> ?Q59 x xa xb xc xd xe t s
 7. \<And>x xa xb xc xd xe xf t. src \<noteq> 0 \<Longrightarrow> \<lbrace>?Q51 x xa xb xc xd xe xf t\<rbrace> getCTE src \<lbrace>\<lambda>rv. tcb_at' t\<rbrace>
 8. \<And>x xa xb xc xd xe xf t s. \<lbrakk>src \<noteq> 0; tcb_at' t s\<rbrakk> \<Longrightarrow> ?Q51 x xa xb xc xd xe xf t s
 9. \<And>x xa xb xc xd xe xf xg t. mdbNext (cteMDBNode x) \<noteq> 0 \<Longrightarrow> \<lbrace>?Q43 x xa xb xc xd xe xf xg t\<rbrace> getCTE (mdbNext (cteMDBNode x)) \<lbrace>\<lambda>rv. tcb_at' t\<rbrace>
 10. \<And>x xa xb xc xd xe xf xg t s. \<lbrakk>mdbNext (cteMDBNode x) \<noteq> 0; tcb_at' t s\<rbrakk> \<Longrightarrow> ?Q43 x xa xb xc xd xe xf xg t s
A total of 26 subgoals... proof (prove)
goal:
No subgoals!