Changeset 1905
 Timestamp:
 Apr 26, 2012, 5:15:06 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Assembly.ma
r1887 r1905 9 9 (**************************************** START OF POLICY ABSTRACTION ********************) 10 10 11 (* definition of & operations on jump length *)11 (* definition of & operations on jump length 12 12 inductive jump_length: Type[0] ≝ 13 13  short_jump: jump_length 14 14  medium_jump: jump_length 15  long_jump: jump_length. 15  long_jump: jump_length. *) 16 16 17 17 definition assembly_preinstruction ≝ … … 418 418 qed. 419 419 420 definition expand_relative_jump_internal_safe: 421 Word → jump_length → Word → ([[relative]] → preinstruction [[relative]]) → 422 option (list instruction) 420 definition expand_relative_jump_internal: 421 ∀lookup_labels:Identifier → Word.∀sigma:Word → Word. 422 Identifier → Word → ([[relative]] → preinstruction [[relative]]) → 423 list instruction 423 424 ≝ 424 λlookup_address,jmp_len.λpc,i. 425 match jmp_len with 426 [ short_jump ⇒ 427 let 〈result, flags〉 ≝ sub_16_with_carry pc lookup_address false in 428 let 〈upper, lower〉 ≝ split ? 8 8 result in 429 if eq_bv ? upper (zero 8) then 430 let address ≝ RELATIVE lower in 431 Some ? [ RealInstruction (i address) ] 432 else 433 None ? 434  medium_jump ⇒ None … 435  long_jump ⇒ 436 Some ? 425 λlookup_labels.λsigma.λlbl.λpc,i. 426 let lookup_address ≝ sigma (lookup_labels lbl) in 427 let 〈result, flags〉 ≝ sub_16_with_carry pc lookup_address false in 428 let 〈upper, lower〉 ≝ split ? 8 8 result in 429 if eq_bv ? upper (zero 8) then 430 let address ≝ RELATIVE lower in 431 [ RealInstruction (i address) ] 432 else 437 433 [ RealInstruction (i (RELATIVE (bitvector_of_nat ? 2))); 438 434 SJMP (RELATIVE (bitvector_of_nat ? 3)); (* LJMP size? *) 439 435 LJMP (ADDR16 lookup_address) 440 ] 441 ]. 436 ]. 442 437 @ I 443 438 qed. 444 439 445 definition rel_jump_length_ok ≝440 (*definition rel_jump_length_ok ≝ 446 441 λlookup_address:Word. 447 442 λpc:Word. … … 456 451 coercion eject_rel_jump_length nocomposites: 457 452 ∀x,y.∀pol:rel_jump_length_ok x y. jump_length ≝ 458 eject_rel_jump_length on _pol:(rel_jump_length_ok ??) to jump_length. 459 460 definition expand_relative_jump_internal: 461 ∀lookup_address:Word. ∀pc:Word. rel_jump_length_ok lookup_address pc → 462 ([[relative]] → preinstruction [[relative]]) → 453 eject_rel_jump_length on _pol:(rel_jump_length_ok ??) to jump_length.*) 454 455 (*definition expand_relative_jump_internal: 456 ∀lookup_address:Word. ∀pc:Word. ([[relative]] → preinstruction [[relative]]) → 463 457 list instruction 464 ≝ λlookup_address,pc, jump_len,i.465 match expand_relative_jump_internal_safe lookup_address jump_lenpc i458 ≝ λlookup_address,pc,i. 459 match expand_relative_jump_internal_safe lookup_address pc i 466 460 return λres. res ≠ None ? → ? 467 461 with … … 469 463  Some res ⇒ λ_.res ] (pi2 … jump_len i). 470 464 cases abs /2/ 471 qed. 472 473 definition expand_relative_jump_safe: ∀lookup_labels:Identifier → Word.Word → jump_length → preinstruction Identifier → option (list instruction) ≝ 474 λlookup_labels. 465 qed.*) 466 467 definition expand_relative_jump: 468 ∀lookup_labels.∀sigma. 469 Word → (*jump_length →*) 470 preinstruction Identifier → list instruction ≝ 471 λlookup_labels: Identifier → Word. 472 λsigma:Word → Word. 475 473 λpc: Word. 476 λjmp_len: jump_length.474 (*λjmp_len: jump_length.*) 477 475 λi: preinstruction Identifier. 478 476 let rel_jmp ≝ RELATIVE (bitvector_of_nat ? 2) in 479 477 match i with 480 [ JC jmp ⇒ expand_relative_jump_internal _safe (lookup_labels jmp) jmp_lenpc (JC ?)481  JNC jmp ⇒ expand_relative_jump_internal _safe (lookup_labels jmp) jmp_lenpc (JNC ?)482  JB baddr jmp ⇒ expand_relative_jump_internal _safe (lookup_labels jmp) jmp_lenpc (JB ? baddr)483  JZ jmp ⇒ expand_relative_jump_internal _safe (lookup_labels jmp) jmp_lenpc (JZ ?)484  JNZ jmp ⇒ expand_relative_jump_internal _safe (lookup_labels jmp) jmp_lenpc (JNZ ?)485  JBC baddr jmp ⇒ expand_relative_jump_internal _safe (lookup_labels jmp) jmp_lenpc (JBC ? baddr)486  JNB baddr jmp ⇒ expand_relative_jump_internal _safe (lookup_labels jmp) jmp_lenpc (JNB ? baddr)487  CJNE addr jmp ⇒ expand_relative_jump_internal _safe (lookup_labels jmp) jmp_lenpc (CJNE ? addr)488  DJNZ addr jmp ⇒ expand_relative_jump_internal _safe (lookup_labels jmp) jmp_lenpc (DJNZ ? addr)489  ADD arg1 arg2 ⇒ Some …[ ADD ? arg1 arg2 ]490  ADDC arg1 arg2 ⇒ Some …[ ADDC ? arg1 arg2 ]491  SUBB arg1 arg2 ⇒ Some …[ SUBB ? arg1 arg2 ]492  INC arg ⇒ Some …[ INC ? arg ]493  DEC arg ⇒ Some …[ DEC ? arg ]494  MUL arg1 arg2 ⇒ Some …[ MUL ? arg1 arg2 ]495  DIV arg1 arg2 ⇒ Some …[ DIV ? arg1 arg2 ]496  DA arg ⇒ Some …[ DA ? arg ]497  ANL arg ⇒ Some …[ ANL ? arg ]498  ORL arg ⇒ Some …[ ORL ? arg ]499  XRL arg ⇒ Some …[ XRL ? arg ]500  CLR arg ⇒ Some …[ CLR ? arg ]501  CPL arg ⇒ Some …[ CPL ? arg ]502  RL arg ⇒ Some …[ RL ? arg ]503  RR arg ⇒ Some …[ RR ? arg ]504  RLC arg ⇒ Some …[ RLC ? arg ]505  RRC arg ⇒ Some …[ RRC ? arg ]506  SWAP arg ⇒ Some …[ SWAP ? arg ]507  MOV arg ⇒ Some …[ MOV ? arg ]508  MOVX arg ⇒ Some …[ MOVX ? arg ]509  SETB arg ⇒ Some …[ SETB ? arg ]510  PUSH arg ⇒ Some …[ PUSH ? arg ]511  POP arg ⇒ Some …[ POP ? arg ]512  XCH arg1 arg2 ⇒ Some …[ XCH ? arg1 arg2 ]513  XCHD arg1 arg2 ⇒ Some …[ XCHD ? arg1 arg2 ]514  RET ⇒ Some …[ RET ? ]515  RETI ⇒ Some …[ RETI ? ]516  NOP ⇒ Some …[ RealInstruction (NOP ?) ]478 [ JC jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp pc (JC ?) 479  JNC jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp pc (JNC ?) 480  JB baddr jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp pc (JB ? baddr) 481  JZ jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp pc (JZ ?) 482  JNZ jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp pc (JNZ ?) 483  JBC baddr jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp pc (JBC ? baddr) 484  JNB baddr jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp pc (JNB ? baddr) 485  CJNE addr jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp pc (CJNE ? addr) 486  DJNZ addr jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp pc (DJNZ ? addr) 487  ADD arg1 arg2 ⇒ [ ADD ? arg1 arg2 ] 488  ADDC arg1 arg2 ⇒ [ ADDC ? arg1 arg2 ] 489  SUBB arg1 arg2 ⇒ [ SUBB ? arg1 arg2 ] 490  INC arg ⇒ [ INC ? arg ] 491  DEC arg ⇒ [ DEC ? arg ] 492  MUL arg1 arg2 ⇒ [ MUL ? arg1 arg2 ] 493  DIV arg1 arg2 ⇒ [ DIV ? arg1 arg2 ] 494  DA arg ⇒ [ DA ? arg ] 495  ANL arg ⇒ [ ANL ? arg ] 496  ORL arg ⇒ [ ORL ? arg ] 497  XRL arg ⇒ [ XRL ? arg ] 498  CLR arg ⇒ [ CLR ? arg ] 499  CPL arg ⇒ [ CPL ? arg ] 500  RL arg ⇒ [ RL ? arg ] 501  RR arg ⇒ [ RR ? arg ] 502  RLC arg ⇒ [ RLC ? arg ] 503  RRC arg ⇒ [ RRC ? arg ] 504  SWAP arg ⇒ [ SWAP ? arg ] 505  MOV arg ⇒ [ MOV ? arg ] 506  MOVX arg ⇒ [ MOVX ? arg ] 507  SETB arg ⇒ [ SETB ? arg ] 508  PUSH arg ⇒ [ PUSH ? arg ] 509  POP arg ⇒ [ POP ? arg ] 510  XCH arg1 arg2 ⇒ [ XCH ? arg1 arg2 ] 511  XCHD arg1 arg2 ⇒ [ XCHD ? arg1 arg2 ] 512  RET ⇒ [ RET ? ] 513  RETI ⇒ [ RETI ? ] 514  NOP ⇒ [ RealInstruction (NOP ?) ] 517 515 ]. 518 516 519 definition expand_pseudo_instruction_safe: 520 ∀lookup_labels,pc. jump_length → ? → pseudo_instruction → option (list instruction) ≝ 521 λlookup_labels. 517 definition expand_pseudo_instruction: 518 ∀lookup_labels.∀sigma.Word → ? → pseudo_instruction → list instruction ≝ 519 λlookup_labels:Identifier → Word. 520 λsigma:Word → Word. 522 521 λpc. 523 λjmp_len. 524 λlookup_datalabels. 522 λlookup_datalabels:Identifier → Word. 525 523 λi. 526 524 match i with 527 [ Cost cost ⇒ Some ?[ ]528  Comment comment ⇒ Some ?[ ]525 [ Cost cost ⇒ [ ] 526  Comment comment ⇒ [ ] 529 527  Call call ⇒ 530 match jmp_len with 531 [ short_jump ⇒ None ? 532  medium_jump ⇒ 533 let 〈ignore, address〉 ≝ split ? 5 11 (lookup_labels call) in 534 let 〈fst_5, rest〉 ≝ split ? 5 11 pc in 535 if eq_bv ? ignore fst_5 then 536 let address ≝ ADDR11 address in 537 Some ? ([ ACALL address ]) 538 else 539 None ? 540  long_jump ⇒ 528 let 〈ignore, address〉 ≝ split ? 5 11 (lookup_labels call) in 529 let 〈fst_5, rest〉 ≝ split ? 5 11 pc in 530 if eq_bv ? ignore fst_5 then 531 let address ≝ ADDR11 address in 532 [ ACALL address ] 533 else 541 534 let address ≝ ADDR16 (lookup_labels call) in 542 Some ? [ LCALL address ] 543 ] 535 [ LCALL address ] 544 536  Mov d trgt ⇒ 545 537 let address ≝ DATA16 (lookup_datalabels trgt) in 546 Some ?[ RealInstruction (MOV ? (inl ? ? (inl ? ? (inr ? ? 〈DPTR, address〉))))]547  Instruction instr ⇒ expand_relative_jump _safe lookup_labels pc jmp_leninstr538 [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inr ? ? 〈DPTR, address〉))))] 539  Instruction instr ⇒ expand_relative_jump lookup_labels sigma pc instr 548 540  Jmp jmp ⇒ 549 match jmp_len with 550 [ short_jump ⇒ 551 let 〈result, flags〉 ≝ sub_16_with_carry pc (lookup_labels jmp) false in 552 let 〈upper, lower〉 ≝ split ? 8 8 result in 553 if eq_bv ? upper (zero 8) then 554 let address ≝ RELATIVE lower in 555 Some ? [ SJMP address ] 556 else 557 None ? 558  medium_jump ⇒ 541 let 〈result, flags〉 ≝ sub_16_with_carry pc (lookup_labels jmp) false in 542 let 〈upper, lower〉 ≝ split ? 8 8 result in 543 if eq_bv ? upper (zero 8) then 544 let address ≝ RELATIVE lower in 545 [ SJMP address ] 546 else 559 547 let 〈fst_5_addr, rest_addr〉 ≝ split ? 5 11 (lookup_labels jmp) in 560 548 let 〈fst_5_pc, rest_pc〉 ≝ split ? 5 11 pc in 561 549 if eq_bv ? fst_5_addr fst_5_pc then 562 550 let address ≝ ADDR11 rest_addr in 563 Some ? ([ AJMP address ]) 564 else 565 None ? 566  long_jump ⇒ 551 [ AJMP address ] 552 else 567 553 let address ≝ ADDR16 (lookup_labels jmp) in 568 Some ? [ LJMP address ] 569 ] 554 [ LJMP address ] 570 555 ]. 571 556 @ I 572 557 qed. 573 558 559 (* 560 (*X? 574 561 definition jump_length_ok ≝ 575 562 λlookup_labels:Identifier → Word. … … 578 565 (* CSC,JPB: Cheating here, use Jaap's better definition select_reljump_length *) 579 566 ∀x,y.expand_pseudo_instruction_safe lookup_labels pc jump_len x y ≠ None ?. 567 *) 580 568 581 569 lemma eject_jump_length: ∀x,y. jump_length_ok x y → jump_length. … … 598 586 cases abs /2/ 599 587 qed. 600 588 *) 589 (*X? 601 590 definition policy_type ≝ 602 591 λlookup_labels:Identifier → Word. 603 592 ∀pc:Word. jump_length_ok lookup_labels pc. 604 605 definition policy_type2 ≝ 606 ∀lookup_labels.policy_type lookup_labels. 593 *) 594 595 (*definition policy_type2 ≝ 596 λprogram. 597 Σpol:Word → jump_length. 598 let lookup_labels ≝ 599 (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) in 600 ∀pc:Word. let jump_len ≝ pol pc in 601 ∀x,y.expand_pseudo_instruction_safe lookup_labels pc jump_len x y ≠ None ?.*) 607 602 608 603 definition assembly_1_pseudoinstruction ≝ 609 604 λlookup_labels. 610 λ jump_expansion: policy_type lookup_labels.605 λsigma. 611 606 (*λppc: Word.*) 612 607 λpc: Word. 613 608 λlookup_datalabels. 614 609 λi. 615 let expansion ≝ jump_expansion pc in 616 let pseudos ≝ expand_pseudo_instruction lookup_labels pc expansion lookup_datalabels i in 610 let pseudos ≝ expand_pseudo_instruction lookup_labels sigma pc lookup_datalabels i in 617 611 let mapped ≝ map ? ? assembly1 pseudos in 618 612 let flattened ≝ flatten ? mapped in … … 621 615 622 616 definition construct_costs ≝ 617 (*X?*)λlookup_labels. 618 λsigma. 623 619 λprogram_counter: nat. 624 λjump_expansion: policy_type (λx.bitvector_of_nat ? program_counter).625 620 λpseudo_program_counter: nat. 626 621 λcosts: BitVectorTrie costlabel 16. … … 635 630 let lookup_datalabels ≝ λx.zero ? in 636 631 let pc_delta_assembled ≝ 637 assembly_1_pseudoinstruction ( λx.pc_bv)638 jump_expansion(*ppc_bv*) pc_bv lookup_datalabels i in632 assembly_1_pseudoinstruction (*X?(λx.pc_bv)*) lookup_labels 633 sigma (*ppc_bv*) pc_bv lookup_datalabels i in 639 634 let 〈pc_delta, assembled〉 ≝ pc_delta_assembled in 640 635 〈pc_delta + program_counter, costs〉 … … 671 666 qed. 672 667 668 (* 673 669 (* This establishes the correspondence between pseudo program counters and 674 670 program counters. It is at the heart of the proof. *) 675 671 (*CSC: code taken from build_maps *) 676 definition sigma00: ∀jump_expansion:policy_type2.∀l:list labelled_instruction.? → 672 definition sigma00: 673 ∀jump_expansion:policy_type2.∀l:list labelled_instruction.? → 677 674 (Σppc_pc_map:ℕ×(ℕ×(BitVectorTrie Word 16)). 678 675 let 〈ppc,pc_map〉 ≝ ppc_pc_map in … … 686 683 bvt_lookup ?? (bitvector_of_nat 16 (S x)) sigma_map (zero ?) = 687 684 bitvector_of_nat 16 ((nat_of_bitvector ? pc_x) + 688 (\fst 689 (assembly_1_pseudoinstruction (λx.pc_x) (jump_expansion (λx.pc_x)) pc_x (λx.zero ?) pi))))) 690 ) ≝ 691 λjump_expansion: policy_type2. 685 (\fst (assembly_1_pseudoinstruction lookup_labels(*X?(λx.pc_x)*) (jump_expansion (*?(λx.pc_x)*)) pc_x 686 (λx.zero ?) pi))))) 687 ) ≝ 688 (*?*)λlookup_labels. 689 λjump_expansion(*X?: policy_type2*). 692 690 λl:list labelled_instruction. 693 691 λacc. … … 704 702 bvt_lookup ?? (bitvector_of_nat 16 (S x)) sigma_map (zero ?) = 705 703 bitvector_of_nat 16 ((nat_of_bitvector ? pc_x) + 706 (\fst (assembly_1_pseudoinstruction (λx.pc_x) (jump_expansion (λx.pc_x)) pc_x (λx.zero ?) pi)))))) 704 (\fst (assembly_1_pseudoinstruction (*X?(λx.pc_x)*)lookup_labels (jump_expansion (*X?(λx.pc_x)*)) pc_x 705 (λx.zero ?) pi)))))) 707 706 ) 708 707 l … … 711 710 let 〈program_counter, sigma_map〉 ≝ pc_map in 712 711 let 〈label, i〉 ≝ i in 713 let 〈pc,ignore〉 ≝ construct_costs program_counter (jump_expansion (λx.bitvector_of_nat ? program_counter)) ppc (Stub …) i in712 let 〈pc,ignore〉 ≝ construct_costs lookup_labels program_counter (jump_expansion (*X?(λx.bitvector_of_nat ? program_counter)*)) ppc (Stub …) i in 714 713 〈S ppc, 〈pc, insert ?? (bitvector_of_nat 16 (S ppc)) (bitvector_of_nat 16 pc) sigma_map〉〉 715 714 ) acc. … … 813 812 None ? 814 813 else 815 Some ? (λx. lookup … x sigma_map (zero …)). 814 Some ? (λx. lookup … x sigma_map (zero …)). *) 816 815 817 816 (* stuff about policy *) 818 817 819 definition policy_ok ≝ λjump_expansion,p. sigma_safe p jump_expansion ≠ None …. 820 821 definition policy ≝ λp. Σjump_expansion:policy_type2. policy_ok jump_expansion p. 822 823 lemma eject_policy: ∀p. policy p → policy_type2.818 (*definition policy_ok ≝ λjump_expansion,p. sigma_safe p jump_expansion ≠ None ….*) 819 820 (*definition policy ≝ λp. Σjump_expansion:policy_type2. policy_ok jump_expansion p.*) 821 822 (*lemma eject_policy: ∀p. policy p → policy_type2. 824 823 #p #pol @(pi1 … pol) 825 824 qed. … … 833 832  Some r ⇒ λ_.r] (pi2 … policy). 834 833 cases abs /2 by / 834 qed.*) 835 836 example half_add_SO: 837 ∀pc. 838 \snd (half_add 16 (bitvector_of_nat … pc) (bitvector_of_nat … 1)) = bitvector_of_nat … (S pc). 839 cases daemon. 835 840 qed. 836 841 837 842 (*CSC: Main axiom here, needs to be proved soon! *) 838 lemma snd_assembly_1_pseudoinstruction_ok:843 (*lemma snd_assembly_1_pseudoinstruction_ok: 839 844 ∀program:pseudo_assembly_program.∀pol: policy program. 840 845 ∀ppc:Word.∀pi,lookup_labels,lookup_datalabels. 841 846 lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) → 842 847 lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) → 848 (nat_of_bitvector 16 ppc) < \snd program → 843 849 \fst (fetch_pseudo_instruction (\snd program) ppc) = pi → 844 850 let len ≝ \fst (assembly_1_pseudoinstruction lookup_labels (pol lookup_labels) (sigma program pol ppc) lookup_datalabels pi) in 845 851 sigma program pol (\snd (half_add ? ppc (bitvector_of_nat ? 1))) = 846 852 bitvector_of_nat … (nat_of_bitvector … (sigma program pol ppc) + len). 847 #program #pol #ppc #pi #lookup_labels #lookup_datalabels #Hll #Hldl 848 whd in match (sigma ???); whd in match (sigma program pol (\snd (half_add ???))); 849 whd in match (sigma_safe program pol); whd in match (sigma0 program pol); 850 lapply (refl ? (pi1 ?? (sigma00 pol (\snd program) 851 «〈0, 〈0, (insert (BitVector 16) 16 (bitvector_of_nat 16 0) (bitvector_of_nat 16 0) (Stub (BitVector 16) 16))〉〉,?»))) 852 [ @conj 853 [ / by refl/ 854  #H >lookup_insert_hit @conj 855 [ @refl 856  #x #Hx @⊥ @(absurd … Hx) @le_to_not_lt @le_O_n 857 ] 858 ] 859  (* here we go *) cases daemon 860 ] 861 qed. 853 #program #pol #ppc #pi #lookup_labels #lookup_datalabels #Hll #Hldl #Hppc 854 lapply (refl … (sigma0 program pol)) whd in match (sigma0 ??) in ⊢ (??%? → ?); 855 cases (sigma00 ???) #x #Hpmap #EQ 856 whd in match (sigma ???); 857 whd in match (sigma program pol (\snd (half_add ???))); 858 whd in match sigma_safe; normalize nodelta 859 (*Problem1: backtracking cases (sigma0 program pol)*) 860 generalize in match (pi2 ???); whd in match policy_ok; normalize nodelta 861 whd in match sigma_safe; normalize nodelta <EQ cases x in Hpmap EQ; x #final_ppc #x 862 cases x x #final_pc #smap normalize nodelta #Hpmap #EQ #Heq #Hfetch cases (gtb final_pc (2^16)) in Heq; 863 normalize nodelta 864 [ #abs @⊥ @(absurd ?? abs) @refl 865  #_ lapply (proj1 ?? ((proj2 ?? Hpmap) (proj1 ?? Hpmap))) #Hpmap1 866 lapply ((proj2 ?? ((proj2 ?? Hpmap) (proj1 ?? Hpmap))) (nat_of_bitvector 16 ppc) Hppc) #Hpmap2 Hpmap 867 <(bitvector_of_nat_nat_of_bitvector 16 ppc) >half_add_SO 868 869 >(Hpmap2 ? (refl …)) @eq_f @eq_f2 [%] 870 >bitvector_of_nat_nat_of_bitvector 871 >Hfetch lapply Hfetch lapply pi 872 873 874 whd in match assembly_1_pseudoinstruction; normalize nodelta 862 875 863 example sigma_0: ∀p,pol. sigma p pol (bitvector_of_nat ? 0) = bitvector_of_nat ? 0. 876 qed.*) 877 878 879 (*example sigma_0: ∀p,pol. sigma p pol (bitvector_of_nat ? 0) = bitvector_of_nat ? 0. 864 880 cases daemon. 865 qed. 881 qed.*) 866 882 867 883 axiom fetch_pseudo_instruction_split: … … 1117 1133 1118 1134 definition build_maps0: 1119 ∀pseudo_program .∀pol:policy pseudo_program.1135 ∀pseudo_program:pseudo_assembly_program.∀sigma:Word → Word. 1120 1136 Σres:((identifier_map ASMTag Word) × (BitVectorTrie costlabel 16)). 1121 1137 let 〈labels, costs〉 ≝ res in 1122 1138 ∀id. occurs_exactly_once ?? id (\snd pseudo_program) → 1123 lookup_def … labels id (zero ?) = sigma pseudo_program pol(address_of_word_labels_code_mem (\snd pseudo_program) id) ≝1139 lookup_def … labels id (zero ?) = sigma (address_of_word_labels_code_mem (\snd pseudo_program) id) ≝ 1124 1140 λpseudo_program. 1125 λ pol:policy pseudo_program.1141 λsigma. 1126 1142 let result ≝ 1127 1143 foldl_strong … … 1132 1148 let 〈pc',costs〉 ≝ pc_costs in 1133 1149 And ( And ( 1134 And (bitvector_of_nat ? pc' = sigma pseudo_program pol(bitvector_of_nat ? ppc')) (*∧*)1150 And (bitvector_of_nat ? pc' = sigma (bitvector_of_nat ? ppc')) (*∧*) 1135 1151 (ppc' = length … pre)) (*∧ *) 1136 ( tech_pc_sigma00 pseudo_program (pi1 … pol) pre = 〈ppc',pc'〉)) (*∧*)1152 (*(tech_pc_sigma00 pseudo_program (pi1 … pol) pre = 〈ppc',pc'〉)*) True) (*∧*) 1137 1153 (∀id. occurs_exactly_once ?? id pre → 1138 lookup_def … labels id (zero …) = sigma pseudo_program pol(address_of_word_labels_code_mem pre id)))1154 lookup_def … labels id (zero …) = sigma (address_of_word_labels_code_mem pre id))) 1139 1155 (\snd pseudo_program) 1140 1156 (λprefix,i,tl,prf,t. … … 1151 1167 ] 1152 1168 in 1153 let construct ≝ construct_costs pc (pol (λx.bitvector_of_nat ? pc)) ppc costs i' in 1169 let construct ≝ construct_costs (λid.lookup_def … labels id (zero ?)) sigma 1170 pc ppc costs i' in 1154 1171 〈labels, 〈S ppc,construct〉〉) 〈empty_map …, 〈0, 〈0, Stub ? ?〉〉〉 1155 1172 in … … 1181 1198 1182 1199 definition build_maps: 1183 ∀pseudo_program. policy pseudo_program →1200 ∀pseudo_program.∀sigma. 1184 1201 (identifier_map ASMTag Word) × (BitVectorTrie costlabel 16) 1185 ≝ λpseudo_program, pol. build_maps0 pseudo_program pol.1202 ≝ λpseudo_program,sigma. build_maps0 pseudo_program sigma. 1186 1203 1187 1204 theorem build_maps_ok: 1188 ∀pseudo_program.∀ pol:policy pseudo_program.1189 let 〈labels, costs〉 ≝ build_maps pseudo_program polin1205 ∀pseudo_program.∀sigma:Word → Word. 1206 let 〈labels, costs〉 ≝ build_maps pseudo_program sigma in 1190 1207 ∀id. occurs_exactly_once ?? id (\snd pseudo_program) → 1191 lookup_def … labels id (zero ?) = sigma pseudo_program pol(address_of_word_labels_code_mem (\snd pseudo_program) id).1192 #pseudo_program # pol @(pi2 … (build_maps0 … pol))1208 lookup_def … labels id (zero ?) = sigma (address_of_word_labels_code_mem (\snd pseudo_program) id). 1209 #pseudo_program #sigma @(pi2 … (build_maps0 … sigma)) 1193 1210 qed. 1194 1211 1195 1212 definition assembly: 1196 ∀p:pseudo_assembly_program. policy p →list Byte × (BitVectorTrie costlabel 16) ≝1213 ∀p:pseudo_assembly_program.∀sigma:Word → Word.list Byte × (BitVectorTrie costlabel 16) ≝ 1197 1214 λp.let 〈preamble, instr_list〉 ≝ p in 1198 λ pol.1199 let 〈labels,costs〉 ≝ build_maps 〈preamble,instr_list〉 polin1215 λsigma. 1216 let 〈labels,costs〉 ≝ build_maps 〈preamble,instr_list〉 sigma in 1200 1217 let datalabels ≝ construct_datalabels preamble in 1201 1218 let lookup_labels ≝ λx. lookup_def … labels x (zero ?) in … … 1210 1227 let 〈pi,newppc〉 ≝ fetch_pseudo_instruction instr_list ppc' in 1211 1228 let 〈len,assembledi〉 ≝ 1212 assembly_1_pseudoinstruction lookup_labels (pol lookup_labels)ppc' lookup_datalabels pi in1229 assembly_1_pseudoinstruction lookup_labels sigma ppc' lookup_datalabels pi in 1213 1230 True) 1214 1231 instr_list … … 1216 1233 let 〈pc, ppc_code〉 ≝ pc_ppc_code in 1217 1234 let 〈ppc, code〉 ≝ ppc_code in 1218 let 〈pc_delta, program〉 ≝ assembly_1_pseudoinstruction lookup_labels (pol lookup_labels)ppc lookup_datalabels (\snd hd) in1235 let 〈pc_delta, program〉 ≝ assembly_1_pseudoinstruction lookup_labels sigma ppc lookup_datalabels (\snd hd) in 1219 1236 let 〈new_pc, flags〉 ≝ add_16_with_carry pc (bitvector_of_nat ? pc_delta) false in 1220 1237 let new_ppc ≝ \snd (half_add ? ppc (bitvector_of_nat ? 1)) in
Note: See TracChangeset
for help on using the changeset viewer.