theory KHeap_DP

lemma lookup_slot_rvu:
  "\<lbrace>\<lambda>s. Q (cap_object cnode_cap, offset cap_ptr r) s \<and>
    < (thread,tcb_cspace_slot) \<mapsto>c cnode_cap \<and>*
    \<box> (r, word_bits) : cnode_cap cap_ptr \<mapsto>u cap' \<and>* R> s\<rbrace>
     lookup_slot thread cap_ptr
   \<lbrace>Q\<rbrace>, \<lbrace>Q'\<rbrace> " apply (clarsimp simp: lookup_slot_def gets_the_resolve_cap[symmetric] split_def) apply (rule hoare_vcg_seqE)+ apply (rule returnOk_wp) apply (rule resolve_cap_u_nf [where r=r]) apply (rule hoare_pre, wp) apply (clarsimp simp: mapu_dest_opt_cap) apply (sep_frule (direct) opt_cap_sep_imp ) apply (sep_frule (direct) user_pointer_at_cnode_cap) apply (clarsimp) apply (frule (1) reset_cap_asid_cnode_cap) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. Q (cap_object cnode_cap, offset cap_ptr r) s \<and> cdl.lift ((thread, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* \<box> (r, word_bits) : cnode_cap cap_ptr \<mapsto>u cap' \<and>* R) s\<rbrace> lookup_slot thread cap_ptr \<lbrace>Q\<rbrace>, \<lbrace>Q'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. Q (cap_object cnode_cap, offset cap_ptr r) s \<and> cdl.lift ((thread, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* \<box> (r, word_bits) : cnode_cap cap_ptr \<mapsto>u cap' \<and>* R) s\<rbrace> doE cspace_root <- liftE (get_cap (thread, tcb_cspace_slot));
