source: src/Clight/toCminorCorrectness.ma @ 3367

Last change on this file since 3367 was 3237, checked in by campbell, 7 years ago

Some incomplete work on Clight -> Cminor call steps.

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