theory Syscall_AI

lemma (in Systemcall_AI_Pre) handle_fault_reply_cte_wp_at:
  "\<lbrace>\<lambda>s :: 'state_ext state. P (cte_wp_at P' p s)\<rbrace>
     handle_fault_reply f t d dl
   \<lbrace>\<lambda>_ s. P (cte_wp_at P' p s)\<rbrace>" proof - have SC:
      "\<And>p' s tcb nc. get_tcb p' s = Some tcb
       \<Longrightarrow> obj_at (same_caps (TCB (tcb \<lparr>tcb_arch := arch_tcb_context_set nc (tcb_arch tcb)\<rparr>))) p' s" apply (drule get_tcb_ko_at [THEN iffD1]) apply (erule ko_at_weakenE) apply (clarsimp simp add: tcb_cap_cases_def) done have NC:
      "\<And>p' s tcb P nc. get_tcb p' s = Some tcb
      \<Longrightarrow> cte_wp_at P p (s\<lparr>kheap := (kheap s)(p' \<mapsto> TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set nc (tcb_arch tcb)\<rparr>))\<rparr>)
          = cte_wp_at P p s" apply (drule_tac nc=nc in SC) apply (drule_tac P=P and p=p in cte_wp_at_after_update) apply (drule sym) apply (clarsimp) apply (rule_tac x="s \<lparr> kheap := p \<rparr>" for p in arg_cong) apply (clarsimp) done show ?thesis apply (case_tac f; clarsimp simp: as_user_def) apply (wp set_object_wp thread_get_wp' | simp add: split_def NC | wp (once) hoare_drop_imps)+ done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cte_wp_at P' p s)\<rbrace> handle_fault_reply f t d dl \<lbrace>\<lambda>_ s. P (cte_wp_at P' p s)\<rbrace> proof (state)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cte_wp_at P' p s)\<rbrace> handle_fault_reply f t d dl \<lbrace>\<lambda>_ s. P (cte_wp_at P' p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>p' s tcb nc. get_tcb p' s = Some tcb \<Longrightarrow> obj_at (same_caps (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set nc (tcb_arch tcb)\<rparr>))) p' s proof (prove)
goal (1 subgoal):
 1. \<And>p' s tcb nc. ko_at (TCB tcb) p' s \<Longrightarrow> obj_at (same_caps (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set nc (tcb_arch tcb)\<rparr>))) p' s proof (prove)
goal (1 subgoal):
 1. \<And>p' s tcb nc. same_caps (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set nc (tcb_arch tcb)\<rparr>)) (TCB tcb) proof (prove)
goal:
No subgoals! proof (state)
this:
get_tcb ?p' ?s = Some ?tcb \<Longrightarrow> obj_at (same_caps (TCB (?tcb\<lparr>tcb_arch := arch_tcb_context_set ?nc (tcb_arch ?tcb)\<rparr>))) ?p' ?s

goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cte_wp_at P' p s)\<rbrace> handle_fault_reply f t d dl \<lbrace>\<lambda>_ s. P (cte_wp_at P' p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>p' s tcb P nc. get_tcb p' s = Some tcb \<Longrightarrow> cte_wp_at P p (s\<lparr>kheap := (kheap s)(p' \<mapsto> TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set nc (tcb_arch tcb)\<rparr>))\<rparr>) = cte_wp_at P p s proof (prove)
goal (1 subgoal):
 1. \<And>p' s tcb P nc. obj_at (same_caps (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set nc (tcb_arch tcb)\<rparr>))) p' s \<Longrightarrow> cte_wp_at P p (s\<lparr>kheap := (kheap s)(p' \<mapsto> TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set nc (tcb_arch tcb)\<rparr>))\<rparr>) = cte_wp_at P p s proof (prove)
goal (1 subgoal):
 1. \<And>p' s tcb P nc. cte_wp_at P p (s\<lparr>kheap := \<lambda>b. if b = p' then Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set nc (tcb_arch tcb)\<rparr>)) else kheap s b\<rparr>) = cte_wp_at P p s \<Longrightarrow> cte_wp_at P p (s\<lparr>kheap := (kheap s)(p' \<mapsto> TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set nc (tcb_arch tcb)\<rparr>))\<rparr>) = cte_wp_at P p s proof (prove)
goal (1 subgoal):
 1. \<And>p' s tcb P nc. cte_wp_at P p s = cte_wp_at P p (s\<lparr>kheap := \<lambda>b. if b = p' then Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set nc (tcb_arch tcb)\<rparr>)) else kheap s b\<rparr>) \<Longrightarrow> cte_wp_at P p (s\<lparr>kheap := (kheap s)(p' \<mapsto> TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set nc (tcb_arch tcb)\<rparr>))\<rparr>) = cte_wp_at P p s proof (prove)
goal (1 subgoal):
 1. \<And>p' s tcb P nc. cte_wp_at P p s = cte_wp_at P p (s\<lparr>kheap := \<lambda>b. if b = p' then Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set nc (tcb_arch tcb)\<rparr>)) else kheap s b\<rparr>) \<Longrightarrow> cte_wp_at P p (s\<lparr>kheap := (kheap s)(p' \<mapsto> TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set nc (tcb_arch tcb)\<rparr>))\<rparr>) = cte_wp_at P p (s\<lparr>kheap := \<lambda>b. if b = p' then Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set nc (tcb_arch tcb)\<rparr>)) else kheap s b\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>p' s tcb P nc. cte_wp_at P p s = cte_wp_at P p (s\<lparr>kheap := \<lambda>b. if b = p' then Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set nc (tcb_arch tcb)\<rparr>)) else kheap s b\<rparr>) \<Longrightarrow> s\<lparr>kheap := (kheap s)(p' \<mapsto> TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set nc (tcb_arch tcb)\<rparr>))\<rparr> = s\<lparr>kheap := \<lambda>b. if b = p' then Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set nc (tcb_arch tcb)\<rparr>)) else kheap s b\<rparr> proof (prove)
