source: src/Clight/labelSimulation.ma @ 2392

Last change on this file since 2392 was 2392, checked in by campbell, 7 years ago
Labelling translations of && and
need a lot of cost labelling to meet

criteria.

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