theory ArchVSpace_AI

lemma arm_context_switch_invs [wp]:
  "\<lbrace>invs and K (a \<le> mask asid_bits)\<rbrace> arm_context_switch pd a \<lbrace>\<lambda>_. invs\<rbrace>" apply (simp add: arm_context_switch_def) apply (wp dmo_invs) apply (rule hoare_post_imp[rotated]) apply (rule get_hw_asid_invs[simplified]) apply safe apply (drule_tac Q="\<lambda>_ m'. underlying_memory m' p = underlying_memory m p"
          in use_valid) apply ((clarsimp simp: setHardwareASID_def set_current_pd_def writeTTBR0_def
                            isb_def dsb_def machine_op_lift_def
                            machine_rest_lift_def split_def | wp)+)[3] apply(erule use_valid) apply(wp no_irq | simp add: no_irq_setHardwareASID no_irq_set_current_pd)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and K (a \<le> mask local.asid_bits)\<rbrace> arm_context_switch pd a \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and (\<lambda>y. a \<le> mask local.asid_bits)\<rbrace> do hwasid <- get_hw_asid a;
do_machine_op (do y <- set_current_pd (addrFromPPtr pd);
setHardwareASID hwasid
od)
od \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> get_hw_asid a \<lbrace>\<lambda>hwasid s. \<forall>m. \<forall>(r, m')\<in>fst ((do y <- set_current_pd (addrFromPPtr pd);
setHardwareASID hwasid
od) m). (\<forall>p. in_user_frame p s \<or> underlying_memory m' p = underlying_memory m p) \<and> (\<forall>irq. m = machine_state s \<longrightarrow> (interrupt_states s irq = IRQInactive \<longrightarrow> irq_masks m' irq) \<or> irq_masks m' irq = irq_masks m irq) \<and> invs s\<rbrace>
 2. \<And>s. (invs and (\<lambda>y. a \<le> mask local.asid_bits)) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?Q\<rbrace> get_hw_asid a \<lbrace>?Q10\<rbrace>
 2. \<And>rv s. ?Q10 rv s \<Longrightarrow> \<forall>m. \<forall>(r, m')\<in>fst ((do y <- set_current_pd (addrFromPPtr pd);
setHardwareASID rv
od) m). (\<forall>p. in_user_frame p s \<or> underlying_memory m' p = underlying_memory m p) \<and> (\<forall>irq. m = machine_state s \<longrightarrow> (interrupt_states s irq = IRQInactive \<longrightarrow> irq_masks m' irq) \<or> irq_masks m' irq = irq_masks m irq) \<and> invs s
 3. \<And>s. (invs and (\<lambda>y. a \<le> mask local.asid_bits)) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<And>rv s. invs s \<Longrightarrow> \<forall>m. \<forall>(r, m')\<in>fst ((do y <- set_current_pd (addrFromPPtr pd);
setHardwareASID rv
od) m). (\<forall>p. in_user_frame p s \<or> underlying_memory m' p = underlying_memory m p) \<and> (\<forall>irq. m = machine_state s \<longrightarrow> (interrupt_states s irq = IRQInactive \<longrightarrow> irq_masks m' irq) \<or> irq_masks m' irq = irq_masks m irq) \<and> invs s
 2. \<And>s. (invs and (\<lambda>y. a \<le> mask local.asid_bits)) s \<Longrightarrow> (invs and (\<lambda>y. a \<le> mask local.asid_bits)) s proof (prove)
goal (2 subgoals):
 1. \<And>rv s m b p. \<lbrakk>invs s; ((), b) \<in> fst ((do y <- set_current_pd (addrFromPPtr pd);
setHardwareASID rv
od) m); underlying_memory b p \<noteq> underlying_memory m p\<rbrakk> \<Longrightarrow> in_user_frame p s
 2. \<And>rv s m b irq. \<lbrakk>invs s; ((), b) \<in> fst ((do y <- set_current_pd (addrFromPPtr pd);
setHardwareASID rv
od) (machine_state s)); interrupt_states s irq = IRQInactive; \<not> irq_masks b irq; irq_masks (machine_state s) irq\<rbrakk> \<Longrightarrow> irq_masks b irq proof (prove)
goal (4 subgoals):
 1. \<And>rv s m b p. \<lbrakk>invs s; underlying_memory b p \<noteq> underlying_memory m p\<rbrakk> \<Longrightarrow> \<lbrace>?P28 rv s m b p\<rbrace> do y <- set_current_pd (addrFromPPtr pd);
setHardwareASID rv
od \<lbrace>\<lambda>_ m'. underlying_memory m' p = underlying_memory m p\<rbrace>
 2. \<And>rv s m b p. \<lbrakk>invs s; underlying_memory b p \<noteq> underlying_memory m p\<rbrakk> \<Longrightarrow> ?P28 rv s m b p m
 3. \<And>rv s m b p. \<lbrakk>invs s; underlying_memory b p \<noteq> underlying_memory m p; underlying_memory b p = underlying_memory m p\<rbrakk> \<Longrightarrow> in_user_frame p s
 4. \<And>rv s m b irq. \<lbrakk>invs s; ((), b) \<in> fst ((do y <- set_current_pd (addrFromPPtr pd);
setHardwareASID rv
od) (machine_state s)); interrupt_states s irq = IRQInactive; \<not> irq_masks b irq; irq_masks (machine_state s) irq\<rbrakk> \<Longrightarrow> irq_masks b irq proof (prove)
goal (1 subgoal):
 1. \<And>rv s m b irq. \<lbrakk>invs s; ((), b) \<in> fst ((do y <- set_current_pd (addrFromPPtr pd);
setHardwareASID rv
od) (machine_state s)); interrupt_states s irq = IRQInactive; \<not> irq_masks b irq; irq_masks (machine_state s) irq\<rbrakk> \<Longrightarrow> irq_masks b irq proof (prove)
goal (2 subgoals):
 1. \<And>rv s m b irq. \<lbrakk>invs s; interrupt_states s irq = IRQInactive; \<not> irq_masks b irq; irq_masks (machine_state s) irq\<rbrakk> \<Longrightarrow> \<lbrace>?P60 rv s m b irq\<rbrace> do y <- set_current_pd (addrFromPPtr pd);
setHardwareASID rv
od \<lbrace>\<lambda>a b. irq_masks b irq\<rbrace>
 2. \<And>rv s m b irq. \<lbrakk>invs s; interrupt_states s irq = IRQInactive; \<not> irq_masks b irq; irq_masks (machine_state s) irq\<rbrakk> \<Longrightarrow> ?P60 rv s m b irq (machine_state s) proof (prove)
goal:
No subgoals!