Changeset 1502 for src/ASM/CostsProof.ma


Ignore:
Timestamp:
Nov 8, 2011, 5:26:59 PM (8 years ago)
Author:
mulligan
Message:

changes to inductive defn

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CostsProof.ma

    r1501 r1502  
    33include "ASM/Status.ma".
    44
    5 inductive trace_lab_ret: Type[0] ≝
    6    sing: ∀p. trace_lab_lab true p → structured_trace
    7  | cons:
    8     ∀p. trace_lab_lab false p → ∀tr:trace_lab_ret.
    9      execute 1 (last p) = hd tr →
    10       structured_trace
     5definition is_jump_p ≝
     6  λs.
     7  match s with
     8  [ AJMP _ ⇒ True
     9  | LJMP _ ⇒ True
     10  | SJMP _ ⇒ True
     11  | JMP _ ⇒ True
     12  | RealInstruction ri ⇒
     13    match ri with
     14    [ JZ _ ⇒ True
     15    | JNZ _ ⇒ True
     16    | JC _ ⇒ True
     17    | JNC _ ⇒ True
     18    | JB _ _ ⇒ True
     19    | JNB _ _ ⇒ True
     20    | JBC _ _ ⇒ True
     21    | CJNE _ _ ⇒ True
     22    | DJNZ _ _ ⇒ True
     23    | _ ⇒ False
     24    ]
     25  | _ ⇒ False
     26  ].
    1127
    12 with trace_lab_lab0: bool → Type[0] ≝ (* true = ends with ret *)
    13    final:
    14     ∀hd.
     28definition is_call_p ≝
     29  λs.
     30  match s with
     31  [ ACALL _ ⇒ True
     32  | LCALL _ ⇒ True
     33  | _ ⇒ False
     34  ].
     35
     36definition size_of_next_instruction ≝
     37  λs: Status.
     38  let 〈ignore, ignore, cost〉 ≝ fetch (code_memory … s) (program_counter … s) in
     39    cost.
     40
     41definition next_instruction ≝
     42  λs: Status.
     43  let 〈instruction, ignore, ignore〉 ≝ fetch (code_memory … s) (program_counter … s) in
     44    instruction.
     45
     46inductive trace_ends_with_ret: Type[0] ≝
     47  | ends_with_ret: trace_ends_with_ret
     48  | doesnt_end_with_ret: trace_ends_with_ret.
     49
     50axiom next_instruction_is_labelled:
     51  ∀s: Status. Prop.
     52
     53inductive trace_label_return (cost_labels: BitVectorTrie Byte 16): Status → Status → Type[0] ≝
     54  | tlr_base:
     55      ∀status_before: Status.
     56      ∀status_after: Status.
     57        trace_label_label cost_labels ends_with_ret status_before status_after →
     58        trace_label_return cost_labels status_before status_after
     59  | tlr_step:
     60      ∀status_initial: Status.
     61      ∀status_pre_fun_call: Status.
     62        trace_label_label cost_labels doesnt_end_with_ret status_initial status_pre_fun_call →
     63          ∀status_start_fun_call: Status.
     64          ∀status_end_fun_call: Status.
     65          ∀fun_call_trace: trace_label_return cost_labels status_start_fun_call status_end_fun_call.
     66            execute 1 status_pre_fun_call = status_start_fun_call →
     67              trace_label_return cost_labels status_initial status_end_fun_call
     68with trace_label_label_pre: trace_ends_with_ret → Status → Status → Type[0] ≝
     69  | tllp_final_not_return:
     70      ∀status: Status.
     71        next_instruction status ≠ (RealInstruction … (RET [[relative]])) →
     72        ¬ (is_jump_p (next_instruction status)) →
     73        lookup_opt … (program_counter … (execute 1 status)) cost_labels = None … →
     74          trace_label_label_pre cost_labels doesnt_end_with_ret status status
     75  | tllp_final_return:
     76      ∀status: Status.
     77         next_instruction status = (RealInstruction … (RET [[relative]])) →
     78           trace_label_label_pre cost_labels ends_with_ret status status
     79  | tllp_final_jump:
     80      ∀status: Status.
     81      ∀cost_label: Byte.
     82        is_jump_p (next_instruction status) →
     83        lookup_opt … (program_counter … (execute 1 status)) cost_labels = Some … cost_label →
     84          trace_label_label_pre cost_labels doesnt_end_with_ret status status
     85  | tllp_call:
     86      ∀end_flag: trace_ends_with_ret.
     87      ∀status_pre_fun_call: Status.
     88      ∀status_start_fun_call: Status.
     89      ∀status_end_fun_call: Status.
     90      ∀status_after_fun_call: Status.
     91      ∀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''
     102with trace_label_label: trace_ends_with_ret → Status → Status → Type[0] ≝
     103  | tll_base:
     104      ∀ends_flag: trace_ends_with_ret.
     105      ∀start_status: Status.
     106      ∀end_status: Status.
     107        trace_label_label_pre cost_labels ends_flag start_status end_status →
     108        next_instruction_is_labelled start_status →
     109        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 … →
    15115     fetch hd ≠ Ret … ≠ JmpA →
    16      fetch (execute 1 hd) = Cost … →
    17       trace_lab_lab0 false
    18  | final_ret:
    19     ∀hd.
    20      fetch hd = Ret … → trace_lab_lab0 true
    21  | final_jmp:
    22     ∀hd.
    23      fetch hd = JmpA … →
    24       fetch (execute 1 hd) = Cost … →
    25        trace_lab_lab0 false
    26  | call:
    27     ∀b.∀bf.∀trace:trace_lab_ret.∀af,tl.
    28      trace_lab_lab0 b tl →
    29      fetch bf = Call … →
    30      pc af = pc bf + 2 →
    31       execute 1 bf = hd trace →
    32       execute 1 (last trace) = af →
    33        trace_lab_lab
    34  | other:
    35     ∀b.∀hd,tl.
    36      trace_lab_lab0 b tl →
    37      fetch hd ≠ Call … →
    38      fetch (execute 1 hd) ≠ Cost … →
    39      fetch hd ≠ Ret … ≠ JmpA →
    40       simple_path_0
    41 
    42 with trace_lab_lab: bool → Type[0] ≝
    43  mk_trace_lab_lab: ∀b.∀p:trace_lab_lab0 b → is_labelled (hd p) → trace_lab_lab b.
     116     execute 1 hd = s →
     117      trace_label_label0 b hd s'
    44118
    45119definition 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.