source: src/Clight/labelSimulation.ma @ 2176

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

Remove memory spaces other than XData and Code; simplify pointers as a
result.

File size: 60.5 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 … 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 ⊢ (??%? → ??%?); >(rg_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 … 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,cs,cpost,k,k'.
267    cont_with_labels k k' →
268    cont_with_labels (Kwhile e s k) (Kwhile (\fst (label_expr e ue)) (Scost cs (\fst (label_statement s us))) (Kseq (Scost cpost Sskip) k'))
269| cwl_dowhile : ∀ue,e,us,s,cs,cpost,k,k'.
270    cont_with_labels k k' →
271    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'))
272| cwl_for1 : ∀ue,e,us1,s1,us2,s2,cs,cpost,k,k'.
273    cont_with_labels k k' →
274    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'))
275| 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'))
276| 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'))
277| cwl_switch : ∀k,k'. cont_with_labels k k' → cont_with_labels (Kswitch k) (Kswitch k')
278| cwl_call : ∀r,f,en,k,k'. cont_with_labels k k' → cont_with_labels (Kcall r f en k) (Kcall r (label_function f) en k')
279| cwl_seqls : ∀ls,u,k,k'. cont_with_labels k k' →
280    cont_with_labels (Kseq (seq_of_labeled_statement ls) k) (Kseq (seq_of_labeled_statement (\fst (label_lstatements ls u))) k').
281
282lemma call_cont_with_labels : ∀k,k'.
283  cont_with_labels k k' →
284  cont_with_labels (call_cont k) (call_cont k').
285#k0 #k0' #K elim K /2/
286qed.
287
288(* Now define almost all of the simulation relation... *)
289inductive state_with_labels_partial : state → state → Prop ≝
290| swl_state : ∀f,us,s,k,k',e,m. cont_with_labels k k' → state_with_labels_partial (State f s k e m) (State (label_function f) (\fst (label_statement s us)) k' e m)
291(* Extra matching states that we can reach that don't quite correspond to the
292   labelling function *)
293| swl_whilestate : ∀f,ua,a,us,s,cs,cpost,k,k',e,m. cont_with_labels k k' →
294    state_with_labels_partial (State f (Swhile a s) k e m) (State (label_function f) (Swhile (\fst (label_expr a ua)) (Scost cs (\fst (label_statement s us)))) (Kseq (Scost cpost Sskip) k') e m)
295| swl_dowhilestate : ∀f,ua,a,us,s,cs,cpost,k,k',e,m. cont_with_labels k k' →
296    state_with_labels_partial (State f (Sdowhile a s) k e m) (State (label_function f) (Sdowhile (\fst (label_expr a ua)) (Scost cs (\fst (label_statement s us)))) (Kseq (Scost cpost Sskip) k') e m)
297| swl_forstate : ∀f,ua2,a2,us3,s3,us,s,cs,cpost,k,k',e,m. cont_with_labels k k' →
298    state_with_labels_partial (State f (Sfor Sskip a2 s3 s) k e m) (State (label_function 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)
299(* and the rest *)
300| swl_callstate : ∀fd,args,k,k',m. cont_with_labels k k' → state_with_labels_partial (Callstate fd args k m) (Callstate (label_fundef fd) args k' m)
301| swl_returnstate : ∀res,k,k',m. cont_with_labels k k' → state_with_labels_partial (Returnstate res k m) (Returnstate res k' m)
302| swl_finalstate : ∀r. state_with_labels_partial (Finalstate r) (Finalstate r)
303.
304
305(* ... and add the states where the cases from switch statements are expanded.
306   We do these separately because in the LSdefault case we have to execute a
307   cost label alongside an arbitrary statement, and we want to reuse the result
308   on arbitrary statements we get for state_with_labels_partial. *)
309inductive state_with_labels : state → state → Prop ≝
310| swl_partial : ∀s,s'. state_with_labels_partial s s' → state_with_labels s s'
311| swl_switchstate : ∀f,u,ls,k,k',e,m. cont_with_labels k k' →
312    state_with_labels (State f (seq_of_labeled_statement ls) k e m)
313                      (State (label_function f) (seq_of_labeled_statement (\fst  (label_lstatements ls u))) k' e m)
314.
315
316(* TODO: this (or something like it) ought to be elsewhere. *)
317inductive plus (ge:genv) : state → trace → state → Prop ≝
318| plus_one : ∀s1,tr,s2. exec_step ge s1 = OK … 〈tr,s2〉 → plus ge s1 tr s2
319| plus_succ : ∀s1,tr,s2,tr',s3. exec_step ge s1 = OK … 〈tr,s2〉 → plus ge s2 tr' s3 → plus ge s1 (tr⧺tr') s3.
320
321(* Some details are invariant under labelling. *)
322lemma label_function_return : ∀f.
323  fn_return (label_function f) = fn_return f.
324* #rty #params #vars #body
325whd in ⊢ (??(?%)?);
326cases (label_statement ??) #body' #u'
327whd in ⊢ (??(?%)?);
328cases (add_cost_before ??) #body'' #u''
329//
330qed.
331
332lemma label_expr_fun_typeof : ∀a,u.
333  fun_typeof (\fst (label_expr a u)) = fun_typeof a.
334#a #u whd in ⊢ (??%?); >label_expr_type @refl
335qed.
336
337lemma label_fundef_typeof_fundef : ∀fd.
338  type_of_fundef (label_fundef fd) = type_of_fundef fd.
339* //
340* #rty #args #vars #body
341normalize cases (label_statement ??) #body' #u
342normalize cases (fresh ??) //
343qed.
344
345lemma label_fn_params : ∀f.
346  fn_params (label_function f) = fn_params f.
347* #rty #params #vars #s whd in ⊢ (??(?%)?); @breakup_pair @breakup_pair //
348qed.
349
350lemma label_fn_vars : ∀f.
351  fn_vars (label_function f) = fn_vars f.
352* #rty #params #vars #s whd in ⊢ (??(?%)?); @breakup_pair @breakup_pair //
353qed.
354
355(* Some annoying rewrite rules *)
356lemma exec_lvalue_labelled : ∀ge,e,m,a,ty,u.
357  exec_lvalue ge e m (\fst (label_expr (Expr a ty) u)) =
358  exec_lvalue' ge e m (\fst (label_expr_descr a u ty)) ty.
359#ge #e #m #a #ty #u
360whd in ⊢ (??(????(???%))?); >shift_fst @refl
361qed.
362
363lemma opt_find_funct : ∀ge,ge',m,vf,fd.
364  related_globals … label_fundef ge ge' →
365  opt_to_io io_out io_in … m (find_funct … ge vf) = Value … fd →
366  opt_to_io io_out io_in … m (find_funct … ge' vf) = Value … (label_fundef fd).
367#ge #ge' #m #vf #fd #RG
368lapply (rg_find_funct … RG … vf fd)
369cases (find_funct … vf)
370[ #_ #E normalize in E; destruct
371| #fd' #H #E normalize in E; destruct >(H (refl ??)) //
372] qed.
373
374lemma labelled_not_skip : ∀s,u.
375  s ≠ Sskip →
376  (\fst (label_statement s u)) ≠ Sskip.
377* #u
378[ * #H cases (H (refl ??))
379| *: #a try #b try #c try #d try #e
380     (* Use the state-monad-like structure of the labelling function to break
381        it up *)
382     whd in match (label_statement ??);
383     repeat @(breakup_pair ???? (λx.\fst x ≠ Sskip))
384     % #E destruct
385] qed.
386
387lemma labelled_is_not_skip : ∀s,u.
388  s ≠ Sskip →
389  ∃pf. is_Sskip (\fst (label_statement s u)) = inr … pf.
390#s #u #NE
391cases (is_Sskip ?)
392[ #E @⊥ @(absurd ? E) @labelled_not_skip //
393| /2/
394] qed.
395
396lemma label_select_ls : ∀sz,i,ls,u.
397  ∃u'.
398    select_switch sz i (\fst (label_lstatements ls u)) =
399    \fst (label_lstatements (select_switch sz i ls) u').
400#sz #i #ls @(labeled_statements_ind … ls)
401[ #s #u % [2: whd in match (label_lstatements ??);
402  @label_gen_elim #u1 >shift_fst @refl | skip ]
403| #sz' #i' #s #tl #IH #u
404  whd in match (label_lstatements ??);
405  whd in match (select_switch ?? (LScase ????));
406  @intsize_eq_elim_elim
407  [ #NE
408    @label_gen_elim #u1 @label_gen_elim #u2 @label_gen_elim #u3
409    cases (IH u2)
410    #u4 #E %{u4} whd in ⊢ (??%?);
411    >intsize_eq_elim_false //
412  | #E <E in i' ⊢ %; #i' whd
413    @eq_bv_elim
414    [ #Ei >Ei
415      %{u}
416      whd in match (label_lstatements (if ? then ? else ?) ?);
417      @label_gen_elim #u1 @label_gen_elim #u2 @label_gen_elim #u3
418      whd in ⊢ (??%?);
419      >intsize_eq_elim_true
420      >eq_bv_true
421      @refl
422    | #NEi
423      @label_gen_elim #u1 @label_gen_elim #u2 @label_gen_elim #u3
424       whd in ⊢ (??(λ_.??%?));
425       >intsize_eq_elim_true
426       >eq_bv_false //
427    ]
428  ]
429] qed.
430
431(* Break up labelling function in one go for statements. *)
432lemma blindly_label : ∀u,s. ∀P:statement → Prop.
433match s with
434[ Sskip ⇒ P Sskip
435| Sassign e1 e2 ⇒ ∀u1,u2. P (Sassign (\fst (label_expr e1 u1)) (\fst (label_expr e2 u2)))
436| 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)))
437| Ssequence s1 s2 ⇒ ∀u1,u2. P (Ssequence (\fst (label_statement s1 u1)) (\fst (label_statement s2 u2)))
438| 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))))
439| Swhile e s1 ⇒ ∀u1,u2,cs,cpost. P (Ssequence (Swhile (\fst (label_expr e u1)) (Scost cs (\fst (label_statement s1 u2)))) (Scost cpost Sskip))
440| 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))
441| 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))
442| Sbreak ⇒ P Sbreak
443| Scontinue ⇒ P Scontinue
444| Sreturn eo ⇒ ∀u1. P (Sreturn (\fst (label_opt_expr eo u1)))
445| Sswitch e ls ⇒ ∀u1,u2. P (Sswitch (\fst (label_expr e u1)) (\fst (label_lstatements ls u2)))
446| Slabel l s1 ⇒ ∀u1,cs. P (Slabel l (Scost cs (\fst (label_statement s1 u1))))
447| Sgoto l ⇒ P (Sgoto l)
448| Scost c s1 ⇒ ∀u1. P (Scost c (\fst (label_statement s1 u1)))
449] → P (\fst (label_statement s u)). 
450#u * // #A #B #C try #D try #E try #F whd in match (label_statement ??);
451@label_gen_elim #u1 //
452@label_gen_elim #u2 //
453[ 6: >shift_fst //
454| *: @label_gen_elim #u3 //
455     @label_gen_elim #u4
456     [ @label_gen_elim #u5 >shift_fst >shift_fst //
457     | 2,3: >shift_fst >shift_fst //
458     | @label_gen_elim #u5 >shift_fst >shift_fst >shift_fst //
459     ]
460] qed.
461
462(* Apply induction hypothesis in label_find_label proof below while getting
463   Matita to infer the continuations k0 and k0', and the universe u0, rather
464   than having to give them explicitly. *)
465lemma lfl_IH : ∀s0,lbl.
466  ∀C:option (statement×cont) → option (statement×cont) → Prop.
467  ∀IH:cont → cont → universe CostTag → Prop.
468  (∀k,k',u. cont_with_labels k k' → IH k k' u) →
469  ∀k0,k0',u0. cont_with_labels k0 k0' →
470   (IH k0 k0' u0 →
471    C (find_label lbl s0 k0) (find_label lbl (\fst (label_statement s0 u0)) k0')) →
472   C (find_label lbl s0 k0) (find_label lbl (\fst (label_statement s0 u0)) k0').
473/3/
474qed.
475
476(* Finding a goto label in a cost-labelled program gives a labelled version of
477   the statement and continuation found by the original function, if any. *)
478lemma label_find_label : ∀lbl,s,k,k',u.
479  cont_with_labels k k' →
480  match find_label lbl s k with
481  [ Some r' ⇒ let 〈s1,k1〉 ≝ r' in
482    ∃u',cs,k1'.
483    find_label lbl (\fst (label_statement s u)) k' = Some ? 〈Scost cs (\fst (label_statement s1 u')), k1'〉 ∧
484    cont_with_labels k1 k1'
485  | None ⇒ find_label lbl (\fst (label_statement s u)) k' = None ?
486  ].
487#lbl #s @(statement_ind2 ? (λls.
488  ∀k,k',u.
489  cont_with_labels k k' →
490  match find_label_ls lbl ls k with
491  [ Some r' ⇒ let 〈s1,k1〉 ≝ r' in
492    ∃u',cs,k1'.
493    find_label_ls lbl (\fst (label_lstatements ls u)) k' = Some ? 〈Scost cs (\fst (label_statement s1 u')), k1'〉 ∧
494    cont_with_labels k1 k1'
495  | None ⇒ find_label_ls lbl (\fst (label_lstatements ls u)) k' = None ?
496  ])
497 … s)
498[ #k #k' #u #F @refl
499| #e1 #e2 #k #k' #u #K @blindly_label #u1 #u2 whd @refl
500| #e0 #e #args #k #k' #u #K @blindly_label #u1 #u2 #u3 whd @refl
501| #sA #sB #IH1 #IH2 #k #k' #u #K @blindly_label #u1 #u2 whd in match (find_label ???);
502  whd in match (find_label ?? k');
503  @(lfl_IH sA … IH1) [ /2/ ]
504  cases (find_label ???)
505  [ whd in ⊢ (% → match % with [_⇒?|_⇒?]); #FIND1'
506    @(lfl_IH … IH2) [ // ]
507    cases (find_label ???)
508    [ whd in ⊢ (% → %); #FIND2' whd in ⊢ (??%?); >FIND1' >FIND2' @refl
509    | * #s3 #k3 whd in ⊢ (% → %); * #u3 * #cs * #k1' * #FIND2' #K1'
510      % [2: %{cs} %{k1'} % // whd in ⊢ (??%?); >FIND1' in ⊢ (??%?); >FIND2' in ⊢ (??%?); @refl | skip ]
511    ]
512  | * #sA' #kA' whd in ⊢ (% → %);
513    * #u1' * #cs * #k1' * #FA' #K'
514         % [2: %{cs} %{k1'} % [ whd in ⊢ (??%?); >FA' in ⊢ (??%?); @refl | // ] |skip]
515  ]
516| #e #s1 #s2 #IH1 #IH2 #k #k' #u @blindly_label #u1 #u2 #u3 #c2 #c3 #K
517  whd in match (find_label ?? k); whd in match (find_label ?? k');
518  whd in match (find_label ?? k');
519  @(lfl_IH  … IH1) [ // ] cases (find_label ???)
520  [ whd in ⊢ (% → match % with [_⇒?|_⇒?]); #FIND1'
521    lapply (IH2 k k' u3 K) cases (find_label ???)
522    [ whd in ⊢ (% → %); #FIND2'
523      whd in match (find_label ???); >FIND1'
524      whd in match (find_label ???); >FIND2' @refl
525    | * #s2' #k2' * #u4 * #cs * #k1' * #FIND2' #K2'
526      % [2: % [2: % [2: % [ whd in ⊢ (??%?);
527      whd in match (find_label ???); >FIND1' in ⊢ (??%?);
528      whd in match (find_label ???); >FIND2' in ⊢ (??%?); @refl
529      | // ]|skip]|skip]|skip]
530    ]
531  | * #s1' #k1 whd in ⊢ (% → %); * #u4 * #cs * #k1' * #FIND1' #K1'
532    % [2: % [2: % [2: % [
533      whd in ⊢ (??%?); whd in match (find_label ???); >FIND1' in ⊢ (??%?);
534      @refl | // ] |skip ]| skip ]| skip ]
535  ]
536| #e #s0 #IH #k #k' #u #K @blindly_label #u1 #u2 #cs #cpost
537  whd in match (find_label ?? k); normalize in match (find_label ?? k');
538  @(lfl_IH s0 … IH) [ /2/ ]
539  cases (find_label ???)
540  [ whd in ⊢ (% → %); #FIND1'
541    whd in ⊢ (??%?); whd in match (find_label ???); >FIND1' @refl
542  | * #s1 #k1 * #u4 * #cs * #k1' * #FIND1' #K1'
543    % [2: % [2: % [2: % [
544      whd in ⊢ (??%?); whd in match (find_label ???); >FIND1' in ⊢ (??%?);
545      @refl | // ]| skip ]| skip ]| skip ]
546  ]
547| #e #s0 #IH #k #k' #u #K @blindly_label #u1 #u2 #cs #cpost
548  whd in match (find_label ?? k); normalize in match (find_label ?? k');
549  @(lfl_IH s0 … IH) [ /2/ ]
550  cases (find_label ???)
551  [ whd in ⊢ (% → %); #FIND1'
552    whd in ⊢ (??%?); whd in match (find_label ???); >FIND1' @refl
553  | * #s1 #k1 * #u4 * #cs * #k1' * #FIND1' #K1'
554    % [2: % [2: % [2: % [
555      whd in ⊢ (??%?); whd in match (find_label ???); >FIND1' in ⊢ (??%?);
556      @refl | // ]| skip ]| skip ]| skip ]
557  ]
558| #s1 #e #s2 #s3 #IH1 #IH2 #IH3 #k #k' #u #K @blindly_label #u1 #u2 #u3 #u4 #c3 #c4
559  whd in match (find_label ???); normalize in match (find_label ?? k');
560  @(lfl_IH s1 … IH1) [ /2/ ]
561  cases (find_label ???)
562  [ whd in ⊢ (% → match % with [_⇒?|_⇒?]); #FIND1' >FIND1'
563    @(lfl_IH s3 … IH3) [ /2/ ]
564    cases (find_label ???)
565    [ whd in ⊢ (% → match % with [_⇒?|_⇒?]); #FIND3' >FIND3'
566      @(lfl_IH s2 … IH2) [ /2/ ]
567      cases (find_label ???)
568      [ whd in ⊢ (% → %); #FIND2' >FIND2' @refl
569      | * #s2' #k2' * #u2' * #cs' * #k1' * #FIND2' #K2'
570        % [2: % [2: % [2: % [
571         whd in ⊢ (??%?); >FIND2' in ⊢ (??%?); @refl
572        | // ]| skip ]| skip ]| skip ]
573      ]
574    | * #s3' #k3' * #u3' * #cs' * #k1' * #FIND3' #K3'
575        % [2: % [2: % [2: % [
576        >FIND3' in ⊢ (??%?); whd in ⊢ (??%?); @refl
577        | // ]| skip ]| skip ]| skip ]
578    ]
579  | * #s1' #k1' * #u1' * #cs' * #k1' * #FIND1' #K1'
580        % [2: % [2: % [2: % [
581        >FIND1' in ⊢ (??%?); whd in ⊢ (??%?); @refl
582        | // ]| skip ]| skip ]| skip ]
583  ]
584| //
585| //
586| #eo #k #k' #u @blindly_label #u1 //
587| #e #ls #IH #k #k' #u #K @blindly_label #u1 #u2
588  normalize in match (find_label ???); normalize in match (find_label ???);
589  lapply (IH (Kswitch k) (Kswitch k') u2 ?) [/2/] cases (find_label_ls ???)
590  [ whd in ⊢ (% → %); //
591  | * #s1' #k1' * #u' * #cs * #k'' * #FIND' #K'
592    % [2: % [2: % [2: % [ @FIND' | // ]|skip ]|skip]|skip]
593  ]
594| #l #s0 #IH #k #k' #u #K @blindly_label #u1 #cs
595  whd in match (find_label ???); whd in match (find_label ?? k');
596  cases (ident_eq lbl l)
597  [ #E destruct whd
598    % [2: % [2: % [2: % [ @refl | // ]|skip ]|skip ]| skip ]
599  | #NE whd in ⊢ (match % with [_⇒?|_⇒?]);
600    normalize in match (find_label ?? k');
601    @(lfl_IH s0 … IH) [ // ]
602    cases (find_label ???)
603    [ //
604    | * #s0' #k0' * #u' * #cs0 * #k1' * #FIND0 #K0
605      % [2: % [2: % [2: % [ @FIND0 | // ]|skip ]|skip]|skip]
606    ]
607  ]
608| //
609| #l #s0 #IH #k #k' #u #K @blindly_label #u1 /2/
610| #s0 #IH #k #k' #u whd in match (label_lstatements ??);
611  @label_gen_elim #u1 >shift_fst >shift_fst
612  whd in match (find_label_ls ???); whd in match (find_label_ls ???);
613  @IH
614| #sz #i #s0 #tl #IH1 #IH2 #k #k' #u #K
615  whd in match (label_lstatements ??); @label_gen_elim #u1 @label_gen_elim #u2
616  @label_gen_elim #u3 >shift_fst
617  whd in match (find_label_ls ???); normalize in match (find_label_ls ?? k');
618  @(lfl_IH s0 … IH1) [ /2/ ]
619  cases (find_label ???)
620  [ whd in ⊢ (% → match % with [_⇒?|_⇒?]); #FIND0 >FIND0
621    lapply (IH2 k k' u2 K) cases (find_label_ls ???)
622    [ whd in ⊢ (% → %); #FINDtl >FINDtl @refl
623    | * #stl #ktl //
624    ]
625  | * #s0' #k0' whd in ⊢ (% → %);
626    * #u' * #cs * #k1' * #FIND0 #K0 >FIND0
627    % [2: % [2: % [2: % [ @refl | // ] | skip ] | skip ] | skip ]
628  ]
629] qed.
630
631lemma label_find_label_fn : ∀lbl,f,k,k',s1,k1.
632  cont_with_labels k k' →
633  find_label lbl (fn_body f) (call_cont k) = Some ? 〈s1,k1〉 →
634  ∃u',cs,k1'.
635    find_label lbl (fn_body (label_function f)) (call_cont k') = Some ? 〈Scost cs (\fst (label_statement s1 u')), k1'〉 ∧
636    cont_with_labels k1 k1'.
637#lbl * #rty #args #vars #s #k #k' #s1 #k1 #K #FIND
638whd in match (label_function ?);
639@label_gen_elim #u1 @label_gen_elim #u2 >shift_fst
640lapply (label_find_label lbl s (call_cont k) (call_cont k') (new_universe ?) ?)
641[ /2/ ]
642>FIND //
643qed.
644
645
646(* We show the main simulation in two stages.  First, we show it for all states
647   in the relation *except* those for labeled_statements, then we'll show the
648   whole thing.  This is so that we can appeal to the other cases in the proof
649   for labeled_statements. *)
650lemma step_with_labels_partial : ∀ge,ge'.
651  related_globals … label_fundef ge ge' →
652  ∀s1,s1',tr,s2.
653  state_with_labels_partial s1 s1' →
654  exec_step ge s1 = Value … 〈tr,s2〉 →
655   ∃tr',s2'. plus ge' s1' 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[ #f #us #s #k #k' #e #m #KL cases s
666  [ #EX inversion KL
667    [ #E1 #E2 #_ destruct %{tr}
668      whd in EX:(??%?);
669      lapply (refl ? (fn_return f)) cases (fn_return f) in ⊢ (???% → ?);
670      [ #E >E in EX; whd in ⊢ (??%% → ?); #EX' destruct %{(Returnstate Vundef Kstop (free_list m (blocks_of_env e)))}
671        % [ % [ @plus_one whd in ⊢ (??%?); >label_function_return >E @refl
672        | // ] | /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 %{tr}
676      %{(State (label_function f) (\fst (label_statement s0 u)) k0' e m)}
677      whd in EX:(??%%); destruct
678      % [ % [ @plus_one @refl | // ] | /3/ ]
679    | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct %{tr}
680      whd in EX:(??%%); destruct
681      % [ 2: % [ % [ @plus_one @refl | // ] | @swl_partial @swl_whilestate // ] | skip ]
682    | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct
683      cases (bindIO_inversion ??????? EX) * #ve #tre * #EXe #EXrem
684      cases (bindIO_inversion ??????? EXrem) * * #EXb #EXbrem -EXrem
685      normalize in EXbrem; destruct
686      cases ((proj1 ?? (label_expr_ok ge ge' e m RG)) ??? EXe ue) #tre' * #EXe' #Te
687      [ % [ 2: % [ 2: % [ % [ @plus_one
688        whd in ⊢ (??%?); >EXe' in ⊢ (??%?);
689        whd in ⊢ (??%?); >label_expr_type >EXb in ⊢ (??%?);
690        whd in ⊢ (??%?); @refl
691        | // ]
692        | @swl_partial @swl_dowhilestate // ] | skip ] | skip ]
693      | % [ 2: % [ 2: % [ % [ @plus_succ [
694        4: whd in ⊢ (??%?); >EXe' in ⊢ (??%?);
695           whd in ⊢ (??%?); >label_expr_type >EXb in ⊢ (??%?);
696           whd in ⊢ (??%?); @refl
697        | skip | skip
698        | 5: @plus_succ [ 4: @refl | skip | skip
699        | 5: @plus_one @refl | skip ] | skip ]
700        | <(E0_right tr) @twel_app /2/ ]
701        | /3/ ] | skip ] | skip ]
702      ]
703    | #ue #e0 #us1 #st1 #us2 #st2 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct
704      whd in EX:(??%?); destruct
705      %{E0} % [2: % [ % [ @plus_one @refl | // ] | /3/ ] | skip ]
706    | #ue #e0 #us1 #st1 #us2 #st2 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct
707      whd in EX:(??%?); destruct
708      %{E0} % [2: % [ % [ @plus_one @refl | // ] | /4/ ] | skip ]
709    | #ue #e0 #us1 #st1 #us2 #st2 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct
710      whd in EX:(??%?); destruct
711      %{E0} % [2: % [ % [ @plus_one @refl | // ] | /4/ ] | skip ]
712    | #k0 #k0' #K #_ #E1 #E2 #E3 destruct
713      whd in EX:(??%?); destruct
714      %{E0} % [2: % [ % [ @plus_one @refl | // ] | /4/ ] | skip ]
715    | #r #f0 #en #k0 #k0' #K #_ #E1 #E2 #E3 destruct
716      whd in EX:(??%?);
717      lapply (refl ? (fn_return f)) cases (fn_return f) in ⊢ (???% → ?);
718      [ #E >E in EX; whd in ⊢ (??%? → ?); #EX destruct
719        %{E0} % [2: % [ % [ @plus_one whd in ⊢ (??%?); >label_function_return >E in ⊢ (??%?);
720        @refl | // ] | /4/ ] | skip ]
721      | *: #A [ 1,4,5,6,7: #B ] #E >E in EX; #EX whd in EX:(??%%); destruct
722      ]
723    | #ls #u #k0 #k0' #K #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
724      % [2: % [2: % [ % [ @plus_one @refl | // ] | /3/ ]| skip ]| skip ]
725    ]
726  | * #a1 #ty1 #a2 #EX
727    cases (bindIO_inversion ??????? EX) -EX * * #b1 #o1 #tr1 * #EX1 #EX
728    cases (bindIO_inversion ??????? EX) -EX * #v2 #tr2 * #EX2 #EX
729    cases (bindIO_inversion ??????? EX) -EX #m3 * #EX3 #EX
730    whd in EX:(??%%); destruct
731    cases (proj2 ?? (label_expr_ok ge ge' e m RG) ????? EX1 us) #tr1' * #EX1' #T1
732    whd in match (label_statement ??);
733    @label_gen_elim #ua1 @label_gen_elim #ua2
734    cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX2 ua1) #tr2' * #EX2' #T2
735    % [2: % [2: % [ % [
736      @plus_one whd in ⊢ (??%?);     
737      >exec_lvalue_labelled >EX1' in ⊢ (??%?);
738      whd in ⊢ (??%?); >EX2' in ⊢ (??%?);
739      whd in ⊢ (??%?); >label_expr_type >EX3 in ⊢ (??%?);
740      @refl
741    | @twel_app // ] | /3/ ] | skip ] | skip ]
742  | * [2: * #er #tyr ] #ef #args #EX
743    cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
744    cases (bindIO_inversion ??????? EX) -EX * #args' #tr2 * #EX2 #EX
745    cases (bindIO_inversion ??????? EX) -EX #fd * #EX3 #EX
746    cases (bindIO_inversion ??????? EX) -EX #E4 * #EX4 #EX
747    whd in EX:(??%%);
748    [ cases (bindIO_inversion ??????? EX) -EX * * #b5 #o5 #tr5 * #EX5 #EX whd in EX:(??%%); ]
749    destruct
750    whd in match (label_statement ??);
751    whd in match (label_opt_expr ??);
752    [ @(label_gen_elim … (Expr er tyr)) #u' @breakup_pair | letin u' ≝ us ]
753    cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 u') #tr1' * #EX1' #T1
754    @label_gen_elim #u1
755    @label_gen_elim #u2
756    cases (label_exprs_ok ge ge' RG e m args args' ? EX2 u1) #tr2' * #EX2' #T2
757    [ cases (proj2 ?? (label_expr_ok ge ge' e m RG) ????? EX5 us) #tr5' * #EX5' #T5 ]
758    % [2,4: % [2,4: % [1,3: % [1,3:
759      @plus_one whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?); | >EX1' in ⊢ (??%?); ] (* XXX why do I need the repetition? *)
760      whd in ⊢ (??%?); [ >EX2' in ⊢ (??%?); | >EX2' in ⊢ (??%?); ]
761      whd in ⊢ (??%?); >(opt_find_funct … RG … EX3) in ⊢ (??%?);
762      whd in ⊢ (??%?); >label_fundef_typeof_fundef >label_expr_fun_typeof [ >EX4 in ⊢ (??%?); | >EX4 in ⊢ (??%?); ]
763      whd in ⊢ (??%?); [ >exec_lvalue_labelled >EX5' in ⊢ (??%?); ]
764      @refl | *: @twel_app /2/ ] | *: @swl_partial @swl_callstate /2/ ] | *: skip ] | *: skip ]
765  | #st1 #st2 #EX
766    whd in EX:(??%%); destruct
767    whd in match (label_statement ??); @label_gen_elim #u1 @label_gen_elim #u2
768    %{E0} % [2: % [ % [ @plus_one @refl | // ] | @swl_partial @swl_state /2/ ] | skip ]
769  | #a #st1 #st2 #EX
770    cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
771    cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX
772    normalize in EX; destruct
773    whd in match (label_statement ??); @label_gen_elim #u1
774    @label_gen_elim #u2 @label_gen_elim #u3 @label_gen_elim #u4
775    @label_gen_elim #u5
776    whd in match (add_cost_before ??); cases (fresh ??) #c6 #u6
777    whd in match (add_cost_before ??); cases (fresh ??) #c7 #u7
778    cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1
779    % [2,4: % [2,4: % [1,3: % [1,3: @plus_succ [ 4,9:
780      whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?); | >EX1' in ⊢ (??%?); ] (* XXX repeated? *)
781      whd in ⊢ (??%?); >label_expr_type [ >EX2 in ⊢ (??%?); | >EX2 in ⊢ (??%?); ]
782      whd in ⊢ (??%?); @refl
783    | 1,2,6,7: skip
784    | 5,10: @plus_one @refl
785    | *: skip
786    ]
787    | 2,4: <(E0_right tr) @twel_app /2/
788    ]| 2,4: /3/ ] | *: skip ] | *: skip ]
789  | #a #st #EX
790    cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
791    cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX
792    normalize in EX; destruct
793    whd in match (label_statement ??); @label_gen_elim #u1
794    @label_gen_elim #u2
795    whd in match (add_cost_before ??); cases (fresh ??) #c6 #u6
796    >shift_fst whd in match (add_cost_after ??); cases (fresh ??) #c7 #u7
797    >shift_fst
798    cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1
799    % [2,4: % [2,4: % [1,3: % [1,3: @plus_succ [ 4,9: @refl | 1,2,6,7: skip
800      | 5,10: @plus_succ [ 4,9:
801      whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?); | >EX1' in ⊢ (??%?); ] (* XXX repeated? *)
802      whd in ⊢ (??%?); >label_expr_type [ >EX2 in ⊢ (??%?); | >EX2 in ⊢ (??%?); ]
803      whd in ⊢ (??%?); @refl
804    | 1,2,6,7: skip
805    | 5: @plus_one @refl
806    | 10: @plus_succ [ 4: @refl | 5: @plus_one @refl | *: skip ] |*: skip ]
807    | *: skip
808    ]
809    | 2,4: <(E0_left tr) @twel_app // <(E0_right tr) @twel_app /2/
810    ]| 2,4: /4/ ] | *: skip ] | *: skip ]
811  | #a #st #EX
812    normalize in EX; destruct
813    whd in match (label_statement ??); @label_gen_elim #u1
814    @label_gen_elim #u2
815    whd in match (add_cost_before ??); cases (fresh ??) #c6 #u6 >shift_fst
816    whd in match (add_cost_after ??); cases (fresh ??) #c7 #u7 >shift_fst
817    % [2: % [2: % [ % [ @plus_succ [ 4: @refl | 1,2: skip
818      | 5: @plus_succ [ 4: @refl | 1,2: skip | 5: @plus_one // | skip ] | skip ]
819      | /2/ ] | /4/ ] | skip ] | skip ]
820  | #st1 #a #st2 #st #EX
821    lapply (refl ? (is_Sskip st1)) cases (is_Sskip st1) in ⊢ (???% → ?); #Esk #Eskip
822    whd in EX:(??%?); >Eskip in EX; #EX
823    whd in match (label_statement ??); @label_gen_elim #u1
824    @label_gen_elim #u2 @label_gen_elim #u3 @label_gen_elim #u4
825    whd in match (add_cost_before ??); cases (fresh ??) #c5 #u5 >shift_fst
826    whd in match (add_cost_after ??); cases (fresh ??) #c6 #u6 >shift_fst
827    [ cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
828      cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX
829      normalize in EX; destruct
830      cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1
831      % [2,4: % [2,4: % [1,3: % [1,3: @plus_succ [ 4,9: @refl | 1,2,6,7: skip
832      | 5,10: @plus_succ [ 4,9:
833      whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?); | >EX1' in ⊢ (??%?); ] (* XXX repeated? *)
834      whd in ⊢ (??%?); >label_expr_type [ >EX2 in ⊢ (??%?); | >EX2 in ⊢ (??%?); ]
835      whd in ⊢ (??%?); @refl
836      | 1,2,6,7: skip
837      | 5: @plus_one @refl
838      | 10: @plus_succ [ 4: @refl | 5: @plus_one @refl | *: skip ] |*: skip ]
839      | *: skip
840      ]
841      | 2,4: <(E0_left tr) @twel_app // <(E0_right tr) @twel_app /2/
842      ]| 2,4: /4/ ] | *: skip ] | *: skip ]
843    | whd in EX:(??%%); destruct
844      % [2: % [2: %[ %[ @plus_succ [ 4: @refl | 5: @plus_one
845        whd in ⊢ (??%?); cases (labelled_is_not_skip ? u1 Esk) #Esk' #Eskip'
846        >Eskip' whd in ⊢ (??%?); @refl | *: skip ]| // ] | @swl_partial @swl_state /2/ ]
847      | skip ] | skip ]
848    ]
849  | #EX inversion KL
850    [ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
851    |#u #s0 #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
852    | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
853    | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
854    | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
855    | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
856    | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
857    | #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
858    | #r #f0 #en #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
859    | #ls #u #k0 #k0' #K #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
860    ]
861    whd in match (label_statement ??);
862    % [2,4,6,8,10,12,14: % [2,4,6,8,10,12,14: % [1,3,5,7,9,11,13: %
863    [1,11,13: @plus_one @refl | 2,12,14: //
864    | @plus_succ [ 4: @refl | 5: @plus_succ [ 4: @refl | 5: @plus_one @refl |*:skip]|*:skip] | /2/
865    | @plus_succ [ 4: @refl | 5: @plus_succ [ 4: @refl | 5: @plus_one @refl |*:skip]|*:skip] | /2/
866    | @plus_succ [ 4: @refl | 5: @plus_one @refl |*:skip] | /2/
867    | @plus_succ [ 4: @refl | 5: @plus_succ [ 4: @refl | 5: @plus_one @refl |*:skip]|*:skip] | /2/
868    ]| *: /3/ ]|*: skip]|*: skip ]
869  | #EX inversion KL
870    [ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
871    |#u #s0 #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
872    | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
873    | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
874    | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
875    | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
876    | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
877    | #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
878    | #r #f0 #en #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
879    | #ls #u #k0 #k0' #K #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
880    ]
881    whd in match (label_statement ??);
882    [ 1,2,4,5,6,7: % [2,4,6,8,10,12: % [2,4,6,8,10,12: % [1,3,5,7,9,11: %
883      [1,3,7,9,11: @plus_one @refl | 5: @plus_succ [4:@refl | 5:@plus_one @refl | *: skip ]
884      | *: // ] | *: @swl_partial /3 by cwl_for3, swl_state, swl_whilestate/ ]| *:skip ]| *: skip ]
885    | cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
886      cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX
887      normalize in EX; destruct
888      cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 ue) #tr1' * #EX1' #T1
889      % [2,4: % [2,4: % [1,3: % [1,3: [ @plus_one | @plus_succ ] [ 1,5:
890        whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?); | >EX1' in ⊢ (??%?); ] (* XXX repeated? *)
891      whd in ⊢ (??%?); >label_expr_type [ >EX2 in ⊢ (??%?); | >EX2 in ⊢ (??%?); ]
892      whd in ⊢ (??%?); @refl
893      | 6: @plus_succ [ 4: @refl | 5: @plus_one @refl | *: skip ] |*: skip ]
894      | // | <(E0_right tr) @twel_app /2/
895      ]
896      | /3/ | /3/ ] | *: skip ] | *: skip ]
897    ]
898  | * [2: #a ] #EX
899    whd in EX:(??%?); cases (type_eq_dec (fn_return f) Tvoid) in EX;
900    #Ety #EX whd in EX:(??%?);
901    [ destruct
902    | cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
903      cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1
904    | >Ety in EX; #EX
905    | @⊥ cases (fn_return f) in Ety EX;
906      [ * #H cases (H (refl ??))
907      | *: normalize #a #b #c try #d try #e destruct
908      ]
909    ]
910    whd in match (label_statement ??);
911    [ @label_gen_elim #u' whd in match (label_opt_expr ??); @label_gen_elim #u'' ]
912    whd in EX:(??%%); destruct
913    % [2,4: % [2,4: % [1,3: %[1,3: @plus_one
914      whd in ⊢ (??%?);
915      [ >label_function_return @(dec_false ? (type_eq_dec ??) Ety) #Ety''
916        whd in ⊢ (??%?); >EX1' in ⊢ (??%?);
917      | >label_function_return >Ety in ⊢ (??%?);
918      ] whd in ⊢ (??%?); @refl
919      | *: // ]| *: @swl_partial @swl_returnstate /2/ ]|*:skip]|*:skip]
920  | #a #ls #EX
921    cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
922    cases v1 in EX1 EX;
923    [ 2: #sz #i #EX1 #EX
924    | *: normalize #A #B try #C destruct
925    ]
926    whd in EX:(??%%); destruct
927    cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1
928    whd in match (label_statement ??); @label_gen_elim #u1 @label_gen_elim #u2
929    % [2: % [2: % [ % [ @plus_one whd in ⊢ (??%?); >EX1' in ⊢ (??%?); @refl
930      | // ]| cases (label_select_ls … sz i ls u1) #u3 #Els >Els /3/
931      ]|skip ]| skip ]
932  | #l #st #EX
933    whd in EX:(??%?); destruct
934    whd in match (label_statement ??); @label_gen_elim #u1 >shift_fst
935    whd in match (add_cost_before ??); cases (fresh ??) #cs #u2 >shift_fst
936    %[2: %[2: %[ %[ @plus_succ
937      [ 4: @refl | 5: @plus_one @refl | *: skip ]
938      | /2/ ] | /3/ ] |skip ]| skip ]
939  | #l #EX
940    whd in EX:(??%?);
941    @blindly_label whd
942    lapply (refl ? (find_label l (fn_body f) (call_cont k)))
943    cases (find_label ???) in ⊢ (???% → ?);
944    [ #F @⊥  >F in EX; #EX whd in EX:(??%?); destruct
945    | * #s1 #k1 #F >F in EX; #EX whd in EX:(??%?); destruct
946      cases (label_find_label_fn … KL F)
947      #u' * #cs * #k1' * #F' #K'
948      % [2: %[2: %[ %[ @plus_succ
949        [ 4: whd in ⊢ (??%?); >F' in ⊢ (??%?); @refl | 5: @plus_one @refl | *: skip ]
950        | /2/ ] | /3/ ] | skip ] | skip ]
951    ]
952  | #c #st #EX whd in EX:(??%?); destruct @blindly_label #u1
953    % [2: % [2: % [ % [ @plus_one @refl | // ] | /3/ ] | skip ]| skip ]
954  ]
955| #f #ua #a #us #s #cs #cpost #k #k' #e #m #K #EX
956  cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
957  cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX
958  whd in EX:(??%%); destruct
959  cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 ua) #tr1' * #EX1' #T1
960  [ % [2: % [2: % [ % [
961    @plus_succ [4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?);
962                   whd in ⊢ (??%?); >label_expr_type >EX2 in ⊢ (??%?); @refl
963               |5: @plus_one @refl | *: skip ]
964    | <(E0_right tr) /3/ ]| /4/ ]| skip ]| skip ]
965  | % [2: % [2: % [ % [
966    @plus_succ [4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?);
967                   whd in ⊢ (??%?); >label_expr_type >EX2 in ⊢ (??%?); @refl
968    | 5: @plus_succ [4: @refl
969    | 5: @plus_one @refl | *: skip ] | *: skip ]
970    | <(E0_right tr) /3/ ]| /3/ ]| skip ]| skip ]
971  ]
972| #f #ua #a #us #s #cs #cpost #k #k' #e #m #K #EX
973  whd in EX:(??%%); destruct
974  % [2: % [2: % [ % [
975    @plus_succ [4: % | 5: @plus_one % | *: skip ]
976    | /2/ ]| /4/ ]| skip ]| skip ]
977| #f #ua2 #a2 #us3 #s3 #us #s #cs #cpost #k #k' #e #m #K #EX
978  cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
979  cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX
980  whd in EX:(??%%); destruct
981  cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 ua2) #tr1' * #EX1' #T1
982  [ % [2: % [2: % [ % [
983    @plus_succ [ 4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?);
984                    whd in ⊢ (??%?); >label_expr_type >EX2 in ⊢ (??%?); @refl
985    | 5: whd in ⊢ (??(??%%??)??); @plus_one @refl
986    | *: skip ]| <(E0_right tr) /3/ ] | /4/ ]| skip ]| skip ]
987  | % [2: % [2: % [ % [
988    @plus_succ [ 4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?);
989                    whd in ⊢ (??%?); >label_expr_type >EX2 in ⊢ (??%?); @refl
990    | 5: whd in ⊢ (??(??%%??)??); @plus_succ [4: @refl
991    | 5: @plus_one @refl ]| *: skip ]| <(E0_right tr) /3/ ]| /3/ ]| skip ]| skip
992    ]
993  ]
994| *
995  [ #f #args #k #k' #m #K whd in ⊢ (??%? → ?); @pair_elim #e #m1 #EX1 #EX
996    cases (bindIO_inversion ??????? EX) -EX #m2 * #EX2 #EX
997    whd in EX:(??%%); destruct
998    whd in match (label_fundef ?);
999    whd in match (label_function ?);
1000    lapply (refl ? (label_function f)) whd in ⊢ (???% → ?);
1001    @label_gen_elim #u1 @label_gen_elim #u2 >shift_fst #Ef
1002    % [2: % [2: % [ % [ @plus_succ [4: whd in ⊢ (??%?); >EX1 in ⊢ (??%?);
1003      whd in ⊢ (??%?); >EX2 in ⊢ (??%?); @refl
1004    | 5: @plus_one @refl | *: skip ] | /2/ ]| <Ef @swl_partial @swl_state @K ]| skip ]| skip ]
1005  | #id #tys #ty #args #k #k' #m #K #EX
1006    cases (bindIO_inversion ??????? EX) -EX #vs * #EX1 #EX
1007    cases (bindIO_inversion ??????? EX) -EX #ety * #EX2 #EX
1008    whd in EX2:(??%%); destruct
1009  ]
1010| #res #k #k' #m #K #EX inversion K
1011  [ #E1 #E2 #E3 destruct cases res in EX ⊢ %;
1012    [ 2: * #i #EX whd in EX:(??%?); destruct
1013    | *: normalize #A try #B try #C destruct
1014    ]
1015    % [2: % [2: % [ % [ @plus_one @refl | // ]| /2/ ]| skip ]| skip ]
1016  | 9: #r #f #en #k0 #k0' #K' #_ #E1 #E2 #E3 destruct cases r in EX ⊢ %;
1017    [ #EX whd in EX:(??%?); destruct
1018      % [2: % [2: % [ % [ @plus_one @refl | // ]| /3/ ]| skip ]| skip ]
1019    | * * #b #o #ty #EX
1020      cases (bindIO_inversion ??????? EX) -EX #m2 * #EX1 #EX
1021      whd in EX:(??%%); destruct
1022      % [2: % [2: % [ % [ @plus_one whd in ⊢ (??%?); >EX1 in ⊢ (??%?); @refl | // ]| /3/ ]| skip ]| skip ]
1023    ]
1024  | *: #A #B #C #D #E #F #G try #H try #I try #J try #L try #M try #N try #O
1025       destruct whd in EX:(??%?); destruct
1026  ]
1027| #r #EX whd in EX:(??%%); destruct
1028] qed.
1029
1030
1031theorem step_with_labels : ∀ge,ge'.
1032  related_globals … label_fundef ge ge' →
1033  ∀s1,s1',tr,s2.
1034  state_with_labels s1 s1' →
1035  (exec_step ge s1 = Value … 〈tr,s2〉 →
1036   ∃tr',s2'. plus ge' s1' tr' s2' ∧
1037             trace_with_extra_labels tr tr' ∧
1038             state_with_labels s2 s2').
1039#ge #ge' #RG #Xs1 #Xs1' #tr #s2 *
1040[ #s1 #s1' @step_with_labels_partial //
1041| #f #u *
1042(* If we have LSdefault we need to smuggle the execution of the cost label in
1043   before the actual statement. *)
1044  [ #s #k #k' #e #m #K #EX
1045    whd in EX:(??(??(??%???))?);
1046    whd in match (label_lstatements ??); @label_gen_elim #u1 @label_gen_elim #u2
1047    >shift_fst whd in match (seq_of_labeled_statement ?);
1048    cases (step_with_labels_partial … RG (State f s k e m) (State (label_function f) (\fst (label_statement s u)) k' e m) tr s2 (swl_state … K) EX)
1049    #tr' * #s2' * * #P #T #S
1050    % [2: % [2: % [ % [ @plus_succ [4: @refl | 5: @P | *: skip ] | /2/ ]| @S ]| skip ]| skip ]
1051(* but for LScase it's just like the cases in step_with_labels_partial *)
1052  | #sz #i #s #ls #k #k' #e #m #K #EX
1053    whd in EX:(??(??(??%???))?);
1054    whd in match (label_lstatements ??); @label_gen_elim #u1 @label_gen_elim #u2
1055    @label_gen_elim #u3 >shift_fst whd in match (seq_of_labeled_statement ?);
1056    whd in EX:(??%?); destruct
1057    % [2: % [2: % [ % [ @plus_succ [4: @refl | 5: @plus_one @refl | *: skip ] | /2/ ]| /4/ ]| skip ]| skip ]
1058  ]   
1059] qed.
1060
1061
1062lemma exec_step_interaction:
1063  ∀ge,s,o,k. exec_step ge s = Interact … o k  →
1064  ∃f,argtys,retty,vargs,k',m. s = Callstate (CL_External f argtys retty) vargs k' m.
1065#ge #s cases s
1066[ #f #st #kk #e #m #o #k #EX @⊥ cases st in EX ⊢ %;
1067  [ 11,14: #a | 2,4,6,7,12,13,15: #a #b | 3,5: #a #b #c | 8: #a #b #c #d ]
1068  whd in ⊢ (??%? → ?);
1069  [ 4,6,8,9: #EX destruct ]
1070  [ cases a
1071    [ whd in ⊢ (??%? → ?); cases (fn_return f) normalize #A try #B try #C try #D destruct
1072    | #a' whd nodelta in ⊢ (??%? → ?); cases (type_eq_dec (fn_return f) Tvoid)
1073      #x whd in ⊢ (??%? → ?); [2: cases (exec_expr ????) #y ] #EX whd in EX:(??%?); destruct
1074    ]
1075  | cases (find_label a (fn_body f) (call_cont kk)) [ 2: * #x #y ] #EX whd in EX:(??%?); destruct
1076  | @bindIO_res_interact #l #El @bindIO_res_interact #vt #Evt @bindIO_opt_interact #m' #Em #EX whd in EX:(??%?); destruct
1077  | 4,7: @bindIO_res_interact #x1 #x2 @bindIO_res_interact #x3 #x4 #EX whd in EX:(??%?); destruct
1078  | @bindIO_res_interact * * normalize #A #B #C try #D try #E destruct
1079  | @bindIO_res_interact #x1 #x2 @bindIO_res_interact #x3 #x4 @bindIO_opt_interact #x5 #x6 @bindIO_res_interact #x7 #x8 cases a
1080      [ 2: #x9 @bindIO_res_interact #x10 #x11 ] #EX whd in EX:(??%?); destruct
1081  | cases (is_Sskip a) #H [ @bindIO_res_interact #vt #Evt @bindIO_res_interact #v #Ev ] #EX whd in EX:(??%?); destruct
1082  | 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
1083    | 2,3,5,6,7: normalize #A #B try #C try #D try #E destruct
1084    | #z1 #z2 #z3 @bindIO_res_interact #x1 #x2 @bindIO_res_interact #x3 #x4 cases x3 #EX whd in EX:(??%?); destruct ]
1085  | cases kk normalize #A try #B try #C try #D try #E destruct
1086  | cases kk [ 4: #z1 #z2 #z3 @bindIO_res_interact #x1 #x2 @bindIO_res_interact #x3 #x4 cases x3 #EX whd in EX:(??%?); destruct
1087    | *: normalize #A try #B try #C try #D try #E destruct
1088    ]
1089  ]
1090| #f #args #kk #m #o #k cases f
1091  [ #f' whd in ⊢ (??%? → ?); cases (exec_alloc_variables empty_env m (fn_params f'@fn_vars f'))
1092    #x1 #x2 @bindIO_res_interact #m #Em #EX whd in EX:(??%?); destruct
1093  (* This is the only case that actually matters! *)
1094  | #fn #argtys #rty whd in ⊢ (??%? → ?);
1095    @bindIO_res_interact #vs #Evs
1096    #EX whd in EX:(??%?); destruct
1097    %{fn} %{argtys} %{rty} %{args} %{kk} %{m} %
1098  ]
1099| #v #kk #m #o #k whd in ⊢ (??%? → ?); cases kk
1100    [ cases v [2: * ] normalize #A try #B destruct
1101    | 8: #x1 #x2 #x3 #x4 cases x1
1102      [ whd in ⊢ (??%? → ?); #EX destruct | #x5 whd in ⊢ (??%? → ?); cases x5
1103          #x6 #x7 @bindIO_opt_interact #m' #Em #EX whd in EX:(??%?); destruct ]
1104    | *: normalize #A try #B try #C try #D try #E destruct ]
1105| #r #o #k #EX whd in EX:(??%?); destruct
1106] qed.
1107
1108lemma state_with_labels_call : ∀f,a,k,m,s1.
1109 state_with_labels (Callstate f a k m) s1 →
1110 ∃k'. cont_with_labels k k' ∧ s1 = Callstate (label_fundef f) a k' m.
1111#f #a #k #m #s1 #S inversion S
1112[ #s #s' #S' #E1 #E2 #E3 destruct inversion S'
1113  [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 destruct
1114  | #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 destruct
1115  | #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 destruct
1116  | #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 #H60 #H61 destruct
1117  | #f' #a' #k' #k'' #m' #K #E1 #E2 #E3 destruct %{k''} % //
1118  | #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 destruct
1119  | #H72 #H73 #H74 #H75 destruct
1120  ]
1121| #H77 #H78 #H79 #H80 #H81 #H82 #H83 #H84 #H85 #H86 #H87 destruct
1122] qed.
1123
1124lemma interactive_step_with_labels : ∀ge,ge'.
1125  related_globals … label_fundef ge ge' →
1126  ∀s1,s1',o,k.
1127  exec_step ge s1 = Interact … o k →
1128  state_with_labels s1 s1' →
1129  ∃k'.
1130      exec_step ge' s1' = Interact … o k' ∧
1131  ∀i. ∃tr,s2.
1132    k i = Value … 〈tr,s2〉 ∧
1133    ∃tr',s2'.
1134      k' i = Value … 〈tr',s2'〉 ∧
1135      trace_with_extra_labels tr tr' ∧
1136      state_with_labels s2 s2'.
1137#ge #ge' #RG #s1 #s1' #o #k #EX
1138cases (exec_step_interaction … EX)
1139#fn * #argtys * #retty * #vargs * #k' * #m #E
1140destruct
1141#S cases (state_with_labels_call … S)
1142#k'' * #K #E2 destruct
1143whd in EX:(??%?);
1144@(bindIO_res_interact ?????????? EX) -EX
1145#vs #CHECK #EX whd in EX:(??%?); destruct
1146% [2: %
1147[ whd in ⊢ (??%?);
1148  >CHECK in ⊢ (??%?);
1149  whd in ⊢ (??%?);
1150  @refl
1151| #i
1152  % [2: % [2: %
1153  [ @refl
1154  | % [2: % [ 2: % [ %
1155    [ @refl
1156    | // ]
1157    | /3/ ]
1158    | skip ]| skip ]
1159  ]| skip ]| skip ]
1160]| skip
1161] qed.
1162
1163
1164lemma initial_state_in_simulation : ∀p,s.
1165  make_initial_state p = OK ? s →
1166  ∃s'. make_initial_state (clight_label p) = OK ? s' ∧ state_with_labels s s'.
1167* #vars #fns #main #s
1168whd in ⊢ (??%? → ?); letin ge ≝ (make_global ?) #EX
1169cases (bind_inversion ????? EX) -EX #m * #Em #EX
1170cases (bind_inversion ????? EX) -EX #b * #Emain #EX
1171cases (bind_inversion ????? EX) -EX #fd * #Emain' #EX
1172whd in EX:(??%%); destruct
1173whd in match (make_initial_state ?);
1174letin ge' ≝ (make_global ?)
1175cut (related_globals … label_fundef ge ge')
1176[ // ] #RG
1177% [2: %
1178[ whd in ⊢ (??%?);
1179  change with (transform_program ??? (mk_program …) (λ_.label_fundef)) in match (mk_program ??? (transf_program ????) ?);
1180  >init_mem_transf >Em in ⊢ (??%?);
1181  whd in ⊢ (??%?); <(rg_find_symbol … RG) >Emain in ⊢ (??%?);
1182  whd in ⊢ (??%?); >(rg_find_funct_ptr … RG … Emain')
1183  whd in ⊢ (??%?); @refl
1184| /3/
1185] | skip ]
1186qed.
1187 
1188
1189
1190lemma not_wrong_init : ∀p.
1191  not_wrong (exec_inf … clight_fullexec p) →
1192  ∃s. make_initial_state … p = OK ? s.
1193#p whd in ⊢ (?% → ?); change with (make_initial_state p) in match (make_initial_state ??? p);
1194cases (make_initial_state p)
1195[ /2/
1196| normalize #m #NW @⊥
1197  inversion NW #H1 #H2 #H3 #H4 try #H5 destruct
1198] qed.
1199
1200lemma final_related : ∀s1,s2.
1201  state_with_labels s1 s2 →
1202  is_final s1 = is_final s2.
1203#s1x #s2x *
1204[ #s1y #s2y * //
1205| //
1206] qed.
1207
1208lemma plus_not_final : ∀ge,s,tr,s'.
1209  plus ge s tr s' →
1210  is_final s = None ?.
1211#ge #s0 #tr0 #s0' *
1212[ #s1 #tr #s2 #EX | #s1 #tr #s2 #tr' #s3 #EX #PL ]
1213lapply (refl ? (is_final s1))
1214cases (is_final s1) in ⊢ (???% → %);
1215//
1216#r cases s1 in EX ⊢ %;
1217#H9 #H10 #H11 try #H12 try #H13 try #H14 try #H15
1218[ 1,5: whd in H15:(??%?); | 2,6: whd in H14:(??%?); | 3,7: whd in H13:(??%?); | 4,8: whd in H11:(??%?); ]
1219destruct
1220normalize in H10;
1221destruct
1222qed.
1223
1224lemma plus_exec : ∀ge,s,tr,s'.
1225  plus ge s tr s' →
1226  is_final s' = None ? →
1227  steps tr (exec_inf_aux … clight_fullexec ge (exec_step ge s))
1228           (exec_inf_aux … clight_fullexec ge (exec_step ge s')).
1229#ge #s0 #tr0 #s0' #P elim P
1230[ #s1 #tr #s2 #EX #NF >EX >exec_inf_aux_unfold
1231  whd in ⊢ (??%?);
1232  whd in match (is_final ?????); >NF
1233  %2
1234| #s1 #tr #s2 #tr' #s3 #EX1 #P2 #IH #NF
1235  >exec_inf_aux_unfold >EX1
1236  whd in ⊢ (??%?);
1237  whd in match (is_final ?????); >(plus_not_final … P2)
1238  %3 @IH //
1239] qed.
1240
1241lemma plus_exec_final : ∀ge,s,tr,s',r.
1242  plus ge s tr s' →
1243  is_final s' = Some ? r →
1244  ∃tr'. steps tr (exec_inf_aux … clight_fullexec ge (exec_step ge s))
1245                 (e_stop … tr' r s').
1246#ge #s0 #tr0 #s0' #r #P elim P
1247[ #s1 #tr #s2 #EX #F >EX >exec_inf_aux_unfold
1248  %{tr} whd in ⊢ (??%?);
1249  whd in match (is_final ?????); >F
1250  %1
1251| #s1 #tr #s2 #tr' #s3 #EX1 #P2 #IH #F
1252  cases (IH … F)
1253  #tr' #S' %{tr'}
1254  >exec_inf_aux_unfold >EX1
1255  whd in ⊢ (??%?);
1256  whd in match (is_final ?????); >(plus_not_final … P2)
1257  %3 @S'
1258] qed.
1259
1260let corec build_exec
1261  (ge1,ge2:genv)
1262  (RG:related_globals … label_fundef ge1 ge2)
1263  (s1,s2:state)
1264  (S:state_with_labels s1 s2)
1265  (NW:not_wrong (exec_inf_aux … clight_fullexec ge1 (exec_step ge1 s1)))
1266: sim_with_labels (exec_inf_aux … clight_fullexec ge1 (exec_step ge1 s1)) (exec_inf_aux … clight_fullexec ge2 (exec_step ge2 s2)) ≝
1267match NW return λe,NW. exec_inf_aux … clight_fullexec ?? = e → sim_with_labels e ? with
1268[ nw_stop tr i s ⇒ ?
1269| nw_step tr1 s1' e1 NW1 ⇒ ?
1270| nw_interact o k NWk ⇒ ?
1271] (refl ? (exec_inf_aux … clight_fullexec ge1 (exec_step ge1 s1))).
1272[ #E1
1273  cases (exec_inf_stops_at_final ?? clight_fullexec … E1)
1274  #EX1 #F1
1275  cases (step_with_labels … RG … S EX1)
1276  #tr2 * #s2' * * #PL #TWL #S'
1277  lapply F1 whd in ⊢ (??%? → ?); >(final_related … S') #F2
1278  cases (plus_exec_final ????? PL F2)
1279  #tr2' #S2
1280  @(swl_stop … S2 TWL)
1281| #E1
1282  cases (extract_step ?? clight_fullexec … E1)
1283  #EX1 #E1'
1284  cases (step_with_labels … RG … S EX1)
1285  #tr2 * #s2' * * #EX2 #TR #S' (*>E1' in NW1 ⊢ %; #NW1*)
1286  @(swl_steps … (plus_exec … EX2 ?))
1287  [ <(final_related … S') @(exec_e_step_not_final ?? clight_fullexec … E1)
1288  | //
1289  | (* Manual rewrite to prevent guardedness condition getting upset. *)
1290    @(match sym_eq … E1' return λe,E1'. sim_with_labels e ? with [refl ⇒ ?])
1291    @build_exec // >E1' in NW1; //
1292  ]
1293| #E1
1294  cases (extract_interact ?? clight_fullexec … E1)
1295  #k' * #EX1 #Ek lapply NWk -NWk @(match sym_eq … Ek with [refl ⇒ ?]) #NWk
1296  cases (interactive_step_with_labels … RG … EX1 S)
1297  #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 ⊢ (??%);
1298  @swl_interact
1299  #i cases (H2 i) #tr1 * #s1' * #K1 * #tr2 * #s2' * * #K2 #TR #S'
1300  lapply (NWk i)
1301  @(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 ⇒ ?])
1302  @(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 ?????);
1303  cases (is_final s2')
1304  [ whd in ⊢ (?% → ?%%); #NW' @(swl_steps … (steps_step …)) // @build_exec //
1305    inversion NW'
1306    [ #H1 #H2 #H3 #H4 #H5 destruct
1307    | #H7 #H8 #H9 #H10 #H11 #H12 destruct //
1308    | #H14 #H15 #H16 #H17 #H18 destruct
1309    ]
1310  | #r whd in ⊢ (?% → ?%%); #NW' @(swl_stop … (steps_stop …)) //
1311  ]
1312] qed.
1313
1314lemma initial_state_is_not_final : ∀p,s.
1315  make_initial_state p = OK ? s →
1316  is_final s = None ?.
1317* #vars #fns #main #s
1318whd in ⊢ (??%? → ?); letin ge ≝ (make_global ?) #EX
1319cases (bind_inversion ????? EX) -EX #m * #Em #EX
1320cases (bind_inversion ????? EX) -EX #b * #Emain #EX
1321cases (bind_inversion ????? EX) -EX #fd * #Emain' #EX
1322whd in EX:(??%%); destruct //
1323qed.
1324
1325
1326theorem labelling_sim : labelled_exec_is_equiv.
1327whd (* let's remind ourselves of the spec *)
1328#p
1329#NW
1330cases (not_wrong_init p NW)
1331#s1 #I1
1332cases (initial_state_in_simulation … I1)
1333#s2 * #I2
1334
1335whd in match (exec_inf ?? clight_fullexec p) in NW ⊢ %;
1336letin ge1 ≝ (make_global ?? clight_fullexec p) in NW ⊢ %;
1337change with (make_initial_state p) in match (make_initial_state ?? clight_fullexec p);
1338>I1
1339
1340whd in match (exec_inf ????);
1341letin ge2 ≝ (make_global ?? clight_fullexec (clight_label p))
1342change with (make_initial_state (clight_label p)) in match (make_initial_state ?? clight_fullexec (clight_label p));
1343>I2
1344
1345whd in ⊢ (?% → ? → ?%%);
1346>exec_inf_aux_unfold
1347>exec_inf_aux_unfold
1348whd in ⊢ (?% → ? → ?%%);
1349whd in match (is_final ?????);
1350>(initial_state_is_not_final … I1)
1351whd in match (is_final ?????);
1352>(initial_state_is_not_final … I2)
1353whd in ⊢ (?% → ? → ?%%);
1354
1355#NW #S
1356@(swl_steps E0 E0)
1357[ 2: @steps_step | skip | // | @build_exec
1358  [ @transform_program_related | // | inversion NW
1359    [ #tr #i #s #E1 #E2 destruct
1360    | #trX #sX #eX #NWX #E1X #E2X destruct //
1361    | #H1 #H2 #H3 #H4 #H5 destruct
1362    ]
1363  ]
1364] qed.
1365
1366
1367
Note: See TracBrowser for help on using the repository browser.