Changeset 2325 for src/correctness.ma
 Timestamp:
 Sep 7, 2012, 11:26:19 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/correctness.ma
r2323 r2325 10 10 theorem correct : 11 11 ∀input_program. 12 13 not_wrong … (exec_inf … clight_fullexec input_program) →14 12 15 13 ∀object_code,costlabel_map,labelled,cost_map. 16 14 compile input_program = OK ? 〈〈object_code,costlabel_map〉,labelled,cost_map〉 → 15 16 not_wrong … (exec_inf … clight_fullexec input_program) → 17 17 18 18 sim_with_labels (exec_inf … clight_fullexec input_program) (exec_inf … clight_fullexec labelled) … … 21 21 22 22 #input_program 23 #NOT_WRONG24 23 #object_code #costlabel_map #labelled #cost_map 25 24 #COMPILE 25 #NOT_WRONG 26 26 cases (bind_inversion ????? COMPILE) COMPILE * * #init_cost #labelled' #rtlabs_program * #FRONTEND #COMPILE 27 27 cases (bind_inversion ????? COMPILE) COMPILE * #object_code' #costlabel_map' * #ASSEMBLER #COMPILE … … 35 35 ] qed. 36 36 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.40 37 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]. *) 38 include "Clight/abstract.ma". 44 39 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. 40 definition Clight_stack_T ≝ ∀s:Clight_state. match Clight_classify s with [ cl_call ⇒ True  cl_return ⇒ True  _ ⇒ False ] → nat. 67 41 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. 42 definition execution_prefix : Type[0] ≝ list (trace × Clight_state). 43 axiom split_trace : execution Clight_state io_out io_in → nat → option (execution_prefix × (execution Clight_state io_out io_in)). 44 axiom stack_after : execution_prefix → nat. 73 45 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 48 let 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 ≝ 50 match 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 ]. 66 definition 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. 78 68 79 69 definition measurable : clight_program → nat → nat → Clight_stack_T → nat → Prop ≝ … … 82 72 split_trace cl_trace m = Some ? 〈prefix,suffix〉 ∧ 83 73 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 ∧ 85 75 max_stack < max_allowed_stack. 86 76 … … 127 117 128 118 (* 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. *) 123 axiom nth_state_of_with_stack : ∀state. (state → nat) → nat → execution state io_out io_in → nat → option state. 124 axiom nth_state_of : ∀state. execution state io_out io_in → nat → option state. 125 129 126 130 127 let cl_trace ≝ exec_inf … clight_fullexec labelled in
Note: See TracChangeset
for help on using the changeset viewer.