Changeset 1582


Ignore:
Timestamp:
Dec 1, 2011, 5:24:41 PM (8 years ago)
Author:
mulligan
Message:

more added to the proof of execute_1_preinstruction --- ~260 cases now reduced to less than 20

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Interpret.ma

    r1581 r1582  
    148148qed.
    149149
     150lemma 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 %
     156qed.
     157
    150158lemma set_8051_sfr_ignores_clock:
    151159  ∀M: Type[0].
     
    156164  #M #s #sfr #v %
    157165qed.
    158  
     166
     167lemma 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  ]
     190qed.
     191
     192lemma 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 %
     208qed.
     209
     210lemma 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 ] %
     220qed.
     221
    159222lemma clock_set_clock:
    160223  ∀M: Type[0].
     
    576639                  s
    577640        ]. (*15s*)
    578     try (destruct(other))
     641    try (cases(other))
    579642    try assumption (*20s*)
    580643    try % (*6s*)
     
    587650    try (/demod/ normalize nodelta >set_8051_sfr_ignores_clock /demod/ %)
    588651    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 %)
    590652    try (/demod/ normalize nodelta >set_8051_sfr_ignores_clock >set_8051_sfr_ignores_clock >clock_set_clock @commutative_plus)
    591653    try (/demod/ normalize nodelta >clock_set_clock @commutative_plus)
    592     [5: /demod/ normalize nodelta >clock_set_clock >set_arg_1_ignores_clock
    593 (* XXX: weird open goals here *)
    594 (*    [14: normalize nodelta <set_arg_8_ignores_clock /demod/ normalize nodelta
    595     try (normalize nodelta /demod/ %)
    596654    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 %)
    599662    cases daemon
    600663qed.
Note: See TracChangeset for help on using the changeset viewer.