kings-crown/FVELER_Isabelle huggingface dataset:
theory CNode_DR

lemma opt_cap_asid_pool_None:
  "\<lbrakk> ko_at (ArchObj (arch_kernel_obj.ASIDPool pool)) w s'; valid_idle s';
   \<not> ba < 2 ^ asid_low_bits \<rbrakk>
   \<Longrightarrow> opt_cap (w, ba) (transform s') = None" by (clarsimp simp: opt_object_asid_pool obj_at_def slots_of_def unat_map_def
     opt_cap_def invs_def valid_state_def object_slots_def transform_asid_pool_contents_def
      asid_low_bits_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ako_at (ASIDPool pool) w s'; valid_idle s'; \<not> ba < 2 ^ local.asid_low_bits\<rbrakk> \<Longrightarrow> opt_cap (w, ba) (transform s') = None
theory CNode_DR

lemma dcorres_unless_r:
  "\<lbrakk> \<not> G \<Longrightarrow> dcorres r P P' f g;
    G \<Longrightarrow> dcorres r Q Q' f (return ()) \<rbrakk>
  \<Longrightarrow> dcorres r (P and Q) (\<lambda>s. (\<not>G \<longrightarrow> P' s) \<and> (G \<longrightarrow> Q' s)) f (unless G g)" apply (cases G, simp_all add: when_def unless_def) apply (rule corres_guard_imp, simp+)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> G \<Longrightarrow> dcorres r P P' f g; G \<Longrightarrow> dcorres r Q Q' f (return ())\<rbrakk> \<Longrightarrow> dcorres r (P and Q) (\<lambda>s. (\<not> G \<longrightarrow> P' s) \<and> (G \<longrightarrow> Q' s)) f (unless G g) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>dcorres r Q Q' f (return ()); G\<rbrakk> \<Longrightarrow> dcorres r (P and Q) Q' f (return ())
 2. \<lbrakk>dcorres r P P' f g; \<not> G\<rbrakk> \<Longrightarrow> dcorres r (P and Q) P' f g proof (prove)
goal:
No subgoals!
theory CNode_DR

lemma opt_cap_pd_Some:
  "\<lbrakk>valid_idle s';kheap s' (ptr && ~~ mask pd_bits)= Some (ArchObj (arch_kernel_obj.PageDirectory fun));
    ucast (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk>
         \<Longrightarrow>  (opt_cap (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)) (transform s'))
    = Some (transform_pde (fun (of_nat (unat (ptr && mask pd_bits >> 2)))))" apply (clarsimp simp:opt_cap_def slots_of_def
    object_slots_def transform_objects_def  restrict_map_def not_idle_thread_def) apply (simp add:opt_object_page_directory object_slots_def) apply (clarsimp simp:transform_page_directory_contents_def
    transform_pde_def unat_map_def below_kernel_base) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_idle s'; kheap s' (ptr && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory fun)); UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> opt_cap (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)) (transform s') = Some (transform_pde (fun (word_of_nat (unat (ptr && mask pd_bits >> 2))))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_idle s'; kheap s' (ptr && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory fun)); UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> (case cdl_objects (transform s') (ptr && ~~ mask pd_bits) of None \<Rightarrow> \<lambda>x. None | Some x \<Rightarrow> object_slots x) (unat (ptr && mask pd_bits >> 2)) = Some (transform_pde (fun (UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2)))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_idle s'; kheap s' (ptr && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory fun)); UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> transform_page_directory_contents fun (unat (ptr && mask pd_bits >> 2)) = Some (transform_pde (fun (UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2)))) proof (prove)
goal:
No subgoals!
theory CNode_DR

lemma inj_neq:"\<lbrakk>inj f;a\<noteq> b\<rbrakk> \<Longrightarrow> f a\<noteq> f b" apply (rule ccontr) apply (clarsimp simp:inj_eq) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>inj f; a \<noteq> b\<rbrakk> \<Longrightarrow> f a \<noteq> f b proof (prove)
goal (1 subgoal):
 1. \<lbrakk>inj f; a \<noteq> b; \<not> f a \<noteq> f b\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory CNode_DR

