Changeset 1503


Ignore:
Timestamp:
Nov 9, 2011, 11:14:26 AM (8 years ago)
Author:
mulligan
Message:

inductive type complete

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CostsProof.ma

    r1502 r1503  
    3939    cost.
    4040
     41definition next_instruction_properly_relates_program_counters ≝
     42  λbefore: Status.
     43  λafter : Status.
     44  let size ≝ size_of_next_instruction before in
     45  let pc_before ≝ program_counter … before in
     46  let pc_after ≝ program_counter … after in
     47  let 〈carry, sum〉 ≝ half_add … pc_before (bitvector_of_nat … size) in
     48    sum = pc_after.
     49
    4150definition next_instruction ≝
    4251  λs: Status.
     
    6776              trace_label_return cost_labels status_initial status_end_fun_call
    6877with trace_label_label_pre: trace_ends_with_ret → Status → Status → Type[0] ≝
    69   | tllp_final_not_return:
     78  | tllp_base_not_return:
    7079      ∀status: Status.
    7180        next_instruction status ≠ (RealInstruction … (RET [[relative]])) →
     
    7382        lookup_opt … (program_counter … (execute 1 status)) cost_labels = None … →
    7483          trace_label_label_pre cost_labels doesnt_end_with_ret status status
    75   | tllp_final_return:
     84  | tllp_base_return:
    7685      ∀status: Status.
    7786         next_instruction status = (RealInstruction … (RET [[relative]])) →
    7887           trace_label_label_pre cost_labels ends_with_ret status status
    79   | tllp_final_jump:
     88  | tllp_base_jump:
    8089      ∀status: Status.
    8190      ∀cost_label: Byte.
     
    8392        lookup_opt … (program_counter … (execute 1 status)) cost_labels = Some … cost_label →
    8493          trace_label_label_pre cost_labels doesnt_end_with_ret status status
    85   | tllp_call:
     94  | tllp_step_call:
    8695      ∀end_flag: trace_ends_with_ret.
    8796      ∀status_pre_fun_call: Status.
     
    9099      ∀status_after_fun_call: Status.
    91100      ∀status_final: Status.
    92       ∀fun_call_trace: trace_label_return cost_labels end_flag status_start_fun_call status_end_fun_call.
    93         trace_label_label_pre cost_labels end_flag
    94  | call:
    95     ∀b.∀bf.∀s.∀s'.∀s''. ∀trace:trace_label_return s s'.∀af.
    96      trace_label_label0 b af s'' →
    97      fetch bf = Call … →
    98      pc af = pc bf + (size_of bf (program_counter … bf)) →
    99       execute 1 bf = s →
    100       execute 1 s' = af →
    101        trace_label_label0 b bf s''
     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
    102119with trace_label_label: trace_ends_with_ret → Status → Status → Type[0] ≝
    103120  | tll_base:
     
    108125        next_instruction_is_labelled start_status →
    109126        trace_label_label cost_labels ends_flag start_status end_status.
    110  | other:
    111     ∀b.∀hd.∀s.∀s'.
    112      trace_label_label0 b s s' →
    113      fetch hd ≠ Call … →
    114      fetch s ≠ Cost … →
    115      fetch hd ≠ Ret … ≠ JmpA →
    116      execute 1 hd = s →
    117       trace_label_label0 b hd s'
    118127
    119128definition compute_simple_path0 (s:Status) (is_labelled s) (well_balanced s) (labelled_p p): trace_lab_ret ≝ ….
Note: See TracChangeset for help on using the changeset viewer.