kings-crown/FVELER_Isabelle huggingface dataset:
theory DetSchedSchedule_AI

lemma thread_set_tcb_fault_set_invs:
  "valid_fault f \<Longrightarrow> \<lbrace>invs\<rbrace>
     thread_set (tcb_fault_update (\<lambda>_. Some f)) t
   \<lbrace>\<lambda>rv. invs\<rbrace>" apply (rule thread_set_invs_trivial) apply (clarsimp simp: ran_tcb_cap_cases)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_fault f \<Longrightarrow> \<lbrace>invs\<rbrace> thread_set (tcb_fault_update (\<lambda>_. Some f)) t \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>tcb. valid_fault f \<Longrightarrow> \<forall>(getF, v)\<in>ran tcb_cap_cases. getF (tcb\<lparr>tcb_fault := Some f\<rparr>) = getF tcb
 2. \<And>tcb. valid_fault f \<Longrightarrow> tcb_state (tcb\<lparr>tcb_fault := Some f\<rparr>) = tcb_state tcb
 3. \<And>tcb. valid_fault f \<Longrightarrow> tcb_bound_notification (tcb\<lparr>tcb_fault := Some f\<rparr>) = tcb_bound_notification tcb
 4. \<And>tcb. valid_fault f \<Longrightarrow> tcb_iarch (tcb\<lparr>tcb_fault := Some f\<rparr>) = tcb_iarch tcb
 5. \<And>tcb. valid_fault f \<Longrightarrow> tcb_ipc_buffer (tcb\<lparr>tcb_fault := Some f\<rparr>) = tcb_ipc_buffer tcb \<or> tcb_ipc_buffer (tcb\<lparr>tcb_fault := Some f\<rparr>) = 0
 6. \<And>tcb. valid_fault f \<Longrightarrow> tcb_fault_handler (tcb\<lparr>tcb_fault := Some f\<rparr>) \<noteq> tcb_fault_handler tcb \<longrightarrow> length (tcb_fault_handler (tcb\<lparr>tcb_fault := Some f\<rparr>)) = word_bits
 7. \<And>tcb. valid_fault f \<Longrightarrow> tcb_fault (tcb\<lparr>tcb_fault := Some f\<rparr>) \<noteq> tcb_fault tcb \<longrightarrow> (case tcb_fault (tcb\<lparr>tcb_fault := Some f\<rparr>) of None \<Rightarrow> True | Some f \<Rightarrow> valid_fault f)
 8. \<And>tcb. valid_fault f \<Longrightarrow> tcb_arch_ref (tcb\<lparr>tcb_fault := Some f\<rparr>) = tcb_arch_ref tcb proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma send_fault_ipc_valid_sched[wp]:
  "\<lbrace>valid_sched and st_tcb_at active tptr and scheduler_act_not tptr and
       not_queued tptr and (ct_active or ct_idle) and invs and (\<lambda>_. valid_fault fault)\<rbrace>
     send_fault_ipc tptr fault
   \<lbrace>\<lambda>_. valid_sched\<rbrace>" apply (simp add: send_fault_ipc_def Let_def) apply (wp send_ipc_valid_sched thread_set_not_state_valid_sched thread_set_no_change_tcb_state
            hoare_gen_asm'[OF thread_set_tcb_fault_set_invs]  hoare_drop_imps hoare_vcg_all_lift_R
            ct_in_state_thread_state_lift thread_set_no_change_tcb_state
            hoare_vcg_disj_lift
         | wpc | simp | wps)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched and st_tcb_at active tptr and scheduler_act_not tptr and not_queued tptr and (ct_active or ct_idle) and invs and (\<lambda>_. valid_fault fault)\<rbrace> send_fault_ipc tptr fault \<lbrace>\<lambda>_. valid_sched\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched and st_tcb_at active tptr and scheduler_act_not tptr and not_queued tptr and (ct_active or ct_idle) and invs and (\<lambda>_. valid_fault fault)\<rbrace> doE handler_cptr <- liftE (thread_get tcb_fault_handler tptr);
