source: src/correctness.ma @ 2338

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

Fill out some Clight bits and pieces in correctness.ma.

File size: 6.9 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  ∀object_code,costlabel_map,labelled,cost_map.
14  compile input_program = OK ? 〈〈object_code,costlabel_map〉,labelled,cost_map〉 →
15
16  not_wrong … (exec_inf … clight_fullexec input_program) →
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#object_code #costlabel_map #labelled #cost_map
24#COMPILE
25#NOT_WRONG
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
37
38include "Clight/abstract.ma".
39
40definition Clight_stack_T ≝ ∀s:Clight_state. match Clight_classify s with [ cl_call ⇒ True | cl_return ⇒ True | _ ⇒ False ] → nat.
41
42definition execution_prefix : Type[0] ≝ list (trace × Clight_state).
43axiom split_trace : execution Clight_state io_out io_in → nat → option (execution_prefix × (execution Clight_state io_out io_in)).
44axiom stack_after : execution_prefix → nat.
45
46(* TODO: cost labels *)
47
48let 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 ≝
50match 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].
66definition 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.
68
69definition measurable : clight_program → nat → nat → Clight_stack_T → nat → Prop ≝
70λp,m,n,stack_cost,max_allowed_stack.  ∀prefix,suffix,interesting,remainder,max_stack.
71  let cl_trace ≝ exec_inf … clight_fullexec p in
72  split_trace cl_trace m = Some ? 〈prefix,suffix〉 ∧
73  split_trace suffix n = Some ? 〈interesting,remainder〉 ∧
74  will_return' stack_cost (stack_after prefix) interesting = Some ? max_stack ∧
75  max_stack < max_allowed_stack.
76
77(* From measurable on Clight, we will end up with an RTLabs flat trace where
78   we know that there are some m' and n' such that the prefix in Clight matches
79   the prefix in RTLabs given by m', the next n steps in Clight are equivalent
80   to the n' steps in RTLabs, and we have a suitable "will_return" for RTLabs
81   for those n' steps so that we can build a corresponding structured trace.
82   
83   "Equivalent" here means, in particular, that the observables will be the same,
84   and those observables will include the stack space costs.
85 *)
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(* [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. *)
123axiom nth_state_of_with_stack : ∀state. (state → nat) → nat → execution state io_out io_in → nat → option state.
124axiom nth_state_of : ∀state. execution state io_out io_in → nat → option state.
125
126
127  let cl_trace ≝ exec_inf … clight_fullexec labelled in
128  let asm_trace ≝ exec_inf … ASM_fullexec object_code in
129  not_wrong ? cl_trace →
130  ∀n,s. nth_state_of_with_stack ? stack_cost stack_bound cl_trace n = Some ? s →
131  𝚺m,s'. nth_state_of ? asm_trace m = Some ? s' ∧ s ≃ s'
132
133*)
134
135(* TODO
136
137
138∀input_program.
139! 〈object_code,costlabel_map,labelled,cost_map〉 ← compile input_program
140
141exec_inf … clight_fullexec input_program ≃l exec_inf … clight_fullexec labelled
142
143
144
145exec_inf … clight_fullexec labelled ≈ exec_inf … ASM_fullexec object_code
146(* Should we be lifting labels in some way here? *)
147
148
149
150∀i,f : clight_status.
151  Clight_labelled i →
152  Clight_labelled f →
153∀mx,time.
154  let trace ≝ exec_inf_aux … clight_fullexec labelled i in
155  will_return O O mx time f trace →
156  mx < max_allowed_stack →
157∃!i',f'. i ≃ i' ∧ f ≃ f' ∧ i' 8051~> f' ∧
158  time = clock f' - clock i'.
159
160
161∀s,flat.
162let ge ≝ (globalenvs … labelled) in
163subtrace_of (exec_inf … RTLabs_fullexec labelled) flat →
164RTLabs_cost s = true →
165∀WR : will_return ge 0 s flat.
166let structured_trace_rtlabs ≝ make_label_return' ge 0 s flat ??? WR in
167let labels_rtlabs ≝ flat_label_trace … flat WR in
168∃!initial,final,structured_trace_asm.
169  structured_trace_rtlabs ≈ structured_trace_asm ∧ 
170  clock … code_memory … final = clock … code_memory … initial +
171     (Σ_{i < |labels_rtlabs|} (cost_map (match nth i labels_rtlabs with [ Some k ⇒ k | None ⇒ 0 ])).
172
173
174
175What is ≃l?  Must show that "labelled" does everything that
176"input_program" does, without getting lost in some
177non-terminating loop part way.
178
179*)
180
Note: See TracBrowser for help on using the repository browser.