source: src/correctness.ma @ 2765

Last change on this file since 2765 was 2765, checked in by sacerdot, 7 years ago
  1. correctness.ma repaired
  2. we used the OC_preclassified_system to make the theorem statement more uniform and close all the axioms

Notes:
a) the next step is to make the compiler return the stack cost too (easy)
b) the component of fullexec that returns the initial state returns a res.

Thus the final statement becomes uglier because program initialization
can fail. The one for the OC never does so, actually! I can call the
low level init function, but this breaks the preclassified_system
abstraction. Do we really need it to fail?

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