theory Invoke_C

lemma decodeUntypedInvocation_ccorres:
notes TripleSuc[simp]
notes valid_untyped_inv_wcap'.simps[simp del]
shows
  "interpret_excaps extraCaps' = excaps_map extraCaps \<Longrightarrow>
   ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_')
       (invs' and (\<lambda>s. ksCurThread s = thread)
              and sch_act_simple and ct_active'
              and valid_cap' cp and K (isUntypedCap cp)
              and cte_wp_at' (\<lambda>cte. cteCap cte = cp) slot
              and (excaps_in_mem extraCaps \<circ> ctes_of)
              and (\<lambda>s. \<forall>v \<in> set extraCaps. \<forall>y \<in> zobj_refs' (fst v).
                              ex_nonz_cap_to' y s)
              and (\<lambda>s. \<forall>v \<in> set extraCaps.
                             s \<turnstile>' fst v)
              and sysargs_rel args buffer)
       (UNIV
             \<inter> {s. invLabel_' s = label}
             \<inter> {s. unat (length___unsigned_long_' s) = length args}
             \<inter> {s. ccap_relation cp (cap_' s)}
             \<inter> {s. slot_' s = cte_Ptr slot}
             \<inter> {s. current_extra_caps_' (globals s) = extraCaps'}
             \<inter> {s. call_' s = from_bool isCall}
             \<inter> {s. buffer_' s = option_to_ptr buffer})
       []
       (decodeUntypedInvocation label args slot cp (map fst extraCaps)
           >>= invocationCatch thread isBlocking isCall InvokeUntyped)
  (Call decodeUntypedInvocation_'proc)" apply (rule ccorres_name_pre) apply (clarsimp simp: isCap_simps) apply (rule ccorres_guard_imp2) apply (rule monadic_rewrite_ccorres_assemble) apply (rule_tac isBlocking=isBlocking and isCall=isCall and buffer=buffer
                in decodeUntypedInvocation_ccorres_helper) apply assumption apply (rule monadic_rewrite_trans[rotated]) apply (rule monadic_rewrite_bind_head) apply (simp add: liftE_bindE stateAssert_def2 bind_assoc) apply (monadic_rewrite_r monadic_rewrite_if_r_True) apply (monadic_rewrite_r_method monadic_rewrite_symb_exec_r_drop wpsimp) apply (rule monadic_rewrite_refl) apply wpsimp apply (rule monadic_rewrite_refl) apply (rule monadic_rewrite_refl) apply (clarsimp simp: ex_cte_cap_wp_to'_def excaps_in_mem_def) apply (drule(1) bspec)+ apply (rule_tac x = b in exI) apply (clarsimp simp: slotcap_in_mem_def cte_wp_at_ctes_of) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. interpret_excaps extraCaps' = excaps_map extraCaps \<Longrightarrow> ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (invs' and (\<lambda>s. ksCurThread s = thread) and sch_act_simple and ct_active' and valid_cap' cp and K (isUntypedCap cp) and cte_wp_at' (\<lambda>cte. cteCap cte = cp) slot and excaps_in_mem extraCaps \<circ> ctes_of and (\<lambda>s. \<forall>v\<in>set extraCaps. \<forall>y\<in>zobj_refs' (fst v). ex_nonz_cap_to' y s) and (\<lambda>s. \<forall>v\<in>set extraCaps. valid_cap' (fst v) s) and sysargs_rel args buffer) (UNIV \<inter> \<lbrace>\<acute>invLabel = label\<rbrace> \<inter> \<lbrace>unat \<acute>length___unsigned_long = length args\<rbrace> \<inter> \<lbrace>ccap_relation cp \<acute>cap\<rbrace> \<inter> \<lbrace>\<acute>slot = cte_Ptr slot\<rbrace> \<inter> \<lbrace>\<acute>current_extra_caps = extraCaps'\<rbrace> \<inter> \<lbrace>\<acute>call = from_bool isCall\<rbrace> \<inter> \<lbrace>\<acute>buffer = option_to_ptr buffer\<rbrace>) [] (decodeUntypedInvocation label args slot cp (map fst extraCaps) >>= invocationCatch thread isBlocking isCall Invocations_H.invocation.InvokeUntyped) (Call decodeUntypedInvocation_'proc) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>interpret_excaps extraCaps' = excaps_map extraCaps; (invs' and (\<lambda>s. ksCurThread s = thread) and sch_act_simple and ct_active' and valid_cap' cp and K (isUntypedCap cp) and cte_wp_at' (\<lambda>cte. cteCap cte = cp) slot and excaps_in_mem extraCaps \<circ> ctes_of and (\<lambda>s. \<forall>v\<in>set extraCaps. \<forall>y\<in>zobj_refs' (fst v). ex_nonz_cap_to' y s) and (\<lambda>s. \<forall>v\<in>set extraCaps. valid_cap' (fst v) s) and sysargs_rel args buffer) s\<rbrakk> \<Longrightarrow> ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (\<lambda>s'. s' = s) (UNIV \<inter> \<lbrace>\<acute>invLabel = label\<rbrace> \<inter> \<lbrace>unat \<acute>length___unsigned_long = length args\<rbrace> \<inter> \<lbrace>ccap_relation cp \<acute>cap\<rbrace> \<inter> \<lbrace>\<acute>slot = cte_Ptr slot\<rbrace> \<inter> \<lbrace>\<acute>current_extra_caps = extraCaps'\<rbrace> \<inter> \<lbrace>\<acute>call = from_bool isCall\<rbrace> \<inter> \<lbrace>\<acute>buffer = option_to_ptr buffer\<rbrace>) [] (decodeUntypedInvocation label args slot cp (map fst extraCaps) >>= invocationCatch thread isBlocking isCall Invocations_H.invocation.InvokeUntyped) (Call decodeUntypedInvocation_'proc) proof (prove)
goal (1 subgoal):
 1. \<And>s d v0 v1 f. \<lbrakk>interpret_excaps extraCaps' = excaps_map extraCaps; invs' s; thread = ksCurThread s; sch_act_simple s; ct_active' s; valid_cap' (capability.UntypedCap d v0 v1 f) s; cp = capability.UntypedCap d v0 v1 f; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d v0 v1 f) slot s; excaps_in_mem extraCaps (ctes_of s); \<forall>v\<in>set extraCaps. \<forall>y\<in>zobj_refs' (fst v). ex_nonz_cap_to' y s; \<forall>v\<in>set extraCaps. valid_cap' (fst v) s; sysargs_rel args buffer s\<rbrakk> \<Longrightarrow> ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (\<lambda>s'. s' = s) (\<lbrace>\<acute>invLabel = label\<rbrace> \<inter> \<lbrace>unat \<acute>length___unsigned_long = length args\<rbrace> \<inter> \<lbrace>ccap_relation (capability.UntypedCap d v0 v1 f) \<acute>cap\<rbrace> \<inter> \<lbrace>\<acute>slot = cte_Ptr slot\<rbrace> \<inter> \<lbrace>\<acute>current_extra_caps = extraCaps'\<rbrace> \<inter> \<lbrace>\<acute>call = from_bool isCall\<rbrace> \<inter> \<lbrace>\<acute>buffer = option_to_ptr buffer\<rbrace>) [] (decodeUntypedInvocation label args slot (capability.UntypedCap d v0 v1 f) (map fst extraCaps) >>= invocationCatch (ksCurThread s) isBlocking isCall Invocations_H.invocation.InvokeUntyped) (Call decodeUntypedInvocation_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>s d v0 v1 f. \<lbrakk>interpret_excaps extraCaps' = excaps_map extraCaps; invs' s; thread = ksCurThread s; sch_act_simple s; ct_active' s; valid_cap' (capability.UntypedCap d v0 v1 f) s; cp = capability.UntypedCap d v0 v1 f; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d v0 v1 f) slot s; excaps_in_mem extraCaps (ctes_of s); \<forall>v\<in>set extraCaps. \<forall>y\<in>zobj_refs' (fst v). ex_nonz_cap_to' y s; \<forall>v\<in>set extraCaps. valid_cap' (fst v) s; sysargs_rel args buffer s\<rbrakk> \<Longrightarrow> ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q25 s d v0 v1 f) (?Q'25 s d v0 v1 f) [] (decodeUntypedInvocation label args slot (capability.UntypedCap d v0 v1 f) (map fst extraCaps) >>= invocationCatch (ksCurThread s) isBlocking isCall Invocations_H.invocation.InvokeUntyped) (Call decodeUntypedInvocation_'proc)
 2. \<And>s d v0 v1 f sa s'. \<lbrakk>interpret_excaps extraCaps' = excaps_map extraCaps; invs' s; thread = ksCurThread s; sch_act_simple s; ct_active' s; valid_cap' (capability.UntypedCap d v0 v1 f) s; cp = capability.UntypedCap d v0 v1 f; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d v0 v1 f) slot s; excaps_in_mem extraCaps (ctes_of s); \<forall>v\<in>set extraCaps. \<forall>y\<in>zobj_refs' (fst v). ex_nonz_cap_to' y s; \<forall>v\<in>set extraCaps. valid_cap' (fst v) s; sysargs_rel args buffer s; (sa, s') \<in> rf_sr; sa = s; s' \<in> \<lbrace>\<acute>invLabel = label\<rbrace> \<inter> \<lbrace>unat \<acute>length___unsigned_long = length args\<rbrace> \<inter> \<lbrace>ccap_relation (capability.UntypedCap d v0 v1 f) \<acute>cap\<rbrace> \<inter> \<lbrace>\<acute>slot = cte_Ptr slot\<rbrace> \<inter> \<lbrace>\<acute>current_extra_caps = extraCaps'\<rbrace> \<inter> \<lbrace>\<acute>call = from_bool isCall\<rbrace> \<inter> \<lbrace>\<acute>buffer = option_to_ptr buffer\<rbrace>\<rbrakk> \<Longrightarrow> ?Q25 s d v0 v1 f sa \<and> s' \<in> ?Q'25 s d v0 v1 f proof (prove)
goal (3 subgoals):
 1. \<And>s d v0 v1 f. \<lbrakk>interpret_excaps extraCaps' = excaps_map extraCaps; invs' s; thread = ksCurThread s; sch_act_simple s; ct_active' s; valid_cap' (capability.UntypedCap d v0 v1 f) s; cp = capability.UntypedCap d v0 v1 f; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d v0 v1 f) slot s; excaps_in_mem extraCaps (ctes_of s); \<forall>v\<in>set extraCaps. \<forall>y\<in>zobj_refs' (fst v). ex_nonz_cap_to' y s; \<forall>v\<in>set extraCaps. valid_cap' (fst v) s; sysargs_rel args buffer s\<rbrakk> \<Longrightarrow> ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?P28 s d v0 v1 f) (?Q'25 s d v0 v1 f) [] (?f28 s d v0 v1 f) (Call decodeUntypedInvocation_'proc)
 2. \<And>s d v0 v1 f. \<lbrakk>interpret_excaps extraCaps' = excaps_map extraCaps; invs' s; thread = ksCurThread s; sch_act_simple s; ct_active' s; valid_cap' (capability.UntypedCap d v0 v1 f) s; cp = capability.UntypedCap d v0 v1 f; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d v0 v1 f) slot s; excaps_in_mem extraCaps (ctes_of s); \<forall>v\<in>set extraCaps. \<forall>y\<in>zobj_refs' (fst v). ex_nonz_cap_to' y s; \<forall>v\<in>set extraCaps. valid_cap' (fst v) s; sysargs_rel args buffer s\<rbrakk> \<Longrightarrow> monadic_rewrite (?F28 s d v0 v1 f) (?E28 s d v0 v1 f) (?Q28 s d v0 v1 f) (decodeUntypedInvocation label args slot (capability.UntypedCap d v0 v1 f) (map fst extraCaps) >>= invocationCatch (ksCurThread s) isBlocking isCall Invocations_H.invocation.InvokeUntyped) (?f28 s d v0 v1 f)
 3. \<And>s d v0 v1 f sa s'. \<lbrakk>interpret_excaps extraCaps' = excaps_map extraCaps; invs' s; thread = ksCurThread s; sch_act_simple s; ct_active' s; valid_cap' (capability.UntypedCap d v0 v1 f) s; cp = capability.UntypedCap d v0 v1 f; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d v0 v1 f) slot s; excaps_in_mem extraCaps (ctes_of s); \<forall>v\<in>set extraCaps. \<forall>y\<in>zobj_refs' (fst v). ex_nonz_cap_to' y s; \<forall>v\<in>set extraCaps. valid_cap' (fst v) s; sysargs_rel args buffer s; (sa, s') \<in> rf_sr; sa = s; s' \<in> \<lbrace>\<acute>invLabel = label\<rbrace> \<inter> \<lbrace>unat \<acute>length___unsigned_long = length args\<rbrace> \<inter> \<lbrace>ccap_relation (capability.UntypedCap d v0 v1 f) \<acute>cap\<rbrace> \<inter> \<lbrace>\<acute>slot = cte_Ptr slot\<rbrace> \<inter> \<lbrace>\<acute>current_extra_caps = extraCaps'\<rbrace> \<inter> \<lbrace>\<acute>call = from_bool isCall\<rbrace> \<inter> \<lbrace>\<acute>buffer = option_to_ptr buffer\<rbrace>\<rbrakk> \<Longrightarrow> (?P28 s d v0 v1 f and ?Q28 s d v0 v1 f) sa \<and> s' \<in> ?Q'25 s d v0 v1 f proof (prove)
goal (3 subgoals):
 1. \<And>s d v0 v1 f. \<lbrakk>interpret_excaps extraCaps' = excaps_map extraCaps; invs' s; thread = ksCurThread s; sch_act_simple s; ct_active' s; valid_cap' (capability.UntypedCap d v0 v1 f) s; cp = capability.UntypedCap d v0 v1 f; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d v0 v1 f) slot s; excaps_in_mem extraCaps (ctes_of s); \<forall>v\<in>set extraCaps. \<forall>y\<in>zobj_refs' (fst v). ex_nonz_cap_to' y s; \<forall>v\<in>set extraCaps. valid_cap' (fst v) s; sysargs_rel args buffer s\<rbrakk> \<Longrightarrow> interpret_excaps (?extraCaps'31 s d v0 v1 f) = excaps_map (?extraCaps31 s d v0 v1 f)
 2. \<And>s d v0 v1 f. \<lbrakk>interpret_excaps extraCaps' = excaps_map extraCaps; invs' s; thread = ksCurThread s; sch_act_simple s; ct_active' s; valid_cap' (capability.UntypedCap d v0 v1 f) s; cp = capability.UntypedCap d v0 v1 f; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d v0 v1 f) slot s; excaps_in_mem extraCaps (ctes_of s); \<forall>v\<in>set extraCaps. \<forall>y\<in>zobj_refs' (fst v). ex_nonz_cap_to' y s; \<forall>v\<in>set extraCaps. valid_cap' (fst v) s; sysargs_rel args buffer s\<rbrakk> \<Longrightarrow> monadic_rewrite (?F28 s d v0 v1 f) (?E28 s d v0 v1 f) (?Q28 s d v0 v1 f) (decodeUntypedInvocation label args slot (capability.UntypedCap d v0 v1 f) (map fst extraCaps) >>= invocationCatch (ksCurThread s) isBlocking isCall Invocations_H.invocation.InvokeUntyped) (doE uinv <- decodeUntypedInvocation (?label31 s d v0 v1 f) (?args31 s d v0 v1 f) (?slot31 s d v0 v1 f) (?cp31 s d v0 v1 f) (map fst (?extraCaps31 s d v0 v1 f));
liftE (stateAssert (valid_untyped_inv' uinv) []);
returnOk uinv
odE >>= invocationCatch (?thread31 s d v0 v1 f) isBlocking isCall Invocations_H.invocation.InvokeUntyped)
 3. \<And>s d v0 v1 f sa s'. \<lbrakk>interpret_excaps extraCaps' = excaps_map extraCaps; invs' s; thread = ksCurThread s; sch_act_simple s; ct_active' s; valid_cap' (capability.UntypedCap d v0 v1 f) s; cp = capability.UntypedCap d v0 v1 f; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d v0 v1 f) slot s; excaps_in_mem extraCaps (ctes_of s); \<forall>v\<in>set extraCaps. \<forall>y\<in>zobj_refs' (fst v). ex_nonz_cap_to' y s; \<forall>v\<in>set extraCaps. valid_cap' (fst v) s; sysargs_rel args buffer s; (sa, s') \<in> rf_sr; sa = s; s' \<in> \<lbrace>\<acute>invLabel = label\<rbrace> \<inter> \<lbrace>unat \<acute>length___unsigned_long = length args\<rbrace> \<inter> \<lbrace>ccap_relation (capability.UntypedCap d v0 v1 f) \<acute>cap\<rbrace> \<inter> \<lbrace>\<acute>slot = cte_Ptr slot\<rbrace> \<inter> \<lbrace>\<acute>current_extra_caps = extraCaps'\<rbrace> \<inter> \<lbrace>\<acute>call = from_bool isCall\<rbrace> \<inter> \<lbrace>\<acute>buffer = option_to_ptr buffer\<rbrace>\<rbrakk> \<Longrightarrow> (invs' and (\<lambda>sa. ksCurThread sa = ?thread31 s d v0 v1 f) and sch_act_simple and ct_active' and valid_cap' (?cp31 s d v0 v1 f) and K (isUntypedCap (?cp31 s d v0 v1 f)) and cte_wp_at' (\<lambda>cte. cteCap cte = ?cp31 s d v0 v1 f) (?slot31 s d v0 v1 f) and excaps_in_mem (?extraCaps31 s d v0 v1 f) \<circ> ctes_of and (\<lambda>sa. \<forall>v\<in>set (?extraCaps31 s d v0 v1 f). \<forall>y\<in>zobj_refs' (fst v). ex_nonz_cap_to' y sa) and (\<lambda>sa. \<forall>v\<in>set (?extraCaps31 s d v0 v1 f). valid_cap' (fst v) sa) and sysargs_rel (?args31 s d v0 v1 f) buffer and ?Q28 s d v0 v1 f) sa \<and> s' \<in> UNIV \<inter> \<lbrace>\<acute>invLabel = ?label31 s d v0 v1 f\<rbrace> \<inter> \<lbrace>unat \<acute>length___unsigned_long = length (?args31 s d v0 v1 f)\<rbrace> \<inter> \<lbrace>ccap_relation (?cp31 s d v0 v1 f) \<acute>cap\<rbrace> \<inter> \<lbrace>\<acute>slot = cte_Ptr (?slot31 s d v0 v1 f)\<rbrace> \<inter> \<lbrace>\<acute>current_extra_caps = ?extraCaps'31 s d v0 v1 f\<rbrace> \<inter> \<lbrace>\<acute>call = from_bool isCall\<rbrace> \<inter> \<lbrace>\<acute>buffer = option_to_ptr buffer\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s d v0 v1 f. \<lbrakk>interpret_excaps extraCaps' = excaps_map extraCaps; invs' s; thread = ksCurThread s; sch_act_simple s; ct_active' s; valid_cap' (capability.UntypedCap d v0 v1 f) s; cp = capability.UntypedCap d v0 v1 f; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d v0 v1 f) slot s; excaps_in_mem extraCaps (ctes_of s); \<forall>v\<in>set extraCaps. \<forall>y\<in>zobj_refs' (fst v). ex_nonz_cap_to' y s; \<forall>v\<in>set extraCaps. valid_cap' (fst v) s; sysargs_rel args buffer s\<rbrakk> \<Longrightarrow> monadic_rewrite (?F28 s d v0 v1 f) (?E28 s d v0 v1 f) (?Q28 s d v0 v1 f) (decodeUntypedInvocation label args slot (capability.UntypedCap d v0 v1 f) (map fst extraCaps) >>= invocationCatch (ksCurThread s) isBlocking isCall Invocations_H.invocation.InvokeUntyped) (doE uinv <- decodeUntypedInvocation (?label31 s d v0 v1 f) (?args31 s d v0 v1 f) (?slot31 s d v0 v1 f) (?cp31 s d v0 v1 f) (map fst extraCaps);
liftE (stateAssert (valid_untyped_inv' uinv) []);
returnOk uinv
odE >>= invocationCatch (?thread31 s d v0 v1 f) isBlocking isCall Invocations_H.invocation.InvokeUntyped)
 2. \<And>s d v0 v1 f sa s'. \<lbrakk>interpret_excaps extraCaps' = excaps_map extraCaps; invs' s; thread = ksCurThread s; sch_act_simple s; ct_active' s; valid_cap' (capability.UntypedCap d v0 v1 f) s; cp = capability.UntypedCap d v0 v1 f; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d v0 v1 f) slot s; excaps_in_mem extraCaps (ctes_of s); \<forall>v\<in>set extraCaps. \<forall>y\<in>zobj_refs' (fst v). ex_nonz_cap_to' y s; \<forall>v\<in>set extraCaps. valid_cap' (fst v) s; sysargs_rel args buffer s; (sa, s') \<in> rf_sr; sa = s; s' \<in> \<lbrace>\<acute>invLabel = label\<rbrace> \<inter> \<lbrace>unat \<acute>length___unsigned_long = length args\<rbrace> \<inter> \<lbrace>ccap_relation (capability.UntypedCap d v0 v1 f) \<acute>cap\<rbrace> \<inter> \<lbrace>\<acute>slot = cte_Ptr slot\<rbrace> \<inter> \<lbrace>\<acute>current_extra_caps = extraCaps'\<rbrace> \<inter> \<lbrace>\<acute>call = from_bool isCall\<rbrace> \<inter> \<lbrace>\<acute>buffer = option_to_ptr buffer\<rbrace>\<rbrakk> \<Longrightarrow> (invs' and (\<lambda>sa. ksCurThread sa = ?thread31 s d v0 v1 f) and sch_act_simple and ct_active' and valid_cap' (?cp31 s d v0 v1 f) and K (isUntypedCap (?cp31 s d v0 v1 f)) and cte_wp_at' (\<lambda>cte. cteCap cte = ?cp31 s d v0 v1 f) (?slot31 s d v0 v1 f) and excaps_in_mem extraCaps \<circ> ctes_of and (\<lambda>s. \<forall>v\<in>set extraCaps. \<forall>y\<in>zobj_refs' (fst v). ex_nonz_cap_to' y s) and (\<lambda>s. \<forall>v\<in>set extraCaps. valid_cap' (fst v) s) and sysargs_rel (?args31 s d v0 v1 f) buffer and ?Q28 s d v0 v1 f) sa \<and> s' \<in> UNIV \<inter> \<lbrace>\<acute>invLabel = ?label31 s d v0 v1 f\<rbrace> \<inter> \<lbrace>unat \<acute>length___unsigned_long = length (?args31 s d v0 v1 f)\<rbrace> \<inter> \<lbrace>ccap_relation (?cp31 s d v0 v1 f) \<acute>cap\<rbrace> \<inter> \<lbrace>\<acute>slot = cte_Ptr (?slot31 s d v0 v1 f)\<rbrace> \<inter> \<lbrace>\<acute>current_extra_caps = extraCaps'\<rbrace> \<inter> \<lbrace>\<acute>call = from_bool isCall\<rbrace> \<inter> \<lbrace>\<acute>buffer = option_to_ptr buffer\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s d v0 v1 f. \<lbrakk>interpret_excaps extraCaps' = excaps_map extraCaps; invs' s; thread = ksCurThread s; sch_act_simple s; ct_active' s; valid_cap' (capability.UntypedCap d v0 v1 f) s; cp = capability.UntypedCap d v0 v1 f; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d v0 v1 f) slot s; excaps_in_mem extraCaps (ctes_of s); \<forall>v\<in>set extraCaps. \<forall>y\<in>zobj_refs' (fst v). ex_nonz_cap_to' y s; \<forall>v\<in>set extraCaps. valid_cap' (fst v) s; sysargs_rel args buffer s\<rbrakk> \<Longrightarrow> monadic_rewrite (?F28 s d v0 v1 f) (?E28 s d v0 v1 f) (?Q32 s d v0 v1 f) (?g32 s d v0 v1 f) (doE uinv <- decodeUntypedInvocation (?label31 s d v0 v1 f) (?args31 s d v0 v1 f) (?slot31 s d v0 v1 f) (?cp31 s d v0 v1 f) (map fst extraCaps);
liftE (stateAssert (valid_untyped_inv' uinv) []);
returnOk uinv
odE >>= invocationCatch (?thread31 s d v0 v1 f) isBlocking isCall Invocations_H.invocation.InvokeUntyped)
 2. \<And>s d v0 v1 f. \<lbrakk>interpret_excaps extraCaps' = excaps_map extraCaps; invs' s; thread = ksCurThread s; sch_act_simple s; ct_active' s; valid_cap' (capability.UntypedCap d v0 v1 f) s; cp = capability.UntypedCap d v0 v1 f; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d v0 v1 f) slot s; excaps_in_mem extraCaps (ctes_of s); \<forall>v\<in>set extraCaps. \<forall>y\<in>zobj_refs' (fst v). ex_nonz_cap_to' y s; \<forall>v\<in>set extraCaps. valid_cap' (fst v) s; sysargs_rel args buffer s\<rbrakk> \<Longrightarrow> monadic_rewrite (?F28 s d v0 v1 f) (?E28 s d v0 v1 f) (?P32 s d v0 v1 f) (decodeUntypedInvocation label args slot (capability.UntypedCap d v0 v1 f) (map fst extraCaps) >>= invocationCatch (ksCurThread s) isBlocking isCall Invocations_H.invocation.InvokeUntyped) (?g32 s d v0 v1 f)
 3. \<And>s d v0 v1 f sa s'. \<lbrakk>interpret_excaps extraCaps' = excaps_map extraCaps; invs' s; thread = ksCurThread s; sch_act_simple s; ct_active' s; valid_cap' (capability.UntypedCap d v0 v1 f) s; cp = capability.UntypedCap d v0 v1 f; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d v0 v1 f) slot s; excaps_in_mem extraCaps (ctes_of s); \<forall>v\<in>set extraCaps. \<forall>y\<in>zobj_refs' (fst v). ex_nonz_cap_to' y s; \<forall>v\<in>set extraCaps. valid_cap' (fst v) s; sysargs_rel args buffer s; (sa, s') \<in> rf_sr; sa = s; s' \<in> \<lbrace>\<acute>invLabel = label\<rbrace> \<inter> \<lbrace>unat \<acute>length___unsigned_long = length args\<rbrace> \<inter> \<lbrace>ccap_relation (capability.UntypedCap d v0 v1 f) \<acute>cap\<rbrace> \<inter> \<lbrace>\<acute>slot = cte_Ptr slot\<rbrace> \<inter> \<lbrace>\<acute>current_extra_caps = extraCaps'\<rbrace> \<inter> \<lbrace>\<acute>call = from_bool isCall\<rbrace> \<inter> \<lbrace>\<acute>buffer = option_to_ptr buffer\<rbrace>\<rbrakk> \<Longrightarrow> (invs' and (\<lambda>sa. ksCurThread sa = ?thread31 s d v0 v1 f) and sch_act_simple and ct_active' and valid_cap' (?cp31 s d v0 v1 f) and K (isUntypedCap (?cp31 s d v0 v1 f)) and cte_wp_at' (\<lambda>cte. cteCap cte = ?cp31 s d v0 v1 f) (?slot31 s d v0 v1 f) and excaps_in_mem extraCaps \<circ> ctes_of and (\<lambda>s. \<forall>v\<in>set extraCaps. \<forall>y\<in>zobj_refs' (fst v). ex_nonz_cap_to' y s) and (\<lambda>s. \<forall>v\<in>set extraCaps. valid_cap' (fst v) s) and sysargs_rel (?args31 s d v0 v1 f) buffer and (?P32 s d v0 v1 f and ?Q32 s d v0 v1 f)) sa \<and> s' \<in> UNIV \<inter> \<lbrace>\<acute>invLabel = ?label31 s d v0 v1 f\<rbrace> \<inter> \<lbrace>unat \<acute>length___unsigned_long = length (?args31 s d v0 v1 f)\<rbrace> \<inter> \<lbrace>ccap_relation (?cp31 s d v0 v1 f) \<acute>cap\<rbrace> \<inter> \<lbrace>\<acute>slot = cte_Ptr (?slot31 s d v0 v1 f)\<rbrace> \<inter> \<lbrace>\<acute>current_extra_caps = extraCaps'\<rbrace> \<inter> \<lbrace>\<acute>call = from_bool isCall\<rbrace> \<inter> \<lbrace>\<acute>buffer = option_to_ptr buffer\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s d v0 v1 f. \<lbrakk>interpret_excaps extraCaps' = excaps_map extraCaps; invs' s; thread = ksCurThread s; sch_act_simple s; ct_active' s; valid_cap' (capability.UntypedCap d v0 v1 f) s; cp = capability.UntypedCap d v0 v1 f; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d v0 v1 f) slot s; excaps_in_mem extraCaps (ctes_of s); \<forall>v\<in>set extraCaps. \<forall>y\<in>zobj_refs' (fst v). ex_nonz_cap_to' y s; \<forall>v\<in>set extraCaps. valid_cap' (fst v) s; sysargs_rel args buffer s\<rbrakk> \<Longrightarrow> monadic_rewrite (?F28 s d v0 v1 f) (?E28 s d v0 v1 f) (?Q32 s d v0 v1 f) (?f35 s d v0 v1 f) (doE uinv <- decodeUntypedInvocation (?label31 s d v0 v1 f) (?args31 s d v0 v1 f) (?slot31 s d v0 v1 f) (?cp31 s d v0 v1 f) (map fst extraCaps);
liftE (stateAssert (valid_untyped_inv' uinv) []);
returnOk uinv
odE)
 2. \<And>s d v0 v1 f. \<lbrakk>interpret_excaps extraCaps' = excaps_map extraCaps; invs' s; thread = ksCurThread s; sch_act_simple s; ct_active' s; valid_cap' (capability.UntypedCap d v0 v1 f) s; cp = capability.UntypedCap d v0 v1 f; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d v0 v1 f) slot s; excaps_in_mem extraCaps (ctes_of s); \<forall>v\<in>set extraCaps. \<forall>y\<in>zobj_refs' (fst v). ex_nonz_cap_to' y s; \<forall>v\<in>set extraCaps. valid_cap' (fst v) s; sysargs_rel args buffer s\<rbrakk> \<Longrightarrow> monadic_rewrite (?F28 s d v0 v1 f) (?E28 s d v0 v1 f) (?P32 s d v0 v1 f) (decodeUntypedInvocation label args slot (capability.UntypedCap d v0 v1 f) (map fst extraCaps) >>= invocationCatch (ksCurThread s) isBlocking isCall Invocations_H.invocation.InvokeUntyped) (?f35 s d v0 v1 f >>= invocationCatch (?thread31 s d v0 v1 f) isBlocking isCall Invocations_H.invocation.InvokeUntyped)
 3. \<And>s d v0 v1 f sa s'. \<lbrakk>interpret_excaps extraCaps' = excaps_map extraCaps; invs' s; thread = ksCurThread s; sch_act_simple s; ct_active' s; valid_cap' (capability.UntypedCap d v0 v1 f) s; cp = capability.UntypedCap d v0 v1 f; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d v0 v1 f) slot s; excaps_in_mem extraCaps (ctes_of s); \<forall>v\<in>set extraCaps. \<forall>y\<in>zobj_refs' (fst v). ex_nonz_cap_to' y s; \<forall>v\<in>set extraCaps. valid_cap' (fst v) s; sysargs_rel args buffer s; (sa, s') \<in> rf_sr; sa = s; s' \<in> \<lbrace>\<acute>invLabel = label\<rbrace> \<inter> \<lbrace>unat \<acute>length___unsigned_long = length args\<rbrace> \<inter> \<lbrace>ccap_relation (capability.UntypedCap d v0 v1 f) \<acute>cap\<rbrace> \<inter> \<lbrace>\<acute>slot = cte_Ptr slot\<rbrace> \<inter> \<lbrace>\<acute>current_extra_caps = extraCaps'\<rbrace> \<inter> \<lbrace>\<acute>call = from_bool isCall\<rbrace> \<inter> \<lbrace>\<acute>buffer = option_to_ptr buffer\<rbrace>\<rbrakk> \<Longrightarrow> (invs' and (\<lambda>sa. ksCurThread sa = ?thread31 s d v0 v1 f) and sch_act_simple and ct_active' and valid_cap' (?cp31 s d v0 v1 f) and K (isUntypedCap (?cp31 s d v0 v1 f)) and cte_wp_at' (\<lambda>cte. cteCap cte = ?cp31 s d v0 v1 f) (?slot31 s d v0 v1 f) and excaps_in_mem extraCaps \<circ> ctes_of and (\<lambda>s. \<forall>v\<in>set extraCaps. \<forall>y\<in>zobj_refs' (fst v). ex_nonz_cap_to' y s) and (\<lambda>s. \<forall>v\<in>set extraCaps. valid_cap' (fst v) s) and sysargs_rel (?args31 s d v0 v1 f) buffer and (?P32 s d v0 v1 f and ?Q32 s d v0 v1 f)) sa \<and> s' \<in> UNIV \<inter> \<lbrace>\<acute>invLabel = ?label31 s d v0 v1 f\<rbrace> \<inter> \<lbrace>unat \<acute>length___unsigned_long = length (?args31 s d v0 v1 f)\<rbrace> \<inter> \<lbrace>ccap_relation (?cp31 s d v0 v1 f) \<acute>cap\<rbrace> \<inter> \<lbrace>\<acute>slot = cte_Ptr (?slot31 s d v0 v1 f)\<rbrace> \<inter> \<lbrace>\<acute>current_extra_caps = extraCaps'\<rbrace> \<inter> \<lbrace>\<acute>call = from_bool isCall\<rbrace> \<inter> \<lbrace>\<acute>buffer = option_to_ptr buffer\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s d v0 v1 f. \<lbrakk>interpret_excaps extraCaps' = excaps_map extraCaps; invs' s; thread = ksCurThread s; sch_act_simple s; ct_active' s; valid_cap' (capability.UntypedCap d v0 v1 f) s; cp = capability.UntypedCap d v0 v1 f; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d v0 v1 f) slot s; excaps_in_mem extraCaps (ctes_of s); \<forall>v\<in>set extraCaps. \<forall>y\<in>zobj_refs' (fst v). ex_nonz_cap_to' y s; \<forall>v\<in>set extraCaps. valid_cap' (fst v) s; sysargs_rel args buffer s\<rbrakk> \<Longrightarrow> monadic_rewrite (?F28 s d v0 v1 f) (?E28 s d v0 v1 f) (?Q32 s d v0 v1 f) (?f35 s d v0 v1 f) (doE uinv <- decodeUntypedInvocation (?label31 s d v0 v1 f) (?args31 s d v0 v1 f) (?slot31 s d v0 v1 f) (?cp31 s d v0 v1 f) (map fst extraCaps);
do x <- gets (valid_untyped_inv' uinv);
y <- if x then return () else fail;
returnOk uinv
od
odE)
 2. \<And>s d v0 v1 f. \<lbrakk>interpret_excaps extraCaps' = excaps_map extraCaps; invs' s; thread = ksCurThread s; sch_act_simple s; ct_active' s; valid_cap' (capability.UntypedCap d v0 v1 f) s; cp = capability.UntypedCap d v0 v1 f; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d v0 v1 f) slot s; excaps_in_mem extraCaps (ctes_of s); \<forall>v\<in>set extraCaps. \<forall>y\<in>zobj_refs' (fst v). ex_nonz_cap_to' y s; \<forall>v\<in>set extraCaps. valid_cap' (fst v) s; sysargs_rel args buffer s\<rbrakk> \<Longrightarrow> monadic_rewrite (?F28 s d v0 v1 f) (?E28 s d v0 v1 f) (?P32 s d v0 v1 f) (decodeUntypedInvocation label args slot (capability.UntypedCap d v0 v1 f) (map fst extraCaps) >>= invocationCatch (ksCurThread s) isBlocking isCall Invocations_H.invocation.InvokeUntyped) (?f35 s d v0 v1 f >>= invocationCatch (?thread31 s d v0 v1 f) isBlocking isCall Invocations_H.invocation.InvokeUntyped)
 3. \<And>s d v0 v1 f sa s'. \<lbrakk>interpret_excaps extraCaps' = excaps_map extraCaps; invs' s; thread = ksCurThread s; sch_act_simple s; ct_active' s; valid_cap' (capability.UntypedCap d v0 v1 f) s; cp = capability.UntypedCap d v0 v1 f; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d v0 v1 f) slot s; excaps_in_mem extraCaps (ctes_of s); \<forall>v\<in>set extraCaps. \<forall>y\<in>zobj_refs' (fst v). ex_nonz_cap_to' y s; \<forall>v\<in>set extraCaps. valid_cap' (fst v) s; sysargs_rel args buffer s; (sa, s') \<in> rf_sr; sa = s; s' \<in> \<lbrace>\<acute>invLabel = label\<rbrace> \<inter> \<lbrace>unat \<acute>length___unsigned_long = length args\<rbrace> \<inter> \<lbrace>ccap_relation (capability.UntypedCap d v0 v1 f) \<acute>cap\<rbrace> \<inter> \<lbrace>\<acute>slot = cte_Ptr slot\<rbrace> \<inter> \<lbrace>\<acute>current_extra_caps = extraCaps'\<rbrace> \<inter> \<lbrace>\<acute>call = from_bool isCall\<rbrace> \<inter> \<lbrace>\<acute>buffer = option_to_ptr buffer\<rbrace>\<rbrakk> \<Longrightarrow> (invs' and (\<lambda>sa. ksCurThread sa = ?thread31 s d v0 v1 f) and sch_act_simple and ct_active' and valid_cap' (?cp31 s d v0 v1 f) and K (isUntypedCap (?cp31 s d v0 v1 f)) and cte_wp_at' (\<lambda>cte. cteCap cte = ?cp31 s d v0 v1 f) (?slot31 s d v0 v1 f) and excaps_in_mem extraCaps \<circ> ctes_of and (\<lambda>s. \<forall>v\<in>set extraCaps. \<forall>y\<in>zobj_refs' (fst v). ex_nonz_cap_to' y s) and (\<lambda>s. \<forall>v\<in>set extraCaps. valid_cap' (fst v) s) and sysargs_rel (?args31 s d v0 v1 f) buffer and (?P32 s d v0 v1 f and ?Q32 s d v0 v1 f)) sa \<and> s' \<in> UNIV \<inter> \<lbrace>\<acute>invLabel = ?label31 s d v0 v1 f\<rbrace> \<inter> \<lbrace>unat \<acute>length___unsigned_long = length (?args31 s d v0 v1 f)\<rbrace> \<inter> \<lbrace>ccap_relation (?cp31 s d v0 v1 f) \<acute>cap\<rbrace> \<inter> \<lbrace>\<acute>slot = cte_Ptr (?slot31 s d v0 v1 f)\<rbrace> \<inter> \<lbrace>\<acute>current_extra_caps = extraCaps'\<rbrace> \<inter> \<lbrace>\<acute>call = from_bool isCall\<rbrace> \<inter> \<lbrace>\<acute>buffer = option_to_ptr buffer\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s d v0 v1 f. \<lbrakk>interpret_excaps extraCaps' = excaps_map extraCaps; invs' s; thread = ksCurThread s; sch_act_simple s; ct_active' s; valid_cap' (capability.UntypedCap d v0 v1 f) s; cp = capability.UntypedCap d v0 v1 f; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d v0 v1 f) slot s; excaps_in_mem extraCaps (ctes_of s); \<forall>v\<in>set extraCaps. \<forall>y\<in>zobj_refs' (fst v). ex_nonz_cap_to' y s; \<forall>v\<in>set extraCaps. valid_cap' (fst v) s; sysargs_rel args buffer s\<rbrakk> \<Longrightarrow> monadic_rewrite (?F28 s d v0 v1 f) (?E28 s d v0 v1 f) (?P37 s d v0 v1 f) (?f35 s d v0 v1 f) (doE uinv <- decodeUntypedInvocation (?label31 s d v0 v1 f) (?args31 s d v0 v1 f) (?slot31 s d v0 v1 f) (capability.UntypedCap (?d69 s d v0 v1 f) (?w69 s d v0 v1 f) (?sz69 s d v0 v1 f) (?idx69 s d v0 v1 f)) (map fst extraCaps);
do x <- gets (valid_untyped_inv' uinv);
y <- return ();
returnOk uinv
od
odE)
 2. \<And>s d v0 v1 f. \<lbrakk>interpret_excaps extraCaps' = excaps_map extraCaps; invs' s; thread = ksCurThread s; sch_act_simple s; ct_active' s; valid_cap' (capability.UntypedCap d v0 v1 f) s; cp = capability.UntypedCap d v0 v1 f; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d v0 v1 f) slot s; excaps_in_mem extraCaps (ctes_of s); \<forall>v\<in>set extraCaps. \<forall>y\<in>zobj_refs' (fst v). ex_nonz_cap_to' y s; \<forall>v\<in>set extraCaps. valid_cap' (fst v) s; sysargs_rel args buffer s\<rbrakk> \<Longrightarrow> monadic_rewrite (?F28 s d v0 v1 f) (?E28 s d v0 v1 f) (?P32 s d v0 v1 f) (decodeUntypedInvocation label args slot (capability.UntypedCap d v0 v1 f) (map fst extraCaps) >>= invocationCatch (ksCurThread s) isBlocking isCall Invocations_H.invocation.InvokeUntyped) (?f35 s d v0 v1 f >>= invocationCatch (?thread31 s d v0 v1 f) isBlocking isCall Invocations_H.invocation.InvokeUntyped)
 3. \<And>s d v0 v1 f sa s'. \<lbrakk>interpret_excaps extraCaps' = excaps_map extraCaps; invs' s; thread = ksCurThread s; sch_act_simple s; ct_active' s; valid_cap' (capability.UntypedCap d v0 v1 f) s; cp = capability.UntypedCap d v0 v1 f; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d v0 v1 f) slot s; excaps_in_mem extraCaps (ctes_of s); \<forall>v\<in>set extraCaps. \<forall>y\<in>zobj_refs' (fst v). ex_nonz_cap_to' y s; \<forall>v\<in>set extraCaps. valid_cap' (fst v) s; sysargs_rel args buffer s; (sa, s') \<in> rf_sr; sa = s; s' \<in> \<lbrace>\<acute>invLabel = label\<rbrace> \<inter> \<lbrace>unat \<acute>length___unsigned_long = length args\<rbrace> \<inter> \<lbrace>ccap_relation (capability.UntypedCap d v0 v1 f) \<acute>cap\<rbrace> \<inter> \<lbrace>\<acute>slot = cte_Ptr slot\<rbrace> \<inter> \<lbrace>\<acute>current_extra_caps = extraCaps'\<rbrace> \<inter> \<lbrace>\<acute>call = from_bool isCall\<rbrace> \<inter> \<lbrace>\<acute>buffer = option_to_ptr buffer\<rbrace>\<rbrakk> \<Longrightarrow> (invs' and (\<lambda>sa. ksCurThread sa = ?thread31 s d v0 v1 f) and sch_act_simple and ct_active' and valid_cap' (capability.UntypedCap (?d69 s d v0 v1 f) (?w69 s d v0 v1 f) (?sz69 s d v0 v1 f) (?idx69 s d v0 v1 f)) and K (isUntypedCap (capability.UntypedCap (?d69 s d v0 v1 f) (?w69 s d v0 v1 f) (?sz69 s d v0 v1 f) (?idx69 s d v0 v1 f))) and cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap (?d69 s d v0 v1 f) (?w69 s d v0 v1 f) (?sz69 s d v0 v1 f) (?idx69 s d v0 v1 f)) (?slot31 s d v0 v1 f) and excaps_in_mem extraCaps \<circ> ctes_of and (\<lambda>s. \<forall>v\<in>set extraCaps. \<forall>y\<in>zobj_refs' (fst v). ex_nonz_cap_to' y s) and (\<lambda>s. \<forall>v\<in>set extraCaps. valid_cap' (fst v) s) and sysargs_rel (?args31 s d v0 v1 f) buffer and (?P32 s d v0 v1 f and (?P37 s d v0 v1 f and (invs' and cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap (?d69 s d v0 v1 f) (?w69 s d v0 v1 f) (?sz69 s d v0 v1 f) (?idx69 s d v0 v1 f)) (?slot31 s d v0 v1 f) and sch_act_simple and (\<lambda>s. \<forall>x\<in>set (map fst extraCaps). valid_cap' x s) and (\<lambda>s. \<forall>x\<in>set (map fst extraCaps). \<forall>r\<in>cte_refs' x (irq_node' s). ex_cte_cap_wp_to' (\<lambda>_. True) r s))))) sa \<and> s' \<in> UNIV \<inter> \<lbrace>\<acute>invLabel = ?label31 s d v0 v1 f\<rbrace> \<inter> \<lbrace>unat \<acute>length___unsigned_long = length (?args31 s d v0 v1 f)\<rbrace> \<inter> \<lbrace>ccap_relation (capability.UntypedCap (?d69 s d v0 v1 f) (?w69 s d v0 v1 f) (?sz69 s d v0 v1 f) (?idx69 s d v0 v1 f)) \<acute>cap\<rbrace> \<inter> \<lbrace>\<acute>slot = cte_Ptr (?slot31 s d v0 v1 f)\<rbrace> \<inter> \<lbrace>\<acute>current_extra_caps = extraCaps'\<rbrace> \<inter> \<lbrace>\<acute>call = from_bool isCall\<rbrace> \<inter> \<lbrace>\<acute>buffer = option_to_ptr buffer\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>s d v0 v1 f uinv. \<lbrakk>interpret_excaps extraCaps' = excaps_map extraCaps; invs' s; thread = ksCurThread s; sch_act_simple s; ct_active' s; valid_cap' (capability.UntypedCap d v0 v1 f) s; cp = capability.UntypedCap d v0 v1 f; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d v0 v1 f) slot s; excaps_in_mem extraCaps (ctes_of s); \<forall>v\<in>set extraCaps. \<forall>y\<in>zobj_refs' (fst v). ex_nonz_cap_to' y s; \<forall>v\<in>set extraCaps. valid_cap' (fst v) s; sysargs_rel args buffer s\<rbrakk> \<Longrightarrow> monadic_rewrite (?F28 s d v0 v1 f) True (?P133 s d v0 v1 f) (?h79 s d v0 v1 f uinv) (do y <- return ();
