Changeset 2785 for src


Ignore:
Timestamp:
Mar 6, 2013, 2:58:09 PM (7 years ago)
Author:
piccolo
Message:

Traces.ma repaired

Location:
src
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLtoERTLptrOK.ma

    r2783 r2785  
    1414(**************************************************************************)
    1515
    16 include "ERTL/ERTLToERTLptr.ma".
    17 include "common/StatusSimulation.ma".   
    18 include "joint/Traces.ma".
    19 include "ERTLptr/ERTLptr_semantics.ma".
    20 include "common/ExtraMonads.ma".
    21 
    22 definition ERTL_status ≝
    23 λprog : ertl_program.λstack_sizes.
    24 joint_abstract_status (mk_prog_params ERTL_semantics prog stack_sizes).
    25 
    26 definition ERTLptr_status ≝
    27 λprog : ertlptr_program.λstack_sizes.
    28 joint_abstract_status (mk_prog_params ERTLptr_semantics prog stack_sizes).
    29 
    30 definition sigma_map ≝  block → label → option label.
    31 definition lbl_funct ≝  block → label → option (list label).
    32 definition regs_funct ≝ block → label → option (list register).
    33  (*
    34 definition get_internal_function_from_ident :
    35 ∀ p: sem_params. ∀ globals : list ident . ∀ge : genv_t (joint_function p globals).
    36 ident → option(joint_closed_internal_function p globals) ≝
    37 λp,globals,ge,id.
    38 ! bl  ← (find_symbol (joint_function p globals) ge id);
    39 ! bl' ← (code_block_of_block bl);
    40 ! 〈f,fn〉 ← res_to_opt … (fetch_internal_function ? ge bl');
    41 return fn.
    42 *)
    43 
    44 lemma match_reg_elim : ∀ A : Type[0]. ∀ P : A → Prop. ∀ r : region.
    45 ∀f : (r = XData) → A. ∀g : (r = Code) → A. (∀ prf : r = XData.P (f prf)) →
    46 (∀ prf : r = Code.P (g prf)) →
    47 P ((match r return λx.(r = x → ?) with
    48     [XData ⇒ f | Code ⇒ g])(refl ? r)).
    49 #A #P * #f #g #H1 #H2 normalize nodelta [ @H1 | @H2]
    50 qed.
     16include "ERTL/ERTLtoERTLptrUtils.ma".
     17
     18
    5119
    5220(*
     
    6836*)
    6937
    70 definition get_sigma :
    71 ertl_program → lbl_funct → sigma_map ≝
    72 λprog,f_lbls.λbl,searched.
    73 let globals ≝ prog_var_names … prog in
    74 let ge ≝ globalenv_noinit … prog in
    75 ! bl ← code_block_of_block bl ;
    76 ! 〈id,fn〉 ← res_to_opt … (fetch_internal_function … ge bl);
    77 !〈res,s〉 ← find ?? (joint_if_code … fn)
    78                 (λlbl.λ_. match f_lbls bl lbl with
    79                           [None ⇒ false
    80                           |Some lbls ⇒
    81                              match split_on_last … lbls with
    82                                 [None ⇒ eq_identifier … searched lbl
    83                                 |Some x ⇒ eq_identifier … searched (\snd x)
    84                                 ]
    85                           ]);
    86 return res.
    87 
    88 definition sigma_pc_opt : 
    89 ertl_program →  lbl_funct →
    90 program_counter → option program_counter ≝
    91 λprog,f_lbls,pc.
    92   let sigma ≝ get_sigma prog f_lbls in
    93   let ertl_ptr_point ≝ point_of_pc ERTLptr_semantics pc in
    94   if eqZb       (block_id (pc_block pc)) (-1) then (* check for dummy exit pc *)
    95     return pc
    96   else
    97        ! ertl_point ← sigma (pc_block pc) ertl_ptr_point;
    98        return pc_of_point
    99                    ERTL_semantics (pc_block pc) ertl_point.
    100 
    101 definition sigma_stored_pc ≝
    102 λprog,f_lbls,pc. match sigma_pc_opt prog f_lbls pc with
    103       [None ⇒ null_pc (pc_offset … pc) | Some x ⇒ x].
    104      
    105      
    106 definition sigma_beval : ertl_program → lbl_funct →
    107   beval → beval ≝
    108 λprog,f_lbls,bv.
    109 match bv with
    110 [ BVpc pc prt ⇒ match sigma_pc_opt prog f_lbls pc with
    111                  [None ⇒ BVundef | Some x ⇒ BVpc x prt]
    112 | _ ⇒ bv
    113 ].
    114 
    115 definition sigma_is : ertl_program → lbl_funct →
    116 internal_stack → internal_stack ≝
    117 λprog,f_lbls,is.
    118 match is with
    119 [ empty_is ⇒ empty_is
    120 | one_is bv ⇒ one_is (sigma_beval prog f_lbls bv)
    121 | both_is bv1 bv2 ⇒
    122   both_is (sigma_beval prog f_lbls bv1) (sigma_beval prog f_lbls bv2)
    123 ].
    124 
    125 lemma sigma_is_empty : ∀prog,sigma.
    126   sigma_is prog sigma empty_is = empty_is.
    127 #prog #sigma % qed.
    128 
    129 definition sigma_mem : ertl_program → lbl_funct →
    130  bemem → bemem ≝
    131  λprog,f_lbls,m.
    132  mk_mem
    133   (λb.
    134     If Zltb (block_id b) (nextblock m) then with prf' do   
    135       let l ≝ low_bound m b in
    136       let h ≝ high_bound m b in
    137       mk_block_contents l h
    138       (λz.If Zleb l z ∧ Zltb z h then with prf'' do
    139         sigma_beval prog f_lbls (contents (blocks m b) z)
    140       else BVundef)
    141     else empty_block OZ OZ)
    142   (nextblock m)
    143   (nextblock_pos m).
    144 
    145 include "common/ExtraIdentifiers.ma".
    146 
    147 
    148 definition sigma_register_env :
    149 ertl_program → lbl_funct →
    150 list register →
    151 register_env beval → register_env beval ≝
    152 λprog,f_lbls,ids,psd_env.
    153 let m' ≝  map ??? psd_env (λbv.sigma_beval prog f_lbls bv) in
    154 m' ∖ ids.
    155 
    156 
    157 definition sigma_frames_opt : ertl_program →
    158 lbl_funct → regs_funct →
    159 list (register_env beval × (Σb:block.block_region b=Code)) →
    160 option (list (register_env beval × (Σb:block.block_region b=Code))) ≝
    161 λprog,f_lbls,f_regs,frms.
    162 let globals ≝ prog_var_names … prog in
    163 let ge ≝ globalenv_noinit … prog in
    164 m_list_map ? ? ?
    165 (λx.let 〈reg_env,bl〉 ≝ x in
    166     ! 〈id,fn〉 ← res_to_opt … (fetch_internal_function … ge bl);
    167     return 〈sigma_register_env prog f_lbls
    168                 (added_registers ERTL globals fn (f_regs bl)) reg_env,bl〉) frms.
    169                
    170 definition sigma_frames :   ertl_program →
    171 lbl_funct → regs_funct →
    172 option (list (register_env beval × (Σb:block.block_region b=Code))) →
    173 option (list (register_env beval × (Σb:block.block_region b=Code))) ≝
    174 λprog,f_lbls,f_regs,frms.
    175 ! frames ← frms;
    176 sigma_frames_opt prog f_lbls f_regs frames.
    177        
    178 include "common/BitVectorTrieMap.ma".
    179 
    180 definition sigma_hw_register_env :ertl_program →
    181 lbl_funct →  hw_register_env → hw_register_env ≝
    182 λprog,f_lbls,h_reg.mk_hw_register_env
    183 (map ? ? (sigma_beval prog f_lbls) 6 (reg_env … h_reg)) (other_bit … h_reg).
    184 
    185 definition sigma_regs :ertl_program →
    186 lbl_funct →  list register →
    187 (register_env beval)×hw_register_env→
    188 (register_env beval)×hw_register_env ≝
    189 λprog,f_lbls,ids,regs.let 〈x,y〉≝ regs in
    190       〈sigma_register_env prog f_lbls ids x,
    191        sigma_hw_register_env prog f_lbls y〉.
    192 
    193 definition dummy_state : state ERTL_semantics ≝
    194 mk_state ERTL_semantics
    195    (None ?) empty_is BBundef 〈empty_map ? ?,mk_hw_register_env … (Stub …) BBundef〉 empty.
    196 
    197 definition sigma_state : ertl_program →
    198 lbl_funct → regs_funct → list register →
    199 state ERTLptr_semantics → state ERTL_semantics ≝
    200 λprog,f_lbls,f_regs,restr,st.
    201 mk_state ERTL_semantics
    202   (sigma_frames prog f_lbls f_regs (st_frms ERTLptr_semantics st))
    203   (sigma_is prog f_lbls (istack … st))
    204   (carry … st)
    205   (sigma_regs prog f_lbls restr (regs … st))
    206   (sigma_mem prog f_lbls (m … st)).
    207    
    208 definition dummy_state_pc : state_pc ERTL_semantics ≝
    209 mk_state_pc ? dummy_state (null_pc one) (null_pc one).
    210 
    211 definition sigma_state_pc : ertl_program → lbl_funct → regs_funct →
    212 state_pc ERTLptr_semantics → state_pc ERTL_semantics ≝
    213 λprog,f_lbls,f_regs,st.
    214 let ge ≝ globalenv_noinit … prog in
    215 let globals ≝ prog_var_names … prog in
    216 match fetch_internal_function … ge (pc_block (pc … st)) with
    217   [ OK y ⇒ let 〈i,fn〉 ≝ y in
    218            let added ≝ added_registers ERTL globals fn
    219                                           (f_regs (pc_block (pc … st))) in
    220            mk_state_pc ?
    221            (sigma_state prog f_lbls f_regs added st)
    222                (pc … st) (sigma_stored_pc prog f_lbls (last_pop … st))
    223   | Error e ⇒ dummy_state_pc
    224   ].
    225 
    226 
    227 lemma ps_reg_retrieve_ok :  ∀prog : ertl_program.
    228 ∀f_lbls : lbl_funct. ∀r,restr.
    229 preserving1 ?? res_preserve1 …
    230      (sigma_regs prog f_lbls restr)
    231      (sigma_beval prog f_lbls)
    232      (λregs.ps_reg_retrieve regs r)
    233      (λregs.ps_reg_retrieve regs r).
    234 #prog #f_lbls #r #restr * #psd_r #hw_r whd in match ps_reg_retrieve;
    235 whd in match reg_retrieve; normalize nodelta @opt_to_res_preserve1
    236 whd in match sigma_regs; whd in match sigma_register_env; normalize nodelta
    237 >lookup_set_minus @if_elim [ #_ @opt_preserve_none1] #id_r_not_in
    238 >(lookup_map ?? RegisterTag ???) #bv #H @('bind_inversion H) -H #bv1
    239 #bv1_spec whd in ⊢ (??%? → ?); #EQ destruct %{bv1} % // >bv1_spec %
    240 qed.
    241 
    242 lemma hw_reg_retrieve_ok : ∀prog : ertl_program.
    243 ∀f_lbls : lbl_funct. ∀r,restr.
    244 preserving1 ?? res_preserve1 …
    245     (sigma_regs prog f_lbls restr)
    246     (sigma_beval prog f_lbls)
    247     (λregs.hw_reg_retrieve regs r)
    248     (λregs.hw_reg_retrieve regs r).
    249 #prog #f_lbls #r #restr * #psd_r * #hw_r #b whd in match hw_reg_retrieve;
    250 whd in match hwreg_retrieve; normalize nodelta whd in match sigma_regs;
    251 whd in match sigma_hw_register_env; normalize nodelta
    252 change with (sigma_beval prog f_lbls BVundef) in ⊢ (???????(??(?????%))?);
    253 #bv >lookup_map whd in ⊢ (???% → ?); #EQ destruct
    254 %{(lookup beval 6 (bitvector_of_register r) hw_r BVundef)}
    255 % //
    256 qed.
    257 
    258 
    259 lemma ps_reg_store_ok : ∀prog : ertl_program.
    260 ∀f_lbls : lbl_funct. ∀r,restr.
    261 ¬(r ∈ (set_from_list RegisterTag restr)) →
    262 preserving21 ?? res_preserve1 …
    263    (sigma_beval prog f_lbls)
    264    (sigma_regs prog f_lbls restr)
    265    (sigma_regs prog f_lbls restr)
    266    (ps_reg_store r)
    267    (ps_reg_store r).
    268 #prog #f_lbls #r #restr #Hreg whd in match ps_reg_store; normalize nodelta
    269 #bv * #psd_r #hw_r @mfr_bind1
    270 [ @(sigma_register_env prog f_lbls restr)
    271 | whd in match reg_store; whd in match sigma_regs; normalize nodelta
    272   #x #x_spec %{(add RegisterTag beval psd_r r bv)} % // whd in x_spec : (???%);
    273   destruct whd in match sigma_register_env; normalize nodelta >map_add
    274   >add_set_minus [% | assumption]
    275 | #z @mfr_return_eq1 %
    276 qed. 
    277 (* 
    278    lapply(update_ok_to_lookup ?????? x_spec) * * #_ #EQpsd #_
    279   lapply x_spec -x_spec lapply EQpsd -EQpsd whd in match sigma_register_env;
    280   normalize nodelta >lookup_set_minus @if_elim [ #_ * #H @⊥ @H %]
    281   #id_not_in #_ >update_set_minus [2: assumption] #H @('bind_inversion H) -H
    282   #x0 >map_update_commute #H @('bind_inversion H) -H #x1 #x1_spec
    283   whd in ⊢ (??%% → ??%% → ?); #EQ1 #EQ2 destruct %{x1} % //
    284 | #x * #psd_r' #hw_r' whd in match sigma_regs; normalize nodelta
    285   whd in ⊢ (???% → ?); #EQ destruct %{〈x,hw_r〉} % //
    286 ]
    287 qed.*)
    288 
    289 
    290 lemma hw_reg_store_ok : ∀prog : ertl_program.
    291 ∀f_lbls : lbl_funct. ∀r,restr.
    292 preserving21 ?? res_preserve1 …
    293    (sigma_beval prog f_lbls)
    294    (sigma_regs prog f_lbls restr)
    295    (sigma_regs prog f_lbls restr)
    296    (hw_reg_store r)
    297    (hw_reg_store r).
    298 #prog #sigma #r #restr whd in match hw_reg_store; normalize nodelta
    299 #bv * #psd_r * #hw_r #b whd in match hwreg_store; whd in match sigma_regs;
    300 normalize nodelta
    301 whd in match sigma_hw_register_env; normalize nodelta <insert_map * #psd_r'
    302 * #hw_r' #b' whd in ⊢ (???% → ?); #EQ destruct % [2: % [%] % |]
    303 qed.
    304 
    305 definition move_dst_not_fresh : list register →  move_dst → Prop ≝
    306 λrestr,mv.match mv with
    307   [PSD r ⇒ bool_to_Prop (¬(r ∈ (set_from_list RegisterTag restr)))
    308   | _ ⇒ True
    309   ].
    310 
    311 lemma ertl_eval_move_ok : ∀prog : ertl_program.
    312 ∀f_lbls : lbl_funct. ∀ restr,pm.
    313 move_dst_not_fresh restr (\fst pm) →
    314 preserving1 ?? res_preserve1 …
    315      (sigma_regs prog f_lbls restr)
    316      (sigma_regs prog f_lbls restr)
    317      (λregs.ertl_eval_move regs pm)
    318      (λregs.ertl_eval_move regs pm).
    319 #prog #sigma #restr * #mv_dst #arg_dst #Hpm #pm whd in match ertl_eval_move;
    320 normalize nodelta @mfr_bind1 [@(sigma_beval prog sigma)
    321 | cases arg_dst normalize nodelta
    322   [2: #b change with (return sigma_beval prog sigma (BVByte b)) in ⊢ (???????%?);
    323       @mfr_return1]
    324   * #r normalize nodelta [@ps_reg_retrieve_ok| @hw_reg_retrieve_ok]
    325 | #bv cases mv_dst in Hpm; #r #Hpm normalize nodelta [@ps_reg_store_ok assumption
    326                                                      | @hw_reg_store_ok
    327                                                      ]
    328 ]
    329 qed.
    330 
    331 lemma ps_arg_retrieve_ok : ∀prog : ertl_program.
    332 ∀f_lbls : lbl_funct. ∀a,restr.
    333 preserving1 ?? res_preserve1 …
    334     (sigma_regs prog f_lbls restr)
    335     (sigma_beval prog f_lbls)
    336     (λregs.ps_arg_retrieve regs a)
    337     (λregs.ps_arg_retrieve regs a).
    338 #prog #sigma #a #restr whd in match ps_arg_retrieve; normalize nodelta cases a -a
    339 normalize nodelta [#r | #b ] #regs
    340 [ @ps_reg_retrieve_ok
    341 | change with (return sigma_beval prog sigma (BVByte b)) in ⊢ (???????%?);
    342   @mfr_return1
    343 ]
    344 qed.
    345 
    346 lemma pop_ok :
    347 ∀prog : ertl_program.∀f_lbls : lbl_funct.
    348 ∀f_regs : regs_funct.∀restr.
    349 preserving1 ?? res_preserve1 ????
    350    (sigma_state prog f_lbls f_regs restr)
    351    (λx.let 〈bv,st〉 ≝ x in
    352       〈sigma_beval prog f_lbls bv,
    353        sigma_state prog f_lbls f_regs restr st〉)
    354    (pop ERTL_semantics)
    355    (pop ERTLptr_semantics).
    356 #prog #f_lbls #f_regs #id whd in match pop; normalize nodelta #st @mfr_bind1
    357 [@(λx.let 〈bv,is〉 ≝ x in
    358      〈sigma_beval prog f_lbls bv,
    359       sigma_is prog f_lbls is 〉)
    360 | whd in match is_pop; normalize nodelta whd in match sigma_state;
    361   normalize nodelta cases(istack ? st) normalize nodelta
    362   [@res_preserve_error1
    363   |2,3: #bv1 [2: #bv2] * #bv3 #is1 whd in ⊢ (??%% → ?); #EQ destruct
    364         % [2,4: % [1,3: %|*: %] |*:]
    365   ]
    366 | * #bv #is normalize nodelta @mfr_return_eq1 %   
    367 ]
    368 qed.
    369 
    370 lemma push_ok :
    371 ∀prog : ertl_program.
    372 ∀f_lbls : lbl_funct.
    373 ∀f_regs : regs_funct.∀restr.
    374 preserving21 ?? res_preserve1 …
    375      (sigma_state prog f_lbls f_regs restr)
    376      (sigma_beval prog f_lbls)
    377      (sigma_state prog f_lbls f_regs restr)
    378      (push ERTL_semantics)
    379      (push ERTLptr_semantics).
    380 #prog #f_lbls #f_regs #restr whd in match push; normalize nodelta #st #bv @mfr_bind1
    381 [ @(sigma_is prog f_lbls)
    382 | whd in match is_push; normalize nodelta whd in match sigma_state; normalize nodelta
    383  cases (istack ? st) [2,3: #bv [2: #bv']]  whd in match sigma_is in ⊢ (???????%?);
    384  normalize nodelta [@res_preserve_error1] @mfr_return_eq1 %
    385 | #is @mfr_return_eq1 %
    386 ]
    387 qed.
    388 
    389 lemma be_opaccs_ok :
    390 ∀prog : ertl_program. ∀f_lbls : lbl_funct. ∀ op.
    391 preserving21 ?? res_preserve1 ??????
    392     (sigma_beval prog f_lbls)
    393     (sigma_beval prog f_lbls)
    394     (λx.let 〈bv1,bv2〉 ≝ x in
    395            〈sigma_beval prog f_lbls bv1,
    396             sigma_beval prog f_lbls bv2〉)
    397     (be_opaccs op)
    398     (be_opaccs op).
    399 #prog #sigma #op #bv #bv1
    400 whd in match be_opaccs; 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; normalize nodelta
    405   try @res_preserve_error1 [ #x whd in ⊢ (???% → ?); #EQ destruct %{x} % //]
    406   whd in match sigma_beval; normalize nodelta cases (sigma_pc_opt ? ? ?)
    407   normalize nodelta [2: #pc] @res_preserve_error1
    408 | #by @mfr_bind1
    409   [ @(λx.x)
    410   | cases bv1
    411     [ | | #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc1 #p1]
    412     whd in match Byte_of_val; normalize nodelta
    413     try @res_preserve_error1 [ #x whd in ⊢ (???% → ?); #EQ destruct %{x} % //]
    414     whd in match sigma_beval; normalize nodelta cases (sigma_pc_opt ? ? ?)
    415     normalize nodelta [2: #pc] @res_preserve_error1
    416  | #by1 * #bv2 #bv3 cases(opaccs eval op by by1) #by' #by1' normalize nodelta
    417    whd in ⊢ (??%% → ?); #EQ destruct % [2: % [%] % |]
    418 qed.
    419 
    420 lemma be_op1_ok : ∀prog : ertl_program.  ∀f_lbls : lbl_funct.
    421 ∀ op.
    422 preserving1 ?? res_preserve1 …
    423      (sigma_beval prog f_lbls)
    424      (sigma_beval prog f_lbls)
    425      (be_op1 op)
    426      (be_op1 op).
    427 #prog #sigma #o #bv whd in match be_op1; normalize nodelta @mfr_bind1
    428 [ @(λx.x)
    429 | cases bv
    430   [ | | #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc1 #p1]
    431   whd in match Byte_of_val; whd in match sigma_beval; normalize nodelta
    432   try @res_preserve_error1 [ @mfr_return_eq1 %]
    433   cases(sigma_pc_opt prog sigma pc1) [2: #pc2] normalize nodelta
    434   @res_preserve_error1
    435 | #by @mfr_return_eq1 %
    436 ]
    437 qed.
    438 
    439 
    440 lemma be_op2_ok : ∀prog : ertl_program. ∀f_lbls : lbl_funct.
    441 ∀ b,op.
    442 preserving21 ?? res_preserve1 …
    443      (sigma_beval prog f_lbls)
    444      (sigma_beval prog f_lbls)
    445      (λx.let 〈bv,b〉≝ x in 〈sigma_beval prog f_lbls bv,b〉)
    446      (be_op2 b op)
    447      (be_op2 b op).
    448 #prog #sigma #b #op #bv #bv1 whd in match be_op2; normalize nodelta
    449 cases bv
    450 [ | | #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc1 #p1]
    451 normalize nodelta [@res_preserve_error1] whd in match sigma_beval;
    452 normalize nodelta
    453 cases bv1
    454 [1,2,8,9,15,16,22,23,29,30,36,37:
    455 |3,10,17,24,31,38: #ptr1' #ptr2' #p'
    456 |4,11,18,25,32,39: #by'
    457 |5,12,19,26,33,40: #p'
    458 |6,13,20,27,34,41: #ptr' #p'
    459 |7,14,21,28,35,42: #pc1' #p1'
    460 ]
    461 normalize nodelta try @res_preserve_error1
    462 [4,5,8,13,16,20,21,22,23,24,25,26 : @res_preserve_error11 %
    463    [2,4,6,8,10,12,14,16,18,20,22,24: cases(sigma_pc_opt ???) try % #pc2 %
    464    |*:]
    465 |*: cases op normalize nodelta
    466     try @res_preserve_error1 try( @mfr_return_eq1 %)
    467     [1,2,12,13,16,17,18: @if_elim #_ try @res_preserve_error1
    468                          try( @mfr_return_eq1 %)
    469                          [ @if_elim #_ @mfr_return_eq1 %
    470                          | cases(ptype ptr) normalize nodelta
    471                            [2: @res_preserve_error1] @mfr_bind1
    472                            [ @(λx.x)
    473                            | whd in match Bit_of_val; normalize nodelta
    474                              cases b [#bo|| #bo #ptr'' #p'' #bit_v]
    475                              normalize nodelta [2,3: @res_preserve_error1]
    476                              @mfr_return_eq1 %
    477                            | #bi cases(op2 ?????) #by #bi1 normalize nodelta
    478                              @mfr_return_eq1 %
    479                            ]
    480                          | cases(ptype ptr) normalize nodelta @res_preserve_error1
    481                          ]
    482     |3,4,5,6,7,8: @mfr_bind1
    483         [1,4,7,10,13,16: @(λx.x)
    484         |2,5,8,11,14,17: whd in match Bit_of_val; normalize nodelta
    485                          cases b [1,4,7,10,13,16: #bo|
    486                                  |2,5,8,11,14,17:
    487                                  |3,6,9,12,15,18: #bo #ptr'' #p'' #bit_v
    488                                  ] normalize nodelta try @res_preserve_error1
    489                                  @mfr_return_eq1 %
    490        |3,6,9,12,15,18: #bi try(@mfr_return_eq1 %) cases(op2 ?????) #by #bi1 normalize nodelta
    491                         @mfr_return_eq1 %
    492        ]
    493     |*: whd in match be_add_sub_byte; normalize nodelta
    494         [1,2,3: cases(ptype ptr) normalize nodelta [2,4,6: @res_preserve_error1]
    495                 cases p * [2,4,6: #p_no] #prf normalize nodelta
    496                 [@res_preserve_error1
    497                 |2,3: cases b [1,4: #bo|2,5: |3,6:  #bo #ptr'' #p'' #bit_v]
    498                       normalize nodelta [1,2,3,4: @res_preserve_error1]
    499                       @if_elim #_ [2,4: @res_preserve_error1]
    500                       @If_elim #INUTILE [2,4: @res_preserve_error1]
    501                       @pair_elim #a1 #a2 #_ normalize nodelta
    502                       @mfr_return_eq1 %
    503                 |*: @mfr_bind1
    504                   [1,4,7: @(λx.x)
    505                   |2,5,8: whd in match Bit_of_val; normalize nodelta
    506                           [@mfr_return_eq1 %] cases b
    507                           [1,4: #bo|2,5: |3,6:  #bo #ptr'' #p'' #bit_v]
    508                           normalize nodelta [3,4,5,6: @res_preserve_error1]
    509                           @mfr_return_eq1 %
    510                   |3,6,9: * normalize nodelta [1,3,5: @res_preserve_error1]
    511                           cases(op2 ?????) #a1 #a2 normalize nodelta
    512                           @mfr_return_eq1 %
    513                   ]
    514                ]
    515          |*: cases(ptype ptr') normalize nodelta [2,4: @res_preserve_error1]
    516              cases p' * [2,4: #part_no] #prf normalize nodelta
    517              [ @res_preserve_error1
    518              | cases b [#bo|| #bo #ptr'' #p'' #bit_v]
    519                normalize nodelta [1,2: @res_preserve_error1] @if_elim #_
    520                [2: @res_preserve_error1] @If_elim #INUTILE [2: @res_preserve_error1]
    521                @pair_elim #a1 #a2 #_ normalize nodelta @mfr_return_eq1 %
    522              |*: @mfr_bind1
    523                 [1,4: @(λx.x)
    524                 |2,5: whd in match Bit_of_val; normalize nodelta [ @mfr_return_eq1 %]
    525                       cases b [#bo|| #bo #ptr'' #p'' #bit_v] normalize nodelta
    526                       [2,3: @res_preserve_error1] @mfr_return_eq1 %
    527                 |3,6: * normalize nodelta [1,3: @res_preserve_error1]   
    528                       cases(op2 ?????) #a1 #a2 normalize nodelta
    529                       @mfr_return_eq1 %
    530                 ]
    531               ]
    532           ]
    533       ]
    534 ]
    535 qed.
    536 
    537 lemma pointer_of_address_ok : ∀prog : ertl_program.∀f_lbls : lbl_funct.
    538 preserving1 … res_preserve1 …
    539      (λx.let 〈bv1,bv2〉 ≝ x in〈sigma_beval prog f_lbls bv1,
    540            sigma_beval prog f_lbls bv2〉)
    541      (λx.x)
    542      pointer_of_address pointer_of_address.
    543 #prog #sigma * #bv1 #bv2 whd in match pointer_of_address;
    544 whd in match pointer_of_bevals; normalize nodelta
    545 cases bv1 normalize nodelta
    546 [ | | #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc1 #p1]
    547 try @res_preserve_error1
    548 [ cases bv2 [ | | #ptr1' #ptr2' #p' | #by' | #p' | #ptr' #p' | #pc1' #p1']
    549   normalize nodelta
    550   [1,2,3,4,5: @res_preserve_error1
    551   | @if_elim #_ [ @mfr_return_eq1 % | @res_preserve_error1]
    552   ]
    553 ] whd in match sigma_beval; normalize nodelta cases(sigma_pc_opt ???)
    554   [2,4: #pc4] normalize nodelta @res_preserve_error1
    555 qed.
    556 
    557 lemma beloadv_ok : ∀prog : ertl_program. ∀f_lbls : lbl_funct.
    558 ∀ptr.
    559 preserving1 … opt_preserve1 …
    560      (sigma_mem prog f_lbls)
    561      (sigma_beval prog f_lbls)
    562      (λm.beloadv m ptr)
    563      (λm.beloadv m ptr).
    564 #prog #sigma #ptr #mem whd in match beloadv; whd in match do_if_in_bounds;
    565 normalize nodelta @if_elim [2: #_ @opt_preserve_none1]
    566 whd in match sigma_mem in ⊢ (% → ?); normalize nodelta #Hzlb
    567 @if_elim [2: #_ @opt_preserve_none1] whd in match sigma_mem in ⊢ (% → ?);
    568 normalize nodelta @If_elim [2: >Hzlb * #H @⊥ @H %] #_ @andb_elim @if_elim
    569 [2: #_ *] #Hzleb #Hzlb' >Hzlb normalize nodelta >Hzlb' normalize nodelta
    570 @mfr_return_eq1 whd in match sigma_mem; normalize nodelta >Hzlb
    571 @If_elim [2: * #H @⊥ @H %] * >Hzleb >Hzlb' @If_elim [2: * #H @⊥ @H %]
    572 * %
    573 qed.
    574 
    575 lemma bestorev_ok : ∀prog : ertl_program.∀f_lbls : lbl_funct.
    576 ∀ptr.
    577 preserving21 … opt_preserve1 …
    578     (sigma_mem prog f_lbls)
    579     (sigma_beval prog f_lbls)
    580     (sigma_mem prog f_lbls)
    581     (λm.bestorev m ptr)
    582     (λm.bestorev m ptr).
    583 #prog #sigma #ptr #mem #bv whd in match bestorev; whd in match do_if_in_bounds;
    584 normalize nodelta @if_elim [2: #_ @opt_preserve_none1]
    585 whd in match sigma_mem in ⊢ (% → ?); normalize nodelta #Hzlb
    586 @if_elim [2: #_ @opt_preserve_none1] @andb_elim @if_elim [2: #_ *]
    587 whd in match sigma_mem in ⊢ (% → % → ?); normalize nodelta >Hzlb
    588 @If_elim [2: * #H @⊥ @H %] * #Hzleb #Hzlb' normalize nodelta >Hzleb
    589 >Hzlb' normalize nodelta @mfr_return_eq1 whd in ⊢ (???%); @eq_f @mem_ext_eq
    590 [ #bl normalize nodelta % [%]
    591   [ whd in match sigma_mem; normalize nodelta >Hzlb @If_elim [2: * #H @⊥ @H %] *
    592     whd in match update_block; normalize nodelta @if_elim
    593     [ @eq_block_elim [2: #_ *] #EQbl * >EQbl >Hzlb @If_elim [2: * #H @⊥ @H %]
    594       * whd in match low_bound; normalize nodelta @if_elim [ #_ %]
    595       @eq_block_elim #_ * %
    596     | @eq_block_elim [#_ *] * #Hbl * @If_elim
    597       [ #Hzlb'' >Hzlb'' @If_elim [2: * #H @⊥ @H %] * whd in match low_bound;
    598         normalize nodelta @if_elim [2: #_ %] @eq_block_elim [2: #_ *] #H @⊥ @Hbl
    599         assumption
    600       | #Hzlb'' >Hzlb'' @If_elim [*] #_ %
    601       ]
    602    ]
    603  | whd in match update_block; whd in match sigma_mem; normalize nodelta
    604    @if_elim @eq_block_elim [2,3: #_ * |4: *] #Hbl #_ @If_elim
    605    [3,4: >Hbl >Hzlb * [2: #H @⊥ @H %] @If_elim [2: * #H @⊥ @H %] *
    606         whd in match high_bound; normalize nodelta @if_elim [#_ %]
    607         @eq_block_elim [ #_ *] * #H @⊥ @H %
    608    | #Hzlb'' >Hzlb'' @If_elim [2: * #H @⊥ @H %] * whd in match high_bound;
    609      normalize nodelta @if_elim [2: #_ %] @eq_block_elim [2: #_ *]
    610      #H @⊥ @Hbl assumption
    611   | #Hzlb'' >Hzlb'' @If_elim [*] #_ %
    612   ]
    613  | #z whd in match update_block; whd in match sigma_mem; normalize nodelta
    614    @if_elim @eq_block_elim [2,3: #_ * |4: *] #Hbl #_
    615    [ @If_elim #Hzlb'' >Hzlb'' [2: @If_elim * #_ %] @If_elim @andb_elim
    616      @if_elim [2: #_ *] #Hzleb' #Hzlb'''
    617      [ @If_elim [2: * #H @⊥ @H %] * whd in match low_bound; normalize nodelta
    618        @If_elim @andb_elim @if_elim [2: #_ *] @if_elim
    619        [1,3,5: @eq_block_elim [2,4,6: #_ *] #H @⊥ @Hbl assumption] #_ >Hzleb' *
    620        whd in match high_bound; normalize nodelta @if_elim
    621        [1,3: @eq_block_elim [2,4: #_ *] #H @⊥ @Hbl assumption] #_ >Hzlb'''
    622        [ * %] * #H @⊥ @H %
    623      | @If_elim * [2: #H @⊥ @H %] whd in match low_bound; normalize nodelta
    624        @if_elim [@eq_block_elim [2: #_ *] #H @⊥ @Hbl assumption] #_
    625        >Hzleb' whd in match high_bound; normalize nodelta @if_elim
    626        [@eq_block_elim [2: #_ *] #H @⊥ @Hbl assumption] #_ >Hzlb'''
    627        @If_elim [2: #_ %] *
    628      | @If_elim [2: * #H @⊥ @H %] whd in match low_bound; normalize nodelta @if_elim
    629        [@eq_block_elim [2: #_ *] #H @⊥ @Hbl assumption] #_ #_
    630        whd in match low_bound in Hzleb'; normalize nodelta in Hzleb';
    631        whd in match high_bound; normalize nodelta @if_elim
    632        [@eq_block_elim [2: #_ *] #H @⊥ @Hbl assumption] #_ @If_elim [2: #_ %]
    633        @andb_elim @if_elim [2: #_ *] #H >H in Hzleb'; *
    634      ]
    635    | whd in ⊢ (??%?); @if_elim @eqZb_elim [2,3: #_ * |4: *] #Hz *
    636        [ >Hzlb @If_elim [2: * #H @⊥ @H %] * @If_elim @andb_elim @if_elim
    637           [2: #_ *] #Hzleb' #Hzlb'' >Hbl >Hzlb @If_elim [2,4,6: * #H @⊥ @H %] #_
    638           whd in match low_bound; normalize nodelta @eq_block_elim
    639           [2,4,6: * #H @⊥ @H %] #_ normalize nodelta whd in match high_bound;
    640           normalize nodelta @eq_block_elim [2,4,6: * #H @⊥ @H %]
    641           #_ normalize nodelta
    642           [1,2: >Hzleb' >Hzlb'' @If_elim [2,3: * #H @⊥ @H %]
    643                 #_ [2: %] whd in ⊢ (???(???%)); @if_elim [2: #_ %]
    644                 @eqZb_elim [2: #_ *] #H @⊥ @Hz assumption
    645           | @If_elim [2: #_ %] @andb_elim @if_elim [2: #_ *] #H >H in Hzleb'; *
    646           ]
    647        | >Hbl >Hzlb @If_elim [2: * #H @⊥ @H %] * whd in match low_bound;
    648          normalize nodelta @eq_block_elim [2: * #H @⊥ @H %] #_ normalize nodelta
    649          whd in match high_bound; normalize nodelta @eq_block_elim [2: * #H @⊥ @H %]
    650          normalize nodelta >Hz >Hzleb >Hzlb' @If_elim [2: * #H @⊥ @H %] #_ #_
    651          whd in ⊢ (???(???%)); @eqZb_elim [2: * #H @⊥ @H %] #_ %
    652        ]
    653     ]
    654  ]
    655 | %
    656 ]
    657 qed.
    658 
    659 
    660 lemma sp_ok : ∀prog : ertl_program.
    661 ∀f_lbls : lbl_funct.
    662 ∀f_regs : regs_funct.∀restr.
    663    preserving1 … res_preserve1 …
    664       (λst.sigma_state prog f_lbls f_regs restr st)
    665       (λx.x)
    666       (sp ERTL_semantics)
    667       (sp ERTLptr_semantics).
    668 #prog #f_lbls #f_regs #restr #st whd in match sp; normalize nodelta
    669 whd in match (load_sp ??); whd in match (load_sp ??); whd in match sigma_state;
    670 normalize nodelta whd in match sigma_regs; normalize nodelta
    671 cases(regs ? st) #psd_r #hw_r normalize nodelta
    672 inversion(pointer_of_address ?) normalize nodelta [2: #e #_ @res_preserve_error1]
    673 #pt #EQ lapply(jmeq_to_eq ??? EQ) -EQ whd in match hwreg_retrieve; normalize nodelta
    674 whd in match sigma_hw_register_env; normalize nodelta
    675 change with (sigma_beval prog f_lbls BVundef) in ⊢ (??(?(???(?????%)(?????%)))? → ?);
    676 >lookup_map >lookup_map
    677 cases(lookup beval 6 (bitvector_of_register RegisterSPL) (reg_env hw_r) BVundef)
    678 [ | | #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc1 #p1]
    679 whd in match pointer_of_address; whd in match pointer_of_bevals; normalize nodelta
    680 [1,2,3,4,5: #ABS destruct
    681 | cases(lookup beval 6 (bitvector_of_register RegisterSPH) (reg_env hw_r) BVundef)
    682   [ | | #ptr1' #ptr2' #p' | #by' | #p' | #ptr' #p' | #pc1' #p1']
    683   whd in match sigma_beval; normalize nodelta
    684   [1,2,3,4,5: #ABS destruct
    685   | @if_elim [2: #_ #ABS destruct] #H whd in ⊢ (??%? → ?); #EQ destruct
    686     normalize nodelta @match_reg_elim #INUTILE
    687     [ @mfr_return_eq1 % | @res_preserve_error1 ]
    688   | cases (sigma_pc_opt ? ? ?) normalize nodelta [2: #x] #EQ destruct
    689   ]
    690 | whd in match sigma_beval; normalize nodelta cases(sigma_pc_opt ? ? ?)
    691  normalize nodelta [2: #x] #EQ destruct
    692 ]
    693 qed.
    694 
    695 lemma set_sp_ok :  ∀prog : ertl_program.
    696 ∀f_lbls : lbl_funct.
    697 ∀f_regs : regs_funct.∀restr.∀ptr,st.
    698 set_sp ? ptr (sigma_state prog f_lbls f_regs restr st) =
    699 sigma_state prog f_lbls f_regs restr (set_sp ? ptr st).
    700 #prog #f_lbls #f_regs #restr #ptr #st whd in match set_sp; whd in match sigma_state;
    701 normalize nodelta @eq_f2 [2: %] whd in match (save_sp ???);
    702 whd in match (save_sp ???); whd in match sigma_regs; normalize nodelta
    703 cases(regs ? st) #psd_env #hw_regs normalize nodelta @eq_f
    704 whd in match hwreg_store_sp; normalize nodelta whd in match sigma_hw_register_env;
    705 normalize nodelta whd in match hwreg_store; normalize nodelta @eq_f2 [2: %]
    706 >insert_map @eq_f >insert_map %
    707 qed.
    708 
    709 (*TO BE MOVED IN TranslateUtils.ma *)
    710 include "utilities/listb_extra.ma".
    711 lemma not_in_added_registers : ∀p : graph_params.
    712 ∀globals : list ident.∀fn,f_regs,r.
    713 (∀lbl. code_has_label p globals (joint_if_code … fn) lbl →
    714        opt_All … (λl.¬(bool_to_Prop (r ∈ l))) (f_regs lbl)) →
    715 ¬ (r ∈ (set_from_list RegisterTag (added_registers p globals fn f_regs))).
    716 #p #globals #fn #f_regs #r #H whd in match added_registers; normalize nodelta
    717 @foldi_ind [@I] #lbl #labels_fn #stmt #regs * #lbl_not_in_fn #EQstmt #IH
    718 lapply(Prop_notb … IH) -IH * #IH
    719 lapply(H lbl ?)
    720  [whd in match code_has_label; whd in match code_has_point; normalize nodelta
    721   whd in match (stmt_at ????); >EQstmt @I] cases(f_regs lbl)
    722   [ #_ @notb_Prop % assumption]
    723 #l whd in ⊢ (% → ?); normalize nodelta * #H1 @notb_elim @if_elim [2: #_ @I] #ABS
    724 lapply(mem_list_as_set … ABS) #ABS' cases(Exists_append … ABS') #ABS''
    725 [ @H1 @Exists_memb lapply ABS'' elim l [ *] #hd #tl #IH whd in ⊢ (% → %);
    726   * [ #EQ >EQ % %] #H %2 @IH @H
    727 | @IH @list_as_set_mem assumption
    728 ]
    729 qed.
    730 
    731 include alias "basics/lists/listb.ma".
    732 
    733 (*RIFARE!!!*)
    734 lemma eval_seq_no_pc_no_call_ok :
    735 ∀prog : ertl_program.
    736 let trans_prog ≝ ertl_to_ertlptr prog in
    737 ∀f_lbls : lbl_funct. ∀f_regs : regs_funct.
    738 ∀stack_size.
    739 ∀bl.∀id. ∀fn : (joint_closed_internal_function ? (prog_var_names ?? prog)).
    740 ∀fn_out : (joint_closed_internal_function ? (prog_var_names ?? trans_prog)).
    741 ∀seq.
    742 (∀l. code_has_label … (joint_if_code … fn) l → 
    743 opt_All …
    744        (λlabs.(All … (λreg.bool_to_Prop(¬(reg ∈ labs)))
    745               (get_used_registers_from_seq … (functs … ERTL) seq)))
    746        (f_regs bl l))  →
    747    preserving1 ?? res_preserve1 ????
    748       (sigma_state prog f_lbls f_regs (added_registers … fn (f_regs bl)))
    749       (sigma_state prog f_lbls f_regs (added_registers … fn (f_regs bl)))
    750       (eval_seq_no_pc ERTL_semantics
    751              (globals (mk_prog_params ERTL_semantics prog stack_size))
    752              (ev_genv (mk_prog_params ERTL_semantics prog stack_size)) id fn seq)
    753       (eval_seq_no_pc ERTLptr_semantics
    754              (globals (mk_prog_params ERTLptr_semantics trans_prog stack_size))
    755              (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_size))
    756              id fn_out (seq_embed … seq)).
    757 #prog #f_lbls #f_regs #stack_size #bl #f #fn #fn_out #seq #fresh_regs
    758 cases seq in fresh_regs;
    759 [ #c #_ #st @mfr_return1
    760 | #pm #fesh_regs #st whd in match pair_reg_move; normalize nodelta
    761   @mfr_bind1
    762   [ 2: change with (ertl_eval_move ??) in ⊢ (???????%%); @ertl_eval_move_ok
    763        whd in match move_dst_not_fresh; normalize nodelta cases pm in fesh_regs;
    764        * [#r1 | #R1] #m_src [2: #_ @I] normalize nodelta #fresh_regs
    765        @not_in_added_registers #lbl #Hlbl lapply(fresh_regs lbl Hlbl)
    766        cases(f_regs bl lbl) [ #_ @I] #labs whd in ⊢ (% → %); * #H #_ @Prop_notb @H
    767   | | #regs  @mfr_return_eq1 %
    768   ]
    769 | #r #fresh_regs #st @mfr_bind1
    770   [2:  @pop_ok |
    771   | * #bv #st whd in match acca_store; normalize nodelta @mfr_bind1
    772     [2: @ps_reg_store_ok @not_in_added_registers #lbl #Hlbl
    773        lapply(fresh_regs lbl Hlbl)
    774        cases(f_regs bl lbl) [ #_ @I] #labs whd in ⊢ (% → %); * #H #_ @Prop_notb @H |
    775     | #regs  @mfr_return_eq1 %
    776     ]
    777   ]
    778 | #r #_ #st @mfr_bind1
    779   [2: whd in match acca_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok |
    780   | #bv @push_ok
    781   ]
    782 | #i
    783   #i_spec
    784   change with ((dpl_reg ERTL) → ?)
    785   #dpl
    786   change with ((dph_reg ERTL) → ?)
    787   #dph #fresh_regs #st @mfr_bind1
    788   [ @(sigma_state prog f_lbls f_regs (added_registers … fn (f_regs bl)))
    789   | whd in match dpl_store; normalize nodelta @mfr_bind1
    790     [2: @opt_safe_elim #bl #EQbl
    791        @opt_safe_elim #bl'
    792        >(find_symbol_transf …
    793           (λvars.transf_fundef … (λfn.(b_graph_translate … fn))) prog i) in ⊢ (%→?);
    794        >EQbl #EQ destruct whd in match sigma_state; normalize nodelta       
    795        change with (sigma_beval prog f_lbls (BVptr …))
    796                                                in ⊢ (???????(?????%?)?);
    797        @ps_reg_store_ok @not_in_added_registers #lbl #Hlbl lapply(fresh_regs lbl Hlbl)
    798        cases(f_regs bl lbl) [ #_ @I] #labs whd in ⊢ (% → %); * #H #_ @Prop_notb @H |
    799     | #regs  @mfr_return_eq1 %
    800     ]
    801   | #st1 @opt_safe_elim #bl #EQbl @opt_safe_elim #bl'   
    802    >(find_symbol_transf …
    803           (λvars.transf_fundef … (λfn.(b_graph_translate … fn))) prog i) in ⊢ (%→?);
    804     >EQbl #EQ destruct whd in match dph_store; normalize nodelta @mfr_bind1
    805     [2: whd in match sigma_state; normalize nodelta       
    806        change with (sigma_beval prog f_lbls (BVptr …))
    807                                                in ⊢ (???????(?????%?)?);
    808       @ps_reg_store_ok @not_in_added_registers #lbl #Hlbl lapply(fresh_regs lbl Hlbl)
    809        cases(f_regs bl lbl) [ #_ @I] #labs whd in ⊢ (% → %); * #_ whd in ⊢ (% → ?); * #H
    810        #_ @Prop_notb @H|
    811     | #regs  @mfr_return_eq1 %
    812     ]
    813   ]     
    814 | #op #a #b #arg1 #arg2 #fresh_regs #st @mfr_bind1
    815   [2: whd in match acca_arg_retrieve; whd in match sigma_state; normalize nodelta
    816      @ps_arg_retrieve_ok |
    817   | #bv1 @mfr_bind1
    818    [2: whd in match accb_arg_retrieve; whd in match sigma_state; normalize nodelta
    819       @ps_arg_retrieve_ok |
    820    | #bv2 @mfr_bind1
    821      [2: @be_opaccs_ok |
    822      | * #bv3 #bv4 normalize nodelta @mfr_bind1
    823        [ @(sigma_state prog f_lbls f_regs (added_registers … fn (f_regs bl)))
    824        | whd in match acca_store; normalize nodelta @mfr_bind1
    825          [2: @ps_reg_store_ok @not_in_added_registers #lbl #Hlbl
    826              lapply(fresh_regs lbl Hlbl)
    827              cases(f_regs bl lbl) [ #_ @I] #labs whd in ⊢ (% → %); * #H #_ @Prop_notb @H |
    828          | #regs  @mfr_return_eq1 %
    829          ]
    830        | #st1 whd in match accb_store; normalize nodelta @mfr_bind1
    831          [2: whd in match sigma_state; normalize nodelta
    832             @ps_reg_store_ok @not_in_added_registers #lbl #Hlbl
    833             lapply(fresh_regs lbl Hlbl)
    834             cases(f_regs bl lbl) [ #_ @I] #labs whd in ⊢ (% → %); * #_ * #H #_
    835             @Prop_notb @H |
    836          | #regs  @mfr_return_eq1 %
    837          ]         
    838        ]
    839      ]
    840    ]
    841   ] 
    842 | #op #r1 #r2 #fresh_regs #st @mfr_bind1
    843   [ @(sigma_beval prog f_lbls)
    844   | whd in match acca_retrieve; normalize nodelta @ps_reg_retrieve_ok
    845   | #bv1 @mfr_bind1
    846     [ @(sigma_beval prog f_lbls)
    847     | @be_op1_ok
    848     | #bv2 whd in match acca_store; normalize nodelta @mfr_bind1
    849       [2: whd in match sigma_state; normalize nodelta @ps_reg_store_ok
    850           @not_in_added_registers #lbl #Hlbl lapply(fresh_regs lbl Hlbl)
    851        cases(f_regs bl lbl) [ #_ @I] #labs whd in ⊢ (% → %); * #H #_ @Prop_notb @H |
    852       | #regs  @mfr_return_eq1 %
    853       ]
    854     ]
    855   ]
    856 | #op2 #r1 #r2 #arg #fresh_regs #st @mfr_bind1
    857   [2: whd in match acca_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok |
    858   | #bv @mfr_bind1
    859     [2: whd in match snd_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok |
    860     | #bv1 @mfr_bind1
    861       [2: @be_op2_ok |
    862       | * #bv2 #b @mfr_bind1
    863         [ @(sigma_state prog f_lbls f_regs (added_registers … fn (f_regs bl)))
    864         | whd in match acca_store; normalize nodelta @mfr_bind1
    865           [2: whd in match sigma_state; normalize nodelta @ps_reg_store_ok
    866               @not_in_added_registers #lbl #Hlbl lapply(fresh_regs lbl Hlbl)
    867               cases(f_regs bl lbl) [ #_ @I] #labs whd in ⊢ (% → %); * #H #_ @Prop_notb @H |
    868           | #regs  @mfr_return_eq1 %
    869           ]
    870         | #st1 @mfr_return_eq1 %
    871         ]
    872       ]
    873     ]
    874   ]
    875 | #_ #st @mfr_return_eq1 %
    876 | #_ #st @mfr_return_eq1 %
    877 | #r1 #dpl #dph #fresh_regs #st @mfr_bind1
    878   [2: whd in match dph_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok |
    879   | #bv @mfr_bind1
    880     [2: whd in match dpl_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok |
    881     | #bv1 @mfr_bind1
    882       [ @(λx.x)
    883       | @(pointer_of_address_ok ? ? 〈bv1,bv〉)
    884       | #ptr @mfr_bind1
    885         [2: @opt_to_res_preserve1 @beloadv_ok |
    886         | #bv2 whd in match acca_store; normalize nodelta @mfr_bind1
    887           [2: whd in match sigma_state; normalize nodelta @ps_reg_store_ok
    888               @not_in_added_registers #lbl #Hlbl lapply(fresh_regs lbl Hlbl)
    889               cases(f_regs bl lbl) [ #_ @I] #labs whd in ⊢ (% → %); * #H #_ @Prop_notb @H |
    890           | #regs  @mfr_return_eq1 %
    891           ]
    892         ] 
    893       ]
    894     ]
    895   ] 
    896 | #dpl #dph #r #_ #st @mfr_bind1
    897   [2: whd in match dph_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok |
    898   | #bv @mfr_bind1
    899     [2: whd in match dpl_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok |
    900     | #bv1 @mfr_bind1
    901       [ @(λx.x)
    902       |  @(pointer_of_address_ok ? ? 〈bv1,bv〉)
    903       | #ptr @mfr_bind1
    904         [2: whd in match acca_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok |
    905         | #bv2 @mfr_bind1
    906           [2: @opt_to_res_preserve1 @bestorev_ok |
    907           | #m @mfr_return_eq1 %
    908           ]
    909         ]
    910       ]
    911     ]
    912   ]
    913 | #ext #fresh_regs #st whd in ⊢ (???????%%); whd in match (stack_sizes ????); cases (stack_size f)
    914   normalize nodelta
    915   [ @res_preserve_error1
    916   | #n cases ext in fresh_regs; normalize nodelta
    917     [1,2: #_ @mfr_bind1
    918       [1,4: @(λx.x)
    919       |2,5: @sp_ok
    920       |3,6: #ptr @mfr_return_eq1 >set_sp_ok %
    921       ]
    922     | #r #fresh_regs whd in match ps_reg_store_status; normalize nodelta @mfr_bind1
    923       [2: whd in match sigma_state; normalize nodelta
    924           change with (sigma_beval prog f_lbls (BVByte ?))
    925                in ⊢ (???????(??%?)?);
    926           @ps_reg_store_ok @not_in_added_registers #lbl #Hlbl lapply(fresh_regs lbl Hlbl)
    927           cases(f_regs bl lbl) [ #_ @I] #labs whd in ⊢ (% → %); * #H #_ @Prop_notb @H
    928       |
    929       | #regs @mfr_return_eq1 %
    930       ]
    931     ]
    932   ]     
    933 ]
    934 qed.
    935 
    936 lemma partial_inj_sigma : ∀ prog : ertl_program.
    937 ∀f_lbls : lbl_funct.
    938 let sigma ≝ get_sigma prog f_lbls in
    939 ∀id,lbl1,lbl2. sigma id lbl1 ≠ None ? → sigma id lbl1 = sigma id lbl2 → lbl1 = lbl2.
    940 #prog #good #bl #lbl1 #lbl2 inversion(get_sigma … lbl1)
    941 [#_ * #H @⊥ @H %] #lbl1' whd in match get_sigma; normalize nodelta
    942 #H @('bind_inversion H) -H #bl' whd in match code_block_of_block; normalize nodelta
    943 @match_reg_elim [#_ #ABS destruct] #prf #EQ destruct #H @('bind_inversion H) -H
    944 * #id #fn #H lapply(res_eq_from_opt ??? H) -H #EQfn #H @('bind_inversion H) -H
    945 * #lbl1'' #stmt1 #H1 whd in ⊢ (??%? → ?); #EQ destruct
    946 #_ #H lapply(sym_eq ??? H) -H >m_return_bind >EQfn >m_return_bind
    947 #H @('bind_inversion H) -H * #lbl2' #stmt2 #H2
    948 whd in ⊢ (??%? → ?); #EQ destruct lapply(find_predicate ?????? H1)
    949 lapply(find_predicate ?????? H2) cases(good ??) normalize nodelta [*]
    950 *
    951   [ normalize nodelta @eq_identifier_elim #EQ1 *
    952     @eq_identifier_elim #EQ2 * >EQ1 >EQ2 %
    953   | #lb #tl whd in match split_on_last; normalize nodelta whd in match (foldr ?????);
    954     cases( foldr label (option (list label×label)) … tl) normalize nodelta
    955     [2: * #x #lb1] @eq_identifier_elim #EQ1 * @eq_identifier_elim #EQ2 *
    956     >EQ1 >EQ2 %
    957   ]
    958 qed.
    959 
    960 lemma pc_of_label_eq :
    961   ∀p,p'.let pars ≝ mk_sem_graph_params p p' in
    962   ∀globals,ge,bl,i_fn,lbl.
    963   fetch_internal_function ? ge bl = return i_fn →
    964   pc_of_label pars globals ge bl lbl =
    965     OK ? (pc_of_point ERTL_semantics bl lbl).
    966 #p #p' #globals #ge #bl #i_fn #lbl #EQf
    967 whd in match pc_of_label;
    968 normalize nodelta >EQf >m_return_bind %
    969 qed.
    970 
    971 lemma pop_ra_ok :
    972 ∀prog : ertl_program.
    973 ∀f_lbls : lbl_funct. ∀f_regs : regs_funct.
    974 ∀restr.
    975 preserving1 … res_preserve1 …
    976      (sigma_state prog f_lbls f_regs restr)
    977      (λx.let 〈st,pc〉 ≝ x in
    978        〈sigma_state prog f_lbls f_regs restr st,
    979         sigma_stored_pc prog f_lbls pc〉)
    980      (pop_ra ERTL_semantics)
    981      (pop_ra ERTLptr_semantics).   
    982 #prog #f_lbls #f_regs #restr1 #st whd in match pop_ra; normalize nodelta
    983 @mfr_bind1
    984 [ | @pop_ok ] * #bv #st1 @mfr_bind1 [ | @pop_ok] * #bv1 #st2 @mfr_bind1
    985 [ @(sigma_stored_pc prog f_lbls)
    986 | whd in match pc_of_bevals; normalize nodelta
    987   cases bv [ | | #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc #p]
    988   whd in match sigma_beval; normalize nodelta try @res_preserve_error1
    989   inversion(sigma_pc_opt ? ? ?) normalize nodelta [ #_ @res_preserve_error1]
    990   #sigma_pc #sigma_pc_spec normalize nodelta cases bv1
    991   [ | | #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc1 #p1]
    992   normalize nodelta try @res_preserve_error1
    993   inversion(sigma_pc_opt ? ? ?) normalize nodelta [#_ @res_preserve_error1]
    994   #sigma_pc1 #sigma_pc1_spec @if_elim [2: #_ @res_preserve_error1]
    995   @andb_elim @if_elim [2: #_ *] @andb_elim @if_elim [2: #_ *]
    996   #_ #H >H @eq_program_counter_elim [2: #_ *]
    997   #EQspc * @eq_program_counter_elim
    998   [#_ normalize nodelta @mfr_return_eq1 whd in match sigma_stored_pc; normalize nodelta
    999    >sigma_pc1_spec %] * #H1 @⊥ @H1 >EQspc in sigma_pc_spec; <sigma_pc1_spec
    1000    whd in match sigma_pc_opt; normalize nodelta @if_elim
    1001   [ #H2 #EQ lapply(sym_eq ??? EQ) -EQ @if_elim [#_  whd in ⊢ (??%% → ?); #EQ destruct %]
    1002     #H3 #H @('bind_inversion H) -H #x #H4 whd in ⊢ (??%? → ?); #EQ destruct >H2 in H3; *
    1003   | #H2 @if_elim
    1004     [ #H3 #H @('bind_inversion H) -H #x1 #_ whd in match pc_of_point; normalize nodelta
    1005       whd in ⊢ (??%? → ?); #EQ destruct >H3 in H2; *
    1006     | #H3 lapply sigma_pc1_spec; whd in match sigma_pc_opt; normalize nodelta @if_elim
    1007      [#H >H in H3; *] #_ #EQ >EQ @('bind_inversion EQ) -EQ * #x cases pc1 #bl1 #pos1
    1008      whd in match (point_of_pc ??); #x_spec whd in match (pc_of_point ???);
    1009      whd in match (offset_of_point ??); whd in ⊢ (??%? → ?); #EQ destruct
    1010      #H @('bind_inversion H) -H * #lbl cases pc #bl #pos whd in match (point_of_pc ??);
    1011      #lbl_spec whd in match pc_of_point; normalize nodelta
    1012      whd in match (offset_of_point ??); whd in ⊢ (??%? → ?); #EQ destruct
    1013      @eq_f cut(an_identifier LabelTag pos = an_identifier LabelTag pos1 → pos = pos1)
    1014      [ #EQ destruct %] #APP @APP @(partial_inj_sigma prog f_lbls bl1 …)
    1015      [ >lbl_spec % #EQ destruct] >x_spec >lbl_spec %
    1016     ]
    1017   ]
    1018 | #pc @mfr_return_eq1 %
    1019 ]
    1020 qed.
    1021 
    1022 lemma pc_block_eq : ∀prog : ertl_program. ∀f_lbls,pc.
    1023 sigma_pc_opt prog f_lbls pc ≠ None ? →
    1024  pc_block … pc = pc_block … (sigma_stored_pc prog f_lbls pc).
    1025 #prog #sigma * #bl #pos whd in match sigma_stored_pc; normalize nodelta
    1026 inversion(sigma_pc_opt ???) [ #_ * #H @⊥ @H %] #pc
    1027 whd in match sigma_pc_opt; normalize nodelta @if_elim
    1028 [#_ whd in ⊢ (??%? → ?); #EQ destruct #_ %] #_
    1029 #H @('bind_inversion H) -H * #lbl #_
    1030  whd in ⊢ (??%? → ?); #EQ destruct
    1031 #_ %
    1032 qed.
    1033 
    1034 include "joint/extra_joint_semantics.ma".
    1035 
    1036 lemma pop_frame_ok : ∀prog : ertl_program.
    1037 let trans_prog ≝ ertl_to_ertlptr prog in
    1038 ∀f_lbls : lbl_funct. ∀f_regs : regs_funct.
    1039 ∀restr.
    1040 preserving1 ?? res_preserve1 ????
    1041        (sigma_state prog f_lbls f_regs restr)
    1042        (λx.let 〈st,pc〉 ≝ x in
    1043            match fetch_internal_function ? (globalenv_noinit … prog)
    1044                  (pc_block pc) with
    1045                   [ OK y ⇒ let 〈id,f〉 ≝ y in
    1046                            〈sigma_state prog f_lbls f_regs
    1047                                  (added_registers ERTL (prog_var_names … prog) f
    1048                              (f_regs (pc_block pc))) st,
    1049                             sigma_stored_pc prog f_lbls pc〉
    1050                   | Error e ⇒ 〈dummy_state,null_pc one〉
    1051                   ])
    1052        (ertl_pop_frame)
    1053        (ertl_pop_frame).
    1054 #prog #f_lbls #f_regs #restr #st whd in match ertl_pop_frame; normalize nodelta
    1055 @mfr_bind1
    1056 [ @(λx.match sigma_frames_opt prog f_lbls f_regs x with [Some l ⇒ l | None ⇒ [ ]])
    1057 | @opt_to_res_preserve1 whd in match sigma_state; normalize nodelta
    1058   cases(st_frms … st) [@opt_preserve_none1] #l whd in match sigma_frames;
    1059   normalize  nodelta >m_return_bind #x #x_spec %{l} % [%] >x_spec %
    1060 | * normalize nodelta [@res_preserve_error1] * #loc_mem #bl #tl normalize nodelta
    1061   inversion(sigma_frames_opt ????) normalize nodelta [ #_ @res_preserve_error1]
    1062   #l whd in match sigma_frames_opt; whd in match m_list_map; normalize nodelta
    1063   whd in match (foldr ?????); normalize nodelta inversion(fetch_internal_function ???)
    1064   normalize nodelta [2: #e #_ #ABS destruct(ABS)] * #f #fn #EQfn
    1065   #H @('bind_inversion H) -H #l1
    1066   change with (sigma_frames_opt prog f_lbls f_regs tl = ? → ?) #EQl1
    1067   whd in ⊢ (??%? → ?); #EQ destruct(EQ) @mfr_bind1
    1068   [2: whd in match sigma_state; whd in match set_regs; whd in match set_frms;
    1069      normalize nodelta
    1070      cut( 〈sigma_register_env prog f_lbls
    1071      (added_registers ERTL (prog_var_names (joint_function ERTL) ℕ prog) fn
    1072       (f_regs bl))
    1073      loc_mem,
    1074     \snd  (sigma_regs prog f_lbls restr (regs ERTLptr_semantics st))〉 =
    1075     sigma_regs prog f_lbls 
    1076      (added_registers ERTL (prog_var_names (joint_function ERTL) ℕ prog) fn
    1077       (f_regs bl)) (〈loc_mem,\snd  (regs ERTL_state st)〉)) [
    1078       whd in match sigma_regs; normalize nodelta cases(regs … st) #x1 #x2
    1079       %] #EQ >EQ -EQ <EQl1 in ⊢ (???????%?);
    1080       change with (sigma_state prog f_lbls f_regs
    1081     (added_registers ERTL (prog_var_names … prog) fn (f_regs bl))
    1082       (mk_state ? (Some ? tl) (istack … st) (carry … st) (〈loc_mem,\snd (regs … st)〉)
    1083       (m … st))) in ⊢ (???????(??%)?); @pop_ra_ok |
    1084   | * #st1 #pc1 @if_elim normalize nodelta [2: #_ @res_preserve_error1]
    1085    normalize nodelta @eq_block_elim [2: #_ *] #EQbl1 * @if_elim
    1086    [2: >EQbl1 @eq_block_elim [#_ *] * #H @⊥ @H <pc_block_eq [%] %
    1087        cases bl in EQbl1 EQfn; #p1 #p2 #EQ destruct lapply p2
    1088        whd in match sigma_stored_pc; normalize nodelta cases(sigma_pc_opt ???)
    1089        normalize nodelta [2: #pc2] #p2 [#_ #EQ destruct]
    1090        >fetch_internal_function_no_zero [2: %] #EQ destruct
    1091    |   @eq_block_elim [2: #_ *] #EQbl11 * @mfr_return_eq1 normalize nodelta
    1092        cases bl in EQbl11 EQfn; #p1 #p2 #EQ destruct
    1093        lapply p2 cases(pc_block pc1) #p11 #p22 #e #EQfn1 >EQfn1 %
    1094    ]
    1095   ]
    1096 ]
    1097 qed.
     38
     39
    109840 
    109941(*
     
    1173115include "joint/semantics_blocks.ma".
    1174116
    1175 lemma fetch_ok_sigma_pc_ok :∀prog : ertl_program.
    1176 ∀ f_lbls,f_regs,id,fn,st.
    1177 fetch_internal_function … (globalenv_noinit … prog)
    1178 (pc_block (pc … (sigma_state_pc prog f_lbls f_regs st))) = return 〈id,fn〉 →
    1179 pc … (sigma_state_pc prog f_lbls f_regs st) = pc … st.
    1180 #prog #f_lbls #f_regs #id #fn #st whd in match sigma_state_pc;
    1181 normalize nodelta cases(fetch_internal_function ?? (pc_block (pc … st)))
    1182 normalize nodelta [* #id1 #fn1 #_ %]
    1183 #e >fetch_internal_function_no_zero [2: %] whd in ⊢ (???% → ?); #EQ destruct(EQ)
    1184 qed.
    1185 
    1186 lemma fetch_ok_sigma_state_ok : ∀prog : ertl_program.
    1187 ∀ f_lbls,f_regs,id,fn,st.
    1188 fetch_internal_function … (globalenv_noinit … prog)
    1189 (pc_block (pc … (sigma_state_pc prog f_lbls f_regs st))) = return 〈id,fn〉 →
    1190 let added ≝ (added_registers ERTL (prog_var_names … prog) fn
    1191                                                (f_regs (pc_block (pc … st)))) in
    1192 st_no_pc … (sigma_state_pc prog f_lbls f_regs st) =
    1193 sigma_state prog f_lbls f_regs added (st_no_pc … st).
    1194 #prog #f_lbls #f_regs #id #fn #st #EQf whd in match sigma_state_pc;
    1195 normalize nodelta <(fetch_ok_sigma_pc_ok … EQf) >EQf %
    1196 qed.
    1197 
    1198 lemma fetch_ok_sigma_pc_block_ok : ∀prog : ertl_program.
    1199 ∀ f_lbls,id,fn,pc.
    1200 fetch_internal_function … (globalenv_noinit … prog)
    1201 (pc_block (sigma_stored_pc prog f_lbls pc)) = return 〈id,fn〉 →
    1202 pc_block (sigma_stored_pc prog f_lbls pc) = pc_block pc.
    1203 #prog #f_lbls #id #fn #pc #EQf <pc_block_eq [%]
    1204 lapply EQf whd in match sigma_stored_pc; normalize nodelta
    1205 cases(sigma_pc_opt ???) normalize nodelta [2: #pc #_ % #EQ destruct(EQ)]
    1206 >fetch_internal_function_no_zero [2: %] whd in ⊢ (???% → ?); #EQ destruct(EQ)
    1207 qed.
    1208 
    1209 lemma fetch_stmt_ok_sigma_pc_ok : ∀prog : ertl_program.
    1210 ∀ f_lbls,f_regs,id,fn,stmt,st.
    1211 fetch_statement ERTL_semantics (prog_var_names … prog)
    1212     (globalenv_noinit … prog) (pc … (sigma_state_pc prog f_lbls f_regs st)) =
    1213                return 〈id,fn,stmt〉 →
    1214 pc … (sigma_state_pc prog f_lbls f_regs st) = pc … st.
    1215 #prog #f_lbls #f_regs #id #fn #stmt #st #H @('bind_inversion H)
    1216 * #id1 #fn1 #EQfn1 #_ @(fetch_ok_sigma_pc_ok … EQfn1)
    1217 qed.
    1218 
    1219 lemma fetch_stmt_ok_sigma_state_ok : ∀prog : ertl_program.
    1220 ∀ f_lbls,f_regs,id,fn,stmt,st.
    1221 fetch_statement ERTL_semantics (prog_var_names … prog)
    1222     (globalenv_noinit … prog) (pc … (sigma_state_pc prog f_lbls f_regs st)) =
    1223                return 〈id,fn,stmt〉 →
    1224 let added ≝ (added_registers ERTL (prog_var_names … prog) fn
    1225                                                (f_regs (pc_block (pc … st)))) in
    1226 st_no_pc … (sigma_state_pc prog f_lbls f_regs st) =
    1227 sigma_state prog f_lbls f_regs added (st_no_pc … st).
    1228 #prog #f_lbls #f_regs #id #fn #stmt #st #H @('bind_inversion H) -H
    1229 * #id1 #fn1 #EQfn1 #H @('bind_inversion H) -H #stmt1 #_
    1230 whd in ⊢ (??%% → ?); #EQ destruct(EQ) @(fetch_ok_sigma_state_ok … EQfn1)
    1231 qed.
    1232 
    1233 lemma fetch_stmt_ok_sigma_pc_block_ok : ∀prog : ertl_program.
    1234 ∀ f_lbls,id,fn,stmt,pc.
    1235 fetch_statement ERTL_semantics (prog_var_names … prog)
    1236   (globalenv_noinit … prog) (sigma_stored_pc prog f_lbls pc) = return 〈id,fn,stmt〉 →
    1237 pc_block (sigma_stored_pc prog f_lbls pc) = pc_block pc.
    1238 #prog #f_lbls #id #fn #stmt #st #H @('bind_inversion H) -H
    1239 * #id1 #fn1 #EQfn1 #H @('bind_inversion H) -H #stmt1 #_
    1240 whd in ⊢ (??%% → ?); #EQ destruct(EQ) @(fetch_ok_sigma_pc_block_ok … EQfn1)
    1241 qed.
     117
    1242118
    1243119lemma as_label_ok : ∀ prog : ertl_program.
     
    1283159qed.
    1284160
    1285 lemma fetch_ok_sigma_last_pop_ok :∀prog : ertl_program.
    1286 ∀ f_lbls,f_regs,id,fn,st.
    1287 fetch_internal_function … (globalenv_noinit … prog)
    1288 (pc_block (pc … (sigma_state_pc prog f_lbls f_regs st))) = return 〈id,fn〉 →
    1289 last_pop … (sigma_state_pc prog f_lbls f_regs st) =
    1290 sigma_stored_pc prog f_lbls (last_pop … st).
    1291 #prog #f_lbls #f_regs #id #fn #st whd in match sigma_state_pc; normalize nodelta
    1292 cases(fetch_internal_function ?? (pc_block (pc … st))) normalize nodelta
    1293 [ * #x #y #_ %] #e >fetch_internal_function_no_zero [2: %] whd in ⊢ (???% → ?);
    1294 #EQ destruct(EQ)
    1295 qed.
    1296 
    1297 lemma fetch_stmt_ok_sigma_last_pop_ok :∀prog : ertl_program.
    1298 ∀ f_lbls,f_regs,id,fn,stmt,st.
    1299 fetch_statement ERTL_semantics (prog_var_names … prog)
    1300     (globalenv_noinit … prog) (pc … (sigma_state_pc prog f_lbls f_regs st))
    1301     = return 〈id,fn,stmt〉 →
    1302 last_pop … (sigma_state_pc prog f_lbls f_regs st) =
    1303 sigma_stored_pc prog f_lbls (last_pop … st).
    1304 #prog #f_lbls #f_regs #id #fn #stmt #st #H @('bind_inversion H) -H
    1305 * #id1 #fn1 #EQfn1 #H @('bind_inversion H) -H #stmt1 #_
    1306 whd in ⊢ (??%% → ?); #EQ destruct(EQ) @(fetch_ok_sigma_last_pop_ok … EQfn1)
    1307 qed.
    1308 
    1309 lemma excluded_middle_list :
    1310 ∀A : Type[0]. ∀P : A → Prop. (∀a.decidable … (P a)) → ∀ l.
    1311 All … P l ∨ Exists … (λa.¬(P a)) l.
    1312 #A #P #Dec #l elim l [% %] #hd #tl #IH
    1313 cases IH [ cases(Dec hd) [ #H1 #H2 % whd % assumption | #H #_ %2 whd % assumption]
    1314          | #H %2 whd %2 assumption
    1315          ]
    1316 qed.
     161include alias "basics/lists/listb.ma".
    1317162
    1318163lemma eval_seq_no_call_ok :
     
    1446291qed.
    1447292
    1448 lemma code_block_of_block_eq : ∀bl : Σb.block_region b = Code.
    1449 code_block_of_block bl = return bl.
    1450 * #bl #prf whd in match code_block_of_block; normalize nodelta @match_reg_elim
    1451 [ >prf in ⊢ (% → ?); #ABS destruct(ABS)] #prf1 %
    1452 qed.
     293
    1453294
    1454295(*
     
    1462303qed.*)
    1463304
    1464 lemma split_on_last_append : ∀A : Type[0]. ∀pre : list A.
    1465 ∀ last : A. split_on_last ? (pre@[last]) = return 〈pre,last〉.
    1466 #A #pre elim pre [#last %] #a #tl #IH #last whd in ⊢ (??%?);lapply(IH last)
    1467 whd in ⊢ (??%? → ?); #EQ >EQ %
    1468 qed.
    1469 
    1470 lemma append_All : ∀A : Type[0]. ∀ P : A → Prop. ∀l1,l2 : list A.
    1471 All ? P (l1 @ l2) → All ? P l1 ∧ All ? P l2.
    1472 #A #P #l1 elim l1
    1473 [ #l2 change with l2 in ⊢ (???% → ?); #H % //]
    1474 #a #tl #IH #l2 change with (P a ∧ All A P (tl @ l2)) in ⊢ (% → ?);
    1475 * #H1 #H2 lapply(IH … H2) * #H3 #H4 % // whd % //
    1476 qed.
    1477 
    1478 include alias "common/Identifiers.ma".
    1479 
    1480 lemma get_sigma_idempotent :
    1481 ∀prog : ertl_program.
    1482 ∀ f_lbls,f_regs.
    1483  ∀f_bl_r.
    1484  b_graph_transform_program_props ERTL_semantics ERTLptr_semantics
    1485      translate_data prog f_bl_r f_lbls f_regs →
    1486 ∀id,fn,bl,pt,stmt.
    1487 fetch_internal_function … (globalenv_noinit … prog) bl = return 〈id,fn〉 →
    1488 stmt_at ERTL (prog_var_names … prog) (joint_if_code … fn) pt = return stmt → 
    1489 f_lbls bl pt = return [ ] → get_sigma prog f_lbls bl pt = return pt.
    1490 #prog #f_lbls #f_regs #f_bl_r #good #id #fn #bl #pt #stmt #EQfn #EQstmt #EQlabels
    1491 cases(b_graph_transform_program_fetch_internal_function … good … EQfn)
    1492 #init_data * #calling' ** #EQcalling' whd in ⊢ (% → ?); cases(f_bl_r ?)
    1493 [2,4: #x #y *] normalize nodelta #EQ destruct(EQ) * #_ #_ #_ #_ #_
    1494 #_ #fresh_labs #_ #_ #_ #H lapply(H … EQstmt) -H * #lbls * #regs ** >EQlabels
    1495 whd in ⊢ (??%? → ?); #EQ destruct(EQ) #EQregs cases stmt in EQstmt; normalize nodelta
    1496 [3: * |2: * [#lbl || *] #EQstmt * #bl * whd in ⊢ (% → ?); cases regs in EQregs;
    1497     [2,4: #x #y #_ *] #EQregs normalize nodelta #EQ destruct(EQ) whd in ⊢ (%→?);
    1498     * #pref * #mid ** #EQmid whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2)
    1499     whd in ⊢ (% → ?); #EQt_stmt
    1500 | * [#c | * [#c_id|#c_ptr] #args #dest | #r #lbl | #seq ] #nxt #EQstmt
    1501   whd in ⊢ (% → ?); * #bl >if_merge_right [2,4,6,8,10: %] * whd in ⊢ (% → ?);
    1502   cases regs in  EQregs; normalize nodelta
    1503   [2,4,5,8,10: [1,2,4,5: #x #y] #_ *|6: #r * [2: #x #y] ]
    1504   #EQregs [1,2: whd in ⊢ (% → ?); [*]] #EQ destruct(EQ) whd in ⊢ (% → ?);
    1505   * #l1 * #mid1 * #mid2 * #l2 *** #EQmid1 whd in ⊢ (%→ ?);
    1506   [ * #mid * #rest ** #EQ destruct(EQ) whd in ⊢ (% → ?); * #nxt1 *
    1507     #EQlow change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ)
    1508     whd in ⊢ (% → ?); * #mid3 * #rest1 ** #EQ destruct(EQ)
    1509      whd in EQmid1 : (???%); destruct(EQmid1) whd in e0 : (???%);
    1510      destruct(e0) ] * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in EQmid1 : (???%);
    1511      destruct(EQmid1) whd in ⊢ (% → ?); * #nxt1 * #EQt_stmt #EQ destruct(EQ)
    1512      whd in ⊢ (% → ?); * #_ #EQ destruct(EQ)
    1513 ] whd in match get_sigma; normalize nodelta >code_block_of_block_eq >m_return_bind
    1514 >EQfn >m_return_bind inversion(find ????)
    1515 [1,3,5,7,9,11: #EQfind @⊥ lapply(find_none ?????? EQfind EQstmt) >EQlabels
    1516   normalize nodelta @eq_identifier_elim [1,3,5,7,9,11: #_ * |*: * #H #_ @H %]]
    1517 * #lbl #s #EQfind >m_return_bind lapply(find_predicate ?????? EQfind)
    1518 inversion(f_lbls ??) [1,3,5,7,9,11: #_ *] #l @(list_elim_left … l …)
    1519 normalize nodelta [1,3,5,7,9,11: #_ @eq_identifier_elim
    1520                          [1,3,5,7,9,11: #EQ destruct(EQ) #_ % |*: #_ *]]
    1521 #last #pre #_ #EQlbl >split_on_last_append normalize nodelta @eq_identifier_elim
    1522 [2,4,6,8,10,12: #_ *] #EQ lapply EQlbl destruct(EQ) #EQlbl #_ @⊥
    1523 lapply(fresh_labs lbl) >EQlbl whd in ⊢ (% → ?); #H lapply(append_All … H) -H
    1524 * #_ whd in ⊢ (% → ?); *** #H #_ #_ @H -H @(code_is_in_universe … (pi2 ?? fn))
    1525 whd in match code_has_label; whd in match code_has_point; normalize nodelta
    1526 >EQstmt @I
    1527 qed.
    1528 
    1529 lemma append_absurd : ∀A : Type[0]. ∀l : list A. ∀ a : A.
    1530 l @ [a] = [ ] → False.
    1531 #A * [2: #x #y] #a normalize #EQ destruct
    1532 qed.
    1533 
    1534 lemma last_append_eq : ∀A : Type[0].∀l1,l2 : list A. ∀a1,a2: A.
    1535 l1 @ [a1] = l2 @ [a2] → a1 = a2.
    1536 #A #l1 elim l1 [ * [2: #hd #tl] #a1 #a2 normalize #EQ destruct [2: %]
    1537 @⊥ lapply(sym_eq ??? e0) -e0 #e0 @(append_absurd ??? e0)] #hd #tl #IH
    1538 * [ #a1 #a2 normalize #EQ destruct @⊥ @(append_absurd ??? e0)]
    1539 #hd1 #tl1 #a1 #a2 normalize #EQ destruct(EQ) @(IH tl1 a1 a2 e0)
    1540 qed.
    1541 
    1542 lemma get_sigma_last :
    1543 ∀prog : ertl_program.
    1544 ∀ f_lbls,f_regs.
    1545  ∀f_bl_r.
    1546  b_graph_transform_program_props ERTL_semantics ERTLptr_semantics
    1547      translate_data prog f_bl_r f_lbls f_regs →
    1548 ∀id,fn,bl,pt,stmt,pre,last.
    1549 fetch_internal_function … (globalenv_noinit … prog) bl = return 〈id,fn〉 →
    1550 stmt_at ERTL (prog_var_names … prog) (joint_if_code … fn) pt = return stmt → 
    1551 f_lbls bl pt = return (pre@[last]) → get_sigma prog f_lbls bl last = return pt.
    1552 #prog #f_lbls #f_regs #f_bl_r #good #id #fn #bl #pt #stmt #pre #last
    1553 #EQfn #EQstmt #EQlabels
    1554 cases(b_graph_transform_program_fetch_internal_function … good … EQfn)
    1555 #init_data * #calling' ** #EQcalling' whd in ⊢ (% → ?); cases(f_bl_r ?)
    1556 [2,4: #x #y *] normalize nodelta #EQ destruct(EQ) * #_ #_ #_ #_ #pp_labs
    1557 #_ #fresh_labs #_ #_ #_ #H lapply(H … EQstmt) -H * #lbls * #regs ** >EQlabels
    1558 whd in ⊢ (??%? → ?); #EQ destruct(EQ) #EQregs cases stmt in EQstmt; normalize nodelta
    1559 [3: *
    1560 |2: * [#lbl || *] #EQstmt whd in ⊢ (%→ ?); * #bl *
    1561 |*: * [#c | * [ #c_id | #c_ptr] #args #dest | #r #lbl | #seq ] #nxt #EQstmt
    1562     >if_merge_right [2,4,6,8,10: %] whd in ⊢ (% → ?); * #bl *
    1563 ] whd in ⊢ (% → ?); cases regs in EQregs; normalize nodelta
    1564 [2,4,6,8,9,12,14: [1,2,3,4,6,7: #x #y] #_ *|10: #r #tl] #EQregs
    1565 [ whd in ⊢ (% → ?); cases tl in EQregs; normalize nodelta [2: #x #y #_ *] #EQregs]
    1566 #EQbl destruct(EQbl) whd in ⊢ (%→?); [2,3: * #pref * #mid **|*: * #l1 * #mid1 * #mid2 * #l2 ***]
    1567 #EQmid1 whd in ⊢ (% → ?);
    1568 [1,2,4,5,6,7: * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in EQmid1 : (??%%); destruct(EQmid1)
    1569 [3,4,5,6: whd in ⊢ (% → ?); * #nxt1 * #EQt_stmt  #EQ destruct(EQ) ]
    1570 whd in ⊢ (% → ?); * [1,2,3,4: #e0] @⊥ @(append_absurd ??? e0)]
    1571 * #mid * #rest ** #EQ destruct(EQ) whd in ⊢ (% → ?); * #nxt1 * #_
    1572 change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) whd in ⊢ (% → ?);
    1573 * #mid3 * #rest1 ** #EQ destruct(EQ) whd in ⊢ (% → ?); * #nxt1 * #_
    1574 change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) whd in ⊢ (% → ?);
    1575 * #mid4 * #rest2 ** #EQ destruct(EQ)  whd in ⊢ (% → ?); * #nxt1 * #_
    1576 change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) whd in ⊢ (% → ?);
    1577 * #mid5 * #rest3 ** #EQ destruct(EQ) whd in ⊢ (% → ?); * #nxt1 * #_
    1578 change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) whd in ⊢ (% → ?);
    1579 * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in ⊢ (% → ?); * #nxt1 * #EQcall
    1580 change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) whd in ⊢ (% → ?);
    1581 * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in EQmid1 : (??%%); destruct(EQmid1)
    1582 >e0 in EQlabels; #EQlabels whd in match get_sigma; normalize nodelta
    1583 >code_block_of_block_eq >m_return_bind >EQfn >m_return_bind
    1584 inversion(find ????)
    1585 [ #EQfind @⊥ lapply(find_none ?????? EQfind EQstmt) >EQlabels
    1586   normalize nodelta @eq_identifier_elim [ #_ *] * #H #_ @H
    1587   whd in EQmid1 : (??%%); destruct(EQmid1) @(last_append_eq ????? e1) ]
    1588 * #lbl #s #EQfind >m_return_bind lapply(find_predicate ?????? EQfind)
    1589 inversion(f_lbls ??) [ #_ normalize nodelta *] #labels
    1590 @(list_elim_left … labels …) -labels normalize nodelta
    1591 [ #EQl @eq_identifier_elim [2: #_ *] #EQ lapply EQl destruct(EQ) #EQl
    1592   lapply(fresh_labs pt) >EQlabels <e0 whd in ⊢ (% → ?);
    1593   #H lapply(append_All … H) -H * #_ whd in ⊢ (% → ?); *** #H #_ #_ #_ @⊥ @H
    1594   @(code_is_in_universe … (pi2 ?? fn)) whd in match code_has_label;
    1595   whd in match code_has_point; normalize nodelta whd in match (stmt_at ????);
    1596   >(find_lookup ?????? EQfind) @I
    1597 | #last1 #pre1 #_ #EQl >split_on_last_append normalize nodelta @eq_identifier_elim
    1598   [2: #_ *] #EQ lapply EQl destruct(EQ) #EQl #_ lapply pp_labs
    1599   whd in match partial_partition; normalize nodelta * #_ #H lapply(H lbl pt)
    1600   >EQl <e0 in EQlabels; #EQlabels >EQlabels whd in ⊢ (% → ?); -H #H
    1601   >(H last1 ? ?) [%] >(memb_append_l2 ? last1 ? [last1] ?) /2 by /
    1602 ]
    1603 qed.
    1604 
    1605 lemma fetch_call_commute :
    1606 ∀prog : ertl_program.
    1607 let trans_prog ≝ ertl_to_ertlptr prog in
    1608 ∀ f_lbls,f_regs.
    1609  ∀f_bl_r.
    1610  b_graph_transform_program_props ERTL_semantics ERTLptr_semantics
    1611      translate_data prog f_bl_r f_lbls f_regs →
    1612 ∀id,fn,c_id,c_args,c_dest,nxt,pc.
    1613 fetch_statement ERTL_semantics
    1614     (prog_var_names … prog) (globalenv_noinit … prog) pc =
    1615     return 〈id,fn, sequential ? ?(CALL ERTL_semantics ? c_id c_args c_dest) nxt〉 →
    1616 ∃fn',pc'. sigma_stored_pc prog f_lbls pc' = pc ∧
    1617 fetch_statement ERTLptr_semantics
    1618     (prog_var_names … trans_prog) (globalenv_noinit … trans_prog) pc' =
    1619 return 〈id,fn', sequential ? ?(CALL ERTLptr_semantics ? c_id c_args c_dest) nxt〉.
    1620 #prog #f_lbls #f_regs #f_bl_r #good #id #fn * [ #c_id | #c_ptr ] #c_args #c_dest
    1621 #nxt #pc #EQfetch lapply(fetch_statement_inv … EQfetch) * #EQfn #EQstmt
    1622 cases(b_graph_transform_program_fetch_internal_function … good … EQfn)
    1623 #init_data * #calling' ** #EQcalling' whd in ⊢ (% → ?); cases(f_bl_r ?)
    1624 [2,4: #x #y *] normalize nodelta #EQ destruct(EQ) * #_ #_ #_ #_ #pp_labs
    1625 #_ #fresh_labs #_ #_ #_ #H cases(H … EQstmt) -H #labels * #registers
    1626 ** #EQlabels #EQregisters normalize nodelta >if_merge_right [2,4: %]
    1627 whd in match translate_step;
    1628 normalize nodelta whd in ⊢ (% → ?); * #bl * whd in ⊢ (% → ?);
    1629 cases registers in EQregisters; -registers normalize nodelta
    1630 [2,3: [ #x #y] #_ *|4: #r #tl] #EQregisters
    1631 [ whd in ⊢ (% → ?); cases tl in EQregisters; -tl [2: #x #y #_ *] normalize nodelta
    1632 #EQregisters] #EQ destruct(EQ) whd in ⊢ (% → ?); *
    1633 #pre_l * #mid1 * #mid2 * #post_l *** #EQmid1 whd in ⊢ (% → ?);
    1634 [ * #mid * #resg ** #EQ destruct(EQ) whd in ⊢ (% → ?);
    1635   * #nxt1 * #EQlow change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ)
    1636   whd in ⊢ (% → ?); * #mid3 * #rest1 ** #EQ destruct(EQ) * #nxt1 *
    1637   #EQpush1 change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ)
    1638   whd in ⊢ (% → ?); * #mid4 * #rest2 ** #EQ destruct(EQ) * #nxt1 * #EQhigh
    1639   change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) whd in ⊢ (% → ?);
    1640   * #mid5 * #rest3 ** #EQ destruct(EQ) * #nxt1 * #EQpush2
    1641   change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) whd in ⊢ (% → ?);
    1642 ] * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in EQmid1 : (??%%); destruct(EQmid1)
    1643 whd in ⊢ (% → ?); * #nxt1 * #EQcall #EQ destruct(EQ) whd in ⊢ (% → ?);
    1644 * #EQ destruct(EQ) change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ)
    1645 %{calling'}
    1646 [  %{(pc_of_point ERTLptr_semantics (pc_block pc) mid1)}
    1647 |  %{pc}
    1648 ] %
    1649 [1,3: whd in match sigma_stored_pc; whd in match sigma_pc_opt; normalize nodelta
    1650       @eqZb_elim change with (pc_block pc) in match (pc_block ?) in ⊢ (% → ?);
    1651       [1,3: #EQbl >fetch_internal_function_no_minus_one in EQfn; try assumption
    1652             #EQ destruct(EQ)] #_ normalize nodelta
    1653             [2: >(get_sigma_idempotent … good … EQfn EQstmt EQlabels)
    1654             |*: change with (pc_block pc) in match (pc_block ?);
    1655                 >point_of_pc_of_point >(get_sigma_last … good … EQfn EQstmt EQlabels)
    1656             ] >m_return_bind normalize nodelta >pc_of_point_of_pc %
    1657 |*: whd in match fetch_statement; normalize nodelta >EQcalling' >m_return_bind
    1658     [>point_of_pc_of_point ] >EQcall %
    1659 ]
    1660 qed.
    1661 
    1662 
    1663 
    1664 lemma next_of_call_pc_ok : ∀prog : ertl_program.
    1665 let trans_prog ≝ ertl_to_ertlptr prog in
    1666 ∀ f_lbls,f_regs.∀f_bl_r.
    1667 b_graph_transform_program_props ERTL_semantics ERTLptr_semantics
    1668      translate_data prog f_bl_r f_lbls f_regs →
    1669 ∀pc,lb.
    1670 next_of_call_pc ERTL_semantics (prog_var_names … prog) (globalenv_noinit … prog)
    1671   pc = return lb →
    1672 ∃pc'. sigma_stored_pc prog f_lbls pc' = pc ∧ 
    1673 next_of_call_pc ERTLptr_semantics (prog_var_names … trans_prog)
    1674              (globalenv_noinit … trans_prog) pc' =  return lb.
    1675 #prog #f_lbls #f_regs #f_bl_r #good #pc #lb whd in match next_of_call_pc;
    1676 normalize nodelta #H @('bind_inversion H) -H ** #id #fn
    1677 *  [ *[ #c | #c_id #c_arg #c_dest | #reg #lbl | #seq ] #prox | #fin | *]
    1678 #EQfetch normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ)
    1679 cases(fetch_call_commute … good … EQfetch) #fn1 * #pc1 * #EQpc1 #EQt_fetch
    1680 %{pc1} % [assumption] >EQt_fetch %
    1681 qed.
    1682 
    1683 lemma next_of_call_pc_error : ∀pars.∀prog : program ? ℕ. ∀init,pc.
    1684 (block_id (pi1 … (pc_block pc)) = 0 ∨ block_id (pi1 … (pc_block pc)) = -1) →
    1685 next_of_call_pc pars (prog_var_names … prog) (globalenv … init prog)
    1686   pc = Error ? [MSG BadFunction].
    1687 #pars #prg #init #pc * #EQ whd in match next_of_call_pc; normalize nodelta
    1688 whd in match fetch_statement; normalize nodelta
    1689 [ >fetch_internal_function_no_zero | >fetch_internal_function_no_minus_one]
    1690 //
    1691 qed.
    1692 
    1693 lemma next_of_call_pc_inv :  ∀pars.∀prog : program ? ℕ. ∀init.
    1694 ∀pc,nxt.
    1695 next_of_call_pc pars (prog_var_names … prog)
    1696 (globalenv … init prog) pc = return nxt →
    1697 ∃id,fn,c_id,c_args,c_dest.
    1698 fetch_statement pars
    1699     (prog_var_names … prog) (globalenv … init prog) pc =
    1700     return 〈id,fn, sequential ? ?(CALL pars ? c_id c_args c_dest) nxt〉.
    1701 #pars #prog #init #pc #nxt whd in match next_of_call_pc; normalize nodelta
    1702 #H @('bind_inversion H) -H ** #id #fn *
    1703 [ *[ #c | #c_id #c_arg #c_dest | #reg #lbl | #seq ] #prox | #fin | #H #r #l #l ]
    1704 #EQfetch normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ)
    1705 %{id} %{fn} %{c_id} %{c_arg} %{c_dest} assumption
    1706 qed.
    1707 
    1708 lemma sigma_stored_pc_inj : ∀ prog : ertl_program.
    1709 ∀f_lbls,pc,pc'. sigma_pc_opt prog f_lbls pc ≠ None ? →
    1710 sigma_pc_opt prog f_lbls pc = sigma_pc_opt prog f_lbls pc' →
    1711 pc = pc'.
    1712 #prog #f_lbls ** #id #EQblid #off ** #id' #EQblid' #off'
    1713 * inversion(sigma_pc_opt ???) [#_ #H @⊥ @H %]
    1714 #pc1 whd in match sigma_pc_opt; normalize nodelta @if_elim
    1715 [ @eqZb_elim [2: #_ *] #EQbl * whd in ⊢ (??%? → ?); #EQ destruct #_
    1716 #H lapply(sym_eq ??? H) -H @if_elim [#_ whd in ⊢ (??%? → ?); #EQ destruct %]
    1717 @eqZb_elim [ #_ *] * #EQbl' #_ #H @('bind_inversion H) -H #lb #EQlb
    1718 whd in ⊢ (??%? → ?); #EQ destruct @⊥ @EQbl' assumption] @eqZb_elim [#_ *] * #EQbl #_
    1719 #H @('bind_inversion H) -H * #lb #EQlb whd in ⊢ (??%? → ?); #EQ destruct #_
    1720 #H lapply(sym_eq ??? H) -H @if_elim
    1721 [ @eqZb_elim [2: #_ *] #EQbl' #_ whd in ⊢ (??%? → ?); #EQ destruct @⊥ @EQbl @EQbl']
    1722 #_ #H @('bind_inversion H) -H * #lb' #EQlb' whd in ⊢ (??%? → ?);
    1723 whd in match (pc_of_point ???); whd in match (offset_of_point ??);
    1724 whd in match (offset_of_point ??); #EQ destruct @eq_f
    1725 cut(an_identifier LabelTag off = an_identifier LabelTag off') [2: #EQ destruct %]
    1726 @(partial_inj_sigma prog f_lbls id) [>EQlb % #ABS destruct | >EQlb >EQlb' %]
    1727 qed.
     305
    1728306
    1729307lemma eval_return_ok :
     
    1869447qed.
    1870448
    1871 lemma bool_of_beval_ok : ∀prog : ertl_program.
    1872 ∀f_lbls. preserving1 … res_preserve1 …
    1873               (sigma_beval prog f_lbls)
    1874               (λx.x)
    1875               (bool_of_beval)
    1876               (bool_of_beval).
    1877 #prog #f_lbls * [ | | #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc1 #p1]
    1878 whd in match bool_of_beval; normalize nodelta try @res_preserve_error1
    1879 try @mfr_return1 whd in match sigma_beval; normalize nodelta
    1880 cases (sigma_pc_opt ???) normalize nodelta [2: #pc] @res_preserve_error1
    1881 qed.
     449
    1882450
    1883451lemma eval_cond_ok :
     
    2033601qed.
    2034602
    2035 lemma block_of_call_ok : ∀prog: ertl_program.
    2036  let trans_prog ≝ ertl_to_ertlptr prog in
    2037  ∀ f_lbls,f_regs.
    2038 ∀called,restr. preserving1 … res_preserve1 …
    2039               (sigma_state prog f_lbls f_regs restr)
    2040               (λx.x)
    2041               (block_of_call ERTL_semantics (prog_var_names … prog)
    2042                       (globalenv_noinit … prog) called)
    2043               (block_of_call ERTLptr_semantics (prog_var_names … trans_prog)
    2044                       (globalenv_noinit … trans_prog) called).
    2045 #prog #f_lbls #f_regs #called #restr #st whd in match block_of_call; normalize nodelta
    2046 @mfr_bind1
    2047 [ @(λx.x)
    2048 | cases(called) [#c_id | #c_ptr] normalize nodelta
    2049   [ @opt_to_res_preserve1 #bl #EQbl %{bl} % [2: %]
    2050     >(find_symbol_transf …
    2051           (λvars.transf_fundef … (λfn.(b_graph_translate … fn))) prog c_id)
    2052    assumption
    2053   | @mfr_bind1
    2054     [2: whd in match dpl_arg_retrieve; normalize nodelta @(ps_arg_retrieve_ok) |
    2055     | #bv1 @mfr_bind1
    2056       [2: whd in match dph_arg_retrieve; normalize nodelta @(ps_arg_retrieve_ok) |
    2057       | #bv2 @mfr_bind1
    2058         [ @(λx.x)
    2059         | whd in match pointer_of_bevals; normalize nodelta
    2060           cases bv1 normalize nodelta
    2061           [ | | #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc1 #p1]
    2062           try @res_preserve_error1
    2063           [ cases bv2 [ | | #ptr1' #ptr2' #p' | #by' | #p' | #ptr' #p' | #pc1' #p1']
    2064           normalize nodelta
    2065           [1,2,3,4,5: @res_preserve_error1
    2066           | @if_elim #_ [@mfr_return_eq1 % | @res_preserve_error1]
    2067           ]
    2068           ] whd in match sigma_beval; normalize nodelta cases(sigma_pc_opt ???)
    2069             normalize nodelta [2,4: #pc ] @res_preserve_error1
    2070         |
    2071         #ptr @if_elim #_ [@mfr_return_eq1 % | @res_preserve_error1]
    2072       ]
    2073     ]
    2074   ]
    2075  ]
    2076 | #bl @opt_to_res_preserve1 whd in match code_block_of_block; normalize nodelta
    2077   @match_reg_elim [ #_ @opt_preserve_none1 | #prf @mfr_return_eq1 %]
    2078 ]
    2079 qed.
    2080 
    2081 lemma bvpc_sigma_pc_to_sigma_beval : ∀prog : ertl_program.
    2082 ∀f_lbls,pc,p. sigma_pc_opt prog f_lbls pc ≠ None ? →
    2083 BVpc (sigma_stored_pc prog f_lbls pc) p =
    2084 sigma_beval prog f_lbls (BVpc pc p).
    2085 #prog #f_lbls #pc #p #prf whd in match sigma_stored_pc;
    2086 whd in match sigma_beval; normalize nodelta lapply prf
    2087 cases(sigma_pc_opt ???) [ * #H @⊥ @H % | #pc' #_ % ]
    2088 qed.
    2089 
    2090 lemma push_ra_ok : ∀prog : ertl_program.
    2091 ∀f_lbls,f_regs,restr,pc. sigma_pc_opt prog f_lbls pc ≠ None ? →
    2092     preserving1 ?? res_preserve1 …
    2093           (sigma_state prog f_lbls f_regs restr)
    2094           (sigma_state prog f_lbls f_regs restr)
    2095           (λst.push_ra ERTL_semantics st (sigma_stored_pc prog f_lbls pc))
    2096           (λst.push_ra ERTLptr_semantics st pc).
    2097 #prog #f_lbls #f_regs #restr #pc #prf #st whd in match push_ra; normalize nodelta
    2098 @mfr_bind1
    2099 [  @(sigma_state prog f_lbls f_regs restr)
    2100 |  >(bvpc_sigma_pc_to_sigma_beval … prf) @push_ok
    2101 |  #st' >(bvpc_sigma_pc_to_sigma_beval … prf) @push_ok
    2102 ] qed.
    2103 
    2104 lemma ertl_save_frame_ok : ∀prog : ertl_program.
    2105 ∀f_lbls.∀f_regs : regs_funct.∀kind,restr.
    2106 preserving1 ?? res_preserve1 ????
    2107            (λst. match fetch_internal_function … (globalenv_noinit … prog)
    2108                        (pc_block (pc … st)) with
    2109                  [ OK y ⇒ let 〈f,fn〉 ≝ y in
    2110                           let added ≝ added_registers … (prog_var_names … prog) fn
    2111                                        (f_regs (pc_block (pc … st))) in
    2112                           mk_state_pc ? (sigma_state prog f_lbls f_regs added st)
    2113                                         (sigma_stored_pc prog f_lbls (pc … st))
    2114                                         (sigma_stored_pc prog f_lbls (last_pop … st))
    2115                  | Error e ⇒ dummy_state_pc
    2116                  ])
    2117            (sigma_state prog f_lbls f_regs restr)
    2118            (ertl_save_frame kind it)
    2119            (match kind with
    2120             [ID ⇒ ertlptr_save_frame ID it
    2121             |PTR ⇒ λst. !st' ← push_ra … st (pc … st);
    2122                         ertlptr_save_frame ID it (set_no_pc … st' st)
    2123             ]).
    2124             xxxxxxxxxxxxxxxxxxx
    2125 #prog #f_lbls #f_regs #kind #restr #st whd in match ertl_save_frame;
    2126 whd in match ertlptr_save_frame; normalize nodelta @mfr_bind1
    2127 [2: cases(fetch_internal_function ???) normalize nodelta
    2128     [ * #id #fn normalize nodelta
    2129    
    2130     change with (st_no_pc … st) in ⊢ (???????(??(?????%)?)(??%?));
    2131       @push_ra_ok
    2132603
    2133604lemma eval_call_ok   :
  • src/joint/Traces.ma

    r2783 r2785  
    7979(*  let ispp : xpointer ≝ mk_pointer ispb (mk_offset (bitvector_of_nat ? 47)) in *)
    8080  let main ≝ prog_main … p in
    81   let st0 ≝ mk_state pars (empty_framesT …) empty_is (BBbit false) (empty_regsT … spp) m in
     81  let st0 ≝ mk_state pars (Some ? (empty_framesT …)) empty_is (BBbit false) (empty_regsT … spp) m in
    8282  (* use exit_pc as ra and call_dest_for_main as dest *)
    8383  let st0' ≝ mk_state_pc … (set_sp … spp st0) exit_pc exit_pc in
Note: See TracChangeset for help on using the changeset viewer.