theory IRQMasks_IF

lemma invoke_cnode_irq_masks:
  "\<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and valid_cnode_inv ci\<rbrace>
   invoke_cnode ci
   \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>" unfolding invoke_cnode_def apply (cases ci) by (wpsimp wp: cap_move_irq_masks cap_insert_irq_masks hoare_vcg_all_lift hoare_drop_imps
                 cap_revoke_irq_masks[where st=st] cap_delete_irq_masks[where st=st]
      split_del: if_split)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and valid_cnode_inv ci\<rbrace> invoke_cnode ci \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and valid_cnode_inv ci\<rbrace> case ci of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | 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 | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>x11 x12 x13. ci = InsertCall x11 x12 x13 \<Longrightarrow> \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and valid_cnode_inv ci\<rbrace> case ci of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | 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 | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 2. \<And>x21 x22 x23. ci = MoveCall x21 x22 x23 \<Longrightarrow> \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and valid_cnode_inv ci\<rbrace> case ci of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | 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 | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 3. \<And>x3. ci = RevokeCall x3 \<Longrightarrow> \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and valid_cnode_inv ci\<rbrace> case ci of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | 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 | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 4. \<And>x4. ci = DeleteCall x4 \<Longrightarrow> \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and valid_cnode_inv ci\<rbrace> case ci of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | 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 | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 5. \<And>x51 x52 x53 x54 x55. ci = RotateCall x51 x52 x53 x54 x55 \<Longrightarrow> \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and valid_cnode_inv ci\<rbrace> case ci of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | 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 | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 6. \<And>x6. ci = SaveCall x6 \<Longrightarrow> \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and valid_cnode_inv ci\<rbrace> case ci of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | 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 | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>
 7. \<And>x7. ci = CancelBadgedSendsCall x7 \<Longrightarrow> \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and valid_cnode_inv ci\<rbrace> case ci of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | 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 | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>