theory Retype_DP

lemma lookup_cap_rvu':
"\<lbrace>\<lambda>s. (\<forall>c. reset_cap_asid c = reset_cap_asid cap' \<longrightarrow> Q c 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_cap thread cap_ptr
   \<lbrace>Q\<rbrace>, \<lbrace>Q'\<rbrace> " apply (clarsimp simp: lookup_cap_def) apply (wp lookup_slot_rvu [where cnode_cap=cnode_cap] get_cap_rv) apply (clarsimp) apply safe apply (clarsimp simp: user_pointer_at_def sep_conj_assoc Let_unfold) apply (sep_solve) apply clarsimp apply (sep_solve) 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 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_cap 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 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 slot <- lookup_slot thread cap_ptr;
liftE (get_cap slot)
odE \<lbrace>Q\<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 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> (cdl.lift ((cap_object cnode_cap, offset cap_ptr ?r4) \<mapsto>c ?cap3 (cap_object cnode_cap, offset cap_ptr ?r4) \<and>* ?R3 (cap_object cnode_cap, offset cap_ptr ?r4)) s \<and> (\<forall>c. reset_cap_asid c = reset_cap_asid (?cap3 (cap_object cnode_cap, offset cap_ptr ?r4)) \<longrightarrow> Q c s)) \<and> cdl.lift ((thread, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* \<box> (?r4, word_bits) : cnode_cap cap_ptr \<mapsto>u ?cap'4 \<and>* ?R4) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<forall>c. reset_cap_asid c = reset_cap_asid cap' \<longrightarrow> Q c 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\<rbrakk> \<Longrightarrow> cdl.lift ((cap_object cnode_cap, offset cap_ptr ?r4) \<mapsto>c ?cap3 (cap_object cnode_cap, offset cap_ptr ?r4) \<and>* ?R3 (cap_object cnode_cap, offset cap_ptr ?r4)) s \<and> (\<forall>c. reset_cap_asid c = reset_cap_asid (?cap3 (cap_object cnode_cap, offset cap_ptr ?r4)) \<longrightarrow> Q c s) \<and> cdl.lift ((thread, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* \<box> (?r4, word_bits) : cnode_cap cap_ptr \<mapsto>u ?cap'4 \<and>* ?R4) s proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>\<forall>c. reset_cap_asid c = reset_cap_asid cap' \<longrightarrow> Q c 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\<rbrakk> \<Longrightarrow> cdl.lift ((cap_object cnode_cap, offset cap_ptr ?r4) \<mapsto>c ?cap3 (cap_object cnode_cap, offset cap_ptr ?r4) \<and>* ?R3 (cap_object cnode_cap, offset cap_ptr ?r4)) s
 2. \<And>s c. \<lbrakk>\<forall>c. reset_cap_asid c = reset_cap_asid cap' \<longrightarrow> Q c 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; reset_cap_asid c = reset_cap_asid (?cap3 (cap_object cnode_cap, offset cap_ptr ?r4))\<rbrakk> \<Longrightarrow> Q c s
 3. \<And>s. \<lbrakk>\<forall>c. reset_cap_asid c = reset_cap_asid cap' \<longrightarrow> Q c 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\<rbrakk> \<Longrightarrow> cdl.lift ((thread, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* \<box> (?r4, word_bits) : cnode_cap cap_ptr \<mapsto>u ?cap'4 \<and>* ?R4) s proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>\<forall>c. reset_cap_asid c = reset_cap_asid cap' \<longrightarrow> Q c s; one_lvl_lookup cnode_cap word_bits r; guard_equal cnode_cap cap_ptr word_bits; is_cnode_cap cnode_cap; cdl.lift ((thread, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* cap_object cnode_cap \<mapsto>f CNode (empty_cnode r) \<and>* (cap_object cnode_cap, offset cap_ptr r) \<mapsto>c cap' \<and>* R) s\<rbrakk> \<Longrightarrow> cdl.lift ((cap_object cnode_cap, offset cap_ptr ?r4) \<mapsto>c ?cap3 (cap_object cnode_cap, offset cap_ptr ?r4) \<and>* ?R3 (cap_object cnode_cap, offset cap_ptr ?r4)) s
 2. \<And>s c. \<lbrakk>\<forall>c. reset_cap_asid c = reset_cap_asid cap' \<longrightarrow> Q c 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; reset_cap_asid c = reset_cap_asid (?cap3 (cap_object cnode_cap, offset cap_ptr ?r4))\<rbrakk> \<Longrightarrow> Q c s
 3. \<And>s. \<lbrakk>\<forall>c. reset_cap_asid c = reset_cap_asid cap' \<longrightarrow> Q c 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\<rbrakk> \<Longrightarrow> cdl.lift ((thread, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* \<box> (?r4, word_bits) : cnode_cap cap_ptr \<mapsto>u ?cap'4 \<and>* ?R4) s proof (prove)
goal (2 subgoals):
 1. \<And>s c. \<lbrakk>\<forall>c. reset_cap_asid c = reset_cap_asid cap' \<longrightarrow> Q c 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; reset_cap_asid c = reset_cap_asid cap'\<rbrakk> \<Longrightarrow> Q c s
 2. \<And>s. \<lbrakk>\<forall>c. reset_cap_asid c = reset_cap_asid cap' \<longrightarrow> Q c 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\<rbrakk> \<Longrightarrow> cdl.lift ((thread, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* \<box> (r, word_bits) : cnode_cap cap_ptr \<mapsto>u ?cap'4 \<and>* ?R4) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<forall>c. reset_cap_asid c = reset_cap_asid cap' \<longrightarrow> Q c 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\<rbrakk> \<Longrightarrow> cdl.lift ((thread, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* \<box> (r, word_bits) : cnode_cap cap_ptr \<mapsto>u ?cap'4 \<and>* ?R4) s proof (prove)
goal:
No subgoals!