kings-crown/FVELER_Isabelle huggingface dataset:
theory ArchTcbAcc_AI

lemma get_cap_valid_ipc [TcbAcc_AI_assms]:
  "\<lbrace>valid_objs and obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> tcb_ipc_buffer tcb = v) t\<rbrace>
     get_cap (t, tcb_cnode_index 4)
   \<lbrace>\<lambda>rv s. valid_ipc_buffer_cap rv v\<rbrace>" apply (wp get_cap_wp) apply clarsimp apply (drule(1) cte_wp_tcb_cap_valid) apply (clarsimp simp add: tcb_cap_valid_def obj_at_def) apply (simp add: valid_ipc_buffer_cap_def mask_cap_def cap_rights_update_def
                   acap_rights_update_def is_tcb
            split: cap.split_asm arch_cap.split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> tcb_ipc_buffer tcb = v) t\<rbrace> get_cap (t, tcb_cnode_index 4) \<lbrace>\<lambda>rv s. valid_ipc_buffer_cap rv v\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_objs and obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> tcb_ipc_buffer tcb = v) t) s \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) (t, tcb_cnode_index 4) s \<longrightarrow> valid_ipc_buffer_cap cap v proof (prove)
goal (1 subgoal):
 1. \<And>s cap. \<lbrakk>valid_objs s; obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> tcb_ipc_buffer tcb = v) t s; cte_wp_at ((=) cap) (t, tcb_cnode_index 4) s\<rbrakk> \<Longrightarrow> valid_ipc_buffer_cap cap v proof (prove)
goal (1 subgoal):
 1. \<And>s cap. \<lbrakk>valid_objs s; obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> tcb_ipc_buffer tcb = v) t s; tcb_cap_valid cap (t, tcb_cnode_index 4) s\<rbrakk> \<Longrightarrow> valid_ipc_buffer_cap cap v proof (prove)
goal (1 subgoal):
 1. \<And>s cap tcb. \<lbrakk>valid_objs s; is_tcb (TCB tcb) \<longrightarrow> st_tcb_at (\<lambda>st. is_nondevice_page_cap cap \<or> NullCap = cap) t s \<and> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb); kheap s t = Some (TCB tcb); v = tcb_ipc_buffer tcb\<rbrakk> \<Longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb) proof (prove)
goal:
No subgoals!
theory ArchTcbAcc_AI

lemma arch_tcb_context_set_eq_ARM[TcbAcc_AI_assms]: "arch_tcb_context_set (arch_tcb_context_get t) t = t" unfolding arch_tcb_context_get_def arch_tcb_context_set_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. arch_tcb_context_set (arch_tcb_context_get t) t = t proof (prove)
goal (1 subgoal):
 1. t\<lparr>tcb_context := tcb_context t\<rparr> = t
theory ArchTcbAcc_AI

lemma arch_tcb_context_get_eq_ARM[TcbAcc_AI_assms]: "arch_tcb_context_get (arch_tcb_context_set uc t) = uc" unfolding arch_tcb_context_get_def arch_tcb_context_set_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. arch_tcb_context_get (arch_tcb_context_set uc t) = uc proof (prove)
goal (1 subgoal):
 1. tcb_context (t\<lparr>tcb_context := uc\<rparr>) = uc
theory ArchTcbAcc_AI

lemma arch_tcb_update_aux2: "(\<lambda>tcb. tcb\<lparr> tcb_arch := f (tcb_arch tcb) \<rparr>)  = tcb_arch_update f" by (rule ext, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<lambda>tcb. tcb\<lparr>tcb_arch := f (tcb_arch tcb)\<rparr>) = tcb_arch_update f
theory ArchTcbAcc_AI

