theory Syscall_DR

lemma invoke_domain_corres:
  "\<lbrakk> i = cdl_invocation.InvokeDomain (SetDomain word1 word2);
     i' = Invocations_A.invocation.InvokeDomain word1 word2\<rbrakk>
       \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True)
           (invs and ct_active and valid_pdpt_objs and valid_etcbs and
            invocation_duplicates_valid (Invocations_A.invocation.InvokeDomain word1 word2) and
            (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s)))
           (Tcb_D.invoke_domain (SetDomain word1 word2)) (Tcb_A.invoke_domain word1 word2)" supply if_cong[cong] apply (clarsimp simp: Tcb_D.invoke_domain_def Tcb_A.invoke_domain_def) apply (rule corres_bind_return_r) apply (clarsimp simp: Tcb_D.set_domain_def Tcb_A.set_domain_def) apply (rule corres_symb_exec_r) apply (rule_tac Q=\<top> and Q'="tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s)" in dcorres_rhs_noop_above) apply (rule tcb_sched_action_dcorres) apply (rule dcorres_rhs_noop_below_True) apply (rule corres_noop) apply (wp reschedule_required_transform tcb_sched_action_transform | simp)+ apply (simp add: update_thread_def ethread_set_def thread_set_domain_def) apply (rule dcorres_gets_the) apply clarsimp apply (drule get_tcb_at) apply (clarsimp simp: opt_object_tcb transform_tcb_def) apply (rule dcorres_set_eobject_tcb[simplified dc_def]) apply (frule get_tcb_SomeD) apply (clarsimp simp: transform_tcb_def) apply simp apply (frule get_tcb_SomeD) apply simp apply (clarsimp simp: get_etcb_def split:option.splits) apply clarsimp apply (drule get_tcb_at) apply (clarsimp simp:opt_object_tcb) apply wp+ apply simp apply wp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain word1 word2) and (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s))) (Tcb_D.invoke_domain (SetDomain word1 word2)) (Tcb_A.invoke_domain word1 word2) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain word1 word2) and (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s))) (Tcb_D.invoke_domain (SetDomain word1 word2)) (Tcb_A.invoke_domain word1 word2) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain word1 word2) and (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s))) (Tcb_D.set_domain word1 word2) (do y <- Tcb_A.set_domain word1 word2;
return []
od) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2\<rbrakk> \<Longrightarrow> dcorres (\<lambda>y ya. dc y []) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain word1 word2) and (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s))) (Tcb_D.set_domain word1 word2) (Tcb_A.set_domain word1 word2) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2\<rbrakk> \<Longrightarrow> dcorres (\<lambda>y ya. True) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain word1 word2) and (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s))) (update_thread word1 (cdl_tcb_domain_update (\<lambda>_. word2))) (do cur <- gets cur_thread;
y <- tcb_sched_action tcb_sched_dequeue word1;
y <- thread_set_domain word1 word2;
ts <- get_thread_state word1;
y <- when (runnable ts) (tcb_sched_action tcb_sched_enqueue word1);
when (word1 = cur) reschedule_required
od) proof (prove)
goal (4 subgoals):
 1. \<And>cur. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2\<rbrakk> \<Longrightarrow> dcorres (\<lambda>y ya. True) (\<lambda>_. True) (?Q'6 cur) (update_thread word1 (cdl_tcb_domain_update (\<lambda>_. word2))) (do y <- tcb_sched_action tcb_sched_dequeue word1;
y <- thread_set_domain word1 word2;
ts <- get_thread_state word1;
y <- when (runnable ts) (tcb_sched_action tcb_sched_enqueue word1);
when (word1 = cur) reschedule_required
od)
 2. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2\<rbrakk> \<Longrightarrow> \<lbrace>invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain word1 word2) and (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s))\<rbrace> gets cur_thread \<lbrace>?Q'6\<rbrace>
 3. \<And>s. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain word1 word2) and (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s))) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets cur_thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; False\<rbrakk> \<Longrightarrow> no_fail (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain word1 word2) and (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s))) (gets cur_thread) proof (prove)
