source: src/correctness.ma @ 2487

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

Get compiler.ma and correctness.ma checking again. Note that the back-end
is in a state of flux at the moment, so is axiomatised out.

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