kings-crown/FVELER_Isabelle huggingface dataset:
theory VSpace_R

lemma dmo_invalidateLocalTLB_VAASID_invs'[wp]:
  "\<lbrace>invs'\<rbrace> doMachineOp (invalidateLocalTLB_VAASID x) \<lbrace>\<lambda>_. invs'\<rbrace>" apply (wp dmo_invs' no_irq_invalidateLocalTLB_VAASID no_irq) apply clarsimp apply (drule_tac Q="\<lambda>_ m'. underlying_memory m' p = underlying_memory m p"
         in use_valid) apply (clarsimp simp: invalidateLocalTLB_VAASID_def machine_op_lift_def
                          machine_rest_lift_def split_def | wp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> doMachineOp (invalidateLocalTLB_VAASID x) \<lbrace>\<lambda>_. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. invs' s \<Longrightarrow> ((\<lambda>s. \<forall>m. \<forall>(r, m')\<in>fst (invalidateLocalTLB_VAASID x m). \<forall>p. pointerInUserData p s \<or> pointerInDeviceData p s \<or> underlying_memory m' p = underlying_memory m p) and invs') s proof (prove)
goal (1 subgoal):
 1. \<And>s m b p. \<lbrakk>invs' s; ((), b) \<in> fst (invalidateLocalTLB_VAASID x m); \<not> pointerInUserData p s; underlying_memory b p \<noteq> underlying_memory m p\<rbrakk> \<Longrightarrow> pointerInDeviceData p s proof (prove)
goal (3 subgoals):
 1. \<And>s m b p. \<lbrakk>invs' s; \<not> pointerInUserData p s; underlying_memory b p \<noteq> underlying_memory m p\<rbrakk> \<Longrightarrow> \<lbrace>?P13 s m b p\<rbrace> invalidateLocalTLB_VAASID x \<lbrace>\<lambda>_ m'. underlying_memory m' p = underlying_memory m p\<rbrace>
 2. \<And>s m b p. \<lbrakk>invs' s; \<not> pointerInUserData p s; underlying_memory b p \<noteq> underlying_memory m p\<rbrakk> \<Longrightarrow> ?P13 s m b p m
 3. \<And>s m b p. \<lbrakk>invs' s; \<not> pointerInUserData p s; underlying_memory b p \<noteq> underlying_memory m p; underlying_memory b p = underlying_memory m p\<rbrakk> \<Longrightarrow> pointerInDeviceData p s proof (prove)
goal:
No subgoals!
theory VSpace_R

lemma dmo_cVA_PoU_invs'[wp]:
  "\<lbrace>invs'\<rbrace> doMachineOp (cleanByVA_PoU w p) \<lbrace>\<lambda>_. invs'\<rbrace>" apply (wp dmo_invs' no_irq_cleanByVA_PoU no_irq) apply clarsimp apply (drule_tac Q="\<lambda>_ m'. underlying_memory m' pa = underlying_memory m pa"
         in use_valid) apply (clarsimp simp: cleanByVA_PoU_def machine_op_lift_def
                          machine_rest_lift_def split_def | wp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> doMachineOp (cleanByVA_PoU w p) \<lbrace>\<lambda>_. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. invs' s \<Longrightarrow> ((\<lambda>s. \<forall>m. \<forall>(r, m')\<in>fst (cleanByVA_PoU w p m). \<forall>p. pointerInUserData p s \<or> pointerInDeviceData p s \<or> underlying_memory m' p = underlying_memory m p) and invs') s proof (prove)
goal (1 subgoal):
 1. \<And>s m b pa. \<lbrakk>invs' s; ((), b) \<in> fst (cleanByVA_PoU w p m); \<not> pointerInUserData pa s; underlying_memory b pa \<noteq> underlying_memory m pa\<rbrakk> \<Longrightarrow> pointerInDeviceData pa s proof (prove)
