kings-crown/FVELER_Isabelle huggingface dataset:
theory ArchFinalise_AI

lemma nat_to_cref_unat_of_bl':
  "\<lbrakk> length xs < 32; n = length xs \<rbrakk> \<Longrightarrow>
   nat_to_cref n (unat (of_bl xs :: machine_word)) = xs" apply (simp add: nat_to_cref_def word_bits_def) apply (rule nth_equalityI) apply simp apply clarsimp apply (subst to_bl_nth) apply (simp add: word_size) apply (simp add: word_size) apply (simp add: test_bit_of_bl rev_nth) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length xs < 32; n = length xs\<rbrakk> \<Longrightarrow> nat_to_cref n (unat (of_bl xs)) = xs proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length xs < 32; n = length xs\<rbrakk> \<Longrightarrow> drop (32 - length xs) (to_bl (of_bl xs)) = xs proof (prove)
goal (2 subgoals):
 1. \<lbrakk>length xs < 32; n = length xs\<rbrakk> \<Longrightarrow> length (drop (32 - length xs) (to_bl (of_bl xs))) = length xs
 2. \<And>i. \<lbrakk>length xs < 32; n = length xs; i < length (drop (32 - length xs) (to_bl (of_bl xs)))\<rbrakk> \<Longrightarrow> drop (32 - length xs) (to_bl (of_bl xs)) ! i = xs ! i proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>length xs < 32; n = length xs; i < length (drop (32 - length xs) (to_bl (of_bl xs)))\<rbrakk> \<Longrightarrow> drop (32 - length xs) (to_bl (of_bl xs)) ! i = xs ! i proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>length xs < 32; n = length xs; i < length xs\<rbrakk> \<Longrightarrow> to_bl (of_bl xs) ! (32 + i - length xs) = xs ! i proof (prove)
goal (2 subgoals):
 1. \<And>i. \<lbrakk>length xs < 32; n = length xs; i < length xs\<rbrakk> \<Longrightarrow> 32 + i - length xs < size (of_bl xs)
 2. \<And>i. \<lbrakk>length xs < 32; n = length xs; i < length xs\<rbrakk> \<Longrightarrow> of_bl xs !! (size (of_bl xs) - Suc (32 + i - length xs)) = xs ! i proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>length xs < 32; n = length xs; i < length xs\<rbrakk> \<Longrightarrow> of_bl xs !! (size (of_bl xs) - Suc (32 + i - length xs)) = xs ! i proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>length xs < 32; n = length xs; i < length xs\<rbrakk> \<Longrightarrow> (rev xs ! (length xs - Suc i) \<and> length xs - Suc i < 32 \<and> length xs - Suc i < length xs) = xs ! i proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>length xs < 32; n = length xs; i < length xs\<rbrakk> \<Longrightarrow> (xs ! i \<and> length xs - Suc i < 32 \<and> length xs - Suc i < length xs) = xs ! i proof (prove)
goal:
No subgoals!
theory ArchFinalise_AI

lemma set_pt_tcb_at:
  "\<lbrace>\<lambda>s. P (ko_at (TCB tcb) t s)\<rbrace> set_pt a b \<lbrace>\<lambda>_ s. P (ko_at (TCB tcb) t s)\<rbrace>" by (clarsimp simp: simpler_set_pt_def valid_def obj_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ko_at (TCB tcb) t s)\<rbrace> set_pt a b \<lbrace>\<lambda>_ s. P (ko_at (TCB tcb) t s)\<rbrace>
theory ArchFinalise_AI

lemma set_pd_tcb_at:
  "\<lbrace>\<lambda>s. P (ko_at (TCB tcb) t s)\<rbrace> set_pd a b \<lbrace>\<lambda>_ s. P (ko_at (TCB tcb) t s)\<rbrace>" by (clarsimp simp: simpler_set_pd_def valid_def obj_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ko_at (TCB tcb) t s)\<rbrace> set_pd a b \<lbrace>\<lambda>_ s. P (ko_at (TCB tcb) t s)\<rbrace>
theory ArchFinalise_AI

