theory Syscall_DR

lemma handle_fault_corres:
  "dcorres dc \<top>
     (\<lambda>s. cur_thread s = thread \<and> not_idle_thread thread s \<and>
          st_tcb_at active thread s \<and> valid_fault ft' \<and>
          invs s \<and> valid_irq_node s \<and> valid_etcbs s)
     Endpoint_D.handle_fault
     (Ipc_A.handle_fault thread ft')" apply (simp add:Endpoint_D.handle_fault_def Ipc_A.handle_fault_def) apply (rule dcorres_gets_the) apply (clarsimp dest!:get_tcb_SomeD) apply (frule(1) valid_etcbs_tcb_etcb, clarsimp) apply (rule corres_guard_imp) apply (rule corres_split_catch[where r=dc and f = dc]) apply (rule_tac tcb = obj' and etcb=etcb in send_fault_ipc_corres) apply (clarsimp simp:transform_def transform_current_thread_def
                             not_idle_thread_def) apply (rule_tac F = "obj = cur_thread s'" in corres_gen_asm2) apply simp apply (rule dcorres_handle_double_fault) apply (wp) apply (simp add:send_fault_ipc_def not_idle_thread_def Let_def) apply (wp hoare_drop_imps hoare_vcg_ball_lift | wpc)+ apply (rule_tac Q'="\<lambda>r s. invs s \<and> valid_etcbs s \<and> obj\<noteq> idle_thread s \<and> obj = cur_thread s'"
        in hoare_post_imp_R) apply wp apply (clarsimp simp:invs_mdb invs_valid_idle) apply wp apply simp apply (clarsimp simp:obj_at_def transform_def
     invs_mdb invs_valid_idle
     transform_current_thread_def not_idle_thread_def) apply (clarsimp dest!:get_tcb_SomeD
    simp: generates_pending_def not_idle_thread_def st_tcb_at_def obj_at_def)+ apply (auto simp:transform_def transform_current_thread_def
    not_idle_thread_def  split:Structures_A.thread_state.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (\<lambda>s. cur_thread s = thread \<and> not_idle_thread thread s \<and> st_tcb_at active thread s \<and> valid_fault ft' \<and> invs s \<and> valid_irq_node s \<and> valid_etcbs s) Endpoint_D.handle_fault (Ipc_A.handle_fault thread ft') proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (\<lambda>s. cur_thread s = thread \<and> not_idle_thread thread s \<and> st_tcb_at active thread s \<and> valid_fault ft' \<and> invs s \<and> valid_irq_node s \<and> valid_etcbs s) (do tcb_id <- gets_the cdl_current_thread;
Endpoint_D.send_fault_ipc tcb_id <catch> (\<lambda>_. KHeap_D.set_cap (tcb_id, tcb_pending_op_slot) cdl_cap.NullCap)
od) (do _ <- gets_the (get_tcb thread);
Ipc_A.send_fault_ipc thread ft' <catch> handle_double_fault thread ft'
od) proof (prove)
goal (2 subgoals):
 1. \<And>s s' obj obj'. \<lbrakk>s = transform s'; True; cur_thread s' = thread \<and> not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_fault ft' \<and> invs s' \<and> valid_irq_node s' \<and> valid_etcbs s'; get_tcb thread s' = Some obj'; cdl_current_thread s = Some obj\<rbrakk> \<Longrightarrow> dcorres dc ((=) s) ((=) s') (Endpoint_D.send_fault_ipc obj <catch> (\<lambda>_. KHeap_D.set_cap (obj, tcb_pending_op_slot) cdl_cap.NullCap)) (Ipc_A.send_fault_ipc thread ft' <catch> handle_double_fault thread ft')
 2. \<And>s s'. \<lbrakk>s = transform s'; True; cur_thread s' = thread \<and> not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_fault ft' \<and> invs s' \<and> valid_irq_node s' \<and> valid_etcbs s'; get_tcb thread s' \<noteq> None\<rbrakk> \<Longrightarrow> cdl_current_thread s \<noteq> None proof (prove)
goal (2 subgoals):
 1. \<And>s' obj obj'. \<lbrakk>cdl_current_thread (transform s') = Some obj; kheap s' (cur_thread s') = Some (TCB obj'); thread = cur_thread s'; not_idle_thread (cur_thread s') s'; st_tcb_at active (cur_thread s') s'; valid_fault ft'; invs s'; valid_irq_node s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (Endpoint_D.send_fault_ipc obj <catch> (\<lambda>_. KHeap_D.set_cap (obj, tcb_pending_op_slot) cdl_cap.NullCap)) (Ipc_A.send_fault_ipc (cur_thread s') ft' <catch> handle_double_fault (cur_thread s') ft')
 2. \<And>s s'. \<lbrakk>s = transform s'; True; cur_thread s' = thread \<and> not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_fault ft' \<and> invs s' \<and> valid_irq_node s' \<and> valid_etcbs s'; get_tcb thread s' \<noteq> None\<rbrakk> \<Longrightarrow> cdl_current_thread s \<noteq> None proof (prove)
goal (2 subgoals):
 1. \<And>s' obj obj' etcb. \<lbrakk>cdl_current_thread (transform s') = Some obj; kheap s' (cur_thread s') = Some (TCB obj'); thread = cur_thread s'; not_idle_thread (cur_thread s') s'; st_tcb_at active (cur_thread s') s'; valid_fault ft'; invs s'; valid_irq_node s'; valid_etcbs s'; ekheap s' (cur_thread s') = Some etcb\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (Endpoint_D.send_fault_ipc obj <catch> (\<lambda>_. KHeap_D.set_cap (obj, tcb_pending_op_slot) cdl_cap.NullCap)) (Ipc_A.send_fault_ipc (cur_thread s') ft' <catch> handle_double_fault (cur_thread s') ft')
 2. \<And>s s'. \<lbrakk>s = transform s'; True; cur_thread s' = thread \<and> not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_fault ft' \<and> invs s' \<and> valid_irq_node s' \<and> valid_etcbs s'; get_tcb thread s' \<noteq> None\<rbrakk> \<Longrightarrow> cdl_current_thread s \<noteq> None proof (prove)