goal (7 subgoals):
 1. \<And>cur. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2\<rbrakk> \<Longrightarrow> dcorres (?anyrel11 cur) (\<lambda>_. True) (?Q'6 cur) (return ()) (tcb_sched_action tcb_sched_dequeue word1)
 2. \<And>cur. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2\<rbrakk> \<Longrightarrow> dcorres (\<lambda>y ya. True) (\<lambda>_. True) (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s)) (update_thread word1 (cdl_tcb_domain_update (\<lambda>_. word2))) (do y <- thread_set_domain word1 word2;
ts <- get_thread_state word1;
y <- when (runnable ts) (tcb_sched_action tcb_sched_enqueue word1);
when (word1 = cur) reschedule_required
od)
 3. \<And>cur. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return () \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>cur. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'6 cur\<rbrace> tcb_sched_action tcb_sched_dequeue word1 \<lbrace>\<lambda>_. tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s)\<rbrace>
 5. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2\<rbrakk> \<Longrightarrow> \<lbrace>invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain word1 word2) and (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s))\<rbrace> gets cur_thread \<lbrace>?Q'6\<rbrace>
 6. \<And>s. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain word1 word2) and (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s))) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets cur_thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 7. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; False\<rbrakk> \<Longrightarrow> no_fail (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain word1 word2) and (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s))) (gets cur_thread) proof (prove)
goal (6 subgoals):
 1. \<And>cur. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2\<rbrakk> \<Longrightarrow> dcorres (\<lambda>y ya. True) (\<lambda>_. True) (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s)) (update_thread word1 (cdl_tcb_domain_update (\<lambda>_. word2))) (do y <- thread_set_domain word1 word2;
ts <- get_thread_state word1;
y <- when (runnable ts) (tcb_sched_action tcb_sched_enqueue word1);
when (word1 = cur) reschedule_required
od)
 2. \<And>cur. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return () \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>cur. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'6 cur\<rbrace> tcb_sched_action tcb_sched_dequeue word1 \<lbrace>\<lambda>_. tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s)\<rbrace>
 4. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2\<rbrakk> \<Longrightarrow> \<lbrace>invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain word1 word2) and (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s))\<rbrace> gets cur_thread \<lbrace>?Q'6\<rbrace>
 5. \<And>s. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain word1 word2) and (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s))) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets cur_thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 6. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; False\<rbrakk> \<Longrightarrow> no_fail (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain word1 word2) and (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s))) (gets cur_thread) proof (prove)
goal (7 subgoals):
 1. \<And>cur. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2\<rbrakk> \<Longrightarrow> dcorres (\<lambda>y ya. True) (\<lambda>y. True) (\<lambda>y. True) (return ()) (do ts <- get_thread_state word1;
y <- when (runnable ts) (tcb_sched_action tcb_sched_enqueue word1);
when (word1 = cur) reschedule_required
od)
 2. \<And>cur. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2\<rbrakk> \<Longrightarrow> dcorres (\<lambda>y ya. True) (\<lambda>_. True) (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s)) (update_thread word1 (cdl_tcb_domain_update (\<lambda>_. word2))) (thread_set_domain word1 word2)
 3. \<And>cur. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return () \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>cur. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'6 cur\<rbrace> tcb_sched_action tcb_sched_dequeue word1 \<lbrace>\<lambda>_. tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s)\<rbrace>
 5. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2\<rbrakk> \<Longrightarrow> \<lbrace>invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain word1 word2) and (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s))\<rbrace> gets cur_thread \<lbrace>?Q'6\<rbrace>
 6. \<And>s. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain word1 word2) and (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s))) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets cur_thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 7. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; False\<rbrakk> \<Longrightarrow> no_fail (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain word1 word2) and (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s))) (gets cur_thread) proof (prove)