lemma store_pte_ct:
  "\<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> store_pte x y \<lbrace>\<lambda>r s. P (cur_thread s)\<rbrace>" apply (clarsimp simp:store_pte_def) apply wp apply (simp add:set_pt_def) apply wp apply (rule_tac Q = "\<lambda>r s. P (cur_thread s)" in hoare_strengthen_post) apply (wp|clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> store_pte x y \<lbrace>\<lambda>r s. P (cur_thread s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> do pt <- get_pt (x && ~~ mask pt_bits);
set_pt (x && ~~ mask pt_bits) (pt(UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2) := y))
od \<lbrace>\<lambda>r s. P (cur_thread s)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrace>?B1 xa\<rbrace> set_pt (x && ~~ mask pt_bits) (xa(UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2) := y)) \<lbrace>\<lambda>r s. P (cur_thread s)\<rbrace>
 2. \<lbrace>?Q\<rbrace> get_pt (x && ~~ mask pt_bits) \<lbrace>?B1\<rbrace>
 3. \<And>s. P (cur_thread s) \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrace>?B1 xa\<rbrace> KHeap_A.set_object (x && ~~ mask pt_bits) (ArchObj (arch_kernel_obj.PageTable (xa(UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2) := y)))) \<lbrace>\<lambda>r s. P (cur_thread s)\<rbrace>
 2. \<lbrace>?Q\<rbrace> get_pt (x && ~~ mask pt_bits) \<lbrace>?B1\<rbrace>
 3. \<And>s. P (cur_thread s) \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> get_pt (x && ~~ mask pt_bits) \<lbrace>\<lambda>x s. P (cur_thread s)\<rbrace>
 2. \<And>s. P (cur_thread s) \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?Q\<rbrace> get_pt (x && ~~ mask pt_bits) \<lbrace>\<lambda>r s. P (cur_thread s)\<rbrace>
 2. \<And>rv s. P (cur_thread s) \<Longrightarrow> P (cur_thread s)
 3. \<And>s. P (cur_thread s) \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory CNode_DR