goal (4 subgoals):
 1. \<And>s' obj obj' etcb. \<lbrakk>cdl_current_thread (transform s') = Some obj; kheap s' (cur_thread s') = Some (TCB obj'); thread = cur_thread s'; not_idle_thread (cur_thread s') s'; st_tcb_at active (cur_thread s') s'; valid_fault ft'; invs s'; valid_irq_node s'; valid_etcbs s'; ekheap s' (cur_thread s') = Some etcb\<rbrakk> \<Longrightarrow> dcorres dc (?Q22 s' obj obj' etcb) (?Q'22 s' obj obj' etcb) (Endpoint_D.send_fault_ipc obj <catch> (\<lambda>_. KHeap_D.set_cap (obj, tcb_pending_op_slot) cdl_cap.NullCap)) (Ipc_A.send_fault_ipc (cur_thread s') ft' <catch> handle_double_fault (cur_thread s') ft')
 2. \<And>s' obj obj' etcb s. \<lbrakk>cdl_current_thread (transform s') = Some obj; kheap s' (cur_thread s') = Some (TCB obj'); thread = cur_thread s'; not_idle_thread (cur_thread s') s'; st_tcb_at active (cur_thread s') s'; valid_fault ft'; invs s'; valid_irq_node s'; valid_etcbs s'; ekheap s' (cur_thread s') = Some etcb; transform s' = s\<rbrakk> \<Longrightarrow> ?Q22 s' obj obj' etcb s
 3. \<And>s' obj obj' etcb s. \<lbrakk>cdl_current_thread (transform s') = Some obj; kheap s' (cur_thread s') = Some (TCB obj'); thread = cur_thread s'; not_idle_thread (cur_thread s') s'; st_tcb_at active (cur_thread s') s'; valid_fault ft'; invs s'; valid_irq_node s'; valid_etcbs s'; ekheap s' (cur_thread s') = Some etcb; s' = s\<rbrakk> \<Longrightarrow> ?Q'22 s' obj obj' etcb s
 4. \<And>s s'. \<lbrakk>s = transform s'; True; cur_thread s' = thread \<and> not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_fault ft' \<and> invs s' \<and> valid_irq_node s' \<and> valid_etcbs s'; get_tcb thread s' \<noteq> None\<rbrakk> \<Longrightarrow> cdl_current_thread s \<noteq> None proof (prove)
goal (7 subgoals):
 1. \<And>s' obj obj' etcb. \<lbrakk>cdl_current_thread (transform s') = Some obj; kheap s' (cur_thread s') = Some (TCB obj'); thread = cur_thread s'; not_idle_thread (cur_thread s') s'; st_tcb_at active (cur_thread s') s'; valid_fault ft'; invs s'; valid_irq_node s'; valid_etcbs s'; ekheap s' (cur_thread s') = Some etcb\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (?P26 s' obj obj' etcb) (?P'26 s' obj obj' etcb) (Endpoint_D.send_fault_ipc obj) (Ipc_A.send_fault_ipc (cur_thread s') ft')
 2. \<And>s' obj obj' etcb uu_ ft'a. \<lbrakk>cdl_current_thread (transform s') = Some obj; kheap s' (cur_thread s') = Some (TCB obj'); thread = cur_thread s'; not_idle_thread (cur_thread s') s'; st_tcb_at active (cur_thread s') s'; valid_fault ft'; invs s'; valid_irq_node s'; valid_etcbs s'; ekheap s' (cur_thread s') = Some etcb; dc uu_ ft'a\<rbrakk> \<Longrightarrow> dcorres dc (?E26 s' obj obj' etcb uu_) (?E'26 s' obj obj' etcb ft'a) (KHeap_D.set_cap (obj, tcb_pending_op_slot) cdl_cap.NullCap) (handle_double_fault (cur_thread s') ft' ft'a)
 3. \<And>s' obj obj' etcb. \<lbrakk>cdl_current_thread (transform s') = Some obj; kheap s' (cur_thread s') = Some (TCB obj'); thread = cur_thread s'; not_idle_thread (cur_thread s') s'; st_tcb_at active (cur_thread s') s'; valid_fault ft'; invs s'; valid_irq_node s'; valid_etcbs s'; ekheap s' (cur_thread s') = Some etcb\<rbrakk> \<Longrightarrow> \<lbrace>?Q26 s' obj obj' etcb\<rbrace> Endpoint_D.send_fault_ipc obj \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?E26 s' obj obj' etcb\<rbrace>
 4. \<And>s' obj obj' etcb. \<lbrakk>cdl_current_thread (transform s') = Some obj; kheap s' (cur_thread s') = Some (TCB obj'); thread = cur_thread s'; not_idle_thread (cur_thread s') s'; st_tcb_at active (cur_thread s') s'; valid_fault ft'; invs s'; valid_irq_node s'; valid_etcbs s'; ekheap s' (cur_thread s') = Some etcb\<rbrakk> \<Longrightarrow> \<lbrace>?Q'26 s' obj obj' etcb\<rbrace> Ipc_A.send_fault_ipc (cur_thread s') ft' \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?E'26 s' obj obj' etcb\<rbrace>
 5. \<And>s' obj obj' etcb s. \<lbrakk>cdl_current_thread (transform s') = Some obj; kheap s' (cur_thread s') = Some (TCB obj'); thread = cur_thread s'; not_idle_thread (cur_thread s') s'; st_tcb_at active (cur_thread s') s'; valid_fault ft'; invs s'; valid_irq_node s'; valid_etcbs s'; ekheap s' (cur_thread s') = Some etcb; transform s' = s\<rbrakk> \<Longrightarrow> (?P26 s' obj obj' etcb and ?Q26 s' obj obj' etcb) s
 6. \<And>s' obj obj' etcb s. \<lbrakk>cdl_current_thread (transform s') = Some obj; kheap s' (cur_thread s') = Some (TCB obj'); thread = cur_thread s'; not_idle_thread (cur_thread s') s'; st_tcb_at active (cur_thread s') s'; valid_fault ft'; invs s'; valid_irq_node s'; valid_etcbs s'; ekheap s' (cur_thread s') = Some etcb; s' = s\<rbrakk> \<Longrightarrow> (?P'26 s' obj obj' etcb and ?Q'26 s' obj obj' etcb) s
 7. \<And>s s'. \<lbrakk>s = transform s'; True; cur_thread s' = thread \<and> not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_fault ft' \<and> invs s' \<and> valid_irq_node s' \<and> valid_etcbs s'; get_tcb thread s' \<noteq> None\<rbrakk> \<Longrightarrow> cdl_current_thread s \<noteq> None proof (prove)
goal (7 subgoals):
 1. \<And>s' obj obj' etcb. \<lbrakk>cdl_current_thread (transform s') = Some obj; kheap s' (cur_thread s') = Some (TCB obj'); thread = cur_thread s'; not_idle_thread (cur_thread s') s'; st_tcb_at active (cur_thread s') s'; valid_fault ft'; invs s'; valid_irq_node s'; valid_etcbs s'; ekheap s' (cur_thread s') = Some etcb\<rbrakk> \<Longrightarrow> obj = cur_thread s'
 2. \<And>s' obj obj' etcb uu_ ft'a. \<lbrakk>cdl_current_thread (transform s') = Some obj; kheap s' (cur_thread s') = Some (TCB obj'); thread = cur_thread s'; not_idle_thread (cur_thread s') s'; st_tcb_at active (cur_thread s') s'; valid_fault ft'; invs s'; valid_irq_node s'; valid_etcbs s'; ekheap s' (cur_thread s') = Some etcb; dc uu_ ft'a\<rbrakk> \<Longrightarrow> dcorres dc (?E26 s' obj obj' etcb uu_) (?E'26 s' obj obj' etcb ft'a) (KHeap_D.set_cap (obj, tcb_pending_op_slot) cdl_cap.NullCap) (handle_double_fault (cur_thread s') ft' ft'a)
 3. \<And>s' obj obj' etcb. \<lbrakk>cdl_current_thread (transform s') = Some obj; kheap s' (cur_thread s') = Some (TCB obj'); thread = cur_thread s'; not_idle_thread (cur_thread s') s'; st_tcb_at active (cur_thread s') s'; valid_fault ft'; invs s'; valid_irq_node s'; valid_etcbs s'; ekheap s' (cur_thread s') = Some etcb\<rbrakk> \<Longrightarrow> \<lbrace>?Q26 s' obj obj' etcb\<rbrace> Endpoint_D.send_fault_ipc obj \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?E26 s' obj obj' etcb\<rbrace>
 4. \<And>s' obj obj' etcb. \<lbrakk>cdl_current_thread (transform s') = Some obj; kheap s' (cur_thread s') = Some (TCB obj'); thread = cur_thread s'; not_idle_thread (cur_thread s') s'; st_tcb_at active (cur_thread s') s'; valid_fault ft'; invs s'; valid_irq_node s'; valid_etcbs s'; ekheap s' (cur_thread s') = Some etcb\<rbrakk> \<Longrightarrow> \<lbrace>?Q'26 s' obj obj' etcb\<rbrace> Ipc_A.send_fault_ipc (cur_thread s') ft' \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?E'26 s' obj obj' etcb\<rbrace>
 5. \<And>s' obj obj' etcb s. \<lbrakk>cdl_current_thread (transform s') = Some obj; kheap s' (cur_thread s') = Some (TCB obj'); thread = cur_thread s'; not_idle_thread (cur_thread s') s'; st_tcb_at active (cur_thread s') s'; valid_fault ft'; invs s'; valid_irq_node s'; valid_etcbs s'; ekheap s' (cur_thread s') = Some etcb; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q26 s' obj obj' etcb) s
 6. \<And>s' obj obj' etcb s. \<lbrakk>cdl_current_thread (transform s') = Some obj; kheap s' (cur_thread s') = Some (TCB obj'); thread = cur_thread s'; not_idle_thread (cur_thread s') s'; st_tcb_at active (cur_thread s') s'; valid_fault ft'; invs s'; valid_irq_node s'; valid_etcbs s'; ekheap s' (cur_thread s') = Some etcb; s' = s\<rbrakk> \<Longrightarrow> (not_idle_thread (cur_thread s') and st_tcb_at active (cur_thread s') and valid_irq_node and invs and ko_at (TCB obj') (cur_thread s') and (\<lambda>s. ekheap s (cur_thread s') = Some etcb) and (\<lambda>s. not_idle_thread (cur_thread s) s) and (\<lambda>_. valid_fault ft') and valid_etcbs and ?Q'26 s' obj obj' etcb) s
 7. \<And>s s'. \<lbrakk>s = transform s'; True; cur_thread s' = thread \<and> not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_fault ft' \<and> invs s' \<and> valid_irq_node s' \<and> valid_etcbs s'; get_tcb thread s' \<noteq> None\<rbrakk> \<Longrightarrow> cdl_current_thread s \<noteq> None proof (prove)
goal (6 subgoals):
 1. \<And>s' obj obj' etcb uu_ ft'a. \<lbrakk>cdl_current_thread (transform s') = Some obj; kheap s' (cur_thread s') = Some (TCB obj'); thread = cur_thread s'; not_idle_thread (cur_thread s') s'; st_tcb_at active (cur_thread s') s'; valid_fault ft'; invs s'; valid_irq_node s'; valid_etcbs s'; ekheap s' (cur_thread s') = Some etcb; dc uu_ ft'a\<rbrakk> \<Longrightarrow> dcorres dc (?E26 s' obj obj' etcb uu_) (?E'26 s' obj obj' etcb ft'a) (KHeap_D.set_cap (obj, tcb_pending_op_slot) cdl_cap.NullCap) (handle_double_fault (cur_thread s') ft' ft'a)
 2. \<And>s' obj obj' etcb. \<lbrakk>cdl_current_thread (transform s') = Some obj; kheap s' (cur_thread s') = Some (TCB obj'); thread = cur_thread s'; not_idle_thread (cur_thread s') s'; st_tcb_at active (cur_thread s') s'; valid_fault ft'; invs s'; valid_irq_node s'; valid_etcbs s'; ekheap s' (cur_thread s') = Some etcb\<rbrakk> \<Longrightarrow> \<lbrace>?Q26 s' obj obj' etcb\<rbrace> Endpoint_D.send_fault_ipc obj \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?E26 s' obj obj' etcb\<rbrace>
 3. \<And>s' obj obj' etcb. \<lbrakk>cdl_current_thread (transform s') = Some obj; kheap s' (cur_thread s') = Some (TCB obj'); thread = cur_thread s'; not_idle_thread (cur_thread s') s'; st_tcb_at active (cur_thread s') s'; valid_fault ft'; invs s'; valid_irq_node s'; valid_etcbs s'; ekheap s' (cur_thread s') = Some etcb\<rbrakk> \<Longrightarrow> \<lbrace>?Q'26 s' obj obj' etcb\<rbrace> Ipc_A.send_fault_ipc (cur_thread s') ft' \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?E'26 s' obj obj' etcb\<rbrace>
 4. \<And>s' obj obj' etcb s. \<lbrakk>cdl_current_thread (transform s') = Some obj; kheap s' (cur_thread s') = Some (TCB obj'); thread = cur_thread s'; not_idle_thread (cur_thread s') s'; st_tcb_at active (cur_thread s') s'; valid_fault ft'; invs s'; valid_irq_node s'; valid_etcbs s'; ekheap s' (cur_thread s') = Some etcb; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q26 s' obj obj' etcb) s
 5. \<And>s' obj obj' etcb s. \<lbrakk>cdl_current_thread (transform s') = Some obj; kheap s' (cur_thread s') = Some (TCB obj'); thread = cur_thread s'; not_idle_thread (cur_thread s') s'; st_tcb_at active (cur_thread s') s'; valid_fault ft'; invs s'; valid_irq_node s'; valid_etcbs s'; ekheap s' (cur_thread s') = Some etcb; s' = s\<rbrakk> \<Longrightarrow> (not_idle_thread (cur_thread s') and st_tcb_at active (cur_thread s') and valid_irq_node and invs and ko_at (TCB obj') (cur_thread s') and (\<lambda>s. ekheap s (cur_thread s') = Some etcb) and (\<lambda>s. not_idle_thread (cur_thread s) s) and (\<lambda>_. valid_fault ft') and valid_etcbs and ?Q'26 s' obj obj' etcb) s
 6. \<And>s s'. \<lbrakk>s = transform s'; True; cur_thread s' = thread \<and> not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_fault ft' \<and> invs s' \<and> valid_irq_node s' \<and> valid_etcbs s'; get_tcb thread s' \<noteq> None\<rbrakk> \<Longrightarrow> cdl_current_thread s \<noteq> None proof (prove)
goal (6 subgoals):
 1. \<And>s' obj obj' etcb uu_ ft'a. \<lbrakk>cdl_current_thread (transform s') = Some obj; kheap s' (cur_thread s') = Some (TCB obj'); thread = cur_thread s'; not_idle_thread (cur_thread s') s'; st_tcb_at active (cur_thread s') s'; valid_fault ft'; invs s'; valid_irq_node s'; valid_etcbs s'; ekheap s' (cur_thread s') = Some etcb; dc uu_ ft'a; obj = cur_thread s'\<rbrakk> \<Longrightarrow> dcorres dc (?E26 s' obj obj' etcb uu_) (?P'33 s' obj obj' etcb ft'a) (KHeap_D.set_cap (obj, tcb_pending_op_slot) cdl_cap.NullCap) (handle_double_fault (cur_thread s') ft' ft'a)
 2. \<And>s' obj obj' etcb. \<lbrakk>cdl_current_thread (transform s') = Some obj; kheap s' (cur_thread s') = Some (TCB obj'); thread = cur_thread s'; not_idle_thread (cur_thread s') s'; st_tcb_at active (cur_thread s') s'; valid_fault ft'; invs s'; valid_irq_node s'; valid_etcbs s'; ekheap s' (cur_thread s') = Some etcb\<rbrakk> \<Longrightarrow> \<lbrace>?Q26 s' obj obj' etcb\<rbrace> Endpoint_D.send_fault_ipc obj \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?E26 s' obj obj' etcb\<rbrace>
 3. \<And>s' obj obj' etcb. \<lbrakk>cdl_current_thread (transform s') = Some obj; kheap s' (cur_thread s') = Some (TCB obj'); thread = cur_thread s'; not_idle_thread (cur_thread s') s'; st_tcb_at active (cur_thread s') s'; valid_fault ft'; invs s'; valid_irq_node s'; valid_etcbs s'; ekheap s' (cur_thread s') = Some etcb\<rbrakk> \<Longrightarrow> \<lbrace>?Q'26 s' obj obj' etcb\<rbrace> Ipc_A.send_fault_ipc (cur_thread s') ft' \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>ft'. ?P'33 s' obj obj' etcb ft' and (\<lambda>s. obj = cur_thread s')\<rbrace>
 4. \<And>s' obj obj' etcb s. \<lbrakk>cdl_current_thread (transform s') = Some obj; kheap s' (cur_thread s') = Some (TCB obj'); thread = cur_thread s'; not_idle_thread (cur_thread s') s'; st_tcb_at active (cur_thread s') s'; valid_fault ft'; invs s'; valid_irq_node s'; valid_etcbs s'; ekheap s' (cur_thread s') = Some etcb; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q26 s' obj obj' etcb) s
 5. \<And>s' obj obj' etcb s. \<lbrakk>cdl_current_thread (transform s') = Some obj; kheap s' (cur_thread s') = Some (TCB obj'); thread = cur_thread s'; not_idle_thread (cur_thread s') s'; st_tcb_at active (cur_thread s') s'; valid_fault ft'; invs s'; valid_irq_node s'; valid_etcbs s'; ekheap s' (cur_thread s') = Some etcb; s' = s\<rbrakk> \<Longrightarrow> (not_idle_thread (cur_thread s') and st_tcb_at active (cur_thread s') and valid_irq_node and invs and ko_at (TCB obj') (cur_thread s') and (\<lambda>s. ekheap s (cur_thread s') = Some etcb) and (\<lambda>s. not_idle_thread (cur_thread s) s) and (\<lambda>_. valid_fault ft') and valid_etcbs and ?Q'26 s' obj obj' etcb) s
 6. \<And>s s'. \<lbrakk>s = transform s'; True; cur_thread s' = thread \<and> not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_fault ft' \<and> invs s' \<and> valid_irq_node s' \<and> valid_etcbs s'; get_tcb thread s' \<noteq> None\<rbrakk> \<Longrightarrow> cdl_current_thread s \<noteq> None proof (prove)
goal (6 subgoals):
 1. \<And>s' obj obj' etcb uu_ ft'a. \<lbrakk>cdl_current_thread (transform s') = Some (cur_thread s'); kheap s' (cur_thread s') = Some (TCB obj'); thread = cur_thread s'; not_idle_thread (cur_thread s') s'; st_tcb_at active (cur_thread s') s'; valid_fault ft'; invs s'; valid_irq_node s'; valid_etcbs s'; ekheap s' (cur_thread s') = Some etcb; obj = cur_thread s'\<rbrakk> \<Longrightarrow> dcorres dc (?E26 s' (cur_thread s') obj' etcb uu_) (?P'33 s' (cur_thread s') obj' etcb ft'a) (KHeap_D.set_cap (cur_thread s', tcb_pending_op_slot) cdl_cap.NullCap) (handle_double_fault (cur_thread s') ft' ft'a)
 2. \<And>s' obj obj' etcb. \<lbrakk>cdl_current_thread (transform s') = Some obj; kheap s' (cur_thread s') = Some (TCB obj'); thread = cur_thread s'; not_idle_thread (cur_thread s') s'; st_tcb_at active (cur_thread s') s'; valid_fault ft'; invs s'; valid_irq_node s'; valid_etcbs s'; ekheap s' (cur_thread s') = Some etcb\<rbrakk> \<Longrightarrow> \<lbrace>?Q26 s' obj obj' etcb\<rbrace> Endpoint_D.send_fault_ipc obj \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?E26 s' obj obj' etcb\<rbrace>
 3. \<And>s' obj obj' etcb. \<lbrakk>cdl_current_thread (transform s') = Some obj; kheap s' (cur_thread s') = Some (TCB obj'); thread = cur_thread s'; not_idle_thread (cur_thread s') s'; st_tcb_at active (cur_thread s') s'; valid_fault ft'; invs s'; valid_irq_node s'; valid_etcbs s'; ekheap s' (cur_thread s') = Some etcb\<rbrakk> \<Longrightarrow> \<lbrace>?Q'26 s' obj obj' etcb\<rbrace> Ipc_A.send_fault_ipc (cur_thread s') ft' \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>ft'. ?P'33 s' obj obj' etcb ft' and (\<lambda>s. obj = cur_thread s')\<rbrace>
 4. \<And>s' obj obj' etcb s. \<lbrakk>cdl_current_thread (transform s') = Some obj; kheap s' (cur_thread s') = Some (TCB obj'); thread = cur_thread s'; not_idle_thread (cur_thread s') s'; st_tcb_at active (cur_thread s') s'; valid_fault ft'; invs s'; valid_irq_node s'; valid_etcbs s'; ekheap s' (cur_thread s') = Some etcb; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q26 s' obj obj' etcb) s
 5. \<And>s' obj obj' etcb s. \<lbrakk>cdl_current_thread (transform s') = Some obj; kheap s' (cur_thread s') = Some (TCB obj'); thread = cur_thread s'; not_idle_thread (cur_thread s') s'; st_tcb_at active (cur_thread s') s'; valid_fault ft'; invs s'; valid_irq_node s'; valid_etcbs s'; ekheap s' (cur_thread s') = Some etcb; s' = s\<rbrakk> \<Longrightarrow> (not_idle_thread (cur_thread s') and st_tcb_at active (cur_thread s') and valid_irq_node and invs and ko_at (TCB obj') (cur_thread s') and (\<lambda>s. ekheap s (cur_thread s') = Some etcb) and (\<lambda>s. not_idle_thread (cur_thread s) s) and (\<lambda>_. valid_fault ft') and valid_etcbs and ?Q'26 s' obj obj' etcb) s
 6. \<And>s s'. \<lbrakk>s = transform s'; True; cur_thread s' = thread \<and> not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_fault ft' \<and> invs s' \<and> valid_irq_node s' \<and> valid_etcbs s'; get_tcb thread s' \<noteq> None\<rbrakk> \<Longrightarrow> cdl_current_thread s \<noteq> None proof (prove)
goal (5 subgoals):
 1. \<And>s' obj obj' etcb. \<lbrakk>cdl_current_thread (transform s') = Some obj; kheap s' (cur_thread s') = Some (TCB obj'); thread = cur_thread s'; not_idle_thread (cur_thread s') s'; st_tcb_at active (cur_thread s') s'; valid_fault ft'; invs s'; valid_irq_node s'; valid_etcbs s'; ekheap s' (cur_thread s') = Some etcb\<rbrakk> \<Longrightarrow> \<lbrace>?Q26 s' obj obj' etcb\<rbrace> Endpoint_D.send_fault_ipc obj \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>a b. True\<rbrace>
 2. \<And>s' obj obj' etcb. \<lbrakk>cdl_current_thread (transform s') = Some obj; kheap s' (cur_thread s') = Some (TCB obj'); thread = cur_thread s'; not_idle_thread (cur_thread s') s'; st_tcb_at active (cur_thread s') s'; valid_fault ft'; invs s'; valid_irq_node s'; valid_etcbs s'; ekheap s' (cur_thread s') = Some etcb\<rbrakk> \<Longrightarrow> \<lbrace>?Q'26 s' obj obj' etcb\<rbrace> Ipc_A.send_fault_ipc (cur_thread s') ft' \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>ft'. valid_mdb and not_idle_thread obj and valid_idle and valid_etcbs and (\<lambda>s. obj = cur_thread s')\<rbrace>
 3. \<And>s' obj obj' etcb s. \<lbrakk>cdl_current_thread (transform s') = Some obj; kheap s' (cur_thread s') = Some (TCB obj'); thread = cur_thread s'; not_idle_thread (cur_thread s') s'; st_tcb_at active (cur_thread s') s'; valid_fault ft'; invs s'; valid_irq_node s'; valid_etcbs s'; ekheap s' (cur_thread s') = Some etcb; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q26 s' obj obj' etcb) s
 4. \<And>s' obj obj' etcb s. \<lbrakk>cdl_current_thread (transform s') = Some obj; kheap s' (cur_thread s') = Some (TCB obj'); thread = cur_thread s'; not_idle_thread (cur_thread s') s'; st_tcb_at active (cur_thread s') s'; valid_fault ft'; invs s'; valid_irq_node s'; valid_etcbs s'; ekheap s' (cur_thread s') = Some etcb; s' = s\<rbrakk> \<Longrightarrow> (not_idle_thread (cur_thread s') and st_tcb_at active (cur_thread s') and valid_irq_node and invs and ko_at (TCB obj') (cur_thread s') and (\<lambda>s. ekheap s (cur_thread s') = Some etcb) and (\<lambda>s. not_idle_thread (cur_thread s) s) and (\<lambda>_. valid_fault ft') and valid_etcbs and ?Q'26 s' obj obj' etcb) s
 5. \<And>s s'. \<lbrakk>s = transform s'; True; cur_thread s' = thread \<and> not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_fault ft' \<and> invs s' \<and> valid_irq_node s' \<and> valid_etcbs s'; get_tcb thread s' \<noteq> None\<rbrakk> \<Longrightarrow> cdl_current_thread s \<noteq> None proof (prove)
goal (4 subgoals):
 1. \<And>s' obj obj' etcb. \<lbrakk>cdl_current_thread (transform s') = Some obj; kheap s' (cur_thread s') = Some (TCB obj'); thread = cur_thread s'; not_idle_thread (cur_thread s') s'; st_tcb_at active (cur_thread s') s'; valid_fault ft'; invs s'; valid_irq_node s'; valid_etcbs s'; ekheap s' (cur_thread s') = Some etcb\<rbrakk> \<Longrightarrow> \<lbrace>?Q'26 s' obj obj' etcb\<rbrace> Ipc_A.send_fault_ipc (cur_thread s') ft' \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>ft'. valid_mdb and not_idle_thread obj and valid_idle and valid_etcbs and (\<lambda>s. obj = cur_thread s')\<rbrace>
 2. \<And>s' obj obj' etcb s. \<lbrakk>cdl_current_thread (transform s') = Some obj; kheap s' (cur_thread s') = Some (TCB obj'); thread = cur_thread s'; not_idle_thread (cur_thread s') s'; st_tcb_at active (cur_thread s') s'; valid_fault ft'; invs s'; valid_irq_node s'; valid_etcbs s'; ekheap s' (cur_thread s') = Some etcb; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True)) s
 3. \<And>s' obj obj' etcb s. \<lbrakk>cdl_current_thread (transform s') = Some obj; kheap s' (cur_thread s') = Some (TCB obj'); thread = cur_thread s'; not_idle_thread (cur_thread s') s'; st_tcb_at active (cur_thread s') s'; valid_fault ft'; invs s'; valid_irq_node s'; valid_etcbs s'; ekheap s' (cur_thread s') = Some etcb; s' = s\<rbrakk> \<Longrightarrow> (not_idle_thread (cur_thread s') and st_tcb_at active (cur_thread s') and valid_irq_node and invs and ko_at (TCB obj') (cur_thread s') and (\<lambda>s. ekheap s (cur_thread s') = Some etcb) and (\<lambda>s. not_idle_thread (cur_thread s) s) and (\<lambda>_. valid_fault ft') and valid_etcbs and ?Q'26 s' obj obj' etcb) s
 4. \<And>s s'. \<lbrakk>s = transform s'; True; cur_thread s' = thread \<and> not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_fault ft' \<and> invs s' \<and> valid_irq_node s' \<and> valid_etcbs s'; get_tcb thread s' \<noteq> None\<rbrakk> \<Longrightarrow> cdl_current_thread s \<noteq> None proof (prove)
goal (4 subgoals):
 1. \<And>s' obj obj' etcb. \<lbrakk>cdl_current_thread (transform s') = Some obj; kheap s' (cur_thread s') = Some (TCB obj'); thread = cur_thread s'; cur_thread s' \<noteq> idle_thread s'; st_tcb_at active (cur_thread s') s'; valid_fault ft'; invs s'; valid_irq_node s'; valid_etcbs s'; ekheap s' (cur_thread s') = Some etcb\<rbrakk> \<Longrightarrow> \<lbrace>?Q'26 s' obj obj' etcb\<rbrace> doE handler_cptr <- liftE (thread_get tcb_fault_handler (cur_thread s'));
handler_cap <- cap_fault_on_failure (of_bl handler_cptr) False (CSpace_A.lookup_cap (cur_thread s') handler_cptr);
case handler_cap of cap.EndpointCap ref badge rights \<Rightarrow> if AllowSend \<in> rights \<and> (AllowGrant \<in> rights \<or> AllowGrantReply \<in> rights) then liftE $ do thread_set (tcb_fault_update (\<lambda>_. Some ft')) (cur_thread s');
Ipc_A.send_ipc True True (cap_ep_badge handler_cap) (AllowGrant \<in> rights) True (cur_thread s') (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>_ _. True\<rbrace>, \<lbrace>\<lambda>ft'. (\<lambda>a. valid_mdb a \<and> obj \<noteq> idle_thread a \<and> valid_idle a \<and> valid_etcbs a) and (\<lambda>s. obj = cur_thread s')\<rbrace>
 2. \<And>s' obj obj' etcb s. \<lbrakk>cdl_current_thread (transform s') = Some obj; kheap s' (cur_thread s') = Some (TCB obj'); thread = cur_thread s'; not_idle_thread (cur_thread s') s'; st_tcb_at active (cur_thread s') s'; valid_fault ft'; invs s'; valid_irq_node s'; valid_etcbs s'; ekheap s' (cur_thread s') = Some etcb; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True)) s
 3. \<And>s' obj obj' etcb s. \<lbrakk>cdl_current_thread (transform s') = Some obj; kheap s' (cur_thread s') = Some (TCB obj'); thread = cur_thread s'; not_idle_thread (cur_thread s') s'; st_tcb_at active (cur_thread s') s'; valid_fault ft'; invs s'; valid_irq_node s'; valid_etcbs s'; ekheap s' (cur_thread s') = Some etcb; s' = s\<rbrakk> \<Longrightarrow> (not_idle_thread (cur_thread s') and st_tcb_at active (cur_thread s') and valid_irq_node and invs and ko_at (TCB obj') (cur_thread s') and (\<lambda>s. ekheap s (cur_thread s') = Some etcb) and (\<lambda>s. not_idle_thread (cur_thread s) s) and (\<lambda>_. valid_fault ft') and valid_etcbs and ?Q'26 s' obj obj' etcb) s
 4. \<And>s s'. \<lbrakk>s = transform s'; True; cur_thread s' = thread \<and> not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_fault ft' \<and> invs s' \<and> valid_irq_node s' \<and> valid_etcbs s'; get_tcb thread s' \<noteq> None\<rbrakk> \<Longrightarrow> cdl_current_thread s \<noteq> None proof (prove)
goal (5 subgoals):
 1. \<And>s' obj obj' etcb handler_cptr. \<lbrakk>cdl_current_thread (transform s') = Some obj; kheap s' (cur_thread s') = Some (TCB obj'); thread = cur_thread s'; cur_thread s' \<noteq> idle_thread s'; st_tcb_at active (cur_thread s') s'; valid_fault ft'; invs s'; valid_irq_node s'; valid_etcbs s'; ekheap s' (cur_thread s') = Some etcb\<rbrakk> \<Longrightarrow> \<lbrace>?P'275 s' obj obj' etcb handler_cptr\<rbrace> CSpace_A.lookup_cap (cur_thread s') handler_cptr \<lbrace>\<lambda>rv s. (\<forall>x xa xb xc. rv = cap.UntypedCap x xa xb xc \<longrightarrow> valid_mdb s \<and> (obj \<noteq> idle_thread s \<and> valid_idle s \<and> valid_etcbs s) \<and> obj = cur_thread s' \<and> True) \<and> (\<forall>x xa xb. rv = cap.EndpointCap x xa xb \<longrightarrow> (AllowSend \<in> xb \<and> (AllowGrant \<in> xb \<or> AllowGrantReply \<in> xb) \<longrightarrow> True \<and> True \<and> True \<and> True) \<and> (\<not> (AllowSend \<in> xb \<and> (AllowGrant \<in> xb \<or> AllowGrantReply \<in> xb)) \<longrightarrow> valid_mdb s \<and> (obj \<noteq> idle_thread s \<and> valid_idle s \<and> valid_etcbs s) \<and> obj = cur_thread s' \<and> True)) \<and> (\<forall>x xa xb. rv = cap.NotificationCap x xa xb \<longrightarrow> valid_mdb s \<and> (obj \<noteq> idle_thread s \<and> valid_idle s \<and> valid_etcbs s) \<and> obj = cur_thread s' \<and> True) \<and> (\<forall>x xa xb. rv = cap.ReplyCap x xa xb \<longrightarrow> valid_mdb s \<and> (obj \<noteq> idle_thread s \<and> valid_idle s \<and> valid_etcbs s) \<and> obj = cur_thread s' \<and> True) \<and> (\<forall>x xa xb. rv = cap.CNodeCap x xa xb \<longrightarrow> valid_mdb s \<and> (obj \<noteq> idle_thread s \<and> valid_idle s \<and> valid_etcbs s) \<and> obj = cur_thread s' \<and> True) \<and> (\<forall>x. rv = ThreadCap x \<longrightarrow> valid_mdb s \<and> (obj \<noteq> idle_thread s \<and> valid_idle s \<and> valid_etcbs s) \<and> obj = cur_thread s' \<and> True) \<and> (rv = cap.DomainCap \<longrightarrow> valid_mdb s \<and> (obj \<noteq> idle_thread s \<and> valid_idle s \<and> valid_etcbs s) \<and> obj = cur_thread s' \<and> True) \<and> (rv = IRQControlCap \<longrightarrow> valid_mdb s \<and> (obj \<noteq> idle_thread s \<and> valid_idle s \<and> valid_etcbs s) \<and> obj = cur_thread s' \<and> True) \<and> (\<forall>x. rv = IRQHandlerCap x \<longrightarrow> valid_mdb s \<and> (obj \<noteq> idle_thread s \<and> valid_idle s \<and> valid_etcbs s) \<and> obj = cur_thread s' \<and> True) \<and> (\<forall>x xa xb. rv = Zombie x xa xb \<longrightarrow> valid_mdb s \<and> (obj \<noteq> idle_thread s \<and> valid_idle s \<and> valid_etcbs s) \<and> obj = cur_thread s' \<and> True) \<and> (\<forall>x. rv = ArchObjectCap x \<longrightarrow> valid_mdb s \<and> (obj \<noteq> idle_thread s \<and> valid_idle s \<and> valid_etcbs s) \<and> obj = cur_thread s' \<and> True)\<rbrace>, -
 2. \<And>s' obj obj' etcb. \<lbrakk>cdl_current_thread (transform s') = Some obj; kheap s' (cur_thread s') = Some (TCB obj'); thread = cur_thread s'; cur_thread s' \<noteq> idle_thread s'; st_tcb_at active (cur_thread s') s'; valid_fault ft'; invs s'; valid_irq_node s'; valid_etcbs s'; ekheap s' (cur_thread s') = Some etcb\<rbrakk> \<Longrightarrow> \<lbrace>?Q'26 s' obj obj' etcb\<rbrace> liftE (thread_get tcb_fault_handler (cur_thread s')) \<lbrace>\<lambda>handler_cptr s. valid_mdb s \<and> (obj \<noteq> idle_thread s \<and> valid_idle s \<and> valid_etcbs s) \<and> obj = cur_thread s' \<and> (valid_mdb s \<and> (obj \<noteq> idle_thread s \<and> valid_idle s \<and> valid_etcbs s) \<and> obj = cur_thread s' \<and> True) \<and> ?P'275 s' obj obj' etcb handler_cptr s\<rbrace>, \<lbrace>\<lambda>ft' s. valid_mdb s \<and> (obj \<noteq> idle_thread s \<and> valid_idle s \<and> valid_etcbs s) \<and> obj = cur_thread s'\<rbrace>
 3. \<And>s' obj obj' etcb s. \<lbrakk>cdl_current_thread (transform s') = Some obj; kheap s' (cur_thread s') = Some (TCB obj'); thread = cur_thread s'; not_idle_thread (cur_thread s') s'; st_tcb_at active (cur_thread s') s'; valid_fault ft'; invs s'; valid_irq_node s'; valid_etcbs s'; ekheap s' (cur_thread s') = Some etcb; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True)) s
 4. \<And>s' obj obj' etcb s. \<lbrakk>cdl_current_thread (transform s') = Some obj; kheap s' (cur_thread s') = Some (TCB obj'); thread = cur_thread s'; not_idle_thread (cur_thread s') s'; st_tcb_at active (cur_thread s') s'; valid_fault ft'; invs s'; valid_irq_node s'; valid_etcbs s'; ekheap s' (cur_thread s') = Some etcb; s' = s\<rbrakk> \<Longrightarrow> (not_idle_thread (cur_thread s') and st_tcb_at active (cur_thread s') and valid_irq_node and invs and ko_at (TCB obj') (cur_thread s') and (\<lambda>s. ekheap s (cur_thread s') = Some etcb) and (\<lambda>s. not_idle_thread (cur_thread s) s) and (\<lambda>_. valid_fault ft') and valid_etcbs and ?Q'26 s' obj obj' etcb) s
 5. \<And>s s'. \<lbrakk>s = transform s'; True; cur_thread s' = thread \<and> not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_fault ft' \<and> invs s' \<and> valid_irq_node s' \<and> valid_etcbs s'; get_tcb thread s' \<noteq> None\<rbrakk> \<Longrightarrow> cdl_current_thread s \<noteq> None proof (prove)
goal (6 subgoals):
 1. \<And>s' obj obj' etcb handler_cptr. \<lbrakk>cdl_current_thread (transform s') = Some obj; kheap s' (cur_thread s') = Some (TCB obj'); thread = cur_thread s'; cur_thread s' \<noteq> idle_thread s'; st_tcb_at active (cur_thread s') s'; valid_fault ft'; invs s'; valid_irq_node s'; valid_etcbs s'; ekheap s' (cur_thread s') = Some etcb\<rbrakk> \<Longrightarrow> \<lbrace>?P'275 s' obj obj' etcb handler_cptr\<rbrace> CSpace_A.lookup_cap (cur_thread s') handler_cptr \<lbrace>\<lambda>r s. invs s \<and> valid_etcbs s \<and> obj \<noteq> idle_thread s \<and> obj = cur_thread s'\<rbrace>, -
 2. \<And>s' obj obj' etcb handler_cptr rv s. \<lbrakk>cdl_current_thread (transform s') = Some obj; kheap s' (cur_thread s') = Some (TCB obj'); thread = cur_thread s'; cur_thread s' \<noteq> idle_thread s'; st_tcb_at active (cur_thread s') s'; valid_fault ft'; invs s'; valid_irq_node s'; valid_etcbs s'; ekheap s' (cur_thread s') = Some etcb; invs s \<and> valid_etcbs s \<and> obj \<noteq> idle_thread s \<and> obj = cur_thread s'\<rbrakk> \<Longrightarrow> (\<forall>x xa xb xc. rv = cap.UntypedCap x xa xb xc \<longrightarrow> valid_mdb s \<and> (obj \<noteq> idle_thread s \<and> valid_idle s \<and> valid_etcbs s) \<and> obj = cur_thread s' \<and> True) \<and> (\<forall>x xa xb. rv = cap.EndpointCap x xa xb \<longrightarrow> (AllowSend \<in> xb \<and> (AllowGrant \<in> xb \<or> AllowGrantReply \<in> xb) \<longrightarrow> True \<and> True \<and> True \<and> True) \<and> (\<not> (AllowSend \<in> xb \<and> (AllowGrant \<in> xb \<or> AllowGrantReply \<in> xb)) \<longrightarrow> valid_mdb s \<and> (obj \<noteq> idle_thread s \<and> valid_idle s \<and> valid_etcbs s) \<and> obj = cur_thread s' \<and> True)) \<and> (\<forall>x xa xb. rv = cap.NotificationCap x xa xb \<longrightarrow> valid_mdb s \<and> (obj \<noteq> idle_thread s \<and> valid_idle s \<and> valid_etcbs s) \<and> obj = cur_thread s' \<and> True) \<and> (\<forall>x xa xb. rv = cap.ReplyCap x xa xb \<longrightarrow> valid_mdb s \<and> (obj \<noteq> idle_thread s \<and> valid_idle s \<and> valid_etcbs s) \<and> obj = cur_thread s' \<and> True) \<and> (\<forall>x xa xb. rv = cap.CNodeCap x xa xb \<longrightarrow> valid_mdb s \<and> (obj \<noteq> idle_thread s \<and> valid_idle s \<and> valid_etcbs s) \<and> obj = cur_thread s' \<and> True) \<and> (\<forall>x. rv = ThreadCap x \<longrightarrow> valid_mdb s \<and> (obj \<noteq> idle_thread s \<and> valid_idle s \<and> valid_etcbs s) \<and> obj = cur_thread s' \<and> True) \<and> (rv = cap.DomainCap \<longrightarrow> valid_mdb s \<and> (obj \<noteq> idle_thread s \<and> valid_idle s \<and> valid_etcbs s) \<and> obj = cur_thread s' \<and> True) \<and> (rv = IRQControlCap \<longrightarrow> valid_mdb s \<and> (obj \<noteq> idle_thread s \<and> valid_idle s \<and> valid_etcbs s) \<and> obj = cur_thread s' \<and> True) \<and> (\<forall>x. rv = IRQHandlerCap x \<longrightarrow> valid_mdb s \<and> (obj \<noteq> idle_thread s \<and> valid_idle s \<and> valid_etcbs s) \<and> obj = cur_thread s' \<and> True) \<and> (\<forall>x xa xb. rv = Zombie x xa xb \<longrightarrow> valid_mdb s \<and> (obj \<noteq> idle_thread s \<and> valid_idle s \<and> valid_etcbs s) \<and> obj = cur_thread s' \<and> True) \<and> (\<forall>x. rv = ArchObjectCap x \<longrightarrow> valid_mdb s \<and> (obj \<noteq> idle_thread s \<and> valid_idle s \<and> valid_etcbs s) \<and> obj = cur_thread s' \<and> True)
 3. \<And>s' obj obj' etcb. \<lbrakk>cdl_current_thread (transform s') = Some obj; kheap s' (cur_thread s') = Some (TCB obj'); thread = cur_thread s'; cur_thread s' \<noteq> idle_thread s'; st_tcb_at active (cur_thread s') s'; valid_fault ft'; invs s'; valid_irq_node s'; valid_etcbs s'; ekheap s' (cur_thread s') = Some etcb\<rbrakk> \<Longrightarrow> \<lbrace>?Q'26 s' obj obj' etcb\<rbrace> liftE (thread_get tcb_fault_handler (cur_thread s')) \<lbrace>\<lambda>handler_cptr s. valid_mdb s \<and> (obj \<noteq> idle_thread s \<and> valid_idle s \<and> valid_etcbs s) \<and> obj = cur_thread s' \<and> (valid_mdb s \<and> (obj \<noteq> idle_thread s \<and> valid_idle s \<and> valid_etcbs s) \<and> obj = cur_thread s' \<and> True) \<and> ?P'275 s' obj obj' etcb handler_cptr s\<rbrace>, \<lbrace>\<lambda>ft' s. valid_mdb s \<and> (obj \<noteq> idle_thread s \<and> valid_idle s \<and> valid_etcbs s) \<and> obj = cur_thread s'\<rbrace>
 4. \<And>s' obj obj' etcb s. \<lbrakk>cdl_current_thread (transform s') = Some obj; kheap s' (cur_thread s') = Some (TCB obj'); thread = cur_thread s'; not_idle_thread (cur_thread s') s'; st_tcb_at active (cur_thread s') s'; valid_fault ft'; invs s'; valid_irq_node s'; valid_etcbs s'; ekheap s' (cur_thread s') = Some etcb; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True)) s
 5. \<And>s' obj obj' etcb s. \<lbrakk>cdl_current_thread (transform s') = Some obj; kheap s' (cur_thread s') = Some (TCB obj'); thread = cur_thread s'; not_idle_thread (cur_thread s') s'; st_tcb_at active (cur_thread s') s'; valid_fault ft'; invs s'; valid_irq_node s'; valid_etcbs s'; ekheap s' (cur_thread s') = Some etcb; s' = s\<rbrakk> \<Longrightarrow> (not_idle_thread (cur_thread s') and st_tcb_at active (cur_thread s') and valid_irq_node and invs and ko_at (TCB obj') (cur_thread s') and (\<lambda>s. ekheap s (cur_thread s') = Some etcb) and (\<lambda>s. not_idle_thread (cur_thread s) s) and (\<lambda>_. valid_fault ft') and valid_etcbs and ?Q'26 s' obj obj' etcb) s
 6. \<And>s s'. \<lbrakk>s = transform s'; True; cur_thread s' = thread \<and> not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_fault ft' \<and> invs s' \<and> valid_irq_node s' \<and> valid_etcbs s'; get_tcb thread s' \<noteq> None\<rbrakk> \<Longrightarrow> cdl_current_thread s \<noteq> None proof (prove)
goal (5 subgoals):
 1. \<And>s' obj obj' etcb handler_cptr rv s. \<lbrakk>cdl_current_thread (transform s') = Some obj; kheap s' (cur_thread s') = Some (TCB obj'); thread = cur_thread s'; cur_thread s' \<noteq> idle_thread s'; st_tcb_at active (cur_thread s') s'; valid_fault ft'; invs s'; valid_irq_node s'; valid_etcbs s'; ekheap s' (cur_thread s') = Some etcb; invs s \<and> valid_etcbs s \<and> obj \<noteq> idle_thread s \<and> obj = cur_thread s'\<rbrakk> \<Longrightarrow> (\<forall>x xa xb xc. rv = cap.UntypedCap x xa xb xc \<longrightarrow> valid_mdb s \<and> (obj \<noteq> idle_thread s \<and> valid_idle s \<and> valid_etcbs s) \<and> obj = cur_thread s' \<and> True) \<and> (\<forall>x xa xb. rv = cap.EndpointCap x xa xb \<longrightarrow> (AllowSend \<in> xb \<and> (AllowGrant \<in> xb \<or> AllowGrantReply \<in> xb) \<longrightarrow> True \<and> True \<and> True \<and> True) \<and> (\<not> (AllowSend \<in> xb \<and> (AllowGrant \<in> xb \<or> AllowGrantReply \<in> xb)) \<longrightarrow> valid_mdb s \<and> (obj \<noteq> idle_thread s \<and> valid_idle s \<and> valid_etcbs s) \<and> obj = cur_thread s' \<and> True)) \<and> (\<forall>x xa xb. rv = cap.NotificationCap x xa xb \<longrightarrow> valid_mdb s \<and> (obj \<noteq> idle_thread s \<and> valid_idle s \<and> valid_etcbs s) \<and> obj = cur_thread s' \<and> True) \<and> (\<forall>x xa xb. rv = cap.ReplyCap x xa xb \<longrightarrow> valid_mdb s \<and> (obj \<noteq> idle_thread s \<and> valid_idle s \<and> valid_etcbs s) \<and> obj = cur_thread s' \<and> True) \<and> (\<forall>x xa xb. rv = cap.CNodeCap x xa xb \<longrightarrow> valid_mdb s \<and> (obj \<noteq> idle_thread s \<and> valid_idle s \<and> valid_etcbs s) \<and> obj = cur_thread s' \<and> True) \<and> (\<forall>x. rv = ThreadCap x \<longrightarrow> valid_mdb s \<and> (obj \<noteq> idle_thread s \<and> valid_idle s \<and> valid_etcbs s) \<and> obj = cur_thread s' \<and> True) \<and> (rv = cap.DomainCap \<longrightarrow> valid_mdb s \<and> (obj \<noteq> idle_thread s \<and> valid_idle s \<and> valid_etcbs s) \<and> obj = cur_thread s' \<and> True) \<and> (rv = IRQControlCap \<longrightarrow> valid_mdb s \<and> (obj \<noteq> idle_thread s \<and> valid_idle s \<and> valid_etcbs s) \<and> obj = cur_thread s' \<and> True) \<and> (\<forall>x. rv = IRQHandlerCap x \<longrightarrow> valid_mdb s \<and> (obj \<noteq> idle_thread s \<and> valid_idle s \<and> valid_etcbs s) \<and> obj = cur_thread s' \<and> True) \<and> (\<forall>x xa xb. rv = Zombie x xa xb \<longrightarrow> valid_mdb s \<and> (obj \<noteq> idle_thread s \<and> valid_idle s \<and> valid_etcbs s) \<and> obj = cur_thread s' \<and> True) \<and> (\<forall>x. rv = ArchObjectCap x \<longrightarrow> valid_mdb s \<and> (obj \<noteq> idle_thread s \<and> valid_idle s \<and> valid_etcbs s) \<and> obj = cur_thread s' \<and> True)
 2. \<And>s' obj obj' etcb. \<lbrakk>cdl_current_thread (transform s') = Some obj; kheap s' (cur_thread s') = Some (TCB obj'); thread = cur_thread s'; cur_thread s' \<noteq> idle_thread s'; st_tcb_at active (cur_thread s') s'; valid_fault ft'; invs s'; valid_irq_node s'; valid_etcbs s'; ekheap s' (cur_thread s') = Some etcb\<rbrakk> \<Longrightarrow> \<lbrace>?Q'26 s' obj obj' etcb\<rbrace> liftE (thread_get tcb_fault_handler (cur_thread s')) \<lbrace>\<lambda>handler_cptr s. valid_mdb s \<and> (obj \<noteq> idle_thread s \<and> valid_idle s \<and> valid_etcbs s) \<and> obj = cur_thread s' \<and> (valid_mdb s \<and> (obj \<noteq> idle_thread s \<and> valid_idle s \<and> valid_etcbs s) \<and> obj = cur_thread s' \<and> True) \<and> invs s \<and> valid_etcbs s \<and> obj \<noteq> idle_thread s \<and> obj = cur_thread s'\<rbrace>, \<lbrace>\<lambda>ft' s. valid_mdb s \<and> (obj \<noteq> idle_thread s \<and> valid_idle s \<and> valid_etcbs s) \<and> obj = cur_thread s'\<rbrace>
 3. \<And>s' obj obj' etcb s. \<lbrakk>cdl_current_thread (transform s') = Some obj; kheap s' (cur_thread s') = Some (TCB obj'); thread = cur_thread s'; not_idle_thread (cur_thread s') s'; st_tcb_at active (cur_thread s') s'; valid_fault ft'; invs s'; valid_irq_node s'; valid_etcbs s'; ekheap s' (cur_thread s') = Some etcb; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True)) s
 4. \<And>s' obj obj' etcb s. \<lbrakk>cdl_current_thread (transform s') = Some obj; kheap s' (cur_thread s') = Some (TCB obj'); thread = cur_thread s'; not_idle_thread (cur_thread s') s'; st_tcb_at active (cur_thread s') s'; valid_fault ft'; invs s'; valid_irq_node s'; valid_etcbs s'; ekheap s' (cur_thread s') = Some etcb; s' = s\<rbrakk> \<Longrightarrow> (not_idle_thread (cur_thread s') and st_tcb_at active (cur_thread s') and valid_irq_node and invs and ko_at (TCB obj') (cur_thread s') and (\<lambda>s. ekheap s (cur_thread s') = Some etcb) and (\<lambda>s. not_idle_thread (cur_thread s) s) and (\<lambda>_. valid_fault ft') and valid_etcbs and ?Q'26 s' obj obj' etcb) s
 5. \<And>s s'. \<lbrakk>s = transform s'; True; cur_thread s' = thread \<and> not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_fault ft' \<and> invs s' \<and> valid_irq_node s' \<and> valid_etcbs s'; get_tcb thread s' \<noteq> None\<rbrakk> \<Longrightarrow> cdl_current_thread s \<noteq> None proof (prove)
goal (4 subgoals):
 1. \<And>s' obj obj' etcb. \<lbrakk>cdl_current_thread (transform s') = Some obj; kheap s' (cur_thread s') = Some (TCB obj'); thread = cur_thread s'; cur_thread s' \<noteq> idle_thread s'; st_tcb_at active (cur_thread s') s'; valid_fault ft'; invs s'; valid_irq_node s'; valid_etcbs s'; ekheap s' (cur_thread s') = Some etcb\<rbrakk> \<Longrightarrow> \<lbrace>?Q'26 s' obj obj' etcb\<rbrace> liftE (thread_get tcb_fault_handler (cur_thread s')) \<lbrace>\<lambda>handler_cptr s. valid_mdb s \<and> (obj \<noteq> idle_thread s \<and> valid_idle s \<and> valid_etcbs s) \<and> obj = cur_thread s' \<and> (valid_mdb s \<and> (obj \<noteq> idle_thread s \<and> valid_idle s \<and> valid_etcbs s) \<and> obj = cur_thread s' \<and> True) \<and> invs s \<and> valid_etcbs s \<and> obj \<noteq> idle_thread s \<and> obj = cur_thread s'\<rbrace>, \<lbrace>\<lambda>ft' s. valid_mdb s \<and> (obj \<noteq> idle_thread s \<and> valid_idle s \<and> valid_etcbs s) \<and> obj = cur_thread s'\<rbrace>
 2. \<And>s' obj obj' etcb s. \<lbrakk>cdl_current_thread (transform s') = Some obj; kheap s' (cur_thread s') = Some (TCB obj'); thread = cur_thread s'; not_idle_thread (cur_thread s') s'; st_tcb_at active (cur_thread s') s'; valid_fault ft'; invs s'; valid_irq_node s'; valid_etcbs s'; ekheap s' (cur_thread s') = Some etcb; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True)) s
 3. \<And>s' obj obj' etcb s. \<lbrakk>cdl_current_thread (transform s') = Some obj; kheap s' (cur_thread s') = Some (TCB obj'); thread = cur_thread s'; not_idle_thread (cur_thread s') s'; st_tcb_at active (cur_thread s') s'; valid_fault ft'; invs s'; valid_irq_node s'; valid_etcbs s'; ekheap s' (cur_thread s') = Some etcb; s' = s\<rbrakk> \<Longrightarrow> (not_idle_thread (cur_thread s') and st_tcb_at active (cur_thread s') and valid_irq_node and invs and ko_at (TCB obj') (cur_thread s') and (\<lambda>s. ekheap s (cur_thread s') = Some etcb) and (\<lambda>s. not_idle_thread (cur_thread s) s) and (\<lambda>_. valid_fault ft') and valid_etcbs and ?Q'26 s' obj obj' etcb) s
 4. \<And>s s'. \<lbrakk>s = transform s'; True; cur_thread s' = thread \<and> not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_fault ft' \<and> invs s' \<and> valid_irq_node s' \<and> valid_etcbs s'; get_tcb thread s' \<noteq> None\<rbrakk> \<Longrightarrow> cdl_current_thread s \<noteq> None proof (prove)
goal (3 subgoals):
 1. \<And>s' obj obj' etcb s. \<lbrakk>cdl_current_thread (transform s') = Some obj; kheap s' (cur_thread s') = Some (TCB obj'); thread = cur_thread s'; not_idle_thread (cur_thread s') s'; st_tcb_at active (cur_thread s') s'; valid_fault ft'; invs s'; valid_irq_node s'; valid_etcbs s'; ekheap s' (cur_thread s') = Some etcb; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True)) s
 2. \<And>s' obj obj' etcb s. \<lbrakk>cdl_current_thread (transform s') = Some obj; kheap s' (cur_thread s') = Some (TCB obj'); thread = cur_thread s'; not_idle_thread (cur_thread s') s'; st_tcb_at active (cur_thread s') s'; valid_fault ft'; invs s'; valid_irq_node s'; valid_etcbs s'; ekheap s' (cur_thread s') = Some etcb; s' = s\<rbrakk> \<Longrightarrow> (not_idle_thread (cur_thread s') and st_tcb_at active (cur_thread s') and valid_irq_node and invs and ko_at (TCB obj') (cur_thread s') and (\<lambda>s. ekheap s (cur_thread s') = Some etcb) and (\<lambda>s. not_idle_thread (cur_thread s) s) and (\<lambda>_. valid_fault ft') and valid_etcbs and (\<lambda>s. valid_mdb s \<and> (obj \<noteq> idle_thread s \<and> valid_idle s \<and> valid_etcbs s) \<and> obj = cur_thread s' \<and> (valid_mdb s \<and> (obj \<noteq> idle_thread s \<and> valid_idle s \<and> valid_etcbs s) \<and> obj = cur_thread s' \<and> True) \<and> invs s \<and> valid_etcbs s \<and> obj \<noteq> idle_thread s \<and> obj = cur_thread s')) s
 3. \<And>s s'. \<lbrakk>s = transform s'; True; cur_thread s' = thread \<and> not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_fault ft' \<and> invs s' \<and> valid_irq_node s' \<and> valid_etcbs s'; get_tcb thread s' \<noteq> None\<rbrakk> \<Longrightarrow> cdl_current_thread s \<noteq> None proof (prove)
goal (2 subgoals):
 1. \<And>s' obj obj' etcb s. \<lbrakk>cdl_current_thread (transform s') = Some obj; kheap s' (cur_thread s') = Some (TCB obj'); thread = cur_thread s'; not_idle_thread (cur_thread s') s'; st_tcb_at active (cur_thread s') s'; valid_fault ft'; invs s'; valid_irq_node s'; valid_etcbs s'; ekheap s' (cur_thread s') = Some etcb; s' = s\<rbrakk> \<Longrightarrow> (not_idle_thread (cur_thread s') and st_tcb_at active (cur_thread s') and valid_irq_node and invs and ko_at (TCB obj') (cur_thread s') and (\<lambda>s. ekheap s (cur_thread s') = Some etcb) and (\<lambda>s. not_idle_thread (cur_thread s) s) and (\<lambda>_. valid_fault ft') and valid_etcbs and (\<lambda>s. valid_mdb s \<and> (obj \<noteq> idle_thread s \<and> valid_idle s \<and> valid_etcbs s) \<and> obj = cur_thread s' \<and> (valid_mdb s \<and> (obj \<noteq> idle_thread s \<and> valid_idle s \<and> valid_etcbs s) \<and> obj = cur_thread s' \<and> True) \<and> invs s \<and> valid_etcbs s \<and> obj \<noteq> idle_thread s \<and> obj = cur_thread s')) s
 2. \<And>s s'. \<lbrakk>s = transform s'; True; cur_thread s' = thread \<and> not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_fault ft' \<and> invs s' \<and> valid_irq_node s' \<and> valid_etcbs s'; get_tcb thread s' \<noteq> None\<rbrakk> \<Longrightarrow> cdl_current_thread s \<noteq> None proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>s = transform s'; True; cur_thread s' = thread \<and> not_idle_thread thread s' \<and> st_tcb_at active thread s' \<and> valid_fault ft' \<and> invs s' \<and> valid_irq_node s' \<and> valid_etcbs s'; get_tcb thread s' \<noteq> None\<rbrakk> \<Longrightarrow> cdl_current_thread s \<noteq> None proof (prove)
goal (1 subgoal):
 1. \<And>s' y. \<lbrakk>thread = cur_thread s'; cur_thread s' \<noteq> idle_thread s'; valid_fault ft'; kheap s' (cur_thread s') = Some (TCB y); invs s'; active (tcb_state y); valid_irq_node s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> \<exists>y. cdl_current_thread (transform s') = Some y proof (prove)
goal:
No subgoals!