goal (8 subgoals):
 1. \<And>cur s. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; True\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s'. (s, s') \<in> {ss'. transform (snd ss') = fst ss'} \<and> True\<rbrace> do ts <- get_thread_state word1;
y <- when (runnable ts) (tcb_sched_action tcb_sched_enqueue word1);
when (word1 = cur) reschedule_required
od \<lbrace>\<lambda>rv s'. (s, s') \<in> {ss'. transform (snd ss') = fst ss'} \<and> True\<rbrace>
 2. \<And>cur s. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; True; False\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s'. (s, s') \<in> {ss'. transform (snd ss') = fst ss'} \<and> True) (do ts <- get_thread_state word1;
y <- when (runnable ts) (tcb_sched_action tcb_sched_enqueue word1);
when (word1 = cur) reschedule_required
od)
 3. \<And>cur. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2\<rbrakk> \<Longrightarrow> dcorres (\<lambda>y ya. True) (\<lambda>_. True) (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s)) (update_thread word1 (cdl_tcb_domain_update (\<lambda>_. word2))) (thread_set_domain word1 word2)
 4. \<And>cur. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return () \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>cur. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'6 cur\<rbrace> tcb_sched_action tcb_sched_dequeue word1 \<lbrace>\<lambda>_. tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s)\<rbrace>
 6. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2\<rbrakk> \<Longrightarrow> \<lbrace>invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain word1 word2) and (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s))\<rbrace> gets cur_thread \<lbrace>?Q'6\<rbrace>
 7. \<And>s. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain word1 word2) and (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s))) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets cur_thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 8. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; False\<rbrakk> \<Longrightarrow> no_fail (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain word1 word2) and (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s))) (gets cur_thread) proof (prove)
goal (6 subgoals):
 1. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2\<rbrakk> \<Longrightarrow> dcorres (\<lambda>y ya. True) (\<lambda>_. True) (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s)) (update_thread word1 (cdl_tcb_domain_update (\<lambda>_. word2))) (thread_set_domain word1 word2)
 2. \<And>cur. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return () \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>cur. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'6 cur\<rbrace> tcb_sched_action tcb_sched_dequeue word1 \<lbrace>\<lambda>_. tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s)\<rbrace>
 4. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2\<rbrakk> \<Longrightarrow> \<lbrace>invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain word1 word2) and (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s))\<rbrace> gets cur_thread \<lbrace>?Q'6\<rbrace>
 5. \<And>s. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain word1 word2) and (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s))) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets cur_thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 6. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; False\<rbrakk> \<Longrightarrow> no_fail (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain word1 word2) and (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s))) (gets cur_thread) proof (prove)
goal (6 subgoals):
 1. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2\<rbrakk> \<Longrightarrow> dcorres (\<lambda>y ya. True) (\<lambda>_. True) (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s)) (do t <- KHeap_D.get_object word1;
case t of Tcb tcb \<Rightarrow> KHeap_D.set_object word1 (Tcb (tcb\<lparr>cdl_tcb_domain := word2\<rparr>)) | _ \<Rightarrow> fail
od) (do tcb <- gets_the (get_etcb word1);
set_eobject word1 (tcb\<lparr>tcb_domain := word2\<rparr>)
od)
 2. \<And>cur. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return () \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>cur. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'6 cur\<rbrace> tcb_sched_action tcb_sched_dequeue word1 \<lbrace>\<lambda>_. tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s)\<rbrace>
 4. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2\<rbrakk> \<Longrightarrow> \<lbrace>invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain word1 word2) and (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s))\<rbrace> gets cur_thread \<lbrace>?Q'6\<rbrace>
 5. \<And>s. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain word1 word2) and (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s))) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets cur_thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 6. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; False\<rbrakk> \<Longrightarrow> no_fail (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain word1 word2) and (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s))) (gets cur_thread) proof (prove)
