theory ArchFinalise_AI

lemma delete_asid_unmapped[wp]:
  "\<lbrace>\<top>\<rbrace>
      delete_asid asid pd
   \<lbrace>\<lambda>rv s.  \<not> ([VSRef (asid && mask asid_low_bits) (Some AASIDPool),
                VSRef (ucast (asid_high_bits_of asid)) None]  \<rhd> pd) s\<rbrace>" apply (simp add: delete_asid_def
                   mask_asid_low_bits_ucast_ucast
             cong: option.case_cong) apply (wp set_asid_pool_unmap load_hw_asid_wp | wpc)+ apply simp apply (intro allI conjI impI) apply (fastforce simp: vs_lookup_def vs_asid_refs_def up_ucast_inj_eq
                   dest!: graph_ofD vs_lookup1_rtrancl_iterations
                          vs_lookup1D) apply (erule vs_lookup_atI) apply (clarsimp simp: vs_lookup_def vs_asid_refs_def up_ucast_inj_eq
                 dest!: graph_ofD vs_lookup1_rtrancl_iterations
                        vs_lookup1D) apply (clarsimp simp: obj_at_def vs_refs_def up_ucast_inj_eq
                 dest!: graph_ofD) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> delete_asid asid pd \<lbrace>\<lambda>rv s. ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], pd) \<notin> vs_lookup s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> do asid_table <- gets (arm_asid_table \<circ> arch_state);
case asid_table (asid_high_bits_of asid) of None \<Rightarrow> return () | Some pool_ptr \<Rightarrow> do pool <- get_asid_pool pool_ptr;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd) (do y <- flush_space asid;
y <- invalidate_asid_entry asid;
y <- set_asid_pool pool_ptr (pool(UCAST(32 \<rightarrow> 10) asid := None));
gets cur_thread >>= set_vm_root
od)
od
od \<lbrace>\<lambda>rv s. ([VSRef (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) asid)) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], pd) \<notin> vs_lookup s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> ((arm_asid_table \<circ> arch_state) s (asid_high_bits_of asid) = None \<longrightarrow> ([VSRef (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) asid)) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], pd) \<notin> vs_lookup s) \<and> (\<forall>x. (arm_asid_table \<circ> arch_state) s (asid_high_bits_of asid) = Some x \<longrightarrow> (\<forall>pool. ako_at (ASIDPool pool) x s \<longrightarrow> (if pool (UCAST(32 \<rightarrow> 10) asid) = Some pd then [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> x else (\<lambda>s. ([VSRef (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) asid)) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], pd) \<notin> vs_lookup s)) s)) proof (prove)
goal (1 subgoal):
 1. \<And>s. (asid_table s (asid_high_bits_of asid) = None \<longrightarrow> ([VSRef (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) asid)) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], pd) \<notin> vs_lookup s) \<and> (\<forall>x. asid_table s (asid_high_bits_of asid) = Some x \<longrightarrow> (\<forall>pool. (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd \<longrightarrow> ako_at (ASIDPool pool) x s \<longrightarrow> ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> x) s) \<and> (pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> Some pd \<longrightarrow> ako_at (ASIDPool pool) x s \<longrightarrow> ([VSRef (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) asid)) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], pd) \<notin> vs_lookup s))) proof (prove)
goal (3 subgoals):
 1. \<And>s. asid_table s (asid_high_bits_of asid) = None \<Longrightarrow> ([VSRef (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) asid)) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], pd) \<notin> vs_lookup s
 2. \<And>s x pool. \<lbrakk>asid_table s (asid_high_bits_of asid) = Some x; pool (UCAST(32 \<rightarrow> 10) asid) = Some pd; ako_at (ASIDPool pool) x s\<rbrakk> \<Longrightarrow> ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> x) s
 3. \<And>s x pool. \<lbrakk>asid_table s (asid_high_bits_of asid) = Some x; pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> Some pd; ako_at (ASIDPool pool) x s\<rbrakk> \<Longrightarrow> ([VSRef (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) asid)) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], pd) \<notin> vs_lookup s proof (prove)
goal (2 subgoals):
 1. \<And>s x pool. \<lbrakk>asid_table s (asid_high_bits_of asid) = Some x; pool (UCAST(32 \<rightarrow> 10) asid) = Some pd; ako_at (ASIDPool pool) x s\<rbrakk> \<Longrightarrow> ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> x) s
 2. \<And>s x pool. \<lbrakk>asid_table s (asid_high_bits_of asid) = Some x; pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> Some pd; ako_at (ASIDPool pool) x s\<rbrakk> \<Longrightarrow> ([VSRef (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) asid)) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], pd) \<notin> vs_lookup s proof (prove)
goal (1 subgoal):
 1. \<And>s x pool. \<lbrakk>asid_table s (asid_high_bits_of asid) = Some x; pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> Some pd; ako_at (ASIDPool pool) x s\<rbrakk> \<Longrightarrow> ([VSRef (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) asid)) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], pd) \<notin> vs_lookup s proof (prove)
goal (1 subgoal):
 1. \<And>s x pool ko. \<lbrakk>pool (UCAST(32 \<rightarrow> 10) asid) \<noteq> Some pd; ako_at (ASIDPool pool) x s; asid_table s (asid_high_bits_of asid) = Some x; ko_at ko x s; (VSRef (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) asid)) (Some AASIDPool), pd) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!