source: src/common/Executions.ma @ 2314

Last change on this file since 2314 was 2206, checked in by campbell, 8 years ago

Add note about cost maps to simulation definition.

File size: 7.0 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(* In some places we do not consider wrong executions. *)
46
47coinductive not_wrong (state:Type[0]) : execution state io_out io_in → Prop ≝
48| nw_stop : ∀tr,i,s. not_wrong state (e_stop … tr i s)
49| nw_step : ∀tr,s,e. not_wrong state e → not_wrong state (e_step … tr s e)
50| nw_interact : ∀o,k. (∀i. not_wrong state (k i)) → not_wrong state (e_interact … o k).
51
52lemma not_wrong_not_wrong : ∀state,m.
53  ¬ (not_wrong state (e_wrong … m)).
54#state #m % #NW inversion NW
55#A #B #C #D #E destruct
56qed.
57
58lemma not_wrong_steps : ∀state,e,e',tr.
59  steps state tr e e' →
60  not_wrong state e →
61  not_wrong state e'.
62#state #e0 #e0' #tr0 #S elim S
63[ //
64| #tr #s #e #NW inversion NW
65  #A #B #C #D #E try #F destruct //
66| #tr #s #e #tr' #e' #S' #IH #NW @IH
67  inversion NW
68  #A #B #C #D #E try #F destruct //
69] qed.
70
71lemma not_wrong_init : ∀FE,p.
72  not_wrong ? (exec_inf … FE p) →
73  ∃s. make_initial_state … p = OK ? s.
74#FE #p whd in ⊢ (??% → ?);
75cases (make_initial_state ??? p)
76[ /2/
77| normalize #m #NW @⊥
78  inversion NW #H1 #H2 #H3 #H4 try #H5 destruct
79] qed.
80
81
82(* One execution is simulated by another, but possibly using a different number
83   of steps.  Note that we have to allow for several steps at the end to make
84   the trace match up.
85   
86   This assumes that the overall traces are exactly the same; this may not be
87   the case everywhere and we might have to add a cost label map.  (There is
88   a separate definition for the cost labelling stage, see
89   Clight/labelSpecification.ma.)
90 *)
91
92coinductive simulates (S1,S2:Type[0]) : execution S1 io_out io_in → execution S2 io_out io_in → Prop ≝
93| sim_stop : ∀tr,r,s1,s2,e1,e2,tr1,tr2.
94    steps S1 tr e1 (e_stop … tr1 r s1) →
95    steps S2 tr e2 (e_stop … tr2 r s2) →
96    simulates S1 S2 e1 e2
97| sim_steps : ∀tr,e1,e1',e2,e2'.
98    steps S1 tr e1 e1' →
99    steps S2 tr e2 e2' →
100    simulates S1 S2 e1' e2' →
101    simulates S1 S2 e1 e2
102| sim_interact : ∀o,k1,k2.
103    (∀i. simulates S1 S2 (k1 i) (k2 i)) →
104    simulates S1 S2 (e_interact … o k1) (e_interact … o k2).
105
106
107(* Result for lifting simulations on states to simulations on execution traces.
108   At the time of writing this hasn't been used in anger yet...
109   
110   This probably isn't the best route for the stages of the compiler that have
111   results in terms of structured traces, but it should be good for the
112   front-end.
113 *)
114
115let corec build_cofix_simulation
116  (FS1,FS2:fullexec io_out io_in)
117  (g1:global … FS1) (g2:global … FS2)
118  (SIM:state … g1 → state … g2 → Prop)
119  (s1:state … g1) (s2:state … g2)
120  (NF:is_final … FS1 g1 s1 = None ?)
121  (S:SIM s1 s2)
122  (SIM_FINAL: ∀x,y. SIM x y → is_final … FS1 g1 x = is_final … FS2 g2 y)
123  (SIM_GOOD: ∀x,y. SIM x y →
124         not_wrong ? (exec_inf_aux … FS1 g1 (step … FS1 g1 x)) →
125         is_final … FS1 g1 x = None ? →
126         ∃tr,x',y'. And (plus … FS1 g1 x tr x') (And (plus … FS2 g2 y tr y') (SIM x' y')) )
127  (NW:not_wrong ? (exec_inf_aux … FS1 g1 (step … FS1 g1 s1)))
128: simulates ?? (exec_inf_aux … FS1 g1 (step … FS1 g1 s1)) (exec_inf_aux ?? FS2 g2 (step … FS2 g2 s2)) ≝ ?.
129lapply (SIM_GOOD … S NW NF)
130* #tr * #s1' * #s2' * #P1 * #P2 #S'
131lapply (refl ? (is_final … FS1 g1 s1'))
132cases (is_final … s1') in ⊢ (???% → ?);
133[ #NF1
134  @(sim_steps … tr … (build_cofix_simulation … S' SIM_FINAL SIM_GOOD ?))
135  [ @(plus_exec … P1) //
136  | @(plus_exec … P2) <SIM_FINAL //
137  | @(not_wrong_steps … (plus_exec … P1 …)) //
138  | //
139  ]
140| #r #F1
141  cases (plus_final … P1 F1) #tr1' #S1
142  cases (plus_final … P2 ?) [ 3: <SIM_FINAL [ @F1 | // | skip ] | 2: skip ] #tr2' #S2
143  @(sim_stop … S1 S2)
144] qed.
145
146theorem lift_simulation : ∀FE1,FE2:fullexec io_out io_in.
147  ∀p1:program … FE1.  ∀p2:program … FE2.
148  let g1 ≝ make_global … p1 in
149  let g2 ≝ make_global … p2 in
150  ∀SIM: state … g1 → state … g2 → Prop.
151  ∀SIM_INIT: ∀s1. make_initial_state … p1 = OK ? s1 →
152             ∃s2. And (make_initial_state … p2 = OK ? s2) (SIM s1 s2).
153  ∀SIM_FINAL: ∀x,y. SIM x y → is_final … FE1 g1 x = is_final … FE2 g2 y.
154  ∀SIM_GOOD: ∀x,y. SIM x y →
155         not_wrong ? (exec_inf_aux … FE1 g1 (step … FE1 g1 x)) →
156         is_final … FE1 g1 x = None ? →
157         ∃tr,x',y'. And (plus … FE1 g1 x tr x') (And (plus … FE2 g2 y tr y') (SIM x' y')).
158  let e1 ≝ exec_inf … FE1 p1 in
159  let e2 ≝ exec_inf … FE2 p2 in
160  not_wrong … e1 →
161  simulates … e1 e2.
162
163#FE1 #FE2 #p1 #p2
164letin g1 ≝ (make_global … p1)
165letin g2 ≝ (make_global … p2)
166#SIM #SIM_INIT #SIM_FINAL #SIM_GOOD
167#NW
168cases (not_wrong_init … p1 NW)
169#s1 #I1
170cases (SIM_INIT … I1) #s2 * #I2 #S
171whd in NW:(??%) ⊢ (???%%);
172>I1 in NW ⊢ %; >I2 whd in ⊢ (??% → ???%%);
173change with g1 in match (make_global … p1);
174change with g2 in match (make_global … p2);
175
176>exec_inf_aux_unfold whd in ⊢ (??% → ???%?);
177lapply (SIM_FINAL … S)
178lapply (refl ? (is_final … s1))
179cases (is_final … s1) in ⊢ (???% → %);
180[ #F1 #F2 >(exec_inf_aux_unfold … FE2) whd in ⊢ (??% → ???%%);
181  <F2 whd in ⊢ (? → ???%%); #NW
182  @(sim_steps … E0 … (build_cofix_simulation … SIM_FINAL SIM_GOOD …)) try assumption
183  [ // | // | inversion NW #A #B #C #D #E try #F destruct assumption ]
184| #r #F1 #F2 #NW whd in ⊢ (???%%);
185  >exec_inf_aux_unfold whd in ⊢ (???%%);
186  <F2 whd in ⊢ (???%%);
187  @(sim_stop … (steps_stop …) (steps_stop …))
188] qed.
189
Note: See TracBrowser for help on using the repository browser.