goal (7 subgoals):
 1. \<And>s s' obj obj'. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; s = transform s'; True; (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s)) s'; get_etcb word1 s' = Some obj'; cdl_objects s word1 = Some obj\<rbrakk> \<Longrightarrow> dcorres (\<lambda>y ya. True) ((=) s) ((=) s') (case obj of Tcb tcb \<Rightarrow> KHeap_D.set_object word1 (Tcb (tcb\<lparr>cdl_tcb_domain := word2\<rparr>)) | _ \<Rightarrow> fail) (set_eobject word1 (obj'\<lparr>tcb_domain := word2\<rparr>))
 2. \<And>s s'. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; s = transform s'; True; (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s)) s'; get_etcb word1 s' \<noteq> None\<rbrakk> \<Longrightarrow> cdl_objects s word1 \<noteq> None
 3. \<And>cur. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return () \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>cur. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'6 cur\<rbrace> tcb_sched_action tcb_sched_dequeue word1 \<lbrace>\<lambda>_. tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s)\<rbrace>
 5. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2\<rbrakk> \<Longrightarrow> \<lbrace>invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain word1 word2) and (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s))\<rbrace> gets cur_thread \<lbrace>?Q'6\<rbrace>
 6. \<And>s. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain word1 word2) and (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s))) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets cur_thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 7. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; False\<rbrakk> \<Longrightarrow> no_fail (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain word1 word2) and (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s))) (gets cur_thread) proof (prove)
goal (7 subgoals):
 1. \<And>s' obj obj'. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; get_etcb word1 s' = Some obj'; cdl_objects (transform s') word1 = Some obj; tcb_at word1 s'; word1 \<noteq> idle_thread s'\<rbrakk> \<Longrightarrow> dcorres (\<lambda>y ya. True) ((=) (transform s')) ((=) s') (case obj of Tcb tcb \<Rightarrow> KHeap_D.set_object word1 (Tcb (tcb\<lparr>cdl_tcb_domain := word2\<rparr>)) | _ \<Rightarrow> fail) (set_eobject word1 (obj'\<lparr>tcb_domain := word2\<rparr>))
 2. \<And>s s'. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; s = transform s'; True; (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s)) s'; get_etcb word1 s' \<noteq> None\<rbrakk> \<Longrightarrow> cdl_objects s word1 \<noteq> None
 3. \<And>cur. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return () \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>cur. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'6 cur\<rbrace> tcb_sched_action tcb_sched_dequeue word1 \<lbrace>\<lambda>_. tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s)\<rbrace>
 5. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2\<rbrakk> \<Longrightarrow> \<lbrace>invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain word1 word2) and (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s))\<rbrace> gets cur_thread \<lbrace>?Q'6\<rbrace>
 6. \<And>s. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain word1 word2) and (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s))) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets cur_thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 7. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; False\<rbrakk> \<Longrightarrow> no_fail (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain word1 word2) and (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s))) (gets cur_thread) proof (prove)
goal (7 subgoals):
 1. \<And>s' obj obj'. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; get_etcb word1 s' = Some obj'; cdl_objects (transform s') word1 = Some obj; word1 \<noteq> idle_thread s'; \<exists>tcb. get_tcb word1 s' = Some tcb\<rbrakk> \<Longrightarrow> dcorres (\<lambda>y ya. True) ((=) (transform s')) ((=) s') (case obj of Tcb tcb \<Rightarrow> KHeap_D.set_object word1 (Tcb (tcb\<lparr>cdl_tcb_domain := word2\<rparr>)) | _ \<Rightarrow> fail) (set_eobject word1 (obj'\<lparr>tcb_domain := word2\<rparr>))
 2. \<And>s s'. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; s = transform s'; True; (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s)) s'; get_etcb word1 s' \<noteq> None\<rbrakk> \<Longrightarrow> cdl_objects s word1 \<noteq> None
 3. \<And>cur. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return () \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>cur. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'6 cur\<rbrace> tcb_sched_action tcb_sched_dequeue word1 \<lbrace>\<lambda>_. tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s)\<rbrace>
 5. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2\<rbrakk> \<Longrightarrow> \<lbrace>invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain word1 word2) and (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s))\<rbrace> gets cur_thread \<lbrace>?Q'6\<rbrace>
 6. \<And>s. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain word1 word2) and (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s))) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets cur_thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 7. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; False\<rbrakk> \<Longrightarrow> no_fail (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain word1 word2) and (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s))) (gets cur_thread) proof (prove)