returnOk uinv
od)
 2. \<And>s d v0 v1 f. \<lbrakk>interpret_excaps extraCaps' = excaps_map extraCaps; invs' s; thread = ksCurThread s; sch_act_simple s; ct_active' s; valid_cap' (capability.UntypedCap d v0 v1 f) s; cp = capability.UntypedCap d v0 v1 f; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d v0 v1 f) slot s; excaps_in_mem extraCaps (ctes_of s); \<forall>v\<in>set extraCaps. \<forall>y\<in>zobj_refs' (fst v). ex_nonz_cap_to' y s; \<forall>v\<in>set extraCaps. valid_cap' (fst v) s; sysargs_rel args buffer s\<rbrakk> \<Longrightarrow> monadic_rewrite (?F28 s d v0 v1 f) True (?P75 s d v0 v1 f) (?f35 s d v0 v1 f) (decodeUntypedInvocation (?label31 s d v0 v1 f) (?args31 s d v0 v1 f) (?slot31 s d v0 v1 f) (capability.UntypedCap (?d69 s d v0 v1 f) (?w69 s d v0 v1 f) (?sz69 s d v0 v1 f) (?idx69 s d v0 v1 f)) (map fst extraCaps) >>=E ?h79 s d v0 v1 f)
 3. \<And>s d v0 v1 f. \<lbrakk>interpret_excaps extraCaps' = excaps_map extraCaps; invs' s; thread = ksCurThread s; sch_act_simple s; ct_active' s; valid_cap' (capability.UntypedCap d v0 v1 f) s; cp = capability.UntypedCap d v0 v1 f; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d v0 v1 f) slot s; excaps_in_mem extraCaps (ctes_of s); \<forall>v\<in>set extraCaps. \<forall>y\<in>zobj_refs' (fst v). ex_nonz_cap_to' y s; \<forall>v\<in>set extraCaps. valid_cap' (fst v) s; sysargs_rel args buffer s\<rbrakk> \<Longrightarrow> monadic_rewrite (?F28 s d v0 v1 f) True (?P32 s d v0 v1 f) (decodeUntypedInvocation label args slot (capability.UntypedCap d v0 v1 f) (map fst extraCaps) >>= invocationCatch (ksCurThread s) isBlocking isCall Invocations_H.invocation.InvokeUntyped) (?f35 s d v0 v1 f >>= invocationCatch (?thread31 s d v0 v1 f) isBlocking isCall Invocations_H.invocation.InvokeUntyped)
 4. \<And>s d v0 v1 f sa s'. \<lbrakk>interpret_excaps extraCaps' = excaps_map extraCaps; invs' s; thread = ksCurThread s; sch_act_simple s; ct_active' s; valid_cap' (capability.UntypedCap d v0 v1 f) s; cp = capability.UntypedCap d v0 v1 f; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d v0 v1 f) slot s; excaps_in_mem extraCaps (ctes_of s); \<forall>v\<in>set extraCaps. \<forall>y\<in>zobj_refs' (fst v). ex_nonz_cap_to' y s; \<forall>v\<in>set extraCaps. valid_cap' (fst v) s; sysargs_rel args buffer s; (sa, s') \<in> rf_sr; sa = s; s' \<in> \<lbrace>\<acute>invLabel = label\<rbrace> \<inter> \<lbrace>unat \<acute>length___unsigned_long = length args\<rbrace> \<inter> \<lbrace>ccap_relation (capability.UntypedCap d v0 v1 f) \<acute>cap\<rbrace> \<inter> \<lbrace>\<acute>slot = cte_Ptr slot\<rbrace> \<inter> \<lbrace>\<acute>current_extra_caps = extraCaps'\<rbrace> \<inter> \<lbrace>\<acute>call = from_bool isCall\<rbrace> \<inter> \<lbrace>\<acute>buffer = option_to_ptr buffer\<rbrace>\<rbrakk> \<Longrightarrow> (invs' and (\<lambda>sa. ksCurThread sa = ?thread31 s d v0 v1 f) and sch_act_simple and ct_active' and valid_cap' (capability.UntypedCap (?d69 s d v0 v1 f) (?w69 s d v0 v1 f) (?sz69 s d v0 v1 f) (?idx69 s d v0 v1 f)) and K (isUntypedCap (capability.UntypedCap (?d69 s d v0 v1 f) (?w69 s d v0 v1 f) (?sz69 s d v0 v1 f) (?idx69 s d v0 v1 f))) and cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap (?d69 s d v0 v1 f) (?w69 s d v0 v1 f) (?sz69 s d v0 v1 f) (?idx69 s d v0 v1 f)) (?slot31 s d v0 v1 f) and excaps_in_mem extraCaps \<circ> ctes_of and (\<lambda>s. \<forall>v\<in>set extraCaps. \<forall>y\<in>zobj_refs' (fst v). ex_nonz_cap_to' y s) and (\<lambda>s. \<forall>v\<in>set extraCaps. valid_cap' (fst v) s) and sysargs_rel (?args31 s d v0 v1 f) buffer and (?P32 s d v0 v1 f and (?P75 s d v0 v1 f and (?P133 s d v0 v1 f and (\<lambda>_. True)) and (invs' and cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap (?d69 s d v0 v1 f) (?w69 s d v0 v1 f) (?sz69 s d v0 v1 f) (?idx69 s d v0 v1 f)) (?slot31 s d v0 v1 f) and sch_act_simple and (\<lambda>s. \<forall>x\<in>set (map fst extraCaps). valid_cap' x s) and (\<lambda>s. \<forall>x\<in>set (map fst extraCaps). \<forall>r\<in>cte_refs' x (irq_node' s). ex_cte_cap_wp_to' (\<lambda>_. True) r s))))) sa \<and> s' \<in> UNIV \<inter> \<lbrace>\<acute>invLabel = ?label31 s d v0 v1 f\<rbrace> \<inter> \<lbrace>unat \<acute>length___unsigned_long = length (?args31 s d v0 v1 f)\<rbrace> \<inter> \<lbrace>ccap_relation (capability.UntypedCap (?d69 s d v0 v1 f) (?w69 s d v0 v1 f) (?sz69 s d v0 v1 f) (?idx69 s d v0 v1 f)) \<acute>cap\<rbrace> \<inter> \<lbrace>\<acute>slot = cte_Ptr (?slot31 s d v0 v1 f)\<rbrace> \<inter> \<lbrace>\<acute>current_extra_caps = extraCaps'\<rbrace> \<inter> \<lbrace>\<acute>call = from_bool isCall\<rbrace> \<inter> \<lbrace>\<acute>buffer = option_to_ptr buffer\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s d v0 v1 f. \<lbrakk>interpret_excaps extraCaps' = excaps_map extraCaps; invs' s; thread = ksCurThread s; sch_act_simple s; ct_active' s; valid_cap' (capability.UntypedCap d v0 v1 f) s; cp = capability.UntypedCap d v0 v1 f; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d v0 v1 f) slot s; excaps_in_mem extraCaps (ctes_of s); \<forall>v\<in>set extraCaps. \<forall>y\<in>zobj_refs' (fst v). ex_nonz_cap_to' y s; \<forall>v\<in>set extraCaps. valid_cap' (fst v) s; sysargs_rel args buffer s\<rbrakk> \<Longrightarrow> monadic_rewrite (?F28 s d v0 v1 f) True (?P75 s d v0 v1 f) (?f35 s d v0 v1 f) (doE uinv <- decodeUntypedInvocation (?label31 s d v0 v1 f) (?args31 s d v0 v1 f) (?slot31 s d v0 v1 f) (capability.UntypedCap (?d69 s d v0 v1 f) (?w69 s d v0 v1 f) (?sz69 s d v0 v1 f) (?idx69 s d v0 v1 f)) (map fst extraCaps);