goal (3 subgoals):
 1. \<And>s m b pa. \<lbrakk>invs' s; \<not> pointerInUserData pa s; underlying_memory b pa \<noteq> underlying_memory m pa\<rbrakk> \<Longrightarrow> \<lbrace>?P13 s m b pa\<rbrace> cleanByVA_PoU w p \<lbrace>\<lambda>_ m'. underlying_memory m' pa = underlying_memory m pa\<rbrace>
 2. \<And>s m b p. \<lbrakk>invs' s; \<not> pointerInUserData p s; underlying_memory b p \<noteq> underlying_memory m p\<rbrakk> \<Longrightarrow> ?P13 s m b p m
 3. \<And>s m b p. \<lbrakk>invs' s; \<not> pointerInUserData p s; underlying_memory b p \<noteq> underlying_memory m p; underlying_memory b p = underlying_memory m p\<rbrakk> \<Longrightarrow> pointerInDeviceData p s proof (prove)
goal:
No subgoals!
theory VSpace_R

lemma dmo_ccr_PoU_invs'[wp]:
  "\<lbrace>invs'\<rbrace> doMachineOp (cleanCacheRange_PoU s e p) \<lbrace>\<lambda>r. invs'\<rbrace>" apply (wp dmo_invs' no_irq_cleanCacheRange_PoU no_irq) apply clarsimp apply (drule_tac Q="\<lambda>_ m'. underlying_memory m' pa = underlying_memory m pa"
         in use_valid) apply (clarsimp simp: cleanCacheRange_PoU_def machine_op_lift_def
                          machine_rest_lift_def split_def | wp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> doMachineOp (cleanCacheRange_PoU s e p) \<lbrace>\<lambda>r. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>sa. invs' sa \<Longrightarrow> ((\<lambda>sa. \<forall>m. \<forall>(r, m')\<in>fst (cleanCacheRange_PoU s e p m). \<forall>p. pointerInUserData p sa \<or> pointerInDeviceData p sa \<or> underlying_memory m' p = underlying_memory m p) and invs') sa proof (prove)
goal (1 subgoal):
 1. \<And>sa m b pa. \<lbrakk>invs' sa; ((), b) \<in> fst (cleanCacheRange_PoU s e p m); \<not> pointerInUserData pa sa; underlying_memory b pa \<noteq> underlying_memory m pa\<rbrakk> \<Longrightarrow> pointerInDeviceData pa sa proof (prove)
goal (3 subgoals):
 1. \<And>sa m b pa. \<lbrakk>invs' sa; \<not> pointerInUserData pa sa; underlying_memory b pa \<noteq> underlying_memory m pa\<rbrakk> \<Longrightarrow> \<lbrace>?P13 sa m b pa\<rbrace> cleanCacheRange_PoU s e p \<lbrace>\<lambda>_ m'. underlying_memory m' pa = underlying_memory m pa\<rbrace>
 2. \<And>s m b p. \<lbrakk>invs' s; \<not> pointerInUserData p s; underlying_memory b p \<noteq> underlying_memory m p\<rbrakk> \<Longrightarrow> ?P13 s m b p m
 3. \<And>s m b p. \<lbrakk>invs' s; \<not> pointerInUserData p s; underlying_memory b p \<noteq> underlying_memory m p; underlying_memory b p = underlying_memory m p\<rbrakk> \<Longrightarrow> pointerInDeviceData p s proof (prove)
goal:
No subgoals!
theory VSpace_R

lemma dmo_invalidateLocalTLB_ASID_invs'[wp]:
  "\<lbrace>invs'\<rbrace> doMachineOp (invalidateLocalTLB_ASID a) \<lbrace>\<lambda>_. invs'\<rbrace>" apply (wp dmo_invs' no_irq_invalidateLocalTLB_ASID no_irq) apply clarsimp apply (drule_tac P4="\<lambda>m'. underlying_memory m' p = underlying_memory m p"
         in use_valid[where P=P and Q="\<lambda>_. P" for P]) apply (simp add: invalidateLocalTLB_ASID_def machine_op_lift_def
                     machine_rest_lift_def split_def | wp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> doMachineOp (invalidateLocalTLB_ASID a) \<lbrace>\<lambda>_. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. invs' s \<Longrightarrow> ((\<lambda>s. \<forall>m. \<forall>(r, m')\<in>fst (invalidateLocalTLB_ASID a m). \<forall>p. pointerInUserData p s \<or> pointerInDeviceData p s \<or> underlying_memory m' p = underlying_memory m p) and invs') s proof (prove)
