Changeset 1582
 Timestamp:
 Dec 1, 2011, 5:24:41 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Interpret.ma
r1581 r1582 148 148 qed. 149 149 150 lemma set_high_internal_ram_ignores_clock: 151 ∀m: Type[0]. 152 ∀s: PreStatus m. 153 ∀ram: BitVectorTrie Byte 7. 154 clock … (set_high_internal_ram … s ram) = clock … s. 155 #m #s #ram % 156 qed. 157 150 158 lemma set_8051_sfr_ignores_clock: 151 159 ∀M: Type[0]. … … 156 164 #M #s #sfr #v % 157 165 qed. 158 166 167 lemma set_arg_1_ignores_clock: 168 ∀m: Type[0]. 169 ∀s: PreStatus m. 170 ∀addr: [[bit_addr; carry]]. 171 ∀bit: Bit. 172 clock … (set_arg_1 m s addr bit) = clock … s. 173 #m #s #addr #bit 174 whd in match set_arg_1; normalize nodelta 175 cases addr #subaddressing_mode 176 cases subaddressing_mode 177 try #assm1 try #assm2 178 try (normalize in assm2; cases assm2) 179 try (normalize in assm1; cases assm1) 180 normalize nodelta 181 cases (split bool 4 4 (get_8051_sfr m s SFR_PSW)) 182 #nu #nl normalize nodelta 183 [ @set_8051_sfr_ignores_clock 184  cases(split … 1 3 nu) 185 #ignore #three_bits normalize nodelta 186 cases(get_index_v … 4 nu 0 ?) 187 normalize nodelta 188 [ <set_bit_addressable_sfr_ignores_clock  >set_low_internal_ram_ignores_clock ] % 189 ] 190 qed. 191 192 lemma set_arg_16_ignores_clock: 193 ∀m: Type[0]. 194 ∀s: PreStatus m. 195 ∀w: Word. 196 ∀addr: [[dptr]]. 197 clock … (set_arg_16 m s w addr) = clock … s. 198 #m #s #w #addr 199 whd in match set_arg_16; normalize nodelta 200 cases addr #subaddressing_modein 201 cases subaddressing_modein 202 try #assm1 try #assm2 203 try (normalize in assm2; cases assm2) 204 try (normalize in assm1; cases assm1) 205 normalize nodelta 206 cases (split … 8 8 w) #bu #bl normalize nodelta 207 >set_8051_sfr_ignores_clock >set_8051_sfr_ignores_clock % 208 qed. 209 210 lemma write_at_stack_pointer_ignores_clock: 211 ∀m: Type[0]. 212 ∀s: PreStatus m. 213 ∀v: Byte. 214 clock … (write_at_stack_pointer m s v) = clock … s. 215 #m #s #v 216 whd in match write_at_stack_pointer; normalize nodelta 217 cases(split … 4 4 ?) #nu #nl normalize nodelta 218 cases(get_index_v … 4 nu 0 ?) normalize nodelta 219 [ >set_low_internal_ram_ignores_clock  >set_high_internal_ram_ignores_clock ] % 220 qed. 221 159 222 lemma clock_set_clock: 160 223 ∀M: Type[0]. … … 576 639 s 577 640 ]. (*15s*) 578 try ( destruct(other))641 try (cases(other)) 579 642 try assumption (*20s*) 580 643 try % (*6s*) … … 587 650 try (/demod/ normalize nodelta >set_8051_sfr_ignores_clock /demod/ %) 588 651 try (normalize nodelta <set_flags_ignores_clock /demod/ %) 589 try (/demod/ normalize nodelta >set_8051_sfr_ignores_clock >set_8051_sfr_ignores_clock >clock_set_clock %)590 652 try (/demod/ normalize nodelta >set_8051_sfr_ignores_clock >set_8051_sfr_ignores_clock >clock_set_clock @commutative_plus) 591 653 try (/demod/ normalize nodelta >clock_set_clock @commutative_plus) 592 [5: /demod/ normalize nodelta >clock_set_clock >set_arg_1_ignores_clock593 (* XXX: weird open goals here *)594 (* [14: normalize nodelta <set_arg_8_ignores_clock /demod/ normalize nodelta595 try (normalize nodelta /demod/ %)596 654 try (/demod/ normalize nodelta >clock_set_clock >set_arg_1_ignores_clock @commutative_plus) 597 598 try (normalize nodelta >set_8051_sfr_ignores_clock >set_8051_sfr_ignores_clock >clock_set_clock %)*) 655 try (/demod/ normalize nodelta >clock_set_clock <set_arg_8_ignores_clock @commutative_plus) 656 try (/demod/ normalize nodelta >set_arg_1_ignores_clock >clock_set_clock @commutative_plus) 657 try (normalize nodelta >clock_set_clock >set_arg_1_ignores_clock >clock_set_clock %) 658 try (normalize nodelta <set_arg_8_ignores_clock >set_8051_sfr_ignores_clock >clock_set_clock %) 659 try (normalize nodelta >set_arg_1_ignores_clock >clock_set_clock %) 660 try (normalize nodelta >clock_set_clock >set_arg_16_ignores_clock >clock_set_clock %) 661 try (normalize nodelta >set_arg_16_ignores_clock >clock_set_clock %) 599 662 cases daemon 600 663 qed.
Note: See TracChangeset
for help on using the changeset viewer.