do y <- return ();
returnOk uinv
od
odE)
 2. \<And>s d v0 v1 f. \<lbrakk>interpret_excaps extraCaps' = excaps_map extraCaps; invs' s; thread = ksCurThread s; sch_act_simple s; ct_active' s; valid_cap' (capability.UntypedCap d v0 v1 f) s; cp = capability.UntypedCap d v0 v1 f; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d v0 v1 f) slot s; excaps_in_mem extraCaps (ctes_of s); \<forall>v\<in>set extraCaps. \<forall>y\<in>zobj_refs' (fst v). ex_nonz_cap_to' y s; \<forall>v\<in>set extraCaps. valid_cap' (fst v) s; sysargs_rel args buffer s\<rbrakk> \<Longrightarrow> monadic_rewrite (?F28 s d v0 v1 f) True (?P32 s d v0 v1 f) (decodeUntypedInvocation label args slot (capability.UntypedCap d v0 v1 f) (map fst extraCaps) >>= invocationCatch (ksCurThread s) isBlocking isCall Invocations_H.invocation.InvokeUntyped) (?f35 s d v0 v1 f >>= invocationCatch (?thread31 s d v0 v1 f) isBlocking isCall Invocations_H.invocation.InvokeUntyped)
 3. \<And>s d v0 v1 f sa s'. \<lbrakk>interpret_excaps extraCaps' = excaps_map extraCaps; invs' s; thread = ksCurThread s; sch_act_simple s; ct_active' s; valid_cap' (capability.UntypedCap d v0 v1 f) s; cp = capability.UntypedCap d v0 v1 f; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d v0 v1 f) slot s; excaps_in_mem extraCaps (ctes_of s); \<forall>v\<in>set extraCaps. \<forall>y\<in>zobj_refs' (fst v). ex_nonz_cap_to' y s; \<forall>v\<in>set extraCaps. valid_cap' (fst v) s; sysargs_rel args buffer s; (sa, s') \<in> rf_sr; sa = s; s' \<in> \<lbrace>\<acute>invLabel = label\<rbrace> \<inter> \<lbrace>unat \<acute>length___unsigned_long = length args\<rbrace> \<inter> \<lbrace>ccap_relation (capability.UntypedCap d v0 v1 f) \<acute>cap\<rbrace> \<inter> \<lbrace>\<acute>slot = cte_Ptr slot\<rbrace> \<inter> \<lbrace>\<acute>current_extra_caps = extraCaps'\<rbrace> \<inter> \<lbrace>\<acute>call = from_bool isCall\<rbrace> \<inter> \<lbrace>\<acute>buffer = option_to_ptr buffer\<rbrace>\<rbrakk> \<Longrightarrow> (invs' and (\<lambda>sa. ksCurThread sa = ?thread31 s d v0 v1 f) and sch_act_simple and ct_active' and valid_cap' (capability.UntypedCap (?d69 s d v0 v1 f) (?w69 s d v0 v1 f) (?sz69 s d v0 v1 f) (?idx69 s d v0 v1 f)) and K (isUntypedCap (capability.UntypedCap (?d69 s d v0 v1 f) (?w69 s d v0 v1 f) (?sz69 s d v0 v1 f) (?idx69 s d v0 v1 f))) and cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap (?d69 s d v0 v1 f) (?w69 s d v0 v1 f) (?sz69 s d v0 v1 f) (?idx69 s d v0 v1 f)) (?slot31 s d v0 v1 f) and excaps_in_mem extraCaps \<circ> ctes_of and (\<lambda>s. \<forall>v\<in>set extraCaps. \<forall>y\<in>zobj_refs' (fst v). ex_nonz_cap_to' y s) and (\<lambda>s. \<forall>v\<in>set extraCaps. valid_cap' (fst v) s) and sysargs_rel (?args31 s d v0 v1 f) buffer and (?P32 s d v0 v1 f and (?P75 s d v0 v1 f and ((\<lambda>_. True) and (\<lambda>_. True)) and (invs' and cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap (?d69 s d v0 v1 f) (?w69 s d v0 v1 f) (?sz69 s d v0 v1 f) (?idx69 s d v0 v1 f)) (?slot31 s d v0 v1 f) and sch_act_simple and (\<lambda>s. \<forall>x\<in>set (map fst extraCaps). valid_cap' x s) and (\<lambda>s. \<forall>x\<in>set (map fst extraCaps). \<forall>r\<in>cte_refs' x (irq_node' s). ex_cte_cap_wp_to' (\<lambda>_. True) r s))))) sa \<and> s' \<in> UNIV \<inter> \<lbrace>\<acute>invLabel = ?label31 s d v0 v1 f\<rbrace> \<inter> \<lbrace>unat \<acute>length___unsigned_long = length (?args31 s d v0 v1 f)\<rbrace> \<inter> \<lbrace>ccap_relation (capability.UntypedCap (?d69 s d v0 v1 f) (?w69 s d v0 v1 f) (?sz69 s d v0 v1 f) (?idx69 s d v0 v1 f)) \<acute>cap\<rbrace> \<inter> \<lbrace>\<acute>slot = cte_Ptr (?slot31 s d v0 v1 f)\<rbrace> \<inter> \<lbrace>\<acute>current_extra_caps = extraCaps'\<rbrace> \<inter> \<lbrace>\<acute>call = from_bool isCall\<rbrace> \<inter> \<lbrace>\<acute>buffer = option_to_ptr buffer\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s d v0 v1 f. \<lbrakk>interpret_excaps extraCaps' = excaps_map extraCaps; invs' s; thread = ksCurThread s; sch_act_simple s; ct_active' s; valid_cap' (capability.UntypedCap d v0 v1 f) s; cp = capability.UntypedCap d v0 v1 f; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d v0 v1 f) slot s; excaps_in_mem extraCaps (ctes_of s); \<forall>v\<in>set extraCaps. \<forall>y\<in>zobj_refs' (fst v). ex_nonz_cap_to' y s; \<forall>v\<in>set extraCaps. valid_cap' (fst v) s; sysargs_rel args buffer s\<rbrakk> \<Longrightarrow> monadic_rewrite (?F28 s d v0 v1 f) True (?P75 s d v0 v1 f) (?f35 s d v0 v1 f) (decodeUntypedInvocation (?label31 s d v0 v1 f) (?args31 s d v0 v1 f) (?slot31 s d v0 v1 f) (capability.UntypedCap (?d69 s d v0 v1 f) (?w69 s d v0 v1 f) (?sz69 s d v0 v1 f) (?idx69 s d v0 v1 f)) (map fst extraCaps))
 2. \<And>s d v0 v1 f. \<lbrakk>interpret_excaps extraCaps' = excaps_map extraCaps; invs' s; thread = ksCurThread s; sch_act_simple s; ct_active' s; valid_cap' (capability.UntypedCap d v0 v1 f) s; cp = capability.UntypedCap d v0 v1 f; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d v0 v1 f) slot s; excaps_in_mem extraCaps (ctes_of s); \<forall>v\<in>set extraCaps. \<forall>y\<in>zobj_refs' (fst v). ex_nonz_cap_to' y s; \<forall>v\<in>set extraCaps. valid_cap' (fst v) s; sysargs_rel args buffer s\<rbrakk> \<Longrightarrow> monadic_rewrite (?F28 s d v0 v1 f) True (?P32 s d v0 v1 f) (decodeUntypedInvocation label args slot (capability.UntypedCap d v0 v1 f) (map fst extraCaps) >>= invocationCatch (ksCurThread s) isBlocking isCall Invocations_H.invocation.InvokeUntyped) (?f35 s d v0 v1 f >>= invocationCatch (?thread31 s d v0 v1 f) isBlocking isCall Invocations_H.invocation.InvokeUntyped)
 3. \<And>s d v0 v1 f sa s'. \<lbrakk>interpret_excaps extraCaps' = excaps_map extraCaps; invs' s; thread = ksCurThread s; sch_act_simple s; ct_active' s; valid_cap' (capability.UntypedCap d v0 v1 f) s; cp = capability.UntypedCap d v0 v1 f; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d v0 v1 f) slot s; excaps_in_mem extraCaps (ctes_of s); \<forall>v\<in>set extraCaps. \<forall>y\<in>zobj_refs' (fst v). ex_nonz_cap_to' y s; \<forall>v\<in>set extraCaps. valid_cap' (fst v) s; sysargs_rel args buffer s; (sa, s') \<in> rf_sr; sa = s; s' \<in> \<lbrace>\<acute>invLabel = label\<rbrace> \<inter> \<lbrace>unat \<acute>length___unsigned_long = length args\<rbrace> \<inter> \<lbrace>ccap_relation (capability.UntypedCap d v0 v1 f) \<acute>cap\<rbrace> \<inter> \<lbrace>\<acute>slot = cte_Ptr slot\<rbrace> \<inter> \<lbrace>\<acute>current_extra_caps = extraCaps'\<rbrace> \<inter> \<lbrace>\<acute>call = from_bool isCall\<rbrace> \<inter> \<lbrace>\<acute>buffer = option_to_ptr buffer\<rbrace>\<rbrakk> \<Longrightarrow> (invs' and (\<lambda>sa. ksCurThread sa = ?thread31 s d v0 v1 f) and sch_act_simple and ct_active' and valid_cap' (capability.UntypedCap (?d69 s d v0 v1 f) (?w69 s d v0 v1 f) (?sz69 s d v0 v1 f) (?idx69 s d v0 v1 f)) and K (isUntypedCap (capability.UntypedCap (?d69 s d v0 v1 f) (?w69 s d v0 v1 f) (?sz69 s d v0 v1 f) (?idx69 s d v0 v1 f))) and cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap (?d69 s d v0 v1 f) (?w69 s d v0 v1 f) (?sz69 s d v0 v1 f) (?idx69 s d v0 v1 f)) (?slot31 s d v0 v1 f) and excaps_in_mem extraCaps \<circ> ctes_of and (\<lambda>s. \<forall>v\<in>set extraCaps. \<forall>y\<in>zobj_refs' (fst v). ex_nonz_cap_to' y s) and (\<lambda>s. \<forall>v\<in>set extraCaps. valid_cap' (fst v) s) and sysargs_rel (?args31 s d v0 v1 f) buffer and (?P32 s d v0 v1 f and (?P75 s d v0 v1 f and ((\<lambda>_. True) and (\<lambda>_. True)) and (invs' and cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap (?d69 s d v0 v1 f) (?w69 s d v0 v1 f) (?sz69 s d v0 v1 f) (?idx69 s d v0 v1 f)) (?slot31 s d v0 v1 f) and sch_act_simple and (\<lambda>s. \<forall>x\<in>set (map fst extraCaps). valid_cap' x s) and (\<lambda>s. \<forall>x\<in>set (map fst extraCaps). \<forall>r\<in>cte_refs' x (irq_node' s). ex_cte_cap_wp_to' (\<lambda>_. True) r s))))) sa \<and> s' \<in> UNIV \<inter> \<lbrace>\<acute>invLabel = ?label31 s d v0 v1 f\<rbrace> \<inter> \<lbrace>unat \<acute>length___unsigned_long = length (?args31 s d v0 v1 f)\<rbrace> \<inter> \<lbrace>ccap_relation (capability.UntypedCap (?d69 s d v0 v1 f) (?w69 s d v0 v1 f) (?sz69 s d v0 v1 f) (?idx69 s d v0 v1 f)) \<acute>cap\<rbrace> \<inter> \<lbrace>\<acute>slot = cte_Ptr (?slot31 s d v0 v1 f)\<rbrace> \<inter> \<lbrace>\<acute>current_extra_caps = extraCaps'\<rbrace> \<inter> \<lbrace>\<acute>call = from_bool isCall\<rbrace> \<inter> \<lbrace>\<acute>buffer = option_to_ptr buffer\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s d v0 v1 f. \<lbrakk>interpret_excaps extraCaps' = excaps_map extraCaps; invs' s; thread = ksCurThread s; sch_act_simple s; ct_active' s; valid_cap' (capability.UntypedCap d v0 v1 f) s; cp = capability.UntypedCap d v0 v1 f; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d v0 v1 f) slot s; excaps_in_mem extraCaps (ctes_of s); \<forall>v\<in>set extraCaps. \<forall>y\<in>zobj_refs' (fst v). ex_nonz_cap_to' y s; \<forall>v\<in>set extraCaps. valid_cap' (fst v) s; sysargs_rel args buffer s\<rbrakk> \<Longrightarrow> monadic_rewrite (?F28 s d v0 v1 f) True (?P32 s d v0 v1 f) (decodeUntypedInvocation label args slot (capability.UntypedCap d v0 v1 f) (map fst extraCaps) >>= invocationCatch (ksCurThread s) isBlocking isCall Invocations_H.invocation.InvokeUntyped) (decodeUntypedInvocation (?label31 s d v0 v1 f) (?args31 s d v0 v1 f) (?slot31 s d v0 v1 f) (capability.UntypedCap (?d69 s d v0 v1 f) (?w69 s d v0 v1 f) (?sz69 s d v0 v1 f) (?idx69 s d v0 v1 f)) (map fst extraCaps) >>= invocationCatch (?thread31 s d v0 v1 f) isBlocking isCall Invocations_H.invocation.InvokeUntyped)
 2. \<And>s d v0 v1 f sa s'. \<lbrakk>interpret_excaps extraCaps' = excaps_map extraCaps; invs' s; thread = ksCurThread s; sch_act_simple s; ct_active' s; valid_cap' (capability.UntypedCap d v0 v1 f) s; cp = capability.UntypedCap d v0 v1 f; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d v0 v1 f) slot s; excaps_in_mem extraCaps (ctes_of s); \<forall>v\<in>set extraCaps. \<forall>y\<in>zobj_refs' (fst v). ex_nonz_cap_to' y s; \<forall>v\<in>set extraCaps. valid_cap' (fst v) s; sysargs_rel args buffer s; (sa, s') \<in> rf_sr; sa = s; s' \<in> \<lbrace>\<acute>invLabel = label\<rbrace> \<inter> \<lbrace>unat \<acute>length___unsigned_long = length args\<rbrace> \<inter> \<lbrace>ccap_relation (capability.UntypedCap d v0 v1 f) \<acute>cap\<rbrace> \<inter> \<lbrace>\<acute>slot = cte_Ptr slot\<rbrace> \<inter> \<lbrace>\<acute>current_extra_caps = extraCaps'\<rbrace> \<inter> \<lbrace>\<acute>call = from_bool isCall\<rbrace> \<inter> \<lbrace>\<acute>buffer = option_to_ptr buffer\<rbrace>\<rbrakk> \<Longrightarrow> (invs' and (\<lambda>sa. ksCurThread sa = ?thread31 s d v0 v1 f) and sch_act_simple and ct_active' and valid_cap' (capability.UntypedCap (?d69 s d v0 v1 f) (?w69 s d v0 v1 f) (?sz69 s d v0 v1 f) (?idx69 s d v0 v1 f)) and K (isUntypedCap (capability.UntypedCap (?d69 s d v0 v1 f) (?w69 s d v0 v1 f) (?sz69 s d v0 v1 f) (?idx69 s d v0 v1 f))) and cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap (?d69 s d v0 v1 f) (?w69 s d v0 v1 f) (?sz69 s d v0 v1 f) (?idx69 s d v0 v1 f)) (?slot31 s d v0 v1 f) and excaps_in_mem extraCaps \<circ> ctes_of and (\<lambda>s. \<forall>v\<in>set extraCaps. \<forall>y\<in>zobj_refs' (fst v). ex_nonz_cap_to' y s) and (\<lambda>s. \<forall>v\<in>set extraCaps. valid_cap' (fst v) s) and sysargs_rel (?args31 s d v0 v1 f) buffer and (?P32 s d v0 v1 f and ((\<lambda>_. True) and ((\<lambda>_. True) and (\<lambda>_. True)) and (invs' and cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap (?d69 s d v0 v1 f) (?w69 s d v0 v1 f) (?sz69 s d v0 v1 f) (?idx69 s d v0 v1 f)) (?slot31 s d v0 v1 f) and sch_act_simple and (\<lambda>s. \<forall>x\<in>set (map fst extraCaps). valid_cap' x s) and (\<lambda>s. \<forall>x\<in>set (map fst extraCaps). \<forall>r\<in>cte_refs' x (irq_node' s). ex_cte_cap_wp_to' (\<lambda>_. True) r s))))) sa \<and> s' \<in> UNIV \<inter> \<lbrace>\<acute>invLabel = ?label31 s d v0 v1 f\<rbrace> \<inter> \<lbrace>unat \<acute>length___unsigned_long = length (?args31 s d v0 v1 f)\<rbrace> \<inter> \<lbrace>ccap_relation (capability.UntypedCap (?d69 s d v0 v1 f) (?w69 s d v0 v1 f) (?sz69 s d v0 v1 f) (?idx69 s d v0 v1 f)) \<acute>cap\<rbrace> \<inter> \<lbrace>\<acute>slot = cte_Ptr (?slot31 s d v0 v1 f)\<rbrace> \<inter> \<lbrace>\<acute>current_extra_caps = extraCaps'\<rbrace> \<inter> \<lbrace>\<acute>call = from_bool isCall\<rbrace> \<inter> \<lbrace>\<acute>buffer = option_to_ptr buffer\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s d v0 v1 f sa s'. \<lbrakk>interpret_excaps extraCaps' = excaps_map extraCaps; invs' s; thread = ksCurThread s; sch_act_simple s; ct_active' s; valid_cap' (capability.UntypedCap d v0 v1 f) s; cp = capability.UntypedCap d v0 v1 f; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d v0 v1 f) slot s; excaps_in_mem extraCaps (ctes_of s); \<forall>v\<in>set extraCaps. \<forall>y\<in>zobj_refs' (fst v). ex_nonz_cap_to' y s; \<forall>v\<in>set extraCaps. valid_cap' (fst v) s; sysargs_rel args buffer s; (sa, s') \<in> rf_sr; sa = s; s' \<in> \<lbrace>\<acute>invLabel = label\<rbrace> \<inter> \<lbrace>unat \<acute>length___unsigned_long = length args\<rbrace> \<inter> \<lbrace>ccap_relation (capability.UntypedCap d v0 v1 f) \<acute>cap\<rbrace> \<inter> \<lbrace>\<acute>slot = cte_Ptr slot\<rbrace> \<inter> \<lbrace>\<acute>current_extra_caps = extraCaps'\<rbrace> \<inter> \<lbrace>\<acute>call = from_bool isCall\<rbrace> \<inter> \<lbrace>\<acute>buffer = option_to_ptr buffer\<rbrace>\<rbrakk> \<Longrightarrow> (invs' and (\<lambda>sa. ksCurThread sa = ksCurThread s) and sch_act_simple and ct_active' and valid_cap' (capability.UntypedCap d v0 v1 f) and K (isUntypedCap (capability.UntypedCap d v0 v1 f)) and cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d v0 v1 f) slot and excaps_in_mem extraCaps \<circ> ctes_of and (\<lambda>s. \<forall>v\<in>set extraCaps. \<forall>y\<in>zobj_refs' (fst v). ex_nonz_cap_to' y s) and (\<lambda>s. \<forall>v\<in>set extraCaps. valid_cap' (fst v) s) and sysargs_rel args buffer and ((\<lambda>_. True) and ((\<lambda>_. True) and ((\<lambda>_. True) and (\<lambda>_. True)) and (invs' and cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d v0 v1 f) slot and sch_act_simple and (\<lambda>s. \<forall>x\<in>set (map fst extraCaps). valid_cap' x s) and (\<lambda>s. \<forall>x\<in>set (map fst extraCaps). \<forall>r\<in>cte_refs' x (irq_node' s). ex_cte_cap_wp_to' (\<lambda>_. True) r s))))) sa \<and> s' \<in> UNIV \<inter> \<lbrace>\<acute>invLabel = label\<rbrace> \<inter> \<lbrace>unat \<acute>length___unsigned_long = length args\<rbrace> \<inter> \<lbrace>ccap_relation (capability.UntypedCap d v0 v1 f) \<acute>cap\<rbrace> \<inter> \<lbrace>\<acute>slot = cte_Ptr slot\<rbrace> \<inter> \<lbrace>\<acute>current_extra_caps = extraCaps'\<rbrace> \<inter> \<lbrace>\<acute>call = from_bool isCall\<rbrace> \<inter> \<lbrace>\<acute>buffer = option_to_ptr buffer\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s d v0 v1 f s' a b r. \<lbrakk>interpret_excaps (current_extra_caps_' (globals s')) = excaps_map extraCaps; invs' s; thread = ksCurThread s; sch_act_simple s; ct_active' s; valid_cap' (capability.UntypedCap d v0 v1 f) s; cp = capability.UntypedCap d v0 v1 f; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d v0 v1 f) slot s; \<forall>x\<in>set extraCaps. case x of (cp, slot) \<Rightarrow> slotcap_in_mem cp slot (ctes_of s); \<forall>v\<in>set extraCaps. \<forall>y\<in>zobj_refs' (fst v). ex_nonz_cap_to' y s; \<forall>v\<in>set extraCaps. valid_cap' (fst v) s; sysargs_rel args buffer s; (s, s') \<in> rf_sr; (a, b) \<in> set extraCaps; r \<in> cte_refs' a (irq_node' s); label = invLabel_' s'; unat (length___unsigned_long_' s') = length args; ccap_relation (capability.UntypedCap d v0 v1 f) (cap_' s'); slot_' s' = cte_Ptr slot; extraCaps' = current_extra_caps_' (globals s'); call_' s' = from_bool isCall; buffer_' s' = option_to_ptr buffer\<rbrakk> \<Longrightarrow> \<exists>cref. cte_wp_at' (\<lambda>c. r \<in> cte_refs' (cteCap c) (irq_node' s)) cref s proof (prove)
