Changeset 2212


Ignore:
Timestamp:
Jul 18, 2012, 5:30:26 PM (5 years ago)
Author:
mulligan
Message:

More work on the INC case

Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProofSplit.ma

    r2210 r2212  
    445445            ]
    446446        | INC addr ⇒ λinstr_refl.
    447             match addr return λx. bool_to_Prop (is_in … [[ acc_a;registr;direct;indirect;dptr ]] x) → x = addr → Σs': PreStatus m cm. ? with
     447            match addr return λx. bool_to_Prop (is_in … [[ acc_a;registr;direct;indirect;dptr ]] x) → x = addr → ? with
    448448              [ ACC_A ⇒ λacc_a: True. λEQaddr.
    449449                let s' ≝ add_ticks1 s in
     
    767767  try (@(execute_1_technical … (subaddressing_modein …)) @I) (*66s*)
    768768  whd in match execute_1_preinstruction; normalize nodelta
    769   [35: (* XRL *)
     769  [(* 35: (* XRL *)
    770770    inversion addr
    771771    [1:
     
    869869      ]
    870870    ]
    871   |4,5,6,7,8,9: (* INC and DEC *)
     871  |33,34: (* ANL and ORL *)
     872    inversion addr
     873    [1,3:
     874      *
     875      [1,3:
     876        #acc_a_others inversion acc_a_others #acc_a #others #acc_a_others_refl #addr_refl
     877        >EQP -P normalize nodelta
     878        #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
     879        whd in maps_assm:(??%%);
     880        inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     881        [2,4: normalize nodelta #absurd destruct(absurd) ]
     882        inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
     883        [2,4: normalize nodelta #absurd destruct(absurd) ]
     884        normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     885        whd in ⊢ (??%?);
     886        <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
     887        change with (set_arg_8 ????? = ?)
     888        @set_arg_8_status_of_pseudo_status try %
     889        >EQs >EQticks <instr_refl >addr_refl
     890        [1,4:
     891          @sym_eq @set_clock_status_of_pseudo_status
     892          [1,3:
     893            @sym_eq @set_program_counter_status_of_pseudo_status %
     894          |2,4:
     895            @eq_f2 %
     896          ]
     897        |2,5:
     898          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … acc_a … addressing_mode_ok_assm_1)
     899          [1,3: @(subaddressing_mode_elim … acc_a) % ] %
     900        |3,6:
     901          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1)
     902          [1,5:
     903            @(subaddressing_mode_elim … acc_a) %
     904          |4,8:
     905            @eq_f2
     906            @(pose … (set_clock ????)) #status #status_refl
     907            @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
     908            [1,5:
     909              @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1)
     910              [1,5: @(subaddressing_mode_elim … acc_a) % |*: % ]
     911            |3,7:
     912              @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2)
     913              [1,5: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ |*: % ]
     914            |2,6:
     915              @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … acc_a … addressing_mode_ok_assm_1)
     916              [1,3: @(subaddressing_mode_elim … acc_a) % |*: % ]
     917            |4,8:
     918              @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2)
     919              [1,3: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ |*: % ]
     920            ]
     921          |*:
     922            %
     923          ]
     924        ]
     925      |2,4:
     926        #direct_others inversion direct_others #direct #others #direct_others_refl #addr_refl
     927        >EQP -P normalize nodelta
     928        #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
     929        whd in maps_assm:(??%%);
     930        inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     931        [2,4: normalize nodelta #absurd destruct(absurd) ]
     932        inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
     933        [2,4: normalize nodelta #absurd destruct(absurd) ]
     934        normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     935        whd in ⊢ (??%?);
     936        <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
     937        change with (set_arg_8 ????? = ?)
     938        @set_arg_8_status_of_pseudo_status try %
     939        >EQs >EQticks <instr_refl >addr_refl
     940        [1,4:
     941          @sym_eq @set_clock_status_of_pseudo_status
     942          [1,3:
     943            @sym_eq @set_program_counter_status_of_pseudo_status %
     944          |2,4:
     945            @eq_f2 %
     946          ]
     947        |2,5:
     948          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … direct … addressing_mode_ok_assm_1)
     949          [1,3: @(subaddressing_mode_elim … direct) #w % ] %
     950        |3,6:
     951          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … direct … addressing_mode_ok_assm_1)
     952          [1,5:
     953            @(subaddressing_mode_elim … direct) #w %
     954          |4,8:
     955            @eq_f2
     956            @(pose … (set_clock ????)) #status #status_refl
     957            @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
     958            [1,5:
     959              @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … direct … addressing_mode_ok_assm_1)
     960              [1,5: @(subaddressing_mode_elim … direct) #w % |*: % ]
     961            |3,7:
     962              @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2)
     963              [1,5: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ |*: % ]
     964            |2,6:
     965              @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … direct … addressing_mode_ok_assm_1)
     966              [1,3: @(subaddressing_mode_elim … direct) #w % |*: % ]
     967            |4,8:
     968              @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2)
     969              [1,3: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ |*: % ]
     970            ]
     971          |*:
     972            %
     973          ]
     974        ]
     975      ]
     976    |2,4:
     977      #carry_others inversion carry_others #carry #others #carry_others_refl #addr_refl
     978      >EQP -P normalize nodelta
     979      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
     980      whd in maps_assm:(??%%);
     981      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     982      [2,4: normalize nodelta #absurd destruct(absurd) ]
     983      inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
     984      [2,4: normalize nodelta #absurd destruct(absurd) ]
     985      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     986      whd in ⊢ (??%?);
     987      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
     988      change with (set_flags ?????? = ?)
     989      [1,4: @set_flags_status_of_pseudo_status try % |*: skip ]
     990      >EQs >EQticks <instr_refl >addr_refl
     991      @sym_eq @set_clock_status_of_pseudo_status %
     992    ]
     993  |*)4: (* INC *)
     994    (* XXX: work on the right hand side *)
     995    (* XXX: switch to the left hand side *)
     996    >EQs >EQticks <instr_refl >EQP -P normalize nodelta
     997    @(subaddressing_mode_elim … addr) normalize nodelta
     998    [1:
     999      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
     1000      whd in maps_assm:(??%%);
     1001      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     1002      [2: normalize nodelta #absurd destruct(absurd) ]
     1003      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     1004      whd in ⊢ (??%?);
     1005      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
     1006      whd in ⊢ (??%?);
     1007      inversion (half_add ???) #carry #result #carry_result_refl normalize nodelta
     1008      @(pair_replace ?????????? (refl_to_jmrefl ??? carry_result_refl))
     1009      [1:
     1010        @eq_f2 try %
     1011        @(pose … (set_clock ????)) #status #status_refl
     1012        @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
     1013        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ACC_A … addressing_mode_ok_assm_1) try %
     1014      |2:
     1015        @set_arg_8_status_of_pseudo_status try %
     1016        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ACC_A … addressing_mode_ok_assm_1) try %
     1017      ]
     1018    |2:
     1019    |3:
     1020    |4:
     1021    |5:
     1022      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
     1023      whd in maps_assm:(??%%); lapply maps_assm @Some_Some_elim #Mrefl destruct(Mrefl)
     1024      whd in ⊢ (??%?);
     1025      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
     1026      whd in ⊢ (??%?);
     1027      inversion (half_add ???) #carry #bl #carry_bl_refl normalize nodelta
     1028      @(pair_replace ?????????? (refl_to_jmrefl ??? carry_bl_refl))
     1029      [1:
     1030      |2:
     1031      ]
     1032    ]
     1033  |5,6,7,8,9: (* INC and DEC *)
    8721034    cases daemon
    8731035  |42,44: (* RL and RR *)
  • src/ASM/Interpret.ma

    r2160 r2212  
    159159            ]
    160160        | INC addr ⇒ λinstr_refl.
    161             match addr return λx. bool_to_Prop (is_in … [[ acc_a;registr;direct;indirect;dptr ]] x) → Σs': PreStatus m cm. ? with
     161            match addr return λx. bool_to_Prop (is_in … [[ acc_a;registr;direct;indirect;dptr ]] x) → ? with
    162162              [ ACC_A ⇒ λacc_a: True.
    163163                let s' ≝ add_ticks1 s in
     
    231231                s
    232232        | CLR addr ⇒ λinstr_refl.
    233           match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → Σs': PreStatus m cm. ? with
     233          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → ? with
    234234            [ ACC_A ⇒ λacc_a: True.
    235235              let s ≝ add_ticks1 s in
     
    244244            ] (subaddressing_modein … addr)
    245245        | CPL addr ⇒ λinstr_refl.
    246           match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → Σs': PreStatus m cm. ? with
     246          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → ? with
    247247            [ ACC_A ⇒ λacc_a: True.
    248248                let s ≝ add_ticks1 s in
     
    298298              set_8051_sfr … s SFR_ACC_A new_acc
    299299        | PUSH addr ⇒ λinstr_refl.
    300             match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → Σs': PreStatus m cm. ? with
     300            match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → ? with
    301301              [ DIRECT d ⇒ λdirect: True.
    302302                let s ≝ add_ticks1 s in
Note: See TracChangeset for help on using the changeset viewer.