theory VSpace_C

lemma rf_sr_armKSASIDTable_rel':
  "\<lbrakk> (s, s') \<in> rf_sr; valid_arch_state' s \<rbrakk>
    \<Longrightarrow> index (armKSHWASIDTable_' (globals s')) (unat x) =
         option_to_0 (armKSHWASIDTable (ksArchState s) x)
            \<and> ((option_to_0 (armKSHWASIDTable (ksArchState s) x) = 0)
                    = (armKSHWASIDTable (ksArchState s) x = None))" apply (rule conjI) apply (drule rf_sr_armKSASIDTable_rel) apply (clarsimp simp: array_relation_def) apply (rule sym, drule spec, erule mp) apply (rule order_trans, rule word_n1_ge) apply simp apply (clarsimp simp: option_to_0_def split: option.splits) apply (clarsimp simp: valid_arch_state'_def valid_asid_map'_def) apply (drule (1) is_inv_SomeD) apply (drule subsetD, fastforce) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> rf_sr; valid_arch_state' s\<rbrakk> \<Longrightarrow> armKSHWASIDTable_' (globals s').[unat x] = option_to_0 (armKSHWASIDTable (ksArchState s) x) \<and> (option_to_0 (armKSHWASIDTable (ksArchState s) x) = 0) = (armKSHWASIDTable (ksArchState s) x = None) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(s, s') \<in> rf_sr; valid_arch_state' s\<rbrakk> \<Longrightarrow> armKSHWASIDTable_' (globals s').[unat x] = option_to_0 (armKSHWASIDTable (ksArchState s) x)
 2. \<lbrakk>(s, s') \<in> rf_sr; valid_arch_state' s\<rbrakk> \<Longrightarrow> (option_to_0 (armKSHWASIDTable (ksArchState s) x) = 0) = (armKSHWASIDTable (ksArchState s) x = None) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_arch_state' s; array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState s)) (armKSHWASIDTable_' (globals s'))\<rbrakk> \<Longrightarrow> armKSHWASIDTable_' (globals s').[unat x] = option_to_0 (armKSHWASIDTable (ksArchState s) x)
 2. \<lbrakk>(s, s') \<in> rf_sr; valid_arch_state' s\<rbrakk> \<Longrightarrow> (option_to_0 (armKSHWASIDTable (ksArchState s) x) = 0) = (armKSHWASIDTable (ksArchState s) x = None) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_arch_state' s; \<forall>i\<le>0xFF. option_to_0 (armKSHWASIDTable (ksArchState s) i) = armKSHWASIDTable_' (globals s').[unat i]\<rbrakk> \<Longrightarrow> armKSHWASIDTable_' (globals s').[unat x] = option_to_0 (armKSHWASIDTable (ksArchState s) x)
 2. \<lbrakk>(s, s') \<in> rf_sr; valid_arch_state' s\<rbrakk> \<Longrightarrow> (option_to_0 (armKSHWASIDTable (ksArchState s) x) = 0) = (armKSHWASIDTable (ksArchState s) x = None) proof (prove)
goal (2 subgoals):
 1. valid_arch_state' s \<Longrightarrow> x \<le> 0xFF
 2. \<lbrakk>(s, s') \<in> rf_sr; valid_arch_state' s\<rbrakk> \<Longrightarrow> (option_to_0 (armKSHWASIDTable (ksArchState s) x) = 0) = (armKSHWASIDTable (ksArchState s) x = None) proof (prove)
goal (2 subgoals):
 1. valid_arch_state' s \<Longrightarrow> - 1 \<le> 0xFF
 2. \<lbrakk>(s, s') \<in> rf_sr; valid_arch_state' s\<rbrakk> \<Longrightarrow> (option_to_0 (armKSHWASIDTable (ksArchState s) x) = 0) = (armKSHWASIDTable (ksArchState s) x = None) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> rf_sr; valid_arch_state' s\<rbrakk> \<Longrightarrow> (option_to_0 (armKSHWASIDTable (ksArchState s) x) = 0) = (armKSHWASIDTable (ksArchState s) x = None) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> rf_sr; valid_arch_state' s; armKSHWASIDTable (ksArchState s) x = Some 0\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> rf_sr; armKSHWASIDTable (ksArchState s) x = Some 0; valid_asid_table' (armKSASIDTable (ksArchState s)) s; page_directory_at' (armKSGlobalPD (ksArchState s)) s; valid_global_pts' (armKSGlobalPTs (ksArchState s)) s; is_inv (armKSHWASIDTable (ksArchState s)) (map_option fst \<circ> armKSASIDMap (ksArchState s)); inj_on (map_option snd \<circ> armKSASIDMap (ksArchState s)) (dom (armKSASIDMap (ksArchState s))); dom (armKSASIDMap (ksArchState s)) \<subseteq> {0..mask local.asid_bits} - {0}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> rf_sr; valid_asid_table' (armKSASIDTable (ksArchState s)) s; page_directory_at' (armKSGlobalPD (ksArchState s)) s; valid_global_pts' (armKSGlobalPTs (ksArchState s)) s; is_inv (armKSHWASIDTable (ksArchState s)) (map_option fst \<circ> armKSASIDMap (ksArchState s)); inj_on (map_option snd \<circ> armKSASIDMap (ksArchState s)) (dom (armKSASIDMap (ksArchState s))); dom (armKSASIDMap (ksArchState s)) \<subseteq> {0..mask local.asid_bits} - {0}; (map_option fst \<circ> armKSASIDMap (ksArchState s)) 0 = Some x\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> rf_sr; valid_asid_table' (armKSASIDTable (ksArchState s)) s; page_directory_at' (armKSGlobalPD (ksArchState s)) s; valid_global_pts' (armKSGlobalPTs (ksArchState s)) s; is_inv (armKSHWASIDTable (ksArchState s)) (map_option fst \<circ> armKSASIDMap (ksArchState s)); inj_on (map_option snd \<circ> armKSASIDMap (ksArchState s)) (dom (armKSASIDMap (ksArchState s))); (map_option fst \<circ> armKSASIDMap (ksArchState s)) 0 = Some x; 0 \<in> {0..mask local.asid_bits} - {0}\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!