/*#
 *# Copyright 2018, Data61, CSIRO (ABN 41 687 119 230)
 *#
 *# SPDX-License-Identifier: BSD-2-Clause
 #*/

(* /*? macros.generated_file_notice() ?*/ *)

/*? macros.check_isabelle_outfile(
        '%s_CDL_Refine' % options.verification_base_name, outfile_name) ?*/
/*- set cdl_thy = '%s_CDL' % options.verification_base_name -*/
/*- set arch_spec_thy = '%s_Arch_Spec' % options.verification_base_name -*/

/*- set group_labels = macros.integrity_group_labels(me.composition, me.configuration) -*/

theory "/*? options.verification_base_name ?*/_CDL_Refine"
imports
  /*? arch_spec_thy ?*/ (* generated arch spec *)
  /*? cdl_thy ?*/ (* generated CDL spec *)
  "CamkesCdlRefine.Policy_CAMKES_CDL"
  "CamkesCdlRefine.Eval_CAMKES_CDL"
  "DPolicy.Dpolicy"
  "Lib.FastMap"
  "Lib.RangeMap"
  "Lib.FP_Eval"
  "Lib.TermPatternAntiquote"
begin

(* FIXME: MOVE *)
setup \<open>
let
  fun check thm = let
    val eta_thm = Conv.fconv_rule Thm.eta_conversion thm;
    fun which_thm thm = if Thm.derivation_name thm <> "" then Thm.derivation_name thm
                       else "\n" ^ @{make_string} thm;
    in if Thm.eq_thm_prop (thm, eta_thm) then thm
       else (warning ("check_eta_norm: fixing thm: " ^ which_thm thm);
             eta_thm)
    end
in
   Attrib.setup \<^binding>\<open>check_eta_norm\<close>
                (pair (fn (_, t) => (NONE, SOME (check t))))
                "eta normalise theorems, and emit warnings"
end
\<close>

context begin interpretation Arch . (* FIXME: needed to talk about ASIDs *)

section \<open>System-specific policy definitions\<close>
text \<open>
  We need to label objects in a way that matches the architecture spec
  and also allows the cap layout to satisfy the access policy.
\<close>

section \<open>Expand policy rules\<close>

/*# FIXME: naming scheme duplicated from arch-definitions #*/
/*- if hasattr(me, 'name') and me.name is not none -*/
    /*- set assembly_name = '%s.%s' % (arch_spec_thy, me.name) -*/
/*- else -*/
    /*- set assembly_name = '%s.assembly\'' % arch_spec_thy -*/
/*- endif -*/
/*- if hasattr(me.composition, 'name') and me.composition.name is not none -*/
    /*- set composition_name = '%s.%s' % (arch_spec_thy, me.composition.name) -*/
/*- else -*/
    /*- set composition_name = '%s.composition\'' % arch_spec_thy -*/
/*- endif -*/

definition /*? options.verification_base_name ?*/_policy
  where
  "/*? options.verification_base_name ?*/_policy \<equiv> policy_of /*? assembly_name ?*/"

schematic_goal /*? options.verification_base_name ?*/_component_names:
  "components (composition /*? assembly_name ?*/) = ?comps"
  apply (clarsimp simp: /*? assembly_name ?*/_def
                        /*? composition_name ?*/_def)
  apply (rule refl)
  done

schematic_goal /*? options.verification_base_name ?*/_connections:
  "connections (composition /*? assembly_name ?*/) = ?spec"
  apply (clarsimp simp: /*? assembly_name ?*/_def
                        /*? composition_name ?*/_def
/*- for c in me.composition.instances -*/
                        /*? arch_spec_thy ?*/./*? isabelle_component(c.name) ?*/_def
/*- endfor -*/
/*- for c in me.composition.connections -*/
                        /*? arch_spec_thy ?*/./*? isabelle_connection(c.name) ?*/_def
/*- endfor -*/
/*- for c in uniq(map(lambda('x: x.type.name'), me.composition.connections)) -*/
                        /*? arch_spec_thy ?*/./*? isabelle_connector(c) ?*/_def
/*- endfor -*/

                        \<comment> \<open>Built-in connector defs\<close>
                        seL4RPC_def
                        seL4Notification_def
                        seL4SharedData_def
                        seL4HardwareMMIO_def
                        seL4HardwareInterrupt_def
        )
  apply (rule refl)
  done

schematic_goal /*? options.verification_base_name ?*/_groups:
  "group_labels (composition /*? assembly_name ?*/) = ?map"
  apply (clarsimp simp: /*? assembly_name ?*/_def
                        /*? composition_name ?*/_def
/*- for c in me.composition.connections -*/
                        /*? arch_spec_thy ?*/./*? isabelle_connection(c.name) ?*/_def
/*- endfor -*/
/*- for c in uniq(map(lambda('x: x.type.name'), me.composition.connections)) -*/
                        /*? arch_spec_thy ?*/./*? isabelle_connector(c) ?*/_def
/*- endfor -*/
        )
  apply (rule refl)
  done

(* Optimise group label lookups *)
lemma /*? options.verification_base_name ?*/_group_label_lookups:
/*- for x in me.composition.instances + me.composition.connections: -*/
  "get_group_label (composition /*? assembly_name ?*/) ''/*? x.name ?*/'' = ''/*? group_labels.get(x.name, x.name) ?*/''"
/*- endfor -*/
  by (simp add: get_group_label_def /*? options.verification_base_name ?*/_groups)+

