Changeset 2101
 Timestamp:
 Jun 19, 2012, 4:43:50 PM (7 years ago)
 Location:
 src
 Files:

 5 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Assembly.ma
r2081 r2101 12 12 inductive jump_length: Type[0] ≝ 13 13  short_jump: jump_length 14  medium_jump: jump_length14  absolute_jump: jump_length 15 15  long_jump: jump_length. 16 16 … … 26 26 〈eq_bv 9 upper (zero …), false:::lower〉. 27 27 28 definition medium_jump_cond: Word → Word → (*pseudo_instruction →*)28 definition absolute_jump_cond: Word → Word → (*pseudo_instruction →*) 29 29 bool × (BitVector 11) ≝ 30 30 λpc_plus_jmp_length.λaddr.(*λinstr.*) … … 528 528 let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in 529 529 let lookup_address ≝ sigma (lookup_labels call) in 530 let 〈mj_possible, disp〉 ≝ medium_jump_cond pc_plus_jmp_length lookup_address in530 let 〈mj_possible, disp〉 ≝ absolute_jump_cond pc_plus_jmp_length lookup_address in 531 531 let do_a_long ≝ policy ppc in 532 532 if mj_possible ∧ ¬ do_a_long then … … 549 549 [ SJMP address ] 550 550 else 551 let 〈mj_possible, disp2〉 ≝ medium_jump_cond pc_plus_jmp_length lookup_address in551 let 〈mj_possible, disp2〉 ≝ absolute_jump_cond pc_plus_jmp_length lookup_address in 552 552 if mj_possible ∧ ¬ do_a_long then 553 553 let address ≝ ADDR11 disp2 in 
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. 
src/ASM/PolicyFront.ma
r2059 r2101 13 13 (* The different properties that we want/need to prove at some point *) 14 14 (* During our iteration, everything not yet seen is None, and vice versa *) 15 definition out_of_program_none : list labelled_instruction → ppc_pc_map → Prop ≝16 λprefix .λsigma.17 ∀i :ℕ.i < 2^16 → (i > prefix ↔ bvt_lookup_opt … (bitvector_of_nat 16i) (\snd sigma) = None ?).15 definition out_of_program_none ≝ 16 λprefix:list labelled_instruction.λsigma:ppc_pc_map. 17 ∀i.i < 2^16 → (i > prefix ↔ bvt_lookup_opt … (bitvector_of_nat ? i) (\snd sigma) = None ?). 18 18 19 19 (* If instruction i is a jump, then there will be something in the policy at … … 77 77 ]. 78 78 79 definition jump_not_in_policy: list labelled_instruction → ppc_pc_map → Prop ≝80 λprefix .λsigma.79 definition not_jump_default ≝ 80 λprefix:list labelled_instruction.λsigma:ppc_pc_map. 81 81 ∀i:ℕ.i < prefix → 82 82 ¬is_jump (\snd (nth i ? prefix 〈None ?, Comment []〉)) → 83 \snd (bvt_lookup … (bitvector_of_nat 16 i) (\snd sigma) 〈0,short_jump〉) = short_jump. 84 85 (* if the instruction 〈p,a〉 is a jump to label l, then label l is at address a *) 86 (* definition labels_okay: label_map → ppc_pc_map → Prop ≝ 87 λlabels.λsigma. 88 bvt_forall ?? (\snd sigma) (λn.λx. 89 let 〈pc,addr_nat〉 ≝ x in 90 ∃id:Identifier.lookup_def … labels id 0 = addr_nat 91 ). *) 92 83 \snd (bvt_lookup … (bitvector_of_nat ? i) (\snd sigma) 〈0,short_jump〉) = short_jump. 84 93 85 (* Between two policies, jumps cannot decrease *) 94 86 definition jmpeqb: jump_length → jump_length → bool ≝ … … 96 88 match j1 with 97 89 [ short_jump ⇒ match j2 with [ short_jump ⇒ true  _ ⇒ false ] 98  medium_jump ⇒ match j2 with [ medium_jump ⇒ true  _ ⇒ false ]90  absolute_jump ⇒ match j2 with [ absolute_jump ⇒ true  _ ⇒ false ] 99 91  long_jump ⇒ match j2 with [ long_jump ⇒ true  _ ⇒ false ] 100 92 ]. … … 114 106  _ ⇒ True 115 107 ] 116  medium_jump ⇒108  absolute_jump ⇒ 117 109 match j2 with 118 110 [ long_jump ⇒ True … … 125 117 λj1.λj2.jmple j1 j2 ∨ j1 = j2. 126 118 127 definition policy_increase: list labelled_instruction → ppc_pc_map → 128 ppc_pc_map → Prop ≝ 129 λprogram.λop.λp. 130 ∀i.i ≤ program → 131 let 〈opc,oj〉 ≝ bvt_lookup … (bitvector_of_nat 16 i) (\snd op) 〈0,short_jump〉 in 132 let 〈pc,j〉 ≝ bvt_lookup … (bitvector_of_nat 16 i) (\snd p) 〈0,short_jump〉 in 119 definition jump_increase ≝ 120 λprefix:list labelled_instruction.λop:ppc_pc_map.λp:ppc_pc_map. 121 ∀i.i ≤ prefix → 122 let 〈opc,oj〉 ≝ bvt_lookup … (bitvector_of_nat ? i) (\snd op) 〈0,short_jump〉 in 123 let 〈pc,j〉 ≝ bvt_lookup … (bitvector_of_nat ? i) (\snd p) 〈0,short_jump〉 in 133 124 (*opc ≤ pc ∧*) jmpleq oj j. 134 125 … … 139 130 match jmp_len with 140 131 [ short_jump ⇒ [ RealInstruction (i (RELATIVE (zero 8))) ] 141  medium_jump ⇒ [ ] (* this should not happen *)132  absolute_jump ⇒ [ ] (* this should not happen *) 142 133  long_jump ⇒ 143 134 [ RealInstruction (i (RELATIVE (bitvector_of_nat ? 2))); … … 202 193 match jmp_len with 203 194 [ short_jump ⇒ [ ] (* this should not happen *) 204  medium_jump ⇒ [ ACALL (ADDR11 (zero 11)) ]195  absolute_jump ⇒ [ ACALL (ADDR11 (zero 11)) ] 205 196  long_jump ⇒ [ LCALL (ADDR16 (zero 16)) ] 206 197 ] … … 211 202 match jmp_len with 212 203 [ short_jump ⇒ [ SJMP (RELATIVE (zero 8)) ] 213  medium_jump ⇒ [ AJMP (ADDR11 (zero 11)) ]204  absolute_jump ⇒ [ AJMP (ADDR11 (zero 11)) ] 214 205  long_jump ⇒ [ LJMP (ADDR16 (zero 16)) ] 215 206 ] … … 222 213 qed. 223 214 224 definition policy_compact_unsafe: list labelled_instruction → label_map → ppc_pc_map → Prop ≝225 λpr ogram.λlabels.λsigma.226 ∀n :ℕ.n < program →215 definition sigma_compact_unsafe ≝ 216 λprefix:list labelled_instruction.λlabels:label_map.λsigma:ppc_pc_map. 217 ∀n.n < prefix → 227 218 match bvt_lookup_opt … (bitvector_of_nat ? n) (\snd sigma) with 228 219 [ None ⇒ False … … 231 222 [ None ⇒ False 232 223  Some x1 ⇒ let 〈pc1,j1〉 ≝ x1 in 233 pc1 = pc + instruction_size_jmplen j (\snd (nth n ? pr ogram〈None ?, Comment []〉))224 pc1 = pc + instruction_size_jmplen j (\snd (nth n ? prefix 〈None ?, Comment []〉)) 234 225 ] 235 226 ]. 236 227 237 (* new safety condition: policycorresponds to program and resulting program is compact *)238 definition policy_compact: list labelled_instruction → label_map → ppc_pc_map → Prop≝239 λprogram .λlabels.λsigma.240 ∀n :ℕ.n < program →228 (* new safety condition: sigma corresponds to program and resulting program is compact *) 229 definition sigma_compact ≝ 230 λprogram:list labelled_instruction.λlabels:label_map.λsigma:ppc_pc_map. 231 ∀n.n < program → 241 232 match bvt_lookup_opt … (bitvector_of_nat ? n) (\snd sigma) with 242 233 [ None ⇒ False … … 251 242 ] 252 243 ]. 244 245 (* jumps are of the proper size *) 246 definition sigma_safe ≝ 247 λprefix:list labelled_instruction.λlabels:label_map.λadded:ℕ. 248 λold_sigma:ppc_pc_map.λsigma:ppc_pc_map. 249 ∀i.i < prefix → 250 let 〈pc,j〉 ≝ bvt_lookup … (bitvector_of_nat ? i) (\snd sigma) 〈0,short_jump〉 in 251 let pc_plus_jmp_length ≝ bitvector_of_nat ? (\fst (bvt_lookup … (bitvector_of_nat ? (S i)) (\snd sigma) 〈0,short_jump〉)) in 252 let 〈label,instr〉 ≝ nth i ? prefix 〈None ?, Comment [ ]〉 in 253 ∀dest.is_jump_to instr dest → 254 let paddr ≝ lookup_def … labels dest 0 in 255 let addr ≝ bitvector_of_nat ? (if leb i paddr (* forward jump *) 256 then \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd old_sigma) 〈0,short_jump〉) + added 257 else \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd sigma) 〈0,short_jump〉)) in 258 match j with 259 [ short_jump ⇒ \fst (short_jump_cond pc_plus_jmp_length addr) = true ∧ 260 ¬is_call instr 261  absolute_jump ⇒ \fst (absolute_jump_cond pc_plus_jmp_length addr) = true ∧ 262 \fst (short_jump_cond pc_plus_jmp_length addr) = false ∧ 263 ¬is_relative_jump instr 264  long_jump ⇒ \fst (short_jump_cond pc_plus_jmp_length addr) = false ∧ 265 \fst (absolute_jump_cond pc_plus_jmp_length addr) = false 266 ]. 267 253 268 254 269 (* Definitions and theorems for the jump_length type (itself defined in Assembly) *) … … 257 272 match j1 with 258 273 [ long_jump ⇒ long_jump 259  medium_jump ⇒274  absolute_jump ⇒ 260 275 match j2 with 261 [ medium_jump ⇒ medium_jump276 [ absolute_jump ⇒ absolute_jump 262 277  _ ⇒ long_jump 263 278 ] … … 283 298 %2 @nmk #H destruct (H) 284 299 qed. 285 286 (* definition policy_isize_sum ≝287 λprefix:list labelled_instruction.λlabels:label_map.λsigma:ppc_pc_map.288 (\fst sigma) = foldl_strong (option Identifier × pseudo_instruction)289 (λacc.ℕ)290 prefix291 (λhd.λx.λtl.λp.λacc.292 acc + (instruction_size (λid.bitvector_of_nat ? (lookup_def ?? labels id 0))293 (λppc.bitvector_of_nat ? (\fst (bvt_lookup ?? ppc (\snd sigma) 〈0,short_jump〉)))294 (λppc.jmpeqb long_jump (\snd (bvt_lookup ?? ppc (\snd sigma) 〈0,short_jump〉)))295 (bitvector_of_nat 16 (\fst sigma)) (\snd x)))296 0. *)297 300 298 301 (* The function that creates the labeltoaddress map *) … … 340 343 + added 341 344 else \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd inc_sigma) 〈0,short_jump〉)) in 342 let 〈 mj_possible, disp〉 ≝ medium_jump_cond pc_plus_jmp_length addr in343 if mj_possible344 then medium_jump345 let 〈aj_possible, disp〉 ≝ absolute_jump_cond pc_plus_jmp_length addr in 346 if aj_possible 347 then absolute_jump 345 348 else long_jump. 346 349 … … 411 414 match policy with 412 415 [ None ⇒ True 413  Some p ⇒ 414 And (And (And (And (And (And(out_of_program_none (pi1 ?? program) p)415 ( jump_not_in_policy(pi1 ?? program) p))416 ( policy_compact_unsafe program labels p))416  Some p ⇒ And (And (And (And (And (And (And 417 (out_of_program_none (pi1 ?? program) p) 418 (not_jump_default (pi1 ?? program) p)) 419 (sigma_compact_unsafe program labels p)) 417 420 (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd p) 〈0,short_jump〉) = 0)) 421 (\fst p = \fst (bvt_lookup … (bitvector_of_nat ? (program)) (\snd p) 〈0,short_jump〉))) 418 422 (∀i.i ≤ program → ∃pc. 419 423 bvt_lookup_opt … (bitvector_of_nat ? i) (\snd p) = Some ? 〈pc,short_jump〉)) 420 (bvt_lookup_opt … (bitvector_of_nat ? (program)) (\snd p) = 421 Some ? 〈\fst p,short_jump〉)) 424 (bvt_lookup_opt … (bitvector_of_nat ? (program)) (\snd p) = Some ? 〈\fst p,short_jump〉)) 422 425 (\fst p < 2^16) 423 426 ] ≝ 424 427 λprogram.λlabels. 425 428 let final_policy ≝ foldl_strong (option Identifier × pseudo_instruction) 426 (λprefix.Σpolicy:ppc_pc_map. 427 And (And (And (And (And(out_of_program_none prefix policy)428 ( jump_not_in_policyprefix policy))429 ( policy_compact_unsafe prefix labels policy))429 (λprefix.Σpolicy:ppc_pc_map.And (And (And (And (And (And 430 (out_of_program_none prefix policy) 431 (not_jump_default prefix policy)) 432 (sigma_compact_unsafe prefix labels policy)) 430 433 (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd policy) 〈0,short_jump〉) = 0)) 434 (\fst policy = \fst (bvt_lookup … (bitvector_of_nat ? (prefix)) (\snd policy) 〈0,short_jump〉))) 431 435 (∀i.i ≤ prefix → ∃pc. 432 436 bvt_lookup_opt … (bitvector_of_nat ? i) (\snd policy) = Some ? 〈pc,short_jump〉)) … … 447 451  lapply p p generalize in match (foldl_strong ?????); * #p #Hp #hg 448 452 @conj [ @Hp  @not_le_to_lt @leb_false_to_not_le <geb_to_leb @hg ] 449  @conj [ @conj [ @conj [ @conj [ @conj 453  @conj [ @conj [ @conj [ @conj [ @conj [ @conj 450 454 [ (* out_of_program_none *) 451 455 #i #Hi2 >append_length <commutative_plus @conj … … 453 457 cases p p #p cases p p #pc #p #Hp cases x x #l #pi 454 458 [ >lookup_opt_insert_miss 455 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))) i Hi2))459 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp))))) i Hi2)) 456 460 @le_S_to_le @le_S_to_le @Hi 457 461  @bitvector_of_nat_abs … … 463 467  >lookup_opt_insert_miss 464 468 [ <Hi 465 @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))) (S (S (prefix))) ?))469 @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp))))) (S (S (prefix))) ?)) 466 470 [ >Hi @Hi2 467 471  @le_S @le_n … … 479 483  #Hi >lookup_opt_insert_miss 480 484 [ #Hl 481 elim (le_to_or_lt_eq … (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))) i Hi2) Hl))485 elim (le_to_or_lt_eq … (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp))))) i Hi2) Hl)) 482 486 [ #Hi3 @Hi3 483 487  #Hi3 @⊥ @(absurd ? Hi3) @sym_neq @Hi … … 492 496 ] 493 497 ] 494  (* jump_not_in_policy*) cases p p #p cases p p #pc #sigma #Hp498  (* not_jump_default *) cases p p #p cases p p #pc #sigma #Hp 495 499 cases x in prf; #lbl #ins #prf #i >append_length <commutative_plus #Hi 496 500 normalize in Hi; normalize nodelta cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi 497 501 [ >lookup_insert_miss 498 [ lapply ((proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp))))) i Hi)502 [ lapply ((proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))))) i Hi) 499 503 >nth_append_first 500 504 [ #H #H2 @H @H2 … … 526 530 [ >lookup_opt_insert_miss 527 531 [ >lookup_opt_insert_miss 528 [ lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp))) i Hi)532 [ lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))) i Hi) 529 533 lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? i) sigma)) 530 534 cases (bvt_lookup_opt … (bitvector_of_nat ? i) sigma) in ⊢ (???% → %); … … 566 570 ] 567 571 ] 568  (* lookup 0 =0 *)572  (* 0 ↦ 0 *) 569 573 cases p p #p cases p p #pc #sigma #Hp cases x #lbl #instr normalize nodelta 570 574 >lookup_insert_miss 571 [ @(proj2 ?? (proj1 ?? (proj1 ?? Hp)))575 [ @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))) 572 576  @bitvector_of_nat_abs 573 577 [ / by / … … 577 581 ] 578 582 ] 583 ] 584  (* fst p = pc *) 585 cases p p #p cases p p #pc #sigma #Hp cases x #lbl #instr normalize nodelta 586 >append_length >(commutative_plus (prefix)) >lookup_insert_hit @refl 579 587 ] 580 588  (* lookup = short_jump *) #i >append_length <commutative_plus #Hi normalize in Hi; … … 599 607 / by refl/ 600 608 ] 601  @conj [ @conj [ @conj [ @conj [ @conj 609  @conj [ @conj [ @conj [ @conj [ @conj [ @conj 602 610 [ #i cases i 603 611 [ #Hi2 @conj … … 629 637  >lookup_insert_hit @refl 630 638 ] 639  >lookup_insert_hit @refl 640 ] 631 641  #i cases i 632 642 [ #Hi >lookup_opt_insert_hit @(ex_intro ?? 0) @refl … … 643 653 * if we have not added anything to the pc, we only know the PC hasn't changed, 644 654 * there might still have been a short/medium jump change *) 645 definition policy_pc_equal ≝655 definition sigma_pc_equal ≝ 646 656 λprogram:list labelled_instruction.λp1,p2:ppc_pc_map. 647 (∀n :ℕ.n ≤ program →657 (∀n.n ≤ program → 648 658 \fst (bvt_lookup … (bitvector_of_nat 16 n) (\snd p1) 〈0,short_jump〉) = 649 659 \fst (bvt_lookup … (bitvector_of_nat 16 n) (\snd p2) 〈0,short_jump〉)). 650 660 651 definition policy_jump_equal ≝661 definition sigma_jump_equal ≝ 652 662 λprogram:list labelled_instruction.λp1,p2:ppc_pc_map. 653 (∀n :ℕ.n < program →663 (∀n.n < program → 654 664 \snd (bvt_lookup … (bitvector_of_nat 16 n) (\snd p1) 〈0,short_jump〉) = 655 665 \snd (bvt_lookup … (bitvector_of_nat 16 n) (\snd p2) 〈0,short_jump〉)). … … 750 760 qed. 751 761 752 definition policy_safe: list labelled_instruction → label_map → ℕ → ppc_pc_map → ppc_pc_map → Prop ≝753 λprogram.λlabels.λadded.λold_sigma.λsigma.754 ∀i.i < program →755 let 〈pc,j〉 ≝ bvt_lookup … (bitvector_of_nat 16 i) (\snd sigma) 〈0,short_jump〉 in756 let pc_plus_jmp_length ≝ bitvector_of_nat ? (\fst (bvt_lookup … (bitvector_of_nat ? (S i)) (\snd sigma) 〈0,short_jump〉)) in757 let 〈label,instr〉 ≝ nth i ? program 〈None ?, Comment [ ]〉 in758 ∀dest.is_jump_to instr dest →759 let paddr ≝ lookup_def … labels dest 0 in760 let addr ≝ bitvector_of_nat ? (if leb i paddr (* forward jump *)761 then \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd old_sigma) 〈0,short_jump〉) + added762 else \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd sigma) 〈0,short_jump〉)) in763 match j with764 [ short_jump ⇒ \fst (short_jump_cond pc_plus_jmp_length addr) = true ∧765 ¬is_call instr766  medium_jump ⇒ \fst (medium_jump_cond pc_plus_jmp_length addr) = true ∧767 \fst (short_jump_cond pc_plus_jmp_length addr) = false ∧768 ¬is_relative_jump instr769  long_jump ⇒ \fst (short_jump_cond pc_plus_jmp_length addr) = false ∧770 \fst (medium_jump_cond pc_plus_jmp_length addr) = false771 ].772 773 762 lemma not_true_is_false: 774 763 ∀b:bool.b ≠ true → b = false. 
src/ASM/PolicyStep.ma
r2059 r2101 12 12 ∀old_policy:(Σpolicy:ppc_pc_map. 13 13 And (And (And (And (out_of_program_none program policy) 14 ( jump_not_in_policyprogram policy))14 (not_jump_default program policy)) 15 15 (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd policy) 〈0,short_jump〉) = 0)) 16 16 (\fst policy = \fst (bvt_lookup … (bitvector_of_nat ? (program)) (\snd policy) 〈0,short_jump〉))) … … 21 21 [ None ⇒ nec_plus_ultra program old_policy 22 22  Some p ⇒ And (And (And (And (And (And (And (And (out_of_program_none program p) 23 ( jump_not_in_policyprogram p))24 ( policy_increase program old_policy p))25 (no_ch = true → policy_compact program labels p))23 (not_jump_default program p)) 24 (jump_increase program old_policy p)) 25 (no_ch = true → sigma_compact program labels p)) 26 26 (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd p) 〈0,short_jump〉) = 0)) 27 27 (\fst p = \fst (bvt_lookup … (bitvector_of_nat ? (program)) (\snd p) 〈0,short_jump〉))) 28 (no_ch = true → policy_pc_equal program old_policy p))29 ( policy_jump_equal program old_policy p → no_ch = true))28 (no_ch = true → sigma_pc_equal program old_policy p)) 29 (sigma_jump_equal program old_policy p → no_ch = true)) 30 30 (\fst p < 2^16) 31 31 ]) … … 37 37 let 〈added,policy〉 ≝ x in 38 38 And (And (And (And (And (And (And (And (out_of_program_none prefix policy) 39 ( jump_not_in_policyprefix policy))40 ( policy_increase prefix old_sigma policy))41 ( policy_compact_unsafe prefix labels policy))42 ( policy_safe prefix labels added old_sigma policy))39 (not_jump_default prefix policy)) 40 (jump_increase prefix old_sigma policy)) 41 (sigma_compact_unsafe prefix labels policy)) 42 (sigma_safe prefix labels added old_sigma policy)) 43 43 (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd policy) 〈0,short_jump〉) = 0)) 44 44 (\fst policy = \fst (bvt_lookup … (bitvector_of_nat ? (prefix)) (\snd policy) 〈0,short_jump〉))) 45 (added = 0 → policy_pc_equal prefix old_sigma policy))46 ( policy_jump_equal prefix old_sigma policy → added = 0))45 (added = 0 → sigma_pc_equal prefix old_sigma policy)) 46 (sigma_jump_equal prefix old_sigma policy → added = 0)) 47 47 program 48 48 (λprefix.λx.λtl.λprf.λacc. … … 165 165 (* USE: added = 0 → policy_pc_equal *) 166 166 >(proj2 ?? (proj1 ?? H) (eqb_true_to_eq … Hch) (lookup_def ?? labels x 0) ?) 167 [2,4,6,8: cases daemon (* XXX *) ] 167 [2,4,6,8: lapply ((pi2 ?? labels) x) 168 whd in match address_of_word_labels_code_mem; 169 normalize nodelta cases daemon (* XXX *) ] 168 170 [1,5: >(eqb_true_to_eq … Hch) <plus_n_O] 169 171 cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false) … … 177 179 1,3,9,11: #_ normalize nodelta @refl 178 180 ] 179 2,5: whd in match short_jump_cond; whd in match medium_jump_cond;181 2,5: whd in match short_jump_cond; whd in match absolute_jump_cond; 180 182 lapply (refl ? (leb i (lookup_def ?? labels x 0))) 181 183 cases (leb i (lookup_def ?? labels x 0)) in ⊢ (???% → %); #Hlab … … 192 194 cases (get_index' bool 2 0 flags) normalize nodelta 193 195 #H >(proj2 ?? (proj1 ?? H)) >(proj1 ?? (proj1 ?? H)) normalize nodelta @refl 194 3,6: whd in match short_jump_cond; whd in match medium_jump_cond;196 3,6: whd in match short_jump_cond; whd in match absolute_jump_cond; 195 197 lapply (refl ? (leb i (lookup_def ?? labels x 0))) 196 198 cases (leb i (lookup_def ?? labels x 0)) in ⊢ (???% → %); #Hlab 
src/utilities/extralib.ma
r2006 r2101 81 81 82 82 lemma dec_bounded_forall: 83 ∀P:ℕ → Prop.(∀n.(P n) + (¬P n)) → ∀k.(∀n.n ≤ k → P n) + ¬(∀n.n ≤k → P n).83 ∀P:ℕ → Prop.(∀n.(P n) + (¬P n)) → ∀k.(∀n.n < k → P n) + ¬(∀n.n < k → P n). 84 84 #P #HP_dec #k elim k k 85 [ cases (HP_dec 0) 86 [ #HP %1 #n #Hn <(le_n_O_to_eq … Hn) @HP 87  #HP %2 @nmk #H cases HP #H2 @H2 @H @le_n 88 ] 85 [ %1 #n #Hn @⊥ @(absurd (n < 0) Hn) @not_le_Sn_O 89 86  #k #Hind cases Hind 90 [ #Hk cases (HP_dec (S k))91 [ #HPk %1 #n #Hn elim(le_to_or_lt_eq … Hn)87 [ #Hk cases (HP_dec k) 88 [ #HPk %1 #n #Hn cases (le_to_or_lt_eq … Hn) 92 89 [ #H @(Hk … (le_S_S_to_le … H)) 93  #H > H@HPk90  #H >(injective_S … H) @HPk 94 91 ] 95  #HPk %2 @nmk #Habs @(absurd (P (S k))) [ @(Habs … (le_n (S k)))  @HPk ]92  #HPk %2 @nmk #Habs @(absurd (P k)) [ @(Habs … (le_n (S k)))  @HPk ] 96 93 ] 97  #Hk %2 @nmk #Habs @(absurd (∀n.n ≤k→P n)) [ #n' #Hn' @(Habs … (le_S … Hn'))  @Hk ]94  #Hk %2 @nmk #Habs @(absurd (∀n.n<k→P n)) [ #n' #Hn' @(Habs … (le_S … Hn'))  @Hk ] 98 95 ] 99 96 ] … … 101 98 102 99 lemma dec_bounded_exists: 103 ∀P:ℕ→Prop.(∀n.(P n) + (¬P n)) → ∀k.(∃n.n ≤ k ∧ P n) + ¬(∃n.n ≤k ∧ P n).100 ∀P:ℕ→Prop.(∀n.(P n) + (¬P n)) → ∀k.(∃n.n < k ∧ P n) + ¬(∃n.n < k ∧ P n). 104 101 #P #HP_dec #k elim k k 105 [ cases (HP_dec 0) 106 [ #HP %1 @(ex_intro ?? 0) @conj [ @le_n  @HP ] 107  #HP %2 @nmk #Habs @(absurd ?? HP) elim Habs #k #Hk 108 >(le_n_O_to_eq … (proj1 ?? Hk)) @(proj2 ?? Hk) 109 ] 102 [ %2 @nmk #Habs elim Habs #n #Hn @(absurd (n < 0) (proj1 … Hn)) @not_le_Sn_O 110 103  #k #Hind cases Hind 111 104 [ #Hk %1 elim Hk #n #Hn @(ex_intro … n) @conj [ @le_S @(proj1 … Hn)  @(proj2 … Hn) ] 112  #Hk cases (HP_dec (S k))113 [ #HPk %1 @(ex_intro … (S k)) @conj [ @le_n  @HPk ]105  #Hk cases (HP_dec k) 106 [ #HPk %1 @(ex_intro … k) @conj [ @le_n  @HPk ] 114 107  #HPk %2 @nmk #Habs elim Habs #n #Hn cases (le_to_or_lt_eq … (proj1 … Hn)) 115 [ #H @(absurd (∃n.n ≤k ∧ P n)) [ @(ex_intro … n) @conj108 [ #H @(absurd (∃n.n < k ∧ P n)) [ @(ex_intro … n) @conj 116 109 [ @(le_S_S_to_le … H)  @(proj2 … Hn) ]  @Hk ] 117  #H @(absurd (P (S k))) [ <H@(proj2 … Hn)  @HPk ]110  #H @(absurd (P k)) [ <(injective_S … H) @(proj2 … Hn)  @HPk ] 118 111 ] 119 112 ] … … 138 131 139 132 lemma not_exists_forall: 140 ∀k:ℕ.∀P:ℕ → Prop.¬(∃x.x ≤ k ∧ P x) → ∀x.x ≤k → ¬P x.133 ∀k:ℕ.∀P:ℕ → Prop.¬(∃x.x < k ∧ P x) → ∀x.x < k → ¬P x. 141 134 #k #P #Hex #x #Hx @nmk #Habs @(absurd ? ? Hex) @(ex_intro … x) 142 135 @conj [ @Hx  @Habs ] … … 144 137 145 138 lemma not_forall_exists: 146 ∀k:ℕ.∀P:ℕ → Prop.(∀n.(P n) + (¬P n)) → ¬(∀x.x ≤ k → P x) → ∃x.x ≤k ∧ ¬P x.139 ∀k:ℕ.∀P:ℕ → Prop.(∀n.(P n) + (¬P n)) → ¬(∀x.x < k → P x) → ∃x.x < k ∧ ¬P x. 147 140 #k #P #Hdec elim k 148 [ #Hfa @(ex_intro … 0) @conj 149 [ @le_n 150  @nmk #HP @(absurd ?? Hfa) #i #Hi <(le_n_O_to_eq … Hi) @HP 151 ] 152  k #k #Hind #Hfa cases (Hdec (S k)) 141 [ #Hfa @⊥ @(absurd ?? Hfa) #z #Hz @⊥ @(absurd ? Hz) @not_le_Sn_O 142  k #k #Hind #Hfa cases (Hdec k) 153 143 [ #HP elim (Hind ?) 154 144 [ Hind; #x #Hx @(ex_intro ?? x) @conj [ @le_S @(proj1 ?? Hx)  @(proj2 ?? Hx) ] 155 145  @nmk #H @(absurd ?? Hfa) #x #Hx cases (le_to_or_lt_eq ?? Hx) 156 146 [ #H2 @H @(le_S_S_to_le … H2) 157  #H2 > H2@HP147  #H2 >(injective_S … H2) @HP 158 148 ] 159 149 ] 160  #HP @(ex_intro … (S k)) @conj [ @le_n  @HP ]150  #HP @(ex_intro … k) @conj [ @le_n  @HP ] 161 151 ] 162 152 ]
Note: See TracChangeset
for help on using the changeset viewer.