 Timestamp:
 Sep 4, 2012, 7:37:52 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/correctness.ma
r2320 r2322 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 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 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. 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. *) 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. 73 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. 78 79 definition 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 87 axiom observables : clight_program → nat → nat → option ((list trace) × (list trace)). 88 axiom observables_8051 : object_code → nat → nat → option ((list trace) × (list trace)). 89 axiom clight_clock_after : clight_program → nat → option nat. 90 axiom initial_8051_status : ∀oc. Status oc. 91 92 definition 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 100 axiom compile' : clight_program → res (object_code × costlabel_map × clight_program 101 × ((Σl:costlabel.in_clight_program l)→ℕ) × Clight_stack_T × nat). 102 103 theorem 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 37 128 (* TODO 129 38 130 39 131 ∀input_program. … … 49 141 ∧ 50 142 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 → 54 150 ∃!i',f'. i ≃ i' ∧ f ≃ f' ∧ i' 8051~> f' ∧ 55 clock f  clock i= clock f'  clock i'.151 time = clock f'  clock i'. 56 152 57 153
Note: See TracChangeset
for help on using the changeset viewer.