source: src/correctness.ma @ 2323

Last change on this file since 2323 was 2323, checked in by campbell, 7 years ago

Some correctness proof comments.

File size: 7.7 KB
RevLine 
[1996]1
2include "compiler.ma".
3
4include "common/SmallstepExec.ma".
5include "Clight/Cexec.ma".
6include "ASM/Interpret2.ma".
7
[2150]8include "Clight/labelSimulation.ma".
9
10theorem correct :
11  ∀input_program.
12
[2205]13  not_wrong … (exec_inf … clight_fullexec input_program) →
[2150]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
[2320]26cases (bind_inversion ????? COMPILE) -COMPILE * * #init_cost #labelled' #rtlabs_program * #FRONTEND #COMPILE
[2150]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
[2322]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
[2323]87(* From measurable on Clight, we will end up with an RTLabs flat trace where
88   we know that there are some m' and n' such that the prefix in Clight matches
89   the prefix in RTLabs given by m', the next n steps in Clight are equivalent
90   to the n' steps in RTLabs, and we have a suitable "will_return" for RTLabs
91   for those n' steps so that we can build a corresponding structured trace.
92   
93   "Equivalent" here means, in particular, that the observables will be the same,
94   and those observables will include the stack space costs.
95 *)
96
[2322]97axiom observables : clight_program → nat → nat → option ((list trace) × (list trace)).
98axiom observables_8051 : object_code → nat → nat → option ((list trace) × (list trace)).
99axiom clight_clock_after : clight_program → nat → option nat.
100axiom initial_8051_status : ∀oc. Status oc.
101
102definition simulates ≝
103  λstack_cost, stack_bound, labelled, object_code.
104  let initial_status ≝ initial_8051_status (load_code_memory object_code) in
105  ∀m1,m2. measurable labelled m1 m2 stack_cost stack_bound →
106  ∀c1,c2. clight_clock_after labelled m1 = Some ? c1 → clight_clock_after labelled m2 = Some ? c2 →
107  ∃n1,n2. observables labelled m1 m2 = observables_8051 object_code n1 n2 ∧
108          c2 - c1 = clock … (execute n2 ? initial_status) - clock … (execute n1 ? initial_status).
109
110axiom compile' : clight_program → res (object_code × costlabel_map × clight_program
111 × ((Σl:costlabel.in_clight_program l)→ℕ) × Clight_stack_T × nat).
112
113theorem correct' :
114  ∀input_program.
115
116  not_wrong … (exec_inf … clight_fullexec input_program) →
117 
118  ∀object_code,costlabel_map,labelled,cost_map,stack_cost,stack_bound.
119  compile' input_program = OK ? 〈〈〈〈object_code,costlabel_map〉,labelled〉,cost_map〉,stack_cost,stack_bound〉 →
120 
121  sim_with_labels (exec_inf … clight_fullexec input_program) (exec_inf … clight_fullexec labelled)
122  ∧
123
124  simulates stack_cost stack_bound labelled object_code.
125 
126
127 
128(* start of old simulates 
129
130  let cl_trace ≝ exec_inf … clight_fullexec labelled in
131  let asm_trace ≝ exec_inf … ASM_fullexec object_code in
132  not_wrong ? cl_trace →
133  ∀n,s. nth_state_of_with_stack ? stack_cost stack_bound cl_trace n = Some ? s →
134  𝚺m,s'. nth_state_of ? asm_trace m = Some ? s' ∧ s ≃ s'
135
136*)
137
[1996]138(* TODO
139
[2322]140
[1996]141∀input_program.
[2003]142! 〈object_code,costlabel_map,labelled,cost_map〉 ← compile input_program
[1996]143
[2001]144exec_inf … clight_fullexec input_program ≃l exec_inf … clight_fullexec labelled
[1996]145
146
147
[2004]148exec_inf … clight_fullexec labelled ≈ exec_inf … ASM_fullexec object_code
149(* Should we be lifting labels in some way here? *)
[1996]150
[2001]151
152
[2322]153∀i,f : clight_status.
154  Clight_labelled i →
155  Clight_labelled f →
156∀mx,time.
157  let trace ≝ exec_inf_aux … clight_fullexec labelled i in
158  will_return O O mx time f trace →
159  mx < max_allowed_stack →
[2004]160∃!i',f'. i ≃ i' ∧ f ≃ f' ∧ i' 8051~> f' ∧
[2322]161  time = clock f' - clock i'.
[1996]162
[2001]163
[2003]164∀s,flat.
165let ge ≝ (globalenvs … labelled) in
166subtrace_of (exec_inf … RTLabs_fullexec labelled) flat →
167RTLabs_cost s = true →
168∀WR : will_return ge 0 s flat.
169let structured_trace_rtlabs ≝ make_label_return' ge 0 s flat ??? WR in
170let labels_rtlabs ≝ flat_label_trace … flat WR in
171∃!initial,final,structured_trace_asm.
172  structured_trace_rtlabs ≈ structured_trace_asm ∧ 
173  clock … code_memory … final = clock … code_memory … initial +
174     (Σ_{i < |labels_rtlabs|} (cost_map (match nth i labels_rtlabs with [ Some k ⇒ k | None ⇒ 0 ])).
[2001]175
[2003]176
177
[2001]178What is ≃l?  Must show that "labelled" does everything that
179"input_program" does, without getting lost in some
180non-terminating loop part way.
181
[1996]182*)
183
Note: See TracBrowser for help on using the repository browser.