source: src/joint/StatusSimulationHelper.ma @ 3154

Last change on this file since 3154 was 3154, checked in by piccolo, 7 years ago

1) changed block_of_call in order to prevent pre-main calls
2) StatusSimulationHelper? in place

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