[1014] | 1 | include "ASM/Status.ma". |
---|
| 2 | |
---|
[1666] | 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 | |
---|
[1014] | 63 | lemma get_register_set_program_counter: |
---|
[1666] | 64 | ∀T,cm,s,pc. get_register T cm (set_program_counter … s pc) = get_register … s. |
---|
| 65 | // |
---|
[1014] | 66 | qed. |
---|
| 67 | |
---|
| 68 | lemma get_8051_sfr_set_program_counter: |
---|
[1666] | 69 | ∀T,cm,s,pc. get_8051_sfr T cm (set_program_counter … s pc) = get_8051_sfr … s. |
---|
| 70 | // |
---|
[1014] | 71 | qed. |
---|
| 72 | |
---|
| 73 | lemma get_bit_addressable_sfr_set_program_counter: |
---|
[1666] | 74 | ∀T,cm,s,pc. get_bit_addressable_sfr T cm (set_program_counter … s pc) = get_bit_addressable_sfr … s. |
---|
| 75 | // |
---|
[1014] | 76 | qed. |
---|
| 77 | |
---|
| 78 | lemma low_internal_ram_set_program_counter: |
---|
[1666] | 79 | ∀T,cm,s,pc. low_internal_ram T cm (set_program_counter … s pc) = low_internal_ram … s. |
---|
| 80 | // |
---|
[1014] | 81 | qed. |
---|
| 82 | |
---|
| 83 | example get_arg_8_set_program_counter: |
---|
| 84 | ∀n.∀l:Vector addressing_mode_tag (S n). |
---|
[1666] | 85 | ∀T,cm,s,pc,b.∀arg:l. |
---|
[1014] | 86 | ∀prf:is_in ? |
---|
| 87 | [[direct;indirect;registr;acc_a;acc_b;data;acc_dptr;ext_indirect;ext_indirect_dptr]] arg. |
---|
[1666] | 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 |
---|
[1014] | 90 | | cases arg in prf; *; normalize // |
---|
| 91 | | skip ] |
---|
| 92 | qed. |
---|
| 93 | |
---|
[1666] | 94 | (* |
---|
[1014] | 95 | lemma 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 |
---|
[1519] | 104 | whd in ⊢ (??%?); |
---|
| 105 | whd in ⊢ (???(???%?)); |
---|
[1014] | 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 | ]]]]]]]]]]]]]]]]]]]]]]]]]] |
---|
| 160 | qed. |
---|
| 161 | |
---|
| 162 | example 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. |
---|
[1606] | 173 | set_arg_8 ? (set_code_memory T U ps code_mem) b val = |
---|
[1014] | 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 * *; |
---|
[1606] | 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 |
---|
[1014] | 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 |
---|
[1666] | 184 | qed. *) |
---|
[1014] | 185 | |
---|
| 186 | example set_arg_8_set_program_counter: |
---|
| 187 | ∀n:nat. |
---|
| 188 | ∀l:Vector addressing_mode_tag (S n). |
---|
[1666] | 189 | ∀T: Type[0]. ∀cm. |
---|
| 190 | ∀ps: PreStatus ? cm. |
---|
[1014] | 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. |
---|
[1666] | 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. |
---|
[1014] | 198 | [2,3: cases b in prf; *; normalize //] |
---|
[1666] | 199 | #n #l #T #cm #ps #pc #val * *; |
---|
[1606] | 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 |
---|
[1014] | 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)*) |
---|
| 207 | qed. |
---|
| 208 | |
---|
[1666] | 209 | (*lemma get_arg_8_set_code_memory: |
---|
[1014] | 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 % |
---|
| 213 | qed. |
---|
| 214 | |
---|
| 215 | lemma 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 % |
---|
[1666] | 220 | qed.*) |
---|
[1014] | 221 | |
---|
| 222 | lemma set_program_counter_set_flags: |
---|
[1666] | 223 | ∀T1,cm,s,f1,f2,f3,pc. |
---|
| 224 | set_program_counter T1 cm (set_flags T1 cm s f1 f2 f3) pc = |
---|
[1014] | 225 | set_flags … (set_program_counter … s pc) f1 f2 f3. |
---|
[1666] | 226 | // |
---|
[1014] | 227 | qed. |
---|
| 228 | |
---|
| 229 | lemma program_counter_set_flags: |
---|
[1666] | 230 | ∀T1,cm,s,f1,f2,f3. |
---|
| 231 | program_counter T1 cm (set_flags T1 cm s f1 f2 f3) = program_counter … s. |
---|
| 232 | // |
---|
[1014] | 233 | qed. |
---|
| 234 | |
---|
| 235 | lemma special_function_registers_8051_write_at_stack_pointer: |
---|
[1666] | 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 ⊢ (??(???%)?); |
---|
[1014] | 240 | cases (split ????) #nu #nl normalize nodelta; |
---|
| 241 | cases (get_index_v bool ????) % |
---|
| 242 | qed. |
---|
| 243 | |
---|
| 244 | lemma get_8051_sfr_write_at_stack_pointer: |
---|
[1666] | 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 |
---|
[1014] | 247 | qed. |
---|
| 248 | |
---|
[1666] | 249 | (*lemma code_memory_write_at_stack_pointer: |
---|
[1014] | 250 | ∀T,s,x. code_memory T (write_at_stack_pointer T s x) = code_memory T s. |
---|
[1519] | 251 | #T #s #x whd in ⊢ (??(??%)?); |
---|
[1014] | 252 | cases (split ????) #nu #nl normalize nodelta; |
---|
| 253 | cases (get_index_v bool ????) % |
---|
[1666] | 254 | qed.*) |
---|
[1014] | 255 | |
---|
| 256 | lemma set_program_counter_set_low_internal_ram: |
---|
[1666] | 257 | ∀T,cm,s,x,y. |
---|
| 258 | set_program_counter T cm (set_low_internal_ram … s x) y = |
---|
[1014] | 259 | set_low_internal_ram … (set_program_counter … s y) x. |
---|
| 260 | // |
---|
| 261 | qed. |
---|
| 262 | |
---|
| 263 | lemma set_clock_set_low_internal_ram: |
---|
[1666] | 264 | ∀T,cm,s,x,y. |
---|
| 265 | set_clock T cm (set_low_internal_ram … s x) y = |
---|
[1014] | 266 | set_low_internal_ram … (set_clock … s y) x. |
---|
| 267 | // |
---|
| 268 | qed. |
---|
| 269 | |
---|
| 270 | lemma set_program_counter_set_high_internal_ram: |
---|
[1666] | 271 | ∀T,cm,s,x,y. |
---|
| 272 | set_program_counter T cm (set_high_internal_ram … s x) y = |
---|
[1014] | 273 | set_high_internal_ram … (set_program_counter … s y) x. |
---|
| 274 | // |
---|
| 275 | qed. |
---|
| 276 | |
---|
| 277 | lemma set_clock_set_high_internal_ram: |
---|
[1666] | 278 | ∀T,cm,s,x,y. |
---|
| 279 | set_clock T cm (set_high_internal_ram … s x) y = |
---|
[1014] | 280 | set_high_internal_ram … (set_clock … s y) x. |
---|
| 281 | // |
---|
| 282 | qed. |
---|
| 283 | |
---|
| 284 | lemma set_low_internal_ram_set_high_internal_ram: |
---|
[1666] | 285 | ∀T,cm,s,x,y. |
---|
| 286 | set_low_internal_ram T cm (set_high_internal_ram … s x) y = |
---|
[1014] | 287 | set_high_internal_ram … (set_low_internal_ram … s y) x. |
---|
| 288 | // |
---|
| 289 | qed. |
---|
| 290 | |
---|
| 291 | lemma external_ram_write_at_stack_pointer: |
---|
[1666] | 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 ⊢ (??(???%)?); |
---|
[1014] | 294 | cases (split ????) #nu #nl normalize nodelta; |
---|
| 295 | cases (get_index_v bool ????) % |
---|
| 296 | qed. |
---|
| 297 | |
---|
| 298 | lemma special_function_registers_8052_write_at_stack_pointer: |
---|
[1666] | 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 ⊢ (??(???%)?); |
---|
[1014] | 303 | cases (split ????) #nu #nl normalize nodelta; |
---|
| 304 | cases (get_index_v bool ????) % |
---|
| 305 | qed. |
---|
| 306 | |
---|
| 307 | lemma p1_latch_write_at_stack_pointer: |
---|
[1666] | 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 ⊢ (??(???%)?); |
---|
[1014] | 310 | cases (split ????) #nu #nl normalize nodelta; |
---|
| 311 | cases (get_index_v bool ????) % |
---|
| 312 | qed. |
---|
| 313 | |
---|
| 314 | lemma p3_latch_write_at_stack_pointer: |
---|
[1666] | 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 ⊢ (??(???%)?); |
---|
[1014] | 317 | cases (split ????) #nu #nl normalize nodelta; |
---|
| 318 | cases (get_index_v bool ????) % |
---|
| 319 | qed. |
---|
| 320 | |
---|
| 321 | axiom get_index_v_set_index: |
---|
| 322 | ∀T,n,x,m,p,y. get_index_v T n (set_index T n x m y p) m p = y. |
---|
| 323 | |
---|
| 324 | lemma get_8051_sfr_set_8051_sfr: |
---|
[1666] | 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 ⊢ (??(???%?)?); |
---|
[1014] | 327 | whd in match get_8051_sfr; normalize nodelta @get_index_v_set_index |
---|
| 328 | qed. |
---|
| 329 | |
---|
| 330 | lemma program_counter_set_8051_sfr: |
---|
[1666] | 331 | ∀T,cm,s,x,y. program_counter T cm (set_8051_sfr … s x y) = program_counter … s. |
---|
[1014] | 332 | // |
---|
| 333 | qed. |
---|
| 334 | |
---|
| 335 | axiom get_arg_8_set_low_internal_ram: |
---|
[1666] | 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. |
---|
[1014] | 337 | |
---|
| 338 | lemma split_eq_status: |
---|
[1666] | 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. |
---|
[1014] | 345 | // |
---|
[1666] | 346 | qed. |
---|