handler_cap <- cap_fault_on_failure (of_bl handler_cptr) False (lookup_cap tptr handler_cptr);
case handler_cap of 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 fault)) tptr;
send_ipc True True (cap_ep_badge handler_cap) (AllowGrant \<in> rights) True tptr (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>_. valid_sched\<rbrace> proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma handle_double_fault_valid_queues:
  "\<lbrace>valid_queues and not_queued tptr\<rbrace>
     handle_double_fault tptr ex1 ex2
   \<lbrace>\<lambda>rv. valid_queues\<rbrace>" apply (simp add: handle_double_fault_def set_thread_state_def) apply (wp | simp add: set_thread_state_ext_def set_object_def get_object_def)+ apply (fastforce simp: valid_queues_def st_tcb_at_kh_if_split not_queued_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_queues and not_queued tptr\<rbrace> handle_double_fault tptr ex1 ex2 \<lbrace>\<lambda>rv. valid_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_queues and not_queued tptr\<rbrace> do tcb <- gets_the (get_tcb tptr);
y <- set_object tptr (TCB (tcb\<lparr>tcb_state := Inactive\<rparr>));
set_thread_state_ext tptr
od \<lbrace>\<lambda>rv. valid_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_queues s \<and> not_queued tptr s \<Longrightarrow> (\<exists>y. get_tcb tptr s = Some y) \<longrightarrow> (\<exists>y. kheap s tptr = Some y) \<longrightarrow> a_type (the (kheap s tptr)) = ATCB \<longrightarrow> valid_queues_2 (ready_queues s) (ekheap s) (\<lambda>a. if a = tptr then Some (TCB (the (get_tcb tptr s)\<lparr>tcb_state := Inactive\<rparr>)) else kheap s a) proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma handle_double_fault_valid_sched_action:
  "\<lbrace>valid_sched_action and scheduler_act_not tptr\<rbrace>
     handle_double_fault tptr ex1 ex2
   \<lbrace>\<lambda>rv. valid_sched_action\<rbrace>" apply (simp add: handle_double_fault_def set_thread_state_def) apply (wp gts_wp | simp add: set_thread_state_ext_def set_object_def get_object_def)+ apply (clarsimp simp: valid_sched_action_def weak_valid_sched_action_def
                        is_activatable_def pred_tcb_at_def obj_at_def
                        st_tcb_at_kh_if_split scheduler_act_not_def
                  split: scheduler_action.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched_action and scheduler_act_not tptr\<rbrace> handle_double_fault tptr ex1 ex2 \<lbrace>\<lambda>rv. valid_sched_action\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched_action and scheduler_act_not tptr\<rbrace> do tcb <- gets_the (get_tcb tptr);
y <- set_object tptr (TCB (tcb\<lparr>tcb_state := Inactive\<rparr>));
set_thread_state_ext tptr
od \<lbrace>\<lambda>rv. valid_sched_action\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_sched_action s \<and> scheduler_act_not tptr s \<Longrightarrow> (\<exists>y. get_tcb tptr s = Some y) \<longrightarrow> (\<exists>y. kheap s tptr = Some y) \<longrightarrow> a_type (the (kheap s tptr)) = ATCB \<longrightarrow> (\<forall>st. (cur_thread s = tptr \<longrightarrow> runnable st \<or> scheduler_action s \<noteq> resume_cur_thread) \<longrightarrow> st_tcb_at ((=) st) tptr (s\<lparr>kheap := \<lambda>a. if a = tptr then Some (TCB (the (get_tcb tptr s)\<lparr>tcb_state := Inactive\<rparr>)) else kheap s a\<rparr>) \<longrightarrow> valid_sched_action_2 (scheduler_action s) (ekheap s) (\<lambda>a. if a = tptr then Some (TCB (the (get_tcb tptr s)\<lparr>tcb_state := Inactive\<rparr>)) else kheap s a) (cur_thread s) (cur_domain s)) proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma handle_double_fault_valid_sched:
  "\<lbrace>valid_sched and not_queued tptr and scheduler_act_not tptr\<rbrace>
     handle_double_fault tptr ex1 ex2
   \<lbrace>\<lambda>rv. valid_sched\<rbrace>" apply (simp add: valid_sched_def) including no_pre apply (wp handle_double_fault_valid_queues handle_double_fault_valid_sched_action
            set_thread_state_not_runnable_valid_blocked
          | rule hoare_conjI | simp add: handle_double_fault_def | fastforce simp: simple_sched_action_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched and not_queued tptr and scheduler_act_not tptr\<rbrace> handle_double_fault tptr ex1 ex2 \<lbrace>\<lambda>rv. valid_sched\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_blocked s \<and> valid_idle_etcb s) and not_queued tptr and scheduler_act_not tptr\<rbrace> handle_double_fault tptr ex1 ex2 \<lbrace>\<lambda>rv s. valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_blocked s \<and> valid_idle_etcb s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_blocked s \<and> valid_idle_etcb s) and not_queued tptr and scheduler_act_not tptr\<rbrace> handle_double_fault tptr ex1 ex2 \<lbrace>\<lambda>rv s. valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_blocked s \<and> valid_idle_etcb s\<rbrace> proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma send_fault_ipc_error_sched_act_not[wp]:
  "\<lbrace>scheduler_act_not t\<rbrace> send_fault_ipc tptr fault -, \<lbrace>\<lambda>rv. scheduler_act_not t\<rbrace>" by (simp add: send_fault_ipc_def Let_def |
      (wp hoare_drop_imps hoare_vcg_all_lift_R)+ | wpc)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>scheduler_act_not t\<rbrace> send_fault_ipc tptr fault -, \<lbrace>\<lambda>rv. scheduler_act_not t\<rbrace>
