Changeset 3036


Ignore:
Timestamp:
Mar 29, 2013, 5:12:09 PM (4 years ago)
Author:
garnier
Message:

Fixing some problems, progress, etc

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/toCminorCorrectness.ma

    r2857 r3036  
    246246    match u2 with
    247247    [ mk_universe p2 ⇒ p2 ≤ p1 ] ].
    248    
     248
    249249definition fte ≝ fresher_than_or_equal.
    250250
     
    256256* // qed.
    257257
    258 definition labgen_include ≝
    259   λgen1, gen2 : labgen.
    260   ∃labels. label_genlist gen2 = labels @ label_genlist gen1.
    261  
    262 definition tmpgen_include ≝
    263   λvartypes.
    264   λgen1, gen2 : tmpgen vartypes.
    265   ∃idents. tmp_env ? gen2 = idents @ (tmp_env ? gen1).
     258(* Express that the [first] tmpgen generates "newer" ids than an other one. *)
     259definition tmpgen_fresher_than ≝
     260  λvars. λgen1, gen2 : tmpgen vars.
     261    fresher_than_or_equal (tmp_universe … gen1) (tmp_universe … gen2).
     262
     263(* Map a predicate on all the /keys/ of an environment, i.e. on a set
     264 * of identifiers. *)
     265definition env_domain_P : cl_env → ∀P:(ident → Prop). Prop ≝
     266 λe, P.
     267  match e with
     268  [ an_id_map m ⇒
     269    fold ?? (λkey,elt,acc. P (an_identifier ? key) ∧ acc) m True
     270  ].
     271
     272(* Property for an identifier to be out of the set
     273 * of identifiers represented by an universe. *)
     274definition ident_below_universe ≝
     275  λi: ident.
     276  λu: universe SymbolTag.
     277  match i with
     278  [ an_identifier id ⇒
     279    match u with
     280    [ mk_universe id_u ⇒
     281      id < id_u         
     282    ]   
     283  ].
     284
     285(* Property of the domain of an environment to be disjoint of the set
     286 * of identifiers represented by an universe. *) 
     287definition env_below_freshgen : env → ∀vars. tmpgen vars → Prop ≝
     288  λe, vars, tmpgen.
     289  env_domain_P e (λid. ident_below_universe id (tmp_universe … tmpgen)).
     290
     291(* The property of interest for the proof. Identifiers generated from an
     292 * universe above the environment are not in the said environment. *)
     293lemma lookup_fails_outside_of_env :
     294  ∀env, vars, ty, gen, id, gen'.
     295  alloc_tmp vars ty gen = 〈id, gen'〉 →
     296  env_below_freshgen env vars gen →
     297  lookup ?? env id = None ?.
     298@cthulhu
     299qed. 
     300
     301(* The property of being above an environment is conserved by fresh ident
     302 * generation *)
     303lemma alloc_tmp_env_invariant :
     304  ∀env, vars, ty, gen, id, gen'.
     305  alloc_tmp vars ty gen = 〈id, gen'〉 →
     306  env_below_freshgen env vars gen →
     307  env_below_freshgen env vars gen'.
     308@cthulhu
     309qed.
    266310
    267311(* --------------------------------------------------------------------------- *)
     
    274318(* Temporary variables generated during conversion are well-allocated. *)
    275319definition tmp_vars_well_allocated ≝
    276    λvartypes.
    277    λtmp_gen: tmpgen vartypes.
     320   λtmpenv: list (ident × type).
    278321   λcm_env.
    279322   λcm_m.
     
    282325   ∀local_variable.
    283326   ∀H:present ?? cm_env local_variable.
    284    ∀ty. Exists ? (λx. x = 〈local_variable, ty〉) (tmp_env … tmp_gen)
     327   ∀ty. Exists ? (λx. x = 〈local_variable, ty〉) tmpenv
    285328   ∀v. val_typ v (typ_of_type ty) →
    286329   ∃cm_m'. storev (typ_of_type ty) cm_m (lookup_present ?? cm_env local_variable H) v = Some ? cm_m' ∧
     
    394437(* --------------------------------------------------------------------------- *)
    395438
    396 record frame_data
    397   (f : function)
    398   (ge_cl : genv_t clight_fundef)
    399   (ge_cm : genv_t (fundef internal_function))
    400   (INV : clight_cminor_inv ge_cl ge_cm) : Type[0] ≝
    401 {
    402 }.
    403 
    404439definition CMcast : ∀t,t'. CMexpr t → t = t' → CMexpr t'.
    405440#t #t' #e #H destruct (H) @e
     
    415450  ∀cl_f: function.                          (* current Clight function *)
    416451  internal_function →                       (* current Cminor function *)
    417   cl_env →
    418   cm_env →
    419   var_types →
    420   (*frame_data cl_f cl_ge cm_ge INV →*)         (* data for the current stack frame in CL and CM *)
    421   option typ →                              (* optional target type - uniform over a given function *)
     452  cl_env →                                  (* Clight local environment *)
     453  cm_env →                                  (* Cminor local environment *)
     454  mem →                                     (* Cminor memory state *)
     455  ∀alloc_type:var_types.                    (* map vars to alloc type *)
     456  ∀tmpenv:list (ident×type).                (* list of generated variables *)
     457  (*tmpgen alloc_type →                       (* input freshgen *)
     458    tmpgen alloc_type →                       (* output freshgen *) *) (* bad idea *)
     459  option typ →                              (* optional target type - arg. uniform over a given function *)
    422460  cl_cont →                                 (* CL cont *)
    423461  cm_cont →                                 (* CM cont *)
    424   stack →                                   (* CM stack *) 
     462  stack →                                   (* CM stack *)
    425463  Prop ≝
    426 (* Stop continuation*) 
     464(* Stop continuation *)
    427465| ClCm_cont_stop:
    428466  ∀cl_ge, cm_ge, INV, cl_f, cm_f, target_type.
    429   ∀cl_env, cm_env, alloc_type.
     467  ∀cl_env, cm_env, cm_m, alloc_type, tmpenv. (*, stmt_univ, stmt_univ'.*)
    430468  ∀cm_stack.
    431469  cm_stack = SStop →
    432   clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type target_type Kstop Kend cm_stack
     470  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
    433471
    434472(* Seq continuation *)
     
    437475  ∀stack.
    438476  ∀alloc_type.
     477  ∀tmpenv.
    439478  ∀cl_s: statement.
    440479  ∀cm_s: stmt.
    441480  ∀cl_env: cl_env.
    442481  ∀cm_env: cm_env.
     482  ∀cm_m: mem.
    443483  ∀cl_k': cl_cont.
    444484  ∀cm_k': cm_cont.
     
    451491  (* ---- invariant on label existence ---- *)
    452492  lset_inclusion ? (labels_of cm_s) (labels_of (f_body cm_f)) →
    453   clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type target_type cl_k' cm_k' stack →
    454   clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type target_type (ClKseq cl_s cl_k') (Kseq cm_s cm_k') stack
     493  (* ---- invariant on fresh variables ---- *)
     494  lset_inclusion ? (tmp_env alloc_type stmt_univ') tmpenv →
     495  clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env cm_m alloc_type tmpenv (*stmt_univ stmt_univ'*) target_type cl_k' cm_k' stack →
     496  clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env cm_m alloc_type tmpenv (*stmt_univ stmt_univ'*) target_type (ClKseq cl_s cl_k') (Kseq cm_s cm_k') stack
    455497
    456498(* While continuation *) 
     
    460502  ∀stack.
    461503  ∀alloc_type.
     504  ∀tmpenv.
    462505  ∀cl_env.
    463506  ∀cm_env.
    464 
     507  ∀cm_m.
    465508  (* sub-continuations *)
    466509  ∀cl_k': cl_cont.
    467510  ∀cm_k': cm_cont.
    468 
    469511  (* elements of the source while statement *)
    470512  ∀sz,sg.
     
    473515  ∀cl_body.
    474516  ∀Heq: ASTint sz sg = typ_of_type cl_ty.
    475 
    476517  (* elements of the converted while statement *)
    477518  ∀cm_cond: CMexpr (ASTint sz sg).
    478519  ∀cm_body.
    479   ∀entry,exit: identifier Label.
    480  
     520  ∀entry,exit: identifier Label.
    481521  (* universes used to generate fresh labels and variables *) 
    482522  ∀stmt_univ, stmt_univ'.
     
    484524  ∀lbls: lenv.
    485525  ∀Htranslate_inv.
    486 
    487526  (* relate CL and CM expressions *)
    488   ∀Hexpr_vars.
    489   translate_expr alloc_type (Expr cl_cond_desc cl_ty) = OK ? («CMcast ?? cm_cond Heq, Hexpr_vars») →
    490 
     527  ∀Hexpr_vars:expr_vars ? cm_cond (local_id alloc_type).
     528  translate_expr alloc_type (Expr cl_cond_desc cl_ty) ≃ OK ? («cm_cond, Hexpr_vars») →
    491529  (* Parameters and results to find_label_always *)
    492530  ∀sInv: stmt_inv cm_f cm_env (f_body cm_f).
    493531  ∀Hlabel_declared: Exists (identifier Label) (λl'.l'=entry) (labels_of (f_body cm_f)).
    494532  ∀Hinv.
    495 
    496533  (* Specify how the labels for the while-replacing gotos are produced *)
    497534  mklabels lbl_univ = 〈〈entry, exit〉, lbl_univ'〉 →
    498535  translate_statement alloc_type stmt_univ lbl_univ' lbls (ConvertTo entry exit) target_type cl_body = OK ? «〈stmt_univ',lbl_univ'',cm_body〉, Htranslate_inv» →
    499   (* Invariant on label existence *)
    500   lset_inclusion ? (labels_of cm_body) (labels_of (f_body cm_f)) → 
     536  (* ---- Invariant on label existence ----  *)
     537  lset_inclusion ? (labels_of cm_body) (labels_of (f_body cm_f)) →
     538  (* ---- invariant on fresh variables ---- *)
     539  lset_inclusion ? (tmp_env alloc_type stmt_univ') tmpenv → 
    501540  find_label_always entry (f_body cm_f) Kend Hlabel_declared cm_f cm_env sInv I =
    502541    «〈(*St_label entry*)
     
    504543            (St_ifthenelse ?? cm_cond (St_seq cm_body (St_goto entry)) St_skip)
    505544            (St_label exit St_skip)), cm_k'〉, Hinv» →
    506   clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type target_type cl_k' cm_k' stack →
    507   clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type target_type (
    508     Kwhile (Expr cl_cond_desc cl_ty) cl_body cl_k')
    509     (Kseq (St_goto entry) (Kseq (St_label exit St_skip) cm_k')) stack.
    510 (* TODO: Kcall *)
    511 
    512 (* TODO XXX *)
    513 (* relation between placeholders for return values *)
    514 
    515 definition return_value_rel :
    516   ∀cl_f, cl_ge, cm_ge.
    517   ∀INV: clight_cminor_inv cl_ge cm_ge.
    518   frame_data cl_f ?? INV →
    519   option (block×offset×type) → option (ident×typ) → Prop ≝
    520 λcl_f, cl_ge, cm_ge, INV, data, opt1, opt2.
    521 match opt1 with
    522 [ None ⇒
    523   match opt2 with
    524   [ None ⇒ True
    525   | _ ⇒ False ]
    526 | Some ptr ⇒
    527   match opt2 with
    528   [ Some id ⇒ True (* TODO, here. *)
    529   | None ⇒ False
    530   ]
    531 ].
     545  clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env cm_m alloc_type tmpenv (* stmt_univ stmt_univ' *) target_type cl_k' cm_k' stack →
     546  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
     547    (Kwhile (Expr cl_cond_desc cl_ty) cl_body cl_k')
     548    (Kseq (St_goto entry) (Kseq (St_label exit St_skip) cm_k')) stack
     549   
     550| ClCm_cont_call_store:
     551  ∀cl_ge, cm_ge, INV, cl_f, cm_f, target_type.
     552  ∀stack.
     553  ∀alloc_type.
     554  ∀tmp_env.
     555  ∀cl_env.
     556  ∀cm_env.
     557  ∀cm_m.
     558  (* sub-continuations *)
     559  ∀cl_k': cl_cont.
     560  ∀cm_k': cm_cont.
     561  (* CL return addr *)
     562  ∀CL_lvalue_block,CL_lvalue_offset,lhs_ty.
     563  ∀CM_lvalue_ptr.
     564  (* CM stack content *)
     565  ∀stackptr.
     566  ∀fInv.
     567  ∀tmp_var, ret_var.
     568  ∀Htmp_var_present.
     569  ∀Hret_present.
     570  ∀Hstmt_inv.
     571  (* TODO: loads of invariants *)
     572  clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env cm_m alloc_type tmp_env (*stmt_univ stmt_univ*) target_type
     573    (Kcall (Some ? 〈CL_lvalue_block, CL_lvalue_offset, lhs_ty〉) cl_f cl_env cl_k')
     574    cm_k'
     575    (Scall (Some ? 〈ret_var,typ_of_type lhs_ty〉) cm_f stackptr
     576     (update_present SymbolTag val cm_env tmp_var Htmp_var_present (Vptr CM_lvalue_ptr)) Hret_present
     577     (stmt_inv_update cm_f cm_env (f_body cm_f) tmp_var (Vptr CM_lvalue_ptr) fInv Htmp_var_present)
     578     (Kseq
     579      (St_store (typ_of_type lhs_ty) (Id ASTptr tmp_var)
     580       (Id (typ_of_type lhs_ty) ret_var)) cm_k') Hstmt_inv stack)
     581
     582| ClCm_cont_call_nostore:
     583  ∀cl_ge, cm_ge, INV, cl_f, cm_f, target_type.
     584  ∀stack.
     585  ∀alloc_type.
     586  ∀tmpenv.
     587  ∀cl_env.
     588  ∀cm_env.
     589  ∀cm_m.
     590  (* sub-continuations *)
     591  ∀cl_k': cl_cont.
     592  ∀cm_k': cm_cont.
     593  (* CM stack content *)
     594  ∀cl_lhs, cm_lhs.
     595  match cl_lhs with
     596  [ None ⇒ match cm_lhs with [ None ⇒ True | _ ⇒ False ]
     597  | Some cl_location ⇒
     598    match cm_lhs with
     599    [ None ⇒ False
     600    | Some cm_location ⇒
     601      ∃CL_lvalue_block, CL_lvalue_offset, lhs_ty, ret_var.
     602       cl_location = 〈CL_lvalue_block,CL_lvalue_offset, lhs_ty〉 ∧
     603       cm_location = 〈ret_var, typ_of_type lhs_ty〉
     604    ]
     605  ] →
     606  ∀Hret_present.
     607  ∀Hstmt_inv.
     608  ∀stackptr.
     609  ∀fInv.
     610(*  ∀stmt_univ.*)
     611  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
     612   (Kcall cl_lhs cl_f cl_env cl_k')
     613    cm_k'
     614   (Scall cm_lhs cm_f stackptr cm_env Hret_present fInv cm_k' Hstmt_inv stack).
     615
     616lemma translate_fundef_internal :
     617  ∀ge1, ge2.
     618  ∀INV: clight_cminor_inv ge1 ge2.
     619  ∀u, cl_f, cm_fundef.
     620  ∀H1, H2. 
     621  translate_fundef u (globals ?? INV) H1 (CL_Internal cl_f) H2 = OK ? cm_fundef →
     622  ∃cm_f. cm_fundef = Internal ? cm_f ∧
     623         translate_function u (globals ge1 ge2 INV) cl_f H1 H2 = OK ? cm_f.
     624#ge1 #ge2 #INV #u #cl_f #cm_fd #H1 #H2
     625whd in ⊢ ((??%?) → ?); cases (translate_function u (globals ge1 ge2 INV) cl_f H1 H2)
     626normalize nodelta
     627[ 2: #er #Habsurd destruct (Habsurd)
     628| 1: #cm_f #Heq destruct (Heq) %{cm_f} @conj @refl ]
     629qed.
     630
     631lemma translate_fundef_external :
     632  ∀ge1, ge2.
     633  ∀INV: clight_cminor_inv ge1 ge2.
     634  ∀u, id, tl, ty.
     635  ∀H1, H2.
     636  translate_fundef u (globals ?? INV) H1 (CL_External id tl ty) H2 =
     637    OK ? (External ? (mk_external_function id (signature_of_type tl ty))).
     638#ge1 #ge2 #INV #u #id #tl #ty #H1 #H2 @refl
     639qed.
    532640
    533641(* Definition of the simulation relation on states. The orders of the parameters is dictated by
    534642 * the necessity of performing an inversion on the continuation sim relation without having to
    535643 * play the usual game of lapplying all previous dependent arguments.  *)
     644
    536645inductive clight_cminor_rel : ∀cl_ge, cm_ge. clight_cminor_inv cl_ge cm_ge  → Clight_state → Cminor_state → Prop ≝
     646(* --------------------------------------------------------------------------- *)
     647(* normal state *)
     648(* --------------------------------------------------------------------------- *)
    537649| CMR_normal :
    538650  (* Clight and Cminor global envs *)
     
    571683  ∀kInv: cont_inv cm_f cm_env cm_k.
    572684  (* ---- relate return type variable to actual return type ---- *)
    573   rettyp = opttyp_of_type (fn_return cl_f) → 
     685  rettyp = opttyp_of_type (fn_return cl_f) →
    574686  (* ---- relate Clight and Cminor functions ---- *)
    575687  ∀func_univ: universe SymbolTag.
     
    592704  lset_inclusion ? (labels_of cm_s) (labels_of (f_body cm_f)) →
    593705  (* ---- relate Clight continuation to Cminor continuation ---- *)
    594   clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type rettyp cl_k cm_k cm_st →
     706  ∀tmpenv.
     707  lset_inclusion ? (tmp_env ? stmt_univ') tmpenv →
     708  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 →
    595709  (* ---- state invariants for memory and environments ---- *)
    596710  (* Embedding *)
    597711  ∀Em: embedding.
    598712  (* locals are properly allocated *)
    599   tmp_vars_well_allocated alloc_type stmt_univ' cm_env cm_m cl_m Em →
     713  tmp_vars_well_allocated tmpenv cm_env cm_m cl_m Em →
    600714  (* specify how alloc_type is built *)
    601715  characterise_vars (globals ?? INV) cl_f = 〈alloc_type, stacksize〉 →
     
    611725  (∀b1.∀delta. Em b1=Some ? 〈stackptr,delta〉 →
    612726               mem block b1 (blocks_of_env cl_env)) →
     727  (* The fresh name generator is compatible with the clight environment *)
     728  env_below_freshgen cl_env alloc_type stmt_univ →
    613729  clight_cminor_rel cl_ge cm_ge INV
    614730    (ClState cl_f cl_s cl_k cl_env cl_m)
    615731    (CmState cm_f cm_s cm_env fInv sInv cm_m stackptr cm_k kInv cm_st)
    616 
     732(* --------------------------------------------------------------------------- *)
     733(* return state *)
     734(* --------------------------------------------------------------------------- *)
    617735| CMR_return :
     736  (* Clight and Cminor global envs *)
    618737  ∀cl_ge, cm_ge.
     738  (* Relates globals to globals and functions to functions. *)
    619739  ∀INV: clight_cminor_inv cl_ge cm_ge.
    620   ∀cl_f: function.                               (* Clight enclosing function *)
    621   ∀cm_f: internal_function.                             (* enclosing function *)
     740  (* ---- Continuations and functions ---- *)
     741  (* Clight continuation *)
     742  ∀cl_k: cl_cont.
     743  (* Cminor continuation *)
     744  ∀cm_k: cm_cont.
     745  (* Cminor stack *)
     746  ∀cm_st: stack.
     747  (* Clight enclosing function *)
     748  ∀cl_f: function.
     749  (* Cminor enclosing function *)
     750  ∀cm_f: internal_function.
     751  (* mapping from variables to their Cminor alloc type *)
    622752  ∀alloc_type.
     753  (* Clight env/mem *)
    623754  ∀cl_env, cl_m.
     755  (* Cminor env/mem *)
    624756  ∀cm_env, cm_m.
    625   ∀cm_st: stack.                                              (* Cminor stack *)
     757  (* Stack pointer (block containing Cminor locals), related size *)
    626758  ∀stackptr, stacksize.
    627   ∀stmt_univ.
     759  (* fresh label generator *)
     760  ∀stmt_univ: tmpgen alloc_type.
     761  ∀tmpenv.
     762  lset_inclusion ? (tmp_env ? stmt_univ) tmpenv →
     763  (* ---- state invariants for memory and environments ---- *)
     764  (* Embedding *)
    628765  ∀Em: embedding.
    629   tmp_vars_well_allocated alloc_type stmt_univ cm_env cm_m cl_m Em →        (* locals are properly allocated *)
    630   characterise_vars (globals ?? INV) cl_f = 〈alloc_type, stacksize〉 →        (* specify how alloc_type is built *)
    631   (∃m,m'. exec_alloc_variables empty_env m (fn_params cl_f @ fn_vars cl_f) = 〈cl_env,m'〉) → (* spec. Clight env *)
    632   memory_inj Em cl_m cm_m →                                                  (* memory injection *)
    633   memory_matching Em cl_ge cm_ge cl_m cm_m cl_env cm_env INV stackptr alloc_type →  (* map CL env to CM env *)             
    634   (∀b. block_region b = Code → Em b = Some ? 〈b, zero_offset〉) →             (* Force embedding to compute identity on functions *)
     766  (* locals are properly allocated *)
     767  tmp_vars_well_allocated tmpenv cm_env cm_m cl_m Em →
     768  (* specify how alloc_type is built *)
     769  characterise_vars (globals ?? INV) cl_f = 〈alloc_type, stacksize〉 →
     770  (* spec. Clight env at alloc time *)
     771  (∃m,m'. exec_alloc_variables empty_env m (fn_params cl_f @ fn_vars cl_f) = 〈cl_env,m'〉) →
     772  (* memory injection *)
     773  memory_inj Em cl_m cm_m →
     774  (* map CL env to CM env *)
     775  memory_matching Em cl_ge cm_ge cl_m cm_m cl_env cm_env INV stackptr alloc_type →
     776  (* Force embedding to compute identity on functions *)
     777  (∀b. block_region b = Code → Em b = Some ? 〈b, zero_offset〉) →
    635778  (* Make explicit the fact that locals in CL are mapped to a single CM block *)
    636779  (∀b1.∀delta. Em b1=Some ? 〈stackptr,delta〉 →
    637                mem block b1 (blocks_of_env cl_env)) → 
     780               mem block b1 (blocks_of_env cl_env)) →
     781  clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env cm_m alloc_type tmpenv (*stmt_univ stmt_univ*) (None ?) cl_k cm_k cm_st →
    638782  clight_cminor_rel cl_ge cm_ge INV
    639     (ClReturnstate Vundef Kstop cl_m)
     783    (ClReturnstate Vundef cl_k cl_m)
    640784    (CmReturnstate (None val) cm_m cm_st)
    641 
    642 | CMR_call_nostore :
    643  (* call to a function with no return value, or which returns in a local variable in Cminor *)
    644  ∀cl_ge, cm_ge, cl_f, cm_f.
    645  ∀INV: clight_cminor_inv cl_ge cm_ge.
    646  ∀alloc_type, cl_env, cl_m, cm_env, cm_m, cm_stack, stackptr.
    647  (* TODO: put the actual invariants on memory and etc. here *)
    648  ∀u: universe SymbolTag.
    649  ∀cl_fundef, cm_fundef.
    650  ∀Hglobals_fresh: globals_fresh_for_univ type (globals cl_ge cm_ge INV) u.
    651  ∀Hfundef_fresh:  fd_fresh_for_univ cl_fundef u.
    652  ∀rettyp. rettyp = opttyp_of_type (fn_return cl_f) →
    653  ∀cl_k, cm_k.
    654  ∀fblock.
    655  match cl_fundef with
    656  [ CL_Internal cl_function ⇒
    657     find_funct clight_fundef cl_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? (CL_Internal cl_function) ∧
    658     find_funct (fundef internal_function) cm_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? cm_fundef ∧
    659     translate_fundef u (globals ?? INV) Hglobals_fresh cl_fundef Hfundef_fresh = OK ? cm_fundef ∧
    660     clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type rettyp cl_k cm_k cm_stack
    661  | CL_External name argtypes rettype ⇒
    662    True
    663  ] →
    664  ∀cl_fun_id, cm_fun_id.
    665  cl_fun_id = cm_fun_id →
    666  ∀cl_retval, cm_retval.
    667  ∀sInv, fInv, kInv.
    668  ∀cl_args_values, cm_args_values.
    669  (* TODO: return_value_rel … INV frame_data cl_retval cm_retval →*)
    670  (* TODO: add invariant All2 value_eq cl_args_values cm_args_values *)
    671  clight_cminor_rel cl_ge cm_ge INV
    672   (ClCallstate cl_fun_id
    673    cl_fundef cl_args_values (Kcall cl_retval cl_f cl_env cl_k) cl_m)
    674   (CmCallstate cm_fun_id cm_fundef
    675    cm_args_values cm_m (Scall cm_retval cm_f stackptr cm_env sInv fInv cm_k kInv cm_stack))
    676 
    677 | CMR_call_store :
    678  (* call to a function which returns to some location in memory in Cminor *)
    679  ∀cl_ge, cm_ge, cl_f, cm_f.
    680  ∀INV: clight_cminor_inv cl_ge cm_ge.
    681  ∀alloc_type, cl_env, cl_m, cm_env, cm_m, cm_stack, stackptr.
    682  (* TODO: put the actual invariants on memory and etc. here *)
    683  ∀u: universe SymbolTag.
    684  ∀cl_fundef, cm_fundef.
    685  ∀Hglobals_fresh: globals_fresh_for_univ type (globals cl_ge cm_ge INV) u.
    686  ∀Hfundef_fresh:  fd_fresh_for_univ cl_fundef u.
    687  ∀rettyp. rettyp = opttyp_of_type (fn_return cl_f) →
    688  ∀cl_k, cm_k.
    689  ∀fblock.
    690  match cl_fundef with
    691  [ CL_Internal cl_function ⇒
    692     find_funct clight_fundef cl_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? (CL_Internal cl_function) ∧
    693     find_funct (fundef internal_function) cm_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? cm_fundef ∧
    694     translate_fundef u (globals ?? INV) Hglobals_fresh cl_fundef Hfundef_fresh = OK ? cm_fundef ∧
    695     clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type rettyp cl_k cm_k cm_stack
    696  | CL_External name argtypes rettype ⇒
    697    True
    698  ] →
    699  ∀cl_fun_id, cm_fun_id.
    700  cl_fun_id = cm_fun_id →
    701  ∀cl_rettyp, cl_retval, cl_rettrace, cm_retval.
    702  ∀cl_lhs, cm_lhs, Hinvariant_on_cm_lhs.
    703  (* Explain where the lhs of the post-return assign comes from *)
    704  exec_lvalue cl_ge cl_env cl_m cl_lhs = OK ? 〈cl_retval, cl_rettrace〉 →
    705  translate_dest alloc_type cl_lhs = OK ? (MemDest ? «cm_lhs, Hinvariant_on_cm_lhs») →
    706  (* TODO: Explain that the actual variable used to store the ret val is fresh and has the
    707   * right type, etc *)
    708  ∀cm_ret_var.
    709  ∀sInv, fInv, kInv.
    710  ∀cl_args_values, cm_args_values.
    711  (* TODO: return_value_rel … INV frame_data cl_retval cm_retval →*)
    712  (* TODO: add invariant All2 value_eq cl_args_values cm_args_values *)
    713  ∀cm_stack.
    714  clight_cminor_rel cl_ge cm_ge INV
    715   (ClCallstate cl_fun_id
    716    cl_fundef cl_args_values (Kcall (Some ? 〈cl_retval,cl_rettyp〉) cl_f cl_env cl_k) cl_m)
    717   (CmCallstate cm_fun_id cm_fundef
    718    cm_args_values cm_m (Scall cm_retval cm_f stackptr cm_env sInv fInv
    719                           (Kseq (St_store (typ_of_type cl_rettyp) cm_lhs
    720                                           (Id (typ_of_type cl_rettyp) cm_ret_var)) cm_k)
    721                            kInv cm_stack))
    722 
     785(* --------------------------------------------------------------------------- *)
     786(* call state *)
     787(* --------------------------------------------------------------------------- *)
     788| CMR_call :
     789  (* Clight and Cminor global envs *)
     790  ∀cl_ge, cm_ge.
     791  (* Relates globals to globals and functions to functions. *) 
     792  ∀INV:  clight_cminor_inv cl_ge cm_ge.
     793  (* ------- Continuations and functions for the current stack frame -------- *)
     794  (* Clight continuation *)
     795  ∀cl_k: cl_cont.
     796  (* Cminor continuation *) 
     797  ∀cm_k: cm_cont.
     798  (* Cminor stack *)
     799  ∀cm_st: stack.
     800  (* Clight enclosing function *)
     801  ∀cl_f: function.
     802  (* Cminor enclosing function *)
     803  ∀cm_f: internal_function.
     804  (* Clight called fundef *)
     805  ∀cl_fundef.
     806  (* Cminor called fundef *)
     807  ∀cm_fundef.
     808  (* block of Clight and Cminor function *)
     809  (* XXX why do I need that already ? *)
     810  ∀fblock: block.
     811  (* optional return type of the function *)
     812  ∀target_type.
     813  (* mapping from variables to their Cminor alloc type *)                                 
     814  ∀alloc_type.
     815  (* Clight env/mem *)
     816  ∀cl_env, cl_m.
     817  (* Cminor env/mem *)
     818  ∀cm_env, cm_m.
     819  (* Stack pointer (block containing Cminor locals), stack frame size *)
     820  ∀stackptr, stacksize.
     821  (* fresh label generator for function *)
     822  ∀func_univ: universe SymbolTag.
     823  (* relate CL and CM enclosing functions *)
     824  ∀Hglobals_fresh, Hfundef_fresh.
     825  translate_function func_univ (globals ?? INV) cl_f Hglobals_fresh Hfundef_fresh = OK ? cm_f →
     826  (* specify fblock *)
     827  find_funct clight_fundef cl_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? cl_fundef →
     828  find_funct (fundef internal_function) cm_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? cm_fundef →
     829  ∀cl_fun_id, cm_fun_id.
     830  ∀stmt_univ: tmpgen alloc_type.
     831  ∀tmpenv.
     832  lset_inclusion ? (tmp_env ? stmt_univ) tmpenv →
     833  match cl_fundef with
     834  [ CL_Internal _ ⇒
     835     (* specify continuation *)
     836     clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env cm_m alloc_type tmpenv target_type cl_k cm_k cm_st
     837(*       ∨
     838     (∃cl_blo, cl_off, cl_ty.         (* Clight return loscation + type *)
     839      ∃cm_loc_ident, cm_return_ident. (* Cminor locals storing the lvalues *)
     840      ∃sInv, fInv, kInv.              (* Invariants required by the stack construction *)
     841       present ?? cm_env cm_loc_ident ∧
     842       present ?? cm_env cm_return_ident ∧
     843       (clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env cm_m alloc_type target_type
     844          (Kcall (Some ? 〈cl_blo, cl_off, cl_ty〉) cl_f cl_env cl_k)
     845           cm_k (Scall (Some ? 〈cm_return_ident,typ_of_type cl_ty〉) cm_f stackptr cm_env sInv fInv
     846                     (Kseq (St_store (typ_of_type cl_ty) (Id ? cm_loc_ident) (Id ? cm_return_ident)) cm_k)
     847                      kInv cm_st))) *)
     848  | CL_External cl_id cl_argtypes cl_rettype ⇒
     849    match cm_fundef with
     850    [ Internal _ ⇒ False
     851    | External cm_f_ext ⇒ True ]
     852(*      match cm_f_ext with
     853      [ mk_external_function cm_id sig ⇒
     854        cl_fun_id = cl_id ∧ cm_fun_id = cm_id ∧ cl_fun_id = cm_fun_id
     855      ] *)
     856  ] →
     857  (* ---- state invariants for memory and environments ---- *)
     858  (* Embedding *)
     859  ∀Em: embedding.
     860  (* locals are properly allocated *)
     861  tmp_vars_well_allocated tmpenv cm_env cm_m cl_m Em →
     862  (* specify how alloc_type is built *)
     863  characterise_vars (globals ?? INV) cl_f = 〈alloc_type, stacksize〉 →
     864  (* spec. Clight env at alloc time *)
     865  (∃m,m'. exec_alloc_variables empty_env m (fn_params cl_f @ fn_vars cl_f) = 〈cl_env,m'〉) →
     866  (* memory injection *)
     867  memory_inj Em cl_m cm_m →
     868  (* map CL env to CM env *)
     869  memory_matching Em cl_ge cm_ge cl_m cm_m cl_env cm_env INV stackptr alloc_type →
     870  (* Force embedding to compute identity on functions *)
     871  (∀b. block_region b = Code → Em b = Some ? 〈b, zero_offset〉) →
     872  (* Make explicit the fact that locals in CL are mapped to a single CM block *)
     873  (∀b1.∀delta. Em b1=Some ? 〈stackptr,delta〉 →
     874               mem block b1 (blocks_of_env cl_env)) →
     875  ∀cl_args_values, cm_args_values.
     876  All2 val val (λcl_val:val.λcm_val:val.value_eq Em cl_val cm_val) cl_args_values cm_args_values →
     877  clight_cminor_rel cl_ge cm_ge INV
     878   (ClCallstate cl_fun_id cl_fundef cl_args_values cl_k cl_m)
     879   (CmCallstate cm_fun_id cm_fundef cm_args_values cm_m cm_st)
     880(* --------------------------------------------------------------------------- *)
     881(* special while state *)
     882(* --------------------------------------------------------------------------- *)
    723883| CMR_while:
    724884 ∀cl_ge,cm_ge,INV,cl_f,cm_f.
     
    750910 translate_function func_univ (globals ?? INV) cl_f Hfresh_globals Hfresh_function = OK ? cm_f →
    751911 (* ---- relate continuations ---- *)
    752  clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type rettyp cl_k cm_k cm_stack →
    753912 ∀stmt_univ,stmt_univ',lbl_univ,lbl_univ',lbl_univ'',lbls.
     913 ∀tmpenv'.
     914 lset_inclusion ? (tmp_env ? stmt_univ') tmpenv' →
     915 clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env cm_m alloc_type tmpenv' rettyp cl_k cm_k cm_stack →
    754916 (* Invariants *)
    755917 ∀Em: embedding.
    756  tmp_vars_well_allocated alloc_type stmt_univ' cm_env cm_m cl_m Em →        (* locals are properly allocated *)
     918 tmp_vars_well_allocated tmpenv' cm_env cm_m cl_m Em →        (* locals are properly allocated *)
    757919 characterise_vars (globals ?? INV) cl_f = 〈alloc_type, stacksize〉 →        (* specify how alloc_type is built *)
    758920 (∃m,m'. exec_alloc_variables empty_env m (fn_params cl_f @ fn_vars cl_f) = 〈cl_env,m'〉) → (* spec. Clight env *)
     
    761923 (∀b. block_region b = Code → Em b = Some ? 〈b, zero_offset〉) →             (* Force embedding to compute identity on functions *)
    762924 (* Make explicit the fact that locals in CL are mapped to a single CM block *)
    763  (∀b1.∀delta. Em b1=Some ? 〈stackptr,delta〉 →
     925 (∀b1.∀delta. Em b1 = Some ? 〈stackptr,delta〉 →
    764926              mem block b1 (blocks_of_env cl_env)) →
     927 (* The fresh name generator is compatible with the clight environment *)
     928 env_below_freshgen cl_env alloc_type stmt_univ →             
    765929 (* Expression translation and related hypotheses *)
    766  ∀Hcond_tr.  (* invariant after converting conditional expr *)
    767  translate_expr alloc_type (Expr cl_cond_desc cl_ty) = OK ? «CMcast ?? cm_cond Heq_ty, Hcond_tr » →
     930 ∀Hcond_tr:expr_vars ? cm_cond (local_id alloc_type).  (* invariant after converting conditional expr *)
     931 (* translate_expr alloc_type (Expr cl_cond_desc cl_ty) = OK ? «CMcast ?? cm_cond Heq_ty, Hcond_tr » → *)
     932 translate_expr alloc_type (Expr cl_cond_desc cl_ty) ≃ OK ? «cm_cond, Hcond_tr » →
    768933 (* Label consistency *)
    769934 Exists ? (λl':identifier Label.l'=entry_label) (labels_of (f_body cm_f)) →
     
    795960     (St_ifthenelse sz sg cm_cond (St_seq cm_body (St_goto entry_label)) St_skip)
    796961     (St_label exit_label St_skip)))
    797    cm_env fInv sInv cm_m stackptr cm_k kInv cm_stack)).
     962   cm_env fInv sInv cm_m stackptr cm_k kInv cm_stack)).
     963
     964   
     965(*
     966| CMR_call_nostore :
     967 (* call to a function with no return value, or which returns in a local variable in Cminor *)
     968 ∀cl_ge, cm_ge. (* cl_f, cm_f.*)
     969 ∀INV: clight_cminor_inv cl_ge cm_ge.
     970 ∀alloc_type, cl_env, cl_m, cm_env, cm_m, cm_stack, stackptr.
     971 (* TODO: put the actual invariants on memory and etc. here *)
     972 ∀func_univ: universe SymbolTag.
     973 ∀cl_f, cm_f.
     974 ∀Hglobals_fresh: globals_fresh_for_univ type (globals cl_ge cm_ge INV) func_univ.
     975 ∀Hfundef_fresh:  fd_fresh_for_univ (CL_Internal cl_f) func_univ.
     976 ∀rettyp.
     977 ∀cl_k, cm_k.
     978 ∀fblock.
     979 rettyp = opttyp_of_type (fn_return cl_f) ∧
     980 find_funct clight_fundef cl_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? (CL_Internal cl_f) →
     981 find_funct (fundef internal_function) cm_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? (Internal ? cm_f) →
     982 translate_function func_univ (globals ?? INV) cl_f Hglobals_fresh Hfundef_fresh = OK ? cm_f →
     983 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 →
     984 ∀fun_id.
     985 ∀cl_retval, cm_retval.
     986 ∀sInv, fInv, kInv.
     987 ∀cl_args_values, cm_args_values.
     988 All2 val val (λcl_val:val.λcm_val:val.value_eq Em cl_val cm_val) cl_args_values cm_args_values →
     989 (* TODO: return_value_rel … INV frame_data cl_retval cm_retval →*)
     990 clight_cminor_rel cl_ge cm_ge INV
     991  (ClCallstate fun_id (CL_Internal cl_f) cl_args_values cl_k cl_m)
     992  (CmCallstate fun_id (Internal ? cm_f) cm_args_values cm_m cm_stack)
     993
     994| CMR_call_store :
     995 (* call to a function which returns to some location in memory in Cminor *)
     996 ∀cl_ge, cm_ge.
     997 ∀INV: clight_cminor_inv cl_ge cm_ge.
     998 ∀alloc_type, cl_env, cl_m, cm_env, cm_m, cm_stack, stackptr.
     999 (* TODO: put the actual invariants on memory and etc. here *)
     1000 ∀func_univ: universe SymbolTag.
     1001 ∀cl_f, cm_f.
     1002 ∀Hglobals_fresh: globals_fresh_for_univ type (globals cl_ge cm_ge INV) func_univ.
     1003 ∀Hfundef_fresh:  fd_fresh_for_univ (CL_Internal cl_f) func_univ.
     1004 ∀rettyp.
     1005 ∀cl_k, cm_k.
     1006 ∀fblock.
     1007 rettyp = opttyp_of_type (fn_return cl_f) →
     1008 find_funct clight_fundef cl_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? (CL_Internal cl_f) →
     1009 find_funct (fundef internal_function) cm_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? (Internal ? cm_f) →
     1010 translate_function func_univ (globals ?? INV) cl_f Hglobals_fresh Hfundef_fresh = OK ? cm_f →
     1011 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 →
     1012 ∀fun_id.
     1013 ∀cl_rettyp, cl_retval, cl_rettrace, cm_retval.
     1014 ∀cl_lhs, cm_lhs, Hinvariant_on_cm_lhs.
     1015 (* Explain where the lhs of the post-return assign comes from *)
     1016 exec_lvalue cl_ge cl_env cl_m cl_lhs = OK ? 〈cl_retval, cl_rettrace〉 →
     1017 translate_dest alloc_type cl_lhs = OK ? (MemDest ? «cm_lhs, Hinvariant_on_cm_lhs») →
     1018 (* TODO: Explain that the actual variable used to store the ret val is fresh and has the
     1019  * right type, etc *)
     1020 ∀cm_ret_var.
     1021 ∀sInv, fInv, kInv.
     1022 ∀cl_args_values, cm_args_values.
     1023 All2 val val (λcl_val:val.λcm_val:val.value_eq Em cl_val cm_val) cl_args_values cm_args_values →
     1024 (* TODO: return_value_rel … INV frame_data cl_retval cm_retval →*)
     1025 ∀cm_stack.
     1026 clight_cminor_rel cl_ge cm_ge INV
     1027  (ClCallstate fun_id (CL_Internal cl_f)
     1028    cl_args_values (Kcall (Some ? 〈cl_retval,cl_rettyp〉) cl_f cl_env cl_k) cl_m)
     1029  (CmCallstate fun_id (Internal ? cm_f)
     1030    cm_args_values cm_m (Scall cm_retval cm_f stackptr cm_env sInv fInv
     1031                          (Kseq (St_store (typ_of_type cl_rettyp) cm_lhs
     1032                                          (Id (typ_of_type cl_rettyp) cm_ret_var)) cm_k)
     1033                           kInv cm_stack))
     1034*)   
    7981035
    7991036definition clight_normal : Clight_state → bool ≝
     
    8881125#p #Hlookup %{p} @conj try @refl assumption
    8891126qed.
     1127
     1128lemma find_funct_id_inversion :
     1129  ∀F: Type[0]. ∀ge: genv_t F. ∀ptr. ∀f. ∀id.
     1130  find_funct_id F ge ptr = Some ? 〈f, id〉 →
     1131  ∃H:(find_funct F ge ptr = Some ? f).
     1132     id = symbol_of_function_val' F ge ptr f H.
     1133#F #ge #ptr #f #id
     1134whd in match (find_funct_id ???);
     1135generalize in match (refl ??);
     1136generalize in ⊢
     1137  (∀_:(???%).
     1138    (??(match %
     1139        with
     1140        [ _ ⇒ λ_. ?
     1141        | _ ⇒ λ_.λ_. ? ] ?)?) → ?);
     1142#o cases o
     1143normalize nodelta
     1144[ #H #Habsurd destruct (Habsurd)
     1145| #f #Hfind #Heq destruct (Heq) %{Hfind}
     1146  cases (find_funct_inversion ???? Hfind) #ptr *
     1147  * * #Hptr lapply Hfind -Hfind >Hptr #Hfind
     1148  #Hoff #Hblock * #id * #Hblock_id #Hlookup_opt
     1149  normalize nodelta @refl
     1150] qed.
    8901151
    8911152(* We should be able to prove that ty = ty' with some more hypotheses, if needed. *)
     
    10121273[ #r | #n | ]
    10131274* #cl_type * #Heq_lookup normalize nodelta
     1275[ 3: cases (type_eq_dec ??) normalize nodelta #H
     1276  [ 2: whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd) ]
     1277| *: ]
    10141278whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
    10151279whd in ⊢ ((??%?) → ?);
     
    10571321  ]
    10581322] qed.
    1059  
     1323
    10601324(* lift simulation result to eval_exprlist *)
     1325
    10611326lemma eval_exprlist_simulation :
    10621327  ∀cl_f.
     
    12111476qed. (* this last lemma has to be refitted. *)
    12121477
    1213 (* This, to say the least, is not pretty. Whenever we update the memory, we have to perform
    1214  * a kind of functional record update on the frame_data. But of course, we also need equations
    1215  * relating the old and new frame data. *)
    1216 (*
    1217 lemma update_clight_cminor_data_cm :
    1218   ∀f, cl_ge, cm_ge, INV.
    1219   ∀frame_data: clight_cminor_data f cl_ge cm_ge INV.
    1220   ∀cl_m_v.
    1221   ∀new_cm_mem.
    1222   cl_m_v = cl_m … frame_data →
    1223   ∀new_inj: memory_inj (Em … frame_data) cl_m_v new_cm_mem.
    1224   ∃data:clight_cminor_data f cl_ge cm_ge INV.
    1225           alloc_type … frame_data = alloc_type … data ∧
    1226           cl_env … frame_data = cl_env … data ∧
    1227           cm_env … frame_data = cm_env … data ∧
    1228           stackptr … frame_data = stackptr … data ∧
    1229           cl_m … frame_data = cl_m … data ∧
    1230           new_cm_mem = (cm_m … data).
    1231 #f #cl_ge #cm_ge #INV #frame_data #cl_m_v #new_cm_mem #H destruct (H) #Hinj
    1232 %{(mk_clight_cminor_data ????
    1233        (alloc_type … frame_data)
    1234        (stacksize … frame_data)
    1235        (alloc_hyp … frame_data)
    1236        (cl_env … frame_data)
    1237        (cm_env … frame_data)
    1238        (cl_env_hyp … frame_data)
    1239        (cl_m … frame_data)
    1240        new_cm_mem
    1241        (Em … frame_data)
    1242        Hinj
    1243        (stackptr … frame_data)
    1244        (matching … frame_data)
    1245        (Em_fn_id … frame_data))}
    1246 @conj try @conj try @conj try @conj try @conj try @refl
    1247 qed.*)
    1248 
    1249 (* Same thing, this time update both CL and CM memory. Here we provide a proof
    1250  * that the data in local env is not touched. *)
    1251 (*
    1252 lemma update_clight_cminor_data_cl_cm_global :
    1253   ∀f, cl_ge, cm_ge, INV.
    1254   ∀frame_data: clight_cminor_data f cl_ge cm_ge INV.
    1255   ∀new_cl_mem, new_cm_mem.
    1256   ∀new_inj: memory_inj (Em … frame_data) new_cl_mem new_cm_mem. 
    1257   (∀id, b, cl_type.
    1258    lookup ?? (cl_env … frame_data) id = Some ? b →
    1259    lookup ?? (alloc_type … frame_data) id = Some ? 〈Local, cl_type〉 →
    1260    load_value_of_type cl_type (cl_m … frame_data) b zero_offset =
    1261    load_value_of_type cl_type new_cl_mem b zero_offset) → 
    1262   ∃data:clight_cminor_data f cl_ge cm_ge INV.
    1263         alloc_type … frame_data = alloc_type … data ∧
    1264         cl_env … frame_data = cl_env … data ∧
    1265         cm_env … frame_data = cm_env … data ∧
    1266         stackptr … frame_data = stackptr … data ∧
    1267         new_cl_mem = (cl_m … data) ∧
    1268         new_cm_mem = (cm_m … data).
    1269 #f #cl_ge #cm_ge #INV #frame_data #new_cl_mem #new_cm_mem #Hinj #Haux
    1270 %{(mk_clight_cminor_data ????
    1271        (alloc_type … frame_data)
    1272        (stacksize … frame_data)
    1273        (alloc_hyp … frame_data)
    1274        (cl_env … frame_data)
    1275        (cm_env … frame_data)
    1276        (cl_env_hyp … frame_data)
    1277        new_cl_mem
    1278        new_cm_mem
    1279        (Em … frame_data)
    1280        Hinj
    1281        (stackptr … frame_data)
    1282        ? (* (matching … frame_data) *)
    1283        (Em_fn_id … frame_data))}
    1284 [ whd #id
    1285   lapply (matching … frame_data id)
    1286   lapply (Haux id)
    1287   cases (lookup ??? id) normalize nodelta
    1288   [ #_ #H @H
    1289   | #b cases (lookup ??? id) normalize nodelta
    1290     [ #_ #H @H
    1291     | * #vartype #cltype normalize nodelta
    1292       cases vartype try // normalize nodelta #Haux
    1293       #H #v #Hload @H >(Haux ?? (refl ??) (refl ??)) @Hload
    1294     ]
    1295   ]
    1296 |
    1297 @conj try @conj try @conj try @conj try @conj try @conj try @refl
    1298 qed.*)
    1299 
    13001478lemma store_value_of_type_success_by_value :
    13011479   ∀ty, m, m', b, o, v.
     
    13361514| *: %1 #id % #Habsurd destruct (Habsurd) ]
    13371515qed.
    1338 
    1339 (* Not provable: need to relate (typeof (e=Evar id, ty)) with the type contained
    1340    in var_ty. Should be doable, but not now. *)
    1341 (*   
    1342 lemma translate_dest_IdDest_typ :
    1343   ∀vars,e,var_id,var_ty,H.
    1344     translate_dest vars e = return (IdDest vars var_id var_ty H) →
    1345     var_ty = typeof e.
    1346 #vars * #ed #ety #var_id #var_ty #H
    1347 cases ed   
    1348 [ #sz #i | #id | #e1 | #e1 | #op #e1 |#op #e1 #e2 | #cast_ty #e1
    1349 | #cond #iftrue #iffalse | #e1 #e2 | #e1 #e2 | #sizeofty | #e1 #field | #cost #e1 ]
    1350 [ 2,3,12:
    1351   [ 2,3:
    1352     whd in ⊢ ((??%?) → ?);
    1353     cases (translate_addr ??) normalize nodelta
    1354     [ 2,3: #error whd in ⊢ ((??%%) → ?); #Habsurd destruct (Habsurd)
    1355     | 1,4: #Hfoo whd in ⊢ ((??%%) → ?); #Habsurd destruct (Habsurd) ]
    1356   | 1: #H' lapply (bind2_eq_inversion ?????? H') * #vt * #t * #Eq
    1357     lapply Eq inversion vt normalize nodelta
    1358     [ 1,2: #foo #bar #Hlookup
    1359       whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
    1360     | 3: #e whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
    1361 | *: whd in ⊢ ((??%?) → ?); whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd)
    1362 normalize nodelta
    1363 [ 2:*)
    1364 
    13651516
    13661517lemma mk_offset_offv_id : ∀o. mk_offset (offv o) = o.
     
    14531604  load_value_of_type ty m b o = Some ? v.
    14541605
     1606(* Make explicit the contents of [exec_bind_parameters ????] *) 
     1607lemma exec_alloc_bind_params_same_length :
     1608  ∀e,m,m',params,vars.
     1609  exec_bind_parameters e m params vars = OK ? m' →
     1610  (params = [ ] ∧ vars = [ ]) ∨
     1611  ∃id,ty,tl_pa,v,tl_vars,b,mi.
     1612   params = 〈id,ty〉 :: tl_pa ∧
     1613   vars   = v :: tl_vars ∧
     1614   lookup ?? e id = Some ? b ∧
     1615   store_value_of_type ty m b zero_offset v = Some ? mi ∧
     1616   exec_bind_parameters e mi tl_pa tl_vars = OK ? m'.
     1617#e #m #m' #params cases params
     1618[ #vars whd in ⊢ ((??%?) → ?); cases vars normalize nodelta
     1619  [ #Heq destruct (Heq) %1 @conj try @refl
     1620  | #hd_pa #tl_pa #Habsurd destruct (Habsurd) ]
     1621| * #id #ty #tl_pa #vars
     1622  whd in ⊢ ((??%?) → ?);
     1623  cases vars normalize nodelta
     1624  [ #Habsurd destruct (Habsurd)
     1625  | #hd_val #tl_val #H
     1626    cases (bind_inversion ????? H) -H
     1627    #blo * #HA #H
     1628    cases (bind_inversion ????? H) -H
     1629    #m'' * #HB #Hexec_bind %2
     1630    %{id} %{ty} %{tl_pa} %{hd_val} %{tl_val} %{blo} %{m''}   
     1631    @conj try @conj try @conj try @conj try @refl
     1632    try @(opt_to_res_inversion ???? HA)
     1633    try @(opt_to_res_inversion ???? HB)
     1634    @Hexec_bind
     1635  ]
     1636] qed.
     1637
     1638(* Axiom-fest, with all the lemmas we need but won't have time to prove. Most of them are not too hard. *)
     1639
     1640(* The way we have of stating this is certainly not the most synthetic. The property we really need is that
     1641 * stmt_univ' is fresher than stmt_univ, which sould be trivially provable by a simple induction. *)
     1642axiom env_below_freshgen_preserved_by_translation :
     1643    ∀cl_env, alloc_type, stmt_univ, lbl_univ, lbls, flag, rettyp, s, stmt_univ', lbl_univ', cm_s, H.
     1644    env_below_freshgen cl_env alloc_type stmt_univ →
     1645    translate_statement alloc_type stmt_univ lbl_univ lbls flag rettyp s = return «〈stmt_univ', lbl_univ', cm_s〉, H» →
     1646    env_below_freshgen cl_env alloc_type stmt_univ'.
     1647
     1648axiom tmp_vars_well_allocated_preserved_by_inclusion :
     1649    ∀cm_env, cm_m, cl_m, Em, tmpenv, tmpenv'.
     1650    lset_inclusion ? tmpenv tmpenv' →
     1651    tmp_vars_well_allocated tmpenv' cm_env cm_m cl_m Em →
     1652    tmp_vars_well_allocated tmpenv cm_env cm_m cl_m Em.
     1653
     1654axiom translation_entails_ident_inclusion :
     1655    ∀alloc_type, stmt_univ, lbl_univ, lbls, flag, rettyp, stmt_univ'.
     1656    ∀cl_s, cm_s, labgen, Htrans_inv.
     1657    translate_statement alloc_type stmt_univ lbl_univ lbls flag rettyp cl_s = return «〈stmt_univ',labgen,cm_s〉,Htrans_inv» →
     1658    lset_inclusion ? (tmp_env … stmt_univ) (tmp_env … stmt_univ').
     1659
     1660(* Same remarks as above apply here too. *)
     1661(*
     1662lemma tmp_vars_well_allocated_preserved_by_translation :
     1663    ∀cm_env, alloc_type, stmt_univ, lbl_univ, lbls, flag, rettyp, stmt_univ'.
     1664    ∀Em, cm_m, cl_m, cl_s, cm_s, labgen, Htrans_inv.
     1665    translate_statement alloc_type stmt_univ lbl_univ lbls flag rettyp cl_s = return «〈stmt_univ',labgen,cm_s〉,Htrans_inv» →
     1666    tmp_vars_well_allocated (tmp_env alloc_type stmt_univ') cm_env cm_m cl_m Em →
     1667    tmp_vars_well_allocated (tmp_env alloc_type stmt_univ) cm_env cm_m cl_m Em.
     1668#cm_env #alloc_type #stmt_univ #lbl_univ #lbls #flag #rettyp #stmt_univ' #Em #cm_m #cl_m #cl_s #cm_s
     1669#labgen #Htrans_inv #Htranslate_statement #H #id #Hpresent #ty #Hexists
     1670@H lapply (translation_entails_ident_inclusion … Htranslate_statement)
     1671#H
     1672@H23*)
     1673
     1674axiom tmp_vars_well_allocated_conserved_by_frame_free :
     1675  ∀alloc_type, tmpenv, cl_env, cm_env, cm_m, cl_m, stackptr.
     1676  ∀Em, cl_ge, cm_ge, INV.
     1677  ∀Hmatching:memory_matching Em cl_ge cm_ge cl_m cm_m cl_env cm_env INV stackptr alloc_type.
     1678  tmp_vars_well_allocated tmpenv cm_env cm_m cl_m Em ->
     1679  tmp_vars_well_allocated tmpenv cm_env (free cm_m stackptr) (free_list cl_m (blocks_of_env cl_env)) Em.
     1680
     1681axiom generated_id_not_in_env :
     1682    ∀id, blo, tmp, ty.
     1683    ∀env: cl_env.
     1684    ∀alloc_type.
     1685    ∀freshgen, freshgen': tmpgen alloc_type.
     1686    env_below_freshgen env alloc_type freshgen →
     1687    lookup ?? env id = Some ? blo →
     1688    alloc_tmp alloc_type ty freshgen = 〈tmp, freshgen'〉 →
     1689    tmp ≠ id.
     1690
     1691(* This should just be lifting a lemma from positive maps to identifier maps.
     1692 * Sadly, the way things are designed requires a boring induction. *)
     1693axiom update_lookup_opt_other :
     1694  ∀b,a,t,H.
     1695  ∀b'. b ≠ b' →
     1696  lookup SymbolTag val t  b' = lookup SymbolTag val (update_present SymbolTag val t b H a) b'.
     1697 
     1698 
     1699(* NOTE: this axiom is way more general than what we need. In practice, cm_m' is cm_m after a store. *)
     1700axiom clight_cminor_cont_rel_parametric_in_mem :
     1701  ∀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.
     1702  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 →
     1703  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.
     1704
     1705(* Same remark as above. *)
     1706axiom well_allocated_preserved_by_parallel_stores :
     1707  ∀tmpenv, cm_env, cm_m, cm_m', cl_m, cl_m', Em.
     1708
     1709(* TODO: proper hypotheses (the following, commented out do not exactly fit)
     1710  (storen cm_m (mk_pointer cl_blo (mk_offset (offv zero_offset))) (fe_to_be_values (typ_of_type (typeof rhs)) cm_rhs_val)
     1711   =Some mem cm_mem_after_store_lhs)
     1712  storev (typ_of_type ty) cl_m (Vptr (mk_pointer cl_blo zero_offset)) cl_rhs_val = Some ? cl_m') *)
     1713
     1714  tmp_vars_well_allocated tmpenv cm_env cm_m  cl_m  Em →
     1715  tmp_vars_well_allocated tmpenv cm_env cm_m' cl_m' Em.
     1716
     1717(* Same remark as above. Moreover, this should be provable from memory injections. *)
     1718axiom memory_matching_preserved_by_parallel_stores :
     1719  ∀Em, cl_ge, cm_ge, cl_m, cl_m', cm_m, cm_m', cl_env, cm_env, INV, stackptr, alloc_type.
     1720  memory_matching Em cl_ge cm_ge cl_m  cm_m  cl_env cm_env INV stackptr alloc_type →
     1721  memory_matching Em cl_ge cm_ge cl_m' cm_m' cl_env cm_env INV stackptr alloc_type.
     1722 
     1723axiom clight_cminor_cont_rel_parametric_in_cm_env :
     1724∀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.
     1725∀Hpresent:present SymbolTag val cm_env var_id.
     1726clight_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 ->
     1727clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env
     1728  (update_present SymbolTag val cm_env var_id Hpresent v) cm_m
     1729  alloc_type tmpenv (*stmt_univ stmt_univ'*) rettyp cl_k cm_k cm_st.
     1730
     1731axiom tmp_vars_well_allocated_preserved_by_local_store :
     1732  ∀Em, cl_value, cm_value, lhs_ty, cl_m, cl_m', cm_m, cl_blo, tmpenv, cm_env, var_id.
     1733  ∀Hpresent:present SymbolTag val cm_env var_id.
     1734  value_eq Em cl_value cm_value →
     1735  store_value_of_type' lhs_ty cl_m 〈cl_blo, zero_offset〉 cl_value = Some ? cl_m' →
     1736  tmp_vars_well_allocated tmpenv cm_env cm_m cl_m Em →
     1737  tmp_vars_well_allocated tmpenv
     1738  (update_present ?? cm_env var_id Hpresent cm_value) cm_m
     1739   cl_m' Em.
     1740
     1741axiom memory_inj_preserved_by_local_store :
     1742∀Em, cl_ge, cm_ge, cl_m, cl_m', cm_m, cl_env, cm_env, INV, stackptr, alloc_type.
     1743 memory_matching Em cl_ge cm_ge cl_m cm_m cl_env cm_env INV stackptr alloc_type ->
     1744 memory_inj Em cl_m cm_m ->
     1745 memory_inj Em cl_m' cm_m.
     1746
     1747axiom memory_matching_preserved_by_local_store :
     1748  ∀Em, cl_ge, cm_ge, cl_m, cl_m', cm_m, cl_env, cm_env, INV, stackptr, alloc_type, cl_value, cm_value.
     1749  ∀cl_blo, var_id, lhs_ty.
     1750  ∀Hpresent:present SymbolTag val cm_env var_id. 
     1751   value_eq Em cl_value cm_value →
     1752   store_value_of_type' lhs_ty cl_m 〈cl_blo, zero_offset〉 cl_value = Some ? cl_m' →
     1753   memory_matching Em cl_ge cm_ge cl_m cm_m cl_env cm_env INV stackptr alloc_type →
     1754   memory_matching Em cl_ge cm_ge cl_m' cm_m cl_env
     1755    (update_present SymbolTag val cm_env var_id Hpresent cm_value) INV stackptr alloc_type.
     1756 
     1757lemma translate_dest_conservation :
     1758  ∀vars, e1.
     1759  ∀id, t, H.
     1760  translate_dest vars e1 = OK ? (IdDest vars id t H) →
     1761  typeof e1 = t.
     1762#vars #e1 #id #t #H #Htranslate lapply (translate_dest_id_inversion … Htranslate)
     1763#Heq >Heq in Htranslate;
     1764whd in ⊢ ((??%?) → ?);
     1765generalize in match (refl ??);
     1766generalize in ⊢ ((???%) → (??(match % with [ _ ⇒ ? | _ ⇒ ? ] ?)?) → ?); *
     1767normalize nodelta
     1768[ 2: #er #_ #Habsurd destruct (Habsurd) ]
     1769* * normalize nodelta
     1770[ #a #b #c #Habsurd
     1771| #n #t #H #Habsurd
     1772| #ty #H ]
     1773[ 1,2: destruct (Habsurd) ]
     1774cases (type_eq_dec ??) normalize nodelta
     1775#Hty #Heq destruct (Heq) >Hty @refl
     1776qed.
     1777
     1778lemma alloc_tmp_monotonic :
     1779  ∀alloc_type, ty, univ, univ', v.
     1780   alloc_tmp alloc_type ty univ = 〈v, univ'〉 →
     1781   lset_inclusion ? (tmp_env ? univ) (tmp_env ? univ').
     1782#alloc_type #ty #univ #univ' #v cases univ
     1783#u #env #Hfresh #Hyp #Halloc
     1784cases (breakup_dependent_match_on_pairs ?????? Halloc) -Halloc
     1785#v * #u' * #Heq * #Heq' normalize nodelta #Heq''
     1786destruct (Heq'')
     1787@cons_preserves_inclusion @reflexive_lset_inclusion
     1788qed.
     1789
     1790(*
     1791lemma lset_inclusion_Exists :
     1792  ∀A. ∀l1, l2: lset A.
     1793  lset_inclusion ? l1 l2 →
     1794  ∀P. Exists ? P l1 → Exists ? P l2.
     1795#A #l1 elim l1
     1796[ #l2 #Hincl #P @False_ind
     1797| #hd #tl #Hind #l2 * #Hmem #Hincl2 #P *
     1798  [ 2: #Htl @Hind assumption ]
     1799  lapply P -P
     1800  lapply Hincl2 -Hincl2
     1801  lapply Hmem -Hmem elim l2
     1802  [ @False_ind ]
     1803  #hd2 #tl2 #Hind2 *
     1804  [ #Heq destruct (Heq)
     1805    #Hincl2 #P #H %1 @H
     1806  | #Hmem #Hincl2 #P #H %2
     1807    elim tl2 in Hmem;
     1808    [ @False_ind
     1809    | #hd2' #tl2' #Hind3 *
     1810      [ #Heq destruct (Heq) %1 assumption
     1811      | #Hmem' %2 @Hind3 @Hmem' ]
     1812    ]
     1813  ]
     1814] qed.  *)
     1815
    14551816(* --------------------------------------------------------------------------- *)
    14561817(* Main simulation results                                                     *)
    1457 (* -------------------------------------------------------------------;-------- *)
     1818(* --------------------------------------------------------------------------- *)
    14581819
    14591820(* Conjectured simulation results
     
    14701831   subtrace corresponding to a measurable Clight subtrace.
    14711832 *)
    1472 
    1473  
     1833(*
     1834lemma clight_cminor_call_return :
     1835  ∀g1, g2.
     1836  ∀INV:clight_cminor_inv g1 g2.
     1837  ∀s1,s1'.
     1838  clight_cminor_rel g1 g2 INV s1 s1' →
     1839  match Clight_classify s1 with
     1840  [ cl_call ⇒ true
     1841  | cl_return ⇒ true
     1842  | _ ⇒ false ] →
     1843  ∀s2,tr. step … (pcs_exec cl_pre) g1 s1 = Value … 〈tr, s2〉 →
     1844  ∃m. after_n_steps m ?? (pcs_exec cm_pre) g2 s1' (λs.cminor_normal s) (λtr',s2'.
     1845    tr = tr' ∧
     1846    clight_cminor_rel g1 g2 INV s2 s2' ∧
     1847      (m = 0 → lex_lt (measure_Clight s2) (measure_Clight s1))
     1848  ).
     1849#g1 #g2 #INV #s1 #s1' #Hstate_rel #Hclight_class
     1850inversion Hstate_rel
     1851[ 1: (* normal *)
     1852  #cl_ge #cm_ge #INV' #cl_s
     1853  #cm_s #cl_k #cm_k #cm_st #cl_f #cm_f #rettyp
     1854  #alloc_type #cl_env #cl_m #cm_env #cm_m #stackptr #stacksize
     1855  (* introduce everything *)
     1856  #fInv #sInv #kInv #Htarget_type #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function
     1857  #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls
     1858  #flag  #Htrans_inv #Htrans_stmt #Hincl #HA #HB #HC
     1859  #HE #HF #HG #HI #HJ #HK
     1860  @(jmeq_absorb ?????) #H1 @(jmeq_absorb ?????) #H2
     1861  destruct (H1 H2)
     1862  @(jmeq_absorb ?????) #H3 @(jmeq_absorb ?????) #H4 @(jmeq_absorb ?????) #H5
     1863  destruct (H3 H4 H5)
     1864  @False_ind @Hclight_class
     1865| 5:
     1866  #cl_ge #cm_ge #INV' #cl_s
     1867  #cm_s #cl_k #cm_k #cm_st #cl_f #cm_f #rettyp
     1868  #alloc_type #cl_k #cm_k #sz #sg #cl_ty #cl_cond_desc #cl_body #entry_lab #exit_lab
     1869  #cm_cond #cm_body #cm_stack #rettyp' #kInv
     1870  (* introduce everything *)
     1871  #fInv #sInv #kInv #Htarget_type #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function
     1872  #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls
     1873  #lbl1 #lbl2 #Em #Htmp_vars #Hcharac #Hexec #Hinj #Hmatching #Hem #Hframe #Hcond_tr
     1874  #Htransl #Hex1 #Hex2 #Htransinv #Hmklabs #Htranstmt #Hincl
     1875  #Hlabdecl #Hinv1 #Hinv2 #Hfindlab
     1876  @(jmeq_absorb ?????) #H1 @(jmeq_absorb ?????) #H2
     1877  destruct (H1 H2)
     1878  @(jmeq_absorb ?????) #H3 @(jmeq_absorb ?????) #H4 @(jmeq_absorb ?????) #H5
     1879  destruct (H3 H4 H5)
     1880  @False_ind @Hclight_class
     1881| 2:
     1882  #cl_ge #cm_ge #INV' #cl_f #cm_f #cl_k #cm_k #alloc_type
     1883  #cl_env #cl_m #cm_env #cm_m #cm_st #stackptr #stacksize
     1884  #stmt_univ #Em #Htmp_vars_well_allocated #Halloc_hyp #Hcl_env_hyp
     1885  #Hinjection #Hmatching #HEm_fn_id #Hframe_spec #Hcont_rel
     1886  @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
     1887  destruct (HA HB)
     1888  @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE #_
     1889  destruct (HC HD HE)
     1890  inversion Hcont_rel
     1891  [ #kcl_ge #kcm_ge #kINV #kcl_f #kcm_f #ktarget_type #kcl_env #kcm_env #kalloc_type #kstack #Hkstack
     1892    @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
     1893    destruct (HA HB)
     1894    @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
     1895    destruct (HC HD HE)
     1896    @(jmeq_absorb ?????) #HF @(jmeq_absorb ?????) #HG @(jmeq_absorb ?????) #HH
     1897    @(jmeq_absorb ?????) #HI @(jmeq_absorb ?????) #HJ @(jmeq_absorb ?????) #HK @(jmeq_absorb ?????) #HL
     1898    destruct (HF HG HH HI HJ HK HL) #_
     1899    #s2 #tr
     1900    whd in ⊢ ((??%?) → ?); #Habsurd destruct (Habsurd)
     1901  | (* Kseq *)
     1902    #kcl_ge #kcm_ge #kINV #kcl_f #kcm_f #ktarget_type #kstack #kalloc_type #kcl_s #kcm_s
     1903    #kcl_env #kcm_env #kcl_k' #kcm_k' #kstmt_univ #kstmt_univ' #klbl_univ #klbl_univ' #klbls #kflag
     1904    * * * * #kHstmt_inv #kHlabels_translated #kHtmps_preserved
     1905    #kHreturn_ok #kHlabel_wf #kHeq_translate #kHlabel_inclusion #kHcont_rel #_
     1906    @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
     1907    destruct (HA HB)
     1908    @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
     1909    destruct (HC HD HE)
     1910    @(jmeq_absorb ?????) #HF @(jmeq_absorb ?????) #HG @(jmeq_absorb ?????) #HH @(jmeq_absorb ?????) #HI
     1911    @(jmeq_absorb ?????) #HJ @(jmeq_absorb ?????) #HK @(jmeq_absorb ?????) #HL
     1912    destruct (HF HG HH HI HJ HK HL) #_
     1913    #s2 #tr
     1914    whd in ⊢ ((??%?) → ?); #Habsurd destruct (Habsurd)
     1915  | (* *)
     1916    #kcl_ge #kcm_ge #kINV #kcl_f #kcm_f #ktarget_type #kstack #kalloc_type #kcl_env #kcm_env
     1917    #kcl_k' #kcm_k' #ksz #ksg #kcl_ty #kcl_cond_desc #kcl_body #kHeq_ty #kcm_cond #kcm_body
     1918    #kentry #kexit #kstmt_univ #kstmt_univ' #klbl_univ #klbl_univ' #klbl_univ''
     1919    #klbls #kHtranslate_inv #kHexpr_vars #kHtranslate_expr #kfInv #kHlabel_declared
     1920    #kHinv #kHmklabels #kHeq_translate #kHlabel_inclusion #kHfind_label
     1921    (*     
     1922    * * * * #kHentry_declared * * * *
     1923    * * * #kHcond_vars_declared #Hnoise #Hnoise' #Hnoise''
     1924    #kHcont_inv #kHmklabels #kHeq_translate
     1925    #kHfind_label *) #kHcont_rel #_
     1926    @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
     1927    destruct (HA HB)
     1928    @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
     1929    destruct (HC HD HE)
     1930    @(jmeq_absorb ?????) #HF @(jmeq_absorb ?????) #HG @(jmeq_absorb ?????) #HH
     1931    @(jmeq_absorb ?????) #HI @(jmeq_absorb ?????) #HJ @(jmeq_absorb ?????) #HK
     1932    @(jmeq_absorb ?????) #HL
     1933    destruct (HF HG HH HI HJ HK HL) #_
     1934    #s2 #tr
     1935    whd in ⊢ ((??%?) → ?); #Habsurd destruct (Habsurd)
     1936  ]   
     1937| 3:
     1938  #cl_ge #cm_ge #INV' #alloc_type
     1939  #cl_env #cl_m #cm_env #cm_m #cm_st #stackptr #func_univ
     1940  #cl_f #cm_f #Hglobals_fresh #Hfundef_fresh
     1941  #rettyp #cl_k #cm_k #fblock *
     1942  #Hrettyp #Hfind_funct_cl #Hfind_func_cm #Htranslate_function #Hcont_rel
     1943  #fun_id #cl_retval #cm_retval #sInv #fInv #kInv #cl_args #cm_args
     1944  @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
     1945  destruct (HA HB)
     1946  @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
     1947  destruct (HC HD HE) #_
     1948  #s2 #tr whd in ⊢ ((??%?) → ?);
     1949  @(match (exec_alloc_variables empty_env cl_m (fn_params cl_f@fn_vars cl_f))
     1950    return λx. (x = (exec_alloc_variables empty_env cl_m (fn_params cl_f@fn_vars cl_f))) → ?
     1951    with
     1952    [ mk_Prod new_cl_env cl_m_alloc ⇒ ?
     1953    ] (refl ? (exec_alloc_variables empty_env cl_m (fn_params cl_f@fn_vars cl_f))))
     1954  #Hexec_alloc_variables normalize nodelta
     1955  #Hstep
     1956  cases (bindIO_inversion ??????? Hstep) -Hstep
     1957  #cl_m_init * #Hexec_bind_parameters
     1958  whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) 
     1959  %{1} whd whd in ⊢ (??%?);
     1960  (* Alloc big chunk of data of size (f_stacksize cm_f) *)
     1961  @(match (alloc cm_m 0 (f_stacksize cm_f))
     1962    return λx. (alloc cm_m 0 (f_stacksize cm_f) = x) → ?
     1963    with
     1964    [ mk_Prod new_cm_mem new_cm_stackptr ⇒ ?
     1965    ] (refl ? (alloc cm_m 0 (f_stacksize cm_f))))
     1966  #H_cm_alloc normalize nodelta
     1967  (* Initialise CM /parameters/ *)
     1968
     1969 
     1970  %{(S (times 3 (|fn_vars|)))} -Hclight_class
     1971  lapply (exec_alloc_bind_params_same_length … Hexec_bind_parameters)
     1972  elim cl_args in Hstate_rel Hexec_alloc;
     1973  [ #Hstate_rel whd in ⊢ ((??%%) → ?);
     1974
     1975    whd in match (exec_bind_parameters ????);
     1976
     1977  exec_alloc_variables empty_env cl_m (fn_params cl_f@fn_vars cl_f) = 〈cl_env, cl_m'〉
     1978   
     1979 
     1980  lapply (let_prod_as_inversion ?????? Hstep)
     1981    @(jmeq_absorb ?????) #HF @(jmeq_absorb ?????) #HG @(jmeq_absorb ?????) #HH
     1982    @(jmeq_absorb ?????) #HI @(jmeq_absorb ?????) #HJ @(jmeq_absorb ?????) #HK
     1983    @(jmeq_absorb ?????) #HL
     1984    destruct (HF HG HH HI HJ HK HL) #_
     1985    #s2 #tr
     1986 
     1987 
     1988  #Em #Htmp_vars_well_allocated #Halloc_hyp #Hcl_env_hyp
     1989  #Hinjection #Hmatching #HEm_fn_id #Hframe_spec #Hcont_rel
     1990] qed.  *)
    14741991
    14751992lemma clight_cminor_normal :
     
    15412058     | #structname #fieldspec | #unionname #fieldspec | #id ]     
    15422059     #Hlabels_translated #Htmps_preserved
    1543      #Hreturn_ok #Hlabel_wf #Htranslate #Hlabel_inclusion
     2060     #Hreturn_ok #Hlabel_wf #Htranslate #Hlabel_inclusion #tmpenv #Htmpenv
    15442061     #Hcont_rel
    1545      #Em #Htmp_vars_well_allocated #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id
    1546      #Hframe_spec
     2062     #Em #Htmp_vars_well_allocated
     2063     #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id
     2064     #Hframe_spec #Henv_below
    15472065     @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
    15482066     destruct (HA HB)
    15492067     @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE #_
    1550      destruct (HC HD HE) 
    1551      lapply Htranslate -Htranslate 
     2068     destruct (HC HD HE)
     2069     lapply Htranslate -Htranslate
    15522070     [ 1: generalize in match (conj ????); #Hugly_inv
    15532071     | 2: generalize in match (conj ????); #Hugly_inv
     
    16372155            @(CMR_normal … Htrans_body) try assumption
    16382156            @(ClCm_cont_while … (sym_eq … Hmk_label_eq) … Htrans_body) try assumption
    1639             [ 1,6,11,16:
    1640               @refl
    1641             | 2,3,7,8,12,13,17,18:
    1642               >CMcast_identity try assumption
    1643             | 4,9,14,19:
     2157            try @refl
     2158            [ 1,4,7,10: @eq_to_jmeq assumption
     2159            | 2,5,8,11:
    16442160                 @conj try assumption @conj @conj try assumption @conj @conj try assumption
    16452161                 try @conj try assumption try @conj try assumption
    16462162                 try @conj try assumption try @conj try assumption
    1647             | 5,10,15,20: (* find_label_always *)
    1648                  (* TODO /!\ we need to find a clever way to prove this. *)
     2163            | *: (* find_label_always *)
     2164                 (* TODO /!\ implement necessary invariant on label lookup *)
    16492165                 @cthulhu
    16502166            ]
     
    16762192       @conj try @conj try @conj
    16772193       [ 1,4,7,10: normalize >append_nil >append_nil @refl
    1678        | 2,5,8,11: 
    1679           @(CMR_normal … Htranslate_function … DoNotConvert … Hcont_rel) try assumption
    1680           [ 2,4,6,8: @refl | *: ]
     2194       | 2,5,8,11:
     2195          @(CMR_normal … Htranslate_function … DoNotConvert) try assumption
     2196          try @refl try @(env_below_freshgen_preserved_by_translation … Henv_below Htrans_body)
    16812197       | *: #Habsurd destruct (Habsurd) ]
    16822198   ]
     
    16902206     (* generalize away ugly proof *)
    16912207     generalize in ⊢ (∀_:(???(??(????%))).?); #Hugly
    1692      #Htranslate #Hlabel_inclusion #Hcont_rel #Em
     2208     #Htranslate #Hlabel_inclusion #tmpenv #Htmpenv #Hcont_rel #Em
    16932209     #Htmp_vars_well_allocated
    16942210     #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id
    1695      #Hframe_spec
     2211     #Hframe_spec #Henv_below
    16962212     @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
    16972213     destruct (HA HB)
     
    17192235       #Hdest cases (bind_inversion ????? Hdest) -Hdest #dest *
    17202236       inversion dest normalize nodelta
    1721        [ (* register dest *) #var_id #var_ty #His_local @(jmeq_absorb ?????) #Hdest       
     2237       [ (* register dest *) #var_id #var_ty #His_local @(jmeq_absorb ?????) #Hdest
    17222238         #Htranslate_dest whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
    17232239         (* make explicit the nature of lhs, allowing to prove that no trace is emitted *)
     
    17342250          generalize in ⊢ ((??(??(????%))?) → ?); #Hugly2
    17352251          whd in ⊢ ((???%) → ?); #Heq destruct (Heq) ]
     2252     (* Now, execute the Clight call *)
    17362253     #s2 #tr #Htranslate
    17372254     cases (bindIO_inversion ??????? Htranslate) -Htranslate *
    1738      #func_ptr_val #func_trace * #Hexec_func_ptr normalize nodelta
     2255     #CL_callee_val #CL_callee_trace * #Hexec_CL_callee normalize nodelta
    17392256     whd in ⊢ ((???%) → ?); #Htranslate
    17402257     cases (bindIO_inversion ??????? Htranslate) -Htranslate *
    1741      #args_values #args_trace * #Hexec_arglist #Htranslate
     2258     #CL_args #CL_args_trace * #Hexec_CL_args #Htranslate
    17422259     cases (bindIO_inversion ??????? Htranslate) -Htranslate
    1743      * #cl_fundef #cl_fun_id * #Hfind_funct
     2260     * #CL_callee_fundef #CL_callee_id * #Hfind_funct
     2261     (* We've got the CL fundef. Extract a function pointer out of it. *)
    17442262     lapply (opt_to_io_Value ?????? Hfind_funct) -Hfind_funct #Hfind_funct
    17452263     cases (find_funct_inversion ???? Hfind_funct)
    1746      #func_ptr * * * #Hfunc_ptr_eq destruct (Hfunc_ptr_eq)
    1747      #Hpoff_eq_zero #Hregion_is_code
    1748      * #block_id * #Hblock_id_neg #Hlookup
     2264     #CL_callee_ptr * * * #HCL_callee_eq destruct (HCL_callee_eq)
     2265     (* Done. Now stash the resulting properties of this pointer in the context. *)
     2266     #HCL_callee_ptr_offset_eq_zero #HCL_callee_ptr_region_eq_Code
     2267     (* Some more properties, that should stay hidden. XXX we discard them, this should not hinder the proof *)     
     2268     * #block_id * #Hblock_id_neg #Hlookup -Hlookup -Hblock_id_neg -block_id
     2269     (* Now, break up a safety check for the type of the function and finally, execute the
     2270      * CL lvalue supposed to store the result of the function call. This will yield a pointer
     2271      * that will be stored in the Callstate, until the function call returns and we store te
     2272      * result inside it. Of course, this does not apply to the case wich returns void. *)
    17492273     #Htranslate
    17502274     cases (bindIO_inversion ??????? Htranslate) -Htranslate #Htype_of_fundef *
    17512275     #Hassert_type_eq
    1752      [ 1,2: #Htranslate
    1753             cases (bindIO_inversion ??????? Htranslate) -Htranslate * *
    1754             #lblock #loffset #ltrace *
    1755             whd in ⊢ ((???%) → (???%) → ?);
    1756             [ >Hlhs_eq #Hexec_lvalue
    1757               cut (ltrace = [])
    1758               [ lapply (res_to_io ????? Hexec_lvalue)
     2276     [ 1,2: (* Cases where we return something. *)
     2277            #Htranslate
     2278            cases (bindIO_inversion ??????? Htranslate) -Htranslate * *
     2279            #CL_lvalue_block #CL_lvalue_offset #CL_lvalue_trace *
     2280            whd in ⊢ ((???%) → (??%%) → ?);
     2281            [ >Hlhs_eq #HCL_exec_lvalue
     2282              (* The trace is empty since we execute a variable *)
     2283              cut (CL_lvalue_trace = [])
     2284              [ lapply (res_to_io ????? HCL_exec_lvalue)
    17592285                #H' whd in H':(??%?); cases (lookup ????) in H'; normalize nodelta
    17602286                [ 2: #b #Heq destruct (Heq) @refl
     
    17622288                  whd in H28:(???%); destruct (H28) @refl ]
    17632289              ] #H destruct (H)
    1764             | #Hexec_lvalue ]
     2290            | #HCL_exec_lvalue ]
    17652291     | 3: ]
    17662292     whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
    1767      [ 1: %{1} whd whd in ⊢ (??%?); normalize nodelta
    1768      | 2: (* Execute Cminor part: evaluate lhs, evaluate assign *)
     2293     (* We have reached the final Clight state. Now execute the Cminor transalted code. *)
     2294     [ 1: (* Return to a variable *)
     2295          %{1} whd whd in ⊢ (??%?); normalize nodelta
     2296     | 2: (* Return to memory location. Need to create a tmp CM local variable to store the
     2297           * lvalue ptr (otherwise trace does not match CL). *)
    17692298          %{5} whd whd in ⊢ (??%?); normalize nodelta
    17702299          whd in match (eval_expr ???????);
    17712300          whd in match (m_bind ?????);
     2301          (* Evalue Cminor lvalue. Need to feed some invariants to the simulation lemma, that
     2302           * we bake here and now. *)
    17722303          cut (expr_vars ASTptr cm_expr
    17732304                  (λid:ident.λty:typ.present SymbolTag val cm_env id))
    17742305          [ cases sInv * * * * * * * #_ #H #_ #_ #_ @H ] #Hexpr_vars_cut
    1775           lapply (translate_dest_MemDest_simulation … Htranslate_dest Hexec_lvalue)
     2306          (* Apply simulation lemma for lvalues *)
     2307          lapply (translate_dest_MemDest_simulation … Htranslate_dest HCL_exec_lvalue)
    17762308          try assumption try @refl
    1777           * #cm_val_tmp * #Heval_expr_tmp >Heval_expr_tmp #Hvalue_eq
     2309          * #CM_lvalue * #HCM_eval_lvalue >HCM_eval_lvalue #Hvalue_eq_lvalues
    17782310          normalize nodelta generalize in match (proj1 ???); #Htmp_var_present
    1779           cases (value_eq_ptr_inversion … Hvalue_eq) #cm_ptr * #Hcm_val_tmp #Hcm_ptr_translation
    1780           >Hcm_val_tmp
    1781           lapply (Htmp_vars_well_allocated … tmp_var Htmp_var_present (Tpointer (typeof lhs)) ? (Vptr cm_ptr) ?)
    1782           [ 2: @(alloc_tmp_in_genlist … (sym_eq ??? Heq_alloc_tmp) (sym_eq ??? Heq_alloc_tmp'))
    1783           | 1: normalize cases cm_ptr #b #o %3 ]
    1784           * #cm_mem_after_store * #Hstorev #Hnew_inj >Hstorev
     2311          (* Make explicit the fact that the CM lvalue is a pointer *)
     2312          cases (value_eq_ptr_inversion … Hvalue_eq_lvalues) #CM_lvalue_ptr * #HCM_value_ptr_eq #HCM_lvalue_ptr_trans
     2313          >HCM_value_ptr_eq
     2314          lapply (Htmp_vars_well_allocated … tmp_var Htmp_var_present (Tpointer (typeof lhs)) ? (Vptr CM_lvalue_ptr) ?)
     2315          [ 1: normalize cases CM_lvalue_ptr #b #o %3
     2316          | 2: lapply (alloc_tmp_in_genlist … (sym_eq ??? Heq_alloc_tmp) (sym_eq ??? Heq_alloc_tmp'))
     2317               #Hexists' @(lset_inclusion_Exists … Hexists' Htmpenv) 
     2318          ]
     2319          * #CM_mem_after_store * #Hstorev #Hnew_inj >Hstorev
    17852320          whd in match (m_bind ?????); normalize nodelta
    17862321          whd whd in ⊢ (??%?); normalize nodelta
    1787 (*          cases (update_clight_cminor_data_cm … frame_ … Hnew_inj)
    1788           try assumption #frame_data'
    1789           * * * * * #Halloctype_eq_frame_data #Hcl_env_eq_frame_data #Hcm_env_eq_frame_data
    1790           #Hstackptr_eq_frame_data #Hcl_m_eq_frame_data #Hcm_m_eq_frame_data *)
    17912322     | 3: %{1} whd whd in ⊢ (??%?); normalize nodelta
    17922323     ]
    1793     (* execute Cminor part *)
     2324    (* cleanup ugliness *)
    17942325    [ 1: generalize in match (proj2 (present ????) (expr_vars ???) (proj1 ???));
    17952326    | 2: generalize in match (proj2 (present ????) (expr_vars ???) (proj1 ???));
     
    18042335                @Hexpr_vars_present_ef' ]
    18052336       #Hexpr_vars_present_ef
    1806        lapply (Hsim_expr … Htranslate_ef … Hexpr_vars_present_ef … Hexec_func_ptr)
     2337       lapply (Hsim_expr … Htranslate_ef … Hexpr_vars_present_ef … Hexec_CL_callee)
    18072338       -Hsim_expr * #cm_func_ptr_val * #Heval_func #Hvalue_eq_func
    18082339       cut (eval_expr cm_ge ASTptr ef' cm_env Hexpr_vars_present_ef'
    1809              stackptr cm_m = OK (trace×val) 〈func_trace,cm_func_ptr_val〉)
     2340             stackptr cm_m = OK (trace×val) 〈CL_callee_trace,cm_func_ptr_val〉)
    18102341       [ 1,3:
    18112342         lapply Heq_ef_ef' lapply Heval_func lapply Hexpr_vars_ef lapply Hexpr_vars_local_ef'
     
    18152346       -Heval_func #Heval_func >Heval_func
    18162347    | 2: (* treat case 2 as special, since the type differs slightly *)
    1817        cases (eval_expr_sim … INV' … Halloc_hyp ? cm_env Hcl_env_hyp … Hnew_inj stackptr Hmatching)
     2348       letin cm_env' ≝ (update_present SymbolTag val cm_env tmp_var Htmp_var_present (Vptr CM_lvalue_ptr))
     2349       cut (memory_matching Em cl_ge cm_ge cl_m cm_m cl_env cm_env' INV' stackptr alloc_type)
     2350     (*  cut (memory_matching Em cl_ge cm_ge cl_m CM_mem_after_store cl_env cm_env' INV' stackptr alloc_type) *)
     2351       [ (* Proving preservation of the memory matching under store in "new" cminor memory zone.
     2352            Use the property that the ident [tmp_var] is not in the clight env. *)
     2353         #id lapply (Hmatching id)
     2354         @(match (lookup ??? id)
     2355           return λx. (lookup ??? id = x) → ?
     2356           with
     2357           [ None ⇒ λHeq_lookup. ?
     2358           | Some blo ⇒ λHeq_lookup. ?
     2359           ] (refl ? (lookup ??? id)))
     2360         [ 1: #H @H ] normalize nodelta         
     2361         cases (lookup ??? id) normalize nodelta
     2362         [ 1: #H @H ] * #var_ty #cl_ty cases var_ty normalize nodelta
     2363         [ #r #H @H
     2364         | #n #H @H
     2365         | #H #v #Hload_value_of_type lapply (H ? Hload_value_of_type)
     2366           * #v' * #Hlookup_cm #Hvalue_eq %{v'} @conj try @Hvalue_eq
     2367           lapply (alloc_tmp_env_invariant ?????? (sym_eq ??? Heq_alloc_tmp) Henv_below) #Henv_below'
     2368           lapply (generated_id_not_in_env ???????? Henv_below' … Heq_lookup (sym_eq ??? Heq_alloc_tmp'))
     2369           #Hneq <(update_lookup_opt_other … (Vptr CM_lvalue_ptr) … cm_env … Htmp_var_present … Hneq)
     2370           assumption ] ] #Hmatching'
     2371       cases (eval_expr_sim … INV' … Halloc_hyp ? cm_env' Hcl_env_hyp … Hinjection stackptr Hmatching')
    18182372       #Hsim_expr #_
    18192373       generalize in match (proj2 ???); #Hall_present
     
    18212375       generalize in match (proj2 ???); #Hstore_inv
    18222376       generalize in match (conj ????); #Hstmt_inv
    1823        cut (eval_expr cm_ge ? ef' cm_env ? stackptr cm_m =
    1824             (eval_expr cm_ge ASTptr ef' cm_env ? stackptr cm_m)) try assumption try @refl
    1825        #Heval_expr_rewrite >Heval_expr_rewrite -Heval_expr_rewrite
    1826        lapply (Hsim_expr … Htranslate_ef … (Vptr func_ptr) func_trace ??)       
     2377(*       cut (eval_expr cm_ge ? ef' cm_env' ? stackptr cm_m =
     2378            (eval_expr cm_ge ASTptr ef' cm_env' ? stackptr cm_m)) try assumption try @refl
     2379       #Heval_expr_rewrite >Heval_expr_rewrite -Heval_expr_rewrite *)
     2380       lapply (Hsim_expr … Htranslate_ef … (Vptr CL_callee_ptr) CL_callee_trace ??)
    18272381       try assumption
    18282382       [ lapply Hexpr_vars_present_ef' lapply Heq_ef_ef' lapply Hexpr_vars_ef lapply Hexpr_vars_local_ef'
    18292383         lapply ef >Htyp_equality_ef #ef #HA #HB @(jmeq_absorb ?????) #Heq destruct (Heq) #x @x ]
    1830        * #cm_func_ptr_val * #Heval_func_cm #Hvalue_eq_func
     2384       * #CM_callee_ptr * #Heval_func_cm #Hvalue_eq_func
    18312385       (* And some more shuffling types around to match the goal *)
    1832        cut (eval_expr cm_ge ? ef' cm_env Hexpr_vars_present_ef' stackptr cm_mem_after_store = OK ? 〈func_trace,cm_func_ptr_val〉)
     2386       cut (eval_expr cm_ge ? ef' cm_env' Hexpr_vars_present_ef' stackptr cm_m = OK ? 〈CL_callee_trace,CM_callee_ptr〉)
    18332387       [ lapply Heval_func_cm -Heval_func_cm
    18342388         generalize in ⊢ ((??(?????%??)?) → ?);
     
    18452399    #Htranslate_fundef #Hfind_funct_cm
    18462400    lapply (value_eq_ptr_inversion … Hvalue_eq_func) * #cm_func_ptr * #Hcm_func_ptr
    1847     whd in ⊢ ((??%?) → ?); cases func_ptr in Hfind_funct Hfind_funct_cm Hregion_is_code Hpoff_eq_zero;
     2401    whd in ⊢ ((??%?) → ?);
     2402    cases CL_callee_ptr in Hfind_funct Hfind_funct_cm HCL_callee_ptr_region_eq_Code HCL_callee_ptr_offset_eq_zero;
    18482403    #cm_block #cm_off #Hfind_funct #Hfind_funct_cm #Hregion_is_code #Hpoff_eq_zero destruct (Hpoff_eq_zero)
    18492404    whd in ⊢ ((??%?) → ?);
    18502405    [ 1,2: >(HEm_fn_id … cm_block Hregion_is_code)
    18512406    | 3: >(HEm_fn_id … cm_block Hregion_is_code) ]
    1852     normalize nodelta cases cm_func_ptr in Hcm_func_ptr; #cm_block' #cm_off'
     2407    normalize nodelta
     2408    cases cm_func_ptr in Hcm_func_ptr; #cm_block' #cm_off'
    18532409    #Hcm_func_ptr #Heq destruct (Hcm_func_ptr Heq)
    18542410    [ 1,2: >addition_n_0 >mk_offset_offv_id
     
    18682424      | 3: cases sInv * * normalize nodelta * #_ #_ #Hall #_ #_ @Hall ]
    18692425      #Hall
    1870       cases (eval_exprlist_simulation …  Halloc_hyp Hcl_env_hyp Hinjection Hmatching ???? Hexec_arglist Hargs_spec Hall)
     2426      cases (eval_exprlist_simulation …  Halloc_hyp Hcl_env_hyp Hinjection Hmatching ???? Hexec_CL_args Hargs_spec Hall)
    18712427      #cm_values * #Hcm_exec_list #Hcl_cm_values_eq >Hcm_exec_list
    18722428    | 3:
    1873       (* Arrrgh *)
    1874       lapply (eval_exprlist_simulation …  Halloc_hyp Hcl_env_hyp Hnew_inj ????? Hexec_arglist Hargs_spec ?)
    1875       try assumption *
    1876       #cm_values * #Hcm_exec_list #Hcl_cm_values_eq >Hcm_exec_list
     2429      lapply (eval_exprlist_simulation …  Halloc_hyp Hcl_env_hyp Hinjection ????? Hexec_CL_args Hargs_spec ?)
     2430      try assumption
     2431      * #cm_values * #Hcm_exec_list #Hcl_cm_values_eq >Hcm_exec_list
    18772432    ]
    18782433    whd in match (m_bind ?????); normalize nodelta whd @conj
    18792434    [ 2,4,6: #Habsurd destruct (Habsurd) ]
    18802435    @conj
    1881     [ 1,3,5: normalize try @refl
    1882              >append_nil >append_nil @refl ]
     2436    [ 1,3,5: normalize try @refl >append_nil >append_nil @refl ]
    18832437    [ 1: generalize in match (proj1 ? (expr_vars ???) (proj1 ???)); #Hugly_pres
    18842438    | 2: generalize in match (proj1 ? (expr_vars ???) (proj1 ???)); #Hugly_pres
    18852439    | 3: ]
    1886 (*    [ 3: >addition_n_0 ]*)
    1887     [ 1,2: (* no return or return to CM local variable *)
    1888            @(CMR_call_nostore … tmp_u) try assumption
    1889            [ 2,4: (* TODO: prove matching between CL and CM function ids *)
    1890                   @cthulhu
     2440    [ 3: @(CMR_call … Htranslate_function … Hinjection … Hmatching … HEm_fn_id) try assumption
     2441         lapply (alloc_tmp_monotonic … (sym_eq ??? Heq_alloc_tmp)) #Hincl1
     2442         lapply (alloc_tmp_monotonic … (sym_eq ??? Heq_alloc_tmp')) #Hincl2
     2443         lapply (transitive_lset_inclusion … Hincl1 Hincl2) #Hincl3
     2444         try /2 by transitive_lset_inclusion/
     2445         lapply Htranslate_fundef -Htranslate_fundef
     2446         lapply Hfundef_fresh_for_tmp_u -Hfundef_fresh_for_tmp_u
     2447         cases CL_callee_fundef normalize nodelta
     2448         [ 1: #cl_called_f #Hfundef_fresh_for_tmp_u #Htranslate_fundef @ClCm_cont_call_store
     2449         | 2: #id #tl #ty #Hfd_fresh
     2450              whd in ⊢ ((??%?) → ?); #Heq destruct (Heq) normalize nodelta @I ]
     2451    | 1,2: (* no return or return to CM local variable *)
     2452           @(CMR_call … Htranslate_function … Hinjection … Hmatching … HEm_fn_id) try assumption
     2453           cases CL_callee_fundef in Hfundef_fresh_for_tmp_u Htranslate_fundef; normalize nodelta
     2454           [ 1,3: (* Internal case *)
     2455             #cl_called_f #Hfundef_fresh_for_tmp_u #Htranslate_fundef
     2456             whd nodelta in match (typeof ?);
     2457             [ <(translate_dest_conservation … Htranslate_dest)
     2458               @ClCm_cont_call_nostore normalize nodelta
     2459               %{CL_lvalue_block} %{CL_lvalue_offset} %{(typeof lhs)} %{var_id}
     2460               @conj @refl
     2461             | @ClCm_cont_call_nostore normalize nodelta @I ]
     2462           | 2,4: #fid #tl #ty #H1 #H2
     2463             whd in H2:(??%?); destruct (H2) @I
    18912464           ]
    1892            lapply Hfind_funct
    1893            lapply Hfind_funct_cm
    1894            lapply Htranslate_fundef
    1895            lapply Hfundef_fresh_for_tmp_u
    1896            lapply Hassert_type_eq
    1897            lapply Htype_of_fundef
    1898            lapply Hlookup
    1899            cases cl_fundef
    1900            [ 2,4: #id #typel #ty #HA #HB #HC #HD #HE #HF #HG @I
    1901            | 1,3: #f #HA #HB #HC #HD #HE #HF #HG normalize nodelta
    1902                   @conj try @conj try @conj try assumption ]
    1903     | 3: (* type mismatch *)
    1904          @(CMR_call_store … tmp_u) try assumption
    1905          [ 2: (* TODO: prove matching between CL and CM function ids *)
    1906               @cthulhu ]
    1907          lapply Hfind_funct
    1908          lapply Htranslate_fundef
    1909          lapply Hfundef_fresh_for_tmp_u
    1910          lapply Hassert_type_eq
    1911          lapply Htype_of_fundef
    1912          lapply Hlookup
    1913          cases cl_fundef
    1914          [ 2: #id #typel #ty #HA #HB #HC #f #HD #HE @I ]
    1915          #f #HA #HB #HC #HD #HE #HF normalize nodelta @conj try @conj try @conj
    1916          try assumption
    19172465    ]
    19182466| 1: (* Skip *)
     
    19262474    #Hreturn_ok #Hlabel_wf generalize in match (conj ????); #Hugly
    19272475    whd in ⊢ ((??%?) → ?); #Heq_translate #Hlabel_inclusion
    1928     #Hcont_rel
     2476    #tmpenv #Htmpenv #Hcont_rel
    19292477    lapply Heq_translate -Heq_translate
    1930     lapply Hugly -Hugly 
    1931     lapply Hlabel_wf -Hlabel_wf 
     2478    lapply Hugly -Hugly
     2479    lapply Hlabel_wf -Hlabel_wf
    19322480    lapply Hreturn_ok -Hreturn_ok
    1933     lapply Htmps_preserved -Htmps_preserved 
     2481    lapply Htmps_preserved -Htmps_preserved
    19342482    lapply Hlabels_translated -Hlabels_translated
    1935     lapply Hstmt_inv -Hstmt_inv 
     2483    lapply Hstmt_inv -Hstmt_inv
    19362484    lapply Htranslate_function -Htranslate_function
    1937     lapply Hfresh_globals -Hfresh_globals 
     2485    lapply Hfresh_globals -Hfresh_globals
    19382486    lapply Hfresh_function -Hfresh_function
    1939     lapply Htarget_type -Htarget_type 
    1940     lapply kInv -kInv 
    1941     lapply sInv -sInv 
     2487    lapply Htarget_type -Htarget_type
     2488    lapply kInv -kInv
     2489    lapply sInv -sInv
    19422490    lapply fInv -fInv
    1943     lapply stmt_univ -stmt_univ
     2491    lapply stmt_univ -stmt_univ   
     2492    lapply Htmpenv -Htmpenv
    19442493    lapply stmt_univ' -stmt_univ'
    19452494    lapply Hlabel_inclusion -Hlabel_inclusion
     
    19482497    [ (* Kstop continuation *)
    19492498      (* simplifying the goal using outcome of the inversion *)
    1950       #kcl_ge #kcm_ge #kINV #kcl_f #kcm_f #ktarget_type #kcl_env #kcm_env #kalloc_type #kstack #Hkstack
     2499      #kcl_ge #kcm_ge #kINV #kcl_f #kcm_f #ktarget_type #kcl_env #kcm_env #kcm_m #kalloc_type #ktmpenv #kstack #Hkstack
    19512500      @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
    19522501      destruct (HA HB)
    19532502      @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
    19542503      destruct (HC HD HE)
    1955       @(jmeq_absorb ?????) #HF @(jmeq_absorb ?????) #HG @(jmeq_absorb ?????) #HH
    1956       @(jmeq_absorb ?????) #HI @(jmeq_absorb ?????) #HJ @(jmeq_absorb ?????) #HK @(jmeq_absorb ?????) #HL
    1957       destruct (HF HG HH HI HJ HK HL) #_
     2504      @(jmeq_absorb ?????) #HF @(jmeq_absorb ?????) #HG @(jmeq_absorb ?????) #HH @(jmeq_absorb ?????) #HI
     2505      destruct (HF HG HH HI)
     2506      @(jmeq_absorb ?????) #HJ @(jmeq_absorb ?????) #HK @(jmeq_absorb ?????) #HL @(jmeq_absorb ?????) #HM
     2507       @(jmeq_absorb ?????) #HN
     2508      destruct (HJ HK HL HM HN) #_
    19582509      (* re-introduce everything *)
    19592510      #Hlabel_inclusion
    1960       #stmt_univ' #stmt_univ #fInv #sInv #kInv #Htarget_type #Hfresh_function #Hfresh_globals
    1961       #Htranslate_function #Hstmt_inv #Hlabels_translated #Htmps_preserved #Hreturn_ok #Hlabel_wf
     2511      #stmt_univ' #Htmpenv #stmt_univ #fInv #sInv #kInv #Htarget_type #Hfresh_function #Hfresh_globals
     2512      #Htranslate_function #Hstmt_inv #Hlabels_translated #Htmps_preserved
     2513      #Hreturn_ok #Hlabel_wf
    19622514      #Hugly generalize in match (conj ????); #Hugly'
    19632515      (* reduce statement translation function *)
     
    19652517      (* In this simple case, trivial translation *)
    19662518      destruct (Heq_translate)
    1967       #Em #Htmp_vars_well_allocated #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id #Hframe_spec
     2519      #Em #Htmp_vars_well_allocated
     2520      #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id #Hframe_spec #Henv_below
    19682521      @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
    19692522      destruct (HA HB)
     
    19792532      [ 2: #Habsurd destruct (Habsurd) ]
    19802533      (* Use the memory injection stuff to produce a new memory injection *)
    1981       cut (memory_inj Em (free_list cl_m (blocks_of_env kcl_env)) (free cm_m stackptr))
    1982       [ @(freelist_memory_inj_m1_m2 Em cl_m cm_m
     2534      cut (memory_inj Em (free_list cl_m (blocks_of_env kcl_env)) (free kcm_m stackptr))
     2535      [ @(freelist_memory_inj_m1_m2 Em cl_m kcm_m
    19832536            (free_list cl_m (blocks_of_env kcl_env))
    1984             (free cm_m stackptr) Hinjection (blocks_of_env kcl_env) stackptr ? (refl ??) (refl ??))
     2537            (free kcm_m stackptr) Hinjection (blocks_of_env kcl_env) stackptr ? (refl ??) (refl ??))
    19852538        assumption ]
    19862539      #Hinjection'
    1987       @(CMR_return … Halloc_hyp Hcl_env_hyp … Hinjection') try assumption
     2540      @(CMR_return … Kend … Halloc_hyp Hcl_env_hyp … Hinjection') try assumption
    19882541      [ 2: #b lapply (Hmatching b)
    19892542           cases (lookup ?? kcl_env b) normalize nodelta
     
    19972550             ]
    19982551           ]
    1999       | 1: (* TODO: lemma *) @cthulhu
    2000       ] 
     2552      | 1: @(tmp_vars_well_allocated_conserved_by_frame_free … Hmatching … Htmp_vars_well_allocated)
     2553      | 3: @ClCm_cont_stop @Hkstack
     2554      ]
    20012555    | (* Kseq *)
    2002       #kcl_ge #kcm_ge #kINV #kcl_f #kcm_f #ktarget_type #kstack #kalloc_type #kcl_s #kcm_s
    2003       #kcl_env #kcm_env #kcl_k' #kcm_k' #kstmt_univ #kstmt_univ' #klbl_univ #klbl_univ' #klbls #kflag
     2556      #kcl_ge #kcm_ge #kINV #kcl_f #kcm_f #ktarget_type #kstack #kalloc_type #ktmpenv #kcl_s #kcm_s
     2557      #kcl_env #kcm_env #kcm_m #kcl_k' #kcm_k' #kstmt_univ #kstmt_univ' #klbl_univ #klbl_univ' #klbls #kflag
    20042558      * * * * #kHstmt_inv #kHlabels_translated #kHtmps_preserved
    2005       #kHreturn_ok #kHlabel_wf #kHeq_translate #kHlabel_inclusion #kHcont_rel #_
     2559      #kHreturn_ok #kHlabel_wf #kHeq_translate #kHlabel_inclusion #kHident_inclusion #kHcont_rel #_
    20062560      @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
    20072561      destruct (HA HB)
     
    20092563      destruct (HC HD HE)
    20102564      @(jmeq_absorb ?????) #HF @(jmeq_absorb ?????) #HG @(jmeq_absorb ?????) #HH @(jmeq_absorb ?????) #HI
    2011       @(jmeq_absorb ?????) #HJ @(jmeq_absorb ?????) #HK @(jmeq_absorb ?????) #HL
    2012       destruct (HF HG HH HI HJ HK HL) #_
     2565      destruct (HF HG HH HI)
     2566      @(jmeq_absorb ?????) #HJ @(jmeq_absorb ?????) #HK @(jmeq_absorb ?????) #HL @(jmeq_absorb ?????) #HM
     2567      @(jmeq_absorb ?????) #HN
     2568      destruct (HJ HK HL HM HN) #_
    20132569      #Hlabel_inclusion
    2014       #stmt_univ' #stmt_univ #fInv #sInv #kInv #Htarget_type #Hfresh_function #Hfresh_globals
     2570      #stmt_univ' #Htmpenv #stmt_univ #fInv #sInv #kInv #Htarget_type #Hfresh_function #Hfresh_globals
    20152571      #Htranslate_function #Hstmt_inv #Hlabels_translated #Htmps_preserved #Hreturn_ok #Hlabel_wf
    20162572      #Hugly generalize in match (conj ????); #Hugly'
    20172573      (* In this simple case, trivial translation *)
    20182574      #Heq_translate destruct (Heq_translate) #Em
    2019       #Htmp_vars_well_alloc #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id #Hframe_spec
     2575      #Htmp_vars_well_alloc
     2576      #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id #Hframe_spec #Henv_below
    20202577      @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
    20212578      destruct (HA HB)
     
    20252582      %{1} whd @conj [ 2: #Habsurd destruct (Habsurd) ] @conj try @refl
    20262583      (* close simulation *)
    2027       @(CMR_normal … kHeq_translate … Hinjection … Hmatching) try assumption
    2028       (* TODO wrap this up properly, by adding some invariant or by threading stmt_univ' into the cont *)
    2029       @cthulhu
    2030       (* TODO: lemma allowing to prove this from [Htmp_vars_well_alloc] + tmp_gen inclusion *)
     2584      @(CMR_normal … kHeq_translate … kHcont_rel … Hinjection … Hmatching) try assumption
     2585      (* TODO Invariant on env_below_freshgen *)
     2586       @cthulhu
    20312587    | (* Kwhile continuation *)
    2032       #kcl_ge #kcm_ge #kINV #kcl_f #kcm_f #ktarget_type #kstack #kalloc_type #kcl_env #kcm_env
     2588      #kcl_ge #kcm_ge #kINV #kcl_f #kcm_f #ktarget_type #kstack #kalloc_type #ktmpenv #kcl_env #kcm_env #kcm_m
    20332589      #kcl_k' #kcm_k' #ksz #ksg #kcl_ty #kcl_cond_desc #kcl_body #kHeq_ty #kcm_cond #kcm_body
    20342590      #kentry #kexit #kstmt_univ #kstmt_univ' #klbl_univ #klbl_univ' #klbl_univ''
    20352591      #klbls #kHtranslate_inv #kHexpr_vars #kHtranslate_expr #kfInv #kHlabel_declared
    2036       #kHinv #kHmklabels #kHeq_translate #kHlabel_inclusion #kHfind_label
     2592      #kHinv #kHmklabels #kHeq_translate #kHlabel_inclusion #kHident_inclusion #kHfind_label
    20372593      (*     
    20382594      * * * * #kHentry_declared * * * *
     
    20462602      @(jmeq_absorb ?????) #HF @(jmeq_absorb ?????) #HG @(jmeq_absorb ?????) #HH
    20472603      @(jmeq_absorb ?????) #HI @(jmeq_absorb ?????) #HJ @(jmeq_absorb ?????) #HK
    2048       @(jmeq_absorb ?????) #HL
    2049       destruct (HF HG HH HI HJ HK HL) #_
     2604      @(jmeq_absorb ?????) #HL @(jmeq_absorb ?????) #HM @(jmeq_absorb ?????) #HN
     2605      destruct (HF HG HH HI HJ HK HL HM HN) #_
    20502606      #Hlabel_inclusion
    2051       #stmt_univ' #stmt_univ #fInv #sInv #kInv #Htarget_type #Hfresh_function #Hfresh_globals
     2607      #stmt_univ' #Htmpenv #stmt_univ #fInv #sInv #kInv #Htarget_type #Hfresh_function #Hfresh_globals
    20522608      #Htranslate_function #Hstmt_inv #Hlabels_translated #Htmps_preserved #Hreturn_ok #Hlabel_wf
    20532609      #Hugly
     
    20552611      (* In this simple case, trivial translation *)
    20562612      #Heq_translate destruct (Heq_translate)
    2057       #Em #Htmp_vars_well_allocated #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching
    2058       #HEm_fn_id #Hframe_spec
     2613      #Em #Htmp_vars_well_allocated
     2614      #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching
     2615      #HEm_fn_id #Hframe_spec #Henv_below
    20592616      @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
    20602617      destruct (HA HB)
     
    20782635      @(CMR_while … stacksize … Hcl_env_hyp … Hinjection … kHtranslate_expr … kHmklabels …  kHeq_translate)
    20792636      try assumption
    2080       [ 1: @cthulhu
    2081          (* TODO: lemma allowing to prove this from [Htmp_vars_well_alloc] + tmp_gen inclusion *)                 
    2082          (* TODO wrap this up properly, by adding some invariant or by threading stmt_univ' into the cont *)
     2637      [ 1: (* TODO: lemma on Henv_below. We need to thread freshgens through cont_rel. *)
     2638           @cthulhu
    20832639      | 2: cases Hmore_invariant * * #_ * * * * #_ #_ * #_ #_ * * #_ #H
    2084            #_ #_ @H ]                 
     2640           #_ #_ @H ]
     2641    | 4,5: (* Continuations for Scall. TODO *)
     2642      @cthulhu
    20852643    ]
    20862644| 2: (* Assign *)
     
    20922650     #flag * * * * #Hstmt_inv_cm #Hlabels_translated #Htmps_preserved
    20932651     #Hreturn_ok #Hlabel_wf generalize in match (conj ????); #Hugly #Htranslate
    2094      #Hlabel_inclusion #Hcont_rel
    2095      #Em #Htmp_vars_well_allocated #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id #Hframe_spec
     2652     #Hlabel_inclusion #tmpenv #Htmpenv #Hcont_rel
     2653     #Em #Htmp_vars_well_allocated
     2654     #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id #Hframe_spec #Henv_below
    20962655     @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
    20972656     destruct (HA HB)
     
    21132672          normalize nodelta
    21142673          [ 1: (* Global *) #r
    2115                #Hlookup_var_success whd in ⊢ ((???%) → ?); #Hlhs_dest_eq 
     2674               #Hlookup_var_success whd in ⊢ ((???%) → ?); #Hlhs_dest_eq
    21162675               destruct (Hlhs_dest_eq) normalize nodelta
    21172676               generalize in match (conj ????); #Hinvariant
     
    21652724                    whd @conj try @conj try @refl
    21662725                    [ 2: #Habsurd destruct (Habsurd) ]
    2167                     generalize in match (conj ????);
    2168                     #Hinv_vars
     2726                    generalize in match (conj ????); #Hinv_vars
    21692727                    @CMR_normal try assumption
    2170                     [ 2: @refl | 1,3,4: ]
    2171                     [ 1: (* TODO: lemma on preservation of well-allocatedness through stores *) @cthulhu
    2172                     | 2: (* TODO: lemma on preservation of memory matching through stores *) @cthulhu ]
     2728                    [ 2: @refl | *: ]
     2729                    [ 3: @(memory_matching_preserved_by_parallel_stores … Hmatching)
     2730                    | 2: @(well_allocated_preserved_by_parallel_stores … Htmp_vars_well_allocated)
     2731                    | 1: @(clight_cminor_cont_rel_parametric_in_mem … Hcont_rel) ]
    21732732               | 2: #b #Heq destruct (Heq)
    21742733                    lapply (opt_to_res_inversion ???? Hlookup_var_success) #Hlookup_aux
     
    21922751                 ] (refl ? (lookup ?? cl_env var_id)))
    21932752               normalize nodelta
    2194                [ (* Contradiction: a stack-allocated variable was necessarily in the environment *)
     2753               [ (* Contradiction: a stack-allocated variable was necessarily in the environment. TODO *)
    21952754                 @cthulhu
    21962755               | #Heq destruct (Heq)
     
    22292788                 whd in match (m_bind ?????); normalize nodelta
    22302789                 whd @conj try @conj try @refl
    2231                  [ 2: #Habsurd destruct (Habsurd) ]
     2790                 [ 2: #Habsurd destruct (Habsurd) ]                 
    22322791                 @(CMR_normal … Halloc_hyp) try assumption
    2233                  [ 2: @refl | 1,3,4,5: ]
    2234                  [ 1: (* TODO: lemma on preservation of well-allocatedness through stores *) @cthulhu
    2235                  | 2: (* TODO: lemma on preservation of memory matching through stores *) @cthulhu ]
     2792                 try @refl
     2793                 try @(memory_matching_preserved_by_parallel_stores … Hmatching)
     2794                 try @(well_allocated_preserved_by_parallel_stores … Htmp_vars_well_allocated)
     2795                 @(clight_cminor_cont_rel_parametric_in_mem … Hcont_rel)
    22362796               ]
    22372797          | 3: (* Local *)
    2238                #Hlookup_var_success whd in ⊢ ((???%) → ?);
     2798               #Hlookup_var_success
     2799               cases (type_eq_dec ??) normalize nodelta #Htype_eq_dec
     2800               whd in ⊢ ((???%) → ?);
    22392801               #Heq destruct (Heq) normalize nodelta -Htranslate_statement
    22402802               #Htranslate
     
    22612823               normalize nodelta
    22622824               [ (* Contradiction: a register-allocated variable was necessarily in the environment *)
     2825                 (* TODO, cf Hlookup_var_success or sInv *)
    22632826                 @cthulhu
    22642827               | #Heq destruct (Heq)
     
    22812844                 generalize in match (proj1 ???); #Hpresent
    22822845                 generalize in match (conj ????); #Hstmt_vars
    2283                  @(CMR_normal … Halloc_hyp) try assumption
    2284                  [ 2: @refl | *: ]
    2285                  [ (* Need a particular kind of continuation relation *) @cthulhu
    2286                  | (* Lemma on preservation of well-allocatedness through update_present *) @cthulhu
    2287                  | (* Memory injection when writing in clight only, and block not mapped *) @cthulhu
    2288                  | (* Memory matching through env update *) @cthulhu ]
     2846                 @(CMR_normal … Halloc_hyp) try assumption try @refl
     2847                 [ 4: @(memory_matching_preserved_by_local_store … Hvalue_eq_rhs Hstore_value_of_type Hmatching)
     2848                 | 3: @(memory_inj_preserved_by_local_store … Hmatching Hinjection)
     2849                 | 2: @(tmp_vars_well_allocated_preserved_by_local_store … Hvalue_eq_rhs Hstore_value_of_type Htmp_vars_well_allocated)
     2850                 | 1: @(clight_cminor_cont_rel_parametric_in_cm_env … Hpresent Hcont_rel) ]
    22892851               ]
    22902852          ]
     
    23452907          whd in match (m_bind ?????); normalize nodelta whd @conj try @conj try @refl
    23462908          [ 2: #Habsurd destruct (Habsurd) ]
    2347           @(CMR_normal … Halloc_hyp) try assumption
    2348           [ 2: @refl | *: ]
    2349           [ 1: (* lemma on well_allocated after CL and CM parallel writes *) @cthulhu
    2350           | 2: (* memory matching *) @cthulhu ]
     2909          @(CMR_normal … Halloc_hyp) try assumption try @refl
     2910          [ 3: @(memory_matching_preserved_by_parallel_stores … Hmatching)
     2911          | 2: @(well_allocated_preserved_by_parallel_stores … Htmp_vars_well_allocated)
     2912          | 1: @(clight_cminor_cont_rel_parametric_in_mem … Hcont_rel) ]
    23512913     ]
    23522914| 4: (* Seq *)
     
    23552917     (* introduce everything *)
    23562918     #fInv #sInv #kInv #Htarget_type #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function
    2357      #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls     
     2919     #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls
    23582920     #flag * * * * #Hstmt_inv_cm #Hlabels_translated #Htmps_preserved
    23592921     #Hreturn_ok #Hlabel_wf generalize in match (conj ????); #Hugly #Htranslate #Hlabel_inclusion
    2360      #Hcont_rel
    2361      #Em #Htmp_vars_well_allocated #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id #Hframe_spec
     2922     #tmpenv #Htmpenv  #Hcont_rel
     2923     #Em #Htmp_vars_well_allocated
     2924     #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id #Hframe_spec #Henv_below
    23622925     @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
    23632926     destruct (HA HB)
     
    23762939          @transitive_lset_inclusion @lset_inclusion_union %1
    23772940          @reflexive_lset_inclusion
    2378      | 2: @(ClCm_cont_seq … Htrans_stm2)
     2941     | 2: lapply (translation_entails_ident_inclusion … Htrans_stm2) #H
     2942          @(transitive_lset_inclusion … (translation_entails_ident_inclusion … Htrans_stm2))
     2943          assumption
     2944     | 3: @(ClCm_cont_seq … Htrans_stm2)
    23792945          [ 1: lapply Hlabel_inclusion @transitive_lset_inclusion @lset_inclusion_union %2
    23802946               @reflexive_lset_inclusion
    2381           | 2: assumption ]
    2382      | 3: @cthulhu ]
    2383 | *: @cthulhu ]
     2947          | 2: assumption
     2948          | 3: assumption ]
     2949     ]
     2950| *: (* Other statements *) @cthulhu ]
    23842951| 2: (* Return state *)
    2385   #cl_ge #cm_ge #INV' #cl_f #cm_f #alloc_type
    2386   #cl_env #cl_m #cm_env #c_m #cm_st #stackptr #stacksize
    2387   #stmt_univ #Em #Htmp_vars_wa #Hcharac #Hexec_alloc #Hinj #Hmatch #Hem_fn_id #Hframe
     2952  #cl_ge #cm_ge #INV' #cl_k #cm_k #cm_st #cl_f #cm_f #alloc_type
     2953  #cl_env #cl_m #cm_env #cm_mt #stackptr #stacksize
     2954  #stmt_univ #tmpenv #Htmpenv #Em #Htmp_vars_wa #Hcharac #Hexec_alloc #Hinj #Hmatch #Hem_fn_id #Hframe #Hcont
    23882955  @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
    23892956  destruct (HA HB)
     
    23932960  whd in Hclight_normal:%;
    23942961  @False_ind @Hclight_normal
    2395 | 3: (* Call state, nostore *)
    2396   #cl_ge #cm_ge #cl_f #cm_f #INV' #alloc_types
    2397   #cl_env #cl_m #cm_env #cm_m #stackptr #u #cl_fundef #cm_fundef
    2398   #Hglobals_fresh #Hfundef_fresh #rettyp #Hrettyp #cl_k #cm_k #fblock
    2399   #Hcont_rel #cl_fun_id #cm_fun_id #Hfun_id_eq #cl_retval #cm_retval
    2400   #sInv #fInv #kInv #cl_argvals #cm_argvals #cm_stack
     2962| 3: (* Call state *)
     2963  #cl_ge #cm_ge #INV' #cl_k #cm_k #cm_st #cl_f #cm_f #cl_fundef #cm_fundef
     2964  #fblock #target_type #alloc_type #cl_env #cl_m #cm_env #cm_m #stackptr #stacksize
     2965  #func_univ #Hgobals_fresh #Hfundef_fresh #Htranslate_function #Hfind_cl #Hfind_cm
     2966  #cl_id #cm_id #stmt_univ #tmpenv #Htmpenv #Hcont_rel
     2967  #Em #Htmp_vars_wa #Hcharac #Hexec_alloc #Hinj #Hmatch #Hem_fn_id #Hframe
     2968  #cl_args_values #cm_args_values #Hall2
    24012969  @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
    24022970  destruct (HA HB)
    24032971  @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
    2404   destruct (HC HD HE)
     2972  destruct (HC HD HE) #_
    24052973  whd in Hclight_normal:%;
    24062974  @False_ind @Hclight_normal
    2407 | 4: (* Call state, store *)
    2408   #cl_ge #cm_ge #cl_f #cm_f #INV' #alloc_types
    2409   #cl_env #cl_m #cm_env #cm_m #cm_stack #stackptr #u #cl_fundef #cm_fundef
    2410   #Hglobals_fresh #Hfundef_fresh #rettyp #Hrettyp #cl_k #cm_k #fblock
    2411   #Hcont_rel #cl_fun_id #cm_fun_id #Hfun_id_eq
    2412   #cl_rettyp #cl_retval #cl_retrace #cm_retval #cl_lhs #cm_lhs
    2413   #Hinvariant_on_cm_lhs #Hexec_lvalue #Htranslate_dest #cm_ret_var
    2414   #sInv #fInv #kInv #cl_argvals #cm_argvals #cm_stack
    2415   @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
    2416   destruct (HA HB)
    2417   @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
    2418   destruct (HC HD HE)
    2419   whd in Hclight_normal:%;
    2420   @False_ind @Hclight_normal
    2421 | 5: (* Intermediary While state *)
     2975| 4: (* Intermediary While state *)
    24222976     (* ---------------------------------------------------------------------- *)
    24232977#cl_ge #cm_ge #INV'
     
    24262980#cm_stack #rettyp #kInv #fInv #sInv #Heq_ty #Hrettyp_eq #func_univ #Hfresh_globals #Hfresh_function
    24272981#Htranslate_function #Hcont_rel
    2428 #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbl_univ'' #lbls
    2429 #Em #Htmp_vars_well_allocated #Halloc_hyp
    2430 #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id #Hframe_spec #Hexpr_vars #Htranslate_expr
    2431 #Hentry_ex #Hexit_ex #Htranslate_inv #Hmk_labels #Htranslate_statement
     2982#stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbl_univ'' #tmpenv #Htmpenv #Hcont_rel
     2983#Em #Htmp_vars_well_allocated
     2984#Hcharacterise #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id #Hframe_spec #Henv_below
     2985#Hexpr_vars #Htranslate_expr #Hentry_ex #Hexit_ex #Htranslate_inv #Hmk_labels #Htranslate_statement
    24322986#Hlabel_inclusion #Hlabel_exists #Hinv1 #Hinv2 #Hfind_label
    24332987@(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
     
    24493003  generalize in match (proj1 ???); #Hpresent_ifthenelse
    24503004  (* Exhibit simulation of condition evaluation *)
    2451   lapply (eval_expr_sim … Halloc_hyp … Hcl_env_hyp … Hinjection … Hmatching) * #Hsim #_
     3005  lapply (eval_expr_sim … Hcharacterise … Hcl_env_hyp … Hinjection … Hmatching) * #Hsim #_
     3006  (* The type of Hsim forces us to wrap cm_cond into a dummy cast. *)
    24523007  lapply (Hsim (Expr cl_cond_desc cl_cond_ty) (CMcast ?? cm_cond ?))
    2453   [ >Heq_ty @refl ] -Hsim #Hsim
    2454   lapply (Hsim … Hexpr_vars … Htranslate_expr ??? Hcl_exec_cond)
    2455   [ lapply Hpresent_ifthenelse whd in ⊢ (% → ?); <Heq_ty >CMcast_identity #H @H ]
     3008  [ >Heq_ty @refl ] -Hsim
     3009  whd in match (typeof ?); #Hsim
     3010  lapply (Hsim ??????)
     3011  [ 2: <Heq_ty >CMcast_identity assumption
     3012  | 1: assumption
     3013  | 6: <Heq_ty >CMcast_identity assumption
     3014  | 5: lapply Htranslate_expr lapply Hexpr_vars lapply cm_cond -cm_cond
     3015       >Heq_ty #cm_cond #Hexpr_vars @(jmeq_absorb ?????) #Hsol @Hsol
     3016  | *: ]
    24563017  * #cm_val_cond * #Hcm_eval_cond #Hvalue_eq -Hsim
    24573018  cut (eval_expr cm_ge (ASTint sz sg) cm_cond cm_env Hpresent_ifthenelse stackptr cm_m = OK ? 〈tr, cm_val_cond〉)
     
    24763037  generalize in match (proj1 ???); #Hpresent_ifthenelse
    24773038  (* Exhibit simulation of condition evaluation *)
    2478   lapply (eval_expr_sim … Halloc_hyp … Hcl_env_hyp … Hinjection … Hmatching) * #Hsim #_
     3039  lapply (eval_expr_sim … Hcharacterise … Hcl_env_hyp … Hinjection … Hmatching) * #Hsim #_
    24793040  lapply (Hsim (Expr cl_cond_desc cl_cond_ty) (CMcast ?? cm_cond ?))
    2480   [ >Heq_ty @refl ] -Hsim #Hsim
    2481   lapply (Hsim … Hexpr_vars … Htranslate_expr ??? Hcl_exec_cond)
    2482   [ lapply Hpresent_ifthenelse whd in ⊢ (% → ?); <Heq_ty >CMcast_identity #H @H ]
     3041  [ >Heq_ty @refl ] -Hsim
     3042  whd in match (typeof ?); #Hsim
     3043  lapply (Hsim ??????)
     3044  [ 2: <Heq_ty >CMcast_identity assumption
     3045  | 1: assumption
     3046  | 6: <Heq_ty >CMcast_identity assumption
     3047  | 5: lapply Htranslate_expr lapply Hexpr_vars lapply cm_cond -cm_cond
     3048       >Heq_ty #cm_cond #Hexpr_vars @(jmeq_absorb ?????) #Hsol @Hsol
     3049  | *: ]
    24833050  * #cm_val_cond * #Hcm_eval_cond #Hvalue_eq -Hsim
    24843051  cut (eval_expr cm_ge (ASTint sz sg) cm_cond cm_env Hpresent_ifthenelse stackptr cm_m = OK ? 〈tr, cm_val_cond〉)
     
    24963063  whd @conj try @conj
    24973064  [ 3: #Habsurd destruct (Habsurd)
    2498   | 1: normalize >append_nil >append_nil @refl 
     3065  | 1: normalize >append_nil >append_nil @refl
    24993066  | 2: @(CMR_normal … DoNotConvert) try assumption
    2500        [ 2: @refl | ]
     3067       try @refl
     3068       @(env_below_freshgen_preserved_by_translation … Htranslate_statement)
     3069       assumption
    25013070  ]
    25023071]
     
    25053074
    25063075 
    2507 lemma clight_cminor_call_return :
    2508   ∀g1, g2.
    2509   ∀INV:clight_cminor_inv g1 g2.
    2510   ∀s1,s1'.
    2511   clight_cminor_rel g1 g2 INV s1 s1' →
    2512   match Clight_classify s1 with
    2513   [ cl_call ⇒ true
    2514   | cl_return ⇒ true
    2515   | _ ⇒ false ] →
    2516   ∀s2,tr. step … (pcs_exec cl_pre) g1 s1 = Value … 〈tr, s2〉 →
    2517   ∃m. after_n_steps m ?? (pcs_exec cm_pre) g2 s1' (λs.cminor_normal s) (λtr',s2'.
    2518     tr = tr' ∧
    2519     clight_cminor_rel g1 g2 INV s2 s2' ∧
    2520       (m = 0 → lex_lt (measure_Clight s2) (measure_Clight s1))
    2521   ).
    2522 #g1 #g2 #INV #s1 #s1' #Hstate_rel #Hclight_class
    2523 inversion Hstate_rel
    2524 [ 1: (* normal *)
    2525   #cl_ge #cm_ge #INV' #cl_s
    2526   #cm_s #cl_k #cm_k #cm_st #cl_f #cm_f #rettyp
    2527   #alloc_type #cl_env #cl_m #cm_env #cm_m #stackptr #stacksize
    2528   (* introduce everything *)
    2529   #fInv #sInv #kInv #Htarget_type #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function
    2530   #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls
    2531   #flag  #Htrans_inv #Htrans_stmt #Hincl #HA #HB #HC
    2532   #HE #HF #HG #HI #HJ #HK
    2533   @(jmeq_absorb ?????) #H1 @(jmeq_absorb ?????) #H2
    2534   destruct (H1 H2)
    2535   @(jmeq_absorb ?????) #H3 @(jmeq_absorb ?????) #H4 @(jmeq_absorb ?????) #H5
    2536   destruct (H3 H4 H5)
    2537   @False_ind @Hclight_class
    2538 | 5:
    2539   #cl_ge #cm_ge #INV' #cl_s
    2540   #cm_s #cl_k #cm_k #cm_st #cl_f #cm_f #rettyp
    2541   #alloc_type #cl_k #cm_k #sz #sg #cl_ty #cl_cond_desc #cl_body #entry_lab #exit_lab
    2542   #cm_cond #cm_body #cm_stack #rettyp' #kInv
    2543   (* introduce everything *)
    2544   #fInv #sInv #kInv #Htarget_type #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function
    2545   #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls
    2546   #lbl1 #lbl2 #Em #Htmp_vars #Hcharac #Hexec #Hinj #Hmatching #Hem #Hframe #Hcond_tr
    2547   #Htransl #Hex1 #Hex2 #Htransinv #Hmklabs #Htranstmt #Hincl
    2548   #Hlabdecl #Hinv1 #Hinv2 #Hfindlab
    2549   @(jmeq_absorb ?????) #H1 @(jmeq_absorb ?????) #H2
    2550   destruct (H1 H2)
    2551   @(jmeq_absorb ?????) #H3 @(jmeq_absorb ?????) #H4 @(jmeq_absorb ?????) #H5
    2552   destruct (H3 H4 H5)
    2553   @False_ind @Hclight_class
    2554 | *: @cthulhu
    2555 ] qed.
     3076
    25563077
    25573078
     
    25743095  make_initial_state ?? clight_fullexec cl_program = OK ? s →
    25753096  make_initial_state ?? Cminor_fullexec cm_program = OK ? s' →
    2576   ∃INV. clight_cminor_rel INV s s'. *)
     3097  ∃INV. clight_cminor_rel INV s
Note: See TracChangeset for help on using the changeset viewer.