source: src/Clight/labelSimulation.ma @ 2145

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

Cost labelling doesn't affect interaction.

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