theory DetSchedSchedule_AI

lemma send_fault_ipc_error_cur_thread[wp]:
  "\<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> send_fault_ipc tptr fault -, \<lbrace>\<lambda>rv s. P (cur_thread s)\<rbrace>" by (simp add: send_fault_ipc_def Let_def |
      (wp hoare_drop_imps hoare_vcg_all_lift_R)+ | wpc)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> send_fault_ipc tptr fault -, \<lbrace>\<lambda>rv s. P (cur_thread s)\<rbrace>
theory DetSchedSchedule_AI

lemma send_fault_ipc_error_not_queued[wp]:
  "\<lbrace>not_queued t\<rbrace> send_fault_ipc tptr fault -, \<lbrace>\<lambda>rv. not_queued t\<rbrace>" by (simp add: send_fault_ipc_def Let_def |
      (wp hoare_drop_imps hoare_vcg_all_lift_R)+ | wpc)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>not_queued t\<rbrace> send_fault_ipc tptr fault -, \<lbrace>\<lambda>rv. not_queued t\<rbrace>
theory DetSchedSchedule_AI

lemma handle_fault_valid_sched:
  "\<lbrace>valid_sched and st_tcb_at active thread and not_queued thread and (ct_active or ct_idle)
      and scheduler_act_not thread and invs and (\<lambda>_. valid_fault ex)\<rbrace>
   handle_fault thread ex \<lbrace>\<lambda>rv. valid_sched\<rbrace>" unfolding handle_fault_def by (simp add: handle_fault_def |
      wp handle_double_fault_valid_sched send_fault_ipc_valid_sched)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched and st_tcb_at active thread and not_queued thread and (ct_active or ct_idle) and scheduler_act_not thread and invs and (\<lambda>_. valid_fault ex)\<rbrace> handle_fault thread ex \<lbrace>\<lambda>rv. valid_sched\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched and st_tcb_at active thread and not_queued thread and (ct_active or ct_idle) and scheduler_act_not thread and invs and (\<lambda>_. valid_fault ex)\<rbrace> do _ <- gets_the $ get_tcb thread;
send_fault_ipc thread ex <catch> handle_double_fault thread ex;
return ()
od \<lbrace>\<lambda>rv. valid_sched\<rbrace>
theory DetSchedSchedule_AI

lemma idle_not_queued'':
  "\<lbrakk>valid_idle s; sym_refs (state_refs_of s); queue \<times> {rt} \<subseteq> state_refs_of s ptr\<rbrakk> \<Longrightarrow>
     idle_thread s \<notin> queue" by (frule idle_no_refs, fastforce simp: valid_idle_def sym_refs_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_idle s; sym_refs (state_refs_of s); queue \<times> {rt} \<subseteq> state_refs_of s ptr\<rbrakk> \<Longrightarrow> idle_thread s \<notin> queue
theory DetSchedSchedule_AI

