Changeset 2258 for src/ASM


Ignore:
Timestamp:
Jul 25, 2012, 1:47:01 PM (9 years ago)
Author:
sacerdot
Message:
  1. lemma generalized
  2. automation replaced with expansion to make everything faster
Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed

  • src/ASM/AssemblyProofSplit.ma

    r2257 r2258  
    898898        |3,7:
    899899          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2) try %
    900           /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/
     900          @(is_in_subvector_is_in_supervector … (subaddressing_modein …))
    901901        |2,6:
    902902          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr1 … addressing_mode_ok_assm_1) try %
    … …  
    904904        |4,8:
    905905          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2) try %
    906           /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/
     906          @(is_in_subvector_is_in_supervector … (subaddressing_modein …))
    907907        ]
    908908      |3: %
    … …  
    943943          >status_refl
    944944          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr1 … addressing_mode_ok_assm_1)
    945           [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] %
     945          [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
    946946        |3:
    947947          >status_refl
    948948          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr1 … addressing_mode_ok_assm_1)
    949           [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] %
     949          [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
    950950        ]
    951951      |2:
    … …  
    957957          >status_refl
    958958          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2)
    959           [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] %
     959          [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
    960960        |3:
    961961          >status_refl
    962962          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2)
    963           [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] %
     963          [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
    964964        ]
    965965      |3:
    … …  
    986986        |3:
    987987          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ps … ACC_A)
    988           [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] try %
     988          [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] try %
    989989          <addressing_mode_ok_assm_1 @(subaddressing_mode_elim … addr1) %
    990990        ]
    … …  
    15341534            |3,7:
    15351535              @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2)
    1536               [1,5: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ |*: % ]
     1536              [1,5: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) |*: % ]
    15371537            |2,6:
    15381538              @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … acc_a … addressing_mode_ok_assm_1)
    … …  
    15401540            |4,8:
    15411541              @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2)
    1542               [1,3: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ |*: % ]
     1542              [1,3: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) |*: % ]
    15431543            ]
    15441544          |*:
    … …  
    15841584            |3,7:
    15851585              @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2)
    1586               [1,5: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ |*: % ]
     1586              [1,5: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) |*: % ]
    15871587            |2,6:
    15881588              @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … direct … addressing_mode_ok_assm_1)
    … …  
    15901590            |4,8:
    15911591              @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2)
    1592               [1,3: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ |*: % ]
     1592              [1,3: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) |*: % ]
    15931593            ]
    15941594          |*:
    … …  
    16531653          |3:
    16541654            @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2)
    1655             [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ |*: % ]
     1655            [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) |*: % ]
    16561656          |2:
    16571657            @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … acc_a … addressing_mode_ok_assm_1)
    … …  
    16591659          |4:
    16601660            @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2)
    1661             [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ |*: % ]
     1661            [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) |*: % ]
    16621662          ]
    16631663        |*:
    … …  
    17031703          |3:
    17041704            @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2)
    1705             [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ |*: % ]
     1705            [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) |*: % ]
    17061706          |2:
    17071707            @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … direct … addressing_mode_ok_assm_1)
    … …  
    17091709          |4:
    17101710            @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2)
    1711             [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ |*: % ]
     1711            [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) |*: % ]
    17121712          ]
    17131713        |*:
    … …  
    19831983                  |2:
    19841984                    @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2)
    1985                     [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] %
     1985                    [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
    19861986                  |3:
    19871987                    @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2)
    1988                     [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] %
     1988                    [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
    19891989                  ]
    19901990                ]
    … …  
    20072007              [1:
    20082008                @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_1)
    2009                 [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] %
     2009                [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
    20102010              |2:
    20112011                @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_1)
    20122012                [1:
    2013                   /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/
     2013                  @(is_in_subvector_is_in_supervector … (subaddressing_modein …))
    20142014                |2,3:
    20152015                  %
    … …  
    20212021                  |2:
    20222022                    @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others' … addressing_mode_ok_assm_2)
    2023                     [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] %
     2023                    [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
    20242024                  |3:
    20252025                    @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others' … addressing_mode_ok_assm_2)
    2026                     [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] %
     2026                    [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
    20272027                  ]
    20282028                ]
    … …  
    20482048            |2:
    20492049              @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … direct … addressing_mode_ok_assm_1)
    2050               [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] %
     2050              [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
    20512051            |3:
    20522052              @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … direct … addressing_mode_ok_assm_1)
    20532053              [1:
    2054                 /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/
     2054                @(is_in_subvector_is_in_supervector … (subaddressing_modein …))
    20552055              |2,3:
    20562056                %
    … …  
    20602060                [1:
    20612061                  @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2)
    2062                   [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] %
     2062                  [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
    20632063                |2:
    20642064                  @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2) %
    … …  
    20802080          <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
    20812081          change with (set_arg_16 ????? = ?)
    2082           @set_arg_16_status_of_pseudo_status
     2082          @set_arg_16_status_of_pseudo_status try %
    20832083          >EQs >EQticks <instr_refl >addr_refl
    20842084          @sym_eq @set_clock_status_of_pseudo_status %
    … …  
    22592259      [1:
    22602260        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2)
    2261         [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ |*: % ]
     2261        [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) |*: % ]
    22622262      |2:
    22632263        @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2)
    2264         [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ |*: % ]
     2264        [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) |*: % ]
    22652265      ]
    22662266    |2:
    22672267      @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2)
    22682268      [1:
    2269         /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/
     2269        @(is_in_subvector_is_in_supervector … (subaddressing_modein …))
    22702270      |*:
    22712271        whd in match get_8051_sfr in ⊢ (???%); normalize nodelta
    … …  
    22772277      @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2) try %
    22782278      [1:
    2279         /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/
     2279        @(is_in_subvector_is_in_supervector … (subaddressing_modein …))
    22802280      |2:
    22812281        whd in match get_8051_sfr in ⊢ (???%); normalize nodelta
    … …  
    23172317        [1:
    23182318          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2)
    2319           [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ |*: % ]
     2319          [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) |*: % ]
    23202320        |2:
    23212321          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2)
    2322           [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ |*: % ]
     2322          [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) |*: % ]
    23232323        ]
    23242324      |2:
    … …  
    23402340              @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2)
    23412341              [1:
    2342                 /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/
     2342                @(is_in_subvector_is_in_supervector … (subaddressing_modein …))
    23432343              |2:
    23442344                whd in match get_8051_sfr in ⊢ (???%); normalize nodelta
    … …  
    23502350              @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2) try %
    23512351              [1:
    2352                 /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/
     2352                @(is_in_subvector_is_in_supervector … (subaddressing_modein …))
    23532353              |2:
    23542354                whd in match get_8051_sfr in ⊢ (???%); normalize nodelta
    … …  
    23622362      ]
    23632363    ]
    2364   |*)50: (* RET *)
     2364  |50: (* RET *)
    23652365    >EQP -P normalize nodelta
    23662366    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    … …  
    24152415    @set_clock_status_of_pseudo_status %
    24162416  ]
     2417cases daemon
    24172418qed.
    24182419
    … …  
    25622563    [1,3:
    25632564      >EQs @eq_f3 [2,3,5,6: % ] >(get_arg_8_set_program_counter … true addr1)
    2564       [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
     2565      [2,4: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ]
    25652566      >(get_arg_8_set_program_counter … true addr1)
    2566       [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
     2567      [2,4: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ]
    25672568      @get_arg_8_pseudo_addressing_mode_ok assumption
    25682569    |2,4:
    … …  
    25742575      [1,10:
    25752576        whd in ⊢ (??%%); >set_arg_8_set_program_counter
    2576         [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
     2577        [2,4: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ]
    25772578        >low_internal_ram_set_program_counter
    25782579        [1:
    … …  
    25852586      |2,11:
    25862587        whd in ⊢ (??%%); >set_arg_8_set_program_counter
    2587         [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
     2588        [2,4: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ]
    25882589        >high_internal_ram_set_program_counter
    25892590        [1:
    … …  
    25962597      |3,12:
    25972598        whd in ⊢ (??%%); >(external_ram_set_arg_8 ??? addr1) in ⊢ (???%);
    2598         [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
     2599        [2,4: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ]
    25992600        >(external_ram_set_arg_8 ??? addr1)
    2600         [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] %
     2601        [2,4: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
    26012602      |4,13:
    26022603        whd in ⊢ (??%%); >EQaddr_of normalize nodelta
    … …  
    26042605          >program_counter_set_program_counter
    26052606          >set_arg_8_set_program_counter
    2606           [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
     2607          [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ]
    26072608          >set_clock_set_program_counter >program_counter_set_program_counter
    26082609          change with (add ??? = ?)
    … …  
    26102611        |2:
    26112612          >set_arg_8_set_program_counter
    2612           [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
     2613          [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ]
    26132614          >program_counter_set_program_counter
    26142615          >set_arg_8_set_program_counter
    2615           [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
     2616          [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ]
    26162617          >set_clock_set_program_counter >program_counter_set_program_counter
    26172618          >sigma_increment_commutation <EQppc
    … …  
    26262627          >special_function_registers_8051_set_clock
    26272628          >set_arg_8_set_program_counter in ⊢ (???%);
    2628           [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
     2629          [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ]
    26292630          >special_function_registers_8051_set_program_counter
    26302631          >set_arg_8_set_program_counter
    2631           [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
     2632          [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ]
    26322633          >special_function_registers_8051_set_program_counter
    26332634          @special_function_registers_8051_set_arg_8 assumption
    … …  
    26352636          >special_function_registers_8051_set_clock
    26362637          >set_arg_8_set_program_counter
    2637           [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
     2638          [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ]
    26382639          >set_arg_8_set_program_counter
    2639           [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
     2640          [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ]
    26402641          >special_function_registers_8051_set_program_counter
    26412642          >special_function_registers_8051_set_program_counter
    … …  
    26472648        [1:
    26482649          >set_arg_8_set_program_counter
    2649           [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
     2650          [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ]
    26502651          >set_arg_8_set_program_counter
    2651           [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
     2652          [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ]
    26522653          >special_function_registers_8052_set_program_counter
    26532654          >special_function_registers_8052_set_program_counter
    … …  
    27322733        change with (add ???) in match (\snd (half_add ???));
    27332734        >set_arg_8_set_program_counter in ⊢ (???%);
    2734         [2,4,6,8: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
     2735        [2,4,6,8: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ]
    27352736        >program_counter_set_program_counter in ⊢ (???%);
    27362737        >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc')

  • src/ASM/Test.ma

    r2247 r2258  
    982982  ∀cm.
    983983  ∀ps.
    984   ∀addr: [[dptr]].
    985   ∀v: Word.
     984  ∀addr,addr': [[dptr]].
     985  ∀v,v': Word.
    986986  ∀M. ∀sigma. ∀policy. ∀s'.
    987987    status_of_pseudo_status M cm ps sigma policy = s' →
     988    v=v' → addr=addr' →
    988989      set_arg_16 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy)
    989       s' v addr =
     990      s' v' addr' =
    990991      status_of_pseudo_status M cm (set_arg_16 ? cm ps v addr) sigma policy.
    991   #cm #ps #addr #v #M #sigma #policy #s' #s_refl <s_refl
     992  #cm #ps #addr #addr' #v #v' #M #sigma #policy #s' #s_refl <s_refl #addr_refl
     993  <addr_refl #v_refl <v_refl
    992994  @(subaddressing_mode_elim … addr)
    993995  whd in match set_arg_16; normalize nodelta
Note: See TracChangeset for help on using the changeset viewer.