kings-crown/FVELER_Isabelle huggingface dataset:
theory Invoke_C

lemma alignUp_spec:
  "\<forall>s. \<Gamma>\<turnstile> \<lbrace>s. alignment_' s < 0x20 \<rbrace> Call alignUp_'proc
         \<lbrace>\<acute>ret__unsigned_long = alignUp (baseValue_' s) (unat (alignment_' s))\<rbrace>" apply vcg apply (simp add:alignUp_def2 mask_def field_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> \<lbrace>s. \<^bsup>s\<^esup>alignment < 0x20\<rbrace> Call alignUp_'proc \<lbrace>\<acute>ret__unsigned_long = Untyped_H.alignUp \<^bsup>s\<^esup>baseValue (unat \<^bsup>s\<^esup>alignment)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>baseValue alignment. alignment < 0x20 \<Longrightarrow> alignment < SCAST(32 signed \<rightarrow> 32) 0x20 \<and> baseValue + ((1 << unat alignment) - SCAST(32 signed \<rightarrow> 32) 1) && ~~ ((1 << unat alignment) - 1) = Untyped_H.alignUp baseValue (unat alignment) proof (prove)
goal:
No subgoals!
theory Invoke_C

lemma ccap_relation_untyped_CL_simps:
  "\<lbrakk>ccap_relation cp cap;isUntypedCap cp\<rbrakk>
   \<Longrightarrow> unat (capBlockSize_CL (cap_untyped_cap_lift cap)) = (capBlockSize cp)
       \<and> (capPtr_CL (cap_untyped_cap_lift cap)) = (capPtr cp)" apply (frule cap_get_tag_UntypedCap) apply (simp add:cap_get_tag_isCap) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccap_relation cp cap; isUntypedCap cp\<rbrakk> \<Longrightarrow> unat (capBlockSize_CL (cap_untyped_cap_lift cap)) = capBlockSize cp \<and> capPtr_CL (cap_untyped_cap_lift cap) = capPtr cp proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccap_relation cp cap; isUntypedCap cp; (cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap) = (cp = capability.UntypedCap (to_bool (capIsDevice_CL (cap_untyped_cap_lift cap))) (capPtr_CL (cap_untyped_cap_lift cap)) (unat (capBlockSize_CL (cap_untyped_cap_lift cap))) (unat (capFreeIndex_CL (cap_untyped_cap_lift cap) << 4)))\<rbrakk> \<Longrightarrow> unat (capBlockSize_CL (cap_untyped_cap_lift cap)) = capBlockSize cp \<and> capPtr_CL (cap_untyped_cap_lift cap) = capPtr cp proof (prove)
goal:
No subgoals!
theory Invoke_C

lemma valid_untyped_capBlockSize_misc:
  "\<lbrakk>s \<turnstile>' cp; isUntypedCap cp; (z::nat) \<le> capFreeIndex cp
   \<rbrakk> \<Longrightarrow> 2 ^ capBlockSize cp - z < 2 ^ word_bits
    \<and> of_nat (2^capBlockSize cp - z) = (2::word32) ^ capBlockSize cp - of_nat z" apply (clarsimp simp: valid_cap'_def isCap_simps untypedBits_defs) apply (rule le_less_trans[OF diff_le_self]) apply (rule power_strict_increasing) apply (simp add:word_bits_def) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_cap' cp s; isUntypedCap cp; z \<le> capFreeIndex cp\<rbrakk> \<Longrightarrow> 2 ^ capBlockSize cp - z < 2 ^ word_bits \<and> word_of_nat (2 ^ capBlockSize cp - z) = 2 ^ capBlockSize cp - word_of_nat z proof (prove)
goal (1 subgoal):
 1. \<And>d v0 v1 f. \<lbrakk>z \<le> f; cp = capability.UntypedCap d v0 v1 f; capAligned (capability.UntypedCap d v0 v1 f); valid_untyped' d v0 v1 f s; v0 \<noteq> 0; 4 \<le> v1; v1 \<le> 29; f \<le> 2 ^ v1; is_aligned (word_of_nat f) 4\<rbrakk> \<Longrightarrow> 2 ^ v1 - z < 2 ^ word_bits proof (prove)