lemma invalidate_tlb_by_asid_dwp:
  "\<lbrace>\<lambda>a. transform a = cs\<rbrace> invalidate_tlb_by_asid aa \<lbrace>\<lambda>r s. transform s = cs\<rbrace>" apply (simp add:invalidate_tlb_by_asid_def) apply (wp do_machine_op_wp|wpc)+ apply clarsimp apply (wp) apply (rule_tac Q = "\<lambda>r s. transform s = cs" in  hoare_strengthen_post) apply (simp add:load_hw_asid_def) apply (wp|clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>a. transform a = cs\<rbrace> invalidate_tlb_by_asid aa \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>a. transform a = cs\<rbrace> do maybe_hw_asid <- load_hw_asid aa;
case maybe_hw_asid of None \<Rightarrow> return () | Some hw_asid \<Rightarrow> do_machine_op $ invalidateLocalTLB_ASID hw_asid
od \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>maybe_hw_asid x2. maybe_hw_asid = Some x2 \<Longrightarrow> \<forall>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> invalidateLocalTLB_ASID x2 \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>
 2. \<lbrace>?Q\<rbrace> load_hw_asid aa \<lbrace>\<lambda>maybe_hw_asid s. (maybe_hw_asid = None \<longrightarrow> transform s = cs) \<and> (\<forall>x. maybe_hw_asid = Some x \<longrightarrow> transform s = cs)\<rbrace>
 3. \<And>s. transform s = cs \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>x2 m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> invalidateLocalTLB_ASID x2 \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>
 2. \<lbrace>?Q\<rbrace> load_hw_asid aa \<lbrace>\<lambda>maybe_hw_asid s. (maybe_hw_asid = None \<longrightarrow> transform s = cs) \<and> (\<forall>x. maybe_hw_asid = Some x \<longrightarrow> transform s = cs)\<rbrace>
 3. \<And>s. transform s = cs \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> load_hw_asid aa \<lbrace>\<lambda>maybe_hw_asid s. (maybe_hw_asid = None \<longrightarrow> transform s = cs) \<and> (\<forall>x. maybe_hw_asid = Some x \<longrightarrow> transform s = cs)\<rbrace>
 2. \<And>s. transform s = cs \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?Q\<rbrace> load_hw_asid aa \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 2. \<And>rv s. transform s = cs \<Longrightarrow> (rv = None \<longrightarrow> transform s = cs) \<and> (\<forall>x. rv = Some x \<longrightarrow> transform s = cs)
 3. \<And>s. transform s = cs \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?Q\<rbrace> do asid_map <- gets (arm_asid_map \<circ> arch_state);
return (map_option fst (asid_map aa))
od \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 2. \<And>rv s. transform s = cs \<Longrightarrow> (rv = None \<longrightarrow> transform s = cs) \<and> (\<forall>x. rv = Some x \<longrightarrow> transform s = cs)
 3. \<And>s. transform s = cs \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory CNode_DR

lemma opt_cap_pd_not_None:
  "\<lbrakk>ko_at (ArchObj (arch_kernel_obj.PageDirectory ptx)) w s'; valid_idle s';ba<4096\<rbrakk>
   \<Longrightarrow> \<exists>y. opt_cap (w, ba) (transform s') = Some y" by (clarsimp simp: opt_object_page_directory obj_at_def slots_of_def unat_map_def
    opt_cap_def invs_def valid_state_def object_slots_def transform_page_directory_contents_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ako_at (arch_kernel_obj.PageDirectory ptx) w s'; valid_idle s'; ba < 4096\<rbrakk> \<Longrightarrow> \<exists>y. opt_cap (w, ba) (transform s') = Some y
theory CNode_DR

lemma opt_cap_pd_None:
  "\<lbrakk>ko_at (ArchObj (arch_kernel_obj.PageDirectory ptx)) w s'; valid_idle s';\<not> ba < 4096\<rbrakk>
   \<Longrightarrow> opt_cap (w, ba) (transform s') = None" by (clarsimp simp: opt_object_page_directory obj_at_def slots_of_def unat_map_def
    opt_cap_def invs_def valid_state_def object_slots_def transform_page_directory_contents_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ako_at (arch_kernel_obj.PageDirectory ptx) w s'; valid_idle s'; \<not> ba < 4096\<rbrakk> \<Longrightarrow> opt_cap (w, ba) (transform s') = None
theory CNode_DR

lemma upto_enum_word_append:
  fixes a :: "('a :: len) word"
  assumes lt: "1 \<le> b" and les: "a \<le> b" "b < c"
  shows "[a .e. b - 1] @ [b .e. c] = [a .e. c]" (is "?LHS = ?RHS") proof - have "?LHS = map of_nat ([unat a ..< unat b] @ [unat b ..< Suc (unat c)])" using lt by (simp add: upto_enum_word Suc_unat_diff_1) also have "... = map of_nat [unat a ..< Suc (unat c)]" using les apply - apply (rule arg_cong [where f = "map of_nat"]) apply (rule upt_add_eq_append' [symmetric]) apply (simp_all add: word_less_nat_alt word_le_nat_alt) done finally show ?thesis by (simp add: upto_enum_word) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. [a .e. b - 1] @ [b .e. c] = [a .e. c] proof (state)
goal (1 subgoal):
 1. [a .e. b - 1] @ [b .e. c] = [a .e. c] proof (prove)
goal (1 subgoal):
 1. [a .e. b - 1] @ [b .e. c] = map word_of_nat ([unat a..<unat b] @ [unat b..<Suc (unat c)]) proof (prove)
using this:
1 \<le> b

goal (1 subgoal):
 1. [a .e. b - 1] @ [b .e. c] = map word_of_nat ([unat a..<unat b] @ [unat b..<Suc (unat c)]) proof (state)
this:
[a .e. b - 1] @ [b .e. c] = map word_of_nat ([unat a..<unat b] @ [unat b..<Suc (unat c)])

goal (1 subgoal):
 1. [a .e. b - 1] @ [b .e. c] = [a .e. c] proof (state)
this:
[a .e. b - 1] @ [b .e. c] = map word_of_nat ([unat a..<unat b] @ [unat b..<Suc (unat c)])

goal (1 subgoal):
 1. [a .e. b - 1] @ [b .e. c] = [a .e. c] proof (prove)
goal (1 subgoal):
 1. map word_of_nat ([unat a..<unat b] @ [unat b..<Suc (unat c)]) = map word_of_nat [unat a..<Suc (unat c)] proof (prove)
using this:
a \<le> b
b < c

goal (1 subgoal):
 1. map word_of_nat ([unat a..<unat b] @ [unat b..<Suc (unat c)]) = map word_of_nat [unat a..<Suc (unat c)] proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<le> b; b < c\<rbrakk> \<Longrightarrow> map word_of_nat ([unat a..<unat b] @ [unat b..<Suc (unat c)]) = map word_of_nat [unat a..<Suc (unat c)] proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<le> b; b < c\<rbrakk> \<Longrightarrow> [unat a..<unat b] @ [unat b..<Suc (unat c)] = [unat a..<Suc (unat c)] proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a \<le> b; b < c\<rbrakk> \<Longrightarrow> unat a \<le> unat b
 2. \<lbrakk>a \<le> b; b < c\<rbrakk> \<Longrightarrow> unat b \<le> Suc (unat c) proof (prove)
goal:
No subgoals! proof (state)
this:
map word_of_nat ([unat a..<unat b] @ [unat b..<Suc (unat c)]) = map word_of_nat [unat a..<Suc (unat c)]

goal (1 subgoal):
 1. [a .e. b - 1] @ [b .e. c] = [a .e. c] proof (chain)
picking this:
[a .e. b - 1] @ [b .e. c] = map word_of_nat [unat a..<Suc (unat c)] proof (prove)
using this:
[a .e. b - 1] @ [b .e. c] = map word_of_nat [unat a..<Suc (unat c)]

goal (1 subgoal):
 1. [a .e. b - 1] @ [b .e. c] = [a .e. c] proof (state)
this:
[a .e. b - 1] @ [b .e. c] = [a .e. c]

goal:
No subgoals!
theory CNode_DR

lemma get_cnode'D:
  "get_cnode' ptr s = Some (sz,cn) \<Longrightarrow> kheap s ptr = Some (Structures_A.CNode sz cn)" unfolding get_cnode'_def by (clarsimp split: Structures_A.kernel_object.splits option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. get_cnode' ptr s = Some (sz, cn) \<Longrightarrow> kheap s ptr = Some (kernel_object.CNode sz cn) proof (prove)
goal (1 subgoal):
 1. (case kheap s ptr of None \<Rightarrow> None | Some (kernel_object.CNode sz cn) \<Rightarrow> Some (sz, cn) | Some _ \<Rightarrow> None) = Some (sz, cn) \<Longrightarrow> kheap s ptr = Some (kernel_object.CNode sz cn)
theory CNode_DR

lemma zombie_get_cnode:
  "\<lbrakk>cte_wp_at ((=) (cap.Zombie x (Some xc) xb)) slot s; invs s\<rbrakk> \<Longrightarrow> get_cnode' x s \<noteq> None" by (clarsimp dest!: cte_wp_at_valid_objs_valid_cap [OF _ invs_valid_objs] simp: valid_cap_simps get_cnode'_def obj_at_def
    elim!: is_cap_tableE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at ((=) (Zombie x (Some xc) xb)) slot s; invs s\<rbrakk> \<Longrightarrow> get_cnode' x s \<noteq> None
theory CNode_DR

lemma dcorres_gba_no_effect:
  "dcorres dc \<top> \<top> (return a) (get_bound_notification tcb)" apply (clarsimp simp: get_bound_notification_def thread_get_def gets_the_def gets_def bind_assoc) apply (rule dcorres_absorb_get_r) apply (clarsimp simp: assert_opt_def corres_free_fail split: Structures_A.kernel_object.splits option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return a) (get_bound_notification tcb) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return a) (do x <- get;
tcb <- assert_opt (get_tcb tcb x);
return (tcb_bound_notification tcb)
od) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>True; True\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return a) (do tcb <- assert_opt (get_tcb tcb s');
return (tcb_bound_notification tcb)
od) proof (prove)
goal:
No subgoals!
theory CNode_DR

lemma cap_revoke_valid_etcbs[wp]:
  "\<lbrace> valid_etcbs \<rbrace> cap_revoke cap \<lbrace> \<lambda>_. valid_etcbs \<rbrace>" by (wp cap_revoke_preservation)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_etcbs\<rbrace> cap_revoke cap \<lbrace>\<lambda>_. valid_etcbs\<rbrace>
theory CNode_DR

lemma transform_cnode_index_and_depth_Some:
  "(transform_cnode_index_and_depth f xs = Some v)
     = (length xs > 1 \<and> f (xs ! 0) (xs ! 1) = v)" by (simp add: transform_cnode_index_and_depth_def split: list.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (transform_cnode_index_and_depth f xs = Some v) = (1 < length xs \<and> f (xs ! 0) (xs ! 1) = v)
theory CNode_DR

lemma ensure_no_children_dummy:
  "dcorres dc \<top> \<top> (return x) (ensure_no_children slot)" apply (simp add: ensure_no_children_def) apply (clarsimp simp: corres_underlying_def return_def in_monad bindE_def lift_def) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return x) (CSpace_A.ensure_no_children slot) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return x) (doE cdt <- liftE (gets cdt);
whenE (\<exists>a b. cdt (a, b) = Some slot) (throwError RevokeFirst)
odE) proof (prove)
goal (1 subgoal):
 1. \<And>b a ba. \<lbrakk>(\<exists>a ba. cdt b (a, ba) = Some slot) \<longrightarrow> a = Inl RevokeFirst \<and> ba = b; (\<forall>a ba. cdt b (a, ba) \<noteq> Some slot) \<longrightarrow> a = Inr () \<and> ba = b\<rbrakk> \<Longrightarrow> transform ba = transform b proof (prove)
goal:
No subgoals!
theory CNode_DR

lemma cdt_transform:
  "cdl_cdt (transform s) = map_lift_over transform_cslot_ptr (cdt s)" by (simp add: transform_def transform_cdt_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cdl_cdt (transform s) = map_lift_over transform_cslot_ptr (cdt s)
theory CNode_DR

lemma derive_cap_Null [simp]:
  "CSpace_D.derive_cap slot cdl_cap.NullCap = returnOk cdl_cap.NullCap" by (simp add: CSpace_D.derive_cap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. CSpace_D.derive_cap slot cdl_cap.NullCap = returnOk cdl_cap.NullCap
theory CNode_DR

lemma transform_cap_rights_update [simp]:
  "transform_cap (cap_rights_update R cap) =
   update_cap_rights R (transform_cap cap)" apply (simp add: cap_rights_update_def update_cap_rights_def) apply (clarsimp simp: transform_cap_def acap_rights_update_def
                  split: cap.splits arch_cap.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. transform_cap (cap_rights_update R cap) = update_cap_rights R (transform_cap cap) proof (prove)
goal (1 subgoal):
 1. transform_cap (case cap of cap.EndpointCap oref badge cr \<Rightarrow> cap.EndpointCap oref badge R | cap.NotificationCap oref badge cr \<Rightarrow> cap.NotificationCap oref badge (R - {AllowGrant, AllowGrantReply}) | cap.ReplyCap t m cr \<Rightarrow> cap.ReplyCap t m (R - {AllowRead, AllowGrantReply} \<union> {AllowWrite}) | ArchObjectCap acap \<Rightarrow> ArchObjectCap (acap_rights_update R acap) | _ \<Rightarrow> cap) = (case transform_cap cap of cdl_cap.EndpointCap f1 f2 x \<Rightarrow> cdl_cap.EndpointCap f1 f2 R | cdl_cap.NotificationCap f1 f2 x \<Rightarrow> cdl_cap.NotificationCap f1 f2 (R - {AllowGrant, AllowGrantReply}) | cdl_cap.ReplyCap f1 x \<Rightarrow> cdl_cap.ReplyCap f1 (R - {AllowRead, AllowGrantReply} \<union> {AllowWrite}) | FrameCap dev f1 x f2 f3 f4 \<Rightarrow> FrameCap dev f1 (validate_vm_rights R) f2 f3 f4 | _ \<Rightarrow> transform_cap cap) proof (prove)
goal:
No subgoals!
theory CNode_DR

lemma lsfco_not_idle:
  "\<lbrace>valid_objs and valid_cap cap and valid_idle\<rbrace>
   CSpace_A.lookup_slot_for_cnode_op b cap idx depth
   \<lbrace>\<lambda>rv. not_idle_thread (fst rv)\<rbrace>, -" apply (rule_tac Q'="\<lambda>rv. real_cte_at rv and valid_idle" in hoare_post_imp_R) apply (rule hoare_pre, wp) apply simp apply (clarsimp simp: obj_at_def not_idle_thread_def valid_idle_def
                        pred_tcb_at_def is_cap_table_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and valid_cap cap and valid_idle\<rbrace> CSpace_A.lookup_slot_for_cnode_op b cap idx depth \<lbrace>\<lambda>rv. not_idle_thread (fst rv)\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>valid_objs and valid_cap cap and valid_idle\<rbrace> CSpace_A.lookup_slot_for_cnode_op b cap idx depth \<lbrace>\<lambda>rv. real_cte_at rv and valid_idle\<rbrace>, -
 2. \<And>rv s. (real_cte_at rv and valid_idle) s \<Longrightarrow> not_idle_thread (fst rv) s proof (prove)
goal (2 subgoals):
 1. \<And>s. (valid_objs and valid_cap cap and valid_idle) s \<Longrightarrow> (valid_objs and valid_cap cap) s \<and> valid_idle s
 2. \<And>rv s. (real_cte_at rv and valid_idle) s \<Longrightarrow> not_idle_thread (fst rv) s proof (prove)
goal (1 subgoal):
 1. \<And>rv s. (real_cte_at rv and valid_idle) s \<Longrightarrow> not_idle_thread (fst rv) s proof (prove)
goal:
No subgoals!
theory CNode_DR

lemma cdl_right_UNIV:
  "UNIV = {Read, Write, Grant, GrantReply}" apply (rule set_eqI) apply (case_tac x, auto) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. UNIV = {AllowRead, AllowWrite, AllowGrant, AllowGrantReply} proof (prove)
goal (1 subgoal):
 1. \<And>x. (x \<in> UNIV) = (x \<in> {AllowRead, AllowWrite, AllowGrant, AllowGrantReply}) proof (prove)
goal:
No subgoals!
theory CNode_DR

lemma has_recycle_rights_eq [simp]:
  "CNode_D.has_cancel_send_rights (transform_cap cap) =
   CSpace_A.has_cancel_send_rights cap" apply (simp add: CNode_D.has_cancel_send_rights_def CSpace_A.has_cancel_send_rights_def split: cap.splits) apply (auto simp: transform_cap_def all_rights_def
              split: rights.splits arch_cap.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. CNode_D.has_cancel_send_rights (transform_cap cap) = CSpace_A.has_cancel_send_rights cap proof (prove)
goal (1 subgoal):
 1. (\<forall>x31 x32 x33. cap = cap.EndpointCap x31 x32 x33 \<longrightarrow> (x33 = UNIV) = (x33 = all_rights)) \<and> (\<forall>x12. cap = ArchObjectCap x12 \<longrightarrow> \<not> (case transform_cap (ArchObjectCap x12) of cdl_cap.EndpointCap x xa R \<Rightarrow> R = UNIV | _ \<Rightarrow> False)) proof (prove)
goal:
No subgoals!
theory CNode_DR

lemma get_index_Nil [simp]:
  "get_index [] n = None" by (simp add: get_index_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. get_index [] n = None
theory CNode_DR

lemma throw_opt_None [simp]:
  "throw_opt x None = throwError x" by (simp add: throw_opt_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. throw_opt x None = throwError x
theory CNode_DR

lemma throw_on_none [simp]:
  "throw_on_none None = Monads_D.throw" by (simp add: throw_on_none_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. throw_on_none None = throw
theory CNode_DR

lemma cnode_decode_throw:
  "\<lbrakk> transform_intent (invocation_type label) args = Some (CNodeIntent ui);
    invocation_type label = GenInvocationLabel CNodeCopy \<or>
    invocation_type label = GenInvocationLabel CNodeMint \<or>
    invocation_type label = GenInvocationLabel CNodeMove \<or>
    invocation_type label = GenInvocationLabel CNodeMutate \<rbrakk> \<Longrightarrow>
  CNode_D.decode_cnode_invocation target target_ref [] ui = Monads_D.throw" apply (auto simp: CNode_D.decode_cnode_invocation_def transform_intent_def
                    transform_intent_cnode_copy_def
                    transform_intent_cnode_mint_def
                    transform_intent_cnode_move_def
                    transform_intent_cnode_mutate_def
                    transform_intent_cnode_rotate_def
              split: list.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>transform_intent (invocation_type label) args = Some (CNodeIntent ui); invocation_type label = GenInvocationLabel CNodeCopy \<or> invocation_type label = GenInvocationLabel CNodeMint \<or> invocation_type label = GenInvocationLabel CNodeMove \<or> invocation_type label = GenInvocationLabel CNodeMutate\<rbrakk> \<Longrightarrow> CNode_D.decode_cnode_invocation target target_ref [] ui = throw proof (prove)
goal:
No subgoals!