Changeset 2008
 Timestamp:
 May 30, 2012, 7:22:05 PM (5 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Policy.ma
r1973 r2008 19 19 definition out_of_program_none: list labelled_instruction → ppc_pc_map → Prop ≝ 20 20 λprefix.λsigma. 21 ∀i:ℕ.i ≥prefix → i < 2^16 → bvt_lookup_opt … (bitvector_of_nat 16 i) (\snd sigma) = None ?.21 ∀i:ℕ.i > prefix → i < 2^16 → bvt_lookup_opt … (bitvector_of_nat 16 i) (\snd sigma) = None ?. 22 22 23 23 (* If instruction i is a jump, then there will be something in the policy at … … 70 70 ∀i:ℕ.i < prefix → 71 71 ¬is_jump (\snd (nth i ? prefix 〈None ?, Comment []〉)) → 72 \snd (bvt_lookup … (bitvector_of_nat 16 i) (\snd sigma) 〈0,short_jump〉) = short_jump.72 \snd (bvt_lookup … (bitvector_of_nat 16 (S i)) (\snd sigma) 〈0,short_jump〉) = short_jump. 73 73 74 74 (* if the instruction 〈p,a〉 is a jump to label l, then label l is at address a *) … … 118 118 λprogram.λop.λp. 119 119 ∀i.i < program → 120 let 〈opc,oj〉 ≝ bvt_lookup … (bitvector_of_nat 16 i) (\snd op) 〈0,short_jump〉 in121 let 〈pc,j〉 ≝ bvt_lookup … (bitvector_of_nat 16 i) (\snd p) 〈0,short_jump〉 in120 let 〈opc,oj〉 ≝ bvt_lookup … (bitvector_of_nat 16 (S i)) (\snd op) 〈0,short_jump〉 in 121 let 〈pc,j〉 ≝ bvt_lookup … (bitvector_of_nat 16 (S i)) (\snd p) 〈0,short_jump〉 in 122 122 (*opc ≤ pc ∧*) jmpleq oj j. 123 123 … … 245 245 qed. 246 246 247 (* new safety condition: policy corresponds to program and resulting program is compact *) 248 definition policy_compact: list labelled_instruction → label_map → ppc_pc_map → Prop ≝ 247 definition policy_compact_unsafe: list labelled_instruction → label_map → ppc_pc_map → Prop ≝ 249 248 λprogram.λlabels.λsigma. 250 ∀n:ℕ. S n < program →249 ∀n:ℕ.n < program → 251 250 match bvt_lookup_opt … (bitvector_of_nat ? n) (\snd sigma) with 252 251 [ None ⇒ False … … 255 254 [ None ⇒ False 256 255  Some x1 ⇒ let 〈pc1,j1〉 ≝ x1 in 257 pc1 = instruction_size (λid.bitvector_of_nat ? (lookup_def ?? labels id 0)) 256 pc1 = pc + instruction_size_jmplen j (\snd (nth n ? program 〈None ?, Comment []〉)) 257 ] 258 ]. 259 260 (* new safety condition: policy corresponds to program and resulting program is compact *) 261 definition policy_compact: list labelled_instruction → label_map → ppc_pc_map → Prop ≝ 262 λprogram.λlabels.λsigma. 263 ∀n:ℕ.n < program → 264 match bvt_lookup_opt … (bitvector_of_nat ? n) (\snd sigma) with 265 [ None ⇒ False 266  Some x ⇒ let 〈pc,j〉 ≝ x in 267 match bvt_lookup_opt … (bitvector_of_nat ? (S n)) (\snd sigma) with 268 [ None ⇒ False 269  Some x1 ⇒ let 〈pc1,j1〉 ≝ x1 in 270 pc1 = pc + instruction_size (λid.bitvector_of_nat ? (lookup_def ?? labels id 0)) 258 271 (λppc.bitvector_of_nat ? (\fst (bvt_lookup ?? ppc (\snd sigma) 〈0,short_jump〉))) 259 272 (λppc.jmpeqb long_jump (\snd (bvt_lookup ?? ppc (\snd sigma) 〈0,short_jump〉))) 260 (bitvector_of_nat ? pc) (\snd (nth n ? program 〈None ?, Comment []〉))273 (bitvector_of_nat ? n) (\snd (nth n ? program 〈None ?, Comment []〉)) 261 274 ] 262 275 ]. … … 406 419 qed. 407 420 421 lemma nth_last: ∀A,a,l. 422 nth (l) A l a = a. 423 #A #a #l elim l 424 [ / by / 425  #h #t #Hind whd in match (nth ????); whd in match (tail ??); @Hind 426 ] 427 qed. 428 408 429 (* The first step of the jump expansion: everything to short. *) 409 430 definition jump_expansion_start: 410 ∀program:(Σl:list labelled_instruction. l< 2^16).431 ∀program:(Σl:list labelled_instruction.S (l) < 2^16). 411 432 ∀labels:label_map. 412 433 Σpolicy:option ppc_pc_map. … … 414 435 [ None ⇒ True 415 436  Some p ⇒ 416 And (And (And (And ( out_of_program_none (pi1 ?? program) p)437 And (And (And (And (And (And (out_of_program_none (pi1 ?? program) p) 417 438 (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)) 439 (policy_compact_unsafe program labels p)) 440 (bvt_lookup_opt … (bitvector_of_nat ? 0) (\snd p) = Some ? 〈0,short_jump〉)) 441 (∀i.i ≤ program → ∃pc. 442 bvt_lookup_opt … (bitvector_of_nat ? i) (\snd p) = Some ? 〈pc,short_jump〉)) 443 (bvt_lookup_opt … (bitvector_of_nat ? (program)) (\snd p) = 444 Some ? 〈\fst p,short_jump〉)) 421 445 (\fst p < 2^16) 422 446 ] ≝ … … 424 448 let final_policy ≝ foldl_strong (option Identifier × pseudo_instruction) 425 449 (λprefix.Σpolicy:ppc_pc_map. 426 And (And (And ( out_of_program_none prefix policy)450 And (And (And (And (And (out_of_program_none prefix policy) 427 451 (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)) 452 (policy_compact_unsafe prefix labels policy)) 453 (bvt_lookup_opt … (bitvector_of_nat ? 0) (\snd policy) = Some ? 〈0,short_jump〉)) 454 (∀i.i ≤ prefix → ∃pc. 455 bvt_lookup_opt … (bitvector_of_nat ? i) (\snd policy) = Some ? 〈pc,short_jump〉)) 456 (bvt_lookup_opt … (bitvector_of_nat ? (prefix)) (\snd policy) = 457 Some ? 〈\fst policy,short_jump〉)) 431 458 program 432 459 (λprefix.λx.λtl.λprf.λp. 433 let 〈pc,sigma〉 ≝ p in460 let 〈pc,sigma〉 ≝ pi1 ?? p in 434 461 let 〈label,instr〉 ≝ x in 435 462 let isize ≝ instruction_size_jmplen short_jump instr in 436 〈pc + isize, bvt_insert … (bitvector_of_nat 16 ( prefix)) 〈pc,short_jump〉 sigma〉437 ) 〈0, Stub ? ?〉 in438 if geb (\fst final_policy) 2^16 then463 〈pc + isize, bvt_insert … (bitvector_of_nat 16 (S (prefix))) 〈pc+isize,short_jump〉 sigma〉 464 ) 〈0, bvt_insert ?? (bitvector_of_nat 16 0) 〈0,short_jump〉 (Stub ??)〉 in 465 if geb (\fst (pi1 ?? final_policy)) 2^16 then 439 466 None ? 440 467 else … … 443 470  lapply p p generalize in match (foldl_strong ?????); * #p #Hp #hg 444 471 @conj [ @Hp  @not_le_to_lt @leb_false_to_not_le <geb_to_leb @hg ] 445  @conj [ @conj [ @conj 472  @conj [ @conj [ @conj [ @conj [ @conj 446 473 [ (* out_of_program_none *) 447 474 #i >append_length <commutative_plus #Hi normalize in Hi; #Hi2 … … 449 476 cases p p #p cases p p #pc #p #Hp cases x x #l #pi 450 477 [ >lookup_opt_insert_miss 451 [ @(proj1 ?? (proj1 ?? (proj1 ?? Hp)) i ? Hi2) @le_S_to_le @le_S_to_le @Hi 478 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))) i ? Hi2) 479 @le_S_to_le @le_S_to_le @Hi 452 480  @bitvector_of_nat_abs 453 481 [ @Hi2 … … 457 485 ] 458 486  >lookup_opt_insert_miss 459 [ <Hi @(proj1 ?? (proj1 ?? (proj1 ?? Hp)) (S (prefix)) (le_S ?? (le_n (prefix))) ?) 460 >Hi @Hi2 487 [ <Hi @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))) (S (S (prefix))) ?) 488 [ @le_S @le_n 489  >Hi @Hi2 490 ] 461 491  @bitvector_of_nat_abs 462 492 [ @Hi2 … … 466 496 ] 467 497 ] 468  (* jump_not_in_policy *) #i >append_length <commutative_plus 469 #Hi normalize in Hi; cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi 470 [ cases p p #p cases p p #pc #sigma #Hp cases x #l #ins >lookup_insert_miss 471 [ >(nth_append_first ? i prefix ?? Hi) @((proj2 ?? (proj1 ?? (proj1 ?? Hp))) i Hi) 498  (* jump_not_in_policy *) cases p p #p cases p p #pc #sigma #Hp 499 cases x in prf; #lbl #ins #prf #i >append_length <commutative_plus #Hi 500 normalize in Hi; normalize nodelta cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi 501 [ >lookup_insert_miss 502 [ lapply ((proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp))))) i ?) 503 [ @Hi 504  >nth_append_first 505 [ #H #H2 @H @H2 506  @Hi 507 ] 508 ] 472 509  @bitvector_of_nat_abs 473 [ @(transitive_lt … (pi2 ?? program)) >prf >append_length >commutative_plus510 [ @(transitive_lt … (pi2 ?? program)) @le_S_S >prf >append_length <commutative_plus @le_S 474 511 @le_plus_a @Hi 512  @(transitive_lt … (pi2 ?? program)) @le_S_S >prf >append_length <plus_n_Sm @le_S_S 513 @le_plus_n_r 514  @lt_to_not_eq @le_S_S @Hi 515 ] 516 ] 517  >Hi >lookup_insert_hit #_ @refl 518 ] 519 ] 520  (* policy_compact_unsafe *) #i >append_length <commutative_plus #Hi normalize in Hi; 521 cases p p #p cases p p #fpc #sigma #Hp cases x #lbl #instr normalize nodelta 522 cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi 523 [ >lookup_opt_insert_miss 524 [ >lookup_opt_insert_miss 525 [ lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp))) i Hi) 526 lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? i) sigma)) 527 cases (bvt_lookup_opt … (bitvector_of_nat ? i) sigma) in ⊢ (???% → %); 528 [ #_ normalize nodelta / by / 529  #x cases x x #pci #ji #EQi 530 lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S i)) sigma)) 531 cases (bvt_lookup_opt … (bitvector_of_nat ? (S i)) sigma) in ⊢ (???% → %); 532 [ #_ normalize nodelta / by / 533  #x cases x x #pcSi #jSi #EQSi normalize nodelta >nth_append_first 534 [ / by / 535  @Hi 536 ] 537 ] 538 ] 539 ] 540 ] 541 [2: lapply (le_S_to_le … Hi) Hi #Hi] 542 @bitvector_of_nat_abs 543 [1,4: @(transitive_lt … (pi2 ?? program)) >prf @le_S_S >append_length <commutative_plus 544 @le_plus_a @Hi 545 2,5: @(transitive_lt … (pi2 ?? program)) >prf @le_S_S >append_length <plus_n_Sm 546 @le_S_S @le_plus_n_r 547 3,6: @lt_to_not_eq @le_S_S @Hi 548 ] 549  >lookup_opt_insert_miss 550 [ >Hi >lookup_opt_insert_hit normalize nodelta 551 >(proj2 ?? Hp) normalize nodelta >nth_append_second 552 [ <minus_n_n whd in match (nth ????); @refl 553  @le_n 554 ] 555  @bitvector_of_nat_abs 556 [ @(transitive_lt … (pi2 ?? program)) >Hi >prf @le_S_S >append_length <commutative_plus 557 @le_plus_a @le_n 558  @(transitive_lt … (pi2 ?? program)) >prf @le_S_S >append_length <plus_n_Sm 559 @le_S_S @le_plus_n_r 560  @lt_to_not_eq @le_S_S >Hi @le_n 561 ] 562 ] 563 ] 564 ] 565  (* lookup 0 = 0 *) 566 cases p p #p cases p p #pc #sigma #Hp cases x #lbl #instr normalize nodelta 567 >lookup_opt_insert_miss 568 [ @(proj2 ?? (proj1 ?? (proj1 ?? Hp))) 569  @bitvector_of_nat_abs 570 [ / by / 571  @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S <plus_n_Sm 572 @le_S_S @le_plus_n_r 573  @lt_to_not_eq / by / 574 ] 575 ] 576 ] 577  (* lookup = short_jump *) #i >append_length <commutative_plus #Hi normalize in Hi; 578 cases p p #p cases p p #pc #sigma #Hp cases x #lbl #instr normalize nodelta 579 cases (le_to_or_lt_eq … Hi) Hi #Hi 580 [ >lookup_opt_insert_miss 581 [ @(proj2 ?? (proj1 ?? Hp) i (le_S_S_to_le … Hi)) 582  @bitvector_of_nat_abs 583 [ @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S >commutative_plus 584 @le_plus_a @le_S_S_to_le @Hi 475 585  @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm @le_S_S 476 @le_ plus_n_r586 @le_S_S @le_plus_n_r 477 587  @lt_to_not_eq @Hi 478 588 ] 479 589 ] 480  >Hi >nth_append_second [2: @le_n] <minus_n_n whd in match (nth ????); 481 cases p p #p cases p p #pc #sigma #Hp cases x #lbl #ins 482 >lookup_insert_hit #_ / by / 483 ] 484 ] 485  (* policy_compact *) cases daemon 486 ] 487  (* lookup = short_jump *) #i >append_length <commutative_plus #Hi normalize in Hi; 488 cases p p #p cases p p #pc #sigma #Hp cases x #lbl #instr normalize nodelta 489 cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi 490 [ >lookup_insert_miss 491 [ @((proj2 ?? Hp) i Hi) 590  >Hi >lookup_opt_insert_hit @(ex_intro ?? (pc+instruction_size_jmplen short_jump instr)) 591 @refl 592 ] 593 ] 594  (* lookup at the end *) cases p p #p cases p p #pc #sigma #Hp cases x 595 #lbl #instr >append_length <plus_n_Sm <plus_n_O >lookup_opt_insert_hit 596 / by refl/ 597 ] 598  @conj [ @conj [ @conj [ @conj [ @conj 599 [ #i cases i 600 [ #Hi @⊥ @(absurd ? Hi) @le_to_not_lt / by / 601  i #i #Hi #Hi2 >lookup_opt_insert_miss 602 [ / by refl/ 492 603  @bitvector_of_nat_abs 493 [ @(transitive_lt … (pi2 ?? program)) >prf >append_length >commutative_plus 494 @le_plus_a @Hi 495  @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm @le_S_S 496 @le_plus_n_r 497  @lt_to_not_eq @Hi 604 [ @Hi2 605  / by / 606  @sym_neq @lt_to_not_eq / by / 498 607 ] 499 608 ] 500  >Hi >lookup_insert_hit @refl 501 ] 502 ] 503  @conj [ @conj [ @conj 504 [ #i #_ #Hi2 / by refl/ 505 ]]] 506 #i #H @⊥ @(absurd … H) @not_le_Sn_O 609 ] 610  #i cases i 611 [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O 612  i #i #Hi #Hj @⊥ @(absurd … Hi) @not_le_Sn_O 613 ] 614 ] 615  #i cases i 616 [ #Hi @⊥ @(absurd … Hi) @le_to_not_lt @le_n 617  i #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O 618 ] 619 ] 620  >lookup_opt_insert_hit @refl 621 ] 622  #i cases i 623 [ #Hi >lookup_opt_insert_hit @(ex_intro ?? 0) @refl 624  i #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O 625 ] 626 ] 627  >lookup_opt_insert_hit @refl 628 ] 507 629 ] 508 630 qed. … … 511 633 λprogram:list labelled_instruction.λp1,p2:ppc_pc_map. 512 634 (* \fst p1 = \fst p2 ∧ *) 513 (∀n:ℕ.n <program →635 (∀n:ℕ.n ≤ program → 514 636 let pc1 ≝ bvt_lookup … (bitvector_of_nat 16 n) (\snd p1) 〈0,short_jump〉 in 515 637 let pc2 ≝ bvt_lookup … (bitvector_of_nat 16 n) (\snd p2) 〈0,short_jump〉 in … … 519 641 λprogram:list labelled_instruction.λp:ppc_pc_map. 520 642 ¬(∀i.i < program → is_jump (\snd (nth i ? program 〈None ?, Comment []〉)) → 521 \snd (bvt_lookup … (bitvector_of_nat 16 i) (\snd p) 〈0,short_jump〉) = long_jump).643 \snd (bvt_lookup … (bitvector_of_nat 16 (S i)) (\snd p) 〈0,short_jump〉) = long_jump). 522 644 523 645 (*include alias "common/Identifiers.ma".*) … … 700 822 701 823 (* One step in the search for a jump expansion fixpoint. *) 702 definition jump_expansion_step: ∀program:(Σl:list labelled_instruction. l< 2^16).824 definition jump_expansion_step: ∀program:(Σl:list labelled_instruction.S (l) < 2^16). 703 825 ∀labels:(Σlm:label_map.∀l. 704 826 occurs_exactly_once ?? l program → … … 706 828 address_of_word_labels_code_mem program l). 707 829 ∀old_policy:(Σpolicy:ppc_pc_map. 708 And (And ( out_of_program_none program policy)830 And (And (And (out_of_program_none program policy) 709 831 (jump_not_in_policy program policy)) 832 (bvt_lookup_opt … (bitvector_of_nat ? 0) (\snd policy) = Some ? 〈0,short_jump〉)) 710 833 (\fst policy < 2^16)). 711 834 (Σx:bool × (option ppc_pc_map). … … 713 836 match y with 714 837 [ None ⇒ nec_plus_ultra program old_policy 715  Some p ⇒ And (And (And (And (And ( out_of_program_none program p)838  Some p ⇒ And (And (And (And (And (And (out_of_program_none program p) 716 839 (jump_not_in_policy program p)) 717 840 (policy_increase program old_policy p)) 718 841 (policy_compact program labels p)) 842 (bvt_lookup_opt … (bitvector_of_nat ? 0) (\snd p) = Some ? 〈0,short_jump〉)) 719 843 (no_ch = true → policy_equal program old_policy p)) 720 844 (\fst p < 2^16) … … 723 847 λprogram.λlabels.λold_sigma. 724 848 let 〈final_added, final_policy〉 ≝ 725 foldl_strong (option Identifier × pseudo_instruction)849 pi1 ?? (foldl_strong (option Identifier × pseudo_instruction) 726 850 (λprefix.Σx:ℕ × ppc_pc_map. 727 851 let 〈added,policy〉 ≝ x in 728 And (And (And (And ( out_of_program_none prefix policy)852 And (And (And (And (And (out_of_program_none prefix policy) 729 853 (jump_not_in_policy prefix policy)) 730 854 (policy_increase prefix old_sigma policy)) 731 (policy_compact prefix labels policy)) 855 (policy_compact_unsafe prefix labels policy)) 856 (bvt_lookup_opt … (bitvector_of_nat ? 0) (\snd policy) = Some ? 〈0,short_jump〉)) 732 857 (added = 0 → policy_equal prefix old_sigma policy)) 733 858 program … … 751 876 ] in 752 877 let 〈inc_pc, inc_sigma〉 ≝ inc_pc_sigma in 753 let 〈old_pc,old_length〉 ≝ bvt_lookup … (bitvector_of_nat ? (prefix)) (\snd old_sigma) 〈0,short_jump〉 in 878 let 〈old_pc,old_length〉 ≝ 879 bvt_lookup … (bitvector_of_nat ? (S (prefix))) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉 in 754 880 let old_size ≝ instruction_size_jmplen old_length instr in 755 881 let 〈new_length, isize〉 ≝ match add_instr with … … 761 887  Some x ⇒ plus inc_added (minus isize old_size) 762 888 ] in 763 〈new_added, 〈plus inc_pc isize, bvt_insert … (bitvector_of_nat ? (prefix)) 〈inc_pc, new_length〉 inc_sigma〉〉 764 ) 〈0, 〈0, Stub ??〉〉 in 889 〈new_added, 〈plus inc_pc isize, 890 bvt_insert … (bitvector_of_nat ? (S (prefix))) 〈inc_pc+isize, new_length〉 inc_sigma〉〉 891 ) 〈0, 〈0, bvt_insert … (bitvector_of_nat 16 0) 〈0, short_jump〉 (Stub ??)〉〉) in 765 892 if geb (\fst final_policy) 2^16 then 766 893 〈eqb final_added 0, None ?〉 … … 771 898 >H2 in H; normalize nodelta H2 x #H @conj 772 899 [ @conj 773 [ @(proj1 ?? H) 900 [ @conj 901 [ @conj 902 [ @(proj1 ?? (proj1 ?? (proj1 ?? H))) 903  cases daemon (* XXX policy_compact_unsafe → policy_compact *) 904 ] 905  @(proj2 ?? (proj1 ?? H)) 906 ] 774 907  #H2 @(proj2 ?? H) @eqb_true_to_eq @H2 775 908 ] 776 909  @not_le_to_lt @leb_false_to_not_le <geb_to_leb @p1 777 910 ] 778  lapply (pi2 ?? acc) >p cases inc_pc_sigma #inc_pc #inc_sigma779 lapply (refl ? (bvt_lookup … (bitvector_of_nat ? ( prefix)) (\snd old_sigma) 〈0,short_jump〉))780 cases (bvt_lookup … (bitvector_of_nat ? ( prefix)) (\snd old_sigma) 〈0,short_jump〉) in ⊢ (???% → %);911 4: lapply (pi2 ?? acc) >p cases inc_pc_sigma #inc_pc #inc_sigma 912 lapply (refl ? (bvt_lookup … (bitvector_of_nat ? (S (prefix))) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉)) 913 cases (bvt_lookup … (bitvector_of_nat ? (S (prefix))) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) in ⊢ (???% → %); 781 914 #old_pc #old_length #Holdeq #Hpolicy @pair_elim #added #policy normalize nodelta 782 915 @pair_elim #new_length #isize normalize nodelta #Heq1 #Heq2 783 @conj [ @conj [ @conj [ @conj 916 @conj [ @conj [ @conj [ @conj [ @conj 784 917 [ (* out_of_program_none *) #i >append_length <commutative_plus #Hi normalize in Hi; #Hi2 785 918 cases instr in Heq2; normalize nodelta 786 919 #x [6: #y] #H <(proj2 ?? (pair_destruct ?????? H)) >lookup_opt_insert_miss 787 [1,3,5,7,9,11: @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))) i ? Hi2)920 [1,3,5,7,9,11: @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) i ? Hi2) 788 921 @le_S_to_le @Hi 789 922 2,4,6,8,10,12: @bitvector_of_nat_abs … … 794 927 ] 795 928  (* jump_not_in_policy *) #i >append_length <commutative_plus #Hi normalize in Hi; 796 cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi797 [ <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss929 cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi 930 [ <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss 798 931 [ >(nth_append_first ? i prefix ?? Hi) 799 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))) i Hi)932 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) i Hi) 800 933  @bitvector_of_nat_abs 801 [ @(transitive_lt … (pi2 ?? program)) >prf >append_length >commutative_plus934 [ @(transitive_lt … (pi2 ?? program)) @le_S_S >prf >append_length >commutative_plus 802 935 @le_plus_a @Hi 803  @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm @le_S_S936  @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S <plus_n_Sm 804 937 @le_plus_n_r 805  @lt_to_not_eq @ Hi938  @lt_to_not_eq @le_S_S @Hi 806 939 ] 807 940 ] 808  >Hi <(proj2 ?? (pair_destruct ?????? Heq2))>lookup_insert_hit809 >nth_append_second810 [ <minus_n_n whd in match (nth ????); cases instr in Heq1;811 [4,5: #x #_ #H cases H #H2 @⊥ @H2 / by I/812 2,3,6: #x [3: #y] #Heq1 <(proj1 ?? (pair_destruct ?????? Heq1)) #_ / by/813 1: #pi cases pi814 [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:815 [1,2,3,6,7,24,25: #x #y816 4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] #Heq1817 <(proj1 ?? (pair_destruct ?????? Heq1)) #_ / by /818 9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y]819 #_ #H @⊥ cases H #H2 @H2 / by I/820 ]821 ]822  @le_n823 ]824 ]825 ]941  <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi >lookup_insert_hit 942 cases instr in Heq1; 943 [2,3,6: #x [3: #y] normalize nodelta #Heq1 <(proj1 ?? (pair_destruct ?????? Heq1)) #_ @refl 944 4,5: #x normalize nodelta #Heq1 #H @⊥ cases H #H @H >nth_append_second 945 [1,3: <minus_n_n whd in match (nth ????); / by I/ 946 2,4: @le_n 947 ] 948 1: #pi >nth_append_second [2: @le_n] <minus_n_n whd in match (nth ????); cases pi 949 [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: 950 [1,2,3,6,7,24,25: #x #y 951 4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] normalize nodelta #Heq1 952 <(proj1 ?? (pair_destruct ?????? Heq1)) #_ @refl 953 9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] normalize nodelta 954 #_ #H @⊥ cases H #H2 @H2 / by I/ 955 ] 956 ] 957 ] 958 ] 826 959  (* policy_increase *) #i >append_length >commutative_plus #Hi normalize in Hi; 827 960 cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi; #Hi 828 [ lapply (proj2 ?? (proj1 ?? (proj1 ?? Hpolicy)) i Hi)961 [ lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))) i Hi) 829 962 <(proj2 ?? (pair_destruct ?????? Heq2)) 830 963 @pair_elim #opc #oj #EQ1 >lookup_insert_miss 831 964 [ @pair_elim #pc #j #EQ2 / by / 832 965  @bitvector_of_nat_abs 833 [ @(transitive_lt … (pi2 ?? program)) >prf >append_length >commutative_plus @le_plus_a834 @ Hi835  @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm @le_S_S@le_plus_n_r836  @lt_to_not_eq @ Hi966 [ @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S >commutative_plus 967 @le_plus_a @Hi 968  @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S <plus_n_Sm @le_plus_n_r 969  @lt_to_not_eq @le_S_S @Hi 837 970 ] 838 971 ] … … 860 993 whd in match jump_expansion_step_instruction; normalize nodelta #Heqi #Heq1 861 994 #Hj <(proj1 ?? (pair_destruct ?????? Heq1)) 862 lapply (proj2 ?? (proj1 ?? (p i2 ?? old_sigma)) (prefix) ??)995 lapply (proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma))) (prefix) ??) 863 996 [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: 864 997 >prf >nth_append_second … … 871 1004 >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r 872 1005 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: 873 cases (lookup ?? (bitvector_of_nat ? ( prefix)) (\snd old_sigma) 〈0,short_jump〉)1006 cases (lookup ?? (bitvector_of_nat ? (S (prefix))) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) 874 1007 #a #b #H >H normalize nodelta %2 @refl 875 1008 ] … … 878 1011 ] 879 1012 2,3,6: #x [3: #y] #Heqi #Heq1 #Hj <(proj1 ?? (pair_destruct ?????? Heq1)) 880 lapply (proj2 ?? (proj1 ?? (p i2 ?? old_sigma)) (prefix) ??)1013 lapply (proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma))) (prefix) ??) 881 1014 [1,4,7: >prf >nth_append_second 882 1015 [1,3,5: <minus_n_n whd in match (nth ????); >p1 >Heqi @Hj … … 884 1017 ] 885 1018 2,5,8: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r 886 3,6,9: cases (lookup ?? (bitvector_of_nat ? ( prefix)) (\snd old_sigma) 〈0,short_jump〉)1019 3,6,9: cases (lookup ?? (bitvector_of_nat ? (S (prefix))) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) 887 1020 #a #b #H >H normalize nodelta %2 @refl 888 1021 ] … … 892 1025 ] 893 1026 ] 894  (* policy_compact *) (*XXX*) cases daemon 895 ] 1027  (* policy_compact_unsafe *) (*XXX*) cases daemon 1028 ] 1029  (* 0 ↦ 0 *) <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_opt_insert_miss 1030 [ @(proj2 ?? (proj1 ?? Hpolicy)) 1031  @bitvector_of_nat_abs 1032 [ / by / 1033  @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S <plus_n_Sm 1034 @le_S_S @le_plus_n_r 1035  @lt_to_not_eq / by / 1036 ] 1037 ] 1038 ] 896 1039  (* added = 0 → policy_equal *) lapply (proj2 ?? Hpolicy) 897 1040 lapply Heq2 Heq2 lapply Heq1 Heq1 lapply (refl ? instr) … … 903 1046 #Hins #Heq1 #Heq2 #Hold <(proj1 ?? (pair_destruct ?????? Heq2)) #Hadded 904 1047 #i >append_length >commutative_plus #Hi normalize in Hi; 905 cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi1048 cases (le_to_or_lt_eq … Hi) Hi #Hi 906 1049 [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: 907 1050 <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss 908 1051 [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: 909 @(Hold Hadded i Hi)1052 @(Hold Hadded i (le_S_S_to_le … Hi)) 910 1053 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: 911 1054 @bitvector_of_nat_abs 912 1055 [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: 913 1056 @(transitive_lt … (pi2 ?? program)) >prf >append_length >commutative_plus 914 @le_ plus_a@Hi1057 @le_S_S @le_plus_a @le_S_S_to_le @Hi 915 1058 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: 916 @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm @le_S_S1059 @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S <plus_n_Sm @le_S_S 917 1060 @le_plus_n_r 918 1061 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: … … 922 1065 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: 923 1066 <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi >lookup_insert_hit 924 lapply (proj2 ?? (proj1 ?? (p i2 ?? old_sigma)) (prefix) ??)1067 lapply (proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma))) (prefix) ??) 925 1068 [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: 926 1069 >prf >nth_append_second … … 933 1076 >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r 934 1077 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: 935 cases (bvt_lookup … (bitvector_of_nat ? ( prefix)) (\snd old_sigma) 〈0,short_jump〉)1078 cases (bvt_lookup … (bitvector_of_nat ? (S (prefix))) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) 936 1079 #a #b #H >H <(proj1 ?? (pair_destruct ?????? Heq1)) normalize nodelta @refl 937 1080 ] … … 940 1083 <(proj1 ?? (pair_destruct ?????? Heq2)) <(proj2 ?? (pair_destruct ?????? Heq1)) 941 1084 #H #i >append_length >commutative_plus #Hi normalize in Hi; 942 cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi1085 cases (le_to_or_lt_eq … Hi) Hi #Hi 943 1086 [1,3,5,7,9,11,13,15,17: <(proj2 ?? (pair_destruct ?????? Heq2)) 944 1087 >lookup_insert_miss 945 [1,3,5,7,9,11,13,15,17: @(Hold ? i Hi)1088 [1,3,5,7,9,11,13,15,17: @(Hold ? i (le_S_S_to_le … Hi)) 946 1089 [1,2,3,4,5,6,7,8,9: @sym_eq @le_n_O_to_eq <H @le_plus_n_r] 947 1090 ] 948 1091 @bitvector_of_nat_abs 949 1092 [1,4,7,10,13,16,19,22,25: @(transitive_lt … (pi2 ?? program)) >prf 950 >append_length >commutative_plus @le_ plus_a@Hi1093 >append_length >commutative_plus @le_S_S @le_plus_a @le_S_S_to_le @Hi 951 1094 2,5,8,11,14,17,20,23,26: @(transitive_lt … (pi2 ?? program)) >prf 952 >append_length <plus_n_Sm @le_S_S1095 >append_length @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r 953 1096 3,6,9,12,15,18,21,24,27: @lt_to_not_eq @Hi 954 ] @le_plus_n_r1097 ] 955 1098 2,4,6,8,10,12,14,16,18: <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi 956 1099 >lookup_insert_hit <(proj1 ?? (pair_destruct ?????? Heq1)) … … 968 1111 2,3,6: #x [3: #y] #Hins #Heq1 #Heq2 #Hold <(proj1 ?? (pair_destruct ?????? Heq2)) 969 1112 #Hadded #i >append_length >commutative_plus #Hi normalize in Hi; 970 cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi1113 cases (le_to_or_lt_eq …Hi) Hi #Hi 971 1114 [1,3,5: <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss 972 [1,3,5: @(Hold Hadded i Hi)1115 [1,3,5: @(Hold Hadded i (le_S_S_to_le … Hi)) 973 1116 2,4,6: @bitvector_of_nat_abs 974 1117 [1,4,7: @(transitive_lt … (pi2 ?? program)) >prf >append_length >commutative_plus 975 @le_ plus_a@Hi976 2,5,8: @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm @le_S_S977 @le_ plus_n_r1118 @le_S_S @le_plus_a @le_S_S_to_le @Hi 1119 2,5,8: @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S <plus_n_Sm 1120 @le_S_S @le_plus_n_r 978 1121 3,6,9: @lt_to_not_eq @Hi 979 1122 ] 980 1123 ] 981 1124 2,4,6: <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi >lookup_insert_hit 982 lapply (proj2 ?? (proj1 ?? (p i2 ?? old_sigma)) (prefix) ??)1125 lapply (proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma))) (prefix) ??) 983 1126 [1,4,7: >prf >nth_append_second 984 1127 [1,3,5: <minus_n_n whd in match (nth ????); >p1 >Hins @nmk #H @H … … 986 1129 ] 987 1130 2,5,8: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r 988 3,6,9: cases (bvt_lookup … (bitvector_of_nat ? ( prefix)) (\snd old_sigma) 〈0,short_jump〉)1131 3,6,9: cases (bvt_lookup … (bitvector_of_nat ? (S (prefix))) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) 989 1132 #a #b #H >H <(proj1 ?? (pair_destruct ?????? Heq1)) normalize nodelta @refl 990 1133 ] … … 993 1136 <(proj1 ?? (pair_destruct ?????? Heq2)) <(proj2 ?? (pair_destruct ?????? Heq1)) 994 1137 #H #i >append_length >commutative_plus #Hi normalize in Hi; 995 cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi1138 cases (le_to_or_lt_eq … Hi) Hi #Hi 996 1139 [1,3: <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss 997 [1,3: @(Hold ? i Hi)1140 [1,3: @(Hold ? i (le_S_S_to_le … Hi)) 998 1141 [1,2: @sym_eq @le_n_O_to_eq <H @le_plus_n_r] 999 1142 ] 1000 1143 @bitvector_of_nat_abs 1001 1144 [1,4: @(transitive_lt … (pi2 ?? program)) >prf 1002 >append_length >commutative_plus @le_ plus_a@Hi1145 >append_length >commutative_plus @le_S_S @le_plus_a @le_S_S_to_le @Hi 1003 1146 2,5: @(transitive_lt … (pi2 ?? program)) >prf 1004 >append_length <plus_n_Sm @le_S_S1147 >append_length @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r 1005 1148 3,6: @lt_to_not_eq @Hi 1006 ] @le_plus_n_r1149 ] 1007 1150 2,4: <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi >lookup_insert_hit 1008 1151 <(proj1 ?? (pair_destruct ?????? Heq1))>Holdeq normalize nodelta … … 1018 1161 ] 1019 1162 ] 1020  normalize nodelta @conj [ @conj [ @conj [ @conj 1021 [ #i #Hi / by refl/ 1022  / by refl/ 1023 ]]]] 1024 [3: #_] 1025 #i #Hi @⊥ @(absurd ? Hi) @not_le_Sn_O 1163  normalize nodelta @conj [ @conj [ @conj [ @conj [ @conj 1164 [ #i cases i 1165 [ #Hi @⊥ @(absurd ? Hi) @le_to_not_lt / by / 1166  i #i #Hi #Hi2 >lookup_opt_insert_miss 1167 [ / by refl/ 1168  @bitvector_of_nat_abs 1169 [ @Hi2 1170  / by / 1171  @sym_neq @lt_to_not_eq / by / 1172 ] 1173 ] 1174 ] 1175  #i cases i 1176 [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O 1177  i #i #Hi #Hj @⊥ @(absurd … Hi) @not_le_Sn_O 1178 ] 1179 ] 1180  #i cases i 1181 [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O 1182  i #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O 1183 ] 1184 ] 1185  #i cases i 1186 [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O 1187  i #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O 1188 ] 1189 ] 1190  >lookup_opt_insert_hit @refl 1191 ] 1192  #_ #i cases i 1193 [ #Hi >lookup_insert_hit 1194 >(lookup_opt_lookup_hit … (proj2 ?? (proj1 ?? (pi2 ?? old_sigma))) 〈0,short_jump〉) 1195 @refl 1196  i #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O 1197 ] 1198 ] 1026 1199 ] 1027 1200 qed. 1028 1201 1029 let rec jump_expansion_internal (program: Σl:list labelled_instruction.lt ( length ? l) 2^16) (n: ℕ)1202 let rec jump_expansion_internal (program: Σl:list labelled_instruction.lt (S (l)) 2^16) (n: ℕ) 1030 1203 on n:(Σx:bool × (option ppc_pc_map). 1031 1204 let 〈c,pol〉 ≝ x in … … 1033 1206 [ None ⇒ True 1034 1207  Some x ⇒ 1035 And (And (And 1208 And (And (And (And 1036 1209 (out_of_program_none program x) 1037 1210 (jump_not_in_policy program x)) 1038 (policy_compact program (create_label_map program) x)) 1211 (n > 0 → policy_compact program (create_label_map program) x)) 1212 (bvt_lookup_opt … (bitvector_of_nat ? 0) (\snd x) = Some ? 〈0,short_jump〉)) 1039 1213 (\fst x < 2^16) 1040 1214 ]) ≝ … … 1051 1225 ]. 1052 1226 [ normalize nodelta cases (jump_expansion_start program (create_label_map program)) 1053 # p cases p1227 #x cases x x 1054 1228 [ / by I/ 1055  #pm normalize nodelta #H @conj [ @(proj1 ?? (proj1 ?? H))  @(proj2 ?? H) ] 1056 ] 1229  #sigma normalize nodelta #H @conj [ @conj [ @conj 1230 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))) 1231  #H @⊥ @(absurd ? H) @le_to_not_lt @le_n 1232 ] 1233  @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) 1234 ] 1235  @(proj2 ?? H) ] 1236 ] 1237  cases daemon 1057 1238  lapply (pi2 ?? (jump_expansion_internal program m)) <p1 >p2 normalize nodelta / by / 1058 1239  lapply (pi2 ?? (jump_expansion_internal program m)) <p1 >p2 normalize nodelta 1059 #H @conj [ @ (proj1 ?? (proj1 ?? H)) @(proj2 ?? H) ]1240 #H @conj [ @conj [ @(proj1 ?? (proj1 ?? (proj1 ?? H)))  @(proj2 ?? (proj1 ?? H)) ]  @(proj2 ?? H) ] 1060 1241  normalize nodelta cases (jump_expansion_step program labels «op,?») 1061 1242 #p cases p p #p #r cases r normalize nodelta … … 1063 1244  #j #H @conj 1064 1245 [ @conj 1065 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) 1246 [ @conj 1247 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))) 1248  cases daemon 1249 ] 1066 1250  @(proj2 ?? (proj1 ?? (proj1 ?? H))) 1067 1251 ] … … 1158 1342 qed. 1159 1343 1160 lemma pe_step: ∀program:(Σl:list labelled_instruction. l< 2^16).1344 lemma pe_step: ∀program:(Σl:list labelled_instruction.S (l) < 2^16). 1161 1345 ∀n.policy_equal_opt program (\snd (pi1 ?? (jump_expansion_internal program n))) 1162 1346 (\snd (pi1 ?? (jump_expansion_internal program (S n)))) → … … 1171 1355 #n (elim n) normalize /2 by S_pred/ qed. 1172 1356 1173 lemma equal_remains_equal: ∀program:(Σl:list labelled_instruction. l< 2^16).∀n:ℕ.1357 lemma equal_remains_equal: ∀program:(Σl:list labelled_instruction.S (l) < 2^16).∀n:ℕ. 1174 1358 policy_equal_opt program (\snd (pi1 … (jump_expansion_internal program n))) 1175 1359 (\snd (pi1 … (jump_expansion_internal program (S n)))) → … … 1192 1376 match program with 1193 1377 [ nil ⇒ acc 1194  cons h t ⇒ match (\snd (bvt_lookup ?? (bitvector_of_nat ? ( t)) (\snd policy) 〈0,short_jump〉)) with1378  cons h t ⇒ match (\snd (bvt_lookup ?? (bitvector_of_nat ? (S (t))) (\snd policy) 〈0,short_jump〉)) with 1195 1379 [ long_jump ⇒ measure_int t policy (acc + 2) 1196 1380  medium_jump ⇒ measure_int t policy (acc + 1) … … 1206 1390 [ / by refl/ 1207 1391  #h #t #Hd #x whd in match (measure_int ???); whd in match (measure_int ?? x); 1208 cases (\snd (bvt_lookup … (bitvector_of_nat ? ( t)) (\snd policy) 〈0,short_jump〉))1392 cases (\snd (bvt_lookup … (bitvector_of_nat ? (S (t))) (\snd policy) 〈0,short_jump〉)) 1209 1393 [ normalize nodelta @Hd 1210 1394 2,3: normalize nodelta >associative_plus >(commutative_plus (S d) ?) <associative_plus … … 1220 1404 [ normalize @le_n 1221 1405  #h #t #Hind whd in match (measure_int ???); 1222 cases (\snd (lookup ?? (bitvector_of_nat ? ( t)) (\snd policy) 〈0,short_jump〉))1406 cases (\snd (lookup ?? (bitvector_of_nat ? (S (t))) (\snd policy) 〈0,short_jump〉)) 1223 1407 [ normalize nodelta @(transitive_le ??? Hind) /2 by monotonic_le_times_r/ 1224 1408 2,3: normalize nodelta >measure_plus <times_n_Sm >(commutative_plus 2 ?) … … 1229 1413 1230 1414 (* uses the second part of policy_increase *) 1231 lemma measure_incr_or_equal: ∀program:Σl:list labelled_instruction. l<2^16.1415 lemma measure_incr_or_equal: ∀program:Σl:list labelled_instruction.S (l) <2^16. 1232 1416 ∀policy:Σp:ppc_pc_map. 1233 1417 out_of_program_none program p ∧ 1234 jump_not_in_policy program p ∧ \fst p < 2^16. 1418 jump_not_in_policy program p ∧ 1419 lookup_opt … (bitvector_of_nat ? 0) (\snd p) = Some ? 〈0,short_jump〉 ∧ 1420 \fst p < 2^16. 1235 1421 ∀l.l ≤ program → ∀acc:ℕ. 1236 match \snd ( jump_expansion_step program (create_label_map program) policy) with1422 match \snd (pi1 ?? (jump_expansion_step program (create_label_map program) policy)) with 1237 1423 [ None ⇒ True 1238 1424  Some p ⇒ measure_int l policy acc ≤ measure_int l p acc … … 1244 1430 cases (jump_expansion_step ???) in ⊢ (???% → %); #pi1 cases pi1 pi1 #c #r cases r 1245 1431 [ / by I/ 1246  #x normalize nodelta #Hx #Hjeq lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hx))) (t) Hp) 1432  #x normalize nodelta #Hx #Hjeq 1433 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hx)))) (t) Hp) 1247 1434 whd in match (measure_int ???); whd in match (measure_int ? x ?); 1248 cases (bvt_lookup ?? (bitvector_of_nat ? ( t)) (\snd policy) 〈0,short_jump〉)1249 #x1 #x2 cases (bvt_lookup ?? (bitvector_of_nat ? ( t)) (\snd x) 〈0,short_jump〉)1250 #y1 #y2 normalize nodelta #Hblerp cases Hblerp cases x2 cases y2 1435 cases (bvt_lookup ?? (bitvector_of_nat ? (S (t))) (\snd (pi1 ?? policy)) 〈0,short_jump〉) 1436 #x1 #x2 cases (bvt_lookup ?? (bitvector_of_nat ? (S (t))) (\snd x) 〈0,short_jump〉) 1437 #y1 #y2 normalize nodelta #Hblerp cases Hblerp cases x2 cases y2 1251 1438 [1,4,5,7,8,9: #H cases H 1252 1439 2,3,6: #_ normalize nodelta … … 1281 1468 measure_int program policy 0 = 2*program → ∀i.i<program → 1282 1469 is_jump (\snd (nth i ? program 〈None ?,Comment []〉)) → 1283 (\snd (bvt_lookup ?? (bitvector_of_nat ? i) (\snd policy) 〈0,short_jump〉)) = long_jump.1470 (\snd (bvt_lookup ?? (bitvector_of_nat ? (S i)) (\snd policy) 〈0,short_jump〉)) = long_jump. 1284 1471 #program #policy elim program in ⊢ (% → ∀i.% → ? → %); 1285 1472 [ #Hm #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O … … 1288 1475 [ #Hi @Hind 1289 1476 [ whd in match (measure_int ???) in Hm; 1290 cases (\snd (bvt_lookup … (bitvector_of_nat ? ( t)) (\snd policy) 〈0,short_jump〉)) in Hm;1477 cases (\snd (bvt_lookup … (bitvector_of_nat ? (S (t))) (\snd policy) 〈0,short_jump〉)) in Hm; 1291 1478 normalize nodelta 1292 1479 [ #H @⊥ @(absurd ? (measure_le t policy)) >H @lt_to_not_le /2 by lt_plus, le_n/ … … 1299 1486 ] 1300 1487  #Hi >(injective_S … Hi) whd in match (measure_int ???) in Hm; 1301 cases (\snd (bvt_lookup … (bitvector_of_nat ? ( t)) (\snd policy) 〈0,short_jump〉)) in Hm;1488 cases (\snd (bvt_lookup … (bitvector_of_nat ? (S (t))) (\snd policy) 〈0,short_jump〉)) in Hm; 1302 1489 normalize nodelta 1303 1490 [ #Hm @⊥ @(absurd ? (measure_le t policy)) >Hm @lt_to_not_le /2 by lt_plus, le_n/ … … 1311 1498 1312 1499 (* uses second part of policy_increase *) 1313 lemma measure_special: ∀program:(Σl:list labelled_instruction. l< 2^16).1500 lemma measure_special: ∀program:(Σl:list labelled_instruction.(S (l)) < 2^16). 1314 1501 ∀policy:Σp:ppc_pc_map. 1315 out_of_program_none program p ∧ jump_not_in_policy program p ∧ \fst p < 2^16. 1502 out_of_program_none program p ∧ jump_not_in_policy program p ∧ 1503 bvt_lookup_opt … (bitvector_of_nat ? 0) (\snd p) = Some ? 〈0,short_jump〉 ∧ 1504 \fst p < 2^16. 1316 1505 match (\snd (pi1 ?? (jump_expansion_step program (create_label_map program) policy))) with 1317 1506 [ None ⇒ True … … 1325 1514 measure_int x policy 0 = measure_int x p 0 → 1326 1515 policy_equal x policy p) ?? (pi1 ?? program)) 1327 [ #_ #_ #i #Hi @⊥ @(absurd ? Hi) @not_le_Sn_O 1516 [ #_ #_ #i #Hi <(le_n_O_to_eq … Hi) 1517 >(lookup_opt_lookup_hit … 〈0,short_jump〉 (proj2 ?? (proj1 ?? (proj1 ?? Hpol)))) 1518 >(lookup_opt_lookup_hit … 〈0,short_jump〉 (proj2 ?? (proj1 ?? (pi2 ?? policy)))) 1519 / by refl/ 1328 1520  #h #t #Hind #Hp #Hm #i #Hi cases (le_to_or_lt_eq … Hi) Hi; 1329 1521 [ #Hi @Hind 1330 1522 [ @(transitive_le … Hp) / by / 1331 1523  whd in match (measure_int ???) in Hm; whd in match (measure_int ? p ?) in Hm; 1332 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol))) (t) Hp) #Hinc1333 cases (bvt_lookup ?? (bitvector_of_nat ? ( t)) ? 〈0,short_jump〉) in Hm Hinc; #x1 #x21334 cases (bvt_lookup ?? (bitvector_of_nat ? ( t)) ? 〈0,short_jump〉); #y1 #y21524 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol)))) (t) Hp) #Hinc 1525 cases (bvt_lookup ?? (bitvector_of_nat ? (S (t))) ? 〈0,short_jump〉) in Hm Hinc; #x1 #x2 1526 cases (bvt_lookup ?? (bitvector_of_nat ? (S (t))) ? 〈0,short_jump〉); #y1 #y2 1335 1527 #Hm #Hinc lapply Hm Hm; lapply Hinc Hinc; normalize nodelta 1336 1528 cases x2 cases y2 normalize nodelta … … 1352 1544  @(le_S_S_to_le … Hi) 1353 1545 ] 1354  #Hi > (injective_S … Hi)whd in match (measure_int ???) in Hm;1546  #Hi >Hi whd in match (measure_int ???) in Hm; 1355 1547 whd in match (measure_int ? p ?) in Hm; 1356 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol))) (t) Hp)1357 cases (bvt_lookup ?? (bitvector_of_nat ? ( t)) ? 〈0,short_jump〉) in Hm;1548 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol)))) (t) Hp) 1549 cases (bvt_lookup ?? (bitvector_of_nat ? (S (t))) ? 〈0,short_jump〉) in Hm; 1358 1550 #x1 #x2 1359 cases (bvt_lookup ?? (bitvector_of_nat ? ( t)) ? 〈0,short_jump〉);1360 #y1 #y2 1551 cases (bvt_lookup ?? (bitvector_of_nat ? (S (t))) ? 〈0,short_jump〉); 1552 #y1 #y2 1361 1553 normalize nodelta cases x2 cases y2 normalize nodelta 1362 1554 [1,5,9: #_ #_ @refl … … 1390 1582 qed. 1391 1583 1392 lemma measure_zero: ∀l.∀program:Σl:list labelled_instruction. l< 2^16.1584 lemma measure_zero: ∀l.∀program:Σl:list labelled_instruction.S (l) < 2^16. 1393 1585 match jump_expansion_start program (create_label_map program) with 1394 1586 [ None ⇒ True … … 1402 1594 [ / by refl/ 1403 1595  #h #t #Hind #Hp whd in match (measure_int ???); 1404 >(proj2 ?? (proj1 ?? Hpl) (t))1405 [ normalize nodelta @Hind ]1406 @(transitive_le … Hp) [ @le_n_Sn  @ le_n ]1596 elim (proj2 ?? (proj1 ?? (proj1 ?? Hpl)) (S (t)) Hp) 1597 #pc #Hpc >(lookup_opt_lookup_hit … Hpc 〈0,short_jump〉) normalize nodelta @Hind 1598 @(transitive_le … Hp) @le_n_Sn 1407 1599 ] 1408 1600 ] … … 1410 1602 1411 1603 (* the actual computation of the fixpoint *) 1412 definition je_fixpoint: ∀program:(Σl:list labelled_instruction. l< 2^16).1604 definition je_fixpoint: ∀program:(Σl:list labelled_instruction.S (l) < 2^16). 1413 1605 Σp:option ppc_pc_map. 1414 1606 And (match p with 1415 1607 [ None ⇒ True 1416 1608  Some pol ⇒ And (out_of_program_none program pol) 1417 ( policy_compact program (create_label_map program) pol)1609 ((pi1 ?? program) ≠ [] → policy_compact program (create_label_map program) pol) 1418 1610 ]) 1419 1611 (∃n.∀k.n < k → … … 1424 1616 #c #pol #Hp cases pol 1425 1617 [ normalize nodelta // 1426  #x normalize nodelta #H @conj [ @(proj1 ?? (proj1 ?? (proj1 ?? H))) 1427  cases daemon ] ] 1618  #x normalize nodelta #H @conj [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) 1619  #Hneq @(proj2 ?? (proj1 ?? (proj1 ?? H))) cases (pi1 ?? program) in Hneq; 1620 [ #H cases H #H @⊥ @H @refl 1621  #h #t #_ / by / 1622 ] ] 1623 ] 1428 1624  cases (dec_bounded_exists (λk.policy_equal_opt (pi1 ?? program) 1429 1625 (\snd (pi1 ?? (jump_expansion_internal program k))) … … 1438 1634  @equal_remains_equal 1439 1635 [ @(proj2 ?? Hx) 1440  @ le_S_S_to_le @le_S @(proj1 ?? Hx)1636  @(proj1 ?? Hx) 1441 1637 ] 1442 1638 ] … … 1452 1648 >EQ normalize nodelta 1453 1649 lapply (refl ? (jump_expansion_step program (create_label_map program) «Fp,?»)) 1454 [ @conj [ @(proj1 ?? (proj1 ?? HFp))  @(proj2 ?? HFp) ] 1650 [ @conj [ @conj 1651 [ @(proj1 ?? (proj1 ?? (proj1 ?? HFp))) 1652  @(proj2 ?? (proj1 ?? HFp)) ] 1653  @(proj2 ?? HFp) ] 1455 1654  lapply (measure_full program Fp ?) 1456 1655 [ @le_to_le_to_eq … … 1489 1688 [ cases (jump_expansion_internal program x) in Hxpol; 1490 1689 #z cases z z #xch #xpol normalize nodelta #H #H2 >(proj1 ?? H2) in H; 1491 normalize nodelta #H @conj [ @(proj1 ?? (proj1 ?? H))  @(proj2 ?? H) ] 1492  lapply (Hfa x Hx) lapply HeqSxpol HeqSxpol 1690 normalize nodelta #H @conj [ @conj 1691 [ @(proj1 ?? (proj1 ?? (proj1 ?? H))) 1692  @(proj2 ?? (proj1 ?? H)) ] 1693  @(proj2 ?? H) ] 1694  lapply (Hfa x (le_S_to_le … Hx)) lapply HeqSxpol HeqSxpol 1493 1695 whd in match (jump_expansion_internal program (S x)); 1494 1696 lapply (refl ? (jump_expansion_internal program x)) … … 1497 1699 #H #Heq cases xch in Heq; #Heq normalize nodelta 1498 1700 [ lapply (refl ? (jump_expansion_step program (create_label_map (pi1 ?? program)) «xpol,?»)) 1499 [ @conj [ @(proj1 ?? (proj1 ?? H))  @(proj2 ?? H) ] 1701 [ @conj [ @conj 1702 [ @(proj1 ?? (proj1 ?? (proj1 ?? H))) 1703  @(proj2 ?? (proj1 ?? H)) ] 1704  @(proj2 ?? H) ] 1500 1705  cases (jump_expansion_step ???) in ⊢ (???% → %); #z cases z z #a #c 1501 1706 normalize nodelta cases c normalize nodelta … … 1504 1709 [ / by / 1505 1710  #H3 lapply (measure_special program «xpol,?») 1506 [ @conj [ @(proj1 ?? (proj1 ?? H))  @(proj2 ?? H) ] 1711 [ @conj [ @conj 1712 [ @(proj1 ?? (proj1 ?? (proj1 ?? H))) 1713  @(proj2 ?? (proj1 ?? H)) ] 1714  @(proj2 ?? H) ] 1507 1715  >Heq normalize nodelta #H4 @⊥ @(absurd … (H4 H3)) @Hfull 1508 1716 ] … … 1511 1719 ] 1512 1720  lapply (refl ? (jump_expansion_step program (create_label_map (pi1 ?? program)) «xpol,?»)) 1513 [ @conj [ @(proj1 ?? (proj1 ?? H))  @(proj2 ?? H) ] 1721 [ @conj [ @conj 1722 [ @(proj1 ?? (proj1 ?? (proj1 ?? H))) 1723  @(proj2 ?? (proj1 ?? H)) ] 1724  @(proj2 ?? H) ] 1514 1725  cases (jump_expansion_step ???) in ⊢ (???% → %); #z cases z z #a #c 1515 1726 normalize nodelta cases c normalize nodelta … … 1531 1742 [ #H #EQ2 @⊥ @(absurd ?? H) @Hfull 1532 1743  #Gp #HGp #EQ2 cases Fch 1533 [ normalize nodelta #i #Hi 1534 cases (dec_is_jump (\snd (nth i ? program 〈None ?, Comment []〉))) #Hj 1535 [ lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp))) i Hi) 1536 lapply (Hfull i Hi Hj) cases (bvt_lookup … (bitvector_of_nat ? i) (\snd Fp) 〈0,short_jump〉) 1537 #fp #fj #Hfj >Hfj normalize nodelta 1538 cases (bvt_lookup … (bitvector_of_nat ? i) (\snd Gp) 〈0,short_jump〉) #gp #gj 1539 cases gj normalize nodelta 1540 [1,2: #H cases H #H2 cases H2 destruct (H2) 1541 3: #_ @refl 1744 [ normalize nodelta #i cases i 1745 [ #_ >(lookup_opt_lookup_hit … (proj2 ?? (proj1 ?? HFp)) 〈0,short_jump〉) 1746 >(lookup_opt_lookup_hit … (proj2 ?? (proj1 ?? (proj1 ?? HGp))) 〈0,short_jump〉) 1747 / by refl/ 1748  i #i #Hi 1749 cases (dec_is_jump (\snd (nth i ? program 〈None ?, Comment []〉))) #Hj 1750 [ lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp)))) i Hi) 1751 lapply (Hfull i Hi Hj) 1752 cases (bvt_lookup … (bitvector_of_nat ? (S i)) (\snd Fp) 〈0,short_jump〉) 1753 #fp #fj #Hfj >Hfj normalize nodelta 1754 cases (bvt_lookup … (bitvector_of_nat ? (S i)) (\snd Gp) 〈0,short_jump〉) 1755 #gp #gj cases gj normalize nodelta 1756 [1,2: #H cases H #H2 cases H2 destruct (H2) 1757 3: #_ @refl 1758 ] 1759  >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp))))) i Hi Hj) 1760 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp))) i Hi Hj) @refl 1542 1761 ] 1543  >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp)))) i Hi Hj)1544 >(proj2 ?? (proj1 ?? (proj1 ?? HFp)) i Hi Hj) @refl1545 1762 ] 1546 1763  normalize nodelta /2 by pe_int_refl/ … … 1560 1777 #H destruct (H) 1561 1778 4: #np #Hnp #Sp #HSp whd in match (policy_equal ???); @dec_bounded_forall #m 1562 1563 1564 1565 1566 1779 cases (bvt_lookup ?? (bitvector_of_nat 16 m) ? 〈0,short_jump〉) 1780 #x1 #x2 1781 cases (bvt_lookup ?? (bitvector_of_nat ? m) ? 〈0,short_jump〉) 1782 #y1 #y2 normalize nodelta 1783 @dec_eq_jump_length 1567 1784 ] 1568 1785 ] … … 1574 1791 (* The glue between Policy and Assembly. *) 1575 1792 definition jump_expansion': 1576 ∀program:preamble × (Σl:list labelled_instruction. l< 2^16).1793 ∀program:preamble × (Σl:list labelled_instruction.S (l) < 2^16). 1577 1794 option (Σsigma:Word → Word × bool. 1578 1795 ∀ppc: Word.
Note: See TracChangeset
for help on using the changeset viewer.