/*- if get_policy_extra() -*/
lemma /*? options.verification_base_name ?*/_policy_extra:
  "(\<lambda>(subj, auth, obj). (get_group_label (composition /*? assembly_name ?*/) subj, auth,
                         get_group_label (composition /*? assembly_name ?*/) obj)) `
     policy_extra /*? assembly_name ?*/ =
   {(subj, auth, obj).
     /*- for i, (subj, auth, obj) in enumerate(get_policy_extra()) -*/
     /*? '\\<or> ' if i else '  ' ?*/subj = ''/*? subj ?*/'' \<and> auth = /*? auth ?*/ \<and> obj = ''/*? obj ?*/''
     /*- endfor -*/
   }"
  apply (rule_tac t="policy_extra /*? assembly_name ?*/" in subst)
   apply (simp add: /*? assembly_name ?*/_def)
  apply (simp add: /*? options.verification_base_name ?*/_group_label_lookups)
  by fastforce
/*- else -*/
lemma /*? options.verification_base_name ?*/_policy_extra:
  "(\<lambda>(subj, auth, obj). (get_group_label (composition /*? assembly_name ?*/) subj, auth,
                         get_group_label (composition /*? assembly_name ?*/) obj)) `
     policy_extra /*? assembly_name ?*/ =
   {}"
  by (simp add: /*? assembly_name ?*/_def)
/*- endif -*/

schematic_goal /*? options.verification_base_name ?*/_policy_def':
  "/*? options.verification_base_name ?*/_policy = ?PAS"
  (* FIXME: this should be more systematic *)
  apply (clarsimp
            simp: policy_of_def
                  /*? options.verification_base_name ?*/_policy_def
                  /*? options.verification_base_name ?*/_component_names
                  /*? options.verification_base_name ?*/_connections
                  /*? options.verification_base_name ?*/_policy_extra
                  /*? options.verification_base_name ?*/_group_label_lookups
                  Collect_Int_pred_eq Collect_union
            simp del: Collect_case_prod
        )
  apply (subst split_Collect_graph_edge)
  apply (rule Collect_graph_cong_helper)
  apply (clarsimp simp: Groebner_Basis.dnf) \<comment> \<open>normalise\<close>
  apply ((clarsimp cong: conj_cong)?, (clarsimp cong: rev_conj_cong)?) \<comment> \<open>normalise some more\<close>
  apply assign_schematic_dnf
  done

(*
 * From /*? options.verification_base_name ?*/_policy_def', generate a list of rules of the form
 *   "(''subj'', auth, ''obj'') \<in> /*? options.verification_base_name ?*/_policy"
 *)
