1 | include "ASM/ASMCosts.ma". |
---|
2 | include alias "arithmetics/nat.ma". |
---|
3 | include alias "basics/logic.ma". |
---|
4 | |
---|
5 | |
---|
6 | (* Also extracts an equality proof (useful when not using Russell). *) |
---|
7 | notation > "hvbox('let' 〈ident x,ident y〉 'as' ident E 'return' ty ≝ t 'in' s)" |
---|
8 | with precedence 10 |
---|
9 | for @{ match $t return λx.∀${ident E}: x = $t. $ty with [ mk_Prod ${ident x} ${ident y} ⇒ |
---|
10 | λ${ident E}.$s ] (refl ? $t) }. |
---|
11 | |
---|
12 | (* |
---|
13 | lemma 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 | |
---|
19 | notation > "hvbox('deplet' 〈ident x,ident y〉 'as' ident E ≝ t 'in' s)" |
---|
20 | with precedence 10 |
---|
21 | for @{ match $t return λx.∀${ident E}: x = $t. Σz: ?. ? with [ mk_Prod ${ident x} ${ident y} ⇒ |
---|
22 | λ${ident E}.$s ] (refl ? $t) }. |
---|
23 | |
---|
24 | (* |
---|
25 | notation > "hvbox('let' 〈ident x,ident y,ident z〉 'as' ident E ≝ t 'in' s)" |
---|
26 | with precedence 10 |
---|
27 | for @{ 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 | |
---|
31 | notation > "hvbox('deplet' 〈ident x,ident y,ident z〉 'as' ident E ≝ t 'in' s)" |
---|
32 | with precedence 10 |
---|
33 | for @{ 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 | |
---|
37 | notation > "hvbox('let' 〈ident x,ident y,ident z〉 'as' ident E 'return' ty ≝ t 'in' s)" |
---|
38 | with precedence 10 |
---|
39 | for @{ 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 | (* |
---|
44 | lemma 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 | |
---|
57 | lemma 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 | |
---|
71 | lemma 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 | |
---|
85 | lemma 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/ |
---|
93 | qed. |
---|
94 | |
---|
95 | lemma 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/ |
---|
103 | qed. *) |
---|
104 | |
---|
105 | |
---|
106 | let 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 | ] |
---|
246 | qed. |
---|
247 | |
---|
248 | definition 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 | |
---|
271 | definition 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 |
---|
280 | qed. |
---|