Changeset 2187 for src/ASM/Test.ma


Ignore:
Timestamp:
Jul 16, 2012, 5:19:06 PM (8 years ago)
Author:
mulligan
Message:

Work from today on the big proof.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Test.ma

    r2183 r2187  
    713713  ∀cm.
    714714  ∀ps.
    715   ∀addr:[[ direct ; indirect ; registr ; acc_a ; acc_b ; ext_indirect ; ext_indirect_dptr ]].
     715  ∀addr, addr':[[ direct ; indirect ; registr ; acc_a ; acc_b ; ext_indirect ; ext_indirect_dptr ]].
    716716  ∀value.
    717717  ∀M. ∀sigma. ∀policy. ∀s'. ∀value'.
     718   addr = addr' →
    718719   status_of_pseudo_status M cm ps sigma policy = s' →
    719720   map_address_mode_using_internal_pseudo_address_map_ok1 M cm ps sigma addr →
     
    722723      (code_memory_of_pseudo_assembly_program cm sigma policy)
    723724      s' addr value' =
    724     status_of_pseudo_status M cm (set_arg_8 … cm ps addr value) sigma policy.
    725   #cm #ps #addr #value
     725    status_of_pseudo_status M cm (set_arg_8 … cm ps addr' value) sigma policy.
     726  #cm #ps #addr #addr' #value
    726727  cases (set_arg_8_status_of_pseudo_status' cm ps addr value) #_ #relevant
     728  #M #sigma #policy #s' #value' #addr_refl <addr_refl
    727729  @relevant
    728730qed.
     
    11051107  ∀cm.
    11061108  ∀ps.
    1107   ∀addr: [[bit_addr; n_bit_addr; carry]].
     1109  ∀addr, addr': [[bit_addr; n_bit_addr; carry]].
    11081110  ∀l.
    11091111  ∀M. ∀sigma. ∀policy. ∀s'.
     1112    addr = addr' →
    11101113    status_of_pseudo_status M cm ps sigma policy = s' →
    11111114      map_bit_address_mode_using_internal_pseudo_address_map_get M cm ps sigma addr l →
    11121115      get_arg_1 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy)
    11131116      s' addr l =
    1114       (get_arg_1 … cm ps addr l).
    1115   #cm #ps #addr #l
     1117      (get_arg_1 … cm ps addr' l).
     1118  #cm #ps #addr #addr' #l
    11161119  cases (get_arg_1_status_of_pseudo_status' cm ps addr l) #_ #assm
     1120  #M #sigma #policy #s' #addr_refl <addr_refl
    11171121  @assm
    11181122qed.
Note: See TracChangeset for help on using the changeset viewer.