Context Navigation

← Previous Changeset
Next Changeset →

Changeset 3036

Timestamp:

Mar 29, 2013, 5:12:09 PM (7 years ago)

Author:

garnier

Message:

Fixing some problems, progress, etc

File:

: 1 edited

src/Clight/toCminorCorrectness.ma (modified) (64 diffs)

Legend:

: Unmodified
: Added
: Removed

src/Clight/toCminorCorrectness.ma

-                      r2857
+                      r3036
     match u2 with
     [ mk_universe p2 ⇒ p2 ≤ p1 ] ].
 definition fte ≝ fresher_than_or_equal.
 …
 * // qed.
+definition labgen_include ≝
+  λgen1, gen2 : labgen.
+  ∃labels. label_genlist gen2 = labels @ label_genlist gen1.
+definition tmpgen_include ≝
+  λvartypes.
+  λgen1, gen2 : tmpgen vartypes.
+  ∃idents. tmp_env ? gen2 = idents @ (tmp_env ? gen1).
+(* Express that the [first] tmpgen generates "newer" ids than an other one. *)
+definition tmpgen_fresher_than ≝
+  λvars. λgen1, gen2 : tmpgen vars.
+    fresher_than_or_equal (tmp_universe … gen1) (tmp_universe … gen2).
+(* Map a predicate on all the /keys/ of an environment, i.e. on a set
+ * of identifiers. *)
+definition env_domain_P : cl_env → ∀P:(ident → Prop). Prop ≝
+ λe, P.
+  match e with
+  [ an_id_map m ⇒
+    fold ?? (λkey,elt,acc. P (an_identifier ? key) ∧ acc) m True
+  ].
+(* Property for an identifier to be out of the set
+ * of identifiers represented by an universe. *)
+definition ident_below_universe ≝
+  λi: ident.
+  λu: universe SymbolTag.
+  match i with
+  [ an_identifier id ⇒
+    match u with
+    [ mk_universe id_u ⇒
+      id < id_u
+    ]
+  ].
+(* Property of the domain of an environment to be disjoint of the set
+ * of identifiers represented by an universe. *)
+definition env_below_freshgen : env → ∀vars. tmpgen vars → Prop ≝
+  λe, vars, tmpgen.
+  env_domain_P e (λid. ident_below_universe id (tmp_universe … tmpgen)).
+(* The property of interest for the proof. Identifiers generated from an
+ * universe above the environment are not in the said environment. *)
+lemma lookup_fails_outside_of_env :
+  ∀env, vars, ty, gen, id, gen'.
+  alloc_tmp vars ty gen = 〈id, gen'〉 →
+  env_below_freshgen env vars gen →
+  lookup ?? env id = None ?.
+@cthulhu
+qed.
+(* The property of being above an environment is conserved by fresh ident
+ * generation *)
+lemma alloc_tmp_env_invariant :
+  ∀env, vars, ty, gen, id, gen'.
+  alloc_tmp vars ty gen = 〈id, gen'〉 →
+  env_below_freshgen env vars gen →
+  env_below_freshgen env vars gen'.
+@cthulhu
+qed.
 (* --------------------------------------------------------------------------- *)
 …
 (* Temporary variables generated during conversion are well-allocated. *)
 definition tmp_vars_well_allocated ≝
+   λvartypes.
+   λtmp_gen: tmpgen vartypes.
+   λtmpenv: list (ident × type).
    λcm_env.
    λcm_m.
 …
    ∀local_variable.
    ∀H:present ?? cm_env local_variable.
    ∀ty. Exists ? (λx. x = 〈local_variable, ty〉) (tmp_env … tmp_gen) →
+   ∀ty. Exists ? (λx. x = 〈local_variable, ty〉) tmpenv →
    ∀v. val_typ v (typ_of_type ty) →
    ∃cm_m'. storev (typ_of_type ty) cm_m (lookup_present ?? cm_env local_variable H) v = Some ? cm_m' ∧
 …
 (* --------------------------------------------------------------------------- *)
-record frame_data
-  (f : function)
-  (ge_cl : genv_t clight_fundef)
-  (ge_cm : genv_t (fundef internal_function))
-  (INV : clight_cminor_inv ge_cl ge_cm) : Type[0] ≝
+{
-}.
 definition CMcast : ∀t,t'. CMexpr t → t = t' → CMexpr t'.
 #t #t' #e #H destruct (H) @e
 …
   ∀cl_f: function.                          (* current Clight function *)
   internal_function →                       (* current Cminor function *)
+  cl_env →
+  cm_env →
+  var_types →
+  (*frame_data cl_f cl_ge cm_ge INV →*)         (* data for the current stack frame in CL and CM *)
+  option typ →                              (* optional target type - uniform over a given function *)
+  cl_env →                                  (* Clight local environment *)
+  cm_env →                                  (* Cminor local environment *)
+  mem →                                     (* Cminor memory state *)
+  ∀alloc_type:var_types.                    (* map vars to alloc type *)
+  ∀tmpenv:list (ident×type).                (* list of generated variables *)
+  (*tmpgen alloc_type →                       (* input freshgen *)
+    tmpgen alloc_type →                       (* output freshgen *) *) (* bad idea *)
+  option typ →                              (* optional target type - arg. uniform over a given function *)
   cl_cont →                                 (* CL cont *)
   cm_cont →                                 (* CM cont *)
   stack →                                   (* CM stack *)
+  stack →                                   (* CM stack *)
   Prop ≝
 (* Stop continuation*)
+(* Stop continuation *)
 | ClCm_cont_stop:
   ∀cl_ge, cm_ge, INV, cl_f, cm_f, target_type.
   ∀cl_env, cm_env, alloc_type.
