source: src/correctness.ma @ 2757

Last change on this file since 2757 was 2722, checked in by campbell, 7 years ago

It's easier to keep the real function identifier in front-end Callstates
than mucking around with the function pointer.

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