 Timestamp:
 May 17, 2012, 12:42:14 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Policy.ma
r1956 r1965 294 294 qed. 295 295 296 definition policy_isize_sum ≝296 (* definition policy_isize_sum ≝ 297 297 λprefix:list labelled_instruction.λlabels:label_map.λsigma:ppc_pc_map. 298 298 (\fst sigma) = foldl_strong (option Identifier × pseudo_instruction) … … 304 304 (λppc.jmpeqb long_jump (\snd (bvt_lookup ?? ppc (\snd sigma) 〈0,short_jump〉))) 305 305 (bitvector_of_nat 16 (\fst sigma)) (\snd x))) 306 0. 306 0. *) 307 307 308 308 (* The function that creates the labeltoaddress map *) … … 406 406 qed. 407 407 408 (* The first step of the jump expansion: everything to short. 409 * The third condition of the dependent type implies jump_in_policy; 410 * I've left it in for convenience of typechecking. *) 408 (* The first step of the jump expansion: everything to short. *) 411 409 definition jump_expansion_start: 412 410 ∀program:(Σl:list labelled_instruction.l < 2^16). … … 416 414 [ None ⇒ True 417 415  Some p ⇒ 418 And (And ( out_of_program_none (pi1 ?? program) p)416 And (And (And (And (out_of_program_none (pi1 ?? program) p) 419 417 (jump_not_in_policy (pi1 ?? program) p)) 418 (policy_compact program labels p)) 419 (∀i.i < program → 420 \snd (bvt_lookup … (bitvector_of_nat ? i) (\snd p) 〈0,short_jump〉) = short_jump)) 420 421 (\fst p < 2^16) 421 422 ] ≝ … … 423 424 let final_policy ≝ foldl_strong (option Identifier × pseudo_instruction) 424 425 (λprefix.Σpolicy:ppc_pc_map. 425 And ( out_of_program_none prefix policy)426 And (And (And (out_of_program_none prefix policy) 426 427 (jump_not_in_policy prefix policy)) 428 (policy_compact prefix labels policy)) 429 (∀i.i < prefix → 430 \snd (bvt_lookup … (bitvector_of_nat ? i) (\snd policy) 〈0,short_jump〉) = short_jump)) 427 431 program 428 432 (λprefix.λx.λtl.λprf.λp. … … 456 460  lapply p p generalize in match (foldl_strong ?????); * #p #Hp #hg 457 461 @conj [ @Hp  @not_le_to_lt @leb_false_to_not_le <geb_to_leb @hg ] 458  @conj 462  @conj [ @conj [ @conj 459 463 [ (* out_of_program_none *) 460 464 #i >append_length <commutative_plus #Hi normalize in Hi; #Hi2 … … 475 479 ] 476 480 ] 477 @(proj1 ?? Hpi ? Hi2) @le_S_to_le @le_S_to_le @Hi481 @(proj1 ?? (proj1 ?? (proj1 ?? Hp)) i ? Hi2) @le_S_to_le @le_S_to_le @Hi 478 482 38,39,40,41,42,43,44,45,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74: 479 483 [1,2,3,6,7,24,25: #x #y … … 490 494 ] 491 495 ] 492 <Hi @(proj1 ?? Hp(S (prefix)) (le_S ?? (le_n (prefix))) ?)496 <Hi @(proj1 ?? (proj1 ?? (proj1 ?? Hp)) (S (prefix)) (le_S ?? (le_n (prefix))) ?) 493 497 >Hi @Hi2 494 498 9,10,11,12,13,14,15,16,17: … … 500 504 ] 501 505 1,3,5,7,9,11,13,15,17: 502 @(proj1 ?? Hpi ? Hi2) @le_S_to_le @le_S_to_le @Hi506 @(proj1 ?? (proj1 ?? (proj1 ?? Hp)) i ? Hi2) @le_S_to_le @le_S_to_le @Hi 503 507 ] 504 508 46,47,48,49,50,51,52,53,54: … … 510 514 ] 511 515 1,3,5,7,9,11,13,15,17: 512 @(proj1 ?? Hpi ? Hi2) <Hi @le_S @le_n516 @(proj1 ?? (proj1 ?? (proj1 ?? Hp)) i ? Hi2) <Hi @le_S @le_n 513 517 ] 514 518 ] … … 522 526 ] 523 527 ] 524 [1,3,4: @(proj1 ?? Hpi ? Hi2) @le_S_to_le @le_S_to_le @Hi528 [1,3,4: @(proj1 ?? (proj1 ?? (proj1 ?? Hp)) i ? Hi2) @le_S_to_le @le_S_to_le @Hi 525 529 2,5,6: 526 <Hi @(proj1 ?? Hp(S (prefix)) (le_S ?? (le_n (prefix))) ?)530 <Hi @(proj1 ?? (proj1 ?? (proj1 ?? Hp)) (S (prefix)) (le_S ?? (le_n (prefix))) ?) 527 531 >Hi @Hi2 528 532 ] … … 535 539 9,12: @sym_neq @lt_to_not_eq <Hi @le_n 536 540 ] 537 1,3: @(proj1 ?? Hpi ? Hi2) @le_S_to_le @le_S_to_le @Hi538 5,7: @(proj1 ?? Hpi ? Hi2) <Hi @le_S @le_n541 1,3: @(proj1 ?? (proj1 ?? (proj1 ?? Hp)) i ? Hi2) @le_S_to_le @le_S_to_le @Hi 542 5,7: @(proj1 ?? (proj1 ?? (proj1 ?? Hp)) i ? Hi2) <Hi @le_S @le_n 539 543 ] 540 544 ] … … 547 551 4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] >lookup_insert_miss 548 552 [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55: 549 >(nth_append_first ? i prefix ?? Hi) @((proj2 ?? Hp) i Hi)553 >(nth_append_first ? i prefix ?? Hi) @((proj2 ?? (proj1 ?? (proj1 ?? Hp))) i Hi) 550 554 2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56: 551 555 @bitvector_of_nat_abs … … 562 566 9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] >lookup_insert_miss 563 567 [1,3,5,7,9,11,13,15,17: 564 >(nth_append_first ? i prefix ?? Hi) @((proj2 ?? Hp) i Hi)568 >(nth_append_first ? i prefix ?? Hi) @((proj2 ?? (proj1 ?? (proj1 ?? Hp))) i Hi) 565 569 2,4,6,8,10,12,14,16,18: 566 570 @bitvector_of_nat_abs … … 578 582 2,3,4,5,6: #x [5: #y] >lookup_insert_miss 579 583 [1,3,5,7,9: 580 >(nth_append_first ? i prefix ?? Hi) @((proj2 ?? Hp) i Hi)584 >(nth_append_first ? i prefix ?? Hi) @((proj2 ?? (proj1 ?? (proj1 ?? Hp))) i Hi) 581 585 2,4,6,8,10: 582 586 @bitvector_of_nat_abs … … 608 612 ] 609 613 ] 610  @conj 614  (* policy_compact *) cases daemon (*XXX*) 615 ] 616  (* lookup = short_jump *) #i >append_length <commutative_plus #Hi normalize in Hi; 617 cases p p #p cases p p #pc #sigma #Hp cases x 618 #lbl #instr cases instr normalize nodelta 619 [ #pi cases pi normalize nodelta 620 [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37: 621 [1,2,3,6,7,24,25: #x #y 622 4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] 623 cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi 624 [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55: 625 >lookup_insert_miss 626 [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55: 627 @((proj2 ?? Hp) i Hi) 628 2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56: 629 @bitvector_of_nat_abs 630 [1,4,7,10,13,16,19,22,25,28,31,34,37,40,43,46,49,52,55,58,61,64,67,70,73,76,79,82: 631 @(transitive_lt … (pi2 ?? program)) >prf >append_length >commutative_plus 632 @le_plus_a @Hi 633 2,5,8,11,14,17,20,23,26,29,32,35,38,41,44,47,50,53,56,59,62,65,68,71,74,77,80,83: 634 @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm @le_S_S 635 @le_plus_n_r 636 3,6,9,12,15,18,21,24,27,30,33,36,39,42,45,48,51,54,57,60,63,66,69,72,75,78,81,84: 637 @lt_to_not_eq @Hi 638 ] 639 ] 640 2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56: 641 >Hi >lookup_insert_hit @refl 642 ] 643 9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] 644 cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi 645 [1,3,5,7,9,11,13,15,17: >lookup_insert_miss 646 [1,3,5,7,9,11,13,15,17: @((proj2 ?? Hp) i Hi) 647 2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs 648 [1,4,7,10,13,16,19,22,25: @(transitive_lt … (pi2 ?? program)) >prf 649 >append_length >commutative_plus @le_plus_a @Hi 650 2,5,8,11,14,17,20,23,26: @(transitive_lt … (pi2 ?? program)) >prf 651 >append_length <plus_n_Sm @le_S_S @le_plus_n_r 652 3,6,9,12,15,18,21,24,27: @lt_to_not_eq @Hi 653 ] 654 ] 655 2,4,6,8,10,12,14,16,18: >Hi >lookup_insert_hit @refl 656 ] 657 ] 658 2,3,4,5,6: #x [5: #y] cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi 659 [1,3,5,7,9: >lookup_insert_miss 660 [1,3,5,7,9: @((proj2 ?? Hp) i Hi) 661 2,4,6,8,10: @bitvector_of_nat_abs 662 [1,4,7,10,13: @(transitive_lt … (pi2 ?? program)) >prf >append_length 663 >commutative_plus @le_plus_a @Hi 664 2,5,8,11,14: @(transitive_lt … (pi2 ?? program)) >prf >append_length 665 <plus_n_Sm @le_S_S @le_plus_n_r 666 3,6,9,12,15: @lt_to_not_eq @Hi 667 ] 668 ] 669 2,4,6,8,10: >Hi >lookup_insert_hit @refl 670 ] 671 ] 672 ] 673  @conj [ @conj [ @conj 611 674 [ #i #_ #Hi2 / by refl/ 675  #i #H @⊥ @(absurd … H) @not_le_Sn_O 676 ] 677  #i #H @⊥ @(absurd … H) @not_le_Sn_O 678 ] 612 679  #i #H @⊥ @(absurd … H) @not_le_Sn_O 613 680 ] … … 770 837 29,30: cases x #ad cases ad #a1 #a2 771 838 [1,3: cases a2 #ad2 cases ad2 772 [1,8,20,27: #b #Hb normalize @le_S @le_S @le_S @le_S @le_S @le_n (* auto inexplicably takes a long time here *)839 [1,8,20,27: #b #Hb / by le_n/ 773 840 2,3,4,9,15,16,17,18,19,21,22,23,28,34,35,36,37,38: #b] #Hb cases Hb 774 841 2,4: cases a1 #ad1 cases ad1 775 [2,4,21,23: #b #Hb normalize @le_S @le_S @le_S @le_S @le_S @le_n842 [2,4,21,23: #b #Hb / by le_n/ 776 843 1,3,8,9,15,16,17,18,19,20,22,27,28,34,35,36,37,38: #b] #Hb cases Hb 777 844 ] … … 807 874 (* One step in the search for a jump expansion fixpoint. *) 808 875 definition jump_expansion_step: ∀program:(Σl:list labelled_instruction.l < 2^16). 809 ∀labels:(Σlm:label_map. ∀i:ℕ.lt i (program) →810 ∀l.occurs_exactly_once ?? l program →811 is_label (nth i ? program 〈None ?, Comment [ ]〉) l →812 lookup … lm l = Some ? i).876 ∀labels:(Σlm:label_map.∀l. 877 occurs_exactly_once ?? l program → 878 bitvector_of_nat ? (lookup_def … lm l 0) = 879 address_of_word_labels_code_mem program l). 813 880 ∀old_policy:(Σpolicy:ppc_pc_map. 814 881 And (And (out_of_program_none program policy) … … 1132 1199 ] 1133 1200 qed. 1134 1135 1136 (* old proof  lapply (pi2 ?? acc) >p #Hpolicy normalize nodelta in Hpolicy; 1137 cases (dec_eq_jump_length new_length old_length) #Hlength normalize nodelta 1138 @conj [1,3: @conj [1,3: @conj [1,3: @conj [1,3: @conj [1,3: @conj 1139 [1,3: (* out_of_policy_none *) 1140 #i >append_length <commutative_plus #Hi normalize in Hi; 1141 #Hi2 >lookup_opt_insert_miss 1142 [1,3: @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) i (le_S_to_le … Hi)) @Hi2 1143 2,4: >eq_bv_sym @bitvector_of_nat_abs 1144 [1,4: @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm 1145 @le_S_S @le_plus_n_r 1146 2,5: @Hi2 1147 3,6: @lt_to_not_eq @Hi 1148 ] 1149 ] 1150 2,4: (* labels_okay *) 1151 @lookup_forall #i cases i i #i cases i i #p #a #j #n #Hl 1152 elim (insert_lookup_opt ?? 〈p,a,j〉 ???? Hl) Hl #Hl 1153 [1,3: elim (forall_lookup … (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))) ? n Hl) 1154 #i #Hi @(ex_intro ?? i Hi) 1155 2,4: normalize nodelta normalize nodelta in p2; cases instr in p2; 1156 [2,3,8,9: #x #abs normalize nodelta in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H) 1157 6,12: #x #y #abs normalize nodelta in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H) 1158 1,7: #pi cases pi 1159 [35,36,37,72,73,74: #abs normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H) 1160 1,2,3,6,7,33,34,38,39,40,43,44,70,71: 1161 #x #y #abs normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H) 1162 4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,41,42,45,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69: 1163 #x #abs normalize in abs;lapply (jmeq_to_eq ??? abs) #H destruct (H) 1164 9,10,14,15,46,47,51,52: 1165 #id normalize nodelta whd in match (jump_expansion_step_instruction ???); 1166 whd in match (select_reljump_length ???); >p3 1167 lapply (refl ? (lookup_def ?? (pi1 ?? labels) id 〈0,\fst pol〉)) 1168 cases (lookup_def ?? labels id 〈0,\fst pol〉) in ⊢ (???% → %); #q1 #q2 1169 normalize nodelta #H 1170 >(pair_eq1 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) 1171 >(pair_eq2 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) lapply (refl ? (leb (\fst pol) q2)) 1172 cases (leb (\fst pol) q2) in ⊢ (???% → %); #Hle1 1173 [1,3,5,7,9,11,13,15: lapply (refl ? (leb (q2\fst pol) 126)) cases (leb (q2\fst pol) 126) in ⊢ (???% → %); 1174 2,4,6,8,10,12,14,16: lapply (refl ? (leb (\fst polq2) 129)) cases (leb (\fst polq2) 129) in ⊢ (???% → %); 1175 ] 1176 #Hle2 normalize nodelta #Hli @(ex_intro ?? id) >H 1177 <(pair_eq1 ?????? (Some_eq ??? Hli)) @refl 1178 11,12,13,16,17,48,49,50,53,54: 1179 #x #id normalize nodelta whd in match (jump_expansion_step_instruction ???); 1180 whd in match (select_reljump_length ???); >p3 1181 lapply (refl ? (lookup_def ?? labels id 〈0,\fst pol〉)) 1182 cases (lookup_def ?? labels id 〈0,\fst pol〉) in ⊢ (???% → %); #q1 #q2 1183 normalize nodelta #H 1184 >(pair_eq1 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) 1185 >(pair_eq2 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) lapply (refl ? (leb (\fst pol) q2)) 1186 cases (leb (\fst pol) q2) in ⊢ (???% → %); #Hle1 1187 [1,3,5,7,9,11,13,15,17,19: lapply (refl ? (leb (q2\fst pol) 126)) cases (leb (q2\fst pol) 126) in ⊢ (???% → %); 1188 2,4,6,8,10,12,14,16,18,20: lapply (refl ? (leb (\fst polq2) 129)) cases (leb (\fst polq2) 129) in ⊢ (???% → %); 1189 ] 1190 #Hle2 normalize nodelta #Hli @(ex_intro ?? id) >H 1191 <(pair_eq1 ?????? (Some_eq ??? Hli)) @refl 1192 ] 1193 4,5,10,11: #id normalize nodelta whd in match (select_jump_length ???); 1194 whd in match (select_call_length ???); >p3 1195 lapply (refl ? (lookup_def ?? labels id 〈0,\fst pol〉)) 1196 cases (lookup_def ?? labels id 〈0,\fst pol〉) in ⊢ (???% → %); #q1 #q2 1197 normalize nodelta #H 1198 [1,3: cases (leb (\fst pol) q2) 1199 [1,3: cases (leb (q2\fst pol) 126) 2,4: cases (leb (\fst polq2) 129) ] 1200 [1,3,5,7: normalize nodelta #H2 >(pair_eq1 ?????? (Some_eq ??? H2)) in H; 1201 #Hli @(ex_intro ?? id) lapply (proj2 ?? Hl) 1202 #H >(pair_eq1 ?????? (pair_eq1 ?????? H)) 1203 >(pair_eq2 ?????? (pair_eq1 ?????? H)) >Hli @refl] 1204 ] 1205 cases (split ? 5 11 (bitvector_of_nat 16 q2)) #n1 #n2 1206 cases (split ? 5 11 (bitvector_of_nat 16 (\fst pol))) #m1 #m2 1207 normalize nodelta cases (eq_bv ? n1 m1) 1208 normalize nodelta #H2 >(pair_eq1 ?????? (Some_eq ??? H2)) in H; #H 1209 @(ex_intro ?? id) lapply (proj2 ?? Hl) #H2 1210 >(pair_eq1 ?????? (pair_eq1 ?????? H2)) >(pair_eq2 ?????? (pair_eq1 ?????? H2)) 1211 >H @refl 1212 ] 1213 ] 1214 ] 1215 2,4: (* jump_in_policy *) 1216 #i #Hi cases (le_to_or_lt_eq … Hi) Hi; 1217 [1,3: >append_length <commutative_plus #Hi normalize in Hi; 1218 >(nth_append_first ?? prefix ??(le_S_S_to_le ?? Hi)) @conj 1219 [1,3: #Hj lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) i (le_S_S_to_le … Hi)) 1220 #Hacc elim (proj1 ?? Hacc Hj) #h #n elim n n #n #H elim H H #j #Hj 1221 @(ex_intro ?? h (ex_intro ?? n (ex_intro ?? j ?))) whd in match (snd ???); 1222 >lookup_opt_insert_miss [1,3: @Hj 2,4: @bitvector_of_nat_abs ] 1223 [3,6: @(lt_to_not_eq i (prefix)) @(le_S_S_to_le … Hi) 1224 1,4: @(transitive_lt ??? (le_S_S_to_le ?? Hi)) 1225 ] 1226 @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm 1227 @le_S_S @le_plus_n_r 1228 2,4: lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) i (le_S_S_to_le … Hi)) 1229 #Hacc #H elim H H; #h #H elim H H; #n #H elim H H #j #Hl 1230 @(proj2 ?? Hacc) @(ex_intro ?? h (ex_intro ?? n (ex_intro ?? j ?))) 1231 <Hl @sym_eq @lookup_opt_insert_miss @bitvector_of_nat_abs 1232 [3,6: @lt_to_not_eq @(le_S_S_to_le … Hi) 1233 1,4: @(transitive_lt ??? (le_S_S_to_le ?? Hi)) 1234 ] 1235 @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm 1236 @le_S_S @le_plus_n_r 1237 ] 1238 2,4: >append_length <commutative_plus #Hi normalize in Hi; >(injective_S … Hi) 1239 >(nth_append_second ?? prefix ?? (le_n (prefix))) 1240 <minus_n_n whd in match (nth ????); normalize nodelta in p2; cases instr in p2; 1241 [1,7: #pi  2,3,8,9: #x  4,5,10,11: #id  6,12: #x #y] #Hinstr @conj normalize nodelta 1242 [5,7,9,11,21,23: #H @⊥ @H (* instr is not a jump *) 1243 6,8,10,12,22,24: normalize nodelta in Hinstr; lapply (jmeq_to_eq ??? Hinstr) 1244 #H destruct (H) 1245 13,15,17,19: (* instr is a jump *) #_ @(ex_intro ?? (\fst pol)) 1246 @(ex_intro ?? addr) @(ex_intro ?? (max_length old_length ai)) 1247 @lookup_opt_insert_hit 1248 14,16,18,20: #_ / by I/ 1249 1,2,3,4: cases pi in Hinstr; 1250 [35,36,37,109,110,111: #Hinstr #H @⊥ @H 1251 4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,78,79,82,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106: 1252 #x #Hinstr #H @⊥ @H 1253 1,2,3,6,7,33,34,75,76,77,80,81,107,108: #x #y #Hinstr #H @⊥ @H 1254 9,10,14,15,83,84,88,89: #id #Hinstr #_ 1255 @(ex_intro ?? (\fst pol)) @(ex_intro ?? addr) @(ex_intro ?? (max_length old_length ai)) 1256 @lookup_opt_insert_hit 1257 11,12,13,16,17,85,86,87,90,91: #x #id #Hinstr #_ 1258 @(ex_intro ?? (\fst pol)) @(ex_intro ?? addr) @(ex_intro ?? (max_length old_length ai)) 1259 @lookup_opt_insert_hit 1260 72,73,74,146,147,148: #Hinstr lapply (jmeq_to_eq ??? Hinstr) #H normalize in H; destruct (H) 1261 41,42,45,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,115,116,119,129,130,131,132,133,134,135,136,137,138,139,140,141,142,143: 1262 #x #Hinstr lapply (jmeq_to_eq ??? Hinstr) #H normalize in H; destruct (H) 1263 38,39,40,43,44,70,71,112,113,114,117,118,144,145: #x #y #Hinstr lapply (jmeq_to_eq ??? Hinstr) #H 1264 normalize in H; destruct (H) 1265 46,47,51,52,120,121,125,126: #id #Hinstr #_ / by I/ 1266 48,49,50,53,54,122,123,124,127,128: #x #id #Hinstr #_ / by I/ 1267 ] 1268 ] 1269 ] 1270 ] 1271 2,4: (* policy increase *) 1272 #i >append_length >commutative_plus #Hi normalize in Hi; 1273 cases (le_to_or_lt_eq … Hi) Hi; #Hi 1274 [1,3: >lookup_insert_miss 1275 [1,3: @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))) i (le_S_S_to_le … Hi)) 1276 2,4: @bitvector_of_nat_abs 1277 [3,6: @lt_to_not_eq @(le_S_S_to_le … Hi) 1278 1,4: @(transitive_lt ??? (le_S_S_to_le … Hi)) 1279 ] 1280 @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm 1281 @le_S_S @le_plus_n_r 1282 ] 1283 2: >(injective_S … Hi) normalize nodelta in Hlength; >lookup_insert_hit normalize nodelta 1284 >Hlength @pair_elim #l1 #l2 #Hl @pair_elim #y1 #y2 #Hy 1285 >Hl %2 @refl 1286 4: cases daemon (* XXX get rest of proof done first *) 1287 ] 1288 ] 1289 2,4: (* policy_safe *) 1290 @lookup_forall #x cases x x #x cases x x #p #a #j #n normalize nodelta #Hl 1291 elim (insert_lookup_opt ?? 〈p,a,j〉 ???? Hl) Hl #Hl 1292 [1,3: @(forall_lookup … (proj2 ?? (proj1 ?? (proj1 ?? Hpolicy))) ? n Hl) 1293 2,4: normalize nodelta in p2; cases instr in p2; 1294 [2,3,8,9: #x #abs normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H) 1295 6,12: #x #y #abs normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H) 1296 1,7: #pi cases pi normalize nodelta 1297 [35,36,37,72,73,74: #abs normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H) 1298 4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,41,42,45,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69: 1299 #x #abs normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H) 1300 1,2,3,6,7,33,34,38,39,40,43,44,70,71: 1301 #x #y #abs normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H) 1302 9,10,14,15,46,47,51,52: #id >p3 whd in match (jump_expansion_step_instruction ???); 1303 whd in match (select_reljump_length ???); 1304 cases (lookup_def ?? labels id 〈0,\fst pol〉) #q1 #q2 normalize nodelta 1305 >(pair_eq1 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) 1306 >(pair_eq2 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) lapply (refl ? (leb (\fst pol) q2)) 1307 cases (leb (\fst pol) q2) in ⊢ (???% → %); #Hle1 1308 [1,3,5,7,9,11,13,15: lapply (refl ? (leb (q2\fst pol) 126)) cases (leb (q2\fst pol) 126) in ⊢ (???% → %); 1309 2,4,6,8,10,12,14,16: lapply (refl ? (leb (\fst polq2) 129)) cases (leb (\fst polq2) 129) in ⊢ (???% → %); 1310 ] 1311 #Hle2 normalize nodelta #Hli 1312 <(pair_eq1 ?????? (Some_eq ??? Hli)) >Hle1 1313 >(pair_eq2 ?????? (proj2 ?? Hl)) <(pair_eq2 ?????? (Some_eq ??? Hli)) 1314 cases (\snd (lookup ?? (bitvector_of_nat ? (prefix)) (\snd old_policy) ?)) 1315 [1,7,13,19,25,31,37,43,49,55,61,67,73,79,85,91: @(leb_true_to_le … Hle2) 1316 ] normalize @I (* much faster than / by I/, strangely enough *) 1317 11,12,13,16,17,48,49,50,53,54: #x #id >p3 whd in match (jump_expansion_step_instruction ???); 1318 whd in match (select_reljump_length ???); 1319 cases (lookup_def ?? labels id 〈0,\fst pol〉) #q1 #q2 normalize nodelta 1320 >(pair_eq1 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) 1321 >(pair_eq2 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) lapply (refl ? (leb (\fst pol) q2)) 1322 cases (leb (\fst pol) q2) in ⊢ (???% → %); #Hle1 1323 [1,3,5,7,9,11,13,15,17,19: lapply (refl ? (leb (q2\fst pol) 126)) cases (leb (q2\fst pol) 126) in ⊢ (???% → %); 1324 2,4,6,8,10,12,14,16,18,20: lapply (refl ? (leb (\fst polq2) 129)) cases (leb (\fst polq2) 129) in ⊢ (???% → %); 1325 ] 1326 #Hle2 normalize nodelta #Hli 1327 <(pair_eq1 ?????? (Some_eq ??? Hli)) >Hle1 >(pair_eq2 ?????? (proj2 ?? Hl)) 1328 <(pair_eq2 ?????? (Some_eq ??? Hli)) 1329 cases (\snd (lookup ?? (bitvector_of_nat ? (prefix)) (\snd old_policy) ?)) 1330 [1,7,13,19,25,31,37,43,49,55,61,67,73,79,85,91,97,103,109,115: @(leb_true_to_le … Hle2) 1331 ] normalize @I (* vide supra *) 1332 ] 1333 4,5,10,11: #id >p3 normalize nodelta whd in match (select_jump_length ???); 1334 whd in match (select_call_length ???); cases (lookup_def ?? labels id 〈0,\fst pol〉) 1335 #q1 #q2 normalize nodelta 1336 >(pair_eq1 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) 1337 >(pair_eq2 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) 1338 [1,3: lapply (refl ? (leb (\fst pol) q2)) cases (leb (\fst pol) q2) in ⊢ (???% → %); #Hle1 1339 [1,3: lapply (refl ? (leb (q2\fst pol) 126)) cases (leb (q2\fst pol) 126) in ⊢ (???% → %); 1340 2,4: lapply (refl ? (leb (\fst polq2) 129)) cases (leb (\fst polq2) 129) in ⊢ (???% → %); 1341 ] 1342 #Hle2 normalize nodelta 1343 ] 1344 [2,4,6,8,9,10: lapply (refl ? (split ? 5 11 (bitvector_of_nat ? q2))) 1345 cases (split ??? (bitvector_of_nat ? q2)) in ⊢ (???% → %); #x1 #x2 #Hle3 1346 lapply (refl ? (split ? 5 11 (bitvector_of_nat ? (\fst pol)))) 1347 cases (split ??? (bitvector_of_nat ? (\fst pol))) in ⊢ (???% → %); #y1 #y2 #Hle4 1348 normalize nodelta lapply (refl ? (eq_bv 5 x1 y1)) 1349 cases (eq_bv 5 x1 y1) in ⊢ (???% → %); #Hle5 1350 ] 1351 #Hli <(pair_eq1 ?????? (Some_eq ??? Hli)) >(pair_eq2 ?????? (proj2 ?? Hl)) 1352 <(pair_eq2 ?????? (Some_eq ??? Hli)) 1353 cases (\snd (lookup ?? (bitvector_of_nat ? (prefix)) (\snd old_policy) ?)) 1354 [2,8,14,20,26,32: >Hle3 @Hle5 1355 37,40,43,46: >Hle1 @(leb_true_to_le … Hle2) 1356 ] normalize @I (* here too *) 1357 ] 1358 ] 1359 ] 1360 2,4: (* changed *) 1361 normalize nodelta #Hc [2: destruct (Hc)] #i #Hi cases (le_to_or_lt_eq … Hi) Hi 1362 >append_length >commutative_plus #Hi 1363 normalize in Hi; 1364 [ >lookup_insert_miss 1365 [ @(proj2 ?? (proj1 ?? Hpolicy) Hc i (le_S_S_to_le … Hi)) 1366  @bitvector_of_nat_abs 1367 [3: @lt_to_not_eq @(le_S_S_to_le … Hi) 1368 1: @(transitive_lt ??? (le_S_S_to_le … Hi)) 1369 ] 1370 @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm 1371 @le_S_S @le_plus_n_r 1372 ] 1373  >(injective_S … Hi) >lookup_insert_hit normalize nodelta in Hlength; >Hlength 1374 normalize nodelta @pair_elim #l1 #l2 #Hl @pair_elim #y1 #y2 #Hy >Hl @refl 1375 ] 1376 ] 1377 2,4: (* policy_isize_sum XXX *) cases daemon 1378 ] 1379  (* Case where add_instr = None *) normalize nodelta lapply (pi2 ?? acc) >p >p1 1380 normalize nodelta #Hpolicy 1381 @conj [ @conj [ @conj [ @conj [ @conj [ @conj 1382 [ (* out_of_program_none *) #i >append_length >commutative_plus #Hi normalize in Hi; 1383 #Hi2 @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) i (le_S_to_le ?? Hi) Hi2) 1384  (* labels_okay *) @lookup_forall #x cases x x #x cases x #p #a #j #lbl #Hl normalize nodelta 1385 elim (forall_lookup … (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))) ? lbl Hl) 1386 #id #Hid @(ex_intro … id Hid) 1387 ] 1388  (* jump_in_policy *) #i >append_length >commutative_plus #Hi normalize in Hi; 1389 elim (le_to_or_lt_eq … Hi) Hi #Hi 1390 [ >(nth_append_first ?? prefix ?? (le_S_S_to_le ?? Hi)) 1391 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) i (le_S_S_to_le ?? Hi)) 1392  >(injective_S … Hi) @conj 1393 [ >(nth_append_second ?? prefix ?? (le_n (prefix))) <minus_n_n whd in match (nth ????); 1394 normalize nodelta in p2; cases instr in p2; 1395 [ #pi cases pi 1396 [1,2,3,6,7,33,34: #x #y #_ #H @⊥ @H 1397 4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #_ #H @⊥ @H 1398 9,10,14,15: #id (* normalize segfaults here *) normalize nodelta 1399 whd in match (jump_expansion_step_instruction ???); 1400 #H lapply (jmeq_to_eq ??? H) #H2 destruct (H2) 1401 11,12,13,16,17: #x #id normalize nodelta 1402 whd in match (jump_expansion_step_instruction ???); 1403 #H lapply (jmeq_to_eq ??? H) #H2 destruct (H2) 1404 35,36,37: #_ #H @⊥ @H 1405 ] 1406 2,3: #x #_ #H @⊥ @H 1407 4,5: #id normalize nodelta #H lapply (jmeq_to_eq ??? H) #H2 destruct (H2) 1408 6: #x #id #_ #H @⊥ @H 1409 ] 1410  #H elim H H #p #H elim H H #a #H elim H H #j #H 1411 >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) (prefix) (le_n (prefix)) ?) in H; 1412 [ #H destruct (H) 1413  @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm 1414 @le_S_S @le_plus_n_r 1415 ] 1416 ] 1417 ] 1418 ] 1419  (* policy_increase *) #i >append_length >commutative_plus #Hi normalize in Hi; 1420 elim (le_to_or_lt_eq … Hi) Hi #Hi 1421 [ @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))) i (le_S_S_to_le … Hi)) 1422  >(injective_S … Hi) >lookup_opt_lookup_miss 1423 [ >lookup_opt_lookup_miss 1424 [ normalize nodelta %2 @refl 1425  @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) (prefix) (le_n (prefix)) ?) 1426 @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm 1427 @le_S_S @le_plus_n_r 1428 ] 1429  @(proj1 ?? (jump_not_in_policy (pi1 … program) «pi1 ?? old_policy,proj1 ?? (proj1 ?? (pi2 ?? old_policy))» (prefix) ?)) >prf 1430 [ >append_length normalize <plus_n_Sm @le_S_S @le_plus_n_r 1431  >(nth_append_second ?? prefix ?? (le_n (prefix))) <minus_n_n >p1 1432 whd in match (nth ????); normalize nodelta in p2; cases instr in p2; 1433 [ #pi cases pi 1434 [1,2,3,6,7,33,34: #x #y #_ normalize /2 by nmk/ 1435 4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #_ normalize /2 by nmk/ 1436 9,10,14,15: #id (* normalize segfaults here *) normalize nodelta 1437 whd in match (jump_expansion_step_instruction ???); 1438 #H lapply (jmeq_to_eq ??? H) #H2 destruct (H2) 1439 11,12,13,16,17: #x #id normalize nodelta 1440 whd in match (jump_expansion_step_instruction ???); 1441 #H lapply (jmeq_to_eq ??? H) #H2 destruct (H2) 1442 35,36,37: #_ normalize /2 by nmk/ 1443 ] 1444 2,3: #x #_ normalize /2 by nmk/ 1445 4,5: #id normalize nodelta #H lapply (jmeq_to_eq ??? H) #H2 destruct (H2) 1446 6: #x #id #_ normalize /2 by nmk/ 1447 ] 1448 ] 1449 ] 1450 ] 1451 ] 1452  (* policy_safe *) @lookup_forall #x cases x x #x cases x x #p #a #j #n #Hl 1453 @(forall_lookup … (proj2 ?? (proj1 ?? (proj1 ?? Hpolicy))) ? n Hl) 1454 ] 1455  (* changed *) #Hc #i >append_length >commutative_plus #Hi normalize in Hi; 1456 elim (le_to_or_lt_eq … Hi) Hi #Hi 1457 [ @(proj2 ?? (proj1 ?? Hpolicy) Hc i (le_S_S_to_le … Hi)) 1458  >(injective_S … Hi) >lookup_opt_lookup_miss 1459 [ >lookup_opt_lookup_miss 1460 [ normalize nodelta @refl 1461  @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) (prefix) (le_n (prefix)) ?) 1462 @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm 1463 @le_S_S @le_plus_n_r 1464 ] 1465  @(proj1 ?? (jump_not_in_policy (pi1 … program) «pi1 ?? old_policy,proj1 ?? (proj1 ?? (pi2 ?? old_policy))» (prefix) ?)) >prf 1466 [ >append_length normalize <plus_n_Sm @le_S_S @le_plus_n_r 1467  >(nth_append_second ?? prefix ?? (le_n (prefix))) <minus_n_n >p1 1468 whd in match (nth ????); normalize nodelta in p2; cases instr in p2; 1469 [ #pi cases pi 1470 [1,2,3,6,7,33,34: #x #y #_ normalize /2 by nmk/ 1471 4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #_ normalize /2 by nmk/ 1472 9,10,14,15: #id (* normalize segfaults here *) normalize nodelta 1473 whd in match (jump_expansion_step_instruction ???); 1474 #H lapply (jmeq_to_eq ??? H) #H2 destruct (H2) 1475 11,12,13,16,17: #x #id normalize nodelta 1476 whd in match (jump_expansion_step_instruction ???); 1477 #H lapply (jmeq_to_eq ??? H) #H2 destruct (H2) 1478 35,36,37: #_ normalize /2 by nmk/ 1479 ] 1480 2,3: #x #_ normalize /2 by nmk/ 1481 4,5: #id normalize nodelta #H lapply (jmeq_to_eq ??? H) #H2 destruct (H2) 1482 6: #x #id #_ normalize /2 by nmk/ 1483 ] 1484 ] 1485 ] 1486 ] 1487 ] 1488  (* XXX policy_isize_sum *) cases daemon 1489 ] 1490  @conj [ @conj [ @conj [ @conj [ @conj [ @conj 1491 [ #i #Hi / by refl/ 1492  / by I/ 1493 ] 1494  #i #Hi @conj [ >nth_nil #H @⊥ @H  #H elim H #x #H1 elim H1 #y #H2 elim H2 #z #H3 1495 normalize in H3; destruct (H3) ] 1496 ] 1497  #i #Hi @⊥ @(absurd (i<0)) [ @Hi  @(not_le_Sn_O) ] 1498 ] 1499  / by I/ 1500 ] 1501  #_ #i #Hi @⊥ @(absurd (i < 0)) [ @Hi  @not_le_Sn_O ] 1502 ] 1503  / by refl/ 1504 ] 1505 ] 1506 qed.*) 1507 1508 (* this might be replaced by a coercion: (∀x.A x → B x) → Σx.A x → Σx.B x *) 1509 (* definition weaken_policy: 1510 ∀program,op. 1511 option (Σp:jump_expansion_policy. 1512 And (And (And (And (out_of_program_none program p) 1513 (labels_okay (create_label_map program op) p)) 1514 (jump_in_policy program p)) (policy_increase program op p)) 1515 (policy_safe p)) → 1516 option (Σp:jump_expansion_policy.And (out_of_program_none program p) 1517 (jump_in_policy program p)) ≝ 1518 λprogram.λop.λx. 1519 match x return λ_.option (Σp.And (out_of_program_none program p) (jump_in_policy program p)) with 1520 [ None ⇒ None ? 1521  Some z ⇒ Some ? (mk_Sig ?? (pi1 ?? z) ?) 1522 ]. 1523 @conj 1524 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? z))))) 1525  @(proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? z)))) 1526 ] 1527 qed. *) 1528 1529 (* This function executes n steps from the starting point. *) 1530 (*let rec jump_expansion_internal (program: Σl:list labelled_instruction.lt (l) 2^16) 1531 (n: ℕ) on n:(Σx:bool × ℕ × (option jump_expansion_policy). 1532 let 〈ch,pc,y〉 ≝ x in 1533 match y with 1534 [ None ⇒ pc > 2^16 1535  Some p ⇒ And (out_of_program_none program p) (jump_in_policy program p) 1536 ]) ≝ 1537 match n with 1538 [ O ⇒ 〈0,Some ? (pi1 … (jump_expansion_start program))〉 1539  S m ⇒ let 〈ch,pc,z〉 as p1 ≝ (pi1 ?? (jump_expansion_internal program m)) in 1540 match z return λx. z=x → Σa:bool × ℕ × (option jump_expansion_policy).? with 1541 [ None ⇒ λp2.〈pc,None ?〉 1542  Some op ⇒ λp2.pi1 … (jump_expansion_step program (create_label_map program op) «op,?») 1543 ] (refl … z) 1544 ].*) 1545 1546 1201 1547 1202 let rec jump_expansion_internal (program: Σl:list labelled_instruction.lt (length ? l) 2^16) (n: ℕ) 1548 1203 on n:(Σx:bool × (option ppc_pc_map). … … 1551 1206 [ None ⇒ True 1552 1207  Some x ⇒ 1553 And (And 1208 And (And (And 1554 1209 (out_of_program_none program x) 1555 (policy_isize_sum program (create_label_map program) x)) 1210 (jump_not_in_policy program x)) 1211 (policy_compact program (create_label_map program) x)) 1556 1212 (\fst x < 2^16) 1557 1213 ]) ≝ … … 1570 1226 #p cases p 1571 1227 [ / by I/ 1572  #pm / by I/1228  #pm normalize nodelta #H @conj [ @(proj1 ?? (proj1 ?? H))  @(proj2 ?? H) ] 1573 1229 ] 1574 1230  lapply (pi2 ?? (jump_expansion_internal program m)) <p1 >p2 normalize nodelta / by / 1575  lapply (pi2 ?? (jump_expansion_internal program m)) <p1 >p2 normalize nodelta / by / 1231  lapply (pi2 ?? (jump_expansion_internal program m)) <p1 >p2 normalize nodelta 1232 #H @conj [ @(proj1 ?? (proj1 ?? H))  @(proj2 ?? H) ] 1576 1233  normalize nodelta cases (jump_expansion_step program labels «op,?») 1577 1234 #p cases p p #p #r cases r normalize nodelta … … 1579 1236  #j #H @conj 1580 1237 [ @conj 1581 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))))1582  @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))))1238 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) 1239  @(proj2 ?? (proj1 ?? (proj1 ?? H))) 1583 1240 ] 1584 1241  @(proj2 ?? H) … … 1748 1405 ∀policy:Σp:ppc_pc_map. 1749 1406 out_of_program_none program p ∧ 1750 policy_isize_sum program (create_label_map program)p ∧ \fst p < 2^16.1407 jump_not_in_policy program p ∧ \fst p < 2^16. 1751 1408 ∀l.l ≤ program → ∀acc:ℕ. 1752 1409 match \snd (jump_expansion_step program (create_label_map program) policy) with … … 1764 1421 cases (bvt_lookup ?? (bitvector_of_nat ? (t)) (\snd policy) 〈0,short_jump〉) 1765 1422 #x1 #x2 cases (bvt_lookup ?? (bitvector_of_nat ? (t)) (\snd x) 〈0,short_jump〉) 1766 #y1 #y2 normalize nodelta #Hblerp cases (proj2 ?? Hblerp)cases x2 cases y21423 #y1 #y2 normalize nodelta #Hblerp cases Hblerp cases x2 cases y2 1767 1424 [1,4,5,7,8,9: #H cases H 1768 1425 2,3,6: #_ normalize nodelta … … 1796 1453 lemma measure_full: ∀program.∀policy. 1797 1454 measure_int program policy 0 = 2*program → ∀i.i<program → 1798 is_jump ( nth i ? program 〈None ?,Comment []〉) →1455 is_jump (\snd (nth i ? program 〈None ?,Comment []〉)) → 1799 1456 (\snd (bvt_lookup ?? (bitvector_of_nat ? i) (\snd policy) 〈0,short_jump〉)) = long_jump. 1800 1457 #program #policy elim program in ⊢ (% → ∀i.% → ? → %); … … 1829 1486 lemma measure_special: ∀program:(Σl:list labelled_instruction.l < 2^16). 1830 1487 ∀policy:Σp:ppc_pc_map. 1831 out_of_program_none program p ∧ policy_isize_sum program (create_label_map program)p ∧ \fst p < 2^16.1488 out_of_program_none program p ∧ jump_not_in_policy program p ∧ \fst p < 2^16. 1832 1489 match (\snd (pi1 ?? (jump_expansion_step program (create_label_map program) policy))) with 1833 1490 [ None ⇒ True … … 1855 1512 lapply (measure_incr_or_equal program policy t ? 0) 1856 1513 [1,3: @(transitive_le … Hp) @le_n_Sn ] >eqpol / by / 1857 4,7,8: #H elim (proj2 ?? H)#H2 [1,3,5: cases H2 2,4,6: destruct (H2) ]1514 4,7,8: #H elim H #H2 [1,3,5: cases H2 2,4,6: destruct (H2) ] 1858 1515 5: >measure_plus >measure_plus >commutative_plus >(commutative_plus ? 1) 1859 1516 #_ #H @(injective_plus_r … H) … … 1871 1528 whd in match (measure_int ? p ?) in Hm; 1872 1529 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol))) (t) Hp) 1873 cases (bvt_lookup ?? (bitvector_of_nat ? (t)) ? 〈0,short_jump〉) in 1874 Hm; 1530 cases (bvt_lookup ?? (bitvector_of_nat ? (t)) ? 〈0,short_jump〉) in Hm; 1875 1531 #x1 #x2 1876 1532 cases (bvt_lookup ?? (bitvector_of_nat ? (t)) ? 〈0,short_jump〉); 1877 1533 #y1 #y2 1878 1534 normalize nodelta cases x2 cases y2 normalize nodelta 1879 cases daemon 1880 (* [1,5,9: #_ #_ // 1881 4,7,8: #_ #H elim H #H2 [1,3,5: @⊥ @H2 2,4,6: destruct (H2) ] 1535 [1,5,9: #_ #_ @refl 1536 4,7,8: #_ #H elim H #H2 [1,3,5: cases H2 2,4,6: destruct (H2) ] 1882 1537 2,3: >measure_plus #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt 1883 1538 lapply (measure_incr_or_equal program policy t ? 0) … … 1888 1543 lapply (measure_incr_or_equal program policy t ? 0) 1889 1544 [ @(transitive_le … Hp) @le_n_Sn ] >eqpol / by / 1890 ] *)1545 ] 1891 1546 ] 1892 1547 ] … … 1908 1563 qed. 1909 1564 1910 (* probably needs some kind of not_jump → short *)1911 1565 lemma measure_zero: ∀l.∀program:Σl:list labelled_instruction.l < 2^16. 1912 1566 match jump_expansion_start program (create_label_map program) with … … 1920 1574  #pl normalize nodelta #Hpl #EQ elim l 1921 1575 [ / by refl/ 1922  #h #t #Hind #Hp 1923 cases daemon (* 1924 cases (dec_is_jump (nth (t) ? program 〈None ?, Comment []〉)) #Hj 1925 [ normalize nodelta @Hind @le_S_to_le ] 1926 @Hp 1927  >(lookup_opt_lookup_miss … (proj1 ?? (jump_not_in_policy program (pi1 ?? (jump_expansion_start program)) (t) ?) Hj) 〈0,0,short_jump〉) 1928 [ normalize nodelta @Hind @le_S_to_le @Hp 1929  @Hp 1930  % 1931 [ @(proj1 ?? (proj1 ?? (pi2 ?? (jump_expansion_start program)))) 1932  @(proj2 ?? (proj1 ?? (pi2 ?? (jump_expansion_start program)))) 1933 ] 1934 ] 1935 ]*) 1936 ] 1576  #h #t #Hind #Hp whd in match (measure_int ???); 1577 >(proj2 ?? (proj1 ?? Hpl) (t)) 1578 [ normalize nodelta @Hind ] 1579 @(transitive_le … Hp) [ @le_n_Sn  @ le_n ] 1580 ] 1581 ] 1937 1582 qed. 1938 1583 … … 1942 1587 And (match p with 1943 1588 [ None ⇒ True 1944  Some pol ⇒ And (And ( 1945 (out_of_program_none program pol)) 1946 (policy_isize_sum program (create_label_map program) pol)) 1589  Some pol ⇒ And (out_of_program_none program pol) 1947 1590 (policy_compact program (create_label_map program) pol) 1948 1591 ]) 1949 1592 (∃n.∀k.n < k → 1950 1593 policy_equal_opt program (\snd (pi1 ?? (jump_expansion_internal program k))) p). 1951 #program @(\snd (pi1 ?? (jump_expansion_internal program (2*program)))) 1952 cases daemon 1953 1954 (* old proof 1955 cases (dec_bounded_exists (λk.policy_equal (pi1 ?? program) 1594 #program @(\snd (pi1 ?? (jump_expansion_internal program (2*program)))) @conj 1595 [ lapply (pi2 ?? (jump_expansion_internal program (2*program))) 1596 cases (jump_expansion_internal program (2*program)) #p cases p p 1597 #c #pol #Hp cases pol 1598 [ normalize nodelta // 1599  #x normalize nodelta #H @conj [ @(proj1 ?? (proj1 ?? (proj1 ?? H))) 1600  cases daemon ] ] 1601  cases (dec_bounded_exists (λk.policy_equal_opt (pi1 ?? program) 1956 1602 (\snd (pi1 ?? (jump_expansion_internal program k))) 1957 1603 (\snd (pi1 ?? (jump_expansion_internal program (S k))))) ? (2*program)) 1958 cases daemon1959 1604 [ #Hex elim Hex Hex #x #Hx @(ex_intro … x) #k #Hk 1960 1605 @pe_trans … … 1969 1614 ] 1970 1615 ] 1971  #Hnex lapply (not_exists_forall … Hnex) Hnex; #Hfa @(ex_intro … (2*program)) #k #Hk1972 @ pe_sym @equal_remains_equal1616  #Hnex lapply (not_exists_forall … Hnex) Hnex; #Hfa 1617 @(ex_intro … (2*program)) #k #Hk @pe_sym @equal_remains_equal 1973 1618 [ lapply (refl ? (jump_expansion_internal program (2*program))) 1974 1619 cases (jump_expansion_internal program (2*program)) in ⊢ (???% → %); … … 1979 1624  #Fp #HFp #EQ whd in match (jump_expansion_internal ??); 1980 1625 >EQ normalize nodelta 1981 lapply (refl ? (jump_expansion_step program (create_label_map program Fp) «Fp,?»))1982 [ @ HFp1626 lapply (refl ? (jump_expansion_step program (create_label_map program) «Fp,?»)) 1627 [ @conj [ @(proj1 ?? (proj1 ?? HFp))  @(proj2 ?? HFp) ] 1983 1628  lapply (measure_full program Fp ?) 1984 1629 [ @le_to_le_to_eq … … 1988 1633 x ≤ measure_int program p 0)) 1989 1634 [ #x elim x 1990 [ #Hx @(ex_intro ?? (jump_expansion_start program)) @conj 1991 [ whd in match (jump_expansion_internal ??); @refl 1992  @le_O_n 1635 [ #Hx lapply (refl ? (jump_expansion_start program (create_label_map program))) 1636 cases (jump_expansion_start program (create_label_map program)) in ⊢ (???% → %); 1637 #z cases z z normalize nodelta 1638 [ #Waar #Heqn @⊥ elim (le_to_eq_plus ?? Hx) #k #Hk 1639 @(absurd … (step_none program 0 ? k)) 1640 [ whd in match (jump_expansion_internal ??); >Heqn @refl 1641  <Hk >EQ @nmk #H destruct (H) 1642 ] 1643  #pol #Hpol #Heqpol @(ex_intro ?? pol) @conj 1644 [ whd in match (jump_expansion_internal ??); >Heqpol @refl 1645  @le_O_n 1646 ] 1993 1647 ] 1994 1648  x #x #Hind #Hx … … 2008 1662 [ cases (jump_expansion_internal program x) in Hxpol; 2009 1663 #z cases z z #xch #xpol normalize nodelta #H #H2 >(proj1 ?? H2) in H; 2010 normalize nodelta / by /1664 normalize nodelta #H @conj [ @(proj1 ?? (proj1 ?? H))  @(proj2 ?? H) ] 2011 1665  lapply (Hfa x Hx) lapply HeqSxpol HeqSxpol 2012 1666 whd in match (jump_expansion_internal program (S x)); … … 2015 1669 #z cases z z #xch #b normalize nodelta #H #Heq >(proj1 ?? Heq) in H; 2016 1670 #H #Heq cases xch in Heq; #Heq normalize nodelta 2017 [ lapply (refl ? (jump_expansion_step program (create_label_map (pi1 ?? program) xpol) «xpol,H»)) 2018 cases (jump_expansion_step ???) in ⊢ (???% → %); #z cases z z #a #c 2019 normalize nodelta cases c normalize nodelta 2020 [ #H1 #Heq #H2 destruct (H2) 2021  #d #H1 #Heq #H2 destruct (H2) #Hfull #H2 elim (le_to_or_lt_eq … H2) 2022 [ / by / 2023  #H3 lapply (measure_special program «xpol,H») >Heq 2024 normalize nodelta #H4 @⊥ 2025 @(absurd … (H4 H3)) 2026 @Hfull 1671 [ lapply (refl ? (jump_expansion_step program (create_label_map (pi1 ?? program)) «xpol,?»)) 1672 [ @conj [ @(proj1 ?? (proj1 ?? H))  @(proj2 ?? H) ] 1673  cases (jump_expansion_step ???) in ⊢ (???% → %); #z cases z z #a #c 1674 normalize nodelta cases c normalize nodelta 1675 [ #H1 #Heq #H2 destruct (H2) 1676  #d #H1 #Heq #H2 destruct (H2) #Hfull #H2 elim (le_to_or_lt_eq … H2) 1677 [ / by / 1678  #H3 lapply (measure_special program «xpol,?») 1679 [ @conj [ @(proj1 ?? (proj1 ?? H))  @(proj2 ?? H) ] 1680  >Heq normalize nodelta #H4 @⊥ @(absurd … (H4 H3)) @Hfull 1681 ] 1682 ] 2027 1683 ] 2028 1684 ] 2029  lapply (refl ? (jump_expansion_step program (create_label_map (pi1 ?? program) xpol) «xpol,H»)) 2030 cases (jump_expansion_step ???) in ⊢ (???% → %); #z cases z z #a #c 2031 normalize nodelta cases c normalize nodelta 2032 [ #H1 #Heq #H2 #H3 #_ @⊥ @(absurd ?? H3) @pe_refl 2033  #d #H1 #Heq #H2 #H3 @⊥ @(absurd ?? H3) @pe_refl 1685  lapply (refl ? (jump_expansion_step program (create_label_map (pi1 ?? program)) «xpol,?»)) 1686 [ @conj [ @(proj1 ?? (proj1 ?? H))  @(proj2 ?? H) ] 1687  cases (jump_expansion_step ???) in ⊢ (???% → %); #z cases z z #a #c 1688 normalize nodelta cases c normalize nodelta 1689 [ #H1 #Heq #H2 #H3 #_ @⊥ @(absurd ?? H3) @pe_refl 1690  #d #H1 #Heq #H2 #H3 @⊥ @(absurd ?? H3) @pe_refl 1691 ] 2034 1692 ] 2035 1693 ] … … 2042 1700 ] 2043 1701 ] 2044  #Hfull cases (jump_expansion_step program (create_label_map program Fp) «Fp,?») in ⊢ (???% → %);1702  #Hfull cases (jump_expansion_step program (create_label_map program) «Fp,?») in ⊢ (???% → %); 2045 1703 #x cases x x #Gch #Gpol cases Gpol normalize nodelta 2046 [ #H #EQ2 @⊥ @(absurd ?? H) @Hfull 1704 [ cases daemon (* XXX will need some form of nec_plus_ultra here 1705 #H #EQ2 @⊥ @(absurd ?? H) @Hfull *) 2047 1706  #Gp #HGp #EQ2 cases Fch 2048 1707 [ normalize nodelta #i #Hi 2049 lapply (refl ? (lookup ?? (bitvector_of_nat 16 i) (\snd Fp) 〈0,0,short_jump〉)) 2050 cases (lookup ?? (bitvector_of_nat 16 i) (\snd Fp) 〈0,0,short_jump〉) in ⊢ (???% → %); 2051 #x cases x x #p #a #j normalize nodelta #H 2052 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp)))) i Hi) lapply (Hfull i Hi) >H 2053 #H2 >H2 normalize nodelta cases (lookup ?? (bitvector_of_nat 16 i) (\snd Gp) 〈0,0,short_jump〉) 2054 #x cases x x #p #a #j' cases j' normalize nodelta #H elim H H #H 2055 [1,3: @⊥ @H 2056 2,4: destruct (H) 2057 5,6: @refl 1708 cases (dec_is_jump (\snd (nth i ? program 〈None ?, Comment []〉))) #Hj 1709 [ lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp))) i Hi) 1710 lapply (Hfull i Hi Hj) cases (bvt_lookup … (bitvector_of_nat ? i) (\snd Fp) 〈0,short_jump〉) 1711 #fp #fj #Hfj >Hfj normalize nodelta 1712 cases (bvt_lookup … (bitvector_of_nat ? i) (\snd Gp) 〈0,short_jump〉) #gp #gj 1713 cases gj normalize nodelta 1714 [1,2: #H cases H #H2 cases H2 destruct (H2) 1715 3: #_ @refl 1716 ] 1717  >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp)))) i Hi Hj) 1718 >(proj2 ?? (proj1 ?? (proj1 ?? HFp)) i Hi Hj) @refl 2058 1719 ] 2059 1720  normalize nodelta /2 by pe_int_refl/ … … 2073 1734 #H destruct (H) 2074 1735 4: #np #Hnp #Sp #HSp whd in match (policy_equal ???); @dec_bounded_forall #m 2075 cases (bvt_lookup ?? (bitvector_of_nat 16 m) ? 〈0, 0,short_jump〉)2076 #x cases x x #x1 #x2 #x32077 cases (bvt_lookup ?? (bitvector_of_nat ? m) ? 〈0, 0,short_jump〉)2078 #y cases y y #y1 #y2 #y3normalize nodelta1736 cases (bvt_lookup ?? (bitvector_of_nat 16 m) ? 〈0,short_jump〉) 1737 #x1 #x2 1738 cases (bvt_lookup ?? (bitvector_of_nat ? m) ? 〈0,short_jump〉) 1739 #y1 #y2 normalize nodelta 2079 1740 @dec_eq_jump_length 2080 1741 ] 2081 ] *)2082 qed. 2083 2084 nclude alias "arithmetics/nat.ma".1742 ] 1743 qed. 1744 1745 include alias "arithmetics/nat.ma". 2085 1746 include alias "basics/logic.ma". 2086 2087 check create_label_cost_map2088 1747 2089 1748 (* The glue between Policy and Assembly. *) … … 2096 1755 let lookup_labels ≝ λx. bitvector_of_nat ? (lookup_def ?? labels x 0) in 2097 1756 let instruction ≝ \fst (fetch_pseudo_instruction (\snd program) ppc) in 2098 let next_pc ≝ \fst (sigma (add …ppc (bitvector_of_nat ? 1))) in2099 (nat_of_bitvector … ppc ≤ \snd program →2100 next_pc = add … pc (bitvector_of_nat … (instruction_size lookup_labels sigma ppc instruction)))2101 ∧2102 ( (nat_of_bitvector … ppc < \snd program →1757 let next_pc ≝ \fst (sigma (add ? ppc (bitvector_of_nat ? 1))) in 1758 And (nat_of_bitvector … ppc ≤ \snd program → 1759 next_pc = add ? pc (bitvector_of_nat … 1760 (instruction_size lookup_labels (λx.\fst (sigma x)) (λx.\snd (sigma x)) ppc instruction))) 1761 (Or (nat_of_bitvector … ppc < \snd program → 2103 1762 nat_of_bitvector … pc < nat_of_bitvector … next_pc) 2104 ∨ 2105 (nat_of_bitvector … ppc = \snd program → next_pc = (zero …)))). 2106 ≝ λprogram. 1763 (nat_of_bitvector … ppc = \snd program → next_pc = (zero …)))) ≝ 1764 λprogram. 2107 1765 let policy ≝ pi1 … (je_fixpoint (\snd program)) in 2108 1766 match policy with … … 2112 1770 〈bitvector_of_nat 16 pc,jmpeqb jl long_jump〉,?» 2113 1771 ]. 2114 cases daemon2115 qed. 1772 #ppc normalize nodelta cases daemon 1773 qed.
Note: See TracChangeset
for help on using the changeset viewer.