Changeset 1562 for src/ASM


Ignore:
Timestamp:
Nov 25, 2011, 1:20:41 PM (8 years ago)
Author:
mulligan
Message:

new version of assembly, fixed conflict in positivemap.ma, changed erroneous axiom in identifiers.ma

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r1556 r1562  
    16151615   tech_pc_sigma00 program pol (prefix@[〈label,i〉]) = Some … 〈S ppc,\fst (construct_costs program pol … ppc pc costs i)〉.
    16161616
    1617 lemma eq_identifier_eq:
     1617axiom eq_identifier_eq:
    16181618  ∀tag: String.
    16191619  ∀l.
    16201620  ∀r.
    16211621    eq_identifier tag l r = true → l = r.
    1622   #tag #l #r cases l cases r #posl #posr
    1623   cases daemon
    1624 qed.
     1622
     1623axiom neq_identifier_neq:
     1624  ∀tag: String.
     1625  ∀l, r: identifier tag.
     1626    eq_identifier tag l r = false → (l = r → False).
    16251627
    16261628definition build_maps:
     
    16751677     | #l #H generalize in match (occurs_exactly_once_Some ???? H) in ⊢ ?;
    16761678       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 @⊥ // ]
    16821686 | generalize in match (sig2 … result) in ⊢ ?;
    16831687   normalize nodelta in p ⊢ %; -result; >p in ⊢ (match % with [_ ⇒ ?] → ?);
     
    16851689qed.
    16861690
    1687 definition build_maps:
    1688  ∀pseudo_program.∀pol:policy pseudo_program.
    1689   Σres:((BitVectorTrie Identifier 16) × (BitVectorTrie costlabel 16)).
    1690    let 〈labels,costs〉 ≝ res in
    1691     ∀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_strong
    1697     (option Identifier × pseudo_instruction)
    1698     (λpre. Σres:((BitVectorTrie Word 16) × (nat × (nat × (BitVectorTrie costlabel 16)))).
    1699       let 〈labels,ppc_pc_costs〉 ≝ res in
    1700       let 〈ppc',pc_costs〉 ≝ ppc_pc_costs in
    1701       let 〈pc',costs〉 ≝ pc_costs in
    1702        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 in
    1711       let 〈ppc, pc_costs〉 ≝ ppc_pc_costs in
    1712       let 〈pc,costs〉 ≝ pc_costs in
    1713        let 〈label, i'〉 ≝ i in
    1714        let labels ≝
    1715          match label with
    1716          [ None ⇒ labels
    1717          | Some label ⇒
    1718            let program_counter_bv ≝ bitvector_of_nat ? pc in
    1719              insert ? ? label program_counter_bv labels]
    1720        in
    1721          let construct ≝ construct_costs pseudo_program pol ppc pc costs i' in
    1722           〈labels, 〈S ppc,construct〉〉
    1723     ) 〈(Stub ? ?), 〈0, 〈0, Stub ? ?〉〉〉
    1724   in
    1725    let 〈labels, ppc_pc_costs〉 ≝ result in
    1726    let 〈ppc,pc_costs〉 ≝ ppc_pc_costs in
    1727    let 〈pc, costs〉 ≝ pc_costs in
    1728     〈labels, costs〉.
    1729  [2: whd generalize in match (sig2 … t) >p >p1 >p2 >p3 * * * #IHn1 #IH0 #IH1 #IH2
    1730    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 nodelta
    1735      [ #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_hit
    1739           <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 
    17481691definition assembly:
    1749  ∀p:pseudo_assembly_program. policy p → list Byte × (BitVectorTrie Identifier 16) ≝
     1692 ∀p:pseudo_assembly_program. policy p → list Byte × (BitVectorTrie costlabel 16) ≝
    17501693  λp.let 〈preamble, instr_list〉 ≝ p in
    17511694   λpol.
    17521695    let 〈labels,costs〉 ≝ build_maps 〈preamble,instr_list〉 pol in
    17531696    let datalabels ≝ construct_datalabels preamble in
    1754     let lookup_labels ≝ λx. lookup ? ? x labels (zero ?) in
    1755     let lookup_datalabels ≝ λx. lookup ? ? x datalabels (zero ?) in
     1697    let lookup_labels ≝ λx. lookup_def … labels x (zero ?) in
     1698    let lookup_datalabels ≝ λx. lookup_def … datalabels x (zero ?) in
    17561699    let result ≝
    17571700     foldl_strong
Note: See TracChangeset for help on using the changeset viewer.