theory Eval_CAMKES_CDL

lemma cdl_state_asids_to_policy__eval:
  assumes policy_spec: "policy_spec \<subseteq> pasPolicy aag"
      and obj_label_spec: "\<And>p l. obj_label_spec p = Some l \<Longrightarrow> pasObjectAbs aag p = l"
      and asid_label_spec: "\<And>asid l. asid_label_spec (asid_high_bits_of asid) = Some l \<Longrightarrow>
                                      pasASIDAbs aag asid = l"
      and cap_asids:
            "\<forall>(p, p_obj) \<in> graph_of (cdl_objects s).
               (case obj_label_spec p of
                  Some pl \<Rightarrow>
                     \<forall>(p_idx, cap) \<in> graph_of (object_slots p_obj).
                       \<forall>asid \<in> asid_high_bits_of ` cdl_cap_asid' cap.
                          (case asid_label_spec asid of
                               Some asidl \<Rightarrow> generic_tag ''asid policy'' (p, cap, asid)
                                                 ((pl, Control, asidl) \<in> policy_spec)
                             | _ \<Rightarrow> False)
                | _ \<Rightarrow> False)"
      and asid_table_lookups:
            "\<forall>(asid_high, asid_pool_cap) \<in> graph_of (cdl_asid_table s).
               \<not>is_null_cap asid_pool_cap \<longrightarrow>
               (case asid_label_spec (of_nat asid_high) of
                  Some asidl \<Rightarrow>
                     (case cdl_objects s (cap_object asid_pool_cap) of
                        Some asid_pool \<Rightarrow>
                           \<forall>(asid_low, pd_cap) \<in> graph_of (object_slots asid_pool).
                             if is_null_cap pd_cap then True else
                                (case obj_label_spec (cap_object pd_cap) of
                                     Some pdl \<Rightarrow> generic_tag ''asid PD policy'' (asid_high, pd_cap)
                                                     ((asidl, Control, pdl) \<in> policy_spec)
                                   | _ \<Rightarrow> False)
                      | _ \<Rightarrow> False)
                     \<and> (case obj_label_spec (cap_object asid_pool_cap) of
                           Some asid_pool_l \<Rightarrow>
                             generic_tag ''asid pool policy'' (asid_high, asid_pool_cap)
                                 ((asid_pool_l, AAuth ASIDPoolMapsASID, asidl) \<in> policy_spec)
                         | _ \<Rightarrow> False)
                | _ \<Rightarrow> False)"

  shows "cdl_state_asids_to_policy aag s \<subseteq> pasPolicy aag" apply clarsimp apply (erule cdl_state_asids_to_policy_aux.cases) using cap_asids[unfolded remove_generic_tag] apply (fastforce simp: opt_cap_def slots_of_def graph_of_def
                     dest: obj_label_spec asid_label_spec
                     intro: subsetD[OF policy_spec]
                     split: option.splits) using asid_table_lookups[unfolded remove_generic_tag] apply (fastforce simp: opt_cap_def slots_of_def graph_of_def transform_asid_def
                    dest: obj_label_spec asid_label_spec
                    intro: subsetD[OF policy_spec]
                    split: option.splits) using asid_table_lookups[unfolded remove_generic_tag] apply (fastforce simp: opt_cap_def slots_of_def graph_of_def transform_asid_def
                   dest: obj_label_spec asid_label_spec
                   intro: subsetD[OF policy_spec]
                   split: option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cdl_state_asids_to_policy aag s \<subseteq> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>a aa b. (a, aa, b) \<in> cdl_state_asids_to_policy aag s \<Longrightarrow> (a, aa, b) \<in> pasPolicy aag proof (prove)
goal (3 subgoals):
 1. \<And>a aa b ptr cap asid. \<lbrakk>a = pasObjectAbs aag (fst ptr); aa = Control; b = pasASIDAbs aag asid; opt_cap ptr s = Some cap; asid \<in> cdl_cap_asid' cap\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy aag
 2. \<And>a aa b asid poolcap pdcap pdptr. \<lbrakk>a = pasASIDAbs aag asid; aa = Control; b = pasObjectAbs aag pdptr; cdl_asid_table s (fst (transform_asid asid)) = Some poolcap; \<not> is_null_cap poolcap; \<not> is_null_cap pdcap; pdptr = cap_object pdcap; opt_cap (cap_object poolcap, snd (transform_asid asid)) s = Some pdcap\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy aag
 3. \<And>a aa b asid poolcap. \<lbrakk>a = pasObjectAbs aag (cap_object poolcap); aa = AAuth ASIDPoolMapsASID; b = pasASIDAbs aag asid; cdl_asid_table s (fst (transform_asid asid)) = Some poolcap; \<not> is_null_cap poolcap; asid \<noteq> 0\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy aag proof (prove)
using this:
\<forall>(p, p_obj)\<in>graph_of (cdl_objects s). case obj_label_spec p of None \<Rightarrow> False | Some pl \<Rightarrow> \<forall>(p_idx, cap)\<in>graph_of (object_slots p_obj). \<forall>asid\<in>asid_high_bits_of ` cdl_cap_asid' cap. case asid_label_spec asid of None \<Rightarrow> False | Some asidl \<Rightarrow> (pl, Control, asidl) \<in> policy_spec

goal (3 subgoals):
 1. \<And>a aa b ptr cap asid. \<lbrakk>a = pasObjectAbs aag (fst ptr); aa = Control; b = pasASIDAbs aag asid; opt_cap ptr s = Some cap; asid \<in> cdl_cap_asid' cap\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy aag
 2. \<And>a aa b asid poolcap pdcap pdptr. \<lbrakk>a = pasASIDAbs aag asid; aa = Control; b = pasObjectAbs aag pdptr; cdl_asid_table s (fst (transform_asid asid)) = Some poolcap; \<not> is_null_cap poolcap; \<not> is_null_cap pdcap; pdptr = cap_object pdcap; opt_cap (cap_object poolcap, snd (transform_asid asid)) s = Some pdcap\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy aag
 3. \<And>a aa b asid poolcap. \<lbrakk>a = pasObjectAbs aag (cap_object poolcap); aa = AAuth ASIDPoolMapsASID; b = pasASIDAbs aag asid; cdl_asid_table s (fst (transform_asid asid)) = Some poolcap; \<not> is_null_cap poolcap; asid \<noteq> 0\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy aag proof (prove)
goal (2 subgoals):
 1. \<And>a aa b asid poolcap pdcap pdptr. \<lbrakk>a = pasASIDAbs aag asid; aa = Control; b = pasObjectAbs aag pdptr; cdl_asid_table s (fst (transform_asid asid)) = Some poolcap; \<not> is_null_cap poolcap; \<not> is_null_cap pdcap; pdptr = cap_object pdcap; opt_cap (cap_object poolcap, snd (transform_asid asid)) s = Some pdcap\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy aag
 2. \<And>a aa b asid poolcap. \<lbrakk>a = pasObjectAbs aag (cap_object poolcap); aa = AAuth ASIDPoolMapsASID; b = pasASIDAbs aag asid; cdl_asid_table s (fst (transform_asid asid)) = Some poolcap; \<not> is_null_cap poolcap; asid \<noteq> 0\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy aag proof (prove)
using this:
\<forall>(asid_high, asid_pool_cap)\<in>graph_of (cdl_asid_table s). \<not> is_null_cap asid_pool_cap \<longrightarrow> (case asid_label_spec (word_of_nat asid_high) of None \<Rightarrow> False | Some asidl \<Rightarrow> (case cdl_objects s (cap_object asid_pool_cap) of None \<Rightarrow> False | Some asid_pool \<Rightarrow> \<forall>(asid_low, pd_cap)\<in>graph_of (object_slots asid_pool). if is_null_cap pd_cap then True else case obj_label_spec (cap_object pd_cap) of None \<Rightarrow> False | Some pdl \<Rightarrow> (asidl, Control, pdl) \<in> policy_spec) \<and> (case obj_label_spec (cap_object asid_pool_cap) of None \<Rightarrow> False | Some asid_pool_l \<Rightarrow> (asid_pool_l, AAuth ASIDPoolMapsASID, asidl) \<in> policy_spec))

goal (2 subgoals):
 1. \<And>a aa b asid poolcap pdcap pdptr. \<lbrakk>a = pasASIDAbs aag asid; aa = Control; b = pasObjectAbs aag pdptr; cdl_asid_table s (fst (transform_asid asid)) = Some poolcap; \<not> is_null_cap poolcap; \<not> is_null_cap pdcap; pdptr = cap_object pdcap; opt_cap (cap_object poolcap, snd (transform_asid asid)) s = Some pdcap\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy aag
 2. \<And>a aa b asid poolcap. \<lbrakk>a = pasObjectAbs aag (cap_object poolcap); aa = AAuth ASIDPoolMapsASID; b = pasASIDAbs aag asid; cdl_asid_table s (fst (transform_asid asid)) = Some poolcap; \<not> is_null_cap poolcap; asid \<noteq> 0\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>a aa b asid poolcap. \<lbrakk>a = pasObjectAbs aag (cap_object poolcap); aa = AAuth ASIDPoolMapsASID; b = pasASIDAbs aag asid; cdl_asid_table s (fst (transform_asid asid)) = Some poolcap; \<not> is_null_cap poolcap; asid \<noteq> 0\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy aag proof (prove)
using this:
\<forall>(asid_high, asid_pool_cap)\<in>graph_of (cdl_asid_table s). \<not> is_null_cap asid_pool_cap \<longrightarrow> (case asid_label_spec (word_of_nat asid_high) of None \<Rightarrow> False | Some asidl \<Rightarrow> (case cdl_objects s (cap_object asid_pool_cap) of None \<Rightarrow> False | Some asid_pool \<Rightarrow> \<forall>(asid_low, pd_cap)\<in>graph_of (object_slots asid_pool). if is_null_cap pd_cap then True else case obj_label_spec (cap_object pd_cap) of None \<Rightarrow> False | Some pdl \<Rightarrow> (asidl, Control, pdl) \<in> policy_spec) \<and> (case obj_label_spec (cap_object asid_pool_cap) of None \<Rightarrow> False | Some asid_pool_l \<Rightarrow> (asid_pool_l, AAuth ASIDPoolMapsASID, asidl) \<in> policy_spec))

goal (1 subgoal):
 1. \<And>a aa b asid poolcap. \<lbrakk>a = pasObjectAbs aag (cap_object poolcap); aa = AAuth ASIDPoolMapsASID; b = pasASIDAbs aag asid; cdl_asid_table s (fst (transform_asid asid)) = Some poolcap; \<not> is_null_cap poolcap; asid \<noteq> 0\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy aag proof (prove)
goal:
No subgoals!