theory ArchArch_IF

lemma set_object_equiv_but_for_labels:
  "\<lbrace>equiv_but_for_labels aag L st and (\<lambda> s. \<not> asid_pool_at ptr s) and
    K ((\<forall>asid_pool. obj \<noteq> ArchObj (ASIDPool asid_pool)) \<and> pasObjectAbs aag ptr \<in> L)\<rbrace>
   set_object ptr obj
   \<lbrace>\<lambda>_. equiv_but_for_labels aag L st\<rbrace>" apply (wpsimp wp: set_object_wp) apply (clarsimp simp: equiv_but_for_labels_def) apply (subst dummy_kheap_update[where st=st]) apply (rule states_equiv_for_non_asid_pool_kheap_update) apply assumption apply (fastforce intro: equiv_forI elim: states_equiv_forE equiv_forE) apply (fastforce simp: non_asid_pool_kheap_update_def) apply (clarsimp simp: non_asid_pool_kheap_update_def asid_pool_at_kheap) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>equiv_but_for_labels aag L st and (\<lambda>s. \<not> typ_at (AArch AASIDPool) ptr s) and K ((\<forall>asid_pool. obj \<noteq> ArchObj (ASIDPool asid_pool)) \<and> pasObjectAbs aag ptr \<in> L)\<rbrace> set_object ptr obj \<lbrace>\<lambda>_. equiv_but_for_labels aag L st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>equiv_but_for_labels aag L st s; \<not> typ_at (AArch AASIDPool) ptr s; \<forall>asid_pool. obj \<noteq> ArchObj (ASIDPool asid_pool); pasObjectAbs aag ptr \<in> L\<rbrakk> \<Longrightarrow> equiv_but_for_labels aag L st (s\<lparr>kheap := (kheap s)(ptr \<mapsto> obj)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<not> typ_at (AArch AASIDPool) ptr s; \<forall>asid_pool. obj \<noteq> ArchObj (ASIDPool asid_pool); pasObjectAbs aag ptr \<in> L; states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st s; cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) (machine_state s)\<rbrakk> \<Longrightarrow> states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (s\<lparr>kheap := (kheap s)(ptr \<mapsto> obj)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<not> typ_at (AArch AASIDPool) ptr s; \<forall>asid_pool. obj \<noteq> ArchObj (ASIDPool asid_pool); pasObjectAbs aag ptr \<in> L; states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st s; cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) (machine_state s)\<rbrakk> \<Longrightarrow> states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) (st\<lparr>kheap := kheap st\<rparr>) (s\<lparr>kheap := (kheap s)(ptr \<mapsto> obj)\<rparr>) proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>\<not> typ_at (AArch AASIDPool) ptr s; \<forall>asid_pool. obj \<noteq> ArchObj (ASIDPool asid_pool); pasObjectAbs aag ptr \<in> L; states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st s; cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) (machine_state s)\<rbrakk> \<Longrightarrow> states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st s
 2. \<And>s. \<lbrakk>\<not> typ_at (AArch AASIDPool) ptr s; \<forall>asid_pool. obj \<noteq> ArchObj (ASIDPool asid_pool); pasObjectAbs aag ptr \<in> L; states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st s; cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) (machine_state s)\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) id (kheap st) ((kheap s)(ptr \<mapsto> obj))
 3. \<And>s. \<lbrakk>\<not> typ_at (AArch AASIDPool) ptr s; \<forall>asid_pool. obj \<noteq> ArchObj (ASIDPool asid_pool); pasObjectAbs aag ptr \<in> L; states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st s; cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) (machine_state s)\<rbrakk> \<Longrightarrow> non_asid_pool_kheap_update st (kheap st)
 4. \<And>s. \<lbrakk>\<not> typ_at (AArch AASIDPool) ptr s; \<forall>asid_pool. obj \<noteq> ArchObj (ASIDPool asid_pool); pasObjectAbs aag ptr \<in> L; states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st s; cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) (machine_state s)\<rbrakk> \<Longrightarrow> non_asid_pool_kheap_update s ((kheap s)(ptr \<mapsto> obj)) proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>\<not> typ_at (AArch AASIDPool) ptr s; \<forall>asid_pool. obj \<noteq> ArchObj (ASIDPool asid_pool); pasObjectAbs aag ptr \<in> L; states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st s; cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) (machine_state s)\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) id (kheap st) ((kheap s)(ptr \<mapsto> obj))
 2. \<And>s. \<lbrakk>\<not> typ_at (AArch AASIDPool) ptr s; \<forall>asid_pool. obj \<noteq> ArchObj (ASIDPool asid_pool); pasObjectAbs aag ptr \<in> L; states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st s; cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) (machine_state s)\<rbrakk> \<Longrightarrow> non_asid_pool_kheap_update st (kheap st)
 3. \<And>s. \<lbrakk>\<not> typ_at (AArch AASIDPool) ptr s; \<forall>asid_pool. obj \<noteq> ArchObj (ASIDPool asid_pool); pasObjectAbs aag ptr \<in> L; states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st s; cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) (machine_state s)\<rbrakk> \<Longrightarrow> non_asid_pool_kheap_update s ((kheap s)(ptr \<mapsto> obj)) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<not> typ_at (AArch AASIDPool) ptr s; \<forall>asid_pool. obj \<noteq> ArchObj (ASIDPool asid_pool); pasObjectAbs aag ptr \<in> L; states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st s; cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) (machine_state s)\<rbrakk> \<Longrightarrow> non_asid_pool_kheap_update st (kheap st)
 2. \<And>s. \<lbrakk>\<not> typ_at (AArch AASIDPool) ptr s; \<forall>asid_pool. obj \<noteq> ArchObj (ASIDPool asid_pool); pasObjectAbs aag ptr \<in> L; states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st s; cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) (machine_state s)\<rbrakk> \<Longrightarrow> non_asid_pool_kheap_update s ((kheap s)(ptr \<mapsto> obj)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<not> typ_at (AArch AASIDPool) ptr s; \<forall>asid_pool. obj \<noteq> ArchObj (ASIDPool asid_pool); pasObjectAbs aag ptr \<in> L; states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st s; cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) (machine_state s)\<rbrakk> \<Longrightarrow> non_asid_pool_kheap_update s ((kheap s)(ptr \<mapsto> obj)) proof (prove)
goal:
No subgoals!