source: src/ASM/ASMCostsSplit.ma @ 1929

Last change on this file since 1929 was 1929, checked in by mulligan, 8 years ago

Simplified proof by removing most of the invariants on the statements all together (reachable_program_counter, good_program), and fixing the size of the total_program_size to be constantly 216.

File size: 11.7 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    deplet 〈carry, new_program_counter'〉 as NEW_PC' ≝ half_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        add … 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 (\snd  (half_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                  <NEW_PC' in S_assm; #relevant <relevant -relevant
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' = \snd (half_add 16 (bitvector_of_nat 16 1) program_counter))
100                [1:
101                  <NEW_PC' %
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 (\snd  (half_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 <NEW_PC' @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 (\snd  (half_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              <NEW_PC' @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 (\snd  (half_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' = \snd (half_add … (bitvector_of_nat … 1) program_counter))
257          [1:
258            <NEW_PC' %
259          |2:
260           #new_program_counter_assm' >new_program_counter_assm'
261           cases program_size_invariant
262           [1:
263             #destruct_assm destruct
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  ∀code_memory: BitVectorTrie Byte 16.
283  ∀cost_labels: BitVectorTrie costlabel 16.
284  ∀cost_labels_injective:
285    ∀pc, pc',l.
286      lookup_opt … pc cost_labels = Some … l → lookup_opt … pc' cost_labels = Some … l →
287        pc = pc'.
288    Σcost_map: identifier_map CostTag nat.
289      (∀pc,k. nat_of_bitvector … pc < 2^16 → lookup_opt … pc cost_labels = Some … k → present … cost_map k) ∧
290      (∀k. ∀k_pres:present … cost_map k. ∀pc. lookup_opt … pc cost_labels = Some … k →
291          pi1 … (block_cost code_memory pc cost_labels) = lookup_present … k_pres) ≝
292  λcode_memory: BitVectorTrie Byte 16.
293  λcost_labels: BitVectorTrie costlabel 16.
294  λcost_labels_injective.
295    pi1 ? ? (traverse_code_internal code_memory cost_labels (zero …) (2^16) ?).
296  [1:
297    @or_intror %
298  |2:
299    cases (traverse_code_internal ?????)
300    #cost_mapping * #inductive_hypothesis1 #inductive_hypothesis2 %
301    [1:
302      #pc #k #pc_program_size_assm
303      @inductive_hypothesis1
304      [1:
305        @le_O_n
306      |2:
307        normalize in match (nat_of_bitvector 16 (zero 16));
308        <plus_n_O assumption
309      ]
310    |2:
311      #k #k_pres #pc #lookup_opt_assm
312      cases (inductive_hypothesis2 ? k_pres)
313      #program_counter' * #lookup_opt_assm' #block_cost_assm
314      >(cost_labels_injective … lookup_opt_assm lookup_opt_assm')
315      assumption
316    ]
317  ]
318qed.
319   
320definition compute_costs ≝
321  λprogram: list Byte.
322  λcost_labels: BitVectorTrie costlabel 16.
323  λcost_labels_injective:
324    ∀pc, pc',l.
325      lookup_opt … pc cost_labels = Some … l → lookup_opt … pc' cost_labels = Some … l →
326        pc = pc'.
327    let program_size ≝ |program| in
328    let code_memory ≝ load_code_memory program in
329      traverse_code code_memory cost_labels cost_labels_injective.
Note: See TracBrowser for help on using the repository browser.