 Timestamp:
 Mar 6, 2013, 2:58:09 PM (7 years ago)
 Location:
 src
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/ERTL/ERTLtoERTLptrOK.ma
r2783 r2785 14 14 (**************************************************************************) 15 15 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. 16 include "ERTL/ERTLtoERTLptrUtils.ma". 17 18 51 19 52 20 (* … … 68 36 *) 69 37 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: #bo2,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: #bo2,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 1098 40 1099 41 (* … … 1173 115 include "joint/semantics_blocks.ma". 1174 116 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 1242 118 1243 119 lemma as_label_ok : ∀ prog : ertl_program. … … 1283 159 qed. 1284 160 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. 161 include alias "basics/lists/listb.ma". 1317 162 1318 163 lemma eval_seq_no_call_ok : … … 1446 291 qed. 1447 292 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 1453 294 1454 295 (* … … 1462 303 qed.*) 1463 304 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 1728 306 1729 307 lemma eval_return_ok : … … 1869 447 qed. 1870 448 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 1882 450 1883 451 lemma eval_cond_ok : … … 2033 601 qed. 2034 602 2035 lemma block_of_call_ok : ∀prog: ertl_program.2036 let trans_prog ≝ ertl_to_ertlptr prog in2037 ∀ 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 nodelta2046 @mfr_bind12047 [ @(λx.x)2048  cases(called) [#c_id  #c_ptr] normalize nodelta2049 [ @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 assumption2053  @mfr_bind12054 [2: whd in match dpl_arg_retrieve; normalize nodelta @(ps_arg_retrieve_ok) 2055  #bv1 @mfr_bind12056 [2: whd in match dph_arg_retrieve; normalize nodelta @(ps_arg_retrieve_ok) 2057  #bv2 @mfr_bind12058 [ @(λx.x)2059  whd in match pointer_of_bevals; normalize nodelta2060 cases bv1 normalize nodelta2061 [   #ptr1 #ptr2 #p  #by  #p  #ptr #p  #pc1 #p1]2062 try @res_preserve_error12063 [ cases bv2 [   #ptr1' #ptr2' #p'  #by'  #p'  #ptr' #p'  #pc1' #p1']2064 normalize nodelta2065 [1,2,3,4,5: @res_preserve_error12066  @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_error12070 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 nodelta2077 @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 prf2087 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 nodelta2098 @mfr_bind12099 [ @(sigma_state prog f_lbls f_regs restr)2100  >(bvpc_sigma_pc_to_sigma_beval … prf) @push_ok2101  #st' >(bvpc_sigma_pc_to_sigma_beval … prf) @push_ok2102 ] 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)) with2109 [ OK y ⇒ let 〈f,fn〉 ≝ y in2110 let added ≝ added_registers … (prog_var_names … prog) fn2111 (f_regs (pc_block (pc … st))) in2112 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_pc2116 ])2117 (sigma_state prog f_lbls f_regs restr)2118 (ertl_save_frame kind it)2119 (match kind with2120 [ID ⇒ ertlptr_save_frame ID it2121 PTR ⇒ λst. !st' ← push_ra … st (pc … st);2122 ertlptr_save_frame ID it (set_no_pc … st' st)2123 ]).2124 xxxxxxxxxxxxxxxxxxx2125 #prog #f_lbls #f_regs #kind #restr #st whd in match ertl_save_frame;2126 whd in match ertlptr_save_frame; normalize nodelta @mfr_bind12127 [2: cases(fetch_internal_function ???) normalize nodelta2128 [ * #id #fn normalize nodelta2129 2130 change with (st_no_pc … st) in ⊢ (???????(??(?????%)?)(??%?));2131 @push_ra_ok2132 603 2133 604 lemma eval_call_ok : 
src/joint/Traces.ma
r2783 r2785 79 79 (* let ispp : xpointer ≝ mk_pointer ispb (mk_offset (bitvector_of_nat ? 47)) in *) 80 80 let main ≝ prog_main … p in 81 let st0 ≝ mk_state pars ( empty_framesT …) empty_is (BBbit false) (empty_regsT … spp) m in81 let st0 ≝ mk_state pars (Some ? (empty_framesT …)) empty_is (BBbit false) (empty_regsT … spp) m in 82 82 (* use exit_pc as ra and call_dest_for_main as dest *) 83 83 let st0' ≝ mk_state_pc … (set_sp … spp st0) exit_pc exit_pc in
Note: See TracChangeset
for help on using the changeset viewer.