# source:src/ASM/ASMCostsSplit.ma@1921

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

Horror proof mostly finished (compiles all way until end of CostsProof?.ma).

File size: 19.2 KB
Line
1include "ASM/ASMCosts.ma".
2include alias "arithmetics/nat.ma".
3include alias "basics/logic.ma".
4
5
6(* Also extracts an equality proof (useful when not using Russell). *)
7notation > "hvbox('let' 〈ident x,ident y〉 'as' ident E 'return' ty ≝ t 'in' s)"
8 with precedence 10
9for @{ match \$t return λx.∀\${ident E}: x = \$t. \$ty with [ mk_Prod \${ident x} \${ident y} ⇒
10        λ\${ident E}.\$s ] (refl ? \$t) }.
11
12(*
13lemma test:
14  ∀c: nat × nat.
15    Σx: nat. ∃y: nat. c = 〈x, y〉 ≝
16  λc: nat × nat. let 〈left, right〉 as T return Σx: ?. ? ≝ c in left.
17*)
18
19notation > "hvbox('deplet' 〈ident x,ident y〉 'as' ident E  ≝ t 'in' s)"
20 with precedence 10
21for @{ match \$t return λx.∀\${ident E}: x = \$t. Σz: ?. ? with [ mk_Prod \${ident x} \${ident y} ⇒
22        λ\${ident E}.\$s ] (refl ? \$t) }.
23
24(*
25notation > "hvbox('let' 〈ident x,ident y,ident z〉 'as' ident E ≝ t 'in' s)"
26 with precedence 10
27for @{ match \$t return λx.x = \$t → ? with [ mk_Prod \${fresh xy} \${ident z} ⇒
28       match \${fresh xy} return λx. ? = \$t → ? with [ mk_Prod \${ident x} \${ident y} ⇒
29        λ\${ident E}.\$s ] ] (refl ? \$t) }. *)
30
31notation > "hvbox('deplet' 〈ident x,ident y,ident z〉 'as' ident E ≝ t 'in' s)"
32 with precedence 10
33for @{ match \$t return λx.∀\${fresh w}:x = \$t. Σq: ?. ? with [ mk_Prod \${fresh xy} \${ident z} ⇒
34       match \${fresh xy} return λx.∀\${ident E}:? = \$t. Σu: ?. ? with [ mk_Prod \${ident x} \${ident y} ⇒
35        λ\${ident E}.\$s ] ] (refl ? \$t) }.
36
37notation > "hvbox('let' 〈ident x,ident y,ident z〉 'as' ident E 'return' ty ≝ t 'in' s)"
38 with precedence 10
39for @{ match \$t return λx.∀\${fresh w}:x = \$t. Σq: ?. ? with [ mk_Prod \${fresh xy} \${ident z} ⇒
40       match \${fresh xy} return λx.∀\${ident E}:? = \$t. \$ty with [ mk_Prod \${ident x} \${ident y} ⇒
41        λ\${ident E}.\$s ] ] (refl ? \$t) }.
42
43definition nat_of_bool: bool → nat ≝
44  λb: bool.
45  match b with
46  [ true ⇒ 1
47  | false ⇒ 0
48  ].
49
50lemma blah:
51  ∀n: nat.
52  ∀bv: BitVector n.
53  ∀buffer: nat.
54    nat_of_bitvector_aux n buffer bv = nat_of_bitvector n bv + (buffer * 2^n).
55  #n #bv elim bv
56  [1:
57    #buffer elim buffer try %
58    #buffer' #inductive_hypothesis
59    normalize <times_n_1 %
60  |2:
61    #n' #hd #tl #inductive_hypothesis
62    #buffer cases hd normalize
63    >inductive_hypothesis
64    >inductive_hypothesis
65    [1:
66      change with (
67        ? + (2 * buffer + 1) * ?) in ⊢ (??%?);
68      change with (
69        ? + buffer * (2 * 2^n')) in ⊢ (???%);
70      cases daemon
71    ]
72  ]
73  cases daemon
74qed.
75
76lemma nat_of_bitvector_aux_hd_tl:
77  ∀n: nat.
78  ∀tl: BitVector n.
79  ∀hd: bool.
80    nat_of_bitvector (S n) (hd:::tl) =
81      nat_of_bitvector n tl + (nat_of_bool hd * 2^n).
82  #n #tl elim tl
83  [1:
84    #hd cases hd %
85  |2:
86    #n' #hd' #tl' #inductive_hypothesis #hd
87    cases hd whd in ⊢ (??%?); normalize nodelta
88    >inductive_hypothesis cases hd' normalize nodelta
89    normalize in match (nat_of_bool ?);
90    normalize in match (nat_of_bool ?);
91    [4:
92      normalize in match (2 * ?);
93      <plus_n_O <plus_n_O %
94    |3:
95      normalize in match (2 * ?);
96      normalize in match (0 + 1);
97      <plus_n_O
98      normalize in match (1 * ?);
99      <plus_n_O
100      cases daemon
101      (* XXX: lemma *)
102    |*:
103      cases daemon
104    ]
105  ]
106qed.
107
109  ∀n: nat.
110  ∀bv: BitVector n.
111  ∀buffer: nat.
112  ∀power_proof: nat_of_bitvector … bv < 2^n - 1.
113    S (nat_of_bitvector_aux n buffer bv) =
114      nat_of_bitvector … (\snd (half_add n (bitvector_of_nat … 1) bv)).
115  #n #bv elim bv
116  [1:
117    #buffer normalize #absurd
118    cases (lt_to_not_zero … absurd)
119  |2:
120    #n' #hd #tl #inductive_hypothesis #buffer
121    cases daemon
122  ]
123qed.
124
126  ∀n: nat.
127  ∀bv: BitVector n.
128  ∀power_proof: nat_of_bitvector … bv < 2^n - 1.
129    S (nat_of_bitvector … bv) = nat_of_bitvector …
130      (\snd (half_add n (bitvector_of_nat … 1) bv)).
131  #n #bv elim bv
132  [1:
133    normalize #absurd
134    cases (lt_to_not_zero … absurd)
135  |2:
136    #n' #hd #tl #inductive_hypothesis
137    cases daemon
138  ]
139qed.
140
141include alias "arithmetics/nat.ma".
142include alias "basics/logic.ma".
143
144let rec traverse_code_internal
145  (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
146    (program_counter: Word) (fixed_program_size: nat) (program_size: nat)
147      (reachable_program_counter_witness:
148          ∀lbl: costlabel.
149          ∀program_counter: Word. Some … lbl = lookup_opt … program_counter cost_labels →
150            reachable_program_counter code_memory fixed_program_size program_counter)
151        (good_program_witness: good_program code_memory fixed_program_size)
152        (program_size_invariant: program_size = 0 ∨ nat_of_bitvector … program_counter + program_size = fixed_program_size)
153        (fixed_program_size_limit: fixed_program_size ≤ 2^16)
154        on program_size:
155          Σcost_map: identifier_map CostTag nat.
156            (∀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) ∧
157            (∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k ∧
158              ∃reachable_witness: reachable_program_counter code_memory fixed_program_size pc.
159                pi1 … (block_cost code_memory pc fixed_program_size fixed_program_size_limit cost_labels reachable_witness good_program_witness) = lookup_present … k_pres) ≝
160  match program_size return λx. x = program_size → Σcost_map: ?. ? with
161  [ O ⇒ λprogram_size_refl. empty_map CostTag nat
162  | S program_size' ⇒ λprogram_size_refl.
163    deplet 〈carry, new_program_counter'〉 as NEW_PC' ≝ half_add 16 (bitvector_of_nat 16 1) program_counter in
164    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
165    match lookup_opt … program_counter cost_labels return λx. x = lookup_opt … program_counter cost_labels → Σcost_map: ?. ? with
166    [ None ⇒ λlookup_refl. pi1 … cost_mapping
167    | Some lbl ⇒ λlookup_refl.
168      let cost ≝ block_cost code_memory program_counter fixed_program_size fixed_program_size_limit cost_labels ? good_program_witness in
169        add … cost_mapping lbl cost
170    ] (refl … (lookup_opt … program_counter cost_labels))
171  ] (refl … program_size).
172  [5:
173    assumption
174  |4:
175    @(reachable_program_counter_witness lbl)
176    @lookup_refl
177  |3:
178    cases program_size_invariant
179    [1:
180      #destruct_assm @⊥ -traverse_code_internal destruct
181    |2:
182      #program_size_invariant'
183      %
184      [1:
185        #pc #k #H1 #H2 #lookup_opt_assm @(eq_identifier_elim … k lbl)
186        [1:
187          #eq_assm >eq_assm
188          cases cost_mapping #cost_mapping' * #ind_hyp #_
190        |2:
192          cases cost_mapping #cost_mapping' * #ind_hyp #_
193          inversion program_size'
194          [1:
195            #program_size_refl_0 -traverse_code_internal destruct @⊥ cases neq_assm #assm @assm
196            cut (Some … k = Some … lbl → k = lbl) (* XXX: lemma *)
197            [1:
198              #Some_assm destruct(Some_assm) %
199            |2:
200              #Some_assm @Some_assm <lookup_opt_assm >lookup_refl
201              >(?:pc=program_counter)
202              [1:
203                %
204              |2:
205                @refl_nat_of_bitvector_to_refl
206                @le_to_le_to_eq
207                try assumption
208                change with (? ≤ ?) in H2;
209                @le_S_S_to_le
210                assumption
211              ]
212            ]
213          |2:
214            #n' #_ #program_size_refl_Sn' -traverse_code_internal destruct
215            cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (\snd  (half_add 16 (bitvector_of_nat 16 1) program_counter)))
216            [1:
217              destruct
219              @le_plus_to_minus_r
220              @(transitive_le … fixed_program_size_limit)
221              change with (S ? ≤ ?) >plus_n_Sm
222              @monotonic_le_plus_r
223              @le_S_S @le_S_S @le_O_n
224            |2:
225              #S_assm
226              @(ind_hyp … lookup_opt_assm)
227              [1:
228                @(eqb_elim (nat_of_bitvector … program_counter)
229                  (nat_of_bitvector … pc))
230                [1:
231                  #eqb_refl_assm
232                  -ind_hyp -H1 -H2
233                  lapply (refl_nat_of_bitvector_to_refl 16 program_counter pc eqb_refl_assm)
234                  #program_counter_refl_assm -eqb_refl_assm
235                  <program_counter_refl_assm in lookup_opt_assm; <lookup_refl
236                  #Some_assm destruct(Some_assm)
237                  cases neq_assm #absurd_assm
238                  cases (absurd_assm (refl … k))
239                |2:
240                  #eqb_ref_assm
241                  -ind_hyp
242                  <NEW_PC' in S_assm; #relevant <relevant -relevant
243                  change with (? < ?)
244                  @le_neq_to_lt assumption
245                ]
246              |2:
247                generalize in match H2; whd in ⊢ (??% → ?);
248                >plus_n_Sm in ⊢ (% → ?);
249                cut(new_program_counter' = \snd (half_add 16 (bitvector_of_nat 16 1) program_counter))
250                [1:
251                  <NEW_PC' %
252                |2:
253                  #new_program_counter_assm' >new_program_counter_assm'
254                  >S_assm #relevant assumption
255                ]
256              ]
257            ]
258          ]
259        ]
260      |2:
261        #k #k_pres
262        @(eq_identifier_elim … k lbl)
263        [1:
264          #eq_assm %{program_counter} %
265          [1:
266            >eq_assm >lookup_refl %
267          |2:
268            %{(reachable_program_counter_witness …)} try assumption
269            >eq_assm in k_pres ⊢ (???%); #k_pres >lookup_present_add_hit %
270          ]
271        |2:
272          #neq_assm
273          cases cost_mapping in k_pres; #cost_mapping' #ind_hyp #present_assm
274          cases ind_hyp #_ #relevant cases (relevant k ?)
275          [2:
277          |1:
278            #program_counter' #ind_hyp' %{program_counter'} %
279            [1:
280              cases ind_hyp' #assm #_ assumption
281            |2:
282              cases ind_hyp' #lookup_opt_assm * #reachable_witness'
283              #ind_hyp'' %{reachable_witness'} >ind_hyp''
285            ]
286          ]
287        ]
288      ]
289    ]
290  |1:
291    %
292    [1:
293      #pc #k #absurd1 #absurd2
294      @⊥ lapply(lt_to_not_le … absurd2) *
295      #absurd @absurd assumption
296    |2:
297      #k #k_pres
298      @⊥ normalize in k_pres; /2/
299    ]
300  |2:
301    cases cost_mapping
302    -traverse_code_internal #cost_mapping *
303    #inductive_hypothesis1 #inductive_hypothesis2 %
304    [1:
305      #pc #k #H1 #H2
306      cases program_size_invariant
307      [1:
308        #destruct_assm @⊥ destruct
309      |2:
310        -program_size_invariant #program_size_invariant
311        inversion program_size'
312        [1:
313          #program_size_refl_0 destruct
314          #lookup_opt_Some_assm
315          >(?:pc = program_counter) in lookup_opt_Some_assm;
316          [1:
317            #absurd <lookup_refl in absurd;
318            #absurd destruct
319          |2:
320            @refl_nat_of_bitvector_to_refl
321            @le_to_le_to_eq
322            try assumption
323            change with (? ≤ ?) in H2;
324            @le_S_S_to_le
325            assumption
326          ]
327        |2:
328          #n' #_ #program_size_Sn_refl #Some_lookup_opt_refl
329          @(inductive_hypothesis1 … pc) try assumption
330          [1:
331            @(eqb_elim … (nat_of_bitvector … program_counter)
332              (nat_of_bitvector … pc));
333            [1:
334              #eq_assm
335              lapply (refl_nat_of_bitvector_to_refl … eq_assm) #pc_refl
336              <pc_refl in Some_lookup_opt_refl; <lookup_refl #absurd
337              destruct
338            |2:
339              #neq_assm
340              @(transitive_le ? (S (nat_of_bitvector … program_counter)))
341              [1:
342                cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (\snd  (half_add 16 (bitvector_of_nat 16 1) program_counter)))
343                [1:
344                  destruct
346                  @le_plus_to_minus_r
347                  @(transitive_le … fixed_program_size_limit)
348                  change with (S ? ≤ ?) >plus_n_Sm
349                  @monotonic_le_plus_r
350                  @le_S_S @le_S_S @le_O_n
351                |2:
352                  #Sn_refl_assm >Sn_refl_assm <NEW_PC' @le_n
353                ]
354              |2:
355                change with (? < ?)
356                @le_neq_to_lt
357                assumption
358              ]
359            ]
360          |2:
361            destruct
362            @(transitive_le … H2)
363            cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (\snd  (half_add 16 (bitvector_of_nat 16 1) program_counter)))
364            [1:
365              destruct
367              @le_plus_to_minus_r
368              @(transitive_le … fixed_program_size_limit)
369              change with (S ? ≤ ?) >plus_n_Sm
370              @monotonic_le_plus_r
371              @le_S_S @le_S_S @le_O_n
372            |2:
373              #S_assm
374              change with (S (S n' + ?) ≤ ?)
375              >plus_n_Sm @monotonic_le_plus_r >S_assm
376              <NEW_PC' @le_n
377            ]
378          ]
379        ]
380      ]
381    |2:
382      assumption
383    ]
384  |6:
385    inversion program_size'
386    [1:
387      #_ %1 %
388    |2:
389      #n' #_ #program_size_refl_Sn @or_intror
390      cases program_size_invariant
391      [1:
392        #absurd destruct
393      |2:
394        #relevant <relevant <plus_n_Sm <program_size_refl <plus_n_Sm
395        @eq_f >program_size_refl_Sn <plus_n_Sm
396        change with (? = (S ?) + ?) @eq_f2 try %
397        cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (\snd  (half_add 16 (bitvector_of_nat 16 1) program_counter)))
398        [1:
399          destruct
401          @le_plus_to_minus_r
402          @(transitive_le … fixed_program_size_limit)
403          change with (S ? ≤ ?) >plus_n_Sm
404          @monotonic_le_plus_r
405          @le_S_S @le_S_S @le_O_n
406        |2:
407          #S_assm
408          cut(new_program_counter' = \snd (half_add … (bitvector_of_nat … 1) program_counter))
409          [1:
410            <NEW_PC' %
411          |2:
412           #new_program_counter_assm' >new_program_counter_assm'
413           cases program_size_invariant
414           [1:
415             #destruct_assm destruct
416           |2:
417             #program_size_invariant
418             <program_size_invariant <program_size_refl
419             <S_assm normalize <plus_n_Sm %
420           ]
421         ]
422      ]
423    ]
424    ]
425  ]
426qed.
427
428(*
429let rec traverse_code_internal
430  (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
431    (program_counter: Word) (fixed_program_size: nat) (program_size: nat)
432      (reachable_program_counter_witness:
433          ∀lbl: costlabel.
434          ∀program_counter: Word. Some … lbl = lookup_opt … program_counter cost_labels →
435            reachable_program_counter code_memory fixed_program_size program_counter)
436        (good_program_witness: good_program code_memory fixed_program_size)
437        (program_size_invariant: program_size = 0 ∨ nat_of_bitvector … program_counter + program_size = fixed_program_size)
438        (fixed_program_size_limit: fixed_program_size < 2^16)
439        on program_size:
440          Σcost_map: identifier_map CostTag nat.
441            (∀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) ∧
442            (∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k →
443              ∃reachable_witness: reachable_program_counter code_memory fixed_program_size pc.
444                pi1 … (block_cost code_memory pc fixed_program_size cost_labels reachable_witness good_program_witness) = lookup_present … k_pres) ≝
445*)
446
447definition traverse_code:
448  ∀code_memory: BitVectorTrie Byte 16.
449  ∀cost_labels: BitVectorTrie costlabel 16.
450  ∀cost_labels_injective:
451    ∀pc, pc',l.
452      lookup_opt … pc cost_labels = Some … l → lookup_opt … pc' cost_labels = Some … l →
453        pc = pc'.
454  ∀program_size: nat.
455  ∀program_size_limit: program_size ≤ 2^16.
456  ∀reachable_program_counter_witness:
457    ∀lbl: costlabel.
458    ∀program_counter: Word. Some … lbl = lookup_opt … program_counter cost_labels →
459      reachable_program_counter code_memory program_size program_counter.
460  ∀good_program_witness: good_program code_memory program_size.
461    Σcost_map: identifier_map CostTag nat.
462      (∀pc,k. nat_of_bitvector … pc < program_size → lookup_opt … pc cost_labels = Some … k → present … cost_map k) ∧
463      (∀k. ∀k_pres:present … cost_map k. ∀pc. lookup_opt … pc cost_labels = Some … k →
464        ∃reachable_witness: reachable_program_counter code_memory program_size pc.
465          pi1 … (block_cost code_memory pc program_size program_size_limit cost_labels reachable_witness good_program_witness) = lookup_present … k_pres) ≝
466  λcode_memory: BitVectorTrie Byte 16.
467  λcost_labels: BitVectorTrie costlabel 16.
468  λcost_labels_injective.
469  λprogram_size: nat.
470  λprogram_size_limit: program_size ≤ 2^16.
471  λreachable_program_counter_witness:
472          ∀lbl: costlabel.
473          ∀program_counter: Word. Some … lbl = lookup_opt … program_counter cost_labels →
474            reachable_program_counter code_memory program_size program_counter.
475  λgood_program_witness: good_program code_memory program_size.
476    pi1 ? ? (traverse_code_internal code_memory cost_labels (zero …) program_size program_size reachable_program_counter_witness good_program_witness ? program_size_limit).
477  [1:
478    @or_intror %
479  |2:
480    cases (traverse_code_internal ? ? ? ? ? ? ? ? ?)
481    #cost_mapping * #inductive_hypothesis1 #inductive_hypothesis2 %
482    [1:
483      #pc #k #pc_program_size_assm
484      @inductive_hypothesis1
485      [1:
486        @le_O_n
487      |2:
488        normalize in match (nat_of_bitvector 16 (zero 16));
489        <plus_n_O assumption
490      ]
491    |2:
492      #k #k_pres #pc #lookup_opt_assm
493      cases (inductive_hypothesis2 ? k_pres)
494      #program_counter' * #lookup_opt_assm' * #reachable_witness
495      #block_cost_assm
496      >(cost_labels_injective … lookup_opt_assm lookup_opt_assm')
497      %{reachable_witness} assumption
498    ]
499  ]
500qed.
501
502definition compute_costs ≝
503  λprogram: list Byte.
504  λcost_labels: BitVectorTrie costlabel 16.
505  λcost_labels_injective:
506    ∀pc, pc',l.
507      lookup_opt … pc cost_labels = Some … l → lookup_opt … pc' cost_labels = Some … l →
508        pc = pc'.
509  λreachable_program_witness.
510  λgood_program_witness: good_program (load_code_memory program) (|program|).
511  λprogram_size_limit: |program| ≤ 2^16.
512    let program_size ≝ |program| in
513    let code_memory ≝ load_code_memory program in
514      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.