theory ArchDetSchedAux_AI

lemma perform_asid_control_etcb_at:"\<lbrace>(\<lambda>s. etcb_at P t s) and valid_etcbs\<rbrace>
          perform_asid_control_invocation aci
          \<lbrace>\<lambda>r s. st_tcb_at (Not \<circ> inactive) t s \<longrightarrow> etcb_at P t s\<rbrace>" apply (simp add: perform_asid_control_invocation_def) apply (rule hoare_pre) apply (wp | wpc | simp)+ apply (wp hoare_imp_lift_something typ_at_pred_tcb_at_lift)[1] apply (rule hoare_drop_imps) apply (wp retype_region_etcb_at)+ apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>etcb_at P t and valid_etcbs\<rbrace> perform_asid_control_invocation aci \<lbrace>\<lambda>r s. st_tcb_at (Not \<circ> inactive) t s \<longrightarrow> etcb_at P t s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>etcb_at P t and valid_etcbs\<rbrace> case aci of MakePool frame slot parent base \<Rightarrow> do delete_objects frame page_bits;
pcap <- get_cap parent;
set_cap (max_free_index_update pcap) parent;
retype_region frame 1 0 (ArchObject ASIDPoolObj) False;
cap_insert (ArchObjectCap $ ASIDPoolCap frame base) parent slot;
assert (base && mask local.asid_low_bits = 0);
asid_table <- gets (arm_asid_table \<circ> arch_state);
asid_table' <- return (asid_table(asid_high_bits_of base \<mapsto> frame));
modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := asid_table'\<rparr>\<rparr>)
od \<lbrace>\<lambda>r s. st_tcb_at (Not \<circ> inactive) t s \<longrightarrow> etcb_at P t s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> case aci of MakePool frame slot parent base \<Rightarrow> do delete_objects frame page_bits;
pcap <- get_cap parent;
set_cap (max_free_index_update pcap) parent;
retype_region frame 1 0 (ArchObject ASIDPoolObj) False;
cap_insert (ArchObjectCap $ ASIDPoolCap frame base) parent slot;
assert (base && mask local.asid_low_bits = 0);
asid_table <- gets (arm_asid_table \<circ> arch_state);
asid_table' <- return (asid_table(asid_high_bits_of base \<mapsto> frame));
modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := asid_table'\<rparr>\<rparr>)
od \<lbrace>\<lambda>r s. st_tcb_at (Not \<circ> inactive) t s \<longrightarrow> etcb_at P t s\<rbrace>
 2. \<And>s. (etcb_at P t and valid_etcbs) s \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>x1 x2 x3 x4 pcap xb. aci = MakePool x1 x2 x3 x4 \<Longrightarrow> \<lbrace>?B19 x1 x2 x3 x4 () pcap () xb\<rbrace> cap_insert (ArchObjectCap (ASIDPoolCap x1 x4)) x3 x2 \<lbrace>\<lambda>xc s. x4 && mask local.asid_low_bits = 0 \<longrightarrow> st_tcb_at (Not \<circ> inactive) t s \<longrightarrow> etcb_at P t s\<rbrace>
 2. \<And>x1 x2 x3 x4 x pcap xa. aci = MakePool x1 x2 x3 x4 \<Longrightarrow> \<lbrace>?B17 x1 x2 x3 x4 x pcap xa\<rbrace> retype_region x1 1 0 (ArchObject ASIDPoolObj) False \<lbrace>?B19 x1 x2 x3 x4 x pcap xa\<rbrace>
 3. \<And>x1 x2 x3 x4 x pcap. aci = MakePool x1 x2 x3 x4 \<Longrightarrow> \<lbrace>?B16 x1 x2 x3 x4 x pcap\<rbrace> set_cap (max_free_index_update pcap) x3 \<lbrace>?B17 x1 x2 x3 x4 x pcap\<rbrace>
 4. \<And>x1 x2 x3 x4 x. aci = MakePool x1 x2 x3 x4 \<Longrightarrow> \<lbrace>?B14 x1 x2 x3 x4 x\<rbrace> get_cap x3 \<lbrace>?B16 x1 x2 x3 x4 x\<rbrace>
 5. \<And>x1 x2 x3 x4. aci = MakePool x1 x2 x3 x4 \<Longrightarrow> \<lbrace>?R12 x1 x2 x3 x4\<rbrace> delete_objects x1 page_bits \<lbrace>?B14 x1 x2 x3 x4\<rbrace>
 6. \<And>s. (etcb_at P t and valid_etcbs) s \<Longrightarrow> \<forall>x xa xb xc. aci = MakePool x xa xb xc \<longrightarrow> ?R12 x xa xb xc s proof (prove)
