theory ArchArch_IF

lemma perform_asid_control_invocation_reads_respects:
  notes K_bind_ev[wp del]
  shows "reads_respects aag l (K (authorised_asid_control_inv aag aci))
                        (perform_asid_control_invocation aci)" unfolding perform_asid_control_invocation_def apply (rule gen_asm_ev) apply (rule equiv_valid_guard_imp) 
   (* we do some hacky rewriting here to separate out the bit that does interesting stuff from the rest *)
    apply (subst (6) my_bind_rewrite_lemma) apply (subst (1) bind_assoc[symmetric]) apply (subst another_hacky_rewrite) apply (subst another_hacky_rewrite) apply (wpc) apply (rule bind_ev) apply (rule K_bind_ev) apply (rule_tac P'=\<top> in bind_ev) apply (rule K_bind_ev) apply (rule bind_ev) apply (rule bind_ev) apply (rule return_ev) apply (rule K_bind_ev) apply simp apply (rule arm_asid_table_update_reads_respects) apply (wp cap_insert_reads_respects retype_region_reads_respects
                   set_cap_reads_respects delete_objects_reads_respects get_cap_rev
                | simp add: authorised_asid_control_inv_def)+ apply (auto dest!: is_aligned_no_overflow) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (authorised_asid_control_inv aag aci)) (perform_asid_control_invocation aci) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (authorised_asid_control_inv aag aci)) (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) proof (prove)
goal (1 subgoal):
 1. authorised_asid_control_inv aag aci \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (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) proof (prove)
goal (2 subgoals):
 1. authorised_asid_control_inv aag aci \<Longrightarrow> reads_respects aag l ?Q2 (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)
 2. \<And>s. \<lbrakk>authorised_asid_control_inv aag aci; True\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (2 subgoals):
 1. authorised_asid_control_inv aag aci \<Longrightarrow> reads_respects aag l ?Q2 (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)
 2. \<And>s. \<lbrakk>authorised_asid_control_inv aag aci; True\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (2 subgoals):
 1. authorised_asid_control_inv aag aci \<Longrightarrow> reads_respects aag l ?Q2 (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;
r <- assert (base && mask local.asid_low_bits = 0);
x <- K_bind (do 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) r;
return ()
od)
 2. \<And>s. \<lbrakk>authorised_asid_control_inv aag aci; True\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (2 subgoals):
 1. authorised_asid_control_inv aag aci \<Longrightarrow> reads_respects aag l ?Q2 (case aci of MakePool frame slot parent base \<Rightarrow> do delete_objects frame page_bits;
do pcap <- get_cap parent;
set_cap (max_free_index_update pcap) parent
od;
retype_region frame 1 0 (ArchObject ASIDPoolObj) False;
cap_insert (ArchObjectCap $ ASIDPoolCap frame base) parent slot;
r <- assert (base && mask local.asid_low_bits = 0);
x <- K_bind (do 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) r;
return ()
od)
 2. \<And>s. \<lbrakk>authorised_asid_control_inv aag aci; True\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (2 subgoals):
 1. authorised_asid_control_inv aag aci \<Longrightarrow> reads_respects aag l ?Q2 (case aci of MakePool frame slot parent base \<Rightarrow> do delete_objects frame page_bits;
do _ <- do pcap <- get_cap parent;
set_cap (max_free_index_update pcap) parent
od;
retype_region frame 1 0 (ArchObject ASIDPoolObj) False
od;
cap_insert (ArchObjectCap $ ASIDPoolCap frame base) parent slot;
r <- assert (base && mask local.asid_low_bits = 0);
x <- K_bind (do 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) r;
return ()
od)
 2. \<And>s. \<lbrakk>authorised_asid_control_inv aag aci; True\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (2 subgoals):
 1. authorised_asid_control_inv aag aci \<Longrightarrow> reads_respects aag l ?Q2 (case aci of MakePool frame slot parent base \<Rightarrow> do delete_objects frame page_bits;
do _ <- do _ <- do pcap <- get_cap parent;
set_cap (max_free_index_update pcap) parent
od;
retype_region frame 1 0 (ArchObject ASIDPoolObj) False
od;
cap_insert (ArchObjectCap $ ASIDPoolCap frame base) parent slot
od;
r <- assert (base && mask local.asid_low_bits = 0);
x <- K_bind (do 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) r;
return ()
od)
 2. \<And>s. \<lbrakk>authorised_asid_control_inv aag aci; True\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 x3 x4. \<lbrakk>authorised_asid_control_inv aag aci; aci = MakePool x1 x2 x3 x4\<rbrakk> \<Longrightarrow> reads_respects aag l (?R26 x1 x2 x3 x4) (do delete_objects x1 page_bits;
do _ <- do _ <- do pcap <- get_cap x3;
set_cap (max_free_index_update pcap) x3
od;
retype_region x1 1 0 (ArchObject ASIDPoolObj) False
od;
cap_insert (ArchObjectCap $ ASIDPoolCap x1 x4) x3 x2
od;
r <- assert (x4 && mask local.asid_low_bits = 0);
x <- K_bind (do asid_table <- gets (arm_asid_table \<circ> arch_state);
asid_table' <- return (asid_table(asid_high_bits_of x4 \<mapsto> x1));
modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := asid_table'\<rparr>\<rparr>)
od) r;
return ()
od)
 2. \<And>s. \<lbrakk>authorised_asid_control_inv aag aci; True\<rbrakk> \<Longrightarrow> \<forall>x xa xb xc. aci = MakePool x xa xb xc \<longrightarrow> ?R26 x xa xb xc s proof (prove)
