theory KHeap_DP

lemma lookup_cap_and_slot_rvu:
  "\<lbrace>\<lambda>s. (\<forall>c. reset_cap_asid c = reset_cap_asid cap' \<longrightarrow>
             Q (c, (cap_object cap, offset cap_ptr r) ) s) \<and>
    < (thread,tcb_cspace_slot) \<mapsto>c cap \<and>*
    \<box> (r, word_bits) : cap cap_ptr \<mapsto>u cap' \<and>* R> s\<rbrace>
     lookup_cap_and_slot thread cap_ptr
   \<lbrace>Q\<rbrace>, \<lbrace>Q'\<rbrace> " apply (clarsimp simp: lookup_cap_and_slot_def) apply (rule hoare_vcg_seqE)+ apply (rule returnOk_wp) apply (wp get_cap_rv) apply (rule hoare_pre, wp lookup_slot_rvu) apply (safe) apply (clarsimp simp: user_pointer_at_def Let_unfold sep.mult_assoc) apply sep_solve apply clarsimp apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<forall>c. reset_cap_asid c = reset_cap_asid cap' \<longrightarrow> Q (c, cap_object cap, offset cap_ptr r) s) \<and> cdl.lift ((thread, tcb_cspace_slot) \<mapsto>c cap \<and>* \<box> (r, word_bits) : cap cap_ptr \<mapsto>u cap' \<and>* R) s\<rbrace> lookup_cap_and_slot thread cap_ptr \<lbrace>Q\<rbrace>, \<lbrace>Q'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<forall>c. reset_cap_asid c = reset_cap_asid cap' \<longrightarrow> Q (c, cap_object cap, offset cap_ptr r) s) \<and> cdl.lift ((thread, tcb_cspace_slot) \<mapsto>c cap \<and>* \<box> (r, word_bits) : cap cap_ptr \<mapsto>u cap' \<and>* R) s\<rbrace> doE slot <- lookup_slot thread cap_ptr;
