source: src/correctness.ma @ 2695

Last change on this file since 2695 was 2677, checked in by campbell, 7 years ago

Retain the pointer for the function called in front-end call states
so that we can do sensible stack costs.

File size: 7.7 KB
Line 
1
2include "compiler.ma".
3
4include "ASM/Interpret2.ma".
5
6include "Clight/Cexec.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[ (* Needs switch removal too, now
34     @labelling_sim @NOT_WRONG
35   *) cases daemon
36| @I
37] qed.
38
39
40include "Clight/Clight_abstract.ma".
41include "common/Measurable.ma".
42
43(* We could restrict this function to identifiers that are function names in the
44   program and lift it (like the lift_cost_map_back_to_front function), but
45   let's go with the easier notion of having a total map and ignore all the
46   extra stuff. *)
47definition stack_cost_T ≝ ident → nat.
48
49(* Again, in principle we can use the fact that the state must be a call and
50   also show some relevant invariants about call states, but we go with the
51   easier option of returning zero elsewhere. *)
52definition Clight_stack_cost :
53  stack_cost_T →
54  cl_genv →
55  ∀s:Clight_state.
56  match Clight_classify s with [ cl_call ⇒ True | _ ⇒ False ] →
57  nat ≝
58λcost,ge,s,H.
59match s with
60[ Callstate v _ _ _ _ ⇒
61  match v with [ Vptr p ⇒ match symbol_for_block … ge (pblock p) with [ Some id ⇒ cost id | _ ⇒ 0 ] | _ ⇒ 0 ]
62| _ ⇒ 0
63].
64
65definition Clight_pcs : preclassified_system ≝
66mk_preclassified_system
67  clight_fullexec
68  (λ_.Clight_labelled)
69  (λ_.Clight_classify)
70  Clight_stack_cost.
71
72(* From measurable on Clight, we will end up with an RTLabs flat trace where
73   we know that there are some m' and n' such that the prefix in Clight matches
74   the prefix in RTLabs given by m', the next n steps in Clight are equivalent
75   to the n' steps in RTLabs, and we have a suitable "will_return" for RTLabs
76   for those n' steps so that we can build a corresponding structured trace.
77   
78   "Equivalent" here means, in particular, that the observables will be the same,
79   and those observables will include the stack space costs.
80 *)
81
82axiom observables_8051 : object_code → nat → nat → option ((list trace) × (list trace)).
83
84definition in_execution_prefix : execution_prefix Clight_state → costlabel → Prop ≝
85λx,l. Exists … (λtrs. Exists … (λev. ev = EVcost l) (\fst trs)) x.
86
87let 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 ≝
88match l' return λl'. (∀b. Exists … (λx.x=b) l' → Exists … (λx.x=b) l) → A with
89[ nil ⇒ λ_. a
90| cons h t ⇒ λH. foldl_exists_aux A B l t f (f a h (H …)) ?
91].
92[ %1 %
93| #b #H' @H %2 @H'
94] qed.
95
96definition foldl_exists : ∀A,B:Type[0]. ∀l:list B. (A → ∀b:B. Exists … (λx. x = b ) l → A) → A → A ≝
97λA,B,l,f,a.  foldl_exists_aux A B l l f a (λb,H. H).
98
99lemma Exists_lift : ∀A,P,Q,l.
100  (∀x. P x → Q x) →
101  Exists A P l →
102  Exists A Q l.
103#A #P #Q #l elim l
104[ //
105| #h #t #IH #H * [ #H' %1 @H @H' | #H' %2 @IH /2/ ]
106] qed.
107
108definition measure_clock : ∀x:execution_prefix Clight_state. ((Σl:costlabel.in_execution_prefix x l)→ℕ) → nat ≝
109λx,costmap. foldl_exists … x
110 (λclock,trs,H.
111    foldl_exists … (\fst trs) (λclock,ev. match ev return λev. Exists … (λx. x=ev) ? → nat with [ EVcost l ⇒ λH'. clock + costmap «l,?» | _ ⇒ λ_. clock ]) clock)
112 0.
113whd @(Exists_lift … H) * #tr1 #s1 #E destruct @(Exists_lift … H') #ev1 #E @E
114qed.
115
116definition clight_clock_after : ∀p:clight_program. nat → ((Σl:costlabel.in_clight_program p l)→ℕ) → option nat ≝
117λp,n,costmap.
118  let x ≝ exec_inf … clight_fullexec p in
119  match split_trace … x n with
120  [ Some traces ⇒
121    Some ? (measure_clock (\fst traces) (λl.costmap «l,?»))
122  | None ⇒ None ?
123  ].
124cases daemon
125qed.
126
127axiom initial_8051_status : ∀oc. Status oc.
128
129definition simulates ≝
130  λstack_cost : stack_cost_T.  λ stack_bound, labelled, object_code, cost_map.
131  let initial_status ≝ initial_8051_status (load_code_memory object_code) in
132  ∀m1,m2. measurable Clight_pcs labelled m1 m2 stack_cost stack_bound →
133  ∀c1,c2. clight_clock_after labelled m1 cost_map = Some ? c1 → clight_clock_after labelled m2 cost_map = Some ? c2 →
134  ∃n1,n2. observables clight_fullexec labelled m1 m2 = observables_8051 object_code n1 n2 ∧
135          c2 - c1 = clock … (execute n2 ? initial_status) - clock … (execute n1 ? initial_status).
136
137axiom compile' : clight_program → res (object_code × costlabel_map ×
138  (𝚺labelled:clight_program. ((Σl:costlabel.in_clight_program labelled l)→ℕ)) × stack_cost_T × nat).
139
140theorem correct' :
141  ∀input_program.
142
143  not_wrong … (exec_inf … clight_fullexec input_program) →
144 
145  ∀object_code,costlabel_map,labelled,cost_map,stack_cost,stack_bound.
146  compile' input_program = OK ? 〈〈〈object_code,costlabel_map〉,❬labelled,cost_map❭〉,stack_cost,stack_bound〉 →
147 
148  sim_with_labels (exec_inf … clight_fullexec input_program) (exec_inf … clight_fullexec labelled)
149  ∧
150
151  simulates stack_cost stack_bound labelled object_code cost_map.
152 
153
154 
155(* start of old simulates 
156
157(* [nth_state_of_with_stack state stack_cost stack_bound exec n] returns [Some s] iff after
158   [n] steps of [exec] we have reached [s] without exceeding the [stack_bound]
159   according to the [stack_cost] function. *)
160axiom nth_state_of_with_stack : ∀state. (state → nat) → nat → execution state io_out io_in → nat → option state.
161axiom nth_state_of : ∀state. execution state io_out io_in → nat → option state.
162
163
164  let cl_trace ≝ exec_inf … clight_fullexec labelled in
165  let asm_trace ≝ exec_inf … ASM_fullexec object_code in
166  not_wrong ? cl_trace →
167  ∀n,s. nth_state_of_with_stack ? stack_cost stack_bound cl_trace n = Some ? s →
168  𝚺m,s'. nth_state_of ? asm_trace m = Some ? s' ∧ s ≃ s'
169
170*)
171
172(* TODO
173
174
175∀input_program.
176! 〈object_code,costlabel_map,labelled,cost_map〉 ← compile input_program
177
178exec_inf … clight_fullexec input_program ≃l exec_inf … clight_fullexec labelled
179
180
181
182exec_inf … clight_fullexec labelled ≈ exec_inf … ASM_fullexec object_code
183(* Should we be lifting labels in some way here? *)
184
185
186
187∀i,f : clight_status.
188  Clight_labelled i →
189  Clight_labelled f →
190∀mx,time.
191  let trace ≝ exec_inf_aux … clight_fullexec labelled i in
192  will_return O O mx time f trace →
193  mx < max_allowed_stack →
194∃!i',f'. i ≃ i' ∧ f ≃ f' ∧ i' 8051~> f' ∧
195  time = clock f' - clock i'.
196
197
198∀s,flat.
199let ge ≝ (globalenvs … labelled) in
200subtrace_of (exec_inf … RTLabs_fullexec labelled) flat →
201RTLabs_cost s = true →
202∀WR : will_return ge 0 s flat.
203let structured_trace_rtlabs ≝ make_label_return' ge 0 s flat ??? WR in
204let labels_rtlabs ≝ flat_label_trace … flat WR in
205∃!initial,final,structured_trace_asm.
206  structured_trace_rtlabs ≈ structured_trace_asm ∧ 
207  clock … code_memory … final = clock … code_memory … initial +
208     (Σ_{i < |labels_rtlabs|} (cost_map (match nth i labels_rtlabs with [ Some k ⇒ k | None ⇒ 0 ])).
209
210
211
212What is ≃l?  Must show that "labelled" does everything that
213"input_program" does, without getting lost in some
214non-terminating loop part way.
215
216*)
217
Note: See TracBrowser for help on using the repository browser.