goal (1 subgoal):
 1. \<And>s m b p. \<lbrakk>invs' s; ((), b) \<in> fst (invalidateLocalTLB_ASID a m); \<not> pointerInUserData p s; underlying_memory b p \<noteq> underlying_memory m p\<rbrakk> \<Longrightarrow> pointerInDeviceData p s proof (prove)
goal (3 subgoals):
 1. \<And>s m b p. \<lbrakk>invs' s; \<not> pointerInUserData p s; underlying_memory b p \<noteq> underlying_memory m p\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>m'. underlying_memory m' p = underlying_memory m p\<rbrace> invalidateLocalTLB_ASID a \<lbrace>\<lambda>_ m'. underlying_memory m' p = underlying_memory m p\<rbrace>
 2. \<And>s m b p. \<lbrakk>invs' s; \<not> pointerInUserData p s; underlying_memory b p \<noteq> underlying_memory m p\<rbrakk> \<Longrightarrow> underlying_memory m p = underlying_memory m p
 3. \<And>s m b p. \<lbrakk>invs' s; \<not> pointerInUserData p s; underlying_memory b p \<noteq> underlying_memory m p; underlying_memory b p = underlying_memory m p\<rbrakk> \<Longrightarrow> pointerInDeviceData p s proof (prove)
goal:
No subgoals!
theory VSpace_R

lemma dmo_cleanCaches_PoU_invs'[wp]:
  "\<lbrace>invs'\<rbrace> doMachineOp cleanCaches_PoU \<lbrace>\<lambda>_. invs'\<rbrace>" apply (wp dmo_invs' no_irq_cleanCaches_PoU no_irq) apply clarsimp apply (drule_tac P4="\<lambda>m'. underlying_memory m' p = underlying_memory m p"
         in use_valid[where P=P and Q="\<lambda>_. P" for P]) apply (simp add: cleanCaches_PoU_def machine_op_lift_def
                     machine_rest_lift_def split_def | wp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> doMachineOp cleanCaches_PoU \<lbrace>\<lambda>_. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. invs' s \<Longrightarrow> ((\<lambda>s. \<forall>m. \<forall>(r, m')\<in>fst (cleanCaches_PoU m). \<forall>p. pointerInUserData p s \<or> pointerInDeviceData p s \<or> underlying_memory m' p = underlying_memory m p) and invs') s proof (prove)
goal (1 subgoal):
 1. \<And>s m b p. \<lbrakk>invs' s; ((), b) \<in> fst (cleanCaches_PoU m); \<not> pointerInUserData p s; underlying_memory b p \<noteq> underlying_memory m p\<rbrakk> \<Longrightarrow> pointerInDeviceData p s proof (prove)
goal (3 subgoals):
 1. \<And>s m b p. \<lbrakk>invs' s; \<not> pointerInUserData p s; underlying_memory b p \<noteq> underlying_memory m p\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>m'. underlying_memory m' p = underlying_memory m p\<rbrace> cleanCaches_PoU \<lbrace>\<lambda>_ m'. underlying_memory m' p = underlying_memory m p\<rbrace>
 2. \<And>s m b p. \<lbrakk>invs' s; \<not> pointerInUserData p s; underlying_memory b p \<noteq> underlying_memory m p\<rbrakk> \<Longrightarrow> underlying_memory m p = underlying_memory m p
 3. \<And>s m b p. \<lbrakk>invs' s; \<not> pointerInUserData p s; underlying_memory b p \<noteq> underlying_memory m p; underlying_memory b p = underlying_memory m p\<rbrakk> \<Longrightarrow> pointerInDeviceData p s proof (prove)
goal:
No subgoals!
theory VSpace_R

