source: src/Clight/toCminorCorrectness.ma @ 2668

Last change on this file since 2668 was 2667, checked in by garnier, 8 years ago

Clight to Cminor, statements: some cases down. Subset of the simulation relation defined and seems to work.
Some cosmetic changes in toCminorCorrectnessExpr in order to clarify things in toCminorCorrectness.

File size: 30.3 KB
Line 
1include "Clight/toCminor.ma".
2include "Clight/CexecInd.ma".
3include "common/Globalenvs.ma".
4include "Clight/memoryInjections.ma".
5include "Clight/Clight_abstract.ma".
6include "Cminor/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
211lemma clight_to_cminor_matches : ∀p,p'.
212  clight_to_cminor p = OK ? p' →
213  match_program (clight_cminor_matching p) p p'.
214* #vars #fns #main * #vars' #fns' #main'
215#TO cases (bind_inversion ????? TO) #fns'' * #MAP #E
216whd in E:(??%%); destruct
217%
218[ -MAP whd in match (m_V ?); whd in match (m_W ?);
219  elim vars
220  [ //
221  | * * #id #r * #init #ty #tl #IH %
222    [ % //
223    | @(All2_mp … IH) * * #a #b * #c #d * * #e #f #g * /2/
224    ]
225  ]
226| @(All2_mp … (map_partial_All_to_All2 … MAP)) -MAP
227  * #id #f * #id' #f' * #H #F cases (bind_inversion ????? F) #f'' * #TRANSF #E
228  normalize in E; destruct
229  <(clight_to_cminor_varnames … TO)
230  % whd
231  % [2: % [2: @TRANSF | skip ] | skip ]
232| %
233] qed.
234
235
236(* This is the statement for expression simulation copied from toCminorCorrectnessExpr.ma,
237   for easier reference.
238lemma eval_expr_sim :
239  (* [cl_cm_inv] maps CL globals to CM globals, including functions *)
240  ∀cl_cm_inv  : clight_cminor_inv.
241  (* current function (defines local environment) *)
242  ∀f          : function.
243  ∀data       : clight_cminor_data f cl_cm_inv.
244  (* clight expr to cminor expr *)
245  (∀(e:expr).
246   ∀(e':CMexpr (typ_of_type (typeof e))).
247   ∀Hexpr_vars.
248   translate_expr (alloc_type ?? data) e = OK ? («e', Hexpr_vars») →
249   ∀cl_val,trace,Hyp_present.
250   exec_expr (ge_cl … cl_cm_inv) (cl_env ?? data) (cl_m ?? data) e = OK ? 〈cl_val, trace〉 →
251   ∃cm_val. eval_expr (ge_cm cl_cm_inv) (typ_of_type (typeof e)) e' (cm_env ?? data) Hyp_present (stackptr ?? data) (cm_m ?? data) = OK ? 〈trace, cm_val〉 ∧
252            value_eq (E ?? data) cl_val cm_val) ∧
253   (* clight /lvalue/ to cminor /expr/ *)
254  (∀ed,ty.
255   ∀(e':CMexpr ASTptr).
256   ∀Hexpr_vars.
257   translate_addr (alloc_type ?? data) (Expr ed ty) = OK ? («e', Hexpr_vars») →
258   ∀cl_blo,cl_off,trace,Hyp_present.
259   exec_lvalue' (ge_cl … cl_cm_inv) (cl_env ?? data) (cl_m ?? data) ed ty = OK ? 〈cl_blo, cl_off, trace〉 →
260   ∃cm_val. eval_expr (ge_cm cl_cm_inv) ASTptr e' (cm_env ?? data) Hyp_present (stackptr ?? data) (cm_m ?? data) = OK ? 〈trace, cm_val〉 ∧
261            value_eq (E ?? data) (Vptr (mk_pointer cl_blo cl_off)) cm_val).
262*)
263
264definition foo ≝ 3.
265
266(* relate Clight continuations and Cminor ones. *)
267inductive clight_cminor_cont_rel :
268  ∀INV:  clight_cminor_inv.  (* stuff on global variables and functions (matching between CL and CM) *)
269  ∀cl_f: function.           (* current Clight function *)
270  internal_function →        (* current Cminor function *)
271  clight_cminor_data cl_f INV → (* data for the current stack frame in CL and CM *)
272  option typ →               (* optional target type - uniform over a given function *)
273  cl_cont →                  (* CL cont *)
274  cm_cont →                  (* CM cont *)
275  Prop ≝
276| ClCm_cont_stop:
277  ∀INV, cl_f, cm_f, frame_data, target_type.
278  clight_cminor_cont_rel INV cl_f cm_f frame_data target_type Kstop Kend
279| ClCm_cont_seq:
280  ∀INV, cl_f, cm_f, frame_data, target_type.
281  ∀cl_s: statement.
282  ∀cm_s: stmt.
283  ∀cl_k':  cl_cont.
284  ∀cm_k':  cm_cont.
285  ∀stmt_univ, stmt_univ'.
286  ∀lbl_univ, lbl_univ'.
287  ∀lbls.
288  ∀flag.
289  ∀Htranslate_inv.
290  translate_statement (alloc_type ?? frame_data) stmt_univ lbl_univ lbls flag target_type cl_s = OK ? «〈stmt_univ',lbl_univ',cm_s〉, Htranslate_inv» →
291  clight_cminor_cont_rel INV cl_f cm_f frame_data target_type cl_k' cm_k' →
292  clight_cminor_cont_rel INV cl_f cm_f frame_data target_type (ClKseq cl_s cl_k') (Kseq cm_s cm_k')
293| ClCm_cont_while:
294  (* Inductive family parameters *)
295  ∀INV, cl_f, cm_f, frame_data, target_type.
296
297  (* sub-continuations *)
298  ∀cl_k': cl_cont.
299  ∀cm_k': cm_cont.
300
301  (* elements of the source while statement *)
302  ∀sz,sg.
303  ∀cl_cond_desc.
304  ∀cl_body.
305
306  (* elements of the converted while statement *)
307  ∀cm_cond: CMexpr (ASTint sz sg).
308  ∀cm_body.
309  ∀entry,exit: identifier Label.
310 
311  (* universes used to generate fresh labels and variables *) 
312  ∀stmt_univ, stmt_univ'.
313  ∀lbl_univ, lbl_univ', lbl_univ''.
314  ∀lbls: lenv.
315  ∀Htranslate_inv.
316
317  (* relate CL and CM expressions *)
318  ∀Hexpr_vars.
319  translate_expr (alloc_type ?? frame_data) (Expr cl_cond_desc (Tint sz sg)) = OK ? («cm_cond, Hexpr_vars») →
320
321  (* Parameters and results to find_label_always *)
322  ∀sInv: stmt_inv cm_f (cm_env ?? frame_data) (f_body cm_f).
323  ∀Hinv.
324
325  (* Specify how the labels for the while-replacing gotos are produced *)
326  mklabels lbl_univ = 〈〈entry, exit〉, lbl_univ'〉 →
327  translate_statement (alloc_type ?? frame_data) stmt_univ lbl_univ' lbls (ConvertTo entry exit) target_type cl_body = OK ? «〈stmt_univ',lbl_univ'',cm_body〉, Htranslate_inv» →
328  find_label_always entry (f_body cm_f) Kend (proj2 … (proj1 … (proj1 … Hinv))) cm_f (cm_env ?? frame_data) sInv I =
329    «〈St_label entry
330          (St_seq
331            (St_ifthenelse ?? cm_cond (St_seq cm_body (St_goto entry)) St_skip)
332            (St_label exit St_skip)), cm_k'〉, Hinv» →
333  clight_cminor_cont_rel INV cl_f cm_f frame_data target_type cl_k' cm_k' →
334  clight_cminor_cont_rel INV cl_f cm_f frame_data target_type (Kwhile (Expr cl_cond_desc (Tint sz sg)) cl_body cl_k') (Kseq (St_goto entry) (Kseq (St_label exit St_skip) cm_k')).
335 
336
337(* The type of maps from labels to Clight continuations *)
338(* definition label_map ≝ identifier_map SymbolTag cont. *)
339
340(* Definition of the simulation relation on states. The orders of the parameters is dictated by
341 * the necessity of performing an inversion on the continuation sim relation without having to
342 * play the usual game of lapplying all previous dependent arguments.  *)
343inductive clight_cminor_rel : clight_cminor_inv → Clight_state → Cminor_state → Prop ≝
344| CMR_normal :
345  (* Relates globals to globals and functions to functions. *)
346  ∀INV:  clight_cminor_inv.
347 
348  (* ---- Statements ---- *)
349  ∀cl_s: statement.                                       (* Clight statement *) 
350  ∀cm_s: stmt.                                            (* Cminor statement *)
351
352  (* ---- Continuations ---- *)
353  ∀cl_k: cl_cont.                                      (* Clight continuation *)
354  ∀cm_k: cm_cont.                                      (* Cminor continuation *)
355  ∀cm_st: stack.                                              (* Cminor stack *)
356 
357  ∀cl_f: function.                               (* Clight enclosing function *)
358  ∀cm_f: internal_function.                             (* enclosing function *)
359  ∀frame_data: clight_cminor_data cl_f INV.
360  (*∀alloctype:  var_types.*)                       (* map from var to alloc type *)
361  ∀rettyp.                                     (* return type of the function *)
362 
363  (* ---- Relate Clight continuation to Cminor continuation ---- *)
364  clight_cminor_cont_rel INV cl_f cm_f frame_data rettyp cl_k cm_k →
365
366  (* ---- Other Cminor variables ---- *)
367  ∀fInv: stmt_inv cm_f (cm_env ?? frame_data) (f_body cm_f).             (* Cminor invariants *)
368  ∀sInv: stmt_inv cm_f (cm_env ?? frame_data) cm_s.
369  ∀kInv: cont_inv cm_f (cm_env ?? frame_data) cm_k.
370
371  (* ---- Relate return type variable to actual return type ---- *)
372  rettyp = opttyp_of_type (fn_return cl_f) →
373
374  (* ---- specification of the contents of clight environment (needed for expr sim) ---- *)
375
376  (* ---- relate Clight and Cminor functions ---- *)
377  ∀func_univ: universe SymbolTag.
378  ∀Hfresh_globals: globals_fresh_for_univ ? (globals INV) func_univ.
379  ∀Hfresh_function: fn_fresh_for_univ cl_f func_univ.
380  translate_function func_univ (globals INV) cl_f Hfresh_globals Hfresh_function = OK ? cm_f →
381
382  (* ---- relate Clight and Cminor statements ---- *)
383  ∀stmt_univ,stmt_univ': tmpgen (alloc_type ?? frame_data).
384  ∀lbl_univ,lbl_univ':   labgen.
385  ∀lbls:      lenv.
386  ∀flag:      convert_flag.
387  ∀Htranslate_inv.
388  translate_statement (alloc_type ?? frame_data) stmt_univ lbl_univ lbls flag rettyp cl_s = OK ? «〈stmt_univ',lbl_univ',cm_s〉, Htranslate_inv» →
389   
390  clight_cminor_rel INV
391    (ClState cl_f cl_s cl_k (cl_env ?? frame_data) (cl_m ?? frame_data))
392    (CmState cm_f cm_s (cm_env ?? frame_data) fInv sInv (cm_m ?? frame_data) (stackptr ?? frame_data) cm_k kInv cm_st).
393
394lemma invert_assert :
395  ∀b. ∀P. assert b P → b = true ∧ P.
396* #P whd in ⊢ (% → ?); #H
397[ @conj try @refl @H
398| @False_ind @H ]
399qed.
400
401lemma res_to_io :
402  ∀A,B:Type[0]. ∀C.
403  ∀x: res A. ∀y.
404  match x with
405  [ OK v ⇒  Value B C ? v
406  | Error m ⇒ Wrong … m ] = return y →
407  x = OK ? y.
408#A #B #C *
409[ #x #y normalize nodelta whd in ⊢ ((???%) → ?); #Heq destruct (Heq) @refl
410| #err #y normalize nodelta whd in ⊢ ((???%) → ?); #Heq destruct (Heq) ]
411qed.
412
413
414(* axiom clight_cminor_rel : clight_cminor_inv → Clight_state → Cminor_state → Prop. *)
415
416(* Conjectured simulation results
417
418   We split these based on the start state:
419   
420   1. ‘normal’ states take some [S n] normal steps and simulates them by [S m]
421      normal steps in Cminor;
422   2. call and return steps are simulated by a call/return step plus [m] normal
423      steps (to copy stack allocated parameters / results); and
424   3. lone cost label steps are simulates by a lone cost label step
425   
426   These should allow us to maintain enough structure to identify the Cminor
427   subtrace corresponding to a measurable Clight subtrace.
428 *)
429
430definition clight_normal : Clight_state → bool ≝
431λs. match Clight_classify s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ].
432
433definition cminor_normal : Cminor_state → bool ≝
434λs. match Cminor_classify s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ].
435
436
437lemma clight_cminor_normal :
438  ∀INV:clight_cminor_inv.
439  ∀s1,s1',s2,tr.
440  clight_cminor_rel INV s1 s1' →
441  clight_normal s1 = true →
442  ¬ Clight_labelled s1 →
443  ∃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〉) →
444  ∃m. after_n_steps (S m) … Cminor_exec (ge_cm INV) s1' (λs.cminor_normal s) (λtr',s2'.
445    tr = tr' ∧
446    clight_cminor_rel INV s2 s2'
447  ).
448#INV #s1 #s1' #s2 #tr #Hstate_rel #Hclight_normal #Hnot_labeleld
449inversion Hstate_rel
450#INV' #cl_s
451(* case analysis on Clight statement *)
452cases cl_s
453[ 1: | 2: #lhs #rhs | 3: #retv #func #args | 4: #stm1 #stm2 | 5: #cond #iftrue #iffalse | 6: #cond #body
454| 7: #cond #body | 8: #init #cond #step #body | 9,10: | 11: #retval | 12: #cond #switchcases | 13: #lab #body
455| 14: #lab | 15: #cost #body ]
456[ 1: (* Skip *)
457     #cm_s #cl_k #cm_k #cm_st #cl_f #cm_f #frame_data #rettyp #Hcont_rel
458     (* case analysis on continuation *)
459     inversion Hcont_rel
460     [ (* Kstop continuation *)
461       (* simplifying the goal using outcome of the inversion *)
462       #kINV #kcl_f #kcm_f #kframe_data #ktarget_type #Heq_INV
463       #Heq_cl_f #Heq_cm_f #Heq_frame #Heq_rettyp #Heq_cl_k #Heq_cm_k  #_
464       (* get rid of jmeqs and destruct *)
465       lapply (jmeq_to_eq ??? Heq_INV) -Heq_INV #Heq_INV
466       lapply (jmeq_to_eq ??? Heq_cl_f) -Heq_cl_f #Heq_cl_f
467       destruct (Heq_INV Heq_cl_f)
468       lapply (jmeq_to_eq ??? Heq_frame) -Heq_frame #Heq_frame
469       lapply (jmeq_to_eq ??? Heq_cm_f) -Heq_cm_f #Heq_cm_f
470       lapply (jmeq_to_eq ??? Heq_rettyp) -Heq_rettyp #Heq_rettypv
471       lapply (jmeq_to_eq ??? Heq_cm_k) -Heq_cm_k #Heq_cm_k
472       lapply (jmeq_to_eq ??? Heq_cl_k) -Heq_cl_k #Heq_cl_k
473       destruct (Heq_frame Heq_cl_k Heq_cm_k Heq_cm_f Heq_rettyp)
474       (* introduce everything *)
475       #fInv #sInv #kInv
476       #Htarget_type #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function
477       #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls
478       #flag * * * * #Hstmt_inv #Hlabels_translated #Htmps_preserved
479       #Hreturn_ok #Hlabel_wf
480       (* reduce statement translation function *)
481       whd in ⊢ ((??%?) → ?);
482       #Heq_translate
483       (* In this simple case, trivial translation *)
484       destruct (Heq_translate)
485       #Heq_INV' #Heq_s1 #Heq_s1'
486       lapply (jmeq_to_eq ??? Heq_INV') -Heq_INV' #Heq_INV'
487       lapply (jmeq_to_eq ??? Heq_s1) -Heq_s1 #Heq_s1
488       lapply (jmeq_to_eq ??? Heq_s1') -Heq_s1' #Heq_s1'
489       destruct (Heq_INV' Heq_s1 Heq_s1') #_
490       (* unfold the clight execution *)
491       %{0}
492       whd in ⊢ (% → ?); whd in match (step io_out io_in clight_exec ??);
493       inversion (fn_return kcl_f) normalize nodelta
494       [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
495       | #structname #fieldspec | #unionname #fieldspec | #id ]
496       #Hfn_return
497       whd in ⊢ (% → ?);
498       @False_ind
499    | (* KSeq continuation *)
500      #kINV #kcl_f #kcm_f #kframe_data #ktarget_type #kcl_s #kcm_s #kcl_k' #kcm_k'
501      #kstmt_univ #kstmt_univ' #klbl_univ #klbl_univ' #klbls #kflag
502      * * * * #kHstmt_inv #kHlabels_translated #kHtmps_preserved
503      #kHreturn_ok #kHlabel_wf #kHeq_translate #kHcont_rel #_
504      #Heq_INV #Heq_cl_f #Heq_cm_f #Heq_frame #Heq_rettyp #Heq_cl_k #Heq_cm_k  #_
505      (* get rid of jmeqs and destruct *)
506      lapply (jmeq_to_eq ??? Heq_INV) -Heq_INV #Heq_INV
507      lapply (jmeq_to_eq ??? Heq_cl_f) -Heq_cl_f #Heq_cl_f
508      destruct (Heq_INV Heq_cl_f)
509      lapply (jmeq_to_eq ??? Heq_frame) -Heq_frame #Heq_frame
510      lapply (jmeq_to_eq ??? Heq_cm_f) -Heq_cm_f #Heq_cm_f
511      lapply (jmeq_to_eq ??? Heq_rettyp) -Heq_rettyp #Heq_rettypv
512      lapply (jmeq_to_eq ??? Heq_cm_k) -Heq_cm_k #Heq_cm_k
513      lapply (jmeq_to_eq ??? Heq_cl_k) -Heq_cl_k #Heq_cl_k
514      destruct (Heq_frame Heq_cl_k Heq_cm_k Heq_cm_f Heq_rettyp)   
515      #fInv #sInv #kInv #Hktarget_type
516      #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function
517      #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls
518      #flag * * * * #Hstmt_inv #Hlabels_translated #Htmps_preserved
519      #Hreturn_ok #Hlabel_wf
520      (* reduce translation function and eliminate result *)
521      (* In this simple case, trivial translation *)
522      whd in ⊢ ((??%?) → ?); #Heq_translate
523      destruct (Heq_translate)
524      #Heq_INV' #Heq_s1 #Heq_s1'
525      lapply (jmeq_to_eq ??? Heq_INV') -Heq_INV' #Heq_INV'
526      lapply (jmeq_to_eq ??? Heq_s1) -Heq_s1 #Heq_s1
527      lapply (jmeq_to_eq ??? Heq_s1') -Heq_s1' #Heq_s1' #_
528      (* unfold the clight execution *)
529      %{0}
530      whd in ⊢ (% → ?); #Hassert
531      cases (invert_assert ?? Hassert) -Hassert #Hclight_class
532      cases (andb_inversion … Hclight_class) -Hclight_class
533      #_ #Hnot_labelled whd in ⊢ (% → ?); #Heq destruct (Heq)
534      %{0} whd in ⊢ %; @conj try @refl
535      (* close simulation *)
536      %1{kINV kHcont_rel ? ? Hfresh_globals Hfresh_function
537         Htranslate_function kstmt_univ kstmt_univ' klbl_univ klbl_univ' klbls kflag}
538      [ 3: @kHeq_translate | assumption ]
539    | (* Kwhile continuation *)
540      #kINV #kcl_f #kcm_f #kframe_data #ktarget_type
541      #kcl_k' #kcm_k' #ksz #ksg #kcl_cond_desc #kcl_body #kcm_cond #kcm_body
542      #kentry #kexit #kstmt_univ #kstmt_univ' #klbl_univ #klbl_univ' #klbl_univ''
543      #klbls #kHtranslate_inv #kHexpr_vars #kHtranslate_expr #kfInv
544      * * * * #kHentry_declared * * * *
545      * * * #kHcond_vars_declared * * * *
546      * * * #kHbody_inv * * *
547      whd in ⊢ (% → ?); #kHentry_declared'
548      * * * * * * * * *
549      whd in ⊢ (% → ?); #kHexit_declared *
550      * * * *
551      #kHcont_inv #kHmklabels #kHeq_translate #kHfind_label #kHcont_rel #_
552      #Heq_INV #Heq_cl_f #Heq_cm_f #Heq_frame #Heq_rettyp #Heq_cm_k #Heq_cl_k
553      lapply (jmeq_to_eq ??? Heq_INV) -Heq_INV #Heq_INV
554      lapply (jmeq_to_eq ??? Heq_cl_f) -Heq_cl_f #Heq_cl_f
555      destruct (Heq_INV Heq_cl_f)     
556      lapply (jmeq_to_eq ??? Heq_cm_f) -Heq_cm_f #Heq_cm_f
557      lapply (jmeq_to_eq ??? Heq_frame) -Heq_frame #Heq_frame
558      lapply (jmeq_to_eq ??? Heq_rettyp) -Heq_rettyp #Heq_rettyp
559      lapply (jmeq_to_eq ??? Heq_cm_k) -Heq_cm_k #Heq_cm_k
560      lapply (jmeq_to_eq ??? Heq_cl_k) -Heq_cl_k #Heq_cl_k #_
561      destruct (Heq_cl_k Heq_cm_k Heq_cm_f Heq_frame Heq_rettyp)
562      (* introduce state relation contents *)
563      #fInv #sInv * whd in ⊢ (% → ?); * *
564      whd in ⊢ (% → ?); * whd in ⊢ (% → ?); #Hlabel_defined * #kInv
565      #Heq_rettyp
566      #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function
567      #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls
568      #flag * * * * #Hstmt_inv #Hlabels_translated #Htmps_preserved
569      #Hreturn_ok #Hlabel_wf
570      (* reduce translation function and eliminate result *)
571      (* In this simple case, trivial translation *)
572      whd in ⊢ ((??%?) → ?); #Heq_translate
573      destruct (Heq_translate)
574      #Heq_INV' #Heq_s1 #Heq_s1'
575      lapply (jmeq_to_eq ??? Heq_INV') -Heq_INV' #Heq_INV'
576      lapply (jmeq_to_eq ??? Heq_s1) -Heq_s1 #Heq_s1
577      lapply (jmeq_to_eq ??? Heq_s1') -Heq_s1' #Heq_s1' #_
578      (* unfold the clight execution *)
579      %{1} whd in ⊢ (% → ?); #Hawait
580      cases (await_value_bind_inv … Hawait) -Hawait
581      * #cl_val #cl_trace * #Hexec_cond #Hawait
582      cases (await_value_bind_inv … Hawait) -Hawait
583      #cond_outcome * #Hcond_outcome
584      cases (eval_expr_sim … kframe_data) #Hsim_expr #_
585      (* use simulation lemma on expressions *)
586      lapply (Hsim_expr … kHtranslate_expr … kHcond_vars_declared … Hexec_cond) -Hsim_expr
587      whd in match (typeof ?) in Hcond_outcome; cases cond_outcome in Hcond_outcome;
588      #Hcond_outcome lapply (exec_bool_of_val_inversion … Hcond_outcome)
589      * [ 2,4: * #ptr * #ty' * * #_ #Habsurd destruct (Habsurd) ]
590      * [ 2,4: * #ty' * * #_ #Habsurd destruct (Habsurd) ]
591      * #vsz * #vsg * #i * * #Hcl_val #Htype_eq destruct (Hcl_val Htype_eq)
592      normalize nodelta #Hi_eq
593      * #cm_val * #Hexec_cond_cm #Hvalue_eq #Hassert
594      cases (invert_assert … Hassert) -Hassert #Handb
595      cases (andb_inversion … Handb) -Handb #_ #HClight_not_labelled
596      whd in ⊢ (% → ?); #Heq destruct (Heq)
597      [ %{5} whd whd in ⊢ (??%?); normalize nodelta
598        >kHfind_label -kHfind_label normalize nodelta
599        whd in match (proj1 ???);
600        whd in match (proj2 ???);
601        whd whd in ⊢ (??%?); normalize nodelta
602        >Hexec_cond_cm normalize nodelta
603        whd in match (m_bind ?????);
604        >(value_eq_int_inversion … Hvalue_eq)
605        whd in match (eval_bool_of_val ?); normalize nodelta
606        <Hi_eq normalize nodelta
607        whd @conj [ normalize >append_nil try @refl ]
608        whd in match (proj1 ???);
609        whd in match (proj2 ???);
610        whd whd in ⊢ (??%?); normalize nodelta
611        %{??????? kframe_data ktarget_type Hcont_rel Heq_rettyp ??? Htranslate_function
612          ??????? kHeq_translate}
613      | %{6} whd whd in ⊢ (??%?); normalize nodelta
614        >kHfind_label -kHfind_label normalize nodelta
615        whd in match (proj1 ???);
616        whd in match (proj2 ???);
617        whd whd in ⊢ (??%?); normalize nodelta
618        >Hexec_cond_cm normalize nodelta
619        whd in match (m_bind ?????);
620        >(value_eq_int_inversion … Hvalue_eq)
621        whd in match (eval_bool_of_val ?); normalize nodelta
622        <Hi_eq normalize nodelta
623        whd @conj [ normalize >append_nil >append_nil try @refl ]
624        whd in match (proj1 ???);
625        whd in match (proj2 ???);
626        whd whd in ⊢ (??%?); normalize nodelta
627        %{??????? kframe_data ktarget_type kHcont_rel Heq_rettyp ??? Htranslate_function}
628        try assumption
629        [ @conj try @conj try @conj try @conj //
630        | @refl ]
631      ]
632  (*| TODO: other continuations *)
633    ]
634| 2: (* Assign *)
635     #cm_s #cl_k #cm_k #cm_st #cl_f #cm_f #frame_data #rettyp #Hcont_rel
636     #fInv #sInv #kInv #Hrettyp #func_univ #Hfresh_globals #Hfresh_function
637     #Htranslate_function #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls #flag
638     * * * * #Hstmt_inv_cm #Huseless_hypothesis
639      #Htmps_preserved #Hreturn_ok #Hlabel_wf     
640     (* case-split on lhs in order to reduce lvalue production in Cminor *)
641     cases lhs #lhs_ed #lhs_ty
642     cases lhs_ed
643     (* intro expr contents *)
644     [ #sz #i | #var_id | #e1 | #e1 | #op #e1 |#op #e1 #e2 | #cast_ty #e1
645     | #cond #iftrue #iffalse | #e1 #e2 | #e1 #e2 | #sizeofty | #e1 #field | #cost #e1 ]
646     [ 2: #Htranslate_statement
647          cases (bind_inversion ????? Htranslate_statement)
648          * #cm_rhs #Hexpr_vars_rhs * #Htranslate_rhs #Htranslate_statement'
649          cases (bind_inversion ????? Htranslate_statement')
650          #lhs_dest * #Htranslate_lhs
651          cases (bind2_eq_inversion ?????? Htranslate_lhs) -Htranslate_lhs
652          #alloctype * #type_of_var * #Hlookup_var_success
653          cases alloctype in Hlookup_var_success;
654          normalize nodelta
655          [ 1: (* Global *) #r
656               #Hlookup_var_success whd in ⊢ ((???%) → ?); #Hlhs_dest_eq
657               destruct (Hlhs_dest_eq) normalize nodelta
658               whd in match (proj1 ???); whd in match (proj2 ???);
659               whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
660               #Heq_INV #Heq_s1 #Heq_s1'
661               lapply (jmeq_to_eq ??? Heq_INV) -Heq_INV #Heq_INV
662               lapply (jmeq_to_eq ??? Heq_s1) -Heq_s1 #Heq_s1
663               lapply (jmeq_to_eq ??? Heq_s1') -Heq_s1' #Heq_s1'
664               destruct (Heq_INV Heq_s1 Heq_s1') #_
665               %{1} whd in ⊢ (% → ?); #Hawait
666               cases (await_value_bind_inv … Hawait) -Hawait
667               * * #cl_blo #cl_off #cl_tr * whd in ⊢ ((??%?) → ?);
668               #Hexec_lvalue
669               lapply (res_to_io ????? Hexec_lvalue) -Hexec_lvalue #Hexec_lvalue
670               #Hawait
671               cases (await_value_bind_inv … Hawait) -Hawait
672               * #rhs_val #rhs_trace * #Hexec_rhs_trace #Hawait
673               cases (await_value_bind_inv … Hawait) -Hawait
674               #mem_after_store * #Hstore_value #Hawait
675               lapply (opt_to_io_Value ?????? Hstore_value) -Hstore_value #Hstore_value
676               -Htranslate_statement' -Htranslate_statement
677               cases (invert_assert … Hawait) -Hawait #Handb
678               cases (andb_inversion … Handb) -Handb #_ #HClight_not_labelled #Hawait               
679               (* TODO: use the memory injection to handle the store,
680                  use INV contents to match up CL global with CM one.
681                  Note to self: globals should be exactly matched in CL and CM,
682                  maybe memory_injection is not useful in this particular case,
683                  only in Stack and Local cases.
684                * *)
685               @cthulhu
686          | 2: (* Stack *) #n @cthulhu
687          | 3: (* Local *) @cthulhu
688          ]
689     | *: (* memdest *) @cthulhu ]     
690| *: @cthulhu
691] qed.
692
693axiom clight_cminor_call_return :
694  ∀INV:clight_cminor_inv.
695  ∀s1,s1',s2,tr.
696  clight_cminor_rel INV s1 s1' →
697  match Clight_classify s1 with [ cl_call ⇒ true | cl_return ⇒ true | _ ⇒ false ] →
698  after_n_steps 1 … clight_exec (ge_cl INV) s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) →
699  ∃m. after_n_steps (S m) … Cminor_exec (ge_cm INV) s1' (λs.cminor_normal s) (λtr',s2'.
700    tr = tr' ∧
701    clight_cminor_rel INV s2 s2'
702  ).
703
704axiom clight_cminor_cost :
705  ∀INV:clight_cminor_inv.
706  ∀s1,s1',s2,tr.
707  clight_cminor_rel INV s1 s1' →
708  Clight_labelled s1 →
709  after_n_steps 1 … clight_exec (ge_cl INV) s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) →
710  after_n_steps 1 … Cminor_exec (ge_cm INV) s1' (λs.true) (λtr',s2'.
711    tr = tr' ∧
712    clight_cminor_rel INV s2 s2'
713  ).
714
715axiom clight_cminor_init : ∀cl_program,cm_program,s,s'.
716  clight_to_cminor cl_program = OK ? cm_program →
717  make_initial_state ?? clight_fullexec cl_program = OK ? s →
718  make_initial_state ?? Cminor_fullexec cm_program = OK ? s' →
719  ∃INV. clight_cminor_rel INV s s'.
Note: See TracBrowser for help on using the repository browser.