kings-crown/FVELER_Isabelle huggingface dataset:
theory CNodeInv_R

lemma sameRegion_cap'_src [simp]:
  "sameRegionAs cap' c = sameRegionAs src_cap c" using parency unfolding weak_derived'_def apply (case_tac "isReplyCap src_cap"; clarsimp) apply (clarsimp simp: capMasterCap_def split: capability.splits arch_capability.splits
         ; fastforce simp: sameRegionAs_def ARM_H.sameRegionAs_def isCap_simps split: if_split_asm)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. global.sameRegionAs cap' c = global.sameRegionAs src_cap c proof (prove)
using this:
weak_derived' src_cap cap'

goal (1 subgoal):
 1. global.sameRegionAs cap' c = global.sameRegionAs src_cap c proof (prove)
using this:
capMasterCap src_cap = capMasterCap cap' \<and> capBadge src_cap = capBadge cap' \<and> capASID src_cap = capASID cap' \<and> cap_asid_base' src_cap = cap_asid_base' cap' \<and> cap_vptr' src_cap = cap_vptr' cap' \<and> (isReplyCap src_cap \<longrightarrow> capTCBPtr src_cap = capTCBPtr cap' \<and> capReplyMaster src_cap = capReplyMaster cap')

goal (1 subgoal):
 1. global.sameRegionAs cap' c = global.sameRegionAs src_cap c proof (prove)
goal (2 subgoals):
 1. \<lbrakk>isReplyCap src_cap; capMasterCap src_cap = capMasterCap cap'; capBadge src_cap = capBadge cap'; capASID src_cap = capASID cap'; cap_asid_base' src_cap = cap_asid_base' cap'; cap_vptr' src_cap = cap_vptr' cap'; capTCBPtr src_cap = capTCBPtr cap'; capReplyMaster src_cap = capReplyMaster cap'\<rbrakk> \<Longrightarrow> global.sameRegionAs cap' c = global.sameRegionAs src_cap c
 2. \<lbrakk>\<not> isReplyCap src_cap; capMasterCap src_cap = capMasterCap cap'; capBadge src_cap = capBadge cap'; capASID src_cap = capASID cap'; cap_asid_base' src_cap = cap_asid_base' cap'; cap_vptr' src_cap = cap_vptr' cap'\<rbrakk> \<Longrightarrow> global.sameRegionAs cap' c = global.sameRegionAs src_cap c proof (prove)
goal:
No subgoals!
theory CNodeInv_R

lemma isUntypedCap':
  "isUntypedCap cap' = isUntypedCap src_cap" using parency unfolding weak_derived'_def by (clarsimp simp: weak_derived'_def dest!: capMaster_isUntyped)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isUntypedCap cap' = isUntypedCap src_cap proof (prove)
using this:
weak_derived' src_cap cap'

goal (1 subgoal):
 1. isUntypedCap cap' = isUntypedCap src_cap proof (prove)
using this:
capMasterCap src_cap = capMasterCap cap' \<and> capBadge src_cap = capBadge cap' \<and> capASID src_cap = capASID cap' \<and> cap_asid_base' src_cap = cap_asid_base' cap' \<and> cap_vptr' src_cap = cap_vptr' cap' \<and> (isReplyCap src_cap \<longrightarrow> capTCBPtr src_cap = capTCBPtr cap' \<and> capReplyMaster src_cap = capReplyMaster cap')

goal (1 subgoal):
 1. isUntypedCap cap' = isUntypedCap src_cap
theory CNodeInv_R

lemma capRange':
  "capRange cap' = capRange src_cap" using parency unfolding weak_derived'_def by (clarsimp simp: weak_derived'_def dest!: capMaster_capRange)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. capRange cap' = capRange src_cap proof (prove)
using this:
weak_derived' src_cap cap'

goal (1 subgoal):
 1. capRange cap' = capRange src_cap proof (prove)
