1 | include "ASM/ASM.ma". |
---|
2 | include "ASM/Arithmetic.ma". |
---|
3 | include "ASM/Fetch.ma". |
---|
4 | include "ASM/Interpret.ma". |
---|
5 | include "common/StructuredTraces.ma". |
---|
6 | |
---|
7 | let rec fetch_program_counter_n |
---|
8 | (n: nat) (code_memory: BitVectorTrie Byte 16) (program_counter: Word) |
---|
9 | on n: option Word ≝ |
---|
10 | match n with |
---|
11 | [ O ⇒ Some … program_counter |
---|
12 | | S n ⇒ |
---|
13 | match fetch_program_counter_n n code_memory program_counter with |
---|
14 | [ None ⇒ None … |
---|
15 | | Some tail_pc ⇒ |
---|
16 | let 〈instr, program_counter, ticks〉 ≝ fetch code_memory tail_pc in |
---|
17 | if ltb (nat_of_bitvector … tail_pc) (nat_of_bitvector … program_counter) then |
---|
18 | Some … program_counter |
---|
19 | else |
---|
20 | None Word (* XXX: overflow! *) |
---|
21 | ] |
---|
22 | ]. |
---|
23 | |
---|
24 | definition reachable_program_counter: BitVectorTrie Byte 16 → nat → Word → Prop ≝ |
---|
25 | λcode_memory: BitVectorTrie Byte 16. |
---|
26 | λprogram_size: nat. |
---|
27 | λprogram_counter: Word. |
---|
28 | (∃n: nat. Some … program_counter = fetch_program_counter_n n code_memory (zero 16)) ∧ |
---|
29 | nat_of_bitvector 16 program_counter < program_size. |
---|
30 | |
---|
31 | definition well_labelling: BitVectorTrie costlabel 16 → Prop ≝ |
---|
32 | λcost_labels. |
---|
33 | injective … (λx. lookup_opt … x cost_labels). |
---|
34 | |
---|
35 | definition good_program: ∀code_memory: BitVectorTrie Byte 16. ∀total_program_size: nat. Prop ≝ |
---|
36 | λcode_memory: BitVectorTrie Byte 16. |
---|
37 | λtotal_program_size: nat. |
---|
38 | ∀program_counter: Word. |
---|
39 | ∀good_program_counter_witness: reachable_program_counter code_memory total_program_size program_counter. |
---|
40 | let 〈instruction, program_counter', ticks〉 ≝ fetch code_memory program_counter in |
---|
41 | match instruction with |
---|
42 | [ RealInstruction instr ⇒ |
---|
43 | match instr with |
---|
44 | [ RET ⇒ True |
---|
45 | | JC relative ⇒ True (* XXX: see below *) |
---|
46 | | JNC relative ⇒ True (* XXX: see below *) |
---|
47 | | JB bit_addr relative ⇒ True |
---|
48 | | JNB bit_addr relative ⇒ True |
---|
49 | | JBC bit_addr relative ⇒ True |
---|
50 | | JZ relative ⇒ True |
---|
51 | | JNZ relative ⇒ True |
---|
52 | | CJNE src_trgt relative ⇒ True |
---|
53 | | DJNZ src_trgt relative ⇒ True |
---|
54 | | _ ⇒ |
---|
55 | nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧ |
---|
56 | nat_of_bitvector … program_counter' < total_program_size |
---|
57 | ] |
---|
58 | | LCALL addr ⇒ |
---|
59 | match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Prop with |
---|
60 | [ ADDR16 addr ⇒ λaddr16: True. |
---|
61 | reachable_program_counter code_memory total_program_size addr ∧ |
---|
62 | nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧ |
---|
63 | nat_of_bitvector … program_counter' < total_program_size |
---|
64 | | _ ⇒ λother: False. ⊥ |
---|
65 | ] (subaddressing_modein … addr) |
---|
66 | | ACALL addr ⇒ |
---|
67 | match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Prop with |
---|
68 | [ ADDR11 addr ⇒ λaddr11: True. |
---|
69 | let 〈pc_bu, pc_bl〉 ≝ split … 8 8 program_counter' in |
---|
70 | let 〈thr, eig〉 ≝ split … 3 8 addr in |
---|
71 | let 〈fiv, thr'〉 ≝ split … 5 3 pc_bu in |
---|
72 | let new_program_counter ≝ (fiv @@ thr) @@ pc_bl in |
---|
73 | reachable_program_counter code_memory total_program_size new_program_counter ∧ |
---|
74 | nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧ |
---|
75 | nat_of_bitvector … program_counter' < total_program_size |
---|
76 | | _ ⇒ λother: False. ⊥ |
---|
77 | ] (subaddressing_modein … addr) |
---|
78 | | AJMP addr ⇒ |
---|
79 | match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Prop with |
---|
80 | [ ADDR11 addr ⇒ λaddr11: True. |
---|
81 | let 〈pc_bu, pc_bl〉 ≝ split … 8 8 program_counter' in |
---|
82 | let 〈nu, nl〉 ≝ split … 4 4 pc_bu in |
---|
83 | let bit ≝ get_index' … O ? nl in |
---|
84 | let 〈relevant1, relevant2〉 ≝ split … 3 8 addr in |
---|
85 | let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in |
---|
86 | let 〈carry, new_program_counter〉 ≝ half_add 16 program_counter new_addr in |
---|
87 | reachable_program_counter code_memory total_program_size new_program_counter |
---|
88 | | _ ⇒ λother: False. ⊥ |
---|
89 | ] (subaddressing_modein … addr) |
---|
90 | | LJMP addr ⇒ |
---|
91 | match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Prop with |
---|
92 | [ ADDR16 addr ⇒ λaddr16: True. |
---|
93 | reachable_program_counter code_memory total_program_size addr |
---|
94 | | _ ⇒ λother: False. ⊥ |
---|
95 | ] (subaddressing_modein … addr) |
---|
96 | | SJMP addr ⇒ |
---|
97 | match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → Prop with |
---|
98 | [ RELATIVE addr ⇒ λrelative: True. |
---|
99 | let 〈carry, new_program_counter〉 ≝ half_add … program_counter' (sign_extension addr) in |
---|
100 | reachable_program_counter code_memory total_program_size new_program_counter |
---|
101 | | _ ⇒ λother: False. ⊥ |
---|
102 | ] (subaddressing_modein … addr) |
---|
103 | | JMP addr ⇒ (* XXX: JMP is used for fptrs and unconstrained *) |
---|
104 | nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧ |
---|
105 | nat_of_bitvector … program_counter' < total_program_size |
---|
106 | | MOVC src trgt ⇒ |
---|
107 | nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧ |
---|
108 | nat_of_bitvector … program_counter' < total_program_size |
---|
109 | ]. |
---|
110 | cases other |
---|
111 | qed. |
---|
112 | |
---|
113 | lemma is_a_decidable: |
---|
114 | ∀hd. |
---|
115 | ∀element. |
---|
116 | is_a hd element = true ∨ is_a hd element = false. |
---|
117 | #hd #element // |
---|
118 | qed. |
---|
119 | |
---|
120 | lemma mem_decidable: |
---|
121 | ∀n: nat. |
---|
122 | ∀v: Vector addressing_mode_tag n. |
---|
123 | ∀element: addressing_mode_tag. |
---|
124 | mem … eq_a n v element = true ∨ |
---|
125 | mem … eq_a … v element = false. |
---|
126 | #n #v #element // |
---|
127 | qed. |
---|
128 | |
---|
129 | lemma eq_a_elim: |
---|
130 | ∀tag. |
---|
131 | ∀hd. |
---|
132 | ∀P: bool → Prop. |
---|
133 | (tag = hd → P (true)) → |
---|
134 | (tag ≠ hd → P (false)) → |
---|
135 | P (eq_a tag hd). |
---|
136 | #tag #hd #P |
---|
137 | cases tag |
---|
138 | cases hd |
---|
139 | #true_hyp #false_hyp |
---|
140 | try @false_hyp |
---|
141 | try @true_hyp |
---|
142 | try % |
---|
143 | #absurd destruct(absurd) |
---|
144 | qed. |
---|
145 | |
---|
146 | lemma is_a_true_to_is_in: |
---|
147 | ∀n: nat. |
---|
148 | ∀x: addressing_mode. |
---|
149 | ∀tag: addressing_mode_tag. |
---|
150 | ∀supervector: Vector addressing_mode_tag n. |
---|
151 | mem addressing_mode_tag eq_a n supervector tag → |
---|
152 | is_a tag x = true → |
---|
153 | is_in … supervector x. |
---|
154 | #n #x #tag #supervector |
---|
155 | elim supervector |
---|
156 | [1: |
---|
157 | #absurd cases absurd |
---|
158 | |2: |
---|
159 | #n' #hd #tl #inductive_hypothesis |
---|
160 | whd in match (mem … eq_a (S n') (hd:::tl) tag); |
---|
161 | @eq_a_elim normalize nodelta |
---|
162 | [1: |
---|
163 | #tag_hd_eq #irrelevant |
---|
164 | whd in match (is_in (S n') (hd:::tl) x); |
---|
165 | <tag_hd_eq #is_a_hyp >is_a_hyp normalize nodelta |
---|
166 | @I |
---|
167 | |2: |
---|
168 | #tag_hd_neq |
---|
169 | whd in match (is_in (S n') (hd:::tl) x); |
---|
170 | change with ( |
---|
171 | mem … eq_a n' tl tag) |
---|
172 | in match (fold_right … n' ? false tl); |
---|
173 | #mem_hyp #is_a_hyp |
---|
174 | cases(is_a hd x) |
---|
175 | [1: |
---|
176 | normalize nodelta // |
---|
177 | |2: |
---|
178 | normalize nodelta |
---|
179 | @inductive_hypothesis assumption |
---|
180 | ] |
---|
181 | ] |
---|
182 | ] |
---|
183 | qed. |
---|
184 | |
---|
185 | lemma is_in_subvector_is_in_supervector: |
---|
186 | ∀m, n: nat. |
---|
187 | ∀subvector: Vector addressing_mode_tag m. |
---|
188 | ∀supervector: Vector addressing_mode_tag n. |
---|
189 | ∀element: addressing_mode. |
---|
190 | subvector_with … eq_a subvector supervector → |
---|
191 | is_in m subvector element → is_in n supervector element. |
---|
192 | #m #n #subvector #supervector #element |
---|
193 | elim subvector |
---|
194 | [1: |
---|
195 | #subvector_with_proof #is_in_proof |
---|
196 | cases is_in_proof |
---|
197 | |2: |
---|
198 | #n' #hd' #tl' #inductive_hypothesis #subvector_with_proof |
---|
199 | whd in match (is_in … (hd':::tl') element); |
---|
200 | cases (is_a_decidable hd' element) |
---|
201 | [1: |
---|
202 | #is_a_true >is_a_true |
---|
203 | #irrelevant |
---|
204 | whd in match (subvector_with … eq_a (hd':::tl') supervector) in subvector_with_proof; |
---|
205 | @(is_a_true_to_is_in … is_a_true) |
---|
206 | lapply(subvector_with_proof) |
---|
207 | cases(mem … eq_a n supervector hd') // |
---|
208 | |2: |
---|
209 | #is_a_false >is_a_false normalize nodelta |
---|
210 | #assm |
---|
211 | @inductive_hypothesis |
---|
212 | [1: |
---|
213 | generalize in match subvector_with_proof; |
---|
214 | whd in match (subvector_with … eq_a (hd':::tl') supervector); |
---|
215 | cases(mem_decidable n supervector hd') |
---|
216 | [1: |
---|
217 | #mem_true >mem_true normalize nodelta |
---|
218 | #assm assumption |
---|
219 | |2: |
---|
220 | #mem_false >mem_false #absurd |
---|
221 | cases absurd |
---|
222 | ] |
---|
223 | |2: |
---|
224 | assumption |
---|
225 | ] |
---|
226 | ] |
---|
227 | ] |
---|
228 | qed. |
---|
229 | |
---|
230 | let rec member_addressing_mode_tag |
---|
231 | (n: nat) (v: Vector addressing_mode_tag n) (a: addressing_mode_tag) |
---|
232 | on v: Prop ≝ |
---|
233 | match v with |
---|
234 | [ VEmpty ⇒ False |
---|
235 | | VCons n' hd tl ⇒ |
---|
236 | bool_to_Prop (eq_a hd a) ∨ member_addressing_mode_tag n' tl a |
---|
237 | ]. |
---|
238 | |
---|
239 | let rec subaddressing_mode_elim_type |
---|
240 | (T: Type[2]) (m: nat) (fixed_v: Vector addressing_mode_tag m) |
---|
241 | (Q: addressing_mode → T → Prop) |
---|
242 | (p_addr11: ∀w: Word11. is_in m fixed_v (ADDR11 w) → T) |
---|
243 | (p_addr16: ∀w: Word. is_in m fixed_v (ADDR16 w) → T) |
---|
244 | (p_direct: ∀w: Byte. is_in m fixed_v (DIRECT w) → T) |
---|
245 | (p_indirect: ∀w: Bit. is_in m fixed_v (INDIRECT w) → T) |
---|
246 | (p_ext_indirect: ∀w: Bit. is_in m fixed_v (EXT_INDIRECT w) → T) |
---|
247 | (p_acc_a: is_in m fixed_v ACC_A → T) |
---|
248 | (p_register: ∀w: BitVector 3. is_in m fixed_v (REGISTER w) → T) |
---|
249 | (p_acc_b: is_in m fixed_v ACC_B → T) |
---|
250 | (p_dptr: is_in m fixed_v DPTR → T) |
---|
251 | (p_data: ∀w: Byte. is_in m fixed_v (DATA w) → T) |
---|
252 | (p_data16: ∀w: Word. is_in m fixed_v (DATA16 w) → T) |
---|
253 | (p_acc_dptr: is_in m fixed_v ACC_DPTR → T) |
---|
254 | (p_acc_pc: is_in m fixed_v ACC_PC → T) |
---|
255 | (p_ext_indirect_dptr: is_in m fixed_v EXT_INDIRECT_DPTR → T) |
---|
256 | (p_indirect_dptr: is_in m fixed_v INDIRECT_DPTR → T) |
---|
257 | (p_carry: is_in m fixed_v CARRY → T) |
---|
258 | (p_bit_addr: ∀w: Byte. is_in m fixed_v (BIT_ADDR w) → T) |
---|
259 | (p_n_bit_addr: ∀w: Byte. is_in m fixed_v (N_BIT_ADDR w) → T) |
---|
260 | (p_relative: ∀w: Byte. is_in m fixed_v (RELATIVE w) → T) |
---|
261 | (n: nat) (v: Vector addressing_mode_tag n) (proof: subvector_with … eq_a v fixed_v) |
---|
262 | on v: Prop ≝ |
---|
263 | match v return λo: nat. λv': Vector addressing_mode_tag o. o = n → v ≃ v' → ? with |
---|
264 | [ VEmpty ⇒ λm_refl. λv_refl. |
---|
265 | ∀addr: addressing_mode. ∀p: is_in m fixed_v addr. |
---|
266 | Q addr ( |
---|
267 | match addr return λx: addressing_mode. is_in … fixed_v x → T with |
---|
268 | [ ADDR11 x ⇒ p_addr11 x |
---|
269 | | ADDR16 x ⇒ p_addr16 x |
---|
270 | | DIRECT x ⇒ p_direct x |
---|
271 | | INDIRECT x ⇒ p_indirect x |
---|
272 | | EXT_INDIRECT x ⇒ p_ext_indirect x |
---|
273 | | ACC_A ⇒ p_acc_a |
---|
274 | | REGISTER x ⇒ p_register x |
---|
275 | | ACC_B ⇒ p_acc_b |
---|
276 | | DPTR ⇒ p_dptr |
---|
277 | | DATA x ⇒ p_data x |
---|
278 | | DATA16 x ⇒ p_data16 x |
---|
279 | | ACC_DPTR ⇒ p_acc_dptr |
---|
280 | | ACC_PC ⇒ p_acc_pc |
---|
281 | | EXT_INDIRECT_DPTR ⇒ p_ext_indirect_dptr |
---|
282 | | INDIRECT_DPTR ⇒ p_indirect_dptr |
---|
283 | | CARRY ⇒ p_carry |
---|
284 | | BIT_ADDR x ⇒ p_bit_addr x |
---|
285 | | N_BIT_ADDR x ⇒ p_n_bit_addr x |
---|
286 | | RELATIVE x ⇒ p_relative x |
---|
287 | ] p) |
---|
288 | | VCons n' hd tl ⇒ λm_refl. λv_refl. |
---|
289 | let tail_call ≝ subaddressing_mode_elim_type T m fixed_v Q p_addr11 |
---|
290 | p_addr16 p_direct p_indirect p_ext_indirect p_acc_a |
---|
291 | p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr |
---|
292 | p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry |
---|
293 | p_bit_addr p_n_bit_addr p_relative n' tl ? |
---|
294 | in |
---|
295 | match hd return λa: addressing_mode_tag. a = hd → ? with |
---|
296 | [ addr11 ⇒ λhd_refl. (∀w. Q (ADDR11 w) (p_addr11 w ?)) → tail_call |
---|
297 | | addr16 ⇒ λhd_refl. (∀w. Q (ADDR16 w) (p_addr16 w ?)) → tail_call |
---|
298 | | direct ⇒ λhd_refl. (∀w. Q (DIRECT w) (p_direct w ?)) → tail_call |
---|
299 | | indirect ⇒ λhd_refl. (∀w. Q (INDIRECT w) (p_indirect w ?)) → tail_call |
---|
300 | | ext_indirect ⇒ λhd_refl. (∀w. Q (EXT_INDIRECT w) (p_ext_indirect w ?)) → tail_call |
---|
301 | | acc_a ⇒ λhd_refl. (Q ACC_A (p_acc_a ?)) → tail_call |
---|
302 | | registr ⇒ λhd_refl. (∀w. Q (REGISTER w) (p_register w ?)) → tail_call |
---|
303 | | acc_b ⇒ λhd_refl. (Q ACC_A (p_acc_b ?)) → tail_call |
---|
304 | | dptr ⇒ λhd_refl. (Q DPTR (p_dptr ?)) → tail_call |
---|
305 | | data ⇒ λhd_refl. (∀w. Q (DATA w) (p_data w ?)) → tail_call |
---|
306 | | data16 ⇒ λhd_refl. (∀w. Q (DATA16 w) (p_data16 w ?)) → tail_call |
---|
307 | | acc_dptr ⇒ λhd_refl. (Q ACC_DPTR (p_acc_dptr ?)) → tail_call |
---|
308 | | acc_pc ⇒ λhd_refl. (Q ACC_PC (p_acc_pc ?)) → tail_call |
---|
309 | | ext_indirect_dptr ⇒ λhd_refl. (Q EXT_INDIRECT_DPTR (p_ext_indirect_dptr ?)) → tail_call |
---|
310 | | indirect_dptr ⇒ λhd_refl. (Q INDIRECT_DPTR (p_indirect_dptr ?)) → tail_call |
---|
311 | | carry ⇒ λhd_refl. (Q CARRY (p_carry ?)) → tail_call |
---|
312 | | bit_addr ⇒ λhd_refl. (∀w. Q (BIT_ADDR w) (p_bit_addr w ?)) → tail_call |
---|
313 | | n_bit_addr ⇒ λhd_refl. (∀w. Q (N_BIT_ADDR w) (p_n_bit_addr w ?)) → tail_call |
---|
314 | | relative ⇒ λhd_refl. (∀w. Q (RELATIVE w) (p_relative w ?)) → tail_call |
---|
315 | ] (refl … hd) |
---|
316 | ] (refl … n) (refl_jmeq … v). |
---|
317 | [20: |
---|
318 | generalize in match proof; destruct |
---|
319 | whd in match (subvector_with … eq_a (hd:::tl) fixed_v); |
---|
320 | cases (mem … eq_a m fixed_v hd) normalize nodelta |
---|
321 | [1: |
---|
322 | whd in match (subvector_with … eq_a tl fixed_v); |
---|
323 | #assm assumption |
---|
324 | |2: |
---|
325 | normalize in ⊢ (% → ?); |
---|
326 | #absurd cases absurd |
---|
327 | ] |
---|
328 | ] |
---|
329 | @(is_in_subvector_is_in_supervector … proof) |
---|
330 | destruct @I |
---|
331 | qed. |
---|
332 | |
---|
333 | (* XXX: todo *) |
---|
334 | lemma subaddressing_mode_elim': |
---|
335 | ∀T: Type[2]. |
---|
336 | ∀n: nat. |
---|
337 | ∀o: nat. |
---|
338 | ∀v1: Vector addressing_mode_tag n. |
---|
339 | ∀v2: Vector addressing_mode_tag o. |
---|
340 | ∀Q: addressing_mode → T → Prop. |
---|
341 | ∀fixed_v: Vector addressing_mode_tag (n + o). |
---|
342 | ∀P1,P2,P3,P4,P5,P6,P7,P8,P9,P10,P11,P12,P13,P14,P15,P16,P17,P18,P19. |
---|
343 | ∀fixed_v_proof: fixed_v = v1 @@ v2. |
---|
344 | ∀subaddressing_mode_proof. |
---|
345 | subaddressing_mode_elim_type T (n + o) fixed_v Q P1 P2 P3 P4 P5 P6 P7 |
---|
346 | P8 P9 P10 P11 P12 P13 P14 P15 P16 P17 P18 P19 (n + o) (v1 @@ v2) subaddressing_mode_proof. |
---|
347 | #T #n #o #v1 #v2 |
---|
348 | elim v1 cases v2 |
---|
349 | [1: |
---|
350 | #Q #fixed_v #P1 #P2 #P3 #P4 #P5 #P6 #P7 #P8 #P9 #P10 |
---|
351 | #P11 #P12 #P13 #P14 #P15 #P16 #P17 #P18 #P19 #fixed_v_proof |
---|
352 | #subaddressing_mode_proof destruct normalize |
---|
353 | #addr #absurd cases absurd |
---|
354 | |2: |
---|
355 | #n' #hd #tl #Q #fixed_v #P1 #P2 #P3 #P4 #P5 #P6 #P7 #P8 #P9 #P10 |
---|
356 | #P11 #P12 #P13 #P14 #P15 #P16 #P17 #P18 #P19 #fixed_v_proof |
---|
357 | destruct normalize in match ([[]]@@hd:::tl); |
---|
358 | ] |
---|
359 | cases daemon |
---|
360 | qed. |
---|
361 | |
---|
362 | (* XXX: todo *) |
---|
363 | axiom subaddressing_mode_elim: |
---|
364 | ∀T: Type[2]. |
---|
365 | ∀m: nat. |
---|
366 | ∀n: nat. |
---|
367 | ∀Q: addressing_mode → T → Prop. |
---|
368 | ∀fixed_v: Vector addressing_mode_tag m. |
---|
369 | ∀P1,P2,P3,P4,P5,P6,P7,P8,P9,P10,P11,P12,P13,P14,P15,P16,P17,P18,P19. |
---|
370 | ∀v: Vector addressing_mode_tag n. |
---|
371 | ∀proof. |
---|
372 | subaddressing_mode_elim_type T m fixed_v Q P1 P2 P3 P4 P5 P6 P7 |
---|
373 | P8 P9 P10 P11 P12 P13 P14 P15 P16 P17 P18 P19 n v proof. |
---|
374 | |
---|
375 | definition current_instruction_is_labelled ≝ |
---|
376 | λcode_memory. |
---|
377 | λcost_labels: BitVectorTrie costlabel 16. |
---|
378 | λs: Status code_memory. |
---|
379 | let pc ≝ program_counter … code_memory s in |
---|
380 | match lookup_opt … pc cost_labels with |
---|
381 | [ None ⇒ False |
---|
382 | | _ ⇒ True |
---|
383 | ]. |
---|
384 | |
---|
385 | definition next_instruction_properly_relates_program_counters ≝ |
---|
386 | λcode_memory. |
---|
387 | λbefore: Status code_memory. |
---|
388 | λafter : Status code_memory. |
---|
389 | let program_counter_before ≝ program_counter ? code_memory before in |
---|
390 | let 〈instruction, program_counter_after, ticks〉 ≝ fetch code_memory program_counter_before in |
---|
391 | program_counter ? code_memory after = program_counter_after. |
---|
392 | (* XXX: why defined like this? |
---|
393 | let size ≝ current_instruction_cost code_memory before in |
---|
394 | let pc_before ≝ program_counter … code_memory before in |
---|
395 | let pc_after ≝ program_counter … code_memory after in |
---|
396 | let sum ≝ \snd (half_add … pc_before (bitvector_of_nat … size)) in |
---|
397 | sum = pc_after. |
---|
398 | *) |
---|
399 | |
---|
400 | definition ASM_abstract_status: ∀code_memory. BitVectorTrie costlabel 16 → abstract_status ≝ |
---|
401 | λcode_memory. |
---|
402 | λcost_labels. |
---|
403 | mk_abstract_status |
---|
404 | (Status code_memory) |
---|
405 | (λs,s'. (execute_1 … s) = s') |
---|
406 | (λs,class. ASM_classify … s = class) |
---|
407 | (current_instruction_is_labelled … cost_labels) |
---|
408 | (next_instruction_properly_relates_program_counters code_memory). |
---|
409 | |
---|
410 | let rec trace_any_label_length |
---|
411 | (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16) |
---|
412 | (trace_ends_flag: trace_ends_with_ret) (start_status: Status code_memory) |
---|
413 | (final_status: Status code_memory) |
---|
414 | (the_trace: trace_any_label (ASM_abstract_status code_memory cost_labels) trace_ends_flag start_status final_status) |
---|
415 | on the_trace: nat ≝ |
---|
416 | match the_trace with |
---|
417 | [ tal_base_not_return the_status _ _ _ _ ⇒ 0 |
---|
418 | | tal_base_call pre_fun_call start_fun_call final _ _ _ _ call_trace ⇒ 0 |
---|
419 | | tal_base_return the_status _ _ _ ⇒ 0 |
---|
420 | | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final _ _ _ call_trace _ final_trace ⇒ |
---|
421 | let tail_length ≝ trace_any_label_length … final_trace in |
---|
422 | let pc_difference ≝ nat_of_bitvector … (program_counter … after_fun_call) - nat_of_bitvector … (program_counter … pre_fun_call) in |
---|
423 | pc_difference + tail_length |
---|
424 | | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒ |
---|
425 | let tail_length ≝ trace_any_label_length … tail_trace in |
---|
426 | let pc_difference ≝ nat_of_bitvector … (program_counter … status_init) - nat_of_bitvector … (program_counter … status_pre) in |
---|
427 | pc_difference + tail_length |
---|
428 | ]. |
---|
429 | |
---|
430 | let rec compute_paid_trace_any_label |
---|
431 | (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16) |
---|
432 | (trace_ends_flag: trace_ends_with_ret) (start_status: Status code_memory) |
---|
433 | (final_status: Status code_memory) |
---|
434 | (the_trace: trace_any_label (ASM_abstract_status code_memory cost_labels) trace_ends_flag start_status final_status) |
---|
435 | on the_trace: nat ≝ |
---|
436 | match the_trace with |
---|
437 | [ tal_base_not_return the_status _ _ _ _ ⇒ current_instruction_cost … the_status |
---|
438 | | tal_base_return the_status _ _ _ ⇒ current_instruction_cost … the_status |
---|
439 | | tal_base_call pre_fun_call start_fun_call final _ _ _ _ call_trace ⇒ current_instruction_cost … pre_fun_call |
---|
440 | | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final |
---|
441 | _ _ _ call_trace _ final_trace ⇒ |
---|
442 | let current_instruction_cost ≝ current_instruction_cost … pre_fun_call in |
---|
443 | let final_trace_cost ≝ compute_paid_trace_any_label … cost_labels end_flag … final_trace in |
---|
444 | current_instruction_cost + final_trace_cost |
---|
445 | | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒ |
---|
446 | let current_instruction_cost ≝ current_instruction_cost … status_pre in |
---|
447 | let tail_trace_cost ≝ |
---|
448 | compute_paid_trace_any_label … cost_labels end_flag |
---|
449 | status_init status_end tail_trace |
---|
450 | in |
---|
451 | current_instruction_cost + tail_trace_cost |
---|
452 | ]. |
---|
453 | |
---|
454 | definition compute_paid_trace_label_label ≝ |
---|
455 | λcode_memory: BitVectorTrie Byte 16. |
---|
456 | λcost_labels: BitVectorTrie costlabel 16. |
---|
457 | λtrace_ends_flag: trace_ends_with_ret. |
---|
458 | λstart_status: Status code_memory. |
---|
459 | λfinal_status: Status code_memory. |
---|
460 | λthe_trace: trace_label_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status. |
---|
461 | match the_trace with |
---|
462 | [ tll_base ends_flag initial final given_trace labelled_proof ⇒ |
---|
463 | compute_paid_trace_any_label … given_trace |
---|
464 | ]. |
---|
465 | |
---|
466 | include alias "arithmetics/nat.ma". |
---|
467 | include alias "basics/logic.ma". |
---|
468 | |
---|
469 | lemma plus_right_monotone: |
---|
470 | ∀m, n, o: nat. |
---|
471 | m = n → m + o = n + o. |
---|
472 | #m #n #o #refl >refl % |
---|
473 | qed. |
---|
474 | |
---|
475 | lemma plus_left_monotone: |
---|
476 | ∀m, n, o: nat. |
---|
477 | m = n → o + m = o + n. |
---|
478 | #m #n #o #refl destruct % |
---|
479 | qed. |
---|
480 | |
---|
481 | lemma minus_plus_cancel: |
---|
482 | ∀m, n : nat. |
---|
483 | ∀proof: n ≤ m. |
---|
484 | (m - n) + n = m. |
---|
485 | #m #n #proof /2 by plus_minus/ |
---|
486 | qed. |
---|
487 | |
---|
488 | (* XXX: indexing bug *) |
---|
489 | lemma fetch_twice_fetch_execute_1: |
---|
490 | ∀code_memory: BitVectorTrie Byte 16. |
---|
491 | ∀start_status: Status code_memory. |
---|
492 | ASM_classify code_memory start_status = cl_other → |
---|
493 | \snd (\fst (fetch code_memory (program_counter … start_status))) = |
---|
494 | program_counter … (execute_1 … start_status). |
---|
495 | #code_memory #start_status #classify_assm |
---|
496 | whd in match execute_1; normalize nodelta |
---|
497 | cases (execute_1' code_memory start_status) #the_status |
---|
498 | * #_ #classify_assm' @classify_assm' assumption |
---|
499 | qed-. |
---|
500 | |
---|
501 | lemma reachable_program_counter_to_0_lt_total_program_size: |
---|
502 | ∀code_memory: BitVectorTrie Byte 16. |
---|
503 | ∀program_counter: Word. |
---|
504 | ∀total_program_size: nat. |
---|
505 | reachable_program_counter code_memory total_program_size program_counter → |
---|
506 | 0 < total_program_size. |
---|
507 | #code_memory #program_counter #total_program_size |
---|
508 | whd in match reachable_program_counter; normalize nodelta * * #some_n |
---|
509 | #_ cases (nat_of_bitvector 16 program_counter) |
---|
510 | [1: |
---|
511 | #assm assumption |
---|
512 | |2: |
---|
513 | #new_pc @ltn_to_ltO |
---|
514 | ] |
---|
515 | qed. |
---|
516 | |
---|
517 | lemma trace_compute_paid_trace_cl_other: |
---|
518 | ∀code_memory' : (BitVectorTrie Byte 16). |
---|
519 | ∀program_counter' : Word. |
---|
520 | ∀total_program_size : ℕ. |
---|
521 | ∀cost_labels : (BitVectorTrie costlabel 16). |
---|
522 | ∀reachable_program_counter_witness : (reachable_program_counter code_memory' total_program_size program_counter'). |
---|
523 | ∀good_program_witness : (good_program code_memory' total_program_size). |
---|
524 | ∀program_size' : ℕ. |
---|
525 | ∀recursive_case : (total_program_size≤S program_size'+nat_of_bitvector 16 program_counter'). |
---|
526 | ∀ticks : ℕ. |
---|
527 | ∀instruction : instruction. |
---|
528 | ∀program_counter'' : Word. |
---|
529 | ∀FETCH : (〈instruction,program_counter'',ticks〉=fetch code_memory' program_counter'). |
---|
530 | ∀start_status : (Status code_memory'). |
---|
531 | ∀final_status : (Status code_memory'). |
---|
532 | ∀trace_ends_flag : trace_ends_with_ret. |
---|
533 | ∀the_trace : (trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status). |
---|
534 | ∀program_counter_refl : (program_counter' = program_counter (BitVectorTrie Byte 16) code_memory' start_status). |
---|
535 | ∀classify_assm: ASM_classify0 instruction = cl_other. |
---|
536 | ∀pi1 : ℕ. |
---|
537 | (if match lookup_opt costlabel 16 program_counter'' cost_labels with |
---|
538 | [None ⇒ true |
---|
539 | |Some _ ⇒ false |
---|
540 | ] |
---|
541 | then |
---|
542 | ∀start_status0:Status code_memory'. |
---|
543 | ∀final_status0:Status code_memory'. |
---|
544 | ∀trace_ends_flag0:trace_ends_with_ret. |
---|
545 | ∀the_trace0:trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag0 start_status0 final_status0. |
---|
546 | program_counter'' = program_counter (BitVectorTrie Byte 16) code_memory' start_status0 → |
---|
547 | (∃n:ℕ. |
---|
548 | trace_any_label_length code_memory' cost_labels |
---|
549 | trace_ends_flag0 start_status0 final_status0 the_trace0 |
---|
550 | + S n |
---|
551 | = total_program_size) ∧ |
---|
552 | pi1 |
---|
553 | =compute_paid_trace_any_label code_memory' cost_labels |
---|
554 | trace_ends_flag0 start_status0 final_status0 the_trace0 |
---|
555 | else (pi1=O) ) |
---|
556 | →(∃n:ℕ. |
---|
557 | trace_any_label_length code_memory' cost_labels trace_ends_flag |
---|
558 | start_status final_status the_trace |
---|
559 | +S n |
---|
560 | =total_program_size) |
---|
561 | ∧ticks+pi1 |
---|
562 | =compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag |
---|
563 | start_status final_status the_trace. |
---|
564 | #code_memory' #program_counter' #total_program_size #cost_labels |
---|
565 | #reachable_program_counter_witness #good_program_witness |
---|
566 | #program_size' #recursive_case #ticks #instruction #program_counter'' #FETCH |
---|
567 | #start_status #final_status |
---|
568 | #trace_ends_flag #the_trace #program_counter_refl #classify_assm #recursive_block_cost |
---|
569 | #recursive_assm |
---|
570 | @(trace_any_label_inv_ind … the_trace) |
---|
571 | [5: |
---|
572 | #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label |
---|
573 | #classifier_assm #costed_assm #trace_ends_refl #start_status_refl #final_status_refl |
---|
574 | #the_trace_refl |
---|
575 | destruct |
---|
576 | whd in match (trace_any_label_length … (tal_step_default …)); |
---|
577 | whd in match (compute_paid_trace_any_label … (tal_step_default …)); |
---|
578 | whd in costed_assm:(?%); |
---|
579 | generalize in match costed_assm; |
---|
580 | generalize in match (refl … (lookup_opt … (program_counter … (execute_1 … status_pre)) cost_labels)); |
---|
581 | generalize in match (lookup_opt … (program_counter … (execute_1 … status_pre)) cost_labels) |
---|
582 | in ⊢ (??%? → ?(match % with [ _ ⇒ ? | _ ⇒ ? ]) → ?); |
---|
583 | #lookup_assm cases lookup_assm |
---|
584 | [1: |
---|
585 | #None_lookup_opt_assm normalize nodelta #ignore |
---|
586 | generalize in match recursive_assm; |
---|
587 | cut(program_counter'' = (program_counter (BitVectorTrie Byte 16) code_memory' (execute_1 code_memory' status_pre))) |
---|
588 | [1: |
---|
589 | <fetch_twice_fetch_execute_1 |
---|
590 | [1: |
---|
591 | <FETCH % |
---|
592 | |2: |
---|
593 | >classifier_assm % |
---|
594 | ] |
---|
595 | |2: |
---|
596 | #program_counter_assm >program_counter_assm <None_lookup_opt_assm |
---|
597 | normalize nodelta #new_recursive_assm |
---|
598 | cases(new_recursive_assm (execute_1 code_memory' status_pre) status_end |
---|
599 | end_flag trace_any_label ?) try % |
---|
600 | #exists_assm #recursive_block_cost_assm % |
---|
601 | [1: |
---|
602 | cases exists_assm #exists_n #total_program_size_refl |
---|
603 | <total_program_size_refl |
---|
604 | %{(exists_n - (nat_of_bitvector 16 |
---|
605 | (program_counter (BitVectorTrie Byte 16) code_memory' |
---|
606 | (execute_1 code_memory' status_pre)) |
---|
607 | - nat_of_bitvector 16 |
---|
608 | (program_counter (BitVectorTrie Byte 16) code_memory' status_pre)))} |
---|
609 | <plus_n_Sm <plus_n_Sm @eq_f >commutative_plus |
---|
610 | cases daemon |
---|
611 | |2: |
---|
612 | >recursive_block_cost_assm |
---|
613 | whd in match (current_instruction_cost … status_pre); |
---|
614 | cut(ticks = \snd (fetch code_memory' |
---|
615 | (program_counter (BitVectorTrie Byte 16) code_memory' status_pre))) |
---|
616 | [1: |
---|
617 | <FETCH % |
---|
618 | |2: |
---|
619 | #ticks_refl_assm >ticks_refl_assm % |
---|
620 | ] |
---|
621 | ] |
---|
622 | ] |
---|
623 | |2: |
---|
624 | #costlabel #Some_lookup_opt_assm <Some_lookup_opt_assm normalize nodelta |
---|
625 | #absurd cases absurd #absurd cases(absurd I) |
---|
626 | ] |
---|
627 | |1: |
---|
628 | #status_start #status_final #execute_assm #classifier_assm #costed_assm |
---|
629 | #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl |
---|
630 | destruct |
---|
631 | whd in match (trace_any_label_length … (tal_base_not_return …)); |
---|
632 | whd in match (compute_paid_trace_any_label … (tal_base_not_return …)); |
---|
633 | whd in costed_assm; |
---|
634 | generalize in match costed_assm; |
---|
635 | generalize in match (refl … (lookup_opt … (program_counter … (execute_1 … status_start)) cost_labels)); |
---|
636 | generalize in match (lookup_opt … (program_counter … (execute_1 code_memory' status_start)) cost_labels) |
---|
637 | in ⊢ (??%? → (match % with [ _ ⇒ ? | _ ⇒ ? ]) → ?); |
---|
638 | #lookup_assm cases lookup_assm |
---|
639 | [1: |
---|
640 | #None_lookup_opt_assm normalize nodelta >None_lookup_opt_assm |
---|
641 | #absurd cases absurd |
---|
642 | |2: |
---|
643 | #costlabel #Some_lookup_opt_assm normalize nodelta #ignore |
---|
644 | generalize in match recursive_assm; |
---|
645 | cut(program_counter'' = (program_counter (BitVectorTrie Byte 16) code_memory' (execute_1 … status_start))) |
---|
646 | [1: |
---|
647 | <fetch_twice_fetch_execute_1 |
---|
648 | [1: |
---|
649 | <FETCH % |
---|
650 | |2: |
---|
651 | cases classifier_assm |
---|
652 | [1: |
---|
653 | whd in ⊢ (% → ?); |
---|
654 | whd in ⊢ (??%? → ?); |
---|
655 | whd in match (current_instruction code_memory' status_start); |
---|
656 | <FETCH generalize in match classify_assm; |
---|
657 | cases instruction |
---|
658 | [8: |
---|
659 | #preinstruction normalize nodelta |
---|
660 | whd in match ASM_classify0; normalize nodelta |
---|
661 | #contradiction >contradiction #absurd destruct(absurd) |
---|
662 | ] |
---|
663 | try(#addr1 #addr2 normalize nodelta #ignore #absurd destruct(absurd)) |
---|
664 | try(#addr normalize nodelta #ignore #absurd destruct(absurd)) |
---|
665 | normalize in ignore; destruct(ignore) |
---|
666 | |2: |
---|
667 | #classifier_assm' >classifier_assm' % |
---|
668 | ] |
---|
669 | ] |
---|
670 | |2: |
---|
671 | #program_counter_assm >program_counter_assm <Some_lookup_opt_assm |
---|
672 | normalize nodelta #new_recursive_assm >new_recursive_assm % |
---|
673 | [1: |
---|
674 | %{(pred total_program_size)} whd in ⊢ (??%?); |
---|
675 | @S_pred |
---|
676 | @(reachable_program_counter_to_0_lt_total_program_size … reachable_program_counter_witness) |
---|
677 | |2: |
---|
678 | cut(ticks = \snd (fetch code_memory' |
---|
679 | (program_counter (BitVectorTrie Byte 16) code_memory' status_start))) |
---|
680 | [1: |
---|
681 | <FETCH % |
---|
682 | |2: |
---|
683 | #ticks_refl_assm >ticks_refl_assm |
---|
684 | <plus_n_O % |
---|
685 | ] |
---|
686 | ] |
---|
687 | ] |
---|
688 | ] |
---|
689 | |2: |
---|
690 | #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_assm |
---|
691 | #start_status_refl #final_status_refl #the_trace_assm destruct @⊥ |
---|
692 | |3: |
---|
693 | #status_pre_fun_call #status_start_fun_call #status_final #execute_assm |
---|
694 | #classifier_assm #after_return_assm #trace_label_return #costed_assm |
---|
695 | #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl |
---|
696 | destruct @⊥ |
---|
697 | |4: |
---|
698 | #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call |
---|
699 | #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return |
---|
700 | #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl |
---|
701 | #final_status_refl #the_trace_refl destruct @⊥ |
---|
702 | ] |
---|
703 | change with (ASM_classify0 ? = ?) in classifier_assm; |
---|
704 | whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm; |
---|
705 | whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm; |
---|
706 | <FETCH in classifier_assm; >classify_assm #absurd destruct(absurd) |
---|
707 | qed. |
---|
708 | |
---|
709 | lemma trace_compute_paid_trace_cl_jump: |
---|
710 | ∀code_memory': BitVectorTrie Byte 16. |
---|
711 | ∀program_counter': Word. |
---|
712 | ∀total_program_size: ℕ. |
---|
713 | ∀cost_labels: BitVectorTrie costlabel 16. |
---|
714 | ∀reachable_program_counter_witness: reachable_program_counter code_memory' total_program_size program_counter'. |
---|
715 | ∀good_program_witness: good_program code_memory' total_program_size. |
---|
716 | ∀first_time_around: bool. |
---|
717 | ∀program_size': ℕ. |
---|
718 | ∀recursive_case: total_program_size ≤ S program_size'+nat_of_bitvector 16 program_counter'. |
---|
719 | ∀ticks: ℕ. |
---|
720 | ∀instruction: instruction. |
---|
721 | ∀program_counter'': Word. |
---|
722 | ∀FETCH: 〈instruction,program_counter'',ticks〉 = fetch code_memory' program_counter'. |
---|
723 | ∀start_status: (Status code_memory'). |
---|
724 | ∀final_status: (Status code_memory'). |
---|
725 | ∀trace_ends_flag: trace_ends_with_ret. |
---|
726 | ∀the_trace: (trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status). |
---|
727 | ∀program_counter_refl: (program_counter' = program_counter (BitVectorTrie Byte 16) code_memory' start_status). |
---|
728 | ∀classify_assm: ASM_classify0 instruction = cl_jump. |
---|
729 | (∃n:ℕ |
---|
730 | .trace_any_label_length code_memory' cost_labels trace_ends_flag |
---|
731 | start_status final_status the_trace |
---|
732 | +S n |
---|
733 | =total_program_size) |
---|
734 | ∧ticks |
---|
735 | =compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag |
---|
736 | start_status final_status the_trace. |
---|
737 | #code_memory' #program_counter' #total_program_size #cost_labels |
---|
738 | #reachable_program_counter_witness #good_program_witness #first_time_around |
---|
739 | #program_size' #recursive_case #ticks #instruction #program_counter'' #FETCH |
---|
740 | #start_status #final_status |
---|
741 | #trace_ends_flag #the_trace #program_counter_refl #classify_assm |
---|
742 | @(trace_any_label_inv_ind … the_trace) |
---|
743 | [5: |
---|
744 | #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label |
---|
745 | #classifier_assm #costed_assm #trace_ends_refl #start_status_refl #final_status_refl |
---|
746 | #the_trace_refl destruct @⊥ |
---|
747 | |1: |
---|
748 | #status_start #status_final #execute_assm #classifier_assm #costed_assm |
---|
749 | #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl |
---|
750 | destruct |
---|
751 | whd in match (trace_any_label_length … (tal_base_not_return …)); |
---|
752 | whd in match (compute_paid_trace_any_label … (tal_base_not_return …)); % |
---|
753 | [1: |
---|
754 | %{(pred total_program_size)} whd in ⊢ (??%?); |
---|
755 | @S_pred |
---|
756 | @(reachable_program_counter_to_0_lt_total_program_size … reachable_program_counter_witness) |
---|
757 | |2: |
---|
758 | <FETCH % |
---|
759 | ] |
---|
760 | |2: |
---|
761 | #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_assm |
---|
762 | #start_status_refl #final_status_refl #the_trace_assm destruct @⊥ |
---|
763 | |3: |
---|
764 | #status_pre_fun_call #status_start_fun_call #status_final #execute_assm |
---|
765 | #classifier_assm #after_return_assm #trace_label_return #costed_assm |
---|
766 | #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl |
---|
767 | destruct @⊥ |
---|
768 | |4: |
---|
769 | #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call |
---|
770 | #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return |
---|
771 | #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl |
---|
772 | #final_status_refl #the_trace_refl destruct @⊥ |
---|
773 | ] |
---|
774 | change with (ASM_classify0 ? = ?) in classifier_assm; |
---|
775 | whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm; |
---|
776 | whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm; |
---|
777 | <FETCH in classifier_assm; >classify_assm #absurd destruct(absurd) |
---|
778 | qed. |
---|
779 | |
---|
780 | lemma trace_compute_paid_trace_cl_call: |
---|
781 | ∀code_memory' : (BitVectorTrie Byte 16). |
---|
782 | ∀program_counter' : Word. |
---|
783 | ∀total_program_size : ℕ. |
---|
784 | ∀cost_labels : (BitVectorTrie costlabel 16). |
---|
785 | ∀reachable_program_counter_witness : (reachable_program_counter code_memory' total_program_size program_counter'). |
---|
786 | ∀good_program_witness : (good_program code_memory' total_program_size). |
---|
787 | ∀program_size' : ℕ. |
---|
788 | ∀recursive_case : (total_program_size≤S program_size'+nat_of_bitvector 16 program_counter'). |
---|
789 | ∀ticks : ℕ. |
---|
790 | ∀instruction : instruction. |
---|
791 | ∀program_counter'' : Word. |
---|
792 | ∀FETCH : (〈instruction,program_counter'',ticks〉=fetch code_memory' program_counter'). |
---|
793 | ∀start_status : (Status code_memory'). |
---|
794 | ∀final_status : (Status code_memory'). |
---|
795 | ∀trace_ends_flag : trace_ends_with_ret. |
---|
796 | ∀the_trace : (trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status). |
---|
797 | ∀program_counter_refl : (program_counter' = program_counter (BitVectorTrie Byte 16) code_memory' start_status). |
---|
798 | ∀classify_assm: ASM_classify0 instruction = cl_call. |
---|
799 | (∀pi1:ℕ |
---|
800 | .if match lookup_opt costlabel 16 program_counter'' cost_labels with |
---|
801 | [None ⇒ true | Some _ ⇒ false] |
---|
802 | then (∀start_status0:Status code_memory' |
---|
803 | .∀final_status0:Status code_memory' |
---|
804 | .∀trace_ends_flag0:trace_ends_with_ret |
---|
805 | .∀the_trace0:trace_any_label |
---|
806 | (ASM_abstract_status code_memory' cost_labels) |
---|
807 | trace_ends_flag0 start_status0 final_status0 |
---|
808 | .program_counter'' |
---|
809 | =program_counter (BitVectorTrie Byte 16) code_memory' start_status0 |
---|
810 | →(∃n:ℕ |
---|
811 | .trace_any_label_length code_memory' cost_labels trace_ends_flag0 |
---|
812 | start_status0 final_status0 the_trace0 |
---|
813 | +S n |
---|
814 | =total_program_size) |
---|
815 | ∧pi1 |
---|
816 | =compute_paid_trace_any_label code_memory' cost_labels |
---|
817 | trace_ends_flag0 start_status0 final_status0 the_trace0) |
---|
818 | else (pi1=O) |
---|
819 | →(∃n:ℕ |
---|
820 | .trace_any_label_length code_memory' cost_labels trace_ends_flag |
---|
821 | start_status final_status the_trace |
---|
822 | +S n |
---|
823 | =total_program_size) |
---|
824 | ∧ticks+pi1 |
---|
825 | =compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag |
---|
826 | start_status final_status the_trace). |
---|
827 | #code_memory' #program_counter' #total_program_size #cost_labels |
---|
828 | #reachable_program_counter_witness #good_program_witness #program_size' |
---|
829 | #recursive_case #ticks #instruction #program_counter'' #FETCH |
---|
830 | #start_status #final_status #trace_ends_flag |
---|
831 | #the_trace #program_counter_refl #classify_assm #recursive_block_cost #recursive_assm |
---|
832 | @(trace_any_label_inv_ind … the_trace) |
---|
833 | [5: |
---|
834 | #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label |
---|
835 | #classifier_assm #costed_assm #trace_ends_refl #start_status_refl #final_status_refl |
---|
836 | #the_trace_refl destruct @⊥ |
---|
837 | |1: |
---|
838 | #status_start #status_final #execute_assm #classifier_assm #costed_assm |
---|
839 | #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl |
---|
840 | destruct @⊥ |
---|
841 | |2: |
---|
842 | #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_assm |
---|
843 | #start_status_refl #final_status_refl #the_trace_assm destruct @⊥ |
---|
844 | |3: |
---|
845 | #status_pre_fun_call #status_start_fun_call #status_final #execute_assm |
---|
846 | #classifier_assm #after_return_assm #trace_label_return #costed_assm |
---|
847 | #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl |
---|
848 | destruct |
---|
849 | whd in match (trace_any_label_length … (tal_base_call …)); |
---|
850 | whd in match (compute_paid_trace_any_label … (tal_base_call …)); |
---|
851 | whd in costed_assm; |
---|
852 | generalize in match costed_assm; |
---|
853 | generalize in match (refl … (lookup_opt … (program_counter … status_final) cost_labels)); |
---|
854 | generalize in match (lookup_opt … (program_counter … status_final) cost_labels) |
---|
855 | in ⊢ (??%? → (match % with [ _ ⇒ ? | _ ⇒ ? ]) → ?); |
---|
856 | #lookup_assm cases lookup_assm |
---|
857 | [1: |
---|
858 | #None_lookup_opt normalize nodelta #absurd cases absurd |
---|
859 | |2: |
---|
860 | #costlabel #Some_lookup_opt normalize nodelta #ignore |
---|
861 | generalize in match recursive_assm; |
---|
862 | cut(program_counter'' = (program_counter (BitVectorTrie Byte 16) code_memory' status_final)) |
---|
863 | [1: |
---|
864 | generalize in match after_return_assm; |
---|
865 | whd in ⊢ (% → ?); <FETCH normalize nodelta #relevant <relevant % |
---|
866 | |2: |
---|
867 | #program_counter_assm >program_counter_assm <Some_lookup_opt |
---|
868 | normalize nodelta #new_recursive_assm >new_recursive_assm % |
---|
869 | [1: |
---|
870 | %{(pred total_program_size)} whd in ⊢ (??%?); |
---|
871 | @S_pred |
---|
872 | @(reachable_program_counter_to_0_lt_total_program_size … reachable_program_counter_witness) |
---|
873 | |2: |
---|
874 | cut(ticks = \snd (fetch code_memory' (program_counter (BitVectorTrie Byte 16) code_memory' status_pre_fun_call))) |
---|
875 | [1: |
---|
876 | <FETCH % |
---|
877 | |2: |
---|
878 | #ticks_refl_assm >ticks_refl_assm |
---|
879 | <plus_n_O % |
---|
880 | ] |
---|
881 | ] |
---|
882 | ] |
---|
883 | ] |
---|
884 | |4: |
---|
885 | #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call |
---|
886 | #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return |
---|
887 | #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl |
---|
888 | #final_status_refl #the_trace_refl |
---|
889 | generalize in match execute_assm; destruct #execute_assm |
---|
890 | whd in match (trace_any_label_length … (tal_step_call …)); |
---|
891 | whd in match (compute_paid_trace_any_label … (tal_step_call …)); |
---|
892 | whd in costed_assm:(?%); |
---|
893 | generalize in match costed_assm; |
---|
894 | generalize in match (refl … (lookup_opt … (program_counter … status_after_fun_call) cost_labels)); |
---|
895 | generalize in match (lookup_opt … (program_counter … status_after_fun_call) cost_labels) |
---|
896 | in ⊢ (??%? → ?(match % with [ _ ⇒ ? | _ ⇒ ? ]) → ?); |
---|
897 | #lookup_assm cases lookup_assm |
---|
898 | [1: |
---|
899 | #None_lookup_opt_assm normalize nodelta #ignore |
---|
900 | generalize in match recursive_assm; |
---|
901 | cut(program_counter'' = program_counter … status_after_fun_call) |
---|
902 | [1: |
---|
903 | generalize in match after_return_assm; |
---|
904 | whd in ⊢ (% → ?); <FETCH normalize nodelta #relevant >relevant % |
---|
905 | |2: |
---|
906 | #program_counter_refl >program_counter_refl <None_lookup_opt_assm |
---|
907 | normalize nodelta #new_recursive_assm % |
---|
908 | cases (new_recursive_assm … trace_any_label ?) |
---|
909 | [1,3: |
---|
910 | #exists_assm #recursive_block_cost_assm |
---|
911 | [2: |
---|
912 | >recursive_block_cost_assm |
---|
913 | @plus_right_monotone |
---|
914 | whd in ⊢ (???%); <FETCH % |
---|
915 | |1: |
---|
916 | cases exists_assm #exists_n #trace_total_program_size_assm |
---|
917 | generalize in match execute_assm; destruct #execute_assm |
---|
918 | %{(exists_n - ((nat_of_bitvector … (program_counter … status_after_fun_call) |
---|
919 | - nat_of_bitvector … (program_counter … status_pre_fun_call))))} |
---|
920 | >commutative_plus in ⊢ (??(?%?)?); |
---|
921 | <plus_n_Sm <plus_n_Sm @eq_f >associative_plus in ⊢ (??%?); |
---|
922 | @plus_left_monotone @sym_eq <commutative_plus in ⊢ (???%); |
---|
923 | @plus_minus_m_m |
---|
924 | cases daemon (* XXX: !!! *) |
---|
925 | ] |
---|
926 | |2,4: |
---|
927 | % |
---|
928 | ] |
---|
929 | ] |
---|
930 | |2: |
---|
931 | #cost_label #Some_lookup_opt_assm normalize nodelta #absurd |
---|
932 | cases absurd #absurd cases (absurd I) |
---|
933 | ] |
---|
934 | ] |
---|
935 | try (change with (ASM_classify0 ? = ? ∨ ASM_classify0 ? = ?) in classifier_assm;) |
---|
936 | try (change with (ASM_classify0 ? = ?) in classifier_assm;) |
---|
937 | whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm; |
---|
938 | whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm; |
---|
939 | <FETCH in classifier_assm; >classify_assm #absurd destruct(absurd) cases absurd |
---|
940 | #absurd destruct(absurd) |
---|
941 | qed. |
---|
942 | |
---|
943 | lemma trace_compute_paid_trace_cl_return: |
---|
944 | ∀code_memory' : (BitVectorTrie Byte 16). |
---|
945 | ∀program_counter' : Word. |
---|
946 | ∀total_program_size : ℕ. |
---|
947 | ∀cost_labels : (BitVectorTrie costlabel 16). |
---|
948 | ∀reachable_program_counter_witness : (reachable_program_counter code_memory' total_program_size program_counter'). |
---|
949 | ∀good_program_witness : (good_program code_memory' total_program_size). |
---|
950 | ∀program_size' : ℕ. |
---|
951 | ∀recursive_case : (total_program_size≤S program_size'+nat_of_bitvector 16 program_counter'). |
---|
952 | ∀ticks : ℕ. |
---|
953 | ∀instruction : instruction. |
---|
954 | ∀program_counter'' : Word. |
---|
955 | ∀FETCH : (〈instruction,program_counter'',ticks〉=fetch code_memory' program_counter'). |
---|
956 | ∀start_status : (Status code_memory'). |
---|
957 | ∀final_status : (Status code_memory'). |
---|
958 | ∀trace_ends_flag : trace_ends_with_ret. |
---|
959 | ∀the_trace : (trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status). |
---|
960 | ∀program_counter_refl : (program_counter' = program_counter (BitVectorTrie Byte 16) code_memory' start_status). |
---|
961 | ∀classify_assm: ASM_classify0 instruction = cl_return. |
---|
962 | (∃n:ℕ |
---|
963 | .trace_any_label_length code_memory' cost_labels trace_ends_flag |
---|
964 | start_status final_status the_trace |
---|
965 | +S n |
---|
966 | =total_program_size) |
---|
967 | ∧ticks |
---|
968 | =compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag |
---|
969 | start_status final_status the_trace. |
---|
970 | #code_memory' #program_counter' #total_program_size #cost_labels |
---|
971 | #reachable_program_counter_witness #good_program_witness #program_size' |
---|
972 | #recursive_case #ticks #instruction #program_counter'' #FETCH |
---|
973 | #start_status #final_status #trace_ends_flag |
---|
974 | #the_trace #program_counter_refl #classify_assm |
---|
975 | @(trace_any_label_inv_ind … the_trace) |
---|
976 | [1: |
---|
977 | #start_status' #final_status' #execute_assm #classifier_assm #costed_assm |
---|
978 | #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl |
---|
979 | destruct @⊥ |
---|
980 | |2: |
---|
981 | #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_flag_refl |
---|
982 | #start_status_refl #final_status_refl #the_trace_refl destruct |
---|
983 | whd in match (trace_any_label_length … (tal_base_return …)); |
---|
984 | whd in match (compute_paid_trace_any_label … (tal_base_return …)); % |
---|
985 | [1: |
---|
986 | %{(pred total_program_size)} whd in ⊢ (??%?); |
---|
987 | @S_pred |
---|
988 | @(reachable_program_counter_to_0_lt_total_program_size … reachable_program_counter_witness) |
---|
989 | |2: |
---|
990 | <FETCH % |
---|
991 | ] |
---|
992 | |3: |
---|
993 | #status_pre_fun_call #status_start_fun_call #status_final #execute_assm |
---|
994 | #classifier_assm #after_return_assm #trace_label_return #costed_assm |
---|
995 | #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl |
---|
996 | destruct @⊥ |
---|
997 | |4: |
---|
998 | #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call |
---|
999 | #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return |
---|
1000 | #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl |
---|
1001 | #final_status_refl #the_trace_refl |
---|
1002 | destruct @⊥ |
---|
1003 | |5: |
---|
1004 | #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label |
---|
1005 | #classifier_assm #costed_assm #trace_ends_flag_refl #start_status_refl |
---|
1006 | #final_status_refl #the_trace_refl destruct @⊥ |
---|
1007 | ] |
---|
1008 | try (change with (ASM_classify0 ? = ? ∨ ASM_classify0 ? = ?) in classifier_assm;) |
---|
1009 | try (change with (ASM_classify0 ? = ?) in classifier_assm;) |
---|
1010 | whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm; |
---|
1011 | whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm; |
---|
1012 | <FETCH in classifier_assm; >classify_assm |
---|
1013 | #absurd try (destruct(absurd)) |
---|
1014 | cases absurd |
---|
1015 | #absurd destruct(absurd) |
---|
1016 | qed. |
---|
1017 | |
---|
1018 | let rec block_cost' |
---|
1019 | (code_memory': BitVectorTrie Byte 16) (program_counter': Word) |
---|
1020 | (program_size: nat) (total_program_size: nat) (cost_labels: BitVectorTrie costlabel 16) |
---|
1021 | (reachable_program_counter_witness: reachable_program_counter code_memory' total_program_size program_counter') |
---|
1022 | (good_program_witness: good_program code_memory' total_program_size) (first_time_around: bool) |
---|
1023 | on program_size: |
---|
1024 | total_program_size ≤ program_size + nat_of_bitvector … program_counter' → |
---|
1025 | Σcost_of_block: nat. |
---|
1026 | if (match lookup_opt … program_counter' cost_labels with [ None ⇒ true | _ ⇒ first_time_around ]) then |
---|
1027 | ∀start_status: Status code_memory'. |
---|
1028 | ∀final_status: Status code_memory'. |
---|
1029 | ∀trace_ends_flag. |
---|
1030 | ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status. |
---|
1031 | program_counter' = program_counter … start_status → |
---|
1032 | (∃n: nat. trace_any_label_length … the_trace + (S n) = total_program_size) ∧ |
---|
1033 | cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace |
---|
1034 | else |
---|
1035 | (cost_of_block = 0) ≝ |
---|
1036 | match program_size return λprogram_size: nat. total_program_size ≤ program_size + nat_of_bitvector … program_counter' → ? with |
---|
1037 | [ O ⇒ λbase_case. ⊥ |
---|
1038 | | S program_size' ⇒ λrecursive_case. |
---|
1039 | let 〈instruction, program_counter'', ticks〉 as FETCH ≝ fetch code_memory' program_counter' in |
---|
1040 | let to_continue ≝ |
---|
1041 | match lookup_opt … program_counter' cost_labels with |
---|
1042 | [ None ⇒ true |
---|
1043 | | Some _ ⇒ first_time_around |
---|
1044 | ] |
---|
1045 | in |
---|
1046 | ((if to_continue then |
---|
1047 | pi1 … (match instruction return λx. x = instruction → ? with |
---|
1048 | [ RealInstruction real_instruction ⇒ λreal_instruction_refl. |
---|
1049 | match real_instruction return λx. x = real_instruction → |
---|
1050 | Σcost_of_block: nat. |
---|
1051 | ∀start_status: Status code_memory'. |
---|
1052 | ∀final_status: Status code_memory'. |
---|
1053 | ∀trace_ends_flag. |
---|
1054 | ∀the_trace: trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status. |
---|
1055 | program_counter' = program_counter … start_status → |
---|
1056 | (∃n: nat. trace_any_label_length … the_trace + (S n) = total_program_size) ∧ |
---|
1057 | cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace with |
---|
1058 | [ RET ⇒ λinstr. ticks |
---|
1059 | | RETI ⇒ λinstr. ticks |
---|
1060 | | JC relative ⇒ λinstr. ticks |
---|
1061 | | JNC relative ⇒ λinstr. ticks |
---|
1062 | | JB bit_addr relative ⇒ λinstr. ticks |
---|
1063 | | JNB bit_addr relative ⇒ λinstr. ticks |
---|
1064 | | JBC bit_addr relative ⇒ λinstr. ticks |
---|
1065 | | JZ relative ⇒ λinstr. ticks |
---|
1066 | | JNZ relative ⇒ λinstr. ticks |
---|
1067 | | CJNE src_trgt relative ⇒ λinstr. ticks |
---|
1068 | | DJNZ src_trgt relative ⇒ λinstr. ticks |
---|
1069 | | _ ⇒ λinstr. |
---|
1070 | |
---|
1071 | ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ? |
---|
1072 | ] (refl …) |
---|
1073 | | ACALL addr ⇒ λinstr. |
---|
1074 | ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ? |
---|
1075 | | AJMP addr ⇒ λinstr. ticks |
---|
1076 | | LCALL addr ⇒ λinstr. |
---|
1077 | ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ? |
---|
1078 | | LJMP addr ⇒ λinstr. ticks |
---|
1079 | | SJMP addr ⇒ λinstr. ticks |
---|
1080 | | JMP addr ⇒ λinstr. (* XXX: actually a call due to use with fptrs *) |
---|
1081 | ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ? |
---|
1082 | | MOVC src trgt ⇒ λinstr. |
---|
1083 | ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ? |
---|
1084 | ] (refl …)) |
---|
1085 | else |
---|
1086 | 0) |
---|
1087 | : Σcost_of_block: nat. |
---|
1088 | match (match lookup_opt … program_counter' cost_labels with [ None ⇒ true | _ ⇒ first_time_around ]) with |
---|
1089 | [ true ⇒ |
---|
1090 | ∀start_status: Status code_memory'. |
---|
1091 | ∀final_status: Status code_memory'. |
---|
1092 | ∀trace_ends_flag. |
---|
1093 | ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status. |
---|
1094 | program_counter' = program_counter … start_status → |
---|
1095 | (∃n: nat. trace_any_label_length … the_trace + (S n) = total_program_size) ∧ |
---|
1096 | cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace |
---|
1097 | | false ⇒ |
---|
1098 | (cost_of_block = 0) |
---|
1099 | ]) |
---|
1100 | ]. |
---|
1101 | [1: |
---|
1102 | cases reachable_program_counter_witness #_ #hyp |
---|
1103 | @(absurd (total_program_size < total_program_size) … (not_le_Sn_n …)) |
---|
1104 | @(le_to_lt_to_lt … base_case hyp) |
---|
1105 | |2: |
---|
1106 | change with (if to_continue then ? else (? = 0)) |
---|
1107 | >p in ⊢ (match % return ? with [ _ ⇒ ? | _ ⇒ ? ]); normalize nodelta |
---|
1108 | @pi2 |
---|
1109 | |3: |
---|
1110 | change with (if to_continue then ? else (0 = 0)) |
---|
1111 | >p normalize nodelta % |
---|
1112 | |7,8: |
---|
1113 | #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl |
---|
1114 | @(trace_compute_paid_trace_cl_return … reachable_program_counter_witness good_program_witness … recursive_case … FETCH … the_trace program_counter_refl) |
---|
1115 | destruct % |
---|
1116 | |96,102,105: |
---|
1117 | #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl |
---|
1118 | cases(block_cost' ?????????) -block_cost' |
---|
1119 | @(trace_compute_paid_trace_cl_call … reachable_program_counter_witness good_program_witness … recursive_case … FETCH … program_counter_refl) |
---|
1120 | destruct % |
---|
1121 | |4,9,12,15,18,21,24,27,30,33,36,39,42,45,48,51,54,57,69,72,75,78,81,84,87, |
---|
1122 | 90,93: |
---|
1123 | #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl |
---|
1124 | cases(block_cost' ?????????) -block_cost' |
---|
1125 | @(trace_compute_paid_trace_cl_other … reachable_program_counter_witness good_program_witness … recursive_case … FETCH … the_trace program_counter_refl) |
---|
1126 | destruct % |
---|
1127 | |60,61,62,63,64,65,66,67,68,69,99,101,100,102: |
---|
1128 | #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl |
---|
1129 | @(trace_compute_paid_trace_cl_jump … reachable_program_counter_witness good_program_witness … recursive_case … FETCH … the_trace program_counter_refl) |
---|
1130 | destruct % |
---|
1131 | |103: |
---|
1132 | cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp |
---|
1133 | lapply(good_program_witness program_counter' reachable_program_counter_witness) |
---|
1134 | <FETCH normalize nodelta <instr normalize nodelta |
---|
1135 | @(subaddressing_mode_elim … [[addr16]] … [[addr16]]) [1: // ] #new_addr |
---|
1136 | * * * * #n' |
---|
1137 | #_ #_ #program_counter_lt' #program_counter_lt_tps' |
---|
1138 | % |
---|
1139 | [1: |
---|
1140 | %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta |
---|
1141 | <FETCH normalize nodelta whd in match ltb; normalize nodelta |
---|
1142 | >(le_to_leb_true … program_counter_lt') % |
---|
1143 | |2: |
---|
1144 | assumption |
---|
1145 | ] |
---|
1146 | |104: |
---|
1147 | cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp |
---|
1148 | lapply(good_program_witness program_counter' reachable_program_counter_witness) |
---|
1149 | <FETCH normalize nodelta <instr normalize nodelta |
---|
1150 | @(subaddressing_mode_elim … [[addr16]] … [[addr16]]) [1: // ] #new_addr |
---|
1151 | * * * * #n' |
---|
1152 | #_ #_ #program_counter_lt' #program_counter_lt_tps' |
---|
1153 | @(transitive_le |
---|
1154 | total_program_size |
---|
1155 | ((S program_size') + nat_of_bitvector … program_counter') |
---|
1156 | (program_size' + nat_of_bitvector … program_counter'') recursive_case) |
---|
1157 | normalize in match (S program_size' + nat_of_bitvector … program_counter'); |
---|
1158 | >plus_n_Sm |
---|
1159 | @monotonic_le_plus_r |
---|
1160 | change with ( |
---|
1161 | nat_of_bitvector … program_counter' < |
---|
1162 | nat_of_bitvector … program_counter'') |
---|
1163 | assumption |
---|
1164 | |106: |
---|
1165 | cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp |
---|
1166 | lapply(good_program_witness program_counter' reachable_program_counter_witness) |
---|
1167 | <FETCH normalize nodelta <instr normalize nodelta |
---|
1168 | @(subaddressing_mode_elim … [[addr11]] … [[addr11]]) [1: // ] #new_addr |
---|
1169 | cases (split … 8 8 program_counter'') #pc_bu #pc_bl normalize nodelta |
---|
1170 | cases (split … 3 8 new_addr) #thr #eig normalize nodelta |
---|
1171 | cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta * * * * #n' |
---|
1172 | #_ #_ #program_counter_lt' #program_counter_lt_tps' |
---|
1173 | % |
---|
1174 | [1: |
---|
1175 | %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta |
---|
1176 | <FETCH normalize nodelta whd in match ltb; normalize nodelta |
---|
1177 | >(le_to_leb_true … program_counter_lt') % |
---|
1178 | |2: |
---|
1179 | assumption |
---|
1180 | ] |
---|
1181 | |107: |
---|
1182 | cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp |
---|
1183 | lapply(good_program_witness program_counter' reachable_program_counter_witness) |
---|
1184 | <FETCH normalize nodelta <instr normalize nodelta |
---|
1185 | @(subaddressing_mode_elim … [[addr11]] … [[addr11]]) [1: // ] #new_addr |
---|
1186 | cases (split … 8 8 program_counter'') #pc_bu #pc_bl normalize nodelta |
---|
1187 | cases (split … 3 8 new_addr) #thr #eig normalize nodelta |
---|
1188 | cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta * * * * #n' |
---|
1189 | #_ #_ #program_counter_lt' #program_counter_lt_tps' |
---|
1190 | @(transitive_le |
---|
1191 | total_program_size |
---|
1192 | ((S program_size') + nat_of_bitvector … program_counter') |
---|
1193 | (program_size' + nat_of_bitvector … program_counter'') recursive_case) |
---|
1194 | normalize in match (S program_size' + nat_of_bitvector … program_counter'); |
---|
1195 | >plus_n_Sm |
---|
1196 | @monotonic_le_plus_r |
---|
1197 | change with ( |
---|
1198 | nat_of_bitvector … program_counter' < |
---|
1199 | nat_of_bitvector … program_counter'') |
---|
1200 | assumption |
---|
1201 | |94,97: |
---|
1202 | cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp |
---|
1203 | lapply(good_program_witness program_counter' reachable_program_counter_witness) |
---|
1204 | <FETCH normalize nodelta <instr normalize nodelta * |
---|
1205 | #program_counter_lt' #program_counter_lt_tps' % |
---|
1206 | [1,3: |
---|
1207 | %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta |
---|
1208 | <FETCH normalize nodelta whd in match ltb; normalize nodelta |
---|
1209 | >(le_to_leb_true … program_counter_lt') % |
---|
1210 | |2,4: |
---|
1211 | assumption |
---|
1212 | ] |
---|
1213 | |5,10,12,13,16,18,19,22,25,28,31,34,37,40,43,46,49,52,55,58,70,73, |
---|
1214 | 76,79,82,85,88,91: |
---|
1215 | cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp |
---|
1216 | lapply(good_program_witness program_counter' reachable_program_counter_witness) |
---|
1217 | <FETCH normalize nodelta <real_instruction_refl <instr normalize nodelta * |
---|
1218 | #program_counter_lt' #program_counter_lt_tps' % |
---|
1219 | try assumption |
---|
1220 | %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta |
---|
1221 | <FETCH normalize nodelta whd in match ltb; normalize nodelta |
---|
1222 | >(le_to_leb_true … program_counter_lt') % |
---|
1223 | |6,11,14,17,20,23,26,29,32,35,38,41,44,47,50,53,56,59,71,74,77,80,83,86,89, |
---|
1224 | 92: |
---|
1225 | cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp |
---|
1226 | lapply(good_program_witness program_counter' reachable_program_counter_witness) |
---|
1227 | <FETCH normalize nodelta |
---|
1228 | <real_instruction_refl <instr normalize nodelta * |
---|
1229 | #pc_pc_lt_hyp' #pc_tps_lt_hyp' |
---|
1230 | @(transitive_le |
---|
1231 | total_program_size |
---|
1232 | ((S program_size') + nat_of_bitvector … program_counter') |
---|
1233 | (program_size' + nat_of_bitvector … program_counter'') recursive_case) |
---|
1234 | normalize in match (S program_size' + nat_of_bitvector … program_counter'); |
---|
1235 | >plus_n_Sm |
---|
1236 | @monotonic_le_plus_r |
---|
1237 | change with ( |
---|
1238 | nat_of_bitvector … program_counter' < |
---|
1239 | nat_of_bitvector … program_counter'') |
---|
1240 | assumption |
---|
1241 | |95,98: |
---|
1242 | cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp |
---|
1243 | lapply(good_program_witness program_counter' reachable_program_counter_witness) |
---|
1244 | <FETCH normalize nodelta <instr normalize nodelta |
---|
1245 | try(<real_instruction_refl <instr normalize nodelta) * |
---|
1246 | #pc_pc_lt_hyp' #pc_tps_lt_hyp' |
---|
1247 | @(transitive_le |
---|
1248 | total_program_size |
---|
1249 | ((S program_size') + nat_of_bitvector … program_counter') |
---|
1250 | (program_size' + nat_of_bitvector … program_counter'') recursive_case) |
---|
1251 | normalize in match (S program_size' + nat_of_bitvector … program_counter'); |
---|
1252 | >plus_n_Sm |
---|
1253 | @monotonic_le_plus_r |
---|
1254 | change with ( |
---|
1255 | nat_of_bitvector … program_counter' < |
---|
1256 | nat_of_bitvector … program_counter'') |
---|
1257 | assumption |
---|
1258 | ] |
---|
1259 | qed. |
---|
1260 | |
---|
1261 | definition block_cost: |
---|
1262 | ∀code_memory': BitVectorTrie Byte 16. |
---|
1263 | ∀program_counter': Word. |
---|
1264 | ∀total_program_size: nat. |
---|
1265 | ∀cost_labels: BitVectorTrie costlabel 16. |
---|
1266 | ∀reachable_program_counter_witness: reachable_program_counter code_memory' total_program_size program_counter'. |
---|
1267 | ∀good_program_witness: good_program code_memory' total_program_size. |
---|
1268 | Σcost_of_block: nat. |
---|
1269 | ∀start_status: Status code_memory'. |
---|
1270 | ∀final_status: Status code_memory'. |
---|
1271 | ∀trace_ends_flag. |
---|
1272 | ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status. |
---|
1273 | program_counter' = program_counter … start_status → |
---|
1274 | (∃n: nat. trace_any_label_length … the_trace + (S n) = total_program_size) ∧ |
---|
1275 | cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace ≝ |
---|
1276 | λcode_memory: BitVectorTrie Byte 16. |
---|
1277 | λprogram_counter: Word. |
---|
1278 | λtotal_program_size: nat. |
---|
1279 | λcost_labels: BitVectorTrie costlabel 16. |
---|
1280 | λreachable_program_counter_witness: reachable_program_counter code_memory total_program_size program_counter. |
---|
1281 | λgood_program_witness: good_program code_memory total_program_size. ?. |
---|
1282 | cases(block_cost' code_memory program_counter total_program_size total_program_size cost_labels |
---|
1283 | reachable_program_counter_witness good_program_witness true ?) |
---|
1284 | [1: |
---|
1285 | #cost_of_block #block_cost_hyp |
---|
1286 | %{cost_of_block} |
---|
1287 | cases(lookup_opt … cost_labels) in block_cost_hyp; |
---|
1288 | [2: #cost_label] normalize nodelta |
---|
1289 | #hyp assumption |
---|
1290 | |2: |
---|
1291 | @le_plus_n_r |
---|
1292 | ] |
---|
1293 | qed. |
---|
1294 | |
---|
1295 | lemma fetch_program_counter_n_Sn: |
---|
1296 | ∀instruction: instruction. |
---|
1297 | ∀program_counter, program_counter': Word. |
---|
1298 | ∀ticks, n: nat. |
---|
1299 | ∀code_memory: BitVectorTrie Byte 16. |
---|
1300 | Some … program_counter = fetch_program_counter_n n code_memory (zero 16) → |
---|
1301 | 〈instruction,program_counter',ticks〉 = fetch code_memory program_counter → |
---|
1302 | nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' → |
---|
1303 | Some … program_counter' = fetch_program_counter_n (S n) code_memory (zero …). |
---|
1304 | #instruction #program_counter #program_counter' #ticks #n #code_memory |
---|
1305 | #fetch_program_counter_n_hyp #fetch_hyp #lt_hyp |
---|
1306 | whd in match (fetch_program_counter_n (S n) code_memory (zero …)); |
---|
1307 | <fetch_program_counter_n_hyp normalize nodelta |
---|
1308 | <fetch_hyp normalize nodelta |
---|
1309 | change with ( |
---|
1310 | leb (S (nat_of_bitvector … program_counter)) (nat_of_bitvector … program_counter') |
---|
1311 | ) in match (ltb (nat_of_bitvector … program_counter) (nat_of_bitvector … program_counter')); |
---|
1312 | >(le_to_leb_true … lt_hyp) % |
---|
1313 | qed. |
---|
1314 | |
---|
1315 | (* XXX: to be moved into common/Identifiers.ma *) |
---|
1316 | lemma lookup_present_add_hit: |
---|
1317 | ∀tag, A, map, k, v, k_pres. |
---|
1318 | lookup_present tag A (add … map k v) k k_pres = v. |
---|
1319 | #tag #a #map #k #v #k_pres |
---|
1320 | lapply (lookup_lookup_present … (add … map k v) … k_pres) |
---|
1321 | >lookup_add_hit #Some_assm destruct(Some_assm) |
---|
1322 | <e0 % |
---|
1323 | qed. |
---|
1324 | |
---|
1325 | lemma lookup_present_add_miss: |
---|
1326 | ∀tag, A, map, k, k', v, k_pres', k_pres''. |
---|
1327 | k' ≠ k → |
---|
1328 | lookup_present tag A (add … map k v) k' k_pres' = lookup_present tag A map k' k_pres''. |
---|
1329 | #tag #A #map #k #k' #v #k_pres' #k_pres'' #neq_assm |
---|
1330 | lapply (lookup_lookup_present … (add … map k v) ? k_pres') |
---|
1331 | >lookup_add_miss try assumption |
---|
1332 | #Some_assm |
---|
1333 | lapply (lookup_lookup_present … map k') >Some_assm #Some_assm' |
---|
1334 | lapply (Some_assm' k_pres'') #Some_assm'' destruct assumption |
---|
1335 | qed. |
---|
1336 | |
---|
1337 | (* XXX: to be moved into basics/types.ma *) |
---|
1338 | lemma not_None_to_Some: |
---|
1339 | ∀A: Type[0]. |
---|
1340 | ∀o: option A. |
---|
1341 | o ≠ None A → ∃v: A. o = Some A v. |
---|
1342 | #A #o cases o |
---|
1343 | [1: |
---|
1344 | #absurd cases absurd #absurd' cases (absurd' (refl …)) |
---|
1345 | |2: |
---|
1346 | #v' #ignore /2/ |
---|
1347 | ] |
---|
1348 | qed. |
---|
1349 | |
---|
1350 | lemma present_add_present: |
---|
1351 | ∀tag, a, map, k, k', v. |
---|
1352 | k' ≠ k → |
---|
1353 | present tag a (add tag a map k v) k' → |
---|
1354 | present tag a map k'. |
---|
1355 | #tag #a #map #k #k' #v #neq_hyp #present_hyp |
---|
1356 | whd in match present; normalize nodelta |
---|
1357 | whd in match present in present_hyp; normalize nodelta in present_hyp; |
---|
1358 | cases (not_None_to_Some a … present_hyp) #v' #Some_eq_hyp |
---|
1359 | lapply (lookup_add_cases tag ?????? Some_eq_hyp) * |
---|
1360 | [1: |
---|
1361 | * #k_eq_hyp @⊥ /2/ |
---|
1362 | |2: |
---|
1363 | #Some_eq_hyp' /2/ |
---|
1364 | ] |
---|
1365 | qed. |
---|
1366 | |
---|
1367 | lemma present_add_hit: |
---|
1368 | ∀tag, a, map, k, v. |
---|
1369 | present tag a (add tag a map k v) k. |
---|
1370 | #tag #a #map #k #v |
---|
1371 | whd >lookup_add_hit |
---|
1372 | % #absurd destruct |
---|
1373 | qed. |
---|
1374 | |
---|
1375 | lemma present_add_miss: |
---|
1376 | ∀tag, a, map, k, k', v. |
---|
1377 | k' ≠ k → present tag a map k' → present tag a (add tag a map k v) k'. |
---|
1378 | #tag #a #map #k #k' #v #neq_assm #present_assm |
---|
1379 | whd >lookup_add_miss assumption |
---|
1380 | qed. |
---|
1381 | |
---|
1382 | lemma lt_to_le_to_le: |
---|
1383 | ∀n, m, p: nat. |
---|
1384 | n < m → m ≤ p → n ≤ p. |
---|
1385 | #n #m #p #H #H1 |
---|
1386 | elim H |
---|
1387 | [1: |
---|
1388 | @(transitive_le n m p) /2/ |
---|
1389 | |2: |
---|
1390 | /2/ |
---|
1391 | ] |
---|
1392 | qed. |
---|
1393 | |
---|
1394 | lemma eqb_decidable: |
---|
1395 | ∀l, r: nat. |
---|
1396 | (eqb l r = true) ∨ (eqb l r = false). |
---|
1397 | #l #r // |
---|
1398 | qed. |
---|
1399 | |
---|
1400 | lemma r_Sr_and_l_r_to_Sl_r: |
---|
1401 | ∀r, l: nat. |
---|
1402 | (∃r': nat. r = S r' ∧ l = r') → S l = r. |
---|
1403 | #r #l #exists_hyp |
---|
1404 | cases exists_hyp #r' |
---|
1405 | #and_hyp cases and_hyp |
---|
1406 | #left_hyp #right_hyp |
---|
1407 | destruct % |
---|
1408 | qed. |
---|
1409 | |
---|
1410 | lemma eqb_Sn_to_exists_n': |
---|
1411 | ∀m, n: nat. |
---|
1412 | eqb (S m) n = true → ∃n': nat. n = S n'. |
---|
1413 | #m #n |
---|
1414 | cases n |
---|
1415 | [1: |
---|
1416 | normalize #absurd |
---|
1417 | destruct(absurd) |
---|
1418 | |2: |
---|
1419 | #n' #_ %{n'} % |
---|
1420 | ] |
---|
1421 | qed. |
---|
1422 | |
---|
1423 | lemma eqb_true_to_eqb_S_S_true: |
---|
1424 | ∀m, n: nat. |
---|
1425 | eqb m n = true → eqb (S m) (S n) = true. |
---|
1426 | #m #n normalize #assm assumption |
---|
1427 | qed. |
---|
1428 | |
---|
1429 | lemma eqb_S_S_true_to_eqb_true: |
---|
1430 | ∀m, n: nat. |
---|
1431 | eqb (S m) (S n) = true → eqb m n = true. |
---|
1432 | #m #n normalize #assm assumption |
---|
1433 | qed. |
---|
1434 | |
---|
1435 | lemma eqb_true_to_refl: |
---|
1436 | ∀l, r: nat. |
---|
1437 | eqb l r = true → l = r. |
---|
1438 | #l |
---|
1439 | elim l |
---|
1440 | [1: |
---|
1441 | #r cases r |
---|
1442 | [1: |
---|
1443 | #_ % |
---|
1444 | |2: |
---|
1445 | #l' normalize |
---|
1446 | #absurd destruct(absurd) |
---|
1447 | ] |
---|
1448 | |2: |
---|
1449 | #l' #inductive_hypothesis #r |
---|
1450 | #eqb_refl @r_Sr_and_l_r_to_Sl_r |
---|
1451 | %{(pred r)} @conj |
---|
1452 | [1: |
---|
1453 | cases (eqb_Sn_to_exists_n' … eqb_refl) |
---|
1454 | #r' #S_assm >S_assm % |
---|
1455 | |2: |
---|
1456 | cases (eqb_Sn_to_exists_n' … eqb_refl) |
---|
1457 | #r' #refl_assm destruct normalize |
---|
1458 | @inductive_hypothesis |
---|
1459 | normalize in eqb_refl; assumption |
---|
1460 | ] |
---|
1461 | ] |
---|
1462 | qed. |
---|
1463 | |
---|
1464 | lemma r_O_or_exists_r_r_Sr_and_l_neq_r_to_Sl_neq_r: |
---|
1465 | ∀r, l: nat. |
---|
1466 | r = O ∨ (∃r': nat. r = S r' ∧ l ≠ r') → S l ≠ r. |
---|
1467 | #r #l #disj_hyp |
---|
1468 | cases disj_hyp |
---|
1469 | [1: |
---|
1470 | #r_O_refl destruct @nmk |
---|
1471 | #absurd destruct(absurd) |
---|
1472 | |2: |
---|
1473 | #exists_hyp cases exists_hyp #r' |
---|
1474 | #conj_hyp cases conj_hyp #left_conj #right_conj |
---|
1475 | destruct @nmk #S_S_refl_hyp |
---|
1476 | elim right_conj #hyp @hyp // |
---|
1477 | ] |
---|
1478 | qed. |
---|
1479 | |
---|
1480 | lemma neq_l_r_to_neq_Sl_Sr: |
---|
1481 | ∀l, r: nat. |
---|
1482 | l ≠ r → S l ≠ S r. |
---|
1483 | #l #r #l_neq_r_assm |
---|
1484 | @nmk #Sl_Sr_assm cases l_neq_r_assm |
---|
1485 | #assm @assm // |
---|
1486 | qed. |
---|
1487 | |
---|
1488 | lemma eqb_false_to_not_refl: |
---|
1489 | ∀l, r: nat. |
---|
1490 | eqb l r = false → l ≠ r. |
---|
1491 | #l |
---|
1492 | elim l |
---|
1493 | [1: |
---|
1494 | #r cases r |
---|
1495 | [1: |
---|
1496 | normalize #absurd destruct(absurd) |
---|
1497 | |2: |
---|
1498 | #r' #_ @nmk |
---|
1499 | #absurd destruct(absurd) |
---|
1500 | ] |
---|
1501 | |2: |
---|
1502 | #l' #inductive_hypothesis #r |
---|
1503 | cases r |
---|
1504 | [1: |
---|
1505 | #eqb_false_assm |
---|
1506 | @r_O_or_exists_r_r_Sr_and_l_neq_r_to_Sl_neq_r |
---|
1507 | @or_introl % |
---|
1508 | |2: |
---|
1509 | #r' #eqb_false_assm |
---|
1510 | @neq_l_r_to_neq_Sl_Sr |
---|
1511 | @inductive_hypothesis |
---|
1512 | assumption |
---|
1513 | ] |
---|
1514 | ] |
---|
1515 | qed. |
---|
1516 | |
---|
1517 | lemma le_to_lt_or_eq: |
---|
1518 | ∀m, n: nat. |
---|
1519 | m ≤ n → m = n ∨ m < n. |
---|
1520 | #m #n #le_hyp |
---|
1521 | cases le_hyp |
---|
1522 | [1: |
---|
1523 | @or_introl % |
---|
1524 | |2: |
---|
1525 | #m' #le_hyp' |
---|
1526 | @or_intror |
---|
1527 | normalize |
---|
1528 | @le_S_S assumption |
---|
1529 | ] |
---|
1530 | qed. |
---|
1531 | |
---|
1532 | lemma le_neq_to_lt: |
---|
1533 | ∀m, n: nat. |
---|
1534 | m ≤ n → m ≠ n → m < n. |
---|
1535 | #m #n #le_hyp #neq_hyp |
---|
1536 | cases neq_hyp |
---|
1537 | #eq_absurd_hyp |
---|
1538 | generalize in match (le_to_lt_or_eq m n le_hyp); |
---|
1539 | #disj_assm cases disj_assm |
---|
1540 | [1: |
---|
1541 | #absurd cases (eq_absurd_hyp absurd) |
---|
1542 | |2: |
---|
1543 | #assm assumption |
---|
1544 | ] |
---|
1545 | qed. |
---|
1546 | |
---|
1547 | inverter nat_jmdiscr for nat. |
---|
1548 | |
---|
1549 | (* XXX: this is false in the general case. For instance, if n = 0 then the |
---|
1550 | base case requires us prove 1 = 0, as it is the carry bit that holds |
---|
1551 | the result of the addition. *) |
---|
1552 | axiom succ_nat_of_bitvector_half_add_1: |
---|
1553 | ∀n: nat. |
---|
1554 | ∀bv: BitVector n. |
---|
1555 | ∀power_proof: nat_of_bitvector … bv < 2^n - 1. |
---|
1556 | S (nat_of_bitvector … bv) = nat_of_bitvector … |
---|
1557 | (\snd (half_add n (bitvector_of_nat … 1) bv)). |
---|
1558 | |
---|
1559 | lemma plus_lt_to_lt: |
---|
1560 | ∀m, n, o: nat. |
---|
1561 | m + n < o → m < o. |
---|
1562 | #m #n #o |
---|
1563 | elim n |
---|
1564 | [1: |
---|
1565 | <(plus_n_O m) in ⊢ (% → ?); |
---|
1566 | #assumption assumption |
---|
1567 | |2: |
---|
1568 | #n' #inductive_hypothesis |
---|
1569 | <(plus_n_Sm m n') in ⊢ (% → ?); |
---|
1570 | #assm @inductive_hypothesis |
---|
1571 | normalize in assm; normalize |
---|
1572 | /2 by lt_S_to_lt/ |
---|
1573 | ] |
---|
1574 | qed. |
---|
1575 | |
---|
1576 | include "arithmetics/div_and_mod.ma". |
---|
1577 | |
---|
1578 | lemma n_plus_1_n_to_False: |
---|
1579 | ∀n: nat. |
---|
1580 | n + 1 = n → False. |
---|
1581 | #n elim n |
---|
1582 | [1: |
---|
1583 | normalize #absurd destruct(absurd) |
---|
1584 | |2: |
---|
1585 | #n' #inductive_hypothesis normalize |
---|
1586 | #absurd @inductive_hypothesis /2/ |
---|
1587 | ] |
---|
1588 | qed. |
---|
1589 | |
---|
1590 | lemma one_two_times_n_to_False: |
---|
1591 | ∀n: nat. |
---|
1592 | 1=2*n→False. |
---|
1593 | #n cases n |
---|
1594 | [1: |
---|
1595 | normalize #absurd destruct(absurd) |
---|
1596 | |2: |
---|
1597 | #n' normalize #absurd |
---|
1598 | lapply (injective_S … absurd) -absurd #absurd |
---|
1599 | /2/ |
---|
1600 | ] |
---|
1601 | qed. |
---|
1602 | |
---|
1603 | lemma generalized_nat_cases: |
---|
1604 | ∀n: nat. |
---|
1605 | n = 0 ∨ n = 1 ∨ ∃m: nat. n = S (S m). |
---|
1606 | #n |
---|
1607 | cases n |
---|
1608 | [1: |
---|
1609 | @or_introl @or_introl % |
---|
1610 | |2: |
---|
1611 | #n' cases n' |
---|
1612 | [1: |
---|
1613 | @or_introl @or_intror % |
---|
1614 | |2: |
---|
1615 | #n'' @or_intror %{n''} % |
---|
1616 | ] |
---|
1617 | ] |
---|
1618 | qed. |
---|
1619 | |
---|
1620 | let rec odd_p |
---|
1621 | (n: nat) |
---|
1622 | on n ≝ |
---|
1623 | match n with |
---|
1624 | [ O ⇒ False |
---|
1625 | | S n' ⇒ even_p n' |
---|
1626 | ] |
---|
1627 | and even_p |
---|
1628 | (n: nat) |
---|
1629 | on n ≝ |
---|
1630 | match n with |
---|
1631 | [ O ⇒ True |
---|
1632 | | S n' ⇒ odd_p n' |
---|
1633 | ]. |
---|
1634 | |
---|
1635 | let rec n_even_p_to_n_plus_2_even_p |
---|
1636 | (n: nat) |
---|
1637 | on n: even_p n → even_p (n + 2) ≝ |
---|
1638 | match n with |
---|
1639 | [ O ⇒ ? |
---|
1640 | | S n' ⇒ ? |
---|
1641 | ] |
---|
1642 | and n_odd_p_to_n_plus_2_odd_p |
---|
1643 | (n: nat) |
---|
1644 | on n: odd_p n → odd_p (n + 2) ≝ |
---|
1645 | match n with |
---|
1646 | [ O ⇒ ? |
---|
1647 | | S n' ⇒ ? |
---|
1648 | ]. |
---|
1649 | [1,3: |
---|
1650 | normalize #assm assumption |
---|
1651 | |2: |
---|
1652 | normalize @n_odd_p_to_n_plus_2_odd_p |
---|
1653 | |4: |
---|
1654 | normalize @n_even_p_to_n_plus_2_even_p |
---|
1655 | ] |
---|
1656 | qed. |
---|
1657 | |
---|
1658 | let rec two_times_n_even_p |
---|
1659 | (n: nat) |
---|
1660 | on n: even_p (2 * n) ≝ |
---|
1661 | match n with |
---|
1662 | [ O ⇒ ? |
---|
1663 | | S n' ⇒ ? |
---|
1664 | ] |
---|
1665 | and two_times_n_plus_one_odd_p |
---|
1666 | (n: nat) |
---|
1667 | on n: odd_p ((2 * n) + 1) ≝ |
---|
1668 | match n with |
---|
1669 | [ O ⇒ ? |
---|
1670 | | S n' ⇒ ? |
---|
1671 | ]. |
---|
1672 | [1,3: |
---|
1673 | normalize @I |
---|
1674 | |2: |
---|
1675 | normalize |
---|
1676 | >plus_n_Sm |
---|
1677 | <(associative_plus n' n' 1) |
---|
1678 | >(plus_n_O (n' + n')) |
---|
1679 | cut(n' + n' + 0 + 1 = 2 * n' + 1) |
---|
1680 | [1: |
---|
1681 | // |
---|
1682 | |2: |
---|
1683 | #refl_assm >refl_assm |
---|
1684 | @two_times_n_plus_one_odd_p |
---|
1685 | ] |
---|
1686 | |4: |
---|
1687 | normalize |
---|
1688 | >plus_n_Sm |
---|
1689 | cut(n' + (n' + 1) + 1 = (2 * n') + 2) |
---|
1690 | [1: |
---|
1691 | normalize /2/ |
---|
1692 | |2: |
---|
1693 | #refl_assm >refl_assm |
---|
1694 | @n_even_p_to_n_plus_2_even_p |
---|
1695 | @two_times_n_even_p |
---|
1696 | ] |
---|
1697 | ] |
---|
1698 | qed. |
---|
1699 | |
---|
1700 | let rec even_p_to_not_odd_p |
---|
1701 | (n: nat) |
---|
1702 | on n: even_p n → ¬ odd_p n ≝ |
---|
1703 | match n with |
---|
1704 | [ O ⇒ ? |
---|
1705 | | S n' ⇒ ? |
---|
1706 | ] |
---|
1707 | and odd_p_to_not_even_p |
---|
1708 | (n: nat) |
---|
1709 | on n: odd_p n → ¬ even_p n ≝ |
---|
1710 | match n with |
---|
1711 | [ O ⇒ ? |
---|
1712 | | S n' ⇒ ? |
---|
1713 | ]. |
---|
1714 | [1: |
---|
1715 | normalize #_ |
---|
1716 | @nmk #assm assumption |
---|
1717 | |3: |
---|
1718 | normalize #absurd |
---|
1719 | cases absurd |
---|
1720 | |2: |
---|
1721 | normalize |
---|
1722 | @odd_p_to_not_even_p |
---|
1723 | |4: |
---|
1724 | normalize |
---|
1725 | @even_p_to_not_odd_p |
---|
1726 | ] |
---|
1727 | qed. |
---|
1728 | |
---|
1729 | lemma even_p_odd_p_cases: |
---|
1730 | ∀n: nat. |
---|
1731 | even_p n ∨ odd_p n. |
---|
1732 | #n elim n |
---|
1733 | [1: |
---|
1734 | normalize @or_introl @I |
---|
1735 | |2: |
---|
1736 | #n' #inductive_hypothesis |
---|
1737 | normalize |
---|
1738 | cases inductive_hypothesis |
---|
1739 | #assm |
---|
1740 | try (@or_introl assumption) |
---|
1741 | try (@or_intror assumption) |
---|
1742 | ] |
---|
1743 | qed. |
---|
1744 | |
---|
1745 | lemma two_times_n_plus_one_refl_two_times_n_to_False: |
---|
1746 | ∀m, n: nat. |
---|
1747 | 2 * m + 1 = 2 * n → False. |
---|
1748 | #m #n |
---|
1749 | #assm |
---|
1750 | cut (even_p (2 * n) ∧ even_p ((2 * m) + 1)) |
---|
1751 | [1: |
---|
1752 | >assm |
---|
1753 | @conj |
---|
1754 | @two_times_n_even_p |
---|
1755 | |2: |
---|
1756 | * #_ #absurd |
---|
1757 | cases (even_p_to_not_odd_p … absurd) |
---|
1758 | #assm @assm |
---|
1759 | @two_times_n_plus_one_odd_p |
---|
1760 | ] |
---|
1761 | qed. |
---|
1762 | |
---|
1763 | lemma nat_of_bitvector_aux_injective: |
---|
1764 | ∀n: nat. |
---|
1765 | ∀l, r: BitVector n. |
---|
1766 | ∀acc_l, acc_r: nat. |
---|
1767 | nat_of_bitvector_aux n acc_l l = nat_of_bitvector_aux n acc_r r → |
---|
1768 | acc_l = acc_r ∧ l ≃ r. |
---|
1769 | #n #l |
---|
1770 | elim l #r |
---|
1771 | [1: |
---|
1772 | #acc_l #acc_r normalize |
---|
1773 | >(BitVector_O r) normalize /2/ |
---|
1774 | |2: |
---|
1775 | #hd #tl #inductive_hypothesis #r #acc_l #acc_r |
---|
1776 | normalize normalize in inductive_hypothesis; |
---|
1777 | cases (BitVector_Sn … r) |
---|
1778 | #r_hd * #r_tl #r_refl destruct normalize |
---|
1779 | cases hd cases r_hd normalize |
---|
1780 | [1: |
---|
1781 | #relevant |
---|
1782 | cases (inductive_hypothesis … relevant) |
---|
1783 | #acc_assm #tl_assm destruct % // |
---|
1784 | lapply (injective_plus_l ? ? ? acc_assm) |
---|
1785 | -acc_assm #acc_assm |
---|
1786 | change with (2 * acc_l = 2 * acc_r) in acc_assm; |
---|
1787 | lapply (injective_times_r ? ? ? ? acc_assm) /2/ |
---|
1788 | |4: |
---|
1789 | #relevant |
---|
1790 | cases (inductive_hypothesis … relevant) |
---|
1791 | #acc_assm #tl_assm destruct % // |
---|
1792 | change with (2 * acc_l = 2 * acc_r) in acc_assm; |
---|
1793 | lapply(injective_times_r ? ? ? ? acc_assm) /2/ |
---|
1794 | |2: |
---|
1795 | #relevant |
---|
1796 | change with ((nat_of_bitvector_aux r (2 * acc_l + 1) tl) = |
---|
1797 | (nat_of_bitvector_aux r (2 * acc_r) r_tl)) in relevant; |
---|
1798 | cases (eqb_decidable … (2 * acc_l + 1) (2 * acc_r)) |
---|
1799 | [1: |
---|
1800 | #eqb_true_assm |
---|
1801 | lapply (eqb_true_to_refl … eqb_true_assm) |
---|
1802 | #refl_assm |
---|
1803 | cases (two_times_n_plus_one_refl_two_times_n_to_False … refl_assm) |
---|
1804 | |2: |
---|
1805 | #eqb_false_assm |
---|
1806 | lapply (eqb_false_to_not_refl … eqb_false_assm) |
---|
1807 | #not_refl_assm cases not_refl_assm #absurd_assm |
---|
1808 | cases (inductive_hypothesis … relevant) #absurd |
---|
1809 | cases (absurd_assm absurd) |
---|
1810 | ] |
---|
1811 | |3: |
---|
1812 | #relevant |
---|
1813 | change with ((nat_of_bitvector_aux r (2 * acc_l) tl) = |
---|
1814 | (nat_of_bitvector_aux r (2 * acc_r + 1) r_tl)) in relevant; |
---|
1815 | cases (eqb_decidable … (2 * acc_l) (2 * acc_r + 1)) |
---|
1816 | [1: |
---|
1817 | #eqb_true_assm |
---|
1818 | lapply (eqb_true_to_refl … eqb_true_assm) |
---|
1819 | #refl_assm |
---|
1820 | lapply (sym_eq ? (2 * acc_l) (2 * acc_r + 1) refl_assm) |
---|
1821 | -refl_assm #refl_assm |
---|
1822 | cases (two_times_n_plus_one_refl_two_times_n_to_False … refl_assm) |
---|
1823 | |2: |
---|
1824 | #eqb_false_assm |
---|
1825 | lapply (eqb_false_to_not_refl … eqb_false_assm) |
---|
1826 | #not_refl_assm cases not_refl_assm #absurd_assm |
---|
1827 | cases (inductive_hypothesis … relevant) #absurd |
---|
1828 | cases (absurd_assm absurd) |
---|
1829 | ] |
---|
1830 | ] |
---|
1831 | ] |
---|
1832 | qed. |
---|
1833 | |
---|
1834 | lemma nat_of_bitvector_destruct: |
---|
1835 | ∀n: nat. |
---|
1836 | ∀l_hd, r_hd: bool. |
---|
1837 | ∀l_tl, r_tl: BitVector n. |
---|
1838 | nat_of_bitvector (S n) (l_hd:::l_tl) = nat_of_bitvector (S n) (r_hd:::r_tl) → |
---|
1839 | l_hd = r_hd ∧ nat_of_bitvector n l_tl = nat_of_bitvector n r_tl. |
---|
1840 | #n #l_hd #r_hd #l_tl #r_tl |
---|
1841 | normalize |
---|
1842 | cases l_hd cases r_hd |
---|
1843 | normalize |
---|
1844 | [4: |
---|
1845 | /2/ |
---|
1846 | |1: |
---|
1847 | #relevant |
---|
1848 | cases (nat_of_bitvector_aux_injective … relevant) |
---|
1849 | #_ #l_r_tl_refl destruct /2/ |
---|
1850 | |2,3: |
---|
1851 | #relevant |
---|
1852 | cases (nat_of_bitvector_aux_injective … relevant) |
---|
1853 | #absurd destruct(absurd) |
---|
1854 | ] |
---|
1855 | qed. |
---|
1856 | |
---|
1857 | lemma BitVector_cons_injective: |
---|
1858 | ∀n: nat. |
---|
1859 | ∀l_hd, r_hd: bool. |
---|
1860 | ∀l_tl, r_tl: BitVector n. |
---|
1861 | l_hd = r_hd → l_tl = r_tl → l_hd:::l_tl = r_hd:::r_tl. |
---|
1862 | #l #l_hd #r_hd #l_tl #r_tl |
---|
1863 | #l_refl #r_refl destruct % |
---|
1864 | qed. |
---|
1865 | |
---|
1866 | lemma refl_nat_of_bitvector_to_refl: |
---|
1867 | ∀n: nat. |
---|
1868 | ∀l, r: BitVector n. |
---|
1869 | nat_of_bitvector n l = nat_of_bitvector n r → l = r. |
---|
1870 | #n |
---|
1871 | elim n |
---|
1872 | [1: |
---|
1873 | #l #r |
---|
1874 | >(BitVector_O l) |
---|
1875 | >(BitVector_O r) |
---|
1876 | #_ % |
---|
1877 | |2: |
---|
1878 | #n' #inductive_hypothesis #l #r |
---|
1879 | lapply (BitVector_Sn ? l) #l_hypothesis |
---|
1880 | lapply (BitVector_Sn ? r) #r_hypothesis |
---|
1881 | cases l_hypothesis #l_hd #l_tail_hypothesis |
---|
1882 | cases r_hypothesis #r_hd #r_tail_hypothesis |
---|
1883 | cases l_tail_hypothesis #l_tl #l_hd_tl_refl |
---|
1884 | cases r_tail_hypothesis #r_tl #r_hd_tl_refl |
---|
1885 | destruct #cons_refl |
---|
1886 | cases (nat_of_bitvector_destruct n' l_hd r_hd l_tl r_tl cons_refl) |
---|
1887 | #hd_refl #tl_refl |
---|
1888 | @BitVector_cons_injective try assumption |
---|
1889 | @inductive_hypothesis assumption |
---|
1890 | ] |
---|
1891 | qed. |
---|