lemma unmap_page_tcb_cap_valid:
  "\<lbrace>\<lambda>s. tcb_cap_valid cap r s\<rbrace>
    unmap_page sz asid vaddr pptr
   \<lbrace>\<lambda>rv s. tcb_cap_valid cap r s\<rbrace>" apply (rule tcb_cap_valid_typ_st) apply wp apply (simp add: pred_tcb_at_def2) apply (wp unmap_page_tcb_at hoare_vcg_ex_lift hoare_vcg_all_lift)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_cap_valid cap r\<rbrace> unmap_page sz asid vaddr pptr \<lbrace>\<lambda>rv. tcb_cap_valid cap r\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>P t. \<lbrace>\<lambda>s. P (typ_at ATCB t s)\<rbrace> unmap_page sz asid vaddr pptr \<lbrace>\<lambda>rv s. P (typ_at ATCB t s)\<rbrace>
 2. \<And>P t. \<lbrace>st_tcb_at P t\<rbrace> unmap_page sz asid vaddr pptr \<lbrace>\<lambda>rv. st_tcb_at P t\<rbrace>
 3. \<And>P t. \<lbrace>\<lambda>s. \<forall>tcb. ko_at (TCB tcb) t s \<longrightarrow> P (tcb_ipc_buffer tcb)\<rbrace> unmap_page sz asid vaddr pptr \<lbrace>\<lambda>rv s. \<forall>tcb. ko_at (TCB tcb) t s \<longrightarrow> P (tcb_ipc_buffer tcb)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>P t. \<lbrace>st_tcb_at P t\<rbrace> unmap_page sz asid vaddr pptr \<lbrace>\<lambda>rv. st_tcb_at P t\<rbrace>
 2. \<And>P t. \<lbrace>\<lambda>s. \<forall>tcb. ko_at (TCB tcb) t s \<longrightarrow> P (tcb_ipc_buffer tcb)\<rbrace> unmap_page sz asid vaddr pptr \<lbrace>\<lambda>rv s. \<forall>tcb. ko_at (TCB tcb) t s \<longrightarrow> P (tcb_ipc_buffer tcb)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>P t. \<lbrace>\<lambda>s. \<exists>tcb. ko_at (TCB tcb) t s \<and> P (tcb_state tcb)\<rbrace> unmap_page sz asid vaddr pptr \<lbrace>\<lambda>rv s. \<exists>tcb. ko_at (TCB tcb) t s \<and> P (tcb_state tcb)\<rbrace>
 2. \<And>P t. \<lbrace>\<lambda>s. \<forall>tcb. ko_at (TCB tcb) t s \<longrightarrow> P (tcb_ipc_buffer tcb)\<rbrace> unmap_page sz asid vaddr pptr \<lbrace>\<lambda>rv s. \<forall>tcb. ko_at (TCB tcb) t s \<longrightarrow> P (tcb_ipc_buffer tcb)\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchFinalise_AI

