theory KHeap_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>\<lambda>_ _. False\<rbrace>" apply (clarsimp simp: lookup_cap_def) using hoare_vcg_prop[wp del] 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>\<lambda>_ _. False\<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>\<lambda>_ _. False\<rbrace> proof (prove)
using this:
\<lbrace>\<lambda>s. ?P\<rbrace> ?f \<lbrace>\<lambda>rv s. ?P\<rbrace>

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>\<lambda>_ _. False\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>P f. \<lbrace>\<lambda>s. P\<rbrace> f \<lbrace>\<lambda>rv s. P\<rbrace>; (\<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\<rbrakk> \<Longrightarrow> (cdl.lift ((cap_object cnode_cap, offset cap_ptr ?r6) \<mapsto>c ?cap5 (cap_object cnode_cap, offset cap_ptr ?r6) \<and>* ?R5 (cap_object cnode_cap, offset cap_ptr ?r6)) s \<and> (\<forall>c. reset_cap_asid c = reset_cap_asid (?cap5 (cap_object cnode_cap, offset cap_ptr ?r6)) \<longrightarrow> Q c s)) \<and> cdl.lift ((thread, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* \<box> (?r6, word_bits) : cnode_cap cap_ptr \<mapsto>u ?cap'6 \<and>* ?R6) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>P f. \<lbrace>\<lambda>s. P\<rbrace> f \<lbrace>\<lambda>rv s. P\<rbrace>; \<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 ?r6) \<mapsto>c ?cap5 (cap_object cnode_cap, offset cap_ptr ?r6) \<and>* ?R5 (cap_object cnode_cap, offset cap_ptr ?r6)) s \<and> (\<forall>c. reset_cap_asid c = reset_cap_asid (?cap5 (cap_object cnode_cap, offset cap_ptr ?r6)) \<longrightarrow> Q c s) \<and> cdl.lift ((thread, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* \<box> (?r6, word_bits) : cnode_cap cap_ptr \<mapsto>u ?cap'6 \<and>* ?R6) s proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>\<And>P f. \<lbrace>\<lambda>s. P\<rbrace> f \<lbrace>\<lambda>rv s. P\<rbrace>; \<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 ?r6) \<mapsto>c ?cap5 (cap_object cnode_cap, offset cap_ptr ?r6) \<and>* ?R5 (cap_object cnode_cap, offset cap_ptr ?r6)) s
 2. \<And>s c. \<lbrakk>\<And>P f. \<lbrace>\<lambda>s. P\<rbrace> f \<lbrace>\<lambda>rv s. P\<rbrace>; \<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 (?cap5 (cap_object cnode_cap, offset cap_ptr ?r6))\<rbrakk> \<Longrightarrow> Q c s
 3. \<And>s. \<lbrakk>\<And>P f. \<lbrace>\<lambda>s. P\<rbrace> f \<lbrace>\<lambda>rv s. P\<rbrace>; \<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> (?r6, word_bits) : cnode_cap cap_ptr \<mapsto>u ?cap'6 \<and>* ?R6) s proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>\<And>P f. \<lbrace>\<lambda>s. P\<rbrace> f \<lbrace>\<lambda>rv s. P\<rbrace>; \<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 ?r6) \<mapsto>c ?cap5 (cap_object cnode_cap, offset cap_ptr ?r6) \<and>* ?R5 (cap_object cnode_cap, offset cap_ptr ?r6)) s
 2. \<And>s c. \<lbrakk>\<And>P f. \<lbrace>\<lambda>s. P\<rbrace> f \<lbrace>\<lambda>rv s. P\<rbrace>; \<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 (?cap5 (cap_object cnode_cap, offset cap_ptr ?r6))\<rbrakk> \<Longrightarrow> Q c s
 3. \<And>s. \<lbrakk>\<And>P f. \<lbrace>\<lambda>s. P\<rbrace> f \<lbrace>\<lambda>rv s. P\<rbrace>; \<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> (?r6, word_bits) : cnode_cap cap_ptr \<mapsto>u ?cap'6 \<and>* ?R6) s proof (prove)
goal (2 subgoals):
 1. \<And>s c. \<lbrakk>\<And>P f. \<lbrace>\<lambda>s. P\<rbrace> f \<lbrace>\<lambda>rv s. P\<rbrace>; \<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>\<And>P f. \<lbrace>\<lambda>s. P\<rbrace> f \<lbrace>\<lambda>rv s. P\<rbrace>; \<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'6 \<and>* ?R6) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>P f. \<lbrace>\<lambda>s. P\<rbrace> f \<lbrace>\<lambda>rv s. P\<rbrace>; \<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'6 \<and>* ?R6) s proof (prove)
goal:
No subgoals!