Changeset 989 for src/ASM/Assembly.ma


Ignore:
Timestamp:
Jun 17, 2011, 10:28:19 AM (8 years ago)
Author:
sacerdot
Message:

Type of build_maps strengthened.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r987 r989  
    657657    jump_expansion_internal n' program new_labels new_policy ].
    658658
     659(**************************************** START OF POLICY ABSTRACTION ********************)
     660
    659661definition policy_type ≝ Word → jump_length.
    660662
     
    798800    → False.
    799801
    800 definition build_maps ≝
     802definition build_maps:
     803 ∀pseudo_program.∀pol:policy pseudo_program.
     804  Σres:((BitVectorTrie Word 16) × (BitVectorTrie Word 16)).
     805   let 〈labels,costs〉 ≝ res in
     806    ∀id. occurs_exactly_once id (\snd pseudo_program) →
     807     lookup ?? id labels (zero …) = sigma pseudo_program pol (address_of_word_labels_code_mem (\snd pseudo_program) id)
     808 ≝
    801809  λpseudo_program.λpol:policy pseudo_program.
    802810  let result ≝
     
    838846   let 〈pc, costs〉 ≝ pc_costs in
    839847    〈labels, costs〉.
    840  [3: whd % [% [%]] // [>sigma_0//] #id normalize in ⊢ (% → ?) #abs @⊥ //
    841  | whd generalize in match (sig2 … t) >p >p1 >p2 >p3 * * * #IHn1 #IH0 #IH1 #IH2
     848 [4: whd % [% [%]] // [>sigma_0//] #id normalize in ⊢ (% → ?) #abs @⊥ //
     849 |2: whd generalize in match (sig2 … t) >p >p1 >p2 >p3 * * * #IHn1 #IH0 #IH1 #IH2
    842850   cases construct in p4 #PC #CODE #JMEQ % [% [%]]
    843851   [ @(construct_costs_sigma … IHn1) [4: <JMEQ % |*: skip]
     
    852860        | #EQ change with (occurs_exactly_once ?? → ?) #K >lookup_insert_miss [2: -IHn1; /2/]
    853861          <(address_of_word_labels_code_mem_Some_miss … EQ … H) @IH2 -IHn1; //]]]
    854  | (* dummy case *) @⊥ generalize in match (sig2 … t) >p >p1 >p2 >p3 * *; #IH0 #IH1 #IH2
    855    @(tech_pc_sigma00_append_None … IH1 (jmeq_to_eq ??? p4)) ]
     862 |3: (* dummy case *) @⊥ generalize in match (sig2 … t) >p >p1 >p2 >p3 * *; #IH0 #IH1 #IH2
     863   @(tech_pc_sigma00_append_None … IH1 (jmeq_to_eq ??? p4))
     864 | generalize in match (sig2 … result) >p normalize nodelta; >p1 normalize nodelta;
     865   >p2; normalize nodelta; * #_; #H @H]
    856866qed.
    857 
    858 (*
    859 lemma build_maps_ok:
    860  ∀p:pseudo_assembly_program.
    861   let 〈labels,costs〉 ≝ build_maps' p in
    862    ∀pc.
    863     (nat_of_bitvector … pc) < length … (\snd p) →
    864      lookup ?? pc labels (zero …) = sigma p (\snd (fetch_pseudo_instruction (\snd p) pc)).
    865  #p cases p #preamble #instr_list
    866   elim instr_list
    867    [ whd #pc #abs normalize in abs; cases (not_le_Sn_O ?) [#H cases (H abs) ]
    868    | #hd #tl #IH
    869     whd in ⊢ (match % with [ _ ⇒ ?])
    870    ]
    871 qed.
    872 *)
    873867
    874868definition assembly: ∀p:pseudo_assembly_program. policy p → option (list Byte × (BitVectorTrie Identifier 16)) ≝
Note: See TracChangeset for help on using the changeset viewer.