source: src/ASM/ASMCostsSplit.ma @ 2999

Last change on this file since 2999 was 2999, checked in by sacerdot, 7 years ago

code_memory added to labelled_object_code to avoid recomputing it every time.
This gives a major speed up in the semantics of the extracted code.

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