source: src/ERTL/ERTLtoERTLptrUtils.ma @ 2943

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

added precondition on seq statement and tested correct in the ERTl-ERTLptr passed

File size: 77.0 KB
Line 
1(**************************************************************************)
2(*       ___                                                              *)
3(*      ||M||                                                             *)
4(*      ||A||       A project by Andrea Asperti                           *)
5(*      ||T||                                                             *)
6(*      ||I||       Developers:                                           *)
7(*      ||T||         The HELM team.                                      *)
8(*      ||A||         http://helm.cs.unibo.it                             *)
9(*      \   /                                                             *)
10(*       \ /        This file is distributed under the terms of the       *)
11(*        v         GNU General Public License Version 2                  *)
12(*                                                                        *)
13(**************************************************************************)
14
15include "ERTL/ERTLToERTLptr.ma".
16include "common/StatusSimulation.ma".   
17include "joint/Traces.ma".
18include "ERTLptr/ERTLptr_semantics.ma".
19include "common/ExtraMonads.ma".
20
21
22definition ERTL_status ≝
23λprog : ertl_program.λstack_sizes.
24joint_abstract_status (mk_prog_params ERTL_semantics prog stack_sizes).
25
26definition ERTLptr_status ≝
27λprog : ertlptr_program.λstack_sizes.
28joint_abstract_status (mk_prog_params ERTLptr_semantics prog stack_sizes).
29
30definition sigma_map ≝  block → label → option label.
31definition lbl_funct ≝  block → label → (list label).
32definition regs_funct ≝ block → label → (list register).
33
34(*TO BE MOVED*)
35lemma match_reg_elim : ∀ A : Type[0]. ∀ P : A → Prop. ∀ r : region.
36∀f : (r = XData) → A. ∀g : (r = Code) → A. (∀ prf : r = XData.P (f prf)) →
37(∀ prf : r = Code.P (g prf)) →
38P ((match r return λx.(r = x → ?) with
39    [XData ⇒ f | Code ⇒ g])(refl ? r)).
40#A #P * #f #g #H1 #H2 normalize nodelta [ @H1 | @H2]
41qed.
42
43definition get_sigma :
44ertl_program → lbl_funct → sigma_map ≝
45λprog,f_lbls.λbl,searched.
46let globals ≝ prog_var_names … prog in
47let ge ≝ globalenv_noinit … prog in
48! bl ← code_block_of_block bl ;
49! 〈id,fn〉 ← res_to_opt … (fetch_internal_function … ge bl);
50!〈res,s〉 ← find ?? (joint_if_code … fn)
51                (λlbl.λ_. match split_on_last … (f_lbls bl lbl) with
52                          [None ⇒ eq_identifier … searched lbl
53                          |Some x ⇒ eq_identifier … searched (\snd x)
54                          ]);
55return res.
56
57definition sigma_pc_opt : 
58ertl_program →  lbl_funct →
59program_counter → option program_counter ≝
60λprog,f_lbls,pc.
61  let sigma ≝ get_sigma prog f_lbls in
62  let ertl_ptr_point ≝ point_of_pc ERTLptr_semantics pc in
63  if eqZb       (block_id (pc_block pc)) (-1) then (* check for dummy exit pc *)
64    return pc
65  else
66       ! ertl_point ← sigma (pc_block pc) ertl_ptr_point;
67       return pc_of_point
68                   ERTL_semantics (pc_block pc) ertl_point.
69
70definition sigma_stored_pc ≝
71λprog,f_lbls,pc. match sigma_pc_opt prog f_lbls pc with
72      [None ⇒ null_pc (pc_offset … pc) | Some x ⇒ x].
73     
74     
75definition sigma_beval : ertl_program → lbl_funct →
76  beval → beval ≝
77λprog,f_lbls,bv.
78match bv with
79[ BVpc pc prt ⇒ match sigma_pc_opt prog f_lbls pc with
80                 [None ⇒ BVundef | Some x ⇒ BVpc x prt]
81| _ ⇒ bv
82].
83
84definition sigma_is : ertl_program → lbl_funct →
85internal_stack → internal_stack ≝
86λprog,f_lbls,is.
87match is with
88[ empty_is ⇒ empty_is
89| one_is bv ⇒ one_is (sigma_beval prog f_lbls bv)
90| both_is bv1 bv2 ⇒
91  both_is (sigma_beval prog f_lbls bv1) (sigma_beval prog f_lbls bv2)
92].
93
94lemma sigma_is_empty : ∀prog,sigma.
95  sigma_is prog sigma empty_is = empty_is.
96#prog #sigma % qed.
97
98definition sigma_mem : ertl_program → lbl_funct →
99 bemem → bemem ≝
100 λprog,f_lbls,m.
101 mk_mem
102  (λb.
103    If Zltb (block_id b) (nextblock m) then with prf' do   
104      let l ≝ low_bound m b in
105      let h ≝ high_bound m b in
106      mk_block_contents l h
107      (λz.If Zleb l z ∧ Zltb z h then with prf'' do
108        sigma_beval prog f_lbls (contents (blocks m b) z)
109      else BVundef)
110    else empty_block OZ OZ)
111  (nextblock m)
112  (nextblock_pos m).
113
114include "common/ExtraIdentifiers.ma".
115
116
117definition sigma_register_env :
118ertl_program → lbl_funct →
119list register →
120register_env beval → register_env beval ≝
121λprog,f_lbls,ids,psd_env.
122let m' ≝  map ??? psd_env (λbv.sigma_beval prog f_lbls bv) in
123m' ∖ ids.
124
125
126definition sigma_frames_opt : ertl_program →
127lbl_funct → regs_funct →
128list (register_env beval × (Σb:block.block_region b=Code)) →
129option (list (register_env beval × (Σb:block.block_region b=Code))) ≝
130λprog,f_lbls,f_regs,frms.
131let globals ≝ prog_var_names … prog in
132let ge ≝ globalenv_noinit … prog in
133m_list_map ? ? ?
134(λx.let 〈reg_env,bl〉 ≝ x in
135    ! 〈id,fn〉 ← res_to_opt … (fetch_internal_function … ge bl);
136    return 〈sigma_register_env prog f_lbls
137                (added_registers ERTL globals fn (f_regs bl)) reg_env,bl〉) frms.
138               
139definition sigma_frames :   ertl_program →
140lbl_funct → regs_funct →
141option (list (register_env beval × (Σb:block.block_region b=Code))) →
142option (list (register_env beval × (Σb:block.block_region b=Code))) ≝
143λprog,f_lbls,f_regs,frms.
144! frames ← frms;
145sigma_frames_opt prog f_lbls f_regs frames.
146       
147include "common/BitVectorTrieMap.ma".
148
149definition sigma_hw_register_env :ertl_program →
150lbl_funct →  hw_register_env → hw_register_env ≝
151λprog,f_lbls,h_reg.mk_hw_register_env
152(map ? ? (sigma_beval prog f_lbls) 6 (reg_env … h_reg)) (other_bit … h_reg).
153
154definition sigma_regs :ertl_program →
155lbl_funct →  list register →
156(register_env beval)×hw_register_env→
157(register_env beval)×hw_register_env ≝
158λprog,f_lbls,ids,regs.let 〈x,y〉≝ regs in
159      〈sigma_register_env prog f_lbls ids x,
160       sigma_hw_register_env prog f_lbls y〉.
161
162definition dummy_state : state ERTL_semantics ≝
163mk_state ERTL_semantics
164   (None ?) empty_is BBundef 〈empty_map ? ?,mk_hw_register_env … (Stub …) BBundef〉 empty.
165
166definition sigma_state : ertl_program →
167lbl_funct → regs_funct → list register →
168state ERTLptr_semantics → state ERTL_semantics ≝
169λprog,f_lbls,f_regs,restr,st.
170mk_state ERTL_semantics
171  (sigma_frames prog f_lbls f_regs (st_frms ERTLptr_semantics st))
172  (sigma_is prog f_lbls (istack … st))
173  (carry … st)
174  (sigma_regs prog f_lbls restr (regs … st))
175  (sigma_mem prog f_lbls (m … st)).
176   
177definition dummy_state_pc : state_pc ERTL_semantics ≝
178mk_state_pc ? dummy_state (null_pc one) (null_pc one).
179
180definition sigma_state_pc : ertl_program → lbl_funct → regs_funct →
181state_pc ERTLptr_semantics → state_pc ERTL_semantics ≝
182λprog,f_lbls,f_regs,st.
183let ge ≝ globalenv_noinit … prog in
184let globals ≝ prog_var_names … prog in
185match fetch_internal_function … ge (pc_block (pc … st)) with
186  [ OK y ⇒ let 〈i,fn〉 ≝ y in
187           let added ≝ added_registers ERTL globals fn
188                                          (f_regs (pc_block (pc … st))) in
189           mk_state_pc ?
190           (sigma_state prog f_lbls f_regs added st)
191               (pc … st) (sigma_stored_pc prog f_lbls (last_pop … st))
192  | Error e ⇒ dummy_state_pc
193  ].
194
195
196lemma ps_reg_retrieve_ok :  ∀prog : ertl_program.
197∀f_lbls : lbl_funct. ∀r,restr.
198preserving1 ?? res_preserve1 …
199     (sigma_regs prog f_lbls restr)
200     (sigma_beval prog f_lbls)
201     (λregs.ps_reg_retrieve regs r)
202     (λregs.ps_reg_retrieve regs r).
203#prog #f_lbls #r #restr * #psd_r #hw_r whd in match ps_reg_retrieve;
204whd in match reg_retrieve; normalize nodelta @opt_to_res_preserve1
205whd in match sigma_regs; whd in match sigma_register_env; normalize nodelta
206>lookup_set_minus @if_elim [ #_ @opt_preserve_none1] #id_r_not_in
207>(lookup_map ?? RegisterTag ???) #bv #H @('bind_inversion H) -H #bv1
208#bv1_spec whd in ⊢ (??%? → ?); #EQ destruct %{bv1} % // >bv1_spec %
209qed.
210
211lemma hw_reg_retrieve_ok : ∀prog : ertl_program.
212∀f_lbls : lbl_funct. ∀r,restr.
213preserving1 ?? res_preserve1 …
214    (sigma_regs prog f_lbls restr)
215    (sigma_beval prog f_lbls)
216    (λregs.hw_reg_retrieve regs r)
217    (λregs.hw_reg_retrieve regs r).
218#prog #f_lbls #r #restr * #psd_r * #hw_r #b whd in match hw_reg_retrieve;
219whd in match hwreg_retrieve; normalize nodelta whd in match sigma_regs;
220whd in match sigma_hw_register_env; normalize nodelta
221change with (sigma_beval prog f_lbls BVundef) in ⊢ (???????(??(?????%))?);
222#bv >lookup_map whd in ⊢ (???% → ?); #EQ destruct
223%{(lookup beval 6 (bitvector_of_register r) hw_r BVundef)}
224% //
225qed.
226
227
228lemma ps_reg_store_ok : ∀prog : ertl_program.
229∀f_lbls : lbl_funct. ∀r,restr.
230¬(r ∈ (set_from_list RegisterTag restr)) →
231preserving21 ?? res_preserve1 …
232   (sigma_beval prog f_lbls)
233   (sigma_regs prog f_lbls restr)
234   (sigma_regs prog f_lbls restr)
235   (ps_reg_store r)
236   (ps_reg_store r).
237#prog #f_lbls #r #restr #Hreg whd in match ps_reg_store; normalize nodelta
238#bv * #psd_r #hw_r @mfr_return_eq1
239whd in match reg_store; whd in match sigma_regs; normalize nodelta
240whd in match sigma_register_env; normalize nodelta >map_add
241  >add_set_minus [% | assumption]
242qed.
243(* 
244   lapply(update_ok_to_lookup ?????? x_spec) * * #_ #EQpsd #_
245  lapply x_spec -x_spec lapply EQpsd -EQpsd whd in match sigma_register_env;
246  normalize nodelta >lookup_set_minus @if_elim [ #_ * #H @⊥ @H %]
247  #id_not_in #_ >update_set_minus [2: assumption] #H @('bind_inversion H) -H
248  #x0 >map_update_commute #H @('bind_inversion H) -H #x1 #x1_spec
249  whd in ⊢ (??%% → ??%% → ?); #EQ1 #EQ2 destruct %{x1} % //
250| #x * #psd_r' #hw_r' whd in match sigma_regs; normalize nodelta
251  whd in ⊢ (???% → ?); #EQ destruct %{〈x,hw_r〉} % //
252]
253qed.*)
254
255
256lemma hw_reg_store_ok : ∀prog : ertl_program.
257∀f_lbls : lbl_funct. ∀r,restr.
258preserving21 ?? res_preserve1 …
259   (sigma_beval prog f_lbls)
260   (sigma_regs prog f_lbls restr)
261   (sigma_regs prog f_lbls restr)
262   (hw_reg_store r)
263   (hw_reg_store r).
264#prog #sigma #r #restr whd in match hw_reg_store; normalize nodelta
265#bv * #psd_r * #hw_r #b whd in match hwreg_store; whd in match sigma_regs;
266normalize nodelta
267whd in match sigma_hw_register_env; normalize nodelta <insert_map * #psd_r'
268* #hw_r' #b' whd in ⊢ (???% → ?); #EQ destruct % [2: % [%] % |]
269qed.
270
271definition move_dst_not_fresh : list register →  move_dst → Prop ≝
272λrestr,mv.match mv with
273  [PSD r ⇒ bool_to_Prop (¬(r ∈ (set_from_list RegisterTag restr)))
274  | _ ⇒ True
275  ].
276
277lemma ertl_eval_move_ok : ∀prog : ertl_program.
278∀f_lbls : lbl_funct. ∀ restr,pm.
279move_dst_not_fresh restr (\fst pm) →
280preserving1 ?? res_preserve1 …
281     (sigma_regs prog f_lbls restr)
282     (sigma_regs prog f_lbls restr)
283     (λregs.ertl_eval_move regs pm)
284     (λregs.ertl_eval_move regs pm).
285#prog #sigma #restr * #mv_dst #arg_dst #Hpm #pm whd in match ertl_eval_move;
286normalize nodelta @mfr_bind1 [@(sigma_beval prog sigma)
287| cases arg_dst normalize nodelta
288  [2: #b change with (return sigma_beval prog sigma (BVByte b)) in ⊢ (???????%?);
289      @mfr_return1]
290  * #r normalize nodelta [@ps_reg_retrieve_ok| @hw_reg_retrieve_ok]
291| #bv cases mv_dst in Hpm; #r #Hpm normalize nodelta [@ps_reg_store_ok assumption
292                                                     | @hw_reg_store_ok
293                                                     ]
294]
295qed.
296
297lemma ps_arg_retrieve_ok : ∀prog : ertl_program.
298∀f_lbls : lbl_funct. ∀a,restr.
299preserving1 ?? res_preserve1 …
300    (sigma_regs prog f_lbls restr)
301    (sigma_beval prog f_lbls)
302    (λregs.ps_arg_retrieve regs a)
303    (λregs.ps_arg_retrieve regs a).
304#prog #sigma #a #restr whd in match ps_arg_retrieve; normalize nodelta cases a -a
305normalize nodelta [#r | #b ] #regs
306[ @ps_reg_retrieve_ok
307| change with (return sigma_beval prog sigma (BVByte b)) in ⊢ (???????%?);
308  @mfr_return1
309]
310qed.
311
312lemma pop_ok :
313∀prog : ertl_program.∀f_lbls : lbl_funct.
314∀f_regs : regs_funct.∀restr.
315preserving1 ?? res_preserve1 ????
316   (sigma_state prog f_lbls f_regs restr)
317   (λx.let 〈bv,st〉 ≝ x in
318      〈sigma_beval prog f_lbls bv,
319       sigma_state prog f_lbls f_regs restr st〉)
320   (pop ERTL_semantics)
321   (pop ERTLptr_semantics).
322#prog #f_lbls #f_regs #id whd in match pop; normalize nodelta #st @mfr_bind1
323[@(λx.let 〈bv,is〉 ≝ x in
324     〈sigma_beval prog f_lbls bv,
325      sigma_is prog f_lbls is 〉)
326| whd in match is_pop; normalize nodelta whd in match sigma_state;
327  normalize nodelta cases(istack ? st) normalize nodelta
328  [@res_preserve_error1
329  |2,3: #bv1 [2: #bv2] * #bv3 #is1 whd in ⊢ (??%% → ?); #EQ destruct
330        % [2,4: % [1,3: %|*: %] |*:]
331  ]
332| * #bv #is normalize nodelta @mfr_return_eq1 %   
333]
334qed.
335
336lemma push_ok :
337∀prog : ertl_program.
338∀f_lbls : lbl_funct.
339∀f_regs : regs_funct.∀restr.
340preserving21 ?? res_preserve1 …
341     (sigma_state prog f_lbls f_regs restr)
342     (sigma_beval prog f_lbls)
343     (sigma_state prog f_lbls f_regs restr)
344     (push ERTL_semantics)
345     (push ERTLptr_semantics).
346#prog #f_lbls #f_regs #restr whd in match push; normalize nodelta #st #bv @mfr_bind1
347[ @(sigma_is prog f_lbls)
348| whd in match is_push; normalize nodelta whd in match sigma_state; normalize nodelta
349 cases (istack ? st) [2,3: #bv [2: #bv']]  whd in match sigma_is in ⊢ (???????%?);
350 normalize nodelta [@res_preserve_error1] @mfr_return_eq1 %
351| #is @mfr_return_eq1 %
352]
353qed.
354
355lemma be_opaccs_ok :
356∀prog : ertl_program. ∀f_lbls : lbl_funct. ∀ op.
357preserving21 ?? res_preserve1 ??????
358    (sigma_beval prog f_lbls)
359    (sigma_beval prog f_lbls)
360    (λx.let 〈bv1,bv2〉 ≝ x in
361           〈sigma_beval prog f_lbls bv1,
362            sigma_beval prog f_lbls bv2〉)
363    (be_opaccs op)
364    (be_opaccs op).
365#prog #sigma #op #bv #bv1
366whd in match be_opaccs; normalize nodelta @mfr_bind1
367[ @(λx.x)
368| cases bv
369  [ | | #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc1 #p1]
370  whd in match Byte_of_val; normalize nodelta
371  try @res_preserve_error1 [ #x whd in ⊢ (???% → ?); #EQ destruct %{x} % //]
372  whd in match sigma_beval; normalize nodelta cases (sigma_pc_opt ? ? ?)
373  normalize nodelta [2: #pc] @res_preserve_error1
374| #by @mfr_bind1
375  [ @(λx.x)
376  | cases bv1
377    [ | | #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc1 #p1]
378    whd in match Byte_of_val; normalize nodelta
379    try @res_preserve_error1 [ #x whd in ⊢ (???% → ?); #EQ destruct %{x} % //]
380    whd in match sigma_beval; normalize nodelta cases (sigma_pc_opt ? ? ?)
381    normalize nodelta [2: #pc] @res_preserve_error1
382 | #by1 * #bv2 #bv3 cases(opaccs eval op by by1) #by' #by1' normalize nodelta
383   whd in ⊢ (??%% → ?); #EQ destruct % [2: % [%] % |]
384qed.
385
386lemma be_op1_ok : ∀prog : ertl_program.  ∀f_lbls : lbl_funct.
387∀ op.
388preserving1 ?? res_preserve1 …
389     (sigma_beval prog f_lbls)
390     (sigma_beval prog f_lbls)
391     (be_op1 op)
392     (be_op1 op).
393#prog #sigma #o #bv whd in match be_op1; normalize nodelta @mfr_bind1
394[ @(λx.x)
395| cases bv
396  [ | | #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc1 #p1]
397  whd in match Byte_of_val; whd in match sigma_beval; normalize nodelta
398  try @res_preserve_error1 [ @mfr_return_eq1 %]
399  cases(sigma_pc_opt prog sigma pc1) [2: #pc2] normalize nodelta
400  @res_preserve_error1
401| #by @mfr_return_eq1 %
402]
403qed.
404
405
406lemma be_op2_ok : ∀prog : ertl_program. ∀f_lbls : lbl_funct.
407∀ b,op.
408preserving21 ?? res_preserve1 …
409     (sigma_beval prog f_lbls)
410     (sigma_beval prog f_lbls)
411     (λx.let 〈bv,b〉≝ x in 〈sigma_beval prog f_lbls bv,b〉)
412     (be_op2 b op)
413     (be_op2 b op).
414#prog #sigma #b #op #bv #bv1 whd in match be_op2; normalize nodelta
415cases daemon
416qed. (*TODO*)
417(*cases bv
418[ | | #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc1 #p1]
419normalize nodelta [cases op normalize nodelta @res_preserve_error1] whd in match sigma_beval;
420normalize nodelta
421cases bv1
422[1,2,8,9,15,16,22,23,29,30,36,37:
423|3,10,17,24,31,38: #ptr1' #ptr2' #p'
424|4,11,18,25,32,39: #by'
425|5,12,19,26,33,40: #p'
426|6,13,20,27,34,41: #ptr' #p'
427|7,14,21,28,35,42: #pc1' #p1'
428]
429normalize nodelta try @res_preserve_error1
430[4,5,8,13,16,20,21,22,23,24,25,26 : @res_preserve_error11 %
431   [2,4,6,8,10,12,14,16,18,20,22,24: cases(sigma_pc_opt ???) try % #pc2 %
432   |*:]
433|*: cases op normalize nodelta
434    try @res_preserve_error1 try( @mfr_return_eq1 %)
435    [1,2,12,13,16,17,18: @if_elim #_ try @res_preserve_error1
436                         try( @mfr_return_eq1 %)
437                         [ @if_elim #_ @mfr_return_eq1 %
438                         | cases(ptype ptr) normalize nodelta
439                           [2: @res_preserve_error1] @mfr_bind1
440                           [ @(λx.x)
441                           | whd in match Bit_of_val; normalize nodelta
442                             cases b [#bo|| #bo #ptr'' #p'' #bit_v]
443                             normalize nodelta [2,3: @res_preserve_error1]
444                             @mfr_return_eq1 %
445                           | #bi cases(op2 ?????) #by #bi1 normalize nodelta
446                             @mfr_return_eq1 %
447                           ]
448                         | cases(ptype ptr) normalize nodelta @res_preserve_error1
449                         ]
450    |3,4,5,6,7,8: @mfr_bind1
451        [1,4,7,10,13,16: @(λx.x)
452        |2,5,8,11,14,17: whd in match Bit_of_val; normalize nodelta
453                         cases b [1,4,7,10,13,16: #bo|
454                                 |2,5,8,11,14,17:
455                                 |3,6,9,12,15,18: #bo #ptr'' #p'' #bit_v
456                                 ] normalize nodelta try @res_preserve_error1
457                                 @mfr_return_eq1 %
458       |3,6,9,12,15,18: #bi try(@mfr_return_eq1 %) cases(op2 ?????) #by #bi1 normalize nodelta
459                        @mfr_return_eq1 %
460       ]
461    |*: whd in match be_add_sub_byte; normalize nodelta
462        [1,2,3: cases(ptype ptr) normalize nodelta [2,4,6: @res_preserve_error1]
463                cases p * [2,4,6: #p_no] #prf normalize nodelta
464                [@res_preserve_error1
465                |2,3: cases b [1,4: #bo|2,5: |3,6:  #bo #ptr'' #p'' #bit_v]
466                      normalize nodelta [1,2,3,4: @res_preserve_error1]
467                      @if_elim #_ [2,4: @res_preserve_error1]
468                      @If_elim #INUTILE [2,4: @res_preserve_error1]
469                      @pair_elim #a1 #a2 #_ normalize nodelta
470                      @mfr_return_eq1 %
471                |*: @mfr_bind1
472                  [1,4,7: @(λx.x)
473                  |2,5,8: whd in match Bit_of_val; normalize nodelta
474                          [@mfr_return_eq1 %] cases b
475                          [1,4: #bo|2,5: |3,6:  #bo #ptr'' #p'' #bit_v]
476                          normalize nodelta [3,4,5,6: @res_preserve_error1]
477                          @mfr_return_eq1 %
478                  |3,6,9: * normalize nodelta [1,3,5: @res_preserve_error1]
479                          cases(op2 ?????) #a1 #a2 normalize nodelta
480                          @mfr_return_eq1 %
481                  ]
482               ]
483         |*: cases(ptype ptr') normalize nodelta [2,4: @res_preserve_error1]
484             cases p' * [2,4: #part_no] #prf normalize nodelta
485             [ @res_preserve_error1
486             | cases b [#bo|| #bo #ptr'' #p'' #bit_v]
487               normalize nodelta [1,2: @res_preserve_error1] @if_elim #_
488               [2: @res_preserve_error1] @If_elim #INUTILE [2: @res_preserve_error1]
489               @pair_elim #a1 #a2 #_ normalize nodelta @mfr_return_eq1 %
490             |*: @mfr_bind1
491                [1,4: @(λx.x)
492                |2,5: whd in match Bit_of_val; normalize nodelta [ @mfr_return_eq1 %]
493                      cases b [#bo|| #bo #ptr'' #p'' #bit_v] normalize nodelta
494                      [2,3: @res_preserve_error1] @mfr_return_eq1 %
495                |3,6: * normalize nodelta [1,3: @res_preserve_error1]   
496                      cases(op2 ?????) #a1 #a2 normalize nodelta
497                      @mfr_return_eq1 %
498                ]
499              ]
500          ]
501      ]
502]
503qed.*)
504
505lemma pointer_of_address_ok : ∀prog : ertl_program.∀f_lbls : lbl_funct.
506preserving1 … res_preserve1 …
507     (λx.let 〈bv1,bv2〉 ≝ x in〈sigma_beval prog f_lbls bv1,
508           sigma_beval prog f_lbls bv2〉)
509     (λx.x)
510     pointer_of_address pointer_of_address.
511#prog #sigma * #bv1 #bv2 whd in match pointer_of_address;
512whd in match pointer_of_bevals; normalize nodelta
513cases bv1 normalize nodelta
514[ | | #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc1 #p1]
515try @res_preserve_error1
516[ cases bv2 [ | | #ptr1' #ptr2' #p' | #by' | #p' | #ptr' #p' | #pc1' #p1']
517  normalize nodelta
518  [1,2,3,4,5: @res_preserve_error1
519  | @if_elim #_ [ @mfr_return_eq1 % | @res_preserve_error1]
520  ]
521] whd in match sigma_beval; normalize nodelta cases(sigma_pc_opt ???)
522  [2,4: #pc4] normalize nodelta @res_preserve_error1
523qed.
524
525lemma beloadv_ok : ∀prog : ertl_program. ∀f_lbls : lbl_funct.
526∀ptr.
527preserving1 … opt_preserve1 …
528     (sigma_mem prog f_lbls)
529     (sigma_beval prog f_lbls)
530     (λm.beloadv m ptr)
531     (λm.beloadv m ptr).
532#prog #sigma #ptr #mem whd in match beloadv; whd in match do_if_in_bounds;
533normalize nodelta @if_elim [2: #_ @opt_preserve_none1]
534whd in match sigma_mem in ⊢ (% → ?); normalize nodelta #Hzlb
535@if_elim [2: #_ @opt_preserve_none1] whd in match sigma_mem in ⊢ (% → ?);
536normalize nodelta @If_elim [2: >Hzlb * #H @⊥ @H %] #_ @andb_elim @if_elim
537[2: #_ *] #Hzleb #Hzlb' >Hzlb normalize nodelta >Hzlb' normalize nodelta
538@mfr_return_eq1 whd in match sigma_mem; normalize nodelta >Hzlb
539@If_elim [2: * #H @⊥ @H %] * >Hzleb >Hzlb' @If_elim [2: * #H @⊥ @H %]
540* %
541qed.
542
543lemma bestorev_ok : ∀prog : ertl_program.∀f_lbls : lbl_funct.
544∀ptr.
545preserving21 … opt_preserve1 …
546    (sigma_mem prog f_lbls)
547    (sigma_beval prog f_lbls)
548    (sigma_mem prog f_lbls)
549    (λm.bestorev m ptr)
550    (λm.bestorev m ptr).
551#prog #sigma #ptr #mem #bv whd in match bestorev; whd in match do_if_in_bounds;
552normalize nodelta @if_elim [2: #_ @opt_preserve_none1]
553whd in match sigma_mem in ⊢ (% → ?); normalize nodelta #Hzlb
554@if_elim [2: #_ @opt_preserve_none1] @andb_elim @if_elim [2: #_ *]
555whd in match sigma_mem in ⊢ (% → % → ?); normalize nodelta >Hzlb
556@If_elim [2: * #H @⊥ @H %] * #Hzleb #Hzlb' normalize nodelta >Hzleb
557>Hzlb' normalize nodelta @mfr_return_eq1 whd in ⊢ (???%); @eq_f @mem_ext_eq
558[ #bl normalize nodelta % [%]
559  [ whd in match sigma_mem; normalize nodelta >Hzlb @If_elim [2: * #H @⊥ @H %] *
560    whd in match update_block; normalize nodelta @if_elim
561    [ @eq_block_elim [2: #_ *] #EQbl * >EQbl >Hzlb @If_elim [2: * #H @⊥ @H %]
562      * whd in match low_bound; normalize nodelta @if_elim [ #_ %]
563      @eq_block_elim #_ * %
564    | @eq_block_elim [#_ *] * #Hbl * @If_elim
565      [ #Hzlb'' >Hzlb'' @If_elim [2: * #H @⊥ @H %] * whd in match low_bound;
566        normalize nodelta @if_elim [2: #_ %] @eq_block_elim [2: #_ *] #H @⊥ @Hbl
567        assumption
568      | #Hzlb'' >Hzlb'' @If_elim [*] #_ %
569      ]
570   ]
571 | whd in match update_block; whd in match sigma_mem; normalize nodelta
572   @if_elim @eq_block_elim [2,3: #_ * |4: *] #Hbl #_ @If_elim
573   [3,4: >Hbl >Hzlb * [2: #H @⊥ @H %] @If_elim [2: * #H @⊥ @H %] *
574        whd in match high_bound; normalize nodelta @if_elim [#_ %]
575        @eq_block_elim [ #_ *] * #H @⊥ @H %
576   | #Hzlb'' >Hzlb'' @If_elim [2: * #H @⊥ @H %] * whd in match high_bound;
577     normalize nodelta @if_elim [2: #_ %] @eq_block_elim [2: #_ *]
578     #H @⊥ @Hbl assumption
579  | #Hzlb'' >Hzlb'' @If_elim [*] #_ %
580  ]
581 | #z whd in match update_block; whd in match sigma_mem; normalize nodelta
582   @if_elim @eq_block_elim [2,3: #_ * |4: *] #Hbl #_
583   [ @If_elim #Hzlb'' >Hzlb'' [2: @If_elim * #_ %] @If_elim @andb_elim
584     @if_elim [2: #_ *] #Hzleb' #Hzlb'''
585     [ @If_elim [2: * #H @⊥ @H %] * whd in match low_bound; normalize nodelta
586       @If_elim @andb_elim @if_elim [2: #_ *] @if_elim
587       [1,3,5: @eq_block_elim [2,4,6: #_ *] #H @⊥ @Hbl assumption] #_ >Hzleb' *
588       whd in match high_bound; normalize nodelta @if_elim
589       [1,3: @eq_block_elim [2,4: #_ *] #H @⊥ @Hbl assumption] #_ >Hzlb'''
590       [ * %] * #H @⊥ @H %
591     | @If_elim * [2: #H @⊥ @H %] whd in match low_bound; normalize nodelta
592       @if_elim [@eq_block_elim [2: #_ *] #H @⊥ @Hbl assumption] #_
593       >Hzleb' whd in match high_bound; normalize nodelta @if_elim
594       [@eq_block_elim [2: #_ *] #H @⊥ @Hbl assumption] #_ >Hzlb'''
595       @If_elim [2: #_ %] *
596     | @If_elim [2: * #H @⊥ @H %] whd in match low_bound; normalize nodelta @if_elim
597       [@eq_block_elim [2: #_ *] #H @⊥ @Hbl assumption] #_ #_
598       whd in match low_bound in Hzleb'; normalize nodelta in Hzleb';
599       whd in match high_bound; normalize nodelta @if_elim
600       [@eq_block_elim [2: #_ *] #H @⊥ @Hbl assumption] #_ @If_elim [2: #_ %]
601       @andb_elim @if_elim [2: #_ *] #H >H in Hzleb'; *
602     ]
603   | whd in ⊢ (??%?); @if_elim @eqZb_elim [2,3: #_ * |4: *] #Hz *
604       [ >Hzlb @If_elim [2: * #H @⊥ @H %] * @If_elim @andb_elim @if_elim
605          [2: #_ *] #Hzleb' #Hzlb'' >Hbl >Hzlb @If_elim [2,4,6: * #H @⊥ @H %] #_
606          whd in match low_bound; normalize nodelta @eq_block_elim
607          [2,4,6: * #H @⊥ @H %] #_ normalize nodelta whd in match high_bound;
608          normalize nodelta @eq_block_elim [2,4,6: * #H @⊥ @H %]
609          #_ normalize nodelta
610          [1,2: >Hzleb' >Hzlb'' @If_elim [2,3: * #H @⊥ @H %]
611                #_ [2: %] whd in ⊢ (???(???%)); @if_elim [2: #_ %]
612                @eqZb_elim [2: #_ *] #H @⊥ @Hz assumption
613          | @If_elim [2: #_ %] @andb_elim @if_elim [2: #_ *] #H >H in Hzleb'; *
614          ]
615       | >Hbl >Hzlb @If_elim [2: * #H @⊥ @H %] * whd in match low_bound;
616         normalize nodelta @eq_block_elim [2: * #H @⊥ @H %] #_ normalize nodelta
617         whd in match high_bound; normalize nodelta @eq_block_elim [2: * #H @⊥ @H %]
618         normalize nodelta >Hz >Hzleb >Hzlb' @If_elim [2: * #H @⊥ @H %] #_ #_
619         whd in ⊢ (???(???%)); @eqZb_elim [2: * #H @⊥ @H %] #_ %
620       ]
621    ]
622 ]
623| %
624]
625qed.
626
627
628lemma sp_ok : ∀prog : ertl_program.
629∀f_lbls : lbl_funct.
630∀f_regs : regs_funct.∀restr.
631   preserving1 … res_preserve1 …
632      (λst.sigma_state prog f_lbls f_regs restr st)
633      (λx.x)
634      (sp ERTL_semantics)
635      (sp ERTLptr_semantics).
636#prog #f_lbls #f_regs #restr #st whd in match sp; normalize nodelta
637whd in match (load_sp ??); whd in match (load_sp ??); whd in match sigma_state;
638normalize nodelta whd in match sigma_regs; normalize nodelta
639cases(regs ? st) #psd_r #hw_r normalize nodelta
640inversion(pointer_of_address ?) normalize nodelta [2: #e #_ @res_preserve_error1]
641#pt #EQ lapply(jmeq_to_eq ??? EQ) -EQ whd in match hwreg_retrieve; normalize nodelta
642whd in match sigma_hw_register_env; normalize nodelta
643change with (sigma_beval prog f_lbls BVundef) in ⊢ (??(?(???(?????%)(?????%)))? → ?);
644>lookup_map >lookup_map
645cases(lookup beval 6 (bitvector_of_register RegisterSPL) (reg_env hw_r) BVundef)
646[ | | #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc1 #p1]
647whd in match pointer_of_address; whd in match pointer_of_bevals; normalize nodelta
648[1,2,3,4,5: #ABS destruct
649| cases(lookup beval 6 (bitvector_of_register RegisterSPH) (reg_env hw_r) BVundef)
650  [ | | #ptr1' #ptr2' #p' | #by' | #p' | #ptr' #p' | #pc1' #p1']
651  whd in match sigma_beval; normalize nodelta
652  [1,2,3,4,5: #ABS destruct
653  | @if_elim [2: #_ #ABS destruct] #H whd in ⊢ (??%? → ?); #EQ destruct
654    normalize nodelta @match_reg_elim #INUTILE
655    [ @mfr_return_eq1 % | @res_preserve_error1 ]
656  | cases (sigma_pc_opt ? ? ?) normalize nodelta [2: #x] #EQ destruct
657  ]
658| whd in match sigma_beval; normalize nodelta cases(sigma_pc_opt ? ? ?)
659 normalize nodelta [2: #x] #EQ destruct
660]
661qed.
662
663lemma set_sp_ok :  ∀prog : ertl_program.
664∀f_lbls : lbl_funct.
665∀f_regs : regs_funct.∀restr.∀ptr,st.
666set_sp ? ptr (sigma_state prog f_lbls f_regs restr st) =
667sigma_state prog f_lbls f_regs restr (set_sp ? ptr st).
668#prog #f_lbls #f_regs #restr #ptr #st whd in match set_sp; whd in match sigma_state;
669normalize nodelta @eq_f2 [2: %] whd in match (save_sp ???);
670whd in match (save_sp ???); whd in match sigma_regs; normalize nodelta
671cases(regs ? st) #psd_env #hw_regs normalize nodelta @eq_f
672whd in match hwreg_store_sp; normalize nodelta whd in match sigma_hw_register_env;
673normalize nodelta whd in match hwreg_store; normalize nodelta @eq_f2 [2: %]
674>insert_map @eq_f >insert_map %
675qed.
676
677(*TO BE MOVED IN TranslateUtils.ma *)
678include "utilities/listb_extra.ma".
679lemma not_in_added_registers : ∀p : graph_params.
680∀globals : list ident.∀fn,f_regs,r.
681(∀lbl. code_has_label p globals (joint_if_code … fn) lbl →
682       ¬(bool_to_Prop (r ∈ (f_regs lbl)))) →
683¬ (r ∈ (set_from_list RegisterTag (added_registers p globals fn f_regs))).
684#p #globals #fn #f_regs #r #H whd in match added_registers; normalize nodelta
685@foldi_ind [@I] #lbl #labels_fn #stmt #regs * #lbl_not_in_fn #EQstmt #IH
686lapply(Prop_notb … IH) -IH * #IH
687lapply(H lbl ?)
688 [whd in match code_has_label; whd in match code_has_point; normalize nodelta
689  whd in match (stmt_at ????); >EQstmt @I]
690* #H1 @notb_elim @if_elim [2: #_ @I] #ABS
691lapply(mem_list_as_set … ABS) #ABS' cases(Exists_append … ABS') #ABS''
692[ @H1 @Exists_memb lapply ABS'' elim (f_regs lbl) [ *] #hd #tl #IH whd in ⊢ (% → %);
693  * [ #EQ >EQ % %] #H %2 @IH @H
694| @IH @list_as_set_mem assumption
695]
696qed.
697
698lemma Exists_append1 : ∀A.∀l1,l2 : list A.∀a : A.In A l1 a → In A (l1@l2) a.
699#A #l1 elim l1 [#l2 #a *] #hd #tl #IH *
700[#a normalize * [#H % assumption | #H %2 >append_nil assumption]]
701#hd1 #tl1 #a normalize * [#H % assumption | #H %2 @IH assumption]
702qed.
703
704lemma Exists_append2 : ∀A.∀l1,l2 : list A.∀a : A.In A l2 a → In A (l1@l2) a.
705#A #l1 #l2 lapply l1 -l1 elim l2 [#l1 #a *] #hd #tl #IH *
706[#a normalize * [#H %1 assumption| #H %2 assumption]]
707#hd1 #tl1 #a normalize *
708[ #H %2 >append_cons @Exists_append1 >H elim tl1 [% %] #hd2 #tl2 #H1 normalize %2 //
709| #H %2 >append_cons @IH assumption]
710qed.
711
712lemma append_All : ∀A : Type[0]. ∀ P : A → Prop. ∀l1,l2 : list A.
713All ? P (l1 @ l2) → All ? P l1 ∧ All ? P l2.
714#A #P #l1 elim l1
715[ #l2 change with l2 in ⊢ (???% → ?); #H % //]
716#a #tl #IH #l2 change with (P a ∧ All A P (tl @ l2)) in ⊢ (% → ?);
717* #H1 #H2 lapply(IH … H2) * #H3 #H4 % // whd % //
718qed.
719
720include alias "common/PositiveMap.ma".
721
722lemma added_register_pm : ∀A,B. ∀m : positive_map A.
723∀f : Pos → list B.∀b.
724let added ≝ fold A (list B) (λp.λ_.λacc.(f p)@acc) m [ ] in
725All B (λx.x≠b) added →
726(∀i. lookup_opt unit i (domain_of_pm A m) ≠ None ? → All B (λx.x≠b) (f i)).
727#A #B #m #f #b normalize nodelta @pm_fold_ind
728[ #_ #i normalize * #H @⊥ @H %
729| #p #ps #a #lst #H #H1 #H2 #H3 #i cases(decidable_eq_pos i p)
730  [1,3: #EQ destruct(EQ) #_ cases(append_All … H3) //
731  |*: #Hi >lookup_opt_insert_miss [2,4: assumption] @H2
732      cases(append_All … H3) //
733  ]
734]
735qed.
736
737lemma decidable_In : ∀A.∀l : list A. ∀a : A. (∀a'.decidable (a = a')) → 
738decidable (In A l a).
739#A #l elim l [ #a #_ %2 % *] #hd #tl #IH #a #DEC cases(IH a DEC)
740[ #H % %2 assumption | * #H cases (DEC hd)
741[ #H1 %1 %1 assumption | * #H1 %2 % * [ #H2 @H1 assumption | #H2 @H assumption]]
742qed.
743
744lemma In_all : ∀A.∀l : list A. ∀ a : A.¬In A l a → All A (λx.x≠a) l.
745#A #l elim l [ #a #_ @I] #hd #tl #IH #a * #H % [2: @IH % #H1 @H %2 assumption]
746% #H1 @H % >H1 %
747qed.
748
749lemma All_In : ∀A.∀l : list A. ∀ a : A.All A (λx.x≠a) l → ¬In A l a.
750#A #l elim l [#a #_ % *] #hd #tl #IH #a ** #H1 #H2 % *
751[ #H3 @H1 >H3 % | cases(IH a H2) #H3 #H4 @H3 assumption]
752qed.
753
754lemma added_register_aux : ∀tag,A,B.∀m : identifier_map tag A.
755∀f : identifier tag → list B.(∀b,b' : B.decidable (b=b')) →
756let added ≝ foldi A (list B) tag (λl.λ_.λacc. (f l)@acc) m [ ] in
757∀i,a,b.lookup tag A m i = Some ? a → In B (f i) b → In B added b.
758#tag #A #B * #m #f #DEC * #i #a #b whd in ⊢ (??%? → ?); normalize nodelta
759#H #H1
760cases(decidable_In ? (foldi A (list B) tag
761            (λl.λ_.λacc.(f l)@acc)
762              (an_id_map tag A m) []) b (DEC b)) [//]
763#H3 @⊥ lapply(In_all ??? H3) -H3 #H3
764lapply(added_register_pm ?? m ?? H3 i ?)
765[cases(domain_of_pm_present ? m i) #H4 #_ @H4 >H % #EQ destruct]
766lapply H1 elim (f ?) [*] #hd #tl #IH * [#EQ * >EQ * #H4 #_ @H4 %]
767#H4 * #_ @IH assumption
768qed.
769
770lemma in_added_registers : ∀p : graph_params.
771∀globals : list ident.∀fn,f_regs,r.
772∀lbl.code_has_label p globals (joint_if_code … fn) lbl →
773 In ? (f_regs lbl) r →
774In ? (added_registers p globals fn f_regs) r.
775#p #globals #fn #f_regs #r #lbl whd in match code_has_label;
776whd in match code_has_point; normalize nodelta whd in match (stmt_at ????);
777inversion(lookup LabelTag ???) [ #_ *] #stmt #EQstmt #_
778#H @(added_register_aux …  EQstmt H)
779* #p * #p' cases(decidable_eq_pos p p') [ #EQ destruct % % | * #H1 %2 % #EQ destruct @H1 %]
780qed.
781
782
783include alias "basics/lists/listb.ma".
784
785(*
786definition get_internal_function_from_ident :
787∀ p: sem_params. ∀ globals : list ident . ∀ge : genv_t (joint_function p globals).
788ident → option (joint_closed_internal_function p globals) ≝
789λp,globals,ge,id.
790! bl  ← (find_symbol (joint_function p globals) ge id);
791! bl' ← (code_block_of_block bl);
792! 〈f,fn〉 ← res_to_opt … (fetch_internal_function ? ge bl');
793return fn.
794
795lemma get_internal_function_from_ident_ok :
796∀p : sem_params. ∀globals : list ident. ∀ge : genv_t (joint_function p globals).
797∀bl,f,fn. fetch_internal_function ? ge bl = return 〈f,fn〉 →
798get_internal_function_from_ident p globals ge f= return fn.
799#p #globals #ge #bl #f #fn #EQf
800@('bind_inversion EQf) * #f1 * #fn1 whd in match fetch_function;
801normalize nodelta #H lapply(opt_eq_from_res ???? H) -H #H @('bind_inversion H) -H
802#f2 #EQf2 #H @('bind_inversion H) -H #fn2 #EQfn2 whd in ⊢ (??%% → ??%% → ?);
803#EQ1 #EQ2 destruct whd in match get_internal_function_from_ident; normalize nodelta
804>(symbol_of_block_rev … EQf2) >m_return_bind
805cut(code_block_of_block bl = return bl)
806 [ whd in match code_block_of_block; normalize nodelta @match_reg_elim
807   [ >(pi2 ?? bl) #ABS destruct] elim bl #bl1 #EQ #prf % ] #EQbl >EQbl
808>m_return_bind >EQf %
809qed.
810*)
811
812lemma eval_seq_no_pc_no_call_ok :
813∀prog : ertl_program.
814let trans_prog ≝ ertl_to_ertlptr prog in
815∀f_lbls : lbl_funct. ∀f_regs : regs_funct.
816∀stack_size.
817∀bl.∀id.
818∀fn : joint_closed_internal_function ERTL (prog_var_names … prog).∀seq.
819(∀l. code_has_label … (joint_if_code … fn) l → 
820(All … (λreg.bool_to_Prop(¬(reg ∈ (f_regs bl l))))
821       (get_used_registers_from_seq … (functs … ERTL) seq)))  →
822   preserving1 ?? res_preserve1 ????
823      (sigma_state prog f_lbls f_regs (added_registers … fn (f_regs bl)))
824      (sigma_state prog f_lbls f_regs (added_registers … fn (f_regs bl)))
825      (eval_seq_no_pc ERTL_semantics
826             (globals (mk_prog_params ERTL_semantics prog stack_size))
827             (ev_genv (mk_prog_params ERTL_semantics prog stack_size)) id seq)
828      (eval_seq_no_pc ERTLptr_semantics
829             (globals (mk_prog_params ERTLptr_semantics trans_prog stack_size))
830             (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_size))
831             id (seq_embed … seq)).
832#prog #f_lbls #f_regs #stack_size #bl #f #fn #seq #fresh_regs
833cases seq in fresh_regs;
834[ #c #_ #st @mfr_return1
835| #pm #fesh_regs #st whd in match pair_reg_move; normalize nodelta
836  @mfr_bind1
837  [ 2: change with (ertl_eval_move ??) in ⊢ (???????%%); @ertl_eval_move_ok
838       whd in match move_dst_not_fresh; normalize nodelta cases pm in fesh_regs;
839       * [#r1 | #R1] #m_src [2: #_ @I] normalize nodelta #fresh_regs
840       @not_in_added_registers #lbl #Hlbl lapply(fresh_regs lbl Hlbl)
841       whd in ⊢ (% → %); * #H #_ @Prop_notb @H
842  | | #regs  @mfr_return_eq1 %
843  ]
844| #r #fresh_regs #st @mfr_bind1
845  [2:  @pop_ok |
846  | * #bv #st whd in match acca_store; normalize nodelta @mfr_bind1
847    [2: @ps_reg_store_ok       
848        @not_in_added_registers #lbl #Hlbl lapply(fresh_regs lbl Hlbl)
849       whd in ⊢ (% → %); * #H #_ @Prop_notb @H
850    ]
851  ]
852| #r #_ #st @mfr_bind1
853  [2: whd in match acca_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok |
854  | #bv @push_ok
855  ]
856| #i
857  #i_spec
858  change with ((dpl_reg ERTL) → ?)
859  #dpl
860  change with ((dph_reg ERTL) → ?)
861  #dph #fresh_regs #st @mfr_bind1
862  [ @(sigma_state prog f_lbls f_regs (added_registers … fn (f_regs bl)))
863  | whd in match dpl_store; normalize nodelta @mfr_bind1
864    [2: @opt_safe_elim #bl #EQbl
865       @opt_safe_elim #bl'
866       >(find_symbol_transf …
867          (λvars.transf_fundef … (λfn.(b_graph_translate … fn))) prog i) in ⊢ (%→?);
868       >EQbl #EQ destruct whd in match sigma_state; normalize nodelta       
869       change with (sigma_beval prog f_lbls (BVptr …))
870                                               in ⊢ (???????(?????%?)?);
871       @ps_reg_store_ok
872              @not_in_added_registers #lbl #Hlbl lapply(fresh_regs lbl Hlbl)
873       whd in ⊢ (% → %); * #H #_ @Prop_notb @H |
874    | #regs  @mfr_return_eq1 %
875    ]
876  | #st1 @opt_safe_elim #bl #EQbl @opt_safe_elim #bl'   
877   >(find_symbol_transf …
878          (λvars.transf_fundef … (λfn.(b_graph_translate … fn))) prog i) in ⊢ (%→?);
879    >EQbl #EQ destruct whd in match dph_store; normalize nodelta @mfr_bind1
880    [2: whd in match sigma_state; normalize nodelta       
881       change with (sigma_beval prog f_lbls (BVptr …))
882                                               in ⊢ (???????(?????%?)?);
883      @ps_reg_store_ok @not_in_added_registers #lbl #Hlbl lapply(fresh_regs lbl Hlbl)
884       whd in ⊢ (% → %); * #_ * #H #_ @Prop_notb @H |
885    | #regs  @mfr_return_eq1 %
886    ]
887  ]     
888| #op #a #b #arg1 #arg2 #fresh_regs #st @mfr_bind1
889  [2: whd in match acca_arg_retrieve; whd in match sigma_state; normalize nodelta
890     @ps_arg_retrieve_ok |
891  | #bv1 @mfr_bind1
892   [2: whd in match accb_arg_retrieve; whd in match sigma_state; normalize nodelta
893      @ps_arg_retrieve_ok |
894   | #bv2 @mfr_bind1
895     [2: @be_opaccs_ok |
896     | * #bv3 #bv4 normalize nodelta @mfr_bind1
897       [ @(sigma_state prog f_lbls f_regs (added_registers … fn (f_regs bl)))
898       | whd in match acca_store; normalize nodelta @mfr_bind1
899         [2: @ps_reg_store_ok @not_in_added_registers #lbl #Hlbl
900             lapply(fresh_regs lbl Hlbl) whd in ⊢ (% → %); * #H #_ @Prop_notb @H |
901         | #regs  @mfr_return_eq1 %
902         ]
903       | #st1 whd in match accb_store; normalize nodelta @mfr_bind1
904         [2: whd in match sigma_state; normalize nodelta
905            @ps_reg_store_ok @not_in_added_registers #lbl #Hlbl
906            lapply(fresh_regs lbl Hlbl) whd in ⊢ (% → %); * #_ * #H #_ @Prop_notb @H |
907         | #regs  @mfr_return_eq1 %
908         ]         
909       ]
910     ]
911   ]
912  ] 
913| #op #r1 #r2 #fresh_regs #st @mfr_bind1
914  [ @(sigma_beval prog f_lbls)
915  | whd in match acca_retrieve; normalize nodelta @ps_reg_retrieve_ok
916  | #bv1 @mfr_bind1
917    [ @(sigma_beval prog f_lbls)
918    | @be_op1_ok
919    | #bv2 whd in match acca_store; normalize nodelta @mfr_bind1
920      [2: whd in match sigma_state; normalize nodelta @ps_reg_store_ok
921          @not_in_added_registers #lbl #Hlbl lapply(fresh_regs lbl Hlbl)
922       whd in ⊢ (% → %); * #H #_ @Prop_notb @H |
923      | #regs  @mfr_return_eq1 %
924      ]
925    ]
926  ]
927| #op2 #r1 #r2 #arg #fresh_regs #st @mfr_bind1
928  [2: whd in match acca_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok |
929  | #bv @mfr_bind1
930    [2: whd in match snd_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok |
931    | #bv1 @mfr_bind1
932      [2: @be_op2_ok |
933      | * #bv2 #b @mfr_bind1
934        [ @(sigma_state prog f_lbls f_regs (added_registers … fn (f_regs bl)))
935        | whd in match acca_store; normalize nodelta @mfr_bind1
936          [2: whd in match sigma_state; normalize nodelta @ps_reg_store_ok
937              @not_in_added_registers #lbl #Hlbl lapply(fresh_regs lbl Hlbl)
938              whd in ⊢ (% → %); * #H #_ @Prop_notb @H |
939          | #regs  @mfr_return_eq1 %
940          ]
941        | #st1 @mfr_return_eq1 %
942        ]
943      ]
944    ]
945  ]
946| #_ #st @mfr_return_eq1 %
947| #_ #st @mfr_return_eq1 %
948| #r1 #dpl #dph #fresh_regs #st @mfr_bind1
949  [2: whd in match dph_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok |
950  | #bv @mfr_bind1
951    [2: whd in match dpl_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok |
952    | #bv1 @mfr_bind1
953      [ @(λx.x)
954      | @(pointer_of_address_ok ? ? 〈bv1,bv〉)
955      | #ptr @mfr_bind1
956        [2: @opt_to_res_preserve1 @beloadv_ok |
957        | #bv2 whd in match acca_store; normalize nodelta @mfr_bind1
958          [2: whd in match sigma_state; normalize nodelta @ps_reg_store_ok
959          @not_in_added_registers #lbl #Hlbl lapply(fresh_regs lbl Hlbl)
960          whd in ⊢ (% → %); * #H #_ @Prop_notb @H |
961          | #regs  @mfr_return_eq1 %
962          ]
963        ] 
964      ]
965    ]
966  ] 
967| #dpl #dph #r #_ #st @mfr_bind1
968  [2: whd in match dph_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok |
969  | #bv @mfr_bind1
970    [2: whd in match dpl_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok |
971    | #bv1 @mfr_bind1
972      [ @(λx.x)
973      |  @(pointer_of_address_ok ? ? 〈bv1,bv〉)
974      | #ptr @mfr_bind1
975        [2: whd in match acca_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok |
976        | #bv2 @mfr_bind1
977          [2: @opt_to_res_preserve1 @bestorev_ok |
978          | #m @mfr_return_eq1 %
979          ]
980        ]
981      ]
982    ]
983  ]
984| #ext #fresh_regs #st whd in ⊢ (???????%%); whd in match (stack_sizes ????); cases (stack_size f)
985  normalize nodelta
986  [ @res_preserve_error1
987  | #n cases ext in fresh_regs; normalize nodelta
988    [1,2: #_ @mfr_bind1
989      [1,4: @(λx.x)
990      |2,5: @sp_ok
991      |3,6: #ptr @mfr_return_eq1 >set_sp_ok %
992      ]
993    | #r #fresh_regs whd in match ps_reg_store_status; normalize nodelta @mfr_bind1
994      [2: whd in match sigma_state; normalize nodelta
995          change with (sigma_beval prog f_lbls (BVByte ?))
996               in ⊢ (???????(??%?)?);
997          @ps_reg_store_ok  @not_in_added_registers #lbl #Hlbl
998          lapply(fresh_regs lbl Hlbl) whd in ⊢ (% → %); * #H #_ @Prop_notb @H |
999      | #regs @mfr_return_eq1 %
1000      ]
1001    ]
1002  ]     
1003]
1004#regs @mfr_return_eq1 %
1005qed.
1006
1007lemma partial_inj_sigma : ∀ prog : ertl_program.
1008∀f_lbls : lbl_funct.
1009let sigma ≝ get_sigma prog f_lbls in
1010∀id,lbl1,lbl2. sigma id lbl1 ≠ None ? → sigma id lbl1 = sigma id lbl2 → lbl1 = lbl2.
1011#prog #good #bl #lbl1 #lbl2 inversion(get_sigma … lbl1)
1012[#_ * #H @⊥ @H %] #lbl1' whd in match get_sigma; normalize nodelta
1013#H @('bind_inversion H) -H #bl' whd in match code_block_of_block; normalize nodelta
1014@match_reg_elim [#_ #ABS destruct] #prf #EQ destruct #H @('bind_inversion H) -H
1015* #id #fn #H lapply(res_eq_from_opt ??? H) -H #EQfn #H @('bind_inversion H) -H
1016* #lbl1'' #stmt1 #H1 whd in ⊢ (??%? → ?); #EQ destruct
1017#_ #H lapply(sym_eq ??? H) -H >m_return_bind >EQfn >m_return_bind
1018#H @('bind_inversion H) -H * #lbl2' #stmt2 #H2
1019whd in ⊢ (??%? → ?); #EQ destruct lapply(find_predicate ?????? H1)
1020lapply(find_predicate ?????? H2) cases(good ??) normalize nodelta
1021  [ normalize nodelta @eq_identifier_elim #EQ1 *
1022    @eq_identifier_elim #EQ2 * >EQ1 >EQ2 %
1023  | #lb #tl whd in match split_on_last; normalize nodelta whd in match (foldr ?????);
1024    cases( foldr label (option (list label×label)) … tl) normalize nodelta
1025    [2: * #x #lb1] @eq_identifier_elim #EQ1 * @eq_identifier_elim #EQ2 *
1026    >EQ1 >EQ2 %
1027  ]
1028qed.
1029
1030
1031(*TO BE MOVED : GENERAL!!!*)
1032lemma pc_of_label_eq :
1033  ∀p,p'.let pars ≝ mk_sem_graph_params p p' in
1034  ∀globals,ge,bl,i_fn,lbl.
1035  fetch_internal_function ? ge bl = return i_fn →
1036  pc_of_label pars globals ge bl lbl =
1037    OK ? (pc_of_point ERTL_semantics bl lbl).
1038#p #p' #globals #ge #bl #i_fn #lbl #EQf
1039whd in match pc_of_label;
1040normalize nodelta >EQf >m_return_bind %
1041qed.
1042
1043lemma pop_ra_ok :
1044∀prog : ertl_program.
1045∀f_lbls : lbl_funct. ∀f_regs : regs_funct.
1046∀restr.
1047preserving1 … res_preserve1 …
1048     (sigma_state prog f_lbls f_regs restr)
1049     (λx.let 〈st,pc〉 ≝ x in
1050       〈sigma_state prog f_lbls f_regs restr st,
1051        sigma_stored_pc prog f_lbls pc〉)
1052     (pop_ra ERTL_semantics)
1053     (pop_ra ERTLptr_semantics).
1054cases daemon (*TODO*) qed.
1055(*       
1056#prog #f_lbls #f_regs #restr1 #st whd in match pop_ra; normalize nodelta
1057@mfr_bind1
1058[ | @pop_ok ] * #bv #st1 @mfr_bind1 [ | @pop_ok] * #bv1 #st2 @mfr_bind1
1059[ @(sigma_stored_pc prog f_lbls)
1060| whd in match pc_of_bevals; normalize nodelta
1061  cases bv [ | | #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc #p]
1062  whd in match sigma_beval; normalize nodelta try @res_preserve_error1
1063  inversion(sigma_pc_opt ? ? ?) normalize nodelta [ #_ @res_preserve_error1]
1064  #sigma_pc #sigma_pc_spec normalize nodelta cases bv1
1065  [ | | #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc1 #p1]
1066  normalize nodelta try @res_preserve_error1
1067  inversion(sigma_pc_opt ? ? ?) normalize nodelta [#_ @res_preserve_error1]
1068  #sigma_pc1 #sigma_pc1_spec @if_elim [2: #_ @res_preserve_error1]
1069  @andb_elim @if_elim [2: #_ *] @andb_elim @if_elim [2: #_ *]
1070  #_ #H >H @eq_program_counter_elim [2: #_ *]
1071  #EQspc * @eq_program_counter_elim
1072  [#_ normalize nodelta @mfr_return_eq1 whd in match sigma_stored_pc; normalize nodelta
1073   >sigma_pc1_spec %] * #H1 @⊥ @H1 >EQspc in sigma_pc_spec; <sigma_pc1_spec
1074   whd in match sigma_pc_opt; normalize nodelta @if_elim
1075  [ #H2 #EQ lapply(sym_eq ??? EQ) -EQ @if_elim [#_  whd in ⊢ (??%% → ?); #EQ destruct %]
1076    #H3 #H @('bind_inversion H) -H #x #H4 whd in ⊢ (??%? → ?); #EQ destruct >H2 in H3; *
1077  | #H2 @if_elim
1078    [ #H3 #H @('bind_inversion H) -H #x1 #_ whd in match pc_of_point; normalize nodelta
1079      whd in ⊢ (??%? → ?); #EQ destruct >H3 in H2; *
1080    | #H3 lapply sigma_pc1_spec; whd in match sigma_pc_opt; normalize nodelta @if_elim
1081     [#H >H in H3; *] #_ #EQ >EQ @('bind_inversion EQ) -EQ * #x cases pc1 #bl1 #pos1
1082     whd in match (point_of_pc ??); #x_spec whd in match (pc_of_point ???);
1083     whd in match (offset_of_point ??); whd in ⊢ (??%? → ?); #EQ destruct
1084     #H @('bind_inversion H) -H * #lbl cases pc #bl #pos whd in match (point_of_pc ??);
1085     #lbl_spec whd in match pc_of_point; normalize nodelta
1086     whd in match (offset_of_point ??); whd in ⊢ (??%? → ?); #EQ destruct
1087     @eq_f cut(an_identifier LabelTag pos = an_identifier LabelTag pos1 → pos = pos1)
1088     [ #EQ destruct %] #APP @APP @(partial_inj_sigma prog f_lbls bl1 …)
1089     [ >lbl_spec % #EQ destruct] >x_spec >lbl_spec %
1090    ]
1091  ]
1092| #pc @mfr_return_eq1 %
1093]
1094qed.*)
1095
1096lemma pc_block_eq : ∀prog : ertl_program. ∀f_lbls,pc.
1097sigma_pc_opt prog f_lbls pc ≠ None ? →
1098 pc_block … pc = pc_block … (sigma_stored_pc prog f_lbls pc).
1099#prog #sigma * #bl #pos whd in match sigma_stored_pc; normalize nodelta
1100inversion(sigma_pc_opt ???) [ #_ * #H @⊥ @H %] #pc
1101whd in match sigma_pc_opt; normalize nodelta @if_elim
1102[#_ whd in ⊢ (??%? → ?); #EQ destruct #_ %] #_
1103#H @('bind_inversion H) -H * #lbl #_
1104 whd in ⊢ (??%? → ?); #EQ destruct
1105#_ %
1106qed.
1107
1108include "joint/extra_joint_semantics.ma".
1109
1110lemma pop_frame_ok : ∀prog : ertl_program.
1111let trans_prog ≝ ertl_to_ertlptr prog in
1112∀f_lbls : lbl_funct. ∀f_regs : regs_funct.
1113∀restr.
1114preserving1 ?? res_preserve1 ????
1115       (sigma_state prog f_lbls f_regs restr)
1116       (λx.let 〈st,pc〉 ≝ x in
1117           match fetch_internal_function ? (globalenv_noinit … prog)
1118                 (pc_block pc) with
1119                  [ OK y ⇒ let 〈id,f〉 ≝ y in
1120                           〈sigma_state prog f_lbls f_regs
1121                                 (added_registers ERTL (prog_var_names … prog) f
1122                             (f_regs (pc_block pc))) st,
1123                            sigma_stored_pc prog f_lbls pc〉
1124                  | Error e ⇒ 〈dummy_state,null_pc one〉
1125                  ])
1126       (ertl_pop_frame)
1127       (ertl_pop_frame).
1128#prog #f_lbls #f_regs #restr #st whd in match ertl_pop_frame; normalize nodelta
1129@mfr_bind1
1130[ @(λx.match sigma_frames_opt prog f_lbls f_regs x with [Some l ⇒ l | None ⇒ [ ]])
1131| @opt_to_res_preserve1 whd in match sigma_state; normalize nodelta
1132  cases(st_frms … st) [@opt_preserve_none1] #l whd in match sigma_frames;
1133  normalize  nodelta >m_return_bind #x #x_spec %{l} % [%] >x_spec %
1134| * normalize nodelta [@res_preserve_error1] * #loc_mem #bl #tl normalize nodelta
1135  inversion(sigma_frames_opt ????) normalize nodelta [ #_ @res_preserve_error1]
1136  #l whd in match sigma_frames_opt; whd in match m_list_map; normalize nodelta
1137  whd in match (foldr ?????); normalize nodelta inversion(fetch_internal_function ???)
1138  normalize nodelta [2: #e #_ #ABS destruct(ABS)] * #f #fn #EQfn
1139  #H @('bind_inversion H) -H #l1
1140  change with (sigma_frames_opt prog f_lbls f_regs tl = ? → ?) #EQl1
1141  whd in ⊢ (??%? → ?); #EQ destruct(EQ) @mfr_bind1
1142  [2: whd in match sigma_state; whd in match set_regs; whd in match set_frms;
1143     normalize nodelta
1144     cut( 〈sigma_register_env prog f_lbls
1145     (added_registers ERTL (prog_var_names (joint_function ERTL) ℕ prog) fn
1146      (f_regs bl))
1147     loc_mem,
1148    \snd  (sigma_regs prog f_lbls restr (regs ERTLptr_semantics st))〉 =
1149    sigma_regs prog f_lbls 
1150     (added_registers ERTL (prog_var_names (joint_function ERTL) ℕ prog) fn
1151      (f_regs bl)) (〈loc_mem,\snd  (regs ERTL_state st)〉)) [
1152      whd in match sigma_regs; normalize nodelta cases(regs … st) #x1 #x2
1153      %] #EQ >EQ -EQ <EQl1 in ⊢ (???????%?);
1154      change with (sigma_state prog f_lbls f_regs
1155    (added_registers ERTL (prog_var_names … prog) fn (f_regs bl))
1156      (mk_state ? (Some ? tl) (istack … st) (carry … st) (〈loc_mem,\snd (regs … st)〉)
1157      (m … st))) in ⊢ (???????(??%)?); @pop_ra_ok |
1158  | * #st1 #pc1 @if_elim normalize nodelta [2: #_ @res_preserve_error1]
1159   normalize nodelta @eq_block_elim [2: #_ *] #EQbl1 * @if_elim
1160   [2: >EQbl1 @eq_block_elim [#_ *] * #H @⊥ @H <pc_block_eq [%] %
1161       cases bl in EQbl1 EQfn; #p1 #p2 #EQ destruct lapply p2
1162       whd in match sigma_stored_pc; normalize nodelta cases(sigma_pc_opt ???)
1163       normalize nodelta [2: #pc2] #p2 [#_ #EQ destruct]
1164       >fetch_internal_function_no_zero [2: %] #EQ destruct
1165   |   @eq_block_elim [2: #_ *] #EQbl11 * @mfr_return_eq1 normalize nodelta
1166       cases bl in EQbl11 EQfn; #p1 #p2 #EQ destruct
1167       lapply p2 cases(pc_block pc1) #p11 #p22 #e #EQfn1 >EQfn1 %
1168   ]
1169  ]
1170]
1171qed.
1172
1173lemma fetch_ok_sigma_pc_ok :∀prog : ertl_program.
1174∀ f_lbls,f_regs,id,fn,st.
1175fetch_internal_function … (globalenv_noinit … prog)
1176(pc_block (pc … (sigma_state_pc prog f_lbls f_regs st))) = return 〈id,fn〉 →
1177pc … (sigma_state_pc prog f_lbls f_regs st) = pc … st.
1178#prog #f_lbls #f_regs #id #fn #st whd in match sigma_state_pc;
1179normalize nodelta cases(fetch_internal_function ?? (pc_block (pc … st)))
1180normalize nodelta [* #id1 #fn1 #_ %]
1181#e >fetch_internal_function_no_zero [2: %] whd in ⊢ (???% → ?); #EQ destruct(EQ)
1182qed.
1183
1184lemma fetch_ok_sigma_state_ok : ∀prog : ertl_program.
1185∀ f_lbls,f_regs,id,fn,st.
1186fetch_internal_function … (globalenv_noinit … prog)
1187(pc_block (pc … (sigma_state_pc prog f_lbls f_regs st))) = return 〈id,fn〉 →
1188let added ≝ (added_registers ERTL (prog_var_names … prog) fn
1189                                               (f_regs (pc_block (pc … st)))) in
1190st_no_pc … (sigma_state_pc prog f_lbls f_regs st) =
1191sigma_state prog f_lbls f_regs added (st_no_pc … st).
1192#prog #f_lbls #f_regs #id #fn #st #EQf whd in match sigma_state_pc;
1193normalize nodelta <(fetch_ok_sigma_pc_ok … EQf) >EQf %
1194qed.
1195
1196lemma fetch_ok_sigma_pc_block_ok : ∀prog : ertl_program.
1197∀ f_lbls,id,fn,pc.
1198fetch_internal_function … (globalenv_noinit … prog)
1199(pc_block (sigma_stored_pc prog f_lbls pc)) = return 〈id,fn〉 →
1200pc_block (sigma_stored_pc prog f_lbls pc) = pc_block pc.
1201#prog #f_lbls #id #fn #pc #EQf <pc_block_eq [%]
1202lapply EQf whd in match sigma_stored_pc; normalize nodelta
1203cases(sigma_pc_opt ???) normalize nodelta [2: #pc #_ % #EQ destruct(EQ)]
1204>fetch_internal_function_no_zero [2: %] whd in ⊢ (???% → ?); #EQ destruct(EQ)
1205qed.
1206
1207lemma fetch_stmt_ok_sigma_pc_ok : ∀prog : ertl_program.
1208∀ f_lbls,f_regs,id,fn,stmt,st.
1209fetch_statement ERTL_semantics (prog_var_names … prog)
1210    (globalenv_noinit … prog) (pc … (sigma_state_pc prog f_lbls f_regs st)) =
1211               return 〈id,fn,stmt〉 →
1212pc … (sigma_state_pc prog f_lbls f_regs st) = pc … st.
1213#prog #f_lbls #f_regs #id #fn #stmt #st #H @('bind_inversion H)
1214* #id1 #fn1 #EQfn1 #_ @(fetch_ok_sigma_pc_ok … EQfn1)
1215qed.
1216
1217lemma fetch_stmt_ok_sigma_state_ok : ∀prog : ertl_program.
1218∀ f_lbls,f_regs,id,fn,stmt,st.
1219fetch_statement ERTL_semantics (prog_var_names … prog)
1220    (globalenv_noinit … prog) (pc … (sigma_state_pc prog f_lbls f_regs st)) =
1221               return 〈id,fn,stmt〉 →
1222let added ≝ (added_registers ERTL (prog_var_names … prog) fn
1223                                               (f_regs (pc_block (pc … st)))) in
1224st_no_pc … (sigma_state_pc prog f_lbls f_regs st) =
1225sigma_state prog f_lbls f_regs added (st_no_pc … st).
1226#prog #f_lbls #f_regs #id #fn #stmt #st #H @('bind_inversion H) -H
1227* #id1 #fn1 #EQfn1 #H @('bind_inversion H) -H #stmt1 #_
1228whd in ⊢ (??%% → ?); #EQ destruct(EQ) @(fetch_ok_sigma_state_ok … EQfn1)
1229qed.
1230
1231lemma fetch_stmt_ok_sigma_pc_block_ok : ∀prog : ertl_program.
1232∀ f_lbls,id,fn,stmt,pc.
1233fetch_statement ERTL_semantics (prog_var_names … prog)
1234  (globalenv_noinit … prog) (sigma_stored_pc prog f_lbls pc) = return 〈id,fn,stmt〉 →
1235pc_block (sigma_stored_pc prog f_lbls pc) = pc_block pc.
1236#prog #f_lbls #id #fn #stmt #st #H @('bind_inversion H) -H
1237* #id1 #fn1 #EQfn1 #H @('bind_inversion H) -H #stmt1 #_
1238whd in ⊢ (??%% → ?); #EQ destruct(EQ) @(fetch_ok_sigma_pc_block_ok … EQfn1)
1239qed.
1240
1241lemma fetch_ok_sigma_last_pop_ok :∀prog : ertl_program.
1242∀ f_lbls,f_regs,id,fn,st.
1243fetch_internal_function … (globalenv_noinit … prog)
1244(pc_block (pc … (sigma_state_pc prog f_lbls f_regs st))) = return 〈id,fn〉 →
1245last_pop … (sigma_state_pc prog f_lbls f_regs st) =
1246sigma_stored_pc prog f_lbls (last_pop … st).
1247#prog #f_lbls #f_regs #id #fn #st whd in match sigma_state_pc; normalize nodelta
1248cases(fetch_internal_function ?? (pc_block (pc … st))) normalize nodelta
1249[ * #x #y #_ %] #e >fetch_internal_function_no_zero [2: %] whd in ⊢ (???% → ?);
1250#EQ destruct(EQ)
1251qed.
1252
1253lemma fetch_stmt_ok_sigma_last_pop_ok :∀prog : ertl_program.
1254∀ f_lbls,f_regs,id,fn,stmt,st.
1255fetch_statement ERTL_semantics (prog_var_names … prog)
1256    (globalenv_noinit … prog) (pc … (sigma_state_pc prog f_lbls f_regs st))
1257    = return 〈id,fn,stmt〉 →
1258last_pop … (sigma_state_pc prog f_lbls f_regs st) =
1259sigma_stored_pc prog f_lbls (last_pop … st).
1260#prog #f_lbls #f_regs #id #fn #stmt #st #H @('bind_inversion H) -H
1261* #id1 #fn1 #EQfn1 #H @('bind_inversion H) -H #stmt1 #_
1262whd in ⊢ (??%% → ?); #EQ destruct(EQ) @(fetch_ok_sigma_last_pop_ok … EQfn1)
1263qed.
1264
1265lemma excluded_middle_list :
1266∀A : Type[0]. ∀P : A → Prop.∀ l : list A. (∀a : A.In A l a → decidable … (P a)) →
1267All … P l ∨ Exists … (λa.¬(P a)) l.
1268#A #P #l elim l [#_  % %] #hd #tl #IH #Dec
1269cases IH [ cases(Dec hd ?)
1270            [ #H1 #H2 % whd % assumption
1271            | #H #_ %2 whd % assumption
1272            | % %
1273            ]
1274         | #H %2 whd %2 assumption
1275         | #a #H @Dec %2 assumption
1276         ]
1277qed.
1278
1279lemma code_block_of_block_eq : ∀bl : Σb.block_region b = Code.
1280code_block_of_block bl = return bl.
1281* #bl #prf whd in match code_block_of_block; normalize nodelta @match_reg_elim
1282[ >prf in ⊢ (% → ?); #ABS destruct(ABS)] #prf1 %
1283qed.
1284
1285lemma split_on_last_append : ∀A : Type[0]. ∀pre : list A.
1286∀ last : A. split_on_last ? (pre@[last]) = return 〈pre,last〉.
1287#A #pre elim pre [#last %] #a #tl #IH #last whd in ⊢ (??%?);lapply(IH last)
1288whd in ⊢ (??%? → ?); #EQ >EQ %
1289qed.
1290
1291include alias "common/Identifiers.ma".
1292
1293lemma get_sigma_idempotent :
1294∀prog : ertl_program.
1295∀ f_lbls,f_regs.
1296 ∀f_bl_r.
1297 b_graph_transform_program_props ERTL_semantics ERTLptr_semantics
1298     (λglobals,fn.«translate_data globals fn,(refl …)») prog f_bl_r f_lbls f_regs →
1299∀id,fn,bl,pt,stmt.
1300fetch_internal_function … (globalenv_noinit … prog) bl = return 〈id,fn〉 →
1301stmt_at ERTL (prog_var_names … prog) (joint_if_code … fn) pt = return stmt → 
1302f_lbls bl pt = [ ] → get_sigma prog f_lbls bl pt = return pt.
1303#prog #f_lbls #f_regs #f_bl_r #good #id #fn #bl #pt #stmt #EQfn #EQstmt #EQlabels
1304cases(b_graph_transform_program_fetch_internal_function … good … EQfn)
1305#init_data * #calling' ** #EQcalling' whd in ⊢ (% → ?); cases(f_bl_r ?)
1306[2,4: #x #y *] normalize nodelta #EQ destruct(EQ) * #_ #_ #_ #_ #_
1307#_ #fresh_labs #_ #_ #_ #H lapply(H … EQstmt) -H cases stmt in EQstmt;
1308[3: *
1309|2: * [#lbl || *] #EQstmt normalize nodelta * #bl * whd in ⊢ (% → ?);
1310   inversion (f_regs ??) [2,4: #x #y #_ #_ *] #EQregs normalize nodelta
1311   #EQ destruct(EQ) whd in ⊢ (%→?); * #pref * #mid ** #EQmid whd in ⊢ (% → ?);
1312   * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in ⊢ (% → ?); #EQt_stmt
1313| * [#c | * [#c_id|#c_ptr] #args #dest | #r #lbl | #seq ] #nxt #EQstmt
1314  whd in ⊢ (% → ?); * #bl >if_merge_right [2,4,6,8,10: %] * whd in ⊢ (% → ?);
1315  inversion(f_regs ??) normalize nodelta
1316  [2,4,5,8,10: [1,2,4,5: #x #y] #_ [1,2,3,4: #_] *|6: #r * [2: #x #y] ]
1317  [1,2: #_] #EQregs [1,2: whd in ⊢ (% → ?); [*]] #EQ destruct(EQ) whd in ⊢ (% → ?);
1318  * #l1 * #mid1 * #mid2 * #l2 *** #EQmid1 whd in ⊢ (%→ ?);
1319  [ * #mid * #rest ** #EQ destruct(EQ) whd in ⊢ (% → ?); * #nxt1 *
1320    #EQlow change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ)
1321    whd in ⊢ (% → ?); * #mid3 * #rest1 ** #EQ destruct(EQ)
1322     whd in EQmid1 : (???%); destruct(EQmid1) whd in e0 : (???%); >EQlabels in e0;
1323    #e0 destruct(e0) ] * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in EQmid1 : (???%);
1324     destruct(EQmid1) whd in ⊢ (% → ?); * #nxt1 * #EQt_stmt
1325     change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) whd in ⊢ (% → ?);
1326     * #_ #EQ destruct(EQ) ]
1327whd in match get_sigma; normalize nodelta >code_block_of_block_eq >m_return_bind
1328>EQfn >m_return_bind inversion(find ????)
1329[1,3,5,7,9,11: #EQfind @⊥ lapply(find_none ?????? EQfind EQstmt) >EQlabels
1330  normalize nodelta @eq_identifier_elim [1,3,5,7,9,11: #_ * |*: * #H #_ @H %]]
1331* #lbl #s #EQfind >m_return_bind lapply(find_predicate ?????? EQfind)
1332inversion(f_lbls ??)
1333[1,3,5,7,9,11: #_ normalize nodelta @eq_identifier_elim [2,4,6,8,10,12: #_ *] #EQ #_ >EQ %]
1334#lb #l @(list_elim_left … l …) normalize nodelta
1335[1,3,5,7,9,11: #_ #EQlb @eq_identifier_elim
1336               [1,3,5,7,9,11: #EQ destruct(EQ) #_ @⊥ |*: #_ *]
1337               lapply(fresh_labs lbl) >EQlb *** #H #_ #_ @H
1338               @(code_is_in_universe … (pi2 ?? fn)) whd in match code_has_label;
1339               whd in match code_has_point; normalize nodelta >EQstmt @I ]
1340#last #pre #_ #_ #EQlbl >(split_on_last_append … (lb::pre) last)
1341normalize nodelta @eq_identifier_elim
1342[2,4,6,8,10,12: #_ *] #EQ lapply EQlbl destruct(EQ) #EQlbl #_ @⊥
1343lapply(fresh_labs lbl) >EQlbl whd in ⊢ (% → ?); * #_ #H lapply(append_All … H) -H
1344* #_ whd in ⊢ (% → ?); *** #H #_ #_ @H -H @(code_is_in_universe … (pi2 ?? fn))
1345whd in match code_has_label; whd in match code_has_point; normalize nodelta
1346>EQstmt @I
1347qed.
1348
1349lemma append_absurd : ∀A : Type[0]. ∀l : list A. ∀ a : A.
1350l @ [a] = [ ] → False.
1351#A * [2: #x #y] #a normalize #EQ destruct
1352qed.
1353
1354lemma last_append_eq : ∀A : Type[0].∀l1,l2 : list A. ∀a1,a2: A.
1355l1 @ [a1] = l2 @ [a2] → a1 = a2.
1356#A #l1 elim l1 [ * [2: #hd #tl] #a1 #a2 normalize #EQ destruct [2: %]
1357@⊥ lapply(sym_eq ??? e0) -e0 #e0 @(append_absurd ??? e0)] #hd #tl #IH
1358* [ #a1 #a2 normalize #EQ destruct @⊥ @(append_absurd ??? e0)]
1359#hd1 #tl1 #a1 #a2 normalize #EQ destruct(EQ) @(IH tl1 a1 a2 e0)
1360qed.
1361
1362
1363lemma get_sigma_last :
1364∀prog : ertl_program.
1365∀ f_lbls,f_regs.
1366 ∀f_bl_r.
1367 b_graph_transform_program_props ERTL_semantics ERTLptr_semantics
1368     (λglobals,fn.«translate_data globals fn,(refl …)») prog f_bl_r f_lbls f_regs →
1369∀id,fn,bl,pt,stmt,pre,last.
1370fetch_internal_function … (globalenv_noinit … prog) bl = return 〈id,fn〉 →
1371stmt_at ERTL (prog_var_names … prog) (joint_if_code … fn) pt = return stmt → 
1372f_lbls bl pt = pre@[last] → get_sigma prog f_lbls bl last = return pt.
1373#prog #f_lbls #f_regs #f_bl_r #good #id #fn #bl #pt #stmt #pre #last
1374#EQfn #EQstmt #EQlabels
1375cases(b_graph_transform_program_fetch_internal_function … good … EQfn)
1376#init_data * #calling' ** #EQcalling' whd in ⊢ (% → ?); cases(f_bl_r ?)
1377[2: #x #y *] normalize nodelta #EQ destruct(EQ) * #_ #_ #_ #_ #pp_labs
1378#_ #fresh_labs #_ #_ #_ #H lapply(H … EQstmt) -H normalize nodelta
1379cases stmt in EQstmt; normalize nodelta
1380[3: *
1381|2: * [#lbl || *] #EQstmt whd in ⊢ (%→ ?); * #bl *
1382|*: * [#c | * [ #c_id | #c_ptr] #args #dest | #r #lbl | #seq ] #nxt #EQstmt
1383    >if_merge_right [2,4,6,8,10: %] whd in ⊢ (% → ?); * #bl *
1384]
1385whd in ⊢ (% → ?); inversion(f_regs ??) normalize nodelta
1386[2,4,6,8,9,12,14: [1,2,3,4,6,7: #x #y #_] #_ *|10: #r #tl #_] #EQregs
1387[ whd in ⊢ (% → ?); cases tl in EQregs; normalize nodelta [2: #x #y #_ *] #EQregs]
1388#EQbl destruct(EQbl) whd in ⊢ (%→?); [2,3: * #pref * #mid **|*: * #l1 * #mid1 * #mid2 * #l2 ***]
1389#EQmid1 whd in ⊢ (% → ?);
1390[1,2,4,5,6,7: * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in EQmid1 : (??%%); destruct(EQmid1)               
1391[3,4,5,6: whd in ⊢ (% → ?); * #nxt1 * #EQt_stmt  #EQ destruct(EQ) ]
1392whd in ⊢ (% → ?); * [1,2,3,4: #e0] @⊥ >EQlabels in e0; #e0 @(append_absurd ??? e0)]
1393* #mid * #rest ** #EQ destruct(EQ) whd in ⊢ (% → ?); * #nxt1 * #_
1394change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) whd in ⊢ (% → ?);
1395* #mid3 * #rest1 ** #EQ destruct(EQ) whd in ⊢ (% → ?); * #nxt1 * #_
1396change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) whd in ⊢ (% → ?);
1397* #mid4 * #rest2 ** #EQ destruct(EQ)  whd in ⊢ (% → ?); * #nxt1 * #_
1398change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) whd in ⊢ (% → ?);
1399* #mid5 * #rest3 ** #EQ destruct(EQ) whd in ⊢ (% → ?); * #nxt1 * #_
1400change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) whd in ⊢ (% → ?);
1401* #EQ1 #EQ2 destruct(EQ1 EQ2) whd in ⊢ (% → ?); * #nxt1 * #EQcall
1402change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) whd in ⊢ (% → ?);
1403* #EQ1 #EQ2 destruct(EQ1 EQ2) whd in EQmid1 : (??%%); destruct(EQmid1)
1404>e0 in EQlabels; #EQlabels whd in match get_sigma; normalize nodelta
1405>code_block_of_block_eq >m_return_bind >EQfn >m_return_bind
1406inversion(find ????)
1407[ #EQfind @⊥ lapply(find_none ?????? EQfind EQstmt) >e0
1408  normalize nodelta @eq_identifier_elim [ #_ *] * #H #_ @H
1409  >(last_append_eq ????? EQlabels) % ]
1410* #lbl #s #EQfind >m_return_bind lapply(find_predicate ?????? EQfind)
1411inversion(f_lbls ??)
1412[ #EQlbl normalize nodelta @eq_identifier_elim [2: #_ *] #EQ destruct(EQ)
1413  lapply(last_append_eq ????? EQlabels) #EQ destruct(EQ) @⊥
1414  lapply(fresh_labs pt) >e0 * #_ * #_ * #_ *** #H #_ #_ @H -H
1415   @(code_is_in_universe … (pi2 ?? fn)) whd in match code_has_label;
1416  whd in match code_has_point; normalize nodelta whd in match (stmt_at ????);
1417  >(find_lookup ?????? EQfind) @I
1418]
1419#lb #labels #_  @(list_elim_left … (labels) …) -labels normalize nodelta
1420[2: #last1 #pre #_] #EQl [ >(split_on_last_append … (lb::pre) last1) ]
1421normalize nodelta @eq_identifier_elim [2,4: #_ *] #EQ destruct(EQ) #_
1422lapply(last_append_eq ????? EQlabels) #EQ destruct(EQ)
1423lapply pp_labs whd in match partial_partition; normalize nodelta * #_ #H
1424lapply(H lbl pt) >e0 whd in EQmid : (??%%); >EQl
1425#H [ >(H last1 ? ?) | >(H lb ? ?) ] [1,4: %
1426               |6: whd in match (memb ???); @if_elim [#_ @I]
1427                  #H lapply(Prop_notb ? H) * -H #H @⊥ @H cases lb #x normalize
1428                  @if_elim [#_ %] #H lapply(Prop_notb ? H) * -H #H @H >(eqb_n_n x) %
1429               |5: >(memb_append_l2 ? lb ? [lb] ?) /2 by /
1430               |*: >(memb_append_l2 ? last1 ? [last1] ?) /2 by /
1431                   @Exists_memb %2 elim pre [ % % | #hd #tl #IH %2 @IH]
1432               ]
1433qed.
1434
1435
1436lemma fetch_call_commute :
1437∀prog : ertl_program.
1438let trans_prog ≝ ertl_to_ertlptr prog in
1439∀ f_lbls,f_regs.
1440 ∀f_bl_r.
1441 b_graph_transform_program_props ERTL_semantics ERTLptr_semantics
1442     (λglobals,fn.«translate_data globals fn,(refl …)») prog f_bl_r f_lbls f_regs →
1443∀id,fn,c_id,c_args,c_dest,nxt,pc.
1444fetch_statement ERTL_semantics
1445    (prog_var_names … prog) (globalenv_noinit … prog) pc =
1446    return 〈id,fn, sequential ? ?(CALL ERTL_semantics ? c_id c_args c_dest) nxt〉 →
1447∃fn',pc'. sigma_stored_pc prog f_lbls pc' = pc ∧
1448fetch_statement ERTLptr_semantics
1449    (prog_var_names … trans_prog) (globalenv_noinit … trans_prog) pc' =
1450return 〈id,fn', sequential ? ?(CALL ERTLptr_semantics ? c_id c_args c_dest) nxt〉.
1451#prog #f_lbls #f_regs #f_bl_r #good #id #fn * [ #c_id | #c_ptr ] #c_args #c_dest
1452#nxt #pc #EQfetch lapply(fetch_statement_inv … EQfetch) * #EQfn #EQstmt
1453cases(b_graph_transform_program_fetch_internal_function … good … EQfn)
1454#init_data * #calling' ** #EQcalling' whd in ⊢ (% → ?); cases(f_bl_r ?)
1455[2,4: #x #y *] normalize nodelta #EQ destruct(EQ) * #_ #_ #_ #_ #_
1456#_ #_ #_ #_ #_ #H cases(H … EQstmt) -H #bl whd in ⊢ (% → ?); *
1457>if_merge_right [2,4: %] whd in match translate_step;
1458normalize nodelta whd in ⊢ (% → ?); inversion(f_regs ??) normalize nodelta
1459[|2,3:[ #x #y #_] #_ * |4: #r #tl #_ ] #EQregs
1460[ | cases tl in EQregs; [2: #x #y #_ *] #EQregs whd in ⊢ (% → ?);] #EQ destruct(EQ)
1461whd in ⊢ (% → ?); * #pre_l * #mid1 * #mid2 * #post_l *** #EQmid1 whd in ⊢ (% → ?);
1462[2: * #mid * #resg ** #EQ destruct(EQ) whd in ⊢ (% → ?);
1463  * #nxt1 * #EQlow change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ)
1464  whd in ⊢ (% → ?); * #mid3 * #rest1 ** #EQ destruct(EQ) * #nxt1 *
1465  #EQpush1 change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ)
1466  whd in ⊢ (% → ?); * #mid4 * #rest2 ** #EQ destruct(EQ) * #nxt1 * #EQhigh
1467  change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) whd in ⊢ (% → ?);
1468  * #mid5 * #rest3 ** #EQ destruct(EQ) * #nxt1 * #EQpush2
1469  change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) whd in ⊢ (% → ?);
1470] * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in EQmid1 : (??%%); destruct(EQmid1)
1471whd in ⊢ (% → ?); * #nxt1 * #EQcall #EQ destruct(EQ) whd in ⊢ (% → ?);
1472* #EQ destruct(EQ) change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ)
1473%{calling'}
1474[  %{(pc_of_point ERTLptr_semantics (pc_block pc) mid1)}
1475|  %{pc}
1476] %
1477[1,3: whd in match sigma_stored_pc; whd in match sigma_pc_opt; normalize nodelta
1478      @eqZb_elim change with (pc_block pc) in match (pc_block ?) in ⊢ (% → ?);
1479      [1,3: #EQbl >fetch_internal_function_no_minus_one in EQfn; try assumption
1480            #EQ destruct(EQ)] #_ normalize nodelta
1481            [2: >(get_sigma_idempotent … good … EQfn EQstmt EQ)
1482            |*: change with (pc_block pc) in match (pc_block ?);
1483                >point_of_pc_of_point >(get_sigma_last … good … EQfn EQstmt e0)
1484            ] >m_return_bind normalize nodelta >pc_of_point_of_pc %
1485|*: whd in match fetch_statement; normalize nodelta >EQcalling' >m_return_bind
1486    [>point_of_pc_of_point ] >EQcall %
1487]
1488qed.
1489
1490
1491
1492lemma next_of_call_pc_ok : ∀prog : ertl_program.
1493let trans_prog ≝ ertl_to_ertlptr prog in
1494∀ f_lbls,f_regs.∀f_bl_r.
1495b_graph_transform_program_props ERTL_semantics ERTLptr_semantics
1496     (λglobals,fn.«translate_data globals fn,(refl …)») prog f_bl_r f_lbls f_regs →
1497∀pc,lb.
1498next_of_call_pc ERTL_semantics (prog_var_names … prog) (globalenv_noinit … prog)
1499  pc = return lb →
1500∃pc'. sigma_stored_pc prog f_lbls pc' = pc ∧ 
1501next_of_call_pc ERTLptr_semantics (prog_var_names … trans_prog)
1502             (globalenv_noinit … trans_prog) pc' =  return lb.
1503#prog #f_lbls #f_regs #f_bl_r #good #pc #lb whd in match next_of_call_pc;
1504normalize nodelta #H @('bind_inversion H) -H ** #id #fn
1505*  [ *[ #c | #c_id #c_arg #c_dest | #reg #lbl | #seq ] #prox | #fin | *]
1506#EQfetch normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ)
1507cases(fetch_call_commute … good … EQfetch) #fn1 * #pc1 * #EQpc1 #EQt_fetch
1508%{pc1} % [assumption] >EQt_fetch %
1509qed.
1510
1511lemma next_of_call_pc_error : ∀pars.∀prog : program ? ℕ. ∀init,pc.
1512(block_id (pi1 … (pc_block pc)) = 0 ∨ block_id (pi1 … (pc_block pc)) = -1) →
1513next_of_call_pc pars (prog_var_names … prog) (globalenv … init prog)
1514  pc = Error ? [MSG BadFunction].
1515#pars #prg #init #pc * #EQ whd in match next_of_call_pc; normalize nodelta
1516whd in match fetch_statement; normalize nodelta
1517[ >fetch_internal_function_no_zero | >fetch_internal_function_no_minus_one]
1518//
1519qed.
1520
1521lemma next_of_call_pc_inv :  ∀pars.∀prog : program ? ℕ. ∀init.
1522∀pc,nxt.
1523next_of_call_pc pars (prog_var_names … prog)
1524(globalenv … init prog) pc = return nxt →
1525∃id,fn,c_id,c_args,c_dest.
1526fetch_statement pars
1527    (prog_var_names … prog) (globalenv … init prog) pc =
1528    return 〈id,fn, sequential ? ?(CALL pars ? c_id c_args c_dest) nxt〉.
1529#pars #prog #init #pc #nxt whd in match next_of_call_pc; normalize nodelta
1530#H @('bind_inversion H) -H ** #id #fn *
1531[ *[ #c | #c_id #c_arg #c_dest | #reg #lbl | #seq ] #prox | #fin | #H #r #l #l ]
1532#EQfetch normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ)
1533%{id} %{fn} %{c_id} %{c_arg} %{c_dest} assumption
1534qed.
1535
1536lemma sigma_stored_pc_inj : ∀ prog : ertl_program.
1537∀f_lbls,pc,pc'. sigma_pc_opt prog f_lbls pc ≠ None ? →
1538sigma_pc_opt prog f_lbls pc = sigma_pc_opt prog f_lbls pc' →
1539pc = pc'.
1540#prog #f_lbls ** #id #EQblid #off ** #id' #EQblid' #off'
1541* inversion(sigma_pc_opt ???) [#_ #H @⊥ @H %]
1542#pc1 whd in match sigma_pc_opt; normalize nodelta @if_elim
1543[ @eqZb_elim [2: #_ *] #EQbl * whd in ⊢ (??%? → ?); #EQ destruct #_
1544#H lapply(sym_eq ??? H) -H @if_elim [#_ whd in ⊢ (??%? → ?); #EQ destruct %]
1545@eqZb_elim [ #_ *] * #EQbl' #_ #H @('bind_inversion H) -H #lb #EQlb
1546whd in ⊢ (??%? → ?); #EQ destruct @⊥ @EQbl' assumption] @eqZb_elim [#_ *] * #EQbl #_
1547#H @('bind_inversion H) -H * #lb #EQlb whd in ⊢ (??%? → ?); #EQ destruct #_
1548#H lapply(sym_eq ??? H) -H @if_elim
1549[ @eqZb_elim [2: #_ *] #EQbl' #_ whd in ⊢ (??%? → ?); #EQ destruct @⊥ @EQbl @EQbl']
1550#_ #H @('bind_inversion H) -H * #lb' #EQlb' whd in ⊢ (??%? → ?);
1551whd in match (pc_of_point ???); whd in match (offset_of_point ??);
1552whd in match (offset_of_point ??); #EQ destruct @eq_f
1553cut(an_identifier LabelTag off = an_identifier LabelTag off') [2: #EQ destruct %]
1554@(partial_inj_sigma prog f_lbls id) [>EQlb % #ABS destruct | >EQlb >EQlb' %]
1555qed.
1556
1557lemma bool_of_beval_ok : ∀prog : ertl_program.
1558∀f_lbls. preserving1 … res_preserve1 …
1559              (sigma_beval prog f_lbls)
1560              (λx.x)
1561              (bool_of_beval)
1562              (bool_of_beval).
1563#prog #f_lbls * [ | | #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc1 #p1]
1564whd in match bool_of_beval; normalize nodelta try @res_preserve_error1
1565try @mfr_return1 whd in match sigma_beval; normalize nodelta
1566cases (sigma_pc_opt ???) normalize nodelta [2: #pc] @res_preserve_error1
1567qed.
1568
1569
1570lemma block_of_call_ok : ∀prog: ertl_program.
1571 let trans_prog ≝ ertl_to_ertlptr prog in
1572 ∀ f_lbls,f_regs.
1573∀called,restr. preserving1 … res_preserve1 …
1574              (sigma_state prog f_lbls f_regs restr)
1575              (λx.x)
1576              (block_of_call ERTL_semantics (prog_var_names … prog)
1577                      (globalenv_noinit … prog) called)
1578              (block_of_call ERTLptr_semantics (prog_var_names … trans_prog)
1579                      (globalenv_noinit … trans_prog) called).
1580#prog #f_lbls #f_regs #called #restr #st whd in match block_of_call; normalize nodelta
1581@mfr_bind1
1582[ @(λx.x)
1583| cases(called) [#c_id | #c_ptr] normalize nodelta
1584  [ @opt_to_res_preserve1 #bl #EQbl %{bl} % [2: %]
1585    >(find_symbol_transf …
1586          (λvars.transf_fundef … (λfn.(b_graph_translate … fn))) prog c_id)
1587   assumption
1588  | @mfr_bind1
1589    [2: whd in match dpl_arg_retrieve; normalize nodelta @(ps_arg_retrieve_ok) |
1590    | #bv1 @mfr_bind1
1591      [2: whd in match dph_arg_retrieve; normalize nodelta @(ps_arg_retrieve_ok) |
1592      | #bv2 @mfr_bind1
1593        [ @(λx.x)
1594        | whd in match pointer_of_bevals; normalize nodelta
1595          cases bv1 normalize nodelta
1596          [ | | #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc1 #p1]
1597          try @res_preserve_error1
1598          [ cases bv2 [ | | #ptr1' #ptr2' #p' | #by' | #p' | #ptr' #p' | #pc1' #p1']
1599          normalize nodelta
1600          [1,2,3,4,5: @res_preserve_error1
1601          | @if_elim #_ [@mfr_return_eq1 % | @res_preserve_error1]
1602          ]
1603          ] whd in match sigma_beval; normalize nodelta cases(sigma_pc_opt ???)
1604            normalize nodelta [2,4: #pc ] @res_preserve_error1
1605        |
1606        #ptr @if_elim #_ [@mfr_return_eq1 % | @res_preserve_error1]
1607      ]
1608    ]
1609  ]
1610 ]
1611| #bl @opt_to_res_preserve1 whd in match code_block_of_block; normalize nodelta
1612  @match_reg_elim [ #_ @opt_preserve_none1 | #prf @mfr_return_eq1 %]
1613]
1614qed.
1615
1616lemma bvpc_sigma_pc_to_sigma_beval : ∀prog : ertl_program.
1617∀f_lbls,pc,p. sigma_pc_opt prog f_lbls pc ≠ None ? →
1618BVpc (sigma_stored_pc prog f_lbls pc) p =
1619sigma_beval prog f_lbls (BVpc pc p).
1620#prog #f_lbls #pc #p #prf whd in match sigma_stored_pc;
1621whd in match sigma_beval; normalize nodelta lapply prf
1622cases(sigma_pc_opt ???) [ * #H @⊥ @H % | #pc' #_ % ]
1623qed.
1624
1625lemma push_ra_ok : ∀prog : ertl_program.
1626∀f_lbls,f_regs,restr,pc. sigma_pc_opt prog f_lbls pc ≠ None ? →
1627    preserving1 ?? res_preserve1 …
1628          (sigma_state prog f_lbls f_regs restr)
1629          (sigma_state prog f_lbls f_regs restr)
1630          (λst.push_ra ERTL_semantics st (sigma_stored_pc prog f_lbls pc))
1631          (λst.push_ra ERTLptr_semantics st pc).
1632#prog #f_lbls #f_regs #restr #pc #prf #st whd in match push_ra; normalize nodelta
1633@mfr_bind1
1634[  @(sigma_state prog f_lbls f_regs restr)
1635|  >(bvpc_sigma_pc_to_sigma_beval … prf) @push_ok
1636|  #st' >(bvpc_sigma_pc_to_sigma_beval … prf) @push_ok
1637] qed.
1638
1639
1640lemma ertl_save_frame_ok : ∀prog : ertl_program.
1641∀f_lbls.∀f_regs : regs_funct.∀kind,restr.
1642preserving1 ?? res_preserve1 ????
1643      (λst : Σs: state_pc ERTLptr_semantics.
1644             sigma_pc_opt prog f_lbls (pc … s) ≠ None ?
1645      . match fetch_internal_function … (globalenv_noinit … prog)
1646                       (pc_block (pc … st)) with
1647                 [ OK y ⇒ let 〈f,fn〉 ≝ y in
1648                          let added ≝ added_registers … (prog_var_names … prog) fn
1649                                       (f_regs (pc_block (pc … st))) in
1650                          mk_state_pc ? (sigma_state prog f_lbls f_regs added st)
1651                                        (sigma_stored_pc prog f_lbls (pc … st))
1652                                        (sigma_stored_pc prog f_lbls (last_pop … st))
1653                 | Error e ⇒ dummy_state_pc
1654                 ])
1655           (sigma_state prog f_lbls f_regs restr)
1656           (ertl_save_frame kind it)
1657           (match kind with
1658            [ID ⇒ ertlptr_save_frame kind it
1659            |PTR ⇒ λst. !st' ← push_ra … st (pc … st);
1660                        ertlptr_save_frame kind it (set_no_pc … st' st)
1661            ]).
1662#prog #f_lbls #f_regs * #restr * #st #st_prf
1663inversion(fetch_internal_function ???) normalize nodelta
1664[1,3: * #f #fn #EQfn normalize nodelta whd in match ertl_save_frame; whd in match ertlptr_save_frame;
1665      normalize nodelta @mfr_bind1
1666      [2,5: @push_ra_ok [1,2: assumption] |1,4: skip
1667      |*: #st1 [ >m_return_bind] @mfr_bind_inversion1
1668          [1,4: @(λf.match sigma_frames_opt prog f_lbls f_regs f with [Some g ⇒  g | None ⇒ [ ]])
1669          |2,5: @opt_to_res_preserve1 whd in match sigma_state; whd in match set_no_pc;
1670                normalize nodelta cases(st_frms … st1) [1,3: @opt_preserve_none1]
1671                #frames #frames1 whd in match sigma_frames; normalize nodelta
1672                >m_return_bind #EQframes %{frames} % [%] >EQframes %
1673          |*: #frames #H lapply(opt_eq_from_res ???? H) -H whd in match sigma_state;
1674              normalize nodelta #EQt_frames #H lapply(opt_eq_from_res ???? H) -H
1675              whd in match set_no_pc; normalize nodelta #EQframes >EQframes in EQt_frames;
1676              whd in match sigma_frames; normalize nodelta >m_return_bind
1677              inversion(sigma_frames_opt ???) [1,3: #_ #ABS destruct(ABS)]
1678              #t_frames #EQt_frames #_ @mfr_return_eq1 normalize nodelta @eq_f
1679              whd in match set_frms; normalize nodelta >m_return_bind
1680              cut(∀ a1,a2,b1,b2,c1,c2,d1,d2,e1,e2.
1681                    a1=a2 → b1 = b2 → c1 = c2 → d1 = d2 → e1 = e2 →
1682                      mk_state ERTL_semantics a1 b1 c1 d1 e1 =
1683                      mk_state ERTL_semantics a2 b2 c2 d2 e2)
1684              [1,3: #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14
1685                    #H15 //] #APP @APP try %
1686              [1,3: whd in match sigma_frames_opt; whd in match m_list_map;
1687                    normalize nodelta  whd in match (foldr ?????); normalize nodelta
1688                    >EQfn >m_return_bind normalize nodelta
1689                    change with (sigma_frames_opt prog f_lbls f_regs frames)
1690                                                         in match (foldr ?????);
1691                    >EQt_frames >m_return_bind whd in match sigma_regs;
1692                    normalize nodelta cases(regs … st1) #ps_reg #hw_reg
1693                    >(pc_block_eq … st_prf) %
1694              |*: whd in match set_regs; whd in match sigma_regs; normalize nodelta
1695                  cases(regs … st1) #ps_r #hw_r normalize nodelta
1696                  whd in match sigma_register_env; normalize nodelta
1697                  @eq_f2 // change with (empty_map RegisterTag beval) in match (map RegisterTag ????);
1698                  <(empty_set_minus … restr) %
1699              ]
1700          ]
1701      ]   
1702|*: #e #_ #x whd in match ertl_save_frame; normalize nodelta normalize nodelta
1703    #H @('bind_inversion H) -H #y whd in match push_ra; normalize nodelta
1704    #H @('bind_inversion H) -H #z whd in match push; normalize nodelta
1705    whd in match (istack ??); whd in match is_push; normalize nodelta
1706    >m_return_bind whd in match set_istack; normalize nodelta whd in ⊢ (??%% →?);
1707    #EQ destruct(EQ) normalize nodelta >m_return_bind whd in ⊢ (??%% → ?);
1708    #EQ destruct(EQ) whd in match (st_frms ??); whd in ⊢ (??%% → ?);
1709    #EQ destruct(EQ)
1710]
1711qed.
1712
1713
Note: See TracBrowser for help on using the repository browser.