Changeset 2899 for src/ASM/AssemblyProof.ma
 Timestamp:
 Mar 19, 2013, 12:33:13 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r2516 r2899 46 46 ] 47 47 qed. 48 49 definition ticks_of_instruction ≝50 λi.51 let trivial_code_memory ≝ assembly1 i in52 let trivial_status ≝ load_code_memory trivial_code_memory in53 \snd (fetch trivial_status (zero ?)).54 48 55 49 lemma fetch_assembly: … … 146 140 ∀sigma: Word → Word. 147 141 ∀policy: Word → bool. 148 let 〈labels, costs〉 ≝ create_label_cost_map ( \sndprogram) in142 let 〈labels, costs〉 ≝ create_label_cost_map (code program) in 149 143 let lookup_labels ≝ λx. bitvector_of_nat 16 (lookup_def … labels x 0) in 150 144 ∀ppc.∀ppc_ok. 151 145 ∀code_memory. 152 let lookup_datalabels ≝ λx:Identifier. lookup_def … (construct_datalabels ( \fstprogram)) x (zero 16) in153 let pi ≝ \fst (fetch_pseudo_instruction ( \sndprogram) ppc ppc_ok) in146 let lookup_datalabels ≝ λx:Identifier. lookup_def … (construct_datalabels (preamble program)) x (zero 16) in 147 let pi ≝ \fst (fetch_pseudo_instruction (code program) ppc ppc_ok) in 154 148 let pc ≝ sigma ppc in 155 149 let instructions ≝ expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels pi in … … 186 180 sigma in the outofbounds region too. *) 187 181 lemma assembly_ok: 188 ∀program .189 ∀length_proof:  \sndprogram ≤ 2^16.182 ∀program: pseudo_assembly_program. 183 ∀length_proof: code program ≤ 2^16. 190 184 ∀sigma: Word → Word. 191 185 ∀policy: Word → bool. 192 186 ∀sigma_policy_witness: sigma_policy_specification program sigma policy. 193 ∀assembled .187 ∀assembled: object_code. 194 188 ∀costs': BitVectorTrie costlabel 16. 195 let 〈preamble, instr_list〉 ≝ program in 189 let preamble ≝ preamble program in 190 let instr_list ≝ code program in 196 191 let 〈labels, costs〉 ≝ create_label_cost_map instr_list in 197 192 let datalabels ≝ construct_datalabels preamble in 198 193 let lookup_datalabels ≝ λx. lookup_def … datalabels x (zero …) in 199 〈assembled,costs'〉 = assembly program sigma policy → 194 let loc ≝ pi1 … (assembly program sigma policy) in 195 let assembled ≝ oc loc in 196 let costs' ≝ costlabels loc in 200 197 (* costs = costs' ∧ CSC: costs != costs', costs' = sigma costs! *) 201 198 let code_memory ≝ load_code_memory assembled in 202 199 let lookup_labels ≝ λx. bitvector_of_nat 16 (lookup_def … labels x 0) in 203 200 ∀ppc.∀ppc_ok. 204 let 〈pi, newppc〉 ≝ fetch_pseudo_instruction ( \sndprogram) ppc ppc_ok in201 let 〈pi, newppc〉 ≝ fetch_pseudo_instruction (code program) ppc ppc_ok in 205 202 let 〈len,assembled〉 ≝ assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi in 206 203 let pc ≝ sigma ppc in … … 209 206 sigma newppc = add … pc (bitvector_of_nat … len). 210 207 #program #length_proof #sigma #policy #sigma_policy_witness #assembled #costs' 211 cases (assembly program sigma policy) * #assembled' #costs'' 212 @pair_elim #preamble #instr_list #EQprogram whd in ⊢ (% → %); 213 cut (instr_list ≤ 2^16) [ >EQprogram in length_proof; // ] #instr_list_ok 208 cases (assembly program sigma policy) * #assembled' #costs'' #symbol_table #fpc #inj 209 cut (code program ≤ 2^16) [ // ] #instr_list_ok 214 210 #H lapply (H sigma_policy_witness instr_list_ok) H whd in ⊢ (% → ?); 215 211 @pair_elim #labels #costs #create_label_cost_refl whd in ⊢ (% → %); 216 * * #assembly_ok1 #assembly_ok3 #assembly_ok2 #Pair_eq destruct(Pair_eq) whd212 * * #assembly_ok1 #assembly_ok3 #assembly_ok2 217 213 #ppc #ppc_ok @pair_elim #pi #newppc #eq_fetch_pseudo_instruction 218 214 @pair_elim #len #assembled #eq_assembly_1_pseudoinstruction whd … … 225 221 [2: >(pair_destruct_2 ????? (sym_eq … eq_fetch_pseudo_instruction)) 226 222 >snd_fetch_pseudo_instruction 227 cases sigma_policy_witness #_ >EQprogram#H cases (H ? ppc_ok) H223 cases sigma_policy_witness #_ #H cases (H ? ppc_ok) H 228 224 #spw1 #_ >spw1 spw1 @eq_f @eq_f 229 225 >eq_fetch_pseudo_instruction whd in match instruction_size; … … 261 257 lemma fetch_assembly_pseudo2: 262 258 ∀program. 263 ∀length_proof:  \sndprogram ≤ 2^16.259 ∀length_proof: code program ≤ 2^16. 264 260 ∀sigma. 265 261 ∀policy. 266 262 ∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy. 267 263 ∀ppc.∀ppc_ok. 268 let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in 269 let 〈assembled, costs'〉 ≝ pi1 … (assembly program sigma policy) in 264 let 〈labels, costs〉 ≝ create_label_cost_map (code program) in 265 let res ≝ pi1 … (assembly program sigma policy) in 266 let assembled ≝ oc res in 267 let cost' ≝ costlabels res in 270 268 let code_memory ≝ load_code_memory assembled in 271 let data_labels ≝ construct_datalabels ( \fstprogram) in269 let data_labels ≝ construct_datalabels (preamble program) in 272 270 let lookup_labels ≝ λx. bitvector_of_nat 16 (lookup_def … labels x 0) in 273 271 let lookup_datalabels ≝ λx. lookup_def ? ? data_labels x (zero ?) in 274 let 〈pi,newppc〉 ≝ fetch_pseudo_instruction ( \sndprogram) ppc ppc_ok in272 let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (code program) ppc ppc_ok in 275 273 let instructions ≝ expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels pi in 276 274 fetch_many code_memory (sigma newppc) (sigma ppc) instructions. 277 * #preamble #instr_list #length_proof #sigma #policy #sigma_policy_specification_witness #ppc #ppc_ok 275 * #preamble #instr_list #code_size_ok #renamed_symbol #final_label 276 #inj #well_labelled #length_proof #sigma #policy #sigma_policy_specification_witness #ppc #ppc_ok 278 277 @pair_elim #labels #costs #create_label_map_refl 279 @pair_elim #assembled #costs' #assembled_refl 278 letin res ≝ (assembly ???) 279 letin assembled ≝ (oc ?) 280 letin costs' ≝ (costlabels ?) 280 281 letin code_memory ≝ (load_code_memory ?) 281 282 letin data_labels ≝ (construct_datalabels ?) 282 283 letin lookup_labels ≝ (λx. ?) 283 284 letin lookup_datalabels ≝ (λx. ?) 284 @pair_elim #pi #newppc #fetch_pseudo_refl 285 lapply (assembly_ok 〈preamble, instr_list〉 ? sigma policy sigma_policy_specification_witness assembled costs') 285 lapply (assembly_ok ?? sigma policy sigma_policy_specification_witness assembled costs') 286 286 normalize nodelta try assumption 287 287 >create_label_map_refl in ⊢ (match % with [_ ⇒ ?] → ?); #H 288 lapply (H (sym_eq … assembled_refl)) H 288 lapply (H … ppc_ok) H 289 @pair_elim #pi #newppc #EQpi_neqppc 290 (*CSC: was working, to be repaired after change in datatypes representation 289 291 lapply (refl … (assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi)) 290 292 cases (assembly_1_pseudoinstruction ??????) in ⊢ (???% → ?); … … 295 297 >EQ4 #H1 cases (H ppc_ok) 296 298 #H2 #H3 >H3 normalize nodelta in H1; normalize nodelta 297 >fetch_pseudo_refl in H1; #assm @assm assumption 299 >fetch_pseudo_refl in H1; #assm @assm assumption *) cases daemon 298 300 qed. 299 301 … … 740 742  Cost _ ⇒ Some … M 741 743  Jmp _ ⇒ Some … M 744  Jnz _ _ _ ⇒ Some … M 745  MovSuccessor _ _ _ ⇒ ? (*CSC: TO BE IMPLEMENTED*) 742 746  Call a ⇒ 743 747 let a' ≝ addr_of a s in … … 789 793 None ? 790 794  JC addr1 ⇒ Some ? M 795  JMP _ ⇒ ? (*CSC: TO BE IMPLEMENTED*) 791 796  JNC addr1 ⇒ Some ? M 792 797  JB addr1 addr2 ⇒ Some ? M … … 1263 1268 (* XXX: check values returned for conditional jumps below! They are wrong, 1264 1269 find correct values *) 1265 definition ticks_of0:1266 ∀p:pseudo_assembly_program.1267 (Identifier → Word) → (Word → Word) → (Word → bool) → Word → pseudo_instruction → nat × nat ≝1268 λprogram: pseudo_assembly_program.1269 λlookup_labels: Identifier → Word.1270 λsigma.1271 λpolicy.1272 λppc: Word.1273 λfetched.1274 match fetched with1275 [ Instruction instr ⇒1276 match instr with1277 [ JC lbl ⇒1278 let lookup_address ≝ sigma (lookup_labels lbl) in1279 let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in1280 let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in1281 if sj_possible then1282 〈2, 2〉1283 else1284 〈4, 4〉1285  JNC lbl ⇒1286 let lookup_address ≝ sigma (lookup_labels lbl) in1287 let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in1288 let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in1289 if sj_possible then1290 〈2, 2〉1291 else1292 〈4, 4〉1293  JB bit lbl ⇒1294 let lookup_address ≝ sigma (lookup_labels lbl) in1295 let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in1296 let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in1297 if sj_possible then1298 〈2, 2〉1299 else1300 〈4, 4〉1301  JNB bit lbl ⇒1302 let lookup_address ≝ sigma (lookup_labels lbl) in1303 let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in1304 let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in1305 if sj_possible then1306 〈2, 2〉1307 else1308 〈4, 4〉1309  JBC bit lbl ⇒1310 let lookup_address ≝ sigma (lookup_labels lbl) in1311 let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in1312 let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in1313 if sj_possible then1314 〈2, 2〉1315 else1316 〈4, 4〉1317  JZ lbl ⇒1318 let lookup_address ≝ sigma (lookup_labels lbl) in1319 let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in1320 let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in1321 if sj_possible then1322 〈2, 2〉1323 else1324 〈4, 4〉1325  JNZ lbl ⇒1326 let lookup_address ≝ sigma (lookup_labels lbl) in1327 let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in1328 let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in1329 if sj_possible then1330 〈2, 2〉1331 else1332 〈4, 4〉1333  CJNE arg lbl ⇒1334 let lookup_address ≝ sigma (lookup_labels lbl) in1335 let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in1336 let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in1337 if sj_possible then1338 〈2, 2〉1339 else1340 〈4, 4〉1341  DJNZ arg lbl ⇒1342 let lookup_address ≝ sigma (lookup_labels lbl) in1343 let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in1344 let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in1345 if sj_possible then1346 〈2, 2〉1347 else1348 〈4, 4〉1349  ADD arg1 arg2 ⇒1350 let ticks ≝ ticks_of_instruction (ADD ? arg1 arg2) in1351 〈ticks, ticks〉1352  ADDC arg1 arg2 ⇒1353 let ticks ≝ ticks_of_instruction (ADDC ? arg1 arg2) in1354 〈ticks, ticks〉1355  SUBB arg1 arg2 ⇒1356 let ticks ≝ ticks_of_instruction (SUBB ? arg1 arg2) in1357 〈ticks, ticks〉1358  INC arg ⇒1359 let ticks ≝ ticks_of_instruction (INC ? arg) in1360 〈ticks, ticks〉1361  DEC arg ⇒1362 let ticks ≝ ticks_of_instruction (DEC ? arg) in1363 〈ticks, ticks〉1364  MUL arg1 arg2 ⇒1365 let ticks ≝ ticks_of_instruction (MUL ? arg1 arg2) in1366 〈ticks, ticks〉1367  DIV arg1 arg2 ⇒1368 let ticks ≝ ticks_of_instruction (DIV ? arg1 arg2) in1369 〈ticks, ticks〉1370  DA arg ⇒1371 let ticks ≝ ticks_of_instruction (DA ? arg) in1372 〈ticks, ticks〉1373  ANL arg ⇒1374 let ticks ≝ ticks_of_instruction (ANL ? arg) in1375 〈ticks, ticks〉1376  ORL arg ⇒1377 let ticks ≝ ticks_of_instruction (ORL ? arg) in1378 〈ticks, ticks〉1379  XRL arg ⇒1380 let ticks ≝ ticks_of_instruction (XRL ? arg) in1381 〈ticks, ticks〉1382  CLR arg ⇒1383 let ticks ≝ ticks_of_instruction (CLR ? arg) in1384 〈ticks, ticks〉1385  CPL arg ⇒1386 let ticks ≝ ticks_of_instruction (CPL ? arg) in1387 〈ticks, ticks〉1388  RL arg ⇒1389 let ticks ≝ ticks_of_instruction (RL ? arg) in1390 〈ticks, ticks〉1391  RLC arg ⇒1392 let ticks ≝ ticks_of_instruction (RLC ? arg) in1393 〈ticks, ticks〉1394  RR arg ⇒1395 let ticks ≝ ticks_of_instruction (RR ? arg) in1396 〈ticks, ticks〉1397  RRC arg ⇒1398 let ticks ≝ ticks_of_instruction (RRC ? arg) in1399 〈ticks, ticks〉1400  SWAP arg ⇒1401 let ticks ≝ ticks_of_instruction (SWAP ? arg) in1402 〈ticks, ticks〉1403  MOV arg ⇒1404 let ticks ≝ ticks_of_instruction (MOV ? arg) in1405 〈ticks, ticks〉1406  MOVX arg ⇒1407 let ticks ≝ ticks_of_instruction (MOVX ? arg) in1408 〈ticks, ticks〉1409  SETB arg ⇒1410 let ticks ≝ ticks_of_instruction (SETB ? arg) in1411 〈ticks, ticks〉1412  PUSH arg ⇒1413 let ticks ≝ ticks_of_instruction (PUSH ? arg) in1414 〈ticks, ticks〉1415  POP arg ⇒1416 let ticks ≝ ticks_of_instruction (POP ? arg) in1417 〈ticks, ticks〉1418  XCH arg1 arg2 ⇒1419 let ticks ≝ ticks_of_instruction (XCH ? arg1 arg2) in1420 〈ticks, ticks〉1421  XCHD arg1 arg2 ⇒1422 let ticks ≝ ticks_of_instruction (XCHD ? arg1 arg2) in1423 〈ticks, ticks〉1424  RET ⇒1425 let ticks ≝ ticks_of_instruction (RET ?) in1426 〈ticks, ticks〉1427  RETI ⇒1428 let ticks ≝ ticks_of_instruction (RETI ?) in1429 〈ticks, ticks〉1430  NOP ⇒1431 let ticks ≝ ticks_of_instruction (NOP ?) in1432 〈ticks, ticks〉1433 ]1434  Comment comment ⇒ 〈0, 0〉1435  Cost cost ⇒ 〈0, 0〉1436  Jmp jmp ⇒1437 let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in1438 let do_a_long ≝ policy ppc in1439 let lookup_address ≝ sigma (lookup_labels jmp) in1440 let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in1441 if sj_possible ∧ ¬ do_a_long then1442 〈2, 2〉 (* XXX: SJMP *)1443 else1444 let 〈mj_possible, disp2〉 ≝ absolute_jump_cond pc_plus_jmp_length lookup_address in1445 if mj_possible ∧ ¬ do_a_long then1446 〈2, 2〉 (* XXX: AJMP *)1447 else1448 〈2, 2〉 (* XXX: LJMP *)1449  Call call ⇒1450 (* XXX: collapse the branches as they are identical? *)1451 let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in1452 let lookup_address ≝ sigma (lookup_labels call) in1453 let 〈mj_possible, disp〉 ≝ absolute_jump_cond pc_plus_jmp_length lookup_address in1454 let do_a_long ≝ policy ppc in1455 if mj_possible ∧ ¬ do_a_long then1456 〈2, 2〉 (* ACALL *)1457 else1458 〈2, 2〉 (* LCALL *)1459  Mov dptr tgt ⇒ 〈2, 2〉1460 ].1461 1462 definition ticks_of:1463 ∀p:pseudo_assembly_program.1464 (Identifier → Word) → (Word → Word) → (Word → bool) → ∀ppc:Word.1465 nat_of_bitvector … ppc < \snd p → nat × nat ≝1466 λprogram: pseudo_assembly_program.1467 λlookup_labels.1468 λsigma.1469 λpolicy.1470 λppc: Word. λppc_ok.1471 let pseudo ≝ \snd program in1472 let 〈fetched, new_ppc〉 ≝ fetch_pseudo_instruction pseudo ppc ppc_ok in1473 ticks_of0 program lookup_labels sigma policy ppc fetched.1474 1270 1475 1271 (*
Note: See TracChangeset
for help on using the changeset viewer.