Changeset 2166


Ignore:
Timestamp:
Jul 8, 2012, 3:59:01 PM (5 years ago)
Author:
sacerdot
Message:
  1. less daemons
  2. more easily usable statement
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Test.ma

    r2165 r2166  
    486486qed.
    487487
    488 definition map_address_mode_using_internal_pseudo_address_map_ok ≝
    489  λM,sigma,cm.λs:PreStatus ? cm.λaddr,v,v'.
     488definition map_address_mode_using_internal_pseudo_address_map_ok1 ≝
     489 λM:internal_pseudo_address_map.λcm.λs:PreStatus ? cm.λaddr.
     490  match addr with
     491  [ INDIRECT i ⇒
     492     assoc_list_lookup ??
     493      (false:::bit_address_of_register pseudo_assembly_program cm s [[false; false; i]]) (eq_bv …) (\fst M) = None …
     494  | EXT_INDIRECT e ⇒
     495     assoc_list_lookup ??
     496      (false:::bit_address_of_register pseudo_assembly_program cm s [[false; false; e]]) (eq_bv …) (\fst M) = None …
     497  | _ ⇒ True ].
     498
     499definition map_address_mode_using_internal_pseudo_address_map_ok2 ≝
     500 λT,M,sigma,cm.λs:PreStatus T cm.λaddr,v.
    490501  match addr with
    491502  [ DIRECT d ⇒
     
    495506      map_address_Byte_using_internal_pseudo_address_map M sigma (true:::seven_bits) v
    496507     | false ⇒
    497       map_internal_ram_address_using_pseudo_address_map M sigma (false:::seven_bits) v ] = v'
     508      map_internal_ram_address_using_pseudo_address_map M sigma (false:::seven_bits) v ]
    498509  | INDIRECT i ⇒
    499      assoc_list_lookup ??
    500       (false:::bit_address_of_register pseudo_assembly_program cm s [[false; false; i]]) (eq_bv …) (\fst M) = None … ∧
    501510     let register ≝ get_register ?? s [[ false; false; i ]] in
    502      map_internal_ram_address_using_pseudo_address_map M sigma register v = v'
    503   | EXT_INDIRECT e ⇒
    504      assoc_list_lookup ??
    505       (false:::bit_address_of_register pseudo_assembly_program cm s [[false; false; e]]) (eq_bv …) (\fst M) = None … ∧
    506      v = v'
    507   | _ ⇒ v = v'].
     511     map_internal_ram_address_using_pseudo_address_map M sigma register v
     512  | ACC_A ⇒
     513     map_address_using_internal_pseudo_address_map M sigma SFR_ACC_A v
     514  | _ ⇒ v ].
    508515
    509516definition set_arg_8: ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. ∀addr: [[ direct ; indirect ; registr ;
     
    584591  ∀addr:[[ direct ; indirect ; registr ; acc_a ; acc_b ; ext_indirect ; ext_indirect_dptr ]].
    585592  ∀value. Σp: PreStatus ? cm. ∀M. ∀sigma. ∀policy. ∀value'.
    586    map_address_mode_using_internal_pseudo_address_map_ok … M sigma cm ps addr value value' →
     593   map_address_mode_using_internal_pseudo_address_map_ok1 M cm ps addr →
     594   map_address_mode_using_internal_pseudo_address_map_ok2 … M sigma cm ps addr value = value' →
    587595    set_arg_8 (BitVectorTrie Byte 16)
    588596      (code_memory_of_pseudo_assembly_program cm sigma policy)
     
    638646          match other in False with [ ]
    639647      ] (subaddressing_modein … a)) normalize nodelta
    640   #M #sigma #policy #v' whd in match map_address_mode_using_internal_pseudo_address_map_ok; normalize nodelta
     648  #M #sigma #policy #v'
     649  whd in match map_address_mode_using_internal_pseudo_address_map_ok1; normalize nodelta
     650  whd in match map_address_mode_using_internal_pseudo_address_map_ok2; normalize nodelta
    641651  [1,2:
    642652    <vsplit_refl normalize nodelta >p normalize nodelta
    643     [ >(vsplit_ok … vsplit_refl) @set_bit_addressable_sfr_status_of_pseudo_status
    644     | #v_ok >(insert_low_internal_ram_status_of_pseudo_status … v) // ]
    645   |3,4: * #EQ1 #EQ2 change with (get_register ????) in match register in p;
     653    [ >(vsplit_ok … vsplit_refl) #_ @set_bit_addressable_sfr_status_of_pseudo_status
     654    | #_ #v_ok >(insert_low_internal_ram_status_of_pseudo_status … v) // ]
     655  |3,4: #EQ1 #EQ2 change with (get_register ????) in match register in p;
    646656      >get_register_status_of_pseudo_status
    647657      whd in match map_internal_ram_address_using_pseudo_address_map; normalize nodelta
     
    650660      | >(insert_low_internal_ram_status_of_pseudo_status … v) // <EQ2
    651661        @eq_f2 try % <(vsplit_ok … (sym_eq … p)) <eq_cons_head_append >p1 % ]
    652   |5: * #EQ1 #EQ2 <EQ2 >get_register_status_of_pseudo_status
     662  |5: #EQ1 #EQ2 <EQ2 >get_register_status_of_pseudo_status
    653663      whd in match map_internal_ram_address_using_pseudo_address_map; normalize nodelta
    654664      >EQ1 normalize nodelta
    655665      >external_ram_status_of_pseudo_status @set_external_ram_status_of_pseudo_status
    656   |6: #EQ <EQ cases daemon (*CSC*)
    657   |7: #EQ <EQ @set_8051_sfr_status_of_pseudo_status cases daemon (*CSC*)
    658   |8: #EQ <EQ @set_8051_sfr_status_of_pseudo_status %
    659   |9: #EQ <EQ >get_8051_sfr_status_of_pseudo_status >get_8051_sfr_status_of_pseudo_status
     666  |6: #_ #EQ <EQ cases daemon (*CSC*)
     667  |7: #EQ1 #EQ2 <EQ2 /2 by set_8051_sfr_status_of_pseudo_status/
     668  |8: #_ #EQ <EQ @set_8051_sfr_status_of_pseudo_status %
     669  |9: #_ #EQ <EQ >get_8051_sfr_status_of_pseudo_status >get_8051_sfr_status_of_pseudo_status
    660670      >external_ram_status_of_pseudo_status @set_external_ram_status_of_pseudo_status ]
    661671qed.
Note: See TracChangeset for help on using the changeset viewer.