theory ArchArch_IF

lemma get_asid_pool_revrv:
  "reads_equiv_valid_rv_inv (affects_equiv aag l) aag (\<lambda>rv rv'. rv (ucast asid) = rv' (ucast asid))
                            (\<lambda>s. Some a = arm_asid_table (arch_state s) (asid_high_bits_of asid) \<and>
                                 is_subject_asid aag asid \<and> asid \<noteq> 0)
                            (get_asid_pool a)" unfolding get_asid_pool_def apply (rule equiv_valid_rv_guard_imp) apply (rule_tac R'="\<lambda>rv rv'. \<forall>p p'. rv = ArchObj (ASIDPool p) \<and> rv' = ArchObj (ASIDPool p')
                                       \<longrightarrow> p (ucast asid) = p' (ucast asid)"
               and P="\<lambda>s. Some a = arm_asid_table (arch_state s) (asid_high_bits_of asid) \<and>
                          is_subject_asid aag asid \<and> asid \<noteq> 0"
               and P'="\<lambda>s. Some a = arm_asid_table (arch_state s) (asid_high_bits_of asid) \<and>
                           is_subject_asid aag asid \<and> asid \<noteq> 0"
                in equiv_valid_2_bind) apply (clarsimp split: kernel_object.splits arch_kernel_obj.splits
                       simp: fail_ev2_l fail_ev2_r return_ev2) apply (clarsimp simp: get_object_def gets_def assert_def bind_def put_def get_def
                           equiv_valid_2_def return_def fail_def
                    split: if_split) apply (erule reads_equivE) apply (clarsimp simp: equiv_asids_def equiv_asid_def asid_pool_at_kheap) apply (drule aag_can_read_own_asids) apply (drule_tac s="Some a" in sym) apply force apply (wp wp_post_taut | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_rv_inv (affects_equiv aag l) aag (\<lambda>rv rv'. rv (UCAST(32 \<rightarrow> 10) asid) = rv' (UCAST(32 \<rightarrow> 10) asid)) (\<lambda>s. Some a = asid_table s (asid_high_bits_of asid) \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) (get_asid_pool a) proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_rv_inv (affects_equiv aag l) aag (\<lambda>rv rv'. rv (UCAST(32 \<rightarrow> 10) asid) = rv' (UCAST(32 \<rightarrow> 10) asid)) (\<lambda>s. Some a = asid_table s (asid_high_bits_of asid) \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) (do kobj <- get_object a;
case kobj of ArchObj (ASIDPool pool) \<Rightarrow> return pool | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail
od) proof (prove)
goal (2 subgoals):
 1. reads_equiv_valid_rv_inv (affects_equiv aag l) aag (\<lambda>rv rv'. rv (UCAST(32 \<rightarrow> 10) asid) = rv' (UCAST(32 \<rightarrow> 10) asid)) ?P (do kobj <- get_object a;
case kobj of ArchObj (ASIDPool pool) \<Rightarrow> return pool | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail
od)
 2. \<And>s. Some a = asid_table s (asid_high_bits_of asid) \<and> is_subject_asid aag asid \<and> asid \<noteq> 0 \<Longrightarrow> ?P s proof (prove)
goal (5 subgoals):
 1. \<And>rv rv'. \<forall>p p'. rv = ArchObj (ASIDPool p) \<and> rv' = ArchObj (ASIDPool p') \<longrightarrow> p (UCAST(32 \<rightarrow> 10) asid) = p' (UCAST(32 \<rightarrow> 10) asid) \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (\<lambda>rv rv'. rv (UCAST(32 \<rightarrow> 10) asid) = rv' (UCAST(32 \<rightarrow> 10) asid)) (?Q3 rv) (?Q'3 rv') (case rv of ArchObj (ASIDPool pool) \<Rightarrow> return pool | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail) (case rv' of ArchObj (ASIDPool pool) \<Rightarrow> return pool | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail)
 2. reads_equiv_valid_rv_inv (affects_equiv aag l) aag (\<lambda>rv rv'. \<forall>p p'. rv = ArchObj (ASIDPool p) \<and> rv' = ArchObj (ASIDPool p') \<longrightarrow> p (UCAST(32 \<rightarrow> 10) asid) = p' (UCAST(32 \<rightarrow> 10) asid)) (\<lambda>s. Some a = asid_table s (asid_high_bits_of asid) \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) (get_object a)
 3. \<lbrace>?S3\<rbrace> get_object a \<lbrace>?Q3\<rbrace>
 4. \<lbrace>?S3\<rbrace> get_object a \<lbrace>?Q'3\<rbrace>
 5. \<And>s. Some a = asid_table s (asid_high_bits_of asid) \<and> is_subject_asid aag asid \<and> asid \<noteq> 0 \<Longrightarrow> (Some a = asid_table s (asid_high_bits_of asid) \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) \<and> ?S3 s proof (prove)
