Changeset 1658


Ignore:
Timestamp:
Jan 25, 2012, 6:18:04 PM (6 years ago)
Author:
mulligan
Message:

asm costs changes from today

Location:
src
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r1650 r1658  
    357357      P8 P9 P10 P11 P12 P13 P14 P15 P16 P17 P18 P19 n v proof.
    358358
     359definition current_instruction0 ≝
     360  λcode_memory: BitVectorTrie Byte 16.
     361  λprogram_counter: Word.
     362    \fst (\fst (fetch … code_memory program_counter)).
     363
     364definition current_instruction ≝
     365  λs: Status.
     366    current_instruction0 (code_memory … s) (program_counter … s).
     367
     368definition ASM_classify0: instruction → status_class ≝
     369  λi: instruction.
     370  match i with
     371   [ RealInstruction pre ⇒
     372     match pre with
     373      [ RET ⇒ cl_return
     374      | JZ _ ⇒ cl_jump
     375      | JNZ _ ⇒ cl_jump
     376      | JC _ ⇒ cl_jump
     377      | JNC _ ⇒ cl_jump
     378      | JB _ _ ⇒ cl_jump
     379      | JNB _ _ ⇒ cl_jump
     380      | JBC _ _ ⇒ cl_jump
     381      | CJNE _ _ ⇒ cl_jump
     382      | DJNZ _ _ ⇒ cl_jump
     383      | _ ⇒ cl_other
     384      ]
     385   | ACALL _ ⇒ cl_call
     386   | LCALL _ ⇒ cl_call
     387   | JMP _ ⇒ cl_call
     388   | AJMP _ ⇒ cl_jump
     389   | LJMP _ ⇒ cl_jump
     390   | SJMP _ ⇒ cl_jump
     391   | _ ⇒ cl_other
     392   ].
     393
     394definition ASM_classify: Status → status_class ≝
     395  λs: Status.
     396    ASM_classify0 (current_instruction s).
     397
     398definition current_instruction_is_labelled ≝
     399  λcost_labels: BitVectorTrie costlabel 16.
     400  λs: Status.
     401  let pc ≝ program_counter … s in
     402    match lookup_opt … pc cost_labels with
     403    [ None ⇒ False
     404    | _    ⇒ True
     405    ].
     406
     407definition next_instruction_properly_relates_program_counters ≝
     408  λbefore: Status.
     409  λafter : Status.
     410  let size ≝ current_instruction_cost before in
     411  let pc_before ≝ program_counter … before in
     412  let pc_after ≝ program_counter … after in
     413  let sum ≝ \snd (half_add … pc_before (bitvector_of_nat … size)) in
     414    sum = pc_after.
     415
     416definition ASM_abstract_status: BitVectorTrie costlabel 16 → abstract_status ≝
     417 λcost_labels.
     418  mk_abstract_status
     419   Status
     420   (λs,s'. (execute_1 s) = s')
     421   (λs,class. ASM_classify s = class)
     422   (current_instruction_is_labelled cost_labels)
     423   next_instruction_properly_relates_program_counters.
     424
     425let rec trace_any_label_length
     426  (cost_labels: BitVectorTrie costlabel 16) (trace_ends_flag: trace_ends_with_ret)
     427    (start_status: Status) (final_status: Status)
     428      (the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status)
     429        on the_trace: nat ≝
     430  match the_trace with
     431  [ tal_base_not_return the_status _ _ _ _ ⇒ 0
     432  | tal_base_call pre_fun_call start_fun_call final _ _ _ call_trace _ ⇒ 0
     433  | tal_base_return the_status _ _ _ ⇒ 0
     434  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final _ _ _ call_trace _ final_trace ⇒
     435      let tail_length ≝ trace_any_label_length … final_trace in
     436      let pc_difference ≝ nat_of_bitvector … (program_counter … after_fun_call) - nat_of_bitvector … (program_counter … pre_fun_call) in       
     437        pc_difference + tail_length
     438  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
     439      let tail_length ≝ trace_any_label_length … tail_trace in
     440      let pc_difference ≝ nat_of_bitvector … (program_counter … status_init) - nat_of_bitvector … (program_counter … status_pre) in
     441        pc_difference + tail_length       
     442  ].
     443
     444let rec compute_paid_trace_any_label
     445  (cost_labels: BitVectorTrie costlabel 16)
     446  (trace_ends_flag: trace_ends_with_ret)
     447   (start_status: Status) (final_status: Status)
     448     (the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status)
     449       on the_trace: nat ≝
     450  match the_trace with
     451  [ tal_base_not_return the_status _ _ _ _ ⇒ current_instruction_cost the_status
     452  | tal_base_return the_status _ _ _ ⇒ current_instruction_cost the_status
     453  | tal_base_call pre_fun_call start_fun_call final _ _ _ call_trace _ ⇒ current_instruction_cost pre_fun_call
     454  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
     455     _ _ _ call_trace _ final_trace ⇒
     456      let current_instruction_cost ≝ current_instruction_cost pre_fun_call in
     457      let final_trace_cost ≝ compute_paid_trace_any_label cost_labels end_flag … final_trace in
     458        current_instruction_cost + final_trace_cost
     459  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
     460      let current_instruction_cost ≝ current_instruction_cost status_pre in
     461      let tail_trace_cost ≝
     462       compute_paid_trace_any_label cost_labels end_flag
     463        status_init status_end tail_trace
     464      in
     465        current_instruction_cost + tail_trace_cost
     466  ].
     467
     468definition compute_paid_trace_label_label ≝
     469 λcost_labels: BitVectorTrie costlabel 16.
     470  λtrace_ends_flag: trace_ends_with_ret.
     471   λstart_status: Status.
     472    λfinal_status: Status.
     473     λthe_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag
     474      start_status final_status.
     475  match the_trace with
     476  [ tll_base ends_flag initial final given_trace labelled_proof ⇒
     477      compute_paid_trace_any_label … given_trace
     478  ].
     479
    359480include alias "arithmetics/nat.ma".
     481include alias "basics/logic.ma".
     482
     483(* Bug to be fixed in the refiner! Compare the two checks
     484axiom T:Type[0].
     485axiom S:Type[0].
     486axiom k: S → T.
     487coercion k.
     488check (λf: T → nat. (f: S → nat))
     489check ((λx:T.0) : S → nat) *)
     490definition foo ≝ (match match 1 with [O ⇒ 0 | S n ⇒ S ?] : Σn:nat. n=n).
    360491
    361492let rec block_cost'
    362   (code_memory: BitVectorTrie Byte 16) (program_counter: Word)
     493  (code_memory': BitVectorTrie Byte 16) (program_counter': Word)
    363494    (program_size: nat) (total_program_size: nat) (cost_labels: BitVectorTrie costlabel 16)
    364       (reachable_program_counter_witness: reachable_program_counter code_memory total_program_size program_counter)
    365         (good_program_witness: good_program code_memory total_program_size) (first_time_around: bool)
    366           on program_size: total_program_size ≤ program_size + nat_of_bitvector … program_counter → nat ≝
    367   match program_size return λprogram_size: nat. total_program_size ≤ program_size + nat_of_bitvector … program_counter → nat with
     495      (reachable_program_counter_witness: reachable_program_counter code_memory' total_program_size program_counter')
     496        (good_program_witness: good_program code_memory' total_program_size) (first_time_around: bool)
     497          on program_size:
     498          total_program_size ≤ program_size + nat_of_bitvector … program_counter' →
     499          Σcost_of_block: nat.
     500            ∀start_status: Status.
     501            ∀final_status: Status.
     502            ∀trace_ends_flag.
     503            ∀the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status.
     504              code_memory' = code_memory … start_status →
     505                program_counter' = program_counter … start_status →
     506                    (∃n: nat. trace_any_label_length … the_trace + (S n) = total_program_size) ∧
     507                      cost_of_block = compute_paid_trace_any_label cost_labels trace_ends_flag start_status final_status the_trace ≝
     508  match program_size return λprogram_size: nat. total_program_size ≤ program_size + nat_of_bitvector … program_counter' → ? with
    368509  [ O ⇒ λbase_case. ⊥
    369510  | S program_size' ⇒ λrecursive_case.
    370     let 〈instruction, program_counter', ticks〉 as FETCH ≝ fetch code_memory program_counter in
     511    let 〈instruction, program_counter'', ticks〉 ≝ fetch code_memory' program_counter' in
    371512    let to_continue ≝
    372       match lookup_opt … program_counter' cost_labels with
     513      match lookup_opt … program_counter'' cost_labels with
    373514      [ None ⇒ true
    374515      | Some _ ⇒ first_time_around
     
    376517    in
    377518      if to_continue then
    378         match instruction return λx. x = instruction → ? with
    379         [ RealInstruction real_instruction ⇒ λreal_instruction_refl.
    380           match real_instruction return λx. x = real_instruction → ? with
    381           [ RET                    ⇒ λinstr. ticks
    382           | JC   relative          ⇒ λinstr. ticks
    383           | JNC  relative          ⇒ λinstr. ticks
    384           | JB   bit_addr relative ⇒ λinstr. ticks
    385           | JNB  bit_addr relative ⇒ λinstr. ticks
    386           | JBC  bit_addr relative ⇒ λinstr. ticks
    387           | JZ   relative          ⇒ λinstr. ticks
    388           | JNZ  relative          ⇒ λinstr. ticks
    389           | CJNE src_trgt relative ⇒ λinstr. ticks
    390           | DJNZ src_trgt relative ⇒ λinstr. ticks
    391           | _                      ⇒ λinstr.
    392               ticks + block_cost' code_memory program_counter' program_size' total_program_size cost_labels ? good_program_witness false ?
    393           ] (refl … real_instruction)
    394         | ACALL addr     ⇒ λinstr.
    395             ticks + block_cost' code_memory program_counter' program_size' total_program_size cost_labels ? good_program_witness false ?
    396         | AJMP  addr     ⇒ λinstr. ticks
    397         | LCALL addr     ⇒ λinstr.
    398             ticks + block_cost' code_memory program_counter' program_size' total_program_size cost_labels ? good_program_witness false ?
    399         | LJMP  addr     ⇒ λinstr. ticks
    400         | SJMP  addr     ⇒ λinstr. ticks
    401         | JMP   addr     ⇒ λinstr. (* XXX: actually a call due to use with fptrs *)
    402             ticks + block_cost' code_memory program_counter' program_size' total_program_size cost_labels ? good_program_witness false ?
    403         | MOVC  src trgt ⇒ λinstr.
    404             ticks + block_cost' code_memory program_counter' program_size' total_program_size cost_labels ? good_program_witness false ?
    405         ] (refl … instruction)
     519        match instruction with
     520        [ RealInstruction real_instruction ⇒
     521          match real_instruction with
     522          [ RET                    ⇒ ticks
     523          | JC   relative          ⇒ ticks
     524          | JNC  relative          ⇒ ticks
     525          | JB   bit_addr relative ⇒ ticks
     526          | JNB  bit_addr relative ⇒ ticks
     527          | JBC  bit_addr relative ⇒ ticks
     528          | JZ   relative          ⇒ ticks
     529          | JNZ  relative          ⇒ ticks
     530          | CJNE src_trgt relative ⇒ ticks
     531          | DJNZ src_trgt relative ⇒ ticks
     532          | _                      ⇒
     533              ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ?
     534          ]
     535        | ACALL addr     ⇒
     536            ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ?
     537        | AJMP  addr     ⇒ ticks
     538        | LCALL addr     ⇒
     539            ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ?
     540        | LJMP  addr     ⇒ ticks
     541        | SJMP  addr     ⇒ ticks
     542        | JMP   addr     ⇒ (* XXX: actually a call due to use with fptrs *)
     543            ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ?
     544        | MOVC  src trgt ⇒
     545            ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ?
     546        ]
    406547      else
    407548        0
    408549  ].
     550  [57:
     551  [1:
     552    cases reachable_program_counter_witness #_ #hyp
     553    @(absurd (total_program_size < total_program_size) … (not_le_Sn_n …))
     554    @(le_to_lt_to_lt … base_case hyp)
     555  |2:
     556    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
     557    lapply(good_program_witness program_counter' reachable_program_counter_witness)
     558    <FETCH normalize nodelta >instr normalize nodelta
     559    @(subaddressing_mode_elim … [[addr11]] … [[addr11]]) [1: // ] #new_addr
     560    cases (split … 8 8 program_counter'') #pc_bu #pc_bl normalize nodelta
     561    cases (split … 3 8 new_addr) #thr #eig normalize nodelta
     562    cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta * * * * #n'
     563    #_ #_ #program_counter_lt' #program_counter_lt_tps'     
     564    @(transitive_le
     565      total_program_size
     566      ((S program_size') + nat_of_bitvector … program_counter')
     567      (program_size' + nat_of_bitvector … program_counter'') recursive_case)
     568    normalize in match (S program_size' + nat_of_bitvector … program_counter');
     569    >plus_n_Sm
     570    @monotonic_le_plus_r
     571    change with (
     572      nat_of_bitvector … program_counter' <
     573        nat_of_bitvector … program_counter'')
     574    assumption
     575  |3:
     576    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
     577    lapply(good_program_witness program_counter' reachable_program_counter_witness)
     578    <FETCH normalize nodelta >instr normalize nodelta
     579    @(subaddressing_mode_elim … [[addr11]] … [[addr11]]) [1: // ] #new_addr
     580    cases (split … 8 8 program_counter'') #pc_bu #pc_bl normalize nodelta
     581    cases (split … 3 8 new_addr) #thr #eig normalize nodelta
     582    cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta * * * * #n'
     583    #_ #_ #program_counter_lt' #program_counter_lt_tps'
     584    %
     585    [1:
     586      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
     587      <FETCH normalize nodelta whd in match ltb; normalize nodelta
     588      >(le_to_leb_true … program_counter_lt') %
     589    |2:
     590      assumption
     591    ]
     592  |4:
     593  |5:
     594    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
     595    lapply(good_program_witness program_counter' reachable_program_counter_witness)
     596      <FETCH normalize nodelta >instr normalize nodelta
     597    @(subaddressing_mode_elim … [[addr16]] … [[addr16]]) [1: // ] #new_addr
     598    * * * * #n'
     599    #_ #_ #program_counter_lt' #program_counter_lt_tps'     
     600    @(transitive_le
     601      total_program_size
     602      ((S program_size') + nat_of_bitvector … program_counter')
     603      (program_size' + nat_of_bitvector … program_counter'') recursive_case)
     604    normalize in match (S program_size' + nat_of_bitvector … program_counter');
     605    >plus_n_Sm
     606    @monotonic_le_plus_r
     607    change with (
     608      nat_of_bitvector … program_counter' <
     609        nat_of_bitvector … program_counter'')
     610    assumption
     611 
     612  [1:
     613    #start_status #final_status #trace_ends_flag #the_trace #code_memory_refl #program_counter_refl
     614    cases(block_cost' ?????? ?? ?) -block_cost'
     615    #recursive_block_cost #recursive_assm
     616    @(trace_any_label_inv_ind … the_trace)
     617    [1:
     618      #start_status' #final_status' #execute_assm #classifier_assm #costed_assm
     619      #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl destruct
     620      cases classifier_assm
     621      whd in match (as_classifier ? ? ?);
     622      whd in ⊢ (??%? → ?);
     623      whd in match current_instruction; normalize nodelta
     624      whd in match current_instruction0; normalize nodelta
     625      #absurd @⊥ >p1 in absurd; normalize nodelta
     626      #absurd destruct(absurd)
     627    |2:
     628      #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_assm
     629      #start_status_refl #final_status_refl #the_trace_assm destruct
     630      whd in classifier_assm;
     631      whd in classifier_assm:(??%?);
     632      whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
     633      whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
     634      @⊥
     635      >p1 in classifier_assm; normalize nodelta
     636      #absurd destruct(absurd)
     637    |3:
     638      #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
     639      #classifier_assm #after_return_assm #trace_label_return #costed_assm
     640      #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
     641      destruct
     642      cases(recursive_assm status_pre_fun_call status_final doesnt_end_with_ret
     643        (tal_base_call (ASM_abstract_status cost_labels) status_pre_fun_call
     644          (execute_1 status_pre_fun_call) status_final
     645          (refl Status (execute_1 status_pre_fun_call)) classifier_assm
     646          after_return_assm trace_label_return costed_assm) ? ?)
     647      [2: %
     648      |3:
     649      |1:
     650      ]
     651    |4:
     652      #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
     653      #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
     654      #costed_assm #trace_any_label #trace_ends_refl #start_status_refl #final_status_refl
     655      #the_trace_refl destruct whd in ⊢ (??(???%)); whd in match (trace_any_label_length … (tal_step_call … trace_any_label));
     656    |5:
     657      #end_flag #status_pre #status_init #status_end #execute_assm #the_trace
     658      #classifier_assm #costed_assm #ends_flag_refl #start_status_refl #final_status_refl
     659      #the_trace_refl -the_trace_refl destruct
     660      whd in classifier_assm;
     661      whd in classifier_assm:(??%?);
     662      whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
     663      whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
     664      @⊥ >p1 in classifier_assm; normalize nodelta
     665      #absurd destruct(absurd)
     666    ]
     667  [1:
     668    #start_status #final_status #trace_ends_flag #the_trace
     669    #code_memory_refl #program_counter_refl
     670    cases(block_cost' ?????? ?? ?) -block_cost'
     671    #recursive_block_cost #recursive_assm
     672    @(trace_any_label_inv_ind … the_trace)
     673    [1:
     674      #start_status' #final_status' #execute_assm #not_return_assm
     675      #costed_assm #trace_ends_flag_assm #start_status_assm #final_status_assm
     676      #the_trace_assm
     677      cases daemon (* XXX: bug in notion of traces here *)
     678    |2:
     679
     680    |3:
     681      cases daemon (* XXX *)
     682    |4:
     683    ]
     684  |108:
     685    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
     686    lapply(good_program_witness program_counter' reachable_program_counter_witness)
     687    <FETCH normalize nodelta <real_instruction_refl <instr normalize nodelta *
     688    #program_counter_lt' #program_counter_lt_tps' %
     689    try assumption
     690    [*:
     691      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
     692      <FETCH normalize nodelta whd in match ltb; normalize nodelta
     693      >(le_to_leb_true … program_counter_lt') %
     694    ]
    409695  [1:
    410696    cases reachable_program_counter_witness #_ #hyp
  • src/ASM/CostsProof.ma

    r1650 r1658  
    611611        generalize in match reachable_program_counter_witness;
    612612        generalize in match good_program_witness;
    613         <trace_length_hyp in ⊢ (∀_:?. ∀_:?. ??(???%??????)?); (*
     613        <trace_length_hyp in ⊢ (∀_:?. ∀_:?. ??(???%??????)?);
    614614        -reachable_program_counter_witness #reachable_program_counter_witness
    615615        -good_program_witness #good_program_witness
    616         whd in ⊢ (??%?); @pair_elim *)
     616        whd in ⊢ (??%?); @pair_elim
    617617      ]
    618618    |2:
  • src/common/StructuredTraces.ma

    r1654 r1658  
    11include "basics/types.ma".
    22include "basics/bool.ma".
     3include "basics/jmeq.ma".
    34
    45inductive status_class : Type[0] ≝
     
    9596          trace_any_label S end_flag status_pre status_end.
    9697
    97 
    9898coinductive trace_label_diverges (S:abstract_status) : S → Type[0] ≝
    9999  | tld_step:
Note: See TracChangeset for help on using the changeset viewer.