1 (* Title: ZF/UNITY/Client.ML |
|
2 ID: $Id$ |
|
3 Author: Sidi O Ehmety, Cambridge University Computer Laboratory |
|
4 Copyright 2002 University of Cambridge |
|
5 |
|
6 Distributed Resource Management System: the Client |
|
7 *) |
|
8 Addsimps [type_assumes, default_val_assumes]; |
|
9 (* This part should be automated *) |
|
10 |
|
11 Goalw [state_def] "s \\<in> state ==> s`ask \\<in> list(nat)"; |
|
12 by (dres_inst_tac [("a", "ask")] apply_type 1); |
|
13 by Auto_tac; |
|
14 qed "ask_value_type"; |
|
15 AddTCs [ask_value_type]; |
|
16 Addsimps [ask_value_type]; |
|
17 |
|
18 Goalw [state_def] "s \\<in> state ==> s`giv \\<in> list(nat)"; |
|
19 by (dres_inst_tac [("a", "giv")] apply_type 1); |
|
20 by Auto_tac; |
|
21 qed "giv_value_type"; |
|
22 AddTCs [giv_value_type]; |
|
23 Addsimps [giv_value_type]; |
|
24 |
|
25 Goalw [state_def] |
|
26 "s \\<in> state ==> s`rel \\<in> list(nat)"; |
|
27 by (dres_inst_tac [("a", "rel")] apply_type 1); |
|
28 by Auto_tac; |
|
29 qed "rel_value_type"; |
|
30 AddTCs [rel_value_type]; |
|
31 Addsimps [rel_value_type]; |
|
32 |
|
33 Goalw [state_def] "s \\<in> state ==> s`tok \\<in> nat"; |
|
34 by (dres_inst_tac [("a", "tok")] apply_type 1); |
|
35 by Auto_tac; |
|
36 qed "tok_value_type"; |
|
37 AddTCs [tok_value_type]; |
|
38 Addsimps [tok_value_type]; |
|
39 |
|
40 (** The Client Program **) |
|
41 |
|
42 Goalw [client_prog_def] "client_prog \\<in> program"; |
|
43 by (Simp_tac 1); |
|
44 qed "client_type"; |
|
45 Addsimps [client_type]; |
|
46 AddTCs [client_type]; |
|
47 |
|
48 Addsimps [client_prog_def RS def_prg_Init, |
|
49 client_prog_def RS def_prg_AllowedActs]; |
|
50 program_defs_ref := [client_prog_def]; |
|
51 |
|
52 Addsimps (map simp_of_act [client_rel_act_def, |
|
53 client_tok_act_def, client_ask_act_def]); |
|
54 |
|
55 Goal "\\<forall>G \\<in> program. (client_prog ok G) <-> \ |
|
56 \ (G \\<in> preserves(lift(rel)) & G \\<in> preserves(lift(ask)) & \ |
|
57 \ G \\<in> preserves(lift(tok)) & client_prog \\<in> Allowed(G))"; |
|
58 by (auto_tac (claset(), |
|
59 simpset() addsimps [ok_iff_Allowed, client_prog_def RS def_prg_Allowed])); |
|
60 qed "client_prog_ok_iff"; |
|
61 |
|
62 Goal "client_prog:(\\<Inter>x \\<in> var-{ask, rel, tok}. preserves(lift(x)))"; |
|
63 by (rtac Inter_var_DiffI 1); |
|
64 by (rtac ballI 2); |
|
65 by (rtac preservesI 2); |
|
66 by (constrains_tac 2); |
|
67 by Auto_tac; |
|
68 qed "client_prog_preserves"; |
|
69 |
|
70 |
|
71 (*Safety property 1: ask, rel are increasing : (24) *) |
|
72 Goalw [guar_def] |
|
73 "client_prog: program guarantees Incr(lift(ask)) Int Incr(lift(rel))"; |
|
74 by (auto_tac (claset() addSIs [increasing_imp_Increasing], |
|
75 simpset() addsimps [client_prog_ok_iff, increasing_def])); |
|
76 by (ALLGOALS(constrains_tac)); |
|
77 by (ALLGOALS(thin_tac "mk_program(?u, ?v, ?w):Allowed(?x)")); |
|
78 by (auto_tac (claset() addDs [ActsD], simpset())); |
|
79 by (dres_inst_tac [("f", "lift(rel)")] preserves_imp_eq 2); |
|
80 by (dres_inst_tac [("f", "lift(ask)")] preserves_imp_eq 1); |
|
81 by (TRYALL(assume_tac)); |
|
82 by (ALLGOALS(dtac ActsD)); |
|
83 by (TRYALL(assume_tac)); |
|
84 by (ALLGOALS(Clarify_tac)); |
|
85 by (ALLGOALS(rotate_tac ~2)); |
|
86 by Auto_tac; |
|
87 qed "client_prog_Increasing_ask_rel"; |
|
88 |
|
89 Addsimps [nth_append, append_one_prefix]; |
|
90 |
|
91 Goal "0<NbT"; |
|
92 by (cut_facts_tac [NbT_pos] 1); |
|
93 by (resolve_tac [Ord_0_lt] 1); |
|
94 by Auto_tac; |
|
95 qed "NbT_pos2"; |
|
96 |
|
97 (*Safety property 2: the client never requests too many tokens. |
|
98 With no Substitution Axiom, we must prove the two invariants simultaneously. *) |
|
99 |
|
100 Goal |
|
101 "[| client_prog ok G; G \\<in> program |]\ |
|
102 \ ==> client_prog Join G : \ |
|
103 \ Always({s \\<in> state. s`tok le NbT} Int \ |
|
104 \ {s \\<in> state. \\<forall>elt \\<in> set_of_list(s`ask). elt le NbT})"; |
|
105 by (rotate_tac ~1 1); |
|
106 by (auto_tac (claset(), simpset() addsimps [client_prog_ok_iff])); |
|
107 by (rtac (invariantI RS stable_Join_Always2) 1); |
|
108 by (ALLGOALS(Clarify_tac)); |
|
109 by (ALLGOALS(Asm_full_simp_tac)); |
|
110 by (rtac stable_Int 2); |
|
111 by (dres_inst_tac [("f", "lift(ask)")] preserves_imp_stable 3); |
|
112 by (dres_inst_tac [("f", "lift(tok)")] preserves_imp_stable 2); |
|
113 by (REPEAT(Force_tac 2)); |
|
114 by (constrains_tac 1); |
|
115 by (auto_tac (claset() addDs [ActsD], simpset())); |
|
116 by (cut_facts_tac [NbT_pos] 1); |
|
117 by (resolve_tac [NbT_pos2 RS mod_less_divisor] 1); |
|
118 by (auto_tac (claset() addDs [ActsD, preserves_imp_eq], |
|
119 simpset() addsimps [set_of_list_append])); |
|
120 qed "ask_Bounded_lemma"; |
|
121 |
|
122 (* Export version, with no mention of tok in the postcondition, but |
|
123 unfortunately tok must be declared local.*) |
|
124 Goal |
|
125 "client_prog \\<in> program guarantees \ |
|
126 \ Always({s \\<in> state. \\<forall>elt \\<in> set_of_list(s`ask). elt le NbT})"; |
|
127 by (rtac guaranteesI 1); |
|
128 by (etac (ask_Bounded_lemma RS Always_weaken) 1); |
|
129 by Auto_tac; |
|
130 qed "client_prog_ask_Bounded"; |
|
131 |
|
132 (*** Towards proving the liveness property ***) |
|
133 |
|
134 Goal |
|
135 "client_prog \\<in> stable({s \\<in> state. <s`rel, s`giv>:prefix(nat)})"; |
|
136 by (constrains_tac 1); |
|
137 by Auto_tac; |
|
138 qed "client_prog_stable_rel_le_giv"; |
|
139 |
|
140 Goal |
|
141 "[| client_prog Join G \\<in> Incr(lift(giv)); G \\<in> preserves(lift(rel)) |] \ |
|
142 \ ==> client_prog Join G \\<in> Stable({s \\<in> state. <s`rel, s`giv>:prefix(nat)})"; |
|
143 by (rtac (client_prog_stable_rel_le_giv RS Increasing_preserves_Stable) 1); |
|
144 by (auto_tac (claset(), simpset() addsimps [lift_def])); |
|
145 qed "client_prog_Join_Stable_rel_le_giv"; |
|
146 |
|
147 Goal "[| client_prog Join G \\<in> Incr(lift(giv)); G \\<in> preserves(lift(rel)) |] \ |
|
148 \ ==> client_prog Join G \\<in> Always({s \\<in> state. <s`rel, s`giv>:prefix(nat)})"; |
|
149 by (force_tac (claset() addSIs [AlwaysI, client_prog_Join_Stable_rel_le_giv], |
|
150 simpset()) 1); |
|
151 qed "client_prog_Join_Always_rel_le_giv"; |
|
152 |
|
153 Goal "xs \\<in> list(A) ==> xs@[a]=xs --> False"; |
|
154 by (etac list.induct 1); |
|
155 by Auto_tac; |
|
156 qed "list_app_lemma"; |
|
157 |
|
158 Goal "A == {<s, t>:state*state. P(s, t)} ==> A={<s, t>:state*state. P(s, t)}"; |
|
159 by Auto_tac; |
|
160 qed "def_act_eq"; |
|
161 |
|
162 Goal "A={<s,t>:state*state. P(s, t)} ==> A<=state*state"; |
|
163 by Auto_tac; |
|
164 qed "act_subset"; |
|
165 |
|
166 Goal |
|
167 "client_prog \\<in> \ |
|
168 \ transient({s \\<in> state. s`rel = k & <k, h>:strict_prefix(nat) \ |
|
169 \ & <h, s`giv>:prefix(nat) & h pfixGe s`ask})"; |
|
170 by (res_inst_tac [("act", "client_rel_act")] transientI 1); |
|
171 by (simp_tac (simpset() addsimps |
|
172 [client_prog_def RS def_prg_Acts]) 1); |
|
173 by (simp_tac (simpset() addsimps |
|
174 [client_rel_act_def RS def_act_eq RS act_subset]) 1); |
|
175 by (auto_tac (claset(), |
|
176 simpset() addsimps [client_prog_def RS def_prg_Acts,domain_def])); |
|
177 by (resolve_tac [ReplaceI] 1); |
|
178 by (res_inst_tac [("x", "x(rel:= x`rel @\ |
|
179 \ [nth(length(x`rel), x`giv)])")] exI 1); |
|
180 by (auto_tac (claset() addSIs [state_update_type, |
|
181 app_type, length_type, nth_type], |
|
182 simpset())); |
|
183 by Auto_tac; |
|
184 by (blast_tac (claset() addIs [lt_trans2, prefix_length_le, |
|
185 strict_prefix_length_lt]) 1); |
|
186 by (blast_tac (claset() addIs [lt_trans2, prefix_length_le, |
|
187 strict_prefix_length_lt]) 1); |
|
188 by (full_simp_tac (simpset() addsimps [gen_prefix_iff_nth]) 1); |
|
189 by (ALLGOALS(subgoal_tac "h \\<in> list(nat)")); |
|
190 by (ALLGOALS(asm_simp_tac (simpset() addsimps [prefix_type RS subsetD RS SigmaD1]))); |
|
191 by (auto_tac (claset(), |
|
192 simpset() addsimps [prefix_def, Ge_def])); |
|
193 by (dtac strict_prefix_length_lt 1); |
|
194 by (dres_inst_tac [("x", "length(x`rel)")] spec 1); |
|
195 by Auto_tac; |
|
196 by (full_simp_tac (simpset() addsimps [gen_prefix_iff_nth]) 1); |
|
197 by (auto_tac (claset(), simpset() addsimps [id_def, lam_def])); |
|
198 qed "transient_lemma"; |
|
199 |
|
200 Goalw [strict_prefix_def,id_def, lam_def] |
|
201 "<xs, ys>:strict_prefix(A) <-> <xs, ys>:prefix(A) & xs~=ys"; |
|
202 by (auto_tac (claset() addDs [prefix_type RS subsetD], simpset())); |
|
203 qed "strict_prefix_is_prefix"; |
|
204 |
|
205 Goal |
|
206 "[| client_prog Join G \\<in> Incr(lift(giv)); client_prog ok G; G \\<in> program |] \ |
|
207 \ ==> client_prog Join G \\<in> \ |
|
208 \ {s \\<in> state. s`rel = k & <k,h>:strict_prefix(nat) \ |
|
209 \ & <h , s`giv>:prefix(nat) & h pfixGe s`ask} \ |
|
210 \ LeadsTo {s \\<in> state. <k, s`rel>:strict_prefix(nat) \ |
|
211 \ & <s`rel, s`giv>:prefix(nat) & \ |
|
212 \ <h, s`giv>:prefix(nat) & \ |
|
213 \ h pfixGe s`ask}"; |
|
214 by (rtac single_LeadsTo_I 1); |
|
215 by (Asm_simp_tac 2); |
|
216 by (ftac (client_prog_Increasing_ask_rel RS guaranteesD) 1); |
|
217 by (rotate_tac 2 3); |
|
218 by (auto_tac (claset(), simpset() addsimps [client_prog_ok_iff])); |
|
219 by (rtac (transient_lemma RS Join_transient_I1 RS transient_imp_leadsTo RS |
|
220 leadsTo_imp_LeadsTo RS PSP_Stable RS LeadsTo_weaken) 1); |
|
221 by (rtac (Stable_Int RS Stable_Int RS Stable_Int) 1); |
|
222 by (eres_inst_tac [("f", "lift(giv)"), ("a", "s`giv")] Increasing_imp_Stable 1); |
|
223 by (Asm_simp_tac 1); |
|
224 by (eres_inst_tac [("f", "lift(ask)"), ("a", "s`ask")] Increasing_imp_Stable 1); |
|
225 by (Asm_simp_tac 1); |
|
226 by (eres_inst_tac [("f", "lift(rel)"), ("a", "s`rel")] Increasing_imp_Stable 1); |
|
227 by (Asm_simp_tac 1); |
|
228 by (etac client_prog_Join_Stable_rel_le_giv 1); |
|
229 by (Blast_tac 1); |
|
230 by (Asm_simp_tac 1); |
|
231 by (Asm_simp_tac 2); |
|
232 by (blast_tac (claset() addIs [sym, strict_prefix_is_prefix RS iffD2, |
|
233 prefix_trans, prefix_imp_pfixGe, |
|
234 pfixGe_trans]) 2); |
|
235 by (auto_tac (claset() addIs [strict_prefix_is_prefix RS iffD1 RS conjunct1, |
|
236 prefix_trans], simpset())); |
|
237 qed "induct_lemma"; |
|
238 |
|
239 Goal |
|
240 "[| client_prog Join G \\<in> Incr(lift(giv)); client_prog ok G; G \\<in> program |] \ |
|
241 \ ==> client_prog Join G \\<in> \ |
|
242 \ {s \\<in> state. <s`rel, h>:strict_prefix(nat) \ |
|
243 \ & <h, s`giv>:prefix(nat) & h pfixGe s`ask} \ |
|
244 \ LeadsTo {s \\<in> state. <h, s`rel>:prefix(nat)}"; |
|
245 by (res_inst_tac [("f", "\\<lambda>x \\<in> state. length(h) #- length(x`rel)")] |
|
246 LessThan_induct 1); |
|
247 by (auto_tac (claset(), simpset() addsimps [vimage_def])); |
|
248 by (rtac single_LeadsTo_I 1); |
|
249 by (rtac (induct_lemma RS LeadsTo_weaken) 1); |
|
250 by Auto_tac; |
|
251 by (resolve_tac [imageI] 3); |
|
252 by (resolve_tac [converseI] 3); |
|
253 by (asm_simp_tac (simpset() addsimps [lam_def]) 3); |
|
254 by (asm_simp_tac (simpset() addsimps [length_type]) 3); |
|
255 by (etac swap 2); |
|
256 by (resolve_tac [imageI] 2); |
|
257 by (resolve_tac [converseI] 2); |
|
258 by (asm_full_simp_tac (simpset() addsimps [lam_def]) 2); |
|
259 by (REPEAT (dtac strict_prefix_length_lt 2)); |
|
260 by (asm_full_simp_tac (simpset() addsimps [length_type, lam_def]) 2); |
|
261 by (ALLGOALS(subgoal_tac "h \\<in> list(nat)")); |
|
262 by (ALLGOALS(asm_simp_tac (simpset() addsimps [prefix_type RS subsetD RS SigmaD1]))); |
|
263 by (dtac less_imp_succ_add 2); |
|
264 by (dtac less_imp_succ_add 3); |
|
265 by (ALLGOALS(Clarify_tac)); |
|
266 by (ALLGOALS(Asm_simp_tac)); |
|
267 by (etac (diff_le_self RS ltD) 2); |
|
268 by (asm_full_simp_tac (simpset() addsimps [length_type, lam_def]) 1); |
|
269 by (auto_tac (claset() addIs [strict_prefix_is_prefix RS iffD2] |
|
270 addDs [rotate_prems 2 common_prefix_linear, |
|
271 prefix_type RS subsetD], simpset())); |
|
272 qed "rel_progress_lemma"; |
|
273 |
|
274 Goal |
|
275 "[| client_prog Join G \\<in> Incr(lift(giv)); client_prog ok G; G \\<in> program |] ==> \ |
|
276 \ client_prog Join G \\<in> \ |
|
277 \ {s \\<in> state. <h, s`giv>:prefix(nat) & h pfixGe s`ask} \ |
|
278 \ LeadsTo {s \\<in> state. <h, s`rel>:prefix(nat)}"; |
|
279 by (rtac (client_prog_Join_Always_rel_le_giv RS Always_LeadsToI) 1); |
|
280 by (rtac ([rel_progress_lemma, subset_refl RS subset_imp_LeadsTo] MRS |
|
281 LeadsTo_Un RS LeadsTo_weaken_L) 3); |
|
282 by Auto_tac; |
|
283 by (auto_tac (claset() addIs [strict_prefix_is_prefix RS iffD2] |
|
284 addDs [rotate_prems 3 common_prefix_linear, |
|
285 prefix_type RS subsetD], simpset())); |
|
286 by (rotate_tac ~1 1); |
|
287 by (force_tac (claset(), simpset() addsimps [client_prog_ok_iff]) 1); |
|
288 qed "progress_lemma"; |
|
289 |
|
290 (*Progress property: all tokens that are given will be released*) |
|
291 Goal |
|
292 "client_prog \\<in> Incr(lift(giv)) guarantees \ |
|
293 \ (\\<Inter>h \\<in> list(nat). {s \\<in> state. <h, s`giv>:prefix(nat) &\ |
|
294 \ h pfixGe s`ask} LeadsTo {s \\<in> state. <h, s`rel>:prefix(nat)})"; |
|
295 by (rtac guaranteesI 1); |
|
296 by (Clarify_tac 1); |
|
297 by (blast_tac (claset() addIs [progress_lemma]) 1); |
|
298 by Auto_tac; |
|
299 qed "client_prog_progress"; |
|
300 |
|
301 Goal "Allowed(client_prog) = \ |
|
302 \ preserves(lift(rel)) Int preserves(lift(ask)) Int preserves(lift(tok))"; |
|
303 by (cut_facts_tac [inst "v" "lift(ask)" preserves_type] 1); |
|
304 by (auto_tac (claset(), |
|
305 simpset() addsimps [Allowed_def, |
|
306 client_prog_def RS def_prg_Allowed, |
|
307 cons_Int_distrib, safety_prop_Acts_iff])); |
|
308 qed "client_prog_Allowed"; |
|
309 |
|