source: src/ASM/ASMCostsSplit.ma @ 1928

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

Moved code from in ASM/ASMCosts*.ma and ASM/CostsProof.ma that should rightfully be in another file. Added a new file, ASM/UtilBranch.ma for code that should rightfully be in ASM/Util.ma but is incomplete (i.e. daemons).

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