goal (1 subgoal):
 1. \<And>d v0 v1 f. \<lbrakk>z \<le> f; cp = capability.UntypedCap d v0 v1 f; capAligned (capability.UntypedCap d v0 v1 f); valid_untyped' d v0 v1 f s; v0 \<noteq> 0; 4 \<le> v1; v1 \<le> 29; f \<le> 2 ^ v1; is_aligned (word_of_nat f) 4\<rbrakk> \<Longrightarrow> 2 ^ v1 < 2 ^ word_bits proof (prove)
goal (2 subgoals):
 1. \<And>d v0 v1 f. \<lbrakk>z \<le> f; cp = capability.UntypedCap d v0 v1 f; capAligned (capability.UntypedCap d v0 v1 f); valid_untyped' d v0 v1 f s; v0 \<noteq> 0; 4 \<le> v1; v1 \<le> 29; f \<le> 2 ^ v1; is_aligned (word_of_nat f) 4\<rbrakk> \<Longrightarrow> v1 < word_bits
 2. \<And>d v0 v1 f. \<lbrakk>z \<le> f; cp = capability.UntypedCap d v0 v1 f; capAligned (capability.UntypedCap d v0 v1 f); valid_untyped' d v0 v1 f s; v0 \<noteq> 0; 4 \<le> v1; v1 \<le> 29; f \<le> 2 ^ v1; is_aligned (word_of_nat f) 4\<rbrakk> \<Longrightarrow> 1 < 2 proof (prove)
goal (1 subgoal):
 1. \<And>d v0 v1 f. \<lbrakk>z \<le> f; cp = capability.UntypedCap d v0 v1 f; capAligned (capability.UntypedCap d v0 v1 f); valid_untyped' d v0 v1 f s; v0 \<noteq> 0; 4 \<le> v1; v1 \<le> 29; f \<le> 2 ^ v1; is_aligned (word_of_nat f) 4\<rbrakk> \<Longrightarrow> 1 < 2 proof (prove)
goal:
No subgoals!
theory Invoke_C

lemma setThreadStateRestart_ct_active':
  "\<lbrace>ct_active'\<rbrace> setThreadState Restart thread
  \<lbrace>\<lambda>rva s. ct_active' s\<rbrace>" apply (simp add:ct_in_state'_def) apply (rule hoare_pre) apply (wps) apply (wp sts_st_tcb_at'_cases) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_active'\<rbrace> setThreadState Structures_H.thread_state.Restart thread \<lbrace>\<lambda>rva. ct_active'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. st_tcb_at' active' (ksCurThread s) s\<rbrace> setThreadState Structures_H.thread_state.Restart thread \<lbrace>\<lambda>rva s. st_tcb_at' active' (ksCurThread s) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> setThreadState Structures_H.thread_state.Restart thread \<lbrace>\<lambda>rva s. st_tcb_at' active' (ksCurThread s) s\<rbrace>
 2. \<And>s. st_tcb_at' active' (ksCurThread s) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<And>prev_s. \<lbrace>?P3 prev_s\<rbrace> setThreadState Structures_H.thread_state.Restart thread \<lbrace>\<lambda>rv. st_tcb_at' active' (ksCurThread prev_s)\<rbrace>
 2. \<And>s. st_tcb_at' active' (ksCurThread s) s \<Longrightarrow> ?P3 s s proof (prove)
goal (1 subgoal):
 1. \<And>s. st_tcb_at' active' (ksCurThread s) s \<Longrightarrow> (thread = ksCurThread s \<longrightarrow> active' Structures_H.thread_state.Restart \<and> tcb_at' (ksCurThread s) s) \<and> (thread \<noteq> ksCurThread s \<longrightarrow> st_tcb_at' active' (ksCurThread s) s) proof (prove)
goal:
No subgoals!
theory Invoke_C

lemma unat_of_nat_APIType_capBits:
  "b \<le> 32
  \<Longrightarrow> unat (of_nat (APIType_capBits z b) ::word32) = APIType_capBits z b" apply (rule unat_of_nat32) apply (case_tac z) apply (clarsimp simp:invokeUntyped_proofs_def word_bits_conv APIType_capBits_def objBits_simps'
    split: apiobject_type.splits)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. b \<le> 32 \<Longrightarrow> unat (word_of_nat (APIType_capBits z b)) = APIType_capBits z b proof (prove)
goal (1 subgoal):
 1. b \<le> 32 \<Longrightarrow> APIType_capBits z b < 2 ^ word_bits proof (prove)
