source: src/ASM/ASMCostsSplit.ma @ 2531

Last change on this file since 2531 was 2516, checked in by mckinna, 7 years ago

removed typedefs; restored older versions; moved typedefs to compiler.ma
AssemblyProofSplit? *still* doesn't typecheck: disambiguation errors!

File size: 12.1 KB
Line 
1include "ASM/ASMCosts.ma".
2include "ASM/UtilBranch.ma".
3include alias "arithmetics/nat.ma".
4include alias "basics/logic.ma".
5
6let rec traverse_code_internal
7  (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
8    (program_counter: Word) (program_size: nat)
9      (program_size_invariant: program_size = 0 ∨ nat_of_bitvector … program_counter + program_size = 2^16)
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) ∧
13            (∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k ∧
14               pi1 … (block_cost code_memory pc cost_labels) = lookup_present … k_pres) ≝
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.
18    let new_program_counter' ≝ add 16 (bitvector_of_nat 16 1) program_counter in
19    let cost_mapping ≝ traverse_code_internal code_memory cost_labels new_program_counter' program_size' ? in
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.
23      let cost ≝ block_cost code_memory program_counter cost_labels in
24        cic:/matita/cerco/common/Identifiers/add.fix(0,2,3) ?? cost_mapping lbl cost
25    ] (refl … (lookup_opt … program_counter cost_labels))
26  ] (refl … program_size).
27  [3:
28    cases program_size_invariant
29    [1:
30      #destruct_assm @⊥ -traverse_code_internal destruct
31    |2:
32      #program_size_invariant'
33      %
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 #_
43          inversion program_size'
44          [1:
45            #program_size_refl_0 -traverse_code_internal destruct @⊥ cases neq_assm #assm @assm
46            cut (Some … k = Some … lbl → k = lbl) (* XXX: lemma *)
47            [1:
48              #Some_assm destruct(Some_assm) %
49            |2:
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              ]
62            ]
63          |2:
64            #n' #_ #program_size_refl_Sn' -traverse_code_internal destruct
65            cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (add 16 (bitvector_of_nat 16 1) program_counter))
66            [1:
67              destruct
68              @succ_nat_of_bitvector_half_add_1
69              @le_plus_to_minus_r
70              change with (S ? ≤ ?) >plus_n_Sm
71              <program_size_invariant'
72              @monotonic_le_plus_r
73              @le_S_S @le_S_S @le_O_n
74            |2:
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
92                  <S_assm
93                  change with (? < ?)
94                  @le_neq_to_lt assumption
95                ]
96              |2:
97                generalize in match H2; whd in ⊢ (??% → ?);
98                >plus_n_Sm in ⊢ (% → ?);
99                cut(new_program_counter' = add 16 (bitvector_of_nat 16 1) program_counter)
100                [1: %
101                |2:
102                  #new_program_counter_assm' >new_program_counter_assm'
103                  >S_assm #relevant assumption
104                ]
105              ]
106            ]
107          ]
108        ]
109      |2:
110        #k #k_pres
111        @(eq_identifier_elim … k lbl)
112        [1:
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          ]
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:
126            #program_counter' #ind_hyp' %{program_counter'} %
127            [1:
128              cases ind_hyp' #assm #_ assumption
129            |2:
130              cases ind_hyp' #lookup_opt_assm #ind_hyp'' >ind_hyp''
131              @sym_eq @lookup_present_add_miss assumption
132            ]
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:
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:
189                cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (add 16 (bitvector_of_nat 16 1) program_counter))
190                [1:
191                  destruct
192                  @succ_nat_of_bitvector_half_add_1
193                  @le_plus_to_minus_r
194                  change with (S ? ≤ ?) >plus_n_Sm
195                  <program_size_invariant
196                  @monotonic_le_plus_r
197                  @le_S_S @le_S_S @le_O_n
198                |2:
199                  #Sn_refl_assm >Sn_refl_assm @le_n
200                ]
201              |2:
202                change with (? < ?)
203                @le_neq_to_lt
204                assumption
205              ]
206            ]
207          |2:
208            destruct
209            @(transitive_le … H2)
210            cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (add 16 (bitvector_of_nat 16 1) program_counter))
211            [1:
212              destruct
213              @succ_nat_of_bitvector_half_add_1
214              @le_plus_to_minus_r
215              change with (S ? ≤ ?) >plus_n_Sm
216              <program_size_invariant
217              @monotonic_le_plus_r
218              @le_S_S @le_S_S @le_O_n
219            |2:
220              #S_assm
221              change with (S (S n' + ?) ≤ ?)
222              >plus_n_Sm @monotonic_le_plus_r >S_assm
223              @le_n
224            ]
225          ]
226        ]
227      ]
228    |2:
229      assumption
230    ]
231  |4:
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 %
244        cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (add 16 (bitvector_of_nat 16 1) program_counter))
245        [1:
246          destruct
247          @succ_nat_of_bitvector_half_add_1
248          @le_plus_to_minus_r
249          change with (S ? ≤ ?) >plus_n_Sm
250          <relevant
251          @monotonic_le_plus_r
252          @le_S_S @le_S_S @le_O_n
253        |2:
254          #S_assm
255          cut(new_program_counter' = add … (bitvector_of_nat … 1) program_counter)
256          [1: %
257          |2:
258           #new_program_counter_assm' >new_program_counter_assm'
259           cases program_size_invariant
260           [1:
261             #destruct_assm @⊥ >destruct_assm in program_size_refl; #abs destruct(abs)
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    ]
271  ]
272qed.
273
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 *)
279definition traverse_code:
280  ∀code_memory: BitVectorTrie Byte 16.
281  ∀cost_labels: BitVectorTrie costlabel 16.
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'.
286    Σcost_map: identifier_map CostTag nat.
287      (∀pc,k. nat_of_bitvector … pc < 2^16 → lookup_opt … pc cost_labels = Some … k → present … cost_map k) ∧
288      (∀k. ∀k_pres:present … cost_map k. ∀pc. lookup_opt … pc cost_labels = Some … k →
289          pi1 … (block_cost code_memory pc cost_labels) = lookup_present … k_pres) ≝
290  λcode_memory: BitVectorTrie Byte 16.
291  λcost_labels: BitVectorTrie costlabel 16.
292  λcost_labels_injective.
293    pi1 ? ? (traverse_code_internal code_memory cost_labels (zero …) (2^16) ?).
294  [1:
295    @or_intror %
296  |2:
297    cases (traverse_code_internal ?????)
298    #cost_mapping * #inductive_hypothesis1 #inductive_hypothesis2 %
299    [1:
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      ]
308    |2:
309      #k #k_pres #pc #lookup_opt_assm
310      cases (inductive_hypothesis2 ? k_pres)
311      #program_counter' * #lookup_opt_assm' #block_cost_assm
312      >(cost_labels_injective … lookup_opt_assm lookup_opt_assm')
313      assumption
314    ]
315  ]
316qed.
317   
318definition compute_costs ≝
319  λprogram: list Byte.
320  λcost_labels: BitVectorTrie costlabel 16.
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'.
325    (* let program_size ≝ |program| in *)
326    let code_memory ≝ load_code_memory program in
327      traverse_code code_memory cost_labels cost_labels_injective.
328
329(* use of this defn in ASM/CostsProof.ma is ill-typed *)
330definition ASM_cost_map :
331  ∀p: (list Byte) × (BitVectorTrie costlabel 16).
332  let code_memory ≝ load_code_memory (\fst p) in
333  let a_s ≝ ASM_abstract_status code_memory (\snd p) in
334  ? → as_cost_map a_s ≝
335  λp.
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 (as_cost_get_label ? 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.