1 | include "ASM/Status.ma". |
---|
2 | |
---|
3 | (* clock_set_bit_addressable_sfr defined in ASM/Status.ma *) |
---|
4 | |
---|
5 | lemma clock_set_low_internal_ram: |
---|
6 | ∀M: Type[0]. ∀cm. |
---|
7 | ∀s: PreStatus M cm. |
---|
8 | ∀ram: BitVectorTrie Byte 7. |
---|
9 | clock M cm (set_low_internal_ram … s ram) = clock M cm s. |
---|
10 | // |
---|
11 | qed. |
---|
12 | |
---|
13 | lemma clock_set_high_internal_ram: |
---|
14 | ∀m: Type[0]. ∀cm. |
---|
15 | ∀s: PreStatus m cm. |
---|
16 | ∀ram: BitVectorTrie Byte 7. |
---|
17 | clock ?? (set_high_internal_ram … s ram) = clock … s. |
---|
18 | // |
---|
19 | qed. |
---|
20 | |
---|
21 | lemma clock_write_at_stack_pointer: |
---|
22 | ∀m: Type[0]. |
---|
23 | ∀cm:m. |
---|
24 | ∀s: PreStatus m cm. |
---|
25 | ∀v: Byte. |
---|
26 | clock ?? (write_at_stack_pointer … s v) = clock ?? s. |
---|
27 | #m #s #v |
---|
28 | whd in match write_at_stack_pointer; normalize nodelta |
---|
29 | cases(split … 4 4 ?) #nu #nl normalize nodelta |
---|
30 | cases(get_index_v … 4 nu 0 ?) // |
---|
31 | qed. |
---|
32 | |
---|
33 | lemma clock_set_clock: |
---|
34 | ∀M: Type[0]. ∀cm. |
---|
35 | ∀s: PreStatus M cm. |
---|
36 | ∀v. |
---|
37 | clock ?? (set_clock … s v) = v. |
---|
38 | // |
---|
39 | qed. |
---|
40 | |
---|
41 | lemma clock_set_program_counter: |
---|
42 | ∀M: Type[0]. ∀cm. |
---|
43 | ∀s: PreStatus M cm. |
---|
44 | ∀pc: Word. |
---|
45 | clock M cm (set_program_counter … s pc) = clock … s. |
---|
46 | // |
---|
47 | qed. |
---|
48 | |
---|
49 | lemma clock_set_8051_sfr: |
---|
50 | ∀M: Type[0]. ∀cm. |
---|
51 | ∀s: PreStatus M cm. |
---|
52 | ∀sfr: SFR8051. |
---|
53 | ∀v: Byte. |
---|
54 | clock ?? (set_8051_sfr … s sfr v) = clock … s. |
---|
55 | // |
---|
56 | qed. |
---|
57 | |
---|
58 | lemma clock_set_flags: |
---|
59 | ∀M,cm,s,f1,f2,f3. clock M cm s = clock … (set_flags … s f1 f2 f3). |
---|
60 | // |
---|
61 | qed. |
---|
62 | |
---|
63 | lemma get_register_set_program_counter: |
---|
64 | ∀T,cm,s,pc. get_register T cm (set_program_counter … s pc) = get_register … s. |
---|
65 | // |
---|
66 | qed. |
---|
67 | |
---|
68 | lemma get_8051_sfr_set_program_counter: |
---|
69 | ∀T,cm,s,pc. get_8051_sfr T cm (set_program_counter … s pc) = get_8051_sfr … s. |
---|
70 | // |
---|
71 | qed. |
---|
72 | |
---|
73 | lemma get_bit_addressable_sfr_set_program_counter: |
---|
74 | ∀T,cm,s,pc. get_bit_addressable_sfr T cm (set_program_counter … s pc) = get_bit_addressable_sfr … s. |
---|
75 | // |
---|
76 | qed. |
---|
77 | |
---|
78 | lemma low_internal_ram_set_program_counter: |
---|
79 | ∀T,cm,s,pc. low_internal_ram T cm (set_program_counter … s pc) = low_internal_ram … s. |
---|
80 | // |
---|
81 | qed. |
---|
82 | |
---|
83 | example get_arg_8_set_program_counter: |
---|
84 | ∀n.∀l:Vector addressing_mode_tag (S n). |
---|
85 | ∀T,cm,s,pc,b.∀arg:l. |
---|
86 | ∀prf:is_in ? |
---|
87 | [[direct;indirect;registr;acc_a;acc_b;data;acc_dptr;ext_indirect;ext_indirect_dptr]] arg. |
---|
88 | get_arg_8 T cm (set_program_counter … s pc) b arg = get_arg_8 … s b arg. |
---|
89 | [ #n #l #T #cm #s #pc #b * *; #X try (#Y #H) try #H try % @⊥ @H |
---|
90 | | cases arg in prf; *; normalize // |
---|
91 | | skip ] |
---|
92 | qed. |
---|
93 | |
---|
94 | (* |
---|
95 | lemma set_bit_addressable_sfr_set_code_memory: |
---|
96 | ∀T, U: Type[0]. |
---|
97 | ∀ps: PreStatus ?. |
---|
98 | ∀code_mem. |
---|
99 | ∀x. |
---|
100 | ∀val. |
---|
101 | set_bit_addressable_sfr ? (set_code_memory T U ps code_mem) x val = |
---|
102 | set_code_memory T U (set_bit_addressable_sfr ? ps x val) code_mem. |
---|
103 | #T #U #ps #code_mem #x #val |
---|
104 | whd in ⊢ (??%?); |
---|
105 | whd in ⊢ (???(???%?)); |
---|
106 | cases (eqb ? 128) [ normalize nodelta cases not_implemented |
---|
107 | | normalize nodelta |
---|
108 | cases (eqb (nat_of_bitvector 8 x) ?) [ normalize nodelta cases not_implemented |
---|
109 | | normalize nodelta |
---|
110 | cases (eqb (nat_of_bitvector 8 x) ?) [ normalize nodelta cases not_implemented |
---|
111 | | normalize nodelta |
---|
112 | cases (eqb ? 176) [ normalize nodelta % |
---|
113 | | normalize nodelta |
---|
114 | cases (eqb ? 153) [ normalize nodelta % |
---|
115 | | normalize nodelta |
---|
116 | cases (eqb ? 138) [ normalize nodelta % |
---|
117 | | normalize nodelta |
---|
118 | cases (eqb ? 139) [ normalize nodelta % |
---|
119 | | normalize nodelta |
---|
120 | cases (eqb ? 140) [ normalize nodelta % |
---|
121 | | normalize nodelta |
---|
122 | cases (eqb ? 141) [ normalize nodelta % |
---|
123 | | normalize nodelta |
---|
124 | cases (eqb ? 200) [ normalize nodelta % |
---|
125 | | normalize nodelta |
---|
126 | cases (eqb ? 202) [ normalize nodelta % |
---|
127 | | normalize nodelta |
---|
128 | cases (eqb ? 203) [ normalize nodelta % |
---|
129 | | normalize nodelta |
---|
130 | cases (eqb ? 204) [ normalize nodelta % |
---|
131 | | normalize nodelta |
---|
132 | cases (eqb ? 205) [ normalize nodelta % |
---|
133 | | normalize nodelta |
---|
134 | cases (eqb ? 135) [ normalize nodelta % |
---|
135 | | normalize nodelta |
---|
136 | cases (eqb ? 136) [ normalize nodelta % |
---|
137 | | normalize nodelta |
---|
138 | cases (eqb ? 137) [ normalize nodelta % |
---|
139 | | normalize nodelta |
---|
140 | cases (eqb ? 152) [ normalize nodelta % |
---|
141 | | normalize nodelta |
---|
142 | cases (eqb ? 168) [ normalize nodelta % |
---|
143 | | normalize nodelta |
---|
144 | cases (eqb ? 184) [ normalize nodelta % |
---|
145 | | normalize nodelta |
---|
146 | cases (eqb ? 129) [ normalize nodelta % |
---|
147 | | normalize nodelta |
---|
148 | cases (eqb ? 130) [ normalize nodelta % |
---|
149 | | normalize nodelta |
---|
150 | cases (eqb ? 131) [ normalize nodelta % |
---|
151 | | normalize nodelta |
---|
152 | cases (eqb ? 208) [ normalize nodelta % |
---|
153 | | normalize nodelta |
---|
154 | cases (eqb ? 224) [ normalize nodelta % |
---|
155 | | normalize nodelta |
---|
156 | cases (eqb ? 240) [ normalize nodelta % |
---|
157 | | normalize nodelta |
---|
158 | cases not_implemented |
---|
159 | ]]]]]]]]]]]]]]]]]]]]]]]]]] |
---|
160 | qed. |
---|
161 | |
---|
162 | example set_arg_8_set_code_memory: |
---|
163 | ∀n:nat. |
---|
164 | ∀l:Vector addressing_mode_tag (S n). |
---|
165 | ∀T: Type[0]. |
---|
166 | ∀U: Type[0]. |
---|
167 | ∀ps: PreStatus ?. |
---|
168 | ∀code_mem. |
---|
169 | ∀val. |
---|
170 | ∀b: l. |
---|
171 | ∀prf:is_in ? |
---|
172 | [[direct;indirect;registr;acc_a;acc_b;ext_indirect;ext_indirect_dptr]] b. |
---|
173 | set_arg_8 ? (set_code_memory T U ps code_mem) b val = |
---|
174 | set_code_memory T U (set_arg_8 ? ps b val) code_mem. |
---|
175 | [2,3: cases b in prf; *; normalize //] |
---|
176 | #n #l #T #U #ps #code_mem #val * *; |
---|
177 | #x try (#y #H) try #H whd in H; try cases H try % |
---|
178 | whd in match set_arg_8; normalize nodelta |
---|
179 | whd in match set_arg_8'; normalize nodelta |
---|
180 | cases (split bool 4 4 ?) #nu' #nl' normalize nodelta |
---|
181 | cases (split bool 1 3 nu') #bit1' #ignore' normalize nodelta |
---|
182 | cases (get_index_v bool 4 nu' 0 ?) normalize nodelta |
---|
183 | try % @set_bit_addressable_sfr_set_code_memory |
---|
184 | qed. *) |
---|
185 | |
---|
186 | example set_arg_8_set_program_counter: |
---|
187 | ∀n:nat. |
---|
188 | ∀l:Vector addressing_mode_tag (S n). |
---|
189 | ∀T: Type[0]. ∀cm. |
---|
190 | ∀ps: PreStatus ? cm. |
---|
191 | ∀pc. |
---|
192 | ∀val. |
---|
193 | ∀b: l. |
---|
194 | ∀prf:is_in ? |
---|
195 | [[direct;indirect;registr;acc_a;acc_b;ext_indirect;ext_indirect_dptr]] b. |
---|
196 | set_arg_8 … (set_program_counter T cm ps pc) b val = |
---|
197 | set_program_counter T cm (set_arg_8 ?? ps b val) pc. |
---|
198 | [2,3: cases b in prf; *; normalize //] |
---|
199 | #n #l #T #cm #ps #pc #val * *; |
---|
200 | #x try (#y #H) try #H whd in H; try cases H try % |
---|
201 | whd in match set_arg_8; normalize nodelta |
---|
202 | whd in match set_arg_8'; normalize nodelta |
---|
203 | cases (split bool 4 4 ?) #nu' #nl' normalize nodelta |
---|
204 | cases (split bool 1 3 nu') #bit1' #ignore' normalize nodelta |
---|
205 | cases (get_index_v bool 4 nu' 0 ?) normalize nodelta |
---|
206 | try % cases daemon (*@(set_bit_addressable_sfr_set_program_counter)*) |
---|
207 | qed. |
---|
208 | |
---|
209 | (*lemma get_arg_8_set_code_memory: |
---|
210 | ∀T1,T2,s,code_mem,b,arg. |
---|
211 | get_arg_8 T1 (set_code_memory T2 T1 s code_mem) b arg = get_arg_8 … s b arg. |
---|
212 | #T1 #T2 #s #code_mem #b #arg % |
---|
213 | qed. |
---|
214 | |
---|
215 | lemma set_code_memory_set_flags: |
---|
216 | ∀T1,T2,s,f1,f2,f3,code_mem. |
---|
217 | set_code_memory T1 T2 (set_flags T1 s f1 f2 f3) code_mem = |
---|
218 | set_flags … (set_code_memory … s code_mem) f1 f2 f3. |
---|
219 | #T1 #T2 #s #f1 #f2 #f3 #code_mem % |
---|
220 | qed.*) |
---|
221 | |
---|
222 | lemma set_program_counter_set_flags: |
---|
223 | ∀T1,cm,s,f1,f2,f3,pc. |
---|
224 | set_program_counter T1 cm (set_flags T1 cm s f1 f2 f3) pc = |
---|
225 | set_flags … (set_program_counter … s pc) f1 f2 f3. |
---|
226 | // |
---|
227 | qed. |
---|
228 | |
---|
229 | lemma program_counter_set_flags: |
---|
230 | ∀T1,cm,s,f1,f2,f3. |
---|
231 | program_counter T1 cm (set_flags T1 cm s f1 f2 f3) = program_counter … s. |
---|
232 | // |
---|
233 | qed. |
---|
234 | |
---|
235 | lemma special_function_registers_8051_write_at_stack_pointer: |
---|
236 | ∀T,cm,s,x. |
---|
237 | special_function_registers_8051 T cm (write_at_stack_pointer T cm s x) |
---|
238 | = special_function_registers_8051 T cm s. |
---|
239 | #T #cm #s #x whd in ⊢ (??(???%)?); |
---|
240 | cases (split ????) #nu #nl normalize nodelta; |
---|
241 | cases (get_index_v bool ????) % |
---|
242 | qed. |
---|
243 | |
---|
244 | lemma get_8051_sfr_write_at_stack_pointer: |
---|
245 | ∀T,cm,s,x,y. get_8051_sfr T cm (write_at_stack_pointer T cm s x) y = get_8051_sfr T cm s y. |
---|
246 | #T #cm #s #x #y whd in ⊢ (??%%); >special_function_registers_8051_write_at_stack_pointer @refl |
---|
247 | qed. |
---|
248 | |
---|
249 | (*lemma code_memory_write_at_stack_pointer: |
---|
250 | ∀T,s,x. code_memory T (write_at_stack_pointer T s x) = code_memory T s. |
---|
251 | #T #s #x whd in ⊢ (??(??%)?); |
---|
252 | cases (split ????) #nu #nl normalize nodelta; |
---|
253 | cases (get_index_v bool ????) % |
---|
254 | qed.*) |
---|
255 | |
---|
256 | lemma set_program_counter_set_low_internal_ram: |
---|
257 | ∀T,cm,s,x,y. |
---|
258 | set_program_counter T cm (set_low_internal_ram … s x) y = |
---|
259 | set_low_internal_ram … (set_program_counter … s y) x. |
---|
260 | // |
---|
261 | qed. |
---|
262 | |
---|
263 | lemma set_clock_set_low_internal_ram: |
---|
264 | ∀T,cm,s,x,y. |
---|
265 | set_clock T cm (set_low_internal_ram … s x) y = |
---|
266 | set_low_internal_ram … (set_clock … s y) x. |
---|
267 | // |
---|
268 | qed. |
---|
269 | |
---|
270 | lemma set_program_counter_set_high_internal_ram: |
---|
271 | ∀T,cm,s,x,y. |
---|
272 | set_program_counter T cm (set_high_internal_ram … s x) y = |
---|
273 | set_high_internal_ram … (set_program_counter … s y) x. |
---|
274 | // |
---|
275 | qed. |
---|
276 | |
---|
277 | lemma set_clock_set_high_internal_ram: |
---|
278 | ∀T,cm,s,x,y. |
---|
279 | set_clock T cm (set_high_internal_ram … s x) y = |
---|
280 | set_high_internal_ram … (set_clock … s y) x. |
---|
281 | // |
---|
282 | qed. |
---|
283 | |
---|
284 | lemma set_clock_set_program_counter: |
---|
285 | ∀T,cm,s,x,y. |
---|
286 | set_clock T cm (set_program_counter … s x) y = |
---|
287 | set_program_counter … (set_clock … s y) x. |
---|
288 | // |
---|
289 | qed. |
---|
290 | |
---|
291 | lemma set_low_internal_ram_set_high_internal_ram: |
---|
292 | ∀T,cm,s,x,y. |
---|
293 | set_low_internal_ram T cm (set_high_internal_ram … s x) y = |
---|
294 | set_high_internal_ram … (set_low_internal_ram … s y) x. |
---|
295 | // |
---|
296 | qed. |
---|
297 | |
---|
298 | lemma external_ram_write_at_stack_pointer: |
---|
299 | ∀T,cm,s,x. external_ram T cm (write_at_stack_pointer T cm s x) = external_ram T cm s. |
---|
300 | #T #cm #s #x whd in ⊢ (??(???%)?); |
---|
301 | cases (split ????) #nu #nl normalize nodelta; |
---|
302 | cases (get_index_v bool ????) % |
---|
303 | qed. |
---|
304 | |
---|
305 | lemma special_function_registers_8052_write_at_stack_pointer: |
---|
306 | ∀T,cm,s,x. |
---|
307 | special_function_registers_8052 T cm (write_at_stack_pointer T cm s x) |
---|
308 | = special_function_registers_8052 T cm s. |
---|
309 | #T #cm #s #x whd in ⊢ (??(???%)?); |
---|
310 | cases (split ????) #nu #nl normalize nodelta; |
---|
311 | cases (get_index_v bool ????) % |
---|
312 | qed. |
---|
313 | |
---|
314 | lemma p1_latch_write_at_stack_pointer: |
---|
315 | ∀T,cm,s,x. p1_latch T cm (write_at_stack_pointer T cm s x) = p1_latch T cm s. |
---|
316 | #T #cm #s #x whd in ⊢ (??(???%)?); |
---|
317 | cases (split ????) #nu #nl normalize nodelta; |
---|
318 | cases (get_index_v bool ????) % |
---|
319 | qed. |
---|
320 | |
---|
321 | lemma p3_latch_write_at_stack_pointer: |
---|
322 | ∀T,cm,s,x. p3_latch T cm (write_at_stack_pointer T cm s x) = p3_latch T cm s. |
---|
323 | #T #cm #s #x whd in ⊢ (??(???%)?); |
---|
324 | cases (split ????) #nu #nl normalize nodelta; |
---|
325 | cases (get_index_v bool ????) % |
---|
326 | qed. |
---|
327 | |
---|
328 | axiom get_index_v_set_index: |
---|
329 | ∀T,n,x,m,p,y. get_index_v T n (set_index T n x m y p) m p = y. |
---|
330 | |
---|
331 | lemma get_8051_sfr_set_8051_sfr: |
---|
332 | ∀T,cm,s,x,y. get_8051_sfr T cm (set_8051_sfr … s x y) x = y. |
---|
333 | #T #cm * #A #B #C #D #E #F #G #H #I * #y whd in ⊢ (??(???%?)?); |
---|
334 | whd in match get_8051_sfr; normalize nodelta @get_index_v_set_index |
---|
335 | qed. |
---|
336 | |
---|
337 | lemma program_counter_set_8051_sfr: |
---|
338 | ∀T,cm,s,x,y. program_counter T cm (set_8051_sfr … s x y) = program_counter … s. |
---|
339 | // |
---|
340 | qed. |
---|
341 | |
---|
342 | axiom program_counter_set_bit_addressable_sfr: |
---|
343 | ∀m, cm, s, addr, v. |
---|
344 | program_counter m cm (set_bit_addressable_sfr m cm s addr v) = program_counter m cm s. |
---|
345 | |
---|
346 | (* XXX: to be moved elsewhere *) |
---|
347 | lemma program_counter_set_arg_8: |
---|
348 | ∀m, cm, s, addr, v. |
---|
349 | program_counter m cm (set_arg_8 m cm s addr v) = program_counter m cm s. |
---|
350 | #m #cm #s #addr #byte |
---|
351 | whd in match set_arg_8; normalize nodelta |
---|
352 | whd in match set_arg_8'; normalize nodelta |
---|
353 | cases addr #subaddressing_modein_proof |
---|
354 | cases subaddressing_modein_proof |
---|
355 | try (#addr normalize in addr; cases addr) |
---|
356 | try (#ignore #addr normalize in addr; cases addr) |
---|
357 | normalize nodelta try #_ try /demod/ try % |
---|
358 | cases (split bool 4 4 ?) #nu #nl normalize nodelta |
---|
359 | cases (split bool 1 3 ?) #ignore #three_bits normalize nodelta |
---|
360 | cases (get_index_v bool 4 nu ? ?) normalize nodelta try /demod/ try % |
---|
361 | qed. |
---|
362 | |
---|
363 | (* XXX: this was compiling before! *) |
---|
364 | lemma program_counter_set_arg_1: |
---|
365 | ∀m, cm, s, addr, v. |
---|
366 | program_counter m cm (set_arg_1 m cm s addr v) = program_counter m cm s. |
---|
367 | #m #cm #s #addr #v |
---|
368 | whd in match set_arg_1; normalize nodelta |
---|
369 | whd in match set_arg_1'; normalize nodelta |
---|
370 | cases addr #subaddressing_modein_proof |
---|
371 | cases subaddressing_modein_proof |
---|
372 | try (#ignore #addr normalize in addr; cases addr) |
---|
373 | try (#addr normalize in addr; cases addr) |
---|
374 | normalize nodelta |
---|
375 | cases (split bool 4 4 ?) #nu #nl normalize nodelta try /demod/ try % |
---|
376 | cases (split bool 1 3 ?) #ignore #three_bits normalize nodelta |
---|
377 | cases (get_index_v bool 4 nu ??) normalize nodelta |
---|
378 | (* XXX: try /demod/ try % *) |
---|
379 | cases daemon |
---|
380 | qed. |
---|
381 | |
---|
382 | lemma program_counter_set_arg_16: |
---|
383 | ∀m, cm, s, addr, v. |
---|
384 | program_counter m cm (set_arg_16 m cm s v addr) = program_counter m cm s. |
---|
385 | #m #cm #s #addr #v |
---|
386 | whd in match set_arg_16; normalize nodelta |
---|
387 | whd in match set_arg_16'; normalize nodelta |
---|
388 | cases addr #subaddressing_modein_proof |
---|
389 | cases subaddressing_modein_proof |
---|
390 | try (#ignore #addr normalize in addr; cases addr) |
---|
391 | try (#addr normalize in addr; cases addr) |
---|
392 | normalize nodelta |
---|
393 | cases (split bool 8 8 v) #bu #bl normalize nodelta /demod/ % |
---|
394 | qed. |
---|
395 | |
---|
396 | lemma program_counter_set_low_internal_ram: |
---|
397 | ∀m, cm, s, v. |
---|
398 | program_counter m cm (set_low_internal_ram m cm s v) = program_counter m cm s. |
---|
399 | #m #cm #s #v |
---|
400 | whd in match set_low_internal_ram; normalize nodelta % |
---|
401 | qed. |
---|
402 | |
---|
403 | lemma program_counter_set_high_internal_ram: |
---|
404 | ∀m, cm, s, v. |
---|
405 | program_counter m cm (set_high_internal_ram m cm s v) = program_counter m cm s. |
---|
406 | #m #cm #s #v |
---|
407 | whd in match set_high_internal_ram; normalize nodelta % |
---|
408 | qed. |
---|
409 | |
---|
410 | lemma program_counter_write_at_stack_pointer: |
---|
411 | ∀m, cm, s, v. |
---|
412 | program_counter m cm (write_at_stack_pointer m cm s v) = program_counter m cm s. |
---|
413 | #m #cm #s #v |
---|
414 | whd in match write_at_stack_pointer; normalize nodelta |
---|
415 | cases (split bool 4 4 ?) #nu #nl normalize nodelta |
---|
416 | cases (get_index_v bool 4 nu ??) normalize nodelta /demod/ % |
---|
417 | qed. |
---|
418 | |
---|
419 | axiom get_arg_8_set_low_internal_ram: |
---|
420 | ∀M,cm,s,x,b,z. |
---|
421 | get_arg_8 M cm (set_low_internal_ram … s x) b z = get_arg_8 … s b z. |
---|
422 | |
---|
423 | lemma split_eq_status: |
---|
424 | ∀T,cm. |
---|
425 | ∀A1,A2,A3,A4,A5,A6,A7,A8,A9. |
---|
426 | ∀B1,B2,B3,B4,B5,B6,B7,B8,B9. |
---|
427 | A1=B1 → A2=B2 → A3=B3 → A4=B4 → A5=B5 → A6=B6 → A7=B7 → A8=B8 → A9=B9 → |
---|
428 | mk_PreStatus T cm A1 A2 A3 A4 A5 A6 A7 A8 A9 = |
---|
429 | mk_PreStatus T cm B1 B2 B3 B4 B5 B6 B7 B8 B9. |
---|
430 | // |
---|
431 | qed. |
---|