goal (7 subgoals):
 1. \<And>x1. \<lbrakk>b \<le> 32; z = APIObjectType x1\<rbrakk> \<Longrightarrow> APIType_capBits z b < 2 ^ word_bits
 2. \<lbrakk>b \<le> 32; z = object_type.SmallPageObject\<rbrakk> \<Longrightarrow> APIType_capBits z b < 2 ^ word_bits
 3. \<lbrakk>b \<le> 32; z = object_type.LargePageObject\<rbrakk> \<Longrightarrow> APIType_capBits z b < 2 ^ word_bits
 4. \<lbrakk>b \<le> 32; z = object_type.SectionObject\<rbrakk> \<Longrightarrow> APIType_capBits z b < 2 ^ word_bits
 5. \<lbrakk>b \<le> 32; z = object_type.SuperSectionObject\<rbrakk> \<Longrightarrow> APIType_capBits z b < 2 ^ word_bits
 6. \<lbrakk>b \<le> 32; z = object_type.PageTableObject\<rbrakk> \<Longrightarrow> APIType_capBits z b < 2 ^ word_bits
 7. \<lbrakk>b \<le> 32; z = object_type.PageDirectoryObject\<rbrakk> \<Longrightarrow> APIType_capBits z b < 2 ^ word_bits proof (prove)
goal:
No subgoals!
theory Invoke_C

lemma  object_type_from_to_H:
  "unat v \<le> (fromEnum::object_type \<Rightarrow> nat) maxBound
         \<Longrightarrow> v = object_type_from_H (object_type_to_H v)" apply (simp add:toEnum_object_type_to_H[symmetric]) apply (rule iffD1[OF word_unat.Rep_inject]) apply (subst fromEnum_object_type_to_H[symmetric]) apply (simp add:from_to_enum) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat v \<le> fromEnum maxBound \<Longrightarrow> v = object_type_from_H (object_type_to_H v) proof (prove)
goal (1 subgoal):
 1. unat v \<le> fromEnum maxBound \<Longrightarrow> v = object_type_from_H (toEnum (unat v)) proof (prove)
goal (1 subgoal):
 1. unat v \<le> fromEnum maxBound \<Longrightarrow> unat v = unat (object_type_from_H (toEnum (unat v))) proof (prove)
goal (1 subgoal):
 1. unat v \<le> fromEnum maxBound \<Longrightarrow> unat v = fromEnum (toEnum (unat v)) proof (prove)
goal:
No subgoals!
theory Invoke_C

