source: C-semantics/CexecIOequiv.ma @ 398

Last change on this file since 398 was 398, checked in by campbell, 10 years ago

This time actually prove the result I intended.

File size: 12.4 KB
Line 
1include "CexecIO.ma".
2include "extralib.ma".
3
4(* A "single execution" - where all of the input values are made explicit. *)
5ncoinductive s_execution : Type ≝
6| se_stop : trace → int → mem → s_execution
7| se_step : trace → state → s_execution → s_execution
8| se_wrong : s_execution
9| se_interact : ∀o:io_out. (io_in o → execution) → io_in o → s_execution → s_execution.
10
11ncoinductive single_exec_of : execution → s_execution → Prop ≝
12| seo_stop : ∀tr,r,m. single_exec_of (e_stop tr r m) (se_stop tr r m)
13| seo_step : ∀tr,s,e,se.
14    single_exec_of e se →
15    single_exec_of (e_step tr s e) (se_step tr s se)
16| seo_wrong : single_exec_of e_wrong se_wrong
17| seo_interact : ∀o,k,i,se.
18    single_exec_of (k i) se →
19    single_exec_of (e_interact o k) (se_interact o k i se).
20
21(* starting after state s, zero or more steps of execution e reach state s'
22   after which comes e'. *)
23ninductive execution_isteps : trace → state → s_execution → state → s_execution → Prop ≝
24| isteps_none : ∀s,e. execution_isteps E0 s e s e
25| isteps_one : ∀e,e',tr,tr',s,s',s0.
26    execution_isteps tr' s e s' e' →
27    execution_isteps (tr⧺tr') s0 (se_step tr s e) s' e'
28| isteps_interact : ∀e,e',o,k,i,s,s',s0,tr,tr'.
29    execution_isteps tr' s e s' e' →
30    execution_isteps (tr⧺tr') s0 (se_interact o k i (se_step tr s e)) s' e'.
31
32nlemma isteps_trans: ∀tr1,tr2,s1,s2,s3,e1,e2,e3.
33  execution_isteps tr1 s1 e1 s2 e2 →
34  execution_isteps tr2 s2 e2 s3 e3 →
35  execution_isteps (tr1⧺tr2) s1 e1 s3 e3.
36#tr1 tr2 s1 s2 s3 e1 e2 e3 H1; nelim H1;
37##[ #s e; //;
38##| #e e' tr tr' s1' s2' s3' H1 H2 H3;
39    nrewrite > (Eapp_assoc …);
40    napply isteps_one;
41    napply H2; napply H3;
42##| #e e' o k i s1' s2' s3' tr tr' H1 H2 H3;
43    nrewrite > (Eapp_assoc …);
44    napply isteps_interact;
45    /2/
46##] nqed.
47
48nlemma exec_e_step: ∀ge,x,tr,s,e.
49  exec_inf_aux ge x = e_step tr s e →
50  exec_inf_aux ge (exec_step ge s) = e.
51#ge x tr s e;
52nrewrite > (exec_inf_aux_unfold …); ncases x;
53##[ #o k EXEC; nwhd in EXEC:(??%?); ndestruct
54##| #y; ncases y; #tr' s'; nwhd in ⊢ (??%? → ?);
55    ncases (is_final_state s'); #FINAL EXEC; nwhd in EXEC:(??%?); ndestruct;
56    napply refl;
57##| #EXEC; nwhd in EXEC:(??%?); ndestruct
58##] nqed.
59
60nlemma exec_e_step_inv: ∀ge,x,tr,s,e.
61  exec_inf_aux ge x = e_step tr s e →
62  x = Value ??? 〈tr,s〉.
63#ge x tr s e;
64nrewrite > (exec_inf_aux_unfold …); ncases x;
65##[ #o k EXEC; nwhd in EXEC:(??%?); ndestruct
66##| #y; ncases y; #tr' s'; nwhd in ⊢ (??%? → ?);
67    ncases (is_final_state s'); #FINAL EXEC; nwhd in EXEC:(??%?); ndestruct;
68    napply refl;
69##| #EXEC; nwhd in EXEC:(??%?); ndestruct
70##] nqed.
71
72nlemma exec_e_step_inv2: ∀ge,x,tr,s,e.
73  exec_inf_aux ge x = e_step tr s e →
74  ¬∃r.final_state s r.
75#ge x tr s e;
76nrewrite > (exec_inf_aux_unfold …); ncases x;
77##[ #o k EXEC; nwhd in EXEC:(??%?); ndestruct
78##| #y; ncases y; #tr' s'; nwhd in ⊢ (??%? → ?);
79    ncases (is_final_state s'); #FINAL EXEC; nwhd in EXEC:(??%?); ndestruct;
80    napply FINAL;
81##| #EXEC; nwhd in EXEC:(??%?); ndestruct
82##] nqed.
83
84ndefinition exec_from : genv → state → s_execution → Prop ≝
85λge,s,se. single_exec_of (exec_inf_aux ge (exec_step ge s)) se.
86
87nlemma exec_from_step : ∀ge,s,tr,s',e.
88exec_from ge s (se_step tr s' e) →
89exec_step ge s = Value ??? 〈tr,s'〉 ∧ exec_from ge s' e.
90#ge s0 tr0 s0' e0 H; ninversion H;
91##[ #tr r m E1 E2; ndestruct
92##| #tr s e se H1 H2 E; ndestruct (E);
93    nrewrite > (exec_e_step_inv … H2);
94    nrewrite < (exec_e_step … H2) in H1; #H1; @; //
95##| #_; #E; ndestruct
96##| #o k i se H1 H2 E; ndestruct
97##] nqed.
98
99nlemma exec_from_interact : ∀ge,s,o,k,i,tr,s',e.
100exec_from ge s (se_interact o k i (se_step tr s' e)) →
101step ge s tr s' ∧
102(*exec_step ge s = Value ??? 〈tr,s'〉 ∧*) exec_from ge s' e.
103#ge s0 o0 k0 i0 tr0 s0' e0 H; ninversion H;
104##[ #tr r m E1 E2; ndestruct
105##| #tr s e se H1 H2 E; ndestruct (E)
106##| #_; #E; ndestruct
107##| #o k i se H1 H2 E; ndestruct (E);
108    nlapply (exec_step_sound ge s0);
109    ncases (exec_step ge s0) in H2 ⊢ %;
110    ##[ #o' k'; nrewrite > (exec_inf_aux_unfold …);
111        #E'; nwhd in E':(??%?); ndestruct (E');
112        #STEP;
113        ninversion H1;
114        ##[ #tr r m E1 E2; ndestruct
115        ##| #tr' s' e' se' H2 H3 E2; ndestruct (E2);
116            nrewrite < (exec_e_step … H3) in H2; #H2; @; //;
117            nlapply (STEP i);
118            nrewrite > (exec_e_step_inv … H3);
119            #S; napply S;
120        ##| #_; #E; ndestruct
121        ##| #o k i se H1 H2 E; ndestruct
122        ##]
123    ##| #x; ncases x; #tr' s'; nrewrite > (exec_inf_aux_unfold …);
124        nwhd in ⊢ (??%? → ?); ncases (is_final_state s');
125        #F E; nwhd in E:(??%?); ndestruct
126    ##| nrewrite > (exec_inf_aux_unfold …);
127        #E'; nwhd in E':(??%?); ndestruct (E');
128    ##]
129##] nqed.
130
131nlemma exec_from_interact_stop : ∀ge,s,o,k,i,tr,r,m.
132exec_from ge s (se_interact o k i (se_stop tr r m)) →
133step ge s tr (Returnstate (Vint r) Kstop m).
134#ge s0 o0 k0 i0 tr0 s0' e0 H; ninversion H;
135##[ #tr r m E1 E2; ndestruct
136##| #tr s e se H1 H2 E; ndestruct (E)
137##| #_; #E; ndestruct
138##| #o k i se H1 H2 E; ndestruct (E);
139    nlapply (exec_step_sound ge s0);
140    nrewrite > (exec_inf_aux_unfold …) in H2;
141    ncases (exec_step ge s0);
142    ##[ #o' k';
143        #E'; nwhd in E':(??%?); ndestruct (E');
144        #STEP;
145        ninversion H1;
146        ##[ #tr r m E1 E2; nlapply (STEP i); ndestruct;
147            nrewrite > (exec_inf_aux_unfold …) in E1;
148            ncases (k' i);
149            ##[ #o2 k2 E; nwhd in E:(??%?); ndestruct (E)
150            ##| #x; ncases x; #tr2 s2; nwhd in ⊢ (??%? → ?);
151                ncases (is_final_state s2);
152                ##[ #F; ncases F; #r' FINAL E; nwhd in E:(??%?);
153                    ndestruct (E);
154                    ninversion FINAL;
155                    #r'' m'' E1 E2; ndestruct (E1 E2); //;
156                ##| #NF E; nwhd in E:(??%?); ndestruct (E)
157                ##]
158            ##| #E; nwhd in E:(??%?); ndestruct (E)
159            ##]
160       ##| #tr s e e' H EXEC E; ndestruct (E)
161       ##| #EXEC E; ndestruct (E)
162       ##| #o2 k2 i2 e2 H EXEC E; ndestruct (E)
163       ##]
164   ##| #x; ncases x; #tr s; nwhd in ⊢ (??%? → ?);
165       ncases (is_final_state s); #F E; nwhd in E:(??%?); ndestruct (E)
166   ##| #E; nwhd in E:(??%?); ndestruct (E)
167   ##]
168##] nqed.
169
170(* NB: the E0 in the execs are irrelevant. *)
171nlemma several_steps: ∀ge,tr,e,e',s,s'.
172  execution_isteps tr s e s' e' →
173  exec_from ge s e →
174  star (mk_transrel … step) ge s tr s' ∧
175  exec_from ge s' e'.
176#ge tr0 e0 e0' s0 s0' H;
177nelim H;
178##[ #s e EXEC; @; //;
179##| #e1 e2 tr1 tr2 s1 s2 s3 STEPS IH EXEC;
180    nelim (exec_from_step … EXEC); #EXEC3 EXEC1;
181    nelim (IH EXEC1);
182    #STAR12 EXEC2; @; //;
183    nlapply (exec_step_sound ge s3);
184    nrewrite > EXEC3; #STEP3;
185    napply (star_step (mk_transrel ?? step) … STEP3 STAR12);
186    napply refl
187##| #e1 e2 o k i s1 s2 s3 tr1 tr2 STEPS IH EXEC;
188    nelim (exec_from_interact … EXEC);
189    #STEP3 EXEC1;
190    nelim (IH EXEC1); #STAR EXEC2;
191    @;
192    ##[ napply (star_step (mk_transrel ?? step) … STEP3 STAR);
193        napply refl
194    ##| //
195    ##]
196##] nqed.
197
198ninductive execution_terminates : trace → state → s_execution → int → mem → Prop ≝
199| terminates : ∀s,s',tr,tr',r,e,m.
200    execution_isteps tr s e s' (se_stop tr' r m) →
201    execution_terminates (tr⧺tr') s (se_step E0 s e) r m
202(* We should only be able to get to here if main is an external function, which is silly. *)
203| annoying_corner_case_terminates: ∀s,s',tr,tr',r,e,m,o,k,i.
204    execution_isteps tr s e s' (se_interact o k i (se_stop tr' r m)) →
205    execution_terminates (tr⧺tr') s (se_step E0 s e) r m.
206
207ncoinductive execution_diverging : s_execution → Prop ≝
208| diverging_step : ∀s,e. execution_diverging e → execution_diverging (se_step E0 s e).
209
210(* Makes a finite number of interactions (including cost labels) before diverging. *)
211ninductive execution_diverges : trace → state → s_execution → Prop ≝
212| diverges_diverging: ∀tr,s,s',e,e'.
213    execution_isteps tr s e s' e' →
214    execution_diverging e' →
215    execution_diverges tr s (se_step E0 s e).
216
217(* NB: "reacting" includes hitting a cost label. *)
218ncoinductive execution_reacting : traceinf → state → s_execution → Prop ≝
219| reacting: ∀tr,tr',s,s',e,e'.
220    execution_reacting tr' s' e' →
221    execution_isteps tr s e s' e' →
222    tr ≠ E0 →
223    execution_reacting (tr⧻tr') s e.
224
225ninductive execution_reacts : traceinf → state → s_execution → Prop ≝
226| reacts: ∀tr,s,e.
227    execution_reacting tr s e →
228    execution_reacts tr s (se_step E0 s e).
229
230ninductive execution_goes_wrong: trace → state → s_execution → state → Prop ≝
231| go_wrong: ∀tr,s,s',e.
232    execution_isteps tr s e s' se_wrong →
233    execution_goes_wrong tr s (se_step E0 s e) s'.
234
235nlet corec silent_sound ge s e
236  (H0:execution_diverging e)
237  (EXEC:exec_from ge s e)
238  : forever_silent (mk_transrel ?? step) … ge s ≝ ?.
239ncut (∃s2.∃e2.And (And (execution_diverging e2) (step ge s E0 s2)) (exec_from ge s2 e2));
240##[ ncases H0 in EXEC ⊢ %; #s1 e1 H1 EXEC;
241    nelim (exec_from_step … EXEC);
242    #EXEC0 EXEC1;
243    @ s1; @ e1; @; //; @; //;
244    nlapply (exec_step_sound ge s); nrewrite > EXEC0; nwhd in ⊢ (% → ?); //;
245##| *; #s2; *; #e2; *; *; #H2 STEP2 EXEC2;
246    napply (forever_silent_intro (mk_transrel ?? step) … ge s s2 ? (silent_sound ge s2 e2 ??));
247    //;
248##] nqed.
249
250nlemma final_step: ∀ge,tr,r,m,s.
251  exec_from ge s (se_stop tr r m) →
252  step ge s tr (Returnstate (Vint r) Kstop m).
253#ge tr r m s EXEC;
254nwhd in EXEC;
255ninversion EXEC;
256##[ #tr' r' m' EXEC' E; ndestruct (E);
257    nlapply (exec_step_sound ge s);
258    nrewrite > (exec_inf_aux_unfold …) in EXEC';
259    ncases (exec_step ge s);
260    ##[ #o k EXEC'; nwhd in EXEC':(??%?); ndestruct (EXEC');
261    ##| #x; ncases x; #tr'' s'; nwhd in ⊢ (??%? → ?);
262        ncases (is_final_state s'); #F; ##[ ##1: ncases F; #r'' FINAL; ##]
263        #EXEC'; nwhd in EXEC':(??%?); ndestruct (EXEC');
264    ##| #EXEC'; nwhd in EXEC':(??%?); ndestruct (EXEC');
265    ##]
266    ninversion FINAL; #r''' m' E1 E2 H; ndestruct (E1 E2);
267    napply H;
268##| #tr' s' e' se' H EXEC' E; ndestruct
269##| #EXEC' E; ndestruct
270##| #o k i e H EXEC E; ndestruct
271##] nqed.
272
273
274nlemma e_stop_inv: ∀ge,x,tr,r,m.
275  exec_inf_aux ge x = e_stop tr r m →
276  x = Value ??? 〈tr,Returnstate (Vint r) Kstop m〉.
277#ge x tr r m;
278nrewrite > (exec_inf_aux_unfold …); ncases x;
279##[ #o k EXEC; nwhd in EXEC:(??%?); ndestruct;
280##| #z; ncases z; #tr' s'; nwhd in ⊢ (??%? → ?); ncases (is_final_state s');
281  ##[ #F; ncases F; #r' FINAL; ncases FINAL; #r'' m' EXEC; nwhd in EXEC:(??%?);
282      ndestruct (EXEC); napply refl;
283  ##| #F EXEC; nwhd in EXEC:(??%?); ndestruct (EXEC);
284  ##]
285##| #EXEC; nwhd in EXEC:(??%?); ndestruct (EXEC);
286##] nqed.
287
288nlemma terminates_sound: ∀ge,tr,s,r,m,e.
289  execution_terminates tr s (se_step E0 s e) r m →
290  exec_from ge s e →
291  star (mk_transrel … step) ge s tr (Returnstate (Vint r) Kstop m).
292#ge tr0 s0 r m e0 H; ninversion H;
293##[ #s s' tr tr' r e m ESTEPS E1 E2 E3 E4 E5 EXEC;
294    ndestruct (E1 E2 E3 E4 E5);
295    ncases (several_steps … ESTEPS EXEC); #STARs' EXECs';
296    napply (star_right … STARs');
297    ##[ ##2: napply (final_step ge tr' r m s' … EXECs');
298    ##| ##skip
299    ##| napply refl
300    ##]
301##| #s s' tr tr' r e m o k i ESTEPS E1 E2 E3 E4 E5 EXEC;
302    ndestruct;
303    ncases (several_steps … ESTEPS EXEC); #STARs' EXECs';
304    napply (star_right … STARs');
305    ##[ napply tr'
306    ##| napply (exec_from_interact_stop … EXECs');
307    ##| napply refl
308    ##]
309##] nqed.
310
311nlet corec reacts_sound ge tr s e
312  (REACTS:execution_reacting tr s e)
313  (EXEC:exec_from ge s e) :
314  forever_reactive (mk_transrel … step) ge s tr ≝ ?.
315ncut (∃s'.∃e'.∃tr'.∃tr''.(And (And (And (execution_reacting tr'' s' e') (execution_isteps tr' s e s' e')) (tr' ≠ E0)) (tr = tr'⧻tr'')));
316##[ ninversion REACTS;
317    #tr0 tr' s0 s' e0 e' EREACTS ESTEPS REACTED E1 E2 E3; ndestruct (E2 E3);
318    @ s'; @ e'; @ tr0; @ tr'; @; ##[ @; ##[ @; //; ##| napply REACTED ##] ##| napply refl ##]
319##| *; #s'; *; #e'; *; #tr'; *; #tr'';
320    *; *; *; #REACTS' ESTEPS REACTED APPTR;
321(*    nrewrite > APPTR;*)
322    napply (match sym_eq ??? APPTR return λx.λ_.forever_reactive (mk_transrel genv state step) ge s x with [ refl ⇒ ? ]);
323    @;
324    ncases (several_steps … ESTEPS EXEC); #STEPS EXEC';
325    ##[ ##2: napply STEPS;
326    ##| ##skip
327    ##| napply REACTED
328    ##| napply reacts_sound;
329      ##[ ##2: napply REACTS';
330      ##| ##skip
331      ##| napply EXEC'
332      ##]
333    ##]
334nqed.
Note: See TracBrowser for help on using the repository browser.