Changeset 1948 for src/ASM/AssemblyProof.ma
 Timestamp:
 May 15, 2012, 11:13:14 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r1947 r1948 43 43 (λb. λc. (if b then c else (if c then false else true))) b c = true → b = c. 44 44 #b #c 45 cases b 46 [1: 47 normalize // 48 2: 49 normalize 50 cases c normalize // 51 ] 45 cases b cases c normalize nodelta 46 try (#_ % @I) 47 #assm destruct % 52 48 qed. 53 49 … … 1416 1412 lemma fetch_assembly_pseudo': 1417 1413 ∀lookup_labels. 1418 ∀sigma: Word → Word × bool. 1414 ∀sigma: Word → Word. 1415 ∀policy: Word → bool. 1419 1416 ∀ppc. 1420 1417 ∀lookup_datalabels. … … 1424 1421 ∀assembled. 1425 1422 ∀instructions. 1426 let 〈pc, force_long_jump〉≝ sigma ppc in1427 instructions = expand_pseudo_instruction lookup_labels sigma p pc lookup_datalabels pi →1428 〈len,assembled〉 = assembly_1_pseudoinstruction lookup_labels sigma p pc lookup_datalabels pi →1423 let pc ≝ sigma ppc in 1424 instructions = expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels pi → 1425 〈len,assembled〉 = assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi → 1429 1426 let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in 1430 1427 encoding_check code_memory pc pc_plus_len assembled → 1431 1428 fetch_many code_memory pc_plus_len pc instructions. 1432 #lookup_labels #sigma #ppc #lookup_datalabels #pi #code_memory #len #assembled #instructions 1433 generalize in match (refl … (sigma ppc)); 1434 cases (sigma ?) in ⊢ (??%? → %); #pc #force_long_jump #sigma_refl normalize nodelta 1435 #instructions_refl whd in ⊢ (???% → ?); <instructions_refl whd in ⊢ (???% → ?); #assembled_refl 1429 #lookup_labels #sigma #policy #ppc #lookup_datalabels #pi #code_memory #len #assembled #instructions 1430 normalize nodelta #instructions_refl whd in ⊢ (???% → ?); <instructions_refl whd in ⊢ (???% → ?); #assembled_refl 1436 1431 cases (pair_destruct ?????? assembled_refl) assembled_refl #len_refl #assembled_refl 1437 1432 >len_refl >assembled_refl len_refl 1438 generalize in match (add 16 pc1433 generalize in match (add 16 (sigma ppc) 1439 1434 (bitvector_of_nat 16 1440 1435 (flatten (Vector bool 8) 1441 1436 (map instruction (list (Vector bool 8)) assembly1 instructions)))); 1442 1437 #final_pc 1443 generalize in match pc; elim instructions1438 generalize in match (sigma ppc); elim instructions 1444 1439 [1: 1445 1440 #pc whd in ⊢ (% → %); #H >H @eq_bv_refl … … 1464 1459 lemma fetch_assembly_pseudo: 1465 1460 ∀program: pseudo_assembly_program. 1466 ∀sigma: Word → Word × bool. 1467 let lookup_labels ≝ λx:Identifier.\fst (sigma (address_of_word_labels_code_mem (\snd program) x)) in 1468 ∀ppc.∀code_memory. 1461 ∀sigma: Word → Word. 1462 ∀policy: Word → bool. 1463 let lookup_labels ≝ λx:Identifier. sigma (address_of_word_labels_code_mem (\snd program) x) in 1464 ∀ppc. 1465 ∀code_memory. 1469 1466 let lookup_datalabels ≝ λx:Identifier.lookup_def … (construct_datalabels (\fst program)) x (zero 16) in 1470 1467 let pi ≝ \fst (fetch_pseudo_instruction (\snd program) ppc) in 1471 let pc ≝ \fst (sigma ppc)in1472 let instructions ≝ expand_pseudo_instruction lookup_labels sigma p pc lookup_datalabels pi in1473 let 〈len,assembled〉 ≝ assembly_1_pseudoinstruction lookup_labels sigma p pc lookup_datalabels pi in1468 let pc ≝ sigma ppc in 1469 let instructions ≝ expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels pi in 1470 let 〈len,assembled〉 ≝ assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi in 1474 1471 let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in 1475 1472 encoding_check code_memory pc pc_plus_len assembled → 1476 1473 fetch_many code_memory pc_plus_len pc instructions. 1477 #program #sigma letin lookup_labels ≝ (λx.?) #ppc #code_memory1474 #program #sigma #policy letin lookup_labels ≝ (λx.?) #ppc #code_memory 1478 1475 letin lookup_datalabels ≝ (λx.?) 1479 1476 letin pi ≝ (fst ???) 1480 letin pc ≝ ( fst ???)1481 letin instructions ≝ (expand_pseudo_instruction ????? )1477 letin pc ≝ (sigma ?) 1478 letin instructions ≝ (expand_pseudo_instruction ??????) 1482 1479 @pair_elim #len #assembled #assembled_refl normalize nodelta 1483 1480 #H 1484 1481 generalize in match 1485 (fetch_assembly_pseudo' lookup_labels sigma ppc lookup_datalabels pi code_memory len assembled instructions) in ⊢ ?; 1486 #X destruct 1487 cases (sigma ppc) in H X; #pc #force_long_jump normalize nodelta 1488 #H #X @X try % <assembled_refl try % assumption 1482 (fetch_assembly_pseudo' lookup_labels sigma policy ppc lookup_datalabels pi code_memory len assembled instructions) in ⊢ ?; 1483 #X destruct normalize nodelta @X try % <assembled_refl try % assumption 1489 1484 qed. 1490 1485 … … 1498 1493 *) 1499 1494 axiom assembly_ok: 1500 ∀program,sigma,assembled,costs'. 1495 ∀program. 1496 ∀sigma: Word → Word. 1497 ∀policy: Word → bool. 1498 ∀assembled. 1499 ∀costs'. 1501 1500 let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in 1502 〈assembled,costs'〉 = assembly program sigma →1501 〈assembled,costs'〉 = assembly program sigma policy → 1503 1502 costs = costs' ∧ 1504 1503 let code_memory ≝ load_code_memory assembled in 1505 1504 let datalabels ≝ construct_datalabels (\fst program) in 1506 let lookup_labels ≝ λx. \fst (sigma (address_of_word_labels_code_mem (\snd program) x)) in1505 let lookup_labels ≝ λx. sigma (address_of_word_labels_code_mem (\snd program) x) in 1507 1506 let lookup_datalabels ≝ λx. lookup_def ?? datalabels x (zero ?) in 1508 1507 ∀ppc. 1509 1508 let 〈pi, newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in 1510 let 〈len,assembled〉 ≝ assembly_1_pseudoinstruction lookup_labels sigma p pc lookup_datalabels pi in1511 let pc ≝ \fst (sigma ppc)in1509 let 〈len,assembled〉 ≝ assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi in 1510 let pc ≝ sigma ppc in 1512 1511 let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in 1513 1512 encoding_check code_memory pc pc_plus_len assembled ∧ 1514 \fst (sigma newppc)= add … pc (bitvector_of_nat … len).1513 sigma newppc = add … pc (bitvector_of_nat … len). 1515 1514 1516 1515 (* XXX: should we add that costs = costs'? *) 1517 1516 lemma fetch_assembly_pseudo2: 1518 ∀program,sigma,ppc. 1517 ∀program. 1518 ∀sigma. 1519 ∀policy. 1520 ∀ppc. 1519 1521 let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in 1520 let 〈assembled, costs'〉 ≝ assembly program sigma in1522 let 〈assembled, costs'〉 ≝ assembly program sigma policy in 1521 1523 let code_memory ≝ load_code_memory assembled in 1522 1524 let data_labels ≝ construct_datalabels (\fst program) in 1523 let lookup_labels ≝ λx. \fst (sigma (address_of_word_labels_code_mem (\snd program) x)) in1525 let lookup_labels ≝ λx. sigma (address_of_word_labels_code_mem (\snd program) x) in 1524 1526 let lookup_datalabels ≝ λx. lookup_def ? ? data_labels x (zero ?) in 1525 1527 let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in 1526 let instructions ≝ expand_pseudo_instruction lookup_labels sigma p pc lookup_datalabels pi in1527 fetch_many code_memory ( \fst (sigma newppc)) (\fst (sigma ppc)) instructions.1528 * #preamble #instr_list #sigma #p pc1528 let instructions ≝ expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels pi in 1529 fetch_many code_memory (sigma newppc) (sigma ppc) instructions. 1530 * #preamble #instr_list #sigma #policy #ppc 1529 1531 @pair_elim #labels #costs #create_label_map_refl 1530 1532 @pair_elim #assembled #costs' #assembled_refl … … 1534 1536 letin lookup_datalabels ≝ (λx. ?) 1535 1537 @pair_elim #pi #newppc #fetch_pseudo_refl 1536 lapply (assembly_ok 〈preamble, instr_list〉 sigma assembled costs')1538 lapply (assembly_ok 〈preamble, instr_list〉 sigma policy assembled costs') 1537 1539 @pair_elim #labels' #costs' #create_label_map_refl' #H 1538 1540 cases (H (sym_eq … assembled_refl)) 1539 1541 #_ 1540 lapply (refl … (assembly_1_pseudoinstruction lookup_labels sigma p pc lookup_datalabels pi))1541 cases (assembly_1_pseudoinstruction ????? ) in ⊢ (???% → ?);1542 lapply (refl … (assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi)) 1543 cases (assembly_1_pseudoinstruction ??????) in ⊢ (???% → ?); 1542 1544 #len #assembledi #EQ4 #H 1543 1545 lapply (H ppc) >fetch_pseudo_refl #H 1544 lapply (fetch_assembly_pseudo 〈preamble,instr_list〉 sigma p pc (load_code_memory assembled))1546 lapply (fetch_assembly_pseudo 〈preamble,instr_list〉 sigma policy ppc (load_code_memory assembled)) 1545 1547 >EQ4 #H1 cases H #H2 #H3 >H3 normalize nodelta in H1; normalize nodelta 1546 1548 >fetch_pseudo_refl in H1; #assm @assm assumption … … 1695 1697 1696 1698 definition code_memory_of_pseudo_assembly_program: 1697 ∀pap:pseudo_assembly_program. (Word → Word × bool) → BitVectorTrie Byte 16 1698 ≝ λpap,sigma. 1699 let p ≝ assembly pap sigma in 1700 load_code_memory (\fst p). 1699 ∀pap:pseudo_assembly_program. 1700 (Word → Word) → (Word → bool) → BitVectorTrie Byte 16 ≝ 1701 λpap. 1702 λsigma. 1703 λpolicy. 1704 let p ≝ assembly pap sigma policy in 1705 load_code_memory (\fst p). 1701 1706 1702 1707 definition status_of_pseudo_status: 1703 internal_pseudo_address_map → ∀pap.∀ps:PseudoStatus pap. ∀sigma: Word → Word × bool. 1704 Status (code_memory_of_pseudo_assembly_program pap sigma) ≝ 1705 λM,pap,ps,sigma. 1706 let cm ≝ code_memory_of_pseudo_assembly_program … sigma in 1707 let pc ≝ \fst (sigma (program_counter … ps)) in 1708 internal_pseudo_address_map → ∀pap. ∀ps: PseudoStatus pap. 1709 ∀sigma: Word → Word. ∀policy: Word → bool. 1710 Status (code_memory_of_pseudo_assembly_program pap sigma policy) ≝ 1711 λM. 1712 λpap. 1713 λps. 1714 λsigma. 1715 λpolicy. 1716 let cm ≝ code_memory_of_pseudo_assembly_program … sigma policy in 1717 let pc ≝ sigma (program_counter … ps) in 1708 1718 let lir ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps) in 1709 1719 let hir ≝ high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram … ps) in … … 1833 1843 *) 1834 1844 1835 definition ticks_of0: ∀p:pseudo_assembly_program. (Word → Word × bool) → Word → pseudo_instruction → nat × nat ≝ 1836 λprogram: pseudo_assembly_program.λsigma. 1845 definition ticks_of0: 1846 ∀p:pseudo_assembly_program. 1847 (Word → Word) → (Word → bool) → Word → pseudo_instruction → nat × nat ≝ 1848 λprogram: pseudo_assembly_program. 1849 λsigma. 1850 λpolicy. 1837 1851 λppc: Word. 1838 1852 λfetched. ?. … … 1989 2003 *)qed. 1990 2004 1991 definition ticks_of: ∀p:pseudo_assembly_program. (Word → Word × bool) → Word → nat × nat ≝ 1992 λprogram: pseudo_assembly_program.λsigma. 2005 definition ticks_of: 2006 ∀p:pseudo_assembly_program. 2007 (Word → Word) → (Word → bool) → Word → nat × nat ≝ 2008 λprogram: pseudo_assembly_program. 2009 λsigma. 2010 λpolicy. 1993 2011 λppc: Word. 1994 2012 let 〈preamble, pseudo〉 ≝ program in 1995 2013 let 〈fetched, new_ppc〉 ≝ fetch_pseudo_instruction pseudo ppc in 1996 ticks_of0 program sigma p pc fetched.2014 ticks_of0 program sigma policy ppc fetched. 1997 2015 1998 2016 lemma eq_rect_Type1_r: 1999 2017 ∀A: Type[1]. 2000 ∀a: A.2018 ∀a: A. 2001 2019 ∀P: ∀x:A. eq ? x a → Type[1]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p. 2002 2020 #A #a #P #H #x #p 2003 2021 generalize in match H; 2004 2022 generalize in match P; 2005 cases p 2006 // 2023 cases p // 2007 2024 qed. 2008 2025 … … 2162 2179 (*CSC: ???*) 2163 2180 axiom snd_assembly_1_pseudoinstruction_ok: 2164 ∀program:pseudo_assembly_program.∀sigma. 2165 ∀ppc:Word.∀pi,lookup_labels,lookup_datalabels. 2166 lookup_labels = (λx. \fst (sigma (address_of_word_labels_code_mem (\snd program) x))) → 2167 lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) → 2168 \fst (fetch_pseudo_instruction (\snd program) ppc) = pi → 2169 let len ≝ \fst (assembly_1_pseudoinstruction lookup_labels sigma (\fst (sigma ppc)) lookup_datalabels pi) in 2170 \fst (sigma (add … ppc (bitvector_of_nat ? 1))) = 2171 add … (\fst (sigma ppc)) (bitvector_of_nat ? len). 2181 ∀program: pseudo_assembly_program. 2182 ∀sigma: Word → Word. 2183 ∀policy: Word → bool. 2184 ∀ppc: Word. 2185 ∀pi. 2186 ∀lookup_labels. 2187 ∀lookup_datalabels. 2188 lookup_labels = (λx. sigma (address_of_word_labels_code_mem (\snd program) x)) → 2189 lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) → 2190 \fst (fetch_pseudo_instruction (\snd program) ppc) = pi → 2191 let len ≝ \fst (assembly_1_pseudoinstruction lookup_labels sigma policy (sigma ppc) lookup_datalabels pi) in 2192 sigma (add … ppc (bitvector_of_nat ? 1)) = add … (sigma ppc) (bitvector_of_nat ? len). 2172 2193 2173 2194 lemma pose: ∀A:Type[0].∀B:A → Type[0].∀a:A. (∀a':A. a'=a → B a') → B a. 2174 /2/2195 /2/ 2175 2196 qed. 2176 2197 2177 2198 (* To be moved in ProofStatus *) 2178 2199 lemma program_counter_set_program_counter: 2179 ∀T,cm,s,x. program_counter T cm (set_program_counter T cm s x) = x. 2180 // 2200 ∀T. 2201 ∀cm. 2202 ∀s. 2203 ∀x. 2204 program_counter T cm (set_program_counter T cm s x) = x. 2205 // 2181 2206 qed. 2182 2207 2183 2208 theorem main_thm: 2184 ∀M,M',cm,ps,sigma. 2185 next_internal_pseudo_address_map M cm ps = Some … M' → 2186 ∃n. 2187 execute n … (status_of_pseudo_status M … ps sigma) 2188 = status_of_pseudo_status M' … (execute_1_pseudo_instruction (ticks_of cm sigma) cm ps) sigma. 2189 #M #M' * #preamble #instr_list #ps #sigma 2190 change with (next_internal_pseudo_address_map0 ????? = ? → ?) 2191 @(pose … (program_counter ?? ps)) #ppc #EQppc 2192 generalize in match (fetch_assembly_pseudo2 〈preamble,instr_list〉 sigma ppc) in ⊢ ?; 2193 @pair_elim #labels #costs #H0 normalize nodelta 2194 @pair_elim #assembled #costs' #EQ1 normalize nodelta 2195 @pair_elim #pi #newppc #EQ2 normalize nodelta 2196 @(pose … (λx. \fst (sigma (address_of_word_labels_code_mem instr_list x)))) #lookup_labels #EQlookup_labels 2197 @(pose … (λx. lookup_def … (construct_datalabels preamble) x (zero 16))) #lookup_datalabels #EQlookup_datalabels 2198 whd in match execute_1_pseudo_instruction; normalize nodelta 2199 whd in match ticks_of; normalize nodelta <EQppc #H2 >EQ2 normalize nodelta 2200 lapply (snd_fetch_pseudo_instruction instr_list ppc) >EQ2 #EQnewppc >EQnewppc 2201 lapply (snd_assembly_1_pseudoinstruction_ok 〈preamble,instr_list〉 … ppc pi … EQlookup_labels EQlookup_datalabels ?) 2202 [>EQ2 %] 2203 inversion pi 2204 [2,3: (* Comment, Cost *) #ARG #EQ 2205 #H3 normalize nodelta in H3; normalize in match (assembly_1_pseudoinstruction ?????) in H3; 2206 whd in ⊢ (??%? → ?); @Some_Some_elim #MAP <MAP 2207 whd in match (execute_1_pseudo_instruction0 ?????); 2208 %{0} @split_eq_status 2209 ∀M. 2210 ∀M'. 2211 ∀cm. 2212 ∀ps. 2213 ∀sigma. 2214 ∀policy. 2215 next_internal_pseudo_address_map M cm ps = Some … M' → 2216 ∃n. execute n … (status_of_pseudo_status M … ps sigma policy) = 2217 status_of_pseudo_status M' … 2218 (execute_1_pseudo_instruction (ticks_of cm sigma policy) cm ps) sigma policy. 2219 #M #M' * #preamble #instr_list #ps #sigma #policy 2220 change with (next_internal_pseudo_address_map0 ????? = ? → ?) 2221 @(pose … (program_counter ?? ps)) #ppc #EQppc 2222 generalize in match (fetch_assembly_pseudo2 〈preamble,instr_list〉 sigma policy ppc) in ⊢ ?; 2223 @pair_elim #labels #costs #H0 normalize nodelta 2224 @pair_elim #assembled #costs' #EQ1 normalize nodelta 2225 @pair_elim #pi #newppc #EQ2 normalize nodelta 2226 @(pose … (λx. sigma (address_of_word_labels_code_mem instr_list x))) #lookup_labels #EQlookup_labels 2227 @(pose … (λx. lookup_def … (construct_datalabels preamble) x (zero 16))) #lookup_datalabels #EQlookup_datalabels 2228 whd in match execute_1_pseudo_instruction; normalize nodelta 2229 whd in match ticks_of; normalize nodelta <EQppc #H2 >EQ2 normalize nodelta 2230 lapply (snd_fetch_pseudo_instruction instr_list ppc) >EQ2 #EQnewppc >EQnewppc 2231 lapply (snd_assembly_1_pseudoinstruction_ok 〈preamble,instr_list〉 … policy … ppc pi … EQlookup_labels EQlookup_datalabels ?) 2232 [>EQ2 %] 2233 inversion pi 2234 [2,3: (* Comment, Cost *) 2235 #ARG #EQ 2236 #H3 normalize nodelta in H3; normalize in match (assembly_1_pseudoinstruction ??????) in H3; 2237 whd in ⊢ (??%? → ?); @Some_Some_elim #MAP <MAP 2238 whd in match (execute_1_pseudo_instruction0 ?????); 2239 %{0} @split_eq_status 2209 2240 CSC: STOP HERE, was // but requires H0 H3 because of \fst and \pi1 2210 2241 ⇒ CHANGE TO AVOID \fst and \pi1! (*
Note: See TracChangeset
for help on using the changeset viewer.