1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: GPL-2.0-only 5 *) 6 7theory Deterministic_AC 8imports 9 "AInvs.ArchDetSchedSchedule_AI" 10begin 11 12(*This theory defines an abstract "integrity" property over 13 the extensible specification that the deterministic specification 14 is shown to preserve. Essentially it demonstrates that the only 15 elements altered in the cdt_list are the given parameters and 16 their descendants. *) 17 18(* Analagous to the Control edges that pas_refined imposes. *) 19definition all_children where 20"all_children P m \<equiv> (\<forall>c p. m c = Some p \<longrightarrow> P p \<longrightarrow> P c)" 21 22primrec list_filter :: "'a list \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a list" where 23 "list_filter [] P = []" | 24 "list_filter (x # xs) P = (if (P x) then (list_filter xs P) 25 else x # (list_filter xs P))" 26 27abbreviation 28"filtered_eq P list list' \<equiv> list_filter list P = list_filter list' P" 29 30lemma list_filter_distr[simp]: "list_filter (list @ list') P = (list_filter list P) @ (list_filter list' P)" 31 apply (induct list,simp+) 32 done 33 34lemma list_filter_empty[simp]: "\<forall>x \<in> set list. P x \<Longrightarrow> list_filter list P = []" 35 apply (induct list,simp+) 36 done 37 38lemma list_filter_replace_list: "\<forall>x \<in> set list'. P x \<Longrightarrow> P a \<Longrightarrow> 39 filtered_eq P (list_replace_list list a list') list" 40 apply (induct list,simp+) 41 done 42 43lemma list_filter_insert_after: "P b \<Longrightarrow> 44 filtered_eq P (list_insert_after list a b) list" 45 apply (induct list,simp+) 46 done 47 48lemma list_filter_swap: "P b \<Longrightarrow> P a \<Longrightarrow> 49 filtered_eq P (list_swap list a b) list" 50 apply (induct list,(simp add: list_swap_def)+) 51 done 52 53lemma list_filter_replace: "P b \<Longrightarrow> P a \<Longrightarrow> 54 filtered_eq P (list_replace list a b) list" 55 apply (induct list,(simp add: list_replace_def)+) 56 done 57 58lemma list_filter_remove: "P a \<Longrightarrow> 59 filtered_eq P (list_remove list a) list" 60 apply (induct list,simp+) 61 done 62 63 64(* Here P is meant to decide whether a cslot_ptr is part of the current 65 subject. Integrity is said to hold of two cdt_lists if either an 66 entry is part of the current subject, or their lists are equivalent 67 with all entries from the current subject removed. 68 69 We use this to reason that changes to a non-subject entry are only allowed 70 if that entry's list contains a child that is part of the current subject. 71 It is stated in this way so that the property can be shown to be transitive.*) 72 73definition list_integ where 74"list_integ P t t' \<equiv> \<forall>x. P x \<or> (filtered_eq P (cdt_list t x) (cdt_list t' x))" 75 76lemmas list_integI = list_integ_def[THEN meta_eq_to_obj_eq,THEN iffD2,rule_format] 77lemma list_integE: 78 assumes hyp: "list_integ P t t'" 79 obtains "P x" | "(filtered_eq P (cdt_list t x) (cdt_list t' x))" 80 using hyp list_integ_def by blast 81 82 83lemma update_cdt_list_wp: 84 "\<lbrace>(\<lambda>s. P (s\<lparr>cdt_list := f (cdt_list s)\<rparr>))\<rbrace> update_cdt_list f \<lbrace>\<lambda>_.P\<rbrace>" 85 apply (simp add: update_cdt_list_def set_cdt_list_def) 86 apply wp 87 done 88 89 90lemma cap_move_list_integrity: 91 notes split_paired_All[simp del] 92 shows 93 "\<lbrace>list_integ P st and K(P src) and K(P dest)\<rbrace> cap_move_ext src dest src_p dest_p \<lbrace>\<lambda>_. list_integ P st\<rbrace>" 94 apply (simp add: cap_move_ext_def split del: if_split) 95 apply (wp update_cdt_list_wp) 96 apply (intro impI conjI allI | simp add: list_filter_replace list_filter_remove split: option.splits | elim conjE | simp add: list_integ_def)+ 97 done 98 99lemma cap_insert_list_integrity: 100 notes split_paired_All[simp del] 101 shows 102 "\<lbrace>list_integ P st and K(P dest)\<rbrace> cap_insert_ext src_parent src dest src_p dest_p \<lbrace>\<lambda>_. list_integ P st\<rbrace>" 103 apply (simp add: cap_insert_ext_def split del: if_split) 104 apply (wp update_cdt_list_wp) 105 by (intro impI conjI allI | 106 simp add: list_filter_insert_after list_filter_remove split: option.splits | 107 elim conjE | simp add: list_integ_def)+ 108 109lemma create_cap_list_integrity: 110 notes split_paired_All[simp del] 111 shows 112 "\<lbrace>list_integ P st and K(P dest)\<rbrace> create_cap_ext untyped dest dest_p \<lbrace>\<lambda>_. list_integ P st\<rbrace>" 113 apply (simp add: create_cap_ext_def split del: if_split) 114 apply (wp update_cdt_list_wp) 115 by (intro impI conjI allI | 116 simp add: list_filter_replace list_filter_remove split: option.splits | 117 elim conjE | simp add: list_integ_def)+ 118 119 120lemma empty_slot_list_integrity: 121 notes split_paired_All[simp del] 122 shows 123 "\<lbrace>list_integ P st and (\<lambda>s. valid_list_2 (cdt_list s) m) and K(P slot) and K( all_children P m)\<rbrace> empty_slot_ext slot slot_p \<lbrace>\<lambda>_. list_integ P st\<rbrace>" 124 apply (simp add: empty_slot_ext_def split del: if_split) 125 apply (wp update_cdt_list_wp) 126 apply (intro impI conjI allI | simp add: list_filter_replace_list list_filter_remove split: option.splits | elim conjE | simp add: list_integ_def)+ 127 apply (drule_tac x="the slot_p" in spec) 128 apply (elim disjE) 129 apply (simp add: all_children_def valid_list_2_def list_filter_replace_list)+ 130 done 131 132 133lemma cap_swap_list_integrity: 134 notes split_paired_All[simp del] 135 shows 136 "\<lbrace>list_integ P st and K(P slot1) and K(P slot2)\<rbrace> cap_swap_ext slot1 slot2 slot1_p slot2_p \<lbrace>\<lambda>_. list_integ P st\<rbrace>" 137 apply (simp add: cap_swap_ext_def split del: if_split) 138 apply (wp update_cdt_list_wp) 139 by (intro impI conjI allI | 140 simp add: list_filter_replace list_filter_swap split: option.splits | 141 elim conjE | simp add: list_integ_def)+ (* slow *) 142 143lemma null_filter: "\<forall>x \<in> set list. \<not> P x \<Longrightarrow> list_filter list P = list" 144 apply (induct list,simp+) 145 done 146 147lemma neq_filtered_ex: "list \<noteq> list' \<Longrightarrow> filtered_eq P list list' \<Longrightarrow> \<exists>x \<in> set list \<union> set list'. P x" 148 apply (rule ccontr) 149 apply (simp add: null_filter) 150 done 151 152lemma weaken_filter: "(\<forall>s. P s \<longrightarrow> T s) \<Longrightarrow> filtered_eq T (list_filter list P) list" 153 apply (induct list,simp+) 154 done 155 156lemmas weaken_filter' = weaken_filter[rule_format,rotated] 157 158lemma weaken_filter_eq: "(\<forall>s. P s \<longrightarrow> T s) \<Longrightarrow> filtered_eq P list list' \<Longrightarrow> filtered_eq T list list'" 159 apply (subst weaken_filter[symmetric],assumption) 160 apply (simp add: weaken_filter) 161 done 162 163lemmas weaken_filter_eq' = weaken_filter_eq[rule_format,rotated] 164 165end 166