source: src/Clight/labelSimulation.ma @ 2353

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

Put the post-loop cost label into the Clight while statement to get rid
of extra skips. (Soon to be followed by other loop constructs.)

File size: 53.6 KB
Line 
1
2include "Clight/labelSpecification.ma".
3include "Clight/CexecInd.ma".
4
5(* Useful for breaking up the labeling functions, because we don't care about
6   *which* cost labels are added here and so can throw away the resulting name
7   generator. *)
8lemma shift_fst : ∀A,B,C,D:Type[0].∀e:A×B.∀F:A → C.∀G:B → D.
9  \fst (let 〈x,y〉 ≝ e in 〈F x, G y〉) =  F (\fst e).
10#A #B #C #D * //
11qed.
12
13
14(* Similarly, lemma to break up label_expr, label_exprs and label_statement in
15   the labelling functions *)
16lemma label_gen_elim : ∀Syn:Type[0].∀syn,u.∀T:Type[0].∀L:Syn → universe CostTag → Syn × (universe CostTag). ∀F:Syn → universe CostTag → T. ∀P:T → Type[0].
17  (∀u'. P (F (\fst (L syn u)) u')) →
18  P (let 〈syn',u'〉 ≝ L syn u in F syn' u').
19#Syn #syn #u #T #L #F #P
20cases (L syn u)
21#syn' #u' #H @H
22qed.
23
24lemma add_cost_expr_elim : ∀e,u.∀T:Type[0].∀F:expr → universe CostTag → T. ∀P:T → Type[0].
25  (∀u',l. P (F (Expr (Ecost l e) (typeof e)) u')) →
26  P (let 〈e',u'〉 ≝ add_cost_expr e u in F e' u').
27#e #u #T #F #P #H whd in match (add_cost_expr ??);
28cases (fresh ??) #l #u' @H
29qed.
30
31
32lemma label_expr_type : ∀e,u.
33  typeof (\fst (label_expr e u)) = typeof e.
34* #e #ty #u >shift_fst //
35qed.
36
37(* Lemmas about trace_with_extra_labels *)
38
39lemma twel_refl : ∀tr. trace_with_extra_labels tr tr.
40#tr elim tr /2/
41qed.
42
43lemma twel_app : ∀tr1,tr2,tr1',tr2'.
44  trace_with_extra_labels tr1 tr1' →
45  trace_with_extra_labels tr2 tr2' →
46  trace_with_extra_labels (tr1⧺tr2) (tr1'⧺tr2').
47#tr1 #tr2 #tr1' #tr2' #twel1 elim twel1 /3/
48qed. 
49
50
51theorem label_expr_ok : ∀ge,ge',en,m.
52  related_globals_gen … label_fundef ge ge' →
53  (∀e,v,tr.
54   exec_expr ge en m e = OK … 〈v,tr〉 →
55   ∀u. ∃tr'. exec_expr ge' en m (\fst (label_expr e u)) = OK … 〈v,tr'〉 ∧
56             trace_with_extra_labels tr tr') ∧
57  (∀e,ty,b,o,tr. exec_lvalue' ge en m e ty = OK … 〈〈b,o〉,tr〉 →
58          ∀u. ∃tr'. exec_lvalue' ge' en m (\fst (label_expr_descr e u ty)) ty = OK … 〈〈b,o〉,tr'〉 ∧
59                    trace_with_extra_labels tr tr').
60(* Proof goes by breaking up the execution in the hypothesis, breaking up the
61   labelling function to get a new term and executing it by rewriting what we
62   learned from the hypothesis. *)
63#ge #ge' #en #m #RG @expr_lvalue_ind_combined
64[ 1,2: normalize /3 by ex_intro, conj/
65| * //
66 [ #id #ty #IH #v #tr #EX #u
67   cases (bind_inversion ????? EX) -EX * * #b #o #tr1 * #EX1 #EX
68   cases (bind_inversion ????? EX) -EX #v2 * #EX2 #EX
69   normalize in EX; destruct
70   cases (IH … EX1 u) #tr1' * #EX1' #T1
71   %{(tr1')} % [ whd in ⊢ (??%?); >EX1' whd in ⊢ (??%?); >EX2 @refl | // ]
72 | #e1 #ty #IH #v #tr #EX #u
73   cases (bind_inversion ????? EX) * * #b #o #tr1 * #EX1 #EX1r
74   cases (bind_inversion ????? EX1r) #v * #EXl #EXrem
75   normalize in EXrem; destruct
76   cases (IH … EX1 u) #tr1' * #EX1' #twel1
77   %{tr1'} >shift_fst in EX1'; >shift_fst >shift_fst #EX1' whd in ⊢ (?(??%?)?); >EX1'
78   whd in ⊢ (?(??%?)?); >EXl /2/
79 | #e1 #id #ty #IH #v #tr #EX #u
80   cases (bind_inversion ????? EX) * * #b #o #tr1 * #EX1 #EX1r
81   cases (bind_inversion ????? EX1r) #v * #EXl #EXrem
82   normalize in EXrem; destruct
83   cases (IH … EX1 u) #tr1' * #EX1' #twel1
84   %{tr1'} >shift_fst in EX1'; >shift_fst >shift_fst #EX1' % // whd in ⊢ (??%?); >EX1'
85   whd in ⊢ (??%?); >EXl @refl
86 ]
87| #v #ty #b #o #tr #EX #u %{tr} % [
88    whd in EX:(??%?) ⊢ (??%?); cases (lookup ??? v) in EX ⊢ %;
89    [ whd in ⊢ (??%? → ??%?); >(rgg_find_symbol … RG) //
90    | #b // ]
91  | // ]
92| #e1 #ty #IH #b #o #tr #EX #u
93  cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem
94  cases (IH … EX1 u) #tr1' * #EX1' #twel1
95  %{tr1'} >shift_fst whd in ⊢ (?(??%?)?); >EX1'
96  whd in ⊢ (?(??%?)?);
97  cases v1 in EX1rem ⊢ %; normalize #A try #B try #C destruct /2/
98| #ty' #e1 #ty #IH #v #tr #EX #u
99  cases (bind_inversion ????? EX) * * #b1 #o1 #tr1 * #EX1 #EX1rem
100  cases (IH … EX1 u) #tr1' * #EX1' #twel1
101  %{tr1'} >shift_fst >shift_fst >shift_fst whd in ⊢ (?(??%?)?);
102  whd in ⊢ (?(??(match % with [_⇒?|_⇒?])?)?); >EX1'
103  whd in ⊢ (?(??%?)?);
104  cases ty' in EX1rem ⊢ %;
105  [ 4: #ty' normalize #E destruct /2/
106  | *: normalize #A try #B try #C try #D destruct
107  ]
108| #ty #op #e1 #IH #v #tr #EX #u
109  cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem
110  cases (bind_inversion ????? EX1rem) #v2 * #EX2 #EXrem
111  normalize in EXrem; destruct
112  cases (IH … EX1 u) #tr1' * #EX1' #twel1
113  %{tr1'} % // >shift_fst
114  whd in ⊢ (??(????(?(???%)?))?);
115  @label_gen_elim #u2
116  whd in ⊢ (??%?); >EX1'
117  whd in ⊢ (??%?); >label_expr_type >EX2 @refl
118| #ty #op #e1 #e2 #IH1 #IH2 #v #tr #EX
119  cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem
120  cases (bind_inversion ????? EX1rem) * #v2 #tr2 * #EX2 #EX2rem
121  cases (bind_inversion ????? EX2rem) #v' * #EXop #EXop'
122  #u
123  cases (IH1 … EX1 u) #tr1' * #EX1' #twel1
124  >shift_fst
125  whd in ⊢ (??(λ_.?(??(????(?(???%)?))?)?));
126  @label_gen_elim #u2
127  cases (IH2 … EX2 u2) #tr2' * #EX2' #twel2
128  @label_gen_elim #u3 %{(tr1'⧺tr2')}
129  whd in ⊢ (?(??%?)?); >EX1'
130  whd in ⊢ (?(??%?)?); >EX2'
131  whd in ⊢ (?(??%?)?); >label_expr_type >label_expr_type >EXop
132  normalize in EXop'; destruct % /2/
133| #ty #ty' #e1 #IH #v #tr #EX #u
134  cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem
135  cases (bind_inversion ????? EX1rem) #v2 * #EX2 #EX2rem
136  normalize in EX2rem; destruct
137  cases (IH … EX1 u) #tr1' * #EX1' #twel1
138  %{tr1'} % // >shift_fst >shift_fst
139  whd in ⊢ (??%?); >EX1'
140  whd in ⊢ (??%?); >label_expr_type >EX2 @refl
141| #ty #e1 #e2 #e3 #IH1 #IH2 #IH3 #v #tr #EX #u
142  cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem
143  cases (bind_inversion ????? EX1rem) * * #EXguard #EXguardrem
144  cases (bind_inversion ????? EXguardrem) * #v2 #tr2 * #EX2 #EX2rem
145  normalize in EX2rem; destruct
146  cases (IH1 … EX1 u) #tr1' * #EX1' #twel1
147  >shift_fst whd in ⊢ (??(λ_.?(??(????(?(???%)?))?)?));
148  @label_gen_elim #u2
149  @label_gen_elim #u3
150  @add_cost_expr_elim #u4 #l4
151  @label_gen_elim #u5
152  @add_cost_expr_elim #u6 #l6
153  [ cases (IH2 … EX2 u2) | cases (IH3 … EX2 u4) ] #trx' * #EXx' #twelx
154  [ %{(tr1'⧺trx'⧺(Echarge l4))} | %{(tr1'⧺trx'⧺(Echarge l6))} ]
155  whd in ⊢ (?(??%?)?); >EX1'
156  whd in ⊢ (?(??%?)?); >label_expr_type >EXguard
157  whd in ⊢ (?(??%?)?); whd in ⊢ (?(??(match % with [_⇒?|_⇒?])?)?); >EXx'
158  normalize % // @twel_app // <(E0_right tr2) @twel_app /2/
159| #ty #e1 #e2 #IH1 #IH2 #v #tr #EX #u
160  cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem
161  cases (bind_inversion ????? EX1rem) * * #EXguard #EXguardrem
162  >shift_fst whd in ⊢ (??(λ_.?(??(????(?(???%)?))?)?));
163  @label_gen_elim #u2
164  @label_gen_elim #u3
165  @add_cost_expr_elim #u4 #l4
166  @add_cost_expr_elim #u5 #l5
167  [ cases (bind_inversion ????? EXguardrem) * #v2 #tr2 * #EX2 #EX2rem
168    cases (bind_inversion ????? EX2rem) * * #EX3 #EX3rem
169    -EX1rem -EXguardrem -EX2rem
170    cases (IH1 … EX1 u) #tr1' * #EX1' #twel1
171    cases (IH2 … EX2 u2) #tr2' * #EX2' #twel2
172    %{(tr1'⧺(tr2'⧺E0)⧺Echarge l4)}
173    whd in ⊢ (?(??%?)?); >EX1'
174    whd in ⊢ (?(??%?)?); >label_expr_type >EX2' >EXguard
175    whd in ⊢ (?(??%?)?); whd in ⊢ (?(??(match % with [_⇒?|_⇒?])?)?);
176    whd in ⊢ (?(??(match (match % with [_⇒?|_⇒?]) with [_⇒?|_⇒?])?)?); >EX2'
177    whd in ⊢ (?(??(match (match % with [_⇒?|_⇒?]) with [_⇒?|_⇒?])?)?); >label_expr_type >EX3
178    whd in EX3rem:(??%%) ⊢ %; destruct % [ 1,3: @refl | *: @twel_app // <(E0_right tr2) @twel_app /2/ ]
179  | cases (IH1 … EX1 u) #tr1' * #EX1' #twel1
180    %{(tr1'⧺E0⧺Echarge l5)}
181    whd in ⊢ (?(??%?)?); >EX1'
182    whd in ⊢ (?(??%?)?); >label_expr_type >EXguard
183    whd in EXguardrem:(??%%); destruct % // <(E0_right tr) @twel_app /2/
184  ]
185| #ty #e1 #e2 #IH1 #IH2 #v #tr #EX #u
186  cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem
187  cases (bind_inversion ????? EX1rem) * * #EXguard #EXguardrem
188  >shift_fst whd in ⊢ (??(λ_.?(??(????(?(???%)?))?)?));
189  @label_gen_elim #u2
190  @add_cost_expr_elim #u4 #l4
191  @label_gen_elim #u3
192  @add_cost_expr_elim #u5 #l5
193  [ cases (IH1 … EX1 u) #tr1' * #EX1' #twel1
194    %{(tr1'⧺Echarge l4)}
195    whd in ⊢ (?(??%?)?); >EX1'
196    whd in ⊢ (?(??%?)?); >label_expr_type >EXguard
197    whd in EXguardrem:(??%%) ⊢ %; destruct % // <(E0_right tr) /3/
198  | cases (bind_inversion ????? EXguardrem) * #v2 #tr2 * #EX2 #EX2rem
199    cases (bind_inversion ????? EX2rem) * * #EX3 #EX3rem
200    cases (IH1 … EX1 u) #tr1' * #EX1' #twel1
201    cases (IH2 … EX2 u4) #tr2' * #EX2' #twel2
202    %{(tr1'⧺(tr2'⧺E0)⧺Echarge l5)}
203    whd in ⊢ (?(??%?)?); >EX1'
204    whd in ⊢ (?(??%?)?); >label_expr_type >EX2' >EXguard
205    whd in ⊢ (?(??%?)?); whd in ⊢ (?(??(match % with [_⇒?|_⇒?])?)?);
206    whd in ⊢ (?(??(match (match % with [_⇒?|_⇒?]) with [_⇒?|_⇒?])?)?); >EX2'
207    whd in ⊢ (?(??(match (match % with [_⇒?|_⇒?]) with [_⇒?|_⇒?])?)?); >label_expr_type >EX3
208    whd in EX3rem:(??%%) ⊢ %; destruct % // @twel_app // <(E0_right tr2) @twel_app /2/
209  ]
210| #ty #ty' #v #tr normalize /3/
211| #ty #e1 #ty' #id #IH #b #o #tr #EX #u cases ty' in IH EX ⊢ %;
212  [ 7: #id #fl #IH #EX
213    cases (bind_inversion ????? EX) * * #b1 #o1 #tr1 * #EX1 #EX1rem
214    cases (bind_inversion ????? EX1rem) #n * #EXoff #EXoffrem
215    whd in EXoffrem:(???%); destruct >shift_fst >shift_fst
216    cases (IH … EX1 u) #tr1' * #EX1' #twel1
217    %{tr1'} % //
218    whd in ⊢ (??%?); whd in ⊢ (??(match % with [_⇒?|_⇒?])?); >EX1'
219    whd in ⊢ (??%?); >EXoff whd in ⊢ (??%?); @refl
220  | 8: #id #fl #IH #EX
221    cases (bind_inversion ????? EX) * * #b1 #o1 #tr1 * #EX1 #EX1rem
222    whd in EX1rem:(???%); destruct >shift_fst >shift_fst
223    cases (IH … EX1 u) #tr1' * #EX1' #twel1
224    %{tr1'} % //
225    whd in ⊢ (??%?); whd in ⊢ (??(match % with [_⇒?|_⇒?])?); >EX1'
226    whd in ⊢ (??%?); @refl
227  | *: normalize #A #B try #C try #D try #F destruct
228  ]
229| #ty #l #e1 #IH #v #tr #EX #u
230  cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem
231  whd in EX1rem:(???%); destruct
232  cases (IH … EX1 u) #tr1' * #EX1' #twel1 %{(tr1'@Echarge l)}
233  >shift_fst >shift_fst whd in ⊢ (?(??%?)?); >EX1'
234  whd in ⊢ (?(??%?)?); /3/
235| #e1 #ty #NLV #b #o #tr #EX @⊥
236  cases e1 in NLV EX; normalize //
237  #A #B #C try #D try #F destruct
238] qed.
239
240lemma label_exprs_ok : ∀ge,ge'.
241   related_globals_gen … label_fundef ge ge' →
242   ∀en,m,es,vs,tr.
243   exec_exprlist ge en m es = OK … 〈vs,tr〉 →
244   ∀u. ∃tr'. exec_exprlist ge' en m (\fst (label_exprs es u)) = OK … 〈vs,tr'〉 ∧
245             trace_with_extra_labels tr tr'.
246#ge #ge' #RG #en #m #es elim es
247[ #vs #tr #EX whd in EX:(??%?); destruct #u %{E0} /2/
248| #e #tl #IH #vs #tr #EX
249  cases (bind_inversion ????? EX) -EX * #v1 #tr1 * #EX1 #EX
250  cases (bind_inversion ????? EX) -EX * #tl' #tr' * #EX2 #EX
251  whd in EX:(??%%); destruct
252  #u whd in match (label_exprs ??); @label_gen_elim #u' >shift_fst
253  cases (proj1 ?? (label_expr_ok ge ge' en m RG) ??? EX1 u) #tr1' * #EX1' #T1
254  cases (IH … EX2 u') #tr'' * #EX2' #T2
255  % [2: % [ whd in ⊢ (??%?); >EX1' in ⊢ (??%?);
256    whd in ⊢ (??%?); >EX2' in ⊢ (??%?); @refl
257  | /2/ ] | skip ]
258] qed.
259
260
261(* Now we move on to describe the simulation relation.  First, relate the
262   continuations. *)
263inductive cont_with_labels : cont → cont → Prop ≝
264| cwl_stop : cont_with_labels Kstop Kstop
265| cwl_seq : ∀u,s,k,k'. cont_with_labels k k' → cont_with_labels (Kseq s k) (Kseq (\fst (label_statement s u)) k')
266| cwl_while : ∀ue,e,us,s,cl,cs,cpost,k,k'.
267    cont_with_labels k k' →
268    (cl = None ? ∨ cl = Some ? cpost) →
269    cont_with_labels (Kwhile e s cl k) (Kwhile (\fst (label_expr e ue)) (Scost cs (\fst (label_statement s us))) (Some ? cpost) k')
270| cwl_dowhile : ∀ue,e,us,s,cs,cpost,k,k'.
271    cont_with_labels k k' →
272    cont_with_labels (Kdowhile e s k) (Kdowhile (\fst (label_expr e ue)) (Scost cs (\fst (label_statement s us))) (Kseq (Scost cpost Sskip) k'))
273| cwl_for1 : ∀ue,e,us1,s1,us2,s2,cs,cpost,k,k'.
274    cont_with_labels k k' →
275    cont_with_labels (Kseq (Sfor Sskip e s1 s2) k) (Kseq (Sfor Sskip (\fst (label_expr e ue)) (\fst (label_statement s1 us1)) (Scost cs (\fst (label_statement s2 us2)))) (Kseq (Scost cpost Sskip) k'))
276| cwl_for2 : ∀ue,e,us1,s1,us2,s2,cs,cpost,k,k'. cont_with_labels k k' → cont_with_labels (Kfor2 e s1 s2 k) (Kfor2 (\fst (label_expr e ue)) (\fst (label_statement s1 us1)) (Scost cs (\fst (label_statement s2 us2))) (Kseq (Scost cpost Sskip) k'))
277| cwl_for3 : ∀ue,e,us1,s1,us2,s2,cs,cpost,k,k'. cont_with_labels k k' → cont_with_labels (Kfor3 e s1 s2 k) (Kfor3 (\fst (label_expr e ue)) (\fst (label_statement s1 us1)) (Scost cs (\fst (label_statement s2 us2))) (Kseq (Scost cpost Sskip) k'))
278| cwl_switch : ∀k,k'. cont_with_labels k k' → cont_with_labels (Kswitch k) (Kswitch k')
279| cwl_call : ∀g,r,f,en,k,k'. cont_with_labels k k' → cont_with_labels (Kcall r f en k) (Kcall r (\fst (label_function g f)) en k')
280| cwl_seqls : ∀ls,u,k,k'. cont_with_labels k k' →
281    cont_with_labels (Kseq (seq_of_labeled_statement ls) k) (Kseq (seq_of_labeled_statement (\fst (label_lstatements ls u))) k').
282
283lemma call_cont_with_labels : ∀k,k'.
284  cont_with_labels k k' →
285  cont_with_labels (call_cont k) (call_cont k').
286#k0 #k0' #K elim K /2/
287qed.
288
289(* Now define almost all of the simulation relation... *)
290inductive state_with_labels_partial : state → state → Prop ≝
291| swl_state : ∀g,f,us,s,k,k',e,m. cont_with_labels k k' → state_with_labels_partial (State f s k e m) (State (\fst (label_function g f)) (\fst (label_statement s us)) k' e m)
292(* Extra matching states that we can reach that don't quite correspond to the
293   labelling function *)
294| swl_whilestate : ∀g,f,ua,a,us,s,cl,cs,cpost,k,k',e,m. cont_with_labels k k' →
295    (cl = None ? ∨ cl = Some ? cpost) →
296    state_with_labels_partial (State f (Swhile a s cl) k e m) (State (\fst (label_function g f)) (Swhile (\fst (label_expr a ua)) (Scost cs (\fst (label_statement s us))) (Some ? cpost)) k' e m)
297| swl_dowhilestate : ∀g,f,ua,a,us,s,cs,cpost,k,k',e,m. cont_with_labels k k' →
298    state_with_labels_partial (State f (Sdowhile a s) k e m) (State (\fst (label_function g f)) (Sdowhile (\fst (label_expr a ua)) (Scost cs (\fst (label_statement s us)))) (Kseq (Scost cpost Sskip) k') e m)
299| swl_forstate : ∀g,f,ua2,a2,us3,s3,us,s,cs,cpost,k,k',e,m. cont_with_labels k k' →
300    state_with_labels_partial (State f (Sfor Sskip a2 s3 s) k e m) (State (\fst (label_function g f)) (Sfor Sskip (\fst (label_expr a2 ua2)) (\fst (label_statement s3 us3)) (Scost cs (\fst (label_statement s us)))) (Kseq (Scost cpost Sskip) k') e m)
301(* and the rest *)
302| swl_callstate : ∀g,fd,args,k,k',m. cont_with_labels k k' → state_with_labels_partial (Callstate fd args k m) (Callstate (\fst (label_fundef g fd)) args k' m)
303| swl_returnstate : ∀res,k,k',m. cont_with_labels k k' → state_with_labels_partial (Returnstate res k m) (Returnstate res k' m)
304| swl_finalstate : ∀r. state_with_labels_partial (Finalstate r) (Finalstate r)
305.
306
307(* ... and add the states where the cases from switch statements are expanded.
308   We do these separately because in the LSdefault case we have to execute a
309   cost label alongside an arbitrary statement, and we want to reuse the result
310   on arbitrary statements we get for state_with_labels_partial. *)
311inductive state_with_labels : state → state → Prop ≝
312| swl_partial : ∀s,s'. state_with_labels_partial s s' → state_with_labels s s'
313| swl_switchstate : ∀g,f,u,ls,k,k',e,m. cont_with_labels k k' →
314    state_with_labels (State f (seq_of_labeled_statement ls) k e m)
315                      (State (\fst (label_function g f)) (seq_of_labeled_statement (\fst  (label_lstatements ls u))) k' e m)
316.
317
318(* Some details are invariant under labelling. *)
319lemma label_function_return : ∀g,f.
320  fn_return (\fst (label_function g f)) = fn_return f.
321#g * #rty #params #vars #body
322whd in match (label_function ??);
323cases (label_statement ??) #body' #u'
324whd in ⊢ (??(?(???%))?);
325cases (add_cost_before ??) #body'' #u''
326//
327qed.
328
329lemma label_expr_fun_typeof : ∀a,u.
330  fun_typeof (\fst (label_expr a u)) = fun_typeof a.
331#a #u whd in ⊢ (??%?); >label_expr_type @refl
332qed.
333
334lemma label_fundef_typeof_fundef : ∀g,fd.
335  type_of_fundef (\fst (label_fundef g fd)) = type_of_fundef fd.
336#g * //
337* #rty #args #vars #body
338normalize cases (label_statement ??) #body' #u
339normalize cases (fresh ??) //
340qed.
341
342lemma label_fn_params : ∀g,f.
343  fn_params (\fst (label_function g f)) = fn_params f.
344#g * #rty #params #vars #s whd in ⊢ (??(?(???%))?); @breakup_pair @breakup_pair //
345qed.
346
347lemma label_fn_vars : ∀g,f.
348  fn_vars (\fst (label_function g f)) = fn_vars f.
349#g * #rty #params #vars #s whd in ⊢ (??(?(???%))?); @breakup_pair @breakup_pair //
350qed.
351
352(* Some annoying rewrite rules *)
353lemma exec_lvalue_labelled : ∀ge,e,m,a,ty,u.
354  exec_lvalue ge e m (\fst (label_expr (Expr a ty) u)) =
355  exec_lvalue' ge e m (\fst (label_expr_descr a u ty)) ty.
356#ge #e #m #a #ty #u
357whd in ⊢ (??(????(???%))?); >shift_fst @refl
358qed.
359
360lemma opt_find_funct : ∀ge,ge',m,vf,fd.
361  related_globals_gen … label_fundef ge ge' →
362  opt_to_io io_out io_in … m (find_funct … ge vf) = Value … fd →
363  ∃u. opt_to_io io_out io_in … m (find_funct … ge' vf) = Value … (\fst (label_fundef u fd)).
364#ge #ge' #m #vf #fd #RG
365lapply (rgg_find_funct … RG … vf fd)
366cases (find_funct … vf)
367[ #_ #E normalize in E; destruct
368| #fd' #H #E normalize in E; destruct cases (H (refl ??)) #u #FF %{u} >FF //
369] qed.
370
371lemma labelled_not_skip : ∀s,u.
372  s ≠ Sskip →
373  (\fst (label_statement s u)) ≠ Sskip.
374* #u
375[ * #H cases (H (refl ??))
376| *: #a try #b try #c try #d try #e
377     (* Use the state-monad-like structure of the labelling function to break
378        it up *)
379     whd in match (label_statement ??);
380     repeat @(breakup_pair ???? (λx.\fst x ≠ Sskip))
381     % #E destruct
382] qed.
383
384lemma labelled_is_not_skip : ∀s,u.
385  s ≠ Sskip →
386  ∃pf. is_Sskip (\fst (label_statement s u)) = inr … pf.
387#s #u #NE
388cases (is_Sskip ?)
389[ #E @⊥ @(absurd ? E) @labelled_not_skip //
390| /2/
391] qed.
392
393lemma label_select_ls : ∀sz,i,ls,u.
394  ∃u'.
395    select_switch sz i (\fst (label_lstatements ls u)) =
396    \fst (label_lstatements (select_switch sz i ls) u').
397#sz #i #ls @(labeled_statements_ind … ls)
398[ #s #u % [2: whd in match (label_lstatements ??);
399  @label_gen_elim #u1 >shift_fst @refl | skip ]
400| #sz' #i' #s #tl #IH #u
401  whd in match (label_lstatements ??);
402  whd in match (select_switch ?? (LScase ????));
403  @intsize_eq_elim_elim
404  [ #NE
405    @label_gen_elim #u1 @label_gen_elim #u2 @label_gen_elim #u3
406    cases (IH u2)
407    #u4 #E %{u4} whd in ⊢ (??%?);
408    >intsize_eq_elim_false //
409  | #E <E in i' ⊢ %; #i' whd
410    @eq_bv_elim
411    [ #Ei >Ei
412      %{u}
413      whd in match (label_lstatements (if ? then ? else ?) ?);
414      @label_gen_elim #u1 @label_gen_elim #u2 @label_gen_elim #u3
415      whd in ⊢ (??%?);
416      >intsize_eq_elim_true
417      >eq_bv_true
418      @refl
419    | #NEi
420      @label_gen_elim #u1 @label_gen_elim #u2 @label_gen_elim #u3
421       whd in ⊢ (??(λ_.??%?));
422       >intsize_eq_elim_true
423       >eq_bv_false //
424    ]
425  ]
426] qed.
427
428(* Break up labelling function in one go for statements. *)
429lemma blindly_label : ∀u,s. ∀P:statement → Prop.
430match s with
431[ Sskip ⇒ P Sskip
432| Sassign e1 e2 ⇒ ∀u1,u2. P (Sassign (\fst (label_expr e1 u1)) (\fst (label_expr e2 u2)))
433| Scall eo e args ⇒ ∀u1,u2,u3. P (Scall (\fst (label_opt_expr eo u1)) (\fst (label_expr e u2)) (\fst (label_exprs args u3)))
434| Ssequence s1 s2 ⇒ ∀u1,u2. P (Ssequence (\fst (label_statement s1 u1)) (\fst (label_statement s2 u2)))
435| Sifthenelse e s1 s2 ⇒ ∀u1,u2,u3,c2,c3. P (Sifthenelse (\fst (label_expr e u1)) (Scost c2 (\fst (label_statement s1 u2))) (Scost c3 (\fst (label_statement s2 u3))))
436| Swhile e s1 cl ⇒ ∀u1,u2,cs,cpost. cl = None ? ∨ cl = Some ? cpost → P (Swhile (\fst (label_expr e u1)) (Scost cs (\fst (label_statement s1 u2))) (Some ? cpost))
437| Sdowhile e s1 ⇒ ∀u1,u2,cs,cpost. P (Ssequence (Sdowhile (\fst (label_expr e u1)) (Scost cs (\fst (label_statement s1 u2)))) (Scost cpost Sskip))
438| Sfor s1 e s2 s3 ⇒ ∀u1,u2,u3,u4,c3,c4. P (Ssequence (Sfor (\fst (label_statement s1 u1)) (\fst (label_expr e u2)) (\fst (label_statement s2 u3)) (Scost c3 (\fst (label_statement s3 u4)))) (Scost c4 Sskip))
439| Sbreak ⇒ P Sbreak
440| Scontinue ⇒ P Scontinue
441| Sreturn eo ⇒ ∀u1. P (Sreturn (\fst (label_opt_expr eo u1)))
442| Sswitch e ls ⇒ ∀u1,u2. P (Sswitch (\fst (label_expr e u1)) (\fst (label_lstatements ls u2)))
443| Slabel l s1 ⇒ ∀u1,cs. P (Slabel l (Scost cs (\fst (label_statement s1 u1))))
444| Sgoto l ⇒ P (Sgoto l)
445| Scost c s1 ⇒ ∀u1. P (Scost c (\fst (label_statement s1 u1)))
446] → P (\fst (label_statement s u)). 
447#u * // #A #B #C try #D try #E try #F whd in match (label_statement ??);
448@label_gen_elim #u1 //
449@label_gen_elim #u2 //
450[ 6: >shift_fst //
451| 3: @label_gen_elim #u3 >shift_fst >shift_fst
452     cases C in E ⊢ %; /3/
453| *: @label_gen_elim #u3 //
454     @label_gen_elim #u4
455     [ @label_gen_elim #u5 >shift_fst >shift_fst //
456     | >shift_fst >shift_fst //
457     | @label_gen_elim #u5 >shift_fst >shift_fst >shift_fst //
458     ]
459] qed.
460
461(* Apply induction hypothesis in label_find_label proof below while getting
462   Matita to infer the continuations k0 and k0', and the universe u0, rather
463   than having to give them explicitly. *)
464lemma lfl_IH : ∀s0,lbl.
465  ∀C:option (statement×cont) → option (statement×cont) → Prop.
466  ∀IH:cont → cont → universe CostTag → Prop.
467  (∀k,k',u. cont_with_labels k k' → IH k k' u) →
468  ∀k0,k0',u0. cont_with_labels k0 k0' →
469   (IH k0 k0' u0 →
470    C (find_label lbl s0 k0) (find_label lbl (\fst (label_statement s0 u0)) k0')) →
471   C (find_label lbl s0 k0) (find_label lbl (\fst (label_statement s0 u0)) k0').
472/3/
473qed.
474
475(* Finding a goto label in a cost-labelled program gives a labelled version of
476   the statement and continuation found by the original function, if any. *)
477lemma label_find_label : ∀lbl,s,k,k',u.
478  cont_with_labels k k' →
479  match find_label lbl s k with
480  [ Some r' ⇒ let 〈s1,k1〉 ≝ r' in
481    ∃u',cs,k1'.
482    find_label lbl (\fst (label_statement s u)) k' = Some ? 〈Scost cs (\fst (label_statement s1 u')), k1'〉 ∧
483    cont_with_labels k1 k1'
484  | None ⇒ find_label lbl (\fst (label_statement s u)) k' = None ?
485  ].
486#lbl #s @(statement_ind2 ? (λls.
487  ∀k,k',u.
488  cont_with_labels k k' →
489  match find_label_ls lbl ls k with
490  [ Some r' ⇒ let 〈s1,k1〉 ≝ r' in
491    ∃u',cs,k1'.
492    find_label_ls lbl (\fst (label_lstatements ls u)) k' = Some ? 〈Scost cs (\fst (label_statement s1 u')), k1'〉 ∧
493    cont_with_labels k1 k1'
494  | None ⇒ find_label_ls lbl (\fst (label_lstatements ls u)) k' = None ?
495  ])
496 … s)
497[ #k #k' #u #F @refl
498| #e1 #e2 #k #k' #u #K @blindly_label #u1 #u2 whd @refl
499| #e0 #e #args #k #k' #u #K @blindly_label #u1 #u2 #u3 whd @refl
500| #sA #sB #IH1 #IH2 #k #k' #u #K @blindly_label #u1 #u2 whd in match (find_label ???);
501  whd in match (find_label ?? k');
502  @(lfl_IH sA … IH1) [ /2/ ]
503  cases (find_label ???)
504  [ whd in ⊢ (% → match % with [_⇒?|_⇒?]); #FIND1'
505    @(lfl_IH … IH2) [ // ]
506    cases (find_label ???)
507    [ whd in ⊢ (% → %); #FIND2' whd in ⊢ (??%?); >FIND1' >FIND2' @refl
508    | * #s3 #k3 whd in ⊢ (% → %); * #u3 * #cs * #k1' * #FIND2' #K1'
509      % [2: %{cs} %{k1'} % // whd in ⊢ (??%?); >FIND1' in ⊢ (??%?); >FIND2' in ⊢ (??%?); @refl | skip ]
510    ]
511  | * #sA' #kA' whd in ⊢ (% → %);
512    * #u1' * #cs * #k1' * #FA' #K'
513         % [2: %{cs} %{k1'} % [ whd in ⊢ (??%?); >FA' in ⊢ (??%?); @refl | // ] |skip]
514  ]
515| #e #s1 #s2 #IH1 #IH2 #k #k' #u @blindly_label #u1 #u2 #u3 #c2 #c3 #K
516  whd in match (find_label ?? k); whd in match (find_label ?? k');
517  whd in match (find_label ?? k');
518  @(lfl_IH  … IH1) [ // ] cases (find_label ???)
519  [ whd in ⊢ (% → match % with [_⇒?|_⇒?]); #FIND1'
520    lapply (IH2 k k' u3 K) cases (find_label ???)
521    [ whd in ⊢ (% → %); #FIND2'
522      whd in match (find_label ???); >FIND1'
523      whd in match (find_label ???); >FIND2' @refl
524    | * #s2' #k2' * #u4 * #cs * #k1' * #FIND2' #K2'
525      % [2: % [2: % [2: % [ whd in ⊢ (??%?);
526      whd in match (find_label ???); >FIND1' in ⊢ (??%?);
527      whd in match (find_label ???); >FIND2' in ⊢ (??%?); @refl
528      | // ]|skip]|skip]|skip]
529    ]
530  | * #s1' #k1 whd in ⊢ (% → %); * #u4 * #cs * #k1' * #FIND1' #K1'
531    % [2: % [2: % [2: % [
532      whd in ⊢ (??%?); whd in match (find_label ???); >FIND1' in ⊢ (??%?);
533      @refl | // ] |skip ]| skip ]| skip ]
534  ]
535| #e #s0 #cl #IH #k #k' #u #K @blindly_label #u1 #u2 #cs #cpost #CL
536  whd in match (find_label ?? k); normalize in match (find_label ?? k');
537  @(lfl_IH s0 … IH) [ /2/ ]
538  cases (find_label ???)
539  [ whd in ⊢ (% → %); #FIND1'
540    whd in ⊢ (??%?); whd in match (find_label ???); >FIND1' @refl
541  | * #s1 #k1 * #u4 * #cs * #k1' * #FIND1' #K1'
542    % [2: % [2: % [2: % [
543      whd in ⊢ (??%?); whd in match (find_label ???); >FIND1' in ⊢ (??%?);
544      @refl | // ]| skip ]| skip ]| skip ]
545  ]
546| #e #s0 #IH #k #k' #u #K @blindly_label #u1 #u2 #cs #cpost
547  whd in match (find_label ?? k); normalize in match (find_label ?? k');
548  @(lfl_IH s0 … IH) [ /2/ ]
549  cases (find_label ???)
550  [ whd in ⊢ (% → %); #FIND1'
551    whd in ⊢ (??%?); whd in match (find_label ???); >FIND1' @refl
552  | * #s1 #k1 * #u4 * #cs * #k1' * #FIND1' #K1'
553    % [2: % [2: % [2: % [
554      whd in ⊢ (??%?); whd in match (find_label ???); >FIND1' in ⊢ (??%?);
555      @refl | // ]| skip ]| skip ]| skip ]
556  ]
557| #s1 #e #s2 #s3 #IH1 #IH2 #IH3 #k #k' #u #K @blindly_label #u1 #u2 #u3 #u4 #c3 #c4
558  whd in match (find_label ???); normalize in match (find_label ?? k');
559  @(lfl_IH s1 … IH1) [ /2/ ]
560  cases (find_label ???)
561  [ whd in ⊢ (% → match % with [_⇒?|_⇒?]); #FIND1' >FIND1'
562    @(lfl_IH s3 … IH3) [ /2/ ]
563    cases (find_label ???)
564    [ whd in ⊢ (% → match % with [_⇒?|_⇒?]); #FIND3' >FIND3'
565      @(lfl_IH s2 … IH2) [ /2/ ]
566      cases (find_label ???)
567      [ whd in ⊢ (% → %); #FIND2' >FIND2' @refl
568      | * #s2' #k2' * #u2' * #cs' * #k1' * #FIND2' #K2'
569        % [2: % [2: % [2: % [
570         whd in ⊢ (??%?); >FIND2' in ⊢ (??%?); @refl
571        | // ]| skip ]| skip ]| skip ]
572      ]
573    | * #s3' #k3' * #u3' * #cs' * #k1' * #FIND3' #K3'
574        % [2: % [2: % [2: % [
575        >FIND3' in ⊢ (??%?); whd in ⊢ (??%?); @refl
576        | // ]| skip ]| skip ]| skip ]
577    ]
578  | * #s1' #k1' * #u1' * #cs' * #k1' * #FIND1' #K1'
579        % [2: % [2: % [2: % [
580        >FIND1' in ⊢ (??%?); whd in ⊢ (??%?); @refl
581        | // ]| skip ]| skip ]| skip ]
582  ]
583| //
584| //
585| #eo #k #k' #u @blindly_label #u1 //
586| #e #ls #IH #k #k' #u #K @blindly_label #u1 #u2
587  normalize in match (find_label ???); normalize in match (find_label ???);
588  lapply (IH (Kswitch k) (Kswitch k') u2 ?) [/2/] cases (find_label_ls ???)
589  [ whd in ⊢ (% → %); //
590  | * #s1' #k1' * #u' * #cs * #k'' * #FIND' #K'
591    % [2: % [2: % [2: % [ @FIND' | // ]|skip ]|skip]|skip]
592  ]
593| #l #s0 #IH #k #k' #u #K @blindly_label #u1 #cs
594  whd in match (find_label ???); whd in match (find_label ?? k');
595  cases (ident_eq lbl l)
596  [ #E destruct whd
597    % [2: % [2: % [2: % [ @refl | // ]|skip ]|skip ]| skip ]
598  | #NE whd in ⊢ (match % with [_⇒?|_⇒?]);
599    normalize in match (find_label ?? k');
600    @(lfl_IH s0 … IH) [ // ]
601    cases (find_label ???)
602    [ //
603    | * #s0' #k0' * #u' * #cs0 * #k1' * #FIND0 #K0
604      % [2: % [2: % [2: % [ @FIND0 | // ]|skip ]|skip]|skip]
605    ]
606  ]
607| //
608| #l #s0 #IH #k #k' #u #K @blindly_label #u1 /2/
609| #s0 #IH #k #k' #u whd in match (label_lstatements ??);
610  @label_gen_elim #u1 >shift_fst >shift_fst
611  whd in match (find_label_ls ???); whd in match (find_label_ls ???);
612  @IH
613| #sz #i #s0 #tl #IH1 #IH2 #k #k' #u #K
614  whd in match (label_lstatements ??); @label_gen_elim #u1 @label_gen_elim #u2
615  @label_gen_elim #u3 >shift_fst
616  whd in match (find_label_ls ???); normalize in match (find_label_ls ?? k');
617  @(lfl_IH s0 … IH1) [ /2/ ]
618  cases (find_label ???)
619  [ whd in ⊢ (% → match % with [_⇒?|_⇒?]); #FIND0 >FIND0
620    lapply (IH2 k k' u2 K) cases (find_label_ls ???)
621    [ whd in ⊢ (% → %); #FINDtl >FINDtl @refl
622    | * #stl #ktl //
623    ]
624  | * #s0' #k0' whd in ⊢ (% → %);
625    * #u' * #cs * #k1' * #FIND0 #K0 >FIND0
626    % [2: % [2: % [2: % [ @refl | // ] | skip ] | skip ] | skip ]
627  ]
628] qed.
629
630lemma label_find_label_fn : ∀g,lbl,f,k,k',s1,k1.
631  cont_with_labels k k' →
632  find_label lbl (fn_body f) (call_cont k) = Some ? 〈s1,k1〉 →
633  ∃u',cs,k1'.
634    find_label lbl (fn_body (\fst (label_function g f))) (call_cont k') = Some ? 〈Scost cs (\fst (label_statement s1 u')), k1'〉 ∧
635    cont_with_labels k1 k1'.
636#g #lbl * #rty #args #vars #s #k #k' #s1 #k1 #K #FIND
637whd in match (label_function ??);
638@label_gen_elim #u1 @label_gen_elim #u2 >shift_fst
639lapply (label_find_label lbl s (call_cont k) (call_cont k') g ?)
640[ /2/ ]
641>FIND whd in ⊢ (% → ?); //
642qed.
643
644
645(* We show the main simulation in two stages.  First, we show it for all states
646   in the relation *except* those for labeled_statements, then we'll show the
647   whole thing.  This is so that we can appeal to the other cases in the proof
648   for labeled_statements. *)
649lemma step_with_labels_partial : ∀ge,ge'.
650  related_globals_gen … label_fundef ge ge' →
651  ∀s1,s1',tr,s2.
652  state_with_labels_partial s1 s1' →
653  exec_step ge s1 = Value … 〈tr,s2〉 →
654  ∃n. after_n_steps (S n) … clight_exec ge' s1'
655  (λtr',s2'.
656     trace_with_extra_labels tr tr' ∧
657     state_with_labels s2 s2').
658
659(* General plan is like the expressions result, except that we do case analysis
660   on the simulation first, then:  break up the original execution, break up the
661   cost labelling, use the earlier results to deal with expressions, then
662   run the labelled version for enough steps.  We try to avoid having to write
663   out the final trace and state and "skip" them afterwards. *)
664#ge #ge' #RG #Xs1 #Xs1' #tr #s2 *
665[ #g #f #us #s #k #k' #e #m #KL cases s
666  [ #EX inversion KL
667    [ #E1 #E2 #_ destruct
668      whd in EX:(??%?);
669      lapply (refl ? (fn_return f)) cases (fn_return f) in ⊢ (???% → ?);
670      [ #E >E in EX; whd in ⊢ (??%% → ?); #EX' destruct
671        %{0} whd whd in ⊢ (??%?);
672        >label_function_return >E whd % /3/
673      | *: #A [ 1,4,5,6,7: #B ] #E >E in EX; #EX whd in EX:(??%%); destruct
674      ]
675    | #u #s0 #k0 #k0' #K #_ #E1 #E2 #E3 destruct %{0} whd
676      whd in EX:(??%%); destruct /4/
677    | #ue #e0 #us0 #s0 #cl #cs #cpost #k0 #k0' #K #CL #_ #E1 #E2 #E3 destruct %{0}
678      whd in EX:(??%%); destruct whd /4/
679    | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct
680      cases (bindIO_inversion ??????? EX) -EX * #ve #tre * #EXe #EX
681      cases (bindIO_inversion ??????? EX) -EX * * #EXb #EX
682      normalize in EX; destruct
683      cases ((proj1 ?? (label_expr_ok ge ge' e m RG)) ??? EXe ue) #tre' * #EXe' #Te
684      [ %{0} whd
685        whd in ⊢ (??%?); >EXe'
686        whd in ⊢ (??%?); >label_expr_type >EXb
687        whd % /4/
688      | %{2} whd
689        whd in ⊢ (??%?); >EXe'
690        whd in ⊢ (??%?); >label_expr_type >EXb
691        whd % [ <(E0_right tr) @twel_app /2/ | /4/ ]
692      ]
693    | #ue #e0 #us1 #st1 #us2 #st2 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct
694      whd in EX:(??%?); destruct
695      %{0} whd /4/
696    | #ue #e0 #us1 #st1 #us2 #st2 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct
697      whd in EX:(??%?); destruct
698      %{0} % /4/
699    | #ue #e0 #us1 #st1 #us2 #st2 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct
700      whd in EX:(??%?); destruct
701      %{0} % /4/
702    | #k0 #k0' #K #_ #E1 #E2 #E3 destruct
703      whd in EX:(??%?); destruct
704      %{0} % /4/
705    | #u0 #r #f0 #en #k0 #k0' #K #_ #E1 #E2 #E3 destruct
706      whd in EX:(??%?);
707      lapply (refl ? (fn_return f)) cases (fn_return f) in ⊢ (???% → ?);
708      [ #E >E in EX; whd in ⊢ (??%? → ?); #EX destruct
709        %{0} whd whd in ⊢ (??%?); >label_function_return >E in ⊢ (??%?);
710        whd % /4/
711      | *: #A [ 1,4,5,6,7: #B ] #E >E in EX; #EX whd in EX:(??%%); destruct
712      ]
713    | #ls #u #k0 #k0' #K #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
714      %{0} % /4/
715    ]
716  | * #a1 #ty1 #a2 #EX
717    cases (bindIO_inversion ??????? EX) -EX * * #b1 #o1 #tr1 * #EX1 #EX
718    cases (bindIO_inversion ??????? EX) -EX * #v2 #tr2 * #EX2 #EX
719    cases (bindIO_inversion ??????? EX) -EX #m3 * #EX3 #EX
720    whd in EX:(??%%); destruct
721    @blindly_label #u1 #u2
722    cases (proj2 ?? (label_expr_ok ge ge' e m RG) ????? EX1 u1) #tr1' * #EX1' #T1
723    cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX2 u2) #tr2' * #EX2' #T2
724    %{0} whd
725    whd in ⊢ (??%?); >exec_lvalue_labelled >EX1'
726    whd in ⊢ (??%?); >EX2'
727    whd in ⊢ (??%?); >label_expr_type >EX3
728    whd % [ whd in ⊢ (??%); @twel_app // | /3/ ]
729  | * [2: * #er #tyr ] #ef #args #EX
730    cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
731    cases (bindIO_inversion ??????? EX) -EX * #args' #tr2 * #EX2 #EX
732    cases (bindIO_inversion ??????? EX) -EX #fd * #EX3 #EX
733    cases (bindIO_inversion ??????? EX) -EX #E4 * #EX4 #EX
734    whd in EX:(??%%);
735    [ cases (bindIO_inversion ??????? EX) -EX * * #b5 #o5 #tr5 * #EX5 #EX whd in EX:(??%%); ]
736    destruct
737    @blindly_label #u1 #u2 #u3
738    cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 u2) #tr1' * #EX1' #T1
739    cases (label_exprs_ok ge ge' RG e m args args' ? EX2 u3) #tr2' * #EX2' #T2
740    [ cases (proj2 ?? (label_expr_ok ge ge' e m RG) ????? EX5 u1) #tr5' * #EX5' #T5 ]
741    cases (opt_find_funct … RG … EX3) #ux #EFF
742    %{0} whd
743    whd in ⊢ (??%?); >EX1'
744    whd in ⊢ (??%?); >EX2'
745    whd in ⊢ (??%?); >EFF
746    whd in ⊢ (??%?); >label_fundef_typeof_fundef >label_expr_fun_typeof >EX4
747    whd in ⊢ (??%?); [ whd in match (label_opt_expr ??); @breakup_pair whd in ⊢ (??%?); >exec_lvalue_labelled >EX5' ]
748    whd % [ 1,3: whd in ⊢ (??%); @twel_app /2/ | *: @swl_partial @swl_callstate /2/ ]
749  | #st1 #st2 #EX
750    whd in EX:(??%%); destruct
751    whd in match (label_statement ??); @label_gen_elim #u1 @label_gen_elim #u2
752    %{0} % /4/
753  | #a #st1 #st2 #EX
754    cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
755    cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX
756    normalize in EX; destruct
757    whd in match (label_statement ??); @label_gen_elim #u1
758    @label_gen_elim #u2 @label_gen_elim #u3 @label_gen_elim #u4
759    @label_gen_elim #u5
760    whd in match (add_cost_before ??); cases (fresh ??) #c6 #u6
761    whd in match (add_cost_before ??); cases (fresh ??) #c7 #u7
762    cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1
763    %{1} whd
764    whd in ⊢ (??%?); >EX1'
765    whd in ⊢ (??%?); >label_expr_type >EX2
766    whd in ⊢ (??%?); % [1,3: <(E0_right tr) ] /4/
767  | #a #st #cl #EX
768    cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
769    cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX
770    normalize in EX; destruct
771    @blindly_label #u1 #u2 #cs #cpost * #CL destruct
772    cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 u1) #tr1' * #EX1' #T1
773    [ 1,2,3: %{1} | %{0} ] whd
774    whd in ⊢ (??%?); >EX1'
775    whd in ⊢ (??%?); >label_expr_type >EX2
776    whd in ⊢ (??%?); whd % [ 1,3,5,7: <(E0_right tr) ] /5 by twel_new, swl_partial, swl_state, cwl_while, twel_app, or_introl, or_intror/
777  | #a #st #EX
778    normalize in EX; destruct
779    whd in match (label_statement ??); @label_gen_elim #u1
780    @label_gen_elim #u2
781    whd in match (add_cost_before ??); cases (fresh ??) #c6 #u6 >shift_fst
782    whd in match (add_cost_after ??); cases (fresh ??) #c7 #u7 >shift_fst
783    %{2} % /4/
784  | #st1 #a #st2 #st #EX
785    lapply (refl ? (is_Sskip st1)) cases (is_Sskip st1) in ⊢ (???% → ?); #Esk #Eskip
786    whd in EX:(??%?); >Eskip in EX; #EX
787    whd in match (label_statement ??); @label_gen_elim #u1
788    @label_gen_elim #u2 @label_gen_elim #u3 @label_gen_elim #u4
789    whd in match (add_cost_before ??); cases (fresh ??) #c5 #u5 >shift_fst
790    whd in match (add_cost_after ??); cases (fresh ??) #c6 #u6 >shift_fst
791    [ cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
792      cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX
793      normalize in EX; destruct
794      cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1
795      [ %{2} | %{3} ] whd
796      whd in ⊢ (??%?); >EX1'
797      whd in ⊢ (??%?); >label_expr_type >EX2
798      whd in ⊢ (??%?); % [ 1,3: <(E0_right tr) ] /4/
799    | whd in EX:(??%%); destruct
800      %{1} whd
801      whd in ⊢ (??%?); cases (labelled_is_not_skip ? u1 Esk) #Esk' #Eskip'
802      >Eskip' whd in ⊢ (??%?); % /4/
803    ]
804  | #EX inversion KL
805    [ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
806    |#u #s0 #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
807    | #ue #e0 #us0 #s0 #cl #cs #cpost #k0 #k0' #K' * #CL #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
808    | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
809    | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
810    | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
811    | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
812    | #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
813    | #ux #r #f0 #en #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
814    | #ls #u #k0 #k0' #K #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
815    ]
816    whd in match (label_statement ??);
817    [ 1,3,7,8: %{0} % /3/
818    | 2,5: %{1} whd % /3/
819    | 4,6: %{2} whd % /3/
820    ]
821  | #EX inversion KL
822    [ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
823    |#u #s0 #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
824    | #ue #e0 #us0 #s0 #cl #cs #cpost #k0 #k0' #K' * #CL #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
825    | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
826    | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
827    | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
828    | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
829    | #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
830    | #g #r #f0 #en #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
831    | #ls #u #k0 #k0' #K #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
832    ]
833    whd in match (label_statement ??);
834    [ 1,2,3,6,7,8: %{0} % /4/
835    | 5: %{1} % /4/
836    | cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
837      cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX
838      normalize in EX; destruct
839      cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 ue) #tr1' * #EX1' #T1
840      [ %{0} | %{2} ] whd
841      whd in ⊢ (??%?); >EX1'
842      whd in ⊢ (??%?); >label_expr_type >EX2
843      whd in ⊢ (??%?); % [ 3: <(E0_right tr) ] /3/
844    ]
845  | * [2: #a ] #EX
846    whd in EX:(??%?); cases (type_eq_dec (fn_return f) Tvoid) in EX;
847    #Ety #EX whd in EX:(??%?);
848    [ destruct
849    | cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
850      cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1
851    | >Ety in EX; #EX
852    | @⊥ cases (fn_return f) in Ety EX;
853      [ * #H cases (H (refl ??))
854      | *: normalize #a #b #c try #d try #e destruct
855      ]
856    ]
857    whd in match (label_statement ??);
858    [ @label_gen_elim #u' whd in match (label_opt_expr ??); @label_gen_elim #u'' ]
859    whd in EX:(??%%); destruct
860    %{0} whd
861    whd in ⊢ (??%?);
862    [ >label_function_return @(dec_false ? (type_eq_dec ??) Ety) #Ety''
863      whd in ⊢ (??%?); >EX1'
864    | >label_function_return >Ety
865    ] whd in ⊢ (??%?); % /4/
866  | #a #ls #EX
867    cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
868    cases v1 in EX1 EX;
869    [ 2: #sz #i #EX1 #EX
870    | *: normalize #A #B try #C destruct
871    ]
872    whd in EX:(??%%); destruct
873    cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1
874    whd in match (label_statement ??); @label_gen_elim #u1 @label_gen_elim #u2
875    %{0} whd
876    whd in ⊢ (??%?); >EX1' % //
877    cases (label_select_ls … sz i ls u1) #u3 #Els >Els /3/
878  | #l #st #EX
879    whd in EX:(??%?); destruct
880    whd in match (label_statement ??); @label_gen_elim #u1 >shift_fst
881    whd in match (add_cost_before ??); cases (fresh ??) #cs #u2 >shift_fst
882    %{1} % /3/
883  | #l #EX
884    whd in EX:(??%?);
885    @blindly_label whd
886    lapply (refl ? (find_label l (fn_body f) (call_cont k)))
887    cases (find_label ???) in ⊢ (???% → ?);
888    [ #F @⊥  >F in EX; #EX whd in EX:(??%?); destruct
889    | * #s1 #k1 #F >F in EX; #EX whd in EX:(??%?); destruct
890      cases (label_find_label_fn g … KL F)
891      #u' * #cs * #k1' * #F' #K'
892      %{1} whd
893      whd in ⊢ (??%?); >F'
894      % /3/
895    ]
896  | #c #st #EX whd in EX:(??%?); destruct @blindly_label #u1
897    %{0} % /3/
898  ]
899| #u0 #f #ua #a #us #s #cl #cs #cpost #k #k' #e #m #K * #CL #EX
900  cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
901  cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX
902  whd in EX:(??%%); destruct
903  cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 ua) #tr1' * #EX1' #T1
904  [ 4: %{0} | 1,2,3: %{1} ] whd
905  whd in ⊢ (??%?); >EX1'
906  whd in ⊢ (??%?); >label_expr_type >EX2
907  whd % [ 1,3,5,7: <(E0_right tr) ] /5/
908| #u0 #f #ua #a #us #s #cs #cpost #k #k' #e #m #K #EX
909  whd in EX:(??%%); destruct
910  %{1} % /4/
911| #u0 #f #ua2 #a2 #us3 #s3 #us #s #cs #cpost #k #k' #e #m #K #EX
912  cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
913  cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX
914  whd in EX:(??%%); destruct
915  cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 ua2) #tr1' * #EX1' #T1
916  [ %{1} | %{2} ] whd
917  whd in ⊢ (??%?); >EX1'
918  whd in ⊢ (??%?); >label_expr_type >EX2
919  % [1,3: <(E0_right tr) ] /4/
920| #u0 *
921  [ #f #args #k #k' #m #K whd in ⊢ (??%? → ?); @pair_elim #e #m1 #EX1 #EX
922    cases (bindIO_inversion ??????? EX) -EX #m2 * #EX2 #EX
923    whd in EX:(??%%); destruct
924    whd in match (label_fundef ??);
925    whd in match (label_function ??);
926    lapply (refl ? (\fst (label_function u0 f))) whd in ⊢ (???(???%) → ?);
927    @label_gen_elim #u1 @label_gen_elim #u2 >shift_fst #Ef
928    %{1} whd
929    whd in ⊢ (??%?); >EX1
930    whd in ⊢ (??%?); >EX2
931    % /4/
932  | #id #tys #ty #args #k #k' #m #K #EX
933    cases (bindIO_inversion ??????? EX) -EX #vs * #EX1 #EX
934    cases (bindIO_inversion ??????? EX) -EX #ety * #EX2 #EX
935    whd in EX2:(??%%); destruct
936  ]
937| #res #k #k' #m #K #EX inversion K
938  [ #E1 #E2 #E3 destruct cases res in EX ⊢ %;
939    [ 2: * #i #EX whd in EX:(??%?); destruct
940    | *: normalize #A try #B try #C destruct
941    ]
942    %{0} % /2/
943  | 9: #u0 #r #f #en #k0 #k0' #K' #_ #E1 #E2 #E3 destruct cases r in EX ⊢ %;
944    [ #EX whd in EX:(??%?); destruct
945      %{0} % /3/
946    | * * #b #o #ty #EX
947      cases (bindIO_inversion ??????? EX) -EX #m2 * #EX1 #EX
948      whd in EX:(??%%); destruct
949      %{0} whd whd in ⊢ (??%?); >EX1 % /3/
950    ]
951  | *: #A #B #C #D #E #F #G try #H try #I try #J try #L try #M try #N try #O
952       destruct whd in EX:(??%?); destruct
953  ]
954| #r #EX whd in EX:(??%%); destruct
955] qed.
956
957theorem step_with_labels : ∀ge,ge'.
958  related_globals_gen … label_fundef ge ge' →
959  ∀s1,s1',tr,s2.
960  state_with_labels s1 s1' →
961  exec_step ge s1 = Value … 〈tr,s2〉 →
962   ∃n. after_n_steps (S n) … clight_exec ge' s1'
963   (λtr',s2'. trace_with_extra_labels tr tr' ∧
964              state_with_labels s2 s2').
965#ge #ge' #RG #Xs1 #Xs1' #tr #s2 *
966[ #s1 #s1' @step_with_labels_partial //
967| #u0 #f #u *
968(* If we have LSdefault we need to smuggle the execution of the cost label in
969   before the actual statement. *)
970  [ #s #k #k' #e #m #K #EX
971    whd in EX:(??(??(??%???))?);
972    whd in match (label_lstatements ??); @label_gen_elim #u1 @label_gen_elim #u2
973    >shift_fst whd in match (seq_of_labeled_statement ?);
974    cases (step_with_labels_partial … RG (State f s k e m) (State (\fst (label_function u0 f)) (\fst (label_statement s u)) k' e m) tr s2 (swl_state … K) EX)
975    #n #H %{(S n)} @(after_n_m 1 (S n) … H) % /2/
976    #trx #sx * /3/
977(* but for LScase it's just like the cases in step_with_labels_partial *)
978  | #sz #i #s #ls #k #k' #e #m #K #EX
979    whd in EX:(??(??(??%???))?);
980    whd in match (label_lstatements ??); @label_gen_elim #u1 @label_gen_elim #u2
981    @label_gen_elim #u3 >shift_fst whd in match (seq_of_labeled_statement ?);
982    whd in EX:(??%?); destruct
983    %{1} % /4/
984  ]   
985] qed.
986
987
988lemma exec_step_interaction:
989  ∀ge,s,o,k. exec_step ge s = Interact … o k  →
990  ∃f,argtys,retty,vargs,k',m. s = Callstate (CL_External f argtys retty) vargs k' m.
991#ge #s cases s
992[ #f #st #kk #e #m #o #k #EX @⊥ cases st in EX ⊢ %;
993  [ 11,14: #a | 2,4,7,12,13,15: #a #b | 3,5,6: #a #b #c | 8: #a #b #c #d ]
994  whd in ⊢ (??%? → ?);
995  [ 4,5,7,8: #EX destruct ]
996  [ cases a
997    [ whd in ⊢ (??%? → ?); cases (fn_return f) normalize #A try #B try #C try #D destruct
998    | #a' whd nodelta in ⊢ (??%? → ?); cases (type_eq_dec (fn_return f) Tvoid)
999      #x whd in ⊢ (??%? → ?); [2: cases (exec_expr ????) #y ] #EX whd in EX:(??%?); destruct
1000    ]
1001  | cases (find_label a (fn_body f) (call_cont kk)) [ 2: * #x #y ] #EX whd in EX:(??%?); destruct
1002  | @bindIO_res_interact #l #El @bindIO_res_interact #vt #Evt @bindIO_opt_interact #m' #Em #EX whd in EX:(??%?); destruct
1003  | @bindIO_res_interact * * normalize #A #B #C try #D try #E destruct
1004  | @bindIO_res_interact #x1 #x2 @bindIO_res_interact #x3 #x4 @bindIO_opt_interact #x5 #x6 @bindIO_res_interact #x7 #x8 cases a
1005      [ 2: #x9 @bindIO_res_interact #x10 #x11 ] #EX whd in EX:(??%?); destruct
1006  | 6,7: @bindIO_res_interact #x1 #x2 @bindIO_res_interact #x3 #x4 #EX whd in EX:(??%?); destruct
1007  | cases (is_Sskip a) #H [ @bindIO_res_interact #vt #Evt @bindIO_res_interact #v #Ev ] #EX whd in EX:(??%?); destruct
1008  | cases kk [ 1,8: cases (fn_return f) normalize #A try #B try #C try #D try #E try #F try #G try #H destruct
1009    | 2,3,5,6,7: normalize #A #B try #C try #D try #E destruct
1010    | #z1 #z2 #z3 @bindIO_res_interact #x1 #x2 @bindIO_res_interact #x3 #x4 cases x3 #EX whd in EX:(??%?); destruct ]
1011  | cases kk normalize #A try #B try #C try #D try #E destruct
1012  | cases kk [ 4: #z1 #z2 #z3 @bindIO_res_interact #x1 #x2 @bindIO_res_interact #x3 #x4 cases x3 #EX whd in EX:(??%?); destruct
1013    | *: normalize #A try #B try #C try #D try #E destruct
1014    ]
1015  ]
1016| #f #args #kk #m #o #k cases f
1017  [ #f' whd in ⊢ (??%? → ?); cases (exec_alloc_variables empty_env m (fn_params f'@fn_vars f'))
1018    #x1 #x2 @bindIO_res_interact #m #Em #EX whd in EX:(??%?); destruct
1019  (* This is the only case that actually matters! *)
1020  | #fn #argtys #rty whd in ⊢ (??%? → ?);
1021    @bindIO_res_interact #vs #Evs
1022    #EX whd in EX:(??%?); destruct
1023    %{fn} %{argtys} %{rty} %{args} %{kk} %{m} %
1024  ]
1025| #v #kk #m #o #k whd in ⊢ (??%? → ?); cases kk
1026    [ cases v [2: * ] normalize #A try #B destruct
1027    | 8: #x1 #x2 #x3 #x4 cases x1
1028      [ whd in ⊢ (??%? → ?); #EX destruct | #x5 whd in ⊢ (??%? → ?); cases x5
1029          #x6 #x7 @bindIO_opt_interact #m' #Em #EX whd in EX:(??%?); destruct ]
1030    | *: normalize #A try #B try #C try #D try #E destruct ]
1031| #r #o #k #EX whd in EX:(??%?); destruct
1032] qed.
1033
1034lemma state_with_labels_call : ∀f,a,k,m,s1.
1035 state_with_labels (Callstate f a k m) s1 →
1036 ∃k'. cont_with_labels k k' ∧ ∃u0. s1 = Callstate (\fst (label_fundef u0 f)) a k' m.
1037#f #a #k #m #s1 #S inversion S
1038[ #s #s' #S' #E1 #E2 #E3 destruct inversion S'
1039  [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 destruct
1040  | #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 destruct
1041  | #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 destruct
1042  | #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 #H60 #H61 destruct
1043  | #u0 #f' #a' #k' #k'' #m' #K #E1 #E2 #E3 destruct %{k''} % /2/
1044  | #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 destruct
1045  | #H72 #H73 #H74 #H75 destruct
1046  ]
1047| #H77 #H78 #H79 #H80 #H81 #H82 #H83 #H84 #H85 #H86 #H87 destruct
1048] qed.
1049
1050lemma interactive_step_with_labels : ∀ge,ge'.
1051  related_globals_gen … label_fundef ge ge' →
1052  ∀s1,s1',o,k.
1053  exec_step ge s1 = Interact … o k →
1054  state_with_labels s1 s1' →
1055  ∃k'.
1056      exec_step ge' s1' = Interact … o k' ∧
1057  ∀i. ∃tr,s2.
1058    k i = Value … 〈tr,s2〉 ∧
1059    ∃tr',s2'.
1060      k' i = Value … 〈tr',s2'〉 ∧
1061      trace_with_extra_labels tr tr' ∧
1062      state_with_labels s2 s2'.
1063#ge #ge' #RG #s1 #s1' #o #k #EX
1064cases (exec_step_interaction … EX)
1065#fn * #argtys * #retty * #vargs * #k' * #m #E
1066destruct
1067#S cases (state_with_labels_call … S)
1068#k'' * #K * #u0 #E2 destruct
1069whd in EX:(??%?);
1070@(bindIO_res_interact ?????????? EX) -EX
1071#vs #CHECK #EX whd in EX:(??%?); destruct
1072% [2: %
1073[ whd in ⊢ (??%?);
1074  >CHECK in ⊢ (??%?);
1075  whd in ⊢ (??%?);
1076  @refl
1077| #i
1078  % [2: % [2: %
1079  [ @refl
1080  | % [2: % [ 2: % [ %
1081    [ @refl
1082    | // ]
1083    | /3/ ]
1084    | skip ]| skip ]
1085  ]| skip ]| skip ]
1086]| skip
1087] qed.
1088
1089
1090lemma initial_state_in_simulation : ∀p,s.
1091  make_initial_state p = OK ? s →
1092  ∃s'. make_initial_state (\fst (clight_label p)) = OK ? s' ∧ state_with_labels s s'.
1093* #vars #fns #main #s
1094whd in ⊢ (??%? → ?); letin ge ≝ (make_global ?) #EX
1095cases (bind_inversion ????? EX) -EX #m * #Em #EX
1096cases (bind_inversion ????? EX) -EX #b * #Emain #EX
1097cases (bind_inversion ????? EX) -EX #fd * #Emain' #EX
1098whd in EX:(??%%); destruct
1099whd in match (make_initial_state ?);
1100letin ge' ≝ (make_global ?)
1101cut (related_globals_gen … label_fundef ge ge')
1102[ // ] #RG
1103cases (rgg_find_funct_ptr … RG … Emain') #u' #FFP
1104% [2: %
1105[ whd in ⊢ (??%?);
1106  change with (transform_program ??? (mk_program …) (λ_.label_fundef)) in match (mk_program ??? (transf_program ????) ?);
1107  >(init_mem_transf_gen … (mk_program ?? vars fns main)) >Em in ⊢ (??%?);
1108  whd in ⊢ (??%?); <(rgg_find_symbol … RG) >Emain in ⊢ (??%?);
1109  whd in ⊢ (??%?); >FFP in ⊢ (??%?);
1110  whd in ⊢ (??%?); @refl
1111| /3/
1112] | skip ]
1113qed.
1114 
1115
1116
1117
1118lemma final_related : ∀s1,s2.
1119  state_with_labels s1 s2 →
1120  is_final s1 = is_final s2.
1121#s1x #s2x *
1122[ #s1y #s2y * //
1123| //
1124] qed.
1125
1126let corec build_exec
1127  (ge1,ge2:genv)
1128  (RG:related_globals_gen … label_fundef ge1 ge2)
1129  (s1,s2:state)
1130  (S:state_with_labels s1 s2)
1131  (NW:not_wrong state (exec_inf_aux … clight_fullexec ge1 (exec_step ge1 s1)))
1132: sim_with_labels (exec_inf_aux … clight_fullexec ge1 (exec_step ge1 s1)) (exec_inf_aux … clight_fullexec ge2 (exec_step ge2 s2)) ≝
1133match NW return λe,NW. exec_inf_aux … clight_fullexec ?? = e → sim_with_labels e ? with
1134[ nw_stop tr i s ⇒ ?
1135| nw_step tr1 s1' e1 NW1 ⇒ ?
1136| nw_interact o k NWk ⇒ ?
1137] (refl ? (exec_inf_aux … clight_fullexec ge1 (exec_step ge1 s1))).
1138[ #E1
1139  cases (exec_inf_stops_at_final ?? clight_fullexec … E1)
1140  #EX1 #F1
1141  cases (step_with_labels … RG … S EX1)
1142  #n #A cases (after_inv clight_fullexec ???? A) #tr' * #s' * * #TWL #S'
1143  lapply F1 whd in ⊢ (??%? → ?); >(final_related … S') #F2
1144  whd in match (is_final … s'); >F2 *
1145  #tr2' #S2
1146  @(swl_stop … S2 TWL)
1147| #E1
1148  cases (extract_step ?? clight_fullexec … E1)
1149  #EX1 #E1'
1150  cases (step_with_labels … RG … S EX1)
1151  #n #AF cases (after_inv clight_fullexec ???? AF) #tr' * #s' * * #TWL #S'
1152  whd in match (is_final … s'); lapply (refl ? (is_final s'))
1153  cases (is_final s') in ⊢ (???% → %);
1154  [ #NF #H whd in H; @(swl_steps … H) //
1155    @(match sym_eq … E1' return λe,E1'. sim_with_labels e ? with [refl ⇒ ?])
1156    @build_exec // >E1' in NW1; //
1157  | #r <(final_related … S') change with (is_final … clight_fullexec ge1 s1') in ⊢ (??%? → ?);
1158    >(exec_e_step_not_final ?? clight_fullexec … E1) #E destruct
1159  ]
1160| #E1
1161  cases (extract_interact ?? clight_fullexec … E1)
1162  #k' * #EX1 #Ek lapply NWk -NWk @(match sym_eq … Ek with [refl ⇒ ?]) #NWk
1163  cases (interactive_step_with_labels … RG … EX1 S)
1164  #k2' * #EX2 #H2 @(match sym_eq … EX2 with [refl ⇒ ?]) @(match sym_eq … (exec_inf_aux_unfold …) with [refl ⇒ ?]) (* XXX why is this necessary? *) whd in ⊢ (??%);
1165  @swl_interact
1166  #i cases (H2 i) #tr1 * #s1' * #K1 * #tr2 * #s2' * * #K2 #TR #S'
1167  lapply (NWk i)
1168  @(match sym_eq … K1 with [refl ⇒ ?]) @(match sym_eq … (exec_inf_aux_unfold …) with [refl ⇒ ?]) whd in ⊢ (??% → ?%%); whd in match (is_final ?????); @(match sym_eq … (final_related … S') with [refl ⇒ ?])
1169  @(match sym_eq … K2 with [refl ⇒ ?]) @(match sym_eq … (exec_inf_aux_unfold ?? clight_fullexec ge2 …) with [refl ⇒ ?]) whd in ⊢ (? → ??%); whd in match (is_final ?????);
1170  cases (is_final s2')
1171  [ whd in ⊢ (??% → ?%%); #NW' @(swl_steps … (steps_step …)) // @build_exec //
1172    inversion NW'
1173    [ #H1 #H2 #H3 #H4 #H5 destruct
1174    | #H7 #H8 #H9 #H10 #H11 #H12 destruct //
1175    | #H14 #H15 #H16 #H17 #H18 destruct
1176    ]
1177  | #r whd in ⊢ (??% → ?%%); #NW' @(swl_stop … (steps_stop …)) //
1178  ]
1179] qed.
1180
1181lemma initial_state_is_not_final : ∀p,s.
1182  make_initial_state p = OK ? s →
1183  is_final s = None ?.
1184* #vars #fns #main #s
1185whd in ⊢ (??%? → ?); letin ge ≝ (make_global ?) #EX
1186cases (bind_inversion ????? EX) -EX #m * #Em #EX
1187cases (bind_inversion ????? EX) -EX #b * #Emain #EX
1188cases (bind_inversion ????? EX) -EX #fd * #Emain' #EX
1189whd in EX:(??%%); destruct //
1190qed.
1191
1192
1193theorem labelling_sim : labelled_exec_is_equiv.
1194whd (* let's remind ourselves of the spec *)
1195#p
1196#NW
1197cases (not_wrong_init clight_fullexec p NW)
1198whd in ⊢ (% → ??%? → ?); #s1 #I1
1199cases (initial_state_in_simulation … I1)
1200#s2 * #I2
1201
1202whd in match (exec_inf ?? clight_fullexec p) in NW ⊢ %;
1203letin ge1 ≝ (make_global ?? clight_fullexec p) in NW ⊢ %;
1204change with (make_initial_state p) in match (make_initial_state ?? clight_fullexec p);
1205>I1
1206
1207whd in match (exec_inf ????);
1208letin ge2 ≝ (make_global ?? clight_fullexec (\fst (clight_label p)))
1209change with (make_initial_state (\fst (clight_label p))) in match (make_initial_state ?? clight_fullexec (\fst (clight_label p)));
1210>I2
1211
1212whd in ⊢ (??% → ? → ?%%);
1213>exec_inf_aux_unfold
1214>exec_inf_aux_unfold
1215whd in ⊢ (??% → ? → ?%%);
1216whd in match (is_final ?????);
1217>(initial_state_is_not_final … I1)
1218whd in match (is_final ?????);
1219>(initial_state_is_not_final … I2)
1220whd in ⊢ (??% → ? → ?%%);
1221
1222#NW #S
1223@(swl_steps E0 E0)
1224[ 2: @steps_step | skip | // | @build_exec
1225  [ @transform_program_gen_related | // | inversion NW
1226    [ #tr #i #s #E1 #E2 destruct
1227    | #trX #sX #eX #NWX #E1X #E2X destruct //
1228    | #H1 #H2 #H3 #H4 #H5 destruct
1229    ]
1230  ]
1231] qed.
1232
1233
1234
Note: See TracBrowser for help on using the repository browser.