lemma arch_tcb_update_aux3: "tcb\<lparr>tcb_arch := f (tcb_arch tcb)\<rparr>  = tcb_arch_update f tcb" by(simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb\<lparr>tcb_arch := f (tcb_arch tcb)\<rparr> = tcb_arch_update f tcb
theory ArchTcbAcc_AI

lemma tcb_context_update_aux: "arch_tcb_context_set (P (arch_tcb_context_get atcb)) atcb
                               = tcb_context_update (\<lambda>ctx. P ctx) atcb" by (simp add: arch_tcb_context_set_def arch_tcb_context_get_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. arch_tcb_context_set (P (arch_tcb_context_get atcb)) atcb = tcb_context_update P atcb
theory VSpacePre_AI

lemma throw_on_false_wp[wp]:
  "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. (rv \<longrightarrow> Q () s) \<and> (\<not> rv \<longrightarrow> E x s)\<rbrace>
    \<Longrightarrow> \<lbrace>P\<rbrace> throw_on_false x f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" apply (simp add: throw_on_false_def unlessE_def) apply wp apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. (rv \<longrightarrow> Q () s) \<and> (\<not> rv \<longrightarrow> E x s)\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> throw_on_false x f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. (rv \<longrightarrow> Q () s) \<and> (\<not> rv \<longrightarrow> E x s)\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> doE v <- liftE f;
if v then returnOk () else throwError x
odE \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. (rv \<longrightarrow> Q () s) \<and> (\<not> rv \<longrightarrow> E x s)\<rbrace> \<Longrightarrow> \<lbrace>?Q\<rbrace> f \<lbrace>\<lambda>v s. (v \<longrightarrow> Q () s) \<and> (\<not> v \<longrightarrow> E x s \<and> True)\<rbrace>
 2. \<And>s. \<lbrakk>\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. (rv \<longrightarrow> Q () s) \<and> (\<not> rv \<longrightarrow> E x s)\<rbrace>; P s\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. (rv \<longrightarrow> Q () s) \<and> (\<not> rv \<longrightarrow> E x s)\<rbrace>; P s\<rbrakk> \<Longrightarrow> P s proof (prove)
goal:
No subgoals!
theory VSpacePre_AI

lemma dmo_asid_map [wp]:
  "\<lbrace>valid_asid_map\<rbrace> do_machine_op f \<lbrace>\<lambda>_. valid_asid_map\<rbrace>" apply (simp add: do_machine_op_def split_def) apply wp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_asid_map\<rbrace> do_machine_op f \<lbrace>\<lambda>_. valid_asid_map\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_asid_map\<rbrace> do ms <- gets machine_state;
p <- select_f (f ms);
y <- modify (machine_state_update (\<lambda>_. snd p));
return (fst p)
od \<lbrace>\<lambda>_. valid_asid_map\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_asid_map s \<Longrightarrow> \<forall>x\<in>fst (f (machine_state s)). valid_asid_map (s\<lparr>machine_state := snd x\<rparr>) proof (prove)
goal:
No subgoals!
theory VSpacePre_AI

lemma valid_irq_states_arch_state_update[simp]:
  "valid_irq_states (s\<lparr>arch_state := x\<rparr>) = valid_irq_states s" by(auto simp: valid_irq_states_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_irq_states (s\<lparr>arch_state := x\<rparr>) = valid_irq_states s
theory VSpacePre_AI

lemma pull_out_P:
  "P s \<and> (\<forall>c. caps_of_state s p = Some c \<longrightarrow> Q s c) \<longrightarrow> (\<forall>c. caps_of_state s p = Some c \<longrightarrow> P s \<and> Q s c)" by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P s \<and> (\<forall>c. caps_of_state s p = Some c \<longrightarrow> Q s c) \<longrightarrow> (\<forall>c. caps_of_state s p = Some c \<longrightarrow> P s \<and> Q s c)
theory VSpacePre_AI

lemma upto_enum_step_subtract:
  "x \<le> z \<Longrightarrow> [x, y .e. z] = (map ((+) x) [0, y - x .e. z - x])" by (auto simp add: upto_enum_step_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<le> z \<Longrightarrow> [x , y .e. z] = map ((+) x) [0 , y - x .e. z - x]
theory VSpacePre_AI

lemma invs_valid_irq_states[elim!]:
  "invs s \<Longrightarrow> valid_irq_states s" by(auto simp: invs_def valid_state_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs s \<Longrightarrow> valid_irq_states s
theory VSpacePre_AI

lemma uint_ucast:
  "(x :: 'a :: len word) < 2 ^ LENGTH('b) \<Longrightarrow> uint (ucast x :: 'b :: len word) = uint x" by (metis Word.of_nat_unat mod_less of_nat_numeral semiring_1_class.of_nat_power unat_less_helper
            unat_ucast)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x < 2 ^ LENGTH('b) \<Longrightarrow> uint (UCAST('a \<rightarrow> 'b) x) = uint x
theory VSpacePre_AI

lemma pd_casting_shifting:
  "size x + n < len_of TYPE('a) \<Longrightarrow>
     ucast (ucast x << n >> n :: ('a :: len) word) = x" apply (rule word_eqI) apply (simp add: nth_ucast nth_shiftr nth_shiftl word_size) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. size x + n < LENGTH('a) \<Longrightarrow> UCAST('a \<rightarrow> 'b) (UCAST('b \<rightarrow> 'a) x << n >> n) = x proof (prove)
goal (1 subgoal):
 1. \<And>na. size x + n < LENGTH('a) \<Longrightarrow> na < size (UCAST('a \<rightarrow> 'b) (UCAST('b \<rightarrow> 'a) x << n >> n)) \<longrightarrow> UCAST('a \<rightarrow> 'b) (UCAST('b \<rightarrow> 'a) x << n >> n) !! na = x !! na proof (prove)
goal:
No subgoals!
theory VSpacePre_AI

lemma set_upto_enum_step_4:
  "set [0, 4 .e. x :: word32]
       = (\<lambda>x. x << 2) ` {.. x >> 2}" by (auto simp: upto_enum_step_def shiftl_t2n shiftr_div_2n_w
                 word_size mult.commute)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set [0 , 4 .e. x] = (\<lambda>x. x << 2) ` {..x >> 2}
theory VSpacePre_AI

lemma set_upto_enum_step_8:
  "set [0, 8 .e. x :: word32]
       = (\<lambda>x. x << 3) ` {.. x >> 3}" by (auto simp: upto_enum_step_def shiftl_t2n shiftr_div_2n_w
                 word_size mult.commute)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set [0 , 8 .e. x] = (\<lambda>x. x << 3) ` {..x >> 3}
theory VSpacePre_AI

lemma set_cap_arch_obj:
  "\<lbrace>ko_at (ArchObj ao) p and cte_at p'\<rbrace> set_cap cap p' \<lbrace>\<lambda>_. ko_at (ArchObj ao) p\<rbrace>" apply (wp set_cap_obj_at_other) apply (clarsimp simp: obj_at_def cte_wp_at_cases) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ako_at ao p and cte_wp_at (\<lambda>_. True) p'\<rbrace> set_cap cap p' \<lbrace>\<lambda>_. ako_at ao p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (ako_at ao p and cte_wp_at (\<lambda>_. True) p') s \<Longrightarrow> ako_at ao p s \<and> p \<noteq> fst p' proof (prove)
goal:
No subgoals!
theory VSpacePre_AI

lemma set_mrs_tcb[wp]:
  "\<lbrace> tcb_at t \<rbrace> set_mrs receiver recv_buf mrs \<lbrace>\<lambda>rv. tcb_at t \<rbrace>" by (simp add: tcb_at_typ, wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_at t\<rbrace> set_mrs receiver recv_buf mrs \<lbrace>\<lambda>rv. tcb_at t\<rbrace>
theory VSpacePre_AI

lemma set_mrs_ntfn_at[wp]:
  "\<lbrace> ntfn_at p \<rbrace> set_mrs receiver recv_buf mrs \<lbrace>\<lambda>rv. ntfn_at p \<rbrace>" by (simp add: ntfn_at_typ, wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ntfn_at p\<rbrace> set_mrs receiver recv_buf mrs \<lbrace>\<lambda>rv. ntfn_at p\<rbrace>
theory ArchVSpace_AI

lemma kernel_base_shift_cast_le:
  fixes x :: "12 word"
  shows
  "(kernel_base >> 20 \<le> ucast x) =
        (ucast (kernel_base >> 20) \<le> x)" apply (simp add: word_le_def) apply (subst uint_ucast, simp, simp add: kernel_base_def) apply (simp only: ucast_def) apply (subst word_uint.Abs_inverse) apply (cut_tac x=x in word_uint.Rep) apply (simp add: uints_num) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (kernel_base >> 20 \<le> UCAST(12 \<rightarrow> 32) x) = (UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x) proof (prove)
goal (1 subgoal):
 1. (uint (kernel_base >> 20) \<le> uint (UCAST(12 \<rightarrow> 32) x)) = (uint (UCAST(32 \<rightarrow> 12) (kernel_base >> 20)) \<le> uint x) proof (prove)
goal (1 subgoal):
 1. (uint (kernel_base >> 20) \<le> uint (UCAST(12 \<rightarrow> 32) x)) = (uint (kernel_base >> 20) \<le> uint x) proof (prove)
goal (1 subgoal):
 1. (uint (kernel_base >> 20) \<le> uint (word_of_int (uint x))) = (uint (kernel_base >> 20) \<le> uint x) proof (prove)
goal (2 subgoals):
 1. uint x \<in> uints LENGTH(32)
 2. (uint (kernel_base >> 20) \<le> uint x) = (uint (kernel_base >> 20) \<le> uint x) proof (prove)
goal (2 subgoals):
 1. uint x \<in> uints LENGTH(12) \<Longrightarrow> uint x \<in> uints LENGTH(32)
 2. (uint (kernel_base >> 20) \<le> uint x) = (uint (kernel_base >> 20) \<le> uint x) proof (prove)
goal (1 subgoal):
 1. (uint (kernel_base >> 20) \<le> uint x) = (uint (kernel_base >> 20) \<le> uint x) proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma asid_word_bits [simp]: "asid_bits < word_bits" by (simp add: asid_bits_def word_bits_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. local.asid_bits < word_bits
theory ArchVSpace_AI

lemma asid_low_high_bits':
  "\<lbrakk> ucast x = (ucast y :: 10 word);
    asid_high_bits_of x = asid_high_bits_of y;
    x \<le> 2 ^ asid_bits - 1; y \<le> 2 ^ asid_bits - 1 \<rbrakk>
  \<Longrightarrow> x = y" by (rule asid_low_high_bits; (assumption|word_eqI_solve simp: asid_low_bits_def)?)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>UCAST(32 \<rightarrow> 10) x = UCAST(32 \<rightarrow> 10) y; asid_high_bits_of x = asid_high_bits_of y; x \<le> 2 ^ local.asid_bits - 1; y \<le> 2 ^ local.asid_bits - 1\<rbrakk> \<Longrightarrow> x = y
theory ArchVSpace_AI

lemma table_cap_ref_at_eq:
  "table_cap_ref c = Some [x] \<longleftrightarrow> vs_cap_ref c = Some [x]" by (auto simp: table_cap_ref_def vs_cap_ref_simps vs_cap_ref_def
          split: cap.splits arch_cap.splits vmpage_size.splits option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (table_cap_ref c = Some [x]) = (vs_cap_ref c = Some [x])
theory ArchVSpace_AI

lemma table_cap_ref_ap_eq:
  "table_cap_ref c = Some [x,y] \<longleftrightarrow> vs_cap_ref c = Some [x,y]" by (auto simp: table_cap_ref_def vs_cap_ref_simps vs_cap_ref_def
          split: cap.splits arch_cap.splits vmpage_size.splits option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (table_cap_ref c = Some [x, y]) = (vs_cap_ref c = Some [x, y])
theory ArchVSpace_AI

lemma pd_at_asid_unique2:
  "\<lbrakk> vspace_at_asid asid pd s; vspace_at_asid asid pd' s \<rbrakk>
         \<Longrightarrow> pd = pd'" apply (clarsimp simp: vspace_at_asid_def vs_asid_refs_def
                 dest!: graph_ofD vs_lookup_2ConsD vs_lookup_atD
                        vs_lookup1D) apply (clarsimp simp: obj_at_def vs_refs_def
                 split: Structures_A.kernel_object.splits
                        arch_kernel_obj.splits
                 dest!: graph_ofD) apply (drule ucast_up_inj, simp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vspace_at_asid asid pd s; vspace_at_asid asid pd' s\<rbrakk> \<Longrightarrow> pd = pd' proof (prove)
goal (1 subgoal):
 1. \<And>p ko koa. \<lbrakk>asid_table s (asid_high_bits_of asid) = Some p; ko_at ko p s; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), pd) \<in> vs_refs ko; ko_at koa p s; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), pd') \<in> vs_refs koa\<rbrakk> \<Longrightarrow> pd = pd' proof (prove)
goal (1 subgoal):
 1. \<And>p x1 a aa. \<lbrakk>asid_table s (asid_high_bits_of asid) = Some p; kheap s p = Some (ArchObj (ASIDPool x1)); x1 a = Some pd; x1 aa = Some pd'; UCAST(10 \<rightarrow> 32) aa = UCAST(10 \<rightarrow> 32) a; asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) a\<rbrakk> \<Longrightarrow> pd = pd' proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma valid_vs_lookupE:
  "\<lbrakk> valid_vs_lookup s; \<And>ref p. (ref \<unrhd> p) s' \<Longrightarrow> (ref \<unrhd> p) s;
           set (arm_global_pts (arch_state s)) \<subseteq> set (arm_global_pts (arch_state s'));
           caps_of_state s = caps_of_state s' \<rbrakk>
     \<Longrightarrow> valid_vs_lookup s'" by (simp add: valid_vs_lookup_def, blast)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_vs_lookup s; \<And>ref p. (ref \<unrhd> p) s' \<Longrightarrow> (ref \<unrhd> p) s; set (arm_global_pts (arch_state s)) \<subseteq> set (arm_global_pts (arch_state s')); caps_of_state s = caps_of_state s'\<rbrakk> \<Longrightarrow> valid_vs_lookup s'
theory ArchVSpace_AI

lemma load_hw_asid_wp:
  "\<lbrace>\<lambda>s. P (option_map fst (arm_asid_map (arch_state s) asid)) s\<rbrace>
         load_hw_asid asid \<lbrace>P\<rbrace>" apply (simp add: load_hw_asid_def) apply wp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (map_option fst (arm_asid_map (arch_state s) asid)) s\<rbrace> load_hw_asid asid \<lbrace>P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (map_option fst (arm_asid_map (arch_state s) asid)) s\<rbrace> do asid_map <- gets (arm_asid_map \<circ> arch_state);
return (map_option fst (asid_map asid))
od \<lbrace>P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (map_option fst (arm_asid_map (arch_state s) asid)) s \<Longrightarrow> P (map_option fst ((arm_asid_map \<circ> arch_state) s asid)) s proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma invalidate_hw_asid_entry_asid_map [wp]:
  "\<lbrace>valid_asid_map\<rbrace> invalidate_hw_asid_entry asid \<lbrace>\<lambda>_. valid_asid_map\<rbrace>" apply (simp add: invalidate_hw_asid_entry_def) apply wp apply (simp add: valid_asid_map_def vspace_at_asid_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_asid_map\<rbrace> invalidate_hw_asid_entry asid \<lbrace>\<lambda>_. valid_asid_map\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_asid_map\<rbrace> do hw_asid_map <- gets (arm_hwasid_table \<circ> arch_state);
modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_hwasid_table := hw_asid_map(asid := None)\<rparr>\<rparr>)
od \<lbrace>\<lambda>_. valid_asid_map\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_asid_map s \<Longrightarrow> valid_asid_map (s\<lparr>arch_state := arch_state s\<lparr>arm_hwasid_table := ((arm_hwasid_table \<circ> arch_state) s)(asid := None)\<rparr>\<rparr>) proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma invalidate_asid_asid_map [wp]:
  "\<lbrace>valid_asid_map\<rbrace> invalidate_asid asid \<lbrace>\<lambda>_. valid_asid_map\<rbrace>" apply (simp add: invalidate_asid_def) apply wp apply (auto simp add: valid_asid_map_def vspace_at_asid_def graph_of_def split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_asid_map\<rbrace> invalidate_asid asid \<lbrace>\<lambda>_. valid_asid_map\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_asid_map\<rbrace> do asid_map <- gets (arm_asid_map \<circ> arch_state);
modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := asid_map(asid := None)\<rparr>\<rparr>)
od \<lbrace>\<lambda>_. valid_asid_map\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_asid_map s \<Longrightarrow> valid_asid_map (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := ((arm_asid_map \<circ> arch_state) s)(asid := None)\<rparr>\<rparr>) proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma find_free_hw_asid_asid_map [wp]:
  "\<lbrace>valid_asid_map\<rbrace> find_free_hw_asid \<lbrace>\<lambda>_. valid_asid_map\<rbrace>" apply (simp add: find_free_hw_asid_def) apply (rule hoare_pre) apply (wp|wpc|simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_asid_map\<rbrace> find_free_hw_asid \<lbrace>\<lambda>_. valid_asid_map\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_asid_map\<rbrace> do hw_asid_table <- gets (arm_hwasid_table \<circ> arch_state);
next_asid <- gets (arm_next_asid \<circ> arch_state);
case find (\<lambda>a. hw_asid_table a = None) (take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid]) of None \<Rightarrow> do invalidate_asid $ the $ hw_asid_table next_asid;
do_machine_op $ invalidateLocalTLB_ASID next_asid;
invalidate_hw_asid_entry next_asid;
new_next_asid <- return (next_asid + 1);
modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_next_asid := new_next_asid\<rparr>\<rparr>);
return next_asid
od | Some x \<Rightarrow> return x
od \<lbrace>\<lambda>_. valid_asid_map\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do hw_asid_table <- gets (arm_hwasid_table \<circ> arch_state);
next_asid <- gets (arm_next_asid \<circ> arch_state);
case find (\<lambda>a. hw_asid_table a = None) (take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid]) of None \<Rightarrow> do invalidate_asid $ the $ hw_asid_table next_asid;
do_machine_op $ invalidateLocalTLB_ASID next_asid;
invalidate_hw_asid_entry next_asid;
new_next_asid <- return (next_asid + 1);
modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_next_asid := new_next_asid\<rparr>\<rparr>);
return next_asid
od | Some x \<Rightarrow> return x
od \<lbrace>\<lambda>_. valid_asid_map\<rbrace>
 2. \<And>s. valid_asid_map s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma dmo_pd_at_asid [wp]:
  "\<lbrace>vspace_at_asid a pd\<rbrace> do_machine_op f \<lbrace>\<lambda>_. vspace_at_asid a pd\<rbrace>" apply (simp add: do_machine_op_def split_def) apply wp apply (simp add: vspace_at_asid_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>vspace_at_asid a pd\<rbrace> do_machine_op f \<lbrace>\<lambda>_. vspace_at_asid a pd\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>vspace_at_asid a pd\<rbrace> do ms <- gets machine_state;
p <- select_f (f ms);
y <- modify (machine_state_update (\<lambda>_. snd p));
return (fst p)
od \<lbrace>\<lambda>_. vspace_at_asid a pd\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. vspace_at_asid a pd s \<Longrightarrow> \<forall>x\<in>fst (f (machine_state s)). vspace_at_asid a pd (s\<lparr>machine_state := snd x\<rparr>) proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma valid_asid_mapD:
  "\<lbrakk> arm_asid_map (arch_state s) asid = Some (vasid, pd); valid_asid_map s \<rbrakk>
      \<Longrightarrow> vspace_at_asid asid pd s \<and> asid \<le> mask asid_bits" by (auto simp add: valid_asid_map_def graph_of_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>arm_asid_map (arch_state s) asid = Some (vasid, pd); valid_asid_map s\<rbrakk> \<Longrightarrow> vspace_at_asid asid pd s \<and> asid \<le> mask local.asid_bits
theory ArchVSpace_AI

lemma invalidateLocalTLB_ASID_underlying_memory:
  "\<lbrace>\<lambda>m'. underlying_memory m' p = um\<rbrace>
   invalidateLocalTLB_ASID asid
   \<lbrace>\<lambda>_ m'. underlying_memory m' p = um\<rbrace>" by (clarsimp simp: invalidateLocalTLB_ASID_def machine_op_lift_def
                     machine_rest_lift_def split_def | wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>m'. underlying_memory m' p = um\<rbrace> invalidateLocalTLB_ASID asid \<lbrace>\<lambda>_ m'. underlying_memory m' p = um\<rbrace>
theory ArchVSpace_AI

lemma isb_underlying_memory[wp]:
  "\<lbrace>\<lambda>m'. underlying_memory m' p = um\<rbrace>
   isb
   \<lbrace>\<lambda>_ m'. underlying_memory m' p = um\<rbrace>" by (clarsimp simp: isb_def machine_op_lift_def
                     machine_rest_lift_def split_def | wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>m'. underlying_memory m' p = um\<rbrace> isb \<lbrace>\<lambda>_ m'. underlying_memory m' p = um\<rbrace>
theory ArchVSpace_AI

lemma dsb_underlying_memory[wp]:
  "\<lbrace>\<lambda>m'. underlying_memory m' p = um\<rbrace>
   dsb
   \<lbrace>\<lambda>_ m'. underlying_memory m' p = um\<rbrace>" by (clarsimp simp: dsb_def machine_op_lift_def
                     machine_rest_lift_def split_def | wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>m'. underlying_memory m' p = um\<rbrace> dsb \<lbrace>\<lambda>_ m'. underlying_memory m' p = um\<rbrace>