 Timestamp:
 Jul 24, 2012, 11:40:43 AM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/PolicyStep.ma
r2239 r2240 452 452 qed. 453 453 454 (* One step in the search for a jump expansion fixpoint. *) 455 definition jump_expansion_step: ∀program:(Σl:list labelled_instruction. 456 S (l) < 2^16 ∧ is_well_labelled_p l). 457 ∀labels:(Σlm:label_map.∀l. 458 occurs_exactly_once ?? l program → 459 bitvector_of_nat ? (lookup_def … lm l 0) = 460 address_of_word_labels_code_mem program l). 461 ∀old_policy:(Σpolicy:ppc_pc_map. 462 (* out_of_program_none program policy *) 463 And (And (And (And (not_jump_default program policy) 464 (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd policy) 〈0,short_jump〉) = 0)) 465 (\fst policy = \fst (bvt_lookup … (bitvector_of_nat ? (program)) (\snd policy) 〈0,short_jump〉))) 466 (sigma_compact_unsafe program labels policy)) 467 (\fst policy ≤ 2^16)). 468 (Σx:bool × (option ppc_pc_map). 469 let 〈no_ch,y〉 ≝ x in 470 match y with 471 [ None ⇒ nec_plus_ultra program old_policy 472  Some p ⇒ And (And (And (And (And (And (And 473 (not_jump_default program p) 474 (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd p) 〈0,short_jump〉) = 0)) 475 (\fst p = \fst (bvt_lookup … (bitvector_of_nat ? (program)) (\snd p) 〈0,short_jump〉))) 476 (jump_increase program old_policy p)) 477 (sigma_compact_unsafe program labels p)) 478 (sigma_jump_equal program old_policy p → no_ch = true)) 479 (no_ch = true → sigma_pc_equal program old_policy p)) 480 (\fst p ≤ 2^16) 481 ]) 482 ≝ 483 λprogram.λlabels.λold_sigma. 484 let 〈final_added, final_policy〉 ≝ 485 pi1 ?? (foldl_strong (option Identifier × pseudo_instruction) 486 (λprefix.Σx:ℕ × ppc_pc_map. 487 let 〈added,policy〉 ≝ x in 488 And (And (And (And (And (And (And (And (And (not_jump_default prefix policy) 489 (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd policy) 〈0,short_jump〉) = 0)) 490 (\fst policy = \fst (bvt_lookup … (bitvector_of_nat ? (prefix)) (\snd policy) 〈0,short_jump〉))) 491 (jump_increase prefix old_sigma policy)) 492 (sigma_compact_unsafe prefix labels policy)) 493 (sigma_jump_equal prefix old_sigma policy → added = 0)) 494 (added = 0 → sigma_pc_equal prefix old_sigma policy)) 495 (out_of_program_none prefix policy)) 496 (\fst (bvt_lookup … (bitvector_of_nat ? (prefix)) (\snd policy) 〈0,short_jump〉) = 497 \fst (bvt_lookup … (bitvector_of_nat ? (prefix)) (\snd old_sigma) 〈0,short_jump〉) + added)) 498 (sigma_safe prefix labels added old_sigma policy)) 499 program 500 (λprefix.λx.λtl.λprf.λacc. 501 let 〈inc_added, inc_pc_sigma〉 ≝ (pi1 ?? acc) in 502 let 〈label,instr〉 ≝ x in 503 (* Now, we must add the current ppc and its pc translation. 504 * Three possibilities: 505 *  Instruction is not a jump; i.e. constant size whatever the sigma we use; 506 *  Instruction is a backward jump; we can use the sigma we're constructing, 507 * since it will already know the translation of its destination; 508 *  Instruction is a forward jump; we must use the old sigma (the new sigma 509 * does not know the translation yet), but compensate for the jumps we 510 * have lengthened. 511 *) 512 let add_instr ≝ match instr with 513 [ Jmp j ⇒ Some ? (select_jump_length labels old_sigma inc_pc_sigma inc_added (prefix) j) 514  Call c ⇒ Some ? (select_call_length labels old_sigma inc_pc_sigma inc_added (prefix) c) 515  Instruction i ⇒ jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added (prefix) i 516  _ ⇒ None ? 517 ] in 518 let 〈inc_pc, inc_sigma〉 ≝ inc_pc_sigma in 519 let old_length ≝ 520 \snd (bvt_lookup … (bitvector_of_nat ? (prefix)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) in 521 let old_size ≝ instruction_size_jmplen old_length instr in 522 let 〈new_length, isize〉 ≝ match add_instr with 523 [ None ⇒ 〈short_jump, instruction_size_jmplen short_jump instr〉 524  Some pl ⇒ 〈max_length old_length pl, instruction_size_jmplen (max_length old_length pl) instr〉 525 ] in 526 let new_added ≝ match add_instr with 527 [ None ⇒ inc_added 528  Some x ⇒ plus inc_added (minus isize old_size) 529 ] in 530 let old_Slength ≝ 531 \snd (bvt_lookup … (bitvector_of_nat ? (S (prefix))) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) in 532 let updated_sigma ≝ 533 (* we add the new PC to the next position and the new jump length to this one *) 534 bvt_insert … (bitvector_of_nat ? (S (prefix))) 〈inc_pc + isize, old_Slength〉 535 (bvt_insert … (bitvector_of_nat ? (prefix)) 〈inc_pc, new_length〉 inc_sigma) in 536 〈new_added, 〈plus inc_pc isize, updated_sigma〉〉 537 ) 〈0, 〈0, 538 bvt_insert … 539 (bitvector_of_nat ? 0) 540 〈0, \snd (bvt_lookup … (bitvector_of_nat ? 0) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉)〉 541 (Stub ??)〉〉 542 ) in 543 if gtb (\fst final_policy) 2^16 then 544 〈eqb final_added 0, None ?〉 545 else 546 〈eqb final_added 0, Some ? final_policy〉. 547 [ normalize nodelta @nmk #Habs lapply p p cases (foldl_strong ? (λ_.Σx.?) ???) 548 #x #H #Heq >Heq in H; normalize nodelta Heq x #Hind 549 (* USE: inc_pc = fst of policy (from fold) *) 550 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))))))) in p1; 551 (* USE: fst policy < 2^16, inc_pc = fst of policy (old_sigma) *) 552 lapply (proj2 ?? (pi2 ?? old_sigma)) >(proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) 553 #Hsig #Hge 554 (* USE: added = 0 → policy_pc_equal (from fold) *) 555 lapply ((proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))) ? (program) (le_n (program))) 556 [ (* USE: policy_jump_equal → added = 0 (from fold) *) 557 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind))))) #i #Hi 558 inversion (is_jump (\snd (nth i ? program 〈None ?, Comment []〉))) 559 [ #Hj 560 (* USE: policy_increase (from fold) *) 561 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))))) i (le_S_to_le … Hi)) 562 lapply (Habs i Hi ?) [ >Hj %] 563 cases (bvt_lookup … (bitvector_of_nat ? i) (\snd old_sigma) 〈0,short_jump〉) 564 #opc #oj 565 cases (bvt_lookup … (bitvector_of_nat ? i) (\snd final_policy) 〈0,short_jump〉) 566 #pc #j normalize nodelta #Heq >Heq cases j 567 [1,2: #abs cases abs #abs2 try (cases abs2) @refl 568 3: #_ @refl 569 ] 570  #Hnj 571 (* USE: not_jump_default (from fold and old_sigma) *) 572 >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))))))) i Hi ?) 573 [2: >Hnj %] 574 >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) i Hi ?) try % 575 >Hnj % 576 ] 577  #abs >abs in Hsig; #Hsig 578 @(absurd ? Hsig) @lt_to_not_le @ltb_true_to_lt @Hge 579 ] 580  normalize nodelta lapply p p cases (foldl_strong ? (λ_.Σx.?)???) in ⊢ (% → ?); #x #H #H2 581 >H2 in H; normalize nodelta H2 x #H @conj 582 [ @conj [ @conj 583 [ (* USE[pass]: not_jump_default, 0 ↦ 0, inc_pc = fst policy, 584 * jump_increase, sigma_compact_unsafe (from fold) *) 585 @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))) 586  #H2 (* USE[pass]: sigma_jump_equal → added = 0 (from fold) *) 587 @eq_to_eqb_true @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))) @H2 588 ] 589  (* USE[pass]: added = 0 → sigma_pc_equal (from fold) *) 590 #H2 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) @eqb_true_to_eq @H2 591 ] 592  @not_lt_to_le @ltb_false_to_not_lt @p1 593 ] 594 4: lapply (pi2 ?? acc) >p lapply (refl ? (inc_pc_sigma)) cases inc_pc_sigma in ⊢ (???% → %); 595 #inc_pc #inc_sigma #Hips 596 inversion (bvt_lookup … (bitvector_of_nat ? (prefix)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) 597 #old_pc #old_length #Holdeq #Hpolicy normalize nodelta in Hpolicy; @pair_elim 598 #added #policy normalize nodelta @pair_elim #new_length #isize normalize nodelta 599 #Heq1 #Heq2 600 cut (S (prefix) < 2^16) 601 [ @(transitive_lt … (proj1 … (pi2 ?? program))) @le_S_S >prf >append_length 602 <plus_n_Sm @le_S_S @le_plus_n_r ] #prefix_ok1 603 cut (prefix < 2^16) [ @(transitive_lt … prefix_ok1) %] #prefix_ok 604 cases (pair_destruct ?????? Heq2) Heq2 #Heq2a #Heq2b 605 % [ % [ % [ % [ % [ % [ % [ % [ % ]]]]]]]] 606 (* NOTE: to save memory and speed up work, there's cases daemon here. They can be 607 * commented out for full proofs, but this needs a lot of memory and time *) 608 [ (* not_jump_default *) 609 @(jump_expansion_step1 … Heq1 Heq2b) try assumption 610 @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))) 611  (* 0 ↦ 0 *) 612 @(jump_expansion_step2 … Heq2b) try assumption 613 [ @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))) 614  @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) ] 615  (* inc_pc = fst of policy *) 616 <Heq2b >append_length >(commutative_plus (prefix)) >lookup_insert_hit @refl 617  (* jump_increase *) 618 @(jump_expansion_step3 … (pi1 ?? old_sigma) … prf … p1 ??? old_length Holdeq 619 … Heq1 prefix_ok1 prefix_ok Heq2b) 620 try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) 621 cases (pi2 … old_sigma) * * * #H #_ #_ #_ #_ @H 622  (* sigma_compact_unsafe *) 623 @(jump_expansion_step4 … Heq1 … Heq2b) try assumption 624 try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) 625 try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))) 626 @(proj2 ?? (proj1 ?? (proj1 ?? Hpolicy))) 627  (* policy_jump_equal → added = 0 *) 628 @(jump_expansion_step5 … Holdeq … Heq1 … Heq2b) try assumption 629 try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) 630 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) 631  (* added = 0 → policy_pc_equal *) cases daemon 454 lemma jump_expansion_step6: 455 (* 456 program : 457 (Σl:list labelled_instruction.S (l)< 2 \sup 16 ∧is_well_labelled_p l) 458 labels : 459 (Σlm:label_map 460 .(∀l:identifier ASMTag 461 .occurs_exactly_once ASMTag pseudo_instruction l program 462 →bitvector_of_nat 16 (lookup_def ASMTag ℕ lm l O) 463 =address_of_word_labels_code_mem program l))*) 464 ∀old_sigma : ppc_pc_map.(* 465 (Σpolicy:ppc_pc_map 466 .not_jump_default program policy 467 ∧\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) (\snd policy) 468 〈O,short_jump〉) 469 =O 470 ∧\fst policy 471 =\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (program)) 472 (\snd policy) 〈O,short_jump〉) 473 ∧sigma_compact_unsafe program labels policy 474 ∧\fst policy≤ 2 \sup 16 )*) 475 ∀prefix : list (option Identifier×pseudo_instruction).(* 476 x : (option Identifier×pseudo_instruction) 477 tl : (list (option Identifier×pseudo_instruction)) 478 prf : (program=prefix@[x]@tl) 479 acc : 480 (Σx0:ℕ×ppc_pc_map 481 .(let 〈added,policy〉 ≝x0 in 482 not_jump_default prefix policy 483 ∧\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) (\snd policy) 484 〈O,short_jump〉) 485 =O 486 ∧\fst policy 487 =\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (prefix)) 488 (\snd policy) 〈O,short_jump〉) 489 ∧jump_increase prefix old_sigma policy 490 ∧sigma_compact_unsafe prefix labels policy 491 ∧(sigma_jump_equal prefix old_sigma policy→added=O) 492 ∧(added=O→sigma_pc_equal prefix old_sigma policy) 493 ∧out_of_program_none prefix policy 494 ∧\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (prefix)) 495 (\snd policy) 〈O,short_jump〉) 496 =\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (prefix)) 497 (\snd old_sigma) 〈O,short_jump〉) 498 +added 499 ∧sigma_safe prefix labels added old_sigma policy)) 500 inc_added : ℕ 501 inc_pc_sigma : ppc_pc_map 502 p : (acc≃〈inc_added,inc_pc_sigma〉)*) 503 ∀label : option Identifier. 504 ∀instr : pseudo_instruction.(* 505 p1 : (x≃〈label,instr〉) 506 add_instr ≝ 507 match instr 508 in pseudo_instruction 509 return λ_:pseudo_instruction.(option jump_length) 510 with 511 [Instruction (i:(preinstruction Identifier))⇒ 512 jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added 513 (prefix) i 514 Comment (_:String)⇒None jump_length 515 Cost (_:costlabel)⇒None jump_length 516 Jmp (j:Identifier)⇒ 517 Some jump_length 518 (select_jump_length labels old_sigma inc_pc_sigma inc_added (prefix) j) 519 Call (c:Identifier)⇒ 520 Some jump_length 521 (select_call_length labels old_sigma inc_pc_sigma inc_added (prefix) c) 522 Mov (_:[[dptr]]) (_0:Identifier)⇒None jump_length] 523 inc_pc : ℕ 524 inc_sigma : (BitVectorTrie (ℕ×jump_length) 16) 525 Hips : (inc_pc_sigma=〈inc_pc,inc_sigma〉) 526 old_pc : ℕ 527 old_length : jump_length 528 Holdeq : 529 (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (prefix)) (\snd old_sigma) 530 〈O,short_jump〉 531 =〈old_pc,old_length〉) 532 Hpolicy : 533 (not_jump_default prefix 〈inc_pc,inc_sigma〉 534 ∧\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) inc_sigma 535 〈O,short_jump〉) 536 =O 537 ∧inc_pc 538 =\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (prefix)) inc_sigma 539 〈O,short_jump〉) 540 ∧jump_increase prefix old_sigma 〈inc_pc,inc_sigma〉 541 ∧sigma_compact_unsafe prefix labels 〈inc_pc,inc_sigma〉 542 ∧(sigma_jump_equal prefix old_sigma 〈inc_pc,inc_sigma〉→inc_added=O) 543 ∧(inc_added=O→sigma_pc_equal prefix old_sigma 〈inc_pc,inc_sigma〉) 544 ∧out_of_program_none prefix 〈inc_pc,inc_sigma〉 545 ∧\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (prefix)) inc_sigma 546 〈O,short_jump〉) 547 =old_pc+inc_added 548 ∧sigma_safe prefix labels inc_added old_sigma 〈inc_pc,inc_sigma〉)*) 549 ∀added : ℕ. 550 ∀policy : ppc_pc_map.(* 551 new_length : jump_length 552 isize : ℕ 553 Heq1 : 554 (match 555 match instr 556 in pseudo_instruction 557 return λ_:pseudo_instruction.(option jump_length) 558 with 559 [Instruction (i:(preinstruction Identifier))⇒ 560 jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added 561 (prefix) i 562 Comment (_:String)⇒None jump_length 563 Cost (_:costlabel)⇒None jump_length 564 Jmp (j:Identifier)⇒ 565 Some jump_length 566 (select_jump_length labels old_sigma inc_pc_sigma inc_added (prefix) j) 567 Call (c:Identifier)⇒ 568 Some jump_length 569 (select_call_length labels old_sigma inc_pc_sigma inc_added (prefix) c) 570 Mov (_:[[dptr]]) (_0:Identifier)⇒None jump_length] 571 in option 572 return λ_0:(option jump_length).(jump_length×ℕ) 573 with 574 [None⇒〈short_jump,instruction_size_jmplen short_jump instr〉 575 Some (pl:jump_length)⇒ 576 〈max_length old_length pl, 577 instruction_size_jmplen (max_length old_length pl) instr〉] 578 =〈new_length,isize〉) 579 prefix_ok1 : (S (prefix)< 2 \sup 16 ) 580 prefix_ok : (prefix< 2 \sup 16 ) 581 Heq2a : 582 (match 583 match instr 584 in pseudo_instruction 585 return λ_0:pseudo_instruction.(option jump_length) 586 with 587 [Instruction (i:(preinstruction Identifier))⇒ 588 jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added 589 (prefix) i 590 Comment (_0:String)⇒None jump_length 591 Cost (_0:costlabel)⇒None jump_length 592 Jmp (j:Identifier)⇒ 593 Some jump_length 594 (select_jump_length labels old_sigma inc_pc_sigma inc_added (prefix) j) 595 Call (c:Identifier)⇒ 596 Some jump_length 597 (select_call_length labels old_sigma inc_pc_sigma inc_added (prefix) c) 598 Mov (_0:[[dptr]]) (_00:Identifier)⇒None jump_length] 599 in option 600 return λ_0:(option jump_length).ℕ 601 with 602 [None⇒inc_added 603 Some (x0:jump_length)⇒ 604 inc_added+(isizeinstruction_size_jmplen old_length instr)] 605 =added) 606 Heq2b : 607 (〈inc_pc+isize, 608 insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (prefix))) 609 〈inc_pc+isize, 610 \snd (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (prefix))) 611 (\snd old_sigma) 〈O,short_jump〉)〉 612 (insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (prefix)) 613 〈inc_pc,new_length〉 inc_sigma)〉 614 =policy) 615 *) 616 added=O→sigma_pc_equal (prefix@[〈label,instr〉]) old_sigma policy. 617 cases daemon(* 632 618 (* USE[pass]: added = 0 → policy_pc_equal *) 633 (*lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))619 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) 634 620 <(proj2 ?? (pair_destruct ?????? Heq2)) 635 621 <(proj1 ?? (pair_destruct ?????? Heq2)) … … 928 914 ] 929 915 ] 930 ] *) 931  (* out_of_program_none *) cases daemon 932 (* #i #Hi2 >append_length <commutative_plus @conj 916 ]*) 917 qed. 918 919 lemma jump_expansion_step7: 920 (* 921 program : 922 (Σl:list labelled_instruction.S (l)< 2 \sup 16 ∧is_well_labelled_p l) 923 labels : 924 (Σlm:label_map 925 .(∀l:identifier ASMTag 926 .occurs_exactly_once ASMTag pseudo_instruction l program 927 →bitvector_of_nat 16 (lookup_def ASMTag ℕ lm l O) 928 =address_of_word_labels_code_mem program l)) 929 old_sigma : 930 (Σpolicy:ppc_pc_map 931 .not_jump_default program policy 932 ∧\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) (\snd policy) 933 〈O,short_jump〉) 934 =O 935 ∧\fst policy 936 =\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (program)) 937 (\snd policy) 〈O,short_jump〉) 938 ∧sigma_compact_unsafe program labels policy 939 ∧\fst policy≤ 2 \sup 16 )*) 940 ∀prefix : list (option Identifier×pseudo_instruction).(* 941 x : (option Identifier×pseudo_instruction) 942 tl : (list (option Identifier×pseudo_instruction)) 943 prf : (program=prefix@[x]@tl) 944 acc : 945 (Σx0:ℕ×ppc_pc_map 946 .(let 〈added,policy〉 ≝x0 in 947 not_jump_default prefix policy 948 ∧\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) (\snd policy) 949 〈O,short_jump〉) 950 =O 951 ∧\fst policy 952 =\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (prefix)) 953 (\snd policy) 〈O,short_jump〉) 954 ∧jump_increase prefix old_sigma policy 955 ∧sigma_compact_unsafe prefix labels policy 956 ∧(sigma_jump_equal prefix old_sigma policy→added=O) 957 ∧(added=O→sigma_pc_equal prefix old_sigma policy) 958 ∧out_of_program_none prefix policy 959 ∧\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (prefix)) 960 (\snd policy) 〈O,short_jump〉) 961 =\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (prefix)) 962 (\snd old_sigma) 〈O,short_jump〉) 963 +added 964 ∧sigma_safe prefix labels added old_sigma policy)) 965 inc_added : ℕ 966 inc_pc_sigma : ppc_pc_map 967 p : (acc≃〈inc_added,inc_pc_sigma〉)*) 968 ∀label : option Identifier. 969 ∀instr : pseudo_instruction.(* 970 p1 : (x≃〈label,instr〉) 971 add_instr ≝ 972 match instr 973 in pseudo_instruction 974 return λ_:pseudo_instruction.(option jump_length) 975 with 976 [Instruction (i:(preinstruction Identifier))⇒ 977 jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added 978 (prefix) i 979 Comment (_:String)⇒None jump_length 980 Cost (_:costlabel)⇒None jump_length 981 Jmp (j:Identifier)⇒ 982 Some jump_length 983 (select_jump_length labels old_sigma inc_pc_sigma inc_added (prefix) j) 984 Call (c:Identifier)⇒ 985 Some jump_length 986 (select_call_length labels old_sigma inc_pc_sigma inc_added (prefix) c) 987 Mov (_:[[dptr]]) (_0:Identifier)⇒None jump_length] 988 inc_pc : ℕ 989 inc_sigma : (BitVectorTrie (ℕ×jump_length) 16) 990 Hips : (inc_pc_sigma=〈inc_pc,inc_sigma〉) 991 old_pc : ℕ 992 old_length : jump_length 993 Holdeq : 994 (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (prefix)) (\snd old_sigma) 995 〈O,short_jump〉 996 =〈old_pc,old_length〉) 997 Hpolicy : 998 (not_jump_default prefix 〈inc_pc,inc_sigma〉 999 ∧\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) inc_sigma 1000 〈O,short_jump〉) 1001 =O 1002 ∧inc_pc 1003 =\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (prefix)) inc_sigma 1004 〈O,short_jump〉) 1005 ∧jump_increase prefix old_sigma 〈inc_pc,inc_sigma〉 1006 ∧sigma_compact_unsafe prefix labels 〈inc_pc,inc_sigma〉 1007 ∧(sigma_jump_equal prefix old_sigma 〈inc_pc,inc_sigma〉→inc_added=O) 1008 ∧(inc_added=O→sigma_pc_equal prefix old_sigma 〈inc_pc,inc_sigma〉) 1009 ∧out_of_program_none prefix 〈inc_pc,inc_sigma〉 1010 ∧\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (prefix)) inc_sigma 1011 〈O,short_jump〉) 1012 =old_pc+inc_added 1013 ∧sigma_safe prefix labels inc_added old_sigma 〈inc_pc,inc_sigma〉) 1014 added : ℕ*) 1015 ∀policy : ppc_pc_map.(* 1016 new_length : jump_length 1017 isize : ℕ 1018 Heq1 : 1019 (match 1020 match instr 1021 in pseudo_instruction 1022 return λ_:pseudo_instruction.(option jump_length) 1023 with 1024 [Instruction (i:(preinstruction Identifier))⇒ 1025 jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added 1026 (prefix) i 1027 Comment (_:String)⇒None jump_length 1028 Cost (_:costlabel)⇒None jump_length 1029 Jmp (j:Identifier)⇒ 1030 Some jump_length 1031 (select_jump_length labels old_sigma inc_pc_sigma inc_added (prefix) j) 1032 Call (c:Identifier)⇒ 1033 Some jump_length 1034 (select_call_length labels old_sigma inc_pc_sigma inc_added (prefix) c) 1035 Mov (_:[[dptr]]) (_0:Identifier)⇒None jump_length] 1036 in option 1037 return λ_0:(option jump_length).(jump_length×ℕ) 1038 with 1039 [None⇒〈short_jump,instruction_size_jmplen short_jump instr〉 1040 Some (pl:jump_length)⇒ 1041 〈max_length old_length pl, 1042 instruction_size_jmplen (max_length old_length pl) instr〉] 1043 =〈new_length,isize〉) 1044 prefix_ok1 : (S (prefix)< 2 \sup 16 ) 1045 prefix_ok : (prefix< 2 \sup 16 ) 1046 Heq2a : 1047 (match 1048 match instr 1049 in pseudo_instruction 1050 return λ_0:pseudo_instruction.(option jump_length) 1051 with 1052 [Instruction (i:(preinstruction Identifier))⇒ 1053 jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added 1054 (prefix) i 1055 Comment (_0:String)⇒None jump_length 1056 Cost (_0:costlabel)⇒None jump_length 1057 Jmp (j:Identifier)⇒ 1058 Some jump_length 1059 (select_jump_length labels old_sigma inc_pc_sigma inc_added (prefix) j) 1060 Call (c:Identifier)⇒ 1061 Some jump_length 1062 (select_call_length labels old_sigma inc_pc_sigma inc_added (prefix) c) 1063 Mov (_0:[[dptr]]) (_00:Identifier)⇒None jump_length] 1064 in option 1065 return λ_0:(option jump_length).ℕ 1066 with 1067 [None⇒inc_added 1068 Some (x0:jump_length)⇒ 1069 inc_added+(isizeinstruction_size_jmplen old_length instr)] 1070 =added) 1071 Heq2b : 1072 (〈inc_pc+isize, 1073 insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (prefix))) 1074 〈inc_pc+isize, 1075 \snd (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (prefix))) 1076 (\snd old_sigma) 〈O,short_jump〉)〉 1077 (insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (prefix)) 1078 〈inc_pc,new_length〉 inc_sigma)〉 1079 =policy) 1080 *) 1081 out_of_program_none (prefix@[〈label,instr〉]) policy. 1082 cases daemon (* 1083 #i #Hi2 >append_length <commutative_plus @conj 933 1084 [ (* → *) #Hi normalize in Hi; 934 1085 cases instr in Heq2; normalize nodelta … … 966 1117 ] 967 1118 ] 968 ] *) 969  (* lookup p = lookup old_sigma + added *) cases daemon 970 (* <(proj2 ?? (pair_destruct ?????? Heq2)) >append_length <plus_n_Sm <plus_n_O 1119 ]*) 1120 qed. 1121 1122 lemma jump_expansion_step8: 1123 (* 1124 program : 1125 (Σl:list labelled_instruction.S (l)< 2 \sup 16 ∧is_well_labelled_p l) 1126 labels : 1127 (Σlm:label_map 1128 .(∀l:identifier ASMTag 1129 .occurs_exactly_once ASMTag pseudo_instruction l program 1130 →bitvector_of_nat 16 (lookup_def ASMTag ℕ lm l O) 1131 =address_of_word_labels_code_mem program l))*) 1132 ∀old_sigma : ppc_pc_map.(* 1133 (Σpolicy:ppc_pc_map 1134 .not_jump_default program policy 1135 ∧\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) (\snd policy) 1136 〈O,short_jump〉) 1137 =O 1138 ∧\fst policy 1139 =\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (program)) 1140 (\snd policy) 〈O,short_jump〉) 1141 ∧sigma_compact_unsafe program labels policy 1142 ∧\fst policy≤ 2 \sup 16 )*) 1143 ∀prefix : list (option Identifier×pseudo_instruction).(* 1144 x : (option Identifier×pseudo_instruction) 1145 tl : (list (option Identifier×pseudo_instruction)) 1146 prf : (program=prefix@[x]@tl) 1147 acc : 1148 (Σx0:ℕ×ppc_pc_map 1149 .(let 〈added,policy〉 ≝x0 in 1150 not_jump_default prefix policy 1151 ∧\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) (\snd policy) 1152 〈O,short_jump〉) 1153 =O 1154 ∧\fst policy 1155 =\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (prefix)) 1156 (\snd policy) 〈O,short_jump〉) 1157 ∧jump_increase prefix old_sigma policy 1158 ∧sigma_compact_unsafe prefix labels policy 1159 ∧(sigma_jump_equal prefix old_sigma policy→added=O) 1160 ∧(added=O→sigma_pc_equal prefix old_sigma policy) 1161 ∧out_of_program_none prefix policy 1162 ∧\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (prefix)) 1163 (\snd policy) 〈O,short_jump〉) 1164 =\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (prefix)) 1165 (\snd old_sigma) 〈O,short_jump〉) 1166 +added 1167 ∧sigma_safe prefix labels added old_sigma policy)) 1168 inc_added : ℕ 1169 inc_pc_sigma : ppc_pc_map 1170 p : (acc≃〈inc_added,inc_pc_sigma〉)*) 1171 ∀label : option Identifier. 1172 ∀instr : pseudo_instruction.(* 1173 p1 : (x≃〈label,instr〉) 1174 add_instr ≝ 1175 match instr 1176 in pseudo_instruction 1177 return λ_:pseudo_instruction.(option jump_length) 1178 with 1179 [Instruction (i:(preinstruction Identifier))⇒ 1180 jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added 1181 (prefix) i 1182 Comment (_:String)⇒None jump_length 1183 Cost (_:costlabel)⇒None jump_length 1184 Jmp (j:Identifier)⇒ 1185 Some jump_length 1186 (select_jump_length labels old_sigma inc_pc_sigma inc_added (prefix) j) 1187 Call (c:Identifier)⇒ 1188 Some jump_length 1189 (select_call_length labels old_sigma inc_pc_sigma inc_added (prefix) c) 1190 Mov (_:[[dptr]]) (_0:Identifier)⇒None jump_length] 1191 inc_pc : ℕ 1192 inc_sigma : (BitVectorTrie (ℕ×jump_length) 16) 1193 Hips : (inc_pc_sigma=〈inc_pc,inc_sigma〉) 1194 old_pc : ℕ 1195 old_length : jump_length 1196 Holdeq : 1197 (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (prefix)) (\snd old_sigma) 1198 〈O,short_jump〉 1199 =〈old_pc,old_length〉) 1200 Hpolicy : 1201 (not_jump_default prefix 〈inc_pc,inc_sigma〉 1202 ∧\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) inc_sigma 1203 〈O,short_jump〉) 1204 =O 1205 ∧inc_pc 1206 =\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (prefix)) inc_sigma 1207 〈O,short_jump〉) 1208 ∧jump_increase prefix old_sigma 〈inc_pc,inc_sigma〉 1209 ∧sigma_compact_unsafe prefix labels 〈inc_pc,inc_sigma〉 1210 ∧(sigma_jump_equal prefix old_sigma 〈inc_pc,inc_sigma〉→inc_added=O) 1211 ∧(inc_added=O→sigma_pc_equal prefix old_sigma 〈inc_pc,inc_sigma〉) 1212 ∧out_of_program_none prefix 〈inc_pc,inc_sigma〉 1213 ∧\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (prefix)) inc_sigma 1214 〈O,short_jump〉) 1215 =old_pc+inc_added 1216 ∧sigma_safe prefix labels inc_added old_sigma 〈inc_pc,inc_sigma〉)*) 1217 ∀added : ℕ. 1218 ∀policy : ppc_pc_map.(* 1219 new_length : jump_length 1220 isize : ℕ 1221 Heq1 : 1222 (match 1223 match instr 1224 in pseudo_instruction 1225 return λ_:pseudo_instruction.(option jump_length) 1226 with 1227 [Instruction (i:(preinstruction Identifier))⇒ 1228 jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added 1229 (prefix) i 1230 Comment (_:String)⇒None jump_length 1231 Cost (_:costlabel)⇒None jump_length 1232 Jmp (j:Identifier)⇒ 1233 Some jump_length 1234 (select_jump_length labels old_sigma inc_pc_sigma inc_added (prefix) j) 1235 Call (c:Identifier)⇒ 1236 Some jump_length 1237 (select_call_length labels old_sigma inc_pc_sigma inc_added (prefix) c) 1238 Mov (_:[[dptr]]) (_0:Identifier)⇒None jump_length] 1239 in option 1240 return λ_0:(option jump_length).(jump_length×ℕ) 1241 with 1242 [None⇒〈short_jump,instruction_size_jmplen short_jump instr〉 1243 Some (pl:jump_length)⇒ 1244 〈max_length old_length pl, 1245 instruction_size_jmplen (max_length old_length pl) instr〉] 1246 =〈new_length,isize〉) 1247 prefix_ok1 : (S (prefix)< 2 \sup 16 ) 1248 prefix_ok : (prefix< 2 \sup 16 ) 1249 Heq2a : 1250 (match 1251 match instr 1252 in pseudo_instruction 1253 return λ_0:pseudo_instruction.(option jump_length) 1254 with 1255 [Instruction (i:(preinstruction Identifier))⇒ 1256 jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added 1257 (prefix) i 1258 Comment (_0:String)⇒None jump_length 1259 Cost (_0:costlabel)⇒None jump_length 1260 Jmp (j:Identifier)⇒ 1261 Some jump_length 1262 (select_jump_length labels old_sigma inc_pc_sigma inc_added (prefix) j) 1263 Call (c:Identifier)⇒ 1264 Some jump_length 1265 (select_call_length labels old_sigma inc_pc_sigma inc_added (prefix) c) 1266 Mov (_0:[[dptr]]) (_00:Identifier)⇒None jump_length] 1267 in option 1268 return λ_0:(option jump_length).ℕ 1269 with 1270 [None⇒inc_added 1271 Some (x0:jump_length)⇒ 1272 inc_added+(isizeinstruction_size_jmplen old_length instr)] 1273 =added) 1274 Heq2b : 1275 (〈inc_pc+isize, 1276 insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (prefix))) 1277 〈inc_pc+isize, 1278 \snd (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (prefix))) 1279 (\snd old_sigma) 〈O,short_jump〉)〉 1280 (insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (prefix)) 1281 〈inc_pc,new_length〉 inc_sigma)〉 1282 =policy) 1283 *) 1284 \fst (lookup (ℕ×jump_length) 16 1285 (bitvector_of_nat 16 ((prefix@[〈label,instr〉]))) (\snd policy) 1286 〈O,short_jump〉) 1287 =\fst (lookup (ℕ×jump_length) 16 1288 (bitvector_of_nat 16 ((prefix@[〈label,instr〉]))) (\snd old_sigma) 1289 〈O,short_jump〉) 1290 +added. 1291 cases daemon(* 1292 <(proj2 ?? (pair_destruct ?????? Heq2)) >append_length <plus_n_Sm <plus_n_O 971 1293 >lookup_insert_hit 972 1294 <(proj1 ?? (pair_destruct ?????? Heq2)) cases instr in p1 Heq1; … … 1098 1420 ] 1099 1421 ] 1100 ] *) 1101  (* sigma_safe *) cases daemon (*#i >append_length >commutative_plus #Hi normalize in Hi; 1422 ]*) 1423 qed. 1424 1425 lemma jump_expansion_step9: 1426 (* 1427 program : 1428 (Σl:list labelled_instruction.S (l)< 2 \sup 16 ∧is_well_labelled_p l)*) 1429 ∀labels : label_map.(* 1430 (Σlm:label_map 1431 .(∀l:identifier ASMTag 1432 .occurs_exactly_once ASMTag pseudo_instruction l program 1433 →bitvector_of_nat 16 (lookup_def ASMTag ℕ lm l O) 1434 =address_of_word_labels_code_mem program l))*) 1435 ∀old_sigma : ppc_pc_map.(* 1436 (Σpolicy:ppc_pc_map 1437 .not_jump_default program policy 1438 ∧\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) (\snd policy) 1439 〈O,short_jump〉) 1440 =O 1441 ∧\fst policy 1442 =\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (program)) 1443 (\snd policy) 〈O,short_jump〉) 1444 ∧sigma_compact_unsafe program labels policy 1445 ∧\fst policy≤ 2 \sup 16 )*) 1446 ∀prefix : list (option Identifier×pseudo_instruction).(* 1447 x : (option Identifier×pseudo_instruction) 1448 tl : (list (option Identifier×pseudo_instruction)) 1449 prf : (program=prefix@[x]@tl) 1450 acc : 1451 (Σx0:ℕ×ppc_pc_map 1452 .(let 〈added,policy〉 ≝x0 in 1453 not_jump_default prefix policy 1454 ∧\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) (\snd policy) 1455 〈O,short_jump〉) 1456 =O 1457 ∧\fst policy 1458 =\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (prefix)) 1459 (\snd policy) 〈O,short_jump〉) 1460 ∧jump_increase prefix old_sigma policy 1461 ∧sigma_compact_unsafe prefix labels policy 1462 ∧(sigma_jump_equal prefix old_sigma policy→added=O) 1463 ∧(added=O→sigma_pc_equal prefix old_sigma policy) 1464 ∧out_of_program_none prefix policy 1465 ∧\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (prefix)) 1466 (\snd policy) 〈O,short_jump〉) 1467 =\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (prefix)) 1468 (\snd old_sigma) 〈O,short_jump〉) 1469 +added 1470 ∧sigma_safe prefix labels added old_sigma policy)) 1471 inc_added : ℕ 1472 inc_pc_sigma : ppc_pc_map 1473 p : (acc≃〈inc_added,inc_pc_sigma〉)*) 1474 ∀label : option Identifier. 1475 ∀instr : pseudo_instruction.(* 1476 p1 : (x≃〈label,instr〉) 1477 add_instr ≝ 1478 match instr 1479 in pseudo_instruction 1480 return λ_:pseudo_instruction.(option jump_length) 1481 with 1482 [Instruction (i:(preinstruction Identifier))⇒ 1483 jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added 1484 (prefix) i 1485 Comment (_:String)⇒None jump_length 1486 Cost (_:costlabel)⇒None jump_length 1487 Jmp (j:Identifier)⇒ 1488 Some jump_length 1489 (select_jump_length labels old_sigma inc_pc_sigma inc_added (prefix) j) 1490 Call (c:Identifier)⇒ 1491 Some jump_length 1492 (select_call_length labels old_sigma inc_pc_sigma inc_added (prefix) c) 1493 Mov (_:[[dptr]]) (_0:Identifier)⇒None jump_length] 1494 inc_pc : ℕ 1495 inc_sigma : (BitVectorTrie (ℕ×jump_length) 16) 1496 Hips : (inc_pc_sigma=〈inc_pc,inc_sigma〉) 1497 old_pc : ℕ 1498 old_length : jump_length 1499 Holdeq : 1500 (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (prefix)) (\snd old_sigma) 1501 〈O,short_jump〉 1502 =〈old_pc,old_length〉) 1503 Hpolicy : 1504 (not_jump_default prefix 〈inc_pc,inc_sigma〉 1505 ∧\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) inc_sigma 1506 〈O,short_jump〉) 1507 =O 1508 ∧inc_pc 1509 =\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (prefix)) inc_sigma 1510 〈O,short_jump〉) 1511 ∧jump_increase prefix old_sigma 〈inc_pc,inc_sigma〉 1512 ∧sigma_compact_unsafe prefix labels 〈inc_pc,inc_sigma〉 1513 ∧(sigma_jump_equal prefix old_sigma 〈inc_pc,inc_sigma〉→inc_added=O) 1514 ∧(inc_added=O→sigma_pc_equal prefix old_sigma 〈inc_pc,inc_sigma〉) 1515 ∧out_of_program_none prefix 〈inc_pc,inc_sigma〉 1516 ∧\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (prefix)) inc_sigma 1517 〈O,short_jump〉) 1518 =old_pc+inc_added 1519 ∧sigma_safe prefix labels inc_added old_sigma 〈inc_pc,inc_sigma〉)*) 1520 ∀added : ℕ. 1521 ∀policy : ppc_pc_map.(* 1522 new_length : jump_length 1523 isize : ℕ 1524 Heq1 : 1525 (match 1526 match instr 1527 in pseudo_instruction 1528 return λ_:pseudo_instruction.(option jump_length) 1529 with 1530 [Instruction (i:(preinstruction Identifier))⇒ 1531 jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added 1532 (prefix) i 1533 Comment (_:String)⇒None jump_length 1534 Cost (_:costlabel)⇒None jump_length 1535 Jmp (j:Identifier)⇒ 1536 Some jump_length 1537 (select_jump_length labels old_sigma inc_pc_sigma inc_added (prefix) j) 1538 Call (c:Identifier)⇒ 1539 Some jump_length 1540 (select_call_length labels old_sigma inc_pc_sigma inc_added (prefix) c) 1541 Mov (_:[[dptr]]) (_0:Identifier)⇒None jump_length] 1542 in option 1543 return λ_0:(option jump_length).(jump_length×ℕ) 1544 with 1545 [None⇒〈short_jump,instruction_size_jmplen short_jump instr〉 1546 Some (pl:jump_length)⇒ 1547 〈max_length old_length pl, 1548 instruction_size_jmplen (max_length old_length pl) instr〉] 1549 =〈new_length,isize〉) 1550 prefix_ok1 : (S (prefix)< 2 \sup 16 ) 1551 prefix_ok : (prefix< 2 \sup 16 ) 1552 Heq2a : 1553 (match 1554 match instr 1555 in pseudo_instruction 1556 return λ_0:pseudo_instruction.(option jump_length) 1557 with 1558 [Instruction (i:(preinstruction Identifier))⇒ 1559 jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added 1560 (prefix) i 1561 Comment (_0:String)⇒None jump_length 1562 Cost (_0:costlabel)⇒None jump_length 1563 Jmp (j:Identifier)⇒ 1564 Some jump_length 1565 (select_jump_length labels old_sigma inc_pc_sigma inc_added (prefix) j) 1566 Call (c:Identifier)⇒ 1567 Some jump_length 1568 (select_call_length labels old_sigma inc_pc_sigma inc_added (prefix) c) 1569 Mov (_0:[[dptr]]) (_00:Identifier)⇒None jump_length] 1570 in option 1571 return λ_0:(option jump_length).ℕ 1572 with 1573 [None⇒inc_added 1574 Some (x0:jump_length)⇒ 1575 inc_added+(isizeinstruction_size_jmplen old_length instr)] 1576 =added) 1577 Heq2b : 1578 (〈inc_pc+isize, 1579 insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (prefix))) 1580 〈inc_pc+isize, 1581 \snd (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (prefix))) 1582 (\snd old_sigma) 〈O,short_jump〉)〉 1583 (insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (prefix)) 1584 〈inc_pc,new_length〉 inc_sigma)〉 1585 =policy) 1586 *) 1587 sigma_safe (prefix@[〈label,instr〉]) labels added old_sigma policy. 1588 cases daemon(* 1589 #i >append_length >commutative_plus #Hi normalize in Hi; 1102 1590 elim (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi 1103 1591 [ >nth_append_first [2: @Hi] … … 1117 1605 #Hind #dest #Hj lapply (Hind dest Hj) Hind Hj lapply (proj1 ?? (pair_destruct ?????? Heq2)) cases instr 1118 1606 [2,3,6: [3: #x] #y normalize nodelta #EQ <EQ cases j normalize nodelta 1119 [1,4,7: *) 1120 1121 ] 1607 [1,4,7: 1608 *) 1609 qed. 1610 1611 (* One step in the search for a jump expansion fixpoint. *) 1612 definition jump_expansion_step: ∀program:(Σl:list labelled_instruction. 1613 S (l) < 2^16 ∧ is_well_labelled_p l). 1614 ∀labels:(Σlm:label_map.∀l. 1615 occurs_exactly_once ?? l program → 1616 bitvector_of_nat ? (lookup_def … lm l 0) = 1617 address_of_word_labels_code_mem program l). 1618 ∀old_policy:(Σpolicy:ppc_pc_map. 1619 (* out_of_program_none program policy *) 1620 And (And (And (And (not_jump_default program policy) 1621 (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd policy) 〈0,short_jump〉) = 0)) 1622 (\fst policy = \fst (bvt_lookup … (bitvector_of_nat ? (program)) (\snd policy) 〈0,short_jump〉))) 1623 (sigma_compact_unsafe program labels policy)) 1624 (\fst policy ≤ 2^16)). 1625 (Σx:bool × (option ppc_pc_map). 1626 let 〈no_ch,y〉 ≝ x in 1627 match y with 1628 [ None ⇒ nec_plus_ultra program old_policy 1629  Some p ⇒ And (And (And (And (And (And (And 1630 (not_jump_default program p) 1631 (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd p) 〈0,short_jump〉) = 0)) 1632 (\fst p = \fst (bvt_lookup … (bitvector_of_nat ? (program)) (\snd p) 〈0,short_jump〉))) 1633 (jump_increase program old_policy p)) 1634 (sigma_compact_unsafe program labels p)) 1635 (sigma_jump_equal program old_policy p → no_ch = true)) 1636 (no_ch = true → sigma_pc_equal program old_policy p)) 1637 (\fst p ≤ 2^16) 1638 ]) 1639 ≝ 1640 λprogram.λlabels.λold_sigma. 1641 let 〈final_added, final_policy〉 ≝ 1642 pi1 ?? (foldl_strong (option Identifier × pseudo_instruction) 1643 (λprefix.Σx:ℕ × ppc_pc_map. 1644 let 〈added,policy〉 ≝ x in 1645 And (And (And (And (And (And (And (And (And (not_jump_default prefix policy) 1646 (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd policy) 〈0,short_jump〉) = 0)) 1647 (\fst policy = \fst (bvt_lookup … (bitvector_of_nat ? (prefix)) (\snd policy) 〈0,short_jump〉))) 1648 (jump_increase prefix old_sigma policy)) 1649 (sigma_compact_unsafe prefix labels policy)) 1650 (sigma_jump_equal prefix old_sigma policy → added = 0)) 1651 (added = 0 → sigma_pc_equal prefix old_sigma policy)) 1652 (out_of_program_none prefix policy)) 1653 (\fst (bvt_lookup … (bitvector_of_nat ? (prefix)) (\snd policy) 〈0,short_jump〉) = 1654 \fst (bvt_lookup … (bitvector_of_nat ? (prefix)) (\snd old_sigma) 〈0,short_jump〉) + added)) 1655 (sigma_safe prefix labels added old_sigma policy)) 1656 program 1657 (λprefix.λx.λtl.λprf.λacc. 1658 let 〈inc_added, inc_pc_sigma〉 ≝ (pi1 ?? acc) in 1659 let 〈label,instr〉 ≝ x in 1660 (* Now, we must add the current ppc and its pc translation. 1661 * Three possibilities: 1662 *  Instruction is not a jump; i.e. constant size whatever the sigma we use; 1663 *  Instruction is a backward jump; we can use the sigma we're constructing, 1664 * since it will already know the translation of its destination; 1665 *  Instruction is a forward jump; we must use the old sigma (the new sigma 1666 * does not know the translation yet), but compensate for the jumps we 1667 * have lengthened. 1668 *) 1669 let add_instr ≝ match instr with 1670 [ Jmp j ⇒ Some ? (select_jump_length labels old_sigma inc_pc_sigma inc_added (prefix) j) 1671  Call c ⇒ Some ? (select_call_length labels old_sigma inc_pc_sigma inc_added (prefix) c) 1672  Instruction i ⇒ jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added (prefix) i 1673  _ ⇒ None ? 1674 ] in 1675 let 〈inc_pc, inc_sigma〉 ≝ inc_pc_sigma in 1676 let old_length ≝ 1677 \snd (bvt_lookup … (bitvector_of_nat ? (prefix)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) in 1678 let old_size ≝ instruction_size_jmplen old_length instr in 1679 let 〈new_length, isize〉 ≝ match add_instr with 1680 [ None ⇒ 〈short_jump, instruction_size_jmplen short_jump instr〉 1681  Some pl ⇒ 〈max_length old_length pl, instruction_size_jmplen (max_length old_length pl) instr〉 1682 ] in 1683 let new_added ≝ match add_instr with 1684 [ None ⇒ inc_added 1685  Some x ⇒ plus inc_added (minus isize old_size) 1686 ] in 1687 let old_Slength ≝ 1688 \snd (bvt_lookup … (bitvector_of_nat ? (S (prefix))) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) in 1689 let updated_sigma ≝ 1690 (* we add the new PC to the next position and the new jump length to this one *) 1691 bvt_insert … (bitvector_of_nat ? (S (prefix))) 〈inc_pc + isize, old_Slength〉 1692 (bvt_insert … (bitvector_of_nat ? (prefix)) 〈inc_pc, new_length〉 inc_sigma) in 1693 〈new_added, 〈plus inc_pc isize, updated_sigma〉〉 1694 ) 〈0, 〈0, 1695 bvt_insert … 1696 (bitvector_of_nat ? 0) 1697 〈0, \snd (bvt_lookup … (bitvector_of_nat ? 0) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉)〉 1698 (Stub ??)〉〉 1699 ) in 1700 if gtb (\fst final_policy) 2^16 then 1701 〈eqb final_added 0, None ?〉 1702 else 1703 〈eqb final_added 0, Some ? final_policy〉. 1704 [ normalize nodelta @nmk #Habs lapply p p cases (foldl_strong ? (λ_.Σx.?) ???) 1705 #x #H #Heq >Heq in H; normalize nodelta Heq x #Hind 1706 (* USE: inc_pc = fst of policy (from fold) *) 1707 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))))))) in p1; 1708 (* USE: fst policy < 2^16, inc_pc = fst of policy (old_sigma) *) 1709 lapply (proj2 ?? (pi2 ?? old_sigma)) >(proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) 1710 #Hsig #Hge 1711 (* USE: added = 0 → policy_pc_equal (from fold) *) 1712 lapply ((proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))) ? (program) (le_n (program))) 1713 [ (* USE: policy_jump_equal → added = 0 (from fold) *) 1714 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind))))) #i #Hi 1715 inversion (is_jump (\snd (nth i ? program 〈None ?, Comment []〉))) 1716 [ #Hj 1717 (* USE: policy_increase (from fold) *) 1718 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))))) i (le_S_to_le … Hi)) 1719 lapply (Habs i Hi ?) [ >Hj %] 1720 cases (bvt_lookup … (bitvector_of_nat ? i) (\snd old_sigma) 〈0,short_jump〉) 1721 #opc #oj 1722 cases (bvt_lookup … (bitvector_of_nat ? i) (\snd final_policy) 〈0,short_jump〉) 1723 #pc #j normalize nodelta #Heq >Heq cases j 1724 [1,2: #abs cases abs #abs2 try (cases abs2) @refl 1725 3: #_ @refl 1726 ] 1727  #Hnj 1728 (* USE: not_jump_default (from fold and old_sigma) *) 1729 >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))))))) i Hi ?) 1730 [2: >Hnj %] 1731 >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) i Hi ?) try % 1732 >Hnj % 1733 ] 1734  #abs >abs in Hsig; #Hsig 1735 @(absurd ? Hsig) @lt_to_not_le @ltb_true_to_lt @Hge 1736 ] 1737  normalize nodelta lapply p p cases (foldl_strong ? (λ_.Σx.?)???) in ⊢ (% → ?); #x #H #H2 1738 >H2 in H; normalize nodelta H2 x #H @conj 1739 [ @conj [ @conj 1740 [ (* USE[pass]: not_jump_default, 0 ↦ 0, inc_pc = fst policy, 1741 * jump_increase, sigma_compact_unsafe (from fold) *) 1742 @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))) 1743  #H2 (* USE[pass]: sigma_jump_equal → added = 0 (from fold) *) 1744 @eq_to_eqb_true @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))) @H2 1745 ] 1746  (* USE[pass]: added = 0 → sigma_pc_equal (from fold) *) 1747 #H2 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) @eqb_true_to_eq @H2 1748 ] 1749  @not_lt_to_le @ltb_false_to_not_lt @p1 1750 ] 1751 4: lapply (pi2 ?? acc) >p lapply (refl ? (inc_pc_sigma)) cases inc_pc_sigma in ⊢ (???% → %); 1752 #inc_pc #inc_sigma #Hips 1753 inversion (bvt_lookup … (bitvector_of_nat ? (prefix)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) 1754 #old_pc #old_length #Holdeq #Hpolicy normalize nodelta in Hpolicy; @pair_elim 1755 #added #policy normalize nodelta @pair_elim #new_length #isize normalize nodelta 1756 #Heq1 #Heq2 1757 cut (S (prefix) < 2^16) 1758 [ @(transitive_lt … (proj1 … (pi2 ?? program))) @le_S_S >prf >append_length 1759 <plus_n_Sm @le_S_S @le_plus_n_r ] #prefix_ok1 1760 cut (prefix < 2^16) [ @(transitive_lt … prefix_ok1) %] #prefix_ok 1761 cases (pair_destruct ?????? Heq2) Heq2 #Heq2a #Heq2b 1762 % [ % [ % [ % [ % [ % [ % [ % [ % ]]]]]]]] 1763 (* NOTE: to save memory and speed up work, there's cases daemon here. They can be 1764 * commented out for full proofs, but this needs a lot of memory and time *) 1765 [ (* not_jump_default *) 1766 @(jump_expansion_step1 … Heq1 Heq2b) try assumption 1767 @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))) 1768  (* 0 ↦ 0 *) 1769 @(jump_expansion_step2 … Heq2b) try assumption 1770 [ @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))) 1771  @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) ] 1772  (* inc_pc = fst of policy *) 1773 <Heq2b >append_length >(commutative_plus (prefix)) >lookup_insert_hit @refl 1774  (* jump_increase *) 1775 @(jump_expansion_step3 … (pi1 ?? old_sigma) … prf … p1 ??? old_length Holdeq 1776 … Heq1 prefix_ok1 prefix_ok Heq2b) 1777 try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) 1778 cases (pi2 … old_sigma) * * * #H #_ #_ #_ #_ @H 1779  (* sigma_compact_unsafe *) 1780 @(jump_expansion_step4 … Heq1 … Heq2b) try assumption 1781 try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) 1782 try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))) 1783 @(proj2 ?? (proj1 ?? (proj1 ?? Hpolicy))) 1784  (* policy_jump_equal → added = 0 *) 1785 @(jump_expansion_step5 … Holdeq … Heq1 … Heq2b) try assumption 1786 try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) 1787 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) 1788  (* added = 0 → policy_pc_equal *) cases daemon (* 1789 @(jump_expansion_step6 … Heq1 … Heq2b) try assumption 1790 try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) 1791 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) 1792 *) 1793  (* out_of_program_none *) cases daemon(* 1794 @jump_expansion_step7 try assumption 1795 @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))))) 1796 *) 1797  (* lookup p = lookup old_sigma + added *) cases daemon(* 1798 @jump_expansion_step8 try assumption 1799 try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) 1800 @(proj2 ?? (proj1 ?? Hpolicy)) *) 1801  (* sigma_safe *) cases daemon (* 1802 @jump_expansion_step9 try assumption 1803 @(proj2 ?? Hpolicy) *) 1804 ] 1122 1805  normalize nodelta % [ % [ % [ % [ % [ % [ % [ % [ % ]]]]]]]] 1123 1806 [ #i cases i
Note: See TracChangeset
for help on using the changeset viewer.