kings-crown/FVELER_Isabelle huggingface dataset:
theory Untyped_AI

lemma detype_invs:
  "ptr && ~~ mask sz = ptr \<Longrightarrow> invs (detype usable_range (clear_um usable_range s))" apply (insert misc cte_wp_at descendants_range) apply clarsimp apply (frule detype_invariants, simp_all) apply (clarsimp simp:blah descendants_range_def2) apply ((simp add: invs_untyped_children blah
          invs_valid_reply_caps invs_valid_reply_masters)+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ptr && ~~ mask sz = ptr \<Longrightarrow> invs (detype {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} (clear_um {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} s)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ptr && ~~ mask sz = ptr; ct_active s; invs s; cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s; descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref s; descendants_range_in {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1} cref s\<rbrakk> \<Longrightarrow> invs (detype {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} (clear_um {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} s)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ptr && ~~ mask sz = ptr; ct_active s; invs s; cte_wp_at ((=) (UntypedCap dev ptr sz idx)) cref s; descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref s\<rbrakk> \<Longrightarrow> invs (detype {ptr..ptr + 2 ^ sz - 1} (clear_um {ptr..ptr + 2 ^ sz - 1} s)) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>ptr && ~~ mask sz = ptr; ct_active s; invs s; cte_wp_at ((=) (UntypedCap dev ptr sz idx)) cref s; descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref s\<rbrakk> \<Longrightarrow> descendants_range (UntypedCap dev ptr sz idx) cref s
 2. \<lbrakk>ptr && ~~ mask sz = ptr; ct_active s; invs s; cte_wp_at ((=) (UntypedCap dev ptr sz idx)) cref s; descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref s\<rbrakk> \<Longrightarrow> untyped_children_in_mdb s
 3. \<lbrakk>ptr && ~~ mask sz = ptr; ct_active s; invs s; cte_wp_at ((=) (UntypedCap dev ptr sz idx)) cref s; descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref s; invs (detype (untyped_range (UntypedCap dev ptr sz idx)) (clear_um (untyped_range (UntypedCap dev ptr sz idx)) s)) \<and> untyped_children_in_mdb (detype (untyped_range (UntypedCap dev ptr sz idx)) (clear_um (untyped_range (UntypedCap dev ptr sz idx)) s))\<rbrakk> \<Longrightarrow> invs (detype {ptr..ptr + 2 ^ sz - 1} (clear_um {ptr..ptr + 2 ^ sz - 1} s)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ptr && ~~ mask sz = ptr; ct_active s; invs s; cte_wp_at ((=) (UntypedCap dev ptr sz idx)) cref s; descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref s\<rbrakk> \<Longrightarrow> untyped_children_in_mdb s
 2. \<lbrakk>ptr && ~~ mask sz = ptr; ct_active s; invs s; cte_wp_at ((=) (UntypedCap dev ptr sz idx)) cref s; descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref s; invs (detype (untyped_range (UntypedCap dev ptr sz idx)) (clear_um (untyped_range (UntypedCap dev ptr sz idx)) s)) \<and> untyped_children_in_mdb (detype (untyped_range (UntypedCap dev ptr sz idx)) (clear_um (untyped_range (UntypedCap dev ptr sz idx)) s))\<rbrakk> \<Longrightarrow> invs (detype {ptr..ptr + 2 ^ sz - 1} (clear_um {ptr..ptr + 2 ^ sz - 1} s)) proof (prove)
goal:
No subgoals!
theory Untyped_AI

lemma idx_le_new_offs:
  "\<not> reset
   \<Longrightarrow> idx \<le> unat ((ptr && mask sz) + (of_nat (length slots) << obj_bits_api tp us))" using misc idx_cases range_cover.range_cover_base_le[OF cover] apply (simp only: simp_thms) apply (erule order_trans) apply (simp add: word_le_nat_alt[symmetric]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> reset \<Longrightarrow> idx \<le> unat ((ptr && mask sz) + (word_of_nat (length slots) << obj_bits_api tp us)) proof (prove)
using this:
ct_active s
invs s
idx \<le> unat (ptr - (ptr && ~~ mask sz)) \<or> reset \<and> ptr = ptr && ~~ mask sz
ptr && mask sz \<le> (ptr && mask sz) + (word_of_nat (length slots) << obj_bits_api tp us)

goal (1 subgoal):
 1. \<not> reset \<Longrightarrow> idx \<le> unat ((ptr && mask sz) + (word_of_nat (length slots) << obj_bits_api tp us)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> reset; ct_active s; invs s; idx \<le> unat (ptr - (ptr && ~~ mask sz)); ptr && mask sz \<le> (ptr && mask sz) + (word_of_nat (length slots) << obj_bits_api tp us)\<rbrakk> \<Longrightarrow> idx \<le> unat ((ptr && mask sz) + (word_of_nat (length slots) << obj_bits_api tp us)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> reset; ct_active s; invs s; ptr && mask sz \<le> (ptr && mask sz) + (word_of_nat (length slots) << obj_bits_api tp us)\<rbrakk> \<Longrightarrow> unat (ptr - (ptr && ~~ mask sz)) \<le> unat ((ptr && mask sz) + (word_of_nat (length slots) << obj_bits_api tp us)) proof (prove)
goal:
No subgoals!
theory Untyped_AI

lemma detype_clear_um_simps[simp]:
 "caps_no_overlap ptr sz (clear_um H s)
  = caps_no_overlap ptr sz s"
 "pspace_no_overlap S (clear_um H s)
  = pspace_no_overlap S s"
 "descendants_range_in S p (clear_um H s)
  = descendants_range_in S p s" apply (clarsimp simp: caps_no_overlap_def pspace_no_overlap_def
                        clear_um.pspace descendants_range_in_def
                  cong: if_cong)+ apply (simp add: clear_um_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. caps_no_overlap ptr sz (clear_um H s) = caps_no_overlap ptr sz s &&& pspace_no_overlap S (clear_um H s) = pspace_no_overlap S s &&& descendants_range_in S p (clear_um H s) = descendants_range_in S p s proof (prove)
goal (1 subgoal):
 1. (\<forall>p'\<in>descendants_of p (cdt (clear_um H s)). cte_wp_at (\<lambda>c. cap_range c \<inter> S = {}) p' s) = (\<forall>p'\<in>descendants_of p (cdt s). cte_wp_at (\<lambda>c. cap_range c \<inter> S = {}) p' s) proof (prove)
goal:
No subgoals!
theory Untyped_AI

lemma tcb_cap_valid_untyped_cong:
  "tcb_cap_valid (UntypedCap dev1 a1 b1 c) =
   tcb_cap_valid (UntypedCap dev2 a2 b2 c2)" apply (rule ext)+ apply (clarsimp simp:tcb_cap_valid_def valid_ipc_buffer_cap_def split:option.splits) apply (simp add: tcb_cap_cases_def
                   is_arch_cap_def is_nondevice_page_cap_simps is_cap_simps
            split: thread_state.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_cap_valid (UntypedCap dev1 a1 b1 c) = tcb_cap_valid (UntypedCap dev2 a2 b2 c2) proof (prove)
goal (1 subgoal):
 1. \<And>x xa. tcb_cap_valid (UntypedCap dev1 a1 b1 c) x xa = tcb_cap_valid (UntypedCap dev2 a2 b2 c2) x xa proof (prove)
goal (1 subgoal):
 1. \<And>a b xa. (tcb_at a xa \<longrightarrow> st_tcb_at (\<lambda>st. \<forall>aa ab ba. tcb_cap_cases b = Some (aa, ab, ba) \<longrightarrow> ba a st (UntypedCap dev1 a1 b1 c)) a xa \<and> (b = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. \<not> ko_at (TCB tcb) a xa))) = (tcb_at a xa \<longrightarrow> st_tcb_at (\<lambda>st. \<forall>aa ab ba. tcb_cap_cases b = Some (aa, ab, ba) \<longrightarrow> ba a st (UntypedCap dev2 a2 b2 c2)) a xa \<and> (b = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. \<not> ko_at (TCB tcb) a xa))) proof (prove)
goal:
No subgoals!
theory Untyped_AI

lemma tcb_cap_valid_untyped_to_thread:
  "tcb_cap_valid (UntypedCap dev a1 b1 c) =
   tcb_cap_valid (cap.ThreadCap 0)" apply (rule ext)+ apply (clarsimp simp:tcb_cap_valid_def valid_ipc_buffer_cap_def split:option.splits) apply (simp add: tcb_cap_cases_def is_cap_simps
                   is_arch_cap_def is_nondevice_page_cap_simps
            split: thread_state.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_cap_valid (UntypedCap dev a1 b1 c) = tcb_cap_valid (ThreadCap 0) proof (prove)
goal (1 subgoal):
 1. \<And>x xa. tcb_cap_valid (UntypedCap dev a1 b1 c) x xa = tcb_cap_valid (ThreadCap 0) x xa proof (prove)
goal (1 subgoal):
 1. \<And>a b xa. (tcb_at a xa \<longrightarrow> st_tcb_at (\<lambda>st. \<forall>aa ab ba. tcb_cap_cases b = Some (aa, ab, ba) \<longrightarrow> ba a st (UntypedCap dev a1 b1 c)) a xa \<and> (b = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. \<not> ko_at (TCB tcb) a xa))) = (tcb_at a xa \<longrightarrow> st_tcb_at (\<lambda>st. \<forall>aa ab ba. tcb_cap_cases b = Some (aa, ab, ba) \<longrightarrow> ba a st (ThreadCap 0)) a xa \<and> (b = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. \<not> ko_at (TCB tcb) a xa))) proof (prove)
goal:
No subgoals!
theory Untyped_AI

lemma mapME_append:
  "mapME f (xs @ ys) = doE
    xs_r \<leftarrow> mapME f xs;
    ys_r \<leftarrow> mapME f ys;
    returnOk (xs_r @ ys_r)
  odE" by (induct xs, simp_all add: mapME_Nil mapME_Cons bindE_assoc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mapME f (xs @ ys) = doE xs_r <- mapME f xs;
ys_r <- mapME f ys;
returnOk (xs_r @ ys_r)
odE
theory Untyped_AI

lemma mapME_x_mapME:
  "mapME_x m l = (mapME m l >>=E (%_. returnOk ()))" apply (simp add: mapME_x_def sequenceE_x_def mapME_def sequenceE_def) apply (induct l, simp_all add: Let_def bindE_assoc) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mapME_x m l = doE _ <- mapME m l;
returnOk ()
odE proof (prove)
goal (1 subgoal):
 1. foldr (\<lambda>x y. doE _ <- x;
y
odE) (map m l) (returnOk ()) = doE _ <- foldr (\<lambda>p q. doE x <- p;
y <- q;
returnOk (x # y)
odE) (map m l) (returnOk []);
returnOk ()
odE proof (prove)
goal:
No subgoals!
theory Untyped_AI

lemma mapME_x_validE_nth:
  "\<lbrakk> \<And>i. i < length xs \<Longrightarrow> \<lbrace>P i\<rbrace> f (xs ! i) \<lbrace>\<lambda>y. P (Suc i)\<rbrace>, \<lbrace>E\<rbrace> \<rbrakk>
    \<Longrightarrow> \<lbrace>P 0\<rbrace> mapME_x f xs \<lbrace>\<lambda>_. P (length xs)\<rbrace>, \<lbrace>E\<rbrace>" by (wp mapME_validE_nth | simp add: mapME_x_mapME)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>i. i < length xs \<Longrightarrow> \<lbrace>P i\<rbrace> f (xs ! i) \<lbrace>\<lambda>y. P (Suc i)\<rbrace>, \<lbrace>E\<rbrace>) \<Longrightarrow> \<lbrace>P 0\<rbrace> mapME_x f xs \<lbrace>\<lambda>_. P (length xs)\<rbrace>, \<lbrace>E\<rbrace>
theory Untyped_AI

lemma alignUp_ge_nat:
  "0 < m
    \<Longrightarrow> (n :: nat) \<le> ((n + m - 1) div m) * m" apply (cases n) apply (simp_all add: Suc_le_eq) apply (metis add.commute add_less_cancel_left dividend_less_div_times) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 0 < m \<Longrightarrow> n \<le> (n + m - 1) div m * m proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < m; n = 0\<rbrakk> \<Longrightarrow> n \<le> (n + m - 1) div m * m
 2. \<And>nat. \<lbrakk>0 < m; n = Suc nat\<rbrakk> \<Longrightarrow> n \<le> (n + m - 1) div m * m proof (prove)
goal (1 subgoal):
 1. \<And>nat. \<lbrakk>0 < m; n = Suc nat\<rbrakk> \<Longrightarrow> nat < (nat + m) div m * m proof (prove)
goal:
No subgoals!
theory Untyped_AI

lemma alignUp_le_nat:
  "0 < m \<Longrightarrow> n \<le> (b :: nat) \<Longrightarrow> m dvd b
    \<Longrightarrow> ((n + m - 1) div m) * m \<le> b" apply (clarsimp simp: dvd_def) apply (rule less_Suc_eq_le[THEN iffD1]) apply (simp add: td_gal_lt[symmetric]) apply (subst less_eq_Suc_le, simp add: mult.commute) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < m; n \<le> b; m dvd b\<rbrakk> \<Longrightarrow> (n + m - 1) div m * m \<le> b proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>0 < m; n \<le> m * k; b = m * k\<rbrakk> \<Longrightarrow> (n + m - Suc 0) div m \<le> k proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>0 < m; n \<le> m * k; b = m * k\<rbrakk> \<Longrightarrow> (n + m - Suc 0) div m < Suc k proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>0 < m; n \<le> m * k; b = m * k\<rbrakk> \<Longrightarrow> n + m - Suc 0 < m + k * m proof (prove)
goal:
No subgoals!
theory Untyped_AI

lemma nat_diff_less2:
  fixes x :: nat
  shows "\<lbrakk> x < y + z; 0 < y\<rbrakk> \<Longrightarrow> x - z < y" apply (cases "z \<le> x") apply (metis nat_diff_less) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x < y + z; 0 < y\<rbrakk> \<Longrightarrow> x - z < y proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x < y + z; 0 < y; z \<le> x\<rbrakk> \<Longrightarrow> x - z < y
 2. \<lbrakk>x < y + z; 0 < y; \<not> z \<le> x\<rbrakk> \<Longrightarrow> x - z < y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x < y + z; 0 < y; \<not> z \<le> x\<rbrakk> \<Longrightarrow> x - z < y proof (prove)
goal:
No subgoals!
theory Untyped_AI

lemma do_machine_op_ex_cte_cap_wp_to[wp]:
  "\<lbrace>ex_cte_cap_wp_to P slot\<rbrace>
    do_machine_op oper
   \<lbrace>\<lambda>rv s. ex_cte_cap_wp_to P slot s\<rbrace>" apply (simp add: do_machine_op_def split_def) apply wp apply (clarsimp simp: ex_cte_cap_wp_to_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ex_cte_cap_wp_to P slot\<rbrace> do_machine_op oper \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P slot\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>ex_cte_cap_wp_to P slot\<rbrace> do ms <- gets machine_state;
p <- select_f (oper ms);
y <- modify (machine_state_update (\<lambda>_. snd p));
return (fst p)
od \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P slot\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. ex_cte_cap_wp_to P slot s \<Longrightarrow> \<forall>x\<in>fst (oper (machine_state s)). ex_cte_cap_wp_to P slot (s\<lparr>machine_state := snd x\<rparr>) proof (prove)
goal:
No subgoals!
theory Untyped_AI

lemma  delete_objects_real_cte_at[wp]:
  "\<lbrace>\<lambda>s. real_cte_at p s \<and> fst p \<notin> {ptr_base .. ptr_base + 2 ^ sz - 1}\<rbrace>
    delete_objects ptr_base sz
  \<lbrace>\<lambda>rv. real_cte_at p\<rbrace>" by (wp | simp add: delete_objects_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. real_cte_at p s \<and> fst p \<notin> {ptr_base..ptr_base + 2 ^ sz - 1}\<rbrace> delete_objects ptr_base sz \<lbrace>\<lambda>rv. real_cte_at p\<rbrace>
theory Untyped_AI

lemma  delete_objects_ct_in_state[wp]:
  "\<lbrace>\<lambda>s. ct_in_state P s \<and> cur_thread s \<notin> {ptr_base .. ptr_base + 2 ^ sz - 1}\<rbrace>
    delete_objects ptr_base sz
  \<lbrace>\<lambda>rv. ct_in_state P\<rbrace>" apply (rule hoare_pre) apply (wp | simp add: delete_objects_def ct_in_state_def
                         st_tcb_at_def
             | simp add: detype_def)+ apply (rule hoare_lift_Pf2[where f=cur_thread]) apply wp+ apply (clarsimp simp: ct_in_state_def st_tcb_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. ct_in_state P s \<and> cur_thread s \<notin> {ptr_base..ptr_base + 2 ^ sz - 1}\<rbrace> delete_objects ptr_base sz \<lbrace>\<lambda>rv. ct_in_state P\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> delete_objects ptr_base sz \<lbrace>\<lambda>rv. ct_in_state P\<rbrace>
 2. \<And>s. ct_in_state P s \<and> cur_thread s \<notin> {ptr_base..ptr_base + 2 ^ sz - 1} \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'8\<rbrace> do_machine_op (freeMemory ptr_base sz) \<lbrace>\<lambda>rv s. obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> P (tcb_state tcb)) (cur_thread s) s\<rbrace>
 2. \<And>s. ct_in_state P s \<and> cur_thread s \<notin> {ptr_base..ptr_base + 2 ^ sz - 1} \<Longrightarrow> (ptr_base \<le> cur_thread s \<longrightarrow> \<not> cur_thread s \<le> ptr_base + 2 ^ sz - 1) \<and> ?P'8 s proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrace>?Q11 x\<rbrace> do_machine_op (freeMemory ptr_base sz) \<lbrace>\<lambda>_. obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> P (tcb_state tcb)) x\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> do_machine_op (freeMemory ptr_base sz) \<lbrace>\<lambda>_ s. P (cur_thread s)\<rbrace>
 3. \<And>s. ct_in_state P s \<and> cur_thread s \<notin> {ptr_base..ptr_base + 2 ^ sz - 1} \<Longrightarrow> (ptr_base \<le> cur_thread s \<longrightarrow> \<not> cur_thread s \<le> ptr_base + 2 ^ sz - 1) \<and> ?Q11 (cur_thread s) s proof (prove)
goal (1 subgoal):
 1. \<And>s. ct_in_state P s \<and> cur_thread s \<notin> {ptr_base..ptr_base + 2 ^ sz - 1} \<Longrightarrow> (ptr_base \<le> cur_thread s \<longrightarrow> \<not> cur_thread s \<le> ptr_base + 2 ^ sz - 1) \<and> obj_at (\<lambda>a. \<exists>tcb. a = TCB tcb \<and> P (tcb_state tcb)) (cur_thread s) s proof (prove)
goal:
No subgoals!
theory Untyped_AI

lemma pspace_no_overlap_subset:
  "pspace_no_overlap S s \<Longrightarrow> T \<subseteq> S
    \<Longrightarrow> pspace_no_overlap T s" by (clarsimp simp: pspace_no_overlap_def disjoint_subset2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_no_overlap S s; T \<subseteq> S\<rbrakk> \<Longrightarrow> pspace_no_overlap T s
theory Untyped_AI

lemma ct_in_state_trans_state[simp]:
  "ct_in_state P (trans_state a s) = ct_in_state P s" by (simp add: ct_in_state_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ct_in_state P (trans_state a s) = ct_in_state P s
theory Untyped_AI

lemma create_cap_iflive[wp]:
  "\<lbrace>if_live_then_nonz_cap
     and cte_wp_at ((=) cap.NullCap) cref\<rbrace>
     create_cap tp sz p dev (cref, oref)
   \<lbrace>\<lambda>rv. if_live_then_nonz_cap\<rbrace>" apply (simp add: create_cap_def) apply (wp new_cap_iflive set_cdt_cte_wp_at | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_live_then_nonz_cap and cte_wp_at ((=) NullCap) cref\<rbrace> create_cap tp sz p dev (cref, oref) \<lbrace>\<lambda>rv. if_live_then_nonz_cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_live_then_nonz_cap and cte_wp_at ((=) NullCap) cref\<rbrace> do dest_p <- gets (\<lambda>s. cdt s cref);
cdt <- gets cdt;
y <- set_cdt (cdt(cref \<mapsto> p));
y <- do_extended_op (create_cap_ext p cref dest_p);
y <- set_original cref True;
set_cap (default_cap tp oref sz dev) cref
od \<lbrace>\<lambda>rv. if_live_then_nonz_cap\<rbrace> proof (prove)
goal:
No subgoals!
theory Untyped_AI

lemma set_cdt_state_refs_of[wp]:
  "\<lbrace>\<lambda>s. P (state_refs_of s)\<rbrace>
     set_cdt m
   \<lbrace>\<lambda>rv s. P (state_refs_of s)\<rbrace>" apply (simp add: set_cdt_def) apply wp apply (clarsimp elim!: state_refs_of_pspaceI) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (state_refs_of s)\<rbrace> set_cdt m \<lbrace>\<lambda>rv s. P (state_refs_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (state_refs_of s)\<rbrace> do s <- get;
put (s\<lparr>cdt := m\<rparr>)
od \<lbrace>\<lambda>rv s. P (state_refs_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (state_refs_of s) \<Longrightarrow> P (state_refs_of (s\<lparr>cdt := m\<rparr>)) proof (prove)
goal:
No subgoals!
theory Untyped_AI

lemma set_cdt_state_hyp_refs_of[wp]:
  "\<lbrace>\<lambda>s. P (state_hyp_refs_of s)\<rbrace>
     set_cdt m
   \<lbrace>\<lambda>rv s. P (state_hyp_refs_of s)\<rbrace>" apply (simp add: set_cdt_def) apply wp apply (clarsimp elim!: state_hyp_refs_of_pspaceI) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (state_hyp_refs_of s)\<rbrace> set_cdt m \<lbrace>\<lambda>rv s. P (state_hyp_refs_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (state_hyp_refs_of s)\<rbrace> do s <- get;
put (s\<lparr>cdt := m\<rparr>)
od \<lbrace>\<lambda>rv s. P (state_hyp_refs_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (state_hyp_refs_of s) \<Longrightarrow> P (state_hyp_refs_of (s\<lparr>cdt := m\<rparr>)) proof (prove)
goal:
No subgoals!
theory Untyped_AI

lemma state_refs_of_rvk[simp]:
  "state_refs_of (is_original_cap_update f s) = state_refs_of s" by (simp add: state_refs_of_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. state_refs_of (is_original_cap_update f s) = state_refs_of s
theory Untyped_AI

lemma create_cap_state_refs_of[wp]:
  "\<lbrace>\<lambda>s. P (state_refs_of s)\<rbrace>
     create_cap tp sz p dev (cref, oref)
   \<lbrace>\<lambda>rv s. P (state_refs_of s)\<rbrace>" unfolding create_cap_def by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (state_refs_of s)\<rbrace> create_cap tp sz p dev (cref, oref) \<lbrace>\<lambda>rv s. P (state_refs_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (state_refs_of s)\<rbrace> case (cref, oref) of (dest, oref) \<Rightarrow> do dest_p <- gets (\<lambda>s. cdt s dest);
cdt <- gets cdt;
set_cdt (cdt(dest \<mapsto> p));
do_extended_op (create_cap_ext p dest dest_p);
set_original dest True;
set_cap (default_cap tp oref sz dev) dest
od \<lbrace>\<lambda>rv s. P (state_refs_of s)\<rbrace>
theory Untyped_AI

lemma create_cap_state_hyp_refs_of[wp]:
  "\<lbrace>\<lambda>s. P (state_hyp_refs_of s)\<rbrace>
     create_cap tp sz p dev (cref, oref)
   \<lbrace>\<lambda>rv s. P (state_hyp_refs_of s)\<rbrace>" apply (simp add: create_cap_def) apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (state_hyp_refs_of s)\<rbrace> create_cap tp sz p dev (cref, oref) \<lbrace>\<lambda>rv s. P (state_hyp_refs_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (state_hyp_refs_of s)\<rbrace> do dest_p <- gets (\<lambda>s. cdt s cref);
cdt <- gets cdt;
y <- set_cdt (cdt(cref \<mapsto> p));
y <- do_extended_op (create_cap_ext p cref dest_p);
y <- set_original cref True;
set_cap (default_cap tp oref sz dev) cref
od \<lbrace>\<lambda>rv s. P (state_hyp_refs_of s)\<rbrace> proof (prove)
goal:
No subgoals!
theory Untyped_AI

lemma create_cap_zombies[wp]:
  "\<lbrace>zombies_final and cte_wp_at ((=) cap.NullCap) cref
     and (\<lambda>s. \<forall>r\<in>obj_refs (default_cap tp oref sz dev). \<forall>p'. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) p' s)\<rbrace>
     create_cap tp sz p dev (cref, oref)
   \<lbrace>\<lambda>rv. zombies_final\<rbrace>" unfolding create_cap_def set_cdt_def by (wpsimp wp: new_cap_zombies)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>zombies_final and cte_wp_at ((=) NullCap) cref and (\<lambda>s. \<forall>r\<in>obj_refs (default_cap tp oref sz dev). \<forall>p'. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) p' s)\<rbrace> create_cap tp sz p dev (cref, oref) \<lbrace>\<lambda>rv. zombies_final\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>zombies_final and cte_wp_at ((=) NullCap) cref and (\<lambda>s. \<forall>r\<in>obj_refs (default_cap tp oref sz dev). \<forall>p'. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) p' s)\<rbrace> case (cref, oref) of (dest, oref) \<Rightarrow> do dest_p <- gets (\<lambda>s. cdt s dest);
cdt <- gets cdt;
do s <- get;
put $ s\<lparr>cdt := cdt(dest \<mapsto> p)\<rparr>
od;
do_extended_op (create_cap_ext p dest dest_p);
set_original dest True;
set_cap (default_cap tp oref sz dev) dest
od \<lbrace>\<lambda>rv. zombies_final\<rbrace>
theory Untyped_AI

lemma create_cap_cur_tcb[wp]:
  "\<lbrace>cur_tcb\<rbrace> create_cap tp sz p dev tup \<lbrace>\<lambda>rv. cur_tcb\<rbrace>" unfolding create_cap_def split_def set_cdt_def by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cur_tcb\<rbrace> create_cap tp sz p dev tup \<lbrace>\<lambda>rv. cur_tcb\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cur_tcb\<rbrace> do dest_p <- gets (\<lambda>s. cdt s (fst tup));
cdt <- gets cdt;
do s <- get;
put $ s\<lparr>cdt := cdt(fst tup \<mapsto> p)\<rparr>
od;
do_extended_op (create_cap_ext p (fst tup) dest_p);
set_original (fst tup) True;
set_cap (default_cap tp (snd tup) sz dev) (fst tup)
od \<lbrace>\<lambda>rv. cur_tcb\<rbrace>
theory Untyped_AI

lemma create_cap_valid_idle[wp]:
  "\<lbrace>valid_idle\<rbrace>
     create_cap tp sz p dev tup
   \<lbrace>\<lambda>rv. valid_idle\<rbrace>" unfolding create_cap_def split_def set_cdt_def by (wpsimp wp: set_cap_idle)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_idle\<rbrace> create_cap tp sz p dev tup \<lbrace>\<lambda>rv. valid_idle\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_idle\<rbrace> do dest_p <- gets (\<lambda>s. cdt s (fst tup));
cdt <- gets cdt;
do s <- get;
put $ s\<lparr>cdt := cdt(fst tup \<mapsto> p)\<rparr>
od;
do_extended_op (create_cap_ext p (fst tup) dest_p);
set_original (fst tup) True;
set_cap (default_cap tp (snd tup) sz dev) (fst tup)
od \<lbrace>\<lambda>rv. valid_idle\<rbrace>