source: src/Clight/toCminorCorrectness.ma @ 2768

Last change on this file since 2768 was 2737, checked in by garnier, 7 years ago

Commit of current proof state for Clight to Cminor translation.

File size: 53.4 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".
7include "common/Measurable.ma".
8
9(* Expr simulation. Contains important definitions for statements, too.  *)
10include "Clight/toCminorCorrectnessExpr.ma".
11
12(* When we characterise the local Clight variables, those that are stack
13   allocated are given disjoint regions of the stack. *)
14lemma characterise_vars_disjoint : ∀globals,f,vartypes,stacksize,id,n,ty.
15  characterise_vars globals f = 〈vartypes, stacksize〉 →
16  lookup ?? vartypes id = Some ? 〈Stack n,ty〉 →
17  ∀id',n',ty'. id ≠ id' →
18  lookup ?? vartypes id' = Some ? 〈Stack n',ty'〉 →
19  n' + sizeof ty' ≤ n ∨ n + sizeof ty ≤ n'.
20#globals * #ret #args #vars #body #vartypes #stacksize #id #n #ty
21whd in ⊢ (??%? → ?);
22generalize in match vartypes; -vartypes
23generalize in match stacksize; -stacksize
24elim (args@vars)
25[ #stacksize #vartypes #CHAR #L @⊥ whd in CHAR:(??%?); destruct
26  elim globals in L;
27  [ normalize #L destruct
28  | * * #id' #r #ty' #tl #IH
29    whd in match (foldr ?????);
30    #L cases (lookup_add_cases ??????? L)
31    [ * #E1 #E2 destruct
32    | @IH
33    ]
34  ]
35| * #id1 #ty1 #tl #IH #stacksize #vartypes
36  whd in match (foldr ?????);
37  (* Avoid writing out the definition again *)
38  letin ih ≝ (foldr ? (Prod ??) ?? tl) in IH ⊢ %;
39  lapply (refl ? ih) whd in match ih; -ih
40  cases (foldr ? (Prod ??) ?? tl) in ⊢ (???% → %);
41  #vartypes' #stack' #FOLD #IH
42  whd in ⊢ (??(match % with [_⇒?])? → ?);
43  cases (orb ??)
44  #CHAR whd in CHAR:(??%?); destruct
45  #L cases (lookup_add_cases ??????? L)
46  [ 1,3: * #E1 #E2 destruct
47    #id' #n' #ty' #NE >lookup_add_miss /2/
48    #L' %1 -L -IH
49    generalize in match vartypes' in FOLD L' ⊢ %; -vartypes'
50    generalize in match stack'; -stack'
51    elim tl
52    [ #stack' #vartypes2 whd in ⊢ (??%? → ?); #F destruct #L' @⊥
53      elim globals in L';
54      [ normalize #E destruct
55      | * * #id2 #r2 #ty2 #tl2 #IH whd in match (foldr ?????);
56        #L cases (lookup_add_cases ??????? L)
57        [ * #E1 #E2 destruct
58        | @IH
59        ]
60      ]
61    | * #id2 #ty2 #tl2 #IH #stack' #vartypes'
62      whd in ⊢ (??%? → ?); cases (foldr ? (Prod ??) ???) in IH ⊢ %;
63      #vartypes2 #stack2 #IH
64      whd in ⊢ (??%? → ?);
65      cases (orb ??)
66      [ #E whd in E:(??%?); destruct #L cases (lookup_add_cases ??????? L)
67        [ * #E1 #E2 destruct //
68        | #L'' lapply (IH ?? (refl ??) L'') /2/
69        ]
70      | #E whd in E:(??%?); destruct #L cases (lookup_add_cases ??????? L)
71        [ * #E1 #E2 destruct
72        | #L'' lapply (IH ?? (refl ??) L'') /2/
73        ]
74      ]
75    ]
76  | -L #L #id' #n' #ty' #NE #L'
77    cases (lookup_add_cases ??????? L')
78    [ * #E1 #E2 destruct
79      %2 -IH -L'
80      generalize in match vartypes' in FOLD L; -vartypes'
81      generalize in match stack'; -stack'
82      elim tl
83      [ #stack' #vartypes' whd in ⊢ (??%? → ?); #F destruct #L @⊥
84        elim globals in L;
85        [ normalize #E destruct
86        | * * #id1 #r1 #ty1 #tl1 #IH whd in match (foldr ?????);
87          #L cases (lookup_add_cases ??????? L)
88          [ * #E1 #E2 destruct
89          | @IH
90          ]
91        ]
92      | * #id1 #ty1 #tl1 #IH #stack' #vartypes'
93        whd in ⊢ (??%? → ?); cases (foldr ? (Prod ??) ???) in IH ⊢ %;
94        #vartypes2 #stack2 #IH
95        whd in ⊢ (??%? → ?);
96        cases (orb ??)
97        #E whd in E:(??%?); destruct
98        #L cases (lookup_add_cases ??????? L)
99        [ 1,3: * #E1 #E2 destruct //
100        | 2,4: #L' lapply (IH ?? (refl ??) L') /2/
101        ]
102      ]
103    | @(IH … (refl ??) L … NE)
104    ]
105  | -L #L #id' #n' #ty' #NE #L'
106    cases (lookup_add_cases ??????? L')
107    [ * #E1 #E2 destruct
108    | @(IH … (refl ??) L … NE)
109    ]
110  ]
111] qed.
112
113(* And everything is in the stack frame. *)
114
115lemma characterise_vars_in_range : ∀globals,f,vartypes,stacksize,id,n,ty.
116  characterise_vars globals f = 〈vartypes, stacksize〉 →
117  lookup ?? vartypes id = Some ? 〈Stack n,ty〉 →
118  n + sizeof ty ≤ stacksize.
119#globals * #ret #args #vars #body whd in match (characterise_vars ??);
120elim (args@vars)
121[ #vartypes #stacksize #id #n #ty #FOLD #L @⊥
122  whd in FOLD:(??%?); destruct elim globals in L;
123  [ #E normalize in E; destruct
124  | * * #id' #r' #ty' #tl' #IH
125    whd in match (foldr ?????); #L cases (lookup_add_cases ??????? L)
126    [ * #E1 #E2 destruct
127    | @IH
128    ]
129  ]
130| * #id' #ty' #tl #IH #vartypes #stacksize #id #n #ty
131  whd in match (foldr ?????); cases (foldr ? (Prod ??) ???) in IH ⊢ %;
132  #vartypes' #stackspace' #IH
133  whd in ⊢ (??(match % with [_⇒?])? → ?);
134  cases (orb ??) whd in ⊢ (??%? → ?);
135  #E destruct #L cases (lookup_add_cases ??????? L)
136  [ 1,3: * #E1 #E2 destruct //
137  | 2,4: #L' lapply (IH … (refl ??) L') /2/
138  ]
139] qed.
140
141
142
143(* Put knowledge that Globals are global into a more useful form than the
144   one used for the invariant. *)   
145(* XXX superfluous lemma ? Commenting it for now.
146       if not superfluous : move to toCminorCorrectnessExpr.ma, after
147       [characterise_vars_localid] *)
148(*
149lemma characterise_vars_global : ∀globals,f,vartypes,stacksize.
150  characterise_vars globals f = 〈vartypes, stacksize〉 →
151  ∀id,r,ty. lookup' vartypes id = OK ? 〈Global r,ty〉 →
152  Exists ? (λx.x = 〈〈id,r〉,ty〉) globals ∧
153  ¬ Exists ? (λx. \fst x = id) (fn_params f @ fn_vars f).
154#globals #f #vartypes #stacksize #CHAR #id #r #ty #L
155cases (characterise_vars_src … CHAR id ?)
156[ * #r' * #ty' >L
157  * #E1 destruct (E1) #EX
158  %
159  [ @EX
160  | % #EX' cases (characterise_vars_localid … CHAR EX')
161    #ty' whd in ⊢ (% → ?); >L *
162  ]
163| * #ty' whd in ⊢ (% → ?); >L *
164| whd >(opt_eq_from_res ???? L) % #E destruct
165] qed. *)
166
167(* Show how the global environments match up. *)
168
169lemma map_partial_All_to_All2 : ∀A,B,P,f,l,H,l'.
170  map_partial_All A B P f l H = OK ? l' →
171  All2 ?? (λa,b. ∃p. f a p = OK ? b) l l'.
172#A #B #P #f #l
173elim l
174[ #H #l' #MAP normalize in MAP; destruct //
175| #h #t #IH * #p #H #l'
176  whd in ⊢ (??%? → ?);
177  lapply (refl ? (f h p)) whd in match (proj1 ???);
178  cases (f h p) in ⊢ (???% → %);
179  [ #b #E #MAP cases (bind_inversion ????? MAP)
180    #tl' * #MAP' #E' normalize in E'; destruct
181    % [ %{p} @E | @IH [ @H | @MAP' ] ]
182  | #m #_ #X normalize in X; destruct
183  ]
184] qed.
185 
186
187definition clight_cminor_matching : clight_program → matching ≝
188λp.
189  let tmpuniverse ≝ universe_for_program p in
190  let fun_globals ≝ map ?? (λidf. 〈\fst idf,Code,type_of_fundef (\snd idf)〉) (prog_funct ?? p) in
191  let var_globals ≝ map ?? (λv. 〈\fst (\fst v), \snd (\fst v), \snd (\snd v)〉) (prog_vars ?? p) in
192  let globals ≝ fun_globals @ var_globals in
193  mk_matching
194    ?? (list init_data × type) (list init_data)
195    (λvs,f_clight,f_cminor. ∃H1,H2. translate_fundef tmpuniverse globals H1 f_clight H2 = OK ? f_cminor)
196    (λv,w. \fst v = w).
197
198lemma clight_to_cminor_varnames : ∀p,p'.
199  clight_to_cminor p = OK ? p' →
200  prog_var_names … p = prog_var_names … p'.
201* #vars #fns #main * #vars' #fns' #main'
202#TO cases (bind_inversion ????? TO) #fns'' * #MAP #E
203whd in E:(??%%); destruct
204-MAP normalize
205elim vars
206[ //
207| * * #id #r * #d #t #tl #IH normalize >IH //
208] qed.
209
210lemma clight_to_cminor_matches : ∀p,p'.
211  clight_to_cminor p = OK ? p' →
212  match_program (clight_cminor_matching p) p p'.
213* #vars #fns #main * #vars' #fns' #main'
214#TO cases (bind_inversion ????? TO) #fns'' * #MAP #E
215whd in E:(??%%); destruct
216%
217[ -MAP whd in match (m_V ?); whd in match (m_W ?);
218  elim vars
219  [ //
220  | * * #id #r * #init #ty #tl #IH %
221    [ % //
222    | @(All2_mp … IH) * * #a #b * #c #d * * #e #f #g * /2/
223    ]
224  ]
225| @(All2_mp … (map_partial_All_to_All2 … MAP)) -MAP
226  * #id #f * #id' #f' * #H #F cases (bind_inversion ????? F) #f'' * #TRANSF #E
227  normalize in E; destruct
228  <(clight_to_cminor_varnames … TO)
229  % whd
230  % [2: % [2: @TRANSF | skip ] | skip ]
231| %
232] qed.
233
234(* A measure on Clight states that is decreasing along execution sequences *)
235
236(* statements *)
237let rec measure_Clight_statement (s : statement) : ℕ ≝
238match s with
239[ Sskip ⇒ 0
240| Ssequence s1 s2 ⇒
241  measure_Clight_statement s1 + measure_Clight_statement s2 + 1
242| Sifthenelse e s1 s2 =>
243  measure_Clight_statement s1 + measure_Clight_statement s2 + 1
244| Swhile e s =>
245  measure_Clight_statement s + 1
246| Sdowhile e s =>
247  measure_Clight_statement s + 1
248| Sfor s1 e s2 s3 =>
249  measure_Clight_statement s1 +
250  measure_Clight_statement s2 +
251  measure_Clight_statement s3 + 1
252| Sswitch e ls =>
253  measure_Clight_ls ls + 1
254| Slabel l s =>
255  measure_Clight_statement s + 1
256| Scost cl s =>
257  measure_Clight_statement s + 1
258| _ => 1
259]
260and measure_Clight_ls (ls : labeled_statements) : ℕ :=
261match ls with
262[ LSdefault s =>
263  measure_Clight_statement s
264| LScase sz i s ls =>
265  measure_Clight_statement s +
266  measure_Clight_ls ls
267].
268
269(* continuations *)
270let rec measure_Clight_cont (cont : cl_cont) : ℕ ≝
271match cont with
272[ Kstop => 0
273| Kseq s k =>
274  measure_Clight_statement s +
275  measure_Clight_cont k + 1
276| Kwhile e s k =>
277  measure_Clight_statement s +
278  measure_Clight_cont k + 1
279| Kdowhile e s k =>
280  measure_Clight_statement s +
281  measure_Clight_cont k + 1
282| Kfor2 e s1 s2 k =>
283  measure_Clight_statement s1 +
284  measure_Clight_statement s2 +
285  measure_Clight_cont k + 1
286| Kfor3 e s1 s2 k =>
287  measure_Clight_statement s1 +
288  measure_Clight_statement s2 +
289  measure_Clight_cont k + 1
290| Kswitch k =>
291  measure_Clight_cont k + 1
292| Kcall retaddr f e k =>
293  measure_Clight_statement (fn_body f) +
294  measure_Clight_cont k + 1
295].
296
297(* Shamelessly copying Compcert. *)
298definition measure_Clight : Clight_state → ℕ × ℕ ≝
299λstate.
300match state with
301[ State f s k e m ⇒
302  〈measure_Clight_statement s + measure_Clight_cont k + 1, measure_Clight_statement s + 1〉
303| Callstate fb fd args k m ⇒ 〈0, 0〉
304| Returnstate res k m ⇒ 〈0, 0〉
305| Finalstate r ⇒ 〈0, 0〉
306].
307
308(* Stuff on lexicographic orders *)
309definition lexicographic : ∀A:Type[0]. (A → A → Prop) → A × A → A × A → Prop ≝
310λA,Ord, x, y.
311  let 〈xa, xb〉 ≝ x in
312  let 〈ya, yb〉 ≝ y in
313  Ord xa ya ∨ (xa = ya ∧ Ord xb yb).
314
315definition lex_lt ≝ lexicographic nat lt.
316
317
318(* relate Clight continuations and Cminor ones. *)
319inductive clight_cminor_cont_rel :
320  ∀cl_ge, cm_ge.
321  ∀INV:  clight_cminor_inv cl_ge cm_ge.     (* stuff on global variables and functions (matching between CL and CM) *)
322  ∀cl_f: function.                          (* current Clight function *)
323  internal_function →                       (* current Cminor function *)
324  clight_cminor_data cl_f cl_ge cm_ge INV → (* data for the current stack frame in CL and CM *)
325  option typ →                              (* optional target type - uniform over a given function *)
326  cl_cont →                                 (* CL cont *)
327  cm_cont →                                 (* CM cont *)
328  Prop ≝
329| ClCm_cont_stop:
330  ∀cl_ge, cm_ge, INV, cl_f, cm_f, frame_data, target_type.
331  clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f frame_data target_type Kstop Kend
332| ClCm_cont_seq:
333  ∀cl_ge, cm_ge, INV, cl_f, cm_f, frame_data, target_type.
334  ∀cl_s: statement.
335  ∀cm_s: stmt.
336  ∀cl_k':  cl_cont.
337  ∀cm_k':  cm_cont.
338  ∀stmt_univ, stmt_univ'.
339  ∀lbl_univ, lbl_univ'.
340  ∀lbls.
341  ∀flag.
342  ∀Htranslate_inv.
343  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» →
344  clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f frame_data target_type cl_k' cm_k' →
345  clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f frame_data target_type (ClKseq cl_s cl_k') (Kseq cm_s cm_k')
346| ClCm_cont_while:
347  (* Inductive family parameters *)
348  ∀cl_ge, cm_ge, INV, cl_f, cm_f, frame_data, target_type.
349
350  (* sub-continuations *)
351  ∀cl_k': cl_cont.
352  ∀cm_k': cm_cont.
353
354  (* elements of the source while statement *)
355  ∀sz,sg.
356  ∀cl_cond_desc.
357  ∀cl_body.
358
359  (* elements of the converted while statement *)
360  ∀cm_cond: CMexpr (ASTint sz sg).
361  ∀cm_body.
362  ∀entry,exit: identifier Label.
363 
364  (* universes used to generate fresh labels and variables *) 
365  ∀stmt_univ, stmt_univ'.
366  ∀lbl_univ, lbl_univ', lbl_univ''.
367  ∀lbls: lenv.
368  ∀Htranslate_inv.
369
370  (* relate CL and CM expressions *)
371  ∀Hexpr_vars.
372  translate_expr (alloc_type … frame_data) (Expr cl_cond_desc (Tint sz sg)) = OK ? («cm_cond, Hexpr_vars») →
373
374  (* Parameters and results to find_label_always *)
375  ∀sInv: stmt_inv cm_f (cm_env … frame_data) (f_body cm_f).
376  ∀Hinv.
377
378  (* Specify how the labels for the while-replacing gotos are produced *)
379  mklabels lbl_univ = 〈〈entry, exit〉, lbl_univ'〉 →
380  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» →
381  find_label_always entry (f_body cm_f) Kend (proj2 … (proj1 … (proj1 … Hinv))) cm_f (cm_env … frame_data) sInv I =
382    «〈St_label entry
383          (St_seq
384            (St_ifthenelse ?? cm_cond (St_seq cm_body (St_goto entry)) St_skip)
385            (St_label exit St_skip)), cm_k'〉, Hinv» →
386  clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f frame_data target_type cl_k' cm_k' →
387  clight_cminor_cont_rel cl_ge cm_ge 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')).
388
389(* Definition of the simulation relation on states. The orders of the parameters is dictated by
390 * the necessity of performing an inversion on the continuation sim relation without having to
391 * play the usual game of lapplying all previous dependent arguments.  *)
392inductive clight_cminor_rel : ∀cl_ge, cm_ge. clight_cminor_inv cl_ge cm_ge  → Clight_state → Cminor_state → Prop ≝
393| CMR_normal :
394  ∀cl_ge, cm_ge.
395  (* Relates globals to globals and functions to functions. *)
396  ∀INV:  clight_cminor_inv cl_ge cm_ge.
397 
398  (* ---- Statements ---- *)
399  ∀cl_s: statement.                                       (* Clight statement *) 
400  ∀cm_s: stmt.                                            (* Cminor statement *)
401
402  (* ---- Continuations ---- *)
403  ∀cl_k: cl_cont.                                      (* Clight continuation *)
404  ∀cm_k: cm_cont.                                      (* Cminor continuation *)
405  ∀cm_st: stack.                                              (* Cminor stack *)
406 
407  ∀cl_f: function.                               (* Clight enclosing function *)
408  ∀cm_f: internal_function.                             (* enclosing function *)
409  ∀frame_data: clight_cminor_data cl_f ?? INV.
410  ∀rettyp.                                     (* return type of the function *)
411 
412  (* ---- Relate Clight continuation to Cminor continuation ---- *)
413  clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f frame_data rettyp cl_k cm_k →
414
415  (* ---- Other Cminor variables ---- *)
416  ∀fInv: stmt_inv cm_f (cm_env … frame_data) (f_body cm_f).             (* Cminor invariants *)
417  ∀sInv: stmt_inv cm_f (cm_env … frame_data) cm_s.
418  ∀kInv: cont_inv cm_f (cm_env … frame_data) cm_k.
419
420  (* ---- Relate return type variable to actual return type ---- *)
421  rettyp = opttyp_of_type (fn_return cl_f) →
422
423  (* ---- specification of the contents of clight environment (needed for expr sim) ---- *)
424
425  (* ---- relate Clight and Cminor functions ---- *)
426  ∀func_univ: universe SymbolTag.
427  ∀Hfresh_globals: globals_fresh_for_univ ? (globals ?? INV) func_univ.
428  ∀Hfresh_function: fn_fresh_for_univ cl_f func_univ.
429  translate_function func_univ (globals ?? INV) cl_f Hfresh_globals Hfresh_function = OK ? cm_f →
430
431  (* ---- relate Clight and Cminor statements ---- *)
432  ∀stmt_univ,stmt_univ': tmpgen (alloc_type … frame_data).
433  ∀lbl_univ,lbl_univ':   labgen.
434  ∀lbls:      lenv.
435  ∀flag:      convert_flag.
436  ∀Htranslate_inv.
437  translate_statement (alloc_type … frame_data) stmt_univ lbl_univ lbls flag rettyp cl_s = OK ? «〈stmt_univ',lbl_univ',cm_s〉, Htranslate_inv» →
438   
439  clight_cminor_rel cl_ge cm_ge INV
440    (ClState cl_f cl_s cl_k (cl_env … frame_data) (cl_m … frame_data))
441    (CmState cm_f cm_s (cm_env … frame_data) fInv sInv (cm_m … frame_data) (stackptr … frame_data) cm_k kInv cm_st)
442
443| CMR_return :
444  ∀cl_ge, cm_ge, cl_f.
445  ∀INV:  clight_cminor_inv cl_ge cm_ge.
446  ∀frame_data: clight_cminor_data cl_f ?? INV.
447  ∀cl_mem, cm_mem.
448  cl_mem = cl_m … frame_data →
449  cm_mem = cm_m … frame_data →
450  ∀cm_st: stack.                                              (* Cminor stack *)
451  clight_cminor_rel cl_ge cm_ge INV
452    (ClReturnstate Vundef Kstop cl_mem)
453    (CmReturnstate (None val) cm_mem cm_st)
454   
455| CMR_call :
456 ∀cl_ge, cm_ge, cl_f, cm_f.
457 ∀INV: clight_cminor_inv cl_ge cm_ge.
458 ∀frame_data: clight_cminor_data cl_f cl_ge cm_ge INV.
459 ∀u: universe SymbolTag.
460 ∀cl_fundef, cm_fundef.
461 ∀Hglobals_fresh: globals_fresh_for_univ type (globals cl_ge cm_ge INV) u.
462 ∀Hfundef_fresh:  fd_fresh_for_univ cl_fundef u.
463 ∀rettyp. rettyp = opttyp_of_type (fn_return cl_f) →
464 ∀cl_k, cm_k.
465 clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f frame_data rettyp cl_k cm_k →
466 ∀fblock.
467 match cl_fundef with
468 [ CL_Internal cl_function ⇒
469   find_funct clight_fundef cl_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? (CL_Internal cl_function) ∧
470   find_funct (fundef internal_function) cm_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? cm_fundef ∧
471   translate_fundef u (globals ?? INV) Hglobals_fresh cl_fundef Hfundef_fresh = OK ? cm_fundef
472 | CL_External name argtypes rettype ⇒
473   True
474 ] →
475 ∀fptr_block.
476 ∀sInv, fInv, kInv.
477 ∀cl_args_values, cm_args_values.
478 (* TODO: add invariant All2 value_eq cl_args_values cm_args_values *)
479 ∀cm_stack.
480 clight_cminor_rel cl_ge cm_ge INV
481  (ClCallstate (Vptr (mk_pointer fptr_block zero_offset))
482   cl_fundef cl_args_values
483   (Kcall (None (block×offset×type)) cl_f (cl_env ???? frame_data) cl_k)
484   (cl_m ???? frame_data))
485  (CmCallstate (Vptr (mk_pointer fptr_block zero_offset)) cm_fundef
486   cm_args_values (cm_m ???? frame_data)
487   (Scall (None (ident×typ)) cm_f (stackptr ???? frame_data) (cm_env ???? frame_data) sInv fInv cm_k kInv cm_stack)).
488
489definition clight_normal : Clight_state → bool ≝
490λs. match Clight_classify s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ].
491
492definition cminor_normal : Cminor_state → bool ≝
493λs. match Cminor_classify s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ].
494
495definition cl_pre : preclassified_system ≝
496  mk_preclassified_system
497    clight_fullexec
498    (λg. Clight_labelled)
499    (λg. Clight_classify)
500    (λf,g,s,H. 0). (* XXX TODO *)
501
502definition cm_pre : preclassified_system ≝
503  mk_preclassified_system
504    Cminor_fullexec
505    (λg. Cminor_labelled)
506    (λg. Cminor_classify)
507    (λf,g,s,H. 0).   (* XXX TODO *)
508
509(* Auxilliary lemmas. *)
510
511lemma invert_assert :
512  ∀b. ∀P. assert b P → b = true ∧ P.
513* #P whd in ⊢ (% → ?); #H
514[ @conj try @refl @H
515| @False_ind @H ]
516qed.
517
518lemma res_to_io :
519  ∀A,B:Type[0]. ∀C.
520  ∀x: res A. ∀y.
521  match x with
522  [ OK v ⇒  Value B C ? v
523  | Error m ⇒ Wrong … m ] = return y →
524  x = OK ? y.
525#A #B #C *
526[ #x #y normalize nodelta whd in ⊢ ((???%) → ?); #Heq destruct (Heq) @refl
527| #err #y normalize nodelta whd in ⊢ ((???%) → ?); #Heq destruct (Heq) ]
528qed.
529
530lemma jmeq_absorb : ∀A:Type[0]. ∀a,b: A. ∀P:Prop. (a = b → P) → a ≃ b → P.
531#A #a #b #P #H #Heq lapply (jmeq_to_eq ??? Heq) #Heq' @H @Heq' qed.
532
533(* wrap up some trivial bit of reasoning to alleviate strange destruct behaviour *)
534lemma pair_eq_split :
535  ∀A,B:Type[0]. ∀a1,a2:A. ∀b1,b2:B.
536  〈a1,b1〉 = 〈a2, b2〉 →
537  a1 = a2 ∧ b1 = b2.
538#A #B #a1 #a2 #b1 #b2 #Heq destruct (Heq) @conj try @refl
539qed.
540
541lemma ok_eq_ok_destruct :
542  ∀A:Type[0]. ∀a,b:A. OK ? a = OK ? b → a = b.
543#H1 #H2 #H3 #H4 destruct @refl qed.
544
545lemma sigma_eq_destruct  : ∀A:Type[0]. ∀a,b:A. ∀P: A → Prop. ∀Ha: P a. ∀Hb: P b.  «a, Ha» = «b,Hb» → a = b ∧ Ha ≃ Hb.
546#A #a #b #P #Ha #Hb #Heq destruct (Heq)
547@conj try %
548qed.
549
550(* inverting find_funct and find_funct_ptr *)
551lemma find_funct_inversion :
552  ∀F: Type[0]. ∀ge: genv_t F. ∀v: val. ∀res: F.
553      find_funct F ge v = Some ? res →
554      (∃ptr. v = Vptr ptr ∧
555            (poff ptr) = zero_offset ∧
556            block_region (pblock ptr) = Code ∧
557            (∃p. block_id (pblock ptr) = neg p ∧
558                 lookup_opt … p (functions … ge) = Some ? res)).
559#F #ge #v #res
560cases v
561[ | #sz #i | | #ptr ]
562whd in ⊢ ((??%?) → ?);
563#Heq destruct (Heq)
564%{ptr} @conj try @conj try @conj try @refl
565lapply Heq -Heq
566@(eq_offset_elim … (poff ptr) zero_offset) //
567normalize nodelta
568[ 1,3,5: #_ #Habsurd destruct (Habsurd) ]
569#Heq destruct (Heq)
570whd in ⊢ ((??%?) → ?);
571cases ptr #blo #off cases (block_region blo) normalize nodelta
572[ 1,3: #Habsurd destruct (Habsurd) ]
573[ // ]
574cases (block_id blo) normalize nodelta
575[ #Habsurd destruct (Habsurd) | #p #Habsurd destruct (Habsurd) ]
576#p #Hlookup %{p} @conj try @refl assumption
577qed.
578
579(* We should be able to prove that ty = ty' with some more hypotheses, if needed. *)
580lemma translate_dest_id_inversion :
581  ∀var_types, e, var_id, ty,H.
582   translate_dest var_types e = return IdDest var_types var_id ty H →
583   e = Expr (Evar var_id) (typeof e).
584@cthulhu
585(*   
586#vars #e #var_id #ty #H
587cases e #ed #ty'
588cases ed
589[ #sz #i | #id | #e1 | #e1 | #op #e1 |#op #e1 #e2 | #cast_ty #e1
590| #cond #iftrue #iffalse | #e1 #e2 | #e1 #e2 | #sizeofty | #e1 #field | #cost #e1 ]
591whd in ⊢ ((??%%) → ?);
592#Heq
593[ 1,4,5,6,7,8,9,10,11,13: destruct (Heq)
594| 3,12: cases (bind_inversion ????? Heq) * #H1 #H2 #H3 cases H3
595        #_ whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) ]
596lapply Heq -Heq
597change with (bind2_eq ????? ) in ⊢ ((??%?) → ?); #Heq
598cases (bind2_eq_inversion ?????? Heq)
599#alloctype
600(* * #alloctype *) * #typ' *
601cases alloctype
602[ #r | #n | ] normalize nodelta #Hlookup'
603[ 1,2: whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) ]
604whd in ⊢ ((??%%) → ?); #Heq' destruct (Heq')
605@refl*)
606qed.
607
608
609(* Note: duplicate in switchRemoval.ma *)
610lemma fresh_elim : ∀u. ∃fv',u'. fresh SymbolTag u = 〈fv', u'〉. #u /3 by ex_intro/ qed.
611
612lemma breakup_dependent_match_on_pairs :
613 ∀A,B,C: Type[0].
614 ∀term: A × B.
615 ∀F: ∀x,y. 〈x, y〉 = term → C.
616 ∀z:C.
617 match term
618 return λx.x = term → ? with
619 [ mk_Prod x y ⇒ λEq. F x y Eq ] (refl ? term) = z →
620 ∃xa,xb,H. term = 〈xa, xb〉 ∧
621           F xa xb H = z.
622#A #B #C * #xa #xb #F #z normalize nodelta #H %{xa} %{xb} %{(refl ??)} @conj try @conj
623// qed.
624
625
626lemma translate_expr_sigma_welltyped : ∀vars, cl_expr, cm_expr.
627  translate_expr_sigma vars cl_expr = OK ? cm_expr →
628  dpi1 ?? (pi1 ?? cm_expr) = typ_of_type (typeof cl_expr).
629#vars #cl_expr * * #typ #cm_expr normalize nodelta #Hexpr_vars
630whd in ⊢ ((??%?) → ?); #H
631cases (bind_inversion ????? H) -H * #cm_expr' #Hexpr_vars' *
632#Htranslate_expr
633whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) @refl
634qed.
635
636lemma translate_exprlist_sigma_welltyped :
637  ∀vars, cl_exprs, cm_exprs.
638  mmap_sigma ??? (translate_expr_sigma vars) cl_exprs = OK ? cm_exprs →
639  All2 ?? (λcl, cm. dpi1 ?? cm = typ_of_type (typeof cl)) cl_exprs (pi1 ?? cm_exprs).
640#vars #cl_exprs
641elim cl_exprs
642[ * #cm_exprs #Hall whd in ⊢ ((??%?) → ?); #Heq destruct (Heq) @I
643| #hd #tl #Hind * #cm_exprs #Hall #H
644  cases (bind_inversion ????? H) -H
645  * * #cm_typ #cm_expr normalize nodelta
646  #Hexpr_vars_cm * #Htranslate_hd
647  lapply (translate_expr_sigma_welltyped … Htranslate_hd)
648  #Heq_cm_typ #H
649  cases (bind_inversion ????? H) -H
650  #cm_tail lapply (Hind cm_tail) cases cm_tail
651  #cm_tail_expr #Hall_tail -Hind #Hind * #Heq_cm_tail normalize nodelta
652   whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) whd @conj
653   [ @Heq_cm_typ
654   | @Hind assumption ]
655] qed.
656
657lemma translate_dest_MemDest_simulation :
658  ∀f.
659  ∀cl_ge : genv_t clight_fundef.
660  ∀cm_ge : genv_t (fundef internal_function).
661  ∀INV   : clight_cminor_inv cl_ge cm_ge.
662  ∀frame_data : clight_cminor_data f cl_ge cm_ge INV.
663  ∀cl_expr. ∀cm_expr.
664  ∀cl_block, cl_offset, trace.
665  ∀Hyp_present.
666     translate_dest (alloc_type … frame_data) cl_expr = OK ? (MemDest ? cm_expr) →
667     exec_lvalue cl_ge (cl_env … frame_data) (cl_m … frame_data) cl_expr = OK ? 〈〈cl_block, cl_offset〉, trace〉 →
668     ∃cm_val. eval_expr cm_ge ASTptr cm_expr (cm_env … frame_data) Hyp_present (stackptr … frame_data) (cm_m … frame_data) = OK ? 〈trace, cm_val〉 ∧
669              value_eq (Em … frame_data) (Vptr (mk_pointer cl_block cl_offset)) cm_val.     
670#f #cl_ge #cm_ge #INV #frame_data #cl_expr * #cm_expr #Hexpr_vars #cl_block #cl_offset #trace #Hyp_present
671whd in match (translate_dest ??); cases cl_expr #cl_desc #cl_typ normalize nodelta
672cases cl_desc normalize nodelta
673[ #sz #i | #id | #e1 | #e1 | #op #e1 |#op #e1 #e2 | #cast_ty #e1
674| #cond #iftrue #iffalse | #e1 #e2 | #e1 #e2 | #sizeofty | #e1 #field | #cost #e1 ]
675#Htranslate
676[ 2:
677| *: cases (bind_inversion ????? Htranslate) -Htranslate * #cm_expr' #Hexpr_vars' *
678     #Htranslate_addr
679     whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) #Hexec_lvalue
680     cases (eval_expr_sim cl_ge cm_ge INV ? frame_data) #_ #Hsim
681     @(Hsim ??? Hexpr_vars … Htranslate_addr ??? ? Hexec_lvalue) ]
682cases (bind2_eq_inversion ?????? Htranslate) -Htranslate *
683[ #r | #n | ]
684* #cl_type * #Heq_lookup normalize nodelta
685whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
686whd in ⊢ ((??%?) → ?);
687@(match lookup SymbolTag block (cl_env f cl_ge cm_ge INV frame_data) id
688  return λx. (lookup SymbolTag block (cl_env f cl_ge cm_ge INV frame_data) id = x) → ?
689  with
690  [ None ⇒ ?
691  | Some loc ⇒ ?
692  ] (refl ? (lookup SymbolTag block (cl_env f cl_ge cm_ge INV frame_data) id ))) normalize nodelta
693#Hlookup_eq
694[ 2,4: #Heq destruct (Heq) whd in match (eval_expr ???????);
695  [ 2: %{(Vptr (mk_pointer (stackptr f cl_ge cm_ge INV frame_data)
696               (shift_offset (bitsize_of_intsize I16) zero_offset (repr I16 n))))}
697       @conj try @refl
698       lapply (matching … frame_data id) 
699       >Hlookup_eq normalize nodelta
700       >(opt_to_res_inversion ???? Heq_lookup) normalize nodelta
701       #Hembed %4 whd in ⊢ (??%?); >Hembed @refl
702  | 1: whd in match (eval_constant ????);
703       lapply (matching … frame_data id)
704       >Hlookup_eq normalize nodelta 
705       >(opt_to_res_inversion ???? Heq_lookup) normalize nodelta
706       @False_ind
707  ]
708| 1,3: #Hfind_symbol
709  cases (bind_inversion ????? Hfind_symbol) -Hfind_symbol #block *
710  whd in ⊢ ((??%%) → ?); #Hfind_symbol
711  lapply (opt_to_res_inversion ???? Hfind_symbol) #Hfind_symbol_eq
712  whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
713  whd in match (eval_expr ???????);
714  whd in match (eval_constant ????);
715  lapply (matching … frame_data id)
716  [ >Hlookup_eq normalize nodelta >Hfind_symbol_eq normalize nodelta
717    #Hembed
718    <(eq_sym … INV id) >Hfind_symbol_eq normalize nodelta
719     %{(Vptr
720         (mk_pointer cl_block
721          (shift_offset (bitsize_of_intsize I16) zero_offset (repr I16 O))))}
722     @conj try @refl
723     %4 whd in ⊢ (??%?); >Hembed try @refl
724  | (* A stack variable is not in the local environment but in the global one. *)
725    (* we have a contradiction somewhere in the context *)
726    (* TODO *)
727    @cthulhu
728  ]
729] qed.
730 
731(* lift simulation result to eval_exprlist *)
732lemma eval_exprlist_simulation :
733  ∀f.
734  ∀cl_ge : genv_t clight_fundef.
735  ∀cm_ge : genv_t (fundef internal_function).
736  ∀INV   : clight_cminor_inv cl_ge cm_ge.
737  ∀frame_data : clight_cminor_data f cl_ge cm_ge INV.
738  ∀cl_exprs,cm_exprs.
739  ∀cl_results,trace.
740  exec_exprlist cl_ge (cl_env … frame_data) (cl_m … frame_data) cl_exprs = OK ? 〈cl_results, trace〉 →
741  mmap_sigma ??? (translate_expr_sigma (alloc_type … frame_data)) cl_exprs = OK ? cm_exprs →
742  ∀H:All ? (λx:𝚺t:typ.expr t.
743             match x with
744             [ mk_DPair ty e ⇒
745                    (expr_vars ty e
746                     (λid:ident.λty:typ.present SymbolTag val (cm_env … frame_data) id)) ]) cm_exprs.
747  ∃cm_results.
748  trace_map_inv … (λe. match e return λe.
749                         match e with
750                         [ mk_DPair _ _ ⇒ ? ] → ?
751                       with
752                       [ mk_DPair ty e ⇒ λp. eval_expr cm_ge ? e (cm_env … frame_data) p (stackptr … frame_data) (cm_m … frame_data) ]) cm_exprs H = OK ? 〈trace, cm_results〉 ∧
753  All2 ?? (λcl_val, cm_val. value_eq (Em … frame_data) cl_val cm_val) cl_results cm_results.
754#f #cl_ge #cm_ge #INV #frame_data #cl_exprs
755elim cl_exprs
756[ #cm_exprs #cl_results #trace
757  whd in ⊢ ((??%?) → ?);
758  #Heq destruct (Heq)
759  whd in ⊢ ((??%?) → ?);
760  #Heq destruct (Heq) #H %{[]}
761  @conj try @refl try @I
762| #cl_hd #cl_tl #Hind #cm_exprs #cl_results #trace
763  #Heq cases (bind_inversion ????? Heq) -Heq
764  * #hd_val #hd_trace * #Hexec_expr_cl
765  #Heq cases (bind_inversion ????? Heq) -Heq 
766  * #cl_tl_vals #cl_tl_trace * #Hexec_expr_tl
767  whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
768  #Htranslate
769  lapply (translate_exprlist_sigma_welltyped … Htranslate)
770  #Htype_eq_all #Hall
771  cases (bind_inversion ????? Htranslate) -Htranslate
772  * * #cmtype #cmexpr normalize nodelta
773  #Hexpr_vars_local_cm * #Htranslate_expr_sigma #Htranslate
774  cases (bind_inversion ????? Htranslate) -Htranslate
775  * #cm_tail #Hexpr_vars_local_cm_tail * #Htranslate_tail
776  normalize nodelta
777  whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
778  cases Htype_eq_all -Htype_eq_all #Hcm_type_eq #Htype_eq_all
779  lapply (Hind cm_tail cl_tl_vals cl_tl_trace Hexec_expr_tl)
780  [ assumption ] -Hind #Hind
781  lapply (Hind Htranslate_tail (proj2 ?? Hall)) -Hind
782  * #cm_results_tl * #Hcm_exec_tl #Hvalues_eq_tl
783  cases (eval_expr_sim cl_ge cm_ge INV ? frame_data) #Hsim #_
784  cases (bind_inversion ????? Htranslate_expr_sigma)
785  * #cmexpr' #Hexpr_vars_local_cm' * #Htranslate
786  whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
787  lapply (Hsim cl_hd cmexpr ??????) -Hsim try assumption
788  [ @(proj1 ?? Hall) ]
789  * #cm_val_hd * #Heval_expr_cm #Hvalue_eq     
790  %{(cm_val_hd :: cm_results_tl)} @conj
791  [ 2: @conj try assumption
792  | 1: whd in ⊢ (??%?); normalize nodelta >Heval_expr_cm
793       normalize nodelta >Hcm_exec_tl @refl
794  ]
795] qed. 
796
797(* Conjectured simulation results
798
799   We split these based on the start state:
800   
801   1. ‘normal’ states take some [S n] normal steps and simulates them by [S m]
802      normal steps in Cminor;
803   2. call and return steps are simulated by a call/return step plus [m] normal
804      steps (to copy stack allocated parameters / results); and
805   3. lone cost label steps are simulates by a lone cost label step
806   
807   These should allow us to maintain enough structure to identify the Cminor
808   subtrace corresponding to a measurable Clight subtrace.
809 *)
810
811lemma clight_cminor_normal :
812    ∀g1,g2.
813    ∀INV:clight_cminor_inv g1 g2.
814    ∀s1,s1'.
815    clight_cminor_rel g1 g2 INV s1 s1' →
816    clight_normal s1 →
817    ¬ pcs_labelled cl_pre g1 s1 →
818    ∀s2,tr. step … (pcs_exec cl_pre) g1 s1 = Value … 〈tr,s2〉 →   
819    ∃m. after_n_steps m ?? (pcs_exec cm_pre) g2 s1' (λs.cminor_normal s) (λtr',s2'.
820      tr = tr' ∧
821      clight_cminor_rel g1 g2 INV s2 s2' ∧
822      (m = 0 → lex_lt (measure_Clight s2) (measure_Clight s1))
823    ).
824#g1 #g2 #INV #s1 #s1' #Hstate_rel #Hclight_normal #Hnot_labeleld
825inversion Hstate_rel
826#cl_ge #cm_ge #INV' #cl_s
827(* case analysis on Clight statement *)
828cases cl_s
829[ 1: | 2: #lhs #rhs | 3: #retv #func #args | 4: #stm1 #stm2 | 5: #cond #iftrue #iffalse | 6: #cond #body
830| 7: #cond #body | 8: #init #cond #step #body | 9,10: | 11: #retval | 12: #cond #switchcases | 13: #lab #body
831| 14: #lab | 15: #cost #body ]
832[ 3: (* Call *)
833     #cm_s #cl_k #cm_k #cm_st #cl_f #cm_f #frame_data #rettyp #Hcont_rel
834     (* introduce everything *)
835     #fInv #sInv #kInv
836     #Htarget_type #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function
837     #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls
838     #flag * * * * #Hstmt_inv #Hlabels_translated #Htmps_preserved
839     #Hreturn_ok #Hlabel_wf
840     (* generalize away ugly proof *)
841     generalize in ⊢ (∀_:(???(??(????%))).?); #Hugly
842     #Htranslate
843     @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
844     destruct (HA HB)
845     @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
846     destruct (HC HD HE) #_
847     (* back to unfolding Clight execution *)
848     cases (bind_inversion ????? Htranslate) -Htranslate *
849     #ef #Hexpr_vars_ef * #Htranslate_ef normalize nodelta #Htranslate
850     cases (bind_inversion ????? Htranslate) -Htranslate *
851     #ef' #Hexpr_vars_local_ef' * #Htyp_should_eq_ef
852     cases (typ_should_eq_inversion (typ_of_type (typeof func)) ASTptr … Htyp_should_eq_ef)
853     -Htyp_should_eq_ef #Htyp_equality_ef
854     #Heq_ef_ef' #Htranslate
855     cases (bind_inversion ????? Htranslate) -Htranslate *
856     #args #Hall_variables_from_args_local *
857     whd in ⊢ ((???%) → ?); #Hargs_spec
858     cases retv normalize nodelta
859     [ 2: (* return something *)
860       #lhs #Hdest
861       cases (bind_inversion ????? Hdest) -Hdest #dest *
862       inversion dest normalize nodelta
863       [ (* register dest *) #var_id #var_ty #His_local @(jmeq_absorb ?????) #Hdest       
864         #Htranslate_dest whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
865         (* make explicit the nature of lhs, allowing to prove that no trace is emitted *)
866         lapply (translate_dest_id_inversion  … Htranslate_dest) #Hlhs_eq
867       | * #cm_expr #Hexpr_vars_cm #Hdest #Htranslate_dest #Hgensym
868         lapply (breakup_dependent_match_on_pairs ?????? Hgensym) -Hgensym
869         * #ret_var * #new_gensym * #Heq_alloc_tmp * #Halloc_tmp #Hgensym
870         lapply (breakup_dependent_match_on_pairs ?????? Hgensym) -Hgensym
871         * #tmp_var * #new_gensym' * #Heq_alloc_tmp' * #Halloc_tmp'         
872         generalize in ⊢ ((??(?? (????%) )?) → ?); #Hstmt_inv_after_gensym
873         whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
874       ]
875     | 1: (* return void *)
876          generalize in ⊢ ((??(??(????%))?) → ?); #Hugly2
877          whd in ⊢ ((???%) → ?); #Heq destruct (Heq) ]
878     #s2 #tr #Htranslate
879     cases (bindIO_inversion ??????? Htranslate) -Htranslate *
880     #func_ptr_val #func_trace * #Hexec_func_ptr normalize nodelta
881     whd in ⊢ ((???%) → ?); #Htranslate
882     cases (bindIO_inversion ??????? Htranslate) -Htranslate *
883     #args_values #args_trace * #Hexec_arglist #Htranslate
884     cases (bindIO_inversion ??????? Htranslate) -Htranslate
885     #cl_fundef * #Hfind_funct
886     lapply (opt_to_io_Value ?????? Hfind_funct) -Hfind_funct #Hfind_funct
887     cases (find_funct_inversion ???? Hfind_funct)
888     #func_ptr * * * #Hfunc_ptr_eq destruct (Hfunc_ptr_eq)
889     #Hpoff_eq_zero #Hregion_is_code
890     * #block_id * #Hblock_id_neg #Hlookup
891     #Htranslate
892     cases (bindIO_inversion ??????? Htranslate) -Htranslate #Htype_of_fundef *
893     #Hassert_type_eq
894     [ 1,2: #Htranslate
895            cases (bindIO_inversion ??????? Htranslate) -Htranslate * *
896            #lblock #loffset #ltrace *
897            #Hexec_lvalue
898            [ 1: (* empty trace *) @cthulhu (* TODO wip *)
899            | 2: @cthulhu (* TODO wip *)
900            ]
901     | 3: @cthulhu ]
902     (* TODO wip  *)
903 (*     
904     whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
905       [ 1: >Hlhs_eq in Hexec_lvalue; #Hexec_lvalue %{1}
906       | 2: (* Execute Cminor part: evaluate lhs, evaluate assign *)
907            %{2} whd whd in ⊢ (??%?); normalize nodelta
908            whd in match (eval_expr ???????);
909            whd in match (m_bind ?????);
910            lapply (Hsim_expr … Htranslate_ef … Hexpr_vars_present_ef … Hexec_func_ptr)
911            -Hsim_expr * #cm_func_ptr_val * #Heval_func #Hvalue_eq_func
912           
913       | 3:
914       ]
915       (* execute Cminor part *)
916       [ %{1} | %{2} | %{1} ]
917       whd whd in ⊢ (??%?); normalize nodelta
918       [ 1: generalize in match (proj2 (present ????) (expr_vars ???) (proj1 ???));
919       | 2: generalize in match (proj2 (present ????) (expr_vars ???) (proj1 ???));
920       | 3: generalize in match (proj2 True ??); ]
921       #Hexpr_vars_present_ef'
922       cases (eval_expr_sim … frame_data) #Hsim_expr #_
923       cut (expr_vars (typ_of_type (typeof func)) ef
924             (λid:ident.λty:typ.present SymbolTag val (cm_env cl_f cl_ge cm_ge INV' frame_data) id))
925       [ 1,3,5: lapply Heq_ef_ef' lapply Hexpr_vars_ef lapply ef >Htyp_equality_ef
926                #ef #Hexpr_vars_ef @(jmeq_absorb ?????) #Heq destruct (Heq)
927                @Hexpr_vars_present_ef' ]
928       #Hexpr_vars_present_ef           
929       (* use simulation lemma on expressions for function *)
930       lapply (Hsim_expr … Htranslate_ef … Hexpr_vars_present_ef … Hexec_func_ptr)
931       -Hsim_expr * #cm_func_ptr_val * #Heval_func #Hvalue_eq_func
932       cut (eval_expr cm_ge ASTptr ef'
933             (cm_env cl_f cl_ge cm_ge INV' frame_data) Hexpr_vars_present_ef'
934             (stackptr cl_f cl_ge cm_ge INV' frame_data)
935             (cm_m cl_f cl_ge cm_ge INV' frame_data)
936               =OK (trace×val) 〈func_trace,cm_func_ptr_val〉)
937       [ 1,3,5:
938         lapply Heq_ef_ef' lapply Heval_func lapply Hexpr_vars_ef lapply Hexpr_vars_local_ef'
939         lapply Hexpr_vars_present_ef lapply ef lapply Hexpr_vars_present_ef' lapply ef'
940         <Htyp_equality_ef #ef' #HA #ef #HB #HC #HD #HE
941         @(jmeq_absorb ?????) #Heq destruct (Heq) @HE ]
942       -Heval_func #Heval_func >Heval_func
943       whd in match (m_bind ?????);
944       lapply (trans_fn … INV' … Hfind_funct)
945       * #tmp_u * #cminor_fundef * #Hglobals_fresh_for_tmp_u * #Hfundef_fresh_for_tmp_u *
946       #Htranslate_fundef #Hfind_funct_cm
947       lapply (value_eq_ptr_inversion … Hvalue_eq_func) * #cm_func_ptr * #Hcm_func_ptr
948       whd in ⊢ ((??%?) → ?); cases func_ptr in Hfind_funct Hfind_funct_cm Hregion_is_code Hpoff_eq_zero;
949       #cm_block #cm_off #Hfind_funct #Hfind_funct_cm #Hregion_is_code #Hpoff_eq_zero destruct (Hpoff_eq_zero)
950       whd in ⊢ ((??%?) → ?); >(Em_fn_id … frame_data … cm_block Hregion_is_code)
951       normalize nodelta cases cm_func_ptr in Hcm_func_ptr; #cm_block' #cm_off'
952       #Hcm_func_ptr #Heq destruct (Hcm_func_ptr Heq) >addition_n_0
953       >Hfind_funct_cm
954       whd in match (opt_to_res ???); normalize nodelta
955       cut (All (𝚺t:typ.CMexpr t)
956              (λx:𝚺t:typ.expr t.(
957                match x with
958                [ mk_DPair ty e ⇒
959                 expr_vars ty e
960                   (λid:ident
961                    .λty0:typ.present SymbolTag val (cm_env cl_f cl_ge cm_ge INV' frame_data) id)])) args)
962       [ 1: cases sInv * * normalize nodelta * #_ #_ #Hall #_ #_ @Hall
963       | 3: cases sInv * * * * * * * normalize nodelta * #_ #_ #Hall #_ #_ #_ @Hall
964       | 5: cases sInv * * normalize nodelta * #_ #_ #Hall #_ #_ @Hall ]
965       #Hall
966       cases (eval_exprlist_simulation … frame_data ???? Hexec_arglist Hargs_spec Hall)
967       #cm_values * #Hcm_exec_list #Hcl_cm_values_eq >Hcm_exec_list
968       whd in match (m_bind ?????); normalize nodelta whd  (* TODO here bug in toCminor to be fixed before going on *) @conj
969       [ 2,4,6: #Habsurd destruct (Habsurd) ]
970       @conj try @refl
971       generalize in match (proj1 True (expr_vars ???) (proj1 ???));
972       * @(CMR_call … tmp_u) try assumption normalize nodelta
973       (* a dependency somewhere prevents case analysis *)
974       lapply Hfind_funct lapply Hfind_funct_cm lapply Htranslate_fundef lapply Hfundef_fresh_for_tmp_u
975       cases cl_fundef
976       [ 2: #H1 #H2 #H3 #H4 #H5 #H6 #H7 @I
977       | 1: #H9 #H10 #H11 #H12 #H13 @conj try @conj try // ]
978     | (* return something *)
979       #lhs #Hdest
980       cases (bind_inversion ????? Hdest) -Hdest #dest *
981       inversion dest normalize nodelta
982       [ (* register dest *) #var_id #var_ty #His_local @(jmeq_absorb ?????) #Hdest
983         #Htranslate_dest whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
984          generalize in match (conj ???);
985     ]
986   
987         
988         whd in match (proj1 ???); whd in match (proj2 ???);
989         
990         
991         [ 2: cases sInv * * normalize nodelta * #_ #_ #Hall #_ #_ @Hall ]
992         
993         >Hfind_funct_cm
994         (* case split away the invariants *)
995         cases sInv * * normalize nodelta * * #Hexpr_vars_ef' #Hall_args_present
996         whd in ⊢ (% → ?); * * normalize nodelta * #Heval_expr #Hvalue_eq
997         >Heval_expr
998         *
999   
1000[ 1: (* Skip *)
1001     #cm_s #cl_k #cm_k #cm_st #cl_f #cm_f #frame_data #rettyp #Hcont_rel
1002     (* case analysis on continuation *)
1003     inversion Hcont_rel
1004     [ (* Kstop continuation *)
1005       (* simplifying the goal using outcome of the inversion *)
1006       #kcl_ge #kcm_ge #kINV #kcl_f #kcm_f #kframe_data #ktarget_type
1007       @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
1008       destruct (HA HB)
1009       @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
1010       destruct (HC HD HE)
1011       @(jmeq_absorb ?????) #HF @(jmeq_absorb ?????) #HG @(jmeq_absorb ?????) #HH @(jmeq_absorb ?????) #HI
1012       destruct (HF HG HH HI) #_
1013       (* introduce everything *)
1014       #fInv #sInv #kInv
1015       #Htarget_type #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function
1016       #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls
1017       #flag * * * * #Hstmt_inv #Hlabels_translated #Htmps_preserved
1018       #Hreturn_ok #Hlabel_wf
1019       (* reduce statement translation function *)
1020       whd in ⊢ ((??%?) → ?);
1021       #Heq_translate
1022       (* In this simple case, trivial translation *)
1023       destruct (Heq_translate)
1024       @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
1025       destruct (HA HB)
1026       @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
1027       destruct (HC HD HE) #_
1028       (* unfold the clight execution *)
1029       #s2 #tr whd in ⊢ ((??%?) → ?);
1030       inversion (fn_return kcl_f) normalize nodelta
1031       normalize nodelta
1032       [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
1033       | #structname #fieldspec | #unionname #fieldspec | #id ]
1034       #Hfn_return whd in ⊢ ((??%?) → ?); #Heq destruct (Heq)
1035       %{1} whd @conj try @conj try @refl
1036       [ 2: #Habsurd destruct (Habsurd) ]
1037       %2{kcl_f}
1038       [ %{ (alloc_type … kframe_data)
1039            (stacksize … kframe_data)
1040            (alloc_hyp … kframe_data)
1041            (cl_env … kframe_data)
1042            (cm_env … kframe_data)
1043            (cl_env_hyp … kframe_data)
1044            (free_list (cl_m … kframe_data) (blocks_of_env (cl_env … kframe_data)))
1045            (free (cm_m … kframe_data) (stackptr … kframe_data))
1046            (Em … kframe_data)
1047            ? (* injection *)
1048            (stackptr … kframe_data)
1049            ? (* matching *)}
1050         [ @(freelist_memory_inj_m1_m2 … (injection … kframe_data) (blocks_of_env (cl_env … kframe_data)) (stackptr … kframe_data))
1051           [ 2,3: @refl
1052           |
1053 
1054     @cthulhu
1055    | (* KSeq continuation *)
1056      #gcl_ge #kcm_ge #kINV #kcl_f #kcm_f #kframe_data #ktarget_type #kcl_s #kcm_s #kcl_k' #kcm_k'
1057      #kstmt_univ #kstmt_univ' #klbl_univ #klbl_univ' #klbls #kflag
1058      * * * * #kHstmt_inv #kHlabels_translated #kHtmps_preserved
1059      #kHreturn_ok #kHlabel_wf #kHeq_translate #kHcont_rel #_
1060      @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
1061      destruct (HA HB)
1062      @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
1063      destruct (HC HD HE)
1064      @(jmeq_absorb ?????) #HF
1065     
1066      #Heq_INV #Heq_cl_f #Heq_cm_f #Heq_frame #Heq_rettyp #Heq_cl_k #Heq_cm_k  #_
1067      (* get rid of jmeqs and destruct *)
1068      lapply (jmeq_to_eq ??? Heq_INV) -Heq_INV #Heq_INV
1069      lapply (jmeq_to_eq ??? Heq_cl_f) -Heq_cl_f #Heq_cl_f
1070      destruct (Heq_INV Heq_cl_f)
1071      lapply (jmeq_to_eq ??? Heq_frame) -Heq_frame #Heq_frame
1072      lapply (jmeq_to_eq ??? Heq_cm_f) -Heq_cm_f #Heq_cm_f
1073      lapply (jmeq_to_eq ??? Heq_rettyp) -Heq_rettyp #Heq_rettypv
1074      lapply (jmeq_to_eq ??? Heq_cm_k) -Heq_cm_k #Heq_cm_k
1075      lapply (jmeq_to_eq ??? Heq_cl_k) -Heq_cl_k #Heq_cl_k
1076      destruct (Heq_frame Heq_cl_k Heq_cm_k Heq_cm_f Heq_rettyp)   
1077      #fInv #sInv #kInv #Hktarget_type
1078      #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function
1079      #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls
1080      #flag * * * * #Hstmt_inv #Hlabels_translated #Htmps_preserved
1081      #Hreturn_ok #Hlabel_wf
1082      (* reduce translation function and eliminate result *)
1083      (* In this simple case, trivial translation *)
1084      whd in ⊢ ((??%?) → ?); #Heq_translate
1085      destruct (Heq_translate)
1086      #Heq_INV' #Heq_s1 #Heq_s1'
1087      lapply (jmeq_to_eq ??? Heq_INV') -Heq_INV' #Heq_INV'
1088      lapply (jmeq_to_eq ??? Heq_s1) -Heq_s1 #Heq_s1
1089      lapply (jmeq_to_eq ??? Heq_s1') -Heq_s1' #Heq_s1' #_
1090      (* unfold the clight execution *)
1091      %{0}
1092      whd in ⊢ (% → ?); #Hassert
1093      cases (invert_assert ?? Hassert) -Hassert #Hclight_class
1094      cases (andb_inversion … Hclight_class) -Hclight_class
1095      #_ #Hnot_labelled whd in ⊢ (% → ?); #Heq destruct (Heq)
1096      %{0} whd in ⊢ %; @conj try @refl
1097      (* close simulation *)
1098      %1{kINV kHcont_rel ? ? Hfresh_globals Hfresh_function
1099         Htranslate_function kstmt_univ kstmt_univ' klbl_univ klbl_univ' klbls kflag}
1100      [ 3: @kHeq_translate | assumption ]
1101    | (* Kwhile continuation *)
1102      #kINV #kcl_f #kcm_f #kframe_data #ktarget_type
1103      #kcl_k' #kcm_k' #ksz #ksg #kcl_cond_desc #kcl_body #kcm_cond #kcm_body
1104      #kentry #kexit #kstmt_univ #kstmt_univ' #klbl_univ #klbl_univ' #klbl_univ''
1105      #klbls #kHtranslate_inv #kHexpr_vars #kHtranslate_expr #kfInv
1106      * * * * #kHentry_declared * * * *
1107      * * * #kHcond_vars_declared * * * *
1108      * * * #kHbody_inv * * *
1109      whd in ⊢ (% → ?); #kHentry_declared'
1110      * * * * * * * * *
1111      whd in ⊢ (% → ?); #kHexit_declared *
1112      * * * *
1113      #kHcont_inv #kHmklabels #kHeq_translate #kHfind_label #kHcont_rel #_
1114      #Heq_INV #Heq_cl_f #Heq_cm_f #Heq_frame #Heq_rettyp #Heq_cm_k #Heq_cl_k
1115      lapply (jmeq_to_eq ??? Heq_INV) -Heq_INV #Heq_INV
1116      lapply (jmeq_to_eq ??? Heq_cl_f) -Heq_cl_f #Heq_cl_f
1117      destruct (Heq_INV Heq_cl_f)     
1118      lapply (jmeq_to_eq ??? Heq_cm_f) -Heq_cm_f #Heq_cm_f
1119      lapply (jmeq_to_eq ??? Heq_frame) -Heq_frame #Heq_frame
1120      lapply (jmeq_to_eq ??? Heq_rettyp) -Heq_rettyp #Heq_rettyp
1121      lapply (jmeq_to_eq ??? Heq_cm_k) -Heq_cm_k #Heq_cm_k
1122      lapply (jmeq_to_eq ??? Heq_cl_k) -Heq_cl_k #Heq_cl_k #_
1123      destruct (Heq_cl_k Heq_cm_k Heq_cm_f Heq_frame Heq_rettyp)
1124      (* introduce state relation contents *)
1125      #fInv #sInv * whd in ⊢ (% → ?); * *
1126      whd in ⊢ (% → ?); * whd in ⊢ (% → ?); #Hlabel_defined * #kInv
1127      #Heq_rettyp
1128      #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function
1129      #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls
1130      #flag * * * * #Hstmt_inv #Hlabels_translated #Htmps_preserved
1131      #Hreturn_ok #Hlabel_wf
1132      (* reduce translation function and eliminate result *)
1133      (* In this simple case, trivial translation *)
1134      whd in ⊢ ((??%?) → ?); #Heq_translate
1135      destruct (Heq_translate)
1136      #Heq_INV' #Heq_s1 #Heq_s1'
1137      lapply (jmeq_to_eq ??? Heq_INV') -Heq_INV' #Heq_INV'
1138      lapply (jmeq_to_eq ??? Heq_s1) -Heq_s1 #Heq_s1
1139      lapply (jmeq_to_eq ??? Heq_s1') -Heq_s1' #Heq_s1' #_
1140      (* unfold the clight execution *)
1141      %{1} whd in ⊢ (% → ?); #Hawait
1142      cases (await_value_bind_inv … Hawait) -Hawait
1143      * #cl_val #cl_trace * #Hexec_cond #Hawait
1144      cases (await_value_bind_inv … Hawait) -Hawait
1145      #cond_outcome * #Hcond_outcome
1146      cases (eval_expr_sim … kframe_data) #Hsim_expr #_
1147      (* use simulation lemma on expressions *)
1148      lapply (Hsim_expr … kHtranslate_expr … kHcond_vars_declared … Hexec_cond) -Hsim_expr
1149      whd in match (typeof ?) in Hcond_outcome; cases cond_outcome in Hcond_outcome;
1150      #Hcond_outcome lapply (exec_bool_of_val_inversion … Hcond_outcome)
1151      * [ 2,4: * #ptr * #ty' * * #_ #Habsurd destruct (Habsurd) ]
1152      * [ 2,4: * #ty' * * #_ #Habsurd destruct (Habsurd) ]
1153      * #vsz * #vsg * #i * * #Hcl_val #Htype_eq destruct (Hcl_val Htype_eq)
1154      normalize nodelta #Hi_eq
1155      * #cm_val * #Hexec_cond_cm #Hvalue_eq #Hassert
1156      cases (invert_assert … Hassert) -Hassert #Handb
1157      cases (andb_inversion … Handb) -Handb #_ #HClight_not_labelled
1158      whd in ⊢ (% → ?); #Heq destruct (Heq)
1159      [ %{5} whd whd in ⊢ (??%?); normalize nodelta
1160        >kHfind_label -kHfind_label normalize nodelta
1161        whd in match (proj1 ???);
1162        whd in match (proj2 ???);
1163        whd whd in ⊢ (??%?); normalize nodelta
1164        >Hexec_cond_cm normalize nodelta
1165        whd in match (m_bind ?????);
1166        >(value_eq_int_inversion … Hvalue_eq)
1167        whd in match (eval_bool_of_val ?); normalize nodelta
1168        <Hi_eq normalize nodelta
1169        whd @conj [ normalize >append_nil try @refl ]
1170        whd in match (proj1 ???);
1171        whd in match (proj2 ???);
1172        whd whd in ⊢ (??%?); normalize nodelta
1173        %{??????? kframe_data ktarget_type Hcont_rel Heq_rettyp ??? Htranslate_function
1174          ??????? kHeq_translate}
1175      | %{6} whd whd in ⊢ (??%?); normalize nodelta
1176        >kHfind_label -kHfind_label normalize nodelta
1177        whd in match (proj1 ???);
1178        whd in match (proj2 ???);
1179        whd whd in ⊢ (??%?); normalize nodelta
1180        >Hexec_cond_cm normalize nodelta
1181        whd in match (m_bind ?????);
1182        >(value_eq_int_inversion … Hvalue_eq)
1183        whd in match (eval_bool_of_val ?); normalize nodelta
1184        <Hi_eq normalize nodelta
1185        whd @conj [ normalize >append_nil >append_nil try @refl ]
1186        whd in match (proj1 ???);
1187        whd in match (proj2 ???);
1188        whd whd in ⊢ (??%?); normalize nodelta
1189        %{??????? kframe_data ktarget_type kHcont_rel Heq_rettyp ??? Htranslate_function}
1190        try assumption
1191        [ @conj try @conj try @conj try @conj //
1192        | @refl ]
1193      ]
1194  (*| TODO: other continuations *)
1195    ]
1196| 2: (* Assign *)
1197     #cm_s #cl_k #cm_k #cm_st #cl_f #cm_f #frame_data #rettyp #Hcont_rel
1198     #fInv #sInv #kInv #Hrettyp #func_univ #Hfresh_globals #Hfresh_function
1199     #Htranslate_function #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls #flag
1200     * * * * #Hstmt_inv_cm #Huseless_hypothesis
1201      #Htmps_preserved #Hreturn_ok #Hlabel_wf     
1202     (* case-split on lhs in order to reduce lvalue production in Cminor *)
1203     cases lhs #lhs_ed #lhs_ty
1204     cases lhs_ed
1205     (* intro expr contents *)
1206     [ #sz #i | #var_id | #e1 | #e1 | #op #e1 |#op #e1 #e2 | #cast_ty #e1
1207     | #cond #iftrue #iffalse | #e1 #e2 | #e1 #e2 | #sizeofty | #e1 #field | #cost #e1 ]
1208     [ 2: #Htranslate_statement
1209          cases (bind_inversion ????? Htranslate_statement)
1210          * #cm_rhs #Hexpr_vars_rhs * #Htranslate_rhs #Htranslate_statement'
1211          cases (bind_inversion ????? Htranslate_statement')
1212          #lhs_dest * #Htranslate_lhs
1213          cases (bind2_eq_inversion ?????? Htranslate_lhs) -Htranslate_lhs
1214          #alloctype * #type_of_var * #Hlookup_var_success
1215          cases alloctype in Hlookup_var_success;
1216          normalize nodelta
1217          [ 1: (* Global *) #r
1218               #Hlookup_var_success whd in ⊢ ((???%) → ?); #Hlhs_dest_eq
1219               destruct (Hlhs_dest_eq) normalize nodelta
1220               whd in match (proj1 ???); whd in match (proj2 ???);
1221               whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1222               #Heq_INV #Heq_s1 #Heq_s1'
1223               lapply (jmeq_to_eq ??? Heq_INV) -Heq_INV #Heq_INV
1224               lapply (jmeq_to_eq ??? Heq_s1) -Heq_s1 #Heq_s1
1225               lapply (jmeq_to_eq ??? Heq_s1') -Heq_s1' #Heq_s1'
1226               destruct (Heq_INV Heq_s1 Heq_s1') #_
1227               %{1} whd in ⊢ (% → ?); #Hawait
1228               cases (await_value_bind_inv … Hawait) -Hawait
1229               * * #cl_blo #cl_off #cl_tr * whd in ⊢ ((??%?) → ?);
1230               #Hexec_lvalue
1231               lapply (res_to_io ????? Hexec_lvalue) -Hexec_lvalue #Hexec_lvalue
1232               #Hawait
1233               cases (await_value_bind_inv … Hawait) -Hawait
1234               * #rhs_val #rhs_trace * #Hexec_rhs_trace #Hawait
1235               cases (await_value_bind_inv … Hawait) -Hawait
1236               #mem_after_store * #Hstore_value #Hawait
1237               lapply (opt_to_io_Value ?????? Hstore_value) -Hstore_value #Hstore_value
1238               -Htranslate_statement' -Htranslate_statement
1239               cases (invert_assert … Hawait) -Hawait #Handb
1240               cases (andb_inversion … Handb) -Handb #_ #HClight_not_labelled #Hawait               
1241               (* TODO: use the memory injection to handle the store,
1242                  use INV contents to match up CL global with CM one.
1243                  Note to self: globals should be exactly matched in CL and CM,
1244                  maybe memory_injection is not useful in this particular case,
1245                  only in Stack and Local cases.
1246                * *)
1247               @cthulhu
1248          | 2: (* Stack *) #n @cthulhu
1249          | 3: (* Local *) @cthulhu
1250          ]
1251     | *: (* memdest *) @cthulhu ]   *) 
1252| *: @cthulhu
1253] qed.
1254
1255(* TODO: adapt the following to the new goal shape. *)
1256axiom clight_cminor_call_return :
1257  ∀INV:clight_cminor_inv.
1258  ∀s1,s1',s2,tr.
1259  clight_cminor_rel INV s1 s1' →
1260  match Clight_classify s1 with [ cl_call ⇒ true | cl_return ⇒ true | _ ⇒ false ] →
1261  after_n_steps 1 … clight_exec (ge_cl INV) s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) →
1262  ∃m. after_n_steps (S m) … Cminor_exec (ge_cm INV) s1' (λs.cminor_normal s) (λtr',s2'.
1263    tr = tr' ∧
1264    clight_cminor_rel INV s2 s2'
1265  ).
1266
1267axiom clight_cminor_cost :
1268  ∀INV:clight_cminor_inv.
1269  ∀s1,s1',s2,tr.
1270  clight_cminor_rel INV s1 s1' →
1271  Clight_labelled s1 →
1272  after_n_steps 1 … clight_exec (ge_cl INV) s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) →
1273  after_n_steps 1 … Cminor_exec (ge_cm INV) s1' (λs.true) (λtr',s2'.
1274    tr = tr' ∧
1275    clight_cminor_rel INV s2 s2'
1276  ).
1277
1278axiom clight_cminor_init : ∀cl_program,cm_program,s,s'.
1279  clight_to_cminor cl_program = OK ? cm_program →
1280  make_initial_state ?? clight_fullexec cl_program = OK ? s →
1281  make_initial_state ?? Cminor_fullexec cm_program = OK ? s' →
1282  ∃INV. clight_cminor_rel INV s s'.
Note: See TracBrowser for help on using the repository browser.