source: src/Clight/labelSimulation.ma @ 2338

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

Use much nicer definition for making several steps in the labelling
simulation.

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