source: src/Clight/toCminorCorrectness.ma @ 2896

Last change on this file since 2896 was 2857, checked in by garnier, 7 years ago

CL to CM: some invariants strengthened.

File size: 113.7 KB
Line 
1include "Clight/toCminor.ma".
2include "Clight/CexecInd.ma".
3include "common/Globalenvs.ma".
4include "Clight/memoryInjections.ma".
5include "Clight/Clight_abstract.ma".
6include "Cminor/Cminor_abstract.ma".
7include "common/Measurable.ma".
8
9(* Expr simulation. Contains important definitions for statements, too.  *)
10include "Clight/toCminorCorrectnessExpr.ma".
11
12(* When we characterise the local Clight variables, those that are stack
13   allocated are given disjoint regions of the stack. *)
14lemma characterise_vars_disjoint : ∀globals,f,vartypes,stacksize,id,n,ty.
15  characterise_vars globals f = 〈vartypes, stacksize〉 →
16  lookup ?? vartypes id = Some ? 〈Stack n,ty〉 →
17  ∀id',n',ty'. id ≠ id' →
18  lookup ?? vartypes id' = Some ? 〈Stack n',ty'〉 →
19  n' + sizeof ty' ≤ n ∨ n + sizeof ty ≤ n'.
20#globals * #ret #args #vars #body #vartypes #stacksize #id #n #ty
21whd in ⊢ (??%? → ?);
22generalize in match vartypes; -vartypes
23generalize in match stacksize; -stacksize
24elim (args@vars)
25[ #stacksize #vartypes #CHAR #L @⊥ whd in CHAR:(??%?); destruct
26  elim globals in L;
27  [ normalize #L destruct
28  | * * #id' #r #ty' #tl #IH
29    whd in match (foldr ?????);
30    #L cases (lookup_add_cases ??????? L)
31    [ * #E1 #E2 destruct
32    | @IH
33    ]
34  ]
35| * #id1 #ty1 #tl #IH #stacksize #vartypes
36  whd in match (foldr ?????);
37  (* Avoid writing out the definition again *)
38  letin ih ≝ (foldr ? (Prod ??) ?? tl) in IH ⊢ %;
39  lapply (refl ? ih) whd in match ih; -ih
40  cases (foldr ? (Prod ??) ?? tl) in ⊢ (???% → %);
41  #vartypes' #stack' #FOLD #IH
42  whd in ⊢ (??(match % with [_⇒?])? → ?);
43  cases (orb ??)
44  #CHAR whd in CHAR:(??%?); destruct
45  #L cases (lookup_add_cases ??????? L)
46  [ 1,3: * #E1 #E2 destruct
47    #id' #n' #ty' #NE >lookup_add_miss /2/
48    #L' %1 -L -IH
49    generalize in match vartypes' in FOLD L' ⊢ %; -vartypes'
50    generalize in match stack'; -stack'
51    elim tl
52    [ #stack' #vartypes2 whd in ⊢ (??%? → ?); #F destruct #L' @⊥
53      elim globals in L';
54      [ normalize #E destruct
55      | * * #id2 #r2 #ty2 #tl2 #IH whd in match (foldr ?????);
56        #L cases (lookup_add_cases ??????? L)
57        [ * #E1 #E2 destruct
58        | @IH
59        ]
60      ]
61    | * #id2 #ty2 #tl2 #IH #stack' #vartypes'
62      whd in ⊢ (??%? → ?); cases (foldr ? (Prod ??) ???) in IH ⊢ %;
63      #vartypes2 #stack2 #IH
64      whd in ⊢ (??%? → ?);
65      cases (orb ??)
66      [ #E whd in E:(??%?); destruct #L cases (lookup_add_cases ??????? L)
67        [ * #E1 #E2 destruct //
68        | #L'' lapply (IH ?? (refl ??) L'') /2/
69        ]
70      | #E whd in E:(??%?); destruct #L cases (lookup_add_cases ??????? L)
71        [ * #E1 #E2 destruct
72        | #L'' lapply (IH ?? (refl ??) L'') /2/
73        ]
74      ]
75    ]
76  | -L #L #id' #n' #ty' #NE #L'
77    cases (lookup_add_cases ??????? L')
78    [ * #E1 #E2 destruct
79      %2 -IH -L'
80      generalize in match vartypes' in FOLD L; -vartypes'
81      generalize in match stack'; -stack'
82      elim tl
83      [ #stack' #vartypes' whd in ⊢ (??%? → ?); #F destruct #L @⊥
84        elim globals in L;
85        [ normalize #E destruct
86        | * * #id1 #r1 #ty1 #tl1 #IH whd in match (foldr ?????);
87          #L cases (lookup_add_cases ??????? L)
88          [ * #E1 #E2 destruct
89          | @IH
90          ]
91        ]
92      | * #id1 #ty1 #tl1 #IH #stack' #vartypes'
93        whd in ⊢ (??%? → ?); cases (foldr ? (Prod ??) ???) in IH ⊢ %;
94        #vartypes2 #stack2 #IH
95        whd in ⊢ (??%? → ?);
96        cases (orb ??)
97        #E whd in E:(??%?); destruct
98        #L cases (lookup_add_cases ??????? L)
99        [ 1,3: * #E1 #E2 destruct //
100        | 2,4: #L' lapply (IH ?? (refl ??) L') /2/
101        ]
102      ]
103    | @(IH … (refl ??) L … NE)
104    ]
105  | -L #L #id' #n' #ty' #NE #L'
106    cases (lookup_add_cases ??????? L')
107    [ * #E1 #E2 destruct
108    | @(IH … (refl ??) L … NE)
109    ]
110  ]
111] qed.
112
113(* And everything is in the stack frame. *)
114
115lemma characterise_vars_in_range : ∀globals,f,vartypes,stacksize,id,n,ty.
116  characterise_vars globals f = 〈vartypes, stacksize〉 →
117  lookup ?? vartypes id = Some ? 〈Stack n,ty〉 →
118  n + sizeof ty ≤ stacksize.
119#globals * #ret #args #vars #body whd in match (characterise_vars ??);
120elim (args@vars)
121[ #vartypes #stacksize #id #n #ty #FOLD #L @⊥
122  whd in FOLD:(??%?); destruct elim globals in L;
123  [ #E normalize in E; destruct
124  | * * #id' #r' #ty' #tl' #IH
125    whd in match (foldr ?????); #L cases (lookup_add_cases ??????? L)
126    [ * #E1 #E2 destruct
127    | @IH
128    ]
129  ]
130| * #id' #ty' #tl #IH #vartypes #stacksize #id #n #ty
131  whd in match (foldr ?????); cases (foldr ? (Prod ??) ???) in IH ⊢ %;
132  #vartypes' #stackspace' #IH
133  whd in ⊢ (??(match % with [_⇒?])? → ?);
134  cases (orb ??) whd in ⊢ (??%? → ?);
135  #E destruct #L cases (lookup_add_cases ??????? L)
136  [ 1,3: * #E1 #E2 destruct //
137  | 2,4: #L' lapply (IH … (refl ??) L') /2/
138  ]
139] qed.
140
141
142
143(* Put knowledge that Globals are global into a more useful form than the
144   one used for the invariant. *)   
145(* XXX superfluous lemma ? Commenting it for now.
146       if not superfluous : move to toCminorCorrectnessExpr.ma, after
147       [characterise_vars_localid] *)
148(*
149lemma characterise_vars_global : ∀globals,f,vartypes,stacksize.
150  characterise_vars globals f = 〈vartypes, stacksize〉 →
151  ∀id,r,ty. lookup' vartypes id = OK ? 〈Global r,ty〉 →
152  Exists ? (λx.x = 〈〈id,r〉,ty〉) globals ∧
153  ¬ Exists ? (λx. \fst x = id) (fn_params f @ fn_vars f).
154#globals #f #vartypes #stacksize #CHAR #id #r #ty #L
155cases (characterise_vars_src … CHAR id ?)
156[ * #r' * #ty' >L
157  * #E1 destruct (E1) #EX
158  %
159  [ @EX
160  | % #EX' cases (characterise_vars_localid … CHAR EX')
161    #ty' whd in ⊢ (% → ?); >L *
162  ]
163| * #ty' whd in ⊢ (% → ?); >L *
164| whd >(opt_eq_from_res ???? L) % #E destruct
165] qed. *)
166
167(* Show how the global environments match up. *)
168
169lemma map_partial_All_to_All2 : ∀A,B,P,f,l,H,l'.
170  map_partial_All A B P f l H = OK ? l' →
171  All2 ?? (λa,b. ∃p. f a p = OK ? b) l l'.
172#A #B #P #f #l
173elim l
174[ #H #l' #MAP normalize in MAP; destruct //
175| #h #t #IH * #p #H #l'
176  whd in ⊢ (??%? → ?);
177  lapply (refl ? (f h p)) whd in match (proj1 ???);
178  cases (f h p) in ⊢ (???% → %);
179  [ #b #E #MAP cases (bind_inversion ????? MAP)
180    #tl' * #MAP' #E' normalize in E'; destruct
181    % [ %{p} @E | @IH [ @H | @MAP' ] ]
182  | #m #_ #X normalize in X; destruct
183  ]
184] qed.
185 
186
187definition clight_cminor_matching : clight_program → matching ≝
188λp.
189  let tmpuniverse ≝ universe_for_program p in
190  let fun_globals ≝ map ?? (λidf. 〈\fst idf,Code,type_of_fundef (\snd idf)〉) (prog_funct ?? p) in
191  let var_globals ≝ map ?? (λv. 〈\fst (\fst v), \snd (\fst v), \snd (\snd v)〉) (prog_vars ?? p) in
192  let globals ≝ fun_globals @ var_globals in
193  mk_matching
194    ?? (list init_data × type) (list init_data)
195    (λvs,f_clight,f_cminor. ∃H1,H2. translate_fundef tmpuniverse globals H1 f_clight H2 = OK ? f_cminor)
196    (λv,w. \fst v = w).
197
198lemma clight_to_cminor_varnames : ∀p,p'.
199  clight_to_cminor p = OK ? p' →
200  prog_var_names … p = prog_var_names … p'.
201* #vars #fns #main * #vars' #fns' #main'
202#TO cases (bind_inversion ????? TO) #fns'' * #MAP #E
203whd in E:(??%%); destruct
204-MAP normalize
205elim vars
206[ //
207| * * #id #r * #d #t #tl #IH normalize >IH //
208] qed.
209
210lemma clight_to_cminor_matches : ∀p,p'.
211  clight_to_cminor p = OK ? p' →
212  match_program (clight_cminor_matching p) p p'.
213* #vars #fns #main * #vars' #fns' #main'
214#TO cases (bind_inversion ????? TO) #fns'' * #MAP #E
215whd in E:(??%%); destruct
216%
217[ -MAP whd in match (m_V ?); whd in match (m_W ?);
218  elim vars
219  [ //
220  | * * #id #r * #init #ty #tl #IH %
221    [ % //
222    | @(All2_mp … IH) * * #a #b * #c #d * * #e #f #g * /2/
223    ]
224  ]
225| @(All2_mp … (map_partial_All_to_All2 … MAP)) -MAP
226  * #id #f * #id' #f' * #H #F cases (bind_inversion ????? F) #f'' * #TRANSF #E
227  normalize in E; destruct
228  <(clight_to_cminor_varnames … TO)
229  % whd
230  % [2: % [2: @TRANSF | skip ] | skip ]
231| %
232] qed.
233
234(* --------------------------------------------------------------------------- *)
235(* Clight to Cminor makes use of fresh symbol generators, which store the list
236 * of symbols they generate. We need to maintain as an invariant that these grow
237 * in a monotonic and consistent fashion. *)
238(* --------------------------------------------------------------------------- *)
239
240(* The two following definitions and two lemmas are duplicated from switchRemoval.ma.
241 * TODO: factorise this in frontend_misc, if they turn out not to be useless *)
242definition fresher_than_or_equal : universe SymbolTag → universe SymbolTag → Prop ≝
243λu1,u2.
244  match u1 with
245  [ mk_universe p1 ⇒
246    match u2 with
247    [ mk_universe p2 ⇒ p2 ≤ p1 ] ].
248   
249definition fte ≝ fresher_than_or_equal.
250
251lemma transitive_fte : ∀u1,u2,u3. fte u1 u2 → fte u2 u3 → fte u1 u3.
252* #u1 * #u2 * #u3 normalize /2 by transitive_le/
253qed.
254
255lemma reflexive_fte : ∀u. fte u u.
256* // qed.
257
258definition labgen_include ≝
259  λgen1, gen2 : labgen.
260  ∃labels. label_genlist gen2 = labels @ label_genlist gen1.
261 
262definition tmpgen_include ≝
263  λvartypes.
264  λgen1, gen2 : tmpgen vartypes.
265  ∃idents. tmp_env ? gen2 = idents @ (tmp_env ? gen1).
266
267(* --------------------------------------------------------------------------- *)
268(* Additional invariants not contain in clight_cminor_data *)
269(* --------------------------------------------------------------------------- *)
270
271(* Fresh variable ident generator *)
272(* tmp_gen     : tmpgen alloc_type; *)
273
274(* Temporary variables generated during conversion are well-allocated. *)
275definition tmp_vars_well_allocated ≝
276   λvartypes.
277   λtmp_gen: tmpgen vartypes.
278   λcm_env.
279   λcm_m.
280   λcl_m.
281   λE: embedding.
282   ∀local_variable.
283   ∀H:present ?? cm_env local_variable.
284   ∀ty. Exists ? (λx. x = 〈local_variable, ty〉) (tmp_env … tmp_gen) →
285   ∀v. val_typ v (typ_of_type ty) →
286   ∃cm_m'. storev (typ_of_type ty) cm_m (lookup_present ?? cm_env local_variable H) v = Some ? cm_m' ∧
287           memory_inj E cl_m cm_m'.
288
289(* wrap the above invariant into a clight_cminor_data-eating prop *)
290(*
291definition tmp_vars_well_allocated' ≝
292   λcl_f, cl_ge, cm_ge, INV.
293   λframe_data: clight_cminor_data cl_f cl_ge cm_ge INV.
294   λtmp_gen: tmpgen (alloc_type … frame_data).
295   ∀vars_v, cl_m_v, cm_env_v, cm_m_v.
296   vars_v   = alloc_type … frame_data →
297   cl_m_v   = cl_m … frame_data →
298   cm_env_v = cm_env … frame_data →
299   cm_m_v   = cm_m … frame_data →   
300   ∀local_variable.
301   ∀H:present ?? cm_env_v local_variable.
302   ∀ty. Exists ? (λx. x = 〈local_variable, ty〉) (tmp_env … tmp_gen) →
303   ∀v. val_typ v (typ_of_type ty) →
304   ∃cm_m'. storev (typ_of_type ty) cm_m_v (lookup_present ?? cm_env_v local_variable H) v = Some ? cm_m' ∧
305           memory_inj (Em … frame_data) cl_m_v cm_m'. *)
306
307(* --------------------------------------------------------------------------- *)           
308(* A measure on Clight states that is decreasing along execution sequences     *)
309(* --------------------------------------------------------------------------- *)
310
311(* statements *)
312let rec measure_Clight_statement (s : statement) : ℕ ≝
313match s with
314[ Sskip ⇒ 0
315| Ssequence s1 s2 ⇒
316  measure_Clight_statement s1 + measure_Clight_statement s2 + 1
317| Sifthenelse e s1 s2 =>
318  measure_Clight_statement s1 + measure_Clight_statement s2 + 1
319| Swhile e s =>
320  measure_Clight_statement s + 1
321| Sdowhile e s =>
322  measure_Clight_statement s + 1
323| Sfor s1 e s2 s3 =>
324  measure_Clight_statement s1 +
325  measure_Clight_statement s2 +
326  measure_Clight_statement s3 + 1
327| Sswitch e ls =>
328  measure_Clight_ls ls + 1
329| Slabel l s =>
330  measure_Clight_statement s + 1
331| Scost cl s =>
332  measure_Clight_statement s + 1
333| _ => 1
334]
335and measure_Clight_ls (ls : labeled_statements) : ℕ :=
336match ls with
337[ LSdefault s =>
338  measure_Clight_statement s
339| LScase sz i s ls =>
340  measure_Clight_statement s +
341  measure_Clight_ls ls
342].
343
344(* continuations *)
345let rec measure_Clight_cont (cont : cl_cont) : ℕ ≝
346match cont with
347[ Kstop => 0
348| Kseq s k =>
349  measure_Clight_statement s +
350  measure_Clight_cont k + 1
351| Kwhile e s k =>
352  measure_Clight_statement s +
353  measure_Clight_cont k + 1
354| Kdowhile e s k =>
355  measure_Clight_statement s +
356  measure_Clight_cont k + 1
357| Kfor2 e s1 s2 k =>
358  measure_Clight_statement s1 +
359  measure_Clight_statement s2 +
360  measure_Clight_cont k + 1
361| Kfor3 e s1 s2 k =>
362  measure_Clight_statement s1 +
363  measure_Clight_statement s2 +
364  measure_Clight_cont k + 1
365| Kswitch k =>
366  measure_Clight_cont k + 1
367| Kcall retaddr f e k =>
368  measure_Clight_statement (fn_body f) +
369  measure_Clight_cont k + 1
370].
371
372(* Shamelessly copying Compcert. *)
373definition measure_Clight : Clight_state → ℕ × ℕ ≝
374λstate.
375match state with
376[ State f s k e m ⇒
377  〈measure_Clight_statement s + measure_Clight_cont k + 1, measure_Clight_statement s + 1〉
378| Callstate fb fd args k m ⇒ 〈0, 0〉
379| Returnstate res k m ⇒ 〈0, 0〉
380| Finalstate r ⇒ 〈0, 0〉
381].
382
383(* Stuff on lexicographic orders *)
384definition lexicographic : ∀A:Type[0]. (A → A → Prop) → A × A → A × A → Prop ≝
385λA,Ord, x, y.
386  let 〈xa, xb〉 ≝ x in
387  let 〈ya, yb〉 ≝ y in
388  Ord xa ya ∨ (xa = ya ∧ Ord xb yb).
389
390definition lex_lt ≝ lexicographic nat lt.
391
392(* --------------------------------------------------------------------------- *)
393(* Simulation relations *)
394(* --------------------------------------------------------------------------- *)
395
396record frame_data
397  (f : function)
398  (ge_cl : genv_t clight_fundef)
399  (ge_cm : genv_t (fundef internal_function))
400  (INV : clight_cminor_inv ge_cl ge_cm) : Type[0] ≝
401{
402}.
403
404definition CMcast : ∀t,t'. CMexpr t → t = t' → CMexpr t'.
405#t #t' #e #H destruct (H) @e
406qed.
407
408lemma CMcast_identity : ∀t. ∀e: CMexpr t. CMcast t t e (refl ??) = e.
409#H1 #H2 @refl qed.
410
411(* relate Clight continuations and Cminor ones. *)
412inductive clight_cminor_cont_rel :
413  ∀cl_ge, cm_ge.
414  ∀INV:  clight_cminor_inv cl_ge cm_ge.     (* stuff on global variables and functions (matching between CL and CM) *)
415  ∀cl_f: function.                          (* current Clight function *)
416  internal_function →                       (* current Cminor function *)
417  cl_env →
418  cm_env →
419  var_types →
420  (*frame_data cl_f cl_ge cm_ge INV →*)         (* data for the current stack frame in CL and CM *)
421  option typ →                              (* optional target type - uniform over a given function *)
422  cl_cont →                                 (* CL cont *)
423  cm_cont →                                 (* CM cont *)
424  stack →                                   (* CM stack *) 
425  Prop ≝
426(* Stop continuation*) 
427| ClCm_cont_stop:
428  ∀cl_ge, cm_ge, INV, cl_f, cm_f, target_type.
429  ∀cl_env, cm_env, alloc_type.
430  ∀cm_stack.
431  cm_stack = SStop →
432  clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type target_type Kstop Kend cm_stack
433
434(* Seq continuation *)
435| ClCm_cont_seq:
436  ∀cl_ge, cm_ge, INV, cl_f, cm_f, target_type.
437  ∀stack.
438  ∀alloc_type.
439  ∀cl_s: statement.
440  ∀cm_s: stmt.
441  ∀cl_env: cl_env.
442  ∀cm_env: cm_env.
443  ∀cl_k': cl_cont.
444  ∀cm_k': cm_cont.
445  ∀stmt_univ, stmt_univ'.
446  ∀lbl_univ, lbl_univ'.
447  ∀lbls.
448  ∀flag.
449  ∀Htranslate_inv.
450  translate_statement alloc_type stmt_univ lbl_univ lbls flag target_type cl_s = OK ? «〈stmt_univ',lbl_univ',cm_s〉, Htranslate_inv» →
451  (* ---- invariant on label existence ---- *)
452  lset_inclusion ? (labels_of cm_s) (labels_of (f_body cm_f)) →
453  clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type target_type cl_k' cm_k' stack →
454  clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type target_type (ClKseq cl_s cl_k') (Kseq cm_s cm_k') stack
455
456(* While continuation *) 
457| ClCm_cont_while:
458  (* Inductive family parameters *)
459  ∀cl_ge, cm_ge, INV, cl_f, cm_f, target_type.
460  ∀stack.
461  ∀alloc_type.
462  ∀cl_env.
463  ∀cm_env.
464
465  (* sub-continuations *)
466  ∀cl_k': cl_cont.
467  ∀cm_k': cm_cont.
468
469  (* elements of the source while statement *)
470  ∀sz,sg.
471  ∀cl_ty.
472  ∀cl_cond_desc.
473  ∀cl_body.
474  ∀Heq: ASTint sz sg = typ_of_type cl_ty.
475
476  (* elements of the converted while statement *)
477  ∀cm_cond: CMexpr (ASTint sz sg).
478  ∀cm_body.
479  ∀entry,exit: identifier Label.
480 
481  (* universes used to generate fresh labels and variables *) 
482  ∀stmt_univ, stmt_univ'.
483  ∀lbl_univ, lbl_univ', lbl_univ''.
484  ∀lbls: lenv.
485  ∀Htranslate_inv.
486
487  (* relate CL and CM expressions *)
488  ∀Hexpr_vars.
489  translate_expr alloc_type (Expr cl_cond_desc cl_ty) = OK ? («CMcast ?? cm_cond Heq, Hexpr_vars») →
490
491  (* Parameters and results to find_label_always *)
492  ∀sInv: stmt_inv cm_f cm_env (f_body cm_f).
493  ∀Hlabel_declared: Exists (identifier Label) (λl'.l'=entry) (labels_of (f_body cm_f)).
494  ∀Hinv.
495
496  (* Specify how the labels for the while-replacing gotos are produced *)
497  mklabels lbl_univ = 〈〈entry, exit〉, lbl_univ'〉 →
498  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» →
499  (* Invariant on label existence *)
500  lset_inclusion ? (labels_of cm_body) (labels_of (f_body cm_f)) → 
501  find_label_always entry (f_body cm_f) Kend Hlabel_declared cm_f cm_env sInv I =
502    «〈(*St_label entry*)
503          (St_seq
504            (St_ifthenelse ?? cm_cond (St_seq cm_body (St_goto entry)) St_skip)
505            (St_label exit St_skip)), cm_k'〉, Hinv» →
506  clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type target_type cl_k' cm_k' stack →
507  clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type target_type (
508    Kwhile (Expr cl_cond_desc cl_ty) cl_body cl_k')
509    (Kseq (St_goto entry) (Kseq (St_label exit St_skip) cm_k')) stack.
510(* TODO: Kcall *)
511
512(* TODO XXX *)
513(* relation between placeholders for return values *)
514
515definition return_value_rel :
516  ∀cl_f, cl_ge, cm_ge.
517  ∀INV: clight_cminor_inv cl_ge cm_ge.
518  frame_data cl_f ?? INV →
519  option (block×offset×type) → option (ident×typ) → Prop ≝
520λcl_f, cl_ge, cm_ge, INV, data, opt1, opt2.
521match opt1 with
522[ None ⇒
523  match opt2 with
524  [ None ⇒ True
525  | _ ⇒ False ]
526| Some ptr ⇒
527  match opt2 with
528  [ Some id ⇒ True (* TODO, here. *)
529  | None ⇒ False
530  ]
531].
532
533(* Definition of the simulation relation on states. The orders of the parameters is dictated by
534 * the necessity of performing an inversion on the continuation sim relation without having to
535 * play the usual game of lapplying all previous dependent arguments.  *)
536inductive clight_cminor_rel : ∀cl_ge, cm_ge. clight_cminor_inv cl_ge cm_ge  → Clight_state → Cminor_state → Prop ≝
537| CMR_normal :
538  (* Clight and Cminor global envs *)
539  ∀cl_ge, cm_ge.
540  (* Relates globals to globals and functions to functions. *)
541  ∀INV:  clight_cminor_inv cl_ge cm_ge. 
542  (* ---- Statements ---- *)
543  (* Clight statement *) 
544  ∀cl_s: statement.
545  (* Cminor statement *)
546  ∀cm_s: stmt.                                           
547  (* ---- Continuations ---- *)
548  (* Clight continuation *)
549  ∀cl_k: cl_cont.
550  (* Cminor continuation *) 
551  ∀cm_k: cm_cont.
552  (* Cminor stack *)
553  ∀cm_st: stack.
554  (* Clight enclosing function *)
555  ∀cl_f: function.
556  (* Cminor enclosing function *)
557  ∀cm_f: internal_function.
558  (* optional return type of the function *)
559  ∀rettyp.
560  (* mapping from variables to their Cminor alloc type *)                                 
561  ∀alloc_type.
562  (* Clight env/mem *)
563  ∀cl_env, cl_m.
564  (* Cminor env/mem *)
565  ∀cm_env, cm_m.
566  (* Stack pointer (block containing Cminor locals), related size *)
567  ∀stackptr, stacksize.
568  (* ---- Cminor invariants ---- *)
569  ∀fInv: stmt_inv cm_f cm_env (f_body cm_f).
570  ∀sInv: stmt_inv cm_f cm_env cm_s.
571  ∀kInv: cont_inv cm_f cm_env cm_k.
572  (* ---- relate return type variable to actual return type ---- *)
573  rettyp = opttyp_of_type (fn_return cl_f) →
574  (* ---- relate Clight and Cminor functions ---- *)
575  ∀func_univ: universe SymbolTag.
576  ∀Hfresh_globals: globals_fresh_for_univ ? (globals ?? INV) func_univ.
577  ∀Hfresh_function: fn_fresh_for_univ cl_f func_univ.
578  translate_function func_univ (globals ?? INV) cl_f Hfresh_globals Hfresh_function = OK ? cm_f →
579  (* ---- relate Clight and Cminor statements ---- *)
580  (* fresh var generators *)
581  ∀stmt_univ,stmt_univ' : tmpgen alloc_type.
582  (* fresh label generators *)
583  ∀lbl_univ,lbl_univ'   : labgen.
584  (* map old labels to new labels *)
585  ∀lbls                 : lenv.
586  (* specify where to goto when encountering a continue or a break *)
587  ∀flag                 : convert_flag.
588  (* Invariant on translation produced by [translate_statement] *)
589  ∀Htranslate_inv.
590  translate_statement alloc_type stmt_univ lbl_univ lbls flag rettyp cl_s = OK ? «〈stmt_univ',lbl_univ',cm_s〉, Htranslate_inv» →
591  (* ---- invariant on label existence ---- *)
592  lset_inclusion ? (labels_of cm_s) (labels_of (f_body cm_f)) →
593  (* ---- relate Clight continuation to Cminor continuation ---- *)
594  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_st →
595  (* ---- state invariants for memory and environments ---- *)
596  (* Embedding *)
597  ∀Em: embedding.
598  (* locals are properly allocated *)
599  tmp_vars_well_allocated alloc_type stmt_univ' cm_env cm_m cl_m Em →
600  (* specify how alloc_type is built *)
601  characterise_vars (globals ?? INV) cl_f = 〈alloc_type, stacksize〉 →
602  (* spec. Clight env at alloc time *)
603  (∃m,m'. exec_alloc_variables empty_env m (fn_params cl_f @ fn_vars cl_f) = 〈cl_env,m'〉) →
604  (* memory injection *)
605  memory_inj Em cl_m cm_m →
606  (* map CL env to CM env *)
607  memory_matching Em cl_ge cm_ge cl_m cm_m cl_env cm_env INV stackptr alloc_type →
608  (* Force embedding to compute identity on functions *)
609  (∀b. block_region b = Code → Em b = Some ? 〈b, zero_offset〉) →
610  (* Make explicit the fact that locals in CL are mapped to a single CM block *)
611  (∀b1.∀delta. Em b1=Some ? 〈stackptr,delta〉 →
612               mem block b1 (blocks_of_env cl_env)) →
613  clight_cminor_rel cl_ge cm_ge INV
614    (ClState cl_f cl_s cl_k cl_env cl_m)
615    (CmState cm_f cm_s cm_env fInv sInv cm_m stackptr cm_k kInv cm_st)
616
617| CMR_return :
618  ∀cl_ge, cm_ge.
619  ∀INV: clight_cminor_inv cl_ge cm_ge.
620  ∀cl_f: function.                               (* Clight enclosing function *)
621  ∀cm_f: internal_function.                             (* enclosing function *)
622  ∀alloc_type.
623  ∀cl_env, cl_m.
624  ∀cm_env, cm_m.
625  ∀cm_st: stack.                                              (* Cminor stack *)
626  ∀stackptr, stacksize.
627  ∀stmt_univ.
628  ∀Em: embedding.
629  tmp_vars_well_allocated alloc_type stmt_univ cm_env cm_m cl_m Em →        (* locals are properly allocated *)
630  characterise_vars (globals ?? INV) cl_f = 〈alloc_type, stacksize〉 →        (* specify how alloc_type is built *)
631  (∃m,m'. exec_alloc_variables empty_env m (fn_params cl_f @ fn_vars cl_f) = 〈cl_env,m'〉) → (* spec. Clight env *)
632  memory_inj Em cl_m cm_m →                                                  (* memory injection *)
633  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 *)             
634  (∀b. block_region b = Code → Em b = Some ? 〈b, zero_offset〉) →             (* Force embedding to compute identity on functions *)
635  (* Make explicit the fact that locals in CL are mapped to a single CM block *)
636  (∀b1.∀delta. Em b1=Some ? 〈stackptr,delta〉 →
637               mem block b1 (blocks_of_env cl_env)) → 
638  clight_cminor_rel cl_ge cm_ge INV
639    (ClReturnstate Vundef Kstop cl_m)
640    (CmReturnstate (None val) cm_m cm_st)
641
642| CMR_call_nostore :
643 (* call to a function with no return value, or which returns in a local variable in Cminor *)
644 ∀cl_ge, cm_ge, cl_f, cm_f.
645 ∀INV: clight_cminor_inv cl_ge cm_ge.
646 ∀alloc_type, cl_env, cl_m, cm_env, cm_m, cm_stack, stackptr.
647 (* TODO: put the actual invariants on memory and etc. here *)
648 ∀u: universe SymbolTag.
649 ∀cl_fundef, cm_fundef.
650 ∀Hglobals_fresh: globals_fresh_for_univ type (globals cl_ge cm_ge INV) u.
651 ∀Hfundef_fresh:  fd_fresh_for_univ cl_fundef u.
652 ∀rettyp. rettyp = opttyp_of_type (fn_return cl_f) →
653 ∀cl_k, cm_k.
654 ∀fblock.
655 match cl_fundef with
656 [ CL_Internal cl_function ⇒
657    find_funct clight_fundef cl_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? (CL_Internal cl_function) ∧
658    find_funct (fundef internal_function) cm_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? cm_fundef ∧
659    translate_fundef u (globals ?? INV) Hglobals_fresh cl_fundef Hfundef_fresh = OK ? cm_fundef ∧
660    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
661 | CL_External name argtypes rettype ⇒
662   True
663 ] →
664 ∀cl_fun_id, cm_fun_id.
665 cl_fun_id = cm_fun_id →
666 ∀cl_retval, cm_retval.
667 ∀sInv, fInv, kInv.
668 ∀cl_args_values, cm_args_values.
669 (* TODO: return_value_rel … INV frame_data cl_retval cm_retval →*)
670 (* TODO: add invariant All2 value_eq cl_args_values cm_args_values *)
671 clight_cminor_rel cl_ge cm_ge INV
672  (ClCallstate cl_fun_id
673   cl_fundef cl_args_values (Kcall cl_retval cl_f cl_env cl_k) cl_m)
674  (CmCallstate cm_fun_id cm_fundef
675   cm_args_values cm_m (Scall cm_retval cm_f stackptr cm_env sInv fInv cm_k kInv cm_stack))
676
677| CMR_call_store :
678 (* call to a function which returns to some location in memory in Cminor *)
679 ∀cl_ge, cm_ge, cl_f, cm_f.
680 ∀INV: clight_cminor_inv cl_ge cm_ge.
681 ∀alloc_type, cl_env, cl_m, cm_env, cm_m, cm_stack, stackptr.
682 (* TODO: put the actual invariants on memory and etc. here *)
683 ∀u: universe SymbolTag.
684 ∀cl_fundef, cm_fundef.
685 ∀Hglobals_fresh: globals_fresh_for_univ type (globals cl_ge cm_ge INV) u.
686 ∀Hfundef_fresh:  fd_fresh_for_univ cl_fundef u.
687 ∀rettyp. rettyp = opttyp_of_type (fn_return cl_f) →
688 ∀cl_k, cm_k.
689 ∀fblock.
690 match cl_fundef with
691 [ CL_Internal cl_function ⇒
692    find_funct clight_fundef cl_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? (CL_Internal cl_function) ∧
693    find_funct (fundef internal_function) cm_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? cm_fundef ∧
694    translate_fundef u (globals ?? INV) Hglobals_fresh cl_fundef Hfundef_fresh = OK ? cm_fundef ∧
695    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
696 | CL_External name argtypes rettype ⇒
697   True
698 ] →
699 ∀cl_fun_id, cm_fun_id.
700 cl_fun_id = cm_fun_id →
701 ∀cl_rettyp, cl_retval, cl_rettrace, cm_retval.
702 ∀cl_lhs, cm_lhs, Hinvariant_on_cm_lhs.
703 (* Explain where the lhs of the post-return assign comes from *)
704 exec_lvalue cl_ge cl_env cl_m cl_lhs = OK ? 〈cl_retval, cl_rettrace〉 →
705 translate_dest alloc_type cl_lhs = OK ? (MemDest ? «cm_lhs, Hinvariant_on_cm_lhs») →
706 (* TODO: Explain that the actual variable used to store the ret val is fresh and has the
707  * right type, etc *)
708 ∀cm_ret_var.
709 ∀sInv, fInv, kInv.
710 ∀cl_args_values, cm_args_values.
711 (* TODO: return_value_rel … INV frame_data cl_retval cm_retval →*)
712 (* TODO: add invariant All2 value_eq cl_args_values cm_args_values *)
713 ∀cm_stack.
714 clight_cminor_rel cl_ge cm_ge INV
715  (ClCallstate cl_fun_id
716   cl_fundef cl_args_values (Kcall (Some ? 〈cl_retval,cl_rettyp〉) cl_f cl_env cl_k) cl_m)
717  (CmCallstate cm_fun_id cm_fundef
718   cm_args_values cm_m (Scall cm_retval cm_f stackptr cm_env sInv fInv
719                          (Kseq (St_store (typ_of_type cl_rettyp) cm_lhs
720                                          (Id (typ_of_type cl_rettyp) cm_ret_var)) cm_k)
721                           kInv cm_stack))
722
723| CMR_while:
724 ∀cl_ge,cm_ge,INV,cl_f,cm_f.
725 ∀cl_env, cl_m, cm_env, cm_m, stackptr, stacksize.
726 ∀alloc_type.
727 ∀cl_k, cm_k. 
728 ∀sz,sg, cl_ty, cl_cond_desc.
729 ∀cl_body.
730 ∀entry_label, exit_label.
731 ∀cm_cond: CMexpr (ASTint sz sg).
732 ∀cm_body.
733 ∀cm_stack.
734 ∀rettyp.
735 ∀kInv: cont_inv cm_f cm_env cm_k.
736 ∀fInv: stmt_inv cm_f cm_env (f_body cm_f).
737 ∀sInv: stmt_inv cm_f cm_env
738           ((*St_label entry_label*)
739            (St_seq
740             (St_ifthenelse sz sg cm_cond (St_seq cm_body (St_goto entry_label)) St_skip)
741             (St_label exit_label St_skip))).
742 (* Constrain the CL type *)             
743 ∀Heq_ty: ASTint sz sg = typ_of_type cl_ty.           
744 (* ---- relate return type variable to actual return type ---- *)
745 rettyp = opttyp_of_type (fn_return cl_f) →
746 (* ---- relate Clight and Cminor functions ---- *)
747 ∀func_univ: universe SymbolTag.
748 ∀Hfresh_globals: globals_fresh_for_univ ? (globals ?? INV) func_univ.
749 ∀Hfresh_function: fn_fresh_for_univ cl_f func_univ.
750 translate_function func_univ (globals ?? INV) cl_f Hfresh_globals Hfresh_function = OK ? cm_f →
751 (* ---- relate continuations ---- *)
752 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 →
753 ∀stmt_univ,stmt_univ',lbl_univ,lbl_univ',lbl_univ'',lbls.
754 (* Invariants *)
755 ∀Em: embedding.
756 tmp_vars_well_allocated alloc_type stmt_univ' cm_env cm_m cl_m Em →        (* locals are properly allocated *)
757 characterise_vars (globals ?? INV) cl_f = 〈alloc_type, stacksize〉 →        (* specify how alloc_type is built *)
758 (∃m,m'. exec_alloc_variables empty_env m (fn_params cl_f @ fn_vars cl_f) = 〈cl_env,m'〉) → (* spec. Clight env *)
759 memory_inj Em cl_m cm_m →                                                  (* memory injection *)
760 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 *)
761 (∀b. block_region b = Code → Em b = Some ? 〈b, zero_offset〉) →             (* Force embedding to compute identity on functions *)
762 (* Make explicit the fact that locals in CL are mapped to a single CM block *)
763 (∀b1.∀delta. Em b1=Some ? 〈stackptr,delta〉 →
764              mem block b1 (blocks_of_env cl_env)) →
765 (* Expression translation and related hypotheses *)
766 ∀Hcond_tr.  (* invariant after converting conditional expr *)
767 translate_expr alloc_type (Expr cl_cond_desc cl_ty) = OK ? «CMcast ?? cm_cond Heq_ty, Hcond_tr » →
768 (* Label consistency *)
769 Exists ? (λl':identifier Label.l'=entry_label) (labels_of (f_body cm_f)) →
770 Exists ? (λl':identifier Label.l'=exit_label) (labels_of (f_body cm_f)) → 
771 (* Statement translation *)
772 ∀Htranslate_inv.
773 mklabels lbl_univ = 〈〈entry_label, exit_label〉, lbl_univ'〉 →
774 translate_statement alloc_type stmt_univ lbl_univ' lbls
775   (ConvertTo entry_label exit_label) rettyp cl_body
776   = OK ? «〈stmt_univ',lbl_univ'',cm_body〉,Htranslate_inv» →
777 (* ---- invariant on label existence ---- *)
778 lset_inclusion ? (labels_of cm_body) (labels_of (f_body cm_f)) → 
779 (* Express the fact that the label points where it ought to *)
780 ∀Hlabel_exists.
781 ∀Hinv1, Hinv2.
782 find_label_always entry_label (f_body cm_f) Kend Hlabel_exists cm_f cm_env fInv Hinv1
783   = «〈(*St_label entry_label*)
784       (St_seq
785        (St_ifthenelse sz sg cm_cond (St_seq cm_body (St_goto entry_label))
786         St_skip)
787        (St_label exit_label St_skip)),
788      cm_k〉,
789   Hinv2» →
790 (clight_cminor_rel cl_ge cm_ge INV
791  (ClState cl_f (Swhile (Expr cl_cond_desc cl_ty) cl_body) cl_k cl_env cl_m)
792  (CmState cm_f
793   ( (*St_label entry_label*)
794    (St_seq
795     (St_ifthenelse sz sg cm_cond (St_seq cm_body (St_goto entry_label)) St_skip)
796     (St_label exit_label St_skip)))
797   cm_env fInv sInv cm_m stackptr cm_k kInv cm_stack)).
798
799definition clight_normal : Clight_state → bool ≝
800λs. match Clight_classify s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ].
801
802definition cminor_normal : Cminor_state → bool ≝
803λs. match Cminor_classify s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ].
804
805definition cl_pre : preclassified_system ≝
806  mk_preclassified_system
807    clight_fullexec
808    (λg. Clight_labelled)
809    (λg. Clight_classify)
810    (λx,y,H. an_identifier ? one). (* XXX TODO *)
811
812definition cm_pre : preclassified_system ≝
813  mk_preclassified_system
814    Cminor_fullexec
815    (λg. Cminor_labelled)
816    (λg. Cminor_classify)
817    (λx,y,H. an_identifier ? one). (* XXX TODO *)
818
819(* --------------------------------------------------------------------------- *)
820(* General purpose auxilliary lemmas. *)
821(* --------------------------------------------------------------------------- *)
822
823lemma invert_assert :
824  ∀b. ∀P. assert b P → b = true ∧ P.
825* #P whd in ⊢ (% → ?); #H
826[ @conj try @refl @H
827| @False_ind @H ]
828qed.
829
830lemma res_to_io :
831  ∀A,B:Type[0]. ∀C.
832  ∀x: res A. ∀y.
833  match x with
834  [ OK v ⇒  Value B C ? v
835  | Error m ⇒ Wrong … m ] = return y →
836  x = OK ? y.
837#A #B #C *
838[ #x #y normalize nodelta whd in ⊢ ((???%) → ?); #Heq destruct (Heq) @refl
839| #err #y normalize nodelta whd in ⊢ ((???%) → ?); #Heq destruct (Heq) ]
840qed.
841
842lemma jmeq_absorb : ∀A:Type[0]. ∀a,b: A. ∀P:Prop. (a = b → P) → a ≃ b → P.
843#A #a #b #P #H #Heq lapply (jmeq_to_eq ??? Heq) #Heq' @H @Heq' qed.
844
845(* wrap up some trivial bit of reasoning to alleviate strange destruct behaviour *)
846lemma pair_eq_split :
847  ∀A,B:Type[0]. ∀a1,a2:A. ∀b1,b2:B.
848  〈a1,b1〉 = 〈a2, b2〉 →
849  a1 = a2 ∧ b1 = b2.
850#A #B #a1 #a2 #b1 #b2 #Heq destruct (Heq) @conj try @refl
851qed.
852
853lemma ok_eq_ok_destruct :
854  ∀A:Type[0]. ∀a,b:A. OK ? a = OK ? b → a = b.
855#H1 #H2 #H3 #H4 destruct @refl qed.
856
857lemma 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.
858#A #a #b #P #Ha #Hb #Heq destruct (Heq)
859@conj try %
860qed.
861
862(* inverting find_funct and find_funct_ptr *)
863lemma find_funct_inversion :
864  ∀F: Type[0]. ∀ge: genv_t F. ∀v: val. ∀res: F.
865      find_funct F ge v = Some ? res →
866      (∃ptr. v = Vptr ptr ∧
867            (poff ptr) = zero_offset ∧
868            block_region (pblock ptr) = Code ∧
869            (∃p. block_id (pblock ptr) = neg p ∧
870                 lookup_opt … p (functions … ge) = Some ? res)).
871#F #ge #v #res
872cases v
873[ | #sz #i | | #ptr ]
874whd in ⊢ ((??%?) → ?);
875#Heq destruct (Heq)
876%{ptr} @conj try @conj try @conj try @refl
877lapply Heq -Heq
878@(eq_offset_elim … (poff ptr) zero_offset) //
879normalize nodelta
880[ 1,3,5: #_ #Habsurd destruct (Habsurd) ]
881#Heq destruct (Heq)
882whd in ⊢ ((??%?) → ?);
883cases ptr #blo #off cases (block_region blo) normalize nodelta
884[ 1,3: #Habsurd destruct (Habsurd) ]
885[ // ]
886cases (block_id blo) normalize nodelta
887[ #Habsurd destruct (Habsurd) | #p #Habsurd destruct (Habsurd) ]
888#p #Hlookup %{p} @conj try @refl assumption
889qed.
890
891(* We should be able to prove that ty = ty' with some more hypotheses, if needed. *)
892lemma translate_dest_id_inversion :
893  ∀var_types, e, var_id, ty,H.
894   translate_dest var_types e = return IdDest var_types var_id ty H →
895   e = Expr (Evar var_id) (typeof e).
896@cthulhu
897(*   
898#vars #e #var_id #ty #H
899cases e #ed #ty'
900cases ed
901[ #sz #i | #id | #e1 | #e1 | #op #e1 |#op #e1 #e2 | #cast_ty #e1
902| #cond #iftrue #iffalse | #e1 #e2 | #e1 #e2 | #sizeofty | #e1 #field | #cost #e1 ]
903whd in ⊢ ((??%%) → ?);
904#Heq
905[ 1,4,5,6,7,8,9,10,11,13: destruct (Heq)
906| 3,12: cases (bind_inversion ????? Heq) * #H1 #H2 #H3 cases H3
907        #_ whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) ]
908lapply Heq -Heq
909change with (bind2_eq ????? ) in ⊢ ((??%?) → ?); #Heq
910cases (bind2_eq_inversion ?????? Heq)
911#alloctype
912(* * #alloctype *) * #typ' *
913cases alloctype
914[ #r | #n | ] normalize nodelta #Hlookup'
915[ 1,2: whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) ]
916whd in ⊢ ((??%%) → ?); #Heq' destruct (Heq')
917@refl*)
918qed.
919
920
921(* Note: duplicate in switchRemoval.ma *)
922lemma fresh_elim : ∀u. ∃fv',u'. fresh SymbolTag u = 〈fv', u'〉. #u /3 by ex_intro/ qed.
923
924lemma fresh_elim_lab : ∀u. ∃fv',u'. fresh Label u = 〈fv', u'〉. #u /3 by ex_intro/ qed.
925
926
927lemma breakup_dependent_match_on_pairs :
928 ∀A,B,C: Type[0].
929 ∀term: A × B.
930 ∀F: ∀x,y. 〈x, y〉 = term → C.
931 ∀z:C.
932 match term
933 return λx.x = term → ? with
934 [ mk_Prod x y ⇒ λEq. F x y Eq ] (refl ? term) = z →
935 ∃xa,xb,H. term = 〈xa, xb〉 ∧
936           F xa xb H = z.
937#A #B #C * #xa #xb #F #z normalize nodelta #H %{xa} %{xb} %{(refl ??)} @conj try @conj
938// qed.
939
940(* --------------------------------------------------------------------------- *)
941(* Extending simulation results on expressions to particular cases             *)
942(* --------------------------------------------------------------------------- *)
943
944lemma translate_expr_sigma_welltyped : ∀vars, cl_expr, cm_expr.
945  translate_expr_sigma vars cl_expr = OK ? cm_expr →
946  dpi1 ?? (pi1 ?? cm_expr) = typ_of_type (typeof cl_expr).
947#vars #cl_expr * * #typ #cm_expr normalize nodelta #Hexpr_vars
948whd in ⊢ ((??%?) → ?); #H
949cases (bind_inversion ????? H) -H * #cm_expr' #Hexpr_vars' *
950#Htranslate_expr
951whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) @refl
952qed.
953
954lemma translate_exprlist_sigma_welltyped :
955  ∀vars, cl_exprs, cm_exprs.
956  mmap_sigma ??? (translate_expr_sigma vars) cl_exprs = OK ? cm_exprs →
957  All2 ?? (λcl, cm. dpi1 ?? cm = typ_of_type (typeof cl)) cl_exprs (pi1 ?? cm_exprs).
958#vars #cl_exprs
959elim cl_exprs
960[ * #cm_exprs #Hall whd in ⊢ ((??%?) → ?); #Heq destruct (Heq) @I
961| #hd #tl #Hind * #cm_exprs #Hall #H
962  cases (bind_inversion ????? H) -H
963  * * #cm_typ #cm_expr normalize nodelta
964  #Hexpr_vars_cm * #Htranslate_hd
965  lapply (translate_expr_sigma_welltyped … Htranslate_hd)
966  #Heq_cm_typ #H
967  cases (bind_inversion ????? H) -H
968  #cm_tail lapply (Hind cm_tail) cases cm_tail
969  #cm_tail_expr #Hall_tail -Hind #Hind * #Heq_cm_tail normalize nodelta
970   whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) whd @conj
971   [ @Heq_cm_typ
972   | @Hind assumption ]
973] qed.
974
975lemma translate_dest_MemDest_simulation :
976  ∀cl_f  : function.
977  ∀cl_ge : genv_t clight_fundef.
978  ∀cm_ge : genv_t (fundef internal_function).
979  ∀INV   : clight_cminor_inv cl_ge cm_ge.
980  ∀alloc_type. 
981  ∀cl_env, cl_m, cm_env, cm_m, stackptr.
982  ∀Em.
983  ∀stacksize     : ℕ. 
984  ∀alloc_hyp     : characterise_vars (globals ?? INV) cl_f = 〈alloc_type, stacksize〉.
985  ∀cl_cm_env_hyp : ∃m,m'. exec_alloc_variables empty_env m (fn_params cl_f @ fn_vars cl_f) = 〈cl_env,m'〉.
986  ∀injection     : memory_inj Em cl_m cm_m.
987  ∀matching      : memory_matching Em cl_ge cm_ge cl_m cm_m cl_env cm_env INV stackptr alloc_type.
988  (* decorrelate goal from input using some eqs *)
989  ∀cl_expr. ∀cm_expr.
990  ∀cl_block, cl_offset, trace.
991  ∀Hyp_present. 
992     translate_dest alloc_type cl_expr = OK ? (MemDest ? cm_expr) →
993     exec_lvalue cl_ge cl_env cl_m cl_expr = OK ? 〈〈cl_block, cl_offset〉, trace〉 →
994     ∃cm_val. eval_expr cm_ge ASTptr cm_expr cm_env Hyp_present stackptr cm_m = OK ? 〈trace, cm_val〉 ∧
995              value_eq Em (Vptr (mk_pointer cl_block cl_offset)) cm_val.     
996#cl_f #cl_ge #cm_ge #INV #alloc_type
997#cl_env #cl_m #cm_env #cm_m #stackptr #Em #stacksize #alloc_hyp #cl_env_hyp #injection #matching
998#cl_expr * #cm_expr #Hexpr_vars #cl_block #cl_offset #trace #Hyp_present
999whd in match (translate_dest ??); cases cl_expr #cl_desc #cl_typ normalize nodelta
1000cases cl_desc normalize nodelta
1001[ #sz #i | #id | #e1 | #e1 | #op #e1 |#op #e1 #e2 | #cast_ty #e1
1002| #cond #iftrue #iffalse | #e1 #e2 | #e1 #e2 | #sizeofty | #e1 #field | #cost #e1 ]
1003#Htranslate
1004[ 2:
1005| *: cases (bind_inversion ????? Htranslate) -Htranslate * #cm_expr' #Hexpr_vars' *
1006     #Htranslate_addr
1007     whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) #Hexec_lvalue
1008     cases (eval_expr_sim cl_ge cm_ge INV cl_f alloc_type stacksize alloc_hyp … cl_env_hyp … injection … matching)
1009     #_ #Hsim
1010     @(Hsim ??? Hexpr_vars … Htranslate_addr ??? ? Hexec_lvalue) ]
1011cases (bind2_eq_inversion ?????? Htranslate) -Htranslate *
1012[ #r | #n | ]
1013* #cl_type * #Heq_lookup normalize nodelta
1014whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
1015whd in ⊢ ((??%?) → ?);
1016@(match lookup SymbolTag block cl_env id
1017  return λx. (lookup SymbolTag block cl_env id = x) → ?
1018  with
1019  [ None ⇒ ?
1020  | Some loc ⇒ ?
1021  ] (refl ? (lookup SymbolTag block cl_env id ))) normalize nodelta
1022#Hlookup_eq
1023[ 2,4: #Heq destruct (Heq) whd in match (eval_expr ???????);
1024  [ 2: %{(Vptr (mk_pointer stackptr (shift_offset (bitsize_of_intsize I16) zero_offset (repr I16 n))))}
1025       @conj try @refl
1026       lapply (matching id)
1027       >Hlookup_eq normalize nodelta
1028       >(opt_to_res_inversion ???? Heq_lookup) normalize nodelta
1029       #Hembed %4 whd in ⊢ (??%?); >Hembed @refl
1030  | 1: whd in match (eval_constant ????);
1031       lapply (matching id)
1032       >Hlookup_eq normalize nodelta 
1033       >(opt_to_res_inversion ???? Heq_lookup) normalize nodelta
1034       @False_ind
1035  ]
1036| 1,3: #Hfind_symbol
1037  cases (bind_inversion ????? Hfind_symbol) -Hfind_symbol #block *
1038  whd in ⊢ ((??%%) → ?); #Hfind_symbol
1039  lapply (opt_to_res_inversion ???? Hfind_symbol) #Hfind_symbol_eq
1040  whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
1041  whd in match (eval_expr ???????);
1042  whd in match (eval_constant ????);
1043  lapply (matching id)
1044  [ >Hlookup_eq normalize nodelta >Hfind_symbol_eq normalize nodelta
1045    #Hembed
1046    <(eq_sym … INV id) >Hfind_symbol_eq normalize nodelta
1047     %{(Vptr
1048         (mk_pointer cl_block
1049          (shift_offset (bitsize_of_intsize I16) zero_offset (repr I16 O))))}
1050     @conj try @refl
1051     %4 whd in ⊢ (??%?); >Hembed try @refl
1052  | (* A stack variable is not in the local environment but in the global one. *)
1053    (* we have a contradiction somewhere in the context *)
1054    lapply (variable_not_in_env_but_in_vartypes_is_global ???????
1055              cl_env_hyp alloc_hyp Hlookup_eq … Heq_lookup)
1056    *  #r #Habsurd destruct (Habsurd)
1057  ]
1058] qed.
1059 
1060(* lift simulation result to eval_exprlist *)
1061lemma eval_exprlist_simulation :
1062  ∀cl_f.
1063  ∀cl_ge : genv_t clight_fundef.
1064  ∀cm_ge : genv_t (fundef internal_function).
1065  ∀INV   : clight_cminor_inv cl_ge cm_ge.
1066  ∀alloc_type. 
1067  ∀cl_env, cl_m, cm_env, cm_m, stackptr.
1068  ∀Em.
1069  ∀stacksize     : ℕ. 
1070  ∀alloc_hyp     : characterise_vars (globals ?? INV) cl_f = 〈alloc_type, stacksize〉.
1071  ∀cl_env_hyp : ∃m,m'. exec_alloc_variables empty_env m (fn_params cl_f @ fn_vars cl_f) = 〈cl_env,m'〉.
1072  ∀injection     : memory_inj Em cl_m cm_m.
1073  ∀matching      : memory_matching Em cl_ge cm_ge cl_m cm_m cl_env cm_env INV stackptr alloc_type.
1074  ∀cl_exprs,cm_exprs.
1075  ∀cl_results,trace.
1076  exec_exprlist cl_ge cl_env cl_m cl_exprs = OK ? 〈cl_results, trace〉 →
1077  mmap_sigma ??? (translate_expr_sigma alloc_type) cl_exprs = OK ? cm_exprs →
1078  ∀H:All ? (λx:𝚺t:typ.expr t.
1079             match x with
1080             [ mk_DPair ty e ⇒
1081                    (expr_vars ty e
1082                     (λid:ident.λty:typ.present SymbolTag val cm_env id)) ]) cm_exprs.
1083  ∃cm_results.
1084  trace_map_inv … (λe. match e return λe.
1085                         match e with
1086                         [ mk_DPair _ _ ⇒ ? ] → ?
1087                       with
1088                       [ mk_DPair ty e ⇒ λp. eval_expr cm_ge ? e cm_env p stackptr cm_m ]) cm_exprs H = OK ? 〈trace, cm_results〉 ∧
1089  All2 ?? (λcl_val, cm_val. value_eq Em cl_val cm_val) cl_results cm_results.
1090#f #cl_ge #cm_ge #INV
1091#alloc_type #cl_env #cl_m #cm_env #cm_m #stackptr #Em #stacksize #alloc_hyp #cl_env_hyp #injection #matching
1092#cl_exprs
1093elim cl_exprs
1094[ #cm_exprs #cl_results #trace
1095  whd in ⊢ ((??%?) → ?);
1096  #Heq destruct (Heq)
1097  whd in ⊢ ((??%?) → ?);
1098  #Heq destruct (Heq) #H %{[]}
1099  @conj try @refl try @I
1100| #cl_hd #cl_tl #Hind #cm_exprs #cl_results #trace
1101  #Heq cases (bind_inversion ????? Heq) -Heq
1102  * #hd_val #hd_trace * #Hexec_expr_cl
1103  #Heq cases (bind_inversion ????? Heq) -Heq 
1104  * #cl_tl_vals #cl_tl_trace * #Hexec_expr_tl
1105  whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
1106  #Htranslate
1107  lapply (translate_exprlist_sigma_welltyped … Htranslate)
1108  #Htype_eq_all #Hall
1109  cases (bind_inversion ????? Htranslate) -Htranslate
1110  * * #cmtype #cmexpr normalize nodelta
1111  #Hexpr_vars_local_cm * #Htranslate_expr_sigma #Htranslate
1112  cases (bind_inversion ????? Htranslate) -Htranslate
1113  * #cm_tail #Hexpr_vars_local_cm_tail * #Htranslate_tail
1114  normalize nodelta
1115  whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
1116  cases Htype_eq_all -Htype_eq_all #Hcm_type_eq #Htype_eq_all
1117  lapply (Hind cm_tail cl_tl_vals cl_tl_trace Hexec_expr_tl)
1118  [ assumption ] -Hind #Hind
1119  lapply (Hind Htranslate_tail (proj2 ?? Hall)) -Hind
1120  * #cm_results_tl * #Hcm_exec_tl #Hvalues_eq_tl
1121  cases (eval_expr_sim cl_ge cm_ge INV f alloc_type stacksize alloc_hyp ?? cl_env_hyp ?? Em injection stackptr matching)
1122  #Hsim #_
1123  cases (bind_inversion ????? Htranslate_expr_sigma)
1124  * #cmexpr' #Hexpr_vars_local_cm' * #Htranslate
1125  whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
1126  lapply (Hsim cl_hd cmexpr ??????) -Hsim try assumption
1127  [ @(proj1 ?? Hall) ]
1128  * #cm_val_hd * #Heval_expr_cm #Hvalue_eq     
1129  %{(cm_val_hd :: cm_results_tl)} @conj
1130  [ 2: @conj try assumption
1131  | 1: whd in ⊢ (??%?); normalize nodelta >Heval_expr_cm
1132       normalize nodelta >Hcm_exec_tl @refl
1133  ]
1134] qed.
1135
1136(* --------------------------------------------------------------------------- *)
1137(* Putting the memory injection at work.                                       *)
1138(* --------------------------------------------------------------------------- *)
1139
1140(* A) Non-interference of local variables with memory injections  *)
1141
1142(* Needed property:
1143 * A local variable allocated via the temporary variable generator should not interfere
1144 * with the memory injection. In particular, we need to show that:
1145 * 1) we can successfuly store stuff of the right type inside (where the type is specified
1146 *    at generation time, and should be in the current context)
1147 * 2) after the store, we can build a consistent memory state and more generally, a
1148 *    correct [clight_cminor_data] invariant record. Cf. toCminorCorrectnessExpr.ma
1149 *)
1150 
1151(* A.1) memory matchings survives memory injection *)
1152
1153lemma offset_plus_0' : ∀o:offset. offset_plus zero_offset o = o.
1154#o cases o #b >offset_plus_0 @refl
1155qed.
1156
1157(*
1158lemma store_value_of_type_memory_matching_to_matching : 
1159  ∀cl_ge, cm_ge, cl_en, cm_en, INV, sp, vars, cl_m, cl_m',cm_m,cm_m'.
1160  ∀E: embedding.
1161  ∀blo, blo', delta, off.
1162  E blo = Some ? 〈blo', delta〉 →
1163  ∀cl_val, cm_val, ty.
1164  value_eq E cl_val cm_val →
1165  storen cl_m (mk_pointer blo off) (fe_to_be_values ty cl_val) = Some ? cl_m' →
1166  storen cm_m (mk_pointer blo (offset_plus off delta)) (fe_to_be_values ty cm_val) = Some ? cm_m' →
1167  (lookup' vars var_id = OK (var_type×type) 〈Global r,type_of_var〉)
1168  memory_inj E cl_m' cm_m' →
1169  memory_matching E cl_ge cm_ge cl_m cm_m cl_en cm_en INV sp vars →
1170  memory_matching E cl_ge cm_ge cl_m' cm_m' cl_en cm_en INV sp vars.
1171#cl_ge #cm_ge #cl_en #cm_en #INV #sp #vars #cl_m #cl_m' #cm_m #cm_m' #E
1172#blo #blo' #delta #off #Hembed #cl_val #cm_val #ty #Hvalue_eq #Hstoren_cl #Hstoren_cm
1173#Hinj #Hmatching #id
1174lapply (Hmatching id)
1175cases (lookup ?? cl_en id) normalize nodelta
1176[ 1: #H @H
1177| 2: #bl cases (lookup ?? vars id) normalize nodelta
1178  [ 1: #H @H
1179  | 2: * #var_type #cl_type normalize nodelta
1180       cases var_type normalize nodelta
1181       [ #r #H @H
1182       | #b #H @H
1183       | #H #v lapply H -H
1184         @(eq_block_elim … bl blo)
1185         [ #Heq destruct (Heq)
1186           @(eq_offset_elim … off zero_offset)
1187           [ (* We actually load exactly where we wrote, but with a potentially different type. *)
1188             #Heq destruct (Heq) #H
1189       ]
1190  ]
1191] qed.*)
1192
1193
1194lemma alloc_tmp_in_genlist :
1195  ∀vartypes. ∀g1, g2, g3.
1196  ∀id1, ty1, id2, ty2.
1197  alloc_tmp vartypes ty1 g1 = 〈id1, g2〉 →
1198  alloc_tmp vartypes ty2 g2 = 〈id2, g3〉 →
1199  Exists (identifier SymbolTag×type)
1200   (λx:identifier SymbolTag×type.x=〈id2,ty2〉) (tmp_env ? g3).
1201#vartypes #g1 #g2 #g3
1202#id1 #ty1 #id2 #ty2 #Halloc1 #Halloc2
1203lapply (breakup_dependent_match_on_pairs ?????? Halloc1) * #id1' * #u' * #Hfg1
1204* #Hfresh_eq generalize in match (fresh_map_add ????????); #ugly
1205generalize in ⊢ ((??(????(?????%))?) → ?); #ugly2
1206#Heq destruct (Heq)
1207lapply (breakup_dependent_match_on_pairs ?????? Halloc2) * #id2' * #u'' * #Hfg2
1208* #Hfresh_eq' generalize in match (fresh_map_add ????????); #ugly'
1209generalize in ⊢ ((??(????(?????%))?) → ?); #ugly2'
1210#Heq destruct (Heq) %1 @refl
1211qed. (* this last lemma has to be refitted. *)
1212
1213(* This, to say the least, is not pretty. Whenever we update the memory, we have to perform
1214 * a kind of functional record update on the frame_data. But of course, we also need equations
1215 * relating the old and new frame data. *)
1216(*
1217lemma update_clight_cminor_data_cm :
1218  ∀f, cl_ge, cm_ge, INV.
1219  ∀frame_data: clight_cminor_data f cl_ge cm_ge INV.
1220  ∀cl_m_v.
1221  ∀new_cm_mem.
1222  cl_m_v = cl_m … frame_data →
1223  ∀new_inj: memory_inj (Em … frame_data) cl_m_v new_cm_mem.
1224  ∃data:clight_cminor_data f cl_ge cm_ge INV.
1225          alloc_type … frame_data = alloc_type … data ∧
1226          cl_env … frame_data = cl_env … data ∧
1227          cm_env … frame_data = cm_env … data ∧
1228          stackptr … frame_data = stackptr … data ∧
1229          cl_m … frame_data = cl_m … data ∧
1230          new_cm_mem = (cm_m … data).
1231#f #cl_ge #cm_ge #INV #frame_data #cl_m_v #new_cm_mem #H destruct (H) #Hinj
1232%{(mk_clight_cminor_data ????
1233       (alloc_type … frame_data)
1234       (stacksize … frame_data)
1235       (alloc_hyp … frame_data)
1236       (cl_env … frame_data)
1237       (cm_env … frame_data)
1238       (cl_env_hyp … frame_data)
1239       (cl_m … frame_data)
1240       new_cm_mem
1241       (Em … frame_data)
1242       Hinj
1243       (stackptr … frame_data)
1244       (matching … frame_data)
1245       (Em_fn_id … frame_data))}
1246@conj try @conj try @conj try @conj try @conj try @refl
1247qed.*)
1248
1249(* Same thing, this time update both CL and CM memory. Here we provide a proof
1250 * that the data in local env is not touched. *)
1251(*
1252lemma update_clight_cminor_data_cl_cm_global :
1253  ∀f, cl_ge, cm_ge, INV.
1254  ∀frame_data: clight_cminor_data f cl_ge cm_ge INV.
1255  ∀new_cl_mem, new_cm_mem.
1256  ∀new_inj: memory_inj (Em … frame_data) new_cl_mem new_cm_mem. 
1257  (∀id, b, cl_type.
1258   lookup ?? (cl_env … frame_data) id = Some ? b →
1259   lookup ?? (alloc_type … frame_data) id = Some ? 〈Local, cl_type〉 →
1260   load_value_of_type cl_type (cl_m … frame_data) b zero_offset =
1261   load_value_of_type cl_type new_cl_mem b zero_offset) → 
1262  ∃data:clight_cminor_data f cl_ge cm_ge INV.
1263        alloc_type … frame_data = alloc_type … data ∧
1264        cl_env … frame_data = cl_env … data ∧
1265        cm_env … frame_data = cm_env … data ∧
1266        stackptr … frame_data = stackptr … data ∧
1267        new_cl_mem = (cl_m … data) ∧
1268        new_cm_mem = (cm_m … data).
1269#f #cl_ge #cm_ge #INV #frame_data #new_cl_mem #new_cm_mem #Hinj #Haux
1270%{(mk_clight_cminor_data ????
1271       (alloc_type … frame_data)
1272       (stacksize … frame_data)
1273       (alloc_hyp … frame_data)
1274       (cl_env … frame_data)
1275       (cm_env … frame_data)
1276       (cl_env_hyp … frame_data)
1277       new_cl_mem
1278       new_cm_mem
1279       (Em … frame_data)
1280       Hinj
1281       (stackptr … frame_data)
1282       ? (* (matching … frame_data) *)
1283       (Em_fn_id … frame_data))}
1284[ whd #id
1285  lapply (matching … frame_data id)
1286  lapply (Haux id)
1287  cases (lookup ??? id) normalize nodelta
1288  [ #_ #H @H
1289  | #b cases (lookup ??? id) normalize nodelta
1290    [ #_ #H @H
1291    | * #vartype #cltype normalize nodelta
1292      cases vartype try // normalize nodelta #Haux
1293      #H #v #Hload @H >(Haux ?? (refl ??) (refl ??)) @Hload
1294    ]
1295  ]
1296|
1297@conj try @conj try @conj try @conj try @conj try @conj try @refl
1298qed.*)
1299
1300lemma store_value_of_type_success_by_value :
1301   ∀ty, m, m', b, o, v.
1302   store_value_of_type ty m b o v = Some ? m' →
1303   access_mode ty = By_value (typ_of_type ty) ∧
1304   storev (typ_of_type ty) m (Vptr (mk_pointer b o)) v = Some ? m'.   
1305#ty #m #m' #b #o #v
1306cases ty
1307[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
1308| #structname #fieldspec | #unionname #fieldspec | #id ]
1309whd in ⊢ ((??%?) → ?);
1310[ 1,4,5,6,7: #Habsurd destruct (Habsurd) ]
1311#H @conj try @refl @H
1312qed.
1313
1314(* Some boilerplate to avoid performing a case analysis on exprs in the middle of
1315 * the proof. *)
1316lemma translate_dest_not_Evar_id :
1317  ∀vars, ed, ty.
1318  (∀id. ed ≠ Evar id) →
1319    translate_dest vars (Expr ed ty) =
1320    (do e1' ← translate_addr vars (Expr ed ty);
1321     OK ? (MemDest ? e1')).
1322#vars *
1323[ #sz #i | #id | #e1 | #e1 | #op #e1 |#op #e1 #e2 | #cast_ty #e1
1324| #cond #iftrue #iffalse | #e1 #e2 | #e1 #e2 | #sizeofty | #e1 #field | #cost #e1 ]
1325#ty #H
1326[ 2: @False_ind @(absurd … (refl ??) (H ?)) ]
1327@refl
1328qed.
1329
1330lemma expr_is_Evar_id_dec :
1331  ∀ed. (∀id. ed ≠ Evar id) ∨ (∃id. ed = Evar id).
1332
1333[ #sz #i | #id | #e1 | #e1 | #op #e1 |#op #e1 #e2 | #cast_ty #e1
1334| #cond #iftrue #iffalse | #e1 #e2 | #e1 #e2 | #sizeofty | #e1 #field | #cost #e1 ]
1335[ 2: %2 %{id} @refl
1336| *: %1 #id % #Habsurd destruct (Habsurd) ]
1337qed.
1338
1339(* Not provable: need to relate (typeof (e=Evar id, ty)) with the type contained
1340   in var_ty. Should be doable, but not now. *)
1341(*   
1342lemma translate_dest_IdDest_typ :
1343  ∀vars,e,var_id,var_ty,H.
1344    translate_dest vars e = return (IdDest vars var_id var_ty H) →
1345    var_ty = typeof e.
1346#vars * #ed #ety #var_id #var_ty #H
1347cases ed   
1348[ #sz #i | #id | #e1 | #e1 | #op #e1 |#op #e1 #e2 | #cast_ty #e1
1349| #cond #iftrue #iffalse | #e1 #e2 | #e1 #e2 | #sizeofty | #e1 #field | #cost #e1 ]
1350[ 2,3,12:
1351  [ 2,3:
1352    whd in ⊢ ((??%?) → ?);
1353    cases (translate_addr ??) normalize nodelta
1354    [ 2,3: #error whd in ⊢ ((??%%) → ?); #Habsurd destruct (Habsurd)
1355    | 1,4: #Hfoo whd in ⊢ ((??%%) → ?); #Habsurd destruct (Habsurd) ]
1356  | 1: #H' lapply (bind2_eq_inversion ?????? H') * #vt * #t * #Eq
1357    lapply Eq inversion vt normalize nodelta
1358    [ 1,2: #foo #bar #Hlookup
1359      whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1360    | 3: #e whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
1361| *: whd in ⊢ ((??%?) → ?); whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd)
1362normalize nodelta
1363[ 2:*)
1364
1365
1366lemma mk_offset_offv_id : ∀o. mk_offset (offv o) = o.
1367* #x @refl qed.
1368
1369lemma find_funct_to_find_funct_id :
1370   ∀F, ge, ptr, fundef.
1371   ∀H:find_funct ? ge ptr = Some ? fundef.
1372   find_funct_id F ge ptr = Some ? 〈fundef, symbol_of_function_val' F ge ptr fundef H〉.
1373#F #ge #ptr #fundef #Hfind whd in match (find_funct_id ???);
1374generalize in ⊢ (??(?%)?);
1375generalize in ⊢
1376 ((???%) → (??
1377    (match %
1378(*     return λ_. (??%?) → ?*)
1379     with
1380     [ _ ⇒ λ_. ?
1381     | _ ⇒ λ_.λ_. ? ] ?)
1382  ?));
1383#o cases o normalize nodelta
1384[ #H @False_ind >Hfind in H; #Habsurd destruct (Habsurd)
1385| #f #Hfind' 
1386  cut (f = fundef)
1387  [ >Hfind in Hfind'; #Heq destruct (Heq) @refl ]
1388  #Heq destruct (Heq)
1389  @refl
1390] qed.
1391
1392lemma eval_bool_of_val_to_Cminor :
1393  ∀E. ∀ty. ∀v1,v2. ∀b.
1394    value_eq E v1 v2 →
1395    exec_bool_of_val v1 ty = return b →
1396    eval_bool_of_val v2 = return  b.
1397#E #ty #v1 #v2 #b #Hvalue_eq
1398whd in ⊢ ((??%%) → (??%%));
1399@(value_eq_inversion … Hvalue_eq) normalize nodelta
1400[ #Habsurd destruct (Habsurd) ]
1401[ #vsz #vi cases ty
1402  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
1403  | #structname #fieldspec | #unionname #fieldspec | #id ] normalize nodelta
1404  [ 2: | *: #Habsurd destruct (Habsurd) ]
1405  @(intsize_eq_elim_elim … vsz sz)
1406  [ 1: #H #Habsurd destruct (Habsurd)
1407  | 2: #Heq destruct (Heq) normalize nodelta #H @H ]
1408| cases ty
1409  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
1410  | #structname #fieldspec | #unionname #fieldspec | #id ] normalize nodelta
1411  #H destruct (H) @refl
1412| #p1 #p2 #Htranslate
1413  cases ty
1414  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
1415  | #structname #fieldspec | #unionname #fieldspec | #id ] normalize nodelta
1416  #H destruct (H) @refl
1417] qed.
1418
1419lemma let_prod_as_inversion :
1420    ∀A,B,C: Type[0].
1421    ∀expr: A × B.
1422    ∀body: ∀a:A. ∀b:B. 〈a,b〉 = expr → res C.
1423    ∀result: C.
1424    (let 〈a,b〉 as E ≝ expr in body a b E) = return result →
1425    ∃x,y. ∃E. 〈x,y〉 = expr ∧
1426          body x y E = return result.
1427#A #B #C * #a #b #body #res normalize nodelta #Heq
1428%{a} %{b} %{(refl ??)} @conj try @refl @Heq
1429qed.
1430
1431(* move this to frontend_misc *)
1432lemma lset_inclusion_Exists : ∀A, l1, l2, P.
1433  Exists A P l1 → lset_inclusion A l1 l2 → Exists A P l2.
1434#A #l1 #l2 #P #Hexists whd in ⊢ (% → ?);
1435lapply Hexists
1436generalize in match l2;
1437elim l1
1438[ #l2 @False_ind
1439| #hd #tl #Hind #l2 *
1440  [ 2: #HA * #Hhd #Htl @Hind try assumption
1441  | 1: #H * #Hmem #_ elim l2 in Hmem;
1442       [ @False_ind
1443       | #hd2 #tl2 #Hind *
1444         [ #Heq destruct (Heq) %1 @H
1445         | #Hneq %2 @Hind @Hneq ]
1446       ]
1447  ]
1448] qed.
1449
1450axiom load_value_after_free_list_inversion :
1451  ∀ty, m, blocks, b, o, v.
1452  load_value_of_type ty (free_list m blocks) b o = Some ? v → 
1453  load_value_of_type ty m b o = Some ? v.
1454
1455(* --------------------------------------------------------------------------- *)
1456(* Main simulation results                                                     *)
1457(* -------------------------------------------------------------------;-------- *)
1458
1459(* Conjectured simulation results
1460
1461   We split these based on the start state:
1462   
1463   1. ‘normal’ states take some [S n] normal steps and simulates them by [S m]
1464      normal steps in Cminor;
1465   2. call and return steps are simulated by a call/return step plus [m] normal
1466      steps (to copy stack allocated parameters / results); and
1467   3. lone cost label steps are simulated by a lone cost label step
1468   
1469   These should allow us to maintain enough structure to identify the Cminor
1470   subtrace corresponding to a measurable Clight subtrace.
1471 *)
1472
1473 
1474
1475lemma clight_cminor_normal :
1476    ∀g1,g2.
1477    ∀INV:clight_cminor_inv g1 g2.
1478    ∀s1,s1'.
1479    clight_cminor_rel g1 g2 INV s1 s1' →
1480    clight_normal s1 →
1481    ¬ pcs_labelled cl_pre g1 s1 →
1482    ∀s2,tr. step … (pcs_exec cl_pre) g1 s1 = Value … 〈tr,s2〉 →   
1483    ∃m. after_n_steps m ?? (pcs_exec cm_pre) g2 s1' (λs.cminor_normal s) (λtr',s2'.
1484      tr = tr' ∧
1485      clight_cminor_rel g1 g2 INV s2 s2' ∧
1486      (m = 0 → lex_lt (measure_Clight s2) (measure_Clight s1))
1487    ).
1488#g1 #g2 #INV #s1 #s1' #Hstate_rel #Hclight_normal #Hnot_labeleld
1489inversion Hstate_rel
1490[ 1: (* Normal state *)
1491     (* ---------------------------------------------------------------------- *)
1492#cl_ge #cm_ge #INV' #cl_s
1493(* case analysis on Clight statement *)
1494cases cl_s
1495[ 1: | 2: #lhs #rhs | 3: #retv #func #args | 4: #stm1 #stm2 | 5: #cond #iftrue #iffalse | 6: #cond #body
1496| 7: #cond #body | 8: #init #cond #step #body | 9,10: | 11: #retval | 12: #cond #switchcases | 13: #lab #body
1497| 14: #lab | 15: #cost #body ]
1498(*
1499[ 11: (* Return case *)
1500     #cm_s #cl_k #cm_k #cm_st #cl_f #cm_f #rettyp
1501     #alloc_type #cl_env #cl_m #cm_env #cm_m #stackptr #stacksize
1502     (* introduce everything *)
1503     #fInv #sInv #kInv #Htarget_type #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function
1504     #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls
1505     #flag #Htrans_inv #Htranslate #Hlabel_inclusion #Hcont_rel
1506     #Em #Htmp_vars_well_allocated #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id
1507     @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
1508     destruct (HA HB)
1509     @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE #_
1510     destruct (HC HD HE)
1511     whd in Htranslate:(??%?);
1512     cases retval in Htranslate; normalize nodelta
1513     [ cases rettyp in Htrans_inv Hcont_rel;
1514       [ 2: #opttyp normalize nodelta #Htrans_inv #_
1515            #Habsurd destruct (Habsurd)
1516       | 1: #Htrans_inv #Hcont_rel normalize nodelta #Heq destruct (Heq)
1517            #s2 #tr whd in ⊢ ((??%?) → ?);
1518            cases (fn_return cl_f)
1519            [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
1520            | #structname #fieldspec | #unionname #fieldspec | #id ]
1521            normalize nodelta
1522            [ 1:
1523            | *: #Habsurd destruct (Habsurd) ]
1524            whd in ⊢ ((??%?) → ?);
1525            #Heq destruct (Heq)
1526            %{1} whd @conj try @conj
1527            [ 3: #Habsurd destruct (Habsurd)
1528            | 1: @refl ]
1529            @CMR_return
1530*)     
1531[ 6: (* While *)
1532     #cm_s #cl_k #cm_k #cm_st #cl_f #cm_f #rettyp
1533     #alloc_type #cl_env #cl_m #cm_env #cm_m #stackptr #stacksize
1534     (* introduce everything *)
1535     #fInv #sInv #kInv #Htarget_type #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function
1536     #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls
1537     #flag * * * * #Hstmt_inv_cm cases cond #cond_desc #cond_ty
1538     (* early case analysis to avoid dependency hell *)
1539     cases cond_ty
1540     [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
1541     | #structname #fieldspec | #unionname #fieldspec | #id ]     
1542     #Hlabels_translated #Htmps_preserved
1543     #Hreturn_ok #Hlabel_wf #Htranslate #Hlabel_inclusion
1544     #Hcont_rel
1545     #Em #Htmp_vars_well_allocated #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id
1546     #Hframe_spec
1547     @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
1548     destruct (HA HB)
1549     @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE #_
1550     destruct (HC HD HE)
1551     lapply Htranslate -Htranslate
1552     [ 1: generalize in match (conj ????); #Hugly_inv
1553     | 2: generalize in match (conj ????); #Hugly_inv
1554     | 3: generalize in match (conj ????); #Hugly_inv
1555     | 4: generalize in match (conj ????); #Hugly_inv
1556     | 5: generalize in match (conj ????); #Hugly_inv
1557     | 6: generalize in match (conj ????); #Hugly_inv
1558     | 7: generalize in match (conj ????); #Hugly_inv
1559     | 8: generalize in match (conj ????); #Hugly_inv ]
1560     #Htranslate
1561     cases (bind_inversion ????? Htranslate) -Htranslate
1562     whd in match (typeof ?); whd in match (typ_of_type ?); *
1563     #cm_cond #Hexpr_vars_cond * #Htranslate_cond normalize nodelta
1564     [ 3,4,5,8: whd in ⊢ ((??%%) → ?); #Habsurd destruct (Habsurd) ]
1565     #Htranslate normalize nodelta
1566     lapply (let_prod_as_inversion ?????? Htranslate) -Htranslate
1567     * * #entry_label #exit_label * #lbl_univ0 * #Hmk_label_eq *
1568     #Hmk_label_eq_bis normalize nodelta #Htranslate
1569     cases (bind_inversion ????? Htranslate) -Htranslate
1570     * * * #stmt_univ0 #lbl_univ1 #cm_body
1571     #Htrans_inv * #Htrans_body normalize nodelta
1572     [ generalize in ⊢ ((??(??(????%))?) → ?);
1573       #Htrans_inv'
1574     | generalize in ⊢ ((??(??(????%))?) → ?);
1575       #Htrans_inv'
1576     | generalize in ⊢ ((??(??(????%))?) → ?);
1577       #Htrans_inv'
1578     | generalize in ⊢ ((??(??(????%))?) → ?);
1579       #Htrans_inv' ]
1580     whd in ⊢ ((???%) → ?);
1581     #Heq destruct (Heq)
1582     #s2 #tr whd in ⊢ ((??%?) → ?);
1583     #Hstep
1584     cases (bindIO_inversion ??????? Hstep) -Hstep * #cond_val #cond_trace
1585     * #Hcl_exec_cond #Hstep
1586     cases (bindIO_inversion ??????? Hstep) -Hstep
1587     #cl_cond_bool * #Hcl_bool_of_val whd in ⊢ ((??%%) → ?);
1588     cases cl_cond_bool in Hcl_bool_of_val;
1589     [ 1,3,5,7: (* cond = true: continue looping *)
1590       #Hcl_bool_of_val normalize nodelta
1591       #Heq destruct (Heq)
1592       %{4} whd whd in ⊢ (??%?); normalize nodelta
1593       [ generalize in match (proj1 ???); #Hpresent_ifthenelse
1594       | generalize in match (proj1 ???); #Hpresent_ifthenelse
1595       | generalize in match (proj1 ???); #Hpresent_ifthenelse
1596       | generalize in match (proj1 ???); #Hpresent_ifthenelse ]
1597       (* Exhibit simulation of condition evaluation *)
1598       lapply (eval_expr_sim … Halloc_hyp … Hcl_env_hyp … Hinjection … Hmatching) * #Hsim #_
1599       [ lapply (Hsim (Expr cond_desc Tvoid) … Htranslate_cond ?? Hpresent_ifthenelse Hcl_exec_cond)
1600       | lapply (Hsim (Expr cond_desc (Tint sz sg)) … Htranslate_cond ?? Hpresent_ifthenelse Hcl_exec_cond)
1601       | lapply (Hsim (Expr cond_desc (Tstruct structname fieldspec)) … Htranslate_cond ?? Hpresent_ifthenelse Hcl_exec_cond)
1602       | lapply (Hsim (Expr cond_desc (Tunion unionname fieldspec)) … Htranslate_cond ?? Hpresent_ifthenelse Hcl_exec_cond) ]
1603       * #cm_val_cond * #Hcm_eval_cond #Hvalue_eq >Hcm_eval_cond
1604       whd in match (m_bind ?????);
1605       >(eval_bool_of_val_to_Cminor … Hvalue_eq … Hcl_bool_of_val)
1606       normalize nodelta whd
1607       [ generalize in match (proj1 ???); #Hnoise'
1608         generalize in match (conj ????); #Hnoise''
1609       | generalize in match (proj1 ???); #Hnoise'
1610         generalize in match (conj ????); #Hnoise''
1611       | generalize in match (proj1 ???); #Hnoise'
1612         generalize in match (conj ????); #Hnoise''
1613       | generalize in match (proj1 ???); #Hnoise'
1614         generalize in match (conj ????); #Hnoise'' ]
1615       @conj try @conj
1616       [ 3,6,9,12: #Habsurd destruct (Habsurd)
1617       | 1,4,7,10: normalize >append_nil @refl
1618       | 2,5,8,11:
1619            cut (lset_inclusion (identifier Label) (labels_of cm_body) (labels_of (f_body cm_f)))
1620            [ 1,3,5,7:
1621              lapply Hlabel_inclusion
1622              @transitive_lset_inclusion
1623              @cons_preserves_inclusion
1624              @lset_inclusion_union %1
1625              @lset_inclusion_union %1
1626              @lset_inclusion_union %1
1627              @reflexive_lset_inclusion ]
1628            #Hlabels_of_body
1629            cut (Exists (identifier Label) (λl'.l'=entry_label) (labels_of (f_body cm_f)))
1630            [ 1,3,5,7: @(lset_inclusion_Exists ????? Hlabel_inclusion)
1631              %1 @refl ]
1632            #Hentry_exists
1633            cut (Exists (identifier Label) (λl'.l'=exit_label) (labels_of (f_body cm_f)))
1634            [ 1,3,5,7: @(lset_inclusion_Exists ????? Hlabel_inclusion)
1635              %2 @Exists_append_r %1 @refl ]
1636            #Hexit_exists
1637            @(CMR_normal … Htrans_body) try assumption
1638            @(ClCm_cont_while … (sym_eq … Hmk_label_eq) … Htrans_body) try assumption
1639            [ 1,6,11,16:
1640              @refl
1641            | 2,3,7,8,12,13,17,18:
1642              >CMcast_identity try assumption
1643            | 4,9,14,19:
1644                 @conj try assumption @conj @conj try assumption @conj @conj try assumption
1645                 try @conj try assumption try @conj try assumption
1646                 try @conj try assumption try @conj try assumption
1647            | 5,10,15,20: (* find_label_always *)
1648                 (* TODO /!\ we need to find a clever way to prove this. *)
1649                 @cthulhu
1650            ]
1651       ]
1652     | 2,4,6,8: (* cond = false: stop looping *)
1653       #Hcl_bool_of_val normalize nodelta #Heq destruct (Heq)
1654       %{5} whd whd in ⊢ (??%?); normalize nodelta
1655       [ generalize in match (proj1 ???); #Hpresent_ifthenelse
1656       | generalize in match (proj1 ???); #Hpresent_ifthenelse
1657       | generalize in match (proj1 ???); #Hpresent_ifthenelse
1658       | generalize in match (proj1 ???); #Hpresent_ifthenelse ]
1659       (* Exhibit simulation of condition evaluation *)
1660       lapply (eval_expr_sim … Halloc_hyp … Hcl_env_hyp … Hinjection … Hmatching) * #Hsim #_
1661       [ lapply (Hsim (Expr cond_desc Tvoid) … Htranslate_cond ?? Hpresent_ifthenelse Hcl_exec_cond)
1662       | lapply (Hsim (Expr cond_desc (Tint sz sg)) … Htranslate_cond ?? Hpresent_ifthenelse Hcl_exec_cond)
1663       | lapply (Hsim (Expr cond_desc (Tstruct structname fieldspec)) … Htranslate_cond ?? Hpresent_ifthenelse Hcl_exec_cond)
1664       | lapply (Hsim (Expr cond_desc (Tunion unionname fieldspec)) … Htranslate_cond ?? Hpresent_ifthenelse Hcl_exec_cond) ]       
1665       * #cm_val_cond * #Hcm_eval_cond #Hvalue_eq >Hcm_eval_cond
1666       whd in match (m_bind ?????);
1667       >(eval_bool_of_val_to_Cminor … Hvalue_eq … Hcl_bool_of_val) normalize nodelta whd
1668       [ generalize in match (proj2 ???); #Hnoise'
1669         generalize in match (proj2 ???); #Hnoise''
1670       | generalize in match (proj2 ???); #Hnoise'
1671         generalize in match (proj2 ???); #Hnoise''
1672       | generalize in match (proj2 ???); #Hnoise'
1673         generalize in match (proj2 ???); #Hnoise''
1674       | generalize in match (proj2 ???); #Hnoise'
1675         generalize in match (proj2 ???); #Hnoise'' ]
1676       @conj try @conj try @conj
1677       [ 1,4,7,10: normalize >append_nil >append_nil @refl
1678       | 2,5,8,11:
1679          @(CMR_normal … Htranslate_function … DoNotConvert … Hcont_rel) try assumption
1680          [ 2,4,6,8: @refl | *: ]
1681       | *: #Habsurd destruct (Habsurd) ]
1682   ]
1683| 3: (* Call *)
1684     #cm_s #cl_k #cm_k #cm_st #cl_f #cm_f #rettyp
1685     #alloc_type #cl_env #cl_m #cm_env #cm_m #stackptr #stacksize
1686     (* introduce everything *)
1687     #fInv #sInv #kInv #Htarget_type #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function
1688     #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls
1689     #flag * * * * #Hstmt_inv #Hlabels_translated #Htmps_preserved #Hreturn_ok #Hlabel_wf
1690     (* generalize away ugly proof *)
1691     generalize in ⊢ (∀_:(???(??(????%))).?); #Hugly
1692     #Htranslate #Hlabel_inclusion #Hcont_rel #Em
1693     #Htmp_vars_well_allocated
1694     #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id
1695     #Hframe_spec
1696     @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
1697     destruct (HA HB)
1698     @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
1699     destruct (HC HD HE) #_
1700     (* back to unfolding Clight execution *)
1701     cases (bind_inversion ????? Htranslate) -Htranslate *
1702     #ef #Hexpr_vars_ef * #Htranslate_ef normalize nodelta #Htranslate
1703     cases (bind_inversion ????? Htranslate) -Htranslate *
1704     #ef' #Hexpr_vars_local_ef' * #Htyp_should_eq_ef
1705     cases (typ_should_eq_inversion (typ_of_type (typeof func)) ASTptr … Htyp_should_eq_ef)
1706     -Htyp_should_eq_ef #Htyp_equality_ef
1707     #Heq_ef_ef' #Htranslate
1708     cases (bind_inversion ????? Htranslate) -Htranslate *
1709     #cm_args #Hall_variables_from_args_local *
1710     whd in ⊢ ((???%) → ?); #Hargs_spec
1711     @(match retv
1712       return λx. retv = x → ?
1713       with
1714       [ None ⇒ λHretv. ?
1715       | Some lhs ⇒ λHretv. ?
1716       ] (refl ? retv))
1717     normalize nodelta
1718     [ 2: (* return something *)
1719       #Hdest cases (bind_inversion ????? Hdest) -Hdest #dest *
1720       inversion dest normalize nodelta
1721       [ (* register dest *) #var_id #var_ty #His_local @(jmeq_absorb ?????) #Hdest       
1722         #Htranslate_dest whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1723         (* make explicit the nature of lhs, allowing to prove that no trace is emitted *)
1724         lapply (translate_dest_id_inversion  … Htranslate_dest) #Hlhs_eq
1725       | * #cm_expr #Hexpr_vars_cm #Hdest #Htranslate_dest #Hgensym
1726         lapply (breakup_dependent_match_on_pairs ?????? Hgensym) -Hgensym
1727         * #ret_var * #new_gensym * #Heq_alloc_tmp * #_ #Hgensym
1728         lapply (breakup_dependent_match_on_pairs ?????? Hgensym) -Hgensym
1729         * #tmp_var * #new_gensym' * #Heq_alloc_tmp' * #_
1730         generalize in ⊢ ((??(?? (????%) )?) → ?); #Hstmt_inv_after_gensym
1731         whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1732       ]
1733     | 1: (* return void *)
1734          generalize in ⊢ ((??(??(????%))?) → ?); #Hugly2
1735          whd in ⊢ ((???%) → ?); #Heq destruct (Heq) ]
1736     #s2 #tr #Htranslate
1737     cases (bindIO_inversion ??????? Htranslate) -Htranslate *
1738     #func_ptr_val #func_trace * #Hexec_func_ptr normalize nodelta
1739     whd in ⊢ ((???%) → ?); #Htranslate
1740     cases (bindIO_inversion ??????? Htranslate) -Htranslate *
1741     #args_values #args_trace * #Hexec_arglist #Htranslate
1742     cases (bindIO_inversion ??????? Htranslate) -Htranslate
1743     * #cl_fundef #cl_fun_id * #Hfind_funct
1744     lapply (opt_to_io_Value ?????? Hfind_funct) -Hfind_funct #Hfind_funct
1745     cases (find_funct_inversion ???? Hfind_funct)
1746     #func_ptr * * * #Hfunc_ptr_eq destruct (Hfunc_ptr_eq)
1747     #Hpoff_eq_zero #Hregion_is_code
1748     * #block_id * #Hblock_id_neg #Hlookup
1749     #Htranslate
1750     cases (bindIO_inversion ??????? Htranslate) -Htranslate #Htype_of_fundef *
1751     #Hassert_type_eq
1752     [ 1,2: #Htranslate
1753            cases (bindIO_inversion ??????? Htranslate) -Htranslate * *
1754            #lblock #loffset #ltrace *
1755            whd in ⊢ ((???%) → (???%) → ?);
1756            [ >Hlhs_eq #Hexec_lvalue
1757              cut (ltrace = [])
1758              [ lapply (res_to_io ????? Hexec_lvalue)
1759                #H' whd in H':(??%?); cases (lookup ????) in H'; normalize nodelta
1760                [ 2: #b #Heq destruct (Heq) @refl
1761                | #H cases (bind_inversion ????? H) #H24 * #H27 #H28
1762                  whd in H28:(???%); destruct (H28) @refl ]
1763              ] #H destruct (H)
1764            | #Hexec_lvalue ]
1765     | 3: ]
1766     whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
1767     [ 1: %{1} whd whd in ⊢ (??%?); normalize nodelta
1768     | 2: (* Execute Cminor part: evaluate lhs, evaluate assign *)
1769          %{5} whd whd in ⊢ (??%?); normalize nodelta
1770          whd in match (eval_expr ???????);
1771          whd in match (m_bind ?????);
1772          cut (expr_vars ASTptr cm_expr
1773                  (λid:ident.λty:typ.present SymbolTag val cm_env id))
1774          [ cases sInv * * * * * * * #_ #H #_ #_ #_ @H ] #Hexpr_vars_cut
1775          lapply (translate_dest_MemDest_simulation … Htranslate_dest Hexec_lvalue)
1776          try assumption try @refl
1777          * #cm_val_tmp * #Heval_expr_tmp >Heval_expr_tmp #Hvalue_eq
1778          normalize nodelta generalize in match (proj1 ???); #Htmp_var_present
1779          cases (value_eq_ptr_inversion … Hvalue_eq) #cm_ptr * #Hcm_val_tmp #Hcm_ptr_translation
1780          >Hcm_val_tmp
1781          lapply (Htmp_vars_well_allocated … tmp_var Htmp_var_present (Tpointer (typeof lhs)) ? (Vptr cm_ptr) ?)
1782          [ 2: @(alloc_tmp_in_genlist … (sym_eq ??? Heq_alloc_tmp) (sym_eq ??? Heq_alloc_tmp'))
1783          | 1: normalize cases cm_ptr #b #o %3 ]
1784          * #cm_mem_after_store * #Hstorev #Hnew_inj >Hstorev
1785          whd in match (m_bind ?????); normalize nodelta
1786          whd whd in ⊢ (??%?); normalize nodelta
1787(*          cases (update_clight_cminor_data_cm … frame_ … Hnew_inj)
1788          try assumption #frame_data'
1789          * * * * * #Halloctype_eq_frame_data #Hcl_env_eq_frame_data #Hcm_env_eq_frame_data
1790          #Hstackptr_eq_frame_data #Hcl_m_eq_frame_data #Hcm_m_eq_frame_data *)
1791     | 3: %{1} whd whd in ⊢ (??%?); normalize nodelta
1792     ]
1793    (* execute Cminor part *)
1794    [ 1: generalize in match (proj2 (present ????) (expr_vars ???) (proj1 ???));
1795    | 2: generalize in match (proj2 (present ????) (expr_vars ???) (proj1 ???));
1796    | 3: generalize in match (proj2 True ??); ]
1797    #Hexpr_vars_present_ef'
1798    [ 1,3:
1799       cases (eval_expr_sim … INV' … Halloc_hyp … Hcl_env_hyp … Hinjection … Hmatching) #Hsim_expr #_
1800       cut (expr_vars (typ_of_type (typeof func)) ef
1801             (λid:ident.λty:typ.present SymbolTag val cm_env id))
1802       [ 1,3: lapply Heq_ef_ef' lapply Hexpr_vars_ef lapply ef >Htyp_equality_ef
1803                #ef #Hexpr_vars_ef @(jmeq_absorb ?????) #Heq destruct (Heq)
1804                @Hexpr_vars_present_ef' ]
1805       #Hexpr_vars_present_ef
1806       lapply (Hsim_expr … Htranslate_ef … Hexpr_vars_present_ef … Hexec_func_ptr)
1807       -Hsim_expr * #cm_func_ptr_val * #Heval_func #Hvalue_eq_func
1808       cut (eval_expr cm_ge ASTptr ef' cm_env Hexpr_vars_present_ef'
1809             stackptr cm_m = OK (trace×val) 〈func_trace,cm_func_ptr_val〉)
1810       [ 1,3:
1811         lapply Heq_ef_ef' lapply Heval_func lapply Hexpr_vars_ef lapply Hexpr_vars_local_ef'
1812         lapply Hexpr_vars_present_ef lapply ef lapply Hexpr_vars_present_ef' lapply ef'
1813         <Htyp_equality_ef #ef' #HA #ef #HB #HC #HD #HE
1814         @(jmeq_absorb ?????) #Heq destruct (Heq) @HE ]
1815       -Heval_func #Heval_func >Heval_func
1816    | 2: (* treat case 2 as special, since the type differs slightly *)
1817       cases (eval_expr_sim … INV' … Halloc_hyp ? cm_env Hcl_env_hyp … Hnew_inj stackptr Hmatching)
1818       #Hsim_expr #_
1819       generalize in match (proj2 ???); #Hall_present
1820       generalize in match (proj1 ???); #Hret_present
1821       generalize in match (proj2 ???); #Hstore_inv
1822       generalize in match (conj ????); #Hstmt_inv
1823       cut (eval_expr cm_ge ? ef' cm_env ? stackptr cm_m =
1824            (eval_expr cm_ge ASTptr ef' cm_env ? stackptr cm_m)) try assumption try @refl
1825       #Heval_expr_rewrite >Heval_expr_rewrite -Heval_expr_rewrite
1826       lapply (Hsim_expr … Htranslate_ef … (Vptr func_ptr) func_trace ??)       
1827       try assumption
1828       [ lapply Hexpr_vars_present_ef' lapply Heq_ef_ef' lapply Hexpr_vars_ef lapply Hexpr_vars_local_ef'
1829         lapply ef >Htyp_equality_ef #ef #HA #HB @(jmeq_absorb ?????) #Heq destruct (Heq) #x @x ]
1830       * #cm_func_ptr_val * #Heval_func_cm #Hvalue_eq_func
1831       (* And some more shuffling types around to match the goal *)
1832       cut (eval_expr cm_ge ? ef' cm_env Hexpr_vars_present_ef' stackptr cm_mem_after_store = OK ? 〈func_trace,cm_func_ptr_val〉)
1833       [ lapply Heval_func_cm -Heval_func_cm
1834         generalize in ⊢ ((??(?????%??)?) → ?);
1835         lapply Heq_ef_ef' -Heq_ef_ef'
1836         lapply Hexpr_vars_ef -Hexpr_vars_ef
1837         lapply Hexpr_vars_local_ef' -Hexpr_vars_local_ef'
1838         lapply Hexpr_vars_present_ef'
1839         lapply ef >Htyp_equality_ef #ef0 #HA #HB #HC @(jmeq_absorb ?????)
1840         #Heq destruct (Heq) #H1 #H2 @H2 ]
1841       #Heval_cm_func >Heval_cm_func ]
1842    whd in match (m_bind ?????);
1843    lapply (trans_fn … INV' … Hfind_funct)
1844    * #tmp_u * #cminor_fundef * #Hglobals_fresh_for_tmp_u * #Hfundef_fresh_for_tmp_u *
1845    #Htranslate_fundef #Hfind_funct_cm
1846    lapply (value_eq_ptr_inversion … Hvalue_eq_func) * #cm_func_ptr * #Hcm_func_ptr
1847    whd in ⊢ ((??%?) → ?); cases func_ptr in Hfind_funct Hfind_funct_cm Hregion_is_code Hpoff_eq_zero;
1848    #cm_block #cm_off #Hfind_funct #Hfind_funct_cm #Hregion_is_code #Hpoff_eq_zero destruct (Hpoff_eq_zero)
1849    whd in ⊢ ((??%?) → ?);
1850    [ 1,2: >(HEm_fn_id … cm_block Hregion_is_code)
1851    | 3: >(HEm_fn_id … cm_block Hregion_is_code) ]
1852    normalize nodelta cases cm_func_ptr in Hcm_func_ptr; #cm_block' #cm_off'
1853    #Hcm_func_ptr #Heq destruct (Hcm_func_ptr Heq)
1854    [ 1,2: >addition_n_0 >mk_offset_offv_id
1855    | 3: ]
1856    >(find_funct_to_find_funct_id ???? Hfind_funct_cm)
1857    whd in match (opt_to_res ???); normalize nodelta
1858    (* Again, isolate cases by type similarity *)
1859    [ 1,2:
1860      cut (All (𝚺t:typ.CMexpr t)
1861            (λx:𝚺t:typ.expr t.(
1862              match x with
1863              [ mk_DPair ty e ⇒
1864               expr_vars ty e
1865                 (λid:ident
1866                  .λty0:typ.present SymbolTag val cm_env id)])) cm_args)
1867      [ 1: cases sInv * * normalize nodelta * #_ #_ #Hall #_ #_ @Hall
1868      | 3: cases sInv * * normalize nodelta * #_ #_ #Hall #_ #_ @Hall ]
1869      #Hall
1870      cases (eval_exprlist_simulation …  Halloc_hyp Hcl_env_hyp Hinjection Hmatching ???? Hexec_arglist Hargs_spec Hall)
1871      #cm_values * #Hcm_exec_list #Hcl_cm_values_eq >Hcm_exec_list
1872    | 3:
1873      (* Arrrgh *)
1874      lapply (eval_exprlist_simulation …  Halloc_hyp Hcl_env_hyp Hnew_inj ????? Hexec_arglist Hargs_spec ?)
1875      try assumption *
1876      #cm_values * #Hcm_exec_list #Hcl_cm_values_eq >Hcm_exec_list
1877    ]
1878    whd in match (m_bind ?????); normalize nodelta whd @conj
1879    [ 2,4,6: #Habsurd destruct (Habsurd) ]
1880    @conj
1881    [ 1,3,5: normalize try @refl
1882             >append_nil >append_nil @refl ]
1883    [ 1: generalize in match (proj1 ? (expr_vars ???) (proj1 ???)); #Hugly_pres
1884    | 2: generalize in match (proj1 ? (expr_vars ???) (proj1 ???)); #Hugly_pres
1885    | 3: ]
1886(*    [ 3: >addition_n_0 ]*)
1887    [ 1,2: (* no return or return to CM local variable *)
1888           @(CMR_call_nostore … tmp_u) try assumption
1889           [ 2,4: (* TODO: prove matching between CL and CM function ids *)
1890                  @cthulhu
1891           ]
1892           lapply Hfind_funct
1893           lapply Hfind_funct_cm
1894           lapply Htranslate_fundef
1895           lapply Hfundef_fresh_for_tmp_u
1896           lapply Hassert_type_eq
1897           lapply Htype_of_fundef
1898           lapply Hlookup
1899           cases cl_fundef
1900           [ 2,4: #id #typel #ty #HA #HB #HC #HD #HE #HF #HG @I
1901           | 1,3: #f #HA #HB #HC #HD #HE #HF #HG normalize nodelta
1902                  @conj try @conj try @conj try assumption ]
1903    | 3: (* type mismatch *)
1904         @(CMR_call_store … tmp_u) try assumption
1905         [ 2: (* TODO: prove matching between CL and CM function ids *)
1906              @cthulhu ]
1907         lapply Hfind_funct
1908         lapply Htranslate_fundef
1909         lapply Hfundef_fresh_for_tmp_u
1910         lapply Hassert_type_eq
1911         lapply Htype_of_fundef
1912         lapply Hlookup
1913         cases cl_fundef
1914         [ 2: #id #typel #ty #HA #HB #HC #f #HD #HE @I ]
1915         #f #HA #HB #HC #HD #HE #HF normalize nodelta @conj try @conj try @conj
1916         try assumption
1917    ]
1918| 1: (* Skip *)
1919    #cm_s #cl_k #cm_k #cm_st #cl_f #cm_f #rettyp
1920    #alloc_type #cl_env #cl_m #cm_env #cm_m #stackptr #stacksize
1921    (* introduce everything *)
1922    #fInv #sInv #kInv
1923    #Htarget_type #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function
1924    #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls
1925    #flag * * * * #Hstmt_inv #Hlabels_translated #Htmps_preserved
1926    #Hreturn_ok #Hlabel_wf generalize in match (conj ????); #Hugly
1927    whd in ⊢ ((??%?) → ?); #Heq_translate #Hlabel_inclusion
1928    #Hcont_rel
1929    lapply Heq_translate -Heq_translate
1930    lapply Hugly -Hugly
1931    lapply Hlabel_wf -Hlabel_wf
1932    lapply Hreturn_ok -Hreturn_ok
1933    lapply Htmps_preserved -Htmps_preserved
1934    lapply Hlabels_translated -Hlabels_translated
1935    lapply Hstmt_inv -Hstmt_inv
1936    lapply Htranslate_function -Htranslate_function
1937    lapply Hfresh_globals -Hfresh_globals
1938    lapply Hfresh_function -Hfresh_function
1939    lapply Htarget_type -Htarget_type
1940    lapply kInv -kInv
1941    lapply sInv -sInv
1942    lapply fInv -fInv
1943    lapply stmt_univ -stmt_univ
1944    lapply stmt_univ' -stmt_univ'
1945    lapply Hlabel_inclusion -Hlabel_inclusion
1946    (* case analysis on continuation *)
1947    inversion Hcont_rel
1948    [ (* Kstop continuation *)
1949      (* simplifying the goal using outcome of the inversion *)
1950      #kcl_ge #kcm_ge #kINV #kcl_f #kcm_f #ktarget_type #kcl_env #kcm_env #kalloc_type #kstack #Hkstack
1951      @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
1952      destruct (HA HB)
1953      @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
1954      destruct (HC HD HE)
1955      @(jmeq_absorb ?????) #HF @(jmeq_absorb ?????) #HG @(jmeq_absorb ?????) #HH
1956      @(jmeq_absorb ?????) #HI @(jmeq_absorb ?????) #HJ @(jmeq_absorb ?????) #HK @(jmeq_absorb ?????) #HL
1957      destruct (HF HG HH HI HJ HK HL) #_
1958      (* re-introduce everything *)
1959      #Hlabel_inclusion
1960      #stmt_univ' #stmt_univ #fInv #sInv #kInv #Htarget_type #Hfresh_function #Hfresh_globals
1961      #Htranslate_function #Hstmt_inv #Hlabels_translated #Htmps_preserved #Hreturn_ok #Hlabel_wf
1962      #Hugly generalize in match (conj ????); #Hugly'
1963      (* reduce statement translation function *)
1964      #Heq_translate
1965      (* In this simple case, trivial translation *)
1966      destruct (Heq_translate)
1967      #Em #Htmp_vars_well_allocated #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id #Hframe_spec
1968      @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
1969      destruct (HA HB)
1970      @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
1971      destruct (HC HD HE) #_
1972      (* unfold the clight execution *)
1973      #s2 #tr whd in ⊢ ((??%?) → ?);
1974      inversion (fn_return kcl_f) normalize nodelta
1975      [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
1976      | #structname #fieldspec | #unionname #fieldspec | #id ]
1977      #Hfn_return whd in ⊢ ((??%?) → ?); #Heq destruct (Heq)
1978      %{1} whd @conj try @conj try @refl
1979      [ 2: #Habsurd destruct (Habsurd) ]
1980      (* Use the memory injection stuff to produce a new memory injection *)
1981      cut (memory_inj Em (free_list cl_m (blocks_of_env kcl_env)) (free cm_m stackptr))
1982      [ @(freelist_memory_inj_m1_m2 Em cl_m cm_m
1983            (free_list cl_m (blocks_of_env kcl_env))
1984            (free cm_m stackptr) Hinjection (blocks_of_env kcl_env) stackptr ? (refl ??) (refl ??))
1985        assumption ]
1986      #Hinjection'
1987      @(CMR_return … Halloc_hyp Hcl_env_hyp … Hinjection') try assumption
1988      [ 2: #b lapply (Hmatching b)
1989           cases (lookup ?? kcl_env b) normalize nodelta
1990           [ 1: #H @H
1991           | 2: #b' cases (lookup ?? kalloc_type b) normalize nodelta
1992             [ 1: #H @H
1993             | 2: * #kalloc_type #ty normalize nodelta
1994                  cases kalloc_type normalize nodelta try //
1995                  #H #v #Hload_after_free @H
1996                  @(load_value_after_free_list_inversion … Hload_after_free)
1997             ]
1998           ]
1999      | 1: (* TODO: lemma *) @cthulhu
2000      ] 
2001    | (* Kseq *)
2002      #kcl_ge #kcm_ge #kINV #kcl_f #kcm_f #ktarget_type #kstack #kalloc_type #kcl_s #kcm_s
2003      #kcl_env #kcm_env #kcl_k' #kcm_k' #kstmt_univ #kstmt_univ' #klbl_univ #klbl_univ' #klbls #kflag
2004      * * * * #kHstmt_inv #kHlabels_translated #kHtmps_preserved
2005      #kHreturn_ok #kHlabel_wf #kHeq_translate #kHlabel_inclusion #kHcont_rel #_
2006      @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
2007      destruct (HA HB)
2008      @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
2009      destruct (HC HD HE)
2010      @(jmeq_absorb ?????) #HF @(jmeq_absorb ?????) #HG @(jmeq_absorb ?????) #HH @(jmeq_absorb ?????) #HI
2011      @(jmeq_absorb ?????) #HJ @(jmeq_absorb ?????) #HK @(jmeq_absorb ?????) #HL
2012      destruct (HF HG HH HI HJ HK HL) #_
2013      #Hlabel_inclusion
2014      #stmt_univ' #stmt_univ #fInv #sInv #kInv #Htarget_type #Hfresh_function #Hfresh_globals
2015      #Htranslate_function #Hstmt_inv #Hlabels_translated #Htmps_preserved #Hreturn_ok #Hlabel_wf
2016      #Hugly generalize in match (conj ????); #Hugly'
2017      (* In this simple case, trivial translation *)
2018      #Heq_translate destruct (Heq_translate) #Em
2019      #Htmp_vars_well_alloc #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id #Hframe_spec
2020      @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
2021      destruct (HA HB)
2022      @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
2023      destruct (HC HD HE) #_
2024      #s2 #tr whd in ⊢ ((??%?) → ?); #Heq destruct (Heq)
2025      %{1} whd @conj [ 2: #Habsurd destruct (Habsurd) ] @conj try @refl
2026      (* close simulation *)
2027      @(CMR_normal … kHeq_translate … Hinjection … Hmatching) try assumption
2028      (* TODO wrap this up properly, by adding some invariant or by threading stmt_univ' into the cont *)
2029      @cthulhu
2030      (* TODO: lemma allowing to prove this from [Htmp_vars_well_alloc] + tmp_gen inclusion *)
2031    | (* Kwhile continuation *)
2032      #kcl_ge #kcm_ge #kINV #kcl_f #kcm_f #ktarget_type #kstack #kalloc_type #kcl_env #kcm_env
2033      #kcl_k' #kcm_k' #ksz #ksg #kcl_ty #kcl_cond_desc #kcl_body #kHeq_ty #kcm_cond #kcm_body
2034      #kentry #kexit #kstmt_univ #kstmt_univ' #klbl_univ #klbl_univ' #klbl_univ''
2035      #klbls #kHtranslate_inv #kHexpr_vars #kHtranslate_expr #kfInv #kHlabel_declared
2036      #kHinv #kHmklabels #kHeq_translate #kHlabel_inclusion #kHfind_label
2037      (*     
2038      * * * * #kHentry_declared * * * *
2039      * * * #kHcond_vars_declared #Hnoise #Hnoise' #Hnoise''
2040      #kHcont_inv #kHmklabels #kHeq_translate
2041      #kHfind_label *) #kHcont_rel #_
2042      @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
2043      destruct (HA HB)
2044      @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
2045      destruct (HC HD HE)
2046      @(jmeq_absorb ?????) #HF @(jmeq_absorb ?????) #HG @(jmeq_absorb ?????) #HH
2047      @(jmeq_absorb ?????) #HI @(jmeq_absorb ?????) #HJ @(jmeq_absorb ?????) #HK
2048      @(jmeq_absorb ?????) #HL
2049      destruct (HF HG HH HI HJ HK HL) #_
2050      #Hlabel_inclusion
2051      #stmt_univ' #stmt_univ #fInv #sInv #kInv #Htarget_type #Hfresh_function #Hfresh_globals
2052      #Htranslate_function #Hstmt_inv #Hlabels_translated #Htmps_preserved #Hreturn_ok #Hlabel_wf
2053      #Hugly
2054      generalize in match (conj ????); #Hugly'
2055      (* In this simple case, trivial translation *)
2056      #Heq_translate destruct (Heq_translate)
2057      #Em #Htmp_vars_well_allocated #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching
2058      #HEm_fn_id #Hframe_spec
2059      @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
2060      destruct (HA HB)
2061      @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
2062      destruct (HC HD HE) #_ #s2 #tr
2063      whd in ⊢ ((??%?) → ?); #Heq destruct (Heq)
2064      lapply kHfind_label -kHfind_label
2065      generalize in ⊢ ((??(????%????)?) → ?); #Hlabel_exists
2066      generalize in ⊢ ((???(????%)) → ?); #Hmore_invariant
2067      #kHfind_label
2068      (* Kwhile cont case *)
2069      %{2} whd whd in ⊢ (??%?); normalize nodelta
2070      generalize in match (proj2 ???); #Hmore_noise
2071      generalize in match (proj1 ???); #Hmore_noise'
2072      >kHfind_label normalize nodelta
2073      whd @conj try @conj try @refl
2074      generalize in match (proj1 ???); #Hvars_present_in_ifthenelse
2075      generalize in match (proj2 ???); #Hcont_inv'
2076      [ 2: #Habsurd destruct (Habsurd) ]
2077      (* go to a special simulation state for while loops *)
2078      @(CMR_while … stacksize … Hcl_env_hyp … Hinjection … kHtranslate_expr … kHmklabels …  kHeq_translate)
2079      try assumption
2080      [ 1: @cthulhu
2081         (* TODO: lemma allowing to prove this from [Htmp_vars_well_alloc] + tmp_gen inclusion *)                 
2082         (* TODO wrap this up properly, by adding some invariant or by threading stmt_univ' into the cont *)
2083      | 2: cases Hmore_invariant * * #_ * * * * #_ #_ * #_ #_ * * #_ #H
2084           #_ #_ @H ]                 
2085    ]
2086| 2: (* Assign *)
2087     #cm_s #cl_k #cm_k #cm_st #cl_f #cm_f #rettyp
2088     #alloc_type #cl_env #cl_m #cm_env #cm_m #stackptr #stacksize
2089     (* introduce everything *)
2090     #fInv #sInv #kInv #Htarget_type #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function
2091     #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls
2092     #flag * * * * #Hstmt_inv_cm #Hlabels_translated #Htmps_preserved
2093     #Hreturn_ok #Hlabel_wf generalize in match (conj ????); #Hugly #Htranslate
2094     #Hlabel_inclusion #Hcont_rel
2095     #Em #Htmp_vars_well_allocated #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id #Hframe_spec
2096     @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
2097     destruct (HA HB)
2098     @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE #_
2099     destruct (HC HD HE)
2100     lapply Htranslate -Htranslate
2101     (* case-split on lhs in order to reduce lvalue production in Cminor *)
2102     cases lhs #lhs_ed #lhs_ty
2103     cases (expr_is_Evar_id_dec lhs_ed)
2104     [ 2: * #var_id #Hlhs_ed destruct (Hlhs_ed)
2105          #Htranslate_statement
2106          cases (bind_inversion ????? Htranslate_statement)
2107          * #cm_rhs #Hexpr_vars_rhs * #Htranslate_rhs #Htranslate_statement'
2108          cases (bind_inversion ????? Htranslate_statement') -Htranslate_statement'
2109          #lhs_dest * #Htranslate_lhs
2110          cases (bind2_eq_inversion ?????? Htranslate_lhs) -Htranslate_lhs
2111          #alloctype * #type_of_var * #Hlookup_var_success
2112          cases alloctype in Hlookup_var_success;
2113          normalize nodelta
2114          [ 1: (* Global *) #r
2115               #Hlookup_var_success whd in ⊢ ((???%) → ?); #Hlhs_dest_eq
2116               destruct (Hlhs_dest_eq) normalize nodelta
2117               generalize in match (conj ????); #Hinvariant
2118               cases (type_eq_dec ??)
2119               [ 2: #Hneq normalize nodelta whd in ⊢ ((??%%) → ?);
2120                    #Habsurd destruct (Habsurd) ]
2121               normalize nodelta whd in match (typeof ?); #Heq_cl_types
2122               whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
2123               #s2 #tr whd in ⊢ ((??%?) → ?); #Hstep
2124               cases (bindIO_inversion ??????? Hstep) -Hstep
2125               * * #cl_blo #cl_off #cl_tr * whd in ⊢ ((??%?) → ?);
2126               #Hexec_lvalue #Hstep
2127               lapply (res_to_io ????? Hexec_lvalue) -Hexec_lvalue #Hexec_lvalue
2128               cases (bindIO_inversion ??????? Hstep) -Hstep
2129               * #cl_rhs_val #cl_trace * #Hexec_rhs #Hstep
2130               cases (bindIO_inversion ??????? Hstep) -Hstep
2131               #cl_mem_after_store_lhs * #Hstore
2132               whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
2133               lapply (opt_to_io_Value ?????? Hstore) -Hstore #Hstore
2134               %{1} whd whd in ⊢ (??%?); normalize nodelta
2135               generalize in match (proj1 ???); whd in ⊢ (% → ?); *
2136               whd in match (eval_expr ???????);
2137               whd in match (eval_constant ????);
2138               whd in Hexec_lvalue:(??%?);
2139               <(eq_sym … INV' var_id)
2140               lapply (Hmatching … var_id)
2141               cases (lookup ?? cl_env var_id) in Hexec_lvalue; normalize nodelta
2142               [ 1: #Heq_find_sym cases (bind_inversion ????? Heq_find_sym) -Heq_find_sym
2143                    #global_b * #Hopt_to_res lapply (opt_to_res_inversion ???? Hopt_to_res) -Hopt_to_res
2144                    #Hfind_symbol >Hfind_symbol
2145                    normalize nodelta
2146                    whd in ⊢ ((???%) → ?); #Heq destruct (Heq) #Hembed_eq
2147                    whd in match (m_bind ?????);
2148                    cases (eval_expr_sim … Halloc_hyp … Hcl_env_hyp … Hinjection … Hmatching) #Hsim_expr #_
2149                    lapply (Hsim_expr … Htranslate_rhs … (proj2 ?? (proj1 ?? (proj1 ?? sInv))) Hexec_rhs)
2150                    * #cm_rhs_val generalize in match (proj2 ???);
2151                    #Hexpr_vars_rhs * #Heval_expr_rhs #Hvalue_eq_rhs >Heval_expr_rhs
2152                    whd in match (m_bind ?????); whd in Hstore:(??%?); whd in Hstore:(??%?);
2153                    cases (store_value_of_type_success_by_value lhs_ty cl_m
2154                                    cl_mem_after_store_lhs cl_blo zero_offset cl_rhs_val Hstore)
2155                    #Haccess_mode #Hstorev
2156                    lapply (storen_parallel_aux ??? Hinjection … Hvalue_eq_rhs … Hembed_eq ??? Hstorev)
2157                    * #cm_mem_after_store_lhs * #Hstoren #Hinj whd in Hstoren:(??%?);
2158                    whd in Hstoren:(??%?); whd in match (shift_offset ???);
2159                    >sign_ext_same_size >addition_n_0
2160                    whd in match (storev ????);
2161                    lapply Hstoren whd in match (offset_plus ??);
2162                    >addition_n_0 -Hstoren
2163                    >Heq_cl_types #Hstoren >Hstoren
2164                    whd in match (opt_to_res ???); normalize nodelta
2165                    whd @conj try @conj try @refl
2166                    [ 2: #Habsurd destruct (Habsurd) ]
2167                    generalize in match (conj ????);
2168                    #Hinv_vars
2169                    @CMR_normal try assumption
2170                    [ 2: @refl | 1,3,4: ]
2171                    [ 1: (* TODO: lemma on preservation of well-allocatedness through stores *) @cthulhu
2172                    | 2: (* TODO: lemma on preservation of memory matching through stores *) @cthulhu ]
2173               | 2: #b #Heq destruct (Heq)
2174                    lapply (opt_to_res_inversion ???? Hlookup_var_success) #Hlookup_aux
2175                    >Hlookup_aux normalize nodelta @False_ind ]
2176          | 2: (* Stack *)
2177               #n #Hlookup_var_success
2178               whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
2179               normalize nodelta whd in ⊢ ((???%) → ?);
2180               cases (type_eq_dec ??) normalize nodelta #Htype_eq
2181               [ 2: #Habsurd destruct (Habsurd) ]
2182               #Heq destruct (Heq) #s2 #tr #Hstep
2183               cases (bindIO_inversion ??????? Hstep)
2184               * * #cl_lvalue_block #cl_offset #cl_trace * #Hexec_lvalue
2185               lapply (res_to_io ????? Hexec_lvalue) -Hexec_lvalue
2186               whd in ⊢ ((??%?) → ?);
2187               @(match lookup ?? cl_env var_id
2188                 return λx. (lookup ?? cl_env var_id = x) → ?
2189                 with
2190                 [ None ⇒ λH. ?
2191                 | Some cl_addr ⇒ λH. ?
2192                 ] (refl ? (lookup ?? cl_env var_id)))
2193               normalize nodelta
2194               [ (* Contradiction: a stack-allocated variable was necessarily in the environment *)
2195                 @cthulhu
2196               | #Heq destruct (Heq)
2197                 lapply (Hmatching var_id) >H normalize nodelta
2198                 >(opt_to_res_inversion ???? Hlookup_var_success) normalize nodelta
2199                 #Hembedding_to_stack #Hexec_cl_rhs
2200                 cases (bindIO_inversion ??????? Hexec_cl_rhs) -Hexec_cl_rhs *
2201                 #cl_rhs_result #cl_rhs_trace * #Hcl_exec_expr_rhs #Hcl_exec_store
2202                 cases (bindIO_inversion ??????? Hcl_exec_store) -Hcl_exec_store #cl_mem_after_store
2203                 * #Hstore_value_of_type lapply (opt_to_io_Value ?????? Hstore_value_of_type)
2204                 -Hstore_value_of_type
2205                 #Hstore_value_of_type
2206                 whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
2207                 %{1} whd whd in ⊢ (??%?); normalize nodelta
2208                 whd in match (eval_expr ???????);
2209                 whd in match (eval_constant ????);
2210                 whd in match (m_bind ?????);
2211                 cases (eval_expr_sim … Halloc_hyp … Hcl_env_hyp … Hinjection … Hmatching) #Hsim_expr #_
2212                 lapply (Hsim_expr … Htranslate_rhs … (proj2 ?? (proj1 ?? (proj1 ?? sInv))) Hcl_exec_expr_rhs)
2213                 * #cm_rhs_val generalize in match (proj2 ???);
2214                 #Hexpr_vars_rhs * #Heval_expr_rhs #Hvalue_eq_rhs >Heval_expr_rhs
2215                 normalize nodelta -Hsim_expr
2216                 whd in match (shift_offset ???); >sign_ext_same_size
2217                 >commutative_addition_n >addition_n_0
2218                 whd in Hstore_value_of_type:(??%?);
2219                 cases (store_value_of_type_success_by_value ? cl_m
2220                                    cl_mem_after_store ?? cl_rhs_result Hstore_value_of_type)
2221                 whd in match (typeof ?) in ⊢ ((??%%) → (??%?) → ?);
2222                 #Haccess_mode #Hstorev -Hstore_value_of_type
2223                 lapply (storen_parallel_aux ??? Hinjection … Hvalue_eq_rhs … Hembedding_to_stack ??? Hstorev)
2224                 * #cm_mem_after_store_lhs * #Hstoren #Hinj whd in Hstoren:(??%?);
2225                 >offset_plus_0 in Hstoren; #Hstorev'
2226                 whd in match (storev ????);
2227                 lapply Htype_eq whd in match (typeof ?) in ⊢ ((??%?) → ?); #Htype_eq'
2228                 <Htype_eq' >Hstorev'
2229                 whd in match (m_bind ?????); normalize nodelta
2230                 whd @conj try @conj try @refl
2231                 [ 2: #Habsurd destruct (Habsurd) ]
2232                 @(CMR_normal … Halloc_hyp) try assumption
2233                 [ 2: @refl | 1,3,4,5: ]
2234                 [ 1: (* TODO: lemma on preservation of well-allocatedness through stores *) @cthulhu
2235                 | 2: (* TODO: lemma on preservation of memory matching through stores *) @cthulhu ]
2236               ]
2237          | 3: (* Local *)
2238               #Hlookup_var_success whd in ⊢ ((???%) → ?);
2239               #Heq destruct (Heq) normalize nodelta -Htranslate_statement
2240               #Htranslate
2241               cases (bind_inversion ????? Htranslate) -Htranslate
2242               * #cm_expr #Hexpr_vars * #Htyp_should_eq
2243               whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
2244               cases (typ_should_eq_inversion (typ_of_type (typeof rhs)) (typ_of_type type_of_var) … Htyp_should_eq)
2245               -Htyp_should_eq #Htyp_eq lapply Hexpr_vars_rhs lapply Hexpr_vars
2246               -Hlabel_wf -Hreturn_ok -Hlabels_translated -Hstmt_inv_cm lapply sInv               
2247               lapply cm_expr -cm_expr <Htyp_eq #cm_expr #sInv #Hexpr_vars #Hexpr_vars'
2248               @(jmeq_absorb ?????) #Heq destruct (Heq)
2249               #s2 #tr whd in ⊢ ((??%?) → ?); #Hcl_exec
2250               cases (bindIO_inversion ??????? Hcl_exec)
2251               * * #cl_blo #cl_off #cl_trace *
2252               whd in ⊢ ((???%) → ?);
2253               #Hexec_lvalue lapply (res_to_io ????? Hexec_lvalue) -Hexec_lvalue
2254               whd in ⊢ ((??%?) → ?);
2255               @(match lookup ?? cl_env var_id
2256                 return λx. (lookup ?? cl_env var_id = x) → ?
2257                 with
2258                 [ None ⇒ λH. ?
2259                 | Some cl_addr ⇒ λH. ?
2260                 ] (refl ? (lookup ?? cl_env var_id)))
2261               normalize nodelta
2262               [ (* Contradiction: a register-allocated variable was necessarily in the environment *)
2263                 @cthulhu
2264               | #Heq destruct (Heq)
2265                 lapply (Hmatching var_id) >H normalize nodelta
2266                 >(opt_to_res_inversion ???? Hlookup_var_success) normalize nodelta
2267                 #Hpresent_in_local #Hexec_cl_rhs
2268                 cases (bindIO_inversion ??????? Hexec_cl_rhs) -Hexec_cl_rhs *
2269                 #cl_rhs_result #cl_rhs_trace * #Hcl_exec_expr_rhs #Hcl_exec_store
2270                 cases (bindIO_inversion ??????? Hcl_exec_store) -Hcl_exec_store #cl_mem_after_store
2271                 * #Hstore_value_of_type lapply (opt_to_io_Value ?????? Hstore_value_of_type)
2272                 -Hstore_value_of_type #Hstore_value_of_type
2273                 whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
2274                 %{1} whd whd in ⊢ (??%?); normalize nodelta
2275                 cases (eval_expr_sim … Halloc_hyp … Hcl_env_hyp … Hinjection … Hmatching) #Hsim_expr #_
2276                 lapply (Hsim_expr … Htranslate_rhs … (proj2 ?? (proj1 ?? (proj1 ?? sInv))) Hcl_exec_expr_rhs)
2277                 * #cm_rhs_val generalize in match (proj2 ???);
2278                 #Hexpr_vars_rhs * #Heval_expr_rhs #Hvalue_eq_rhs >Heval_expr_rhs
2279                 normalize nodelta -Hsim_expr whd @conj try @conj try @refl
2280                 [ 2: #Habsurd destruct (Habsurd) ]
2281                 generalize in match (proj1 ???); #Hpresent
2282                 generalize in match (conj ????); #Hstmt_vars
2283                 @(CMR_normal … Halloc_hyp) try assumption
2284                 [ 2: @refl | *: ]
2285                 [ (* Need a particular kind of continuation relation *) @cthulhu
2286                 | (* Lemma on preservation of well-allocatedness through update_present *) @cthulhu
2287                 | (* Memory injection when writing in clight only, and block not mapped *) @cthulhu
2288                 | (* Memory matching through env update *) @cthulhu ]
2289               ]
2290          ]
2291     | 1: #Hnot_evar #Htranslate_statement
2292          cases (bind_inversion ????? Htranslate_statement) -Htranslate_statement
2293          * #cm_rhs #Hexpr_vars_rhs * #Htranslate_rhs #Htranslate_statement'
2294          cases (bind_inversion ????? Htranslate_statement') -Htranslate_statement' #dest
2295          lapply (translate_dest_not_Evar_id alloc_type ? lhs_ty Hnot_evar)
2296          #Htranslate_dest * #Htranslate_dest'
2297          >Htranslate_dest' in Htranslate_dest; #Haux lapply (sym_eq ??? Haux) -Haux #Haux
2298          cases (bind_inversion ????? Haux) -Haux
2299          * #translated_dest #Hexpr_vars_dest * #Htranslate_addr
2300          whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) normalize nodelta
2301          cases (type_eq_dec ??)
2302          [ 2: #Hneq normalize nodelta whd in ⊢ ((??%%) → ?);
2303               #Habsurd destruct (Habsurd) ]
2304          normalize nodelta whd in match (typeof ?); #Heq_cl_types
2305          whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
2306          #s2 #tr whd in ⊢ ((??%?) → ?); #Hstep
2307          cases (bindIO_inversion ??????? Hstep) -Hstep
2308          * * #cl_blo #cl_off #cl_tr * whd in ⊢ ((??%?) → ?);
2309          #Hexec_lvalue #Hstep
2310          lapply (translate_dest_MemDest_simulation …
2311                     INV' ???????? Halloc_hyp Hcl_env_hyp Hinjection Hmatching ??????
2312                     Htranslate_dest' Hexec_lvalue)
2313          [ 1: @(proj1 ?? (proj1 ?? (proj1 ?? sInv))) ]
2314          * #cm_val_dest * #Heval_cm_dest #Hvalue_eq_dest
2315          %{1} whd whd in ⊢ (??%?); normalize nodelta
2316          >Heval_cm_dest
2317          whd in match (m_bind ?????);
2318          cases (bindIO_inversion ??????? Hstep) -Hstep
2319          * #val #trace * #Hexec_expr #Hstep
2320          cases (bindIO_inversion ??????? Hstep) -Hstep
2321          #cl_mem_after_store * #Hopt_store
2322          whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
2323          lapply (opt_to_io_Value ?????? Hopt_store) -Hopt_store
2324          #Hstore_value_of_type whd in Hstore_value_of_type:(??%?);
2325          cases (eval_expr_sim … Halloc_hyp … Hcl_env_hyp … Hinjection … Hmatching) #Hsim_expr #_
2326          lapply (Hsim_expr … Htranslate_rhs … (proj2 ?? (proj1 ?? (proj1 ?? sInv))) Hexec_expr)
2327          * #cm_rhs_val generalize in match (proj2 ???);
2328          #Hexpr_vars_rhs * #Heval_expr_rhs #Hvalue_eq_rhs >Heval_expr_rhs
2329          normalize nodelta -Hsim_expr
2330          cases (store_value_of_type_success_by_value ? cl_m
2331                                    cl_mem_after_store ?? val Hstore_value_of_type)
2332          whd in match (typeof ?) in ⊢ ((??%%) → (??%?) → ?);
2333          #Haccess_mode #Hstorev -Hstore_value_of_type
2334          cases (value_eq_ptr_inversion … Hvalue_eq_dest) * #cm_blo #cm_off * #Hcm_val_dest destruct (Hcm_val_dest)
2335          whd in ⊢ ((??%?) → ?); #Hembed
2336          cases (some_inversion ????? Hembed) -Hembed
2337          * #cm_blo' #cm_off' * #Hembed normalize nodelta #Heq destruct (Heq)
2338          lapply (storen_parallel_aux ??? Hinjection … Hvalue_eq_rhs … Hembed ??? Hstorev)
2339          * #cm_mem_after_store_lhs * #Hstoren #Hinj whd in Hstoren:(??%?);
2340          whd in match (storev ????);
2341          lapply Hstoren
2342          (* make the types match *)
2343          generalize in match (conj ????); #Hstmt_vars' >Heq_cl_types
2344          #Hstoren >Hstoren
2345          whd in match (m_bind ?????); normalize nodelta whd @conj try @conj try @refl
2346          [ 2: #Habsurd destruct (Habsurd) ]
2347          @(CMR_normal … Halloc_hyp) try assumption
2348          [ 2: @refl | *: ]
2349          [ 1: (* lemma on well_allocated after CL and CM parallel writes *) @cthulhu
2350          | 2: (* memory matching *) @cthulhu ]
2351     ]
2352| 4: (* Seq *)
2353     #cm_s #cl_k #cm_k #cm_st #cl_f #cm_f #rettyp
2354     #alloc_type #cl_env #cl_m #cm_env #cm_m #stackptr #stacksize
2355     (* introduce everything *)
2356     #fInv #sInv #kInv #Htarget_type #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function
2357     #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls     
2358     #flag * * * * #Hstmt_inv_cm #Hlabels_translated #Htmps_preserved
2359     #Hreturn_ok #Hlabel_wf generalize in match (conj ????); #Hugly #Htranslate #Hlabel_inclusion
2360     #Hcont_rel
2361     #Em #Htmp_vars_well_allocated #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id #Hframe_spec
2362     @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
2363     destruct (HA HB)
2364     @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE #_
2365     destruct (HC HD HE)
2366     cases (bind_inversion ????? Htranslate) -Htranslate
2367     * * * #tmp_gen #labgen #cm_s1 #Htrans_inv * #Htrans_stm1 normalize nodelta
2368     #Htranslate cases (bind_inversion ????? Htranslate) -Htranslate     
2369     * * * #tmp_gen' #labgen' #cm_s2 #Htrans_inv' * #Htrans_stm2 normalize nodelta
2370     whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
2371     #s2 #tr whd in ⊢ ((??%?) → ?); #Heq destruct (Heq)
2372     %{1} whd @conj try @conj try @refl
2373     [ 2: #Habsurd destruct (Habsurd) ]
2374     @(CMR_normal … Htrans_stm1) try assumption
2375     [ 1: lapply Hlabel_inclusion
2376          @transitive_lset_inclusion @lset_inclusion_union %1
2377          @reflexive_lset_inclusion
2378     | 2: @(ClCm_cont_seq … Htrans_stm2)
2379          [ 1: lapply Hlabel_inclusion @transitive_lset_inclusion @lset_inclusion_union %2
2380               @reflexive_lset_inclusion
2381          | 2: assumption ]
2382     | 3: @cthulhu ]
2383| *: @cthulhu ]
2384| 2: (* Return state *)
2385  #cl_ge #cm_ge #INV' #cl_f #cm_f #alloc_type
2386  #cl_env #cl_m #cm_env #c_m #cm_st #stackptr #stacksize
2387  #stmt_univ #Em #Htmp_vars_wa #Hcharac #Hexec_alloc #Hinj #Hmatch #Hem_fn_id #Hframe
2388  @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
2389  destruct (HA HB)
2390  @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
2391  destruct (HC HD HE)
2392  #_
2393  whd in Hclight_normal:%;
2394  @False_ind @Hclight_normal
2395| 3: (* Call state, nostore *)
2396  #cl_ge #cm_ge #cl_f #cm_f #INV' #alloc_types
2397  #cl_env #cl_m #cm_env #cm_m #stackptr #u #cl_fundef #cm_fundef
2398  #Hglobals_fresh #Hfundef_fresh #rettyp #Hrettyp #cl_k #cm_k #fblock
2399  #Hcont_rel #cl_fun_id #cm_fun_id #Hfun_id_eq #cl_retval #cm_retval
2400  #sInv #fInv #kInv #cl_argvals #cm_argvals #cm_stack
2401  @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
2402  destruct (HA HB)
2403  @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
2404  destruct (HC HD HE)
2405  whd in Hclight_normal:%;
2406  @False_ind @Hclight_normal
2407| 4: (* Call state, store *)
2408  #cl_ge #cm_ge #cl_f #cm_f #INV' #alloc_types
2409  #cl_env #cl_m #cm_env #cm_m #cm_stack #stackptr #u #cl_fundef #cm_fundef
2410  #Hglobals_fresh #Hfundef_fresh #rettyp #Hrettyp #cl_k #cm_k #fblock
2411  #Hcont_rel #cl_fun_id #cm_fun_id #Hfun_id_eq
2412  #cl_rettyp #cl_retval #cl_retrace #cm_retval #cl_lhs #cm_lhs
2413  #Hinvariant_on_cm_lhs #Hexec_lvalue #Htranslate_dest #cm_ret_var
2414  #sInv #fInv #kInv #cl_argvals #cm_argvals #cm_stack
2415  @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
2416  destruct (HA HB)
2417  @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
2418  destruct (HC HD HE)
2419  whd in Hclight_normal:%;
2420  @False_ind @Hclight_normal
2421| 5: (* Intermediary While state *)
2422     (* ---------------------------------------------------------------------- *)
2423#cl_ge #cm_ge #INV'
2424#cl_f #cm_f #cl_env #cl_m #cm_env #cm_m #stackptr #stacksize #alloc_type
2425#cl_k #cm_k #sz #sg #cl_cond_ty #cl_cond_desc #cl_body #entry_label #exit_label #cm_cond #cm_body
2426#cm_stack #rettyp #kInv #fInv #sInv #Heq_ty #Hrettyp_eq #func_univ #Hfresh_globals #Hfresh_function
2427#Htranslate_function #Hcont_rel
2428#stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbl_univ'' #lbls
2429#Em #Htmp_vars_well_allocated #Halloc_hyp
2430#Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id #Hframe_spec #Hexpr_vars #Htranslate_expr
2431#Hentry_ex #Hexit_ex #Htranslate_inv #Hmk_labels #Htranslate_statement
2432#Hlabel_inclusion #Hlabel_exists #Hinv1 #Hinv2 #Hfind_label
2433@(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
2434destruct (HA HB)
2435@(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
2436destruct (HC HD HE) #_
2437#s2 #tr whd in ⊢ ((??%?) → ?); #Hstep
2438(* execute clight condition *)
2439cases (bindIO_inversion ??????? Hstep) -Hstep
2440* #cl_cond_val #cl_cond_trace * #Hcl_exec_cond #Hstep
2441cases (bindIO_inversion ??????? Hstep) -Hstep
2442#cl_cond_bool * #Hcl_bool_of_val whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
2443(* The numbers of steps to execute in Cminor depends on the outcome of the condition
2444   evaluation *)
2445cases cl_cond_bool in Hcl_bool_of_val;
2446[ (* cond = true: continue looping *)
2447  #Hcl_bool_of_val
2448  %{3} whd whd in ⊢ (??%?); normalize nodelta
2449  generalize in match (proj1 ???); #Hpresent_ifthenelse
2450  (* Exhibit simulation of condition evaluation *)
2451  lapply (eval_expr_sim … Halloc_hyp … Hcl_env_hyp … Hinjection … Hmatching) * #Hsim #_
2452  lapply (Hsim (Expr cl_cond_desc cl_cond_ty) (CMcast ?? cm_cond ?))
2453  [ >Heq_ty @refl ] -Hsim #Hsim
2454  lapply (Hsim … Hexpr_vars … Htranslate_expr ??? Hcl_exec_cond)
2455  [ lapply Hpresent_ifthenelse whd in ⊢ (% → ?); <Heq_ty >CMcast_identity #H @H ]
2456  * #cm_val_cond * #Hcm_eval_cond #Hvalue_eq -Hsim
2457  cut (eval_expr cm_ge (ASTint sz sg) cm_cond cm_env Hpresent_ifthenelse stackptr cm_m = OK ? 〈tr, cm_val_cond〉)
2458  [ lapply Hpresent_ifthenelse
2459    <(CMcast_identity (ASTint sz sg) cm_cond) #foo
2460    lapply Hcm_eval_cond whd in match (eq_ind_r ??????); normalize nodelta cases Heq_ty
2461    #H @H ]
2462  #Heval >Heval
2463  whd in match (m_bind ?????);
2464  >(eval_bool_of_val_to_Cminor … Hvalue_eq … Hcl_bool_of_val)
2465  normalize nodelta whd
2466  generalize in match (proj1 ???); #Hnoise'
2467  generalize in match (conj ????); #Hnoise'' @conj try @conj
2468  [ 3: #Habsurd destruct (Habsurd)
2469  | 1: normalize >append_nil @refl
2470  | 2: @(CMR_normal … Htranslate_function … Htranslate_statement) try assumption
2471       @(ClCm_cont_while … Htranslate_inv … Hmk_labels … Htranslate_statement) try assumption
2472  ]
2473| (* cond = false: stop looping *)
2474  #Hcl_bool_of_val
2475  %{4} whd whd in ⊢ (??%?); normalize nodelta
2476  generalize in match (proj1 ???); #Hpresent_ifthenelse
2477  (* Exhibit simulation of condition evaluation *)
2478  lapply (eval_expr_sim … Halloc_hyp … Hcl_env_hyp … Hinjection … Hmatching) * #Hsim #_
2479  lapply (Hsim (Expr cl_cond_desc cl_cond_ty) (CMcast ?? cm_cond ?))
2480  [ >Heq_ty @refl ] -Hsim #Hsim
2481  lapply (Hsim … Hexpr_vars … Htranslate_expr ??? Hcl_exec_cond)
2482  [ lapply Hpresent_ifthenelse whd in ⊢ (% → ?); <Heq_ty >CMcast_identity #H @H ]
2483  * #cm_val_cond * #Hcm_eval_cond #Hvalue_eq -Hsim
2484  cut (eval_expr cm_ge (ASTint sz sg) cm_cond cm_env Hpresent_ifthenelse stackptr cm_m = OK ? 〈tr, cm_val_cond〉)
2485  [ lapply Hpresent_ifthenelse
2486    <(CMcast_identity (ASTint sz sg) cm_cond) #foo
2487    lapply Hcm_eval_cond whd in match (eq_ind_r ??????); normalize nodelta cases Heq_ty
2488    #H @H ]
2489  #Heval >Heval
2490  whd in match (m_bind ?????);
2491  >(eval_bool_of_val_to_Cminor … Hvalue_eq … Hcl_bool_of_val)
2492  normalize nodelta whd
2493  generalize in match (proj1 ???); #Hnoise'
2494  generalize in match (proj2 ???); #Hnoise''
2495  generalize in match (conj ????); #Hnoise'''
2496  whd @conj try @conj
2497  [ 3: #Habsurd destruct (Habsurd)
2498  | 1: normalize >append_nil >append_nil @refl
2499  | 2: @(CMR_normal … DoNotConvert) try assumption
2500       [ 2: @refl | ]
2501  ]
2502]
2503
2504] qed.
2505
2506 
2507lemma clight_cminor_call_return :
2508  ∀g1, g2.
2509  ∀INV:clight_cminor_inv g1 g2.
2510  ∀s1,s1'.
2511  clight_cminor_rel g1 g2 INV s1 s1' →
2512  match Clight_classify s1 with
2513  [ cl_call ⇒ true
2514  | cl_return ⇒ true
2515  | _ ⇒ false ] →
2516  ∀s2,tr. step … (pcs_exec cl_pre) g1 s1 = Value … 〈tr, s2〉 →
2517  ∃m. after_n_steps m ?? (pcs_exec cm_pre) g2 s1' (λs.cminor_normal s) (λtr',s2'.
2518    tr = tr' ∧
2519    clight_cminor_rel g1 g2 INV s2 s2' ∧
2520      (m = 0 → lex_lt (measure_Clight s2) (measure_Clight s1))
2521  ).
2522#g1 #g2 #INV #s1 #s1' #Hstate_rel #Hclight_class
2523inversion Hstate_rel
2524[ 1: (* normal *)
2525  #cl_ge #cm_ge #INV' #cl_s
2526  #cm_s #cl_k #cm_k #cm_st #cl_f #cm_f #rettyp
2527  #alloc_type #cl_env #cl_m #cm_env #cm_m #stackptr #stacksize
2528  (* introduce everything *)
2529  #fInv #sInv #kInv #Htarget_type #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function
2530  #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls
2531  #flag  #Htrans_inv #Htrans_stmt #Hincl #HA #HB #HC
2532  #HE #HF #HG #HI #HJ #HK
2533  @(jmeq_absorb ?????) #H1 @(jmeq_absorb ?????) #H2
2534  destruct (H1 H2)
2535  @(jmeq_absorb ?????) #H3 @(jmeq_absorb ?????) #H4 @(jmeq_absorb ?????) #H5
2536  destruct (H3 H4 H5)
2537  @False_ind @Hclight_class
2538| 5:
2539  #cl_ge #cm_ge #INV' #cl_s
2540  #cm_s #cl_k #cm_k #cm_st #cl_f #cm_f #rettyp
2541  #alloc_type #cl_k #cm_k #sz #sg #cl_ty #cl_cond_desc #cl_body #entry_lab #exit_lab
2542  #cm_cond #cm_body #cm_stack #rettyp' #kInv
2543  (* introduce everything *)
2544  #fInv #sInv #kInv #Htarget_type #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function
2545  #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls
2546  #lbl1 #lbl2 #Em #Htmp_vars #Hcharac #Hexec #Hinj #Hmatching #Hem #Hframe #Hcond_tr
2547  #Htransl #Hex1 #Hex2 #Htransinv #Hmklabs #Htranstmt #Hincl
2548  #Hlabdecl #Hinv1 #Hinv2 #Hfindlab
2549  @(jmeq_absorb ?????) #H1 @(jmeq_absorb ?????) #H2
2550  destruct (H1 H2)
2551  @(jmeq_absorb ?????) #H3 @(jmeq_absorb ?????) #H4 @(jmeq_absorb ?????) #H5
2552  destruct (H3 H4 H5)
2553  @False_ind @Hclight_class
2554| *: @cthulhu
2555] qed.
2556
2557
2558(* TODO: adapt the following to the new goal shape. *)
2559(*
2560 
2561axiom clight_cminor_cost :
2562  ∀INV:clight_cminor_inv.
2563  ∀s1,s1',s2,tr.
2564  clight_cminor_rel INV s1 s1' →
2565  Clight_labelled s1 →
2566  after_n_steps 1 … clight_exec (ge_cl INV) s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) →
2567  after_n_steps 1 … Cminor_exec (ge_cm INV) s1' (λs.true) (λtr',s2'.
2568    tr = tr' ∧
2569    clight_cminor_rel INV s2 s2'
2570  ).
2571
2572axiom clight_cminor_init : ∀cl_program,cm_program,s,s'.
2573  clight_to_cminor cl_program = OK ? cm_program →
2574  make_initial_state ?? clight_fullexec cl_program = OK ? s →
2575  make_initial_state ?? Cminor_fullexec cm_program = OK ? s' →
2576  ∃INV. clight_cminor_rel INV s s'. *)
Note: See TracBrowser for help on using the repository browser.