theory DetSchedSchedule_AI

lemma invoke_cnode_valid_sched:
  "\<lbrace>valid_sched and invs and valid_cnode_inv a and simple_sched_action\<rbrace> invoke_cnode a \<lbrace>\<lambda>rv. valid_sched\<rbrace>" apply (simp add: invoke_cnode_def) apply (rule hoare_pre) apply wpc apply (simp add: liftE_def | (wp hoare_vcg_all_lift)+ | wp (once) hoare_drop_imps | wpc)+ apply force done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched and invs and valid_cnode_inv a and simple_sched_action\<rbrace> invoke_cnode a \<lbrace>\<lambda>rv. valid_sched\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched and invs and valid_cnode_inv a and simple_sched_action\<rbrace> case a 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>rv. valid_sched\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> case a 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>rv. valid_sched\<rbrace>
 2. \<And>s. (valid_sched and invs and valid_cnode_inv a and simple_sched_action) s \<Longrightarrow> ?Q s proof (prove)
goal (8 subgoals):
 1. \<And>x11 x12 x13. a = InsertCall x11 x12 x13 \<Longrightarrow> \<lbrace>?R35 x11 x12 x13\<rbrace> without_preemption $ cap_insert x11 x12 x13 \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 2. \<And>x21 x22 x23. a = MoveCall x21 x22 x23 \<Longrightarrow> \<lbrace>?R36 x21 x22 x23\<rbrace> without_preemption $ cap_move x21 x22 x23 \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 3. \<And>x3. a = RevokeCall x3 \<Longrightarrow> \<lbrace>?R37 x3\<rbrace> cap_revoke x3 \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 4. \<And>x4. a = DeleteCall x4 \<Longrightarrow> \<lbrace>?R38 x4\<rbrace> cap_delete x4 \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 5. \<And>x51 x52 x53 x54 x55. a = RotateCall x51 x52 x53 x54 x55 \<Longrightarrow> \<lbrace>?R39 x51 x52 x53 x54 x55\<rbrace> without_preemption $ if x53 = x55 then cap_swap x51 x53 x52 x54 else do cap_move x52 x54 x55;
cap_move x51 x53 x54
od \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 6. \<And>x6. a = SaveCall x6 \<Longrightarrow> \<lbrace>?R40 x6\<rbrace> 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 x6 | _ \<Rightarrow> fail
od \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 7. \<And>x7. a = CancelBadgedSendsCall x7 \<Longrightarrow> \<lbrace>?R41 x7\<rbrace> case x7 of EndpointCap ep b R \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | _ \<Rightarrow> fail \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 8. \<And>s. (valid_sched and invs and valid_cnode_inv a and simple_sched_action) s \<Longrightarrow> (\<forall>x xa xb. a = InsertCall x xa xb \<longrightarrow> ?R35 x xa xb s) \<and> (\<forall>x xa xb. a = MoveCall x xa xb \<longrightarrow> ?R36 x xa xb s) \<and> (\<forall>x. a = RevokeCall x \<longrightarrow> ?R37 x s) \<and> (\<forall>x. a = DeleteCall x \<longrightarrow> ?R38 x s) \<and> (\<forall>x xa xb xc xd. a = RotateCall x xa xb xc xd \<longrightarrow> ?R39 x xa xb xc xd s) \<and> (\<forall>x. a = SaveCall x \<longrightarrow> ?R40 x s) \<and> (\<forall>x. a = CancelBadgedSendsCall x \<longrightarrow> ?R41 x s) proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_sched s \<and> invs s \<and> valid_cnode_inv a s \<and> simple_sched_action s \<Longrightarrow> \<forall>x. a = CancelBadgedSendsCall x \<longrightarrow> (x = NullCap \<longrightarrow> ?R311 NullCap s) \<and> (\<forall>xa xb xc xd. x = UntypedCap xa xb xc xd \<longrightarrow> ?R312 (UntypedCap xa xb xc xd) xa xb xc xd s) proof (prove)
goal:
No subgoals!