Changeset 2322


Ignore:
Timestamp:
Sep 4, 2012, 7:37:52 PM (7 years ago)
Author:
campbell
Message:

Today's correctness groupthink.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/correctness.ma

    r2320 r2322  
    3535] qed.
    3636
     37axiom Clight_classify : state → status_class.
     38axiom Clight_labelled : state → bool.
     39definition Clight_stack_T ≝ ∀s:state. match Clight_classify s with [ cl_call ⇒ True | cl_return ⇒ True | _ ⇒ False ] → nat.
     40
     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]. *)
     44
     45inductive 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.
     67
     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. *)
     71axiom nth_state_of_with_stack : ∀state. (state → nat) → nat → execution state io_out io_in → nat → option state.
     72axiom nth_state_of : ∀state. execution state io_out io_in → nat → option state.
     73
     74definition execution_prefix : Type[0] ≝ list (trace × state).
     75axiom split_trace : execution state io_out io_in → nat → option (execution_prefix × (execution state io_out io_in)).
     76axiom stack_after : execution_prefix → nat.
     77axiom will_return' : Clight_stack_T → nat → nat → execution_prefix → option nat.
     78
     79definition measurable : clight_program → nat → nat → Clight_stack_T → nat → Prop ≝
     80λp,m,n,stack_cost,max_allowed_stack.  ∀prefix,suffix,interesting,remainder,max_stack.
     81  let cl_trace ≝ exec_inf … clight_fullexec p in
     82  split_trace cl_trace m = Some ? 〈prefix,suffix〉 ∧
     83  split_trace suffix n = Some ? 〈interesting,remainder〉 ∧
     84  will_return' stack_cost O (stack_after prefix) interesting = Some ? max_stack ∧
     85  max_stack < max_allowed_stack.
     86
     87axiom observables : clight_program → nat → nat → option ((list trace) × (list trace)).
     88axiom observables_8051 : object_code → nat → nat → option ((list trace) × (list trace)).
     89axiom clight_clock_after : clight_program → nat → option nat.
     90axiom initial_8051_status : ∀oc. Status oc.
     91
     92definition simulates ≝
     93  λstack_cost, stack_bound, labelled, object_code.
     94  let initial_status ≝ initial_8051_status (load_code_memory object_code) in
     95  ∀m1,m2. measurable labelled m1 m2 stack_cost stack_bound →
     96  ∀c1,c2. clight_clock_after labelled m1 = Some ? c1 → clight_clock_after labelled m2 = Some ? c2 →
     97  ∃n1,n2. observables labelled m1 m2 = observables_8051 object_code n1 n2 ∧
     98          c2 - c1 = clock … (execute n2 ? initial_status) - clock … (execute n1 ? initial_status).
     99
     100axiom compile' : clight_program → res (object_code × costlabel_map × clight_program
     101 × ((Σl:costlabel.in_clight_program l)→ℕ) × Clight_stack_T × nat).
     102
     103theorem correct' :
     104  ∀input_program.
     105
     106  not_wrong … (exec_inf … clight_fullexec input_program) →
     107 
     108  ∀object_code,costlabel_map,labelled,cost_map,stack_cost,stack_bound.
     109  compile' input_program = OK ? 〈〈〈〈object_code,costlabel_map〉,labelled〉,cost_map〉,stack_cost,stack_bound〉 →
     110 
     111  sim_with_labels (exec_inf … clight_fullexec input_program) (exec_inf … clight_fullexec labelled)
     112  ∧
     113
     114  simulates stack_cost stack_bound labelled object_code.
     115 
     116
     117 
     118(* start of old simulates 
     119
     120  let cl_trace ≝ exec_inf … clight_fullexec labelled in
     121  let asm_trace ≝ exec_inf … ASM_fullexec object_code in
     122  not_wrong ? cl_trace →
     123  ∀n,s. nth_state_of_with_stack ? stack_cost stack_bound cl_trace n = Some ? s →
     124  𝚺m,s'. nth_state_of ? asm_trace m = Some ? s' ∧ s ≃ s'
     125
     126*)
     127
    37128(* TODO
     129
    38130
    39131∀input_program.
     
    49141
    50142
    51 
    52 ∀i,f : clight_status.  [i,f labelled, at same level]
    53 i clight~> f →
     143∀i,f : clight_status.
     144  Clight_labelled i →
     145  Clight_labelled f →
     146∀mx,time.
     147  let trace ≝ exec_inf_aux … clight_fullexec labelled i in
     148  will_return O O mx time f trace →
     149  mx < max_allowed_stack →
    54150∃!i',f'. i ≃ i' ∧ f ≃ f' ∧ i' 8051~> f' ∧
    55   clock f - clock i = clock f' - clock i'.
     151  time = clock f' - clock i'.
    56152
    57153
Note: See TracChangeset for help on using the changeset viewer.