theory Arch_DP

lemma cdl_lookup_pt_slot_rv:
  "\<lbrace> K (R (p, unat ((ptr >> 12) && 0xFF))) and <(pd, unat (ptr >> 20)) \<mapsto>c PageTableCap p Fake None \<and>* (\<lambda>s. True)>\<rbrace>
  cdl_lookup_pt_slot pd ptr \<lbrace>\<lambda>r s. R r\<rbrace>,-" apply (rule validE_validE_R) apply (clarsimp simp : cdl_lookup_pt_slot_def) apply (clarsimp simp: validE_def valid_def bindE_def
    bind_def bind_assoc Nondet_Monad.lift_def) apply (case_tac a) apply (clarsimp simp:liftE_def bindE_def bind_def return_def) apply (clarsimp simp:liftE_def bindE_def bind_def return_def) apply (drule use_valid[OF _  cdl_get_pde_result_pt]) apply simp apply (clarsimp split:option.splits) apply (clarsimp simp: returnOk_def return_def) apply (clarsimp simp:throwError_def return_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>K (R (p, unat ((ptr >> 12) && 0xFF))) and cdl.lift ((pd, unat (ptr >> 20)) \<mapsto>c PageTableCap p Fake None \<and>* (\<lambda>s. True))\<rbrace> cdl_lookup_pt_slot pd ptr \<lbrace>\<lambda>r s. R r\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>K (R (p, unat ((ptr >> 12) && 0xFF))) and cdl.lift ((pd, unat (ptr >> 20)) \<mapsto>c PageTableCap p Fake None \<and>* (\<lambda>s. True))\<rbrace> cdl_lookup_pt_slot pd ptr \<lbrace>\<lambda>r s. R r\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>y. R (p, unat ((ptr >> 12) && 0xFF))) and cdl.lift ((pd, unat (ptr >> 20)) \<mapsto>c PageTableCap p Fake None \<and>* (\<lambda>s. True))\<rbrace> liftE (cdl_get_pde (cdl_lookup_pd_slot pd ptr)) >>=E case_cdl_cap throw (\<lambda>bool set1 set2. throw) (\<lambda>word1 word2 set. throw) (\<lambda>word1 word2 set. throw) (\<lambda>word set. throw) (\<lambda>word. throw) (\<lambda>word1 word2 nat1 nat2. throw) (\<lambda>word. throw) throw (\<lambda>word1 word2 bool1 bool2 bool3 bool4. throw) (\<lambda>word bool1 bool2. throw) (\<lambda>word. throw) throw throw throw (\<lambda>word. throw) (\<lambda>bool word set nat cdl_frame_cap_type option. throw) (\<lambda>ref cdl_frame_cap_type option. case cdl_frame_cap_type of Real \<Rightarrow> throw | Fake \<Rightarrow> case option of None \<Rightarrow> doE pt <- returnOk ref;
pt_index <- returnOk ((ptr >> 12) && 0xFF);
returnOk (pt, unat pt_index)
odE | Some a \<Rightarrow> throw) (\<lambda>word cdl_frame_cap_type option. throw) throw (\<lambda>word nat. throw) (\<lambda>word set. throw) throw (\<lambda>word. throw) (\<lambda>word. throw) (\<lambda>word. throw) (\<lambda>word. throw) \<lbrace>\<lambda>r s. R r\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b aa ba. \<lbrakk>(a, b) \<in> fst (liftE (cdl_get_pde (cdl_lookup_pd_slot pd ptr)) s); (aa, ba) \<in> fst ((case a of Inl e \<Rightarrow> throwError e | Inr (PageTableCap ref Real option) \<Rightarrow> throw | Inr (PageTableCap ref Fake None) \<Rightarrow> doE pt <- returnOk ref;
pt_index <- returnOk ((ptr >> 12) && 0xFF);
returnOk (pt, unat pt_index)
odE | Inr (PageTableCap ref Fake (Some a)) \<Rightarrow> throw | Inr _ \<Rightarrow> throw) b); R (p, unat ((ptr >> 12) && 0xFF)); cdl.lift ((pd, unat (ptr >> 20)) \<mapsto>c PageTableCap p Fake None \<and>* (\<lambda>s. True)) s\<rbrakk> \<Longrightarrow> case aa of Inl e \<Rightarrow> True | Inr x \<Rightarrow> R x proof (prove)
goal (2 subgoals):
 1. \<And>s a b aa ba ab. \<lbrakk>(a, b) \<in> fst (liftE (cdl_get_pde (cdl_lookup_pd_slot pd ptr)) s); (aa, ba) \<in> fst ((case a of Inl e \<Rightarrow> throwError e | Inr (PageTableCap ref Real option) \<Rightarrow> throw | Inr (PageTableCap ref Fake None) \<Rightarrow> doE pt <- returnOk ref;
pt_index <- returnOk ((ptr >> 12) && 0xFF);
returnOk (pt, unat pt_index)
odE | Inr (PageTableCap ref Fake (Some a)) \<Rightarrow> throw | Inr _ \<Rightarrow> throw) b); R (p, unat ((ptr >> 12) && 0xFF)); cdl.lift ((pd, unat (ptr >> 20)) \<mapsto>c PageTableCap p Fake None \<and>* (\<lambda>s. True)) s; a = Inl ab\<rbrakk> \<Longrightarrow> case aa of Inl e \<Rightarrow> True | Inr x \<Rightarrow> R x
 2. \<And>s a b aa ba bb. \<lbrakk>(a, b) \<in> fst (liftE (cdl_get_pde (cdl_lookup_pd_slot pd ptr)) s); (aa, ba) \<in> fst ((case a of Inl e \<Rightarrow> throwError e | Inr (PageTableCap ref Real option) \<Rightarrow> throw | Inr (PageTableCap ref Fake None) \<Rightarrow> doE pt <- returnOk ref;
pt_index <- returnOk ((ptr >> 12) && 0xFF);
returnOk (pt, unat pt_index)
odE | Inr (PageTableCap ref Fake (Some a)) \<Rightarrow> throw | Inr _ \<Rightarrow> throw) b); R (p, unat ((ptr >> 12) && 0xFF)); cdl.lift ((pd, unat (ptr >> 20)) \<mapsto>c PageTableCap p Fake None \<and>* (\<lambda>s. True)) s; a = Inr bb\<rbrakk> \<Longrightarrow> case aa of Inl e \<Rightarrow> True | Inr x \<Rightarrow> R x proof (prove)
goal (1 subgoal):
 1. \<And>s a b aa ba bb. \<lbrakk>(a, b) \<in> fst (liftE (cdl_get_pde (cdl_lookup_pd_slot pd ptr)) s); (aa, ba) \<in> fst ((case a of Inl e \<Rightarrow> throwError e | Inr (PageTableCap ref Real option) \<Rightarrow> throw | Inr (PageTableCap ref Fake None) \<Rightarrow> doE pt <- returnOk ref;
pt_index <- returnOk ((ptr >> 12) && 0xFF);
returnOk (pt, unat pt_index)
odE | Inr (PageTableCap ref Fake (Some a)) \<Rightarrow> throw | Inr _ \<Rightarrow> throw) b); R (p, unat ((ptr >> 12) && 0xFF)); cdl.lift ((pd, unat (ptr >> 20)) \<mapsto>c PageTableCap p Fake None \<and>* (\<lambda>s. True)) s; a = Inr bb\<rbrakk> \<Longrightarrow> case aa of Inl e \<Rightarrow> True | Inr x \<Rightarrow> R x proof (prove)
goal (1 subgoal):
 1. \<And>s b aa ba a. \<lbrakk>(aa, ba) \<in> fst ((case a of PageTableCap ref Real option \<Rightarrow> throw | PageTableCap ref Fake None \<Rightarrow> doE pt <- returnOk ref;
pt_index <- returnOk ((ptr >> 12) && 0xFF);
returnOk (pt, unat pt_index)
odE | PageTableCap ref Fake (Some a) \<Rightarrow> throw | _ \<Rightarrow> throw) b); R (p, unat ((ptr >> 12) && 0xFF)); cdl.lift ((pd, unat (ptr >> 20)) \<mapsto>c PageTableCap p Fake None \<and>* (\<lambda>s. True)) s; (a, b) \<in> fst (cdl_get_pde (cdl_lookup_pd_slot pd ptr) s)\<rbrakk> \<Longrightarrow> case aa of Inl e \<Rightarrow> True | Inr x \<Rightarrow> R x proof (prove)
goal (2 subgoals):
 1. \<And>s b aa ba a. \<lbrakk>(aa, ba) \<in> fst ((case a of PageTableCap ref Real option \<Rightarrow> throw | PageTableCap ref Fake None \<Rightarrow> doE pt <- returnOk ref;
pt_index <- returnOk ((ptr >> 12) && 0xFF);
returnOk (pt, unat pt_index)
odE | PageTableCap ref Fake (Some a) \<Rightarrow> throw | _ \<Rightarrow> throw) b); R (p, unat ((ptr >> 12) && 0xFF)); cdl.lift ((pd, unat (ptr >> 20)) \<mapsto>c PageTableCap p Fake None \<and>* (\<lambda>s. True)) s\<rbrakk> \<Longrightarrow> cdl.lift ((pd, unat (ptr >> 20)) \<mapsto>c PageTableCap (?p28 s b aa ba a) (?b28 s b aa ba a) None \<and>* (\<lambda>s. True)) s
 2. \<And>s b aa ba a. \<lbrakk>(aa, ba) \<in> fst ((case a of PageTableCap ref Real option \<Rightarrow> throw | PageTableCap ref Fake None \<Rightarrow> doE pt <- returnOk ref;
pt_index <- returnOk ((ptr >> 12) && 0xFF);
returnOk (pt, unat pt_index)
odE | PageTableCap ref Fake (Some a) \<Rightarrow> throw | _ \<Rightarrow> throw) b); R (p, unat ((ptr >> 12) && 0xFF)); cdl.lift ((pd, unat (ptr >> 20)) \<mapsto>c PageTableCap p Fake None \<and>* (\<lambda>s. True)) s; \<exists>asid. a = PageTableCap (?p28 s b aa ba a) (?b28 s b aa ba a) asid\<rbrakk> \<Longrightarrow> case aa of Inl e \<Rightarrow> True | Inr x \<Rightarrow> R x proof (prove)
goal (1 subgoal):
 1. \<And>s b aa ba a. \<lbrakk>(aa, ba) \<in> fst ((case a of PageTableCap ref Real option \<Rightarrow> throw | PageTableCap ref Fake None \<Rightarrow> doE pt <- returnOk ref;
pt_index <- returnOk ((ptr >> 12) && 0xFF);
returnOk (pt, unat pt_index)
odE | PageTableCap ref Fake (Some a) \<Rightarrow> throw | _ \<Rightarrow> throw) b); R (p, unat ((ptr >> 12) && 0xFF)); cdl.lift ((pd, unat (ptr >> 20)) \<mapsto>c PageTableCap p Fake None \<and>* (\<lambda>s. True)) s; \<exists>asid. a = PageTableCap p Fake asid\<rbrakk> \<Longrightarrow> case aa of Inl e \<Rightarrow> True | Inr x \<Rightarrow> R x proof (prove)
goal (2 subgoals):
 1. \<And>s b aa ba. \<lbrakk>R (p, unat ((ptr >> 12) && 0xFF)); cdl.lift ((pd, unat (ptr >> 20)) \<mapsto>c PageTableCap p Fake None \<and>* (\<lambda>s. True)) s; (aa, ba) \<in> fst (returnOk (p, unat ((ptr >> 12) && 0xFF)) b)\<rbrakk> \<Longrightarrow> case aa of Inl e \<Rightarrow> True | Inr x \<Rightarrow> R x
 2. \<And>s b aa ba asid x2. \<lbrakk>R (p, unat ((ptr >> 12) && 0xFF)); cdl.lift ((pd, unat (ptr >> 20)) \<mapsto>c PageTableCap p Fake None \<and>* (\<lambda>s. True)) s; asid = Some x2; (aa, ba) \<in> fst (throw b)\<rbrakk> \<Longrightarrow> case aa of Inl e \<Rightarrow> True | Inr x \<Rightarrow> R x proof (prove)
goal (1 subgoal):
 1. \<And>s b aa ba asid x2. \<lbrakk>R (p, unat ((ptr >> 12) && 0xFF)); cdl.lift ((pd, unat (ptr >> 20)) \<mapsto>c PageTableCap p Fake None \<and>* (\<lambda>s. True)) s; asid = Some x2; (aa, ba) \<in> fst (throw b)\<rbrakk> \<Longrightarrow> case aa of Inl e \<Rightarrow> True | Inr x \<Rightarrow> R x proof (prove)
goal:
No subgoals!