lemma (* replaceable_cdt_update *)[simp,Finalise_AI_asms]:
  "replaceable (cdt_update f s) = replaceable s" by (fastforce simp: replaceable_def tcb_cap_valid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. replaceable (cdt_update f s) = replaceable s
theory ArchFinalise_AI

lemma (* replaceable_more_update *) [simp,Finalise_AI_asms]:
  "replaceable (trans_state f s) sl cap cap' = replaceable s sl cap cap'" by (simp add: replaceable_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. replaceable (trans_state f s) sl cap cap' = replaceable s sl cap cap'
theory ArchFinalise_AI

lemma (* obj_ref_ofI *) [Finalise_AI_asms]: "obj_refs cap = {x} \<Longrightarrow> obj_ref_of cap = x" by (case_tac cap, simp_all) (rename_tac arch_cap, case_tac arch_cap, simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. obj_refs cap = {x} \<Longrightarrow> obj_ref_of cap = x
theory ArchFinalise_AI

lemma dom_tcb_cap_cases_lt_ARCH [Finalise_AI_asms]:
  "dom tcb_cap_cases = {xs. length xs = 3 \<and> unat (of_bl xs :: machine_word) < 5}" apply (rule set_eqI, rule iffI) apply clarsimp apply (simp add: tcb_cap_cases_def tcb_cnode_index_def to_bl_1 split: if_split_asm) apply clarsimp apply (frule tcb_cap_cases_lt) apply (clarsimp simp: nat_to_cref_unat_of_bl') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dom tcb_cap_cases = {xs. length xs = 3 \<and> unat (of_bl xs) < 5} proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> dom tcb_cap_cases \<Longrightarrow> x \<in> {xs. length xs = 3 \<and> unat (of_bl xs) < 5}
 2. \<And>x. x \<in> {xs. length xs = 3 \<and> unat (of_bl xs) < 5} \<Longrightarrow> x \<in> dom tcb_cap_cases proof (prove)
goal (2 subgoals):
 1. \<And>x a aa b. tcb_cap_cases x = Some (a, aa, b) \<Longrightarrow> length x = 3 \<and> unat (of_bl x) < 5
 2. \<And>x. x \<in> {xs. length xs = 3 \<and> unat (of_bl xs) < 5} \<Longrightarrow> x \<in> dom tcb_cap_cases proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> {xs. length xs = 3 \<and> unat (of_bl xs) < 5} \<Longrightarrow> x \<in> dom tcb_cap_cases proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>length x = 3; unat (of_bl x) < 5\<rbrakk> \<Longrightarrow> \<exists>a aa b. tcb_cap_cases x = Some (a, aa, b) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>length x = 3; unat (of_bl x) < 5; tcb_cap_cases (nat_to_cref 3 (unat (of_bl x))) \<noteq> None\<rbrakk> \<Longrightarrow> \<exists>a aa b. tcb_cap_cases x = Some (a, aa, b) proof (prove)
goal:
No subgoals!
theory ArchFinalise_AI

lemma (* unbind_notification_final *) [wp,Finalise_AI_asms]:
  "\<lbrace>is_final_cap' cap\<rbrace> unbind_notification t \<lbrace> \<lambda>rv. is_final_cap' cap\<rbrace>" unfolding unbind_notification_def apply (wp final_cap_lift thread_set_caps_of_state_trivial hoare_drop_imps
       | wpc | simp add: tcb_cap_cases_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>is_final_cap' cap\<rbrace> unbind_notification t \<lbrace>\<lambda>rv. is_final_cap' cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>is_final_cap' cap\<rbrace> do ntfnptr <- get_bound_notification t;
case ntfnptr of None \<Rightarrow> return () | Some ntfnptr' \<Rightarrow> do ntfn <- get_notification ntfnptr';
do_unbind_notification ntfnptr' ntfn t
od
od \<lbrace>\<lambda>rv. is_final_cap' cap\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchFinalise_AI

lemma obj_at_not_live_valid_arch_cap_strg [Finalise_AI_asms]:
  "(s \<turnstile> ArchObjectCap cap \<and> aobj_ref cap = Some r)
        \<longrightarrow> obj_at (\<lambda>ko. \<not> live ko) r s" by (clarsimp simp: valid_cap_def obj_at_def
                     a_type_arch_live live_def hyp_live_def
              split: arch_cap.split_asm if_splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s \<turnstile> ArchObjectCap cap \<and> aobj_ref cap = Some r \<longrightarrow> obj_at (\<lambda>ko. \<not> live ko) r s
theory ArchFinalise_AI

lemma (* suspend_no_cap_to_obj_ref *)[wp,Finalise_AI_asms]:
  "\<lbrace>no_cap_to_obj_with_diff_ref cap S\<rbrace>
     suspend t
   \<lbrace>\<lambda>rv. no_cap_to_obj_with_diff_ref cap S\<rbrace>" apply (simp add: no_cap_to_obj_with_diff_ref_def
                   cte_wp_at_caps_of_state) apply (wp suspend_caps_of_state) apply (clarsimp simp: table_cap_ref_simps
                 dest!: obj_ref_none_no_asid[rule_format]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>no_cap_to_obj_with_diff_ref cap S\<rbrace> suspend t \<lbrace>\<lambda>rv. no_cap_to_obj_with_diff_ref cap S\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>p\<in>UNIV - S. \<forall>capa. obj_refs capa = obj_refs cap \<longrightarrow> caps_of_state s p = Some capa \<longrightarrow> table_cap_ref capa = table_cap_ref cap\<rbrace> suspend t \<lbrace>\<lambda>rv s. \<forall>p\<in>UNIV - S. \<forall>capa. obj_refs capa = obj_refs cap \<longrightarrow> caps_of_state s p = Some capa \<longrightarrow> table_cap_ref capa = table_cap_ref cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<forall>p\<in>UNIV - S. \<forall>capa. obj_refs capa = obj_refs cap \<longrightarrow> caps_of_state s p = Some capa \<longrightarrow> table_cap_ref capa = table_cap_ref cap \<Longrightarrow> (\<forall>p. cte_wp_at can_fast_finalise p s \<longrightarrow> (\<forall>pa\<in>UNIV - S. \<forall>capa. obj_refs capa = obj_refs cap \<longrightarrow> ((caps_of_state s)(p \<mapsto> NullCap)) pa = Some capa \<longrightarrow> table_cap_ref capa = table_cap_ref cap)) \<and> (\<forall>p\<in>UNIV - S. \<forall>capa. obj_refs capa = obj_refs cap \<longrightarrow> caps_of_state s p = Some capa \<longrightarrow> table_cap_ref capa = table_cap_ref cap) proof (prove)
goal:
No subgoals!
theory ArchFinalise_AI

lemma (* deleting_irq_handler_cte_preserved *)[Finalise_AI_asms]:
  assumes x: "\<And>cap. P cap \<Longrightarrow> \<not> can_fast_finalise cap"
  shows "\<lbrace>cte_wp_at P p\<rbrace> deleting_irq_handler irq \<lbrace>\<lambda>rv. cte_wp_at P p\<rbrace>" apply (simp add: deleting_irq_handler_def) apply (wp cap_delete_one_cte_wp_at_preserved | simp add: x)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at P p\<rbrace> deleting_irq_handler irq \<lbrace>\<lambda>rv. cte_wp_at P p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at P p\<rbrace> get_irq_slot irq >>= cap_delete_one \<lbrace>\<lambda>rv. cte_wp_at P p\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchFinalise_AI

lemma (* cap_delete_one_invs *) [Finalise_AI_asms,wp]:
  "\<lbrace>invs and emptyable ptr\<rbrace> cap_delete_one ptr \<lbrace>\<lambda>rv. invs\<rbrace>" apply (simp add: cap_delete_one_def unless_def is_final_cap_def) apply (rule hoare_pre) apply (wp empty_slot_invs get_cap_wp) apply clarsimp apply (drule cte_wp_at_valid_objs_valid_cap, fastforce+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and emptyable ptr\<rbrace> cap_delete_one ptr \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and emptyable ptr\<rbrace> do cap <- get_cap ptr;
when (cap \<noteq> NullCap) (do final <- gets (is_final_cap' cap);
y <- fast_finalise cap final;
empty_slot ptr NullCap
od)
od \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do cap <- get_cap ptr;
when (cap \<noteq> NullCap) (do final <- gets (is_final_cap' cap);
y <- fast_finalise cap final;
empty_slot ptr NullCap
od)
od \<lbrace>\<lambda>rv. invs\<rbrace>
 2. \<And>s. (invs and emptyable ptr) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs and emptyable ptr) s \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) ptr s \<longrightarrow> (if cap \<noteq> NullCap then \<lambda>s. invs s \<and> (s \<turnstile> cap \<and> is_final_cap' cap s = is_final_cap' cap s \<and> cte_wp_at ((=) cap) ptr s \<and> valid_asid_table (asid_table s) s \<and> valid_mdb s \<and> valid_objs s \<and> sym_refs (state_refs_of s)) \<and> (invs and emptyable ptr) s \<and> (NullCap \<noteq> NullCap \<longrightarrow> post_cap_delete_pre NullCap ((caps_of_state s)(ptr \<mapsto> NullCap))) else invs) s proof (prove)
goal (1 subgoal):
 1. \<And>s cap. \<lbrakk>invs s; emptyable ptr s; cap \<noteq> NullCap; cte_wp_at ((=) cap) ptr s\<rbrakk> \<Longrightarrow> s \<turnstile> cap \<and> valid_asid_table (asid_table s) s \<and> valid_mdb s \<and> valid_objs s \<and> sym_refs (state_refs_of s) proof (prove)
goal:
No subgoals!
theory ArchFinalise_AI

lemma tcb_cap_valid_pagetable:
  "tcb_cap_valid (ArchObjectCap (PageTableCap word (Some v))) slot
    = tcb_cap_valid (ArchObjectCap (PageTableCap word None)) slot" apply (rule ext) apply (simp add: tcb_cap_valid_def tcb_cap_cases_def is_nondevice_page_cap_arch_def
                   is_cap_simps valid_ipc_buffer_cap_def is_nondevice_page_cap_simps
                   is_valid_vtable_root_def
            split: Structures_A.thread_state.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_cap_valid (ArchObjectCap (PageTableCap word (Some v))) slot = tcb_cap_valid (ArchObjectCap (PageTableCap word None)) slot proof (prove)
goal (1 subgoal):
 1. \<And>x. tcb_cap_valid (ArchObjectCap (PageTableCap word (Some v))) slot x = tcb_cap_valid (ArchObjectCap (PageTableCap word None)) slot x proof (prove)
goal:
No subgoals!
theory ArchFinalise_AI

lemma store_pde_unmap_empty:
  "\<lbrace>\<lambda>s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s\<rbrace>
    store_pde pd_slot InvalidPDE
   \<lbrace>\<lambda>rv s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s\<rbrace>" apply (clarsimp simp: store_pde_def set_pd_def set_object_def) apply (wp get_object_wp) apply (clarsimp simp: obj_at_def empty_table_def pde_ref_def valid_pde_mappings_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s\<rbrace> store_pde pd_slot InvalidPDE \<lbrace>\<lambda>rv s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s\<rbrace> do pd <- get_pd (pd_slot && ~~ mask pd_bits);
kobj <- get_object (pd_slot && ~~ mask pd_bits);
y <- assert (a_type kobj = a_type (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (pd_slot && mask pd_bits >> 2) := InvalidPDE)))));
s <- get;
put (s\<lparr>kheap := (kheap s)(pd_slot && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (pd_slot && mask pd_bits >> 2) := InvalidPDE))))\<rparr>)
od \<lbrace>\<lambda>rv s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<Longrightarrow> \<forall>pd. ako_at (PageDirectory pd) (pd_slot && ~~ mask pd_bits) s \<longrightarrow> (\<forall>ko. ko_at ko (pd_slot && ~~ mask pd_bits) s \<longrightarrow> a_type ko = a_type (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (pd_slot && mask pd_bits >> 2) := InvalidPDE)))) \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state (s\<lparr>kheap := (kheap s)(pd_slot && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (pd_slot && mask pd_bits >> 2) := InvalidPDE))))\<rparr>))))) word (s\<lparr>kheap := (kheap s)(pd_slot && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (pd_slot && mask pd_bits >> 2) := InvalidPDE))))\<rparr>)) proof (prove)
goal:
No subgoals!
theory ArchFinalise_AI

