source: src/Clight/CexecEquiv.ma @ 2391

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

Revert "Put the post-loop cost label into the Clight while statement ..."
Rely on the Cminor to RTLabs stage ignoring Cminor skips instead.
This reverts commit 2353.
File size: 39.7 KB
Line 
1include "Clight/CexecComplete.ma".
2include "Clight/CexecSound.ma".
3include "utilities/extralib.ma".
4
5include "basics/jmeq.ma".
6include alias "basics/logic.ma".
7
8(* A "single execution" - where all of the input values are made explicit. *)
9coinductive s_execution : Type[0] ≝
10| se_stop : trace → int → s_execution
11| se_step : trace → state → s_execution → s_execution
12| se_wrong : errmsg → s_execution
13| se_interact : ∀o:io_out. (io_in o → execution state io_out io_in) → io_in o → s_execution → s_execution.
14
15coinductive single_exec_of : execution state io_out io_in → s_execution → Prop ≝
16| seo_stop : ∀tr,r,s. single_exec_of (e_stop ??? tr r s) (se_stop tr r)
17| seo_step : ∀tr,s,e,se.
18    single_exec_of e se →
19    single_exec_of (e_step ??? tr s e) (se_step tr s se)
20| seo_wrong : ∀msg:errmsg. single_exec_of (e_wrong ??? msg) (se_wrong msg)
21| seo_interact : ∀o,k,i,se.
22    single_exec_of (k i) se →
23    single_exec_of (e_interact ??? o k) (se_interact o k i se).
24
25(* starting after state s, zero or more steps of execution e reach state s'
26   after which comes e'. *)
27inductive execution_isteps : trace → state → s_execution → state → s_execution → Prop ≝
28| isteps_none : ∀s,e. execution_isteps E0 s e s e
29| isteps_one : ∀e,e',tr,tr',s,s',s0.
30    execution_isteps tr' s e s' e' →
31    execution_isteps (tr⧺tr') s0 (se_step tr s e) s' e'
32| isteps_interact : ∀e,e',o,k,i,s,s',s0,tr,tr'.
33    execution_isteps tr' s e s' e' →
34    execution_isteps (tr⧺tr') s0 (se_interact o k i (se_step tr s e)) s' e'.
35
36lemma isteps_trans: ∀tr1,tr2,s1,s2,s3,e1,e2,e3.
37  execution_isteps tr1 s1 e1 s2 e2 →
38  execution_isteps tr2 s2 e2 s3 e3 →
39  execution_isteps (tr1⧺tr2) s1 e1 s3 e3.
40#tr1 #tr2 #s1 #s2 #s3 #e1 #e2 #e3 #H1 elim H1;
41[ #s #e //;
42| #e #e' #tr #tr' #s1' #s2' #s3' #H1 #H2 #H3
43    >(Eapp_assoc …)
44    @isteps_one
45    @H2 @H3
46| #e #e' #o #k #i #s1' #s2' #s3' #tr #tr' #H1 #H2 #H3
47    >(Eapp_assoc …)
48    @isteps_interact
49    /2/
50] qed.
51
52lemma is_final_elim: ∀s.∀P:option int → Type[0].
53 (∀r. final_state s r → P (Some ? r)) →
54 ((¬∃r.final_state s r) → P (None ?)) →
55P (is_final s).
56#s #P #F #NF lapply (refl ? (is_final s))
57cases (is_final s) in ⊢ (???% → %);
58[ #E @NF % * #r #H whd in E:(??%?); > (is_final_complete … H) in E; #H destruct
59| #r #E @F @is_final_sound @E
60] qed.
61
62lemma is_final_elim': ∀ge,s.∀P:option int → Type[0].
63 (∀r. final_state s r → P (Some ? r)) →
64 ((¬∃r.final_state s r) → P (None ?)) →
65P (is_final io_out io_in clight_fullexec ge s).
66#ge @is_final_elim qed.
67
68lemma exec_e_step: ∀ge,x,tr,s,e.
69  exec_inf_aux ?? clight_exec ge x = e_step ??? tr s e →
70  exec_inf_aux ?? clight_exec ge (exec_step ge s) = e.
71#ge #x #tr #s #e
72>(exec_inf_aux_unfold …) cases x;
73[ #o #k #EXEC whd in EXEC:(??%?); destruct
74| #y cases y #tr' #s' whd in ⊢ (??%? → ?);
75  @is_final_elim'
76  [ #r #FINAL | #FINAL ]
77  #EXEC whd in EXEC:(??%?); destruct @refl
78| #msg #EXEC whd in EXEC:(??%?); destruct
79] qed.
80
81lemma exec_e_step_inv: ∀ge,x,tr,s,e.
82  exec_inf_aux ?? clight_exec ge x = e_step ??? tr s e →
83  x = Value ??? 〈tr,s〉.
84#ge #x #tr #s #e
85>(exec_inf_aux_unfold …) cases x;
86[ #o #k #EXEC whd in EXEC:(??%?); destruct
87| #y cases y; #tr' #s' whd in ⊢ (??%? → ?);
88  @is_final_elim'
89  [ #r ] #FINAL #EXEC whd in EXEC:(??%?);
90  destruct @refl
91| #msg #EXEC whd in EXEC:(??%?); destruct
92] qed.
93
94lemma exec_e_step_inv2: ∀ge,x,tr,s,e.
95  exec_inf_aux ?? clight_exec ge x = e_step ??? tr s e →
96  ¬∃r.final_state s r.
97#ge #x #tr #s #e
98>(exec_inf_aux_unfold …) cases x;
99[ #o #k #EXEC whd in EXEC:(??%?); destruct
100| #y cases y; #tr' #s' whd in ⊢ (??%? → ?);
101  @is_final_elim' [ #r ] #F #EXEC whd in EXEC:(??%?); destruct @F
102| #msg #EXEC whd in EXEC:(??%?); destruct
103] qed.
104
105definition exec_from : genv → state → s_execution → Prop ≝
106λge,s,se. single_exec_of (exec_inf_aux ?? clight_exec ge (exec_step ge s)) se.
107
108lemma se_step_eq : ∀tr,s,e,tr',s',e'.
109 se_step tr s e = se_step tr' s' e' →
110 tr = tr' ∧ s = s' ∧ e = e'.
111#tr #s #e #tr' #s' #e' #E destruct
112% try % @refl qed.
113
114lemma exec_from_step : ∀ge,s,tr,s',e.
115exec_from ge s (se_step tr s' e) →
116exec_step ge s = Value ??? 〈tr,s'〉 ∧ exec_from ge s' e.
117#ge #s0 #tr0 #s0' #e0 #H inversion H;
118[ #tr #r #m #E1 #E2 destruct
119| #tr #s #e #se #H1 #H2 #E (* destruct (E) ;*)
120  cases (se_step_eq … E) * #E1 #E2 #E3 #E4 >E1 >E2 >E3
121    >(exec_e_step_inv … H2)
122    <(exec_e_step … H2) in H1; #H1 % //
123| #msg #_ #E destruct
124| #o #k #i #se #H1 #H2 #E destruct
125] qed.
126
127lemma exec_from_interact : ∀ge,s,o,k,i,tr,s',e.
128exec_from ge s (se_interact o k i (se_step tr s' e)) →
129step ge s tr s' ∧
130(*exec_step ge s = Value ??? 〈tr,s'〉 ∧*) exec_from ge s' e.
131#ge #s0 #o0 #k0 #i0 #tr0 #s0' #e0 #H inversion H;
132[ #tr #r #m #E1 #E2 destruct
133| #tr #s #e #se #H1 #H2 #E destruct (E)
134| #msg #_ #E destruct
135| #o #k #i #se #H1 #H2 #E #X destruct (E);
136    lapply (exec_step_sound ge s0);
137    cases (exec_step ge s0) in H2 ⊢ %;
138    [ #o' #k' >(exec_inf_aux_unfold …)
139        #E' whd in E':(??%??); destruct (E');
140        #STEP
141        inversion H1;
142        [ #tr #r #m #E1 #E2 destruct
143        | #tr' #s' #e' #se' #H2 #H3 #E2 #_ destruct (E2);
144            <(exec_e_step … H3) in H2; #H2 % [ 2: @H2 ]
145            lapply (STEP i);
146            >(exec_e_step_inv … H3)
147            #S @S
148        | #msg #_ #E destruct
149        | #o #k #i #se #H1 #H2 #E destruct
150        ]
151    | #x cases x; #tr' #s' >(exec_inf_aux_unfold …)
152        whd in ⊢ (??%?? → ?); @is_final_elim'
153        [ #r ] #F #E whd in E:(??%??); destruct
154    | #msg >(exec_inf_aux_unfold …)
155        #E' whd in E':(??%??); destruct (E');
156    ]
157] qed.
158
159lemma exec_from_interact_stop : ∀ge,s,o,k,i,tr,r.
160exec_from ge s (se_interact o k i (se_stop tr r)) →
161step ge s tr (Finalstate r).
162#ge #s0 #o0 #k0 #i0 #tr0 #r0 #H inversion H
163[ #tr #r #m #E1 #E2 destruct
164| #tr #s #e #se #H1 #H2 #E destruct (E)
165| #msg #_ #E destruct
166| #o #k #i #se #H1 #H2 #E #_ destruct (E)
167    lapply (exec_step_sound ge s0)
168    >(exec_inf_aux_unfold …) in H2;
169    cases (exec_step ge s0)
170    [ #o' #k'
171        #E' whd in E':(??%??); destruct (E');
172        #STEP
173        inversion H1;
174        [ #tr #r #m #E1 #E2 #_ lapply (STEP i); destruct;
175            >(exec_inf_aux_unfold …) in E1;
176            cases (k' i);
177            [ #o2 #k2 #E whd in E:(??%??); destruct (E)
178            | #x cases x; #tr2 #s2 whd in ⊢ (??%?? → ?);
179                lapply (is_final_elim s2) #IFE whd in IFE:(∀_. ? → ? → ?%);
180                change with (is_final s2) in match (is_final ?????);
181                @IFE
182                [ #r' #FINAL #E whd in E:(??%??);
183                    destruct (E);
184                    inversion FINAL;
185                    #r'' #m'' #E1 #E2 destruct (E1 E2); //;
186                | #NF #E whd in E:(??%??); destruct (E)
187                ]
188            | #msg #E whd in E:(??%??); destruct (E)
189            ]
190       | #tr #s #e #e' #H #EXEC #E destruct (E)
191       | #msg #EXEC #E destruct (E)
192       | #o2 #k2 #i2 #e2 #H #EXEC #E destruct (E)
193       ]
194   | #x cases x; #tr #s whd in ⊢ (??%?? → ?);
195       @is_final_elim' [ #r ] #F #E whd in E:(??%??); destruct (E)
196   | #msg #E whd in E:(??%??); destruct (E)
197   ]
198] qed.
199
200(* NB: the E0 in the execs are irrelevant. *)
201lemma several_steps: ∀ge,tr,e,e',s,s'.
202  execution_isteps tr s e s' e' →
203  exec_from ge s e →
204  star (mk_transrel … step) ge s tr s' ∧
205  exec_from ge s' e'.
206#ge #tr0 #e0 #e0' #s0 #s0' #H
207elim H;
208[ #s #e #EXEC % //;
209| #e1 #e2 #tr1 #tr2 #s1 #s2 #s3 #STEPS #IH #EXEC
210    elim (exec_from_step … EXEC); #EXEC3 #EXEC1
211    elim (IH EXEC1);
212    #STAR12 #EXEC2 % //;
213    lapply (exec_step_sound ge s3);
214    >EXEC3 #STEP3
215    @(star_step (mk_transrel ?? step) … STEP3 STAR12)
216    @refl
217| #e1 #e2 #o #k #i #s1 #s2 #s3 #tr1 #tr2 #STEPS #IH #EXEC
218    elim (exec_from_interact … EXEC);
219    #STEP3 #EXEC1
220    elim (IH EXEC1); #STAR #EXEC2
221    %
222    [ @(star_step (mk_transrel ?? step) … STEP3 STAR)
223        @refl
224    | //
225    ]
226] qed.
227
228inductive execution_terminates : trace → state → s_execution → int → Prop ≝
229| terminates : ∀s,s',tr,tr',r,e.
230    execution_isteps tr s e s' (se_stop tr' r) →
231    execution_terminates (tr⧺tr') s (se_step E0 s e) r
232(* We should only be able to get to here if main is an external function, which is silly. *)
233| annoying_corner_case_terminates: ∀s,s',tr,tr',r,e,o,k,i.
234    execution_isteps tr s e s' (se_interact o k i (se_stop tr' r)) →
235    execution_terminates (tr⧺tr') s (se_step E0 s e) r.
236
237coinductive execution_diverging : s_execution → Prop ≝
238| diverging_step : ∀s,e. execution_diverging e → execution_diverging (se_step E0 s e).
239
240(* Makes a finite number of interactions (including cost labels) before diverging. *)
241inductive execution_diverges : trace → state → s_execution → Prop ≝
242| diverges_diverging: ∀tr,s,s',e,e'.
243    execution_isteps tr s e s' e' →
244    execution_diverging e' →
245    execution_diverges tr s (se_step E0 s e).
246
247(* NB: "reacting" includes hitting a cost label. *)
248coinductive execution_reacting : traceinf → state → s_execution → Prop ≝
249| reacting: ∀tr,tr',s,s',e,e'.
250    execution_reacting tr' s' e' →
251    execution_isteps tr s e s' e' →
252    tr ≠ E0 →
253    execution_reacting (tr⧻tr') s e.
254
255inductive execution_reacts : traceinf → state → s_execution → Prop ≝
256| reacts: ∀tr,s,e.
257    execution_reacting tr s e →
258    execution_reacts tr s (se_step E0 s e).
259
260inductive execution_goes_wrong: trace → state → s_execution → state → Prop ≝
261| go_wrong: ∀tr,s,s',e,msg.
262    execution_isteps tr s e s' (se_wrong msg) →
263    execution_goes_wrong tr s (se_step E0 s e) s'.
264
265let corec silent_sound ge s e
266  (H0:execution_diverging e)
267  (EXEC:exec_from ge s e)
268  : forever_silent (mk_transrel ?? step) … ge s ≝ ?.
269cut (∃s2.∃e2.And (And (execution_diverging e2) (step ge s E0 s2)) (exec_from ge s2 e2));
270[ cases H0 in EXEC ⊢ %; #s1 #e1 #H1 #EXEC
271    elim (exec_from_step … EXEC);
272    #EXEC0 #EXEC1
273    %{ s1} %{ e1} % //; % //;
274    lapply (exec_step_sound ge s); >EXEC0 whd in ⊢ (% → ?); #H @H
275| *; #s2 *; #e2 *; *; #H2 #STEP2 #EXEC2
276    @(forever_silent_intro (mk_transrel ?? step) … ge s s2 ? (silent_sound ge s2 e2 ??))
277    //;
278] qed.
279
280lemma final_step: ∀ge,tr,r,s.
281  exec_from ge s (se_stop tr r) →
282  step ge s tr (Finalstate r).
283#ge #tr #r #s #EXEC
284whd in EXEC;
285inversion EXEC;
286[ #tr' #r' #s' #EXEC' #E #_ destruct (E)
287    lapply (exec_step_sound ge s)
288    >(exec_inf_aux_unfold …) in EXEC';
289    cases (exec_step ge s)
290    [ #o #k #EXEC' whd in EXEC':(??%??); destruct (EXEC');
291    | #x cases x; #tr'' #s' whd in ⊢ (??%?? → ?);
292        @is_final_elim' [ #r'' #FINAL | #F ]
293        #EXEC' whd in EXEC':(??%??); destruct (EXEC');
294    | #msg #EXEC' whd in EXEC':(??%??); destruct (EXEC');
295    ]
296    inversion FINAL #r''' #E1 #E2 #_ #H destruct (E1 E2);
297    @H
298| #tr' #s' #e' #se' #H #EXEC' #E destruct
299| #msg #EXEC' #E destruct
300| #o #k #i #e #H #EXEC #E destruct
301] qed.
302
303
304lemma e_stop_inv: ∀ge,x,tr,r,s.
305  exec_inf_aux ?? clight_exec ge x = e_stop ??? tr r s →
306  x = Value ??? 〈tr,Finalstate r〉.
307#ge #x #tr #r #s
308>(exec_inf_aux_unfold …) cases x;
309[ #o #k #EXEC whd in EXEC:(??%?); destruct;
310| #z cases z; #tr' #s' whd in ⊢ (??%? → ?); @is_final_elim'
311  [ #r' #FINAL cases FINAL; #r'' #EXEC whd in EXEC:(??%?);
312      destruct (EXEC); @refl
313  | #F #EXEC whd in EXEC:(??%?); destruct (EXEC);
314  ]
315| #msg #EXEC whd in EXEC:(??%?); destruct (EXEC);
316] qed.
317
318lemma terminates_sound: ∀ge,tr,s,r,e.
319  execution_terminates tr s (se_step E0 s e) r →
320  exec_from ge s e →
321  star (mk_transrel … step) ge s tr (Finalstate r).
322#ge #tr0 #s0 #r #e0 #H inversion H;
323[ #s #s' #tr #tr' #r' #e #ESTEPS #E1 #E2 #E3 #E4 #_ #EXEC
324    destruct (E1 E2 E3 E4 E5);
325    cases (several_steps … ESTEPS EXEC); #STARs' #EXECs'
326    @(star_right … STARs')
327    [ 2: @(final_step ge tr' r' s' … EXECs')
328    | skip
329    | @refl
330    ]
331| #s #s' #tr #tr' #r' #e #o #k #i #ESTEPS #E1 #E2 #E3 #E4 #_ #EXEC
332    destruct
333    cases (several_steps … ESTEPS EXEC) #STARs' #EXECs'
334    @(star_right … STARs')
335    [ @tr'
336    | @(exec_from_interact_stop … EXECs')
337    | @refl
338    ]
339] qed.
340
341let corec reacts_sound ge tr s e
342  (REACTS:execution_reacting tr s e)
343  (EXEC:exec_from ge s e) :
344  forever_reactive (mk_transrel … step) ge s tr ≝ ?.
345cut (∃s'.∃e'.∃tr'.∃tr''.(And (And (And (execution_reacting tr'' s' e') (execution_isteps tr' s e s' e')) (tr' ≠ E0)) (tr = tr'⧻tr'')));
346[ inversion REACTS;
347    #tr0 #tr' #s0 #s' #e0 #e' #EREACTS #ESTEPS #REACTED #E1 #E2 #E3 #_ destruct (E2 E3);
348    %{ s'} %{ e'} %{ tr0} %{ tr'} % [ % [ % //; | @REACTED ] | @refl ]
349| *; #s' *; #e' *; #tr' *; #tr''
350    *; *; *; #REACTS' #ESTEPS #REACTED #APPTR
351(*    >APPTR *)
352    @(match sym_eq ??? APPTR return λx.λ_.forever_reactive (mk_transrel genv state step) ge s x with [ refl ⇒ ? ])
353    %
354    cases (several_steps … ESTEPS EXEC); #STEPS #EXEC'
355    [ 2: @STEPS
356    | skip
357    | @REACTED
358    | @reacts_sound
359      [ 2: @REACTS'
360      | skip
361      | @EXEC'
362      ]
363    ]
364qed.
365
366lemma exec_from_wrong: ∀ge,s,msg.
367  exec_from ge s (se_wrong msg) →
368  exec_step ge s = Wrong ??? msg.
369#ge #s #msg #H whd in H;
370inversion H;
371[ #tr #r #m #EXEC #E destruct (E)
372| #tr #s' #e #e' #H #EXEC #E destruct (E)
373| #msg #EXEC #H #_ generalize in match H; -H; generalize in match EXEC; -EXEC;
374  generalize in match msg; -msg; >(exec_inf_aux_unfold …)
375    cases (exec_step ge s);
376  [ #o #k #msg' #EXEC whd in EXEC:(??%??); destruct
377  | #x cases x; #tr #s' #msg' whd in ⊢ (??%?? → ?); @is_final_elim'
378      [ #r ] #F #EXEC whd in EXEC:(??%??); destruct
379  | #msg1 #msg2 #EXEC #E whd in EXEC:(??%??); destruct @refl
380  ]
381| #o #k #i #e #H #EXEC #E destruct
382] qed.
383
384lemma exec_from_step_notfinal: ∀ge,s,tr,s',e.
385  exec_from ge s (se_step tr s' e) →
386  ¬(∃r. final_state s' r).
387#ge #s #tr #s' #e #H whd in H; inversion H;
388[ #tr' #r #m #EXEC #E destruct
389| #tr' #s'' #e' #e'' #H #EXEC #E #_ destruct (E);
390    >(exec_inf_aux_unfold …) in EXEC;
391    cases (exec_step ge s);
392    [ #o #k #EXEC whd in EXEC:(??%??); destruct
393    | #x cases x; #tr1 #s1 whd in ⊢ (??%?? → ?); @is_final_elim'
394        [ #r ] #F #E whd in E:(??%??); destruct @F
395    | #msg #E whd in E:(??%??); destruct
396    ]
397| #msg #EXEC #E destruct
398| #o #k #i #e' #H #EXEC #E destruct
399] qed.
400
401lemma exec_from_interact_step_notfinal: ∀ge,s,o,k,i,tr,s',e.
402  exec_from ge s (se_interact o k i (se_step tr s' e)) →
403  ¬(∃r. final_state s' r).
404#ge #s #o #k #i #tr #s' #e #H
405% *; #r #F cases F in H; #r' #H
406inversion H;
407[ #tr' #r #m #EXEC #E destruct
408| #tr' #s'' #e' #e'' #H #EXEC #E destruct (E);
409| #msg #EXEC #E destruct
410| #o' #k' #i' #e' #H #EXEC #E #_ destruct;
411    >(exec_inf_aux_unfold …) in EXEC;
412    cases (exec_step ge s);
413    [ #o1 #k1 #EXEC1 whd in EXEC1:(??%??); destruct (EXEC1);
414        inversion H;
415        [ #tr1 #r1 #m1 #EXECK #E destruct (E);
416        | #tr1 #s1 #e1 #e2 #H1 #EXECK #E #_ destruct (E);
417            >(exec_inf_aux_unfold …) in EXECK;
418            cases (k1 i');
419            [ #o2 #k2 #EXECK whd in EXECK:(??%??); destruct
420            | #x cases x; #tr2 #s2 whd in ⊢ (??%?? → ?);
421                lapply (is_final_elim s2) #IFE whd in IFE:(∀_. ? → ? → ?%);
422                change with (is_final s2) in match (is_final ?????);
423                @IFE [ #r ] #F #EXECK
424                whd in EXECK:(??%??); destruct;
425                @(absurd ?? F)
426                %{ r'} //;
427            | #msg #E whd in E:(??%??); destruct
428            ]
429        | #msg #EXECK #E  whd in E:(??%??); destruct
430        | #o2 #k2 #i2 #e2 #H2 #EXECK #E destruct
431        ]
432    | #x cases x; #tr1 #s1 whd in ⊢ (??%?? → ?);
433        @is_final_elim' [ #r ] #F #E whd in E:(??%??); destruct;
434    | #msg #E whd in E:(??%??); destruct
435    ]
436] qed.
437
438lemma wrong_sound: ∀ge,tr,s,s',e.
439  execution_goes_wrong tr s (se_step E0 s e) s' →
440  exec_from ge s e →
441  (¬∃r. final_state s r) →
442  star (mk_transrel … step) ge s tr s' ∧
443  nostep (mk_transrel … step) ge s' ∧
444  (¬∃r. final_state s' r).
445#ge #tr0 #s0 #s0' #e0 #WRONG inversion WRONG;
446#tr #s #s' #e #msg #ESTEPS #E1 #E2 #E3 #E4 #_ #EXEC #NOTFINAL destruct (E1 E2 E3 E4);
447cases (several_steps … ESTEPS EXEC);
448#STAR #EXEC' %
449[ % [ @STAR
450       | #badtr #bads % #badSTEP
451           lapply (step_complete … badSTEP);
452           >(exec_from_wrong … EXEC')
453           //;
454       ]
455| %
456    elim ESTEPS in NOTFINAL EXEC ⊢ %;
457    [ #s1 #e1 #NF #EX #F @(absurd ? F NF)
458    | #e1 #e2 #tr1 #tr2 #s1 #s2 #s3 #ESTEPS1 #IH #NF #EXEC
459        cases (exec_from_step … EXEC); #EXEC3 #EXEC1
460        @(IH … EXEC1)
461        @(exec_from_step_notfinal … EXEC)
462    | #e1 #e2 #o #k #i #s1 #s2 #s3 #tr1 #tr2 #ESTEPS1 #IH #NF #EXEC
463        @IH
464        [ @(exec_from_interact_step_notfinal … EXEC)
465        | cases (exec_from_interact … EXEC) #STEP #EF1 @EF1
466        ]
467    ]
468] qed.
469
470inductive execution_characterisation : state → s_execution → Prop ≝
471| ec_terminates: ∀s,r,e,tr.
472    execution_terminates tr s e r →
473    execution_characterisation s e
474| ec_diverges: ∀s,e,tr.
475    execution_diverges tr s e →
476    execution_characterisation s e
477| ec_reacts: ∀s,e,tr.
478    execution_reacts tr s e →
479    execution_characterisation s e
480| ec_wrong: ∀e,s,s',tr.
481    execution_goes_wrong tr s e s' →
482    execution_characterisation s e.
483
484(* bit of a hack to avoid inability to reduce term in match *)
485definition interact_prop : ∀A:Type[0].(∀o:io_out. (io_in o → IO io_out io_in A) → Prop) → IO io_out io_in A → Prop ≝
486λA,P,e. match e return λ_.Prop with [ Interact o k ⇒ P o k | _ ⇒ True ].
487
488lemma err_does_not_interact: ∀A,B,P,e1,e2.
489  (∀x:B.interact_prop A P (e2 x)) →
490  interact_prop A P (bindIO ?? B A (err_to_io ??? e1) e2).
491#A #B #P #e1 #e2 #H
492cases e1; //; qed.
493
494lemma err2_does_not_interact: ∀A,B,C,P,e1,e2.
495  (∀x,y.interact_prop A P (e2 x y)) →
496  interact_prop A P (bindIO2 ?? B C A (err_to_io ??? e1) e2).
497#A #B #C #P #e1 #e2 #H
498cases e1; [ #z cases z; ] //; qed.
499
500lemma err_sig_does_not_interact: ∀A,B,P.∀Q:B→Prop.∀e1,e2.
501  (∀x.interact_prop A P (e2 x)) →
502  interact_prop A P (bindIO ?? (Sig B Q) A (err_to_io_sig ??? Q e1) e2).
503#A #B #P #Q #e1 #e2 #H
504cases e1; //; qed.
505
506lemma opt_does_not_interact: ∀A,B,P,e1,e2,msg.
507  (∀x:B.interact_prop A P (e2 x)) →
508  interact_prop A P (bindIO ?? B A (opt_to_io ??? msg e1) e2).
509#A #B #P #e1 #e2 #msg #H
510cases e1; //; qed.
511
512lemma exec_step_interaction:
513  ∀ge,s. interact_prop ? (λo,k. ∀i.∃tr.∃s'. k i = Value ??? 〈tr,s'〉 ∧ tr ≠ E0) (exec_step ge s).
514#ge #s cases s;
515[ #f #st #kk #e #m cases st;
516  [ 11,14: #a | 2,4,6,7,12,13,15: #a #b | 3,5: #a #b #c | 8: #a #b #c #d ]
517  [ 4,6,8,9: @I ]
518  whd in ⊢ (???%);
519  [ cases a; [ cases (fn_return f); //; | #e whd nodelta in ⊢ (???%);
520                    cases (type_eq_dec (fn_return f) Tvoid); #x //; @err2_does_not_interact // ]
521  | cases (find_label a (fn_body f) (call_cont kk)); [ @I | #z cases z #x #y @I ]
522  | @err2_does_not_interact #x1 #x2 @err2_does_not_interact #x3 #x4 @opt_does_not_interact #x5 @I
523  | 4,7: @err2_does_not_interact #x1 #x2 @err_does_not_interact #x3 @I
524  | @err2_does_not_interact #x1 #x2 cases x1; //;
525  | @err2_does_not_interact #x1 #x2 @err2_does_not_interact #x3 #x4 @opt_does_not_interact #x5  @err_does_not_interact #x6 cases a;
526      [ @I | #x7 @err2_does_not_interact #x8 #x9 @I ]
527  | cases (is_Sskip a); #H [ @err2_does_not_interact #x1 #x2 @err_does_not_interact #x3 @I
528      | @I ]
529  | cases kk; [ 1,8: cases (fn_return f); //; | 2,3,5,6,7: //;
530      | #z1 #z2 #z3 @err2_does_not_interact #x1 #x2 @err_does_not_interact #x3 cases x3; @I ]
531  | cases kk; //;
532  | cases kk; [ 4: #z1 #z2 #z3  @err2_does_not_interact #x1 #x2 @err_does_not_interact #x3 cases x3; @I
533      | *: // ]
534  ]
535| #f #args #kk #m cases f;
536  [ #f' whd in ⊢ (???%); cases (exec_alloc_variables empty_env m (fn_params f'@fn_vars f'))
537    #x1 #x2 whd in ⊢ (???%); @err_does_not_interact //
538  (* This is the only case that actually matters! *)
539  | #fn #argtys #rty whd in ⊢ (???%);
540      @err_does_not_interact #x1
541      whd; #i % [ 2: % [ 2: % [ % whd in ⊢ (??%?); @refl
542        | % #E whd in E:(??%%); destruct (E); ] ] ]
543  ]
544| #v #kk #m whd in ⊢ (???%); cases kk;
545    [ cases v // * //
546    | 8: #x1 #x2 #x3 #x4 cases x1;
547      [ whd in ⊢ (???%); cases v; // | #x5 whd in ⊢ (???%); cases x5;
548          #x6 #x7 @opt_does_not_interact // ]
549    | *: // ]
550| #r //
551] qed.
552
553
554(* Some classical logic (roughly like a fragment of Coq's library) *)
555lemma classical_doubleneg:
556  ∀classic:(∀P:Prop.P ∨ ¬P).
557  ∀P:Prop. ¬ (¬ P) → P.
558#classic #P *; #H
559cases (classic P);
560[ // | #H' @False_ind /2/; ]
561qed.
562
563lemma classical_not_all_not_ex:
564  ∀classic:(∀P:Prop.P ∨ ¬P).
565  ∀A:Type[0].∀P:A → Prop. ¬ (∀x. ¬ P x) → ∃x. P x.
566#classic #A #P *; #H
567@(classical_doubleneg classic) % *; #H'
568@H #x % #H'' @H' %{x} @H''
569qed.
570
571lemma classical_not_all_ex_not:
572  ∀classic:(∀P:Prop.P ∨ ¬P).
573  ∀A:Type[0].∀P:A → Prop. ¬ (∀x. P x) → ∃x. ¬ P x.
574#classic #A #P *; #H
575@(classical_not_all_not_ex classic A (λx.¬ P x))
576% #H' @H #x @(classical_doubleneg classic)
577@H'
578qed.
579
580lemma not_ex_all_not:
581  ∀A:Type[0].∀P:A → Prop. ¬ (∃x. P x) → ∀x. ¬ P x.
582#A #P *; #H #x % #H'
583@H %{ x} @H'
584qed.
585
586lemma not_imply_elim:
587  ∀classic:(∀P:Prop.P ∨ ¬P).
588  ∀P,Q:Prop. ¬ (P → Q) → P.
589#classic #P #Q *; #H
590@(classical_doubleneg classic) % *; #H'
591@H #H'' @False_ind @H' @H''
592qed.
593
594lemma not_imply_elim2:
595  ∀P,Q:Prop. ¬ (P → Q) → ¬ Q.
596#P #Q *; #H % #H'
597@H #_ @H'
598qed.
599
600lemma imply_to_and:
601  ∀classic:(∀P:Prop.P ∨ ¬P).
602  ∀P,Q:Prop. ¬ (P → Q) → P ∧ ¬Q.
603#classic #P #Q #H %
604[ @(not_imply_elim classic P Q H)
605| @(not_imply_elim2 P Q H)
606] qed.
607
608lemma not_and_to_imply:
609  ∀classic:(∀P:Prop.P ∨ ¬P).
610  ∀P,Q:Prop. ¬ (P ∧ Q) → P → ¬Q.
611#classic #P #Q *; #H #H'
612% #H'' @H % //;
613qed.
614
615inductive execution_not_over : s_execution → Prop ≝
616| eno_step: ∀tr,s,e. execution_not_over (se_step tr s e)
617| eno_interact: ∀o,k,tr,s,e,i. execution_not_over (se_interact o k i (se_step tr s e)).
618
619lemma eno_stop: ∀tr,r. execution_not_over (se_stop tr r) → False.
620#tr0 #r0 #H inversion H;
621[ #tr #s #e #E destruct
622| #o #k #tr #s #e #i #E destruct
623] qed.
624
625lemma eno_wrong: ∀msg. execution_not_over (se_wrong msg) → False.
626#msg #H inversion H;
627[ #tr #s #e #E destruct
628| #o #k #tr #s #e #i #E destruct
629] qed.
630
631let corec show_divergence s e
632 (NONTERMINATING:∀tr1,s1,e1. execution_isteps tr1 s e s1 e1 →
633                 execution_not_over e1)
634 (UNREACTIVE:∀tr2,s2,e2. execution_isteps tr2 s e s2 e2 → tr2 = E0)
635 (CONTINUES:∀tr2,s2,o,k,i,e'. execution_isteps tr2 s e s2 (se_interact o k i e') → ∃tr3.∃s3.∃e3. And (e' = se_step tr3 s3 e3) (tr3 ≠ E0))
636 : execution_diverging e ≝ ?.
637lapply (NONTERMINATING E0 s e ?); //;
638cases e in UNREACTIVE NONTERMINATING CONTINUES ⊢ %;
639[ #tr #i #_ #_ #_ #ENO elim (eno_stop … ENO);
640| #tr #s' #e' #UNREACTIVE lapply (UNREACTIVE tr s' e' ?);
641  [ <(E0_right tr) in ⊢ (?%????);
642      @isteps_one @isteps_none
643  | #TR @(match sym_eq ??? TR with [ refl ⇒ ? ]) (* >TR in UNREACTIVE ⊢ % *)
644      #NONTERMINATING #CONTINUES #_ %
645      @(show_divergence s')
646      [ #tr1 #s1 #e1 #S @(NONTERMINATING tr1 s1 e1)
647        change with (Eapp E0 tr1) in ⊢ (?%????); @isteps_one
648        @S
649      | #tr2 #s2 #e2 #S >TR in UNREACTIVE; #UNREACTIVE @(UNREACTIVE tr2 s2 e2)
650          change with (Eapp E0 tr2) in ⊢ (?%????);
651          @isteps_one @S
652      | #tr2 #s2 #o #k #i #e2 #S @(CONTINUES tr2 s2 o k i)
653          change with (Eapp E0 tr2) in ⊢ (?%????);
654          @(isteps_one … S)
655      ]
656  ]
657| #msg #_ #_ #_ #ENO elim (eno_wrong … ENO);
658| #o #k #i #e' #UNREACTIVE #NONTERMINATING #CONTINUES #_
659    lapply (CONTINUES E0 s o k i e' (isteps_none …));
660    *; #tr' *; #s' *; #e' *; #EXEC #NOTSILENT
661    @False_ind @(absurd ?? NOTSILENT)
662    @(UNREACTIVE … s' e')
663    <(E0_right tr') in ⊢ (?%????);
664    >EXEC
665    @isteps_interact //;
666] qed.
667
668lemma se_inv: ∀e1,e2.
669  single_exec_of e1 e2 →
670  match e1 with
671  [ e_stop tr r s ⇒ match e2 with [ se_stop tr' r' ⇒ tr = tr' ∧ r = r' | _ ⇒ False ]
672  | e_step tr s e1' ⇒ match e2 with [ se_step tr' s' e2' ⇒ tr = tr' ∧ s = s' ∧ single_exec_of e1' e2' | _ ⇒ False ]
673  | e_wrong _ ⇒ match e2 with [ se_wrong _ ⇒ True | _ ⇒ False ]
674  | e_interact o k ⇒ match e2 with [ se_interact o' k' i e ⇒ o' = o ∧ k' ≃ k ∧ single_exec_of (k' i) e | _ ⇒ False ]
675  ].
676#e01 #e02 #H
677cases H;
678[ #tr #r #s whd; % [ % ] //
679| #tr #s #e1' #e2' #H' whd; % [ % ] //
680| #msg whd; //
681| #o #k #i #e #H' whd; % [ % ] //
682] qed.
683
684lemma interaction_is_not_silent: ∀ge,o,k,i,tr,s,s',e.
685  exec_from ge s (se_interact o k i (se_step tr s' e)) →
686  tr ≠ E0.
687#ge #o #k #i #tr #s #s' #e whd in ⊢ (% → ?); >(exec_inf_aux_unfold …)
688lapply (exec_step_interaction ge s);
689cases (exec_step ge s);
690[ #o' #k' ; whd in ⊢ (% → ?%? → ?); #H #K cases (se_inv … K);
691    *; #E1 #E2 #H1 destruct (E1);
692    lapply (H i); *; #tr' *; #s'' *; #K' #TR
693    >E2 in H1; #H1 whd in H1:(?%?); >K' in H1;
694    >(exec_inf_aux_unfold …) whd in ⊢ (?%? → ?);
695    change with (is_final s'') in match (is_final ?????);
696    @is_final_elim
697    [ #r #F whd in ⊢ (?%? → ?); #S
698        @False_ind @(absurd ? S) cases (se_inv … S)
699    | #NF #S whd in S:(?%?); cases (se_inv … S);
700        *; #E1 #E2 #S' <E1 @TR
701    ]
702| #x cases x; #tr' #s'' #H whd in ⊢ (?%? → ?);
703    @is_final_elim' [ #r ] #F #E whd in E:(?%?);
704    inversion E;
705    [ 1,5: #tr1 #e1 #m1 #E1 #E2 destruct
706    | 2,6: #tr #s1 #e1 #e2 #H #E1 #E2 destruct
707    | 3,7: #msg #E destruct
708    | 4,8: #o1 #k1 #i1 #e1 #H1 #E1 #E2 destruct
709    ]
710| #msg #_ #E whd in E:(?%?);
711    inversion E;
712    [ 1,5: #tr1 #e1 #m1 #E1 #E2 destruct
713    | 2,6: #tr #s1 #e1 #e2 #H #E1 #E2 destruct
714    | 3,7: #msg #E1 #E2 destruct
715    | 4,8: #o1 #k1 #i1 #e1 #H1 #E1 #E2 destruct
716    ]
717] qed.
718
719let corec reactive_traceinf' ge s e
720  (EXEC:exec_from ge s e)
721  (REACTIVE: ∀tr,s1,e1.
722    execution_isteps tr s e s1 e1 →
723    (Σx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0))
724  : traceinf' ≝ ?.
725lapply (REACTIVE E0 s e (isteps_none …));
726*; #x cases x; #tr #y cases y; #s' #e' *; #STEPS #H
727%{ tr ? H}
728@(reactive_traceinf' ge s' e' ?)
729[ cases (several_steps … STEPS EXEC); #_ #H' @H'
730| #tr1 #s1 #e1 #STEPS1
731    @REACTIVE
732    [ 2:
733        @(isteps_trans … STEPS STEPS1)
734    | skip
735    ]
736]
737qed.
738
739(* A slightly different version of the above, to work around a problem with the
740   next result. *)
741let corec reactive_traceinf'' ge s e
742  (EXEC:exec_from ge s e)
743  (REACTIVE0: Σx.execution_isteps (\fst x) s e (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0)
744  (REACTIVE: ∀tr,s1,e1.
745    execution_isteps tr s e s1 e1 →
746    (Σx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0))
747  : traceinf' ≝ ?.
748cases REACTIVE0; #x cases x; #tr #y cases y; #s' #e' *; #STEPS #H
749%{ tr ? H}
750@(reactive_traceinf'' ge s' e' ?)
751[ cases (several_steps … STEPS EXEC); #_ #H' @H'
752| @(REACTIVE … STEPS)
753| #tr1 #s1 #e1 #STEPS1
754    @REACTIVE
755    [ 2:
756        @(isteps_trans … STEPS STEPS1)
757    | skip
758    ]
759] qed.
760
761(* We want to prove
762
763lemma show_reactive : ∀ge,s.
764  ∀REACTIVE:∀tr,s1,e1.
765    execution_isteps tr s (exec_inf_aux ge (exec_step ge s)) s1 e1 →
766    Σx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0.
767  execution_reacting (traceinf_of_traceinf' (reactive_traceinf' ge s REACTIVE)) s (exec_inf_aux ge (exec_step ge s)).
768 
769but the current matita won't unfold reactive_traceinf' so that we can do case
770analysis on (REACTIVE …).  Instead we take an "applied" version of REACTIVE that
771we can do case analysis on, then get it into the desired form afterwards.
772*)
773let corec show_reactive' ge s e
774  (EXEC:exec_from ge s e)
775  (REACTIVE0: Σx.execution_isteps (\fst x) s e (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0)
776  (REACTIVE: ∀tr1,s1,e1.
777    execution_isteps tr1 s e s1 e1 →
778    (Σx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0))
779  : execution_reacting (traceinf_of_traceinf' (reactive_traceinf'' ge s e EXEC REACTIVE0 REACTIVE)) s e ≝ ?.
780(*>(unroll_traceinf' (reactive_traceinf'' …)) *)
781@(match sym_eq ??? (unroll_traceinf' (reactive_traceinf'' …)) with [ refl ⇒ ? ])
782cases REACTIVE0;
783#x cases x; #tr1 #y cases y; #s1 #e1 #z cases z; #STEPS #NOTSILENT
784whd in ⊢ (?(?%)??);
785(*>(traceinf_traceinfp_app …) *)
786@(match sym_eq ??? (traceinf_traceinfp_app …) with [ refl ⇒ ? ])
787@(reacting … STEPS NOTSILENT)
788@show_reactive'
789qed.
790
791lemma show_reactive : ∀ge,s,e.
792  ∀EXEC:exec_from ge s e.
793  ∀REACTIVE:∀tr,s1,e1.
794    execution_isteps tr s e s1 e1 →
795    (Σx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0).
796  execution_reacting (traceinf_of_traceinf' (reactive_traceinf'' ge s e EXEC ? REACTIVE)) s e.
797[ #ge #s #e #EXEC #REACTIVE
798    @show_reactive'
799| @(REACTIVE … (isteps_none …))
800] qed.
801
802lemma execution_characterisation_complete:
803  ∀classic:(∀P:Prop.P ∨ ¬P).
804  ∀constructive_indefinite_description:(∀A:Type[0]. ∀P:A→Prop. (∃x. P x) → Sig A P).
805   ∀ge,s,e.
806   exec_from ge s e →
807   execution_characterisation s (se_step E0 s e).
808#classic #constructive_indefinite_description #ge #s #e #EXEC
809cases (classic (∀tr1,s1,e1. execution_isteps tr1 s e s1 e1 →
810                 execution_not_over e1));
811[ #NONTERMINATING
812    cases (classic (∃tr,s1,e1. execution_isteps tr s e s1 e1 ∧
813                     ∀tr2,s2,e2. execution_isteps tr2 s1 e1 s2 e2 → tr2 = E0));
814  [ *; #tr *; #s1 *; #e1 *; #INITIAL #UNREACTIVE
815      @(ec_diverges … s ? tr)
816      @(diverges_diverging … INITIAL)
817      @(show_divergence s1 e1)
818      [ #tr2 #s2 #e2 #S @(NONTERMINATING (Eapp tr tr2) s2 e2)
819          @(isteps_trans … INITIAL S)
820      | #tr2 #s2 #e2 #S @(UNREACTIVE … S)
821      | #tr2 #s2 #o #k #i #e2 #STEPS
822          lapply (NONTERMINATING (Eapp tr tr2) s2 (se_interact o k i e2) ?);
823          [ @(isteps_trans … INITIAL STEPS) ]
824          #NOTOVER inversion NOTOVER;
825          [ #tr' #s' #e' #E destruct (E);
826          | #o' #k' #tr' #s' #e' #i' #E #_ destruct (E);
827              %{ tr'} %{s'} %{e'} % //;
828              cases (several_steps … INITIAL EXEC); #_ #EXEC1
829              cases (several_steps … STEPS EXEC1); #_ #EXEC2
830              @(interaction_is_not_silent … EXEC2)
831          ]
832      ]
833
834  | *; #NOTUNREACTIVE
835      cut (∀tr,s1,e1.execution_isteps tr s e s1 e1 →
836            ∃x.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0);
837      [ #tr #s1 #e1 #STEPS
838          @(classical_doubleneg classic) % #NOREACTION
839          @NOTUNREACTIVE
840          %{ tr} %{s1} %{e1} % //;
841          #tr2 #s2 #e2 #STEPS2
842          lapply (not_ex_all_not … NOREACTION); #NR1
843          lapply (not_and_to_imply classic … (NR1 〈tr2,〈s2,e2〉〉)); #NR2
844          @(classical_doubleneg classic)
845          @NR2 normalize //
846      | #REACTIVE
847          @ec_reacts
848          [ 2: @reacts
849                   @(show_reactive ge s … EXEC)
850                   #tr #s1 #e1 #STEPS
851                   @constructive_indefinite_description
852                   @(REACTIVE … tr s1 e1 STEPS)
853          | skip
854          ]
855      ]
856  ]
857 
858| #NOTNONTERMINATING lapply (classical_not_all_ex_not classic … NOTNONTERMINATING);
859    *; #tr #NNT2 lapply (classical_not_all_ex_not classic … NNT2);
860    *; #s' #NNT3 lapply (classical_not_all_ex_not classic … NNT3);
861    *; #e #NNT4 elim (imply_to_and classic … NNT4);
862    cases e;
863    [ #tr' #r #STEPS #NOSTEP
864        @(ec_terminates s r ? (Eapp tr tr')) %
865        [ @s'
866        | @STEPS
867        ]
868    | #tr' #s'' #e' #STEPS *; #NOSTEP @False_rect_Type0
869        @NOSTEP //
870    | #msg #STEPS #NOSTEP
871        @(ec_wrong ? s s' tr) % //;
872    (* The following is stupidly complicated when most of the cases are impossible.
873       It ought to be simplified. *)
874    | #o #k #i #e' #STEPS #NOSTEP
875        cases e' in STEPS NOSTEP;
876        [ #tr' #r #STEPS #NOSTEP
877            @(ec_terminates s ???)
878           [ 3: @(annoying_corner_case_terminates … STEPS) ]
879        | #tr1 #s1 #e1 #STEPS *; #NOSTEP
880            @False_ind @NOSTEP //
881        | #msg #STEPS #NOSTEP
882            lapply (exec_step_interaction ge s');
883            cases (several_steps … STEPS EXEC); #_
884            whd in ⊢ (% → ?);
885            >(exec_inf_aux_unfold …)
886            cases (exec_step ge s');
887            [ #o1 #k1 #EXEC' #H whd in EXEC':(?%?) H;
888                cases (se_inv … EXEC'); *; #E1 #E2 #H2 destruct (E1 E2); normalize in H2;
889                cases (H i); #tr1 *; #s1 *; #K #E >K in H2;
890                >(exec_inf_aux_unfold …)
891                whd in ⊢ (?%? → ?); @is_final_elim [ #r ]
892                #F #S whd in S:(?%?); cases (se_inv … S);
893            | #x cases x; #tr' #s' whd in ⊢ (?%? → ?);
894                @is_final_elim' [ #r ] #F #S whd in S:(?%?);
895                cases (se_inv … S);
896            | #msg #S cases (se_inv … S);
897            ]
898        | #o1 #k1 #i1 #e1 #STEPS #NOSTEP
899            lapply (exec_step_interaction ge s');
900            cases (several_steps … STEPS EXEC); #_
901            whd in ⊢ (% → ?);
902            >(exec_inf_aux_unfold …)
903            cases (exec_step ge s');
904            [ #o1 #k1 #EXEC' #H whd in EXEC':(?%?) H;
905                cases (se_inv … EXEC'); *; #E1 #E2 #H2 destruct (E1 E2); normalize in H2;
906                cases (H i); #tr1 *; #s1 *; #K #E >K in H2;
907                >(exec_inf_aux_unfold …)
908                whd in ⊢ (?%? → ?); @is_final_elim [ #r ]
909                #F #S whd in S:(?%?); cases (se_inv … S);
910            | #x cases x; #tr' #s' whd in ⊢ (?%? → ?);
911                @is_final_elim' [ #r ] #F #S whd in S:(?%?);
912                cases (se_inv … S);
913            | #msg #S cases (se_inv … S);
914            ]
915        ]
916    ]
917]
918qed.   
919
920inductive execution_matches_behavior: s_execution → program_behavior → Prop ≝
921| emb_terminates: ∀s,e,tr,r.
922    execution_terminates tr s e r →
923    execution_matches_behavior e (Terminates tr r)
924| emb_diverges: ∀s,e,tr.
925    execution_diverges tr s e →
926    execution_matches_behavior e (Diverges tr)
927| emb_reacts: ∀s,e,tr.
928    execution_reacts tr s e →
929    execution_matches_behavior e (Reacts tr)
930| emb_wrong: ∀e,s,s',tr.
931    execution_goes_wrong tr s e s' →
932    execution_matches_behavior e (Goes_wrong tr)
933| emb_initially_wrong: ∀msg.
934    execution_matches_behavior (se_wrong msg) (Goes_wrong E0).
935
936lemma exec_state_terminates: ∀tr,tr',s,s',e,r.
937  execution_terminates tr s (se_step tr' s' e) r → s = s'.
938#tr #tr' #s #s' #e #r #H inversion H;
939[ #s1 #s2 #tr1 #tr2 #r' #e' #H' #E1 #E2 #E3 #E4 #_ destruct; @refl
940| #s1 #s2 #tr1 #tr2 #r' #e' #o #k #i #H' #E1 #E2 #E3 #E4 #_ destruct; @refl
941] qed.
942
943lemma exec_state_diverges: ∀tr,tr',s,s',e.
944  execution_diverges tr s (se_step tr' s' e) → s = s'.
945#tr #tr' #s #s' #e #H inversion H;
946#tr1 #s1 #s2 #e1 #e2 #H' #E1 #E2 #E3 #E4 #_ destruct; @refl qed.
947
948lemma exec_state_reacts: ∀tr,tr',s,s',e.
949  execution_reacts tr s (se_step tr' s' e) → s = s'.
950#tr #tr' #s #s' #e #H inversion H;
951#tr1 #s1 #e1 #H' #E1 #E2 #E3 #_ destruct; @refl qed.
952
953lemma exec_state_wrong: ∀tr,tr',s,s',s'',e.
954  execution_goes_wrong tr s (se_step tr' s' e) s'' → s = s'.
955#tr #tr' #s #s' #s'' #e #H inversion H;
956#tr1 #s1 #s2 #e1 #msg #H' #E1 #E2 #E3 #E4 #_ destruct; @refl qed.
957
958lemma behavior_of_execution: ∀s,e.
959  execution_characterisation s e →
960  ∃b:program_behavior. execution_matches_behavior e b.
961#s0 #e0 #exec
962cases exec;
963[ #s #r #e #tr #TERM
964    %{ (Terminates tr r)}
965    @(emb_terminates … TERM)
966| #s #e #tr #DIV
967    %{ (Diverges tr)}
968    @(emb_diverges … DIV)
969| #s #e #tr #REACTS
970    %{ (Reacts tr)}
971    @(emb_reacts … REACTS)
972| #e #s #s' #tr #WRONG
973    %{ (Goes_wrong tr)}
974    @(emb_wrong … WRONG)
975] qed.
976
977lemma initial_state_not_final: ∀ge,s.
978  initial_state ge s →
979  ¬ ∃r.final_state s r.
980#ge #s #H cases H;
981#b #f #ge #m #E1 #E2 #E3 #E4 % *; #r #H2
982inversion H2;
983#r' #E5 #E6 destruct (E5);
984qed.
985
986lemma initial_step: ∀ge,s,e.
987  exec_inf_aux ?? clight_exec ge (Value ??? 〈E0,s〉) = e →
988  ¬(∃r.final_state s r) →
989  ∃e'.e = e_step ??? E0 s e'.
990#ge #s #e >(exec_inf_aux_unfold …)
991whd in ⊢ (??%? → ?); @is_final_elim'
992[ #r #FINAL #EXEC #NOTFINAL
993    @False_ind @(absurd ?? NOTFINAL)
994    %{r} @FINAL
995| #F1 #EXEC #F2 whd in EXEC:(??%?); % [ 2: <EXEC @refl ]
996qed.
997
998theorem exec_inf_equivalence:
999  ∀classic:(∀P:Prop.P ∨ ¬P).
1000  ∀constructive_indefinite_description:(∀A:Type[0]. ∀P:A→Prop. (∃x. P x) → Sig A P).
1001  ∀p,e. single_exec_of (exec_inf ?? clight_fullexec p) e →
1002   ∃b.execution_matches_behavior e b ∧ exec_program p b.
1003#classic #constructive_indefinite_description #p #e
1004whd in ⊢ (?%? → ??(λ_.?(?%?)%));
1005lapply (make_initial_state_sound p)
1006lapply (the_initial_state p)
1007whd in ⊢ (? → ? → ?(match % with [_ ⇒ ? | _ ⇒ ?])? → ?);
1008cases (make_initial_state p)
1009[ #s #INITIAL' #INITIAL whd in INITIAL ⊢ (?%? → ?);
1010    >exec_inf_aux_unfold
1011    whd in ⊢ (?%? → ?);
1012    @is_final_elim'
1013    [ #r #F @False_ind
1014        @(absurd ?? (initial_state_not_final … INITIAL))
1015        %{r} @F
1016    | #NOTFINAL whd in ⊢ (?%? → ?); cases e;
1017        [ #tr #r #EXEC0 | #tr #s' #e0 #EXEC0 | #msg #EXEC0 | #o #k #i #e #EXEC0 ]
1018        cases (se_inv … EXEC0); *; #E1 #E2 <E1 <E2 #EXEC'
1019    lapply (behavior_of_execution ??
1020              (execution_characterisation_complete classic constructive_indefinite_description ? s ? EXEC'));
1021        *; #b #MATCHES %{b} % [ @MATCHES ]
1022        #ge #Ege
1023        inversion MATCHES;
1024        [ #s0 #e1 #tr1 #r #TERM #EXEC #BEHAVES <EXEC in TERM;
1025            #TERM
1026            lapply (exec_state_terminates … TERM); #E1
1027            >E1 in TERM; #TERM #_
1028            @(program_terminates (mk_transrel … step) ?? ge s)
1029            [ 2: @INITIAL
1030            | 3: <Ege @(terminates_sound … TERM EXEC')
1031            | skip
1032            | //;
1033            ]
1034        | #s0 #e #tr #DIVERGES #EXEC #E2 <EXEC in DIVERGES; #DIVERGES
1035            lapply (exec_state_diverges … DIVERGES);
1036            #E1 >E1 in DIVERGES; #DIVERGES #_
1037            inversion DIVERGES; #tr' #s1 #s2 #e1 #e2 #INITSTEPS #DIVERGING #E4 #E5 #E6
1038            <E4 in INITSTEPS ⊢ %; <E5 in E6 ⊢ %; #E6 #INITSTEPS
1039            cut (e0 = e1); [ destruct (E6) skip (MATCHES EXEC0 EXEC'); // ]
1040            #E7 <E7 in INITSTEPS; #INITSTEPS
1041            cases (several_steps … INITSTEPS EXEC'); #INITSTAR #EXECDIV #_
1042            @(program_diverges (mk_transrel … step) ?? ge s … INITIAL)
1043            [ 2: <Ege @INITSTAR
1044            | 3: <Ege @(silent_sound … DIVERGING EXECDIV)
1045            ]
1046        | #s0 #e #tr #REACTS #EXEC #E2 <EXEC in REACTS; #REACTS
1047            lapply (exec_state_reacts … REACTS);
1048            #E1 >E1 in REACTS; #REACTS #_
1049            inversion REACTS; #tr' #s' #e'' #REACTING #E4 #E5
1050            <E4 in REACTING ⊢ %; <E5 #REACTING #E6
1051            cut (e0 = e''); [ destruct (E6) skip (MATCHES EXEC0 EXEC'); // ]
1052            #E7 <E7 in REACTING; #REACTING #_
1053            @(program_reacts (mk_transrel … step) ?? ge s … INITIAL)
1054            <Ege @(reacts_sound … REACTING EXEC')
1055        | #e #s1 #s2 #tr #WRONG #EXEC #E2 <EXEC in WRONG; #WRONG
1056            lapply (exec_state_wrong … WRONG);
1057            #E1 >E1 in WRONG; #WRONG #_
1058            inversion WRONG; #tr' #s1' #s2' #e'' #msg #GOESWRONG #E4 #E5 #E6 #E7
1059            <E4 in GOESWRONG ⊢ %; <E5 <E7 #GOESWRONG
1060            cut (e0 = e''); [ destruct (E6) skip (INITIAL Ege MATCHES EXEC0 EXEC'); // ]
1061            #E8 <E8 in GOESWRONG; #GOESWRONG
1062            elim (wrong_sound … WRONG EXEC' NOTFINAL); *; #STAR #STOP #FINAL
1063            <Ege #_
1064            @(program_goes_wrong (mk_transrel … step) ?? ? s … INITIAL STAR STOP)
1065            #r % #F @(absurd ?? FINAL) %{r} @F
1066        | #msg #E destruct (E);
1067        ]
1068   ]
1069| #msg whd in ⊢ ((∀_.? → %) → ?);
1070    #NOINIT #_ #EXEC
1071    %{ (Goes_wrong E0)} %
1072    [ whd in EXEC:(?%?);
1073        cases e in EXEC;
1074        [ #tr #r #EXEC0 | #tr #s' #e0 #EXEC0 | #msg #EXEC0 | #o #k #i #e #EXEC0 ]
1075        cases (se_inv … EXEC0);
1076        @emb_initially_wrong
1077    | #ge #Ege
1078        @program_goes_initially_wrong
1079        #s % #INIT cases (NOINIT s INIT); #ge' #H @H
1080    ]
1081] qed.
1082
Note: See TracBrowser for help on using the repository browser.