lemma ctes_of_ex_cte_cap_to':
  "ctes_of s p = Some cte \<Longrightarrow> \<forall>r \<in> cte_refs' (cteCap cte) (irq_node' s). ex_cte_cap_to' r s" by (auto simp add: ex_cte_cap_wp_to'_def cte_wp_at_ctes_of)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ctes_of s p = Some cte \<Longrightarrow> \<forall>r\<in>cte_refs' (cteCap cte) (irq_node' s). ex_cte_cap_wp_to' (\<lambda>_. True) r s
theory Tcb_C

lemma getObject_sched:
  "(x::tcb, s') \<in> fst (getObject t s) \<Longrightarrow>
  (x,s'\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>) \<in> fst (getObject t (s\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>))" apply (clarsimp simp: in_monad getObject_def split_def loadObject_default_def
                        magnitudeCheck_def projectKOs
                  split: option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x, s') \<in> fst (getObject t s) \<Longrightarrow> (x, s'\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>) \<in> fst (getObject t (s\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>)) proof (prove)
goal:
No subgoals!
theory Tcb_C

lemma setObject_sched:
  "(x, s') \<in> fst (setObject t (v::tcb) s) \<Longrightarrow>
  (x, s'\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>) \<in> fst (setObject t v (s\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>))" apply (clarsimp simp: in_monad setObject_def split_def updateObject_default_def
                        magnitudeCheck_def projectKOs
                  split: option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x, s') \<in> fst (setObject t v s) \<Longrightarrow> (x, s'\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>) \<in> fst (setObject t v (s\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>)) proof (prove)
goal:
No subgoals!
theory Tcb_C

lemma threadSet_sched:
  "(x, s') \<in> fst (threadSet f t s) \<Longrightarrow>
  (x,s'\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>) \<in> fst (threadSet f t (s\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>))" apply (clarsimp simp: in_monad threadSet_def) apply (drule getObject_sched) apply (drule setObject_sched) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x, s') \<in> fst (threadSet f t s) \<Longrightarrow> (x, s'\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>) \<in> fst (threadSet f t (s\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s'' tcb. \<lbrakk>(tcb, s'') \<in> fst (getObject t s); ((), s') \<in> fst (setObject t (f tcb) s'')\<rbrakk> \<Longrightarrow> \<exists>s'' tcb. (tcb, s'') \<in> fst (getObject t (s\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>)) \<and> ((), s'\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>) \<in> fst (setObject t (f tcb) s'') proof (prove)
goal (1 subgoal):
 1. \<And>s'' tcb. \<lbrakk>((), s') \<in> fst (setObject t (f tcb) s''); (tcb, s''\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>) \<in> fst (getObject t (s\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>))\<rbrakk> \<Longrightarrow> \<exists>s'' tcb. (tcb, s'') \<in> fst (getObject t (s\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>)) \<and> ((), s'\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>) \<in> fst (setObject t (f tcb) s'') proof (prove)
goal (1 subgoal):
 1. \<And>s'' tcb. \<lbrakk>(tcb, s''\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>) \<in> fst (getObject t (s\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>)); ((), s'\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>) \<in> fst (setObject t (f tcb) (s''\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>))\<rbrakk> \<Longrightarrow> \<exists>s'' tcb. (tcb, s'') \<in> fst (getObject t (s\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>)) \<and> ((), s'\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>) \<in> fst (setObject t (f tcb) s'') proof (prove)
goal:
No subgoals!
theory Tcb_C

lemma asUser_sched:
  "(rv,s') \<in> fst (asUser t f s) \<Longrightarrow>
  (rv,s'\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>) \<in> fst (asUser t f (s\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>))" apply (clarsimp simp: asUser_def split_def in_monad select_f_def) apply (drule threadGet_sched) apply (drule threadSet_sched) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (rv, s') \<in> fst (asUser t f s) \<Longrightarrow> (rv, s'\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>) \<in> fst (asUser t f (s\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s'' uc b. \<lbrakk>(uc, s'') \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) t s); (rv, b) \<in> fst (f uc); ((), s') \<in> fst (threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch tcb)) tcb) t s'')\<rbrakk> \<Longrightarrow> \<exists>s'' uc. (uc, s'') \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) t (s\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>)) \<and> (\<exists>b. (rv, b) \<in> fst (f uc) \<and> ((), s'\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>) \<in> fst (threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch tcb)) tcb) t s'')) proof (prove)
goal (1 subgoal):
 1. \<And>s'' uc b. \<lbrakk>(rv, b) \<in> fst (f uc); ((), s') \<in> fst (threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch tcb)) tcb) t s''); (uc, s''\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>) \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) t (s\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>))\<rbrakk> \<Longrightarrow> \<exists>s'' uc. (uc, s'') \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) t (s\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>)) \<and> (\<exists>b. (rv, b) \<in> fst (f uc) \<and> ((), s'\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>) \<in> fst (threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch tcb)) tcb) t s'')) proof (prove)
goal (1 subgoal):
 1. \<And>s'' uc b. \<lbrakk>(rv, b) \<in> fst (f uc); (uc, s''\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>) \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) t (s\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>)); ((), s'\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>) \<in> fst (threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch tcb)) tcb) t (s''\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>))\<rbrakk> \<Longrightarrow> \<exists>s'' uc. (uc, s'') \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) t (s\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>)) \<and> (\<exists>b. (rv, b) \<in> fst (f uc) \<and> ((), s'\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>) \<in> fst (threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch tcb)) tcb) t s'')) proof (prove)
goal:
No subgoals!
theory Tcb_C

