Changeset 1506 for src/ASM/CostsProof.ma


Ignore:
Timestamp:
Nov 15, 2011, 10:05:43 AM (8 years ago)
Author:
mulligan
Message:

changes to costs proof over weekend

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CostsProof.ma

    r1503 r1506  
    3434  ].
    3535
    36 definition size_of_next_instruction ≝
     36definition next_instruction ≝
     37  λs: Status.
     38  let 〈instruction, ignore, ignore〉 ≝ fetch (code_memory … s) (program_counter … s) in
     39    instruction.
     40
     41inductive trace_ends_with_ret: Type[0] ≝
     42  | ends_with_ret: trace_ends_with_ret
     43  | doesnt_end_with_ret: trace_ends_with_ret.
     44
     45definition next_instruction_is_labelled ≝
     46  λcost_labels: BitVectorTrie Byte 16.
     47  λs: Status.
     48  let pc ≝ program_counter … (execute 1 s) in
     49    match lookup_opt … pc cost_labels with
     50    [ None ⇒ False
     51    | _    ⇒ True
     52    ].
     53
     54definition current_instruction_cost ≝
    3755  λs: Status.
    3856  let 〈ignore, ignore, cost〉 ≝ fetch (code_memory … s) (program_counter … s) in
     
    4260  λbefore: Status.
    4361  λafter : Status.
    44   let size ≝ size_of_next_instruction before in
     62  let size ≝ current_instruction_cost before in
    4563  let pc_before ≝ program_counter … before in
    4664  let pc_after ≝ program_counter … after in
     
    4866    sum = pc_after.
    4967
    50 definition next_instruction ≝
     68definition current_instruction ≝
    5169  λs: Status.
    52   let 〈instruction, ignore, ignore〉 ≝ fetch (code_memory … s) (program_counter … s) in
     70  let pc ≝ program_counter … s in
     71  let 〈instruction, new_pc, cost〉 ≝ fetch … (code_memory … s) pc in
    5372    instruction.
    5473
    55 inductive trace_ends_with_ret: Type[0] ≝
    56   | ends_with_ret: trace_ends_with_ret
    57   | doesnt_end_with_ret: trace_ends_with_ret.
    58 
    59 axiom next_instruction_is_labelled:
    60   ∀s: Status. Prop.
     74definition current_instruction_is_labelled ≝
     75  λcost_labels: BitVectorTrie Byte 16.
     76  λs: Status.
     77  let pc ≝ program_counter … s in
     78    match lookup_opt … pc cost_labels with
     79    [ None ⇒ False
     80    | _    ⇒ True
     81    ].
    6182
    6283inductive trace_label_return (cost_labels: BitVectorTrie Byte 16): Status → Status → Type[0] ≝
     
    6889  | tlr_step:
    6990      ∀status_initial: Status.
    70       ∀status_pre_fun_call: Status.
    71         trace_label_label cost_labels doesnt_end_with_ret status_initial status_pre_fun_call →
    72           ∀status_start_fun_call: Status.
    73           ∀status_end_fun_call: Status.
    74           ∀fun_call_trace: trace_label_return cost_labels status_start_fun_call status_end_fun_call.
    75             execute 1 status_pre_fun_call = status_start_fun_call →
    76               trace_label_return cost_labels status_initial status_end_fun_call
    77 with trace_label_label_pre: trace_ends_with_ret → Status → Status → Type[0] ≝
    78   | tllp_base_not_return:
    79       ∀status: Status.
    80         next_instruction status ≠ (RealInstruction … (RET [[relative]])) →
    81         ¬ (is_jump_p (next_instruction status)) →
    82         lookup_opt … (program_counter … (execute 1 status)) cost_labels = None … →
    83           trace_label_label_pre cost_labels doesnt_end_with_ret status status
    84   | tllp_base_return:
    85       ∀status: Status.
    86          next_instruction status = (RealInstruction … (RET [[relative]])) →
    87            trace_label_label_pre cost_labels ends_with_ret status status
    88   | tllp_base_jump:
    89       ∀status: Status.
    90       ∀cost_label: Byte.
    91         is_jump_p (next_instruction status) →
    92         lookup_opt … (program_counter … (execute 1 status)) cost_labels = Some … cost_label →
    93           trace_label_label_pre cost_labels doesnt_end_with_ret status status
    94   | tllp_step_call:
    95       ∀end_flag: trace_ends_with_ret.
    96       ∀status_pre_fun_call: Status.
    97       ∀status_start_fun_call: Status.
    98       ∀status_end_fun_call: Status.
    99       ∀status_after_fun_call: Status.
     91      ∀status_labelled: Status.
    10092      ∀status_final: Status.
    101       ∀fun_call_trace: trace_label_return cost_labels status_start_fun_call status_end_fun_call.
    102         is_call_p (next_instruction status_pre_fun_call) →
    103         next_instruction_properly_relates_program_counters status_pre_fun_call status_after_fun_call →
    104         execute 1 status_pre_fun_call = status_start_fun_call →
    105         execute 1 status_end_fun_call = status_after_fun_call →
    106         trace_label_label_pre cost_labels end_flag status_after_fun_call status_final →
    107         trace_label_label_pre cost_labels end_flag status_pre_fun_call status_final
    108   | tllp_step_default:
    109       ∀end_flag: trace_ends_with_ret.
    110       ∀status_pre: Status.
    111       ∀status_init: Status.
    112       ∀status_end: Status.
    113         trace_label_label_pre cost_labels end_flag status_init status_end →
    114         ¬ (is_call_p (next_instruction status_pre)) →
    115         ¬ (is_jump_p (next_instruction status_pre)) →
    116         (next_instruction status_pre) ≠ (RealInstruction … (RET [[relative]])) →
    117         lookup_opt … (program_counter … status_init) cost_labels = None … →
    118           trace_label_label_pre cost_labels end_flag status_pre status_end
     93          trace_label_label cost_labels doesnt_end_with_ret status_initial status_labelled →
     94            trace_label_return cost_labels status_labelled status_final →
     95              trace_label_return cost_labels status_initial status_final
    11996with trace_label_label: trace_ends_with_ret → Status → Status → Type[0] ≝
    12097  | tll_base:
     
    123100      ∀end_status: Status.
    124101        trace_label_label_pre cost_labels ends_flag start_status end_status →
    125         next_instruction_is_labelled start_status →
    126         trace_label_label cost_labels ends_flag start_status end_status.
    127 
     102        current_instruction_is_labelled cost_labels start_status →
     103        trace_label_label cost_labels ends_flag start_status end_status
     104with trace_label_label_pre: trace_ends_with_ret → Status → Status → Type[0] ≝
     105  | tllp_base_not_return:
     106      ∀start_status: Status.
     107        let final_status ≝ execute 1 start_status in
     108        current_instruction start_status ≠ (RealInstruction … (RET [[relative]])) →
     109        ¬ (is_jump_p (current_instruction start_status)) →
     110        current_instruction_is_labelled cost_labels final_status →
     111          trace_label_label_pre cost_labels doesnt_end_with_ret start_status final_status
     112  | tllp_base_return:
     113      ∀start_status: Status.
     114        let final_status ≝ execute 1 start_status in
     115          current_instruction start_status = (RealInstruction … (RET [[relative]])) →
     116            trace_label_label_pre cost_labels ends_with_ret start_status final_status
     117  | tllp_base_jump:
     118      ∀start_status: Status.
     119        let final_status ≝ execute 1 start_status in
     120          is_jump_p (current_instruction start_status) →
     121            current_instruction_is_labelled cost_labels final_status →
     122              trace_label_label_pre cost_labels doesnt_end_with_ret start_status final_status
     123  | tllp_step_call:
     124      ∀end_flag: trace_ends_with_ret.
     125      ∀status_pre_fun_call: Status.
     126      ∀status_after_fun_call: Status.
     127      ∀status_final: Status.
     128        let status_start_fun_call ≝ execute 1 status_pre_fun_call in
     129          is_call_p (current_instruction status_pre_fun_call) →
     130          next_instruction_properly_relates_program_counters status_pre_fun_call status_after_fun_call →
     131          trace_label_return cost_labels status_start_fun_call status_after_fun_call →
     132          trace_label_label_pre cost_labels end_flag status_after_fun_call status_final →
     133            trace_label_label_pre cost_labels end_flag status_pre_fun_call status_final
     134  | tllp_step_default:
     135      ∀end_flag: trace_ends_with_ret.
     136      ∀status_pre: Status.
     137      ∀status_end: Status.
     138        let status_init ≝ execute 1 status_pre in
     139          trace_label_label_pre cost_labels end_flag status_init status_end →
     140          ¬ (is_call_p (current_instruction status_pre)) →
     141          ¬ (is_jump_p (current_instruction status_pre)) →
     142          (current_instruction status_pre) ≠ (RealInstruction … (RET [[relative]])) →
     143          ¬ (current_instruction_is_labelled cost_labels status_init) →
     144            trace_label_label_pre cost_labels end_flag status_pre status_end.
     145
     146(* XXX: to do later
    128147definition compute_simple_path0 (s:Status) (is_labelled s) (well_balanced s) (labelled_p p): trace_lab_ret ≝ ….
    129148
     
    136155      τ = cost_trace p)
    137156  ].
    138 
    139 let rec trace_lab_rec_cost (p: trace_lab_ret) : nat. COUNTS EVERYTHING
     157*)
     158
     159let rec compute_max_trace_label_label_cost
     160  (cost_labels: BitVectorTrie Byte 16) (trace_ends_flag: trace_ends_with_ret)
     161    (start_status: Status) (final_status: Status)
     162      (the_trace: trace_label_label cost_labels trace_ends_flag start_status final_status)
     163        on the_trace: nat ≝
     164  match the_trace with
     165  [ tll_base ends_flag initial final given_trace labelled_proof ⇒
     166      compute_max_trace_label_label_pre_cost … given_trace
     167  ]
     168and compute_max_trace_label_label_pre_cost
     169  (cost_labels: BitVectorTrie Byte 16) (trace_ends_flag: trace_ends_with_ret)
     170    (start_status: Status) (final_status: Status)
     171      (the_trace: trace_label_label_pre cost_labels trace_ends_flag start_status final_status)
     172        on the_trace: nat ≝
     173  match the_trace with
     174  [ tllp_base_not_return the_status not_return not_jump not_cost_label ⇒
     175      current_instruction_cost the_status
     176  | tllp_base_return the_status is_return ⇒ current_instruction_cost the_status
     177  | tllp_base_jump the_status is_jump is_cost ⇒
     178      current_instruction_cost the_status
     179  | tllp_step_call end_flag pre_fun_call after_fun_call final is_call
     180        next_intruction_coherence call_trace final_trace ⇒
     181      let current_instruction_cost ≝ current_instruction_cost pre_fun_call in
     182      let call_trace_cost ≝ compute_max_trace_label_return_cost cost_labels … call_trace in
     183      let final_trace_cost ≝ compute_max_trace_label_label_pre_cost cost_labels end_flag after_fun_call final final_trace in
     184        call_trace_cost + current_instruction_cost + final_trace_cost
     185  | tllp_step_default end_flag status_pre status_end tail_trace is_not_call
     186        is_not_jump is_not_ret is_not_labelled ⇒
     187      let current_instruction_cost ≝ current_instruction_cost status_pre in
     188      let tail_trace_cost ≝ compute_max_trace_label_label_pre_cost cost_labels end_flag (execute 1 status_pre) status_end tail_trace in
     189        current_instruction_cost + tail_trace_cost
     190  ]
     191and compute_max_trace_label_return_cost
     192  (cost_labels: BitVectorTrie Byte 16) (start_status: Status) (final_status: Status)
     193    (the_trace: trace_label_return cost_labels start_status final_status)
     194      on the_trace: nat ≝
     195  match the_trace with
     196  [ tlr_base before after trace_to_lift ⇒ compute_max_trace_label_label_cost … trace_to_lift
     197  | tlr_step initial labelled final labelled_trace ret_trace ⇒
     198      let labelled_cost ≝ compute_max_trace_label_label_cost … labelled_trace in
     199      let return_cost ≝ compute_max_trace_label_return_cost … ret_trace in
     200        labelled_cost + return_cost
     201  ].
     202
     203lemma pred_minus_1:
     204  ∀m, n: nat.
     205  ∀proof: n < m.
     206    pred (m - n) = m - n - 1.
     207  #m #n
     208  elim m
     209  [ #proof
     210    cases(lt_to_not_zero … proof)
     211  | #m' #ind_hyp #proof
     212    normalize in ⊢ (???%)
     213    cases n
     214    [ normalize //
     215    | #n' normalize
     216      <ind_hyp
     217  | #m' #ind_hyp
     218    normalize
     219    cases n
     220    [ normalize //
     221    | #n' normalize
     222
     223lemma plus_minus_rearrangement:
     224  ∀m, n, o: nat.
     225  ∀proof_n_m: n < m.
     226  ∀proof_m_o: m < o.
     227    (m - n) + (o - m) = o - n.
     228  #m #n #o
     229  elim m
     230  [1: #proof_n_m
     231      cases(lt_to_not_zero … proof_n_m)
     232  |2: #m' #ind_hyp
     233      #proof_n_m' #proof_m_o
     234      >minus_Sn_m
     235      [2: normalize in proof_n_m';
     236          @le_S_S_to_le
     237          assumption
     238      |1: >eq_minus_S_pred
     239          [2: /2/
     240          |3: normalize
     241              normalize in proof_n_m';
     242              elim(le_S … proof_n_m')
     243              @le_S
     244          |1:
     245          ]
     246
     247lemma status_execution_progresses_processor_clock:
     248  ∀s: Status.
     249    clock … s ≤ clock … (execute 1 s).
     250  #status
     251  cases status
     252  #ignore1 #ignore2 #ignore3 #ignore4 #ignore5 #ignore6 #ignore7 #ignore8
     253  #ignore9 #clock
     254 
     255
     256let rec compute_max_trace_label_label_cost_is_ok
     257  (cost_labels: BitVectorTrie Byte 16) (trace_ends_flag: trace_ends_with_ret)
     258    (start_status: Status) (final_status: Status)
     259      (the_trace: trace_label_label cost_labels trace_ends_flag start_status final_status)
     260      on the_trace:
     261        compute_max_trace_label_label_cost cost_labels trace_ends_flag start_status final_status the_trace =
     262          (clock … final_status) - (clock … start_status) ≝ ?
     263and compute_max_trace_label_label_pre_cost_is_ok
     264  (cost_labels: BitVectorTrie Byte 16) (trace_ends_flag: trace_ends_with_ret)
     265    (start_status: Status) (final_status: Status)
     266      (the_trace: trace_label_label_pre cost_labels trace_ends_flag start_status final_status)
     267        on the_trace:
     268          compute_max_trace_label_label_pre_cost cost_labels trace_ends_flag start_status final_status the_trace =
     269            (clock … final_status) - (clock … start_status) ≝ ?
     270and compute_max_trace_label_return_cost_is_ok
     271  (cost_labels: BitVectorTrie Byte 16) (start_status: Status) (final_status: Status)
     272    (the_trace: trace_label_return cost_labels start_status final_status)
     273      on the_trace:
     274        compute_max_trace_label_return_cost cost_labels start_status final_status the_trace =
     275          (clock … final_status) - (clock … start_status) ≝ ?.
     276  [1:
     277    cases the_trace
     278    #ends_flag #start_status #end_status #label_label_pre_trace
     279    #labelled_proof
     280    normalize
     281    @compute_max_trace_label_label_pre_cost_is_ok
     282  |3:
     283    cases the_trace
     284    [1:
     285      #status_before #status_after #trace_to_lift
     286      @compute_max_trace_label_label_cost_is_ok
     287    |2:
     288      #status_initial #status_labelled #status_final #labelled_trace #return_trace
     289      >compute_max_trace_label_return_cost_is_ok %
     290    ]
     291  |2: cases the_trace
     292    [1: #the_status #not_return #not_jump #not_cost
     293    |2: #the_status #is_return
     294    |3: #the_status #is_jump #is_cost
     295    |4: #end_flag #pre_fun_call #after_fun_call #final #is_call
     296        #next_intruction_coherence #call_trace #final_trace
     297    |5: #end_flag #status_pre #status_end #tail_trace #is_not_call
     298        #is_not_jump #is_not_ret #is_not_labelled
     299        @current_instruction_cost
     300    ]
     301  ]
     302qed.
     303       
     304let rec compute_max_trace_label_ret_cost_is_ok
     305  (cost_labels: BitVectorTrie Byte 16) (start_status: Status) (final_status: Status)
     306    (the_trace: trace_label_return cost_labels start_status final_status)
     307      on the_trace:
     308        compute_max_trace_label_ret_cost cost_labels start_status final_status the_trace =
     309        (clock … final_status) - (clock … start_status) ≝
     310  match the_trace with
     311  [ tlr_base before after trace_to_lift ⇒ ?
     312  | tlr_step initial pre_fun_call pre_fun_call_trace start_fun_call end_fun_call
     313      fun_call_trace pre_start_fun_call_coherence ⇒ ?
     314  ]
     315and compute_max_trace_label_label_pre_cost_is_ok
     316  (cost_labels: BitVectorTrie Byte 16) (ends_flag: trace_ends_with_ret)
     317    (start_status: Status) (final_status: Status)
     318      (the_trace: trace_label_label_pre cost_labels ends_flag start_status final_status)
     319        on the_trace:
     320          compute_max_trace_label_label_pre_cost cost_labels ends_flag start_status final_status the_trace =
     321            (clock … final_status) - (clock … start_status) ≝
     322  match the_trace with
     323  [ tllp_base_not_return the_status not_return not_jump not_cost_label ⇒ ?
     324  | tllp_base_return the_status is_return ⇒ ?
     325  | tllp_base_jump the_status cost_label is_jump is_cost ⇒ ?
     326  | tllp_step_call end_flag pre_fun_call start_fun_call end_fun_call after_fun_call final
     327      fun_call_trace is_call statuses_related pre_start_fun_call_coherence
     328      end_after_fun_call_coherence after_fun_call_trace ⇒ ?
     329  | tllp_step_default end_flag start initial end initial_end_trace not_call
     330      not_jump not_return not_cost ⇒ ?
     331  ]
     332and compute_max_trace_label_label_cost_is_ok
     333  (cost_labels: BitVectorTrie Byte 16) (ends_flag: trace_ends_with_ret)
     334    (start_status: Status) (final_status: Status)
     335      (the_trace: trace_label_label cost_labels ends_flag start_status final_status)
     336        on the_trace:
     337          compute_max_trace_label_label_cost cost_labels ends_flag start_status final_status the_trace =
     338            (clock … final_status) - (clock … start_status) ≝
     339  match the_trace with
     340  [ tll_base ends_flag initial final given_trace labelled_proof ⇒ ?
     341  ].
     342  [8: @(compute_max_trace_label_label_pre_cost_is_ok cost_labels ends_flag initial final given_trace)
     343  |1: @(compute_max_trace_label_label_cost_is_ok cost_labels ends_with_ret before after trace_to_lift)
     344  |4: normalize
     345      @minus_n_n
     346  |3: normalize
     347      @minus_n_n
     348  |5: normalize
     349      @minus_n_n
     350  |6: letin fun_call_cost_ok ≝ (compute_max_trace_label_ret_cost_is_ok cost_labels start_fun_call end_fun_call fun_call_trace)
     351      letin the_trace_cost_ok ≝ (compute_max_trace_label_label_pre_cost_is_ok cost_labels ends_flag start_status final_status the_trace)
     352  |*:
     353  ]
     354qed.
     355 
     356lemma compute_max_trace_label_ret_cost_is_ok:
     357  ∀cost_labels: BitVectorTrie Byte 16.
     358  ∀start_status: Status.
     359  ∀final_status: Status.
     360  ∀the_trace: trace_label_return cost_labels start_status final_status.
     361    compute_max_trace_label_ret_cost cost_labels start_status final_status the_trace =
     362      (clock … final_status) - (clock … start_status).
     363  #COST_LABELS #START_STATUS #FINAL_STATUS #THE_TRACE
     364  elim THE_TRACE
    140365
    141366lemma trace_lab_rec_cost_ok:
Note: See TracChangeset for help on using the changeset viewer.