using this:
capMasterCap src_cap = capMasterCap cap' \<and> capBadge src_cap = capBadge cap' \<and> capASID src_cap = capASID cap' \<and> cap_asid_base' src_cap = cap_asid_base' cap' \<and> cap_vptr' src_cap = cap_vptr' cap' \<and> (isReplyCap src_cap \<longrightarrow> capTCBPtr src_cap = capTCBPtr cap' \<and> capReplyMaster src_cap = capReplyMaster cap')

goal (1 subgoal):
 1. capRange cap' = capRange src_cap
theory CNodeInv_R

lemma untypedRange':
  "untypedRange cap' = untypedRange src_cap" using parency unfolding weak_derived'_def by (clarsimp simp: weak_derived'_def dest!: capMaster_untypedRange)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. untypedRange cap' = untypedRange src_cap proof (prove)
using this:
weak_derived' src_cap cap'

goal (1 subgoal):
 1. untypedRange cap' = untypedRange src_cap proof (prove)
using this:
capMasterCap src_cap = capMasterCap cap' \<and> capBadge src_cap = capBadge cap' \<and> capASID src_cap = capASID cap' \<and> cap_asid_base' src_cap = cap_asid_base' cap' \<and> cap_vptr' src_cap = cap_vptr' cap' \<and> (isReplyCap src_cap \<longrightarrow> capTCBPtr src_cap = capTCBPtr cap' \<and> capReplyMaster src_cap = capReplyMaster cap')

goal (1 subgoal):
 1. untypedRange cap' = untypedRange src_cap
theory CNodeInv_R

