Changeset 2211 for src/ASM/PolicyFront.ma
 Timestamp:
 Jul 18, 2012, 3:57:09 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/PolicyFront.ma
r2152 r2211 122 122 let 〈opc,oj〉 ≝ bvt_lookup … (bitvector_of_nat ? i) (\snd op) 〈0,short_jump〉 in 123 123 let 〈pc,j〉 ≝ bvt_lookup … (bitvector_of_nat ? i) (\snd p) 〈0,short_jump〉 in 124 (*opc ≤ pc ∧*)jmpleq oj j.124 jmpleq oj j. 125 125 126 126 (* this is the instruction size as determined by the jump length given *) … … 407 407 (∀i.i ≤ program → ∃pc. 408 408 bvt_lookup_opt … (bitvector_of_nat ? i) (\snd p) = Some ? 〈pc,short_jump〉)) 409 (\fst p <2^16)409 (\fst p ≤ 2^16) 410 410 ] ≝ 411 411 λprogram.λlabels. … … 425 425 〈pc + isize, bvt_insert … (bitvector_of_nat 16 (S (prefix))) 〈pc+isize,short_jump〉 sigma〉 426 426 ) 〈0, bvt_insert ?? (bitvector_of_nat 16 0) 〈0,short_jump〉 (Stub ??)〉 in 427 if g eb (\fst (pi1 ?? final_policy)) 2^16 then427 if gtb (\fst (pi1 ?? final_policy)) 2^16 then 428 428 None ? 429 429 else … … 431 431 [ / by I/ 432 432  lapply p p generalize in match (foldl_strong ?????); * #p #Hp #hg 433 @conj [ @Hp  @not_le_to_lt @leb_false_to_not_le <geb_to_leb @hg ] 434  @conj [ @conj [ @conj [ @conj (*[@conj 435 [ (* out_of_program_none *) 436 #i #Hi2 >append_length <commutative_plus @conj 437 [ (* → *) #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) Hi #Hi 438 cases p p #p cases p p #pc #p #Hp cases x x #l #pi 439 [ >lookup_opt_insert_miss 440 [ (* USE[pass]: out_of_program_none → *) 441 @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))) i Hi2)) 442 @le_S_to_le @le_S_to_le @Hi 443  @bitvector_of_nat_abs 444 [ @Hi2 445  @(transitive_lt … Hi2) @le_S_to_le @Hi 446  @sym_neq @lt_to_not_eq @le_S_to_le @Hi 447 ] 448 ] 449  >lookup_opt_insert_miss 450 [ <Hi 451 (* USE[pass]: out_of_program_none → *) 452 @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))) (S (S (prefix))) ?)) 453 [ >Hi @Hi2 454  @le_S @le_n 455 ] 456  @bitvector_of_nat_abs 457 [ @Hi2 458  @(transitive_lt … Hi2) <Hi @le_n 459  @sym_neq @lt_to_not_eq <Hi @le_n 460 ] 461 ] 462 ] 463  (* ← *) cases p p #p cases p p #pc #p #Hp cases x in prf; x #l #pi #prf 464 normalize nodelta cases (decidable_eq_nat i (S (prefix))) 465 [ #Hi >Hi >lookup_opt_insert_hit #H destruct (H) 466  #Hi >lookup_opt_insert_miss 467 [ #Hl 468 (* USE[pass]: out_of_program_none ← *) 469 elim (le_to_or_lt_eq … (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))) i Hi2) Hl)) 470 [ #Hi3 @Hi3 471  #Hi3 @⊥ @(absurd ? Hi3) @sym_neq @Hi 472 ] 473  @bitvector_of_nat_abs 474 [ @Hi2 475  @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf @le_S_S >append_length 476 <plus_n_Sm @le_S_S @le_plus_n_r 477  @Hi 478 ] 479 ] 480 ] 481 ] 482  *) 433 @conj [ @Hp  @not_lt_to_le @ltb_false_to_not_lt @hg ] 434  @conj [ @conj [ @conj [ @conj 483 435 [ (* not_jump_default *) cases p p #p cases p p #pc #sigma #Hp 484 436 cases x in prf; #lbl #ins #prf #i >append_length <commutative_plus #Hi … … 594 546 ] 595 547 ] 596  @conj [ @conj [ @conj [ @conj (*[ @conj 597 [ #i cases i 598 [ #Hi2 @conj 599 [ (* → *) #Hi @⊥ @(absurd ? Hi) @le_to_not_lt / by / 600  (* ← *) >lookup_opt_insert_hit #Hl destruct (Hl) 601 ] 602  i #i #Hi2 @conj 603 [ #Hi >lookup_opt_insert_miss 604 [ / by refl/ 605  @bitvector_of_nat_abs 606 [ @Hi2 607  / by / 608  @sym_neq @lt_to_not_eq / by / 609 ] 610 ] 611  #_ @le_S_S @le_O_n 612 ] 613 ] *) 548  @conj [ @conj [ @conj [ @conj 614 549 [ #i cases i 615 550 [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
Note: See TracChangeset
for help on using the changeset viewer.