goal (7 subgoals):
 1. \<And>s' obj' tcb. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; get_etcb word1 s' = Some obj'; word1 \<noteq> idle_thread s'; get_tcb word1 s' = Some tcb\<rbrakk> \<Longrightarrow> dcorres (\<lambda>y ya. True) ((=) (transform s')) ((=) s') (KHeap_D.set_object word1 (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe tcb), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op word1 (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = transform_full_intent (machine_state s') word1 tcb, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = word2\<rparr>)) (set_eobject word1 (obj'\<lparr>tcb_domain := word2\<rparr>))
 2. \<And>s s'. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; s = transform s'; True; (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s)) s'; get_etcb word1 s' \<noteq> None\<rbrakk> \<Longrightarrow> cdl_objects s word1 \<noteq> None
 3. \<And>cur. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return () \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>cur. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'6 cur\<rbrace> tcb_sched_action tcb_sched_dequeue word1 \<lbrace>\<lambda>_. tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s)\<rbrace>
 5. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2\<rbrakk> \<Longrightarrow> \<lbrace>invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain word1 word2) and (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s))\<rbrace> gets cur_thread \<lbrace>?Q'6\<rbrace>
 6. \<And>s. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain word1 word2) and (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s))) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets cur_thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 7. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; False\<rbrakk> \<Longrightarrow> no_fail (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain word1 word2) and (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s))) (gets cur_thread) proof (prove)
goal (10 subgoals):
 1. \<And>s' obj' tcb. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; get_etcb word1 s' = Some obj'; word1 \<noteq> idle_thread s'; get_tcb word1 s' = Some tcb\<rbrakk> \<Longrightarrow> \<exists>tcb'. transform_tcb (machine_state s') word1 tcb' (obj'\<lparr>tcb_domain := word2\<rparr>) = Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe tcb), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op word1 (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = transform_full_intent (machine_state s') word1 tcb, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = word2\<rparr> \<and> kheap s' word1 = Some (TCB tcb')
 2. \<And>s' obj' tcb. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; get_etcb word1 s' = Some obj'; word1 \<noteq> idle_thread s'; get_tcb word1 s' = Some tcb\<rbrakk> \<Longrightarrow> word1 \<noteq> idle_thread s'
 3. \<And>s' obj' tcb. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; get_etcb word1 s' = Some obj'; word1 \<noteq> idle_thread s'; get_tcb word1 s' = Some tcb\<rbrakk> \<Longrightarrow> kheap s' word1 \<noteq> None
 4. \<And>s' obj' tcb. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; get_etcb word1 s' = Some obj'; word1 \<noteq> idle_thread s'; get_tcb word1 s' = Some tcb\<rbrakk> \<Longrightarrow> ekheap s' word1 \<noteq> None
 5. \<And>s s'. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; s = transform s'; True; (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s)) s'; get_etcb word1 s' \<noteq> None\<rbrakk> \<Longrightarrow> cdl_objects s word1 \<noteq> None
 6. \<And>cur. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return () \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>cur. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'6 cur\<rbrace> tcb_sched_action tcb_sched_dequeue word1 \<lbrace>\<lambda>_. tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s)\<rbrace>
 8. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2\<rbrakk> \<Longrightarrow> \<lbrace>invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain word1 word2) and (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s))\<rbrace> gets cur_thread \<lbrace>?Q'6\<rbrace>
 9. \<And>s. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain word1 word2) and (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s))) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets cur_thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 10. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; False\<rbrakk> \<Longrightarrow> no_fail (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain word1 word2) and (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s))) (gets cur_thread) proof (prove)
