source: src/Clight/labelSimulation.ma @ 2486

Last change on this file since 2486 was 2468, checked in by garnier, 8 years ago

Floats are gone from the front-end. Some trace amount might remain in RTL/RTLabs, but this should be easily fixable.
Also, work-in-progress in Clight/memoryInjections.ma
File size: 54.1 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: 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  [ 3: #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  [ 6: #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  | 7: #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,ls',u.
395    select_switch sz i ls = Some ? ls' →
396  ∃u'.
397    select_switch sz i (\fst (label_lstatements ls u)) =
398    Some ? (\fst (label_lstatements ls' u')).
399#sz #i #ls @(labeled_statements_ind … ls)
400[ #s #ls' #u #S normalize in S; destruct
401  % [2: whd in match (label_lstatements ??);
402  @label_gen_elim #u1 >shift_fst @refl | skip ]
403| #sz' #i' #s #tl #IH #ls' #u
404  whd in ⊢ (??%? → ?); @intsize_eq_elim_elim [ #NE #E destruct ]
405  #E destruct whd @eq_bv_elim
406  [ #E' destruct #S whd in S:(??%%); destruct
407    % [2: whd in match (label_lstatements ??);
408    @label_gen_elim #u1 @label_gen_elim #u2 @label_gen_elim #u3
409    whd in ⊢ (??%%); >intsize_eq_elim_true >eq_bv_true %
410    | skip ]
411  | #NE #S whd in S:(??%?);
412    whd in match (label_lstatements ??); 
413    @label_gen_elim #u1 @label_gen_elim #u2 @label_gen_elim #u3
414    whd in match (select_switch ?? (LScase ????));
415    >intsize_eq_elim_true >(eq_bv_false … NE)
416    @IH assumption
417  ]
418] qed.
419
420(* Break up labelling function in one go for statements. *)
421lemma blindly_label : ∀u,s. ∀P:statement → Prop.
422match s with
423[ Sskip ⇒ P Sskip
424| Sassign e1 e2 ⇒ ∀u1,u2. P (Sassign (\fst (label_expr e1 u1)) (\fst (label_expr e2 u2)))
425| 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)))
426| Ssequence s1 s2 ⇒ ∀u1,u2. P (Ssequence (\fst (label_statement s1 u1)) (\fst (label_statement s2 u2)))
427| 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))))
428| 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))
429| 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))
430| 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))
431| Sbreak ⇒ P Sbreak
432| Scontinue ⇒ P Scontinue
433| Sreturn eo ⇒ ∀u1. P (Sreturn (\fst (label_opt_expr eo u1)))
434| Sswitch e ls ⇒ ∀u1,u2. P (Sswitch (\fst (label_expr e u1)) (\fst (label_lstatements ls u2)))
435| Slabel l s1 ⇒ ∀u1,cs. P (Slabel l (Scost cs (\fst (label_statement s1 u1))))
436| Sgoto l ⇒ P (Sgoto l)
437| Scost c s1 ⇒ ∀u1. P (Scost c (\fst (label_statement s1 u1)))
438] → P (\fst (label_statement s u)). 
439#u * // #A #B #C try #D try #E try #F whd in match (label_statement ??);
440@label_gen_elim #u1 //
441@label_gen_elim #u2 //
442[ 6: >shift_fst //
443| *: @label_gen_elim #u3 //
444     @label_gen_elim #u4
445     [ @label_gen_elim #u5 >shift_fst >shift_fst //
446     | 2,3: >shift_fst >shift_fst //
447     | @label_gen_elim #u5 >shift_fst >shift_fst >shift_fst //
448     ]
449] qed.
450
451(* Apply induction hypothesis in label_find_label proof below while getting
452   Matita to infer the continuations k0 and k0', and the universe u0, rather
453   than having to give them explicitly. *)
454lemma lfl_IH : ∀s0,lbl.
455  ∀C:option (statement×cont) → option (statement×cont) → Prop.
456  ∀IH:cont → cont → universe CostTag → Prop.
457  (∀k,k',u. cont_with_labels k k' → IH k k' u) →
458  ∀k0,k0',u0. cont_with_labels k0 k0' →
459   (IH k0 k0' u0 →
460    C (find_label lbl s0 k0) (find_label lbl (\fst (label_statement s0 u0)) k0')) →
461   C (find_label lbl s0 k0) (find_label lbl (\fst (label_statement s0 u0)) k0').
462/3/
463qed.
464
465(* Finding a goto label in a cost-labelled program gives a labelled version of
466   the statement and continuation found by the original function, if any. *)
467lemma label_find_label : ∀lbl,s,k,k',u.
468  cont_with_labels k k' →
469  match find_label lbl s k with
470  [ Some r' ⇒ let 〈s1,k1〉 ≝ r' in
471    ∃u',cs,k1'.
472    find_label lbl (\fst (label_statement s u)) k' = Some ? 〈Scost cs (\fst (label_statement s1 u')), k1'〉 ∧
473    cont_with_labels k1 k1'
474  | None ⇒ find_label lbl (\fst (label_statement s u)) k' = None ?
475  ].
476#lbl #s @(statement_ind2 ? (λls.
477  ∀k,k',u.
478  cont_with_labels k k' →
479  match find_label_ls lbl ls k with
480  [ Some r' ⇒ let 〈s1,k1〉 ≝ r' in
481    ∃u',cs,k1'.
482    find_label_ls lbl (\fst (label_lstatements ls u)) k' = Some ? 〈Scost cs (\fst (label_statement s1 u')), k1'〉 ∧
483    cont_with_labels k1 k1'
484  | None ⇒ find_label_ls lbl (\fst (label_lstatements ls u)) k' = None ?
485  ])
486 … s)
487[ #k #k' #u #F @refl
488| #e1 #e2 #k #k' #u #K @blindly_label #u1 #u2 whd @refl
489| #e0 #e #args #k #k' #u #K @blindly_label #u1 #u2 #u3 whd @refl
490| #sA #sB #IH1 #IH2 #k #k' #u #K @blindly_label #u1 #u2 whd in match (find_label ???);
491  whd in match (find_label ?? k');
492  @(lfl_IH sA … IH1) [ /2/ ]
493  cases (find_label ???)
494  [ whd in ⊢ (% → match % with [_⇒?|_⇒?]); #FIND1'
495    @(lfl_IH … IH2) [ // ]
496    cases (find_label ???)
497    [ whd in ⊢ (% → %); #FIND2' whd in ⊢ (??%?); >FIND1' >FIND2' @refl
498    | * #s3 #k3 whd in ⊢ (% → %); * #u3 * #cs * #k1' * #FIND2' #K1'
499      % [2: %{cs} %{k1'} % // whd in ⊢ (??%?); >FIND1' in ⊢ (??%?); >FIND2' in ⊢ (??%?); @refl | skip ]
500    ]
501  | * #sA' #kA' whd in ⊢ (% → %);
502    * #u1' * #cs * #k1' * #FA' #K'
503         % [2: %{cs} %{k1'} % [ whd in ⊢ (??%?); >FA' in ⊢ (??%?); @refl | // ] |skip]
504  ]
505| #e #s1 #s2 #IH1 #IH2 #k #k' #u @blindly_label #u1 #u2 #u3 #c2 #c3 #K
506  whd in match (find_label ?? k); whd in match (find_label ?? k');
507  whd in match (find_label ?? k');
508  @(lfl_IH  … IH1) [ // ] cases (find_label ???)
509  [ whd in ⊢ (% → match % with [_⇒?|_⇒?]); #FIND1'
510    lapply (IH2 k k' u3 K) cases (find_label ???)
511    [ whd in ⊢ (% → %); #FIND2'
512      whd in match (find_label ???); >FIND1'
513      whd in match (find_label ???); >FIND2' @refl
514    | * #s2' #k2' * #u4 * #cs * #k1' * #FIND2' #K2'
515      % [2: % [2: % [2: % [ whd in ⊢ (??%?);
516      whd in match (find_label ???); >FIND1' in ⊢ (??%?);
517      whd in match (find_label ???); >FIND2' in ⊢ (??%?); @refl
518      | // ]|skip]|skip]|skip]
519    ]
520  | * #s1' #k1 whd in ⊢ (% → %); * #u4 * #cs * #k1' * #FIND1' #K1'
521    % [2: % [2: % [2: % [
522      whd in ⊢ (??%?); whd in match (find_label ???); >FIND1' in ⊢ (??%?);
523      @refl | // ] |skip ]| skip ]| skip ]
524  ]
525| #e #s0 #IH #k #k' #u #K @blindly_label #u1 #u2 #cs #cpost
526  whd in match (find_label ?? k); normalize in match (find_label ?? k');
527  @(lfl_IH s0 … IH) [ /2/ ]
528  cases (find_label ???)
529  [ whd in ⊢ (% → %); #FIND1'
530    whd in ⊢ (??%?); whd in match (find_label ???); >FIND1' @refl
531  | * #s1 #k1 * #u4 * #cs * #k1' * #FIND1' #K1'
532    % [2: % [2: % [2: % [
533      whd in ⊢ (??%?); whd in match (find_label ???); >FIND1' in ⊢ (??%?);
534      @refl | // ]| skip ]| skip ]| skip ]
535  ]
536| #e #s0 #IH #k #k' #u #K @blindly_label #u1 #u2 #cs #cpost
537  whd in match (find_label ?? k); normalize in match (find_label ?? k');
538  @(lfl_IH s0 … IH) [ /2/ ]
539  cases (find_label ???)
540  [ whd in ⊢ (% → %); #FIND1'
541    whd in ⊢ (??%?); whd in match (find_label ???); >FIND1' @refl
542  | * #s1 #k1 * #u4 * #cs * #k1' * #FIND1' #K1'
543    % [2: % [2: % [2: % [
544      whd in ⊢ (??%?); whd in match (find_label ???); >FIND1' in ⊢ (??%?);
545      @refl | // ]| skip ]| skip ]| skip ]
546  ]
547| #s1 #e #s2 #s3 #IH1 #IH2 #IH3 #k #k' #u #K @blindly_label #u1 #u2 #u3 #u4 #c3 #c4
548  whd in match (find_label ???); normalize in match (find_label ?? k');
549  @(lfl_IH s1 … IH1) [ /2/ ]
550  cases (find_label ???)
551  [ whd in ⊢ (% → match % with [_⇒?|_⇒?]); #FIND1' >FIND1'
552    @(lfl_IH s3 … IH3) [ /2/ ]
553    cases (find_label ???)
554    [ whd in ⊢ (% → match % with [_⇒?|_⇒?]); #FIND3' >FIND3'
555      @(lfl_IH s2 … IH2) [ /2/ ]
556      cases (find_label ???)
557      [ whd in ⊢ (% → %); #FIND2' >FIND2' @refl
558      | * #s2' #k2' * #u2' * #cs' * #k1' * #FIND2' #K2'
559        % [2: % [2: % [2: % [
560         whd in ⊢ (??%?); >FIND2' in ⊢ (??%?); @refl
561        | // ]| skip ]| skip ]| skip ]
562      ]
563    | * #s3' #k3' * #u3' * #cs' * #k1' * #FIND3' #K3'
564        % [2: % [2: % [2: % [
565        >FIND3' in ⊢ (??%?); whd in ⊢ (??%?); @refl
566        | // ]| skip ]| skip ]| skip ]
567    ]
568  | * #s1' #k1' * #u1' * #cs' * #k1' * #FIND1' #K1'
569        % [2: % [2: % [2: % [
570        >FIND1' in ⊢ (??%?); whd in ⊢ (??%?); @refl
571        | // ]| skip ]| skip ]| skip ]
572  ]
573| //
574| //
575| #eo #k #k' #u @blindly_label #u1 //
576| #e #ls #IH #k #k' #u #K @blindly_label #u1 #u2
577  normalize in match (find_label ???); normalize in match (find_label ???);
578  lapply (IH (Kswitch k) (Kswitch k') u2 ?) [/2/] cases (find_label_ls ???)
579  [ whd in ⊢ (% → %); //
580  | * #s1' #k1' * #u' * #cs * #k'' * #FIND' #K'
581    % [2: % [2: % [2: % [ @FIND' | // ]|skip ]|skip]|skip]
582  ]
583| #l #s0 #IH #k #k' #u #K @blindly_label #u1 #cs
584  whd in match (find_label ???); whd in match (find_label ?? k');
585  cases (ident_eq lbl l)
586  [ #E destruct whd
587    % [2: % [2: % [2: % [ @refl | // ]|skip ]|skip ]| skip ]
588  | #NE whd in ⊢ (match % with [_⇒?|_⇒?]);
589    normalize in match (find_label ?? k');
590    @(lfl_IH s0 … IH) [ // ]
591    cases (find_label ???)
592    [ //
593    | * #s0' #k0' * #u' * #cs0 * #k1' * #FIND0 #K0
594      % [2: % [2: % [2: % [ @FIND0 | // ]|skip ]|skip]|skip]
595    ]
596  ]
597| //
598| #l #s0 #IH #k #k' #u #K @blindly_label #u1 /2/
599| #s0 #IH #k #k' #u whd in match (label_lstatements ??);
600  @label_gen_elim #u1 >shift_fst >shift_fst
601  whd in match (find_label_ls ???); whd in match (find_label_ls ???);
602  @IH
603| #sz #i #s0 #tl #IH1 #IH2 #k #k' #u #K
604  whd in match (label_lstatements ??); @label_gen_elim #u1 @label_gen_elim #u2
605  @label_gen_elim #u3 >shift_fst
606  whd in match (find_label_ls ???); normalize in match (find_label_ls ?? k');
607  @(lfl_IH s0 … IH1) [ /2/ ]
608  cases (find_label ???)
609  [ whd in ⊢ (% → match % with [_⇒?|_⇒?]); #FIND0 >FIND0
610    lapply (IH2 k k' u2 K) cases (find_label_ls ???)
611    [ whd in ⊢ (% → %); #FINDtl >FINDtl @refl
612    | * #stl #ktl //
613    ]
614  | * #s0' #k0' whd in ⊢ (% → %);
615    * #u' * #cs * #k1' * #FIND0 #K0 >FIND0
616    % [2: % [2: % [2: % [ @refl | // ] | skip ] | skip ] | skip ]
617  ]
618] qed.
619
620lemma label_find_label_fn : ∀g,lbl,f,k,k',s1,k1.
621  cont_with_labels k k' →
622  find_label lbl (fn_body f) (call_cont k) = Some ? 〈s1,k1〉 →
623  ∃u',cs,k1'.
624    find_label lbl (fn_body (\fst (label_function g f))) (call_cont k') = Some ? 〈Scost cs (\fst (label_statement s1 u')), k1'〉 ∧
625    cont_with_labels k1 k1'.
626#g #lbl * #rty #args #vars #s #k #k' #s1 #k1 #K #FIND
627whd in match (label_function ??);
628@label_gen_elim #u1 @label_gen_elim #u2 >shift_fst
629lapply (label_find_label lbl s (call_cont k) (call_cont k') g ?)
630[ /2/ ]
631>FIND whd in ⊢ (% → ?); //
632qed.
633
634
635(* We show the main simulation in two stages.  First, we show it for all states
636   in the relation *except* those for labeled_statements, then we'll show the
637   whole thing.  This is so that we can appeal to the other cases in the proof
638   for labeled_statements. *)
639lemma step_with_labels_partial : ∀ge,ge'.
640  related_globals_gen … label_fundef ge ge' →
641  ∀s1,s1',tr,s2.
642  state_with_labels_partial s1 s1' →
643  exec_step ge s1 = Value … 〈tr,s2〉 →
644  ∃n. after_n_steps (S n) … clight_exec ge' s1'
645  (λtr',s2'.
646     trace_with_extra_labels tr tr' ∧
647     state_with_labels s2 s2').
648
649(* General plan is like the expressions result, except that we do case analysis
650   on the simulation first, then:  break up the original execution, break up the
651   cost labelling, use the earlier results to deal with expressions, then
652   run the labelled version for enough steps.  We try to avoid having to write
653   out the final trace and state and "skip" them afterwards. *)
654#ge #ge' #RG #Xs1 #Xs1' #tr #s2 *
655[ #g #f #us #s #k #k' #e #m #KL cases s
656  [ #EX inversion KL
657    [ #E1 #E2 #_ destruct
658      whd in EX:(??%?);
659      lapply (refl ? (fn_return f)) cases (fn_return f) in ⊢ (???% → ?);
660      [ #E >E in EX; whd in ⊢ (??%% → ?); #EX' destruct
661        %{0} whd whd in ⊢ (??%?);
662        >label_function_return >E whd % /3/
663      | *: #A [ 1,3,4,5,6: #B ] #E >E in EX; #EX whd in EX:(??%%); destruct
664      ]
665    | #u #s0 #k0 #k0' #K #_ #E1 #E2 #E3 destruct %{0} whd
666      whd in EX:(??%%); destruct /4/
667    | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct %{0}
668      whd in EX:(??%%); destruct whd /4/
669    | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct
670      cases (bindIO_inversion ??????? EX) -EX * #ve #tre * #EXe #EX
671      cases (bindIO_inversion ??????? EX) -EX * * #EXb #EX
672      normalize in EX; destruct
673      cases ((proj1 ?? (label_expr_ok ge ge' e m RG)) ??? EXe ue) #tre' * #EXe' #Te
674      [ %{0} whd
675        whd in ⊢ (??%?); >EXe'
676        whd in ⊢ (??%?); >label_expr_type >EXb
677        whd % /4/
678      | %{2} whd
679        whd in ⊢ (??%?); >EXe'
680        whd in ⊢ (??%?); >label_expr_type >EXb
681        whd % [ <(E0_right tr) @twel_app /2/ | /4/ ]
682      ]
683    | #ue #e0 #us1 #st1 #us2 #st2 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct
684      whd in EX:(??%?); destruct
685      %{0} whd /4/
686    | #ue #e0 #us1 #st1 #us2 #st2 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct
687      whd in EX:(??%?); destruct
688      %{0} % /4/
689    | #ue #e0 #us1 #st1 #us2 #st2 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct
690      whd in EX:(??%?); destruct
691      %{0} % /4/
692    | #k0 #k0' #K #_ #E1 #E2 #E3 destruct
693      whd in EX:(??%?); destruct
694      %{0} % /4/
695    | #u0 #r #f0 #en #k0 #k0' #K #_ #E1 #E2 #E3 destruct
696      whd in EX:(??%?);
697      lapply (refl ? (fn_return f)) cases (fn_return f) in ⊢ (???% → ?);
698      [ #E >E in EX; whd in ⊢ (??%? → ?); #EX destruct
699        %{0} whd whd in ⊢ (??%?); >label_function_return >E in ⊢ (??%?);
700        whd % /4/
701      | *: #A [ 1,3,4,5,6: #B ] #E >E in EX; #EX whd in EX:(??%%); destruct
702      ]
703    | #ls #u #k0 #k0' #K #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
704      %{0} % /4/
705    ]
706  | * #a1 #ty1 #a2 #EX
707    cases (bindIO_inversion ??????? EX) -EX * * #b1 #o1 #tr1 * #EX1 #EX
708    cases (bindIO_inversion ??????? EX) -EX * #v2 #tr2 * #EX2 #EX
709    cases (bindIO_inversion ??????? EX) -EX #m3 * #EX3 #EX
710    whd in EX:(??%%); destruct
711    @blindly_label #u1 #u2
712    cases (proj2 ?? (label_expr_ok ge ge' e m RG) ????? EX1 u1) #tr1' * #EX1' #T1
713    cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX2 u2) #tr2' * #EX2' #T2
714    %{0} whd
715    whd in ⊢ (??%?); >exec_lvalue_labelled >EX1'
716    whd in ⊢ (??%?); >EX2'
717    whd in ⊢ (??%?); >label_expr_type >EX3
718    whd % [ whd in ⊢ (??%); @twel_app // | /3/ ]
719  | * [2: * #er #tyr ] #ef #args #EX
720    cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
721    cases (bindIO_inversion ??????? EX) -EX * #args' #tr2 * #EX2 #EX
722    cases (bindIO_inversion ??????? EX) -EX #fd * #EX3 #EX
723    cases (bindIO_inversion ??????? EX) -EX #E4 * #EX4 #EX
724    whd in EX:(??%%);
725    [ cases (bindIO_inversion ??????? EX) -EX * * #b5 #o5 #tr5 * #EX5 #EX whd in EX:(??%%); ]
726    destruct
727    @blindly_label #u1 #u2 #u3
728    cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 u2) #tr1' * #EX1' #T1
729    cases (label_exprs_ok ge ge' RG e m args args' ? EX2 u3) #tr2' * #EX2' #T2
730    [ cases (proj2 ?? (label_expr_ok ge ge' e m RG) ????? EX5 u1) #tr5' * #EX5' #T5 ]
731    cases (opt_find_funct … RG … EX3) #ux #EFF
732    %{0} whd
733    whd in ⊢ (??%?); >EX1'
734    whd in ⊢ (??%?); >EX2'
735    whd in ⊢ (??%?); >EFF
736    whd in ⊢ (??%?); >label_fundef_typeof_fundef >label_expr_fun_typeof >EX4
737    whd in ⊢ (??%?); [ whd in match (label_opt_expr ??); @breakup_pair whd in ⊢ (??%?); >exec_lvalue_labelled >EX5' ]
738    whd % [ 1,3: whd in ⊢ (??%); @twel_app /2/ | *: @swl_partial @swl_callstate /2/ ]
739  | #st1 #st2 #EX
740    whd in EX:(??%%); destruct
741    whd in match (label_statement ??); @label_gen_elim #u1 @label_gen_elim #u2
742    %{0} % /4/
743  | #a #st1 #st2 #EX
744    cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
745    cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX
746    normalize in EX; destruct
747    whd in match (label_statement ??); @label_gen_elim #u1
748    @label_gen_elim #u2 @label_gen_elim #u3 @label_gen_elim #u4
749    @label_gen_elim #u5
750    whd in match (add_cost_before ??); cases (fresh ??) #c6 #u6
751    whd in match (add_cost_before ??); cases (fresh ??) #c7 #u7
752    cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1
753    %{1} whd
754    whd in ⊢ (??%?); >EX1'
755    whd in ⊢ (??%?); >label_expr_type >EX2
756    whd in ⊢ (??%?); % [1,3: <(E0_right tr) ] /4/
757  | #a #st #EX
758    cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
759    cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX
760    normalize in EX; destruct
761    whd in match (label_statement ??); @label_gen_elim #u1
762    @label_gen_elim #u2
763    whd in match (add_cost_before ??); cases (fresh ??) #c6 #u6
764    >shift_fst whd in match (add_cost_after ??); cases (fresh ??) #c7 #u7
765    >shift_fst
766    cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1
767    [ %{2} | %{3} ] whd
768    whd in ⊢ (??%?); >EX1'
769    whd in ⊢ (??%?); >label_expr_type >EX2
770    whd in ⊢ (??%?); % [ 1,3: <(E0_right tr) ] /5/
771  | #a #st #EX
772    normalize in EX; destruct
773    whd in match (label_statement ??); @label_gen_elim #u1
774    @label_gen_elim #u2
775    whd in match (add_cost_before ??); cases (fresh ??) #c6 #u6 >shift_fst
776    whd in match (add_cost_after ??); cases (fresh ??) #c7 #u7 >shift_fst
777    %{2} % /4/
778  | #st1 #a #st2 #st #EX
779    lapply (refl ? (is_Sskip st1)) cases (is_Sskip st1) in ⊢ (???% → ?); #Esk #Eskip
780    whd in EX:(??%?); >Eskip in EX; #EX
781    whd in match (label_statement ??); @label_gen_elim #u1
782    @label_gen_elim #u2 @label_gen_elim #u3 @label_gen_elim #u4
783    whd in match (add_cost_before ??); cases (fresh ??) #c5 #u5 >shift_fst
784    whd in match (add_cost_after ??); cases (fresh ??) #c6 #u6 >shift_fst
785    [ cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
786      cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX
787      normalize in EX; destruct
788      cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1
789      [ %{2} | %{3} ] whd
790      whd in ⊢ (??%?); >EX1'
791      whd in ⊢ (??%?); >label_expr_type >EX2
792      whd in ⊢ (??%?); % [ 1,3: <(E0_right tr) ] /4/
793    | whd in EX:(??%%); destruct
794      %{1} whd
795      whd in ⊢ (??%?); cases (labelled_is_not_skip ? u1 Esk) #Esk' #Eskip'
796      >Eskip' whd in ⊢ (??%?); % /4/
797    ]
798  | #EX inversion KL
799    [ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
800    |#u #s0 #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
801    | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
802    | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
803    | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
804    | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
805    | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
806    | #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
807    | #ux #r #f0 #en #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
808    | #ls #u #k0 #k0' #K #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
809    ]
810    whd in match (label_statement ??);
811    [ 1,6,7: %{0} % /3/
812    | 2,3,5: %{2} % /3/
813    | %{1} % /3/
814    ]
815  | #EX inversion KL
816    [ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
817    |#u #s0 #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
818    | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
819    | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
820    | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
821    | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
822    | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
823    | #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
824    | #g #r #f0 #en #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
825    | #ls #u #k0 #k0' #K #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
826    ]
827    whd in match (label_statement ??);
828    [ 1,2,5,6,7: %{0} % /4/
829    | 4: %{1} % /4/
830    | cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
831      cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX
832      normalize in EX; destruct
833      cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 ue) #tr1' * #EX1' #T1
834      [ %{0} | %{2} ] whd
835      whd in ⊢ (??%?); >EX1'
836      whd in ⊢ (??%?); >label_expr_type >EX2
837      whd in ⊢ (??%?); % [ 3: <(E0_right tr) ] /3/
838    ]
839  | * [2: #a ] #EX
840    whd in EX:(??%?); cases (type_eq_dec (fn_return f) Tvoid) in EX;
841    #Ety #EX whd in EX:(??%?);
842    [ destruct
843    | cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
844      cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1
845    | >Ety in EX; #EX
846    | @⊥ cases (fn_return f) in Ety EX;
847      [ * #H cases (H (refl ??))
848      | *: normalize #a #b #c try #d try #e destruct
849      ]
850    ]
851    whd in match (label_statement ??);
852    [ @label_gen_elim #u' whd in match (label_opt_expr ??); @label_gen_elim #u'' ]
853    whd in EX:(??%%); destruct
854    %{0} whd
855    whd in ⊢ (??%?);
856    [ >label_function_return @(dec_false ? (type_eq_dec ??) Ety) #Ety''
857      whd in ⊢ (??%?); >EX1'
858    | >label_function_return >Ety
859    ] whd in ⊢ (??%?); % /4/
860  | * #a #ty #ls #EX
861    cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
862    cases v1 in EX1 EX;
863    [ 2: #sz #i #EX1 #EX
864    | *: normalize #A #B try #C destruct
865    ]
866    whd in EX:(??%%); cases ty in EX1 EX ⊢ %; normalize nodelta #sz' try #sg try #EX1 try #EX destruct
867    cases (sz_eq_dec sz sz') in EX; #SZ #EX whd in EX:(??%%); destruct
868    cases (bindIO_inversion ??????? EX) -EX #ls' * #EXls #EX
869    whd in EX:(??%%); destruct
870    cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1
871    whd in match (label_statement ??); @label_gen_elim #u1 @label_gen_elim #u2
872    %{0} whd
873    whd in ⊢ (??%?); >EX1'
874    whd in ⊢ (??%?); >label_expr_type
875    whd in ⊢ (??%?); @(dec_true ? (sz_eq_dec sz' sz') (refl ??)) #SZ'
876    whd in ⊢ (??%?); cases (label_select_ls ????? EXls)
877    [ #u3 #Els' >Els' whd % /3/ | skip ]
878  | #l #st #EX
879    whd in EX:(??%?); destruct
880    whd in match (label_statement ??); @label_gen_elim #u1 >shift_fst
881    whd in match (add_cost_before ??); cases (fresh ??) #cs #u2 >shift_fst
882    %{1} % /3/
883  | #l #EX
884    whd in EX:(??%?);
885    @blindly_label whd
886    lapply (refl ? (find_label l (fn_body f) (call_cont k)))
887    cases (find_label ???) in ⊢ (???% → ?);
888    [ #F @⊥  >F in EX; #EX whd in EX:(??%?); destruct
889    | * #s1 #k1 #F >F in EX; #EX whd in EX:(??%?); destruct
890      cases (label_find_label_fn g … KL F)
891      #u' * #cs * #k1' * #F' #K'
892      %{1} whd
893      whd in ⊢ (??%?); >F'
894      % /3/
895    ]
896  | #c #st #EX whd in EX:(??%?); destruct @blindly_label #u1
897    %{0} % /3/
898  ]
899| #u0 #f #ua #a #us #s #cs #cpost #k #k' #e #m #K #EX
900  cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
901  cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX
902  whd in EX:(??%%); destruct
903  cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 ua) #tr1' * #EX1' #T1
904  [ %{1} | %{2} ] whd
905  whd in ⊢ (??%?); >EX1'
906  whd in ⊢ (??%?); >label_expr_type >EX2
907  % [ 1,3: <(E0_right tr) ] /4/
908| #u0 #f #ua #a #us #s #cs #cpost #k #k' #e #m #K #EX
909  whd in EX:(??%%); destruct
910  %{1} % /4/
911| #u0 #f #ua2 #a2 #us3 #s3 #us #s #cs #cpost #k #k' #e #m #K #EX
912  cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
913  cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX
914  whd in EX:(??%%); destruct
915  cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 ua2) #tr1' * #EX1' #T1
916  [ %{1} | %{2} ] whd
917  whd in ⊢ (??%?); >EX1'
918  whd in ⊢ (??%?); >label_expr_type >EX2
919  % [1,3: <(E0_right tr) ] /4/
920| #u0 *
921  [ #f #args #k #k' #m #K whd in ⊢ (??%? → ?); @pair_elim #e #m1 #EX1 #EX
922    cases (bindIO_inversion ??????? EX) -EX #m2 * #EX2 #EX
923    whd in EX:(??%%); destruct
924    whd in match (label_fundef ??);
925    whd in match (label_function ??);
926    lapply (refl ? (\fst (label_function u0 f))) whd in ⊢ (???(???%) → ?);
927    @label_gen_elim #u1 @label_gen_elim #u2 >shift_fst #Ef
928    %{1} whd
929    whd in ⊢ (??%?); >EX1
930    whd in ⊢ (??%?); >EX2
931    % /4/
932  | #id #tys #ty #args #k #k' #m #K #EX
933    cases (bindIO_inversion ??????? EX) -EX #vs * #EX1 #EX
934    cases (bindIO_inversion ??????? EX) -EX #ety * #EX2 #EX
935    whd in EX2:(??%%); destruct
936  ]
937| #res #k #k' #m #K #EX inversion K
938  [ #E1 #E2 #E3 destruct cases res in EX ⊢ %;
939    [ 2: * #i #EX whd in EX:(??%?); destruct
940    | *: normalize #A try #B try #C destruct
941    ]
942    %{0} % /2/
943  | 9: #u0 #r #f #en #k0 #k0' #K' #_ #E1 #E2 #E3 destruct cases r in EX ⊢ %;
944    [ #EX whd in EX:(??%?); destruct
945      %{0} % /3/
946    | * * #b #o #ty #EX
947      cases (bindIO_inversion ??????? EX) -EX #m2 * #EX1 #EX
948      whd in EX:(??%%); destruct
949      %{0} whd whd in ⊢ (??%?); >EX1 % /3/
950    ]
951  | *: #A #B #C #D #E #F #G try #H try #I try #J try #L try #M try #N try #O
952       destruct whd in EX:(??%?); destruct
953  ]
954| #r #EX whd in EX:(??%%); destruct
955] qed.
956
957theorem step_with_labels : ∀ge,ge'.
958  related_globals_gen … label_fundef ge ge' →
959  ∀s1,s1',tr,s2.
960  state_with_labels s1 s1' →
961  exec_step ge s1 = Value … 〈tr,s2〉 →
962   ∃n. after_n_steps (S n) … clight_exec ge' s1'
963   (λtr',s2'. trace_with_extra_labels tr tr' ∧
964              state_with_labels s2 s2').
965#ge #ge' #RG #Xs1 #Xs1' #tr #s2 *
966[ #s1 #s1' @step_with_labels_partial //
967| #u0 #f #u *
968(* If we have LSdefault we need to smuggle the execution of the cost label in
969   before the actual statement. *)
970  [ #s #k #k' #e #m #K #EX
971    whd in EX:(??(??(??%???))?);
972    whd in match (label_lstatements ??); @label_gen_elim #u1 @label_gen_elim #u2
973    >shift_fst whd in match (seq_of_labeled_statement ?);
974    cases (step_with_labels_partial … RG (State f s k e m) (State (\fst (label_function u0 f)) (\fst (label_statement s u)) k' e m) tr s2 (swl_state … K) EX)
975    #n #H %{(S n)} @(after_n_m 1 (S n) … H) % /2/
976    #trx #sx * /3/
977(* but for LScase it's just like the cases in step_with_labels_partial *)
978  | #sz #i #s #ls #k #k' #e #m #K #EX
979    whd in EX:(??(??(??%???))?);
980    whd in match (label_lstatements ??); @label_gen_elim #u1 @label_gen_elim #u2
981    @label_gen_elim #u3 >shift_fst whd in match (seq_of_labeled_statement ?);
982    whd in EX:(??%?); destruct
983    %{1} % /4/
984  ]   
985] qed.
986
987
988lemma exec_step_interaction:
989  ∀ge,s,o,k. exec_step ge s = Interact … o k  →
990  ∃f,argtys,retty,vargs,k',m. s = Callstate (CL_External f argtys retty) vargs k' m.
991#ge #s cases s
992[ #f #st #kk #e #m #o #k #EX @⊥ cases st in EX ⊢ %;
993  [ 11,14: #a | 2,4,6,7,12,13,15: #a #b | 3,5: #a #b #c | 8: #a #b #c #d ]
994  whd in ⊢ (??%? → ?);
995  [ 4,6,8,9: #EX destruct ]
996  [ cases a
997    [ whd in ⊢ (??%? → ?); cases (fn_return f) normalize #A try #B try #C try #D destruct
998    | #a' whd nodelta in ⊢ (??%? → ?); cases (type_eq_dec (fn_return f) Tvoid)
999      #x whd in ⊢ (??%? → ?); [2: cases (exec_expr ????) #y ] #EX whd in EX:(??%?); destruct
1000    ]
1001  | cases (find_label a (fn_body f) (call_cont kk)) [ 2: * #x #y ] #EX whd in EX:(??%?); destruct
1002  | @bindIO_res_interact #l #El @bindIO_res_interact #vt #Evt @bindIO_opt_interact #m' #Em #EX whd in EX:(??%?); destruct
1003  | 4,7: @bindIO_res_interact #x1 #x2 @bindIO_res_interact #x3 #x4 #EX whd in EX:(??%?); destruct
1004  | @bindIO_res_interact * * normalize nodelta #A #B #C try #D try #E destruct
1005    cases (typeof a) in E; normalize nodelta #E try #F try #G destruct
1006    cases (sz_eq_dec A E) in G; normalize nodelta #G [2: #H destruct]
1007    @bindIO_opt_interact #ls' #H #I normalize in I; 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.