schematic_goal /*? options.verification_base_name ?*/_policy_gen_cases_:
  "((subj, auth, obj) \<in> /*? options.verification_base_name ?*/_policy) = ?cases"
  apply (clarsimp simp only: /*? options.verification_base_name ?*/_policy_def' mem_Collect_eq)
  by assign_schematic_dnf

local_setup \<open>fn ctxt => let
    fun try_repeat f x = case try f x of SOME x' => try_repeat f x' | NONE => x;
    (* convert "(a = x \<and> b = y \<and> \<dots>) \<longrightarrow> foo a b \<dots>" to "foo x y \<dots>" *)
    val subst_values =
          REPEAT_ALL_NEW (resolve_tac @{context} @{thms conjI}) 1
          #> Seq.hd
          #> Simplifier.rewrite_rule @{context} @{thms atomize_imp}
          #> try_repeat (fn t => t RS @{thm subst_eqn_helper});
    fun process thm =
          case try subst_values thm of
              SOME eqn => [eqn]
            | NONE => process (@{thm disjI1} RS thm) @ process (@{thm disjI2} RS thm);
    val /*? options.verification_base_name ?*/_policy_intros =
          process @{thm /*? options.verification_base_name ?*/_policy_gen_cases_[THEN iffD2]}
          |> distinct Thm.eq_thm_prop; (* remove dups *)
  in
    ctxt
    |> Local_Theory.notes [((Binding.name "/*? options.verification_base_name ?*/_policy_intros", []),
                            [(/*? options.verification_base_name ?*/_policy_intros, [])])]
    |> snd
  end
\<close>
thm /*? options.verification_base_name ?*/_policy_intros


section \<open>Object label mappings\<close>

text \<open>
  Construct mapping of integrity labels for each object.
\<close>

ML \<open>
(* The RangeMap package expects the input in sorted order,
   we need to sort the object IDs by numeric value. *)
fun /*? options.verification_base_name ?*/_id_value ctxt obj_name =
    Proof_Context.get_thm ctxt ("/*? cdl_thy ?*/." ^ obj_name ^ "_id_def")
    |> Thm.prop_of
    |> Logic.dest_equals |> snd
    |> HOLogic.dest_number |> snd;

val /*? options.verification_base_name ?*/_obj_labels =
      (* object name, size bits, policy label *)
    /*- set delim = namespace(value='[') -*//*# need this nonsense to modify variable -- see jinja2 docs #*/
    /*- for obj, label in sorted(object_label_mapping(), key=lambda('x: x[0].name')) -*/
      /*- if not obj.name.startswith('root_untyped_') -*//*# Exclude root untypeds because they overlap other objects and have no policy. FIXME: better way to detect these #*/
        /*? delim.value ?*/ ("/*? isabelle_capdl_identifier(obj.name) ?*/", /*? obj.get_size_bits() if obj.get_size_bits() != None else '0' ?*/, "/*? group_labels.get(label, label) ?*/")
        /*- set delim.value = ',' -*/
      /*- endif -*/
    /*- endfor -*/
    ]
    |> sort (apply2 (#1 #> /*? options.verification_base_name ?*/_id_value @{context}) #> int_ord);

val id_value : string -> int =
  fn id =>
    Proof_Context.get_thm @{context} (id ^ "_def")
    |> Thm.rhs_of |> Thm.term_of |> HOLogic.dest_number |> snd;

(* Now construct our mapping from (ptr, ptr + 2^sz) to labels *)
val /*? options.verification_base_name ?*/_label_entries =
  /*? options.verification_base_name ?*/_obj_labels
  |> map (fn (obj_name, sz, label) => ("/*? cdl_thy ?*/." ^ obj_name ^ "_id", sz, label))
  |> map (fn (id, sz, label) =>
            ((Const (id, @{typ cdl_object_id}),
              @{term "(+) :: cdl_object_id \<Rightarrow> _ \<Rightarrow> _"} $
                Const (id, @{typ cdl_object_id}) $
                (@{term "(^) 2 :: _ \<Rightarrow> cdl_object_id"} $ HOLogic.mk_number @{typ nat} sz)),
             HOLogic.mk_string label))
  |> map (fn (range, label) =>
      (apply2 (Thm.cterm_of @{context}) range, Thm.cterm_of @{context} label));
\<close>

local_setup \<open>
  RangeMap.define_map (RangeMap.name_opts_default "/*? options.verification_base_name ?*/_label")
      /*? options.verification_base_name ?*/_label_entries @{typ cdl_object_id} @{typ label}
      (FP_Eval.eval_conv @{context}
        (FP_Eval.make_rules @{thms word_rel_simps_small word_pow_arith_simps /*? cdl_thy ?*/.ids} []))
\<close>
(* we will primarily use these *)
lemmas /*? options.verification_base_name ?*/_label_lookups =
  /*? options.verification_base_name ?*/_label.start_lookups
    [unfolded /*? options.verification_base_name ?*/_label.tree_list_lookup_eq]

text \<open>
  Define admissible labelling functions to be those that are consistent
  with the mapping we defined above.
\<close>

definition /*? options.verification_base_name ?*/_labelling :: "cdl_object_id \<Rightarrow> string option"
  where
  "/*? options.verification_base_name ?*/_labelling x \<equiv> map_option snd (RangeMap.range_map_of /*? options.verification_base_name ?*/_label.list x)"

definition /*? options.verification_base_name ?*/_admissible_labelling :: "label agent_map \<Rightarrow> bool"
  where
  "/*? options.verification_base_name ?*/_admissible_labelling label_of \<equiv>
      (\<forall>i l. /*? options.verification_base_name ?*/_labelling i = Some l \<longrightarrow> label_of i = l)"

lemma /*? options.verification_base_name ?*/_admissible_labelling_default:
  "/*? options.verification_base_name ?*/_admissible_labelling (the o /*? options.verification_base_name ?*/_labelling)"
  by (simp add: /*? options.verification_base_name ?*/_admissible_labelling_def)

text \<open>Make sure that an admissible labelling exists.\<close>
corollary /*? options.verification_base_name ?*/_admissible_labelling_exists:
  "\<exists>label_of. /*? options.verification_base_name ?*/_admissible_labelling label_of"
  by (blast intro: /*? options.verification_base_name ?*/_admissible_labelling_default)


subsection \<open>Sanity checks for object labelling\<close>

text \<open>
  Check that we always label certain important objects with the obvious
  component name. We check this for each component's:

  \begin{itemize}
    \item Control TCB
    \item Root CNode (CAmkES only generates one CNode level for each component,
          so this suffices for now)
    \item PD and its PTs
    \item TCB root caps (this also covers the CNode and PD, but includes
          additional things like the IPC buffer frame)
  \end{itemize}
\<close>
lemma /*? options.verification_base_name ?*/_admissible_labelling__tcbs_correct:
  "/*? options.verification_base_name ?*/_admissible_labelling label_of \<Longrightarrow>
      (
/*- set delim = namespace(value=' ') -*//*# need this nonsense to modify variable -- see jinja2 docs #*/
/*- for c in me.composition.instances -*/
  /*- if c.type.control -*/
    /*- set group = group_labels.get(c.name, c.name) -*/
      /*? delim.value ?*/ label_of /*? isabelle_capdl_identifier(group) ?*/_cnode_id = ''/*? group ?*/''
      \<and> label_of /*? isabelle_capdl_identifier('%s_%s_0_control_tcb_id' % (c.name, c.name.replace('.', '_'))) ?*/ = ''/*? group ?*/''/*#
  XXX: the extra 'replace' in the second name component duplicates what the camkes tool does internally #*/
      \<and> label_of /*? isabelle_capdl_identifier('%s_group_bin_pd_id' % group) ?*/ = ''/*? group ?*/''
      \<and> (\<forall>cap \<in> ran /*? isabelle_capdl_identifier('%s_%s_0_control_tcb_caps' % (c.name, c.name.replace('.', '_'))) ?*/. \<forall>i \<in> cap_objects cap. label_of i = ''/*? group ?*/'')/*# XXX: ditto here #*/
      \<and> (\<forall>pt_i \<in> mapped_pts_of /*? cdl_thy ?*/.objects /*? isabelle_capdl_identifier('%s_group_bin_pd_caps' % group) ?*/. label_of pt_i = ''/*? group ?*/'')
    /*- set delim.value = '\\<and>' -*/
  /*- endif -*/
/*- endfor -*/
      )"
  (* FIXME: cleanup *)
  apply (simp only: rel_simps arith_simps simp_thms if_False if_True conj_assoc imp_disjL
                    option.map prod.sel
                    ball_simps bex_simps fun_upd_apply ran_map_upd ran_empty
                    finite_set_simps
                    cdl_cap.case cap_objects.simps mapped_pts_of_def object_slots_def

                    /*? options.verification_base_name ?*/_CDL.cap_defs
                    /*? options.verification_base_name ?*/_CDL.obj_defs
                    /*? options.verification_base_name ?*/_CDL.objects_lookups

                    /*? options.verification_base_name ?*/_admissible_labelling_def
                    /*? options.verification_base_name ?*/_labelling_def
                    /*? options.verification_base_name ?*/_label_lookups
              cong: imp_cong)
  done

(*
text \<open>
  Potential check that all labels are inhabited. It is currently allowed for connections
  without any objects which would fail this check. However this check could be useful
  as a sanity check.
\<close>
lemma /*? options.verification_base_name ?*/_admissible_labelling__all_labels_inhabited:
  "/*? options.verification_base_name ?*/_admissible_labelling label_of \<Longrightarrow>
/*- set delim = namespace(value=' ') -*//*# need this nonsense to modify variable -- see jinja2 docs #*/
/*- set seen = set() -*/
/*- for c in composition.instances + me.composition.connections -*/
  /*- set name = group_labels.get(c.name, c.name) -*/
  /*- if name not in seen -*/
    /*? delim.value ?*/ (\<exists>obj. label_of obj = ''/*? name ?*/'')
    /*- do seen.add(name) -*/
    /*- set delim.value = '\\<and>' -*/
  /*- endif -*/
/*- endfor -*/
  "
  apply (simp add: /*? options.verification_base_name ?*/_admissible_labelling_def
                   /*? options.verification_base_name ?*/_labelling_def)
  apply (fastforce intro: /*? options.verification_base_name ?*/_label_lookups)
  done
*)

(* FIXME: more sanity checks *)


subsection \<open>Admissible ASID labels\<close>
/*- set have_ASIDPools = namespace(value=False) -*//*# need this nonsense to modify variable -- see jinja2 docs #*/
/*- for asid_pool, label in object_label_mapping() -*/
    /*- if is_ASIDPool_object(asid_pool) and not (asid_pool.asid_high is none) -*/
        /*- set have_ASIDPools.value = True -*/
    /*- endif -*/
/*- endfor -*/

definition /*? options.verification_base_name ?*/_asids :: "asid_high \<Rightarrow> label option"
  where
/*- if have_ASIDPools.value -*/
  "/*? options.verification_base_name ?*/_asids \<equiv> [
    /*- set delim = namespace(value=' ') -*//*# need this nonsense to modify variable -- see jinja2 docs #*/
    /*- for asid_pool, label in object_label_mapping() -*/
        /*- if is_ASIDPool_object(asid_pool) and not (asid_pool.asid_high is none) -*/
            /*? delim.value ?*/ /*? '0x%x' % asid_pool.asid_high ?*/ \<mapsto> ''/*? label ?*/''
            /*- set delim.value = ',' -*/
        /*- endif -*/
    /*- endfor -*/
   ]"
/*- else -*/
   "/*? options.verification_base_name ?*/_asids \<equiv> map_of []"
/*- endif -*/

definition /*? options.verification_base_name ?*/_admissible_asids :: "label agent_asid_map \<Rightarrow> bool"
  where
  "/*? options.verification_base_name ?*/_admissible_asids asidAbs \<equiv>
     (\<forall>asid label. /*? options.verification_base_name ?*/_asids (asid_high_bits_of asid) = Some label \<longrightarrow> asidAbs asid = label)"

(* Expanded (FIXME: assumes exactly one ASID slot) *)
schematic_goal /*? options.verification_base_name ?*/_admissible_asids_cases:
  "/*? options.verification_base_name ?*/_admissible_asids irqAbs = ?cases"
  apply (clarsimp simp: /*? options.verification_base_name ?*/_admissible_asids_def /*? options.verification_base_name ?*/_asids_def)
/*- if have_ASIDPools.value -*/
  apply (rule refl)
/*- else -*/
  apply (rule TrueI)
/*- endif -*/
  done

subsection \<open>Admissible IRQ labels\<close>

/*# FIXME: maybe should be generated from components' .irq configuration
    rather than blindly scraping the objects list #*/
/*- set have_IRQs = namespace(value=False) -*//*# need this nonsense to modify variable -- see jinja2 docs #*/
/*- for obj, label in object_label_mapping() -*/
  /*- if is_IRQ_object(obj) -*/
    /*- set have_IRQs.value = True -*/
  /*- endif -*/
/*- endfor -*/

/*# FIXME: workaround because FastMap currently doesn't support empty maps #*/
/*- if have_IRQs.value -*/
local_setup \<open>
let
  val entries =
    /*- for obj, label in object_label_mapping() -*/
      /*- if is_IRQ_object(obj) -*/
        (/*? obj.number ?*/, "/*? group_labels.get(label, label) ?*/") ::
      /*- endif -*/
    /*- endfor -*/
    []
    |> sort (prod_ord int_ord string_ord);
in
  FastMap.define_map
    (FastMap.name_opts_default "/*? options.verification_base_name ?*/_irqs")
    (map (fn (irq, l) => (HOLogic.mk_number @{typ cdl_irq} irq, HOLogic.mk_string l))
         entries)
    @{term "id :: cdl_irq \<Rightarrow> _"}
    []
    false
end
\<close>
/*- else -*/
definition /*? options.verification_base_name ?*/_irqs :: "label option agent_irq_map"
  where
  "/*? options.verification_base_name ?*/_irqs \<equiv> map_of []"
/*# would have been generated by FastMap #*/
lemmas /*? options.verification_base_name ?*/_irqs_lookups = refl
/*- endif -*/

definition /*? options.verification_base_name ?*/_admissible_irqs :: "label agent_irq_map \<Rightarrow> bool"
  where
  "/*? options.verification_base_name ?*/_admissible_irqs irqAbs \<equiv>
     (\<forall>irq label. /*? options.verification_base_name ?*/_irqs irq = Some label \<longrightarrow> irqAbs irq = label)"

(* Expanded *)
schematic_goal /*? options.verification_base_name ?*/_admissible_irqs_cases:
  "/*? options.verification_base_name ?*/_admissible_irqs irqAbs = ?cases"
  apply (clarsimp simp only: /*? options.verification_base_name ?*/_admissible_irqs_def)
/*- if have_IRQs.value -*/
  apply (subst iterate_labelling_helper)
    apply (rule /*? options.verification_base_name ?*/_irqs_to_lookup_list)
   apply (rule /*? options.verification_base_name ?*/_irqs_keys_distinct)
  apply (clarsimp simp only: FastMap.list_all_dest)
  apply (rule refl)
/*- else -*//*# no FastMap theorems #*/
  apply (clarsimp simp: /*? options.verification_base_name ?*/_irqs_def)
  apply (rule TrueI)
/*- endif -*/
  done


section \<open>Admissible PAS\<close>

text \<open>
  This defines a set of policies that fit our arch spec and cap layout.
\<close>
definition /*? options.verification_base_name ?*/_admissible_pas :: "label PAS \<Rightarrow> bool"
  where
  "/*? options.verification_base_name ?*/_admissible_pas pas \<equiv>
     /*? options.verification_base_name ?*/_admissible_labelling (pasObjectAbs pas) \<and>
     /*? options.verification_base_name ?*/_admissible_asids (pasASIDAbs pas) \<and>
     /*? options.verification_base_name ?*/_admissible_irqs (pasIRQAbs pas) \<and>
     pasSubject pas \<in> fst ` set (components (composition /*? assembly_name ?*/)) \<and>
     /*? options.verification_base_name ?*/_policy \<subseteq> pasPolicy pas"

text \<open>Again, ensure that admissible policies exist.\<close>
lemma /*? options.verification_base_name ?*/_admissible_pas_exists:
  "\<exists>pas. /*? options.verification_base_name ?*/_admissible_pas pas"
  apply (insert /*? options.verification_base_name ?*/_admissible_labelling_exists)
  apply (erule exE, rename_tac poa)
  (* For now, just fill in the fields we need. *)
  apply (rule_tac x = "undefined\<lparr>
                         pasObjectAbs := poa,
                         pasPolicy := /*? options.verification_base_name ?*/_policy,
                         pasSubject := fst (hd (components (composition /*? assembly_name ?*/))),
                         pasASIDAbs := the o /*? options.verification_base_name ?*/_asids o asid_high_bits_of,
                         pasIRQAbs := the o /*? options.verification_base_name ?*/_irqs
                         \<rparr>"
                  in exI)

  apply (simp add: /*? options.verification_base_name ?*/_admissible_pas_def)
  apply (intro conjI)
    apply (simp add: /*? options.verification_base_name ?*/_admissible_asids_def)
   apply (simp add: /*? options.verification_base_name ?*/_admissible_irqs_def)
  apply (simp add: /*? options.verification_base_name ?*/_admissible_pas_def /*? options.verification_base_name ?*/_connections /*? options.verification_base_name ?*/_component_names)
  done

text \<open>
  Checking the transitivity conditions for @{const policy_wellformed} is quadratic in
  the size of our policy; here we extract relevant subsets of the policy cases to
  make things a bit faster.

  Ultimately, we would like to prove a generic @{const policy_wellformed} theorem for
  all @{const policy_of} outputs, but the current messiness of
  @{const policy_of} and @{const wellformed_assembly} are not conducive for that.
\<close>

lemmas /*? options.verification_base_name ?*/_policy_cases_Control =
  /*? options.verification_base_name ?*/_policy_gen_cases_[where auth = "Control", simplified]
lemmas /*? options.verification_base_name ?*/_policy_cases_Receive =
  /*? options.verification_base_name ?*/_policy_gen_cases_[where auth = "Receive", simplified]
lemmas /*? options.verification_base_name ?*/_policy_cases_Reply =
  /*? options.verification_base_name ?*/_policy_gen_cases_[where auth = "Reply", simplified]
lemmas /*? options.verification_base_name ?*/_policy_cases_Grant =
  /*? options.verification_base_name ?*/_policy_gen_cases_[where auth = "auth.Grant", simplified]
lemmas /*? options.verification_base_name ?*/_policy_cases_Call =
  /*? options.verification_base_name ?*/_policy_gen_cases_[where auth = "Call", simplified]
lemmas /*? options.verification_base_name ?*/_policy_cases_DeleteDerived =
  /*? options.verification_base_name ?*/_policy_gen_cases_[where auth = "DeleteDerived", simplified]
lemmas /*? options.verification_base_name ?*/_policy_cases_DeleteDerived2 =
/*- for c in me.composition.instances -*/
  /*? options.verification_base_name ?*/_policy_cases_DeleteDerived[
        where subj = "''/*? group_labels.get(c.name, c.name) ?*/''", simplified simp_thms list.distinct list.inject char.inject]
/*- endfor -*/

text \<open>
  Ensure that our base access policy is wellformed.
  This lets us extend it to other wellformed policies.
\<close>

(* Expand a policy rule of the form
 *   "(a, auth, b) \<in> policy \<Longrightarrow> (a = ''a'' \<and> b = ''b'' \<or> ...)"
 * and simplify string label comparisons *)
method unfold_policy uses expand =
  (drule expand;
   elim conjE disjE;
   (simp only: simp_thms list.distinct list.inject char.inject cong: disj_cong)?)

lemma /*? options.verification_base_name ?*/_policy_wellformed:
  "\<lbrakk> pasPolicy aag = /*? options.verification_base_name ?*/_policy;
     pasSubject aag \<in> get_group_label (composition /*? assembly_name ?*/)
                      ` fst ` set (components (composition /*? assembly_name ?*/));
     \<not> pasMaySendIrqs aag \<comment> \<open>ignore IRQs for now\<close>
   \<rbrakk> \<Longrightarrow> pas_wellformed aag"
  apply clarsimp
  apply (rule camkes_policy_wellformedI)
             (* Components may not send IRQs *)
             subgoal
               apply blast
               done
            (* Components are agents *)
            subgoal
              apply (fastforce simp: /*? options.verification_base_name ?*/_connections
                                     /*? options.verification_base_name ?*/_component_names
                                     /*? options.verification_base_name ?*/_group_label_lookups
                               intro: /*? options.verification_base_name ?*/_policy_intros)
              done
           (* All subjects have self Control *)
           subgoal
             apply (unfold_policy expand: /*? options.verification_base_name ?*/_policy_gen_cases_[THEN iffD1];
                    (intro /*? options.verification_base_name ?*/_policy_intros)?)
             done
          (* Grant confinement *)
          subgoal
            apply (unfold_policy expand: /*? options.verification_base_name ?*/_policy_cases_Grant[THEN iffD1];
                   (intro /*? options.verification_base_name ?*/_policy_intros)?)
            done
         (* Control confinement *)
         subgoal
           apply (fastforce dest: /*? options.verification_base_name ?*/_policy_cases_Control[THEN iffD1]
                            intro: /*? options.verification_base_name ?*/_policy_intros)
           done
        (* Control implies all rights *)
        subgoal
          apply (fastforce dest: /*? options.verification_base_name ?*/_policy_cases_Control[THEN iffD1]
                           intro: /*? options.verification_base_name ?*/_policy_intros)
          done
       (* Components are not Receive targets *)
       subgoal
         apply (unfold_policy expand: /*? options.verification_base_name ?*/_policy_cases_Receive[THEN iffD1];
                unfold_policy expand: /*? options.verification_base_name ?*/_policy_cases_Control[THEN iffD1];
                (intro /*? options.verification_base_name ?*/_policy_intros)?)
         done
      (* Components are not Call targets *)
      subgoal
        apply (unfold_policy expand: /*? options.verification_base_name ?*/_policy_cases_Call[THEN iffD1];
               unfold_policy expand: /*? options.verification_base_name ?*/_policy_cases_Control[THEN iffD1];
               (intro /*? options.verification_base_name ?*/_policy_intros)?)
        done
     (* Call implies SyncSend *)
     subgoal
       apply (unfold_policy expand: /*? options.verification_base_name ?*/_policy_cases_Call[THEN iffD1];
              (intro /*? options.verification_base_name ?*/_policy_intros)?)
       done
    (* Reply implies DeleteDerived *)
    subgoal
      apply (unfold_policy expand: /*? options.verification_base_name ?*/_policy_cases_Reply[THEN iffD1];
             (intro /*? options.verification_base_name ?*/_policy_intros)?)
      done
   (* Call + Receive implies Reply *)
   subgoal
     apply (unfold_policy expand: /*? options.verification_base_name ?*/_policy_cases_Call[THEN iffD1];
            unfold_policy expand: /*? options.verification_base_name ?*/_policy_cases_Receive[THEN iffD1];
            (intro /*? options.verification_base_name ?*/_policy_intros)?)
     done
  (* DeleteDerived is transitive (see also VER-1030) *)
  subgoal
    apply (erule(4) complete_graph_is_transitive')
    apply (subst let_weak_cong)
     apply (simp only: /*? options.verification_base_name ?*/_policy_cases_DeleteDerived Collect_case_prod_dnf)
    apply (simp only: Let_def finite_set_simps prod.sel
                      image_insert image_empty
                      (* performance note: insert_commute sorts labels in the simplifier,
                         then insert_absorb2 removes duplicates *)
                      insert_commute insert_absorb2)
    apply (simp; intro conjI /*? options.verification_base_name ?*/_policy_intros)

    (* slow version, O(#labels ^ 4) cases*)
    (*
    apply (unfold_policy expand: /*? options.verification_base_name ?*/_policy_cases_DeleteDerived[THEN iffD1];
           unfold_policy expand: /*? options.verification_base_name ?*/_policy_cases_DeleteDerived2[THEN iffD1];
           (intro /*? options.verification_base_name ?*/_policy_intros)?)
    *)
    done
  done


section \<open>CAmkES-capDL refinement proof\<close>

(* specialise ptr_range rewrite rule *)
lemmas /*? options.verification_base_name ?*/_label_over_ptr_range =
  label_over_ptr_range[
      (* FP_Eval only supports first-order matching, so instantiate P *)
      where P = "\<lambda>l. generic_tag type tag ((_, _, l) \<in> _)"
        and label_spec = /*? options.verification_base_name ?*/_labelling
        for type tag,
      OF /*? options.verification_base_name ?*/_label.list_monotonic,
      (* expand labelling into tree lookup *)
      unfolded /*? options.verification_base_name ?*/_labelling_def, OF refl]
lemmas /*? options.verification_base_name ?*/_label_over_ptr_range_cases =
  /*? options.verification_base_name ?*/_label_lookups[THEN /*? options.verification_base_name ?*/_label_over_ptr_range]

lemma /*? options.verification_base_name ?*/_asid_policy:
  assumes admissible_pas:
     "/*? options.verification_base_name ?*/_admissible_pas pas"
  shows
    "cdl_state_asids_to_policy pas /*? options.verification_base_name ?*/_CDL.state \<subseteq> pasPolicy pas"
proof -
  (* everything needed to evaluate asid integrity... *)
  note obj_policy_eval_simps' =
        /*? options.verification_base_name ?*/_label_lookups
        /*? options.verification_base_name ?*/_CDL.obj_defs
        /*? options.verification_base_name ?*/_CDL.objects_lookups
        (* Map.empty is actually an abbrev for a lambda, which fp_eval
           doesn't allow as a rule LHS. Rewrite eagerly first *)
        (* FIXME: generate these with map_of in the first place.
           Also fix "rev ..." in graph_of_map_of__sorted_eval *)
        /*? options.verification_base_name ?*/_CDL.cap_defs[simplified fun_upds_to_map_of]
        /*? options.verification_base_name ?*/_label_over_ptr_range_cases

        \<comment> \<open>FIXME: Isabelle2019 simplifier doesn't eta-normalise??\<close>
        Collect_asid_high__eval_helper
            [simplified asid_high_bits_def, simplified, check_eta_norm]

        /*? options.verification_base_name ?*/_asids_def[simplified fun_upds_to_map_of] map_of_Cons_code
        /*? options.verification_base_name ?*/_CDL.asid_table_def[simplified fun_upds_to_map_of]

        obj_policy_eval_simps

  show ?thesis
    apply (rule cdl_state_asids_to_policy__eval[where
                  policy_spec=/*? options.verification_base_name ?*/_policy and
                  obj_label_spec=/*? options.verification_base_name ?*/_labelling and
                  asid_label_spec=/*? options.verification_base_name ?*/_asids
           ])
        using admissible_pas /*? options.verification_base_name ?*/_admissible_pas_def apply blast
       using admissible_pas /*? options.verification_base_name ?*/_admissible_pas_def /*? options.verification_base_name ?*/_admissible_labelling_def apply blast
      using admissible_pas /*? options.verification_base_name ?*/_admissible_pas_def /*? options.verification_base_name ?*/_admissible_asids_def apply blast

     (* ASIDs in objects *)
     subgoal
       apply (simp only: /*? options.verification_base_name ?*/_labelling_def)
       apply (tactic \<open>let
                val rules = @{thms /*? options.verification_base_name ?*/_CDL.state_def cdl_state.simps
                                   /*? options.verification_base_name ?*/_CDL.objects_to_lookup_list
                                   graph_of_map_of__distinct_eval if_True
                                   /*? options.verification_base_name ?*/_CDL.objects_keys_distinct};
                val congs = @{thms obj_policy_eval_congs};
                in SUBGOAL (fn _ => FP_Eval.eval_tac @{context} (FP_Eval.make_rules rules congs) 1)
                           1 end\<close>)
       (* this is a separate step for now, because graph_of_map_of__sorted_eval
          won't work for objects list *)
       apply (tactic \<open>let
                val rules = @{thms obj_policy_eval_simps'};
                val congs = @{thms obj_policy_eval_congs};
                val conv = rpair FP_Eval.skel0
                         #> FP_Eval.eval @{context} (FP_Eval.make_rules rules congs)
                         #> tap (fn (_, c) => tracing ("fp_eval counters: " ^ @{make_string} c))
                         #> fst #> fst;
                in SUBGOAL (fn _ => Conv.gconv_rule conv 1 #> Seq.succeed) 1 end\<close>;
              intro TrueI conjI /*? options.verification_base_name ?*/_policy_intros[THEN generic_tagP_I])
       done

    (* ASID pools *)
    apply (simp only: /*? options.verification_base_name ?*/_labelling_def /*? options.verification_base_name ?*/_CDL.state_def cdl_state.simps)
    apply (tactic \<open>let
             val rules = @{thms /*? options.verification_base_name ?*/_CDL.state_def cdl_state.simps
                                /*? options.verification_base_name ?*/_CDL.objects_to_lookup_list
                                graph_of_map_of__distinct_eval if_True
                                /*? options.verification_base_name ?*/_CDL.objects_keys_distinct};
             val congs = @{thms obj_policy_eval_congs};
             in SUBGOAL (fn _ => FP_Eval.eval_tac @{context} (FP_Eval.make_rules rules congs) 1)
                        1 end\<close>)
    (* this is a separate step for now, because graph_of_map_of__sorted_eval
       won't work for objects list *)
    apply (tactic \<open>let
             val rules = @{thms obj_policy_eval_simps'};
             val congs = @{thms obj_policy_eval_congs};
             val conv = rpair FP_Eval.skel0
                      #> FP_Eval.eval @{context} (FP_Eval.make_rules rules congs)
                      #> tap (fn (_, c) => tracing ("fp_eval counters: " ^ @{make_string} c))
                      #> fst #> fst;
             in SUBGOAL (fn _ => Conv.gconv_rule conv 1 #> Seq.succeed) 1 end\<close>;
           intro TrueI conjI /*? options.verification_base_name ?*/_policy_intros[THEN generic_tagP_I])
    done
qed

lemma /*? options.verification_base_name ?*/_irq_policy:
  assumes admissible_pas:
     "/*? options.verification_base_name ?*/_admissible_pas pas"
  shows
    "cdl_state_irqs_to_policy pas /*? options.verification_base_name ?*/_CDL.state \<subseteq> pasPolicy pas"
proof -
  (* everything needed to evaluate asid integrity... *)
  note obj_policy_eval_simps' =
        /*? options.verification_base_name ?*/_label_lookups
        /*? options.verification_base_name ?*/_CDL.obj_defs
        (* Map.empty is actually an abbrev for a lambda, which fp_eval
           doesn't allow as a rule LHS. Rewrite eagerly first *)
        (* FIXME: generate these with map_of in the first place.
           Also fix "rev ..." in graph_of_map_of__sorted_eval *)
        /*? options.verification_base_name ?*/_CDL.cap_defs[simplified fun_upds_to_map_of]
        /*? options.verification_base_name ?*/_label_over_ptr_range_cases

        /*? options.verification_base_name ?*/_irqs_lookups

        obj_policy_eval_simps

  show ?thesis
    apply (rule cdl_state_irqs_to_policy__eval[where
                  policy_spec=/*? options.verification_base_name ?*/_policy and
                  obj_label_spec=/*? options.verification_base_name ?*/_labelling and
                  irq_label_spec=/*? options.verification_base_name ?*/_irqs
           ])
       using admissible_pas /*? options.verification_base_name ?*/_admissible_pas_def apply blast
      using admissible_pas /*? options.verification_base_name ?*/_admissible_pas_def /*? options.verification_base_name ?*/_admissible_labelling_def apply blast
     using admissible_pas /*? options.verification_base_name ?*/_admissible_pas_def /*? options.verification_base_name ?*/_admissible_irqs_def apply blast

    apply (simp only: /*? options.verification_base_name ?*/_labelling_def)
    apply (tactic \<open>let
             val rules = @{thms /*? options.verification_base_name ?*/_CDL.state_def cdl_state.simps
                                /*? options.verification_base_name ?*/_CDL.objects_to_lookup_list
                                graph_of_map_of__distinct_eval if_True
                                /*? options.verification_base_name ?*/_CDL.objects_keys_distinct};
             val congs = @{thms obj_policy_eval_congs};
             in SUBGOAL (fn _ => FP_Eval.eval_tac @{context} (FP_Eval.make_rules rules congs) 1)
                        1 end\<close>)
    (* this is a separate step for now, because graph_of_map_of__sorted_eval
       won't work for objects list *)
    apply (tactic \<open>let
             val rules = @{thms obj_policy_eval_simps'};
             val congs = @{thms obj_policy_eval_congs};
             val conv = rpair FP_Eval.skel0
                      #> FP_Eval.eval @{context} (FP_Eval.make_rules rules congs)
                      #> tap (fn (_, c) => tracing ("fp_eval counters: " ^ @{make_string} c))
                      #> fst #> fst;
             in SUBGOAL (fn _ => Conv.gconv_rule conv 1 #> Seq.succeed) 1 end\<close>;
           intro TrueI conjI /*? options.verification_base_name ?*/_policy_intros[THEN generic_tagP_I])
    done
qed

text \<open>Main integrity proof\<close>

theorem /*? options.verification_base_name ?*/_pcs_refined:
  assumes other_assms:
     "pas_wellformed pas"
     (* TODO *) "cdl_irq_map_wellformed pas /*? options.verification_base_name ?*/_CDL.state"
     (* TODO *) "cdl_tcb_domain_map_wellformed pas /*? options.verification_base_name ?*/_CDL.state"
  assumes admissible_pas:
     "/*? options.verification_base_name ?*/_admissible_pas pas"
  shows
     "pcs_refined pas /*? options.verification_base_name ?*/_CDL.state"
proof -
  from admissible_pas have /*? options.verification_base_name ?*/_policy:
    "/*? options.verification_base_name ?*/_policy \<subseteq> pasPolicy pas"
    by (simp add: /*? options.verification_base_name ?*/_admissible_pas_def)

  (* everything needed to evaluate object integrity... *)
  note obj_policy_eval_simps' =
        /*? options.verification_base_name ?*/_label_lookups
        /*? options.verification_base_name ?*/_CDL.obj_defs
        (* Map.empty is actually an abbrev for a lambda, which fp_eval
           doesn't allow as a rule LHS. Rewrite eagerly first *)
        (* FIXME: generate these with map_of in the first place.
           Also fix "rev ..." in graph_of_map_of__sorted_eval *)
        /*? options.verification_base_name ?*/_CDL.cap_defs[simplified fun_upds_to_map_of]
        /*? options.verification_base_name ?*/_label_over_ptr_range_cases

        obj_policy_eval_simps

  show ?thesis
    apply (clarsimp simp only: simp_thms
                               pcs_refined_def other_assms
                               /*? options.verification_base_name ?*/_asid_policy[OF admissible_pas]
                               /*? options.verification_base_name ?*/_irq_policy[OF admissible_pas]
                    del: subsetI)
    apply (rule helper_pcs_refined_policy__eval[
                  where policy_spec = /*? options.verification_base_name ?*/_policy
                    and label_spec = /*? options.verification_base_name ?*/_labelling])
        (* instantiate policy specs *)
        apply (rule /*? options.verification_base_name ?*/_policy)
       using admissible_pas /*? options.verification_base_name ?*/_admissible_pas_def /*? options.verification_base_name ?*/_admissible_labelling_def
       apply blast

      text \<open>
         CDT properties.
         FIXME: Our capDL assigns an empty CDT, so there's not much to do here right now.
      \<close>
      apply ((fastforce simp: /*? options.verification_base_name ?*/_CDL.state_def /*? options.verification_base_name ?*/_CDL.cdt_def)+)[2]

    text \<open>Object case.\<close>
    apply (simp only: /*? options.verification_base_name ?*/_labelling_def)
    (* this is a separate step for now, because graph_of_map_of__sorted_eval
       won't work for objects list *)
    apply (tactic \<open>let
             val rules = @{thms /*? options.verification_base_name ?*/_CDL.state_def cdl_state.simps
                                /*? options.verification_base_name ?*/_CDL.objects_to_lookup_list
                                graph_of_map_of__distinct_eval if_True
                                /*? options.verification_base_name ?*/_CDL.objects_keys_distinct};
             val congs = @{thms obj_policy_eval_congs};
             in SUBGOAL (fn _ => FP_Eval.eval_tac @{context} (FP_Eval.make_rules rules congs) 1)
                        1 end\<close>)
    (* this is a separate step for now, because graph_of_map_of__sorted_eval
       won't work for objects list *)
    apply (tactic \<open>let
             val rules = @{thms obj_policy_eval_simps'};
             val congs = @{thms obj_policy_eval_congs};
             val conv = rpair FP_Eval.skel0
                      #> FP_Eval.eval @{context} (FP_Eval.make_rules rules congs)
                      #> tap (fn (_, c) => tracing ("fp_eval counters: " ^ @{make_string} c))
                      #> fst #> fst;
             in SUBGOAL (fn _ => Conv.gconv_rule conv 1 #> Seq.succeed) 1 end\<close>;
           intro TrueI conjI /*? options.verification_base_name ?*/_policy_intros[THEN generic_tagP_I])
    done
qed

end
end