p <- gets_the (resolve_cap cspace_root cap_ptr word_bits);
returnOk (fst p)
odE \<lbrace>Q\<rbrace>, \<lbrace>Q'\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>cspace_root p. \<lbrace>?B3 cspace_root p\<rbrace> returnOk (fst p) \<lbrace>Q\<rbrace>, \<lbrace>Q'\<rbrace>
 2. \<And>cspace_root. \<lbrace>?B cspace_root\<rbrace> gets_the (resolve_cap cspace_root cap_ptr word_bits) \<lbrace>?B3 cspace_root\<rbrace>, \<lbrace>Q'\<rbrace>
 3. \<lbrace>\<lambda>s. Q (cap_object cnode_cap, offset cap_ptr r) s \<and> cdl.lift ((thread, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* \<box> (r, word_bits) : cnode_cap cap_ptr \<mapsto>u cap' \<and>* R) s\<rbrace> liftE (get_cap (thread, tcb_cspace_slot)) \<lbrace>?B\<rbrace>, \<lbrace>Q'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>cspace_root. \<lbrace>?B cspace_root\<rbrace> gets_the (resolve_cap cspace_root cap_ptr word_bits) \<lbrace>\<lambda>p. Q (fst p)\<rbrace>, \<lbrace>Q'\<rbrace>
 2. \<lbrace>\<lambda>s. Q (cap_object cnode_cap, offset cap_ptr r) s \<and> cdl.lift ((thread, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* \<box> (r, word_bits) : cnode_cap cap_ptr \<mapsto>u cap' \<and>* R) s\<rbrace> liftE (get_cap (thread, tcb_cspace_slot)) \<lbrace>?B\<rbrace>, \<lbrace>Q'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. Q (cap_object cnode_cap, offset cap_ptr r) s \<and> cdl.lift ((thread, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* \<box> (r, word_bits) : cnode_cap cap_ptr \<mapsto>u cap' \<and>* R) s\<rbrace> liftE (get_cap (thread, tcb_cspace_slot)) \<lbrace>\<lambda>cspace_root s. Q (fst ((cap_object cspace_root, offset cap_ptr r), 0)) s \<and> cdl.lift (\<box> (r, word_bits) : cspace_root cap_ptr \<mapsto>u ?cap7 cspace_root \<and>* ?R7 cspace_root) s\<rbrace>, \<lbrace>Q'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. Q (cap_object cnode_cap, offset cap_ptr r) s \<and> cdl.lift ((thread, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* \<box> (r, word_bits) : cnode_cap cap_ptr \<mapsto>u cap' \<and>* R) s \<Longrightarrow> opt_cap (thread, tcb_cspace_slot) s \<noteq> None \<longrightarrow> Q (fst ((cap_object (the (opt_cap (thread, tcb_cspace_slot) s)), offset cap_ptr r), 0)) s \<and> cdl.lift (\<box> (r, word_bits) : the (opt_cap (thread, tcb_cspace_slot) s) cap_ptr \<mapsto>u ?cap7 (the (opt_cap (thread, tcb_cspace_slot) s)) \<and>* ?R7 (the (opt_cap (thread, tcb_cspace_slot) s))) s proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>Q (cap_object cnode_cap, offset cap_ptr r) s; cdl.lift ((thread, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* \<box> (r, word_bits) : cnode_cap cap_ptr \<mapsto>u cap' \<and>* R) s; opt_cap (thread, tcb_cspace_slot) s = Some y\<rbrakk> \<Longrightarrow> Q (cap_object y, offset cap_ptr r) s \<and> cdl.lift (\<box> (r, word_bits) : y cap_ptr \<mapsto>u ?cap7 y \<and>* ?R7 y) s proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>Q (cap_object cnode_cap, offset cap_ptr r) s; opt_cap (thread, tcb_cspace_slot) s = Some y; cdl.lift ((thread, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* \<box> (r, word_bits) : cnode_cap cap_ptr \<mapsto>u cap' \<and>* R) s; \<exists>cap'. opt_cap (thread, tcb_cspace_slot) s = Some cap' \<and> reset_cap_asid cap' = reset_cap_asid cnode_cap\<rbrakk> \<Longrightarrow> Q (cap_object y, offset cap_ptr r) s \<and> cdl.lift (\<box> (r, word_bits) : y cap_ptr \<mapsto>u ?cap7 y \<and>* ?R7 y) s proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>Q (cap_object cnode_cap, offset cap_ptr r) s; opt_cap (thread, tcb_cspace_slot) s = Some y; \<exists>cap'. opt_cap (thread, tcb_cspace_slot) s = Some cap' \<and> reset_cap_asid cap' = reset_cap_asid cnode_cap; cdl.lift (\<box> (r, word_bits) : cnode_cap cap_ptr \<mapsto>u cap' \<and>* (thread, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) s; is_cnode_cap cnode_cap\<rbrakk> \<Longrightarrow> Q (cap_object y, offset cap_ptr r) s \<and> cdl.lift (\<box> (r, word_bits) : y cap_ptr \<mapsto>u ?cap7 y \<and>* ?R7 y) s proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>Q (cap_object cnode_cap, offset cap_ptr r) s; opt_cap (thread, tcb_cspace_slot) s = Some y; reset_cap_asid y = reset_cap_asid cnode_cap; cdl.lift (\<box> (r, word_bits) : cnode_cap cap_ptr \<mapsto>u cap' \<and>* (thread, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) s; is_cnode_cap cnode_cap\<rbrakk> \<Longrightarrow> Q (cap_object y, offset cap_ptr r) s \<and> cdl.lift (\<box> (r, word_bits) : y cap_ptr \<mapsto>u ?cap7 y \<and>* ?R7 y) s proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>Q (cap_object cnode_cap, offset cap_ptr r) s; opt_cap (thread, tcb_cspace_slot) s = Some y; reset_cap_asid y = reset_cap_asid cnode_cap; cdl.lift (\<box> (r, word_bits) : cnode_cap cap_ptr \<mapsto>u cap' \<and>* (thread, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) s; is_cnode_cap cnode_cap; y = cnode_cap\<rbrakk> \<Longrightarrow> Q (cap_object y, offset cap_ptr r) s \<and> cdl.lift (\<box> (r, word_bits) : y cap_ptr \<mapsto>u ?cap7 y \<and>* ?R7 y) s proof (prove)
goal:
No subgoals!