theory DetSchedAux_AI

lemma retype_region_etcb_at:"\<lbrace>(\<lambda>s. etcb_at P t s) and valid_etcbs\<rbrace> retype_region a b c d dev \<lbrace>\<lambda>r s. st_tcb_at (Not o inactive) t s \<longrightarrow> etcb_at P t s\<rbrace> " apply (simp add: retype_region_def) apply (simp add: retype_region_ext_def bind_assoc) apply wp apply (clarsimp simp add: pred_tcb_at_def obj_at_def simp del: fun_upd_apply) apply (blast intro: retype_etcb_at_helper) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>etcb_at P t and valid_etcbs\<rbrace> retype_region a b c d dev \<lbrace>\<lambda>r s. st_tcb_at (Not \<circ> inactive) t s \<longrightarrow> etcb_at P t s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>etcb_at P t and valid_etcbs\<rbrace> do y <- when (d \<noteq> Untyped) (do kh <- gets kheap;
y <- retype_region_ext (map (\<lambda>p. ptr_add a (p * 2 ^ obj_bits_api d c)) [0..<b]) d;
modify (kheap_update (\<lambda>y. foldr (\<lambda>p kh. kh(p \<mapsto> default_object d dev c)) (map (\<lambda>p. ptr_add a (p * 2 ^ obj_bits_api d c)) [0..<b]) kh))
od);
return (map (\<lambda>p. ptr_add a (p * 2 ^ obj_bits_api d c)) [0..<b])
od \<lbrace>\<lambda>r s. st_tcb_at (Not \<circ> inactive) t s \<longrightarrow> etcb_at P t s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>etcb_at P t and valid_etcbs\<rbrace> do y <- when (d \<noteq> Untyped) (do kh <- gets kheap;
x <- gets ekheap;
xa <- gets cur_domain;
y <- modify (ekheap_update (\<lambda>_. foldr (\<lambda>p ekh. ekh(p := default_ext d xa)) (map (\<lambda>p. ptr_add a (p * 2 ^ obj_bits_api d c)) [0..<b]) x));
modify (kheap_update (\<lambda>y. foldr (\<lambda>p kh. kh(p \<mapsto> default_object d dev c)) (map (\<lambda>p. ptr_add a (p * 2 ^ obj_bits_api d c)) [0..<b]) kh))
od);
return (map (\<lambda>p. ptr_add a (p * 2 ^ obj_bits_api d c)) [0..<b])
od \<lbrace>\<lambda>r s. st_tcb_at (Not \<circ> inactive) t s \<longrightarrow> etcb_at P t s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (etcb_at P t and valid_etcbs) s \<Longrightarrow> (if d \<noteq> Untyped then \<lambda>s. st_tcb_at (Not \<circ> inactive) t (s\<lparr>ekheap := foldr (\<lambda>p ekh. ekh(p := default_ext d (cur_domain s))) (map (\<lambda>p. ptr_add a (p * 2 ^ obj_bits_api d c)) [0..<b]) (ekheap s), kheap := foldr (\<lambda>p kh. kh(p \<mapsto> default_object d dev c)) (map (\<lambda>p. ptr_add a (p * 2 ^ obj_bits_api d c)) [0..<b]) (kheap s)\<rparr>) \<longrightarrow> etcb_at P t (s\<lparr>ekheap := foldr (\<lambda>p ekh. ekh(p := default_ext d (cur_domain s))) (map (\<lambda>p. ptr_add a (p * 2 ^ obj_bits_api d c)) [0..<b]) (ekheap s), kheap := foldr (\<lambda>p kh. kh(p \<mapsto> default_object d dev c)) (map (\<lambda>p. ptr_add a (p * 2 ^ obj_bits_api d c)) [0..<b]) (kheap s)\<rparr>) else (\<lambda>a. st_tcb_at (Not \<circ> inactive) t a \<longrightarrow> etcb_at P t a)) s proof (prove)
goal (1 subgoal):
 1. \<And>s tcb. \<lbrakk>etcb_at P t s; valid_etcbs s; d \<noteq> Untyped; foldr (\<lambda>p kh. kh(p \<mapsto> default_object d dev c)) (map (\<lambda>p. ptr_add a (p * 2 ^ obj_bits_api d c)) [0..<b]) (kheap s) t = Some (TCB tcb); tcb_state tcb \<noteq> Inactive\<rbrakk> \<Longrightarrow> etcb_at' P t (foldr (\<lambda>p ekh. ekh(p := default_ext d (cur_domain s))) (map (\<lambda>p. ptr_add a (p * 2 ^ obj_bits_api d c)) [0..<b]) (ekheap s)) proof (prove)
goal:
No subgoals!