 Timestamp:
 May 15, 2012, 11:13:14 AM (8 years ago)
 Location:
 src/ASM
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Assembly.ma
r1946 r1948 5 5 include alias "basics/logic.ma". 6 6 include alias "arithmetics/nat.ma". 7 include "utilities/extralib.ma". 7 include "utilities/extralib.ma". 8 8 9 9 (**************************************** START OF POLICY ABSTRACTION ********************) … … 419 419 420 420 definition expand_relative_jump_internal: 421 ∀lookup_labels:Identifier → Word.∀sigma:Word → Word × bool.421 ∀lookup_labels:Identifier → Word.∀sigma:Word → Word. 422 422 Identifier → Word → ([[relative]] → preinstruction [[relative]]) → 423 423 list instruction 424 424 ≝ 425 425 λlookup_labels.λsigma.λlbl.λppc,i. 426 let lookup_address ≝ \fst (sigma (lookup_labels lbl)) in427 let pc ≝ \fst (sigma ppc)in426 let lookup_address ≝ sigma (lookup_labels lbl) in 427 let pc ≝ sigma ppc in 428 428 let 〈result, flags〉 ≝ sub_16_with_carry pc lookup_address false in 429 429 let 〈upper, lower〉 ≝ split ? 8 8 result in … … 436 436 LJMP (ADDR16 lookup_address) 437 437 ]. 438 @ I438 % 439 439 qed. 440 440 … … 471 471 preinstruction Identifier → list instruction ≝ 472 472 λlookup_labels: Identifier → Word. 473 λsigma:Word → Word × bool.473 λsigma:Word → Word. 474 474 λppc: Word. 475 475 (*λjmp_len: jump_length.*) … … 517 517 518 518 definition expand_pseudo_instruction: 519 ∀lookup_labels.∀sigma.Word → ? → pseudo_instruction → list instruction ≝ 520 λlookup_labels:Identifier → Word. 521 λsigma:Word → Word × bool. 519 ∀lookup_labels. 520 ∀sigma: Word → Word. 521 ∀policy: Word → bool. 522 Word → ? → pseudo_instruction → list instruction ≝ 523 λlookup_labels: Identifier → Word. 524 λsigma: Word → Word. 525 λpolicy: Word → bool. 522 526 λppc. 523 527 λlookup_datalabels:Identifier → Word. … … 527 531  Comment comment ⇒ [ ] 528 532  Call call ⇒ 529 let 〈addr_5, resta〉 ≝ split ? 5 11 (\fst (sigma (lookup_labels call))) in 530 let 〈pc, do_a_long〉 ≝ sigma ppc in 533 let 〈addr_5, resta〉 ≝ split ? 5 11 (sigma (lookup_labels call)) in 534 let pc ≝ sigma ppc in 535 let do_a_long ≝ policy ppc in 531 536 let 〈pc_5, restp〉 ≝ split ? 5 11 pc in 532 537 if eq_bv ? addr_5 pc_5 ∧ ¬ do_a_long then … … 534 539 [ ACALL address ] 535 540 else 536 let address ≝ ADDR16 ( \fst (sigma (lookup_labels call))) in541 let address ≝ ADDR16 (sigma (lookup_labels call)) in 537 542 [ LCALL address ] 538 543  Mov d trgt ⇒ … … 541 546  Instruction instr ⇒ expand_relative_jump lookup_labels sigma ppc instr 542 547  Jmp jmp ⇒ 543 let 〈pc, do_a_long〉 ≝ sigma ppc in 544 let lookup_address ≝ \fst (sigma (lookup_labels jmp)) in 548 let pc ≝ sigma ppc in 549 let do_a_long ≝ policy ppc in 550 let lookup_address ≝ sigma (lookup_labels jmp) in 545 551 let 〈result, flags〉 ≝ sub_16_with_carry pc lookup_address false in 546 552 let 〈upper, lower〉 ≝ split ? 8 8 result in … … 558 564 [ LJMP address ] 559 565 ]. 560 @ I566 % 561 567 qed. 562 568 … … 607 613 definition assembly_1_pseudoinstruction ≝ 608 614 λlookup_labels. 609 λsigma. 615 λsigma: Word → Word. 616 λpolicy: Word → bool. 610 617 λppc: Word. 611 618 λlookup_datalabels. 612 619 λi. 613 let pseudos ≝ expand_pseudo_instruction lookup_labels sigma p pc lookup_datalabels i in620 let pseudos ≝ expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels i in 614 621 let mapped ≝ map ? ? assembly1 pseudos in 615 622 let flattened ≝ flatten ? mapped in … … 618 625 619 626 definition instruction_size ≝ 620 λlookup_labels.λsigma.λppc.λi. 621 \fst (assembly_1_pseudoinstruction lookup_labels sigma ppc (λx.zero …) i). 627 λlookup_labels. 628 λsigma: Word → Word. 629 λpolicy: Word → bool. 630 λppc. 631 λi. 632 \fst (assembly_1_pseudoinstruction lookup_labels sigma policy ppc (λx.zero …) i). 622 633 623 634 (* Jaap: never used … … 1136 1147 1137 1148 (* The function that creates the labeltoaddress map *) 1138 definition create_label_cost_map : ∀program:list labelled_instruction.1149 definition create_label_cost_map0: ∀program:list labelled_instruction. 1139 1150 (Σlabels_costs:label_map × (BitVectorTrie costlabel 16). (* Both on ppcs *) 1140 1151 let 〈labels,costs〉 ≝ labels_costs in 1141 (*∀i:ℕ.lt i (program) → *)1142 1152 ∀l.occurs_exactly_once ?? l program → 1143 (*is_label (nth i ? program 〈None ?, Comment [ ]〉) l →1144 lookup ?? labels l = Some ? i*)1145 1153 bitvector_of_nat ? (lookup_def ?? labels l 0) = 1146 1154 address_of_word_labels_code_mem program l … … 1153 1161 ∀l.occurs_exactly_once ?? l prefix → 1154 1162 bitvector_of_nat ? (lookup_def ?? labels l 0) = 1155 address_of_word_labels_code_mem prefix l 1156 (* 1157 ∀i:ℕ.lt i (prefix) → 1158 ∀l.occurs_exactly_once ?? l prefix → 1159 is_label (nth i ? prefix 〈None ?, Comment [ ]〉) l → 1160 lookup … labels l = Some ? i *) 1161 ) 1163 address_of_word_labels_code_mem prefix l) 1162 1164 program 1163 1165 (λprefix.λx.λtl.λprf.λlabels_costs_ppc. … … 1197 1199 ] 1198 1200 ] 1199 (* 1200 [ @Hocc1201  >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hlbl; / by /1202 ]1203 [1,2: normalize nodelta1204 (* #i >append_length >commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) Hi;1205 [3: #Hi *) #lbl #Hocc (*#Hlbl*) lapply (occurs_exactly_once_Some_stronger ?????? Hocc) Hocc1206 @eq_identifier_elim1207 [ #Heq #Hocc normalize in Hocc; >(nth_append_first ?? prefix ?? (le_S_S_to_le … Hi)) in Hlbl; #Hl1208 @⊥ @(absurd … Hocc) >(label_does_not_occur i … Hl) normalize nodelta /2 by nmk/1209  #Heq #Hocc normalize in Hocc; >lookup_add_miss1210 [ @(IH2 … i (le_S_S_to_le … Hi))1211 [ @Hocc1212  >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hlbl; / by /1213 ]1214  @sym_neq @Heq1215 ]1216 ]1217 4: #Hi #lbl #Hocc >(injective_S … Hi) >nth_append_second1218 [ <minus_n_n #Hl normalize in Hl; >Hl >IH1 @lookup_add_hit1219  @le_n1220 ]1221 1: #Hi #lbl >occurs_exactly_once_None #Hocc #Hlbl1222 @(IH2 … i (le_S_S_to_le … Hi))1223 [ @Hocc1224  >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hlbl; / by /1225 ]1226 2: #Hi #lbl #Hocc >(injective_S … Hi) >nth_append_second1227 [ <minus_n_n #Hl cases Hl1228  @le_n1229 ]1230 ]1231 ] *)1232 1201  @pair_elim * #labels #costs #ppc #EQ destruct normalize nodelta % try % 1233 1202 #l #abs cases (abs) … … 1237 1206 qed. 1238 1207 1208 (* The function that creates the labeltoaddress map *) 1209 definition create_label_cost_map: ∀program:list labelled_instruction. 1210 label_map × (BitVectorTrie costlabel 16) ≝ 1211 λprogram. 1212 pi1 … (create_label_cost_map0 program). 1213 1239 1214 theorem create_label_cost_map_ok: 1240 1215 ∀pseudo_program: pseudo_assembly_program. … … 1242 1217 ∀id. occurs_exactly_once ?? id (\snd pseudo_program) → 1243 1218 bitvector_of_nat ? (lookup_def ?? labels id 0) = address_of_word_labels_code_mem (\snd pseudo_program) id. 1244 #p @pi21219 #p change with (pi1 … (create_label_cost_map0 ?)) in match (create_label_cost_map ?); @pi2 1245 1220 qed. 1246 1221 1247 1222 definition assembly: 1248 ∀p:pseudo_assembly_program.∀sigma:Word → Word × bool.list Byte × (BitVectorTrie costlabel 16) ≝ 1249 λp.let 〈preamble, instr_list〉 ≝ p in 1250 λsigma. 1251 let 〈labels_to_ppc,ppc_to_costs〉 ≝ create_label_cost_map instr_list in 1252 let datalabels ≝ construct_datalabels preamble in 1253 let lookup_labels ≝ λx. \fst (sigma (bitvector_of_nat ? (lookup_def … labels_to_ppc x 0))) in 1254 let lookup_datalabels ≝ λx. lookup_def … datalabels x (zero ?) in 1255 let result ≝ 1223 ∀p: pseudo_assembly_program. 1224 ∀sigma: Word → Word. 1225 ∀policy: Word → bool. 1226 list Byte × (BitVectorTrie costlabel 16) ≝ 1227 λp. 1228 let 〈preamble, instr_list〉 ≝ p in 1229 λsigma. 1230 λpolicy. 1231 let 〈labels_to_ppc,ppc_to_costs〉 ≝ create_label_cost_map instr_list in 1232 let datalabels ≝ construct_datalabels preamble in 1233 let lookup_labels ≝ λx. sigma (bitvector_of_nat ? (lookup_def … labels_to_ppc x 0)) in 1234 let lookup_datalabels ≝ λx. lookup_def … datalabels x (zero ?) in 1235 let result ≝ 1256 1236 foldl_strong 1257 1237 (option Identifier × pseudo_instruction) … … 1262 1242 let 〈pi,newppc〉 ≝ fetch_pseudo_instruction instr_list ppc' in 1263 1243 let 〈len,assembledi〉 ≝ 1264 assembly_1_pseudoinstruction lookup_labels sigma p pc' lookup_datalabels pi in1244 assembly_1_pseudoinstruction lookup_labels sigma policy ppc' lookup_datalabels pi in 1265 1245 True) 1266 1246 instr_list … … 1268 1248 let 〈pc, ppc_code〉 ≝ pc_ppc_code in 1269 1249 let 〈ppc, code〉 ≝ ppc_code in 1270 let 〈pc_delta, program〉 ≝ assembly_1_pseudoinstruction lookup_labels sigma p pc lookup_datalabels (\snd hd) in1250 let 〈pc_delta, program〉 ≝ assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels (\snd hd) in 1271 1251 let 〈new_pc, flags〉 ≝ add_16_with_carry pc (bitvector_of_nat ? pc_delta) false in 1272 1252 let new_ppc ≝ add ? ppc (bitvector_of_nat ? 1) in … … 1275 1255 in 1276 1256 〈\snd (\snd result), 1277 fold … (λppc.λcost.λpc_to_costs. insert … (\fst (sigma ppc)) cost pc_to_costs) ppc_to_costs (Stub ??)〉. 1278 @pair_elim normalize nodelta #x #y #z @pair_elim normalize nodelta #w1 #w2 #w3 #w4 @pair_elim // 1279 qed. 1280 1281 definition assembly_unlabelled_program: assembly_program → option (list Byte × (BitVectorTrie Identifier 16)) ≝ 1282 λp. Some ? (〈foldr ? ? (λi,l. assembly1 i @ l) [ ] p, Stub …〉). 1257 fold … (λppc.λcost.λpc_to_costs. insert … (sigma ppc) cost pc_to_costs) ppc_to_costs (Stub ??)〉. 1258 @pair_elim normalize nodelta #x #y #z 1259 @pair_elim normalize nodelta #w1 #w2 #w3 #w4 1260 @pair_elim // 1261 qed. 1262 1263 definition assembly_unlabelled_program: 1264 assembly_program → option (list Byte × (BitVectorTrie Identifier 16)) ≝ 1265 λp. 1266 Some … (〈foldr … (λi,l. assembly1 i @ l) [ ] p, Stub …〉). 
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! (* 
src/ASM/Interpret.ma
r1946 r1948 8 8 let b ≝ get_index_v ? 8 c 1 ? in 9 9 [[ b; b; b; b; b; b; b; b ]] @@ c. 10 normalize ;11 repeat (@ (le_S_S ?));12 @ (le_O_n);10 normalize 11 repeat (@le_S_S) 12 @le_O_n 13 13 qed. 14 14 15 lemma eq_a_to_eq: ∀a,b. eq_a a b = true → a=b.16 # a17 # b18 cases a19 cases b15 lemma eq_a_to_eq: 16 ∀a,b. 17 eq_a a b = true → a = b. 18 #a #b 19 cases a cases b 20 20 normalize 21 # 21 #K 22 22 try % 23 23 cases (eq_true_false K) … … 25 25 26 26 lemma is_a_to_mem_to_is_in: 27 ∀he,a,m,q. is_a he … a = true → mem … eq_a (S m) q he = true → is_in … q a = true. 28 # he 29 # a 30 # m 31 # q 27 ∀he,a,m,q. 28 is_a he … a = true → mem … eq_a (S m) q he = true → is_in … q a = true. 29 #he #a #m #q 32 30 elim q 33 [ normalize 34 # _ 35 # K 36 assumption 37  # m' 38 # t 39 # q' 40 # II 41 # H1 42 # H2 31 [1: 32 #_ #K assumption 33 2: 34 #m' #t #q' #II #H1 #H2 43 35 normalize 44 change with (orb ??) in H2: 36 change with (orb ??) in H2:(??%?); 45 37 cases (inclusive_disjunction_true … H2) 46 [ # K47 < (eq_a_to_eq … K)48 > H149 %50  #K51 > 38 [1: 39 #K 40 <(eq_a_to_eq … K) >H1 % 41 2: 42 #K 43 >II 52 44 try assumption 53 45 cases (is_a t a)
Note: See TracChangeset
for help on using the changeset viewer.