Changeset 1937 for src/ASM/Policy.ma
 Timestamp:
 May 11, 2012, 3:06:15 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Policy.ma
r1934 r1937 15 15 16 16 (* ppc_pc_map: program length × (pseudo program counter ↦ 〈pc, jump_length〉) *) 17 definition ppc_pc_map ≝ ℕ × (BitVectorTrie (ℕ × bool) 16).17 definition ppc_pc_map ≝ ℕ × (BitVectorTrie (ℕ × jump_length) 16). 18 18 19 19 (* The different properties that we want/need to prove at some point *) … … 85 85 86 86 (* Between two policies, jumps cannot decrease *) 87 definition jmpeqb: jump_length → jump_length → bool ≝ 88 λj1.λj2. 89 match j1 with 90 [ short_jump ⇒ match j2 with [ short_jump ⇒ true  _ ⇒ false ] 91  medium_jump ⇒ match j2 with [ medium_jump ⇒ true  _ ⇒ false ] 92  long_jump ⇒ match j2 with [ long_jump ⇒ true  _ ⇒ false ] 93 ]. 94 95 lemma jmpeqb_to_eq: ∀j1,j2.jmpeqb j1 j2 → j1 = j2. 96 #j1 #j2 cases j1 cases j2 97 [1,5,9: / by /] 98 #H cases H 99 qed. 100 87 101 definition jmple: jump_length → jump_length → Prop ≝ 88 102 λj1.λj2. … … 108 122 λprogram.λop.λp. 109 123 ∀i.i < program → 110 let 〈opc,ox〉 ≝ bvt_lookup … (bitvector_of_nat 16 i) (\snd op) 〈0,false〉 in 111 let 〈pc,x〉 ≝ bvt_lookup … (bitvector_of_nat 16 i) (\snd p) 〈0,false〉 in 112 opc ≤ pc. 113 (*∧ match ox with 114 [ Some oj ⇒ 115 match x with 116 [ Some j ⇒ jmpleq oj j 117  _ ⇒ True 118 ] 119  _ ⇒ True 120 ].*) 121 122 (* 124 let 〈opc,oj〉 ≝ bvt_lookup … (bitvector_of_nat 16 i) (\snd op) 〈0,short_jump〉 in 125 let 〈pc,j〉 ≝ bvt_lookup … (bitvector_of_nat 16 i) (\snd p) 〈0,short_jump〉 in 126 opc ≤ pc ∧ jmpleq oj j. 123 127 124 128 (* Policy safety *) … … 149 153 150 154 (* this is the instruction size as determined by the distance from origin to destination *) 151 definition instruction_size_sigma: label_map → ppc_pc_map → Word → pseudo_instruction → ℕ ≝155 (*definition instruction_size_sigma: label_map → ppc_pc_map → Word → pseudo_instruction → ℕ ≝ 152 156 λlabels.λsigma.λpc.λi. 153 157 \fst (assembly_1_pseudoinstruction 154 158 (λid.bitvector_of_nat 16 (lookup_def … labels id 0)) 155 (λi.bitvector_of_nat 16 (\fst (bvt_lookup ?? i (\snd sigma) 〈0, None ?〉))) pc156 (λx.zero 16) i). 159 (λi.bitvector_of_nat 16 (\fst (bvt_lookup ?? i (\snd sigma) 〈0,false〉))) pc 160 (λx.zero 16) i).*) 157 161 158 162 (* this is the instruction size as determined by the jump length given *) … … 255 259 [ None ⇒ False 256 260  Some x1 ⇒ let 〈pc1,j1〉 ≝ x1 in 257 pc1 = instruction_size_sigma labels sigma (bitvector_of_nat ? pc) (\snd (nth n ? program 〈None ?, Comment []〉)) 261 pc1 = instruction_size (λid.bitvector_of_nat ? (lookup_def ?? labels id 0)) 262 (λppc.let 〈x,y〉 ≝ bvt_lookup ?? ppc (\snd sigma) 〈0,short_jump〉 in 263 〈bitvector_of_nat ? x, jmpeqb y long_jump〉) 264 (bitvector_of_nat ? pc) (\snd (nth n ? program 〈None ?, Comment []〉)) 258 265 ] 259 266 ]. … … 297 304 prefix 298 305 (λhd.λx.λtl.λp.λacc. 299 acc + (instruction_size_sigma labels sigma (bitvector_of_nat 16 (\fst sigma)) (\snd x))) 306 acc + (instruction_size (λid.bitvector_of_nat ? (lookup_def ?? labels id 0)) 307 (λppc.let 〈x,y〉 ≝ bvt_lookup ?? ppc (\snd sigma) 〈0,short_jump〉 in 308 〈bitvector_of_nat ? x, jmpeqb y long_jump〉) 309 (bitvector_of_nat 16 (\fst sigma)) (\snd x))) 300 310 0. 301 311 … … 309 319 ) ≝ 310 320 λprogram. 311 321 \fst (create_label_cost_map program). 322 #i #Hi #l #Hl1 #Hl2 lapply (pi2 ?? (create_label_cost_map program)) @pair_elim 323 #labels #costs #EQ normalize nodelta #H @(H i Hi l Hl1 Hl2) 312 324 qed. 313 325 … … 318 330 if leb ppc paddr (* forward jump *) 319 331 then 320 let addr ≝ \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd old_sigma) 〈0, None ?〉)332 let addr ≝ \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd old_sigma) 〈0,short_jump〉) 321 333 + added in 322 334 if leb (addr  \fst inc_sigma) 126 … … 324 336 else long_jump 325 337 else 326 let addr ≝ \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd inc_sigma) 〈0, None ?〉) in338 let addr ≝ \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd inc_sigma) 〈0,short_jump〉) in 327 339 if leb (\fst inc_sigma  addr) 129 328 340 then short_jump … … 335 347 let addr ≝ 336 348 if leb ppc paddr (* forward jump *) 337 then \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd old_sigma) 〈0, None ?〉)349 then \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd old_sigma) 〈0,short_jump〉) 338 350 + added 339 else \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd inc_sigma) 〈0, None ?〉) in351 else \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd inc_sigma) 〈0,short_jump〉) in 340 352 let 〈fst_5_addr, rest_addr〉 ≝ split ? 5 11 (bitvector_of_nat ? addr) in 341 353 let 〈fst_5_pc, rest_pc〉 ≝ split ? 5 11 (bitvector_of_nat ? (\fst inc_sigma)) in … … 350 362 if leb ppc paddr (* forward jump *) 351 363 then 352 let addr ≝ \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd old_sigma) 〈0, None ?〉)364 let addr ≝ \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd old_sigma) 〈0,short_jump〉) 353 365 + added in 354 366 if leb (addr  \fst inc_sigma) 126 … … 356 368 else select_call_length labels old_sigma inc_sigma added ppc lbl 357 369 else 358 let addr ≝ \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd inc_sigma) 〈0, None ?〉) in370 let addr ≝ \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd inc_sigma) 〈0,short_jump〉) in 359 371 if leb (\fst inc_sigma  addr) 129 360 372 then short_jump … … 394 406 qed. 395 407 396 lemma jump_not_in_policy: ∀prefix:list labelled_instruction.408 (*lemma jump_not_in_policy: ∀prefix:list labelled_instruction. 397 409 ∀policy:(Σp:ppc_pc_map. 398 410 out_of_program_none prefix p ∧ jump_in_policy prefix p). … … 411 423 #H elim H H; #x #H >H in Hnone; #abs destruct (abs) 412 424 ] 413 qed. 414 415 (* these two obviously belong somewhere else *) 416 lemma pi1_eq: ∀A:Type[0].∀P:A>Prop.∀s1:Σa1:A.P a1.∀s2:Σa2:A.P a2. 417 s1 = s2 → (pi1 ?? s1) = (pi1 ?? s2). 418 #A #P #s1 #s2 / by / 419 qed. 420 421 lemma Some_eq: 422 ∀T:Type[0].∀x,y:T. Some T x = Some T y → x = y. 423 #T #x #y #H @option_destruct_Some @H 424 qed. 425 qed.*) 425 426 426 427 (* The first step of the jump expansion: everything to short. … … 431 432 ∀labels:label_map. 432 433 Σpolicy:ppc_pc_map. 433 And (And (out_of_program_none (pi1 ?? program) policy) 434 (jump_in_policy (pi1 ?? program) policy)) 434 And (out_of_program_none (pi1 ?? program) policy) 435 435 (policy_isize_sum (pi1 ?? program) labels policy) ≝ 436 436 λprogram.λlabels. 437 437 foldl_strong (option Identifier × pseudo_instruction) 438 438 (λprefix.Σpolicy:ppc_pc_map. 439 And (And (out_of_program_none prefix policy) 440 (jump_in_policy prefix policy)) 439 And (out_of_program_none prefix policy) 441 440 (policy_isize_sum prefix labels policy)) 442 441 program … … 448 447 match instr with 449 448 [ Instruction i ⇒ match i with 450 [ JC jmp ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈pc, Some ?short_jump〉 sigma451  JNC _ ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈pc, Some ?short_jump〉 sigma452  JZ _ ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈pc, Some ?short_jump〉 sigma453  JNZ _ ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈pc, Some ?short_jump〉 sigma454  JB _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈pc, Some ?short_jump〉 sigma455  JNB _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈pc, Some ?short_jump〉 sigma456  JBC _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈pc, Some ?short_jump〉 sigma457  CJNE _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈pc, Some ?short_jump〉 sigma458  DJNZ _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈pc, Some ?short_jump〉 sigma459  _ ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈pc, None ?〉 sigma449 [ JC jmp ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈pc,short_jump〉 sigma 450  JNC _ ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈pc,short_jump〉 sigma 451  JZ _ ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈pc,short_jump〉 sigma 452  JNZ _ ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈pc,short_jump〉 sigma 453  JB _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈pc,short_jump〉 sigma 454  JNB _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈pc,short_jump〉 sigma 455  JBC _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈pc,short_jump〉 sigma 456  CJNE _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈pc,short_jump〉 sigma 457  DJNZ _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈pc,short_jump〉 sigma 458  _ ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈pc,short_jump〉 sigma 460 459 ] 461  Call c ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈pc, Some ?short_jump〉 sigma462  Jmp j ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈pc, Some ?short_jump〉 sigma463  _ ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈pc, None ?〉 sigma460  Call c ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈pc,short_jump〉 sigma 461  Jmp j ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈pc,short_jump〉 sigma 462  _ ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈pc,short_jump〉 sigma 464 463 ]〉 465 464 ) 〈0, Stub ? ?〉. 466 [ @conj [ @conj #i >append_length <commutative_plus #Hi normalize in Hi;467 [ # Hi2465 [ @conj 466 [ #i >append_length <commutative_plus #Hi normalize in Hi; #Hi2 468 467 cases (le_to_or_lt_eq … Hi) Hi #Hi 469 468 cases p p #p cases p p #pc #p #Hp cases x x #l #pi cases pi … … 482 481 ] 483 482 ] 484 @(proj1 ?? (proj1 ?? Hp)i ? Hi2) @le_S_to_le @le_S_to_le @Hi483 @(proj1 ?? Hp i ? Hi2) @le_S_to_le @le_S_to_le @Hi 485 484 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: 486 485 [1,2,3,6,7,24,25: #x #y … … 497 496 ] 498 497 ] 499 <Hi @(proj1 ?? (proj1 ?? Hp)(S (prefix)) (le_S ?? (le_n (prefix))) ?)498 <Hi @(proj1 ?? Hp (S (prefix)) (le_S ?? (le_n (prefix))) ?) 500 499 >Hi @Hi2 501 500 9,10,11,12,13,14,15,16,17: … … 507 506 ] 508 507 1,3,5,7,9,11,13,15,17: 509 @(proj1 ?? (proj1 ?? Hp)i ? Hi2) @le_S_to_le @le_S_to_le @Hi508 @(proj1 ?? Hp i ? Hi2) @le_S_to_le @le_S_to_le @Hi 510 509 ] 511 510 46,47,48,49,50,51,52,53,54: … … 517 516 ] 518 517 1,3,5,7,9,11,13,15,17: 519 @(proj1 ?? (proj1 ?? Hp)i ? Hi2) <Hi @le_S @le_n518 @(proj1 ?? Hp i ? Hi2) <Hi @le_S @le_n 520 519 ] 521 520 ] … … 529 528 ] 530 529 ] 531 [1,3,4: @(proj1 ?? (proj1 ?? Hp)i ? Hi2) @le_S_to_le @le_S_to_le @Hi530 [1,3,4: @(proj1 ?? Hp i ? Hi2) @le_S_to_le @le_S_to_le @Hi 532 531 2,5,6: 533 <Hi @(proj1 ?? (proj1 ?? Hp)(S (prefix)) (le_S ?? (le_n (prefix))) ?)532 <Hi @(proj1 ?? Hp (S (prefix)) (le_S ?? (le_n (prefix))) ?) 534 533 >Hi @Hi2 535 534 ] … … 542 541 9,12: @sym_neq @lt_to_not_eq <Hi @le_n 543 542 ] 544 1,3: @(proj1 ?? (proj1 ?? Hp)i ? Hi2) @le_S_to_le @le_S_to_le @Hi545 5,7: @(proj1 ?? (proj1 ?? Hp)i ? Hi2) <Hi @le_S @le_n543 1,3: @(proj1 ?? Hp i ? Hi2) @le_S_to_le @le_S_to_le @Hi 544 5,7: @(proj1 ?? Hp i ? Hi2) <Hi @le_S @le_n 546 545 ] 547 546 ] 548  cases (le_to_or_lt_eq … Hi) Hi #Hi547 (*  cases (le_to_or_lt_eq … Hi) Hi #Hi 549 548 [ >(nth_append_first ?? prefix ?? (le_S_S_to_le … Hi)) @conj 550 549 [ #Hj cases p p #p cases p #pc #pol #Hp cases x #l #ins cases ins normalize nodelta … … 615 614 ] 616 615 ] 617 @(proj1 ?? (proj2 ?? (proj1 ?? Hp) i (le_S_S_to_le … Hi)) Hj) 616 @(proj1 ?? (proj2 ?? (proj1 ?? Hp) i (le_S_S_to_le … Hi)) Hj) 618 617  #H @(proj2 ?? (proj2 ?? (proj1 ?? (pi2 ?? p)) i (le_S_S_to_le … Hi))) 619 618 cases p in H; p #p cases p #pc #pol #Hp cases x #l #ins cases ins normalize nodelta … … 682 681 / by / 683 682 ] 684 ] 683 ] 685 684  >(injective_S … Hi) >(nth_append_second ?? prefix ?? (le_n (prefix))) 686 685 <minus_n_n whd in match (nth ????); cases x #l #ins cases ins … … 717 716 ] 718 717 ] 719 ] 718 ] *) 720 719  cases daemon 721 720 ] 722 721  @conj 723 [ @conj 724 [#i #_ #Hi2 / by refl/ 725  #i #_ @conj 726 [ >nth_nil #H @⊥ @H 727  #H elim H H #p >lookup_stub #H destruct (H) 728 ] 729 ] 722 [ #i #_ #Hi2 / by refl/ 730 723  whd in match policy_isize_sum; normalize nodelta 731 724 cases daemon … … 738 731 (* \fst p1 = \fst p2 ∧ *) 739 732 (∀n:ℕ.n < program → 740 let pc1 ≝ bvt_lookup … (bitvector_of_nat 16 n) (\snd p1) 〈0, None ?〉 in741 let pc2 ≝ bvt_lookup … (bitvector_of_nat 16 n) (\snd p2) 〈0, None ?〉 in733 let pc1 ≝ bvt_lookup … (bitvector_of_nat 16 n) (\snd p1) 〈0,short_jump〉 in 734 let pc2 ≝ bvt_lookup … (bitvector_of_nat 16 n) (\snd p2) 〈0,short_jump〉 in 742 735 pc1 = pc2). 743 736 … … 756 749 include alias "basics/logic.ma". 757 750 758 759 751 (* One step in the search for a jump expansion fixpoint. *) 760 (* Takes a horrible amount of time to typecheck. I suspect disambiguation problems. *)761 752 definition jump_expansion_step: ∀program:(Σl:list labelled_instruction.l < 2^16). 762 753 ∀labels:(Σlm:label_map. ∀i:ℕ.lt i (program) → … … 765 756 lookup … lm l = Some ? i). 766 757 ∀old_policy:(Σpolicy:ppc_pc_map. 767 And (And (And (out_of_program_none program policy) 768 (jump_in_policy program policy)) 758 And (And (out_of_program_none program policy) 769 759 (policy_isize_sum program labels policy)) 770 760 (\fst policy < 2^16)). … … 773 763 match y with 774 764 [ None ⇒ (* nec_plus_ultra program old_policy *) True 775  Some p ⇒ And (And (And (And (And (And (And (out_of_program_none (pi1 ?? program) p) (* labels_okay labels p ∧*) 776 (jump_in_policy program p)) 765  Some p ⇒ And (And (And (And (And (out_of_program_none (pi1 ?? program) p) (* labels_okay labels p ∧*) 777 766 (policy_isize_sum program labels p)) 778 767 (policy_increase program old_policy p)) 779 (policy_safe program labels p))780 768 (policy_compact program labels p)) 781 769 (no_ch = true → policy_equal program old_policy p)) … … 788 776 (λprefix.Σx:ℕ × ppc_pc_map. 789 777 let 〈added,policy〉 ≝ x in 790 And (And (And (And (And (And (out_of_program_none prefix policy) 791 (jump_in_policy prefix policy)) 778 And (And (And (And (out_of_program_none prefix policy) 792 779 (policy_isize_sum prefix labels policy)) 793 780 (policy_increase prefix old_sigma policy)) 794 (policy_safe prefix labels policy))795 781 (policy_compact prefix labels policy)) 796 782 (added = 0 → policy_equal prefix old_sigma policy)) … … 815 801 ] in 816 802 let 〈inc_pc, inc_sigma〉 ≝ inc_pc_sigma in 817 let 〈old_pc, ol〉 ≝ bvt_lookup … (bitvector_of_nat ? (prefix)) (\snd old_sigma) 〈0,None ?〉 in 818 let old_length ≝ match ol with 819 [ None ⇒ short_jump 820  Some x ⇒ x 821 ] in 803 let 〈old_pc,old_length〉 ≝ bvt_lookup … (bitvector_of_nat ? (prefix)) (\snd old_sigma) 〈0,short_jump〉 in 822 804 let old_size ≝ instruction_size_jmplen old_length instr in 823 805 let 〈new_length, isize〉 ≝ match add_instr with 824 [ None ⇒ 〈 None ?, instruction_size_jmplen short_jump instr〉825  Some pl ⇒ 〈 Some ? (max_length old_length pl), instruction_size_jmplen (max_length old_length pl) instr〉806 [ None ⇒ 〈short_jump, instruction_size_jmplen short_jump instr〉 807  Some pl ⇒ 〈max_length old_length pl, instruction_size_jmplen (max_length old_length pl) instr〉 826 808 ] in 827 809 let new_added ≝ match add_instr with … … 845 827 ] 846 828  lapply (pi2 ?? acc) >p cases inc_pc_sigma #inc_pc #inc_sigma 847 cases (bvt_lookup … (bitvector_of_nat ? (prefix)) (\snd old_sigma) 〈0, None ?〉)829 cases (bvt_lookup … (bitvector_of_nat ? (prefix)) (\snd old_sigma) 〈0,short_jump〉) 848 830 #old_pc #old_length normalize nodelta 849 831 (* XXX complicated proof *) cases daemon 850  normalize nodelta @conj [ @conj [ @conj [ @conj [ @conj [ @conj832  normalize nodelta @conj [ @conj [ @conj [ @conj 851 833 [ #i #Hi / by refl/ 852  #i #Hi @conj [ >nth_nil #H @⊥ @H  #H elim H #x H #H853 normalize in Hi; @⊥ @(absurd ? Hi) @not_le_Sn_O ]854 ]855 834  / by refl/ 856 ]]]] ]857 [ 4: #_]835 ]]]] 836 [3: #_] 858 837 #i #Hi @⊥ @(absurd ? Hi) @not_le_Sn_O 859 838 ] … … 1277 1256 [ None ⇒ True 1278 1257  Some x ⇒ 1279 And (And (And1258 And (And 1280 1259 (out_of_program_none program x) 1281 (jump_in_policy program x))1282 1260 (policy_isize_sum program (create_label_map program) x)) 1283 1261 (\fst x < 2^16) … … 1305 1283  #j #H @conj 1306 1284 [ @conj 1307 [ @conj 1308 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))))) 1309  @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))))) 1310 ] 1311  @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))))) 1285 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))) 1286  @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))) 1312 1287 ] 1313 1288  @(proj2 ?? H) … … 1319 1294 lemma pe_int_refl: ∀program.reflexive ? (policy_equal program). 1320 1295 #program whd #x whd #n #Hn 1321 cases (bvt_lookup … (bitvector_of_nat 16 n) (\snd x) 〈0, None ?〉)1296 cases (bvt_lookup … (bitvector_of_nat 16 n) (\snd x) 〈0,short_jump〉) 1322 1297 #y #z normalize nodelta @refl 1323 1298 qed. … … 1325 1300 lemma pe_int_sym: ∀program.symmetric ? (policy_equal program). 1326 1301 #program whd #x #y #Hxy whd #n #Hn 1327 lapply (Hxy n Hn) cases (bvt_lookup … (bitvector_of_nat ? n) (\snd x) 〈0, None ?〉)1302 lapply (Hxy n Hn) cases (bvt_lookup … (bitvector_of_nat ? n) (\snd x) 〈0,short_jump〉) 1328 1303 #x1 #x2 1329 cases (bvt_lookup … (bitvector_of_nat ? n) (\snd y) 〈0, None ?〉)1304 cases (bvt_lookup … (bitvector_of_nat ? n) (\snd y) 〈0,short_jump〉) 1330 1305 #y1 #y2 normalize nodelta // 1331 1306 qed. … … 1334 1309 #program whd #x #y #z whd in match (policy_equal ???); whd in match (policy_equal ?y ?); 1335 1310 whd in match (policy_equal ? x z); #Hxy #Hyz #n #Hn lapply (Hxy n Hn) Hxy 1336 lapply (Hyz n Hn) Hyz cases (bvt_lookup … (bitvector_of_nat ? n) (\snd x) 〈0, None ?〉)1311 lapply (Hyz n Hn) Hyz cases (bvt_lookup … (bitvector_of_nat ? n) (\snd x) 〈0,short_jump〉) 1337 1312 #x1 #x2 1338 cases (bvt_lookup … (bitvector_of_nat ? n) (\snd y) 〈0, None ?〉) #y1 #y21339 cases (bvt_lookup … (bitvector_of_nat ? n) (\snd z) 〈0, None ?〉) #z1 #z21313 cases (bvt_lookup … (bitvector_of_nat ? n) (\snd y) 〈0,short_jump〉) #y1 #y2 1314 cases (bvt_lookup … (bitvector_of_nat ? n) (\snd z) 〈0,short_jump〉) #z1 #z2 1340 1315 normalize nodelta // 1341 1316 qed. … … 1437 1412 match program with 1438 1413 [ nil ⇒ acc 1439  cons h t ⇒ match (\snd (bvt_lookup ?? (bitvector_of_nat ? (t)) (\snd policy) 〈0,None ?〉)) with 1440 [ None ⇒ measure_int t policy acc 1441  Some j ⇒ match j with 1442 [ long_jump ⇒ measure_int t policy (acc + 2) 1443  medium_jump ⇒ measure_int t policy (acc + 1) 1444  _ ⇒ measure_int t policy acc 1445 ] 1414  cons h t ⇒ match (\snd (bvt_lookup ?? (bitvector_of_nat ? (t)) (\snd policy) 〈0,short_jump〉)) with 1415 [ long_jump ⇒ measure_int t policy (acc + 2) 1416  medium_jump ⇒ measure_int t policy (acc + 1) 1417  _ ⇒ measure_int t policy acc 1446 1418 ] 1447 1419 ]. … … 1454 1426 [ / by refl/ 1455 1427  #h #t #Hd #x whd in match (measure_int ???); whd in match (measure_int ?? x); 1456 cases (\snd (bvt_lookup … (bitvector_of_nat ? (t)) (\snd policy) 〈0, None ?〉))1428 cases (\snd (bvt_lookup … (bitvector_of_nat ? (t)) (\snd policy) 〈0,short_jump〉)) 1457 1429 [ normalize nodelta @Hd 1458  #x cases x 1459 [ normalize nodelta @Hd 1460 2,3: normalize nodelta >associative_plus >(commutative_plus (S d) ?) <associative_plus 1461 @Hd 1462 ] 1430 2,3: normalize nodelta >associative_plus >(commutative_plus (S d) ?) <associative_plus 1431 @Hd 1463 1432 ] 1464 1433 ] … … 1471 1440 [ normalize @le_n 1472 1441  #h #t #Hind whd in match (measure_int ???); 1473 cases (\snd (lookup ?? (bitvector_of_nat ? (t)) (\snd policy) 〈0, None ?〉))1442 cases (\snd (lookup ?? (bitvector_of_nat ? (t)) (\snd policy) 〈0,short_jump〉)) 1474 1443 [ normalize nodelta @(transitive_le ??? Hind) /2 by monotonic_le_times_r/ 1475  #x cases x 1476 [ normalize nodelta @(transitive_le ??? Hind) /2 by monotonic_le_times_r/ 1477 2,3: normalize nodelta >measure_plus <times_n_Sm >(commutative_plus 2 ?) 1478 @le_plus [1,3: @Hind 2,4: / by le_n/ ] 1479 ] 1444 2,3: normalize nodelta >measure_plus <times_n_Sm >(commutative_plus 2 ?) 1445 @le_plus [1,3: @Hind 2,4: / by le_n/ ] 1480 1446 ] 1481 1447 ] … … 1484 1450 lemma measure_incr_or_equal: ∀program:Σl:list labelled_instruction.l<2^16. 1485 1451 ∀policy:Σp:ppc_pc_map. 1486 out_of_program_none program p ∧ jump_in_policy program p ∧1452 out_of_program_none program p ∧ 1487 1453 policy_isize_sum program (create_label_map program) p ∧ \fst p < 2^16. 1488 1454 ∀l.l ≤ program → ∀acc:ℕ. … … 1497 1463 cases (jump_expansion_step ???) in ⊢ (???% → %); #pi1 cases pi1 pi1 #c #r cases r 1498 1464 [ / by I/ 1499  #x normalize nodelta #Hx #Hjeq lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hx)))) (t) Hp)1465  #x normalize nodelta #Hx #Hjeq lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hx))) (t) Hp) 1500 1466 whd in match (measure_int ???); whd in match (measure_int ? x ?); 1501 cases (dec_is_jump (nth (t) ? program 〈None ?, Comment []〉)) 1502 [ #Hj 1503 elim (proj1 ?? (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hx)))))) (t) ?) Hj) 1504 [ #j2 elim (proj1 ?? (proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? policy))) (t) ?) Hj) 1505 [ #j1 normalize nodelta 1506 cases (bvt_lookup ?? (bitvector_of_nat ? (t)) (\snd policy) 〈0,None ?〉) 1507 #x1 #x2 1508 cases (bvt_lookup ?? (bitvector_of_nat ? (t)) (\snd x) 〈0,None ?〉) 1509 #y1 #y2 normalize nodelta #Hx #Hy >Hx >Hy normalize nodelta 1510 #Hblerp cases (proj2 ?? Hblerp) cases j1 cases j2 1511 [1,4,5,7,8,9: #H cases H 1512 2,3,6: #_ normalize nodelta 1513 [1,2: @(transitive_le ? (measure_int t x acc)) 1514 3: @(transitive_le ? (measure_int t x (acc+1))) 1515 ] 1516 [2,4,5,6: >measure_plus [1,2: @le_plus_n_r] >measure_plus @le_plus / by le_n/] 1517 >Hjeq in Hind; #Hind @Hind @(transitive_le … Hp) @le_n_Sn 1518 11,12,13,15,16,17: #H destruct (H) 1519 10,14,18: normalize nodelta #_ >Hjeq in Hind; #Hind @Hind @(transitive_le … Hp) @le_n_Sn 1520 ] 1521  @(transitive_le … Hp) @le_n 1522 ] 1523  @(transitive_le … Hp) @le_n 1524 ] 1525  #Hnj 1526 lapply (proj1 ?? (jump_not_in_policy (pi1 ?? program) (pi1 ?? policy) (t) ?) Hnj) 1527 [3: lapply (proj1 ?? (jump_not_in_policy (pi1 ?? program) x (t) ?) Hnj) 1528 [3: cases (bvt_lookup ?? (bitvector_of_nat ? (t)) (\snd policy) 〈0,None ?〉) 1529 #x1 #x2 cases (bvt_lookup ?? (bitvector_of_nat ? (t)) (\snd x) 〈0,None ?〉) 1530 #y1 #y2 #Hy #Hx >Hx >Hy normalize nodelta 1531 #_ >Hjeq in Hind; #Hind @Hind @(transitive_le … Hp) @le_n_Sn 1532 1: @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hx)))))) 1533 2: @(transitive_le … Hp) @le_n 1534 ] 1535 1: @(proj1 ?? (proj1 ?? (pi2 ?? policy))) 1536 2: @(transitive_le … Hp) @le_n 1537 ] 1538 ] 1539 ] 1467 cases (bvt_lookup ?? (bitvector_of_nat ? (t)) (\snd policy) 〈0,short_jump〉) 1468 #x1 #x2 cases (bvt_lookup ?? (bitvector_of_nat ? (t)) (\snd x) 〈0,short_jump〉) 1469 #y1 #y2 normalize nodelta #Hblerp cases (proj2 ?? Hblerp) cases x2 cases y2 1470 [1,4,5,7,8,9: #H cases H 1471 2,3,6: #_ normalize nodelta 1472 [1,2: @(transitive_le ? (measure_int t x acc)) 1473 3: @(transitive_le ? (measure_int t x (acc+1))) 1474 ] 1475 [2,4,5,6: >measure_plus [1,2: @le_plus_n_r] >measure_plus @le_plus / by le_n/] 1476 >Hjeq in Hind; #Hind @Hind @(transitive_le … Hp) @le_n_Sn 1477 11,12,13,15,16,17: #H destruct (H) 1478 10,14,18: normalize nodelta #_ >Hjeq in Hind; #Hind @Hind @(transitive_le … Hp) @le_n_Sn 1479 ] 1480 ] 1481 ] 1540 1482 qed. 1541 1483 … … 1557 1499 lemma measure_full: ∀program.∀policy. 1558 1500 measure_int program policy 0 = 2*program → ∀i.i<program → 1559 (\snd (bvt_lookup ?? (bitvector_of_nat ? i) (\snd policy) 〈0,None ?〉)) = None ? ∨1560 (\snd (bvt_lookup ?? (bitvector_of_nat ? i) (\snd policy) 〈0, None ?〉)) = Some ?long_jump.1561 #program #policy elim program 1501 is_jump (nth i ? program 〈None ?,Comment []〉) → 1502 (\snd (bvt_lookup ?? (bitvector_of_nat ? i) (\snd policy) 〈0,short_jump〉)) = long_jump. 1503 #program #policy elim program in ⊢ (% → ∀i.% → ? → %); 1562 1504 [ #Hm #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O 1563  #h #t #Hind #Hm #i #Hi cut (measure_int t policy 0 = 2*t)1564 [ whd in match (measure_int ???) in Hm;1565 cases (\snd (bvt_lookup … (bitvector_of_nat ? (t)) (\snd policy) 〈0,None ?〉)) in Hm;1566 normalize nodelta1567 [ #H @⊥ @(absurd ? (measure_le t policy)) >H @lt_to_not_le /2 by lt_plus, le_n/1568  #j cases j normalize nodelta1505  #h #t #Hind #Hm #i #Hi #Hj 1506 cases (le_to_or_lt_eq … Hi) Hi 1507 [ #Hi @Hind 1508 [ whd in match (measure_int ???) in Hm; 1509 cases (\snd (bvt_lookup … (bitvector_of_nat ? (t)) (\snd policy) 〈0,short_jump〉)) in Hm; 1510 normalize nodelta 1569 1511 [ #H @⊥ @(absurd ? (measure_le t policy)) >H @lt_to_not_le /2 by lt_plus, le_n/ 1570 1512  >measure_plus >commutative_plus #H @⊥ @(absurd ? (measure_le t policy)) 1571 <(plus_to_minus … (sym_eq … H)) @lt_to_not_le normalize 1572 >(commutative_plus (t) 0) <plus_O_n <minus_n_O 1573 >plus_n_Sm @le_n 1574  >measure_plus <times_n_Sm >commutative_plus #H lapply (injective_plus_r … H) // 1575 ] 1576 ] 1577  #Hmt cases (le_to_or_lt_eq … Hi) Hi; 1578 [ #Hi @(Hind Hmt i (le_S_S_to_le … Hi)) 1513 <(plus_to_minus … (sym_eq … H)) @lt_to_not_le normalize /2 by le_n/ 1514  >measure_plus <times_n_Sm >commutative_plus /2 by injective_plus_r/ 1515 ] 1516  @(le_S_S_to_le … Hi) 1517  @Hj 1518 ] 1579 1519  #Hi >(injective_S … Hi) whd in match (measure_int ???) in Hm; 1580 cases (\snd (bvt_lookup … (bitvector_of_nat ? (t)) (\snd policy) 〈0, None ?〉)) in Hm;1520 cases (\snd (bvt_lookup … (bitvector_of_nat ? (t)) (\snd policy) 〈0,short_jump〉)) in Hm; 1581 1521 normalize nodelta 1582 [ #_ %1 @refl 1583  #j cases j normalize nodelta 1584 [ >Hmt normalize <plus_n_O >(commutative_plus (t) (S (t))) 1585 >plus_n_Sm #H @⊥ @(absurd ? (bla ?? H)) @sth_not_s 1586  >measure_plus >Hmt normalize <plus_n_O >commutative_plus normalize 1587 #H @⊥ @(absurd ? (injective_plus_r … (injective_S ?? H))) @sth_not_s 1588  #_ %2 @refl 1589 ] 1590 ] 1591 ]] 1522 [ #Hm @⊥ @(absurd ? (measure_le t policy)) >Hm @lt_to_not_le /2 by lt_plus, le_n/ 1523  >measure_plus >commutative_plus #H @⊥ @(absurd ? (measure_le t policy)) 1524 <(plus_to_minus … (sym_eq … H)) @lt_to_not_le normalize /2 by le_n/ 1525  >measure_plus <times_n_Sm >commutative_plus /2 by injective_plus_r/ 1526 ] 1527 ] 1592 1528 ] 1593 1529 qed. … … 1595 1531 lemma measure_special: ∀program:(Σl:list labelled_instruction.l < 2^16). 1596 1532 ∀policy:Σp:ppc_pc_map. 1597 out_of_program_none program p ∧ jump_in_policy program p ∧policy_isize_sum program (create_label_map program) p ∧ \fst p < 2^16.1533 out_of_program_none program p ∧ policy_isize_sum program (create_label_map program) p ∧ \fst p < 2^16. 1598 1534 match (\snd (pi1 ?? (jump_expansion_step program (create_label_map program) policy))) with 1599 1535 [ None ⇒ True … … 1612 1548 [ @(transitive_le … Hp) / by / 1613 1549  whd in match (measure_int ???) in Hm; whd in match (measure_int ? p ?) in Hm; 1614 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol)))) (t) Hp) #Hinc 1615 cases (dec_is_jump (nth (t) ? program 〈None ?, Comment []〉)) 1616 [ #Hj elim (proj1 ?? (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol)))))) (t) ?) Hj) 1617 [ #j2 elim (proj1 ?? (proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? policy))) (t) ?) Hj) 1618 [ #j1 normalize nodelta 1619 cases (bvt_lookup ?? (bitvector_of_nat ? (t)) ? 〈0,None ?〉) in Hm Hinc; #x1 #x2 1620 cases (bvt_lookup ?? (bitvector_of_nat ? (t)) ? 〈0,None ?〉); #y1 #y2 1621 #Hm #Hinc #Hx #Hy lapply Hm Hm; lapply Hinc Hinc; >Hx >Hy normalize nodelta 1622 cases j1 cases j2 normalize nodelta 1623 [1: / by / 1624 2,3: >measure_plus #_ #H @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt 1625 lapply (measure_incr_or_equal program policy t ? 0) 1626 [1,3: @(transitive_le … Hp) @le_n_Sn ] >eqpol / by / 1627 4,7,8: #H elim (proj2 ?? H) #H2 [1,3,5: cases H2 2,4,6: destruct (H2) ] 1628 5: >measure_plus >measure_plus >commutative_plus >(commutative_plus ? 1) 1629 #_ #H @(injective_plus_r … H) 1630 6: >measure_plus >measure_plus 1631 change with (1+1) in match (2); >assoc_plus1 >(commutative_plus 1 (measure_int ???)) 1632 #_ #H @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt @monotonic_le_plus_l 1633 lapply (measure_incr_or_equal program policy t ? 0) 1634 [ @(transitive_le … Hp) @le_n_Sn ] >eqpol / by / 1635 9: >measure_plus >measure_plus >commutative_plus >(commutative_plus ? 2) 1636 #_ #H @(injective_plus_r … H) 1637 ] 1638  @(transitive_le … Hp) @le_n 1639 ] 1640  @(transitive_le … Hp) @le_n 1641 ] 1642  #Hnj lapply (proj1 ?? (jump_not_in_policy (pi1 ?? program) (pi1 ?? policy) (t) ?) Hnj) 1643 [3: lapply (proj1 ?? (jump_not_in_policy (pi1 ?? program) p (t) ?) Hnj) 1644 [3: cases (bvt_lookup ?? (bitvector_of_nat ? (t)) (\snd policy) 〈0,None ?〉) in Hm Hinc; 1645 #x1 #x2 cases (bvt_lookup ?? (bitvector_of_nat ? (t)) (\snd p) 〈0,None ?〉) 1646 #y1 #y2 #Hm #Hinc #Hy #Hx lapply Hm Hm; lapply Hinc Hinc; >Hx >Hy normalize nodelta 1647 #_ / by / 1648 1: @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol)))))) 1649 2: @(transitive_le … Hp) @le_n 1650 ] 1651 1: @(proj1 ?? (proj1 ?? (pi2 ?? policy))) 1652 2: @(transitive_le … Hp) @le_n 1653 ] 1654 ] 1655  @(le_S_S_to_le … Hi) 1550 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol))) (t) Hp) #Hinc 1551 cases (bvt_lookup ?? (bitvector_of_nat ? (t)) ? 〈0,short_jump〉) in Hm Hinc; #x1 #x2 1552 cases (bvt_lookup ?? (bitvector_of_nat ? (t)) ? 〈0,short_jump〉); #y1 #y2 1553 #Hm #Hinc lapply Hm Hm; lapply Hinc Hinc; normalize nodelta 1554 cases x2 cases y2 normalize nodelta 1555 [1: / by / 1556 2,3: >measure_plus #_ #H @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt 1557 lapply (measure_incr_or_equal program policy t ? 0) 1558 [1,3: @(transitive_le … Hp) @le_n_Sn ] >eqpol / by / 1559 4,7,8: #H elim (proj2 ?? H) #H2 [1,3,5: cases H2 2,4,6: destruct (H2) ] 1560 5: >measure_plus >measure_plus >commutative_plus >(commutative_plus ? 1) 1561 #_ #H @(injective_plus_r … H) 1562 6: >measure_plus >measure_plus 1563 change with (1+1) in match (2); >assoc_plus1 >(commutative_plus 1 (measure_int ???)) 1564 #_ #H @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt @monotonic_le_plus_l 1565 lapply (measure_incr_or_equal program policy t ? 0) 1566 [ @(transitive_le … Hp) @le_n_Sn ] >eqpol / by / 1567 9: >measure_plus >measure_plus >commutative_plus >(commutative_plus ? 2) 1568 #_ #H @(injective_plus_r … H) 1569 ] 1570  @(le_S_S_to_le … Hi) 1656 1571 ] 1657 1572  #Hi >(injective_S … Hi) whd in match (measure_int ???) in Hm; 1658 1573 whd in match (measure_int ? p ?) in Hm; 1659 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol)))) (t) Hp)1574 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol))) (t) Hp) 1660 1575 (* XXX *) cases daemon 1661 1576 (* change proof for not_jump … … 1727 1642 And (match p with 1728 1643 [ None ⇒ True 1729  Some pol ⇒ And (And ( And (And (1644  Some pol ⇒ And (And ( 1730 1645 (out_of_program_none program pol)) 1731 (jump_in_policy program pol))1732 1646 (policy_isize_sum program (create_label_map program) pol)) 1733 (policy_safe program (create_label_map program) pol))1734 1647 (policy_compact program (create_label_map program) pol) 1735 1648 ]) … … 1868 1781 ] *) 1869 1782 qed. 1870 *)1871 1783 1872 1784 (* The glue between Policy and Assembly. *) … … 1883 1795 sigma ppc (\fst (fetch_pseudo_instruction (\snd program) ppc))))) 1884 1796 = \fst (sigma (\snd (half_add ? ppc (bitvector_of_nat ? 1))))) 1885 ≝ ?. 1886 (* 1887 λprogram.λppc:ℕ. 1797 ≝ λprogram. 1888 1798 let policy ≝ pi1 … (je_fixpoint (\snd program)) in 1889 1799 match policy with 1890 [ None ⇒ 〈0, Some ? long_jump〉 1891  Some x ⇒ bvt_lookup ?? (bitvector_of_nat 16 ppc) (\snd x) 〈0,Some ? long_jump〉 1892 ].*) 1800 [ None ⇒ None ? 1801  Some x ⇒ Some ? 1802 «λppc.let 〈pc,jl〉 ≝ bvt_lookup ?? ppc (\snd x) 〈0,short_jump〉 in 1803 〈bitvector_of_nat 16 pc,jmpeqb jl long_jump〉,?» 1804 ]. 1893 1805 cases daemon 1894 1806 qed.
Note: See TracChangeset
for help on using the changeset viewer.