kings-crown/FVELER_Isabelle huggingface dataset:
theory KHeap_DP

lemma lookup_slot_for_cnode_op_rvu':
     "\<lbrace>\<lambda>s. Q ((cap_object cnode_cap), offset cap_ptr r) s \<and> remaining_size \<le> word_bits
         \<and> 0 < remaining_size \<and>
         < \<box> (r, remaining_size): cnode_cap cap_ptr \<mapsto>u cap  \<and>* R> s \<rbrace>
      lookup_slot_for_cnode_op cnode_cap cap_ptr remaining_size
     \<lbrace>Q\<rbrace>,\<lbrace>Q'\<rbrace>" apply (clarsimp simp: lookup_slot_for_cnode_op_def gets_the_resolve_cap[symmetric] split_def fault_to_except_def) apply (wp resolve_cap_u_nf[where r=r and R=R and cap=cap] whenE_wp) apply (clarsimp simp add:user_pointer_at_def Let_def guard_equal_def
    cap_guard_reset_cap_asid one_lvl_lookup_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. Q (cap_object cnode_cap, offset cap_ptr r) s \<and> remaining_size \<le> word_bits \<and> 0 < remaining_size \<and> cdl.lift (\<box> (r, remaining_size) : cnode_cap cap_ptr \<mapsto>u cap \<and>* R) s\<rbrace> lookup_slot_for_cnode_op cnode_cap cap_ptr remaining_size \<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> remaining_size \<le> word_bits \<and> 0 < remaining_size \<and> cdl.lift (\<box> (r, remaining_size) : cnode_cap cap_ptr \<mapsto>u cap \<and>* R) s\<rbrace> doE y <- whenE (remaining_size = 0 \<or> word_bits < remaining_size) throw;