goal (10 subgoals):
 1. \<And>s' obj' tcb. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; get_etcb word1 s' = Some obj'; word1 \<noteq> idle_thread s'; get_tcb word1 s' = Some tcb; kheap s' word1 = Some (TCB tcb)\<rbrakk> \<Longrightarrow> \<exists>tcb'. transform_tcb (machine_state s') word1 tcb' (obj'\<lparr>tcb_domain := word2\<rparr>) = Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe tcb), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op word1 (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = transform_full_intent (machine_state s') word1 tcb, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = word2\<rparr> \<and> kheap s' word1 = Some (TCB tcb')
 2. \<And>s' obj' tcb. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; get_etcb word1 s' = Some obj'; word1 \<noteq> idle_thread s'; get_tcb word1 s' = Some tcb\<rbrakk> \<Longrightarrow> word1 \<noteq> idle_thread s'
 3. \<And>s' obj' tcb. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; get_etcb word1 s' = Some obj'; word1 \<noteq> idle_thread s'; get_tcb word1 s' = Some tcb\<rbrakk> \<Longrightarrow> kheap s' word1 \<noteq> None
 4. \<And>s' obj' tcb. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; get_etcb word1 s' = Some obj'; word1 \<noteq> idle_thread s'; get_tcb word1 s' = Some tcb\<rbrakk> \<Longrightarrow> ekheap s' word1 \<noteq> None
 5. \<And>s s'. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; s = transform s'; True; (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s)) s'; get_etcb word1 s' \<noteq> None\<rbrakk> \<Longrightarrow> cdl_objects s word1 \<noteq> None
 6. \<And>cur. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return () \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>cur. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'6 cur\<rbrace> tcb_sched_action tcb_sched_dequeue word1 \<lbrace>\<lambda>_. tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s)\<rbrace>
 8. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2\<rbrakk> \<Longrightarrow> \<lbrace>invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain word1 word2) and (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s))\<rbrace> gets cur_thread \<lbrace>?Q'6\<rbrace>
 9. \<And>s. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain word1 word2) and (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s))) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets cur_thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 10. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; False\<rbrakk> \<Longrightarrow> no_fail (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain word1 word2) and (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s))) (gets cur_thread) proof (prove)
goal (9 subgoals):
 1. \<And>s' obj' tcb. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; get_etcb word1 s' = Some obj'; word1 \<noteq> idle_thread s'; get_tcb word1 s' = Some tcb\<rbrakk> \<Longrightarrow> word1 \<noteq> idle_thread s'
 2. \<And>s' obj' tcb. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; get_etcb word1 s' = Some obj'; word1 \<noteq> idle_thread s'; get_tcb word1 s' = Some tcb\<rbrakk> \<Longrightarrow> kheap s' word1 \<noteq> None
 3. \<And>s' obj' tcb. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; get_etcb word1 s' = Some obj'; word1 \<noteq> idle_thread s'; get_tcb word1 s' = Some tcb\<rbrakk> \<Longrightarrow> ekheap s' word1 \<noteq> None
 4. \<And>s s'. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; s = transform s'; True; (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s)) s'; get_etcb word1 s' \<noteq> None\<rbrakk> \<Longrightarrow> cdl_objects s word1 \<noteq> None
 5. \<And>cur. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return () \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>cur. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'6 cur\<rbrace> tcb_sched_action tcb_sched_dequeue word1 \<lbrace>\<lambda>_. tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s)\<rbrace>
 7. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2\<rbrakk> \<Longrightarrow> \<lbrace>invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain word1 word2) and (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s))\<rbrace> gets cur_thread \<lbrace>?Q'6\<rbrace>
 8. \<And>s. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain word1 word2) and (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s))) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets cur_thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 9. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; False\<rbrakk> \<Longrightarrow> no_fail (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain word1 word2) and (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s))) (gets cur_thread) proof (prove)
