source: src/ERTL/ERTLtoERTLptrOK.ma @ 2898

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

1) simplification of cond and seq case for StatusSimulationHelper? which has
been tested correct in ERTL to ERTlptr correctness proof.

2) the cond case for ERTLptr to LTL correctenss proof has been adapted to the
new specification

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