source: src/Clight/labelSimulation.ma @ 2588

Last change on this file since 2588 was 2588, checked in by garnier, 7 years ago

modified Cexec/Csem? semantics:
. force andbool and orbool types to be Tint sz sg, fail otherwise
. cast result of evaluation to (bitvector sz)
. in lvalue evaluation, field offset for structs is now 16 bit instead of 32
/!\ induction principles modified accordingly
. soundness and correctness adapted

modified label/labelSimulation:
. andbool and orbool are modified so that the true/false constants are

casted to the (integer) type of the enclosing expression, to match
Csem/Cexec?. If the type is not an integer, default on 32 bits.

. labelSimulation proof adapted to match changes.

proof of simulation for expressions Cl to Cm finished
. caveat : eats up all my RAM (8gb) when using matita (not matitac), barely typecheckable
. moved some lemmas from toCminorCorrectness.ma to new file toCminorOps.ma

and frontend_misc.ma to alleviate this, to no avail - more radical splitting required ?

slight modification in SimplifyCasts? to take into account modifications in semantics,
removed some duplicate lemmas and replaced them by wrappers to avoid breaking the
rest of the development.

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