source: src/common/SmallstepExec.ma @ 2755

Last change on this file since 2755 was 2685, checked in by campbell, 7 years ago

Progress on measurable trace preservation: prefix preserves observable
intensional events (costs and calls).

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