source: src/Clight/toCminorCorrectness.ma @ 2825

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

Progress, Clight to Cminor

File size: 91.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
404(* relate Clight continuations and Cminor ones. *)
405inductive clight_cminor_cont_rel :
406  ∀cl_ge, cm_ge.
407  ∀INV:  clight_cminor_inv cl_ge cm_ge.     (* stuff on global variables and functions (matching between CL and CM) *)
408  ∀cl_f: function.                          (* current Clight function *)
409  internal_function →                       (* current Cminor function *)
410  cl_env →
411  cm_env →
412  var_types →
413  (*frame_data cl_f cl_ge cm_ge INV →*)         (* data for the current stack frame in CL and CM *)
414  option typ →                              (* optional target type - uniform over a given function *)
415  cl_cont →                                 (* CL cont *)
416  cm_cont →                                 (* CM cont *)
417  Prop ≝
418(* Stop continuation*) 
419| ClCm_cont_stop:
420  ∀cl_ge, cm_ge, INV, cl_f, cm_f, target_type.
421  ∀cl_env, cm_env, alloc_type.
422  clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type target_type Kstop Kend
423
424(* Seq continuation *)
425| ClCm_cont_seq:
426  ∀cl_ge, cm_ge, INV, cl_f, cm_f, target_type.
427  ∀alloc_type.
428  ∀cl_s: statement.
429  ∀cm_s: stmt.
430  ∀cl_env: cl_env.
431  ∀cm_env: cm_env.
432  ∀cl_k': cl_cont.
433  ∀cm_k': cm_cont.
434  ∀stmt_univ, stmt_univ'.
435  ∀lbl_univ, lbl_univ'.
436  ∀lbls.
437  ∀flag.
438  ∀Htranslate_inv.
439  translate_statement alloc_type stmt_univ lbl_univ lbls flag target_type cl_s = OK ? «〈stmt_univ',lbl_univ',cm_s〉, Htranslate_inv» →
440  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' →
441  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')
442
443(* While continuation *) 
444| ClCm_cont_while:
445  (* Inductive family parameters *)
446  ∀cl_ge, cm_ge, INV, cl_f, cm_f, target_type.
447
448  ∀alloc_type.
449  ∀cl_env.
450  ∀cm_env.
451
452  (* sub-continuations *)
453  ∀cl_k': cl_cont.
454  ∀cm_k': cm_cont.
455
456  (* elements of the source while statement *)
457  ∀sz,sg.
458  ∀cl_cond_desc.
459  ∀cl_body.
460
461  (* elements of the converted while statement *)
462  ∀cm_cond: CMexpr (ASTint sz sg).
463  ∀cm_body.
464  ∀entry,exit: identifier Label.
465 
466  (* universes used to generate fresh labels and variables *) 
467  ∀stmt_univ, stmt_univ'.
468  ∀lbl_univ, lbl_univ', lbl_univ''.
469  ∀lbls: lenv.
470  ∀Htranslate_inv.
471
472  (* relate CL and CM expressions *)
473  ∀Hexpr_vars.
474  translate_expr alloc_type (Expr cl_cond_desc (Tint sz sg)) = OK ? («cm_cond, Hexpr_vars») →
475
476  (* Parameters and results to find_label_always *)
477  ∀sInv: stmt_inv cm_f cm_env (f_body cm_f).
478  ∀Hinv.
479
480  (* Specify how the labels for the while-replacing gotos are produced *)
481  mklabels lbl_univ = 〈〈entry, exit〉, lbl_univ'〉 →
482  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» →
483  find_label_always entry (f_body cm_f) Kend (proj2 … (proj1 … (proj1 … Hinv))) cm_f cm_env sInv I =
484    «〈St_label entry
485          (St_seq
486            (St_ifthenelse ?? cm_cond (St_seq cm_body (St_goto entry)) St_skip)
487            (St_label exit St_skip)), cm_k'〉, Hinv» →
488  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' →
489  clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type target_type (Kwhile (Expr cl_cond_desc (Tint sz sg)) cl_body cl_k') (Kseq (St_goto entry) (Kseq (St_label exit St_skip) cm_k')).
490
491
492(* TODO XXX *)
493(* relation between placeholders for return values *)
494
495definition return_value_rel :
496  ∀cl_f, cl_ge, cm_ge.
497  ∀INV: clight_cminor_inv cl_ge cm_ge.
498  frame_data cl_f ?? INV →
499  option (block×offset×type) → option (ident×typ) → Prop ≝
500λcl_f, cl_ge, cm_ge, INV, data, opt1, opt2.
501match opt1 with
502[ None ⇒
503  match opt2 with
504  [ None ⇒ True
505  | _ ⇒ False ]
506| Some ptr ⇒
507  match opt2 with
508  [ Some id ⇒ True (* TODO, here. *)
509  | None ⇒ False
510  ]
511].
512
513(* Definition of the simulation relation on states. The orders of the parameters is dictated by
514 * the necessity of performing an inversion on the continuation sim relation without having to
515 * play the usual game of lapplying all previous dependent arguments.  *)
516inductive clight_cminor_rel : ∀cl_ge, cm_ge. clight_cminor_inv cl_ge cm_ge  → Clight_state → Cminor_state → Prop ≝
517| CMR_normal :
518  ∀cl_ge, cm_ge.
519  (* Relates globals to globals and functions to functions. *)
520  ∀INV:  clight_cminor_inv cl_ge cm_ge. 
521  (* ---- Statements ---- *)
522  ∀cl_s: statement.                                       (* Clight statement *) 
523  ∀cm_s: stmt.                                            (* Cminor statement *)
524  (* ---- Continuations ---- *)
525  ∀cl_k: cl_cont.                                      (* Clight continuation *)
526  ∀cm_k: cm_cont.                                      (* Cminor continuation *)
527  ∀cm_st: stack.                                              (* Cminor stack *) 
528  ∀cl_f: function.                               (* Clight enclosing function *)
529  ∀cm_f: internal_function.                             (* enclosing function *)
530  ∀rettyp.                                     (* return type of the function *)
531  ∀alloc_type.
532  ∀cl_env, cl_m.
533  ∀cm_env, cm_m.
534  ∀stackptr, stacksize. 
535  (* ---- Cminor invariants ---- *)
536  ∀fInv: stmt_inv cm_f cm_env (f_body cm_f).
537  ∀sInv: stmt_inv cm_f cm_env cm_s.
538  ∀kInv: cont_inv cm_f cm_env cm_k.
539  (* ---- relate return type variable to actual return type ---- *)
540  rettyp = opttyp_of_type (fn_return cl_f) →
541  (* ---- relate Clight and Cminor functions ---- *)
542  ∀func_univ: universe SymbolTag.
543  ∀Hfresh_globals: globals_fresh_for_univ ? (globals ?? INV) func_univ.
544  ∀Hfresh_function: fn_fresh_for_univ cl_f func_univ.
545  translate_function func_univ (globals ?? INV) cl_f Hfresh_globals Hfresh_function = OK ? cm_f →
546  (* ---- relate Clight and Cminor statements ---- *)
547  ∀stmt_univ,stmt_univ' : tmpgen alloc_type.
548  ∀lbl_univ,lbl_univ'   : labgen.
549  ∀lbls                 : lenv.
550  ∀flag                 : convert_flag.
551  ∀Htranslate_inv.
552  translate_statement alloc_type stmt_univ lbl_univ lbls flag rettyp cl_s = OK ? «〈stmt_univ',lbl_univ',cm_s〉, Htranslate_inv» → 
553  (* ---- relate Clight continuation to Cminor continuation ---- *)
554  clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type rettyp cl_k cm_k →
555  (* ---- state additional invariants ---- *) 
556  ∀Em: embedding.
557  tmp_vars_well_allocated alloc_type stmt_univ' cm_env cm_m cl_m Em →        (* locals are properly allocated *)
558  characterise_vars (globals ?? INV) cl_f = 〈alloc_type, stacksize〉 →        (* specify how alloc_type is built *)
559  (∃m,m'. exec_alloc_variables empty_env m (fn_params cl_f @ fn_vars cl_f) = 〈cl_env,m'〉) → (* spec. Clight env *)
560  memory_inj Em cl_m cm_m →                                                  (* memory injection *)
561  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 *)             
562  (∀b. block_region b = Code → Em b = Some ? 〈b, zero_offset〉) →             (* Force embedding to compute identity on functions *)
563  clight_cminor_rel cl_ge cm_ge INV
564    (ClState cl_f cl_s cl_k cl_env cl_m)
565    (CmState cm_f cm_s cm_env fInv sInv cm_m stackptr cm_k kInv cm_st)
566
567| CMR_return :
568  ∀cl_ge, cm_ge.
569  ∀INV: clight_cminor_inv cl_ge cm_ge.
570  (*  ∀frame_data: clight_cminor_data cl_f ?? INV.*)
571  ∀cl_m, cm_m.
572  ∀cm_st: stack.                                              (* Cminor stack *)
573  clight_cminor_rel cl_ge cm_ge INV
574    (ClReturnstate Vundef Kstop cl_m)
575    (CmReturnstate (None val) cm_m cm_st)
576
577| CMR_call_nostore :
578 (* call to a function with no return value, or which returns in a local variable in Cminor *)
579 ∀cl_ge, cm_ge, cl_f, cm_f.
580 ∀INV: clight_cminor_inv cl_ge cm_ge.
581 ∀alloc_type, cl_env, cl_m, cm_env, cm_m, stackptr.
582 (* TODO: put the actual invariants on memory and etc. here *)
583 ∀u: universe SymbolTag.
584 ∀cl_fundef, cm_fundef.
585 ∀Hglobals_fresh: globals_fresh_for_univ type (globals cl_ge cm_ge INV) u.
586 ∀Hfundef_fresh:  fd_fresh_for_univ cl_fundef u.
587 ∀rettyp. rettyp = opttyp_of_type (fn_return cl_f) →
588 ∀cl_k, cm_k.
589 ∀fblock.
590 match cl_fundef with
591 [ CL_Internal cl_function ⇒
592    find_funct clight_fundef cl_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? (CL_Internal cl_function) ∧
593    find_funct (fundef internal_function) cm_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? cm_fundef ∧
594    translate_fundef u (globals ?? INV) Hglobals_fresh cl_fundef Hfundef_fresh = OK ? cm_fundef ∧
595    clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type rettyp cl_k cm_k
596 | CL_External name argtypes rettype ⇒
597   True
598 ] →
599 ∀cl_fun_id, cm_fun_id.
600 cl_fun_id = cm_fun_id →
601 ∀cl_retval, cm_retval.
602 ∀sInv, fInv, kInv.
603 ∀cl_args_values, cm_args_values.
604 (* TODO: return_value_rel … INV frame_data cl_retval cm_retval →*)
605 (* TODO: add invariant All2 value_eq cl_args_values cm_args_values *)
606 ∀cm_stack.
607 clight_cminor_rel cl_ge cm_ge INV
608  (ClCallstate cl_fun_id
609   cl_fundef cl_args_values (Kcall cl_retval cl_f cl_env cl_k) cl_m)
610  (CmCallstate cm_fun_id cm_fundef
611   cm_args_values cm_m (Scall cm_retval cm_f stackptr cm_env sInv fInv cm_k kInv cm_stack))
612
613| CMR_call_store :
614 (* call to a function which returns to some location in memory in Cminor *)
615 ∀cl_ge, cm_ge, cl_f, cm_f.
616 ∀INV: clight_cminor_inv cl_ge cm_ge.
617 ∀alloc_type, cl_env, cl_m, cm_env, cm_m, stackptr.
618 (* TODO: put the actual invariants on memory and etc. here *)
619 ∀u: universe SymbolTag.
620 ∀cl_fundef, cm_fundef.
621 ∀Hglobals_fresh: globals_fresh_for_univ type (globals cl_ge cm_ge INV) u.
622 ∀Hfundef_fresh:  fd_fresh_for_univ cl_fundef u.
623 ∀rettyp. rettyp = opttyp_of_type (fn_return cl_f) →
624 ∀cl_k, cm_k.
625 ∀fblock.
626 match cl_fundef with
627 [ CL_Internal cl_function ⇒
628    find_funct clight_fundef cl_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? (CL_Internal cl_function) ∧
629    find_funct (fundef internal_function) cm_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? cm_fundef ∧
630    translate_fundef u (globals ?? INV) Hglobals_fresh cl_fundef Hfundef_fresh = OK ? cm_fundef ∧
631    clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type rettyp cl_k cm_k
632 | CL_External name argtypes rettype ⇒
633   True
634 ] →
635 ∀cl_fun_id, cm_fun_id.
636 cl_fun_id = cm_fun_id →
637 ∀cl_rettyp, cl_retval, cl_rettrace, cm_retval.
638 ∀cl_lhs, cm_lhs, Hinvariant_on_cm_lhs.
639 (* Explain where the lhs of the post-return assign comes from *)
640 exec_lvalue cl_ge cl_env cl_m cl_lhs = OK ? 〈cl_retval, cl_rettrace〉 →
641 translate_dest alloc_type cl_lhs = OK ? (MemDest ? «cm_lhs, Hinvariant_on_cm_lhs») →
642 (* TODO: Explain that the actual variable used to store the ret val is fresh and has the
643  * right type, etc *)
644 ∀cm_ret_var.
645 ∀sInv, fInv, kInv.
646 ∀cl_args_values, cm_args_values.
647 (* TODO: return_value_rel … INV frame_data cl_retval cm_retval →*)
648 (* TODO: add invariant All2 value_eq cl_args_values cm_args_values *)
649 ∀cm_stack.
650 clight_cminor_rel cl_ge cm_ge INV
651  (ClCallstate cl_fun_id
652   cl_fundef cl_args_values (Kcall (Some ? 〈cl_retval,cl_rettyp〉) cl_f cl_env cl_k) cl_m)
653  (CmCallstate cm_fun_id cm_fundef
654   cm_args_values cm_m (Scall cm_retval cm_f stackptr cm_env sInv fInv
655                          (Kseq (St_store (typ_of_type cl_rettyp) cm_lhs
656                                          (Id (typ_of_type cl_rettyp) cm_ret_var)) cm_k)
657                           kInv cm_stack))
658
659| CMR_while:
660 ∀cl_ge,cm_ge,INV,cl_f,cm_f.
661 ∀cl_env, cl_m, cm_env, cm_m, stackptr, stacksize.
662 ∀alloc_type.
663 ∀cl_k, cm_k. 
664 ∀sz,sg, cl_cond_desc.
665 ∀cl_body.
666 ∀entry_label, exit_label.
667 ∀cm_cond, cm_body.
668 ∀cm_stack.
669 ∀kInv: cont_inv cm_f cm_env cm_k.
670 ∀fInv: stmt_inv cm_f cm_env (f_body cm_f).
671 ∀sInv: stmt_inv cm_f cm_env
672           (St_label entry_label
673            (St_seq
674             (St_ifthenelse sz sg cm_cond (St_seq cm_body (St_goto entry_label)) St_skip)
675             (St_label exit_label St_skip))).             
676 ∀stmt_univ,stmt_univ',lbl_univ,lbl_univ',lbls.
677 (* Invariants *)
678 ∀Em: embedding.
679 tmp_vars_well_allocated alloc_type stmt_univ' cm_env cm_m cl_m Em →        (* locals are properly allocated *)
680 characterise_vars (globals ?? INV) cl_f = 〈alloc_type, stacksize〉 →        (* specify how alloc_type is built *)
681 (∃m,m'. exec_alloc_variables empty_env m (fn_params cl_f @ fn_vars cl_f) = 〈cl_env,m'〉) → (* spec. Clight env *)
682 memory_inj Em cl_m cm_m →                                                  (* memory injection *)
683 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 *)
684 (* Expression translation and related hypotheses *)
685 ∀Hcond_tr.  (* invariant after converting conditional expr *)
686 translate_expr alloc_type (Expr cl_cond_desc (Tint sz sg)) = OK ? «cm_cond, Hcond_tr » →
687 (* Statement translation *)
688 ∀target_type, Htranslate_inv.
689 translate_statement alloc_type stmt_univ lbl_univ lbls
690   (ConvertTo entry_label exit_label) target_type cl_body
691   = OK ? «〈stmt_univ',lbl_univ',cm_body〉,Htranslate_inv» →
692(* translate_statement alloc_type *)
693 (clight_cminor_rel cl_ge cm_ge INV
694  (ClState cl_f (Swhile (Expr cl_cond_desc (Tint sz sg)) cl_body) cl_k cl_env cl_m)
695  (CmState cm_f
696   (St_label entry_label
697    (St_seq
698     (St_ifthenelse sz sg cm_cond (St_seq cm_body (St_goto entry_label)) St_skip)
699     (St_label exit_label St_skip)))
700   cm_env fInv sInv cm_m stackptr cm_k kInv cm_stack)).
701
702definition clight_normal : Clight_state → bool ≝
703λs. match Clight_classify s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ].
704
705definition cminor_normal : Cminor_state → bool ≝
706λs. match Cminor_classify s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ].
707
708definition cl_pre : preclassified_system ≝
709  mk_preclassified_system
710    clight_fullexec
711    (λg. Clight_labelled)
712    (λg. Clight_classify)
713    (λx,y,H. an_identifier ? one). (* XXX TODO *)
714
715definition cm_pre : preclassified_system ≝
716  mk_preclassified_system
717    Cminor_fullexec
718    (λg. Cminor_labelled)
719    (λg. Cminor_classify)
720    (λx,y,H. an_identifier ? one).   (* XXX TODO *)
721
722(* --------------------------------------------------------------------------- *)
723(* General purpose auxilliary lemmas. *)
724(* --------------------------------------------------------------------------- *)
725
726lemma invert_assert :
727  ∀b. ∀P. assert b P → b = true ∧ P.
728* #P whd in ⊢ (% → ?); #H
729[ @conj try @refl @H
730| @False_ind @H ]
731qed.
732
733lemma res_to_io :
734  ∀A,B:Type[0]. ∀C.
735  ∀x: res A. ∀y.
736  match x with
737  [ OK v ⇒  Value B C ? v
738  | Error m ⇒ Wrong … m ] = return y →
739  x = OK ? y.
740#A #B #C *
741[ #x #y normalize nodelta whd in ⊢ ((???%) → ?); #Heq destruct (Heq) @refl
742| #err #y normalize nodelta whd in ⊢ ((???%) → ?); #Heq destruct (Heq) ]
743qed.
744
745lemma jmeq_absorb : ∀A:Type[0]. ∀a,b: A. ∀P:Prop. (a = b → P) → a ≃ b → P.
746#A #a #b #P #H #Heq lapply (jmeq_to_eq ??? Heq) #Heq' @H @Heq' qed.
747
748(* wrap up some trivial bit of reasoning to alleviate strange destruct behaviour *)
749lemma pair_eq_split :
750  ∀A,B:Type[0]. ∀a1,a2:A. ∀b1,b2:B.
751  〈a1,b1〉 = 〈a2, b2〉 →
752  a1 = a2 ∧ b1 = b2.
753#A #B #a1 #a2 #b1 #b2 #Heq destruct (Heq) @conj try @refl
754qed.
755
756lemma ok_eq_ok_destruct :
757  ∀A:Type[0]. ∀a,b:A. OK ? a = OK ? b → a = b.
758#H1 #H2 #H3 #H4 destruct @refl qed.
759
760lemma 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.
761#A #a #b #P #Ha #Hb #Heq destruct (Heq)
762@conj try %
763qed.
764
765(* inverting find_funct and find_funct_ptr *)
766lemma find_funct_inversion :
767  ∀F: Type[0]. ∀ge: genv_t F. ∀v: val. ∀res: F.
768      find_funct F ge v = Some ? res →
769      (∃ptr. v = Vptr ptr ∧
770            (poff ptr) = zero_offset ∧
771            block_region (pblock ptr) = Code ∧
772            (∃p. block_id (pblock ptr) = neg p ∧
773                 lookup_opt … p (functions … ge) = Some ? res)).
774#F #ge #v #res
775cases v
776[ | #sz #i | | #ptr ]
777whd in ⊢ ((??%?) → ?);
778#Heq destruct (Heq)
779%{ptr} @conj try @conj try @conj try @refl
780lapply Heq -Heq
781@(eq_offset_elim … (poff ptr) zero_offset) //
782normalize nodelta
783[ 1,3,5: #_ #Habsurd destruct (Habsurd) ]
784#Heq destruct (Heq)
785whd in ⊢ ((??%?) → ?);
786cases ptr #blo #off cases (block_region blo) normalize nodelta
787[ 1,3: #Habsurd destruct (Habsurd) ]
788[ // ]
789cases (block_id blo) normalize nodelta
790[ #Habsurd destruct (Habsurd) | #p #Habsurd destruct (Habsurd) ]
791#p #Hlookup %{p} @conj try @refl assumption
792qed.
793
794(* We should be able to prove that ty = ty' with some more hypotheses, if needed. *)
795lemma translate_dest_id_inversion :
796  ∀var_types, e, var_id, ty,H.
797   translate_dest var_types e = return IdDest var_types var_id ty H →
798   e = Expr (Evar var_id) (typeof e).
799@cthulhu
800(*   
801#vars #e #var_id #ty #H
802cases e #ed #ty'
803cases ed
804[ #sz #i | #id | #e1 | #e1 | #op #e1 |#op #e1 #e2 | #cast_ty #e1
805| #cond #iftrue #iffalse | #e1 #e2 | #e1 #e2 | #sizeofty | #e1 #field | #cost #e1 ]
806whd in ⊢ ((??%%) → ?);
807#Heq
808[ 1,4,5,6,7,8,9,10,11,13: destruct (Heq)
809| 3,12: cases (bind_inversion ????? Heq) * #H1 #H2 #H3 cases H3
810        #_ whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) ]
811lapply Heq -Heq
812change with (bind2_eq ????? ) in ⊢ ((??%?) → ?); #Heq
813cases (bind2_eq_inversion ?????? Heq)
814#alloctype
815(* * #alloctype *) * #typ' *
816cases alloctype
817[ #r | #n | ] normalize nodelta #Hlookup'
818[ 1,2: whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) ]
819whd in ⊢ ((??%%) → ?); #Heq' destruct (Heq')
820@refl*)
821qed.
822
823
824(* Note: duplicate in switchRemoval.ma *)
825lemma fresh_elim : ∀u. ∃fv',u'. fresh SymbolTag u = 〈fv', u'〉. #u /3 by ex_intro/ qed.
826
827lemma breakup_dependent_match_on_pairs :
828 ∀A,B,C: Type[0].
829 ∀term: A × B.
830 ∀F: ∀x,y. 〈x, y〉 = term → C.
831 ∀z:C.
832 match term
833 return λx.x = term → ? with
834 [ mk_Prod x y ⇒ λEq. F x y Eq ] (refl ? term) = z →
835 ∃xa,xb,H. term = 〈xa, xb〉 ∧
836           F xa xb H = z.
837#A #B #C * #xa #xb #F #z normalize nodelta #H %{xa} %{xb} %{(refl ??)} @conj try @conj
838// qed.
839
840(* --------------------------------------------------------------------------- *)
841(* Extending simulation results on expressions to particular cases             *)
842(* --------------------------------------------------------------------------- *)
843
844lemma translate_expr_sigma_welltyped : ∀vars, cl_expr, cm_expr.
845  translate_expr_sigma vars cl_expr = OK ? cm_expr →
846  dpi1 ?? (pi1 ?? cm_expr) = typ_of_type (typeof cl_expr).
847#vars #cl_expr * * #typ #cm_expr normalize nodelta #Hexpr_vars
848whd in ⊢ ((??%?) → ?); #H
849cases (bind_inversion ????? H) -H * #cm_expr' #Hexpr_vars' *
850#Htranslate_expr
851whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) @refl
852qed.
853
854lemma translate_exprlist_sigma_welltyped :
855  ∀vars, cl_exprs, cm_exprs.
856  mmap_sigma ??? (translate_expr_sigma vars) cl_exprs = OK ? cm_exprs →
857  All2 ?? (λcl, cm. dpi1 ?? cm = typ_of_type (typeof cl)) cl_exprs (pi1 ?? cm_exprs).
858#vars #cl_exprs
859elim cl_exprs
860[ * #cm_exprs #Hall whd in ⊢ ((??%?) → ?); #Heq destruct (Heq) @I
861| #hd #tl #Hind * #cm_exprs #Hall #H
862  cases (bind_inversion ????? H) -H
863  * * #cm_typ #cm_expr normalize nodelta
864  #Hexpr_vars_cm * #Htranslate_hd
865  lapply (translate_expr_sigma_welltyped … Htranslate_hd)
866  #Heq_cm_typ #H
867  cases (bind_inversion ????? H) -H
868  #cm_tail lapply (Hind cm_tail) cases cm_tail
869  #cm_tail_expr #Hall_tail -Hind #Hind * #Heq_cm_tail normalize nodelta
870   whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) whd @conj
871   [ @Heq_cm_typ
872   | @Hind assumption ]
873] qed.
874
875lemma translate_dest_MemDest_simulation :
876  ∀cl_f  : function.
877  ∀cl_ge : genv_t clight_fundef.
878  ∀cm_ge : genv_t (fundef internal_function).
879  ∀INV   : clight_cminor_inv cl_ge cm_ge.
880  ∀alloc_type. 
881  ∀cl_env, cl_m, cm_env, cm_m, stackptr.
882  ∀Em.
883  ∀stacksize     : ℕ. 
884  ∀alloc_hyp     : characterise_vars (globals ?? INV) cl_f = 〈alloc_type, stacksize〉.
885  ∀cl_cm_env_hyp : ∃m,m'. exec_alloc_variables empty_env m (fn_params cl_f @ fn_vars cl_f) = 〈cl_env,m'〉.
886  ∀injection     : memory_inj Em cl_m cm_m.
887  ∀matching      : memory_matching Em cl_ge cm_ge cl_m cm_m cl_env cm_env INV stackptr alloc_type.
888  (* decorrelate goal from input using some eqs *)
889  ∀cl_expr. ∀cm_expr.
890  ∀cl_block, cl_offset, trace.
891  ∀Hyp_present. 
892     translate_dest alloc_type cl_expr = OK ? (MemDest ? cm_expr) →
893     exec_lvalue cl_ge cl_env cl_m cl_expr = OK ? 〈〈cl_block, cl_offset〉, trace〉 →
894     ∃cm_val. eval_expr cm_ge ASTptr cm_expr cm_env Hyp_present stackptr cm_m = OK ? 〈trace, cm_val〉 ∧
895              value_eq Em (Vptr (mk_pointer cl_block cl_offset)) cm_val.     
896#cl_f #cl_ge #cm_ge #INV #alloc_type
897#cl_env #cl_m #cm_env #cm_m #stackptr #Em #stacksize #alloc_hyp #cl_env_hyp #injection #matching
898#cl_expr * #cm_expr #Hexpr_vars #cl_block #cl_offset #trace #Hyp_present
899whd in match (translate_dest ??); cases cl_expr #cl_desc #cl_typ normalize nodelta
900cases cl_desc normalize nodelta
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 ]
903#Htranslate
904[ 2:
905| *: cases (bind_inversion ????? Htranslate) -Htranslate * #cm_expr' #Hexpr_vars' *
906     #Htranslate_addr
907     whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) #Hexec_lvalue
908     cases (eval_expr_sim cl_ge cm_ge INV cl_f alloc_type stacksize alloc_hyp … cl_env_hyp … injection … matching)
909     #_ #Hsim
910     @(Hsim ??? Hexpr_vars … Htranslate_addr ??? ? Hexec_lvalue) ]
911cases (bind2_eq_inversion ?????? Htranslate) -Htranslate *
912[ #r | #n | ]
913* #cl_type * #Heq_lookup normalize nodelta
914whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
915whd in ⊢ ((??%?) → ?);
916@(match lookup SymbolTag block cl_env id
917  return λx. (lookup SymbolTag block cl_env id = x) → ?
918  with
919  [ None ⇒ ?
920  | Some loc ⇒ ?
921  ] (refl ? (lookup SymbolTag block cl_env id ))) normalize nodelta
922#Hlookup_eq
923[ 2,4: #Heq destruct (Heq) whd in match (eval_expr ???????);
924  [ 2: %{(Vptr (mk_pointer stackptr (shift_offset (bitsize_of_intsize I16) zero_offset (repr I16 n))))}
925       @conj try @refl
926       lapply (matching id)
927       >Hlookup_eq normalize nodelta
928       >(opt_to_res_inversion ???? Heq_lookup) normalize nodelta
929       #Hembed %4 whd in ⊢ (??%?); >Hembed @refl
930  | 1: whd in match (eval_constant ????);
931       lapply (matching id)
932       >Hlookup_eq normalize nodelta 
933       >(opt_to_res_inversion ???? Heq_lookup) normalize nodelta
934       @False_ind
935  ]
936| 1,3: #Hfind_symbol
937  cases (bind_inversion ????? Hfind_symbol) -Hfind_symbol #block *
938  whd in ⊢ ((??%%) → ?); #Hfind_symbol
939  lapply (opt_to_res_inversion ???? Hfind_symbol) #Hfind_symbol_eq
940  whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
941  whd in match (eval_expr ???????);
942  whd in match (eval_constant ????);
943  lapply (matching id)
944  [ >Hlookup_eq normalize nodelta >Hfind_symbol_eq normalize nodelta
945    #Hembed
946    <(eq_sym … INV id) >Hfind_symbol_eq normalize nodelta
947     %{(Vptr
948         (mk_pointer cl_block
949          (shift_offset (bitsize_of_intsize I16) zero_offset (repr I16 O))))}
950     @conj try @refl
951     %4 whd in ⊢ (??%?); >Hembed try @refl
952  | (* A stack variable is not in the local environment but in the global one. *)
953    (* we have a contradiction somewhere in the context *)
954    lapply (variable_not_in_env_but_in_vartypes_is_global ???????
955              cl_env_hyp alloc_hyp Hlookup_eq … Heq_lookup)
956    *  #r #Habsurd destruct (Habsurd)
957  ]
958] qed.
959 
960(* lift simulation result to eval_exprlist *)
961lemma eval_exprlist_simulation :
962  ∀cl_f.
963  ∀cl_ge : genv_t clight_fundef.
964  ∀cm_ge : genv_t (fundef internal_function).
965  ∀INV   : clight_cminor_inv cl_ge cm_ge.
966  ∀alloc_type. 
967  ∀cl_env, cl_m, cm_env, cm_m, stackptr.
968  ∀Em.
969  ∀stacksize     : ℕ. 
970  ∀alloc_hyp     : characterise_vars (globals ?? INV) cl_f = 〈alloc_type, stacksize〉.
971  ∀cl_env_hyp : ∃m,m'. exec_alloc_variables empty_env m (fn_params cl_f @ fn_vars cl_f) = 〈cl_env,m'〉.
972  ∀injection     : memory_inj Em cl_m cm_m.
973  ∀matching      : memory_matching Em cl_ge cm_ge cl_m cm_m cl_env cm_env INV stackptr alloc_type.
974  ∀cl_exprs,cm_exprs.
975  ∀cl_results,trace.
976  exec_exprlist cl_ge cl_env cl_m cl_exprs = OK ? 〈cl_results, trace〉 →
977  mmap_sigma ??? (translate_expr_sigma alloc_type) cl_exprs = OK ? cm_exprs →
978  ∀H:All ? (λx:𝚺t:typ.expr t.
979             match x with
980             [ mk_DPair ty e ⇒
981                    (expr_vars ty e
982                     (λid:ident.λty:typ.present SymbolTag val cm_env id)) ]) cm_exprs.
983  ∃cm_results.
984  trace_map_inv … (λe. match e return λe.
985                         match e with
986                         [ mk_DPair _ _ ⇒ ? ] → ?
987                       with
988                       [ mk_DPair ty e ⇒ λp. eval_expr cm_ge ? e cm_env p stackptr cm_m ]) cm_exprs H = OK ? 〈trace, cm_results〉 ∧
989  All2 ?? (λcl_val, cm_val. value_eq Em cl_val cm_val) cl_results cm_results.
990#f #cl_ge #cm_ge #INV
991#alloc_type #cl_env #cl_m #cm_env #cm_m #stackptr #Em #stacksize #alloc_hyp #cl_env_hyp #injection #matching
992#cl_exprs
993elim cl_exprs
994[ #cm_exprs #cl_results #trace
995  whd in ⊢ ((??%?) → ?);
996  #Heq destruct (Heq)
997  whd in ⊢ ((??%?) → ?);
998  #Heq destruct (Heq) #H %{[]}
999  @conj try @refl try @I
1000| #cl_hd #cl_tl #Hind #cm_exprs #cl_results #trace
1001  #Heq cases (bind_inversion ????? Heq) -Heq
1002  * #hd_val #hd_trace * #Hexec_expr_cl
1003  #Heq cases (bind_inversion ????? Heq) -Heq 
1004  * #cl_tl_vals #cl_tl_trace * #Hexec_expr_tl
1005  whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
1006  #Htranslate
1007  lapply (translate_exprlist_sigma_welltyped … Htranslate)
1008  #Htype_eq_all #Hall
1009  cases (bind_inversion ????? Htranslate) -Htranslate
1010  * * #cmtype #cmexpr normalize nodelta
1011  #Hexpr_vars_local_cm * #Htranslate_expr_sigma #Htranslate
1012  cases (bind_inversion ????? Htranslate) -Htranslate
1013  * #cm_tail #Hexpr_vars_local_cm_tail * #Htranslate_tail
1014  normalize nodelta
1015  whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
1016  cases Htype_eq_all -Htype_eq_all #Hcm_type_eq #Htype_eq_all
1017  lapply (Hind cm_tail cl_tl_vals cl_tl_trace Hexec_expr_tl)
1018  [ assumption ] -Hind #Hind
1019  lapply (Hind Htranslate_tail (proj2 ?? Hall)) -Hind
1020  * #cm_results_tl * #Hcm_exec_tl #Hvalues_eq_tl
1021  cases (eval_expr_sim cl_ge cm_ge INV f alloc_type stacksize alloc_hyp ?? cl_env_hyp ?? Em injection stackptr matching)
1022  #Hsim #_
1023  cases (bind_inversion ????? Htranslate_expr_sigma)
1024  * #cmexpr' #Hexpr_vars_local_cm' * #Htranslate
1025  whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
1026  lapply (Hsim cl_hd cmexpr ??????) -Hsim try assumption
1027  [ @(proj1 ?? Hall) ]
1028  * #cm_val_hd * #Heval_expr_cm #Hvalue_eq     
1029  %{(cm_val_hd :: cm_results_tl)} @conj
1030  [ 2: @conj try assumption
1031  | 1: whd in ⊢ (??%?); normalize nodelta >Heval_expr_cm
1032       normalize nodelta >Hcm_exec_tl @refl
1033  ]
1034] qed.
1035
1036(* --------------------------------------------------------------------------- *)
1037(* Putting the memory injection at work.                                       *)
1038(* --------------------------------------------------------------------------- *)
1039
1040(* A) Non-interference of local variables with memory injections  *)
1041
1042(* Needed property:
1043 * A local variable allocated via the temporary variable generator should not interfere
1044 * with the memory injection. In particular, we need to show that:
1045 * 1) we can successfuly store stuff of the right type inside (where the type is specified
1046 *    at generation time, and should be in the current context)
1047 * 2) after the store, we can build a consistent memory state and more generally, a
1048 *    correct [clight_cminor_data] invariant record. Cf. toCminorCorrectnessExpr.ma
1049 *)
1050 
1051(* A.1) memory matchings survives memory injection *)
1052
1053lemma offset_plus_0' : ∀o:offset. offset_plus zero_offset o = o.
1054#o cases o #b >offset_plus_0 @refl
1055qed.
1056
1057(*
1058lemma store_value_of_type_memory_matching_to_matching : 
1059  ∀cl_ge, cm_ge, cl_en, cm_en, INV, sp, vars, cl_m, cl_m',cm_m,cm_m'.
1060  ∀E: embedding.
1061  ∀blo, blo', delta, off.
1062  E blo = Some ? 〈blo', delta〉 →
1063  ∀cl_val, cm_val, ty.
1064  value_eq E cl_val cm_val →
1065  storen cl_m (mk_pointer blo off) (fe_to_be_values ty cl_val) = Some ? cl_m' →
1066  storen cm_m (mk_pointer blo (offset_plus off delta)) (fe_to_be_values ty cm_val) = Some ? cm_m' →
1067  (lookup' vars var_id = OK (var_type×type) 〈Global r,type_of_var〉)
1068  memory_inj E cl_m' cm_m' →
1069  memory_matching E cl_ge cm_ge cl_m cm_m cl_en cm_en INV sp vars →
1070  memory_matching E cl_ge cm_ge cl_m' cm_m' cl_en cm_en INV sp vars.
1071#cl_ge #cm_ge #cl_en #cm_en #INV #sp #vars #cl_m #cl_m' #cm_m #cm_m' #E
1072#blo #blo' #delta #off #Hembed #cl_val #cm_val #ty #Hvalue_eq #Hstoren_cl #Hstoren_cm
1073#Hinj #Hmatching #id
1074lapply (Hmatching id)
1075cases (lookup ?? cl_en id) normalize nodelta
1076[ 1: #H @H
1077| 2: #bl cases (lookup ?? vars id) normalize nodelta
1078  [ 1: #H @H
1079  | 2: * #var_type #cl_type normalize nodelta
1080       cases var_type normalize nodelta
1081       [ #r #H @H
1082       | #b #H @H
1083       | #H #v lapply H -H
1084         @(eq_block_elim … bl blo)
1085         [ #Heq destruct (Heq)
1086           @(eq_offset_elim … off zero_offset)
1087           [ (* We actually load exactly where we wrote, but with a potentially different type. *)
1088             #Heq destruct (Heq) #H
1089       ]
1090  ]
1091] qed.*)
1092
1093
1094lemma alloc_tmp_in_genlist :
1095  ∀vartypes. ∀g1, g2, g3.
1096  ∀id1, ty1, id2, ty2.
1097  alloc_tmp vartypes ty1 g1 = 〈id1, g2〉 →
1098  alloc_tmp vartypes ty2 g2 = 〈id2, g3〉 →
1099  Exists (identifier SymbolTag×type)
1100   (λx:identifier SymbolTag×type.x=〈id2,ty2〉) (tmp_env ? g3).
1101#vartypes #g1 #g2 #g3
1102#id1 #ty1 #id2 #ty2 #Halloc1 #Halloc2
1103lapply (breakup_dependent_match_on_pairs ?????? Halloc1) * #id1' * #u' * #Hfg1
1104* #Hfresh_eq generalize in match (fresh_map_add ????????); #ugly
1105generalize in ⊢ ((??(????(?????%))?) → ?); #ugly2
1106#Heq destruct (Heq)
1107lapply (breakup_dependent_match_on_pairs ?????? Halloc2) * #id2' * #u'' * #Hfg2
1108* #Hfresh_eq' generalize in match (fresh_map_add ????????); #ugly'
1109generalize in ⊢ ((??(????(?????%))?) → ?); #ugly2'
1110#Heq destruct (Heq) %1 @refl
1111qed. (* this last lemma has to be refitted. *)
1112
1113(* This, to say the least, is not pretty. Whenever we update the memory, we have to perform
1114 * a kind of functional record update on the frame_data. But of course, we also need equations
1115 * relating the old and new frame data. *)
1116(*
1117lemma update_clight_cminor_data_cm :
1118  ∀f, cl_ge, cm_ge, INV.
1119  ∀frame_data: clight_cminor_data f cl_ge cm_ge INV.
1120  ∀cl_m_v.
1121  ∀new_cm_mem.
1122  cl_m_v = cl_m … frame_data →
1123  ∀new_inj: memory_inj (Em … frame_data) cl_m_v new_cm_mem.
1124  ∃data:clight_cminor_data f cl_ge cm_ge INV.
1125          alloc_type … frame_data = alloc_type … data ∧
1126          cl_env … frame_data = cl_env … data ∧
1127          cm_env … frame_data = cm_env … data ∧
1128          stackptr … frame_data = stackptr … data ∧
1129          cl_m … frame_data = cl_m … data ∧
1130          new_cm_mem = (cm_m … data).
1131#f #cl_ge #cm_ge #INV #frame_data #cl_m_v #new_cm_mem #H destruct (H) #Hinj
1132%{(mk_clight_cminor_data ????
1133       (alloc_type … frame_data)
1134       (stacksize … frame_data)
1135       (alloc_hyp … frame_data)
1136       (cl_env … frame_data)
1137       (cm_env … frame_data)
1138       (cl_env_hyp … frame_data)
1139       (cl_m … frame_data)
1140       new_cm_mem
1141       (Em … frame_data)
1142       Hinj
1143       (stackptr … frame_data)
1144       (matching … frame_data)
1145       (Em_fn_id … frame_data))}
1146@conj try @conj try @conj try @conj try @conj try @refl
1147qed.*)
1148
1149(* Same thing, this time update both CL and CM memory. Here we provide a proof
1150 * that the data in local env is not touched. *)
1151(*
1152lemma update_clight_cminor_data_cl_cm_global :
1153  ∀f, cl_ge, cm_ge, INV.
1154  ∀frame_data: clight_cminor_data f cl_ge cm_ge INV.
1155  ∀new_cl_mem, new_cm_mem.
1156  ∀new_inj: memory_inj (Em … frame_data) new_cl_mem new_cm_mem. 
1157  (∀id, b, cl_type.
1158   lookup ?? (cl_env … frame_data) id = Some ? b →
1159   lookup ?? (alloc_type … frame_data) id = Some ? 〈Local, cl_type〉 →
1160   load_value_of_type cl_type (cl_m … frame_data) b zero_offset =
1161   load_value_of_type cl_type new_cl_mem b zero_offset) → 
1162  ∃data:clight_cminor_data f cl_ge cm_ge INV.
1163        alloc_type … frame_data = alloc_type … data ∧
1164        cl_env … frame_data = cl_env … data ∧
1165        cm_env … frame_data = cm_env … data ∧
1166        stackptr … frame_data = stackptr … data ∧
1167        new_cl_mem = (cl_m … data) ∧
1168        new_cm_mem = (cm_m … data).
1169#f #cl_ge #cm_ge #INV #frame_data #new_cl_mem #new_cm_mem #Hinj #Haux
1170%{(mk_clight_cminor_data ????
1171       (alloc_type … frame_data)
1172       (stacksize … frame_data)
1173       (alloc_hyp … frame_data)
1174       (cl_env … frame_data)
1175       (cm_env … frame_data)
1176       (cl_env_hyp … frame_data)
1177       new_cl_mem
1178       new_cm_mem
1179       (Em … frame_data)
1180       Hinj
1181       (stackptr … frame_data)
1182       ? (* (matching … frame_data) *)
1183       (Em_fn_id … frame_data))}
1184[ whd #id
1185  lapply (matching … frame_data id)
1186  lapply (Haux id)
1187  cases (lookup ??? id) normalize nodelta
1188  [ #_ #H @H
1189  | #b cases (lookup ??? id) normalize nodelta
1190    [ #_ #H @H
1191    | * #vartype #cltype normalize nodelta
1192      cases vartype try // normalize nodelta #Haux
1193      #H #v #Hload @H >(Haux ?? (refl ??) (refl ??)) @Hload
1194    ]
1195  ]
1196|
1197@conj try @conj try @conj try @conj try @conj try @conj try @refl
1198qed.*)
1199
1200lemma store_value_of_type_success_by_value :
1201   ∀ty, m, m', b, o, v.
1202   store_value_of_type ty m b o v = Some ? m' →
1203   access_mode ty = By_value (typ_of_type ty) ∧
1204   storev (typ_of_type ty) m (Vptr (mk_pointer b o)) v = Some ? m'.   
1205#ty #m #m' #b #o #v
1206cases ty
1207[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
1208| #structname #fieldspec | #unionname #fieldspec | #id ]
1209whd in ⊢ ((??%?) → ?);
1210[ 1,4,5,6,7: #Habsurd destruct (Habsurd) ]
1211#H @conj try @refl @H
1212qed.
1213
1214(* Some boilerplate to avoid performing a case analysis on exprs in the middle of
1215 * the proof. *)
1216lemma translate_dest_not_Evar_id :
1217  ∀vars, ed, ty.
1218  (∀id. ed ≠ Evar id) →
1219    translate_dest vars (Expr ed ty) =
1220    (do e1' ← translate_addr vars (Expr ed ty);
1221     OK ? (MemDest ? e1')).
1222#vars *
1223[ #sz #i | #id | #e1 | #e1 | #op #e1 |#op #e1 #e2 | #cast_ty #e1
1224| #cond #iftrue #iffalse | #e1 #e2 | #e1 #e2 | #sizeofty | #e1 #field | #cost #e1 ]
1225#ty #H
1226[ 2: @False_ind @(absurd … (refl ??) (H ?)) ]
1227@refl
1228qed.
1229
1230lemma expr_is_Evar_id_dec :
1231  ∀ed. (∀id. ed ≠ Evar id) ∨ (∃id. ed = Evar id).
1232
1233[ #sz #i | #id | #e1 | #e1 | #op #e1 |#op #e1 #e2 | #cast_ty #e1
1234| #cond #iftrue #iffalse | #e1 #e2 | #e1 #e2 | #sizeofty | #e1 #field | #cost #e1 ]
1235[ 2: %2 %{id} @refl
1236| *: %1 #id % #Habsurd destruct (Habsurd) ]
1237qed.
1238
1239(* Not provable: need to relate (typeof (e=Evar id, ty)) with the type contained
1240   in var_ty. Should be doable, but not now. *)
1241(*   
1242lemma translate_dest_IdDest_typ :
1243  ∀vars,e,var_id,var_ty,H.
1244    translate_dest vars e = return (IdDest vars var_id var_ty H) →
1245    var_ty = typeof e.
1246#vars * #ed #ety #var_id #var_ty #H
1247cases ed   
1248[ #sz #i | #id | #e1 | #e1 | #op #e1 |#op #e1 #e2 | #cast_ty #e1
1249| #cond #iftrue #iffalse | #e1 #e2 | #e1 #e2 | #sizeofty | #e1 #field | #cost #e1 ]
1250[ 2,3,12:
1251  [ 2,3:
1252    whd in ⊢ ((??%?) → ?);
1253    cases (translate_addr ??) normalize nodelta
1254    [ 2,3: #error whd in ⊢ ((??%%) → ?); #Habsurd destruct (Habsurd)
1255    | 1,4: #Hfoo whd in ⊢ ((??%%) → ?); #Habsurd destruct (Habsurd) ]
1256  | 1: #H' lapply (bind2_eq_inversion ?????? H') * #vt * #t * #Eq
1257    lapply Eq inversion vt normalize nodelta
1258    [ 1,2: #foo #bar #Hlookup
1259      whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1260    | 3: #e whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
1261| *: whd in ⊢ ((??%?) → ?); whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd)
1262normalize nodelta
1263[ 2:*)
1264
1265
1266lemma mk_offset_offv_id : ∀o. mk_offset (offv o) = o.
1267* #x @refl qed.
1268
1269lemma find_funct_to_find_funct_id :
1270   ∀F, ge, ptr, fundef.
1271   ∀H:find_funct ? ge ptr = Some ? fundef.
1272   find_funct_id F ge ptr = Some ? 〈fundef, symbol_of_function_val' F ge ptr fundef H〉.
1273#F #ge #ptr #fundef #Hfind whd in match (find_funct_id ???);
1274generalize in ⊢ (??(?%)?);
1275generalize in ⊢
1276 ((???%) → (??
1277    (match %
1278(*     return λ_. (??%?) → ?*)
1279     with
1280     [ _ ⇒ λ_. ?
1281     | _ ⇒ λ_.λ_. ? ] ?)
1282  ?));
1283#o cases o normalize nodelta
1284[ #H @False_ind >Hfind in H; #Habsurd destruct (Habsurd)
1285| #f #Hfind' 
1286  cut (f = fundef)
1287  [ >Hfind in Hfind'; #Heq destruct (Heq) @refl ]
1288  #Heq destruct (Heq)
1289  @refl
1290] qed.
1291
1292lemma eval_bool_of_val_to_Cminor :
1293  ∀E. ∀ty. ∀v1,v2. ∀b.
1294    value_eq E v1 v2 →
1295    exec_bool_of_val v1 ty = return b →
1296    eval_bool_of_val v2 = return  b.
1297#E #ty #v1 #v2 #b #Hvalue_eq
1298whd in ⊢ ((??%%) → (??%%));
1299@(value_eq_inversion … Hvalue_eq) normalize nodelta
1300[ #Habsurd destruct (Habsurd) ]
1301[ #vsz #vi cases ty
1302  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
1303  | #structname #fieldspec | #unionname #fieldspec | #id ] normalize nodelta
1304  [ 2: | *: #Habsurd destruct (Habsurd) ]
1305  @(intsize_eq_elim_elim … vsz sz)
1306  [ 1: #H #Habsurd destruct (Habsurd)
1307  | 2: #Heq destruct (Heq) normalize nodelta #H @H ]
1308| cases ty
1309  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
1310  | #structname #fieldspec | #unionname #fieldspec | #id ] normalize nodelta
1311  #H destruct (H) @refl
1312| #p1 #p2 #Htranslate
1313  cases ty
1314  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
1315  | #structname #fieldspec | #unionname #fieldspec | #id ] normalize nodelta
1316  #H destruct (H) @refl
1317] qed.
1318
1319(* --------------------------------------------------------------------------- *)
1320(* Main simulation results                                                     *)
1321(* --------------------------------------------------------------------------- *)
1322
1323(* Conjectured simulation results
1324
1325   We split these based on the start state:
1326   
1327   1. ‘normal’ states take some [S n] normal steps and simulates them by [S m]
1328      normal steps in Cminor;
1329   2. call and return steps are simulated by a call/return step plus [m] normal
1330      steps (to copy stack allocated parameters / results); and
1331   3. lone cost label steps are simulates by a lone cost label step
1332   
1333   These should allow us to maintain enough structure to identify the Cminor
1334   subtrace corresponding to a measurable Clight subtrace.
1335 *)
1336
1337lemma clight_cminor_normal :
1338    ∀g1,g2.
1339    ∀INV:clight_cminor_inv g1 g2.
1340    ∀s1,s1'.
1341    clight_cminor_rel g1 g2 INV s1 s1' →
1342    clight_normal s1 →
1343    ¬ pcs_labelled cl_pre g1 s1 →
1344    ∀s2,tr. step … (pcs_exec cl_pre) g1 s1 = Value … 〈tr,s2〉 →   
1345    ∃m. after_n_steps m ?? (pcs_exec cm_pre) g2 s1' (λs.cminor_normal s) (λtr',s2'.
1346      tr = tr' ∧
1347      clight_cminor_rel g1 g2 INV s2 s2' ∧
1348      (m = 0 → lex_lt (measure_Clight s2) (measure_Clight s1))
1349    ).
1350#g1 #g2 #INV #s1 #s1' #Hstate_rel #Hclight_normal #Hnot_labeleld
1351inversion Hstate_rel
1352[ 1: (* Normal state *)
1353     (* ---------------------------------------------------------------------- *)
1354#cl_ge #cm_ge #INV' #cl_s
1355(* case analysis on Clight statement *)
1356cases cl_s
1357[ 1: | 2: #lhs #rhs | 3: #retv #func #args | 4: #stm1 #stm2 | 5: #cond #iftrue #iffalse | 6: #cond #body
1358| 7: #cond #body | 8: #init #cond #step #body | 9,10: | 11: #retval | 12: #cond #switchcases | 13: #lab #body
1359| 14: #lab | 15: #cost #body ]
1360[ 3: (* Call *)
1361     #cm_s #cl_k #cm_k #cm_st #cl_f #cm_f #rettyp
1362     #alloc_type #cl_env #cl_m #cm_env #cm_m #stackptr #stacksize
1363     (* introduce everything *)
1364     #fInv #sInv #kInv #Htarget_type #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function
1365     #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls
1366     #flag * * * * #Hstmt_inv #Hlabels_translated #Htmps_preserved #Hreturn_ok #Hlabel_wf
1367     (* generalize away ugly proof *)
1368     generalize in ⊢ (∀_:(???(??(????%))).?); #Hugly
1369     #Htranslate #Hcont_rel #Em
1370     #Htmp_vars_well_allocated
1371     #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id
1372     @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
1373     destruct (HA HB)
1374     @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
1375     destruct (HC HD HE) #_
1376     (* back to unfolding Clight execution *)
1377     cases (bind_inversion ????? Htranslate) -Htranslate *
1378     #ef #Hexpr_vars_ef * #Htranslate_ef normalize nodelta #Htranslate
1379     cases (bind_inversion ????? Htranslate) -Htranslate *
1380     #ef' #Hexpr_vars_local_ef' * #Htyp_should_eq_ef
1381     cases (typ_should_eq_inversion (typ_of_type (typeof func)) ASTptr … Htyp_should_eq_ef)
1382     -Htyp_should_eq_ef #Htyp_equality_ef
1383     #Heq_ef_ef' #Htranslate
1384     cases (bind_inversion ????? Htranslate) -Htranslate *
1385     #cm_args #Hall_variables_from_args_local *
1386     whd in ⊢ ((???%) → ?); #Hargs_spec
1387     @(match retv
1388       return λx. retv = x → ?
1389       with
1390       [ None ⇒ λHretv. ?
1391       | Some lhs ⇒ λHretv. ?
1392       ] (refl ? retv))
1393     normalize nodelta
1394     [ 2: (* return something *)
1395       #Hdest cases (bind_inversion ????? Hdest) -Hdest #dest *
1396       inversion dest normalize nodelta
1397       [ (* register dest *) #var_id #var_ty #His_local @(jmeq_absorb ?????) #Hdest       
1398         #Htranslate_dest whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1399         (* make explicit the nature of lhs, allowing to prove that no trace is emitted *)
1400         lapply (translate_dest_id_inversion  … Htranslate_dest) #Hlhs_eq
1401       | * #cm_expr #Hexpr_vars_cm #Hdest #Htranslate_dest #Hgensym
1402         lapply (breakup_dependent_match_on_pairs ?????? Hgensym) -Hgensym
1403         * #ret_var * #new_gensym * #Heq_alloc_tmp * #_ #Hgensym
1404         lapply (breakup_dependent_match_on_pairs ?????? Hgensym) -Hgensym
1405         * #tmp_var * #new_gensym' * #Heq_alloc_tmp' * #_
1406         generalize in ⊢ ((??(?? (????%) )?) → ?); #Hstmt_inv_after_gensym
1407         whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1408       ]
1409     | 1: (* return void *)
1410          generalize in ⊢ ((??(??(????%))?) → ?); #Hugly2
1411          whd in ⊢ ((???%) → ?); #Heq destruct (Heq) ]
1412     #s2 #tr #Htranslate
1413     cases (bindIO_inversion ??????? Htranslate) -Htranslate *
1414     #func_ptr_val #func_trace * #Hexec_func_ptr normalize nodelta
1415     whd in ⊢ ((???%) → ?); #Htranslate
1416     cases (bindIO_inversion ??????? Htranslate) -Htranslate *
1417     #args_values #args_trace * #Hexec_arglist #Htranslate
1418     cases (bindIO_inversion ??????? Htranslate) -Htranslate
1419     * #cl_fundef #cl_fun_id * #Hfind_funct
1420     lapply (opt_to_io_Value ?????? Hfind_funct) -Hfind_funct #Hfind_funct
1421     cases (find_funct_inversion ???? Hfind_funct)
1422     #func_ptr * * * #Hfunc_ptr_eq destruct (Hfunc_ptr_eq)
1423     #Hpoff_eq_zero #Hregion_is_code
1424     * #block_id * #Hblock_id_neg #Hlookup
1425     #Htranslate
1426     cases (bindIO_inversion ??????? Htranslate) -Htranslate #Htype_of_fundef *
1427     #Hassert_type_eq
1428     [ 1,2: #Htranslate
1429            cases (bindIO_inversion ??????? Htranslate) -Htranslate * *
1430            #lblock #loffset #ltrace *
1431            whd in ⊢ ((???%) → (???%) → ?);
1432            [ >Hlhs_eq #Hexec_lvalue
1433              cut (ltrace = [])
1434              [ lapply (res_to_io ????? Hexec_lvalue)
1435                #H' whd in H':(??%?); cases (lookup ????) in H'; normalize nodelta
1436                [ 2: #b #Heq destruct (Heq) @refl
1437                | #H cases (bind_inversion ????? H) #H24 * #H27 #H28
1438                  whd in H28:(???%); destruct (H28) @refl ]
1439              ] #H destruct (H)
1440            | #Hexec_lvalue ]
1441     | 3: ]
1442     whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
1443     [ 1: %{1} whd whd in ⊢ (??%?); normalize nodelta
1444     | 2: (* Execute Cminor part: evaluate lhs, evaluate assign *)
1445          %{5} whd whd in ⊢ (??%?); normalize nodelta
1446          whd in match (eval_expr ???????);
1447          whd in match (m_bind ?????);
1448          cut (expr_vars ASTptr cm_expr
1449                  (λid:ident.λty:typ.present SymbolTag val cm_env id))
1450          [ cases sInv * * * * * * * #_ #H #_ #_ #_ @H ] #Hexpr_vars_cut
1451          lapply (translate_dest_MemDest_simulation … Htranslate_dest Hexec_lvalue)
1452          try assumption try @refl
1453          * #cm_val_tmp * #Heval_expr_tmp >Heval_expr_tmp #Hvalue_eq
1454          normalize nodelta generalize in match (proj1 ???); #Htmp_var_present
1455          cases (value_eq_ptr_inversion … Hvalue_eq) #cm_ptr * #Hcm_val_tmp #Hcm_ptr_translation
1456          >Hcm_val_tmp
1457          lapply (Htmp_vars_well_allocated … tmp_var Htmp_var_present (Tpointer (typeof lhs)) ? (Vptr cm_ptr) ?)
1458          [ 2: @(alloc_tmp_in_genlist … (sym_eq ??? Heq_alloc_tmp) (sym_eq ??? Heq_alloc_tmp'))
1459          | 1: normalize cases cm_ptr #b #o %3 ]
1460          * #cm_mem_after_store * #Hstorev #Hnew_inj >Hstorev
1461          whd in match (m_bind ?????); normalize nodelta
1462          whd whd in ⊢ (??%?); normalize nodelta
1463(*          cases (update_clight_cminor_data_cm … frame_ … Hnew_inj)
1464          try assumption #frame_data'
1465          * * * * * #Halloctype_eq_frame_data #Hcl_env_eq_frame_data #Hcm_env_eq_frame_data
1466          #Hstackptr_eq_frame_data #Hcl_m_eq_frame_data #Hcm_m_eq_frame_data *)
1467     | 3: %{1} whd whd in ⊢ (??%?); normalize nodelta
1468     ]
1469    (* execute Cminor part *)
1470    [ 1: generalize in match (proj2 (present ????) (expr_vars ???) (proj1 ???));
1471    | 2: generalize in match (proj2 (present ????) (expr_vars ???) (proj1 ???));
1472    | 3: generalize in match (proj2 True ??); ]
1473    #Hexpr_vars_present_ef'
1474    [ 1,3:
1475       cases (eval_expr_sim … INV' … Halloc_hyp … Hcl_env_hyp … Hinjection … Hmatching) #Hsim_expr #_
1476       cut (expr_vars (typ_of_type (typeof func)) ef
1477             (λid:ident.λty:typ.present SymbolTag val cm_env id))
1478       [ 1,3: lapply Heq_ef_ef' lapply Hexpr_vars_ef lapply ef >Htyp_equality_ef
1479                #ef #Hexpr_vars_ef @(jmeq_absorb ?????) #Heq destruct (Heq)
1480                @Hexpr_vars_present_ef' ]
1481       #Hexpr_vars_present_ef
1482       lapply (Hsim_expr … Htranslate_ef … Hexpr_vars_present_ef … Hexec_func_ptr)
1483       -Hsim_expr * #cm_func_ptr_val * #Heval_func #Hvalue_eq_func
1484       cut (eval_expr cm_ge ASTptr ef' cm_env Hexpr_vars_present_ef'
1485             stackptr cm_m = OK (trace×val) 〈func_trace,cm_func_ptr_val〉)
1486       [ 1,3:
1487         lapply Heq_ef_ef' lapply Heval_func lapply Hexpr_vars_ef lapply Hexpr_vars_local_ef'
1488         lapply Hexpr_vars_present_ef lapply ef lapply Hexpr_vars_present_ef' lapply ef'
1489         <Htyp_equality_ef #ef' #HA #ef #HB #HC #HD #HE
1490         @(jmeq_absorb ?????) #Heq destruct (Heq) @HE ]
1491       -Heval_func #Heval_func >Heval_func
1492    | 2: (* treat case 2 as special, since the type differs slightly *)
1493       cases (eval_expr_sim … INV' … Halloc_hyp ? cm_env Hcl_env_hyp … Hnew_inj stackptr Hmatching)
1494       #Hsim_expr #_
1495       generalize in match (proj2 ???); #Hall_present
1496       generalize in match (proj1 ???); #Hret_present
1497       generalize in match (proj2 ???); #Hstore_inv
1498       generalize in match (conj ????); #Hstmt_inv
1499       cut (eval_expr cm_ge ? ef' cm_env ? stackptr cm_m =
1500            (eval_expr cm_ge ASTptr ef' cm_env ? stackptr cm_m)) try assumption try @refl
1501       #Heval_expr_rewrite >Heval_expr_rewrite -Heval_expr_rewrite
1502       lapply (Hsim_expr … Htranslate_ef … (Vptr func_ptr) func_trace ??)       
1503       try assumption
1504       [ lapply Hexpr_vars_present_ef' lapply Heq_ef_ef' lapply Hexpr_vars_ef lapply Hexpr_vars_local_ef'
1505         lapply ef >Htyp_equality_ef #ef #HA #HB @(jmeq_absorb ?????) #Heq destruct (Heq) #x @x ]
1506       * #cm_func_ptr_val * #Heval_func_cm #Hvalue_eq_func
1507       (* And some more shuffling types around to match the goal *)
1508       cut (eval_expr cm_ge ? ef' cm_env Hexpr_vars_present_ef' stackptr cm_mem_after_store = OK ? 〈func_trace,cm_func_ptr_val〉)
1509       [ lapply Heval_func_cm -Heval_func_cm
1510         generalize in ⊢ ((??(?????%??)?) → ?);
1511         lapply Heq_ef_ef' -Heq_ef_ef'
1512         lapply Hexpr_vars_ef -Hexpr_vars_ef
1513         lapply Hexpr_vars_local_ef' -Hexpr_vars_local_ef'
1514         lapply Hexpr_vars_present_ef'
1515         lapply ef >Htyp_equality_ef #ef0 #HA #HB #HC @(jmeq_absorb ?????)
1516         #Heq destruct (Heq) #H1 #H2 @H2 ]
1517       #Heval_cm_func >Heval_cm_func ]
1518    whd in match (m_bind ?????);
1519    lapply (trans_fn … INV' … Hfind_funct)
1520    * #tmp_u * #cminor_fundef * #Hglobals_fresh_for_tmp_u * #Hfundef_fresh_for_tmp_u *
1521    #Htranslate_fundef #Hfind_funct_cm
1522    lapply (value_eq_ptr_inversion … Hvalue_eq_func) * #cm_func_ptr * #Hcm_func_ptr
1523    whd in ⊢ ((??%?) → ?); cases func_ptr in Hfind_funct Hfind_funct_cm Hregion_is_code Hpoff_eq_zero;
1524    #cm_block #cm_off #Hfind_funct #Hfind_funct_cm #Hregion_is_code #Hpoff_eq_zero destruct (Hpoff_eq_zero)
1525    whd in ⊢ ((??%?) → ?);
1526    [ 1,2: >(HEm_fn_id … cm_block Hregion_is_code)
1527    | 3: >(HEm_fn_id … cm_block Hregion_is_code) ]
1528    normalize nodelta cases cm_func_ptr in Hcm_func_ptr; #cm_block' #cm_off'
1529    #Hcm_func_ptr #Heq destruct (Hcm_func_ptr Heq)
1530    [ 1,2: >addition_n_0 >mk_offset_offv_id
1531    | 3: ]
1532    >(find_funct_to_find_funct_id ???? Hfind_funct_cm)
1533    whd in match (opt_to_res ???); normalize nodelta
1534    (* Again, isolate cases by type similarity *)
1535    [ 1,2:
1536      cut (All (𝚺t:typ.CMexpr t)
1537            (λx:𝚺t:typ.expr t.(
1538              match x with
1539              [ mk_DPair ty e ⇒
1540               expr_vars ty e
1541                 (λid:ident
1542                  .λty0:typ.present SymbolTag val cm_env id)])) cm_args)
1543      [ 1: cases sInv * * normalize nodelta * #_ #_ #Hall #_ #_ @Hall
1544      | 3: cases sInv * * normalize nodelta * #_ #_ #Hall #_ #_ @Hall ]
1545      #Hall
1546      cases (eval_exprlist_simulation …  Halloc_hyp Hcl_env_hyp Hinjection Hmatching ???? Hexec_arglist Hargs_spec Hall)
1547      #cm_values * #Hcm_exec_list #Hcl_cm_values_eq >Hcm_exec_list
1548    | 3:
1549      (* Arrrgh *)
1550      lapply (eval_exprlist_simulation …  Halloc_hyp Hcl_env_hyp Hnew_inj ????? Hexec_arglist Hargs_spec ?)
1551      try assumption *
1552      #cm_values * #Hcm_exec_list #Hcl_cm_values_eq >Hcm_exec_list
1553    ]
1554    whd in match (m_bind ?????); normalize nodelta whd @conj
1555    [ 2,4,6: #Habsurd destruct (Habsurd) ]
1556    @conj
1557    [ 1,3,5: normalize try @refl
1558             >append_nil >append_nil @refl ]
1559    [ 1: generalize in match (proj1 ? (expr_vars ???) (proj1 ???)); #Hugly_pres
1560    | 2: generalize in match (proj1 ? (expr_vars ???) (proj1 ???)); #Hugly_pres
1561    | 3: ]
1562(*    [ 3: >addition_n_0 ]*)
1563    [ 1,2: (* no return or return to CM local variable *)
1564           @(CMR_call_nostore … tmp_u) try assumption
1565           [ 2,4: (* TODO: prove matching between CL and CM function ids *)
1566                  @cthulhu
1567           ]
1568           lapply Hfind_funct
1569           lapply Hfind_funct_cm
1570           lapply Htranslate_fundef
1571           lapply Hfundef_fresh_for_tmp_u
1572           lapply Hassert_type_eq
1573           lapply Htype_of_fundef
1574           lapply Hlookup
1575           cases cl_fundef
1576           [ 2,4: #id #typel #ty #HA #HB #HC #HD #HE #HF #HG @I
1577           | 1,3: #f #HA #HB #HC #HD #HE #HF #HG normalize nodelta
1578                  @conj try @conj try @conj try assumption ]
1579    | 3: (* type mismatch *)
1580         @(CMR_call_store … tmp_u) try assumption
1581         [ 2: (* TODO: prove matching between CL and CM function ids *)
1582              @cthulhu ]
1583         lapply Hfind_funct
1584         lapply Htranslate_fundef
1585         lapply Hfundef_fresh_for_tmp_u
1586         lapply Hassert_type_eq
1587         lapply Htype_of_fundef
1588         lapply Hlookup
1589         cases cl_fundef
1590         [ 2: #id #typel #ty #HA #HB #HC #f #HD #HE @I ]
1591         #f #HA #HB #HC #HD #HE #HF normalize nodelta @conj try @conj try @conj
1592         try assumption
1593    ]
1594| 1: (* Skip *)
1595    #cm_s #cl_k #cm_k #cm_st #cl_f #cm_f #rettyp
1596    #alloc_type #cl_env #cl_m #cm_env #cm_m #stackptr #stacksize
1597    (* introduce everything *)
1598    #fInv #sInv #kInv
1599    #Htarget_type #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function
1600    #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls
1601    #flag * * * * #Hstmt_inv #Hlabels_translated #Htmps_preserved
1602    #Hreturn_ok #Hlabel_wf generalize in match (conj ????); #Hugly
1603    whd in ⊢ ((??%?) → ?); #Heq_translate   
1604    #Hcont_rel
1605    lapply Heq_translate -Heq_translate
1606    lapply Hugly -Hugly
1607    lapply Hlabel_wf -Hlabel_wf
1608    lapply Hreturn_ok -Hreturn_ok
1609    lapply Htmps_preserved -Htmps_preserved
1610    lapply Hlabels_translated -Hlabels_translated
1611    lapply Hstmt_inv -Hstmt_inv
1612    lapply Htranslate_function -Htranslate_function
1613    lapply Hfresh_globals -Hfresh_globals
1614    lapply Hfresh_function -Hfresh_function
1615    lapply Htarget_type -Htarget_type
1616    lapply kInv -kInv
1617    lapply sInv -sInv
1618    lapply fInv -fInv
1619    lapply stmt_univ -stmt_univ
1620    lapply stmt_univ' -stmt_univ'
1621    (* case analysis on continuation *)
1622    inversion Hcont_rel
1623    [ (* Kstop continuation *)
1624      (* simplifying the goal using outcome of the inversion *)
1625      #kcl_ge #kcm_ge #kINV #kcl_f #kcm_f #ktarget_type #kcl_env #kcm_env #kalloc_type
1626      @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
1627      destruct (HA HB)
1628      @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
1629      destruct (HC HD HE)
1630      @(jmeq_absorb ?????) #HF @(jmeq_absorb ?????) #HG @(jmeq_absorb ?????) #HH
1631      @(jmeq_absorb ?????) #HI @(jmeq_absorb ?????) #HJ @(jmeq_absorb ?????) #HK
1632      destruct (HF HG HH HI HJ HK) #_
1633      (* introduce everything *)
1634      #stmt_univ' #stmt_univ #fInv #sInv #kInv #Htarget_type #Hfresh_function #Hfresh_globals
1635      #Htranslate_function #Hstmt_inv #Hlabels_translated #Htmps_preserved #Hreturn_ok #Hlabel_wf
1636      #Hugly generalize in match (conj ????); #Hugly'
1637      (* reduce statement translation function *)
1638      #Heq_translate
1639      (* In this simple case, trivial translation *)
1640      destruct (Heq_translate)
1641      #Em #Htmp_vars_well_allocated #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id
1642      @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
1643      destruct (HA HB)
1644      @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
1645      destruct (HC HD HE) #_
1646      (* unfold the clight execution *)
1647      #s2 #tr whd in ⊢ ((??%?) → ?);
1648      inversion (fn_return kcl_f) normalize nodelta
1649      [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
1650      | #structname #fieldspec | #unionname #fieldspec | #id ]
1651      #Hfn_return whd in ⊢ ((??%?) → ?); #Heq destruct (Heq)
1652      %{1} whd @conj try @conj try @refl
1653      [ 2: #Habsurd destruct (Habsurd) ]
1654      @CMR_return
1655    | #kcl_ge #kcm_ge #kINV #kcl_f #kcm_f #ktarget_type #kalloc_type #kcl_s #kcm_s
1656      #kcl_env #kcm_env #kcl_k' #kcm_k' #kstmt_univ #kstmt_univ' #klbl_univ #klbl_univ' #klbls #kflag
1657      * * * * #kHstmt_inv #kHlabels_translated #kHtmps_preserved
1658      #kHreturn_ok #kHlabel_wf #kHeq_translate #kHcont_rel #_
1659      @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
1660      destruct (HA HB)
1661      @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
1662      destruct (HC HD HE)
1663      @(jmeq_absorb ?????) #HF @(jmeq_absorb ?????) #HG @(jmeq_absorb ?????) #HH @(jmeq_absorb ?????) #HI
1664      @(jmeq_absorb ?????) #HJ @(jmeq_absorb ?????) #HK
1665      destruct (HF HG HH HI HJ HK) #_
1666      #stmt_univ' #stmt_univ #fInv #sInv #kInv #Htarget_type #Hfresh_function #Hfresh_globals
1667      #Htranslate_function #Hstmt_inv #Hlabels_translated #Htmps_preserved #Hreturn_ok #Hlabel_wf
1668      #Hugly generalize in match (conj ????); #Hugly'
1669      (* In this simple case, trivial translation *)
1670      #Heq_translate destruct (Heq_translate)
1671      #Em
1672      #Htmp_vars_well_alloc #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id
1673      @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
1674      destruct (HA HB)
1675      @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
1676      destruct (HC HD HE) #_
1677      #s2 #tr whd in ⊢ ((??%?) → ?); #Heq destruct (Heq)
1678      %{1} whd @conj [ 2: #Habsurd destruct (Habsurd) ] @conj try @refl
1679      (* close simulation *)
1680      @(CMR_normal … kHeq_translate … Hinjection … Hmatching) try assumption
1681      (* TODO wrap this up properly, by adding some invariant or by threading stmt_univ' into the cont *)
1682      @cthulhu
1683      (* TODO: lemma allowing to prove this from [Htmp_vars_well_alloc] + tmp_gen inclusion *)
1684    | (* Kwhile continuation *)
1685      #kcl_ge #kcm_ge #kINV #kcl_f #kcm_f #ktarget_type #kalloc_type #kcl_env #kcm_env
1686      #kcl_k' #kcm_k' #ksz #ksg #kcl_cond_desc #kcl_body #kcm_cond #kcm_body
1687      #kentry #kexit #kstmt_univ #kstmt_univ' #klbl_univ #klbl_univ' #klbl_univ''
1688      #klbls #kHtranslate_inv #kHexpr_vars #kHtranslate_expr #kfInv
1689      * * * * #kHentry_declared * * * *
1690      * * * #kHcond_vars_declared #Hnoise #Hnoise' #Hnoise''
1691      #kHcont_inv #kHmklabels #kHeq_translate
1692      #kHfind_label #kHcont_rel #_
1693      @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
1694      destruct (HA HB)
1695      @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
1696      destruct (HC HD HE)
1697      @(jmeq_absorb ?????) #HF @(jmeq_absorb ?????) #HG @(jmeq_absorb ?????) #HH
1698      @(jmeq_absorb ?????) #HI @(jmeq_absorb ?????) #HJ @(jmeq_absorb ?????) #HK
1699      destruct (HF HG HH HI HJ HK) #_
1700      #stmt_univ' #stmt_univ #fInv #sInv #kInv #Htarget_type #Hfresh_function #Hfresh_globals
1701      #Htranslate_function #Hstmt_inv #Hlabels_translated #Htmps_preserved #Hreturn_ok #Hlabel_wf
1702      #Hugly generalize in match (conj ????); #Hugly'
1703      (* In this simple case, trivial translation *)
1704      #Heq_translate destruct (Heq_translate)
1705      #Em #Htmp_vars_well_allocated #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching
1706      #HEm_fn_id
1707      @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
1708      destruct (HA HB)
1709      @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
1710      destruct (HC HD HE) #_ #s2 #tr
1711      whd in ⊢ ((??%?) → ?); #Heq destruct (Heq)
1712      lapply kHfind_label -kHfind_label
1713      generalize in ⊢ ((??(????%????)?) → ?); #Hlabel_exists
1714      generalize in ⊢ ((???(????%)) → ?); #Hmore_invariant
1715      #kHfind_label
1716      %{2} whd whd in ⊢ (??%?); normalize nodelta generalize in match (proj2 ???); #Hmore_noise
1717      generalize in match (proj1 ???); #Hmore_noise'
1718      >kHfind_label normalize nodelta
1719      whd @conj try @conj try @refl
1720      generalize in match (proj1 ???); #Hvars_present_in_ifthenelse
1721      generalize in match (proj2 ???); #Hcont_inv'
1722      [ 2: #Habsurd destruct (Habsurd) ]
1723      (* go to a special simulation state for while loops *)
1724      @(CMR_while … stacksize … Hcl_env_hyp … Hinjection … kHtranslate_expr … kHeq_translate)
1725      try assumption
1726      (* TODO wrap this up properly, by adding some invariant or by threading stmt_univ' into the cont *)
1727      @cthulhu
1728      (* TODO: lemma allowing to prove this from [Htmp_vars_well_alloc] + tmp_gen inclusion *)           
1729    ]
1730| 2: (* Assign *)
1731     #cm_s #cl_k #cm_k #cm_st #cl_f #cm_f #rettyp
1732     #alloc_type #cl_env #cl_m #cm_env #cm_m #stackptr #stacksize
1733     (* introduce everything *)
1734     #fInv #sInv #kInv #Htarget_type #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function
1735     #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls
1736     #flag * * * * #Hstmt_inv_cm #Hlabels_translated #Htmps_preserved
1737     #Hreturn_ok #Hlabel_wf generalize in match (conj ????); #Hugly #Htranslate
1738     #Hcont_rel
1739     #Em #Htmp_vars_well_allocated #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id
1740     @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
1741     destruct (HA HB)
1742     @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE #_
1743     destruct (HC HD HE)
1744     lapply Htranslate -Htranslate
1745     (* case-split on lhs in order to reduce lvalue production in Cminor *)
1746     cases lhs #lhs_ed #lhs_ty
1747     cases (expr_is_Evar_id_dec lhs_ed)
1748     [ 2: * #var_id #Hlhs_ed destruct (Hlhs_ed)
1749          #Htranslate_statement
1750          cases (bind_inversion ????? Htranslate_statement)
1751          * #cm_rhs #Hexpr_vars_rhs * #Htranslate_rhs #Htranslate_statement'
1752          cases (bind_inversion ????? Htranslate_statement') -Htranslate_statement'
1753          #lhs_dest * #Htranslate_lhs
1754          cases (bind2_eq_inversion ?????? Htranslate_lhs) -Htranslate_lhs
1755          #alloctype * #type_of_var * #Hlookup_var_success
1756          cases alloctype in Hlookup_var_success;
1757          normalize nodelta
1758          [ 1: (* Global *) #r
1759               #Hlookup_var_success whd in ⊢ ((???%) → ?); #Hlhs_dest_eq
1760               destruct (Hlhs_dest_eq) normalize nodelta
1761               generalize in match (conj ????); #Hinvariant
1762               cases (type_eq_dec ??)
1763               [ 2: #Hneq normalize nodelta whd in ⊢ ((??%%) → ?);
1764                    #Habsurd destruct (Habsurd) ]
1765               normalize nodelta whd in match (typeof ?); #Heq_cl_types
1766               whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1767               #s2 #tr whd in ⊢ ((??%?) → ?); #Hstep
1768               cases (bindIO_inversion ??????? Hstep) -Hstep
1769               * * #cl_blo #cl_off #cl_tr * whd in ⊢ ((??%?) → ?);
1770               #Hexec_lvalue #Hstep
1771               lapply (res_to_io ????? Hexec_lvalue) -Hexec_lvalue #Hexec_lvalue
1772               cases (bindIO_inversion ??????? Hstep) -Hstep
1773               * #cl_rhs_val #cl_trace * #Hexec_rhs #Hstep
1774               cases (bindIO_inversion ??????? Hstep) -Hstep
1775               #cl_mem_after_store_lhs * #Hstore
1776               whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
1777               lapply (opt_to_io_Value ?????? Hstore) -Hstore #Hstore
1778               %{1} whd whd in ⊢ (??%?); normalize nodelta
1779               generalize in match (proj1 ???); whd in ⊢ (% → ?); *
1780               whd in match (eval_expr ???????);
1781               whd in match (eval_constant ????);
1782               whd in Hexec_lvalue:(??%?);
1783               <(eq_sym … INV' var_id)
1784               lapply (Hmatching … var_id)
1785               cases (lookup ?? cl_env var_id) in Hexec_lvalue; normalize nodelta
1786               [ 1: #Heq_find_sym cases (bind_inversion ????? Heq_find_sym) -Heq_find_sym
1787                    #global_b * #Hopt_to_res lapply (opt_to_res_inversion ???? Hopt_to_res) -Hopt_to_res
1788                    #Hfind_symbol >Hfind_symbol
1789                    normalize nodelta
1790                    whd in ⊢ ((???%) → ?); #Heq destruct (Heq) #Hembed_eq
1791                    whd in match (m_bind ?????);
1792                    cases (eval_expr_sim … Halloc_hyp … Hcl_env_hyp … Hinjection … Hmatching) #Hsim_expr #_
1793                    lapply (Hsim_expr … Htranslate_rhs … (proj2 ?? (proj1 ?? (proj1 ?? sInv))) Hexec_rhs)
1794                    * #cm_rhs_val generalize in match (proj2 ???);
1795                    #Hexpr_vars_rhs * #Heval_expr_rhs #Hvalue_eq_rhs >Heval_expr_rhs
1796                    whd in match (m_bind ?????); whd in Hstore:(??%?); whd in Hstore:(??%?);
1797                    cases (store_value_of_type_success_by_value lhs_ty cl_m
1798                                    cl_mem_after_store_lhs cl_blo zero_offset cl_rhs_val Hstore)
1799                    #Haccess_mode #Hstorev
1800                    lapply (storen_parallel_aux ??? Hinjection … Hvalue_eq_rhs … Hembed_eq ??? Hstorev)
1801                    * #cm_mem_after_store_lhs * #Hstoren #Hinj whd in Hstoren:(??%?);
1802                    whd in Hstoren:(??%?); whd in match (shift_offset ???);
1803                    >sign_ext_same_size >addition_n_0
1804                    whd in match (storev ????);
1805                    lapply Hstoren whd in match (offset_plus ??);
1806                    >addition_n_0 -Hstoren
1807                    >Heq_cl_types #Hstoren >Hstoren
1808                    whd in match (opt_to_res ???); normalize nodelta
1809                    whd @conj try @conj try @refl
1810                    [ 2: #Habsurd destruct (Habsurd) ]
1811                    generalize in match (conj ????);
1812                    #Hinv_vars
1813                    @CMR_normal try assumption
1814                    [ 2: @refl | 1,3,4: ]
1815                    [ 1: (* TODO: lemma on preservation of well-allocatedness through stores *) @cthulhu
1816                    | 2: (* TODO: lemma on preservation of memory matching through stores *) @cthulhu ]
1817               | 2: #b #Heq destruct (Heq)
1818                    lapply (opt_to_res_inversion ???? Hlookup_var_success) #Hlookup_aux
1819                    >Hlookup_aux normalize nodelta @False_ind ]
1820          | 2: (* Stack *)
1821               #n #Hlookup_var_success
1822               whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1823               normalize nodelta whd in ⊢ ((???%) → ?);
1824               cases (type_eq_dec ??) normalize nodelta #Htype_eq
1825               [ 2: #Habsurd destruct (Habsurd) ]
1826               #Heq destruct (Heq) #s2 #tr #Hstep
1827               cases (bindIO_inversion ??????? Hstep)
1828               * * #cl_lvalue_block #cl_offset #cl_trace * #Hexec_lvalue
1829               lapply (res_to_io ????? Hexec_lvalue) -Hexec_lvalue
1830               whd in ⊢ ((??%?) → ?);
1831               @(match lookup ?? cl_env var_id
1832                 return λx. (lookup ?? cl_env var_id = x) → ?
1833                 with
1834                 [ None ⇒ λH. ?
1835                 | Some cl_addr ⇒ λH. ?
1836                 ] (refl ? (lookup ?? cl_env var_id)))
1837               normalize nodelta
1838               [ (* Contradiction: a stack-allocated variable was necessarily in the environment *)
1839                 @cthulhu
1840               | #Heq destruct (Heq)
1841                 lapply (Hmatching var_id) >H normalize nodelta
1842                 >(opt_to_res_inversion ???? Hlookup_var_success) normalize nodelta
1843                 #Hembedding_to_stack #Hexec_cl_rhs
1844                 cases (bindIO_inversion ??????? Hexec_cl_rhs) -Hexec_cl_rhs *
1845                 #cl_rhs_result #cl_rhs_trace * #Hcl_exec_expr_rhs #Hcl_exec_store
1846                 cases (bindIO_inversion ??????? Hcl_exec_store) -Hcl_exec_store #cl_mem_after_store
1847                 * #Hstore_value_of_type lapply (opt_to_io_Value ?????? Hstore_value_of_type)
1848                 -Hstore_value_of_type
1849                 #Hstore_value_of_type
1850                 whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
1851                 %{1} whd whd in ⊢ (??%?); normalize nodelta
1852                 whd in match (eval_expr ???????);
1853                 whd in match (eval_constant ????);
1854                 whd in match (m_bind ?????);
1855                 cases (eval_expr_sim … Halloc_hyp … Hcl_env_hyp … Hinjection … Hmatching) #Hsim_expr #_
1856                 lapply (Hsim_expr … Htranslate_rhs … (proj2 ?? (proj1 ?? (proj1 ?? sInv))) Hcl_exec_expr_rhs)
1857                 * #cm_rhs_val generalize in match (proj2 ???);
1858                 #Hexpr_vars_rhs * #Heval_expr_rhs #Hvalue_eq_rhs >Heval_expr_rhs
1859                 normalize nodelta -Hsim_expr
1860                 whd in match (shift_offset ???); >sign_ext_same_size
1861                 >commutative_addition_n >addition_n_0
1862                 whd in Hstore_value_of_type:(??%?);
1863                 cases (store_value_of_type_success_by_value ? cl_m
1864                                    cl_mem_after_store ?? cl_rhs_result Hstore_value_of_type)
1865                 whd in match (typeof ?) in ⊢ ((??%%) → (??%?) → ?);
1866                 #Haccess_mode #Hstorev -Hstore_value_of_type
1867                 lapply (storen_parallel_aux ??? Hinjection … Hvalue_eq_rhs … Hembedding_to_stack ??? Hstorev)
1868                 * #cm_mem_after_store_lhs * #Hstoren #Hinj whd in Hstoren:(??%?);
1869                 >offset_plus_0 in Hstoren; #Hstorev'
1870                 whd in match (storev ????);
1871                 lapply Htype_eq whd in match (typeof ?) in ⊢ ((??%?) → ?); #Htype_eq'
1872                 <Htype_eq' >Hstorev'
1873                 whd in match (m_bind ?????); normalize nodelta
1874                 whd @conj try @conj try @refl
1875                 [ 2: #Habsurd destruct (Habsurd) ]
1876                 @(CMR_normal … Halloc_hyp) try assumption
1877                 [ 2: @refl | 1,3,4,5: ]
1878                 [ 1: (* TODO: lemma on preservation of well-allocatedness through stores *) @cthulhu
1879                 | 2: (* TODO: lemma on preservation of memory matching through stores *) @cthulhu ]
1880               ]
1881          | 3: (* Local *)
1882               #Hlookup_var_success whd in ⊢ ((???%) → ?);
1883               #Heq destruct (Heq) normalize nodelta -Htranslate_statement
1884               #Htranslate
1885               cases (bind_inversion ????? Htranslate) -Htranslate
1886               * #cm_expr #Hexpr_vars * #Htyp_should_eq
1887               whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
1888               cases (typ_should_eq_inversion (typ_of_type (typeof rhs)) (typ_of_type type_of_var) … Htyp_should_eq)
1889               -Htyp_should_eq #Htyp_eq lapply Hexpr_vars_rhs lapply Hexpr_vars
1890               -Hlabel_wf -Hreturn_ok -Hlabels_translated -Hstmt_inv_cm lapply sInv               
1891               lapply cm_expr -cm_expr <Htyp_eq #cm_expr #sInv #Hexpr_vars #Hexpr_vars'
1892               @(jmeq_absorb ?????) #Heq destruct (Heq)
1893               #s2 #tr whd in ⊢ ((??%?) → ?); #Hcl_exec
1894               cases (bindIO_inversion ??????? Hcl_exec)
1895               * * #cl_blo #cl_off #cl_trace *
1896               whd in ⊢ ((???%) → ?);
1897               #Hexec_lvalue lapply (res_to_io ????? Hexec_lvalue) -Hexec_lvalue
1898               whd in ⊢ ((??%?) → ?);
1899               @(match lookup ?? cl_env var_id
1900                 return λx. (lookup ?? cl_env var_id = x) → ?
1901                 with
1902                 [ None ⇒ λH. ?
1903                 | Some cl_addr ⇒ λH. ?
1904                 ] (refl ? (lookup ?? cl_env var_id)))
1905               normalize nodelta
1906               [ (* Contradiction: a register-allocated variable was necessarily in the environment *)
1907                 @cthulhu
1908               | #Heq destruct (Heq)
1909                 lapply (Hmatching var_id) >H normalize nodelta
1910                 >(opt_to_res_inversion ???? Hlookup_var_success) normalize nodelta
1911                 #Hpresent_in_local #Hexec_cl_rhs
1912                 cases (bindIO_inversion ??????? Hexec_cl_rhs) -Hexec_cl_rhs *
1913                 #cl_rhs_result #cl_rhs_trace * #Hcl_exec_expr_rhs #Hcl_exec_store
1914                 cases (bindIO_inversion ??????? Hcl_exec_store) -Hcl_exec_store #cl_mem_after_store
1915                 * #Hstore_value_of_type lapply (opt_to_io_Value ?????? Hstore_value_of_type)
1916                 -Hstore_value_of_type #Hstore_value_of_type
1917                 whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
1918                 %{1} whd whd in ⊢ (??%?); normalize nodelta
1919                 cases (eval_expr_sim … Halloc_hyp … Hcl_env_hyp … Hinjection … Hmatching) #Hsim_expr #_
1920                 lapply (Hsim_expr … Htranslate_rhs … (proj2 ?? (proj1 ?? (proj1 ?? sInv))) Hcl_exec_expr_rhs)
1921                 * #cm_rhs_val generalize in match (proj2 ???);
1922                 #Hexpr_vars_rhs * #Heval_expr_rhs #Hvalue_eq_rhs >Heval_expr_rhs
1923                 normalize nodelta -Hsim_expr whd @conj try @conj try @refl
1924                 [ 2: #Habsurd destruct (Habsurd) ]
1925                 generalize in match (proj1 ???); #Hpresent
1926                 generalize in match (conj ????); #Hstmt_vars
1927                 @(CMR_normal … Halloc_hyp) try assumption
1928                 [ 2: @refl | *: ]
1929                 [ (* Need a particular kind of continuation relation *) @cthulhu
1930                 | (* Lemma on preservation of well-allocatedness through update_present *) @cthulhu
1931                 | (* Memory injection when writing in clight only, and block not mapped *) @cthulhu
1932                 | (* Memory matching through env update *) @cthulhu ]
1933               ]
1934          ]
1935     | 1: #Hnot_evar #Htranslate_statement
1936          cases (bind_inversion ????? Htranslate_statement) -Htranslate_statement
1937          * #cm_rhs #Hexpr_vars_rhs * #Htranslate_rhs #Htranslate_statement'
1938          cases (bind_inversion ????? Htranslate_statement') -Htranslate_statement' #dest
1939          lapply (translate_dest_not_Evar_id alloc_type ? lhs_ty Hnot_evar)
1940          #Htranslate_dest * #Htranslate_dest'
1941          >Htranslate_dest' in Htranslate_dest; #Haux lapply (sym_eq ??? Haux) -Haux #Haux
1942          cases (bind_inversion ????? Haux) -Haux
1943          * #translated_dest #Hexpr_vars_dest * #Htranslate_addr
1944          whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) normalize nodelta
1945          cases (type_eq_dec ??)
1946          [ 2: #Hneq normalize nodelta whd in ⊢ ((??%%) → ?);
1947               #Habsurd destruct (Habsurd) ]
1948          normalize nodelta whd in match (typeof ?); #Heq_cl_types
1949          whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1950          #s2 #tr whd in ⊢ ((??%?) → ?); #Hstep
1951          cases (bindIO_inversion ??????? Hstep) -Hstep
1952          * * #cl_blo #cl_off #cl_tr * whd in ⊢ ((??%?) → ?);
1953          #Hexec_lvalue #Hstep
1954          lapply (translate_dest_MemDest_simulation …
1955                     INV' ???????? Halloc_hyp Hcl_env_hyp Hinjection Hmatching ??????
1956                     Htranslate_dest' Hexec_lvalue)
1957          [ 1: @(proj1 ?? (proj1 ?? (proj1 ?? sInv))) ]
1958          * #cm_val_dest * #Heval_cm_dest #Hvalue_eq_dest
1959          %{1} whd whd in ⊢ (??%?); normalize nodelta
1960          >Heval_cm_dest
1961          whd in match (m_bind ?????);
1962          cases (bindIO_inversion ??????? Hstep) -Hstep
1963          * #val #trace * #Hexec_expr #Hstep
1964          cases (bindIO_inversion ??????? Hstep) -Hstep
1965          #cl_mem_after_store * #Hopt_store
1966          whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
1967          lapply (opt_to_io_Value ?????? Hopt_store) -Hopt_store
1968          #Hstore_value_of_type whd in Hstore_value_of_type:(??%?);
1969          cases (eval_expr_sim … Halloc_hyp … Hcl_env_hyp … Hinjection … Hmatching) #Hsim_expr #_
1970          lapply (Hsim_expr … Htranslate_rhs … (proj2 ?? (proj1 ?? (proj1 ?? sInv))) Hexec_expr)
1971          * #cm_rhs_val generalize in match (proj2 ???);
1972          #Hexpr_vars_rhs * #Heval_expr_rhs #Hvalue_eq_rhs >Heval_expr_rhs
1973          normalize nodelta -Hsim_expr
1974          cases (store_value_of_type_success_by_value ? cl_m
1975                                    cl_mem_after_store ?? val Hstore_value_of_type)
1976          whd in match (typeof ?) in ⊢ ((??%%) → (??%?) → ?);
1977          #Haccess_mode #Hstorev -Hstore_value_of_type
1978          cases (value_eq_ptr_inversion … Hvalue_eq_dest) * #cm_blo #cm_off * #Hcm_val_dest destruct (Hcm_val_dest)
1979          whd in ⊢ ((??%?) → ?); #Hembed
1980          cases (some_inversion ????? Hembed) -Hembed
1981          * #cm_blo' #cm_off' * #Hembed normalize nodelta #Heq destruct (Heq)
1982          lapply (storen_parallel_aux ??? Hinjection … Hvalue_eq_rhs … Hembed ??? Hstorev)
1983          * #cm_mem_after_store_lhs * #Hstoren #Hinj whd in Hstoren:(??%?);
1984          whd in match (storev ????);
1985          lapply Hstoren
1986          (* make the types match *)
1987          generalize in match (conj ????); #Hstmt_vars' >Heq_cl_types
1988          #Hstoren >Hstoren
1989          whd in match (m_bind ?????); normalize nodelta whd @conj try @conj try @refl
1990          [ 2: #Habsurd destruct (Habsurd) ]
1991          @(CMR_normal … Halloc_hyp) try assumption
1992          [ 2: @refl | *: ]
1993          [ 1: (* lemma on well_allocated after CL and CM parallel writes *) @cthulhu
1994          | 2: (* memory matching *) @cthulhu ]
1995     ]
1996| *: @cthulhu ]
1997| 2: (* Return state *)
1998  @cthulhu
1999| 3: (* Call state, nostore *)
2000  @cthulhu
2001| 4: (* Call state, store *)
2002  @cthulhu
2003| 5: (* Intermediary While state *)
2004     (* ---------------------------------------------------------------------- *)
2005#cl_ge #cm_ge #INV'
2006#cl_f #cm_f #cl_env #cl_m #cm_env #cm_m #stackptr #stacksize #alloc_type
2007#cl_k #cm_k #sz #sg #cl_cond_desc #cl_body #entry_label #exit_label #cm_cond #cm_body
2008#cm_stack #kInv #fInv #sInv #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls
2009#Em #Htmp_vars_well_allocated #Halloc_hyp
2010#Hcl_env_hyp #Hinjection #Hmatching #Hexpr_vars #Htranslate_expr #target_type
2011#Htranslate_inv #Htranslate_statement
2012@(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
2013destruct (HA HB)
2014@(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
2015destruct (HC HD HE) #_
2016#s2 #tr whd in ⊢ ((??%?) → ?); #Hstep
2017(* execute clight condition *)
2018cases (bindIO_inversion ??????? Hstep) -Hstep
2019* #cl_cond_val #cl_cond_trace * #Hcl_exec_cond #Hstep
2020cases (bindIO_inversion ??????? Hstep) -Hstep
2021#cl_cond_bool * #Hcl_bool_of_val whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
2022(* The numbers of steps to execute in Cminor depends on the outcome of the condition
2023   evaluation *)
2024cases cl_cond_bool in Hcl_bool_of_val;
2025[ (* cond = true: continue looping *)
2026  #Hcl_bool_of_val
2027  %{4} whd whd in ⊢ (??%?); normalize nodelta
2028  generalize in match (proj1 ???); #Hpresent_ifthenelse
2029  (* Exhibit simulation of condition evaluation *)
2030  lapply (eval_expr_sim … Halloc_hyp … Hcl_env_hyp … Hinjection … Hmatching) * #Hsim #_
2031  lapply (Hsim … Hexpr_vars … Htranslate_expr ?? Hpresent_ifthenelse Hcl_exec_cond)
2032  * #cm_val_cond * #Hcm_eval_cond #Hvalue_eq >Hcm_eval_cond
2033  whd in match (m_bind ?????);
2034  >(eval_bool_of_val_to_Cminor … Hvalue_eq … Hcl_bool_of_val)
2035  normalize nodelta whd
2036  generalize in match (proj1 ???); #Hnoise'
2037  generalize in match (conj ????); #Hnoise'' @conj try @conj
2038  [ 3: #Habsurd destruct (Habsurd)
2039  | 1: normalize >append_nil @refl
2040  | 2: @cthulhu
2041       (* @(CMR_normal … Htranslate_statement) try assumption *)
2042       (* TODO: new continuation relation
2043        *       pump the necessary invariants up in CMR_while so that CMR_normal can complete here *)
2044  ]
2045| (* cond = false: stop looping *)
2046  #Hcl_bool_of_val
2047  %{3} whd whd in ⊢ (??%?); normalize nodelta
2048  generalize in match (proj1 ???); #Hpresent_ifthenelse
2049  (* Exhibit simulation of condition evaluation *)
2050  lapply (eval_expr_sim … Halloc_hyp … Hcl_env_hyp … Hinjection … Hmatching) * #Hsim #_
2051  lapply (Hsim … Hexpr_vars … Htranslate_expr ?? Hpresent_ifthenelse Hcl_exec_cond)
2052  * #cm_val_cond * #Hcm_eval_cond #Hvalue_eq >Hcm_eval_cond
2053  whd in match (m_bind ?????);
2054  >(eval_bool_of_val_to_Cminor … Hvalue_eq … Hcl_bool_of_val)
2055  normalize nodelta whd
2056  generalize in match (proj1 ???); #Hnoise'
2057  generalize in match (proj2 ???); #Hnoise''
2058  generalize in match (conj ????); #Hnoise'''
2059  @conj try @conj
2060  [ 3: #Habsurd destruct (Habsurd)
2061  | 1: normalize @refl
2062  | 2: @cthulhu
2063       (* @(CMR_normal … Htranslate_statement) try assumption *)
2064       (* TODO: new continuation relation
2065        *       pump the necessary invariants up in CMR_while so that CMR_normal can complete here *)
2066  ]
2067]
2068
2069] qed. 
2070
2071(* TODO: adapt the following to the new goal shape. *)
2072(*
2073axiom clight_cminor_call_return :
2074  ∀INV:clight_cminor_inv.
2075  ∀s1,s1',s2,tr.
2076  clight_cminor_rel INV s1 s1' →
2077  match Clight_classify s1 with [ cl_call ⇒ true | cl_return ⇒ true | _ ⇒ false ] →
2078  after_n_steps 1 … clight_exec (ge_cl INV) s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) →
2079  ∃m. after_n_steps (S m) … Cminor_exec (ge_cm INV) s1' (λs.cminor_normal s) (λtr',s2'.
2080    tr = tr' ∧
2081    clight_cminor_rel INV s2 s2'
2082  ).
2083
2084axiom clight_cminor_cost :
2085  ∀INV:clight_cminor_inv.
2086  ∀s1,s1',s2,tr.
2087  clight_cminor_rel INV s1 s1' →
2088  Clight_labelled s1 →
2089  after_n_steps 1 … clight_exec (ge_cl INV) s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) →
2090  after_n_steps 1 … Cminor_exec (ge_cm INV) s1' (λs.true) (λtr',s2'.
2091    tr = tr' ∧
2092    clight_cminor_rel INV s2 s2'
2093  ).
2094
2095axiom clight_cminor_init : ∀cl_program,cm_program,s,s'.
2096  clight_to_cminor cl_program = OK ? cm_program →
2097  make_initial_state ?? clight_fullexec cl_program = OK ? s →
2098  make_initial_state ?? Cminor_fullexec cm_program = OK ? s' →
2099  ∃INV. clight_cminor_rel INV s s'. *)
Note: See TracBrowser for help on using the repository browser.