goal (4 subgoals):
 1. \<And>x1 x2 x3 x4 rv. \<lbrakk>authorised_asid_control_inv aag aci; aci = MakePool x1 x2 x3 x4\<rbrakk> \<Longrightarrow> reads_respects aag l (?Q27 x1 x2 x3 x4 rv) (K_bind (do do _ <- do _ <- do pcap <- get_cap x3;
set_cap (max_free_index_update pcap) x3
od;
retype_region x1 1 0 (ArchObject ASIDPoolObj) False
od;
cap_insert (ArchObjectCap $ ASIDPoolCap x1 x4) x3 x2
od;
r <- assert (x4 && mask local.asid_low_bits = 0);
x <- K_bind (do asid_table <- gets (arm_asid_table \<circ> arch_state);
asid_table' <- return (asid_table(asid_high_bits_of x4 \<mapsto> x1));
modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := asid_table'\<rparr>\<rparr>)
od) r;
return ()
od) rv)
 2. \<And>x1 x2 x3 x4. \<lbrakk>authorised_asid_control_inv aag aci; aci = MakePool x1 x2 x3 x4\<rbrakk> \<Longrightarrow> reads_respects aag l (?P'27 x1 x2 x3 x4) (delete_objects x1 page_bits)
 3. \<And>x1 x2 x3 x4. \<lbrakk>authorised_asid_control_inv aag aci; aci = MakePool x1 x2 x3 x4\<rbrakk> \<Longrightarrow> \<lbrace>?P''27 x1 x2 x3 x4\<rbrace> delete_objects x1 page_bits \<lbrace>?Q27 x1 x2 x3 x4\<rbrace>
 4. \<And>s. \<lbrakk>authorised_asid_control_inv aag aci; True\<rbrakk> \<Longrightarrow> \<forall>x xa xb xc. aci = MakePool x xa xb xc \<longrightarrow> ?P'27 x xa xb xc s \<and> ?P''27 x xa xb xc s proof (prove)
goal (4 subgoals):
 1. \<And>x1 x2 x3 x4 rv. \<lbrakk>authorised_asid_control_inv aag aci; aci = MakePool x1 x2 x3 x4\<rbrakk> \<Longrightarrow> reads_respects aag l (?Q27 x1 x2 x3 x4 rv) (do do _ <- do _ <- do pcap <- get_cap x3;
set_cap (max_free_index_update pcap) x3
od;
retype_region x1 1 0 (ArchObject ASIDPoolObj) False
od;
cap_insert (ArchObjectCap $ ASIDPoolCap x1 x4) x3 x2
od;
r <- assert (x4 && mask local.asid_low_bits = 0);
x <- K_bind (do asid_table <- gets (arm_asid_table \<circ> arch_state);
asid_table' <- return (asid_table(asid_high_bits_of x4 \<mapsto> x1));
modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := asid_table'\<rparr>\<rparr>)
od) r;
return ()
od)
 2. \<And>x1 x2 x3 x4. \<lbrakk>authorised_asid_control_inv aag aci; aci = MakePool x1 x2 x3 x4\<rbrakk> \<Longrightarrow> reads_respects aag l (?P'27 x1 x2 x3 x4) (delete_objects x1 page_bits)
 3. \<And>x1 x2 x3 x4. \<lbrakk>authorised_asid_control_inv aag aci; aci = MakePool x1 x2 x3 x4\<rbrakk> \<Longrightarrow> \<lbrace>?P''27 x1 x2 x3 x4\<rbrace> delete_objects x1 page_bits \<lbrace>?Q27 x1 x2 x3 x4\<rbrace>
 4. \<And>s. \<lbrakk>authorised_asid_control_inv aag aci; True\<rbrakk> \<Longrightarrow> \<forall>x xa xb xc. aci = MakePool x xa xb xc \<longrightarrow> ?P'27 x xa xb xc s \<and> ?P''27 x xa xb xc s proof (prove)
goal (6 subgoals):
 1. \<And>x1 x2 x3 x4 rv rva. \<lbrakk>authorised_asid_control_inv aag aci; aci = MakePool x1 x2 x3 x4\<rbrakk> \<Longrightarrow> reads_respects aag l (?Q33 x1 x2 x3 x4 rv rva) (K_bind (do r <- assert (x4 && mask local.asid_low_bits = 0);
x <- K_bind (do asid_table <- gets (arm_asid_table \<circ> arch_state);
asid_table' <- return (asid_table(asid_high_bits_of x4 \<mapsto> x1));
modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := asid_table'\<rparr>\<rparr>)
od) r;
return ()
od) rva)
 2. \<And>x1 x2 x3 x4 rv. \<lbrakk>authorised_asid_control_inv aag aci; aci = MakePool x1 x2 x3 x4\<rbrakk> \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (do _ <- do _ <- do pcap <- get_cap x3;
set_cap (max_free_index_update pcap) x3
od;
retype_region x1 1 0 (ArchObject ASIDPoolObj) False
od;
cap_insert (ArchObjectCap $ ASIDPoolCap x1 x4) x3 x2
od)
 3. \<And>x1 x2 x3 x4 rv. \<lbrakk>authorised_asid_control_inv aag aci; aci = MakePool x1 x2 x3 x4\<rbrakk> \<Longrightarrow> \<lbrace>?P''33 x1 x2 x3 x4 rv\<rbrace> do _ <- do _ <- do pcap <- get_cap x3;
set_cap (max_free_index_update pcap) x3
od;
retype_region x1 1 0 (ArchObject ASIDPoolObj) False
od;
cap_insert (ArchObjectCap $ ASIDPoolCap x1 x4) x3 x2
od \<lbrace>?Q33 x1 x2 x3 x4 rv\<rbrace>
 4. \<And>x1 x2 x3 x4. \<lbrakk>authorised_asid_control_inv aag aci; aci = MakePool x1 x2 x3 x4\<rbrakk> \<Longrightarrow> reads_respects aag l (?P'27 x1 x2 x3 x4) (delete_objects x1 page_bits)
 5. \<And>x1 x2 x3 x4. \<lbrakk>authorised_asid_control_inv aag aci; aci = MakePool x1 x2 x3 x4\<rbrakk> \<Longrightarrow> \<lbrace>?P''27 x1 x2 x3 x4\<rbrace> delete_objects x1 page_bits \<lbrace>\<lambda>rv s. True \<and> ?P''33 x1 x2 x3 x4 rv s\<rbrace>
 6. \<And>s. \<lbrakk>authorised_asid_control_inv aag aci; True\<rbrakk> \<Longrightarrow> \<forall>x xa xb xc. aci = MakePool x xa xb xc \<longrightarrow> ?P'27 x xa xb xc s \<and> ?P''27 x xa xb xc s proof (prove)
goal (6 subgoals):
 1. \<And>x1 x2 x3 x4 rv rva. \<lbrakk>authorised_asid_control_inv aag aci; aci = MakePool x1 x2 x3 x4\<rbrakk> \<Longrightarrow> reads_respects aag l (?Q33 x1 x2 x3 x4 rv rva) (do r <- assert (x4 && mask local.asid_low_bits = 0);
x <- K_bind (do asid_table <- gets (arm_asid_table \<circ> arch_state);
asid_table' <- return (asid_table(asid_high_bits_of x4 \<mapsto> x1));
modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := asid_table'\<rparr>\<rparr>)
od) r;
return ()
od)
 2. \<And>x1 x2 x3 x4 rv. \<lbrakk>authorised_asid_control_inv aag aci; aci = MakePool x1 x2 x3 x4\<rbrakk> \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (do _ <- do _ <- do pcap <- get_cap x3;
set_cap (max_free_index_update pcap) x3
od;
retype_region x1 1 0 (ArchObject ASIDPoolObj) False
od;
cap_insert (ArchObjectCap $ ASIDPoolCap x1 x4) x3 x2
od)
 3. \<And>x1 x2 x3 x4 rv. \<lbrakk>authorised_asid_control_inv aag aci; aci = MakePool x1 x2 x3 x4\<rbrakk> \<Longrightarrow> \<lbrace>?P''33 x1 x2 x3 x4 rv\<rbrace> do _ <- do _ <- do pcap <- get_cap x3;
set_cap (max_free_index_update pcap) x3
od;
retype_region x1 1 0 (ArchObject ASIDPoolObj) False
od;
cap_insert (ArchObjectCap $ ASIDPoolCap x1 x4) x3 x2
od \<lbrace>?Q33 x1 x2 x3 x4 rv\<rbrace>
 4. \<And>x1 x2 x3 x4. \<lbrakk>authorised_asid_control_inv aag aci; aci = MakePool x1 x2 x3 x4\<rbrakk> \<Longrightarrow> reads_respects aag l (?P'27 x1 x2 x3 x4) (delete_objects x1 page_bits)
 5. \<And>x1 x2 x3 x4. \<lbrakk>authorised_asid_control_inv aag aci; aci = MakePool x1 x2 x3 x4\<rbrakk> \<Longrightarrow> \<lbrace>?P''27 x1 x2 x3 x4\<rbrace> delete_objects x1 page_bits \<lbrace>\<lambda>rv s. True \<and> ?P''33 x1 x2 x3 x4 rv s\<rbrace>
 6. \<And>s. \<lbrakk>authorised_asid_control_inv aag aci; True\<rbrakk> \<Longrightarrow> \<forall>x xa xb xc. aci = MakePool x xa xb xc \<longrightarrow> ?P'27 x xa xb xc s \<and> ?P''27 x xa xb xc s proof (prove)
goal (8 subgoals):
 1. \<And>x1 x2 x3 x4 rv rva rvb. \<lbrakk>authorised_asid_control_inv aag aci; aci = MakePool x1 x2 x3 x4\<rbrakk> \<Longrightarrow> reads_respects aag l (?Q37 x1 x2 x3 x4 rv rva rvb) (do x <- K_bind (do asid_table <- gets (arm_asid_table \<circ> arch_state);
asid_table' <- return (asid_table(asid_high_bits_of x4 \<mapsto> x1));
modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := asid_table'\<rparr>\<rparr>)
od) rvb;
return ()
od)
 2. \<And>x1 x2 x3 x4 rv rva. \<lbrakk>authorised_asid_control_inv aag aci; aci = MakePool x1 x2 x3 x4\<rbrakk> \<Longrightarrow> reads_respects aag l (?P'37 x1 x2 x3 x4 rv rva) (assert (x4 && mask local.asid_low_bits = 0))
 3. \<And>x1 x2 x3 x4 rv rva. \<lbrakk>authorised_asid_control_inv aag aci; aci = MakePool x1 x2 x3 x4\<rbrakk> \<Longrightarrow> \<lbrace>?P''37 x1 x2 x3 x4 rv rva\<rbrace> assert (x4 && mask local.asid_low_bits = 0) \<lbrace>?Q37 x1 x2 x3 x4 rv rva\<rbrace>
 4. \<And>x1 x2 x3 x4 rv. \<lbrakk>authorised_asid_control_inv aag aci; aci = MakePool x1 x2 x3 x4\<rbrakk> \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (do _ <- do _ <- do pcap <- get_cap x3;
set_cap (max_free_index_update pcap) x3
od;
retype_region x1 1 0 (ArchObject ASIDPoolObj) False
od;
cap_insert (ArchObjectCap $ ASIDPoolCap x1 x4) x3 x2
od)
 5. \<And>x1 x2 x3 x4 rv. \<lbrakk>authorised_asid_control_inv aag aci; aci = MakePool x1 x2 x3 x4\<rbrakk> \<Longrightarrow> \<lbrace>?P''33 x1 x2 x3 x4 rv\<rbrace> do _ <- do _ <- do pcap <- get_cap x3;
set_cap (max_free_index_update pcap) x3
od;
retype_region x1 1 0 (ArchObject ASIDPoolObj) False
od;
cap_insert (ArchObjectCap $ ASIDPoolCap x1 x4) x3 x2
od \<lbrace>\<lambda>rva s. ?P'37 x1 x2 x3 x4 rv rva s \<and> ?P''37 x1 x2 x3 x4 rv rva s\<rbrace>
 6. \<And>x1 x2 x3 x4. \<lbrakk>authorised_asid_control_inv aag aci; aci = MakePool x1 x2 x3 x4\<rbrakk> \<Longrightarrow> reads_respects aag l (?P'27 x1 x2 x3 x4) (delete_objects x1 page_bits)
 7. \<And>x1 x2 x3 x4. \<lbrakk>authorised_asid_control_inv aag aci; aci = MakePool x1 x2 x3 x4\<rbrakk> \<Longrightarrow> \<lbrace>?P''27 x1 x2 x3 x4\<rbrace> delete_objects x1 page_bits \<lbrace>\<lambda>rv s. True \<and> ?P''33 x1 x2 x3 x4 rv s\<rbrace>
 8. \<And>s. \<lbrakk>authorised_asid_control_inv aag aci; True\<rbrakk> \<Longrightarrow> \<forall>x xa xb xc. aci = MakePool x xa xb xc \<longrightarrow> ?P'27 x xa xb xc s \<and> ?P''27 x xa xb xc s proof (prove)
goal (10 subgoals):
 1. \<And>x1 x2 x3 x4 rv rva rvb rvc. \<lbrakk>authorised_asid_control_inv aag aci; aci = MakePool x1 x2 x3 x4\<rbrakk> \<Longrightarrow> reads_respects aag l (?Q41 x1 x2 x3 x4 rv rva rvb rvc) (return ())
 2. \<And>x1 x2 x3 x4 rv rva rvb. \<lbrakk>authorised_asid_control_inv aag aci; aci = MakePool x1 x2 x3 x4\<rbrakk> \<Longrightarrow> reads_respects aag l (?P'41 x1 x2 x3 x4 rv rva rvb) (K_bind (do asid_table <- gets (arm_asid_table \<circ> arch_state);
asid_table' <- return (asid_table(asid_high_bits_of x4 \<mapsto> x1));
modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := asid_table'\<rparr>\<rparr>)
od) rvb)
 3. \<And>x1 x2 x3 x4 rv rva rvb. \<lbrakk>authorised_asid_control_inv aag aci; aci = MakePool x1 x2 x3 x4\<rbrakk> \<Longrightarrow> \<lbrace>?P''41 x1 x2 x3 x4 rv rva rvb\<rbrace> K_bind (do asid_table <- gets (arm_asid_table \<circ> arch_state);
asid_table' <- return (asid_table(asid_high_bits_of x4 \<mapsto> x1));
modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := asid_table'\<rparr>\<rparr>)
od) rvb \<lbrace>?Q41 x1 x2 x3 x4 rv rva rvb\<rbrace>
 4. \<And>x1 x2 x3 x4 rv rva. \<lbrakk>authorised_asid_control_inv aag aci; aci = MakePool x1 x2 x3 x4\<rbrakk> \<Longrightarrow> reads_respects aag l (?P'37 x1 x2 x3 x4 rv rva) (assert (x4 && mask local.asid_low_bits = 0))
 5. \<And>x1 x2 x3 x4 rv rva. \<lbrakk>authorised_asid_control_inv aag aci; aci = MakePool x1 x2 x3 x4\<rbrakk> \<Longrightarrow> \<lbrace>?P''37 x1 x2 x3 x4 rv rva\<rbrace> assert (x4 && mask local.asid_low_bits = 0) \<lbrace>\<lambda>rvb s. ?P'41 x1 x2 x3 x4 rv rva rvb s \<and> ?P''41 x1 x2 x3 x4 rv rva rvb s\<rbrace>
 6. \<And>x1 x2 x3 x4 rv. \<lbrakk>authorised_asid_control_inv aag aci; aci = MakePool x1 x2 x3 x4\<rbrakk> \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (do _ <- do _ <- do pcap <- get_cap x3;
set_cap (max_free_index_update pcap) x3
od;
retype_region x1 1 0 (ArchObject ASIDPoolObj) False
od;
cap_insert (ArchObjectCap $ ASIDPoolCap x1 x4) x3 x2
od)
 7. \<And>x1 x2 x3 x4 rv. \<lbrakk>authorised_asid_control_inv aag aci; aci = MakePool x1 x2 x3 x4\<rbrakk> \<Longrightarrow> \<lbrace>?P''33 x1 x2 x3 x4 rv\<rbrace> do _ <- do _ <- do pcap <- get_cap x3;
set_cap (max_free_index_update pcap) x3
od;
retype_region x1 1 0 (ArchObject ASIDPoolObj) False
od;
cap_insert (ArchObjectCap $ ASIDPoolCap x1 x4) x3 x2
od \<lbrace>\<lambda>rva s. ?P'37 x1 x2 x3 x4 rv rva s \<and> ?P''37 x1 x2 x3 x4 rv rva s\<rbrace>
 8. \<And>x1 x2 x3 x4. \<lbrakk>authorised_asid_control_inv aag aci; aci = MakePool x1 x2 x3 x4\<rbrakk> \<Longrightarrow> reads_respects aag l (?P'27 x1 x2 x3 x4) (delete_objects x1 page_bits)
 9. \<And>x1 x2 x3 x4. \<lbrakk>authorised_asid_control_inv aag aci; aci = MakePool x1 x2 x3 x4\<rbrakk> \<Longrightarrow> \<lbrace>?P''27 x1 x2 x3 x4\<rbrace> delete_objects x1 page_bits \<lbrace>\<lambda>rv s. True \<and> ?P''33 x1 x2 x3 x4 rv s\<rbrace>
 10. \<And>s. \<lbrakk>authorised_asid_control_inv aag aci; True\<rbrakk> \<Longrightarrow> \<forall>x xa xb xc. aci = MakePool x xa xb xc \<longrightarrow> ?P'27 x xa xb xc s \<and> ?P''27 x xa xb xc s proof (prove)
goal (9 subgoals):
 1. \<And>x1 x2 x3 x4 rv rva rvb. \<lbrakk>authorised_asid_control_inv aag aci; aci = MakePool x1 x2 x3 x4\<rbrakk> \<Longrightarrow> reads_respects aag l (?P'41 x1 x2 x3 x4 rv rva rvb) (K_bind (do asid_table <- gets (arm_asid_table \<circ> arch_state);
asid_table' <- return (asid_table(asid_high_bits_of x4 \<mapsto> x1));
modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := asid_table'\<rparr>\<rparr>)
od) rvb)
 2. \<And>x1 x2 x3 x4 rv rva rvb. \<lbrakk>authorised_asid_control_inv aag aci; aci = MakePool x1 x2 x3 x4\<rbrakk> \<Longrightarrow> \<lbrace>?P''41 x1 x2 x3 x4 rv rva rvb\<rbrace> K_bind (do asid_table <- gets (arm_asid_table \<circ> arch_state);
asid_table' <- return (asid_table(asid_high_bits_of x4 \<mapsto> x1));
modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := asid_table'\<rparr>\<rparr>)
od) rvb \<lbrace>\<lambda>rvc _. True\<rbrace>
 3. \<And>x1 x2 x3 x4 rv rva. \<lbrakk>authorised_asid_control_inv aag aci; aci = MakePool x1 x2 x3 x4\<rbrakk> \<Longrightarrow> reads_respects aag l (?P'37 x1 x2 x3 x4 rv rva) (assert (x4 && mask local.asid_low_bits = 0))
 4. \<And>x1 x2 x3 x4 rv rva. \<lbrakk>authorised_asid_control_inv aag aci; aci = MakePool x1 x2 x3 x4\<rbrakk> \<Longrightarrow> \<lbrace>?P''37 x1 x2 x3 x4 rv rva\<rbrace> assert (x4 && mask local.asid_low_bits = 0) \<lbrace>\<lambda>rvb s. ?P'41 x1 x2 x3 x4 rv rva rvb s \<and> ?P''41 x1 x2 x3 x4 rv rva rvb s\<rbrace>
 5. \<And>x1 x2 x3 x4 rv. \<lbrakk>authorised_asid_control_inv aag aci; aci = MakePool x1 x2 x3 x4\<rbrakk> \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (do _ <- do _ <- do pcap <- get_cap x3;
set_cap (max_free_index_update pcap) x3
od;
retype_region x1 1 0 (ArchObject ASIDPoolObj) False
od;
cap_insert (ArchObjectCap $ ASIDPoolCap x1 x4) x3 x2
od)
 6. \<And>x1 x2 x3 x4 rv. \<lbrakk>authorised_asid_control_inv aag aci; aci = MakePool x1 x2 x3 x4\<rbrakk> \<Longrightarrow> \<lbrace>?P''33 x1 x2 x3 x4 rv\<rbrace> do _ <- do _ <- do pcap <- get_cap x3;
set_cap (max_free_index_update pcap) x3
od;
retype_region x1 1 0 (ArchObject ASIDPoolObj) False
od;
cap_insert (ArchObjectCap $ ASIDPoolCap x1 x4) x3 x2
od \<lbrace>\<lambda>rva s. ?P'37 x1 x2 x3 x4 rv rva s \<and> ?P''37 x1 x2 x3 x4 rv rva s\<rbrace>
 7. \<And>x1 x2 x3 x4. \<lbrakk>authorised_asid_control_inv aag aci; aci = MakePool x1 x2 x3 x4\<rbrakk> \<Longrightarrow> reads_respects aag l (?P'27 x1 x2 x3 x4) (delete_objects x1 page_bits)
 8. \<And>x1 x2 x3 x4. \<lbrakk>authorised_asid_control_inv aag aci; aci = MakePool x1 x2 x3 x4\<rbrakk> \<Longrightarrow> \<lbrace>?P''27 x1 x2 x3 x4\<rbrace> delete_objects x1 page_bits \<lbrace>\<lambda>rv s. True \<and> ?P''33 x1 x2 x3 x4 rv s\<rbrace>
 9. \<And>s. \<lbrakk>authorised_asid_control_inv aag aci; True\<rbrakk> \<Longrightarrow> \<forall>x xa xb xc. aci = MakePool x xa xb xc \<longrightarrow> ?P'27 x xa xb xc s \<and> ?P''27 x xa xb xc s proof (prove)
goal (9 subgoals):
 1. \<And>x1 x2 x3 x4 rv rva rvb. \<lbrakk>authorised_asid_control_inv aag aci; aci = MakePool x1 x2 x3 x4\<rbrakk> \<Longrightarrow> reads_respects aag l (?P'41 x1 x2 x3 x4 rv rva rvb) (do asid_table <- gets (arm_asid_table \<circ> arch_state);
asid_table' <- return (asid_table(asid_high_bits_of x4 \<mapsto> x1));
modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := asid_table'\<rparr>\<rparr>)
od)
 2. \<And>x1 x2 x3 x4 rv rva rvb. \<lbrakk>authorised_asid_control_inv aag aci; aci = MakePool x1 x2 x3 x4\<rbrakk> \<Longrightarrow> \<lbrace>?P''41 x1 x2 x3 x4 rv rva rvb\<rbrace> K_bind (do asid_table <- gets (arm_asid_table \<circ> arch_state);
asid_table' <- return (asid_table(asid_high_bits_of x4 \<mapsto> x1));
modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := asid_table'\<rparr>\<rparr>)
od) rvb \<lbrace>\<lambda>rvc _. True\<rbrace>
 3. \<And>x1 x2 x3 x4 rv rva. \<lbrakk>authorised_asid_control_inv aag aci; aci = MakePool x1 x2 x3 x4\<rbrakk> \<Longrightarrow> reads_respects aag l (?P'37 x1 x2 x3 x4 rv rva) (assert (x4 && mask local.asid_low_bits = 0))
 4. \<And>x1 x2 x3 x4 rv rva. \<lbrakk>authorised_asid_control_inv aag aci; aci = MakePool x1 x2 x3 x4\<rbrakk> \<Longrightarrow> \<lbrace>?P''37 x1 x2 x3 x4 rv rva\<rbrace> assert (x4 && mask local.asid_low_bits = 0) \<lbrace>\<lambda>rvb s. ?P'41 x1 x2 x3 x4 rv rva rvb s \<and> ?P''41 x1 x2 x3 x4 rv rva rvb s\<rbrace>
 5. \<And>x1 x2 x3 x4 rv. \<lbrakk>authorised_asid_control_inv aag aci; aci = MakePool x1 x2 x3 x4\<rbrakk> \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (do _ <- do _ <- do pcap <- get_cap x3;
set_cap (max_free_index_update pcap) x3
od;
retype_region x1 1 0 (ArchObject ASIDPoolObj) False
od;
cap_insert (ArchObjectCap $ ASIDPoolCap x1 x4) x3 x2
od)
 6. \<And>x1 x2 x3 x4 rv. \<lbrakk>authorised_asid_control_inv aag aci; aci = MakePool x1 x2 x3 x4\<rbrakk> \<Longrightarrow> \<lbrace>?P''33 x1 x2 x3 x4 rv\<rbrace> do _ <- do _ <- do pcap <- get_cap x3;
set_cap (max_free_index_update pcap) x3
od;
retype_region x1 1 0 (ArchObject ASIDPoolObj) False
od;
cap_insert (ArchObjectCap $ ASIDPoolCap x1 x4) x3 x2
od \<lbrace>\<lambda>rva s. ?P'37 x1 x2 x3 x4 rv rva s \<and> ?P''37 x1 x2 x3 x4 rv rva s\<rbrace>
 7. \<And>x1 x2 x3 x4. \<lbrakk>authorised_asid_control_inv aag aci; aci = MakePool x1 x2 x3 x4\<rbrakk> \<Longrightarrow> reads_respects aag l (?P'27 x1 x2 x3 x4) (delete_objects x1 page_bits)
 8. \<And>x1 x2 x3 x4. \<lbrakk>authorised_asid_control_inv aag aci; aci = MakePool x1 x2 x3 x4\<rbrakk> \<Longrightarrow> \<lbrace>?P''27 x1 x2 x3 x4\<rbrace> delete_objects x1 page_bits \<lbrace>\<lambda>rv s. True \<and> ?P''33 x1 x2 x3 x4 rv s\<rbrace>
 9. \<And>s. \<lbrakk>authorised_asid_control_inv aag aci; True\<rbrakk> \<Longrightarrow> \<forall>x xa xb xc. aci = MakePool x xa xb xc \<longrightarrow> ?P'27 x xa xb xc s \<and> ?P''27 x xa xb xc s proof (prove)
goal (9 subgoals):
 1. \<And>x1 x2 x3 x4. \<lbrakk>authorised_asid_control_inv aag (MakePool x1 x2 x3 x4); aci = MakePool x1 x2 x3 x4\<rbrakk> \<Longrightarrow> reads_respects aag l (?P'41 x1 x2 x3 x4 () () ()) (do asid_table <- gets (arm_asid_table \<circ> arch_state);
modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := asid_table(asid_high_bits_of x4 \<mapsto> x1)\<rparr>\<rparr>)
od)
 2. \<And>x1 x2 x3 x4 rv rva rvb. \<lbrakk>authorised_asid_control_inv aag aci; aci = MakePool x1 x2 x3 x4\<rbrakk> \<Longrightarrow> \<lbrace>?P''41 x1 x2 x3 x4 rv rva rvb\<rbrace> K_bind (do asid_table <- gets (arm_asid_table \<circ> arch_state);
asid_table' <- return (asid_table(asid_high_bits_of x4 \<mapsto> x1));
modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := asid_table'\<rparr>\<rparr>)
od) rvb \<lbrace>\<lambda>rvc _. True\<rbrace>
 3. \<And>x1 x2 x3 x4 rv rva. \<lbrakk>authorised_asid_control_inv aag aci; aci = MakePool x1 x2 x3 x4\<rbrakk> \<Longrightarrow> reads_respects aag l (?P'37 x1 x2 x3 x4 rv rva) (assert (x4 && mask local.asid_low_bits = 0))
 4. \<And>x1 x2 x3 x4 rv rva. \<lbrakk>authorised_asid_control_inv aag aci; aci = MakePool x1 x2 x3 x4\<rbrakk> \<Longrightarrow> \<lbrace>?P''37 x1 x2 x3 x4 rv rva\<rbrace> assert (x4 && mask local.asid_low_bits = 0) \<lbrace>\<lambda>rvb s. ?P'41 x1 x2 x3 x4 rv rva rvb s \<and> ?P''41 x1 x2 x3 x4 rv rva rvb s\<rbrace>
 5. \<And>x1 x2 x3 x4 rv. \<lbrakk>authorised_asid_control_inv aag aci; aci = MakePool x1 x2 x3 x4\<rbrakk> \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (do _ <- do _ <- do pcap <- get_cap x3;
set_cap (max_free_index_update pcap) x3
od;
retype_region x1 1 0 (ArchObject ASIDPoolObj) False
od;
cap_insert (ArchObjectCap $ ASIDPoolCap x1 x4) x3 x2
od)
 6. \<And>x1 x2 x3 x4 rv. \<lbrakk>authorised_asid_control_inv aag aci; aci = MakePool x1 x2 x3 x4\<rbrakk> \<Longrightarrow> \<lbrace>?P''33 x1 x2 x3 x4 rv\<rbrace> do _ <- do _ <- do pcap <- get_cap x3;
set_cap (max_free_index_update pcap) x3
od;
retype_region x1 1 0 (ArchObject ASIDPoolObj) False
od;
cap_insert (ArchObjectCap $ ASIDPoolCap x1 x4) x3 x2
od \<lbrace>\<lambda>rva s. ?P'37 x1 x2 x3 x4 rv rva s \<and> ?P''37 x1 x2 x3 x4 rv rva s\<rbrace>
 7. \<And>x1 x2 x3 x4. \<lbrakk>authorised_asid_control_inv aag aci; aci = MakePool x1 x2 x3 x4\<rbrakk> \<Longrightarrow> reads_respects aag l (?P'27 x1 x2 x3 x4) (delete_objects x1 page_bits)
 8. \<And>x1 x2 x3 x4. \<lbrakk>authorised_asid_control_inv aag aci; aci = MakePool x1 x2 x3 x4\<rbrakk> \<Longrightarrow> \<lbrace>?P''27 x1 x2 x3 x4\<rbrace> delete_objects x1 page_bits \<lbrace>\<lambda>rv s. True \<and> ?P''33 x1 x2 x3 x4 rv s\<rbrace>
 9. \<And>s. \<lbrakk>authorised_asid_control_inv aag aci; True\<rbrakk> \<Longrightarrow> \<forall>x xa xb xc. aci = MakePool x xa xb xc \<longrightarrow> ?P'27 x xa xb xc s \<and> ?P''27 x xa xb xc s proof (prove)
goal (8 subgoals):
 1. \<And>x1 x2 x3 x4 rv rva rvb. \<lbrakk>authorised_asid_control_inv aag aci; aci = MakePool x1 x2 x3 x4\<rbrakk> \<Longrightarrow> \<lbrace>?P''41 x1 x2 x3 x4 rv rva rvb\<rbrace> K_bind (do asid_table <- gets (arm_asid_table \<circ> arch_state);
asid_table' <- return (asid_table(asid_high_bits_of x4 \<mapsto> x1));
modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := asid_table'\<rparr>\<rparr>)
od) rvb \<lbrace>\<lambda>rvc _. True\<rbrace>
 2. \<And>x1 x2 x3 x4 rv rva. \<lbrakk>authorised_asid_control_inv aag aci; aci = MakePool x1 x2 x3 x4\<rbrakk> \<Longrightarrow> reads_respects aag l (?P'37 x1 x2 x3 x4 rv rva) (assert (x4 && mask local.asid_low_bits = 0))
 3. \<And>x1 x2 x3 x4 rv rva. \<lbrakk>authorised_asid_control_inv aag aci; aci = MakePool x1 x2 x3 x4\<rbrakk> \<Longrightarrow> \<lbrace>?P''37 x1 x2 x3 x4 rv rva\<rbrace> assert (x4 && mask local.asid_low_bits = 0) \<lbrace>\<lambda>rvb s. K (is_subject aag x1) s \<and> ?P''41 x1 x2 x3 x4 rv rva rvb s\<rbrace>
 4. \<And>x1 x2 x3 x4 rv. \<lbrakk>authorised_asid_control_inv aag aci; aci = MakePool x1 x2 x3 x4\<rbrakk> \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (do _ <- do _ <- do pcap <- get_cap x3;
set_cap (max_free_index_update pcap) x3
od;
retype_region x1 1 0 (ArchObject ASIDPoolObj) False
od;
cap_insert (ArchObjectCap $ ASIDPoolCap x1 x4) x3 x2
od)
 5. \<And>x1 x2 x3 x4 rv. \<lbrakk>authorised_asid_control_inv aag aci; aci = MakePool x1 x2 x3 x4\<rbrakk> \<Longrightarrow> \<lbrace>?P''33 x1 x2 x3 x4 rv\<rbrace> do _ <- do _ <- do pcap <- get_cap x3;
set_cap (max_free_index_update pcap) x3
od;
retype_region x1 1 0 (ArchObject ASIDPoolObj) False
od;
cap_insert (ArchObjectCap $ ASIDPoolCap x1 x4) x3 x2
od \<lbrace>\<lambda>rva s. ?P'37 x1 x2 x3 x4 rv rva s \<and> ?P''37 x1 x2 x3 x4 rv rva s\<rbrace>
 6. \<And>x1 x2 x3 x4. \<lbrakk>authorised_asid_control_inv aag aci; aci = MakePool x1 x2 x3 x4\<rbrakk> \<Longrightarrow> reads_respects aag l (?P'27 x1 x2 x3 x4) (delete_objects x1 page_bits)
 7. \<And>x1 x2 x3 x4. \<lbrakk>authorised_asid_control_inv aag aci; aci = MakePool x1 x2 x3 x4\<rbrakk> \<Longrightarrow> \<lbrace>?P''27 x1 x2 x3 x4\<rbrace> delete_objects x1 page_bits \<lbrace>\<lambda>rv s. True \<and> ?P''33 x1 x2 x3 x4 rv s\<rbrace>
 8. \<And>s. \<lbrakk>authorised_asid_control_inv aag aci; True\<rbrakk> \<Longrightarrow> \<forall>x xa xb xc. aci = MakePool x xa xb xc \<longrightarrow> ?P'27 x xa xb xc s \<and> ?P''27 x xa xb xc s proof (prove)
goal (1 subgoal):
 1. case aci of MakePool frame slot parent base \<Rightarrow> is_subject aag (fst slot) \<and> is_aligned frame pageBits \<and> (\<forall>asid. is_subject_asid aag asid) \<and> is_subject aag (fst parent) \<and> (\<forall>x\<in>{frame..frame + 2 ^ pageBits - 1}. is_subject aag x) \<Longrightarrow> \<forall>x. (\<exists>a b aa ba xa. aci = MakePool x (a, b) (aa, ba) xa) \<longrightarrow> is_subject aag x proof (prove)
goal:
No subgoals!