source: src/ASM/ASMCostsSplit.ma @ 1895

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

Split the ASMCosts files while working on traverse_code_internal. A lot of refactoring of the proof.

File size: 11.5 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
43(*
44lemma test:
45  ∀b: nat.
46  ∀c: nat × nat.
47    Σx: nat. ∃y: nat. c = 〈y, x〉 ≝
48  λb: nat.
49  λc: nat × nat.
50  match b return λb': nat. ∀r:b' = b. Σx: ?. ? with
51  [ O ⇒ λr.
52    let 〈left, right〉 as T return Σz:nat.∃y. c = 〈y,z〉 ≝ c in
53    deplet 〈left', right'〉 as T' ≝ c in left'
54  | S n ⇒ λr. deplet 〈left, right〉 as T ≝ c in left
55  ] (refl … b).
56
57lemma test:
58  ∀b: nat.
59  ∀c: nat × nat.
60    Σx: nat. ∃y: nat. c = 〈y, x〉 ≝
61  λb: nat.
62  λc: nat × nat.
63  match b return λb': nat. b' = b → Σx: ?. ? with
64  [ O ⇒ λr.
65    deplet 〈left, right〉 as T ≝ c in
66    deplet 〈left', right'〉 as T' ≝ c in
67      left'
68  | S n ⇒ λr. deplet 〈left, right〉 as T ≝ c in left
69  ] (refl … b).
70
71lemma test:
72  ∀b: nat.
73  ∀c: nat × nat × nat.
74    Σx: nat. ∃y: nat × nat. c = 〈y, x〉 ≝
75  λb: nat.
76  λc: nat × nat × nat.
77  match b return λb': nat. b' = b → Σx: ?. ? with
78  [ O ⇒ λr.
79    deplet 〈left, centre, right〉 as T ≝ c in
80    deplet 〈left', centre', right'〉 as T' ≝ c in
81      left'
82  | S n ⇒ λr. deplet 〈left, centre, right〉 as T ≝ c in left
83  ] (refl … b).
84
85lemma pair_elim_as:
86  ∀A,B,C: Type[0].
87  ∀p.
88  ∀T: ∀a: A. ∀b: B. 〈a, b〉 = p → C.
89  ∀P: A×B → C → Prop.
90    (∀lft, rgt. ∀H: 〈lft,rgt〉 = p. P 〈lft,rgt〉 (T lft rgt H)) →
91      P p (let 〈lft, rgt〉 as H ≝ p in T lft rgt H).
92 #A #B #C * /2/
93qed.
94
95lemma triple_elim_as:
96  ∀A,B,C,D: Type[0].
97  ∀p.
98  ∀T: ∀a: A. ∀b: B. ∀c: C. 〈a, b, c〉 = p → D.
99  ∀P: A×B×C → D → Prop.
100    (∀lft, cntr, rgt. ∀H: 〈lft,cntr,rgt〉 = p. P 〈lft,cntr,rgt〉 (T lft cntr rgt H)) →
101      P p (let 〈lft, cntr, rgt〉 as H ≝ p in T lft cntr rgt H).
102 #A #B #C #D * * /2/
103qed. *)
104
105
106let rec traverse_code_internal
107  (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
108    (program_counter: Word) (fixed_program_size: nat) (program_size: nat)
109      (reachable_program_counter_witness:
110          ∀lbl: costlabel.
111          ∀program_counter: Word. Some … lbl = lookup_opt … program_counter cost_labels →
112            reachable_program_counter code_memory fixed_program_size program_counter)
113        (good_program_witness: good_program code_memory fixed_program_size)
114        (program_size_invariant: nat_of_bitvector … program_counter + program_size = fixed_program_size)
115        (fixed_program_size_limit: fixed_program_size < 2^16 - 1)
116        on program_size:
117          Σcost_map: identifier_map CostTag nat.
118            (∀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) ∧
119            (∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k →
120              ∃reachable_witness: reachable_program_counter code_memory fixed_program_size pc.
121                pi1 … (block_cost code_memory pc fixed_program_size cost_labels reachable_witness good_program_witness) = lookup_present … k_pres) ≝
122  match program_size return λx. x = program_size → Σcost_map: ?. ? with
123  [ O ⇒ λprogram_size_refl. empty_map CostTag nat
124  | S program_size' ⇒ λprogram_size_refl.
125    (deplet 〈instruction, new_program_counter, ticks〉 as FETCH ≝ fetch … code_memory program_counter in
126    deplet 〈carry, new_program_counter'〉 as NEW_PC' ≝ half_add 16 (bitvector_of_nat 16 1) program_counter in
127    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
128    match lookup_opt … program_counter cost_labels return λx. x = lookup_opt … program_counter cost_labels → Σcost_map: ?. ? with
129    [ None ⇒ λlookup_refl. pi1 … cost_mapping
130    | Some lbl ⇒ λlookup_refl.
131      let cost ≝ block_cost code_memory program_counter fixed_program_size cost_labels ? good_program_witness in
132        add … cost_mapping lbl cost
133    ] (refl … (lookup_opt … program_counter cost_labels)))
134  ] (refl … program_size).
135  [5:
136    assumption
137  |4:
138    @(reachable_program_counter_witness lbl)
139    @lookup_refl
140  |3,6:
141    cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (\snd  (half_add 16 (bitvector_of_nat 16 1) program_counter)))
142    [1,3:
143      destruct
144      @succ_nat_of_bitvector_half_add_1
145      @(plus_lt_to_lt ? (S program_size') (2^16 - 1))
146      assumption 
147    |2:
148      #S_assm %
149      [1:
150        #pc #k #H1 #H2 #lookup_opt_assm @(eq_identifier_elim … k lbl)
151        [1:
152          #eq_assm >eq_assm
153          cases cost_mapping #cost_mapping' * #ind_hyp #_
154          @present_add_hit
155        |2:
156          #neq_assm @present_add_miss try assumption
157          cases cost_mapping #cost_mapping' * #ind_hyp #_
158          @(ind_hyp … lookup_opt_assm)
159          [1:
160            generalize in match (eqb_decidable (nat_of_bitvector … program_counter)
161              (nat_of_bitvector … pc));
162            #hyp cases hyp
163            [1:
164              #eqb_assm generalize in match (eqb_true_to_refl … eqb_assm);
165              #eqb_refl_assm
166              -eqb_assm -hyp -ind_hyp -H1 -H2
167              lapply (refl_nat_of_bitvector_to_refl 16 program_counter pc eqb_refl_assm)
168              #program_counter_refl_assm -eqb_refl_assm
169              <program_counter_refl_assm in lookup_opt_assm; <lookup_refl
170              #Some_assm destruct(Some_assm)
171              cases neq_assm #absurd_assm
172              cases (absurd_assm (refl … k))
173            |2:
174              #eqb_assm generalize in match (eqb_false_to_not_refl … eqb_assm);
175              #eqb_refl_assm
176              -eqb_assm -hyp -ind_hyp -H1 -H2 -cost_mapping -traverse_code_internal
177              <NEW_PC' in S_assm; #relevant <relevant -relevant
178              change with (? < ?) (* XXX: open here *)
179            ]
180          |2:
181            generalize in match H2; <program_size_refl whd in ⊢ (??% → ?);
182            >plus_n_Sm in ⊢ (% → ?);
183            cut(new_program_counter' = \snd (half_add 16 (bitvector_of_nat 16 1) program_counter))
184            [1:
185              <NEW_PC' %
186            |2:
187              #new_program_counter_assm' >new_program_counter_assm'
188              >S_assm #relevant assumption
189            ]
190          ]
191        ]
192      |2:
193        #k #k_pres
194        @(eq_identifier_elim … k lbl)
195        [1:
196          #eq_assm %{program_counter} #lookup_opt_assm
197          %{(reachable_program_counter_witness …)} try assumption
198          >eq_assm in k_pres ⊢ (???%); #k_pres >lookup_present_add_hit %
199        |2:
200          #neq_assm
201          cases cost_mapping in k_pres; #cost_mapping' #ind_hyp #present_assm
202          cases ind_hyp #_ #relevant cases (relevant k ?)
203          [2:
204            @(present_add_present … present_assm) assumption
205          |1:
206            #program_counter' #ind_hyp' %{program_counter'}
207            #relevant cases (ind_hyp' relevant) #reachable_witness'
208            #ind_hyp'' %{reachable_witness'} >ind_hyp''
209            @sym_eq @lookup_present_add_miss assumption
210          ]
211        ]
212      ]
213    |4:
214      #S_assm
215      cut(new_program_counter' = \snd (half_add … (bitvector_of_nat … 1) program_counter))
216      [1:
217        <NEW_PC' %
218      |2:
219        #new_program_counter_assm' >new_program_counter_assm'
220        <program_size_invariant <program_size_refl
221        <S_assm normalize <plus_n_Sm %
222      ]
223    ]
224  |1:
225    %
226    [1:
227      #pc #k #absurd1 #absurd2
228      @⊥ lapply(lt_to_not_le … absurd2) *
229      #absurd @absurd assumption
230    |2:
231      #k #k_pres
232      @⊥ normalize in k_pres; /2/
233    ]
234  |2:
235    cases cost_mapping
236    -traverse_code_internal #cost_mapping *
237    #inductive_hypothesis1 #inductive_hypothesis2 %
238    [1:
239      #pc #k #H1 #H2 @inductive_hypothesis1
240      try assumption
241      (* XXX: same goal as above *)
242    |2:
243      assumption
244    ]
245  ]
246qed.
247
248definition traverse_code:
249  ∀code_memory: BitVectorTrie Byte 16.
250  ∀cost_labels: BitVectorTrie costlabel 16.
251  ∀program_size: nat.
252  ∀reachable_program_counter_witness:
253    ∀lbl: costlabel.
254    ∀program_counter: Word. Some … lbl = lookup_opt … program_counter cost_labels →
255      reachable_program_counter code_memory program_size program_counter.
256  ∀good_program_witness: good_program code_memory program_size.
257    Σcost_map: identifier_map CostTag nat.
258      (∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k →
259        ∃reachable_witness: reachable_program_counter code_memory program_size pc.
260          pi1 … (block_cost code_memory pc program_size cost_labels reachable_witness good_program_witness) = lookup_present … k_pres) ≝
261  λcode_memory: BitVectorTrie Byte 16.
262  λcost_labels: BitVectorTrie costlabel 16.
263  λprogram_size: nat.
264  λreachable_program_counter_witness:
265          ∀lbl: costlabel.
266          ∀program_counter: Word. Some … lbl = lookup_opt … program_counter cost_labels →
267            reachable_program_counter code_memory program_size program_counter.
268  λgood_program_witness: good_program code_memory program_size.
269    traverse_code_internal code_memory cost_labels (zero …) program_size program_size reachable_program_counter_witness good_program_witness.
270 
271definition compute_costs ≝
272  λprogram: list Byte.
273  λcost_labels: BitVectorTrie costlabel 16.
274  λreachable_program_witness.
275  λgood_program_witness: good_program (load_code_memory program) (|program| + 1).
276    let program_size ≝ |program| + 1 in
277    let code_memory ≝ load_code_memory program in
278      traverse_code code_memory cost_labels program_size reachable_program_witness ?.
279  @good_program_witness
280qed.
Note: See TracBrowser for help on using the repository browser.