source: src/ASM/StatusProofs.ma @ 1959

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

Commented out diverging application of demodulation and closed goals with a daemon in order to get ASM/StatusProofs.ma to compile.
File size: 13.4 KB
Line 
1include "ASM/Status.ma".
2
3(* clock_set_bit_addressable_sfr defined in ASM/Status.ma *)
4
5lemma 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  //
11qed.
12
13lemma 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  //
19qed.
20
21lemma 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 ?) //
31qed.
32
33lemma clock_set_clock:
34  ∀M: Type[0]. ∀cm.
35  ∀s: PreStatus M cm.
36  ∀v.
37    clock ?? (set_clock … s v) = v.
38 //
39qed.
40
41lemma 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  //
47qed.
48
49lemma 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 //
56qed.
57
58lemma clock_set_flags:
59 ∀M,cm,s,f1,f2,f3. clock M cm s = clock … (set_flags … s f1 f2 f3).
60//
61qed.
62
63lemma get_register_set_program_counter:
64 ∀T,cm,s,pc. get_register T cm (set_program_counter … s pc) = get_register … s.
65 //
66qed.
67
68lemma 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 //
71qed.
72
73lemma 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 //
76qed.
77
78lemma 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 //
81qed.
82
83example 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 ]
92qed.
93
94(*
95lemma 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  ]]]]]]]]]]]]]]]]]]]]]]]]]]
160qed.
161
162example 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
184qed. *)
185
186example 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)*)
207qed.
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 %
213qed.
214
215lemma 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 %
220qed.*)
221
222lemma 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 //
227qed.
228
229lemma 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 //
233qed.
234
235lemma 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 ????) %
242qed.
243
244lemma 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
247qed.
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 ????) %
254qed.*)
255
256lemma 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 //
261qed.
262
263lemma 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 //
268qed.
269
270lemma 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 //
275qed.
276
277lemma 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 //
282qed.
283
284lemma 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 //
289qed.
290
291lemma 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 //
296qed.
297
298lemma 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 ????) %
303qed.
304
305lemma 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 ????) %
312qed.
313
314lemma 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 ????) %
319qed.
320
321lemma 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 ????) %
326qed.
327
328axiom 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
331lemma 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
335qed.
336
337lemma 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 //
340qed.
341
342axiom 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 *)
347lemma 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 %
361qed.
362
363(* XXX: this was compiling before! *)
364lemma 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
380qed.
381
382lemma 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/ %
394qed.
395
396lemma 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 %
401qed.
402
403lemma 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 %
408qed.
409
410lemma 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/ %
417qed.
418
419axiom 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
423lemma 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 //
431qed.
Note: See TracBrowser for help on using the repository browser.