Changeset 2274 for src/ASM/Test.ma


Ignore:
Timestamp:
Jul 30, 2012, 1:14:40 AM (8 years ago)
Author:
sacerdot
Message:

Dead code commented out and code out of place moved to Test.ma.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Test.ma

    r2273 r2274  
    18731873qed.
    18741874
     1875lemma special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051:
     1876  ∀M: internal_pseudo_address_map.
     1877  ∀cm: pseudo_assembly_program.
     1878  ∀ps.
     1879  ∀sigma: Word → Word.
     1880  ∀policy: Word → bool.
     1881  ∀sfr.
     1882  ∀result: Byte.
     1883    eqb (sfr_8051_index sfr) (sfr_8051_index SFR_ACC_A) = false →
     1884      special_function_registers_8051 (BitVectorTrie Byte 16)
     1885        (code_memory_of_pseudo_assembly_program cm sigma policy)
     1886        (set_8051_sfr (BitVectorTrie Byte 16)
     1887        (code_memory_of_pseudo_assembly_program cm sigma policy)
     1888        (status_of_pseudo_status M cm ps sigma policy) sfr result) =
     1889      sfr_8051_of_pseudo_sfr_8051 M
     1890        (special_function_registers_8051 pseudo_assembly_program cm
     1891        (set_8051_sfr pseudo_assembly_program cm ps sfr result)) sigma.
     1892  ** #low #high * [2: * #upper_lower #addr] #cm #ps #sigma #policy #sfr #result #sfr_neq_assm
     1893  whd in match (set_8051_sfr ?????);
     1894  whd in match (special_function_registers_8051 ???);
     1895  whd in match (sfr_8051_of_pseudo_sfr_8051 ???); normalize nodelta try %
     1896  cases upper_lower normalize nodelta whd in match (set_8051_sfr ?????);
     1897  >get_index_v_set_index_miss [2,4: @eqb_false_to_not_eq assumption]
     1898  @vsplit_elim #h #l #h_l_refl normalize nodelta
     1899  @set_index_set_index_commutation @eqb_false_to_not_eq assumption
     1900qed.
     1901
    18751902(*
    18761903lemma addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_1:
Note: See TracChangeset for help on using the changeset viewer.