source: src/correctness.ma @ 2474

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

Tidy up measurable definition a bit more.

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