source: src/ERTL/ERTLtoERTLptrUtils.ma @ 2786

Last change on this file since 2786 was 2786, checked in by piccolo, 8 years ago

Splitted ERTLtoERTLptrOK.ma and added new file with commutation lemmas

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