Changeset 1692 for src/ASM/CostsProof.ma


Ignore:
Timestamp:
Feb 14, 2012, 1:18:25 PM (8 years ago)
Author:
mulligan
Message:

resolved conflict in asm costs this morning

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CostsProof.ma

    r1658 r1692  
    1313
    1414definition current_instruction ≝
    15   λs: Status.
    16     current_instruction0 (code_memory … s) (program_counter … s).
     15  λcm.
     16  λs: Status cm.
     17    current_instruction0 cm (program_counter … s).
    1718
    1819definition ASM_classify0: instruction → status_class ≝
     
    4243   ].
    4344
    44 definition ASM_classify: Status → status_class ≝
    45   λs: Status.
    46     ASM_classify0 (current_instruction s).
     45definition ASM_classify: ∀cm. Status cm → status_class ≝
     46  λcm.
     47  λs: Status cm.
     48    ASM_classify0 (current_instruction cm s).
    4749
    4850definition current_instruction_is_labelled ≝
     51  λcm.
    4952  λcost_labels: BitVectorTrie costlabel 16.
    50   λs: Status.
    51   let pc ≝ program_counter s in
     53  λs: Status cm.
     54  let pc ≝ program_counter ? cm s in
    5255    match lookup_opt … pc cost_labels with
    5356    [ None ⇒ False
     
    5659
    5760definition next_instruction_properly_relates_program_counters ≝
    58   λbefore: Status.
    59   λafter : Status.
    60   let size ≝ current_instruction_cost before in
    61   let pc_before ≝ program_counter … before in
    62   let pc_after ≝ program_counter … after in
     61  λcm.
     62  λbefore: Status cm.
     63  λafter : Status cm.
     64  let size ≝ current_instruction_cost cm before in
     65  let pc_before ≝ program_counter … cm before in
     66  let pc_after ≝ program_counter … cm after in
    6367  let sum ≝ \snd (half_add … pc_before (bitvector_of_nat … size)) in
    6468    sum = pc_after.
    6569
    66 definition ASM_abstract_status: BitVectorTrie costlabel 16 → abstract_status ≝
    67  λcost_labels.
     70definition ASM_abstract_status: ∀cm. BitVectorTrie costlabel 16 → abstract_status ≝
     71  λcm.
     72  λcost_labels.
    6873  mk_abstract_status
    69    Status
    70    (λs,s'. (execute_1 s) = s')
    71    (λs,class. ASM_classify s = class)
    72    (current_instruction_is_labelled cost_labels)
    73    next_instruction_properly_relates_program_counters.
     74   (Status cm)
     75   (λs,s'. (execute_1 cm s) = s')
     76   (λs,class. ASM_classify cm s = class)
     77   (current_instruction_is_labelled cm cost_labels)
     78   (next_instruction_properly_relates_program_counters cm).
    7479
    7580let rec compute_max_trace_label_label_cost
     81  (cm: ?)
    7682  (cost_labels: BitVectorTrie costlabel 16)
    7783   (trace_ends_flag: trace_ends_with_ret)
    78     (start_status: Status) (final_status: Status)
    79       (the_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag
     84    (start_status: Status cm) (final_status: Status cm)
     85      (the_trace: trace_label_label (ASM_abstract_status cm cost_labels) trace_ends_flag
    8086        start_status final_status) on the_trace: nat ≝
    8187  match the_trace with
     
    8490  ]
    8591and compute_max_trace_any_label_cost
     92  (cm: ?)
    8693  (cost_labels: BitVectorTrie costlabel 16)
    8794  (trace_ends_flag: trace_ends_with_ret)
    88    (start_status: Status) (final_status: Status)
    89      (the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status)
     95   (start_status: Status cm) (final_status: Status cm)
     96     (the_trace: trace_any_label (ASM_abstract_status cm cost_labels) trace_ends_flag start_status final_status)
    9097       on the_trace: nat ≝
    9198  match the_trace with
    9299  [ tal_base_not_return the_status _ _ _ _ ⇒ current_instruction_cost the_status
    93100  | tal_base_return the_status _ _ _ ⇒ current_instruction_cost the_status
     101  | tal_base_call pre_fun_call start_fun_call final _ _ _ call_trace _ ⇒
     102      let current_instruction_cost ≝ current_instruction_cost cm pre_fun_call in
     103      let call_trace_cost ≝ compute_max_trace_label_return_cost … call_trace in
     104        call_trace_cost + current_instruction_cost
    94105  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
    95      _ _ _ call_trace final_trace ⇒
    96       let current_instruction_cost ≝ current_instruction_cost pre_fun_call in
     106     _ _ _ call_trace _ final_trace ⇒
     107      let current_instruction_cost ≝ current_instruction_cost cm pre_fun_call in
    97108      let call_trace_cost ≝ compute_max_trace_label_return_cost … call_trace in
    98109      let final_trace_cost ≝ compute_max_trace_any_label_cost cost_labels end_flag … final_trace in
    99110        call_trace_cost + current_instruction_cost + final_trace_cost
    100111  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
    101       let current_instruction_cost ≝ current_instruction_cost status_pre in
     112      let current_instruction_cost ≝ current_instruction_cost cm status_pre in
    102113      let tail_trace_cost ≝
    103114       compute_max_trace_any_label_cost cost_labels end_flag
     
    107118  ]
    108119and compute_max_trace_label_return_cost
    109   (cost_labels: BitVectorTrie costlabel 16)
    110   (start_status: Status) (final_status: Status)
    111     (the_trace: trace_label_return (ASM_abstract_status cost_labels) start_status final_status)
     120  (cm: ?)
     121  (cost_labels: BitVectorTrie costlabel 16)
     122  (start_status: Status cm) (final_status: Status cm)
     123    (the_trace: trace_label_return (ASM_abstract_status cm cost_labels) start_status final_status)
    112124      on the_trace: nat ≝
    113125  match the_trace with
     
    575587qed.
    576588   
    577 
    578589let rec block_cost_trace_any_label_static_dynamic_ok
    579590  (total_program_size: nat) (cost_labels: BitVectorTrie costlabel 16)
Note: See TracChangeset for help on using the changeset viewer.