source: src/ERTL/ERTLtoERTLptrOK.ma @ 2940

Last change on this file since 2940 was 2940, checked in by sacerdot, 7 years ago
  1. StatusSimulationHelper? changed to allow to use status_rel that depends on the pc (necessary for ERTLptrToLTL)
  2. partial repairing of ERTLToERTLptrOK.ma, still in progress
  3. some progress in ERTLptrToLTLProof, but: a) some axioms were wrong, once fixed we now see some proof obligations

related to liveness analysis. Example: the variables live before and
after a COND must be the same. I have put daemons for the time being.

b) I strongly suspect that Interference should be changed to use livebefore,

in the correctness conditions (now it uses liveafter, the two sets
are probably equivalent for correct programs, but one is simpler to use:
which one?)

c) to_be_cleared_* must consult livebefore, but it is now passed liveafter.

Passing liveafter is necessary to typechek the graph, unless we do
b) first. Passing only the set computed by livebefore would be so much
better.

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