theory Eval_CAMKES_CDL

lemma helper_pcs_refined_policy__eval:
      (* policy specification, to be generated *)
  assumes policy_spec: "policy_spec \<subseteq> pasPolicy aag"
      and label_spec: "\<And>p l. label_spec p = Some l \<Longrightarrow> pasObjectAbs aag p = l"
      (* we don't handle the CDT for now, so these are unchanged *)
      and cdt_policy:
            "\<And>p slot p' slot'.
                 cdl_cdt s (p, slot) = Some (p', slot') \<Longrightarrow>
                 (pasObjectAbs aag p', Control, pasObjectAbs aag p) \<in> pasPolicy aag"
      and delete_derived_policy:
            "\<And>p slot p' slot'.
                 cdl_cdt s (p, slot) = Some (p', slot') \<Longrightarrow>
                 (pasObjectAbs aag p', DeleteDerived, pasObjectAbs aag p) \<in> pasPolicy aag"
      (* main specification, as nested set traversals *)
      and obj_policy:
            "\<forall>(p, p_obj) \<in> graph_of (cdl_objects s).
               (case label_spec p of
                  Some pl \<Rightarrow>
                     \<forall>(p_idx, cap) \<in> graph_of (object_slots p_obj).
                       \<forall>auth \<in> cdl_cap_auth_conferred cap.
                         \<forall>oref \<in> cdl_obj_refs cap.
                            (case label_spec oref of
                               Some orefl \<Rightarrow> generic_tag ''obj policy'' (p, cap, cdl_obj_refs cap)
                                                 ((pl, auth, orefl) \<in> policy_spec)
                             | _ \<Rightarrow> False)
                | _ \<Rightarrow> False)"
  shows "auth_graph_map (pasObjectAbs aag) (cdl_state_objs_to_policy s) \<subseteq> (pasPolicy aag)" apply (rule helper_pcs_refined_policyI) apply (blast intro: cdt_policy) apply (blast intro: delete_derived_policy) apply (fastforce simp: remove_generic_tag
                   intro: subsetD[OF policy_spec]
                   dest: label_spec obj_policy[simplified graph_of_def, simplified, rule_format]
                   split: option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. auth_graph_map (pasObjectAbs aag) (cdl_state_objs_to_policy s) \<subseteq> pasPolicy aag proof (prove)
goal (3 subgoals):
 1. \<And>p slot p' slot'. cdl_cdt s (p, slot) = Some (p', slot') \<Longrightarrow> (pasObjectAbs aag p', Control, pasObjectAbs aag p) \<in> pasPolicy aag
 2. \<And>p slot p' slot'. cdl_cdt s (p, slot) = Some (p', slot') \<Longrightarrow> (pasObjectAbs aag p', DeleteDerived, pasObjectAbs aag p) \<in> pasPolicy aag
 3. \<And>p p_obj p_idx cap auth oref. \<lbrakk>cdl_objects s p = Some p_obj; object_slots p_obj p_idx = Some cap; auth \<in> cdl_cap_auth_conferred cap; oref \<in> cdl_obj_refs cap\<rbrakk> \<Longrightarrow> (pasObjectAbs aag p, auth, pasObjectAbs aag oref) \<in> pasPolicy aag proof (prove)
goal (2 subgoals):
 1. \<And>p slot p' slot'. cdl_cdt s (p, slot) = Some (p', slot') \<Longrightarrow> (pasObjectAbs aag p', DeleteDerived, pasObjectAbs aag p) \<in> pasPolicy aag
 2. \<And>p p_obj p_idx cap auth oref. \<lbrakk>cdl_objects s p = Some p_obj; object_slots p_obj p_idx = Some cap; auth \<in> cdl_cap_auth_conferred cap; oref \<in> cdl_obj_refs cap\<rbrakk> \<Longrightarrow> (pasObjectAbs aag p, auth, pasObjectAbs aag oref) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>p p_obj p_idx cap auth oref. \<lbrakk>cdl_objects s p = Some p_obj; object_slots p_obj p_idx = Some cap; auth \<in> cdl_cap_auth_conferred cap; oref \<in> cdl_obj_refs cap\<rbrakk> \<Longrightarrow> (pasObjectAbs aag p, auth, pasObjectAbs aag oref) \<in> pasPolicy aag proof (prove)
goal:
No subgoals!