theory Ipc_AI

lemma setup_caller_cap_refs_respects_device_region[wp]:
    "\<lbrace>cap_refs_respects_device_region and
     valid_objs\<rbrace>
    setup_caller_cap tcb cap grant
    \<lbrace>\<lambda>_. cap_refs_respects_device_region\<rbrace>" apply (simp add: setup_caller_cap_def set_thread_state_def)+ apply (intro conjI impI) apply (wp set_object_cap_refs_respects_device_region set_object_cte_wp_at | clarsimp )+ apply (clarsimp dest!: get_tcb_SomeD simp: tcb_cap_cases_def obj_at_def cap_range_def) apply (rule tcb_at_cte_at_2) apply (simp add: tcb_at_def get_tcb_def) apply (wp set_object_cap_refs_respects_device_region set_object_cte_wp_at | clarsimp )+ apply (clarsimp dest!: get_tcb_SomeD simp: tcb_cap_cases_def obj_at_def cap_range_def) apply (rule tcb_at_cte_at_2) apply (simp add: tcb_at_def get_tcb_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cap_refs_respects_device_region and valid_objs\<rbrace> setup_caller_cap tcb cap grant \<lbrace>\<lambda>_. cap_refs_respects_device_region\<rbrace> proof (prove)
goal (1 subgoal):
 1. (grant \<longrightarrow> \<lbrace>cap_refs_respects_device_region and valid_objs\<rbrace> do y <- do tcba <- gets_the (get_tcb tcb);
y <- set_object tcb (TCB (tcba\<lparr>tcb_state := BlockedOnReply\<rparr>));
do_extended_op (set_thread_state_ext tcb)
od;
cap_insert (ReplyCap tcb False {AllowGrant, AllowWrite}) (tcb, tcb_cnode_index 2) (cap, tcb_cnode_index 3)
od \<lbrace>\<lambda>_. cap_refs_respects_device_region\<rbrace>) \<and> (\<not> grant \<longrightarrow> \<lbrace>cap_refs_respects_device_region and valid_objs\<rbrace> do y <- do tcba <- gets_the (get_tcb tcb);
y <- set_object tcb (TCB (tcba\<lparr>tcb_state := BlockedOnReply\<rparr>));
do_extended_op (set_thread_state_ext tcb)
od;
cap_insert (ReplyCap tcb False {AllowWrite}) (tcb, tcb_cnode_index 2) (cap, tcb_cnode_index 3)
od \<lbrace>\<lambda>_. cap_refs_respects_device_region\<rbrace>) proof (prove)
goal (2 subgoals):
 1. grant \<Longrightarrow> \<lbrace>cap_refs_respects_device_region and valid_objs\<rbrace> do y <- do tcba <- gets_the (get_tcb tcb);
y <- set_object tcb (TCB (tcba\<lparr>tcb_state := BlockedOnReply\<rparr>));
do_extended_op (set_thread_state_ext tcb)
od;
cap_insert (ReplyCap tcb False {AllowGrant, AllowWrite}) (tcb, tcb_cnode_index 2) (cap, tcb_cnode_index 3)
od \<lbrace>\<lambda>_. cap_refs_respects_device_region\<rbrace>
 2. \<not> grant \<Longrightarrow> \<lbrace>cap_refs_respects_device_region and valid_objs\<rbrace> do y <- do tcba <- gets_the (get_tcb tcb);
