theory Tcb_R

lemma decodeTCBInvocation_corres:
 "\<lbrakk> c = Structures_A.ThreadCap t; cap_relation c c';
      list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) extras extras';
      length args < 2 ^ word_bits \<rbrakk> \<Longrightarrow>
  corres (ser \<oplus> tcbinv_relation) (einvs and tcb_at t and (\<lambda>s. \<forall>x \<in> set extras. s \<turnstile> fst x \<and> cte_at (snd x) s))
                                 (invs' and tcb_at' t and (\<lambda>s. \<forall>x \<in> set extras'. s \<turnstile>' fst x \<and> cte_at' (snd x) s))
         (decode_tcb_invocation label args c slot extras)
         (decodeTCBInvocation label args c' (cte_map slot) extras')" apply (rule_tac F="cap_aligned c \<and> capAligned c'" in corres_req) apply (clarsimp simp: cap_aligned_def capAligned_def objBits_simps word_bits_def) apply (drule obj_at_aligned', simp_all add: objBits_simps') apply (clarsimp simp: decode_tcb_invocation_def
                        decodeTCBInvocation_def
             split del: if_split split: gen_invocation_labels.split) apply (simp add: returnOk_def) apply (intro conjI impI
             corres_guard_imp[OF decodeReadRegisters_corres]
             corres_guard_imp[OF decodeWriteRegisters_corres]
             corres_guard_imp[OF decodeCopyRegisters_corres]
             corres_guard_imp[OF decodeTCBConfigure_corres]
             corres_guard_imp[OF decodeSetPriority_corres]
             corres_guard_imp[OF decodeSetMCPriority_corres]
             corres_guard_imp[OF decodeSetSchedParams_corres]
             corres_guard_imp[OF decodeSetIPCBuffer_corres]
             corres_guard_imp[OF decodeSetSpace_corres]
             corres_guard_imp[OF decodeBindNotification_corres]
             corres_guard_imp[OF decodeUnbindNotification_corres]
             corres_guard_imp[OF decodeSetTLSBase_corres],
         simp_all add: valid_cap_simps valid_cap_simps' invs_def valid_sched_def) apply (auto simp: list_all2_map1 list_all2_map2
             elim!: list_all2_mono) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c = cap.ThreadCap t; cap_relation c c'; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) extras extras'; length args < 2 ^ word_bits\<rbrakk> \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (einvs and tcb_at t and (\<lambda>s. \<forall>x\<in>set extras. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>_. True) (snd x) s)) (invs' and tcb_at' t and (\<lambda>s. \<forall>x\<in>set extras'. valid_cap' (fst x) s \<and> cte_wp_at' (\<lambda>_. True) (snd x) s)) (decode_tcb_invocation label args c slot extras) (decodeTCBInvocation label args c' (cte_map slot) extras') proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>c = cap.ThreadCap t; cap_relation c c'; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) extras extras'; length args < 2 ^ word_bits; (s, s') \<in> state_relation; (einvs and tcb_at t and (\<lambda>s. \<forall>x\<in>set extras. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>_. True) (snd x) s)) s; (invs' and tcb_at' t and (\<lambda>s. \<forall>x\<in>set extras'. valid_cap' (fst x) s \<and> cte_wp_at' (\<lambda>_. True) (snd x) s)) s'\<rbrakk> \<Longrightarrow> cap_aligned c \<and> capAligned c'
 2. \<lbrakk>c = cap.ThreadCap t; cap_relation c c'; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) extras extras'; length args < 2 ^ word_bits; cap_aligned c \<and> capAligned c'\<rbrakk> \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (einvs and tcb_at t and (\<lambda>s. \<forall>x\<in>set extras. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>_. True) (snd x) s)) (invs' and tcb_at' t and (\<lambda>s. \<forall>x\<in>set extras'. valid_cap' (fst x) s \<and> cte_wp_at' (\<lambda>_. True) (snd x) s)) (decode_tcb_invocation label args c slot extras) (decodeTCBInvocation label args c' (cte_map slot) extras') proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>c = cap.ThreadCap t; c' = capability.ThreadCap t; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) extras extras'; length args < 4294967296; (s, s') \<in> state_relation; invs s; invs' s'; valid_list s; tcb_at' t s'; \<forall>x\<in>set extras'. valid_cap' (fst x) s' \<and> cte_wp_at' (\<lambda>_. True) (snd x) s'; valid_sched s; tcb_at t s; \<forall>x\<in>set extras. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>_. True) (snd x) s\<rbrakk> \<Longrightarrow> is_aligned t 9 \<and> is_aligned t tcbBlockSizeBits \<and> tcbBlockSizeBits < 32
 2. \<lbrakk>c = cap.ThreadCap t; cap_relation c c'; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) extras extras'; length args < 2 ^ word_bits; cap_aligned c \<and> capAligned c'\<rbrakk> \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (einvs and tcb_at t and (\<lambda>s. \<forall>x\<in>set extras. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>_. True) (snd x) s)) (invs' and tcb_at' t and (\<lambda>s. \<forall>x\<in>set extras'. valid_cap' (fst x) s \<and> cte_wp_at' (\<lambda>_. True) (snd x) s)) (decode_tcb_invocation label args c slot extras) (decodeTCBInvocation label args c' (cte_map slot) extras') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c = cap.ThreadCap t; c' = capability.ThreadCap t; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) extras extras'; length args < 2 ^ word_bits; cap_aligned (cap.ThreadCap t) \<and> capAligned (capability.ThreadCap t)\<rbrakk> \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (einvs and tcb_at t and (\<lambda>s. \<forall>x\<in>set extras. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>_. True) (snd x) s)) (invs' and tcb_at' t and (\<lambda>s. \<forall>x\<in>set extras'. valid_cap' (fst x) s \<and> cte_wp_at' (\<lambda>_. True) (snd x) s)) (decode_tcb_invocation label args (cap.ThreadCap t) slot extras) (decodeTCBInvocation label args (capability.ThreadCap t) (cte_map slot) extras') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c = cap.ThreadCap t; c' = capability.ThreadCap t; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) extras extras'; length args < 2 ^ word_bits; cap_aligned (cap.ThreadCap t); capAligned (capability.ThreadCap t)\<rbrakk> \<Longrightarrow> (gen_invocation_type label = TCBReadRegisters \<longrightarrow> corres (ser \<oplus> tcbinv_relation) (einvs and tcb_at t and (\<lambda>s. \<forall>x\<in>set extras. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>_. True) (snd x) s)) (invs' and tcb_at' t and (\<lambda>s. \<forall>x\<in>set extras'. valid_cap' (fst x) s \<and> cte_wp_at' (\<lambda>_. True) (snd x) s)) (decode_read_registers args (cap.ThreadCap t)) (decodeReadRegisters args (capability.ThreadCap t))) \<and> (gen_invocation_type label = TCBWriteRegisters \<longrightarrow> corres (ser \<oplus> tcbinv_relation) (einvs and tcb_at t and (\<lambda>s. \<forall>x\<in>set extras. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>_. True) (snd x) s)) (invs' and tcb_at' t and (\<lambda>s. \<forall>x\<in>set extras'. valid_cap' (fst x) s \<and> cte_wp_at' (\<lambda>_. True) (snd x) s)) (decode_write_registers args (cap.ThreadCap t)) (decodeWriteRegisters args (capability.ThreadCap t))) \<and> (gen_invocation_type label = TCBCopyRegisters \<longrightarrow> corres (ser \<oplus> tcbinv_relation) (einvs and tcb_at t and (\<lambda>s. \<forall>x\<in>set extras. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>_. True) (snd x) s)) (invs' and tcb_at' t and (\<lambda>s. \<forall>x\<in>set extras'. valid_cap' (fst x) s \<and> cte_wp_at' (\<lambda>_. True) (snd x) s)) (decode_copy_registers args (cap.ThreadCap t) (map fst extras)) (decodeCopyRegisters args (capability.ThreadCap t) (map fst extras'))) \<and> (gen_invocation_type label = TCBConfigure \<longrightarrow> corres (ser \<oplus> tcbinv_relation) (einvs and tcb_at t and (\<lambda>s. \<forall>x\<in>set extras. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>_. True) (snd x) s)) (invs' and tcb_at' t and (\<lambda>s. \<forall>x\<in>set extras'. valid_cap' (fst x) s \<and> cte_wp_at' (\<lambda>_. True) (snd x) s)) (decode_tcb_configure args (cap.ThreadCap t) slot extras) (decodeTCBConfigure args (capability.ThreadCap t) (cte_map slot) extras')) \<and> (gen_invocation_type label = TCBSetPriority \<longrightarrow> corres (ser \<oplus> tcbinv_relation) (einvs and tcb_at t and (\<lambda>s. \<forall>x\<in>set extras. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>_. True) (snd x) s)) (invs' and tcb_at' t and (\<lambda>s. \<forall>x\<in>set extras'. valid_cap' (fst x) s \<and> cte_wp_at' (\<lambda>_. True) (snd x) s)) (decode_set_priority args (cap.ThreadCap t) slot extras) (decodeSetPriority args (capability.ThreadCap t) extras')) \<and> (gen_invocation_type label = TCBSetMCPriority \<longrightarrow> corres (ser \<oplus> tcbinv_relation) (einvs and tcb_at t and (\<lambda>s. \<forall>x\<in>set extras. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>_. True) (snd x) s)) (invs' and tcb_at' t and (\<lambda>s. \<forall>x\<in>set extras'. valid_cap' (fst x) s \<and> cte_wp_at' (\<lambda>_. True) (snd x) s)) (decode_set_mcpriority args (cap.ThreadCap t) slot extras) (decodeSetMCPriority args (capability.ThreadCap t) extras')) \<and> (gen_invocation_type label = TCBSetSchedParams \<longrightarrow> corres (ser \<oplus> tcbinv_relation) (einvs and tcb_at t and (\<lambda>s. \<forall>x\<in>set extras. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>_. True) (snd x) s)) (invs' and tcb_at' t and (\<lambda>s. \<forall>x\<in>set extras'. valid_cap' (fst x) s \<and> cte_wp_at' (\<lambda>_. True) (snd x) s)) (decode_set_sched_params args (cap.ThreadCap t) slot extras) (decodeSetSchedParams args (capability.ThreadCap t) extras')) \<and> (gen_invocation_type label = TCBSetIPCBuffer \<longrightarrow> corres (ser \<oplus> tcbinv_relation) (einvs and tcb_at t and (\<lambda>s. \<forall>x\<in>set extras. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>_. True) (snd x) s)) (invs' and tcb_at' t and (\<lambda>s. \<forall>x\<in>set extras'. valid_cap' (fst x) s \<and> cte_wp_at' (\<lambda>_. True) (snd x) s)) (decode_set_ipc_buffer args (cap.ThreadCap t) slot extras) (decodeSetIPCBuffer args (capability.ThreadCap t) (cte_map slot) extras')) \<and> (gen_invocation_type label = TCBSetSpace \<longrightarrow> corres (ser \<oplus> tcbinv_relation) (einvs and tcb_at t and (\<lambda>s. \<forall>x\<in>set extras. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>_. True) (snd x) s)) (invs' and tcb_at' t and (\<lambda>s. \<forall>x\<in>set extras'. valid_cap' (fst x) s \<and> cte_wp_at' (\<lambda>_. True) (snd x) s)) (decode_set_space args (cap.ThreadCap t) slot extras) (decodeSetSpace args (capability.ThreadCap t) (cte_map slot) extras')) \<and> (gen_invocation_type label = TCBSuspend \<longrightarrow> corres (ser \<oplus> tcbinv_relation) (einvs and tcb_at t and (\<lambda>s. \<forall>x\<in>set extras. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>_. True) (snd x) s)) (invs' and tcb_at' t and (\<lambda>s. \<forall>x\<in>set extras'. valid_cap' (fst x) s \<and> cte_wp_at' (\<lambda>_. True) (snd x) s)) (returnOk (tcb_invocation.Suspend t)) (returnOk (tcbinvocation.Suspend t))) \<and> (gen_invocation_type label = TCBResume \<longrightarrow> corres (ser \<oplus> tcbinv_relation) (einvs and tcb_at t and (\<lambda>s. \<forall>x\<in>set extras. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>_. True) (snd x) s)) (invs' and tcb_at' t and (\<lambda>s. \<forall>x\<in>set extras'. valid_cap' (fst x) s \<and> cte_wp_at' (\<lambda>_. True) (snd x) s)) (returnOk (tcb_invocation.Resume t)) (returnOk (tcbinvocation.Resume t))) \<and> (gen_invocation_type label = TCBBindNotification \<longrightarrow> corres (ser \<oplus> tcbinv_relation) (einvs and tcb_at t and (\<lambda>s. \<forall>x\<in>set extras. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>_. True) (snd x) s)) (invs' and tcb_at' t and (\<lambda>s. \<forall>x\<in>set extras'. valid_cap' (fst x) s \<and> cte_wp_at' (\<lambda>_. True) (snd x) s)) (decode_bind_notification (cap.ThreadCap t) extras) (decodeBindNotification (capability.ThreadCap t) extras')) \<and> (gen_invocation_type label = TCBUnbindNotification \<longrightarrow> corres (ser \<oplus> tcbinv_relation) (einvs and tcb_at t and (\<lambda>s. \<forall>x\<in>set extras. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>_. True) (snd x) s)) (invs' and tcb_at' t and (\<lambda>s. \<forall>x\<in>set extras'. valid_cap' (fst x) s \<and> cte_wp_at' (\<lambda>_. True) (snd x) s)) (decode_unbind_notification (cap.ThreadCap t)) (decodeUnbindNotification (capability.ThreadCap t))) \<and> (gen_invocation_type label = TCBSetTLSBase \<longrightarrow> corres (ser \<oplus> tcbinv_relation) (einvs and tcb_at t and (\<lambda>s. \<forall>x\<in>set extras. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>_. True) (snd x) s)) (invs' and tcb_at' t and (\<lambda>s. \<forall>x\<in>set extras'. valid_cap' (fst x) s \<and> cte_wp_at' (\<lambda>_. True) (snd x) s)) (decode_set_tls_base args (cap.ThreadCap t)) (decodeSetTLSBase args (capability.ThreadCap t))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c = cap.ThreadCap t; c' = capability.ThreadCap t; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) extras extras'; length args < 2 ^ word_bits; cap_aligned (cap.ThreadCap t); capAligned (capability.ThreadCap t)\<rbrakk> \<Longrightarrow> (gen_invocation_type label = TCBReadRegisters \<longrightarrow> corres (ser \<oplus> tcbinv_relation) (einvs and tcb_at t and (\<lambda>s. \<forall>x\<in>set extras. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>_. True) (snd x) s)) (invs' and tcb_at' t and (\<lambda>s. \<forall>x\<in>set extras'. valid_cap' (fst x) s \<and> cte_wp_at' (\<lambda>_. True) (snd x) s)) (decode_read_registers args (cap.ThreadCap t)) (decodeReadRegisters args (capability.ThreadCap t))) \<and> (gen_invocation_type label = TCBWriteRegisters \<longrightarrow> corres (ser \<oplus> tcbinv_relation) (einvs and tcb_at t and (\<lambda>s. \<forall>x\<in>set extras. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>_. True) (snd x) s)) (invs' and tcb_at' t and (\<lambda>s. \<forall>x\<in>set extras'. valid_cap' (fst x) s \<and> cte_wp_at' (\<lambda>_. True) (snd x) s)) (decode_write_registers args (cap.ThreadCap t)) (decodeWriteRegisters args (capability.ThreadCap t))) \<and> (gen_invocation_type label = TCBCopyRegisters \<longrightarrow> corres (ser \<oplus> tcbinv_relation) (einvs and tcb_at t and (\<lambda>s. \<forall>x\<in>set extras. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>_. True) (snd x) s)) (invs' and tcb_at' t and (\<lambda>s. \<forall>x\<in>set extras'. valid_cap' (fst x) s \<and> cte_wp_at' (\<lambda>_. True) (snd x) s)) (decode_copy_registers args (cap.ThreadCap t) (map fst extras)) (decodeCopyRegisters args (capability.ThreadCap t) (map fst extras'))) \<and> (gen_invocation_type label = TCBConfigure \<longrightarrow> corres (ser \<oplus> tcbinv_relation) (einvs and tcb_at t and (\<lambda>s. \<forall>x\<in>set extras. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>_. True) (snd x) s)) (invs' and tcb_at' t and (\<lambda>s. \<forall>x\<in>set extras'. valid_cap' (fst x) s \<and> cte_wp_at' (\<lambda>_. True) (snd x) s)) (decode_tcb_configure args (cap.ThreadCap t) slot extras) (decodeTCBConfigure args (capability.ThreadCap t) (cte_map slot) extras')) \<and> (gen_invocation_type label = TCBSetPriority \<longrightarrow> corres (ser \<oplus> tcbinv_relation) (einvs and tcb_at t and (\<lambda>s. \<forall>x\<in>set extras. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>_. True) (snd x) s)) (invs' and tcb_at' t and (\<lambda>s. \<forall>x\<in>set extras'. valid_cap' (fst x) s \<and> cte_wp_at' (\<lambda>_. True) (snd x) s)) (decode_set_priority args (cap.ThreadCap t) slot extras) (decodeSetPriority args (capability.ThreadCap t) extras')) \<and> (gen_invocation_type label = TCBSetMCPriority \<longrightarrow> corres (ser \<oplus> tcbinv_relation) (einvs and tcb_at t and (\<lambda>s. \<forall>x\<in>set extras. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>_. True) (snd x) s)) (invs' and tcb_at' t and (\<lambda>s. \<forall>x\<in>set extras'. valid_cap' (fst x) s \<and> cte_wp_at' (\<lambda>_. True) (snd x) s)) (decode_set_mcpriority args (cap.ThreadCap t) slot extras) (decodeSetMCPriority args (capability.ThreadCap t) extras')) \<and> (gen_invocation_type label = TCBSetSchedParams \<longrightarrow> corres (ser \<oplus> tcbinv_relation) (einvs and tcb_at t and (\<lambda>s. \<forall>x\<in>set extras. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>_. True) (snd x) s)) (invs' and tcb_at' t and (\<lambda>s. \<forall>x\<in>set extras'. valid_cap' (fst x) s \<and> cte_wp_at' (\<lambda>_. True) (snd x) s)) (decode_set_sched_params args (cap.ThreadCap t) slot extras) (decodeSetSchedParams args (capability.ThreadCap t) extras')) \<and> (gen_invocation_type label = TCBSetIPCBuffer \<longrightarrow> corres (ser \<oplus> tcbinv_relation) (einvs and tcb_at t and (\<lambda>s. \<forall>x\<in>set extras. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>_. True) (snd x) s)) (invs' and tcb_at' t and (\<lambda>s. \<forall>x\<in>set extras'. valid_cap' (fst x) s \<and> cte_wp_at' (\<lambda>_. True) (snd x) s)) (decode_set_ipc_buffer args (cap.ThreadCap t) slot extras) (decodeSetIPCBuffer args (capability.ThreadCap t) (cte_map slot) extras')) \<and> (gen_invocation_type label = TCBSetSpace \<longrightarrow> corres (ser \<oplus> tcbinv_relation) (einvs and tcb_at t and (\<lambda>s. \<forall>x\<in>set extras. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>_. True) (snd x) s)) (invs' and tcb_at' t and (\<lambda>s. \<forall>x\<in>set extras'. valid_cap' (fst x) s \<and> cte_wp_at' (\<lambda>_. True) (snd x) s)) (decode_set_space args (cap.ThreadCap t) slot extras) (decodeSetSpace args (capability.ThreadCap t) (cte_map slot) extras')) \<and> (gen_invocation_type label = TCBBindNotification \<longrightarrow> corres (ser \<oplus> tcbinv_relation) (einvs and tcb_at t and (\<lambda>s. \<forall>x\<in>set extras. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>_. True) (snd x) s)) (invs' and tcb_at' t and (\<lambda>s. \<forall>x\<in>set extras'. valid_cap' (fst x) s \<and> cte_wp_at' (\<lambda>_. True) (snd x) s)) (decode_bind_notification (cap.ThreadCap t) extras) (decodeBindNotification (capability.ThreadCap t) extras')) \<and> (gen_invocation_type label = TCBUnbindNotification \<longrightarrow> corres (ser \<oplus> tcbinv_relation) (einvs and tcb_at t and (\<lambda>s. \<forall>x\<in>set extras. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>_. True) (snd x) s)) (invs' and tcb_at' t and (\<lambda>s. \<forall>x\<in>set extras'. valid_cap' (fst x) s \<and> cte_wp_at' (\<lambda>_. True) (snd x) s)) (decode_unbind_notification (cap.ThreadCap t)) (decodeUnbindNotification (capability.ThreadCap t))) \<and> (gen_invocation_type label = TCBSetTLSBase \<longrightarrow> corres (ser \<oplus> tcbinv_relation) (einvs and tcb_at t and (\<lambda>s. \<forall>x\<in>set extras. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>_. True) (snd x) s)) (invs' and tcb_at' t and (\<lambda>s. \<forall>x\<in>set extras'. valid_cap' (fst x) s \<and> cte_wp_at' (\<lambda>_. True) (snd x) s)) (decode_set_tls_base args (cap.ThreadCap t)) (decodeSetTLSBase args (capability.ThreadCap t))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>c = cap.ThreadCap t; c' = capability.ThreadCap t; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) extras extras'; length args < 2 ^ word_bits; cap_aligned (cap.ThreadCap t); capAligned (capability.ThreadCap t); gen_invocation_type label = TCBCopyRegisters\<rbrakk> \<Longrightarrow> list_all2 cap_relation (map fst extras) (map fst extras')
 2. \<lbrakk>c = cap.ThreadCap t; c' = capability.ThreadCap t; list_all2 (\<lambda>(c, sl) (c', sl'). cap_relation c c' \<and> sl' = cte_map sl) extras extras'; length args < 2 ^ word_bits; cap_aligned (cap.ThreadCap t); capAligned (capability.ThreadCap t); gen_invocation_type label = TCBBindNotification\<rbrakk> \<Longrightarrow> list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras' proof (prove)
goal:
No subgoals!