Changeset 1966 for src/ASM/AssemblyProof.ma
 Timestamp:
 May 17, 2012, 5:45:21 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r1957 r1966 1312 1312 1313 1313 lemma destruct_bug_fix: 1314 3 = 0 → False. 1315 #absurd destruct(absurd) 1314 ∀n: nat. 1315 S n = 0 → False. 1316 #n #absurd destruct(absurd) 1316 1317 qed. 1317 1318 … … 1319 1320 ∀b: BitVector 3. 1320 1321 ∃l, c, r: bool. 1321 b ≃ [[l; c; r]] ≝ ?.1322 b ≃ [[l; c; r]]. 1322 1323 #b 1323 1324 @(Vector_inv_ind bool 3 b (λn: nat. λv: Vector bool n. ∃l:bool.∃c:bool.∃r:bool. v ≃ [[l; c; r]])) 1324 1325 [1: 1325 #absurd @⊥ @destruct_bug_fix1326 #absurd @⊥ b @(destruct_bug_fix 2) 1326 1327 >absurd % 1327 1328 2: 1328 #n #hd #tl #_ #_ #_ %{hd} 1329 #n #hd #tl #_ #size_refl #hd_tl_refl %{hd} 1330 cut (n = 2) 1331 [1: 1332 2: 1333 #n_refl >n_refl in tl; 1329 1334 cases daemon 1330 1335 ] 1336 cases daemon 1331 1337 qed. 1332 1338 … … 1477 1483 encoding_check code_memory pc pc_plus_len assembled → 1478 1484 fetch_many code_memory pc_plus_len pc instructions. 1479 #program #sigma #policy letin lookup_labels ≝ (λx.?) #ppc #code_memory 1480 letin lookup_datalabels ≝ (λx.?) 1481 letin pi ≝ (fst ???) 1482 letin pc ≝ (sigma ?) 1483 letin instructions ≝ (expand_pseudo_instruction ??????) 1484 @pair_elim #len #assembled #assembled_refl normalize nodelta 1485 #H 1486 generalize in match 1487 (fetch_assembly_pseudo' lookup_labels sigma policy ppc lookup_datalabels pi code_memory len assembled instructions) in ⊢ ?; 1488 #X destruct normalize nodelta @X try % <assembled_refl try % assumption 1489 qed. 1485 #program #sigma #policy letin lookup_labels ≝ (λx.?) #ppc #code_memory 1486 letin lookup_datalabels ≝ (λx.?) 1487 letin pi ≝ (fst ???) 1488 letin pc ≝ (sigma ?) 1489 letin instructions ≝ (expand_pseudo_instruction ??????) 1490 @pair_elim #len #assembled #assembled_refl normalize nodelta 1491 #H 1492 generalize in match 1493 (fetch_assembly_pseudo' lookup_labels sigma policy ppc lookup_datalabels pi code_memory len assembled instructions) in ⊢ ?; 1494 #X destruct normalize nodelta @X try % <assembled_refl try % assumption 1495 qed. 1496 1497 definition is_present_in_machine_code_image_p: ∀pseudo_instruction. Prop ≝ 1498 λpseudo_instruction. 1499 match pseudo_instruction with 1500 [ Comment c ⇒ False 1501  Cost c ⇒ False 1502  _ ⇒ True 1503 ]. 1504 1505 definition sigma_policy_specification ≝ 1506 λprogram: pseudo_assembly_program. 1507 λsigma: Word → Word. 1508 λpolicy: Word → bool. 1509 ∀ppc: Word. 1510 let 〈preamble, instr_list〉 ≝ program in 1511 let pc ≝ sigma ppc in 1512 let labels ≝ \fst (create_label_cost_map instr_list) in 1513 let lookup_labels ≝ λx. bitvector_of_nat 16 (lookup_def … labels x 0) in 1514 let instruction ≝ \fst (fetch_pseudo_instruction instr_list ppc) in 1515 let next_pc ≝ sigma (add 16 ppc (bitvector_of_nat 16 1)) in 1516 And (nat_of_bitvector … ppc ≤ instr_list → 1517 next_pc = add 16 pc (bitvector_of_nat … 1518 (instruction_size lookup_labels sigma policy ppc instruction))) 1519 (Or (nat_of_bitvector … ppc < instr_list → 1520 nat_of_bitvector … pc < nat_of_bitvector … next_pc) 1521 (nat_of_bitvector … ppc = instr_list → next_pc = (zero …))). 1490 1522 1491 1523 (* This is a trivial consequence of fetch_assembly_pseudo + the proof that the … … 1501 1533 ∀sigma: Word → Word. 1502 1534 ∀policy: Word → bool. 1535 ∀sigma_policy_witness: sigma_policy_specification program sigma policy. 1503 1536 ∀assembled. 1504 1537 ∀costs'. 1505 1538 let 〈preamble, instr_list〉 ≝ program in 1506 1539 let 〈labels, costs〉 ≝ create_label_cost_map instr_list in 1507 〈assembled,costs'〉 = assembly program sigma policy →1508 costs = costs' ∧1509 let code_memory ≝ load_code_memory assembled in1510 let datalabels ≝ construct_datalabels (\fst program) in1511 let lookup_labels ≝ λx. sigma (address_of_word_labels_code_mem (\snd program) x) in1512 let lookup_datalabels ≝ λx. lookup_def ?? datalabels x (zero ?) in1513 ∀ppc.1514 let 〈pi, newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in1515 let 〈len,assembled〉 ≝ assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi in1516 let pc ≝ sigma ppc in1517 let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in1518 encoding_check code_memory pc pc_plus_len assembled ∧1519 sigma newppc = add … pc (bitvector_of_nat … len).1520 #program #sigma #policy # assembled #costs'1540 let datalabels ≝ construct_datalabels preamble in 1541 let lookup_datalabels ≝ λx. lookup_def … datalabels x (zero …) in 1542 〈assembled,costs'〉 = assembly program sigma policy → 1543 costs = costs' ∧ 1544 let code_memory ≝ load_code_memory assembled in 1545 let lookup_labels ≝ λx. sigma (address_of_word_labels_code_mem instr_list x) in 1546 ∀ppc. 1547 let 〈pi, newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in 1548 let 〈len,assembled〉 ≝ assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi in 1549 let pc ≝ sigma ppc in 1550 let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in 1551 encoding_check code_memory pc pc_plus_len assembled ∧ 1552 sigma newppc = add … pc (bitvector_of_nat … len). 1553 #program #sigma #policy #sigma_policy_witness #assembled #costs' 1521 1554 @pair_elim #preamble #instr_list #program_refl 1522 1555 @pair_elim #labels #costs #create_label_cost_refl 1523 #assembly_refl % 1556 #assembly_refl % cases daemon (* 1524 1557 [1: 1525 >(?: costs = \snd (create_label_cost_map instr_list)) 1526 [1: 1527 >(?: costs' = \snd (assembly program sigma policy)) 1558 (* XXX: lemma on BitVectorTries *) 1559 cases daemon 1560 2: 1561 #ppc #sigma_policy_specification_witness 1562 @pair_elim #pi #newppc #fetch_pseudo_refl 1563 cases pi 1564 [2,3: (* Cost and Comment cases *) 1565 #comment_or_cost normalize in ⊢ (% → ?); #absurd cases absurd 1566 1: (* PreInstruction cases *) 1567 #preinstruction #_ 1568 @pair_elim #len #assembled' #assembly_1_pseudo_refl 1569 normalize nodelta % 1528 1570 [1: 1529 whd in match assembly; normalize nodelta 1530 >program_refl normalize nodelta 1531 >create_label_cost_refl in ⊢ (???%); normalize nodelta 1532 whd in match create_label_cost_map; normalize nodelta 1533 whd in match create_label_cost_map0; normalize nodelta 1571 cases assembled' normalize 1534 1572 2: 1535 <assembly_refl %1536 1573 ] 1537 2: 1538 >create_label_cost_refl % 1539 ] 1540 2: 1574 ] 1541 1575 ] 1542 cases daemon (* XXX: !!! *) 1576 cases daemon (* XXX: !!! *) *) 1543 1577 qed. 1544 1578 … … 1548 1582 ∀sigma. 1549 1583 ∀policy. 1584 ∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy. 1550 1585 ∀ppc. 1551 1586 let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in … … 1558 1593 let instructions ≝ expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels pi in 1559 1594 fetch_many code_memory (sigma newppc) (sigma ppc) instructions. 1560 * #preamble #instr_list #sigma #policy # ppc1595 * #preamble #instr_list #sigma #policy #sigma_policy_specification_witness #ppc 1561 1596 @pair_elim #labels #costs #create_label_map_refl 1562 1597 @pair_elim #assembled #costs' #assembled_refl … … 1566 1601 letin lookup_datalabels ≝ (λx. ?) 1567 1602 @pair_elim #pi #newppc #fetch_pseudo_refl 1568 lapply (assembly_ok 〈preamble, instr_list〉 sigma policy assembled costs')1603 lapply (assembly_ok 〈preamble, instr_list〉 sigma policy sigma_policy_specification_witness assembled costs') 1569 1604 normalize nodelta 1570 1605 @pair_elim #labels' #costs' #create_label_map_refl' #H … … 1576 1611 lapply (H ppc) >fetch_pseudo_refl #H 1577 1612 lapply (fetch_assembly_pseudo 〈preamble,instr_list〉 sigma policy ppc (load_code_memory assembled)) 1578 >EQ4 #H1 cases H #H2 #H3 >H3 normalize nodelta in H1; normalize nodelta 1613 >EQ4 #H1 cases H 1614 #H2 #H3 >H3 normalize nodelta in H1; normalize nodelta 1579 1615 >fetch_pseudo_refl in H1; #assm @assm assumption 1580 1616 qed. … … 2218 2254 qed. 2219 2255 2220 definition is_present_in_machine_code_image_p: ∀pseudo_instruction. Prop ≝2221 λpseudo_instruction.2222 match pseudo_instruction with2223 [ Comment c ⇒ False2224  Cost c ⇒ False2225  _ ⇒ True2226 ].2227 2228 2256 lemma pair_destruct_right: 2229 2257 ∀A: Type[0]. … … 2240 2268 ∀sigma: Word → Word. 2241 2269 ∀policy: Word → bool. 2270 ∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy. 2242 2271 ∀ppc: Word. 2243 2272 ∀pi. 2244 ∀present_in_machine_code_image_witness: is_present_in_machine_code_image_p pi.2245 2273 ∀lookup_labels. 2246 2274 ∀lookup_datalabels. … … 2250 2278 let len ≝ \fst (assembly_1_pseudoinstruction lookup_labels sigma policy (*(sigma ppc)*) ppc lookup_datalabels pi) in 2251 2279 sigma (add … ppc (bitvector_of_nat ? 1)) = add … (sigma ppc) (bitvector_of_nat ? len). 2252 #program #sigma #policy # ppc #pi #is_present_in_machine_code_image_witness2253 #lookup_labels #lookup_datalabels #lookup_labels_refl #lookup_datalabels_refl2254 # fetch_pseudo_refl2280 #program #sigma #policy #sigma_policy_specification_witness #ppc #pi 2281 #lookup_labels #lookup_datalabels 2282 #lookup_labels_refl #lookup_datalabels_refl #fetch_pseudo_refl 2255 2283 normalize nodelta 2256 2284 generalize in match fetch_pseudo_refl; fetch_pseudo_refl 2257 generalize in match is_present_in_machine_code_image_witness; is_present_in_machine_code_image_witness2258 cases pi2259 [1:2260 #preinstruction #_2261 2,3:2262 (* XXX: bug in original statement here, to prove: sigma (ppc + 1) = sigma ppc *)2263 #cost_or_comment normalize in ⊢ (% → ?); #absurd cases absurd2264 4,5:2265 #identifier #_2266 6:2267 #dptr #identifier #_2268 ]2269 2285 #fetch_pseudo_refl 2270 2286 letin assembled ≝ (\fst (assembly program sigma policy)) 2271 2287 letin costs ≝ (\snd (assembly program sigma policy)) 2272 lapply (assembly_ok program sigma policy assembled costs)2288 lapply (assembly_ok program sigma policy sigma_policy_specification_witness assembled costs) 2273 2289 @pair_elim #preamble #instr_list #program_refl 2274 2290 @pair_elim #labels #costs' #create_label_cost_map_refl … … 2276 2292 lapply (H ppc) H 2277 2293 @pair_elim #pi' #newppc #fetch_pseudo_refl' 2278 @pair_elim #len #assembled #assembly1_refl #H cases H 2294 @pair_elim #len #assembled #assembly1_refl #H 2295 cases H 2279 2296 #encoding_check_assm #sigma_newppc_refl 2280 2297 >fetch_pseudo_refl' in fetch_pseudo_refl; #pi_refl' 2281 2298 >pi_refl' in assembly1_refl; #assembly1_refl 2282 >lookup_labels_refl >lookup_datalabels_refl >assembly1_refl 2299 >lookup_labels_refl >lookup_datalabels_refl 2300 >program_refl normalize nodelta 2301 >assembly1_refl 2283 2302 <sigma_newppc_refl 2284 2303 generalize in match fetch_pseudo_refl';
Note: See TracChangeset
for help on using the changeset viewer.