Changeset 1562
 Timestamp:
 Nov 25, 2011, 1:20:41 PM (9 years ago)
 Location:
 src
 Files:

 3 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 
src/common/Identifiers.ma
r1535 r1562 59 59 qed. 60 60 61 axiom eq_identifier_sym: 62 ∀tag: String. 63 ∀l : identifier tag. 64 ∀r : identifier tag. 65 eq_identifier tag l r = eq_identifier tag r l. 66 61 67 lemma eq_identifier_false : ∀tag,x,y. x≠y → eq_identifier tag x y = false. 62 68 #tag * #x * #y #NE normalize @not_eq_to_eqb_false /2/ … … 105 111 qed. 106 112 113 lemma lookup_def_add_hit : ∀tag,A,m,i,a,d. 114 lookup_def tag A (add tag A m i a) i d = a. 115 #tag #A * #m * #i #a #d 116 @lookup_insert_hit 117 qed. 118 107 119 lemma lookup_add_miss : ∀tag,A,m,i,j,a. 108 120 i ≠ j → … … 111 123 @lookup_opt_insert_miss /2/ 112 124 qed. 125 126 axiom lookup_def_add_miss : ∀tag,A,m,i,j,a,d. 127 i ≠ j → 128 lookup_def tag A (add tag A m j a) i d = lookup_def tag A m i d. 113 129 114 130 lemma lookup_add_oblivious : ∀tag,A,m,i,j,a. 
src/common/PositiveMap.ma
r1555 r1562 24 24  Some r ⇒ r 25 25 ]. 26 26 27 27 let rec insert (A:Type[0]) (b:Pos) (a:A) (t:positive_map A) on b : positive_map A ≝ 28 28 match b with … … 77 77 ] 78 78 ] qed. 79 80 axiom lookup_insert_hit: 81 ∀a: Type[0]. 82 ∀v: a. 83 ∀b: Pos. 84 ∀t: positive_map a. 85 ∀d: a. 86 lookup … b (insert … b v t) d = v. 79 87 80 88 lemma lookup_opt_insert_miss:
Note: See TracChangeset
for help on using the changeset viewer.