[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 | |
---|
| 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 | |
---|
[1962] | 83 | lemma get_arg_8_set_program_counter: |
---|
[1014] | 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 |
---|
[2032] | 180 | cases (vsplit bool 4 4 ?) #nu' #nl' normalize nodelta |
---|
| 181 | cases (vsplit bool 1 3 nu') #bit1' #ignore' normalize nodelta |
---|
[1014] | 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 | |
---|
[1962] | 186 | lemma set_arg_8_set_program_counter: |
---|
[1014] | 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 |
---|
[2172] | 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) *) |
---|
[1014] | 205 | qed. |
---|
| 206 | |
---|
[1666] | 207 | (*lemma get_arg_8_set_code_memory: |
---|
[1014] | 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 % |
---|
| 211 | qed. |
---|
| 212 | |
---|
| 213 | lemma 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 % |
---|
[1666] | 218 | qed.*) |
---|
[1014] | 219 | |
---|
| 220 | lemma set_program_counter_set_flags: |
---|
[1666] | 221 | ∀T1,cm,s,f1,f2,f3,pc. |
---|
| 222 | set_program_counter T1 cm (set_flags T1 cm s f1 f2 f3) pc = |
---|
[1014] | 223 | set_flags … (set_program_counter … s pc) f1 f2 f3. |
---|
[1666] | 224 | // |
---|
[1014] | 225 | qed. |
---|
| 226 | |
---|
| 227 | lemma program_counter_set_flags: |
---|
[1666] | 228 | ∀T1,cm,s,f1,f2,f3. |
---|
| 229 | program_counter T1 cm (set_flags T1 cm s f1 f2 f3) = program_counter … s. |
---|
| 230 | // |
---|
[1014] | 231 | qed. |
---|
| 232 | |
---|
| 233 | lemma special_function_registers_8051_write_at_stack_pointer: |
---|
[1666] | 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 ⊢ (??(???%)?); |
---|
[2272] | 238 | cases (vsplit ????) #bit_one #seven_bits normalize nodelta |
---|
| 239 | cases (head' bool ??) normalize nodelta % |
---|
[1014] | 240 | qed. |
---|
| 241 | |
---|
| 242 | lemma get_8051_sfr_write_at_stack_pointer: |
---|
[1666] | 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 |
---|
[1014] | 245 | qed. |
---|
| 246 | |
---|
[1666] | 247 | (*lemma code_memory_write_at_stack_pointer: |
---|
[1014] | 248 | ∀T,s,x. code_memory T (write_at_stack_pointer T s x) = code_memory T s. |
---|
[1519] | 249 | #T #s #x whd in ⊢ (??(??%)?); |
---|
[2032] | 250 | cases (vsplit ????) #nu #nl normalize nodelta; |
---|
[1014] | 251 | cases (get_index_v bool ????) % |
---|
[1666] | 252 | qed.*) |
---|
[1014] | 253 | |
---|
| 254 | lemma set_program_counter_set_low_internal_ram: |
---|
[1666] | 255 | ∀T,cm,s,x,y. |
---|
| 256 | set_program_counter T cm (set_low_internal_ram … s x) y = |
---|
[1014] | 257 | set_low_internal_ram … (set_program_counter … s y) x. |
---|
| 258 | // |
---|
| 259 | qed. |
---|
| 260 | |
---|
| 261 | lemma set_clock_set_low_internal_ram: |
---|
[1666] | 262 | ∀T,cm,s,x,y. |
---|
| 263 | set_clock T cm (set_low_internal_ram … s x) y = |
---|
[1014] | 264 | set_low_internal_ram … (set_clock … s y) x. |
---|
| 265 | // |
---|
| 266 | qed. |
---|
| 267 | |
---|
| 268 | lemma set_program_counter_set_high_internal_ram: |
---|
[1666] | 269 | ∀T,cm,s,x,y. |
---|
| 270 | set_program_counter T cm (set_high_internal_ram … s x) y = |
---|
[1014] | 271 | set_high_internal_ram … (set_program_counter … s y) x. |
---|
| 272 | // |
---|
| 273 | qed. |
---|
| 274 | |
---|
| 275 | lemma set_clock_set_high_internal_ram: |
---|
[1666] | 276 | ∀T,cm,s,x,y. |
---|
| 277 | set_clock T cm (set_high_internal_ram … s x) y = |
---|
[1014] | 278 | set_high_internal_ram … (set_clock … s y) x. |
---|
| 279 | // |
---|
| 280 | qed. |
---|
| 281 | |
---|
[1958] | 282 | lemma 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 | // |
---|
| 287 | qed. |
---|
| 288 | |
---|
[1014] | 289 | lemma set_low_internal_ram_set_high_internal_ram: |
---|
[1666] | 290 | ∀T,cm,s,x,y. |
---|
| 291 | set_low_internal_ram T cm (set_high_internal_ram … s x) y = |
---|
[1014] | 292 | set_high_internal_ram … (set_low_internal_ram … s y) x. |
---|
| 293 | // |
---|
| 294 | qed. |
---|
| 295 | |
---|
| 296 | lemma external_ram_write_at_stack_pointer: |
---|
[1666] | 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 ⊢ (??(???%)?); |
---|
[2272] | 299 | cases (vsplit ????) #bit_one #seven_bits normalize nodelta |
---|
| 300 | cases (head' bool ??) % |
---|
[1014] | 301 | qed. |
---|
| 302 | |
---|
| 303 | lemma special_function_registers_8052_write_at_stack_pointer: |
---|
[1666] | 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 ⊢ (??(???%)?); |
---|
[2272] | 308 | cases (vsplit ????) #bit_one #seven_bits normalize nodelta |
---|
| 309 | cases (head' bool ??) % |
---|
[1014] | 310 | qed. |
---|
| 311 | |
---|
| 312 | lemma p1_latch_write_at_stack_pointer: |
---|
[1666] | 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 ⊢ (??(???%)?); |
---|
[2272] | 315 | cases (vsplit ????) #bit_one #seven_bits normalize nodelta |
---|
| 316 | cases (head' bool ??) % |
---|
[1014] | 317 | qed. |
---|
| 318 | |
---|
| 319 | lemma p3_latch_write_at_stack_pointer: |
---|
[1666] | 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 ⊢ (??(???%)?); |
---|
[2272] | 322 | cases (vsplit ????) #bit_one #seven_bits normalize nodelta |
---|
| 323 | cases (head' bool ??) % |
---|
[1014] | 324 | qed. |
---|
| 325 | |
---|
| 326 | axiom 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 | |
---|
| 329 | lemma get_8051_sfr_set_8051_sfr: |
---|
[1666] | 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 ⊢ (??(???%?)?); |
---|
[1014] | 332 | whd in match get_8051_sfr; normalize nodelta @get_index_v_set_index |
---|
| 333 | qed. |
---|
| 334 | |
---|
| 335 | lemma program_counter_set_8051_sfr: |
---|
[1666] | 336 | ∀T,cm,s,x,y. program_counter T cm (set_8051_sfr … s x y) = program_counter … s. |
---|
[1014] | 337 | // |
---|
| 338 | qed. |
---|
| 339 | |
---|
[1710] | 340 | axiom 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 | |
---|
| 344 | lemma 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 |
---|
[2172] | 349 | cases daemon (* |
---|
[1710] | 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 % |
---|
[2032] | 356 | cases (vsplit bool 4 4 ?) #nu #nl normalize nodelta |
---|
| 357 | cases (vsplit bool 1 3 ?) #ignore #three_bits normalize nodelta |
---|
[2172] | 358 | cases (get_index_v bool 4 nu ? ?) normalize nodelta try /demod/ try % *) |
---|
[1710] | 359 | qed. |
---|
| 360 | |
---|
[1958] | 361 | (* XXX: this was compiling before! *) |
---|
[1710] | 362 | lemma 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 |
---|
[2172] | 367 | cases daemon (* |
---|
[1710] | 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 |
---|
[2032] | 374 | cases (vsplit bool 4 4 ?) #nu #nl normalize nodelta try /demod/ try % |
---|
| 375 | cases (vsplit bool 1 3 ?) #ignore #three_bits normalize nodelta |
---|
[1959] | 376 | cases (get_index_v bool 4 nu ??) normalize nodelta |
---|
| 377 | (* XXX: try /demod/ try % *) |
---|
[2172] | 378 | cases daemon *) |
---|
[1710] | 379 | qed. |
---|
| 380 | |
---|
| 381 | lemma 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 |
---|
[2032] | 392 | cases (vsplit bool 8 8 v) #bu #bl normalize nodelta /demod/ % |
---|
[1710] | 393 | qed. |
---|
| 394 | |
---|
| 395 | lemma 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 % |
---|
| 400 | qed. |
---|
| 401 | |
---|
| 402 | lemma 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 % |
---|
| 407 | qed. |
---|
| 408 | |
---|
| 409 | lemma 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 |
---|
[2272] | 414 | cases (vsplit ????) #bit_one #seven_bits normalize nodelta |
---|
| 415 | cases (head' bool ??) % |
---|
[1710] | 416 | qed. |
---|
| 417 | |
---|
[1014] | 418 | axiom get_arg_8_set_low_internal_ram: |
---|
[1710] | 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. |
---|
[1014] | 421 | |
---|
| 422 | lemma split_eq_status: |
---|
[1666] | 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. |
---|
[1014] | 429 | // |
---|
[1666] | 430 | qed. |
---|