y <- set_object tcb (TCB (tcba\<lparr>tcb_state := BlockedOnReply\<rparr>));
do_extended_op (set_thread_state_ext tcb)
od;
cap_insert (ReplyCap tcb False {AllowWrite}) (tcb, tcb_cnode_index 2) (cap, tcb_cnode_index 3)
od \<lbrace>\<lambda>_. cap_refs_respects_device_region\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s y. \<lbrakk>grant; cap_refs_respects_device_region s; valid_objs s; get_tcb tcb s = Some y\<rbrakk> \<Longrightarrow> obj_at (\<lambda>val. \<exists>tcb'. val = TCB tcb' \<and> (\<forall>x\<in>ran tcb_cap_cases. case x of (getF, t) \<Rightarrow> getF tcb' = getF (y\<lparr>tcb_state := BlockedOnReply\<rparr>))) tcb s \<and> cte_wp_at (\<lambda>c. cap_range (ReplyCap tcb False {AllowGrant, AllowWrite}) \<subseteq> cap_range c \<and> (cap_range (ReplyCap tcb False {AllowGrant, AllowWrite}) \<noteq> {} \<longrightarrow> \<not> cap_is_device c)) (tcb, tcb_cnode_index 2) (s\<lparr>kheap := (kheap s)(tcb \<mapsto> TCB (y\<lparr>tcb_state := BlockedOnReply\<rparr>))\<rparr>)
 2. \<not> grant \<Longrightarrow> \<lbrace>cap_refs_respects_device_region and valid_objs\<rbrace> do y <- do tcba <- gets_the (get_tcb tcb);
y <- set_object tcb (TCB (tcba\<lparr>tcb_state := BlockedOnReply\<rparr>));
do_extended_op (set_thread_state_ext tcb)
od;
cap_insert (ReplyCap tcb False {AllowWrite}) (tcb, tcb_cnode_index 2) (cap, tcb_cnode_index 3)
od \<lbrace>\<lambda>_. cap_refs_respects_device_region\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s y. \<lbrakk>grant; cap_refs_respects_device_region s; valid_objs s; kheap s tcb = Some (TCB y)\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. True) (tcb, tcb_cnode_index 2) (s\<lparr>kheap := (kheap s)(tcb \<mapsto> TCB (y\<lparr>tcb_state := BlockedOnReply\<rparr>))\<rparr>)
 2. \<not> grant \<Longrightarrow> \<lbrace>cap_refs_respects_device_region and valid_objs\<rbrace> do y <- do tcba <- gets_the (get_tcb tcb);
y <- set_object tcb (TCB (tcba\<lparr>tcb_state := BlockedOnReply\<rparr>));
do_extended_op (set_thread_state_ext tcb)
od;
cap_insert (ReplyCap tcb False {AllowWrite}) (tcb, tcb_cnode_index 2) (cap, tcb_cnode_index 3)
od \<lbrace>\<lambda>_. cap_refs_respects_device_region\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s y. \<lbrakk>grant; cap_refs_respects_device_region s; valid_objs s; kheap s tcb = Some (TCB y)\<rbrakk> \<Longrightarrow> tcb_at tcb (s\<lparr>kheap := (kheap s)(tcb \<mapsto> TCB (y\<lparr>tcb_state := BlockedOnReply\<rparr>))\<rparr>)
 2. \<not> grant \<Longrightarrow> \<lbrace>cap_refs_respects_device_region and valid_objs\<rbrace> do y <- do tcba <- gets_the (get_tcb tcb);
y <- set_object tcb (TCB (tcba\<lparr>tcb_state := BlockedOnReply\<rparr>));
do_extended_op (set_thread_state_ext tcb)
od;
cap_insert (ReplyCap tcb False {AllowWrite}) (tcb, tcb_cnode_index 2) (cap, tcb_cnode_index 3)
od \<lbrace>\<lambda>_. cap_refs_respects_device_region\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<not> grant \<Longrightarrow> \<lbrace>cap_refs_respects_device_region and valid_objs\<rbrace> do y <- do tcba <- gets_the (get_tcb tcb);
y <- set_object tcb (TCB (tcba\<lparr>tcb_state := BlockedOnReply\<rparr>));
do_extended_op (set_thread_state_ext tcb)
od;
cap_insert (ReplyCap tcb False {AllowWrite}) (tcb, tcb_cnode_index 2) (cap, tcb_cnode_index 3)
od \<lbrace>\<lambda>_. cap_refs_respects_device_region\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>\<not> grant; cap_refs_respects_device_region s; valid_objs s; get_tcb tcb s = Some y\<rbrakk> \<Longrightarrow> obj_at (\<lambda>val. \<exists>tcb'. val = TCB tcb' \<and> (\<forall>x\<in>ran tcb_cap_cases. case x of (getF, t) \<Rightarrow> getF tcb' = getF (y\<lparr>tcb_state := BlockedOnReply\<rparr>))) tcb s \<and> cte_wp_at (\<lambda>c. cap_range (ReplyCap tcb False {AllowWrite}) \<subseteq> cap_range c \<and> (cap_range (ReplyCap tcb False {AllowWrite}) \<noteq> {} \<longrightarrow> \<not> cap_is_device c)) (tcb, tcb_cnode_index 2) (s\<lparr>kheap := (kheap s)(tcb \<mapsto> TCB (y\<lparr>tcb_state := BlockedOnReply\<rparr>))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>\<not> grant; cap_refs_respects_device_region s; valid_objs s; kheap s tcb = Some (TCB y)\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. True) (tcb, tcb_cnode_index 2) (s\<lparr>kheap := (kheap s)(tcb \<mapsto> TCB (y\<lparr>tcb_state := BlockedOnReply\<rparr>))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>\<not> grant; cap_refs_respects_device_region s; valid_objs s; kheap s tcb = Some (TCB y)\<rbrakk> \<Longrightarrow> tcb_at tcb (s\<lparr>kheap := (kheap s)(tcb \<mapsto> TCB (y\<lparr>tcb_state := BlockedOnReply\<rparr>))\<rparr>) proof (prove)
goal:
No subgoals!