From 2c3b4c24fc58b28ab688b1ee98e7a7459275e976 Mon Sep 17 00:00:00 2001 From: Japheth Lim Date: Fri, 26 Jul 2019 11:32:07 +1000 Subject: [PATCH] CamkesCdlRefine, Lib: add debug tag for integrity policy This tags each generated policy goal with the object and cap that led to that goal. We create a new constant `generic_tag` in Lib for this purpose. --- camkes/cdl-refine/Eval_CAMKES_CDL.thy | 27 ++++++++++------ lib/GenericTag.thy | 44 +++++++++++++++++++++++++++ lib/ROOT | 1 + 3 files changed, 62 insertions(+), 10 deletions(-) create mode 100644 lib/GenericTag.thy diff --git a/camkes/cdl-refine/Eval_CAMKES_CDL.thy b/camkes/cdl-refine/Eval_CAMKES_CDL.thy index 21b5c06f1..a05b32165 100644 --- a/camkes/cdl-refine/Eval_CAMKES_CDL.thy +++ b/camkes/cdl-refine/Eval_CAMKES_CDL.thy @@ -17,6 +17,7 @@ imports "Lib.FastMap" "Lib.RangeMap" "Lib.FP_Eval" + "Lib.GenericTag" begin text \ @@ -244,14 +245,16 @@ lemma helper_pcs_refined_policy__eval: \auth \ cdl_cap_auth_conferred cap. \oref \ cdl_obj_refs cap. (case label_spec oref of - Some orefl \ (pl, auth, orefl) \ policy_spec + Some orefl \ generic_tag ''obj policy'' (p, cap, cdl_obj_refs cap) + ((pl, auth, orefl) \ policy_spec) | _ \ False) | _ \ False)" shows "auth_graph_map (pasObjectAbs aag) (cdl_state_objs_to_policy s) \ (pasPolicy aag)" apply (rule helper_pcs_refined_policyI) apply (blast intro: cdt_policy) apply (blast intro: delete_derived_policy) - apply (fastforce intro: subsetD[OF policy_spec] + 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 @@ -398,13 +401,14 @@ lemma cdl_state_irqs_to_policy__eval: \(p_idx, cap) \ graph_of (object_slots p_obj). \irq \ cdl_cap_irqs_controlled cap. (case irq_label_spec irq of - Some irql \ (pl, Control, irql) \ policy_spec + Some irql \ generic_tag ''irq policy'' (p, cap, irq) + ((pl, Control, irql) \ policy_spec) | _ \ False) | _ \ False) \ cdl_state_irqs_to_policy aag s \ pasPolicy aag" apply clarsimp apply (erule cdl_state_irqs_to_policy_aux.cases) - apply (fastforce simp: opt_cap_def slots_of_def graph_of_def + apply (fastforce simp: opt_cap_def slots_of_def graph_of_def remove_generic_tag split: option.splits dest: obj_label_spec irq_label_spec intro: subsetD[OF policy_spec]) @@ -422,7 +426,8 @@ lemma cdl_state_asids_to_policy__eval: \(p_idx, cap) \ graph_of (object_slots p_obj). \asid \ asid_high_bits_of ` cdl_cap_asid' cap. (case asid_label_spec asid of - Some irql \ (pl, Control, irql) \ policy_spec + Some asidl \ generic_tag ''asid policy'' (p, cap, asid) + ((pl, Control, asidl) \ policy_spec) | _ \ False) | _ \ False)" and asid_table_lookups: @@ -435,29 +440,31 @@ lemma cdl_state_asids_to_policy__eval: \(asid_low, pd_cap) \ 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 \ (asidl, Control, pdl) \ policy_spec + Some pdl \ generic_tag ''asid PD policy'' (asid_high, pd_cap) + ((asidl, Control, pdl) \ policy_spec) | _ \ False) | _ \ False) \ (case obj_label_spec (cap_object asid_pool_cap) of Some asid_pool_l \ - (asid_pool_l, ASIDPoolMapsASID, asidl) \ policy_spec + generic_tag ''asid pool policy'' (asid_high, asid_pool_cap) + ((asid_pool_l, ASIDPoolMapsASID, asidl) \ policy_spec) | _ \ False) | _ \ False)" shows "cdl_state_asids_to_policy aag s \ pasPolicy aag" apply clarsimp apply (erule cdl_state_asids_to_policy_aux.cases) - using cap_asids + 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 + 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 + 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] diff --git a/lib/GenericTag.thy b/lib/GenericTag.thy new file mode 100644 index 000000000..cfc9b641c --- /dev/null +++ b/lib/GenericTag.thy @@ -0,0 +1,44 @@ +(* + * Copyright 2019, Data61 + * Commonwealth Scientific and Industrial Research Organisation (CSIRO) + * ABN 41 687 119 230. + + * This software may be distributed and modified according to the terms of + * the BSD 2-Clause license. Note that NO WARRANTY is provided. + * See "LICENSE_BSD2.txt" for details. + + * @TAG(DATA61_BSD) + *) + +theory GenericTag +imports + HOL.HOL +begin + +text \ + Generic annotation constant. + + @{typ 'ns} is a namespace parameter and should be a different + type or constant for each distinct use of this constant. + + @{typ 'tag} is an arbitrary annotation associated with the actual + value @{term x}. +\ +definition generic_tag :: "'ns \ 'tag \ 'a \ 'a" + where remove_generic_tag[code del]: "generic_tag _ _ x \ x" + +text \Often the tagged value is a proposition to be proved.\ +lemma generic_tagP_I: + "P \ generic_tag ns tag P" + by (simp add: remove_generic_tag) + +lemma generic_tag_True: + "generic_tag ns tag True" + by (simp add: remove_generic_tag) + +text \We often want to avoid rewriting under annotations.\ +lemma generic_tag_cong: + "x = x' \ generic_tag ns tag x = generic_tag ns tag x'" + by simp + +end \ No newline at end of file diff --git a/lib/ROOT b/lib/ROOT index 72cb07a87..8f5530b15 100644 --- a/lib/ROOT +++ b/lib/ROOT @@ -78,6 +78,7 @@ session Lib (lib) = Word_Lib + Conjuncts DetWPLib Guess_ExI + GenericTag (* should really be a separate session, but too entangled atm: *) NonDetMonadLemmaBucket