Changeset 1587 for src/ASM/CostsProof.ma


Ignore:
Timestamp:
Dec 5, 2011, 5:16:55 PM (8 years ago)
Author:
mulligan
Message:

changes from today, including removing indexing of problematic function in utilities/binary/positive.ma

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CostsProof.ma

    r1581 r1587  
    1 
    21include "ASM/ASMCosts.ma".
    32include "ASM/WellLabeled.ma".
    43include "ASM/Status.ma".
    54include "common/StructuredTraces.ma".
    6 
    7 (*
    8 definition next_instruction_is_labelled ≝
    9   λcost_labels: BitVectorTrie Byte 16.
    10   λs: Status.
    11   let pc ≝ program_counter … (execute_1 s) in
    12     match lookup_opt … pc cost_labels with
    13     [ None ⇒ False
    14     | _    ⇒ True
    15     ].
    16 
    17 definition current_instruction_cost ≝
    18   λs: Status. \snd (fetch (code_memory … s) (program_counter … s)).
    19 
    20 definition is_call_p ≝
    21   λs.
    22   match s with
    23   [ ACALL _ ⇒ True
    24   | LCALL _ ⇒ True
    25   | JMP ⇒ True (* XXX: is function pointer call *)
    26   | _ ⇒ False
    27   ].
    28 
    29 definition next_instruction ≝
    30   λs: Status.
    31   let 〈instruction, ignore, ignore〉 ≝ fetch (code_memory … s) (program_counter … s) in
    32     instruction.
    33 
    34 inductive trace_ends_with_ret: Type[0] ≝
    35   | ends_with_ret: trace_ends_with_ret
    36   | doesnt_end_with_ret: trace_ends_with_ret.
    37 
    38 definition next_instruction_is_labelled ≝
    39   λcost_labels: BitVectorTrie Byte 16.
    40   λs: Status.
    41   let pc ≝ program_counter … (execute 1 s) in
    42     match lookup_opt … pc cost_labels with
    43     [ None ⇒ False
    44     | _    ⇒ True
    45     ].
    46 
    47 definition next_instruction_properly_relates_program_counters ≝
    48   λbefore: Status.
    49   λafter : Status.
    50   let size ≝ current_instruction_cost before in
    51   let pc_before ≝ program_counter … before in
    52   let pc_after ≝ program_counter … after in
    53   let sum ≝ \snd (half_add … pc_before (bitvector_of_nat … size)) in
    54     sum = pc_after.
    55 
    56 definition current_instruction ≝
    57   λs: Status.
    58   let pc ≝ program_counter … s in
    59   \fst (\fst (fetch … (code_memory … s) pc)).
    60 
    61 definition current_instruction_is_labelled ≝
    62   λcost_labels: BitVectorTrie Byte 16.
    63   λs: Status.
    64   let pc ≝ program_counter … s in
    65     match lookup_opt … pc cost_labels with
    66     [ None ⇒ False
    67     | _    ⇒ True
    68     ].
    69 
    70 inductive trace_label_return (cost_labels: BitVectorTrie Byte 16): Status → Status → Type[0] ≝
    71   | tlr_base:
    72       ∀status_before: Status.
    73       ∀status_after: Status.
    74         trace_label_label cost_labels ends_with_ret status_before status_after →
    75         trace_label_return cost_labels status_before status_after
    76   | tlr_step:
    77       ∀status_initial: Status.
    78       ∀status_labelled: Status.
    79       ∀status_final: Status.
    80           trace_label_label cost_labels doesnt_end_with_ret status_initial status_labelled →
    81             trace_label_return cost_labels status_labelled status_final →
    82               trace_label_return cost_labels status_initial status_final
    83 with trace_label_label: trace_ends_with_ret → Status → Status → Type[0] ≝
    84   | tll_base:
    85       ∀ends_flag: trace_ends_with_ret.
    86       ∀start_status: Status.
    87       ∀end_status: Status.
    88         trace_label_label_pre cost_labels ends_flag start_status end_status →
    89         current_instruction_is_labelled cost_labels start_status →
    90         trace_label_label cost_labels ends_flag start_status end_status
    91 with trace_label_label_pre: trace_ends_with_ret → Status → Status → Type[0] ≝
    92   | tllp_base_not_return:
    93       ∀start_status: Status.
    94         let final_status ≝ execute 1 start_status in
    95         current_instruction start_status ≠ (RealInstruction … (RET [[relative]])) →
    96         ¬ (is_jump_p (current_instruction start_status)) →
    97         current_instruction_is_labelled cost_labels final_status →
    98           trace_label_label_pre cost_labels doesnt_end_with_ret start_status final_status
    99   | tllp_base_return:
    100       ∀start_status: Status.
    101         let final_status ≝ execute 1 start_status in
    102           current_instruction start_status = (RealInstruction … (RET [[relative]])) →
    103             trace_label_label_pre cost_labels ends_with_ret start_status final_status
    104   | tllp_base_jump:
    105       ∀start_status: Status.
    106         let final_status ≝ execute 1 start_status in
    107           is_jump_p (current_instruction start_status) →
    108             current_instruction_is_labelled cost_labels final_status →
    109               trace_label_label_pre cost_labels doesnt_end_with_ret start_status final_status
    110   | tllp_step_call:
    111       ∀end_flag: trace_ends_with_ret.
    112       ∀status_pre_fun_call: Status.
    113       ∀status_after_fun_call: Status.
    114       ∀status_final: Status.
    115         let status_start_fun_call ≝ execute 1 status_pre_fun_call in
    116           is_call_p (current_instruction status_pre_fun_call) →
    117           next_instruction_properly_relates_program_counters status_pre_fun_call status_after_fun_call →
    118           trace_label_return cost_labels status_start_fun_call status_after_fun_call →
    119           trace_label_label_pre cost_labels end_flag status_after_fun_call status_final →
    120             trace_label_label_pre cost_labels end_flag status_pre_fun_call status_final
    121   | tllp_step_default:
    122       ∀end_flag: trace_ends_with_ret.
    123       ∀status_pre: Status.
    124       ∀status_end: Status.
    125         let status_init ≝ execute 1 status_pre in
    126           trace_label_label_pre cost_labels end_flag status_init status_end →
    127           ¬ (is_call_p (current_instruction status_pre)) →
    128           ¬ (is_jump_p (current_instruction status_pre)) →
    129           (current_instruction status_pre) ≠ (RealInstruction … (RET [[relative]])) →
    130           ¬ (current_instruction_is_labelled cost_labels status_init) →
    131             trace_label_label_pre cost_labels end_flag status_pre status_end.
    132 *)
    133 
    134 (* XXX: not us
    135 definition compute_simple_path0 (s:Status) (is_labelled s) (well_balanced s) (labelled_p p): trace_lab_ret ≝ ….
    136 
    137 lemma simple_path_ok:
    138  ∀st: Status.∀H.
    139  let p ≝ compute_simple_path0 st H in
    140    ∀n.
    141     nth_path n p = execute n st ∧
    142      (execute' (path_length p) st = 〈st',τ〉 →
    143       τ = cost_trace p)
    144   ].
    145 *)
    1465
    1476let rec compute_max_trace_label_label_cost
     
    23089 /3 by lt_plus_to_minus_r, plus_minus/
    23190qed.
    232 *)
    23391
    23492lemma plus_minus_rearrangement_1:
     
    266124  #m #n #o /2 by /
    267125qed.
     126*)
    268127
    269128let rec compute_max_trace_label_label_cost_is_ok
     
    737596  i < |l1| →
    738597   tech_cost_of_label cost_labels cost_map codom_dom l2 i =
    739    tech_cost_of_label cost_labels cost_map codom_dom (l1@l2) (i+|l1|).
     598   tech_cost_of_label cost_labels cost_mnth_safe ? i ctrace H) ?ap codom_dom (l1@l2) (i+|l1|).
    740599 #cost_labels #cost_Map #codom_dom #l1 #l2 #i #H
    741600 cut (ltb i (|l2|) = ltb (i+|l1|) (|l1@l2|))
     
    794653  ]
    795654]
    796 
     655(*
    797656lemma
    798657 compute_max_trace_any_label_cost cost_label trace_ends_flag start_status
     
    873732 let p ≝ compute_simple_path0 s in
    874733  execute' (path_length p) s = 〈s',τ〉 →
    875    Timer s' - Timer s = ∑ τ cost_map.
     734   Timer s' - Timer s = ∑ τ cost_map. *)
Note: See TracChangeset for help on using the changeset viewer.