1 | include "common/Executions.ma". |
---|
2 | include "common/StructuredTraces.ma". (* just for status_class *) |
---|
3 | |
---|
4 | (* A small-step executable semantics, together with some kind of global |
---|
5 | environment, notion of cost labelled state, classification function and |
---|
6 | stack costs. *) |
---|
7 | |
---|
8 | record classified_system : Type[2] ≝ { |
---|
9 | cs_exec :> fullexec io_out io_in; |
---|
10 | cs_global : global … cs_exec; |
---|
11 | cs_labelled : state … cs_exec cs_global → bool; |
---|
12 | cs_classify : state … cs_exec cs_global → status_class; |
---|
13 | cs_stack : ∀s. match cs_classify … s with [ cl_call ⇒ True | cl_return ⇒ True | _ ⇒ False ] → nat |
---|
14 | }. |
---|
15 | |
---|
16 | definition cs_state : classified_system → Type[0] ≝ |
---|
17 | λC. state … C (cs_global … C). |
---|
18 | |
---|
19 | (* Ideally we would also allow measurable traces to be from one cost label to |
---|
20 | another (in the same function call), but due to time constraints we'll stick |
---|
21 | to ending measurable traces at the end of the function only. |
---|
22 | *) |
---|
23 | |
---|
24 | definition trace_is_label_to_return : ∀C. execution_prefix (cs_state … C) → Prop ≝ |
---|
25 | λC,x. ∃tr1,s1,x',tr2,s2,s3. x = 〈tr1,s1〉::(x'@[〈tr2,s2〉;〈E0,s3〉]) ∧ bool_to_Prop (cs_labelled C s1) ∧ cs_classify C s2 = cl_return. |
---|
26 | |
---|
27 | definition measure_stack_aux ≝ |
---|
28 | λC. (λx. λtrs:trace × (cs_state … C). |
---|
29 | let 〈current,max_stack〉 ≝ x in |
---|
30 | let 〈tr,s〉 ≝ trs in |
---|
31 | let new ≝ |
---|
32 | match cs_classify C s return λcl. (match cl in status_class with [_⇒?] → ?) → ? with |
---|
33 | [ cl_call ⇒ λsc. current + sc I |
---|
34 | | cl_return ⇒ λsc. current - sc I |
---|
35 | | _ ⇒ λ_. current |
---|
36 | ] (cs_stack C s) in |
---|
37 | 〈new, max max_stack new〉). |
---|
38 | |
---|
39 | definition measure_stack : ∀C. nat → execution_prefix (cs_state … C) → nat × nat ≝ |
---|
40 | λC,current. |
---|
41 | foldl … (measure_stack_aux C) 〈current,0〉. |
---|
42 | |
---|
43 | definition stack_after : ∀C. nat → execution_prefix (cs_state … C) → nat ≝ |
---|
44 | λC,current,x. \fst (measure_stack C current x). |
---|
45 | |
---|
46 | definition max_stack : ∀C. nat → execution_prefix (cs_state … C) → nat ≝ |
---|
47 | λC,current,x. \snd (measure_stack C current x). |
---|
48 | |
---|
49 | lemma foldl_inv : ∀A,B. ∀P:A → Prop. ∀f. |
---|
50 | (∀acc,el. P acc → P (f acc el)) → |
---|
51 | ∀l,acc. P acc → |
---|
52 | P (foldl A B f acc l). |
---|
53 | #A #B #P #f #IH #l elim l |
---|
54 | [ // |
---|
55 | | #h #t #IH' #acc #H @IH' @IH @H |
---|
56 | ] qed. |
---|
57 | |
---|
58 | lemma max_stack_step : ∀C,a,m,a',m',tr,s. |
---|
59 | measure_stack_aux C 〈a,m〉 〈tr,s〉 = 〈a',m'〉 → |
---|
60 | m' = max m a'. |
---|
61 | #C #a #m #a' #m' #tr #s |
---|
62 | whd in match (measure_stack_aux ???); |
---|
63 | generalize in match (cs_stack C s); cases (cs_classify C s) #f |
---|
64 | normalize nodelta #E destruct // |
---|
65 | qed. |
---|
66 | |
---|
67 | lemma max_stack_step' : ∀C,a,a1',a2',m1,m1',m2,m2',trs. |
---|
68 | measure_stack_aux C 〈a,m1〉 trs = 〈a1',m1'〉 → |
---|
69 | measure_stack_aux C 〈a,m2〉 trs = 〈a2',m2'〉 → |
---|
70 | a1' = a2'. |
---|
71 | #C #a #a1' #a2' #m1 #m2 #m1' #m2' * #tr #s |
---|
72 | whd in match (measure_stack_aux ???); whd in match (measure_stack_aux ???); |
---|
73 | generalize in match (cs_stack C s); cases (cs_classify C s) #f |
---|
74 | normalize nodelta |
---|
75 | #E1 #E2 destruct |
---|
76 | % |
---|
77 | qed. |
---|
78 | |
---|
79 | (* TODO: move*) |
---|
80 | lemma max_O_n : ∀n. max O n = n. |
---|
81 | * // |
---|
82 | qed. |
---|
83 | |
---|
84 | lemma max_n_O : ∀n. max n O = n. |
---|
85 | * // |
---|
86 | qed. |
---|
87 | |
---|
88 | lemma associative_max : associative nat max. |
---|
89 | #n #m #o normalize |
---|
90 | @(leb_elim n m) |
---|
91 | [ normalize @(leb_elim m o) normalize #H1 #H2 |
---|
92 | [ >(le_to_leb_true n o) /2/ |
---|
93 | | >(le_to_leb_true n m) // |
---|
94 | ] |
---|
95 | | normalize @(leb_elim m o) normalize #H1 #H2 |
---|
96 | [ % |
---|
97 | | >(not_le_to_leb_false … H2) |
---|
98 | >(not_le_to_leb_false n o) // @lt_to_not_le @(transitive_lt … m) /2/ |
---|
99 | ] |
---|
100 | ] qed. |
---|
101 | |
---|
102 | |
---|
103 | lemma max_stack_steps : ∀C,trace,a,m. |
---|
104 | \snd (foldl … (measure_stack_aux C) 〈a,m〉 trace) = |
---|
105 | max m (\snd (foldl … (measure_stack_aux C) 〈a,0〉 trace)). |
---|
106 | #C #trace elim trace |
---|
107 | [ #a #m >max_n_O % |
---|
108 | | * #tr #s #tl #IH #a #m |
---|
109 | whd in match (foldl ?????); |
---|
110 | letin x ≝ (measure_stack_aux ???) lapply (refl ? x) cases x in ⊢ (???% → %); #a' #m' #M |
---|
111 | whd in match (foldl ??? 〈a,O〉 ?); |
---|
112 | letin y ≝ (measure_stack_aux ? 〈a,O〉 ?) lapply (refl ? y) cases y in ⊢ (???% → %); #a'' #m'' #M' |
---|
113 | >(IH a'') >IH |
---|
114 | >(max_stack_step … M) |
---|
115 | >(max_stack_step … M') >max_O_n >(max_stack_step' … M M') >associative_max % |
---|
116 | ] qed. |
---|
117 | |
---|
118 | (* |
---|
119 | lemma max_stack_step : ∀C,a,m,tr,s. |
---|
120 | m ≤ \snd (measure_stack_aux C 〈a,m〉 〈tr,s〉). |
---|
121 | #C #a #m #tr #s |
---|
122 | whd in match (measure_stack_aux ???); |
---|
123 | generalize in match (cs_stack C s); cases (cs_classify C s) normalize |
---|
124 | #f @(leb_elim m) normalize #H /2/ |
---|
125 | qed. |
---|
126 | |
---|
127 | lemma max_stack_steps : ∀C. ∀am. ∀trace. |
---|
128 | \snd am ≤ \snd (foldl … (measure_stack_aux C) am trace). |
---|
129 | #C * #a #m #trace |
---|
130 | @foldl_inv |
---|
131 | [ * #a' #m' * #tr #s #H @(transitive_le … H) @max_stack_step |
---|
132 | | // |
---|
133 | ] qed. |
---|
134 | |
---|
135 | lemma max_stack_step' : ∀C,a,m,a',m',tr,s. |
---|
136 | a ≤ a' → m ≤ m' → |
---|
137 | \snd (measure_stack_aux C 〈a,m〉 〈tr,s〉) ≤ \snd (measure_stack_aux C 〈a',m'〉 〈tr,s〉). |
---|
138 | #C #a #m #a' #m' #tr #s #H1 #H2 |
---|
139 | whd in match (measure_stack_aux ???);whd in match (measure_stack_aux ???); |
---|
140 | generalize in match (cs_stack C s); cases (cs_classify C s) #f |
---|
141 | whd in ⊢ (?(??%)(??%)); |
---|
142 | [ @to_max [ @(transitive_le … m') /2/ | @(transitive_le … (a'-f I)) /2/ ] |
---|
143 | | 2,4,5: @to_max /2 by max_r, max_l/ |
---|
144 | | @to_max [ @(transitive_le … m') /2/ | @(transitive_le … (a'+f I)) /2/ ] |
---|
145 | ] qed. |
---|
146 | |
---|
147 | lemma max_stack_step'' : ∀C,a,m,a',m',tr,s. |
---|
148 | a ≤ a' → |
---|
149 | \fst (measure_stack_aux C 〈a,m〉 〈tr,s〉) ≤ \fst (measure_stack_aux C 〈a',m'〉 〈tr,s〉). |
---|
150 | #C #a #m #a' #m' #tr #s #H1 |
---|
151 | whd in match (measure_stack_aux ???);whd in match (measure_stack_aux ???); |
---|
152 | generalize in match (cs_stack C s); cases (cs_classify C s) #f |
---|
153 | whd in ⊢ (?%%); /2/ |
---|
154 | qed. |
---|
155 | |
---|
156 | lemma max_stack_steps' : ∀C. ∀trace,am,am'. |
---|
157 | \fst am ≤ \fst am' → \snd am ≤ \snd am' → |
---|
158 | \snd (foldl … (measure_stack_aux C) am trace) ≤ \snd (foldl … (measure_stack_aux C) am' trace). |
---|
159 | #C #trace elim trace |
---|
160 | [ * #a #m * #a' #m' #H1 #H2 @H2 |
---|
161 | | * #tr #s #tl #IH * #a #m * #a' #m' #H1 #H2 @IH [ @max_stack_step'' // | @max_stack_step' // ] |
---|
162 | ] qed. |
---|
163 | |
---|
164 | lemma max_stack_append_l : ∀C,ex1,ex2. |
---|
165 | max_stack C ex1 ≤ max_stack C (ex1@ex2). |
---|
166 | #C #ex1 #ex2 whd in ⊢ (??%); |
---|
167 | whd in match (measure_stack ? (ex1@ex2)); |
---|
168 | >foldl_append |
---|
169 | @max_stack_steps |
---|
170 | qed. |
---|
171 | |
---|
172 | lemma max_stack_append_r : ∀C,ex1,ex2. |
---|
173 | max_stack C ex2 ≤ max_stack C (ex1@ex2). |
---|
174 | #C #ex1 #ex2 whd in ⊢ (??%); |
---|
175 | whd in match (measure_stack ? (ex1@ex2)); |
---|
176 | >foldl_append |
---|
177 | @max_stack_steps' // |
---|
178 | qed. |
---|
179 | *)(* |
---|
180 | lemma max_stack_append : ∀C,ex1,ex2. |
---|
181 | max (max_stack C ex1) (max_stack C ex2) = max_stack C (ex1@ex2). |
---|
182 | #C #ex1 #ex2 |
---|
183 | whd in match (max_stack ??); whd in match (max_stack ? (ex1@ex2)); |
---|
184 | whd in match (measure_stack ??); whd in match (measure_stack ? (ex1@ex2)); |
---|
185 | generalize in match 〈O,O〉; elim ex1 |
---|
186 | [ * #a #m whd in ⊢ (??(?%?)%); >max_stack_steps |
---|
187 | |
---|
188 | elim ex1 |
---|
189 | [ #ex2 >max_O_n % |
---|
190 | | * #tr #s #tl #IH #ex2 |
---|
191 | whd in match (max_stack ??); whd in match (measure_stack ??); |
---|
192 | lapply (refl ? (measure_stack_aux C 〈O,O〉 〈tr,s〉)) |
---|
193 | cases (measure_stack_aux ???) in ⊢ (???% → %); |
---|
194 | #a #m #M |
---|
195 | |
---|
196 | #ex2 |
---|
197 | @le_to_le_to_eq |
---|
198 | [ @to_max // |
---|
199 | | |
---|
200 | whd in ⊢ (???%); |
---|
201 | |
---|
202 | whd in match (measure_stack ? (ex1@ex2)); |
---|
203 | >foldl_append |
---|
204 | @max_stack_steps' // |
---|
205 | *) |
---|
206 | lemma max_stack_append : ∀C,c1,ex1,ex2. |
---|
207 | max (max_stack C c1 ex1) (max_stack C (stack_after C c1 ex1) ex2) = max_stack C c1 (ex1@ex2). |
---|
208 | #C #c1 #ex1 #ex2 |
---|
209 | whd in match (max_stack ???); whd in match (stack_after ???); |
---|
210 | whd in match (max_stack ?? (ex1@ex2)); |
---|
211 | whd in match (measure_stack ???); whd in match (measure_stack ?? (ex1@ex2)); |
---|
212 | generalize in match O; generalize in match c1; elim ex1 |
---|
213 | [ #c #m whd in ⊢ (??(?%?)%); >max_stack_steps % |
---|
214 | | * #tr #s #tl #IH #c #m |
---|
215 | whd in match (foldl ?????); whd in ⊢ (???(???%)); |
---|
216 | lapply (refl ? (measure_stack_aux C 〈c1,m〉 〈tr,s〉)) |
---|
217 | cases (measure_stack_aux ???) in ⊢ (???% → %); #a' #m' #M |
---|
218 | >IH % |
---|
219 | ] qed. |
---|
220 | |
---|
221 | |
---|
222 | (* Check that the trace ends with the return from the starting function and one |
---|
223 | further state. *) |
---|
224 | |
---|
225 | let rec will_return_aux C (depth:nat) |
---|
226 | (trace:execution_prefix (cs_state … C)) on trace : bool ≝ |
---|
227 | match trace with |
---|
228 | [ nil ⇒ false |
---|
229 | | cons h tl ⇒ |
---|
230 | let 〈tr,s〉 ≝ h in |
---|
231 | match cs_classify C s with |
---|
232 | [ cl_call ⇒ will_return_aux C (S depth) tl |
---|
233 | | cl_return ⇒ |
---|
234 | match depth with |
---|
235 | (* We need to see the state after the return to build the structured |
---|
236 | trace. *) |
---|
237 | [ O ⇒ match tl with [ cons _ tl' ⇒ match tl' with [ nil ⇒ true | _ ⇒ false ] | _ ⇒ false ] |
---|
238 | | S d ⇒ will_return_aux C d tl |
---|
239 | ] |
---|
240 | | _ ⇒ will_return_aux C depth tl |
---|
241 | ] |
---|
242 | ]. |
---|
243 | definition will_return' : ∀C. execution_prefix (cs_state … C) → bool ≝ λC. will_return_aux C O. |
---|
244 | |
---|
245 | (* Like classified_system, but we don't fix the global environment so that we |
---|
246 | talk about the program separately. *) |
---|
247 | |
---|
248 | record preclassified_system : Type[2] ≝ { |
---|
249 | pcs_exec :> fullexec io_out io_in; |
---|
250 | pcs_labelled : ∀g. state … pcs_exec g → bool; |
---|
251 | pcs_classify : ∀g. state … pcs_exec g → status_class; |
---|
252 | pcs_stack : (ident → nat) → ∀g,s. match pcs_classify g s with [ cl_call ⇒ True | cl_return ⇒ True | _ ⇒ False ] → nat |
---|
253 | }. |
---|
254 | |
---|
255 | definition pcs_to_cs : ∀C:preclassified_system. global … C → (ident → nat) → classified_system ≝ |
---|
256 | λC,g,stack_cost. |
---|
257 | mk_classified_system (pcs_exec C) g (pcs_labelled C ?) (pcs_classify C ?) (pcs_stack C stack_cost ?). |
---|
258 | |
---|
259 | (* FIXME: this definition is unreasonable because it presumes we can easily |
---|
260 | identify the change in stack usage from return states, but that information |
---|
261 | is rather implicit (we only really record the function called in the |
---|
262 | extended RTLabs states when building the structured traces). *) |
---|
263 | |
---|
264 | definition measurable : ∀C:preclassified_system. |
---|
265 | ∀p:program ?? C. nat → nat → |
---|
266 | (ident → nat) (* stack cost *) → |
---|
267 | nat → Prop ≝ |
---|
268 | λC,p,m,n,stack_cost,max_allowed_stack. ∃s0,prefix,s1,interesting,s2. |
---|
269 | let g ≝ make_global … (pcs_exec … C) p in |
---|
270 | let C' ≝ pcs_to_cs C g stack_cost in |
---|
271 | make_initial_state … p = OK ? s0 ∧ |
---|
272 | exec_steps m ?? (cs_exec … C') g s0 = OK ? 〈prefix,s1〉 ∧ |
---|
273 | exec_steps n ?? (cs_exec … C') g s1 = OK ? 〈interesting,s2〉 ∧ |
---|
274 | trace_is_label_to_return C' interesting ∧ |
---|
275 | bool_to_Prop (will_return' C' interesting) ∧ |
---|
276 | le (max_stack C' 0 (prefix@interesting)) max_allowed_stack. |
---|
277 | |
---|
278 | (* TODO: probably ought to be elsewhere; use exec_steps instead |
---|
279 | |
---|
280 | Note that this does not include stack space |
---|
281 | *) |
---|
282 | |
---|
283 | definition observables : ∀FE:fullexec io_out io_in. program … FE → nat → nat → option ((list trace) × (list trace)) ≝ |
---|
284 | λFE,p,m,n. |
---|
285 | let trace ≝ exec_inf … FE p in |
---|
286 | match split_trace … trace m with |
---|
287 | [ Some x ⇒ |
---|
288 | let 〈prefix,suffix〉 ≝ x in |
---|
289 | match split_trace … suffix n with |
---|
290 | [ Some y ⇒ |
---|
291 | let interesting ≝ \fst y in |
---|
292 | Some ? 〈map … (fst ??) prefix, map … (fst ??) interesting〉 |
---|
293 | | _ ⇒ None ? |
---|
294 | ] |
---|
295 | | _ ⇒ None ? |
---|
296 | ]. |
---|
297 | |
---|
298 | definition state_at : ∀FE:fullexec io_out io_in. ∀p:program … FE. nat → option (state … FE (make_global … p)) ≝ |
---|
299 | λFE,p,m. |
---|
300 | let trace ≝ exec_inf … FE p in |
---|
301 | match split_trace … trace m with |
---|
302 | [ Some x ⇒ |
---|
303 | match \snd x with |
---|
304 | [ e_step _ s _ ⇒ Some ? s |
---|
305 | | e_stop _ _ s ⇒ Some ? s |
---|
306 | | _ ⇒ None ? |
---|
307 | ] |
---|
308 | | _ ⇒ None ? |
---|
309 | ]. |
---|