source: src/ERTL/ERTLtoERTLptrUtils.ma @ 2801

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

Partial commit not yet finished

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