kings-crown/FVELER_Isabelle huggingface dataset:
theory Syscall_DR

lemma transform_intent_zombie_cap_None:
  "\<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.Zombie w option n\<rbrakk>
         \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot cap excaps \<lbrace>\<lambda>r. \<bottom>\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>" apply (clarsimp simp:Decode_A.decode_invocation_def) apply (wp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = Zombie w option n\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot cap excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = Zombie w option n\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> throwError (InvalidCapability 0) \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace> proof (prove)
goal:
No subgoals!
theory Syscall_DR

lemma decode_invocation_zombiecap_corres:
  "\<lbrakk> Some intent = transform_intent (invocation_type label') args';
     invoked_cap_ref = transform_cslot_ptr invoked_cap_ref';
     invoked_cap = transform_cap invoked_cap';
     excaps = transform_cap_list excaps';
     invoked_cap' = cap.Zombie x y z \<rbrakk> \<Longrightarrow>
    dcorres (dc \<oplus> cdl_invocation_relation) \<top> \<top>
        (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent)
        (Decode_A.decode_invocation label' args' cap_index' invoked_cap_ref' invoked_cap' excaps')" by (simp add:Decode_A.decode_invocation_def Decode_D.decode_invocation_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Some intent = transform_intent (invocation_type label') args'; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = transform_cap invoked_cap'; excaps = transform_cap_list excaps'; invoked_cap' = Zombie x y z\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label' args' cap_index' invoked_cap_ref' invoked_cap' excaps')
theory Syscall_DR

lemma ct_running_not_idle_etc:
  "\<lbrakk> invs s; ct_running s \<rbrakk> \<Longrightarrow> not_idle_thread (cur_thread s) s \<and> thread_is_running (cur_thread s) s" apply (simp add: not_idle_thread_def ct_in_state_def) apply (subgoal_tac "valid_idle s") apply (clarsimp simp: valid_idle_def pred_tcb_at_def obj_at_def) apply (clarsimp simp: invs_def valid_state_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; ct_running s\<rbrakk> \<Longrightarrow> not_idle_thread (cur_thread s) s \<and> thread_is_running (cur_thread s) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; st_tcb_at (\<lambda>st. st = Running) (cur_thread s) s\<rbrakk> \<Longrightarrow> cur_thread s \<noteq> idle_thread s \<and> thread_is_running (cur_thread s) s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>invs s; st_tcb_at (\<lambda>st. st = Running) (cur_thread s) s; valid_idle s\<rbrakk> \<Longrightarrow> cur_thread s \<noteq> idle_thread s \<and> thread_is_running (cur_thread s) s
 2. \<lbrakk>invs s; st_tcb_at (\<lambda>st. st = Running) (cur_thread s) s\<rbrakk> \<Longrightarrow> valid_idle s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; st_tcb_at (\<lambda>st. st = Running) (cur_thread s) s\<rbrakk> \<Longrightarrow> valid_idle s proof (prove)
goal:
No subgoals!
theory Syscall_DR

lemma ct_active_not_idle_etc:
  "\<lbrakk> invs s; ct_active s \<rbrakk> \<Longrightarrow> not_idle_thread (cur_thread s) s" apply (simp add: not_idle_thread_def ct_in_state_def) apply (subgoal_tac "valid_idle s") apply (clarsimp simp: valid_idle_def pred_tcb_at_def obj_at_def) apply (clarsimp simp: invs_def valid_state_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; ct_active s\<rbrakk> \<Longrightarrow> not_idle_thread (cur_thread s) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; st_tcb_at active (cur_thread s) s\<rbrakk> \<Longrightarrow> cur_thread s \<noteq> idle_thread s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>invs s; st_tcb_at active (cur_thread s) s; valid_idle s\<rbrakk> \<Longrightarrow> cur_thread s \<noteq> idle_thread s
 2. \<lbrakk>invs s; st_tcb_at active (cur_thread s) s\<rbrakk> \<Longrightarrow> valid_idle s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; st_tcb_at active (cur_thread s) s\<rbrakk> \<Longrightarrow> valid_idle s proof (prove)
goal:
No subgoals!
theory Syscall_DR

lemma sfi_generate_pending:
  "\<lbrace>st_tcb_at(\<lambda>st. \<not>(generates_pending st)) thread\<rbrace> Ipc_A.send_fault_ipc thread ft
  \<lbrace>\<lambda>t. \<top>\<rbrace>, \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. \<not> (generates_pending st)) thread\<rbrace>" apply (clarsimp simp:send_fault_ipc_def Let_def lookup_cap_def) apply (wp hoare_drop_imps hoare_allI|wpc|clarsimp|rule hoare_conjI)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at (\<lambda>st. \<not> generates_pending st) thread\<rbrace> Ipc_A.send_fault_ipc thread ft \<lbrace>\<lambda>t _. True\<rbrace>, \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. \<not> generates_pending st) thread\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at (\<lambda>st. \<not> generates_pending st) thread\<rbrace> doE handler_cptr <- liftE (thread_get tcb_fault_handler thread);
handler_cap <- cap_fault_on_failure (of_bl handler_cptr) False (doE (ref', uu_) <- lookup_slot_for_thread thread handler_cptr;
liftE (CSpaceAcc_A.get_cap ref')
odE);
case handler_cap of cap.EndpointCap ref badge rights \<Rightarrow> if AllowSend \<in> rights \<and> (AllowGrant \<in> rights \<or> AllowGrantReply \<in> rights) then liftE $ do thread_set (tcb_fault_update (\<lambda>_. Some ft)) thread;
Ipc_A.send_ipc True True (cap_ep_badge handler_cap) (AllowGrant \<in> rights) True thread (cap_ep_ptr handler_cap)
od else throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0)) | _ \<Rightarrow> throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0))
odE \<lbrace>\<lambda>t _. True\<rbrace>, \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. \<not> generates_pending st) thread\<rbrace> proof (prove)
goal:
No subgoals!
theory Syscall_DR

