theory Orphanage

lemma deleteASIDPool_no_orphans [wp]:
  "\<lbrace> \<lambda>s. no_orphans s \<rbrace>
   deleteASIDPool asid pool
   \<lbrace> \<lambda>rv s. no_orphans s \<rbrace>" unfolding deleteASIDPool_def apply (wp | clarsimp)+ apply (rule_tac Q="\<lambda>rv s. no_orphans s" in hoare_post_imp) apply (clarsimp simp: no_orphans_def all_queued_tcb_ptrs_def
                            all_active_tcb_ptrs_def is_active_tcb_ptr_def) apply (wp mapM_wp_inv getObject_inv loadObject_default_inv | clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>no_orphans\<rbrace> deleteASIDPool asid pool \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>no_orphans\<rbrace> do haskell_assert (asid && mask asidLowBits = 0) [];
asidTable <- gets (armKSASIDTable \<circ> ksArchState);
when (asidTable (asidHighBitsOf asid) = Just pool) $ do pool <- liftM (inv asidpool.ASIDPool) $ getObject pool;
forM [0 .e. HaskellLib_H.bit asidLowBits - 1] (\<lambda>offset. when (isJust $ pool offset) $ do flushSpace $ asid + offset;
invalidateASIDEntry $ asid + offset
od);
asidTable' <- return (asidTable aLU [(asidHighBitsOf asid, Nothing)]);
modify (\<lambda>s. s\<lparr>ksArchState := armKSASIDTable_update (\<lambda>_. asidTable') (ksArchState s)\<rparr>);
getCurThread >>= setVMRoot
od
od \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>asidTable poola. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some pool \<Longrightarrow> \<lbrace>?B6 () asidTable poola\<rbrace> mapM (\<lambda>offset. when (\<exists>y. poola offset = Some y) (do y <- flushSpace (asid + offset);
invalidateASIDEntry (asid + offset)
od)) [0 .e. 2 ^ local.asid_low_bits - 1] \<lbrace>\<lambda>xa a. no_orphans (a\<lparr>ksArchState := armKSASIDTable_update (\<lambda>_ a. if a = UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) then None else asidTable a) (ksArchState a)\<rparr>)\<rbrace>
 2. \<And>x asidTable. asidTable (asidHighBitsOf asid) = Just pool \<Longrightarrow> \<lbrace>?Q5 x asidTable\<rbrace> liftM (inv asidpool.ASIDPool) $ getObject pool \<lbrace>?B6 x asidTable\<rbrace>
 3. \<And>x. \<lbrace>?B1 x\<rbrace> gets (armKSASIDTable \<circ> ksArchState) \<lbrace>\<lambda>asidTable. if asidTable (asidHighBitsOf asid) = Just pool then ?Q5 x asidTable else no_orphans\<rbrace>
 4. \<lbrace>?Q\<rbrace> haskell_assert (asid && mask asidLowBits = 0) [] \<lbrace>?B1\<rbrace>
 5. \<And>s. no_orphans s \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>asidTable poola rv s. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some pool; no_orphans s\<rbrakk> \<Longrightarrow> no_orphans (s\<lparr>ksArchState := armKSASIDTable_update (\<lambda>_ a. if a = UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) then None else asidTable a) (ksArchState s)\<rparr>)
 2. \<And>asidTable poola. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some pool \<Longrightarrow> \<lbrace>?B6 () asidTable poola\<rbrace> mapM (\<lambda>offset. when (\<exists>y. poola offset = Some y) (do y <- flushSpace (asid + offset);
invalidateASIDEntry (asid + offset)
od)) [0 .e. 2 ^ local.asid_low_bits - 1] \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 3. \<And>x asidTable. asidTable (asidHighBitsOf asid) = Just pool \<Longrightarrow> \<lbrace>?Q5 x asidTable\<rbrace> liftM (inv asidpool.ASIDPool) $ getObject pool \<lbrace>?B6 x asidTable\<rbrace>
 4. \<And>x. \<lbrace>?B1 x\<rbrace> gets (armKSASIDTable \<circ> ksArchState) \<lbrace>\<lambda>asidTable. if asidTable (asidHighBitsOf asid) = Just pool then ?Q5 x asidTable else no_orphans\<rbrace>
 5. \<lbrace>?Q\<rbrace> haskell_assert (asid && mask asidLowBits = 0) [] \<lbrace>?B1\<rbrace>
 6. \<And>s. no_orphans s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>asidTable poola. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some pool \<Longrightarrow> \<lbrace>?B6 () asidTable poola\<rbrace> mapM (\<lambda>offset. when (\<exists>y. poola offset = Some y) (do y <- flushSpace (asid + offset);
invalidateASIDEntry (asid + offset)
od)) [0 .e. 2 ^ local.asid_low_bits - 1] \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 2. \<And>x asidTable. asidTable (asidHighBitsOf asid) = Just pool \<Longrightarrow> \<lbrace>?Q5 x asidTable\<rbrace> liftM (inv asidpool.ASIDPool) $ getObject pool \<lbrace>?B6 x asidTable\<rbrace>
 3. \<And>x. \<lbrace>?B1 x\<rbrace> gets (armKSASIDTable \<circ> ksArchState) \<lbrace>\<lambda>asidTable. if asidTable (asidHighBitsOf asid) = Just pool then ?Q5 x asidTable else no_orphans\<rbrace>
 4. \<lbrace>?Q\<rbrace> haskell_assert (asid && mask asidLowBits = 0) [] \<lbrace>?B1\<rbrace>
 5. \<And>s. no_orphans s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!