Changeset 2325


Ignore:
Timestamp:
Sep 7, 2012, 11:26:19 AM (7 years ago)
Author:
campbell
Message:

Fill out some Clight bits and pieces in correctness.ma.

Location:
src
Files:
1 added
1 edited

Legend:

Unmodified
Added
Removed
  • src/correctness.ma

    r2323 r2325  
    1010theorem correct :
    1111  ∀input_program.
    12 
    13   not_wrong … (exec_inf … clight_fullexec input_program) →
    1412 
    1513  ∀object_code,costlabel_map,labelled,cost_map.
    1614  compile input_program = OK ? 〈〈object_code,costlabel_map〉,labelled,cost_map〉 →
     15
     16  not_wrong … (exec_inf … clight_fullexec input_program) →
    1717 
    1818  sim_with_labels (exec_inf … clight_fullexec input_program) (exec_inf … clight_fullexec labelled)
     
    2121
    2222#input_program
    23 #NOT_WRONG
    2423#object_code #costlabel_map #labelled #cost_map
    2524#COMPILE
     25#NOT_WRONG
    2626cases (bind_inversion ????? COMPILE) -COMPILE * * #init_cost #labelled' #rtlabs_program * #FRONTEND #COMPILE
    2727cases (bind_inversion ????? COMPILE) -COMPILE * #object_code' #costlabel_map' * #ASSEMBLER #COMPILE
     
    3535] qed.
    3636
    37 axiom Clight_classify : state → status_class.
    38 axiom Clight_labelled : state → bool.
    39 definition Clight_stack_T ≝ ∀s:state. match Clight_classify s with [ cl_call ⇒ True | cl_return ⇒ True | _ ⇒ False ] → nat.
    4037
    41 (* [will_return depth stack max time s trace] says that there is a prefix of [trace],
    42    whose successor state is [s], which exits [depth] number of functions, starting with [stack]
    43    amount of stack space, using a maximum of [max] amount of stack space and [time]. *)
     38include "Clight/abstract.ma".
    4439
    45 inductive will_return (time_cost:state → nat) (stack_cost:Clight_stack_T) :  nat → nat → nat → nat → state → execution state io_out io_in → Prop ≝
    46 | wr_step : ∀s,tr,depth,stack,mx,tm,s',trace.
    47     Clight_classify s = cl_other ∨ Clight_classify s = cl_jump →
    48     will_return ?? depth stack mx tm s' trace →
    49     will_return ?? depth stack mx (tm + time_cost s) s' (e_step … tr s trace)
    50 | wr_call : ∀s,tr,depth,stack,mx,tm,s',trace.
    51     ∀CL:Clight_classify s = cl_call.
    52     will_return ?? (S depth) (stack + stack_cost s ?) mx tm s' trace →
    53     will_return ?? depth stack mx (tm + time_cost s) s' (e_step … tr s trace)
    54 | wr_ret : ∀s,tr,depth,stack,mx,tm,s',trace.
    55     ∀CL:Clight_classify s = cl_return.
    56     will_return ?? depth (stack - stack_cost s ?) mx tm s' trace →
    57     will_return ?? (S depth) stack (max mx stack) (tm + time_cost s) s' (e_step … tr s trace)
    58 (*    will_return ?? depth stack mx tm s' trace →
    59     let prev_stack ≝ (stack + stack_cost s ?) in
    60     will_return ?? (S depth) prev_stack (max mx prev_stack) (tm + time_cost s) s' (e_step … tr s trace)*)
    61     (* Note that we require the ability to make a step after the return (this
    62        corresponds to somewhere that will be guaranteed to be a label at the
    63        end of the compilation chain). *)
    64 | wr_base : ∀base_stack,s,tr,trace.
    65     will_return ?? O base_stack base_stack O s (e_step … tr s trace)
    66 . >CL @I qed.
     40definition Clight_stack_T ≝ ∀s:Clight_state. match Clight_classify s with [ cl_call ⇒ True | cl_return ⇒ True | _ ⇒ False ] → nat.
    6741
    68 (* [nth_state_of_with_stack state stack_cost stack_bound exec n] returns [Some s] iff after
    69    [n] steps of [exec] we have reached [s] without exceeding the [stack_bound]
    70    according to the [stack_cost] function. *)
    71 axiom nth_state_of_with_stack : ∀state. (state → nat) → nat → execution state io_out io_in → nat → option state.
    72 axiom nth_state_of : ∀state. execution state io_out io_in → nat → option state.
     42definition execution_prefix : Type[0] ≝ list (trace × Clight_state).
     43axiom split_trace : execution Clight_state io_out io_in → nat → option (execution_prefix × (execution Clight_state io_out io_in)).
     44axiom stack_after : execution_prefix → nat.
    7345
    74 definition execution_prefix : Type[0] ≝ list (trace × state).
    75 axiom split_trace : execution state io_out io_in → nat → option (execution_prefix × (execution state io_out io_in)).
    76 axiom stack_after : execution_prefix → nat.
    77 axiom will_return' : Clight_stack_T → nat → nat → execution_prefix → option nat.
     46(* TODO: cost labels *)
     47
     48let rec will_return_aux (stack_cost:Clight_stack_T) (depth:nat) (current_stack:nat)
     49                        (max_stack:nat) (trace:execution_prefix) on trace : option nat ≝
     50match trace with
     51[ nil ⇒ match depth with [ O ⇒ Some ? max_stack | _ ⇒ None ? ]
     52| cons h tl ⇒
     53  let 〈tr,s〉 ≝ h in
     54  match Clight_classify s return λcl. (match cl in status_class with [_⇒?] → ?) → ?  with
     55  [ cl_call ⇒ λsc.
     56      let new_stack ≝ current_stack + sc I in
     57      will_return_aux stack_cost (S depth) new_stack (max max_stack new_stack) tl
     58  | cl_return ⇒ λsc.
     59      match depth with
     60      [ O ⇒ None ?
     61      | S d ⇒ will_return_aux stack_cost d (current_stack - sc I) max_stack tl
     62      ]
     63  | _ ⇒ λ_. will_return_aux stack_cost depth current_stack max_stack tl
     64  ] (stack_cost s)
     65].
     66definition will_return' : Clight_stack_T → nat → execution_prefix → option nat ≝
     67λstack_cost,current_stack,trace. will_return_aux stack_cost O current_stack current_stack trace.
    7868
    7969definition measurable : clight_program → nat → nat → Clight_stack_T → nat → Prop ≝
     
    8272  split_trace cl_trace m = Some ? 〈prefix,suffix〉 ∧
    8373  split_trace suffix n = Some ? 〈interesting,remainder〉 ∧
    84   will_return' stack_cost O (stack_after prefix) interesting = Some ? max_stack ∧
     74  will_return' stack_cost (stack_after prefix) interesting = Some ? max_stack ∧
    8575  max_stack < max_allowed_stack.
    8676
     
    127117 
    128118(* start of old simulates 
     119
     120(* [nth_state_of_with_stack state stack_cost stack_bound exec n] returns [Some s] iff after
     121   [n] steps of [exec] we have reached [s] without exceeding the [stack_bound]
     122   according to the [stack_cost] function. *)
     123axiom nth_state_of_with_stack : ∀state. (state → nat) → nat → execution state io_out io_in → nat → option state.
     124axiom nth_state_of : ∀state. execution state io_out io_in → nat → option state.
     125
    129126
    130127  let cl_trace ≝ exec_inf … clight_fullexec labelled in
Note: See TracChangeset for help on using the changeset viewer.