lemma dcorres_handle_double_fault:
  "dcorres dc \<top> (valid_mdb and not_idle_thread thread and valid_idle and valid_etcbs)
    (KHeap_D.set_cap (thread, tcb_pending_op_slot) cdl_cap.NullCap)
    (handle_double_fault thread ft' ft'a)" apply (simp add:handle_double_fault_def  ) apply (rule corres_guard_imp) apply (rule set_thread_state_corres ) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (valid_mdb and not_idle_thread thread and valid_idle and valid_etcbs) (KHeap_D.set_cap (thread, tcb_pending_op_slot) cdl_cap.NullCap) (handle_double_fault thread ft' ft'a) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (valid_mdb and not_idle_thread thread and valid_idle and valid_etcbs) (KHeap_D.set_cap (thread, tcb_pending_op_slot) cdl_cap.NullCap) (set_thread_state thread Inactive) proof (prove)
goal (3 subgoals):
 1. dcorres dc ?Q ?Q' (KHeap_D.set_cap (thread, tcb_pending_op_slot) cdl_cap.NullCap) (set_thread_state thread Inactive)
 2. \<And>s. True \<Longrightarrow> ?Q s
 3. \<And>s. (valid_mdb and not_idle_thread thread and valid_idle and valid_etcbs) s \<Longrightarrow> ?Q' s proof (prove)
goal (2 subgoals):
 1. \<And>s. True \<Longrightarrow> True
 2. \<And>s. (valid_mdb and not_idle_thread thread and valid_idle and valid_etcbs) s \<Longrightarrow> (not_idle_thread thread and K (cdl_cap.NullCap = infer_tcb_pending_op thread Inactive) and valid_etcbs) s proof (prove)
goal:
No subgoals!
theory Syscall_DR

lemma dcorres_when_r:
  "\<lbrakk>R \<Longrightarrow> dcorres dc \<top> P l r; \<not> R \<Longrightarrow> dcorres dc \<top> Q l (return ())\<rbrakk>
    \<Longrightarrow> dcorres dc \<top> (\<lambda>s. (R \<longrightarrow> P s) \<and> (\<not> R \<longrightarrow> Q s)) l (when R r)" by (clarsimp simp:when_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>R \<Longrightarrow> dcorres dc (\<lambda>_. True) P l r; \<not> R \<Longrightarrow> dcorres dc (\<lambda>_. True) Q l (return ())\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>s. (R \<longrightarrow> P s) \<and> (\<not> R \<longrightarrow> Q s)) l (when R r)
theory Syscall_DR

