source: src/ASM/StatusProofs.ma @ 1600

Last change on this file since 1600 was 1530, checked in by campbell, 9 years ago

Update due to Russell changes.
File size: 9.2 KB
Line 
1include "ASM/Status.ma".
2
3lemma get_register_set_program_counter:
4 ∀T,s,pc. get_register T (set_program_counter … s pc) = get_register … s.
5 #T #s #pc %
6qed.
7
8lemma get_8051_sfr_set_program_counter:
9 ∀T,s,pc. get_8051_sfr T (set_program_counter … s pc) = get_8051_sfr … s.
10 #T #s #pc %
11qed.
12
13lemma get_bit_addressable_sfr_set_program_counter:
14 ∀T,s,pc. get_bit_addressable_sfr T (set_program_counter … s pc) = get_bit_addressable_sfr … s.
15 #T #s #pc %
16qed.
17
18lemma low_internal_ram_set_program_counter:
19 ∀T,s,pc. low_internal_ram T (set_program_counter … s pc) = low_internal_ram … s.
20 #T #s #pc %
21qed.
22
23example get_arg_8_set_program_counter:
24 ∀n.∀l:Vector addressing_mode_tag (S n).
25  ∀T,s,pc,b.∀arg:l.
26   ∀prf:is_in ?
27    [[direct;indirect;registr;acc_a;acc_b;data;acc_dptr;ext_indirect;ext_indirect_dptr]] arg.
28   get_arg_8 T (set_program_counter … s pc) b arg = get_arg_8 … s b arg.
29 [ #n #l #T #s #pc #b * *; #X try (#Y #H) try #H try % @⊥ @H
30 | cases arg in prf; *; normalize //
31 | skip ]
32qed.
33
34lemma set_bit_addressable_sfr_set_code_memory:
35  ∀T, U: Type[0].
36  ∀ps: PreStatus ?.
37  ∀code_mem.
38  ∀x.
39  ∀val.
40  set_bit_addressable_sfr ? (set_code_memory T U ps code_mem) x val =
41  set_code_memory T U (set_bit_addressable_sfr ? ps x val) code_mem.
42  #T #U #ps #code_mem #x #val
43  whd in ⊢ (??%?);
44  whd in ⊢ (???(???%?));
45  cases (eqb ? 128) [ normalize nodelta cases not_implemented
46  | normalize nodelta
47  cases (eqb (nat_of_bitvector 8 x) ?) [ normalize nodelta cases not_implemented
48  | normalize nodelta
49  cases (eqb (nat_of_bitvector 8 x) ?) [ normalize nodelta cases not_implemented
50  | normalize nodelta
51  cases (eqb ? 176) [ normalize nodelta %
52  | normalize nodelta
53  cases (eqb ? 153) [ normalize nodelta %
54  | normalize nodelta
55  cases (eqb ? 138) [ normalize nodelta %
56  | normalize nodelta
57  cases (eqb ? 139) [ normalize nodelta %
58  | normalize nodelta
59  cases (eqb ? 140) [ normalize nodelta %
60  | normalize nodelta
61  cases (eqb ? 141) [ normalize nodelta %
62  | normalize nodelta
63  cases (eqb ? 200) [ normalize nodelta %
64  | normalize nodelta
65  cases (eqb ? 202) [ normalize nodelta %
66  | normalize nodelta
67  cases (eqb ? 203) [ normalize nodelta %
68  | normalize nodelta
69  cases (eqb ? 204) [ normalize nodelta %
70  | normalize nodelta
71  cases (eqb ? 205) [ normalize nodelta %
72  | normalize nodelta
73  cases (eqb ? 135) [ normalize nodelta %
74  | normalize nodelta
75  cases (eqb ? 136) [ normalize nodelta %
76  | normalize nodelta
77  cases (eqb ? 137) [ normalize nodelta %
78  | normalize nodelta
79  cases (eqb ? 152) [ normalize nodelta %
80  | normalize nodelta
81  cases (eqb ? 168) [ normalize nodelta %
82  | normalize nodelta
83  cases (eqb ? 184) [ normalize nodelta %
84  | normalize nodelta
85  cases (eqb ? 129) [ normalize nodelta %
86  | normalize nodelta
87  cases (eqb ? 130) [ normalize nodelta %
88  | normalize nodelta
89  cases (eqb ? 131) [ normalize nodelta %
90  | normalize nodelta
91  cases (eqb ? 208) [ normalize nodelta %
92  | normalize nodelta
93  cases (eqb ? 224) [ normalize nodelta %
94  | normalize nodelta
95  cases (eqb ? 240) [ normalize nodelta %
96  | normalize nodelta
97    cases not_implemented
98  ]]]]]]]]]]]]]]]]]]]]]]]]]]
99qed.
100
101example set_arg_8_set_code_memory:
102  ∀n:nat.
103  ∀l:Vector addressing_mode_tag (S n).
104    ∀T: Type[0].
105    ∀U: Type[0].
106    ∀ps: PreStatus ?.
107    ∀code_mem.
108    ∀val.
109    ∀b: l.
110    ∀prf:is_in ?
111     [[direct;indirect;registr;acc_a;acc_b;ext_indirect;ext_indirect_dptr]] b.
112  eject … (set_arg_8 ? (set_code_memory T U ps code_mem) b val) =
113  set_code_memory T U (set_arg_8 ? ps b val) code_mem.
114  [2,3: cases b in prf; *; normalize //]
115  #n #l #T #U #ps #code_mem #val * *;
116  #x try (#y #H) try #H whd in H; try cases H
117  whd in ⊢ (??(???(%))?); whd in ⊢ (???(???(???(%))?)); try %
118  cases (split bool 4 4 ?) #nu' #nl' normalize nodelta
119  cases (split bool 1 3 nu') #bit1' #ignore' normalize nodelta
120  cases (get_index_v bool 4 nu' 0 ?) normalize nodelta
121  try % @set_bit_addressable_sfr_set_code_memory
122qed.
123
124example set_arg_8_set_program_counter:
125  ∀n:nat.
126  ∀l:Vector addressing_mode_tag (S n).
127    ∀T: Type[0].
128    ∀ps: PreStatus ?.
129    ∀pc.
130    ∀val.
131    ∀b: l.
132    ∀prf:is_in ?
133     [[direct;indirect;registr;acc_a;acc_b;ext_indirect;ext_indirect_dptr]] b.
134  eject … (set_arg_8 ? (set_program_counter T ps pc) b val) =
135  set_program_counter T (set_arg_8 ? ps b val) pc.
136  [2,3: cases b in prf; *; normalize //]
137  #n #l #T #ps #pc #val * *;
138  #x try (#y #H) try #H whd in H; try cases H
139  whd in ⊢ (??(???(%))?); whd in ⊢ (???(??(%)?)); try %
140  cases (split bool 4 4 ?) #nu' #nl' normalize nodelta
141  cases (split bool 1 3 nu') #bit1' #ignore' normalize nodelta
142  cases (get_index_v bool 4 nu' 0 ?) normalize nodelta
143  try % cases daemon (*@(set_bit_addressable_sfr_set_program_counter)*)
144qed.
145 
146
147lemma get_arg_8_set_code_memory:
148 ∀T1,T2,s,code_mem,b,arg.
149   get_arg_8 T1 (set_code_memory T2 T1 s code_mem) b arg = get_arg_8 … s b arg.
150 #T1 #T2 #s #code_mem #b #arg %
151qed.
152
153lemma set_code_memory_set_flags:
154 ∀T1,T2,s,f1,f2,f3,code_mem.
155  set_code_memory T1 T2 (set_flags T1 s f1 f2 f3) code_mem =
156   set_flags … (set_code_memory … s code_mem) f1 f2 f3.
157 #T1 #T2 #s #f1 #f2 #f3 #code_mem %
158qed.
159
160lemma set_program_counter_set_flags:
161 ∀T1,s,f1,f2,f3,pc.
162  set_program_counter T1 (set_flags T1 s f1 f2 f3) pc =
163   set_flags … (set_program_counter … s pc) f1 f2 f3.
164 #T1 #s #f1 #f2 #f3 #pc  %
165qed.
166
167lemma program_counter_set_flags:
168 ∀T1,s,f1,f2,f3.
169  program_counter T1 (set_flags T1 s f1 f2 f3) = program_counter … s.
170 #T1 #s #f1 #f2 #f3 %
171qed.
172
173lemma special_function_registers_8051_write_at_stack_pointer:
174 ∀T,s,x.
175    special_function_registers_8051 T (write_at_stack_pointer T s x)
176  = special_function_registers_8051 T s.
177 #T #s #x whd in ⊢ (??(??%)?);
178 cases (split ????) #nu #nl normalize nodelta;
179 cases (get_index_v bool ????) %
180qed.
181
182lemma get_8051_sfr_write_at_stack_pointer:
183 ∀T,s,x,y. get_8051_sfr T (write_at_stack_pointer T s x) y = get_8051_sfr T s y.
184 #T #s #x #y whd in ⊢ (??%%); >special_function_registers_8051_write_at_stack_pointer @refl
185qed.
186
187lemma code_memory_write_at_stack_pointer:
188 ∀T,s,x. code_memory T (write_at_stack_pointer T s x) = code_memory T s.
189 #T #s #x whd in ⊢ (??(??%)?);
190 cases (split ????) #nu #nl normalize nodelta;
191 cases (get_index_v bool ????) %
192qed.
193
194lemma set_program_counter_set_low_internal_ram:
195 ∀T,s,x,y.
196  set_program_counter T (set_low_internal_ram … s x) y =
197   set_low_internal_ram … (set_program_counter … s y) x.
198 //
199qed.
200
201lemma set_clock_set_low_internal_ram:
202 ∀T,s,x,y.
203  set_clock T (set_low_internal_ram … s x) y =
204   set_low_internal_ram … (set_clock … s y) x.
205 //
206qed.
207
208lemma set_program_counter_set_high_internal_ram:
209 ∀T,s,x,y.
210  set_program_counter T (set_high_internal_ram … s x) y =
211   set_high_internal_ram … (set_program_counter … s y) x.
212 //
213qed.
214
215lemma set_clock_set_high_internal_ram:
216 ∀T,s,x,y.
217  set_clock T (set_high_internal_ram … s x) y =
218   set_high_internal_ram … (set_clock … s y) x.
219 //
220qed.
221
222lemma set_low_internal_ram_set_high_internal_ram:
223 ∀T,s,x,y.
224  set_low_internal_ram T (set_high_internal_ram … s x) y =
225   set_high_internal_ram … (set_low_internal_ram … s y) x.
226 //
227qed.
228
229lemma external_ram_write_at_stack_pointer:
230 ∀T,s,x. external_ram T (write_at_stack_pointer T s x) = external_ram T s.
231 #T #s #x whd in ⊢ (??(??%)?);
232 cases (split ????) #nu #nl normalize nodelta;
233 cases (get_index_v bool ????) %
234qed.
235
236lemma special_function_registers_8052_write_at_stack_pointer:
237 ∀T,s,x.
238    special_function_registers_8052 T (write_at_stack_pointer T s x)
239  = special_function_registers_8052 T s.
240 #T #s #x whd in ⊢ (??(??%)?);
241 cases (split ????) #nu #nl normalize nodelta;
242 cases (get_index_v bool ????) %
243qed.
244
245lemma p1_latch_write_at_stack_pointer:
246 ∀T,s,x. p1_latch T (write_at_stack_pointer T s x) = p1_latch T s.
247 #T #s #x whd in ⊢ (??(??%)?);
248 cases (split ????) #nu #nl normalize nodelta;
249 cases (get_index_v bool ????) %
250qed.
251
252lemma p3_latch_write_at_stack_pointer:
253 ∀T,s,x. p3_latch T (write_at_stack_pointer T s x) = p3_latch T s.
254 #T #s #x whd in ⊢ (??(??%)?);
255 cases (split ????) #nu #nl normalize nodelta;
256 cases (get_index_v bool ????) %
257qed.
258
259lemma clock_write_at_stack_pointer:
260 ∀T,s,x. clock T (write_at_stack_pointer T s x) = clock T s.
261 #T #s #x whd in ⊢ (??(??%)?);
262 cases (split ????) #nu #nl normalize nodelta;
263 cases (get_index_v bool ????) %
264qed.
265
266axiom get_index_v_set_index:
267 ∀T,n,x,m,p,y. get_index_v T n (set_index T n x m y p) m p = y.
268
269lemma get_8051_sfr_set_8051_sfr:
270 ∀T,s,x,y. get_8051_sfr T (set_8051_sfr ? s x y) x = y.
271 #T *; #A #B #C #D #E #F #G #H #I #J *; #y whd in ⊢ (??(??%?)?);
272 whd in match get_8051_sfr; normalize nodelta @get_index_v_set_index
273qed.
274
275lemma program_counter_set_8051_sfr:
276 ∀T,s,x,y. program_counter T (set_8051_sfr ? s x y) = program_counter ? s.
277 //
278qed.
279
280axiom get_arg_8_set_low_internal_ram:
281 ∀M,s,x,b,z. get_arg_8 M (set_low_internal_ram ? s x) b z = get_arg_8 ? s b z.
282
283lemma split_eq_status:
284 ∀T.
285 ∀A1,A2,A3,A4,A5,A6,A7,A8,A9,A10.
286 ∀B1,B2,B3,B4,B5,B6,B7,B8,B9,B10.
287  A1=B1 → A2=B2 → A3=B3 → A4=B4 → A5=B5 → A6=B6 → A7=B7 → A8=B8 → A9=B9 → A10=B10 →
288   mk_PreStatus T A1 A2 A3 A4 A5 A6 A7 A8 A9 A10 =
289   mk_PreStatus T B1 B2 B3 B4 B5 B6 B7 B8 B9 B10.
290 //
291qed.
Note: See TracBrowser for help on using the repository browser.