lemma store_pte_unmap_empty:
  "\<lbrace>\<lambda>s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s\<rbrace>
    store_pte xa InvalidPTE
   \<lbrace>\<lambda>rv s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s\<rbrace>" apply (wp get_object_wp | simp add: store_pte_def set_pt_def set_object_def)+ apply (clarsimp simp: obj_at_def empty_table_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s\<rbrace> store_pte xa InvalidPTE \<lbrace>\<lambda>rv s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<Longrightarrow> \<forall>pt. ako_at (PageTable pt) (xa && ~~ mask pt_bits) s \<longrightarrow> (\<forall>ko. ko_at ko (xa && ~~ mask pt_bits) s \<longrightarrow> a_type ko = a_type (ArchObj (PageTable (pt(UCAST(32 \<rightarrow> 8) (xa && mask pt_bits >> 2) := InvalidPTE)))) \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word (s\<lparr>kheap := \<lambda>a. if a = xa && ~~ mask pt_bits then Some (ArchObj (PageTable (\<lambda>a. if a = UCAST(32 \<rightarrow> 8) (xa && mask pt_bits >> 2) then InvalidPTE else pt a))) else kheap s a\<rparr>)) proof (prove)
goal:
No subgoals!
theory ArchFinalise_AI

lemma invalidate_tlb_by_asid_pspace_aligned:
  "\<lbrace>pspace_aligned\<rbrace> invalidate_tlb_by_asid aa \<lbrace>\<lambda>_. pspace_aligned\<rbrace>" apply (simp add: invalidate_tlb_by_asid_def load_hw_asid_def | wp | wpc)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned\<rbrace> invalidate_tlb_by_asid aa \<lbrace>\<lambda>_. pspace_aligned\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchFinalise_AI

