kings-crown/FVELER_Isabelle huggingface dataset:
theory Tcb_R

lemma tcbPriority_Queued_caps_safe:
  "\<forall>tcb. \<forall>x\<in>ran tcb_cte_cases. (\<lambda>(getF, setF). getF (tcbPriority_update f (tcbQueued_update g tcb)) = getF tcb) x" by (rule all_tcbI, rule ball_tcb_cte_casesI, simp+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>tcb. \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> getF (tcbPriority_update f (tcbQueued_update g tcb)) = getF tcb
theory Tcb_R

lemma cte_map_tcb_0:
  "cte_map (t, tcb_cnode_index 0) = t" by (simp add: cte_map_def tcb_cnode_index_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_map (t, tcb_cnode_index 0) = t
theory Tcb_R

lemma cte_map_tcb_1:
  "cte_map (t, tcb_cnode_index 1) = t + 2^cteSizeBits" by (simp add: cte_map_def tcb_cnode_index_def to_bl_1 objBits_defs cte_level_bits_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_map (t, tcb_cnode_index 1) = t + 2 ^ cteSizeBits
theory Tcb_R

lemma sameRegion_corres2:
  "\<lbrakk> cap_relation c c'; cap_relation d d' \<rbrakk>
     \<Longrightarrow> same_region_as c d = sameRegionAs c' d'" by (erule(1) same_region_as_relation)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_relation c c'; cap_relation d d'\<rbrakk> \<Longrightarrow> same_region_as c d = global.sameRegionAs c' d'
theory Tcb_R

lemma untyped_derived_eq_from_sameObjectAs:
  "sameObjectAs cap cap2
    \<Longrightarrow> untyped_derived_eq cap cap2" by (clarsimp simp: untyped_derived_eq_def sameObjectAs_def2 isCap_Master)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. global.sameObjectAs cap cap2 \<Longrightarrow> untyped_derived_eq cap cap2
theory Tcb_R

lemma checkCap_inv:
  assumes x: "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv. P\<rbrace>"
  shows      "\<lbrace>P\<rbrace> checkCapAt cap slot f \<lbrace>\<lambda>rv. P\<rbrace>" unfolding checkCapAt_def by (wp x | simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> checkCapAt cap slot f \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> do cap' <- liftM cteCap $ getCTE slot;
when (global.sameObjectAs cap cap') f
od \<lbrace>\<lambda>rv. P\<rbrace>
theory Tcb_R

lemma checkCap_wp:
  assumes x: "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv. Q\<rbrace>"
  and PQ: "\<And>s. P s \<Longrightarrow> Q s"
  shows "\<lbrace>P\<rbrace> checkCapAt cap slot f \<lbrace>\<lambda>rv. Q\<rbrace>" unfolding checkCapAt_def apply (wp x) apply (rule hoare_strengthen_post[rotated]) apply clarsimp apply (strengthen PQ) apply assumption apply simp apply (wp x | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> checkCapAt cap slot f \<lbrace>\<lambda>rv. Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> do cap' <- liftM cteCap $ getCTE slot;
when (global.sameObjectAs cap cap') f
od \<lbrace>\<lambda>rv. Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> getCTE slot \<lbrace>(\<lambda>cap'. if global.sameObjectAs cap cap' then P else Q) \<circ> cteCap\<rbrace>
 2. \<And>s. P s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>rv s. ?Q5 rv s \<Longrightarrow> ((\<lambda>cap'. if global.sameObjectAs cap cap' then P else Q) \<circ> cteCap) rv s
 2. \<lbrace>?Q\<rbrace> getCTE slot \<lbrace>?Q5\<rbrace>
 3. \<And>s. P s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>rv s. ?Q5 rv s \<Longrightarrow> (global.sameObjectAs cap (cteCap rv) \<longrightarrow> P s) \<and> (\<not> global.sameObjectAs cap (cteCap rv) \<longrightarrow> Q s)
 2. \<lbrace>?Q\<rbrace> getCTE slot \<lbrace>?Q5\<rbrace>
 3. \<And>s. P s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>rv s. ?Q5 rv s \<Longrightarrow> (global.sameObjectAs cap (cteCap rv) \<longrightarrow> P s) \<and> (\<not> global.sameObjectAs cap (cteCap rv) \<longrightarrow> P s)
 2. \<lbrace>?Q\<rbrace> getCTE slot \<lbrace>?Q5\<rbrace>
 3. \<And>s. P s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> getCTE slot \<lbrace>\<lambda>rv s. (global.sameObjectAs cap (cteCap rv) \<longrightarrow> P s) \<and> (\<not> global.sameObjectAs cap (cteCap rv) \<longrightarrow> P s)\<rbrace>
 2. \<And>s. P s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> getCTE slot \<lbrace>\<lambda>rv. P\<rbrace>
 2. \<And>s. P s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory Tcb_R

lemma isValidVTableRootD:
  "isValidVTableRoot cap
     \<Longrightarrow> isArchObjectCap cap \<and> isPageDirectoryCap (capCap cap)
             \<and> capPDMappedASID (capCap cap) \<noteq> None" by (simp add: isValidVTableRoot_def
                ARM_H.isValidVTableRoot_def
                isCap_simps
         split: capability.split_asm arch_capability.split_asm
                option.split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isValidVTableRoot cap \<Longrightarrow> isArchObjectCap cap \<and> isPageDirectoryCap (capCap cap) \<and> capPDMappedASID (capCap cap) \<noteq> None
theory Tcb_R

lemma assertDerived_wp:
  "\<lbrace>P and (\<lambda>s. cte_wp_at' (is_derived' (ctes_of s) slot cap o cteCap) slot s)\<rbrace> f \<lbrace>Q\<rbrace> \<Longrightarrow>
  \<lbrace>P\<rbrace> assertDerived slot cap f \<lbrace>Q\<rbrace>" apply (simp add: assertDerived_def) apply wpsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P and (\<lambda>s. cte_wp_at' (is_derived' (ctes_of s) slot cap \<circ> cteCap) slot s)\<rbrace> f \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> assertDerived slot cap f \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P and (\<lambda>s. cte_wp_at' (is_derived' (ctes_of s) slot cap \<circ> cteCap) slot s)\<rbrace> f \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> do y <- stateAssert (\<lambda>s. cte_wp_at' (is_derived' (ctes_of s) slot cap \<circ> cteCap) slot s) [];
f
od \<lbrace>Q\<rbrace> proof (prove)
goal:
No subgoals!
theory Tcb_R

lemma assertDerived_wp_weak:
  "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> assertDerived slot cap f \<lbrace>Q\<rbrace>" apply (wpsimp simp: assertDerived_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> assertDerived slot cap f \<lbrace>Q\<rbrace> proof (prove)
goal:
No subgoals!
theory Tcb_R

lemma tcbMCP_caps_safe:
  "\<forall>tcb. \<forall>x\<in>ran tcb_cte_cases. (\<lambda>(getF, setF). getF (tcbMCP_update f tcb) = getF tcb) x" by (rule all_tcbI, rule ball_tcb_cte_casesI, simp+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>tcb. \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> getF (tcbMCP_update f tcb) = getF tcb
theory Tcb_R

lemma tcbMCP_Queued_caps_safe:
  "\<forall>tcb. \<forall>x\<in>ran tcb_cte_cases. (\<lambda>(getF, setF). getF (tcbMCP_update f (tcbQueued_update g tcb)) = getF tcb) x" by (rule all_tcbI, rule ball_tcb_cte_casesI, simp+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>tcb. \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> getF (tcbMCP_update f (tcbQueued_update g tcb)) = getF tcb
theory Tcb_R

lemma setMCPriority_invs':
  "\<lbrace>invs' and tcb_at' t and K (prio \<le> maxPriority)\<rbrace> setMCPriority t prio \<lbrace>\<lambda>rv. invs'\<rbrace>" unfolding setMCPriority_def apply (rule hoare_gen_asm) apply (rule hoare_pre) by (wp threadSet_invs_trivial, (clarsimp simp: inQ_def)+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and tcb_at' t and K (prio \<le> maxPriority)\<rbrace> setMCPriority t prio \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and tcb_at' t and K (prio \<le> maxPriority)\<rbrace> threadSet (tcbMCP_update (\<lambda>_. prio)) t \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. prio \<le> maxPriority \<Longrightarrow> \<lbrace>invs' and tcb_at' t\<rbrace> threadSet (tcbMCP_update (\<lambda>_. prio)) t \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (2 subgoals):
 1. prio \<le> maxPriority \<Longrightarrow> \<lbrace>?Q2\<rbrace> threadSet (tcbMCP_update (\<lambda>_. prio)) t \<lbrace>\<lambda>rv. invs'\<rbrace>
 2. \<And>s. \<lbrakk>prio \<le> maxPriority; (invs' and tcb_at' t) s\<rbrakk> \<Longrightarrow> ?Q2 s
theory Tcb_R

lemma valid_tcb'_tcbMCP_update:
  "\<lbrakk>valid_tcb' tcb s \<and> f (tcbMCP tcb) \<le> maxPriority\<rbrakk> \<Longrightarrow> valid_tcb' (tcbMCP_update f tcb) s" apply (simp add: valid_tcb'_def tcb_cte_cases_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_tcb' tcb s \<and> f (tcbMCP tcb) \<le> maxPriority \<Longrightarrow> valid_tcb' (tcbMCP_update f tcb) s proof (prove)
goal:
No subgoals!
theory Tcb_R

lemma inQ_tc_corres_helper:
  "(\<forall>d p. (\<exists>tcb. tcbQueued tcb \<and> tcbPriority tcb = p \<and> tcbDomain tcb = d \<and> (tcbQueued tcb \<longrightarrow> tcbDomain tcb \<noteq> d)) \<longrightarrow> a \<notin> set (ksReadyQueues s (d, p))) = True" by clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<forall>d p. (\<exists>tcb. tcbQueued tcb \<and> tcbPriority tcb = p \<and> tcbDomain tcb = d \<and> (tcbQueued tcb \<longrightarrow> tcbDomain tcb \<noteq> d)) \<longrightarrow> a \<notin> set (ksReadyQueues s (d, p))) = True
theory Tcb_R

lemma threadcontrol_corres_helper2:
  "is_aligned a msg_align_bits \<Longrightarrow> \<lbrace>invs' and tcb_at' t\<rbrace>
      threadSet (tcbIPCBuffer_update (\<lambda>_. a)) t
           \<lbrace>\<lambda>x s. Invariants_H.valid_queues s \<and> valid_queues' s \<and> weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>" by (wp threadSet_invs_trivial
      | strengthen  invs_valid_queues' invs_queues invs_weak_sch_act_wf
      | clarsimp simp: inQ_def )+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned a msg_align_bits \<Longrightarrow> \<lbrace>invs' and tcb_at' t\<rbrace> threadSet (tcbIPCBuffer_update (\<lambda>_. a)) t \<lbrace>\<lambda>x s. Invariants_H.valid_queues s \<and> valid_queues' s \<and> weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>
theory Tcb_R

lemma threadcontrol_corres_helper3:
  "\<lbrace> einvs and simple_sched_action\<rbrace>
           check_cap_at aaa (ab, ba) (check_cap_at (cap.ThreadCap a) slot (cap_insert aaa (ab, ba) (a, tcb_cnode_index 4)))
           \<lbrace>\<lambda>x. weak_valid_sched_action and valid_etcbs \<rbrace>" apply (rule hoare_pre) apply (wp check_cap_inv | simp add:)+ by (clarsimp simp add: weak_valid_sched_action_def valid_etcbs_2_def st_tcb_at_kh_def
               get_tcb_def obj_at_kh_def obj_at_def is_etcb_at'_def valid_sched_def valid_sched_action_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>einvs and simple_sched_action\<rbrace> check_cap_at aaa (ab, ba) (check_cap_at (cap.ThreadCap a) slot (cap_insert aaa (ab, ba) (a, tcb_cnode_index 4))) \<lbrace>\<lambda>x. weak_valid_sched_action and valid_etcbs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> check_cap_at aaa (ab, ba) (check_cap_at (cap.ThreadCap a) slot (cap_insert aaa (ab, ba) (a, tcb_cnode_index 4))) \<lbrace>\<lambda>x. weak_valid_sched_action and valid_etcbs\<rbrace>
 2. \<And>s. (einvs and simple_sched_action) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. invs s \<and> valid_list s \<and> valid_sched s \<and> simple_sched_action s \<Longrightarrow> weak_valid_sched_action s \<and> valid_etcbs s
theory Tcb_R

lemma threadcontrol_corres_helper4:
  "isArchObjectCap ac \<Longrightarrow>
  \<lbrace>invs' and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) (cte_map (a, tcb_cnode_index 4)) and valid_cap' ac \<rbrace>
    checkCapAt ac (cte_map (ab, ba))
      (checkCapAt (capability.ThreadCap a) (cte_map slot)
         (assertDerived (cte_map (ab, ba)) ac (cteInsert ac (cte_map (ab, ba)) (cte_map (a, tcb_cnode_index 4)))))
  \<lbrace>\<lambda>x. Invariants_H.valid_queues and valid_queues' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)\<rbrace>" apply (wp
       | strengthen  invs_valid_queues' invs_queues invs_weak_sch_act_wf
       | clarsimp simp: )+ by (case_tac ac;
      clarsimp simp: capBadge_def isArchObjectCap_def isNotificationCap_def isEndpointCap_def
                     isReplyCap_def isIRQControlCap_def tcb_cnode_index_def cte_map_def cte_wp_at'_def
                     cte_level_bits_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isArchObjectCap ac \<Longrightarrow> \<lbrace>invs' and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) (cte_map (a, tcb_cnode_index 4)) and valid_cap' ac\<rbrace> checkCapAt ac (cte_map (ab, ba)) (checkCapAt (capability.ThreadCap a) (cte_map slot) (assertDerived (cte_map (ab, ba)) ac (cteInsert ac (cte_map (ab, ba)) (cte_map (a, tcb_cnode_index 4))))) \<lbrace>\<lambda>x. Invariants_H.valid_queues and valid_queues' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>isArchObjectCap ac; invs' s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) (cte_map (a, tcb_cnode_index 4)) s; valid_cap' ac s\<rbrakk> \<Longrightarrow> capBadge ac = None \<and> cte_map (a, tcb_cnode_index 4) \<in> (+) a ` dom tcb_cte_cases \<and> \<not> isReplyCap ac \<and> \<not> isIRQControlCap ac
theory Tcb_R

lemma getThreadBufferSlot_dom_tcb_cte_cases:
  "\<lbrace>\<top>\<rbrace> getThreadBufferSlot a \<lbrace>\<lambda>rv s. rv \<in> (+) a ` dom tcb_cte_cases\<rbrace>" by (wpsimp simp: tcb_cte_cases_def getThreadBufferSlot_def locateSlot_conv cte_level_bits_def
                   tcbIPCBufferSlot_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> getThreadBufferSlot a \<lbrace>\<lambda>rv s. rv \<in> (+) a ` dom tcb_cte_cases\<rbrace>
theory Tcb_R

lemma tcb_at'_cteInsert[wp]:
  "\<lbrace>\<lambda>s. tcb_at' (ksCurThread s) s\<rbrace> cteInsert t x y \<lbrace>\<lambda>_ s. tcb_at' (ksCurThread s) s\<rbrace>" by (rule hoare_weaken_pre, wps cteInsert_ct, wp, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. tcb_at' (ksCurThread s) s\<rbrace> cteInsert t x y \<lbrace>\<lambda>_ s. tcb_at' (ksCurThread s) s\<rbrace>
theory Tcb_R

lemma tcb_at'_asUser[wp]:
  "\<lbrace>\<lambda>s. tcb_at' (ksCurThread s) s\<rbrace> asUser a (setTCBIPCBuffer b) \<lbrace>\<lambda>_ s. tcb_at' (ksCurThread s) s\<rbrace>" by (rule hoare_weaken_pre, wps asUser_typ_ats(1), wp, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. tcb_at' (ksCurThread s) s\<rbrace> asUser a (setTCBIPCBuffer b) \<lbrace>\<lambda>_ s. tcb_at' (ksCurThread s) s\<rbrace>
theory Tcb_R

lemma tcb_at'_threadSet[wp]:
  "\<lbrace>\<lambda>s. tcb_at' (ksCurThread s) s\<rbrace> threadSet (tcbIPCBuffer_update (\<lambda>_. b)) a \<lbrace>\<lambda>_ s. tcb_at' (ksCurThread s) s\<rbrace>" by (rule hoare_weaken_pre, wps threadSet_tcb', wp, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. tcb_at' (ksCurThread s) s\<rbrace> threadSet (tcbIPCBuffer_update (\<lambda>_. b)) a \<lbrace>\<lambda>_ s. tcb_at' (ksCurThread s) s\<rbrace>
theory Tcb_R

lemma cteDelete_it [wp]:
  "\<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> cteDelete slot e \<lbrace>\<lambda>_ s. P (ksIdleThread s)\<rbrace>" by (rule cteDelete_preservation) (wp | clarsimp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> cteDelete slot e \<lbrace>\<lambda>_ s. P (ksIdleThread s)\<rbrace>
theory Tcb_R

lemma valid_tcb_ipc_buffer_update:
  "\<And>buf s. is_aligned buf msg_align_bits
   \<Longrightarrow> (\<forall>tcb. valid_tcb' tcb s \<longrightarrow> valid_tcb' (tcbIPCBuffer_update (\<lambda>_. buf) tcb) s)" by (simp add: valid_tcb'_def tcb_cte_cases_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>buf s. is_aligned buf msg_align_bits \<Longrightarrow> \<forall>tcb. valid_tcb' tcb s \<longrightarrow> valid_tcb' (tcbIPCBuffer_update (\<lambda>_. buf) tcb) s
theory Tcb_R

lemma isReplyCapD:
  "isReplyCap cap \<Longrightarrow> \<exists>ptr master grant. cap = capability.ReplyCap ptr master grant" by (simp add: isCap_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isReplyCap cap \<Longrightarrow> \<exists>ptr master grant. cap = capability.ReplyCap ptr master grant
theory Tcb_R

lemma cteInsert_sa_simple[wp]:
  "\<lbrace>sch_act_simple\<rbrace> cteInsert newCap srcSlot destSlot \<lbrace>\<lambda>_. sch_act_simple\<rbrace>" by (simp add: sch_act_simple_def, wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>sch_act_simple\<rbrace> cteInsert newCap srcSlot destSlot \<lbrace>\<lambda>_. sch_act_simple\<rbrace>
theory Tcb_R

lemma tcbBoundNotification_caps_safe[simp]:
  "\<forall>(getF, setF)\<in>ran tcb_cte_cases.
     getF (tcbBoundNotification_update (\<lambda>_. Some ntfnptr) tcb) = getF tcb" by (case_tac tcb, simp add: tcb_cte_cases_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>(getF, setF)\<in>ran tcb_cte_cases. getF (tcbBoundNotification_update (\<lambda>_. Some ntfnptr) tcb) = getF tcb
theory Tcb_R

lemma valid_bound_ntfn_lift:
  assumes P: "\<And>P T p. \<lbrace>\<lambda>s. P (typ_at' T p s)\<rbrace> f \<lbrace>\<lambda>rv s. P (typ_at' T p s)\<rbrace>"
  shows      "\<lbrace>\<lambda>s. valid_bound_ntfn' a s\<rbrace> f \<lbrace>\<lambda>rv s. valid_bound_ntfn' a s\<rbrace>" apply (simp add: valid_bound_ntfn'_def, case_tac a, simp_all) apply (wp typ_at_lifts[OF P])+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_bound_ntfn' a\<rbrace> f \<lbrace>\<lambda>rv. valid_bound_ntfn' a\<rbrace> proof (prove)
goal (2 subgoals):
 1. a = None \<Longrightarrow> \<lbrace>\<lambda>s. True\<rbrace> f \<lbrace>\<lambda>rv s. True\<rbrace>
 2. \<And>aa. a = Some aa \<Longrightarrow> \<lbrace>ntfn_at' aa\<rbrace> f \<lbrace>\<lambda>rv. ntfn_at' aa\<rbrace> proof (prove)
goal:
No subgoals!
theory Tcb_R

lemma tcbntfn_invs':
  "\<lbrace>invs' and tcb_inv_wf' (tcbinvocation.NotificationControl tcb ntfnptr)\<rbrace>
       invokeTCB (tcbinvocation.NotificationControl tcb ntfnptr)
   \<lbrace>\<lambda>rv. invs'\<rbrace>" apply (simp add: invokeTCB_def) apply (case_tac ntfnptr, simp_all) apply (wp unbindNotification_invs bindNotification_invs' | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and tcb_inv_wf' (tcbinvocation.NotificationControl tcb ntfnptr)\<rbrace> invokeTCB (tcbinvocation.NotificationControl tcb ntfnptr) \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and (tcb_at' tcb and ex_nonz_cap_to' tcb and (case ntfnptr of None \<Rightarrow> \<lambda>_. True | Some ntfnptr \<Rightarrow> obj_at' (\<lambda>ko. ntfnBoundTCB ko = None \<and> (\<forall>q. ntfnObj ko \<noteq> Structures_H.ntfn.WaitingNtfn q)) ntfnptr and ex_nonz_cap_to' ntfnptr and bound_tcb_at' ((=) None) tcb))\<rbrace> case ntfnptr of None \<Rightarrow> liftE (do y <- unbindNotification tcb;
return []
od) | Some ntfnPtr \<Rightarrow> liftE (do y <- bindNotification tcb ntfnPtr;
return []
od) \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (2 subgoals):
 1. ntfnptr = None \<Longrightarrow> \<lbrace>invs' and (tcb_at' tcb and ex_nonz_cap_to' tcb)\<rbrace> liftE (do y <- unbindNotification tcb;
return []
od) \<lbrace>\<lambda>rv. invs'\<rbrace>
 2. \<And>a. ntfnptr = Some a \<Longrightarrow> \<lbrace>invs' and (tcb_at' tcb and ex_nonz_cap_to' tcb and (obj_at' (\<lambda>ko. ntfnBoundTCB ko = None \<and> (\<forall>q. ntfnObj ko \<noteq> Structures_H.ntfn.WaitingNtfn q)) a and ex_nonz_cap_to' a and bound_tcb_at' ((=) None) tcb))\<rbrace> liftE (do y <- bindNotification tcb a;
return []
od) \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal:
No subgoals!
theory Tcb_R

lemma setTLSBase_invs'[wp]:
  "\<lbrace>invs' and tcb_inv_wf' (tcbinvocation.SetTLSBase tcb tls_base)\<rbrace>
       invokeTCB (tcbinvocation.SetTLSBase tcb tls_base)
   \<lbrace>\<lambda>rv. invs'\<rbrace>" by (wpsimp simp: invokeTCB_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and tcb_inv_wf' (tcbinvocation.SetTLSBase tcb tls_base)\<rbrace> invokeTCB (tcbinvocation.SetTLSBase tcb tls_base) \<lbrace>\<lambda>rv. invs'\<rbrace>
theory Tcb_R

lemma copyregsets_map_only[simp]:
  "copyregsets_map v = ARMNoExtraRegisters" by (cases "copyregsets_map v", simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. copyregsets_map v = copy_register_sets.ARMNoExtraRegisters
theory Tcb_R

lemma decodeReadReg_wf:
  "\<lbrace>invs' and tcb_at' t and ex_nonz_cap_to' t\<rbrace>
     decodeReadRegisters args (ThreadCap t)
   \<lbrace>tcb_inv_wf'\<rbrace>,-" apply (simp add: decodeReadRegisters_def decodeTransfer_def whenE_def
             cong: list.case_cong) apply (rule hoare_pre) apply (wp | wpc)+ apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and tcb_at' t and ex_nonz_cap_to' t\<rbrace> decodeReadRegisters args (capability.ThreadCap t) \<lbrace>tcb_inv_wf'\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and tcb_at' t and ex_nonz_cap_to' t\<rbrace> case args of [] \<Rightarrow> throwError Fault_H.syscall_error.TruncatedMessage | [flags] \<Rightarrow> throwError Fault_H.syscall_error.TruncatedMessage | flags # n # x \<Rightarrow> doE y <- rangeCheck n (Suc 0) (length TCB_H.frameRegisters + length TCB_H.gpRegisters);
self <- liftE getCurThread;
y <- if t = self then throwError Fault_H.syscall_error.IllegalOperation else returnOk ();
returnOk (tcbinvocation.ReadRegisters t (flags !! 0) n copy_register_sets.ARMNoExtraRegisters)
odE \<lbrace>tcb_inv_wf'\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'6\<rbrace> case args of [] \<Rightarrow> throwError Fault_H.syscall_error.TruncatedMessage | [flags] \<Rightarrow> throwError Fault_H.syscall_error.TruncatedMessage | flags # n # x \<Rightarrow> doE y <- rangeCheck n (Suc 0) (length TCB_H.frameRegisters + length TCB_H.gpRegisters);
self <- liftE getCurThread;
y <- if t = self then throwError Fault_H.syscall_error.IllegalOperation else returnOk ();
returnOk (tcbinvocation.ReadRegisters t (flags !! 0) n copy_register_sets.ARMNoExtraRegisters)
odE \<lbrace>tcb_inv_wf'\<rbrace>, -
 2. \<And>s. (invs' and tcb_at' t and ex_nonz_cap_to' t) s \<Longrightarrow> ?P'6 s proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs' and tcb_at' t and ex_nonz_cap_to' t) s \<Longrightarrow> (args = [] \<longrightarrow> True) \<and> (\<forall>x xa. args = x # xa \<longrightarrow> (xa = [] \<longrightarrow> True) \<and> (\<forall>xb xc. xa = xb # xc \<longrightarrow> True \<and> True \<and> True \<and> (t = ksCurThread s \<longrightarrow> True) \<and> (t \<noteq> ksCurThread s \<longrightarrow> tcb_inv_wf' (tcbinvocation.ReadRegisters t (x !! 0) xb copy_register_sets.ARMNoExtraRegisters) s))) proof (prove)
goal:
No subgoals!