Changeset 1666 for src/ASM/StatusProofs.ma
 Timestamp:
 Jan 28, 2012, 1:42:15 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/StatusProofs.ma
r1606 r1666 1 1 include "ASM/Status.ma". 2 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 3 63 lemma get_register_set_program_counter: 4 ∀T, s,pc. get_register T(set_program_counter … s pc) = get_register … s.5 #T #s #pc %64 ∀T,cm,s,pc. get_register T cm (set_program_counter … s pc) = get_register … s. 65 // 6 66 qed. 7 67 8 68 lemma 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 %69 ∀T,cm,s,pc. get_8051_sfr T cm (set_program_counter … s pc) = get_8051_sfr … s. 70 // 11 71 qed. 12 72 13 73 lemma 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 %74 ∀T,cm,s,pc. get_bit_addressable_sfr T cm (set_program_counter … s pc) = get_bit_addressable_sfr … s. 75 // 16 76 qed. 17 77 18 78 lemma 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 %79 ∀T,cm,s,pc. low_internal_ram T cm (set_program_counter … s pc) = low_internal_ram … s. 80 // 21 81 qed. 22 82 23 83 example get_arg_8_set_program_counter: 24 84 ∀n.∀l:Vector addressing_mode_tag (S n). 25 ∀T, s,pc,b.∀arg:l.85 ∀T,cm,s,pc,b.∀arg:l. 26 86 ∀prf:is_in ? 27 87 [[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 % @⊥ @H88 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 30 90  cases arg in prf; *; normalize // 31 91  skip ] 32 92 qed. 33 93 94 (* 34 95 lemma set_bit_addressable_sfr_set_code_memory: 35 96 ∀T, U: Type[0]. … … 121 182 cases (get_index_v bool 4 nu' 0 ?) normalize nodelta 122 183 try % @set_bit_addressable_sfr_set_code_memory 123 qed. 184 qed. *) 124 185 125 186 example set_arg_8_set_program_counter: 126 187 ∀n:nat. 127 188 ∀l:Vector addressing_mode_tag (S n). 128 ∀T: Type[0]. 129 ∀ps: PreStatus ? .189 ∀T: Type[0]. ∀cm. 190 ∀ps: PreStatus ? cm. 130 191 ∀pc. 131 192 ∀val. … … 133 194 ∀prf:is_in ? 134 195 [[direct;indirect;registr;acc_a;acc_b;ext_indirect;ext_indirect_dptr]] b. 135 set_arg_8 ? (set_program_counter Tps pc) b val =136 set_program_counter T (set_arg_8? ps b val) pc.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. 137 198 [2,3: cases b in prf; *; normalize //] 138 #n #l #T # ps #pc #val * *;199 #n #l #T #cm #ps #pc #val * *; 139 200 #x try (#y #H) try #H whd in H; try cases H try % 140 201 whd in match set_arg_8; normalize nodelta … … 146 207 qed. 147 208 148 149 lemma get_arg_8_set_code_memory: 209 (*lemma get_arg_8_set_code_memory: 150 210 ∀T1,T2,s,code_mem,b,arg. 151 211 get_arg_8 T1 (set_code_memory T2 T1 s code_mem) b arg = get_arg_8 … s b arg. … … 158 218 set_flags … (set_code_memory … s code_mem) f1 f2 f3. 159 219 #T1 #T2 #s #f1 #f2 #f3 #code_mem % 160 qed. 220 qed.*) 161 221 162 222 lemma set_program_counter_set_flags: 163 ∀T1, s,f1,f2,f3,pc.164 set_program_counter T1 (set_flags T1s f1 f2 f3) pc =223 ∀T1,cm,s,f1,f2,f3,pc. 224 set_program_counter T1 cm (set_flags T1 cm s f1 f2 f3) pc = 165 225 set_flags … (set_program_counter … s pc) f1 f2 f3. 166 #T1 #s #f1 #f2 #f3 #pc %226 // 167 227 qed. 168 228 169 229 lemma program_counter_set_flags: 170 ∀T1, s,f1,f2,f3.171 program_counter T1 (set_flags T1s f1 f2 f3) = program_counter … s.172 #T1 #s #f1 #f2 #f3 %230 ∀T1,cm,s,f1,f2,f3. 231 program_counter T1 cm (set_flags T1 cm s f1 f2 f3) = program_counter … s. 232 // 173 233 qed. 174 234 175 235 lemma special_function_registers_8051_write_at_stack_pointer: 176 ∀T, s,x.177 special_function_registers_8051 T (write_at_stack_pointer Ts x)178 = special_function_registers_8051 T s.179 #T # s #x whd in ⊢ (??(??%)?);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 ⊢ (??(???%)?); 180 240 cases (split ????) #nu #nl normalize nodelta; 181 241 cases (get_index_v bool ????) % … … 183 243 184 244 lemma get_8051_sfr_write_at_stack_pointer: 185 ∀T, s,x,y. get_8051_sfr T (write_at_stack_pointer T s x) y = get_8051_sfr Ts y.186 #T # s #x #y whd in ⊢ (??%%); >special_function_registers_8051_write_at_stack_pointer @refl187 qed. 188 189 lemma code_memory_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: 190 250 ∀T,s,x. code_memory T (write_at_stack_pointer T s x) = code_memory T s. 191 251 #T #s #x whd in ⊢ (??(??%)?); 192 252 cases (split ????) #nu #nl normalize nodelta; 193 253 cases (get_index_v bool ????) % 194 qed. 254 qed.*) 195 255 196 256 lemma set_program_counter_set_low_internal_ram: 197 ∀T, s,x,y.198 set_program_counter T (set_low_internal_ram … s x) y =257 ∀T,cm,s,x,y. 258 set_program_counter T cm (set_low_internal_ram … s x) y = 199 259 set_low_internal_ram … (set_program_counter … s y) x. 200 260 // … … 202 262 203 263 lemma set_clock_set_low_internal_ram: 204 ∀T, s,x,y.205 set_clock T (set_low_internal_ram … s x) y =264 ∀T,cm,s,x,y. 265 set_clock T cm (set_low_internal_ram … s x) y = 206 266 set_low_internal_ram … (set_clock … s y) x. 207 267 // … … 209 269 210 270 lemma set_program_counter_set_high_internal_ram: 211 ∀T, s,x,y.212 set_program_counter T (set_high_internal_ram … s x) y =271 ∀T,cm,s,x,y. 272 set_program_counter T cm (set_high_internal_ram … s x) y = 213 273 set_high_internal_ram … (set_program_counter … s y) x. 214 274 // … … 216 276 217 277 lemma set_clock_set_high_internal_ram: 218 ∀T, s,x,y.219 set_clock T (set_high_internal_ram … s x) y =278 ∀T,cm,s,x,y. 279 set_clock T cm (set_high_internal_ram … s x) y = 220 280 set_high_internal_ram … (set_clock … s y) x. 221 281 // … … 223 283 224 284 lemma set_low_internal_ram_set_high_internal_ram: 225 ∀T, s,x,y.226 set_low_internal_ram T (set_high_internal_ram … s x) y =285 ∀T,cm,s,x,y. 286 set_low_internal_ram T cm (set_high_internal_ram … s x) y = 227 287 set_high_internal_ram … (set_low_internal_ram … s y) x. 228 288 // … … 230 290 231 291 lemma external_ram_write_at_stack_pointer: 232 ∀T, s,x. external_ram T (write_at_stack_pointer T s x) = external_ram Ts.233 #T # s #x whd in ⊢ (??(??%)?);292 ∀T,cm,s,x. external_ram T cm (write_at_stack_pointer T cm s x) = external_ram T cm s. 293 #T #cm #s #x whd in ⊢ (??(???%)?); 234 294 cases (split ????) #nu #nl normalize nodelta; 235 295 cases (get_index_v bool ????) % … … 237 297 238 298 lemma special_function_registers_8052_write_at_stack_pointer: 239 ∀T, s,x.240 special_function_registers_8052 T (write_at_stack_pointer Ts x)241 = special_function_registers_8052 T s.242 #T # s #x whd in ⊢ (??(??%)?);299 ∀T,cm,s,x. 300 special_function_registers_8052 T cm (write_at_stack_pointer T cm s x) 301 = special_function_registers_8052 T cm s. 302 #T #cm #s #x whd in ⊢ (??(???%)?); 243 303 cases (split ????) #nu #nl normalize nodelta; 244 304 cases (get_index_v bool ????) % … … 246 306 247 307 lemma p1_latch_write_at_stack_pointer: 248 ∀T, s,x. p1_latch T (write_at_stack_pointer T s x) = p1_latch Ts.249 #T # s #x whd in ⊢ (??(??%)?);308 ∀T,cm,s,x. p1_latch T cm (write_at_stack_pointer T cm s x) = p1_latch T cm s. 309 #T #cm #s #x whd in ⊢ (??(???%)?); 250 310 cases (split ????) #nu #nl normalize nodelta; 251 311 cases (get_index_v bool ????) % … … 253 313 254 314 lemma p3_latch_write_at_stack_pointer: 255 ∀T,s,x. p3_latch T (write_at_stack_pointer T s x) = p3_latch T s. 256 #T #s #x whd in ⊢ (??(??%)?); 257 cases (split ????) #nu #nl normalize nodelta; 258 cases (get_index_v bool ????) % 259 qed. 260 261 lemma clock_write_at_stack_pointer: 262 ∀T,s,x. clock T (write_at_stack_pointer T s x) = clock T s. 263 #T #s #x whd in ⊢ (??(??%)?); 315 ∀T,cm,s,x. p3_latch T cm (write_at_stack_pointer T cm s x) = p3_latch T cm s. 316 #T #cm #s #x whd in ⊢ (??(???%)?); 264 317 cases (split ????) #nu #nl normalize nodelta; 265 318 cases (get_index_v bool ????) % … … 270 323 271 324 lemma get_8051_sfr_set_8051_sfr: 272 ∀T, s,x,y. get_8051_sfr T (set_8051_sfr ?s x y) x = y.273 #T *; #A #B #C #D #E #F #G #H #I #J *; #y whd in ⊢ (??(??%?)?);325 ∀T,cm,s,x,y. get_8051_sfr T cm (set_8051_sfr … s x y) x = y. 326 #T #cm * #A #B #C #D #E #F #G #H #I * #y whd in ⊢ (??(???%?)?); 274 327 whd in match get_8051_sfr; normalize nodelta @get_index_v_set_index 275 328 qed. 276 329 277 330 lemma program_counter_set_8051_sfr: 278 ∀T, s,x,y. program_counter T (set_8051_sfr ? s x y) = program_counter ?s.331 ∀T,cm,s,x,y. program_counter T cm (set_8051_sfr … s x y) = program_counter … s. 279 332 // 280 333 qed. 281 334 282 335 axiom get_arg_8_set_low_internal_ram: 283 ∀M, s,x,b,z. get_arg_8 M (set_low_internal_ram ? s x) b z = get_arg_8 ?s b z.336 ∀M,cm,s,x,b,z. get_arg_8 M cm (set_low_internal_ram … s x) b z = get_arg_8 … s b z. 284 337 285 338 lemma split_eq_status: 286 ∀T .287 ∀A1,A2,A3,A4,A5,A6,A7,A8,A9 ,A10.288 ∀B1,B2,B3,B4,B5,B6,B7,B8,B9 ,B10.289 A1=B1 → A2=B2 → A3=B3 → A4=B4 → A5=B5 → A6=B6 → A7=B7 → A8=B8 → A9=B9 → A10=B10 →290 mk_PreStatus T A1 A2 A3 A4 A5 A6 A7 A8 A9 A10=291 mk_PreStatus T B1 B2 B3 B4 B5 B6 B7 B8 B9 B10.292 // 293 qed. 339 ∀T,cm. 340 ∀A1,A2,A3,A4,A5,A6,A7,A8,A9. 341 ∀B1,B2,B3,B4,B5,B6,B7,B8,B9. 342 A1=B1 → A2=B2 → A3=B3 → A4=B4 → A5=B5 → A6=B6 → A7=B7 → A8=B8 → A9=B9 → 343 mk_PreStatus T cm A1 A2 A3 A4 A5 A6 A7 A8 A9 = 344 mk_PreStatus T cm B1 B2 B3 B4 B5 B6 B7 B8 B9. 345 // 346 qed.
Note: See TracChangeset
for help on using the changeset viewer.