1 | (* *********************************************************************) |
---|
2 | (* *) |
---|
3 | (* The Compcert verified compiler *) |
---|
4 | (* *) |
---|
5 | (* Xavier Leroy, INRIA Paris-Rocquencourt *) |
---|
6 | (* *) |
---|
7 | (* Copyright Institut National de Recherche en Informatique et en *) |
---|
8 | (* Automatique. All rights reserved. This file is distributed *) |
---|
9 | (* under the terms of the GNU General Public License as published by *) |
---|
10 | (* the Free Software Foundation, either version 2 of the License, or *) |
---|
11 | (* (at your option) any later version. This file is also distributed *) |
---|
12 | (* under the terms of the INRIA Non-Commercial License Agreement. *) |
---|
13 | (* *) |
---|
14 | (* *********************************************************************) |
---|
15 | |
---|
16 | (* * Tools for small-step operational semantics *) |
---|
17 | |
---|
18 | (* * This module defines generic operations and theorems over |
---|
19 | the one-step transition relations that are used to specify |
---|
20 | operational semantics in small-step style. *) |
---|
21 | |
---|
22 | (* |
---|
23 | Require Import Wf. |
---|
24 | Require Import Wf_nat. |
---|
25 | Require Import Classical. |
---|
26 | Require Import Coqlib. |
---|
27 | Require Import AST. |
---|
28 | *) |
---|
29 | include "Events.ma". |
---|
30 | (* |
---|
31 | Require Import Globalenvs. |
---|
32 | Require Import Integers. |
---|
33 | |
---|
34 | Set Implicit Arguments. |
---|
35 | *) |
---|
36 | (* * * Closures of transitions relations *) |
---|
37 | |
---|
38 | record transrel : Type[1] ≝ { |
---|
39 | genv : Type[0]; |
---|
40 | state: Type[0]; |
---|
41 | step : genv → state → trace → state → Prop |
---|
42 | }. |
---|
43 | |
---|
44 | (*Section CLOSURES. |
---|
45 | |
---|
46 | Variable genv: Type. |
---|
47 | Variable state: Type. |
---|
48 | |
---|
49 | (* * A one-step transition relation has the following signature. |
---|
50 | It is parameterized by a global environment, which does not |
---|
51 | change during the transition. It relates the initial state |
---|
52 | of the transition with its final state. The [trace] parameter |
---|
53 | captures the observable events possibly generated during the |
---|
54 | transition. *) |
---|
55 | |
---|
56 | Variable step: genv -> state -> trace -> state -> Prop. |
---|
57 | *) |
---|
58 | (* * No transitions: stuck state *) |
---|
59 | |
---|
60 | definition nostep ≝ λtr:transrel. λge: genv tr. λs: state tr. |
---|
61 | ∀t,s'. ¬((step tr) ge s t s'). |
---|
62 | |
---|
63 | (* * Zero, one or several transitions. Also known as Kleene closure, |
---|
64 | or reflexive transitive closure. *) |
---|
65 | |
---|
66 | inductive star (tr:transrel) (ge: genv tr): state tr -> trace -> state tr -> Prop := |
---|
67 | | star_refl: ∀s. |
---|
68 | star tr ge s E0 s |
---|
69 | | star_step: ∀s1,t1,s2,t2,s3,t. |
---|
70 | (step tr) ge s1 t1 s2 -> star tr ge s2 t2 s3 -> t = t1 ⧺ t2 -> |
---|
71 | star tr ge s1 t s3. |
---|
72 | |
---|
73 | lemma star_one: |
---|
74 | ∀tr,ge,s1,t,s2. (step tr) ge s1 t s2 -> star tr ge s1 t s2. |
---|
75 | #tr #ge #s1 #t #s2 #H @(star_step … H (star_refl …)) |
---|
76 | >(E0_right …) //; |
---|
77 | qed. |
---|
78 | |
---|
79 | lemma star_trans: |
---|
80 | ∀tr,ge,s1,t1,s2. star tr ge s1 t1 s2 -> |
---|
81 | ∀t2,s3,t. star tr ge s2 t2 s3 -> t = t1 ⧺ t2 -> star tr ge s1 t s3. |
---|
82 | #tr #ge #s1 #t1 #s2 #H elim H; |
---|
83 | [ #s #t2 #s3 #t #H0 #H1 >H1 normalize; //; |
---|
84 | | #s #t #s' #t' #s'' #t'' #H0 #H1 #H2 #H3 |
---|
85 | #t2 #s3 #t3 #H4 #H5 |
---|
86 | @(star_step … H0 (H3 … H4 …) ?) |
---|
87 | [ @(t'⧺t2) |
---|
88 | | // |
---|
89 | | <(Eapp_assoc …) <H2 @H5 |
---|
90 | ] |
---|
91 | ] |
---|
92 | qed. |
---|
93 | |
---|
94 | lemma star_left: |
---|
95 | ∀tr,ge,s1,t1,s2,t2,s3,t. |
---|
96 | (step tr) ge s1 t1 s2 -> star tr ge s2 t2 s3 -> t = t1 ⧺ t2 -> |
---|
97 | star tr ge s1 t s3. |
---|
98 | @star_step |
---|
99 | qed. |
---|
100 | |
---|
101 | lemma star_right: |
---|
102 | ∀tr,ge,s1,t1,s2,t2,s3,t. |
---|
103 | star tr ge s1 t1 s2 -> (step tr) ge s2 t2 s3 -> t = t1 ⧺ t2 -> |
---|
104 | star tr ge s1 t s3. |
---|
105 | #tr #ge #s1 #t1 #s2 #t2 #s3 #t #H1 #H2 #H3 |
---|
106 | @(star_trans … H1 … (star_one … H2)) @H3 |
---|
107 | qed. |
---|
108 | |
---|
109 | (* * One or several transitions. Also known as the transitive closure. *) |
---|
110 | |
---|
111 | inductive plus (tr:transrel) (ge: genv tr): state tr → trace → state tr → Prop ≝ |
---|
112 | | plus_left: ∀s1,t1,s2,t2,s3,t. |
---|
113 | step tr ge s1 t1 s2 -> star tr ge s2 t2 s3 -> t = t1 ⧺ t2 -> |
---|
114 | plus tr ge s1 t s3. |
---|
115 | |
---|
116 | lemma plus_one: |
---|
117 | ∀tr,ge,s1,t,s2. |
---|
118 | step tr ge s1 t s2 -> plus tr ge s1 t s2. |
---|
119 | #tr #ge #s1 #t #s2 #H @(plus_left … H (star_refl …)) |
---|
120 | >(E0_right …) //; |
---|
121 | qed. |
---|
122 | |
---|
123 | lemma plus_star: |
---|
124 | ∀tr,ge,s1,t,s2. plus tr ge s1 t s2 -> star tr ge s1 t s2. |
---|
125 | #tr #ge #s1 #t #s2 #H elim H; #s1' #t1' #s2' #t2' #s3' #t3' #H1 #H2 #e1 |
---|
126 | @(star_step … H1 H2 …) @e1; |
---|
127 | qed. |
---|
128 | |
---|
129 | lemma plus_right: |
---|
130 | ∀tr,ge,s1,t1,s2,t2,s3,t. |
---|
131 | star tr ge s1 t1 s2 -> step tr ge s2 t2 s3 -> t = t1 ⧺ t2 -> |
---|
132 | plus tr ge s1 t s3. |
---|
133 | #tr #ge #s1 #t1 #s2 #t2 #s3 #t3 #Hstar #Hstep #e1 inversion Hstar; |
---|
134 | [ #s2' #e2 #e3 #e4 destruct; @plus_one //; |
---|
135 | | #s1' #t1' #s1'' #t1'' #s2' #t2' #H1 #H2 #e2 #foo #e3 #e4 #e5 destruct; |
---|
136 | >(Eapp_assoc …) @(plus_left … H1) |
---|
137 | [ 2: @(star_right … H2 Hstep) //; |
---|
138 | | skip; |
---|
139 | | // |
---|
140 | ] |
---|
141 | ] |
---|
142 | qed. |
---|
143 | (* |
---|
144 | Lemma plus_left': |
---|
145 | forall ge s1 t1 s2 t2 s3 t, |
---|
146 | step ge s1 t1 s2 -> plus ge s2 t2 s3 -> t = t1 ** t2 -> |
---|
147 | plus ge s1 t s3. |
---|
148 | Proof. |
---|
149 | intros. eapply plus_left; eauto. apply plus_star; auto. |
---|
150 | Qed. |
---|
151 | |
---|
152 | Lemma plus_right': |
---|
153 | forall ge s1 t1 s2 t2 s3 t, |
---|
154 | plus ge s1 t1 s2 -> step ge s2 t2 s3 -> t = t1 ** t2 -> |
---|
155 | plus ge s1 t s3. |
---|
156 | Proof. |
---|
157 | intros. eapply plus_right; eauto. apply plus_star; auto. |
---|
158 | Qed. |
---|
159 | |
---|
160 | Lemma plus_star_trans: |
---|
161 | forall ge s1 t1 s2 t2 s3 t, |
---|
162 | plus ge s1 t1 s2 -> star ge s2 t2 s3 -> t = t1 ** t2 -> plus ge s1 t s3. |
---|
163 | Proof. |
---|
164 | intros. inversion H; subst. |
---|
165 | econstructor; eauto. eapply star_trans; eauto. |
---|
166 | traceEq. |
---|
167 | Qed. |
---|
168 | |
---|
169 | Lemma star_plus_trans: |
---|
170 | forall ge s1 t1 s2 t2 s3 t, |
---|
171 | star ge s1 t1 s2 -> plus ge s2 t2 s3 -> t = t1 ** t2 -> plus ge s1 t s3. |
---|
172 | Proof. |
---|
173 | intros. inversion H; subst. |
---|
174 | simpl; auto. |
---|
175 | rewrite Eapp_assoc. |
---|
176 | econstructor. eauto. eapply star_trans. eauto. |
---|
177 | apply plus_star. eauto. eauto. auto. |
---|
178 | Qed. |
---|
179 | |
---|
180 | Lemma plus_trans: |
---|
181 | forall ge s1 t1 s2 t2 s3 t, |
---|
182 | plus ge s1 t1 s2 -> plus ge s2 t2 s3 -> t = t1 ** t2 -> plus ge s1 t s3. |
---|
183 | Proof. |
---|
184 | intros. eapply plus_star_trans. eauto. apply plus_star. eauto. auto. |
---|
185 | Qed. |
---|
186 | |
---|
187 | Lemma plus_inv: |
---|
188 | forall ge s1 t s2, |
---|
189 | plus ge s1 t s2 -> |
---|
190 | step ge s1 t s2 \/ exists s', exists t1, exists t2, step ge s1 t1 s' /\ plus ge s' t2 s2 /\ t = t1 ** t2. |
---|
191 | Proof. |
---|
192 | intros. inversion H; subst. inversion H1; subst. |
---|
193 | left. rewrite E0_right. auto. |
---|
194 | right. exists s3; exists t1; exists (t0 ** t3); split. auto. |
---|
195 | split. econstructor; eauto. auto. |
---|
196 | Qed. |
---|
197 | |
---|
198 | Lemma star_inv: |
---|
199 | forall ge s1 t s2, |
---|
200 | star ge s1 t s2 -> |
---|
201 | (s2 = s1 /\ t = E0) \/ plus ge s1 t s2. |
---|
202 | Proof. |
---|
203 | intros. inv H. left; auto. right; econstructor; eauto. |
---|
204 | Qed. |
---|
205 | *) |
---|
206 | (* * Infinitely many transitions *) |
---|
207 | |
---|
208 | coinductive forever (tr:transrel) (ge: genv tr): state tr -> traceinf -> Prop := |
---|
209 | | forever_intro: ∀s1,t,s2,T. |
---|
210 | step tr ge s1 t s2 -> forever tr ge s2 T -> |
---|
211 | forever tr ge s1 (t ⧻ T). |
---|
212 | |
---|
213 | lemma star_forever: |
---|
214 | ∀tr,ge,s1,t,s2. star tr ge s1 t s2 -> |
---|
215 | ∀T. forever tr ge s2 T -> |
---|
216 | forever tr ge s1 (t ⧻ T). |
---|
217 | #tr #ge #s1 #t1 #s2 #H elim H; |
---|
218 | [ #s' #T #H2 @H2 |
---|
219 | | #s1' #t1 #s0 #t0 #s2' #t2' #H1 #H2 #e1 #IH #T #H3 |
---|
220 | >e1 >(Eappinf_assoc …) |
---|
221 | % /2/; |
---|
222 | ] qed. |
---|
223 | (* |
---|
224 | (** An alternate, equivalent definition of [forever] that is useful |
---|
225 | for coinductive reasoning. *) |
---|
226 | |
---|
227 | Variable A: Type. |
---|
228 | Variable order: A -> A -> Prop. |
---|
229 | |
---|
230 | CoInductive forever_N (ge: genv) : A -> state -> traceinf -> Prop := |
---|
231 | | forever_N_star: forall s1 t s2 a1 a2 T1 T2, |
---|
232 | star ge s1 t s2 -> |
---|
233 | order a2 a1 -> |
---|
234 | forever_N ge a2 s2 T2 -> |
---|
235 | T1 = t *** T2 -> |
---|
236 | forever_N ge a1 s1 T1 |
---|
237 | | forever_N_plus: forall s1 t s2 a1 a2 T1 T2, |
---|
238 | plus ge s1 t s2 -> |
---|
239 | forever_N ge a2 s2 T2 -> |
---|
240 | T1 = t *** T2 -> |
---|
241 | forever_N ge a1 s1 T1. |
---|
242 | |
---|
243 | Hypothesis order_wf: well_founded order. |
---|
244 | |
---|
245 | Lemma forever_N_inv: |
---|
246 | forall ge a s T, |
---|
247 | forever_N ge a s T -> |
---|
248 | exists t, exists s', exists a', exists T', |
---|
249 | step ge s t s' /\ forever_N ge a' s' T' /\ T = t *** T'. |
---|
250 | Proof. |
---|
251 | intros ge a0. pattern a0. apply (well_founded_ind order_wf). |
---|
252 | intros. inv H0. |
---|
253 | (* star case *) |
---|
254 | inv H1. |
---|
255 | (* no transition *) |
---|
256 | change (E0 *** T2) with T2. apply H with a2. auto. auto. |
---|
257 | (* at least one transition *) |
---|
258 | exists t1; exists s0; exists x; exists (t2 *** T2). |
---|
259 | split. auto. split. eapply forever_N_star; eauto. |
---|
260 | apply Eappinf_assoc. |
---|
261 | (* plus case *) |
---|
262 | inv H1. |
---|
263 | exists t1; exists s0; exists a2; exists (t2 *** T2). |
---|
264 | split. auto. |
---|
265 | split. inv H3. auto. |
---|
266 | eapply forever_N_plus. econstructor; eauto. eauto. auto. |
---|
267 | apply Eappinf_assoc. |
---|
268 | Qed. |
---|
269 | |
---|
270 | Lemma forever_N_forever: |
---|
271 | forall ge a s T, forever_N ge a s T -> forever ge s T. |
---|
272 | Proof. |
---|
273 | cofix COINDHYP; intros. |
---|
274 | destruct (forever_N_inv H) as [t [s' [a' [T' [P [Q R]]]]]]. |
---|
275 | rewrite R. apply forever_intro with s'. auto. |
---|
276 | apply COINDHYP with a'; auto. |
---|
277 | Qed. |
---|
278 | |
---|
279 | (** Yet another alternative definition of [forever]. *) |
---|
280 | |
---|
281 | CoInductive forever_plus (ge: genv) : state -> traceinf -> Prop := |
---|
282 | | forever_plus_intro: forall s1 t s2 T1 T2, |
---|
283 | plus ge s1 t s2 -> |
---|
284 | forever_plus ge s2 T2 -> |
---|
285 | T1 = t *** T2 -> |
---|
286 | forever_plus ge s1 T1. |
---|
287 | |
---|
288 | Lemma forever_plus_inv: |
---|
289 | forall ge s T, |
---|
290 | forever_plus ge s T -> |
---|
291 | exists s', exists t, exists T', |
---|
292 | step ge s t s' /\ forever_plus ge s' T' /\ T = t *** T'. |
---|
293 | Proof. |
---|
294 | intros. inv H. inv H0. exists s0; exists t1; exists (t2 *** T2). |
---|
295 | split. auto. |
---|
296 | split. exploit star_inv; eauto. intros [[P Q] | R]. |
---|
297 | subst. simpl. auto. econstructor; eauto. |
---|
298 | traceEq. |
---|
299 | Qed. |
---|
300 | |
---|
301 | Lemma forever_plus_forever: |
---|
302 | forall ge s T, forever_plus ge s T -> forever ge s T. |
---|
303 | Proof. |
---|
304 | cofix COINDHYP; intros. |
---|
305 | destruct (forever_plus_inv H) as [s' [t [T' [P [Q R]]]]]. |
---|
306 | subst. econstructor; eauto. |
---|
307 | Qed. |
---|
308 | *) |
---|
309 | (* * Infinitely many silent transitions *) |
---|
310 | |
---|
311 | coinductive forever_silent (tr:transrel) (ge: genv tr): state tr → Prop ≝ |
---|
312 | | forever_silent_intro: ∀s1,s2. |
---|
313 | step tr ge s1 E0 s2 → forever_silent tr ge s2 → |
---|
314 | forever_silent tr ge s1. |
---|
315 | (* |
---|
316 | (** An alternate definition. *) |
---|
317 | |
---|
318 | CoInductive forever_silent_N (ge: genv) : A -> state -> Prop := |
---|
319 | | forever_silent_N_star: forall s1 s2 a1 a2, |
---|
320 | star ge s1 E0 s2 -> |
---|
321 | order a2 a1 -> |
---|
322 | forever_silent_N ge a2 s2 -> |
---|
323 | forever_silent_N ge a1 s1 |
---|
324 | | forever_silent_N_plus: forall s1 s2 a1 a2, |
---|
325 | plus ge s1 E0 s2 -> |
---|
326 | forever_silent_N ge a2 s2 -> |
---|
327 | forever_silent_N ge a1 s1. |
---|
328 | |
---|
329 | Lemma forever_silent_N_inv: |
---|
330 | forall ge a s, |
---|
331 | forever_silent_N ge a s -> |
---|
332 | exists s', exists a', |
---|
333 | step ge s E0 s' /\ forever_silent_N ge a' s'. |
---|
334 | Proof. |
---|
335 | intros ge a0. pattern a0. apply (well_founded_ind order_wf). |
---|
336 | intros. inv H0. |
---|
337 | (* star case *) |
---|
338 | inv H1. |
---|
339 | (* no transition *) |
---|
340 | apply H with a2. auto. auto. |
---|
341 | (* at least one transition *) |
---|
342 | exploit Eapp_E0_inv; eauto. intros [P Q]. subst. |
---|
343 | exists s0; exists x. |
---|
344 | split. auto. eapply forever_silent_N_star; eauto. |
---|
345 | (* plus case *) |
---|
346 | inv H1. exploit Eapp_E0_inv; eauto. intros [P Q]. subst. |
---|
347 | exists s0; exists a2. |
---|
348 | split. auto. inv H3. auto. |
---|
349 | eapply forever_silent_N_plus. econstructor; eauto. eauto. |
---|
350 | Qed. |
---|
351 | |
---|
352 | Lemma forever_silent_N_forever: |
---|
353 | forall ge a s, forever_silent_N ge a s -> forever_silent ge s. |
---|
354 | Proof. |
---|
355 | cofix COINDHYP; intros. |
---|
356 | destruct (forever_silent_N_inv H) as [s' [a' [P Q]]]. |
---|
357 | apply forever_silent_intro with s'. auto. |
---|
358 | apply COINDHYP with a'; auto. |
---|
359 | Qed. |
---|
360 | *) |
---|
361 | (* * Infinitely many non-silent transitions *) |
---|
362 | |
---|
363 | coinductive forever_reactive (tr:transrel) (ge: genv tr): state tr → traceinf → Prop ≝ |
---|
364 | | forever_reactive_intro: ∀s1,s2,t,T. |
---|
365 | star tr ge s1 t s2 → t ≠ E0 → forever_reactive tr ge s2 T → |
---|
366 | forever_reactive tr ge s1 (t ⧻ T). |
---|
367 | (* |
---|
368 | lemma star_forever_reactive: |
---|
369 | ∀tr,ge,s1,t,s2,T. |
---|
370 | star tr ge s1 t s2 → forever_reactive tr ge s2 T → |
---|
371 | forever_reactive tr ge s1 (t ⧻ T). |
---|
372 | #tr #ge #s1 #t #s2 #T #H1 #H2 inversion H2; |
---|
373 | Proof. |
---|
374 | intros. inv H0. rewrite <- Eappinf_assoc. econstructor. |
---|
375 | eapply star_trans; eauto. |
---|
376 | red; intro. exploit Eapp_E0_inv; eauto. intros [P Q]. contradiction. |
---|
377 | auto. |
---|
378 | Qed. |
---|
379 | *) |
---|
380 | (* * * Outcomes for program executions *) |
---|
381 | |
---|
382 | (* * The four possible outcomes for the execution of a program: |
---|
383 | - Termination, with a finite trace of observable events |
---|
384 | and an integer value that stands for the process exit code |
---|
385 | (the return value of the main function). |
---|
386 | - Divergence with a finite trace of observable events. |
---|
387 | (At some point, the program runs forever without doing any I/O.) |
---|
388 | - Reactive divergence with an infinite trace of observable events. |
---|
389 | (The program performs infinitely many I/O operations separated |
---|
390 | by finite amounts of internal computations.) |
---|
391 | - Going wrong, with a finite trace of observable events |
---|
392 | performed before the program gets stuck. |
---|
393 | *) |
---|
394 | |
---|
395 | inductive program_behavior: Type[0] := |
---|
396 | | Terminates: trace -> int -> program_behavior |
---|
397 | | Diverges: trace -> program_behavior |
---|
398 | | Reacts: traceinf -> program_behavior |
---|
399 | | Goes_wrong: trace -> program_behavior. |
---|
400 | |
---|
401 | definition not_wrong : program_behavior → Prop ≝ λbeh. |
---|
402 | match beh with |
---|
403 | [ Terminates _ _ => True |
---|
404 | | Diverges _ => True |
---|
405 | | Reacts _ => True |
---|
406 | | Goes_wrong _ => False |
---|
407 | ]. |
---|
408 | |
---|
409 | (* * Given a characterization of initial states and final states, |
---|
410 | [program_behaves] relates a program behaviour with the |
---|
411 | sequences of transitions that can be taken from an initial state |
---|
412 | to a final state. *) |
---|
413 | (* |
---|
414 | Variable initial_state: state -> Prop. |
---|
415 | Variable final_state: state -> int -> Prop. |
---|
416 | *) |
---|
417 | inductive program_behaves (tr:transrel) |
---|
418 | (initial_state:state tr → Prop) |
---|
419 | (final_state : state tr → int → Prop) |
---|
420 | (ge: genv tr) : program_behavior -> Prop ≝ |
---|
421 | | program_terminates: ∀s,t,s',r. |
---|
422 | initial_state s -> |
---|
423 | star tr ge s t s' -> |
---|
424 | final_state s' r -> |
---|
425 | program_behaves tr initial_state final_state ge (Terminates t r) |
---|
426 | | program_diverges: ∀s,t,s'. |
---|
427 | initial_state s -> |
---|
428 | star tr ge s t s' -> forever_silent tr ge s' -> |
---|
429 | program_behaves tr initial_state final_state ge (Diverges t) |
---|
430 | | program_reacts: ∀s,T. |
---|
431 | initial_state s -> |
---|
432 | forever_reactive tr ge s T -> |
---|
433 | program_behaves tr initial_state final_state ge (Reacts T) |
---|
434 | | program_goes_wrong: ∀s,t,s'. |
---|
435 | initial_state s -> |
---|
436 | star tr ge s t s' -> |
---|
437 | nostep tr ge s' -> |
---|
438 | (∀r. ¬final_state s' r) -> |
---|
439 | program_behaves tr initial_state final_state ge (Goes_wrong t) |
---|
440 | | program_goes_initially_wrong: |
---|
441 | (∀s. ¬initial_state s) -> |
---|
442 | program_behaves tr initial_state final_state ge (Goes_wrong E0). |
---|
443 | |
---|
444 | (*End CLOSURES.*) |
---|
445 | (* |
---|
446 | (** * Simulations between two small-step semantics. *) |
---|
447 | |
---|
448 | (** In this section, we show that if two transition relations |
---|
449 | satisfy certain simulation diagrams, then every program behaviour |
---|
450 | generated by the first transition relation can also occur |
---|
451 | with the second transition relation. *) |
---|
452 | |
---|
453 | Section SIMULATION. |
---|
454 | |
---|
455 | (** The first small-step semantics is axiomatized as follows. *) |
---|
456 | |
---|
457 | Variable genv1: Type. |
---|
458 | Variable state1: Type. |
---|
459 | Variable step1: genv1 -> state1 -> trace -> state1 -> Prop. |
---|
460 | Variable initial_state1: state1 -> Prop. |
---|
461 | Variable final_state1: state1 -> int -> Prop. |
---|
462 | Variable ge1: genv1. |
---|
463 | *) |
---|
464 | |
---|
465 | record semantics : Type[1] ≝ |
---|
466 | { trans :> transrel |
---|
467 | ; initial : (state trans) → Prop |
---|
468 | ; final : (state trans) → int → Prop |
---|
469 | ; ge : (genv trans) |
---|
470 | }. |
---|
471 | |
---|
472 | (* |
---|
473 | (** The second small-step semantics is also axiomatized. *) |
---|
474 | |
---|
475 | Variable genv2: Type[0]. |
---|
476 | Variable state2: Type[0]. |
---|
477 | Variable step2: genv2 -> state2 -> trace -> state2 -> Prop. |
---|
478 | Variable initial_state2: state2 -> Prop. |
---|
479 | Variable final_state2: state2 -> int -> Prop. |
---|
480 | Variable ge2: genv2. |
---|
481 | |
---|
482 | (** We assume given a matching relation between states of both semantics. |
---|
483 | This matching relation must be compatible with initial states |
---|
484 | and with final states. *) |
---|
485 | |
---|
486 | Variable match_states: state1 -> state2 -> Prop. |
---|
487 | |
---|
488 | Hypothesis match_initial_states: |
---|
489 | forall st1, initial_state1 st1 -> |
---|
490 | exists st2, initial_state2 st2 /\ match_states st1 st2. |
---|
491 | |
---|
492 | Hypothesis match_final_states: |
---|
493 | forall st1 st2 r, |
---|
494 | match_states st1 st2 -> |
---|
495 | final_state1 st1 r -> |
---|
496 | final_state2 st2 r. |
---|
497 | *) |
---|
498 | |
---|
499 | record related_semantics : Type[1] ≝ |
---|
500 | { sem1 : semantics |
---|
501 | ; sem2 : semantics |
---|
502 | ; match_states : state sem1 → state sem2 → Prop |
---|
503 | ; match_initial_states : ∀st1. (initial sem1) st1 → ∃st2. (initial sem2) st2 ∧ match_states st1 st2 |
---|
504 | ; match_final_states : ∀st1,st2,r. match_states st1 st2 → (final sem1) st1 r → (final sem2) st2 r |
---|
505 | }. |
---|
506 | |
---|
507 | (* |
---|
508 | (** Simulation when one transition in the first program |
---|
509 | corresponds to zero, one or several transitions in the second program. |
---|
510 | However, there is no stuttering: infinitely many transitions |
---|
511 | in the source program must correspond to infinitely many |
---|
512 | transitions in the second program. *) |
---|
513 | |
---|
514 | Section SIMULATION_STAR_WF. |
---|
515 | |
---|
516 | (** [order] is a well-founded ordering associated with states |
---|
517 | of the first semantics. Stuttering steps must correspond |
---|
518 | to states that decrease w.r.t. [order]. *) |
---|
519 | |
---|
520 | Variable order: state1 -> state1 -> Prop. |
---|
521 | Hypothesis order_wf: well_founded order. |
---|
522 | |
---|
523 | Hypothesis simulation: |
---|
524 | forall st1 t st1', step1 ge1 st1 t st1' -> |
---|
525 | forall st2, match_states st1 st2 -> |
---|
526 | exists st2', |
---|
527 | (plus step2 ge2 st2 t st2' \/ (star step2 ge2 st2 t st2' /\ order st1' st1)) |
---|
528 | /\ match_states st1' st2'. |
---|
529 | *) |
---|
530 | record order_sim : Type[1] ≝ |
---|
531 | { sem :> related_semantics |
---|
532 | ; order : state (sem1 sem) → state (sem1 sem) → Prop |
---|
533 | (* ; order_wf ? *) |
---|
534 | ; simulation : ∀st1,t,st1'. step (sem1 sem) (ge (sem1 sem)) st1 t st1' → |
---|
535 | ∀st2. match_states sem st1 st2 → |
---|
536 | ∃st2'. (plus (sem2 sem) (ge (sem2 sem)) st2 t st2' ∨ |
---|
537 | (star (sem2 sem) (ge (sem2 sem)) st2 t st2' ∧ |
---|
538 | order st1' st1)) |
---|
539 | ∧ match_states sem st1' st2' |
---|
540 | }. |
---|
541 | |
---|
542 | lemma simulation_star_star: ∀sim:order_sim. |
---|
543 | ∀st1,t,st1'. star (sem1 sim) (ge (sem1 sim)) st1 t st1' → |
---|
544 | ∀st2. match_states sim st1 st2 → |
---|
545 | ∃st2'. star (sem2 sim) (ge (sem2 sim)) st2 t st2' ∧ match_states sim st1' st2'. |
---|
546 | #sim #st1 #t #st1' #H elim H; |
---|
547 | [ #st1'' #st2 #Hmatch |
---|
548 | %{ st2} % //; |
---|
549 | | #st1 #tA #st1A #tB #st1B #t #Hstep #Hstar #Ht #IH #st2 #Hmatch |
---|
550 | elim (simulation sim ??? Hstep ? Hmatch); #st2' *; #A #B |
---|
551 | elim (IH ? B); #st3' *; #C #D |
---|
552 | %{ st3'} % //; |
---|
553 | @(star_trans ??? tA st2' ? tB ?? C Ht) |
---|
554 | elim A /2/ * // |
---|
555 | ] qed. |
---|
556 | |
---|
557 | (* |
---|
558 | Lemma simulation_star_forever_silent: |
---|
559 | forall st1 st2, |
---|
560 | forever_silent step1 ge1 st1 -> match_states st1 st2 -> |
---|
561 | forever_silent step2 ge2 st2. |
---|
562 | Proof. |
---|
563 | assert (forall st1 st2, |
---|
564 | forever_silent step1 ge1 st1 -> match_states st1 st2 -> |
---|
565 | forever_silent_N step2 order ge2 st1 st2). |
---|
566 | cofix COINDHYP; intros. |
---|
567 | inversion H; subst. |
---|
568 | destruct (simulation H1 H0) as [st2' [A B]]. |
---|
569 | destruct A as [C | [C D]]. |
---|
570 | apply forever_silent_N_plus with st2' s2. |
---|
571 | auto. apply COINDHYP. assumption. assumption. |
---|
572 | apply forever_silent_N_star with st2' s2. |
---|
573 | auto. auto. apply COINDHYP. assumption. auto. |
---|
574 | intros. eapply forever_silent_N_forever; eauto. |
---|
575 | Qed. |
---|
576 | |
---|
577 | Lemma simulation_star_forever_reactive: |
---|
578 | forall st1 st2 T, |
---|
579 | forever_reactive step1 ge1 st1 T -> match_states st1 st2 -> |
---|
580 | forever_reactive step2 ge2 st2 T. |
---|
581 | Proof. |
---|
582 | cofix COINDHYP; intros. |
---|
583 | inv H. |
---|
584 | destruct (simulation_star_star H1 H0) as [st2' [A B]]. |
---|
585 | econstructor. eexact A. auto. |
---|
586 | eapply COINDHYP. eauto. auto. |
---|
587 | Qed. |
---|
588 | |
---|
589 | Lemma simulation_star_wf_preservation: |
---|
590 | forall beh, |
---|
591 | not_wrong beh -> |
---|
592 | program_behaves step1 initial_state1 final_state1 ge1 beh -> |
---|
593 | program_behaves step2 initial_state2 final_state2 ge2 beh. |
---|
594 | Proof. |
---|
595 | intros. inv H0; simpl in H. |
---|
596 | destruct (match_initial_states H1) as [s2 [A B]]. |
---|
597 | destruct (simulation_star_star H2 B) as [s2' [C D]]. |
---|
598 | econstructor; eauto. |
---|
599 | destruct (match_initial_states H1) as [s2 [A B]]. |
---|
600 | destruct (simulation_star_star H2 B) as [s2' [C D]]. |
---|
601 | econstructor; eauto. |
---|
602 | eapply simulation_star_forever_silent; eauto. |
---|
603 | destruct (match_initial_states H1) as [s2 [A B]]. |
---|
604 | econstructor; eauto. eapply simulation_star_forever_reactive; eauto. |
---|
605 | contradiction. |
---|
606 | contradiction. |
---|
607 | Qed. |
---|
608 | |
---|
609 | End SIMULATION_STAR_WF. |
---|
610 | |
---|
611 | Section SIMULATION_STAR. |
---|
612 | |
---|
613 | (** We now consider the case where we have a nonnegative integer measure |
---|
614 | associated with states of the first semantics. It must decrease when we take |
---|
615 | a stuttering step. *) |
---|
616 | |
---|
617 | Variable measure: state1 -> nat. |
---|
618 | |
---|
619 | Hypothesis simulation: |
---|
620 | forall st1 t st1', step1 ge1 st1 t st1' -> |
---|
621 | forall st2, match_states st1 st2 -> |
---|
622 | (exists st2', plus step2 ge2 st2 t st2' /\ match_states st1' st2') |
---|
623 | \/ (measure st1' < measure st1 /\ t = E0 /\ match_states st1' st2)%nat. |
---|
624 | |
---|
625 | Lemma simulation_star_preservation: |
---|
626 | forall beh, |
---|
627 | not_wrong beh -> |
---|
628 | program_behaves step1 initial_state1 final_state1 ge1 beh -> |
---|
629 | program_behaves step2 initial_state2 final_state2 ge2 beh. |
---|
630 | Proof. |
---|
631 | intros. |
---|
632 | apply simulation_star_wf_preservation with (ltof _ measure). |
---|
633 | apply well_founded_ltof. intros. |
---|
634 | destruct (simulation H1 H2) as [[st2' [A B]] | [A [B C]]]. |
---|
635 | exists st2'; auto. |
---|
636 | exists st2; split. right; split. rewrite B. apply star_refl. auto. auto. |
---|
637 | auto. auto. |
---|
638 | Qed. |
---|
639 | |
---|
640 | End SIMULATION_STAR. |
---|
641 | |
---|
642 | (** Lock-step simulation: each transition in the first semantics |
---|
643 | corresponds to exactly one transition in the second semantics. *) |
---|
644 | |
---|
645 | Section SIMULATION_STEP. |
---|
646 | |
---|
647 | Hypothesis simulation: |
---|
648 | forall st1 t st1', step1 ge1 st1 t st1' -> |
---|
649 | forall st2, match_states st1 st2 -> |
---|
650 | exists st2', step2 ge2 st2 t st2' /\ match_states st1' st2'. |
---|
651 | |
---|
652 | Lemma simulation_step_preservation: |
---|
653 | forall beh, |
---|
654 | not_wrong beh -> |
---|
655 | program_behaves step1 initial_state1 final_state1 ge1 beh -> |
---|
656 | program_behaves step2 initial_state2 final_state2 ge2 beh. |
---|
657 | Proof. |
---|
658 | intros. |
---|
659 | pose (measure := fun (st: state1) => 0%nat). |
---|
660 | assert (simulation': |
---|
661 | forall st1 t st1', step1 ge1 st1 t st1' -> |
---|
662 | forall st2, match_states st1 st2 -> |
---|
663 | (exists st2', plus step2 ge2 st2 t st2' /\ match_states st1' st2') |
---|
664 | \/ (measure st1' < measure st1 /\ t = E0 /\ match_states st1' st2)%nat). |
---|
665 | intros. destruct (simulation H1 H2) as [st2' [A B]]. |
---|
666 | left; exists st2'; split. apply plus_one; auto. auto. |
---|
667 | eapply simulation_star_preservation; eauto. |
---|
668 | Qed. |
---|
669 | |
---|
670 | End SIMULATION_STEP. |
---|
671 | |
---|
672 | (** Simulation when one transition in the first program corresponds |
---|
673 | to one or several transitions in the second program. *) |
---|
674 | |
---|
675 | Section SIMULATION_PLUS. |
---|
676 | |
---|
677 | Hypothesis simulation: |
---|
678 | forall st1 t st1', step1 ge1 st1 t st1' -> |
---|
679 | forall st2, match_states st1 st2 -> |
---|
680 | exists st2', plus step2 ge2 st2 t st2' /\ match_states st1' st2'. |
---|
681 | |
---|
682 | Lemma simulation_plus_preservation: |
---|
683 | forall beh, |
---|
684 | not_wrong beh -> |
---|
685 | program_behaves step1 initial_state1 final_state1 ge1 beh -> |
---|
686 | program_behaves step2 initial_state2 final_state2 ge2 beh. |
---|
687 | Proof. |
---|
688 | intros. |
---|
689 | pose (measure := fun (st: state1) => 0%nat). |
---|
690 | assert (simulation': |
---|
691 | forall st1 t st1', step1 ge1 st1 t st1' -> |
---|
692 | forall st2, match_states st1 st2 -> |
---|
693 | (exists st2', plus step2 ge2 st2 t st2' /\ match_states st1' st2') |
---|
694 | \/ (measure st1' < measure st1 /\ t = E0 /\ match_states st1' st2)%nat). |
---|
695 | intros. destruct (simulation H1 H2) as [st2' [A B]]. |
---|
696 | left; exists st2'; auto. |
---|
697 | eapply simulation_star_preservation; eauto. |
---|
698 | Qed. |
---|
699 | |
---|
700 | End SIMULATION_PLUS. |
---|
701 | |
---|
702 | (** Simulation when one transition in the first program |
---|
703 | corresponds to zero or one transitions in the second program. |
---|
704 | However, there is no stuttering: infinitely many transitions |
---|
705 | in the source program must correspond to infinitely many |
---|
706 | transitions in the second program. *) |
---|
707 | |
---|
708 | Section SIMULATION_OPT. |
---|
709 | |
---|
710 | Variable measure: state1 -> nat. |
---|
711 | |
---|
712 | Hypothesis simulation: |
---|
713 | forall st1 t st1', step1 ge1 st1 t st1' -> |
---|
714 | forall st2, match_states st1 st2 -> |
---|
715 | (exists st2', step2 ge2 st2 t st2' /\ match_states st1' st2') |
---|
716 | \/ (measure st1' < measure st1 /\ t = E0 /\ match_states st1' st2)%nat. |
---|
717 | |
---|
718 | Lemma simulation_opt_preservation: |
---|
719 | forall beh, |
---|
720 | not_wrong beh -> |
---|
721 | program_behaves step1 initial_state1 final_state1 ge1 beh -> |
---|
722 | program_behaves step2 initial_state2 final_state2 ge2 beh. |
---|
723 | Proof. |
---|
724 | assert (simulation': |
---|
725 | forall st1 t st1', step1 ge1 st1 t st1' -> |
---|
726 | forall st2, match_states st1 st2 -> |
---|
727 | (exists st2', plus step2 ge2 st2 t st2' /\ match_states st1' st2') |
---|
728 | \/ (measure st1' < measure st1 /\ t = E0 /\ match_states st1' st2)%nat). |
---|
729 | intros. elim (simulation H H0). |
---|
730 | intros [st2' [A B]]. left. exists st2'; split. apply plus_one; auto. auto. |
---|
731 | intros [A [B C]]. right. intuition. |
---|
732 | intros. eapply simulation_star_preservation; eauto. |
---|
733 | Qed. |
---|
734 | |
---|
735 | End SIMULATION_OPT. |
---|
736 | |
---|
737 | End SIMULATION. |
---|
738 | |
---|
739 | (** * Additional results about infinite reduction sequences *) |
---|
740 | |
---|
741 | (** We now show that any infinite sequence of reductions is either of |
---|
742 | the "reactive" kind or of the "silent" kind (after a finite number |
---|
743 | of non-silent transitions). The proof necessitates the axiom of |
---|
744 | excluded middle. This result is used in [Csem] and [Cminor] to |
---|
745 | relate the coinductive big-step semantics for divergence with the |
---|
746 | small-step notions of divergence. *) |
---|
747 | |
---|
748 | Require Import Classical. |
---|
749 | Unset Implicit Arguments. |
---|
750 | |
---|
751 | Section INF_SEQ_DECOMP. |
---|
752 | |
---|
753 | Variable genv: Type. |
---|
754 | Variable state: Type. |
---|
755 | Variable step: genv -> state -> trace -> state -> Prop. |
---|
756 | |
---|
757 | Variable ge: genv. |
---|
758 | |
---|
759 | Inductive State: Type := |
---|
760 | ST: forall (s: state) (T: traceinf), forever step ge s T -> State. |
---|
761 | |
---|
762 | Definition state_of_State (S: State): state := |
---|
763 | match S with ST s T F => s end. |
---|
764 | Definition traceinf_of_State (S: State) : traceinf := |
---|
765 | match S with ST s T F => T end. |
---|
766 | |
---|
767 | Inductive Step: trace -> State -> State -> Prop := |
---|
768 | | Step_intro: forall s1 t T s2 S F, |
---|
769 | Step t (ST s1 (t *** T) (@forever_intro genv state step ge s1 t s2 T S F)) |
---|
770 | (ST s2 T F). |
---|
771 | |
---|
772 | Inductive Steps: State -> State -> Prop := |
---|
773 | | Steps_refl: forall S, Steps S S |
---|
774 | | Steps_left: forall t S1 S2 S3, Step t S1 S2 -> Steps S2 S3 -> Steps S1 S3. |
---|
775 | |
---|
776 | Remark Steps_trans: |
---|
777 | forall S1 S2, Steps S1 S2 -> forall S3, Steps S2 S3 -> Steps S1 S3. |
---|
778 | Proof. |
---|
779 | induction 1; intros. auto. econstructor; eauto. |
---|
780 | Qed. |
---|
781 | |
---|
782 | Let Reactive (S: State) : Prop := |
---|
783 | forall S1, |
---|
784 | Steps S S1 -> |
---|
785 | exists S2, exists S3, exists t, Steps S1 S2 /\ Step t S2 S3 /\ t <> E0. |
---|
786 | |
---|
787 | Let Silent (S: State) : Prop := |
---|
788 | forall S1 t S2, Steps S S1 -> Step t S1 S2 -> t = E0. |
---|
789 | |
---|
790 | Lemma Reactive_or_Silent: |
---|
791 | forall S, Reactive S \/ (exists S', Steps S S' /\ Silent S'). |
---|
792 | Proof. |
---|
793 | intros. destruct (classic (exists S', Steps S S' /\ Silent S')). |
---|
794 | auto. |
---|
795 | left. red; intros. |
---|
796 | generalize (not_ex_all_not _ _ H S1). intros. |
---|
797 | destruct (not_and_or _ _ H1). contradiction. |
---|
798 | unfold Silent in H2. |
---|
799 | generalize (not_all_ex_not _ _ H2). intros [S2 A]. |
---|
800 | generalize (not_all_ex_not _ _ A). intros [t B]. |
---|
801 | generalize (not_all_ex_not _ _ B). intros [S3 C]. |
---|
802 | generalize (imply_to_and _ _ C). intros [D F]. |
---|
803 | generalize (imply_to_and _ _ F). intros [G J]. |
---|
804 | exists S2; exists S3; exists t. auto. |
---|
805 | Qed. |
---|
806 | |
---|
807 | Lemma Steps_star: |
---|
808 | forall S1 S2, Steps S1 S2 -> |
---|
809 | exists t, star step ge (state_of_State S1) t (state_of_State S2) |
---|
810 | /\ traceinf_of_State S1 = t *** traceinf_of_State S2. |
---|
811 | Proof. |
---|
812 | induction 1. |
---|
813 | exists E0; split. apply star_refl. auto. |
---|
814 | inv H. destruct IHSteps as [t' [A B]]. |
---|
815 | exists (t ** t'); split. |
---|
816 | simpl; eapply star_left; eauto. |
---|
817 | simpl in *. subst T. traceEq. |
---|
818 | Qed. |
---|
819 | |
---|
820 | Lemma Silent_forever_silent: |
---|
821 | forall S, |
---|
822 | Silent S -> forever_silent step ge (state_of_State S). |
---|
823 | Proof. |
---|
824 | cofix COINDHYP; intro S. case S. intros until f. simpl. case f. intros. |
---|
825 | assert (Step t (ST s1 (t *** T0) (forever_intro s1 t s0 f0)) |
---|
826 | (ST s2 T0 f0)). |
---|
827 | constructor. |
---|
828 | assert (t = E0). |
---|
829 | red in H. eapply H; eauto. apply Steps_refl. |
---|
830 | apply forever_silent_intro with (state_of_State (ST s2 T0 f0)). |
---|
831 | rewrite <- H1. assumption. |
---|
832 | apply COINDHYP. |
---|
833 | red; intros. eapply H. eapply Steps_left; eauto. eauto. |
---|
834 | Qed. |
---|
835 | |
---|
836 | Lemma Reactive_forever_reactive: |
---|
837 | forall S, |
---|
838 | Reactive S -> forever_reactive step ge (state_of_State S) (traceinf_of_State S). |
---|
839 | Proof. |
---|
840 | cofix COINDHYP; intros. |
---|
841 | destruct (H S) as [S1 [S2 [t [A [B C]]]]]. apply Steps_refl. |
---|
842 | destruct (Steps_star _ _ A) as [t' [P Q]]. |
---|
843 | inv B. simpl in *. rewrite Q. rewrite <- Eappinf_assoc. |
---|
844 | apply forever_reactive_intro with s2. |
---|
845 | eapply star_right; eauto. |
---|
846 | red; intros. destruct (Eapp_E0_inv _ _ H0). contradiction. |
---|
847 | change (forever_reactive step ge (state_of_State (ST s2 T F)) (traceinf_of_State (ST s2 T F))). |
---|
848 | apply COINDHYP. |
---|
849 | red; intros. apply H. |
---|
850 | eapply Steps_trans. eauto. |
---|
851 | eapply Steps_left. constructor. eauto. |
---|
852 | Qed. |
---|
853 | |
---|
854 | Theorem forever_silent_or_reactive: |
---|
855 | forall s T, |
---|
856 | forever step ge s T -> |
---|
857 | forever_reactive step ge s T \/ |
---|
858 | exists t, exists s', exists T', |
---|
859 | star step ge s t s' /\ forever_silent step ge s' /\ T = t *** T'. |
---|
860 | Proof. |
---|
861 | intros. |
---|
862 | destruct (Reactive_or_Silent (ST s T H)). |
---|
863 | left. |
---|
864 | change (forever_reactive step ge (state_of_State (ST s T H)) (traceinf_of_State (ST s T H))). |
---|
865 | apply Reactive_forever_reactive. auto. |
---|
866 | destruct H0 as [S' [A B]]. |
---|
867 | exploit Steps_star; eauto. intros [t [C D]]. simpl in *. |
---|
868 | right. exists t; exists (state_of_State S'); exists (traceinf_of_State S'). |
---|
869 | split. auto. |
---|
870 | split. apply Silent_forever_silent. auto. |
---|
871 | auto. |
---|
872 | Qed. |
---|
873 | |
---|
874 | End INF_SEQ_DECOMP. |
---|
875 | |
---|
876 | *) |
---|