Changeset 1625


Ignore:
Timestamp:
Dec 16, 2011, 6:35:45 PM (8 years ago)
Author:
mulligan
Message:

before christmas

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r1624 r1625  
    187187qed.
    188188
     189axiom is_in_subvector_is_in_supervector:
     190  ∀m, n: nat.
     191  ∀subvector: Vector addressing_mode_tag m.
     192  ∀supervector: Vector addressing_mode_tag n.
     193  ∀element: addressing_mode.
     194    subvector_with … eq_a subvector supervector →
     195      is_in m subvector element → is_in n supervector element.
     196
    189197let rec member_addressing_mode_tag
    190198  (n: nat) (v: Vector addressing_mode_tag n) (a: addressing_mode_tag)
     
    197205 
    198206let rec subaddressing_mode_elim_type
    199   (T: Type[2]) (n: nat) (v: Vector addressing_mode_tag n)
     207  (T: Type[2]) (m: nat) (fixed_v: Vector addressing_mode_tag m)
    200208    (Q: addressing_mode → T → Prop)
    201       on v:
    202     (∀w: Word11.      is_in n v (ADDR11 w)        → T) →
    203     (∀w: Word.        is_in n v (ADDR16 w)        → T) →
    204     (∀w: Byte.        is_in n v (DIRECT w)        → T) →
    205     (∀w: Bit.         is_in n v (INDIRECT w)      → T) →
    206     (∀w: Bit.         is_in n v (EXT_INDIRECT w)  → T) →
    207     (                 is_in n v ACC_A             → T) →
    208     (∀w: BitVector 3. is_in n v (REGISTER w)      → T) →
    209     (                 is_in n v ACC_B             → T) →
    210     (                 is_in n v DPTR              → T) →
    211     (∀w: Byte.        is_in n v (DATA w)          → T) →
    212     (∀w: Word.        is_in n v (DATA16 w)        → T) →
    213     (                 is_in n v ACC_DPTR          → T) →
    214     (                 is_in n v ACC_PC            → T) →
    215     (                 is_in n v EXT_INDIRECT_DPTR → T) →
    216     (                 is_in n v INDIRECT_DPTR     → T) →
    217     (                 is_in n v CARRY             → T) →
    218     (∀w: Byte.        is_in n v (BIT_ADDR w)      → T) →
    219     (∀w: Byte.        is_in n v (N_BIT_ADDR w)    → T) →
    220     (∀w: Byte.        is_in n v (RELATIVE w)      → T) → Prop ≝
    221   match v return λm: nat. λv': Vector addressing_mode_tag m. m = n → v ≃ v' → ? with
     209      (p_addr11:            ∀w: Word11.      is_in m fixed_v (ADDR11 w)        → T)
     210      (p_addr16:            ∀w: Word.        is_in m fixed_v (ADDR16 w)        → T)
     211      (p_direct:            ∀w: Byte.        is_in m fixed_v (DIRECT w)        → T)
     212      (p_indirect:          ∀w: Bit.         is_in m fixed_v (INDIRECT w)      → T)
     213      (p_ext_indirect:      ∀w: Bit.         is_in m fixed_v (EXT_INDIRECT w)  → T)
     214      (p_acc_a:                              is_in m fixed_v ACC_A             → T)
     215      (p_register:          ∀w: BitVector 3. is_in m fixed_v (REGISTER w)      → T)
     216      (p_acc_b:                              is_in m fixed_v ACC_B             → T)
     217      (p_dptr:                               is_in m fixed_v DPTR              → T)
     218      (p_data:              ∀w: Byte.        is_in m fixed_v (DATA w)          → T)
     219      (p_data16:            ∀w: Word.        is_in m fixed_v (DATA16 w)        → T)
     220      (p_acc_dptr:                           is_in m fixed_v ACC_DPTR          → T)
     221      (p_acc_pc:                             is_in m fixed_v ACC_PC            → T)
     222      (p_ext_indirect_dptr:                  is_in m fixed_v EXT_INDIRECT_DPTR → T)
     223      (p_indirect_dptr:                      is_in m fixed_v INDIRECT_DPTR     → T)
     224      (p_carry:                              is_in m fixed_v CARRY             → T)
     225      (p_bit_addr:          ∀w: Byte.        is_in m fixed_v (BIT_ADDR w)      → T)
     226      (p_n_bit_addr:        ∀w: Byte.        is_in m fixed_v (N_BIT_ADDR w)    → T)
     227      (p_relative:          ∀w: Byte.        is_in m fixed_v (RELATIVE w)      → T)
     228        (n: nat) (v: Vector addressing_mode_tag n) (proof: subvector_with … eq_a v fixed_v)
     229      on v: Prop ≝
     230  match v return λo: nat. λv': Vector addressing_mode_tag o. o = n → v ≃ v' → ? with
    222231  [ VEmpty         ⇒ λm_refl. λv_refl.
    223     λp_addr11. λp_addr16. λp_direct. λp_indirect. λp_ext_indirect. λp_acc_a.
    224     λp_register. λp_acc_b. λp_dptr. λp_data. λp_data16. λp_acc_dptr. λp_acc_pc.
    225     λp_ext_indirect_dptr. λp_indirect_dptr. λp_carry. λp_bit_addr.
    226     λp_n_bit_addr. λp_relative.
    227       ∀addr. ∀p: is_in … v addr.
     232      ∀addr: addressing_mode. ∀p: is_in m fixed_v addr.
    228233        Q addr (
    229         match addr return λx: addressing_mode. is_in … v x → T with 
     234        match addr return λx: addressing_mode. is_in … fixed_v x → T with 
    230235        [ ADDR11 x          ⇒ p_addr11 x
    231236        | ADDR16 x          ⇒ p_addr16 x
     
    249254        ] p)
    250255  | VCons n' hd tl ⇒ λm_refl. λv_refl.
    251     λp_addr11. λp_addr16: (∀w: Word. is_in n v (ADDR16 w)            → T).
    252     λp_direct. λp_indirect. λp_ext_indirect. λp_acc_a. λp_register. λp_acc_b.
    253     λp_dptr. λp_data. λp_data16. λp_acc_dptr. λp_acc_pc. λp_ext_indirect_dptr.
    254     λp_indirect_dptr. λp_carry. λp_bit_addr. λp_n_bit_addr. λp_relative.
    255     let tail_call ≝ subaddressing_mode_elim_type T n' tl Q (? p_addr11)
    256       (? p_addr16) (? p_direct) (? p_indirect) (? p_ext_indirect) (? p_acc_a)
    257         (? p_register) (? p_acc_b) (? p_dptr) (? p_data) (? p_data16) (? p_acc_dptr)
    258           (? p_acc_pc) (? p_ext_indirect_dptr) (? p_indirect_dptr) (? p_carry)
    259             (? p_bit_addr) (? p_n_bit_addr) (? p_relative)
     256    let tail_call ≝ subaddressing_mode_elim_type T m fixed_v Q p_addr11
     257      p_addr16 p_direct p_indirect p_ext_indirect p_acc_a
     258        p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr
     259          p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry
     260            p_bit_addr p_n_bit_addr p_relative n' tl ?
    260261    in
    261262    match hd return λa: addressing_mode_tag. a = hd → ? with
     
    281282    ] (refl … hd)
    282283  ] (refl … n) (refl_jmeq … v).
    283   try (#_ #w1 try #w2)
    284284  [20:
    285     destruct @p_addr11 try assumption
    286     @is_in_tail_to_is_in_cons_hd_tl assumption
    287   |21:
    288     destruct @p_addr16 try assumption
    289     @is_in_tail_to_is_in_cons_hd_tl assumption
    290   |22:
    291     destruct @p_direct try assumption
    292     @is_in_tail_to_is_in_cons_hd_tl assumption
    293   |23:
    294     destruct @p_indirect try assumption
    295     @is_in_tail_to_is_in_cons_hd_tl assumption
    296   |24:
    297     destruct @p_ext_indirect try assumption
    298     @is_in_tail_to_is_in_cons_hd_tl assumption
    299   |25:
    300     destruct @p_acc_a try assumption
    301     @is_in_tail_to_is_in_cons_hd_tl assumption
    302   |26:
    303     destruct @p_register try assumption
    304     @is_in_tail_to_is_in_cons_hd_tl assumption
    305   |27:
    306     destruct @p_acc_b try assumption
    307     @is_in_tail_to_is_in_cons_hd_tl assumption
    308   |28:
    309     destruct @p_dptr try assumption
    310     @is_in_tail_to_is_in_cons_hd_tl assumption
    311   |29:
    312     destruct @p_data try assumption
    313     @is_in_tail_to_is_in_cons_hd_tl assumption
    314   |30:
    315     destruct @p_data16 try assumption
    316     @is_in_tail_to_is_in_cons_hd_tl assumption
    317   |31:
    318     destruct @p_acc_dptr try assumption
    319     @is_in_tail_to_is_in_cons_hd_tl assumption
    320   |32:
    321     destruct @p_acc_pc try assumption
    322     @is_in_tail_to_is_in_cons_hd_tl assumption
    323   |33:
    324     destruct @p_ext_indirect_dptr try assumption
    325     @is_in_tail_to_is_in_cons_hd_tl assumption
    326   |34:
    327     destruct @p_indirect_dptr try assumption
    328     @is_in_tail_to_is_in_cons_hd_tl assumption
    329   |35:
    330     destruct @p_carry try assumption
    331     @is_in_tail_to_is_in_cons_hd_tl assumption
    332   |36:
    333     destruct @p_bit_addr try assumption
    334     @is_in_tail_to_is_in_cons_hd_tl assumption
    335   |37:
    336     destruct @p_n_bit_addr try assumption
    337     @is_in_tail_to_is_in_cons_hd_tl assumption
    338   |38:
    339     destruct @p_relative try assumption
    340     @is_in_tail_to_is_in_cons_hd_tl assumption
    341   |*:
    342     -tail_call destruct @I
    343  ]
     285    generalize in match proof; destruct
     286    whd in match (subvector_with … eq_a (hd:::tl) fixed_v);
     287    cases (mem … eq_a m fixed_v hd) normalize nodelta
     288    [1:
     289      whd in match (subvector_with … eq_a tl fixed_v);
     290      #assm assumption
     291    |2:
     292      normalize in ⊢ (% → ?);
     293      #absurd cases absurd
     294    ]
     295  ]
     296  @(is_in_subvector_is_in_supervector n m v fixed_v … proof)
     297  destruct @I
    344298qed.
    345299
    346 axiom subaddressing_mode_elim:
     300lemma subaddressing_mode_elim':
    347301  ∀T: Type[2].
    348   ∀n: nat.
    349   ∀v: Vector addressing_mode_tag n.
     302  ∀m: nat.
     303  ∀fixed_v: Vector addressing_mode_tag m.
    350304  ∀Q: addressing_mode → T → Prop.
    351305  ∀P1,P2,P3,P4,P5,P6,P7,P8,P9,P10,P11,P12,P13,P14,P15,P16,P17,P18,P19.
    352     subaddressing_mode_elim_type T n v Q P1 P2 P3 P4 P5 P6 P7
    353       P8 P9 P10 P11 P12 P13 P14 P15 P16 P17 P18 P19.
     306  ∀n: nat.
     307 
     308  ∀v: Vector addressing_mode_tag n.
     309  ∀proof.
     310    subaddressing_mode_elim_type T m fixed_v Q P1 P2 P3 P4 P5 P6 P7
     311      P8 P9 P10 P11 P12 P13 P14 P15 P16 P17 P18 P19 n v proof.
     312  #T #m #fixed_v #Q #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 #n #v
     313  elim v
     314  [ #proof normalize
     315   
     316qed.
    354317
    355318(*
     
    454417    cases FETCH normalize nodelta
    455418    cases instr normalize nodelta
    456     @(subaddressing_mode_elim Prop 1 [[ addr11 ]]) try //
    457     [2: normalize // #new_addr
     419    @(subaddressing_mode_elim … [[ addr11 ]]) #new_addr
     420    cases (split … 8 8 program_counter') #pc_bu #pc_bl normalize nodelta
     421    cases (split … 3 8 new_addr) #thr #eig normalize nodelta
     422    cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta
     423    #assm cases assm #ignore
     424    whd in match good_program_counter; normalize nodelta * #n * *
     425    #program_counter_eq' #program_counter_lt_total_program_size
     426    #fetch_n_leq_program_counter'
     427    @(transitive_le
     428      total_program_size
     429      ((S program_size') + nat_of_bitvector … program_counter)
     430      (program_size' + nat_of_bitvector … program_counter') recursive_case)
     431    whd in ⊢ (?%?);
     432    change with (
     433      program_size' + (nat_of_bitvector … program_counter) <
     434        program_size' + (nat_of_bitvector … program_counter'))
     435    @lt_n_o_to_plus_m_n_lt_plus_m_o
     436    >(fetch_program_counter_n_technical code_memory program_counter
     437      program_counter' instruction ticks n)
     438    /2 by pair_destruct_2/
     439  |7:
     440    generalize in match good_program_witness;
     441    whd in match good_program; normalize nodelta
     442    cases FETCH normalize nodelta
     443    cases instr normalize nodelta
     444    @(subaddressing_mode_elim … [[ acc_dptr; acc_pc ]]) #new_addr
    458445    cases (split … 8 8 program_counter') #pc_bu #pc_bl normalize nodelta
    459446    cases (split … 3 8 new_addr) #thr #eig normalize nodelta
Note: See TracChangeset for help on using the changeset viewer.