source: src/Clight/toCminorCorrectness.ma @ 3195

(*
include "Clight/toCminor.ma".
include "Clight/CexecInd.ma".
include "common/Globalenvs.ma".
include "Clight/memoryInjections.ma".
include "Clight/Clight_abstract.ma".
include "Cminor/Cminor_abstract.ma".
*)
include "common/Measurable.ma".

(* Expr simulation. Contains important definitions for statements, too.  *)
include "Clight/toCminorCorrectnessExpr.ma".

(* When we characterise the local Clight variables, those that are stack
   allocated are given disjoint regions of the stack. *)
lemma characterise_vars_disjoint : ∀globals,f,vartypes,stacksize,id,n,ty.
  characterise_vars globals f = 〈vartypes, stacksize〉 →
  lookup ?? vartypes id = Some ? 〈Stack n,ty〉 →
  ∀id',n',ty'. id ≠ id' →
  lookup ?? vartypes id' = Some ? 〈Stack n',ty'〉 →
  n' + sizeof ty' ≤ n ∨ n + sizeof ty ≤ n'.
#globals * #ret #args #vars #body #vartypes #stacksize #id #n #ty
whd in ⊢ (??%? → ?);
generalize in match vartypes; -vartypes
generalize in match stacksize; -stacksize
elim (args@vars)
[ #stacksize #vartypes #CHAR #L @⊥ whd in CHAR:(??%?); destruct
  elim globals in L;
  [ normalize #L destruct
  | * * #id' #r #ty' #tl #IH
    whd in match (foldr ?????);
    #L cases (lookup_add_cases ??????? L)
    [ * #E1 #E2 destruct
    | @IH
    ]
  ]
| * #id1 #ty1 #tl #IH #stacksize #vartypes
  whd in match (foldr ?????);
  (* Avoid writing out the definition again *)
  letin ih ≝ (foldr ? (Prod ??) ?? tl) in IH ⊢ %;
  lapply (refl ? ih) whd in match ih; -ih
  cases (foldr ? (Prod ??) ?? tl) in ⊢ (???% → %);
  #vartypes' #stack' #FOLD #IH
  whd in ⊢ (??(match % with [_⇒?])? → ?);
  cases (orb ??)
  #CHAR whd in CHAR:(??%?); destruct
  #L cases (lookup_add_cases ??????? L)
  [ 1,3: * #E1 #E2 destruct
    #id' #n' #ty' #NE >lookup_add_miss /2/
    #L' %1 -L -IH
    generalize in match vartypes' in FOLD L' ⊢ %; -vartypes'
    generalize in match stack'; -stack'
    elim tl
    [ #stack' #vartypes2 whd in ⊢ (??%? → ?); #F destruct #L' @⊥
      elim globals in L';
      [ normalize #E destruct
      | * * #id2 #r2 #ty2 #tl2 #IH whd in match (foldr ?????);
        #L cases (lookup_add_cases ??????? L)
        [ * #E1 #E2 destruct
        | @IH
        ]
      ]
    | * #id2 #ty2 #tl2 #IH #stack' #vartypes'
      whd in ⊢ (??%? → ?); cases (foldr ? (Prod ??) ???) in IH ⊢ %;
      #vartypes2 #stack2 #IH
      whd in ⊢ (??%? → ?);
      cases (orb ??)
      [ #E whd in E:(??%?); destruct #L cases (lookup_add_cases ??????? L)
        [ * #E1 #E2 destruct //
        | #L'' lapply (IH ?? (refl ??) L'') /2/
        ]
      | #E whd in E:(??%?); destruct #L cases (lookup_add_cases ??????? L)
        [ * #E1 #E2 destruct
        | #L'' lapply (IH ?? (refl ??) L'') /2/
        ]
      ]
    ]
  | -L #L #id' #n' #ty' #NE #L'
    cases (lookup_add_cases ??????? L')
    [ * #E1 #E2 destruct
      %2 -IH -L'
      generalize in match vartypes' in FOLD L; -vartypes'
      generalize in match stack'; -stack'
      elim tl
      [ #stack' #vartypes' whd in ⊢ (??%? → ?); #F destruct #L @⊥
        elim globals in L;
        [ normalize #E destruct
        | * * #id1 #r1 #ty1 #tl1 #IH whd in match (foldr ?????);
          #L cases (lookup_add_cases ??????? L)
          [ * #E1 #E2 destruct
          | @IH
          ]
        ]
      | * #id1 #ty1 #tl1 #IH #stack' #vartypes'
        whd in ⊢ (??%? → ?); cases (foldr ? (Prod ??) ???) in IH ⊢ %;
        #vartypes2 #stack2 #IH
        whd in ⊢ (??%? → ?);
        cases (orb ??)
        #E whd in E:(??%?); destruct
        #L cases (lookup_add_cases ??????? L)
        [ 1,3: * #E1 #E2 destruct //
        | 2,4: #L' lapply (IH ?? (refl ??) L') /2/
        ]
      ]
    | @(IH … (refl ??) L … NE)
    ]
  | -L #L #id' #n' #ty' #NE #L'
    cases (lookup_add_cases ??????? L')
    [ * #E1 #E2 destruct
    | @(IH … (refl ??) L … NE)
    ]
  ]
] qed.

(* And everything is in the stack frame. *)

lemma characterise_vars_in_range : ∀globals,f,vartypes,stacksize,id,n,ty.
  characterise_vars globals f = 〈vartypes, stacksize〉 →
  lookup ?? vartypes id = Some ? 〈Stack n,ty〉 →
  n + sizeof ty ≤ stacksize.
#globals * #ret #args #vars #body whd in match (characterise_vars ??);
elim (args@vars)
[ #vartypes #stacksize #id #n #ty #FOLD #L @⊥
  whd in FOLD:(??%?); destruct elim globals in L;
  [ #E normalize in E; destruct
  | * * #id' #r' #ty' #tl' #IH
    whd in match (foldr ?????); #L cases (lookup_add_cases ??????? L)
    [ * #E1 #E2 destruct
    | @IH
    ]
  ]
| * #id' #ty' #tl #IH #vartypes #stacksize #id #n #ty
  whd in match (foldr ?????); cases (foldr ? (Prod ??) ???) in IH ⊢ %;
  #vartypes' #stackspace' #IH
  whd in ⊢ (??(match % with [_⇒?])? → ?);
  cases (orb ??) whd in ⊢ (??%? → ?);
  #E destruct #L cases (lookup_add_cases ??????? L)
  [ 1,3: * #E1 #E2 destruct //
  | 2,4: #L' lapply (IH … (refl ??) L') /2/
  ]
] qed.



(* Put knowledge that Globals are global into a more useful form than the
   one used for the invariant. *)   
(* XXX superfluous lemma ? Commenting it for now. 
       if not superfluous : move to toCminorCorrectnessExpr.ma, after
       [characterise_vars_localid] *)
(*
lemma characterise_vars_global : ∀globals,f,vartypes,stacksize.
  characterise_vars globals f = 〈vartypes, stacksize〉 →
  ∀id,r,ty. lookup' vartypes id = OK ? 〈Global r,ty〉 →
  Exists ? (λx.x = 〈〈id,r〉,ty〉) globals ∧
  ¬ Exists ? (λx. \fst x = id) (fn_params f @ fn_vars f).
#globals #f #vartypes #stacksize #CHAR #id #r #ty #L
cases (characterise_vars_src … CHAR id ?)
[ * #r' * #ty' >L
  * #E1 destruct (E1) #EX
  %
  [ @EX
  | % #EX' cases (characterise_vars_localid … CHAR EX')
    #ty' whd in ⊢ (% → ?); >L *
  ]
| * #ty' whd in ⊢ (% → ?); >L *
| whd >(opt_eq_from_res ???? L) % #E destruct
] qed. *)

(* Show how the global environments match up. *)

lemma map_partial_All_to_All2 : ∀A,B,P,f,l,H,l'.
  map_partial_All A B P f l H = OK ? l' →
  All2 ?? (λa,b. ∃p. f a p = OK ? b) l l'.
#A #B #P #f #l
elim l
[ #H #l' #MAP normalize in MAP; destruct //
| #h #t #IH * #p #H #l'
  whd in ⊢ (??%? → ?);
  lapply (refl ? (f h p)) whd in match (proj1 ???);
  cases (f h p) in ⊢ (???% → %);
  [ #b #E #MAP cases (bind_inversion ????? MAP)
    #tl' * #MAP' #E' normalize in E'; destruct
    % [ %{p} @E | @IH [ @H | @MAP' ] ]
  | #m #_ #X normalize in X; destruct
  ]
] qed.
  

definition clight_cminor_matching : clight_program → matching ≝
λp.
  let tmpuniverse ≝ universe_for_program p in
  let fun_globals ≝ map ?? (λidf. 〈\fst idf,Code,type_of_fundef (\snd idf)〉) (prog_funct ?? p) in
  let var_globals ≝ map ?? (λv. 〈\fst (\fst v), \snd (\fst v), \snd (\snd v)〉) (prog_vars ?? p) in
  let globals ≝ fun_globals @ var_globals in
  mk_matching
    ?? (list init_data × type) (list init_data)
    (λvs,f_clight,f_cminor. ∃H1,H2. translate_fundef tmpuniverse globals H1 f_clight H2 = OK ? f_cminor)
    (λv,w. \fst v = w).

lemma clight_to_cminor_varnames : ∀p,p'.
  clight_to_cminor p = OK ? p' →
  prog_var_names … p = prog_var_names … p'.
* #vars #fns #main * #vars' #fns' #main'
#TO cases (bind_inversion ????? TO) #fns'' * #MAP #E
whd in E:(??%%); destruct
-MAP normalize
elim vars
[ //
| * * #id #r * #d #t #tl #IH normalize >IH //
] qed.

lemma clight_to_cminor_matches : ∀p,p'.
  clight_to_cminor p = OK ? p' →
  match_program (clight_cminor_matching p) p p'.
* #vars #fns #main * #vars' #fns' #main'
#TO cases (bind_inversion ????? TO) #fns'' * #MAP #E
whd in E:(??%%); destruct
%
[ -MAP whd in match (m_V ?); whd in match (m_W ?);
  elim vars
  [ //
  | * * #id #r * #init #ty #tl #IH %
    [ % //
    | @(All2_mp … IH) * * #a #b * #c #d * * #e #f #g * /2/
    ]
  ]
| @(All2_mp … (map_partial_All_to_All2 … MAP)) -MAP
  * #id #f * #id' #f' * #H #F cases (bind_inversion ????? F) #f'' * #TRANSF #E
  normalize in E; destruct
  <(clight_to_cminor_varnames … TO)
  % whd
  % [2: % [2: @TRANSF | skip ] | skip ]
| %
] qed.

(* --------------------------------------------------------------------------- *)
(* Clight to Cminor makes use of fresh symbol generators, which store the list
 * of symbols they generate. We need to maintain as an invariant that these grow
 * in a monotonic and consistent fashion. *)
(* --------------------------------------------------------------------------- *)

(* The two following definitions and two lemmas are duplicated from switchRemoval.ma.
 * TODO: factorise this in frontend_misc, if they turn out not to be useless *)
definition fresher_than_or_equal : universe SymbolTag → universe SymbolTag → Prop ≝ 
λu1,u2.
  match u1 with
  [ mk_universe p1 ⇒
    match u2 with
    [ mk_universe p2 ⇒ p2 ≤ p1 ] ].

definition fte ≝ fresher_than_or_equal.

lemma transitive_fte : ∀u1,u2,u3. fte u1 u2 → fte u2 u3 → fte u1 u3.
* #u1 * #u2 * #u3 normalize /2 by transitive_le/
qed.

lemma reflexive_fte : ∀u. fte u u.
* // qed.

(* 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.

(* --------------------------------------------------------------------------- *)
(* Additional invariants not contain in clight_cminor_data *)
(* --------------------------------------------------------------------------- *)

(* Fresh variable ident generator *)
(* tmp_gen     : tmpgen alloc_type; *)

(* Temporary variables generated during conversion are well-allocated. *)
definition tmp_vars_well_allocated ≝
   λtmpenv: list (ident × type).
   λcm_env.
   λcm_m.
   λcl_m.
   λE: embedding.
   ∀local_variable.
   ∀H:present ?? cm_env local_variable.
   ∀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' ∧
           memory_inj E cl_m cm_m'.

(* wrap the above invariant into a clight_cminor_data-eating prop *)
(*
definition tmp_vars_well_allocated' ≝
   λcl_f, cl_ge, cm_ge, INV.
   λframe_data: clight_cminor_data cl_f cl_ge cm_ge INV.
   λtmp_gen: tmpgen (alloc_type … frame_data).
   ∀vars_v, cl_m_v, cm_env_v, cm_m_v.
   vars_v   = alloc_type … frame_data →
   cl_m_v   = cl_m … frame_data →
   cm_env_v = cm_env … frame_data →
   cm_m_v   = cm_m … frame_data →   
   ∀local_variable.
   ∀H:present ?? cm_env_v local_variable.
   ∀ty. Exists ? (λx. x = 〈local_variable, ty〉) (tmp_env … tmp_gen) →
   ∀v. val_typ v (typ_of_type ty) →
   ∃cm_m'. storev (typ_of_type ty) cm_m_v (lookup_present ?? cm_env_v local_variable H) v = Some ? cm_m' ∧
           memory_inj (Em … frame_data) cl_m_v cm_m'. *)

(* --------------------------------------------------------------------------- *)           
(* A measure on Clight states that is decreasing along execution sequences     *)
(* --------------------------------------------------------------------------- *)

(* statements *)
let rec measure_Clight_statement (s : statement) : ℕ ≝
match s with
[ Sskip ⇒ 0
| Ssequence s1 s2 ⇒
  measure_Clight_statement s1 + measure_Clight_statement s2 + 1
| Sifthenelse e s1 s2 =>
  measure_Clight_statement s1 + measure_Clight_statement s2 + 1
| Swhile e s => 
  measure_Clight_statement s + 1
| Sdowhile e s =>
  measure_Clight_statement s + 1
| Sfor s1 e s2 s3 => 
  measure_Clight_statement s1 + 
  measure_Clight_statement s2 +
  measure_Clight_statement s3 + 1
| Sswitch e ls =>
  measure_Clight_ls ls + 1
| Slabel l s => 
  measure_Clight_statement s + 1
| Scost cl s =>
  measure_Clight_statement s + 1
| _ => 1
]
and measure_Clight_ls (ls : labeled_statements) : ℕ :=
match ls with
[ LSdefault s =>
  measure_Clight_statement s
| LScase sz i s ls =>
  measure_Clight_statement s +
  measure_Clight_ls ls
].

(* continuations *)
let rec measure_Clight_cont (cont : cl_cont) : ℕ ≝
match cont with
[ Kstop => 0
| Kseq s k =>
  measure_Clight_statement s +
  measure_Clight_cont k + 1
| Kwhile e s k =>
  measure_Clight_statement s +
  measure_Clight_cont k + 1
| Kdowhile e s k => 
  measure_Clight_statement s +
  measure_Clight_cont k + 1
| Kfor2 e s1 s2 k => 
  measure_Clight_statement s1 +
  measure_Clight_statement s2 +
  measure_Clight_cont k + 1
| Kfor3 e s1 s2 k =>
  measure_Clight_statement s1 +
  measure_Clight_statement s2 +
  measure_Clight_cont k + 1
| Kswitch k =>
  measure_Clight_cont k + 1
| Kcall retaddr f e k =>
  measure_Clight_statement (fn_body f) +
  measure_Clight_cont k + 1
].

(* Shamelessly copying Compcert. *)
definition measure_Clight : Clight_state → ℕ × ℕ ≝
λstate.
match state with
[ State f s k e m ⇒
  〈measure_Clight_statement s + measure_Clight_cont k + 1, measure_Clight_statement s + 1〉
| Callstate fb fd args k m ⇒ 〈0, 0〉
| Returnstate res k m ⇒ 〈0, 0〉
| Finalstate r ⇒ 〈0, 0〉
].

(* Stuff on lexicographic orders *)
definition lexicographic : ∀A:Type[0]. (A → A → Prop) → A × A → A × A → Prop ≝
λA,Ord, x, y.
  let 〈xa, xb〉 ≝ x in
  let 〈ya, yb〉 ≝ y in
  Ord xa ya ∨ (xa = ya ∧ Ord xb yb).

definition lex_lt ≝ lexicographic nat lt.

(* --------------------------------------------------------------------------- *)
(* Simulation relations *)
(* --------------------------------------------------------------------------- *)

definition CMcast : ∀t,t'. CMexpr t → t = t' → CMexpr t'.
#t #t' #e #H destruct (H) @e
qed.

lemma CMcast_identity : ∀t. ∀e: CMexpr t. CMcast t t e (refl ??) = e.
#H1 #H2 @refl qed.

(* relate Clight continuations and Cminor ones. *)
inductive clight_cminor_cont_rel :
  ∀cl_ge, cm_ge.
  ∀INV:  clight_cminor_inv cl_ge cm_ge.     (* stuff on global variables and functions (matching between CL and CM) *)
  ∀cl_fd: clight_fundef.                    (* current Clight function *)
  fundef internal_function →                (* current Cminor 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 *)
  Prop ≝
(* Stop continuation *)
| ClCm_cont_stop:
  ∀cl_ge, cm_ge, INV, cl_f, cm_f, target_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 cm_m alloc_type tmpenv (* stmt_univ stmt_univ' *) target_type Kstop Kend cm_stack

(* Seq continuation *)
| ClCm_cont_seq:
  ∀cl_ge, cm_ge, INV, cl_f, cm_f, target_type.
  ∀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.
  ∀stmt_univ, stmt_univ'.
  ∀lbl_univ, lbl_univ'.
  ∀lbls.
  ∀flag.
  ∀Htranslate_inv.
  translate_statement alloc_type stmt_univ lbl_univ lbls flag target_type cl_s = OK ? «〈stmt_univ',lbl_univ',cm_s〉, Htranslate_inv» →
  (* ---- invariant on label existence ---- *)
  lset_inclusion ? (labels_of cm_s) (labels_of (f_body cm_f)) →
  (* ---- invariant on fresh variables ---- *)
  lset_inclusion ? (tmp_env alloc_type stmt_univ') tmpenv →
  clight_cminor_cont_rel cl_ge cm_ge INV (CL_Internal cl_f) (Internal … cm_f) cl_env cm_env cm_m alloc_type tmpenv (*stmt_univ stmt_univ'*) target_type cl_k' cm_k' stack →
  clight_cminor_cont_rel cl_ge cm_ge INV (CL_Internal cl_f) (Internal … cm_f) cl_env cm_env cm_m alloc_type tmpenv (*stmt_univ stmt_univ'*) target_type (ClKseq cl_s cl_k') (Kseq cm_s cm_k') stack

(* While continuation *)  
| ClCm_cont_while:
  (* Inductive family parameters *)
  ∀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.
  (* elements of the source while statement *)
  ∀sz,sg.
  ∀cl_ty.
  ∀cl_cond_desc.
  ∀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. 
  (* universes used to generate fresh labels and variables *)  
  ∀stmt_univ, stmt_univ'.
  ∀lbl_univ, lbl_univ', lbl_univ''.
  ∀lbls: lenv.
  ∀Htranslate_inv.
  (* relate CL and CM expressions *)
  ∀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 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_seq
            (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_Internal cl_f) (Internal … cm_f) cl_env cm_env cm_m alloc_type tmpenv (* stmt_univ stmt_univ' *) target_type cl_k' cm_k' stack →
  clight_cminor_cont_rel cl_ge cm_ge INV (CL_Internal cl_f) (Internal … cm_f) cl_env cm_env cm_m alloc_type tmpenv (* stmt_univ stmt_univ' *) target_type
    (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, (* callee fn *) cl_fd, cm_fd, (* caller *) cl_f, cm_f, target_type, target_type'.
  ∀stack.
  ∀alloc_type,alloc_type'.
  ∀tmp_env,tmp_env'.
  ∀cl_env,cl_env'.
  ∀cm_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_Internal cl_f) (Internal … cm_f) cl_env' cm_env' cm_m alloc_type' tmp_env' (* stmt_univ stmt_univ' *) target_type' cl_k' cm_k' stack →
  clight_cminor_cont_rel cl_ge cm_ge INV cl_fd cm_fd cl_env cm_env cm_m alloc_type tmp_env (*stmt_univ stmt_univ*) target_type
    (Kcall (Some ? 〈CL_lvalue_block, CL_lvalue_offset, lhs_ty〉) cl_f cl_env cl_k')
    Kend (* cm_k' is on the Cminor stack, below *)
    (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, (* callee *) cl_fd, cm_fd, (* caller *) cl_f, cm_f, target_type, target_type'.
  ∀stack.
  ∀alloc_type,alloc_type'.
  ∀tmpenv, tmpenv'.
  ∀cl_env,cl_env'.
  ∀cm_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_Internal cl_f) (Internal … cm_f) cl_env' cm_env' cm_m alloc_type' tmpenv' (* stmt_univ stmt_univ' *) target_type' cl_k' cm_k' stack →
  clight_cminor_cont_rel cl_ge cm_ge INV cl_fd cm_fd cl_env cm_env cm_m alloc_type tmpenv (*stmt_univ stmt_univ*) target_type
   (Kcall cl_lhs cl_f cl_env cl_k')
   Kend
   (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 *)
  ∀cl_ge, cm_ge.
  (* Relates globals to globals and functions to functions. *)
  ∀INV:  clight_cminor_inv cl_ge cm_ge.  
  (* ---- Statements ---- *)
  (* Clight statement *)  
  ∀cl_s: statement.
  (* Cminor statement *)
  ∀cm_s: stmt.                                            
  (* ---- Continuations ---- *)
  (* 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.
  (* optional return type of the function *)
  ∀rettyp.
  (* 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), related size *)
  ∀stackptr, stacksize.
  (* ---- Cminor invariants ---- *)
  ∀fInv: stmt_inv cm_f cm_env (f_body cm_f).
  ∀sInv: stmt_inv cm_f cm_env cm_s.
  ∀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) →
  (* ---- relate Clight and Cminor functions ---- *)
  ∀func_univ: universe SymbolTag.
  ∀Hfresh_globals: globals_fresh_for_univ ? (globals ?? INV) func_univ.
  ∀Hfresh_function: fn_fresh_for_univ cl_f func_univ.
  translate_function func_univ (globals ?? INV) cl_f Hfresh_globals Hfresh_function = OK ? cm_f →
  (* ---- relate Clight and Cminor statements ---- *)
  (* fresh var generators *)
  ∀stmt_univ,stmt_univ' : tmpgen alloc_type.
  (* fresh label generators *)
  ∀lbl_univ,lbl_univ'   : labgen.
  (* map old labels to new labels *)
  ∀lbls                 : lenv.
  (* specify where to goto when encountering a continue or a break *)
  ∀flag                 : convert_flag.
  (* Invariant on translation produced by [translate_statement] *)
  ∀Htranslate_inv.
  translate_statement alloc_type stmt_univ lbl_univ lbls flag rettyp cl_s = OK ? «〈stmt_univ',lbl_univ',cm_s〉, Htranslate_inv» →
  (* ---- invariant on label existence ---- *)
  lset_inclusion ? (labels_of cm_s) (labels_of (f_body cm_f)) →
  (* ---- relate Clight continuation to Cminor continuation ---- *)
  ∀tmpenv.
  lset_inclusion ? (tmp_env ? stmt_univ') tmpenv →
  clight_cminor_cont_rel cl_ge cm_ge INV (CL_Internal cl_f) (Internal … cm_f) cl_env cm_env cm_m alloc_type tmpenv (*stmt_univ stmt_univ'*) rettyp cl_k cm_k cm_st →
  (* ---- 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)) →
  (* 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.
  (* ---- 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.
  (* Stack pointer (block containing Cminor locals), related size *)
  ∀stackptr, stacksize.
  (* 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.
  (* 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)) →
  clight_cminor_cont_rel cl_ge cm_ge INV (CL_Internal cl_f) (Internal … cm_f) cl_env cm_env cm_m alloc_type tmpenv (*stmt_univ stmt_univ*) (None ?) cl_k cm_k cm_st →
  clight_cminor_rel cl_ge cm_ge INV
    (ClReturnstate Vundef cl_k cl_m)
    (CmReturnstate (None val) cm_m cm_st)
(* --------------------------------------------------------------------------- *)
(* 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 stack *)
  ∀cm_st: stack.
  (* 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.
  (* Clight env/mem *)
  ∀cl_env, cl_m.
  (* Cminor env/mem *)
  ∀cm_env, cm_m.
  (* specify fblock; as a consequence of these and INV we can deduce that
     cm_fundef is the translation of cl_fundef *)
  ∀fun_id.
  find_funct_id clight_fundef cl_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? 〈cl_fundef,fun_id〉 →
  find_funct_id (fundef internal_function) cm_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? 〈cm_fundef,fun_id〉 →
  ∀tmpenv.
  (*match cl_fundef with
  [ CL_Internal _ ⇒*)
     (* specify continuation *)
     clight_cminor_cont_rel cl_ge cm_ge INV cl_fundef cm_fundef cl_env cm_env cm_m (empty_map …) tmpenv target_type cl_k Kend cm_st
(*       ∨
     (∃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.
  (* memory injection *)
  memory_inj Em cl_m cm_m →
  (* Force embedding to compute identity on functions *)
  (∀b. block_region b = Code → Em b = Some ? 〈b, zero_offset〉) →
  ∀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 fun_id cl_fundef cl_args_values cl_k cl_m)
   (CmCallstate 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.
 ∀cl_env, cl_m, cm_env, cm_m, stackptr, stacksize.
 ∀alloc_type.
 ∀cl_k, cm_k.  
 ∀sz,sg, cl_ty, cl_cond_desc.
 ∀cl_body. 
 ∀entry_label, exit_label.
 ∀cm_cond: CMexpr (ASTint sz sg).
 ∀cm_body.
 ∀cm_stack.
 ∀rettyp.
 ∀kInv: cont_inv cm_f cm_env cm_k.
 ∀fInv: stmt_inv cm_f cm_env (f_body cm_f).
 ∀sInv: stmt_inv cm_f cm_env
           ((*St_label entry_label*)
            (St_seq
             (St_ifthenelse sz sg cm_cond (St_seq cm_body (St_goto entry_label)) St_skip)
             (St_label exit_label St_skip))).
 (* Constrain the CL type *)             
 ∀Heq_ty: ASTint sz sg = typ_of_type cl_ty.            
 (* ---- relate return type variable to actual return type ---- *)
 rettyp = opttyp_of_type (fn_return cl_f) →
 (* ---- relate Clight and Cminor functions ---- *)
 ∀func_univ: universe SymbolTag.
 ∀Hfresh_globals: globals_fresh_for_univ ? (globals ?? INV) func_univ.
 ∀Hfresh_function: fn_fresh_for_univ cl_f func_univ.
 translate_function func_univ (globals ?? INV) cl_f Hfresh_globals Hfresh_function = OK ? cm_f → 
 (* ---- relate continuations ---- *)
 ∀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_Internal cl_f) (Internal … 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 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 *)
 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 *)
 (* 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)) →
 (* 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: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)) →
 Exists ? (λl':identifier Label.l'=exit_label) (labels_of (f_body cm_f)) →  
 (* Statement translation *)
 ∀Htranslate_inv.
 mklabels lbl_univ = 〈〈entry_label, exit_label〉, lbl_univ'〉 →
 translate_statement alloc_type stmt_univ lbl_univ' lbls
   (ConvertTo entry_label exit_label) rettyp 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)) →  
 (* Express the fact that the label points where it ought to *)
 ∀Hlabel_exists.
 ∀Hinv1, Hinv2.
 find_label_always entry_label (f_body cm_f) Kend Hlabel_exists cm_f cm_env fInv Hinv1
   = «〈(*St_label entry_label*)
       (St_seq
        (St_ifthenelse sz sg cm_cond (St_seq cm_body (St_goto entry_label))
         St_skip)
        (St_label exit_label St_skip)),
      cm_k〉,
   Hinv2» →
 (clight_cminor_rel cl_ge cm_ge INV
  (ClState cl_f (Swhile (Expr cl_cond_desc cl_ty) cl_body) cl_k cl_env cl_m)
  (CmState cm_f
   ( (*St_label entry_label*)
    (St_seq
     (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)).

   
(*
| 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 ≝
λs. match Clight_classify s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ].

definition cminor_normal : Cminor_state → bool ≝
λs. match Cminor_classify s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ].

definition cl_pre : preclassified_system ≝
  mk_preclassified_system
    clight_fullexec
    (λg. Clight_labelled)
    (λg. Clight_classify)
    (λx,y,H. an_identifier ? one). (* XXX TODO *)

definition cm_pre : preclassified_system ≝
  mk_preclassified_system
    Cminor_fullexec
    (λg. Cminor_labelled)
    (λg. Cminor_classify)
    (λx,y,H. an_identifier ? one). (* XXX TODO *)

(* --------------------------------------------------------------------------- *)
(* General purpose auxilliary lemmas. *)
(* --------------------------------------------------------------------------- *)

lemma invert_assert : 
  ∀b. ∀P. assert b P → b = true ∧ P.
* #P whd in ⊢ (% → ?); #H
[ @conj try @refl @H
| @False_ind @H ]
qed.

lemma res_to_io :
  ∀A,B:Type[0]. ∀C. 
  ∀x: res A. ∀y.
  match x with
  [ OK v ⇒  Value B C ? v
  | Error m ⇒ Wrong … m ] = return y →
  x = OK ? y.
#A #B #C *
[ #x #y normalize nodelta whd in ⊢ ((???%) → ?); #Heq destruct (Heq) @refl
| #err #y normalize nodelta whd in ⊢ ((???%) → ?); #Heq destruct (Heq) ]
qed.

lemma jmeq_absorb : ∀A:Type[0]. ∀a,b: A. ∀P:Prop. (a = b → P) → a ≃ b → P.
#A #a #b #P #H #Heq lapply (jmeq_to_eq ??? Heq) #Heq' @H @Heq' qed.

(* wrap up some trivial bit of reasoning to alleviate strange destruct behaviour *)
lemma pair_eq_split : 
  ∀A,B:Type[0]. ∀a1,a2:A. ∀b1,b2:B. 
  〈a1,b1〉 = 〈a2, b2〉 →
  a1 = a2 ∧ b1 = b2.
#A #B #a1 #a2 #b1 #b2 #Heq destruct (Heq) @conj try @refl
qed.

lemma ok_eq_ok_destruct :
  ∀A:Type[0]. ∀a,b:A. OK ? a = OK ? b → a = b.
#H1 #H2 #H3 #H4 destruct @refl qed.

lemma sigma_eq_destruct  : ∀A:Type[0]. ∀a,b:A. ∀P: A → Prop. ∀Ha: P a. ∀Hb: P b.  «a, Ha» = «b,Hb» → a = b ∧ Ha ≃ Hb.
#A #a #b #P #Ha #Hb #Heq destruct (Heq)
@conj try %
qed.

(* inverting find_funct and find_funct_ptr *)
lemma find_funct_inversion : 
  ∀F: Type[0]. ∀ge: genv_t F. ∀v: val. ∀res: F.
      find_funct F ge v = Some ? res →
      (∃ptr. v = Vptr ptr ∧
            (poff ptr) = zero_offset ∧
            block_region (pblock ptr) = Code ∧
            (∃p. block_id (pblock ptr) = neg p ∧
                 lookup_opt … p (functions … ge) = Some ? res)).
#F #ge #v #res
cases v
[ | #sz #i | | #ptr ]
whd in ⊢ ((??%?) → ?);
#Heq destruct (Heq)
%{ptr} @conj try @conj try @conj try @refl
lapply Heq -Heq
@(eq_offset_elim … (poff ptr) zero_offset) //
normalize nodelta
[ 1,3,5: #_ #Habsurd destruct (Habsurd) ]
#Heq destruct (Heq)
whd in ⊢ ((??%?) → ?);
cases ptr #blo #off cases (block_region blo) normalize nodelta
[ 1,3: #Habsurd destruct (Habsurd) ]
[ // ]
cases (block_id blo) normalize nodelta
[ #Habsurd destruct (Habsurd) | #p #Habsurd destruct (Habsurd) ]
#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. *)
lemma translate_dest_id_inversion :
  ∀var_types, e, var_id, H.
   translate_dest var_types e = return IdDest var_types ? var_id H →
   e = Expr (Evar var_id) (typeof e).
@cthulhu
(*   
#vars #e #var_id #ty #H
cases e #ed #ty'
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 ]
whd in ⊢ ((??%%) → ?);
#Heq
[ 1,4,5,6,7,8,9,10,11,13: destruct (Heq)
| 3,12: cases (bind_inversion ????? Heq) * #H1 #H2 #H3 cases H3
        #_ whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) ]
lapply Heq -Heq
change with (bind2_eq ????? ) in ⊢ ((??%?) → ?); #Heq
cases (bind2_eq_inversion ?????? Heq)
#alloctype
(* * #alloctype *) * #typ' *
cases alloctype
[ #r | #n | ] normalize nodelta #Hlookup'
[ 1,2: whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) ]
whd in ⊢ ((??%%) → ?); #Heq' destruct (Heq')
@refl*)
qed.


(* Note: duplicate in switchRemoval.ma *)
lemma fresh_elim : ∀u. ∃fv',u'. fresh SymbolTag u = 〈fv', u'〉. #u /3 by ex_intro/ qed.

lemma fresh_elim_lab : ∀u. ∃fv',u'. fresh Label u = 〈fv', u'〉. #u /3 by ex_intro/ qed.


lemma breakup_dependent_match_on_pairs :
 ∀A,B,C: Type[0].
 ∀term: A × B.
 ∀F: ∀x,y. 〈x, y〉 = term → C.
 ∀z:C.
 match term
 return λx.x = term → ? with 
 [ mk_Prod x y ⇒ λEq. F x y Eq ] (refl ? term) = z →
 ∃xa,xb,H. term = 〈xa, xb〉 ∧
           F xa xb H = z.
#A #B #C * #xa #xb #F #z normalize nodelta #H %{xa} %{xb} %{(refl ??)} @conj try @conj
// qed.

(* --------------------------------------------------------------------------- *)
(* Extending simulation results on expressions to particular cases             *)
(* --------------------------------------------------------------------------- *)

lemma translate_expr_sigma_welltyped : ∀vars, cl_expr, cm_expr.
  translate_expr_sigma vars cl_expr = OK ? cm_expr →
  dpi1 ?? (pi1 ?? cm_expr) = typ_of_type (typeof cl_expr).
#vars #cl_expr * * #typ #cm_expr normalize nodelta #Hexpr_vars
whd in ⊢ ((??%?) → ?); #H
cases (bind_inversion ????? H) -H * #cm_expr' #Hexpr_vars' *
#Htranslate_expr
whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) @refl
qed.

lemma translate_exprlist_sigma_welltyped :
  ∀vars, cl_exprs, cm_exprs.
  mmap_sigma ??? (translate_expr_sigma vars) cl_exprs = OK ? cm_exprs →
  All2 ?? (λcl, cm. dpi1 ?? cm = typ_of_type (typeof cl)) cl_exprs (pi1 ?? cm_exprs).
#vars #cl_exprs
elim cl_exprs
[ * #cm_exprs #Hall whd in ⊢ ((??%?) → ?); #Heq destruct (Heq) @I
| #hd #tl #Hind * #cm_exprs #Hall #H
  cases (bind_inversion ????? H) -H
  * * #cm_typ #cm_expr normalize nodelta
  #Hexpr_vars_cm * #Htranslate_hd
  lapply (translate_expr_sigma_welltyped … Htranslate_hd)
  #Heq_cm_typ #H
  cases (bind_inversion ????? H) -H
  #cm_tail lapply (Hind cm_tail) cases cm_tail
  #cm_tail_expr #Hall_tail -Hind #Hind * #Heq_cm_tail normalize nodelta
   whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) whd @conj
   [ @Heq_cm_typ
   | @Hind assumption ]
] qed.

lemma translate_dest_MemDest_simulation :
  ∀cl_f  : function.
  ∀cl_ge : genv_t clight_fundef.
  ∀cm_ge : genv_t (fundef internal_function).
  ∀INV   : clight_cminor_inv cl_ge cm_ge.
  ∀alloc_type.  
  ∀cl_env, cl_m, cm_env, cm_m, stackptr.
  ∀Em.
  ∀stacksize     : ℕ.  
  ∀alloc_hyp     : characterise_vars (globals ?? INV) cl_f = 〈alloc_type, stacksize〉.
  ∀cl_cm_env_hyp : ∃m,m'. exec_alloc_variables empty_env m (fn_params cl_f @ fn_vars cl_f) = 〈cl_env,m'〉.
  ∀injection     : memory_inj Em cl_m cm_m.
  ∀matching      : memory_matching Em cl_ge cm_ge cl_m cm_m cl_env cm_env INV stackptr alloc_type.
  (* decorrelate goal from input using some eqs *)
  ∀cl_expr. ∀cm_expr. 
  ∀cl_block, cl_offset, trace.
  ∀Hyp_present.  
     translate_dest alloc_type cl_expr = OK ? (MemDest … cm_expr) →
     exec_lvalue cl_ge cl_env cl_m cl_expr = OK ? 〈〈cl_block, cl_offset〉, trace〉 →
     ∃cm_val. eval_expr cm_ge ASTptr cm_expr cm_env Hyp_present stackptr cm_m = OK ? 〈trace, cm_val〉 ∧
              value_eq Em (Vptr (mk_pointer cl_block cl_offset)) cm_val.     
#cl_f #cl_ge #cm_ge #INV #alloc_type
#cl_env #cl_m #cm_env #cm_m #stackptr #Em #stacksize #alloc_hyp #cl_env_hyp #injection #matching
#cl_expr * #cm_expr #Hexpr_vars #cl_block #cl_offset #trace #Hyp_present
whd in match (translate_dest ??); cases cl_expr #cl_desc #cl_typ normalize nodelta
cases cl_desc normalize nodelta
[ #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 ]
#Htranslate
[ 2:
| *: cases (bind_inversion ????? Htranslate) -Htranslate * #cm_expr' #Hexpr_vars' *
     #Htranslate_addr
     whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) #Hexec_lvalue
     cases (eval_expr_sim cl_ge cm_ge INV cl_f alloc_type stacksize alloc_hyp … cl_env_hyp … injection … matching)
     #_ #Hsim
     @(Hsim ??? Hexpr_vars … Htranslate_addr ??? ? Hexec_lvalue) ]
cases (bind2_eq_inversion ?????? Htranslate) -Htranslate *
[ #r | #n | ]
* #cl_type * #Heq_lookup normalize nodelta
whd in ⊢ ((??%%) → ?); [3: cases (typ_eq ??) #Htyp whd in ⊢ (??%% → ?); ] #Heq destruct (Heq)
whd in ⊢ ((??%?) → ?);
@(match lookup SymbolTag block cl_env id 
  return λx. (lookup SymbolTag block cl_env id = x) → ?
  with
  [ None ⇒ ?
  | Some loc ⇒ ? 
  ] (refl ? (lookup SymbolTag block cl_env id ))) normalize nodelta
#Hlookup_eq
[ 2,4: #Heq destruct (Heq) whd in match (eval_expr ???????);
  [ 2: %{(Vptr (mk_pointer stackptr (shift_offset (bitsize_of_intsize I16) zero_offset (repr I16 n))))}
       @conj try @refl
       lapply (matching id)
       >Hlookup_eq normalize nodelta 
       >(opt_to_res_inversion ???? Heq_lookup) normalize nodelta
       #Hembed %4 whd in ⊢ (??%?); >Hembed @refl
  | 1: whd in match (eval_constant ????);
       lapply (matching id)
       >Hlookup_eq normalize nodelta  
       >(opt_to_res_inversion ???? Heq_lookup) normalize nodelta
       @False_ind
  ]
| 1,3: #Hfind_symbol
  cases (bind_inversion ????? Hfind_symbol) -Hfind_symbol #block *
  whd in ⊢ ((??%%) → ?); #Hfind_symbol
  lapply (opt_to_res_inversion ???? Hfind_symbol) #Hfind_symbol_eq
  whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
  whd in match (eval_expr ???????);
  whd in match (eval_constant ????);
  lapply (matching id)
  [ >Hlookup_eq normalize nodelta >Hfind_symbol_eq normalize nodelta
    #Hembed
    <(eq_sym … INV id) >Hfind_symbol_eq normalize nodelta
     %{(Vptr
         (mk_pointer cl_block
          (shift_offset (bitsize_of_intsize I16) zero_offset (repr I16 O))))}
     @conj try @refl
     %4 whd in ⊢ (??%?); >Hembed try @refl
  | (* A stack variable is not in the local environment but in the global one. *)
    (* we have a contradiction somewhere in the context *)
    lapply (variable_not_in_env_but_in_vartypes_is_global ??????? 
              cl_env_hyp alloc_hyp Hlookup_eq … Heq_lookup)
    *  #r #Habsurd destruct (Habsurd)
  ]
] qed.

(* lift simulation result to eval_exprlist *)

lemma eval_exprlist_simulation :
  ∀cl_f.
  ∀cl_ge : genv_t clight_fundef.
  ∀cm_ge : genv_t (fundef internal_function).
  ∀INV   : clight_cminor_inv cl_ge cm_ge.
  ∀alloc_type.  
  ∀cl_env, cl_m, cm_env, cm_m, stackptr.
  ∀Em.
  ∀stacksize     : ℕ.  
  ∀alloc_hyp     : characterise_vars (globals ?? INV) cl_f = 〈alloc_type, stacksize〉.
  ∀cl_env_hyp : ∃m,m'. exec_alloc_variables empty_env m (fn_params cl_f @ fn_vars cl_f) = 〈cl_env,m'〉.
  ∀injection     : memory_inj Em cl_m cm_m.
  ∀matching      : memory_matching Em cl_ge cm_ge cl_m cm_m cl_env cm_env INV stackptr alloc_type.
  ∀cl_exprs,cm_exprs.
  ∀cl_results,trace.
  exec_exprlist cl_ge cl_env cl_m cl_exprs = OK ? 〈cl_results, trace〉 →
  mmap_sigma ??? (translate_expr_sigma alloc_type) cl_exprs = OK ? cm_exprs →
  ∀H:All ? (λx:𝚺t:typ.expr t.
             match x with
             [ mk_DPair ty e ⇒ 
                    (expr_vars ty e
                     (λid:ident.λty:typ.present SymbolTag val cm_env id)) ]) cm_exprs.
  ∃cm_results.
  trace_map_inv … (λe. match e return λe.
                         match e with 
                         [ mk_DPair _ _ ⇒ ? ] → ? 
                       with
                       [ mk_DPair ty e ⇒ λp. eval_expr cm_ge ? e cm_env p stackptr cm_m ]) cm_exprs H = OK ? 〈trace, cm_results〉 ∧
  All2 ?? (λcl_val, cm_val. value_eq Em cl_val cm_val) cl_results cm_results.
#f #cl_ge #cm_ge #INV
#alloc_type #cl_env #cl_m #cm_env #cm_m #stackptr #Em #stacksize #alloc_hyp #cl_env_hyp #injection #matching
#cl_exprs
elim cl_exprs
[ #cm_exprs #cl_results #trace
  whd in ⊢ ((??%?) → ?);
  #Heq destruct (Heq)
  whd in ⊢ ((??%?) → ?);
  #Heq destruct (Heq) #H %{[]}
  @conj try @refl try @I
| #cl_hd #cl_tl #Hind #cm_exprs #cl_results #trace
  #Heq cases (bind_inversion ????? Heq) -Heq
  * #hd_val #hd_trace * #Hexec_expr_cl
  #Heq cases (bind_inversion ????? Heq) -Heq  
  * #cl_tl_vals #cl_tl_trace * #Hexec_expr_tl
  whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
  #Htranslate
  lapply (translate_exprlist_sigma_welltyped … Htranslate)
  #Htype_eq_all #Hall
  cases (bind_inversion ????? Htranslate) -Htranslate
  * * #cmtype #cmexpr normalize nodelta
  #Hexpr_vars_local_cm * #Htranslate_expr_sigma #Htranslate
  cases (bind_inversion ????? Htranslate) -Htranslate
  * #cm_tail #Hexpr_vars_local_cm_tail * #Htranslate_tail
  normalize nodelta
  whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
  cases Htype_eq_all -Htype_eq_all #Hcm_type_eq #Htype_eq_all
  lapply (Hind cm_tail cl_tl_vals cl_tl_trace Hexec_expr_tl)
  [ assumption ] -Hind #Hind
  lapply (Hind Htranslate_tail (proj2 ?? Hall)) -Hind
  * #cm_results_tl * #Hcm_exec_tl #Hvalues_eq_tl
  cases (eval_expr_sim cl_ge cm_ge INV f alloc_type stacksize alloc_hyp ?? cl_env_hyp ?? Em injection stackptr matching) 
  #Hsim #_
  cases (bind_inversion ????? Htranslate_expr_sigma)
  * #cmexpr' #Hexpr_vars_local_cm' * #Htranslate
  whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
  lapply (Hsim cl_hd cmexpr ??????) -Hsim try assumption
  [ @(proj1 ?? Hall) ]
  * #cm_val_hd * #Heval_expr_cm #Hvalue_eq      
  %{(cm_val_hd :: cm_results_tl)} @conj
  [ 2: @conj try assumption
  | 1: whd in ⊢ (??%?); normalize nodelta >Heval_expr_cm
       normalize nodelta >Hcm_exec_tl @refl
  ]
] qed.

(* --------------------------------------------------------------------------- *)
(* Putting the memory injection at work.                                       *)
(* --------------------------------------------------------------------------- *)

(* A) Non-interference of local variables with memory injections  *)

(* Needed property:
 * A local variable allocated via the temporary variable generator should not interfere
 * with the memory injection. In particular, we need to show that:
 * 1) we can successfuly store stuff of the right type inside (where the type is specified
 *    at generation time, and should be in the current context)
 * 2) after the store, we can build a consistent memory state and more generally, a
 *    correct [clight_cminor_data] invariant record. Cf. toCminorCorrectnessExpr.ma
 *)
 
(* A.1) memory matchings survives memory injection *)

lemma offset_plus_0' : ∀o:offset. offset_plus zero_offset o = o.
#o cases o #b >offset_plus_0 @refl
qed.

(*
lemma store_value_of_type_memory_matching_to_matching :  
  ∀cl_ge, cm_ge, cl_en, cm_en, INV, sp, vars, cl_m, cl_m',cm_m,cm_m'.
  ∀E: embedding.
  ∀blo, blo', delta, off.
  E blo = Some ? 〈blo', delta〉 →
  ∀cl_val, cm_val, ty.
  value_eq E cl_val cm_val →
  storen cl_m (mk_pointer blo off) (fe_to_be_values ty cl_val) = Some ? cl_m' →
  storen cm_m (mk_pointer blo (offset_plus off delta)) (fe_to_be_values ty cm_val) = Some ? cm_m' →
  (lookup' vars var_id = OK (var_type×type) 〈Global r,type_of_var〉)
  memory_inj E cl_m' cm_m' →
  memory_matching E cl_ge cm_ge cl_m cm_m cl_en cm_en INV sp vars →
  memory_matching E cl_ge cm_ge cl_m' cm_m' cl_en cm_en INV sp vars.
#cl_ge #cm_ge #cl_en #cm_en #INV #sp #vars #cl_m #cl_m' #cm_m #cm_m' #E
#blo #blo' #delta #off #Hembed #cl_val #cm_val #ty #Hvalue_eq #Hstoren_cl #Hstoren_cm
#Hinj #Hmatching #id
lapply (Hmatching id)
cases (lookup ?? cl_en id) normalize nodelta
[ 1: #H @H
| 2: #bl cases (lookup ?? vars id) normalize nodelta
  [ 1: #H @H
  | 2: * #var_type #cl_type normalize nodelta
       cases var_type normalize nodelta
       [ #r #H @H
       | #b #H @H
       | #H #v lapply H -H
         @(eq_block_elim … bl blo)
         [ #Heq destruct (Heq)
           @(eq_offset_elim … off zero_offset)
           [ (* We actually load exactly where we wrote, but with a potentially different type. *)
             #Heq destruct (Heq) #H 
       ]
  ]
] qed.*)


lemma alloc_tmp_in_genlist :
  ∀vartypes. ∀g1, g2, g3.
  ∀id1, ty1, id2, ty2.
  alloc_tmp vartypes ty1 g1 = 〈id1, g2〉 →
  alloc_tmp vartypes ty2 g2 = 〈id2, g3〉 →
  Exists (identifier SymbolTag×type)
   (λx:identifier SymbolTag×type.x=〈id2,ty2〉) (tmp_env ? g3).
#vartypes #g1 #g2 #g3
#id1 #ty1 #id2 #ty2 #Halloc1 #Halloc2
lapply (breakup_dependent_match_on_pairs ?????? Halloc1) * #id1' * #u' * #Hfg1
* #Hfresh_eq generalize in match (fresh_map_add ????????); #ugly
generalize in ⊢ ((??(????(?????%))?) → ?); #ugly2
#Heq destruct (Heq)
lapply (breakup_dependent_match_on_pairs ?????? Halloc2) * #id2' * #u'' * #Hfg2
* #Hfresh_eq' generalize in match (fresh_map_add ????????); #ugly'
generalize in ⊢ ((??(????(?????%))?) → ?); #ugly2'
#Heq destruct (Heq) %1 @refl
qed. (* this last lemma has to be refitted. *)

lemma store_value_of_type_success_by_value :
   ∀ty, m, m', b, o, v.
   store_value_of_type ty m b o v = Some ? m' →
   access_mode ty = By_value (typ_of_type ty) ∧
   storev (typ_of_type ty) m (Vptr (mk_pointer b o)) v = Some ? m'.   
#ty #m #m' #b #o #v
cases ty
[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
| #structname #fieldspec | #unionname #fieldspec | #id ]
whd in ⊢ ((??%?) → ?);
[ 1,4,5,6,7: #Habsurd destruct (Habsurd) ]
#H @conj try @refl @H
qed.

(* Some boilerplate to avoid performing a case analysis on exprs in the middle of
 * the proof. *)
lemma translate_dest_not_Evar_id :
  ∀vars, ed, ty.
  (∀id. ed ≠ Evar id) →
    translate_dest vars (Expr ed ty) =
    (do e1' ← translate_addr vars (Expr ed ty);
     OK ? (MemDest … e1')).
#vars *
[ #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 ]
#ty #H
[ 2: @False_ind @(absurd … (refl ??) (H ?)) ]
@refl
qed.

lemma expr_is_Evar_id_dec :
  ∀ed. (∀id. ed ≠ Evar id) ∨ (∃id. ed = Evar id).
*  
[ #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: %2 %{id} @refl
| *: %1 #id % #Habsurd destruct (Habsurd) ]
qed.

lemma mk_offset_offv_id : ∀o. mk_offset (offv o) = o.
* #x @refl qed.

lemma find_funct_to_find_funct_id :
   ∀F, ge, ptr, fundef.
   ∀H:find_funct ? ge ptr = Some ? fundef.
   find_funct_id F ge ptr = Some ? 〈fundef, symbol_of_function_val' F ge ptr fundef H〉.
#F #ge #ptr #fundef #Hfind whd in match (find_funct_id ???);
generalize in ⊢ (??(?%)?);
generalize in ⊢ 
 ((???%) → (??
    (match %
(*     return λ_. (??%?) → ?*)
     with
     [ _ ⇒ λ_. ?
     | _ ⇒ λ_.λ_. ? ] ?)
  ?));
#o cases o normalize nodelta
[ #H @False_ind >Hfind in H; #Habsurd destruct (Habsurd)
| #f #Hfind'  
  cut (f = fundef)
  [ >Hfind in Hfind'; #Heq destruct (Heq) @refl ]
  #Heq destruct (Heq)
  @refl
] qed.

lemma eval_bool_of_val_to_Cminor :
  ∀E. ∀ty. ∀v1,v2. ∀b.
    value_eq E v1 v2 →
    exec_bool_of_val v1 ty = return b →
    eval_bool_of_val v2 = return  b.
#E #ty #v1 #v2 #b #Hvalue_eq
whd in ⊢ ((??%%) → (??%%));
@(value_eq_inversion … Hvalue_eq) normalize nodelta
[ #Habsurd destruct (Habsurd) ]
[ #vsz #vi cases ty
  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
  | #structname #fieldspec | #unionname #fieldspec | #id ] normalize nodelta
  [ 2: | *: #Habsurd destruct (Habsurd) ]
  @(intsize_eq_elim_elim … vsz sz)
  [ 1: #H #Habsurd destruct (Habsurd)
  | 2: #Heq destruct (Heq) normalize nodelta #H @H ]
| cases ty
  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
  | #structname #fieldspec | #unionname #fieldspec | #id ] normalize nodelta
  #H destruct (H) @refl
| #p1 #p2 #Htranslate
  cases ty
  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
  | #structname #fieldspec | #unionname #fieldspec | #id ] normalize nodelta
  #H destruct (H) @refl
] qed.

lemma let_prod_as_inversion : 
    ∀A,B,C: Type[0].
    ∀expr: A × B.
    ∀body: ∀a:A. ∀b:B. 〈a,b〉 = expr → res C.
    ∀result: C.
    (let 〈a,b〉 as E ≝ expr in body a b E) = return result →
    ∃x,y. ∃E. 〈x,y〉 = expr ∧
          body x y E = return result.
#A #B #C * #a #b #body #res normalize nodelta #Heq
%{a} %{b} %{(refl ??)} @conj try @refl @Heq
qed.

(* move this to frontend_misc *)
lemma lset_inclusion_Exists : ∀A, l1, l2, P.
  Exists A P l1 → lset_inclusion A l1 l2 → Exists A P l2.
#A #l1 #l2 #P #Hexists whd in ⊢ (% → ?);
lapply Hexists
generalize in match l2;
elim l1
[ #l2 @False_ind
| #hd #tl #Hind #l2 *
  [ 2: #HA * #Hhd #Htl @Hind try assumption
  | 1: #H * #Hmem #_ elim l2 in Hmem;
       [ @False_ind
       | #hd2 #tl2 #Hind *
         [ #Heq destruct (Heq) %1 @H
         | #Hneq %2 @Hind @Hneq ]
       ]
  ]
] qed.

axiom load_value_after_free_list_inversion :
  ∀ty, m, blocks, b, o, v.
  load_value_of_type ty (free_list m blocks) b o = Some ? v →  
  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 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.

(* TODO: move *)
lemma extract_pair' : ∀A,B,C.  ∀u:A×B. ∀Q:A → B → C. ∀x.
((let 〈a,b〉 ≝ u in Q a b) = x) →
∃a,b. 〈a,b〉 = u ∧ Q a b = x.
#A #B #C * #a #b #Q #x normalize #E1 %{a} %{b} % try @refl @E1 qed.

lemma pair_as_elim:
  ∀A,B,C: Type[0].
  ∀p.
  ∀T: ∀a:A. ∀b:B. 〈a,b〉 = p → C.
  ∀P: A×B → C → Prop.
    (∀lft, rgt. ∀E:〈lft,rgt〉 = p. P 〈lft,rgt〉 (T lft rgt E)) →
      P p (let 〈lft, rgt〉 as E ≝ p in T lft rgt E).
#A #B #C * /2/
qed.

(* TODO: move *)
lemma alloc_low_bound : ∀m,l,h,m',b.
  alloc m l h = 〈m',b〉 →
  low_bound m' b = l.
* #contents #next #next_ok #l #h #m' #b #E
whd in E:(??%%); destruct
whd in ⊢ (??%?); >update_block_s
%
qed.

lemma alloc_high_bound : ∀m,l,h,m',b.
  alloc m l h = 〈m',b〉 →
  high_bound m' b = h.
* #contents #next #next_ok #l #h #m' #b #E
whd in E:(??%%); destruct
whd in ⊢ (??%?); >update_block_s
%
qed.

(* Weaker version of Zlt_to_Zle *)
lemma Zlt_Zle : ∀x,y:Z. x < y → x ≤ y.
#x #y #H
@(transitive_Zle … (Zsucc_le x)) @Zlt_to_Zle @H
qed.

axiom unZoo : ∀off:Z.
  off < Z_two_power_nat 16 →
  Zoo (offset_of_Z off) = off.

lemma le_to_Zle : ∀x,y:nat. le x y → Zle x y.
#x #y #H @(le_ind ????? H)
[ //
| #m #H1 #H2 >Zsucc_pos @(transitive_Zle … (Zsucc_le m)) assumption
] qed.

lemma lt_to_Zlt : ∀x,y:nat. lt x y → Zlt x y.
#x #y whd in ⊢ (% → ?); #H
<(Zpred_Zsucc x) @Zle_to_Zlt
<Zsucc_pos
@le_to_Zle assumption
qed.

lemma Zlt_Zsucc : ∀z:Z. z < Zsucc z.
/2/
qed.

lemma Zle_Zlt_Zsucc : ∀x,y:Z. x ≤ y → x < Zsucc y.
/2/
qed.

theorem Zle_to_Zlt_to_Zlt: ∀n,m,p:Z. n ≤ m → m < p → n < p.
#n #m #p #Hle #Hlt lapply (Zlt_to_Zle … Hlt)
@Zlt_to_Zle_to_Zlt @Zle_Zlt_Zsucc assumption
qed.


(* This roughly corresponds to lemma 69 of Leroy and Blazy *)
(*
lemma alloc_vars_rel : ∀vartypes, cl_m, cm_m, stacksize, cm_m1, cm_frame.
∀Em. memory_inj Em cl_m cm_m →
Z_of_nat stacksize < Z_two_power_nat 16 →
alloc cm_m O (Z_of_nat stacksize) = 〈cm_m1,cm_frame〉 →
∀L, cl_env, cl_m1.
exec_alloc_variables empty_env cl_m L = 〈cl_env,cl_m1〉 →
(∀v,ty. Exists … (λx.x = 〈v,ty〉) L → ∃c. lookup' vartypes v = return 〈c,ty〉 ∧
  match c with
  [ Local ⇒ True
  | Stack off ⇒ 
    le O off ∧ le (sizeof ty + off) stacksize ∧
    (∀v',off',t'. v≠v' → lookup' vartypes v' = return 〈Stack off',t'〉 → le (off' + sizeof t') off ∨ le (off + sizeof ty) off')
  | Global _ ⇒ False
  ]) →
∃Em'. memory_inj Em' cl_m1 cm_m1 ∧
  embedding_compatible Em Em' ∧
  ∀v. Exists … (λx.\fst x = v) L →
  ∃b,c,t. lookup … cl_env v = Some ? b ∧
    lookup' vartypes v = return 〈c,t〉 ∧
    match c with
    [ Local ⇒ Em' b = None ?
    | Stack off ⇒ Em' b = Some ? 〈cm_frame, offset_of_Z (Z_of_nat off)〉
    | Global _ ⇒ False
    ].
#vartypes #cl_m #cm_m #stacksize #cm_m1 #cm_frame #Em #Inj #stack_ok #cm_alloc #L
cut (block_implementable_bv cm_m1 cm_frame)
[ whd >(alloc_low_bound … cm_alloc) >(alloc_high_bound … cm_alloc) % % //
  cases stacksize // ] #cm_bi
lapply (alloc_memory_inj_m2 … Inj cm_alloc cm_bi)
lapply (alloc_valid_new_block … cm_alloc) #cm_frame_valid
cut (∀b:block. ∀delta':offset.
    Em b=Some (block×offset) 〈cm_frame,delta'〉 → 
    ∀v,off,ty. lookup' vartypes v = OK ? 〈Stack off, ty〉 →
    high_bound cl_m b+Zoo delta'≤O+Zoo (offset_of_Z off)
      ∨ sizeof ty+Zoo (offset_of_Z off)≤low_bound cl_m b+Zoo delta')
[ #b #delta' #E @⊥ lapply (mi_nodangling … Inj … E) #V
  @(absurd … V) @(new_block_invalid_before_alloc … cm_alloc) ]

generalize in match Em; -Em generalize in match empty_env; elim L
[ #cl_env #Em #_ #Inj #cl_env' #cl_m1 #cl_alloc
  whd in cl_alloc:(??%%); destruct #H
  %{Em} % [ % [ @Inj | // ] | #v * ]
| * #v #ty #tl #IH
  #cl_env #Em #Hexisting #Inj #cl_env' #cl_m1
  whd in ⊢ (??%? → ?); @pair_elim #cl_m2 #cl_b #cl_alloc #cl_alloc' #H
  cases (H v ty ?) [2: %1 % ] *
  [ #r * #L *
  | #off * #L * * #off_low #off_high #other
    lapply (alloc_memory_inj_m1_to_m2 … (offset_of_Z off) cm_frame_valid … cm_bi … cl_alloc … Inj)
    [ #b #delta' #NE #E @(Hexisting … E … L)
    | cases (alloc_properties … cm_alloc) #_ #U #i #LOW #HIGH @U
      [ /2/
      | @(transitive_Zle … HIGH) >unZoo
        [ <eq_plus_Zplus /2/
        | @(Zlt_to_Zle_to_Zlt ? (sizeof ty + off))
          [ <eq_plus_Zplus @lt_to_Zlt whd in ⊢ (??%); /2/
          | @(transitive_Zlt … stacksize) [ <eq_plus_Zplus @(lt_to_Zlt … off_high) | // ]
          ]
        ]
      ]
    | >unZoo
        [ <eq_plus_Zplus >(alloc_high_bound … cm_alloc) 
*)
(*
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

   We split these based on the start state:
   
   1. ‘normal’ states take some [S n] normal steps and simulates them by [S m]
      normal steps in Cminor;
   2. call and return steps are simulated by a call/return step plus [m] normal
      steps (to copy stack allocated parameters / results); and
   3. lone cost label steps are simulated by a lone cost label step
   
   These should allow us to maintain enough structure to identify the Cminor
   subtrace corresponding to a measurable Clight subtrace.
 *)
(* WIP 
include "common/ExtraMonads.ma".

lemma clight_cminor_call :
    ∀g,g'.
    ∀INV:clight_cminor_inv g g'.
    ∀s1,s1'.
    clight_cminor_rel g g' INV s1 s1' →
    Clight_classify s1 = cl_call →
    ∀s2,tr2,s3,tr3.
    step … (pcs_exec cl_pre) g s1 = Value … 〈tr2,s2〉 →    
    step … (pcs_exec cl_pre) g s2 = Value … 〈tr3,s3〉 →    
    Clight_labelled s2 →
    after_n_steps 1 ?? (pcs_exec cm_pre) g' s1' (λs.cminor_normal s) (λtr2',s2'.
      tr2 = tr2' ∧
      bool_to_Prop (Cminor_labelled s2') ∧
      ∃m.
      after_n_steps m ?? (pcs_exec cm_pre) g' s2' (λs.cminor_normal s) (λtr3',s3'.
        tr3 = tr3' ∧
        clight_cminor_rel g g' INV s2 s2')
    ).
#Xg #Xg' #XINV #Xs1 #Xs1' *
[ #g #g' #INV #cl_s #cm_s #cl_k #cm_k #cm_st #cl_f #cm_f #rettyp #alloc_type #cl_env #cl_m #cm_env #cm_m #stackptr #stacksize #fInv #sInv #kInv #Erettyp #func_univ #Hfresh_globals #Hfresh_function #Htranslate_fn #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls #flag #Htranslate_inv #Htranslate_s #Hlbls_inc #tmpenv #Htmpenv #CONT #Em #HtmpEm #CHAR #ALLOC #INJ #MATCH #HEm_fn #HEm_env #Henv_below
  #CL whd in CL:(??%?); destruct
| #g #g' #INV #cl_k #cm_k #cm_st #cl_f #cm_f #alloc_type #cl_env #cl_m #cm_env #cm_m #stackptr #stacksize #stmt_univ #tmpenv #Htmpenv #Em #HEm_tmp #CHAR #ALLOC #INJ #MATCH #HEm_fn #HEm_env #CONT
  #CL whd in CL:(??%?); destruct
| #g #g' #INV #cl_k #cm_st #cl_fd #cm_fd #fblock #target_type #cl_env #cl_m #cm_env #cm_m #fid #Hfind_cl #Hfind_cm #tmpenv #CONT #Em #INJ #HEm_fn #cl_args #cm_args #Hargs
  #CL #s2 #tr2 #s3 #tr3 #STEP1 #STEP2 #CS2
  
  (* Note that cm_fd is the translation of cl_fd *)
  cases (trans_fn … INV … Hfind_cl)
  #func_univ * #cm_fd' * #Hglobals_fresh * #Hfundef_fresh * #Htranslate
  >Hfind_cm #E destruct
  
  (* Must be a CL_Internal function *)
  cases cl_fd in Hfundef_fresh Htranslate Hfind_cl CONT STEP1;
  [ #cl_f
  | #ext #ext_argtys #ext_retty
  ]
  #Hfundef_fresh #Htranslate #Hfind_cl #CONT #STEP1
  [2: cases (bindIO_inversion ??????? STEP1) -STEP1 #vs * #_ #STEP1
      whd in STEP1:(??%%); destruct ]
  -cl_fd
  (* and the Cminor one must be Internal *)
  @('bind_inversion Htranslate) #cm_f #Htranslate' #E
  whd in E:(??%%); destruct

  (* Invert function translation *)
  (* NB: if you want to examine the proof state in here, you probably want to
     turn off the pretty printer - it doesn't cope well with a large proof
     term. *)
  @('bind_inversion Htranslate') * * #lbls #Ilbls #ul #Hbuild_label_env
  whd in ⊢ (??%? → ?);
  @pair_as_elim #vartypes #stacksize #Hcharacterise
  letin uv ≝ (mk_tmpgen ?? [ ] ??) #H
  @('bind_inversion H) -H #s0 #Htranslate_statement #H
  @('bind_inversion H) -H * * #fgens #s1 #Is #Halloc_params
  letin cm_params ≝ (map ??? (fn_params cl_f))
  whd in ⊢ (??%? → ?);
  letin cm_vars ≝ (map ??? (?@fn_vars cl_f)) #H
  @('bind_inversion H) -H #D #Hcheck_distinct_env
  whd in ⊢ (??%% → ?); generalize in ⊢ (??(??(???????%))? → ?);
  (* It's safe to use the pretty printer again. *)
  #cm_Sinv #H destruct

  (* Invert Clight STEP1 *)  
  cases (extract_pair' ?????? STEP1) -STEP1 #cl_env * #cl_m1 * #ALLOC #STEP1
  cases (bindIO_inversion ??????? STEP1) -STEP1 #cl_m2 * #BIND #STEP1
  whd in STEP1:(??%%); destruct

  whd whd in ⊢ (??%?);
  @pair_elim #cm_m1 #cm_frame #CM_ALLOC

 (〈vartypes,stacksize〉=characterise_vars (globals g g' INV) cl_f)
We need to build an extended memory injection to reflect the new allocations;
then the bind functions put the correct local variables in;
then after execution the appropriate number of Cminor steps the stored values
match.

Oh, and there are the locals too.


alloc_memory_inj_m2 shows that embedding is fine after the Cminor alloc

∀Em. memory_inj Em cl_m cm_m →
(∀b. block_region b = Code → Em' b = Some ? 〈b,zero_offset〉) →
exec_alloc_variables empty_env cl_m (fn_params cl_f@fn_vars cl_f) = 〈cl_env,cl_m1〉 →
alloc cm_m O (f_stacksize cm_f) = 〈cm_m1,cm_frame〉 →
∃Em'.
  memory_inj Em' cl_m1 cm_m1 ∧
  (∀b. block_region b = Code → Em' b = Some ? 〈b,zero_offset〉) ∧
  (∀v,v'. value_eq Em v v' → value_eq Em' v v') ∧
  (∀b1.∀delta. Em' b1=Some ? 〈cm_frame,delta〉 →
             mem block b1 (blocks_of_env cl_env)).
             
  ∀b. Em b = Em' b ∨ (Em b = None ? ∧ ∃off. Em' b = Some ? 〈cm_frame,off〉).


translate_function func_univ (globals … INV) cl_f H1 H2 = return cm_f →
All2 … (λcl,cm.value_eq Em cl cm) cl_args cm_args →
exec_bind_parameters cl_env cl_m1 (fn_params cl_f) cl_args = return cl_m2 →
∃cm_en,Hcm_args_present.
  bind_params cm_args (f_params cm_f) = return «cm_en, Hcm_args_present» ∧
  

*)

(*
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 :
    ∀g1,g2.
    ∀INV:clight_cminor_inv g1 g2.
    ∀s1,s1'.
    clight_cminor_rel g1 g2 INV s1 s1' →
    clight_normal s1 →
    ¬ pcs_labelled cl_pre g1 s1 →
    ∀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))
    ).
#Xg1 #Xg2 #XINV #Xs1 #Xs1' *
[ 1: (* Normal state *)
     (* ---------------------------------------------------------------------- *)
#cl_ge #cm_ge #INV' #cl_s
(* case analysis on Clight statement *)
cases cl_s
[ 1: | 2: #lhs #rhs | 3: #retv #func #args | 4: #stm1 #stm2 | 5: #cond #iftrue #iffalse | 6: #cond #body
| 7: #cond #body | 8: #init #cond #step #body | 9,10: | 11: #retval | 12: #cond #switchcases | 13: #lab #body
| 14: #lab | 15: #cost #body ]
(*
[ 11: (* Return case *)
     #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 #Htranslate #Hlabel_inclusion #Hcont_rel
     #Em #Htmp_vars_well_allocated #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id
     @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
     destruct (HA HB)
     @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE #_
     destruct (HC HD HE)
     whd in Htranslate:(??%?);
     cases retval in Htranslate; normalize nodelta
     [ cases rettyp in Htrans_inv Hcont_rel;
       [ 2: #opttyp normalize nodelta #Htrans_inv #_
            #Habsurd destruct (Habsurd)
       | 1: #Htrans_inv #Hcont_rel normalize nodelta #Heq destruct (Heq)
            #s2 #tr whd in ⊢ ((??%?) → ?);
            cases (fn_return cl_f)
            [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
            | #structname #fieldspec | #unionname #fieldspec | #id ]
            normalize nodelta
            [ 1:
            | *: #Habsurd destruct (Habsurd) ]
            whd in ⊢ ((??%?) → ?);
            #Heq destruct (Heq)
            %{1} whd @conj try @conj
            [ 3: #Habsurd destruct (Habsurd)
            | 1: @refl ]
            @CMR_return
*)     
[ 6: (* While *)
     #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 * * * * #Hstmt_inv_cm cases cond #cond_desc #cond_ty
     (* early case analysis to avoid dependency hell *)
     cases cond_ty
     [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
     | #structname #fieldspec | #unionname #fieldspec | #id ]     
     #Hlabels_translated #Htmps_preserved
     #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 #Henv_below #Hclight_normal #Hnot_labeleld
     lapply Htranslate -Htranslate
     [ 1: generalize in match (conj ????); #Hugly_inv
     | 2: generalize in match (conj ????); #Hugly_inv
     | 3: generalize in match (conj ????); #Hugly_inv
     | 4: generalize in match (conj ????); #Hugly_inv
     | 5: generalize in match (conj ????); #Hugly_inv
     | 6: generalize in match (conj ????); #Hugly_inv
     | 7: generalize in match (conj ????); #Hugly_inv
     | 8: generalize in match (conj ????); #Hugly_inv ]
     #Htranslate
     cases (bind_inversion ????? Htranslate) -Htranslate
     whd in match (typeof ?); whd in match (typ_of_type ?); *
     #cm_cond #Hexpr_vars_cond * #Htranslate_cond normalize nodelta
     [ 3,4,5,8: whd in ⊢ ((??%%) → ?); #Habsurd destruct (Habsurd) ]
     #Htranslate normalize nodelta
     lapply (let_prod_as_inversion ?????? Htranslate) -Htranslate
     * * #entry_label #exit_label * #lbl_univ0 * #Hmk_label_eq *
     #Hmk_label_eq_bis normalize nodelta #Htranslate
     cases (bind_inversion ????? Htranslate) -Htranslate
     * * * #stmt_univ0 #lbl_univ1 #cm_body
     #Htrans_inv * #Htrans_body normalize nodelta
     [ generalize in ⊢ ((??(??(????%))?) → ?);
       #Htrans_inv'
     | generalize in ⊢ ((??(??(????%))?) → ?);
       #Htrans_inv'
     | generalize in ⊢ ((??(??(????%))?) → ?);
       #Htrans_inv'
     | generalize in ⊢ ((??(??(????%))?) → ?);
       #Htrans_inv' ]
     whd in ⊢ ((???%) → ?);
     #Heq destruct (Heq)
     #s2 #tr whd in ⊢ ((??%?) → ?); 
     #Hstep
     cases (bindIO_inversion ??????? Hstep) -Hstep * #cond_val #cond_trace
     * #Hcl_exec_cond #Hstep
     cases (bindIO_inversion ??????? Hstep) -Hstep
     #cl_cond_bool * #Hcl_bool_of_val whd in ⊢ ((??%%) → ?);
     cases cl_cond_bool in Hcl_bool_of_val;
     [ 1,3,5,7: (* cond = true: continue looping *)
       #Hcl_bool_of_val normalize nodelta
       #Heq destruct (Heq)
       %{4} whd whd in ⊢ (??%?); normalize nodelta
       [ generalize in match (proj1 ???); #Hpresent_ifthenelse
       | generalize in match (proj1 ???); #Hpresent_ifthenelse
       | generalize in match (proj1 ???); #Hpresent_ifthenelse
       | generalize in match (proj1 ???); #Hpresent_ifthenelse ]
       (* Exhibit simulation of condition evaluation *)
       lapply (eval_expr_sim … Halloc_hyp … Hcl_env_hyp … Hinjection … Hmatching) * #Hsim #_
       [ lapply (Hsim (Expr cond_desc Tvoid) … Htranslate_cond ?? Hpresent_ifthenelse Hcl_exec_cond)
       | lapply (Hsim (Expr cond_desc (Tint sz sg)) … Htranslate_cond ?? Hpresent_ifthenelse Hcl_exec_cond)
       | lapply (Hsim (Expr cond_desc (Tstruct structname fieldspec)) … Htranslate_cond ?? Hpresent_ifthenelse Hcl_exec_cond)
       | lapply (Hsim (Expr cond_desc (Tunion unionname fieldspec)) … Htranslate_cond ?? Hpresent_ifthenelse Hcl_exec_cond) ]
       * #cm_val_cond * #Hcm_eval_cond #Hvalue_eq >Hcm_eval_cond
       whd in match (m_bind ?????);
       >(eval_bool_of_val_to_Cminor … Hvalue_eq … Hcl_bool_of_val)
       normalize nodelta whd
       [ generalize in match (proj1 ???); #Hnoise'
         generalize in match (conj ????); #Hnoise'' 
       | generalize in match (proj1 ???); #Hnoise'
         generalize in match (conj ????); #Hnoise''
       | generalize in match (proj1 ???); #Hnoise'
         generalize in match (conj ????); #Hnoise'' 
       | generalize in match (proj1 ???); #Hnoise'
         generalize in match (conj ????); #Hnoise'' ]
       @conj try @conj
       [ 3,6,9,12: #Habsurd destruct (Habsurd)
       | 1,4,7,10: normalize >append_nil @refl
       | 2,5,8,11:
            cut (lset_inclusion (identifier Label) (labels_of cm_body) (labels_of (f_body cm_f)))
            [ 1,3,5,7:
              lapply Hlabel_inclusion
              @transitive_lset_inclusion
              @cons_preserves_inclusion
              @lset_inclusion_union %1
              @lset_inclusion_union %1
              @lset_inclusion_union %1
              @reflexive_lset_inclusion ]
            #Hlabels_of_body
            cut (Exists (identifier Label) (λl'.l'=entry_label) (labels_of (f_body cm_f)))
            [ 1,3,5,7: @(lset_inclusion_Exists ????? Hlabel_inclusion)
              %1 @refl ]
            #Hentry_exists
            cut (Exists (identifier Label) (λl'.l'=exit_label) (labels_of (f_body cm_f)))
            [ 1,3,5,7: @(lset_inclusion_Exists ????? Hlabel_inclusion)
              %2 @Exists_append_r %1 @refl ]
            #Hexit_exists
            @(CMR_normal … Htrans_body) try assumption
            @(ClCm_cont_while … (sym_eq … Hmk_label_eq) … Htrans_body) try assumption
            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
            | *: (* find_label_always *)
                 (* TODO /!\ implement necessary invariant on label lookup *)
                 @cthulhu
            ]
       ]
     | 2,4,6,8: (* cond = false: stop looping *)
       #Hcl_bool_of_val normalize nodelta #Heq destruct (Heq)
       %{5} whd whd in ⊢ (??%?); normalize nodelta
       [ generalize in match (proj1 ???); #Hpresent_ifthenelse
       | generalize in match (proj1 ???); #Hpresent_ifthenelse
       | generalize in match (proj1 ???); #Hpresent_ifthenelse
       | generalize in match (proj1 ???); #Hpresent_ifthenelse ]
       (* Exhibit simulation of condition evaluation *)
       lapply (eval_expr_sim … Halloc_hyp … Hcl_env_hyp … Hinjection … Hmatching) * #Hsim #_
       [ lapply (Hsim (Expr cond_desc Tvoid) … Htranslate_cond ?? Hpresent_ifthenelse Hcl_exec_cond)
       | lapply (Hsim (Expr cond_desc (Tint sz sg)) … Htranslate_cond ?? Hpresent_ifthenelse Hcl_exec_cond)
       | lapply (Hsim (Expr cond_desc (Tstruct structname fieldspec)) … Htranslate_cond ?? Hpresent_ifthenelse Hcl_exec_cond)
       | lapply (Hsim (Expr cond_desc (Tunion unionname fieldspec)) … Htranslate_cond ?? Hpresent_ifthenelse Hcl_exec_cond) ]       
       * #cm_val_cond * #Hcm_eval_cond #Hvalue_eq >Hcm_eval_cond
       whd in match (m_bind ?????);
       >(eval_bool_of_val_to_Cminor … Hvalue_eq … Hcl_bool_of_val) normalize nodelta whd
       [ generalize in match (proj2 ???); #Hnoise'
         generalize in match (proj2 ???); #Hnoise''
       | generalize in match (proj2 ???); #Hnoise'
         generalize in match (proj2 ???); #Hnoise''
       | generalize in match (proj2 ???); #Hnoise'
         generalize in match (proj2 ???); #Hnoise''
       | generalize in match (proj2 ???); #Hnoise'
         generalize in match (proj2 ???); #Hnoise'' ]
       @conj try @conj try @conj
       [ 1,4,7,10: normalize >append_nil >append_nil @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) ]
   ]
| 3: (* Call *)
     #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 * * * * #Hstmt_inv #Hlabels_translated #Htmps_preserved #Hreturn_ok #Hlabel_wf
     (* generalize away ugly proof *)
     generalize in ⊢ (∀_:(???(??(????%))).?); #Hugly
     #Htranslate #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 #Hclight_normal #Hnot_labeleld
     (* back to unfolding Clight execution *)
     cases (bind_inversion ????? Htranslate) -Htranslate *
     #ef #Hexpr_vars_ef * #Htranslate_ef normalize nodelta #Htranslate
     cases (bind_inversion ????? Htranslate) -Htranslate *
     #ef' #Hexpr_vars_local_ef' * #Htyp_should_eq_ef
     cases (typ_should_eq_inversion (typ_of_type (typeof func)) ASTptr … Htyp_should_eq_ef)
     -Htyp_should_eq_ef #Htyp_equality_ef
     #Heq_ef_ef' #Htranslate
     cases (bind_inversion ????? Htranslate) -Htranslate *
     #cm_args #Hall_variables_from_args_local *
     whd in ⊢ ((???%) → ?); #Hargs_spec
     @(match retv
       return λx. retv = x → ?
       with
       [ None ⇒ λHretv. ?
       | Some lhs ⇒ λHretv. ?
       ] (refl ? retv))
     normalize nodelta
     [ 2: (* return something *)
       #Hdest cases (bind_inversion ????? Hdest) -Hdest #dest *
       inversion dest normalize nodelta
       [ (* register dest *) #var_id #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 *)
         lapply (translate_dest_id_inversion  … Htranslate_dest) #Hlhs_eq
       | * #cm_expr #Hexpr_vars_cm #Hdest #Htranslate_dest #Hgensym
         lapply (breakup_dependent_match_on_pairs ?????? Hgensym) -Hgensym
         * #ret_var * #new_gensym * #Heq_alloc_tmp * #_ #Hgensym
         lapply (breakup_dependent_match_on_pairs ?????? Hgensym) -Hgensym
         * #tmp_var * #new_gensym' * #Heq_alloc_tmp' * #_
         generalize in ⊢ ((??(?? (????%) )?) → ?); #Hstmt_inv_after_gensym
         whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
       ]
     | 1: (* return void *)
          generalize in ⊢ ((??(??(????%))?) → ?); #Hugly2
          whd in ⊢ ((???%) → ?); #Heq destruct (Heq) ]
     (* Now, execute the Clight call *)
     #s2 #tr #Htranslate
     cases (bindIO_inversion ??????? Htranslate) -Htranslate *
     #CL_callee_val #CL_callee_trace * #Hexec_CL_callee normalize nodelta
     whd in ⊢ ((???%) → ?); #Htranslate
     cases (bindIO_inversion ??????? Htranslate) -Htranslate *
     #CL_args #CL_args_trace * #Hexec_CL_args #Htranslate
     cases (bindIO_inversion ??????? Htranslate) -Htranslate
     * #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)
     #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: (* 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
                | #H cases (bind_inversion ????? H) #H24 * #H27 #H28
                  whd in H28:(???%); destruct (H28) @refl ]
              ] #H destruct (H)
            | #HCL_exec_lvalue ]
     | 3: ]
     whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
     (* 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
          (* Apply simulation lemma for lvalues *)
          lapply (translate_dest_MemDest_simulation … Htranslate_dest HCL_exec_lvalue)
          try assumption try @refl
          * #CM_lvalue * #HCM_eval_lvalue >HCM_eval_lvalue #Hvalue_eq_lvalues
          normalize nodelta generalize in match (proj1 ???); #Htmp_var_present
          (* 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
     | 3: %{1} whd whd in ⊢ (??%?); normalize nodelta
     ]
    (* cleanup ugliness *)
    [ 1: generalize in match (proj2 (present ????) (expr_vars ???) (proj1 ???));
    | 2: generalize in match (proj2 (present ????) (expr_vars ???) (proj1 ???));
    | 3: generalize in match (proj2 True ??); ]
    #Hexpr_vars_present_ef'
    [ 1,3:
       cases (eval_expr_sim … INV' … Halloc_hyp … Hcl_env_hyp … Hinjection … Hmatching) #Hsim_expr #_
       cut (expr_vars (typ_of_type (typeof func)) ef
             (λid:ident.λty:typ.present SymbolTag val cm_env id))
       [ 1,3: lapply Heq_ef_ef' lapply Hexpr_vars_ef lapply ef >Htyp_equality_ef
                #ef #Hexpr_vars_ef @(jmeq_absorb ?????) #Heq destruct (Heq)
                @Hexpr_vars_present_ef' ]
       #Hexpr_vars_present_ef
       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) 〈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'
         lapply Hexpr_vars_present_ef lapply ef lapply Hexpr_vars_present_ef' lapply ef'
         <Htyp_equality_ef #ef' #HA #ef #HB #HC #HD #HE
         @(jmeq_absorb ?????) #Heq destruct (Heq) @HE ]
       -Heval_func #Heval_func >Heval_func
    | 2: (* treat case 2 as special, since the type differs slightly *)
       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 (proj1 ???); #Hret_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 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_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_m = OK ? 〈CL_callee_trace,CM_callee_ptr〉)
       [ lapply Heval_func_cm -Heval_func_cm
         generalize in ⊢ ((??(?????%??)?) → ?);
         lapply Heq_ef_ef' -Heq_ef_ef'
         lapply Hexpr_vars_ef -Hexpr_vars_ef
         lapply Hexpr_vars_local_ef' -Hexpr_vars_local_ef'
         lapply Hexpr_vars_present_ef'
         lapply ef >Htyp_equality_ef #ef0 #HA #HB #HC @(jmeq_absorb ?????)
         #Heq destruct (Heq) #H1 #H2 @H2 ]
       #Heval_cm_func >Heval_cm_func ]
    whd in match (m_bind ?????);
    lapply (trans_fn … INV' … Hfind_funct)
    * #tmp_u * #cminor_fundef * #Hglobals_fresh_for_tmp_u * #Hfundef_fresh_for_tmp_u *
    #Htranslate_fundef #Hfind_funct_cm
    lapply (value_eq_ptr_inversion … Hvalue_eq_func) * #cm_func_ptr * #Hcm_func_ptr
    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'
    #Hcm_func_ptr #Heq destruct (Hcm_func_ptr Heq)
    [ 1,2: >addition_n_0 >mk_offset_offv_id
    | 3: ]
    >Hfind_funct_cm
    whd in match (opt_to_res ???); normalize nodelta
    (* Again, isolate cases by type similarity *)
    [ 1,2:
      cut (All (𝚺t:typ.CMexpr t)
            (λx:𝚺t:typ.expr t.(
              match x with
              [ mk_DPair ty e ⇒
               expr_vars ty e
                 (λid:ident
                  .λty0:typ.present SymbolTag val cm_env id)])) cm_args)
      [ 1: cases sInv * * normalize nodelta * #_ #_ #Hall #_ #_ @Hall
      | 3: cases sInv * * normalize nodelta * #_ #_ #Hall #_ #_ @Hall ]
      #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:
      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: generalize in match (proj1 ? (expr_vars ???) (proj1 ???)); #Hugly_pres
    | 2: generalize in match (proj1 ? (expr_vars ???) (proj1 ???)); #Hugly_pres
    | 3: ]
    [ 3: @(CMR_call … Hinjection … 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
         #Hfundef_fresh_for_tmp_u #Htranslate_fundef
         @ClCm_cont_call_store assumption
    | 1,2: (* no return or return to CM local variable *)
           @(CMR_call … Hinjection … HEm_fn_id) try assumption
           @(ClCm_cont_call_nostore … Hcont_rel) try assumption
           whd %{CL_lvalue_block} %{CL_lvalue_offset} %{(typeof lhs)} %{var_id}
           % %
    ]
| 1: (* Skip *)
    #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 * * * * #Hstmt_inv #Hlabels_translated #Htmps_preserved
    #Hreturn_ok #Hlabel_wf generalize in match (conj ????); #Hugly
    whd in ⊢ ((??%?) → ?); #Heq_translate #Hlabel_inclusion
    #tmpenv #Htmpenv #Hcont_rel
    lapply Heq_translate -Heq_translate
    lapply Hugly -Hugly
    lapply Hlabel_wf -Hlabel_wf
    lapply Hreturn_ok -Hreturn_ok
    lapply Htmps_preserved -Htmps_preserved
    lapply Hlabels_translated -Hlabels_translated
    lapply Hstmt_inv -Hstmt_inv
    lapply Htranslate_function -Htranslate_function
    lapply Hfresh_globals -Hfresh_globals
    lapply Hfresh_function -Hfresh_function
    lapply Htarget_type -Htarget_type
    lapply kInv -kInv
    lapply sInv -sInv
    lapply fInv -fInv
    lapply stmt_univ -stmt_univ    
    lapply Htmpenv -Htmpenv
    lapply stmt_univ' -stmt_univ'
    lapply Hlabel_inclusion -Hlabel_inclusion
    (* case analysis on continuation *)
    inversion Hcont_rel
    [ (* 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 #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
      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' #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 *)
      #Heq_translate
      (* 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 #Henv_below
      #Hclight_normal #Hnot_labeleld
      (* unfold the clight execution *)
      #s2 #tr whd in ⊢ ((??%?) → ?);
      inversion (fn_return cl_f) normalize nodelta
      [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
      | #structname #fieldspec | #unionname #fieldspec | #id ]
      #Hfn_return whd in ⊢ ((??%?) → ?); #Heq destruct (Heq)
      %{1} whd @conj try @conj try @refl
      [ 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 kcm_m stackptr))
      [ @(freelist_memory_inj_m1_m2 Em cl_m kcm_m 
            (free_list cl_m (blocks_of_env kcl_env)) 
            (free kcm_m stackptr) Hinjection (blocks_of_env kcl_env) stackptr ? (refl ??) (refl ??))
        assumption ]
      #Hinjection'
      @(CMR_return … Kend … Halloc_hyp Hcl_env_hyp … Hinjection') try assumption
      [ 2: #b lapply (Hmatching b)
           cases (lookup ?? kcl_env b) normalize nodelta
           [ 1: #H @H
           | 2: #b' cases (lookup ?? kalloc_type b) normalize nodelta
             [ 1: #H @H
             | 2: * #kalloc_type #ty normalize nodelta
                  cases kalloc_type normalize nodelta try //
                  #H #v #Hload_after_free @H
                  @(load_value_after_free_list_inversion … Hload_after_free)
             ]
           ]
      | 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 #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 #kHident_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
      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' #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 #Henv_below
      #Hclight_normal #Hnot_labeleld
      #s2 #tr whd in ⊢ ((??%?) → ?); #Heq destruct (Heq)
      %{1} whd @conj [ 2: #Habsurd destruct (Habsurd) ] @conj try @refl
      (* close simulation *)
      @(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 #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 #kHident_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 @(jmeq_absorb ?????) #HM @(jmeq_absorb ?????) #HN
      destruct (HF HG HH HI HJ HK HL HM HN) #_
      #Hlabel_inclusion
      #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_allocated
      #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching
      #HEm_fn_id #Hframe_spec #Henv_below
      #Hclight_normal #Hnot_labeleld
      #s2 #tr
      whd in ⊢ ((??%?) → ?); #Heq destruct (Heq)
      lapply kHfind_label -kHfind_label
      generalize in ⊢ ((??(????%????)?) → ?); #Hlabel_exists
      generalize in ⊢ ((???(????%)) → ?); #Hmore_invariant
      #kHfind_label
      (* Kwhile cont case *)
      %{2} whd whd in ⊢ (??%?); normalize nodelta 
      generalize in match (proj2 ???); #Hmore_noise
      generalize in match (proj1 ???); #Hmore_noise'
      >kHfind_label normalize nodelta
      whd @conj try @conj try @refl
      generalize in match (proj1 ???); #Hvars_present_in_ifthenelse
      generalize in match (proj2 ???); #Hcont_inv'
      [ 2: #Habsurd destruct (Habsurd) ]
      (* go to a special simulation state for while loops *)
      @(CMR_while … stacksize … Hcl_env_hyp … Hinjection … kHtranslate_expr … kHmklabels …  kHeq_translate)
      try assumption
      [ 1: (* TODO: lemma on Henv_below. We need to thread freshgens through cont_rel. *)
           @cthulhu
      | 2: cases Hmore_invariant * * #_ * * * * #_ #_ * #_ #_ * * #_ #H
           #_ #_ @H ]
    | 4,5: (* Continuations for Scall. TODO *)
      @cthulhu
    ]
| 2: (* Assign *)
     #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 * * * * #Hstmt_inv_cm #Hlabels_translated #Htmps_preserved
     #Hreturn_ok #Hlabel_wf generalize in match (conj ????); #Hugly #Htranslate
     #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
     #Hclight_normal #Hnot_labeleld
     lapply Htranslate -Htranslate
     (* case-split on lhs in order to reduce lvalue production in Cminor *)
     cases lhs #lhs_ed #lhs_ty
     cases (expr_is_Evar_id_dec lhs_ed)
     [ 2: * #var_id #Hlhs_ed destruct (Hlhs_ed)
          #Htranslate_statement
          cases (bind_inversion ????? Htranslate_statement)
          * #cm_rhs #Hexpr_vars_rhs * #Htranslate_rhs #Htranslate_statement'
          cases (bind_inversion ????? Htranslate_statement') -Htranslate_statement'
          #lhs_dest * #Htranslate_lhs
          cases (bind2_eq_inversion ?????? Htranslate_lhs) -Htranslate_lhs
          #alloctype * #type_of_var * #Hlookup_var_success
          cases alloctype in Hlookup_var_success;
          normalize nodelta
          [ 1: (* Global *) #r
               #Hlookup_var_success whd in ⊢ ((???%) → ?); #Hlhs_dest_eq
               destruct (Hlhs_dest_eq) normalize nodelta
               generalize in match (conj ????); #Hinvariant
               cases (type_eq_dec ??)
               [ 2: #Hneq normalize nodelta whd in ⊢ ((??%%) → ?);
                    #Habsurd destruct (Habsurd) ]
               normalize nodelta whd in match (typeof ?); #Heq_cl_types
               whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
               #s2 #tr whd in ⊢ ((??%?) → ?); #Hstep
               cases (bindIO_inversion ??????? Hstep) -Hstep
               * * #cl_blo #cl_off #cl_tr * whd in ⊢ ((??%?) → ?);
               #Hexec_lvalue #Hstep
               lapply (res_to_io ????? Hexec_lvalue) -Hexec_lvalue #Hexec_lvalue
               cases (bindIO_inversion ??????? Hstep) -Hstep
               * #cl_rhs_val #cl_trace * #Hexec_rhs #Hstep
               cases (bindIO_inversion ??????? Hstep) -Hstep
               #cl_mem_after_store_lhs * #Hstore
               whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
               lapply (opt_to_io_Value ?????? Hstore) -Hstore #Hstore
               %{1} whd whd in ⊢ (??%?); normalize nodelta
               generalize in match (proj1 ???); whd in ⊢ (% → ?); *
               whd in match (eval_expr ???????);
               whd in match (eval_constant ????);
               whd in Hexec_lvalue:(??%?);
               <(eq_sym … INV' var_id)
               lapply (Hmatching … var_id)
               cases (lookup ?? cl_env var_id) in Hexec_lvalue; normalize nodelta
               [ 1: #Heq_find_sym cases (bind_inversion ????? Heq_find_sym) -Heq_find_sym
                    #global_b * #Hopt_to_res lapply (opt_to_res_inversion ???? Hopt_to_res) -Hopt_to_res
                    #Hfind_symbol >Hfind_symbol
                    normalize nodelta
                    whd in ⊢ ((???%) → ?); #Heq destruct (Heq) #Hembed_eq
                    whd in match (m_bind ?????);
                    cases (eval_expr_sim … Halloc_hyp … Hcl_env_hyp … Hinjection … Hmatching) #Hsim_expr #_
                    lapply (Hsim_expr … Htranslate_rhs … (proj2 ?? (proj1 ?? (proj1 ?? sInv))) Hexec_rhs)
                    * #cm_rhs_val generalize in match (proj2 ???);
                    #Hexpr_vars_rhs * #Heval_expr_rhs #Hvalue_eq_rhs >Heval_expr_rhs
                    whd in match (m_bind ?????); whd in Hstore:(??%?); whd in Hstore:(??%?);
                    cases (store_value_of_type_success_by_value lhs_ty cl_m
                                    cl_mem_after_store_lhs cl_blo zero_offset cl_rhs_val Hstore)
                    #Haccess_mode #Hstorev
                    lapply (storen_parallel_aux ??? Hinjection … Hvalue_eq_rhs … Hembed_eq ??? Hstorev)
                    * #cm_mem_after_store_lhs * #Hstoren #Hinj whd in Hstoren:(??%?);
                    whd in Hstoren:(??%?); whd in match (shift_offset ???);
                    >sign_ext_same_size >addition_n_0
                    whd in match (storev ????);
                    lapply Hstoren whd in match (offset_plus ??);
                    >addition_n_0 -Hstoren
                    >Heq_cl_types #Hstoren >Hstoren
                    whd in match (opt_to_res ???); normalize nodelta
                    whd @conj try @conj try @refl
                    [ 2: #Habsurd destruct (Habsurd) ]
                    generalize in match (conj ????); #Hinv_vars
                    @CMR_normal try assumption
                    [ 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
                    >Hlookup_aux normalize nodelta @False_ind ]
          | 2: (* Stack *)
               #n #Hlookup_var_success
               whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
               normalize nodelta whd in ⊢ ((???%) → ?);
               cases (type_eq_dec ??) normalize nodelta #Htype_eq
               [ 2: #Habsurd destruct (Habsurd) ]
               #Heq destruct (Heq) #s2 #tr #Hstep
               cases (bindIO_inversion ??????? Hstep) 
               * * #cl_lvalue_block #cl_offset #cl_trace * #Hexec_lvalue
               lapply (res_to_io ????? Hexec_lvalue) -Hexec_lvalue
               whd in ⊢ ((??%?) → ?);
               @(match lookup ?? cl_env var_id
                 return λx. (lookup ?? cl_env var_id = x) → ?
                 with
                 [ None ⇒ λH. ?
                 | Some cl_addr ⇒ λH. ?
                 ] (refl ? (lookup ?? cl_env var_id)))
               normalize nodelta
               [ (* Contradiction: a stack-allocated variable was necessarily in the environment. TODO *)
                 @cthulhu
               | #Heq destruct (Heq)
                 lapply (Hmatching var_id) >H normalize nodelta
                 >(opt_to_res_inversion ???? Hlookup_var_success) normalize nodelta
                 #Hembedding_to_stack #Hexec_cl_rhs
                 cases (bindIO_inversion ??????? Hexec_cl_rhs) -Hexec_cl_rhs *
                 #cl_rhs_result #cl_rhs_trace * #Hcl_exec_expr_rhs #Hcl_exec_store
                 cases (bindIO_inversion ??????? Hcl_exec_store) -Hcl_exec_store #cl_mem_after_store
                 * #Hstore_value_of_type lapply (opt_to_io_Value ?????? Hstore_value_of_type)
                 -Hstore_value_of_type
                 #Hstore_value_of_type
                 whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
                 %{1} whd whd in ⊢ (??%?); normalize nodelta
                 whd in match (eval_expr ???????); 
                 whd in match (eval_constant ????);
                 whd in match (m_bind ?????);
                 cases (eval_expr_sim … Halloc_hyp … Hcl_env_hyp … Hinjection … Hmatching) #Hsim_expr #_
                 lapply (Hsim_expr … Htranslate_rhs … (proj2 ?? (proj1 ?? (proj1 ?? sInv))) Hcl_exec_expr_rhs)
                 * #cm_rhs_val generalize in match (proj2 ???);
                 #Hexpr_vars_rhs * #Heval_expr_rhs #Hvalue_eq_rhs >Heval_expr_rhs
                 normalize nodelta -Hsim_expr
                 whd in match (shift_offset ???); >sign_ext_same_size
                 >commutative_addition_n >addition_n_0
                 whd in Hstore_value_of_type:(??%?);
                 cases (store_value_of_type_success_by_value ? cl_m
                                    cl_mem_after_store ?? cl_rhs_result Hstore_value_of_type)
                 whd in match (typeof ?) in ⊢ ((??%%) → (??%?) → ?);
                 #Haccess_mode #Hstorev -Hstore_value_of_type
                 lapply (storen_parallel_aux ??? Hinjection … Hvalue_eq_rhs … Hembedding_to_stack ??? Hstorev)
                 * #cm_mem_after_store_lhs * #Hstoren #Hinj whd in Hstoren:(??%?);
                 >offset_plus_0 in Hstoren; #Hstorev'
                 whd in match (storev ????);
                 lapply Htype_eq whd in match (typeof ?) in ⊢ ((??%?) → ?); #Htype_eq'
                 <Htype_eq' >Hstorev'
                 whd in match (m_bind ?????); normalize nodelta
                 whd @conj try @conj try @refl
                 [ 2: #Habsurd destruct (Habsurd) ]                 
                 @(CMR_normal … Halloc_hyp) try assumption
                 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 
               cases (typ_eq ??) normalize nodelta #Htyp_eq
               whd in ⊢ ((???%) → ?);
               #Heq destruct (Heq) normalize nodelta -Htranslate_statement
               #Htranslate
               cases (bind_inversion ????? Htranslate) -Htranslate
               * #cm_expr #Hexpr_vars * #Htyp_should_eq
               whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
               cases (typ_should_eq_inversion (typ_of_type (typeof rhs)) (typ_of_type lhs_ty) … Htyp_should_eq)
               -Htyp_should_eq #Htyp_eq lapply Hexpr_vars_rhs lapply Hexpr_vars
               -Hlabel_wf -Hreturn_ok -Hlabels_translated -Hstmt_inv_cm lapply sInv               
               lapply cm_expr -cm_expr <Htyp_eq #cm_expr #sInv #Hexpr_vars #Hexpr_vars'
               @(jmeq_absorb ?????) #Heq destruct (Heq)
               #s2 #tr whd in ⊢ ((??%?) → ?); #Hcl_exec
               cases (bindIO_inversion ??????? Hcl_exec)
               * * #cl_blo #cl_off #cl_trace *
               whd in ⊢ ((???%) → ?);
               #Hexec_lvalue lapply (res_to_io ????? Hexec_lvalue) -Hexec_lvalue
               whd in ⊢ ((??%?) → ?);
               @(match lookup ?? cl_env var_id
                 return λx. (lookup ?? cl_env var_id = x) → ?
                 with
                 [ None ⇒ λH. ?
                 | Some cl_addr ⇒ λH. ?
                 ] (refl ? (lookup ?? cl_env var_id)))
               normalize nodelta
               [ (* Contradiction: a register-allocated variable was necessarily in the environment *)
                 (* TODO, cf Hlookup_var_success or sInv *)
                 @cthulhu
               | #Heq destruct (Heq)
                 lapply (Hmatching var_id) >H normalize nodelta
                 >(opt_to_res_inversion ???? Hlookup_var_success) normalize nodelta
                 #Hpresent_in_local #Hexec_cl_rhs
                 cases (bindIO_inversion ??????? Hexec_cl_rhs) -Hexec_cl_rhs *
                 #cl_rhs_result #cl_rhs_trace * #Hcl_exec_expr_rhs #Hcl_exec_store
                 cases (bindIO_inversion ??????? Hcl_exec_store) -Hcl_exec_store #cl_mem_after_store
                 * #Hstore_value_of_type lapply (opt_to_io_Value ?????? Hstore_value_of_type)
                 -Hstore_value_of_type #Hstore_value_of_type
                 whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
                 %{1} whd whd in ⊢ (??%?); normalize nodelta
                 cases (eval_expr_sim … Halloc_hyp … Hcl_env_hyp … Hinjection … Hmatching) #Hsim_expr #_
                 lapply (Hsim_expr … Htranslate_rhs … (proj2 ?? (proj1 ?? (proj1 ?? sInv))) Hcl_exec_expr_rhs)
                 * #cm_rhs_val generalize in match (proj2 ???);
                 #Hexpr_vars_rhs * #Heval_expr_rhs #Hvalue_eq_rhs >Heval_expr_rhs
                 normalize nodelta -Hsim_expr whd @conj try @conj try @refl
                 [ 2: #Habsurd destruct (Habsurd) ]
                 generalize in match (proj1 ???); #Hpresent
                 generalize in match (conj ????); #Hstmt_vars
                 @(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) ]
               ]
          ]
     | 1: #Hnot_evar #Htranslate_statement
          cases (bind_inversion ????? Htranslate_statement) -Htranslate_statement
          * #cm_rhs #Hexpr_vars_rhs * #Htranslate_rhs #Htranslate_statement'
          cases (bind_inversion ????? Htranslate_statement') -Htranslate_statement' #dest
          lapply (translate_dest_not_Evar_id alloc_type ? lhs_ty Hnot_evar)
          #Htranslate_dest * #Htranslate_dest'
          >Htranslate_dest' in Htranslate_dest; #Haux lapply (sym_eq ??? Haux) -Haux #Haux
          cases (bind_inversion ????? Haux) -Haux
          * #translated_dest #Hexpr_vars_dest * #Htranslate_addr
          whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) normalize nodelta
          cases (type_eq_dec ??)
          [ 2: #Hneq normalize nodelta whd in ⊢ ((??%%) → ?);
               #Habsurd destruct (Habsurd) ]
          normalize nodelta whd in match (typeof ?); #Heq_cl_types
          whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
          #s2 #tr whd in ⊢ ((??%?) → ?); #Hstep
          cases (bindIO_inversion ??????? Hstep) -Hstep
          * * #cl_blo #cl_off #cl_tr * whd in ⊢ ((??%?) → ?);
          #Hexec_lvalue #Hstep
          lapply (translate_dest_MemDest_simulation …
                     INV' ???????? Halloc_hyp Hcl_env_hyp Hinjection Hmatching ??????
                     Htranslate_dest' Hexec_lvalue)
          [ 1: @(proj1 ?? (proj1 ?? (proj1 ?? sInv))) ]
          * #cm_val_dest * #Heval_cm_dest #Hvalue_eq_dest
          %{1} whd whd in ⊢ (??%?); normalize nodelta
          >Heval_cm_dest
          whd in match (m_bind ?????);
          cases (bindIO_inversion ??????? Hstep) -Hstep
          * #val #trace * #Hexec_expr #Hstep
          cases (bindIO_inversion ??????? Hstep) -Hstep
          #cl_mem_after_store * #Hopt_store
          whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
          lapply (opt_to_io_Value ?????? Hopt_store) -Hopt_store
          #Hstore_value_of_type whd in Hstore_value_of_type:(??%?);
          cases (eval_expr_sim … Halloc_hyp … Hcl_env_hyp … Hinjection … Hmatching) #Hsim_expr #_
          lapply (Hsim_expr … Htranslate_rhs … (proj2 ?? (proj1 ?? (proj1 ?? sInv))) Hexec_expr)
          * #cm_rhs_val generalize in match (proj2 ???);
          #Hexpr_vars_rhs * #Heval_expr_rhs #Hvalue_eq_rhs >Heval_expr_rhs
          normalize nodelta -Hsim_expr
          cases (store_value_of_type_success_by_value ? cl_m
                                    cl_mem_after_store ?? val Hstore_value_of_type)
          whd in match (typeof ?) in ⊢ ((??%%) → (??%?) → ?);
          #Haccess_mode #Hstorev -Hstore_value_of_type
          cases (value_eq_ptr_inversion … Hvalue_eq_dest) * #cm_blo #cm_off * #Hcm_val_dest destruct (Hcm_val_dest)
          whd in ⊢ ((??%?) → ?); #Hembed
          cases (some_inversion ????? Hembed) -Hembed
          * #cm_blo' #cm_off' * #Hembed normalize nodelta #Heq destruct (Heq)
          lapply (storen_parallel_aux ??? Hinjection … Hvalue_eq_rhs … Hembed ??? Hstorev)
          * #cm_mem_after_store_lhs * #Hstoren #Hinj whd in Hstoren:(??%?);
          whd in match (storev ????);
          lapply Hstoren
          (* make the types match *)
          generalize in match (conj ????); #Hstmt_vars' >Heq_cl_types 
          #Hstoren >Hstoren
          whd in match (m_bind ?????); normalize nodelta whd @conj try @conj try @refl
          [ 2: #Habsurd destruct (Habsurd) ]
          @(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 *)
     #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 * * * * #Hstmt_inv_cm #Hlabels_translated #Htmps_preserved
     #Hreturn_ok #Hlabel_wf generalize in match (conj ????); #Hugly #Htranslate #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
     #Hclight_normal #Hnot_labeleld
     cases (bind_inversion ????? Htranslate) -Htranslate
     * * * #tmp_gen #labgen #cm_s1 #Htrans_inv * #Htrans_stm1 normalize nodelta
     #Htranslate cases (bind_inversion ????? Htranslate) -Htranslate     
     * * * #tmp_gen' #labgen' #cm_s2 #Htrans_inv' * #Htrans_stm2 normalize nodelta
     whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
     #s2 #tr whd in ⊢ ((??%?) → ?); #Heq destruct (Heq)
     %{1} whd @conj try @conj try @refl
     [ 2: #Habsurd destruct (Habsurd) ]
     @(CMR_normal … Htrans_stm1) try assumption
     [ 1: lapply Hlabel_inclusion
          @transitive_lset_inclusion @lset_inclusion_union %1
          @reflexive_lset_inclusion
     | 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: assumption ]
     ]
| *: (* Other statements *) @cthulhu ]
| 2: (* Return state *)
  #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
  #Hclight_normal #Hnot_labeleld
  whd in Hclight_normal:%;
  @False_ind @Hclight_normal
| 3: (* Call state *)
  #cl_ge #cm_ge #INV' #cl_k #cm_st #cl_fundef #cm_fundef
  #fblock #target_type #cl_env #cl_m #cm_env #cm_m
  #fn_id #Hfind_cl #Hfind_cm
  #tmpenv #Hcont_rel
  #Em #Hinj #Hem_fn_id
  #cl_args_values #cm_args_values #Hall2
  #Hclight_normal #Hnot_labeleld
  whd in Hclight_normal:%;
  @False_ind @Hclight_normal
| 4: (* Intermediary While state *)
     (* ---------------------------------------------------------------------- *)
#cl_ge #cm_ge #INV' 
#cl_f #cm_f #cl_env #cl_m #cm_env #cm_m #stackptr #stacksize #alloc_type
#cl_k #cm_k #sz #sg #cl_cond_ty #cl_cond_desc #cl_body #entry_label #exit_label #cm_cond #cm_body
#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'' #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
#Hclight_normal #Hnot_labeleld
#s2 #tr whd in ⊢ ((??%?) → ?); #Hstep
(* execute clight condition *)
cases (bindIO_inversion ??????? Hstep) -Hstep
* #cl_cond_val #cl_cond_trace * #Hcl_exec_cond #Hstep
cases (bindIO_inversion ??????? Hstep) -Hstep
#cl_cond_bool * #Hcl_bool_of_val whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
(* The numbers of steps to execute in Cminor depends on the outcome of the condition
   evaluation *)
cases cl_cond_bool in Hcl_bool_of_val;
[ (* cond = true: continue looping *)
  #Hcl_bool_of_val
  %{3} whd whd in ⊢ (??%?); normalize nodelta
  generalize in match (proj1 ???); #Hpresent_ifthenelse
  (* Exhibit simulation of condition evaluation *)
  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
  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〉)
  [ lapply Hpresent_ifthenelse
    <(CMcast_identity (ASTint sz sg) cm_cond) #foo
    lapply Hcm_eval_cond whd in match (eq_ind_r ??????); normalize nodelta cases Heq_ty
    #H @H ]
  #Heval >Heval
  whd in match (m_bind ?????);
  >(eval_bool_of_val_to_Cminor … Hvalue_eq … Hcl_bool_of_val)
  normalize nodelta whd
  generalize in match (proj1 ???); #Hnoise'
  generalize in match (conj ????); #Hnoise'' @conj try @conj
  [ 3: #Habsurd destruct (Habsurd)
  | 1: normalize >append_nil @refl
  | 2: @(CMR_normal … Htranslate_function … Htranslate_statement) try assumption
       @(ClCm_cont_while … Htranslate_inv … Hmk_labels … Htranslate_statement) try assumption
  ]
| (* cond = false: stop looping *)
  #Hcl_bool_of_val
  %{4} whd whd in ⊢ (??%?); normalize nodelta
  generalize in match (proj1 ???); #Hpresent_ifthenelse
  (* Exhibit simulation of condition evaluation *)
  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
  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〉)
  [ lapply Hpresent_ifthenelse
    <(CMcast_identity (ASTint sz sg) cm_cond) #foo
    lapply Hcm_eval_cond whd in match (eq_ind_r ??????); normalize nodelta cases Heq_ty
    #H @H ]
  #Heval >Heval
  whd in match (m_bind ?????);
  >(eval_bool_of_val_to_Cminor … Hvalue_eq … Hcl_bool_of_val)
  normalize nodelta whd
  generalize in match (proj1 ???); #Hnoise'
  generalize in match (proj2 ???); #Hnoise''
  generalize in match (conj ????); #Hnoise'''
  whd @conj try @conj
  [ 3: #Habsurd destruct (Habsurd)
  | 1: normalize >append_nil >append_nil @refl
  | 2: @(CMR_normal … DoNotConvert) try assumption
       try @refl
       @(env_below_freshgen_preserved_by_translation … Htranslate_statement)
       assumption
  ]
]

] qed.

 
(* TODO: move to globalenvs *)
(* The hypotheses are a little strong - we don't need to know that the size of
   the initialisation data is the same. *)
lemma find_funct_id_match:
    ∀M:matching.
    ∀initV,initW. (∀v,w. match_var_entry M v w → size_init_data_list (initV (\snd v)) = size_init_data_list (initW (\snd w))) →
    ∀p: program (m_A M) (m_V M). ∀p': program (m_B M) (m_W M).
    ∀MATCH:match_program … M p p'.
    ∀v. ∀f: m_A M (prog_var_names … p). ∀id.
    find_funct_id … (globalenv … initV p) v = Some ? 〈f,id〉 →
    ∃tf : m_B M (prog_var_names … p').
    find_funct_id … (globalenv … initW p') v = Some ? 〈tf,id〉 ∧ match_fundef M ? f (tf⌈m_B M ? ↦ m_B M (prog_var_names … p)⌉).
[ 2: >(matching_vars … (mp_vars … MATCH)) % ]
#M #initV #initW #varsOK #p #p' #MP * [ | #sz #i | | #p ] #f #id
[ 1,2,3: #FF whd in FF:(??%?); destruct ]
#FFI cases (find_funct_id_ptr ????? FFI) #b * * #E destruct #FS #FFPI
cases (find_funct_ptr_id_inv ????? FFPI) #FFP #SFB
cases (find_funct_ptr_match M initV initW … MP ? f FFP)
#f' * #FFP' #MF %{f'} %
[ @find_funct_ptr_id_conv
  @(make_find_funct_ptr_id ???? id FFP' ?)
  whd in ⊢ (??%?); >(symbols_match … initV … MP) [ @SFB | @varsOK ]
| @MF
] qed.

lemma clight_cminor_inv_exists : ∀p,p'.
  clight_to_cminor p = OK … p' →
  clight_cminor_inv (make_global … clight_fullexec p) (make_global … Cminor_fullexec p').
#p #p' #COMPILE
lapply (clight_to_cminor_matches … COMPILE) #MATCHES -COMPILE
%
[2: #sym lapply (find_symbol_match (clight_cminor_matching p) ????? MATCHES)
    [4: #H @sym_eq @H | #X #Y * #id #r #v1 #v2 * % | skip | skip ]
|3: #v #f #id #FF cases (find_funct_id_match … MATCHES … FF)
  [ #f' * #FF' whd in ⊢ (% → ?); * #H1 * #H2 #Efd
    % [2: %{f'} %{H1} %{H2} % [ >Efd
    -Efd -H1 -H2 -FF' -FF
    generalize in ⊢ (??(??(match % with [_⇒?]))?);
    >(matching_vars … (mp_vars … MATCHES)) -MATCHES
    #E @(streicherK ???? E) %
    | @FF'
    ]
   | skip
   ]
  | skip
  | #X #Y * #id' #r #v1 #v2 * %
  ]
| skip
] qed.

(* TODO: move to common/Pointers.ma *)
axiom offset_plus_zero : ∀o.
  offset_plus o zero_offset = o.

(* TODO: move to memory model *)
lemma valid_block_dec: ∀m,b. (valid_block m b) + (¬valid_block m b).
#m * #b
whd in ⊢ (?%(?%));
lapply (refl ? (Zltb b (nextblock m)))
cases (Zltb b (nextblock m)) in ⊢ (???% → ?);
#H
[ %1 @Zltb_true_to_Zlt assumption
| %2 @Zltb_false_to_not_Zlt assumption
] qed.

definition equal_embedding : mem → block → option (block × offset) ≝
λm,b. match valid_block_dec m b with
[ inl _ ⇒ Some ? 〈b,zero_offset〉
| inr _ ⇒ None ?
].

lemma valid_pointer_valid_block : ∀m,b,o.
  valid_pointer m (mk_pointer b o) →
  valid_block m b.
#m #b #o #VP
cases (andb_Prop_true … VP) #H
cases (andb_Prop_true … H) #B #_ #_
whd @(Zltb_true_to_Zlt … B)
qed.

lemma valid_block_dec_true : ∀m,b.
  valid_block m b →
  ∃H. valid_block_dec m b = inl … H.
#m * #b #H whd in ⊢ (??(λ_.??%?)); whd in H;
generalize in ⊢ (??(λ_.??(?%)?));
>(Zlt_to_Zltb_true … H) in ⊢ (???% → ??(λ_.??(match % with [_⇒?|_⇒?]?)?));
#E % [2: % | skip ]
qed.

lemma not_Zlt_to_Zltb_false : ∀x,y.
  ¬(Zlt x y) →
  Zltb x y = false.
#x #y #N lapply (Zltb_true_to_Zlt x y)
cases (Zltb x y) //
#H @⊥ @(absurd … (H (refl ??))) @N
qed.

lemma valid_block_dec_false : ∀m,b.
  ¬valid_block m b →
  ∃H. valid_block_dec m b = inr … H.
#m * #b #H whd in ⊢ (??(λ_.??%?)); whd in H;
generalize in ⊢ (??(λ_.??(?%)?));
>(not_Zlt_to_Zltb_false … H) in ⊢ (???% → ??(λ_.??(match % with [_⇒?|_⇒?]?)?));
#E % [2: % | skip ]
qed.

(* TODO: move to memoryInjections.ma? *)
lemma equal_value_eq : ∀m,ty,b,o,v.
  (∀p. load_value_of_type ty m b o = Some ? (Vptr p) → valid_pointer m p) →
  load_value_of_type ty m b o = Some ? v →
  value_eq (equal_embedding m) v v.
#m #ty #b #o * //
* #b' #o' #H1 #H2 @vptr_eq
whd in ⊢ (??%?); whd in match (equal_embedding ??);
cases (valid_block_dec_true … (valid_pointer_valid_block m b' o' ?))
[2: @H1 @H2 ]
#H3 #E >E whd in ⊢ (??%?);
>offset_plus_zero %
qed.

lemma equal_embedding_elim : ∀m,b,b',o. ∀P:block → offset → Prop.
  equal_embedding m b = Some ? 〈b',o〉 →
  (valid_block m b → P b zero_offset) →
  P b' o.
#m * #b #b' #o #P
whd in ⊢ (??%? → ?);
cases (valid_block_dec ??) #H #E
whd in E:(??%%); destruct
/2/
qed.

lemma pointer_translation_elim : ∀m,p,p'. ∀P:pointer → Prop.
  pointer_translation p (equal_embedding m) = Some ? p' →
  P p →
  P p'.
#m * #b #o * #b' #o' #P whd in ⊢ (??%? → ?);
whd in match (equal_embedding m b);
cases (valid_block_dec ??)
#H #E whd in E:(??%?); [ >offset_plus_zero in E; #E ] destruct
//
qed.

lemma pointer_translation_elim' : ∀m,b,o,b',o'. ∀P:block → offset → Prop.
  pointer_translation (mk_pointer b o) (equal_embedding m) = Some ? (mk_pointer b' o') →
  P b o →
  P b' o'.
#m #b #o #b' #o' #P whd in ⊢ (??%? → ?);
whd in match (equal_embedding m b);
cases (valid_block_dec ??)
#H #E whd in E:(??%?); [ >offset_plus_zero in E; #E ] destruct
//
qed.

lemma equal_memory_injection : ∀m.
  (∀b. valid_block m b → block_implementable_bv m b) →
  (∀ty,b,o,p. load_value_of_type ty m b o = Some ? (Vptr p) → valid_pointer m p) →
  memory_inj (equal_embedding m) m m.
#m #addr_ok #contents_ok %
[ whd #b1 #off1 #b2 #off2 #ty #v1 #Hvalid #Htrans
  @(pointer_translation_elim' … Htrans)
  #Hload
  %{v1} destruct %{Hload} @(equal_value_eq … Hload) @contents_ok
| #b #H whd in ⊢ (??%?);
  cases (valid_block_dec_false … H) #H' #E >E %
| * #b #o #p' #Hv #Ht @(pointer_translation_elim … Ht)
  @Hv
| #b #b' #off #Hem @(equal_embedding_elim … Hem) //
| #b #b' #o' #Hem @(equal_embedding_elim … Hem) //
| whd #b1 #b2 #b1' #b2' #delta1 #delta2 #NE #Hem1 #Hem2
  @(equal_embedding_elim … Hem1)
  @(equal_embedding_elim … Hem2)
  #_ #_ @eq_block_elim [ #E @⊥ @(absurd … E NE) | // ]
| #b whd whd in match (equal_embedding m b);
  cases (valid_block_dec m b) #H whd //
  % [ % @addr_ok assumption | cases (addr_ok … H) #_ * #_ #H' >Zplus_z_OZ @H' ]
] qed.

axiom init_mem_good : ∀F,V,i,p,m.
  init_mem F V i p = OK … m →
  (∀b. valid_block m b → block_implementable_bv m b) ∧
  (∀ty,b,o,p. load_value_of_type ty m b o = Some ? (Vptr p) → valid_pointer m p).

lemma init_clight_cminor : ∀p,p',s.
  make_initial_state … clight_fullexec p = OK … s →
  clight_to_cminor p = OK … p' →
  ∃INV:clight_cminor_inv (make_global … clight_fullexec p) (make_global … Cminor_fullexec p').
  ∃s'.
    make_initial_state … Cminor_fullexec p' = OK … s' ∧
    clight_cminor_rel (make_global … clight_fullexec p) (make_global … Cminor_fullexec p') INV s s'.
#p #p' #s #INIT #COMPILE
lapply (clight_to_cminor_matches … COMPILE) #MATCHES

%{(clight_cminor_inv_exists … COMPILE)}

lapply (find_funct_ptr_match (clight_cminor_matching p) (fst ??) (λx.x) … MATCHES)
lapply (find_symbol_match (clight_cminor_matching p) (fst ??) (λx.x) … MATCHES)
[ #v #w * // ]
lapply (init_mem_match (clight_cminor_matching p) (fst ??) (λx.x) … MATCHES)
[ #v #w * // ]
cases p in INIT COMPILE MATCHES ⊢ %; #vars #fns #main #INIT #COMPILE #MATCHES
cases (bind_inversion ????? INIT) -INIT #m * #INITMEM #INIT
cases (bind_inversion ????? INIT) -INIT #b * #FINDSYM #INIT
cases (bind_inversion ????? INIT) -INIT #fd * #FFP #INIT
whd in INIT:(??%%); destruct
whd in match (m_A ??); whd in match (m_B ??); whd in match (m_V ?); whd in match (m_W ?);
#M_initmem #M_findsym #M_ffp
cases (M_ffp … FFP) -M_ffp #f' * #FFP' #Mf'
%{(Callstate main f' [ ] m SStop)} %
[ whd in ⊢ (??%?); normalize in M_initmem:(??(?%%%?)(?%%%?)); >M_initmem >INITMEM
  whd in ⊢ (??%?); lapply (M_findsym main) <(mp_main … MATCHES) 
  whd in match (m_A ??); whd in match (m_B ??);
  change with (make_global p') in match (globalenv ????); #E >E
  >FINDSYM
  whd in ⊢ (??%?); >FFP'
  whd in ⊢ (??%?); %
| @(CMR_call … b (Some ? (ASTint I32 Signed)) (empty_map …) ? (empty_map …) … (ClCm_cont_stop …))
  [ @find_funct_ptr_id_conv @make_find_funct_ptr_id
    [ @FFP
    | @(symbol_for_block_fn … FINDSYM FFP)
    ]
  | @find_funct_ptr_id_conv @make_find_funct_ptr_id
    [ @FFP'
    | @(symbol_for_block_fn … FFP') >M_findsym @FINDSYM
    ]
  | @([ ])
  | %
  | whd @(equal_embedding m)
  | cases (init_mem_good … INITMEM) #H1 #H2 @equal_memory_injection assumption 
  | (* This is a little too concrete... and the property is true but a little
       strong (we always map function blocks in the embedding - even if there's
       no function!) *)
    #b #CODE cut (valid_block m b)
    [ cases b in CODE ⊢ %; * [2,3:#z] #CODE whd in CODE:(??%?); destruct whd
      lapply (nextblock_pos m) cases (nextblock m) [2,3,5,6:#z'] try * %
    ] #VALID
    whd in ⊢ (??%?); cases (valid_block_dec ??)
    [ //
    | #INVALID @⊥ @(absurd … VALID INVALID)
    ]
  | %
  ]
] qed.