Changeset 1909 for src/ASM/ASMCosts.ma


Ignore:
Timestamp:
Apr 27, 2012, 10:59:03 AM (8 years ago)
Author:
mulligan
Message:

Ported new statements to remainder of Interpret.ma file.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r1907 r1909  
    110110  cases other
    111111qed.
    112        
    113 lemma is_a_decidable:
    114   ∀hd.
    115   ∀element.
    116     is_a hd element = true ∨ is_a hd element = false.
    117   #hd #element //
    118 qed.
    119 
    120 lemma mem_decidable:
    121   ∀n: nat.
    122   ∀v: Vector addressing_mode_tag n.
    123   ∀element: addressing_mode_tag.
    124     mem … eq_a n v element = true ∨
    125       mem … eq_a … v element = false.
    126   #n #v #element //
    127 qed.
    128 
    129 lemma eq_a_elim:
    130   ∀tag.
    131   ∀hd.
    132   ∀P: bool → Prop.
    133     (tag = hd → P (true)) →
    134       (tag ≠ hd → P (false)) →
    135         P (eq_a tag hd).
    136   #tag #hd #P
    137   cases tag
    138   cases hd
    139   #true_hyp #false_hyp
    140   try @false_hyp
    141   try @true_hyp
    142   try %
    143   #absurd destruct(absurd)
    144 qed.
    145  
    146 lemma is_a_true_to_is_in:
    147   ∀n: nat.
    148   ∀x: addressing_mode.
    149   ∀tag: addressing_mode_tag.
    150   ∀supervector: Vector addressing_mode_tag n.
    151   mem addressing_mode_tag eq_a n supervector tag →
    152     is_a tag x = true →
    153       is_in … supervector x.
    154   #n #x #tag #supervector
    155   elim supervector
    156   [1:
    157     #absurd cases absurd
    158   |2:
    159     #n' #hd #tl #inductive_hypothesis
    160     whd in match (mem … eq_a (S n') (hd:::tl) tag);
    161     @eq_a_elim normalize nodelta
    162     [1:
    163       #tag_hd_eq #irrelevant
    164       whd in match (is_in (S n') (hd:::tl) x);
    165       <tag_hd_eq #is_a_hyp >is_a_hyp normalize nodelta
    166       @I
    167     |2:
    168       #tag_hd_neq
    169       whd in match (is_in (S n') (hd:::tl) x);
    170       change with (
    171         mem … eq_a n' tl tag)
    172           in match (fold_right … n' ? false tl);
    173       #mem_hyp #is_a_hyp
    174       cases(is_a hd x)
    175       [1:
    176         normalize nodelta //
    177       |2:
    178         normalize nodelta
    179         @inductive_hypothesis assumption
    180       ]
    181     ]
    182   ]
    183 qed.
    184 
    185 lemma is_in_subvector_is_in_supervector:
    186   ∀m, n: nat.
    187   ∀subvector: Vector addressing_mode_tag m.
    188   ∀supervector: Vector addressing_mode_tag n.
    189   ∀element: addressing_mode.
    190     subvector_with … eq_a subvector supervector →
    191       is_in m subvector element → is_in n supervector element.
    192   #m #n #subvector #supervector #element
    193   elim subvector
    194   [1:
    195     #subvector_with_proof #is_in_proof
    196     cases is_in_proof
    197   |2:
    198     #n' #hd' #tl' #inductive_hypothesis #subvector_with_proof
    199     whd in match (is_in … (hd':::tl') element);
    200     cases (is_a_decidable hd' element)
    201     [1:
    202       #is_a_true >is_a_true
    203       #irrelevant
    204       whd in match (subvector_with … eq_a (hd':::tl') supervector) in subvector_with_proof;
    205       @(is_a_true_to_is_in … is_a_true)
    206       lapply(subvector_with_proof)
    207       cases(mem … eq_a n supervector hd') //
    208     |2:
    209       #is_a_false >is_a_false normalize nodelta
    210       #assm
    211       @inductive_hypothesis
    212       [1:
    213         generalize in match subvector_with_proof;
    214         whd in match (subvector_with … eq_a (hd':::tl') supervector);
    215         cases(mem_decidable n supervector hd')
    216         [1:
    217           #mem_true >mem_true normalize nodelta
    218           #assm assumption
    219         |2:
    220           #mem_false >mem_false #absurd
    221           cases absurd
    222         ]
    223       |2:
    224         assumption
    225       ]
    226     ]
    227   ]
    228 qed.
    229 
    230 let rec member_addressing_mode_tag
    231   (n: nat) (v: Vector addressing_mode_tag n) (a: addressing_mode_tag)
    232     on v: Prop ≝
    233   match v with
    234   [ VEmpty ⇒ False
    235   | VCons n' hd tl ⇒
    236       bool_to_Prop (eq_a hd a) ∨ member_addressing_mode_tag n' tl a
    237   ].
    238  
    239 let rec subaddressing_mode_elim_type
    240   (T: Type[2]) (m: nat) (fixed_v: Vector addressing_mode_tag m)
    241     (Q: addressing_mode → T → Prop)
    242       (p_addr11:            ∀w: Word11.      is_in m fixed_v (ADDR11 w)        → T)
    243       (p_addr16:            ∀w: Word.        is_in m fixed_v (ADDR16 w)        → T)
    244       (p_direct:            ∀w: Byte.        is_in m fixed_v (DIRECT w)        → T)
    245       (p_indirect:          ∀w: Bit.         is_in m fixed_v (INDIRECT w)      → T)
    246       (p_ext_indirect:      ∀w: Bit.         is_in m fixed_v (EXT_INDIRECT w)  → T)
    247       (p_acc_a:                              is_in m fixed_v ACC_A             → T)
    248       (p_register:          ∀w: BitVector 3. is_in m fixed_v (REGISTER w)      → T)
    249       (p_acc_b:                              is_in m fixed_v ACC_B             → T)
    250       (p_dptr:                               is_in m fixed_v DPTR              → T)
    251       (p_data:              ∀w: Byte.        is_in m fixed_v (DATA w)          → T)
    252       (p_data16:            ∀w: Word.        is_in m fixed_v (DATA16 w)        → T)
    253       (p_acc_dptr:                           is_in m fixed_v ACC_DPTR          → T)
    254       (p_acc_pc:                             is_in m fixed_v ACC_PC            → T)
    255       (p_ext_indirect_dptr:                  is_in m fixed_v EXT_INDIRECT_DPTR → T)
    256       (p_indirect_dptr:                      is_in m fixed_v INDIRECT_DPTR     → T)
    257       (p_carry:                              is_in m fixed_v CARRY             → T)
    258       (p_bit_addr:          ∀w: Byte.        is_in m fixed_v (BIT_ADDR w)      → T)
    259       (p_n_bit_addr:        ∀w: Byte.        is_in m fixed_v (N_BIT_ADDR w)    → T)
    260       (p_relative:          ∀w: Byte.        is_in m fixed_v (RELATIVE w)      → T)
    261         (n: nat) (v: Vector addressing_mode_tag n) (proof: subvector_with … eq_a v fixed_v)
    262       on v: Prop ≝
    263   match v return λo: nat. λv': Vector addressing_mode_tag o. o = n → v ≃ v' → ? with
    264   [ VEmpty         ⇒ λm_refl. λv_refl.
    265       ∀addr: addressing_mode. ∀p: is_in m fixed_v addr.
    266         Q addr (
    267         match addr return λx: addressing_mode. is_in … fixed_v x → T with 
    268         [ ADDR11 x          ⇒ p_addr11 x
    269         | ADDR16 x          ⇒ p_addr16 x
    270         | DIRECT x          ⇒ p_direct x
    271         | INDIRECT x        ⇒ p_indirect x
    272         | EXT_INDIRECT x    ⇒ p_ext_indirect x
    273         | ACC_A             ⇒ p_acc_a
    274         | REGISTER x        ⇒ p_register x
    275         | ACC_B             ⇒ p_acc_b
    276         | DPTR              ⇒ p_dptr
    277         | DATA x            ⇒ p_data x
    278         | DATA16 x          ⇒ p_data16 x
    279         | ACC_DPTR          ⇒ p_acc_dptr
    280         | ACC_PC            ⇒ p_acc_pc
    281         | EXT_INDIRECT_DPTR ⇒ p_ext_indirect_dptr
    282         | INDIRECT_DPTR     ⇒ p_indirect_dptr
    283         | CARRY             ⇒ p_carry
    284         | BIT_ADDR x        ⇒ p_bit_addr x
    285         | N_BIT_ADDR x      ⇒ p_n_bit_addr x
    286         | RELATIVE x        ⇒ p_relative x
    287         ] p)
    288   | VCons n' hd tl ⇒ λm_refl. λv_refl.
    289     let tail_call ≝ subaddressing_mode_elim_type T m fixed_v Q p_addr11
    290       p_addr16 p_direct p_indirect p_ext_indirect p_acc_a
    291         p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr
    292           p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry
    293             p_bit_addr p_n_bit_addr p_relative n' tl ?
    294     in
    295     match hd return λa: addressing_mode_tag. a = hd → ? with
    296     [ addr11            ⇒ λhd_refl. (∀w. Q (ADDR11 w) (p_addr11 w ?)) → tail_call
    297     | addr16            ⇒ λhd_refl. (∀w. Q (ADDR16 w) (p_addr16 w ?)) → tail_call
    298     | direct            ⇒ λhd_refl. (∀w. Q (DIRECT w) (p_direct w ?)) → tail_call
    299     | indirect          ⇒ λhd_refl. (∀w. Q (INDIRECT w) (p_indirect w ?)) → tail_call
    300     | ext_indirect      ⇒ λhd_refl. (∀w. Q (EXT_INDIRECT w) (p_ext_indirect w ?)) → tail_call
    301     | acc_a             ⇒ λhd_refl. (Q ACC_A (p_acc_a ?)) → tail_call
    302     | registr           ⇒ λhd_refl. (∀w. Q (REGISTER w) (p_register w ?)) → tail_call
    303     | acc_b             ⇒ λhd_refl. (Q ACC_A (p_acc_b ?)) → tail_call
    304     | dptr              ⇒ λhd_refl. (Q DPTR (p_dptr ?)) → tail_call
    305     | data              ⇒ λhd_refl. (∀w. Q (DATA w) (p_data w ?)) → tail_call
    306     | data16            ⇒ λhd_refl. (∀w. Q (DATA16 w) (p_data16 w ?)) → tail_call
    307     | acc_dptr          ⇒ λhd_refl. (Q ACC_DPTR (p_acc_dptr ?)) → tail_call
    308     | acc_pc            ⇒ λhd_refl. (Q ACC_PC (p_acc_pc ?)) → tail_call
    309     | ext_indirect_dptr ⇒ λhd_refl. (Q EXT_INDIRECT_DPTR (p_ext_indirect_dptr ?)) → tail_call
    310     | indirect_dptr     ⇒ λhd_refl. (Q INDIRECT_DPTR (p_indirect_dptr ?)) → tail_call
    311     | carry             ⇒ λhd_refl. (Q CARRY (p_carry ?)) → tail_call
    312     | bit_addr          ⇒ λhd_refl. (∀w. Q (BIT_ADDR w) (p_bit_addr w ?)) → tail_call
    313     | n_bit_addr        ⇒ λhd_refl. (∀w. Q (N_BIT_ADDR w) (p_n_bit_addr w ?)) → tail_call
    314     | relative          ⇒ λhd_refl. (∀w. Q (RELATIVE w) (p_relative w ?)) → tail_call
    315     ] (refl … hd)
    316   ] (refl … n) (refl_jmeq … v).
    317   [20:
    318     generalize in match proof; destruct
    319     whd in match (subvector_with … eq_a (hd:::tl) fixed_v);
    320     cases (mem … eq_a m fixed_v hd) normalize nodelta
    321     [1:
    322       whd in match (subvector_with … eq_a tl fixed_v);
    323       #assm assumption
    324     |2:
    325       normalize in ⊢ (% → ?);
    326       #absurd cases absurd
    327     ]
    328   ]
    329   @(is_in_subvector_is_in_supervector … proof)
    330   destruct @I
    331 qed.
    332 
    333 (* XXX: todo *)
    334 lemma subaddressing_mode_elim':
    335   ∀T: Type[2].
    336   ∀n: nat.
    337   ∀o: nat.
    338   ∀v1: Vector addressing_mode_tag n.
    339   ∀v2: Vector addressing_mode_tag o.
    340   ∀Q: addressing_mode → T → Prop.
    341   ∀fixed_v: Vector addressing_mode_tag (n + o).
    342   ∀P1,P2,P3,P4,P5,P6,P7,P8,P9,P10,P11,P12,P13,P14,P15,P16,P17,P18,P19.
    343   ∀fixed_v_proof: fixed_v = v1 @@ v2.
    344   ∀subaddressing_mode_proof.
    345     subaddressing_mode_elim_type T (n + o) fixed_v Q P1 P2 P3 P4 P5 P6 P7
    346       P8 P9 P10 P11 P12 P13 P14 P15 P16 P17 P18 P19 (n + o) (v1 @@ v2) subaddressing_mode_proof.
    347   #T #n #o #v1 #v2
    348   elim v1 cases v2
    349   [1:
    350     #Q #fixed_v #P1 #P2 #P3 #P4 #P5 #P6 #P7 #P8 #P9 #P10
    351     #P11 #P12 #P13 #P14 #P15 #P16 #P17 #P18 #P19 #fixed_v_proof
    352     #subaddressing_mode_proof destruct normalize
    353     #addr #absurd cases absurd
    354   |2:
    355     #n' #hd #tl #Q #fixed_v #P1 #P2 #P3 #P4 #P5 #P6 #P7 #P8 #P9 #P10
    356     #P11 #P12 #P13 #P14 #P15 #P16 #P17 #P18 #P19 #fixed_v_proof
    357     destruct normalize in match ([[]]@@hd:::tl);
    358   ]
    359   cases daemon
    360 qed.
    361 
    362 (* XXX: todo *)
    363 lemma subaddressing_mode_elim:
    364   ∀T: Type[2].
    365   ∀m: nat.
    366   ∀n: nat.
    367   ∀Q: addressing_mode → T → Prop.
    368   ∀fixed_v: Vector addressing_mode_tag m.
    369   ∀P1,P2,P3,P4,P5,P6,P7,P8,P9,P10,P11,P12,P13,P14,P15,P16,P17,P18,P19.
    370   ∀v: Vector addressing_mode_tag n.
    371   ∀proof.
    372     subaddressing_mode_elim_type T m fixed_v Q P1 P2 P3 P4 P5 P6 P7
    373       P8 P9 P10 P11 P12 P13 P14 P15 P16 P17 P18 P19 n v proof.
    374   #T #m #n #Q #fixed_v
    375   elim fixed_v
    376   [1:
    377     #P1 #P2 #P3 #P4 #P5 #P6 #P7 #P8 #P9 #P10 #P11 #P12 #P13
    378     #P14 #P15 #P16 #P17 #P18 #P19 #v #proof
    379     normalize
    380   |2:
    381   ]
    382   cases daemon
    383 qed.
    384112
    385113definition current_instruction_is_labelled ≝
     
    496224qed.
    497225
     226(*
    498227(* XXX: indexing bug *)
    499228lemma fetch_twice_fetch_execute_1:
     
    508237  * #_ #classify_assm' @classify_assm' assumption
    509238qed-.
     239*)
    510240
    511241lemma reachable_program_counter_to_0_lt_total_program_size:
     
    685415  whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
    686416  <FETCH in classifier_assm; >classify_assm #absurd destruct(absurd)
    687 qed.
     417qed. *)
    688418
    689419lemma trace_compute_paid_trace_cl_jump:
     
    998728        | ACALL addr     ⇒ λinstr.
    999729            ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ?
    1000         | AJMP  addr     ⇒ λinstr. ticks
     730        | AJMP  addr     ⇒ λinstr.
     731            ticks + block_cost' code_memory' ? program_size' total_program_size cost_labels ? good_program_witness false ?
    1001732        | LCALL addr     ⇒ λinstr.
    1002733            ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ?
Note: See TracChangeset for help on using the changeset viewer.