source: src/correctness.ma @ 2623

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

Name change update.

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