Changeset 2412


Ignore:
Timestamp:
Oct 22, 2012, 4:21:04 PM (7 years ago)
Author:
campbell
Message:

Tidy up measurable definition a bit more.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/correctness.ma

    r2399 r2412  
    7575λsc,x. \snd (measure_stack sc x).
    7676
    77 (* TODO: cost labels *)
    78 
    79 let rec will_return_aux (stack_cost:Clight_stack_T) (depth:nat) (current_stack:nat)
    80                         (max_stack:nat) (trace:execution_prefix) on trace : option nat ≝
     77let rec will_return_aux (depth:nat)
     78                        (trace:execution_prefix) on trace : bool ≝
    8179match trace with
    82 [ nil ⇒ match depth with [ O ⇒ Some ? max_stack | _ ⇒ None ? ]
     80[ nil ⇒ match depth with [ O ⇒ true | _ ⇒ false ]
    8381| cons h tl ⇒
    8482  let 〈tr,s〉 ≝ h in
    85   match Clight_classify s return λcl. (match cl in status_class with [_⇒?] → ?) → ?  with
    86   [ cl_call ⇒ λsc.
    87       let new_stack ≝ current_stack + sc I in
    88       will_return_aux stack_cost (S depth) new_stack (max max_stack new_stack) tl
    89   | cl_return ⇒ λsc.
     83  match Clight_classify s with
     84  [ cl_call ⇒ will_return_aux (S depth) tl
     85  | cl_return ⇒
    9086      match depth with
    91       [ O ⇒ None ?
    92       | S d ⇒ will_return_aux stack_cost d (current_stack - sc I) max_stack tl
     87      [ O ⇒ false
     88      | S d ⇒ will_return_aux d tl
    9389      ]
    94   | _ ⇒ λ_. will_return_aux stack_cost depth current_stack max_stack tl
    95   ] (stack_cost s)
     90  | _ ⇒ will_return_aux depth tl
     91  ]
    9692].
    97 definition will_return' : Clight_stack_T → nat → execution_prefix → option nat ≝
    98 λstack_cost,current_stack,trace. will_return_aux stack_cost O current_stack current_stack trace.
     93definition will_return' : execution_prefix → bool ≝ will_return_aux O.
    9994
    10095definition measurable : clight_program → nat → nat → Clight_stack_T → nat → Prop ≝
    101 λp,m,n,stack_cost,max_allowed_stack.  ∀prefix,suffix,interesting,remainder,max_stack.
     96λp,m,n,stack_cost,max_allowed_stack.  ∀prefix,suffix,interesting,remainder.
    10297  let cl_trace ≝ exec_inf … clight_fullexec p in
    10398  split_trace cl_trace m = Some ? 〈prefix,suffix〉 ∧
    10499  split_trace suffix n = Some ? 〈interesting,remainder〉 ∧
    105   trace_labelled interesting
    106   will_return' stack_cost (stack_after stack_cost prefix) interesting = Some ? max_stack
    107   max_stack < max_allowed_stack.
     100  trace_labelled interesting
     101  bool_to_Prop (will_return' interesting)
     102  max_stack stack_cost (prefix@interesting) < max_allowed_stack.
    108103
    109104(* From measurable on Clight, we will end up with an RTLabs flat trace where
Note: See TracChangeset for help on using the changeset viewer.