source: src/correctness.ma @ 2782

Last change on this file since 2782 was 2774, checked in by sacerdot, 7 years ago
  1. the compiler now outputs both the stack cost model and the max stack available
  2. hypothesis on initial status not failing removed from correctness.ma by using the low level definition
File size: 7.0 KB
Line 
1
2include "compiler.ma".
3
4include "ASM/Interpret2.ma".
5
6include "Clight/labelSimulation.ma".
7
8theorem correct :
9  ∀input_program,output.
10(*  ∀lobject_code,labelled,cost_map. *)
11  compile input_program = OK ? output →
12
13  not_wrong … (exec_inf … clight_fullexec input_program) →
14 
15  sim_with_labels
16   (exec_inf … clight_fullexec input_program)
17   (exec_inf … clight_fullexec (c_labelled_clight … output))
18  ∧
19  True (* TODO *).
20
21#input_program #output
22#COMPILE
23#NOT_WRONG
24cases (bind_inversion ????? COMPILE) -COMPILE * * #init_cost #labelled' #rtlabs_program * #FRONTEND #COMPILE
25cases (bind_inversion ????? COMPILE) -COMPILE #lobject_code' * #ASSEMBLER #COMPILE
26whd in COMPILE:(??%%); destruct
27cases (bind_inversion ????? FRONTEND) -FRONTEND #cminor_program * #CMINOR #FRONTEND
28whd in FRONTEND:(??%%); destruct
29
30%
31[ (* Needs switch removal too, now
32     @labelling_sim @NOT_WRONG
33   *) cases daemon
34| @I
35] qed.
36
37
38include "Clight/Clight_abstract.ma".
39include "common/Measurable.ma".
40
41definition Clight_stack_ident :
42  cl_genv →
43  ∀s:Clight_state.
44  match Clight_classify s with [ cl_call ⇒ True | _ ⇒ False ] →
45  ident ≝
46λge,s.
47match s return λs. match Clight_classify s with [ cl_call ⇒ True | _ ⇒ False ] → ident with
48[ Callstate id _ _ _ _ ⇒ λ_. id
49| _ ⇒ λH.⊥
50].
51@H
52qed.
53
54definition Clight_pcs : preclassified_system ≝
55mk_preclassified_system
56  clight_fullexec
57  (λ_.Clight_labelled)
58  (λ_.Clight_classify)
59  Clight_stack_ident.
60
61(* From measurable on Clight, we will end up with an RTLabs flat trace where
62   we know that there are some m' and n' such that the prefix in Clight matches
63   the prefix in RTLabs given by m', the next n steps in Clight are equivalent
64   to the n' steps in RTLabs, and we have a suitable "will_return" for RTLabs
65   for those n' steps so that we can build a corresponding structured trace.
66   
67   "Equivalent" here means, in particular, that the observables will be the same,
68   and those observables will include the stack space costs.
69 *)
70
71definition in_execution_prefix : execution_prefix Clight_state → costlabel → Prop ≝
72λx,l. Exists … (λtrs. Exists … (λev. ev = EVcost l) (\fst trs)) x.
73
74let 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 ≝
75match l' return λl'. (∀b. Exists … (λx.x=b) l' → Exists … (λx.x=b) l) → A with
76[ nil ⇒ λ_. a
77| cons h t ⇒ λH. foldl_exists_aux A B l t f (f a h (H …)) ?
78].
79[ %1 %
80| #b #H' @H %2 @H'
81] qed.
82
83definition foldl_exists : ∀A,B:Type[0]. ∀l:list B. (A → ∀b:B. Exists … (λx. x = b ) l → A) → A → A ≝
84λA,B,l,f,a.  foldl_exists_aux A B l l f a (λb,H. H).
85
86lemma Exists_lift : ∀A,P,Q,l.
87  (∀x. P x → Q x) →
88  Exists A P l →
89  Exists A Q l.
90#A #P #Q #l elim l
91[ //
92| #h #t #IH #H * [ #H' %1 @H @H' | #H' %2 @IH /2/ ]
93] qed.
94
95definition measure_clock : ∀x:execution_prefix Clight_state. ((Σl:costlabel.in_execution_prefix x l)→ℕ) → nat ≝
96λx,costmap. foldl_exists … x
97 (λclock,trs,H.
98    foldl_exists … (\fst trs) (λclock,ev. match ev return λev. Exists … (λx. x=ev) ? → nat with [ EVcost l ⇒ λH'. clock + costmap «l,?» | _ ⇒ λ_. clock ]) clock)
99 0.
100whd @(Exists_lift … H) * #tr1 #s1 #E destruct @(Exists_lift … H') #ev1 #E @E
101qed.
102
103definition clight_clock_after : ∀p:clight_program. nat → ((Σl:costlabel.in_clight_program p l)→ℕ) → option nat ≝
104λp,n,costmap.
105  let x ≝ exec_inf … clight_fullexec p in
106  match split_trace … x n with
107  [ Some traces ⇒
108    Some ? (measure_clock (\fst traces) (λl.costmap «l,?»))
109  | None ⇒ None ?
110  ].
111cases daemon
112qed.
113
114include "common/AssocList.ma".
115
116definition lookup_stack_cost : stack_cost_model → ident → nat ≝
117 λstack_cost,id.
118  match assoc_list_lookup ?? id (eq_identifier …) stack_cost with
119  [ None ⇒ 0 | Some n ⇒ n ].
120
121definition simulates ≝
122  λp: compiler_output.
123  let initial_status ≝ initialise_status … (load_code_memory (oc (c_labelled_object_code … p))) in
124  ∀m1,m2.
125   measurable Clight_pcs (c_labelled_clight … p) m1 m2
126    (lookup_stack_cost (c_stack_cost … p)) (c_max_stack … p) →
127  ∀c1,c2.
128   clight_clock_after (c_labelled_clight … p) m1 (c_clight_cost_map … p) = Some ? c1 →
129   clight_clock_after (c_labelled_clight … p) m2 (c_clight_cost_map … p) = Some ? c2 →
130  ∃n1,n2.
131   observables Clight_pcs (c_labelled_clight … p) m1 m2 =
132   observables (OC_preclassified_system (c_labelled_object_code … p)) it n1 n2
133  ∧
134   minus c2 c1 = clock … (execute n2 ? initial_status) - clock … (execute n1 ? initial_status).
135
136theorem correct' :
137  ∀input_program,output.
138  ∀initial_status.
139  compile input_program = OK ? output →
140  not_wrong … (exec_inf … clight_fullexec input_program) →
141  sim_with_labels
142   (exec_inf … clight_fullexec input_program)
143   (exec_inf … clight_fullexec (c_labelled_clight … output))
144  ∧
145  simulates output.
146 
147(* start of old simulates 
148
149(* [nth_state_of_with_stack state stack_cost stack_bound exec n] returns [Some s] iff after
150   [n] steps of [exec] we have reached [s] without exceeding the [stack_bound]
151   according to the [stack_cost] function. *)
152axiom nth_state_of_with_stack : ∀state. (state → nat) → nat → execution state io_out io_in → nat → option state.
153axiom nth_state_of : ∀state. execution state io_out io_in → nat → option state.
154
155
156  let cl_trace ≝ exec_inf … clight_fullexec labelled in
157  let asm_trace ≝ exec_inf … ASM_fullexec object_code in
158  not_wrong ? cl_trace →
159  ∀n,s. nth_state_of_with_stack ? stack_cost stack_bound cl_trace n = Some ? s →
160  𝚺m,s'. nth_state_of ? asm_trace m = Some ? s' ∧ s ≃ s'
161
162*)
163
164(* TODO
165
166
167∀input_program.
168! 〈object_code,costlabel_map,labelled,cost_map〉 ← compile input_program
169
170exec_inf … clight_fullexec input_program ≃l exec_inf … clight_fullexec labelled
171
172
173
174exec_inf … clight_fullexec labelled ≈ exec_inf … ASM_fullexec object_code
175(* Should we be lifting labels in some way here? *)
176
177
178
179∀i,f : clight_status.
180  Clight_labelled i →
181  Clight_labelled f →
182∀mx,time.
183  let trace ≝ exec_inf_aux … clight_fullexec labelled i in
184  will_return O O mx time f trace →
185  mx < max_allowed_stack →
186∃!i',f'. i ≃ i' ∧ f ≃ f' ∧ i' 8051~> f' ∧
187  time = clock f' - clock i'.
188
189
190∀s,flat.
191let ge ≝ (globalenvs … labelled) in
192subtrace_of (exec_inf … RTLabs_fullexec labelled) flat →
193RTLabs_cost s = true →
194∀WR : will_return ge 0 s flat.
195let structured_trace_rtlabs ≝ make_label_return' ge 0 s flat ??? WR in
196let labels_rtlabs ≝ flat_label_trace … flat WR in
197∃!initial,final,structured_trace_asm.
198  structured_trace_rtlabs ≈ structured_trace_asm ∧ 
199  clock … code_memory … final = clock … code_memory … initial +
200     (Σ_{i < |labels_rtlabs|} (cost_map (match nth i labels_rtlabs with [ Some k ⇒ k | None ⇒ 0 ])).
201
202
203
204What is ≃l?  Must show that "labelled" does everything that
205"input_program" does, without getting lost in some
206non-terminating loop part way.
207
208*)
209
Note: See TracBrowser for help on using the repository browser.