 Timestamp:
 Aug 27, 2013, 6:11:57 PM (6 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ERTL/ERTLToLTLProof.ma
r3372 r3388 42 42 λlocalss,live_fun,color_fun,R,hw1,hw2,mem. 43 43 hwreg_retrieve_sp hw1 = hwreg_retrieve_sp hw2 ∧ 44 ∀r : Register. live_fun (inr ?? r) → hwreg_retrieve hw1 r ≠ BVundef →44 ∀r : Register.r ≠ RegisterCarry → live_fun (inr ?? r) → hwreg_retrieve hw1 r ≠ BVundef → 45 45 match color_fun (inr ?? r) with 46 46 [ decision_colour r' ⇒ R (hwreg_retrieve hw1 r) (hwreg_retrieve hw2 r') … … 129 129 ]. 130 130 131 xxxxxxxxxxxxx 132 131 (* 133 132 let rec frames_relation_aux (prog : ertl_program) (stacksize : ident → option ℕ) 134 133 (color_f : (Σb:block.block_region b=Code) → option (list register → vertex → decision)) … … 163 162 (λd.acc (callee_saved_remap (pc_block (funct_pc hd)) init_regs color_f d)) 164 163 init_regs 165 ]. 166 167 (* 164 ].*) 165 168 166 let rec frames_relation_aux (fix_comp : fixpoint_computer) 169 167 (build : coloured_graph_computer) (prog : ertl_program) (R : beval → beval → Prop) … … 200 198 (λd.acc (callee_saved_remap fix_comp build prog (pc_block (funct_pc hd)) init_regs d)) 201 199 init_regs 202 ]. *)200 ]. 203 201 204 202 definition frames_relation : 203 (* 205 204 ∀prog : ertl_program.(ident → option ℕ) → (beval → beval → Prop) → 206 205 ((Σb:block.block_region b=Code) → option(list register → vertex → decision)) → … … 209 208 λprog,stacksize,R,color_fun,live_fun,frames,regs,m,init_regs. 210 209 frames_relation_aux prog stacksize color_fun live_fun R frames regs m (λx.x) init_regs. 211 212 (* 210 *) 213 211 fixpoint_computer → coloured_graph_computer → 214 212 ertl_program → (beval → beval → Prop) → list ERTL_frame → … … 217 215 frames_relation_aux fix_comp build prog R frames regs m (λx.x) init_regs. 218 216 219 217 (* 220 218 definition register_of_bitvector : BitVector 6 → option Register≝ 221 219 λvect. … … 334 332 335 333 definition gen_state_rel : 336 ∀prog : ertl_program.(ident → option ℕ) → ? → 337 ((Σb:block.block_region b=Code) → option (list register → vertex → decision)) → 338 ((Σb:block.block_region b=Code)→ option (list register → live_type)) → 339 ? → ? → 340 (block → list register) → 341 lbl_funct_type → regs_funct_type → 342 joint_state_relation ERTL_semantics LTL_semantics ≝ 343 λprog,stacksizes,init,color_f,live_f,color_fun,live_fun,init_regs,f_lbls,f_regs,pc,st1,st2. 334 fixpoint_computer → coloured_graph_computer → 335 ertl_program → (block → list register) → lbl_funct_type → regs_funct_type → 336 local_live_type → (vertex → decision) → 337 joint_state_relation ERTL_semantics LTL_semantics ≝ 338 λfix_comp,colour,prog,init_regs,f_lbls,f_regs,live_fun,color_fun,pc,st1,st2. 339 let m1 ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in 340 let stacksizes ≝ lookup_stack_cost … m1 in 344 341 let ge ≝ joint_globalenv ERTL_semantics prog stacksizes in 342 let init ≝ translate_data fix_comp colour in 345 343 ∃f,fn,ssize. 346 344 fetch_internal_function … ge (pc_block pc) = return 〈f,fn〉 ∧ … … 351 349  Some frames ⇒ 352 350 mem_relation prog stacksizes R f st1 (m … st1) (m … st2) ∧ 353 frames_relation prog stacksizes R color_f live_fframes (regs … st2) (m … st2) init_regs ∧354 hw_relation (joint_if_local_stacksize … fn) (live_fun fn (point_of_pc ERTL_semantics pc))355 (color_fun fn)R (\snd (regs … st1)) (regs … st2) (m … st2) ∧351 frames_relation fix_comp colour prog R frames (regs … st2) (m … st2) init_regs ∧ 352 hw_relation (joint_if_local_stacksize … fn) live_fun 353 color_fun R (\snd (regs … st1)) (regs … st2) (m … st2) ∧ 356 354 make_is_relation_from_beval R (istack … st1) (istack … st2) ∧ 357 (live_fun fn (point_of_pc ERTL_semantics pc) 358 (inr ?? RegisterCarry) → carry … st1 = carry … st2) ∧ 355 ((live_fun (inr ?? RegisterCarry)) → carry … st1 ≠ BBundef → carry … st1 = carry … st2) ∧ 359 356 stack_usage … st1 = stack_usage … st2 ∧ 360 357 ∃ptr.sp … st2 = return ptr ∧ 361 358 le ((nat_of_bitvector … (offv (poff … ptr))) + ssize) (2^16 1) ∧ 362 359 plus (nat_of_bitvector … (offv (poff … ptr))) (stack_usage … st2) = 2^16 ∧ 363 ps_relation (joint_if_local_stacksize … fn) 364 (live_fun fn (point_of_pc ERTL_semantics pc)) 365 (color_fun fn) 366 R ptr (\fst (regs … st1)) 〈regs … st2,m … st2〉 360 ps_relation (joint_if_local_stacksize … fn) live_fun 361 color_fun R ptr (\fst (regs … st1)) 〈regs … st2,m … st2〉 367 362 ]. 368 363 … … 374 369 ertl_program → (block → list register) → lbl_funct_type → regs_funct_type → 375 370 joint_state_relation ERTL_semantics LTL_semantics ≝ 376 λfix_comp,build,prog,init_regs,f_lbls,f_regs,pc. 377 let after ≝ λfn,callee.analyse_liveness fix_comp (prog_names … prog) fn callee in 378 let before ≝ λfn,callee.livebefore … fn callee (after fn callee) in 379 let coloured_graph ≝ λfn,callee.build … fn (after fn callee) callee in 371 λfix_comp,build,prog,init_regs,f_lbls,f_regs,pc,st1,st2. 380 372 let m1 ≝ (\snd (\fst (ertl_to_ltl fix_comp build prog))) in 381 373 let stacksizes ≝ lookup_stack_cost … m1 in 382 let init ≝ translate_data fix_comp build in 383 gen_state_rel prog stacksizes init 384 (λbl. 385 match fetch_internal_function … 386 (joint_globalenv ERTL_semantics prog stacksizes) bl with 387 [ OK x ⇒ Some ? (λcallee.colouring … (coloured_graph (\snd x) callee)) 388  Error e ⇒ None ? 389 ]) 390 (λbl. 391 match fetch_internal_function … 392 (joint_globalenv ERTL_semantics prog stacksizes) bl with 393 [ OK x ⇒ Some ? (λcallee,l,v. 394 in_lattice v ((before (\snd x) callee) l) ∧ 395 match v with 396 [ inl r ⇒ true 397  inr R ⇒ all … (λR'.¬ eq_Register R' R) RegisterAlwaysDead 398 ]) 399  Error e ⇒ None ? 400 ]) (λfn.colouring … (coloured_graph fn (init_regs (pc_block pc)))) 401 (λfn,l,v. in_lattice v (before fn (init_regs (pc_block pc)) l) ∧ 402 match v with 374 let ge ≝ joint_globalenv ERTL_semantics prog stacksizes in 375 ∃f,fn. 376 fetch_internal_function … ge (pc_block pc) = return 〈f,fn〉 ∧ 377 let after ≝ analyse_liveness fix_comp (prog_names … prog) fn (init_regs (pc_block pc)) in 378 let before ≝ livebefore … fn (init_regs (pc_block pc)) after in 379 let coloured_graph ≝ build … fn after (init_regs (pc_block pc)) in 380 gen_state_rel fix_comp build prog init_regs f_lbls f_regs 381 (λv.in_lattice v (before (point_of_pc ERTL_semantics pc)) ∧ 382 match v with 403 383 [ inl r ⇒ true 404 384  inr R ⇒ all … (λR'.¬ eq_Register R' R) RegisterAlwaysDead 405 385 ]) 406 init_regs f_lbls f_regs pc. 386 (colouring … coloured_graph) pc st1 st2. 387 407 388 (* 408 389 definition state_rel : fixpoint_computer → coloured_graph_computer → … … 526 507 527 508 lemma ps_reg_retrieve_hw_reg_retrieve_commute : 528 ∀ prog,stacksize,init,color_f,live_f,color_fun,live_fun.509 ∀fix_comp,colour,prog,color_fun,live_fun. 529 510 ∀init_regs : (block → list register).∀f_lbls,f_regs.∀f : ident. 530 511 ∀fn : joint_closed_internal_function ERTL (prog_names … prog). 531 512 ∀pc. 513 let m1 ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in 514 let stacksize ≝ lookup_stack_cost … m1 in 532 515 fetch_internal_function … (joint_globalenv ERTL_semantics prog stacksize) 533 516 (pc_block pc) = return 〈f,fn〉→ 517 let init ≝ translate_data fix_comp colour in 534 518 gen_preserving2 ?? gen_res_preserve ?????? 535 (gen_state_rel prog stacksize init color_f live_f color_fun live_fun init_regs f_lbls f_regspc)519 (gen_state_rel fix_comp colour prog init_regs f_lbls f_regs live_fun color_fun pc) 536 520 (λr,d. 537 bool_to_Prop 538 (live_fun fn (point_of_pc ERTL_semantics pc) 539 (inl ?? r)) ∧ 540 d = 541 (color_fun fn (inl register Register r))) 521 bool_to_Prop (live_fun (inl ?? r)) ∧ 522 d = (color_fun (inl register Register r))) 542 523 (λbv,bv'.bv = sigma_beval prog stacksize init init_regs f_lbls f_regs bv') … 543 524 (λst1.ps_reg_retrieve (regs … st1)) 544 525 (λst,d.m_map Res ?? (\fst …) 545 526 (read_arg_decision (joint_if_local_stacksize ?? fn) st d)). 546 # prog #stacksize #init #color_f #live_f#color_fun #live_fun #init_regs #f_lbls527 #fix_comp #colour #prog #color_fun #live_fun #init_regs #f_lbls 547 528 #f_regs #f #fn #pc #EQfn #st1 #st2 #r #d 548 529 whd in match gen_state_rel; normalize nodelta * #f1 * #fn1 * #ssize … … 1063 1044 qed. 1064 1045 1065 lemma vertex_retrieve_read_arg_decision_commute :1066 ∀prog,stacksize,init,color_f,live_f,color_fun,live_fun.1067 ∀init_regs : (block → list register).∀f_lbls,f_regs.∀f : ident.1068 ∀fn : joint_closed_internal_function ERTL (prog_names … prog).1069 ∀pc.1070 fetch_internal_function … (joint_globalenv ERTL_semantics prog stacksize)1071 (pc_block pc) = return 〈f,fn〉→1072 gen_preserving2 ?? gen_res_preserve ??????1073 (gen_state_rel prog stacksize init color_f live_f color_fun live_fun init_regs f_lbls f_regs pc)1074 (λv,d.1075 bool_to_Prop1076 (live_fun fn (point_of_pc ERTL_semantics pc) v) ∧1077 d =1078 (color_fun fn v))1079 (λx,y.\fst x = sigma_beval prog stacksize init init_regs f_lbls f_regs (\fst y) ∧1080 gen_state_rel prog stacksize init color_f live_f color_fun1081 live_fun init_regs f_lbls f_regs pc (\snd x) (\snd y)) …1082 (λst1,v.! bv ← ertl_vertex_retrieve (regs … st1) v;1083 return〈bv,st1〉)1084 (λst,d.(read_arg_decision (joint_if_local_stacksize ?? fn) st d)).1085 #prog #stacksize #init #color_f #live_f #color_fun #live_fun #init_regs #f_lbls #f_regs1086 #f #fn #pc #EQfn #st1 #st2 *1087 [ @ps_reg_retrieve_hw_reg_retrieve_commute assumption] #R #d * #f1 * #fn1 * #ssize1088 ** >EQfn whd in ⊢ (??%% → ?); #EQ1 destruct(EQ1) #_ cases(st_frms ??) [*] #frames1089 normalize nodelta ***** #_ #H1 #_ #_ #_ #_ * #live_R #EQ destruct(EQ) #bv #EQbv1090 lapply((proj2 ?? H1 …) R live_R ?)1091 [ % #ABS whd in match ertl_vertex_retrieve in EQbv; normalize nodelta in EQbv;1092 >ABS in EQbv; normalize nodelta whd in ⊢ (???% → ?); #EQ destruct(EQ) ]1093 cases(color_fun ??) normalize nodelta [#n1  #R1 ] lapply(ertl_vertex_retrieve_ok_on_hw_regs … EQbv)1094 #EQ destruct(EQ)1095 [ inversion (hwreg_retrieve_sp ?) normalize nodelta [2: #e #_ *] #sp #EQsp1096 inversion(beloadv ??) normalize nodelta [ #_ *] #bv1 #EQbv1 #Hbv1 %{bv1}1097 % [2: assumption] whd in match m_map; whd in match read_arg_decision; normalize nodelta1098 @pair_elim #off_h #off_l #EQoff >m_return_bind >m_return_bind @('bind_inversion EQsp)1099 #ptr1 #EQptr1 @match_reg_elim1100 [2: #_ whd in ⊢ (??%% → ?); #EQ destruct] #prf whd in ⊢ (??%% → ?); #EQ destruct1101 cases(shift_pointer_commute1102 (bitvector_of_nat 16 (joint_if_local_stacksize … fn1 +n1)) (carry … st2) …1103 〈hwreg_retrieve (regs LTL_semantics st2) RegisterSPL,1104 hwreg_retrieve (regs LTL_semantics st2) RegisterSPH〉 …)1105 [3: %1106 5: >EQptr1 in ⊢ (??%?); >m_return_bind whd in match xpointer_of_pointer; normalize nodelta1107 @match_reg_elim [2: >prf in ⊢ (% → ?); #EQ destruct] #prf1 >m_return_bind %1108 *:1109 ]1110 #x * >EQoff normalize nodelta #H @('bind_inversion H) H #val1 #EQval11111 #H @('bind_inversion H) H #val2 #EQval2 #EQx #EQ destruct(EQ)1112 >EQval1 >m_return_bind >EQval2 >m_return_bind >EQx >m_return_bind >EQbv1 >m_return_bind %1113  #EQ %{(hwreg_retrieve (regs … st2) R1)} %{(refl …)} assumption1114 ]1115 qed.1116 1117 1046 lemma hwreg_retrieve_sp_insensitive_to_set_other : ∀b,rgs. 1118 1047 hwreg_retrieve_sp (hwreg_set_other b rgs) = hwreg_retrieve_sp rgs. … … 1129 1058 qed. 1130 1059 1131 lemma shift_pointer_inj : ∀n,ptr.∀b1,b2 : BitVector n. 1132 nat_of_bitvector … (offv (poff … ptr)) + nat_of_bitvector … b1 ≤ 2^16  1 → 1133 nat_of_bitvector … (offv (poff … ptr)) + nat_of_bitvector … b2 ≤ 2^16  1 → 1134 shift_pointer n ptr b1 = shift_pointer n ptr b2 → 1135 b1 = b2. 1060 lemma vertex_retrieve_read_arg_decision_commute : 1061 ∀fix_comp,colour,prog,color_fun,live_fun. 1062 ∀init_regs : (block → list register).∀f_lbls,f_regs.∀f : ident. 1063 ∀fn : joint_closed_internal_function ERTL (prog_names … prog). 1064 ∀pc. 1065 let m1 ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in 1066 let stacksize ≝ lookup_stack_cost … m1 in 1067 fetch_internal_function … (joint_globalenv ERTL_semantics prog stacksize) 1068 (pc_block pc) = return 〈f,fn〉→ 1069 let init ≝ translate_data fix_comp colour in 1070 (∀v.∀R. color_fun v = decision_colour R → R = RegisterDPL ∨ R = RegisterDPH → ¬ live_fun v) → 1071 bool_to_Prop (¬ live_fun (inr ?? RegisterDPL)) → 1072 bool_to_Prop (¬ live_fun (inr ?? RegisterDPH)) → 1073 gen_preserving2 ?? gen_res_preserve ?????? 1074 (gen_state_rel fix_comp colour prog init_regs f_lbls f_regs live_fun color_fun pc) 1075 (λv,d.v ≠ (inr ?? RegisterCarry) ∧ bool_to_Prop(live_fun v) ∧ d = (color_fun v)) 1076 (λx,y.\fst x = sigma_beval prog stacksize init init_regs f_lbls f_regs (\fst y) ∧ 1077 gen_state_rel fix_comp colour prog init_regs f_lbls f_regs 1078 (update_fun … eq_vertex live_fun (inr ?? RegisterCarry) false) 1079 color_fun pc (\snd x) (\snd y)) … 1080 (λst1,v.! bv ← ertl_vertex_retrieve (regs … st1) v; 1081 return〈bv,st1〉) 1082 (λst,d.(read_arg_decision (joint_if_local_stacksize ?? fn) st d)). 1083 #fix_comp #colour #prog #color_fun #live_fun #init_regs #f_lbls #f_regs 1084 #f #fn #pc #EQfn #Hvert #Hdpl #Hdph #st1 #st2 * 1085 [ #r #d #Rst1st2 ** #_ #live_r #colour_d * #bv #st #H @('bind_inversion H) H 1086 #bv1 whd in match ertl_vertex_retrieve; normalize nodelta #EQbv1 1087 whd in ⊢ (??%% → ?); #EQ destruct(EQ) 1088 cases (ps_reg_retrieve_hw_reg_retrieve_commute … EQfn … Rst1st2 … EQbv1) 1089 [3: % assumption 2:] #fbv * whd in match m_map; normalize nodelta 1090 #H @('bind_inversion H) H * #fbv1 #st2' #EQfbv1 whd in ⊢ (??%% → ?); 1091 #EQ destruct(EQ) #EQ destruct(EQ) %{〈fbv,st2'〉} %{EQfbv1} % [%] 1092 whd in match read_arg_decision in EQfbv1; normalize nodelta in EQfbv1; 1093 destruct cases (color_fun ?) in EQfbv1; [#n  #R] normalize nodelta 1094 [2: whd in ⊢ (??%% → ?); #EQ destruct(EQ) 1095  @pair_elim #high #low #EQhl >m_return_bind >m_return_bind #H @('bind_inversion H) H 1096 #val1 #EQval1 #H @('bind_inversion H) H #val2 #EQval2 #H @('bind_inversion H) 1097 H #ptr #EQptr #H @('bind_inversion H) H #fbv1 #H lapply(opt_eq_from_res ???? H) 1098 H #EQfbv1 whd in ⊢ (??%% → ?); #EQ destruct(EQ) whd in match set_carry; 1099 normalize nodelta 1100 ] 1101 cases Rst1st2 #f1 * #fn1 * #ssize ** >EQfn whd in ⊢ (??%% → ?); 1102 #EQ destruct(EQ) #EQssize inversion(st_frms ??) [1,3: #_ *] #frames #EQframes 1103 normalize nodelta ****** #Hmem #Hframes #Hhw #His #Hcarry #Hstack #Hpsregs 1104 %{f1} %{fn1} %{ssize} % [1,3: % assumption] >EQframes normalize nodelta % 1105 [2,4: cases Hpsregs Hpsregs #ptr *** #EQptr #H1 #H2 #H3 %{ptr} % 1106 [1,3: % [2,4: assumption] % [1,2,4: assumption] 1107 change with (hwreg_retrieve_sp ?) in ⊢ (??%?); 1108 >hwreg_retrieve_sp_insensitive_to_regstore 1109 [ >hwreg_retrieve_sp_insensitive_to_regstore [ assumption]] 1110 normalize % #EQ destruct 1111 *: #r1 #d1 * whd in match update_fun; normalize nodelta #r1_live #EQ destruct(EQ) 1112 #bv1 #EQbv1 [ @(H3 … EQbv1) % //] cases(H3 … EQbv1) [3: % [ assumption  % ] 2:] 1113 #bv1' inversion(color_fun ?) [ #n  #R ] #EQcol normalize nodelta * 1114 [ #H lapply(opt_eq_from_res ???? H) H #EQbv1' 1115  whd in ⊢ (??%% → ?); #EQ destruct(EQ) 1116 ] 1117 #EQ destruct(EQ) [ %{bv1'} % [ >EQbv1' %  %]] 1118 %{(hwreg_retrieve (regs … st2) R)} % [2: %] >hwreg_retrieve_hwregstore_miss 1119 [ >hwreg_retrieve_hwregstore_miss [%]] % #H lapply(Hvert … EQcol ?) 1120 [1,3: [%2%] assumption] >r1_live * 1121 ] 1122 *: % [2,4: assumption] % [2,4: *] % [2,4: assumption] % 1123 [2,4: [2: whd >hwreg_retrieve_sp_insensitive_to_regstore 1124 [ >hwreg_retrieve_sp_insensitive_to_regstore ] ] 1125 [2,3,4,5: normalize % #EQ destruct(EQ) *: %{(proj1 ?? Hhw)} ] 1126 #r1 * #r1_no_c whd in match update_fun; normalize nodelta 1127 @eq_vertex_elim [1,3: #EQ destruct(EQ) @⊥ @r1_no_c % ] #_ 1128 normalize nodelta #r1_live #r1_no_undef [2: @(proj2 … Hhw) [%] assumption] 1129 lapply(proj2 ?? Hhw … r1_live r1_no_undef) [% assumption] 1130 inversion(color_fun ?) normalize nodelta [ #n #_ #H @H] 1131 #R1 #HR1 #H >hwreg_retrieve_hwregstore_miss 1132 [ >hwreg_retrieve_hwregstore_miss [ @H ] ] % #H1 1133 lapply(Hvert … HR1 ?) [1,3: [%2%] assumption] >r1_live * 1134 #H1 #H2 assumption 1135 *: % [1,2,3: assumption ] cases daemon (*TODO in a separate lemma *) 1136 ] 1137 ] 1138 ] 1139 #Reg #dec #Rst1st2 *** #Reg_nocarry #Reg_live #EQ destruct(EQ) * #bv #st1' 1140 #H @('bind_inversion H) H #bv1 #EQbv1 whd in ⊢ (??%% → ?); #EQ destruct(EQ) 1141 cases Rst1st2 #f1 * #fn1 * #ssize ** >EQfn whd in ⊢ (??%% → ?); #EQ destruct(EQ) 1142 #EQsszie inversion(st_frms ??) [ #_ *] #frames #EQframes normalize nodelta ****** 1143 #Hmem #Hframes #Hhw #His #Hcarry #Hstack #Hps cut(? : Prop) 1144 [3: #H_nocarry lapply(proj2 ?? Hhw … Reg_live H_nocarry) 1145 [% #EQ destruct(EQ) @Reg_nocarry %] cases(color_fun ?) normalize nodelta 1146 [ #n inversion(hwreg_retrieve_sp ?) normalize nodelta [2: #e #_ *] 1147 #ptr #EQptr inversion(beloadv ??) [#_ *] #bv2 #EQbv2 normalize nodelta 1148 #Hbv2 @('bind_inversion EQptr) #ptr1 #EQptr1 @match_reg_elim 1149 [2: #_ whd in ⊢ (??%% → ?); #EQ destruct(EQ)] #prf whd in ⊢ (??%% → ?); 1150 #EQ destruct(EQ) 1151 cases(shift_pointer_commute (bitvector_of_nat 16 (joint_if_local_stacksize … fn1 +n)) 1152 (carry … st2) … 1153 〈hwreg_retrieve (regs LTL_semantics st2) RegisterSPL, 1154 hwreg_retrieve (regs LTL_semantics st2) RegisterSPH〉 …) 1155 [5: >EQptr1 in ⊢ (??(????%?)?); >m_return_bind whd in match xpointer_of_pointer; 1156 normalize nodelta @match_reg_elim [2: >prf in ⊢ (% → ?); #EQ destruct(EQ)] 1157 #prf1 >m_return_bind % 1158 3: % 1159 *: 1160 ] 1161 @pair_elim #ptr_h #ptr_l #EQvsplit #ptr2 * #H @('bind_inversion H) H #val1 1162 #EQval1 #H @('bind_inversion H) H #val2 #EQval2 #EQptr2 #EQ destruct(EQ) 1163 % 1164 [ % [ @bv2] 1165  % 1166 [ whd in match read_arg_decision; normalize nodelta >EQvsplit in ⊢ (??%?); 1167 normalize nodelta >m_return_bind >m_return_bind >EQval1 in ⊢ (??%?); 1168 >m_return_bind >EQval2 in ⊢ (??%?); >m_return_bind >EQptr2 in ⊢ (??%?); 1169 >m_return_bind >EQbv2 in ⊢ (??%?); % 1170  % [ <Hbv2 whd in match ertl_vertex_retrieve in EQbv1; normalize nodelta in EQbv1; 1171 cases(hwreg_retrieve ??) in EQbv1; normalize nodelta 1172 try (whd in ⊢ (??%% → ?); #EQ destruct(EQ) %) 1173 try (#x1 whd in ⊢ (??%% → ?); #EQ destruct(EQ) %) 1174 try (#x1 #x2 whd in ⊢ (??%% → ?); #EQ destruct(EQ) %) 1175 #x1 #x2 #x3 whd in ⊢ (??%% → ?); #EQ destruct(EQ) % ] 1176 %{f1} %{fn1} %{ssize} % [ %{EQfn} assumption ] >EQframes normalize nodelta 1177 % 1178 [2: cases Hps #ptr3 *** change with (hwreg_retrieve_sp ?) in ⊢ (??%? → ?); 1179 >EQptr in ⊢ (% → ?); whd in ⊢ (??%% → ?); #EQ destruct(EQ) #H1 #H2 #H3 1180 %{(«ptr1,prf»)} whd in match set_regs; normalize nodelta 1181 % 1182 [ % 1183 [ % [2: assumption] change with (hwreg_retrieve_sp ?) in ⊢ (??%?); 1184 >hwreg_retrieve_sp_insensitive_to_regstore 1185 [ >hwreg_retrieve_sp_insensitive_to_regstore [ assumption] ] 1186 % normalize #EQ destruct 1187  assumption 1188 ] 1189 ] 1190 #r1 #d1 * whd in match update_fun; normalize nodelta #live_r1 #EQ destruct(EQ) 1191 #bev #EQbev cases(H3 … (color_fun (inl ?? r1)) … EQbev) [2: %{live_r1} %] 1192 #bev1 inversion(color_fun ?) normalize nodelta [#n #_ #H1 %{bev1} assumption] 1193 #R1 #EQR1 * whd in ⊢ (??%% → ?); #EQ1 #EQ2 destruct %{(hwreg_retrieve (regs … st2) R1)} 1194 % [2: %] >hwreg_retrieve_hwregstore_miss [ >hwreg_retrieve_hwregstore_miss [%]] 1195 % #H lapply(Hvert … EQR1 ?) [1,3: [%2%] assumption ] >live_r1 * 1196  % [2: assumption] % [2: *] % [2: assumption ] % cases daemon (*TODO*) 1197 ] 1198 ] 1199 ] 1200  cases daemon (*TODO*) 1201 ] 1202  1203  whd in match ertl_vertex_retrieve in EQbv1; normalize nodelta in EQbv1; 1204 cases(hwreg_retrieve ??) in EQbv1; normalize nodelta 1205 [ whd in ⊢ (??%% → ?); #EQ destruct(EQ) 1206 *: try( #H1 #H2 #H3 #H4) try( #H1 #H2 #H3) try( #H1 #H2) try( #H1) % #EQ destruct 1207 ] 1208 ] 1209 qed. 1210 1211 definition ertl_vertex_store : vertex → beval → state ERTL_state → state ERTL_state ≝ 1212 λv,bv,st.match v with 1213 [ inl r ⇒ set_regs ERTL_state 〈reg_store r bv (\fst (regs … st)),\snd (regs … st)〉 st 1214  inr r ⇒ set_regs ERTL_state 〈\fst (regs … st),hwreg_store r bv (\snd (regs … st))〉 st 1215 ]. 1216 1217 lemma state_rel_insensitive_to_dead_write_decision : 1218 ∀fix_comp,colour,prog,color_fun,live_fun. 1219 ∀init_regs : (block → list register).∀f_lbls,f_regs.∀f : ident. 1220 ∀fn : joint_closed_internal_function ERTL (prog_names … prog). 1221 ∀pc. 1222 let m1 ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in 1223 let stacksize ≝ lookup_stack_cost … m1 in 1224 fetch_internal_function … (joint_globalenv ERTL_semantics prog stacksize) 1225 (pc_block pc) = return 〈f,fn〉→ 1226 ∀r : Register. 1227 In … RegisterAlwaysDead r → 1228 ∀bv.(∀v.color_fun v = (decision_colour r) → ¬ live_fun v) → 1229 gen_preserving ?? gen_res_preserve ???? 1230 (gen_state_rel fix_comp colour prog init_regs f_lbls f_regs live_fun color_fun pc) 1231 (gen_state_rel fix_comp colour prog init_regs f_lbls f_regs live_fun color_fun pc) 1232 (m_return …) 1233 (λst.write_decision (joint_if_local_stacksize ?? fn) (decision_colour r) bv st). 1234 #fix_comp #colour #prog #color_fun #live_fun #init_regs #f_lbls #f_regs #f #fn #pc 1235 #EQfn #r #r_forb #bv #Hr #st1 #st2 #Rst1st2 #st1' whd in ⊢ (??%% → ?); 1236 #EQ destruct(EQ) % 1237 [2: % [ whd in match write_decision; normalize nodelta >m_return_bind %] ] 1238 cases Rst1st2 #f1 * #fn1 * #ssize ** >EQfn whd in ⊢ (??%% → ?); #EQ destruct(EQ) 1239 #EQssize inversion(st_frms ??); [ #_ * ] #frames #EQframes normalize nodelta 1240 ****** #Hmem #Hframes #Hhw #His #Hcarry #Hstack * #sp *** #EQsp #H1 #H2 #Hps 1241 %{f1} %{fn1} %{ssize} % [ %{EQfn} assumption ] >EQframes normalize nodelta 1242 % 1243 [2: %{sp} % 1244 [ % [2: assumption ] % [2: assumption ] 1245 change with (hwreg_retrieve_sp ?) in ⊢ (??%?); whd in match set_regs; 1246 normalize nodelta >hwreg_retrieve_sp_insensitive_to_regstore 1247 [ assumption ] % #EQ destruct(EQ) cases r_forb 1248 [1,3: normalize #EQ destruct(EQ) ] * 1249 [1,3: normalize #EQ destruct(EQ) ] * 1250 [1,3: normalize #EQ destruct(EQ) ] * 1251 [1,3: normalize #EQ destruct(EQ) ] * 1252 [1,3: normalize #EQ destruct(EQ) ] * 1253  whd #r1 #d1 * #live_r1 #EQ destruct(EQ) #bv1 #EQbv1 1254 cases(Hps … (color_fun (inl ?? r1)) … EQbv1) [2: % // ] 1255 #bv2 inversion(color_fun ?) normalize nodelta 1256 [#n #_ * #EQ1 #EQ2 destruct %{bv2} %{EQ1} % ] 1257 #R #EQR * whd in ⊢ (??%% → ?); #EQ1 #EQ2 destruct 1258 %{(hwreg_retrieve (regs … st2) R)} % [2: %] 1259 whd in match set_regs; normalize nodelta 1260 >hwreg_retrieve_hwregstore_miss [%] % #EQ destruct 1261 lapply(Hr … EQR) >live_r1 * 1262 ] 1263 ] 1264 % [2: assumption] % [2: assumption ] % [2: assumption] cases daemon (*TODO*) 1265 qed. 1266 1267 lemma beloadv_ok_bestorev_ok : 1268 ∀m,ptr,bv,bv'.beloadv m ptr = return bv → 1269 ∃m'.bestorev m ptr bv' = return m'. 1136 1270 cases daemon (*TODO*) 1137 1271 qed. 1272 1273 include alias "arithmetics/nat.ma". 1274 1275 lemma vertex_retrieve_write_decision_commute : 1276 ∀fix_comp,colour,prog,color_fun,live_fun. 1277 ∀init_regs : (block → list register).∀f_lbls,f_regs.∀f : ident. 1278 ∀fn : joint_closed_internal_function ERTL (prog_names … prog). 1279 ∀pc. 1280 let m1 ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in 1281 let stacksize ≝ lookup_stack_cost … m1 in 1282 fetch_internal_function … (joint_globalenv ERTL_semantics prog stacksize) 1283 (pc_block pc) = return 〈f,fn〉→ 1284 let init ≝ translate_data fix_comp colour in 1285 (∀v.∀R. color_fun v = decision_colour R → R = RegisterDPL ∨ R = RegisterDPH → ¬ live_fun v) → 1286 bool_to_Prop (¬ live_fun (inr ?? RegisterDPL)) → 1287 bool_to_Prop (¬ live_fun (inr ?? RegisterDPH)) → 1288 (∀v.∀n : ℕ.color_fun v = decision_spill n → le n (joint_if_stacksize … fn)) → 1289 gen_preserving ?? gen_res_preserve ???? 1290 (λx,y.gen_state_rel fix_comp colour prog init_regs f_lbls f_regs live_fun 1291 color_fun pc (\snd (\fst x)) (\snd (\fst y)) ∧ 1292 (\fst (\fst x)) = sigma_beval prog stacksize init init_regs f_lbls f_regs (\fst (\fst y)) ∧ 1293 (\snd x) ≠ (inr ?? RegisterCarry) ∧ bool_to_Prop(live_fun (\snd x)) ∧ 1294 (\snd y) = (color_fun (\snd x)) ∧ 1295 (∃bv'.ertl_vertex_retrieve (regs … (\snd (\fst x))) (\snd x) = return bv') ∧ 1296 (∀v'.v' ≠ (\snd x) → bool_to_Prop (live_fun v') → color_fun v' = (\snd y) → 1297 False)) 1298 (gen_state_rel fix_comp colour prog init_regs f_lbls f_regs 1299 (update_fun … eq_vertex live_fun (inr ?? RegisterCarry) false) 1300 color_fun pc) … 1301 (λx.return ertl_vertex_store (\snd x) (\fst (\fst x)) (\snd (\fst x))) 1302 (λx.write_decision (joint_if_local_stacksize ?? fn) (\snd x) (\fst (\fst x)) (\snd (\fst x))). 1303 #fix_comp #colour #prog #color_fun #live_fun #init_regs #f_lbls #f_regs #f #fn #pc 1304 #EQfn #Hdpl_dph #dpl_dead #dph_dead #Hspill ** #bv1 #st1 * #r ** #bv2 #st2 #d ******* #f1 * #fn1 * #sszie ** 1305 >EQfn whd in ⊢ (??%% → ?); #EQ destruct(EQ) #EQsszie inversion(st_frms …) [1,3: #_ *] 1306 #frames #EQframes normalize nodelta ****** #Hmem #Hframes #Hhw #His #Hcarry #Hstack 1307 * #sp *** change with (hwreg_retrieve_sp ?) in ⊢ (??%? → ?); #EQsp #H1 #H2 #Hps #EQ destruct(EQ) 1308 [ #_  * #r_nocarry ] #live_r #EQ destruct(EQ) * #bv' #EQbv' #Hinterf #st1' whd in ⊢ (??%% → ?); 1309 whd in match ertl_vertex_store; normalize nodelta #EQ destruct(EQ) 1310 [ cases(Hps … EQbv') [3: % [ assumption  %] *:] #bv'' inversion(color_fun …) 1311 [ #n  #R ] #EQcol normalize nodelta * 1312 [ #H lapply(opt_eq_from_res ???? H) H #EQbv'' 1313  whd in ⊢ (??%% → ?); #EQ1 1314 ] 1315 #EQ2 destruct 1316 [ @('bind_inversion EQsp) #ptr #EQptr @match_reg_elim #prf whd in ⊢ (??%% → ?); #EQ destruct 1317 cases(shift_pointer_commute (bitvector_of_nat 16 (joint_if_local_stacksize … fn1 +n)) 1318 (carry … st2) … 1319 〈hwreg_retrieve (regs LTL_semantics st2) RegisterSPL, 1320 hwreg_retrieve (regs LTL_semantics st2) RegisterSPH〉 …) 1321 [3: % 1322 5: >EQptr in ⊢ (??%?); >m_return_bind whd in match xpointer_of_pointer; normalize nodelta 1323 @match_reg_elim [2: >prf in ⊢ (% → ?); #EQ destruct] #prf' >m_return_bind % 1324 *: 1325 ] 1326 #ptr1 @pair_elim #x1 #x2 #EQx1x2 * #H @('bind_inversion H) H #x1' #EQx1' 1327 #H @('bind_inversion H) H #x2' #EQx2' #EQptr1 #EQ destruct(EQ) 1328 cases(beloadv_ok_bestorev_ok … bv2 … EQbv'') #m' #EQm' 1329 % [2: % 1330 [ whd in match write_decision; normalize nodelta 1331 >EQx1x2 in ⊢ (??%?); normalize nodelta >m_return_bind 1332 >m_return_bind >EQx1' in ⊢ (??%?); >m_return_bind 1333 >EQx2' in ⊢ (??%?); >m_return_bind >EQptr1 in ⊢ (??%?); 1334 >m_return_bind >EQm' in ⊢ (??%?); >m_return_bind % 1335  whd %{f1} %{fn1} %{sszie} % [ % assumption ] >EQframes normalize nodelta 1336 % 1337 [2: %{(«ptr,prf»)} % 1338 [ % [2: assumption] % [2: assumption] 1339 change with (hwreg_retrieve_sp ?) in ⊢ (??%?); whd in match set_m; 1340 whd in match set_regs; normalize nodelta 1341 >hwreg_retrieve_sp_insensitive_to_regstore 1342 [ >hwreg_retrieve_sp_insensitive_to_regstore [assumption]] 1343 % normalize #EQ destruct ] #r1 #d1 * whd in match update_fun; 1344 normalize nodelta #liv_r1 #EQ destruct(EQ) #val1 1345 cut(eq_identifier … r r1 ∨ ¬ eq_identifier … r r1) 1346 [ @eq_identifier_elim #_ // ] @eq_identifier_elim 1347 [ #EQ destruct(EQ) #_ whd in match reg_retrieve; whd in match reg_store; 1348 normalize nodelta >lookup_add_hit whd in ⊢ (??%% → ?); #EQ destruct 1349 %{bv2} >EQcol normalize nodelta % [2: %] whd in match set_m; whd in match set_regs; 1350 normalize nodelta >beloadv_bestorev_hit [%  @EQm' *:] 1351  #r_neq_r1 #_ whd in match reg_retrieve; whd in match reg_store; 1352 normalize nodelta >lookup_add_miss 1353 [2: % #EQ destruct cases r_neq_r1 #H @H %] 1354 change with (ps_reg_retrieve ??) in ⊢ (??%? → ?); 1355 #EQval1 cases(Hps … EQval1) [3: % [ assumption  %] *:] 1356 #val2 inversion(color_fun ?) [ #n1  #R1 ] #col_r1 normalize nodelta * 1357 [ #H lapply(opt_eq_from_res ???? H) H #EQval2  whd in ⊢ (??%% → ?); #EQ1 ] 1358 #EQ2 %{val2} destruct % 1359 [2,4: % 3: >hwreg_retrieve_hwregstore_miss [ >hwreg_retrieve_hwregstore_miss [%]] 1360 % #EQ destruct(EQ) lapply(Hdpl_dph … col_r1 ?) [1,3: [ %2  %] %] 1361 >liv_r1 * ] 1362 whd in match set_m; whd in match set_regs; normalize nodelta 1363 cut(eqb … n n1 ∨ ¬ eqb … n n1) [ @eqb_elim #_ //] 1364 @eqb_elim 1365 [ #EQ destruct(EQ) #_ >(beloadv_bestorev_hit … EQm') 1366 whd in ⊢ (??%%); @eq_f 1367 cases(Hinterf (inl ?? r1) ? liv_r1 ?) 1368 [ % #EQ destruct cases r_neq_r1 #H @H % 1369  >EQcol >col_r1 % 1370 ] 1371  * #n_no_n1 #_ >(beloadv_bestorev_miss … EQm') 1372 [ >EQval2 % ] 1373 % #ABS @n_no_n1 1374 @(injective_plus_r (joint_if_local_stacksize … fn1)) 1375 @(eq_bitvector_of_nat_to_eq … (shift_pointer_injective … ABS)) 1376 whd change with (plus 1 ?) in ⊢ (?%?); 1377 @monotonic_le_plus_r @(transitive_le … H1) 1378 [ cut (joint_if_local_stacksize … fn1 + n ≤ sszie) 1379 [ cases daemon (*TODO an invariant to be added*) ] 1380  cut (joint_if_local_stacksize … fn1 + n1 ≤ sszie) 1381 [ cases daemon (*TODO an invariant to be added*) ] 1382 ] 1383 #H2 @(transitive_le … H2) @le_plus_n 1384 ] 1385 ] 1386  % [2: assumption ] % [2: *] % [2: assumption] % 1387 [2: % [ >(proj1 … Hhw) >hwreg_retrieve_sp_insensitive_to_regstore 1388 [ >hwreg_retrieve_sp_insensitive_to_regstore [%]] normalize % #EQ destruct] 1389 #r1 * #r1_nocarry whd in match update_fun; normalize nodelta @eq_vertex_elim 1390 [ #EQ @⊥ destruct(EQ) @r1_nocarry %] #_ normalize nodelta 1391 #live_r1 #r1_noundef inversion(color_fun ?) 1392 [ #n1  #r1'] #col_r1 normalize nodelta 1393 [ >hwreg_retrieve_sp_insensitive_to_regstore 1394 [ >hwreg_retrieve_sp_insensitive_to_regstore ] 1395 [2,3,4,5: normalize % #EQ destruct] 1396 >EQsp normalize nodelta whd in match set_m; normalize nodelta 1397 cases daemon (*TODO*) 1398  >hwreg_retrieve_hwregstore_miss 1399 [ >hwreg_retrieve_hwregstore_miss ] [2,3: % #EQ destruct(EQ) 1400 lapply(Hdpl_dph … col_r1 ?) [1,3: [ %2  % ] %] >live_r1 * ] 1401 lapply(proj2 … Hhw r1 … live_r1 r1_noundef) [% assumption] 1402 >col_r1 normalize nodelta #H @H 1403 ] 1404  cases daemon (*TODO*) 1405 ] 1406 ] 1407 ] 1408  1409 ] 1410  cases daemon (*TODO*) 1411 ] 1412  cases daemon (*TODO*) 1413 ] 1414 qed. 1415 1416 xxxxxxx 1417 @transitive_le\ 1418 1419 1420 check plus lapply injective_S whd in match injective; 1421 normalize nodelta change with(plus ? 1 ≤ 2 ^16); check injective_plus_l 1422 1423 1424 1425 1426 1427 1428 % 1429 [2,4: % 1430 [1,3: whd in match write_decision; normalize nodelta [2: %] @pair_elim 1431 #h_l #h_h #EQh >m_return_bind >m_return_bind 1432 @('bind_inversion EQsp) #ptr #EQptr @match_reg_elim #prf whd in ⊢ (??%% → ?); 1433 #EQ destruct(EQ) 1434 cases(shift_pointer_commute (bitvector_of_nat 16 (joint_if_local_stacksize … fn1 +n)) 1435 (carry … st2) … 1436 〈hwreg_retrieve (regs LTL_semantics st2) RegisterSPL, 1437 hwreg_retrieve (regs LTL_semantics st2) RegisterSPH〉 …) 1438 [ 1439 1440 inversion(color_fun …) [1,3: #n *: #R ] #EQcol % 1441 [2: % 1442 [ whd in match write_decision; normalize nodelta 1443 1444 1445 [ cases(Hps … EQbv') 1446 1447 1448 1449 #Rst1st2 **** 1450 #EQ destruct(EQ) [ #_  * #r_nocarry] #live_r #EQ destruct(EQ) #Hinterf #st1' 1451 whd in ⊢ (??%% → ?); #EQ destruct(EQ) cases Rst1st2 1452 [ cases(Hps … r) 1453 1454 1455 1456 1457 1458 1138 1459 1139 1460 (* … … 1206 1527 cases daemon qed. *) 1207 1528 1208 lemma move_preserve : 1209 ∀fix_comp,colour,prog,init. 1210 ∀color_f : ((Σb:block.block_region b=Code) → option (list register → vertex → decision)). 1211 ∀live_f : ((Σb:block.block_region b=Code)→ option (list register → live_type)). 1212 ∀color_fun : (joint_closed_internal_function ERTL (prog_names … prog) → vertex → decision). 1213 ∀live_fun : (joint_closed_internal_function ERTL (prog_names … prog) → label → vertex → bool). 1214 let p_out ≝ (\fst (\fst (ertl_to_ltl fix_comp colour prog))) in 1215 let m1 ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in 1216 let stacksizes ≝ lookup_stack_cost … m1 in 1217 ∀init_regs : block → list register.∀f_lbls,f_regs. ∀pc,carry_lives_after. 1218 ∀src,dest : decision. 1219 ∀f.∀fn : joint_closed_internal_function ? (prog_names … prog). 1220 fetch_internal_function … (joint_globalenv ERTL_semantics prog stacksizes) 1221 (pc_block pc) = return 〈f,fn〉 → 1222 ∀v1,v2. color_fun fn v1 = src → 1223 color_fun fn v2 = dest → 1224 v2 ≠ (inr ?? RegisterCarry) → 1225 live_fun fn (point_of_pc ERTL_semantics pc) v1 → 1226 invariant_for_move src → 1227 (∀v. live_fun fn (point_of_pc ERTL_semantics pc) v → 1228 color_fun fn v ≠ decision_colour RegisterDPL ∧ 1229 color_fun fn v ≠ decision_colour RegisterDPH ∧ 1230 color_fun fn v ≠ decision_colour RegisterST1) → 1231 live_fun fn (point_of_pc ERTL_semantics pc) 1232 (inr ?? RegisterCarry) = carry_lives_after → 1233 gen_preserving ?? gen_res_preserve ???? 1234 (λst1,st2. 1235 gen_state_rel prog stacksizes init color_f live_f color_fun live_fun init_regs 1236 f_lbls f_regs pc st1 st2 ∧ 1237 ∃bv.ertl_vertex_retrieve (regs … st1) v1 = return bv ∧ 1238 (∀v.live_fun fn (point_of_pc ERTL_semantics pc) v → v ≠ v1 → v ≠ v2 → 1239 color_fun fn v = dest → 1240 ertl_vertex_retrieve (regs … st1) v = return bv) ∧ 1241 (∀ptr. 1242 sp … st2 = return ptr → 1243 match dest with 1244 [ decision_spill n ⇒ 1245 ∀bv.bestorev (m … st2) 1246 (shift_pointer ? ptr (bitvector_of_nat 16 ((joint_if_local_stacksize … fn) + n))) 1247 bv ≠ None ? 1248  _ ⇒ True 1249 ])) 1250 (gen_state_rel prog stacksizes init color_f live_f 1251 (λfn.update_fun ?? eq_vertex (color_fun fn) v1 dest) 1252 (λfn.update_fun ?? (eq_identifier …) (live_fun fn) (point_of_pc ERTL_semantics pc) 1253 (update_fun ?? eq_vertex (live_fun fn (point_of_pc ERTL_semantics pc)) v2 1254 (eq_decision src dest))) 1255 init_regs f_lbls f_regs pc) 1256 (m_return ??) 1257 (repeat_eval_seq_no_pc LTL_semantics (mk_prog_params LTL_semantics p_out stacksizes) f 1258 (move (prog_names … prog) (joint_if_local_stacksize … fn) carry_lives_after dest src)). 1259 #fix_comp #colour #prog #init #color_f #live_f #color_fun #live_fun #init_regs #f_lbls 1260 #f_regs #pc #carry_live #src #dst #f #fn #EQfn #v1 #v2 #EQsrc 1261 #EQdst * #v2_noCarry #v1_live #Hsrc #dst_spec #EQcarry_live #st1 #st2 * #Rst1st2 * #bv ** #EQbv 1262 #Hv1v2 #Hdst >move_spec [2: assumption] 1263 cases(vertex_retrieve_read_arg_decision_commute … init … EQfn … Rst1st2 … EQbv) 1264 [3: %{v1_live} % 2: ] #bv1 * whd in match m_map; normalize nodelta 1265 #H @('bind_inversion H) H * #bv2 #st2' #EQread_arg whd in ⊢ (??%% → ?); #EQ1 #EQ2 1266 destruct(EQ1 EQ2) cases src in EQsrc Hsrc; normalize nodelta src 1267 [ #n1  #R1 ] #EQcol_src * [2: #R1_noDPL #R1_noDPH ] cases dst in EQdst Hdst Hv1v2 dst_spec; 1268 [1,3: #n2 *: #R2 ] #EQcol_dst normalize nodelta [1,2: #Hn2 *: #_] #Hv1v2 #dst_spec 1269 >EQcol_src in EQread_arg; #EQread_arg >EQread_arg whd in EQread_arg : (??%%); 1270 [2,4: lapply EQread_arg EQread_arg @pair_elim #off_h_src #off_l_src #EQoff_src 1271 >m_return_bind >m_return_bind #H @('bind_inversion H) H #val1_src #EQval1_src 1272 #H @('bind_inversion H) H #val2_src #EQval2_src #H @('bind_inversion H) H 1273 #ptr_shift_src #EQptr_shift_src #H @('bind_inversion H) H #bv_src #H 1274 lapply(opt_eq_from_res ???? H) H #EQbv_src whd in ⊢ (??%% → ?); #EQread_arg ] 1275 destruct(EQread_arg) >m_return_bind #st1' whd in ⊢ (??%% → ?); #EQ destruct(EQ) 1276 cases Rst1st2 #f1 * #fn1 * #ssize ** >EQfn whd in ⊢ (??%% → ?); #EQ1 destruct(EQ1) 1277 #EQssize inversion(st_frms ??) normalize nodelta [1,3,5,7: #_ *] #frames #EQframes ****** 1278 #Hmem #Hframes #Hhw_reg #His #Hcarry #Hsu * #sp *** 1279 change with (hwreg_retrieve_sp ?) in ⊢ (??%? → ?); #EQsp #Hssize #Hstack_usage #Hps_reg 1280 [ @eqb_elim normalize nodelta [ #EQ destruct(EQ) %{st2} %{(refl …)}  * #src_dest_spec ] 1281  @eq_Register_elim normalize nodelta [ #EQ destruct(EQ)  * #R2_noA ] 1282  @eq_Register_elim normalize nodelta [ #EQ destruct(EQ)  * #R1_noA ] 1283  @eq_Register_elim normalize nodelta 1284 [ #EQ destruct(EQ) %{st2'} %{(refl …)} 1285  * #src_dest_spec @eq_Register_elim normalize nodelta [#EQ destruct(EQ)  * #R2_noA >m_return_bind ] 1286 ] 1287 ] 1288 [1,7: @(update_color_lemma … EQfn) 1289 [1,3: @(update_live_fun_lemma … EQfn) [1,3: assumption] @eq_decision_elim 1290 [2,4: * #H @⊥ @H %] #_ normalize nodelta inversion(live_fun ??) 1291 [1,3: #_ @I] normalize nodelta >EQcol_dst normalize nodelta cases v2 in EQcol_dst; [1,3: #r *: #R ] #EQcol_dst #v2_dead 1292 normalize nodelta #bv1 whd in match ertl_vertex_retrieve; normalize nodelta #EQbv1 1293 >EQcol_dst normalize nodelta 1294 [1,3: %{sp} %{EQsp} cases v1 in EQcol_src v1_live EQbv; [1,3: #r1 *: #R1] #EQcol_src 1295 #v1_live whd in match ertl_vertex_retrieve; normalize nodelta 1296 [1,2: #EQbv cases(Hps_reg r1 (decision_spill n2) … EQbv) [2,4: % assumption] #bv2 1297 normalize nodelta 1298 1299 1300 1301 1302 1303 @(update_color_lemma … EQfn) 1304 cases daemon (*TODO: it follows by extensionality: 1305 maybe to be merged with other proof obbligations *) 1306 ] 1307 * #src_dest_spec 1308 1309 1310 [2,4: 1311 1312 1313 [1,3: whd in EQread_arg : (??%%); destruct(EQread_arg) @eq_Register_elim normalize nodelta 1314 [ #EQ destruct(EQ) @('bind_inversion EQsp) #ptr #EQptr @match_reg_elim 1315 [2: #_ whd in ⊢ (??%% → ?); #EQ destruct] #prf whd in ⊢ (??%% → ?); 1316 #EQ destruct(EQ) 1317 cases(shift_pointer_commute 1318 (bitvector_of_nat 16 (joint_if_local_stacksize … fn1 +n2)) (carry … st2') … 1319 〈hwreg_retrieve (regs LTL_semantics st2') RegisterSPL, 1320 hwreg_retrieve (regs LTL_semantics st2') RegisterSPH〉 …) 1321 [3: % 1322 5: >EQptr in ⊢ (??%?); >m_return_bind whd in match xpointer_of_pointer; normalize nodelta 1323 @match_reg_elim [2: >prf in ⊢ (% → ?); #EQ destruct] #prf1 >m_return_bind % 1324 *: 1325 ] 1326 #x * @pair_elim #offh #offl #EQoff #H @('bind_inversion H) H #val1 #EQval1 1327 #H @('bind_inversion H) H #val2 #EQval2 #EQx #EQ destruct(EQ) % 1328 [2: % 1329 [ whd in match write_decision; whd in match set_regs; whd in match set_carry; 1330 normalize nodelta > EQoff in ⊢ (??%?); normalize nodelta 1331 >m_return_bind >m_return_bind >hwreg_retrieve_hwregstore_miss 1332 [ >EQval1 in ⊢ (??%?); >m_return_bind >hwreg_retrieve_hwregstore_miss 1333 [ >EQval2 in ⊢ (??%?); >m_return_bind >EQx in ⊢ (??%?); >m_return_bind 1334 >(opt_to_opt_safe … (Hn2 … EQsp …)) >m_return_bind <commute_if 1335 whd in match set_m; normalize nodelta % 1336 ] 1337 ] 1338 normalize % #EQ destruct 1339  %{f1} %{fn1} %{ssize} % [ %{EQfn EQssize} ] 1340 >EQframes normalize nodelta % 1341 [ % [2: cases carry_live normalize nodelta assumption ] 1342 % [2: whd in match update_fun; normalize nodelta @eq_identifier_elim 1343 [2: * #H @⊥ @H %] #_ normalize nodelta 1344 @eq_vertex_elim [ #EQ destruct @⊥ @v2_noCarry %] #_ 1345 @eq_decision_elim [ #EQ destruct] #_ normalize nodelta 1346 destruct #H >H normalize nodelta @Hcarry assumption ] 1347 % [2: @if_elim #_ assumption ] % 1348 [2: whd in match update_fun; normalize nodelta @eq_identifier_elim 1349 [2: * #H @⊥ @H %] #_ normalize nodelta % 1350 [ cases carry_live normalize nodelta 1351 [ >hwreg_retrieve_sp_insensitive_to_set_other] 1352 >hwreg_retrieve_sp_insensitive_to_regstore 1353 [1,4: >hwreg_retrieve_sp_insensitive_to_regstore 1354 [1,4: >hwreg_retrieve_sp_insensitive_to_regstore 1355 [1,4: @(proj1 … Hhw_reg) ] ] ] 1356 % normalize #EQ destruct 1357  #R' @eq_vertex_elim normalize nodelta [ #_ @eq_decision_elim [#EQ destruct] #_ *] 1358 #v2_noR' #live_R' @eq_vertex_elim 1359 [ #EQ destruct(EQ) normalize nodelta cases carry_live in EQcarry_live; 1360 #EQcarry_live normalize nodelta 1361 [ >hwreg_retrieve_sp_insensitive_to_set_other] 1362 >hwreg_retrieve_sp_insensitive_to_regstore 1363 [1,4: >hwreg_retrieve_sp_insensitive_to_regstore 1364 [1,4: >hwreg_retrieve_sp_insensitive_to_regstore ]] 1365 [1,4: *: % normalize #EQ destruct] 1366 try >EQsp in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ?]); normalize nodelta 1367 @opt_safe_elim #m' #EQm' >(beloadv_bestorev_hit … EQm') 1368 normalize nodelta whd in EQbv : (??%%); 1369 cut(∀A,a1,a2. OK A a1 = OK A a2 → a1 = a2) 1370 [1,3: #H1 #H2 #H3 #H4 destruct %] #AUX 1371 @(AUX … EQbv) 1372  #v1_noR' normalize nodelta 1373 cut(bool_to_Prop(eq_decision (decision_spill n2) (color_fun fn1 (inr ?? R'))) ∨ 1374 bool_to_Prop(¬ eq_decision (decision_spill n2) (color_fun fn1 (inr ?? R')))) 1375 [ @eq_decision_elim #_ [%%%2%]] * 1376 [ @eq_decision_elim [2: #_ *] #EQ lapply(sym_eq ??? EQ) EQ #EQcolR' 1377 #_ >EQcolR' normalize nodelta cases carry_live 1378 [ >hwreg_retrieve_sp_insensitive_to_set_other] 1379 >hwreg_retrieve_sp_insensitive_to_regstore 1380 [1,4: >hwreg_retrieve_sp_insensitive_to_regstore 1381 [1,4: >hwreg_retrieve_sp_insensitive_to_regstore ]] 1382 [1,4: *: % normalize #EQ destruct] 1383 try >EQsp in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ? ]); normalize nodelta 1384 @opt_safe_elim #m' #EQm' >(beloadv_bestorev_hit … EQm') normalize nodelta 1385 lapply(Hv1v2 (inr ?? R') live_R' v1_noR' v2_noR' EQcolR') 1386 whd in match ertl_vertex_retrieve; normalize nodelta 1387 whd in ⊢ (??%% → ?); cut(∀A,a1,a2. OK A a1 = OK A a2 → a1 = a2) 1388 [1,3: #H1 #H2 #H3 #H4 destruct %] #AUX #EQ 1389 >(AUX ??? EQ) % 1390  @eq_decision_elim [ #_ *] #Hnodet_R' #_ inversion(color_fun ??) 1391 [ #n3 #EQn3 normalize nodelta cases carry_live 1392 [ >hwreg_retrieve_sp_insensitive_to_set_other] 1393 >hwreg_retrieve_sp_insensitive_to_regstore 1394 [1,4: >hwreg_retrieve_sp_insensitive_to_regstore 1395 [1,4: >hwreg_retrieve_sp_insensitive_to_regstore ]] 1396 [1,4: *: % normalize #EQ destruct] 1397 try >EQsp in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ? ]); normalize nodelta 1398 @opt_safe_elim #m' #EQm' >(beloadv_bestorev_miss … EQm') 1399 [1,3: lapply(proj2 ?? Hhw_reg R' live_R') >EQn3 normalize nodelta 1400 >EQsp normalize nodelta #H @H ] 1401 % #ABS >EQn3 in Hnodet_R'; * #H @H @eq_f H 1402 @(injective_plus_r … (joint_if_local_stacksize … fn1)) 1403 cut(? : Prop) 1404 [3,6: cut(? : Prop) 1405 [3,6: #H1 #H2 @(eq_bitvector_of_nat_to_eq 16) 1406 [1,4: @H1 2,5: @H2 ] 1407 @(shift_pointer_inj … ABS) >nat_of_bitvector_bitvector_of_nat_inverse 1408 try assumption @(transitive_le … Hssize) 1409 @monotonic_le_plus_r cases daemon (*TODO*) 1410 1,4: 1411 *: cases daemon (*TODO*) 1412 ] 1413 1,4: 1414 *: cases daemon (*TODO*) 1415 ] 1416  #R'' #EQR'' normalize nodelta cases carry_live normalize nodelta 1417 [ >hwreg_retrieve_insensitive_to_set_other ] 1418 >hwreg_retrieve_hwregstore_miss 1419 [1,3: >hwreg_retrieve_hwregstore_miss 1420 [1,3: >hwreg_retrieve_hwregstore_miss 1421 [1,3: lapply(proj2 ?? Hhw_reg R' live_R') > EQR'' 1422 normalize nodelta #H @H ] ] ] 1423 cases(dst_spec … live_R') * >EQR'' * #H1 * #H2 * #H3 % #EQ destruct(EQ) 1424 try(@H1 %) try(@H2 %) try(@H3 %) 1425 1426 1427 [@H3 try @H1 try @H2 try assumption 1428 cases daemon (*hypothesis on colouring function to be added TODO *) 1429 ] 1430 1431 1432 lapply EQssize whd in ⊢ (??%% → ?); 1433 whd in match ertl_to_ltl; normalize nodelta whd in match (stack_cost ??); 1434 whd in ⊢ (??%% → ?); 1435 xxxxxxxx 1436 1437 1438 <EQbv destruct(EQbv) 1439 1440 1441 whd in match hwreg_retrieve_sp; 1442 normalize nodelta 1443 @eq_vertex_elim 1444 1445 1446 1447 1448  normalize nodelta 1449 1450 1451 1452 %{live_fun1} %{color_fun1} % 1453 [% 1454 [ %{EQfn} 1455 1456 1457 1458 cases src in EQsrc Hsrc; src normalize nodelta 1459 [ #n1  #R1 ] #EQcol_src * [2: #R1_noDPL #R1_noDPH] cases dst in EQdst Hdst; 1460 [1,3: #n2 *: #R2 ] #EQcol_dst normalize nodelta [1,2: #Hn2 *: #_] 1461 #st1' whd in ⊢ (??%% → ?); #EQ destruct(EQ) 1462 cases daemon (*TODO*) 1463 qed. 1464 1465 1466 1467 1468 1469 1470 1471 1472 1529 1530 1531 1532 1533 1534 1535 1536 (* 1473 1537 lemma state_rel_insensitive_to_forbidden_Reg : 1474 1538 ∀fix_comp,colour,prog,init_regs,f_lbls,f_regs,pc. … … 1561 1625 ] 1562 1626 qed. 1563 1627 *) 1564 1628 1565 1629 … … 1707 1771 whd in match acca_retrieve; normalize nodelta 1708 1772 change with (ps_reg_retrieve ??) in ⊢ (??%? → ?); 1709 #EQbv #EQb whd in match state_pc_rel; normalize nodelta ** #Rst1st2 #_ #_ 1710 #t_fn #_ #z1 #z2 #z3 #z4 #z5 #z6 #z7 #z8 whd #EQinit_regs 1773 #EQbv #EQb whd in match state_pc_rel; normalize nodelta ** 1774 whd in match state_rel; normalize nodelta * #f1 * #fn1 * 1775 >(proj1 … (fetch_statement_inv … EQfetch)) whd in ⊢ (???% → ?); #EQ destruct(EQ) 1776 #Rst1st2 #_ #_ #t_fn #_ #z1 #z2 #z3 #z4 #z5 #z6 #z7 #z8 whd #EQinit_regs 1711 1777 whd normalize nodelta %{(refl …)} #mid #_ <EQinit_regs 1778 >map_eval_add_dummy_variance_id >move_spec normalize nodelta 1779 [2: whd inversion(colouring …) normalize nodelta [#n #_ @I] #R 1780 #EQR 1781 cases(colouring_is_never_forbidden … (proj1 … (fetch_statement_inv … EQfetch)) … EQR) 1782 #_ * #_ * #H1 * #H2 #_ %{H1 H2} ] 1783 cases(vertex_retrieve_read_arg_decision_commute … (proj1 … (fetch_statement_inv … EQfetch)) … (inl ?? r) … Rst1st2 …) 1784 [2: * 1785 [ #r1 #R #EQR * #EQ destruct 1786 cases(colouring_is_never_forbidden … (proj1 … (fetch_statement_inv … EQfetch)) … EQR) 1787 #_ * #_ * * #H1 * * #H2 #_ @⊥ try( @H1 %) @H2 % 1788  #R1 #R2 >hdw_same_colouring #EQ destruct * #EQ destruct cases(in_lattice …) % 1789 ] 1790 3,4: cases(in_lattice …) % 1791 6: % [2: %] % [ % #EQ destruct] 1792 >(all_used_are_live_before fix_comp … (proj2 … (fetch_statement_inv … EQfetch))) 1793 [%  %  @set_member_singl] 1794 8: whd in match ertl_vertex_retrieve; normalize nodelta >EQbv in ⊢ (??%?); % 1795 *: 1796 ] 1797 * #bv' #st2' * #EQst2' * #EQ destruct(EQ) #Rst1st2' >EQst2' >m_return_bind >m_return_bind 1798 >m_return_bind >m_return_bind 1799 cases(state_rel_insensitive_to_dead_write_decision … (proj1 … (fetch_statement_inv … EQfetch)) … RegisterA … bv' … Rst1st2' … (refl …)) 1800 [2: %% 1801 3: * [#r #EQr cases(colouring_is_never_forbidden … (proj1 … (fetch_statement_inv … EQfetch)) … EQr) * #H @⊥ @H % 1802  #R >hdw_same_colouring #EQ destruct(EQ) whd in match update_fun; normalize nodelta 1803 cases(in_lattice …) % 1804 ] 1805 ] 1806 #st2'' * #EQst2'' #Rst1st2'' >EQst2'' inversion(colouring …) normalize nodelta 1807 [ #n  #R] #EQcol <commute_if % [2,4: %{(refl …)} *:] % 1808 [1,3: %{f1} %{fn1} % [1,3: @if_elim #_ @(proj1 ?? (fetch_statement_inv … EQfetch)) ] 1809 cases Rst1st2'' #f2 * #fn2 * #ssize ** >(proj1 ?? (fetch_statement_inv … EQfetch)) 1810 whd in ⊢ (??%% → ?); #EQ destruct #EQssize inversion(st_frms …) [1,3: #_ *] 1811 #frames #EQframes ****** #Hmem #Hframes #Hhw #His #_ #Hstack * #sp *** #EQsp 1812 #H1 #H2 #Hps %{f2} %{fn2} %{ssize} % 1813 [1,3: @if_elim #_ %{(proj1 … (fetch_statement_inv … EQfetch))} assumption] 1814 >EQframes normalize nodelta % 1815 [2,4: %{sp} 1816 [ @eq_Register_elim 1817 [ #EQ destruct(EQ) 1818 cases(colouring_is_never_forbidden … 1819 (proj1 … (fetch_statement_inv … EQfetch)) … EQcol) 1820 * #ABS #_ @⊥ @ABS % ] 1821 #RnoA normalize nodelta ] % 1822 [2,4: #r1 #d1 * @andb_elim @if_elim <commute_if in ⊢ (% → ?); 1823 whd in match (pc_block ?); >point_of_pc_of_point #r1_live * 1824 [ <commute_if in ⊢ (% → ?); ] whd in match (pc_block ?); #EQ 1825 destruct(EQ) #v1 #EQv1 cases(Hps … EQv1) 1826 [3,6: % [2,4: %] whd in match update_fun; normalize nodelta 1827 whd in match (livebefore ?????); 1828 change with (stmt_at ??? (point_of_pc ERTL_semantics ?)) in 1829 ⊢ (?(?(??match % with [_ ⇒ ?  _ ⇒ ? ])?)); 1830 >(proj2 … (fetch_statement_inv … EQfetch)) normalize nodelta 1831 whd in match statement_semantics; normalize nodelta 1832 @andb_Prop [2,4: @I] 1833 @set_member_union1 @set_member_diff [2,4: @set_member_empty] 1834 @(set_member_subset_if … r1_live) 1835 lapply(included_livebefore_livebeafter_stmt_labels 1836 fix_comp … (init_regs (pc_block (pc … st1))) … 1837 (proj2 ?? (fetch_statement_inv … EQfetch)) 1838 (if b then ltrue else lfalse) ?) 1839 [1,3: cases b normalize nodelta 1840 whd in match stmt_labels; whd in match stmt_explicit_labels; 1841 whd in match step_labels; normalize nodelta 1842 [1,3: >memb_cons [1,3: @I *: @memb_hd] *: >memb_hd @I ] ] 1843 whd in match (l_included ???); cases(set_subset (identifier ?) ??) 1844 [1,3: #_ @I] @if_elim ** 1845 *: 1846 ] 1847 #v1' inversion(colouring …) normalize nodelta 1848 [1,3: #n #EQn * #H1 #EQ destruct(EQ) %{v1'} % [2,4: %] 1849 [ >(commute_if ????? (λx.m LTL_semantics x)) 1850 whd in match (m ??); @if_elim #_ ] 1851 whd in match write_decision in EQst2''; normalize nodelta in EQst2''; 1852 >m_return_bind in EQst2''; whd in ⊢ (??%% → ?); #EQ destruct(EQ) 1853 assumption 1854 *: #R #EQR * whd in ⊢ (??%% → ?); #EQ1 #EQ2 destruct(EQ1 EQ2) 1855 %{(hwreg_retrieve (regs … st2'') R)} % [2,3,4: % ] 1856 @if_elim #_ whd in match set_regs; normalize nodelta 1857 [ >hwreg_retrieve_insensitive_to_set_other ] 1858 >hwreg_retrieve_hwregstore_miss 1859 [1,3: whd in match write_decision in EQst2''; normalize nodelta in EQst2''; 1860 >m_return_bind in EQst2''; whd in ⊢ (??%% → ?); #EQ destruct(EQ) 1861 >hwreg_retrieve_hwregstore_miss [1,3: %] ] 1862 % #EQ destruct(EQ) 1863 cases(colouring_is_never_forbidden … 1864 (proj1 … (fetch_statement_inv … EQfetch)) … EQR) 1865 * #ABS #_ @ABS % 1866 ] 1867 *: % try % try assumption 1868 [1,3: change with (hwreg_retrieve_sp ?) in ⊢ (??%?); 1869 [ @if_elim #_ whd in match set_regs; normalize nodelta 1870 [ >hwreg_retrieve_sp_insensitive_to_set_other ] 1871 >hwreg_retrieve_sp_insensitive_to_regstore 1872 [1,4: whd in match write_decision in EQst2''; 1873 normalize nodelta in EQst2''; >m_return_bind in EQst2''; 1874 whd in ⊢ (??%% → ?); #EQ destruct(EQ) 1875 change with (hwreg_retrieve_sp ?) in EQsp : (??%?); 1876 >hwreg_retrieve_sp_insensitive_to_regstore in EQsp; 1877 [1,4: //] 1878 ] 1879 % normalize #EQ destruct 1880  @eq_Register_elim [2: #_ assumption ] #EQ destruct(EQ) 1881 cases(colouring_is_never_forbidden … 1882 (proj1 … (fetch_statement_inv … EQfetch)) … EQcol) 1883 * #ABS #_ @⊥ @ABS % 1884 ] 1885 *: 1886 1887 1888 1889 1712 1890 cases(ps_reg_retrieve_hw_reg_retrieve_commute prog ???? init_regs f_lbls 1713 1891 f_regs f fn (pc … st1) ?????????)
Note: See TracChangeset
for help on using the changeset viewer.