Changeset 2101 for src/ASM/Policy.ma
 Timestamp:
 Jun 19, 2012, 4:43:50 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Policy.ma
r2078 r2101 8 8 on n:(Σx:bool × (option ppc_pc_map). 9 9 let 〈no_ch,pol〉 ≝ x in 10 And 11 (match pol with 10 match pol with 12 11 [ None ⇒ True 13 12  Some x ⇒ 14 13 And (And (And (And (And 15 14 (out_of_program_none program x) 16 (jump_not_in_policy program x)) 17 (no_ch = true → policy_compact program (create_label_map program) x)) 15 (not_jump_default program x)) 18 16 (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd x) 〈0,short_jump〉) = 0)) 19 17 (\fst x = \fst (bvt_lookup … (bitvector_of_nat ? (program)) (\snd x) 〈0,short_jump〉))) 20 (\fst x < 2^16) 21 ]) (n = 0 → no_ch = false)) ≝ 22 let labels ≝ create_label_map program in 18 (\fst x < 2^16)) 19 (no_ch = true → sigma_compact program (create_label_map program) x) 20 ]) ≝ 21 let labels ≝ create_label_map program in 23 22 match n return λx.n = x → Σa:bool × (option ppc_pc_map).? with 24 23 [ O ⇒ λp.〈false,pi1 ?? (jump_expansion_start program labels)〉 … … 33 32 [ normalize nodelta cases (jump_expansion_start program (create_label_map program)) 34 33 #x cases x x 35 [ #H @conj/ by I/36  #sigma normalize nodelta #H @conj [ @conj [ @conj [ @conj [ @conj37 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))))38  >p #H destruct (H)34 [ #H / by I/ 35  #sigma normalize nodelta #H @conj [ @conj [ @conj [ @conj 36 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))))) 37  @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))) 39 38 ] 40 39  @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) 41 40 ] 42  cases daemon (* XXX add this to jump_expansion_start *)43 ]44 41  @(proj2 ?? H) 45 42 ] 46  / by /47 ] 48 ] 49  normalize nodelta @conj [ / by I/  >p #H destruct (H) ]43  #H destruct (H) 44 ] 45 ] 46  / by I/ 50 47  cases no_ch in p1; #p1 51 [ normalize nodelta lapply (pi2 ?? (jump_expansion_internal program m)) 52 <p1 >p2 normalize nodelta #H @conj 53 [ @(proj1 ?? H) 54  >p #H2 destruct (H2) 55 ] 48 [ @(pi2 ?? (jump_expansion_internal program m)) 56 49  cases (jump_expansion_step program (create_label_map program) «op,?») 57 50 #x cases x x #ch2 #z2 cases z2 normalize nodelta 58 [ #_ @conj [ / by I/  >p #H2 destruct (H2) ]59  #j2 #H2 @conj [ @conj [ @conj [ @conj [ @conj51 [ #_ / by I/ 52  #j2 #H2 @conj [ @conj [ @conj [ @conj 60 53 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2))))))) 54  @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2))))) 55 ] 56  @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2)))) 57 ] 58  @(proj2 ?? H2) 59 ] 61 60  @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2)))))) 62 ]63  @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2)))))64 ]65  @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2))))66 ]67  @(proj2 ?? H2)68 ]69  >p #H3 destruct (H3)70 61 ] 71 62 ] … … 75 66 [ #_ >p2 #ABS destruct (ABS) 76 67  #map >p2 normalize nodelta 77 #H #eq destruct (eq) @conj [ @conj [ @conj 78 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))) 79  @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) 80 ] 81  @(proj2 ?? (proj1 ?? (proj1 ?? H))) 82 ] 83  @(proj2 ?? (proj1 ?? H)) 84 ] 85 ] 86 ] 87 qed. 88 89 lemma pe_int_refl: ∀program.reflexive ? (policy_jump_equal program). 68 #H #eq destruct (eq) @(proj1 ?? H) 69 ] 70 ] 71 qed. 72 73 lemma pe_int_refl: ∀program.reflexive ? (sigma_jump_equal program). 90 74 #program whd #x whd #n #Hn 91 75 cases (bvt_lookup … (bitvector_of_nat 16 n) (\snd x) 〈0,short_jump〉) … … 93 77 qed. 94 78 95 lemma pe_int_sym: ∀program.symmetric ? ( policy_jump_equal program).79 lemma pe_int_sym: ∀program.symmetric ? (sigma_jump_equal program). 96 80 #program whd #x #y #Hxy whd #n #Hn 97 81 lapply (Hxy n Hn) cases (bvt_lookup … (bitvector_of_nat ? n) (\snd x) 〈0,short_jump〉) … … 101 85 qed. 102 86 103 lemma pe_int_trans: ∀program.transitive ? ( policy_jump_equal program).104 #program whd #x #y #z whd in match ( policy_jump_equal ???); whd in match (policy_jump_equal ?y ?);105 whd in match ( policy_jump_equal ? x z); #Hxy #Hyz #n #Hn lapply (Hxy n Hn) Hxy87 lemma pe_int_trans: ∀program.transitive ? (sigma_jump_equal program). 88 #program whd #x #y #z whd in match (sigma_jump_equal ???); whd in match (sigma_jump_equal ?y ?); 89 whd in match (sigma_jump_equal ? x z); #Hxy #Hyz #n #Hn lapply (Hxy n Hn) Hxy 106 90 lapply (Hyz n Hn) Hyz cases (bvt_lookup … (bitvector_of_nat ? n) (\snd x) 〈0,short_jump〉) 107 91 #x1 #x2 … … 115 99 match p1 with 116 100 [ Some x1 ⇒ match p2 with 117 [ Some x2 ⇒ policy_jump_equal program x1 x2101 [ Some x2 ⇒ sigma_jump_equal program x1 x2 118 102  _ ⇒ False 119 103 ] … … 161 145 #x1 cases x1 #p1 #j1 x1; #H1 #Heqj #Hj #k elim k 162 146 [ <plus_n_O >Heqj @Hj 163  #k' k <plus_n_Sm (*whd in match (jump_expansion_internal program (S (n+k')));*)147  #k' k <plus_n_Sm 164 148 lapply (refl ? (jump_expansion_internal program (n+k'))) 165 149 cases (jump_expansion_internal program (n+k')) in ⊢ (???% → %); … … 209 193  cons h t ⇒ match (\snd (bvt_lookup ?? (bitvector_of_nat ? (t)) (\snd policy) 〈0,short_jump〉)) with 210 194 [ long_jump ⇒ measure_int t policy (acc + 2) 211  medium_jump ⇒ measure_int t policy (acc + 1)195  absolute_jump ⇒ measure_int t policy (acc + 1) 212 196  _ ⇒ measure_int t policy acc 213 197 ] … … 247 231 ∀policy:Σp:ppc_pc_map. 248 232 out_of_program_none program p ∧ 249 jump_not_in_policyprogram p ∧233 not_jump_default program p ∧ 250 234 \fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd p) 〈0,short_jump〉) = 0 ∧ 251 235 \fst p = \fst (bvt_lookup … (bitvector_of_nat ? (program)) (\snd p) 〈0,short_jump〉) ∧ … … 332 316 lemma measure_special: ∀program:(Σl:list labelled_instruction.(S (l)) < 2^16). 333 317 ∀policy:Σp:ppc_pc_map. 334 out_of_program_none program p ∧ jump_not_in_policyprogram p ∧318 out_of_program_none program p ∧ not_jump_default program p ∧ 335 319 \fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd p) 〈0,short_jump〉) = 0 ∧ 336 320 \fst p = \fst (bvt_lookup … (bitvector_of_nat ? (program)) (\snd p) 〈0,short_jump〉) ∧ … … 338 322 match (\snd (pi1 ?? (jump_expansion_step program (create_label_map program) policy))) with 339 323 [ None ⇒ True 340  Some p ⇒ measure_int program policy 0 = measure_int program p 0 → policy_jump_equal program policy p ].324  Some p ⇒ measure_int program policy 0 = measure_int program p 0 → sigma_jump_equal program policy p ]. 341 325 #program #policy lapply (refl ? (pi1 ?? (jump_expansion_step program (create_label_map program) policy))) 342 326 cases (jump_expansion_step program (create_label_map program) policy) in ⊢ (???% → %); … … 346 330 @(list_ind ? (λx.x ≤ pi1 ?? program → 347 331 measure_int x policy 0 = measure_int x p 0 → 348 policy_jump_equal x policy p) ?? (pi1 ?? program))332 sigma_jump_equal x policy p) ?? (pi1 ?? program)) 349 333 [ #_ #_ #i #Hi @⊥ @(absurd ? Hi) @le_to_not_lt @le_O_n 350 334  #h #t #Hind #Hp #Hm #i #Hi cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi … … 432 416 definition je_fixpoint: ∀program:(Σl:list labelled_instruction.S (l) < 2^16). 433 417 Σp:option ppc_pc_map. 434 And (match p with418 match p with 435 419 [ None ⇒ True 436  Some pol ⇒ And (out_of_program_none program pol) 437 (policy_compact program (create_label_map program) pol) 438 ]) 439 (∃n.∀k.n < k → 440 policy_equal_opt program (\snd (pi1 ?? (jump_expansion_internal program k))) p). 441 #program @(\snd (pi1 ?? (jump_expansion_internal program (2*program)))) @conj 442 [ lapply (pi2 ?? (jump_expansion_internal program (2*program))) 443 cases (jump_expansion_internal program (2*program)) #p cases p p 444 #c #pol #Hp cases pol 445 [ normalize nodelta // 446  #x normalize nodelta #H @conj 447 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))))) 448  #Hneq @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))) 449 cases daemon (* XXX add invariant here *) 450 ] 451 ] 452  cases (dec_bounded_exists (λk.policy_equal_opt (pi1 ?? program) 420  Some pol ⇒ And (And (out_of_program_none program pol) 421 (sigma_compact program (create_label_map program) pol)) 422 (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd pol) 〈0,short_jump〉) = 0) 423 ]. 424 #program @(\snd (jump_expansion_internal program (S (2*program)))) 425 cases (dec_bounded_exists (λk.policy_equal_opt (pi1 ?? program) 453 426 (\snd (pi1 ?? (jump_expansion_internal program k))) 454 427 (\snd (pi1 ?? (jump_expansion_internal program (S k))))) ? (2*program)) 455 [ #Hex elim Hex Hex #x #Hx @(ex_intro … x) #k #Hk 456 @pe_trans 457 [ @(\snd (pi1 ?? (jump_expansion_internal program x))) 458  @pe_sym @equal_remains_equal 459 [ @(proj2 ?? Hx) 460  @le_S_S_to_le @le_S @Hk 461 ] 462  @equal_remains_equal 463 [ @(proj2 ?? Hx) 464  @(proj1 ?? Hx) 465 ] 466 ] 467  #Hnex lapply (not_exists_forall … Hnex) Hnex; #Hfa 468 @(ex_intro … (2*program)) #k #Hk @pe_sym @equal_remains_equal 469 [ lapply (refl ? (jump_expansion_internal program (2*program))) 470 cases (jump_expansion_internal program (2*program)) in ⊢ (???% → %); 471 #x cases x x #Fch #Fpol normalize nodelta #HFpol cases Fpol in HFpol; normalize nodelta 472 [ (* if we're at None in 2*program, we're at None in S 2*program too *) 473 #HFpol #EQ whd in match (jump_expansion_internal ??); >EQ 474 normalize nodelta / by / 475  #Fp #HFp #EQ whd in match (jump_expansion_internal ??); 476 >EQ normalize nodelta 477 lapply (refl ? (jump_expansion_step program (create_label_map program) «Fp,?»)) 478 [ @conj [ @conj [ @conj 479 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp))))) 480  @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp)))) 481 ] 482  @(proj2 ?? (proj1 ?? (proj1 ?? HFp))) 483 ] 484  @(proj2 ?? (proj1 ?? HFp)) 485 ] 486  lapply (measure_full program Fp ?) 487 [ @le_to_le_to_eq 488 [ @measure_le 489  cut (∀x:ℕ.x ≤ 2*program → 490 ∃p.(\snd (pi1 ?? (jump_expansion_internal program x)) = Some ? p ∧ 491 x ≤ measure_int program p 0)) 492 [ #x elim x 493 [ #Hx lapply (refl ? (jump_expansion_start program (create_label_map program))) 494 cases (jump_expansion_start program (create_label_map program)) in ⊢ (???% → %); 495 #z cases z z normalize nodelta 496 [ #Waar #Heqn @⊥ elim (le_to_eq_plus ?? Hx) #k #Hk 497 @(absurd … (step_none program 0 ? k)) 498 [ whd in match (jump_expansion_internal ??); >Heqn @refl 499  <Hk >EQ @nmk #H destruct (H) 500 ] 501  #pol #Hpol #Heqpol @(ex_intro ?? pol) @conj 502 [ whd in match (jump_expansion_internal ??); >Heqpol @refl 503  @le_O_n 504 ] 505 ] 506  x #x #Hind #Hx 507 lapply (refl ? (jump_expansion_internal program (S x))) 508 cases (jump_expansion_internal program (S x)) in ⊢ (???% → %); 509 #z cases z z #Sxch #Sxpol cases Sxpol Sxpol normalize nodelta 510 [ #H #HeqSxpol @⊥ elim (le_to_eq_plus ?? Hx) #k #Hk 511 @(absurd … (step_none program (S x) ? k)) 512 [ >HeqSxpol / by / 513  <Hk >EQ @nmk #H destruct (H) 514 ] 515  #Sxpol #HSxpol #HeqSxpol @(ex_intro ?? Sxpol) @conj 516 [ @refl 517  elim (Hind (transitive_le … (le_n_Sn x) Hx)) 518 #xpol #Hxpol @(le_to_lt_to_lt … (proj2 ?? Hxpol)) 519 lapply (measure_incr_or_equal program xpol program (le_n (program)) 0) 520 [ cases (jump_expansion_internal program x) in Hxpol; 521 #z cases z z #xch #xpol normalize nodelta #H #H2 >(proj1 ?? H2) in H; 522 normalize nodelta #H @conj [ @conj [ @conj 523 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))) 524  @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) ] 525  @(proj2 ?? (proj1 ?? (proj1 ?? H))) ] 526  @(proj2 ?? (proj1 ?? H)) ] 527  lapply (Hfa x (le_S_to_le … Hx)) lapply HeqSxpol HeqSxpol 528 lapply (refl ? (jump_expansion_internal program x)) 529 lapply Hxpol Hxpol 530 cases daemon (* this whd takes an enormous amount of time *) 531 (* whd in match (pi1 ?? (jump_expansion_internal program (S x))); 532 cases (jump_expansion_internal program x) in ⊢ (% → ???% → %); 533 #z cases z z #xch #b normalize nodelta #H #Heq >(proj1 ?? Heq) in H; 534 #H #Heq2 cases xch in H Heq2; #H #Heq2 normalize nodelta 535 [ lapply (refl ? (jump_expansion_step program (create_label_map (pi1 ?? program)) «xpol,?»)) 536 [ @conj [ @conj [ @conj 537 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) 538  @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) ] 539  @(proj2 ?? (proj1 ?? (proj1 ?? H))) ] 540  @(proj2 ?? (proj1 ?? H)) ] 541  cases (jump_expansion_step ???) in ⊢ (???% → %); #z cases z z #a #c 542 normalize nodelta cases c normalize nodelta 543 [ #H1 #Heq #H2 destruct (H2) 544  #d #H1 #Heq #H2 destruct (H2) #Hfull #H2 elim (le_to_or_lt_eq … H2) 545 [ / by / 546  #H3 lapply (measure_special program «xpol,?») 547 [ @conj [ @conj 548 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) 549  @(proj2 ?? (proj1 ?? (proj1 ?? H))) ] 550  @(proj2 ?? (proj1 ?? H)) ] 551  >Heq normalize nodelta #H4 @⊥ @(absurd … (H4 H3)) @Hfull 552 ] 553 ] 554 ] 555 ] 556  lapply (refl ? (jump_expansion_step program (create_label_map (pi1 ?? program)) «xpol,?»)) 557 [ @conj [ @conj 558 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) 559  @(proj2 ?? (proj1 ?? (proj1 ?? H))) ] 560  @(proj2 ?? (proj1 ?? H)) ] 561  cases (jump_expansion_step ???) in ⊢ (???% → %); #z cases z z #a #c 562 normalize nodelta cases c normalize nodelta 563 [ #H1 #Heq #H2 #H3 #_ @⊥ @(absurd ?? H3) @pe_refl 564  #d #H1 #Heq #H2 #H3 @⊥ @(absurd ?? H3) @pe_refl 565 ] 566 ] 567 ] *) 568 ] 569 ] 570 ] 571 ] 572  #H elim (H (2*program) (le_n ?)) #plp >EQ #Hplp 573 >(Some_eq ??? (proj1 ?? Hplp)) @(proj2 ?? Hplp) 574 ] 575 ] 576  #Hfull cases (jump_expansion_step program (create_label_map program) «Fp,?») in ⊢ (???% → %); 577 #x cases x x #Gch #Gpol cases Gpol normalize nodelta 578 [ #H #EQ2 @⊥ @(absurd ?? H) @Hfull 579  #Gp #HGp #EQ2 cases Fch 580 [ normalize nodelta /2 by pe_int_refl/ 581  normalize nodelta #i #Hi 582 cases (dec_is_jump (\snd (nth i ? program 〈None ?, Comment []〉))) #Hj 583 [ lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp)))))) i (le_S_to_le … Hi)) 584 lapply (Hfull i Hi Hj) 585 cases (bvt_lookup … (bitvector_of_nat ? i) (\snd Fp) 〈0,short_jump〉) 586 #fp #fj #Hfj >Hfj normalize nodelta 587 cases (bvt_lookup … (bitvector_of_nat ? i) (\snd Gp) 〈0,short_jump〉) 588 #gp #gj cases gj normalize nodelta 589 [1,2: #H cases H #H2 cases H2 destruct (H2) 590 3: #_ @refl 591 ] 592  >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp))))))) i Hi Hj) 593 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp))))) i Hi Hj) @refl 428 [ #Hex cases Hex Hex #k #Hk 429 lapply (refl ? (jump_expansion_internal program (S (2*program)))) 430 cases (jump_expansion_internal ? (S (2*program))) in ⊢ (???% → %); 431 #x cases x x #Gno_ch #Go cases Go normalize nodelta 432 [ #H #Heq / by I/ 433  Go #Gp #HGp #Geq 434 cut (policy_equal_opt program (\snd (jump_expansion_internal program (2*program))) 435 (\snd (jump_expansion_internal program (S (2*program))))) 436 [ @(pe_trans … (equal_remains_equal program k (proj2 ?? Hk) (S (2*program)) (le_S … (le_S_to_le … (proj1 ?? Hk))))) 437 @pe_sym @equal_remains_equal [ @(proj2 ?? Hk)  @(le_S_to_le … (proj1 ?? Hk)) ] 438  >Geq lapply (refl ? (jump_expansion_internal program (2*program))) 439 cases (jump_expansion_internal program (2*program)) in ⊢ (???% → %); 440 #x cases x x #Fno_ch #Fo cases Fo normalize nodelta 441 [ #H #Feq whd in match policy_equal_opt; normalize nodelta #ABS destruct (ABS) 442  Fo #Fp #HFp #Feq whd in match policy_equal_opt; normalize nodelta #Heq 443 @conj [ @conj 444 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp))))) 445  @(proj2 ?? HGp) whd in match (jump_expansion_internal program (S (2*program))) in Geq; (*80s*) 446 >Feq in Geq; cases Fno_ch in HFp Feq; normalize nodelta #HFp #Feq #Geq 447 [ destruct (Geq) / by / 448  cases (jump_expansion_step program (create_label_map (pi1 ?? program)) «Fp,?») in Geq; 449 #x cases x x #Sch #So normalize nodelta cases So 450 [ normalize nodelta #_ #ABS destruct (ABS) 451  So normalize nodelta #Sp #HSp #Seq <(proj1 ?? (pair_destruct ?????? (pi1_eq ???? Seq))) 452 cases Sch in HSp Seq; #HSp #Seq 453 [ @refl 454  normalize nodelta in Seq; @(proj2 ?? (proj1 ?? HSp)) 455 >(Some_eq ??? (proj2 ?? (pair_destruct ?????? (pi1_eq ???? Seq)))) 456 @Heq 594 457 ] 595 458 ] 596 459 ] 597 460 ] 598 ] 599 ] 600  @le_S_S_to_le @le_S @Hk 461  @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp)))) 462 ] 463 ] 464 ] 465 ] 466  #Hnex lapply (not_exists_forall … Hnex) Hnex #Hfa 467 lapply (refl ? (jump_expansion_internal program (2*program))) 468 cases (jump_expansion_internal program (2*program)) in ⊢ (???% → %); 469 #x cases x x #Fno_ch #Fo cases Fo normalize nodelta 470 [ (* None *) 471 #HF #Feq lapply (step_none program (2*program) ? 1) >Feq / by / 472 <plus_n_Sm <plus_n_O #H >H H normalize nodelta / by I/ 473  Fo #Fp #HFp #Feq lapply (measure_full program Fp ?) 474 [ @le_to_le_to_eq 475 [ @measure_le 476  cut (∀x:ℕ.x ≤ 2*program → 477 ∃p.(\snd (pi1 ?? (jump_expansion_internal program x)) = Some ? p ∧ 478 x ≤ measure_int program p 0)) 479 [ #x elim x 480 [ #Hx lapply (refl ? (jump_expansion_start program (create_label_map program))) 481 cases (jump_expansion_start program (create_label_map program)) in ⊢ (???% → %); 482 #z cases z z normalize nodelta 483 [ #H #Heqn @⊥ elim (le_to_eq_plus ?? Hx) #n #Hn 484 @(absurd … (step_none program 0 ? n)) 485 [ whd in match (jump_expansion_internal ??); >Heqn @refl 486  <Hn >Feq @nmk #H destruct (H) 487 ] 488  #Zp #HZp #Zeq @(ex_intro ?? Zp) @conj 489 [ whd in match (jump_expansion_internal ??); >Zeq @refl 490  @le_O_n 491 ] 492 ] 493  x #x #Hind #Hx 494 lapply (refl ? (jump_expansion_internal program (S x))) 495 cases (jump_expansion_internal program (S x)) in ⊢ (???% → %); 496 #z cases z z #Sno_ch #So cases So So 497 [ #HSp #Seq normalize nodelta @⊥ elim (le_to_eq_plus ?? Hx) #k #Hk 498 @(absurd … (step_none program (S x) ? k)) 499 [ >Seq @refl 500  <Hk >Feq @nmk #H destruct (H) 501 ] 502  #Sp #HSp #Seq @(ex_intro ?? Sp) @conj 503 [ @refl 504  elim (Hind (transitive_le … (le_n_Sn x) Hx)) 505 #pol #Hpol @(le_to_lt_to_lt … (proj2 ?? Hpol)) 506 lapply (proj1 ?? Hpol) Hpol 507 lapply (refl ? (jump_expansion_internal program x)) 508 cases (jump_expansion_internal program x) in ⊢ (???% → %); 509 #z cases z z #Xno_ch #Xo cases Xo 510 [ #HXp #Xeq #abs destruct (abs) 511  normalize nodelta #Xp #HXp #Xeq #H <(Some_eq ??? H) H pol 512 lapply (Hfa x Hx) >Xeq >Seq whd in match policy_equal_opt; 513 normalize nodelta #Hpe 514 lapply (measure_incr_or_equal program Xp program (le_n (program)) 0) 515 [ @(proj1 ?? HXp) 516  lapply (Hfa x Hx) >Xeq >Seq 517 lapply (measure_special program «Xp,?») 518 [ @(proj1 ?? HXp) 519  lapply Seq whd in match (jump_expansion_internal program (S x)); (*340s*) 520 >Xeq normalize nodelta cases Xno_ch in HXp Xeq; #HXp #Xeq 521 [ normalize nodelta #EQ 522 >(proj2 ?? (pair_destruct ?????? (pi1_eq ???? EQ))) 523 #_ #abs @⊥ @(absurd ?? abs) / by / 524  normalize nodelta cases (jump_expansion_step ???); 525 #z cases z z #stch #sto cases sto 526 [ normalize nodelta #_ #ABS destruct (ABS) 527  sto #stp normalize nodelta #Hstp #steq 528 >(Some_eq ??? (proj2 ?? (pair_destruct ?????? (pi1_eq ???? steq)))) 529 #Hms #Hneq #glerp elim (le_to_or_lt_eq … glerp) 530 [ / by / 531  #glorp @⊥ @(absurd ?? Hneq) @Hms @glorp 532 ] 533 ] 534 ] 535 ] 536 ] 537 ] 538 ] 539 ] 540 ] 541  #H elim (H (2*program) (le_n ?)) #plp >Feq #Hplp 542 >(Some_eq ??? (proj1 ?? Hplp)) @(proj2 ?? Hplp) 543 ] 544 ] 545  #Hfull 546 whd in match (jump_expansion_internal program (S (2*program))); (*65s*) 547 >Feq normalize nodelta cases Fno_ch in HFp Feq; #HFp #Feq 548 normalize nodelta 549 [ @conj [ @conj 550 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp))))) 551  @((proj2 ?? HFp) (refl ? true)) ] 552  @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp)))) 553 ] 554  cases (jump_expansion_step ???); #z cases z z #stch #sto cases sto 555 [ #_ / by I/ 556  sto #stp normalize nodelta #Hstp @conj [ @conj 557 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hstp)))))))) 558  @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hstp)))))) 559 @(proj2 ?? (proj1 ?? Hstp)) #i #Hi 560 cases (dec_is_jump (\snd (nth i ? program 〈None ?, Comment []〉))) 561 [ #Hj 562 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hstp)))))) i (le_S_to_le … Hi)) 563 lapply (Hfull i Hi Hj) 564 cases (bvt_lookup … (bitvector_of_nat ? i) (\snd Fp) 〈0,short_jump〉) 565 #fp #fj #Hfj >Hfj normalize nodelta 566 cases (bvt_lookup … (bitvector_of_nat ? i) (\snd stp) 〈0,short_jump〉) 567 #stp #stj cases stj normalize nodelta 568 [1,2: #H cases H #H2 cases H2 destruct (H2) 569 3: #_ @refl 570 ] 571  #Hj >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hstp))))))) i Hi Hj) 572 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp)))) i Hi Hj) @refl 573 ] 574 ] 575  @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hstp))))) ] 576 ] 577 ] 578 ] 601 579 ] 602 580  #n cases (jump_expansion_internal program n) cases (jump_expansion_internal program (S n)) … … 607 585 2,3: #x #Hnpol #HSpol %2 @nmk whd in match (policy_equal_opt ???); // 608 586 #H destruct (H) 609 4: #np #Hnp #Sp #HSp whd in match (policy_equal_opt ???); cases program #p #_ cases p 610 [ %1 #m #Hm @⊥ @(absurd ? Hm) @le_to_not_lt @le_O_n 611  #h #t elim (dec_bounded_forall ?? (t)) 612 [1: #Hyp %1 #m #Hm @(Hyp m) @(le_S_S_to_le … Hm) 613 2: #Hyp %2 @nmk #H @(absurd ?? Hyp) #m #Hm @(H m) @(le_S_S … Hm) 614  #m cases (bvt_lookup ?? (bitvector_of_nat 16 m) ? 〈0,short_jump〉) 615 #x1 #x2 616 cases (bvt_lookup ?? (bitvector_of_nat ? m) ? 〈0,short_jump〉) 617 #y1 #y2 normalize nodelta 618 @dec_eq_jump_length 619 ] 620 621 ] 622 ] 623 ] 587 4: #np #Hnp #Sp #HSp whd in match (policy_equal_opt ???); @dec_bounded_forall #m 588 cases (bvt_lookup ?? (bitvector_of_nat 16 m) ? 〈0,short_jump〉) 589 #x1 #x2 590 cases (bvt_lookup ?? (bitvector_of_nat ? m) ? 〈0,short_jump〉) 591 #y1 #y2 normalize nodelta 592 @dec_eq_jump_length 593 ] 594 ] 624 595 qed. 625 596 … … 627 598 include alias "basics/logic.ma". 628 599 600 lemma nth_safe_nth: 601 ∀A:Type[0].∀l:list A.∀i.∀proof:i < l.∀x.nth_safe A i l proof = nth i A l x. 602 #A #l elim l 603 [ #i #prf @⊥ @(absurd ? prf) @le_to_not_lt @le_O_n 604  l #h #t #Hind #i elim i 605 [ #prf #x normalize @refl 606  i #i #Hind2 #prf #x whd in match (nth ????); whd in match (tail ??); 607 whd in match (nth_safe ????); @Hind 608 ] 609 ] 610 qed. 611 629 612 (* The glue between Policy and Assembly. *) 630 (*CSC: modified to really use the specification in Assembly.ma. 631 I have modified all that follows in vi without testing it in Matita. 632 Jaap, please repair it *) 613 (*CSC: modified to really use the specification in Assembly.ma.*) 633 614 definition jump_expansion': 634 615 ∀program:preamble × (Σl:list labelled_instruction.S (l) < 2^16). 635 616 option (Σsigma_policy:(Word → Word) × (Word → bool). 636 617 let 〈sigma,policy〉≝ sigma_policy in 637 sigma_policy_specification program sigma policy638 ≝618 sigma_policy_specification 〈\fst program,\snd program〉 sigma policy) 619 ≝ 639 620 λprogram. 640 let policy ≝ pi1 … (je_fixpoint (\snd program)) in641 match policywith642 [ None ⇒ None ?643  Some x ⇒ Some ?621 let f: option ppc_pc_map ≝ je_fixpoint (\snd program) in 622 match f return λx.f = x → ? with 623 [ None ⇒ λp.None ? 624  Some x ⇒ λp.Some ? 644 625 «〈(λppc.let 〈pc,jl〉 ≝ bvt_lookup ?? ppc (\snd x) 〈0,short_jump〉 in 645 626 bitvector_of_nat 16 pc), 646 627 (λppc.let 〈pc,jl〉 ≝ bvt_lookup ?? ppc (\snd x) 〈0,short_jump〉 in 647 628 jmpeqb jl long_jump)〉,?» 648 ]. 649 #ppc normalize nodelta cases daemon 650 qed. 629 ] (refl ? f). 630 normalize nodelta in p; whd in match sigma_policy_specification; normalize nodelta 631 lapply (pi2 ?? (je_fixpoint (\snd program))) >p normalize nodelta cases x 632 #fpc #fpol #Hfpol 633 @conj 634 [ lapply (proj2 ?? Hfpol) cases (bvt_lookup ??? fpol 〈0,short_jump〉) 635 #x #y #Hx normalize nodelta >Hx / by refl/ 636  #ppc #ppc_ok @conj 637 [ #Hppc lapply (proj2 ?? (proj1 ?? Hfpol) (nat_of_bitvector 16 ppc) ppc_ok) 638 >bitvector_of_nat_inverse_nat_of_bitvector 639 lapply (refl ? (lookup_opt … ppc fpol)) cases (lookup_opt … ppc fpol) in ⊢ (???% → %); 640 [ normalize nodelta #_ #abs cases abs 641  #x cases x x #x1 #y1 normalize nodelta #Hl_ppc 642 >(plus_n_O (nat_of_bitvector 16 ppc)) >plus_n_Sm <add_bitvector_of_nat_plus 643 >bitvector_of_nat_inverse_nat_of_bitvector 644 lapply (refl ? (lookup_opt … (add 16 ppc (bitvector_of_nat 16 1)) fpol)) 645 cases (lookup_opt … (add 16 ppc (bitvector_of_nat 16 1)) fpol) in ⊢ (???% → %); 646 [ normalize nodelta #_ #abs cases abs 647  #x cases x x #x2 #y2 normalize nodelta #Hl_Sppc 648 #Hcompact >(lookup_opt_lookup_hit … Hl_Sppc 〈0,short_jump〉) 649 >(lookup_opt_lookup_hit … Hl_ppc 〈0,short_jump〉) normalize nodelta 650 >add_bitvector_of_nat_plus whd in match (fetch_pseudo_instruction ???); 651 >(nth_safe_nth … 〈None ?, Comment []〉) 652 >Hcompact <plus_n_O 653 cases (nth (nat_of_bitvector ? ppc) ? (\snd program) ?) #a #b normalize nodelta 654 whd in match instruction_size; normalize nodelta 655 whd in match assembly_1_pseudoinstruction; normalize nodelta 656 whd in match expand_pseudo_instruction; normalize nodelta 657 cases b 658 [2,3,6: #p [3: #q] normalize nodelta @refl 659 4,5: #p normalize nodelta 660 >(lookup_opt_lookup_hit … Hl_Sppc 〈0,short_jump〉) normalize nodelta 661 >(lookup_opt_lookup_hit … Hl_ppc 〈0,short_jump〉) normalize nodelta 662 whd in match (create_label_map ?); 663 cases (lookup ?? (bitvector_of_nat ? 664 (lookup_def ?? (\fst (create_label_cost_map (\snd program))) p 0)) fpol 〈0,short_jump〉) 665 #z1 #z2 normalize nodelta @refl 666 1: #pi cases pi 667 [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: 668 [1,2,3,6,7,24,25: #p #q 669 4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #p] 670 normalize nodelta @refl 671 9,10,11,12,13,14,15,16,17: [1,2,6,7: #p 3,4,5,8,9: #q #p] normalize nodelta 672 whd in match expand_relative_jump; normalize nodelta 673 whd in match expand_relative_jump_internal; normalize nodelta 674 >(lookup_opt_lookup_hit … Hl_Sppc 〈0,short_jump〉) normalize nodelta 675 >(lookup_opt_lookup_hit … Hl_ppc 〈0,short_jump〉) normalize nodelta 676 whd in match (create_label_map ?); 677 cases (lookup ?? (bitvector_of_nat ? 678 (lookup_def ?? (\fst (create_label_cost_map (\snd program))) p 0)) fpol 〈0,short_jump〉) 679 #z1 #z2 normalize nodelta @refl 680 ] 681 ] 682 ] 683 ] 684  cases daemon (* XXX remains to be done *) 685 ] 686 ] 687 qed. 688 689 690 691 692 >(add_bitvector_of_nat_plus ?? ppc) 693 694 qed.
Note: See TracChangeset
for help on using the changeset viewer.