+  ∀cl_env, cm_env, cm_m, alloc_type, tmpenv. (*, stmt_univ, stmt_univ'.*)
   ∀cm_stack.
   cm_stack = SStop →
   clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type target_type Kstop Kend cm_stack
+  clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env cm_m alloc_type tmpenv (* stmt_univ stmt_univ' *) target_type Kstop Kend cm_stack
 (* Seq continuation *)
 …
   ∀stack.
   ∀alloc_type.
+  ∀tmpenv.
   ∀cl_s: statement.
   ∀cm_s: stmt.
   ∀cl_env: cl_env.
   ∀cm_env: cm_env.
+  ∀cm_m: mem.
   ∀cl_k': cl_cont.
   ∀cm_k': cm_cont.
 …
   (* ---- invariant on label existence ---- *)
   lset_inclusion ? (labels_of cm_s) (labels_of (f_body cm_f)) →
+  clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type target_type cl_k' cm_k' stack →
+  clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type target_type (ClKseq cl_s cl_k') (Kseq cm_s cm_k') stack
+  (* ---- invariant on fresh variables ---- *)
+  lset_inclusion ? (tmp_env alloc_type stmt_univ') tmpenv →
+  clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env cm_m alloc_type tmpenv (*stmt_univ stmt_univ'*) target_type cl_k' cm_k' stack →
+  clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env cm_m alloc_type tmpenv (*stmt_univ stmt_univ'*) target_type (ClKseq cl_s cl_k') (Kseq cm_s cm_k') stack
 (* While continuation *)
 …
   ∀stack.
   ∀alloc_type.
+  ∀tmpenv.
   ∀cl_env.
   ∀cm_env.
+  ∀cm_m.
   (* sub-continuations *)
   ∀cl_k': cl_cont.
   ∀cm_k': cm_cont.
   (* elements of the source while statement *)
   ∀sz,sg.
 …
   ∀cl_body.
   ∀Heq: ASTint sz sg = typ_of_type cl_ty.
   (* elements of the converted while statement *)
   ∀cm_cond: CMexpr (ASTint sz sg).
   ∀cm_body.
+  ∀entry,exit: identifier Label.
+  ∀entry,exit: identifier Label.
   (* universes used to generate fresh labels and variables *)
   ∀stmt_univ, stmt_univ'.
 …
   ∀lbls: lenv.
   ∀Htranslate_inv.
   (* relate CL and CM expressions *)
+  ∀Hexpr_vars.
+  translate_expr alloc_type (Expr cl_cond_desc cl_ty) = OK ? («CMcast ?? cm_cond Heq, Hexpr_vars») →
+  ∀Hexpr_vars:expr_vars ? cm_cond (local_id alloc_type).
+  translate_expr alloc_type (Expr cl_cond_desc cl_ty) ≃ OK ? («cm_cond, Hexpr_vars») →
   (* Parameters and results to find_label_always *)
   ∀sInv: stmt_inv cm_f cm_env (f_body cm_f).
   ∀Hlabel_declared: Exists (identifier Label) (λl'.l'=entry) (labels_of (f_body cm_f)).
   ∀Hinv.
   (* Specify how the labels for the while-replacing gotos are produced *)
   mklabels lbl_univ = 〈〈entry, exit〉, lbl_univ'〉 →
   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» →
+  (* Invariant on label existence *)
+  lset_inclusion ? (labels_of cm_body) (labels_of (f_body cm_f)) →
+  (* ---- Invariant on label existence ----  *)
+  lset_inclusion ? (labels_of cm_body) (labels_of (f_body cm_f)) →
+  (* ---- invariant on fresh variables ---- *)
+  lset_inclusion ? (tmp_env alloc_type stmt_univ') tmpenv →
   find_label_always entry (f_body cm_f) Kend Hlabel_declared cm_f cm_env sInv I =
     «〈(*St_label entry*)
 …
             (St_ifthenelse ?? cm_cond (St_seq cm_body (St_goto entry)) St_skip)
             (St_label exit St_skip)), cm_k'〉, Hinv» →
+  clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type target_type cl_k' cm_k' stack →
+  clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type target_type (
+    Kwhile (Expr cl_cond_desc cl_ty) cl_body cl_k')
+    (Kseq (St_goto entry) (Kseq (St_label exit St_skip) cm_k')) stack.
+(* TODO: Kcall *)
+(* TODO XXX *)
+(* relation between placeholders for return values *)
+definition return_value_rel :
+  ∀cl_f, cl_ge, cm_ge.
+  ∀INV: clight_cminor_inv cl_ge cm_ge.
+  frame_data cl_f ?? INV →
+  option (block×offset×type) → option (ident×typ) → Prop ≝
+λcl_f, cl_ge, cm_ge, INV, data, opt1, opt2.
+match opt1 with
+[ None ⇒
+  match opt2 with
+  [ None ⇒ True
+  | _ ⇒ False ]
+| Some ptr ⇒
+  match opt2 with
+  [ Some id ⇒ True (* TODO, here. *)
+  | None ⇒ False
+  ]
+].
+  clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env cm_m alloc_type tmpenv (* stmt_univ stmt_univ' *) target_type cl_k' cm_k' stack →
+  clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env cm_m alloc_type tmpenv (* stmt_univ stmt_univ' *) target_type
+    (Kwhile (Expr cl_cond_desc cl_ty) cl_body cl_k')
+    (Kseq (St_goto entry) (Kseq (St_label exit St_skip) cm_k')) stack
+| ClCm_cont_call_store:
+  ∀cl_ge, cm_ge, INV, cl_f, cm_f, target_type.
+  ∀stack.
+  ∀alloc_type.
+  ∀tmp_env.
+  ∀cl_env.
+  ∀cm_env.
+  ∀cm_m.
+  (* sub-continuations *)
+  ∀cl_k': cl_cont.
+  ∀cm_k': cm_cont.
+  (* CL return addr *)
+  ∀CL_lvalue_block,CL_lvalue_offset,lhs_ty.
+  ∀CM_lvalue_ptr.
+  (* CM stack content *)
+  ∀stackptr.
+  ∀fInv.
+  ∀tmp_var, ret_var.
+  ∀Htmp_var_present.
+  ∀Hret_present.
+  ∀Hstmt_inv.
+  (* TODO: loads of invariants *)
+  clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env cm_m alloc_type tmp_env (*stmt_univ stmt_univ*) target_type
+    (Kcall (Some ? 〈CL_lvalue_block, CL_lvalue_offset, lhs_ty〉) cl_f cl_env cl_k')
+    cm_k'
+    (Scall (Some ? 〈ret_var,typ_of_type lhs_ty〉) cm_f stackptr
+     (update_present SymbolTag val cm_env tmp_var Htmp_var_present (Vptr CM_lvalue_ptr)) Hret_present
+     (stmt_inv_update cm_f cm_env (f_body cm_f) tmp_var (Vptr CM_lvalue_ptr) fInv Htmp_var_present)
+     (Kseq
+      (St_store (typ_of_type lhs_ty) (Id ASTptr tmp_var)
+       (Id (typ_of_type lhs_ty) ret_var)) cm_k') Hstmt_inv stack)
+| ClCm_cont_call_nostore:
+  ∀cl_ge, cm_ge, INV, cl_f, cm_f, target_type.
+  ∀stack.
+  ∀alloc_type.
+  ∀tmpenv.
+  ∀cl_env.
+  ∀cm_env.
+  ∀cm_m.
+  (* sub-continuations *)
+  ∀cl_k': cl_cont.
+  ∀cm_k': cm_cont.
+  (* CM stack content *)
+  ∀cl_lhs, cm_lhs.
+  match cl_lhs with
+  [ None ⇒ match cm_lhs with [ None ⇒ True | _ ⇒ False ]
+  | Some cl_location ⇒
+    match cm_lhs with
+    [ None ⇒ False
+    | Some cm_location ⇒
+      ∃CL_lvalue_block, CL_lvalue_offset, lhs_ty, ret_var.
+       cl_location = 〈CL_lvalue_block,CL_lvalue_offset, lhs_ty〉 ∧
+       cm_location = 〈ret_var, typ_of_type lhs_ty〉
+    ]
+  ] →
+  ∀Hret_present.
+  ∀Hstmt_inv.
+  ∀stackptr.
+  ∀fInv.
+(*  ∀stmt_univ.*)
+  clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env cm_m alloc_type tmpenv (*stmt_univ stmt_univ*) target_type
+   (Kcall cl_lhs cl_f cl_env cl_k')
+    cm_k'
+   (Scall cm_lhs cm_f stackptr cm_env Hret_present fInv cm_k' Hstmt_inv stack).
+lemma translate_fundef_internal :
+  ∀ge1, ge2.
+  ∀INV: clight_cminor_inv ge1 ge2.
+  ∀u, cl_f, cm_fundef.
+  ∀H1, H2.
+  translate_fundef u (globals ?? INV) H1 (CL_Internal cl_f) H2 = OK ? cm_fundef →
+  ∃cm_f. cm_fundef = Internal ? cm_f ∧
+         translate_function u (globals ge1 ge2 INV) cl_f H1 H2 = OK ? cm_f.
+#ge1 #ge2 #INV #u #cl_f #cm_fd #H1 #H2
+whd in ⊢ ((??%?) → ?); cases (translate_function u (globals ge1 ge2 INV) cl_f H1 H2)
+normalize nodelta
+[ 2: #er #Habsurd destruct (Habsurd)
+| 1: #cm_f #Heq destruct (Heq) %{cm_f} @conj @refl ]
+qed.
+lemma translate_fundef_external :
+  ∀ge1, ge2.
+  ∀INV: clight_cminor_inv ge1 ge2.
+  ∀u, id, tl, ty.
+  ∀H1, H2.
+  translate_fundef u (globals ?? INV) H1 (CL_External id tl ty) H2 =
+    OK ? (External ? (mk_external_function id (signature_of_type tl ty))).
+#ge1 #ge2 #INV #u #id #tl #ty #H1 #H2 @refl
+qed.
 (* Definition of the simulation relation on states. The orders of the parameters is dictated by
  * the necessity of performing an inversion on the continuation sim relation without having to
  * play the usual game of lapplying all previous dependent arguments.  *)
 inductive clight_cminor_rel : ∀cl_ge, cm_ge. clight_cminor_inv cl_ge cm_ge  → Clight_state → Cminor_state → Prop ≝
+(* --------------------------------------------------------------------------- *)
+(* normal state *)
+(* --------------------------------------------------------------------------- *)
 | CMR_normal :
   (* Clight and Cminor global envs *)
 …
   ∀kInv: cont_inv cm_f cm_env cm_k.
   (* ---- relate return type variable to actual return type ---- *)
   rettyp = opttyp_of_type (fn_return cl_f) →
+  rettyp = opttyp_of_type (fn_return cl_f) →
   (* ---- relate Clight and Cminor functions ---- *)
   ∀func_univ: universe SymbolTag.
 …
   lset_inclusion ? (labels_of cm_s) (labels_of (f_body cm_f)) →
   (* ---- relate Clight continuation to Cminor continuation ---- *)
+  clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type rettyp cl_k cm_k cm_st →
+  ∀tmpenv.
+  lset_inclusion ? (tmp_env ? stmt_univ') tmpenv →
+  clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env cm_m alloc_type tmpenv (*stmt_univ stmt_univ'*) rettyp cl_k cm_k cm_st →
   (* ---- state invariants for memory and environments ---- *)
   (* Embedding *)
   ∀Em: embedding.
   (* locals are properly allocated *)
   tmp_vars_well_allocated alloc_type stmt_univ' cm_env cm_m cl_m Em →
+  tmp_vars_well_allocated tmpenv cm_env cm_m cl_m Em →
   (* specify how alloc_type is built *)
   characterise_vars (globals ?? INV) cl_f = 〈alloc_type, stacksize〉 →
 …
   (∀b1.∀delta. Em b1=Some ? 〈stackptr,delta〉 →
                mem block b1 (blocks_of_env cl_env)) →
+  (* The fresh name generator is compatible with the clight environment *)
+  env_below_freshgen cl_env alloc_type stmt_univ →
   clight_cminor_rel cl_ge cm_ge INV
     (ClState cl_f cl_s cl_k cl_env cl_m)
     (CmState cm_f cm_s cm_env fInv sInv cm_m stackptr cm_k kInv cm_st)
+(* --------------------------------------------------------------------------- *)
+(* return state *)
+(* --------------------------------------------------------------------------- *)
 | CMR_return :
+  (* Clight and Cminor global envs *)
   ∀cl_ge, cm_ge.
+  (* Relates globals to globals and functions to functions. *)
   ∀INV: clight_cminor_inv cl_ge cm_ge.
+  ∀cl_f: function.                               (* Clight enclosing function *)
+  ∀cm_f: internal_function.                             (* enclosing function *)
+  (* ---- Continuations and functions ---- *)
+  (* Clight continuation *)
+  ∀cl_k: cl_cont.
+  (* Cminor continuation *)
+  ∀cm_k: cm_cont.
+  (* Cminor stack *)
+  ∀cm_st: stack.
+  (* Clight enclosing function *)
+  ∀cl_f: function.
+  (* Cminor enclosing function *)
+  ∀cm_f: internal_function.
+  (* mapping from variables to their Cminor alloc type *)
   ∀alloc_type.
+  (* Clight env/mem *)
   ∀cl_env, cl_m.
+  (* Cminor env/mem *)
   ∀cm_env, cm_m.
   ∀cm_st: stack.                                              (* Cminor stack *)
+  (* Stack pointer (block containing Cminor locals), related size *)
   ∀stackptr, stacksize.
+  ∀stmt_univ.
+  (* fresh label generator *)
+  ∀stmt_univ: tmpgen alloc_type.
+  ∀tmpenv.
+  lset_inclusion ? (tmp_env ? stmt_univ) tmpenv →
+  (* ---- state invariants for memory and environments ---- *)
+  (* Embedding *)
   ∀Em: embedding.
+  tmp_vars_well_allocated alloc_type stmt_univ cm_env cm_m cl_m Em →        (* locals are properly allocated *)
+  characterise_vars (globals ?? INV) cl_f = 〈alloc_type, stacksize〉 →        (* specify how alloc_type is built *)
+  (∃m,m'. exec_alloc_variables empty_env m (fn_params cl_f @ fn_vars cl_f) = 〈cl_env,m'〉) → (* spec. Clight env *)
+  memory_inj Em cl_m cm_m →                                                  (* memory injection *)
+  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 *)
+  (∀b. block_region b = Code → Em b = Some ? 〈b, zero_offset〉) →             (* Force embedding to compute identity on functions *)
+  (* locals are properly allocated *)
+  tmp_vars_well_allocated tmpenv cm_env cm_m cl_m Em →
+  (* specify how alloc_type is built *)
+  characterise_vars (globals ?? INV) cl_f = 〈alloc_type, stacksize〉 →
+  (* spec. Clight env at alloc time *)
+  (∃m,m'. exec_alloc_variables empty_env m (fn_params cl_f @ fn_vars cl_f) = 〈cl_env,m'〉) →
+  (* memory injection *)
+  memory_inj Em cl_m cm_m →
+  (* map CL env to CM env *)
+  memory_matching Em cl_ge cm_ge cl_m cm_m cl_env cm_env INV stackptr alloc_type →
+  (* Force embedding to compute identity on functions *)
+  (∀b. block_region b = Code → Em b = Some ? 〈b, zero_offset〉) →
   (* Make explicit the fact that locals in CL are mapped to a single CM block *)
   (∀b1.∀delta. Em b1=Some ? 〈stackptr,delta〉 →
+               mem block b1 (blocks_of_env cl_env)) →
+               mem block b1 (blocks_of_env cl_env)) →
+  clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env cm_m alloc_type tmpenv (*stmt_univ stmt_univ*) (None ?) cl_k cm_k cm_st →
   clight_cminor_rel cl_ge cm_ge INV
     (ClReturnstate Vundef Kstop cl_m)
+    (ClReturnstate Vundef cl_k cl_m)
     (CmReturnstate (None val) cm_m cm_st)
+| CMR_call_nostore :
+ (* call to a function with no return value, or which returns in a local variable in Cminor *)
+ ∀cl_ge, cm_ge, cl_f, cm_f.
+ ∀INV: clight_cminor_inv cl_ge cm_ge.
+ ∀alloc_type, cl_env, cl_m, cm_env, cm_m, cm_stack, stackptr.
+ (* TODO: put the actual invariants on memory and etc. here *)
+ ∀u: universe SymbolTag.
+ ∀cl_fundef, cm_fundef.
+ ∀Hglobals_fresh: globals_fresh_for_univ type (globals cl_ge cm_ge INV) u.
+ ∀Hfundef_fresh:  fd_fresh_for_univ cl_fundef u.
+ ∀rettyp. rettyp = opttyp_of_type (fn_return cl_f) →
+ ∀cl_k, cm_k.
+ ∀fblock.
+ match cl_fundef with
+ [ CL_Internal cl_function ⇒
+    find_funct clight_fundef cl_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? (CL_Internal cl_function) ∧
+    find_funct (fundef internal_function) cm_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? cm_fundef ∧
+    translate_fundef u (globals ?? INV) Hglobals_fresh cl_fundef Hfundef_fresh = OK ? cm_fundef ∧
+    clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type rettyp cl_k cm_k cm_stack
+ | CL_External name argtypes rettype ⇒
+   True
+ ] →
+ ∀cl_fun_id, cm_fun_id.
+ cl_fun_id = cm_fun_id →
+ ∀cl_retval, cm_retval.
+ ∀sInv, fInv, kInv.
+ ∀cl_args_values, cm_args_values.
+ (* TODO: return_value_rel … INV frame_data cl_retval cm_retval →*)
+ (* TODO: add invariant All2 value_eq cl_args_values cm_args_values *)
+ clight_cminor_rel cl_ge cm_ge INV
+  (ClCallstate cl_fun_id
+   cl_fundef cl_args_values (Kcall cl_retval cl_f cl_env cl_k) cl_m)
+  (CmCallstate cm_fun_id cm_fundef
+   cm_args_values cm_m (Scall cm_retval cm_f stackptr cm_env sInv fInv cm_k kInv cm_stack))
+| CMR_call_store :
+ (* call to a function which returns to some location in memory in Cminor *)
+ ∀cl_ge, cm_ge, cl_f, cm_f.
+ ∀INV: clight_cminor_inv cl_ge cm_ge.
+ ∀alloc_type, cl_env, cl_m, cm_env, cm_m, cm_stack, stackptr.
+ (* TODO: put the actual invariants on memory and etc. here *)
+ ∀u: universe SymbolTag.
+ ∀cl_fundef, cm_fundef.
+ ∀Hglobals_fresh: globals_fresh_for_univ type (globals cl_ge cm_ge INV) u.
+ ∀Hfundef_fresh:  fd_fresh_for_univ cl_fundef u.
+ ∀rettyp. rettyp = opttyp_of_type (fn_return cl_f) →
+ ∀cl_k, cm_k.
+ ∀fblock.
+ match cl_fundef with
+ [ CL_Internal cl_function ⇒
+    find_funct clight_fundef cl_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? (CL_Internal cl_function) ∧
+    find_funct (fundef internal_function) cm_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? cm_fundef ∧
+    translate_fundef u (globals ?? INV) Hglobals_fresh cl_fundef Hfundef_fresh = OK ? cm_fundef ∧
+    clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type rettyp cl_k cm_k cm_stack
+ | CL_External name argtypes rettype ⇒
+   True
+ ] →
+ ∀cl_fun_id, cm_fun_id.
+ cl_fun_id = cm_fun_id →
+ ∀cl_rettyp, cl_retval, cl_rettrace, cm_retval.
+ ∀cl_lhs, cm_lhs, Hinvariant_on_cm_lhs.
+ (* Explain where the lhs of the post-return assign comes from *)
+ exec_lvalue cl_ge cl_env cl_m cl_lhs = OK ? 〈cl_retval, cl_rettrace〉 →
+ translate_dest alloc_type cl_lhs = OK ? (MemDest ? «cm_lhs, Hinvariant_on_cm_lhs») →
+ (* TODO: Explain that the actual variable used to store the ret val is fresh and has the
+  * right type, etc *)
+ ∀cm_ret_var.
+ ∀sInv, fInv, kInv.
+ ∀cl_args_values, cm_args_values.
+ (* TODO: return_value_rel … INV frame_data cl_retval cm_retval →*)
+ (* TODO: add invariant All2 value_eq cl_args_values cm_args_values *)
+ ∀cm_stack.
+ clight_cminor_rel cl_ge cm_ge INV
+  (ClCallstate cl_fun_id
+   cl_fundef cl_args_values (Kcall (Some ? 〈cl_retval,cl_rettyp〉) cl_f cl_env cl_k) cl_m)
+  (CmCallstate cm_fun_id cm_fundef
+   cm_args_values cm_m (Scall cm_retval cm_f stackptr cm_env sInv fInv
+                          (Kseq (St_store (typ_of_type cl_rettyp) cm_lhs
+                                          (Id (typ_of_type cl_rettyp) cm_ret_var)) cm_k)
+                           kInv cm_stack))
+(* --------------------------------------------------------------------------- *)
+(* call state *)
+(* --------------------------------------------------------------------------- *)
+| CMR_call :
+  (* Clight and Cminor global envs *)
+  ∀cl_ge, cm_ge.
+  (* Relates globals to globals and functions to functions. *)
+  ∀INV:  clight_cminor_inv cl_ge cm_ge.
+  (* ------- Continuations and functions for the current stack frame -------- *)
+  (* Clight continuation *)
+  ∀cl_k: cl_cont.
+  (* Cminor continuation *)
+  ∀cm_k: cm_cont.
+  (* Cminor stack *)
+  ∀cm_st: stack.
+  (* Clight enclosing function *)
+  ∀cl_f: function.
+  (* Cminor enclosing function *)
+  ∀cm_f: internal_function.
+  (* Clight called fundef *)
+  ∀cl_fundef.
+  (* Cminor called fundef *)
+  ∀cm_fundef.
+  (* block of Clight and Cminor function *)
+  (* XXX why do I need that already ? *)
+  ∀fblock: block.
+  (* optional return type of the function *)
+  ∀target_type.
+  (* mapping from variables to their Cminor alloc type *)
+  ∀alloc_type.
+  (* Clight env/mem *)
+  ∀cl_env, cl_m.
+  (* Cminor env/mem *)
+  ∀cm_env, cm_m.
+  (* Stack pointer (block containing Cminor locals), stack frame size *)
+  ∀stackptr, stacksize.
+  (* fresh label generator for function *)
+  ∀func_univ: universe SymbolTag.
+  (* relate CL and CM enclosing functions *)
+  ∀Hglobals_fresh, Hfundef_fresh.
+  translate_function func_univ (globals ?? INV) cl_f Hglobals_fresh Hfundef_fresh = OK ? cm_f →
+  (* specify fblock *)
+  find_funct clight_fundef cl_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? cl_fundef →
+  find_funct (fundef internal_function) cm_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? cm_fundef →
+  ∀cl_fun_id, cm_fun_id.
+  ∀stmt_univ: tmpgen alloc_type.
+  ∀tmpenv.
+  lset_inclusion ? (tmp_env ? stmt_univ) tmpenv →
+  match cl_fundef with
+  [ CL_Internal _ ⇒
+     (* specify continuation *)
+     clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env cm_m alloc_type tmpenv target_type cl_k cm_k cm_st
+(*       ∨
+     (∃cl_blo, cl_off, cl_ty.         (* Clight return loscation + type *)
+      ∃cm_loc_ident, cm_return_ident. (* Cminor locals storing the lvalues *)
+      ∃sInv, fInv, kInv.              (* Invariants required by the stack construction *)
+       present ?? cm_env cm_loc_ident ∧
+       present ?? cm_env cm_return_ident ∧
+       (clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env cm_m alloc_type target_type
+          (Kcall (Some ? 〈cl_blo, cl_off, cl_ty〉) cl_f cl_env cl_k)
+           cm_k (Scall (Some ? 〈cm_return_ident,typ_of_type cl_ty〉) cm_f stackptr cm_env sInv fInv
+                     (Kseq (St_store (typ_of_type cl_ty) (Id ? cm_loc_ident) (Id ? cm_return_ident)) cm_k)
+                      kInv cm_st))) *)
+  | CL_External cl_id cl_argtypes cl_rettype ⇒
+    match cm_fundef with
+    [ Internal _ ⇒ False
+    | External cm_f_ext ⇒ True ]
+(*      match cm_f_ext with
+      [ mk_external_function cm_id sig ⇒
+        cl_fun_id = cl_id ∧ cm_fun_id = cm_id ∧ cl_fun_id = cm_fun_id
+      ] *)
+  ] →
+  (* ---- state invariants for memory and environments ---- *)
+  (* Embedding *)
+  ∀Em: embedding.
+  (* locals are properly allocated *)
+  tmp_vars_well_allocated tmpenv cm_env cm_m cl_m Em →
+  (* specify how alloc_type is built *)
+  characterise_vars (globals ?? INV) cl_f = 〈alloc_type, stacksize〉 →
+  (* spec. Clight env at alloc time *)
+  (∃m,m'. exec_alloc_variables empty_env m (fn_params cl_f @ fn_vars cl_f) = 〈cl_env,m'〉) →
+  (* memory injection *)
+  memory_inj Em cl_m cm_m →
+  (* map CL env to CM env *)
+  memory_matching Em cl_ge cm_ge cl_m cm_m cl_env cm_env INV stackptr alloc_type →
+  (* Force embedding to compute identity on functions *)
+  (∀b. block_region b = Code → Em b = Some ? 〈b, zero_offset〉) →
+  (* Make explicit the fact that locals in CL are mapped to a single CM block *)
+  (∀b1.∀delta. Em b1=Some ? 〈stackptr,delta〉 →
+               mem block b1 (blocks_of_env cl_env)) →
+  ∀cl_args_values, cm_args_values.
+  All2 val val (λcl_val:val.λcm_val:val.value_eq Em cl_val cm_val) cl_args_values cm_args_values →
+  clight_cminor_rel cl_ge cm_ge INV
+   (ClCallstate cl_fun_id cl_fundef cl_args_values cl_k cl_m)
+   (CmCallstate cm_fun_id cm_fundef cm_args_values cm_m cm_st)
+(* --------------------------------------------------------------------------- *)
+(* special while state *)
+(* --------------------------------------------------------------------------- *)
 | CMR_while:
  ∀cl_ge,cm_ge,INV,cl_f,cm_f.
 …
  translate_function func_univ (globals ?? INV) cl_f Hfresh_globals Hfresh_function = OK ? cm_f →
  (* ---- relate continuations ---- *)
- clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type rettyp cl_k cm_k cm_stack →
  ∀stmt_univ,stmt_univ',lbl_univ,lbl_univ',lbl_univ'',lbls.
+ ∀tmpenv'.
+ lset_inclusion ? (tmp_env ? stmt_univ') tmpenv' →
+ clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env cm_m alloc_type tmpenv' rettyp cl_k cm_k cm_stack →
  (* Invariants *)
  ∀Em: embedding.
  tmp_vars_well_allocated alloc_type stmt_univ' cm_env cm_m cl_m Em →        (* locals are properly allocated *)
+ tmp_vars_well_allocated tmpenv' cm_env cm_m cl_m Em →        (* locals are properly allocated *)
  characterise_vars (globals ?? INV) cl_f = 〈alloc_type, stacksize〉 →        (* specify how alloc_type is built *)
  (∃m,m'. exec_alloc_variables empty_env m (fn_params cl_f @ fn_vars cl_f) = 〈cl_env,m'〉) → (* spec. Clight env *)
 …
  (∀b. block_region b = Code → Em b = Some ? 〈b, zero_offset〉) →             (* Force embedding to compute identity on functions *)
  (* Make explicit the fact that locals in CL are mapped to a single CM block *)
  (∀b1.∀delta. Em b1=Some ? 〈stackptr,delta〉 →
+ (∀b1.∀delta. Em b1 = Some ? 〈stackptr,delta〉 →
               mem block b1 (blocks_of_env cl_env)) →
+ (* The fresh name generator is compatible with the clight environment *)
+ env_below_freshgen cl_env alloc_type stmt_univ →
  (* Expression translation and related hypotheses *)
+ ∀Hcond_tr.  (* invariant after converting conditional expr *)
+ translate_expr alloc_type (Expr cl_cond_desc cl_ty) = OK ? «CMcast ?? cm_cond Heq_ty, Hcond_tr » →
+ ∀Hcond_tr:expr_vars ? cm_cond (local_id alloc_type).  (* invariant after converting conditional expr *)
+ (* translate_expr alloc_type (Expr cl_cond_desc cl_ty) = OK ? «CMcast ?? cm_cond Heq_ty, Hcond_tr » → *)
+ translate_expr alloc_type (Expr cl_cond_desc cl_ty) ≃ OK ? «cm_cond, Hcond_tr » →
  (* Label consistency *)
  Exists ? (λl':identifier Label.l'=entry_label) (labels_of (f_body cm_f)) →
 …
      (St_ifthenelse sz sg cm_cond (St_seq cm_body (St_goto entry_label)) St_skip)
      (St_label exit_label St_skip)))
+   cm_env fInv sInv cm_m stackptr cm_k kInv cm_stack)).
+   cm_env fInv sInv cm_m stackptr cm_k kInv cm_stack)).
+(*
+| CMR_call_nostore :
+ (* call to a function with no return value, or which returns in a local variable in Cminor *)
+ ∀cl_ge, cm_ge. (* cl_f, cm_f.*)
+ ∀INV: clight_cminor_inv cl_ge cm_ge.
+ ∀alloc_type, cl_env, cl_m, cm_env, cm_m, cm_stack, stackptr.
+ (* TODO: put the actual invariants on memory and etc. here *)
+ ∀func_univ: universe SymbolTag.
+ ∀cl_f, cm_f.
+ ∀Hglobals_fresh: globals_fresh_for_univ type (globals cl_ge cm_ge INV) func_univ.
+ ∀Hfundef_fresh:  fd_fresh_for_univ (CL_Internal cl_f) func_univ.
+ ∀rettyp.
+ ∀cl_k, cm_k.
+ ∀fblock.
+ rettyp = opttyp_of_type (fn_return cl_f) ∧
+ find_funct clight_fundef cl_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? (CL_Internal cl_f) →
+ find_funct (fundef internal_function) cm_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? (Internal ? cm_f) →
+ translate_function func_univ (globals ?? INV) cl_f Hglobals_fresh Hfundef_fresh = OK ? cm_f →
+ clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type rettyp cl_k cm_k cm_stack →
+ ∀fun_id.
+ ∀cl_retval, cm_retval.
+ ∀sInv, fInv, kInv.
+ ∀cl_args_values, cm_args_values.
+ All2 val val (λcl_val:val.λcm_val:val.value_eq Em cl_val cm_val) cl_args_values cm_args_values →
+ (* TODO: return_value_rel … INV frame_data cl_retval cm_retval →*)
+ clight_cminor_rel cl_ge cm_ge INV
+  (ClCallstate fun_id (CL_Internal cl_f) cl_args_values cl_k cl_m)
+  (CmCallstate fun_id (Internal ? cm_f) cm_args_values cm_m cm_stack)
+| CMR_call_store :
+ (* call to a function which returns to some location in memory in Cminor *)
+ ∀cl_ge, cm_ge.
+ ∀INV: clight_cminor_inv cl_ge cm_ge.
+ ∀alloc_type, cl_env, cl_m, cm_env, cm_m, cm_stack, stackptr.
+ (* TODO: put the actual invariants on memory and etc. here *)
+ ∀func_univ: universe SymbolTag.
+ ∀cl_f, cm_f.
+ ∀Hglobals_fresh: globals_fresh_for_univ type (globals cl_ge cm_ge INV) func_univ.
+ ∀Hfundef_fresh:  fd_fresh_for_univ (CL_Internal cl_f) func_univ.
+ ∀rettyp.
+ ∀cl_k, cm_k.
+ ∀fblock.
+ rettyp = opttyp_of_type (fn_return cl_f) →
+ find_funct clight_fundef cl_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? (CL_Internal cl_f) →
+ find_funct (fundef internal_function) cm_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? (Internal ? cm_f) →
+ translate_function func_univ (globals ?? INV) cl_f Hglobals_fresh Hfundef_fresh = OK ? cm_f →
+ clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type rettyp cl_k cm_k cm_stack →
+ ∀fun_id.
+ ∀cl_rettyp, cl_retval, cl_rettrace, cm_retval.
+ ∀cl_lhs, cm_lhs, Hinvariant_on_cm_lhs.
+ (* Explain where the lhs of the post-return assign comes from *)
+ exec_lvalue cl_ge cl_env cl_m cl_lhs = OK ? 〈cl_retval, cl_rettrace〉 →
+ translate_dest alloc_type cl_lhs = OK ? (MemDest ? «cm_lhs, Hinvariant_on_cm_lhs») →
+ (* TODO: Explain that the actual variable used to store the ret val is fresh and has the
+  * right type, etc *)
+ ∀cm_ret_var.
+ ∀sInv, fInv, kInv.
+ ∀cl_args_values, cm_args_values.
+ All2 val val (λcl_val:val.λcm_val:val.value_eq Em cl_val cm_val) cl_args_values cm_args_values →
+ (* TODO: return_value_rel … INV frame_data cl_retval cm_retval →*)
+ ∀cm_stack.
+ clight_cminor_rel cl_ge cm_ge INV
+  (ClCallstate fun_id (CL_Internal cl_f)
+    cl_args_values (Kcall (Some ? 〈cl_retval,cl_rettyp〉) cl_f cl_env cl_k) cl_m)
+  (CmCallstate fun_id (Internal ? cm_f)
+    cm_args_values cm_m (Scall cm_retval cm_f stackptr cm_env sInv fInv
+                          (Kseq (St_store (typ_of_type cl_rettyp) cm_lhs
+                                          (Id (typ_of_type cl_rettyp) cm_ret_var)) cm_k)
+                           kInv cm_stack))
+*)
 definition clight_normal : Clight_state → bool ≝
 …
 #p #Hlookup %{p} @conj try @refl assumption
 qed.
+lemma find_funct_id_inversion :
+  ∀F: Type[0]. ∀ge: genv_t F. ∀ptr. ∀f. ∀id.
+  find_funct_id F ge ptr = Some ? 〈f, id〉 →
+  ∃H:(find_funct F ge ptr = Some ? f).
+     id = symbol_of_function_val' F ge ptr f H.
+#F #ge #ptr #f #id
+whd in match (find_funct_id ???);
+generalize in match (refl ??);
+generalize in ⊢
+  (∀_:(???%).
+    (??(match %
+        with
+        [ _ ⇒ λ_. ?
+        | _ ⇒ λ_.λ_. ? ] ?)?) → ?);
+#o cases o
+normalize nodelta
+[ #H #Habsurd destruct (Habsurd)
+| #f #Hfind #Heq destruct (Heq) %{Hfind}
+  cases (find_funct_inversion ???? Hfind) #ptr *
+  * * #Hptr lapply Hfind -Hfind >Hptr #Hfind
+  #Hoff #Hblock * #id * #Hblock_id #Hlookup_opt
+  normalize nodelta @refl
+] qed.
 (* We should be able to prove that ty = ty' with some more hypotheses, if needed. *)
 …
 [ #r | #n | ]
 * #cl_type * #Heq_lookup normalize nodelta
+[ 3: cases (type_eq_dec ??) normalize nodelta #H
+  [ 2: whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd) ]
+| *: ]
 whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
 whd in ⊢ ((??%?) → ?);
 …
+  ]
 ] qed.
 (* lift simulation result to eval_exprlist *)
 lemma eval_exprlist_simulation :
   ∀cl_f.
 …
 qed. (* this last lemma has to be refitted. *)
-(* This, to say the least, is not pretty. Whenever we update the memory, we have to perform
- * a kind of functional record update on the frame_data. But of course, we also need equations
- * relating the old and new frame data. *)
-(*
-lemma update_clight_cminor_data_cm :
-  ∀f, cl_ge, cm_ge, INV.
-  ∀frame_data: clight_cminor_data f cl_ge cm_ge INV.
-  ∀cl_m_v.
-  ∀new_cm_mem.
-  cl_m_v = cl_m … frame_data →
-  ∀new_inj: memory_inj (Em … frame_data) cl_m_v new_cm_mem.
-  ∃data:clight_cminor_data f cl_ge cm_ge INV.
-          alloc_type … frame_data = alloc_type … data ∧
-          cl_env … frame_data = cl_env … data ∧
-          cm_env … frame_data = cm_env … data ∧
-          stackptr … frame_data = stackptr … data ∧
-          cl_m … frame_data = cl_m … data ∧
-          new_cm_mem = (cm_m … data).
-#f #cl_ge #cm_ge #INV #frame_data #cl_m_v #new_cm_mem #H destruct (H) #Hinj
-%{(mk_clight_cminor_data ????
-       (alloc_type … frame_data)
-       (stacksize … frame_data)
-       (alloc_hyp … frame_data)
-       (cl_env … frame_data)
-       (cm_env … frame_data)
-       (cl_env_hyp … frame_data)
-       (cl_m … frame_data)
-       new_cm_mem
-       (Em … frame_data)
-       Hinj
-       (stackptr … frame_data)
-       (matching … frame_data)
-       (Em_fn_id … frame_data))}
-@conj try @conj try @conj try @conj try @conj try @refl
-qed.*)
-(* Same thing, this time update both CL and CM memory. Here we provide a proof
- * that the data in local env is not touched. *)
-(*
-lemma update_clight_cminor_data_cl_cm_global :
-  ∀f, cl_ge, cm_ge, INV.
-  ∀frame_data: clight_cminor_data f cl_ge cm_ge INV.
-  ∀new_cl_mem, new_cm_mem.
-  ∀new_inj: memory_inj (Em … frame_data) new_cl_mem new_cm_mem.
-  (∀id, b, cl_type.
-   lookup ?? (cl_env … frame_data) id = Some ? b →
-   lookup ?? (alloc_type … frame_data) id = Some ? 〈Local, cl_type〉 →
-   load_value_of_type cl_type (cl_m … frame_data) b zero_offset =
-   load_value_of_type cl_type new_cl_mem b zero_offset) →
-  ∃data:clight_cminor_data f cl_ge cm_ge INV.
-        alloc_type … frame_data = alloc_type … data ∧
-        cl_env … frame_data = cl_env … data ∧
-        cm_env … frame_data = cm_env … data ∧
-        stackptr … frame_data = stackptr … data ∧
-        new_cl_mem = (cl_m … data) ∧
-        new_cm_mem = (cm_m … data).
-#f #cl_ge #cm_ge #INV #frame_data #new_cl_mem #new_cm_mem #Hinj #Haux
-%{(mk_clight_cminor_data ????
-       (alloc_type … frame_data)
-       (stacksize … frame_data)
-       (alloc_hyp … frame_data)
-       (cl_env … frame_data)
-       (cm_env … frame_data)
-       (cl_env_hyp … frame_data)
-       new_cl_mem
-       new_cm_mem
-       (Em … frame_data)
-       Hinj
-       (stackptr … frame_data)
-       ? (* (matching … frame_data) *)
-       (Em_fn_id … frame_data))}
-[ whd #id
-  lapply (matching … frame_data id)
-  lapply (Haux id)
-  cases (lookup ??? id) normalize nodelta
-  [ #_ #H @H
-  | #b cases (lookup ??? id) normalize nodelta
-    [ #_ #H @H
-    | * #vartype #cltype normalize nodelta
-      cases vartype try // normalize nodelta #Haux
-      #H #v #Hload @H >(Haux ?? (refl ??) (refl ??)) @Hload
+    ]
+  ]
+|
-@conj try @conj try @conj try @conj try @conj try @conj try @refl
-qed.*)
 lemma store_value_of_type_success_by_value :
    ∀ty, m, m', b, o, v.
 …
 | *: %1 #id % #Habsurd destruct (Habsurd) ]
 qed.
-(* Not provable: need to relate (typeof (e=Evar id, ty)) with the type contained
-   in var_ty. Should be doable, but not now. *)
-(*
-lemma translate_dest_IdDest_typ :
-  ∀vars,e,var_id,var_ty,H.
-    translate_dest vars e = return (IdDest vars var_id var_ty H) →
-    var_ty = typeof e.
-#vars * #ed #ety #var_id #var_ty #H
-cases ed
-[ #sz #i | #id | #e1 | #e1 | #op #e1 |#op #e1 #e2 | #cast_ty #e1
-| #cond #iftrue #iffalse | #e1 #e2 | #e1 #e2 | #sizeofty | #e1 #field | #cost #e1 ]
-[ 2,3,12:
-  [ 2,3:
-    whd in ⊢ ((??%?) → ?);
-    cases (translate_addr ??) normalize nodelta
-    [ 2,3: #error whd in ⊢ ((??%%) → ?); #Habsurd destruct (Habsurd)
-    | 1,4: #Hfoo whd in ⊢ ((??%%) → ?); #Habsurd destruct (Habsurd) ]
-  | 1: #H' lapply (bind2_eq_inversion ?????? H') * #vt * #t * #Eq
-    lapply Eq inversion vt normalize nodelta
-    [ 1,2: #foo #bar #Hlookup
-      whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
-    | 3: #e whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
-| *: whd in ⊢ ((??%?) → ?); whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd)
-normalize nodelta
-[ 2:*)
 lemma mk_offset_offv_id : ∀o. mk_offset (offv o) = o.
 …
   load_value_of_type ty m b o = Some ? v.
+(* Make explicit the contents of [exec_bind_parameters ????] *)
+lemma exec_alloc_bind_params_same_length :
+  ∀e,m,m',params,vars.
+  exec_bind_parameters e m params vars = OK ? m' →
+  (params = [ ] ∧ vars = [ ]) ∨
+  ∃id,ty,tl_pa,v,tl_vars,b,mi.
+   params = 〈id,ty〉 :: tl_pa ∧
+   vars   = v :: tl_vars ∧
+   lookup ?? e id = Some ? b ∧
+   store_value_of_type ty m b zero_offset v = Some ? mi ∧
+   exec_bind_parameters e mi tl_pa tl_vars = OK ? m'.
+#e #m #m' #params cases params
+[ #vars whd in ⊢ ((??%?) → ?); cases vars normalize nodelta
+  [ #Heq destruct (Heq) %1 @conj try @refl
+  | #hd_pa #tl_pa #Habsurd destruct (Habsurd) ]
+| * #id #ty #tl_pa #vars
+  whd in ⊢ ((??%?) → ?);
+  cases vars normalize nodelta
+  [ #Habsurd destruct (Habsurd)
+  | #hd_val #tl_val #H
+    cases (bind_inversion ????? H) -H
+    #blo * #HA #H
+    cases (bind_inversion ????? H) -H
+    #m'' * #HB #Hexec_bind %2
+    %{id} %{ty} %{tl_pa} %{hd_val} %{tl_val} %{blo} %{m''}
+    @conj try @conj try @conj try @conj try @refl
+    try @(opt_to_res_inversion ???? HA)
+    try @(opt_to_res_inversion ???? HB)
+    @Hexec_bind
+  ]
+] qed.
+(* Axiom-fest, with all the lemmas we need but won't have time to prove. Most of them are not too hard. *)
+(* The way we have of stating this is certainly not the most synthetic. The property we really need is that
+ * stmt_univ' is fresher than stmt_univ, which sould be trivially provable by a simple induction. *)
+axiom env_below_freshgen_preserved_by_translation :
+    ∀cl_env, alloc_type, stmt_univ, lbl_univ, lbls, flag, rettyp, s, stmt_univ', lbl_univ', cm_s, H.
+    env_below_freshgen cl_env alloc_type stmt_univ →
+    translate_statement alloc_type stmt_univ lbl_univ lbls flag rettyp s = return «〈stmt_univ', lbl_univ', cm_s〉, H» →
+    env_below_freshgen cl_env alloc_type stmt_univ'.
+axiom tmp_vars_well_allocated_preserved_by_inclusion :
+    ∀cm_env, cm_m, cl_m, Em, tmpenv, tmpenv'.
+    lset_inclusion ? tmpenv tmpenv' →
+    tmp_vars_well_allocated tmpenv' cm_env cm_m cl_m Em →
+    tmp_vars_well_allocated tmpenv cm_env cm_m cl_m Em.
+axiom translation_entails_ident_inclusion :
+    ∀alloc_type, stmt_univ, lbl_univ, lbls, flag, rettyp, stmt_univ'.
+    ∀cl_s, cm_s, labgen, Htrans_inv.
+    translate_statement alloc_type stmt_univ lbl_univ lbls flag rettyp cl_s = return «〈stmt_univ',labgen,cm_s〉,Htrans_inv» →
+    lset_inclusion ? (tmp_env … stmt_univ) (tmp_env … stmt_univ').
+(* Same remarks as above apply here too. *)
+(*
+lemma tmp_vars_well_allocated_preserved_by_translation :
+    ∀cm_env, alloc_type, stmt_univ, lbl_univ, lbls, flag, rettyp, stmt_univ'.
+    ∀Em, cm_m, cl_m, cl_s, cm_s, labgen, Htrans_inv.
+    translate_statement alloc_type stmt_univ lbl_univ lbls flag rettyp cl_s = return «〈stmt_univ',labgen,cm_s〉,Htrans_inv» →
+    tmp_vars_well_allocated (tmp_env alloc_type stmt_univ') cm_env cm_m cl_m Em →
+    tmp_vars_well_allocated (tmp_env alloc_type stmt_univ) cm_env cm_m cl_m Em.
+#cm_env #alloc_type #stmt_univ #lbl_univ #lbls #flag #rettyp #stmt_univ' #Em #cm_m #cl_m #cl_s #cm_s
+#labgen #Htrans_inv #Htranslate_statement #H #id #Hpresent #ty #Hexists
+@H lapply (translation_entails_ident_inclusion … Htranslate_statement)
+#H
+@H23*)
+axiom tmp_vars_well_allocated_conserved_by_frame_free :
+  ∀alloc_type, tmpenv, cl_env, cm_env, cm_m, cl_m, stackptr.
+  ∀Em, cl_ge, cm_ge, INV.
+  ∀Hmatching:memory_matching Em cl_ge cm_ge cl_m cm_m cl_env cm_env INV stackptr alloc_type.
+  tmp_vars_well_allocated tmpenv cm_env cm_m cl_m Em ->
+  tmp_vars_well_allocated tmpenv cm_env (free cm_m stackptr) (free_list cl_m (blocks_of_env cl_env)) Em.
+axiom generated_id_not_in_env :
+    ∀id, blo, tmp, ty.
+    ∀env: cl_env.
+    ∀alloc_type.
+    ∀freshgen, freshgen': tmpgen alloc_type.
+    env_below_freshgen env alloc_type freshgen →
+    lookup ?? env id = Some ? blo →
+    alloc_tmp alloc_type ty freshgen = 〈tmp, freshgen'〉 →
+    tmp ≠ id.
+(* This should just be lifting a lemma from positive maps to identifier maps.
+ * Sadly, the way things are designed requires a boring induction. *)
+axiom update_lookup_opt_other :
+  ∀b,a,t,H.
+  ∀b'. b ≠ b' →
+  lookup SymbolTag val t  b' = lookup SymbolTag val (update_present SymbolTag val t b H a) b'.
+(* NOTE: this axiom is way more general than what we need. In practice, cm_m' is cm_m after a store. *)
+axiom clight_cminor_cont_rel_parametric_in_mem :
+  ∀cl_ge, cm_ge, INV, cl_f, cm_f, cl_env, cm_env, cm_m, cm_m', alloc_type, tmpenv, (*stmt_univ, stmt_univ', *) rettyp, cl_k, cm_k, cm_st.
+  clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env cm_m alloc_type tmpenv (*stmt_univ stmt_univ'*) rettyp cl_k cm_k cm_st →
+  clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env cm_m' alloc_type tmpenv (*stmt_univ stmt_univ'*) rettyp cl_k cm_k cm_st.
+(* Same remark as above. *)
+axiom well_allocated_preserved_by_parallel_stores :
+  ∀tmpenv, cm_env, cm_m, cm_m', cl_m, cl_m', Em.
+(* TODO: proper hypotheses (the following, commented out do not exactly fit)
+  (storen cm_m (mk_pointer cl_blo (mk_offset (offv zero_offset))) (fe_to_be_values (typ_of_type (typeof rhs)) cm_rhs_val)
+   =Some mem cm_mem_after_store_lhs)
+  storev (typ_of_type ty) cl_m (Vptr (mk_pointer cl_blo zero_offset)) cl_rhs_val = Some ? cl_m') *)
+  tmp_vars_well_allocated tmpenv cm_env cm_m  cl_m  Em →
+  tmp_vars_well_allocated tmpenv cm_env cm_m' cl_m' Em.
+(* Same remark as above. Moreover, this should be provable from memory injections. *)
+axiom memory_matching_preserved_by_parallel_stores :
+  ∀Em, cl_ge, cm_ge, cl_m, cl_m', cm_m, cm_m', cl_env, cm_env, INV, stackptr, alloc_type.
+  memory_matching Em cl_ge cm_ge cl_m  cm_m  cl_env cm_env INV stackptr alloc_type →
+  memory_matching Em cl_ge cm_ge cl_m' cm_m' cl_env cm_env INV stackptr alloc_type.
+axiom clight_cminor_cont_rel_parametric_in_cm_env :
+∀cl_ge, cm_ge, INV, cl_f, cm_f, cl_env, cm_env, cm_m, alloc_type, tmpenv, (*stmt_univ, stmt_univ',*) rettyp, cl_k, cm_k, cm_st, var_id, v.
+∀Hpresent:present SymbolTag val cm_env var_id.
+clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env cm_m alloc_type tmpenv (*stmt_univ stmt_univ'*) rettyp cl_k cm_k cm_st ->
+clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env
+  (update_present SymbolTag val cm_env var_id Hpresent v) cm_m
+  alloc_type tmpenv (*stmt_univ stmt_univ'*) rettyp cl_k cm_k cm_st.
+axiom tmp_vars_well_allocated_preserved_by_local_store :
+  ∀Em, cl_value, cm_value, lhs_ty, cl_m, cl_m', cm_m, cl_blo, tmpenv, cm_env, var_id.
+  ∀Hpresent:present SymbolTag val cm_env var_id.
+  value_eq Em cl_value cm_value →
+  store_value_of_type' lhs_ty cl_m 〈cl_blo, zero_offset〉 cl_value = Some ? cl_m' →
+  tmp_vars_well_allocated tmpenv cm_env cm_m cl_m Em →
+  tmp_vars_well_allocated tmpenv
+  (update_present ?? cm_env var_id Hpresent cm_value) cm_m
+   cl_m' Em.
+axiom memory_inj_preserved_by_local_store :
+∀Em, cl_ge, cm_ge, cl_m, cl_m', cm_m, cl_env, cm_env, INV, stackptr, alloc_type.
+ memory_matching Em cl_ge cm_ge cl_m cm_m cl_env cm_env INV stackptr alloc_type ->
+ memory_inj Em cl_m cm_m ->
+ memory_inj Em cl_m' cm_m.
+axiom memory_matching_preserved_by_local_store :
+  ∀Em, cl_ge, cm_ge, cl_m, cl_m', cm_m, cl_env, cm_env, INV, stackptr, alloc_type, cl_value, cm_value.
+  ∀cl_blo, var_id, lhs_ty.
+  ∀Hpresent:present SymbolTag val cm_env var_id.
+   value_eq Em cl_value cm_value →
+   store_value_of_type' lhs_ty cl_m 〈cl_blo, zero_offset〉 cl_value = Some ? cl_m' →
+   memory_matching Em cl_ge cm_ge cl_m cm_m cl_env cm_env INV stackptr alloc_type →
+   memory_matching Em cl_ge cm_ge cl_m' cm_m cl_env
+    (update_present SymbolTag val cm_env var_id Hpresent cm_value) INV stackptr alloc_type.
+lemma translate_dest_conservation :
+  ∀vars, e1.
+  ∀id, t, H.
+  translate_dest vars e1 = OK ? (IdDest vars id t H) →
+  typeof e1 = t.
+#vars #e1 #id #t #H #Htranslate lapply (translate_dest_id_inversion … Htranslate)
+#Heq >Heq in Htranslate;
+whd in ⊢ ((??%?) → ?);
+generalize in match (refl ??);
+generalize in ⊢ ((???%) → (??(match % with [ _ ⇒ ? | _ ⇒ ? ] ?)?) → ?); *
+normalize nodelta
+[ 2: #er #_ #Habsurd destruct (Habsurd) ]
+* * normalize nodelta
+[ #a #b #c #Habsurd
+| #n #t #H #Habsurd
+| #ty #H ]
+[ 1,2: destruct (Habsurd) ]
+cases (type_eq_dec ??) normalize nodelta
+#Hty #Heq destruct (Heq) >Hty @refl
+qed.
+lemma alloc_tmp_monotonic :
+  ∀alloc_type, ty, univ, univ', v.
+   alloc_tmp alloc_type ty univ = 〈v, univ'〉 →
+   lset_inclusion ? (tmp_env ? univ) (tmp_env ? univ').
+#alloc_type #ty #univ #univ' #v cases univ
+#u #env #Hfresh #Hyp #Halloc
+cases (breakup_dependent_match_on_pairs ?????? Halloc) -Halloc
+#v * #u' * #Heq * #Heq' normalize nodelta #Heq''
+destruct (Heq'')
+@cons_preserves_inclusion @reflexive_lset_inclusion
+qed.
+(*
+lemma lset_inclusion_Exists :
+  ∀A. ∀l1, l2: lset A.
+  lset_inclusion ? l1 l2 →
+  ∀P. Exists ? P l1 → Exists ? P l2.
+#A #l1 elim l1
+[ #l2 #Hincl #P @False_ind
+| #hd #tl #Hind #l2 * #Hmem #Hincl2 #P *
+  [ 2: #Htl @Hind assumption ]
+  lapply P -P
+  lapply Hincl2 -Hincl2
+  lapply Hmem -Hmem elim l2
+  [ @False_ind ]
+  #hd2 #tl2 #Hind2 *
+  [ #Heq destruct (Heq)
+    #Hincl2 #P #H %1 @H
+  | #Hmem #Hincl2 #P #H %2
+    elim tl2 in Hmem;
+    [ @False_ind
+    | #hd2' #tl2' #Hind3 *
+      [ #Heq destruct (Heq) %1 assumption
+      | #Hmem' %2 @Hind3 @Hmem' ]
+    ]
+  ]
+] qed.  *)
 (* --------------------------------------------------------------------------- *)
 (* Main simulation results                                                     *)
 (* -------------------------------------------------------------------;-------- *)
+(* --------------------------------------------------------------------------- *)
 (* Conjectured simulation results
 …
    subtrace corresponding to a measurable Clight subtrace.
  *)
+(*
+lemma clight_cminor_call_return :
+  ∀g1, g2.
+  ∀INV:clight_cminor_inv g1 g2.
+  ∀s1,s1'.
+  clight_cminor_rel g1 g2 INV s1 s1' →
+  match Clight_classify s1 with
+  [ cl_call ⇒ true
+  | cl_return ⇒ true
+  | _ ⇒ false ] →
+  ∀s2,tr. step … (pcs_exec cl_pre) g1 s1 = Value … 〈tr, s2〉 →
+  ∃m. after_n_steps m ?? (pcs_exec cm_pre) g2 s1' (λs.cminor_normal s) (λtr',s2'.
+    tr = tr' ∧
+    clight_cminor_rel g1 g2 INV s2 s2' ∧
+      (m = 0 → lex_lt (measure_Clight s2) (measure_Clight s1))
+  ).
+#g1 #g2 #INV #s1 #s1' #Hstate_rel #Hclight_class
+inversion Hstate_rel
+[ 1: (* normal *)
+  #cl_ge #cm_ge #INV' #cl_s
+  #cm_s #cl_k #cm_k #cm_st #cl_f #cm_f #rettyp
+  #alloc_type #cl_env #cl_m #cm_env #cm_m #stackptr #stacksize
+  (* introduce everything *)
+  #fInv #sInv #kInv #Htarget_type #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function
+  #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls
+  #flag  #Htrans_inv #Htrans_stmt #Hincl #HA #HB #HC
+  #HE #HF #HG #HI #HJ #HK
+  @(jmeq_absorb ?????) #H1 @(jmeq_absorb ?????) #H2
+  destruct (H1 H2)
+  @(jmeq_absorb ?????) #H3 @(jmeq_absorb ?????) #H4 @(jmeq_absorb ?????) #H5
+  destruct (H3 H4 H5)
+  @False_ind @Hclight_class
+| 5:
+  #cl_ge #cm_ge #INV' #cl_s
+  #cm_s #cl_k #cm_k #cm_st #cl_f #cm_f #rettyp
+  #alloc_type #cl_k #cm_k #sz #sg #cl_ty #cl_cond_desc #cl_body #entry_lab #exit_lab
+  #cm_cond #cm_body #cm_stack #rettyp' #kInv
+  (* introduce everything *)
+  #fInv #sInv #kInv #Htarget_type #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function
+  #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls
+  #lbl1 #lbl2 #Em #Htmp_vars #Hcharac #Hexec #Hinj #Hmatching #Hem #Hframe #Hcond_tr
+  #Htransl #Hex1 #Hex2 #Htransinv #Hmklabs #Htranstmt #Hincl
+  #Hlabdecl #Hinv1 #Hinv2 #Hfindlab
+  @(jmeq_absorb ?????) #H1 @(jmeq_absorb ?????) #H2
+  destruct (H1 H2)
+  @(jmeq_absorb ?????) #H3 @(jmeq_absorb ?????) #H4 @(jmeq_absorb ?????) #H5
+  destruct (H3 H4 H5)
+  @False_ind @Hclight_class
+| 2:
+  #cl_ge #cm_ge #INV' #cl_f #cm_f #cl_k #cm_k #alloc_type
+  #cl_env #cl_m #cm_env #cm_m #cm_st #stackptr #stacksize
+  #stmt_univ #Em #Htmp_vars_well_allocated #Halloc_hyp #Hcl_env_hyp
+  #Hinjection #Hmatching #HEm_fn_id #Hframe_spec #Hcont_rel
+  @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
+  destruct (HA HB)
+  @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE #_
+  destruct (HC HD HE)
+  inversion Hcont_rel
+  [ #kcl_ge #kcm_ge #kINV #kcl_f #kcm_f #ktarget_type #kcl_env #kcm_env #kalloc_type #kstack #Hkstack
+    @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
+    destruct (HA HB)
+    @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
+    destruct (HC HD HE)
+    @(jmeq_absorb ?????) #HF @(jmeq_absorb ?????) #HG @(jmeq_absorb ?????) #HH
+    @(jmeq_absorb ?????) #HI @(jmeq_absorb ?????) #HJ @(jmeq_absorb ?????) #HK @(jmeq_absorb ?????) #HL
+    destruct (HF HG HH HI HJ HK HL) #_
+    #s2 #tr
+    whd in ⊢ ((??%?) → ?); #Habsurd destruct (Habsurd)
+  | (* Kseq *)
+    #kcl_ge #kcm_ge #kINV #kcl_f #kcm_f #ktarget_type #kstack #kalloc_type #kcl_s #kcm_s
+    #kcl_env #kcm_env #kcl_k' #kcm_k' #kstmt_univ #kstmt_univ' #klbl_univ #klbl_univ' #klbls #kflag
+    * * * * #kHstmt_inv #kHlabels_translated #kHtmps_preserved
+    #kHreturn_ok #kHlabel_wf #kHeq_translate #kHlabel_inclusion #kHcont_rel #_
+    @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
+    destruct (HA HB)
+    @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
+    destruct (HC HD HE)
+    @(jmeq_absorb ?????) #HF @(jmeq_absorb ?????) #HG @(jmeq_absorb ?????) #HH @(jmeq_absorb ?????) #HI
+    @(jmeq_absorb ?????) #HJ @(jmeq_absorb ?????) #HK @(jmeq_absorb ?????) #HL
+    destruct (HF HG HH HI HJ HK HL) #_
+    #s2 #tr
+    whd in ⊢ ((??%?) → ?); #Habsurd destruct (Habsurd)
+  | (* *)
+    #kcl_ge #kcm_ge #kINV #kcl_f #kcm_f #ktarget_type #kstack #kalloc_type #kcl_env #kcm_env
+    #kcl_k' #kcm_k' #ksz #ksg #kcl_ty #kcl_cond_desc #kcl_body #kHeq_ty #kcm_cond #kcm_body
+    #kentry #kexit #kstmt_univ #kstmt_univ' #klbl_univ #klbl_univ' #klbl_univ''
+    #klbls #kHtranslate_inv #kHexpr_vars #kHtranslate_expr #kfInv #kHlabel_declared
+    #kHinv #kHmklabels #kHeq_translate #kHlabel_inclusion #kHfind_label
+    (*
+    * * * * #kHentry_declared * * * *
+    * * * #kHcond_vars_declared #Hnoise #Hnoise' #Hnoise''
+    #kHcont_inv #kHmklabels #kHeq_translate
+    #kHfind_label *) #kHcont_rel #_
+    @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
+    destruct (HA HB)
+    @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
+    destruct (HC HD HE)
+    @(jmeq_absorb ?????) #HF @(jmeq_absorb ?????) #HG @(jmeq_absorb ?????) #HH
+    @(jmeq_absorb ?????) #HI @(jmeq_absorb ?????) #HJ @(jmeq_absorb ?????) #HK
+    @(jmeq_absorb ?????) #HL
+    destruct (HF HG HH HI HJ HK HL) #_
+    #s2 #tr
+    whd in ⊢ ((??%?) → ?); #Habsurd destruct (Habsurd)
+  ]
+| 3:
+  #cl_ge #cm_ge #INV' #alloc_type
+  #cl_env #cl_m #cm_env #cm_m #cm_st #stackptr #func_univ
+  #cl_f #cm_f #Hglobals_fresh #Hfundef_fresh
+  #rettyp #cl_k #cm_k #fblock *
+  #Hrettyp #Hfind_funct_cl #Hfind_func_cm #Htranslate_function #Hcont_rel
+  #fun_id #cl_retval #cm_retval #sInv #fInv #kInv #cl_args #cm_args
+  @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
+  destruct (HA HB)
+  @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
+  destruct (HC HD HE) #_
+  #s2 #tr whd in ⊢ ((??%?) → ?);
+  @(match (exec_alloc_variables empty_env cl_m (fn_params cl_f@fn_vars cl_f))
+    return λx. (x = (exec_alloc_variables empty_env cl_m (fn_params cl_f@fn_vars cl_f))) → ?
+    with
+    [ mk_Prod new_cl_env cl_m_alloc ⇒ ?
+    ] (refl ? (exec_alloc_variables empty_env cl_m (fn_params cl_f@fn_vars cl_f))))
+  #Hexec_alloc_variables normalize nodelta
+  #Hstep
+  cases (bindIO_inversion ??????? Hstep) -Hstep
+  #cl_m_init * #Hexec_bind_parameters
+  whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
+  %{1} whd whd in ⊢ (??%?);
+  (* Alloc big chunk of data of size (f_stacksize cm_f) *)
+  @(match (alloc cm_m 0 (f_stacksize cm_f))
+    return λx. (alloc cm_m 0 (f_stacksize cm_f) = x) → ?
+    with
+    [ mk_Prod new_cm_mem new_cm_stackptr ⇒ ?
+    ] (refl ? (alloc cm_m 0 (f_stacksize cm_f))))
+  #H_cm_alloc normalize nodelta
+  (* Initialise CM /parameters/ *)
+  %{(S (times 3 (|fn_vars|)))} -Hclight_class
+  lapply (exec_alloc_bind_params_same_length … Hexec_bind_parameters)
+  elim cl_args in Hstate_rel Hexec_alloc;
+  [ #Hstate_rel whd in ⊢ ((??%%) → ?);
+    whd in match (exec_bind_parameters ????);
+  exec_alloc_variables empty_env cl_m (fn_params cl_f@fn_vars cl_f) = 〈cl_env, cl_m'〉
+  lapply (let_prod_as_inversion ?????? Hstep)
+    @(jmeq_absorb ?????) #HF @(jmeq_absorb ?????) #HG @(jmeq_absorb ?????) #HH
+    @(jmeq_absorb ?????) #HI @(jmeq_absorb ?????) #HJ @(jmeq_absorb ?????) #HK
+    @(jmeq_absorb ?????) #HL
+    destruct (HF HG HH HI HJ HK HL) #_
+    #s2 #tr
+  #Em #Htmp_vars_well_allocated #Halloc_hyp #Hcl_env_hyp
+  #Hinjection #Hmatching #HEm_fn_id #Hframe_spec #Hcont_rel
+] qed.  *)
 lemma clight_cminor_normal :
 …
      | #structname #fieldspec | #unionname #fieldspec | #id ]
      #Hlabels_translated #Htmps_preserved
      #Hreturn_ok #Hlabel_wf #Htranslate #Hlabel_inclusion
+     #Hreturn_ok #Hlabel_wf #Htranslate #Hlabel_inclusion #tmpenv #Htmpenv
      #Hcont_rel
+     #Em #Htmp_vars_well_allocated #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id
+     #Hframe_spec
+     #Em #Htmp_vars_well_allocated
+     #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id
+     #Hframe_spec #Henv_below
      @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
      destruct (HA HB)
      @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE #_
      destruct (HC HD HE)
      lapply Htranslate -Htranslate
+     destruct (HC HD HE)
+     lapply Htranslate -Htranslate
      [ 1: generalize in match (conj ????); #Hugly_inv
      | 2: generalize in match (conj ????); #Hugly_inv
 …
             @(CMR_normal … Htrans_body) try assumption
             @(ClCm_cont_while … (sym_eq … Hmk_label_eq) … Htrans_body) try assumption
+            [ 1,6,11,16:
+              @refl
+            | 2,3,7,8,12,13,17,18:
+              >CMcast_identity try assumption
+            | 4,9,14,19:
+            try @refl
+            [ 1,4,7,10: @eq_to_jmeq assumption
+            | 2,5,8,11:
                  @conj try assumption @conj @conj try assumption @conj @conj try assumption
                  try @conj try assumption try @conj try assumption
                  try @conj try assumption try @conj try assumption
             | 5,10,15,20: (* find_label_always *)
                  (* TODO /!\ we need to find a clever way to prove this. *)
+            | *: (* find_label_always *)
+                 (* TODO /!\ implement necessary invariant on label lookup *)
                  @cthulhu
+            ]
 …
        @conj try @conj try @conj
        [ 1,4,7,10: normalize >append_nil >append_nil @refl
        | 2,5,8,11:
           @(CMR_normal … Htranslate_function … DoNotConvert … Hcont_rel) try assumption
           [ 2,4,6,8: @refl | *: ]
+       | 2,5,8,11:
+          @(CMR_normal … Htranslate_function … DoNotConvert) try assumption
+          try @refl try @(env_below_freshgen_preserved_by_translation … Henv_below Htrans_body)
        | *: #Habsurd destruct (Habsurd) ]
+   ]
 …
      (* generalize away ugly proof *)
      generalize in ⊢ (∀_:(???(??(????%))).?); #Hugly
      #Htranslate #Hlabel_inclusion #Hcont_rel #Em
+     #Htranslate #Hlabel_inclusion #tmpenv #Htmpenv #Hcont_rel #Em
      #Htmp_vars_well_allocated
      #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id
      #Hframe_spec
+     #Hframe_spec #Henv_below
      @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
      destruct (HA HB)
 …
        #Hdest cases (bind_inversion ????? Hdest) -Hdest #dest *
        inversion dest normalize nodelta
        [ (* register dest *) #var_id #var_ty #His_local @(jmeq_absorb ?????) #Hdest
+       [ (* register dest *) #var_id #var_ty #His_local @(jmeq_absorb ?????) #Hdest
          #Htranslate_dest whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
          (* make explicit the nature of lhs, allowing to prove that no trace is emitted *)
 …
           generalize in ⊢ ((??(??(????%))?) → ?); #Hugly2
           whd in ⊢ ((???%) → ?); #Heq destruct (Heq) ]
+     (* Now, execute the Clight call *)
      #s2 #tr #Htranslate
      cases (bindIO_inversion ??????? Htranslate) -Htranslate *
      #func_ptr_val #func_trace * #Hexec_func_ptr normalize nodelta
+     #CL_callee_val #CL_callee_trace * #Hexec_CL_callee normalize nodelta
      whd in ⊢ ((???%) → ?); #Htranslate
      cases (bindIO_inversion ??????? Htranslate) -Htranslate *
      #args_values #args_trace * #Hexec_arglist #Htranslate
+     #CL_args #CL_args_trace * #Hexec_CL_args #Htranslate
      cases (bindIO_inversion ??????? Htranslate) -Htranslate
+     * #cl_fundef #cl_fun_id * #Hfind_funct
+     * #CL_callee_fundef #CL_callee_id * #Hfind_funct
+     (* We've got the CL fundef. Extract a function pointer out of it. *)
      lapply (opt_to_io_Value ?????? Hfind_funct) -Hfind_funct #Hfind_funct
      cases (find_funct_inversion ???? Hfind_funct)
+     #func_ptr * * * #Hfunc_ptr_eq destruct (Hfunc_ptr_eq)
+     #Hpoff_eq_zero #Hregion_is_code
+     * #block_id * #Hblock_id_neg #Hlookup
+     #CL_callee_ptr * * * #HCL_callee_eq destruct (HCL_callee_eq)
+     (* Done. Now stash the resulting properties of this pointer in the context. *)
+     #HCL_callee_ptr_offset_eq_zero #HCL_callee_ptr_region_eq_Code
+     (* Some more properties, that should stay hidden. XXX we discard them, this should not hinder the proof *)
+     * #block_id * #Hblock_id_neg #Hlookup -Hlookup -Hblock_id_neg -block_id
+     (* Now, break up a safety check for the type of the function and finally, execute the
+      * CL lvalue supposed to store the result of the function call. This will yield a pointer
+      * that will be stored in the Callstate, until the function call returns and we store te
+      * result inside it. Of course, this does not apply to the case wich returns void. *)
      #Htranslate
      cases (bindIO_inversion ??????? Htranslate) -Htranslate #Htype_of_fundef *
      #Hassert_type_eq
+     [ 1,2: #Htranslate
+            cases (bindIO_inversion ??????? Htranslate) -Htranslate * *
+            #lblock #loffset #ltrace *
+            whd in ⊢ ((???%) → (???%) → ?);
+            [ >Hlhs_eq #Hexec_lvalue
+              cut (ltrace = [])
+              [ lapply (res_to_io ????? Hexec_lvalue)
+     [ 1,2: (* Cases where we return something. *)
+            #Htranslate
+            cases (bindIO_inversion ??????? Htranslate) -Htranslate * *
+            #CL_lvalue_block #CL_lvalue_offset #CL_lvalue_trace *
+            whd in ⊢ ((???%) → (??%%) → ?);
+            [ >Hlhs_eq #HCL_exec_lvalue
+              (* The trace is empty since we execute a variable *)
+              cut (CL_lvalue_trace = [])
+              [ lapply (res_to_io ????? HCL_exec_lvalue)
                 #H' whd in H':(??%?); cases (lookup ????) in H'; normalize nodelta
                 [ 2: #b #Heq destruct (Heq) @refl
 …
                   whd in H28:(???%); destruct (H28) @refl ]
               ] #H destruct (H)
             | #Hexec_lvalue ]
+            | #HCL_exec_lvalue ]
      | 3: ]
      whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
+     [ 1: %{1} whd whd in ⊢ (??%?); normalize nodelta
+     | 2: (* Execute Cminor part: evaluate lhs, evaluate assign *)
+     (* We have reached the final Clight state. Now execute the Cminor transalted code. *)
+     [ 1: (* Return to a variable *)
+          %{1} whd whd in ⊢ (??%?); normalize nodelta
+     | 2: (* Return to memory location. Need to create a tmp CM local variable to store the
+           * lvalue ptr (otherwise trace does not match CL). *)
           %{5} whd whd in ⊢ (??%?); normalize nodelta
           whd in match (eval_expr ???????);
           whd in match (m_bind ?????);
+          (* Evalue Cminor lvalue. Need to feed some invariants to the simulation lemma, that
+           * we bake here and now. *)
           cut (expr_vars ASTptr cm_expr
                   (λid:ident.λty:typ.present SymbolTag val cm_env id))
           [ cases sInv * * * * * * * #_ #H #_ #_ #_ @H ] #Hexpr_vars_cut
+          lapply (translate_dest_MemDest_simulation … Htranslate_dest Hexec_lvalue)
+          (* Apply simulation lemma for lvalues *)
+          lapply (translate_dest_MemDest_simulation … Htranslate_dest HCL_exec_lvalue)
           try assumption try @refl
           * #cm_val_tmp * #Heval_expr_tmp >Heval_expr_tmp #Hvalue_eq
+          * #CM_lvalue * #HCM_eval_lvalue >HCM_eval_lvalue #Hvalue_eq_lvalues
           normalize nodelta generalize in match (proj1 ???); #Htmp_var_present
+          cases (value_eq_ptr_inversion … Hvalue_eq) #cm_ptr * #Hcm_val_tmp #Hcm_ptr_translation
+          >Hcm_val_tmp
+          lapply (Htmp_vars_well_allocated … tmp_var Htmp_var_present (Tpointer (typeof lhs)) ? (Vptr cm_ptr) ?)
+          [ 2: @(alloc_tmp_in_genlist … (sym_eq ??? Heq_alloc_tmp) (sym_eq ??? Heq_alloc_tmp'))
+          | 1: normalize cases cm_ptr #b #o %3 ]
+          * #cm_mem_after_store * #Hstorev #Hnew_inj >Hstorev
+          (* Make explicit the fact that the CM lvalue is a pointer *)
+          cases (value_eq_ptr_inversion … Hvalue_eq_lvalues) #CM_lvalue_ptr * #HCM_value_ptr_eq #HCM_lvalue_ptr_trans
+          >HCM_value_ptr_eq
+          lapply (Htmp_vars_well_allocated … tmp_var Htmp_var_present (Tpointer (typeof lhs)) ? (Vptr CM_lvalue_ptr) ?)
+          [ 1: normalize cases CM_lvalue_ptr #b #o %3
+          | 2: lapply (alloc_tmp_in_genlist … (sym_eq ??? Heq_alloc_tmp) (sym_eq ??? Heq_alloc_tmp'))
+               #Hexists' @(lset_inclusion_Exists … Hexists' Htmpenv)
+          ]
+          * #CM_mem_after_store * #Hstorev #Hnew_inj >Hstorev
           whd in match (m_bind ?????); normalize nodelta
           whd whd in ⊢ (??%?); normalize nodelta
-(*          cases (update_clight_cminor_data_cm … frame_ … Hnew_inj)
-          try assumption #frame_data'
-          * * * * * #Halloctype_eq_frame_data #Hcl_env_eq_frame_data #Hcm_env_eq_frame_data
-          #Hstackptr_eq_frame_data #Hcl_m_eq_frame_data #Hcm_m_eq_frame_data *)
      | 3: %{1} whd whd in ⊢ (??%?); normalize nodelta
+     ]
     (* execute Cminor part *)
+    (* cleanup ugliness *)
     [ 1: generalize in match (proj2 (present ????) (expr_vars ???) (proj1 ???));
     | 2: generalize in match (proj2 (present ????) (expr_vars ???) (proj1 ???));
 …
                 @Hexpr_vars_present_ef' ]
        #Hexpr_vars_present_ef
        lapply (Hsim_expr … Htranslate_ef … Hexpr_vars_present_ef … Hexec_func_ptr)
+       lapply (Hsim_expr … Htranslate_ef … Hexpr_vars_present_ef … Hexec_CL_callee)
        -Hsim_expr * #cm_func_ptr_val * #Heval_func #Hvalue_eq_func
        cut (eval_expr cm_ge ASTptr ef' cm_env Hexpr_vars_present_ef'
              stackptr cm_m = OK (trace×val) 〈func_trace,cm_func_ptr_val〉)
+             stackptr cm_m = OK (trace×val) 〈CL_callee_trace,cm_func_ptr_val〉)
        [ 1,3:
          lapply Heq_ef_ef' lapply Heval_func lapply Hexpr_vars_ef lapply Hexpr_vars_local_ef'
 …
        -Heval_func #Heval_func >Heval_func
     | 2: (* treat case 2 as special, since the type differs slightly *)
+       cases (eval_expr_sim … INV' … Halloc_hyp ? cm_env Hcl_env_hyp … Hnew_inj stackptr Hmatching)
+       letin cm_env' ≝ (update_present SymbolTag val cm_env tmp_var Htmp_var_present (Vptr CM_lvalue_ptr))
+       cut (memory_matching Em cl_ge cm_ge cl_m cm_m cl_env cm_env' INV' stackptr alloc_type)
+     (*  cut (memory_matching Em cl_ge cm_ge cl_m CM_mem_after_store cl_env cm_env' INV' stackptr alloc_type) *)
+       [ (* Proving preservation of the memory matching under store in "new" cminor memory zone.
+            Use the property that the ident [tmp_var] is not in the clight env. *)
+         #id lapply (Hmatching id)
+         @(match (lookup ??? id)
+           return λx. (lookup ??? id = x) → ?
+           with
+           [ None ⇒ λHeq_lookup. ?
+           | Some blo ⇒ λHeq_lookup. ?
+           ] (refl ? (lookup ??? id)))
+         [ 1: #H @H ] normalize nodelta
+         cases (lookup ??? id) normalize nodelta
+         [ 1: #H @H ] * #var_ty #cl_ty cases var_ty normalize nodelta
+         [ #r #H @H
+         | #n #H @H
+         | #H #v #Hload_value_of_type lapply (H ? Hload_value_of_type)
+           * #v' * #Hlookup_cm #Hvalue_eq %{v'} @conj try @Hvalue_eq
+           lapply (alloc_tmp_env_invariant ?????? (sym_eq ??? Heq_alloc_tmp) Henv_below) #Henv_below'
+           lapply (generated_id_not_in_env ???????? Henv_below' … Heq_lookup (sym_eq ??? Heq_alloc_tmp'))
+           #Hneq <(update_lookup_opt_other … (Vptr CM_lvalue_ptr) … cm_env … Htmp_var_present … Hneq)
+           assumption ] ] #Hmatching'
+       cases (eval_expr_sim … INV' … Halloc_hyp ? cm_env' Hcl_env_hyp … Hinjection stackptr Hmatching')
        #Hsim_expr #_
        generalize in match (proj2 ???); #Hall_present
 …
        generalize in match (proj2 ???); #Hstore_inv
        generalize in match (conj ????); #Hstmt_inv
        cut (eval_expr cm_ge ? ef' cm_env ? stackptr cm_m =
             (eval_expr cm_ge ASTptr ef' cm_env ? stackptr cm_m)) try assumption try @refl
        #Heval_expr_rewrite >Heval_expr_rewrite -Heval_expr_rewrite
        lapply (Hsim_expr … Htranslate_ef … (Vptr func_ptr) func_trace ??)
+(*       cut (eval_expr cm_ge ? ef' cm_env' ? stackptr cm_m =
+            (eval_expr cm_ge ASTptr ef' cm_env' ? stackptr cm_m)) try assumption try @refl
+       #Heval_expr_rewrite >Heval_expr_rewrite -Heval_expr_rewrite *)
+       lapply (Hsim_expr … Htranslate_ef … (Vptr CL_callee_ptr) CL_callee_trace ??)
        try assumption
        [ lapply Hexpr_vars_present_ef' lapply Heq_ef_ef' lapply Hexpr_vars_ef lapply Hexpr_vars_local_ef'
          lapply ef >Htyp_equality_ef #ef #HA #HB @(jmeq_absorb ?????) #Heq destruct (Heq) #x @x ]
        * #cm_func_ptr_val * #Heval_func_cm #Hvalue_eq_func
+       * #CM_callee_ptr * #Heval_func_cm #Hvalue_eq_func
        (* And some more shuffling types around to match the goal *)
        cut (eval_expr cm_ge ? ef' cm_env Hexpr_vars_present_ef' stackptr cm_mem_after_store = OK ? 〈func_trace,cm_func_ptr_val〉)
+       cut (eval_expr cm_ge ? ef' cm_env' Hexpr_vars_present_ef' stackptr cm_m = OK ? 〈CL_callee_trace,CM_callee_ptr〉)
        [ lapply Heval_func_cm -Heval_func_cm
          generalize in ⊢ ((??(?????%??)?) → ?);
 …
     #Htranslate_fundef #Hfind_funct_cm
     lapply (value_eq_ptr_inversion … Hvalue_eq_func) * #cm_func_ptr * #Hcm_func_ptr
+    whd in ⊢ ((??%?) → ?); cases func_ptr in Hfind_funct Hfind_funct_cm Hregion_is_code Hpoff_eq_zero;
+    whd in ⊢ ((??%?) → ?);
+    cases CL_callee_ptr in Hfind_funct Hfind_funct_cm HCL_callee_ptr_region_eq_Code HCL_callee_ptr_offset_eq_zero;
     #cm_block #cm_off #Hfind_funct #Hfind_funct_cm #Hregion_is_code #Hpoff_eq_zero destruct (Hpoff_eq_zero)
     whd in ⊢ ((??%?) → ?);
     [ 1,2: >(HEm_fn_id … cm_block Hregion_is_code)
     | 3: >(HEm_fn_id … cm_block Hregion_is_code) ]
+    normalize nodelta cases cm_func_ptr in Hcm_func_ptr; #cm_block' #cm_off'
+    normalize nodelta
+    cases cm_func_ptr in Hcm_func_ptr; #cm_block' #cm_off'
     #Hcm_func_ptr #Heq destruct (Hcm_func_ptr Heq)
     [ 1,2: >addition_n_0 >mk_offset_offv_id
 …
       | 3: cases sInv * * normalize nodelta * #_ #_ #Hall #_ #_ @Hall ]
       #Hall
       cases (eval_exprlist_simulation …  Halloc_hyp Hcl_env_hyp Hinjection Hmatching ???? Hexec_arglist Hargs_spec Hall)
+      cases (eval_exprlist_simulation …  Halloc_hyp Hcl_env_hyp Hinjection Hmatching ???? Hexec_CL_args Hargs_spec Hall)
       #cm_values * #Hcm_exec_list #Hcl_cm_values_eq >Hcm_exec_list
     | 3:
+      (* Arrrgh *)
+      lapply (eval_exprlist_simulation …  Halloc_hyp Hcl_env_hyp Hnew_inj ????? Hexec_arglist Hargs_spec ?)
+      try assumption *
+      #cm_values * #Hcm_exec_list #Hcl_cm_values_eq >Hcm_exec_list
+      lapply (eval_exprlist_simulation …  Halloc_hyp Hcl_env_hyp Hinjection ????? Hexec_CL_args Hargs_spec ?)
+      try assumption
+      * #cm_values * #Hcm_exec_list #Hcl_cm_values_eq >Hcm_exec_list
+    ]
     whd in match (m_bind ?????); normalize nodelta whd @conj
     [ 2,4,6: #Habsurd destruct (Habsurd) ]
     @conj
+    [ 1,3,5: normalize try @refl
+             >append_nil >append_nil @refl ]
+    [ 1,3,5: normalize try @refl >append_nil >append_nil @refl ]
     [ 1: generalize in match (proj1 ? (expr_vars ???) (proj1 ???)); #Hugly_pres
     | 2: generalize in match (proj1 ? (expr_vars ???) (proj1 ???)); #Hugly_pres
     | 3: ]
+(*    [ 3: >addition_n_0 ]*)
+    [ 1,2: (* no return or return to CM local variable *)
+           @(CMR_call_nostore … tmp_u) try assumption
+           [ 2,4: (* TODO: prove matching between CL and CM function ids *)
+                  @cthulhu
+    [ 3: @(CMR_call … Htranslate_function … Hinjection … Hmatching … HEm_fn_id) try assumption
+         lapply (alloc_tmp_monotonic … (sym_eq ??? Heq_alloc_tmp)) #Hincl1
+         lapply (alloc_tmp_monotonic … (sym_eq ??? Heq_alloc_tmp')) #Hincl2
+         lapply (transitive_lset_inclusion … Hincl1 Hincl2) #Hincl3
+         try /2 by transitive_lset_inclusion/
+         lapply Htranslate_fundef -Htranslate_fundef
+         lapply Hfundef_fresh_for_tmp_u -Hfundef_fresh_for_tmp_u
+         cases CL_callee_fundef normalize nodelta
+         [ 1: #cl_called_f #Hfundef_fresh_for_tmp_u #Htranslate_fundef @ClCm_cont_call_store
+         | 2: #id #tl #ty #Hfd_fresh
+              whd in ⊢ ((??%?) → ?); #Heq destruct (Heq) normalize nodelta @I ]
+    | 1,2: (* no return or return to CM local variable *)
+           @(CMR_call … Htranslate_function … Hinjection … Hmatching … HEm_fn_id) try assumption
+           cases CL_callee_fundef in Hfundef_fresh_for_tmp_u Htranslate_fundef; normalize nodelta
+           [ 1,3: (* Internal case *)
+             #cl_called_f #Hfundef_fresh_for_tmp_u #Htranslate_fundef
+             whd nodelta in match (typeof ?);
+             [ <(translate_dest_conservation … Htranslate_dest)
+               @ClCm_cont_call_nostore normalize nodelta
+               %{CL_lvalue_block} %{CL_lvalue_offset} %{(typeof lhs)} %{var_id}
+               @conj @refl
+             | @ClCm_cont_call_nostore normalize nodelta @I ]
+           | 2,4: #fid #tl #ty #H1 #H2
+             whd in H2:(??%?); destruct (H2) @I
+           ]
-           lapply Hfind_funct
-           lapply Hfind_funct_cm
-           lapply Htranslate_fundef
-           lapply Hfundef_fresh_for_tmp_u
-           lapply Hassert_type_eq
-           lapply Htype_of_fundef
-           lapply Hlookup
-           cases cl_fundef
-           [ 2,4: #id #typel #ty #HA #HB #HC #HD #HE #HF #HG @I
-           | 1,3: #f #HA #HB #HC #HD #HE #HF #HG normalize nodelta
-                  @conj try @conj try @conj try assumption ]
-    | 3: (* type mismatch *)
-         @(CMR_call_store … tmp_u) try assumption
-         [ 2: (* TODO: prove matching between CL and CM function ids *)
-              @cthulhu ]
-         lapply Hfind_funct
-         lapply Htranslate_fundef
-         lapply Hfundef_fresh_for_tmp_u
-         lapply Hassert_type_eq
-         lapply Htype_of_fundef
-         lapply Hlookup
-         cases cl_fundef
-         [ 2: #id #typel #ty #HA #HB #HC #f #HD #HE @I ]
-         #f #HA #HB #HC #HD #HE #HF normalize nodelta @conj try @conj try @conj
-         try assumption
+    ]
 | 1: (* Skip *)
 …
     #Hreturn_ok #Hlabel_wf generalize in match (conj ????); #Hugly
     whd in ⊢ ((??%?) → ?); #Heq_translate #Hlabel_inclusion
     #Hcont_rel
+    #tmpenv #Htmpenv #Hcont_rel
     lapply Heq_translate -Heq_translate
     lapply Hugly -Hugly
     lapply Hlabel_wf -Hlabel_wf
+    lapply Hugly -Hugly
+    lapply Hlabel_wf -Hlabel_wf
     lapply Hreturn_ok -Hreturn_ok
     lapply Htmps_preserved -Htmps_preserved
+    lapply Htmps_preserved -Htmps_preserved
     lapply Hlabels_translated -Hlabels_translated
     lapply Hstmt_inv -Hstmt_inv
+    lapply Hstmt_inv -Hstmt_inv
     lapply Htranslate_function -Htranslate_function
     lapply Hfresh_globals -Hfresh_globals
+    lapply Hfresh_globals -Hfresh_globals
     lapply Hfresh_function -Hfresh_function
     lapply Htarget_type -Htarget_type
     lapply kInv -kInv
     lapply sInv -sInv
+    lapply Htarget_type -Htarget_type
+    lapply kInv -kInv
+    lapply sInv -sInv
     lapply fInv -fInv
+    lapply stmt_univ -stmt_univ
+    lapply stmt_univ -stmt_univ
+    lapply Htmpenv -Htmpenv
     lapply stmt_univ' -stmt_univ'
     lapply Hlabel_inclusion -Hlabel_inclusion
 …
     [ (* Kstop continuation *)
       (* simplifying the goal using outcome of the inversion *)
       #kcl_ge #kcm_ge #kINV #kcl_f #kcm_f #ktarget_type #kcl_env #kcm_env #kalloc_type #kstack #Hkstack
+      #kcl_ge #kcm_ge #kINV #kcl_f #kcm_f #ktarget_type #kcl_env #kcm_env #kcm_m #kalloc_type #ktmpenv #kstack #Hkstack
       @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
       destruct (HA HB)
       @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
       destruct (HC HD HE)
+      @(jmeq_absorb ?????) #HF @(jmeq_absorb ?????) #HG @(jmeq_absorb ?????) #HH
+      @(jmeq_absorb ?????) #HI @(jmeq_absorb ?????) #HJ @(jmeq_absorb ?????) #HK @(jmeq_absorb ?????) #HL
+      destruct (HF HG HH HI HJ HK HL) #_
+      @(jmeq_absorb ?????) #HF @(jmeq_absorb ?????) #HG @(jmeq_absorb ?????) #HH @(jmeq_absorb ?????) #HI
+      destruct (HF HG HH HI)
+      @(jmeq_absorb ?????) #HJ @(jmeq_absorb ?????) #HK @(jmeq_absorb ?????) #HL @(jmeq_absorb ?????) #HM
+       @(jmeq_absorb ?????) #HN
+      destruct (HJ HK HL HM HN) #_
       (* re-introduce everything *)
       #Hlabel_inclusion
+      #stmt_univ' #stmt_univ #fInv #sInv #kInv #Htarget_type #Hfresh_function #Hfresh_globals
+      #Htranslate_function #Hstmt_inv #Hlabels_translated #Htmps_preserved #Hreturn_ok #Hlabel_wf
+      #stmt_univ' #Htmpenv #stmt_univ #fInv #sInv #kInv #Htarget_type #Hfresh_function #Hfresh_globals
+      #Htranslate_function #Hstmt_inv #Hlabels_translated #Htmps_preserved
+      #Hreturn_ok #Hlabel_wf
       #Hugly generalize in match (conj ????); #Hugly'
       (* reduce statement translation function *)
 …
       (* In this simple case, trivial translation *)
       destruct (Heq_translate)
+      #Em #Htmp_vars_well_allocated #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id #Hframe_spec
+      #Em #Htmp_vars_well_allocated
+      #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id #Hframe_spec #Henv_below
       @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
       destruct (HA HB)
 …
       [ 2: #Habsurd destruct (Habsurd) ]
       (* Use the memory injection stuff to produce a new memory injection *)
       cut (memory_inj Em (free_list cl_m (blocks_of_env kcl_env)) (free cm_m stackptr))
       [ @(freelist_memory_inj_m1_m2 Em cl_m cm_m
+      cut (memory_inj Em (free_list cl_m (blocks_of_env kcl_env)) (free kcm_m stackptr))
+      [ @(freelist_memory_inj_m1_m2 Em cl_m kcm_m
             (free_list cl_m (blocks_of_env kcl_env))
             (free cm_m stackptr) Hinjection (blocks_of_env kcl_env) stackptr ? (refl ??) (refl ??))
+            (free kcm_m stackptr) Hinjection (blocks_of_env kcl_env) stackptr ? (refl ??) (refl ??))
         assumption ]
       #Hinjection'
       @(CMR_return … Halloc_hyp Hcl_env_hyp … Hinjection') try assumption
+      @(CMR_return … Kend … Halloc_hyp Hcl_env_hyp … Hinjection') try assumption
       [ 2: #b lapply (Hmatching b)
            cases (lookup ?? kcl_env b) normalize nodelta
 …
+             ]
+           ]
+      | 1: (* TODO: lemma *) @cthulhu
+      ]
+      | 1: @(tmp_vars_well_allocated_conserved_by_frame_free … Hmatching … Htmp_vars_well_allocated)
+      | 3: @ClCm_cont_stop @Hkstack
+      ]
     | (* Kseq *)
       #kcl_ge #kcm_ge #kINV #kcl_f #kcm_f #ktarget_type #kstack #kalloc_type #kcl_s #kcm_s
       #kcl_env #kcm_env #kcl_k' #kcm_k' #kstmt_univ #kstmt_univ' #klbl_univ #klbl_univ' #klbls #kflag
+      #kcl_ge #kcm_ge #kINV #kcl_f #kcm_f #ktarget_type #kstack #kalloc_type #ktmpenv #kcl_s #kcm_s
+      #kcl_env #kcm_env #kcm_m #kcl_k' #kcm_k' #kstmt_univ #kstmt_univ' #klbl_univ #klbl_univ' #klbls #kflag
       * * * * #kHstmt_inv #kHlabels_translated #kHtmps_preserved
       #kHreturn_ok #kHlabel_wf #kHeq_translate #kHlabel_inclusion #kHcont_rel #_
+      #kHreturn_ok #kHlabel_wf #kHeq_translate #kHlabel_inclusion #kHident_inclusion #kHcont_rel #_
       @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
       destruct (HA HB)
 …
       destruct (HC HD HE)
       @(jmeq_absorb ?????) #HF @(jmeq_absorb ?????) #HG @(jmeq_absorb ?????) #HH @(jmeq_absorb ?????) #HI
+      @(jmeq_absorb ?????) #HJ @(jmeq_absorb ?????) #HK @(jmeq_absorb ?????) #HL
+      destruct (HF HG HH HI HJ HK HL) #_
+      destruct (HF HG HH HI)
+      @(jmeq_absorb ?????) #HJ @(jmeq_absorb ?????) #HK @(jmeq_absorb ?????) #HL @(jmeq_absorb ?????) #HM
+      @(jmeq_absorb ?????) #HN
+      destruct (HJ HK HL HM HN) #_
       #Hlabel_inclusion
       #stmt_univ' #stmt_univ #fInv #sInv #kInv #Htarget_type #Hfresh_function #Hfresh_globals
+      #stmt_univ' #Htmpenv #stmt_univ #fInv #sInv #kInv #Htarget_type #Hfresh_function #Hfresh_globals
       #Htranslate_function #Hstmt_inv #Hlabels_translated #Htmps_preserved #Hreturn_ok #Hlabel_wf
       #Hugly generalize in match (conj ????); #Hugly'
       (* In this simple case, trivial translation *)
       #Heq_translate destruct (Heq_translate) #Em
+      #Htmp_vars_well_alloc #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id #Hframe_spec
+      #Htmp_vars_well_alloc
+      #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id #Hframe_spec #Henv_below
       @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
       destruct (HA HB)
 …
       %{1} whd @conj [ 2: #Habsurd destruct (Habsurd) ] @conj try @refl
       (* close simulation *)
+      @(CMR_normal … kHeq_translate … Hinjection … Hmatching) try assumption
+      (* TODO wrap this up properly, by adding some invariant or by threading stmt_univ' into the cont *)
+      @cthulhu
+      (* TODO: lemma allowing to prove this from [Htmp_vars_well_alloc] + tmp_gen inclusion *)
+      @(CMR_normal … kHeq_translate … kHcont_rel … Hinjection … Hmatching) try assumption
+      (* TODO Invariant on env_below_freshgen *)
+       @cthulhu
     | (* Kwhile continuation *)
       #kcl_ge #kcm_ge #kINV #kcl_f #kcm_f #ktarget_type #kstack #kalloc_type #kcl_env #kcm_env
+      #kcl_ge #kcm_ge #kINV #kcl_f #kcm_f #ktarget_type #kstack #kalloc_type #ktmpenv #kcl_env #kcm_env #kcm_m
       #kcl_k' #kcm_k' #ksz #ksg #kcl_ty #kcl_cond_desc #kcl_body #kHeq_ty #kcm_cond #kcm_body
       #kentry #kexit #kstmt_univ #kstmt_univ' #klbl_univ #klbl_univ' #klbl_univ''
       #klbls #kHtranslate_inv #kHexpr_vars #kHtranslate_expr #kfInv #kHlabel_declared
       #kHinv #kHmklabels #kHeq_translate #kHlabel_inclusion #kHfind_label
+      #kHinv #kHmklabels #kHeq_translate #kHlabel_inclusion #kHident_inclusion #kHfind_label
       (*
       * * * * #kHentry_declared * * * *
 …
       @(jmeq_absorb ?????) #HF @(jmeq_absorb ?????) #HG @(jmeq_absorb ?????) #HH
       @(jmeq_absorb ?????) #HI @(jmeq_absorb ?????) #HJ @(jmeq_absorb ?????) #HK
       @(jmeq_absorb ?????) #HL
       destruct (HF HG HH HI HJ HK HL) #_
+      @(jmeq_absorb ?????) #HL @(jmeq_absorb ?????) #HM @(jmeq_absorb ?????) #HN
+      destruct (HF HG HH HI HJ HK HL HM HN) #_
       #Hlabel_inclusion
       #stmt_univ' #stmt_univ #fInv #sInv #kInv #Htarget_type #Hfresh_function #Hfresh_globals
+      #stmt_univ' #Htmpenv #stmt_univ #fInv #sInv #kInv #Htarget_type #Hfresh_function #Hfresh_globals
       #Htranslate_function #Hstmt_inv #Hlabels_translated #Htmps_preserved #Hreturn_ok #Hlabel_wf
       #Hugly
 …
       (* In this simple case, trivial translation *)
       #Heq_translate destruct (Heq_translate)
+      #Em #Htmp_vars_well_allocated #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching
+      #HEm_fn_id #Hframe_spec
+      #Em #Htmp_vars_well_allocated
+      #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching
+      #HEm_fn_id #Hframe_spec #Henv_below
       @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
       destruct (HA HB)
 …
       @(CMR_while … stacksize … Hcl_env_hyp … Hinjection … kHtranslate_expr … kHmklabels …  kHeq_translate)
       try assumption
+      [ 1: @cthulhu
+         (* TODO: lemma allowing to prove this from [Htmp_vars_well_alloc] + tmp_gen inclusion *)
+         (* TODO wrap this up properly, by adding some invariant or by threading stmt_univ' into the cont *)
+      [ 1: (* TODO: lemma on Henv_below. We need to thread freshgens through cont_rel. *)
+           @cthulhu
       | 2: cases Hmore_invariant * * #_ * * * * #_ #_ * #_ #_ * * #_ #H
+           #_ #_ @H ]
+           #_ #_ @H ]
+    | 4,5: (* Continuations for Scall. TODO *)
+      @cthulhu
+    ]
 | 2: (* Assign *)
 …
      #flag * * * * #Hstmt_inv_cm #Hlabels_translated #Htmps_preserved
      #Hreturn_ok #Hlabel_wf generalize in match (conj ????); #Hugly #Htranslate
+     #Hlabel_inclusion #Hcont_rel
+     #Em #Htmp_vars_well_allocated #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id #Hframe_spec
+     #Hlabel_inclusion #tmpenv #Htmpenv #Hcont_rel
+     #Em #Htmp_vars_well_allocated
+     #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id #Hframe_spec #Henv_below
      @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
      destruct (HA HB)
 …
           normalize nodelta
           [ 1: (* Global *) #r
                #Hlookup_var_success whd in ⊢ ((???%) → ?); #Hlhs_dest_eq
+               #Hlookup_var_success whd in ⊢ ((???%) → ?); #Hlhs_dest_eq
                destruct (Hlhs_dest_eq) normalize nodelta
                generalize in match (conj ????); #Hinvariant
 …
                     whd @conj try @conj try @refl
                     [ 2: #Habsurd destruct (Habsurd) ]
+                    generalize in match (conj ????);
+                    #Hinv_vars
+                    generalize in match (conj ????); #Hinv_vars
                     @CMR_normal try assumption
+                    [ 2: @refl | 1,3,4: ]
+                    [ 1: (* TODO: lemma on preservation of well-allocatedness through stores *) @cthulhu
+                    | 2: (* TODO: lemma on preservation of memory matching through stores *) @cthulhu ]
+                    [ 2: @refl | *: ]
+                    [ 3: @(memory_matching_preserved_by_parallel_stores … Hmatching)
+                    | 2: @(well_allocated_preserved_by_parallel_stores … Htmp_vars_well_allocated)
+                    | 1: @(clight_cminor_cont_rel_parametric_in_mem … Hcont_rel) ]
                | 2: #b #Heq destruct (Heq)
                     lapply (opt_to_res_inversion ???? Hlookup_var_success) #Hlookup_aux
 …
                  ] (refl ? (lookup ?? cl_env var_id)))
                normalize nodelta
                [ (* Contradiction: a stack-allocated variable was necessarily in the environment *)
+               [ (* Contradiction: a stack-allocated variable was necessarily in the environment. TODO *)
                  @cthulhu
                | #Heq destruct (Heq)
 …
                  whd in match (m_bind ?????); normalize nodelta
                  whd @conj try @conj try @refl
                  [ 2: #Habsurd destruct (Habsurd) ]
+                 [ 2: #Habsurd destruct (Habsurd) ]
                  @(CMR_normal … Halloc_hyp) try assumption
+                 [ 2: @refl | 1,3,4,5: ]
+                 [ 1: (* TODO: lemma on preservation of well-allocatedness through stores *) @cthulhu
+                 | 2: (* TODO: lemma on preservation of memory matching through stores *) @cthulhu ]
+                 try @refl
+                 try @(memory_matching_preserved_by_parallel_stores … Hmatching)
+                 try @(well_allocated_preserved_by_parallel_stores … Htmp_vars_well_allocated)
+                 @(clight_cminor_cont_rel_parametric_in_mem … Hcont_rel)
+               ]
           | 3: (* Local *)
+               #Hlookup_var_success whd in ⊢ ((???%) → ?);
+               #Hlookup_var_success
+               cases (type_eq_dec ??) normalize nodelta #Htype_eq_dec
+               whd in ⊢ ((???%) → ?);
                #Heq destruct (Heq) normalize nodelta -Htranslate_statement
                #Htranslate
 …
                normalize nodelta
                [ (* Contradiction: a register-allocated variable was necessarily in the environment *)
+                 (* TODO, cf Hlookup_var_success or sInv *)
                  @cthulhu
                | #Heq destruct (Heq)
 …
                  generalize in match (proj1 ???); #Hpresent
                  generalize in match (conj ????); #Hstmt_vars
+                 @(CMR_normal … Halloc_hyp) try assumption
+                 [ 2: @refl | *: ]
+                 [ (* Need a particular kind of continuation relation *) @cthulhu
+                 | (* Lemma on preservation of well-allocatedness through update_present *) @cthulhu
+                 | (* Memory injection when writing in clight only, and block not mapped *) @cthulhu
+                 | (* Memory matching through env update *) @cthulhu ]
+                 @(CMR_normal … Halloc_hyp) try assumption try @refl
+                 [ 4: @(memory_matching_preserved_by_local_store … Hvalue_eq_rhs Hstore_value_of_type Hmatching)
+                 | 3: @(memory_inj_preserved_by_local_store … Hmatching Hinjection)
+                 | 2: @(tmp_vars_well_allocated_preserved_by_local_store … Hvalue_eq_rhs Hstore_value_of_type Htmp_vars_well_allocated)
+                 | 1: @(clight_cminor_cont_rel_parametric_in_cm_env … Hpresent Hcont_rel) ]
+               ]
+          ]
 …
           whd in match (m_bind ?????); normalize nodelta whd @conj try @conj try @refl
           [ 2: #Habsurd destruct (Habsurd) ]
           @(CMR_normal … Halloc_hyp) try assumption
           [ 2: @refl | *: ]
           [ 1: (* lemma on well_allocated after CL and CM parallel writes *) @cthulhu
           | 2: (* memory matching *) @cthulhu ]
+          @(CMR_normal … Halloc_hyp) try assumption try @refl
+          [ 3: @(memory_matching_preserved_by_parallel_stores … Hmatching)
+          | 2: @(well_allocated_preserved_by_parallel_stores … Htmp_vars_well_allocated)
+          | 1: @(clight_cminor_cont_rel_parametric_in_mem … Hcont_rel) ]
+     ]
 | 4: (* Seq *)
 …
      (* introduce everything *)
      #fInv #sInv #kInv #Htarget_type #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function
      #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls
+     #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls
      #flag * * * * #Hstmt_inv_cm #Hlabels_translated #Htmps_preserved
      #Hreturn_ok #Hlabel_wf generalize in match (conj ????); #Hugly #Htranslate #Hlabel_inclusion
+     #Hcont_rel
+     #Em #Htmp_vars_well_allocated #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id #Hframe_spec
+     #tmpenv #Htmpenv  #Hcont_rel
+     #Em #Htmp_vars_well_allocated
+     #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id #Hframe_spec #Henv_below
      @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
      destruct (HA HB)
 …
           @transitive_lset_inclusion @lset_inclusion_union %1
           @reflexive_lset_inclusion
+     | 2: @(ClCm_cont_seq … Htrans_stm2)
+     | 2: lapply (translation_entails_ident_inclusion … Htrans_stm2) #H
+          @(transitive_lset_inclusion … (translation_entails_ident_inclusion … Htrans_stm2))
+          assumption
+     | 3: @(ClCm_cont_seq … Htrans_stm2)
           [ 1: lapply Hlabel_inclusion @transitive_lset_inclusion @lset_inclusion_union %2
                @reflexive_lset_inclusion
+          | 2: assumption ]
+     | 3: @cthulhu ]
+| *: @cthulhu ]
+          | 2: assumption
+          | 3: assumption ]
+     ]
+| *: (* Other statements *) @cthulhu ]
 | 2: (* Return state *)
   #cl_ge #cm_ge #INV' #cl_f #cm_f #alloc_type
   #cl_env #cl_m #cm_env #c_m #cm_st #stackptr #stacksize
   #stmt_univ #Em #Htmp_vars_wa #Hcharac #Hexec_alloc #Hinj #Hmatch #Hem_fn_id #Hframe
+  #cl_ge #cm_ge #INV' #cl_k #cm_k #cm_st #cl_f #cm_f #alloc_type
+  #cl_env #cl_m #cm_env #cm_mt #stackptr #stacksize
+  #stmt_univ #tmpenv #Htmpenv #Em #Htmp_vars_wa #Hcharac #Hexec_alloc #Hinj #Hmatch #Hem_fn_id #Hframe #Hcont
   @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
   destruct (HA HB)
 …
   whd in Hclight_normal:%;
   @False_ind @Hclight_normal
+| 3: (* Call state, nostore *)
+  #cl_ge #cm_ge #cl_f #cm_f #INV' #alloc_types
+  #cl_env #cl_m #cm_env #cm_m #stackptr #u #cl_fundef #cm_fundef
+  #Hglobals_fresh #Hfundef_fresh #rettyp #Hrettyp #cl_k #cm_k #fblock
+  #Hcont_rel #cl_fun_id #cm_fun_id #Hfun_id_eq #cl_retval #cm_retval
+  #sInv #fInv #kInv #cl_argvals #cm_argvals #cm_stack
+| 3: (* Call state *)
+  #cl_ge #cm_ge #INV' #cl_k #cm_k #cm_st #cl_f #cm_f #cl_fundef #cm_fundef
+  #fblock #target_type #alloc_type #cl_env #cl_m #cm_env #cm_m #stackptr #stacksize
+  #func_univ #Hgobals_fresh #Hfundef_fresh #Htranslate_function #Hfind_cl #Hfind_cm
+  #cl_id #cm_id #stmt_univ #tmpenv #Htmpenv #Hcont_rel
+  #Em #Htmp_vars_wa #Hcharac #Hexec_alloc #Hinj #Hmatch #Hem_fn_id #Hframe
+  #cl_args_values #cm_args_values #Hall2
   @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
   destruct (HA HB)
   @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
   destruct (HC HD HE)
+  destruct (HC HD HE) #_
   whd in Hclight_normal:%;
   @False_ind @Hclight_normal
+| 4: (* Call state, store *)
+  #cl_ge #cm_ge #cl_f #cm_f #INV' #alloc_types
+  #cl_env #cl_m #cm_env #cm_m #cm_stack #stackptr #u #cl_fundef #cm_fundef
+  #Hglobals_fresh #Hfundef_fresh #rettyp #Hrettyp #cl_k #cm_k #fblock
+  #Hcont_rel #cl_fun_id #cm_fun_id #Hfun_id_eq
+  #cl_rettyp #cl_retval #cl_retrace #cm_retval #cl_lhs #cm_lhs
+  #Hinvariant_on_cm_lhs #Hexec_lvalue #Htranslate_dest #cm_ret_var
+  #sInv #fInv #kInv #cl_argvals #cm_argvals #cm_stack
+  @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
+  destruct (HA HB)
+  @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
+  destruct (HC HD HE)
+  whd in Hclight_normal:%;
+  @False_ind @Hclight_normal
+| 5: (* Intermediary While state *)
+| 4: (* Intermediary While state *)
      (* ---------------------------------------------------------------------- *)
 #cl_ge #cm_ge #INV'
 …
 #cm_stack #rettyp #kInv #fInv #sInv #Heq_ty #Hrettyp_eq #func_univ #Hfresh_globals #Hfresh_function
 #Htranslate_function #Hcont_rel
 #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbl_univ'' #lbls
 #Em #Htmp_vars_well_allocated #Halloc_hyp
 #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id #Hframe_spec #Hexpr_vars #Htranslate_expr
 #Hentry_ex #Hexit_ex #Htranslate_inv #Hmk_labels #Htranslate_statement
+#stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbl_univ'' #tmpenv #Htmpenv #Hcont_rel
+#Em #Htmp_vars_well_allocated
+#Hcharacterise #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id #Hframe_spec #Henv_below
+#Hexpr_vars #Htranslate_expr #Hentry_ex #Hexit_ex #Htranslate_inv #Hmk_labels #Htranslate_statement
 #Hlabel_inclusion #Hlabel_exists #Hinv1 #Hinv2 #Hfind_label
 @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
 …
   generalize in match (proj1 ???); #Hpresent_ifthenelse
   (* Exhibit simulation of condition evaluation *)
+  lapply (eval_expr_sim … Halloc_hyp … Hcl_env_hyp … Hinjection … Hmatching) * #Hsim #_
+  lapply (eval_expr_sim … Hcharacterise … Hcl_env_hyp … Hinjection … Hmatching) * #Hsim #_
+  (* The type of Hsim forces us to wrap cm_cond into a dummy cast. *)
   lapply (Hsim (Expr cl_cond_desc cl_cond_ty) (CMcast ?? cm_cond ?))
+  [ >Heq_ty @refl ] -Hsim #Hsim
+  lapply (Hsim … Hexpr_vars … Htranslate_expr ??? Hcl_exec_cond)
+  [ lapply Hpresent_ifthenelse whd in ⊢ (% → ?); <Heq_ty >CMcast_identity #H @H ]
+  [ >Heq_ty @refl ] -Hsim
+  whd in match (typeof ?); #Hsim
+  lapply (Hsim ??????)
+  [ 2: <Heq_ty >CMcast_identity assumption
+  | 1: assumption
+  | 6: <Heq_ty >CMcast_identity assumption
+  | 5: lapply Htranslate_expr lapply Hexpr_vars lapply cm_cond -cm_cond
+       >Heq_ty #cm_cond #Hexpr_vars @(jmeq_absorb ?????) #Hsol @Hsol
+  | *: ]
   * #cm_val_cond * #Hcm_eval_cond #Hvalue_eq -Hsim
   cut (eval_expr cm_ge (ASTint sz sg) cm_cond cm_env Hpresent_ifthenelse stackptr cm_m = OK ? 〈tr, cm_val_cond〉)
 …
   generalize in match (proj1 ???); #Hpresent_ifthenelse
   (* Exhibit simulation of condition evaluation *)
   lapply (eval_expr_sim … Halloc_hyp … Hcl_env_hyp … Hinjection … Hmatching) * #Hsim #_
+  lapply (eval_expr_sim … Hcharacterise … Hcl_env_hyp … Hinjection … Hmatching) * #Hsim #_
   lapply (Hsim (Expr cl_cond_desc cl_cond_ty) (CMcast ?? cm_cond ?))
+  [ >Heq_ty @refl ] -Hsim #Hsim
+  lapply (Hsim … Hexpr_vars … Htranslate_expr ??? Hcl_exec_cond)
+  [ lapply Hpresent_ifthenelse whd in ⊢ (% → ?); <Heq_ty >CMcast_identity #H @H ]
+  [ >Heq_ty @refl ] -Hsim
+  whd in match (typeof ?); #Hsim
+  lapply (Hsim ??????)
+  [ 2: <Heq_ty >CMcast_identity assumption
+  | 1: assumption
+  | 6: <Heq_ty >CMcast_identity assumption
+  | 5: lapply Htranslate_expr lapply Hexpr_vars lapply cm_cond -cm_cond
+       >Heq_ty #cm_cond #Hexpr_vars @(jmeq_absorb ?????) #Hsol @Hsol
+  | *: ]
   * #cm_val_cond * #Hcm_eval_cond #Hvalue_eq -Hsim
   cut (eval_expr cm_ge (ASTint sz sg) cm_cond cm_env Hpresent_ifthenelse stackptr cm_m = OK ? 〈tr, cm_val_cond〉)
 …
   whd @conj try @conj
   [ 3: #Habsurd destruct (Habsurd)
   | 1: normalize >append_nil >append_nil @refl
+  | 1: normalize >append_nil >append_nil @refl
   | 2: @(CMR_normal … DoNotConvert) try assumption
+       [ 2: @refl | ]
+       try @refl
+       @(env_below_freshgen_preserved_by_translation … Htranslate_statement)
+       assumption
+  ]
+]
 …
+lemma clight_cminor_call_return :
+  ∀g1, g2.
+  ∀INV:clight_cminor_inv g1 g2.
+  ∀s1,s1'.
+  clight_cminor_rel g1 g2 INV s1 s1' →
+  match Clight_classify s1 with
+  [ cl_call ⇒ true
+  | cl_return ⇒ true
+  | _ ⇒ false ] →
+  ∀s2,tr. step … (pcs_exec cl_pre) g1 s1 = Value … 〈tr, s2〉 →
+  ∃m. after_n_steps m ?? (pcs_exec cm_pre) g2 s1' (λs.cminor_normal s) (λtr',s2'.
+    tr = tr' ∧
+    clight_cminor_rel g1 g2 INV s2 s2' ∧
+      (m = 0 → lex_lt (measure_Clight s2) (measure_Clight s1))
+  ).
+#g1 #g2 #INV #s1 #s1' #Hstate_rel #Hclight_class
+inversion Hstate_rel
+[ 1: (* normal *)
+  #cl_ge #cm_ge #INV' #cl_s
+  #cm_s #cl_k #cm_k #cm_st #cl_f #cm_f #rettyp
+  #alloc_type #cl_env #cl_m #cm_env #cm_m #stackptr #stacksize
+  (* introduce everything *)
+  #fInv #sInv #kInv #Htarget_type #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function
+  #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls
+  #flag  #Htrans_inv #Htrans_stmt #Hincl #HA #HB #HC
+  #HE #HF #HG #HI #HJ #HK
+  @(jmeq_absorb ?????) #H1 @(jmeq_absorb ?????) #H2
+  destruct (H1 H2)
+  @(jmeq_absorb ?????) #H3 @(jmeq_absorb ?????) #H4 @(jmeq_absorb ?????) #H5
+  destruct (H3 H4 H5)
+  @False_ind @Hclight_class
+| 5:
+  #cl_ge #cm_ge #INV' #cl_s
+  #cm_s #cl_k #cm_k #cm_st #cl_f #cm_f #rettyp
+  #alloc_type #cl_k #cm_k #sz #sg #cl_ty #cl_cond_desc #cl_body #entry_lab #exit_lab
+  #cm_cond #cm_body #cm_stack #rettyp' #kInv
+  (* introduce everything *)
+  #fInv #sInv #kInv #Htarget_type #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function
+  #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls
+  #lbl1 #lbl2 #Em #Htmp_vars #Hcharac #Hexec #Hinj #Hmatching #Hem #Hframe #Hcond_tr
+  #Htransl #Hex1 #Hex2 #Htransinv #Hmklabs #Htranstmt #Hincl
+  #Hlabdecl #Hinv1 #Hinv2 #Hfindlab
+  @(jmeq_absorb ?????) #H1 @(jmeq_absorb ?????) #H2
+  destruct (H1 H2)
+  @(jmeq_absorb ?????) #H3 @(jmeq_absorb ?????) #H4 @(jmeq_absorb ?????) #H5
+  destruct (H3 H4 H5)
+  @False_ind @Hclight_class
+| *: @cthulhu
+] qed.
 …
   make_initial_state ?? clight_fullexec cl_program = OK ? s →
   make_initial_state ?? Cminor_fullexec cm_program = OK ? s' →
   ∃INV. clight_cminor_rel INV s s'. *)
+  ∃INV. clight_cminor_rel INV s

Note: See TracChangeset for help on using the changeset viewer.

Context Navigation

Changeset 3036

Legend:

src/Clight/toCminorCorrectness.ma

Download in other formats: