source: src/correctness.ma @ 2322

Last change on this file since 2322 was 2322, checked in by campbell, 8 years ago

Today's correctness groupthink.

File size: 7.2 KB
Line 
1
2include "compiler.ma".
3
4include "common/SmallstepExec.ma".
5include "Clight/Cexec.ma".
6include "ASM/Interpret2.ma".
7
8include "Clight/labelSimulation.ma".
9
10theorem correct :
11  ∀input_program.
12
13  not_wrong … (exec_inf … clight_fullexec input_program) →
14 
15  ∀object_code,costlabel_map,labelled,cost_map.
16  compile input_program = OK ? 〈〈object_code,costlabel_map〉,labelled,cost_map〉 →
17 
18  sim_with_labels (exec_inf … clight_fullexec input_program) (exec_inf … clight_fullexec labelled)
19  ∧
20  True (* TODO *).
21
22#input_program
23#NOT_WRONG
24#object_code #costlabel_map #labelled #cost_map
25#COMPILE
26cases (bind_inversion ????? COMPILE) -COMPILE * * #init_cost #labelled' #rtlabs_program * #FRONTEND #COMPILE
27cases (bind_inversion ????? COMPILE) -COMPILE * #object_code' #costlabel_map' * #ASSEMBLER #COMPILE
28whd in COMPILE:(??%%); destruct
29cases (bind_inversion ????? FRONTEND) -FRONTEND #cminor_program * #CMINOR #FRONTEND
30whd in FRONTEND:(??%%); destruct
31
32%
33[ @labelling_sim @NOT_WRONG
34| @I
35] qed.
36
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
128(* TODO
129
130
131∀input_program.
132! 〈object_code,costlabel_map,labelled,cost_map〉 ← compile input_program
133
134exec_inf … clight_fullexec input_program ≃l exec_inf … clight_fullexec labelled
135
136
137
138exec_inf … clight_fullexec labelled ≈ exec_inf … ASM_fullexec object_code
139(* Should we be lifting labels in some way here? *)
140
141
142
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 →
150∃!i',f'. i ≃ i' ∧ f ≃ f' ∧ i' 8051~> f' ∧
151  time = clock f' - clock i'.
152
153
154∀s,flat.
155let ge ≝ (globalenvs … labelled) in
156subtrace_of (exec_inf … RTLabs_fullexec labelled) flat →
157RTLabs_cost s = true →
158∀WR : will_return ge 0 s flat.
159let structured_trace_rtlabs ≝ make_label_return' ge 0 s flat ??? WR in
160let labels_rtlabs ≝ flat_label_trace … flat WR in
161∃!initial,final,structured_trace_asm.
162  structured_trace_rtlabs ≈ structured_trace_asm ∧ 
163  clock … code_memory … final = clock … code_memory … initial +
164     (Σ_{i < |labels_rtlabs|} (cost_map (match nth i labels_rtlabs with [ Some k ⇒ k | None ⇒ 0 ])).
165
166
167
168What is ≃l?  Must show that "labelled" does everything that
169"input_program" does, without getting lost in some
170non-terminating loop part way.
171
172*)
173
Note: See TracBrowser for help on using the repository browser.