Changeset 1493 for src/ASM/WellLabeled.ma
 Timestamp:
 Nov 4, 2011, 5:01:39 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/WellLabeled.ma
r1487 r1493 3 3 include "ASM/Arithmetic.ma". 4 4 5 let rec member_p 6 (a: Type[0]) (eq: a → a → bool) (element: a) (the_list: list a) 7 on the_list: Prop ≝ 8 match the_list with 9 [ nil ⇒ False 10  cons hd tl ⇒ 11 match eq hd element with 12 [ true ⇒ True 13  false ⇒ member_p … eq element tl 14 ] 15 ]. 16 5 17 definition well_labelled_p ≝ 6 18 ∀pc: Word. 19 ∀dptr: Word. 20 ∀acc_a: Byte. 21 ∀function_locations: list Word. 7 22 ∀program: BitVectorTrie Byte 16. 8 23 ∀cost_labels. 9 24 let 〈instruction, newpc, cost〉 ≝ fetch program pc in 10 25 match instruction with 11 [ LCALL lcall ⇒ ? 12  ACALL acall ⇒ ? 26 [ LCALL lcall ⇒ 27 match lcall return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with 28 [ ADDR16 addr16 ⇒ λ_. member_p … (eq_bv …) addr16 function_locations 29  _ ⇒ λabsurd. ⊥ 30 ] (subaddressing_modein … lcall) 31  ACALL acall ⇒ 32 match acall return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with 33 [ ADDR11 addr11 ⇒ λ_. 34 let 〈pc_bu, pc_bl〉 ≝ split … 8 8 pc in 35 let 〈thr, eig〉 ≝ split … 3 8 addr11 in 36 let 〈fiv, thr'〉 ≝ split … 5 3 pc_bu in 37 let new_pc ≝ (fiv @@ thr) @@ pc_bl in 38 match lookup_opt … new_pc cost_labels with 39 [ None ⇒ False 40  _ ⇒ True 41 ] 42  _ ⇒ λabsurd. ⊥ 43 ] (subaddressing_modein … acall) 13 44  AJMP ajmp ⇒ 14 45 match ajmp return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with … … 24 55  _ ⇒ True 25 56 ] 26  _ ⇒ λ _. ⊥57  _ ⇒ λabsurd. ⊥ 27 58 ] (subaddressing_modein … ajmp) 28 59  LJMP ljmp ⇒ … … 33 64  _ ⇒ True 34 65 ] 35  _ ⇒ λ _. ⊥66  _ ⇒ λabsurd. ⊥ 36 67 ] (subaddressing_modein … ljmp) 37 68  SJMP sjmp ⇒ … … 43 74  _ ⇒ True 44 75 ] 45  _ ⇒ λ _. ⊥76  _ ⇒ λabsurd. ⊥ 46 77 ] (subaddressing_modein … sjmp) 47  JMP jmp ⇒ ? 78  JMP jmp ⇒ 79 let big_acc_a ≝ (zero 8) @@ acc_a in 80 let 〈carry, jmp_addr〉 ≝ half_add … big_acc_a dptr in 81 let 〈carry, new_pc〉 ≝ half_add … pc jmp_addr in 82 match lookup_opt … new_pc cost_labels with 83 [ None ⇒ False 84  _ ⇒ True 85 ] 48 86  MOVC _ _ ⇒ True 49 87  RealInstruction instruction ⇒ 50 88 match instruction with 51 [ JZ jz ⇒ ? 52  _ ⇒ ? 89 [ JZ jz ⇒ 90 match jz return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with 91 [ RELATIVE rel ⇒ λ_. 92 let 〈carry, new_pc〉 ≝ half_add … pc (sign_extend 8 8 rel) in 93 match lookup_opt … new_pc cost_labels with 94 [ None ⇒ False 95  _ ⇒ True 96 ] 97  _ ⇒ λabsurd. ⊥ 98 ] (subaddressing_modein … jz) 99  JNZ jnz ⇒ 100 match jnz return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with 101 [ RELATIVE rel ⇒ λ_. 102 let 〈carry, new_pc〉 ≝ half_add … pc (sign_extend 8 8 rel) in 103 match lookup_opt … new_pc cost_labels with 104 [ None ⇒ False 105  _ ⇒ True 106 ] 107  _ ⇒ λabsurd. ⊥ 108 ] (subaddressing_modein … jnz) 109  JC jc ⇒ 110 match jc return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with 111 [ RELATIVE rel ⇒ λ_. 112 let 〈carry, new_pc〉 ≝ half_add … pc (sign_extend 8 8 rel) in 113 match lookup_opt … new_pc cost_labels with 114 [ None ⇒ False 115  _ ⇒ True 116 ] 117  _ ⇒ λabsurd. ⊥ 118 ] (subaddressing_modein … jc) 119  JNC jnc ⇒ 120 match jnc return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with 121 [ RELATIVE rel ⇒ λ_. 122 let 〈carry, new_pc〉 ≝ half_add … pc (sign_extend 8 8 rel) in 123 match lookup_opt … new_pc cost_labels with 124 [ None ⇒ False 125  _ ⇒ True 126 ] 127  _ ⇒ λabsurd. ⊥ 128 ] (subaddressing_modein … jnc) 129  JB baddr jb ⇒ 130 match jb return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with 131 [ RELATIVE rel ⇒ λ_. 132 let 〈carry, new_pc〉 ≝ half_add … pc (sign_extend 8 8 rel) in 133 match lookup_opt … new_pc cost_labels with 134 [ None ⇒ False 135  _ ⇒ True 136 ] 137  _ ⇒ λabsurd. ⊥ 138 ] (subaddressing_modein … jb) 139  JNB baddr jnb ⇒ 140 match jnb return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with 141 [ RELATIVE rel ⇒ λ_. 142 let 〈carry, new_pc〉 ≝ half_add … pc (sign_extend 8 8 rel) in 143 match lookup_opt … new_pc cost_labels with 144 [ None ⇒ False 145  _ ⇒ True 146 ] 147  _ ⇒ λabsurd. ⊥ 148 ] (subaddressing_modein … jnb) 149  JBC baddr jbc ⇒ 150 match jbc return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with 151 [ RELATIVE rel ⇒ λ_. 152 let 〈carry, new_pc〉 ≝ half_add … pc (sign_extend 8 8 rel) in 153 match lookup_opt … new_pc cost_labels with 154 [ None ⇒ False 155  _ ⇒ True 156 ] 157  _ ⇒ λabsurd. ⊥ 158 ] (subaddressing_modein … jbc) 159  CJNE args cjne ⇒ 160 match cjne return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with 161 [ RELATIVE rel ⇒ λ_. 162 let 〈carry, new_pc〉 ≝ half_add … pc (sign_extend 8 8 rel) in 163 match lookup_opt … new_pc cost_labels with 164 [ None ⇒ False 165  _ ⇒ True 166 ] 167  _ ⇒ λabsurd. ⊥ 168 ] (subaddressing_modein … cjne) 169  DJNZ args djnz ⇒ 170 match djnz return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with 171 [ RELATIVE rel ⇒ λ_. 172 let 〈carry, new_pc〉 ≝ half_add … pc (sign_extend 8 8 rel) in 173 match lookup_opt … new_pc cost_labels with 174 [ None ⇒ False 175  _ ⇒ True 176 ] 177  _ ⇒ λabsurd. ⊥ 178 ] (subaddressing_modein … djnz) 179  _ ⇒ True 53 180 ] 54 181 ]. 182 [*: normalize in absurd; // ] 183 qed.
Note: See TracChangeset
for help on using the changeset viewer.