source: src/Clight/toCminorCorrectness.ma @ 2838

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

Closing some more cases

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