lemma doMachineOp_sched:
  "(rv,s') \<in> fst (doMachineOp f s) \<Longrightarrow>
  (rv,s'\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>) \<in> fst (doMachineOp f (s\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>))" apply (clarsimp simp: doMachineOp_def split_def in_monad select_f_def) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (rv, s') \<in> fst (doMachineOp f s) \<Longrightarrow> (rv, s'\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>) \<in> fst (doMachineOp f (s\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>b. \<lbrakk>(rv, b) \<in> fst (f (ksMachineState s)); s' = s\<lparr>ksMachineState := b\<rparr>\<rbrakk> \<Longrightarrow> \<exists>ba. (rv, ba) \<in> fst (f (ksMachineState s)) \<and> s\<lparr>ksMachineState := b, ksSchedulerAction := ChooseNewThread\<rparr> = s\<lparr>ksSchedulerAction := ChooseNewThread, ksMachineState := ba\<rparr> proof (prove)
goal:
No subgoals!
theory Tcb_C

lemma doMachineOp_state:
  "(rv,s') \<in> fst (doMachineOp f s) \<Longrightarrow>
  (rv,s'\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>)
  \<in> fst (doMachineOp f (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>))" apply (clarsimp simp: doMachineOp_def split_def in_monad select_f_def) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (rv, s') \<in> fst (doMachineOp f s) \<Longrightarrow> (rv, s'\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>) \<in> fst (doMachineOp f (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>b. \<lbrakk>(rv, b) \<in> fst (f (ksMachineState s)); s' = s\<lparr>ksMachineState := b\<rparr>\<rbrakk> \<Longrightarrow> \<exists>ba. (rv, ba) \<in> fst (f (ksMachineState s)) \<and> s\<lparr>ksMachineState := b, ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko))\<rparr> = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) ko)), ksMachineState := ba\<rparr> proof (prove)
goal:
No subgoals!
theory Tcb_C

lemma setThreadState_sysargs_rel:
  "\<lbrace>sysargs_rel args buffer and (\<lambda>_. runnable' st)\<rbrace> setThreadState st t \<lbrace>\<lambda>_. sysargs_rel args buffer\<rbrace>" apply (cases buffer, simp_all add: sysargs_rel_def) apply (rule hoare_pre) apply (wp setThreadState_getMRs_rel hoare_valid_ipc_buffer_ptr_typ_at'|simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>sysargs_rel args buffer and (\<lambda>_. runnable' st)\<rbrace> setThreadState st t \<lbrace>\<lambda>_. sysargs_rel args buffer\<rbrace> proof (prove)
goal (2 subgoals):
 1. buffer = None \<Longrightarrow> \<lbrace>cur_tcb' and getMRs_rel args None and (\<lambda>_. \<not> unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters) < length args) and (\<lambda>_. runnable' st)\<rbrace> setThreadState st t \<lbrace>\<lambda>_. cur_tcb' and getMRs_rel args None and (\<lambda>_. \<not> unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters) < length args)\<rbrace>
 2. \<And>a. buffer = Some a \<Longrightarrow> \<lbrace>cur_tcb' and valid_ipc_buffer_ptr' a and getMRs_rel args (Some a) and (\<lambda>_. runnable' st)\<rbrace> setThreadState st t \<lbrace>\<lambda>_. cur_tcb' and valid_ipc_buffer_ptr' a and getMRs_rel args (Some a)\<rbrace> proof (prove)
goal (3 subgoals):
 1. buffer = None \<Longrightarrow> \<lbrace>?Q4\<rbrace> setThreadState st t \<lbrace>\<lambda>_. cur_tcb' and getMRs_rel args None and (\<lambda>_. \<not> unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters) < length args)\<rbrace>
 2. \<And>s. \<lbrakk>buffer = None; (cur_tcb' and getMRs_rel args None and (\<lambda>_. \<not> unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters) < length args) and (\<lambda>_. runnable' st)) s\<rbrakk> \<Longrightarrow> ?Q4 s
 3. \<And>a. buffer = Some a \<Longrightarrow> \<lbrace>cur_tcb' and valid_ipc_buffer_ptr' a and getMRs_rel args (Some a) and (\<lambda>_. runnable' st)\<rbrace> setThreadState st t \<lbrace>\<lambda>_. cur_tcb' and valid_ipc_buffer_ptr' a and getMRs_rel args (Some a)\<rbrace> proof (prove)
goal:
No subgoals!
theory Tcb_C

lemma ccorres_abstract_known:
  "\<lbrakk> \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' g (g' rv'); ccorres rvr xf P P' hs f (g' val) \<rbrakk>
     \<Longrightarrow> ccorres rvr xf P (P' \<inter> {s. xf' s = val}) hs f g" apply (rule ccorres_guard_imp2) apply (rule_tac xf'=xf' in ccorres_abstract) apply assumption apply (rule_tac P="rv' = val" in ccorres_gen_asm2) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' g (g' rv'); ccorres rvr xf P P' hs f (g' val)\<rbrakk> \<Longrightarrow> ccorres rvr xf P (P' \<inter> {s. xf' s = val}) hs f g proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' g (g' rv'); ccorres rvr xf P P' hs f (g' val)\<rbrakk> \<Longrightarrow> ccorres rvr xf ?Q ?Q' hs f g
 2. \<And>s s'. \<lbrakk>\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' g (g' rv'); ccorres rvr xf P P' hs f (g' val); (s, s') \<in> rf_sr; P s; s' \<in> P' \<inter> {s. xf' s = val}\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> ?Q' proof (prove)
