Ignore:
Timestamp:
Jul 30, 2012, 2:36:41 PM (8 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProofSplit.ma

    r2273 r2276  
    5656qed.
    5757
     58lemma get_arg_8_status_of_pseudo_status':
     59  ∀cm,ps,l.
     60  ∀addr:[[ direct ; indirect ; registr ; acc_a ; acc_b ; data ; acc_dptr ; acc_pc ; ext_indirect ; ext_indirect_dptr ]].
     61  ∀M. ∀sigma. ∀policy. ∀s.
     62      s = status_of_pseudo_status M cm ps sigma policy →
     63      map_address_mode_using_internal_pseudo_address_map_ok1 M cm ps sigma addr →
     64      map_address_mode_using_internal_pseudo_address_map_ok2 … M sigma cm ps addr (get_arg_8 … cm ps l addr)
     65      = get_arg_8 … ps l addr →
     66      get_arg_8 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy)
     67      s l addr = get_arg_8 … ps l addr.
     68 #cm #ps #l #addr #M #sigma #policy #s #H1 #H2 #H3 @get_arg_8_status_of_pseudo_status
     69 try assumption %
     70qed.
     71
    5872lemma main_lemma_preinstruction:
    5973  ∀M, M': internal_pseudo_address_map.
     
    98112    P instr (execute_1_preinstruction ticks Identifier pseudo_assembly_program cm addr_of instr s).
    99113  (* XXX: takes about 45 minutes to type check! *)
    100   #M #M' #preamble #instr_list #cm #EQcm #is_well_labelled_witness #sigma #policy
     114  ** #low #high #accA #M' #preamble #instr_list #cm #EQcm #is_well_labelled_witness #sigma #policy
    101115  #sigma_policy_witness #ps #ppc #ppc_in_bounds_witness #EQppc #labels
    102116  #costs #create_label_cost_refl #newppc #lookup_labels #EQlookup_labels
     
    513527  try (@(execute_1_technical … (subaddressing_modein …)) @I) (*66s*)
    514528  whd in match execute_1_preinstruction; normalize nodelta
    515   [(*1,2: (* ADD and ADDC *)
     529  [1,2: (* ADD and ADDC *)
    516530    (* XXX: work on the right hand side *)
    517531    (* XXX: switch to the left hand side *)
     
    519533    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    520534    whd in maps_assm:(??%%);
    521     inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     535    inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1
    522536    [2,4: normalize nodelta #absurd destruct(absurd) ]
    523     inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
     537    inversion (assert_data ?????) #addressing_mode_ok_assm_2
    524538    [2,4: normalize nodelta #absurd destruct(absurd) ]
    525539    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
    526     whd in ⊢ (??%?);
    527     <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl
     540    letin M' ≝ (〈low,high,accA〉)
     541    whd in ⊢ (??%?);
     542    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
    528543    whd in ⊢ (??%?);
    529544    normalize nodelta >EQs >EQticks <instr_refl
     
    531546    [1,3:
    532547      @eq_f3
    533       [1,2,4,5:
    534         @(pose … (set_clock ????)) #status #status_refl
    535         @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
    536         [1,5:
     548      [1,2,4,5: @(get_arg_8_status_of_pseudo_status' … M')
     549        [3,9:
    537550          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr1 … addressing_mode_ok_assm_1) try %
    538551          @(subaddressing_mode_elim … addr1) %
    539         |3,7:
     552        |6,12:
    540553          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2) try %
    541554          @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %
    542         |2,6:
     555        |2,8:
    543556          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr1 … addressing_mode_ok_assm_1) try %
    544557          @(subaddressing_mode_elim … addr1) %
    545         |4,8:
     558        |5,11:
    546559          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2) try %
    547560          @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %
    548         ]
     561        |*: % ]
    549562      |3:
    550563        %
    551       |6:
    552         @sym_eq @(get_cy_flag_status_of_pseudo_status M')
    553         @sym_eq @set_clock_status_of_pseudo_status %
    554       ]
     564      |6: @(get_cy_flag_status_of_pseudo_status M') @set_clock_status_of_pseudo_status % ]
    555565    |2,4:
    556       #result #flags @sym_eq
    557       @set_flags_status_of_pseudo_status try %
    558       @sym_eq @set_arg_8_status_of_pseudo_status try %
    559       @(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm_1)
    560     ]
    561   |3: (* SUBB *)
     566      #result #flags @set_flags_status_of_pseudo_status try %
     567      @set_arg_8_status_of_pseudo_status try %
     568      @(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm_1)]
     569  |(*3: (* SUBB *)
    562570    (* XXX: work on the right hand side *)
    563571    (* XXX: switch to the left hand side *)
     
    11311139      ]
    11321140    ]
    1133   |*)12: (* JC *)
     1141  |12: (* JC *)
    11341142    >EQP -P normalize nodelta
    11351143    whd in match expand_pseudo_instruction; normalize nodelta
     
    18721880      @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_2 … ps ps … b … false (refl …) addressing_mode_ok_assm_1)
    18731881    ]
    1874   |*)42: (* PUSH *)
     1882  |*)*)42: (* PUSH *)
    18751883    >EQP -P normalize nodelta lapply instr_refl
    18761884    @(subaddressing_mode_elim … addr) #w #instr_refl normalize nodelta
    18771885    #sigma_increment_commutation
    1878     whd in ⊢ (??%? → ?); inversion M #callM #accM #callM_accM_refl normalize nodelta
     1886    whd in ⊢ (??%? → ?);
     1887    @vsplit_elim #bit_one #seven_bits
     1888    cases (Vector_Sn … bit_one) #bitone * #empty >(Vector_O … empty) #H >H -bit_one
     1889    cases bitone #bit_one_seven_bits_refl normalize nodelta
     1890    [ @eq_bv_elim #seven_bits_refl normalize nodelta
     1891    | inversion (lookup_from_internal_ram ??) normalize nodelta [2: #addr_entry]
     1892      #lookup_from_internal_ram_refl ]
    18791893    @Some_Some_elim #Mrefl destruct(Mrefl) #fetch_many_assm %{1}
    18801894    whd in ⊢ (??%?);
     
    18831897    @pair_elim #carry #new_sp #carry_new_sp_refl normalize nodelta
    18841898    @(pair_replace ?????????? (eq_to_jmeq … carry_new_sp_refl))
    1885     [1:
     1899    [1,3,5,7:
    18861900      @eq_f2 try %
    18871901      @(pose … (set_clock ????)) #status #status_refl
    1888       @sym_eq @(get_8051_sfr_status_of_pseudo_status … 〈callM, accM〉 … status) >status_refl -status_refl try %
    1889       @sym_eq @set_clock_status_of_pseudo_status
    1890       >EQs >EQticks <instr_refl %
    1891     |2:
     1902      @sym_eq @(get_8051_sfr_status_of_pseudo_status … 〈low,high,accA〉 … status) >status_refl -status_refl try %
     1903      @set_clock_status_of_pseudo_status >EQs >EQticks <instr_refl %
     1904    |*:
    18921905      >EQs >EQticks <instr_refl
    18931906      cases daemon (* XXX: write_at_stack_pointer_status_of_pseudo_status *)
Note: See TracChangeset for help on using the changeset viewer.