[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 |
---|
[2272] | 29 | cases(vsplit … 1 7 ?) #bit_one #seven_bits normalize nodelta |
---|
| 30 | cases (head' bool ??) normalize nodelta // |
---|
[1666] | 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 | |
---|
[2285] | 73 | lemma get_8051_sfr_set_clock: |
---|
| 74 | ∀T,cm,s,pc. get_8051_sfr T cm (set_clock … s pc) = get_8051_sfr … s. |
---|
| 75 | // |
---|
| 76 | qed. |
---|
| 77 | |
---|
[1014] | 78 | lemma get_bit_addressable_sfr_set_program_counter: |
---|
[1666] | 79 | ∀T,cm,s,pc. get_bit_addressable_sfr T cm (set_program_counter … s pc) = get_bit_addressable_sfr … s. |
---|
| 80 | // |
---|
[1014] | 81 | qed. |
---|
| 82 | |
---|
| 83 | lemma low_internal_ram_set_program_counter: |
---|
[1666] | 84 | ∀T,cm,s,pc. low_internal_ram T cm (set_program_counter … s pc) = low_internal_ram … s. |
---|
| 85 | // |
---|
[1014] | 86 | qed. |
---|
| 87 | |
---|
[1962] | 88 | lemma get_arg_8_set_program_counter: |
---|
[1014] | 89 | ∀n.∀l:Vector addressing_mode_tag (S n). |
---|
[1666] | 90 | ∀T,cm,s,pc,b.∀arg:l. |
---|
[1014] | 91 | ∀prf:is_in ? |
---|
| 92 | [[direct;indirect;registr;acc_a;acc_b;data;acc_dptr;ext_indirect;ext_indirect_dptr]] arg. |
---|
[1666] | 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 |
---|
[1014] | 95 | | cases arg in prf; *; normalize // |
---|
| 96 | | skip ] |
---|
| 97 | qed. |
---|
| 98 | |
---|
[1666] | 99 | (* |
---|
[1014] | 100 | lemma 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 |
---|
[1519] | 109 | whd in ⊢ (??%?); |
---|
| 110 | whd in ⊢ (???(???%?)); |
---|
[1014] | 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 | ]]]]]]]]]]]]]]]]]]]]]]]]]] |
---|
| 165 | qed. |
---|
| 166 | |
---|
| 167 | example 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. |
---|
[1606] | 178 | set_arg_8 ? (set_code_memory T U ps code_mem) b val = |
---|
[1014] | 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 * *; |
---|
[1606] | 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 |
---|
[2032] | 185 | cases (vsplit bool 4 4 ?) #nu' #nl' normalize nodelta |
---|
| 186 | cases (vsplit bool 1 3 nu') #bit1' #ignore' normalize nodelta |
---|
[1014] | 187 | cases (get_index_v bool 4 nu' 0 ?) normalize nodelta |
---|
| 188 | try % @set_bit_addressable_sfr_set_code_memory |
---|
[1666] | 189 | qed. *) |
---|
[1014] | 190 | |
---|
[1962] | 191 | lemma set_arg_8_set_program_counter: |
---|
[1014] | 192 | ∀n:nat. |
---|
| 193 | ∀l:Vector addressing_mode_tag (S n). |
---|
[1666] | 194 | ∀T: Type[0]. ∀cm. |
---|
| 195 | ∀ps: PreStatus ? cm. |
---|
[1014] | 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. |
---|
[1666] | 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. |
---|
[1014] | 203 | [2,3: cases b in prf; *; normalize //] |
---|
[1666] | 204 | #n #l #T #cm #ps #pc #val * *; |
---|
[1606] | 205 | #x try (#y #H) try #H whd in H; try cases H try % |
---|
| 206 | whd in match set_arg_8; normalize nodelta |
---|
[2172] | 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) *) |
---|
[1014] | 210 | qed. |
---|
| 211 | |
---|
[1666] | 212 | (*lemma get_arg_8_set_code_memory: |
---|
[1014] | 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 % |
---|
| 216 | qed. |
---|
| 217 | |
---|
| 218 | lemma 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 % |
---|
[1666] | 223 | qed.*) |
---|
[1014] | 224 | |
---|
| 225 | lemma set_program_counter_set_flags: |
---|
[1666] | 226 | ∀T1,cm,s,f1,f2,f3,pc. |
---|
| 227 | set_program_counter T1 cm (set_flags T1 cm s f1 f2 f3) pc = |
---|
[1014] | 228 | set_flags … (set_program_counter … s pc) f1 f2 f3. |
---|
[1666] | 229 | // |
---|
[1014] | 230 | qed. |
---|
| 231 | |
---|
| 232 | lemma program_counter_set_flags: |
---|
[1666] | 233 | ∀T1,cm,s,f1,f2,f3. |
---|
| 234 | program_counter T1 cm (set_flags T1 cm s f1 f2 f3) = program_counter … s. |
---|
| 235 | // |
---|
[1014] | 236 | qed. |
---|
| 237 | |
---|
| 238 | lemma special_function_registers_8051_write_at_stack_pointer: |
---|
[1666] | 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 ⊢ (??(???%)?); |
---|
[2272] | 243 | cases (vsplit ????) #bit_one #seven_bits normalize nodelta |
---|
| 244 | cases (head' bool ??) normalize nodelta % |
---|
[1014] | 245 | qed. |
---|
| 246 | |
---|
| 247 | lemma get_8051_sfr_write_at_stack_pointer: |
---|
[1666] | 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 |
---|
[1014] | 250 | qed. |
---|
| 251 | |
---|
[1666] | 252 | (*lemma code_memory_write_at_stack_pointer: |
---|
[1014] | 253 | ∀T,s,x. code_memory T (write_at_stack_pointer T s x) = code_memory T s. |
---|
[1519] | 254 | #T #s #x whd in ⊢ (??(??%)?); |
---|
[2032] | 255 | cases (vsplit ????) #nu #nl normalize nodelta; |
---|
[1014] | 256 | cases (get_index_v bool ????) % |
---|
[1666] | 257 | qed.*) |
---|
[1014] | 258 | |
---|
| 259 | lemma set_program_counter_set_low_internal_ram: |
---|
[1666] | 260 | ∀T,cm,s,x,y. |
---|
| 261 | set_program_counter T cm (set_low_internal_ram … s x) y = |
---|
[1014] | 262 | set_low_internal_ram … (set_program_counter … s y) x. |
---|
| 263 | // |
---|
| 264 | qed. |
---|
| 265 | |
---|
| 266 | lemma set_clock_set_low_internal_ram: |
---|
[1666] | 267 | ∀T,cm,s,x,y. |
---|
| 268 | set_clock T cm (set_low_internal_ram … s x) y = |
---|
[1014] | 269 | set_low_internal_ram … (set_clock … s y) x. |
---|
| 270 | // |
---|
| 271 | qed. |
---|
| 272 | |
---|
| 273 | lemma set_program_counter_set_high_internal_ram: |
---|
[1666] | 274 | ∀T,cm,s,x,y. |
---|
| 275 | set_program_counter T cm (set_high_internal_ram … s x) y = |
---|
[1014] | 276 | set_high_internal_ram … (set_program_counter … s y) x. |
---|
| 277 | // |
---|
| 278 | qed. |
---|
| 279 | |
---|
| 280 | lemma set_clock_set_high_internal_ram: |
---|
[1666] | 281 | ∀T,cm,s,x,y. |
---|
| 282 | set_clock T cm (set_high_internal_ram … s x) y = |
---|
[1014] | 283 | set_high_internal_ram … (set_clock … s y) x. |
---|
| 284 | // |
---|
| 285 | qed. |
---|
| 286 | |
---|
[1958] | 287 | lemma 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 | // |
---|
| 292 | qed. |
---|
| 293 | |
---|
[1014] | 294 | lemma set_low_internal_ram_set_high_internal_ram: |
---|
[1666] | 295 | ∀T,cm,s,x,y. |
---|
| 296 | set_low_internal_ram T cm (set_high_internal_ram … s x) y = |
---|
[1014] | 297 | set_high_internal_ram … (set_low_internal_ram … s y) x. |
---|
| 298 | // |
---|
| 299 | qed. |
---|
| 300 | |
---|
| 301 | lemma external_ram_write_at_stack_pointer: |
---|
[1666] | 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 ⊢ (??(???%)?); |
---|
[2272] | 304 | cases (vsplit ????) #bit_one #seven_bits normalize nodelta |
---|
| 305 | cases (head' bool ??) % |
---|
[1014] | 306 | qed. |
---|
| 307 | |
---|
| 308 | lemma special_function_registers_8052_write_at_stack_pointer: |
---|
[1666] | 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 ⊢ (??(???%)?); |
---|
[2272] | 313 | cases (vsplit ????) #bit_one #seven_bits normalize nodelta |
---|
| 314 | cases (head' bool ??) % |
---|
[1014] | 315 | qed. |
---|
| 316 | |
---|
| 317 | lemma p1_latch_write_at_stack_pointer: |
---|
[1666] | 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 ⊢ (??(???%)?); |
---|
[2272] | 320 | cases (vsplit ????) #bit_one #seven_bits normalize nodelta |
---|
| 321 | cases (head' bool ??) % |
---|
[1014] | 322 | qed. |
---|
| 323 | |
---|
| 324 | lemma p3_latch_write_at_stack_pointer: |
---|
[1666] | 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 ⊢ (??(???%)?); |
---|
[2272] | 327 | cases (vsplit ????) #bit_one #seven_bits normalize nodelta |
---|
| 328 | cases (head' bool ??) % |
---|
[1014] | 329 | qed. |
---|
| 330 | |
---|
| 331 | axiom 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 | |
---|
| 334 | lemma get_8051_sfr_set_8051_sfr: |
---|
[1666] | 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 ⊢ (??(???%?)?); |
---|
[1014] | 337 | whd in match get_8051_sfr; normalize nodelta @get_index_v_set_index |
---|
| 338 | qed. |
---|
| 339 | |
---|
| 340 | lemma program_counter_set_8051_sfr: |
---|
[1666] | 341 | ∀T,cm,s,x,y. program_counter T cm (set_8051_sfr … s x y) = program_counter … s. |
---|
[1014] | 342 | // |
---|
| 343 | qed. |
---|
| 344 | |
---|
[1710] | 345 | axiom 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 | |
---|
| 349 | lemma 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 |
---|
[2172] | 354 | cases daemon (* |
---|
[1710] | 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 % |
---|
[2032] | 361 | cases (vsplit bool 4 4 ?) #nu #nl normalize nodelta |
---|
| 362 | cases (vsplit bool 1 3 ?) #ignore #three_bits normalize nodelta |
---|
[2172] | 363 | cases (get_index_v bool 4 nu ? ?) normalize nodelta try /demod/ try % *) |
---|
[1710] | 364 | qed. |
---|
| 365 | |
---|
[1958] | 366 | (* XXX: this was compiling before! *) |
---|
[1710] | 367 | lemma 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 |
---|
[2172] | 372 | cases daemon (* |
---|
[1710] | 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 |
---|
[2032] | 379 | cases (vsplit bool 4 4 ?) #nu #nl normalize nodelta try /demod/ try % |
---|
| 380 | cases (vsplit bool 1 3 ?) #ignore #three_bits normalize nodelta |
---|
[1959] | 381 | cases (get_index_v bool 4 nu ??) normalize nodelta |
---|
| 382 | (* XXX: try /demod/ try % *) |
---|
[2172] | 383 | cases daemon *) |
---|
[1710] | 384 | qed. |
---|
| 385 | |
---|
| 386 | lemma 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 |
---|
[2032] | 397 | cases (vsplit bool 8 8 v) #bu #bl normalize nodelta /demod/ % |
---|
[1710] | 398 | qed. |
---|
| 399 | |
---|
| 400 | lemma 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 % |
---|
| 405 | qed. |
---|
| 406 | |
---|
| 407 | lemma 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 % |
---|
| 412 | qed. |
---|
| 413 | |
---|
| 414 | lemma 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 |
---|
[2272] | 419 | cases (vsplit ????) #bit_one #seven_bits normalize nodelta |
---|
| 420 | cases (head' bool ??) % |
---|
[1710] | 421 | qed. |
---|
| 422 | |
---|
[1014] | 423 | axiom get_arg_8_set_low_internal_ram: |
---|
[1710] | 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. |
---|
[1014] | 426 | |
---|
| 427 | lemma split_eq_status: |
---|
[1666] | 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. |
---|
[1014] | 434 | // |
---|
[1666] | 435 | qed. |
---|