goal (1 subgoal):
 1. \<And>s d v0 v1 f s' a b r. \<lbrakk>interpret_excaps (current_extra_caps_' (globals s')) = excaps_map extraCaps; invs' s; thread = ksCurThread s; sch_act_simple s; ct_active' s; valid_cap' (capability.UntypedCap d v0 v1 f) s; cp = capability.UntypedCap d v0 v1 f; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d v0 v1 f) slot s; sysargs_rel args buffer s; (s, s') \<in> rf_sr; (a, b) \<in> set extraCaps; r \<in> cte_refs' a (irq_node' s); label = invLabel_' s'; unat (length___unsigned_long_' s') = length args; ccap_relation (capability.UntypedCap d v0 v1 f) (cap_' s'); slot_' s' = cte_Ptr slot; extraCaps' = current_extra_caps_' (globals s'); call_' s' = from_bool isCall; buffer_' s' = option_to_ptr buffer; case (a, b) of (cp, slot) \<Rightarrow> slotcap_in_mem cp slot (ctes_of s); \<forall>y\<in>zobj_refs' (fst (a, b)). ex_nonz_cap_to' y s; valid_cap' (fst (a, b)) s\<rbrakk> \<Longrightarrow> \<exists>cref. cte_wp_at' (\<lambda>c. r \<in> cte_refs' (cteCap c) (irq_node' s)) cref s proof (prove)
