source: src/common/SmallstepExec.ma @ 3081

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

Tidy up recent work a little.

File size: 23.8 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
237lemma after_aux_result : ∀avs,n,s,tr,P.
238  after_aux avs n s tr P →
239  ∃tr',s'. P tr' s' ∧ after_aux avs n s tr (λtr'',s''. 〈tr'',s''〉 = 〈tr',s'〉).
240#avs #n elim n
241[ #s #tr #P #A whd in A; %{tr} %{s} % [ @A | % ]
242| #n' #IH #s #tr #P
243  whd in ⊢ (% → ?);
244  lapply (refl ? (is_final … s))
245  cases (is_final … s) in ⊢ (???% → %);
246  [ #F whd in ⊢ (% → ?);
247    lapply (refl ? (step … s))
248    cases (step … s) in ⊢ (???% → %);
249    [ #o #k #_ *
250    | * #tr1 #s1 #ST whd in ⊢ (% → ?);
251      cases n' in IH ⊢ %;
252      [ #_ whd in ⊢ (% → ?); #p % [2: % [2: %{p} whd >F whd >ST whd % | skip ] | skip ]
253      | #n'' #IH lapply (refl ? (avs_inv avs s1)) cases (avs_inv avs s1) in ⊢ (???% → %);
254        [ #INV #AF
255          cases (IH … AF) #tr' * #s' * #p #AF'
256         % [2: % [2: %{p} whd >F whd >ST whd >INV @AF' | skip ] | skip ]
257        | #_ *
258        ]
259      ]
260    | #m #_ *
261    ]
262  | #r #F *
263  ]
264] qed.
265
266lemma after_n_result : ∀n,O,I,exec,g,s,P,inv.
267  after_n_steps n O I exec g s inv P →
268  ∃tr',s'.
269    P tr' s' ∧
270    after_n_steps n O I exec g s inv (λtr'',s''. 〈tr'',s''〉 = 〈tr',s'〉).
271#n #O #I #exec #g #s #P #inv #A
272cases (after_aux_result … A) #tr * #s' * #p #A'
273%{tr} %{s'} %{p} @A'
274qed.
275
276lemma after_1_of_n_steps' : ∀n,O,I,exec,g,tr,s',s.
277  after_n_steps (S n) O I exec g s (λ_.true) (λtrx,sx. 〈trx,sx〉 = 〈tr,s'〉) →
278  ∃tr1,tr2,s1.
279  is_final … exec g s = None ? ∧
280  step … exec g s = Value … 〈tr1,s1〉 ∧
281  tr = tr1⧺tr2 ∧
282  after_n_steps n O I exec g s1 (λ_.true) (λtrx,sx. 〈trx,sx〉 = 〈tr2,s'〉).
283#n #O #I #exec #g #tr #s' #s #A
284cases (after_1_of_n_steps … A)
285#tr1 * #s1 * * * #F #ST #_ #A'
286cases (after_n_result … A')
287#tr'' * #s'' * #E #A'' destruct
288% [2: % [2: % [2: % [ % [% [ @F | @ST ] | % ] | @A'' ] | skip ] | skip ] | skip ]
289qed.
290
291(* A typical way to use the following:
292
293   With a hypothesis
294     EX : after_n_steps n ... (State ...) ...
295   reduce it [whd in EX;] to
296     EX : await_value ...
297   then perform inversion
298   [cases (await_value_bind_inv … EX) -EX * #x * #E1 #EX]
299      x : T
300     E1 : f = return x
301     EX : await_value ...
302 *)
303
304lemma await_value_bind_inv : ∀avs,T,f,g,P.
305  await_value avs (m_bind … f g) P →
306  ∃x:T. (f = return x) ∧ await_value avs (g x) P.
307#avs #T *
308[ #o #k #g #P *
309| #x #g #P #AWAIT %{x} % //
310| #m #g #P *
311] qed.
312
313(* A (possibly non-terminating) execution.   *)
314coinductive execution (state:Type[0]) (output:Type[0]) (input:output → Type[0]) : Type[0] ≝
315| e_stop : trace → int → state → execution state output input
316| e_step : trace → state → execution state output input → execution state output input
317| e_wrong : errmsg → execution state output input
318| e_interact : ∀o:output. (input o → execution state output input) → execution state output input.
319
320(* This definition is slightly awkward because of the need to provide resumptions.
321   It records the last trace/state passed in, then recursively processes the next
322   state. *)
323
324let corec exec_inf_aux (output:Type[0]) (input:output → Type[0])
325                       (exec:trans_system output input) (g:global ?? exec)
326                       (s:IO output input (trace×(state ?? exec g)))
327                       : execution ??? ≝
328match s with
329[ Wrong m ⇒ e_wrong ??? m
330| Value v ⇒ let 〈t,s'〉 ≝ v in
331    match is_final ?? exec g s' with
332    [ Some r ⇒ e_stop ??? t r s'
333    | None ⇒ e_step ??? t s' (exec_inf_aux ??? g (step ?? exec g s')) ]
334| Interact out k' ⇒ e_interact ??? out (λv. exec_inf_aux ??? g (k' v))
335].
336
337lemma execution_cases: ∀o,i,s.∀e:execution s o i.
338 e = match e with [ e_stop tr r m ⇒ e_stop ??? tr r m
339 | e_step tr s e ⇒ e_step ??? tr s e
340 | e_wrong m ⇒ e_wrong ??? m | e_interact o k ⇒ e_interact ??? o k ].
341#o #i #s #e cases e; [1: #T #I #M % | 2: #T #S #E % | 3: #E %
342 | 4: #O #I % ] qed. (* XXX: assertion failed: superposition.ml when using auto
343  here, used reflexivity instead *)
344
345axiom exec_inf_aux_unfold: ∀o,i,exec,g,s. exec_inf_aux o i exec g s =
346match s with
347[ Wrong m ⇒ e_wrong ??? m
348| Value v ⇒ let 〈t,s'〉 ≝ v in
349    match is_final ?? exec g s' with
350    [ Some r ⇒ e_stop ??? t r s'
351    | None ⇒ e_step ??? t s' (exec_inf_aux ??? g (step ?? exec g s')) ]
352| Interact out k' ⇒ e_interact ??? out (λv. exec_inf_aux ??? g (k' v))
353].
354(*
355#exec #ge #s >(execution_cases ? (exec_inf_aux …)) cases s
356[ #o #k
357| #x cases x #tr #s' (* XXX Can't unfold exec_inf_aux here *)
358| ]
359whd in ⊢ (??%%); //;
360qed.
361*)
362
363lemma exec_inf_stops_at_final : ∀O,I,TS,ge,s,s',tr,r.
364  exec_inf_aux O I TS ge (step … ge s) = e_stop … tr r s' →
365  step … ge s = Value … 〈tr, s'〉 ∧
366  is_final … s' = Some ? r.
367#O #I #TS #ge #s #s' #tr #r
368>exec_inf_aux_unfold
369cases (step … ge s)
370[ 1,3: normalize #H1 #H2 try #H3 destruct
371| * #tr' #s''
372  whd in ⊢ (??%? → ?);
373  lapply (refl ? (is_final … s''))
374  cases (is_final … s'') in ⊢ (???% → %);
375  [ #_ whd in ⊢ (??%? → ?); #E destruct
376  | #r' #E1 #E2 whd in E2:(??%?);  destruct % //
377  ]
378] qed.
379
380lemma extract_step : ∀O,I,TS,ge,s,s',tr,e.
381  exec_inf_aux O I TS ge (step … ge s) = e_step … tr s' e →
382  step … ge s = Value …  〈tr,s'〉 ∧ e = exec_inf_aux O I TS ge (step … ge s').
383#O #I #TS #ge #s #s' #tr #e
384>exec_inf_aux_unfold
385cases (step … s)
386[ 1,3: normalize #H1 #H2 try #H3 destruct
387| * #tr' #s''
388  whd in ⊢ (??%? → ?);
389  cases (is_final … s'')
390  [ #E normalize in E; destruct /2/
391  | #r #E normalize in E; destruct
392  ]
393] qed.
394
395lemma extract_interact : ∀O,I,TS,ge,s,o,k.
396  exec_inf_aux O I TS ge (step … ge s) = e_interact … o k →
397  ∃k'. step … ge s = Interact … o k' ∧ k = (λv. exec_inf_aux ??? ge (k' v)).
398#O #I #TS #ge #s #o #k >exec_inf_aux_unfold
399cases (step … s)
400[ #o' #k' normalize #E destruct %{k'} /2/
401| * #x #y normalize cases (is_final ?????) normalize
402  #X try #Y destruct
403| normalize #m #E destruct
404] qed.
405
406lemma exec_e_step_not_final : ∀O,I,TS,ge,s,s',tr,e.
407  exec_inf_aux O I TS ge (step … ge s) = e_step … tr s' e →
408  is_final … s' = None ?.
409#O #I #TS #ge #s #s' #tr #e
410>exec_inf_aux_unfold
411cases (step … s)
412[ 1,3: normalize #H1 #H2 try #H3 destruct
413| * #tr' #s''
414  whd in ⊢ (??%? → ?);
415  lapply (refl ? (is_final … s''))
416  cases (is_final … s'') in ⊢ (???% → %);
417  [ #F whd in ⊢ (??%? → ?); #E destruct @F
418  | #r' #_ #E whd in E:(??%?);  destruct
419  ]
420] qed.
421
422
423
424record fullexec (outty:Type[0]) (inty:outty → Type[0]) : Type[2] ≝
425{ program : Type[0]
426; es1 :> trans_system outty inty
427; make_global : program → global ?? es1
428; make_initial_state : ∀p:program. res (state ?? es1 (make_global p))
429}.
430
431definition exec_inf : ∀o,i.∀fx:fullexec o i. ∀p:program ?? fx. execution (state ?? fx (make_global … fx p)) o i ≝
432λo,i,fx,p.
433  match make_initial_state ?? fx p with
434  [ OK s ⇒ exec_inf_aux ?? fx (make_global … fx p) (Value … 〈E0,s〉)
435  | Error m ⇒ e_wrong ??? m
436  ].
437
438
439
440
441definition execution_prefix : Type[0] → Type[0] ≝ λstate. list (trace × state).
442
443let 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)) ≝
444match n with
445[ O ⇒ Some ? 〈[ ], x〉
446| S n' ⇒
447  match x with
448  [ e_step tr s x' ⇒
449    ! 〈pre,x''〉 ← split_trace ?? state x' n';
450    Some ? 〈〈tr,s〉::pre,x''〉
451    (* Necessary for a measurable trace at the end of the program *)
452  | e_stop tr r s ⇒
453    match n' with
454    [ O ⇒ Some ? 〈[〈tr,s〉], x〉
455    | _ ⇒ None ?
456    ]
457  | _ ⇒ None ?
458  ]
459].
460
461(* For now I'm doing this without I/O, to keep things simple.  In the place I
462   intend to use it (the definition of measurable subtraces, and proofs using
463   that) I should allow I/O for the prefix.
464   
465   If the execution has the form
466   
467     s1 -tr1→ s2 -tr2→ … sn -trn→ s'
468   
469   then the function returns
470   
471     〈[〈s1,tr1〉; 〈s2,tr2〉; …; 〈sn,trn〉], s'〉
472   *)
473
474let 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)) ≝
475match n with
476[ O ⇒ return 〈[ ], s〉
477| S m ⇒
478  match is_final … fx g s with
479  [ Some r ⇒ Error … (msg TerminatedEarly)
480  | None ⇒
481    match step … fx g s with
482    [ Value trs ⇒
483        ! 〈tl,s'〉 ← exec_steps m O I fx g (\snd trs);
484        return 〈〈s, \fst trs〉::tl, s'〉
485    | Interact _ _ ⇒ Error … (msg UnexpectedIO)
486    | Wrong m ⇒ Error … m
487    ]
488  ]
489].
490
491(* Show that it's nice. *)
492
493lemma exec_steps_S : ∀O,I,fx,g,n,s,trace,s''.
494  exec_steps (S n) O I fx g s = OK … 〈trace,s''〉 →
495  is_final … fx g s = None ? ∧
496  ∃tr',s',tl.
497    trace = 〈s,tr'〉::tl ∧
498    step … fx g s = Value … 〈tr',s'〉 ∧
499    exec_steps n O I fx g s' = OK … 〈tl,s''〉.
500#O #I #fx #g #n #s #trace #s''
501whd in ⊢ (??%? → ?);
502cases (is_final … s)
503[ whd in ⊢ (??%? → ?);
504  cases (step … s)
505  [ #o #i #EX whd in EX:(??%?); destruct
506  | * #tr' #s' whd in ⊢ (??%? → ?); #EX %{(refl ??)}
507    %{tr'} %{s'} cases (exec_steps … g s') in EX ⊢ %;
508    [ * #tl #s'' #EX whd in EX:(??%?); destruct %{tl} /3/
509    | #m #EX whd in EX:(??%?); destruct
510    ]
511  | #m #EX whd in EX:(??%?); destruct
512  ]
513| #r #EX whd in EX:(??%?); destruct
514] qed.
515
516lemma exec_steps_length : ∀O,I,fx,g,n,s,trace,s'.
517  exec_steps n O I fx g s = OK … 〈trace,s'〉 →
518  n = |trace|.
519#O #I #fx #g #n elim n
520[ #s #trace #s' #EX whd in EX:(??%?); destruct %
521| #m #IH #s #trace #s' #EX
522  cases (exec_steps_S … EX) #notfinal * #tr' * #s'' * #tl * * #Etl #Estep #steps
523  >(IH … steps) >Etl %
524] qed.
525
526lemma exec_steps_nonterm : ∀O,I,fx,g,n,s,h,t,s'.
527  exec_steps n O I fx g s = OK … 〈h::t,s'〉 →
528  is_final … s = None ?.
529#O #I #fx #g #n #s #h #t #s' #EX
530lapply (exec_steps_length … EX)
531#Elen destruct whd in EX:(??%?);
532cases (is_final … s) in EX ⊢ %;
533[ //
534| #r #EX whd in EX:(??%?); destruct
535] qed.
536
537lemma exec_steps_nonterm' : ∀O,I,fx,g,n,s,h,t,s'.
538  exec_steps n O I fx g s = OK … 〈h@[t], s'〉 →
539  is_final … s = None ?.
540#O #I #fx #g #n #s * [2: #h1 #h2] #t #s' @exec_steps_nonterm
541qed.
542
543let rec gather_trace S (l:list (S × trace)) on l : trace ≝
544match l with
545[ nil ⇒ E0
546| cons h t ⇒ (\snd h)⧺(gather_trace S t)
547].
548
549lemma exec_steps_after_n_simple : ∀n,O,I,fx,g,s,trace,s'.
550  exec_steps n O I fx g s = OK ? 〈trace,s'〉 →
551  after_n_steps n O I fx g s (λ_. true) (λtr,s''. 〈tr,s''〉 = 〈gather_trace ? trace,s'〉).
552#n elim n
553[ #O #I #fx #g #s #trace #s' #EXEC whd in EXEC:(??%?); destruct
554  whd %
555| #m #IH #O #I #fx #g #s #trace #s' #EXEC
556  cases (exec_steps_S … EXEC) #NOTFINAL * #tr1 * #s1 * #tl * * #E1 #STEP #STEPS
557  @(after_n_m 1 … (IH … STEPS)) //
558  whd >NOTFINAL whd >STEP whd %{(refl ??)} #tr'' #s'' #E destruct %
559] qed.
560
561lemma exec_steps_after_n : ∀n,O,I,fx,g,s,trace,s',inv,P.
562  exec_steps n O I fx g s = OK ? 〈trace,s'〉 →
563  all ? (λstr. inv (\fst str)) (tail … trace) →
564  P (gather_trace ? trace) s' →
565  after_n_steps n O I fx g s inv P.
566#n elim n
567[ #O #I #fx #g #s #trace #s' #inv #P #EXEC whd in EXEC:(??%?); destruct
568  #ALL #p whd @p
569| #m #IH #O #I #fx #g #s #trace #s' #inv #P #EXEC
570  cases (exec_steps_S … EXEC) #NOTFINAL * #tr1 * #s1 * #tl * * #E1 #STEP #STEPS
571  destruct
572  #ALL cut ((notb (eqb m 0) → bool_to_Prop (inv s1)) ∧ bool_to_Prop (all ? (λst. inv (\fst st)) (tail … tl)))
573  [ cases m in STEPS;
574    [ whd in ⊢ (??%? → ?); #E destruct % [ * #H cases (H (refl ??)) | /2/ ]
575    | #m' #STEPS cases (exec_steps_S … STEPS) #_ * #tr'' * #s'' * #tl'' * * #E #_ #_ destruct
576      whd in ALL:(?%); cases (inv s1) in ALL ⊢ %; [ /2/ | * ]
577    ]
578  ] * #i1 #itl
579  #p @(after_n_m 1 … (λtr,s. P (tr1⧺tr) s) … (IH … STEPS itl ?))
580  [ @p
581  | @i1
582  | whd >NOTFINAL whd >STEP whd %{(refl ??)} #tr'' #s'' #p' @p'
583  ]
584] qed.
585
586lemma exec_steps_after_n_noinv : ∀n,O,I,fx,g,s,trace,s',P.
587  exec_steps n O I fx g s = OK ? 〈trace,s'〉 →
588  P (gather_trace ? trace) s' →
589  after_n_steps n O I fx g s (λ_.true) P.
590#n #O #I #fx #g #s #trace #s' #P #EXEC #p
591@(exec_steps_after_n … EXEC) //
592cases trace // #x #trace'
593elim trace' /2/
594qed.
595
596lemma exec_steps_first : ∀n,O,I,fx,g,s,s1,tr1,tl,s'.
597  exec_steps n O I fx g s = OK ? 〈〈s1,tr1〉::tl,s'〉 →
598  s = s1.
599#n #O #I #fx #g #s #s1 #tr1 #tl #s' #EXEC
600lapply (exec_steps_length … EXEC) #E normalize in E; destruct
601cases (exec_steps_S … EXEC) #_ * #tr2 * #s2 * #tl2 * * #E #_ #_ destruct
602%
603qed.
604
605lemma after_n_exec_steps : ∀n,O,I. ∀fx:fullexec O I. ∀g,s,inv,P.
606  after_n_steps n O I fx g s inv P →
607  ∃trace,s'.
608    exec_steps n O I fx g s = OK ? 〈trace,s'〉 ∧
609    bool_to_Prop (all ? (λstr. inv (\fst str)) (tail … trace)) ∧
610    P (gather_trace ? trace) s'.
611#n elim n
612[ #O #I #fx #g #s #inv #P #AFTER %{[ ]} %{s} % [ %{(refl ??)} % | @AFTER ]
613| #m #IH #O #I #fx #g #s #inv #P #AFTER
614  cases (after_1_of_n_steps … AFTER)
615  #tr1 * #s1 * * * #NF #STEP #INV #AFTER'
616  cases (IH … AFTER')
617  #tl * #s' * * #STEPS #INV' #p
618  %{(〈s,tr1〉::tl)} %{s'} %
619  [ %
620    [ whd in ⊢ (??%?); >NF whd in ⊢ (??%?); >STEP whd in ⊢ (??%?); >STEPS %
621    | cases tl in STEPS INV INV' ⊢ %; [ // | * #sx #trx #t #STEPS #INV #INV'
622      <(exec_steps_first … STEPS) whd in ⊢ (?%); >INV //
623      >(exec_steps_length … STEPS) %
624      ]
625    ]
626  | // ]
627] qed.
628
629lemma exec_steps_split : ∀n,m,O,I,fx,g,s,trace,s'.
630  exec_steps (n+m) O I fx g s = OK ? 〈trace,s'〉 →
631  ∃trace1,trace2,s1.
632    exec_steps n O I fx g s = OK ? 〈trace1,s1〉 ∧
633    exec_steps m O I fx g s1 = OK ? 〈trace2,s'〉 ∧   
634    trace = trace1 @ trace2.
635#n elim n
636[ #m #O #I #fx #g #s #trace #s' #EXEC
637  %{[ ]} %{trace} %{s} /3/
638| #n' #IH #m #O #I #fx #g #s #trace #s' #EXEC
639  cases (exec_steps_S … EXEC) #NF * #tr' * #s' * #tl * * #E1 #STEP #EXEC'
640  cases (IH … EXEC') #trace1 * #trace2 * #s1 * * #EXEC1 #EXEC2 #E2
641  %{(〈s,tr'〉::trace1)} %{trace2} %{s1}
642  %
643  [ %
644    [ whd in ⊢ (??%?); >NF >STEP whd in ⊢ (??%?); >EXEC1 %
645    | @EXEC2
646    ]
647  | destruct %
648  ]
649] qed.
650
651lemma exec_steps_join : ∀n,m,O,I,fx,g,s1,trace1,s2,trace2,s3.
652  exec_steps n O I fx g s1 = OK ? 〈trace1,s2〉 →
653  exec_steps m O I fx g s2 = OK ? 〈trace2,s3〉 →
654  exec_steps (n+m) O I fx g s1 = OK ? 〈trace1@trace2,s3〉.
655#n elim n
656[ #m #O #I #fx #g #s1 #trace1 #s2 #trace2 #s3 #EXEC1 #EXEC2
657  whd in EXEC1:(??%?); destruct @EXEC2
658| #n' #IH #m #O #I #fx #g #s1 #trace1 #s2 #trace2 #s3 #EXEC1 #EXEC2
659  cases (exec_steps_S … EXEC1) #NF * #tr' * #s' * #tl' * * #E1 #STEP #EXEC'
660  whd in ⊢ (??%?); >NF >STEP whd in ⊢ (??%?); >(IH … EXEC' EXEC2)
661  destruct %
662] qed.
663
664(* Show that it corresponds to split_trace … (exec_inf …).
665   We need to adjust the form of trace. *)
666
667let rec switch_trace_aux S tr (l:list (S × trace)) (s':S) on l : list (trace × S) ≝
668match l with
669[ nil ⇒ [〈tr,s'〉]
670| cons h t ⇒ 〈tr,\fst h〉::(switch_trace_aux S (\snd h) t s')
671].
672
673definition switch_trace ≝
674λS,l,s'. match l with
675[ nil ⇒ nil ?
676| cons h t ⇒ switch_trace_aux S (\snd h) t s'
677].
678
679lemma exec_steps_inf_aux : ∀O,I. ∀fx:fullexec O I. ∀g,n,s,trace,s'.
680  exec_steps n O I fx g s = OK ? 〈trace,s'〉 →
681  match is_final … s' with
682  [ 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')〉
683  | 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'〉
684  ].
685#O #I #fx #g #n elim n
686[ #s #trace #s' #EX whd in EX:(??%%); destruct
687  cases (is_final … s') [ % | #r %1 % ]
688| #m #IH #s #trace #s' #EX
689  cases (exec_steps_S … EX)
690  #notfinal * #tr'' * #s'' * #tl * * #Etrace #Estep #Esteps
691  cases tl in Etrace Esteps ⊢ %;
692  [ #E destruct #Esteps
693    lapply (exec_steps_length … Esteps) #Elen normalize in Elen; destruct
694    whd in Esteps:(??%?); destruct
695    >Estep
696    >exec_inf_aux_unfold normalize nodelta
697    cases (is_final … s')
698    [ whd %
699    | #r %2 %{tr''} %
700    ]
701  | * #s1 #tr1 #tl1 #E normalize in E; destruct #Esteps
702    lapply (IH … Esteps) cases (is_final … s')
703    [ normalize nodelta #IH' >Estep <(exec_steps_first … Esteps)
704      >exec_inf_aux_unfold whd in ⊢ (??(????%?)?);
705      >(exec_steps_nonterm … Esteps) whd in ⊢ (??%?); >IH' normalize nodelta %
706    | normalize nodelta #r *
707      [ #E @⊥ >(exec_steps_length … Esteps) in E; #E normalize in E; destruct
708      | * #tr'' #IH' %2 %{tr''} >Estep <(exec_steps_first … Esteps)
709        >exec_inf_aux_unfold whd in ⊢ (??(????%?)?);
710        >(exec_steps_nonterm … Esteps) whd in ⊢ (??%?); >IH' %
711      ]
712    ]
713  ]
714] qed.
Note: See TracBrowser for help on using the repository browser.