goal (5 subgoals):
 1. \<And>x1 x2 x3 x4 x pcap xa. aci = MakePool x1 x2 x3 x4 \<Longrightarrow> \<lbrace>?B17 x1 x2 x3 x4 x pcap xa\<rbrace> retype_region x1 1 0 (ArchObject ASIDPoolObj) False \<lbrace>\<lambda>a b. x4 && mask local.asid_low_bits = 0 \<longrightarrow> st_tcb_at (Not \<circ> inactive) t b \<longrightarrow> etcb_at P t b\<rbrace>
 2. \<And>x1 x2 x3 x4 x pcap. aci = MakePool x1 x2 x3 x4 \<Longrightarrow> \<lbrace>?B16 x1 x2 x3 x4 x pcap\<rbrace> set_cap (max_free_index_update pcap) x3 \<lbrace>?B17 x1 x2 x3 x4 x pcap\<rbrace>
 3. \<And>x1 x2 x3 x4 x. aci = MakePool x1 x2 x3 x4 \<Longrightarrow> \<lbrace>?B14 x1 x2 x3 x4 x\<rbrace> get_cap x3 \<lbrace>?B16 x1 x2 x3 x4 x\<rbrace>
 4. \<And>x1 x2 x3 x4. aci = MakePool x1 x2 x3 x4 \<Longrightarrow> \<lbrace>?R12 x1 x2 x3 x4\<rbrace> delete_objects x1 page_bits \<lbrace>?B14 x1 x2 x3 x4\<rbrace>
 5. \<And>s. (etcb_at P t and valid_etcbs) s \<Longrightarrow> \<forall>x xa xb xc. aci = MakePool x xa xb xc \<longrightarrow> ?R12 x xa xb xc s proof (prove)
goal (5 subgoals):
 1. \<And>x1 x2 x3 x4 x pcap xa. aci = MakePool x1 x2 x3 x4 \<Longrightarrow> \<lbrace>?B17 x1 x2 x3 x4 x pcap xa\<rbrace> retype_region x1 1 0 (ArchObject ASIDPoolObj) False \<lbrace>\<lambda>rv s. st_tcb_at (Not \<circ> inactive) t s \<longrightarrow> etcb_at P t s\<rbrace>
 2. \<And>x1 x2 x3 x4 x pcap. aci = MakePool x1 x2 x3 x4 \<Longrightarrow> \<lbrace>?B16 x1 x2 x3 x4 x pcap\<rbrace> set_cap (max_free_index_update pcap) x3 \<lbrace>?B17 x1 x2 x3 x4 x pcap\<rbrace>
 3. \<And>x1 x2 x3 x4 x. aci = MakePool x1 x2 x3 x4 \<Longrightarrow> \<lbrace>?B14 x1 x2 x3 x4 x\<rbrace> get_cap x3 \<lbrace>?B16 x1 x2 x3 x4 x\<rbrace>
 4. \<And>x1 x2 x3 x4. aci = MakePool x1 x2 x3 x4 \<Longrightarrow> \<lbrace>?R12 x1 x2 x3 x4\<rbrace> delete_objects x1 page_bits \<lbrace>?B14 x1 x2 x3 x4\<rbrace>
 5. \<And>s. (etcb_at P t and valid_etcbs) s \<Longrightarrow> \<forall>x xa xb xc. aci = MakePool x xa xb xc \<longrightarrow> ?R12 x xa xb xc s proof (prove)
goal (1 subgoal):
 1. \<And>s. (etcb_at P t and valid_etcbs) s \<Longrightarrow> \<forall>x xa xb xc. aci = MakePool x xa xb xc \<longrightarrow> etcb_at P t s \<and> valid_etcbs s proof (prove)
goal:
No subgoals!