lemma mapM_storePTE_invs:
  "\<lbrace>invs' and valid_pte' pte\<rbrace> mapM (swp storePTE pte) ps \<lbrace>\<lambda>xa. invs'\<rbrace>" apply (rule hoare_post_imp) prefer 2 apply (rule mapM_wp') apply simp apply (wp valid_pte_lift') apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and valid_pte' pte\<rbrace> mapM (swp storePTE pte) ps \<lbrace>\<lambda>xa. invs'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv s. ?Q rv s \<Longrightarrow> invs' s
 2. \<lbrace>invs' and valid_pte' pte\<rbrace> mapM (swp storePTE pte) ps \<lbrace>?Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>invs' and valid_pte' pte\<rbrace> mapM (swp storePTE pte) ps \<lbrace>?Q\<rbrace>
 2. \<And>rv s. ?Q rv s \<Longrightarrow> invs' s proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> set ps \<Longrightarrow> \<lbrace>invs' and valid_pte' pte\<rbrace> swp storePTE pte x \<lbrace>\<lambda>rv. invs' and valid_pte' pte\<rbrace>
 2. \<And>rv s. (invs' and valid_pte' pte) s \<Longrightarrow> invs' s proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> set ps \<Longrightarrow> \<lbrace>invs' and valid_pte' pte\<rbrace> storePTE x pte \<lbrace>\<lambda>rv. invs' and valid_pte' pte\<rbrace>
 2. \<And>rv s. (invs' and valid_pte' pte) s \<Longrightarrow> invs' s proof (prove)
goal (2 subgoals):
 1. \<And>x s. \<lbrakk>x \<in> set ps; (invs' and valid_pte' pte) s\<rbrakk> \<Longrightarrow> (invs' and valid_pte' pte) s \<and> valid_pte' pte s
 2. \<And>rv s. (invs' and valid_pte' pte) s \<Longrightarrow> invs' s proof (prove)
goal:
No subgoals!
theory VSpace_R