lemma cteMove_idle'[wp]:
  "\<lbrace>\<lambda>s. valid_idle' s\<rbrace>
     cteMove cap src dest
   \<lbrace>\<lambda>rv. valid_idle'\<rbrace>" apply (simp add: cteMove_def) apply (wp updateCap_idle' | simp)+ apply (wp getCTE_wp') apply (clarsimp simp: valid_idle'_def cte_wp_at_ctes_of weak_derived'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_idle'\<rbrace> cteMove cap src dest \<lbrace>\<lambda>rv. valid_idle'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_idle'\<rbrace> do oldCTE <- getCTE dest;
y <- assert (cteCap oldCTE = capability.NullCap);
y <- assert (mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer);
cte <- getCTE src;
y <- updateCap dest cap;
y <- updateCap src capability.NullCap;
y <- updateMDB dest (const (cteMDBNode cte));
y <- updateMDB src (const nullMDBNode);
y <- updateMDB (mdbPrev (cteMDBNode cte)) (mdbNext_update (\<lambda>_. dest));
updateMDB (mdbNext (cteMDBNode cte)) (mdbPrev_update (\<lambda>_. dest))
od \<lbrace>\<lambda>rv. valid_idle'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> getCTE dest \<lbrace>\<lambda>oldCTE s. cteCap oldCTE = capability.NullCap \<longrightarrow> mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer \<longrightarrow> valid_idle' s\<rbrace>
 2. \<And>s. valid_idle' s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_idle' s \<Longrightarrow> \<forall>cte. cte_wp_at' ((=) cte) dest s \<longrightarrow> cteCap cte = capability.NullCap \<longrightarrow> mdbPrev (cteMDBNode cte) = nullPointer \<and> mdbNext (cteMDBNode cte) = nullPointer \<longrightarrow> valid_idle' s proof (prove)
goal:
No subgoals!
theory CNodeInv_R

lemma cteMove_cte_wp_at:
  "\<lbrace>\<lambda>s. cte_at' ptr s \<and> (if p = ptr  then (Q capability.NullCap) else (if p' = ptr then Q cap else cte_wp_at' (Q \<circ> cteCap) ptr s))\<rbrace>
  cteMove cap p p'
  \<lbrace>\<lambda>_ s. cte_wp_at' (\<lambda>c. Q (cteCap c)) ptr s\<rbrace>" unfolding cteMove_def apply (fold o_def) apply (wp updateCap_cte_wp_at_cases updateMDB_weak_cte_wp_at getCTE_wp hoare_weak_lift_imp|simp add: o_def)+ apply (clarsimp simp: cte_wp_at_ctes_of) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cte_wp_at' (\<lambda>_. True) ptr s \<and> (if p = ptr then Q capability.NullCap else if p' = ptr then Q cap else cte_wp_at' (Q \<circ> cteCap) ptr s)\<rbrace> cteMove cap p p' \<lbrace>\<lambda>_. cte_wp_at' (\<lambda>c. Q (cteCap c)) ptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cte_wp_at' (\<lambda>_. True) ptr s \<and> (if p = ptr then Q capability.NullCap else if p' = ptr then Q cap else cte_wp_at' (Q \<circ> cteCap) ptr s)\<rbrace> do oldCTE <- getCTE p';
haskell_assert (isNullCap $ cteCap oldCTE) [];
haskell_assert (mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer) [];
cte <- getCTE p;
mdb <- return (cteMDBNode cte);
updateCap p' cap;
updateCap p capability.NullCap;
updateMDB p' (const mdb);
updateMDB p (const nullMDBNode);
updateMDB (mdbPrev mdb) (mdbNext_update (\<lambda>_. p'));
updateMDB (mdbNext mdb) (mdbPrev_update (\<lambda>_. p'))
od \<lbrace>\<lambda>_. cte_wp_at' (\<lambda>c. Q (cteCap c)) ptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cte_wp_at' (\<lambda>_. True) ptr s \<and> (if p = ptr then Q capability.NullCap else if p' = ptr then Q cap else cte_wp_at' (Q \<circ> cteCap) ptr s)\<rbrace> do oldCTE <- getCTE p';
haskell_assert (isNullCap $ cteCap oldCTE) [];
haskell_assert (mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer) [];
cte <- getCTE p;
mdb <- return (cteMDBNode cte);
updateCap p' cap;
updateCap p capability.NullCap;
updateMDB p' (const mdb);
updateMDB p (const nullMDBNode);
updateMDB (mdbPrev mdb) (mdbNext_update (\<lambda>_. p'));
updateMDB (mdbNext mdb) (mdbPrev_update (\<lambda>_. p'))
od \<lbrace>\<lambda>_. cte_wp_at' (Q \<circ> cteCap) ptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. cte_wp_at' (\<lambda>_. True) ptr s \<and> (if p = ptr then Q capability.NullCap else if p' = ptr then Q cap else cte_wp_at' (\<lambda>x. Q (cteCap x)) ptr s) \<Longrightarrow> cte_wp_at' (\<lambda>_. True) p' s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) p' s \<and> (mdbPrev (cteMDBNode cte) = nullPointer \<and> mdbNext (cteMDBNode cte) = nullPointer \<longrightarrow> cteCap cte = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>_. True) p s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) p s))) proof (prove)
goal:
No subgoals!
theory CNodeInv_R

lemma cap_relation_same:
  "\<lbrakk> cap_relation cap cap'; cap_relation cap cap'' \<rbrakk>
         \<Longrightarrow> cap' = cap''" by (clarsimp split: cap_relation_split_asm
                      arch_cap.split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_relation cap cap'; cap_relation cap cap''\<rbrakk> \<Longrightarrow> cap' = cap''
theory CNodeInv_R

lemma finaliseSlot_IRQInactive:
  "\<lbrace>valid_irq_states'\<rbrace> finaliseSlot a b
  -, \<lbrace>\<lambda>rv s. intStateIRQTable (ksInterruptState s) rv \<noteq> irqstate.IRQInactive\<rbrace>" apply (unfold validE_E_def) apply (rule hoare_post_impErr) apply (rule use_spec(2) [OF finaliseSlot_IRQInactive', folded finaliseSlot_def]) apply (rule TrueI) apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_irq_states'\<rbrace> finaliseSlot a b -, \<lbrace>\<lambda>rv s. intStateIRQTable (ksInterruptState s) rv \<noteq> irqstate.IRQInactive\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_irq_states'\<rbrace> finaliseSlot a b \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>rv s. intStateIRQTable (ksInterruptState s) rv \<noteq> irqstate.IRQInactive\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrace>valid_irq_states'\<rbrace> finaliseSlot a b \<lbrace>?Q\<rbrace>, \<lbrace>?E\<rbrace>
 2. \<And>rv s. ?Q rv s \<Longrightarrow> True
 3. \<And>e s. ?E e s \<Longrightarrow> intStateIRQTable (ksInterruptState s) e \<noteq> irqstate.IRQInactive proof (prove)
goal (2 subgoals):
 1. \<And>rv s. valid_irq_states' s \<Longrightarrow> True
 2. \<And>e s. intStateIRQTable (ksInterruptState s) e \<noteq> irqstate.IRQInactive \<Longrightarrow> intStateIRQTable (ksInterruptState s) e \<noteq> irqstate.IRQInactive proof (prove)
goal (1 subgoal):
 1. \<And>e s. intStateIRQTable (ksInterruptState s) e \<noteq> irqstate.IRQInactive \<Longrightarrow> intStateIRQTable (ksInterruptState s) e \<noteq> irqstate.IRQInactive proof (prove)
goal:
No subgoals!
theory CNodeInv_R

lemma finaliseSlot_irq_states':
  "\<lbrace>valid_irq_states'\<rbrace> finaliseSlot a b \<lbrace>\<lambda>rv. valid_irq_states'\<rbrace>" by (wp finaliseSlot_preservation | clarsimp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_irq_states'\<rbrace> finaliseSlot a b \<lbrace>\<lambda>rv. valid_irq_states'\<rbrace>
theory CNodeInv_R

lemma cteDelete_IRQInactive:
  "\<lbrace>valid_irq_states'\<rbrace> cteDelete x y
  -, \<lbrace>\<lambda>rv s. intStateIRQTable (ksInterruptState s) rv \<noteq> irqstate.IRQInactive\<rbrace>" apply (simp add: cteDelete_def split_def) apply (wp whenE_wp) apply (rule hoare_post_impErr) apply (rule validE_E_validE) apply (rule finaliseSlot_IRQInactive) apply simp apply simp apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_irq_states'\<rbrace> cteDelete x y -, \<lbrace>\<lambda>rv s. intStateIRQTable (ksInterruptState s) rv \<noteq> irqstate.IRQInactive\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_irq_states'\<rbrace> doE p <- finaliseSlot x y;
whenE (y \<or> fst p) (liftE (emptySlot x (snd p)))
odE -, \<lbrace>\<lambda>rv s. intStateIRQTable (ksInterruptState s) rv \<noteq> irqstate.IRQInactive\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<rbrace> finaliseSlot x y \<lbrace>\<lambda>p. if y \<or> fst p then \<lambda>s. True else (\<lambda>_. True)\<rbrace>, \<lbrace>\<lambda>rv s. intStateIRQTable (ksInterruptState s) rv \<noteq> irqstate.IRQInactive\<rbrace>
 2. \<And>s. valid_irq_states' s \<Longrightarrow> ?P' s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?P'\<rbrace> finaliseSlot x y \<lbrace>?Q6\<rbrace>, \<lbrace>?E6\<rbrace>
 2. \<And>rv s. ?Q6 rv s \<Longrightarrow> (if y \<or> fst rv then \<lambda>s. True else (\<lambda>_. True)) s
 3. \<And>e s. ?E6 e s \<Longrightarrow> intStateIRQTable (ksInterruptState s) e \<noteq> irqstate.IRQInactive
 4. \<And>s. valid_irq_states' s \<Longrightarrow> ?P' s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?P'\<rbrace> finaliseSlot x y -, \<lbrace>?E6\<rbrace>
 2. \<And>rv s. True \<Longrightarrow> (if y \<or> fst rv then \<lambda>s. True else (\<lambda>_. True)) s
 3. \<And>e s. ?E6 e s \<Longrightarrow> intStateIRQTable (ksInterruptState s) e \<noteq> irqstate.IRQInactive
 4. \<And>s. valid_irq_states' s \<Longrightarrow> ?P' s proof (prove)
goal (3 subgoals):
 1. \<And>rv s. True \<Longrightarrow> (if y \<or> fst rv then \<lambda>s. True else (\<lambda>_. True)) s
 2. \<And>e s. intStateIRQTable (ksInterruptState s) e \<noteq> irqstate.IRQInactive \<Longrightarrow> intStateIRQTable (ksInterruptState s) e \<noteq> irqstate.IRQInactive
 3. \<And>s. valid_irq_states' s \<Longrightarrow> valid_irq_states' s proof (prove)
goal (2 subgoals):
 1. \<And>e s. intStateIRQTable (ksInterruptState s) e \<noteq> irqstate.IRQInactive \<Longrightarrow> intStateIRQTable (ksInterruptState s) e \<noteq> irqstate.IRQInactive
 2. \<And>s. valid_irq_states' s \<Longrightarrow> valid_irq_states' s proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_irq_states' s \<Longrightarrow> valid_irq_states' s proof (prove)
goal:
No subgoals!
theory CNodeInv_R

lemma cteDelete_irq_states':
  "\<lbrace>valid_irq_states'\<rbrace> cteDelete x y
  \<lbrace>\<lambda>rv. valid_irq_states'\<rbrace>" apply (simp add: cteDelete_def split_def) apply (wp whenE_wp) apply (rule hoare_post_impErr) apply (rule hoare_valid_validE) apply (rule finaliseSlot_irq_states') apply simp apply simp apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_irq_states'\<rbrace> cteDelete x y \<lbrace>\<lambda>rv. valid_irq_states'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_irq_states'\<rbrace> doE p <- finaliseSlot x y;
whenE (y \<or> fst p) (liftE (emptySlot x (snd p)))
odE \<lbrace>\<lambda>rv. valid_irq_states'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> finaliseSlot x y \<lbrace>\<lambda>p. if y \<or> fst p then valid_irq_states' else valid_irq_states'\<rbrace>, \<lbrace>\<lambda>rv. valid_irq_states'\<rbrace>
 2. \<And>s. valid_irq_states' s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?Q\<rbrace> finaliseSlot x y \<lbrace>?Q6\<rbrace>, \<lbrace>?E6\<rbrace>
 2. \<And>rv s. ?Q6 rv s \<Longrightarrow> (if y \<or> fst rv then valid_irq_states' else valid_irq_states') s
 3. \<And>e s. ?E6 e s \<Longrightarrow> valid_irq_states' s
 4. \<And>s. valid_irq_states' s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?Q\<rbrace> finaliseSlot x y \<lbrace>\<lambda>_. ?E12\<rbrace>
 2. \<And>rv s. ?E12 s \<Longrightarrow> (if y \<or> fst rv then valid_irq_states' else valid_irq_states') s
 3. \<And>e s. ?E12 s \<Longrightarrow> valid_irq_states' s
 4. \<And>s. valid_irq_states' s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>rv s. valid_irq_states' s \<Longrightarrow> (if y \<or> fst rv then valid_irq_states' else valid_irq_states') s
 2. \<And>e s. valid_irq_states' s \<Longrightarrow> valid_irq_states' s
 3. \<And>s. valid_irq_states' s \<Longrightarrow> valid_irq_states' s proof (prove)
goal (2 subgoals):
 1. \<And>e s. valid_irq_states' s \<Longrightarrow> valid_irq_states' s
 2. \<And>s. valid_irq_states' s \<Longrightarrow> valid_irq_states' s proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_irq_states' s \<Longrightarrow> valid_irq_states' s proof (prove)
goal:
No subgoals!
theory CNodeInv_R

lemma cteRevoke_IRQInactive:
  "\<lbrace>valid_irq_states'\<rbrace> cteRevoke x
  -, \<lbrace>\<lambda>rv s. intStateIRQTable (ksInterruptState s) rv \<noteq> irqstate.IRQInactive\<rbrace>" apply (unfold validE_E_def) apply (rule use_spec) apply (rule cteRevoke_IRQInactive') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_irq_states'\<rbrace> cteRevoke x -, \<lbrace>\<lambda>rv s. intStateIRQTable (ksInterruptState s) rv \<noteq> irqstate.IRQInactive\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_irq_states'\<rbrace> cteRevoke x \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>rv s. intStateIRQTable (ksInterruptState s) rv \<noteq> irqstate.IRQInactive\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. s \<turnstile> \<lbrace>valid_irq_states'\<rbrace> cteRevoke x \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>rv s. intStateIRQTable (ksInterruptState s) rv \<noteq> irqstate.IRQInactive\<rbrace> proof (prove)
goal:
No subgoals!
theory Tcb_R

lemma asUser_setNextPC_corres:
  "corres dc (tcb_at t and invs) (tcb_at' t and invs')
             (as_user t (setNextPC v)) (asUser t (setNextPC v))" apply (rule asUser_corres) apply (rule corres_Id, simp, simp) apply (rule no_fail_setNextPC) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (tcb_at t and invs) (tcb_at' t and invs') (as_user t (setNextPC v)) (asUser t (setNextPC v)) proof (prove)
goal (1 subgoal):
 1. corres_underlying Id False True dc (\<lambda>_. True) (\<lambda>_. True) (setNextPC v) (setNextPC v) proof (prove)
goal (1 subgoal):
 1. True \<Longrightarrow> no_fail (\<lambda>_. True) (setNextPC v) proof (prove)
goal:
No subgoals!
theory Tcb_R

lemma activateIdleThread_corres:
 "corres dc (invs and st_tcb_at idle t)
            (invs' and st_tcb_at' idle' t)
    (arch_activate_idle_thread t) (activateIdleThread t)" by (simp add: arch_activate_idle_thread_def activateIdleThread_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (invs and st_tcb_at idle t) (invs' and st_tcb_at' idle' t) (arch_activate_idle_thread t) (activateIdleThread t)
theory Tcb_R

lemma gts_st_tcb':
  "\<lbrace>tcb_at' t\<rbrace> getThreadState t \<lbrace>\<lambda>rv. st_tcb_at' (\<lambda>st. st = rv) t\<rbrace>" apply (rule hoare_vcg_precond_imp) apply (rule hoare_post_imp[where Q="\<lambda>rv s. \<exists>rv'. rv = rv' \<and> st_tcb_at' (\<lambda>st. st = rv') t s"]) apply simp apply (wp hoare_vcg_ex_lift) apply (clarsimp simp add: pred_tcb_at'_def obj_at'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_at' t\<rbrace> getThreadState t \<lbrace>\<lambda>rv. st_tcb_at' (\<lambda>st. st = rv) t\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> getThreadState t \<lbrace>\<lambda>rv. st_tcb_at' (\<lambda>st. st = rv) t\<rbrace>
 2. \<And>s. tcb_at' t s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>rv s. \<exists>rv'. rv = rv' \<and> st_tcb_at' (\<lambda>st. st = rv') t s \<Longrightarrow> st_tcb_at' (\<lambda>st. st = rv) t s
 2. \<lbrace>?Q\<rbrace> getThreadState t \<lbrace>\<lambda>rv s. \<exists>rv'. rv = rv' \<and> st_tcb_at' (\<lambda>st. st = rv') t s\<rbrace>
 3. \<And>s. tcb_at' t s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> getThreadState t \<lbrace>\<lambda>rv s. \<exists>rv'. rv = rv' \<and> st_tcb_at' (\<lambda>st. st = rv') t s\<rbrace>
 2. \<And>s. tcb_at' t s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. tcb_at' t s \<Longrightarrow> \<exists>x. st_tcb_at' (\<lambda>rv. rv = x) t s \<and> st_tcb_at' (\<lambda>st. st = x) t s proof (prove)
goal:
No subgoals!
theory Tcb_R

lemma activateIdle_invs:
  "\<lbrace>invs' and ct_idle'\<rbrace>
     activateIdleThread thread
   \<lbrace>\<lambda>rv. invs' and ct_idle'\<rbrace>" by (simp add: activateIdleThread_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and ct_idle'\<rbrace> activateIdleThread thread \<lbrace>\<lambda>rv. invs' and ct_idle'\<rbrace>
theory Tcb_R

lemma runnable_tsr:
  "thread_state_relation ts ts' \<Longrightarrow> runnable' ts' = runnable ts" by (case_tac ts, auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. thread_state_relation ts ts' \<Longrightarrow> runnable' ts' = runnable ts
theory Tcb_R

lemma idle_tsr:
  "thread_state_relation ts ts' \<Longrightarrow> idle' ts' = idle ts" by (case_tac ts, auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. thread_state_relation ts ts' \<Longrightarrow> idle' ts' = idle ts
theory Tcb_R

lemma setCTE_weak_sch_act_wf[wp]:
  "\<lbrace>\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>
   setCTE c cte
   \<lbrace>\<lambda>rv s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>" apply (simp add: weak_sch_act_wf_def) apply (wp hoare_vcg_all_lift hoare_convert_imp setCTE_pred_tcb_at' setCTE_tcb_in_cur_domain') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace> setCTE c cte \<lbrace>\<lambda>rv s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>t. ksSchedulerAction s = SwitchToThread t \<longrightarrow> st_tcb_at' runnable' t s \<and> tcb_in_cur_domain' t s\<rbrace> setCTE c cte \<lbrace>\<lambda>rv s. \<forall>t. ksSchedulerAction s = SwitchToThread t \<longrightarrow> st_tcb_at' runnable' t s \<and> tcb_in_cur_domain' t s\<rbrace> proof (prove)
goal:
No subgoals!
theory Tcb_R

lemma setupReplyMaster_weak_sch_act_wf[wp]:
  "\<lbrace>\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>
   setupReplyMaster thread
   \<lbrace>\<lambda>rv s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>" apply (simp add: setupReplyMaster_def) apply (wp) apply (rule_tac Q="\<lambda>_ s. weak_sch_act_wf (ksSchedulerAction s) s"
               in hoare_post_imp, clarsimp) apply (wp)+ apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace> setupReplyMaster thread \<lbrace>\<lambda>rv s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace> do slot <- locateSlotTCB thread tcbReplySlot;
oldCTE <- getCTE slot;
when (cteCap oldCTE = capability.NullCap) (do y <- stateAssert (noReplyCapsFor thread) [];
setCTE slot (CTE (capability.ReplyCap thread True True) (mdbFirstBadged_update (\<lambda>_. True) (mdbRevocable_update (\<lambda>_. True) nullMDBNode)))
od)
od \<lbrace>\<lambda>rv s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>slot. \<lbrace>?B1 slot\<rbrace> getCTE slot \<lbrace>\<lambda>oldCTE. if cteCap oldCTE = capability.NullCap then \<lambda>s. noReplyCapsFor thread s \<longrightarrow> weak_sch_act_wf (ksSchedulerAction s) s else (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)\<rbrace>
 2. \<lbrace>?Q\<rbrace> locateSlotTCB thread tcbReplySlot \<lbrace>?B1\<rbrace>
 3. \<And>s. weak_sch_act_wf (ksSchedulerAction s) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>slot. \<lbrace>?B1 slot\<rbrace> getCTE slot \<lbrace>\<lambda>_ s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>
 2. \<lbrace>?Q\<rbrace> locateSlotTCB thread tcbReplySlot \<lbrace>?B1\<rbrace>
 3. \<And>s. weak_sch_act_wf (ksSchedulerAction s) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. weak_sch_act_wf (ksSchedulerAction s) s \<Longrightarrow> weak_sch_act_wf (ksSchedulerAction s) s proof (prove)
goal:
No subgoals!