goal (8 subgoals):
 1. \<And>s' obj' tcb. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; get_etcb word1 s' = Some obj'; word1 \<noteq> idle_thread s'; get_tcb word1 s' = Some tcb\<rbrakk> \<Longrightarrow> kheap s' word1 \<noteq> None
 2. \<And>s' obj' tcb. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; get_etcb word1 s' = Some obj'; word1 \<noteq> idle_thread s'; get_tcb word1 s' = Some tcb\<rbrakk> \<Longrightarrow> ekheap s' word1 \<noteq> None
 3. \<And>s s'. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; s = transform s'; True; (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s)) s'; get_etcb word1 s' \<noteq> None\<rbrakk> \<Longrightarrow> cdl_objects s word1 \<noteq> None
 4. \<And>cur. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return () \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>cur. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'6 cur\<rbrace> tcb_sched_action tcb_sched_dequeue word1 \<lbrace>\<lambda>_. tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s)\<rbrace>
 6. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2\<rbrakk> \<Longrightarrow> \<lbrace>invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain word1 word2) and (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s))\<rbrace> gets cur_thread \<lbrace>?Q'6\<rbrace>
 7. \<And>s. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain word1 word2) and (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s))) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets cur_thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 8. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; False\<rbrakk> \<Longrightarrow> no_fail (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain word1 word2) and (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s))) (gets cur_thread) proof (prove)
goal (8 subgoals):
 1. \<And>s' obj' tcb. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; get_etcb word1 s' = Some obj'; word1 \<noteq> idle_thread s'; get_tcb word1 s' = Some tcb; kheap s' word1 = Some (TCB tcb)\<rbrakk> \<Longrightarrow> kheap s' word1 \<noteq> None
 2. \<And>s' obj' tcb. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; get_etcb word1 s' = Some obj'; word1 \<noteq> idle_thread s'; get_tcb word1 s' = Some tcb\<rbrakk> \<Longrightarrow> ekheap s' word1 \<noteq> None
 3. \<And>s s'. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; s = transform s'; True; (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s)) s'; get_etcb word1 s' \<noteq> None\<rbrakk> \<Longrightarrow> cdl_objects s word1 \<noteq> None
 4. \<And>cur. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return () \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>cur. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'6 cur\<rbrace> tcb_sched_action tcb_sched_dequeue word1 \<lbrace>\<lambda>_. tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s)\<rbrace>
 6. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2\<rbrakk> \<Longrightarrow> \<lbrace>invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain word1 word2) and (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s))\<rbrace> gets cur_thread \<lbrace>?Q'6\<rbrace>
 7. \<And>s. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain word1 word2) and (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s))) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets cur_thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 8. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; False\<rbrakk> \<Longrightarrow> no_fail (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain word1 word2) and (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s))) (gets cur_thread) proof (prove)
goal (7 subgoals):
 1. \<And>s' obj' tcb. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; get_etcb word1 s' = Some obj'; word1 \<noteq> idle_thread s'; get_tcb word1 s' = Some tcb\<rbrakk> \<Longrightarrow> ekheap s' word1 \<noteq> None
 2. \<And>s s'. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; s = transform s'; True; (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s)) s'; get_etcb word1 s' \<noteq> None\<rbrakk> \<Longrightarrow> cdl_objects s word1 \<noteq> None
 3. \<And>cur. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return () \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>cur. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'6 cur\<rbrace> tcb_sched_action tcb_sched_dequeue word1 \<lbrace>\<lambda>_. tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s)\<rbrace>
 5. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2\<rbrakk> \<Longrightarrow> \<lbrace>invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain word1 word2) and (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s))\<rbrace> gets cur_thread \<lbrace>?Q'6\<rbrace>
 6. \<And>s. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain word1 word2) and (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s))) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets cur_thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 7. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; False\<rbrakk> \<Longrightarrow> no_fail (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain word1 word2) and (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s))) (gets cur_thread) proof (prove)