lemma mapM_storePDE_invs:
  "\<lbrace>invs' and valid_pde' pde
       and K (\<forall>p \<in> set ps. valid_pde_mapping' (p && mask pdBits) pde)\<rbrace>
       mapM (swp storePDE pde) ps \<lbrace>\<lambda>xa. invs'\<rbrace>" apply (rule hoare_post_imp) prefer 2 apply (rule mapM_wp') apply simp apply (wp valid_pde_lift') apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and valid_pde' pde and K (\<forall>p\<in>set ps. valid_pde_mapping' (p && mask pdBits) pde)\<rbrace> mapM (swp storePDE pde) ps \<lbrace>\<lambda>xa. invs'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv s. ?Q rv s \<Longrightarrow> invs' s
 2. \<lbrace>invs' and valid_pde' pde and K (\<forall>p\<in>set ps. valid_pde_mapping' (p && mask pdBits) pde)\<rbrace> mapM (swp storePDE pde) ps \<lbrace>?Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>invs' and valid_pde' pde and K (\<forall>p\<in>set ps. valid_pde_mapping' (p && mask pdBits) pde)\<rbrace> mapM (swp storePDE pde) ps \<lbrace>?Q\<rbrace>
 2. \<And>rv s. ?Q rv s \<Longrightarrow> invs' s proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> set ps \<Longrightarrow> \<lbrace>invs' and valid_pde' pde and K (\<forall>p\<in>set ps. valid_pde_mapping' (p && mask pdBits) pde)\<rbrace> swp storePDE pde x \<lbrace>\<lambda>rv. invs' and valid_pde' pde and K (\<forall>p\<in>set ps. valid_pde_mapping' (p && mask pdBits) pde)\<rbrace>
 2. \<And>rv s. (invs' and valid_pde' pde and K (\<forall>p\<in>set ps. valid_pde_mapping' (p && mask pdBits) pde)) s \<Longrightarrow> invs' s proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> set ps \<Longrightarrow> \<lbrace>invs' and valid_pde' pde and (\<lambda>y. \<forall>p\<in>set ps. valid_pde_mapping' (p && mask pdBits) pde)\<rbrace> storePDE x pde \<lbrace>\<lambda>rv. invs' and valid_pde' pde and (\<lambda>y. \<forall>p\<in>set ps. valid_pde_mapping' (p && mask pdBits) pde)\<rbrace>
 2. \<And>rv s. (invs' and valid_pde' pde and K (\<forall>p\<in>set ps. valid_pde_mapping' (p && mask pdBits) pde)) s \<Longrightarrow> invs' s proof (prove)
goal (2 subgoals):
 1. \<And>x s. \<lbrakk>x \<in> set ps; (invs' and valid_pde' pde and (\<lambda>y. \<forall>p\<in>set ps. valid_pde_mapping' (p && mask pdBits) pde)) s\<rbrakk> \<Longrightarrow> (invs' and valid_pde' pde and (\<lambda>s. valid_pde_mapping' (x && mask pdBits) pde)) s \<and> valid_pde' pde s \<and> (\<forall>p\<in>set ps. valid_pde_mapping' (p && mask pdBits) pde)
 2. \<And>rv s. (invs' and valid_pde' pde and K (\<forall>p\<in>set ps. valid_pde_mapping' (p && mask pdBits) pde)) s \<Longrightarrow> invs' s proof (prove)
goal:
No subgoals!
theory VSpace_R

lemma flushPage_invs' [wp]:
  "\<lbrace>invs'\<rbrace> flushPage sz pd asid vptr \<lbrace>\<lambda>_. invs'\<rbrace>" apply (simp add: flushPage_def) apply (wp dmo_invalidateLocalTLB_VAASID_invs' hoare_drop_imps setVMRootForFlush_invs'
            no_irq_invalidateLocalTLB_VAASID
         |simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> flushPage sz pd asid vptr \<lbrace>\<lambda>_. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> do y <- assert (vptr && mask pageBits = 0);
root_switched <- setVMRootForFlush pd asid;
maybe_hw_asid <- loadHWASID asid;
when (\<exists>y. maybe_hw_asid = Some y) (do y <- doMachineOp (invalidateLocalTLB_VAASID (vptr || UCAST(8 \<rightarrow> 32) (the maybe_hw_asid)));
when root_switched (getCurThread >>= setVMRoot)
od)
od \<lbrace>\<lambda>_. invs'\<rbrace> proof (prove)
goal:
No subgoals!
theory VSpace_R

lemma ucast_ucast_le_low_bits [simp]:
  "ucast (ucast x :: 10 word) \<le> (2 ^ asid_low_bits - 1 :: word32)" apply (rule word_less_sub_1) apply (rule order_less_le_trans) apply (rule ucast_less) apply simp apply (simp add: asid_low_bits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. UCAST(10 \<rightarrow> 32) (UCAST('a \<rightarrow> 10) x) \<le> 2 ^ local.asid_low_bits - 1 proof (prove)
goal (1 subgoal):
 1. UCAST(10 \<rightarrow> 32) (UCAST('a \<rightarrow> 10) x) < 2 ^ local.asid_low_bits proof (prove)
goal (2 subgoals):
 1. UCAST(10 \<rightarrow> 32) (UCAST('a \<rightarrow> 10) x) < ?y2
 2. ?y2 \<le> 2 ^ local.asid_low_bits proof (prove)
goal (2 subgoals):
 1. LENGTH(10) < LENGTH(32)
 2. 2 ^ LENGTH(10) \<le> 2 ^ local.asid_low_bits proof (prove)
goal (1 subgoal):
 1. 2 ^ LENGTH(10) \<le> 2 ^ local.asid_low_bits proof (prove)
goal:
No subgoals!
theory VSpace_R

lemma capMaster_isPDCap:
  "capMasterCap cap' = capMasterCap cap \<Longrightarrow> isPDCap cap' = isPDCap cap" by (simp add: capMasterCap_def isPDCap_def split: capability.splits arch_capability.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. capMasterCap cap' = capMasterCap cap \<Longrightarrow> isPDCap cap' = isPDCap cap
theory VSpace_R

lemma isPDCap_PD :
  "isPDCap (ArchObjectCap (PageDirectoryCap r m))" by (simp add: isPDCap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isPDCap (capability.ArchObjectCap (arch_capability.PageDirectoryCap r m))
theory VSpace_R

lemma cteCaps_of_ctes_of_lift:
  "(\<And>P. \<lbrace>\<lambda>s. P (ctes_of s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ctes_of s)\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. P (cteCaps_of s) \<rbrace> f \<lbrace>\<lambda>_ s. P (cteCaps_of s)\<rbrace>" unfolding cteCaps_of_def .

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>P. \<lbrace>\<lambda>s. P (ctes_of s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ctes_of s)\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. P (cteCaps_of s)\<rbrace> f \<lbrace>\<lambda>_ s. P (cteCaps_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. (\<And>P. \<lbrace>\<lambda>s. P (ctes_of s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ctes_of s)\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. P (map_option cteCap \<circ> ctes_of s)\<rbrace> f \<lbrace>\<lambda>_ s. P (map_option cteCap \<circ> ctes_of s)\<rbrace>
theory Schedule_R

lemma invs_no_cicd'_queues:
  "invs_no_cicd' s \<Longrightarrow> valid_queues s" unfolding invs_no_cicd'_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. all_invs_but_ct_idle_or_in_cur_domain' s \<Longrightarrow> Invariants_H.valid_queues s proof (prove)
goal (1 subgoal):
 1. valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> irqs_masked' s \<and> valid_machine_state' s \<and> cur_tcb' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> valid_dom_schedule' s \<and> untyped_ranges_zero' s \<Longrightarrow> Invariants_H.valid_queues s
theory Schedule_R

lemma corres_if2:
 "\<lbrakk> G = G'; G \<Longrightarrow> corres r P P' a c; \<not> G' \<Longrightarrow> corres r Q Q' b d \<rbrakk>
    \<Longrightarrow> corres r (if G then P else Q) (if G' then P' else Q') (if G then a else b) (if G' then c else d)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>G = G'; G \<Longrightarrow> corres r P P' a c; \<not> G' \<Longrightarrow> corres r Q Q' b d\<rbrakk> \<Longrightarrow> corres r (if G then P else Q) (if G' then P' else Q') (if G then a else b) (if G' then c else d)
theory Schedule_R

lemma schedule_choose_new_thread_sched_act_rct[wp]:
  "\<lbrace>\<top>\<rbrace> schedule_choose_new_thread \<lbrace>\<lambda>rs s. scheduler_action s = resume_cur_thread\<rbrace>" unfolding schedule_choose_new_thread_def by wp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> schedule_choose_new_thread \<lbrace>\<lambda>rs s. scheduler_action s = resume_cur_thread\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> do dom_time <- gets domain_time;
when (dom_time = 0) next_domain;
choose_thread;
set_scheduler_action resume_cur_thread
od \<lbrace>\<lambda>rs s. scheduler_action s = resume_cur_thread\<rbrace>
theory Schedule_R

lemma removeFromBitmap_valid_queues_no_bitmap_except[wp]:
" \<lbrace> valid_queues_no_bitmap_except t \<rbrace>
     removeFromBitmap d p
  \<lbrace>\<lambda>_. valid_queues_no_bitmap_except t \<rbrace>" unfolding bitmapQ_defs valid_queues_no_bitmap_except_def by (wp | clarsimp simp: bitmap_fun_defs)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_queues_no_bitmap_except t\<rbrace> removeFromBitmap d p \<lbrace>\<lambda>_. valid_queues_no_bitmap_except t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>d p. (\<forall>ta\<in>set (ksReadyQueues s (d, p)). ta \<noteq> t \<longrightarrow> obj_at' (inQ d p and runnable' \<circ> tcbState) ta s) \<and> distinct (ksReadyQueues s (d, p)) \<and> (maxDomain < d \<or> maxPriority < p \<longrightarrow> ksReadyQueues s (d, p) = [])\<rbrace> removeFromBitmap d p \<lbrace>\<lambda>_ s. \<forall>d p. (\<forall>ta\<in>set (ksReadyQueues s (d, p)). ta \<noteq> t \<longrightarrow> obj_at' (inQ d p and runnable' \<circ> tcbState) ta s) \<and> distinct (ksReadyQueues s (d, p)) \<and> (maxDomain < d \<or> maxPriority < p \<longrightarrow> ksReadyQueues s (d, p) = [])\<rbrace>
theory Schedule_R

lemma removeFromBitmap_bitmapQ:
  "\<lbrace> \<lambda>s. True \<rbrace> removeFromBitmap d p \<lbrace>\<lambda>_ s. \<not> bitmapQ d p s \<rbrace>" unfolding bitmapQ_defs bitmap_fun_defs by (wpsimp simp: bitmap_fun_defs wordRadix_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. True\<rbrace> removeFromBitmap d p \<lbrace>\<lambda>_ s. \<not> bitmapQ d p s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. True\<rbrace> do l1index <- return (prioToL1Index p);
l1indexInverted <- return (invertL1Index l1index);
l2bit <- return (fromIntegral (fromIntegral p && mask wordRadix));
(\<lambda>f. do l2 <- gets (\<lambda>ks. ksReadyQueuesL2Bitmap ks (d, l1indexInverted));
modify (\<lambda>ks. ks\<lparr>ksReadyQueuesL2Bitmap := ksReadyQueuesL2Bitmap ks aLU [((d, l1indexInverted), f l2)]\<rparr>)
od) $ (\<lambda>w. w && (wordNOT $ HaskellLib_H.bit l2bit));
l2 <- gets (\<lambda>ks. ksReadyQueuesL2Bitmap ks (d, l1indexInverted));
when (l2 = 0) $ (\<lambda>f. do l1 <- gets (\<lambda>ks. ksReadyQueuesL1Bitmap ks d);
modify (\<lambda>ks. ks\<lparr>ksReadyQueuesL1Bitmap := ksReadyQueuesL1Bitmap ks aLU [(d, f l1)]\<rparr>)
od) $ (\<lambda>w. w && (wordNOT $ HaskellLib_H.bit l1index))
od \<lbrace>\<lambda>_ s. \<not> (ksReadyQueuesL1Bitmap s d !! prioToL1Index p \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) !! unat (p && mask wordRadix))\<rbrace>
theory Schedule_R

lemma setQueue_valid_queues_no_bitmap_except_dequeue_wp:
  "\<And>d p ts t.
   \<lbrace> \<lambda>s. valid_queues_no_bitmap_except t s \<and>
         (\<forall>t' \<in> set ts. obj_at' (inQ d p and runnable' \<circ> tcbState) t' s) \<and>
         t \<notin> set ts \<and> distinct ts \<and> p \<le> maxPriority \<and> d \<le> maxDomain \<rbrace>
       setQueue d p ts
   \<lbrace>\<lambda>rv. valid_queues_no_bitmap_except t \<rbrace>" unfolding setQueue_def valid_queues_no_bitmap_except_def null_def by wp force

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>d p ts t. \<lbrace>\<lambda>s. valid_queues_no_bitmap_except t s \<and> (\<forall>t'\<in>set ts. obj_at' (inQ d p and runnable' \<circ> tcbState) t' s) \<and> t \<notin> set ts \<and> distinct ts \<and> p \<le> maxPriority \<and> d \<le> maxDomain\<rbrace> setQueue d p ts \<lbrace>\<lambda>rv. valid_queues_no_bitmap_except t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>d p ts t. \<lbrace>\<lambda>s. (\<forall>d p. (\<forall>ta\<in>set (ksReadyQueues s (d, p)). ta \<noteq> t \<longrightarrow> obj_at' (inQ d p and runnable' \<circ> tcbState) ta s) \<and> distinct (ksReadyQueues s (d, p)) \<and> (maxDomain < d \<or> maxPriority < p \<longrightarrow> ksReadyQueues s (d, p) = [])) \<and> (\<forall>t'\<in>set ts. obj_at' (inQ d p and runnable' \<circ> tcbState) t' s) \<and> t \<notin> set ts \<and> distinct ts \<and> p \<le> maxPriority \<and> d \<le> maxDomain\<rbrace> modify (\<lambda>ks. ks\<lparr>ksReadyQueues := ksReadyQueues ks aLU [((d, p), ts)]\<rparr>) \<lbrace>\<lambda>rv s. \<forall>d p. (\<forall>ta\<in>set (ksReadyQueues s (d, p)). ta \<noteq> t \<longrightarrow> obj_at' (inQ d p and runnable' \<circ> tcbState) ta s) \<and> distinct (ksReadyQueues s (d, p)) \<and> (maxDomain < d \<or> maxPriority < p \<longrightarrow> ksReadyQueues s (d, p) = [])\<rbrace>