source: src/Clight/CexecEquiv.ma @ 1344

Last change on this file since 1344 was 1344, checked in by sacerdot, 8 years ago

Ported to new destruct.

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