source: src/ASM/ASMCostsSplit.ma @ 2051

Last change on this file since 2051 was 2001, checked in by campbell, 8 years ago

Get the compiler to output more.

File size: 12.1 KB
RevLine 
[1895]1include "ASM/ASMCosts.ma".
[1928]2include "ASM/UtilBranch.ma".
[1895]3include alias "arithmetics/nat.ma".
4include alias "basics/logic.ma".
[1946]5
[1895]6let rec traverse_code_internal
7  (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
[1929]8    (program_counter: Word) (program_size: nat)
9      (program_size_invariant: program_size = 0 ∨ nat_of_bitvector … program_counter + program_size = 2^16)
[1895]10        on program_size:
11          Σcost_map: identifier_map CostTag nat.
12            (∀pc,k. nat_of_bitvector … program_counter ≤ nat_of_bitvector 16 pc → nat_of_bitvector … pc < program_size + nat_of_bitvector … program_counter → lookup_opt … pc cost_labels = Some … k → present … cost_map k) ∧
[1899]13            (∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k ∧
[1929]14               pi1 … (block_cost code_memory pc cost_labels) = lookup_present … k_pres) ≝
[1895]15  match program_size return λx. x = program_size → Σcost_map: ?. ? with
16  [ O ⇒ λprogram_size_refl. empty_map CostTag nat
17  | S program_size' ⇒ λprogram_size_refl.
[1946]18    let new_program_counter' ≝ add 16 (bitvector_of_nat 16 1) program_counter in
[1929]19    let cost_mapping ≝ traverse_code_internal code_memory cost_labels new_program_counter' program_size' ? in
[1895]20    match lookup_opt … program_counter cost_labels return λx. x = lookup_opt … program_counter cost_labels → Σcost_map: ?. ? with
21    [ None ⇒ λlookup_refl. pi1 … cost_mapping
22    | Some lbl ⇒ λlookup_refl.
[1929]23      let cost ≝ block_cost code_memory program_counter cost_labels in
[1946]24        cic:/matita/cerco/common/Identifiers/add.fix(0,2,2) ?? cost_mapping lbl cost
[1896]25    ] (refl … (lookup_opt … program_counter cost_labels))
[1895]26  ] (refl … program_size).
[1929]27  [3:
[1896]28    cases program_size_invariant
29    [1:
30      #destruct_assm @⊥ -traverse_code_internal destruct
[1895]31    |2:
[1896]32      #program_size_invariant'
33      %
[1895]34      [1:
35        #pc #k #H1 #H2 #lookup_opt_assm @(eq_identifier_elim … k lbl)
36        [1:
37          #eq_assm >eq_assm
38          cases cost_mapping #cost_mapping' * #ind_hyp #_
39          @present_add_hit
40        |2:
41          #neq_assm @present_add_miss try assumption
42          cases cost_mapping #cost_mapping' * #ind_hyp #_
[1896]43          inversion program_size'
[1895]44          [1:
[1896]45            #program_size_refl_0 -traverse_code_internal destruct @⊥ cases neq_assm #assm @assm
46            cut (Some … k = Some … lbl → k = lbl) (* XXX: lemma *)
[1895]47            [1:
[1896]48              #Some_assm destruct(Some_assm) %
[1895]49            |2:
[1896]50              #Some_assm @Some_assm <lookup_opt_assm >lookup_refl
51              >(?:pc=program_counter)
52              [1:
53                %
54              |2:
55                @refl_nat_of_bitvector_to_refl
56                @le_to_le_to_eq
57                try assumption
58                change with (? ≤ ?) in H2;
59                @le_S_S_to_le
60                assumption
61              ]
[1895]62            ]
63          |2:
[1896]64            #n' #_ #program_size_refl_Sn' -traverse_code_internal destruct
[1946]65            cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (add 16 (bitvector_of_nat 16 1) program_counter))
[1895]66            [1:
[1896]67              destruct
68              @succ_nat_of_bitvector_half_add_1
69              @le_plus_to_minus_r
[1897]70              change with (S ? ≤ ?) >plus_n_Sm
[1929]71              <program_size_invariant'
[1897]72              @monotonic_le_plus_r
73              @le_S_S @le_S_S @le_O_n
[1895]74            |2:
[1896]75              #S_assm
76              @(ind_hyp … lookup_opt_assm)
77              [1:
78                @(eqb_elim (nat_of_bitvector … program_counter)
79                  (nat_of_bitvector … pc))
80                [1:
81                  #eqb_refl_assm
82                  -ind_hyp -H1 -H2
83                  lapply (refl_nat_of_bitvector_to_refl 16 program_counter pc eqb_refl_assm)
84                  #program_counter_refl_assm -eqb_refl_assm
85                  <program_counter_refl_assm in lookup_opt_assm; <lookup_refl
86                  #Some_assm destruct(Some_assm)
87                  cases neq_assm #absurd_assm
88                  cases (absurd_assm (refl … k))
89                |2:
90                  #eqb_ref_assm
91                  -ind_hyp
[1946]92                  <S_assm
[1896]93                  change with (? < ?)
94                  @le_neq_to_lt assumption
95                ]
96              |2:
97                generalize in match H2; whd in ⊢ (??% → ?);
98                >plus_n_Sm in ⊢ (% → ?);
[1946]99                cut(new_program_counter' = add 16 (bitvector_of_nat 16 1) program_counter)
100                [1: %
[1896]101                |2:
102                  #new_program_counter_assm' >new_program_counter_assm'
103                  >S_assm #relevant assumption
104                ]
105              ]
[1895]106            ]
107          ]
108        ]
109      |2:
110        #k #k_pres
111        @(eq_identifier_elim … k lbl)
112        [1:
[1899]113          #eq_assm %{program_counter} %
114          [1:
115            >eq_assm >lookup_refl %
116          |2:
117            >eq_assm in k_pres ⊢ (???%); #k_pres >lookup_present_add_hit %
118          ]
[1895]119        |2:
120          #neq_assm
121          cases cost_mapping in k_pres; #cost_mapping' #ind_hyp #present_assm
122          cases ind_hyp #_ #relevant cases (relevant k ?)
123          [2:
124            @(present_add_present … present_assm) assumption
125          |1:
[1899]126            #program_counter' #ind_hyp' %{program_counter'} %
127            [1:
128              cases ind_hyp' #assm #_ assumption
129            |2:
[1929]130              cases ind_hyp' #lookup_opt_assm #ind_hyp'' >ind_hyp''
[1899]131              @sym_eq @lookup_present_add_miss assumption
132            ]
[1895]133          ]
134        ]
135      ]
136    ]
137  |1:
138    %
139    [1:
140      #pc #k #absurd1 #absurd2
141      @⊥ lapply(lt_to_not_le … absurd2) *
142      #absurd @absurd assumption
143    |2:
144      #k #k_pres
145      @⊥ normalize in k_pres; /2/
146    ]
147  |2:
148    cases cost_mapping
149    -traverse_code_internal #cost_mapping *
150    #inductive_hypothesis1 #inductive_hypothesis2 %
151    [1:
[1896]152      #pc #k #H1 #H2
153      cases program_size_invariant
154      [1:
155        #destruct_assm @⊥ destruct
156      |2:
157        -program_size_invariant #program_size_invariant
158        inversion program_size'
159        [1:
160          #program_size_refl_0 destruct
161          #lookup_opt_Some_assm
162          >(?:pc = program_counter) in lookup_opt_Some_assm;
163          [1:
164            #absurd <lookup_refl in absurd;
165            #absurd destruct
166          |2:
167            @refl_nat_of_bitvector_to_refl
168            @le_to_le_to_eq
169            try assumption
170            change with (? ≤ ?) in H2;
171            @le_S_S_to_le
172            assumption
173          ]
174        |2:
175          #n' #_ #program_size_Sn_refl #Some_lookup_opt_refl
176          @(inductive_hypothesis1 … pc) try assumption
177          [1:
178            @(eqb_elim … (nat_of_bitvector … program_counter)
179              (nat_of_bitvector … pc));
180            [1:
181              #eq_assm
182              lapply (refl_nat_of_bitvector_to_refl … eq_assm) #pc_refl
183              <pc_refl in Some_lookup_opt_refl; <lookup_refl #absurd
184              destruct
185            |2:
186              #neq_assm
187              @(transitive_le ? (S (nat_of_bitvector … program_counter)))
188              [1:
[1946]189                cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (add 16 (bitvector_of_nat 16 1) program_counter))
[1896]190                [1:
191                  destruct
192                  @succ_nat_of_bitvector_half_add_1
193                  @le_plus_to_minus_r
[1897]194                  change with (S ? ≤ ?) >plus_n_Sm
[1929]195                  <program_size_invariant
[1897]196                  @monotonic_le_plus_r
197                  @le_S_S @le_S_S @le_O_n
[1896]198                |2:
[1946]199                  #Sn_refl_assm >Sn_refl_assm @le_n
[1896]200                ]
201              |2:
202                change with (? < ?)
203                @le_neq_to_lt
204                assumption
205              ]
206            ]
207          |2:
208            destruct
209            @(transitive_le … H2)
[1946]210            cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (add 16 (bitvector_of_nat 16 1) program_counter))
[1896]211            [1:
[1897]212              destruct
[1896]213              @succ_nat_of_bitvector_half_add_1
214              @le_plus_to_minus_r
[1897]215              change with (S ? ≤ ?) >plus_n_Sm
[1929]216              <program_size_invariant
[1897]217              @monotonic_le_plus_r
218              @le_S_S @le_S_S @le_O_n
[1896]219            |2:
220              #S_assm
221              change with (S (S n' + ?) ≤ ?)
222              >plus_n_Sm @monotonic_le_plus_r >S_assm
[1946]223              @le_n
[1896]224            ]
225          ]
226        ]
227      ]
[1895]228    |2:
229      assumption
230    ]
[1929]231  |4:
[1896]232    inversion program_size'
233    [1:
234      #_ %1 %
235    |2:
236      #n' #_ #program_size_refl_Sn @or_intror
237      cases program_size_invariant
238      [1:
239        #absurd destruct
240      |2:
241        #relevant <relevant <plus_n_Sm <program_size_refl <plus_n_Sm
242        @eq_f >program_size_refl_Sn <plus_n_Sm
243        change with (? = (S ?) + ?) @eq_f2 try %
[1946]244        cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (add 16 (bitvector_of_nat 16 1) program_counter))
[1896]245        [1:
[1897]246          destruct
[1896]247          @succ_nat_of_bitvector_half_add_1
248          @le_plus_to_minus_r
[1897]249          change with (S ? ≤ ?) >plus_n_Sm
[1929]250          <relevant
[1897]251          @monotonic_le_plus_r
252          @le_S_S @le_S_S @le_O_n
[1896]253        |2:
254          #S_assm
[1946]255          cut(new_program_counter' = add … (bitvector_of_nat … 1) program_counter)
256          [1: %
[1896]257          |2:
258           #new_program_counter_assm' >new_program_counter_assm'
259           cases program_size_invariant
260           [1:
[1946]261             #destruct_assm @⊥ >destruct_assm in program_size_refl; #abs destruct(abs)
[1896]262           |2:
263             #program_size_invariant
264             <program_size_invariant <program_size_refl
265             <S_assm normalize <plus_n_Sm %
266           ]
267         ]
268      ]
269    ]
270    ]
[1895]271  ]
272qed.
273
[1929]274(* XXX:
275 * At the moment we do a full traversal of the code memory, however we could do
276 * a fold over the domain of the cost labels map.
277 *
278 *)
[1895]279definition traverse_code:
280  ∀code_memory: BitVectorTrie Byte 16.
281  ∀cost_labels: BitVectorTrie costlabel 16.
[1899]282  ∀cost_labels_injective:
283    ∀pc, pc',l.
284      lookup_opt … pc cost_labels = Some … l → lookup_opt … pc' cost_labels = Some … l →
285        pc = pc'.
[1895]286    Σcost_map: identifier_map CostTag nat.
[1929]287      (∀pc,k. nat_of_bitvector … pc < 2^16 → lookup_opt … pc cost_labels = Some … k → present … cost_map k) ∧
[1899]288      (∀k. ∀k_pres:present … cost_map k. ∀pc. lookup_opt … pc cost_labels = Some … k →
[1929]289          pi1 … (block_cost code_memory pc cost_labels) = lookup_present … k_pres) ≝
[1895]290  λcode_memory: BitVectorTrie Byte 16.
291  λcost_labels: BitVectorTrie costlabel 16.
[1899]292  λcost_labels_injective.
[1929]293    pi1 ? ? (traverse_code_internal code_memory cost_labels (zero …) (2^16) ?).
[1897]294  [1:
295    @or_intror %
296  |2:
[1929]297    cases (traverse_code_internal ?????)
[1897]298    #cost_mapping * #inductive_hypothesis1 #inductive_hypothesis2 %
299    [1:
[1899]300      #pc #k #pc_program_size_assm
301      @inductive_hypothesis1
302      [1:
303        @le_O_n
304      |2:
305        normalize in match (nat_of_bitvector 16 (zero 16));
306        <plus_n_O assumption
307      ]
[1897]308    |2:
[1899]309      #k #k_pres #pc #lookup_opt_assm
310      cases (inductive_hypothesis2 ? k_pres)
[1929]311      #program_counter' * #lookup_opt_assm' #block_cost_assm
[1899]312      >(cost_labels_injective … lookup_opt_assm lookup_opt_assm')
[1929]313      assumption
[1897]314    ]
315  ]
316qed.
317   
[1895]318definition compute_costs ≝
319  λprogram: list Byte.
320  λcost_labels: BitVectorTrie costlabel 16.
[1899]321  λcost_labels_injective:
322    ∀pc, pc',l.
323      lookup_opt … pc cost_labels = Some … l → lookup_opt … pc' cost_labels = Some … l →
324        pc = pc'.
[1897]325    let program_size ≝ |program| in
[1895]326    let code_memory ≝ load_code_memory program in
[1946]327      traverse_code code_memory cost_labels cost_labels_injective.
[2001]328
329definition object_code ≝ list Byte.
330definition costlabel_map ≝ BitVectorTrie costlabel 16.     
331
332definition ASM_cost_map :
333  ∀p.let code_memory ≝ load_code_memory (\fst p) in
334  ? → as_cost_map (ASM_abstract_status code_memory (\snd p)) ≝
335  λp : object_code × costlabel_map.
336  λcost_labels_injective.
337  let cost_map ≝ compute_costs (\fst p) (\snd p) cost_labels_injective in
338  λl_sig.
339  lookup_present … cost_map l_sig ?.
340  cases cost_map
341  #m * #prf #_ cases l_sig cases daemon (*bla bla*)
342  qed.
Note: See TracBrowser for help on using the repository browser.