lemma unmap_page_table_empty:
  "\<lbrace>\<lambda>s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s\<rbrace>
    unmap_page_table aa b word
   \<lbrace>\<lambda>rv s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s\<rbrace>" apply (simp add: unmap_page_table_def) apply (wp store_pde_unmap_empty flush_table_empty page_table_mapped_empty | simp | wpc)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s\<rbrace> unmap_page_table aa b word \<lbrace>\<lambda>rv s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s\<rbrace> do pdOpt <- page_table_mapped aa b word;
case pdOpt of None \<Rightarrow> return () | Some pd \<Rightarrow> do pd_slot <- return $ lookup_pd_slot pd b;
store_pde pd_slot InvalidPDE;
do_machine_op $ cleanByVA_PoU pd_slot (addrFromPPtr pd_slot);
flush_table pd aa b word
od
od \<lbrace>\<lambda>rv s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchFinalise_AI

lemma mapM_x_store_pte_valid_vspace_objs:
  "\<lbrace>invs and (\<lambda>s. \<exists>p' cap. caps_of_state s p' = Some cap \<and> is_pt_cap cap \<and>
    (\<forall>x \<in> set pteptrs. x && ~~ mask pt_bits \<in> obj_refs cap)) \<rbrace>
    mapM_x (\<lambda>p. store_pte p InvalidPTE) pteptrs
   \<lbrace>\<lambda>rv. valid_vspace_objs\<rbrace>" apply (rule hoare_strengthen_post, rule mapM_x_wp') apply wp+ apply (fastforce simp: is_pt_cap_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and (\<lambda>s. \<exists>p' cap. caps_of_state s p' = Some cap \<and> is_pt_cap cap \<and> (\<forall>x\<in>set pteptrs. x && ~~ mask pt_bits \<in> obj_refs cap))\<rbrace> mapM_x (\<lambda>p. store_pte p InvalidPTE) pteptrs \<lbrace>\<lambda>rv. valid_vspace_objs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> set pteptrs \<Longrightarrow> \<lbrace>invs and (\<lambda>s. \<exists>p' cap. caps_of_state s p' = Some cap \<and> is_pt_cap cap \<and> (\<forall>x\<in>set pteptrs. x && ~~ mask pt_bits \<in> obj_refs cap))\<rbrace> store_pte x InvalidPTE \<lbrace>\<lambda>rv. invs and (\<lambda>s. \<exists>p' cap. caps_of_state s p' = Some cap \<and> is_pt_cap cap \<and> (\<forall>x\<in>set pteptrs. x && ~~ mask pt_bits \<in> obj_refs cap))\<rbrace>
 2. \<And>rv s. (invs and (\<lambda>s. \<exists>p' cap. caps_of_state s p' = Some cap \<and> is_pt_cap cap \<and> (\<forall>x\<in>set pteptrs. x && ~~ mask pt_bits \<in> obj_refs cap))) s \<Longrightarrow> valid_vspace_objs s proof (prove)
