source: src/ASM/StatusProofs.ma @ 2272

Last change on this file since 2272 was 2272, checked in by mulligan, 7 years ago

Changed proof strategy for main lemma after noticed that the current approach would not work with POP, RET, etc. Ported throughout the assembly proof and all the way up to Test.ma.

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(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_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
83lemma 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 (vsplit bool 4 4 ?) #nu' #nl' normalize nodelta
181  cases (vsplit 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
186lemma 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  cases (vsplit bool ???) #bit_one #seven_bits normalize nodelta
203  cases (head' bool ??) normalize nodelta
204  try % cases daemon (* XXX: need @(set_bit_addressable_sfr_set_program_counter) *)
205qed.
206 
207(*lemma get_arg_8_set_code_memory:
208 ∀T1,T2,s,code_mem,b,arg.
209   get_arg_8 T1 (set_code_memory T2 T1 s code_mem) b arg = get_arg_8 … s b arg.
210 #T1 #T2 #s #code_mem #b #arg %
211qed.
212
213lemma set_code_memory_set_flags:
214 ∀T1,T2,s,f1,f2,f3,code_mem.
215  set_code_memory T1 T2 (set_flags T1 s f1 f2 f3) code_mem =
216   set_flags … (set_code_memory … s code_mem) f1 f2 f3.
217 #T1 #T2 #s #f1 #f2 #f3 #code_mem %
218qed.*)
219
220lemma set_program_counter_set_flags:
221 ∀T1,cm,s,f1,f2,f3,pc.
222  set_program_counter T1 cm (set_flags T1 cm s f1 f2 f3) pc =
223   set_flags … (set_program_counter … s pc) f1 f2 f3.
224 //
225qed.
226
227lemma program_counter_set_flags:
228 ∀T1,cm,s,f1,f2,f3.
229  program_counter T1 cm (set_flags T1 cm s f1 f2 f3) = program_counter … s.
230 //
231qed.
232
233lemma special_function_registers_8051_write_at_stack_pointer:
234 ∀T,cm,s,x.
235    special_function_registers_8051 T cm (write_at_stack_pointer T cm s x)
236  = special_function_registers_8051 T cm s.
237 #T #cm #s #x whd in ⊢ (??(???%)?);
238 cases (vsplit ????) #bit_one #seven_bits normalize nodelta
239  cases (head' bool ??) normalize nodelta %
240qed.
241
242lemma get_8051_sfr_write_at_stack_pointer:
243 ∀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.
244 #T #cm #s #x #y whd in ⊢ (??%%); >special_function_registers_8051_write_at_stack_pointer @refl
245qed.
246
247(*lemma code_memory_write_at_stack_pointer:
248 ∀T,s,x. code_memory T (write_at_stack_pointer T s x) = code_memory T s.
249 #T #s #x whd in ⊢ (??(??%)?);
250 cases (vsplit ????) #nu #nl normalize nodelta;
251 cases (get_index_v bool ????) %
252qed.*)
253
254lemma set_program_counter_set_low_internal_ram:
255 ∀T,cm,s,x,y.
256  set_program_counter T cm (set_low_internal_ram … s x) y =
257   set_low_internal_ram … (set_program_counter … s y) x.
258 //
259qed.
260
261lemma set_clock_set_low_internal_ram:
262 ∀T,cm,s,x,y.
263  set_clock T cm (set_low_internal_ram … s x) y =
264   set_low_internal_ram … (set_clock … s y) x.
265 //
266qed.
267
268lemma set_program_counter_set_high_internal_ram:
269 ∀T,cm,s,x,y.
270  set_program_counter T cm (set_high_internal_ram … s x) y =
271   set_high_internal_ram … (set_program_counter … s y) x.
272 //
273qed.
274
275lemma set_clock_set_high_internal_ram:
276 ∀T,cm,s,x,y.
277  set_clock T cm (set_high_internal_ram … s x) y =
278   set_high_internal_ram … (set_clock … s y) x.
279 //
280qed.
281
282lemma set_clock_set_program_counter:
283  ∀T,cm,s,x,y.
284    set_clock T cm (set_program_counter … s x) y =
285      set_program_counter … (set_clock … s y) x.
286 //
287qed.
288
289lemma set_low_internal_ram_set_high_internal_ram:
290 ∀T,cm,s,x,y.
291  set_low_internal_ram T cm (set_high_internal_ram … s x) y =
292   set_high_internal_ram … (set_low_internal_ram … s y) x.
293 //
294qed.
295
296lemma external_ram_write_at_stack_pointer:
297 ∀T,cm,s,x. external_ram T cm (write_at_stack_pointer T cm s x) = external_ram T cm s.
298 #T #cm #s #x whd in ⊢ (??(???%)?);
299 cases (vsplit ????) #bit_one #seven_bits normalize nodelta
300 cases (head' bool ??) %
301qed.
302
303lemma special_function_registers_8052_write_at_stack_pointer:
304 ∀T,cm,s,x.
305    special_function_registers_8052 T cm (write_at_stack_pointer T cm s x)
306  = special_function_registers_8052 T cm s.
307 #T #cm #s #x whd in ⊢ (??(???%)?);
308 cases (vsplit ????) #bit_one #seven_bits normalize nodelta
309 cases (head' bool ??) %
310qed.
311
312lemma p1_latch_write_at_stack_pointer:
313 ∀T,cm,s,x. p1_latch T cm (write_at_stack_pointer T cm s x) = p1_latch T cm s.
314 #T #cm #s #x whd in ⊢ (??(???%)?);
315 cases (vsplit ????) #bit_one #seven_bits normalize nodelta
316 cases (head' bool ??) %
317qed.
318
319lemma p3_latch_write_at_stack_pointer:
320 ∀T,cm,s,x. p3_latch T cm (write_at_stack_pointer T cm s x) = p3_latch T cm s.
321 #T #cm #s #x whd in ⊢ (??(???%)?);
322 cases (vsplit ????) #bit_one #seven_bits normalize nodelta
323 cases (head' bool ??) %
324qed.
325
326axiom get_index_v_set_index:
327 ∀T,n,x,m,p,y. get_index_v T n (set_index T n x m y p) m p = y.
328
329lemma get_8051_sfr_set_8051_sfr:
330 ∀T,cm,s,x,y. get_8051_sfr T cm (set_8051_sfr … s x y) x = y.
331 #T #cm * #A #B #C #D #E #F #G #H #I * #y whd in ⊢ (??(???%?)?);
332 whd in match get_8051_sfr; normalize nodelta @get_index_v_set_index
333qed.
334
335lemma program_counter_set_8051_sfr:
336 ∀T,cm,s,x,y. program_counter T cm (set_8051_sfr … s x y) = program_counter … s.
337 //
338qed.
339
340axiom program_counter_set_bit_addressable_sfr:
341  ∀m, cm, s, addr, v.
342   program_counter m cm (set_bit_addressable_sfr m cm s addr v) = program_counter m cm s.
343
344lemma program_counter_set_arg_8:
345  ∀m, cm, s, addr, v.
346   program_counter m cm (set_arg_8 m cm s addr v) = program_counter m cm s.
347  #m #cm #s #addr #byte
348  whd in match set_arg_8; normalize nodelta
349  cases daemon (*
350  whd in match set_arg_8'; normalize nodelta
351  cases addr #subaddressing_modein_proof
352  cases subaddressing_modein_proof
353  try (#addr normalize in addr; cases addr)
354  try (#ignore #addr normalize in addr; cases addr)
355  normalize nodelta try #_ try /demod/ try %
356  cases (vsplit bool 4 4 ?) #nu #nl normalize nodelta
357  cases (vsplit bool 1 3 ?) #ignore #three_bits normalize nodelta
358  cases (get_index_v bool 4 nu ? ?) normalize nodelta try /demod/ try % *)
359qed.
360
361(* XXX: this was compiling before! *)
362lemma program_counter_set_arg_1:
363  ∀m, cm, s, addr, v.
364   program_counter m cm (set_arg_1 m cm s addr v) = program_counter m cm s.
365  #m #cm #s #addr #v
366  whd in match set_arg_1; normalize nodelta
367  cases daemon (*
368  whd in match set_arg_1'; normalize nodelta
369  cases addr #subaddressing_modein_proof
370  cases subaddressing_modein_proof
371  try (#ignore #addr normalize in addr; cases addr)
372  try (#addr normalize in addr; cases addr)
373  normalize nodelta
374  cases (vsplit bool 4 4 ?) #nu #nl normalize nodelta try /demod/ try %
375  cases (vsplit bool 1 3 ?) #ignore #three_bits normalize nodelta
376  cases (get_index_v bool 4 nu ??) normalize nodelta
377  (* XXX: try /demod/ try % *)
378  cases daemon *)
379qed.
380
381lemma program_counter_set_arg_16:
382  ∀m, cm, s, addr, v.
383   program_counter m cm (set_arg_16 m cm s v addr) = program_counter m cm s.
384  #m #cm #s #addr #v
385  whd in match set_arg_16; normalize nodelta
386  whd in match set_arg_16'; normalize nodelta
387  cases addr #subaddressing_modein_proof
388  cases subaddressing_modein_proof
389  try (#ignore #addr normalize in addr; cases addr)
390  try (#addr normalize in addr; cases addr)
391  normalize nodelta
392  cases (vsplit bool 8 8 v) #bu #bl normalize nodelta /demod/ %
393qed.
394
395lemma program_counter_set_low_internal_ram:
396  ∀m, cm, s, v.
397   program_counter m cm (set_low_internal_ram m cm s v) = program_counter m cm s.
398  #m #cm #s #v
399  whd in match set_low_internal_ram; normalize nodelta %
400qed.
401
402lemma program_counter_set_high_internal_ram:
403  ∀m, cm, s, v.
404   program_counter m cm (set_high_internal_ram m cm s v) = program_counter m cm s.
405  #m #cm #s #v
406  whd in match set_high_internal_ram; normalize nodelta %
407qed.
408
409lemma program_counter_write_at_stack_pointer:
410  ∀m, cm, s, v.
411   program_counter m cm (write_at_stack_pointer m cm s v) = program_counter m cm s.
412  #m #cm #s #v
413  whd in match write_at_stack_pointer; normalize nodelta
414 cases (vsplit ????) #bit_one #seven_bits normalize nodelta
415 cases (head' bool ??) %
416qed.
417
418axiom get_arg_8_set_low_internal_ram:
419  ∀M,cm,s,x,b,z.
420    get_arg_8 M cm (set_low_internal_ram … s x) b z = get_arg_8 … s b z.
421
422lemma split_eq_status:
423 ∀T,cm.
424 ∀A1,A2,A3,A4,A5,A6,A7,A8,A9.
425 ∀B1,B2,B3,B4,B5,B6,B7,B8,B9.
426  A1=B1 → A2=B2 → A3=B3 → A4=B4 → A5=B5 → A6=B6 → A7=B7 → A8=B8 → A9=B9 →
427   mk_PreStatus T cm A1 A2 A3 A4 A5 A6 A7 A8 A9 =
428   mk_PreStatus T cm B1 B2 B3 B4 B5 B6 B7 B8 B9.
429 //
430qed.
Note: See TracBrowser for help on using the repository browser.