theory Arch_DP

lemma invoke_page_wp:
  "pinv = PageMap (FrameCap dev frame_ptr rights n fake asid)
  (FrameCap False frame_ptr rights' n fake' asid') ref x
  \<Longrightarrow>\<lbrace><ref \<mapsto>c - \<and>* \<And>* map sep_any_map_c (invoke_page_map_slots (InvokePage pinv))
    \<and>* P (invoke_page_map_slots (InvokePage pinv)) >\<rbrace>
    invoke_page pinv
   \<lbrace>\<lambda>r. <\<And>* map (\<lambda>ptr. ptr\<mapsto>c (FrameCap False frame_ptr rights' n fake' asid'))
          (invoke_page_map_slots (InvokePage pinv))
       \<and>* ref \<mapsto>c (FrameCap dev frame_ptr rights n fake asid) \<and>* P (invoke_page_map_slots (InvokePage pinv))>\<rbrace>" apply (simp add:invoke_page_def) apply wp apply (rule sep_lifted.mapM_x_sep_inv
    [where lft = sep_state_projection and I' = \<top>,simplified]) apply (simp add:swp_def) apply (rule hoare_pre) apply (rule set_cap_wp) apply simp apply (wp sep_wp: set_cap_wp, sep_solve) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pinv = PageMap (FrameCap dev frame_ptr rights n fake asid) (FrameCap False frame_ptr rights' n fake' asid') ref x \<Longrightarrow> \<lbrace>cdl.lift (ref \<mapsto>c - \<and>* \<And>* map sep_any_map_c (case InvokePage pinv of InvokePage (PageMap cap cap' ref xs) \<Rightarrow> xs) \<and>* P (case InvokePage pinv of InvokePage (PageMap cap cap' ref xs) \<Rightarrow> xs))\<rbrace> invoke_page pinv \<lbrace>\<lambda>r. cdl.lift (\<And>* map (\<lambda>ptr. ptr \<mapsto>c FrameCap False frame_ptr rights' n fake' asid') (case InvokePage pinv of InvokePage (PageMap cap cap' ref xs) \<Rightarrow> xs) \<and>* ref \<mapsto>c FrameCap dev frame_ptr rights n fake asid \<and>* P (case InvokePage pinv of InvokePage (PageMap cap cap' ref xs) \<Rightarrow> xs))\<rbrace> proof (prove)
goal (1 subgoal):
 1. pinv = PageMap (FrameCap dev frame_ptr rights n fake asid) (FrameCap False frame_ptr rights' n fake' asid') ref x \<Longrightarrow> \<lbrace>cdl.lift (ref \<mapsto>c - \<and>* \<And>* map sep_any_map_c x \<and>* P x)\<rbrace> do y <- set_cap ref (FrameCap dev frame_ptr rights n fake asid);
mapM_x (swp set_cap (FrameCap False frame_ptr rights' n fake' asid')) x
od \<lbrace>\<lambda>r. cdl.lift (\<And>* map (\<lambda>ptr. ptr \<mapsto>c FrameCap False frame_ptr rights' n fake' asid') x \<and>* ref \<mapsto>c FrameCap dev frame_ptr rights n fake asid \<and>* P x)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>y. pinv = PageMap (FrameCap dev frame_ptr rights n fake asid) (FrameCap False frame_ptr rights' n fake' asid') ref x \<Longrightarrow> \<lbrace>?B3 y\<rbrace> mapM_x (swp set_cap (FrameCap False frame_ptr rights' n fake' asid')) x \<lbrace>\<lambda>r. cdl.lift (\<And>* map (\<lambda>ptr. ptr \<mapsto>c FrameCap False frame_ptr rights' n fake' asid') x \<and>* ref \<mapsto>c FrameCap dev frame_ptr rights n fake asid \<and>* P x)\<rbrace>
 2. pinv = PageMap (FrameCap dev frame_ptr rights n fake asid) (FrameCap False frame_ptr rights' n fake' asid') ref x \<Longrightarrow> \<lbrace>?Q2\<rbrace> set_cap ref (FrameCap dev frame_ptr rights n fake asid) \<lbrace>?B3\<rbrace>
 3. \<And>s. \<lbrakk>pinv = PageMap (FrameCap dev frame_ptr rights n fake asid) (FrameCap False frame_ptr rights' n fake' asid') ref x; cdl.lift (ref \<mapsto>c - \<and>* \<And>* map sep_any_map_c x \<and>* P x) s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (3 subgoals):
 1. \<And>y R xa. \<lbrakk>pinv = PageMap (FrameCap dev frame_ptr rights n fake asid) (FrameCap False frame_ptr rights' n fake' asid') ref x; xa \<in> set x\<rbrakk> \<Longrightarrow> \<lbrace>cdl.lift (?P4 y xa \<and>* ref \<mapsto>c FrameCap dev frame_ptr rights n fake asid \<and>* R)\<rbrace> swp set_cap (FrameCap False frame_ptr rights' n fake' asid') xa \<lbrace>\<lambda>r. cdl.lift (xa \<mapsto>c FrameCap False frame_ptr rights' n fake' asid' \<and>* ref \<mapsto>c FrameCap dev frame_ptr rights n fake asid \<and>* R)\<rbrace>
 2. pinv = PageMap (FrameCap dev frame_ptr rights n fake asid) (FrameCap False frame_ptr rights' n fake' asid') ref x \<Longrightarrow> \<lbrace>?Q2\<rbrace> set_cap ref (FrameCap dev frame_ptr rights n fake asid) \<lbrace>\<lambda>y. cdl.lift (\<And>* map (?P4 y) x \<and>* ref \<mapsto>c FrameCap dev frame_ptr rights n fake asid \<and>* P x)\<rbrace>
 3. \<And>s. \<lbrakk>pinv = PageMap (FrameCap dev frame_ptr rights n fake asid) (FrameCap False frame_ptr rights' n fake' asid') ref x; cdl.lift (ref \<mapsto>c - \<and>* \<And>* map sep_any_map_c x \<and>* P x) s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (3 subgoals):
 1. \<And>R xa. \<lbrakk>pinv = PageMap (FrameCap dev frame_ptr rights n fake asid) (FrameCap False frame_ptr rights' n fake' asid') ref x; xa \<in> set x\<rbrakk> \<Longrightarrow> \<lbrace>cdl.lift (?P4 () xa \<and>* ref \<mapsto>c FrameCap dev frame_ptr rights n fake asid \<and>* R)\<rbrace> set_cap xa (FrameCap False frame_ptr rights' n fake' asid') \<lbrace>\<lambda>r. cdl.lift (xa \<mapsto>c FrameCap False frame_ptr rights' n fake' asid' \<and>* ref \<mapsto>c FrameCap dev frame_ptr rights n fake asid \<and>* R)\<rbrace>
 2. pinv = PageMap (FrameCap dev frame_ptr rights n fake asid) (FrameCap False frame_ptr rights' n fake' asid') ref x \<Longrightarrow> \<lbrace>?Q2\<rbrace> set_cap ref (FrameCap dev frame_ptr rights n fake asid) \<lbrace>\<lambda>y. cdl.lift (\<And>* map (?P4 y) x \<and>* ref \<mapsto>c FrameCap dev frame_ptr rights n fake asid \<and>* P x)\<rbrace>
 3. \<And>s. \<lbrakk>pinv = PageMap (FrameCap dev frame_ptr rights n fake asid) (FrameCap False frame_ptr rights' n fake' asid') ref x; cdl.lift (ref \<mapsto>c - \<and>* \<And>* map sep_any_map_c x \<and>* P x) s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (4 subgoals):
 1. \<And>R xa. \<lbrakk>pinv = PageMap (FrameCap dev frame_ptr rights n fake asid) (FrameCap False frame_ptr rights' n fake' asid') ref x; xa \<in> set x\<rbrakk> \<Longrightarrow> \<lbrace>?Q6 R xa\<rbrace> set_cap xa (FrameCap False frame_ptr rights' n fake' asid') \<lbrace>\<lambda>r. cdl.lift (xa \<mapsto>c FrameCap False frame_ptr rights' n fake' asid' \<and>* ref \<mapsto>c FrameCap dev frame_ptr rights n fake asid \<and>* R)\<rbrace>
 2. \<And>R xa s. \<lbrakk>pinv = PageMap (FrameCap dev frame_ptr rights n fake asid) (FrameCap False frame_ptr rights' n fake' asid') ref x; xa \<in> set x; cdl.lift (?P4 () xa \<and>* ref \<mapsto>c FrameCap dev frame_ptr rights n fake asid \<and>* R) s\<rbrakk> \<Longrightarrow> ?Q6 R xa s
 3. pinv = PageMap (FrameCap dev frame_ptr rights n fake asid) (FrameCap False frame_ptr rights' n fake' asid') ref x \<Longrightarrow> \<lbrace>?Q2\<rbrace> set_cap ref (FrameCap dev frame_ptr rights n fake asid) \<lbrace>\<lambda>y. cdl.lift (\<And>* map (?P4 y) x \<and>* ref \<mapsto>c FrameCap dev frame_ptr rights n fake asid \<and>* P x)\<rbrace>
 4. \<And>s. \<lbrakk>pinv = PageMap (FrameCap dev frame_ptr rights n fake asid) (FrameCap False frame_ptr rights' n fake' asid') ref x; cdl.lift (ref \<mapsto>c - \<and>* \<And>* map sep_any_map_c x \<and>* P x) s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (3 subgoals):
 1. \<And>R xa s. \<lbrakk>pinv = PageMap (FrameCap dev frame_ptr rights n fake asid) (FrameCap False frame_ptr rights' n fake' asid') ref x; xa \<in> set x; cdl.lift (?P4 () xa \<and>* ref \<mapsto>c FrameCap dev frame_ptr rights n fake asid \<and>* R) s\<rbrakk> \<Longrightarrow> cdl.lift (xa \<mapsto>c - \<and>* ref \<mapsto>c FrameCap dev frame_ptr rights n fake asid \<and>* R) s
 2. pinv = PageMap (FrameCap dev frame_ptr rights n fake asid) (FrameCap False frame_ptr rights' n fake' asid') ref x \<Longrightarrow> \<lbrace>?Q2\<rbrace> set_cap ref (FrameCap dev frame_ptr rights n fake asid) \<lbrace>\<lambda>y. cdl.lift (\<And>* map (?P4 y) x \<and>* ref \<mapsto>c FrameCap dev frame_ptr rights n fake asid \<and>* P x)\<rbrace>
 3. \<And>s. \<lbrakk>pinv = PageMap (FrameCap dev frame_ptr rights n fake asid) (FrameCap False frame_ptr rights' n fake' asid') ref x; cdl.lift (ref \<mapsto>c - \<and>* \<And>* map sep_any_map_c x \<and>* P x) s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (2 subgoals):
 1. pinv = PageMap (FrameCap dev frame_ptr rights n fake asid) (FrameCap False frame_ptr rights' n fake' asid') ref x \<Longrightarrow> \<lbrace>?Q2\<rbrace> set_cap ref (FrameCap dev frame_ptr rights n fake asid) \<lbrace>\<lambda>y. cdl.lift (\<And>* map sep_any_map_c x \<and>* ref \<mapsto>c FrameCap dev frame_ptr rights n fake asid \<and>* P x)\<rbrace>
 2. \<And>s. \<lbrakk>pinv = PageMap (FrameCap dev frame_ptr rights n fake asid) (FrameCap False frame_ptr rights' n fake' asid') ref x; cdl.lift (ref \<mapsto>c - \<and>* \<And>* map sep_any_map_c x \<and>* P x) s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal:
No subgoals!