p <- gets_the (resolve_cap cnode_cap cap_ptr remaining_size) <handle2> (\<lambda>x. throw);
if snd p = 0 then returnOk (fst p) else throw
odE \<lbrace>Q\<rbrace>, \<lbrace>Q'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. Q (cap_object cnode_cap, offset cap_ptr r) s \<and> remaining_size \<le> word_bits \<and> 0 < remaining_size \<and> cdl.lift (\<box> (r, remaining_size) : cnode_cap cap_ptr \<mapsto>u cap \<and>* R) s \<Longrightarrow> (if remaining_size = 0 \<or> word_bits < remaining_size then \<lambda>s. Q' undefined s \<and> True else (\<lambda>s. ((snd ((cap_object cnode_cap, offset cap_ptr r), 0) = 0 \<longrightarrow> Q (fst ((cap_object cnode_cap, offset cap_ptr r), 0)) s) \<and> (snd ((cap_object cnode_cap, offset cap_ptr r), 0) \<noteq> 0 \<longrightarrow> Q' undefined s \<and> True)) \<and> cdl.lift (\<box> (r, remaining_size) : cnode_cap cap_ptr \<mapsto>u cap \<and>* R) s)) s proof (prove)
goal:
No subgoals!
theory KHeap_DP

lemma lookup_slot_for_cnode_op_rv_2:
  "\<lbrace>\<lambda>s. cap_object cnode_cap = c \<and> slot = offset cap_ptr r \<and>
    < c \<mapsto>f CNode (empty_cnode r)  \<and>* (c, slot) \<mapsto>c cap \<and>* R> s \<and>
    one_lvl_lookup cnode_cap remaining_size r\<rbrace>
      lookup_slot_for_cnode_op cnode_cap cap_ptr remaining_size
  \<lbrace>\<lambda>rv s. rv = (c,slot) \<and> < c \<mapsto>f CNode (empty_cnode r) \<and>* (c,slot) \<mapsto>c cap \<and>* R> s\<rbrace>,-" apply (wp lookup_slot_for_cnode_op_rv') apply (fastforce) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cap_object cnode_cap = c \<and> slot = offset cap_ptr r \<and> cdl.lift (c \<mapsto>f CNode (empty_cnode r) \<and>* (c, slot) \<mapsto>c cap \<and>* R) s \<and> one_lvl_lookup cnode_cap remaining_size r\<rbrace> lookup_slot_for_cnode_op cnode_cap cap_ptr remaining_size \<lbrace>\<lambda>rv s. rv = (c, slot) \<and> cdl.lift (c \<mapsto>f CNode (empty_cnode r) \<and>* (c, slot) \<mapsto>c cap \<and>* R) s\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>s. cap_object cnode_cap = c \<and> slot = offset cap_ptr r \<and> cdl.lift (c \<mapsto>f CNode (empty_cnode r) \<and>* (c, slot) \<mapsto>c cap \<and>* R) s \<and> one_lvl_lookup cnode_cap remaining_size r \<Longrightarrow> ((?c1, ?slot1) = (c, slot) \<and> cdl.lift (c \<mapsto>f CNode (empty_cnode r) \<and>* (c, slot) \<mapsto>c cap \<and>* R) s) \<and> cap_object cnode_cap = ?c1 \<and> ?slot1 = offset cap_ptr ?r1 \<and> cdl.lift (?c1 \<mapsto>f CNode (empty_cnode ?r1) \<and>* (?c1, ?slot1) \<mapsto>c ?cap1 \<and>* ?R1) s \<and> one_lvl_lookup cnode_cap remaining_size ?r1 proof (prove)
goal:
No subgoals!
theory KHeap_DP

lemma derive_cap_wp [wp]:
"\<lbrace>P\<rbrace> derive_cap slot cap  \<lbrace>\<lambda>_. P\<rbrace>" apply (clarsimp simp: derive_cap_def returnOk_def split: cdl_cap.splits) apply (safe) apply ((wp whenE_wp)|(clarsimp simp: ensure_no_children_def))+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> derive_cap slot cap \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. (\<forall>x21 x22 x23. cap = UntypedCap x21 x22 x23 \<longrightarrow> \<lbrace>P\<rbrace> doE y <- ensure_no_children slot;
return (Inr (UntypedCap x21 x22 x23))
odE \<lbrace>\<lambda>_. P\<rbrace>) \<and> (\<forall>x181 x182 x183. cap = PageTableCap x181 x182 x183 \<longrightarrow> \<lbrace>P\<rbrace> throw \<sqinter> return (Inr (PageTableCap x181 x182 x183)) \<lbrace>\<lambda>_. P\<rbrace>) \<and> (\<forall>x191 x192 x193. cap = PageDirectoryCap x191 x192 x193 \<longrightarrow> \<lbrace>P\<rbrace> throw \<sqinter> return (Inr (PageDirectoryCap x191 x192 x193)) \<lbrace>\<lambda>_. P\<rbrace>) proof (prove)
goal (3 subgoals):
 1. \<And>x21 x22 x23. cap = UntypedCap x21 x22 x23 \<Longrightarrow> \<lbrace>P\<rbrace> doE y <- ensure_no_children slot;
return (Inr (UntypedCap x21 x22 x23))
odE \<lbrace>\<lambda>_. P\<rbrace>
 2. \<And>x181 x182 x183. cap = PageTableCap x181 x182 x183 \<Longrightarrow> \<lbrace>P\<rbrace> throw \<sqinter> return (Inr (PageTableCap x181 x182 x183)) \<lbrace>\<lambda>_. P\<rbrace>
 3. \<And>x191 x192 x193. cap = PageDirectoryCap x191 x192 x193 \<Longrightarrow> \<lbrace>P\<rbrace> throw \<sqinter> return (Inr (PageDirectoryCap x191 x192 x193)) \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal:
No subgoals!
theory KHeap_DP

lemma derive_cap_wpE:
"\<lbrace>P\<rbrace> derive_cap slot cap \<lbrace>\<lambda>_.P\<rbrace>,\<lbrace>\<lambda>_.P\<rbrace>" apply (clarsimp simp: derive_cap_def) apply (case_tac cap, (wp whenE_wp |
                        simp add: ensure_no_children_def)+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> derive_cap slot cap \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> case cap of UntypedCap x xa xb \<Rightarrow> doE ensure_no_children slot;
returnOk cap
odE | ReplyCap x xa \<Rightarrow> returnOk NullCap | MasterReplyCap oref \<Rightarrow> returnOk NullCap | IrqControlCap \<Rightarrow> returnOk NullCap | FrameCap dev p r sz b x \<Rightarrow> returnOk (FrameCap dev p r sz b None) | PageTableCap x xa xb \<Rightarrow> throw \<sqinter> returnOk cap | PageDirectoryCap x xa xb \<Rightarrow> throw \<sqinter> returnOk cap | ZombieCap x \<Rightarrow> returnOk NullCap | _ \<Rightarrow> returnOk cap \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal:
No subgoals!
theory KHeap_DP

lemma derive_cap_wp2: "\<lbrace>P\<rbrace> derive_cap slot cap \<lbrace>\<lambda>rv s. if rv = NullCap then True else P s\<rbrace>, -" apply (rule hoare_post_imp_R) apply (wp (once) derive_cap_wpE) apply (clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> derive_cap slot cap \<lbrace>\<lambda>rv s. if rv = NullCap then True else P s\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>P\<rbrace> derive_cap slot cap \<lbrace>?Q'\<rbrace>, -
 2. \<And>rv s. ?Q' rv s \<Longrightarrow> if rv = NullCap then True else P s proof (prove)
goal (1 subgoal):
 1. \<And>rv s. P s \<Longrightarrow> if rv = NullCap then True else P s proof (prove)
goal:
No subgoals!
theory KHeap_DP

lemma ensure_empty_wpE [wp]: "\<lbrace>P\<rbrace>
     ensure_empty x
     \<lbrace> \<lambda>_. P \<rbrace>,\<lbrace>\<lambda>_. P\<rbrace>" apply (clarsimp simp: ensure_empty_def) apply (wp liftE_wp unlessE_wp) apply (clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> ensure_empty x \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> doE cap <- liftE (get_cap x);
unlessE (cap = NullCap) throw
odE \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P s \<Longrightarrow> opt_cap x s \<noteq> None \<longrightarrow> (if the (opt_cap x s) = NullCap then P else (\<lambda>s. P s \<and> True)) s proof (prove)
goal:
No subgoals!
theory KHeap_DP

lemma decode_cnode_copy_wp: "\<lbrace>P\<rbrace>
     decode_cnode_invocation target target_ref caps (CNodeCopyIntent dest_index dest_depth src_index src_depth rights)
     \<lbrace> \<lambda>_. P \<rbrace>,\<lbrace>\<lambda>_. P\<rbrace>" apply (clarsimp simp: decode_cnode_invocation_def split_def) apply (wp whenE_wp hoare_drop_imps | simp cong: if_cong)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> decode_cnode_invocation target target_ref caps (CNodeCopyIntent dest_index dest_depth src_index src_depth rights) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> doE p <- throw_on_none (get_index caps 0);
dest_slot <- lookup_slot_for_cnode_op target dest_index (unat dest_depth);
y <- ensure_empty dest_slot;
src_slot <- lookup_slot_for_cnode_op (fst p) src_index (unat src_depth);
src_cap <- liftE (get_cap src_slot);
cap <- derive_cap src_slot (update_cap_rights (cap_rights src_cap \<inter> rights) src_cap);
y <- whenE (cap = NullCap) throw;
returnOk (InsertCall cap src_slot dest_slot)
odE \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal:
No subgoals!
theory KHeap_DP

lemma ensure_empty_wp [wp]: "\<lbrace>P\<rbrace> ensure_empty slot \<lbrace>\<lambda>_. P\<rbrace>" by (clarsimp simp: ensure_empty_def,wp unlessE_wp,clarsimp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> ensure_empty slot \<lbrace>\<lambda>_. P\<rbrace>
theory KHeap_DP

lemma ensure_no_children_wp [wp]: "\<lbrace>P\<rbrace> ensure_no_children slot \<lbrace>\<lambda>_. P\<rbrace>" apply (clarsimp simp: ensure_no_children_def) apply (wp whenE_wp) apply (clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> ensure_no_children slot \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> doE c <- liftE (gets (has_children slot));
whenE c throw
odE \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P s \<Longrightarrow> (if has_children slot s then \<lambda>s. P s \<and> True else P) s proof (prove)
goal:
No subgoals!
theory KHeap_DP

lemma mapu_dest_opt_cap:
  "< \<box> (sz, r): cr ci \<mapsto>u cap \<and>* R> s
  \<Longrightarrow> \<exists>cap'. opt_cap (cap_object cr, offset ci sz) s = Some cap' \<and>
             reset_cap_asid cap' = reset_cap_asid cap" apply (clarsimp simp: user_pointer_at_def Let_unfold sep.mult_assoc) apply (sep_drule (direct) opt_cap_sep_imp) apply (clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cdl.lift (\<box> (sz, r) : cr ci \<mapsto>u cap \<and>* R) s \<Longrightarrow> \<exists>cap'. opt_cap (cap_object cr, offset ci sz) s = Some cap' \<and> reset_cap_asid cap' = reset_cap_asid cap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>one_lvl_lookup cr r sz; guard_equal cr ci r; is_cnode_cap cr; cdl.lift (cap_object cr \<mapsto>f CNode (empty_cnode sz) \<and>* (cap_object cr, offset ci sz) \<mapsto>c cap \<and>* R) s\<rbrakk> \<Longrightarrow> \<exists>cap'. opt_cap (cap_object cr, offset ci sz) s = Some cap' \<and> reset_cap_asid cap' = reset_cap_asid cap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>one_lvl_lookup cr r sz; guard_equal cr ci r; is_cnode_cap cr; \<exists>cap'. opt_cap (cap_object cr, offset ci sz) s = Some cap' \<and> reset_cap_asid cap' = reset_cap_asid cap\<rbrakk> \<Longrightarrow> \<exists>cap'. opt_cap (cap_object cr, offset ci sz) s = Some cap' \<and> reset_cap_asid cap' = reset_cap_asid cap proof (prove)
goal:
No subgoals!
theory KHeap_DP

lemma ensure_empty_no_exception:
  "\<lbrace> < dest_slot \<mapsto>c NullCap \<and>* R> and Q \<rbrace> ensure_empty dest_slot \<lbrace>\<lambda>r. Q \<rbrace>, \<lbrace>Q'\<rbrace>" apply (simp add:ensure_empty_def) apply (wp unlessE_wp) apply (clarsimp dest!:opt_cap_sep_imp reset_cap_asid_simps2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cdl.lift (dest_slot \<mapsto>c NullCap \<and>* R) and Q\<rbrace> ensure_empty dest_slot \<lbrace>\<lambda>r. Q\<rbrace>, \<lbrace>Q'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cdl.lift (dest_slot \<mapsto>c NullCap \<and>* R) and Q\<rbrace> doE cap <- liftE (get_cap dest_slot);
unlessE (cap = NullCap) throw
odE \<lbrace>\<lambda>r. Q\<rbrace>, \<lbrace>Q'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (cdl.lift (dest_slot \<mapsto>c NullCap \<and>* R) and Q) s \<Longrightarrow> opt_cap dest_slot s \<noteq> None \<longrightarrow> (if the (opt_cap dest_slot s) = NullCap then Q else (\<lambda>s. Q' undefined s \<and> True)) s proof (prove)
goal:
No subgoals!
theory KHeap_DP

lemma reset_cap_asid_cap_type:
  "reset_cap_asid cap = reset_cap_asid cap'
  \<Longrightarrow> cap_type cap = cap_type cap'" by (clarsimp simp: reset_cap_asid_def split: cdl_cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reset_cap_asid cap = reset_cap_asid cap' \<Longrightarrow> cap_type cap = cap_type cap'
theory KHeap_DP

lemma ep_related_cap_update_cap_rights[simp]:
  "ep_related_cap (update_cap_rights rights cap) = ep_related_cap cap"
  "\<lbrakk> is_ep_cap cap \<rbrakk> \<Longrightarrow> cap_badge (update_cap_rights rights cap) = cap_badge cap"
  "\<lbrakk> is_ntfn_cap cap \<rbrakk> \<Longrightarrow> cap_badge (update_cap_rights rights cap) = cap_badge cap" by (auto simp:ep_related_cap_def cap_badge_def cap_type_def update_cap_rights_def
          split:cdl_cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ep_related_cap (update_cap_rights rights cap) = ep_related_cap cap &&& (is_ep_cap cap \<Longrightarrow> cap_badge (update_cap_rights rights cap) = cap_badge cap) &&& (is_ntfn_cap cap \<Longrightarrow> cap_badge (update_cap_rights rights cap) = cap_badge cap)
theory KHeap_DP

lemma reset_cap_asid_cap_badge:
  "\<lbrakk>reset_cap_asid cap = reset_cap_asid cap';ep_related_cap cap\<rbrakk>
  \<Longrightarrow> cap_badge cap = cap_badge cap'" apply (clarsimp simp: ep_related_cap_def split:cdl_cap.splits) by (simp_all add: ep_related_cap_def
    reset_cap_asid_def split:cdl_cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reset_cap_asid cap = reset_cap_asid cap'; ep_related_cap cap\<rbrakk> \<Longrightarrow> cap_badge cap = cap_badge cap' proof (prove)
goal (3 subgoals):
 1. \<And>x31 x32 x33. \<lbrakk>EndpointCap x31 x32 x33 = reset_cap_asid cap'; cap = reset_cap_asid cap'\<rbrakk> \<Longrightarrow> cap_badge (reset_cap_asid cap') = cap_badge cap'
 2. \<And>x41 x42 x43. \<lbrakk>NotificationCap x41 x42 x43 = reset_cap_asid cap'; cap = reset_cap_asid cap'\<rbrakk> \<Longrightarrow> cap_badge (reset_cap_asid cap') = cap_badge cap'
 3. \<And>x51 x52. \<lbrakk>ReplyCap x51 x52 = reset_cap_asid cap'; cap = reset_cap_asid cap'\<rbrakk> \<Longrightarrow> cap_badge (reset_cap_asid cap') = cap_badge cap'
theory KHeap_DP

lemma reset_cap_asid_ep_related_cap:
  "reset_cap_asid cap = reset_cap_asid cap'
  \<Longrightarrow> ep_related_cap cap = ep_related_cap cap'" apply (clarsimp simp: ep_related_cap_def) apply (case_tac cap, (case_tac cap', simp_all add: reset_cap_asid_def)+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reset_cap_asid cap = reset_cap_asid cap' \<Longrightarrow> ep_related_cap cap = ep_related_cap cap' proof (prove)
goal (1 subgoal):
 1. reset_cap_asid cap = reset_cap_asid cap' \<Longrightarrow> (case cap of EndpointCap o_id badge rights \<Rightarrow> True | NotificationCap o_id badge rights \<Rightarrow> True | ReplyCap o_id rights \<Rightarrow> True | _ \<Rightarrow> False) = (case cap' of EndpointCap o_id badge rights \<Rightarrow> True | NotificationCap o_id badge rights \<Rightarrow> True | ReplyCap o_id rights \<Rightarrow> True | _ \<Rightarrow> False) proof (prove)
goal:
No subgoals!
theory KHeap_DP

lemma reset_cap_asid_ep_cap:
  "reset_cap_asid cap = reset_cap_asid cap'
  \<Longrightarrow> is_ep_cap cap = is_ep_cap cap'" apply (case_tac cap; case_tac cap'; simp add: reset_cap_asid_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reset_cap_asid cap = reset_cap_asid cap' \<Longrightarrow> is_ep_cap cap = is_ep_cap cap' proof (prove)
goal:
No subgoals!
theory KHeap_DP

lemma reset_cap_asid_ntfn_cap:
  "reset_cap_asid cap = reset_cap_asid cap'
  \<Longrightarrow> is_ntfn_cap cap = is_ntfn_cap cap'" by (case_tac cap; case_tac cap'; simp add: reset_cap_asid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reset_cap_asid cap = reset_cap_asid cap' \<Longrightarrow> is_ntfn_cap cap = is_ntfn_cap cap'
theory KHeap_DP

lemma cap_rights_reset_cap_asid:
  "reset_cap_asid cap = reset_cap_asid cap'
 \<Longrightarrow> cap_rights cap = cap_rights cap'" apply (clarsimp simp: cap_rights_def reset_cap_asid_def) by (case_tac cap; (case_tac cap'; simp))

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reset_cap_asid cap = reset_cap_asid cap' \<Longrightarrow> cap_rights cap = cap_rights cap' proof (prove)
goal (1 subgoal):
 1. (case cap of FrameCap dev f1 f2 f3 f4 ad \<Rightarrow> FrameCap dev f1 f2 f3 f4 None | PageTableCap f1 f2 ad \<Rightarrow> PageTableCap f1 f2 None | PageDirectoryCap f1 f2 ad \<Rightarrow> PageDirectoryCap f1 f2 None | _ \<Rightarrow> cap) = (case cap' of FrameCap dev f1 f2 f3 f4 ad \<Rightarrow> FrameCap dev f1 f2 f3 f4 None | PageTableCap f1 f2 ad \<Rightarrow> PageTableCap f1 f2 None | PageDirectoryCap f1 f2 ad \<Rightarrow> PageDirectoryCap f1 f2 None | _ \<Rightarrow> cap') \<Longrightarrow> (case cap of EndpointCap xa xb x \<Rightarrow> x | NotificationCap xa xb x \<Rightarrow> x | ReplyCap xa x \<Rightarrow> x | FrameCap xa xb x xc xd xe \<Rightarrow> x | _ \<Rightarrow> all_cdl_rights) = (case cap' of EndpointCap xa xb x \<Rightarrow> x | NotificationCap xa xb x \<Rightarrow> x | ReplyCap xa x \<Rightarrow> x | FrameCap xa xb x xc xd xe \<Rightarrow> x | _ \<Rightarrow> all_cdl_rights)
theory KHeap_DP

lemma reset_cap_asid_cnode_cap:
  "\<lbrakk>reset_cap_asid cap' = reset_cap_asid cap ; is_cnode_cap cap\<rbrakk>
  \<Longrightarrow> cap' = cap" apply (drule sym) apply (drule reset_cap_asid_id) apply (clarsimp simp: cap_type_def split: cdl_cap.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reset_cap_asid cap' = reset_cap_asid cap; is_cnode_cap cap\<rbrakk> \<Longrightarrow> cap' = cap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_cnode_cap cap; reset_cap_asid cap = reset_cap_asid cap'\<rbrakk> \<Longrightarrow> cap' = cap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_cnode_cap cap; cap = cap' \<or> (\<exists>a b c d e f. cap = FrameCap f a b c d e) \<or> (\<exists>a b c. cap = PageTableCap a b c) \<or> (\<exists>a b c. cap = PageDirectoryCap a b c)\<rbrakk> \<Longrightarrow> cap' = cap proof (prove)
goal:
No subgoals!
theory KHeap_DP

lemma valid_src_cap_asid_cong:
  "reset_cap_asid cap' = reset_cap_asid cap
       \<Longrightarrow> valid_src_cap cap' = valid_src_cap cap" apply (rule ext) apply (clarsimp simp:valid_src_cap_def) apply (rule iffI[rotated]) apply (drule sym) apply (clarsimp dest!:reset_cap_asid_cnode_cap)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reset_cap_asid cap' = reset_cap_asid cap \<Longrightarrow> valid_src_cap cap' = valid_src_cap cap proof (prove)
goal (1 subgoal):
 1. \<And>x. reset_cap_asid cap' = reset_cap_asid cap \<Longrightarrow> valid_src_cap cap' x = valid_src_cap cap x proof (prove)
goal (1 subgoal):
 1. \<And>x. reset_cap_asid cap' = reset_cap_asid cap \<Longrightarrow> (is_cnode_cap cap' \<longrightarrow> unat ((x >> 3) && mask 5) + cnode_cap_size cap' \<le> word_bits) = (is_cnode_cap cap \<longrightarrow> unat ((x >> 3) && mask 5) + cnode_cap_size cap \<le> word_bits) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>reset_cap_asid cap' = reset_cap_asid cap; is_cnode_cap cap \<longrightarrow> unat ((x >> 3) && mask 5) + cnode_cap_size cap \<le> word_bits\<rbrakk> \<Longrightarrow> is_cnode_cap cap' \<longrightarrow> unat ((x >> 3) && mask 5) + cnode_cap_size cap' \<le> word_bits
 2. \<And>x. \<lbrakk>reset_cap_asid cap' = reset_cap_asid cap; is_cnode_cap cap' \<longrightarrow> unat ((x >> 3) && mask 5) + cnode_cap_size cap' \<le> word_bits\<rbrakk> \<Longrightarrow> is_cnode_cap cap \<longrightarrow> unat ((x >> 3) && mask 5) + cnode_cap_size cap \<le> word_bits proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>is_cnode_cap cap \<longrightarrow> unat ((x >> 3) && mask 5) + cnode_cap_size cap \<le> word_bits; reset_cap_asid cap = reset_cap_asid cap'\<rbrakk> \<Longrightarrow> is_cnode_cap cap' \<longrightarrow> unat ((x >> 3) && mask 5) + cnode_cap_size cap' \<le> word_bits
 2. \<And>x. \<lbrakk>reset_cap_asid cap' = reset_cap_asid cap; is_cnode_cap cap' \<longrightarrow> unat ((x >> 3) && mask 5) + cnode_cap_size cap' \<le> word_bits\<rbrakk> \<Longrightarrow> is_cnode_cap cap \<longrightarrow> unat ((x >> 3) && mask 5) + cnode_cap_size cap \<le> word_bits proof (prove)
goal:
No subgoals!
theory KHeap_DP

lemma cap_type_null:
  "cap_has_type cap \<Longrightarrow> cap \<noteq> NullCap"
  "cap_type cap = Some type \<Longrightarrow> cap \<noteq> NullCap" by (clarsimp simp: cap_type_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (cap_has_type cap \<Longrightarrow> cap \<noteq> NullCap) &&& (cap_type cap = Some type \<Longrightarrow> cap \<noteq> NullCap)
theory KHeap_DP

lemma decode_invocation_wp:
  "\<lbrace>P\<rbrace> decode_invocation (CNodeCap x y z sz) ref caps (CNodeIntent intent) \<lbrace>\<lambda>_. P\<rbrace>, -" apply (clarsimp simp: decode_invocation_def) apply (wp) apply (clarsimp simp: comp_def) apply (wpsimp simp: throw_opt_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> decode_invocation (CNodeCap x y z sz) ref caps (CNodeIntent intent) \<lbrace>\<lambda>_. P\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> doE cnode_intent <- throw_opt undefined (get_cnode_intent (CNodeIntent intent));
liftME InvokeCNode (decode_cnode_invocation (CNodeCap x y z sz) ref caps cnode_intent)
odE \<lbrace>\<lambda>_. P\<rbrace>, - proof (prove)
goal (3 subgoals):
 1. \<And>cnode_intent. \<lbrace>?B1 cnode_intent\<rbrace> decode_cnode_invocation (CNodeCap x y z sz) ref caps cnode_intent \<lbrace>(\<lambda>_. P) \<circ> InvokeCNode\<rbrace>, -
 2. \<lbrace>?P'\<rbrace> throw_opt undefined (get_cnode_intent (CNodeIntent intent)) \<lbrace>?B1\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>s. P s \<Longrightarrow> ?P' s proof (prove)
goal (3 subgoals):
 1. \<And>cnode_intent. \<lbrace>?B1 cnode_intent\<rbrace> decode_cnode_invocation (CNodeCap x y z sz) ref caps cnode_intent \<lbrace>\<lambda>_. P\<rbrace>, -
 2. \<lbrace>?P'\<rbrace> throw_opt undefined (get_cnode_intent (CNodeIntent intent)) \<lbrace>?B1\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>s. P s \<Longrightarrow> ?P' s proof (prove)
goal:
No subgoals!