1 | include "utilities/extralib.ma". |
---|
2 | include "common/IOMonad.ma". |
---|
3 | include "common/Integers.ma". |
---|
4 | include "common/Events.ma". |
---|
5 | |
---|
6 | record trans_system (outty:Type[0]) (inty:outty → Type[0]) : Type[2] ≝ |
---|
7 | { global : Type[1] |
---|
8 | ; state : global → Type[0] |
---|
9 | ; is_final : ∀g. state g → option int |
---|
10 | ; step : ∀g. state g → IO outty inty (trace×(state g)) |
---|
11 | }. |
---|
12 | |
---|
13 | let rec repeat (n:nat) (outty:Type[0]) (inty:outty → Type[0]) (exec:trans_system outty inty) |
---|
14 | (g:global ?? exec) (s:state ?? exec g) |
---|
15 | : IO outty inty (trace × (state ?? exec g)) ≝ |
---|
16 | match n with |
---|
17 | [ O ⇒ Value ??? 〈E0, s〉 |
---|
18 | | S n' ⇒ ! 〈t1,s1〉 ← step ?? exec g s; |
---|
19 | ! 〈tn,sn〉 ← repeat n' ?? exec g s1; |
---|
20 | Value ??? 〈t1⧺tn,sn〉 |
---|
21 | ]. |
---|
22 | |
---|
23 | (* We take care here to check that we're not at the final state. It is not |
---|
24 | necessarily the case that a success step guarantees this (e.g., because |
---|
25 | there may be no way to stop a processor, so an infinite loop is used |
---|
26 | instead). *) |
---|
27 | inductive plus (O) (I) (TS:trans_system O I) (ge:global … TS) : state … TS ge → trace → state … TS ge → Prop ≝ |
---|
28 | | plus_one : ∀s1,tr,s2. |
---|
29 | is_final … TS ge s1 = None ? → |
---|
30 | step … TS ge s1 = OK … 〈tr,s2〉 → |
---|
31 | plus … ge s1 tr s2 |
---|
32 | | plus_succ : ∀s1,tr,s2,tr',s3. |
---|
33 | is_final … TS ge s1 = None ? → |
---|
34 | step … TS ge s1 = OK … 〈tr,s2〉 → |
---|
35 | plus … ge s2 tr' s3 → |
---|
36 | plus … ge s1 (tr⧺tr') s3. |
---|
37 | |
---|
38 | lemma plus_not_final : ∀O,I,FE. ∀gl,s,tr,s'. |
---|
39 | plus O I FE gl s tr s' → |
---|
40 | is_final … FE gl s = None ?. |
---|
41 | #O #I #FE #gl #s0 #tr0 #s0' * // |
---|
42 | qed. |
---|
43 | |
---|
44 | let rec trace_map (A,B:Type[0]) (f:A → res (trace × B)) |
---|
45 | (l:list A) on l : res (trace × (list B)) ≝ |
---|
46 | match l with |
---|
47 | [ nil ⇒ OK ? 〈E0, [ ]〉 |
---|
48 | | cons h t ⇒ |
---|
49 | do 〈tr,h'〉 ← f h; |
---|
50 | do 〈tr',t'〉 ← trace_map … f t; |
---|
51 | OK ? 〈tr ⧺ tr',h'::t'〉 |
---|
52 | ]. |
---|
53 | |
---|
54 | (* A third version of making several steps (!) |
---|
55 | |
---|
56 | The idea here is to have a computational definition of reducing serveral |
---|
57 | steps then showing some property about the resulting trace and state. By |
---|
58 | careful use of let rec we can ensure that reduction stops in a sensible |
---|
59 | way whenever the number of steps or the step currently being executed is |
---|
60 | not (reducible to) a value. |
---|
61 | |
---|
62 | An invariant is also asserted on every state other than the initial one. |
---|
63 | |
---|
64 | For example, we state a property to prove by something like |
---|
65 | |
---|
66 | ∃n. after_n_steps n … clight_exec ge s inv (λtr,s'. <some property>) |
---|
67 | |
---|
68 | then start reducing by giving the number of steps and reducing the |
---|
69 | definition |
---|
70 | |
---|
71 | %{3} whd |
---|
72 | |
---|
73 | and then whenever the reduction gets stuck, the currently reducing step is |
---|
74 | the third subterm, which we can reduce and unblock with (for example) |
---|
75 | rewriting |
---|
76 | |
---|
77 | whd in ⊢ (??%?); >EXe' |
---|
78 | |
---|
79 | and at the end reduce with whd to get the property as the goal. |
---|
80 | |
---|
81 | There are a few inversion-like results to get back the information contained in |
---|
82 | the proof below, and other that provides all the steps in an inductive form |
---|
83 | in Executions.ma. |
---|
84 | |
---|
85 | *) |
---|
86 | |
---|
87 | record await_value_stuff : Type[2] ≝ { |
---|
88 | avs_O : Type[0]; |
---|
89 | avs_I : avs_O → Type[0]; |
---|
90 | avs_exec : trans_system avs_O avs_I; |
---|
91 | avs_g : global ?? avs_exec; |
---|
92 | avs_inv : state ?? avs_exec avs_g → bool |
---|
93 | }. |
---|
94 | |
---|
95 | let rec await_value (avs:await_value_stuff) |
---|
96 | (v:IO (avs_O avs) (avs_I avs) (trace × (state ?? (avs_exec avs) (avs_g avs)))) |
---|
97 | (P:trace → state ?? (avs_exec avs) (avs_g avs) → Prop) on v : Prop ≝ |
---|
98 | match v with |
---|
99 | [ Value ts ⇒ P (\fst ts) (\snd ts) |
---|
100 | | _ ⇒ False |
---|
101 | ]. |
---|
102 | |
---|
103 | let rec assert (b:bool) (P:Prop) on b ≝ |
---|
104 | if b then P else False. |
---|
105 | |
---|
106 | let rec after_aux (avs:await_value_stuff) |
---|
107 | (n:nat) (s:state ?? (avs_exec avs) (avs_g avs)) (tr:trace) |
---|
108 | (P:trace → state ?? (avs_exec avs) (avs_g avs) → Prop) |
---|
109 | on n : Prop ≝ |
---|
110 | match n with |
---|
111 | [ O ⇒ P tr s |
---|
112 | | S n' ⇒ |
---|
113 | match is_final … s with |
---|
114 | [ None ⇒ |
---|
115 | await_value avs (step ?? (avs_exec avs) (avs_g avs) s) (λtr',s. |
---|
116 | assert (avs_inv avs s) (after_aux avs n' s (tr ⧺ tr') P)) |
---|
117 | | _ ⇒ False |
---|
118 | ] |
---|
119 | ]. |
---|
120 | |
---|
121 | definition after_n_steps : nat → |
---|
122 | ∀O,I. ∀exec:trans_system O I. ∀g:global ?? exec. |
---|
123 | state ?? exec g → |
---|
124 | (state ?? exec g → bool) → |
---|
125 | (trace → state ?? exec g → Prop) → Prop ≝ |
---|
126 | λn,O,I,exec,g,s,inv,P. after_aux (mk_await_value_stuff O I exec g inv) n s E0 P. |
---|
127 | |
---|
128 | lemma after_aux_covariant : ∀avs,P,Q,tr'. |
---|
129 | (∀tr,s. P (tr'⧺tr) s → Q tr s) → |
---|
130 | ∀n,s,tr. |
---|
131 | after_aux avs n s (tr'⧺tr) P → |
---|
132 | after_aux avs n s tr Q. |
---|
133 | #avs #P #Q #tr' #H #n elim n |
---|
134 | [ normalize /2/ |
---|
135 | | #n' #IH #s #tr |
---|
136 | whd in ⊢ (% → %); cases (is_final … s) [ 2: #x * ] |
---|
137 | whd in ⊢ (% → %); |
---|
138 | cases (step … s) [1,3: normalize /2/ ] |
---|
139 | * #tr'' #s'' |
---|
140 | whd in ⊢ (% → %); |
---|
141 | cases (avs_inv avs s'') [ 2: * ] |
---|
142 | whd in ⊢ (% → %); |
---|
143 | >Eapp_assoc @IH |
---|
144 | ] qed. |
---|
145 | |
---|
146 | lemma after_n_covariant : ∀n,O,I,exec,g,P,inv,Q. |
---|
147 | (∀tr,s. P tr s → Q tr s) → |
---|
148 | ∀s. |
---|
149 | after_n_steps n O I exec g s inv P → |
---|
150 | after_n_steps n O I exec g s inv Q. |
---|
151 | normalize /3/ |
---|
152 | qed. |
---|
153 | |
---|
154 | (* for joining a couple of these together *) |
---|
155 | |
---|
156 | lemma after_n_m : ∀n,m,O,I,exec,g,inv,P,Q,s,s'. |
---|
157 | after_n_steps m O I exec g s' inv Q → |
---|
158 | after_n_steps n O I exec g s inv (λtr1,s1. s' = s1 ∧ (∀tr'',s''. Q tr'' s'' → P (tr1⧺tr'') s'')) → |
---|
159 | after_n_steps (n+m) O I exec g s inv P. |
---|
160 | #n #m #O #I #exec #g #inv #P #Q whd in ⊢ (? → ? → ? → % → %); generalize in match E0; elim n |
---|
161 | [ #tr #s #s' #H whd in ⊢ (% → %); * #E destruct #H2 |
---|
162 | whd in H; <(E0_right tr) generalize in match E0 in H ⊢ %; |
---|
163 | generalize in match s; -s |
---|
164 | elim m |
---|
165 | [ #s #tr' whd in ⊢ (% → %); @H2 |
---|
166 | | #m' #IH #s #tr' whd in ⊢ (% → %); |
---|
167 | cases (is_final … s) [2: #r * ] |
---|
168 | whd in ⊢ (% → %); |
---|
169 | cases (step O I exec g s) [1,3: normalize //] * #tr'' #s'' whd in ⊢ (% → %); |
---|
170 | cases (inv s'') [2: * ] |
---|
171 | >Eapp_assoc @IH ] |
---|
172 | | #n' #IH #tr #s #s' #H whd in ⊢ (% → %); |
---|
173 | cases (is_final … s) [2: #r * ] |
---|
174 | whd in ⊢ (% → %); |
---|
175 | cases (step O I exec g s) [1,3: normalize // ] |
---|
176 | * #tr1 #s1 whd in ⊢ (% → %); |
---|
177 | cases (inv s1) [2:*] |
---|
178 | @IH @H |
---|
179 | ] qed. |
---|
180 | |
---|
181 | (* Inversion lemmas. *) |
---|
182 | |
---|
183 | lemma after_1_of_n_steps : ∀n,O,I,exec,g,inv,P,s. |
---|
184 | after_n_steps (S n) O I exec g s inv P → |
---|
185 | ∃tr,s'. |
---|
186 | is_final … exec g s = None ? ∧ |
---|
187 | step … exec g s = Value … 〈tr,s'〉 ∧ |
---|
188 | bool_to_Prop (inv s') ∧ |
---|
189 | after_n_steps n O I exec g s' inv (λtr'',s''. P (tr⧺tr'') s''). |
---|
190 | #n #O #I #exec #g #inv #P #s |
---|
191 | whd in ⊢ (% → ?); |
---|
192 | cases (is_final … s) |
---|
193 | [ whd in ⊢ (% → ?); |
---|
194 | cases (step … s) |
---|
195 | [ #o #k * |
---|
196 | | * #tr #s' whd in ⊢ (% → ?); >E0_left <(E0_right tr) #AFTER |
---|
197 | %{tr} %{s'} cases (inv s') in AFTER ⊢ %; #AFTER % /3/ cases AFTER |
---|
198 | | #m * |
---|
199 | ] |
---|
200 | | #r * |
---|
201 | ] qed. |
---|
202 | |
---|
203 | lemma after_1_step : ∀O,I,exec,g,inv,P,s. |
---|
204 | after_n_steps 1 O I exec g s inv P → |
---|
205 | ∃tr,s'. is_final … exec g s = None ? ∧ |
---|
206 | step ?? exec g s = Value … 〈tr,s'〉 ∧ |
---|
207 | bool_to_Prop (inv s') ∧ P tr s'. |
---|
208 | #O #I #exec #g #inv #P #s #AFTER |
---|
209 | cases (after_1_of_n_steps … AFTER) |
---|
210 | #tr * #s' * * * #NF #STEP #INV #FIN %{tr} %{s'} % [%[%]] // whd in FIN; >E0_right in FIN; // |
---|
211 | qed. |
---|
212 | |
---|
213 | (* A typical way to use the following: |
---|
214 | |
---|
215 | With a hypothesis |
---|
216 | EX : after_n_steps n ... (State ...) ... |
---|
217 | reduce it [whd in EX;] to |
---|
218 | EX : await_value ... |
---|
219 | then perform inversion |
---|
220 | [cases (await_value_bind_inv … EX) -EX * #x * #E1 #EX] |
---|
221 | x : T |
---|
222 | E1 : f = return x |
---|
223 | EX : await_value ... |
---|
224 | *) |
---|
225 | |
---|
226 | lemma await_value_bind_inv : ∀avs,T,f,g,P. |
---|
227 | await_value avs (m_bind … f g) P → |
---|
228 | ∃x:T. (f = return x) ∧ await_value avs (g x) P. |
---|
229 | #avs #T * |
---|
230 | [ #o #k #g #P * |
---|
231 | | #x #g #P #AWAIT %{x} % // |
---|
232 | | #m #g #P * |
---|
233 | ] qed. |
---|
234 | |
---|
235 | (* A (possibly non-terminating) execution. *) |
---|
236 | coinductive execution (state:Type[0]) (output:Type[0]) (input:output → Type[0]) : Type[0] ≝ |
---|
237 | | e_stop : trace → int → state → execution state output input |
---|
238 | | e_step : trace → state → execution state output input → execution state output input |
---|
239 | | e_wrong : errmsg → execution state output input |
---|
240 | | e_interact : ∀o:output. (input o → execution state output input) → execution state output input. |
---|
241 | |
---|
242 | (* This definition is slightly awkward because of the need to provide resumptions. |
---|
243 | It records the last trace/state passed in, then recursively processes the next |
---|
244 | state. *) |
---|
245 | |
---|
246 | let corec exec_inf_aux (output:Type[0]) (input:output → Type[0]) |
---|
247 | (exec:trans_system output input) (g:global ?? exec) |
---|
248 | (s:IO output input (trace×(state ?? exec g))) |
---|
249 | : execution ??? ≝ |
---|
250 | match s with |
---|
251 | [ Wrong m ⇒ e_wrong ??? m |
---|
252 | | Value v ⇒ let 〈t,s'〉 ≝ v in |
---|
253 | match is_final ?? exec g s' with |
---|
254 | [ Some r ⇒ e_stop ??? t r s' |
---|
255 | | None ⇒ e_step ??? t s' (exec_inf_aux ??? g (step ?? exec g s')) ] |
---|
256 | | Interact out k' ⇒ e_interact ??? out (λv. exec_inf_aux ??? g (k' v)) |
---|
257 | ]. |
---|
258 | |
---|
259 | lemma execution_cases: ∀o,i,s.∀e:execution s o i. |
---|
260 | e = match e with [ e_stop tr r m ⇒ e_stop ??? tr r m |
---|
261 | | e_step tr s e ⇒ e_step ??? tr s e |
---|
262 | | e_wrong m ⇒ e_wrong ??? m | e_interact o k ⇒ e_interact ??? o k ]. |
---|
263 | #o #i #s #e cases e; [1: #T #I #M % | 2: #T #S #E % | 3: #E % |
---|
264 | | 4: #O #I % ] qed. (* XXX: assertion failed: superposition.ml when using auto |
---|
265 | here, used reflexivity instead *) |
---|
266 | |
---|
267 | axiom exec_inf_aux_unfold: ∀o,i,exec,g,s. exec_inf_aux o i exec g s = |
---|
268 | match s with |
---|
269 | [ Wrong m ⇒ e_wrong ??? m |
---|
270 | | Value v ⇒ let 〈t,s'〉 ≝ v in |
---|
271 | match is_final ?? exec g s' with |
---|
272 | [ Some r ⇒ e_stop ??? t r s' |
---|
273 | | None ⇒ e_step ??? t s' (exec_inf_aux ??? g (step ?? exec g s')) ] |
---|
274 | | Interact out k' ⇒ e_interact ??? out (λv. exec_inf_aux ??? g (k' v)) |
---|
275 | ]. |
---|
276 | (* |
---|
277 | #exec #ge #s >(execution_cases ? (exec_inf_aux …)) cases s |
---|
278 | [ #o #k |
---|
279 | | #x cases x #tr #s' (* XXX Can't unfold exec_inf_aux here *) |
---|
280 | | ] |
---|
281 | whd in ⊢ (??%%); //; |
---|
282 | qed. |
---|
283 | *) |
---|
284 | |
---|
285 | lemma exec_inf_stops_at_final : ∀O,I,TS,ge,s,s',tr,r. |
---|
286 | exec_inf_aux O I TS ge (step … ge s) = e_stop … tr r s' → |
---|
287 | step … ge s = Value … 〈tr, s'〉 ∧ |
---|
288 | is_final … s' = Some ? r. |
---|
289 | #O #I #TS #ge #s #s' #tr #r |
---|
290 | >exec_inf_aux_unfold |
---|
291 | cases (step … ge s) |
---|
292 | [ 1,3: normalize #H1 #H2 try #H3 destruct |
---|
293 | | * #tr' #s'' |
---|
294 | whd in ⊢ (??%? → ?); |
---|
295 | lapply (refl ? (is_final … s'')) |
---|
296 | cases (is_final … s'') in ⊢ (???% → %); |
---|
297 | [ #_ whd in ⊢ (??%? → ?); #E destruct |
---|
298 | | #r' #E1 #E2 whd in E2:(??%?); destruct % // |
---|
299 | ] |
---|
300 | ] qed. |
---|
301 | |
---|
302 | lemma extract_step : ∀O,I,TS,ge,s,s',tr,e. |
---|
303 | exec_inf_aux O I TS ge (step … ge s) = e_step … tr s' e → |
---|
304 | step … ge s = Value … 〈tr,s'〉 ∧ e = exec_inf_aux O I TS ge (step … ge s'). |
---|
305 | #O #I #TS #ge #s #s' #tr #e |
---|
306 | >exec_inf_aux_unfold |
---|
307 | cases (step … s) |
---|
308 | [ 1,3: normalize #H1 #H2 try #H3 destruct |
---|
309 | | * #tr' #s'' |
---|
310 | whd in ⊢ (??%? → ?); |
---|
311 | cases (is_final … s'') |
---|
312 | [ #E normalize in E; destruct /2/ |
---|
313 | | #r #E normalize in E; destruct |
---|
314 | ] |
---|
315 | ] qed. |
---|
316 | |
---|
317 | lemma extract_interact : ∀O,I,TS,ge,s,o,k. |
---|
318 | exec_inf_aux O I TS ge (step … ge s) = e_interact … o k → |
---|
319 | ∃k'. step … ge s = Interact … o k' ∧ k = (λv. exec_inf_aux ??? ge (k' v)). |
---|
320 | #O #I #TS #ge #s #o #k >exec_inf_aux_unfold |
---|
321 | cases (step … s) |
---|
322 | [ #o' #k' normalize #E destruct %{k'} /2/ |
---|
323 | | * #x #y normalize cases (is_final ?????) normalize |
---|
324 | #X try #Y destruct |
---|
325 | | normalize #m #E destruct |
---|
326 | ] qed. |
---|
327 | |
---|
328 | lemma exec_e_step_not_final : ∀O,I,TS,ge,s,s',tr,e. |
---|
329 | exec_inf_aux O I TS ge (step … ge s) = e_step … tr s' e → |
---|
330 | is_final … s' = None ?. |
---|
331 | #O #I #TS #ge #s #s' #tr #e |
---|
332 | >exec_inf_aux_unfold |
---|
333 | cases (step … s) |
---|
334 | [ 1,3: normalize #H1 #H2 try #H3 destruct |
---|
335 | | * #tr' #s'' |
---|
336 | whd in ⊢ (??%? → ?); |
---|
337 | lapply (refl ? (is_final … s'')) |
---|
338 | cases (is_final … s'') in ⊢ (???% → %); |
---|
339 | [ #F whd in ⊢ (??%? → ?); #E destruct @F |
---|
340 | | #r' #_ #E whd in E:(??%?); destruct |
---|
341 | ] |
---|
342 | ] qed. |
---|
343 | |
---|
344 | |
---|
345 | |
---|
346 | record fullexec (outty:Type[0]) (inty:outty → Type[0]) : Type[2] ≝ |
---|
347 | { program : Type[0] |
---|
348 | ; es1 :> trans_system outty inty |
---|
349 | ; make_global : program → global ?? es1 |
---|
350 | ; make_initial_state : ∀p:program. res (state ?? es1 (make_global p)) |
---|
351 | }. |
---|
352 | |
---|
353 | definition exec_inf : ∀o,i.∀fx:fullexec o i. ∀p:program ?? fx. execution (state ?? fx (make_global … fx p)) o i ≝ |
---|
354 | λo,i,fx,p. |
---|
355 | match make_initial_state ?? fx p with |
---|
356 | [ OK s ⇒ exec_inf_aux ?? fx (make_global … fx p) (Value … 〈E0,s〉) |
---|
357 | | Error m ⇒ e_wrong ??? m |
---|
358 | ]. |
---|
359 | |
---|
360 | |
---|
361 | |
---|
362 | |
---|
363 | definition execution_prefix : Type[0] → Type[0] ≝ λstate. list (trace × state). |
---|
364 | |
---|
365 | let rec split_trace O I (state:Type[0]) (x:execution state O I) (n:nat) on n : option (execution_prefix state × (execution state O I)) ≝ |
---|
366 | match n with |
---|
367 | [ O ⇒ Some ? 〈[ ], x〉 |
---|
368 | | S n' ⇒ |
---|
369 | match x with |
---|
370 | [ e_step tr s x' ⇒ |
---|
371 | ! 〈pre,x''〉 ← split_trace ?? state x' n'; |
---|
372 | Some ? 〈〈tr,s〉::pre,x''〉 |
---|
373 | (* Necessary for a measurable trace at the end of the program *) |
---|
374 | | e_stop tr r s ⇒ |
---|
375 | match n' with |
---|
376 | [ O ⇒ Some ? 〈[〈tr,s〉], x〉 |
---|
377 | | _ ⇒ None ? |
---|
378 | ] |
---|
379 | | _ ⇒ None ? |
---|
380 | ] |
---|
381 | ]. |
---|
382 | |
---|
383 | (* For now I'm doing this without I/O, to keep things simple. In the place I |
---|
384 | intend to use it (the definition of measurable subtraces, and proofs using |
---|
385 | that) I should allow I/O for the prefix. *) |
---|
386 | |
---|
387 | let rec exec_steps (n:nat) O I (fx:fullexec O I) (g:global … fx) (s:state … fx g) : res (list (trace × (state … fx g)) × (state … fx g)) ≝ |
---|
388 | match n with |
---|
389 | [ O ⇒ return 〈[ ], s〉 |
---|
390 | | S m ⇒ |
---|
391 | match is_final … fx g s with |
---|
392 | [ Some r ⇒ Error … (msg TerminatedEarly) |
---|
393 | | None ⇒ |
---|
394 | match step … fx g s with |
---|
395 | [ Value trs ⇒ |
---|
396 | ! 〈tl,s'〉 ← exec_steps m O I fx g (\snd trs); |
---|
397 | return 〈trs::tl, s'〉 |
---|
398 | | Interact _ _ ⇒ Error … (msg UnexpectedIO) |
---|
399 | | Wrong m ⇒ Error … m |
---|
400 | ] |
---|
401 | ] |
---|
402 | ]. |
---|
403 | |
---|
404 | (* Show that it's nice. *) |
---|
405 | |
---|
406 | lemma exec_steps_S : ∀O,I,fx,g,n,s,trace,s''. |
---|
407 | exec_steps (S n) O I fx g s = OK … 〈trace,s''〉 → |
---|
408 | is_final … fx g s = None ? ∧ |
---|
409 | ∃tr',s',tl. |
---|
410 | trace = 〈tr',s'〉::tl ∧ |
---|
411 | step … fx g s = Value … 〈tr',s'〉 ∧ |
---|
412 | exec_steps n O I fx g s' = OK … 〈tl,s''〉. |
---|
413 | #O #I #fx #g #n #s #trace #s'' |
---|
414 | whd in ⊢ (??%? → ?); |
---|
415 | cases (is_final … s) |
---|
416 | [ whd in ⊢ (??%? → ?); |
---|
417 | cases (step … s) |
---|
418 | [ #o #i #EX whd in EX:(??%?); destruct |
---|
419 | | * #tr' #s' whd in ⊢ (??%? → ?); #EX %{(refl ??)} |
---|
420 | %{tr'} %{s'} cases (exec_steps … g s') in EX ⊢ %; |
---|
421 | [ * #tl #s'' #EX whd in EX:(??%?); destruct %{tl} /3/ |
---|
422 | | #m #EX whd in EX:(??%?); destruct |
---|
423 | ] |
---|
424 | | #m #EX whd in EX:(??%?); destruct |
---|
425 | ] |
---|
426 | | #r #EX whd in EX:(??%?); destruct |
---|
427 | ] qed. |
---|
428 | |
---|
429 | lemma exec_steps_length : ∀O,I,fx,g,n,s,trace,s'. |
---|
430 | exec_steps n O I fx g s = OK … 〈trace,s'〉 → |
---|
431 | n = |trace|. |
---|
432 | #O #I #fx #g #n elim n |
---|
433 | [ #s #trace #s' #EX whd in EX:(??%?); destruct % |
---|
434 | | #m #IH #s #trace #s' #EX |
---|
435 | cases (exec_steps_S … EX) #notfinal * #tr' * #s'' * #tl * * #Etl #Estep #steps |
---|
436 | >(IH … steps) >Etl % |
---|
437 | ] qed. |
---|
438 | |
---|
439 | lemma exec_steps_nonterm : ∀O,I,fx,g,n,s,h,t,s'. |
---|
440 | exec_steps n O I fx g s = OK … 〈h::t,s'〉 → |
---|
441 | is_final … s = None ?. |
---|
442 | #O #I #fx #g #n #s #h #t #s' #EX |
---|
443 | lapply (exec_steps_length … EX) |
---|
444 | #Elen destruct whd in EX:(??%?); |
---|
445 | cases (is_final … s) in EX ⊢ %; |
---|
446 | [ // |
---|
447 | | #r #EX whd in EX:(??%?); destruct |
---|
448 | ] qed. |
---|
449 | |
---|
450 | lemma exec_steps_nonterm' : ∀O,I,fx,g,n,s,h,t,s'. |
---|
451 | exec_steps n O I fx g s = OK … 〈h@[t], s'〉 → |
---|
452 | is_final … s = None ?. |
---|
453 | #O #I #fx #g #n #s * [2: #h1 #h2] #t #s' @exec_steps_nonterm |
---|
454 | qed. |
---|
455 | |
---|
456 | let rec gather_trace S (l:list (trace × S)) on l : trace ≝ |
---|
457 | match l with |
---|
458 | [ nil ⇒ E0 |
---|
459 | | cons h t ⇒ (\fst h)⧺(gather_trace S t) |
---|
460 | ]. |
---|
461 | |
---|
462 | lemma exec_steps_after_n_simple : ∀n,O,I,fx,g,s,trace,s'. |
---|
463 | exec_steps n O I fx g s = OK ? 〈trace,s'〉 → |
---|
464 | after_n_steps n O I fx g s (λ_. true) (λtr,s''. 〈tr,s''〉 = 〈gather_trace ? trace,s'〉). |
---|
465 | #n elim n |
---|
466 | [ #O #I #fx #g #s #trace #s' #EXEC whd in EXEC:(??%?); destruct |
---|
467 | whd % |
---|
468 | | #m #IH #O #I #fx #g #s #trace #s' #EXEC |
---|
469 | cases (exec_steps_S … EXEC) #NOTFINAL * #tr1 * #s1 * #tl * * #E1 #STEP #STEPS |
---|
470 | @(after_n_m 1 … (IH … STEPS)) |
---|
471 | whd >NOTFINAL whd >STEP whd %{(refl ??)} #tr'' #s'' #E destruct % |
---|
472 | ] qed. |
---|
473 | |
---|
474 | lemma exec_steps_after_n : ∀n,O,I,fx,g,s,trace,s',inv,P. |
---|
475 | exec_steps n O I fx g s = OK ? 〈trace,s'〉 → |
---|
476 | all … (λts. inv (\snd ts)) trace → |
---|
477 | P (gather_trace ? trace) s' → |
---|
478 | after_n_steps n O I fx g s inv P. |
---|
479 | #n elim n |
---|
480 | [ #O #I #fx #g #s #trace #s' #inv #P #EXEC whd in EXEC:(??%?); destruct |
---|
481 | #ALL #p whd @p |
---|
482 | | #m #IH #O #I #fx #g #s #trace #s' #inv #P #EXEC |
---|
483 | cases (exec_steps_S … EXEC) #NOTFINAL * #tr1 * #s1 * #tl * * #E1 #STEP #STEPS |
---|
484 | destruct |
---|
485 | #ALL cut (bool_to_Prop (inv s1) ∧ bool_to_Prop (all … (λts. inv (\snd ts)) tl)) |
---|
486 | [ whd in ALL:(?%); cases (inv s1) in ALL ⊢ %; /2/ ] * #i1 #itl |
---|
487 | #p @(after_n_m 1 … (λtr,s. P (tr1⧺tr) s) … (IH … STEPS itl ?)) |
---|
488 | [ @p |
---|
489 | | whd >NOTFINAL whd >STEP whd >i1 whd %{(refl ??)} #tr'' #s'' #p' @p' |
---|
490 | ] |
---|
491 | ] qed. |
---|
492 | |
---|
493 | lemma exec_steps_after_n_noinv : ∀n,O,I,fx,g,s,trace,s',P. |
---|
494 | exec_steps n O I fx g s = OK ? 〈trace,s'〉 → |
---|
495 | P (gather_trace ? trace) s' → |
---|
496 | after_n_steps n O I fx g s (λ_.true) P. |
---|
497 | #n #O #I #fx #g #s #trace #s' #P #EXEC #p |
---|
498 | @(exec_steps_after_n … EXEC) // |
---|
499 | elim trace /2/ |
---|
500 | qed. |
---|
501 | |
---|
502 | lemma after_n_exec_steps : ∀n,O,I. ∀fx:fullexec O I. ∀g,s,inv,P. |
---|
503 | after_n_steps n O I fx g s inv P → |
---|
504 | ∃trace,s'. exec_steps n O I fx g s = OK ? 〈trace,s'〉 ∧ P (gather_trace ? trace) s'. |
---|
505 | #n elim n |
---|
506 | [ #O #I #fx #g #s #inv #P #AFTER %{[ ]} %{s} %{(refl ??)} @AFTER |
---|
507 | | #m #IH #O #I #fx #g #s #inv #P #AFTER |
---|
508 | cases (after_1_of_n_steps … AFTER) |
---|
509 | #tr1 * #s1 * * * #NF #STEP #INV #AFTER' |
---|
510 | cases (IH … AFTER') |
---|
511 | #tl * #s' * #STEPS #p |
---|
512 | %{(〈tr1,s1〉::tl)} %{s'} % |
---|
513 | [ whd in ⊢ (??%?); >NF whd in ⊢ (??%?); >STEP whd in ⊢ (??%?); >STEPS % | // ] |
---|
514 | ] qed. |
---|
515 | |
---|
516 | lemma exec_steps_split : ∀n,m,O,I,fx,g,s,trace,s'. |
---|
517 | exec_steps (n+m) O I fx g s = OK ? 〈trace,s'〉 → |
---|
518 | ∃trace1,trace2,s1. |
---|
519 | exec_steps n O I fx g s = OK ? 〈trace1,s1〉 ∧ |
---|
520 | exec_steps m O I fx g s1 = OK ? 〈trace2,s'〉 ∧ |
---|
521 | trace = trace1 @ trace2. |
---|
522 | #n elim n |
---|
523 | [ #m #O #I #fx #g #s #trace #s' #EXEC |
---|
524 | %{[ ]} %{trace} %{s} /3/ |
---|
525 | | #n' #IH #m #O #I #fx #g #s #trace #s' #EXEC |
---|
526 | cases (exec_steps_S … EXEC) #NF * #tr' * #s' * #tl * * #E1 #STEP #EXEC' |
---|
527 | cases (IH … EXEC') #trace1 * #trace2 * #s1 * * #EXEC1 #EXEC2 #E2 |
---|
528 | %{(〈tr',s'〉::trace1)} %{trace2} %{s1} |
---|
529 | % |
---|
530 | [ % |
---|
531 | [ whd in ⊢ (??%?); >NF >STEP whd in ⊢ (??%?); >EXEC1 % |
---|
532 | | @EXEC2 |
---|
533 | ] |
---|
534 | | destruct % |
---|
535 | ] |
---|
536 | ] qed. |
---|
537 | |
---|
538 | lemma exec_steps_join : ∀n,m,O,I,fx,g,s1,trace1,s2,trace2,s3. |
---|
539 | exec_steps n O I fx g s1 = OK ? 〈trace1,s2〉 → |
---|
540 | exec_steps m O I fx g s2 = OK ? 〈trace2,s3〉 → |
---|
541 | exec_steps (n+m) O I fx g s1 = OK ? 〈trace1@trace2,s3〉. |
---|
542 | #n elim n |
---|
543 | [ #m #O #I #fx #g #s1 #trace1 #s2 #trace2 #s3 #EXEC1 #EXEC2 |
---|
544 | whd in EXEC1:(??%?); destruct @EXEC2 |
---|
545 | | #n' #IH #m #O #I #fx #g #s1 #trace1 #s2 #trace2 #s3 #EXEC1 #EXEC2 |
---|
546 | cases (exec_steps_S … EXEC1) #NF * #tr' * #s' * #tl' * * #E1 #STEP #EXEC' |
---|
547 | whd in ⊢ (??%?); >NF >STEP whd in ⊢ (??%?); >(IH … EXEC' EXEC2) |
---|
548 | destruct % |
---|
549 | ] qed. |
---|
550 | |
---|
551 | (* Show that it corresponds to split_trace … (exec_inf …) *) |
---|
552 | |
---|
553 | lemma exec_steps_inf_aux : ∀O,I. ∀fx:fullexec O I. ∀g,n,s,trace,s'. |
---|
554 | exec_steps n O I fx g s = OK ? 〈trace,s'〉 → |
---|
555 | match is_final … s' with |
---|
556 | [ None ⇒ split_trace … (exec_inf_aux … fx g (step … fx g s)) n = Some ? 〈trace, exec_inf_aux … fx g (step … s')〉 |
---|
557 | | Some r ⇒ n = 0 ∨ ∃tr'. split_trace … (exec_inf_aux … fx g (step … fx g s)) n = Some ? 〈trace, e_stop … tr' r s'〉 |
---|
558 | ]. |
---|
559 | #O #I #fx #g #n elim n |
---|
560 | [ #s #trace #s' #EX whd in EX:(??%%); destruct |
---|
561 | cases (is_final … s') [ % | #r %1 % ] |
---|
562 | | #m #IH #s #trace #s' #EX |
---|
563 | cases (exec_steps_S … EX) |
---|
564 | #notfinal * #tr'' * #s'' * #tl * * #Etrace #Estep #Esteps |
---|
565 | cases tl in Etrace Esteps ⊢ %; |
---|
566 | [ #E destruct #Esteps |
---|
567 | lapply (exec_steps_length … Esteps) #Elen normalize in Elen; destruct |
---|
568 | whd in Esteps:(??%?); destruct |
---|
569 | >Estep |
---|
570 | >exec_inf_aux_unfold normalize nodelta |
---|
571 | cases (is_final … s') |
---|
572 | [ % |
---|
573 | | #r %2 %{tr''} % |
---|
574 | ] |
---|
575 | | * #tr1 #s1 #tl1 #E normalize in E; destruct #Esteps |
---|
576 | lapply (IH … Esteps) cases (is_final … s') |
---|
577 | [ normalize nodelta #IH' >Estep >exec_inf_aux_unfold whd in ⊢ (??(????%?)?); |
---|
578 | >(exec_steps_nonterm … Esteps) whd in ⊢ (??%?); >IH' % |
---|
579 | | normalize nodelta #r * |
---|
580 | [ #E @⊥ >(exec_steps_length … Esteps) in E; #E normalize in E; destruct |
---|
581 | | * #tr'' #IH' %2 %{tr''} >Estep >exec_inf_aux_unfold whd in ⊢ (??(????%?)?); |
---|
582 | >(exec_steps_nonterm … Esteps) whd in ⊢ (??%?); >IH' % |
---|
583 | ] |
---|
584 | ] |
---|
585 | ] |
---|
586 | ] qed. |
---|