goal (4 subgoals):
 1. reads_equiv_valid_rv_inv (affects_equiv aag l) aag (\<lambda>rv rv'. \<forall>p p'. rv = ArchObj (ASIDPool p) \<and> rv' = ArchObj (ASIDPool p') \<longrightarrow> p (UCAST(32 \<rightarrow> 10) asid) = p' (UCAST(32 \<rightarrow> 10) asid)) (\<lambda>s. Some a = asid_table s (asid_high_bits_of asid) \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) (get_object a)
 2. \<lbrace>?S3\<rbrace> get_object a \<lbrace>?Q3\<rbrace>
 3. \<lbrace>?S3\<rbrace> get_object a \<lbrace>?Q'3\<rbrace>
 4. \<And>s. Some a = asid_table s (asid_high_bits_of asid) \<and> is_subject_asid aag asid \<and> asid \<noteq> 0 \<Longrightarrow> (Some a = asid_table s (asid_high_bits_of asid) \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) \<and> ?S3 s proof (prove)
goal (4 subgoals):
 1. \<And>s t p p'. \<lbrakk>kheap s a = Some (ArchObj (ASIDPool p)); kheap t a = Some (ArchObj (ASIDPool p')); asid_table t (asid_high_bits_of asid) = asid_table s (asid_high_bits_of asid); Some a = asid_table s (asid_high_bits_of asid); is_subject_asid aag asid; asid \<noteq> 0; reads_equiv aag s t; affects_equiv aag l s t\<rbrakk> \<Longrightarrow> p (UCAST(32 \<rightarrow> 10) asid) = p' (UCAST(32 \<rightarrow> 10) asid)
 2. \<lbrace>?S3\<rbrace> get_object a \<lbrace>?Q3\<rbrace>
 3. \<lbrace>?S3\<rbrace> get_object a \<lbrace>?Q'3\<rbrace>
 4. \<And>s. Some a = asid_table s (asid_high_bits_of asid) \<and> is_subject_asid aag asid \<and> asid \<noteq> 0 \<Longrightarrow> (Some a = asid_table s (asid_high_bits_of asid) \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) \<and> ?S3 s proof (prove)
goal (4 subgoals):
 1. \<And>s t p p'. \<lbrakk>kheap s a = Some (ArchObj (ASIDPool p)); kheap t a = Some (ArchObj (ASIDPool p')); asid_table t (asid_high_bits_of asid) = asid_table s (asid_high_bits_of asid); Some a = asid_table s (asid_high_bits_of asid); is_subject_asid aag asid; asid \<noteq> 0; affects_equiv aag l s t; equiv_for (aag_can_read aag) kheap s t; equiv_machine_state (aag_can_read aag) (machine_state s) (machine_state t); equiv_for (aag_can_read aag \<circ> fst) cdt s t; equiv_for (aag_can_read aag \<circ> fst) cdt_list s t; equiv_for (aag_can_read aag) ekheap s t; equiv_for (aag_can_read aag \<circ> fst) is_original_cap s t; equiv_for (aag_can_read_irq aag) interrupt_states s t; equiv_for (aag_can_read_irq aag) interrupt_irq_node s t; equiv_asids (aag_can_read_asid aag) s t; equiv_for (aag_can_read_domain aag) ready_queues s t; cur_thread s = cur_thread t; cur_domain s = cur_domain t; scheduler_action s = scheduler_action t; work_units_completed s = work_units_completed t; equiv_irq_state (machine_state s) (machine_state t)\<rbrakk> \<Longrightarrow> p (UCAST(32 \<rightarrow> 10) asid) = p' (UCAST(32 \<rightarrow> 10) asid)
 2. \<lbrace>?S3\<rbrace> get_object a \<lbrace>?Q3\<rbrace>
 3. \<lbrace>?S3\<rbrace> get_object a \<lbrace>?Q'3\<rbrace>
 4. \<And>s. Some a = asid_table s (asid_high_bits_of asid) \<and> is_subject_asid aag asid \<and> asid \<noteq> 0 \<Longrightarrow> (Some a = asid_table s (asid_high_bits_of asid) \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) \<and> ?S3 s proof (prove)
