source: src/Clight/toCminorCorrectness.ma @ 2597

Last change on this file since 2597 was 2597, checked in by campbell, 8 years ago

Some work in progress on measurable subtrace preservation.

File size: 12.3 KB
Line 
1include "Clight/toCminor.ma".
2include "Clight/CexecInd.ma".
3include "common/Globalenvs.ma".
4include "Clight/memoryInjections.ma".
5include "Clight/abstract.ma".
6include "Cminor/abstract.ma".
7
8(* Expr simulation. Contains important definitions for statements, too.  *)
9include "Clight/toCminorCorrectnessExpr.ma".
10
11
12(* When we characterise the local Clight variables, those that are stack
13   allocated are given disjoint regions of the stack. *)
14
15lemma characterise_vars_disjoint : ∀globals,f,vartypes,stacksize,id,n,ty.
16  characterise_vars globals f = 〈vartypes, stacksize〉 →
17  lookup ?? vartypes id = Some ? 〈Stack n,ty〉 →
18  ∀id',n',ty'. id ≠ id' →
19  lookup ?? vartypes id' = Some ? 〈Stack n',ty'〉 →
20  n' + sizeof ty' ≤ n ∨ n + sizeof ty ≤ n'.
21#globals * #ret #args #vars #body #vartypes #stacksize #id #n #ty
22whd in ⊢ (??%? → ?);
23generalize in match vartypes; -vartypes
24generalize in match stacksize; -stacksize
25elim (args@vars)
26[ #stacksize #vartypes #CHAR #L @⊥ whd in CHAR:(??%?); destruct
27  elim globals in L;
28  [ normalize #L destruct
29  | * * #id' #r #ty' #tl #IH
30    whd in match (foldr ?????);
31    #L cases (lookup_add_cases ??????? L)
32    [ * #E1 #E2 destruct
33    | @IH
34    ]
35  ]
36| * #id1 #ty1 #tl #IH #stacksize #vartypes
37  whd in match (foldr ?????);
38  (* Avoid writing out the definition again *)
39  letin ih ≝ (foldr ? (Prod ??) ?? tl) in IH ⊢ %;
40  lapply (refl ? ih) whd in match ih; -ih
41  cases (foldr ? (Prod ??) ?? tl) in ⊢ (???% → %);
42  #vartypes' #stack' #FOLD #IH
43  whd in ⊢ (??(match % with [_⇒?])? → ?);
44  cases (orb ??)
45  #CHAR whd in CHAR:(??%?); destruct
46  #L cases (lookup_add_cases ??????? L)
47  [ 1,3: * #E1 #E2 destruct
48    #id' #n' #ty' #NE >lookup_add_miss /2/
49    #L' %1 -L -IH
50    generalize in match vartypes' in FOLD L' ⊢ %; -vartypes'
51    generalize in match stack'; -stack'
52    elim tl
53    [ #stack' #vartypes2 whd in ⊢ (??%? → ?); #F destruct #L' @⊥
54      elim globals in L';
55      [ normalize #E destruct
56      | * * #id2 #r2 #ty2 #tl2 #IH whd in match (foldr ?????);
57        #L cases (lookup_add_cases ??????? L)
58        [ * #E1 #E2 destruct
59        | @IH
60        ]
61      ]
62    | * #id2 #ty2 #tl2 #IH #stack' #vartypes'
63      whd in ⊢ (??%? → ?); cases (foldr ? (Prod ??) ???) in IH ⊢ %;
64      #vartypes2 #stack2 #IH
65      whd in ⊢ (??%? → ?);
66      cases (orb ??)
67      [ #E whd in E:(??%?); destruct #L cases (lookup_add_cases ??????? L)
68        [ * #E1 #E2 destruct //
69        | #L'' lapply (IH ?? (refl ??) L'') /2/
70        ]
71      | #E whd in E:(??%?); destruct #L cases (lookup_add_cases ??????? L)
72        [ * #E1 #E2 destruct
73        | #L'' lapply (IH ?? (refl ??) L'') /2/
74        ]
75      ]
76    ]
77  | -L #L #id' #n' #ty' #NE #L'
78    cases (lookup_add_cases ??????? L')
79    [ * #E1 #E2 destruct
80      %2 -IH -L'
81      generalize in match vartypes' in FOLD L; -vartypes'
82      generalize in match stack'; -stack'
83      elim tl
84      [ #stack' #vartypes' whd in ⊢ (??%? → ?); #F destruct #L @⊥
85        elim globals in L;
86        [ normalize #E destruct
87        | * * #id1 #r1 #ty1 #tl1 #IH whd in match (foldr ?????);
88          #L cases (lookup_add_cases ??????? L)
89          [ * #E1 #E2 destruct
90          | @IH
91          ]
92        ]
93      | * #id1 #ty1 #tl1 #IH #stack' #vartypes'
94        whd in ⊢ (??%? → ?); cases (foldr ? (Prod ??) ???) in IH ⊢ %;
95        #vartypes2 #stack2 #IH
96        whd in ⊢ (??%? → ?);
97        cases (orb ??)
98        #E whd in E:(??%?); destruct
99        #L cases (lookup_add_cases ??????? L)
100        [ 1,3: * #E1 #E2 destruct //
101        | 2,4: #L' lapply (IH ?? (refl ??) L') /2/
102        ]
103      ]
104    | @(IH … (refl ??) L … NE)
105    ]
106  | -L #L #id' #n' #ty' #NE #L'
107    cases (lookup_add_cases ??????? L')
108    [ * #E1 #E2 destruct
109    | @(IH … (refl ??) L … NE)
110    ]
111  ]
112] qed.
113
114(* And everything is in the stack frame. *)
115
116lemma characterise_vars_in_range : ∀globals,f,vartypes,stacksize,id,n,ty.
117  characterise_vars globals f = 〈vartypes, stacksize〉 →
118  lookup ?? vartypes id = Some ? 〈Stack n,ty〉 →
119  n + sizeof ty ≤ stacksize.
120#globals * #ret #args #vars #body whd in match (characterise_vars ??);
121elim (args@vars)
122[ #vartypes #stacksize #id #n #ty #FOLD #L @⊥
123  whd in FOLD:(??%?); destruct elim globals in L;
124  [ #E normalize in E; destruct
125  | * * #id' #r' #ty' #tl' #IH
126    whd in match (foldr ?????); #L cases (lookup_add_cases ??????? L)
127    [ * #E1 #E2 destruct
128    | @IH
129    ]
130  ]
131| * #id' #ty' #tl #IH #vartypes #stacksize #id #n #ty
132  whd in match (foldr ?????); cases (foldr ? (Prod ??) ???) in IH ⊢ %;
133  #vartypes' #stackspace' #IH
134  whd in ⊢ (??(match % with [_⇒?])? → ?);
135  cases (orb ??) whd in ⊢ (??%? → ?);
136  #E destruct #L cases (lookup_add_cases ??????? L)
137  [ 1,3: * #E1 #E2 destruct //
138  | 2,4: #L' lapply (IH … (refl ??) L') /2/
139  ]
140] qed.
141
142
143
144(* Put knowledge that Globals are global into a more useful form than the
145   one used for the invariant. *)   
146(* XXX superfluous lemma ? Commenting it for now.
147       if not superfluous : move to toCminorCorrectnessExpr.ma, after
148       [characterise_vars_localid] *)
149(*
150lemma characterise_vars_global : ∀globals,f,vartypes,stacksize.
151  characterise_vars globals f = 〈vartypes, stacksize〉 →
152  ∀id,r,ty. lookup' vartypes id = OK ? 〈Global r,ty〉 →
153  Exists ? (λx.x = 〈〈id,r〉,ty〉) globals ∧
154  ¬ Exists ? (λx. \fst x = id) (fn_params f @ fn_vars f).
155#globals #f #vartypes #stacksize #CHAR #id #r #ty #L
156cases (characterise_vars_src … CHAR id ?)
157[ * #r' * #ty' >L
158  * #E1 destruct (E1) #EX
159  %
160  [ @EX
161  | % #EX' cases (characterise_vars_localid … CHAR EX')
162    #ty' whd in ⊢ (% → ?); >L *
163  ]
164| * #ty' whd in ⊢ (% → ?); >L *
165| whd >(opt_eq_from_res ???? L) % #E destruct
166] qed. *)
167
168(* Show how the global environments match up. *)
169
170lemma map_partial_All_to_All2 : ∀A,B,P,f,l,H,l'.
171  map_partial_All A B P f l H = OK ? l' →
172  All2 ?? (λa,b. ∃p. f a p = OK ? b) l l'.
173#A #B #P #f #l
174elim l
175[ #H #l' #MAP normalize in MAP; destruct //
176| #h #t #IH * #p #H #l'
177  whd in ⊢ (??%? → ?);
178  lapply (refl ? (f h p)) whd in match (proj1 ???);
179  cases (f h p) in ⊢ (???% → %);
180  [ #b #E #MAP cases (bind_inversion ????? MAP)
181    #tl' * #MAP' #E' normalize in E'; destruct
182    % [ %{p} @E | @IH [ @H | @MAP' ] ]
183  | #m #_ #X normalize in X; destruct
184  ]
185] qed.
186 
187
188definition clight_cminor_matching : clight_program → matching ≝
189λp.
190  let tmpuniverse ≝ universe_for_program p in
191  let fun_globals ≝ map ?? (λidf. 〈\fst idf,Code,type_of_fundef (\snd idf)〉) (prog_funct ?? p) in
192  let var_globals ≝ map ?? (λv. 〈\fst (\fst v), \snd (\fst v), \snd (\snd v)〉) (prog_vars ?? p) in
193  let globals ≝ fun_globals @ var_globals in
194  mk_matching
195    ?? (list init_data × type) (list init_data)
196    (λvs,f_clight,f_cminor. ∃H1,H2. translate_fundef tmpuniverse globals H1 f_clight H2 = OK ? f_cminor)
197    (λv,w. \fst v = w).
198
199lemma clight_to_cminor_varnames : ∀p,p'.
200  clight_to_cminor p = OK ? p' →
201  prog_var_names … p = prog_var_names … p'.
202* #vars #fns #main * #vars' #fns' #main'
203#TO cases (bind_inversion ????? TO) #fns'' * #MAP #E
204whd in E:(??%%); destruct
205-MAP normalize
206elim vars
207[ //
208| * * #id #r * #d #t #tl #IH normalize >IH //
209] qed.
210
211
212lemma clight_to_cminor_matches : ∀p,p'.
213  clight_to_cminor p = OK ? p' →
214  match_program (clight_cminor_matching p) p p'.
215* #vars #fns #main * #vars' #fns' #main'
216#TO cases (bind_inversion ????? TO) #fns'' * #MAP #E
217whd in E:(??%%); destruct
218%
219[ -MAP whd in match (m_V ?); whd in match (m_W ?);
220  elim vars
221  [ //
222  | * * #id #r * #init #ty #tl #IH %
223    [ % //
224    | @(All2_mp … IH) * * #a #b * #c #d * * #e #f #g * /2/
225    ]
226  ]
227| @(All2_mp … (map_partial_All_to_All2 … MAP)) -MAP
228  * #id #f * #id' #f' * #H #F cases (bind_inversion ????? F) #f'' * #TRANSF #E
229  normalize in E; destruct
230  <(clight_to_cminor_varnames … TO)
231  % whd
232  % [2: % [2: @TRANSF | skip ] | skip ]
233| %
234] qed.
235
236
237(* This is the statement for expression simulation copied fro toCminorCorrectnessExpr.ma,
238   for easier reference.
239lemma eval_expr_sim :
240  (* [cl_cm_inv] maps CL globals to CM globals, including functions *)
241  ∀cl_cm_inv  : clight_cminor_inv.
242  (* current function (defines local environment) *)
243  ∀f          : function.
244  (* [alloctype] maps variables to their allocation type (global, stack, register) *)
245  ∀alloctype  : var_types.
246  ∀stacksize  : ℕ.
247  ∀alloc_hyp  : characterise_vars (globals cl_cm_inv) f = 〈alloctype, stacksize〉.
248  (* environments *)
249  ∀cl_env     : cl_env.
250  ∀cm_env     : cm_env.
251  (* Characterise clight environment. Needed to prove that some variable is either a parameter or a local.  *)
252  ∀cl_env_hyp : ∃m,m'. exec_alloc_variables empty_env m (fn_params f @ fn_vars f) = 〈cl_env,m'〉.
253  (* CL and CM memories *)
254  ∀cl_m       : mem.
255  ∀cm_m       : mem.
256  (* memory injection and matching *)
257  ∀embed      : embedding.
258  ∀injection  : memory_inj embed cl_m cm_m.
259  ∀stackptr   : block.
260  ∀matching   : memory_matching embed cl_m cm_m cl_env cm_env cl_cm_inv stackptr alloctype.
261  (* clight expr to cminor expr *)
262  (∀(e:expr).
263   ∀(e':CMexpr (typ_of_type (typeof e))).
264   ∀Hexpr_vars.
265   translate_expr alloctype e = OK ? («e', Hexpr_vars») →
266   ∀cl_val,trace,Hyp_present.
267   exec_expr (ge_cl … cl_cm_inv) cl_env cl_m e = OK ? 〈cl_val, trace〉 →
268   ∃cm_val. eval_expr (ge_cm cl_cm_inv) (typ_of_type (typeof e)) e' cm_env Hyp_present stackptr cm_m = OK ? 〈trace, cm_val〉 ∧
269            value_eq embed cl_val cm_val) ∧
270   (* clight /lvalue/ to cminor /expr/ *)
271  (∀ed,ty.
272   ∀(e':CMexpr ASTptr).
273   ∀Hexpr_vars.
274   translate_addr alloctype (Expr ed ty) = OK ? («e', Hexpr_vars») →
275   ∀cl_blo,cl_off,trace,Hyp_present.
276   exec_lvalue' (ge_cl … cl_cm_inv) cl_env cl_m ed ty = OK ? 〈cl_blo, cl_off, trace〉 →
277   ∃cm_val. eval_expr (ge_cm cl_cm_inv) ASTptr e' cm_env Hyp_present stackptr cm_m = OK ? 〈trace, cm_val〉 ∧
278            value_eq embed (Vptr (mk_pointer cl_blo cl_off)) cm_val).   
279*)
280
281
282
283
284axiom clight_cminor_rel : clight_cminor_inv → Clight_state → Cminor_state → Prop.
285
286(* Conjectured simulation results
287
288   We split these based on the start state:
289   
290   1. ‘normal’ states take some [S n] normal steps and simulates them by [S m]
291      normal steps in Cminor;
292   2. call and return steps are simulated by a call/return step plus [m] normal
293      steps (to copy stack allocated parameters / results); and
294   3. lone cost label steps are simulates by a lone cost label step
295   
296   These should allow us to maintain enough structure to identify the Cminor
297   subtrace corresponding to a measurable Clight subtrace.
298 *)
299
300definition clight_normal : Clight_state → bool ≝
301λs. match Clight_classify s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ].
302
303definition cminor_normal : Cminor_state → bool ≝
304λs. match Cminor_classify s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ].
305
306axiom clight_cminor_normal :
307  ∀INV:clight_cminor_inv.
308  ∀s1,s1',s2,tr.
309  clight_cminor_rel INV s1 s1' →
310  clight_normal s1 →
311  ¬ Clight_labelled s1 →
312  ∃n. after_n_steps (S n) … clight_exec (ge_cl INV) s1 (λs.clight_normal s ∧ ¬ Clight_labelled s) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) →
313  ∃m. after_n_steps (S m) … Cminor_exec (ge_cm INV) s1' (λs.cminor_normal s) (λtr',s2'.
314    tr = tr' ∧
315    clight_cminor_rel INV s2 s2'
316  ).
317
318axiom clight_cminor_call_return :
319  ∀INV:clight_cminor_inv.
320  ∀s1,s1',s2,tr.
321  clight_cminor_rel INV s1 s1' →
322  match Clight_classify s1 with [ cl_call ⇒ true | cl_return ⇒ true | _ ⇒ false ] →
323  after_n_steps 1 … clight_exec (ge_cl INV) s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) →
324  ∃m. after_n_steps (S m) … Cminor_exec (ge_cm INV) s1' (λs.cminor_normal s) (λtr',s2'.
325    tr = tr' ∧
326    clight_cminor_rel INV s2 s2'
327  ).
328
329axiom clight_cminor_cost :
330  ∀INV:clight_cminor_inv.
331  ∀s1,s1',s2,tr.
332  clight_cminor_rel INV s1 s1' →
333  Clight_labelled s1 →
334  after_n_steps 1 … clight_exec (ge_cl INV) s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) →
335  after_n_steps 1 … Cminor_exec (ge_cm INV) s1' (λs.true) (λtr',s2'.
336    tr = tr' ∧
337    clight_cminor_rel INV s2 s2'
338  ).
339
340axiom clight_cminor_init : ∀cl_program,cm_program,s,s'.
341  clight_to_cminor cl_program = OK ? cm_program →
342  make_initial_state ?? clight_fullexec cl_program = OK ? s →
343  make_initial_state ?? Cminor_fullexec cm_program = OK ? s' →
344  ∃INV. clight_cminor_rel INV s s'.
Note: See TracBrowser for help on using the repository browser.