lemma tcb_sched_action_enqueue_not_queued:
  "\<lbrace>not_queued t and K (thread \<noteq> t)\<rbrace>
     tcb_sched_action tcb_sched_enqueue thread
   \<lbrace>\<lambda>rv. not_queued t\<rbrace>" apply (simp add: tcb_sched_action_def | wp)+ apply (clarsimp simp: etcb_at_def tcb_sched_enqueue_def not_queued_def
                  split: option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>not_queued t and K (thread \<noteq> t)\<rbrace> tcb_sched_action tcb_sched_enqueue thread \<lbrace>\<lambda>rv. not_queued t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. not_queued t s \<and> thread \<noteq> t \<Longrightarrow> etcb_at (\<lambda>ta. etcb_at (\<lambda>tb. not_queued_2 (\<lambda>a b. if a = tcb_domain ta \<and> b = tcb_priority tb then tcb_sched_enqueue thread (ready_queues s (tcb_domain ta) (tcb_priority tb)) else ready_queues s a b) t) thread s) thread s proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma reschedule_required_not_queued:
  "\<lbrace>not_queued t and scheduler_act_not t\<rbrace>
    reschedule_required
   \<lbrace>\<lambda>rv. not_queued t\<rbrace>" apply (simp add: reschedule_required_def tcb_sched_action_def
                   set_scheduler_action_def | wp | wpc)+ apply (clarsimp simp: etcb_at_def tcb_sched_enqueue_def not_queued_def
                        scheduler_act_not_def
                  split: option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>not_queued t and scheduler_act_not t\<rbrace> reschedule_required \<lbrace>\<lambda>rv. not_queued t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. not_queued t s \<and> scheduler_act_not t s \<Longrightarrow> \<forall>x. scheduler_action s = switch_thread x \<longrightarrow> etcb_at (\<lambda>ta. etcb_at (\<lambda>tb. not_queued_2 (\<lambda>a b. if a = tcb_domain ta \<and> b = tcb_priority tb then tcb_sched_enqueue x (ready_queues s (tcb_domain ta) (tcb_priority tb)) else ready_queues s a b) t) x s) x s proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma unbind_maybe_notification_valid_objs:
  "\<lbrace>valid_objs\<rbrace>
   unbind_maybe_notification ptr \<lbrace>\<lambda>rv. valid_objs\<rbrace>" unfolding unbind_maybe_notification_def apply (wp thread_set_valid_objs_triv set_simple_ko_valid_objs hoare_drop_imp
            get_simple_ko_wp | wpc | simp add: tcb_cap_cases_def
         | strengthen unbind_notification_valid_objs_helper)+ apply (clarsimp) apply (erule (1) obj_at_valid_objsE) apply (clarsimp simp:valid_obj_def valid_tcb_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs\<rbrace> unbind_maybe_notification ptr \<lbrace>\<lambda>rv. valid_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs\<rbrace> do ntfn <- get_notification ptr;
case ntfn_bound_tcb ntfn of None \<Rightarrow> return () | Some t \<Rightarrow> do_unbind_notification ptr ntfn t
od \<lbrace>\<lambda>rv. valid_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_objs s \<Longrightarrow> \<forall>x. ko_at (Notification x) ptr s \<longrightarrow> (\<exists>xa. ntfn_bound_tcb x = Some xa) \<longrightarrow> valid_ntfn x s proof (prove)
goal (1 subgoal):
 1. \<And>s x xa. \<lbrakk>valid_objs s; ko_at (Notification x) ptr s; ntfn_bound_tcb x = Some xa\<rbrakk> \<Longrightarrow> valid_ntfn x s proof (prove)
goal (1 subgoal):
 1. \<And>s x xa ko. \<lbrakk>valid_objs s; ntfn_bound_tcb x = Some xa; kheap s ptr = Some ko; Notification x = ko; valid_obj ptr ko s\<rbrakk> \<Longrightarrow> valid_ntfn x s proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma fast_finalise_not_queued:
  "\<lbrace>not_queued t and (st_tcb_at active t and valid_objs and scheduler_act_not t and
    sym_refs \<circ> state_refs_of)\<rbrace>
   fast_finalise cap final
   \<lbrace>\<lambda>_. not_queued t\<rbrace>" apply (cases cap, simp_all) apply (wp cancel_all_ipc_not_queued cancel_all_signals_not_queued
            get_simple_ko_wp unbind_maybe_notification_valid_objs | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>not_queued t and (st_tcb_at active t and valid_objs and scheduler_act_not t and sym_refs \<circ> state_refs_of)\<rbrace> fast_finalise cap final \<lbrace>\<lambda>_. not_queued t\<rbrace> proof (prove)