goal (2 subgoals):
 1. \<And>x s. \<lbrakk>x \<in> set pteptrs; (invs and (\<lambda>s. \<exists>p' cap. caps_of_state s p' = Some cap \<and> is_pt_cap cap \<and> (\<forall>x\<in>set pteptrs. x && ~~ mask pt_bits \<in> obj_refs cap))) s\<rbrakk> \<Longrightarrow> (invs and (\<lambda>s. (\<exists>ref. (ref \<rhd> (x && ~~ mask pt_bits)) s) \<longrightarrow> valid_pte InvalidPTE s) and (\<lambda>s. wellformed_pte InvalidPTE) and (\<lambda>s. \<exists>slot asid. caps_of_state s slot = Some (ArchObjectCap (PageTableCap (x && ~~ mask pt_bits) asid)) \<and> (InvalidPTE = InvalidPTE \<or> asid \<noteq> None)) and (\<lambda>s. \<forall>ref. (ref \<rhd> (x && ~~ mask pt_bits)) s \<longrightarrow> (\<forall>q. pte_ref_pages InvalidPTE = Some q \<longrightarrow> (\<exists>p' cap. caps_of_state s p' = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (x && mask pt_bits >> 2) (Some APageTable) # ref))))) s \<and> (\<exists>p' cap. caps_of_state s p' = Some cap \<and> is_pt_cap cap \<and> (\<forall>x\<in>set pteptrs. x && ~~ mask pt_bits \<in> obj_refs cap))
 2. \<And>rv s. (invs and (\<lambda>s. \<exists>p' cap. caps_of_state s p' = Some cap \<and> is_pt_cap cap \<and> (\<forall>x\<in>set pteptrs. x && ~~ mask pt_bits \<in> obj_refs cap))) s \<Longrightarrow> valid_vspace_objs s proof (prove)
goal:
No subgoals!