source: src/common/Executions.ma @ 2428

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

Use much nicer definition for making several steps in the labelling
simulation.

File size: 8.7 KB
Line 
1include "common/SmallstepExec.ma".
2include "common/IO.ma".
3
4(* Equivalences of execution traces. *)
5
6(* A finite trace is produced by some prefix of an execution. *)
7
8inductive steps (state:Type[0]) : trace → execution state io_out io_in → execution state io_out io_in → Prop ≝
9| steps_stop : ∀tr,s,r. steps state tr (e_stop … tr s r) (e_stop … tr s r)
10| steps_step : ∀tr,s,e. steps state tr (e_step … tr s e) e
11| steps_steps : ∀tr,s,e,tr',e'. steps state tr e e' → steps state (tr'⧺tr) (e_step … tr' s e) e'.
12
13(* Go from individual steps to part of an execution trace. *)
14lemma plus_exec : ∀FE:fullexec io_out io_in. ∀gl,s,tr,s'.
15  plus … FE gl s tr s' →
16  is_final … FE gl s' = None ? →
17  steps (state … gl) tr
18    (exec_inf_aux … FE gl (step … FE gl s))
19    (exec_inf_aux … FE gl (step … FE gl s')).
20#FE #gl #s0 #tr0 #s0' #P elim P
21[ #s1 #tr #s2 #NF1 #EX #NF2 >EX >exec_inf_aux_unfold
22  whd in ⊢ (???%?); >NF2
23  %2
24| #s1 #tr #s2 #tr' #s3 #NF1 #EX1 #P2 #IH #NF3
25  >EX1 >exec_inf_aux_unfold
26  whd in ⊢ (???%?); >(plus_not_final … P2) /3/
27] qed.
28
29lemma plus_final : ∀FE:fullexec io_out io_in. ∀gl,s,tr,s',r.
30  plus … FE gl s tr s' →
31  is_final … FE gl s' = Some ? r →
32  ∃tr'. steps (state … gl) tr
33    (exec_inf_aux … FE gl (step … FE gl s))
34    (e_stop … tr' r s').
35#FE #gl #s0 #tr0 #s0' #r #P elim P
36[ #s1 #tr #s2 #NF1 #EX #F2 >EX >exec_inf_aux_unfold
37  whd in ⊢ (??(λ_.???%?)); >F2
38  %{tr} %1
39| #s1 #tr #s2 #tr' #s3 #NF1 #EX1 #P2 #IH #F3
40  >EX1 >exec_inf_aux_unfold
41  whd in ⊢ (??(λ_.???%?)); >(plus_not_final … P2)
42  cases (IH F3) #tr'' #S' %{tr''} /2/
43] qed.
44
45(* And similarly for after_n_steps *)
46
47lemma after_inv : ∀FE:fullexec io_out io_in.
48 ∀n,g,P,s.
49  after_n_steps (S n) … FE g s P →
50  ∃tr,s'.
51    P tr s' ∧
52    match is_final ?? FE g s' with
53    [ Some r ⇒ ∃tr'.
54      steps ? tr (exec_inf_aux … FE g (step … FE g s))
55                 (e_stop ??? tr' r s')
56    | None ⇒
57      steps ? tr (exec_inf_aux … FE g (step … FE g s))
58                 (exec_inf_aux … FE g (step … FE g s'))
59    ].
60#FE #n #g #P
61(* Rather nasty generalisation *)
62#s whd in ⊢ (% → ?); cases (is_final … s) [2: #r * ] whd in ⊢ (% → ?); #AW
63cut (∃tr,s'. P (E0⧺tr) s' ∧ ?) [3: #H @H | skip ]
64generalize in match E0 in AW ⊢ %; generalize in match s; -s
65elim n
66[ #s #tr whd in ⊢ (% → %);
67  cases (step … s) [ #o #K * | 3: #m * ]
68  * #tr' #s' #AW %{tr'} %{s'} %{AW}
69  lapply (refl ? (is_final … s')) cases (is_final … s') in ⊢ (???% → %);
70  [ #NF whd >exec_inf_aux_unfold whd in ⊢ (???%?); >NF @steps_step
71  | #r #F whd %{tr'} >exec_inf_aux_unfold whd in ⊢ (???%?); >F whd in ⊢ (???%?); @steps_stop
72  ]
73| #n' #IH #s #tr whd in ⊢ (% → ?);
74  cases (step … s) [ #o #K * | 3: #m * ] * #tr1 #s1
75  whd in ⊢ (% → ?); lapply (refl ? (is_final … s1)) cases (is_final … s1) in ⊢ (???% → %);
76  [ 2: #r #_ * ] #NF1 whd in ⊢ (% → ?); #AW1
77  cases (IH s1 ? AW1)
78  #tr' * #s' * #p #H1 %{(tr1⧺tr')} %{s'}
79  lapply (refl ? (is_final … s')) cases (is_final … s') in ⊢ (???% → %);
80  [ #NF <Eapp_assoc %{p} whd >exec_inf_aux_unfold whd in ⊢ (???%?); >NF1
81    @steps_steps >NF in H1; //
82  | #r #F <Eapp_assoc %{p} whd >exec_inf_aux_unfold whd in ⊢ (??(λ_.???%?)); >NF1
83    >F in H1; whd in ⊢ (% → ?); * #tr1 #H1 %{tr1}
84    @steps_steps @H1
85  ]
86] qed.
87
88(* In some places we do not consider wrong executions. *)
89
90coinductive not_wrong (state:Type[0]) : execution state io_out io_in → Prop ≝
91| nw_stop : ∀tr,i,s. not_wrong state (e_stop … tr i s)
92| nw_step : ∀tr,s,e. not_wrong state e → not_wrong state (e_step … tr s e)
93| nw_interact : ∀o,k. (∀i. not_wrong state (k i)) → not_wrong state (e_interact … o k).
94
95lemma not_wrong_not_wrong : ∀state,m.
96  ¬ (not_wrong state (e_wrong … m)).
97#state #m % #NW inversion NW
98#A #B #C #D #E destruct
99qed.
100
101lemma not_wrong_steps : ∀state,e,e',tr.
102  steps state tr e e' →
103  not_wrong state e →
104  not_wrong state e'.
105#state #e0 #e0' #tr0 #S elim S
106[ //
107| #tr #s #e #NW inversion NW
108  #A #B #C #D #E try #F destruct //
109| #tr #s #e #tr' #e' #S' #IH #NW @IH
110  inversion NW
111  #A #B #C #D #E try #F destruct //
112] qed.
113
114lemma not_wrong_init : ∀FE,p.
115  not_wrong ? (exec_inf … FE p) →
116  ∃s. make_initial_state … p = OK ? s.
117#FE #p whd in ⊢ (??% → ?);
118cases (make_initial_state ??? p)
119[ /2/
120| normalize #m #NW @⊥
121  inversion NW #H1 #H2 #H3 #H4 try #H5 destruct
122] qed.
123
124
125(* One execution is simulated by another, but possibly using a different number
126   of steps.  Note that we have to allow for several steps at the end to make
127   the trace match up.
128   
129   This assumes that the overall traces are exactly the same; this may not be
130   the case everywhere and we might have to add a cost label map.  (There is
131   a separate definition for the cost labelling stage, see
132   Clight/labelSpecification.ma.)
133 *)
134
135coinductive simulates (S1,S2:Type[0]) : execution S1 io_out io_in → execution S2 io_out io_in → Prop ≝
136| sim_stop : ∀tr,r,s1,s2,e1,e2,tr1,tr2.
137    steps S1 tr e1 (e_stop … tr1 r s1) →
138    steps S2 tr e2 (e_stop … tr2 r s2) →
139    simulates S1 S2 e1 e2
140| sim_steps : ∀tr,e1,e1',e2,e2'.
141    steps S1 tr e1 e1' →
142    steps S2 tr e2 e2' →
143    simulates S1 S2 e1' e2' →
144    simulates S1 S2 e1 e2
145| sim_interact : ∀o,k1,k2.
146    (∀i. simulates S1 S2 (k1 i) (k2 i)) →
147    simulates S1 S2 (e_interact … o k1) (e_interact … o k2).
148
149
150(* Result for lifting simulations on states to simulations on execution traces.
151   At the time of writing this hasn't been used in anger yet...
152   
153   This probably isn't the best route for the stages of the compiler that have
154   results in terms of structured traces, but it should be good for the
155   front-end.
156 *)
157
158let corec build_cofix_simulation
159  (FS1,FS2:fullexec io_out io_in)
160  (g1:global … FS1) (g2:global … FS2)
161  (SIM:state … g1 → state … g2 → Prop)
162  (s1:state … g1) (s2:state … g2)
163  (NF:is_final … FS1 g1 s1 = None ?)
164  (S:SIM s1 s2)
165  (SIM_FINAL: ∀x,y. SIM x y → is_final … FS1 g1 x = is_final … FS2 g2 y)
166  (SIM_GOOD: ∀x,y. SIM x y →
167         not_wrong ? (exec_inf_aux … FS1 g1 (step … FS1 g1 x)) →
168         is_final … FS1 g1 x = None ? →
169         ∃tr,x',y'. And (plus … FS1 g1 x tr x') (And (plus … FS2 g2 y tr y') (SIM x' y')) )
170  (NW:not_wrong ? (exec_inf_aux … FS1 g1 (step … FS1 g1 s1)))
171: simulates ?? (exec_inf_aux … FS1 g1 (step … FS1 g1 s1)) (exec_inf_aux ?? FS2 g2 (step … FS2 g2 s2)) ≝ ?.
172lapply (SIM_GOOD … S NW NF)
173* #tr * #s1' * #s2' * #P1 * #P2 #S'
174lapply (refl ? (is_final … FS1 g1 s1'))
175cases (is_final … s1') in ⊢ (???% → ?);
176[ #NF1
177  @(sim_steps … tr … (build_cofix_simulation … S' SIM_FINAL SIM_GOOD ?))
178  [ @(plus_exec … P1) //
179  | @(plus_exec … P2) <SIM_FINAL //
180  | @(not_wrong_steps … (plus_exec … P1 …)) //
181  | //
182  ]
183| #r #F1
184  cases (plus_final … P1 F1) #tr1' #S1
185  cases (plus_final … P2 ?) [ 3: <SIM_FINAL [ @F1 | // | skip ] | 2: skip ] #tr2' #S2
186  @(sim_stop … S1 S2)
187] qed.
188
189theorem lift_simulation : ∀FE1,FE2:fullexec io_out io_in.
190  ∀p1:program … FE1.  ∀p2:program … FE2.
191  let g1 ≝ make_global … p1 in
192  let g2 ≝ make_global … p2 in
193  ∀SIM: state … g1 → state … g2 → Prop.
194  ∀SIM_INIT: ∀s1. make_initial_state … p1 = OK ? s1 →
195             ∃s2. And (make_initial_state … p2 = OK ? s2) (SIM s1 s2).
196  ∀SIM_FINAL: ∀x,y. SIM x y → is_final … FE1 g1 x = is_final … FE2 g2 y.
197  ∀SIM_GOOD: ∀x,y. SIM x y →
198         not_wrong ? (exec_inf_aux … FE1 g1 (step … FE1 g1 x)) →
199         is_final … FE1 g1 x = None ? →
200         ∃tr,x',y'. And (plus … FE1 g1 x tr x') (And (plus … FE2 g2 y tr y') (SIM x' y')).
201  let e1 ≝ exec_inf … FE1 p1 in
202  let e2 ≝ exec_inf … FE2 p2 in
203  not_wrong … e1 →
204  simulates … e1 e2.
205
206#FE1 #FE2 #p1 #p2
207letin g1 ≝ (make_global … p1)
208letin g2 ≝ (make_global … p2)
209#SIM #SIM_INIT #SIM_FINAL #SIM_GOOD
210#NW
211cases (not_wrong_init … p1 NW)
212#s1 #I1
213cases (SIM_INIT … I1) #s2 * #I2 #S
214whd in NW:(??%) ⊢ (???%%);
215>I1 in NW ⊢ %; >I2 whd in ⊢ (??% → ???%%);
216change with g1 in match (make_global … p1);
217change with g2 in match (make_global … p2);
218
219>exec_inf_aux_unfold whd in ⊢ (??% → ???%?);
220lapply (SIM_FINAL … S)
221lapply (refl ? (is_final … s1))
222cases (is_final … s1) in ⊢ (???% → %);
223[ #F1 #F2 >(exec_inf_aux_unfold … FE2) whd in ⊢ (??% → ???%%);
224  <F2 whd in ⊢ (? → ???%%); #NW
225  @(sim_steps … E0 … (build_cofix_simulation … SIM_FINAL SIM_GOOD …)) try assumption
226  [ // | // | inversion NW #A #B #C #D #E try #F destruct assumption ]
227| #r #F1 #F2 #NW whd in ⊢ (???%%);
228  >exec_inf_aux_unfold whd in ⊢ (???%%);
229  <F2 whd in ⊢ (???%%);
230  @(sim_stop … (steps_stop …) (steps_stop …))
231] qed.
232
Note: See TracBrowser for help on using the repository browser.