theory VSpace_C

lemma getKSASIDTable_ccorres_stuff:
  "\<lbrakk> invs' \<sigma>; (\<sigma>, x) \<in> rf_sr; idx' = unat idx;
             idx < 2 ^ asid_high_bits \<rbrakk>
     \<Longrightarrow> case armKSASIDTable (ksArchState \<sigma>)
                idx of
        None \<Rightarrow>
            index (armKSASIDTable_' (globals x))
                idx' =
               NULL
             | Some v \<Rightarrow>
                 index (armKSASIDTable_' (globals x))
                  idx' = Ptr v \<and>
                 index (armKSASIDTable_' (globals x))
                  idx' \<noteq> NULL" apply (drule rf_asidTable [where idx=idx]) apply fastforce apply (simp add: mask_def) apply (simp add: word_le_minus_one_leq) apply (clarsimp split: option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs' \<sigma>; (\<sigma>, x) \<in> rf_sr; idx' = unat idx; idx < 2 ^ local.asid_high_bits\<rbrakk> \<Longrightarrow> case armKSASIDTable (ksArchState \<sigma>) idx of None \<Rightarrow> armKSASIDTable_' (globals x).[idx'] = NULL | Some v \<Rightarrow> armKSASIDTable_' (globals x).[idx'] = ap_Ptr v \<and> armKSASIDTable_' (globals x).[idx'] \<noteq> NULL proof (prove)
goal (3 subgoals):
 1. \<lbrakk>invs' \<sigma>; idx' = unat idx; idx < 2 ^ local.asid_high_bits\<rbrakk> \<Longrightarrow> valid_arch_state' \<sigma>
 2. \<lbrakk>invs' \<sigma>; idx' = unat idx; idx < 2 ^ local.asid_high_bits\<rbrakk> \<Longrightarrow> idx \<le> mask local.asid_high_bits
 3. \<lbrakk>invs' \<sigma>; idx' = unat idx; idx < 2 ^ local.asid_high_bits; case armKSASIDTable (ksArchState \<sigma>) idx of None \<Rightarrow> armKSASIDTable_' (globals x).[unat idx] = NULL | Some v \<Rightarrow> armKSASIDTable_' (globals x).[unat idx] = ap_Ptr v \<and> armKSASIDTable_' (globals x).[unat idx] \<noteq> NULL\<rbrakk> \<Longrightarrow> case armKSASIDTable (ksArchState \<sigma>) idx of None \<Rightarrow> armKSASIDTable_' (globals x).[idx'] = NULL | Some v \<Rightarrow> armKSASIDTable_' (globals x).[idx'] = ap_Ptr v \<and> armKSASIDTable_' (globals x).[idx'] \<noteq> NULL proof (prove)
goal (2 subgoals):
 1. \<lbrakk>invs' \<sigma>; idx' = unat idx; idx < 2 ^ local.asid_high_bits\<rbrakk> \<Longrightarrow> idx \<le> mask local.asid_high_bits
 2. \<lbrakk>invs' \<sigma>; idx' = unat idx; idx < 2 ^ local.asid_high_bits; case armKSASIDTable (ksArchState \<sigma>) idx of None \<Rightarrow> armKSASIDTable_' (globals x).[unat idx] = NULL | Some v \<Rightarrow> armKSASIDTable_' (globals x).[unat idx] = ap_Ptr v \<and> armKSASIDTable_' (globals x).[unat idx] \<noteq> NULL\<rbrakk> \<Longrightarrow> case armKSASIDTable (ksArchState \<sigma>) idx of None \<Rightarrow> armKSASIDTable_' (globals x).[idx'] = NULL | Some v \<Rightarrow> armKSASIDTable_' (globals x).[idx'] = ap_Ptr v \<and> armKSASIDTable_' (globals x).[idx'] \<noteq> NULL proof (prove)
goal (2 subgoals):
 1. \<lbrakk>invs' \<sigma>; idx' = unat idx; idx < 2 ^ local.asid_high_bits\<rbrakk> \<Longrightarrow> idx \<le> 2 ^ local.asid_high_bits - 1
 2. \<lbrakk>invs' \<sigma>; idx' = unat idx; idx < 2 ^ local.asid_high_bits; case armKSASIDTable (ksArchState \<sigma>) idx of None \<Rightarrow> armKSASIDTable_' (globals x).[unat idx] = NULL | Some v \<Rightarrow> armKSASIDTable_' (globals x).[unat idx] = ap_Ptr v \<and> armKSASIDTable_' (globals x).[unat idx] \<noteq> NULL\<rbrakk> \<Longrightarrow> case armKSASIDTable (ksArchState \<sigma>) idx of None \<Rightarrow> armKSASIDTable_' (globals x).[idx'] = NULL | Some v \<Rightarrow> armKSASIDTable_' (globals x).[idx'] = ap_Ptr v \<and> armKSASIDTable_' (globals x).[idx'] \<noteq> NULL proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs' \<sigma>; idx' = unat idx; idx < 2 ^ local.asid_high_bits; case armKSASIDTable (ksArchState \<sigma>) idx of None \<Rightarrow> armKSASIDTable_' (globals x).[unat idx] = NULL | Some v \<Rightarrow> armKSASIDTable_' (globals x).[unat idx] = ap_Ptr v \<and> armKSASIDTable_' (globals x).[unat idx] \<noteq> NULL\<rbrakk> \<Longrightarrow> case armKSASIDTable (ksArchState \<sigma>) idx of None \<Rightarrow> armKSASIDTable_' (globals x).[idx'] = NULL | Some v \<Rightarrow> armKSASIDTable_' (globals x).[idx'] = ap_Ptr v \<and> armKSASIDTable_' (globals x).[idx'] \<noteq> NULL proof (prove)
goal:
No subgoals!