goal (4 subgoals):
 1. \<And>s t p p'. \<lbrakk>kheap s a = Some (ArchObj (ASIDPool p)); kheap t a = Some (ArchObj (ASIDPool p')); Some a = asid_table t (asid_high_bits_of asid); is_subject_asid aag asid; asid \<noteq> 0; affects_equiv aag l s t; equiv_for (aag_can_read aag) kheap s t; equiv_for (aag_can_read aag \<circ> fst) cdt s t; equiv_for (aag_can_read aag \<circ> fst) cdt_list s t; equiv_for (aag_can_read aag) ekheap s t; equiv_for (aag_can_read aag \<circ> fst) is_original_cap s t; equiv_for (aag_can_read_irq aag) interrupt_states s t; equiv_for (aag_can_read_irq aag) interrupt_irq_node s t; \<forall>asid. asid \<noteq> 0 \<and> aag_can_read_asid aag asid \<longrightarrow> asid_table s (asid_high_bits_of asid) = asid_table t (asid_high_bits_of asid) \<and> (\<forall>pool_ptr. asid_table s (asid_high_bits_of asid) = Some pool_ptr \<longrightarrow> (\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool))) = (\<exists>asid_pool. kheap t pool_ptr = Some (ArchObj (ASIDPool asid_pool))) \<and> (\<forall>asid_pool asid_pool'. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)) \<and> kheap t pool_ptr = Some (ArchObj (ASIDPool asid_pool')) \<longrightarrow> asid_pool (UCAST(32 \<rightarrow> 10) asid) = asid_pool' (UCAST(32 \<rightarrow> 10) asid))); equiv_for (aag_can_read_domain aag) ready_queues s t; cur_thread s = cur_thread t; cur_domain s = cur_domain t; scheduler_action s = scheduler_action t; work_units_completed s = work_units_completed t; equiv_irq_state (machine_state s) (machine_state t); equiv_for (aag_can_read aag) underlying_memory (machine_state s) (machine_state t); equiv_for (aag_can_read aag) device_state (machine_state s) (machine_state t)\<rbrakk> \<Longrightarrow> p (UCAST(32 \<rightarrow> 10) asid) = p' (UCAST(32 \<rightarrow> 10) asid)
 2. \<lbrace>?S3\<rbrace> get_object a \<lbrace>?Q3\<rbrace>
 3. \<lbrace>?S3\<rbrace> get_object a \<lbrace>?Q'3\<rbrace>
 4. \<And>s. Some a = asid_table s (asid_high_bits_of asid) \<and> is_subject_asid aag asid \<and> asid \<noteq> 0 \<Longrightarrow> (Some a = asid_table s (asid_high_bits_of asid) \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) \<and> ?S3 s proof (prove)
goal (4 subgoals):
 1. \<And>s t p p'. \<lbrakk>kheap s a = Some (ArchObj (ASIDPool p)); kheap t a = Some (ArchObj (ASIDPool p')); Some a = asid_table t (asid_high_bits_of asid); asid \<noteq> 0; affects_equiv aag l s t; equiv_for (aag_can_read aag) kheap s t; equiv_for (aag_can_read aag \<circ> fst) cdt s t; equiv_for (aag_can_read aag \<circ> fst) cdt_list s t; equiv_for (aag_can_read aag) ekheap s t; equiv_for (aag_can_read aag \<circ> fst) is_original_cap s t; equiv_for (aag_can_read_irq aag) interrupt_states s t; equiv_for (aag_can_read_irq aag) interrupt_irq_node s t; \<forall>asid. asid \<noteq> 0 \<and> aag_can_read_asid aag asid \<longrightarrow> asid_table s (asid_high_bits_of asid) = asid_table t (asid_high_bits_of asid) \<and> (\<forall>pool_ptr. asid_table s (asid_high_bits_of asid) = Some pool_ptr \<longrightarrow> (\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool))) = (\<exists>asid_pool. kheap t pool_ptr = Some (ArchObj (ASIDPool asid_pool))) \<and> (\<forall>asid_pool asid_pool'. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)) \<and> kheap t pool_ptr = Some (ArchObj (ASIDPool asid_pool')) \<longrightarrow> asid_pool (UCAST(32 \<rightarrow> 10) asid) = asid_pool' (UCAST(32 \<rightarrow> 10) asid))); equiv_for (aag_can_read_domain aag) ready_queues s t; cur_thread s = cur_thread t; cur_domain s = cur_domain t; scheduler_action s = scheduler_action t; work_units_completed s = work_units_completed t; equiv_irq_state (machine_state s) (machine_state t); equiv_for (aag_can_read aag) underlying_memory (machine_state s) (machine_state t); equiv_for (aag_can_read aag) device_state (machine_state s) (machine_state t); aag_can_read_asid aag asid\<rbrakk> \<Longrightarrow> p (UCAST(32 \<rightarrow> 10) asid) = p' (UCAST(32 \<rightarrow> 10) asid)
 2. \<lbrace>?S3\<rbrace> get_object a \<lbrace>?Q3\<rbrace>
 3. \<lbrace>?S3\<rbrace> get_object a \<lbrace>?Q'3\<rbrace>
 4. \<And>s. Some a = asid_table s (asid_high_bits_of asid) \<and> is_subject_asid aag asid \<and> asid \<noteq> 0 \<Longrightarrow> (Some a = asid_table s (asid_high_bits_of asid) \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) \<and> ?S3 s proof (prove)
