theory FinalCaps

lemma max_free_index_update_intra_label_cap[wp]:
  "\<lbrace>intra_label_cap aag slot and cte_wp_at ((=) cap) slot\<rbrace>
   set_cap (max_free_index_update cap) slot
   \<lbrace>\<lambda>rv s. intra_label_cap aag slot s\<rbrace>" unfolding set_cap_def apply (wp set_object_wp get_object_wp | wpc| simp add: split_def)+ apply (clarsimp simp: intra_label_cap_def cap_points_to_label_def) apply (fastforce elim: cte_wp_atE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>intra_label_cap aag slot and cte_wp_at ((=) cap) slot\<rbrace> set_cap (max_free_index_update cap) slot \<lbrace>\<lambda>rv. intra_label_cap aag slot\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>intra_label_cap aag slot and cte_wp_at ((=) cap) slot\<rbrace> case slot of (oref, cref) \<Rightarrow> do obj <- get_object oref;
(case obj of CNode sz cn \<Rightarrow> if cref \<in> dom cn \<and> well_formed_cnode_n sz cn then return $ CNode sz $ cn(cref \<mapsto> max_free_index_update cap) else fail | TCB tcb \<Rightarrow> if cref = tcb_cnode_index 0 then return $ TCB $ tcb\<lparr>tcb_ctable := max_free_index_update cap\<rparr> else if cref = tcb_cnode_index 1 then return $ TCB $ tcb\<lparr>tcb_vtable := max_free_index_update cap\<rparr> else if cref = tcb_cnode_index 2 then return $ TCB $ tcb\<lparr>tcb_reply := max_free_index_update cap\<rparr> else if cref = tcb_cnode_index 3 then return $ TCB $ tcb\<lparr>tcb_caller := max_free_index_update cap\<rparr> else if cref = tcb_cnode_index 4 then return $ TCB $ tcb\<lparr>tcb_ipcframe := max_free_index_update cap\<rparr> else fail | _ \<Rightarrow> fail) >>= set_object oref
od \<lbrace>\<lambda>rv. intra_label_cap aag slot\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. intra_label_cap aag slot s \<and> cte_wp_at ((=) cap) slot s \<Longrightarrow> \<forall>x xa. slot = (x, xa) \<longrightarrow> (\<forall>ko. ko_at ko x s \<longrightarrow> (\<forall>xb xc. ko = CNode xb xc \<longrightarrow> xa \<in> dom xc \<and> well_formed_cnode_n xb xc \<longrightarrow> intra_label_cap aag (x, xa) (s\<lparr>kheap := (kheap s)(x \<mapsto> CNode xb (\<lambda>a. if a = xa then Some (max_free_index_update cap) else xc a))\<rparr>)) \<and> (\<forall>xb. ko = TCB xb \<longrightarrow> (xa = tcb_cnode_index 0 \<longrightarrow> intra_label_cap aag (x, tcb_cnode_index 0) (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (xb\<lparr>tcb_ctable := max_free_index_update cap\<rparr>))\<rparr>)) \<and> (xa \<noteq> tcb_cnode_index 0 \<longrightarrow> (xa = tcb_cnode_index (Suc 0) \<longrightarrow> intra_label_cap aag (x, tcb_cnode_index (Suc 0)) (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (xb\<lparr>tcb_vtable := max_free_index_update cap\<rparr>))\<rparr>)) \<and> (xa \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> (xa = tcb_cnode_index 2 \<longrightarrow> intra_label_cap aag (x, tcb_cnode_index 2) (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (xb\<lparr>tcb_reply := max_free_index_update cap\<rparr>))\<rparr>)) \<and> (xa \<noteq> tcb_cnode_index 2 \<longrightarrow> (xa = tcb_cnode_index 3 \<longrightarrow> intra_label_cap aag (x, tcb_cnode_index 3) (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (xb\<lparr>tcb_caller := max_free_index_update cap\<rparr>))\<rparr>)) \<and> (xa \<noteq> tcb_cnode_index 3 \<longrightarrow> xa = tcb_cnode_index 4 \<longrightarrow> intra_label_cap aag (x, tcb_cnode_index 4) (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (xb\<lparr>tcb_ipcframe := max_free_index_update cap\<rparr>))\<rparr>))))))) proof (prove)
goal (1 subgoal):
 1. \<And>s x xa ko. \<lbrakk>\<forall>cap. cte_wp_at ((=) cap) (x, xa) s \<longrightarrow> (\<forall>xa\<in>obj_refs cap. pasObjectAbs aag xa = pasObjectAbs aag x) \<and> (\<forall>xa\<in>cap_irqs cap. pasIRQAbs aag xa = pasObjectAbs aag x); cte_wp_at ((=) cap) (x, xa) s; slot = (x, xa); ko_at ko x s\<rbrakk> \<Longrightarrow> (\<forall>xb xc. ko = CNode xb xc \<longrightarrow> xa \<in> dom xc \<and> well_formed_cnode_n xb xc \<longrightarrow> (\<forall>capa. cte_wp_at ((=) capa) (x, xa) (s\<lparr>kheap := (kheap s)(x \<mapsto> CNode xb (\<lambda>a. if a = xa then Some (max_free_index_update cap) else xc a))\<rparr>) \<longrightarrow> (\<forall>xa\<in>obj_refs capa. pasObjectAbs aag xa = pasObjectAbs aag x) \<and> (\<forall>xa\<in>cap_irqs capa. pasIRQAbs aag xa = pasObjectAbs aag x))) \<and> (\<forall>xb. ko = TCB xb \<longrightarrow> (xa = tcb_cnode_index 0 \<longrightarrow> (\<forall>capa. cte_wp_at ((=) capa) (x, tcb_cnode_index 0) (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (xb\<lparr>tcb_ctable := max_free_index_update cap\<rparr>))\<rparr>) \<longrightarrow> (\<forall>xa\<in>obj_refs capa. pasObjectAbs aag xa = pasObjectAbs aag x) \<and> (\<forall>xa\<in>cap_irqs capa. pasIRQAbs aag xa = pasObjectAbs aag x))) \<and> (xa \<noteq> tcb_cnode_index 0 \<longrightarrow> (xa = tcb_cnode_index (Suc 0) \<longrightarrow> (\<forall>capa. cte_wp_at ((=) capa) (x, tcb_cnode_index (Suc 0)) (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (xb\<lparr>tcb_vtable := max_free_index_update cap\<rparr>))\<rparr>) \<longrightarrow> (\<forall>xa\<in>obj_refs capa. pasObjectAbs aag xa = pasObjectAbs aag x) \<and> (\<forall>xa\<in>cap_irqs capa. pasIRQAbs aag xa = pasObjectAbs aag x))) \<and> (xa \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> (xa = tcb_cnode_index 2 \<longrightarrow> (\<forall>capa. cte_wp_at ((=) capa) (x, tcb_cnode_index 2) (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (xb\<lparr>tcb_reply := max_free_index_update cap\<rparr>))\<rparr>) \<longrightarrow> (\<forall>xa\<in>obj_refs capa. pasObjectAbs aag xa = pasObjectAbs aag x) \<and> (\<forall>xa\<in>cap_irqs capa. pasIRQAbs aag xa = pasObjectAbs aag x))) \<and> (xa \<noteq> tcb_cnode_index 2 \<longrightarrow> (xa = tcb_cnode_index 3 \<longrightarrow> (\<forall>capa. cte_wp_at ((=) capa) (x, tcb_cnode_index 3) (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (xb\<lparr>tcb_caller := max_free_index_update cap\<rparr>))\<rparr>) \<longrightarrow> (\<forall>xa\<in>obj_refs capa. pasObjectAbs aag xa = pasObjectAbs aag x) \<and> (\<forall>xa\<in>cap_irqs capa. pasIRQAbs aag xa = pasObjectAbs aag x))) \<and> (xa \<noteq> tcb_cnode_index 3 \<longrightarrow> xa = tcb_cnode_index 4 \<longrightarrow> (\<forall>capa. cte_wp_at ((=) capa) (x, tcb_cnode_index 4) (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (xb\<lparr>tcb_ipcframe := max_free_index_update cap\<rparr>))\<rparr>) \<longrightarrow> (\<forall>xa\<in>obj_refs capa. pasObjectAbs aag xa = pasObjectAbs aag x) \<and> (\<forall>xa\<in>cap_irqs capa. pasIRQAbs aag xa = pasObjectAbs aag x))))))) proof (prove)
goal:
No subgoals!