goal (3 subgoals):
 1. \<And>rv' t t'. \<lbrakk>\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' g (g' rv'); ccorres rvr xf P P' hs f (g' val)\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xf' rv' t t' g (?d'3 rv')
 2. \<And>rv'. \<lbrakk>\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' g (g' rv'); ccorres rvr xf P P' hs f (g' val)\<rbrakk> \<Longrightarrow> ccorres rvr xf ?Q (?G'3 rv') hs f (?d'3 rv')
 3. \<And>s s'. \<lbrakk>\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' g (g' rv'); ccorres rvr xf P P' hs f (g' val); (s, s') \<in> rf_sr; P s; s' \<in> P' \<inter> {s. xf' s = val}\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> {s. s \<in> ?G'3 (xf' s)} proof (prove)
goal (2 subgoals):
 1. \<And>rv'. \<lbrakk>\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' g (g' rv'); ccorres rvr xf P P' hs f (g' val)\<rbrakk> \<Longrightarrow> ccorres rvr xf ?Q (?G'3 rv') hs f (g' rv')
 2. \<And>s s'. \<lbrakk>\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' g (g' rv'); ccorres rvr xf P P' hs f (g' val); (s, s') \<in> rf_sr; P s; s' \<in> P' \<inter> {s. xf' s = val}\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> {s. s \<in> ?G'3 (xf' s)} proof (prove)
goal (2 subgoals):
 1. \<And>rv'. \<lbrakk>\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' g (g' rv'); ccorres rvr xf P P' hs f (g' val); rv' = val\<rbrakk> \<Longrightarrow> ccorres rvr xf ?Q (?G'7 rv') hs f (g' rv')
 2. \<And>s s'. \<lbrakk>\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' g (g' rv'); ccorres rvr xf P P' hs f (g' val); (s, s') \<in> rf_sr; P s; s' \<in> P' \<inter> {s. xf' s = val}\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> {s. s \<in> ?G'7 (xf' s) \<inter> \<lbrace>xf' s = val\<rbrace>} proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' g (g' rv'); ccorres rvr xf P P' hs f (g' val); (s, s') \<in> rf_sr; P s; s' \<in> P' \<inter> {s. xf' s = val}\<rbrakk> \<Longrightarrow> P s \<and> s' \<in> {s. s \<in> P' \<inter> \<lbrace>xf' s = val\<rbrace>} proof (prove)
goal:
No subgoals!
theory Tcb_C

lemma ccorres_subgoal_tailE:
  "\<lbrakk> ccorres rvr xf Q Q' hs (b ()) d;
      ccorres rvr xf Q Q' hs (b ()) d \<Longrightarrow> ccorres rvr xf P P' hs (a >>=E b) (c ;; d) \<rbrakk>
        \<Longrightarrow> ccorres rvr xf P P' hs (a >>=E b) (c ;; d)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccorres rvr xf Q Q' hs (b ()) d; ccorres rvr xf Q Q' hs (b ()) d \<Longrightarrow> ccorres rvr xf P P' hs (a >>=E b) (c;;
d)\<rbrakk> \<Longrightarrow> ccorres rvr xf P P' hs (a >>=E b) (c;;
d)
theory Tcb_C

lemma cte_is_derived_capMasterCap_strg:
  "cte_wp_at' (is_derived' (ctes_of s) ptr cap \<circ> cteCap) ptr s
    \<longrightarrow> cte_wp_at' (\<lambda>scte. capMasterCap (cteCap scte) = capMasterCap cap \<or> P) ptr s" by (clarsimp simp: cte_wp_at_ctes_of is_derived'_def
                     badge_derived'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_wp_at' (is_derived' (ctes_of s) ptr cap \<circ> cteCap) ptr s \<longrightarrow> cte_wp_at' (\<lambda>scte. capMasterCap (cteCap scte) = capMasterCap cap \<or> P) ptr s