lemma evalMonad_from_wp:
  "\<lbrakk>evalMonad f s = Some a;\<lbrace>P\<rbrace>f\<lbrace> \<lambda>rv s. R rv\<rbrace>;P s;empty_when_fail f;\<And>Q. weak_det_spec Q f \<rbrakk>\<Longrightarrow> R a" apply (clarsimp simp:evalMonad_def valid_def) apply (drule_tac x = "(=) s" in meta_spec) apply (fastforce simp:weak_det_spec_def empty_when_fail_def no_fail_def det_spec_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>evalMonad f s = Some a; \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. R rv\<rbrace>; P s; empty_when_fail f; \<And>Q. weak_det_spec Q f\<rbrakk> \<Longrightarrow> R a proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(if fst (f s) = {} then None else Some (pick (fst ` fst (f s)))) = Some a; \<forall>s. P s \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (r, s') \<Rightarrow> R r); P s; empty_when_fail f; \<And>Q. weak_det_spec Q f\<rbrakk> \<Longrightarrow> R a proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(if fst (f s) = {} then None else Some (pick (fst ` fst (f s)))) = Some a; \<forall>s. P s \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (r, s') \<Rightarrow> R r); P s; empty_when_fail f; weak_det_spec ((=) s) f\<rbrakk> \<Longrightarrow> R a proof (prove)
goal:
No subgoals!
theory Syscall_DR

lemma lookup_cap_and_slot_inv:
  "\<lbrace>P\<rbrace> CSpace_A.lookup_cap_and_slot t (to_bl (arch_tcb_context_get (tcb_arch obj'a) cap_register)) \<lbrace>\<lambda>x. P\<rbrace>, \<lbrace>\<lambda>ft s. True\<rbrace>" apply (simp add:CSpace_A.lookup_cap_and_slot_def) apply (wp | clarsimp simp:liftE_bindE)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> CSpace_A.lookup_cap_and_slot t (to_bl (arch_tcb_context_get (tcb_arch obj'a) cap_register)) \<lbrace>\<lambda>x. P\<rbrace>, \<lbrace>\<lambda>ft s. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> doE (slot, cr) <- lookup_slot_for_thread t (to_bl (arch_tcb_context_get (tcb_arch obj'a) cap_register));
cap <- liftE (CSpaceAcc_A.get_cap slot);
returnOk (cap, slot)
odE \<lbrace>\<lambda>x. P\<rbrace>, \<lbrace>\<lambda>ft s. True\<rbrace> proof (prove)
goal:
No subgoals!
theory Syscall_DR

lemma liftE_distrib':
  "liftE (do x \<leftarrow> A;B x od) =
  doE x \<leftarrow> liftE A;
  liftE (B x)
  odE" by (simp add:bindE_def liftE_def bind_assoc lift_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. liftE (A >>= B) = doE x <- liftE A;
liftE (B x)
odE
theory Syscall_DR

lemma invoke_cnode_idle:
  "\<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> invoke_cnode pa \<lbrace>\<lambda>r s. P (idle_thread s)\<rbrace>" apply (cases pa) apply (clarsimp simp:invoke_cnode_def
            | wpsimp wp: crunch_wps hoare_vcg_all_lift | rule conjI)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> CSpace_A.invoke_cnode pa \<lbrace>\<lambda>r s. P (idle_thread s)\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>x11 x12 x13. pa = cnode_invocation.InsertCall x11 x12 x13 \<Longrightarrow> \<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> CSpace_A.invoke_cnode pa \<lbrace>\<lambda>r s. P (idle_thread s)\<rbrace>
 2. \<And>x21 x22 x23. pa = cnode_invocation.MoveCall x21 x22 x23 \<Longrightarrow> \<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> CSpace_A.invoke_cnode pa \<lbrace>\<lambda>r s. P (idle_thread s)\<rbrace>
 3. \<And>x3. pa = cnode_invocation.RevokeCall x3 \<Longrightarrow> \<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> CSpace_A.invoke_cnode pa \<lbrace>\<lambda>r s. P (idle_thread s)\<rbrace>
 4. \<And>x4. pa = cnode_invocation.DeleteCall x4 \<Longrightarrow> \<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> CSpace_A.invoke_cnode pa \<lbrace>\<lambda>r s. P (idle_thread s)\<rbrace>
 5. \<And>x51 x52 x53 x54 x55. pa = cnode_invocation.RotateCall x51 x52 x53 x54 x55 \<Longrightarrow> \<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> CSpace_A.invoke_cnode pa \<lbrace>\<lambda>r s. P (idle_thread s)\<rbrace>
 6. \<And>x6. pa = cnode_invocation.SaveCall x6 \<Longrightarrow> \<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> CSpace_A.invoke_cnode pa \<lbrace>\<lambda>r s. P (idle_thread s)\<rbrace>
 7. \<And>x7. pa = cnode_invocation.CancelBadgedSendsCall x7 \<Longrightarrow> \<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> CSpace_A.invoke_cnode pa \<lbrace>\<lambda>r s. P (idle_thread s)\<rbrace> proof (prove)
goal:
No subgoals!
theory Syscall_DR

lemma invoke_domain_idle:
  "\<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> invoke_domain t d  \<lbrace>\<lambda>r s. P (idle_thread s)\<rbrace>" by  (clarsimp simp: Tcb_A.invoke_domain_def trans_state_def | wp dxo_wp_weak)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> Tcb_A.invoke_domain t d \<lbrace>\<lambda>r s. P (idle_thread s)\<rbrace>
theory Syscall_DR

lemma msg_from_syscall_error_simp:
  "fst (msg_from_syscall_error rv) \<le> mask 19"
  "0 < fst (msg_from_syscall_error rv)" apply (case_tac rv) apply (clarsimp simp:mask_def)+ apply (case_tac rv) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. fst (msg_from_syscall_error rv) \<le> mask 19 &&& 0 < fst (msg_from_syscall_error rv) proof (prove)
goal (11 subgoals):
 1. \<And>x1. rv = InvalidArgument x1 \<Longrightarrow> fst (msg_from_syscall_error rv) \<le> mask 19
 2. \<And>x2. rv = InvalidCapability x2 \<Longrightarrow> fst (msg_from_syscall_error rv) \<le> mask 19
 3. rv = IllegalOperation \<Longrightarrow> fst (msg_from_syscall_error rv) \<le> mask 19
 4. \<And>x41 x42. rv = RangeError x41 x42 \<Longrightarrow> fst (msg_from_syscall_error rv) \<le> mask 19
 5. rv = AlignmentError \<Longrightarrow> fst (msg_from_syscall_error rv) \<le> mask 19
 6. \<And>x61 x62. rv = FailedLookup x61 x62 \<Longrightarrow> fst (msg_from_syscall_error rv) \<le> mask 19
 7. rv = TruncatedMessage \<Longrightarrow> fst (msg_from_syscall_error rv) \<le> mask 19
 8. rv = DeleteFirst \<Longrightarrow> fst (msg_from_syscall_error rv) \<le> mask 19
 9. rv = RevokeFirst \<Longrightarrow> fst (msg_from_syscall_error rv) \<le> mask 19
 10. \<And>x10. rv = NotEnoughMemory x10 \<Longrightarrow> fst (msg_from_syscall_error rv) \<le> mask 19
A total of 11 subgoals... proof (prove)
goal (1 subgoal):
 1. 0 < fst (msg_from_syscall_error rv) proof (prove)
goal (10 subgoals):
 1. \<And>x1. rv = InvalidArgument x1 \<Longrightarrow> 0 < fst (msg_from_syscall_error rv)
 2. \<And>x2. rv = InvalidCapability x2 \<Longrightarrow> 0 < fst (msg_from_syscall_error rv)
 3. rv = IllegalOperation \<Longrightarrow> 0 < fst (msg_from_syscall_error rv)
 4. \<And>x41 x42. rv = RangeError x41 x42 \<Longrightarrow> 0 < fst (msg_from_syscall_error rv)
 5. rv = AlignmentError \<Longrightarrow> 0 < fst (msg_from_syscall_error rv)
 6. \<And>x61 x62. rv = FailedLookup x61 x62 \<Longrightarrow> 0 < fst (msg_from_syscall_error rv)
 7. rv = TruncatedMessage \<Longrightarrow> 0 < fst (msg_from_syscall_error rv)
 8. rv = DeleteFirst \<Longrightarrow> 0 < fst (msg_from_syscall_error rv)
 9. rv = RevokeFirst \<Longrightarrow> 0 < fst (msg_from_syscall_error rv)
 10. \<And>x10. rv = NotEnoughMemory x10 \<Longrightarrow> 0 < fst (msg_from_syscall_error rv) proof (prove)
goal:
No subgoals!
theory Syscall_DR

lemma not_master_reply_cap_lcs'[wp]:
  "\<lbrace>valid_reply_masters and valid_objs\<rbrace> CSpace_A.lookup_cap_and_slot t ptr
            \<lbrace>\<lambda>rv s. cte_wp_at (Not \<circ> is_master_reply_cap) (snd rv) s\<rbrace>,-" apply (rule_tac Q' = "\<lambda>rv s. \<not> is_master_reply_cap (fst rv) \<and> cte_wp_at ((=) (fst rv)) (snd rv) s"
           in hoare_post_imp_R) apply (rule hoare_pre,wp,simp) apply (clarsimp simp:cte_wp_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_reply_masters and valid_objs\<rbrace> CSpace_A.lookup_cap_and_slot t ptr \<lbrace>\<lambda>rv. cte_wp_at (Not \<circ> is_master_reply_cap) (snd rv)\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>valid_reply_masters and valid_objs\<rbrace> CSpace_A.lookup_cap_and_slot t ptr \<lbrace>\<lambda>rv s. \<not> is_master_reply_cap (fst rv) \<and> cte_wp_at ((=) (fst rv)) (snd rv) s\<rbrace>, -
 2. \<And>rv s. \<not> is_master_reply_cap (fst rv) \<and> cte_wp_at ((=) (fst rv)) (snd rv) s \<Longrightarrow> cte_wp_at (Not \<circ> is_master_reply_cap) (snd rv) s proof (prove)
goal (1 subgoal):
 1. \<And>rv s. \<not> is_master_reply_cap (fst rv) \<and> cte_wp_at ((=) (fst rv)) (snd rv) s \<Longrightarrow> cte_wp_at (Not \<circ> is_master_reply_cap) (snd rv) s proof (prove)
goal:
No subgoals!
theory Syscall_DR

lemma set_thread_state_ct_active:
  "\<lbrace>\<lambda>s. cur_thread s = cur_thread s'\<rbrace>
   set_thread_state (cur_thread s') Structures_A.thread_state.Restart \<lbrace>\<lambda>rv. ct_active\<rbrace>" apply (simp add: set_thread_state_def) apply (wp dxo_wp_weak
       | clarsimp simp: set_object_def get_object_def trans_state_def
                        ct_in_state_def st_tcb_at_def obj_at_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cur_thread s = cur_thread s'\<rbrace> set_thread_state (cur_thread s') Restart \<lbrace>\<lambda>rv. ct_active\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cur_thread s = cur_thread s'\<rbrace> do tcb <- gets_the (get_tcb (cur_thread s'));