goal (1 subgoal):
 1. \<And>s d v0 v1 f s' a b r. \<lbrakk>interpret_excaps (current_extra_caps_' (globals s')) = excaps_map extraCaps; invs' s; thread = ksCurThread s; sch_act_simple s; ct_active' s; valid_cap' (capability.UntypedCap d v0 v1 f) s; cp = capability.UntypedCap d v0 v1 f; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d v0 v1 f) slot s; sysargs_rel args buffer s; (s, s') \<in> rf_sr; (a, b) \<in> set extraCaps; r \<in> cte_refs' a (irq_node' s); label = invLabel_' s'; unat (length___unsigned_long_' s') = length args; ccap_relation (capability.UntypedCap d v0 v1 f) (cap_' s'); slot_' s' = cte_Ptr slot; extraCaps' = current_extra_caps_' (globals s'); call_' s' = from_bool isCall; buffer_' s' = option_to_ptr buffer; case (a, b) of (cp, slot) \<Rightarrow> slotcap_in_mem cp slot (ctes_of s); \<forall>y\<in>zobj_refs' (fst (a, b)). ex_nonz_cap_to' y s; valid_cap' (fst (a, b)) s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>c. r \<in> cte_refs' (cteCap c) (irq_node' s)) b s proof (prove)
goal:
No subgoals!