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