source: src/correctness.ma @ 2399

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

Fill in some details about the statement of correctness.

File size: 10.0 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).
43let rec split_trace (x:execution Clight_state io_out io_in) (n:nat) on n : option (execution_prefix × (execution Clight_state io_out io_in)) ≝
44match n with
45[ O ⇒ Some ? 〈[ ], x〉
46| S n' ⇒
47  match x with
48  [ e_step tr s x' ⇒
49    ! 〈pre,x''〉 ← split_trace x' n';
50    Some ? 〈〈tr,s〉::pre,x''〉
51  | _ ⇒ None ?
52  ]
53].
54
55definition trace_labelled : execution_prefix → Prop ≝
56λx. ∃tr1,s1,x',tr2,s2. x = 〈tr1,s1〉::(x'@[〈tr2,s2〉]) ∧ bool_to_Prop (Clight_labelled s1) ∧ bool_to_Prop (Clight_labelled s2).
57
58definition measure_stack : Clight_stack_T → execution_prefix → nat × nat ≝
59λstack_cost.
60  foldl … (λx, trs.
61    let 〈current,max_stack〉 ≝ x in
62    let 〈tr,s〉 ≝ trs in
63    let new ≝
64      match Clight_classify s return λcl. (match cl in status_class with [_⇒?] → ?) → ?  with
65      [ cl_call ⇒ λsc. current + sc I
66      | cl_return ⇒ λsc. current - sc I
67      | _ ⇒ λ_. current
68      ] (stack_cost s) in
69    〈new, max max_stack new〉) 〈0,0〉.
70
71definition stack_after : Clight_stack_T → execution_prefix → nat ≝
72λsc,x. \fst (measure_stack sc x).
73
74definition max_stack :  Clight_stack_T → execution_prefix → nat ≝
75λsc,x. \snd (measure_stack sc x).
76
77(* TODO: cost labels *)
78
79let rec will_return_aux (stack_cost:Clight_stack_T) (depth:nat) (current_stack:nat)
80                        (max_stack:nat) (trace:execution_prefix) on trace : option nat ≝
81match trace with
82[ nil ⇒ match depth with [ O ⇒ Some ? max_stack | _ ⇒ None ? ]
83| cons h tl ⇒
84  let 〈tr,s〉 ≝ h in
85  match Clight_classify s return λcl. (match cl in status_class with [_⇒?] → ?) → ?  with
86  [ cl_call ⇒ λsc.
87      let new_stack ≝ current_stack + sc I in
88      will_return_aux stack_cost (S depth) new_stack (max max_stack new_stack) tl
89  | cl_return ⇒ λsc.
90      match depth with
91      [ O ⇒ None ?
92      | S d ⇒ will_return_aux stack_cost d (current_stack - sc I) max_stack tl
93      ]
94  | _ ⇒ λ_. will_return_aux stack_cost depth current_stack max_stack tl
95  ] (stack_cost s)
96].
97definition will_return' : Clight_stack_T → nat → execution_prefix → option nat ≝
98λstack_cost,current_stack,trace. will_return_aux stack_cost O current_stack current_stack trace.
99
100definition measurable : clight_program → nat → nat → Clight_stack_T → nat → Prop ≝
101λp,m,n,stack_cost,max_allowed_stack.  ∀prefix,suffix,interesting,remainder,max_stack.
102  let cl_trace ≝ exec_inf … clight_fullexec p in
103  split_trace cl_trace m = Some ? 〈prefix,suffix〉 ∧
104  split_trace suffix n = Some ? 〈interesting,remainder〉 ∧
105  trace_labelled interesting →
106  will_return' stack_cost (stack_after stack_cost prefix) interesting = Some ? max_stack ∧
107  max_stack < max_allowed_stack.
108
109(* From measurable on Clight, we will end up with an RTLabs flat trace where
110   we know that there are some m' and n' such that the prefix in Clight matches
111   the prefix in RTLabs given by m', the next n steps in Clight are equivalent
112   to the n' steps in RTLabs, and we have a suitable "will_return" for RTLabs
113   for those n' steps so that we can build a corresponding structured trace.
114   
115   "Equivalent" here means, in particular, that the observables will be the same,
116   and those observables will include the stack space costs.
117 *)
118
119definition observables : clight_program → nat → nat → option ((list trace) × (list trace)) ≝
120λp,m,n.
121  let cl_trace ≝ exec_inf … clight_fullexec p in
122  match split_trace cl_trace m with
123  [ Some x ⇒
124    let 〈prefix,suffix〉 ≝ x in
125    match split_trace suffix n with
126    [ Some y ⇒
127      let interesting ≝ \fst y in
128      Some ? 〈map … (fst ??) prefix, map … (fst ??) interesting〉
129    | _ ⇒ None ?
130    ]
131  | _ ⇒ None ?
132  ].
133
134axiom observables_8051 : object_code → nat → nat → option ((list trace) × (list trace)).
135
136definition in_execution_prefix : execution_prefix → costlabel → Prop ≝
137λx,l. Exists … (λtrs. Exists … (λev. ev = EVcost l) (\fst trs)) x.
138
139let rec foldl_exists_aux (A,B:Type[0]) (l,l':list B) (f:A → ∀b:B. Exists … (λx.x=b) l → A) (a:A) on l' : (∀b. Exists … (λx.x=b) l' → Exists … (λx.x=b) l) → A ≝
140match l' return λl'. (∀b. Exists … (λx.x=b) l' → Exists … (λx.x=b) l) → A with
141[ nil ⇒ λ_. a
142| cons h t ⇒ λH. foldl_exists_aux A B l t f (f a h (H …)) ?
143].
144[ %1 %
145| #b #H' @H %2 @H'
146] qed.
147
148definition foldl_exists : ∀A,B:Type[0]. ∀l:list B. (A → ∀b:B. Exists … (λx. x = b ) l → A) → A → A ≝
149λA,B,l,f,a.  foldl_exists_aux A B l l f a (λb,H. H).
150
151lemma Exists_lift : ∀A,P,Q,l.
152  (∀x. P x → Q x) →
153  Exists A P l →
154  Exists A Q l.
155#A #P #Q #l elim l
156[ //
157| #h #t #IH #H * [ #H' %1 @H @H' | #H' %2 @IH /2/ ]
158] qed.
159
160definition measure_clock : ∀x:execution_prefix. ((Σl:costlabel.in_execution_prefix x l)→ℕ) → nat ≝
161λx,costmap. foldl_exists … x
162 (λclock,trs,H.
163    foldl_exists … (\fst trs) (λclock,ev. match ev return λev. Exists … (λx. x=ev) ? → nat with [ EVcost l ⇒ λH'. clock + costmap «l,?» | _ ⇒ λ_. clock ]) clock)
164 0.
165whd @(Exists_lift … H) * #tr1 #s1 #E destruct @(Exists_lift … H') #ev1 #E @E
166qed.
167
168definition clight_clock_after : ∀p:clight_program. nat → ((Σl:costlabel.in_clight_program p l)→ℕ) → option nat ≝
169λp,n,costmap.
170  let x ≝ exec_inf … clight_fullexec p in
171  match split_trace x n with
172  [ Some traces ⇒
173    Some ? (measure_clock (\fst traces) (λl.costmap «l,?»))
174  | None ⇒ None ?
175  ].
176cases daemon
177qed.
178
179axiom initial_8051_status : ∀oc. Status oc.
180
181definition simulates ≝
182  λstack_cost, stack_bound, labelled, object_code, cost_map.
183  let initial_status ≝ initial_8051_status (load_code_memory object_code) in
184  ∀m1,m2. measurable labelled m1 m2 stack_cost stack_bound →
185  ∀c1,c2. clight_clock_after labelled m1 cost_map = Some ? c1 → clight_clock_after labelled m2 cost_map = Some ? c2 →
186  ∃n1,n2. observables labelled m1 m2 = observables_8051 object_code n1 n2 ∧
187          c2 - c1 = clock … (execute n2 ? initial_status) - clock … (execute n1 ? initial_status).
188
189axiom compile' : clight_program → res (object_code × costlabel_map ×
190  (𝚺labelled:clight_program. ((Σl:costlabel.in_clight_program labelled l)→ℕ)) × Clight_stack_T × nat).
191
192theorem correct' :
193  ∀input_program.
194
195  not_wrong … (exec_inf … clight_fullexec input_program) →
196 
197  ∀object_code,costlabel_map,labelled,cost_map,stack_cost,stack_bound.
198  compile' input_program = OK ? 〈〈〈object_code,costlabel_map〉,❬labelled,cost_map❭〉,stack_cost,stack_bound〉 →
199 
200  sim_with_labels (exec_inf … clight_fullexec input_program) (exec_inf … clight_fullexec labelled)
201  ∧
202
203  simulates stack_cost stack_bound labelled object_code cost_map.
204 
205
206 
207(* start of old simulates 
208
209(* [nth_state_of_with_stack state stack_cost stack_bound exec n] returns [Some s] iff after
210   [n] steps of [exec] we have reached [s] without exceeding the [stack_bound]
211   according to the [stack_cost] function. *)
212axiom nth_state_of_with_stack : ∀state. (state → nat) → nat → execution state io_out io_in → nat → option state.
213axiom nth_state_of : ∀state. execution state io_out io_in → nat → option state.
214
215
216  let cl_trace ≝ exec_inf … clight_fullexec labelled in
217  let asm_trace ≝ exec_inf … ASM_fullexec object_code in
218  not_wrong ? cl_trace →
219  ∀n,s. nth_state_of_with_stack ? stack_cost stack_bound cl_trace n = Some ? s →
220  𝚺m,s'. nth_state_of ? asm_trace m = Some ? s' ∧ s ≃ s'
221
222*)
223
224(* TODO
225
226
227∀input_program.
228! 〈object_code,costlabel_map,labelled,cost_map〉 ← compile input_program
229
230exec_inf … clight_fullexec input_program ≃l exec_inf … clight_fullexec labelled
231
232
233
234exec_inf … clight_fullexec labelled ≈ exec_inf … ASM_fullexec object_code
235(* Should we be lifting labels in some way here? *)
236
237
238
239∀i,f : clight_status.
240  Clight_labelled i →
241  Clight_labelled f →
242∀mx,time.
243  let trace ≝ exec_inf_aux … clight_fullexec labelled i in
244  will_return O O mx time f trace →
245  mx < max_allowed_stack →
246∃!i',f'. i ≃ i' ∧ f ≃ f' ∧ i' 8051~> f' ∧
247  time = clock f' - clock i'.
248
249
250∀s,flat.
251let ge ≝ (globalenvs … labelled) in
252subtrace_of (exec_inf … RTLabs_fullexec labelled) flat →
253RTLabs_cost s = true →
254∀WR : will_return ge 0 s flat.
255let structured_trace_rtlabs ≝ make_label_return' ge 0 s flat ??? WR in
256let labels_rtlabs ≝ flat_label_trace … flat WR in
257∃!initial,final,structured_trace_asm.
258  structured_trace_rtlabs ≈ structured_trace_asm ∧ 
259  clock … code_memory … final = clock … code_memory … initial +
260     (Σ_{i < |labels_rtlabs|} (cost_map (match nth i labels_rtlabs with [ Some k ⇒ k | None ⇒ 0 ])).
261
262
263
264What is ≃l?  Must show that "labelled" does everything that
265"input_program" does, without getting lost in some
266non-terminating loop part way.
267
268*)
269
Note: See TracBrowser for help on using the repository browser.