theory Tcb_AI

lemma (in Tcb_AI) decode_set_space_wf[wp]:
  "\<lbrace>(invs::('state_ext::state_ext) state\<Rightarrow>bool)
  and tcb_at t and cte_at slot and ex_cte_cap_to slot
          and ex_nonz_cap_to t
          and (\<lambda>s. \<forall>x \<in> set extras. s \<turnstile> fst x \<and> cte_at (snd x) s
                          \<and> ex_cte_cap_to (snd x) s
                          \<and> t \<noteq> fst (snd x)
                          \<and> no_cap_to_obj_dr_emp (fst x) s)\<rbrace>
     decode_set_space args (ThreadCap t) slot extras
   \<lbrace>tcb_inv_wf\<rbrace>,-" apply (simp   add: decode_set_space_def whenE_def unlessE_def
          split del: if_split) apply (rule hoare_pre) apply (wp derive_cap_valid_cap
             | simp add: o_def split del: if_split
             | rule hoare_drop_imps)+ apply (clarsimp split del: if_split simp: ball_conj_distrib
                   simp del: length_greater_0_conv) apply (simp add: update_cap_data_validI word_bits_def
                   no_cap_to_obj_with_diff_ref_update_cap_data
              del: length_greater_0_conv) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and tcb_at t and cte_wp_at (\<lambda>_. True) slot and ex_cte_cap_wp_to (\<lambda>_. True) slot and ex_nonz_cap_to t and (\<lambda>s. \<forall>x\<in>set extras. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>_. True) (snd x) s \<and> ex_cte_cap_wp_to (\<lambda>_. True) (snd x) s \<and> t \<noteq> fst (snd x) \<and> no_cap_to_obj_dr_emp (fst x) s)\<rbrace> decode_set_space args (ThreadCap t) slot extras \<lbrace>tcb_inv_wf\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and tcb_at t and cte_wp_at (\<lambda>_. True) slot and ex_cte_cap_wp_to (\<lambda>_. True) slot and ex_nonz_cap_to t and (\<lambda>s. \<forall>x\<in>set extras. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>_. True) (snd x) s \<and> ex_cte_cap_wp_to (\<lambda>_. True) (snd x) s \<and> t \<noteq> fst (snd x) \<and> no_cap_to_obj_dr_emp (fst x) s)\<rbrace> doE y <- if length args < 3 \<or> length extras < 2 then throwError TruncatedMessage else returnOk ();
can_chg_cr <- liftE (liftM Not (slot_cap_long_running_delete (get_tcb_ctable_ptr t)));
can_chg_vr <- liftE (liftM Not (slot_cap_long_running_delete (get_tcb_vtable_ptr t)));
y <- if can_chg_cr \<and> can_chg_vr then returnOk () else throwError IllegalOperation;
croot_cap' <- derive_cap (snd (extras ! 0)) ((if args ! Suc 0 = 0 then id else update_cap_data False (args ! Suc 0)) (fst (extras ! 0)));
y <- if is_cnode_cap croot_cap' then returnOk () else throwError IllegalOperation;
vroot_cap' <- derive_cap (snd (extras ! Suc 0)) ((if args ! 2 = 0 then id else update_cap_data False (args ! 2)) (fst (extras ! Suc 0)));
y <- if is_valid_vtable_root vroot_cap' then returnOk () else throwError IllegalOperation;
returnOk (ThreadControl t slot (Some (to_bl (args ! 0))) None None (Some (croot_cap', snd (extras ! 0))) (Some (vroot_cap', snd (extras ! Suc 0))) None)
odE \<lbrace>tcb_inv_wf\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'1\<rbrace> doE y <- if length args < 3 \<or> length extras < 2 then throwError TruncatedMessage else returnOk ();
can_chg_cr <- liftE (liftM Not (slot_cap_long_running_delete (get_tcb_ctable_ptr t)));
can_chg_vr <- liftE (liftM Not (slot_cap_long_running_delete (get_tcb_vtable_ptr t)));
y <- if can_chg_cr \<and> can_chg_vr then returnOk () else throwError IllegalOperation;
croot_cap' <- derive_cap (snd (extras ! 0)) ((if args ! Suc 0 = 0 then id else update_cap_data False (args ! Suc 0)) (fst (extras ! 0)));
y <- if is_cnode_cap croot_cap' then returnOk () else throwError IllegalOperation;
vroot_cap' <- derive_cap (snd (extras ! Suc 0)) ((if args ! 2 = 0 then id else update_cap_data False (args ! 2)) (fst (extras ! Suc 0)));
y <- if is_valid_vtable_root vroot_cap' then returnOk () else throwError IllegalOperation;
returnOk (ThreadControl t slot (Some (to_bl (args ! 0))) None None (Some (croot_cap', snd (extras ! 0))) (Some (vroot_cap', snd (extras ! Suc 0))) None)
odE \<lbrace>tcb_inv_wf\<rbrace>, -
 2. \<And>s. (invs and tcb_at t and cte_wp_at (\<lambda>_. True) slot and ex_cte_cap_wp_to (\<lambda>_. True) slot and ex_nonz_cap_to t and (\<lambda>s. \<forall>x\<in>set extras. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>_. True) (snd x) s \<and> ex_cte_cap_wp_to (\<lambda>_. True) (snd x) s \<and> t \<noteq> fst (snd x) \<and> no_cap_to_obj_dr_emp (fst x) s)) s \<Longrightarrow> ?P'1 s proof (prove)
