Ignore:
Timestamp:
Jul 10, 2012, 5:29:32 PM (8 years ago)
Author:
mulligan
Message:

MUL case of main lemma nearly complete (subject to two small holes that require a lemma) using new proof strategy.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProofSplit.ma

    r2172 r2173  
    1919include alias "ASM/Vector.ma".
    2020include "ASM/Test.ma".
     21
     22lemma addressing_mode_ok_to_map_address_using_internal_pseudo_address_map:
     23  ∀M, cm, ps, sigma, x.
     24  ∀addr1: [[acc_a]].
     25    addressing_mode_ok pseudo_assembly_program M cm ps addr1=true →
     26      map_address_using_internal_pseudo_address_map M sigma SFR_ACC_A x = x.
     27  #M #cm #ps #sigma #x #addr1
     28  @(subaddressing_mode_elim … addr1)
     29  whd in ⊢ (??%? → ??%?);
     30  cases (\snd M)
     31  [1:
     32    //
     33  |2:
     34    #upper_lower #address normalize nodelta #absurd
     35    destruct(absurd)
     36  ]
     37qed.
    2138
    2239lemma main_lemma_preinstruction:
     
    477494  try (@(execute_1_technical … (subaddressing_modein …)) @I) (*66s*)
    478495  whd in match execute_1_preinstruction; normalize nodelta
    479   [31,32: (* DJNZ *)
     496
     497(*  [31,32: (* DJNZ *)
    480498  (* XXX: work on the right hand side *)
    481499  >p normalize nodelta >p1 normalize nodelta
     
    10491067  (* XXX: finally, prove the equality using sigma commutation *)
    10501068  try @split_eq_status try %
    1051   cases daemon
    1052   |10,42,43,44,45,49,52,56: (* MUL *)
     1069  cases daemon *)
     1070  [42,43,44,45,49,52,56:
     1071  |10: (* MUL *)
    10531072  (* XXX: work on the right hand side *)
    10541073  (* XXX: switch to the left hand side *)
    1055   -instr_refl >EQP -P normalize nodelta
     1074  >EQP -P normalize nodelta
    10561075  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
     1076  whd in maps_assm:(??%%);
     1077  inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     1078  [2: normalize nodelta #absurd destruct(absurd) ]
     1079  inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
     1080  [2: normalize nodelta #absurd destruct(absurd) ]
     1081  normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
    10571082  whd in ⊢ (??%?);
    1058   <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
     1083  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl
     1084  change with (set_8051_sfr ????? = ?) @set_8051_sfr_status_of_pseudo_status
     1085  [2:
     1086    whd in ⊢ (??%?); @eq_f2 try % @eq_f2 try % @eq_f2 @eq_f
     1087    @sym_eq
     1088    [1:
     1089      @(get_8051_sfr_status_of_pseudo_status … policy)
     1090      cases daemon (* XXX: need a lemma *)
     1091    |2:
     1092      @(get_8051_sfr_status_of_pseudo_status M' … policy)
     1093      @sym_eq @set_clock_status_of_pseudo_status [2: % ]
     1094      @sym_eq @set_program_counter_status_of_pseudo_status %
     1095    ]
     1096  ]
     1097  @sym_eq @set_8051_sfr_status_of_pseudo_status
     1098  [2:
     1099    >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm_1)
     1100    @eq_f @eq_f2 try % @eq_f2 @eq_f
     1101    @sym_eq
     1102    [1:
     1103      @(get_8051_sfr_status_of_pseudo_status … policy)
     1104      cases daemon (* XXX: needs a lemma *)
     1105    |2:
     1106      @(get_8051_sfr_status_of_pseudo_status M' … policy)
     1107      @sym_eq @set_clock_status_of_pseudo_status [2: % ]
     1108      @sym_eq @set_program_counter_status_of_pseudo_status %
     1109    ]
     1110  ]
     1111  @sym_eq @set_clock_status_of_pseudo_status
     1112  [2:
     1113    @eq_f %
     1114  ]
     1115  @sym_eq @set_program_counter_status_of_pseudo_status %
     1116   
    10591117  (* XXX: work on the left hand side *)
    10601118  (* XXX: switch to the right hand side *)
Note: See TracChangeset for help on using the changeset viewer.