source: src/ERTL/ERTLtoERTLptrOK.ma @ 2801

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

Partial commit not yet finished

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