source: src/correctness.ma @ 2766

Last change on this file since 2766 was 2766, checked in by mckinna, 7 years ago

pruned redundant dependency on Clight/Cexec?.ma

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