source: src/ERTLptr/ERTLtoERTLptrOK.ma @ 3362

Last change on this file since 3362 was 3018, checked in by sacerdot, 7 years ago

1) some files repaired
2) all stuff related to the aborted pass ERTLptr (now merged with

ERTLToLTL) moved into the ERTLptr directory (no longer used/linked)

File size: 69.0 KB
Line 
1
2(**************************************************************************)
3(*       ___                                                              *)
4(*      ||M||                                                             *)
5(*      ||A||       A project by Andrea Asperti                           *)
6(*      ||T||                                                             *)
7(*      ||I||       Developers:                                           *)
8(*      ||T||         The HELM team.                                      *)
9(*      ||A||         http://helm.cs.unibo.it                             *)
10(*      \   /                                                             *)
11(*       \ /        This file is distributed under the terms of the       *)
12(*        v         GNU General Public License Version 2                  *)
13(*                                                                        *)
14(**************************************************************************)
15
16
17include "joint/StatusSimulationHelper.ma".
18include "ERTL/ERTLtoERTLptrUtils.ma".
19
20
21
22(*
23lemma get_internal_function_from_ident_ok :
24∀p : sem_params. ∀globals : list ident. ∀ge : genv_t (joint_function p globals).
25∀bl,f,fn. fetch_internal_function ? ge bl = return 〈f,fn〉 →
26get_internal_function_from_ident p globals ge f= return fn.
27#p #globals #ge #bl #f #fn #EQf
28@('bind_inversion EQf) * #f1 * #fn1 whd in match fetch_function;
29normalize nodelta #H lapply(opt_eq_from_res ???? H) -H #H @('bind_inversion H) -H
30#f2 #EQf2 #H @('bind_inversion H) -H #fn2 #EQfn2 whd in ⊢ (??%% → ??%% → ?);
31#EQ1 #EQ2 destruct whd in match get_internal_function_from_ident; normalize nodelta
32>(symbol_of_block_rev … EQf2) >m_return_bind
33cut(code_block_of_block bl = return bl)
34 [ whd in match code_block_of_block; normalize nodelta @match_reg_elim
35   [ >(pi2 ?? bl) #ABS destruct] elim bl #bl1 #EQ #prf % ] #EQbl >EQbl
36>m_return_bind >EQf %
37qed.
38*)
39
40
41
42 
43(*
44  whd in match sigma_frames_opt; whd in match m_list_map; normalize nodelta
45whd in match sigma_state in ⊢ (???????%%); normalize nodelta
46cases(st_frms … st) normalize nodelta [ @res_preserve_error1]
47* #loc_mem #bl #tl inversion(sigma_frames ????)
48[ #_ normalize nodelta @res_preserve_error1] * #loc_mem1 #bl1 #tl1
49whd in match sigma_frames; normalize nodelta inversion(sigma_frames_opt ????)
50[ #_ normalize nodelta #_ #ABS destruct] #l whd in match sigma_frames_opt;
51whd in match m_list_map; normalize nodelta whd in match (foldr ?????);
52normalize nodelta inversion(fetch_internal_function ???)
53[2: #e #_ whd in ⊢ (??%% → ?); #ABS destruct] * #id1 #fn1 #EQfn1 >m_return_bind
54normalize nodelta #H @('bind_inversion H) -H #l1
55change with (sigma_frames_opt ???? = ? → ?) #EQl1
56cut (sigma_frames prog f_lbls f_regs tl = l1)
57[whd in match sigma_frames; normalize nodelta >EQl1 %] #EQl11
58cases l [ whd in ⊢ (??%? → ?); #EQ destruct] #x #y
59whd in ⊢ (??%? → ?); #EQ1 #_ #EQ2 destruct @mfr_bind1
60[2: whd in match set_regs; whd in match set_frms; normalize nodelta
61    >EQl1 in ⊢ (???????%?); normalize nodelta
62cut(sigma_regs prog f_lbls (added_registers ERTL (prog_var_names … prog) fn1 (f_regs bl1))
63    〈loc_mem,\snd (regs … st)〉 =  〈map RegisterTag beval beval loc_mem
64       (λbv:beval.sigma_beval prog f_lbls bv)∖
65         added_registers ERTL (prog_var_names … prog) fn1 (f_regs bl1),
66   \snd  (sigma_regs prog f_lbls restr (regs ERTLptr_semantics st))〉)
67[ whd in match sigma_regs; normalize nodelta @eq_f2 [ %] cases(regs ? st)
68     #x #y %] #EQ <EQ -EQ
69change with (sigma_state ???? (set_regs ERTL_semantics 〈loc_mem,\snd (regs … st)〉
70            (set_frms ERTL_semantics tl st))) in ⊢ (???????(??%)?);
71@pop_ra_ok |
72| * #st1 #pc1 @if_elim [2: #_ @res_preserve_error1] normalize nodelta
73@eq_block_elim [2: #_ *] #EQbl1 * @if_elim
74[2: >EQbl1 @eq_block_elim [#_ *] * #H @⊥ @H <pc_block_eq [%] %
75    cases bl1 in EQbl1 EQfn1; #p1 #p2 #EQ destruct lapply p2
76    whd in match sigma_stored_pc; normalize nodelta cases(sigma_pc_opt ???)
77    normalize nodelta [2: #pc2] #p2 [#_ #EQ destruct]
78    >fetch_internal_function_no_zero [2: %] #EQ destruct
79] @eq_block_elim [2: #_ *] #EQbl11 * @mfr_return_eq1 normalize nodelta
80  cases bl1 in EQbl11 EQfn1; #p1 #p2 #EQ destruct
81  lapply p2 cases(pc_block pc1) #p11 #p22 #e #EQfn1 >EQfn1
82  %
83]
84qed.
85*)
86
87
88definition ERTLptrStatusSimulation :
89∀ prog : ertl_program.
90let trans_prog ≝ ertl_to_ertlptr prog in
91∀stack_sizes.∀ f_lbls : lbl_funct. ∀ f_regs : regs_funct.
92∀f_bl_r.
93b_graph_transform_program_props ERTL_semantics ERTLptr_semantics
94     translate_data prog f_bl_r f_lbls f_regs →
95status_rel (ERTL_status prog stack_sizes) (ERTLptr_status trans_prog stack_sizes) ≝
96λprog,stack_sizes,f_lbls,f_regs,f_lb_r,good.
97  let trans_prog ≝ ertl_to_ertlptr prog in
98    mk_status_rel ??
99    (* sem_rel ≝ *) (λs1:ERTL_status prog stack_sizes
100       .λs2:ERTLptr_status trans_prog stack_sizes
101        .s1=sigma_state_pc prog f_lbls f_regs s2)
102    (* call_rel ≝ *) 
103          (λs1:Σs:ERTL_status prog stack_sizes
104               .as_classifier (ERTL_status prog stack_sizes) s cl_call
105       .λs2:Σs:ERTLptr_status trans_prog stack_sizes
106                .as_classifier (ERTLptr_status trans_prog stack_sizes) s cl_call
107        .
108        pc (mk_prog_params ERTL_semantics prog stack_sizes) s1
109         =sigma_stored_pc prog f_lbls
110          (pc
111           (mk_prog_params ERTLptr_semantics (ertl_to_ertlptr prog) stack_sizes)
112           s2))
113    (* sim_final ≝ *) ?.
114cases daemon
115qed.
116
117include "joint/semantics_blocks.ma".
118
119
120
121lemma as_label_ok : ∀ prog : ertl_program.
122let trans_prog ≝ ertl_to_ertlptr prog in
123∀ f_lbls,f_regs,stack_sizes.
124∀f_bl_r.
125b_graph_transform_program_props ERTL_semantics ERTLptr_semantics
126     (λglobals,fn.«translate_data globals fn,(refl …)») prog f_bl_r f_lbls f_regs →
127∀st,fn,id,stmt.
128fetch_statement ERTL_semantics (prog_var_names … prog)
129      (globalenv_noinit … prog) (pc … (sigma_state_pc prog f_lbls f_regs st)) =
130               return 〈id,fn,stmt〉 →
131as_label (ERTLptr_status trans_prog stack_sizes) st = as_label
132(ERTL_status prog stack_sizes) (sigma_state_pc prog f_lbls f_regs st).
133#prog #f_lbls #f_regs #stack_size #f_lb_r #good #st #fn #id #stmt #EQfetch
134whd in match as_label; normalize nodelta change with (pc ? ?) in ⊢ (??(??%)(??%));
135cases(b_graph_transform_program_fetch_statement … good … EQfetch)
136#init_data * #t_fn ** #EQt_fn whd in ⊢ (% → ?); cases(f_lb_r ?)
137normalize nodelta [2: #r #tl *] #EQinit destruct(EQinit) * #l_labs * #l_regs **
138#_ #_ cases stmt in EQfetch;
139[ * [ #c | * [ #c_id | #c_ptr ] #c_arg #c_dest | #reg #lbl | #s ] #nxt | #fin | * ]
140#EQfetch normalize nodelta * #bl * [1,2,3,4,5: >if_merge_right in ⊢ (% → ?); try %]
141whd in ⊢ (%→?); cases l_regs normalize nodelta [2,4,5,8,10,12: [3: *] #x #y *]
142[1,2,4,5,6:| #r #tl whd in ⊢ (% → ?); cases tl -tl normalize nodelta [2: #r1 #tl1 *]]
143#EQ destruct(EQ)
144[1,2,3,4,6: * #pre_l * #mid1 * #mid2 * #post_l *** #EQmid1
145            whd in match map_eval in ⊢ (% → ?); normalize nodelta
146            whd in ⊢ (?????%?? → ?);
147            whd in match (seq_list_in_code ???????) in ⊢ (%→?); *
148           [1,2,3,4: #EQ1 #EQ2 destruct(EQ1 EQ2) whd in EQmid1 : (???%);
149                     destruct(EQmid1) * #nxt1 * #EQt_stmt #_ #_
150           |        * #lbl1 * #rest ** #EQ destruct(EQ) * #nxt1 *
151                    #EQt_stmt #_ #_ #_ #_
152           ]
153|           * #pre_l * #mid ** #EQmid whd in ⊢ (% → ?); * #EQ destruct(EQ)
154            whd in EQmid : (???%); destruct(EQmid) #EQ destruct(EQ)
155            whd in ⊢ (% → ?); #EQt_stmt
156]
157whd in ⊢ (??%%); >EQfetch normalize nodelta whd in match fetch_statement;
158normalize nodelta >(fetch_stmt_ok_sigma_pc_ok … EQfetch) in EQt_fn;
159#EQt_fn >EQt_fn >m_return_bind >(fetch_stmt_ok_sigma_pc_ok … EQfetch) in EQt_stmt;
160#EQt_stmt >EQt_stmt %
161qed.
162
163include alias "basics/lists/listb.ma".
164
165definition state_rel ≝ λprog : ertl_program.λf_lbls.
166λf_regs : (block → label → list register).
167λbl.λ_ : label.λst1,st2.∃f,fn.
168fetch_internal_function ? (globalenv_noinit … prog) bl = return 〈f,fn〉 ∧
169let added ≝ added_registers ERTL (prog_var_names … prog) fn (f_regs bl) in
170st1 = (sigma_state prog f_lbls f_regs added st2).
171 
172lemma make_ERTL_To_ERTLptr_good_state_relation :
173∀prog : ertl_program.
174let p_out ≝ ertl_to_ertlptr prog in
175∀stack_sizes.
176∃init_regs : block → list register.
177∃f_lbls : block → label → list label.
178∃f_regs : block → label → list register.
179∃good : b_graph_transform_program_props ERTL_semantics ERTLptr_semantics
180        (λglobals,fn.«translate_data globals fn,(refl …)»)
181        prog init_regs f_lbls f_regs.
182good_state_relation ERTL_semantics ERTLptr_semantics prog stack_sizes
183 (λglobals,fn.«translate_data globals fn,(refl …)») init_regs f_lbls f_regs
184 good (state_rel prog f_lbls f_regs)
185 (sem_rel … (ERTLptrStatusSimulation prog … stack_sizes … good)).
186#prog #stack_sizes
187cases(make_b_graph_transform_program_props ERTL_semantics ERTLptr_semantics
188          (λglobals,fn.«translate_data globals fn,(refl …)») prog)
189#init_regs * #f_lbls * #f_regs #good %{init_regs} %{f_lbls} %{f_regs} %{good}
190%
191[ #st1 #st2 #f #fn whd in ⊢ (% → ?); #EQ destruct(EQ) #EQfn whd %{f} %{fn}
192  >EQfn %{(refl …)} whd in match sigma_state_pc; normalize nodelta
193  lapply EQfn >(fetch_ok_sigma_pc_ok … EQfn) #EQfn1 >EQfn1 %
194| #st1 #st2 #f #fn whd in ⊢ (% → ?); #EQ destruct(EQ) #EQfn @fetch_ok_sigma_pc_ok
195  assumption
196| #st1 #st2 #f #fn whd in ⊢ (% → ?); #EQ destruct(EQ) #EQfn
197  >(fetch_ok_sigma_last_pop_ok … f fn st2 EQfn) %
198| #st1 #st2 #pc #lp1 #lp2 #f #fn #EQfn * #f1 * #fn1 * >EQfn whd in ⊢ (??%% → ?);
199  #EQ destruct(EQ) normalize nodelta #EQ destruct(EQ) #EQ destruct(EQ) whd
200  whd in match sigma_state_pc; normalize nodelta >EQfn %
201| #st1 #st2 #f #fn #stmt #EQfetch whd in ⊢ (% → ?); #EQ destruct(EQ)
202  lapply(as_label_ok … stack_sizes … good st2 … EQfetch) #EQ <EQ in ⊢ (??%?); %
203| normalize nodelta whd in ⊢ (% → % → % → ?); #st1 #st1' #st2 #f #fn
204  #a #ltrue #lfalse #EQfetch cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt
205   whd in match eval_state; whd in match eval_statement_no_pc;
206  normalize nodelta >EQfetch >m_return_bind normalize nodelta >m_return_bind
207  whd in match eval_statement_advance; normalize nodelta
208  change with (ps_reg_retrieve ??) in match (acca_retrieve ?????);
209  #H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H
210  #bv whd in match set_no_pc; normalize nodelta #EQbv
211   #H @('bind_inversion H) -H * #EQbool normalize nodelta
212   [whd in match goto; normalize nodelta >(pc_of_label_eq … EQfn)
213    >m_return_bind] whd in ⊢ (??%% → ?); #EQ destruct(EQ)
214  whd in ⊢ (% → ?); #EQ destruct(EQ)
215  >(fetch_stmt_ok_sigma_state_ok … EQfetch) in EQbv;
216  whd in match sigma_state; normalize nodelta #EQbv
217  cases(ps_reg_retrieve_ok ?????? EQbv) #bv1 * #EQbv1 #EQ destruct(EQ)
218  cases(bool_of_beval_ok … EQbool) #b * #EQb #EQ destruct(EQ) #t_fn #EQt_fn
219  whd %{(refl …)} #mid #EQt_stmt %{(st_no_pc … st2)} %
220  [1,3: %
221       [1,3: %
222             [1,3: %{(refl …)}
223             |*: %
224             ]
225       |*: %
226       ]
227  |*: normalize nodelta 
228      change with (ps_reg_retrieve ??) in match (acca_retrieve ?????);
229      >EQbv1 >m_return_bind >EQb >m_return_bind normalize nodelta
230      [ >(pc_of_label_eq … EQt_fn) >m_return_bind]
231      >(fetch_stmt_ok_sigma_pc_ok … EQfetch) %
232   ]
233  whd %{f} %{fn} >EQfn %{(refl …)} >(fetch_stmt_ok_sigma_pc_ok … EQfetch)
234  cases st2 * #frms #is #b #regs #m #pc2 #lp2 %
235| #st1 #st1' #st2 #f #fn #stmt #nxt #EQfetch whd in match eval_state;
236  whd in match eval_statement_no_pc; normalize nodelta >EQfetch >m_return_bind
237  normalize nodelta #H @('bind_inversion H) -H #st1_no_pc' #EQst1_no_pc'
238  whd in ⊢ (??%% → ?); #EQ destruct(EQ)
239  whd in match (succ_pc ???); normalize nodelta
240  whd in match (set_no_pc ???); normalize nodelta
241  whd in ⊢ (%→?); #EQ destruct(EQ)
242  whd in match sigma_state_pc in EQst1_no_pc'; normalize  nodelta in EQst1_no_pc';
243  cases(fetch_statement_inv … EQfetch) >(fetch_stmt_ok_sigma_pc_ok … EQfetch)
244  #EQfn #EQstmt >EQfn in EQst1_no_pc'; normalize nodelta #EQst1_no_pc'
245  #t_fn #EQt_fn whd % [2: %{(refl …)} |] lapply(err_eq_from_io ????? EQst1_no_pc')
246  -EQst1_no_pc' #EQst1_no_pc'
247  cases(eval_seq_no_pc_no_call_ok prog f_lbls f_regs ???????? EQst1_no_pc')
248  [ #st2_no_pc' * #EQst2_no_pc' #EQ destruct(EQ) %{st2_no_pc'} %
249    [ whd in ⊢ (??%?); >EQst2_no_pc' %
250    | whd %{f} %{fn} >EQfn %{(refl …)} whd in match sigma_state_pc; normalize nodelta
251      >EQfn %
252    ]
253  |  #lbl whd in match code_has_label; whd in match code_has_point; normalize nodelta
254  inversion(stmt_at ????) [#_ *] #stmt1 #EQstmt1 #_
255  cut(fetch_statement ERTL_semantics (prog_var_names … prog) (globalenv_noinit … prog)
256                      (pc_of_point ERTL_semantics (pc_block (pc … st2)) lbl) =
257                 return 〈f,fn,stmt1〉)
258   [ whd in ⊢ (??%?); >EQfn normalize nodelta >point_of_pc_of_point >EQstmt1 %] #EQf_stmt1
259  cases(b_graph_transform_program_fetch_statement_plus … good … EQf_stmt1)
260  #init * #t_fn' ** #EQt_fn' whd in ⊢ (% → ?); cases(init_regs ?) [2: #x #y *]
261  normalize nodelta #EQ destruct(EQ) * #labels * #registers
262  ******* #EQlabels >point_of_pc_of_point change with (pc_block (pc … st2)) in match (pc_block ?);
263  #EQregisters #_ #_ #_ #_ #fresh_regs #_ >EQregisters
264  cases(excluded_middle_list ? (λreg.bool_to_Prop(¬(reg∈registers)))
265         (get_used_registers_from_seq … (functs ERTL) stmt) ?)
266  [3: #a #_ cases(¬a∈registers) // |1: #H assumption] #H @⊥
267  cases(Exists_All … H (regs_are_in_univers … (pi2 ?? fn) … EQstmt))
268   #reg ** #H1 #H2 @H1 -H1 @notb_Prop % #H1 lapply(fresh_regs … lbl) >EQregisters
269  #H3 lapply(All_memb … H3 H1) ** #H4 #_ @H4 assumption
270  ]
271]
272qed.
273
274include alias "basics/lists/listb.ma".
275
276lemma eval_seq_no_call_ok :
277 ∀prog.
278 let trans_prog ≝ ertl_to_ertlptr prog in
279 ∀ f_lbls,f_regs,stack_sizes.
280 ∀f_bl_r.
281 b_graph_transform_program_props ERTL_semantics ERTLptr_semantics
282     (λglobals,fn.«translate_data globals fn,(refl …)») prog f_bl_r f_lbls f_regs →
283 ∀st2 : state_pc ERTLptr_semantics.
284 let st1 ≝ sigma_state_pc prog f_lbls f_regs st2 in
285 ∀st1' : state_pc ERTL_semantics.
286 ∀f,fn,stmt,nxt.
287   fetch_statement ERTL_semantics
288     (prog_var_names (joint_function ERTL_semantics) ℕ prog)
289    (ev_genv (mk_prog_params ERTL_semantics prog stack_sizes))
290    (pc … st1) =
291      return 〈f, fn,  sequential … (step_seq ERTL … stmt) nxt〉 →
292   eval_state ERTL_semantics
293   (prog_var_names (joint_function ERTL_semantics) ℕ prog)
294   (ev_genv … (mk_prog_params ERTL_semantics prog stack_sizes))
295   st1 =
296    return st1' →
297 ∃st2'. st1' = sigma_state_pc prog f_lbls f_regs st2' ∧
298 ∃taf : trace_any_any_free (ERTLptr_status trans_prog stack_sizes)
299  st2
300  st2'.
301 if taaf_non_empty … taf then True else
302(¬as_costed (ERTL_status prog stack_sizes) st1 ∨
303 ¬as_costed (ERTL_status prog stack_sizes) st1').
304#prog #f_lbls #f_regs #stack_size #f_bl_r #good #st2 #st1' #f #fn #stmt #nxt
305#EQfetch whd in match eval_state; normalize nodelta >EQfetch >m_return_bind
306#H @('bind_inversion H)-H #st_no_pc
307whd in match eval_statement_no_pc; normalize nodelta #EQnopc
308whd in match eval_statement_advance; normalize nodelta
309whd in match set_no_pc; whd in match next; whd in match set_pc;
310normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ) lapply EQfetch
311>(fetch_stmt_ok_sigma_pc_ok … EQfetch) #EQfetch'
312cases(b_graph_transform_program_fetch_statement_plus … good … EQfetch')
313#init_data * #t_fn1 ** #EQt_fn1 whd in ⊢ (% → ?); cases (f_bl_r ?) normalize nodelta
314[2: #r #tl *] #EQ destruct(EQ) * #labs * #regs ******* #EQlabs #EQregs #_ #_ #_ #_
315#fresh_regs * #bl * >if_merge_right in ⊢ (% → ?); [2: %]
316whd in ⊢ (% → ?); cases regs in EQregs; normalize nodelta [2: #x #y #_ *] #EQregs
317#EQ destruct(EQ) #eval_spec
318lapply(err_eq_from_io ????? EQnopc) -EQnopc >(fetch_stmt_ok_sigma_state_ok … EQfetch)
319#EQnopc
320cases(eval_seq_no_pc_no_call_ok prog f_lbls f_regs ???????? EQnopc)
321[ #stnopc'' * #EQstnopc'' #EQsem %
322  [ % [@stnopc'' | @(succ_pc ERTL_semantics (pc … st2) nxt) | @(last_pop … st2)]]
323  %
324  [ whd in match sigma_state_pc; normalize nodelta @('bind_inversion EQfetch)
325    * #f1 #fn1 >(fetch_stmt_ok_sigma_pc_ok … EQfetch) #EQfn1
326    #H @('bind_inversion H) -H #stmt1 #_ whd in ⊢ (??%% → ?); #EQ destruct(EQ)
327    >EQfn1 normalize nodelta >EQsem % ]
328  % [ @(produce_trace_any_any_free_coerced) [ @f | @t_fn1 |6: @eval_spec ||| @EQt_fn1]
329    whd in match repeat_eval_seq_no_pc; normalize nodelta whd in ⊢ (??%?);
330    >EQstnopc'' %] @if_elim [#_ @I] #_ %1 % whd in match as_costed;
331    normalize nodelta * #H @H whd in ⊢ (??%?); >EQfetch %
332| #lbl whd in match code_has_label; whd in match code_has_point; normalize nodelta
333  inversion(stmt_at ????) [#_ *] #stmt1 #EQstmt1 #_
334  cut(fetch_statement ERTL_semantics (prog_var_names … prog) (globalenv_noinit … prog)
335                      (pc_of_point ERTL_semantics (pc_block (pc … st2)) lbl) =
336                 return 〈f,fn,stmt1〉)
337   [ lapply(fetch_statement_inv … EQfetch') * #EQfn #_ whd in ⊢ (??%?);
338     >EQfn normalize nodelta >point_of_pc_of_point >EQstmt1 %] #EQf_stmt1
339  cases(b_graph_transform_program_fetch_statement_plus … good … EQf_stmt1)
340  #init * #t_fn' ** #EQt_fn' whd in ⊢ (% → ?); cases(f_bl_r ?) [2: #x #y *]
341  normalize nodelta #EQ destruct(EQ) * #labels * #registers
342  ******* #EQlabels >point_of_pc_of_point change with (pc_block (pc … st2)) in match (pc_block ?);
343  #EQregisters #_ #_ #_ #_ #_ #_ >EQregisters
344  cases(excluded_middle_list ? (λreg.bool_to_Prop(¬(reg∈registers)))
345         (get_used_registers_from_seq … (functs ERTL) stmt) ?)
346  [3: #a #_ cases(¬a∈registers) // |1: #H assumption] #H @⊥
347  lapply(fetch_statement_inv … EQfetch') * #_ normalize nodelta #EQstmt
348  cases(Exists_All … H (regs_are_in_univers … (pi2 ?? fn) … EQstmt))
349   #reg ** #H1 #H2 @H1 -H1 @notb_Prop % #H1 lapply(fresh_regs … lbl) >EQregisters
350  whd in ⊢ (% → ?); #H3 lapply(All_memb … H3 H1) ** #H4 #_ @H4 assumption
351]
352qed.
353
354lemma eval_goto_ok :
355 ∀prog : ertl_program.
356 let trans_prog ≝ ertl_to_ertlptr prog in
357∀ f_lbls,f_regs,stack_sizes.
358 ∀f_bl_r.
359 b_graph_transform_program_props ERTL_semantics ERTLptr_semantics
360     (λglobals,fn.«translate_data globals fn,(refl …)») prog f_bl_r f_lbls f_regs →
361 ∀st2.
362 let st1 ≝ (sigma_state_pc prog f_lbls f_regs st2) in
363 ∀st1',f,fn,nxt.
364   fetch_statement ERTL_semantics …
365    (globalenv_noinit ? prog) (pc … st1) =
366      return 〈f, fn,  final … (GOTO ERTL … nxt)〉 →
367   eval_state ERTL_semantics
368   (prog_var_names (joint_function ERTL_semantics) ℕ prog)
369   (ev_genv … (mk_prog_params ERTL_semantics prog stack_sizes))
370   st1 =
371    return st1' →
372    ∃ st2'. st1' = sigma_state_pc prog f_lbls f_regs st2' ∧
373 ∃taf : trace_any_any_free (ERTLptr_status trans_prog stack_sizes)
374  st2
375  st2'.
376  bool_to_Prop (taaf_non_empty … taf).
377#prog #f_lbls #f_regs #stack_size #f_bl_r #good #st2 #st1' #f #fn #nxt #EQfetch
378whd in match eval_state; normalize nodelta >EQfetch >m_return_bind
379whd in match eval_statement_no_pc; normalize nodelta
380>m_return_bind whd in match eval_statement_advance; whd in match set_no_pc;
381whd in match goto; normalize nodelta #H lapply(err_eq_from_io ????? H) -H
382#H @('bind_inversion H) -H #new_pc lapply(fetch_statement_inv … EQfetch) *
383#EQfn #_ >(pc_of_label_eq … EQfn) whd in ⊢ (??%% → ??%% → ?);
384#EQ1 #EQ2 destruct(EQ1 EQ2)
385% [ % [ @st2 | @(mk_program_counter (pc_block (pc … st2))
386                         (offset_of_point ERTL_semantics nxt)) | @(last_pop … st2)]]
387% [ >(fetch_stmt_ok_sigma_state_ok … EQfetch) >(fetch_stmt_ok_sigma_pc_ok … EQfetch)
388    >(fetch_stmt_ok_sigma_last_pop_ok … EQfetch) whd in match sigma_state_pc;
389    normalize nodelta >(fetch_stmt_ok_sigma_pc_ok … EQfetch) in EQfn; #EQfn
390    >EQfn %]
391cases(b_graph_transform_program_fetch_statement … good … EQfetch)
392#init_data * #t_fn1 ** #EQt_fn1 whd in ⊢ (% → ?); cases (f_bl_r ?) normalize nodelta
393[2: #r #tl *] #EQ destruct(EQ) * #labs **
394[2: #hd #tl ** #_ #_ ** #pre #inst * whd in ⊢ (%→?); *] ** #EQlabs #EQf_regs
395whd in match translate_fin_step; normalize nodelta * #bl *
396whd in ⊢ (% → ?); #EQ destruct(EQ) **
397[2: #lb #tl * #mid ** #EQmid whd in ⊢ (% → ?); * #ABS destruct(ABS)] * #mid **
398whd in ⊢ (???% → ?); #EQ destruct(EQ) * #_ #_ change with (stmt_at ???? = ? → ?)
399#EQstmt >(fetch_stmt_ok_sigma_pc_ok … EQfetch) in EQt_fn1; #EQt_fn1
400>(fetch_stmt_ok_sigma_pc_ok … EQfetch) in EQstmt; #EQstmt
401%{(taaf_step … (taa_base …) …)}
402[ whd in match as_classifier; normalize nodelta whd in ⊢ (??%?);
403  whd in match fetch_statement; normalize nodelta 
404  >EQt_fn1 >m_return_bind >EQstmt %
405| whd whd in match eval_state; normalize nodelta whd in match fetch_statement;
406  normalize nodelta  >EQt_fn1 >m_return_bind >EQstmt >m_return_bind
407  whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
408  whd in match eval_statement_advance; normalize nodelta
409  whd in match goto; normalize nodelta >(pc_of_label_eq … EQt_fn1) %
410] @I
411qed.
412
413
414
415(*
416lemma list_elim_on_last : ∀A : Type[0].∀ P : (list A) → Prop. ∀ l.
417                 P ([ ]) → (∀pre,last. P (pre@[last])) → P l.
418#A #P #l #H1 #H2 cut(∀A.∀l : list A.l = [ ] ∨ ∃pre,last. l = pre@[last])
419[ #A #l elim l [ %1 % | #a #tl * [ #EQ destruct %2 %{([ ])} %{a} %]
420* #l1 * #a1 #EQ destruct %2 %{(a::l1)} %{a1} %]] #APP1
421lapply(APP1 … l) * [ #EQ >EQ assumption]
422 * #pre * #last #EQ >EQ @H2
423qed.*)
424
425
426
427lemma eval_return_ok :
428∀prog : ertl_program.
429let trans_prog ≝ ertl_to_ertlptr prog in
430∀ f_lbls,f_regs,stack_sizes.
431 ∀f_bl_r.
432 ∀ good :b_graph_transform_program_props ERTL_semantics ERTLptr_semantics
433     translate_data prog f_bl_r f_lbls f_regs.
434∀st2, st1',f,fn.
435 let st1 ≝ sigma_state_pc prog f_lbls f_regs st2 in
436 fetch_statement ERTL_semantics …
437  (globalenv_noinit ? prog) (pc … st1) =
438    return 〈f, fn,  final … (RETURN ERTL … )〉 →
439 eval_state ERTL_semantics
440   (prog_var_names (joint_function ERTL_semantics) ℕ prog)
441   (ev_genv … (mk_prog_params ERTL_semantics prog stack_sizes))
442   st1 =
443  return st1' →
444joint_classify (mk_prog_params ERTLptr_semantics trans_prog stack_sizes)
445  st2 = cl_return ∧
446∃st2'. st1' = sigma_state_pc prog f_lbls f_regs st2' ∧
447∃st2_after_ret.
448∃taf : trace_any_any_free (ERTLptr_status trans_prog stack_sizes) (* always empty in this case *)
449st2_after_ret
450st2'.
451(if taaf_non_empty … taf then
452  ¬as_costed (ERTLptr_status trans_prog stack_sizes)
453    st2_after_ret
454 else True) ∧
455eval_state … (ev_genv …  (mk_prog_params ERTLptr_semantics trans_prog stack_sizes)) st2 =
456return st2_after_ret ∧
457ret_rel ?? (ERTLptrStatusSimulation prog stack_sizes ??? good) st1' st2_after_ret.
458#prog #f_lbls #f_regs #stack_size #f_bl_r #good #st2 #st1' #f #fn #EQfetch
459whd in match eval_state; normalize nodelta >EQfetch >m_return_bind
460#H @('bind_inversion H) -H #st1_tmp whd in ⊢ (??%%→?); #EQ destruct
461whd in match set_no_pc in ⊢ (%→?); whd in match eval_statement_advance in ⊢ (%→?);
462whd in match eval_return; normalize nodelta #H lapply(err_eq_from_io ????? H) -H
463#H @('bind_inversion H) -H * #n_st #n_pc change with (ertl_pop_frame ? = ? → ?)
464>(fetch_stmt_ok_sigma_state_ok … EQfetch) #EQpop_frame
465cases(pop_frame_ok ?????? EQpop_frame) * #t_n_st #t_n_pc * #EQt_pop_frame
466normalize nodelta
467inversion (fetch_internal_function ??) normalize nodelta
468[ * #id1 #fn1 | #err ] normalize nodelta #EQfetch_fn1 #EQ destruct(EQ)
469#H @('bind_inversion H) -H #next_of_n_pc
470[2: >next_of_call_pc_error [2: % %] whd in ⊢ (???% → ?); #EQ destruct(EQ)]
471#EQnext_of_n_pc cases(next_of_call_pc_ok … good … EQnext_of_n_pc)
472#pc1 * #EQpc1 cut(pc1 = t_n_pc)
473[ @(sigma_stored_pc_inj prog f_lbls)
474  lapply EQnext_of_n_pc; <EQpc1 whd in match sigma_stored_pc; normalize nodelta
475  inversion(sigma_pc_opt ???) [1,3: #_ >next_of_call_pc_error [2,4: % %]
476  whd in ⊢ (???% → ?); #EQ destruct| #x #_ #_ % #EQ destruct] #x #EQx #_
477  lapply EQnext_of_n_pc whd in match sigma_stored_pc; normalize nodelta
478  inversion (sigma_pc_opt ???) [ #_ >next_of_call_pc_error [2: % %]
479  whd in ⊢ (???% → ?); #EQ destruct] #y #EQy #_ lapply EQpc1
480  whd in match sigma_stored_pc; normalize nodelta >EQx >EQy normalize nodelta
481  #EQ destruct %
482] #EQ destruct(EQ) #EQnxt whd in match next; whd in match set_last_pop;
483whd in match set_pc; normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ)
484cases(b_graph_transform_program_fetch_statement … good … EQfetch)
485#init_data * #t_fn1 ** #EQt_fn1 whd in ⊢ (% → ?); cases (f_bl_r ?) normalize nodelta
486[2: #r #tl *] #EQ destruct(EQ) * #labs **
487[2: #hd #tl ** #_ #_ * #ibl * whd in ⊢ (%→?); *] ** #EQlabs #EQf_regs
488whd in match translate_fin_step; normalize nodelta * #bl *
489whd in ⊢ (% → ?); #EQ destruct(EQ) **
490[2: #lb #tl * #mid ** #EQmid whd in ⊢ (% → ?); * #ABS destruct(ABS)] * #mid **
491whd in ⊢ (???% → ?); #EQ destruct(EQ) * #_ #_ change with (stmt_at ???? = ? → ?)
492#EQstmt %
493[ whd in match joint_classify; normalize nodelta whd in match fetch_statement;
494  normalize nodelta <(fetch_stmt_ok_sigma_pc_ok … EQfetch) >EQt_fn1 >m_return_bind
495  >EQstmt %
496| %
497    [ %
498        [ @t_n_st
499        | @(succ_pc ERTL_semantics (sigma_stored_pc prog f_lbls t_n_pc) next_of_n_pc)
500        | @t_n_pc]
501    ]
502  % 
503    [ whd in match sigma_state_pc; normalize nodelta
504      lapply(next_of_call_pc_inv … EQnext_of_n_pc) * #id2 * #fn2 * #c_id * #c_arg
505      * #c_dest #EQfetch1 whd in match (succ_pc ???);
506      >(fetch_stmt_ok_sigma_pc_block_ok … EQfetch1) >EQfetch_fn1
507      normalize nodelta %
508    ]
509  %
510    [ %
511        [ @t_n_st
512        | @(succ_pc ERTL_semantics (sigma_stored_pc prog f_lbls t_n_pc) next_of_n_pc)
513        | @t_n_pc]
514    ]
515  %{(taaf_base … )} normalize nodelta % [% [@I]]
516    [ whd in match fetch_statement; normalize nodelta <(fetch_stmt_ok_sigma_pc_ok … EQfetch)
517      >EQt_fn1 >m_return_bind >EQstmt >m_return_bind whd in match eval_statement_no_pc;
518      normalize nodelta >m_return_bind whd in match eval_statement_advance;
519      whd in match eval_return; normalize nodelta 
520      change with (ertl_pop_frame ?) in match (pop_frame ????????);
521      >EQt_pop_frame >m_return_bind >EQnxt >m_return_bind whd in match next;
522      whd in match set_pc; whd in match set_last_pop; whd in match succ_pc;
523      normalize nodelta lapply(next_of_call_pc_inv … EQnext_of_n_pc)
524      * #id2 * #fn2 * #c_id * #c_arg * #c_dest #EQfetch1 whd in match (succ_pc ???);
525      >(fetch_stmt_ok_sigma_pc_block_ok … EQfetch1) %
526    | whd * #s1_pre #s1_call
527      cases (joint_classify_call … s1_call)
528      * #calling_i #calling * #call_spec * #arg * #dest * #nxt' #EQfetch_call
529      * #s2_pre #s2_call whd in ⊢ (% → ?); >EQfetch_call normalize nodelta
530      * #s1_pre_prf #EQpc_s2_pre whd in ⊢ (% → ?); #EQ1
531      >EQ1 in EQfetch_call; #EQfetch_call
532      cases(fetch_call_commute … good … EQfetch_call) #calling' * #pc1 *
533      #EQ1 cut(pc … s2_pre = pc1)
534      [ @(sigma_stored_pc_inj prog f_lbls) lapply(EQfetch_call)
535        whd in match sigma_stored_pc; normalize nodelta inversion(sigma_pc_opt ???)
536        [1,3: #_ >fetch_statement_no_zero [2,4: %] #EQ destruct(EQ)| #x #_ #_ % #EQ destruct]
537        #pc2 #EQpc2 #_ lapply EQ1 whd in match sigma_stored_pc;
538        normalize nodelta >EQpc2 normalize nodelta cases(sigma_pc_opt ???)
539        [2: #x normalize nodelta #EQ >EQ %] normalize nodelta #EQ <EQ in EQpc2;
540        #EQ1 lapply EQfetch_call >fetch_statement_no_zero [ #ABS destruct(ABS)]
541        whd in match sigma_stored_pc; normalize nodelta >EQ1 %
542      ] #EQ2 destruct(EQ2) #EQt_fetch_call whd >EQt_fetch_call normalize nodelta %
543       [ >EQ1 in s1_pre_prf; #EQ @(sigma_stored_pc_inj prog f_lbls)
544        lapply EQnext_of_n_pc whd in match sigma_stored_pc; normalize nodelta
545        inversion(sigma_pc_opt ???) [1,3: #_ >next_of_call_pc_error [2,4: % %]
546        whd in ⊢ (???% → ?); #EQ destruct] #pc1 #EQpc1 #_ [ % #EQ destruct]
547        lapply EQ whd in match sigma_stored_pc; normalize nodelta
548        >EQpc1 normalize nodelta inversion(sigma_pc_opt ???)
549        [2: #pc2 #_ normalize nodelta #EQ >EQ %] normalize nodelta
550        #ABS #ABS1 lapply EQnext_of_n_pc whd in match sigma_stored_pc;
551        normalize nodelta >EQpc1 >ABS1 normalize nodelta
552        >next_of_call_pc_error [2: % %] whd in ⊢ (???% → ?); #EQ destruct
553       | whd in match succ_pc; normalize nodelta
554        change with next_of_n_pc in match (point_of_succ ???);
555        change with nxt' in match (point_of_succ ???);
556        lapply EQpc_s2_pre whd in match succ_pc; normalize nodelta
557        change with next_of_n_pc in match (point_of_succ ???);
558        change with nxt' in match (point_of_succ ???); #EQ >EQ
559        cut(pc_block (pc … s1_pre) = pc_block (pc … s2_pre))
560        [2: #EQ >EQ %] >EQ1 <(pc_block_eq prog f_lbls …) [%]
561        lapply EQfetch_call whd in match sigma_stored_pc; normalize nodelta
562        cases(sigma_pc_opt ???) [ >fetch_statement_no_zero [2: %] #EQ destruct]
563        #x #_ % #EQ destruct
564       ]
565     ]
566]
567qed.
568
569
570
571lemma eval_cond_ok :
572∀prog.
573let trans_prog ≝ ertl_to_ertlptr prog in
574∀ f_lbls,f_regs,stack_sizes.
575 ∀f_bl_r.
576 ∀ good :b_graph_transform_program_props ERTL_semantics ERTLptr_semantics
577     (λglobals,fn.«translate_data globals fn,(refl …)») prog f_bl_r f_lbls f_regs.
578∀st2,st1',f,fn,a,ltrue,lfalse.
579let st1 ≝ sigma_state_pc prog f_lbls f_regs st2 in
580 fetch_statement ERTL_semantics …
581  (globalenv_noinit ? prog) (pc … st1) =
582    return 〈f, fn,  sequential … (COND ERTL … a ltrue) lfalse〉 →
583 eval_state ERTL_semantics
584   (prog_var_names (joint_function ERTL_semantics) ℕ prog)
585   (ev_genv … (mk_prog_params ERTL_semantics prog stack_sizes))
586   st1 = return st1' →
587as_costed (ERTL_status prog stack_sizes) st1' →
588∃ st2'. st1' = sigma_state_pc prog f_lbls f_regs st2' ∧
589∃taf : trace_any_any_free (ERTLptr_status trans_prog stack_sizes)
590st2 st2'.
591bool_to_Prop (taaf_non_empty … taf).
592#prog #f_lbls #f_regs #stack_size #f_bl_r #good #st2 #st1' #f #fn #a #ltrue #lfalse
593#EQfetch whd in match eval_state; normalize nodelta >EQfetch >m_return_bind
594whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
595whd in match eval_statement_advance; normalize nodelta
596change with (ps_reg_retrieve ??) in match (acca_retrieve ?????);
597#H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H
598#bv >(fetch_stmt_ok_sigma_state_ok … EQfetch) in ⊢ (% → ?); whd in match set_no_pc;
599normalize nodelta #EQbv #H @('bind_inversion H) -H * #EQbool normalize nodelta
600 lapply(fetch_statement_inv … EQfetch) * #EQfn #_
601[ whd in match goto; normalize nodelta >(pc_of_label_eq ??????? EQfn) >m_return_bind
602| whd in match next; normalize nodelta
603] whd in match set_pc; normalize nodelta
604>(fetch_stmt_ok_sigma_state_ok … EQfetch) whd in match set_no_pc; normalize nodelta
605>(fetch_stmt_ok_sigma_pc_ok … EQfetch) >(fetch_stmt_ok_sigma_last_pop_ok … EQfetch)
606whd in ⊢ (??%% → ?); #EQ destruct #n_cost
607%{(mk_state_pc ? (st_no_pc … st2)
608                 (pc_of_point ERTLptr_semantics (pc_block (pc … st2)) ?)
609                 (last_pop … st2))} [ @ltrue |3: @lfalse]
610% [1,3: whd in match sigma_state_pc; normalize nodelta
611        >(fetch_stmt_ok_sigma_pc_ok … EQfetch) in EQfn; #EQfn >EQfn %]
612cases(b_graph_transform_program_fetch_statement … good … EQfetch)
613#init_data * #t_fn1 ** #EQt_fn1 whd in ⊢ (% → ?); cases (f_bl_r ?) normalize nodelta
614[2,4: #r #tl *] #EQ destruct(EQ) >if_merge_right in ⊢ (% → ?); [2,4: %] * #labs **
615[2,4: #hd #tl ** #_ #_ *** #pre #inst #post * whd in ⊢ (%→?); *] ** #EQlabs #EQf_regs
616whd in match translate_step; normalize nodelta * #bl *
617whd in ⊢ (% → ?); #EQ destruct(EQ) whd in ⊢ (% → ?); * #l1 * #mid1 * #mid2 * #l2
618*** #EQmid1 whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in ⊢ (% → ?); *
619#nxt1 * #EQcond #EQ destruct(EQ) whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2)
620whd in EQmid1 : (??%%); destruct(EQmid1)
621%{(taaf_step_jump … (taa_base …) …) I}
622[2,5: whd whd in ⊢ (??%?); whd in match fetch_statement; normalize nodelta 
623      <(fetch_stmt_ok_sigma_pc_ok … EQfetch) >EQt_fn1 >m_return_bind
624      >EQcond %
625|3,6: whd whd in match eval_state; normalize nodelta whd in match eval_statement_no_pc;
626      normalize nodelta whd in match fetch_statement; normalize nodelta
627      <(fetch_stmt_ok_sigma_pc_ok … EQfetch) >EQt_fn1 >m_return_bind
628      >EQcond >m_return_bind normalize nodelta >m_return_bind
629      whd in match eval_statement_advance; normalize nodelta
630      change with (ps_reg_retrieve ??) in match (acca_retrieve ?????);
631      cases(ps_reg_retrieve_ok … EQbv) #bv1 * #EQbv1 #EQsem >EQbv1
632      >m_return_bind >EQsem in EQbool; #EQbool cases(bool_of_beval_ok … EQbool)
633      #bool1 * #EQbool1 #EQ destruct(EQ) >EQbool1 >m_return_bind normalize nodelta
634      >(fetch_stmt_ok_sigma_pc_ok … EQfetch) [2: %] whd in match goto;
635      normalize nodelta >(fetch_stmt_ok_sigma_pc_ok … EQfetch) in EQt_fn1; #EQt_fn1
636      >(pc_of_label_eq … EQt_fn1) >m_return_bind %
637|*: lapply n_cost whd in match as_costed; normalize nodelta
638    [ cut((mk_state_pc ERTL_semantics
639   (sigma_state prog f_lbls f_regs
640    (added_registers ERTL (prog_var_names (joint_function ERTL) ℕ prog) fn
641     (f_regs (pc_block (pc ERTLptr_semantics st2)))) st2)
642   (pc_of_point ERTL_semantics (pc_block (pc ERTLptr_semantics st2)) ltrue)
643   (sigma_stored_pc prog f_lbls (last_pop ERTLptr_semantics st2))) =
644   sigma_state_pc prog f_lbls f_regs (mk_state_pc ERTLptr_semantics st2
645    (pc_of_point ERTLptr_semantics (pc_block (pc ERTLptr_semantics st2)) ltrue)
646    (last_pop ERTLptr_semantics st2))) [ whd in match sigma_state_pc; normalize  nodelta
647    >(fetch_stmt_ok_sigma_pc_ok … EQfetch) in EQfn; #EQfn >EQfn %]
648    #EQ >EQ >(as_label_ok … good … (mk_state_pc ERTLptr_semantics st2
649    (pc_of_point ERTLptr_semantics (pc_block (pc ERTLptr_semantics st2)) ltrue)
650    (last_pop ERTLptr_semantics st2))) [#H @H] cases daemon (*needs lemma see below *)
651    | cut((mk_state_pc ERTL_semantics
652   (sigma_state prog f_lbls f_regs
653    (added_registers ERTL (prog_var_names (joint_function ERTL) ℕ prog) fn
654     (f_regs (pc_block (pc ERTLptr_semantics st2)))) st2)
655   (succ_pc ERTL_semantics (pc ERTLptr_semantics st2)
656    (point_of_succ ERTLptr_semantics
657     (point_of_pc ERTLptr_semantics
658      (pc ERTL_semantics (sigma_state_pc prog f_lbls f_regs st2))) nxt1))
659   (sigma_stored_pc prog f_lbls (last_pop ERTLptr_semantics st2))) =
660   sigma_state_pc prog f_lbls f_regs (mk_state_pc ERTLptr_semantics st2
661    (pc_of_point ERTLptr_semantics (pc_block (pc ERTLptr_semantics st2))
662     (point_of_succ ERTLptr_semantics
663      (point_of_pc ERTLptr_semantics
664       (pc ERTL_semantics (sigma_state_pc prog f_lbls f_regs st2))) nxt1))
665    (last_pop ERTLptr_semantics st2))) [ whd in match sigma_state_pc; normalize  nodelta
666    >(fetch_stmt_ok_sigma_pc_ok … EQfetch) in EQfn; #EQfn >EQfn %] #EQ >EQ
667    >(as_label_ok … good … (mk_state_pc ERTLptr_semantics st2
668    (pc_of_point ERTLptr_semantics (pc_block (pc ERTLptr_semantics st2))
669     (point_of_succ ERTLptr_semantics
670      (point_of_pc ERTLptr_semantics
671       (pc ERTL_semantics (sigma_state_pc prog f_lbls f_regs st2))) nxt1))
672    (last_pop ERTLptr_semantics st2))) [#H @H] cases daemon (*needs lemma see below ! *)
673]
674qed.
675     
676lemma eval_cost_ok :
677∀prog.
678let trans_prog ≝ ertl_to_ertlptr prog in
679∀ f_lbls,f_regs,stack_sizes.
680 ∀f_bl_r.
681 ∀ good :b_graph_transform_program_props ERTL_semantics ERTLptr_semantics
682     (λglobals,fn.«translate_data globals fn,(refl …)») prog f_bl_r f_lbls f_regs.
683∀st2,st1',f,fn,c,nxt.
684let st1 ≝ sigma_state_pc prog f_lbls f_regs st2 in
685 fetch_statement ERTL_semantics …
686  (globalenv_noinit ? prog) (pc … st1) =
687    return 〈f, fn,  sequential … (COST_LABEL ERTL … c) nxt〉 →
688 eval_state ERTL_semantics
689   (prog_var_names (joint_function ERTL_semantics) ℕ prog)
690   (ev_genv … (mk_prog_params ERTL_semantics prog stack_sizes))
691   st1 = return st1' →
692∃ st2'. st1' = sigma_state_pc prog f_lbls f_regs st2' ∧
693∃taf : trace_any_any_free (ERTLptr_status trans_prog stack_sizes)
694st2 st2'.
695bool_to_Prop (taaf_non_empty … taf).
696#prog #f_lbls #f_regs #stack_Size #f_bl_r #good #st2 #st1' #f #fn #c #nxt
697#EQfetch whd in match eval_state; normalize nodelta >EQfetch >m_return_bind
698whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
699whd in match eval_statement_advance; normalize nodelta
700>(fetch_stmt_ok_sigma_state_ok … EQfetch) whd in match set_no_pc;
701normalize nodelta >(fetch_stmt_ok_sigma_pc_ok … EQfetch)
702>(fetch_stmt_ok_sigma_last_pop_ok … EQfetch) whd in match next;
703whd in match set_pc; normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ)
704%{(set_pc ? (pc_of_point ERTLptr_semantics (pc_block (pc … st2)) nxt) st2)}
705% [ whd in match sigma_state_pc; normalize nodelta
706    lapply(fetch_statement_inv … EQfetch) >(fetch_stmt_ok_sigma_pc_ok … EQfetch) *
707    #EQfn #_ >EQfn %] lapply EQfetch >(fetch_stmt_ok_sigma_pc_ok … EQfetch)
708#EQfetch'
709cases(b_graph_transform_program_fetch_statement … good … EQfetch')
710#init_data * #t_fn ** #EQt_fn whd in ⊢ (% → ?); cases(f_bl_r ?) [2: #x #y *]
711normalize nodelta #EQ destruct(EQ) * #lbls * #regs ** #_ #_ whd in ⊢ (% → ?);
712* #bl * >if_merge_right [2: %] whd in ⊢ (% → ?); cases regs [2: #x #y *]
713normalize nodelta #EQ destruct(EQ) whd in ⊢ (% → ?); * #l1 * #mid1 * #mid2 * #l2
714*** #EQmid whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in EQmid : (???%);
715destruct(EQmid) whd in ⊢ (% → ?); * #nxt1 * #EQstmt #EQ destruct(EQ)
716whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2) %{(taaf_step … (taa_base …) …)}
717[1,2: whd [ whd in ⊢ (??%?); | whd in match eval_state; ] 
718      whd in match fetch_statement; normalize nodelta >EQt_fn >m_return_bind
719      >EQstmt [%] >m_return_bind whd in match eval_statement_no_pc;
720      normalize nodelta >m_return_bind %] @I
721qed.
722
723
724lemma eval_call_ok   :
725 ∀prog : ertl_program.
726 let trans_prog ≝ ertl_to_ertlptr prog in
727∀ f_lbls,f_regs,stack_sizes.
728 ∀f_bl_r.
729 ∀ good :b_graph_transform_program_props ERTL_semantics ERTLptr_semantics
730     (λglobals,fn.«translate_data globals fn,(refl …)») prog f_bl_r f_lbls f_regs.
731 ∀st2,st1',f,fn,called,args,dest,nxt.
732 let st1 ≝ sigma_state_pc prog f_lbls f_regs st2 in
733  fetch_statement ERTL_semantics …
734    (globalenv_noinit ? prog) (pc … st1) =
735      return 〈f, fn,
736        sequential … (CALL ERTL … called args dest ) nxt〉 →
737   eval_state … (ev_genv … (mk_prog_params ERTL_semantics prog stack_sizes)) st1 =
738    return st1' →
739∃is_call,st2_pre_call,is_call'.
740as_call_ident (ERTLptr_status trans_prog stack_sizes)
741 («st2_pre_call,is_call'») = as_call_ident (ERTL_status prog stack_sizes)
742  («st1, is_call») ∧
743(pc … st1) = sigma_stored_pc prog f_lbls (pc … st2_pre_call) ∧
744∃taa2 : trace_any_any (ERTLptr_status trans_prog stack_sizes) st2 st2_pre_call.
745∃ st2'. st1' = sigma_state_pc prog f_lbls f_regs st2' ∧
746eval_state ERTLptr_semantics …
747 (ev_genv … (mk_prog_params ERTLptr_semantics trans_prog stack_sizes)) st2_pre_call
748 =return st2'.
749#prog #f_lbls #f_regs #stack_size #f_bl_r #good #st2 #st1' #f #fn * [#c_id | * #c_ptr1 #c_ptr2 ]
750#args #dest #nxt #EQfetch whd in match eval_state; normalize nodelta >EQfetch
751>m_return_bind whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
752whd in match eval_statement_advance; whd in match eval_call; normalize nodelta
753>(fetch_stmt_ok_sigma_state_ok … EQfetch) >(fetch_stmt_ok_sigma_pc_ok … EQfetch)
754>(fetch_stmt_ok_sigma_last_pop_ok … EQfetch) #H @('bind_inversion H) -H
755#c_bl whd in match set_no_pc; normalize nodelta #H lapply(err_eq_from_io ????? H) -H
756#EQc_bl cases(block_of_call_ok ??????? EQc_bl) #c_bl' * #EQc_bl' #EQ destruct(EQ)
757#H @('bind_inversion H) -H * #f1 * [1,3: #fn1 |*: #ext_f] #H
758lapply(err_eq_from_io ????? H) -H  #EQfn1 normalize nodelta
759[3,4: #H @('bind_inversion H) -H #st whd in match eval_external_call; normalize nodelta
760      #H @('bind_inversion H) -H #list_val #_ #H @('bind_inversion H) -H #x
761      #_ #H @('bind_inversion H) -H #y whd in match do_io; normalize nodelta
762      whd in ⊢ (???% → ?); #ABS destruct(ABS) ] #H lapply(err_eq_from_io ????? H) -H
763#H @('bind_inversion H) -H #st1'' >(fetch_stmt_ok_sigma_pc_ok … EQfetch)
764>(fetch_stmt_ok_sigma_last_pop_ok … EQfetch) whd in match kind_of_call;
765normalize nodelta change with (ertl_save_frame ? it ?) in ⊢ (??%? → ?);
766[2: @ID |4: @PTR] #EQst1''  #H @('bind_inversion H) -H #st1'''
767whd in match eval_internal_call; normalize nodelta #H @('bind_inversion H) -H
768#s_size #H lapply(opt_eq_from_res ???? H) -H
769change with (stack_size ?) in ⊢ (??%? → ?); #EQs_size whd in ⊢ (??%? → ?);
770whd in ⊢ (???% → ??%% → ?); #EQ #EQ1 destruct(EQ EQ1)
771lapply EQfetch >(fetch_stmt_ok_sigma_pc_ok … EQfetch) in ⊢ (% → ?);
772#EQfetch' lapply(fetch_statement_inv … EQfetch') * #EQfn normalize nodelta #EQstmt
773cases(b_graph_transform_program_fetch_statement_plus … good … EQfetch')
774#init_data * #calling' ** #EQcalling' whd in ⊢ (% → ?); cases(f_bl_r ?)
775[2,4: #x #y *] normalize nodelta #EQ destruct(EQ) * #labels * #registers
776******* #EQlabels #EQregisters #_ #_ #_ #_ #fresh_regs
777normalize nodelta >if_merge_right [2,4: %] whd in match translate_step;
778normalize nodelta * #bl * cases registers in EQregisters; -registers
779normalize nodelta [2,3: [ #x #y] #_ *|4: #r #tl] #EQregisters
780[ whd in ⊢ (% → ?); cases tl in EQregisters; -tl [2: #x #y #_ *] normalize nodelta
781#EQregisters | whd in ⊢ (% → ?);] #EQ destruct(EQ)
782* #pre_l * #mid1 * #mid2 * #post_l *** #EQmid1 #m_fetch_pre whd in ⊢ (% → ?);
783* #nxt1 * #EQcall change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ)
784whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2) cases(pre_l) in m_fetch_pre EQmid1;
785[* #x * #y ** #ABS destruct(ABS)
786|4: #lab #tl * #ABS destruct(ABS)
787| #l1 #tl #m_fetch_pre whd in ⊢ (???% → ?); #EQ destruct(EQ)
788| * #_ #EQ destruct(EQ) whd in ⊢ (???% → ?); #EQ destruct(EQ)
789]
790%
791[1,3: @hide_prf whd in ⊢ (??%?); >EQfetch %]
792cases(ertl_save_frame_ok prog f_lbls f_regs ?
793  (added_registers ERTL (prog_var_names … prog) fn1 (f_regs c_bl')) ? st1''' ?)
794[2: @PTR
795|3,7: [ %{(mk_state_pc ? (st_no_pc … st2)
796                     (pc_of_point ERTLptr_semantics (pc_block (pc … st2)) mid1)
797                     (last_pop … st2))}
798      |%{(st2)}
799      ] @hide_prf whd in match sigma_pc_opt; normalize nodelta @if_elim
800      [1,3: @eqZb_elim [2,4: #_ *] #EQbl >fetch_internal_function_no_minus_one in EQfn;
801           [1,3: #EQ destruct(EQ) |*: assumption]]
802      #_ [>point_of_pc_of_point >(get_sigma_last … good … EQfn EQstmt EQlabels)
803         | >(get_sigma_idempotent … good … EQfn EQstmt EQlabels)
804         ] >m_return_bind % whd in ⊢ (??%? → ?); #ABS destruct(ABS)
805|6: @ID
806|4,8: [change with (pc_block (pc … st2)) in match (pc_block ?);
807       >EQfn in ⊢ (??(???match % with [_ ⇒ ?| _ ⇒ ?])?);
808      |>EQfn in ⊢ (??(???match % with [_ ⇒ ?| _ ⇒ ?])?);
809      ] normalize nodelta whd in match (st_no_pc ??);
810      whd in match sigma_stored_pc in ⊢ (??(???(???%?))?);
811      whd in match sigma_pc_opt; normalize nodelta @if_elim
812     [1,3: @eqZb_elim [2,4: #_ *] #EQbl >fetch_internal_function_no_minus_one in EQfn;
813           [1,3: #EQ destruct(EQ) |*: assumption]]
814      #_ [>point_of_pc_of_point >(get_sigma_last … good … EQfn EQstmt EQlabels)
815         | >(get_sigma_idempotent … good … EQfn EQstmt EQlabels)
816         ] >m_return_bind normalize nodelta
817         change with (pc_block (pc … st2)) in match (pc_block ?);
818         >pc_of_point_of_pc assumption
819] #st_no_pc_after_call normalize nodelta *
820[ #H @('bind_inversion H) -H #st_no_pc_pre_call #EQst_no_pc_pre_call
821  whd in match set_no_pc; normalize nodelta]
822#EQst_no_pc_after_call #EQ destruct(EQ)
823[ letin pairpc ≝ (beval_pair_of_pc
824                     (pc_of_point ERTLptr_semantics (pc_block (pc … st2)) mid1))
825  %{(mk_state_pc ? (set_regs ERTL_state
826                      (〈add ?? (\fst (regs … st2)) r (\snd pairpc),\snd(regs … st2)〉)
827                      st_no_pc_pre_call)
828                   (pc_of_point ERTLptr_semantics (pc_block (pc … st2)) mid1)
829                   (last_pop … st2))}
830| %{st2}
831]
832%
833[1,3: @hide_prf whd in ⊢ (??%?); whd in match fetch_statement; normalize nodelta
834      >EQcalling' >m_return_bind [>point_of_pc_of_point ] >EQcall >m_return_bind %]
835%
836[1,3: %
837  [1,3: whd in ⊢ (??%%); whd in match fetch_statement in ⊢ (??%?);
838        normalize nodelta >EQcalling' in ⊢ (??(match % with [_ ⇒ ? | _ ⇒ ?])?);
839        >m_return_bind in ⊢ (??(match % with [_ ⇒ ? | _ ⇒ ?])?);
840       [ >point_of_pc_of_point in ⊢ (??(match % with [_ ⇒ ? | _ ⇒ ?])?);]
841       >EQcall in ⊢ (??(match % with [_ ⇒ ? | _ ⇒ ?])?); normalize nodelta
842       >(fetch_stmt_ok_sigma_pc_ok … EQfetch) in ⊢ (???(match % with [_ ⇒ ? | _ ⇒ ?]));
843       >EQfetch' in ⊢ (???(match % with [_ ⇒ ? | _ ⇒ ?])); normalize nodelta
844       >(fetch_stmt_ok_sigma_state_ok … EQfetch) >EQc_bl >m_return_bind
845       lapply EQc_bl' whd in match block_of_call; normalize nodelta
846       cases daemon (* CSC: The proof used to be %, why did it change? *)
847                    (* This point will be generalized when the call case
848                       will be available in StatusSimulationHelper*)
849       (*
850       XXX
851       
852       [cut (block_of_call
853        (mk_prog_params ERTLptr_semantics (ertl_to_ertlptr prog) stack_size)
854        (globals
855         (mk_prog_params ERTLptr_semantics (ertl_to_ertlptr prog) stack_size))
856        (ev_genv
857         (mk_prog_params ERTLptr_semantics (ertl_to_ertlptr prog) stack_size))
858        (inr ident … 〈c_ptr1,c_ptr2〉)
859        (set_regs ERTL_state
860         〈add RegisterTag beval (\fst  (regs ERTLptr_semantics st2)) r
861          (\snd  (beval_pair_of_pc
862                       (pc_of_point ERTLptr_semantics
863                        (pc_block (pc ERTLptr_semantics st2)) mid1))),
864         \snd  (regs ERTLptr_semantics st2)〉
865         st_no_pc_pre_call) =
866         block_of_call (mk_prog_params ERTL_semantics prog stack_size)
867         (globals (mk_prog_params ERTL_semantics prog stack_size))
868         (ev_genv (mk_prog_params ERTL_semantics prog stack_size))
869         (inr ident … 〈c_ptr1,c_ptr2〉)
870         (sigma_state_pc prog f_lbls f_regs st2))
871         
872         [2: #URCA <URCA cases block_of_call #xyz
873             [2: whd in ⊢ (??%%); %]
874             >m_return_bind >m_return_bind
875             whd in match fetch_internal_function; normalize nodelta
876             whd in match fetch_function; normalize nodelta
877         XXX
878         %*)
879  |*:  whd in match sigma_stored_pc; whd in match sigma_pc_opt; normalize nodelta
880      @if_elim change with (pc_block(pc … st2)) in match (pc_block ?);
881      [1,3: @eqZb_elim [2,4: #_ *] #EQbl #_
882      >fetch_internal_function_no_minus_one in EQcalling'; [2,4: assumption]
883      whd in ⊢ (???% → ?); #ABS destruct(ABS) ] #_
884      [ >point_of_pc_of_point >(get_sigma_last … good … EQfn EQstmt EQlabels)
885      | >(get_sigma_idempotent … good … EQfn EQstmt EQlabels)
886      ]
887      >m_return_bind >pc_of_point_of_pc %
888  ]
889|4: %{(taa_base …)}
890| %{(taaf_to_taa ???
891      (produce_trace_any_any_free
892           (mk_prog_params ERTLptr_semantics (ertl_to_ertlptr prog) stack_size)
893           st2 ?????
894           (mk_state_pc ?
895                (set_regs ERTL_state
896                      (〈add ?? (\fst (regs … st2)) r (\snd pairpc),\snd(regs … st2)〉)
897                      st_no_pc_pre_call)
898                (pc_of_point ERTLptr_semantics (pc_block (pc … st2)) mid1)
899                (last_pop … st2))
900           EQcalling' m_fetch_pre ?) ?)}
901  [ @if_elim [2: #_ @I] #_ % whd in ⊢ (% → ?); whd in match (as_label ??);
902    whd in match (as_pc_of ??); whd in match fetch_statement; normalize nodelta
903    >EQcalling' >m_return_bind whd in match point_of_pc; normalize nodelta
904    >point_of_offset_of_point >EQcall >m_return_bind normalize nodelta
905    whd in match cost_label_of_stmt; normalize nodelta * #H @H %
906  | whd in match repeat_eval_seq_no_pc; normalize nodelta whd in ⊢ (??%?);
907    whd in match eval_seq_no_pc in ⊢ (??match % with [_ ⇒ ?| _ ⇒ ?]?);
908    normalize nodelta whd in match (eval_ext_seq ????????);
909    whd in match (get_pc_from_label ?????); whd in match block_of_funct_id;
910    normalize nodelta @('bind_inversion EQfn) * #f2 * #fn2
911    whd in match fetch_function; normalize nodelta #H
912    lapply(opt_eq_from_res ???? H) -H #H @('bind_inversion H) -H #f3 #EQf3
913    #H @('bind_inversion H) -H #fn4 #_ whd in ⊢ (??%%→ ??%% → ?); #EQ1 #EQ2
914    destruct(EQ1 EQ2)
915    >(find_symbol_transf …
916            (λvars.transf_fundef … (λfn.(b_graph_translate … fn))) prog f)
917    >(symbol_of_block_rev … EQf3) >m_return_bind >code_block_of_block_eq
918    normalize nodelta >(pc_of_label_eq … EQcalling') normalize nodelta
919    whd in ⊢ (??%?);
920    whd in match eval_seq_no_pc in ⊢ (??match % with [_ ⇒ ?| _ ⇒ ?]?);
921    normalize nodelta whd in match (eval_ext_seq ????????);
922    whd in match acca_arg_retrieve; normalize nodelta
923    change with (ps_reg_retrieve ??) in match (acca_arg_retrieve_ ?????);
924    whd in match ps_reg_retrieve; whd in match reg_retrieve; normalize nodelta
925    >lookup_add_hit >m_return_bind whd in match set_regs; normalize nodelta
926    @('bind_inversion EQst_no_pc_pre_call) #new_st whd in match push in ⊢ (%→ ?);
927    normalize nodelta #H @('bind_inversion H) -H #is1 #EQis1 whd in ⊢ (??%% → ?);
928    #EQ destruct(EQ) #H @('bind_inversion H) -H #is2 #EQis2 whd in match set_istack;
929    normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ) whd in match push;
930    normalize nodelta >EQis1 >m_return_bind whd in match set_istack; normalize nodelta
931    whd in ⊢ (??%?); whd in match eval_seq_no_pc in ⊢ (??match % with [_ ⇒ ?| _ ⇒ ?]?);
932    normalize nodelta whd in match (eval_ext_seq ????????);
933    whd in match (get_pc_from_label ?????); whd in match block_of_funct_id;
934    normalize nodelta
935    >(find_symbol_transf …
936            (λvars.transf_fundef … (λfn.(b_graph_translate … fn))) prog f)
937    >(symbol_of_block_rev … EQf3) >m_return_bind >code_block_of_block_eq
938    normalize nodelta >(pc_of_label_eq … EQcalling') normalize nodelta
939    whd in ⊢ (??%?);
940    whd in match eval_seq_no_pc in ⊢ (??match % with [_ ⇒ ?| _ ⇒ ?]?);
941    normalize nodelta whd in match (eval_ext_seq ????????);
942    whd in match acca_arg_retrieve; normalize nodelta
943    change with (ps_reg_retrieve ??) in match (acca_arg_retrieve_ ?????);
944    whd in match ps_reg_retrieve; whd in match reg_retrieve; normalize nodelta
945    >lookup_add_hit >m_return_bind whd in match set_regs; normalize nodelta
946    whd in match push; normalize nodelta >EQis2 >m_return_bind normalize nodelta
947    whd in ⊢ (??%?); @eq_f whd in match set_istack; normalize nodelta
948    whd in match reg_store; normalize  nodelta >add_idempotent %
949  | cut(∀st,st',kind.ertlptr_save_frame kind it st = return st' →
950                ∃hd,tl.st_frms … st' = return (cons ? hd tl) ∧
951                \snd hd = pc_block (pc … st))
952    [ #st * #frms #is #b #regs #m * whd in match ertlptr_save_frame;
953      normalize nodelta [ >m_return_bind | #H @('bind_inversion H) -H #st'' #EQst'']
954      #H @('bind_inversion H) -H #frames #H lapply(opt_eq_from_res ???? H) -H
955      #EQframes whd in ⊢ (??%% → ?); whd in match set_frms; whd in match set_regs;
956      normalize nodelta #EQ destruct(EQ) %{(〈\fst (regs ERTLptr_semantics ?),pc_block (pc … st)〉)}
957      [2,4: %{frames} % [1,3: %] |1,3:] %]
958    ] #save_frame_non_empty cases(save_frame_non_empty … EQst_no_pc_after_call)
959    * #fst_hd #snd_hd * #rest * #EQrest #EQhd
960  ]
961cases(b_graph_transform_program_fetch_internal_function … good c_bl' f1 fn1 ?)
962[2,4: whd in match fetch_internal_function; normalize nodelta >EQfn1 %]
963#init * #t_fn1 ** #EQt_fn1 #_ * #_ #_ #_ #EQentry #_ #_ #_ #_ #_ #_ #_
964[ %{(mk_state_pc ? st_no_pc_after_call
965        (pc_of_point
966            (mk_prog_params ERTLptr_semantics (ertl_to_ertlptr prog) stack_size)
967             c_bl' (joint_if_entry … t_fn1))
968        (last_pop … st2))}
969|
970%{(mk_state_pc ? (set_frms ERTL_state (〈(add ?? (fst_hd) r (\snd pairpc)),snd_hd〉
971                                 :: rest)
972                          st_no_pc_after_call)
973        (pc_of_point
974            (mk_prog_params ERTLptr_semantics (ertl_to_ertlptr prog) stack_size)
975             c_bl' (joint_if_entry … t_fn1))
976        (last_pop … st2))}
977]
978%
979[1,3: whd in match sigma_state_pc; normalize nodelta
980      whd in match pc_of_point in ⊢ (???%); normalize nodelta
981      whd in match fetch_internal_function; normalize nodelta >EQfn1
982      >m_return_bind normalize nodelta @eq_f3
983      [1,3,6: % |2,5: >EQentry %]
984      whd in match sigma_state; normalize nodelta
985      cut(∀ a1,a2,b1,b2,c1,c2,d1,d2,e1,e2.
986                    a1=a2 → b1 = b2 → c1 = c2 → d1 = d2 → e1 = e2 →
987                      mk_state ERTL_semantics a1 b1 c1 d1 e1 =
988                      mk_state ERTL_semantics a2 b2 c2 d2 e2)
989       [1,3: #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14
990                    #H15 //] #APP @APP try %
991       whd in match set_frms; normalize nodelta >EQrest
992       whd in match sigma_frames; normalize nodelta >m_return_bind
993       >m_return_bind whd in match sigma_frames_opt; whd in match m_list_map;
994       normalize nodelta whd in match (foldr ?????) in ⊢ (???%);
995       normalize nodelta >EQhd >EQfn >m_return_bind normalize nodelta
996       whd in match (foldr ?????); normalize nodelta
997       >EQfn >m_return_bind normalize nodelta 
998       change with (sigma_frames_opt prog f_lbls f_regs ?)
999                                            in match (foldr ?????);
1000       change with (sigma_frames_opt prog f_lbls f_regs ?)
1001                                                         in match (foldr ?????);
1002       cases(sigma_frames_opt ????) [%] #t_rest >m_return_bind >m_return_bind
1003       @eq_f @eq_f2 [2: %] @eq_f2 [2: %]
1004       change with (pc_block (pc … st2)) in match (pc_block ?);
1005       change with (pc_block (pc … st2)) in match (pc_block ?);
1006       whd in match sigma_register_env; normalize nodelta
1007       >map_add >set_minus_add [%] @list_as_set_mem @in_added_registers
1008       [@(point_of_pc ERTL_semantics (pc ERTLptr_semantics st2))
1009       | whd in match code_has_label; whd in match code_has_point; normalize nodelta
1010         >EQstmt % | >EQregisters % % ]
1011|*:    whd in match fetch_statement; normalize nodelta; >EQcalling' >m_return_bind
1012       [2: >point_of_pc_of_point ] >EQcall >m_return_bind normalize nodelta
1013       >m_return_bind
1014       [2: >EQc_bl' >m_return_bind
1015       | whd in match block_of_call; normalize nodelta
1016         @('bind_inversion EQst_no_pc_pre_call) #st3 #H @('bind_inversion H) -H
1017         #is3 inversion(istack … st2) [2: #bv |3: #bv1 #bv2] #EQis3
1018         whd in match is_push; normalize nodelta whd in ⊢ (??%% → ??%% → ?);
1019         #EQ1 #EQ2 destruct(EQ1 EQ2) #H @('bind_inversion H) -H #is3
1020         whd in ⊢ (??%% → ??%% → ?); #EQ1 #EQ2 destruct(EQ1 EQ2)
1021         whd in match set_regs; whd in match dpl_arg_retrieve; normalize nodelta
1022         change with (ps_arg_retrieve ??) in match (dpl_arg_retrieve_ ?????);
1023         @('bind_inversion EQc_bl') #c_bl'' whd in match dpl_arg_retrieve; normalize nodelta
1024         change with (ps_arg_retrieve ??) in match (dpl_arg_retrieve_ ?????);
1025         #H @('bind_inversion H) -H #bv_ptr1 whd in match ps_arg_retrieve;
1026         normalize nodelta cases (c_ptr1) in EQstmt; [#r_ptr1 | #b_ptr1] #EQstmt
1027         normalize nodelta
1028         [ whd in match ps_reg_retrieve; whd in match reg_retrieve; normalize nodelta
1029           #H lapply(opt_eq_from_res ???? H) -H #EQbv_ptr1
1030         | whd in ⊢ (??%% → ?); #EQ destruct(EQ)
1031         ]
1032         whd in match dph_arg_retrieve; normalize nodelta
1033         change with (ps_arg_retrieve ??) in match (dph_arg_retrieve_ ?????);
1034         whd in match ps_arg_retrieve; normalize nodelta cases c_ptr2 in EQstmt;
1035         [1,3: #r_ptr2 |*: #b_ptr2] #EQstmt normalize nodelta
1036         [1,2: whd in match ps_reg_retrieve; whd in match reg_retrieve;
1037               normalize nodelta #H @('bind_inversion H) -H
1038               #bv_ptr2 #H lapply(opt_eq_from_res ???? H) -H #EQbv_ptr2
1039         |*:   >m_return_bind
1040         ] #H @('bind_inversion H) -H #ptr #EQptr @if_elim #ptr_ok whd in ⊢ (??%% → ?);
1041         #EQ destruct(EQ) #H lapply(opt_eq_from_res ???? H) -H #EQptr_code
1042         [2,4: >m_return_bind
1043         |*: >lookup_add_miss
1044             [1,3: >EQbv_ptr1 >m_return_bind
1045             |*: % #ABS destruct(ABS)
1046                lapply(fresh_regs (point_of_pc ERTL_semantics (pc … st2)))
1047                >EQregisters whd in ⊢ (% → ?); *** #ABS #_ #_ @ABS
1048                lapply(regs_are_in_univers … (pi2 ?? fn) … EQstmt) whd in match stmt_registers;
1049                whd in match get_used_registers_from_step; normalize nodelta
1050                whd in ⊢ (???% → ?); * //
1051             ]
1052         ]
1053         change with (ps_arg_retrieve ??) in match (dph_arg_retrieve_ ?????);
1054         whd in match ps_arg_retrieve; normalize nodelta
1055         [2,4: >m_return_bind   
1056         |*: whd in match ps_reg_retrieve; whd in match reg_retrieve;
1057             normalize nodelta >lookup_add_miss
1058             [1,3: >EQbv_ptr2 >m_return_bind
1059             |*: % #ABS destruct(ABS)
1060                lapply(fresh_regs (point_of_pc ERTL_semantics (pc … st2)))
1061                >EQregisters whd in ⊢ (% → ?); *** #ABS #_ #_ @ABS
1062                lapply(regs_are_in_univers … (pi2 ?? fn) … EQstmt) whd in match stmt_registers;
1063                whd in match get_used_registers_from_step; normalize nodelta
1064                whd in ⊢ (???% → ?); * // #_ * //
1065             ]
1066         ]
1067         >EQptr >m_return_bind @if_elim [2,4,6,8: >ptr_ok *] #_ >m_return_bind
1068         >EQptr_code >m_return_bind
1069       ]
1070       @('bind_inversion EQt_fn1) * #f2 * #fn2 #EQfn2 normalize nodelta
1071       whd in ⊢ (??%% → ?); #EQ destruct(EQ) >EQfn2 >m_return_bind normalize nodelta
1072       [   change with (ertlptr_save_frame ? it ?) in match (save_frame ??????);
1073           cut(st2 = mk_state_pc ? st2 (pc … st2) (last_pop … st2))
1074           [ cases st2 #H1 #H2 #H3 %] #EQ <EQ -EQ >EQst_no_pc_after_call
1075           >m_return_bind
1076       |*: change with (ertlptr_save_frame PTR it ?) in match (save_frame ??????);
1077           @('bind_inversion EQst_no_pc_after_call) #st4 whd in ⊢ (??%% → ?);
1078           #EQ destruct(EQ) #H @('bind_inversion H) -H #frms4 #H
1079           lapply(opt_eq_from_res ???? H) -H #EQfrms4 whd in ⊢ (??%% → ?);
1080           #EQ destruct(EQ) whd in match ertlptr_save_frame; normalize nodelta
1081           >m_return_bind whd in EQrest : (???%); destruct(EQrest) >EQfrms4
1082           >m_return_bind
1083       ]
1084       change with (stack_size ?) in match (stack_sizes ????); >EQs_size
1085       >m_return_bind %
1086]
1087qed.
1088         
1089
1090inductive ex_Type1 (A:Type[1]) (P:A → Prop) : Prop ≝
1091    ex1_intro: ∀ x:A. P x →  ex_Type1 A P.
1092(*interpretation "exists in Type[1]" 'exists x = (ex_Type1 ? x).*)
1093
1094lemma ertl_to_ertlptr_ok:
1095∀prog.∀stack_sizes.
1096let trans_prog ≝ ertl_to_ertlptr prog in
1097   ex_Type1 … (λR.
1098   status_simulation
1099    (ERTL_status prog stack_sizes) (ERTLptr_status trans_prog stack_sizes) R).
1100#prog #stack_size
1101cases(make_b_graph_transform_program_props ERTL_semantics ERTLptr_semantics
1102          (λglobals,fn.«translate_data globals fn,(refl …)») prog)
1103#fregs * #f_lbls * #f_bl_r #good %
1104[@ERTLptrStatusSimulation assumption]
1105whd in match status_simulation; normalize nodelta
1106whd in match ERTL_status; whd in match ERTLptr_status; normalize nodelta
1107whd in ⊢ (% → % → % → % → ?); #st1 #st1' #st2
1108change with
1109  (eval_state ERTL_semantics (prog_var_names ???) ?? = ? → ?) 
1110#EQeval @('bind_inversion EQeval)
1111** #id #fn #stmt #H lapply (err_eq_from_io ????? H) -H #EQfetch
1112#_  whd in match ERTLptrStatusSimulation; normalize nodelta #EQst2 destruct
1113cases stmt in EQfetch; -stmt
1114[ * [ #cost | #called_id #args #dest| #reg #lbl | #seq] #nxt | #fin_step | *]
1115#EQfetch
1116change with (joint_classify ??) in
1117                     ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]);
1118[ (*COST*) whd in match joint_classify; normalize nodelta >EQfetch normalize nodelta
1119  cases(eval_cost_ok … good … EQfetch EQeval) #st2' * #EQst2' * #taf #tafne
1120  %{st2'} %{taf} >tafne normalize nodelta % [ % [@I | assumption]]
1121  whd >EQst2' >(as_label_ok … good … st2') [%] cases daemon (* needs lemma see below!! *)
1122| (*CALL*)  whd in match joint_classify; normalize nodelta >EQfetch
1123          normalize nodelta #is_call_st1
1124          cases(eval_call_ok … good … EQfetch EQeval) #is_call_st1'
1125          * #st2_pre_call * #is_call_st2_pre_call * * #Hcall
1126          #call_rel * #taa * #st2' * #sem_rel #eval_rel
1127          %{(«st2_pre_call,is_call_st2_pre_call»)} % [ % assumption]
1128          %{st2'} %{st2'} %{taa} %{(taa_base …)} % [ % assumption]
1129          whd >sem_rel >(as_label_ok … good … st2') [%] cases daemon (*TODO*)
1130| (*COND*) whd in match joint_classify; normalize nodelta >EQfetch
1131          normalize nodelta #n_costed
1132          cases(eval_cond_ok … good … EQfetch EQeval) [2: @n_costed]
1133          #st2' * #EQst2' * #taf #tafne %{st2'} %{taf} >tafne % [% [@I|assumption]]
1134          whd >EQst2' >(as_label_ok … good … st2') [%] cases daemon (*TODO*)
1135| (*seq*) whd in match joint_classify; normalize nodelta >EQfetch
1136          normalize nodelta
1137          cases (eval_seq_no_call_ok … good … EQfetch EQeval)
1138          #st3 * #EQ destruct *  #taf #taf_spec %{st3} %{taf} 
1139          % [% //] whd >(as_label_ok … good … st3) [%]
1140          cases daemon (*needs lemma about preservation of fetch_statement *)
1141|  cases fin_step in EQfetch;
1142  [ (*GOTO*) #lbl #EQfetch  whd in match joint_classify; normalize nodelta
1143     >EQfetch normalize nodelta
1144    cases (eval_goto_ok … good  … EQfetch EQeval)
1145    #st3 * #EQ destruct * #taf #tarne %{st3} %{taf} >tarne normalize nodelta
1146    % [% //] whd >(as_label_ok … good … st3) [%]
1147    cases daemon (*needs lemma about preservation of fetch_statement *)
1148  | (*RETURN*) #EQfetch
1149     whd in match joint_classify; normalize nodelta
1150    >EQfetch  normalize nodelta
1151    cases (eval_return_ok … good … EQfetch EQeval) #is_ret
1152    * #st3 * #EQ destruct * #after_ret * #taf ** #taf_prf #EQeval' #ret_prf
1153    % [2: % [2: % [2: %{(taa_base …)} %{taf}] |*: ] |*:]
1154    % [2: whd >(as_label_ok … good … st3) [%] cases daemon (*needs lemma *)]
1155    % [2: assumption] % [2: %] % [2: assumption] % assumption
1156  | (*TAILCALL*) *
1157  ]
1158]
1159qed.
1160
1161(*
1162lemma foo :
1163 ∀P1_unser,P2_unser: unserialized_params.
1164 ∀P1_sem_unser,P2_sem_unser.
1165 let P1_sem ≝ make_sem_graph_params P1_unser P1_sem_unser in
1166 let P2_sem ≝ make_sem_graph_params P2_unser P2_sem_unser in
1167 ∀init,translate_step.
1168 ∀translate_fin_step.
1169 ∀closed_graph_translate.
1170 let translate_internal :
1171  ∀globals.
1172   joint_closed_internal_function P1_sem globals →
1173   joint_closed_internal_function P2_sem globals
1174  ≝
1175  λglobals,fun.
1176   «b_graph_translate (mk_graph_params P1_sem) (mk_graph_params P2_sem) globals
1177    (init globals)
1178    (translate_step globals)
1179    (translate_fin_step globals)
1180    (pi1 … fun), closed_graph_translate globals fun» in
1181 ∀prog.
1182 let trans_prog ≝ transform_program ??? prog (λvarnames. transf_fundef ?? (translate_internal varnames)) in
1183 ∀stack_size.
1184 ∀sigma_state_pc.
1185 (∀s. pc_block (pc … (sigma_state_pc s)) = pc_block … (pc … s)) →
1186 ∀st : state_pc P2_sem.
1187 ∀st' : state_pc P1_sem.
1188 ∀f.
1189 ∀fn: joint_closed_internal_function P1_sem (globals (mk_prog_params P1_sem prog stack_size)).
1190 luniverse_ok … fn →
1191 ∀stmt,nxt.
1192 ∀P : (state_pc P2_sem) → Prop.
1193 (∀pre_Instrs',last_Instrs',dst.
1194   ∃st''.∃st'''.∃st''''.
1195    repeat_eval_seq_no_pc (mk_prog_params P2_sem trans_prog stack_size)
1196     f (translate_internal ? fn) (map_eval ?? pre_Instrs' dst) st = return st''' ∧
1197    eval_seq_no_pc ? (prog_var_names … trans_prog) (ev_genv … (mk_prog_params P2_sem trans_prog stack_size))
1198                      f (translate_internal … fn) (last_Instrs' dst) st''' = return st'''' ∧
1199    st'' = (mk_state_pc (mk_prog_params P2_sem trans_prog stack_size)
1200     st'''' (pc_of_point P2_sem (pc_block (pc … (sigma_state_pc st))) dst) (last_pop … st)) ∧
1201    P st'' (*st' = sigma_state_pc st''*) ∧
1202    let P2_prog_params ≝ mk_prog_params P2_sem trans_prog stack_size in
1203    let P2_globals ≝ globals P2_prog_params in
1204     All
1205      (joint_seq … P2_globals)
1206      (no_cost_label … P2_globals)
1207      (map_eval (code_point P2_sem) (joint_seq … P2_globals) pre_Instrs' dst)) →
1208 fetch_statement …
1209  (prog_var_names (joint_function P1_sem) ℕ prog)
1210  (ev_genv (mk_prog_params P1_sem prog stack_size))
1211  (pc … (sigma_state_pc st)) =
1212    return 〈f, fn,  sequential … (step_seq P1_sem … stmt) nxt〉 →
1213 eval_state …
1214 (prog_var_names (joint_function P1_sem) ℕ prog)
1215 (ev_genv … (mk_prog_params P1_sem prog stack_size))
1216 (sigma_state_pc st) = return st' →
1217 ∃st''. (*CSC: this needs to be linked back again st' = sigma_state_pc ? good st'' ∧*)
1218 P st'' ∧
1219 ∃taf : trace_any_any_free (joint_abstract_status (mk_prog_params P2_sem trans_prog stack_size)) st st''.
1220(if taaf_non_empty … taf then True else
1221(¬as_costed (joint_abstract_status (mk_prog_params P1_sem prog stack_size)) (sigma_state_pc st) ∨
1222 ¬as_costed (joint_abstract_status (mk_prog_params P1_sem prog stack_size)) st'))
1223 (* the length of taf is the same of the length of ??? *).
1224#P1_unser #P2_unser #P1_sem_unser #P2_sem_unser
1225letin P1_sem ≝ (make_sem_graph_params P1_unser P1_sem_unser)
1226letin P2_sem ≝ (make_sem_graph_params P2_unser P2_sem_unser)
1227#init #translate_step #translate_fin_step #closed_graph_translate.
1228letin translate_internal ≝
1229 (λglobals,fun.
1230   «b_graph_translate (mk_graph_params P1_sem) (mk_graph_params P2_sem) globals
1231    (init globals)
1232    (translate_step globals)
1233    (translate_fin_step globals)
1234    (pi1 … fun), closed_graph_translate globals fun»)
1235#prog
1236letin trans_prog ≝ (transform_program ??? prog (λvarnames. transf_fundef ?? (translate_internal varnames)))
1237#stack_size #sigma_state_pc #sigma_state_pc_ok #st #st' #f #fn #fn_universe_ok #stmt #nxt #P
1238#Hpass #EQfetch lapply(fetch_statement_inv … EQfetch) * #EQfn #EQstmt
1239cases
1240 (b_graph_translate_ok … (init …) (translate_step …) (translate_fin_step …) … fn_universe_ok)
1241#_ * #MK_fresh_labels * #MK_fresh_registers **** #_ #_ #_ #_ (*CSC: useful things thrown out here *)
1242#MULTI_FETCH_OK cases (MULTI_FETCH_OK … EQstmt)
1243#list_b_last * #fresh_registers ** #EQlist_b_last #EQfresh_registers
1244normalize nodelta * #Instrs * #fresh_registers_spec whd in ⊢ (% → ?);
1245@pair_elim #pre_Instrs #last_Instrs #EQInstrs * #dst * #Multi_fetch #STEP_in_code
1246#EQeval
1247cut((list
1248   (code_point P2_sem
1249    →joint_seq P2_sem (prog_var_names (joint_function P1_sem) ℕ prog)))) [ cases daemon (*Paolo should fix the lemma*)]
1250#pre_Instrs'
1251cut((code_point P2_sem
1252   →joint_seq P2_sem (prog_var_names (joint_function P1_sem) ℕ prog))) [ cases daemon (*Paolo should fix the lemma*)]
1253#last_Instrs'
1254cases (Hpass pre_Instrs' last_Instrs' dst (* MANY MORE HERE *))
1255#st'' * #st''' * #st'''' **** #REPEAT #EVAL_NO_PC_Last #EQst'' #EQst' #NO_COSTED
1256lapply(produce_trace_any_any_free … NO_COSTED … REPEAT)
1257[ cases daemon (* should be @Multi_fetch *)
1258| <sigma_state_pc_ok @(fetch_internal_function_transf … (λvars.translate_internal vars))
1259  assumption
1260| @dst
1261| @list_b_last (*wrong, should dst be destination or the last of list_b_last *)
1262] #TAAF
1263lapply
1264  (produce_step_trace (mk_prog_params P2_sem trans_prog stack_size)
1265    (mk_state_pc (mk_prog_params P2_sem trans_prog stack_size)
1266       st''' (pc_of_point P2_sem (pc_block (pc … st)) dst) (last_pop … st))
1267    f (translate_internal ? fn) (last_Instrs' dst) nxt st'''' … EVAL_NO_PC_Last)
1268[ cases daemon (* should be @STEP_In_code *)
1269| <sigma_state_pc_ok
1270  @(fetch_internal_function_transf … (λvars. translate_internal vars) … EQfn) ]
1271#LAST_STEP
1272cases daemon
1273qed.
1274
1275lemma eval_seq_no_call_ok :
1276 ∀prog.
1277 let trans_prog ≝ ertl_to_ertlptr prog in
1278 ∀good : (∀fn.good_state_transformation prog fn).     
1279 ∀stack_sizes.
1280 (*? →*)
1281 ∀st : state_pc ERTLptr_semantics.
1282 ∀st' : state_pc ERTL_semantics.
1283 ∀f,fn,stmt,nxt.
1284   fetch_statement ERTL_semantics
1285     (prog_var_names (joint_function ERTL_semantics) ℕ prog)
1286    (ev_genv (mk_prog_params ERTL_semantics prog stack_sizes))
1287    (pc … (sigma_state_pc ? good st)) =
1288      return 〈f, fn,  sequential … (step_seq ERTL … stmt) nxt〉 →
1289   eval_state ERTL_semantics
1290   (prog_var_names (joint_function ERTL_semantics) ℕ prog)
1291   (ev_genv … (mk_prog_params ERTL_semantics prog stack_sizes))
1292   (sigma_state_pc ? good st) =
1293    return st' →
1294 ∃st''. st' = sigma_state_pc ? good st'' ∧
1295 ∃taf : trace_any_any_free (ERTLptr_status trans_prog stack_sizes)
1296  st
1297  st''.
1298 bool_to_Prop (taaf_non_empty … taf).
1299#prog #good #stack_size #st #st' #f #fn #stmt #nxt #EQfetch #EQeval
1300cases (foo … translate_step translate_fin_step … EQfetch EQeval)
1301[2,3: cases daemon (* first one, take out init definition from ERTLtoERTLptr;
1302                      second one to be taken from somewhere *)
1303|4: #x cases daemon (* TO BE DONE, EASY *)
1304|5: cases daemon (* to be taken in input *)
1305|6: @(λst''.st' = sigma_state_pc ? good st'')
1306|7: cases daemon
1307| #st'' * #EQ destruct * change with ERTL_uns in match (mk_unserialized_params ???????????????);
1308  change with ERTLptr_uns in match (mk_unserialized_params ???????????????);
1309  (* change with ERTL_semantics in match (make_sem_graph_params ??);
1310  change with ERTLptr_semantics in match (make_sem_graph_params ??); *)
1311#taaf #Htaaf %{st''}
1312 % [%] cases daemon
1313 qed. *)
Note: See TracBrowser for help on using the repository browser.