goal:
No subgoals! proof (state)
this:
get_tcb ?p'1 ?s1 = Some ?tcb1 \<Longrightarrow> cte_wp_at ?P1 p (?s1\<lparr>kheap := (kheap ?s1)(?p'1 \<mapsto> TCB (?tcb1\<lparr>tcb_arch := arch_tcb_context_set ?nc1 (tcb_arch ?tcb1)\<rparr>))\<rparr>) = cte_wp_at ?P1 p ?s1

goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cte_wp_at P' p s)\<rbrace> handle_fault_reply f t d dl \<lbrace>\<lambda>_ s. P (cte_wp_at P' p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cte_wp_at P' p s)\<rbrace> handle_fault_reply f t d dl \<lbrace>\<lambda>_ s. P (cte_wp_at P' p s)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x2. f = UnknownSyscallException x2 \<Longrightarrow> \<lbrace>\<lambda>s. P (cte_wp_at P' p s)\<rbrace> do ta <- arch_get_sanitise_register_info t;
y <- do tcb <- gets_the (get_tcb t);
(a, uc') <- select_f (zipWithM_x (\<lambda>r v. setRegister r (sanitise_register ta r v)) syscallMessage dl (arch_tcb_context_get (tcb_arch tcb)));
set_object t (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>))
od;
return (d = 0)
od \<lbrace>\<lambda>_ s. P (cte_wp_at P' p s)\<rbrace>
 2. \<And>x31 x32. f = UserException x31 x32 \<Longrightarrow> \<lbrace>\<lambda>s. P (cte_wp_at P' p s)\<rbrace> do ta <- arch_get_sanitise_register_info t;
y <- do tcb <- gets_the (get_tcb t);
(a, uc') <- select_f (zipWithM_x (\<lambda>r v. setRegister r (sanitise_register ta r v)) exceptionMessage dl (arch_tcb_context_get (tcb_arch tcb)));
set_object t (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>))
od;
return (d = 0)
od \<lbrace>\<lambda>_ s. P (cte_wp_at P' p s)\<rbrace>
 3. \<And>x4. f = ArchFault x4 \<Longrightarrow> \<lbrace>\<lambda>s. P (cte_wp_at P' p s)\<rbrace> handle_arch_fault_reply x4 t d dl \<lbrace>\<lambda>_ s. P (cte_wp_at P' p s)\<rbrace> proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>\<lambda>s. P (cte_wp_at P' p s)\<rbrace> handle_fault_reply f t d dl \<lbrace>\<lambda>_ s. P (cte_wp_at P' p s)\<rbrace>

goal:
No subgoals!