source: src/joint/StatusSimulationHelper.ma

Last change on this file was 3371, checked in by piccolo, 6 years ago

Modified RTLsemantics and ERTLsemantics. Now the pop frame will set
to undef the carry bit and all RegisterCallerSaved? exept those used to
pass the return value of a function.

Added an overflow check in ERTL_semantics

File size: 89.7 KB
Line 
1(**************************************************************************)
2(*       ___                                                              *)
3(*      ||M||                                                             *)
4(*      ||A||       A project by Andrea Asperti                           *)
5(*      ||T||                                                             *)
6(*      ||I||       Developers:                                           *)
7(*      ||T||         The HELM team.                                      *)
8(*      ||A||         http://helm.cs.unibo.it                             *)
9(*      \   /                                                             *)
10(*       \ /        This file is distributed under the terms of the       *)
11(*        v         GNU General Public License Version 2                  *)
12(*                                                                        *)
13(**************************************************************************)
14
15include "joint/StatusSimulationUtils.ma".
16
17lemma fetch_stmt_ok_sigma_state_ok : ∀ P_in , P_out: sem_graph_params.
18∀prog : joint_program P_in.
19∀stack_sizes.
20∀ f_lbls,f_regs.∀f_bl_r.∀init.∀st_no_pc_rel,st_rel.
21∀f,fn,stmt,st1,st2.
22good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs
23                    st_no_pc_rel st_rel →
24st_rel st1 st2 →
25fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) =
26 return 〈f,fn,stmt〉 →
27st_no_pc_rel (pc … st1) (st_no_pc … st1) (st_no_pc … st2).
28#P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_lb_r #init #st_no_pc_rel
29#st_rel #f #fn #stmt #st1 #st2 #goodR #Hst_rel #EQfetch
30cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt
31@(fetch_ok_sigma_state_ok … goodR … EQfn) assumption
32qed.
33
34lemma fetch_stmt_ok_sigma_pc_ok : ∀ P_in , P_out: sem_graph_params.
35∀prog : joint_program P_in.
36∀stack_sizes.
37∀ f_lbls,f_regs.∀f_bl_r.∀init.
38∀st_no_pc_rel,st_rel.
39∀f,fn,stmt,st1,st2.
40good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs 
41                    st_no_pc_rel st_rel→
42st_rel st1 st2 →
43fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) =
44 return 〈f,fn,stmt〉 →
45pc … st1 = pc … st2.
46#P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_lb_r #init #st_no_pc_rel
47#st_rel #f #fn #stmt #st1 #st2 #goodR #Hst_rel #EQfetch
48cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt
49@(fetch_ok_pc_ok … goodR … EQfn) assumption
50qed.
51
52lemma fetch_stmt_ok_sigma_last_pop_ok : ∀ P_in , P_out: sem_graph_params.
53∀prog : joint_program P_in.
54∀stack_sizes.
55∀ f_lbls,f_regs.∀f_bl_r.∀init.
56∀st_no_pc_rel,st_rel.
57∀f,fn,stmt,st1,st2.
58good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs
59                    st_no_pc_rel st_rel →
60st_rel st1 st2 →
61fetch_statement P_in … (ev_genv … (mk_prog_params P_in prog stack_sizes)) (pc … st1) =
62 return 〈f,fn,stmt〉 →
63(last_pop … st1) =
64 sigma_stored_pc P_in P_out prog stack_sizes init f_bl_r f_lbls
65  f_regs (last_pop … st2).
66#P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_lb_r #init #st_no_pc_rel
67#st_rel #f #fn #stmt #st1 #st2 #goodR #Hst_rel #EQfetch
68cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt
69@(fetch_ok_sigma_last_pop_ok … goodR … EQfn) assumption
70qed.
71
72lemma as_label_ok_non_entry :  ∀ P_in , P_out: sem_graph_params.
73∀prog : joint_program P_in.
74∀stack_sizes.
75∀ f_lbls,f_regs.∀f_bl_r.∀init.
76∀st_no_pc_rel,st_rel.
77let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in
78let trans_prog  ≝ b_graph_transform_program P_in P_out init prog in
79let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in
80good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs
81                    st_no_pc_rel st_rel →
82∀st1,st2,f,fn,stmt.
83fetch_statement …
84 (joint_globalenv P_in prog stack_sizes) (pc … st1) = return〈f,fn,stmt〉 →
85block_id … (pc_block (pc … st1)) ≠ -1 →
86 st_rel st1 st2 → point_of_pc P_in (pc … st1) ≠ joint_if_entry … fn →
87as_label (joint_status P_in prog stack_sizes) st1 =
88 as_label (joint_status P_out trans_prog stack_sizes) st2.
89#p_in #p_out #prog #stack_size #f_lbls #f_regs #init_regs #init #st_no_pc_rel #st_rel
90#good #st1 #st2 #f #fn #stmt #EQfetch * #Hbl #Rst1st2 * #Hentry
91whd in ⊢ (??%%); >EQfetch normalize nodelta
92lapply(b_graph_transform_program_fetch_statement … good (pc … st1) f fn ?)
93[2: @eqZb_elim [1: #ABS @⊥ >ABS in Hbl; #H @H %] #_ normalize nodelta
94      #H cases(H EQfetch) -H |*:] #data * #t_fn ** #EQt_fn #Hdata #H
95whd in match fetch_statement; normalize nodelta
96>(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in EQt_fn; #EQt_fn >EQt_fn
97>m_return_bind cases stmt in EQfetch H;
98[ * [ #c | #id #args #dest | #r #lb | #seq] #nxt | * [ #lb | | #has #id #args ] | * ]
99#EQfetch normalize nodelta * #bl
100[1,2,3,4: @eq_identifier_elim
101  [1,3,5,7: #EQ @⊥ @Hentry >EQ %
102  |*: #_ cut(∀b.andb b false = false) [1,3,5,7: * %] #EQ >EQ -EQ normalize nodelta
103  ]
104]
105*
106[ >(f_step_on_cost … data) whd in ⊢ (% → ?); cases(f_regs ??) [2: # x #y *]
107  normalize nodelta #EQ destruct(EQ) * #l1 * #mid1 * #mid2 * #l2 *** #EQmid1
108  whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2) * #nxt1 * #EQcost
109  change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) * #EQ1 #EQ2 destruct(EQ1 EQ2)
110  >(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in EQcost; #EQcost >EQcost %
111]
112#Hregs *
113[1,2,3: * [2,4,6: #hd #tl * #mid1 * #mid2 * #l2 *** #EQmid1 cases(\fst (\fst bl))
114          [1,3,5: whd in ⊢ (% → ?); * #EQ destruct(EQ)] #hd1 #tl1 whd in ⊢ (% → ?);
115          * #mid3 * #rest ** #EQ destruct(EQ) * #nxt1 * #EQ
116          change with nxt1 in ⊢ (??%? → ?); #EQ1 destruct(EQ1) #_ #_ #_
117          >(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in EQ; #EQ >EQ % ]
118        * #mid1 * #mid2 * #l2 *** #_ cases bl in Hregs; **
119        [2,4,6: #x #y #z #w #_ whd in ⊢ (% → ?); * #a * #b ** #EQ destruct(EQ)]
120        #instr #post #Hregs whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2) *
121        #nxt1 * #EQ change with nxt1 in ⊢ (??%? → ?); #EQ1 destruct(EQ1)
122         >(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in EQ; #EQ #_ >EQ
123        inversion(instr ?)
124        [2,3,4,6,7,8,10,11,12: [1,4,7: #id1 #arg1 #dest1 |2,5,8: #r1 #lb1 |*: #seq]
125          #EQ1 >EQ1 %] #c1 #EQc1
126        lapply(bind_new_bind_new_instantiates … Hregs (cost_in_f_step … data … c1) …
127             (jmeq_to_eq ??? EQc1)) #EQ destruct(EQ)
128|*: * [2,4,6: #hd #tl * #mid ** #_ cases (\fst bl) [1,3,5: * #EQ destruct(EQ)]
129      #hd1 #tl1 whd in ⊢ (% → ?); * #mid1 * #rest ** #EQ destruct(EQ) whd in ⊢ (% → ?);
130      * #nxt1 * #EQ change with nxt1 in ⊢ (??%? → ?); #EQ1 destruct(EQ1) #_ #_         
131      >(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in EQ; #EQ >EQ %
132      |*: * #mid ** #_ cases bl in Hregs; * [2,4,6: #x #y #z #_ * #w * #a ** #EQ destruct]
133          #instr #_ * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in ⊢ (% → ?);
134          >(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) #EQ >EQ %
135      ]   
136]
137qed.
138 
139
140lemma eval_goto_ok : ∀ P_in , P_out: sem_graph_params.
141∀prog : joint_program P_in.
142∀stack_sizes.
143∀ f_lbls,f_regs.∀f_bl_r.∀init.
144∀st_no_pc_rel,st_rel.
145let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in
146let trans_prog  ≝ b_graph_transform_program P_in P_out init prog in
147let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in
148good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs
149                    st_no_pc_rel st_rel →
150∀st1,st1' : joint_abstract_status prog_pars_in.
151∀st2 : joint_abstract_status prog_pars_out.
152∀f : ident.
153∀fn : joint_closed_internal_function P_in ?.
154∀lbl.
155block_id … (pc_block (pc … st1)) ≠ -1 →
156st_rel st1 st2 →
157 let goto ≝ (GOTO P_in lbl) in
158  fetch_statement P_in ?
159   (joint_globalenv P_in prog stack_sizes) (pc … st1) =
160     return 〈f, fn, final … goto〉 →
161 eval_state P_in …
162  (joint_globalenv P_in prog stack_sizes) st1 = return st1' →
163∃ st2'. st_rel st1' st2' ∧
164∃taf : trace_any_any_free (joint_abstract_status prog_pars_out) st2 st2'.
165bool_to_Prop (taaf_non_empty … taf) ∧
166as_label (joint_abstract_status prog_pars_in) st1' =
167as_label (joint_abstract_status prog_pars_out) st2'.
168#p_in #p_out #prog #stack_size #f_lbls #f_regs #init_regs #init #st_no_pc_rel
169#st_rel #good #st1 #st1' #st2 #f #fn #lbl * #Hbl #Rst1st2 #EQfetch
170whd in match eval_state; normalize nodelta >EQfetch >m_return_bind
171whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
172whd in match eval_statement_advance; normalize nodelta whd in match goto;
173normalize nodelta >pc_of_label_eq
174[2: @(proj1 … (fetch_statement_inv … EQfetch)) |*: ]
175>m_return_bind whd in match set_no_pc;
176whd in match set_pc; normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ)
177lapply(b_graph_transform_program_fetch_statement … good (pc … st1) f fn ?)
178[2,4: @eqZb_elim [1,3: #ABS @⊥ >ABS in Hbl; #H @H %] #_ normalize nodelta
179      #H cases(H EQfetch) -H |*:]
180#data * #t_fn ** #EQt_fn #Hdata normalize nodelta ** #pre #instr * #Hregs
181* #l1 * #mid ** #EQmid #EQl1 whd in ⊢ (% → ?); #EQfin
182cases(bind_new_bind_new_instantiates' … Hregs
183  ((bind_new_bind_new_instantiates' … Hdata (goto_commutation … good …
184       EQfetch Rst1st2 …) ? )))
185[3: % assumption
186|5: <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in ⊢ (??%?); assumption
187|4:
188|2: @sym_eq @(bind_new_bind_new_instantiates' … Hdata (pi2 ?? (init ? fn)))
189]
190#st2_fin ** #EQst2_fin #EQ destruct(EQ) #Hfin_rel
191%{(mk_state_pc ? st2_fin (pc_of_point p_out (pc_block (pc … st2)) lbl)
192    (last_pop … st2))}
193cut(? : Prop)
194[3: #Rst1st2' %{Rst1st2'}
195|
196| <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) @(st_rel_def … good)
197  [3: @(proj1 … (fetch_statement_inv … EQfetch)) |1,2:
198  |5: @(fetch_stmt_ok_sigma_last_pop_ok … good … Rst1st2 EQfetch)
199  | assumption
200  ]
201]
202>(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in EQl1; #EQl1
203lapply(taaf_to_taa … (produce_trace_any_any_free … st2 … … EQl1 … EQst2_fin) ?)
204[ @if_elim #_ [2: @I] % whd in ⊢ (% → ?); * #H @H -H whd in ⊢ (??%?);
205  whd in match (as_pc_of ??); whd in match fetch_statement; normalize nodelta
206  <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) >EQt_fn >m_return_bind
207  whd in match point_of_pc; normalize nodelta >point_of_offset_of_point
208  >EQfin %
209| <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) >EQt_fn %
210]
211#taa %{(taaf_step … taa …)}
212[3: %{I}
213|*: whd [ whd in ⊢ (??%?); | whd in match eval_state;] whd in match fetch_statement;
214    normalize nodelta <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) >EQt_fn
215    >m_return_bind >point_of_pc_of_point >EQfin [%] >m_return_bind
216    whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
217    whd in match eval_statement_advance; whd in match goto; normalize nodelta
218    >pc_of_label_eq
219    [2: whd in match (pc_block ?); >EQt_fn in ⊢ (??%?); % |3:] %
220]
221cases(fetch_stmt_ok_succ_ok … lbl … EQfetch) [4: %|3: % % |*:]
222#stmt' #EQstmt'
223@(as_label_ok_non_entry … good)
224[4: <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in ⊢ (??%?); @EQstmt'
225|1,2,3:
226| <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) % assumption
227| <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in ⊢ (?%?); assumption
228| <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch)
229  cases(entry_unused ??? (pi2 ?? fn) ?? (proj2 ?? (fetch_statement_inv … EQfetch)))
230  * whd in match (point_of_label ????); * #H #_ #_ % >point_of_pc_of_point #EQ destruct(EQ)
231  @H %
232]
233qed.
234
235lemma eval_goto_premain_ok : ∀ P_in , P_out: sem_graph_params.
236∀prog : joint_program P_in.
237∀stack_sizes.
238∀ f_lbls,f_regs.∀f_bl_r.∀init.
239∀st_no_pc_rel,st_rel.
240let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in
241let trans_prog  ≝ b_graph_transform_program P_in P_out init prog in
242let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in
243good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs
244                    st_no_pc_rel st_rel →
245∀st1,st1' : joint_abstract_status prog_pars_in.
246∀st2 : joint_abstract_status prog_pars_out.
247∀f : ident.
248∀fn : joint_closed_internal_function P_in ?.
249∀lbl.
250block_id … (pc_block (pc … st1)) = -1 →
251st_rel st1 st2 →
252 let goto ≝ (GOTO P_in lbl) in
253  fetch_statement P_in ?
254   (joint_globalenv P_in prog stack_sizes) (pc … st1) =
255     return 〈f, fn, final … goto〉 →
256 eval_state P_in …
257  (joint_globalenv P_in prog stack_sizes) st1 = return st1' →
258∃ st2'. st_rel st1' st2' ∧
259∃taf : trace_any_any_free (joint_abstract_status prog_pars_out) st2 st2'.
260bool_to_Prop (taaf_non_empty … taf) ∧
261as_label (joint_abstract_status prog_pars_in) st1' =
262as_label (joint_abstract_status prog_pars_out) st2'.
263#p_in #p_out #prog #stack_sizes #f_lbls #f_regs #init_regs #init #st_no_pc_rel
264#st_rel #good #st1 #st1' #st2 #f #fn #lbl #EQbl #Rst1st2 #EQfetch #EQeval
265cases(pre_main_ok … good … EQbl EQeval Rst1st2) #Hclass * #st2' ** #Rst1st2'
266#EQst2' #Hlab %{st2'} % [assumption] %{(taaf_step … (taa_base …)…)}
267[ whd change with (joint_classify ???) in ⊢ (??%?); <Hclass whd in match joint_classify;
268  normalize nodelta >EQfetch %
269| assumption ] %{I} assumption
270qed.
271
272
273lemma eval_tailcall_ok : ∀ P_in , P_out: sem_graph_params.
274∀prog : joint_program P_in.
275∀stack_sizes.
276∀ f_lbls,f_regs.∀f_bl_r.∀init.
277∀st_no_pc_rel,st_rel.
278let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in
279let trans_prog  ≝ b_graph_transform_program P_in P_out init prog in
280let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in
281good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs
282                    st_no_pc_rel st_rel →
283∀st1,st1' : joint_abstract_status prog_pars_in.
284∀st2 : joint_abstract_status prog_pars_out.
285∀f : ident.
286∀fn : joint_closed_internal_function P_in ?.
287∀has_tail,id,arg.
288block_id … (pc_block (pc … st1)) ≠ -1 →
289st_rel st1 st2 →
290fetch_statement P_in ?
291   (joint_globalenv P_in prog stack_sizes) (pc … st1) =
292     return 〈f, fn, final … (TAILCALL P_in has_tail id arg)〉 →
293 eval_state P_in …
294  (joint_globalenv P_in prog stack_sizes) st1 = return st1' →
295∃is_tail,st2_pre_call,t_is_tail.
296as_tailcall_ident ? («st2_pre_call,t_is_tail») = as_tailcall_ident ? («st1, is_tail») ∧
297∃st2_after_call,st2' : joint_abstract_status prog_pars_out.
298∃taa2 : trace_any_any … st2 st2_pre_call.
299∃taa2' : trace_any_any … st2_after_call st2'.
300eval_state P_out … (joint_globalenv P_out trans_prog stack_sizes)
301st2_pre_call = return st2_after_call ∧
302st_rel st1' st2' ∧
303as_label (joint_abstract_status prog_pars_in) st1' =
304 as_label (joint_abstract_status prog_pars_out) st2_after_call.
305#p_in #p_out #prog #stack_size #f_lbls #f_regs #init_regs #init #st_no_pc_rel #st_rel
306#good #st1 #st1' #st2 #f #fn #has_tail #id #arg * #Hbl #Rst1st2 #EQfetch
307whd in match eval_state in ⊢ (% → ?); normalize nodelta >EQfetch >m_return_bind
308whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
309whd in match eval_statement_advance; whd in match eval_tailcall; normalize nodelta
310>set_no_pc_eta #H @('bind_inversion H) -H #bl #EQbl lapply(err_eq_from_io ????? EQbl)
311-EQbl #EQbl #H @('bind_inversion H) -H
312* #id1 * #fn1 #H lapply(err_eq_from_io ????? H) -H #EQfn1 normalize nodelta
313[2: #H @('bind_inversion H) -H #x whd in match eval_external_call; normalize nodelta
314    #H @('bind_inversion H) -H #y #_ #H @('bind_inversion H) -H #z #_
315    #H @('bind_inversion H) -H #w whd in ⊢ (??%%→ ?); #ABS destruct(ABS) ]
316whd in match (stack_sizes ????); #H lapply(err_eq_from_io ????? H) -H
317#H @('bind_inversion H) -H #ssize_f #H lapply(opt_eq_from_res ???? H) -H #EQssize_f
318#H @('bind_inversion H) -H #st1_fin whd in match eval_internal_call;
319normalize nodelta whd in match (stack_sizes ????); #H @('bind_inversion H) -H
320#ssize_f1 #H lapply(opt_eq_from_res ???? H) -H #EQssize_f1 #H @('bind_inversion H) -H
321#st1_setup #EQst1_setup whd in ⊢ (??%% → ??%% → ?); #EQ1 #EQ2 destruct(EQ1 EQ2)
322% [@hide_prf whd in ⊢ (??%?); >EQfetch %]
323lapply(b_graph_transform_program_fetch_statement … good (pc … st1) f fn ?)
324[2,4: @eqZb_elim [1,3: #ABS @⊥ >ABS in Hbl; #H @H %] #_ normalize nodelta
325      #H cases(H EQfetch) -H |*:]
326#data * #t_fn ** #EQt_fn #Hdata normalize nodelta ** #pre #instr * #Hregs *
327#l1 * #mid ** #EQmid #EQpre whd in ⊢ (% → ?); #EQmid
328cut(? : Prop)
329[3: #EQint_fn1
330    lapply(b_graph_transform_program_fetch_internal_function … good bl id1 fn1)
331    @eqZb_elim [ #ABS cases(block_of_call_no_minus_one … EQbl) >ABS #H @⊥ @H % ]
332    #_ normalize nodelta
333    #H cases(H EQint_fn1) -H #data1 * #t_fn1 ** #EQt_fn1 #Hregs1 #good1
334    cases(bind_new_bind_new_instantiates' … Hregs
335    ((bind_new_bind_new_instantiates' ?????? Hdata
336     (tailcall_commutation ?????????? good ???????? EQfetch ? EQbl … EQint_fn1 …
337       EQssize_f … EQssize_f1 … EQst1_setup … Rst1st2 … EQt_fn1)) ?))
338    [3: % assumption
339    |2: @sym_eq @(bind_new_bind_new_instantiates' … Hdata (pi2 ?? (init ? fn)))
340    ]
341    #has_tail' * #id' * #arg' * #EQ destruct(EQ) * #st2_pre ** #EQst2_pre #EQt_bl
342    * #st2_after * #EQst2_after #H cases(bind_new_bind_new_instantiates' … Hregs1 H)
343    -H [2: @sym_eq
344           @(bind_new_bind_new_instantiates' … Hregs1 (pi2 ?? (init ? fn1)))]
345    #st2' * #EQst2' #fin_sem_rel
346|2: whd in match fetch_internal_function; normalize nodelta >EQfn1 %
347|
348]
349%{(mk_state_pc ? st2_pre (pc_of_point p_out (pc_block … (pc … st2)) mid) (last_pop … st2))}
350%
351[ @hide_prf whd in ⊢ (??%?); whd in match fetch_statement; normalize nodelta
352  <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) >EQt_fn >m_return_bind
353  >point_of_pc_of_point >EQmid % ]
354%
355[ whd in ⊢ (??%%); >EQfetch in ⊢ (???(match % with [_ ⇒ ? | _ ⇒ ?]));
356  whd in match fetch_statement; normalize nodelta
357  <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in
358     ⊢ (??(match % with [_ ⇒ ? | _ ⇒ ?])?);
359  >EQt_fn in ⊢ (??(match % with [_ ⇒ ? | _ ⇒ ?])?);
360  >m_return_bind in ⊢ (??(match % with [_ ⇒ ? | _ ⇒ ?])?);
361  >point_of_pc_of_point in ⊢ (??(match % with [_ ⇒ ? | _ ⇒ ?])?);
362  >EQmid in ⊢ (??(match % with [_ ⇒ ? | _ ⇒ ?])?); normalize nodelta
363  >EQbl >EQt_bl >m_return_bind >m_return_bind >EQt_fn1 >EQint_fn1 %
364]
365%{(mk_state_pc ? (increment_stack_usage p_out ssize_f1 st2_after)
366   (pc_of_point p_out bl (joint_if_entry … t_fn1)) (last_pop … st2))}
367%{(mk_state_pc ? st2' (pc_of_point p_out bl (joint_if_entry … fn1)) (last_pop … st2))}
368>(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in EQt_fn; #EQt_fn
369>(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in EQpre; #EQpre
370%{(taaf_to_taa … (produce_trace_any_any_free … st2 … EQt_fn … EQpre EQst2_pre) …)}
371[ @if_elim #_ [2: @I] % whd in ⊢ (% → ?); * #H @H -H whd in ⊢ (??%?);
372  whd in match fetch_statement; normalize nodelta >EQt_fn >m_return_bind
373  >point_of_pc_of_point >EQmid % ]
374cases good1 -good1 #_ #_ #_ #_ #_ #_ #_ #_ #_ #_ #_ cases(entry_is_cost … (pi2 ?? fn1))
375#nxt1 * #c #EQin #H lapply(H … EQin) -H normalize nodelta >(f_step_on_cost … data1)
376* #st_bl @eq_identifier_elim [2: * #H @⊥ @H % #_ ] #_
377cases(added_prologue … data1) in EQst2';
378[ whd in ⊢ (??%% → ?); #EQ destruct(EQ) normalize nodelta * whd in ⊢ (% → ?);
379  inversion(f_regs ??) normalize nodelta [2: #x #y #_ #_ *] #EQregs #EQ destruct(EQ)
380  * #l1 * #mid1 * #mid2 * #l2 *** #EQmid1 * #EQ1 #EQ2 destruct(EQ1 EQ2) *
381  #nxt2 * #EQt_cost change with nxt2 in ⊢ (??%? → ?); #EQ destruct(EQ) *
382  #EQ1 #EQ2 destruct(EQ1 EQ2) #EQentry >EQentry %{(taa_base …)}
383| #hd #tl #EQst2' * normalize nodelta whd in ⊢ (% → ?); inversion(f_regs ??)
384  [2: #x #y #_ #_ *] #EQregs normalize nodelta #EQ destruct(EQ) * #l1 * #mid1 * #mid2
385  * #l2 *** #EQmid1 whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in ⊢ (% → ?);
386  * #nxt2 * #EQnop change with nxt2 in ⊢ (??%? → ?); #EQ destruct(EQ) whd in ⊢ (% → ?);
387  * #EQ1 #EQ2 destruct(EQ1 EQ2) * #star * #_  whd in ⊢ (% → ?); * #l3 * #mid3 * #mid4
388  * #l4 *** #_ * #EQ1 #EQ2 destruct(EQ1 EQ2) * #nxt2 * #EQt_cost
389  change with nxt2 in ⊢ (??%? → ?); #EQ destruct(EQ) #EQl4
390  letin trans_prog ≝ (b_graph_transform_program ????)
391  lapply(taaf_to_taa …
392   (produce_trace_any_any_free … (mk_prog_params p_out trans_prog stack_size)
393    (mk_state_pc ? (increment_stack_usage p_out ssize_f1 st2_after)
394     (pc_of_point p_out bl mid4) (last_pop … st2)) … EQt_fn1 … EQst2') ?)
395  [4: >point_of_pc_of_point in ⊢ (????%???); assumption
396  | @if_elim #_ [2: @I] % * #H @H -H whd in ⊢ (??%?); whd in match fetch_statement;
397    normalize nodelta >EQt_fn1 >m_return_bind >point_of_pc_of_point >EQnop %
398  |*:]
399  #taa %{(taa_step … taa)}
400  [ % * #H @H whd in ⊢ (??%?); whd in match fetch_statement; normalize nodelta
401    >EQt_fn1 >m_return_bind >point_of_pc_of_point cases EQl4 #mid5 * #rest **
402    #EQ destruct(EQ) * #nxt3 * #EQ #_ #_ >EQ %
403  |2,3: whd [ whd in ⊢ (??%?); | whd in match eval_state; ]
404    whd in match fetch_statement; normalize nodelta >EQt_fn1
405    >m_return_bind >point_of_pc_of_point >EQt_cost [2: %] >m_return_bind %
406  ]
407]
408%
409[2,4: whd in ⊢ (??%%); whd in match (as_pc_of ??);  whd in match (as_pc_of ??);
410      whd in match fetch_statement; normalize nodelta >EQint_fn1 >EQt_fn1
411      >m_return_bind >m_return_bind whd in match point_of_pc; normalize nodelta
412      >point_of_offset_of_point >point_of_offset_of_point >EQin >m_return_bind
413      normalize nodelta >EQt_cost >m_return_bind normalize nodelta [ %]
414      whd in match get_first_costlabel; normalize nodelta whd in ⊢ (??%%);
415      whd in match (get_first_costlabel_next ???);
416      generalize in match (refl ??);
417      >EQin in ⊢ (∀e:???%. ???(??(???(match % return ? with [_ ⇒ ? | _ ⇒ ?]?))));
418      #EQcost' normalize nodelta %
419]
420%
421[1,3: whd in match eval_state; whd in match fetch_statement; normalize nodelta
422      >EQt_fn >m_return_bind >point_of_pc_of_point >EQmid >m_return_bind
423      whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
424      whd in match eval_statement_advance; whd in match eval_tailcall;
425      normalize nodelta >EQt_bl >m_return_bind @('bind_inversion EQt_fn1)
426      * #id2 * #fn2 normalize nodelta #EQ whd in ⊢ (??%% → ?); #EQ1 destruct(EQ1)
427      >EQ -EQ >m_return_bind normalize nodelta whd in match (stack_sizes ????);
428      >EQssize_f >m_return_bind whd in match eval_internal_call; normalize nodelta
429      whd in match (stack_sizes ????); >EQssize_f1 >m_return_bind >EQst2_after
430      >m_return_bind [2: %] whd in match set_no_pc; normalize nodelta >EQentry %
431|*: @(st_rel_def … good … fin_sem_rel …) [3,7: @EQint_fn1 |1,2,5,6:]
432    @(fetch_stmt_ok_sigma_last_pop_ok … good … EQfetch) assumption
433]
434qed.
435
436lemma eval_tailcall_premain_ok : ∀ P_in , P_out: sem_graph_params.
437∀prog : joint_program P_in.
438∀stack_sizes.
439∀ f_lbls,f_regs.∀f_bl_r.∀init.
440∀st_no_pc_rel,st_rel.
441let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in
442let trans_prog  ≝ b_graph_transform_program P_in P_out init prog in
443let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in
444good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs
445                    st_no_pc_rel st_rel →
446∀st1,st1' : joint_abstract_status prog_pars_in.
447∀st2 : joint_abstract_status prog_pars_out.
448∀f : ident.
449∀fn : joint_closed_internal_function P_in ?.
450∀has_tail,id,arg.
451block_id … (pc_block (pc … st1)) = -1 →
452st_rel st1 st2 →
453fetch_statement P_in ?
454   (joint_globalenv P_in prog stack_sizes) (pc … st1) =
455     return 〈f, fn, final … (TAILCALL P_in has_tail id arg)〉 →
456 eval_state P_in …
457  (joint_globalenv P_in prog stack_sizes) st1 = return st1' →
458∃is_tail,st2_pre_call,t_is_tail.
459as_tailcall_ident ? («st2_pre_call,t_is_tail») = as_tailcall_ident ? («st1, is_tail») ∧
460∃st2_after_call,st2' : joint_abstract_status prog_pars_out.
461∃taa2 : trace_any_any … st2 st2_pre_call.
462∃taa2' : trace_any_any … st2_after_call st2'.
463eval_state P_out … (joint_globalenv P_out trans_prog stack_sizes)
464st2_pre_call = return st2_after_call ∧
465st_rel st1' st2' ∧
466as_label (joint_abstract_status prog_pars_in) st1' =
467 as_label (joint_abstract_status prog_pars_out) st2_after_call.
468#p_in #p_out #prog #stack_size #f_lbls #f_regs #init_regs #init #st_no_pc_rel
469#st_rel #good #st1 #st1' #st2 #f #fn #has #id #arg #EQbl #Rst1st2 #EQfetch
470#EQeval cases(pre_main_ok … good … EQbl EQeval Rst1st2) #Hclass * #st2' **
471#Rst1st2' #EQst2' #Hlab % [ @hide_prf whd in ⊢ (??%?); >EQfetch %] %{st2}
472% [ @hide_prf change with (joint_classify ???) in ⊢ (??%?); <Hclass
473    whd in ⊢ (??%?); >EQfetch %]
474%
475[ letin trans_prog  ≝ (b_graph_transform_program p_in p_out init prog)
476  cut(∃f',fn',has',id',arg'.
477    fetch_statement p_out … (joint_globalenv p_out trans_prog stack_size)
478     (pc … st2) = return 〈f',fn',final ?? (TAILCALL p_out has' id' arg')〉)
479  [ lapply Hclass whd in ⊢ (??%? → ?); >EQfetch whd in match joint_classify_final;
480    normalize nodelta whd in match joint_classify; normalize nodelta
481    inversion (fetch_statement ????) [2: #e #_ normalize nodelta #EQ destruct(EQ)]
482    ** #f' #fn' *
483    [ * [ #c | #c_id #arg #dest | #r #lbl | #seq ] #nxt | * [ #lbl | | #has' #id' #arg' ] | *]
484    #EQt_fetch normalize nodelta whd in ⊢ (???% → ?); #EQ destruct(EQ)
485    %{f'} %{fn'} %{has'} %{id'} %{arg'} % ]
486  * #f' * #fn' * #has' * #id' * #arg' #EQt_fetch
487  @('bind_inversion EQeval) #x >EQfetch in ⊢ (% → ?); whd in ⊢ (??%% → ?);
488  #EQ destruct(EQ) whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
489  whd in match eval_statement_advance; whd in match eval_tailcall; normalize nodelta
490  #H @('bind_inversion H) -H #bl #H lapply(err_eq_from_io ????? H) -H #EQbl
491  #H @('bind_inversion H) -H * #f1 * #fn1 #H lapply(err_eq_from_io ????? H) -H
492  #EQfn1 normalize nodelta
493  [2: #H @('bind_inversion H) -H #st whd in match eval_external_call; normalize nodelta
494    #H @('bind_inversion H) -H #x #_ #H @('bind_inversion H) -H #y #_
495    #H @('bind_inversion H) -H #z whd in ⊢ (??%% → ?); #EQ destruct(EQ)
496  ]
497  #H lapply(err_eq_from_io ????? H) -H #H@('bind_inversion H) -H #f_ssize
498  #H lapply(opt_eq_from_res ???? H) -H whd in match (stack_sizes ????); #EQf_ssize
499  #H @('bind_inversion H) -H #st1_fin whd in match eval_internal_call; normalize nodelta
500  #H @('bind_inversion H) -H #f1_ssize #H lapply(opt_eq_from_res ???? H) -H
501  whd in match (stack_sizes ????); #EQf1_ssize #H @('bind_inversion H) -H
502  #st1_setup #EQst1_setup whd in ⊢ (??%% → ??%% → ?); #EQ1 #EQ2 destruct(EQ1 EQ2)
503  @('bind_inversion EQst2') #x >EQt_fetch in ⊢ (% → ?); whd in ⊢ (??%% → ?);
504  #EQ destruct(EQ) whd in match eval_statement_no_pc; normalize nodelta
505  >m_return_bind whd in match eval_statement_advance; whd in match eval_tailcall;
506  normalize nodelta #H @('bind_inversion H) -H #bl' #H lapply(err_eq_from_io ????? H)
507  -H #EQbl' #H @('bind_inversion H) -H * #f1' * #fn1' #H lapply(err_eq_from_io ????? H)
508  -H #EQfn1' normalize nodelta
509  [2: #H @('bind_inversion H) -H #st whd in match eval_external_call; normalize nodelta
510    #H @('bind_inversion H) -H #x #_ #H @('bind_inversion H) -H #y #_
511    #H @('bind_inversion H) -H #z whd in ⊢ (??%% → ?); #EQ destruct(EQ)
512  ]
513  #H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H #f_ssize'
514  #H lapply(opt_eq_from_res ???? H) -H whd in match (stack_sizes ????); #EQf_ssize'
515  #H @('bind_inversion H) -H #st2_fin whd in match eval_internal_call;
516  normalize nodelta #H @('bind_inversion H) -H #f1_ssize' #H lapply(opt_eq_from_res ???? H)
517  -H whd in match (stack_sizes ????); #EQf1_ssize' #H @('bind_inversion H) -H
518  #st2_setup #EQst2_setup whd in ⊢ (??%% → ??%% → ?); #EQ1 #EQ2 destruct(EQ1 EQ2)
519  whd in ⊢ (??%%); >EQfetch in ⊢ (???(match % with [ _ ⇒ ? | _ ⇒ ? ]));
520      normalize nodelta >EQt_fetch in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? ])?);
521     normalize nodelta >EQbl >EQbl' >m_return_bind >m_return_bind
522     whd in match fetch_internal_function; normalize nodelta
523     lapply(fetch_ok_pc_ok … good … Rst1st2' ?)
524     [ whd in match fetch_internal_function; normalize nodelta >EQfn1 in ⊢ (??%?); %
525     |*:
526      ]
527    whd in match pc_of_point in ⊢ (% → ?); normalize nodelta #EQ destruct(EQ)
528    >EQfn1 >EQfn1' >m_return_bind >m_return_bind normalize nodelta
529    lapply EQfn1 whd in match fetch_function; normalize nodelta
530    @eqZb_elim [ #ABS @⊥ cases(block_of_call_no_minus_one …  EQbl) #H @H assumption]
531    #Hbl' normalize nodelta #H lapply(opt_eq_from_res ???? H) -H #H @('bind_inversion H)
532    #f2 #EQf2 #H @('bind_inversion H) -H #fn2 #_ whd in ⊢ (??%? → ?); -e0 -EQ
533    #EQ destruct(EQ) -H lapply EQfn1' whd in match fetch_function; normalize nodelta
534    @eqZb_elim [ #ABS >ABS in Hbl'; * #H @⊥ @H %] #_ normalize nodelta
535    #H lapply(opt_eq_from_res ???? H) -H
536    whd in match joint_globalenv in ⊢ (% → ?); normalize nodelta
537    whd in match b_graph_transform_program in ⊢ (% → ?); normalize nodelta
538    whd in match transform_joint_program; normalize nodelta
539    >(symbol_for_block_transf ??? (λx.x) prog
540      (λvars.transf_fundef ?? (λdef_in.b_graph_translate ??? (init ? def_in) def_in)) bl') in ⊢ (% → ?);
541    >EQf2 >m_return_bind in ⊢ (% → ?); #H @('bind_inversion H) -H #fn2' #_
542    whd in ⊢ (??%% → ?); #EQ destruct(EQ) %
543]
544%{st2'} %{st2'} %{(taa_base …)} %{(taa_base …)} % [2: assumption] %{EQst2' Rst1st2'}
545qed.
546 
547
548lemma eval_cond_ok : ∀ P_in , P_out: sem_graph_params.
549∀prog : joint_program P_in.
550∀stack_sizes.
551∀ f_lbls,f_regs.∀f_bl_r.∀init.
552∀st_no_pc_rel,st_rel.
553let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in
554let trans_prog  ≝ b_graph_transform_program P_in P_out init prog in
555let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in
556good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs
557                    st_no_pc_rel st_rel →
558∀st1,st1' : joint_abstract_status prog_pars_in.
559∀st2 : joint_abstract_status prog_pars_out.
560∀f : ident.
561∀fn : joint_closed_internal_function P_in ?.
562∀a,ltrue,lfalse.
563block_id … (pc_block (pc … st1)) ≠ -1 →
564st_rel st1 st2 →
565 let cond ≝ (COND P_in ? a ltrue) in
566  fetch_statement P_in ?
567   (joint_globalenv P_in prog stack_sizes) (pc … st1) =
568     return 〈f, fn, sequential … cond lfalse〉 →
569 eval_state P_in …
570  (joint_globalenv P_in prog stack_sizes) st1 = return st1' →
571as_costed (joint_abstract_status prog_pars_in) st1' →
572∃ st2'. st_rel st1' st2' ∧
573∃taf : trace_any_any_free (joint_abstract_status prog_pars_out) st2 st2'.
574bool_to_Prop (taaf_non_empty … taf) ∧
575as_label (joint_abstract_status prog_pars_in) st1' =
576 as_label (joint_abstract_status prog_pars_out) st2'.
577#P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_bl_r #init #st_no_pc_rel
578#st_rel #goodR #st1 #st1' #st2 #f #fn #a #ltrue #lfalse * #Hbl #Rst1st2
579#EQfetch #EQeval
580@('bind_inversion EQeval) #x >EQfetch whd in ⊢ (??%% → ?); #EQ destruct(EQ)
581whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
582#H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H #bv #EQbv
583#H @('bind_inversion H) -H * #EQbool normalize nodelta whd in ⊢ (??%% → ?);
584cases(fetch_statement_inv … EQfetch) #EQfn normalize nodelta #EQstmt
585[ >(pc_of_label_eq … EQfn)
586  normalize nodelta whd in match set_pc; normalize nodelta whd in ⊢ (??%? → ?);
587| whd in match next; whd in match set_pc; whd in match set_no_pc; normalize nodelta
588]
589#EQ destruct(EQ) #n_costed
590lapply(b_graph_transform_program_fetch_internal_function … goodR (pc_block (pc … st1)) f fn)
591@eqZb_elim [1,3: #ABS @⊥ >ABS in Hbl; #H @H %] #_ normalize nodelta #H
592cases(H (proj1 … (fetch_statement_inv … EQfetch))) -H
593#init_data * #t_fn1 **  >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch)
594#EQt_fn1 #Hinit * #_ #_ #_ #_ #_ #_ #_ #_ #_ #_ #_ #H
595lapply(H ?? (proj2 … (fetch_statement_inv … EQfetch))) -H normalize nodelta
596 whd in ⊢ (% → ?);
597*** #blp #blm #bls * @if_elim
598[1,3: @eq_identifier_elim [2,4: #_ cases(not_emptyb ??) *]
599      #ABS #_ lapply(fetch_statement_inv … EQfetch) * #_ <ABS
600      cases(entry_is_cost … (pi2 ?? fn)) #nxt1 * #c #EQ >EQ #EQ1 destruct(EQ1)
601]
602#_ <(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) #EQbl whd in ⊢ (% → ?); *
603#l1 * #mid1 * #mid2 * #l2 *** #EQmid1 whd in ⊢ (% → ?); #seq_pre_l whd in ⊢ (% → ?); * #nxt1
604* #EQmid change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ)
605cases(bind_new_bind_new_instantiates' … EQbl ((bind_new_bind_new_instantiates' … Hinit
606               (cond_commutation … goodR … EQfetch EQbv EQbool Rst1st2 t_fn1 EQt_fn1)) ?))
607[2,5: @sym_eq >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch)
608      @(bind_new_bind_new_instantiates' … Hinit (pi2 ?? (init ? fn)))
609|3,6: % assumption
610]
611#EQ destruct(EQ) #APP whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2)
612cases(APP … EQmid) -APP #st_pre_mid_no_pc * #EQst_pre_mid_no_pc *
613normalize nodelta
614#Hsem * #a' * #EQt_cond * #bv' * #EQbv' #rel_v_v' #_
615[ %{(mk_state_pc ? st_pre_mid_no_pc (pc_of_point P_in (pc_block (pc … st1)) ltrue)
616     (last_pop … st2))}
617| %{(mk_state_pc ? st_pre_mid_no_pc (pc_of_point P_in (pc_block (pc … st1)) lfalse)
618     (last_pop … st2))}
619]
620letin st1' ≝ (mk_state_pc P_in ???)
621letin st2' ≝ (mk_state_pc P_out ???)
622cut(st_rel st1' st2')
623[1,3: @(st_rel_def … goodR … f fn ?)
624      [1,4: change with (pc_block (pc … st1)) in match (pc_block ?); assumption
625      |2,5: assumption
626      |3,6: @(fetch_stmt_ok_sigma_last_pop_ok … goodR … EQfetch) assumption
627      ]
628]
629#H_fin
630%
631[1,3: assumption]
632>(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) in seq_pre_l; #seq_pre_l
633lapply(taaf_to_taa ???
634           (produce_trace_any_any_free ? st2 f t_fn1 ??? st_pre_mid_no_pc EQt_fn1
635                                       seq_pre_l EQst_pre_mid_no_pc) ?)
636[1,3: @if_elim #_ // % whd in ⊢ (% → ?); whd in match (as_label ??);
637      whd in match fetch_statement; normalize nodelta >EQt_fn1 >m_return_bind
638      whd in match (as_pc_of ??); whd in match point_of_pc; normalize nodelta
639      >point_of_offset_of_point >EQmid >m_return_bind normalize nodelta >EQt_cond *
640      #H @H %
641]
642#taa_pre_mid %{(taaf_step_jump ? ??? taa_pre_mid ???)}
643[1,5: cases(fetch_stmt_ok_succ_ok … (pc … st1) (pc … st1') … EQfetch ?)
644      [2: @ltrue|3: %2 % % |4: % |6: @lfalse |7: % % |8: %] #stmt' #EQstmt'
645      whd <(as_label_ok_non_entry … goodR … EQstmt' ? H_fin)
646      [1,4: assumption
647      |2,5: cases(entry_unused … (pi2 ?? fn) … EQstmt)
648            [ whd in match stmt_forall_labels; whd in match stmt_labels;
649              normalize nodelta #H cases(append_All … H) #_
650              whd in match stmt_explicit_labels; whd in match step_labels;
651              normalize nodelta * whd in match (point_of_label ????);
652              * #H1 #_ #_ >point_of_pc_of_point % #H2 @H1 >H2 %
653            | ** whd in match (point_of_label ????); #H1 #_ #_ % whd in match st1';
654              #H2 @H1 <H2 whd in match succ_pc; whd in match point_of_pc;
655              normalize nodelta whd in match pc_of_point; normalize nodelta
656              >point_of_offset_of_point %
657            ]
658      |*: % assumption
659      ]
660|2,6: whd whd in match (as_classify ??); whd in match fetch_statement; normalize nodelta
661      >EQt_fn1 >m_return_bind >point_of_pc_of_point >EQmid normalize nodelta
662      >EQt_cond %
663|3,7: whd whd in match eval_state; whd in match fetch_statement; normalize nodelta
664    >EQt_fn1 >m_return_bind >point_of_pc_of_point >EQmid >m_return_bind >EQt_cond
665    whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
666    whd in match eval_statement_advance; normalize nodelta >EQbv' >m_return_bind
667    >rel_v_v' >m_return_bind normalize nodelta
668    [ whd in match goto; normalize nodelta >(pc_of_label_eq … EQt_fn1)]
669      >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 … EQfetch) %
670|*: %{I} cases(fetch_stmt_ok_succ_ok … (pc … st1') … EQfetch)
671    [4,8: %
672    |3: whd in match stmt_labels; normalize nodelta @Exists_append2
673        whd in match stmt_explicit_labels; whd in match step_labels;
674        normalize nodelta %1 //
675    |7: @Exists_append1 %1 %
676    |2,6:
677    ]
678    #stmt' #EQstmt' @(as_label_ok_non_entry … goodR)
679    [4,11: @EQstmt'
680    |1,2,3,8,9,10:
681    |5,12: % assumption
682    |6,13: assumption
683    |*: cases(entry_unused ??? (pi2 ?? fn) ?? (proj2 ?? (fetch_statement_inv … EQfetch)))
684        [ * #_ ** whd in match (point_of_label ????); #H #_ #_ % #H1 @H <H1
685          >point_of_pc_of_point %
686        | ** whd in match (point_of_label ????); #H #_ #_ % #H1 @H <H1
687          >point_of_pc_of_point %
688        ]
689    ]
690]
691qed.
692
693lemma eval_cond_premain_ok : ∀ P_in , P_out: sem_graph_params.
694∀prog : joint_program P_in.
695∀stack_sizes.
696∀ f_lbls,f_regs.∀f_bl_r.∀init.
697∀st_no_pc_rel,st_rel.
698let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in
699let trans_prog  ≝ b_graph_transform_program P_in P_out init prog in
700let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in
701good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs
702                    st_no_pc_rel st_rel →
703∀st1,st1' : joint_abstract_status prog_pars_in.
704∀st2 : joint_abstract_status prog_pars_out.
705∀f : ident.
706∀fn : joint_closed_internal_function P_in ?.
707∀a,ltrue,lfalse.
708block_id … (pc_block (pc … st1)) = -1 →
709st_rel st1 st2 →
710 let cond ≝ (COND P_in ? a ltrue) in
711  fetch_statement P_in ?
712   (joint_globalenv P_in prog stack_sizes) (pc … st1) =
713     return 〈f, fn, sequential … cond lfalse〉 →
714 eval_state P_in …
715  (joint_globalenv P_in prog stack_sizes) st1 = return st1' →
716as_costed (joint_abstract_status prog_pars_in) st1' →
717∃ st2'. st_rel st1' st2' ∧
718∃taf : trace_any_any_free (joint_abstract_status prog_pars_out) st2 st2'.
719bool_to_Prop (taaf_non_empty … taf) ∧
720as_label (joint_abstract_status prog_pars_in) st1' =
721 as_label (joint_abstract_status prog_pars_out) st2'.
722#p_in #p_out #prog #stack_size #f_lbls #f_regs #init_regs #init #st_no_pc_rel
723#st_rel #good #st1 #st1' #st2 #f #fn #a #ltrue #lfalse #EQbl #Rst1st2 #EQfetch
724#EQeval cases(pre_main_ok … good …  EQbl EQeval Rst1st2) #Hclass  * #st2'
725** #Rst1st2' #EQst2' #Hlab whd in ⊢ (% → ?); * #ncost %{st2'} %{Rst1st2'}
726%{(taaf_step_jump … (taa_base …) …)}
727[ whd <Hlab % assumption
728| whd change with (joint_classify ???) in ⊢ (??%?); <Hclass
729  whd in match joint_classify; normalize nodelta >EQfetch %
730| assumption
731]
732%{I} assumption
733qed.
734
735
736lemma general_eval_seq_no_call_ok :∀ P_in , P_out: sem_graph_params.
737∀prog : joint_program P_in.
738∀stack_sizes.
739∀ f_lbls,f_regs.∀f_bl_r.∀init.
740∀st_no_pc_rel,st_rel.
741let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in
742let trans_prog  ≝ b_graph_transform_program P_in P_out init prog in
743let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in
744good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs
745                    st_no_pc_rel st_rel →
746∀st1,st1' : joint_abstract_status prog_pars_in.
747∀st2 : joint_abstract_status prog_pars_out.
748∀f.∀fn : joint_closed_internal_function P_in ?.
749∀stmt,nxt.
750block_id … (pc_block (pc … st1)) ≠ -1 →
751st_rel st1 st2 →
752 let seq ≝ (step_seq P_in ? stmt) in
753  fetch_statement P_in …
754   (joint_globalenv P_in prog stack_sizes) (pc … st1) =
755     return 〈f, fn,  sequential ?? seq nxt〉 →
756 eval_state P_in … (joint_globalenv P_in prog stack_sizes)
757  st1 = return st1' →
758∃st2'. st_rel st1' st2' ∧           
759∃taf : trace_any_any_free (joint_abstract_status prog_pars_out) st2 st2'.           
760 if taaf_non_empty … taf then True else  (*IT CAN BE SIMPLIFIED *)
761(¬as_costed (joint_abstract_status (mk_prog_params P_in prog stack_sizes)) st1 ∨
762 ¬as_costed (joint_abstract_status (mk_prog_params P_in prog stack_sizes)) st1') ∧
763as_label (joint_abstract_status prog_pars_in) st1' =
764 as_label (joint_abstract_status prog_pars_out) st2'. 
765#P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_bl_r #init #st_no_pc_rel #st_rel
766#goodR #st1 #st1' #st2 #f #fn #stmt #nxt * #Hbl #Rst1st2 #EQfetch #EQeval
767@('bind_inversion EQeval) #x >EQfetch whd in ⊢ (??%% → ?); #EQ destruct(EQ)
768#H @('bind_inversion H) -H #st1_no_pc #H lapply(err_eq_from_io ????? H) -H
769#EQst1_no_pc whd in ⊢ (??%% → ?); whd in match next; whd in match set_pc;
770whd in match set_no_pc; normalize nodelta #EQ destruct(EQ)
771lapply(b_graph_transform_program_fetch_statement … goodR (pc … st1) f fn ?)
772[2: @eqZb_elim [ #ABS @⊥ >ABS in Hbl; #H @H %] #_ normalize nodelta
773      #H cases(H EQfetch) -H |*:]
774#init_data * #t_fn ** >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch)
775#EQt_fn #Hinit normalize nodelta * #bl * @if_elim
776[ @eq_identifier_elim [2: #_ cases(not_emptyb ??) *] whd in match point_of_pc;
777  normalize nodelta whd in match (point_of_offset ??); #ABS #_
778  lapply(fetch_statement_inv … EQfetch) * #_
779  >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) whd in match point_of_pc;
780  normalize nodelta whd in match (point_of_offset ??); <ABS
781  cases(entry_is_cost … (pi2 ?? fn)) #nxt1 * #c #EQ >EQ #EQ1 destruct(EQ1)
782]
783#_ <(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) #EQbl
784>(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) #SBiC
785cases(bind_new_bind_new_instantiates' … EQbl ((bind_new_bind_new_instantiates' … Hinit
786               (seq_commutation … goodR … EQfetch EQeval Rst1st2 t_fn EQt_fn)) ? ))
787[2: @sym_eq >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) 
788    @(bind_new_bind_new_instantiates' … Hinit (pi2 ?? (init ? fn)))
789|3: % assumption
790]
791#l * #EQ destruct(EQ) * #st2_fin_no_pc * #EQst2_fin_no_pc #Rsem
792%{(mk_state_pc ? st2_fin_no_pc (pc_of_point P_out (pc_block (pc … st2)) nxt) (last_pop … st2))}
793cases(fetch_statement_inv … EQfetch) >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch)
794#EQfn #_ cut(? : Prop) [3: #Hfin % [@Hfin] |1:
795| @(st_rel_def ?????????? goodR … f fn)
796      [ change with (pc_block (pc … st2)) in match (pc_block ?); assumption
797      | <(fetch_stmt_ok_sigma_pc_ok … goodR … EQfetch) assumption
798      | @(fetch_stmt_ok_sigma_last_pop_ok … goodR … EQfetch) assumption
799      ]
800]
801%{(produce_trace_any_any_free_coerced ? st2 f t_fn l ?? st2_fin_no_pc EQt_fn
802                                      SBiC EQst2_fin_no_pc)}
803% [ @if_elim #_ [@I] % % whd in ⊢ (% → ?); * #H @H -H whd in ⊢ (??%?); >EQfetch % ]
804cases(fetch_stmt_ok_succ_ok … nxt … EQfetch) [4: % |3: % % |2:]
805#stmt' #EQstmt'  @(as_label_ok_non_entry … goodR)
806[4: <(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) in ⊢ (??%?); @EQstmt'
807|1,2,3:
808| % <(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) assumption
809| assumption
810| cases(entry_unused ??? (pi2 ?? fn) ?? (proj2 ?? (fetch_statement_inv … EQfetch)))
811  * whd in match (point_of_label ????); * #H #_ #_ % #H1 @H <H1 whd in match succ_pc;
812  whd in match point_of_pc; whd in match pc_of_point; normalize nodelta
813  >point_of_offset_of_point %
814]
815qed.
816
817lemma general_eval_seq_no_call_premain_ok :∀ P_in , P_out: sem_graph_params.
818∀prog : joint_program P_in.
819∀stack_sizes.
820∀ f_lbls,f_regs.∀f_bl_r.∀init.
821∀st_no_pc_rel,st_rel.
822let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in
823let trans_prog  ≝ b_graph_transform_program P_in P_out init prog in
824let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in
825good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs
826                    st_no_pc_rel st_rel →
827∀st1,st1' : joint_abstract_status prog_pars_in.
828∀st2 : joint_abstract_status prog_pars_out.
829∀f.∀fn : joint_closed_internal_function P_in ?.
830∀stmt,nxt.
831block_id … (pc_block (pc … st1)) = -1 →
832st_rel st1 st2 →
833 let seq ≝ (step_seq P_in ? stmt) in
834  fetch_statement P_in …
835   (joint_globalenv P_in prog stack_sizes) (pc … st1) =
836     return 〈f, fn,  sequential ?? seq nxt〉 →
837 eval_state P_in … (joint_globalenv P_in prog stack_sizes)
838  st1 = return st1' →
839∃st2'. st_rel st1' st2' ∧           
840∃taf : trace_any_any_free (joint_abstract_status prog_pars_out) st2 st2'.           
841bool_to_Prop (taaf_non_empty … taf) ∧
842as_label (joint_abstract_status prog_pars_in) st1' =
843 as_label (joint_abstract_status prog_pars_out) st2'.
844#p_in #p_out #prog #stack_size #f_lbls #f_regs #init_regs #init #st_no_pc_rel
845#st_rel #good #st1 #st1' #st2 #f #fn #stmt #nxt #EQbl #Rst1st2 #EQfetch
846#EQeval cases(pre_main_ok … good …  EQbl EQeval Rst1st2) #Hclass * #st2'
847** #Rst1st2' #EQst2' #Hlab %{st2'} %{Rst1st2'} %{(taaf_step … (taa_base …) …)}
848[ whd change with (joint_classify ???) in ⊢ (??%?); <Hclass whd in match joint_classify;
849  normalize nodelta >EQfetch %
850| assumption
851]
852%{I} assumption
853qed.
854
855lemma general_eval_cost_ok :
856∀ P_in , P_out: sem_graph_params.
857∀prog : joint_program P_in.
858∀stack_sizes.
859∀ f_lbls,f_regs.∀f_bl_r.∀init.
860∀st_no_pc_rel,st_rel.
861let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in
862let trans_prog  ≝ b_graph_transform_program P_in P_out init prog in
863let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in
864good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs
865                    st_no_pc_rel st_rel →
866∀st1,st1' : joint_abstract_status prog_pars_in.
867∀st2 : joint_abstract_status prog_pars_out.
868∀f.
869∀fn : joint_closed_internal_function P_in ?.∀c,nxt.
870block_id … (pc_block (pc … st1)) ≠ -1 →
871st_rel st1 st2 →
872let cost ≝ COST_LABEL P_in ? c in
873 fetch_statement P_in …
874  (joint_globalenv P_in prog stack_sizes) (pc … st1) =
875    return 〈f, fn,  sequential ?? cost nxt〉 →
876 eval_state P_in … (ev_genv … prog_pars_in)
877            st1 = return st1' →
878∃ st2'. st_rel st1' st2' ∧
879∃taf : trace_any_any_free
880        (joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes))
881        st2 st2'.
882bool_to_Prop (taaf_non_empty … taf) ∧
883as_label (joint_abstract_status prog_pars_in) st1' =
884 as_label (joint_abstract_status prog_pars_out) st2'.
885#P_in #P_out #prog #stack_size #f_lbls #f_regs #f_bl_r #init #st_no_pc_rel
886#st_rel #goodR #st1 #st1' #st2 #f #fn #c #nxt * #Hbl #Rst1st2 normalize nodelta
887#EQfetch
888whd in match eval_state; whd in match eval_statement_no_pc; normalize nodelta
889>EQfetch >m_return_bind normalize nodelta >m_return_bind whd in ⊢ (??%% → ?);
890#EQ destruct(EQ)
891%{(mk_state_pc ? (st_no_pc … st2) (pc_of_point P_out (pc_block (pc … st2)) nxt)
892                 (last_pop … st2))}
893cut(? : Prop) [3: #Hfin % [@Hfin] |
894| cases(fetch_statement_inv … EQfetch) #EQfn #_
895  <(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch)
896  whd in match (succ_pc ???); whd in match (point_of_succ ???);
897  >set_no_pc_eta
898  @(st_rel_def … prog … stack_size … goodR
899          (st_no_pc … st1) (st_no_pc … st2)) [3: >EQfn in ⊢ (??%?); %|1,2:]
900  [ @(cost_commutation … prog … stack_size … goodR … EQfetch) [ % assumption]
901    @(fetch_stmt_ok_sigma_state_ok … goodR … Rst1st2 EQfetch)
902  | @(fetch_stmt_ok_sigma_last_pop_ok … goodR … Rst1st2 EQfetch)
903  ]
904]
905lapply(b_graph_transform_program_fetch_statement … goodR (pc … st1) f fn ?)
906  [2: @eqZb_elim [ #ABS @⊥ >ABS in Hbl; #H @H %] #_ normalize nodelta
907      #H cases(H EQfetch) -H |*:]
908  #init_data * #t_fn ** >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch)
909  #EQt_fn #Hinit normalize nodelta * #bl *
910  @if_elim @eq_identifier_elim [2: #_ cases(not_emptyb ??) *]
911  [ #EQentry inversion(not_emptyb ??) [2: #_ *] #non_empty_pre #_ whd in ⊢ (% → ?);
912    inversion (f_regs ??) [2: #x #y #_ #_ *] #EQregs normalize nodelta #EQ destruct(EQ)
913    whd in ⊢ (% → ?); * #pre * #mid1 * #mid2 * #post *** #EQmid1 whd in ⊢ (% → ?);
914    * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in ⊢ (% → ?); * #nxt1 * #EQt_stmt
915    change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) whd in ⊢ (% → ?);
916    * #EQ1 #EQ2 destruct(EQ1 EQ2)
917  | #EQentry inversion(not_emptyb ??) [ #_ *] #empty_pre #_
918    >(f_step_on_cost … init_data) whd in ⊢ (% → ?); inversion(f_regs ??) [2: #x #y #_ #_ *]
919   #EQregs normalize nodelta #EQ destruct(EQ) whd in ⊢ (% → ?); * #pre * #mid1 *
920   #mid2 * #post *** #EQmid1 * #EQ1 #EQ2 destruct(EQ1 EQ2) * #nxt1 * #EQt_stmt
921   change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) * #EQ1 #EQ2 destruct(EQ1 EQ2)
922  | #EQentry #_  >(f_step_on_cost … init_data) whd in ⊢ (% → ?);
923    inversion(f_regs ??) [2: #x #y #_ #_ *] #EQregs normalize nodelta #EQ destruct(EQ)
924    * #pre * #mid1 * #mid2 * #post *** #EQmid1 * #EQ1 #EQ2 destruct(EQ1 EQ2) *
925    #nxt1 * #EQt_stmt change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ)
926    * #EQ1 #EQ2 destruct(EQ1 EQ2)
927  ] 
928  %{(taaf_step … (taa_base …) …)}
929  [3,6,9: %{I}
930  |*: whd whd in ⊢ (??%?); whd in match fetch_statement; normalize nodelta
931     >EQt_fn >m_return_bind >EQt_stmt >m_return_bind %
932  ]
933cases(fetch_stmt_ok_succ_ok … nxt … EQfetch) [4,8,12: % |2,6,10: |3,7,11: % %]
934#stmt' #EQstmt'  @(as_label_ok_non_entry … goodR)
935[4,11,18: @EQstmt'
936|1,2,3,8,9,10,15,16,17:
937|5,12,19: % assumption
938|6,13,20: assumption
939|*: cases(entry_unused ??? (pi2 ?? fn) ?? (proj2 ?? (fetch_statement_inv … EQfetch)))
940  * whd in match (point_of_label ????); * #H #_ #_ % #H1 @H <H1 whd in match succ_pc;
941  whd in match point_of_pc; whd in match pc_of_point; normalize nodelta
942  >point_of_offset_of_point %
943]
944qed.
945
946lemma general_eval_cost_premain_ok :
947∀ P_in , P_out: sem_graph_params.
948∀prog : joint_program P_in.
949∀stack_sizes.
950∀ f_lbls,f_regs.∀f_bl_r.∀init.
951∀st_no_pc_rel,st_rel.
952let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in
953let trans_prog  ≝ b_graph_transform_program P_in P_out init prog in
954let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in
955good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs
956                    st_no_pc_rel st_rel →
957∀st1,st1' : joint_abstract_status prog_pars_in.
958∀st2 : joint_abstract_status prog_pars_out.
959∀f.
960∀fn : joint_closed_internal_function P_in ?.∀c,nxt.
961block_id … (pc_block (pc … st1)) = -1 →
962st_rel st1 st2 →
963let cost ≝ COST_LABEL P_in ? c in
964 fetch_statement P_in …
965  (joint_globalenv P_in prog stack_sizes) (pc … st1) =
966    return 〈f, fn,  sequential ?? cost nxt〉 →
967 eval_state P_in … (ev_genv … prog_pars_in)
968            st1 = return st1' →
969∃ st2'. st_rel st1' st2' ∧
970∃taf : trace_any_any_free
971        (joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes))
972        st2 st2'.
973bool_to_Prop (taaf_non_empty … taf) ∧
974as_label (joint_abstract_status prog_pars_in) st1' =
975 as_label (joint_abstract_status prog_pars_out) st2'.
976#p_in #p_out #prog #stack_size #f_lbls #f_regs #init_regs #init #st_no_pc_rel #st_rel
977#good #st1 #st1' #st2 #f #fn #c #nxt #EQbl #Rst1st2 #EQfetch #EQeval
978cases(pre_main_ok … good …  EQbl EQeval Rst1st2) #Hclass * #st2'
979** #Rst1st2' #EQst2' #Hlab %{st2'} %{Rst1st2'} %{(taaf_step … (taa_base …) …)}
980[ whd change with (joint_classify ???) in ⊢ (??%?); <Hclass
981  whd in match joint_classify; normalize nodelta >EQfetch %
982| assumption
983]
984%{I} assumption
985qed.
986
987lemma next_of_call_pc_inv :  ∀pars.∀prog. ∀stack_size.
988∀pc,nxt.
989next_of_call_pc pars … (ev_genv … (mk_prog_params pars prog stack_size)) pc
990= return nxt →
991∃id,fn,c_id,c_args,c_dest.
992fetch_statement pars
993    … (ev_genv … (mk_prog_params pars prog stack_size)) pc =
994    return 〈id,fn, sequential ? ?(CALL pars ? c_id c_args c_dest) nxt〉.
995#pars #prog #init #pc #nxt whd in match next_of_call_pc; normalize nodelta
996#H @('bind_inversion H) -H ** #id #fn *
997[ *[ #c | #c_id #c_arg #c_dest | #reg #lbl | #seq ] #prox | #fin | #H #r #l #l ]
998#EQfetch normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ)
999%{id} %{fn} %{c_id} %{c_arg} %{c_dest} assumption
1000qed.
1001
1002lemma stored_pc_inj :
1003∀p_in,p_out,prog,stack_size,init,init_regs,f_lbls,f_regs,pc,pc'.
1004sigma_pc_opt p_in p_out prog stack_size init init_regs f_lbls f_regs pc ≠ None ? →
1005block_id (pc_block pc) ≠ OZ →
1006sigma_stored_pc p_in p_out prog stack_size init init_regs f_lbls f_regs pc =
1007sigma_stored_pc p_in p_out prog stack_size init init_regs f_lbls f_regs pc' →
1008pc = pc'.
1009#p_in #p_out #prog #stack_size #init #init_regs #f_lbls #f_regs #pc #pc' #H *#H1
1010whd in match sigma_stored_pc; normalize nodelta
1011 inversion(sigma_pc_opt ?????????) [ #ABS >ABS in H; * #H @⊥ @H %] #pc1 #EQpc1
1012normalize nodelta inversion(sigma_pc_opt ?????????)
1013[ #ABS normalize nodelta #EQ destruct(EQ) lapply EQpc1 whd in match sigma_pc_opt;
1014  normalize nodelta @if_elim
1015  [ #Hbl whd in ⊢ (??%? → ?); #EQ destruct(EQ) lapply(Hbl) -Hbl @eqZb_elim
1016    [whd in ⊢ (??%% → ?); #EQ destruct(EQ)] @eqZb_elim [#ABS >ABS in H1; #H @⊥ @H %]
1017    @⊥ @H1 %]
1018  #Hbl normalize nodelta #H @('bind_inversion H) -H #lbl whd in match sigma_label;
1019  normalize nodelta >code_block_of_block_eq >m_return_bind
1020  >fetch_internal_function_no_zero [ whd in ⊢ (??%% → ?); #EQ destruct(EQ)]
1021  >(pc_block_eq … H) whd in match sigma_stored_pc; normalize nodelta >EQpc1 %
1022]
1023#pc2 #EQpc2 normalize nodelta #EQ destruct(EQ)
1024@(sigma_stored_pc_inj p_in p_out prog stack_size init init_regs f_lbls f_regs …)
1025[ assumption] >EQpc1 >EQpc2 %
1026qed.
1027
1028lemma eval_return_ok :
1029∀ P_in , P_out: sem_graph_params.
1030∀prog : joint_program P_in.
1031∀stack_sizes.
1032∀ f_lbls,f_regs.∀f_bl_r.∀init.
1033∀st_no_pc_rel,st_rel.
1034let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in
1035let trans_prog  ≝ b_graph_transform_program P_in P_out init prog in
1036let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in
1037∀good : good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs
1038                    st_no_pc_rel st_rel.
1039∀st1,st1' : joint_abstract_status prog_pars_in.
1040∀st2 : joint_abstract_status prog_pars_out.
1041∀f.
1042∀fn : joint_closed_internal_function P_in ?.
1043block_id … (pc_block (pc … st1)) ≠ -1 →
1044st_rel st1 st2 →
1045 fetch_statement P_in …
1046  (joint_globalenv P_in prog stack_sizes) (pc … st1) =
1047    return 〈f, fn,final P_in ? (RETURN …)〉 →
1048 eval_state P_in … (ev_genv … prog_pars_in)
1049            st1 = return st1' →
1050∃st2_ret,st2_after_ret,st2' : joint_abstract_status prog_pars_out.
1051∃taa2 : trace_any_any … st2 st2_ret.
1052∃taa2' : trace_any_any_free … st2_after_ret st2'.
1053(if taaf_non_empty … taa2' then ¬as_costed … st2_after_ret else True) ∧
1054as_classifier … st2_ret cl_return ∧
1055        as_execute … st2_ret st2_after_ret ∧ st_rel st1' st2' ∧
1056        ret_rel ?? (JointStatusSimulation … good) st1' st2_after_ret ∧
1057as_label (joint_abstract_status prog_pars_in) st1' =
1058 as_label (joint_abstract_status prog_pars_out) st2'.
1059#p_in #p_out #prog #stack_size #f_lbls #f_regs #init_regs #init #st_no_pc_rel
1060#st_rel #good #st1 #st1' #st2 #f #fn #Hbl #Rst1st2 #EQfetch
1061whd in match eval_state; normalize nodelta >EQfetch >m_return_bind
1062whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
1063whd in match eval_statement_advance; whd in match eval_return; normalize nodelta
1064#H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H #ssize
1065#H lapply(opt_eq_from_res ???? H) -H change with (stack_size f) in ⊢ (??%? → ?);
1066#EQssize #H @('bind_inversion H) -H * #st_pop #pc_pop #EQpop #H @('bind_inversion H)
1067-H #next_of_call #EQnext_of_call whd in ⊢ (??%% → ?); whd in match next;
1068whd in match set_last_pop; whd in match set_pc; normalize nodelta #EQ destruct(EQ)
1069lapply(b_graph_transform_program_fetch_statement … good (pc … st1) f fn ?)
1070[2: @eqZb_elim [ #ABS @⊥ >ABS in Hbl; * #H @H %] #_ normalize nodelta
1071      #H cases(H EQfetch) -H |*:]
1072#data * #t_fn ** #EQt_fn >(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in EQt_fn;
1073#EQt_fn #Hinit normalize nodelta ** #pre #fin_s * #Hregs * #pre * #mid
1074** #EQmid #EQpre whd in ⊢ (% → ?); #EQt_stmt
1075cases(next_of_call_pc_inv … EQnext_of_call) #f1 * #fn1 * #id * #args * #dest #EQcall
1076<(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in Hregs; #Hregs
1077cases(bind_new_bind_new_instantiates' … Hregs ((bind_new_bind_new_instantiates' … Hinit
1078 (return_commutation ?????????? good … Hbl EQfetch … EQssize … EQpop … EQcall …
1079   Rst1st2 t_fn EQt_fn)) ? ))
1080[2: @sym_eq >(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch)
1081    @(bind_new_bind_new_instantiates' … Hinit (pi2 ?? (init ? fn))) ] 
1082#EQ destruct(EQ) * #st_fin * #EQst_fin * #t_st_pop * #t_pc_pop
1083** #EQt_pop #EQt_pc_pop @eqZb_elim #Hbl_pcpop normalize nodelta
1084[ * #sem_rel #EQt_next
1085  %{(mk_state_pc ? st_fin (pc_of_point p_out (pc_block (pc … st2)) mid) (last_pop … st2))}
1086  %{(mk_state_pc ? (decrement_stack_usage p_out ssize t_st_pop)
1087      (pc_of_point p_out (pc_block t_pc_pop) next_of_call) t_pc_pop)}
1088  %{(mk_state_pc ? (decrement_stack_usage p_out ssize t_st_pop)
1089      (pc_of_point p_out (pc_block t_pc_pop) next_of_call) t_pc_pop)}
1090  %{((taaf_to_taa …
1091     (produce_trace_any_any_free ? st2 f t_fn … EQt_fn EQpre EQst_fin) ?))}
1092 [ @if_elim #_ [2: @I] % * #H @H -H whd in ⊢ (??%?); whd in match fetch_statement;
1093 normalize nodelta >EQt_fn >m_return_bind >point_of_pc_of_point >EQt_stmt % ]
1094 %{(taaf_base …)} cut(? : Prop)
1095 [3: #Hfin % [ %
1096 [ % [ % [%{I} ]
1097       whd [whd in ⊢ (??%?); | whd in match eval_state;] whd in match fetch_statement;
1098       normalize nodelta >EQt_fn >m_return_bind >point_of_pc_of_point >EQt_stmt [%]
1099       >m_return_bind whd in match eval_statement_no_pc; normalize nodelta
1100       >m_return_bind whd in match eval_statement_advance; whd in match eval_return;
1101       normalize nodelta whd in match (stack_sizes ????); >EQssize >m_return_bind
1102       >EQt_pop >m_return_bind >EQt_next >m_return_bind %
1103     | @Hfin
1104     ]
1105 | whd * #s1_pre #s1_call cases (joint_classify_call … s1_call) * #calling_i
1106   #calling * #id1 * #arg1 * #dest1 * #nxt' #EQfetch_call * #s2_pre #s2_call
1107   whd in ⊢ (% → ?); >EQfetch_call normalize nodelta * #EQ destruct(EQ)
1108   whd in ⊢ (??%% → ?); whd in match (point_of_succ ???);
1109   whd in match (point_of_succ ???); #EQ cut(next_of_call =nxt')
1110   [ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) cases next_of_call in e0; #x
1111     normalize nodelta whd in match (offset_of_point ??); cases nxt' #y
1112     normalize nodelta #EQ1 destruct(EQ1) % ]
1113   -EQ #EQ destruct(EQ) whd in ⊢ (% → ?); <EQt_pc_pop #EQ1
1114     lapply(stored_pc_inj … EQ1)
1115     [2: % #ABS cases(fetch_statement_inv … EQcall) <EQt_pc_pop
1116       >fetch_internal_function_no_zero [#EQ destruct] whd in match sigma_stored_pc;
1117       normalize nodelta >ABS %
1118     | % #ABS cases(next_of_call_pc_inv … EQt_next) #x * #y * #z * #w * #a
1119       whd in match fetch_statement; normalize nodelta >fetch_internal_function_no_zero
1120       [whd in ⊢ (??%% → ?); #EQ destruct(EQ) ] assumption
1121     ] #EQ2 destruct(EQ2) whd
1122     cases(next_of_call_pc_inv … EQt_next) #id'' * #fn'' * #c_id'' * #c_args''
1123     * #c_dest'' #EQ3 >EQ3 normalize nodelta % [%] % ] ]
1124  |2:  whd in match succ_pc; normalize nodelta whd in match (point_of_succ ???);
1125       destruct(EQt_pc_pop) lapply(proj1 ?? (fetch_statement_inv … EQcall))
1126       <pc_block_eq in Hbl_pcpop sem_rel ⊢ %;
1127       [2: % #H cases(fetch_statement_inv … EQcall) >fetch_internal_function_no_zero
1128       [ #EQ destruct] whd in match sigma_stored_pc; normalize nodelta >H %]
1129       #Hbl_pcpop #sem_rel #EQ @(st_rel_def … good … sem_rel … ) [3: @EQ |1,2:] %
1130  |
1131  ]
1132 cases(fetch_stmt_ok_succ_ok … next_of_call … EQcall) [4: % |3: % % |2:]
1133 #stmt' #EQstmt' cases(decidable_eq_Z (block_id (pc_block pc_pop)) (neg one))
1134 [ #Hbl @(as_label_premain_ok ?????????? good) [assumption | assumption ]
1135 | #Hbl_pc_pop @(as_label_ok_non_entry … good)
1136   [4: @EQstmt'
1137   |1,2,3:
1138   | assumption
1139   | assumption
1140   |  cases(entry_unused ??? (pi2 ?? fn1) ?? (proj2 ?? (fetch_statement_inv … EQcall)))
1141     * whd in match (point_of_label ????); * #H #_ #_ % >point_of_pc_of_point
1142     #H1 @H <H1 %
1143   ]
1144 ]
1145]   
1146cases(fetch_statement_sigma_stored_pc … good … Hbl_pcpop … EQcall) #data1 * #Hinit1
1147normalize nodelta *** #pre_c #instr_c #post_c * #Hregs1 * #pc1 * destruct(EQt_pc_pop)
1148whd in match sigma_stored_pc in ⊢ (% → ?); normalize nodelta
1149inversion(sigma_pc_opt ???????? t_pc_pop)
1150[ #ABS cases(fetch_statement_inv … EQcall) >fetch_internal_function_no_zero [#EQ destruct(EQ)]
1151  whd in match sigma_stored_pc; normalize nodelta >ABS %]
1152#pc2 #EQpc2 normalize nodelta inversion(sigma_pc_opt ?????????)
1153[ #_ normalize nodelta #EQ destruct(EQ) cases(fetch_statement_inv … EQcall)
1154  >fetch_internal_function_no_zero [2: whd in match sigma_stored_pc; normalize nodelta >EQpc2 %]
1155  #EQ destruct(EQ) ]
1156#pc3 #EQpc3 normalize nodelta #EQ destruct(EQ) <EQpc2 in EQpc3; #H lapply(sym_eq ??? H) -H #H
1157lapply(sigma_stored_pc_inj … H) [ >EQpc2 % #EQ destruct] #EQ destruct(EQ) * #t_fn1 * #nxt1
1158* #pre * #post @eq_identifier_elim
1159[ #EQentry cases(entry_is_cost … (pi2 ?? fn1)) #nxt1 * #c <EQentry #ABS
1160  cases(fetch_statement_inv … EQcall) #_ normalize nodelta >ABS #EQ destruct(EQ) ]
1161#_ cut(∀x : bool.andb x false = false) [* %] #EQ >EQ -EQ normalize nodelta ***
1162cases(bind_new_bind_new_instantiates' … (bind_instantiates_to_instantiate … Hregs1)
1163 (bind_new_bind_new_instantiates' … (bind_instantiates_to_instantiate … Hinit1)
1164  ((call_is_call … good … (proj1 … (fetch_statement_inv … EQcall))) id args dest ?)) (point_of_pc p_in pc1))
1165#id' * #args' * #dest' #EQ >EQ -EQ #EQt_call #EQpre_c #EQpost_c #EQnxt1 #H
1166cases(bind_new_bind_new_instantiates' … (bind_instantiates_to_instantiate … Hregs1)
1167      (bind_new_bind_new_instantiates' … (bind_instantiates_to_instantiate … Hinit1) H))
1168-H #st2' * #EQst2' #fin_sem_rel
1169%{(mk_state_pc ? st_fin (pc_of_point p_out (pc_block (pc … st2)) mid) (last_pop … st2))}
1170%{(next p_out nxt1
1171   (set_last_pop p_out (decrement_stack_usage ? ssize t_st_pop) pc1))}
1172%{(mk_state_pc ? st2' (pc_of_point p_out (pc_block pc1) next_of_call) pc1)}
1173%{((taaf_to_taa …
1174     (produce_trace_any_any_free ? st2 f t_fn … EQt_fn EQpre EQst_fin) ?))}
1175[ @if_elim #_ [2: @I] % whd in ⊢ (% → ?); whd in match (as_label ??);
1176  whd in match fetch_statement; normalize nodelta >EQt_fn >m_return_bind
1177  >point_of_pc_of_point >EQt_stmt >m_return_bind normalize nodelta * #H @H % ]
1178letin trans_prog ≝ (b_graph_transform_program p_in p_out init prog)
1179lapply(produce_trace_any_any_free (mk_prog_params p_out trans_prog stack_size) ??????????)
1180[11: * #taaf * #_ #prf %{taaf}
1181|3: change with (pc_block pc1) in match (pc_block ?);
1182    @(proj1 … (fetch_statement_inv … EQt_call))
1183|2: whd in match next; whd in match succ_pc; whd in match set_pc;
1184    whd in match point_of_pc; normalize nodelta whd in match pc_of_point;
1185    normalize nodelta >point_of_offset_of_point in ⊢ (????%???);
1186    whd in match (point_of_succ ???); @EQpost_c
1187|1: assumption
1188|*:
1189]
1190cut(? : Prop)
1191[3: #Hfin %
1192  [ %
1193    [ %
1194      [2: @Hfin
1195      | %
1196        [ %
1197          [ @if_elim [2: #_ @I] #H lapply(prf H) cases post_c in EQpost_c; [#_ *]
1198            #hd #tl whd in ⊢ (% → ?); * #lab * #rest ** #EQ destruct(EQ) *
1199            #succ * #EQnxt1 change with succ in ⊢ (??%? → ?); #EQ destruct(EQ)
1200            #EQrest #_ % whd in ⊢ (% → ?); whd in match (as_label ??);
1201            whd in match (as_pc_of ??); whd in match (point_of_succ ???);
1202            change with (pc_block pc1) in match (pc_block ?);
1203            whd in match fetch_statement; normalize nodelta
1204            >(proj1 … (fetch_statement_inv … EQt_call)) >m_return_bind
1205            whd in match point_of_pc; normalize nodelta >point_of_offset_of_point
1206            >EQnxt1 >m_return_bind normalize nodelta whd in match cost_label_of_stmt;
1207            normalize nodelta * #H @H % ]
1208    ]
1209    whd [ whd in match (as_classify ??); | whd in match eval_state; normalize nodelta]
1210    whd in match fetch_statement; normalize nodelta >EQt_fn >m_return_bind
1211    >point_of_pc_of_point >EQt_stmt [%] >m_return_bind whd in match eval_statement_no_pc;
1212    normalize nodelta >m_return_bind whd in match eval_statement_advance;
1213    whd in match eval_return; normalize nodelta whd in match (stack_sizes ????);
1214    >EQssize >m_return_bind >EQt_pop >m_return_bind whd in match next_of_call_pc;
1215    normalize nodelta >EQt_call >m_return_bind %
1216    ]
1217  ]
1218]
1219|
1220| whd in match succ_pc; normalize nodelta <(pc_block_eq) [2: >EQpc2 % #EQ destruct]
1221    whd in match (point_of_succ ???); @(st_rel_def … good)
1222    [3: change with (pc_block pc1) in match (pc_block ?);
1223        lapply(proj1 ?? (fetch_statement_inv … EQcall)) <pc_block_eq in ⊢ (% → ?);
1224        [2: >EQpc2 % #EQ destruct] #H @H
1225    |1,2:
1226    | <pc_block_eq in fin_sem_rel; [2: >EQpc2 % #EQ destruct] #H @H
1227    | %
1228    ]
1229  ]
1230[ whd * #s1_pre #s1_call cases (joint_classify_call … s1_call) * #calling_i 
1231  #calling * #call_spec * #arg * #dest * #nxt' #EQfetch_call * #s2_pre #s2_call
1232whd in ⊢ (% → ?); >EQfetch_call normalize nodelta * #EQpc1_pc_s1_pre  #EQsucc_pc
1233whd in ⊢ (% → ?); #EQpc_s1_pre >EQpc_s1_pre in EQfetch_call; #EQfetch_call
1234cases(fetch_statement_sigma_stored_pc … good … EQfetch_call)
1235[2: <EQpc_s1_pre % #ABS elim Hbl_pcpop #H @H -H >EQpc1_pc_s1_pre assumption ]
1236#data2 * #EQdata2 normalize nodelta * #bl2 * #EQbl2 * #pc3 * #EQstored
1237lapply(stored_pc_inj … (sym_eq ??? EQstored))
1238[2: % #ABS cases(fetch_statement_inv … EQfetch_call) >fetch_internal_function_no_zero
1239  [ #EQ destruct(EQ)] whd in match sigma_stored_pc; normalize nodelta >ABS %
1240| % #ABS cases(fetch_statement_inv … EQfetch_call) >fetch_internal_function_no_zero
1241  [2: <pc_block_eq [assumption] % #ABS1 cases(fetch_statement_inv … EQfetch_call)
1242      whd in match sigma_stored_pc; normalize nodelta >ABS1
1243      >fetch_internal_function_no_zero [2: %]  ] whd in ⊢ (??%% → ?); #EQ destruct
1244]
1245#EQ destruct(EQ) * #fn' * #nxt'' * #l1 * #l2 @eq_identifier_elim
1246[ #EQentry cases(fetch_statement_inv … EQfetch_call) #_ >EQentry normalize nodelta
1247  cases(entry_is_cost … (pi2 ?? calling)) #nxt1 * #c #EQ >EQ #EQ1 destruct]
1248#_ cut(∀b : bool.andb b false = false) [ * //] #EQ >EQ -EQ normalize nodelta
1249*** #EQt_fetch_call #_ #_ #EQnxt' whd >EQt_fetch_call normalize nodelta
1250cut(? : Prop)
1251[3: whd in match (last_pop ??); #H %{H}
1252|2: @(stored_pc_inj p_in p_out prog stack_size init init_regs f_lbls f_regs … )
1253  [ % #ABS cases(fetch_statement_inv … EQcall) >fetch_internal_function_no_zero
1254   [#EQ destruct] whd in match sigma_stored_pc; normalize nodelta >ABS %
1255  |3: >EQpc1_pc_s1_pre assumption
1256  | % #ABS cases(fetch_statement_inv … EQt_call) >fetch_internal_function_no_zero
1257    [2: assumption] #EQ destruct
1258  ]
1259|]
1260destruct(H)
1261cut(nxt'' = nxt1) [2: #EQ destruct whd in ⊢ (??%%); % ]
1262cut(nxt' = next_of_call)
1263[ lapply EQsucc_pc whd in match (succ_pc); normalize nodelta
1264  whd in match (point_of_succ ???); whd in match (point_of_succ ???);
1265  whd in ⊢ (??%% → ?); cases next_of_call #x cases nxt' #y
1266  whd in match (offset_of_point ??); whd in match (offset_of_point ??);
1267  #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) % ]
1268#EQ destruct(EQ) >EQcall in EQfetch_call; >EQt_call in EQt_fetch_call;
1269whd in ⊢ (? → ??%? → ?); #EQ1 #EQ2 lapply(eq_to_jmeq ??? EQ1) -EQ1 #EQ1 destruct(EQ1) %
1270]
1271cases(fetch_stmt_ok_succ_ok … next_of_call … EQcall) [4: % |3: % % |2:]
1272 #stmt' #EQstmt' cases(decidable_eq_Z (block_id (pc_block pc1)) (neg one))
1273 [ #Hbl  @(as_label_premain_ok ?????????? good)
1274   [ change with (pc_block (sigma_stored_pc ?????????)) in match (pc_block ?);
1275     <pc_block_eq [ assumption] % #ABS cases(fetch_statement_inv … EQstmt')
1276     >fetch_internal_function_no_zero [#EQ destruct] whd in match sigma_stored_pc;
1277     normalize nodelta >ABS %
1278   | assumption
1279   ]
1280 | #Hbl_pc_pop @(as_label_ok_non_entry … good)
1281   [4: @EQstmt'
1282   |1,2,3:
1283   | assumption
1284   | assumption
1285   |  cases(entry_unused ??? (pi2 ?? fn1) ?? (proj2 ?? (fetch_statement_inv … EQcall)))
1286     * whd in match (point_of_label ????); * #H #_ #_ % >point_of_pc_of_point
1287     #H1 @H <H1 %
1288   ]
1289]
1290qed.
1291
1292lemma eval_call_ok : ∀ P_in , P_out: sem_graph_params.
1293∀prog : joint_program P_in.
1294∀stack_size.
1295∀ f_lbls,f_regs.∀init_regs.∀init.
1296∀st_no_pc_rel,st_rel.
1297let prog_pars_in ≝ mk_prog_params P_in prog stack_size in
1298let trans_prog  ≝ b_graph_transform_program P_in P_out init prog in
1299let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_size in
1300∀good : good_state_relation P_in P_out prog stack_size init init_regs f_lbls f_regs
1301                    st_no_pc_rel st_rel.
1302∀st1,st1' : joint_abstract_status prog_pars_in.
1303∀st2 : joint_abstract_status prog_pars_out.
1304∀f.
1305∀fn : joint_closed_internal_function P_in ?.
1306∀id,arg,dest,nxt.
1307block_id … (pc_block (pc … st1)) ≠ -1 →
1308st_rel st1 st2 →
1309 fetch_statement P_in …
1310  (joint_globalenv P_in prog stack_size) (pc … st1) =
1311    return 〈f, fn,sequential P_in ? (CALL ?? id arg dest) nxt〉 →
1312 eval_state P_in … (ev_genv … prog_pars_in)
1313            st1 = return st1' →
1314∃is_call,st2_pre_call,t_is_call.
1315as_call_ident (joint_abstract_status prog_pars_in) «st1,is_call» =
1316 as_call_ident (joint_abstract_status prog_pars_out) «st2_pre_call,t_is_call» ∧
1317(pc … st1) = sigma_stored_pc P_in P_out prog stack_size
1318 init init_regs f_lbls f_regs (pc … st2_pre_call) ∧
1319∃st2_after_call,st2' : joint_abstract_status prog_pars_out.
1320∃taa2 : trace_any_any … st2 st2_pre_call.
1321∃taa2' : trace_any_any … st2_after_call st2'.
1322eval_state P_out … (joint_globalenv P_out trans_prog stack_size) st2_pre_call =
1323return st2_after_call ∧
1324st_rel st1' st2' ∧
1325as_label (joint_abstract_status prog_pars_in) st1' =
1326as_label (joint_abstract_status prog_pars_out) st2_after_call.
1327#p_in #p_out #prog #stack_size #f_lbls #f_regs #init_regs #init #st_no_pc_rel #st_rel
1328#good #st1 #st1' #st2 #f #fn #id #arg #dest #nxt #Hbl #Rst1st2 #EQfetch
1329whd in match eval_state in ⊢ (% → ?); normalize nodelta >EQfetch >m_return_bind
1330whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
1331#H @('bind_inversion H) -H #bl >set_no_pc_eta #H lapply(err_eq_from_io ????? H) -H
1332#EQbl #H @('bind_inversion H) -H * #f1 *
1333#fn1 #H lapply(err_eq_from_io ????? H) -H #EQfn1 normalize nodelta
1334[2: #H @('bind_inversion H) -H #x whd in match eval_external_call; normalize nodelta
1335    #H @('bind_inversion H) -H #y #_ #H @('bind_inversion H) -H #z #_
1336    #H @('bind_inversion H) -H #w whd in ⊢ (??%% → ?); #ABS destruct(ABS) ]
1337#H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H #st1_save #EQst1_save
1338#H @('bind_inversion H) -H #st1_no_pc' whd in match eval_internal_call;
1339normalize nodelta change with (stack_size ?) in match (stack_sizes ????); #H
1340@('bind_inversion H) -H #ssize #H lapply(opt_eq_from_res ???? H) -H #EQssize
1341#H @('bind_inversion H) -H #st1_no_pc'' #EQst1_no_pc'' whd in ⊢ (??%% → ?);
1342#EQ destruct(EQ) whd in ⊢ (??%% → ?); #EQ destruct(EQ)
1343% [@hide_prf whd in ⊢ (??%?); >EQfetch %]
1344cases(fetch_statement_sigma_stored_pc … good … Hbl EQfetch)
1345#data * #EQdata normalize nodelta *** #pre #instr #post * #Hregs * #pc' * #EQpc'
1346* #t_fn * #nxt' * #l1 * #l2 @eq_identifier_elim
1347[ #EQentry cases(fetch_statement_inv … EQfetch) #_ >EQentry normalize nodelta
1348  cases(entry_is_cost … (pi2 ?? fn)) #nxt1 * #c #EQ >EQ #ABS destruct(ABS) ]
1349#_ cut(∀b.andb b false = false) [* %] #EQ ** >EQ -EQ normalize nodelta *
1350#EQt_call #EQpre #EQpost #_
1351lapply(b_graph_transform_program_fetch_internal_function … good … bl f1 fn1)
1352@eqZb_elim [ normalize nodelta #ABS @⊥ cases(block_of_call_no_minus_one … EQbl) >ABS #H @H %]
1353#_ normalize nodelta #H cut(? : Prop)
1354[3: #EQint_fn cases(H EQint_fn) -H
1355|2: whd in match fetch_internal_function; normalize nodelta >EQfn1 %|*:]
1356#data1 * #t_fn1 ** #EQt_fn1 #Hdata1 #good1
1357cases(bind_new_bind_new_instantiates' …  (bind_instantiates_to_instantiate … Hregs)
1358          (bind_new_bind_new_instantiates' …  (bind_instantiates_to_instantiate … EQdata)
1359           (call_is_call … good … )) … (point_of_pc p_out pc'))
1360[4: @(proj1 … (fetch_statement_inv … EQfetch)) |*:]
1361#id' * #args' * #dest' #EQinstr
1362cases(bind_new_bind_new_instantiates' … (bind_instantiates_to_instantiate … Hregs)
1363  ((bind_new_bind_new_instantiates' … (bind_instantiates_to_instantiate … EQdata)
1364 (call_commutation … good … Hbl EQfetch bl EQbl … EQint_fn … EQst1_save … EQssize …
1365   EQst1_no_pc'' … Rst1st2 … EQt_fn1)) ?) … EQpc' EQt_call EQinstr)
1366[2: @sym_eq
1367    @(bind_new_bind_new_instantiates' …
1368        (bind_instantiates_to_instantiate … EQdata) (pi2 ?? (init ? fn))) ]
1369#st2_pre ** #EQst2_pre #EQt_bl * #st2_save * #EQst2_save * #st2_after * #EQst2_after
1370#Hprologue
1371%{(mk_state_pc ? st2_pre pc' (last_pop … st2))}
1372%
1373[ @hide_prf whd in ⊢ (??%?); >EQt_call >EQinstr %]
1374%
1375[ % [2: @sym_eq assumption] whd in ⊢ (??%%);
1376  >EQfetch in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? ])?);
1377  >EQt_call in ⊢ (???(match % with [ _ ⇒ ? | _ ⇒ ? ])); normalize nodelta >EQbl
1378  >m_return_bind >EQint_fn normalize nodelta >EQinstr normalize nodelta
1379  >EQt_bl >m_return_bind >EQt_fn1 % ]
1380%{(mk_state_pc ? (increment_stack_usage p_out ssize st2_after)
1381   (pc_of_point p_out bl (joint_if_entry … t_fn1)) (last_pop … st2))}
1382cases(bind_new_bind_new_instantiates' … Hdata1 Hprologue)
1383[2: @sym_eq @(bind_new_bind_new_instantiates' … Hdata1 (pi2 ?? (init ? fn1)))] 
1384-Hprologue #st2' * #EQst2'
1385#fin_sem_rel cases good1 #_ #_ #_ #_ #_ #_ #_ #_ #_ #_ #_ cases(entry_is_cost … (pi2 ?? fn1))
1386#nxt1 * #c #EQcost #H lapply(H … EQcost) -H -good1 normalize nodelta
1387>(f_step_on_cost … data1) *** #pre1 #instr1 #post1 @eq_identifier_elim [2: * #H @⊥ @H %]
1388#_ cases(added_prologue … data1) in EQst2'; normalize nodelta
1389[ whd in ⊢ (??%% → ?); #EQ destruct(EQ)
1390| #hd #tl #EQst2'
1391]
1392* whd in ⊢ (% → ?); inversion(f_regs ??) normalize nodelta [2,4: #x #y #_ #_ *]
1393#EQf_regs #EQ [2: whd in EQ : (???%);] destruct(EQ) * #l1 * #mid1 * #mid2 * #l2 ***
1394#EQmid1 whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in ⊢ (% → ?); *
1395#nxt2 * [ #EQnop | #EQt_cost ] change with nxt2 in ⊢ (??%? → ?); #EQ destruct(EQ)
1396whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2)
1397[ * #star_lab * #Hstar_lab * #l1 * #mid1 * #mid2 * #l2 *** #EQmid1' whd in ⊢ (% → ?);
1398  * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in ⊢ (% → ?); * #nxt2 * #EQt_cost
1399  change with nxt2 in ⊢ (??%? → ?); #EQ destruct(EQ) #EQl2
1400| #EQentry
1401]
1402whd in EQmid1 : (??%%); destruct(EQmid1)
1403%{(mk_state_pc ? ? (pc_of_point p_out bl (joint_if_entry … fn1)) (last_pop … st2))}
1404[ @st2' |3: @(increment_stack_usage p_out ssize st2_after)]
1405>(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in EQpre; #EQpre
1406lapply(taaf_to_taa … (produce_trace_any_any_free … st2 f t_fn … EQpre … EQst2_pre) ?)
1407[3,6: <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) <EQpc' <pc_block_eq
1408      [2,4: inversion (sigma_pc_opt ?????????) [2,4: #x #_ % #ABS destruct(ABS) ]
1409            #ABS cases(fetch_statement_inv … EQfetch) <EQpc'
1410            >fetch_internal_function_no_zero [1,3: #EQ destruct]
1411            whd in match sigma_stored_pc; normalize nodelta >ABS %]
1412      >(pc_of_point_of_pc … pc') #taa1 %{taa1}
1413|1,4: @if_elim #_ [2,4: @I] % whd in ⊢ (% → ?); * #H @H -H whd in ⊢ (??%?);
1414      <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) <EQpc' <pc_block_eq
1415      [2,4: inversion (sigma_pc_opt ?????????) [2,4: #x #_ % #ABS destruct(ABS) ]
1416            #ABS cases(fetch_statement_inv … EQfetch) <EQpc'
1417            >fetch_internal_function_no_zero [1,3: #EQ destruct]
1418            whd in match sigma_stored_pc; normalize nodelta >ABS %]
1419      >(pc_of_point_of_pc … pc') whd in match (as_pc_of ??); >EQt_call
1420      >EQinstr %
1421|2,5: <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) <EQpc' <pc_block_eq
1422      [2,4: inversion (sigma_pc_opt ?????????) [2,4: #x #_ % #ABS destruct(ABS) ]
1423            #ABS cases(fetch_statement_inv … EQfetch) <EQpc'
1424            >fetch_internal_function_no_zero [1,3: #EQ destruct]
1425            whd in match sigma_stored_pc; normalize nodelta >ABS %]
1426      @(proj1 … (fetch_statement_inv … EQt_call))
1427]
1428-taa1
1429[ letin trans_prog ≝ (b_graph_transform_program ????)
1430  lapply(produce_trace_any_any_free (mk_prog_params p_out trans_prog stack_size)
1431         (mk_state_pc ? (increment_stack_usage p_out ssize st2_after)
1432           (pc_of_point p_out bl mid2) (last_pop … st2)) … EQst2')
1433  [ >point_of_pc_of_point in ⊢ (????%???); @EQl2
1434  | change with bl in match (pc_block ?); assumption
1435  |*:
1436  ]
1437  #taaf %{(taaf_to_taa … (taa_append_taaf … (taa_step … (taa_base …) …) taaf) ?)}
1438  [1,2: [ @if_elim #_ [2: @I] ] % whd in ⊢ (% → ?); * #H @H -H whd in ⊢ (??%?);
1439        whd in match (as_pc_of ??); whd in match fetch_statement; normalize nodelta
1440        >EQt_fn1 >m_return_bind whd in match point_of_pc; normalize nodelta
1441        >point_of_offset_of_point  [ >EQnop %] cases EQl2 #mid * #rest **
1442        #EQ destruct(EQ) * #nxt2 * #EQmid2 change with nxt2 in ⊢ (??%? → ?);
1443        #EQ destruct(EQ) #_ >EQmid2 %
1444  |3,4: whd [ whd in ⊢ (??%?); | whd in match eval_state; ]
1445        whd in match fetch_statement; normalize nodelta
1446        >EQt_fn1 >m_return_bind >point_of_pc_of_point >EQt_cost [%] >m_return_bind
1447        whd in match eval_statement_no_pc; normalize nodelta >m_return_bind %
1448  ]
1449| >EQentry %{(taa_base …)}
1450]
1451%
1452[2,4: whd in ⊢ (??%%); whd in match (as_pc_of ??);  whd in match (as_pc_of ??);
1453      whd in match fetch_statement; normalize nodelta >EQint_fn >EQt_fn1
1454      >m_return_bind >m_return_bind whd in match point_of_pc; normalize nodelta
1455      >point_of_offset_of_point >point_of_offset_of_point >EQcost >m_return_bind
1456      normalize nodelta >EQt_cost >m_return_bind [2: %] normalize nodelta
1457      whd in match get_first_costlabel; normalize nodelta whd in ⊢ (??%%);
1458      whd in match (get_first_costlabel_next ???);
1459      generalize in match (refl ??);
1460      >EQcost in ⊢ (∀e:???%. ???(??(???(match % return ? with [_ ⇒ ? | _ ⇒ ?]?))));
1461      #EQcost' normalize nodelta %
1462]
1463%
1464[1,3: whd in match eval_state; normalize nodelta >EQt_call >m_return_bind
1465      whd in match eval_statement_no_pc; normalize nodelta >EQinstr normalize nodelta
1466      >m_return_bind whd in match eval_statement_advance; whd in match eval_call;
1467      normalize nodelta >EQt_bl >m_return_bind @('bind_inversion EQt_fn1)
1468      * #f2 * #fn2 #EQ normalize nodelta whd in ⊢ (??%% → ?); #EQ1 destruct(EQ1)
1469      >EQ -EQ >m_return_bind normalize nodelta >EQst2_save >m_return_bind
1470      whd in match eval_internal_call; normalize nodelta whd in match (stack_sizes ????);
1471      >EQssize >m_return_bind >EQst2_after >m_return_bind [%] >EQentry %
1472|*: @(st_rel_def … good … fin_sem_rel …) [3,7: @EQint_fn |1,2,5,6:]
1473    @(fetch_stmt_ok_sigma_last_pop_ok … good … EQfetch) assumption
1474]
1475qed.
1476
1477lemma eval_call_premain_ok : ∀ P_in , P_out: sem_graph_params.
1478∀prog : joint_program P_in.
1479∀stack_size.
1480∀ f_lbls,f_regs.∀init_regs.∀init.
1481∀st_no_pc_rel,st_rel.
1482let prog_pars_in ≝ mk_prog_params P_in prog stack_size in
1483let trans_prog  ≝ b_graph_transform_program P_in P_out init prog in
1484let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_size in
1485∀good : good_state_relation P_in P_out prog stack_size init init_regs f_lbls f_regs
1486                    st_no_pc_rel st_rel.
1487∀st1,st1' : joint_abstract_status prog_pars_in.
1488∀st2 : joint_abstract_status prog_pars_out.
1489∀f.
1490∀fn : joint_closed_internal_function P_in ?.
1491∀id,arg,dest,nxt.
1492block_id … (pc_block (pc … st1)) = -1 →
1493st_rel st1 st2 →
1494 fetch_statement P_in …
1495  (joint_globalenv P_in prog stack_size) (pc … st1) =
1496    return 〈f, fn,sequential P_in ? (CALL ?? id arg dest) nxt〉 →
1497 eval_state P_in … (ev_genv … prog_pars_in)
1498            st1 = return st1' →
1499∃is_call,st2_pre_call,t_is_call.
1500as_call_ident (joint_abstract_status prog_pars_in) «st1,is_call» =
1501 as_call_ident (joint_abstract_status prog_pars_out) «st2_pre_call,t_is_call» ∧
1502(pc … st1) = sigma_stored_pc P_in P_out prog stack_size
1503 init init_regs f_lbls f_regs (pc … st2_pre_call) ∧
1504∃st2_after_call,st2' : joint_abstract_status prog_pars_out.
1505∃taa2 : trace_any_any … st2 st2_pre_call.
1506∃taa2' : trace_any_any … st2_after_call st2'.
1507eval_state P_out … (joint_globalenv P_out trans_prog stack_size) st2_pre_call =
1508return st2_after_call ∧
1509st_rel st1' st2' ∧
1510as_label (joint_abstract_status prog_pars_in) st1' =
1511as_label (joint_abstract_status prog_pars_out) st2_after_call.
1512#p_in #p_out #prog #stack_size #f_lbls #f_regs #init_regs #init #st_no_pc_rel #st_rel
1513#good #st1 #st1' #st2  #f #fn #id #arg #dest #nxt #EQbl #Rst1st2 #EQfetch #EQeval
1514% [ whd in ⊢ (??%?); >EQfetch %] %{st2} cases(pre_main_ok … good …  EQbl EQeval Rst1st2)
1515#Hclass * #st2' ** #Rst1st2' #EQst2' #Hlab %
1516[ change with (joint_classify ???) in ⊢ (??%?); <Hclass whd in ⊢ (??%?); >EQfetch %]
1517% [ % [2: whd in match sigma_stored_pc; whd in match sigma_pc_opt; normalize nodelta
1518          <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) >EQbl % ]
1519  | %{st2'} %{st2'} %{(taa_base …)} %{(taa_base …)} % [%{EQst2' Rst1st2'}]
1520    assumption
1521  ]
1522whd in ⊢ (??%%); >EQfetch in ⊢ (??(match % with [_ ⇒ ? | _ ⇒ ?])?); normalize nodelta
1523lapply Hclass whd in ⊢ (??%% → ?); >EQfetch in ⊢ (% → ?); whd in match joint_classify_step;
1524normalize nodelta inversion(fetch_statement ????) [2: #e #_ normalize nodelta #EQ destruct]
1525** #f' #fn' *
1526[ * [ #c | #id' #arg' #dest' | #r #lbl | #seq ] #nxt | * [ #lb || #h #id' #arg'] | *]
1527#EQt_fetch whd in ⊢ (??%% → ?); #EQ destruct normalize nodelta @('bind_inversion EQeval)
1528#x >EQfetch whd in ⊢ (??%% → ?); #EQ destruct(EQ) whd in match eval_statement_no_pc;
1529normalize nodelta >m_return_bind whd in match eval_statement_advance;
1530whd in match eval_call; normalize nodelta #H @('bind_inversion H) -H #bl #H
1531lapply(err_eq_from_io ????? H) -H #EQbl #H @('bind_inversion H) -H * #f1
1532* #fn1 #H lapply(err_eq_from_io ????? H) -H #EQfn1 normalize nodelta
1533[2: #H @('bind_inversion H) -H #st whd in match eval_external_call; normalize nodelta
1534   #H @('bind_inversion H) -H #x #_ #H @('bind_inversion H) -H #y #_
1535   #H @('bind_inversion H) -H #z whd in ⊢ (??%% → ?); #EQ destruct(EQ) ]
1536   #H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H #st1_save
1537   #_ #H @('bind_inversion H) -H #st1_fin #_ whd in ⊢ (??%% → ?); #EQ destruct(EQ)
1538   >EQbl >m_return_bind whd in match fetch_internal_function; normalize nodelta
1539   >EQfn1 >m_return_bind normalize nodelta @('bind_inversion EQst2') #x
1540   >EQt_fetch whd in ⊢ (??%% → ?); #EQ destruct(EQ) whd in match eval_statement_no_pc;
1541   normalize nodelta >m_return_bind whd in match eval_statement_advance;
1542   whd in match eval_call; normalize nodelta #H @('bind_inversion H) -H
1543   #bl' >set_no_pc_eta #H lapply(err_eq_from_io ????? H) -H #EQbl'
1544   #H @('bind_inversion H) -H * #f1' * #fn1' #H lapply(err_eq_from_io ????? H) -H
1545   #EQfn1' normalize nodelta
1546[2: #H @('bind_inversion H) -H #st whd in match eval_external_call; normalize nodelta
1547   #H @('bind_inversion H) -H #x #_ #H @('bind_inversion H) -H #y #_
1548   #H @('bind_inversion H) -H #z whd in ⊢ (??%% → ?); #EQ destruct(EQ) ]
1549#H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H
1550#st2_save #_ #H @('bind_inversion H) -H #st2_fin #_ whd in ⊢ (??%% → ?);
1551#EQ destruct(EQ) >EQbl' >m_return_bind >EQfn1' >m_return_bind normalize nodelta
1552lapply(fetch_ok_pc_ok … good … Rst1st2' ?)
1553     [ whd in match fetch_internal_function; normalize nodelta >EQfn1 in ⊢ (??%?); %
1554     |*:
1555      ]
1556    whd in match pc_of_point in ⊢ (% → ?); normalize nodelta #EQ destruct(EQ)
1557    lapply EQfn1 whd in match fetch_function; normalize nodelta
1558    @eqZb_elim [ #ABS @⊥ cases(block_of_call_no_minus_one …  EQbl) #H @H assumption]
1559    #Hbl' normalize nodelta #H lapply(opt_eq_from_res ???? H) -H #H @('bind_inversion H)
1560    #f2 #EQf2 #H @('bind_inversion H) -H #fn2 #_ whd in ⊢ (??%? → ?); -e0 -EQ
1561    #EQ destruct(EQ) -H lapply EQfn1' whd in match fetch_function; normalize nodelta
1562    @eqZb_elim [ #ABS >ABS in Hbl'; * #H @⊥ @H %] #_ normalize nodelta
1563    #H lapply(opt_eq_from_res ???? H) -H
1564    whd in match joint_globalenv in ⊢ (% → ?); normalize nodelta
1565    whd in match b_graph_transform_program in ⊢ (% → ?); normalize nodelta
1566    whd in match transform_joint_program; normalize nodelta
1567    >(symbol_for_block_transf ??? (λx.x) prog
1568      (λvars.transf_fundef ?? (λdef_in.b_graph_translate ??? (init ? def_in) def_in)) bl') in ⊢ (% → ?);
1569    >EQf2 >m_return_bind in ⊢ (% → ?); #H @('bind_inversion H) -H #fn2' #_
1570    whd in ⊢ (??%% → ?); #EQ destruct(EQ) %
1571qed.
1572
1573
1574lemma pair_dep_match_elim : ∀A,B,C : Type[0].∀P : C → Prop.∀t:A×B.
1575∀c.
1576(∀x,y,prf.P (c x y prf)) →
1577P (let 〈x,y〉 as prf ≝ t in c x y prf).
1578#A #B #C #P * // qed.
1579
1580theorem joint_correctness : ∀p_in,p_out : sem_graph_params.
1581∀prog : joint_program p_in.∀stack_size : ident → option ℕ.
1582∀init : (∀globals.joint_closed_internal_function p_in globals →
1583         bound_b_graph_translate_data p_in p_out globals).
1584∀init_regs : block → list register.∀f_lbls : lbl_funct_type.
1585∀f_regs : regs_funct_type.∀st_no_pc_rel : joint_state_relation p_in p_out.
1586∀st_rel : joint_state_pc_relation p_in p_out.
1587good_state_relation p_in p_out prog stack_size init init_regs
1588 f_lbls f_regs st_no_pc_rel st_rel →
1589good_init_relation p_in p_out prog stack_size init st_no_pc_rel →
1590let trans_prog ≝ b_graph_transform_program … init prog in
1591∀init_in.make_initial_state (mk_prog_params p_in prog stack_size) = OK ? init_in →
1592∃init_out.make_initial_state (mk_prog_params p_out trans_prog stack_size) = OK ? init_out ∧
1593∃[1] R.
1594  status_simulation_with_init
1595    (joint_abstract_status (mk_prog_params p_in prog stack_size))
1596    (joint_abstract_status (mk_prog_params p_out trans_prog stack_size))
1597    R init_in init_out.
1598#p_in #p_out #prog #stack_size #init #init_regs #f_lbls #f_regs #st_no_pc_rel
1599#st_rel #good #good_init #init_in whd in match make_initial_state; normalize nodelta
1600#H @('bind_inversion H) -H #init_m #EQinit_m @pair_dep_match_elim #m #bl #prf
1601whd in ⊢ (??%% → ?); #EQ destruct(EQ)
1602letin trans_prog ≝ (b_graph_transform_program ????)
1603letin globals_size ≝ (globals_stacksize … trans_prog)
1604letin spp ≝
1605   («mk_pointer bl (mk_offset (bitvector_of_Z 16 (-S (globals_size)))),
1606     pi2 … bl»)
1607letin st ≝ (mk_state p_out
1608    (* frames ≝ *)(Some ? (empty_framesT …))
1609    (* internal_stack ≝ *) empty_is
1610    (* carry ≝ *)(BBbit false)
1611    (* regs ≝ *)(empty_regsT … spp)
1612    (* mem ≝ *)m
1613    (* stack_usage ≝ *)0)
1614%{(mk_state_pc ? (set_sp … spp st) init_pc (null_pc one))} >init_mem_transf
1615>EQinit_m >m_return_bind @pair_dep_match_elim #m1 #bl1 #prf' lapply prf
1616lapply prf' lapply prf' <prf in ⊢ (%→?); #EQ destruct(EQ) -prf' #prf' #_
1617%{(refl …)} %{(JointStatusSimulation … good)} %
1618[ whd @(st_rel_def … good)
1619  [3: % |1,2:
1620  | lapply(good_empty ?????? good_init ? EQinit_m) <prf' normalize nodelta #H @H
1621  | %
1622  ]
1623| whd whd in ⊢ (??%%); lapply(good_init_cost_label … good_init) normalize nodelta
1624  cases(fetch_statement ????) normalize nodelta
1625  [2: #e * [ *#e' #EQ >EQ % | * #x * #EQ #EQ1 >EQ normalize nodelta >EQ1 % ] ]
1626  #x cases(cost_label_of_stmt ???) normalize nodelta
1627  [ * [ * #e' #EQ >EQ % | * #y * #EQ1 #EQ2 >EQ1 normalize nodelta >EQ2 %]
1628  | #c * #y * #EQ1 #EQ2 >EQ1 normalize nodelta >EQ2 %
1629  ]
1630]
1631%
1632[ #st1 #st1' #st2 whd in ⊢ (% → ?); #EQeval @('bind_inversion EQeval)
1633  ** #f #fn #stmt #H lapply(err_eq_from_io ????? H) -H cases stmt -stmt
1634  [ * [ #c | #id #arg #dest | #r #lb | #seq ] #nxt | #fin | * ] #EQfetch #_
1635  whd in ⊢ (% → ?); #Rst1st2
1636  change with (joint_classify ???) in
1637                     ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]);
1638  [ whd in match joint_classify; normalize nodelta >EQfetch normalize nodelta
1639    cases(decidable_eq_Z (block_id (pc_block … (pc … st1))) (neg one)) #Hbl
1640    [ cases(general_eval_cost_premain_ok … good … Hbl Rst1st2 EQfetch EQeval)
1641    | cases(general_eval_cost_ok … good … Hbl Rst1st2 EQfetch EQeval)
1642    ] #st2' * #Rst1st2' * #taaf * #H #H1 %{st2'} %{taaf} >H % [1,3: %{I} assumption]
1643      assumption
1644  | whd in match joint_classify; normalize nodelta >EQfetch normalize nodelta #prf
1645    cases(decidable_eq_Z (block_id (pc_block … (pc … st1))) (neg one)) #Hbl
1646    [ cases(eval_call_premain_ok … good … Hbl Rst1st2 EQfetch EQeval)
1647    | cases(eval_call_ok … good … Hbl Rst1st2 EQfetch EQeval)
1648    ]
1649    #prf' * #st2_pre * #prf'' ** #EQ #EQ1 * #st2_after * #st2' * #taa * #taa1 ** #EQ2 #H #EQ3
1650    %{st2_pre} [1,3: assumption] % [1,3: % [1,3: >EQ % |*: assumption ] ]
1651    %{st2_after} %{st2'} %{taa} %{taa1} % [1,3: %{EQ2 H}] assumption
1652  | whd in match joint_classify; normalize nodelta >EQfetch normalize nodelta
1653    #ncost cases(decidable_eq_Z (block_id (pc_block … (pc … st1))) (neg one)) #Hbl
1654    [ cases(eval_cond_premain_ok … good … Hbl Rst1st2 EQfetch EQeval ncost)
1655    | cases(eval_cond_ok … good … Hbl Rst1st2 EQfetch EQeval ncost)
1656    ]
1657    #st2' * #H * #taaf * #H1 #H2 %{st2'} %{taaf} >H1 % [1,3: %{I} assumption]
1658    assumption
1659  | whd in match joint_classify; normalize nodelta >EQfetch normalize nodelta
1660    cases(decidable_eq_Z (block_id (pc_block … (pc … st1))) (neg one)) #Hbl
1661    [ cases(general_eval_seq_no_call_premain_ok … good … Hbl Rst1st2 EQfetch EQeval)
1662    | cases(general_eval_seq_no_call_ok … good … Hbl Rst1st2 EQfetch EQeval)
1663    ]
1664    #st2' * #H * #taaf * #H1 #H2 %{st2'} %{taaf} % [ >H1 %{I H} |3: %{H1 H} ]
1665    assumption
1666    ]
1667  | @(as_result_ok … good)
1668  ]
1669cases fin in EQfetch; -fin
1670  [ #lb #EQfetch whd in match joint_classify; normalize nodelta >EQfetch
1671    normalize nodelta
1672    cases(decidable_eq_Z (block_id (pc_block … (pc … st1))) (neg one))
1673    #Hbl
1674    [ cases(eval_goto_premain_ok … good … Hbl Rst1st2 EQfetch EQeval)
1675    | cases(eval_goto_ok … good … Hbl Rst1st2 EQfetch EQeval)
1676    ]
1677    #st2' * #H * #taaf * #H1 #H2 %{st2'} %{taaf} >H1 % [1,3: %{I H}] assumption
1678 | #EQfetch whd in match joint_classify; normalize nodelta >EQfetch
1679   normalize nodelta
1680   cases(decidable_eq_Z (block_id (pc_block … (pc … st1))) (neg one))
1681   #Hbl
1682   [ @⊥ @(pre_main_no_return … good … Hbl … EQfetch) ]
1683   cases(eval_return_ok … good … Hbl Rst1st2 EQfetch EQeval) #st2_pre * #st2_after
1684   * #st2' * #taa * #taaf ***** #H #H1 #H2 #H3 #H4 #H5 %{st2_pre} %{st2_after}
1685   %{st2'} %{taa} %{taaf} % [2: assumption] % [2: assumption] % [2: assumption]
1686   % [2: assumption] %{H H1}
1687 | #has #id #arg #EQfetch whd in match joint_classify; normalize nodelta
1688   >EQfetch normalize nodelta
1689   cases(decidable_eq_Z (block_id (pc_block … (pc … st1))) (neg one))
1690   #Hbl
1691   [ cases(eval_tailcall_premain_ok … good … Hbl Rst1st2 EQfetch EQeval)
1692   | cases(eval_tailcall_ok … good … Hbl Rst1st2 EQfetch EQeval)
1693   ]
1694   #prf * #st2_pre * #t_is_call * #H * #st2_after * #st2' * #taa1 * #taa2
1695   ** #H1 #H2 #H3 #prf' %{st2_pre} [1,3: assumption] %{H} %{st2_after} %{st2'}
1696   %{taa1} %{taa2} % [2,4: assumption] %{H1 H2}
1697 ]
1698qed.
1699
Note: See TracBrowser for help on using the repository browser.