source: src/ASM/StatusProofs.ma @ 3051

Last change on this file since 3051 was 2285, checked in by sacerdot, 7 years ago
  1. duplicated code erased
  2. POP case finished up to lemmas on read_at_stack_pointer
File size: 13.5 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(vsplit … 1 7 ?) #bit_one #seven_bits normalize nodelta
30  cases (head' bool ??) normalize nodelta //
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_8051_sfr_set_clock:
74 ∀T,cm,s,pc. get_8051_sfr T cm (set_clock … s pc) = get_8051_sfr … s.
75 //
76qed.
77
78lemma get_bit_addressable_sfr_set_program_counter:
79 ∀T,cm,s,pc. get_bit_addressable_sfr T cm (set_program_counter … s pc) = get_bit_addressable_sfr … s.
80 //
81qed.
82
83lemma low_internal_ram_set_program_counter:
84 ∀T,cm,s,pc. low_internal_ram T cm (set_program_counter … s pc) = low_internal_ram … s.
85 //
86qed.
87
88lemma get_arg_8_set_program_counter:
89 ∀n.∀l:Vector addressing_mode_tag (S n).
90  ∀T,cm,s,pc,b.∀arg:l.
91   ∀prf:is_in ?
92    [[direct;indirect;registr;acc_a;acc_b;data;acc_dptr;ext_indirect;ext_indirect_dptr]] arg.
93   get_arg_8 T cm (set_program_counter … s pc) b arg = get_arg_8 … s b arg.
94 [ #n #l #T #cm #s #pc #b * *; #X try (#Y #H) try #H try % @⊥ @H
95 | cases arg in prf; *; normalize //
96 | skip ]
97qed.
98
99(*
100lemma set_bit_addressable_sfr_set_code_memory:
101  ∀T, U: Type[0].
102  ∀ps: PreStatus ?.
103  ∀code_mem.
104  ∀x.
105  ∀val.
106  set_bit_addressable_sfr ? (set_code_memory T U ps code_mem) x val =
107  set_code_memory T U (set_bit_addressable_sfr ? ps x val) code_mem.
108  #T #U #ps #code_mem #x #val
109  whd in ⊢ (??%?);
110  whd in ⊢ (???(???%?));
111  cases (eqb ? 128) [ normalize nodelta cases not_implemented
112  | normalize nodelta
113  cases (eqb (nat_of_bitvector 8 x) ?) [ normalize nodelta cases not_implemented
114  | normalize nodelta
115  cases (eqb (nat_of_bitvector 8 x) ?) [ normalize nodelta cases not_implemented
116  | normalize nodelta
117  cases (eqb ? 176) [ normalize nodelta %
118  | normalize nodelta
119  cases (eqb ? 153) [ normalize nodelta %
120  | normalize nodelta
121  cases (eqb ? 138) [ normalize nodelta %
122  | normalize nodelta
123  cases (eqb ? 139) [ normalize nodelta %
124  | normalize nodelta
125  cases (eqb ? 140) [ normalize nodelta %
126  | normalize nodelta
127  cases (eqb ? 141) [ normalize nodelta %
128  | normalize nodelta
129  cases (eqb ? 200) [ normalize nodelta %
130  | normalize nodelta
131  cases (eqb ? 202) [ normalize nodelta %
132  | normalize nodelta
133  cases (eqb ? 203) [ normalize nodelta %
134  | normalize nodelta
135  cases (eqb ? 204) [ normalize nodelta %
136  | normalize nodelta
137  cases (eqb ? 205) [ normalize nodelta %
138  | normalize nodelta
139  cases (eqb ? 135) [ normalize nodelta %
140  | normalize nodelta
141  cases (eqb ? 136) [ normalize nodelta %
142  | normalize nodelta
143  cases (eqb ? 137) [ normalize nodelta %
144  | normalize nodelta
145  cases (eqb ? 152) [ normalize nodelta %
146  | normalize nodelta
147  cases (eqb ? 168) [ normalize nodelta %
148  | normalize nodelta
149  cases (eqb ? 184) [ normalize nodelta %
150  | normalize nodelta
151  cases (eqb ? 129) [ normalize nodelta %
152  | normalize nodelta
153  cases (eqb ? 130) [ normalize nodelta %
154  | normalize nodelta
155  cases (eqb ? 131) [ normalize nodelta %
156  | normalize nodelta
157  cases (eqb ? 208) [ normalize nodelta %
158  | normalize nodelta
159  cases (eqb ? 224) [ normalize nodelta %
160  | normalize nodelta
161  cases (eqb ? 240) [ normalize nodelta %
162  | normalize nodelta
163    cases not_implemented
164  ]]]]]]]]]]]]]]]]]]]]]]]]]]
165qed.
166
167example set_arg_8_set_code_memory:
168  ∀n:nat.
169  ∀l:Vector addressing_mode_tag (S n).
170    ∀T: Type[0].
171    ∀U: Type[0].
172    ∀ps: PreStatus ?.
173    ∀code_mem.
174    ∀val.
175    ∀b: l.
176    ∀prf:is_in ?
177     [[direct;indirect;registr;acc_a;acc_b;ext_indirect;ext_indirect_dptr]] b.
178  set_arg_8 ? (set_code_memory T U ps code_mem) b val =
179  set_code_memory T U (set_arg_8 ? ps b val) code_mem.
180  [2,3: cases b in prf; *; normalize //]
181  #n #l #T #U #ps #code_mem #val * *;
182  #x try (#y #H) try #H whd in H; try cases H try %
183  whd in match set_arg_8; normalize nodelta
184  whd in match set_arg_8'; normalize nodelta
185  cases (vsplit bool 4 4 ?) #nu' #nl' normalize nodelta
186  cases (vsplit bool 1 3 nu') #bit1' #ignore' normalize nodelta
187  cases (get_index_v bool 4 nu' 0 ?) normalize nodelta
188  try % @set_bit_addressable_sfr_set_code_memory
189qed. *)
190
191lemma set_arg_8_set_program_counter:
192  ∀n:nat.
193  ∀l:Vector addressing_mode_tag (S n).
194    ∀T: Type[0]. ∀cm.
195    ∀ps: PreStatus ? cm.
196    ∀pc.
197    ∀val.
198    ∀b: l.
199    ∀prf:is_in ?
200     [[direct;indirect;registr;acc_a;acc_b;ext_indirect;ext_indirect_dptr]] b.
201  set_arg_8 … (set_program_counter T cm ps pc) b val =
202  set_program_counter T cm (set_arg_8 ?? ps b val) pc.
203  [2,3: cases b in prf; *; normalize //]
204  #n #l #T #cm #ps #pc #val * *;
205  #x try (#y #H) try #H whd in H; try cases H try %
206  whd in match set_arg_8; normalize nodelta
207  cases (vsplit bool ???) #bit_one #seven_bits normalize nodelta
208  cases (head' bool ??) normalize nodelta
209  try % cases daemon (* XXX: need @(set_bit_addressable_sfr_set_program_counter) *)
210qed.
211 
212(*lemma get_arg_8_set_code_memory:
213 ∀T1,T2,s,code_mem,b,arg.
214   get_arg_8 T1 (set_code_memory T2 T1 s code_mem) b arg = get_arg_8 … s b arg.
215 #T1 #T2 #s #code_mem #b #arg %
216qed.
217
218lemma set_code_memory_set_flags:
219 ∀T1,T2,s,f1,f2,f3,code_mem.
220  set_code_memory T1 T2 (set_flags T1 s f1 f2 f3) code_mem =
221   set_flags … (set_code_memory … s code_mem) f1 f2 f3.
222 #T1 #T2 #s #f1 #f2 #f3 #code_mem %
223qed.*)
224
225lemma set_program_counter_set_flags:
226 ∀T1,cm,s,f1,f2,f3,pc.
227  set_program_counter T1 cm (set_flags T1 cm s f1 f2 f3) pc =
228   set_flags … (set_program_counter … s pc) f1 f2 f3.
229 //
230qed.
231
232lemma program_counter_set_flags:
233 ∀T1,cm,s,f1,f2,f3.
234  program_counter T1 cm (set_flags T1 cm s f1 f2 f3) = program_counter … s.
235 //
236qed.
237
238lemma special_function_registers_8051_write_at_stack_pointer:
239 ∀T,cm,s,x.
240    special_function_registers_8051 T cm (write_at_stack_pointer T cm s x)
241  = special_function_registers_8051 T cm s.
242 #T #cm #s #x whd in ⊢ (??(???%)?);
243 cases (vsplit ????) #bit_one #seven_bits normalize nodelta
244  cases (head' bool ??) normalize nodelta %
245qed.
246
247lemma get_8051_sfr_write_at_stack_pointer:
248 ∀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.
249 #T #cm #s #x #y whd in ⊢ (??%%); >special_function_registers_8051_write_at_stack_pointer @refl
250qed.
251
252(*lemma code_memory_write_at_stack_pointer:
253 ∀T,s,x. code_memory T (write_at_stack_pointer T s x) = code_memory T s.
254 #T #s #x whd in ⊢ (??(??%)?);
255 cases (vsplit ????) #nu #nl normalize nodelta;
256 cases (get_index_v bool ????) %
257qed.*)
258
259lemma set_program_counter_set_low_internal_ram:
260 ∀T,cm,s,x,y.
261  set_program_counter T cm (set_low_internal_ram … s x) y =
262   set_low_internal_ram … (set_program_counter … s y) x.
263 //
264qed.
265
266lemma set_clock_set_low_internal_ram:
267 ∀T,cm,s,x,y.
268  set_clock T cm (set_low_internal_ram … s x) y =
269   set_low_internal_ram … (set_clock … s y) x.
270 //
271qed.
272
273lemma set_program_counter_set_high_internal_ram:
274 ∀T,cm,s,x,y.
275  set_program_counter T cm (set_high_internal_ram … s x) y =
276   set_high_internal_ram … (set_program_counter … s y) x.
277 //
278qed.
279
280lemma set_clock_set_high_internal_ram:
281 ∀T,cm,s,x,y.
282  set_clock T cm (set_high_internal_ram … s x) y =
283   set_high_internal_ram … (set_clock … s y) x.
284 //
285qed.
286
287lemma set_clock_set_program_counter:
288  ∀T,cm,s,x,y.
289    set_clock T cm (set_program_counter … s x) y =
290      set_program_counter … (set_clock … s y) x.
291 //
292qed.
293
294lemma set_low_internal_ram_set_high_internal_ram:
295 ∀T,cm,s,x,y.
296  set_low_internal_ram T cm (set_high_internal_ram … s x) y =
297   set_high_internal_ram … (set_low_internal_ram … s y) x.
298 //
299qed.
300
301lemma external_ram_write_at_stack_pointer:
302 ∀T,cm,s,x. external_ram T cm (write_at_stack_pointer T cm s x) = external_ram T cm s.
303 #T #cm #s #x whd in ⊢ (??(???%)?);
304 cases (vsplit ????) #bit_one #seven_bits normalize nodelta
305 cases (head' bool ??) %
306qed.
307
308lemma special_function_registers_8052_write_at_stack_pointer:
309 ∀T,cm,s,x.
310    special_function_registers_8052 T cm (write_at_stack_pointer T cm s x)
311  = special_function_registers_8052 T cm s.
312 #T #cm #s #x whd in ⊢ (??(???%)?);
313 cases (vsplit ????) #bit_one #seven_bits normalize nodelta
314 cases (head' bool ??) %
315qed.
316
317lemma p1_latch_write_at_stack_pointer:
318 ∀T,cm,s,x. p1_latch T cm (write_at_stack_pointer T cm s x) = p1_latch T cm s.
319 #T #cm #s #x whd in ⊢ (??(???%)?);
320 cases (vsplit ????) #bit_one #seven_bits normalize nodelta
321 cases (head' bool ??) %
322qed.
323
324lemma p3_latch_write_at_stack_pointer:
325 ∀T,cm,s,x. p3_latch T cm (write_at_stack_pointer T cm s x) = p3_latch T cm s.
326 #T #cm #s #x whd in ⊢ (??(???%)?);
327 cases (vsplit ????) #bit_one #seven_bits normalize nodelta
328 cases (head' bool ??) %
329qed.
330
331axiom get_index_v_set_index:
332 ∀T,n,x,m,p,y. get_index_v T n (set_index T n x m y p) m p = y.
333
334lemma get_8051_sfr_set_8051_sfr:
335 ∀T,cm,s,x,y. get_8051_sfr T cm (set_8051_sfr … s x y) x = y.
336 #T #cm * #A #B #C #D #E #F #G #H #I * #y whd in ⊢ (??(???%?)?);
337 whd in match get_8051_sfr; normalize nodelta @get_index_v_set_index
338qed.
339
340lemma program_counter_set_8051_sfr:
341 ∀T,cm,s,x,y. program_counter T cm (set_8051_sfr … s x y) = program_counter … s.
342 //
343qed.
344
345axiom program_counter_set_bit_addressable_sfr:
346  ∀m, cm, s, addr, v.
347   program_counter m cm (set_bit_addressable_sfr m cm s addr v) = program_counter m cm s.
348
349lemma program_counter_set_arg_8:
350  ∀m, cm, s, addr, v.
351   program_counter m cm (set_arg_8 m cm s addr v) = program_counter m cm s.
352  #m #cm #s #addr #byte
353  whd in match set_arg_8; normalize nodelta
354  cases daemon (*
355  whd in match set_arg_8'; normalize nodelta
356  cases addr #subaddressing_modein_proof
357  cases subaddressing_modein_proof
358  try (#addr normalize in addr; cases addr)
359  try (#ignore #addr normalize in addr; cases addr)
360  normalize nodelta try #_ try /demod/ try %
361  cases (vsplit bool 4 4 ?) #nu #nl normalize nodelta
362  cases (vsplit bool 1 3 ?) #ignore #three_bits normalize nodelta
363  cases (get_index_v bool 4 nu ? ?) normalize nodelta try /demod/ try % *)
364qed.
365
366(* XXX: this was compiling before! *)
367lemma program_counter_set_arg_1:
368  ∀m, cm, s, addr, v.
369   program_counter m cm (set_arg_1 m cm s addr v) = program_counter m cm s.
370  #m #cm #s #addr #v
371  whd in match set_arg_1; normalize nodelta
372  cases daemon (*
373  whd in match set_arg_1'; normalize nodelta
374  cases addr #subaddressing_modein_proof
375  cases subaddressing_modein_proof
376  try (#ignore #addr normalize in addr; cases addr)
377  try (#addr normalize in addr; cases addr)
378  normalize nodelta
379  cases (vsplit bool 4 4 ?) #nu #nl normalize nodelta try /demod/ try %
380  cases (vsplit bool 1 3 ?) #ignore #three_bits normalize nodelta
381  cases (get_index_v bool 4 nu ??) normalize nodelta
382  (* XXX: try /demod/ try % *)
383  cases daemon *)
384qed.
385
386lemma program_counter_set_arg_16:
387  ∀m, cm, s, addr, v.
388   program_counter m cm (set_arg_16 m cm s v addr) = program_counter m cm s.
389  #m #cm #s #addr #v
390  whd in match set_arg_16; normalize nodelta
391  whd in match set_arg_16'; normalize nodelta
392  cases addr #subaddressing_modein_proof
393  cases subaddressing_modein_proof
394  try (#ignore #addr normalize in addr; cases addr)
395  try (#addr normalize in addr; cases addr)
396  normalize nodelta
397  cases (vsplit bool 8 8 v) #bu #bl normalize nodelta /demod/ %
398qed.
399
400lemma program_counter_set_low_internal_ram:
401  ∀m, cm, s, v.
402   program_counter m cm (set_low_internal_ram m cm s v) = program_counter m cm s.
403  #m #cm #s #v
404  whd in match set_low_internal_ram; normalize nodelta %
405qed.
406
407lemma program_counter_set_high_internal_ram:
408  ∀m, cm, s, v.
409   program_counter m cm (set_high_internal_ram m cm s v) = program_counter m cm s.
410  #m #cm #s #v
411  whd in match set_high_internal_ram; normalize nodelta %
412qed.
413
414lemma program_counter_write_at_stack_pointer:
415  ∀m, cm, s, v.
416   program_counter m cm (write_at_stack_pointer m cm s v) = program_counter m cm s.
417  #m #cm #s #v
418  whd in match write_at_stack_pointer; normalize nodelta
419 cases (vsplit ????) #bit_one #seven_bits normalize nodelta
420 cases (head' bool ??) %
421qed.
422
423axiom get_arg_8_set_low_internal_ram:
424  ∀M,cm,s,x,b,z.
425    get_arg_8 M cm (set_low_internal_ram … s x) b z = get_arg_8 … s b z.
426
427lemma split_eq_status:
428 ∀T,cm.
429 ∀A1,A2,A3,A4,A5,A6,A7,A8,A9.
430 ∀B1,B2,B3,B4,B5,B6,B7,B8,B9.
431  A1=B1 → A2=B2 → A3=B3 → A4=B4 → A5=B5 → A6=B6 → A7=B7 → A8=B8 → A9=B9 →
432   mk_PreStatus T cm A1 A2 A3 A4 A5 A6 A7 A8 A9 =
433   mk_PreStatus T cm B1 B2 B3 B4 B5 B6 B7 B8 B9.
434 //
435qed.
Note: See TracBrowser for help on using the repository browser.