Changeset 2274


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

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

Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/StatusProofsSplit.ma

    r2272 r2274  
    603603qed.
    604604
    605 lemma special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051:
    606   ∀M: internal_pseudo_address_map.
    607   ∀cm: pseudo_assembly_program.
    608   ∀ps.
    609   ∀sigma: Word → Word.
    610   ∀policy: Word → bool.
    611   ∀sfr.
    612   ∀result: Byte.
    613     eqb (sfr_8051_index sfr) (sfr_8051_index SFR_ACC_A) = false →
    614       special_function_registers_8051 (BitVectorTrie Byte 16)
    615         (code_memory_of_pseudo_assembly_program cm sigma policy)
    616         (set_8051_sfr (BitVectorTrie Byte 16)
    617         (code_memory_of_pseudo_assembly_program cm sigma policy)
    618         (status_of_pseudo_status M cm ps sigma policy) sfr result) =
    619       sfr_8051_of_pseudo_sfr_8051 M
    620         (special_function_registers_8051 pseudo_assembly_program cm
    621         (set_8051_sfr pseudo_assembly_program cm ps sfr result)) sigma.
    622   #M #cm #ps #sigma #policy #sfr #result #sfr_neq_assm
    623   whd in match (set_8051_sfr ?????);
    624   cases M * #low #high * try % * *
    625   whd in match (special_function_registers_8051 ???);
    626   whd in match (sfr_8051_of_pseudo_sfr_8051 ???); normalize nodelta
    627   @pair_elim #high #low #high_low_refl normalize nodelta
    628   cases (eq_upper_lower ??) normalize nodelta
    629   whd in match (set_8051_sfr ?????);
    630   @set_index_set_index_commutation @nmk #relevant
    631   @(absurd ? relevant (eqb_false_to_not_eq ?? sfr_neq_assm))
    632 qed.
    633 
     605(*CSC: dead and unfinished code
    634606lemma special_function_registers_8051_set_arg_8:
    635607  ∀M: internal_pseudo_address_map.
     
    695667  cases not_implemented *)
    696668qed.
     669*)
  • 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.