theory Finalise_R

lemma deleteASIDPool_invs[wp]:
  "\<lbrace>invs'\<rbrace> deleteASIDPool asid pool \<lbrace>\<lambda>rv. invs'\<rbrace>" apply (simp add: deleteASIDPool_def) apply wp apply (simp del: fun_upd_apply) apply (strengthen invs_asid_update_strg') apply (wp mapM_wp' getObject_inv loadObject_default_inv
              | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> deleteASIDPool asid pool \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> do y <- assert (asid && mask local.asid_low_bits = 0);
asidTable <- gets (armKSASIDTable \<circ> ksArchState);
when (asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some pool) (do pool <- liftM (inv asidpool.ASIDPool) (getObject pool);
y <- mapM (\<lambda>offset. when (\<exists>y. pool offset = Some y) (do y <- flushSpace (asid + offset);
invalidateASIDEntry (asid + offset)
od)) [0 .e. 2 ^ local.asid_low_bits - 1];
y <- modify (\<lambda>s. s\<lparr>ksArchState := armKSASIDTable_update (\<lambda>_. asidTable(UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) := None)) (ksArchState s)\<rparr>);
getCurThread >>= setVMRoot
od)
od \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>y asidTable poola. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some pool \<Longrightarrow> \<lbrace>?B5 y 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>ya s. invs' (s\<lparr>ksArchState := armKSASIDTable_update (\<lambda>_. asidTable(UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) := None)) (ksArchState s)\<rparr>)\<rbrace>
 2. \<And>y asidTable. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some pool \<Longrightarrow> \<lbrace>?Q4 y asidTable\<rbrace> liftM (inv asidpool.ASIDPool) (getObject pool) \<lbrace>?B5 y asidTable\<rbrace>
 3. \<And>y. \<lbrace>?B2 y\<rbrace> gets (armKSASIDTable \<circ> ksArchState) \<lbrace>\<lambda>asidTable. if asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some pool then ?Q4 y asidTable else invs'\<rbrace>
 4. \<lbrace>?Q1\<rbrace> assert (asid && mask local.asid_low_bits = 0) \<lbrace>?B2\<rbrace>
 5. \<And>s. invs' s \<Longrightarrow> ?Q1 s proof (prove)
goal (5 subgoals):
 1. \<And>asidTable poola. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some pool \<Longrightarrow> \<lbrace>?B5 () 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>ya s. invs' (s\<lparr>ksArchState := armKSASIDTable_update (\<lambda>_. asidTable(UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) := None)) (ksArchState s)\<rparr>)\<rbrace>
 2. \<And>y asidTable. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some pool \<Longrightarrow> \<lbrace>?Q4 y asidTable\<rbrace> liftM (inv asidpool.ASIDPool) (getObject pool) \<lbrace>?B5 y asidTable\<rbrace>
 3. \<And>y. \<lbrace>?B2 y\<rbrace> gets (armKSASIDTable \<circ> ksArchState) \<lbrace>\<lambda>asidTable. if asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some pool then ?Q4 y asidTable else invs'\<rbrace>
 4. \<lbrace>?Q1\<rbrace> assert (asid && mask local.asid_low_bits = 0) \<lbrace>?B2\<rbrace>
 5. \<And>s. invs' s \<Longrightarrow> ?Q1 s proof (prove)
goal (5 subgoals):
 1. \<And>asidTable poola. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some pool \<Longrightarrow> \<lbrace>?B5 () 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>r s. invs' s \<and> asidTable = armKSASIDTable (ksArchState s)\<rbrace>
 2. \<And>y asidTable. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some pool \<Longrightarrow> \<lbrace>?Q4 y asidTable\<rbrace> liftM (inv asidpool.ASIDPool) (getObject pool) \<lbrace>?B5 y asidTable\<rbrace>
 3. \<And>y. \<lbrace>?B2 y\<rbrace> gets (armKSASIDTable \<circ> ksArchState) \<lbrace>\<lambda>asidTable. if asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some pool then ?Q4 y asidTable else invs'\<rbrace>
 4. \<lbrace>?Q1\<rbrace> assert (asid && mask local.asid_low_bits = 0) \<lbrace>?B2\<rbrace>
 5. \<And>s. invs' s \<Longrightarrow> ?Q1 s proof (prove)
goal:
No subgoals!