goal (1 subgoal):
 1. \<And>s. invs s \<and> tcb_at t s \<and> cte_wp_at (\<lambda>_. True) slot s \<and> ex_cte_cap_wp_to (\<lambda>_. True) slot s \<and> ex_nonz_cap_to t s \<and> (\<forall>x\<in>set extras. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>_. True) (snd x) s \<and> ex_cte_cap_wp_to (\<lambda>_. True) (snd x) s \<and> t \<noteq> fst (snd x) \<and> no_cap_to_obj_dr_emp (fst x) s) \<Longrightarrow> \<not> length args < 3 \<and> \<not> length extras < 2 \<longrightarrow> s \<turnstile> (if args ! Suc 0 = 0 then \<lambda>a. a else update_cap_data False (args ! Suc 0)) (fst (extras ! 0)) \<and> cte_wp_at (\<lambda>_. True) (snd (extras ! 0)) s \<and> ex_cte_cap_wp_to (\<lambda>_. True) (snd (extras ! 0)) s \<and> no_cap_to_obj_dr_emp ((if args ! Suc 0 = 0 then \<lambda>a. a else update_cap_data False (args ! Suc 0)) (fst (extras ! 0))) s \<and> s \<turnstile> (if args ! 2 = 0 then \<lambda>a. a else update_cap_data False (args ! 2)) (fst (extras ! Suc 0)) \<and> no_cap_to_obj_dr_emp ((if args ! 2 = 0 then \<lambda>a. a else update_cap_data False (args ! 2)) (fst (extras ! Suc 0))) s \<and> word_bits = 32 proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>invs s; tcb_at t s; cte_wp_at (\<lambda>_. True) slot s; ex_cte_cap_wp_to (\<lambda>_. True) slot s; ex_nonz_cap_to t s; \<forall>x\<in>set extras. s \<turnstile> fst x; \<forall>x\<in>set extras. cte_wp_at (\<lambda>_. True) (snd x) s; \<forall>x\<in>set extras. ex_cte_cap_wp_to (\<lambda>_. True) (snd x) s; \<forall>x\<in>set extras. t \<noteq> fst (snd x); \<forall>x\<in>set extras. no_cap_to_obj_dr_emp (fst x) s; \<not> length args < 3; \<not> length extras < 2\<rbrakk> \<Longrightarrow> s \<turnstile> (if args ! Suc 0 = 0 then \<lambda>a. a else update_cap_data False (args ! Suc 0)) (fst (extras ! 0)) \<and> no_cap_to_obj_dr_emp ((if args ! Suc 0 = 0 then \<lambda>a. a else update_cap_data False (args ! Suc 0)) (fst (extras ! 0))) s \<and> s \<turnstile> (if args ! 2 = 0 then \<lambda>a. a else update_cap_data False (args ! 2)) (fst (extras ! Suc 0)) \<and> no_cap_to_obj_dr_emp ((if args ! 2 = 0 then \<lambda>a. a else update_cap_data False (args ! 2)) (fst (extras ! Suc 0))) s \<and> word_bits = 32 proof (prove)
goal:
No subgoals!