- Timestamp:
- Nov 25, 2011, 1:20:41 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Assembly.ma
r1556 r1562 1615 1615 tech_pc_sigma00 program pol (prefix@[〈label,i〉]) = Some … 〈S ppc,\fst (construct_costs program pol … ppc pc costs i)〉. 1616 1616 1617 lemmaeq_identifier_eq:1617 axiom eq_identifier_eq: 1618 1618 ∀tag: String. 1619 1619 ∀l. 1620 1620 ∀r. 1621 1621 eq_identifier tag l r = true → l = r. 1622 #tag #l #r cases l cases r #posl #posr 1623 cases daemon 1624 qed. 1622 1623 axiom neq_identifier_neq: 1624 ∀tag: String. 1625 ∀l, r: identifier tag. 1626 eq_identifier tag l r = false → (l = r → False). 1625 1627 1626 1628 definition build_maps: … … 1675 1677 | #l #H generalize in match (occurs_exactly_once_Some ???? H) in ⊢ ?; 1676 1678 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 @⊥ // 1679 [ #EQ #_ <(eq_identifier_eq … EQ) >lookup_def_add_hit >address_of_word_labels_code_mem_Some_hit 1680 <IH0 [@IHn1 | <(eq_identifier_eq … EQ) in H; #H @H] 1681 | #EQ change with (occurs_exactly_once ?? → ?) #K >lookup_def_add_miss [2: -IHn1; 1682 (*Andrea:XXXX used to work /2/*)@nmk #IDL lapply (sym_eq ? ? ? IDL) 1683 lapply (neq_identifier_neq ? ? ? EQ) #ASSM assumption ] 1684 <(address_of_word_labels_code_mem_Some_miss … EQ … H) @IH2 assumption ]]] 1685 |3: whd % [% [%]] [>sigma_0 % | % | % | #id normalize in ⊢ (% → ?); #abs @⊥ // ] 1682 1686 | generalize in match (sig2 … result) in ⊢ ?; 1683 1687 normalize nodelta in p ⊢ %; -result; >p in ⊢ (match % with [_ ⇒ ?] → ?); … … 1685 1689 qed. 1686 1690 1687 definition build_maps:1688 ∀pseudo_program.∀pol:policy pseudo_program.1689 Σres:((BitVectorTrie Identifier 16) × (BitVectorTrie costlabel 16)).1690 let 〈labels,costs〉 ≝ res in1691 ∀id. occurs_exactly_once id (\snd pseudo_program) →1692 lookup ? ? id labels (zero …) = ? (* sigma pseudo_program pol (address_of_word_labels_code_mem (\snd pseudo_program) id) *)1693 ≝ ?.1694 λpseudo_program.λpol:policy pseudo_program.1695 let result ≝1696 foldl_strong1697 (option Identifier × pseudo_instruction)1698 (λpre. Σres:((BitVectorTrie Word 16) × (nat × (nat × (BitVectorTrie costlabel 16)))).1699 let 〈labels,ppc_pc_costs〉 ≝ res in1700 let 〈ppc',pc_costs〉 ≝ ppc_pc_costs in1701 let 〈pc',costs〉 ≝ pc_costs in1702 And ( And (1703 And (bitvector_of_nat ? pc' = sigma pseudo_program pol (bitvector_of_nat ? ppc')) (*∧*)1704 (ppc' = length … pre)) (*∧ *)1705 (tech_pc_sigma00 pseudo_program (eject … pol) pre = Some ? 〈ppc',pc'〉)) (*∧*)1706 (∀id. occurs_exactly_once id pre →1707 lookup ?? id labels (zero …) = sigma pseudo_program pol (address_of_word_labels_code_mem pre id)))1708 (\snd pseudo_program)1709 (λprefix,i,tl,prf,t.1710 let 〈labels, ppc_pc_costs〉 ≝ t in1711 let 〈ppc, pc_costs〉 ≝ ppc_pc_costs in1712 let 〈pc,costs〉 ≝ pc_costs in1713 let 〈label, i'〉 ≝ i in1714 let labels ≝1715 match label with1716 [ None ⇒ labels1717 | Some label ⇒1718 let program_counter_bv ≝ bitvector_of_nat ? pc in1719 insert ? ? label program_counter_bv labels]1720 in1721 let construct ≝ construct_costs pseudo_program pol ppc pc costs i' in1722 〈labels, 〈S ppc,construct〉〉1723 ) 〈(Stub ? ?), 〈0, 〈0, Stub ? ?〉〉〉1724 in1725 let 〈labels, ppc_pc_costs〉 ≝ result in1726 let 〈ppc,pc_costs〉 ≝ ppc_pc_costs in1727 let 〈pc, costs〉 ≝ pc_costs in1728 〈labels, costs〉.1729 [2: whd generalize in match (sig2 … t) >p >p1 >p2 >p3 * * * #IHn1 #IH0 #IH1 #IH21730 generalize in match (refl … construct); cases construct in ⊢ (???% → %) #PC #CODE #JMEQ % [% [%]]1731 [ <(construct_costs_sigma … costs i1 IHn1) change with (? = ?(\fst construct)) >JMEQ %1732 | >append_length <IH0 normalize; -IHn1; (*CSC: otherwise it diverges!*) //1733 | >(tech_pc_sigma00_append_Some … costs … IH1) change with (Some … 〈S ppc,\fst construct〉 = ?) >JMEQ %1734 | #id normalize nodelta; -labels1; cases label; normalize nodelta1735 [ #K <address_of_word_labels_code_mem_None [2:@K] @IH2 -IHn1; (*CSC: otherwise it diverges!*) //1736 | #l #H generalize in match (occurs_exactly_once_Some ???? H) in ⊢ ?;1737 generalize in match (refl … (eq_bv ? l id)); cases (eq_bv … l id) in ⊢ (???% → %)1738 [ #EQ #_ <(eq_bv_eq … EQ) >lookup_insert_hit >address_of_word_labels_code_mem_Some_hit1739 <IH0 [@IHn1 | <(eq_bv_eq … EQ) in H #H @H]1740 | #EQ change with (occurs_exactly_once ?? → ?) #K >lookup_insert_miss [2: -IHn1; (*Andrea:XXXX used to work /2/*)>eq_bv_sym >EQ // ]1741 <(address_of_word_labels_code_mem_Some_miss … EQ … H) @IH2 -IHn1; //]]]1742 |3: whd % [% [%]] // [>sigma_0//] #id normalize in ⊢ (% → ?) #abs @⊥ //1743 | generalize in match (sig2 … result) in ⊢ ?;1744 normalize nodelta in p ⊢ %; -result; >p in ⊢ (match % with [_ ⇒ ?] → ?)1745 normalize nodelta; >p1 normalize nodelta; >p2; normalize nodelta; * #_; #H @H]1746 qed.1747 1748 1691 definition assembly: 1749 ∀p:pseudo_assembly_program. policy p → list Byte × (BitVectorTrie Identifier16) ≝1692 ∀p:pseudo_assembly_program. policy p → list Byte × (BitVectorTrie costlabel 16) ≝ 1750 1693 λp.let 〈preamble, instr_list〉 ≝ p in 1751 1694 λpol. 1752 1695 let 〈labels,costs〉 ≝ build_maps 〈preamble,instr_list〉 pol in 1753 1696 let datalabels ≝ construct_datalabels preamble in 1754 let lookup_labels ≝ λx. lookup ? ? x labels(zero ?) in1755 let lookup_datalabels ≝ λx. lookup ? ? x datalabels(zero ?) in1697 let lookup_labels ≝ λx. lookup_def … labels x (zero ?) in 1698 let lookup_datalabels ≝ λx. lookup_def … datalabels x (zero ?) in 1756 1699 let result ≝ 1757 1700 foldl_strong
Note: See TracChangeset
for help on using the changeset viewer.