source: src/common/Executions.ma @ 2203

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

A general result about simulations of executions.

File size: 6.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(* 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
86coinductive simulates (S1,S2:Type[0]) : execution S1 io_out io_in → execution S2 io_out io_in → Prop ≝
87| sim_stop : ∀tr,r,s1,s2,e1,e2,tr1,tr2.
88    steps S1 tr e1 (e_stop … tr1 r s1) →
89    steps S2 tr e2 (e_stop … tr2 r s2) →
90    simulates S1 S2 e1 e2
91| sim_steps : ∀tr,e1,e1',e2,e2'.
92    steps S1 tr e1 e1' →
93    steps S2 tr e2 e2' →
94    simulates S1 S2 e1' e2' →
95    simulates S1 S2 e1 e2
96| sim_interact : ∀o,k1,k2.
97    (∀i. simulates S1 S2 (k1 i) (k2 i)) →
98    simulates S1 S2 (e_interact … o k1) (e_interact … o k2).
99
100
101(* Result for lifting simulations on states to simulations on execution traces.
102   At the time of writing this hasn't been used in anger yet...
103   
104   This probably isn't the best route for the stages of the compiler that have
105   results in terms of structured traces, but it should be good for the
106   front-end.
107 *)
108
109let corec build_cofix_simulation
110  (FS1,FS2:fullexec io_out io_in)
111  (g1:global … FS1) (g2:global … FS2)
112  (SIM:state … g1 → state … g2 → Prop)
113  (s1:state … g1) (s2:state … g2)
114  (NF:is_final … FS1 g1 s1 = None ?)
115  (S:SIM s1 s2)
116  (SIM_FINAL: ∀x,y. SIM x y → is_final … FS1 g1 x = is_final … FS2 g2 y)
117  (SIM_GOOD: ∀x,y. SIM x y →
118         not_wrong ? (exec_inf_aux … FS1 g1 (step … FS1 g1 x)) →
119         is_final … FS1 g1 x = None ? →
120         ∃tr,x',y'. And (plus … FS1 g1 x tr x') (And (plus … FS2 g2 y tr y') (SIM x' y')) )
121  (NW:not_wrong ? (exec_inf_aux … FS1 g1 (step … FS1 g1 s1)))
122: simulates ?? (exec_inf_aux … FS1 g1 (step … FS1 g1 s1)) (exec_inf_aux ?? FS2 g2 (step … FS2 g2 s2)) ≝ ?.
123lapply (SIM_GOOD … S NW NF)
124* #tr * #s1' * #s2' * #P1 * #P2 #S'
125lapply (refl ? (is_final … FS1 g1 s1'))
126cases (is_final … s1') in ⊢ (???% → ?);
127[ #NF1
128  @(sim_steps … tr … (build_cofix_simulation … S' SIM_FINAL SIM_GOOD ?))
129  [ @(plus_exec … P1) //
130  | @(plus_exec … P2) <SIM_FINAL //
131  | @(not_wrong_steps … (plus_exec … P1 …)) //
132  | //
133  ]
134| #r #F1
135  cases (plus_final … P1 F1) #tr1' #S1
136  cases (plus_final … P2 ?) [ 3: <SIM_FINAL [ @F1 | // | skip ] | 2: skip ] #tr2' #S2
137  @(sim_stop … S1 S2)
138] qed.
139
140theorem lift_simulation : ∀FE1,FE2:fullexec io_out io_in.
141  ∀p1:program … FE1.  ∀p2:program … FE2.
142  let g1 ≝ make_global … p1 in
143  let g2 ≝ make_global … p2 in
144  ∀SIM: state … g1 → state … g2 → Prop.
145  ∀SIM_INIT: ∀s1. make_initial_state … p1 = OK ? s1 →
146             ∃s2. And (make_initial_state … p2 = OK ? s2) (SIM s1 s2).
147  ∀SIM_FINAL: ∀x,y. SIM x y → is_final … FE1 g1 x = is_final … FE2 g2 y.
148  ∀SIM_GOOD: ∀x,y. SIM x y →
149         not_wrong ? (exec_inf_aux … FE1 g1 (step … FE1 g1 x)) →
150         is_final … FE1 g1 x = None ? →
151         ∃tr,x',y'. And (plus … FE1 g1 x tr x') (And (plus … FE2 g2 y tr y') (SIM x' y')).
152  let e1 ≝ exec_inf … FE1 p1 in
153  let e2 ≝ exec_inf … FE2 p2 in
154  not_wrong … e1 →
155  simulates … e1 e2.
156
157#FE1 #FE2 #p1 #p2
158letin g1 ≝ (make_global … p1)
159letin g2 ≝ (make_global … p2)
160#SIM #SIM_INIT #SIM_FINAL #SIM_GOOD
161#NW
162cases (not_wrong_init … p1 NW)
163#s1 #I1
164cases (SIM_INIT … I1) #s2 * #I2 #S
165whd in NW:(??%) ⊢ (???%%);
166>I1 in NW ⊢ %; >I2 whd in ⊢ (??% → ???%%);
167change with g1 in match (make_global … p1);
168change with g2 in match (make_global … p2);
169
170>exec_inf_aux_unfold whd in ⊢ (??% → ???%?);
171lapply (SIM_FINAL … S)
172lapply (refl ? (is_final … s1))
173cases (is_final … s1) in ⊢ (???% → %);
174[ #F1 #F2 >(exec_inf_aux_unfold … FE2) whd in ⊢ (??% → ???%%);
175  <F2 whd in ⊢ (? → ???%%); #NW
176  @(sim_steps … E0 … (build_cofix_simulation … SIM_FINAL SIM_GOOD …)) try assumption
177  [ // | // | inversion NW #A #B #C #D #E try #F destruct assumption ]
178| #r #F1 #F2 #NW whd in ⊢ (???%%);
179  >exec_inf_aux_unfold whd in ⊢ (???%%);
180  <F2 whd in ⊢ (???%%);
181  @(sim_stop … (steps_stop …) (steps_stop …))
182] qed.
183
Note: See TracBrowser for help on using the repository browser.