Changeset 1650 for src/ASM/ASMCosts.ma


Ignore:
Timestamp:
Jan 19, 2012, 4:56:17 PM (8 years ago)
Author:
mulligan
Message:

changes over the last couple of days: stuck due to matita producing terms so large that the program cannot print them out!

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r1648 r1650  
    106106  cases other
    107107qed.
    108 
    109 lemma is_in_tl_to_is_in_cons_hd_tl:
    110   ∀n: nat.
    111   ∀the_vect: Vector addressing_mode_tag n.
    112   ∀h: addressing_mode_tag.
    113   ∀element: addressing_mode.
    114     is_in n the_vect element → is_in (S n) (h:::the_vect) element.
    115   #n #the_vect #h #element #assm
    116   normalize cases (is_a h element) normalize nodelta
    117   //
    118 qed.
    119 
    120 lemma is_in_singleton_to_is_a:
    121   ∀tag.
    122   ∀element.
    123     is_in … [[tag]] element → is_a tag element.
    124   #tag #element
    125   normalize in ⊢ (% → ?);
    126   cases (is_a tag element)
    127   [1:
    128     normalize nodelta #irrelevant
    129     @I
    130   |2:
    131     normalize nodelta #absurd
    132     cases absurd
    133   ]
    134 qed.
    135108       
    136109lemma is_a_decidable:
     
    150123qed.
    151124
    152 (*
    153 lemma is_in_cons_hd_tl_to_is_in_tl:
     125lemma eq_a_elim:
     126  ∀tag.
     127  ∀hd.
     128  ∀P: bool → Prop.
     129    (tag = hd → P (true)) →
     130      (tag ≠ hd → P (false)) →
     131        P (eq_a tag hd).
     132  #tag #hd #P
     133  cases tag
     134  cases hd
     135  #true_hyp #false_hyp
     136  try @false_hyp
     137  try @true_hyp
     138  try %
     139  #absurd destruct(absurd)
     140qed.
     141 
     142lemma is_a_true_to_is_in:
    154143  ∀n: nat.
    155   ∀the_vect: Vector addressing_mode_tag n.
    156   ∀h: addressing_mode_tag.
    157   ∀element: addressing_mode.
    158     is_in (S n) (h:::the_vect) element →
    159       is_in n the_vect element. *)
     144  ∀x: addressing_mode.
     145  ∀tag: addressing_mode_tag.
     146  ∀supervector: Vector addressing_mode_tag n.
     147  mem addressing_mode_tag eq_a n supervector tag →
     148    is_a tag x = true →
     149      is_in … supervector x.
     150  #n #x #tag #supervector
     151  elim supervector
     152  [1:
     153    #absurd cases absurd
     154  |2:
     155    #n' #hd #tl #inductive_hypothesis
     156    whd in match (mem … eq_a (S n') (hd:::tl) tag);
     157    @eq_a_elim normalize nodelta
     158    [1:
     159      #tag_hd_eq #irrelevant
     160      whd in match (is_in (S n') (hd:::tl) x);
     161      <tag_hd_eq #is_a_hyp >is_a_hyp normalize nodelta
     162      @I
     163    |2:
     164      #tag_hd_neq
     165      whd in match (is_in (S n') (hd:::tl) x);
     166      change with (
     167        mem … eq_a n' tl tag)
     168          in match (fold_right … n' ? false tl);
     169      #mem_hyp #is_a_hyp
     170      cases(is_a hd x)
     171      [1:
     172        normalize nodelta //
     173      |2:
     174        normalize nodelta
     175        @inductive_hypothesis assumption
     176      ]
     177    ]
     178  ]
     179qed.
    160180
    161181lemma is_in_subvector_is_in_supervector:
     
    166186    subvector_with … eq_a subvector supervector →
    167187      is_in m subvector element → is_in n supervector element.
    168   (*
    169188  #m #n #subvector #supervector #element
    170189  elim subvector
     
    173192    cases is_in_proof
    174193  |2:
    175     #n #hd #tl #inductive_hypothesis
    176     cases supervector
     194    #n' #hd' #tl' #inductive_hypothesis #subvector_with_proof
     195    whd in match (is_in … (hd':::tl') element);
     196    cases (is_a_decidable hd' element)
    177197    [1:
    178       #subvector_with_proof #is_in_proof
    179       cases subvector_with_proof
    180     |2:
    181       #n' #hd' #tl' #subvector_with_proof #is_in_proof
    182       whd in match (is_in … (hd':::tl') element);
    183       cases (is_a_decidable hd' element)
    184       [1:
    185         #is_a_true >is_a_true normalize nodelta
    186         @I
    187       |2:
    188         #is_a_false >is_a_false normalize nodelta
    189         @inductive_hypothesis'
    190         [2:
    191           assumption
    192         |1:
    193         ]
    194       ]     
    195     ]
    196   ]
    197 qed.
    198   |3:
    199     #n #hd #tl #inductive_hypothesis
    200     #subvector_with_proof #is_in_proof
    201     @inductive_hypothesis
    202     [1:
    203       assumption
    204   |4:
    205   ]
    206 qed.
    207  
    208  
    209  
    210   [1:
    211     #n #supervector #subvector_proof #is_in_proof
    212     cases is_in_proof
    213   |2:
    214     #m' #hd #tl #inductive_hypothesis #n' #supervector
    215     #subvector_proof #is_in_proof
    216     generalize in match is_in_proof;
    217     cases(is_a_decidable hd element)
    218     whd in match (is_in … (hd:::tl) element);
    219     [1:
    220       #is_a_true >is_a_true normalize nodelta
     198      #is_a_true >is_a_true
    221199      #irrelevant
     200      whd in match (subvector_with … eq_a (hd':::tl') supervector) in subvector_with_proof;
     201      @(is_a_true_to_is_in … is_a_true)
     202      lapply(subvector_with_proof)
     203      cases(mem … eq_a n supervector hd') //
    222204    |2:
    223205      #is_a_false >is_a_false normalize nodelta
     
    225207      @inductive_hypothesis
    226208      [1:
    227         generalize in match subvector_proof;
    228         whd in match (subvector_with … eq_a (hd:::tl) supervector);
    229         cases(mem_decidable n' supervector hd)
     209        generalize in match subvector_with_proof;
     210        whd in match (subvector_with … eq_a (hd':::tl') supervector);
     211        cases(mem_decidable n supervector hd')
    230212        [1:
    231213          #mem_true >mem_true normalize nodelta
     
    239221      ]
    240222    ]
    241    
    242    
    243    
    244    
    245     generalize in match subvector_proof;
    246     whd in match (subvector_with … eq_a (hd:::tl) supervector);
    247     cases(mem_decidable n' supervector hd)
    248     [1:
    249       #mem_true >mem_true normalize nodelta
    250       #subvector_with_proof
    251       @inductive_hypothesis
    252       [1:
    253         assumption
    254       |2:
    255         generalize in match is_in_proof;
    256         whd in match (is_in (S m') (hd:::tl) element);
    257         cases(is_a_decidable hd element)
    258         [1:
    259           #is_a_true >is_a_true normalize nodelta
    260           #irrelevant
    261           whd whd in match (is_in … tl element);
    262         |2:
    263           #is_a_false >is_a_false normalize nodelta
    264           #assm assumption
    265         ]
    266       ]
    267     |2:
    268       #mem_false >mem_false normalize nodelta
    269       #absurd cases absurd
    270     ]
    271     |1:
    272       normalize nodelta #subvector_with_assm
    273       cases(is_a_decidable hd element)
    274       [1:
    275         #is_a_hd
    276         generalize in match subvector_proof;
    277         whd in match (subvector_with … eq_a (hd:::tl) supervector);
    278       |2:
    279         #not_is_a_hd
    280       ]
    281     ]
    282   ] *)
    283   cases daemon
     223  ]
    284224qed.
    285225
     
    417357      P8 P9 P10 P11 P12 P13 P14 P15 P16 P17 P18 P19 n v proof.
    418358
    419 (*
    420 lemma subaddressing_mode_elim:
    421   ∀T:Type[2].
    422   ∀P1: Word11 → T.
    423   ∀P2,P3,P4,P5,P6,P7,P8,P9,P10,P11,P12,P13,P14,P15,P16,P17,P18,P19: False → T.
    424   ∀addr: addressing_mode.
    425   ∀p: is_in 1 [[ addr11 ]] addr.
    426   ∀Q: addressing_mode → T → Prop.
    427     (∀w. Q (ADDR11 w) (P1 w)) →
    428       Q addr (
    429         match addr return λx:addressing_mode. (is_in 1 [[addr11]] x → T) with 
    430         [ ADDR11 (x:Word11) ⇒ λH:True. P1 x
    431         | ADDR16 _ ⇒ λH:False. P2 H
    432         | DIRECT _ ⇒ λH:False. P3 H
    433         | INDIRECT _ ⇒ λH:False. P4 H
    434         | EXT_INDIRECT _ ⇒ λH:False. P5 H
    435         | ACC_A ⇒ λH:False. P6 H
    436         | REGISTER _ ⇒ λH:False. P7 H
    437         | ACC_B ⇒ λH:False. P8 H
    438         | DPTR ⇒ λH:False. P9 H
    439         | DATA _ ⇒ λH:False. P10 H
    440         | DATA16 _ ⇒ λH:False. P11 H
    441         | ACC_DPTR ⇒ λH:False. P12 H
    442         | ACC_PC ⇒ λH:False. P13 H
    443         | EXT_INDIRECT_DPTR ⇒ λH:False. P14 H
    444         | INDIRECT_DPTR ⇒ λH:False. P15 H
    445         | CARRY ⇒ λH:False. P16 H
    446         | BIT_ADDR _ ⇒ λH:False. P17 H
    447         | N_BIT_ADDR _ ⇒ λH:False. P18 H   
    448         | RELATIVE _ ⇒ λH:False. P19 H
    449         ] p).
    450   #T #P1 #P2 #P3 #P4 #P5 #P6 #P7 #P8 #P9 #P10 #P11 #P12 #P13
    451   #P14 #P15 #P16 #P17 #P18 #P19
    452   * try #x1 try #x2 try #x3 try #x4
    453   try (@⊥ assumption) normalize @x4
    454 qed. *)
    455 
    456359include alias "arithmetics/nat.ma".
    457360
    458 let rec block_cost
     361let rec block_cost'
    459362  (code_memory: BitVectorTrie Byte 16) (program_counter: Word)
    460363    (program_size: nat) (total_program_size: nat) (cost_labels: BitVectorTrie costlabel 16)
    461364      (reachable_program_counter_witness: reachable_program_counter code_memory total_program_size program_counter)
    462         (good_program_witness: good_program code_memory total_program_size)
     365        (good_program_witness: good_program code_memory total_program_size) (first_time_around: bool)
    463366          on program_size: total_program_size ≤ program_size + nat_of_bitvector … program_counter → nat ≝
    464367  match program_size return λprogram_size: nat. total_program_size ≤ program_size + nat_of_bitvector … program_counter → nat with
     
    466369  | S program_size' ⇒ λrecursive_case.
    467370    let 〈instruction, program_counter', ticks〉 as FETCH ≝ fetch code_memory program_counter in
    468       match lookup_opt … program_counter' cost_labels return λx: option costlabel. nat with
    469       [ None   ⇒
     371    let to_continue ≝
     372      match lookup_opt … program_counter' cost_labels with
     373      [ None ⇒ true
     374      | Some _ ⇒ first_time_around
     375      ]
     376    in
     377      if to_continue then
    470378        match instruction return λx. x = instruction → ? with
    471379        [ RealInstruction real_instruction ⇒ λreal_instruction_refl.
     
    482390          | DJNZ src_trgt relative ⇒ λinstr. ticks
    483391          | _                      ⇒ λinstr.
    484               ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? good_program_witness ?
     392              ticks + block_cost' code_memory program_counter' program_size' total_program_size cost_labels ? good_program_witness false ?
    485393          ] (refl … real_instruction)
    486394        | ACALL addr     ⇒ λinstr.
    487             ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? good_program_witness ?
     395            ticks + block_cost' code_memory program_counter' program_size' total_program_size cost_labels ? good_program_witness false ?
    488396        | AJMP  addr     ⇒ λinstr. ticks
    489397        | LCALL addr     ⇒ λinstr.
    490             ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? good_program_witness ?
     398            ticks + block_cost' code_memory program_counter' program_size' total_program_size cost_labels ? good_program_witness false ?
    491399        | LJMP  addr     ⇒ λinstr. ticks
    492400        | SJMP  addr     ⇒ λinstr. ticks
    493401        | JMP   addr     ⇒ λinstr. (* XXX: actually a call due to use with fptrs *)
    494             ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? good_program_witness ?
     402            ticks + block_cost' code_memory program_counter' program_size' total_program_size cost_labels ? good_program_witness false ?
    495403        | MOVC  src trgt ⇒ λinstr.
    496             ticks + block_cost code_memory program_counter' program_size' total_program_size cost_labels ? good_program_witness ?
     404            ticks + block_cost' code_memory program_counter' program_size' total_program_size cost_labels ? good_program_witness false ?
    497405        ] (refl … instruction)
    498       | Some _ ⇒ ticks
    499       ]
     406      else
     407        0
    500408  ].
    501409  [1:
     
    635543qed.
    636544
     545definition block_cost ≝
     546  λcode_memory: BitVectorTrie Byte 16.
     547  λprogram_counter: Word.
     548  λtotal_program_size: nat.
     549  λcost_labels: BitVectorTrie costlabel 16.
     550  λreachable_program_counter_witness: reachable_program_counter code_memory total_program_size program_counter.
     551  λgood_program_witness: good_program code_memory total_program_size.
     552    block_cost' code_memory program_counter total_program_size total_program_size cost_labels
     553      reachable_program_counter_witness good_program_witness true ?.
     554  @le_plus_n_r
     555qed.
     556
    637557lemma fetch_program_counter_n_Sn:
    638558  ∀instruction: instruction.
     
    672592    [ None ⇒ λlookup_refl. cost_mapping
    673593    | Some lbl ⇒ λlookup_refl.
    674       let cost ≝ block_cost code_memory program_counter fixed_program_size fixed_program_size cost_labels ? good_program_witness ? in
     594      let cost ≝ block_cost code_memory program_counter fixed_program_size cost_labels ? good_program_witness in
    675595        add … cost_mapping lbl cost
    676596    ] (refl … (lookup_opt … program_counter cost_labels))
     
    680600    assumption
    681601  |2:
    682     //
    683   |3:
    684602    assumption
    685603  ]
Note: See TracChangeset for help on using the changeset viewer.