goal (6 subgoals):
 1. \<And>s s'. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; s = transform s'; True; (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s)) s'; get_etcb word1 s' \<noteq> None\<rbrakk> \<Longrightarrow> cdl_objects s word1 \<noteq> None
 2. \<And>cur. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return () \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>cur. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'6 cur\<rbrace> tcb_sched_action tcb_sched_dequeue word1 \<lbrace>\<lambda>_. tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s)\<rbrace>
 4. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2\<rbrakk> \<Longrightarrow> \<lbrace>invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain word1 word2) and (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s))\<rbrace> gets cur_thread \<lbrace>?Q'6\<rbrace>
 5. \<And>s. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain word1 word2) and (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s))) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets cur_thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 6. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; False\<rbrakk> \<Longrightarrow> no_fail (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain word1 word2) and (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s))) (gets cur_thread) proof (prove)
goal (6 subgoals):
 1. \<And>s' y. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; get_etcb word1 s' = Some y; tcb_at word1 s'; word1 \<noteq> idle_thread s'\<rbrakk> \<Longrightarrow> \<exists>y. cdl_objects (transform s') word1 = Some y
 2. \<And>cur. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return () \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>cur. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'6 cur\<rbrace> tcb_sched_action tcb_sched_dequeue word1 \<lbrace>\<lambda>_. tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s)\<rbrace>
 4. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2\<rbrakk> \<Longrightarrow> \<lbrace>invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain word1 word2) and (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s))\<rbrace> gets cur_thread \<lbrace>?Q'6\<rbrace>
 5. \<And>s. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain word1 word2) and (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s))) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets cur_thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 6. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; False\<rbrakk> \<Longrightarrow> no_fail (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain word1 word2) and (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s))) (gets cur_thread) proof (prove)
goal (6 subgoals):
 1. \<And>s' y. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; get_etcb word1 s' = Some y; word1 \<noteq> idle_thread s'; \<exists>tcb. get_tcb word1 s' = Some tcb\<rbrakk> \<Longrightarrow> \<exists>y. cdl_objects (transform s') word1 = Some y
 2. \<And>cur. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return () \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>cur. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'6 cur\<rbrace> tcb_sched_action tcb_sched_dequeue word1 \<lbrace>\<lambda>_. tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s)\<rbrace>
 4. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2\<rbrakk> \<Longrightarrow> \<lbrace>invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain word1 word2) and (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s))\<rbrace> gets cur_thread \<lbrace>?Q'6\<rbrace>
 5. \<And>s. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain word1 word2) and (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s))) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets cur_thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 6. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; False\<rbrakk> \<Longrightarrow> no_fail (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain word1 word2) and (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s))) (gets cur_thread) proof (prove)
goal (5 subgoals):
 1. \<And>cur. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return () \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>cur. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'6 cur\<rbrace> tcb_sched_action tcb_sched_dequeue word1 \<lbrace>\<lambda>_. tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s)\<rbrace>
 3. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2\<rbrakk> \<Longrightarrow> \<lbrace>invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain word1 word2) and (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s))\<rbrace> gets cur_thread \<lbrace>?Q'6\<rbrace>
 4. \<And>s. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain word1 word2) and (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s))) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets cur_thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; False\<rbrakk> \<Longrightarrow> no_fail (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain word1 word2) and (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s))) (gets cur_thread) proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain word1 word2) and (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s))) s\<rbrakk> \<Longrightarrow> tcb_at word1 s \<and> word1 \<noteq> idle_thread s
 2. \<And>s. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain word1 word2) and (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s))) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets cur_thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; False\<rbrakk> \<Longrightarrow> no_fail (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain word1 word2) and (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s))) (gets cur_thread) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain word1 word2) and (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s))) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets cur_thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 2. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; False\<rbrakk> \<Longrightarrow> no_fail (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain word1 word2) and (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s))) (gets cur_thread) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain word1 word2); i' = invocation.InvokeDomain word1 word2; False\<rbrakk> \<Longrightarrow> no_fail (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain word1 word2) and (tcb_at word1 and (\<lambda>s. word1 \<noteq> idle_thread s))) (gets cur_thread) proof (prove)
goal:
No subgoals!