Changeset 1941 for src/ASM/AssemblyProof.ma
 Timestamp:
 May 14, 2012, 4:33:20 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r1939 r1941 21 21 2: 22 22 letin res ≝ (bit ::: prefix) 23 <minus_S_S 24 >minus_Sn_m 25 [1: 26 @res 27 2: 28 assumption 29 ] 23 <minus_S_S >minus_Sn_m 24 try assumption @res 30 25 3: 31 26 @le_S_to_le … … 53 48 2: 54 49 normalize 55 cases c 56 [1: 57 normalize // 58 2: 59 normalize // 60 ] 50 cases c normalize // 61 51 ] 62 52 qed. … … 78 68 2: 79 69 letin res ≝ (bit ::: prefix) 80 <(minus_S_S ? ?) 81 >(minus_Sn_m ? ?) 82 [1: 83 @res 84 2: 85 @prf2 86 ] 70 <(minus_S_S ? ?) >(minus_Sn_m ? ?) 71 try @prf2 @res 87 72 3: 88 73 /2/ … … 94 79 λP: BitVector n → bool. 95 80 bitvector_elim_internal n P n ? ?. 96 [ @(le_n ?) 97  <(minus_n_n ?) 98 @[[ ]] 99 ] 81 try @le_n 82 <minus_n_n @[[]] 100 83 qed. 101 84 … … 943 926 lemma eq_instruction_refl: 944 927 ∀i. eq_instruction i i = true. 945 #i cases i 946 [1,2,3,4,5,6: 947 #arg1 @eq_addressing_mode_refl 948 7: 949 #arg1 #arg2 950 whd in ⊢ (??%?); 951 >eq_addressing_mode_refl 952 >eq_addressing_mode_refl % 953 8: 954 #arg @eq_preinstruction_refl 955 ] 928 #i cases i [*: #arg1 ] 929 try @eq_addressing_mode_refl 930 try @eq_preinstruction_refl 931 #arg2 whd in ⊢ (??%?); 932 >eq_addressing_mode_refl >eq_addressing_mode_refl % 956 933 qed. 957 934 … … 1150 1127 p = q → 〈p, r〉 = 〈q, r〉. 1151 1128 #A #p #q #r #hyp 1152 >hyp%1129 destruct % 1153 1130 qed. 1154 1131 … … 1158 1135 p = q → 〈r, p〉 = 〈r, q〉. 1159 1136 #A #p #q #r #hyp 1160 >hyp%1137 destruct % 1161 1138 qed. 1162 1139 … … 1168 1145 #A #n #q #r 1169 1146 generalize in match (Vector_O A q …); 1170 #hyp >hyp in ⊢ (??%?);%1147 #hyp destruct % 1171 1148 qed. 1172 1149 … … 1205 1182 [1: 1206 1183 #n #l #r #v #hd #eq #hyp 1207 destruct 1208 >(Vector_O … l) % 1184 destruct >(Vector_O … l) % 1209 1185 2: 1210 1186 #m' #inductive_hypothesis #n #l #r #v #hd #equal #hyp … … 1214 1190 >tail_head 1215 1191 <(? : split A (S m') n (l@@r) = split' A (S m') n (l@@r)) 1216 [1: 1217 <hyp <head_head' % 1218 2: 1219 elim l normalize // 1220 ] 1192 try (<hyp <head_head' %) 1193 elim l normalize // 1221 1194 ] 1222 1195 qed. … … 1240 1213 cases (Vector_Sn A r v) #hd #exists 1241 1214 cases exists #tl #jmeq 1242 >jmeq 1243 @split_succ try % 1215 >jmeq @split_succ try % 1244 1216 @ih % 1245 1217 ] … … 1275 1247 λl, m: nat. 1276 1248 λv: Vector a (l + m). 1277 λP. 1278 match v return λn: nat. λv: Vector a (n + m). 1279 (∀vl: Vector a ?. 1280 ∀vm: Vector a m. 1281 v = vl@@vm → P 〈vl,vm〉) → P (split a ? m v) with 1282 [ VEmpty ⇒ ? 1283  VCons v' hd tl ⇒ ? 1284 ] ?. 1249 λP. ?. 1250 cases daemon 1251 qed. 1285 1252 1286 1253 (* XXX: this looks almost certainly wrong *) … … 1328 1295 ]. 1329 1296 1297 axiom add_bitvector_of_nat_Sm: 1298 ∀n, m: nat. 1299 add … (bitvector_of_nat … 1) (bitvector_of_nat … m) = 1300 bitvector_of_nat n (S m). 1301 1330 1302 lemma encoding_check_append: 1331 1303 ∀code_memory: BitVectorTrie Byte 16. 1332 ∀final_pc: nat.1304 ∀final_pc: Word. 1333 1305 ∀l1: list Byte. 1334 ∀pc: nat.1306 ∀pc: Word. 1335 1307 ∀l2: list Byte. 1336 encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … final_pc)(l1@l2) →1337 let intermediate_pc ≝ pc + length … l1in1338 encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … intermediate_pc)l1 ∧1339 encoding_check code_memory (bitvector_of_nat … intermediate_pc) (bitvector_of_nat … final_pc)l2.1308 encoding_check code_memory pc final_pc (l1@l2) → 1309 let pc_plus_len ≝ add … pc (bitvector_of_nat … (length … l1)) in 1310 encoding_check code_memory pc pc_plus_len l1 ∧ 1311 encoding_check code_memory pc_plus_len final_pc l2. 1340 1312 #code_memory #final_pc #l1 elim l1 1341 1313 [1: 1342 1314 #pc #l2 1343 1315 whd in ⊢ (????% → ?); #H 1344 < plus_n_O1316 <add_zero 1345 1317 whd whd in ⊢ (?%?); /2/ 1346 1318 2: 1347 1319 #hd #tl #IH #pc #l2 * #H1 #H2 1348 >half_add_SO in H2; #H2 1349 cases (IH … H2) <plus_n_Sm 1350 #K1 #K2 % [2: @K2 ] whd % // 1351 >half_add_SO @K1 1320 (* >half_add_SO in H2; #H2 *) 1321 cases (IH … H2) #E1 #E2 % 1322 [1: 1323 % try @H1 1324 <(add_bitvector_of_nat_Sm 16 (tl)) in E1; 1325 <add_associative #assm assumption 1326 2: 1327 <add_associative in E2; 1328 <(add_bitvector_of_nat_Sm 16 (tl)) #assm 1329 assumption 1330 ] 1352 1331 ] 1353 1332 qed. 1354 1333 1355 axiom bitvector_3_elim_prop: 1334 axiom bitvector_3_cases: 1335 ∀b: BitVector 3. 1336 ∃l, c, r: bool. 1337 b = [[l; c; r]]. 1338 1339 lemma bitvector_3_elim_prop: 1356 1340 ∀P: BitVector 3 → Prop. 1357 1341 P [[false;false;false]] → P [[false;false;true]] → P [[false;true;false]] → 1358 1342 P [[false;true;true]] → P [[true;false;false]] → P [[true;false;true]] → 1359 1343 P [[true;true;false]] → P [[true;true;true]] → ∀v. P v. 1344 #P #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 1345 cases (bitvector_3_cases … H9) #l #assm cases assm 1346 assm #c #assm cases assm 1347 assm #r #assm cases assm destruct 1348 cases l cases c cases r // 1349 qed. 1360 1350 1361 1351 definition ticks_of_instruction ≝ … … 1366 1356 1367 1357 lemma fetch_assembly: 1368 ∀pc: nat.1358 ∀pc: Word. 1369 1359 ∀i: instruction. 1370 1360 ∀code_memory: BitVectorTrie Byte 16. … … 1372 1362 assembled = assembly1 i → 1373 1363 let len ≝ length … assembled in 1374 encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … (pc + len)) assembled → 1375 let fetched ≝ fetch code_memory (bitvector_of_nat … pc) in 1376 let 〈instr_pc, ticks〉 ≝ fetched in 1377 let 〈instr,pc'〉 ≝ instr_pc in 1378 (eq_instruction instr i ∧ eqb ticks (ticks_of_instruction instr) ∧ eq_bv … pc' (bitvector_of_nat … (pc + len))) = true. 1364 let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in 1365 encoding_check code_memory pc pc_plus_len assembled → 1366 let 〈instr, pc', ticks〉 ≝ fetch code_memory pc in 1367 (eq_instruction instr i ∧ eqb ticks (ticks_of_instruction instr) ∧ eq_bv … pc' pc_plus_len) = true. 1379 1368 #pc #i #code_memory #assembled cases i [8: *] 1380 1369 [16,20,29: * * 18,19: * * [1,2,4,5: *] 28: * * [1,2: * [1,2: * [1,2: * [1,2: *]]]]] … … 1430 1419 axiom eq_instruction_to_eq: 1431 1420 ∀i1, i2: instruction. 1432 eq_instruction i1 i2 = true → i1 =i2.1421 eq_instruction i1 i2 = true → i1 ≃ i2. 1433 1422 1434 (*1435 1423 lemma fetch_assembly_pseudo': 1436 1424 ∀lookup_labels. 1437 ∀ pol: policy_type lookup_labels.1425 ∀sigma: Word → Word × bool. 1438 1426 ∀ppc. 1439 1427 ∀lookup_datalabels. … … 1443 1431 ∀assembled. 1444 1432 ∀instructions. 1445 ∀pc. 1446 let expansion ≝ pol ppc in 1447 instructions = expand_pseudo_instruction lookup_labels ppc expansion lookup_datalabels pi → 1448 〈len,assembled〉 = assembly_1_pseudoinstruction lookup_labels pol ppc lookup_datalabels pi → 1449 encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … (pc + len)) assembled → 1450 fetch_many code_memory (bitvector_of_nat … (pc + len)) (bitvector_of_nat … pc) instructions. 1451 #lookup_labels #pol #ppc #lookup_datalabels #pi #code_memory #len #assembled #instructions #pc 1452 #EQ1 whd in ⊢ (???% → ?); <EQ1 whd in ⊢ (???% → ?); #EQ2 1453 cases (pair_destruct ?????? EQ2) EQ2; #EQ2a #EQ2b 1454 >EQ2a >EQ2b EQ2a EQ2b; 1455 generalize in match (pc + flatten … (map … assembly1 instructions)); #final_pc 1433 let 〈pc, force_long_jump〉 ≝ sigma ppc in 1434 instructions = expand_pseudo_instruction lookup_labels sigma ppc lookup_datalabels pi → 1435 〈len,assembled〉 = assembly_1_pseudoinstruction lookup_labels sigma ppc lookup_datalabels pi → 1436 let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in 1437 encoding_check code_memory pc pc_plus_len assembled → 1438 fetch_many code_memory pc_plus_len pc instructions. 1439 #lookup_labels #sigma #ppc #lookup_datalabels #pi #code_memory #len #assembled #instructions 1440 generalize in match (refl … (sigma ppc)); 1441 cases (sigma ?) in ⊢ (??%? → %); #pc #force_long_jump #sigma_refl normalize nodelta 1442 #instructions_refl whd in ⊢ (???% → ?); <instructions_refl whd in ⊢ (???% → ?); #assembled_refl 1443 cases (pair_destruct ?????? assembled_refl) assembled_refl #len_refl #assembled_refl 1444 >len_refl >assembled_refl len_refl 1445 generalize in match (add 16 pc 1446 (bitvector_of_nat 16 1447 (flatten (Vector bool 8) 1448 (map instruction (list (Vector bool 8)) assembly1 instructions)))); 1449 #final_pc 1456 1450 generalize in match pc; elim instructions 1457 1451 [1: 1458 1452 #pc whd in ⊢ (% → %); #H >H @eq_bv_refl 1459 1453 2: 1460 #i #tl #IH #pc #H whd cases (encoding_check_append … H); H; #H1 #H2 whd 1461 generalize in match (fetch_assembly pc i code_memory … (refl …) H1); 1462 cases (fetch code_memory (bitvector_of_nat … pc)) #newi_pc #ticks whd in ⊢ (% → %); 1463 cases newi_pc #newi #newpc whd in ⊢ (% → %); #K cases (conjunction_true … K) K; #K1 1464 cases (conjunction_true … K1) K1; #K1 #K2 #K3 % try % 1454 #i #tl #IH #pc #H whd 1455 cases (encoding_check_append ????? H) H #H1 #H2 1456 @pair_elim #instr_pc #ticks #fetch_refl normalize nodelta 1457 @pair_elim #instr #pc' #instr_pc_refl normalize nodelta 1458 lapply (fetch_assembly pc i code_memory (assembly1 i) (refl …)) whd in ⊢ (% → ?); 1459 #H3 lapply (H3 H1) H3 >fetch_refl >instr_pc_refl normalize nodelta 1460 #H3 lapply (conjunction_true ?? H3) * #H4 #H5 % 1465 1461 [1: 1466 @K1 1462 lapply (conjunction_true … H4) * #B1 #B2 1463 % try assumption @eqb_true_to_eq 1464 <(eq_instruction_to_eq … B1) assumption 1467 1465 2: 1468 @eqb_true_to_eq <(eq_instruction_to_eq … K1) @K2 1469 3: 1470 >(eq_bv_eq … K3) @IH @H2 1466 >(eq_bv_eq … H5) @IH @H2 1471 1467 ] 1472 1468 ] 1473 1469 qed. 1474 *) 1475 1476 axiom bitvector_of_nat_nat_of_bitvector: 1477 ∀n,v. 1478 bitvector_of_nat n (nat_of_bitvector n v) = v. 1479 1480 (* CSC: soo long next one; can we merge with previous one now? *) 1470 1481 1471 lemma fetch_assembly_pseudo: 1482 1472 ∀program: pseudo_assembly_program. 1483 ∀ pol: policy program.1484 let lookup_labels ≝ λx:Identifier. sigma … pol (address_of_word_labels_code_mem (\snd program) x) in1473 ∀sigma: Word → Word × bool. 1474 let lookup_labels ≝ λx:Identifier.\fst (sigma (address_of_word_labels_code_mem (\snd program) x)) in 1485 1475 ∀ppc.∀code_memory. 1486 1476 let lookup_datalabels ≝ λx:Identifier.lookup_def … (construct_datalabels (\fst program)) x (zero 16) in 1487 let pc ≝ sigma program pol ppc in1488 1477 let pi ≝ \fst (fetch_pseudo_instruction (\snd program) ppc) in 1489 let instructions ≝ expand_pseudo_instruction lookup_labels ppc (pol lookup_labels ppc) lookup_datalabels pi in 1490 let 〈len,assembled〉 ≝ assembly_1_pseudoinstruction lookup_labels (pol lookup_labels) ppc lookup_datalabels pi in 1491 encoding_check code_memory pc (bitvector_of_nat … (nat_of_bitvector ? pc + len)) assembled → 1492 fetch_many code_memory (bitvector_of_nat … (nat_of_bitvector ? pc + len)) pc instructions. 1493 #program #pol letin lookup_labels ≝ (λx.?) #ppc #code_memory 1478 let pc ≝ \fst (sigma ppc) in 1479 let instructions ≝ expand_pseudo_instruction lookup_labels sigma ppc lookup_datalabels pi in 1480 let 〈len,assembled〉 ≝ assembly_1_pseudoinstruction lookup_labels sigma ppc lookup_datalabels pi in 1481 let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in 1482 encoding_check code_memory pc pc_plus_len assembled → 1483 fetch_many code_memory pc_plus_len pc instructions. 1484 #program #sigma letin lookup_labels ≝ (λx.?) #ppc #code_memory 1494 1485 letin lookup_datalabels ≝ (λx.?) 1495 letin pc ≝ (sigma ???) letin pi ≝ (fst ???) 1486 letin pi ≝ (fst ???) 1487 letin pc ≝ (fst ???) 1496 1488 letin instructions ≝ (expand_pseudo_instruction ?????) 1497 @pair_elim #len #assembled #EQ1 #H 1489 @pair_elim #len #assembled #assembled_refl normalize nodelta 1490 #H 1498 1491 generalize in match 1499 (fetch_assembly_pseudo' lookup_labels ((pi1 ?? pol) lookup_labels) ppc lookup_datalabels pi code_memory len1500 assembled instructions (nat_of_bitvector ? pc)) in ⊢ ?;1501 >bitvector_of_nat_nat_of_bitvector >EQ1normalize nodelta1502 #X @X //1503 qed. 1504 1505 (* This is a trivial consequence of fetch_assembly + the proof that the1492 (fetch_assembly_pseudo' lookup_labels sigma ppc lookup_datalabels pi code_memory len assembled instructions) in ⊢ ?; 1493 #X destruct 1494 cases (sigma ppc) in H X; #pc #force_long_jump normalize nodelta 1495 #H #X @X try % <assembled_refl try % assumption 1496 qed. 1497 1498 (* This is a trivial consequence of fetch_assembly_pseudo + the proof that the 1506 1499 function that load the code in memory is correct. The latter is based 1507 1500 on missing properties from the standard library on the BitVectorTrie 1508 data structrure. *) 1501 data structrure. 1502 1503 Wrong at the moment, requires Jaap's precondition to ensure that the program 1504 does not overflow when put into code memory (i.e. shorter than 2^16 bytes). 1505 *) 1509 1506 axiom assembly_ok: 1510 ∀program, pol,assembled,costs'.1511 let 〈labels, costs〉 ≝ build_maps program polin1512 〈assembled,costs'〉 = assembly program pol→1507 ∀program,sigma,assembled,costs'. 1508 let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in 1509 〈assembled,costs'〉 = assembly program sigma → 1513 1510 costs = costs' ∧ 1514 1511 let code_memory ≝ load_code_memory assembled in 1515 let preamble ≝ \fst program in 1516 let datalabels ≝ construct_datalabels preamble in 1517 let lookup_labels ≝ λx.sigma … pol (address_of_word_labels_code_mem (\snd program) x) in 1512 let datalabels ≝ construct_datalabels (\fst program) in 1513 let lookup_labels ≝ λx.\fst (sigma (address_of_word_labels_code_mem (\snd program) x)) in 1518 1514 let lookup_datalabels ≝ λx. lookup_def ?? datalabels x (zero ?) in 1519 1515 ∀ppc. 1520 let pi_newppc ≝ fetch_pseudo_instruction (\snd program) ppc in 1521 ∀len,assembledi. 1522 〈len,assembledi〉 = assembly_1_pseudoinstruction lookup_labels (pol lookup_labels) ppc lookup_datalabels (\fst pi_newppc) → 1523 encoding_check code_memory (sigma program pol ppc) (bitvector_of_nat … (nat_of_bitvector … (sigma program pol ppc) + len)) assembledi ∧ 1524 sigma program pol (\snd pi_newppc) = bitvector_of_nat … (nat_of_bitvector … (sigma program pol ppc) + len). 1525 1516 let 〈pi, newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in 1517 let 〈len,assembled〉 ≝ assembly_1_pseudoinstruction lookup_labels sigma ppc lookup_datalabels pi in 1518 let pc ≝ \fst (sigma ppc) in 1519 let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in 1520 encoding_check code_memory pc pc_plus_len assembled ∧ 1521 \fst (sigma newppc) = add … pc (bitvector_of_nat … len). 1522 1523 (* XXX: should we add that costs = costs'? *) 1526 1524 lemma fetch_assembly_pseudo2: 1527 ∀program, pol,ppc.1528 (* let 〈labels,costs〉 ≝ build_maps program pol in *) 1529 let assembled ≝ \fst (assembly program pol)in1525 ∀program,sigma,ppc. 1526 let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in 1527 let 〈assembled, costs'〉 ≝ assembly program sigma in 1530 1528 let code_memory ≝ load_code_memory assembled in 1531 1529 let data_labels ≝ construct_datalabels (\fst program) in 1532 let lookup_labels ≝ λx. sigma … pol (address_of_word_labels_code_mem (\snd program) x) in1530 let lookup_labels ≝ λx.\fst (sigma (address_of_word_labels_code_mem (\snd program) x)) in 1533 1531 let lookup_datalabels ≝ λx. lookup_def ? ? data_labels x (zero ?) in 1534 1532 let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in 1535 let instructions ≝ expand_pseudo_instruction lookup_labels ppc (pol lookup_labels ppc) lookup_datalabels pi in 1536 fetch_many code_memory (sigma program pol newppc) (sigma program pol ppc) instructions. 1537 * #preamble #instr_list #pol #ppc 1538 letin assembled ≝ (\fst (assembly 〈preamble,instr_list〉 pol)) 1539 letin code_memory ≝ (load_code_memory assembled) 1540 letin data_labels ≝ (construct_datalabels preamble) 1541 letin lookup_labels ≝ (λx. sigma … pol (address_of_word_labels_code_mem instr_list x)) 1542 letin lookup_datalabels ≝ (λx. lookup_def ? ? data_labels x (zero ?)) 1543 @pair_elim #pi #newppc #EQ1 change with (fetch_pseudo_instruction instr_list ? = ?) in EQ1; 1544 generalize in match (assembly_ok ? pol assembled (\snd (assembly 〈preamble,instr_list〉 pol))); 1545 @pair_elim #labels #costs #EQ2 <eq_pair_fst_snd 1546 #H cases (H (refl \ldots)) H; #EQ3 1547 generalize in match (refl … (assembly_1_pseudoinstruction lookup_labels (pol lookup_labels) ppc lookup_datalabels ?)); 1548 [ cases (assembly_1_pseudoinstruction ?????) in ⊢ (???% → ?); #len #assembledi #EQ4 1549 #H cases (H ppc len assembledi ?) [2: <EQ4 %] H; #H1 #H2 1550 (* XXX JPB: attention to lookup_labels *) 1551 generalize in match (fetch_assembly_pseudo 〈preamble,instr_list〉 pol ppc (load_code_memory assembled)) in ⊢ ?; 1552 >EQ4; #H generalize in match (H H1) in ⊢ ?; H >(pair_destruct_2 ????? (sym_eq … EQ1)) 1553 >H2 >EQ1 #K @K 1533 let instructions ≝ expand_pseudo_instruction lookup_labels sigma ppc lookup_datalabels pi in 1534 fetch_many code_memory (\fst (sigma newppc)) (\fst (sigma ppc)) instructions. 1535 * #preamble #instr_list #sigma #ppc 1536 @pair_elim #labels #costs #create_label_map_refl 1537 @pair_elim #assembled #costs' #assembled_refl 1538 letin code_memory ≝ (load_code_memory ?) 1539 letin data_labels ≝ (construct_datalabels ?) 1540 letin lookup_labels ≝ (λx. ?) 1541 letin lookup_datalabels ≝ (λx. ?) 1542 @pair_elim #pi #newppc #fetch_pseudo_refl 1543 lapply (assembly_ok 〈preamble, instr_list〉 sigma assembled costs') 1544 @pair_elim #labels' #costs' #create_label_map_refl' #H 1545 cases (H (sym_eq … assembled_refl)) 1546 #_ 1547 lapply (refl … (assembly_1_pseudoinstruction lookup_labels sigma ppc lookup_datalabels pi)) 1548 cases (assembly_1_pseudoinstruction ?????) in ⊢ (???% → ?); 1549 #len #assembledi #EQ4 #H 1550 lapply (H ppc) >fetch_pseudo_refl #H 1551 lapply (fetch_assembly_pseudo 〈preamble,instr_list〉 sigma ppc (load_code_memory assembled)) 1552 >EQ4 #H1 cases H #H2 #H3 >H3 normalize nodelta in H1; normalize nodelta 1553 >fetch_pseudo_refl in H1; #assm @assm assumption 1554 1554 qed. 1555 1555
Note: See TracChangeset
for help on using the changeset viewer.