goal (4 subgoals):
 1. \<And>s t p p'. \<lbrakk>kheap s a = Some (ArchObj (ASIDPool p)); kheap t a = Some (ArchObj (ASIDPool p')); asid \<noteq> 0; affects_equiv aag l s t; equiv_for (aag_can_read aag) kheap s t; equiv_for (aag_can_read aag \<circ> fst) cdt s t; equiv_for (aag_can_read aag \<circ> fst) cdt_list s t; equiv_for (aag_can_read aag) ekheap s t; equiv_for (aag_can_read aag \<circ> fst) is_original_cap s t; equiv_for (aag_can_read_irq aag) interrupt_states s t; equiv_for (aag_can_read_irq aag) interrupt_irq_node s t; \<forall>asid. asid \<noteq> 0 \<and> aag_can_read_asid aag asid \<longrightarrow> asid_table s (asid_high_bits_of asid) = asid_table t (asid_high_bits_of asid) \<and> (\<forall>pool_ptr. asid_table s (asid_high_bits_of asid) = Some pool_ptr \<longrightarrow> (\<exists>asid_pool. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool))) = (\<exists>asid_pool. kheap t pool_ptr = Some (ArchObj (ASIDPool asid_pool))) \<and> (\<forall>asid_pool asid_pool'. kheap s pool_ptr = Some (ArchObj (ASIDPool asid_pool)) \<and> kheap t pool_ptr = Some (ArchObj (ASIDPool asid_pool')) \<longrightarrow> asid_pool (UCAST(32 \<rightarrow> 10) asid) = asid_pool' (UCAST(32 \<rightarrow> 10) asid))); equiv_for (aag_can_read_domain aag) ready_queues s t; cur_thread s = cur_thread t; cur_domain s = cur_domain t; scheduler_action s = scheduler_action t; work_units_completed s = work_units_completed t; equiv_irq_state (machine_state s) (machine_state t); equiv_for (aag_can_read aag) underlying_memory (machine_state s) (machine_state t); equiv_for (aag_can_read aag) device_state (machine_state s) (machine_state t); aag_can_read_asid aag asid; asid_table t (asid_high_bits_of asid) = Some a\<rbrakk> \<Longrightarrow> p (UCAST(32 \<rightarrow> 10) asid) = p' (UCAST(32 \<rightarrow> 10) asid)
 2. \<lbrace>?S3\<rbrace> get_object a \<lbrace>?Q3\<rbrace>
 3. \<lbrace>?S3\<rbrace> get_object a \<lbrace>?Q'3\<rbrace>
 4. \<And>s. Some a = asid_table s (asid_high_bits_of asid) \<and> is_subject_asid aag asid \<and> asid \<noteq> 0 \<Longrightarrow> (Some a = asid_table s (asid_high_bits_of asid) \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) \<and> ?S3 s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?S3\<rbrace> get_object a \<lbrace>?Q3\<rbrace>
 2. \<lbrace>?S3\<rbrace> get_object a \<lbrace>?Q'3\<rbrace>
 3. \<And>s. Some a = asid_table s (asid_high_bits_of asid) \<and> is_subject_asid aag asid \<and> asid \<noteq> 0 \<Longrightarrow> (Some a = asid_table s (asid_high_bits_of asid) \<and> is_subject_asid aag asid \<and> asid \<noteq> 0) \<and> ?S3 s proof (prove)
goal:
No subgoals!