- Timestamp:
- Nov 24, 2011, 5:24:10 PM (9 years ago)
- Location:
- src/ASM
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Assembly.ma
r1555 r1556 1307 1307 λl:list labelled_instruction. 1308 1308 λacc. 1309 foldl ??1309 foldl … 1310 1310 (λt,i. 1311 1311 match t with 1312 [ None ⇒ None ?1312 [ None ⇒ None … 1313 1313 | Some ppc_pc_map ⇒ 1314 1314 let 〈ppc,pc_map〉 ≝ ppc_pc_map in … … 1319 1319 | Some pc_ignore ⇒ 1320 1320 let 〈pc,ignore〉 ≝ pc_ignore in 1321 Some … 〈S ppc,〈pc, insert ? ? (bitvector_of_nat ? ppc) (bitvector_of_nat ?pc) sigma_map〉〉 ]1321 Some … 〈S ppc, 〈pc, insert ?? (bitvector_of_nat 16 ppc) (bitvector_of_nat 16 pc) sigma_map〉〉 ] 1322 1322 ]) acc l. 1323 1323 1324 definition sigma0: pseudo_assembly_program → policy_type → option (nat × (nat × (BitVectorTrie Word 16))) 1325 ≝ λprog.λjump_expansion.sigma00 prog jump_expansion (\snd prog) (Some ? 〈0, 〈0, (Stub ? ?)〉〉). 1324 definition sigma0: pseudo_assembly_program → policy_type → option (nat × (nat × (BitVectorTrie Word 16))) ≝ 1325 λprog. 1326 λjump_expansion. 1327 sigma00 prog jump_expansion (\snd prog) (Some ? 〈0, 〈0, Stub …〉〉). 1326 1328 1327 1329 definition tech_pc_sigma00: pseudo_assembly_program → policy_type → list labelled_instruction → option (nat × nat) ≝ … … 1344 1346 None ? 1345 1347 else 1346 Some ? (λx. lookup ??x sigma_map (zero …)) ].1348 Some ? (λx. lookup … x sigma_map (zero …)) ]. 1347 1349 1348 1350 (* stuff about policy *) … … 1427 1429 ∀ppc:Word.∀lookup_labels,lookup_datalabels,pc. 1428 1430 lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) → 1429 lookup_datalabels = (λx. lookup ?? x (construct_datalabels (\fst program))(zero ?)) →1431 lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) → 1430 1432 let pi ≝ \fst (fetch_pseudo_instruction (\snd program) ppc) in 1431 1433 pc = sigma program pol ppc → … … 1436 1438 | Some res ⇒ res ]. 1437 1439 [ @⊥ whd in p:(??%??); 1438 generalize in match (sig2 ?? pol) whd in ⊢ (% → ?)1439 whd in ⊢ (?(??%?) → ?) change in ⊢ (?(??(match % with [_ ⇒ ? | _ ⇒ ?])?) → ?) with (sigma00 ????)1440 generalize in match (refl … (sigma00 program pol (\snd program) (Some ? 〈O,〈O,Stub (BitVector 16) 16〉〉))) 1441 cases (sigma00 ????) in ⊢ (??%? → %) normalize nodelta [#_ * #abs @abs %]1440 generalize in match (sig2 ?? pol); whd in ⊢ (% → ?); 1441 whd in ⊢ (?(??%?) → ?); change with (sigma00 ????) in ⊢ (?(??(match % with [_ ⇒ ? | _ ⇒ ?])?) → ?); 1442 generalize in match (refl … (sigma00 program pol (\snd program) (Some ? 〈O,〈O,Stub (BitVector 16) 16〉〉))); 1443 cases (sigma00 ????) in ⊢ (??%? → %); normalize nodelta [#_ * #abs @abs %] 1442 1444 #res #K 1443 1445 cases (fetch_pseudo_instruction_split (\snd program) ppc) #pre * #suff * #lbl #EQ1 1444 generalize in match (policy_ok_prefix_hd_ok program pol … EQ1 ?) in ⊢ ? 1446 generalize in match (policy_ok_prefix_hd_ok program pol … EQ1 ?) in ⊢ ?; 1445 1447 cases daemon (* CSC: XXXXXXXX Ero qui 1446 1448 … … 1461 1463 ∀ppc:Word.∀lookup_labels,lookup_datalabels,pi. 1462 1464 lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) → 1463 lookup_datalabels = (λx. lookup ?? x (construct_datalabels (\fst program))(zero ?)) →1465 lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) → 1464 1466 \fst (fetch_pseudo_instruction (\snd program) ppc) = pi → 1465 1467 Σres:(nat × (list Byte)). … … 1478 1480 [ None ⇒ let dummy ≝ 〈0,[ ]〉 in dummy 1479 1481 | Some res ⇒ res ]. 1480 [ @⊥ elim pi in p [*]1482 [ @⊥ elim pi in p; [*] 1481 1483 try (#ARG1 #ARG2 #ARG3 #abs) try (#ARG1 #ARG2 #abs) try (#ARG1 #abs) try #abs 1482 generalize in match (jmeq_to_eq ??? abs) -abs; #abs whd in abs:(??%?); try destruct(abs)1484 generalize in match (jmeq_to_eq ??? abs); -abs; #abs whd in abs:(??%?); try destruct(abs) 1483 1485 whd in abs:(??match % with [_ ⇒ ? | _ ⇒ ?]?); 1484 1486 (* WRONG HERE, NEEDS LEMMA SAYING THAT THE POLICY DOES NOT RETURN MEDIUM! *) … … 1494 1496 ∀ppc:Word.∀lookup_labels,lookup_datalabels,pi. 1495 1497 lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) → 1496 lookup_datalabels = (λx. lookup ?? x (construct_datalabels (\fst program))(zero ?)) →1498 lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) → 1497 1499 \fst (fetch_pseudo_instruction (\snd program) ppc) = pi → 1498 1500 nat × (list Byte) … … 1505 1507 ∀ppc:Word.∀lookup_labels,lookup_datalabels,pi. 1506 1508 ∀prf1:lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)). 1507 ∀prf2:lookup_datalabels = (λx. lookup ?? x (construct_datalabels (\fst program))(zero ?)).1509 ∀prf2:lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)). 1508 1510 ∀prf3:\fst (fetch_pseudo_instruction (\snd program) ppc) = pi. 1509 1511 Some … (assembly_1_pseudoinstruction program pol ppc lookup_labels lookup_datalabels pi prf1 prf2 prf3) … … 1517 1519 definition construct_costs': 1518 1520 ∀program. ∀pol:policy program. ∀ppc,pc,costs,i. 1519 Σres:(nat × (BitVectorTrie Word16)). Some … res = construct_costs_safe program pol ppc pc costs i1521 Σres:(nat × (BitVectorTrie costlabel 16)). Some … res = construct_costs_safe program pol ppc pc costs i 1520 1522 ≝ 1521 1523 λprogram.λpol: policy program.λppc,pc,costs,i. 1522 1524 match construct_costs_safe program pol ppc pc costs i with 1523 [ None ⇒ let dummy ≝ 〈0, Stub ??〉 in dummy1525 [ None ⇒ let dummy ≝ 〈0, Stub costlabel 16〉 in dummy 1524 1526 | Some res ⇒ res ]. 1525 1527 [ cases daemon … … 1613 1615 tech_pc_sigma00 program pol (prefix@[〈label,i〉]) = Some … 〈S ppc,\fst (construct_costs program pol … ppc pc costs i)〉. 1614 1616 1617 lemma eq_identifier_eq: 1618 ∀tag: String. 1619 ∀l. 1620 ∀r. 1621 eq_identifier tag l r = true → l = r. 1622 #tag #l #r cases l cases r #posl #posr 1623 cases daemon 1624 qed. 1625 1615 1626 definition build_maps: 1616 1627 ∀pseudo_program.∀pol:policy pseudo_program. 1617 Σres:((BitVectorTrie Word 16) × (BitVectorTrie Word 16)). 1628 Σres:((identifier_map ASMTag Word) × (BitVectorTrie costlabel 16)). 1629 let 〈labels, costs〉 ≝ res in 1630 ∀id. occurs_exactly_once id (\snd pseudo_program) → 1631 lookup_def … labels id (zero ?) = sigma pseudo_program pol (address_of_word_labels_code_mem (\snd pseudo_program) id) ≝ 1632 λpseudo_program. 1633 λpol:policy pseudo_program. 1634 let result ≝ 1635 foldl_strong 1636 (option Identifier × pseudo_instruction) 1637 (λpre. Σres:((identifier_map ASMTag Word) × (nat × (nat × (BitVectorTrie costlabel 16)))). 1638 let 〈labels,ppc_pc_costs〉 ≝ res in 1639 let 〈ppc',pc_costs〉 ≝ ppc_pc_costs in 1640 let 〈pc',costs〉 ≝ pc_costs in 1641 And ( And ( 1642 And (bitvector_of_nat ? pc' = sigma pseudo_program pol (bitvector_of_nat ? ppc')) (*∧*) 1643 (ppc' = length … pre)) (*∧ *) 1644 (tech_pc_sigma00 pseudo_program (eject … pol) pre = Some ? 〈ppc',pc'〉)) (*∧*) 1645 (∀id. occurs_exactly_once id pre → 1646 lookup_def … labels id (zero …) = sigma pseudo_program pol (address_of_word_labels_code_mem pre id))) 1647 (\snd pseudo_program) 1648 (λprefix,i,tl,prf,t. 1649 let 〈labels, ppc_pc_costs〉 ≝ t in 1650 let 〈ppc, pc_costs〉 ≝ ppc_pc_costs in 1651 let 〈pc,costs〉 ≝ pc_costs in 1652 let 〈label, i'〉 ≝ i in 1653 let labels ≝ 1654 match label with 1655 [ None ⇒ labels 1656 | Some label ⇒ 1657 let program_counter_bv ≝ bitvector_of_nat ? pc in 1658 add ? ? labels label program_counter_bv 1659 ] 1660 in 1661 let construct ≝ construct_costs pseudo_program pol ppc pc costs i' in 1662 〈labels, 〈S ppc,construct〉〉) 〈empty_map …, 〈0, 〈0, Stub ? ?〉〉〉 1663 in 1664 let 〈labels, ppc_pc_costs〉 ≝ result in 1665 let 〈ppc,pc_costs〉 ≝ ppc_pc_costs in 1666 let 〈pc, costs〉 ≝ pc_costs in 1667 〈labels, costs〉. 1668 [2: whd generalize in match (sig2 … t); >p >p1 >p2 >p3 * * * #IHn1 #IH0 #IH1 #IH2 1669 generalize in match (refl … construct); cases construct in ⊢ (???% → %); #PC #CODE #JMEQ % [% [%]] 1670 [ <(construct_costs_sigma … costs i1 IHn1) change with (? = ?(\fst construct)) >JMEQ % 1671 | >append_length <IH0 normalize; -IHn1; (*CSC: otherwise it diverges!*) // 1672 | >(tech_pc_sigma00_append_Some … costs … IH1) change with (Some … 〈S ppc,\fst construct〉 = ?) >JMEQ % 1673 | #id normalize nodelta; -labels1; cases label; normalize nodelta 1674 [ #K <address_of_word_labels_code_mem_None [2:@K] @IH2 -IHn1; (*CSC: otherwise it diverges!*) // 1675 | #l #H generalize in match (occurs_exactly_once_Some ???? H) in ⊢ ?; 1676 generalize in match (refl … (eq_identifier ? l id)); cases (eq_identifier … l id) in ⊢ (???% → %); 1677 [ #EQ #_ <(eq_identifier_eq … EQ) check lookup_add_hit. >lookup_insert_hit >address_of_word_labels_code_mem_Some_hit 1678 <IH0 [@IHn1 | <(eq_bv_eq … EQ) in H #H @H] 1679 | #EQ change with (occurs_exactly_once ?? → ?) #K >lookup_insert_miss [2: -IHn1; (*Andrea:XXXX used to work /2/*)>eq_bv_sym >EQ // ] 1680 <(address_of_word_labels_code_mem_Some_miss … EQ … H) @IH2 -IHn1; //]]] 1681 |3: whd % [% [%]] // [>sigma_0//] #id normalize in ⊢ (% → ?); #abs @⊥ // 1682 | generalize in match (sig2 … result) in ⊢ ?; 1683 normalize nodelta in p ⊢ %; -result; >p in ⊢ (match % with [_ ⇒ ?] → ?); 1684 normalize nodelta; >p1 normalize nodelta; >p2; normalize nodelta; * #_; #H @H] 1685 qed. 1686 1687 definition build_maps: 1688 ∀pseudo_program.∀pol:policy pseudo_program. 1689 Σres:((BitVectorTrie Identifier 16) × (BitVectorTrie costlabel 16)). 1618 1690 let 〈labels,costs〉 ≝ res in 1619 1691 ∀id. occurs_exactly_once id (\snd pseudo_program) → 1620 lookup ? ? id labels (zero …) = sigma pseudo_program pol (address_of_word_labels_code_mem (\snd pseudo_program) id)1621 ≝ 1692 lookup ? ? id labels (zero …) = ? (* sigma pseudo_program pol (address_of_word_labels_code_mem (\snd pseudo_program) id) *) 1693 ≝ ?. 1622 1694 λpseudo_program.λpol:policy pseudo_program. 1623 1695 let result ≝ 1624 1696 foldl_strong 1625 1697 (option Identifier × pseudo_instruction) 1626 (λpre. Σres:((BitVectorTrie Word 16) × (nat × (nat × (BitVectorTrie Word16)))).1698 (λpre. Σres:((BitVectorTrie Word 16) × (nat × (nat × (BitVectorTrie costlabel 16)))). 1627 1699 let 〈labels,ppc_pc_costs〉 ≝ res in 1628 1700 let 〈ppc',pc_costs〉 ≝ ppc_pc_costs in -
src/ASM/CostsProof.ma
r1554 r1556 290 290 include alias "arithmetics/nat.ma". 291 291 292 (* Useless now?292 (* 293 293 lemma minus_m_n_minus_minus_plus_1: 294 294 ∀m, n: nat. … … 297 297 /3 by lt_plus_to_minus_r, plus_minus/ 298 298 qed. 299 *) 299 300 300 301 lemma plus_minus_rearrangement_1: … … 313 314 (m - n) + (n - o) = m - o. 314 315 /2 by plus_minus_rearrangement_1/ 315 qed. *)316 qed. 316 317 317 318 (* … … 344 345 normalize @compute_max_trace_any_label_cost_is_ok 345 346 |2: 347 cases the_trace 348 [1: 349 #start_status #final_status #is_next #is_not_return #is_costed 350 normalize nodelta; 351 change with ( 352 let current_instruction_cost ≝ current_instruction_cost start_status in 353 let call_trace_cost ≝ compute_max_trace_label_return_cost cost_labels start_fun_call after_fun_call call_trace in 354 let final_trace_cost ≝ compute_max_trace_any_label_cost cost_labels end_flag after_fun_call final final_trace in 355 call_trace_cost+current_instruction_cost+final_trace_cost 356 ) in ⊢ (??%?); 357 |2: 358 #start_status #final_status #is_next #is_return 359 |3: 360 #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call 361 #status_final #is_next #is_call #is_after_return #fun_call_trace #after_fun_call_trace 362 change with ( 363 let current_instruction_cost ≝ current_instruction_cost status_pre_fun_call in 364 let call_trace_cost ≝ compute_max_trace_label_return_cost cost_labels status_start_fun_call status_after_fun_call fun_call_trace in 365 let final_trace_cost ≝ compute_max_trace_any_label_cost cost_labels end_flag status_after_fun_call status_final after_fun_call_trace in 366 call_trace_cost+current_instruction_cost+final_trace_cost) in ⊢ (??%?); 367 normalize nodelta; 368 >compute_max_trace_label_return_cost_is_ok 369 >compute_max_trace_any_label_cost_is_ok 370 |4: 371 ] 346 372 |3: 347 373 cases the_trace … … 353 379 normalize >compute_max_trace_label_label_cost_is_ok 354 380 >compute_max_trace_label_return_cost_is_ok 381 >plus_minus_rearrangement_1 382 [1: % 383 |2: 384 |3: 385 ] 355 386 ] 356 387 ].
Note: See TracChangeset
for help on using the changeset viewer.