source: src/ASM/ASMCostsSplit.ma @ 2899

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