 Timestamp:
 Jul 23, 2012, 9:22:02 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/PolicyFront.ma
r2225 r2235 140 140 qed. 141 141 142 definition strip_target: 143 preinstruction Identifier → 144 ([[relative]] → preinstruction [[relative]]) ⊎ instruction ≝ 145 λi. 146 match i with 147 [ JC _ ⇒ inl … (JC ?) 148  JNC _ ⇒ inl … (JNC ?) 149  JB baddr _ ⇒ inl … (JB ? baddr) 150  JZ _ ⇒ inl … (JZ ?) 151  JNZ _ ⇒ inl … (JNZ ?) 152  JBC baddr _ ⇒ inl … (JBC ? baddr) 153  JNB baddr _ ⇒ inl … (JNB ? baddr) 154  CJNE addr _ ⇒ inl … (CJNE ? addr) 155  DJNZ addr _ ⇒ inl … (DJNZ ? addr) 156  ADD arg1 arg2 ⇒ inr … (ADD ? arg1 arg2) 157  ADDC arg1 arg2 ⇒ inr … (ADDC ? arg1 arg2) 158  SUBB arg1 arg2 ⇒ inr … (SUBB ? arg1 arg2) 159  INC arg ⇒ inr … (INC ? arg) 160  DEC arg ⇒ inr … (DEC ? arg) 161  MUL arg1 arg2 ⇒ inr … (MUL ? arg1 arg2) 162  DIV arg1 arg2 ⇒ inr … (DIV ? arg1 arg2) 163  DA arg ⇒ inr … (DA ? arg) 164  ANL arg ⇒ inr … (ANL ? arg) 165  ORL arg ⇒ inr … (ORL ? arg) 166  XRL arg ⇒ inr … (XRL ? arg) 167  CLR arg ⇒ inr … (CLR ? arg) 168  CPL arg ⇒ inr … (CPL ? arg) 169  RL arg ⇒ inr … (RL ? arg) 170  RR arg ⇒ inr … (RR ? arg) 171  RLC arg ⇒ inr … (RLC ? arg) 172  RRC arg ⇒ inr … (RRC ? arg) 173  SWAP arg ⇒ inr … (SWAP ? arg) 174  MOV arg ⇒ inr … (MOV ? arg) 175  MOVX arg ⇒ inr … (MOVX ? arg) 176  SETB arg ⇒ inr … (SETB ? arg) 177  PUSH arg ⇒ inr … (PUSH ? arg) 178  POP arg ⇒ inr … (POP ? arg) 179  XCH arg1 arg2 ⇒ inr … (XCH ? arg1 arg2) 180  XCHD arg1 arg2 ⇒ inr … (XCHD ? arg1 arg2) 181  RET ⇒ inr … (RET ?) 182  RETI ⇒ inr … (RETI ?) 183  NOP ⇒ inr … (RealInstruction (NOP ?)) 184 ]. 185 142 186 definition expand_relative_jump_unsafe: 143 187 jump_length → preinstruction Identifier → list instruction ≝ 144 188 λjmp_len:jump_length.λi. 145 match i with 146 [ JC jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JC ?) 147  JNC jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JNC ?) 148  JB baddr jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JB ? baddr) 149  JZ jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JZ ?) 150  JNZ jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JNZ ?) 151  JBC baddr jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JBC ? baddr) 152  JNB baddr jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JNB ? baddr) 153  CJNE addr jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (CJNE ? addr) 154  DJNZ addr jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (DJNZ ? addr) 155  ADD arg1 arg2 ⇒ [ ADD ? arg1 arg2 ] 156  ADDC arg1 arg2 ⇒ [ ADDC ? arg1 arg2 ] 157  SUBB arg1 arg2 ⇒ [ SUBB ? arg1 arg2 ] 158  INC arg ⇒ [ INC ? arg ] 159  DEC arg ⇒ [ DEC ? arg ] 160  MUL arg1 arg2 ⇒ [ MUL ? arg1 arg2 ] 161  DIV arg1 arg2 ⇒ [ DIV ? arg1 arg2 ] 162  DA arg ⇒ [ DA ? arg ] 163  ANL arg ⇒ [ ANL ? arg ] 164  ORL arg ⇒ [ ORL ? arg ] 165  XRL arg ⇒ [ XRL ? arg ] 166  CLR arg ⇒ [ CLR ? arg ] 167  CPL arg ⇒ [ CPL ? arg ] 168  RL arg ⇒ [ RL ? arg ] 169  RR arg ⇒ [ RR ? arg ] 170  RLC arg ⇒ [ RLC ? arg ] 171  RRC arg ⇒ [ RRC ? arg ] 172  SWAP arg ⇒ [ SWAP ? arg ] 173  MOV arg ⇒ [ MOV ? arg ] 174  MOVX arg ⇒ [ MOVX ? arg ] 175  SETB arg ⇒ [ SETB ? arg ] 176  PUSH arg ⇒ [ PUSH ? arg ] 177  POP arg ⇒ [ POP ? arg ] 178  XCH arg1 arg2 ⇒ [ XCH ? arg1 arg2 ] 179  XCHD arg1 arg2 ⇒ [ XCHD ? arg1 arg2 ] 180  RET ⇒ [ RET ? ] 181  RETI ⇒ [ RETI ? ] 182  NOP ⇒ [ RealInstruction (NOP ?) ] 183 ]. 184 185 definition instruction_size_jmplen: 186 jump_length → pseudo_instruction → ℕ ≝ 189 match strip_target i with 190 [ inl jmp ⇒ expand_relative_jump_internal_unsafe jmp_len jmp 191  inr instr ⇒ [ instr ] ]. 192 193 definition expand_pseudo_instruction_unsafe: 194 jump_length → pseudo_instruction → list instruction ≝ 187 195 λjmp_len. 188 196 λi. 189 let pseudos ≝match i with197 match i with 190 198 [ Cost cost ⇒ [ ] 191 199  Comment comment ⇒ [ ] … … 205 213  long_jump ⇒ [ LJMP (ADDR16 (zero 16)) ] 206 214 ] 207 ] in 208 let mapped ≝ map ? ? assembly1 pseudos in 215 ]. 216 % 217 qed. 218 219 definition instruction_size_jmplen: 220 jump_length → pseudo_instruction → ℕ ≝ 221 λjmp_len. 222 λi. 223 let mapped ≝ map ? ? assembly1 (expand_pseudo_instruction_unsafe jmp_len i) in 209 224 let flattened ≝ flatten ? mapped in 210 225 let pc_len ≝ length ? flattened in 211 226 pc_len. 212 @I.213 qed.214 227 215 228 definition sigma_compact_unsafe ≝ … … 625 638 #Hsafe #Hcp_unsafe #i #Hi 626 639 lapply (Hcp_unsafe i Hi) lapply (Hsafe i Hi) 627 lapply (refl ? (lookup_opt … (bitvector_of_nat ? i) (\snd sigma))) 628 cases (lookup_opt … (bitvector_of_nat ? i) (\snd sigma)) in ⊢ (???% → %); 640 inversion (lookup_opt … (bitvector_of_nat ? i) (\snd sigma)) 629 641 [ / by / 630 642  #x cases x x #x1 #x2 #EQ … … 632 644 [ / by / 633 645  #y cases y y #y1 #y2 normalize nodelta #H #H2 646 (*CSC: make a lemma here; to shorten the proof, reimplement the 647 safe case so that it also does a pattern matching on the jump_length 648 type *) 634 649 cut (instruction_size_jmplen x2 635 650 (\snd (nth i ? program 〈None ?, Comment []〉)) = … … 641 656 whd in match (assembly_1_pseudoinstruction …); 642 657 whd in match (expand_pseudo_instruction …); 643 normalize nodelta whd in match (append …) in H; 644 lapply (refl ? (nth i ? program 〈None ?, Comment []〉)) lapply H 645 cases (nth i ? program 〈None ?,Comment []〉) in ⊢ (% → ???% → %); 658 normalize nodelta whd in match (append …) in H; lapply H 659 inversion (nth i ? program 〈None ?,Comment []〉) 646 660 #lbl #instr cases instr 647 661 [2,3,6: #x [3: #y] normalize nodelta #H #_ % 648 4,5: #x >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) #H j #Heq662 4,5: #x >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) #Heq #Hj 649 663 lapply (Hj x (refl ? x)) Hj normalize nodelta 650 664 >add_bitvector_of_nat_plus <(plus_n_Sm i 0) <plus_n_O … … 679 693 ] 680 694 ] 681 2, 5: whd in match short_jump_cond; whd in match absolute_jump_cond;695 2,3,5,6: whd in match short_jump_cond; whd in match absolute_jump_cond; 682 696 cut (lookup_def ?? (create_label_map program) x 0 ≤ (program)) 683 [1,3 : cases (create_label_map program) #clm #Hclm697 [1,3,5,7: cases (create_label_map program) #clm #Hclm 684 698 @le_S_to_le @(proj2 ?? (Hclm x ?)) 685 [1 : @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (Jmp x) ??)686  2: @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (Call x) ??)]687 [1,4 : >nat_of_bitvector_bitvector_of_nat_inverse688 [2,4 : @(transitive_lt … (proj1 ?? Hprogram)) @le_S] @Hi689 2,5 : whd in match fetch_pseudo_instruction; normalize nodelta699 [1,2: @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (Jmp x) ??) 700 3,4: @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (Call x) ??)] 701 [1,4,7,10: >nat_of_bitvector_bitvector_of_nat_inverse 702 [2,4,6,8: @(transitive_lt … (proj1 ?? Hprogram)) @le_S] @Hi 703 2,5,8,11: whd in match fetch_pseudo_instruction; normalize nodelta 690 704 >nth_safe_nth 691 [1,3 : >nat_of_bitvector_bitvector_of_nat_inverse692 [1,3 : >Heq / by refl/693  2,4: @(transitive_lt … (proj1 ?? Hprogram)) @le_S @Hi705 [1,3,5,7: >nat_of_bitvector_bitvector_of_nat_inverse 706 [1,3,5,7: >Heq / by refl/ 707 *: @(transitive_lt … (proj1 ?? Hprogram)) @le_S @Hi 694 708 ] 695 709 ] 696  3,6: / by /710 *: / by / 697 711 ] 698  2,4: #H >(le_to_leb_true … H) normalize nodelta <plus_n_O712 *: #H >(le_to_leb_true … H) normalize nodelta <plus_n_O 699 713 normalize nodelta cases (vsplit bool 5 11 ?) #addr1 #addr2 700 714 cases (vsplit bool 5 11 ?) #pc1 #pc2 normalize nodelta … … 703 717 cases (vsplit bool 9 7 result) #upper #lower normalize nodelta 704 718 cases (get_index' bool 2 0 flags) normalize nodelta 705 #H >(proj2 ?? (proj1 ?? H)) >(proj1 ?? (proj1 ?? H)) normalize nodelta @refl 706 ] 707 3,6: whd in match short_jump_cond; whd in match absolute_jump_cond; 708 cut (lookup_def ?? (create_label_map program) x 0 ≤ (program)) 709 [1,3: cases (create_label_map program) #clm #Hclm 710 @le_S_to_le @(proj2 ?? (Hclm x ?)) 711 [1: @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (Jmp x) ??) 712 2: @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (Call x) ??)] 713 [1,4: >nat_of_bitvector_bitvector_of_nat_inverse 714 [2,4: @(transitive_lt … (proj1 ?? Hprogram)) @le_S] @Hi 715 2,5: whd in match fetch_pseudo_instruction; normalize nodelta 716 >nth_safe_nth 717 [1,3: >nat_of_bitvector_bitvector_of_nat_inverse 718 [1,3: >Heq / by refl/ 719 2,4: @(transitive_lt … (proj1 ?? Hprogram)) @le_S @Hi 720 ] 721 ] 722 3,6: / by / 723 ] 724 2,4: #H >(le_to_leb_true … H) normalize nodelta <plus_n_O 725 cases (vsplit bool 5 11 ?) #addr1 #addr2 726 cases (vsplit bool 5 11 ?) #pc1 #pc2 normalize nodelta 727 cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false) 728 #result #flags normalize nodelta 729 cases (vsplit bool 9 7 result) #upper #lower normalize nodelta 730 cases (get_index' bool 2 0 flags) normalize nodelta 731 #H >(proj1 ?? H) >(proj2 ?? H) normalize nodelta @refl 732 ] 733 ] 734 1: cut (∀A,B,ab.fst A B ab = (let 〈a,b〉 ≝ ab in a)) 719 #H 720 [1,2,5,6: >(proj2 ?? (proj1 ?? H)) >(proj1 ?? (proj1 ?? H)) normalize nodelta @refl 721 *: >(proj1 ?? H) >(proj2 ?? H) normalize nodelta @refl 722 ]]] 723 1: normalize nodelta 724 cut (∀A,B,ab.fst A B ab = (let 〈a,b〉 ≝ ab in a)) 735 725 [#A #B * / by refl/] #fst_foo 736 726 cut (∀x. … … 749 739  assumption ]] #lookup_in_program 750 740 H #pi cases pi 751 try (#y #x #H #Heq) try (#x #H #Heq) try (#H #Heq) try %752 normalize nodelta >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) in H;741 try (#y #x #Heq #H) try (#x #Heq #H) try (#Heq #H) try % lapply H H 742 normalize nodelta >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) 753 743 #Hj lapply (Hj x (refl ? x)) Hj 754 744 whd in match expand_relative_jump; normalize nodelta
Note: See TracChangeset
for help on using the changeset viewer.