goal (4 subgoals):
 1. cap = NullCap \<Longrightarrow> \<lbrace>not_queued t and (st_tcb_at active t and valid_objs and scheduler_act_not t and sym_refs \<circ> state_refs_of)\<rbrace> return () \<lbrace>\<lambda>_. not_queued t\<rbrace>
 2. \<And>x31 x32 x33. cap = EndpointCap x31 x32 x33 \<Longrightarrow> \<lbrace>not_queued t and (st_tcb_at active t and valid_objs and scheduler_act_not t and sym_refs \<circ> state_refs_of)\<rbrace> when final (cancel_all_ipc x31) \<lbrace>\<lambda>_. not_queued t\<rbrace>
 3. \<And>x41 x42 x43. cap = NotificationCap x41 x42 x43 \<Longrightarrow> \<lbrace>not_queued t and (st_tcb_at active t and valid_objs and scheduler_act_not t and sym_refs \<circ> state_refs_of)\<rbrace> when final (do y <- unbind_maybe_notification x41;
cancel_all_signals x41
od) \<lbrace>\<lambda>_. not_queued t\<rbrace>
 4. \<And>x51 x52 x53. cap = ReplyCap x51 x52 x53 \<Longrightarrow> \<lbrace>not_queued t and (st_tcb_at active t and valid_objs and scheduler_act_not t and sym_refs \<circ> state_refs_of)\<rbrace> return () \<lbrace>\<lambda>_. not_queued t\<rbrace> proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma set_simple_ko_ct_active:
  "\<lbrace>ct_active\<rbrace> set_simple_ko f ptr ep \<lbrace>\<lambda>rv. ct_active\<rbrace>" apply (simp add: set_simple_ko_def set_object_def | wp get_object_wp)+ apply (clarsimp simp: ct_in_state_def pred_tcb_at_def obj_at_def
                  split: kernel_object.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_active\<rbrace> set_simple_ko f ptr ep \<lbrace>\<lambda>rv. ct_active\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. ct_active s \<Longrightarrow> \<forall>ko. ko_at ko ptr s \<longrightarrow> (a_type ko = AEndpoint \<longrightarrow> (\<exists>y. partial_inv f ko = Some y) \<longrightarrow> (\<forall>ko. ko_at ko ptr s \<longrightarrow> a_type ko = a_type (f ep) \<longrightarrow> ct_active (s\<lparr>kheap := \<lambda>a. if a = ptr then Some (f ep) else kheap s a\<rparr>))) \<and> (a_type ko = ANTFN \<longrightarrow> (\<exists>y. partial_inv f ko = Some y) \<longrightarrow> (\<forall>ko. ko_at ko ptr s \<longrightarrow> a_type ko = a_type (f ep) \<longrightarrow> ct_active (s\<lparr>kheap := \<lambda>a. if a = ptr then Some (f ep) else kheap s a\<rparr>))) proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma set_eobject_is_etcb_at_ext[wp]:
  "\<lbrace>is_etcb_at t\<rbrace> set_eobject ptr etcb \<lbrace>\<lambda>_. is_etcb_at t\<rbrace>" apply (simp add: set_eobject_def | wp)+ apply (simp add: is_etcb_at_def split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>is_etcb_at t\<rbrace> set_eobject ptr etcb \<lbrace>\<lambda>_. is_etcb_at t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. is_etcb_at t s \<Longrightarrow> is_etcb_at' t (\<lambda>a. if a = ptr then Some etcb else ekheap s a) proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma cap_insert_check_cap_ext_valid[wp]:"
  \<lbrace>valid_list\<rbrace>
   check_cap_at new_cap src_slot (check_cap_at t slot (cap_insert new_cap src_slot x))
  \<lbrace>\<lambda>rv. valid_list\<rbrace>" apply (simp add: check_cap_at_def) apply (wp get_cap_wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_list\<rbrace> check_cap_at new_cap src_slot (check_cap_at t slot (cap_insert new_cap src_slot x)) \<lbrace>\<lambda>rv. valid_list\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_list\<rbrace> do cap' <- get_cap src_slot;
when (same_object_as new_cap cap') (do cap' <- get_cap slot;
when (same_object_as t cap') (cap_insert new_cap src_slot x)
od)
od \<lbrace>\<lambda>rv. valid_list\<rbrace> proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma opt_update_thread_valid_sched[wp]:
  "(\<And>x a. tcb_state (fn a x) = tcb_state x) \<Longrightarrow>
    \<lbrace>valid_sched\<rbrace> option_update_thread t fn v \<lbrace>\<lambda>_. valid_sched\<rbrace>" apply (rule hoare_pre) apply (simp add: option_update_thread_def) apply (wp thread_set_not_state_valid_sched | wpc | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x a. tcb_state (fn a x) = tcb_state x) \<Longrightarrow> \<lbrace>valid_sched\<rbrace> option_update_thread t fn v \<lbrace>\<lambda>_. valid_sched\<rbrace> proof (prove)
goal (2 subgoals):
 1. (\<And>x a. tcb_state (fn a x) = tcb_state x) \<Longrightarrow> \<lbrace>?Q\<rbrace> option_update_thread t fn v \<lbrace>\<lambda>_. valid_sched\<rbrace>
 2. \<And>s. \<lbrakk>\<And>x a. tcb_state (fn a x) = tcb_state x; valid_sched s\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. (\<And>x a. tcb_state (fn a x) = tcb_state x) \<Longrightarrow> \<lbrace>?Q\<rbrace> case v of None \<Rightarrow> return () | Some v \<Rightarrow> thread_set (fn v) t \<lbrace>\<lambda>_. valid_sched\<rbrace>
 2. \<And>s. \<lbrakk>\<And>x a. tcb_state (fn a x) = tcb_state x; valid_sched s\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma opt_update_thread_simple_sched_action[wp]:
  "\<lbrace>simple_sched_action\<rbrace>
    option_update_thread t fn v
   \<lbrace>\<lambda>_. simple_sched_action\<rbrace>" apply (rule hoare_pre) apply (simp add: option_update_thread_def) apply (wp | wpc | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>simple_sched_action\<rbrace> option_update_thread t fn v \<lbrace>\<lambda>_. simple_sched_action\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> option_update_thread t fn v \<lbrace>\<lambda>_. simple_sched_action\<rbrace>
 2. \<And>s. simple_sched_action s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> case v of None \<Rightarrow> return () | Some v \<Rightarrow> thread_set (fn v) t \<lbrace>\<lambda>_. simple_sched_action\<rbrace>
 2. \<And>s. simple_sched_action s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma test:
"invs s \<longrightarrow> (\<exists>y. get_tcb thread s = Some y) \<longrightarrow> s \<turnstile> tcb_ctable (the (get_tcb thread s))" apply (simp add: invs_valid_tcb_ctable_strengthen) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs s \<longrightarrow> (\<exists>y. get_tcb thread s = Some y) \<longrightarrow> s \<turnstile> tcb_ctable (the (get_tcb thread s)) proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma handle_recv_valid_sched':
  "\<lbrace>invs and valid_sched and ct_active and ct_not_queued and scheduler_act_sane\<rbrace>
    handle_recv is_blocking
   \<lbrace>\<lambda>_. valid_sched\<rbrace>" apply (wp handle_recv_valid_sched) apply (simp add: invs_def valid_state_def valid_pspace_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and valid_sched and ct_active and ct_not_queued and scheduler_act_sane\<rbrace> handle_recv is_blocking \<lbrace>\<lambda>_. valid_sched\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs and valid_sched and ct_active and ct_not_queued and scheduler_act_sane) s \<Longrightarrow> (valid_sched and invs and ct_active and ct_not_queued and scheduler_act_sane) s proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma set_thread_state_Running_valid_sched:
  "\<lbrace>valid_sched and ct_active and (\<lambda>s. cur_thread s = ct)\<rbrace>
     set_thread_state ct Running \<lbrace>\<lambda>_. valid_sched\<rbrace>" by (rule set_thread_state_active_valid_sched) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched and ct_active and (\<lambda>s. cur_thread s = ct)\<rbrace> set_thread_state ct Running \<lbrace>\<lambda>_. valid_sched\<rbrace>