cap <- liftE (get_cap slot);
returnOk (cap, slot)
odE \<lbrace>Q\<rbrace>, \<lbrace>Q'\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>slot cap. \<lbrace>?B3 slot cap\<rbrace> returnOk (cap, slot) \<lbrace>Q\<rbrace>, \<lbrace>Q'\<rbrace>
 2. \<And>slot. \<lbrace>?B slot\<rbrace> liftE (get_cap slot) \<lbrace>?B3 slot\<rbrace>, \<lbrace>Q'\<rbrace>
 3. \<lbrace>\<lambda>s. (\<forall>c. reset_cap_asid c = reset_cap_asid cap' \<longrightarrow> Q (c, cap_object cap, offset cap_ptr r) s) \<and> cdl.lift ((thread, tcb_cspace_slot) \<mapsto>c cap \<and>* \<box> (r, word_bits) : cap cap_ptr \<mapsto>u cap' \<and>* R) s\<rbrace> lookup_slot thread cap_ptr \<lbrace>?B\<rbrace>, \<lbrace>Q'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>slot. \<lbrace>?B slot\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>cap. Q (cap, slot)\<rbrace>, \<lbrace>Q'\<rbrace>
 2. \<lbrace>\<lambda>s. (\<forall>c. reset_cap_asid c = reset_cap_asid cap' \<longrightarrow> Q (c, cap_object cap, offset cap_ptr r) s) \<and> cdl.lift ((thread, tcb_cspace_slot) \<mapsto>c cap \<and>* \<box> (r, word_bits) : cap cap_ptr \<mapsto>u cap' \<and>* R) s\<rbrace> lookup_slot thread cap_ptr \<lbrace>?B\<rbrace>, \<lbrace>Q'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<forall>c. reset_cap_asid c = reset_cap_asid cap' \<longrightarrow> Q (c, cap_object cap, offset cap_ptr r) s) \<and> cdl.lift ((thread, tcb_cspace_slot) \<mapsto>c cap \<and>* \<box> (r, word_bits) : cap cap_ptr \<mapsto>u cap' \<and>* R) s\<rbrace> lookup_slot thread cap_ptr \<lbrace>\<lambda>slot s. cdl.lift (slot \<mapsto>c ?cap9 slot \<and>* ?R9 slot) s \<and> (\<forall>c. reset_cap_asid c = reset_cap_asid (?cap9 slot) \<longrightarrow> Q (c, slot) s)\<rbrace>, \<lbrace>Q'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<forall>c. reset_cap_asid c = reset_cap_asid cap' \<longrightarrow> Q (c, cap_object cap, offset cap_ptr r) s) \<and> cdl.lift ((thread, tcb_cspace_slot) \<mapsto>c cap \<and>* \<box> (r, word_bits) : cap cap_ptr \<mapsto>u cap' \<and>* R) s \<Longrightarrow> (cdl.lift ((cap_object ?cnode_cap15, offset cap_ptr ?r15) \<mapsto>c ?cap9 (cap_object ?cnode_cap15, offset cap_ptr ?r15) \<and>* ?R9 (cap_object ?cnode_cap15, offset cap_ptr ?r15)) s \<and> (\<forall>c. reset_cap_asid c = reset_cap_asid (?cap9 (cap_object ?cnode_cap15, offset cap_ptr ?r15)) \<longrightarrow> Q (c, cap_object ?cnode_cap15, offset cap_ptr ?r15) s)) \<and> cdl.lift ((thread, tcb_cspace_slot) \<mapsto>c ?cnode_cap15 \<and>* \<box> (?r15, word_bits) : ?cnode_cap15 cap_ptr \<mapsto>u ?cap'15 \<and>* ?R15) s proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>\<forall>c. reset_cap_asid c = reset_cap_asid cap' \<longrightarrow> Q (c, cap_object cap, offset cap_ptr r) s; cdl.lift ((thread, tcb_cspace_slot) \<mapsto>c cap \<and>* \<box> (r, word_bits) : cap cap_ptr \<mapsto>u cap' \<and>* R) s\<rbrakk> \<Longrightarrow> cdl.lift ((cap_object ?cnode_cap15, offset cap_ptr ?r15) \<mapsto>c ?cap9 (cap_object ?cnode_cap15, offset cap_ptr ?r15) \<and>* ?R9 (cap_object ?cnode_cap15, offset cap_ptr ?r15)) s
 2. \<And>s c. \<lbrakk>\<forall>c. reset_cap_asid c = reset_cap_asid cap' \<longrightarrow> Q (c, cap_object cap, offset cap_ptr r) s; cdl.lift ((thread, tcb_cspace_slot) \<mapsto>c cap \<and>* \<box> (r, word_bits) : cap cap_ptr \<mapsto>u cap' \<and>* R) s; reset_cap_asid c = reset_cap_asid (?cap9 (cap_object ?cnode_cap15, offset cap_ptr ?r15))\<rbrakk> \<Longrightarrow> Q (c, cap_object ?cnode_cap15, offset cap_ptr ?r15) s
 3. \<And>s. \<lbrakk>\<forall>c. reset_cap_asid c = reset_cap_asid cap' \<longrightarrow> Q (c, cap_object cap, offset cap_ptr r) s; cdl.lift ((thread, tcb_cspace_slot) \<mapsto>c cap \<and>* \<box> (r, word_bits) : cap cap_ptr \<mapsto>u cap' \<and>* R) s\<rbrakk> \<Longrightarrow> cdl.lift ((thread, tcb_cspace_slot) \<mapsto>c ?cnode_cap15 \<and>* \<box> (?r15, word_bits) : ?cnode_cap15 cap_ptr \<mapsto>u ?cap'15 \<and>* ?R15) s proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>\<forall>c. reset_cap_asid c = reset_cap_asid cap' \<longrightarrow> Q (c, cap_object cap, offset cap_ptr r) s; one_lvl_lookup cap word_bits r; guard_equal cap cap_ptr word_bits; is_cnode_cap cap; cdl.lift ((thread, tcb_cspace_slot) \<mapsto>c cap \<and>* cap_object cap \<mapsto>f CNode (empty_cnode r) \<and>* (cap_object cap, offset cap_ptr r) \<mapsto>c cap' \<and>* R) s\<rbrakk> \<Longrightarrow> cdl.lift ((cap_object ?cnode_cap15, offset cap_ptr ?r15) \<mapsto>c ?cap9 (cap_object ?cnode_cap15, offset cap_ptr ?r15) \<and>* ?R9 (cap_object ?cnode_cap15, offset cap_ptr ?r15)) s
 2. \<And>s c. \<lbrakk>\<forall>c. reset_cap_asid c = reset_cap_asid cap' \<longrightarrow> Q (c, cap_object cap, offset cap_ptr r) s; cdl.lift ((thread, tcb_cspace_slot) \<mapsto>c cap \<and>* \<box> (r, word_bits) : cap cap_ptr \<mapsto>u cap' \<and>* R) s; reset_cap_asid c = reset_cap_asid (?cap9 (cap_object ?cnode_cap15, offset cap_ptr ?r15))\<rbrakk> \<Longrightarrow> Q (c, cap_object ?cnode_cap15, offset cap_ptr ?r15) s
 3. \<And>s. \<lbrakk>\<forall>c. reset_cap_asid c = reset_cap_asid cap' \<longrightarrow> Q (c, cap_object cap, offset cap_ptr r) s; cdl.lift ((thread, tcb_cspace_slot) \<mapsto>c cap \<and>* \<box> (r, word_bits) : cap cap_ptr \<mapsto>u cap' \<and>* R) s\<rbrakk> \<Longrightarrow> cdl.lift ((thread, tcb_cspace_slot) \<mapsto>c ?cnode_cap15 \<and>* \<box> (?r15, word_bits) : ?cnode_cap15 cap_ptr \<mapsto>u ?cap'15 \<and>* ?R15) s proof (prove)
goal (2 subgoals):
 1. \<And>s c. \<lbrakk>\<forall>c. reset_cap_asid c = reset_cap_asid cap' \<longrightarrow> Q (c, cap_object cap, offset cap_ptr r) s; cdl.lift ((thread, tcb_cspace_slot) \<mapsto>c cap \<and>* \<box> (r, word_bits) : cap cap_ptr \<mapsto>u cap' \<and>* R) s; reset_cap_asid c = reset_cap_asid cap'\<rbrakk> \<Longrightarrow> Q (c, cap_object cap, offset cap_ptr r) s
 2. \<And>s. \<lbrakk>\<forall>c. reset_cap_asid c = reset_cap_asid cap' \<longrightarrow> Q (c, cap_object cap, offset cap_ptr r) s; cdl.lift ((thread, tcb_cspace_slot) \<mapsto>c cap \<and>* \<box> (r, word_bits) : cap cap_ptr \<mapsto>u cap' \<and>* R) s\<rbrakk> \<Longrightarrow> cdl.lift ((thread, tcb_cspace_slot) \<mapsto>c cap \<and>* \<box> (r, word_bits) : cap cap_ptr \<mapsto>u ?cap'15 \<and>* ?R15) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<forall>c. reset_cap_asid c = reset_cap_asid cap' \<longrightarrow> Q (c, cap_object cap, offset cap_ptr r) s; cdl.lift ((thread, tcb_cspace_slot) \<mapsto>c cap \<and>* \<box> (r, word_bits) : cap cap_ptr \<mapsto>u cap' \<and>* R) s\<rbrakk> \<Longrightarrow> cdl.lift ((thread, tcb_cspace_slot) \<mapsto>c cap \<and>* \<box> (r, word_bits) : cap cap_ptr \<mapsto>u ?cap'15 \<and>* ?R15) s proof (prove)
goal:
No subgoals!