source: src/Clight/toCminorCorrectness.ma @ 3095

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

Start getting partial Clight to Cminor proof in shape for
measurability preservation.

File size: 140.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(* --------------------------------------------------------------------------- *)
235(* Clight to Cminor makes use of fresh symbol generators, which store the list
236 * of symbols they generate. We need to maintain as an invariant that these grow
237 * in a monotonic and consistent fashion. *)
238(* --------------------------------------------------------------------------- *)
239
240(* The two following definitions and two lemmas are duplicated from switchRemoval.ma.
241 * TODO: factorise this in frontend_misc, if they turn out not to be useless *)
242definition fresher_than_or_equal : universe SymbolTag → universe SymbolTag → Prop ≝
243λu1,u2.
244  match u1 with
245  [ mk_universe p1 ⇒
246    match u2 with
247    [ mk_universe p2 ⇒ p2 ≤ p1 ] ].
248
249definition fte ≝ fresher_than_or_equal.
250
251lemma transitive_fte : ∀u1,u2,u3. fte u1 u2 → fte u2 u3 → fte u1 u3.
252* #u1 * #u2 * #u3 normalize /2 by transitive_le/
253qed.
254
255lemma reflexive_fte : ∀u. fte u u.
256* // qed.
257
258(* Express that the [first] tmpgen generates "newer" ids than an other one. *)
259definition tmpgen_fresher_than ≝
260  λvars. λgen1, gen2 : tmpgen vars.
261    fresher_than_or_equal (tmp_universe … gen1) (tmp_universe … gen2).
262
263(* Map a predicate on all the /keys/ of an environment, i.e. on a set
264 * of identifiers. *)
265definition env_domain_P : cl_env → ∀P:(ident → Prop). Prop ≝
266 λe, P.
267  match e with
268  [ an_id_map m ⇒
269    fold ?? (λkey,elt,acc. P (an_identifier ? key) ∧ acc) m True
270  ].
271
272(* Property for an identifier to be out of the set
273 * of identifiers represented by an universe. *)
274definition ident_below_universe ≝
275  λi: ident.
276  λu: universe SymbolTag.
277  match i with
278  [ an_identifier id ⇒
279    match u with
280    [ mk_universe id_u ⇒
281      id < id_u         
282    ]   
283  ].
284
285(* Property of the domain of an environment to be disjoint of the set
286 * of identifiers represented by an universe. *) 
287definition env_below_freshgen : env → ∀vars. tmpgen vars → Prop ≝
288  λe, vars, tmpgen.
289  env_domain_P e (λid. ident_below_universe id (tmp_universe … tmpgen)).
290
291(* The property of interest for the proof. Identifiers generated from an
292 * universe above the environment are not in the said environment. *)
293lemma lookup_fails_outside_of_env :
294  ∀env, vars, ty, gen, id, gen'.
295  alloc_tmp vars ty gen = 〈id, gen'〉 →
296  env_below_freshgen env vars gen →
297  lookup ?? env id = None ?.
298@cthulhu
299qed. 
300
301(* The property of being above an environment is conserved by fresh ident
302 * generation *)
303lemma alloc_tmp_env_invariant :
304  ∀env, vars, ty, gen, id, gen'.
305  alloc_tmp vars ty gen = 〈id, gen'〉 →
306  env_below_freshgen env vars gen →
307  env_below_freshgen env vars gen'.
308@cthulhu
309qed.
310
311(* --------------------------------------------------------------------------- *)
312(* Additional invariants not contain in clight_cminor_data *)
313(* --------------------------------------------------------------------------- *)
314
315(* Fresh variable ident generator *)
316(* tmp_gen     : tmpgen alloc_type; *)
317
318(* Temporary variables generated during conversion are well-allocated. *)
319definition tmp_vars_well_allocated ≝
320   λtmpenv: list (ident × type).
321   λcm_env.
322   λcm_m.
323   λcl_m.
324   λE: embedding.
325   ∀local_variable.
326   ∀H:present ?? cm_env local_variable.
327   ∀ty. Exists ? (λx. x = 〈local_variable, ty〉) tmpenv →
328   ∀v. val_typ v (typ_of_type ty) →
329   ∃cm_m'. storev (typ_of_type ty) cm_m (lookup_present ?? cm_env local_variable H) v = Some ? cm_m' ∧
330           memory_inj E cl_m cm_m'.
331
332(* wrap the above invariant into a clight_cminor_data-eating prop *)
333(*
334definition tmp_vars_well_allocated' ≝
335   λcl_f, cl_ge, cm_ge, INV.
336   λframe_data: clight_cminor_data cl_f cl_ge cm_ge INV.
337   λtmp_gen: tmpgen (alloc_type … frame_data).
338   ∀vars_v, cl_m_v, cm_env_v, cm_m_v.
339   vars_v   = alloc_type … frame_data →
340   cl_m_v   = cl_m … frame_data →
341   cm_env_v = cm_env … frame_data →
342   cm_m_v   = cm_m … frame_data →   
343   ∀local_variable.
344   ∀H:present ?? cm_env_v local_variable.
345   ∀ty. Exists ? (λx. x = 〈local_variable, ty〉) (tmp_env … tmp_gen) →
346   ∀v. val_typ v (typ_of_type ty) →
347   ∃cm_m'. storev (typ_of_type ty) cm_m_v (lookup_present ?? cm_env_v local_variable H) v = Some ? cm_m' ∧
348           memory_inj (Em … frame_data) cl_m_v cm_m'. *)
349
350(* --------------------------------------------------------------------------- *)           
351(* A measure on Clight states that is decreasing along execution sequences     *)
352(* --------------------------------------------------------------------------- *)
353
354(* statements *)
355let rec measure_Clight_statement (s : statement) : ℕ ≝
356match s with
357[ Sskip ⇒ 0
358| Ssequence s1 s2 ⇒
359  measure_Clight_statement s1 + measure_Clight_statement s2 + 1
360| Sifthenelse e s1 s2 =>
361  measure_Clight_statement s1 + measure_Clight_statement s2 + 1
362| Swhile e s =>
363  measure_Clight_statement s + 1
364| Sdowhile e s =>
365  measure_Clight_statement s + 1
366| Sfor s1 e s2 s3 =>
367  measure_Clight_statement s1 +
368  measure_Clight_statement s2 +
369  measure_Clight_statement s3 + 1
370| Sswitch e ls =>
371  measure_Clight_ls ls + 1
372| Slabel l s =>
373  measure_Clight_statement s + 1
374| Scost cl s =>
375  measure_Clight_statement s + 1
376| _ => 1
377]
378and measure_Clight_ls (ls : labeled_statements) : ℕ :=
379match ls with
380[ LSdefault s =>
381  measure_Clight_statement s
382| LScase sz i s ls =>
383  measure_Clight_statement s +
384  measure_Clight_ls ls
385].
386
387(* continuations *)
388let rec measure_Clight_cont (cont : cl_cont) : ℕ ≝
389match cont with
390[ Kstop => 0
391| Kseq s k =>
392  measure_Clight_statement s +
393  measure_Clight_cont k + 1
394| Kwhile e s k =>
395  measure_Clight_statement s +
396  measure_Clight_cont k + 1
397| Kdowhile e s k =>
398  measure_Clight_statement s +
399  measure_Clight_cont k + 1
400| Kfor2 e s1 s2 k =>
401  measure_Clight_statement s1 +
402  measure_Clight_statement s2 +
403  measure_Clight_cont k + 1
404| Kfor3 e s1 s2 k =>
405  measure_Clight_statement s1 +
406  measure_Clight_statement s2 +
407  measure_Clight_cont k + 1
408| Kswitch k =>
409  measure_Clight_cont k + 1
410| Kcall retaddr f e k =>
411  measure_Clight_statement (fn_body f) +
412  measure_Clight_cont k + 1
413].
414
415(* Shamelessly copying Compcert. *)
416definition measure_Clight : Clight_state → ℕ × ℕ ≝
417λstate.
418match state with
419[ State f s k e m ⇒
420  〈measure_Clight_statement s + measure_Clight_cont k + 1, measure_Clight_statement s + 1〉
421| Callstate fb fd args k m ⇒ 〈0, 0〉
422| Returnstate res k m ⇒ 〈0, 0〉
423| Finalstate r ⇒ 〈0, 0〉
424].
425
426(* Stuff on lexicographic orders *)
427definition lexicographic : ∀A:Type[0]. (A → A → Prop) → A × A → A × A → Prop ≝
428λA,Ord, x, y.
429  let 〈xa, xb〉 ≝ x in
430  let 〈ya, yb〉 ≝ y in
431  Ord xa ya ∨ (xa = ya ∧ Ord xb yb).
432
433definition lex_lt ≝ lexicographic nat lt.
434
435(* --------------------------------------------------------------------------- *)
436(* Simulation relations *)
437(* --------------------------------------------------------------------------- *)
438
439definition CMcast : ∀t,t'. CMexpr t → t = t' → CMexpr t'.
440#t #t' #e #H destruct (H) @e
441qed.
442
443lemma CMcast_identity : ∀t. ∀e: CMexpr t. CMcast t t e (refl ??) = e.
444#H1 #H2 @refl qed.
445
446(* relate Clight continuations and Cminor ones. *)
447inductive clight_cminor_cont_rel :
448  ∀cl_ge, cm_ge.
449  ∀INV:  clight_cminor_inv cl_ge cm_ge.     (* stuff on global variables and functions (matching between CL and CM) *)
450  ∀cl_f: function.                          (* current Clight function *)
451  internal_function →                       (* current Cminor function *)
452  cl_env →                                  (* Clight local environment *)
453  cm_env →                                  (* Cminor local environment *)
454  mem →                                     (* Cminor memory state *)
455  ∀alloc_type:var_types.                    (* map vars to alloc type *)
456  ∀tmpenv:list (ident×type).                (* list of generated variables *)
457  (*tmpgen alloc_type →                       (* input freshgen *)
458    tmpgen alloc_type →                       (* output freshgen *) *) (* bad idea *)
459  option typ →                              (* optional target type - arg. uniform over a given function *)
460  cl_cont →                                 (* CL cont *)
461  cm_cont →                                 (* CM cont *)
462  stack →                                   (* CM stack *)
463  Prop ≝
464(* Stop continuation *)
465| ClCm_cont_stop:
466  ∀cl_ge, cm_ge, INV, cl_f, cm_f, target_type.
467  ∀cl_env, cm_env, cm_m, alloc_type, tmpenv. (*, stmt_univ, stmt_univ'.*)
468  ∀cm_stack.
469  cm_stack = SStop →
470  clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env cm_m alloc_type tmpenv (* stmt_univ stmt_univ' *) target_type Kstop Kend cm_stack
471
472(* Seq continuation *)
473| ClCm_cont_seq:
474  ∀cl_ge, cm_ge, INV, cl_f, cm_f, target_type.
475  ∀stack.
476  ∀alloc_type.
477  ∀tmpenv.
478  ∀cl_s: statement.
479  ∀cm_s: stmt.
480  ∀cl_env: cl_env.
481  ∀cm_env: cm_env.
482  ∀cm_m: mem.
483  ∀cl_k': cl_cont.
484  ∀cm_k': cm_cont.
485  ∀stmt_univ, stmt_univ'.
486  ∀lbl_univ, lbl_univ'.
487  ∀lbls.
488  ∀flag.
489  ∀Htranslate_inv.
490  translate_statement alloc_type stmt_univ lbl_univ lbls flag target_type cl_s = OK ? «〈stmt_univ',lbl_univ',cm_s〉, Htranslate_inv» →
491  (* ---- invariant on label existence ---- *)
492  lset_inclusion ? (labels_of cm_s) (labels_of (f_body cm_f)) →
493  (* ---- invariant on fresh variables ---- *)
494  lset_inclusion ? (tmp_env alloc_type stmt_univ') tmpenv →
495  clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env cm_m alloc_type tmpenv (*stmt_univ stmt_univ'*) target_type cl_k' cm_k' stack →
496  clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env cm_m alloc_type tmpenv (*stmt_univ stmt_univ'*) target_type (ClKseq cl_s cl_k') (Kseq cm_s cm_k') stack
497
498(* While continuation *) 
499| ClCm_cont_while:
500  (* Inductive family parameters *)
501  ∀cl_ge, cm_ge, INV, cl_f, cm_f, target_type.
502  ∀stack.
503  ∀alloc_type.
504  ∀tmpenv.
505  ∀cl_env.
506  ∀cm_env.
507  ∀cm_m.
508  (* sub-continuations *)
509  ∀cl_k': cl_cont.
510  ∀cm_k': cm_cont.
511  (* elements of the source while statement *)
512  ∀sz,sg.
513  ∀cl_ty.
514  ∀cl_cond_desc.
515  ∀cl_body.
516  ∀Heq: ASTint sz sg = typ_of_type cl_ty.
517  (* elements of the converted while statement *)
518  ∀cm_cond: CMexpr (ASTint sz sg).
519  ∀cm_body.
520  ∀entry,exit: identifier Label.
521  (* universes used to generate fresh labels and variables *) 
522  ∀stmt_univ, stmt_univ'.
523  ∀lbl_univ, lbl_univ', lbl_univ''.
524  ∀lbls: lenv.
525  ∀Htranslate_inv.
526  (* relate CL and CM expressions *)
527  ∀Hexpr_vars:expr_vars ? cm_cond (local_id alloc_type).
528  translate_expr alloc_type (Expr cl_cond_desc cl_ty) ≃ OK ? («cm_cond, Hexpr_vars») →
529  (* Parameters and results to find_label_always *)
530  ∀sInv: stmt_inv cm_f cm_env (f_body cm_f).
531  ∀Hlabel_declared: Exists (identifier Label) (λl'.l'=entry) (labels_of (f_body cm_f)).
532  ∀Hinv.
533  (* Specify how the labels for the while-replacing gotos are produced *)
534  mklabels lbl_univ = 〈〈entry, exit〉, lbl_univ'〉 →
535  translate_statement alloc_type stmt_univ lbl_univ' lbls (ConvertTo entry exit) target_type cl_body = OK ? «〈stmt_univ',lbl_univ'',cm_body〉, Htranslate_inv» →
536  (* ---- Invariant on label existence ----  *)
537  lset_inclusion ? (labels_of cm_body) (labels_of (f_body cm_f)) →
538  (* ---- invariant on fresh variables ---- *)
539  lset_inclusion ? (tmp_env alloc_type stmt_univ') tmpenv → 
540  find_label_always entry (f_body cm_f) Kend Hlabel_declared cm_f cm_env sInv I =
541    «〈(*St_label entry*)
542          (St_seq
543            (St_ifthenelse ?? cm_cond (St_seq cm_body (St_goto entry)) St_skip)
544            (St_label exit St_skip)), cm_k'〉, Hinv» →
545  clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env cm_m alloc_type tmpenv (* stmt_univ stmt_univ' *) target_type cl_k' cm_k' stack →
546  clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env cm_m alloc_type tmpenv (* stmt_univ stmt_univ' *) target_type
547    (Kwhile (Expr cl_cond_desc cl_ty) cl_body cl_k')
548    (Kseq (St_goto entry) (Kseq (St_label exit St_skip) cm_k')) stack
549   
550| ClCm_cont_call_store:
551  ∀cl_ge, cm_ge, INV, cl_f, cm_f, target_type.
552  ∀stack.
553  ∀alloc_type.
554  ∀tmp_env.
555  ∀cl_env.
556  ∀cm_env.
557  ∀cm_m.
558  (* sub-continuations *)
559  ∀cl_k': cl_cont.
560  ∀cm_k': cm_cont.
561  (* CL return addr *)
562  ∀CL_lvalue_block,CL_lvalue_offset,lhs_ty.
563  ∀CM_lvalue_ptr.
564  (* CM stack content *)
565  ∀stackptr.
566  ∀fInv.
567  ∀tmp_var, ret_var.
568  ∀Htmp_var_present.
569  ∀Hret_present.
570  ∀Hstmt_inv.
571  (* TODO: loads of invariants *)
572  clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env cm_m alloc_type tmp_env (*stmt_univ stmt_univ*) target_type
573    (Kcall (Some ? 〈CL_lvalue_block, CL_lvalue_offset, lhs_ty〉) cl_f cl_env cl_k')
574    cm_k'
575    (Scall (Some ? 〈ret_var,typ_of_type lhs_ty〉) cm_f stackptr
576     (update_present SymbolTag val cm_env tmp_var Htmp_var_present (Vptr CM_lvalue_ptr)) Hret_present
577     (stmt_inv_update cm_f cm_env (f_body cm_f) tmp_var (Vptr CM_lvalue_ptr) fInv Htmp_var_present)
578     (Kseq
579      (St_store (typ_of_type lhs_ty) (Id ASTptr tmp_var)
580       (Id (typ_of_type lhs_ty) ret_var)) cm_k') Hstmt_inv stack)
581
582| ClCm_cont_call_nostore:
583  ∀cl_ge, cm_ge, INV, cl_f, cm_f, target_type.
584  ∀stack.
585  ∀alloc_type.
586  ∀tmpenv.
587  ∀cl_env.
588  ∀cm_env.
589  ∀cm_m.
590  (* sub-continuations *)
591  ∀cl_k': cl_cont.
592  ∀cm_k': cm_cont.
593  (* CM stack content *)
594  ∀cl_lhs, cm_lhs.
595  match cl_lhs with
596  [ None ⇒ match cm_lhs with [ None ⇒ True | _ ⇒ False ]
597  | Some cl_location ⇒
598    match cm_lhs with
599    [ None ⇒ False
600    | Some cm_location ⇒
601      ∃CL_lvalue_block, CL_lvalue_offset, lhs_ty, ret_var.
602       cl_location = 〈CL_lvalue_block,CL_lvalue_offset, lhs_ty〉 ∧
603       cm_location = 〈ret_var, typ_of_type lhs_ty〉
604    ]
605  ] →
606  ∀Hret_present.
607  ∀Hstmt_inv.
608  ∀stackptr.
609  ∀fInv.
610(*  ∀stmt_univ.*)
611  clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env cm_m alloc_type tmpenv (*stmt_univ stmt_univ*) target_type
612   (Kcall cl_lhs cl_f cl_env cl_k')
613    cm_k'
614   (Scall cm_lhs cm_f stackptr cm_env Hret_present fInv cm_k' Hstmt_inv stack).
615
616lemma translate_fundef_internal :
617  ∀ge1, ge2.
618  ∀INV: clight_cminor_inv ge1 ge2.
619  ∀u, cl_f, cm_fundef.
620  ∀H1, H2. 
621  translate_fundef u (globals ?? INV) H1 (CL_Internal cl_f) H2 = OK ? cm_fundef →
622  ∃cm_f. cm_fundef = Internal ? cm_f ∧
623         translate_function u (globals ge1 ge2 INV) cl_f H1 H2 = OK ? cm_f.
624#ge1 #ge2 #INV #u #cl_f #cm_fd #H1 #H2
625whd in ⊢ ((??%?) → ?); cases (translate_function u (globals ge1 ge2 INV) cl_f H1 H2)
626normalize nodelta
627[ 2: #er #Habsurd destruct (Habsurd)
628| 1: #cm_f #Heq destruct (Heq) %{cm_f} @conj @refl ]
629qed.
630
631lemma translate_fundef_external :
632  ∀ge1, ge2.
633  ∀INV: clight_cminor_inv ge1 ge2.
634  ∀u, id, tl, ty.
635  ∀H1, H2.
636  translate_fundef u (globals ?? INV) H1 (CL_External id tl ty) H2 =
637    OK ? (External ? (mk_external_function id (signature_of_type tl ty))).
638#ge1 #ge2 #INV #u #id #tl #ty #H1 #H2 @refl
639qed.
640
641(* Definition of the simulation relation on states. The orders of the parameters is dictated by
642 * the necessity of performing an inversion on the continuation sim relation without having to
643 * play the usual game of lapplying all previous dependent arguments.  *)
644
645inductive clight_cminor_rel : ∀cl_ge, cm_ge. clight_cminor_inv cl_ge cm_ge  → Clight_state → Cminor_state → Prop ≝
646(* --------------------------------------------------------------------------- *)
647(* normal state *)
648(* --------------------------------------------------------------------------- *)
649| CMR_normal :
650  (* Clight and Cminor global envs *)
651  ∀cl_ge, cm_ge.
652  (* Relates globals to globals and functions to functions. *)
653  ∀INV:  clight_cminor_inv cl_ge cm_ge. 
654  (* ---- Statements ---- *)
655  (* Clight statement *) 
656  ∀cl_s: statement.
657  (* Cminor statement *)
658  ∀cm_s: stmt.                                           
659  (* ---- Continuations ---- *)
660  (* Clight continuation *)
661  ∀cl_k: cl_cont.
662  (* Cminor continuation *) 
663  ∀cm_k: cm_cont.
664  (* Cminor stack *)
665  ∀cm_st: stack.
666  (* Clight enclosing function *)
667  ∀cl_f: function.
668  (* Cminor enclosing function *)
669  ∀cm_f: internal_function.
670  (* optional return type of the function *)
671  ∀rettyp.
672  (* mapping from variables to their Cminor alloc type *)                                 
673  ∀alloc_type.
674  (* Clight env/mem *)
675  ∀cl_env, cl_m.
676  (* Cminor env/mem *)
677  ∀cm_env, cm_m.
678  (* Stack pointer (block containing Cminor locals), related size *)
679  ∀stackptr, stacksize.
680  (* ---- Cminor invariants ---- *)
681  ∀fInv: stmt_inv cm_f cm_env (f_body cm_f).
682  ∀sInv: stmt_inv cm_f cm_env cm_s.
683  ∀kInv: cont_inv cm_f cm_env cm_k.
684  (* ---- relate return type variable to actual return type ---- *)
685  rettyp = opttyp_of_type (fn_return cl_f) →
686  (* ---- relate Clight and Cminor functions ---- *)
687  ∀func_univ: universe SymbolTag.
688  ∀Hfresh_globals: globals_fresh_for_univ ? (globals ?? INV) func_univ.
689  ∀Hfresh_function: fn_fresh_for_univ cl_f func_univ.
690  translate_function func_univ (globals ?? INV) cl_f Hfresh_globals Hfresh_function = OK ? cm_f →
691  (* ---- relate Clight and Cminor statements ---- *)
692  (* fresh var generators *)
693  ∀stmt_univ,stmt_univ' : tmpgen alloc_type.
694  (* fresh label generators *)
695  ∀lbl_univ,lbl_univ'   : labgen.
696  (* map old labels to new labels *)
697  ∀lbls                 : lenv.
698  (* specify where to goto when encountering a continue or a break *)
699  ∀flag                 : convert_flag.
700  (* Invariant on translation produced by [translate_statement] *)
701  ∀Htranslate_inv.
702  translate_statement alloc_type stmt_univ lbl_univ lbls flag rettyp cl_s = OK ? «〈stmt_univ',lbl_univ',cm_s〉, Htranslate_inv» →
703  (* ---- invariant on label existence ---- *)
704  lset_inclusion ? (labels_of cm_s) (labels_of (f_body cm_f)) →
705  (* ---- relate Clight continuation to Cminor continuation ---- *)
706  ∀tmpenv.
707  lset_inclusion ? (tmp_env ? stmt_univ') tmpenv →
708  clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env cm_m alloc_type tmpenv (*stmt_univ stmt_univ'*) rettyp cl_k cm_k cm_st →
709  (* ---- state invariants for memory and environments ---- *)
710  (* Embedding *)
711  ∀Em: embedding.
712  (* locals are properly allocated *)
713  tmp_vars_well_allocated tmpenv cm_env cm_m cl_m Em →
714  (* specify how alloc_type is built *)
715  characterise_vars (globals ?? INV) cl_f = 〈alloc_type, stacksize〉 →
716  (* spec. Clight env at alloc time *)
717  (∃m,m'. exec_alloc_variables empty_env m (fn_params cl_f @ fn_vars cl_f) = 〈cl_env,m'〉) →
718  (* memory injection *)
719  memory_inj Em cl_m cm_m →
720  (* map CL env to CM env *)
721  memory_matching Em cl_ge cm_ge cl_m cm_m cl_env cm_env INV stackptr alloc_type →
722  (* Force embedding to compute identity on functions *)
723  (∀b. block_region b = Code → Em b = Some ? 〈b, zero_offset〉) →
724  (* Make explicit the fact that locals in CL are mapped to a single CM block *)
725  (∀b1.∀delta. Em b1=Some ? 〈stackptr,delta〉 →
726               mem block b1 (blocks_of_env cl_env)) →
727  (* The fresh name generator is compatible with the clight environment *)
728  env_below_freshgen cl_env alloc_type stmt_univ →
729  clight_cminor_rel cl_ge cm_ge INV
730    (ClState cl_f cl_s cl_k cl_env cl_m)
731    (CmState cm_f cm_s cm_env fInv sInv cm_m stackptr cm_k kInv cm_st)
732(* --------------------------------------------------------------------------- *)
733(* return state *)
734(* --------------------------------------------------------------------------- *)
735| CMR_return :
736  (* Clight and Cminor global envs *)
737  ∀cl_ge, cm_ge.
738  (* Relates globals to globals and functions to functions. *)
739  ∀INV: clight_cminor_inv cl_ge cm_ge.
740  (* ---- Continuations and functions ---- *)
741  (* Clight continuation *)
742  ∀cl_k: cl_cont.
743  (* Cminor continuation *)
744  ∀cm_k: cm_cont.
745  (* Cminor stack *)
746  ∀cm_st: stack.
747  (* Clight enclosing function *)
748  ∀cl_f: function.
749  (* Cminor enclosing function *)
750  ∀cm_f: internal_function.
751  (* mapping from variables to their Cminor alloc type *)
752  ∀alloc_type.
753  (* Clight env/mem *)
754  ∀cl_env, cl_m.
755  (* Cminor env/mem *)
756  ∀cm_env, cm_m.
757  (* Stack pointer (block containing Cminor locals), related size *)
758  ∀stackptr, stacksize.
759  (* fresh label generator *)
760  ∀stmt_univ: tmpgen alloc_type.
761  ∀tmpenv.
762  lset_inclusion ? (tmp_env ? stmt_univ) tmpenv →
763  (* ---- state invariants for memory and environments ---- *)
764  (* Embedding *)
765  ∀Em: embedding.
766  (* locals are properly allocated *)
767  tmp_vars_well_allocated tmpenv cm_env cm_m cl_m Em →
768  (* specify how alloc_type is built *)
769  characterise_vars (globals ?? INV) cl_f = 〈alloc_type, stacksize〉 →
770  (* spec. Clight env at alloc time *)
771  (∃m,m'. exec_alloc_variables empty_env m (fn_params cl_f @ fn_vars cl_f) = 〈cl_env,m'〉) →
772  (* memory injection *)
773  memory_inj Em cl_m cm_m →
774  (* map CL env to CM env *)
775  memory_matching Em cl_ge cm_ge cl_m cm_m cl_env cm_env INV stackptr alloc_type →
776  (* Force embedding to compute identity on functions *)
777  (∀b. block_region b = Code → Em b = Some ? 〈b, zero_offset〉) →
778  (* Make explicit the fact that locals in CL are mapped to a single CM block *)
779  (∀b1.∀delta. Em b1=Some ? 〈stackptr,delta〉 →
780               mem block b1 (blocks_of_env cl_env)) →
781  clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env cm_m alloc_type tmpenv (*stmt_univ stmt_univ*) (None ?) cl_k cm_k cm_st →
782  clight_cminor_rel cl_ge cm_ge INV
783    (ClReturnstate Vundef cl_k cl_m)
784    (CmReturnstate (None val) cm_m cm_st)
785(* --------------------------------------------------------------------------- *)
786(* call state *)
787(* --------------------------------------------------------------------------- *)
788| CMR_call :
789  (* Clight and Cminor global envs *)
790  ∀cl_ge, cm_ge.
791  (* Relates globals to globals and functions to functions. *) 
792  ∀INV:  clight_cminor_inv cl_ge cm_ge.
793  (* ------- Continuations and functions for the current stack frame -------- *)
794  (* Clight continuation *)
795  ∀cl_k: cl_cont.
796  (* Cminor continuation *) 
797  ∀cm_k: cm_cont.
798  (* Cminor stack *)
799  ∀cm_st: stack.
800  (* Clight enclosing function *)
801  ∀cl_f: function.
802  (* Cminor enclosing function *)
803  ∀cm_f: internal_function.
804  (* Clight called fundef *)
805  ∀cl_fundef.
806  (* Cminor called fundef *)
807  ∀cm_fundef.
808  (* block of Clight and Cminor function *)
809  (* XXX why do I need that already ? *)
810  ∀fblock: block.
811  (* optional return type of the function *)
812  ∀target_type.
813  (* mapping from variables to their Cminor alloc type *)                                 
814  ∀alloc_type.
815  (* Clight env/mem *)
816  ∀cl_env, cl_m.
817  (* Cminor env/mem *)
818  ∀cm_env, cm_m.
819  (* Stack pointer (block containing Cminor locals), stack frame size *)
820  ∀stackptr, stacksize.
821  (* fresh label generator for function *)
822  ∀func_univ: universe SymbolTag.
823  (* relate CL and CM enclosing functions *)
824  ∀Hglobals_fresh, Hfundef_fresh.
825  translate_function func_univ (globals ?? INV) cl_f Hglobals_fresh Hfundef_fresh = OK ? cm_f →
826  (* specify fblock *)
827  find_funct clight_fundef cl_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? cl_fundef →
828  find_funct (fundef internal_function) cm_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? cm_fundef →
829  ∀cl_fun_id, cm_fun_id.
830  ∀stmt_univ: tmpgen alloc_type.
831  ∀tmpenv.
832  lset_inclusion ? (tmp_env ? stmt_univ) tmpenv →
833  match cl_fundef with
834  [ CL_Internal _ ⇒
835     (* specify continuation *)
836     clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env cm_m alloc_type tmpenv target_type cl_k cm_k cm_st
837(*       ∨
838     (∃cl_blo, cl_off, cl_ty.         (* Clight return loscation + type *)
839      ∃cm_loc_ident, cm_return_ident. (* Cminor locals storing the lvalues *)
840      ∃sInv, fInv, kInv.              (* Invariants required by the stack construction *)
841       present ?? cm_env cm_loc_ident ∧
842       present ?? cm_env cm_return_ident ∧
843       (clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env cm_m alloc_type target_type
844          (Kcall (Some ? 〈cl_blo, cl_off, cl_ty〉) cl_f cl_env cl_k)
845           cm_k (Scall (Some ? 〈cm_return_ident,typ_of_type cl_ty〉) cm_f stackptr cm_env sInv fInv
846                     (Kseq (St_store (typ_of_type cl_ty) (Id ? cm_loc_ident) (Id ? cm_return_ident)) cm_k)
847                      kInv cm_st))) *)
848  | CL_External cl_id cl_argtypes cl_rettype ⇒
849    match cm_fundef with
850    [ Internal _ ⇒ False
851    | External cm_f_ext ⇒ True ]
852(*      match cm_f_ext with
853      [ mk_external_function cm_id sig ⇒
854        cl_fun_id = cl_id ∧ cm_fun_id = cm_id ∧ cl_fun_id = cm_fun_id
855      ] *)
856  ] →
857  (* ---- state invariants for memory and environments ---- *)
858  (* Embedding *)
859  ∀Em: embedding.
860  (* locals are properly allocated *)
861  tmp_vars_well_allocated tmpenv cm_env cm_m cl_m Em →
862  (* specify how alloc_type is built *)
863  characterise_vars (globals ?? INV) cl_f = 〈alloc_type, stacksize〉 →
864  (* spec. Clight env at alloc time *)
865  (∃m,m'. exec_alloc_variables empty_env m (fn_params cl_f @ fn_vars cl_f) = 〈cl_env,m'〉) →
866  (* memory injection *)
867  memory_inj Em cl_m cm_m →
868  (* map CL env to CM env *)
869  memory_matching Em cl_ge cm_ge cl_m cm_m cl_env cm_env INV stackptr alloc_type →
870  (* Force embedding to compute identity on functions *)
871  (∀b. block_region b = Code → Em b = Some ? 〈b, zero_offset〉) →
872  (* Make explicit the fact that locals in CL are mapped to a single CM block *)
873  (∀b1.∀delta. Em b1=Some ? 〈stackptr,delta〉 →
874               mem block b1 (blocks_of_env cl_env)) →
875  ∀cl_args_values, cm_args_values.
876  All2 val val (λcl_val:val.λcm_val:val.value_eq Em cl_val cm_val) cl_args_values cm_args_values →
877  clight_cminor_rel cl_ge cm_ge INV
878   (ClCallstate cl_fun_id cl_fundef cl_args_values cl_k cl_m)
879   (CmCallstate cm_fun_id cm_fundef cm_args_values cm_m cm_st)
880(* --------------------------------------------------------------------------- *)
881(* special while state *)
882(* --------------------------------------------------------------------------- *)
883| CMR_while:
884 ∀cl_ge,cm_ge,INV,cl_f,cm_f.
885 ∀cl_env, cl_m, cm_env, cm_m, stackptr, stacksize.
886 ∀alloc_type.
887 ∀cl_k, cm_k. 
888 ∀sz,sg, cl_ty, cl_cond_desc.
889 ∀cl_body.
890 ∀entry_label, exit_label.
891 ∀cm_cond: CMexpr (ASTint sz sg).
892 ∀cm_body.
893 ∀cm_stack.
894 ∀rettyp.
895 ∀kInv: cont_inv cm_f cm_env cm_k.
896 ∀fInv: stmt_inv cm_f cm_env (f_body cm_f).
897 ∀sInv: stmt_inv cm_f cm_env
898           ((*St_label entry_label*)
899            (St_seq
900             (St_ifthenelse sz sg cm_cond (St_seq cm_body (St_goto entry_label)) St_skip)
901             (St_label exit_label St_skip))).
902 (* Constrain the CL type *)             
903 ∀Heq_ty: ASTint sz sg = typ_of_type cl_ty.           
904 (* ---- relate return type variable to actual return type ---- *)
905 rettyp = opttyp_of_type (fn_return cl_f) →
906 (* ---- relate Clight and Cminor functions ---- *)
907 ∀func_univ: universe SymbolTag.
908 ∀Hfresh_globals: globals_fresh_for_univ ? (globals ?? INV) func_univ.
909 ∀Hfresh_function: fn_fresh_for_univ cl_f func_univ.
910 translate_function func_univ (globals ?? INV) cl_f Hfresh_globals Hfresh_function = OK ? cm_f →
911 (* ---- relate continuations ---- *)
912 ∀stmt_univ,stmt_univ',lbl_univ,lbl_univ',lbl_univ'',lbls.
913 ∀tmpenv'.
914 lset_inclusion ? (tmp_env ? stmt_univ') tmpenv' →
915 clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env cm_m alloc_type tmpenv' rettyp cl_k cm_k cm_stack →
916 (* Invariants *)
917 ∀Em: embedding.
918 tmp_vars_well_allocated tmpenv' cm_env cm_m cl_m Em →        (* locals are properly allocated *)
919 characterise_vars (globals ?? INV) cl_f = 〈alloc_type, stacksize〉 →        (* specify how alloc_type is built *)
920 (∃m,m'. exec_alloc_variables empty_env m (fn_params cl_f @ fn_vars cl_f) = 〈cl_env,m'〉) → (* spec. Clight env *)
921 memory_inj Em cl_m cm_m →                                                  (* memory injection *)
922 memory_matching Em cl_ge cm_ge cl_m cm_m cl_env cm_env INV stackptr alloc_type →  (* map CL env to CM env *)
923 (∀b. block_region b = Code → Em b = Some ? 〈b, zero_offset〉) →             (* Force embedding to compute identity on functions *)
924 (* Make explicit the fact that locals in CL are mapped to a single CM block *)
925 (∀b1.∀delta. Em b1 = Some ? 〈stackptr,delta〉 →
926              mem block b1 (blocks_of_env cl_env)) →
927 (* The fresh name generator is compatible with the clight environment *)
928 env_below_freshgen cl_env alloc_type stmt_univ →             
929 (* Expression translation and related hypotheses *)
930 ∀Hcond_tr:expr_vars ? cm_cond (local_id alloc_type).  (* invariant after converting conditional expr *)
931 (* translate_expr alloc_type (Expr cl_cond_desc cl_ty) = OK ? «CMcast ?? cm_cond Heq_ty, Hcond_tr » → *)
932 translate_expr alloc_type (Expr cl_cond_desc cl_ty) ≃ OK ? «cm_cond, Hcond_tr » →
933 (* Label consistency *)
934 Exists ? (λl':identifier Label.l'=entry_label) (labels_of (f_body cm_f)) →
935 Exists ? (λl':identifier Label.l'=exit_label) (labels_of (f_body cm_f)) → 
936 (* Statement translation *)
937 ∀Htranslate_inv.
938 mklabels lbl_univ = 〈〈entry_label, exit_label〉, lbl_univ'〉 →
939 translate_statement alloc_type stmt_univ lbl_univ' lbls
940   (ConvertTo entry_label exit_label) rettyp cl_body
941   = OK ? «〈stmt_univ',lbl_univ'',cm_body〉,Htranslate_inv» →
942 (* ---- invariant on label existence ---- *)
943 lset_inclusion ? (labels_of cm_body) (labels_of (f_body cm_f)) → 
944 (* Express the fact that the label points where it ought to *)
945 ∀Hlabel_exists.
946 ∀Hinv1, Hinv2.
947 find_label_always entry_label (f_body cm_f) Kend Hlabel_exists cm_f cm_env fInv Hinv1
948   = «〈(*St_label entry_label*)
949       (St_seq
950        (St_ifthenelse sz sg cm_cond (St_seq cm_body (St_goto entry_label))
951         St_skip)
952        (St_label exit_label St_skip)),
953      cm_k〉,
954   Hinv2» →
955 (clight_cminor_rel cl_ge cm_ge INV
956  (ClState cl_f (Swhile (Expr cl_cond_desc cl_ty) cl_body) cl_k cl_env cl_m)
957  (CmState cm_f
958   ( (*St_label entry_label*)
959    (St_seq
960     (St_ifthenelse sz sg cm_cond (St_seq cm_body (St_goto entry_label)) St_skip)
961     (St_label exit_label St_skip)))
962   cm_env fInv sInv cm_m stackptr cm_k kInv cm_stack)).
963
964   
965(*
966| CMR_call_nostore :
967 (* call to a function with no return value, or which returns in a local variable in Cminor *)
968 ∀cl_ge, cm_ge. (* cl_f, cm_f.*)
969 ∀INV: clight_cminor_inv cl_ge cm_ge.
970 ∀alloc_type, cl_env, cl_m, cm_env, cm_m, cm_stack, stackptr.
971 (* TODO: put the actual invariants on memory and etc. here *)
972 ∀func_univ: universe SymbolTag.
973 ∀cl_f, cm_f.
974 ∀Hglobals_fresh: globals_fresh_for_univ type (globals cl_ge cm_ge INV) func_univ.
975 ∀Hfundef_fresh:  fd_fresh_for_univ (CL_Internal cl_f) func_univ.
976 ∀rettyp.
977 ∀cl_k, cm_k.
978 ∀fblock.
979 rettyp = opttyp_of_type (fn_return cl_f) ∧
980 find_funct clight_fundef cl_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? (CL_Internal cl_f) →
981 find_funct (fundef internal_function) cm_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? (Internal ? cm_f) →
982 translate_function func_univ (globals ?? INV) cl_f Hglobals_fresh Hfundef_fresh = OK ? cm_f →
983 clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type rettyp cl_k cm_k cm_stack →
984 ∀fun_id.
985 ∀cl_retval, cm_retval.
986 ∀sInv, fInv, kInv.
987 ∀cl_args_values, cm_args_values.
988 All2 val val (λcl_val:val.λcm_val:val.value_eq Em cl_val cm_val) cl_args_values cm_args_values →
989 (* TODO: return_value_rel … INV frame_data cl_retval cm_retval →*)
990 clight_cminor_rel cl_ge cm_ge INV
991  (ClCallstate fun_id (CL_Internal cl_f) cl_args_values cl_k cl_m)
992  (CmCallstate fun_id (Internal ? cm_f) cm_args_values cm_m cm_stack)
993
994| CMR_call_store :
995 (* call to a function which returns to some location in memory in Cminor *)
996 ∀cl_ge, cm_ge.
997 ∀INV: clight_cminor_inv cl_ge cm_ge.
998 ∀alloc_type, cl_env, cl_m, cm_env, cm_m, cm_stack, stackptr.
999 (* TODO: put the actual invariants on memory and etc. here *)
1000 ∀func_univ: universe SymbolTag.
1001 ∀cl_f, cm_f.
1002 ∀Hglobals_fresh: globals_fresh_for_univ type (globals cl_ge cm_ge INV) func_univ.
1003 ∀Hfundef_fresh:  fd_fresh_for_univ (CL_Internal cl_f) func_univ.
1004 ∀rettyp.
1005 ∀cl_k, cm_k.
1006 ∀fblock.
1007 rettyp = opttyp_of_type (fn_return cl_f) →
1008 find_funct clight_fundef cl_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? (CL_Internal cl_f) →
1009 find_funct (fundef internal_function) cm_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? (Internal ? cm_f) →
1010 translate_function func_univ (globals ?? INV) cl_f Hglobals_fresh Hfundef_fresh = OK ? cm_f →
1011 clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type rettyp cl_k cm_k cm_stack →
1012 ∀fun_id.
1013 ∀cl_rettyp, cl_retval, cl_rettrace, cm_retval.
1014 ∀cl_lhs, cm_lhs, Hinvariant_on_cm_lhs.
1015 (* Explain where the lhs of the post-return assign comes from *)
1016 exec_lvalue cl_ge cl_env cl_m cl_lhs = OK ? 〈cl_retval, cl_rettrace〉 →
1017 translate_dest alloc_type cl_lhs = OK ? (MemDest ? «cm_lhs, Hinvariant_on_cm_lhs») →
1018 (* TODO: Explain that the actual variable used to store the ret val is fresh and has the
1019  * right type, etc *)
1020 ∀cm_ret_var.
1021 ∀sInv, fInv, kInv.
1022 ∀cl_args_values, cm_args_values.
1023 All2 val val (λcl_val:val.λcm_val:val.value_eq Em cl_val cm_val) cl_args_values cm_args_values →
1024 (* TODO: return_value_rel … INV frame_data cl_retval cm_retval →*)
1025 ∀cm_stack.
1026 clight_cminor_rel cl_ge cm_ge INV
1027  (ClCallstate fun_id (CL_Internal cl_f)
1028    cl_args_values (Kcall (Some ? 〈cl_retval,cl_rettyp〉) cl_f cl_env cl_k) cl_m)
1029  (CmCallstate fun_id (Internal ? cm_f)
1030    cm_args_values cm_m (Scall cm_retval cm_f stackptr cm_env sInv fInv
1031                          (Kseq (St_store (typ_of_type cl_rettyp) cm_lhs
1032                                          (Id (typ_of_type cl_rettyp) cm_ret_var)) cm_k)
1033                           kInv cm_stack))
1034*)   
1035
1036definition clight_normal : Clight_state → bool ≝
1037λs. match Clight_classify s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ].
1038
1039definition cminor_normal : Cminor_state → bool ≝
1040λs. match Cminor_classify s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ].
1041
1042definition cl_pre : preclassified_system ≝
1043  mk_preclassified_system
1044    clight_fullexec
1045    (λg. Clight_labelled)
1046    (λg. Clight_classify)
1047    (λx,y,H. an_identifier ? one). (* XXX TODO *)
1048
1049definition cm_pre : preclassified_system ≝
1050  mk_preclassified_system
1051    Cminor_fullexec
1052    (λg. Cminor_labelled)
1053    (λg. Cminor_classify)
1054    (λx,y,H. an_identifier ? one). (* XXX TODO *)
1055
1056(* --------------------------------------------------------------------------- *)
1057(* General purpose auxilliary lemmas. *)
1058(* --------------------------------------------------------------------------- *)
1059
1060lemma invert_assert :
1061  ∀b. ∀P. assert b P → b = true ∧ P.
1062* #P whd in ⊢ (% → ?); #H
1063[ @conj try @refl @H
1064| @False_ind @H ]
1065qed.
1066
1067lemma res_to_io :
1068  ∀A,B:Type[0]. ∀C.
1069  ∀x: res A. ∀y.
1070  match x with
1071  [ OK v ⇒  Value B C ? v
1072  | Error m ⇒ Wrong … m ] = return y →
1073  x = OK ? y.
1074#A #B #C *
1075[ #x #y normalize nodelta whd in ⊢ ((???%) → ?); #Heq destruct (Heq) @refl
1076| #err #y normalize nodelta whd in ⊢ ((???%) → ?); #Heq destruct (Heq) ]
1077qed.
1078
1079lemma jmeq_absorb : ∀A:Type[0]. ∀a,b: A. ∀P:Prop. (a = b → P) → a ≃ b → P.
1080#A #a #b #P #H #Heq lapply (jmeq_to_eq ??? Heq) #Heq' @H @Heq' qed.
1081
1082(* wrap up some trivial bit of reasoning to alleviate strange destruct behaviour *)
1083lemma pair_eq_split :
1084  ∀A,B:Type[0]. ∀a1,a2:A. ∀b1,b2:B.
1085  〈a1,b1〉 = 〈a2, b2〉 →
1086  a1 = a2 ∧ b1 = b2.
1087#A #B #a1 #a2 #b1 #b2 #Heq destruct (Heq) @conj try @refl
1088qed.
1089
1090lemma ok_eq_ok_destruct :
1091  ∀A:Type[0]. ∀a,b:A. OK ? a = OK ? b → a = b.
1092#H1 #H2 #H3 #H4 destruct @refl qed.
1093
1094lemma 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.
1095#A #a #b #P #Ha #Hb #Heq destruct (Heq)
1096@conj try %
1097qed.
1098
1099(* inverting find_funct and find_funct_ptr *)
1100lemma find_funct_inversion :
1101  ∀F: Type[0]. ∀ge: genv_t F. ∀v: val. ∀res: F.
1102      find_funct F ge v = Some ? res →
1103      (∃ptr. v = Vptr ptr ∧
1104            (poff ptr) = zero_offset ∧
1105            block_region (pblock ptr) = Code ∧
1106            (∃p. block_id (pblock ptr) = neg p ∧
1107                 lookup_opt … p (functions … ge) = Some ? res)).
1108#F #ge #v #res
1109cases v
1110[ | #sz #i | | #ptr ]
1111whd in ⊢ ((??%?) → ?);
1112#Heq destruct (Heq)
1113%{ptr} @conj try @conj try @conj try @refl
1114lapply Heq -Heq
1115@(eq_offset_elim … (poff ptr) zero_offset) //
1116normalize nodelta
1117[ 1,3,5: #_ #Habsurd destruct (Habsurd) ]
1118#Heq destruct (Heq)
1119whd in ⊢ ((??%?) → ?);
1120cases ptr #blo #off cases (block_region blo) normalize nodelta
1121[ 1,3: #Habsurd destruct (Habsurd) ]
1122[ // ]
1123cases (block_id blo) normalize nodelta
1124[ #Habsurd destruct (Habsurd) | #p #Habsurd destruct (Habsurd) ]
1125#p #Hlookup %{p} @conj try @refl assumption
1126qed.
1127
1128lemma find_funct_id_inversion :
1129  ∀F: Type[0]. ∀ge: genv_t F. ∀ptr. ∀f. ∀id.
1130  find_funct_id F ge ptr = Some ? 〈f, id〉 →
1131  ∃H:(find_funct F ge ptr = Some ? f).
1132     id = symbol_of_function_val' F ge ptr f H.
1133#F #ge #ptr #f #id
1134whd in match (find_funct_id ???);
1135generalize in match (refl ??);
1136generalize in ⊢
1137  (∀_:(???%).
1138    (??(match %
1139        with
1140        [ _ ⇒ λ_. ?
1141        | _ ⇒ λ_.λ_. ? ] ?)?) → ?);
1142#o cases o
1143normalize nodelta
1144[ #H #Habsurd destruct (Habsurd)
1145| #f #Hfind #Heq destruct (Heq) %{Hfind}
1146  cases (find_funct_inversion ???? Hfind) #ptr *
1147  * * #Hptr lapply Hfind -Hfind >Hptr #Hfind
1148  #Hoff #Hblock * #id * #Hblock_id #Hlookup_opt
1149  normalize nodelta @refl
1150] qed.
1151
1152(* We should be able to prove that ty = ty' with some more hypotheses, if needed. *)
1153lemma translate_dest_id_inversion :
1154  ∀var_types, e, var_id, H.
1155   translate_dest var_types e = return IdDest var_types ? var_id H →
1156   e = Expr (Evar var_id) (typeof e).
1157@cthulhu
1158(*   
1159#vars #e #var_id #ty #H
1160cases e #ed #ty'
1161cases ed
1162[ #sz #i | #id | #e1 | #e1 | #op #e1 |#op #e1 #e2 | #cast_ty #e1
1163| #cond #iftrue #iffalse | #e1 #e2 | #e1 #e2 | #sizeofty | #e1 #field | #cost #e1 ]
1164whd in ⊢ ((??%%) → ?);
1165#Heq
1166[ 1,4,5,6,7,8,9,10,11,13: destruct (Heq)
1167| 3,12: cases (bind_inversion ????? Heq) * #H1 #H2 #H3 cases H3
1168        #_ whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) ]
1169lapply Heq -Heq
1170change with (bind2_eq ????? ) in ⊢ ((??%?) → ?); #Heq
1171cases (bind2_eq_inversion ?????? Heq)
1172#alloctype
1173(* * #alloctype *) * #typ' *
1174cases alloctype
1175[ #r | #n | ] normalize nodelta #Hlookup'
1176[ 1,2: whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) ]
1177whd in ⊢ ((??%%) → ?); #Heq' destruct (Heq')
1178@refl*)
1179qed.
1180
1181
1182(* Note: duplicate in switchRemoval.ma *)
1183lemma fresh_elim : ∀u. ∃fv',u'. fresh SymbolTag u = 〈fv', u'〉. #u /3 by ex_intro/ qed.
1184
1185lemma fresh_elim_lab : ∀u. ∃fv',u'. fresh Label u = 〈fv', u'〉. #u /3 by ex_intro/ qed.
1186
1187
1188lemma breakup_dependent_match_on_pairs :
1189 ∀A,B,C: Type[0].
1190 ∀term: A × B.
1191 ∀F: ∀x,y. 〈x, y〉 = term → C.
1192 ∀z:C.
1193 match term
1194 return λx.x = term → ? with
1195 [ mk_Prod x y ⇒ λEq. F x y Eq ] (refl ? term) = z →
1196 ∃xa,xb,H. term = 〈xa, xb〉 ∧
1197           F xa xb H = z.
1198#A #B #C * #xa #xb #F #z normalize nodelta #H %{xa} %{xb} %{(refl ??)} @conj try @conj
1199// qed.
1200
1201(* --------------------------------------------------------------------------- *)
1202(* Extending simulation results on expressions to particular cases             *)
1203(* --------------------------------------------------------------------------- *)
1204
1205lemma translate_expr_sigma_welltyped : ∀vars, cl_expr, cm_expr.
1206  translate_expr_sigma vars cl_expr = OK ? cm_expr →
1207  dpi1 ?? (pi1 ?? cm_expr) = typ_of_type (typeof cl_expr).
1208#vars #cl_expr * * #typ #cm_expr normalize nodelta #Hexpr_vars
1209whd in ⊢ ((??%?) → ?); #H
1210cases (bind_inversion ????? H) -H * #cm_expr' #Hexpr_vars' *
1211#Htranslate_expr
1212whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) @refl
1213qed.
1214
1215lemma translate_exprlist_sigma_welltyped :
1216  ∀vars, cl_exprs, cm_exprs.
1217  mmap_sigma ??? (translate_expr_sigma vars) cl_exprs = OK ? cm_exprs →
1218  All2 ?? (λcl, cm. dpi1 ?? cm = typ_of_type (typeof cl)) cl_exprs (pi1 ?? cm_exprs).
1219#vars #cl_exprs
1220elim cl_exprs
1221[ * #cm_exprs #Hall whd in ⊢ ((??%?) → ?); #Heq destruct (Heq) @I
1222| #hd #tl #Hind * #cm_exprs #Hall #H
1223  cases (bind_inversion ????? H) -H
1224  * * #cm_typ #cm_expr normalize nodelta
1225  #Hexpr_vars_cm * #Htranslate_hd
1226  lapply (translate_expr_sigma_welltyped … Htranslate_hd)
1227  #Heq_cm_typ #H
1228  cases (bind_inversion ????? H) -H
1229  #cm_tail lapply (Hind cm_tail) cases cm_tail
1230  #cm_tail_expr #Hall_tail -Hind #Hind * #Heq_cm_tail normalize nodelta
1231   whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) whd @conj
1232   [ @Heq_cm_typ
1233   | @Hind assumption ]
1234] qed.
1235
1236lemma translate_dest_MemDest_simulation :
1237  ∀cl_f  : function.
1238  ∀cl_ge : genv_t clight_fundef.
1239  ∀cm_ge : genv_t (fundef internal_function).
1240  ∀INV   : clight_cminor_inv cl_ge cm_ge.
1241  ∀alloc_type. 
1242  ∀cl_env, cl_m, cm_env, cm_m, stackptr.
1243  ∀Em.
1244  ∀stacksize     : ℕ. 
1245  ∀alloc_hyp     : characterise_vars (globals ?? INV) cl_f = 〈alloc_type, stacksize〉.
1246  ∀cl_cm_env_hyp : ∃m,m'. exec_alloc_variables empty_env m (fn_params cl_f @ fn_vars cl_f) = 〈cl_env,m'〉.
1247  ∀injection     : memory_inj Em cl_m cm_m.
1248  ∀matching      : memory_matching Em cl_ge cm_ge cl_m cm_m cl_env cm_env INV stackptr alloc_type.
1249  (* decorrelate goal from input using some eqs *)
1250  ∀cl_expr. ∀cm_expr.
1251  ∀cl_block, cl_offset, trace.
1252  ∀Hyp_present. 
1253     translate_dest alloc_type cl_expr = OK ? (MemDest … cm_expr) →
1254     exec_lvalue cl_ge cl_env cl_m cl_expr = OK ? 〈〈cl_block, cl_offset〉, trace〉 →
1255     ∃cm_val. eval_expr cm_ge ASTptr cm_expr cm_env Hyp_present stackptr cm_m = OK ? 〈trace, cm_val〉 ∧
1256              value_eq Em (Vptr (mk_pointer cl_block cl_offset)) cm_val.     
1257#cl_f #cl_ge #cm_ge #INV #alloc_type
1258#cl_env #cl_m #cm_env #cm_m #stackptr #Em #stacksize #alloc_hyp #cl_env_hyp #injection #matching
1259#cl_expr * #cm_expr #Hexpr_vars #cl_block #cl_offset #trace #Hyp_present
1260whd in match (translate_dest ??); cases cl_expr #cl_desc #cl_typ normalize nodelta
1261cases cl_desc normalize nodelta
1262[ #sz #i | #id | #e1 | #e1 | #op #e1 |#op #e1 #e2 | #cast_ty #e1
1263| #cond #iftrue #iffalse | #e1 #e2 | #e1 #e2 | #sizeofty | #e1 #field | #cost #e1 ]
1264#Htranslate
1265[ 2:
1266| *: cases (bind_inversion ????? Htranslate) -Htranslate * #cm_expr' #Hexpr_vars' *
1267     #Htranslate_addr
1268     whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) #Hexec_lvalue
1269     cases (eval_expr_sim cl_ge cm_ge INV cl_f alloc_type stacksize alloc_hyp … cl_env_hyp … injection … matching)
1270     #_ #Hsim
1271     @(Hsim ??? Hexpr_vars … Htranslate_addr ??? ? Hexec_lvalue) ]
1272cases (bind2_eq_inversion ?????? Htranslate) -Htranslate *
1273[ #r | #n | ]
1274* #cl_type * #Heq_lookup normalize nodelta
1275whd in ⊢ ((??%%) → ?); [3: cases (typ_eq ??) #Htyp whd in ⊢ (??%% → ?); ] #Heq destruct (Heq)
1276whd in ⊢ ((??%?) → ?);
1277@(match lookup SymbolTag block cl_env id
1278  return λx. (lookup SymbolTag block cl_env id = x) → ?
1279  with
1280  [ None ⇒ ?
1281  | Some loc ⇒ ?
1282  ] (refl ? (lookup SymbolTag block cl_env id ))) normalize nodelta
1283#Hlookup_eq
1284[ 2,4: #Heq destruct (Heq) whd in match (eval_expr ???????);
1285  [ 2: %{(Vptr (mk_pointer stackptr (shift_offset (bitsize_of_intsize I16) zero_offset (repr I16 n))))}
1286       @conj try @refl
1287       lapply (matching id)
1288       >Hlookup_eq normalize nodelta
1289       >(opt_to_res_inversion ???? Heq_lookup) normalize nodelta
1290       #Hembed %4 whd in ⊢ (??%?); >Hembed @refl
1291  | 1: whd in match (eval_constant ????);
1292       lapply (matching id)
1293       >Hlookup_eq normalize nodelta 
1294       >(opt_to_res_inversion ???? Heq_lookup) normalize nodelta
1295       @False_ind
1296  ]
1297| 1,3: #Hfind_symbol
1298  cases (bind_inversion ????? Hfind_symbol) -Hfind_symbol #block *
1299  whd in ⊢ ((??%%) → ?); #Hfind_symbol
1300  lapply (opt_to_res_inversion ???? Hfind_symbol) #Hfind_symbol_eq
1301  whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
1302  whd in match (eval_expr ???????);
1303  whd in match (eval_constant ????);
1304  lapply (matching id)
1305  [ >Hlookup_eq normalize nodelta >Hfind_symbol_eq normalize nodelta
1306    #Hembed
1307    <(eq_sym … INV id) >Hfind_symbol_eq normalize nodelta
1308     %{(Vptr
1309         (mk_pointer cl_block
1310          (shift_offset (bitsize_of_intsize I16) zero_offset (repr I16 O))))}
1311     @conj try @refl
1312     %4 whd in ⊢ (??%?); >Hembed try @refl
1313  | (* A stack variable is not in the local environment but in the global one. *)
1314    (* we have a contradiction somewhere in the context *)
1315    lapply (variable_not_in_env_but_in_vartypes_is_global ???????
1316              cl_env_hyp alloc_hyp Hlookup_eq … Heq_lookup)
1317    *  #r #Habsurd destruct (Habsurd)
1318  ]
1319] qed.
1320
1321(* lift simulation result to eval_exprlist *)
1322
1323lemma eval_exprlist_simulation :
1324  ∀cl_f.
1325  ∀cl_ge : genv_t clight_fundef.
1326  ∀cm_ge : genv_t (fundef internal_function).
1327  ∀INV   : clight_cminor_inv cl_ge cm_ge.
1328  ∀alloc_type. 
1329  ∀cl_env, cl_m, cm_env, cm_m, stackptr.
1330  ∀Em.
1331  ∀stacksize     : ℕ. 
1332  ∀alloc_hyp     : characterise_vars (globals ?? INV) cl_f = 〈alloc_type, stacksize〉.
1333  ∀cl_env_hyp : ∃m,m'. exec_alloc_variables empty_env m (fn_params cl_f @ fn_vars cl_f) = 〈cl_env,m'〉.
1334  ∀injection     : memory_inj Em cl_m cm_m.
1335  ∀matching      : memory_matching Em cl_ge cm_ge cl_m cm_m cl_env cm_env INV stackptr alloc_type.
1336  ∀cl_exprs,cm_exprs.
1337  ∀cl_results,trace.
1338  exec_exprlist cl_ge cl_env cl_m cl_exprs = OK ? 〈cl_results, trace〉 →
1339  mmap_sigma ??? (translate_expr_sigma alloc_type) cl_exprs = OK ? cm_exprs →
1340  ∀H:All ? (λx:𝚺t:typ.expr t.
1341             match x with
1342             [ mk_DPair ty e ⇒
1343                    (expr_vars ty e
1344                     (λid:ident.λty:typ.present SymbolTag val cm_env id)) ]) cm_exprs.
1345  ∃cm_results.
1346  trace_map_inv … (λe. match e return λe.
1347                         match e with
1348                         [ mk_DPair _ _ ⇒ ? ] → ?
1349                       with
1350                       [ mk_DPair ty e ⇒ λp. eval_expr cm_ge ? e cm_env p stackptr cm_m ]) cm_exprs H = OK ? 〈trace, cm_results〉 ∧
1351  All2 ?? (λcl_val, cm_val. value_eq Em cl_val cm_val) cl_results cm_results.
1352#f #cl_ge #cm_ge #INV
1353#alloc_type #cl_env #cl_m #cm_env #cm_m #stackptr #Em #stacksize #alloc_hyp #cl_env_hyp #injection #matching
1354#cl_exprs
1355elim cl_exprs
1356[ #cm_exprs #cl_results #trace
1357  whd in ⊢ ((??%?) → ?);
1358  #Heq destruct (Heq)
1359  whd in ⊢ ((??%?) → ?);
1360  #Heq destruct (Heq) #H %{[]}
1361  @conj try @refl try @I
1362| #cl_hd #cl_tl #Hind #cm_exprs #cl_results #trace
1363  #Heq cases (bind_inversion ????? Heq) -Heq
1364  * #hd_val #hd_trace * #Hexec_expr_cl
1365  #Heq cases (bind_inversion ????? Heq) -Heq 
1366  * #cl_tl_vals #cl_tl_trace * #Hexec_expr_tl
1367  whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
1368  #Htranslate
1369  lapply (translate_exprlist_sigma_welltyped … Htranslate)
1370  #Htype_eq_all #Hall
1371  cases (bind_inversion ????? Htranslate) -Htranslate
1372  * * #cmtype #cmexpr normalize nodelta
1373  #Hexpr_vars_local_cm * #Htranslate_expr_sigma #Htranslate
1374  cases (bind_inversion ????? Htranslate) -Htranslate
1375  * #cm_tail #Hexpr_vars_local_cm_tail * #Htranslate_tail
1376  normalize nodelta
1377  whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
1378  cases Htype_eq_all -Htype_eq_all #Hcm_type_eq #Htype_eq_all
1379  lapply (Hind cm_tail cl_tl_vals cl_tl_trace Hexec_expr_tl)
1380  [ assumption ] -Hind #Hind
1381  lapply (Hind Htranslate_tail (proj2 ?? Hall)) -Hind
1382  * #cm_results_tl * #Hcm_exec_tl #Hvalues_eq_tl
1383  cases (eval_expr_sim cl_ge cm_ge INV f alloc_type stacksize alloc_hyp ?? cl_env_hyp ?? Em injection stackptr matching)
1384  #Hsim #_
1385  cases (bind_inversion ????? Htranslate_expr_sigma)
1386  * #cmexpr' #Hexpr_vars_local_cm' * #Htranslate
1387  whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
1388  lapply (Hsim cl_hd cmexpr ??????) -Hsim try assumption
1389  [ @(proj1 ?? Hall) ]
1390  * #cm_val_hd * #Heval_expr_cm #Hvalue_eq     
1391  %{(cm_val_hd :: cm_results_tl)} @conj
1392  [ 2: @conj try assumption
1393  | 1: whd in ⊢ (??%?); normalize nodelta >Heval_expr_cm
1394       normalize nodelta >Hcm_exec_tl @refl
1395  ]
1396] qed.
1397
1398(* --------------------------------------------------------------------------- *)
1399(* Putting the memory injection at work.                                       *)
1400(* --------------------------------------------------------------------------- *)
1401
1402(* A) Non-interference of local variables with memory injections  *)
1403
1404(* Needed property:
1405 * A local variable allocated via the temporary variable generator should not interfere
1406 * with the memory injection. In particular, we need to show that:
1407 * 1) we can successfuly store stuff of the right type inside (where the type is specified
1408 *    at generation time, and should be in the current context)
1409 * 2) after the store, we can build a consistent memory state and more generally, a
1410 *    correct [clight_cminor_data] invariant record. Cf. toCminorCorrectnessExpr.ma
1411 *)
1412 
1413(* A.1) memory matchings survives memory injection *)
1414
1415lemma offset_plus_0' : ∀o:offset. offset_plus zero_offset o = o.
1416#o cases o #b >offset_plus_0 @refl
1417qed.
1418
1419(*
1420lemma store_value_of_type_memory_matching_to_matching : 
1421  ∀cl_ge, cm_ge, cl_en, cm_en, INV, sp, vars, cl_m, cl_m',cm_m,cm_m'.
1422  ∀E: embedding.
1423  ∀blo, blo', delta, off.
1424  E blo = Some ? 〈blo', delta〉 →
1425  ∀cl_val, cm_val, ty.
1426  value_eq E cl_val cm_val →
1427  storen cl_m (mk_pointer blo off) (fe_to_be_values ty cl_val) = Some ? cl_m' →
1428  storen cm_m (mk_pointer blo (offset_plus off delta)) (fe_to_be_values ty cm_val) = Some ? cm_m' →
1429  (lookup' vars var_id = OK (var_type×type) 〈Global r,type_of_var〉)
1430  memory_inj E cl_m' cm_m' →
1431  memory_matching E cl_ge cm_ge cl_m cm_m cl_en cm_en INV sp vars →
1432  memory_matching E cl_ge cm_ge cl_m' cm_m' cl_en cm_en INV sp vars.
1433#cl_ge #cm_ge #cl_en #cm_en #INV #sp #vars #cl_m #cl_m' #cm_m #cm_m' #E
1434#blo #blo' #delta #off #Hembed #cl_val #cm_val #ty #Hvalue_eq #Hstoren_cl #Hstoren_cm
1435#Hinj #Hmatching #id
1436lapply (Hmatching id)
1437cases (lookup ?? cl_en id) normalize nodelta
1438[ 1: #H @H
1439| 2: #bl cases (lookup ?? vars id) normalize nodelta
1440  [ 1: #H @H
1441  | 2: * #var_type #cl_type normalize nodelta
1442       cases var_type normalize nodelta
1443       [ #r #H @H
1444       | #b #H @H
1445       | #H #v lapply H -H
1446         @(eq_block_elim … bl blo)
1447         [ #Heq destruct (Heq)
1448           @(eq_offset_elim … off zero_offset)
1449           [ (* We actually load exactly where we wrote, but with a potentially different type. *)
1450             #Heq destruct (Heq) #H
1451       ]
1452  ]
1453] qed.*)
1454
1455
1456lemma alloc_tmp_in_genlist :
1457  ∀vartypes. ∀g1, g2, g3.
1458  ∀id1, ty1, id2, ty2.
1459  alloc_tmp vartypes ty1 g1 = 〈id1, g2〉 →
1460  alloc_tmp vartypes ty2 g2 = 〈id2, g3〉 →
1461  Exists (identifier SymbolTag×type)
1462   (λx:identifier SymbolTag×type.x=〈id2,ty2〉) (tmp_env ? g3).
1463#vartypes #g1 #g2 #g3
1464#id1 #ty1 #id2 #ty2 #Halloc1 #Halloc2
1465lapply (breakup_dependent_match_on_pairs ?????? Halloc1) * #id1' * #u' * #Hfg1
1466* #Hfresh_eq generalize in match (fresh_map_add ????????); #ugly
1467generalize in ⊢ ((??(????(?????%))?) → ?); #ugly2
1468#Heq destruct (Heq)
1469lapply (breakup_dependent_match_on_pairs ?????? Halloc2) * #id2' * #u'' * #Hfg2
1470* #Hfresh_eq' generalize in match (fresh_map_add ????????); #ugly'
1471generalize in ⊢ ((??(????(?????%))?) → ?); #ugly2'
1472#Heq destruct (Heq) %1 @refl
1473qed. (* this last lemma has to be refitted. *)
1474
1475lemma store_value_of_type_success_by_value :
1476   ∀ty, m, m', b, o, v.
1477   store_value_of_type ty m b o v = Some ? m' →
1478   access_mode ty = By_value (typ_of_type ty) ∧
1479   storev (typ_of_type ty) m (Vptr (mk_pointer b o)) v = Some ? m'.   
1480#ty #m #m' #b #o #v
1481cases ty
1482[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
1483| #structname #fieldspec | #unionname #fieldspec | #id ]
1484whd in ⊢ ((??%?) → ?);
1485[ 1,4,5,6,7: #Habsurd destruct (Habsurd) ]
1486#H @conj try @refl @H
1487qed.
1488
1489(* Some boilerplate to avoid performing a case analysis on exprs in the middle of
1490 * the proof. *)
1491lemma translate_dest_not_Evar_id :
1492  ∀vars, ed, ty.
1493  (∀id. ed ≠ Evar id) →
1494    translate_dest vars (Expr ed ty) =
1495    (do e1' ← translate_addr vars (Expr ed ty);
1496     OK ? (MemDest … e1')).
1497#vars *
1498[ #sz #i | #id | #e1 | #e1 | #op #e1 |#op #e1 #e2 | #cast_ty #e1
1499| #cond #iftrue #iffalse | #e1 #e2 | #e1 #e2 | #sizeofty | #e1 #field | #cost #e1 ]
1500#ty #H
1501[ 2: @False_ind @(absurd … (refl ??) (H ?)) ]
1502@refl
1503qed.
1504
1505lemma expr_is_Evar_id_dec :
1506  ∀ed. (∀id. ed ≠ Evar id) ∨ (∃id. ed = Evar id).
1507
1508[ #sz #i | #id | #e1 | #e1 | #op #e1 |#op #e1 #e2 | #cast_ty #e1
1509| #cond #iftrue #iffalse | #e1 #e2 | #e1 #e2 | #sizeofty | #e1 #field | #cost #e1 ]
1510[ 2: %2 %{id} @refl
1511| *: %1 #id % #Habsurd destruct (Habsurd) ]
1512qed.
1513
1514lemma mk_offset_offv_id : ∀o. mk_offset (offv o) = o.
1515* #x @refl qed.
1516
1517lemma find_funct_to_find_funct_id :
1518   ∀F, ge, ptr, fundef.
1519   ∀H:find_funct ? ge ptr = Some ? fundef.
1520   find_funct_id F ge ptr = Some ? 〈fundef, symbol_of_function_val' F ge ptr fundef H〉.
1521#F #ge #ptr #fundef #Hfind whd in match (find_funct_id ???);
1522generalize in ⊢ (??(?%)?);
1523generalize in ⊢
1524 ((???%) → (??
1525    (match %
1526(*     return λ_. (??%?) → ?*)
1527     with
1528     [ _ ⇒ λ_. ?
1529     | _ ⇒ λ_.λ_. ? ] ?)
1530  ?));
1531#o cases o normalize nodelta
1532[ #H @False_ind >Hfind in H; #Habsurd destruct (Habsurd)
1533| #f #Hfind' 
1534  cut (f = fundef)
1535  [ >Hfind in Hfind'; #Heq destruct (Heq) @refl ]
1536  #Heq destruct (Heq)
1537  @refl
1538] qed.
1539
1540lemma eval_bool_of_val_to_Cminor :
1541  ∀E. ∀ty. ∀v1,v2. ∀b.
1542    value_eq E v1 v2 →
1543    exec_bool_of_val v1 ty = return b →
1544    eval_bool_of_val v2 = return  b.
1545#E #ty #v1 #v2 #b #Hvalue_eq
1546whd in ⊢ ((??%%) → (??%%));
1547@(value_eq_inversion … Hvalue_eq) normalize nodelta
1548[ #Habsurd destruct (Habsurd) ]
1549[ #vsz #vi cases ty
1550  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
1551  | #structname #fieldspec | #unionname #fieldspec | #id ] normalize nodelta
1552  [ 2: | *: #Habsurd destruct (Habsurd) ]
1553  @(intsize_eq_elim_elim … vsz sz)
1554  [ 1: #H #Habsurd destruct (Habsurd)
1555  | 2: #Heq destruct (Heq) normalize nodelta #H @H ]
1556| cases ty
1557  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
1558  | #structname #fieldspec | #unionname #fieldspec | #id ] normalize nodelta
1559  #H destruct (H) @refl
1560| #p1 #p2 #Htranslate
1561  cases ty
1562  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
1563  | #structname #fieldspec | #unionname #fieldspec | #id ] normalize nodelta
1564  #H destruct (H) @refl
1565] qed.
1566
1567lemma let_prod_as_inversion :
1568    ∀A,B,C: Type[0].
1569    ∀expr: A × B.
1570    ∀body: ∀a:A. ∀b:B. 〈a,b〉 = expr → res C.
1571    ∀result: C.
1572    (let 〈a,b〉 as E ≝ expr in body a b E) = return result →
1573    ∃x,y. ∃E. 〈x,y〉 = expr ∧
1574          body x y E = return result.
1575#A #B #C * #a #b #body #res normalize nodelta #Heq
1576%{a} %{b} %{(refl ??)} @conj try @refl @Heq
1577qed.
1578
1579(* move this to frontend_misc *)
1580lemma lset_inclusion_Exists : ∀A, l1, l2, P.
1581  Exists A P l1 → lset_inclusion A l1 l2 → Exists A P l2.
1582#A #l1 #l2 #P #Hexists whd in ⊢ (% → ?);
1583lapply Hexists
1584generalize in match l2;
1585elim l1
1586[ #l2 @False_ind
1587| #hd #tl #Hind #l2 *
1588  [ 2: #HA * #Hhd #Htl @Hind try assumption
1589  | 1: #H * #Hmem #_ elim l2 in Hmem;
1590       [ @False_ind
1591       | #hd2 #tl2 #Hind *
1592         [ #Heq destruct (Heq) %1 @H
1593         | #Hneq %2 @Hind @Hneq ]
1594       ]
1595  ]
1596] qed.
1597
1598axiom load_value_after_free_list_inversion :
1599  ∀ty, m, blocks, b, o, v.
1600  load_value_of_type ty (free_list m blocks) b o = Some ? v → 
1601  load_value_of_type ty m b o = Some ? v.
1602
1603(* Make explicit the contents of [exec_bind_parameters ????] *) 
1604lemma exec_alloc_bind_params_same_length :
1605  ∀e,m,m',params,vars.
1606  exec_bind_parameters e m params vars = OK ? m' →
1607  (params = [ ] ∧ vars = [ ]) ∨
1608  ∃id,ty,tl_pa,v,tl_vars,b,mi.
1609   params = 〈id,ty〉 :: tl_pa ∧
1610   vars   = v :: tl_vars ∧
1611   lookup ?? e id = Some ? b ∧
1612   store_value_of_type ty m b zero_offset v = Some ? mi ∧
1613   exec_bind_parameters e mi tl_pa tl_vars = OK ? m'.
1614#e #m #m' #params cases params
1615[ #vars whd in ⊢ ((??%?) → ?); cases vars normalize nodelta
1616  [ #Heq destruct (Heq) %1 @conj try @refl
1617  | #hd_pa #tl_pa #Habsurd destruct (Habsurd) ]
1618| * #id #ty #tl_pa #vars
1619  whd in ⊢ ((??%?) → ?);
1620  cases vars normalize nodelta
1621  [ #Habsurd destruct (Habsurd)
1622  | #hd_val #tl_val #H
1623    cases (bind_inversion ????? H) -H
1624    #blo * #HA #H
1625    cases (bind_inversion ????? H) -H
1626    #m'' * #HB #Hexec_bind %2
1627    %{id} %{ty} %{tl_pa} %{hd_val} %{tl_val} %{blo} %{m''}   
1628    @conj try @conj try @conj try @conj try @refl
1629    try @(opt_to_res_inversion ???? HA)
1630    try @(opt_to_res_inversion ???? HB)
1631    @Hexec_bind
1632  ]
1633] qed.
1634
1635(* Axiom-fest, with all the lemmas we need but won't have time to prove. Most of them are not too hard. *)
1636
1637(* The way we have of stating this is certainly not the most synthetic. The property we really need is that
1638 * stmt_univ' is fresher than stmt_univ, which sould be trivially provable by a simple induction. *)
1639axiom env_below_freshgen_preserved_by_translation :
1640    ∀cl_env, alloc_type, stmt_univ, lbl_univ, lbls, flag, rettyp, s, stmt_univ', lbl_univ', cm_s, H.
1641    env_below_freshgen cl_env alloc_type stmt_univ →
1642    translate_statement alloc_type stmt_univ lbl_univ lbls flag rettyp s = return «〈stmt_univ', lbl_univ', cm_s〉, H» →
1643    env_below_freshgen cl_env alloc_type stmt_univ'.
1644
1645axiom tmp_vars_well_allocated_preserved_by_inclusion :
1646    ∀cm_env, cm_m, cl_m, Em, tmpenv, tmpenv'.
1647    lset_inclusion ? tmpenv tmpenv' →
1648    tmp_vars_well_allocated tmpenv' cm_env cm_m cl_m Em →
1649    tmp_vars_well_allocated tmpenv cm_env cm_m cl_m Em.
1650
1651axiom translation_entails_ident_inclusion :
1652    ∀alloc_type, stmt_univ, lbl_univ, lbls, flag, rettyp, stmt_univ'.
1653    ∀cl_s, cm_s, labgen, Htrans_inv.
1654    translate_statement alloc_type stmt_univ lbl_univ lbls flag rettyp cl_s = return «〈stmt_univ',labgen,cm_s〉,Htrans_inv» →
1655    lset_inclusion ? (tmp_env … stmt_univ) (tmp_env … stmt_univ').
1656
1657(* Same remarks as above apply here too. *)
1658(*
1659lemma tmp_vars_well_allocated_preserved_by_translation :
1660    ∀cm_env, alloc_type, stmt_univ, lbl_univ, lbls, flag, rettyp, stmt_univ'.
1661    ∀Em, cm_m, cl_m, cl_s, cm_s, labgen, Htrans_inv.
1662    translate_statement alloc_type stmt_univ lbl_univ lbls flag rettyp cl_s = return «〈stmt_univ',labgen,cm_s〉,Htrans_inv» →
1663    tmp_vars_well_allocated (tmp_env alloc_type stmt_univ') cm_env cm_m cl_m Em →
1664    tmp_vars_well_allocated (tmp_env alloc_type stmt_univ) cm_env cm_m cl_m Em.
1665#cm_env #alloc_type #stmt_univ #lbl_univ #lbls #flag #rettyp #stmt_univ' #Em #cm_m #cl_m #cl_s #cm_s
1666#labgen #Htrans_inv #Htranslate_statement #H #id #Hpresent #ty #Hexists
1667@H lapply (translation_entails_ident_inclusion … Htranslate_statement)
1668#H
1669@H23*)
1670
1671axiom tmp_vars_well_allocated_conserved_by_frame_free :
1672  ∀alloc_type, tmpenv, cl_env, cm_env, cm_m, cl_m, stackptr.
1673  ∀Em, cl_ge, cm_ge, INV.
1674  ∀Hmatching:memory_matching Em cl_ge cm_ge cl_m cm_m cl_env cm_env INV stackptr alloc_type.
1675  tmp_vars_well_allocated tmpenv cm_env cm_m cl_m Em ->
1676  tmp_vars_well_allocated tmpenv cm_env (free cm_m stackptr) (free_list cl_m (blocks_of_env cl_env)) Em.
1677
1678axiom generated_id_not_in_env :
1679    ∀id, blo, tmp, ty.
1680    ∀env: cl_env.
1681    ∀alloc_type.
1682    ∀freshgen, freshgen': tmpgen alloc_type.
1683    env_below_freshgen env alloc_type freshgen →
1684    lookup ?? env id = Some ? blo →
1685    alloc_tmp alloc_type ty freshgen = 〈tmp, freshgen'〉 →
1686    tmp ≠ id.
1687
1688(* This should just be lifting a lemma from positive maps to identifier maps.
1689 * Sadly, the way things are designed requires a boring induction. *)
1690axiom update_lookup_opt_other :
1691  ∀b,a,t,H.
1692  ∀b'. b ≠ b' →
1693  lookup SymbolTag val t  b' = lookup SymbolTag val (update_present SymbolTag val t b H a) b'.
1694 
1695 
1696(* NOTE: this axiom is way more general than what we need. In practice, cm_m' is cm_m after a store. *)
1697axiom clight_cminor_cont_rel_parametric_in_mem :
1698  ∀cl_ge, cm_ge, INV, cl_f, cm_f, cl_env, cm_env, cm_m, cm_m', alloc_type, tmpenv, (*stmt_univ, stmt_univ', *) rettyp, cl_k, cm_k, cm_st.
1699  clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env cm_m alloc_type tmpenv (*stmt_univ stmt_univ'*) rettyp cl_k cm_k cm_st →
1700  clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env cm_m' alloc_type tmpenv (*stmt_univ stmt_univ'*) rettyp cl_k cm_k cm_st.
1701
1702(* Same remark as above. *)
1703axiom well_allocated_preserved_by_parallel_stores :
1704  ∀tmpenv, cm_env, cm_m, cm_m', cl_m, cl_m', Em.
1705
1706(* TODO: proper hypotheses (the following, commented out do not exactly fit)
1707  (storen cm_m (mk_pointer cl_blo (mk_offset (offv zero_offset))) (fe_to_be_values (typ_of_type (typeof rhs)) cm_rhs_val)
1708   =Some mem cm_mem_after_store_lhs)
1709  storev (typ_of_type ty) cl_m (Vptr (mk_pointer cl_blo zero_offset)) cl_rhs_val = Some ? cl_m') *)
1710
1711  tmp_vars_well_allocated tmpenv cm_env cm_m  cl_m  Em →
1712  tmp_vars_well_allocated tmpenv cm_env cm_m' cl_m' Em.
1713
1714(* Same remark as above. Moreover, this should be provable from memory injections. *)
1715axiom memory_matching_preserved_by_parallel_stores :
1716  ∀Em, cl_ge, cm_ge, cl_m, cl_m', cm_m, cm_m', cl_env, cm_env, INV, stackptr, alloc_type.
1717  memory_matching Em cl_ge cm_ge cl_m  cm_m  cl_env cm_env INV stackptr alloc_type →
1718  memory_matching Em cl_ge cm_ge cl_m' cm_m' cl_env cm_env INV stackptr alloc_type.
1719 
1720axiom clight_cminor_cont_rel_parametric_in_cm_env :
1721∀cl_ge, cm_ge, INV, cl_f, cm_f, cl_env, cm_env, cm_m, alloc_type, tmpenv, (*stmt_univ, stmt_univ',*) rettyp, cl_k, cm_k, cm_st, var_id, v.
1722∀Hpresent:present SymbolTag val cm_env var_id.
1723clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env cm_m alloc_type tmpenv (*stmt_univ stmt_univ'*) rettyp cl_k cm_k cm_st ->
1724clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env
1725  (update_present SymbolTag val cm_env var_id Hpresent v) cm_m
1726  alloc_type tmpenv (*stmt_univ stmt_univ'*) rettyp cl_k cm_k cm_st.
1727
1728axiom tmp_vars_well_allocated_preserved_by_local_store :
1729  ∀Em, cl_value, cm_value, lhs_ty, cl_m, cl_m', cm_m, cl_blo, tmpenv, cm_env, var_id.
1730  ∀Hpresent:present SymbolTag val cm_env var_id.
1731  value_eq Em cl_value cm_value →
1732  store_value_of_type' lhs_ty cl_m 〈cl_blo, zero_offset〉 cl_value = Some ? cl_m' →
1733  tmp_vars_well_allocated tmpenv cm_env cm_m cl_m Em →
1734  tmp_vars_well_allocated tmpenv
1735  (update_present ?? cm_env var_id Hpresent cm_value) cm_m
1736   cl_m' Em.
1737
1738axiom memory_inj_preserved_by_local_store :
1739∀Em, cl_ge, cm_ge, cl_m, cl_m', cm_m, cl_env, cm_env, INV, stackptr, alloc_type.
1740 memory_matching Em cl_ge cm_ge cl_m cm_m cl_env cm_env INV stackptr alloc_type ->
1741 memory_inj Em cl_m cm_m ->
1742 memory_inj Em cl_m' cm_m.
1743
1744axiom memory_matching_preserved_by_local_store :
1745  ∀Em, cl_ge, cm_ge, cl_m, cl_m', cm_m, cl_env, cm_env, INV, stackptr, alloc_type, cl_value, cm_value.
1746  ∀cl_blo, var_id, lhs_ty.
1747  ∀Hpresent:present SymbolTag val cm_env var_id. 
1748   value_eq Em cl_value cm_value →
1749   store_value_of_type' lhs_ty cl_m 〈cl_blo, zero_offset〉 cl_value = Some ? cl_m' →
1750   memory_matching Em cl_ge cm_ge cl_m cm_m cl_env cm_env INV stackptr alloc_type →
1751   memory_matching Em cl_ge cm_ge cl_m' cm_m cl_env
1752    (update_present SymbolTag val cm_env var_id Hpresent cm_value) INV stackptr alloc_type.
1753
1754lemma alloc_tmp_monotonic :
1755  ∀alloc_type, ty, univ, univ', v.
1756   alloc_tmp alloc_type ty univ = 〈v, univ'〉 →
1757   lset_inclusion ? (tmp_env ? univ) (tmp_env ? univ').
1758#alloc_type #ty #univ #univ' #v cases univ
1759#u #env #Hfresh #Hyp #Halloc
1760cases (breakup_dependent_match_on_pairs ?????? Halloc) -Halloc
1761#v * #u' * #Heq * #Heq' normalize nodelta #Heq''
1762destruct (Heq'')
1763@cons_preserves_inclusion @reflexive_lset_inclusion
1764qed.
1765
1766(*
1767lemma lset_inclusion_Exists :
1768  ∀A. ∀l1, l2: lset A.
1769  lset_inclusion ? l1 l2 →
1770  ∀P. Exists ? P l1 → Exists ? P l2.
1771#A #l1 elim l1
1772[ #l2 #Hincl #P @False_ind
1773| #hd #tl #Hind #l2 * #Hmem #Hincl2 #P *
1774  [ 2: #Htl @Hind assumption ]
1775  lapply P -P
1776  lapply Hincl2 -Hincl2
1777  lapply Hmem -Hmem elim l2
1778  [ @False_ind ]
1779  #hd2 #tl2 #Hind2 *
1780  [ #Heq destruct (Heq)
1781    #Hincl2 #P #H %1 @H
1782  | #Hmem #Hincl2 #P #H %2
1783    elim tl2 in Hmem;
1784    [ @False_ind
1785    | #hd2' #tl2' #Hind3 *
1786      [ #Heq destruct (Heq) %1 assumption
1787      | #Hmem' %2 @Hind3 @Hmem' ]
1788    ]
1789  ]
1790] qed.  *)
1791
1792(* --------------------------------------------------------------------------- *)
1793(* Main simulation results                                                     *)
1794(* --------------------------------------------------------------------------- *)
1795
1796(* Conjectured simulation results
1797
1798   We split these based on the start state:
1799   
1800   1. ‘normal’ states take some [S n] normal steps and simulates them by [S m]
1801      normal steps in Cminor;
1802   2. call and return steps are simulated by a call/return step plus [m] normal
1803      steps (to copy stack allocated parameters / results); and
1804   3. lone cost label steps are simulated by a lone cost label step
1805   
1806   These should allow us to maintain enough structure to identify the Cminor
1807   subtrace corresponding to a measurable Clight subtrace.
1808 *)
1809(*
1810lemma clight_cminor_call_return :
1811  ∀g1, g2.
1812  ∀INV:clight_cminor_inv g1 g2.
1813  ∀s1,s1'.
1814  clight_cminor_rel g1 g2 INV s1 s1' →
1815  match Clight_classify s1 with
1816  [ cl_call ⇒ true
1817  | cl_return ⇒ true
1818  | _ ⇒ false ] →
1819  ∀s2,tr. step … (pcs_exec cl_pre) g1 s1 = Value … 〈tr, s2〉 →
1820  ∃m. after_n_steps m ?? (pcs_exec cm_pre) g2 s1' (λs.cminor_normal s) (λtr',s2'.
1821    tr = tr' ∧
1822    clight_cminor_rel g1 g2 INV s2 s2' ∧
1823      (m = 0 → lex_lt (measure_Clight s2) (measure_Clight s1))
1824  ).
1825#g1 #g2 #INV #s1 #s1' #Hstate_rel #Hclight_class
1826inversion Hstate_rel
1827[ 1: (* normal *)
1828  #cl_ge #cm_ge #INV' #cl_s
1829  #cm_s #cl_k #cm_k #cm_st #cl_f #cm_f #rettyp
1830  #alloc_type #cl_env #cl_m #cm_env #cm_m #stackptr #stacksize
1831  (* introduce everything *)
1832  #fInv #sInv #kInv #Htarget_type #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function
1833  #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls
1834  #flag  #Htrans_inv #Htrans_stmt #Hincl #HA #HB #HC
1835  #HE #HF #HG #HI #HJ #HK
1836  @(jmeq_absorb ?????) #H1 @(jmeq_absorb ?????) #H2
1837  destruct (H1 H2)
1838  @(jmeq_absorb ?????) #H3 @(jmeq_absorb ?????) #H4 @(jmeq_absorb ?????) #H5
1839  destruct (H3 H4 H5)
1840  @False_ind @Hclight_class
1841| 5:
1842  #cl_ge #cm_ge #INV' #cl_s
1843  #cm_s #cl_k #cm_k #cm_st #cl_f #cm_f #rettyp
1844  #alloc_type #cl_k #cm_k #sz #sg #cl_ty #cl_cond_desc #cl_body #entry_lab #exit_lab
1845  #cm_cond #cm_body #cm_stack #rettyp' #kInv
1846  (* introduce everything *)
1847  #fInv #sInv #kInv #Htarget_type #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function
1848  #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls
1849  #lbl1 #lbl2 #Em #Htmp_vars #Hcharac #Hexec #Hinj #Hmatching #Hem #Hframe #Hcond_tr
1850  #Htransl #Hex1 #Hex2 #Htransinv #Hmklabs #Htranstmt #Hincl
1851  #Hlabdecl #Hinv1 #Hinv2 #Hfindlab
1852  @(jmeq_absorb ?????) #H1 @(jmeq_absorb ?????) #H2
1853  destruct (H1 H2)
1854  @(jmeq_absorb ?????) #H3 @(jmeq_absorb ?????) #H4 @(jmeq_absorb ?????) #H5
1855  destruct (H3 H4 H5)
1856  @False_ind @Hclight_class
1857| 2:
1858  #cl_ge #cm_ge #INV' #cl_f #cm_f #cl_k #cm_k #alloc_type
1859  #cl_env #cl_m #cm_env #cm_m #cm_st #stackptr #stacksize
1860  #stmt_univ #Em #Htmp_vars_well_allocated #Halloc_hyp #Hcl_env_hyp
1861  #Hinjection #Hmatching #HEm_fn_id #Hframe_spec #Hcont_rel
1862  @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
1863  destruct (HA HB)
1864  @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE #_
1865  destruct (HC HD HE)
1866  inversion Hcont_rel
1867  [ #kcl_ge #kcm_ge #kINV #kcl_f #kcm_f #ktarget_type #kcl_env #kcm_env #kalloc_type #kstack #Hkstack
1868    @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
1869    destruct (HA HB)
1870    @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
1871    destruct (HC HD HE)
1872    @(jmeq_absorb ?????) #HF @(jmeq_absorb ?????) #HG @(jmeq_absorb ?????) #HH
1873    @(jmeq_absorb ?????) #HI @(jmeq_absorb ?????) #HJ @(jmeq_absorb ?????) #HK @(jmeq_absorb ?????) #HL
1874    destruct (HF HG HH HI HJ HK HL) #_
1875    #s2 #tr
1876    whd in ⊢ ((??%?) → ?); #Habsurd destruct (Habsurd)
1877  | (* Kseq *)
1878    #kcl_ge #kcm_ge #kINV #kcl_f #kcm_f #ktarget_type #kstack #kalloc_type #kcl_s #kcm_s
1879    #kcl_env #kcm_env #kcl_k' #kcm_k' #kstmt_univ #kstmt_univ' #klbl_univ #klbl_univ' #klbls #kflag
1880    * * * * #kHstmt_inv #kHlabels_translated #kHtmps_preserved
1881    #kHreturn_ok #kHlabel_wf #kHeq_translate #kHlabel_inclusion #kHcont_rel #_
1882    @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
1883    destruct (HA HB)
1884    @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
1885    destruct (HC HD HE)
1886    @(jmeq_absorb ?????) #HF @(jmeq_absorb ?????) #HG @(jmeq_absorb ?????) #HH @(jmeq_absorb ?????) #HI
1887    @(jmeq_absorb ?????) #HJ @(jmeq_absorb ?????) #HK @(jmeq_absorb ?????) #HL
1888    destruct (HF HG HH HI HJ HK HL) #_
1889    #s2 #tr
1890    whd in ⊢ ((??%?) → ?); #Habsurd destruct (Habsurd)
1891  | (* *)
1892    #kcl_ge #kcm_ge #kINV #kcl_f #kcm_f #ktarget_type #kstack #kalloc_type #kcl_env #kcm_env
1893    #kcl_k' #kcm_k' #ksz #ksg #kcl_ty #kcl_cond_desc #kcl_body #kHeq_ty #kcm_cond #kcm_body
1894    #kentry #kexit #kstmt_univ #kstmt_univ' #klbl_univ #klbl_univ' #klbl_univ''
1895    #klbls #kHtranslate_inv #kHexpr_vars #kHtranslate_expr #kfInv #kHlabel_declared
1896    #kHinv #kHmklabels #kHeq_translate #kHlabel_inclusion #kHfind_label
1897    (*     
1898    * * * * #kHentry_declared * * * *
1899    * * * #kHcond_vars_declared #Hnoise #Hnoise' #Hnoise''
1900    #kHcont_inv #kHmklabels #kHeq_translate
1901    #kHfind_label *) #kHcont_rel #_
1902    @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
1903    destruct (HA HB)
1904    @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
1905    destruct (HC HD HE)
1906    @(jmeq_absorb ?????) #HF @(jmeq_absorb ?????) #HG @(jmeq_absorb ?????) #HH
1907    @(jmeq_absorb ?????) #HI @(jmeq_absorb ?????) #HJ @(jmeq_absorb ?????) #HK
1908    @(jmeq_absorb ?????) #HL
1909    destruct (HF HG HH HI HJ HK HL) #_
1910    #s2 #tr
1911    whd in ⊢ ((??%?) → ?); #Habsurd destruct (Habsurd)
1912  ]   
1913| 3:
1914  #cl_ge #cm_ge #INV' #alloc_type
1915  #cl_env #cl_m #cm_env #cm_m #cm_st #stackptr #func_univ
1916  #cl_f #cm_f #Hglobals_fresh #Hfundef_fresh
1917  #rettyp #cl_k #cm_k #fblock *
1918  #Hrettyp #Hfind_funct_cl #Hfind_func_cm #Htranslate_function #Hcont_rel
1919  #fun_id #cl_retval #cm_retval #sInv #fInv #kInv #cl_args #cm_args
1920  @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
1921  destruct (HA HB)
1922  @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
1923  destruct (HC HD HE) #_
1924  #s2 #tr whd in ⊢ ((??%?) → ?);
1925  @(match (exec_alloc_variables empty_env cl_m (fn_params cl_f@fn_vars cl_f))
1926    return λx. (x = (exec_alloc_variables empty_env cl_m (fn_params cl_f@fn_vars cl_f))) → ?
1927    with
1928    [ mk_Prod new_cl_env cl_m_alloc ⇒ ?
1929    ] (refl ? (exec_alloc_variables empty_env cl_m (fn_params cl_f@fn_vars cl_f))))
1930  #Hexec_alloc_variables normalize nodelta
1931  #Hstep
1932  cases (bindIO_inversion ??????? Hstep) -Hstep
1933  #cl_m_init * #Hexec_bind_parameters
1934  whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) 
1935  %{1} whd whd in ⊢ (??%?);
1936  (* Alloc big chunk of data of size (f_stacksize cm_f) *)
1937  @(match (alloc cm_m 0 (f_stacksize cm_f))
1938    return λx. (alloc cm_m 0 (f_stacksize cm_f) = x) → ?
1939    with
1940    [ mk_Prod new_cm_mem new_cm_stackptr ⇒ ?
1941    ] (refl ? (alloc cm_m 0 (f_stacksize cm_f))))
1942  #H_cm_alloc normalize nodelta
1943  (* Initialise CM /parameters/ *)
1944
1945 
1946  %{(S (times 3 (|fn_vars|)))} -Hclight_class
1947  lapply (exec_alloc_bind_params_same_length … Hexec_bind_parameters)
1948  elim cl_args in Hstate_rel Hexec_alloc;
1949  [ #Hstate_rel whd in ⊢ ((??%%) → ?);
1950
1951    whd in match (exec_bind_parameters ????);
1952
1953  exec_alloc_variables empty_env cl_m (fn_params cl_f@fn_vars cl_f) = 〈cl_env, cl_m'〉
1954   
1955 
1956  lapply (let_prod_as_inversion ?????? Hstep)
1957    @(jmeq_absorb ?????) #HF @(jmeq_absorb ?????) #HG @(jmeq_absorb ?????) #HH
1958    @(jmeq_absorb ?????) #HI @(jmeq_absorb ?????) #HJ @(jmeq_absorb ?????) #HK
1959    @(jmeq_absorb ?????) #HL
1960    destruct (HF HG HH HI HJ HK HL) #_
1961    #s2 #tr
1962 
1963 
1964  #Em #Htmp_vars_well_allocated #Halloc_hyp #Hcl_env_hyp
1965  #Hinjection #Hmatching #HEm_fn_id #Hframe_spec #Hcont_rel
1966] qed.  *)
1967
1968lemma clight_cminor_normal :
1969    ∀g1,g2.
1970    ∀INV:clight_cminor_inv g1 g2.
1971    ∀s1,s1'.
1972    clight_cminor_rel g1 g2 INV s1 s1' →
1973    clight_normal s1 →
1974    ¬ pcs_labelled cl_pre g1 s1 →
1975    ∀s2,tr. step … (pcs_exec cl_pre) g1 s1 = Value … 〈tr,s2〉 →   
1976    ∃m. after_n_steps m ?? (pcs_exec cm_pre) g2 s1' (λs.cminor_normal s) (λtr',s2'.
1977      tr = tr' ∧
1978      clight_cminor_rel g1 g2 INV s2 s2' ∧
1979      (m = 0 → lex_lt (measure_Clight s2) (measure_Clight s1))
1980    ).
1981#g1 #g2 #INV #s1 #s1' #Hstate_rel #Hclight_normal #Hnot_labeleld
1982inversion Hstate_rel
1983[ 1: (* Normal state *)
1984     (* ---------------------------------------------------------------------- *)
1985#cl_ge #cm_ge #INV' #cl_s
1986(* case analysis on Clight statement *)
1987cases cl_s
1988[ 1: | 2: #lhs #rhs | 3: #retv #func #args | 4: #stm1 #stm2 | 5: #cond #iftrue #iffalse | 6: #cond #body
1989| 7: #cond #body | 8: #init #cond #step #body | 9,10: | 11: #retval | 12: #cond #switchcases | 13: #lab #body
1990| 14: #lab | 15: #cost #body ]
1991(*
1992[ 11: (* Return case *)
1993     #cm_s #cl_k #cm_k #cm_st #cl_f #cm_f #rettyp
1994     #alloc_type #cl_env #cl_m #cm_env #cm_m #stackptr #stacksize
1995     (* introduce everything *)
1996     #fInv #sInv #kInv #Htarget_type #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function
1997     #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls
1998     #flag #Htrans_inv #Htranslate #Hlabel_inclusion #Hcont_rel
1999     #Em #Htmp_vars_well_allocated #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id
2000     @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
2001     destruct (HA HB)
2002     @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE #_
2003     destruct (HC HD HE)
2004     whd in Htranslate:(??%?);
2005     cases retval in Htranslate; normalize nodelta
2006     [ cases rettyp in Htrans_inv Hcont_rel;
2007       [ 2: #opttyp normalize nodelta #Htrans_inv #_
2008            #Habsurd destruct (Habsurd)
2009       | 1: #Htrans_inv #Hcont_rel normalize nodelta #Heq destruct (Heq)
2010            #s2 #tr whd in ⊢ ((??%?) → ?);
2011            cases (fn_return cl_f)
2012            [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
2013            | #structname #fieldspec | #unionname #fieldspec | #id ]
2014            normalize nodelta
2015            [ 1:
2016            | *: #Habsurd destruct (Habsurd) ]
2017            whd in ⊢ ((??%?) → ?);
2018            #Heq destruct (Heq)
2019            %{1} whd @conj try @conj
2020            [ 3: #Habsurd destruct (Habsurd)
2021            | 1: @refl ]
2022            @CMR_return
2023*)     
2024[ 6: (* While *)
2025     #cm_s #cl_k #cm_k #cm_st #cl_f #cm_f #rettyp
2026     #alloc_type #cl_env #cl_m #cm_env #cm_m #stackptr #stacksize
2027     (* introduce everything *)
2028     #fInv #sInv #kInv #Htarget_type #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function
2029     #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls
2030     #flag * * * * #Hstmt_inv_cm cases cond #cond_desc #cond_ty
2031     (* early case analysis to avoid dependency hell *)
2032     cases cond_ty
2033     [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
2034     | #structname #fieldspec | #unionname #fieldspec | #id ]     
2035     #Hlabels_translated #Htmps_preserved
2036     #Hreturn_ok #Hlabel_wf #Htranslate #Hlabel_inclusion #tmpenv #Htmpenv
2037     #Hcont_rel
2038     #Em #Htmp_vars_well_allocated
2039     #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id
2040     #Hframe_spec #Henv_below
2041     @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
2042     destruct (HA HB)
2043     @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE #_
2044     destruct (HC HD HE)
2045     lapply Htranslate -Htranslate
2046     [ 1: generalize in match (conj ????); #Hugly_inv
2047     | 2: generalize in match (conj ????); #Hugly_inv
2048     | 3: generalize in match (conj ????); #Hugly_inv
2049     | 4: generalize in match (conj ????); #Hugly_inv
2050     | 5: generalize in match (conj ????); #Hugly_inv
2051     | 6: generalize in match (conj ????); #Hugly_inv
2052     | 7: generalize in match (conj ????); #Hugly_inv
2053     | 8: generalize in match (conj ????); #Hugly_inv ]
2054     #Htranslate
2055     cases (bind_inversion ????? Htranslate) -Htranslate
2056     whd in match (typeof ?); whd in match (typ_of_type ?); *
2057     #cm_cond #Hexpr_vars_cond * #Htranslate_cond normalize nodelta
2058     [ 3,4,5,8: whd in ⊢ ((??%%) → ?); #Habsurd destruct (Habsurd) ]
2059     #Htranslate normalize nodelta
2060     lapply (let_prod_as_inversion ?????? Htranslate) -Htranslate
2061     * * #entry_label #exit_label * #lbl_univ0 * #Hmk_label_eq *
2062     #Hmk_label_eq_bis normalize nodelta #Htranslate
2063     cases (bind_inversion ????? Htranslate) -Htranslate
2064     * * * #stmt_univ0 #lbl_univ1 #cm_body
2065     #Htrans_inv * #Htrans_body normalize nodelta
2066     [ generalize in ⊢ ((??(??(????%))?) → ?);
2067       #Htrans_inv'
2068     | generalize in ⊢ ((??(??(????%))?) → ?);
2069       #Htrans_inv'
2070     | generalize in ⊢ ((??(??(????%))?) → ?);
2071       #Htrans_inv'
2072     | generalize in ⊢ ((??(??(????%))?) → ?);
2073       #Htrans_inv' ]
2074     whd in ⊢ ((???%) → ?);
2075     #Heq destruct (Heq)
2076     #s2 #tr whd in ⊢ ((??%?) → ?);
2077     #Hstep
2078     cases (bindIO_inversion ??????? Hstep) -Hstep * #cond_val #cond_trace
2079     * #Hcl_exec_cond #Hstep
2080     cases (bindIO_inversion ??????? Hstep) -Hstep
2081     #cl_cond_bool * #Hcl_bool_of_val whd in ⊢ ((??%%) → ?);
2082     cases cl_cond_bool in Hcl_bool_of_val;
2083     [ 1,3,5,7: (* cond = true: continue looping *)
2084       #Hcl_bool_of_val normalize nodelta
2085       #Heq destruct (Heq)
2086       %{4} whd whd in ⊢ (??%?); normalize nodelta
2087       [ generalize in match (proj1 ???); #Hpresent_ifthenelse
2088       | generalize in match (proj1 ???); #Hpresent_ifthenelse
2089       | generalize in match (proj1 ???); #Hpresent_ifthenelse
2090       | generalize in match (proj1 ???); #Hpresent_ifthenelse ]
2091       (* Exhibit simulation of condition evaluation *)
2092       lapply (eval_expr_sim … Halloc_hyp … Hcl_env_hyp … Hinjection … Hmatching) * #Hsim #_
2093       [ lapply (Hsim (Expr cond_desc Tvoid) … Htranslate_cond ?? Hpresent_ifthenelse Hcl_exec_cond)
2094       | lapply (Hsim (Expr cond_desc (Tint sz sg)) … Htranslate_cond ?? Hpresent_ifthenelse Hcl_exec_cond)
2095       | lapply (Hsim (Expr cond_desc (Tstruct structname fieldspec)) … Htranslate_cond ?? Hpresent_ifthenelse Hcl_exec_cond)
2096       | lapply (Hsim (Expr cond_desc (Tunion unionname fieldspec)) … Htranslate_cond ?? Hpresent_ifthenelse Hcl_exec_cond) ]
2097       * #cm_val_cond * #Hcm_eval_cond #Hvalue_eq >Hcm_eval_cond
2098       whd in match (m_bind ?????);
2099       >(eval_bool_of_val_to_Cminor … Hvalue_eq … Hcl_bool_of_val)
2100       normalize nodelta whd
2101       [ generalize in match (proj1 ???); #Hnoise'
2102         generalize in match (conj ????); #Hnoise''
2103       | generalize in match (proj1 ???); #Hnoise'
2104         generalize in match (conj ????); #Hnoise''
2105       | generalize in match (proj1 ???); #Hnoise'
2106         generalize in match (conj ????); #Hnoise''
2107       | generalize in match (proj1 ???); #Hnoise'
2108         generalize in match (conj ????); #Hnoise'' ]
2109       @conj try @conj
2110       [ 3,6,9,12: #Habsurd destruct (Habsurd)
2111       | 1,4,7,10: normalize >append_nil @refl
2112       | 2,5,8,11:
2113            cut (lset_inclusion (identifier Label) (labels_of cm_body) (labels_of (f_body cm_f)))
2114            [ 1,3,5,7:
2115              lapply Hlabel_inclusion
2116              @transitive_lset_inclusion
2117              @cons_preserves_inclusion
2118              @lset_inclusion_union %1
2119              @lset_inclusion_union %1
2120              @lset_inclusion_union %1
2121              @reflexive_lset_inclusion ]
2122            #Hlabels_of_body
2123            cut (Exists (identifier Label) (λl'.l'=entry_label) (labels_of (f_body cm_f)))
2124            [ 1,3,5,7: @(lset_inclusion_Exists ????? Hlabel_inclusion)
2125              %1 @refl ]
2126            #Hentry_exists
2127            cut (Exists (identifier Label) (λl'.l'=exit_label) (labels_of (f_body cm_f)))
2128            [ 1,3,5,7: @(lset_inclusion_Exists ????? Hlabel_inclusion)
2129              %2 @Exists_append_r %1 @refl ]
2130            #Hexit_exists
2131            @(CMR_normal … Htrans_body) try assumption
2132            @(ClCm_cont_while … (sym_eq … Hmk_label_eq) … Htrans_body) try assumption
2133            try @refl
2134            [ 1,4,7,10: @eq_to_jmeq assumption
2135            | 2,5,8,11:
2136                 @conj try assumption @conj @conj try assumption @conj @conj try assumption
2137                 try @conj try assumption try @conj try assumption
2138                 try @conj try assumption try @conj try assumption
2139            | *: (* find_label_always *)
2140                 (* TODO /!\ implement necessary invariant on label lookup *)
2141                 @cthulhu
2142            ]
2143       ]
2144     | 2,4,6,8: (* cond = false: stop looping *)
2145       #Hcl_bool_of_val normalize nodelta #Heq destruct (Heq)
2146       %{5} whd whd in ⊢ (??%?); normalize nodelta
2147       [ generalize in match (proj1 ???); #Hpresent_ifthenelse
2148       | generalize in match (proj1 ???); #Hpresent_ifthenelse
2149       | generalize in match (proj1 ???); #Hpresent_ifthenelse
2150       | generalize in match (proj1 ???); #Hpresent_ifthenelse ]
2151       (* Exhibit simulation of condition evaluation *)
2152       lapply (eval_expr_sim … Halloc_hyp … Hcl_env_hyp … Hinjection … Hmatching) * #Hsim #_
2153       [ lapply (Hsim (Expr cond_desc Tvoid) … Htranslate_cond ?? Hpresent_ifthenelse Hcl_exec_cond)
2154       | lapply (Hsim (Expr cond_desc (Tint sz sg)) … Htranslate_cond ?? Hpresent_ifthenelse Hcl_exec_cond)
2155       | lapply (Hsim (Expr cond_desc (Tstruct structname fieldspec)) … Htranslate_cond ?? Hpresent_ifthenelse Hcl_exec_cond)
2156       | lapply (Hsim (Expr cond_desc (Tunion unionname fieldspec)) … Htranslate_cond ?? Hpresent_ifthenelse Hcl_exec_cond) ]       
2157       * #cm_val_cond * #Hcm_eval_cond #Hvalue_eq >Hcm_eval_cond
2158       whd in match (m_bind ?????);
2159       >(eval_bool_of_val_to_Cminor … Hvalue_eq … Hcl_bool_of_val) normalize nodelta whd
2160       [ generalize in match (proj2 ???); #Hnoise'
2161         generalize in match (proj2 ???); #Hnoise''
2162       | generalize in match (proj2 ???); #Hnoise'
2163         generalize in match (proj2 ???); #Hnoise''
2164       | generalize in match (proj2 ???); #Hnoise'
2165         generalize in match (proj2 ???); #Hnoise''
2166       | generalize in match (proj2 ???); #Hnoise'
2167         generalize in match (proj2 ???); #Hnoise'' ]
2168       @conj try @conj try @conj
2169       [ 1,4,7,10: normalize >append_nil >append_nil @refl
2170       | 2,5,8,11:
2171          @(CMR_normal … Htranslate_function … DoNotConvert) try assumption
2172          try @refl try @(env_below_freshgen_preserved_by_translation … Henv_below Htrans_body)
2173       | *: #Habsurd destruct (Habsurd) ]
2174   ]
2175| 3: (* Call *)
2176     #cm_s #cl_k #cm_k #cm_st #cl_f #cm_f #rettyp
2177     #alloc_type #cl_env #cl_m #cm_env #cm_m #stackptr #stacksize
2178     (* introduce everything *)
2179     #fInv #sInv #kInv #Htarget_type #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function
2180     #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls
2181     #flag * * * * #Hstmt_inv #Hlabels_translated #Htmps_preserved #Hreturn_ok #Hlabel_wf
2182     (* generalize away ugly proof *)
2183     generalize in ⊢ (∀_:(???(??(????%))).?); #Hugly
2184     #Htranslate #Hlabel_inclusion #tmpenv #Htmpenv #Hcont_rel #Em
2185     #Htmp_vars_well_allocated
2186     #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id
2187     #Hframe_spec #Henv_below
2188     @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
2189     destruct (HA HB)
2190     @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
2191     destruct (HC HD HE) #_
2192     (* back to unfolding Clight execution *)
2193     cases (bind_inversion ????? Htranslate) -Htranslate *
2194     #ef #Hexpr_vars_ef * #Htranslate_ef normalize nodelta #Htranslate
2195     cases (bind_inversion ????? Htranslate) -Htranslate *
2196     #ef' #Hexpr_vars_local_ef' * #Htyp_should_eq_ef
2197     cases (typ_should_eq_inversion (typ_of_type (typeof func)) ASTptr … Htyp_should_eq_ef)
2198     -Htyp_should_eq_ef #Htyp_equality_ef
2199     #Heq_ef_ef' #Htranslate
2200     cases (bind_inversion ????? Htranslate) -Htranslate *
2201     #cm_args #Hall_variables_from_args_local *
2202     whd in ⊢ ((???%) → ?); #Hargs_spec
2203     @(match retv
2204       return λx. retv = x → ?
2205       with
2206       [ None ⇒ λHretv. ?
2207       | Some lhs ⇒ λHretv. ?
2208       ] (refl ? retv))
2209     normalize nodelta
2210     [ 2: (* return something *)
2211       #Hdest cases (bind_inversion ????? Hdest) -Hdest #dest *
2212       inversion dest normalize nodelta
2213       [ (* register dest *) #var_id #His_local @(jmeq_absorb ?????) #Hdest
2214         #Htranslate_dest whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
2215         (* make explicit the nature of lhs, allowing to prove that no trace is emitted *)
2216         lapply (translate_dest_id_inversion  … Htranslate_dest) #Hlhs_eq
2217       | * #cm_expr #Hexpr_vars_cm #Hdest #Htranslate_dest #Hgensym
2218         lapply (breakup_dependent_match_on_pairs ?????? Hgensym) -Hgensym
2219         * #ret_var * #new_gensym * #Heq_alloc_tmp * #_ #Hgensym
2220         lapply (breakup_dependent_match_on_pairs ?????? Hgensym) -Hgensym
2221         * #tmp_var * #new_gensym' * #Heq_alloc_tmp' * #_
2222         generalize in ⊢ ((??(?? (????%) )?) → ?); #Hstmt_inv_after_gensym
2223         whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
2224       ]
2225     | 1: (* return void *)
2226          generalize in ⊢ ((??(??(????%))?) → ?); #Hugly2
2227          whd in ⊢ ((???%) → ?); #Heq destruct (Heq) ]
2228     (* Now, execute the Clight call *)
2229     #s2 #tr #Htranslate
2230     cases (bindIO_inversion ??????? Htranslate) -Htranslate *
2231     #CL_callee_val #CL_callee_trace * #Hexec_CL_callee normalize nodelta
2232     whd in ⊢ ((???%) → ?); #Htranslate
2233     cases (bindIO_inversion ??????? Htranslate) -Htranslate *
2234     #CL_args #CL_args_trace * #Hexec_CL_args #Htranslate
2235     cases (bindIO_inversion ??????? Htranslate) -Htranslate
2236     * #CL_callee_fundef #CL_callee_id * #Hfind_funct
2237     (* We've got the CL fundef. Extract a function pointer out of it. *)
2238     lapply (opt_to_io_Value ?????? Hfind_funct) -Hfind_funct #Hfind_funct
2239     cases (find_funct_inversion ???? Hfind_funct)
2240     #CL_callee_ptr * * * #HCL_callee_eq destruct (HCL_callee_eq)
2241     (* Done. Now stash the resulting properties of this pointer in the context. *)
2242     #HCL_callee_ptr_offset_eq_zero #HCL_callee_ptr_region_eq_Code
2243     (* Some more properties, that should stay hidden. XXX we discard them, this should not hinder the proof *)     
2244     * #block_id * #Hblock_id_neg #Hlookup -Hlookup -Hblock_id_neg -block_id
2245     (* Now, break up a safety check for the type of the function and finally, execute the
2246      * CL lvalue supposed to store the result of the function call. This will yield a pointer
2247      * that will be stored in the Callstate, until the function call returns and we store te
2248      * result inside it. Of course, this does not apply to the case wich returns void. *)
2249     #Htranslate
2250     cases (bindIO_inversion ??????? Htranslate) -Htranslate #Htype_of_fundef *
2251     #Hassert_type_eq
2252     [ 1,2: (* Cases where we return something. *)
2253            #Htranslate
2254            cases (bindIO_inversion ??????? Htranslate) -Htranslate * *
2255            #CL_lvalue_block #CL_lvalue_offset #CL_lvalue_trace *
2256            whd in ⊢ ((???%) → (??%%) → ?);
2257            [ >Hlhs_eq #HCL_exec_lvalue
2258              (* The trace is empty since we execute a variable *)
2259              cut (CL_lvalue_trace = [])
2260              [ lapply (res_to_io ????? HCL_exec_lvalue)
2261                #H' whd in H':(??%?); cases (lookup ????) in H'; normalize nodelta
2262                [ 2: #b #Heq destruct (Heq) @refl
2263                | #H cases (bind_inversion ????? H) #H24 * #H27 #H28
2264                  whd in H28:(???%); destruct (H28) @refl ]
2265              ] #H destruct (H)
2266            | #HCL_exec_lvalue ]
2267     | 3: ]
2268     whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
2269     (* We have reached the final Clight state. Now execute the Cminor transalted code. *)
2270     [ 1: (* Return to a variable *)
2271          %{1} whd whd in ⊢ (??%?); normalize nodelta
2272     | 2: (* Return to memory location. Need to create a tmp CM local variable to store the
2273           * lvalue ptr (otherwise trace does not match CL). *)
2274          %{5} whd whd in ⊢ (??%?); normalize nodelta
2275          whd in match (eval_expr ???????);
2276          whd in match (m_bind ?????);
2277          (* Evalue Cminor lvalue. Need to feed some invariants to the simulation lemma, that
2278           * we bake here and now. *)
2279          cut (expr_vars ASTptr cm_expr
2280                  (λid:ident.λty:typ.present SymbolTag val cm_env id))
2281          [ cases sInv * * * * * * * #_ #H #_ #_ #_ @H ] #Hexpr_vars_cut
2282          (* Apply simulation lemma for lvalues *)
2283          lapply (translate_dest_MemDest_simulation … Htranslate_dest HCL_exec_lvalue)
2284          try assumption try @refl
2285          * #CM_lvalue * #HCM_eval_lvalue >HCM_eval_lvalue #Hvalue_eq_lvalues
2286          normalize nodelta generalize in match (proj1 ???); #Htmp_var_present
2287          (* Make explicit the fact that the CM lvalue is a pointer *)
2288          cases (value_eq_ptr_inversion … Hvalue_eq_lvalues) #CM_lvalue_ptr * #HCM_value_ptr_eq #HCM_lvalue_ptr_trans
2289          >HCM_value_ptr_eq
2290          lapply (Htmp_vars_well_allocated … tmp_var Htmp_var_present (Tpointer (typeof lhs)) ? (Vptr CM_lvalue_ptr) ?)
2291          [ 1: normalize cases CM_lvalue_ptr #b #o %3
2292          | 2: lapply (alloc_tmp_in_genlist … (sym_eq ??? Heq_alloc_tmp) (sym_eq ??? Heq_alloc_tmp'))
2293               #Hexists' @(lset_inclusion_Exists … Hexists' Htmpenv) 
2294          ]
2295          * #CM_mem_after_store * #Hstorev #Hnew_inj >Hstorev
2296          whd in match (m_bind ?????); normalize nodelta
2297          whd whd in ⊢ (??%?); normalize nodelta
2298     | 3: %{1} whd whd in ⊢ (??%?); normalize nodelta
2299     ]
2300    (* cleanup ugliness *)
2301    [ 1: generalize in match (proj2 (present ????) (expr_vars ???) (proj1 ???));
2302    | 2: generalize in match (proj2 (present ????) (expr_vars ???) (proj1 ???));
2303    | 3: generalize in match (proj2 True ??); ]
2304    #Hexpr_vars_present_ef'
2305    [ 1,3:
2306       cases (eval_expr_sim … INV' … Halloc_hyp … Hcl_env_hyp … Hinjection … Hmatching) #Hsim_expr #_
2307       cut (expr_vars (typ_of_type (typeof func)) ef
2308             (λid:ident.λty:typ.present SymbolTag val cm_env id))
2309       [ 1,3: lapply Heq_ef_ef' lapply Hexpr_vars_ef lapply ef >Htyp_equality_ef
2310                #ef #Hexpr_vars_ef @(jmeq_absorb ?????) #Heq destruct (Heq)
2311                @Hexpr_vars_present_ef' ]
2312       #Hexpr_vars_present_ef
2313       lapply (Hsim_expr … Htranslate_ef … Hexpr_vars_present_ef … Hexec_CL_callee)
2314       -Hsim_expr * #cm_func_ptr_val * #Heval_func #Hvalue_eq_func
2315       cut (eval_expr cm_ge ASTptr ef' cm_env Hexpr_vars_present_ef'
2316             stackptr cm_m = OK (trace×val) 〈CL_callee_trace,cm_func_ptr_val〉)
2317       [ 1,3:
2318         lapply Heq_ef_ef' lapply Heval_func lapply Hexpr_vars_ef lapply Hexpr_vars_local_ef'
2319         lapply Hexpr_vars_present_ef lapply ef lapply Hexpr_vars_present_ef' lapply ef'
2320         <Htyp_equality_ef #ef' #HA #ef #HB #HC #HD #HE
2321         @(jmeq_absorb ?????) #Heq destruct (Heq) @HE ]
2322       -Heval_func #Heval_func >Heval_func
2323    | 2: (* treat case 2 as special, since the type differs slightly *)
2324       letin cm_env' ≝ (update_present SymbolTag val cm_env tmp_var Htmp_var_present (Vptr CM_lvalue_ptr))
2325       cut (memory_matching Em cl_ge cm_ge cl_m cm_m cl_env cm_env' INV' stackptr alloc_type)
2326     (*  cut (memory_matching Em cl_ge cm_ge cl_m CM_mem_after_store cl_env cm_env' INV' stackptr alloc_type) *)
2327       [ (* Proving preservation of the memory matching under store in "new" cminor memory zone.
2328            Use the property that the ident [tmp_var] is not in the clight env. *)
2329         #id lapply (Hmatching id)
2330         @(match (lookup ??? id)
2331           return λx. (lookup ??? id = x) → ?
2332           with
2333           [ None ⇒ λHeq_lookup. ?
2334           | Some blo ⇒ λHeq_lookup. ?
2335           ] (refl ? (lookup ??? id)))
2336         [ 1: #H @H ] normalize nodelta         
2337         cases (lookup ??? id) normalize nodelta
2338         [ 1: #H @H ] * #var_ty #cl_ty cases var_ty normalize nodelta
2339         [ #r #H @H
2340         | #n #H @H
2341         | #H #v #Hload_value_of_type lapply (H ? Hload_value_of_type)
2342           * #v' * #Hlookup_cm #Hvalue_eq %{v'} @conj try @Hvalue_eq
2343           lapply (alloc_tmp_env_invariant ?????? (sym_eq ??? Heq_alloc_tmp) Henv_below) #Henv_below'
2344           lapply (generated_id_not_in_env ???????? Henv_below' … Heq_lookup (sym_eq ??? Heq_alloc_tmp'))
2345           #Hneq <(update_lookup_opt_other … (Vptr CM_lvalue_ptr) … cm_env … Htmp_var_present … Hneq)
2346           assumption ] ] #Hmatching'
2347       cases (eval_expr_sim … INV' … Halloc_hyp ? cm_env' Hcl_env_hyp … Hinjection stackptr Hmatching')
2348       #Hsim_expr #_
2349       generalize in match (proj2 ???); #Hall_present
2350       generalize in match (proj1 ???); #Hret_present
2351       generalize in match (proj2 ???); #Hstore_inv
2352       generalize in match (conj ????); #Hstmt_inv
2353(*       cut (eval_expr cm_ge ? ef' cm_env' ? stackptr cm_m =
2354            (eval_expr cm_ge ASTptr ef' cm_env' ? stackptr cm_m)) try assumption try @refl
2355       #Heval_expr_rewrite >Heval_expr_rewrite -Heval_expr_rewrite *)
2356       lapply (Hsim_expr … Htranslate_ef … (Vptr CL_callee_ptr) CL_callee_trace ??)
2357       try assumption
2358       [ lapply Hexpr_vars_present_ef' lapply Heq_ef_ef' lapply Hexpr_vars_ef lapply Hexpr_vars_local_ef'
2359         lapply ef >Htyp_equality_ef #ef #HA #HB @(jmeq_absorb ?????) #Heq destruct (Heq) #x @x ]
2360       * #CM_callee_ptr * #Heval_func_cm #Hvalue_eq_func
2361       (* And some more shuffling types around to match the goal *)
2362       cut (eval_expr cm_ge ? ef' cm_env' Hexpr_vars_present_ef' stackptr cm_m = OK ? 〈CL_callee_trace,CM_callee_ptr〉)
2363       [ lapply Heval_func_cm -Heval_func_cm
2364         generalize in ⊢ ((??(?????%??)?) → ?);
2365         lapply Heq_ef_ef' -Heq_ef_ef'
2366         lapply Hexpr_vars_ef -Hexpr_vars_ef
2367         lapply Hexpr_vars_local_ef' -Hexpr_vars_local_ef'
2368         lapply Hexpr_vars_present_ef'
2369         lapply ef >Htyp_equality_ef #ef0 #HA #HB #HC @(jmeq_absorb ?????)
2370         #Heq destruct (Heq) #H1 #H2 @H2 ]
2371       #Heval_cm_func >Heval_cm_func ]
2372    whd in match (m_bind ?????);
2373    lapply (trans_fn … INV' … Hfind_funct)
2374    * #tmp_u * #cminor_fundef * #Hglobals_fresh_for_tmp_u * #Hfundef_fresh_for_tmp_u *
2375    #Htranslate_fundef #Hfind_funct_cm
2376    lapply (value_eq_ptr_inversion … Hvalue_eq_func) * #cm_func_ptr * #Hcm_func_ptr
2377    whd in ⊢ ((??%?) → ?);
2378    cases CL_callee_ptr in Hfind_funct Hfind_funct_cm HCL_callee_ptr_region_eq_Code HCL_callee_ptr_offset_eq_zero;
2379    #cm_block #cm_off #Hfind_funct #Hfind_funct_cm #Hregion_is_code #Hpoff_eq_zero destruct (Hpoff_eq_zero)
2380    whd in ⊢ ((??%?) → ?);
2381    [ 1,2: >(HEm_fn_id … cm_block Hregion_is_code)
2382    | 3: >(HEm_fn_id … cm_block Hregion_is_code) ]
2383    normalize nodelta
2384    cases cm_func_ptr in Hcm_func_ptr; #cm_block' #cm_off'
2385    #Hcm_func_ptr #Heq destruct (Hcm_func_ptr Heq)
2386    [ 1,2: >addition_n_0 >mk_offset_offv_id
2387    | 3: ]
2388    >(find_funct_to_find_funct_id ???? Hfind_funct_cm)
2389    whd in match (opt_to_res ???); normalize nodelta
2390    (* Again, isolate cases by type similarity *)
2391    [ 1,2:
2392      cut (All (𝚺t:typ.CMexpr t)
2393            (λx:𝚺t:typ.expr t.(
2394              match x with
2395              [ mk_DPair ty e ⇒
2396               expr_vars ty e
2397                 (λid:ident
2398                  .λty0:typ.present SymbolTag val cm_env id)])) cm_args)
2399      [ 1: cases sInv * * normalize nodelta * #_ #_ #Hall #_ #_ @Hall
2400      | 3: cases sInv * * normalize nodelta * #_ #_ #Hall #_ #_ @Hall ]
2401      #Hall
2402      cases (eval_exprlist_simulation …  Halloc_hyp Hcl_env_hyp Hinjection Hmatching ???? Hexec_CL_args Hargs_spec Hall)
2403      #cm_values * #Hcm_exec_list #Hcl_cm_values_eq >Hcm_exec_list
2404    | 3:
2405      lapply (eval_exprlist_simulation …  Halloc_hyp Hcl_env_hyp Hinjection ????? Hexec_CL_args Hargs_spec ?)
2406      try assumption
2407      * #cm_values * #Hcm_exec_list #Hcl_cm_values_eq >Hcm_exec_list
2408    ]
2409    whd in match (m_bind ?????); normalize nodelta whd @conj
2410    [ 2,4,6: #Habsurd destruct (Habsurd) ]
2411    @conj
2412    [ 1,3,5: normalize try @refl >append_nil >append_nil @refl ]
2413    [ 1: generalize in match (proj1 ? (expr_vars ???) (proj1 ???)); #Hugly_pres
2414    | 2: generalize in match (proj1 ? (expr_vars ???) (proj1 ???)); #Hugly_pres
2415    | 3: ]
2416    [ 3: @(CMR_call … Htranslate_function … Hinjection … Hmatching … HEm_fn_id) try assumption
2417         lapply (alloc_tmp_monotonic … (sym_eq ??? Heq_alloc_tmp)) #Hincl1
2418         lapply (alloc_tmp_monotonic … (sym_eq ??? Heq_alloc_tmp')) #Hincl2
2419         lapply (transitive_lset_inclusion … Hincl1 Hincl2) #Hincl3
2420         try /2 by transitive_lset_inclusion/
2421         lapply Htranslate_fundef -Htranslate_fundef
2422         lapply Hfundef_fresh_for_tmp_u -Hfundef_fresh_for_tmp_u
2423         cases CL_callee_fundef normalize nodelta
2424         [ 1: #cl_called_f #Hfundef_fresh_for_tmp_u #Htranslate_fundef @ClCm_cont_call_store
2425         | 2: #id #tl #ty #Hfd_fresh
2426              whd in ⊢ ((??%?) → ?); #Heq destruct (Heq) normalize nodelta @I ]
2427    | 1,2: (* no return or return to CM local variable *)
2428           @(CMR_call … Htranslate_function … Hinjection … Hmatching … HEm_fn_id) try assumption
2429           cases CL_callee_fundef in Hfundef_fresh_for_tmp_u Htranslate_fundef; normalize nodelta
2430           [ 1,3: (* Internal case *)
2431             #cl_called_f #Hfundef_fresh_for_tmp_u #Htranslate_fundef
2432             whd nodelta in match (typeof ?);
2433             [ @ClCm_cont_call_nostore normalize nodelta
2434               %{CL_lvalue_block} %{CL_lvalue_offset} %{(typeof lhs)} %{var_id}
2435               @conj @refl
2436             | @ClCm_cont_call_nostore normalize nodelta @I ]
2437           | 2,4: #fid #tl #ty #H1 #H2
2438             whd in H2:(??%?); destruct (H2) @I
2439           ]
2440    ]
2441| 1: (* Skip *)
2442    #cm_s #cl_k #cm_k #cm_st #cl_f #cm_f #rettyp
2443    #alloc_type #cl_env #cl_m #cm_env #cm_m #stackptr #stacksize
2444    (* introduce everything *)
2445    #fInv #sInv #kInv
2446    #Htarget_type #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function
2447    #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls
2448    #flag * * * * #Hstmt_inv #Hlabels_translated #Htmps_preserved
2449    #Hreturn_ok #Hlabel_wf generalize in match (conj ????); #Hugly
2450    whd in ⊢ ((??%?) → ?); #Heq_translate #Hlabel_inclusion
2451    #tmpenv #Htmpenv #Hcont_rel
2452    lapply Heq_translate -Heq_translate
2453    lapply Hugly -Hugly
2454    lapply Hlabel_wf -Hlabel_wf
2455    lapply Hreturn_ok -Hreturn_ok
2456    lapply Htmps_preserved -Htmps_preserved
2457    lapply Hlabels_translated -Hlabels_translated
2458    lapply Hstmt_inv -Hstmt_inv
2459    lapply Htranslate_function -Htranslate_function
2460    lapply Hfresh_globals -Hfresh_globals
2461    lapply Hfresh_function -Hfresh_function
2462    lapply Htarget_type -Htarget_type
2463    lapply kInv -kInv
2464    lapply sInv -sInv
2465    lapply fInv -fInv
2466    lapply stmt_univ -stmt_univ   
2467    lapply Htmpenv -Htmpenv
2468    lapply stmt_univ' -stmt_univ'
2469    lapply Hlabel_inclusion -Hlabel_inclusion
2470    (* case analysis on continuation *)
2471    inversion Hcont_rel
2472    [ (* Kstop continuation *)
2473      (* simplifying the goal using outcome of the inversion *)
2474      #kcl_ge #kcm_ge #kINV #kcl_f #kcm_f #ktarget_type #kcl_env #kcm_env #kcm_m #kalloc_type #ktmpenv #kstack #Hkstack
2475      @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
2476      destruct (HA HB)
2477      @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
2478      destruct (HC HD HE)
2479      @(jmeq_absorb ?????) #HF @(jmeq_absorb ?????) #HG @(jmeq_absorb ?????) #HH @(jmeq_absorb ?????) #HI
2480      destruct (HF HG HH HI)
2481      @(jmeq_absorb ?????) #HJ @(jmeq_absorb ?????) #HK @(jmeq_absorb ?????) #HL @(jmeq_absorb ?????) #HM
2482       @(jmeq_absorb ?????) #HN
2483      destruct (HJ HK HL HM HN) #_
2484      (* re-introduce everything *)
2485      #Hlabel_inclusion
2486      #stmt_univ' #Htmpenv #stmt_univ #fInv #sInv #kInv #Htarget_type #Hfresh_function #Hfresh_globals
2487      #Htranslate_function #Hstmt_inv #Hlabels_translated #Htmps_preserved
2488      #Hreturn_ok #Hlabel_wf
2489      #Hugly generalize in match (conj ????); #Hugly'
2490      (* reduce statement translation function *)
2491      #Heq_translate
2492      (* In this simple case, trivial translation *)
2493      destruct (Heq_translate)
2494      #Em #Htmp_vars_well_allocated
2495      #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id #Hframe_spec #Henv_below
2496      @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
2497      destruct (HA HB)
2498      @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
2499      destruct (HC HD HE) #_
2500      (* unfold the clight execution *)
2501      #s2 #tr whd in ⊢ ((??%?) → ?);
2502      inversion (fn_return kcl_f) normalize nodelta
2503      [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
2504      | #structname #fieldspec | #unionname #fieldspec | #id ]
2505      #Hfn_return whd in ⊢ ((??%?) → ?); #Heq destruct (Heq)
2506      %{1} whd @conj try @conj try @refl
2507      [ 2: #Habsurd destruct (Habsurd) ]
2508      (* Use the memory injection stuff to produce a new memory injection *)
2509      cut (memory_inj Em (free_list cl_m (blocks_of_env kcl_env)) (free kcm_m stackptr))
2510      [ @(freelist_memory_inj_m1_m2 Em cl_m kcm_m
2511            (free_list cl_m (blocks_of_env kcl_env))
2512            (free kcm_m stackptr) Hinjection (blocks_of_env kcl_env) stackptr ? (refl ??) (refl ??))
2513        assumption ]
2514      #Hinjection'
2515      @(CMR_return … Kend … Halloc_hyp Hcl_env_hyp … Hinjection') try assumption
2516      [ 2: #b lapply (Hmatching b)
2517           cases (lookup ?? kcl_env b) normalize nodelta
2518           [ 1: #H @H
2519           | 2: #b' cases (lookup ?? kalloc_type b) normalize nodelta
2520             [ 1: #H @H
2521             | 2: * #kalloc_type #ty normalize nodelta
2522                  cases kalloc_type normalize nodelta try //
2523                  #H #v #Hload_after_free @H
2524                  @(load_value_after_free_list_inversion … Hload_after_free)
2525             ]
2526           ]
2527      | 1: @(tmp_vars_well_allocated_conserved_by_frame_free … Hmatching … Htmp_vars_well_allocated)
2528      | 3: @ClCm_cont_stop @Hkstack
2529      ]
2530    | (* Kseq *)
2531      #kcl_ge #kcm_ge #kINV #kcl_f #kcm_f #ktarget_type #kstack #kalloc_type #ktmpenv #kcl_s #kcm_s
2532      #kcl_env #kcm_env #kcm_m #kcl_k' #kcm_k' #kstmt_univ #kstmt_univ' #klbl_univ #klbl_univ' #klbls #kflag
2533      * * * * #kHstmt_inv #kHlabels_translated #kHtmps_preserved
2534      #kHreturn_ok #kHlabel_wf #kHeq_translate #kHlabel_inclusion #kHident_inclusion #kHcont_rel #_
2535      @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
2536      destruct (HA HB)
2537      @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
2538      destruct (HC HD HE)
2539      @(jmeq_absorb ?????) #HF @(jmeq_absorb ?????) #HG @(jmeq_absorb ?????) #HH @(jmeq_absorb ?????) #HI
2540      destruct (HF HG HH HI)
2541      @(jmeq_absorb ?????) #HJ @(jmeq_absorb ?????) #HK @(jmeq_absorb ?????) #HL @(jmeq_absorb ?????) #HM
2542      @(jmeq_absorb ?????) #HN
2543      destruct (HJ HK HL HM HN) #_
2544      #Hlabel_inclusion
2545      #stmt_univ' #Htmpenv #stmt_univ #fInv #sInv #kInv #Htarget_type #Hfresh_function #Hfresh_globals
2546      #Htranslate_function #Hstmt_inv #Hlabels_translated #Htmps_preserved #Hreturn_ok #Hlabel_wf
2547      #Hugly generalize in match (conj ????); #Hugly'
2548      (* In this simple case, trivial translation *)
2549      #Heq_translate destruct (Heq_translate) #Em
2550      #Htmp_vars_well_alloc
2551      #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id #Hframe_spec #Henv_below
2552      @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
2553      destruct (HA HB)
2554      @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
2555      destruct (HC HD HE) #_
2556      #s2 #tr whd in ⊢ ((??%?) → ?); #Heq destruct (Heq)
2557      %{1} whd @conj [ 2: #Habsurd destruct (Habsurd) ] @conj try @refl
2558      (* close simulation *)
2559      @(CMR_normal … kHeq_translate … kHcont_rel … Hinjection … Hmatching) try assumption
2560      (* TODO Invariant on env_below_freshgen *)
2561       @cthulhu
2562    | (* Kwhile continuation *)
2563      #kcl_ge #kcm_ge #kINV #kcl_f #kcm_f #ktarget_type #kstack #kalloc_type #ktmpenv #kcl_env #kcm_env #kcm_m
2564      #kcl_k' #kcm_k' #ksz #ksg #kcl_ty #kcl_cond_desc #kcl_body #kHeq_ty #kcm_cond #kcm_body
2565      #kentry #kexit #kstmt_univ #kstmt_univ' #klbl_univ #klbl_univ' #klbl_univ''
2566      #klbls #kHtranslate_inv #kHexpr_vars #kHtranslate_expr #kfInv #kHlabel_declared
2567      #kHinv #kHmklabels #kHeq_translate #kHlabel_inclusion #kHident_inclusion #kHfind_label
2568      (*     
2569      * * * * #kHentry_declared * * * *
2570      * * * #kHcond_vars_declared #Hnoise #Hnoise' #Hnoise''
2571      #kHcont_inv #kHmklabels #kHeq_translate
2572      #kHfind_label *) #kHcont_rel #_
2573      @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
2574      destruct (HA HB)
2575      @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
2576      destruct (HC HD HE)
2577      @(jmeq_absorb ?????) #HF @(jmeq_absorb ?????) #HG @(jmeq_absorb ?????) #HH
2578      @(jmeq_absorb ?????) #HI @(jmeq_absorb ?????) #HJ @(jmeq_absorb ?????) #HK
2579      @(jmeq_absorb ?????) #HL @(jmeq_absorb ?????) #HM @(jmeq_absorb ?????) #HN
2580      destruct (HF HG HH HI HJ HK HL HM HN) #_
2581      #Hlabel_inclusion
2582      #stmt_univ' #Htmpenv #stmt_univ #fInv #sInv #kInv #Htarget_type #Hfresh_function #Hfresh_globals
2583      #Htranslate_function #Hstmt_inv #Hlabels_translated #Htmps_preserved #Hreturn_ok #Hlabel_wf
2584      #Hugly
2585      generalize in match (conj ????); #Hugly'
2586      (* In this simple case, trivial translation *)
2587      #Heq_translate destruct (Heq_translate)
2588      #Em #Htmp_vars_well_allocated
2589      #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching
2590      #HEm_fn_id #Hframe_spec #Henv_below
2591      @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
2592      destruct (HA HB)
2593      @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
2594      destruct (HC HD HE) #_ #s2 #tr
2595      whd in ⊢ ((??%?) → ?); #Heq destruct (Heq)
2596      lapply kHfind_label -kHfind_label
2597      generalize in ⊢ ((??(????%????)?) → ?); #Hlabel_exists
2598      generalize in ⊢ ((???(????%)) → ?); #Hmore_invariant
2599      #kHfind_label
2600      (* Kwhile cont case *)
2601      %{2} whd whd in ⊢ (??%?); normalize nodelta
2602      generalize in match (proj2 ???); #Hmore_noise
2603      generalize in match (proj1 ???); #Hmore_noise'
2604      >kHfind_label normalize nodelta
2605      whd @conj try @conj try @refl
2606      generalize in match (proj1 ???); #Hvars_present_in_ifthenelse
2607      generalize in match (proj2 ???); #Hcont_inv'
2608      [ 2: #Habsurd destruct (Habsurd) ]
2609      (* go to a special simulation state for while loops *)
2610      @(CMR_while … stacksize … Hcl_env_hyp … Hinjection … kHtranslate_expr … kHmklabels …  kHeq_translate)
2611      try assumption
2612      [ 1: (* TODO: lemma on Henv_below. We need to thread freshgens through cont_rel. *)
2613           @cthulhu
2614      | 2: cases Hmore_invariant * * #_ * * * * #_ #_ * #_ #_ * * #_ #H
2615           #_ #_ @H ]
2616    | 4,5: (* Continuations for Scall. TODO *)
2617      @cthulhu
2618    ]
2619| 2: (* Assign *)
2620     #cm_s #cl_k #cm_k #cm_st #cl_f #cm_f #rettyp
2621     #alloc_type #cl_env #cl_m #cm_env #cm_m #stackptr #stacksize
2622     (* introduce everything *)
2623     #fInv #sInv #kInv #Htarget_type #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function
2624     #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls
2625     #flag * * * * #Hstmt_inv_cm #Hlabels_translated #Htmps_preserved
2626     #Hreturn_ok #Hlabel_wf generalize in match (conj ????); #Hugly #Htranslate
2627     #Hlabel_inclusion #tmpenv #Htmpenv #Hcont_rel
2628     #Em #Htmp_vars_well_allocated
2629     #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id #Hframe_spec #Henv_below
2630     @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
2631     destruct (HA HB)
2632     @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE #_
2633     destruct (HC HD HE)
2634     lapply Htranslate -Htranslate
2635     (* case-split on lhs in order to reduce lvalue production in Cminor *)
2636     cases lhs #lhs_ed #lhs_ty
2637     cases (expr_is_Evar_id_dec lhs_ed)
2638     [ 2: * #var_id #Hlhs_ed destruct (Hlhs_ed)
2639          #Htranslate_statement
2640          cases (bind_inversion ????? Htranslate_statement)
2641          * #cm_rhs #Hexpr_vars_rhs * #Htranslate_rhs #Htranslate_statement'
2642          cases (bind_inversion ????? Htranslate_statement') -Htranslate_statement'
2643          #lhs_dest * #Htranslate_lhs
2644          cases (bind2_eq_inversion ?????? Htranslate_lhs) -Htranslate_lhs
2645          #alloctype * #type_of_var * #Hlookup_var_success
2646          cases alloctype in Hlookup_var_success;
2647          normalize nodelta
2648          [ 1: (* Global *) #r
2649               #Hlookup_var_success whd in ⊢ ((???%) → ?); #Hlhs_dest_eq
2650               destruct (Hlhs_dest_eq) normalize nodelta
2651               generalize in match (conj ????); #Hinvariant
2652               cases (type_eq_dec ??)
2653               [ 2: #Hneq normalize nodelta whd in ⊢ ((??%%) → ?);
2654                    #Habsurd destruct (Habsurd) ]
2655               normalize nodelta whd in match (typeof ?); #Heq_cl_types
2656               whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
2657               #s2 #tr whd in ⊢ ((??%?) → ?); #Hstep
2658               cases (bindIO_inversion ??????? Hstep) -Hstep
2659               * * #cl_blo #cl_off #cl_tr * whd in ⊢ ((??%?) → ?);
2660               #Hexec_lvalue #Hstep
2661               lapply (res_to_io ????? Hexec_lvalue) -Hexec_lvalue #Hexec_lvalue
2662               cases (bindIO_inversion ??????? Hstep) -Hstep
2663               * #cl_rhs_val #cl_trace * #Hexec_rhs #Hstep
2664               cases (bindIO_inversion ??????? Hstep) -Hstep
2665               #cl_mem_after_store_lhs * #Hstore
2666               whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
2667               lapply (opt_to_io_Value ?????? Hstore) -Hstore #Hstore
2668               %{1} whd whd in ⊢ (??%?); normalize nodelta
2669               generalize in match (proj1 ???); whd in ⊢ (% → ?); *
2670               whd in match (eval_expr ???????);
2671               whd in match (eval_constant ????);
2672               whd in Hexec_lvalue:(??%?);
2673               <(eq_sym … INV' var_id)
2674               lapply (Hmatching … var_id)
2675               cases (lookup ?? cl_env var_id) in Hexec_lvalue; normalize nodelta
2676               [ 1: #Heq_find_sym cases (bind_inversion ????? Heq_find_sym) -Heq_find_sym
2677                    #global_b * #Hopt_to_res lapply (opt_to_res_inversion ???? Hopt_to_res) -Hopt_to_res
2678                    #Hfind_symbol >Hfind_symbol
2679                    normalize nodelta
2680                    whd in ⊢ ((???%) → ?); #Heq destruct (Heq) #Hembed_eq
2681                    whd in match (m_bind ?????);
2682                    cases (eval_expr_sim … Halloc_hyp … Hcl_env_hyp … Hinjection … Hmatching) #Hsim_expr #_
2683                    lapply (Hsim_expr … Htranslate_rhs … (proj2 ?? (proj1 ?? (proj1 ?? sInv))) Hexec_rhs)
2684                    * #cm_rhs_val generalize in match (proj2 ???);
2685                    #Hexpr_vars_rhs * #Heval_expr_rhs #Hvalue_eq_rhs >Heval_expr_rhs
2686                    whd in match (m_bind ?????); whd in Hstore:(??%?); whd in Hstore:(??%?);
2687                    cases (store_value_of_type_success_by_value lhs_ty cl_m
2688                                    cl_mem_after_store_lhs cl_blo zero_offset cl_rhs_val Hstore)
2689                    #Haccess_mode #Hstorev
2690                    lapply (storen_parallel_aux ??? Hinjection … Hvalue_eq_rhs … Hembed_eq ??? Hstorev)
2691                    * #cm_mem_after_store_lhs * #Hstoren #Hinj whd in Hstoren:(??%?);
2692                    whd in Hstoren:(??%?); whd in match (shift_offset ???);
2693                    >sign_ext_same_size >addition_n_0
2694                    whd in match (storev ????);
2695                    lapply Hstoren whd in match (offset_plus ??);
2696                    >addition_n_0 -Hstoren
2697                    >Heq_cl_types #Hstoren >Hstoren
2698                    whd in match (opt_to_res ???); normalize nodelta
2699                    whd @conj try @conj try @refl
2700                    [ 2: #Habsurd destruct (Habsurd) ]
2701                    generalize in match (conj ????); #Hinv_vars
2702                    @CMR_normal try assumption
2703                    [ 2: @refl | *: ]
2704                    [ 3: @(memory_matching_preserved_by_parallel_stores … Hmatching)
2705                    | 2: @(well_allocated_preserved_by_parallel_stores … Htmp_vars_well_allocated)
2706                    | 1: @(clight_cminor_cont_rel_parametric_in_mem … Hcont_rel) ]
2707               | 2: #b #Heq destruct (Heq)
2708                    lapply (opt_to_res_inversion ???? Hlookup_var_success) #Hlookup_aux
2709                    >Hlookup_aux normalize nodelta @False_ind ]
2710          | 2: (* Stack *)
2711               #n #Hlookup_var_success
2712               whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
2713               normalize nodelta whd in ⊢ ((???%) → ?);
2714               cases (type_eq_dec ??) normalize nodelta #Htype_eq
2715               [ 2: #Habsurd destruct (Habsurd) ]
2716               #Heq destruct (Heq) #s2 #tr #Hstep
2717               cases (bindIO_inversion ??????? Hstep)
2718               * * #cl_lvalue_block #cl_offset #cl_trace * #Hexec_lvalue
2719               lapply (res_to_io ????? Hexec_lvalue) -Hexec_lvalue
2720               whd in ⊢ ((??%?) → ?);
2721               @(match lookup ?? cl_env var_id
2722                 return λx. (lookup ?? cl_env var_id = x) → ?
2723                 with
2724                 [ None ⇒ λH. ?
2725                 | Some cl_addr ⇒ λH. ?
2726                 ] (refl ? (lookup ?? cl_env var_id)))
2727               normalize nodelta
2728               [ (* Contradiction: a stack-allocated variable was necessarily in the environment. TODO *)
2729                 @cthulhu
2730               | #Heq destruct (Heq)
2731                 lapply (Hmatching var_id) >H normalize nodelta
2732                 >(opt_to_res_inversion ???? Hlookup_var_success) normalize nodelta
2733                 #Hembedding_to_stack #Hexec_cl_rhs
2734                 cases (bindIO_inversion ??????? Hexec_cl_rhs) -Hexec_cl_rhs *
2735                 #cl_rhs_result #cl_rhs_trace * #Hcl_exec_expr_rhs #Hcl_exec_store
2736                 cases (bindIO_inversion ??????? Hcl_exec_store) -Hcl_exec_store #cl_mem_after_store
2737                 * #Hstore_value_of_type lapply (opt_to_io_Value ?????? Hstore_value_of_type)
2738                 -Hstore_value_of_type
2739                 #Hstore_value_of_type
2740                 whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
2741                 %{1} whd whd in ⊢ (??%?); normalize nodelta
2742                 whd in match (eval_expr ???????);
2743                 whd in match (eval_constant ????);
2744                 whd in match (m_bind ?????);
2745                 cases (eval_expr_sim … Halloc_hyp … Hcl_env_hyp … Hinjection … Hmatching) #Hsim_expr #_
2746                 lapply (Hsim_expr … Htranslate_rhs … (proj2 ?? (proj1 ?? (proj1 ?? sInv))) Hcl_exec_expr_rhs)
2747                 * #cm_rhs_val generalize in match (proj2 ???);
2748                 #Hexpr_vars_rhs * #Heval_expr_rhs #Hvalue_eq_rhs >Heval_expr_rhs
2749                 normalize nodelta -Hsim_expr
2750                 whd in match (shift_offset ???); >sign_ext_same_size
2751                 >commutative_addition_n >addition_n_0
2752                 whd in Hstore_value_of_type:(??%?);
2753                 cases (store_value_of_type_success_by_value ? cl_m
2754                                    cl_mem_after_store ?? cl_rhs_result Hstore_value_of_type)
2755                 whd in match (typeof ?) in ⊢ ((??%%) → (??%?) → ?);
2756                 #Haccess_mode #Hstorev -Hstore_value_of_type
2757                 lapply (storen_parallel_aux ??? Hinjection … Hvalue_eq_rhs … Hembedding_to_stack ??? Hstorev)
2758                 * #cm_mem_after_store_lhs * #Hstoren #Hinj whd in Hstoren:(??%?);
2759                 >offset_plus_0 in Hstoren; #Hstorev'
2760                 whd in match (storev ????);
2761                 lapply Htype_eq whd in match (typeof ?) in ⊢ ((??%?) → ?); #Htype_eq'
2762                 <Htype_eq' >Hstorev'
2763                 whd in match (m_bind ?????); normalize nodelta
2764                 whd @conj try @conj try @refl
2765                 [ 2: #Habsurd destruct (Habsurd) ]                 
2766                 @(CMR_normal … Halloc_hyp) try assumption
2767                 try @refl
2768                 try @(memory_matching_preserved_by_parallel_stores … Hmatching)
2769                 try @(well_allocated_preserved_by_parallel_stores … Htmp_vars_well_allocated)
2770                 @(clight_cminor_cont_rel_parametric_in_mem … Hcont_rel)
2771               ]
2772          | 3: (* Local *)
2773               #Hlookup_var_success
2774               cases (typ_eq ??) normalize nodelta #Htyp_eq
2775               whd in ⊢ ((???%) → ?);
2776               #Heq destruct (Heq) normalize nodelta -Htranslate_statement
2777               #Htranslate
2778               cases (bind_inversion ????? Htranslate) -Htranslate
2779               * #cm_expr #Hexpr_vars * #Htyp_should_eq
2780               whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
2781               cases (typ_should_eq_inversion (typ_of_type (typeof rhs)) (typ_of_type lhs_ty) … Htyp_should_eq)
2782               -Htyp_should_eq #Htyp_eq lapply Hexpr_vars_rhs lapply Hexpr_vars
2783               -Hlabel_wf -Hreturn_ok -Hlabels_translated -Hstmt_inv_cm lapply sInv               
2784               lapply cm_expr -cm_expr <Htyp_eq #cm_expr #sInv #Hexpr_vars #Hexpr_vars'
2785               @(jmeq_absorb ?????) #Heq destruct (Heq)
2786               #s2 #tr whd in ⊢ ((??%?) → ?); #Hcl_exec
2787               cases (bindIO_inversion ??????? Hcl_exec)
2788               * * #cl_blo #cl_off #cl_trace *
2789               whd in ⊢ ((???%) → ?);
2790               #Hexec_lvalue lapply (res_to_io ????? Hexec_lvalue) -Hexec_lvalue
2791               whd in ⊢ ((??%?) → ?);
2792               @(match lookup ?? cl_env var_id
2793                 return λx. (lookup ?? cl_env var_id = x) → ?
2794                 with
2795                 [ None ⇒ λH. ?
2796                 | Some cl_addr ⇒ λH. ?
2797                 ] (refl ? (lookup ?? cl_env var_id)))
2798               normalize nodelta
2799               [ (* Contradiction: a register-allocated variable was necessarily in the environment *)
2800                 (* TODO, cf Hlookup_var_success or sInv *)
2801                 @cthulhu
2802               | #Heq destruct (Heq)
2803                 lapply (Hmatching var_id) >H normalize nodelta
2804                 >(opt_to_res_inversion ???? Hlookup_var_success) normalize nodelta
2805                 #Hpresent_in_local #Hexec_cl_rhs
2806                 cases (bindIO_inversion ??????? Hexec_cl_rhs) -Hexec_cl_rhs *
2807                 #cl_rhs_result #cl_rhs_trace * #Hcl_exec_expr_rhs #Hcl_exec_store
2808                 cases (bindIO_inversion ??????? Hcl_exec_store) -Hcl_exec_store #cl_mem_after_store
2809                 * #Hstore_value_of_type lapply (opt_to_io_Value ?????? Hstore_value_of_type)
2810                 -Hstore_value_of_type #Hstore_value_of_type
2811                 whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
2812                 %{1} whd whd in ⊢ (??%?); normalize nodelta
2813                 cases (eval_expr_sim … Halloc_hyp … Hcl_env_hyp … Hinjection … Hmatching) #Hsim_expr #_
2814                 lapply (Hsim_expr … Htranslate_rhs … (proj2 ?? (proj1 ?? (proj1 ?? sInv))) Hcl_exec_expr_rhs)
2815                 * #cm_rhs_val generalize in match (proj2 ???);
2816                 #Hexpr_vars_rhs * #Heval_expr_rhs #Hvalue_eq_rhs >Heval_expr_rhs
2817                 normalize nodelta -Hsim_expr whd @conj try @conj try @refl
2818                 [ 2: #Habsurd destruct (Habsurd) ]
2819                 generalize in match (proj1 ???); #Hpresent
2820                 generalize in match (conj ????); #Hstmt_vars
2821                 @(CMR_normal … Halloc_hyp) try assumption try @refl
2822                 [ 4: @(memory_matching_preserved_by_local_store … Hvalue_eq_rhs Hstore_value_of_type Hmatching)
2823                 | 3: @(memory_inj_preserved_by_local_store … Hmatching Hinjection)
2824                 | 2: @(tmp_vars_well_allocated_preserved_by_local_store … Hvalue_eq_rhs Hstore_value_of_type Htmp_vars_well_allocated)
2825                 | 1: @(clight_cminor_cont_rel_parametric_in_cm_env … Hpresent Hcont_rel) ]
2826               ]
2827          ]
2828     | 1: #Hnot_evar #Htranslate_statement
2829          cases (bind_inversion ????? Htranslate_statement) -Htranslate_statement
2830          * #cm_rhs #Hexpr_vars_rhs * #Htranslate_rhs #Htranslate_statement'
2831          cases (bind_inversion ????? Htranslate_statement') -Htranslate_statement' #dest
2832          lapply (translate_dest_not_Evar_id alloc_type ? lhs_ty Hnot_evar)
2833          #Htranslate_dest * #Htranslate_dest'
2834          >Htranslate_dest' in Htranslate_dest; #Haux lapply (sym_eq ??? Haux) -Haux #Haux
2835          cases (bind_inversion ????? Haux) -Haux
2836          * #translated_dest #Hexpr_vars_dest * #Htranslate_addr
2837          whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) normalize nodelta
2838          cases (type_eq_dec ??)
2839          [ 2: #Hneq normalize nodelta whd in ⊢ ((??%%) → ?);
2840               #Habsurd destruct (Habsurd) ]
2841          normalize nodelta whd in match (typeof ?); #Heq_cl_types
2842          whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
2843          #s2 #tr whd in ⊢ ((??%?) → ?); #Hstep
2844          cases (bindIO_inversion ??????? Hstep) -Hstep
2845          * * #cl_blo #cl_off #cl_tr * whd in ⊢ ((??%?) → ?);
2846          #Hexec_lvalue #Hstep
2847          lapply (translate_dest_MemDest_simulation …
2848                     INV' ???????? Halloc_hyp Hcl_env_hyp Hinjection Hmatching ??????
2849                     Htranslate_dest' Hexec_lvalue)
2850          [ 1: @(proj1 ?? (proj1 ?? (proj1 ?? sInv))) ]
2851          * #cm_val_dest * #Heval_cm_dest #Hvalue_eq_dest
2852          %{1} whd whd in ⊢ (??%?); normalize nodelta
2853          >Heval_cm_dest
2854          whd in match (m_bind ?????);
2855          cases (bindIO_inversion ??????? Hstep) -Hstep
2856          * #val #trace * #Hexec_expr #Hstep
2857          cases (bindIO_inversion ??????? Hstep) -Hstep
2858          #cl_mem_after_store * #Hopt_store
2859          whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
2860          lapply (opt_to_io_Value ?????? Hopt_store) -Hopt_store
2861          #Hstore_value_of_type whd in Hstore_value_of_type:(??%?);
2862          cases (eval_expr_sim … Halloc_hyp … Hcl_env_hyp … Hinjection … Hmatching) #Hsim_expr #_
2863          lapply (Hsim_expr … Htranslate_rhs … (proj2 ?? (proj1 ?? (proj1 ?? sInv))) Hexec_expr)
2864          * #cm_rhs_val generalize in match (proj2 ???);
2865          #Hexpr_vars_rhs * #Heval_expr_rhs #Hvalue_eq_rhs >Heval_expr_rhs
2866          normalize nodelta -Hsim_expr
2867          cases (store_value_of_type_success_by_value ? cl_m
2868                                    cl_mem_after_store ?? val Hstore_value_of_type)
2869          whd in match (typeof ?) in ⊢ ((??%%) → (??%?) → ?);
2870          #Haccess_mode #Hstorev -Hstore_value_of_type
2871          cases (value_eq_ptr_inversion … Hvalue_eq_dest) * #cm_blo #cm_off * #Hcm_val_dest destruct (Hcm_val_dest)
2872          whd in ⊢ ((??%?) → ?); #Hembed
2873          cases (some_inversion ????? Hembed) -Hembed
2874          * #cm_blo' #cm_off' * #Hembed normalize nodelta #Heq destruct (Heq)
2875          lapply (storen_parallel_aux ??? Hinjection … Hvalue_eq_rhs … Hembed ??? Hstorev)
2876          * #cm_mem_after_store_lhs * #Hstoren #Hinj whd in Hstoren:(??%?);
2877          whd in match (storev ????);
2878          lapply Hstoren
2879          (* make the types match *)
2880          generalize in match (conj ????); #Hstmt_vars' >Heq_cl_types
2881          #Hstoren >Hstoren
2882          whd in match (m_bind ?????); normalize nodelta whd @conj try @conj try @refl
2883          [ 2: #Habsurd destruct (Habsurd) ]
2884          @(CMR_normal … Halloc_hyp) try assumption try @refl
2885          [ 3: @(memory_matching_preserved_by_parallel_stores … Hmatching)
2886          | 2: @(well_allocated_preserved_by_parallel_stores … Htmp_vars_well_allocated)
2887          | 1: @(clight_cminor_cont_rel_parametric_in_mem … Hcont_rel) ]
2888     ]
2889| 4: (* Seq *)
2890     #cm_s #cl_k #cm_k #cm_st #cl_f #cm_f #rettyp
2891     #alloc_type #cl_env #cl_m #cm_env #cm_m #stackptr #stacksize
2892     (* introduce everything *)
2893     #fInv #sInv #kInv #Htarget_type #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function
2894     #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls
2895     #flag * * * * #Hstmt_inv_cm #Hlabels_translated #Htmps_preserved
2896     #Hreturn_ok #Hlabel_wf generalize in match (conj ????); #Hugly #Htranslate #Hlabel_inclusion
2897     #tmpenv #Htmpenv  #Hcont_rel
2898     #Em #Htmp_vars_well_allocated
2899     #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id #Hframe_spec #Henv_below
2900     @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
2901     destruct (HA HB)
2902     @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE #_
2903     destruct (HC HD HE)
2904     cases (bind_inversion ????? Htranslate) -Htranslate
2905     * * * #tmp_gen #labgen #cm_s1 #Htrans_inv * #Htrans_stm1 normalize nodelta
2906     #Htranslate cases (bind_inversion ????? Htranslate) -Htranslate     
2907     * * * #tmp_gen' #labgen' #cm_s2 #Htrans_inv' * #Htrans_stm2 normalize nodelta
2908     whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
2909     #s2 #tr whd in ⊢ ((??%?) → ?); #Heq destruct (Heq)
2910     %{1} whd @conj try @conj try @refl
2911     [ 2: #Habsurd destruct (Habsurd) ]
2912     @(CMR_normal … Htrans_stm1) try assumption
2913     [ 1: lapply Hlabel_inclusion
2914          @transitive_lset_inclusion @lset_inclusion_union %1
2915          @reflexive_lset_inclusion
2916     | 2: lapply (translation_entails_ident_inclusion … Htrans_stm2) #H
2917          @(transitive_lset_inclusion … (translation_entails_ident_inclusion … Htrans_stm2))
2918          assumption
2919     | 3: @(ClCm_cont_seq … Htrans_stm2)
2920          [ 1: lapply Hlabel_inclusion @transitive_lset_inclusion @lset_inclusion_union %2
2921               @reflexive_lset_inclusion
2922          | 2: assumption
2923          | 3: assumption ]
2924     ]
2925| *: (* Other statements *) @cthulhu ]
2926| 2: (* Return state *)
2927  #cl_ge #cm_ge #INV' #cl_k #cm_k #cm_st #cl_f #cm_f #alloc_type
2928  #cl_env #cl_m #cm_env #cm_mt #stackptr #stacksize
2929  #stmt_univ #tmpenv #Htmpenv #Em #Htmp_vars_wa #Hcharac #Hexec_alloc #Hinj #Hmatch #Hem_fn_id #Hframe #Hcont
2930  @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
2931  destruct (HA HB)
2932  @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
2933  destruct (HC HD HE)
2934  #_
2935  whd in Hclight_normal:%;
2936  @False_ind @Hclight_normal
2937| 3: (* Call state *)
2938  #cl_ge #cm_ge #INV' #cl_k #cm_k #cm_st #cl_f #cm_f #cl_fundef #cm_fundef
2939  #fblock #target_type #alloc_type #cl_env #cl_m #cm_env #cm_m #stackptr #stacksize
2940  #func_univ #Hgobals_fresh #Hfundef_fresh #Htranslate_function #Hfind_cl #Hfind_cm
2941  #cl_id #cm_id #stmt_univ #tmpenv #Htmpenv #Hcont_rel
2942  #Em #Htmp_vars_wa #Hcharac #Hexec_alloc #Hinj #Hmatch #Hem_fn_id #Hframe
2943  #cl_args_values #cm_args_values #Hall2
2944  @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
2945  destruct (HA HB)
2946  @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
2947  destruct (HC HD HE) #_
2948  whd in Hclight_normal:%;
2949  @False_ind @Hclight_normal
2950| 4: (* Intermediary While state *)
2951     (* ---------------------------------------------------------------------- *)
2952#cl_ge #cm_ge #INV'
2953#cl_f #cm_f #cl_env #cl_m #cm_env #cm_m #stackptr #stacksize #alloc_type
2954#cl_k #cm_k #sz #sg #cl_cond_ty #cl_cond_desc #cl_body #entry_label #exit_label #cm_cond #cm_body
2955#cm_stack #rettyp #kInv #fInv #sInv #Heq_ty #Hrettyp_eq #func_univ #Hfresh_globals #Hfresh_function
2956#Htranslate_function #Hcont_rel
2957#stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbl_univ'' #tmpenv #Htmpenv #Hcont_rel
2958#Em #Htmp_vars_well_allocated
2959#Hcharacterise #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id #Hframe_spec #Henv_below
2960#Hexpr_vars #Htranslate_expr #Hentry_ex #Hexit_ex #Htranslate_inv #Hmk_labels #Htranslate_statement
2961#Hlabel_inclusion #Hlabel_exists #Hinv1 #Hinv2 #Hfind_label
2962@(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
2963destruct (HA HB)
2964@(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
2965destruct (HC HD HE) #_
2966#s2 #tr whd in ⊢ ((??%?) → ?); #Hstep
2967(* execute clight condition *)
2968cases (bindIO_inversion ??????? Hstep) -Hstep
2969* #cl_cond_val #cl_cond_trace * #Hcl_exec_cond #Hstep
2970cases (bindIO_inversion ??????? Hstep) -Hstep
2971#cl_cond_bool * #Hcl_bool_of_val whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
2972(* The numbers of steps to execute in Cminor depends on the outcome of the condition
2973   evaluation *)
2974cases cl_cond_bool in Hcl_bool_of_val;
2975[ (* cond = true: continue looping *)
2976  #Hcl_bool_of_val
2977  %{3} whd whd in ⊢ (??%?); normalize nodelta
2978  generalize in match (proj1 ???); #Hpresent_ifthenelse
2979  (* Exhibit simulation of condition evaluation *)
2980  lapply (eval_expr_sim … Hcharacterise … Hcl_env_hyp … Hinjection … Hmatching) * #Hsim #_
2981  (* The type of Hsim forces us to wrap cm_cond into a dummy cast. *)
2982  lapply (Hsim (Expr cl_cond_desc cl_cond_ty) (CMcast ?? cm_cond ?))
2983  [ >Heq_ty @refl ] -Hsim
2984  whd in match (typeof ?); #Hsim
2985  lapply (Hsim ??????)
2986  [ 2: <Heq_ty >CMcast_identity assumption
2987  | 1: assumption
2988  | 6: <Heq_ty >CMcast_identity assumption
2989  | 5: lapply Htranslate_expr lapply Hexpr_vars lapply cm_cond -cm_cond
2990       >Heq_ty #cm_cond #Hexpr_vars @(jmeq_absorb ?????) #Hsol @Hsol
2991  | *: ]
2992  * #cm_val_cond * #Hcm_eval_cond #Hvalue_eq -Hsim
2993  cut (eval_expr cm_ge (ASTint sz sg) cm_cond cm_env Hpresent_ifthenelse stackptr cm_m = OK ? 〈tr, cm_val_cond〉)
2994  [ lapply Hpresent_ifthenelse
2995    <(CMcast_identity (ASTint sz sg) cm_cond) #foo
2996    lapply Hcm_eval_cond whd in match (eq_ind_r ??????); normalize nodelta cases Heq_ty
2997    #H @H ]
2998  #Heval >Heval
2999  whd in match (m_bind ?????);
3000  >(eval_bool_of_val_to_Cminor … Hvalue_eq … Hcl_bool_of_val)
3001  normalize nodelta whd
3002  generalize in match (proj1 ???); #Hnoise'
3003  generalize in match (conj ????); #Hnoise'' @conj try @conj
3004  [ 3: #Habsurd destruct (Habsurd)
3005  | 1: normalize >append_nil @refl
3006  | 2: @(CMR_normal … Htranslate_function … Htranslate_statement) try assumption
3007       @(ClCm_cont_while … Htranslate_inv … Hmk_labels … Htranslate_statement) try assumption
3008  ]
3009| (* cond = false: stop looping *)
3010  #Hcl_bool_of_val
3011  %{4} whd whd in ⊢ (??%?); normalize nodelta
3012  generalize in match (proj1 ???); #Hpresent_ifthenelse
3013  (* Exhibit simulation of condition evaluation *)
3014  lapply (eval_expr_sim … Hcharacterise … Hcl_env_hyp … Hinjection … Hmatching) * #Hsim #_
3015  lapply (Hsim (Expr cl_cond_desc cl_cond_ty) (CMcast ?? cm_cond ?))
3016  [ >Heq_ty @refl ] -Hsim
3017  whd in match (typeof ?); #Hsim
3018  lapply (Hsim ??????)
3019  [ 2: <Heq_ty >CMcast_identity assumption
3020  | 1: assumption
3021  | 6: <Heq_ty >CMcast_identity assumption
3022  | 5: lapply Htranslate_expr lapply Hexpr_vars lapply cm_cond -cm_cond
3023       >Heq_ty #cm_cond #Hexpr_vars @(jmeq_absorb ?????) #Hsol @Hsol
3024  | *: ]
3025  * #cm_val_cond * #Hcm_eval_cond #Hvalue_eq -Hsim
3026  cut (eval_expr cm_ge (ASTint sz sg) cm_cond cm_env Hpresent_ifthenelse stackptr cm_m = OK ? 〈tr, cm_val_cond〉)
3027  [ lapply Hpresent_ifthenelse
3028    <(CMcast_identity (ASTint sz sg) cm_cond) #foo
3029    lapply Hcm_eval_cond whd in match (eq_ind_r ??????); normalize nodelta cases Heq_ty
3030    #H @H ]
3031  #Heval >Heval
3032  whd in match (m_bind ?????);
3033  >(eval_bool_of_val_to_Cminor … Hvalue_eq … Hcl_bool_of_val)
3034  normalize nodelta whd
3035  generalize in match (proj1 ???); #Hnoise'
3036  generalize in match (proj2 ???); #Hnoise''
3037  generalize in match (conj ????); #Hnoise'''
3038  whd @conj try @conj
3039  [ 3: #Habsurd destruct (Habsurd)
3040  | 1: normalize >append_nil >append_nil @refl
3041  | 2: @(CMR_normal … DoNotConvert) try assumption
3042       try @refl
3043       @(env_below_freshgen_preserved_by_translation … Htranslate_statement)
3044       assumption
3045  ]
3046]
3047
3048] qed.
3049
3050 
3051(* TODO: move to globalenvs *)
3052lemma find_funct_match:
3053    ∀M:matching.∀initV,initW.
3054    ∀p: program (m_A M) (m_V M). ∀p': program (m_B M) (m_W M).
3055    ∀MATCH:match_program … M p p'.
3056    ∀v. ∀f: m_A M (prog_var_names … p).
3057    find_funct … (globalenv … initV p) v = Some ? f →
3058    ∃tf : m_B M (prog_var_names … p').
3059    find_funct … (globalenv … initW p') v = Some ? tf ∧ match_fundef M ? f (tf⌈m_B M ? ↦ m_B M (prog_var_names … p)⌉).
3060[ 2: >(matching_vars … (mp_vars … MATCH)) % ]
3061#M #initV #initW #p #p' #MP * [ | #sz #i | | #p ] #f
3062[ 1,2,3: #FF whd in FF:(??%?); destruct ]
3063whd in ⊢ (??%? → ?); @eq_offset_elim #OFF #FFP
3064[2: whd in FFP:(??%?); destruct ]
3065cases (find_funct_ptr_match M initV initW … MP (pblock p) f FFP)
3066#f' * #FFP' #MF %{f'} %
3067[ whd in ⊢ (??%?); >OFF >reflexive_eq_offset @FFP'
3068| @MF
3069] qed.
3070
3071lemma clight_cminor_inv_exists : ∀p,p'.
3072  clight_to_cminor p = OK … p' →
3073  clight_cminor_inv (make_global … clight_fullexec p) (make_global … Cminor_fullexec p').
3074#p #p' #COMPILE
3075lapply (clight_to_cminor_matches … COMPILE) #MATCHES -COMPILE
3076%
3077[2: #sym lapply (find_symbol_match (clight_cminor_matching p) ????? MATCHES)
3078    [4: #H @sym_eq @H | #X #Y * #id #r #v1 #v2 * % | skip | skip ]
3079|3: #v #f #FF cases (find_funct_match … MATCHES … FF)
3080  [ #f' * #FF' whd in ⊢ (% → ?); * #H1 * #H2 #Efd
3081    % [2: %{f'} %{H1} %{H2} % [ >Efd
3082    -Efd -H1 -H2 -FF' -FF
3083    generalize in ⊢ (??(??(match % with [_⇒?]))?);
3084    >(matching_vars … (mp_vars … MATCHES)) -MATCHES
3085    #E @(streicherK ???? E) %
3086    | @FF'
3087    ]
3088   | skip
3089   ]
3090  | skip
3091  ]
3092| skip
3093] qed.
3094
3095
3096lemma init_clight_cminor : ∀p,p',s.
3097  make_initial_state … clight_fullexec p = OK … s →
3098  clight_to_cminor p = OK … p' →
3099  ∃INV:clight_cminor_inv (make_global … clight_fullexec p) (make_global … Cminor_fullexec p').
3100  ∃s'.
3101    make_initial_state … Cminor_fullexec p' = OK … s' ∧
3102    clight_cminor_rel (make_global … clight_fullexec p) (make_global … Cminor_fullexec p') INV s s'.
3103#p #p' #s #INIT #COMPILE
3104lapply (clight_to_cminor_matches … COMPILE) #MATCHES
3105
3106%{(clight_cminor_inv_exists … COMPILE)}
3107
3108lapply (find_funct_ptr_match (clight_cminor_matching p) (fst ??) (λx.x) … MATCHES)
3109lapply (find_symbol_match (clight_cminor_matching p) (fst ??) (λx.x) … MATCHES)
3110[ #v #w * // ]
3111lapply (init_mem_match (clight_cminor_matching p) (fst ??) (λx.x) … MATCHES)
3112[ #v #w * // ]
3113cases p in INIT COMPILE MATCHES ⊢ %; #vars #fns #main #INIT #COMPILE #MATCHES
3114cases (bind_inversion ????? INIT) -INIT #m * #INITMEM #INIT
3115cases (bind_inversion ????? INIT) -INIT #b * #FINDSYM #INIT
3116cases (bind_inversion ????? INIT) -INIT #fd * #FFP #INIT
3117whd in INIT:(??%%); destruct
3118whd in match (m_A ??); whd in match (m_B ??); whd in match (m_V ?); whd in match (m_W ?);
3119#M_initmem #M_findsym #M_ffp
3120cases (M_ffp … FFP) -M_ffp #f' * #FFP' #Mf'
3121%{(Callstate main f' [ ] m SStop)} %
3122[ whd in ⊢ (??%?); normalize in M_initmem:(??(?%%%?)(?%%%?)); >M_initmem >INITMEM
3123  whd in ⊢ (??%?); lapply (M_findsym main) <(mp_main … MATCHES)
3124  whd in match (m_A ??); whd in match (m_B ??);
3125  change with (make_global p') in match (globalenv ????); #E >E
3126  >FINDSYM
3127  whd in ⊢ (??%?); >FFP'
3128  whd in ⊢ (??%?); %
3129| (* Axiomatised - we don't have the simulation step out of Callstate yet anyway. *)
3130  cases daemon
3131] qed.
3132
Note: See TracBrowser for help on using the repository browser.