Changeset 2207 for src


Ignore:
Timestamp:
Jul 18, 2012, 12:29:14 PM (9 years ago)
Author:
mulligan
Message:

Improvements and corrections to the main lemma proof in AssemblyProofSplit?.ma.

Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed

  • src/ASM/AssemblyProofSplit.ma

    r2204 r2207  
    109109qed.
    110110
     111lemma sfr_psw_eq_to_bit_address_of_register_eq:
     112  ∀A: Type[0].
     113  ∀code_memory: A.
     114  ∀status, status', register_address.
     115    get_8051_sfr … status SFR_PSW = get_8051_sfr … status' SFR_PSW →
     116      bit_address_of_register A code_memory status register_address = bit_address_of_register A code_memory status' register_address.
     117  #A #code_memory #status #status' #register_address #sfr_psw_refl
     118  whd in match bit_address_of_register; normalize nodelta
     119  <sfr_psw_refl %
     120qed.
     121
     122lemma sfr_psw_and_low_internal_ram_eq_to_get_register_eq:
     123  ∀A: Type[0].
     124  ∀code_memory: A.
     125  ∀status, status', register_address.
     126    get_8051_sfr … status SFR_PSW = get_8051_sfr … status' SFR_PSW →
     127      low_internal_ram A code_memory status = low_internal_ram A code_memory status' →
     128        get_register A code_memory status register_address = get_register A code_memory status' register_address.
     129  #A #code_memory #status #status' #register_address #sfr_psw_refl #low_internal_ram_refl
     130  whd in match get_register; normalize nodelta <low_internal_ram_refl
     131  >(sfr_psw_eq_to_bit_address_of_register_eq … status status') //
     132qed.
     133
    111134lemma map_address_mode_using_internal_pseudo_address_map_ok1_addr:
    112135  ∀M', cm, status, status', sigma.
    113136  ∀addr1: [[acc_a; registr; direct; indirect; data]]. (* XXX: expand as needed *)
    114     status = status' →
     137    get_8051_sfr … status SFR_PSW = get_8051_sfr … status' SFR_PSW →
    115138    addressing_mode_ok pseudo_assembly_program M' cm status addr1 = true →
    116139    map_address_mode_using_internal_pseudo_address_map_ok1 M' cm status' sigma addr1.
    117   #M' #cm #status #status' #sigma #addr1 #status_refl <status_refl
     140  #M' #cm #status #status' #sigma #addr1 #sfr_refl
    118141  @(subaddressing_mode_elim … addr1) try (#w #_ @I)
    119142  [1: #_ @I ]
    … …  
    125148    #_
    126149    @(assoc_list_exists_false_to_assoc_list_lookup_None … (refl …) … assoc_list_exists_refl)
    127     cases w whd in ⊢ (??%%); @lookup_low_internal_ram_false % (* XXX: dubious *)
     150    whd in match get_register; normalize nodelta
     151    cases w whd in ⊢ (??%%); @lookup_low_internal_ram_false
     152    @sfr_psw_eq_to_bit_address_of_register_eq assumption (* XXX: dubious *)
    128153  ]
    129154qed.
     155(* XXX: indirect case false above *)
    130156
    131157lemma addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2:
    132158  ∀M', cm.
    133   ∀sigma, status, b.
     159  ∀sigma, status, status', b, b'.
    134160  ∀addr1: [[acc_a; registr; direct; indirect; data; bit_addr]]. (* XXX: expand as needed *)
     161    get_8051_sfr … status SFR_PSW = get_8051_sfr … status' SFR_PSW →
     162    low_internal_ram pseudo_assembly_program cm status = low_internal_ram pseudo_assembly_program cm status' →
     163    b = b' →
    135164    addressing_mode_ok pseudo_assembly_program M' cm status addr1 = true →
    136       map_address_mode_using_internal_pseudo_address_map_ok2 pseudo_assembly_program M' sigma cm status addr1 b = b.
    137   #M' #cm #sigma #status #b #addr1
     165      map_address_mode_using_internal_pseudo_address_map_ok2 pseudo_assembly_program M' sigma cm status' addr1 b = b'.
     166  #M' #cm #sigma #status #status' #b #b' #addr1 #sfr_refl #low_internal_ram_refl #b_refl <b_refl
    138167  @(subaddressing_mode_elim … addr1)
    139168  [1:
    … …  
    149178    [1,3:
    150179      #absurd destruct(absurd)
    151     |2,4:
    152       #_ >(assoc_list_exists_false_to_assoc_list_lookup_None … (refl …) … assoc_list_exists_refl)
     180    |2:
     181      #_
     182      <(sfr_psw_eq_to_bit_address_of_register_eq … status status' w … sfr_refl)
     183      >(assoc_list_exists_false_to_assoc_list_lookup_None … (refl …) … assoc_list_exists_refl)
     184      normalize nodelta %
     185    |4:
     186      #_
     187      <(sfr_psw_and_low_internal_ram_eq_to_get_register_eq … status status' [[false; false; w]] … sfr_refl low_internal_ram_refl)
     188      >(assoc_list_exists_false_to_assoc_list_lookup_None … (refl …) … assoc_list_exists_refl)
    153189      normalize nodelta %
    154190    ]
    … …  
    665701      @set_arg_8_status_of_pseudo_status try %
    666702      [ @sym_eq @set_clock_status_of_pseudo_status
    667         [ @sym_eq @set_program_counter_status_of_pseudo_status
    668           [
    669           |
    670           ]
    671         |
    672         ]
    673       |
    674       | @sym_eq
    675       ]
    676 cases daemon (*
    677       whd in ⊢ (??%?); normalize nodelta
    678       lapply addr_refl @(subaddressing_mode_elim … acc_a) #addr_refl normalize nodelta
    679       @set_8051_sfr_status_of_pseudo_status
    680       [1:
    681         @sym_eq @set_clock_status_of_pseudo_status
    682         >EQs >EQticks <instr_refl >addr_refl %
    683       |2:
    684         whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … acc_a addressing_mode_ok_assm_1)
    685         normalize nodelta @eq_f2
     703        [ @sym_eq >EQs @set_program_counter_status_of_pseudo_status %
     704        | >EQs >EQticks <instr_refl >addr_refl @eq_f2 %
     705        ]
     706      | @(subaddressing_mode_elim … acc_a) @I
     707      | >EQs >EQticks <instr_refl >addr_refl
     708        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1)
    686709        [1:
     710          @(subaddressing_mode_elim … acc_a) %
     711        |2:
     712          %
     713        |3:
     714          %
     715        |4:
     716          @eq_f2
    687717          @(pose … (set_clock ????)) #status #status_refl
    688           @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl
    689           >EQs >EQticks <instr_refl >addr_refl
     718          @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
    690719          [1:
    691             @sym_eq @set_clock_status_of_pseudo_status try %
    692           |2:
    693             whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … acc_a addressing_mode_ok_assm_1) %
    694           |3:
    695             @I
    696           ]
    697         |2:
    698           @(pose … (set_clock ????)) #status #status_refl
    699           @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl
    700           >EQs >EQticks <instr_refl >addr_refl
    701           [1:
    702             @sym_eq @set_clock_status_of_pseudo_status try %
    703           |2:
    704             lapply addressing_mode_ok_assm_2 cases others #addressing_mode cases addressing_mode
    705             try (#w whd in ⊢ (% → ?); #absurd #addressing_mode_ok_assm_2 cases absurd)
    706             try (whd in ⊢ (% → ?); #absurd #addressing_mode_ok_assm_2 cases absurd)
    707             whd in ⊢ (??%?); try % whd in addressing_mode_ok_assm_2:(??%?);
    708             (* XXX: subaddressing_mode_elim is too slow above so do it by hand *)
     720            @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1)
    709721            [1:
    710             |2,3:
    711               lapply addressing_mode_ok_assm_2
    712               inversion (assoc_list_exists ?????) #assoc_list_exists_assm normalize nodelta
    713               [1,3: #absurd destruct(absurd) ] #_
    714               >(assoc_list_exists_false_to_assoc_list_lookup_None ????????? assoc_list_exists_assm) in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? ])?);
     722              @(subaddressing_mode_elim … acc_a) %
     723            |*:
    715724              %
    716725            ]
    717726          |3:
    718             @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others)
    719             [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/]
    720             whd in ⊢ (??%?);
    721             lapply addressing_mode_ok_assm_2 cases others #addressing_mode cases addressing_mode
    722             try (#w whd in ⊢ (% → ?); #absurd #addressing_mode_ok_assm_2 cases absurd)
    723             try (whd in ⊢ (% → ?); #absurd #addressing_mode_ok_assm_2 cases absurd)
    724             whd whd in addressing_mode_ok_assm_2:(??%?); try @I
    725             inversion (assoc_list_exists ?????) in addressing_mode_ok_assm_2;
    726             #assoc_list_exists_assm normalize nodelta
     727            @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2)
    727728            [1:
    728               #absurd destruct(absurd)
     729              /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/
     730            |*:
     731              %
     732            ]
     733          |2:
     734            @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … acc_a … addressing_mode_ok_assm_1)
     735            [1:
     736              @(subaddressing_mode_elim … acc_a) %
    729737            |2:
    730               #_ @(assoc_list_exists_false_to_assoc_list_lookup_None ????????? assoc_list_exists_assm)
    731               try %
    732               whd in match get_register; normalize nodelta
    733               @lookup_low_internal_ram_false
    734               @eq_f2 try % whd in ⊢ (???%);
     738              %
     739            ]
     740          |4:
     741            @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2)
     742            [1:
     743              /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/
     744            |*:
     745              %
    735746            ]
    736747          ]
    … …  
    738749      ]
    739750    |2:
    740     ]*)]
     751      cases daemon (* XXX: todo *)
     752    ]
    741753  |4,5,6,7,8,9: (* INC and DEC *)
    742754    cases daemon
    … …  
    806818    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl
    807819    whd in ⊢ (??%?);
     820    normalize nodelta >EQs >EQticks <instr_refl
    808821    @let_pair_in_status_of_pseudo_status
    809822    [1,3:
    810823      @eq_f3
    811       [1,2,4,5:
    812        @sym_eq
    813        [ @(get_arg_8_status_of_pseudo_status) FOO
    814        normalize nodelta >EQs >EQticks <instr_refl %
     824      [1,2,4,5:
     825        @(pose … (set_clock ????)) #status #status_refl
     826        @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
     827        [1,5:
     828          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr1 … addressing_mode_ok_assm_1) try %
     829          @(subaddressing_mode_elim … addr1) %
     830        |3,7:
     831          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2) try %
     832          /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/
     833        |2,6:
     834          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr1 … addressing_mode_ok_assm_1) try %
     835          @(subaddressing_mode_elim … addr1) %
     836        |4,8:
     837          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2) try %
     838          /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/
     839        ]
    815840      |3: %
    816       |6: normalize nodelta
    817           @eq_f @eq_f2
    818           [1: >EQs %
    819           |2: >EQticks @eq_f2 <instr_refl try % >EQs %
    820           ]
    821       ]
    822 
    823 
    824 
    825     @(pair_replace ?????????? p)
    826     [2,4:
    827       @(pair_replace ?????????? p)
    828       [2,4:
    829         normalize nodelta
    830         @set_flags_status_of_pseudo_status try %
    831         @sym_eq @set_arg_8_status_of_pseudo_status try %
    832         @(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm_1)
    833       |1,3:
    834         @eq_f3
    835         [1,2,4,5:
    836           normalize nodelta
    837           >EQs >EQticks <instr_refl %
    838         |3:
    839           %
    840         |6:
    841           normalize nodelta
    842           @eq_f @eq_f2
    843           [1:
    844             >EQs %
    845           |2:
    846             >EQticks @eq_f2 <instr_refl try % >EQs %
    847           ]
    848         ]
    849       ]
    850     |1,3:
    851       @eq_f3
    852       [1,2,4,5:
    853         normalize nodelta
    854         >EQs >EQticks <instr_refl
    855         cases daemon (* XXX: matita dies here *)
    856       |3:
    857         %
    858841      |6:
    859         normalize nodelta
    860         @(get_cy_flag_status_of_pseudo_status … M')
    861         @sym_eq @set_clock_status_of_pseudo_status
    862         [1:
    863           @sym_eq >EQs
    864           @set_program_counter_status_of_pseudo_status %
    865         |2:
    866           >EQticks <instr_refl >EQs %
    867         ]
    868       ]
     842        @sym_eq @(get_cy_flag_status_of_pseudo_status M')
     843        @sym_eq @set_clock_status_of_pseudo_status %
     844      ]
     845    |2,4:
     846      #result #flags @sym_eq
     847      @set_flags_status_of_pseudo_status try %
     848      @sym_eq @set_arg_8_status_of_pseudo_status try %
     849      @(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm_1)
    869850    ]
    870851  |3: (* SUB *)

  • src/ASM/Test.ma

    r2204 r2207  
    13551355qed.
    13561356
    1357 lemma get_cy_flag_status_of_pseudo_status:
    1358   ∀M: internal_pseudo_address_map.
    1359   ∀sigma: Word → Word.
    1360   ∀policy: Word → bool.
    1361   ∀code_memory: pseudo_assembly_program.
    1362   ∀s: PreStatus ? code_memory.
    1363   ∀s'.
    1364     status_of_pseudo_status M code_memory s sigma policy = s' →
    1365       get_cy_flag ?? s' = get_cy_flag ? code_memory s.
    1366   #M #sigma #policy #code_memory #s #s' #s_refl <s_refl
    1367   whd in match get_cy_flag; normalize nodelta
    1368   whd in match status_of_pseudo_status; normalize nodelta
    1369   whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
    1370   cases (\snd M) try %
    1371   * normalize nodelta #address
    1372   @(vsplit_elim bool ???) #high #low #high_low_refl normalize nodelta
    1373   whd in match sfr_8051_index; normalize nodelta
    1374   >get_index_v_set_index_miss [2,4: /2/] %
    1375 qed.
    1376 
    13771357lemma get_ov_flag_status_of_pseudo_status:
    13781358  ∀M: internal_pseudo_address_map.
Note: See TracChangeset for help on using the changeset viewer.