Changeset 1495
 Timestamp:
 Nov 7, 2011, 3:45:18 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/ASMCosts.ma
r1486 r1495 25 25 qed. 26 26 27 definition instruction_nature_next_pc_length ≝ 28 λvariety: instruction_nature. 29 match variety with 30 [ ret ⇒ 0 31  branch _ ⇒ 2 32  goto _ ⇒ 1 33  direct_fun_call _ ⇒ 1 34  other ⇒ 1 35 ]. 36 27 37 definition instruction_info: 28 BitVectorTrie Byte 16 → Word → ?≝38 BitVectorTrie Byte 16 → Word → Σprod: (instruction_nature × Word × (list Word) × nat). \snd (\fst prod) = instruction_nature_next_pc_length (\fst (\fst (\fst prod))) ≝ 29 39 λmem. 30 40 λpc. 31 41 let 〈inst, next_pc, inst_cost〉 ≝ fetch mem pc in 32 let 〈nature, next_pcs〉≝33 match inst with42 let nature_next_pcs_proof ≝ 43 match inst return λx. Σpair: (instruction_nature × (list Word)). (\snd pair) = instruction_nature_next_pc_length (\fst pair) with 34 44 [ RealInstruction ri ⇒ 35 45 match ri with 36 [ RET ⇒ 〈ret, [ ]〉37  RETI ⇒ 〈ret, [ ]〉46 [ RET ⇒ dp … 〈ret, [ ]〉 ? 47  RETI ⇒ dp … 〈ret, [ ]〉 ? 38 48  JC addr ⇒ 39 49 match addr return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with 40 50 [ RELATIVE addr ⇒ λ_. 41 51 let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in 42 〈branch addr, [ next_pc; addr ]〉52 dp … 〈branch addr, [ next_pc; addr ]〉 ? 43 53  _ ⇒ λp. match p in False with [ ] 44 54 ] (subaddressing_modein … addr) … … 47 57 [ RELATIVE addr ⇒ λ_. 48 58 let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in 49 〈branch addr, [ next_pc; addr ]〉59 dp … 〈branch addr, [ next_pc; addr ]〉 ? 50 60  _ ⇒ λp. match p in False with [ ] 51 61 ] (subaddressing_modein … addr) … … 54 64 [ RELATIVE addr ⇒ λ_. 55 65 let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in 56 〈branch addr, [ next_pc; addr ]〉66 dp … 〈branch addr, [ next_pc; addr ]〉 ? 57 67  _ ⇒ λp. match p in False with [ ] 58 68 ] (subaddressing_modein … addr) … … 61 71 [ RELATIVE addr ⇒ λ_. 62 72 let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in 63 〈branch addr, [ next_pc; addr ]〉73 dp … 〈branch addr, [ next_pc; addr ]〉 ? 64 74  _ ⇒ λp. match p in False with [ ] 65 75 ] (subaddressing_modein … addr) … … 68 78 [ RELATIVE addr ⇒ λ_. 69 79 let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in 70 〈branch addr, [ next_pc; addr ]〉80 dp … 〈branch addr, [ next_pc; addr ]〉 ? 71 81  _ ⇒ λp. match p in False with [ ] 72 82 ] (subaddressing_modein … addr2) … … 75 85 [ RELATIVE addr ⇒ λ_. 76 86 let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in 77 〈branch addr, [ next_pc; addr ]〉87 dp … 〈branch addr, [ next_pc; addr ]〉 ? 78 88  _ ⇒ λp. match p in False with [ ] 79 89 ] (subaddressing_modein … addr2) … … 82 92 [ RELATIVE addr ⇒ λ_. 83 93 let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in 84 〈branch addr, [ next_pc; addr ]〉94 dp … 〈branch addr, [ next_pc; addr ]〉 ? 85 95  _ ⇒ λp. match p in False with [ ] 86 96 ] (subaddressing_modein … addr2) … … 89 99 [ RELATIVE addr ⇒ λ_. 90 100 let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in 91 〈branch addr, [ next_pc; addr ]〉101 dp … 〈branch addr, [ next_pc; addr ]〉 ? 92 102  _ ⇒ λp. match p in False with [ ] 93 103 ] (subaddressing_modein … addr2) … … 96 106 [ RELATIVE addr ⇒ λ_. 97 107 let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in 98 〈branch addr, [ next_pc; addr ]〉99  _ ⇒ λp. match p in False with [ ] 100 ] (subaddressing_modein … addr2) 101  _ ⇒ 〈other, [ next_pc ]〉108 dp … 〈branch addr, [ next_pc; addr ]〉 ? 109  _ ⇒ λp. match p in False with [ ] 110 ] (subaddressing_modein … addr2) 111  _ ⇒ dp … 〈other, [ next_pc ]〉 ? 102 112 ] 103 113  ACALL addr ⇒ … … 105 115 [ ADDR11 addr ⇒ λ_. 106 116 let addr ≝ addr16_of_addr11 pc addr in 107 〈direct_fun_call addr, [ next_pc ]〉117 dp … 〈direct_fun_call addr, [ next_pc ]〉 ? 108 118  _ ⇒ λp. match p in False with [ ] 109 119 ] (subaddressing_modein … addr) 110 120  LCALL addr ⇒ 111 121 match addr return λx. bool_to_Prop (is_in ? [[ addr16 ]] x) → ? with 112 [ ADDR16 addr ⇒ λ_. 〈direct_fun_call addr, [ next_pc ]〉122 [ ADDR16 addr ⇒ λ_. dp … 〈direct_fun_call addr, [ next_pc ]〉 ? 113 123  _ ⇒ λp. match p in False with [ ] 114 124 ] (subaddressing_modein … addr) … … 117 127 [ ADDR11 addr ⇒ λ_. 118 128 let addr ≝ addr16_of_addr11 pc addr in 119 〈goto addr, [ addr ]〉129 dp … 〈goto addr, [ addr ]〉 ? 120 130  _ ⇒ λp. match p in False with [ ] 121 131 ] (subaddressing_modein … addr) 122 132  LJMP addr ⇒ 123 133 match addr return λx. bool_to_Prop (is_in ? [[ addr16 ]] x) → ? with 124 [ ADDR16 addr ⇒ λ_. 〈goto addr, [ addr ]〉134 [ ADDR16 addr ⇒ λ_. dp … 〈goto addr, [ addr ]〉 ? 125 135  _ ⇒ λp. match p in False with [ ] 126 136 ] (subaddressing_modein … addr) … … 129 139 [ RELATIVE addr ⇒ λ_. 130 140 let 〈carry, addr〉 ≝ half_add 16 next_pc (sign_extend 8 8 addr) in 131 〈goto addr, [ addr ]〉132  _ ⇒ λp. match p in False with [ ] 133 ] (subaddressing_modein … addr) 134  JMP addr ⇒ 〈other, [ next_pc ]〉135  MOVC acc_a addr ⇒ 〈other, [ next_pc ]〉141 dp … 〈goto addr, [ addr ]〉 ? 142  _ ⇒ λp. match p in False with [ ] 143 ] (subaddressing_modein … addr) 144  JMP addr ⇒ dp … 〈other, [ next_pc ]〉 ? 145  MOVC acc_a addr ⇒ dp … 〈other, [ next_pc ]〉 ? 136 146 ] 137 147 in 138 〈nature, next_pc, next_pcs, inst_cost〉. 148 match nature_next_pcs_proof with 149 [ dp nature_next_pcs their_proof ⇒ 150 let nature ≝ \fst nature_next_pcs in 151 let next_pcs ≝ \snd nature_next_pcs in 152 dp … 〈〈〈nature, next_pc〉, next_pcs〉, inst_cost〉 ? 153 ]. 154 [1: >their_proof % 155 *: % 156 ] 157 qed. 139 158 140 159 let rec compare … … 160 179 qed. 161 180 162 let rec block_cost 181 let rec block_cost' 163 182 (mem: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie Byte 16) 164 ( the_list: list Word) (program_size: nat)165 on program_size : nat≝183 (program_counter: Word) (program_size: nat) (cost_so_far: nat) 184 on program_size ≝ 166 185 match program_size with 167 [ O ⇒ 0 (* XXX: empty program *) 168  S program_size ⇒ 169 match the_list with 170 [ nil ⇒ 0 (* XXX: should be empty program *) 171  cons pc tl ⇒ 172 match tl with 173 [ nil ⇒ 174 match lookup_opt … pc cost_labels with 175 [ None ⇒ 176 let 〈ignore, ignore, next_pcs, cost〉 ≝ instruction_info mem pc in 177 let tail ≝ block_cost mem cost_labels next_pcs program_size in 178 cost + tail 179  Some _ ⇒ O 180 ] 181  _ ⇒ compare ? (map … (λpc. 〈pc, block_cost mem cost_labels [pc] program_size〉) the_list) 186 [ O ⇒ 0 187  S program_size ⇒ 188 let sigma ≝ instruction_info mem program_counter in 189 match sigma with 190 [ dp variety_costs their_proof ⇒ 191 let variety ≝ \fst (\fst (\fst variety_costs)) in 192 let next_pc ≝ \snd (\fst (\fst variety_costs)) in 193 let next_pcs ≝ \snd (\fst variety_costs) in 194 let inst_cost ≝ \snd variety_costs in 195 match variety return λx. next_pcs = instruction_nature_next_pc_length x → nat with 196 [ other ⇒ λproof. 197 match next_pcs return λx. x = 1 → nat with 198 [ nil ⇒ λabsurd. ⊥ 199  cons hd tl ⇒ λproof. 200 match lookup_opt … hd cost_labels with 201 [ None ⇒ block_cost' mem cost_labels hd program_size (cost_so_far + inst_cost) 202  Some _ ⇒ inst_cost + cost_so_far 203 ] 204 ] proof 205  _ ⇒ λ_. inst_cost + cost_so_far 206 ] their_proof 182 207 ] 183 ] 184 ]. 208 ]. 209 normalize in absurd 210 destruct(absurd) 211 qed. 212 213 definition block_cost ≝ 214 λmem: BitVectorTrie Byte 16. 215 λcost_labels: BitVectorTrie Byte 16. 216 λprogram_counter: Word. 217 λprogram_size: nat. 218 block_cost' mem cost_labels program_counter program_size 0. 185 219 186 220 let rec traverse_code_internal … … 188 222 (cost_labels: BitVectorTrie Byte 16) (pc: Word) (program_size: nat) 189 223 on program: BitVectorTrie nat 8 ≝ 190 let 〈ignore, newpc, ignore, ignore〉 ≝ instruction_info mem pc in 191 match program with 192 [ nil ⇒ Stub … 193  cons hd tl ⇒ 194 match lookup_opt … pc cost_labels with 195 [ None ⇒ traverse_code_internal tl mem cost_labels newpc program_size 196  Some lbl ⇒ 197 let cost ≝ block_cost mem cost_labels [ pc ] program_size in 198 let cost_mapping ≝ traverse_code_internal tl mem cost_labels newpc program_size in 199 insert … lbl cost cost_mapping 224 match instruction_info mem pc with 225 [ dp info proof ⇒ 226 let newpc ≝ \snd (\fst (\fst info)) in 227 match program with 228 [ nil ⇒ Stub … 229  cons hd tl ⇒ 230 match lookup_opt … pc cost_labels with 231 [ None ⇒ traverse_code_internal tl mem cost_labels newpc program_size 232  Some lbl ⇒ 233 let cost ≝ block_cost mem cost_labels pc program_size in 234 let cost_mapping ≝ traverse_code_internal tl mem cost_labels newpc program_size in 235 insert … lbl cost cost_mapping 236 ] 200 237 ] 201 238 ]. … … 217 254 match lookup_opt … oldpc cost_labels with 218 255 [ None ⇒ 219 let 〈nature, pc, ignore, inst_cost〉 ≝ instruction_info mem oldpc in 256 match instruction_info mem oldpc with 257 [ dp info proof ⇒ 258 let nature ≝ \fst (\fst (\fst info)) in 259 let pc ≝ \snd (\fst (\fst info)) in 260 let inst_cost ≝ \snd info in 220 261 match nature with 221 262 [ direct_fun_call addr ⇒ … … 227 268  _ ⇒ ⊥ (* XXX: was assert false in o'caml *) 228 269 ] 270 ] 229 271  Some cost ⇒ 〈cost, 0〉 230 272 ]
Note: See TracChangeset
for help on using the changeset viewer.