source: src/common/Executions.ma @ 2500

Last change on this file since 2500 was 2487, checked in by campbell, 7 years ago

Set up "after_n_steps" to enforce an invariant on states.

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