y <- KHeap_A.set_object (cur_thread s') (TCB (update_tcb_state Restart tcb));
do_extended_op (set_thread_state_ext (cur_thread s'))
od \<lbrace>\<lambda>rv. ct_active\<rbrace> proof (prove)
goal:
No subgoals!
theory Syscall_DR

lemma invoke_cnode_valid_etcbs[wp]:
  "\<lbrace>valid_etcbs\<rbrace> invoke_cnode ci \<lbrace>\<lambda>_. valid_etcbs\<rbrace>" apply (simp add: invoke_cnode_def) apply (rule hoare_pre) apply (wp crunch_wps hoare_vcg_all_lift | wpc | simp add: split del: if_split)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_etcbs\<rbrace> CSpace_A.invoke_cnode ci \<lbrace>\<lambda>_. valid_etcbs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_etcbs\<rbrace> case ci of cnode_invocation.InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | cnode_invocation.MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | cnode_invocation.RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | cnode_invocation.DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | cnode_invocation.RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | cnode_invocation.SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- CSpaceAcc_A.get_cap src_slot;
case cap of cap.NullCap \<Rightarrow> return () | cap.ReplyCap x True xa \<Rightarrow> fail | cap.ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | cnode_invocation.CancelBadgedSendsCall (cap.EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ IpcCancel_A.cancel_badged_sends ep b | cnode_invocation.CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>_. valid_etcbs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> case ci of cnode_invocation.InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | cnode_invocation.MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | cnode_invocation.RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | cnode_invocation.DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | cnode_invocation.RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | cnode_invocation.SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- CSpaceAcc_A.get_cap src_slot;
case cap of cap.NullCap \<Rightarrow> return () | cap.ReplyCap x True xa \<Rightarrow> fail | cap.ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | cnode_invocation.CancelBadgedSendsCall (cap.EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ IpcCancel_A.cancel_badged_sends ep b | cnode_invocation.CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>_. valid_etcbs\<rbrace>
 2. \<And>s. valid_etcbs s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory Syscall_DR

lemma cap_delete_one_st_tcb_at_and_valid_etcbs:
  "\<lbrace>st_tcb_at P t and K (\<forall>st. active st \<longrightarrow> P st) and valid_etcbs\<rbrace> cap_delete_one ptr \<lbrace>\<lambda>rv s. st_tcb_at P t s \<and> valid_etcbs s\<rbrace>" by (wp cap_delete_one_st_tcb_at cap_delete_one_valid_etcbs | simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at P t and K (\<forall>st. active st \<longrightarrow> P st) and valid_etcbs\<rbrace> cap_delete_one ptr \<lbrace>\<lambda>rv s. st_tcb_at P t s \<and> valid_etcbs s\<rbrace>