theory Retype_R

lemma createNewCaps_cur:
  "\<lbrakk>range_cover ptr sz (APIType_capBits ty us) n ; n \<noteq> 0\<rbrakk> \<Longrightarrow>
   \<lbrace>\<lambda>s. valid_pspace' s \<and>
        pspace_no_overlap' ptr sz s \<and>
        cur_tcb' s\<rbrace>
      createNewCaps ty ptr n us d
   \<lbrace>\<lambda>rv. cur_tcb'\<rbrace>" apply (rule hoare_post_imp [where Q="\<lambda>rv s. \<exists>t. ksCurThread s = t \<and> tcb_at' t s"]) apply (simp add: cur_tcb'_def) apply (wp hoare_vcg_ex_lift createNewCaps_obj_at') apply (clarsimp simp: pspace_no_overlap'_def cur_tcb'_def valid_pspace'_def) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) n; n \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. valid_pspace' s \<and> pspace_no_overlap' ptr sz s \<and> cur_tcb' s\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv. cur_tcb'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) n; n \<noteq> 0; \<exists>t. ksCurThread s = t \<and> tcb_at' t s\<rbrakk> \<Longrightarrow> cur_tcb' s
 2. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) n; n \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. valid_pspace' s \<and> pspace_no_overlap' ptr sz s \<and> cur_tcb' s\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv s. \<exists>t. ksCurThread s = t \<and> tcb_at' t s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) n; n \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. valid_pspace' s \<and> pspace_no_overlap' ptr sz s \<and> cur_tcb' s\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv s. \<exists>t. ksCurThread s = t \<and> tcb_at' t s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) n; n \<noteq> 0; valid_pspace' s \<and> pspace_no_overlap' ptr sz s \<and> cur_tcb' s\<rbrakk> \<Longrightarrow> \<exists>x. ksCurThread s = x \<and> tcb_at' x s \<and> range_cover ptr (?sz7 x) (APIType_capBits ty us) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr (?sz7 x) s \<and> koType TYPE(Structures_H.tcb) \<noteq> koType TYPE(ARM_H.pde) \<and> (\<forall>tcb d. \<not> tcbQueued tcb \<and> tcbState tcb = Structures_H.thread_state.Inactive \<longrightarrow> (\<exists>obj. injectKOS obj = KOTCB (tcbDomain_update (\<lambda>_. d) tcb) \<and> True) = (\<exists>obj. injectKOS obj = KOTCB tcb \<and> True)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) n; 0 < n; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; \<forall>x ko. ksPSpace s x = Some ko \<longrightarrow> x \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) \<longrightarrow> ptr \<le> x + 2 ^ objBitsKO ko - 1 \<longrightarrow> x \<le> x + 2 ^ objBitsKO ko - 1 \<longrightarrow> \<not> ptr \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1); tcb_at' (ksCurThread s) s\<rbrakk> \<Longrightarrow> range_cover ptr (?sz7 (ksCurThread s)) (APIType_capBits ty us) n \<and> (\<forall>x ko. ksPSpace s x = Some ko \<longrightarrow> x \<le> (ptr && ~~ mask (?sz7 (ksCurThread s))) + (2 ^ ?sz7 (ksCurThread s) - 1) \<longrightarrow> ptr \<le> x + 2 ^ objBitsKO ko - 1 \<longrightarrow> x \<le> x + 2 ^ objBitsKO ko - 1 \<longrightarrow> \<not> ptr \<le> (ptr && ~~ mask (?sz7 (ksCurThread s))) + (2 ^ ?sz7 (ksCurThread s) - 1)) proof (prove)
goal:
No subgoals!