Changeset 2822


Ignore:
Timestamp:
Mar 8, 2013, 12:48:20 PM (6 years ago)
Author:
garnier
Message:

A consitent proof state for Clight to Cminor, with some progress (and some temporary regressions)

Location:
src/Clight
Files:
6 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Csem.ma

    r2722 r2822  
    129129].
    130130
    131 (* Ilias, 16 jan 2013: semantics of pointer/pointer subtraction slightly changed. Matched in toCminor.ma.
    132  * operation done on 32 bits and cast down to the target size using sign_ext or zero_ext, according to the
    133  * sign of the target type. We have to do the same in toCminor.ma
    134  * At least two things are ugly here : the fact that offsets are 32 bits (our arch is 8 bit right ?), and the downcast.
    135  * TODO: check the C standard to see if the following alternative is meaningful ?
    136  *   . the division can directly take as an argument a target size. There is also two [repr], one
    137  *     with type nat → bvint I32 (used here), one with type ∀sz. nat → bvint sz. Matching changes
    138  *     would have to be done in Cminor.
    139  *)
     131(* Ilias, 16 jan 2013: semantics of pointer/pointer subtraction slightly changed. Matched in toCminor.ma. *)
    140132let rec sem_sub (v1:val) (t1:type) (v2: val) (t2:type) (target:type) : option val ≝
    141133  match classify_sub t1 t2 with
  • src/Clight/frontend_misc.ma

    r2608 r2822  
    3939[ 1: #Heq destruct elim Hneq #Hcontr elim (Hcontr (refl ? t2))
    4040| 2: #Hneq' normalize // ] qed.
     41
     42lemma typ_eq_dec : ∀t1,t2:typ. (t1=t2)⊎(t1≠t2).
     43#t1 #t2
     44cases t1 cases t2
     45[ #sz #sg #sz' #sg' cases sz cases sz'
     46  try //
     47| #sz #sg %2 % #Habsurd destruct (Habsurd)
     48| #sz #sg %2 % #Habsurd destruct (Habsurd)
     49| %1 @refl ]
     50qed.
    4151
    4252lemma le_S_O_absurd : ∀x:nat. S x ≤ 0 → False. /2 by absurd/ qed.
  • src/Clight/memoryInjections.ma

    r2698 r2822  
    20202020(* Lift the above result to memory_inj
    20212021 * This is Lemma 40 of Leroy & Blazy *)
    2022 lemma bestorev_memory_inj_to_memory_inj :
     2022lemma store_value_of_type_memory_inj_to_memory_inj :
    20232023  ∀E,mA,mB,mC.
    20242024  ∀Hext:memory_inj E mA mB.
     
    22112211  ∀b1,b2,delta. E b1 = Some ? 〈b2, delta〉 →
    22122212  ∀ty,i,m1'.
    2213   ast_typ_consistent_with_value ty v1 →
     2213  (* ast_typ_consistent_with_value ty v1 → *)
    22142214  storen m1 (mk_pointer b1 i) (fe_to_be_values ty v1) = Some ? m1' →
    22152215  ∃m2'. storen m2 (mk_pointer b2 (offset_plus i delta)) (fe_to_be_values ty v2) = Some ? m2' ∧
     
    22992299  ∀b1,b2,delta. E b1 = Some ? 〈b2, delta〉 →
    23002300  ∀ty,i,m1'.
    2301   type_consistent_with_value ty v1 →
     2301  (* type_consistent_with_value ty v1 → *)
    23022302  store_value_of_type ty m1 b1 i v1 = Some ? m1' →
    23032303  ∃m2'. store_value_of_type ty m2 b2 (offset_plus i delta) v2 = Some ? m2' ∧
     
    23072307[ | #sz' #sg' | #ptr_ty' | #array_ty' #array_sz' | #domain' #codomain'
    23082308| #structname' #fieldspec' | #unionname' #fieldspec' | #id' ]
    2309 #Hconsistent whd in ⊢ ((??%?) → ?);
     2309whd in ⊢ ((??%?) → ?);
    23102310[ 1,4,5,6,7: #Habsurd destruct ]
    23112311whd in match (store_value_of_type ?????);
    2312 @(storen_parallel_aux … Hinj … Hembed … Hconsistent) //
     2312@(storen_parallel_aux … Hinj … Hembed) //
    23132313qed.
    23142314
  • src/Clight/toCminor.ma

    r2686 r2822  
    701701        - if e1 is a struct* or a function ptr, then we acess by reference, in which case we :
    702702           1) check the consistency of the regions in the type of e1 and in the access mode of its type
    703            2) return directly the converted CMinor expression "as is" (TODO : what is the strange notation with the ceil function and the mapsto ?)
     703           2) return directly the converted CMinor expression "as is"
    704704      *)
    705705      match typ_of_type (typeof e1) return λx.(Σz:CMexpr x.expr_vars ? z (local_id vars)) → ? with
     
    11841184       do e2' ← typ_should_eq (typ_of_type (typeof e2)) (typ_of_type ty) ? e2';
    11851185       OK ? «〈uv, ul, St_assign ? id e2'〉, ?»
    1186     | MemDest e1' ⇒
    1187        OK ? «〈uv, ul, St_store ? e1' e2'〉, ?»
     1186    | MemDest e1' ⇒
     1187       match type_eq_dec (typeof e1) (typeof e2) with
     1188       [ inl Hcl_typ_eq ⇒       
     1189         OK ? «〈uv, ul, St_store ? e1' e2'〉, ?»
     1190       | inr Hcl_typ_neq ⇒
     1191         Error ? (msg TypeMismatch)
     1192       ]
    11881193    ]
    11891194| Scall ret ef args ⇒
     
    11961201        do dest ← translate_dest vars e1;
    11971202        match dest with
    1198         [ IdDest id ty p ⇒ OK ? «〈uv, ul, St_call (Some ? 〈id,typ_of_type ty〉) ef' args'〉, ?»
     1203        [ IdDest id ty p ⇒
     1204            (* No trace generated here, by inversion on translate_dest _ _ = IdDest _ _ _ *)
     1205            OK ? «〈uv, ul, St_call (Some ? 〈id,typ_of_type ty〉) ef' args'〉, ?»
    11991206        | MemDest e1' ⇒
    12001207            let 〈tmp, uv1〉 as Etmp ≝ alloc_tmp ? (typeof e1) uv in
    1201             OK ? «〈uv1, ul, St_seq (St_call (Some ? 〈tmp,typ_of_type (typeof e1)〉) ef' args') (St_store (typ_of_type (typeof e1)) e1' (Id ? tmp))〉, ?»
     1208            (* alloc a new variable to serve as a placeholder for the evaluation of e1',
     1209             * which /must/ happen before the call. Otherwise, the cost labels are not
     1210             * emitted as in Clight.  *)
     1211            let 〈tmp2, uv2〉 as Etmp' ≝ alloc_tmp ? (Tpointer (typeof e1)) uv1 in
     1212            OK ? «〈uv2, ul,
     1213                    (St_seq (St_store ? (Id ? tmp2) e1')
     1214                    (St_seq (St_call (Some ? 〈tmp,typ_of_type (typeof e1)〉) ef' args')
     1215                            (St_store (typ_of_type (typeof e1)) e1' (Id ? tmp))))〉, ?»
    12021216        ]
    12031217    ]
     
    13361350try (#H1 try #H2 assumption)
    13371351[ 1,5: @(tmp_preserved … p) ]
    1338 [ 1,3: elim e2' | 2,9,23: elim e1' | 4,7,13: elim ef' ]
    1339 [ 1,2,3,4,5,6,7,8 : #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal) ]
    1340 [ 1: @All_mp [ 1: @(λe.match e with [ mk_DPair t e0 ⇒ expr_vars t e0 (local_id vars) ])
     1352[ 6: @(local_id_fresh_tmp vars tmp2 uv2 (Tpointer (typeof e1)) uv1 Etmp')
     1353| 7: cases e1' #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal)
     1354| 8: @conj try @conj normalize nodelta
     1355     [ 1: cases e1' #e #Hvars lapply (local_id_fresh_tmp vars tmp uv1 (typeof e1) uv Etmp)
     1356          @(alloc_tmp_preserves … Etmp')
     1357     | 3: @All_mp [ 1: @(λe.match e with [ mk_DPair t e0 ⇒ expr_vars t e0 (local_id vars) ])
     1358                  | 2: * #t #e #Hev whd in Hev ⊢ %; @(expr_vars_mp … Hev) #i #t #Hp @(tmp_preserved … Hp)
     1359                  | 3: elim args' // ]
     1360     | 2: cases ef' #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal) ] ]
     1361[ 5: @All_mp [ 1: @(λe.match e with [ mk_DPair t e0 ⇒ expr_vars t e0 (local_id vars) ])
    13411362             | 2: * #t #e #Hev whd in Hev ⊢ %; @(expr_vars_mp … Hev) #i #t #Hp @(tmp_preserved … Hp)
    1342              | 3: elim args' // ]
    1343 | 7: (* we should be able to merge this case with the previous ... *)
    1344      @All_mp [ 1: @(λe.match e with [ mk_DPair t e0 ⇒ expr_vars t e0 (local_id vars) ])
     1363             | 3: elim args' // ] ]
     1364[ 5: whd @conj
     1365     [ 1: cases e1' #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal)
     1366     | 2: @(alloc_tmp_preserves … Etmp') @(local_id_fresh_tmp … Etmp) ] ]     
     1367[ 1,3: elim e2' #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal)
     1368| 2: elim e1' #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal)
     1369| 4,7: elim ef' #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal) ]
     1370[ 3: @All_mp [ 1: @(λe.match e with [ mk_DPair t e0 ⇒ expr_vars t e0 (local_id vars) ])
    13451371             | 2: * #t #e #Hev whd in Hev ⊢ %; @(expr_vars_mp … Hev) #i #t #Hp @(tmp_preserved … Hp)
    13461372             | 3: elim args' // ]
    1347 | 2: @(local_id_fresh_tmp vars tmp uv1 (typeof e1) uv Etmp)
    1348 | 3:  @(All_mp (𝚺 t:typ.expr t) (λe. match e with [ mk_DPair t e0 ⇒ expr_vars t e0 (local_id vars)]))
    1349        [ 1: #a #Ha elim a in Ha ⊢ ?; #ta #a #Ha whd @(expr_vars_mp ?? (local_id vars))
    1350        [ 1: #i0 #t0 #H0 @(tmp_preserved vars uv1 i0 t0 H0)
    1351        | 2: assumption ]
    1352        | 2: elim args' // ]
    1353 | 4: @(local_id_fresh_tmp vars tmp uv1 (typeof e1) uv Etmp) ]
    1354 [ 1: #size #sign | 2: ]
    1355 [ 1,2: #H @(alloc_tmp_preserves vars tmp uv uv1 … Etmp) @H ]
     1373| 2: #H @(alloc_tmp_preserves … Etmp' l ASTptr) @(alloc_tmp_preserves … Etmp l ASTptr) @H
     1374| 1: #sz #sg #H @(alloc_tmp_preserves … Etmp' l) @(alloc_tmp_preserves … Etmp l) @H ]
    13561375try @refl (* Does (at least) the return_ok cases *)
    13571376try @(match fgens1 return λx.x=fgens1 → ? with
     
    13671386try (elim H2 -H2 * * * #Hstmt_inv2 #Hlabels_tr2 #Htmps_pres2 #Hret2)
    13681387try (elim H3 -H3 * * * #Hstmt_inv3 #Hlabels_tr3 #Htmps_pres3 #Hret3)
     1388[ 8: whd cases e1' #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal) ]
    13691389[ 1,2: #Hind1 #Hind2 | 3,4,8,10: #Hind | 5: #Hind1 #Hind2 #Hind3 ]
    13701390try @conj try @conj try @conj try @conj try @conj try @conj try (whd @I) try assumption
  • src/Clight/toCminorCorrectness.ma

    r2737 r2822  
    232232] qed.
    233233
    234 (* A measure on Clight states that is decreasing along execution sequences *)
     234(* --------------------------------------------------------------------------- *)
     235(* Clight to Cminor makes use of fresh symbol generators, which store the list
     236 * of symbols they generate. We need to maintain as an invariant that these grow
     237 * in a monotonic and consistent fashion. *)
     238(* --------------------------------------------------------------------------- *)
     239
     240(* The two following definitions and two lemmas are duplicated from switchRemoval.ma.
     241 * TODO: factorise this in frontend_misc, if they turn out not to be useless *)
     242definition fresher_than_or_equal : universe SymbolTag → universe SymbolTag → Prop ≝
     243λu1,u2.
     244  match u1 with
     245  [ mk_universe p1 ⇒
     246    match u2 with
     247    [ mk_universe p2 ⇒ p2 ≤ p1 ] ].
     248   
     249definition fte ≝ fresher_than_or_equal.
     250
     251lemma transitive_fte : ∀u1,u2,u3. fte u1 u2 → fte u2 u3 → fte u1 u3.
     252* #u1 * #u2 * #u3 normalize /2 by transitive_le/
     253qed.
     254
     255lemma reflexive_fte : ∀u. fte u u.
     256* // qed.
     257
     258definition labgen_include ≝
     259  λgen1, gen2 : labgen.
     260  ∃labels. label_genlist gen2 = labels @ label_genlist gen1.
     261 
     262definition tmpgen_include ≝
     263  λvartypes.
     264  λgen1, gen2 : tmpgen vartypes.
     265  ∃idents. tmp_env ? gen2 = idents @ (tmp_env ? gen1).
     266
     267(* --------------------------------------------------------------------------- *)
     268(* Additional invariants not contain in clight_cminor_data *)
     269(* --------------------------------------------------------------------------- *)
     270
     271(* Fresh variable ident generator *)
     272(* tmp_gen     : tmpgen alloc_type; *)
     273
     274(* Temporary variables generated during conversion are well-allocated. *)
     275definition tmp_vars_well_allocated ≝
     276   λvartypes.
     277   λtmp_gen: tmpgen vartypes.
     278   λcm_env.
     279   λcm_m.
     280   λcl_m.
     281   λE: embedding.
     282   ∀local_variable.
     283   ∀H:present ?? cm_env local_variable.
     284   ∀ty. Exists ? (λx. x = 〈local_variable, ty〉) (tmp_env … tmp_gen) →
     285   ∀v. val_typ v (typ_of_type ty) →
     286   ∃cm_m'. storev (typ_of_type ty) cm_m (lookup_present ?? cm_env local_variable H) v = Some ? cm_m' ∧
     287           memory_inj E cl_m cm_m'.
     288
     289(* wrap the above invariant into a clight_cminor_data-eating prop *)
     290(*
     291definition tmp_vars_well_allocated' ≝
     292   λcl_f, cl_ge, cm_ge, INV.
     293   λframe_data: clight_cminor_data cl_f cl_ge cm_ge INV.
     294   λtmp_gen: tmpgen (alloc_type … frame_data).
     295   ∀vars_v, cl_m_v, cm_env_v, cm_m_v.
     296   vars_v   = alloc_type … frame_data →
     297   cl_m_v   = cl_m … frame_data →
     298   cm_env_v = cm_env … frame_data →
     299   cm_m_v   = cm_m … frame_data →   
     300   ∀local_variable.
     301   ∀H:present ?? cm_env_v local_variable.
     302   ∀ty. Exists ? (λx. x = 〈local_variable, ty〉) (tmp_env … tmp_gen) →
     303   ∀v. val_typ v (typ_of_type ty) →
     304   ∃cm_m'. storev (typ_of_type ty) cm_m_v (lookup_present ?? cm_env_v local_variable H) v = Some ? cm_m' ∧
     305           memory_inj (Em … frame_data) cl_m_v cm_m'. *)
     306
     307(* --------------------------------------------------------------------------- *)           
     308(* A measure on Clight states that is decreasing along execution sequences     *)
     309(* --------------------------------------------------------------------------- *)
    235310
    236311(* statements *)
     
    315390definition lex_lt ≝ lexicographic nat lt.
    316391
     392(* --------------------------------------------------------------------------- *)
     393(* Simulation relations *)
     394(* --------------------------------------------------------------------------- *)
     395
     396record frame_data
     397  (f : function)
     398  (ge_cl : genv_t clight_fundef)
     399  (ge_cm : genv_t (fundef internal_function))
     400  (INV : clight_cminor_inv ge_cl ge_cm) : Type[0] ≝
     401{
     402}.
    317403
    318404(* relate Clight continuations and Cminor ones. *)
     
    322408  ∀cl_f: function.                          (* current Clight function *)
    323409  internal_function →                       (* current Cminor function *)
    324   clight_cminor_data cl_f cl_ge cm_ge INV → (* data for the current stack frame in CL and CM *)
     410  cl_env →
     411  cm_env →
     412  (*frame_data cl_f cl_ge cm_ge INV →*)         (* data for the current stack frame in CL and CM *)
    325413  option typ →                              (* optional target type - uniform over a given function *)
    326414  cl_cont →                                 (* CL cont *)
    327415  cm_cont →                                 (* CM cont *)
    328416  Prop ≝
     417(* Stop continuation*) 
    329418| ClCm_cont_stop:
    330   ∀cl_ge, cm_ge, INV, cl_f, cm_f, frame_data, target_type.
    331   clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f frame_data target_type Kstop Kend
     419  ∀cl_ge, cm_ge, INV, cl_f, cm_f, target_type.
     420  ∀cl_env, cm_env.
     421  clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env target_type Kstop Kend
     422
     423(* Seq continuation *)
    332424| ClCm_cont_seq:
    333   ∀cl_ge, cm_ge, INV, cl_f, cm_f, frame_data, target_type.
     425  ∀cl_ge, cm_ge, INV, cl_f, cm_f, target_type.
     426  ∀alloc_type.
    334427  ∀cl_s: statement.
    335428  ∀cm_s: stmt.
    336   ∀cl_k':  cl_cont.
    337   ∀cm_k':  cm_cont.
     429  ∀cl_env: cl_env.
     430  ∀cm_env: cm_env.
     431  ∀cl_k': cl_cont.
     432  ∀cm_k': cm_cont.
    338433  ∀stmt_univ, stmt_univ'.
    339434  ∀lbl_univ, lbl_univ'.
     
    341436  ∀flag.
    342437  ∀Htranslate_inv.
    343   translate_statement (alloc_type … frame_data) stmt_univ lbl_univ lbls flag target_type cl_s = OK ? «〈stmt_univ',lbl_univ',cm_s〉, Htranslate_inv» →
    344   clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f frame_data target_type cl_k' cm_k' →
    345   clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f frame_data target_type (ClKseq cl_s cl_k') (Kseq cm_s cm_k')
     438  translate_statement alloc_type stmt_univ lbl_univ lbls flag target_type cl_s = OK ? «〈stmt_univ',lbl_univ',cm_s〉, Htranslate_inv» →
     439  clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env target_type cl_k' cm_k' →
     440  clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env target_type (ClKseq cl_s cl_k') (Kseq cm_s cm_k')
     441
     442(* While continuation *) 
    346443| ClCm_cont_while:
    347444  (* Inductive family parameters *)
    348   ∀cl_ge, cm_ge, INV, cl_f, cm_f, frame_data, target_type.
     445  ∀cl_ge, cm_ge, INV, cl_f, cm_f, target_type.
     446
     447  ∀alloc_type.
     448  ∀cl_env.
     449  ∀cm_env.
    349450
    350451  (* sub-continuations *)
     
    370471  (* relate CL and CM expressions *)
    371472  ∀Hexpr_vars.
    372   translate_expr (alloc_type … frame_data) (Expr cl_cond_desc (Tint sz sg)) = OK ? («cm_cond, Hexpr_vars») →
     473  translate_expr alloc_type (Expr cl_cond_desc (Tint sz sg)) = OK ? («cm_cond, Hexpr_vars») →
    373474
    374475  (* Parameters and results to find_label_always *)
    375   ∀sInv: stmt_inv cm_f (cm_env … frame_data) (f_body cm_f).
     476  ∀sInv: stmt_inv cm_f cm_env (f_body cm_f).
    376477  ∀Hinv.
    377478
    378479  (* Specify how the labels for the while-replacing gotos are produced *)
    379480  mklabels lbl_univ = 〈〈entry, exit〉, lbl_univ'〉 →
    380   translate_statement (alloc_type … frame_data) stmt_univ lbl_univ' lbls (ConvertTo entry exit) target_type cl_body = OK ? «〈stmt_univ',lbl_univ'',cm_body〉, Htranslate_inv» →
    381   find_label_always entry (f_body cm_f) Kend (proj2 … (proj1 … (proj1 … Hinv))) cm_f (cm_env … frame_data) sInv I =
     481  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» →
     482  find_label_always entry (f_body cm_f) Kend (proj2 … (proj1 … (proj1 … Hinv))) cm_f cm_env sInv I =
    382483    «〈St_label entry
    383484          (St_seq
    384485            (St_ifthenelse ?? cm_cond (St_seq cm_body (St_goto entry)) St_skip)
    385486            (St_label exit St_skip)), cm_k'〉, Hinv» →
    386   clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f frame_data target_type cl_k' cm_k' →
    387   clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f frame_data target_type (Kwhile (Expr cl_cond_desc (Tint sz sg)) cl_body cl_k') (Kseq (St_goto entry) (Kseq (St_label exit St_skip) cm_k')).
     487  clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env target_type cl_k' cm_k' →
     488  clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env target_type (Kwhile (Expr cl_cond_desc (Tint sz sg)) cl_body cl_k') (Kseq (St_goto entry) (Kseq (St_label exit St_skip) cm_k')).
     489
     490
     491(* TODO XXX *)
     492(* relation between placeholders for return values *)
     493
     494definition return_value_rel :
     495  ∀cl_f, cl_ge, cm_ge.
     496  ∀INV: clight_cminor_inv cl_ge cm_ge.
     497  frame_data cl_f ?? INV →
     498  option (block×offset×type) → option (ident×typ) → Prop ≝
     499λcl_f, cl_ge, cm_ge, INV, data, opt1, opt2.
     500match opt1 with
     501[ None ⇒
     502  match opt2 with
     503  [ None ⇒ True
     504  | _ ⇒ False ]
     505| Some ptr ⇒
     506  match opt2 with
     507  [ Some id ⇒ True (* TODO, here. *)
     508  | None ⇒ False
     509  ]
     510].
    388511
    389512(* Definition of the simulation relation on states. The orders of the parameters is dictated by
     
    394517  ∀cl_ge, cm_ge.
    395518  (* Relates globals to globals and functions to functions. *)
    396   ∀INV:  clight_cminor_inv cl_ge cm_ge.
    397  
     519  ∀INV:  clight_cminor_inv cl_ge cm_ge. 
    398520  (* ---- Statements ---- *)
    399521  ∀cl_s: statement.                                       (* Clight statement *) 
    400522  ∀cm_s: stmt.                                            (* Cminor statement *)
    401 
    402523  (* ---- Continuations ---- *)
    403524  ∀cl_k: cl_cont.                                      (* Clight continuation *)
    404525  ∀cm_k: cm_cont.                                      (* Cminor continuation *)
    405   ∀cm_st: stack.                                              (* Cminor stack *)
    406  
     526  ∀cm_st: stack.                                              (* Cminor stack *) 
    407527  ∀cl_f: function.                               (* Clight enclosing function *)
    408528  ∀cm_f: internal_function.                             (* enclosing function *)
    409   ∀frame_data: clight_cminor_data cl_f ?? INV.
    410529  ∀rettyp.                                     (* return type of the function *)
    411  
    412   (* ---- Relate Clight continuation to Cminor continuation ---- *)
    413   clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f frame_data rettyp cl_k cm_k →
    414 
    415   (* ---- Other Cminor variables ---- *)
    416   ∀fInv: stmt_inv cm_f (cm_env … frame_data) (f_body cm_f).             (* Cminor invariants *)
    417   ∀sInv: stmt_inv cm_f (cm_env … frame_data) cm_s.
    418   ∀kInv: cont_inv cm_f (cm_env … frame_data) cm_k.
    419 
    420   (* ---- Relate return type variable to actual return type ---- *)
     530  ∀alloc_type.
     531  ∀cl_env, cl_m.
     532  ∀cm_env, cm_m.
     533  ∀stackptr, stacksize. 
     534  (* ---- relate Clight continuation to Cminor continuation ---- *)
     535  clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env rettyp cl_k cm_k →
     536  (* ---- Cminor invariants ---- *)
     537  ∀fInv: stmt_inv cm_f cm_env (f_body cm_f).
     538  ∀sInv: stmt_inv cm_f cm_env cm_s.
     539  ∀kInv: cont_inv cm_f cm_env cm_k.
     540  (* ---- relate return type variable to actual return type ---- *)
    421541  rettyp = opttyp_of_type (fn_return cl_f) →
    422 
    423   (* ---- specification of the contents of clight environment (needed for expr sim) ---- *)
    424 
    425542  (* ---- relate Clight and Cminor functions ---- *)
    426543  ∀func_univ: universe SymbolTag.
     
    428545  ∀Hfresh_function: fn_fresh_for_univ cl_f func_univ.
    429546  translate_function func_univ (globals ?? INV) cl_f Hfresh_globals Hfresh_function = OK ? cm_f →
    430 
    431547  (* ---- relate Clight and Cminor statements ---- *)
    432   ∀stmt_univ,stmt_univ': tmpgen (alloc_type … frame_data).
    433   ∀lbl_univ,lbl_univ' labgen.
    434   ∀lbls:      lenv.
    435   ∀flag:      convert_flag.
     548  ∀stmt_univ,stmt_univ' : tmpgen alloc_type.
     549  ∀lbl_univ,lbl_univ'   : labgen.
     550  ∀lbls                 : lenv.
     551  ∀flag                 : convert_flag.
    436552  ∀Htranslate_inv.
    437   translate_statement (alloc_type … frame_data) stmt_univ lbl_univ lbls flag rettyp cl_s = OK ? «〈stmt_univ',lbl_univ',cm_s〉, Htranslate_inv» →
    438    
    439   clight_cminor_rel cl_ge cm_ge INV
    440     (ClState cl_f cl_s cl_k (cl_env … frame_data) (cl_m … frame_data))
    441     (CmState cm_f cm_s (cm_env … frame_data) fInv sInv (cm_m … frame_data) (stackptr … frame_data) cm_k kInv cm_st)
     553  translate_statement alloc_type stmt_univ lbl_univ lbls flag rettyp cl_s = OK ? «〈stmt_univ',lbl_univ',cm_s〉, Htranslate_inv» → 
     554  (* ---- state additional invariants ---- *) 
     555  ∀Em: embedding.
     556  tmp_vars_well_allocated alloc_type stmt_univ' cm_env cm_m cl_m Em →        (* locals are properly allocated *)
     557  characterise_vars (globals ?? INV) cl_f = 〈alloc_type, stacksize〉 →        (* specify how alloc_type is built *)
     558  (∃m,m'. exec_alloc_variables empty_env m (fn_params cl_f @ fn_vars cl_f) = 〈cl_env,m'〉) → (* spec. Clight env *)
     559  memory_inj Em cl_m cm_m →                                                  (* memory injection *)
     560  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 *)             
     561  (∀b. block_region b = Code → Em b = Some ? 〈b, zero_offset〉) →             (* Force embedding to compute identity on functions *)
     562  clight_cminor_rel cl_ge cm_ge INV
     563    (ClState cl_f cl_s cl_k cl_env cl_m)
     564    (CmState cm_f cm_s cm_env fInv sInv cm_m stackptr cm_k kInv cm_st)
    442565
    443566| CMR_return :
    444   ∀cl_ge, cm_ge, cl_f.
    445   ∀INV:  clight_cminor_inv cl_ge cm_ge.
    446   ∀frame_data: clight_cminor_data cl_f ?? INV.
    447   ∀cl_mem, cm_mem.
    448   cl_mem = cl_m … frame_data →
    449   cm_mem = cm_m … frame_data →
     567  ∀cl_ge, cm_ge.
     568  ∀INV: clight_cminor_inv cl_ge cm_ge.
     569  (*  ∀frame_data: clight_cminor_data cl_f ?? INV.*)
     570  ∀cl_m, cm_m.
    450571  ∀cm_st: stack.                                              (* Cminor stack *)
    451572  clight_cminor_rel cl_ge cm_ge INV
    452     (ClReturnstate Vundef Kstop cl_mem)
    453     (CmReturnstate (None val) cm_mem cm_st)
    454    
    455 | CMR_call :
     573    (ClReturnstate Vundef Kstop cl_m)
     574    (CmReturnstate (None val) cm_m cm_st)
     575
     576| CMR_call_nostore :
     577 (* call to a function with no return value, or which returns in a local variable in Cminor *)
    456578 ∀cl_ge, cm_ge, cl_f, cm_f.
    457  ∀INV: clight_cminor_inv cl_ge cm_ge.
    458  ∀frame_data: clight_cminor_data cl_f cl_ge cm_ge INV.
     579 ∀INV: clight_cminor_inv cl_ge cm_ge.
     580 ∀cl_env, cl_m, cm_env, cm_m, stackptr.
     581 (* TODO: put the actual invariants on memory and etc. here *)
    459582 ∀u: universe SymbolTag.
    460583 ∀cl_fundef, cm_fundef.
     
    463586 ∀rettyp. rettyp = opttyp_of_type (fn_return cl_f) →
    464587 ∀cl_k, cm_k.
    465  clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f frame_data rettyp cl_k cm_k →
    466588 ∀fblock.
    467589 match cl_fundef with
    468590 [ CL_Internal cl_function ⇒
    469    find_funct clight_fundef cl_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? (CL_Internal cl_function) ∧
    470    find_funct (fundef internal_function) cm_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? cm_fundef ∧
    471    translate_fundef u (globals ?? INV) Hglobals_fresh cl_fundef Hfundef_fresh = OK ? cm_fundef
     591    find_funct clight_fundef cl_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? (CL_Internal cl_function) ∧
     592    find_funct (fundef internal_function) cm_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? cm_fundef ∧
     593    translate_fundef u (globals ?? INV) Hglobals_fresh cl_fundef Hfundef_fresh = OK ? cm_fundef ∧
     594    clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env rettyp cl_k cm_k
    472595 | CL_External name argtypes rettype ⇒
    473596   True
    474597 ] →
    475  ∀fptr_block.
     598 ∀cl_fun_id, cm_fun_id.
     599 cl_fun_id = cm_fun_id →
     600 ∀cl_retval, cm_retval.
    476601 ∀sInv, fInv, kInv.
    477602 ∀cl_args_values, cm_args_values.
     603 (* TODO: return_value_rel … INV frame_data cl_retval cm_retval →*)
    478604 (* TODO: add invariant All2 value_eq cl_args_values cm_args_values *)
    479605 ∀cm_stack.
    480606 clight_cminor_rel cl_ge cm_ge INV
    481   (ClCallstate (Vptr (mk_pointer fptr_block zero_offset))
    482    cl_fundef cl_args_values
    483    (Kcall (None (block×offset×type)) cl_f (cl_env ???? frame_data) cl_k)
    484    (cl_m ???? frame_data))
    485   (CmCallstate (Vptr (mk_pointer fptr_block zero_offset)) cm_fundef
    486    cm_args_values (cm_m ???? frame_data)
    487    (Scall (None (ident×typ)) cm_f (stackptr ???? frame_data) (cm_env ???? frame_data) sInv fInv cm_k kInv cm_stack)).
     607  (ClCallstate cl_fun_id
     608   cl_fundef cl_args_values (Kcall cl_retval cl_f cl_env cl_k) cl_m)
     609  (CmCallstate cm_fun_id cm_fundef
     610   cm_args_values cm_m (Scall cm_retval cm_f stackptr cm_env sInv fInv cm_k kInv cm_stack))
     611
     612| CMR_call_store :
     613 (* call to a function which returns to some location in memory in Cminor *)
     614 ∀cl_ge, cm_ge, cl_f, cm_f.
     615 ∀INV: clight_cminor_inv cl_ge cm_ge.
     616 ∀alloc_type, cl_env, cl_m, cm_env, cm_m, stackptr.
     617 (* TODO: put the actual invariants on memory and etc. here *)
     618 ∀u: universe SymbolTag.
     619 ∀cl_fundef, cm_fundef.
     620 ∀Hglobals_fresh: globals_fresh_for_univ type (globals cl_ge cm_ge INV) u.
     621 ∀Hfundef_fresh:  fd_fresh_for_univ cl_fundef u.
     622 ∀rettyp. rettyp = opttyp_of_type (fn_return cl_f) →
     623 ∀cl_k, cm_k.
     624 ∀fblock.
     625 match cl_fundef with
     626 [ CL_Internal cl_function ⇒
     627    find_funct clight_fundef cl_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? (CL_Internal cl_function) ∧
     628    find_funct (fundef internal_function) cm_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? cm_fundef ∧
     629    translate_fundef u (globals ?? INV) Hglobals_fresh cl_fundef Hfundef_fresh = OK ? cm_fundef ∧
     630    clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env rettyp cl_k cm_k
     631 | CL_External name argtypes rettype ⇒
     632   True
     633 ] →
     634 ∀cl_fun_id, cm_fun_id.
     635 cl_fun_id = cm_fun_id →
     636 ∀cl_rettyp, cl_retval, cl_rettrace, cm_retval.
     637 ∀cl_lhs, cm_lhs, Hinvariant_on_cm_lhs.
     638 (* Explain where the lhs of the post-return assign comes from *)
     639 exec_lvalue cl_ge cl_env cl_m cl_lhs = OK ? 〈cl_retval, cl_rettrace〉 →
     640 translate_dest alloc_type cl_lhs = OK ? (MemDest ? «cm_lhs, Hinvariant_on_cm_lhs») →
     641 (* TODO: Explain that the actual variable used to store the ret val is fresh and has the
     642  * right type, etc *)
     643 ∀cm_ret_var.
     644 ∀sInv, fInv, kInv.
     645 ∀cl_args_values, cm_args_values.
     646 (* TODO: return_value_rel … INV frame_data cl_retval cm_retval →*)
     647 (* TODO: add invariant All2 value_eq cl_args_values cm_args_values *)
     648 ∀cm_stack.
     649 clight_cminor_rel cl_ge cm_ge INV
     650  (ClCallstate cl_fun_id
     651   cl_fundef cl_args_values (Kcall (Some ? 〈cl_retval,cl_rettyp〉) cl_f cl_env cl_k) cl_m)
     652  (CmCallstate cm_fun_id cm_fundef
     653   cm_args_values cm_m (Scall cm_retval cm_f stackptr cm_env sInv fInv
     654                          (Kseq (St_store (typ_of_type cl_rettyp) cm_lhs
     655                                          (Id (typ_of_type cl_rettyp) cm_ret_var)) cm_k)
     656                           kInv cm_stack))
     657
     658| CMR_while:
     659 ∀cl_ge,cm_ge,INV,cl_f,cm_f.
     660 ∀cl_env, cl_m, cm_env, cm_m, stackptr.
     661 ∀cl_k, cm_k. 
     662 ∀sz,sg, cl_cond_desc.
     663 ∀cl_body.
     664 ∀entry_label, exit_label.
     665 ∀cm_cond, cm_body.
     666 ∀cm_stack.
     667 ∀kInv: cont_inv cm_f cm_env cm_k.
     668 ∀fInv: stmt_inv cm_f cm_env (f_body cm_f).
     669 ∀sInv: stmt_inv cm_f cm_env
     670           (St_label entry_label
     671            (St_seq
     672             (St_ifthenelse sz sg cm_cond (St_seq cm_body (St_goto entry_label)) St_skip)
     673             (St_label exit_label St_skip))).
     674 (clight_cminor_rel cl_ge cm_ge INV
     675  (ClState cl_f (Swhile (Expr cl_cond_desc (Tint sz sg)) cl_body) cl_k cl_env cl_m)
     676  (CmState cm_f
     677   (St_label entry_label
     678    (St_seq
     679     (St_ifthenelse sz sg cm_cond (St_seq cm_body (St_goto entry_label)) St_skip)
     680     (St_label exit_label St_skip)))
     681   cm_env fInv sInv cm_m stackptr cm_k kInv cm_stack)).   
     682   
    488683
    489684definition clight_normal : Clight_state → bool ≝
     
    498693    (λg. Clight_labelled)
    499694    (λg. Clight_classify)
    500     (λf,g,s,H. 0). (* XXX TODO *)
     695    (λx,y,H. an_identifier ? one). (* XXX TODO *)
    501696
    502697definition cm_pre : preclassified_system ≝
     
    505700    (λg. Cminor_labelled)
    506701    (λg. Cminor_classify)
    507     (λf,g,s,H. 0).   (* XXX TODO *)
    508 
    509 (* Auxilliary lemmas. *)
     702    (λx,y,H. an_identifier ? one).   (* XXX TODO *)
     703
     704(* --------------------------------------------------------------------------- *)
     705(* General purpose auxilliary lemmas. *)
     706(* --------------------------------------------------------------------------- *)
    510707
    511708lemma invert_assert :
     
    623820// qed.
    624821
     822(* --------------------------------------------------------------------------- *)
     823(* Extending simulation results on expressions to particular cases             *)
     824(* --------------------------------------------------------------------------- *)
    625825
    626826lemma translate_expr_sigma_welltyped : ∀vars, cl_expr, cm_expr.
     
    656856
    657857lemma translate_dest_MemDest_simulation :
    658   ∀f.
     858  ∀cl_f  : function.
    659859  ∀cl_ge : genv_t clight_fundef.
    660860  ∀cm_ge : genv_t (fundef internal_function).
    661861  ∀INV   : clight_cminor_inv cl_ge cm_ge.
    662   ∀frame_data : clight_cminor_data f cl_ge cm_ge INV.
     862  ∀alloc_type. 
     863  ∀cl_env, cl_m, cm_env, cm_m, stackptr.
     864  ∀Em.
     865  ∀stacksize     : ℕ. 
     866  ∀alloc_hyp     : characterise_vars (globals ?? INV) cl_f = 〈alloc_type, stacksize〉.
     867  ∀cl_cm_env_hyp : ∃m,m'. exec_alloc_variables empty_env m (fn_params cl_f @ fn_vars cl_f) = 〈cl_env,m'〉.
     868  ∀injection     : memory_inj Em cl_m cm_m.
     869  ∀matching      : memory_matching Em cl_ge cm_ge cl_m cm_m cl_env cm_env INV stackptr alloc_type.
     870  (* decorrelate goal from input using some eqs *)
    663871  ∀cl_expr. ∀cm_expr.
    664872  ∀cl_block, cl_offset, trace.
    665   ∀Hyp_present.
    666      translate_dest (alloc_type … frame_data) cl_expr = OK ? (MemDest ? cm_expr) →
    667      exec_lvalue cl_ge (cl_env … frame_data) (cl_m … frame_data) cl_expr = OK ? 〈〈cl_block, cl_offset〉, trace〉 →
    668      ∃cm_val. eval_expr cm_ge ASTptr cm_expr (cm_env … frame_data) Hyp_present (stackptr … frame_data) (cm_m … frame_data) = OK ? 〈trace, cm_val〉 ∧
    669               value_eq (Em … frame_data) (Vptr (mk_pointer cl_block cl_offset)) cm_val.     
    670 #f #cl_ge #cm_ge #INV #frame_data #cl_expr * #cm_expr #Hexpr_vars #cl_block #cl_offset #trace #Hyp_present
     873  ∀Hyp_present. 
     874     translate_dest alloc_type cl_expr = OK ? (MemDest ? cm_expr) →
     875     exec_lvalue cl_ge cl_env cl_m cl_expr = OK ? 〈〈cl_block, cl_offset〉, trace〉 →
     876     ∃cm_val. eval_expr cm_ge ASTptr cm_expr cm_env Hyp_present stackptr cm_m = OK ? 〈trace, cm_val〉 ∧
     877              value_eq Em (Vptr (mk_pointer cl_block cl_offset)) cm_val.     
     878#cl_f #cl_ge #cm_ge #INV #alloc_type
     879#cl_env #cl_m #cm_env #cm_m #stackptr #Em #stacksize #alloc_hyp #cl_env_hyp #injection #matching
     880#cl_expr * #cm_expr #Hexpr_vars #cl_block #cl_offset #trace #Hyp_present
    671881whd in match (translate_dest ??); cases cl_expr #cl_desc #cl_typ normalize nodelta
    672882cases cl_desc normalize nodelta
     
    678888     #Htranslate_addr
    679889     whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) #Hexec_lvalue
    680      cases (eval_expr_sim cl_ge cm_ge INV ? frame_data) #_ #Hsim
     890     cases (eval_expr_sim cl_ge cm_ge INV cl_f alloc_type stacksize alloc_hyp … cl_env_hyp … injection … matching)
     891     #_ #Hsim
    681892     @(Hsim ??? Hexpr_vars … Htranslate_addr ??? ? Hexec_lvalue) ]
    682893cases (bind2_eq_inversion ?????? Htranslate) -Htranslate *
     
    685896whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
    686897whd in ⊢ ((??%?) → ?);
    687 @(match lookup SymbolTag block (cl_env f cl_ge cm_ge INV frame_data) id
    688   return λx. (lookup SymbolTag block (cl_env f cl_ge cm_ge INV frame_data) id = x) → ?
     898@(match lookup SymbolTag block cl_env id
     899  return λx. (lookup SymbolTag block cl_env id = x) → ?
    689900  with
    690901  [ None ⇒ ?
    691902  | Some loc ⇒ ?
    692   ] (refl ? (lookup SymbolTag block (cl_env f cl_ge cm_ge INV frame_data) id ))) normalize nodelta
     903  ] (refl ? (lookup SymbolTag block cl_env id ))) normalize nodelta
    693904#Hlookup_eq
    694905[ 2,4: #Heq destruct (Heq) whd in match (eval_expr ???????);
    695   [ 2: %{(Vptr (mk_pointer (stackptr f cl_ge cm_ge INV frame_data)
    696                (shift_offset (bitsize_of_intsize I16) zero_offset (repr I16 n))))}
     906  [ 2: %{(Vptr (mk_pointer stackptr (shift_offset (bitsize_of_intsize I16) zero_offset (repr I16 n))))}
    697907       @conj try @refl
    698        lapply (matching … frame_data id) 
     908       lapply (matching id)
    699909       >Hlookup_eq normalize nodelta
    700910       >(opt_to_res_inversion ???? Heq_lookup) normalize nodelta
    701911       #Hembed %4 whd in ⊢ (??%?); >Hembed @refl
    702912  | 1: whd in match (eval_constant ????);
    703        lapply (matching … frame_data id)
     913       lapply (matching id)
    704914       >Hlookup_eq normalize nodelta 
    705915       >(opt_to_res_inversion ???? Heq_lookup) normalize nodelta
     
    713923  whd in match (eval_expr ???????);
    714924  whd in match (eval_constant ????);
    715   lapply (matching … frame_data id)
     925  lapply (matching id)
    716926  [ >Hlookup_eq normalize nodelta >Hfind_symbol_eq normalize nodelta
    717927    #Hembed
     
    724934  | (* A stack variable is not in the local environment but in the global one. *)
    725935    (* we have a contradiction somewhere in the context *)
    726     (* TODO *)
    727     @cthulhu
     936    lapply (variable_not_in_env_but_in_vartypes_is_global ???????
     937              cl_env_hyp alloc_hyp Hlookup_eq … Heq_lookup)
     938    *  #r #Habsurd destruct (Habsurd)
    728939  ]
    729940] qed.
     
    731942(* lift simulation result to eval_exprlist *)
    732943lemma eval_exprlist_simulation :
    733   ∀f.
     944  ∀cl_f.
    734945  ∀cl_ge : genv_t clight_fundef.
    735946  ∀cm_ge : genv_t (fundef internal_function).
    736947  ∀INV   : clight_cminor_inv cl_ge cm_ge.
    737   ∀frame_data : clight_cminor_data f cl_ge cm_ge INV.
     948  ∀alloc_type. 
     949  ∀cl_env, cl_m, cm_env, cm_m, stackptr.
     950  ∀Em.
     951  ∀stacksize     : ℕ. 
     952  ∀alloc_hyp     : characterise_vars (globals ?? INV) cl_f = 〈alloc_type, stacksize〉.
     953  ∀cl_env_hyp : ∃m,m'. exec_alloc_variables empty_env m (fn_params cl_f @ fn_vars cl_f) = 〈cl_env,m'〉.
     954  ∀injection     : memory_inj Em cl_m cm_m.
     955  ∀matching      : memory_matching Em cl_ge cm_ge cl_m cm_m cl_env cm_env INV stackptr alloc_type.
    738956  ∀cl_exprs,cm_exprs.
    739957  ∀cl_results,trace.
    740   exec_exprlist cl_ge (cl_env … frame_data) (cl_m … frame_data) cl_exprs = OK ? 〈cl_results, trace〉 →
    741   mmap_sigma ??? (translate_expr_sigma (alloc_type … frame_data)) cl_exprs = OK ? cm_exprs →
     958  exec_exprlist cl_ge cl_env cl_m cl_exprs = OK ? 〈cl_results, trace〉 →
     959  mmap_sigma ??? (translate_expr_sigma alloc_type) cl_exprs = OK ? cm_exprs →
    742960  ∀H:All ? (λx:𝚺t:typ.expr t.
    743961             match x with
    744962             [ mk_DPair ty e ⇒
    745963                    (expr_vars ty e
    746                      (λid:ident.λty:typ.present SymbolTag val (cm_env … frame_data) id)) ]) cm_exprs.
     964                     (λid:ident.λty:typ.present SymbolTag val cm_env id)) ]) cm_exprs.
    747965  ∃cm_results.
    748966  trace_map_inv … (λe. match e return λe.
     
    750968                         [ mk_DPair _ _ ⇒ ? ] → ?
    751969                       with
    752                        [ mk_DPair ty e ⇒ λp. eval_expr cm_ge ? e (cm_env … frame_data) p (stackptr … frame_data) (cm_m … frame_data) ]) cm_exprs H = OK ? 〈trace, cm_results〉 ∧
    753   All2 ?? (λcl_val, cm_val. value_eq (Em … frame_data) cl_val cm_val) cl_results cm_results.
    754 #f #cl_ge #cm_ge #INV #frame_data #cl_exprs
     970                       [ mk_DPair ty e ⇒ λp. eval_expr cm_ge ? e cm_env p stackptr cm_m ]) cm_exprs H = OK ? 〈trace, cm_results〉 ∧
     971  All2 ?? (λcl_val, cm_val. value_eq Em cl_val cm_val) cl_results cm_results.
     972#f #cl_ge #cm_ge #INV
     973#alloc_type #cl_env #cl_m #cm_env #cm_m #stackptr #Em #stacksize #alloc_hyp #cl_env_hyp #injection #matching
     974#cl_exprs
    755975elim cl_exprs
    756976[ #cm_exprs #cl_results #trace
     
    7811001  lapply (Hind Htranslate_tail (proj2 ?? Hall)) -Hind
    7821002  * #cm_results_tl * #Hcm_exec_tl #Hvalues_eq_tl
    783   cases (eval_expr_sim cl_ge cm_ge INV ? frame_data) #Hsim #_
     1003  cases (eval_expr_sim cl_ge cm_ge INV f alloc_type stacksize alloc_hyp ?? cl_env_hyp ?? Em injection stackptr matching)
     1004  #Hsim #_
    7841005  cases (bind_inversion ????? Htranslate_expr_sigma)
    7851006  * #cmexpr' #Hexpr_vars_local_cm' * #Htranslate
     
    7931014       normalize nodelta >Hcm_exec_tl @refl
    7941015  ]
    795 ] qed. 
     1016] qed.
     1017
     1018(* --------------------------------------------------------------------------- *)
     1019(* Putting the memory injection at work.                                       *)
     1020(* --------------------------------------------------------------------------- *)
     1021
     1022(* A) Non-interference of local variables with memory injections  *)
     1023
     1024(* Needed property:
     1025 * A local variable allocated via the temporary variable generator should not interfere
     1026 * with the memory injection. In particular, we need to show that:
     1027 * 1) we can successfuly store stuff of the right type inside (where the type is specified
     1028 *    at generation time, and should be in the current context)
     1029 * 2) after the store, we can build a consistent memory state and more generally, a
     1030 *    correct [clight_cminor_data] invariant record. Cf. toCminorCorrectnessExpr.ma
     1031 *)
     1032 
     1033(* A.1) memory matchings survives memory injection *)
     1034
     1035lemma offset_plus_0' : ∀o:offset. offset_plus zero_offset o = o.
     1036#o cases o #b >offset_plus_0 @refl
     1037qed.
     1038
     1039(*
     1040lemma store_value_of_type_memory_matching_to_matching : 
     1041  ∀cl_ge, cm_ge, cl_en, cm_en, INV, sp, vars, cl_m, cl_m',cm_m,cm_m'.
     1042  ∀E: embedding.
     1043  ∀blo, blo', delta, off.
     1044  E blo = Some ? 〈blo', delta〉 →
     1045  ∀cl_val, cm_val, ty.
     1046  value_eq E cl_val cm_val →
     1047  storen cl_m (mk_pointer blo off) (fe_to_be_values ty cl_val) = Some ? cl_m' →
     1048  storen cm_m (mk_pointer blo (offset_plus off delta)) (fe_to_be_values ty cm_val) = Some ? cm_m' →
     1049  (lookup' vars var_id = OK (var_type×type) 〈Global r,type_of_var〉)
     1050  memory_inj E cl_m' cm_m' →
     1051  memory_matching E cl_ge cm_ge cl_m cm_m cl_en cm_en INV sp vars →
     1052  memory_matching E cl_ge cm_ge cl_m' cm_m' cl_en cm_en INV sp vars.
     1053#cl_ge #cm_ge #cl_en #cm_en #INV #sp #vars #cl_m #cl_m' #cm_m #cm_m' #E
     1054#blo #blo' #delta #off #Hembed #cl_val #cm_val #ty #Hvalue_eq #Hstoren_cl #Hstoren_cm
     1055#Hinj #Hmatching #id
     1056lapply (Hmatching id)
     1057cases (lookup ?? cl_en id) normalize nodelta
     1058[ 1: #H @H
     1059| 2: #bl cases (lookup ?? vars id) normalize nodelta
     1060  [ 1: #H @H
     1061  | 2: * #var_type #cl_type normalize nodelta
     1062       cases var_type normalize nodelta
     1063       [ #r #H @H
     1064       | #b #H @H
     1065       | #H #v lapply H -H
     1066         @(eq_block_elim … bl blo)
     1067         [ #Heq destruct (Heq)
     1068           @(eq_offset_elim … off zero_offset)
     1069           [ (* We actually load exactly where we wrote, but with a potentially different type. *)
     1070             #Heq destruct (Heq) #H
     1071       ]
     1072  ]
     1073] qed.*)
     1074
     1075
     1076lemma alloc_tmp_in_genlist :
     1077  ∀vartypes. ∀g1, g2, g3.
     1078  ∀id1, ty1, id2, ty2.
     1079  alloc_tmp vartypes ty1 g1 = 〈id1, g2〉 →
     1080  alloc_tmp vartypes ty2 g2 = 〈id2, g3〉 →
     1081  Exists (identifier SymbolTag×type)
     1082   (λx:identifier SymbolTag×type.x=〈id2,ty2〉) (tmp_env ? g3).
     1083#vartypes #g1 #g2 #g3
     1084#id1 #ty1 #id2 #ty2 #Halloc1 #Halloc2
     1085lapply (breakup_dependent_match_on_pairs ?????? Halloc1) * #id1' * #u' * #Hfg1
     1086* #Hfresh_eq generalize in match (fresh_map_add ????????); #ugly
     1087generalize in ⊢ ((??(????(?????%))?) → ?); #ugly2
     1088#Heq destruct (Heq)
     1089lapply (breakup_dependent_match_on_pairs ?????? Halloc2) * #id2' * #u'' * #Hfg2
     1090* #Hfresh_eq' generalize in match (fresh_map_add ????????); #ugly'
     1091generalize in ⊢ ((??(????(?????%))?) → ?); #ugly2'
     1092#Heq destruct (Heq) %1 @refl
     1093qed. (* this last lemma has to be refitted. *)
     1094
     1095(* This, to say the least, is not pretty. Whenever we update the memory, we have to perform
     1096 * a kind of functional record update on the frame_data. But of course, we also need equations
     1097 * relating the old and new frame data. *)
     1098(*
     1099lemma update_clight_cminor_data_cm :
     1100  ∀f, cl_ge, cm_ge, INV.
     1101  ∀frame_data: clight_cminor_data f cl_ge cm_ge INV.
     1102  ∀cl_m_v.
     1103  ∀new_cm_mem.
     1104  cl_m_v = cl_m … frame_data →
     1105  ∀new_inj: memory_inj (Em … frame_data) cl_m_v new_cm_mem.
     1106  ∃data:clight_cminor_data f cl_ge cm_ge INV.
     1107          alloc_type … frame_data = alloc_type … data ∧
     1108          cl_env … frame_data = cl_env … data ∧
     1109          cm_env … frame_data = cm_env … data ∧
     1110          stackptr … frame_data = stackptr … data ∧
     1111          cl_m … frame_data = cl_m … data ∧
     1112          new_cm_mem = (cm_m … data).
     1113#f #cl_ge #cm_ge #INV #frame_data #cl_m_v #new_cm_mem #H destruct (H) #Hinj
     1114%{(mk_clight_cminor_data ????
     1115       (alloc_type … frame_data)
     1116       (stacksize … frame_data)
     1117       (alloc_hyp … frame_data)
     1118       (cl_env … frame_data)
     1119       (cm_env … frame_data)
     1120       (cl_env_hyp … frame_data)
     1121       (cl_m … frame_data)
     1122       new_cm_mem
     1123       (Em … frame_data)
     1124       Hinj
     1125       (stackptr … frame_data)
     1126       (matching … frame_data)
     1127       (Em_fn_id … frame_data))}
     1128@conj try @conj try @conj try @conj try @conj try @refl
     1129qed.*)
     1130
     1131(* Same thing, this time update both CL and CM memory. Here we provide a proof
     1132 * that the data in local env is not touched. *)
     1133(*
     1134lemma update_clight_cminor_data_cl_cm_global :
     1135  ∀f, cl_ge, cm_ge, INV.
     1136  ∀frame_data: clight_cminor_data f cl_ge cm_ge INV.
     1137  ∀new_cl_mem, new_cm_mem.
     1138  ∀new_inj: memory_inj (Em … frame_data) new_cl_mem new_cm_mem. 
     1139  (∀id, b, cl_type.
     1140   lookup ?? (cl_env … frame_data) id = Some ? b →
     1141   lookup ?? (alloc_type … frame_data) id = Some ? 〈Local, cl_type〉 →
     1142   load_value_of_type cl_type (cl_m … frame_data) b zero_offset =
     1143   load_value_of_type cl_type new_cl_mem b zero_offset) → 
     1144  ∃data:clight_cminor_data f cl_ge cm_ge INV.
     1145        alloc_type … frame_data = alloc_type … data ∧
     1146        cl_env … frame_data = cl_env … data ∧
     1147        cm_env … frame_data = cm_env … data ∧
     1148        stackptr … frame_data = stackptr … data ∧
     1149        new_cl_mem = (cl_m … data) ∧
     1150        new_cm_mem = (cm_m … data).
     1151#f #cl_ge #cm_ge #INV #frame_data #new_cl_mem #new_cm_mem #Hinj #Haux
     1152%{(mk_clight_cminor_data ????
     1153       (alloc_type … frame_data)
     1154       (stacksize … frame_data)
     1155       (alloc_hyp … frame_data)
     1156       (cl_env … frame_data)
     1157       (cm_env … frame_data)
     1158       (cl_env_hyp … frame_data)
     1159       new_cl_mem
     1160       new_cm_mem
     1161       (Em … frame_data)
     1162       Hinj
     1163       (stackptr … frame_data)
     1164       ? (* (matching … frame_data) *)
     1165       (Em_fn_id … frame_data))}
     1166[ whd #id
     1167  lapply (matching … frame_data id)
     1168  lapply (Haux id)
     1169  cases (lookup ??? id) normalize nodelta
     1170  [ #_ #H @H
     1171  | #b cases (lookup ??? id) normalize nodelta
     1172    [ #_ #H @H
     1173    | * #vartype #cltype normalize nodelta
     1174      cases vartype try // normalize nodelta #Haux
     1175      #H #v #Hload @H >(Haux ?? (refl ??) (refl ??)) @Hload
     1176    ]
     1177  ]
     1178|
     1179@conj try @conj try @conj try @conj try @conj try @conj try @refl
     1180qed.*)
     1181
     1182lemma store_value_of_type_success_by_value :
     1183   ∀ty, m, m', b, o, v.
     1184   store_value_of_type ty m b o v = Some ? m' →
     1185   access_mode ty = By_value (typ_of_type ty) ∧
     1186   storev (typ_of_type ty) m (Vptr (mk_pointer b o)) v = Some ? m'.   
     1187#ty #m #m' #b #o #v
     1188cases ty
     1189[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
     1190| #structname #fieldspec | #unionname #fieldspec | #id ]
     1191whd in ⊢ ((??%?) → ?);
     1192[ 1,4,5,6,7: #Habsurd destruct (Habsurd) ]
     1193#H @conj try @refl @H
     1194qed.
     1195
     1196(* Some boilerplate to avoid performing a case analysis on exprs in the middle of
     1197 * the proof. *)
     1198lemma translate_dest_not_Evar_id :
     1199  ∀vars, ed, ty.
     1200  (∀id. ed ≠ Evar id) →
     1201    translate_dest vars (Expr ed ty) =
     1202    (do e1' ← translate_addr vars (Expr ed ty);
     1203     OK ? (MemDest ? e1')).
     1204#vars *
     1205[ #sz #i | #id | #e1 | #e1 | #op #e1 |#op #e1 #e2 | #cast_ty #e1
     1206| #cond #iftrue #iffalse | #e1 #e2 | #e1 #e2 | #sizeofty | #e1 #field | #cost #e1 ]
     1207#ty #H
     1208[ 2: @False_ind @(absurd … (refl ??) (H ?)) ]
     1209@refl
     1210qed.
     1211
     1212lemma expr_is_Evar_id_dec :
     1213  ∀ed. (∀id. ed ≠ Evar id) ∨ (∃id. ed = Evar id).
     1214
     1215[ #sz #i | #id | #e1 | #e1 | #op #e1 |#op #e1 #e2 | #cast_ty #e1
     1216| #cond #iftrue #iffalse | #e1 #e2 | #e1 #e2 | #sizeofty | #e1 #field | #cost #e1 ]
     1217[ 2: %2 %{id} @refl
     1218| *: %1 #id % #Habsurd destruct (Habsurd) ]
     1219qed.
     1220
     1221(* Not provable: need to relate (typeof (e=Evar id, ty)) with the type contained
     1222   in var_ty. Should be doable, but not now. *)
     1223(*   
     1224lemma translate_dest_IdDest_typ :
     1225  ∀vars,e,var_id,var_ty,H.
     1226    translate_dest vars e = return (IdDest vars var_id var_ty H) →
     1227    var_ty = typeof e.
     1228#vars * #ed #ety #var_id #var_ty #H
     1229cases ed   
     1230[ #sz #i | #id | #e1 | #e1 | #op #e1 |#op #e1 #e2 | #cast_ty #e1
     1231| #cond #iftrue #iffalse | #e1 #e2 | #e1 #e2 | #sizeofty | #e1 #field | #cost #e1 ]
     1232[ 2,3,12:
     1233  [ 2,3:
     1234    whd in ⊢ ((??%?) → ?);
     1235    cases (translate_addr ??) normalize nodelta
     1236    [ 2,3: #error whd in ⊢ ((??%%) → ?); #Habsurd destruct (Habsurd)
     1237    | 1,4: #Hfoo whd in ⊢ ((??%%) → ?); #Habsurd destruct (Habsurd) ]
     1238  | 1: #H' lapply (bind2_eq_inversion ?????? H') * #vt * #t * #Eq
     1239    lapply Eq inversion vt normalize nodelta
     1240    [ 1,2: #foo #bar #Hlookup
     1241      whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
     1242    | 3: #e whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
     1243| *: whd in ⊢ ((??%?) → ?); whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd)
     1244normalize nodelta
     1245[ 2:*)
     1246
     1247
     1248lemma mk_offset_offv_id : ∀o. mk_offset (offv o) = o.
     1249* #x @refl qed.
     1250
     1251lemma find_funct_to_find_funct_id :
     1252   ∀F, ge, ptr, fundef.
     1253   ∀H:find_funct ? ge ptr = Some ? fundef.
     1254   find_funct_id F ge ptr = Some ? 〈fundef, symbol_of_function_val' F ge ptr fundef H〉.
     1255#F #ge #ptr #fundef #Hfind whd in match (find_funct_id ???);
     1256generalize in ⊢ (??(?%)?);
     1257generalize in ⊢
     1258 ((???%) → (??
     1259    (match %
     1260(*     return λ_. (??%?) → ?*)
     1261     with
     1262     [ _ ⇒ λ_. ?
     1263     | _ ⇒ λ_.λ_. ? ] ?)
     1264  ?));
     1265#o cases o normalize nodelta
     1266[ #H @False_ind >Hfind in H; #Habsurd destruct (Habsurd)
     1267| #f #Hfind' 
     1268  cut (f = fundef)
     1269  [ >Hfind in Hfind'; #Heq destruct (Heq) @refl ]
     1270  #Heq destruct (Heq)
     1271  @refl
     1272] qed.
     1273
     1274(* --------------------------------------------------------------------------- *)
     1275(* Main simulation results                                                     *)
     1276(* --------------------------------------------------------------------------- *)
    7961277
    7971278(* Conjectured simulation results
     
    8241305#g1 #g2 #INV #s1 #s1' #Hstate_rel #Hclight_normal #Hnot_labeleld
    8251306inversion Hstate_rel
     1307[ 1: (* Normal state *)
     1308     (* ---------------------------------------------------------------------- *)
    8261309#cl_ge #cm_ge #INV' #cl_s
    8271310(* case analysis on Clight statement *)
     
    8311314| 14: #lab | 15: #cost #body ]
    8321315[ 3: (* Call *)
    833      #cm_s #cl_k #cm_k #cm_st #cl_f #cm_f #frame_data #rettyp #Hcont_rel
     1316     #cm_s #cl_k #cm_k #cm_st #cl_f #cm_f #rettyp
     1317     #alloc_type #cl_env #cl_m #cm_env #cm_m #stackptr #stacksize #Hcont_rel
    8341318     (* introduce everything *)
    835      #fInv #sInv #kInv
    836      #Htarget_type #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function
     1319     #fInv #sInv #kInv #Htarget_type #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function
    8371320     #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls
    838      #flag * * * * #Hstmt_inv #Hlabels_translated #Htmps_preserved
    839      #Hreturn_ok #Hlabel_wf
     1321     #flag * * * * #Hstmt_inv #Hlabels_translated #Htmps_preserved #Hreturn_ok #Hlabel_wf
    8401322     (* generalize away ugly proof *)
    8411323     generalize in ⊢ (∀_:(???(??(????%))).?); #Hugly
    842      #Htranslate
     1324     #Htranslate #Em
     1325     #Htmp_vars_well_allocated
     1326     #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id
    8431327     @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
    8441328     destruct (HA HB)
     
    8541338     #Heq_ef_ef' #Htranslate
    8551339     cases (bind_inversion ????? Htranslate) -Htranslate *
    856      #args #Hall_variables_from_args_local *
     1340     #cm_args #Hall_variables_from_args_local *
    8571341     whd in ⊢ ((???%) → ?); #Hargs_spec
    858      cases retv normalize nodelta
     1342     @(match retv
     1343       return λx. retv = x → ?
     1344       with
     1345       [ None ⇒ λHretv. ?
     1346       | Some lhs ⇒ λHretv. ?
     1347       ] (refl ? retv))
     1348     normalize nodelta
    8591349     [ 2: (* return something *)
    860        #lhs #Hdest
    861        cases (bind_inversion ????? Hdest) -Hdest #dest *
     1350       #Hdest cases (bind_inversion ????? Hdest) -Hdest #dest *
    8621351       inversion dest normalize nodelta
    8631352       [ (* register dest *) #var_id #var_ty #His_local @(jmeq_absorb ?????) #Hdest       
     
    8671356       | * #cm_expr #Hexpr_vars_cm #Hdest #Htranslate_dest #Hgensym
    8681357         lapply (breakup_dependent_match_on_pairs ?????? Hgensym) -Hgensym
    869          * #ret_var * #new_gensym * #Heq_alloc_tmp * #Halloc_tmp #Hgensym
     1358         * #ret_var * #new_gensym * #Heq_alloc_tmp * #_ #Hgensym
    8701359         lapply (breakup_dependent_match_on_pairs ?????? Hgensym) -Hgensym
    871          * #tmp_var * #new_gensym' * #Heq_alloc_tmp' * #Halloc_tmp'         
     1360         * #tmp_var * #new_gensym' * #Heq_alloc_tmp' * #_
    8721361         generalize in ⊢ ((??(?? (????%) )?) → ?); #Hstmt_inv_after_gensym
    8731362         whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
     
    8831372     #args_values #args_trace * #Hexec_arglist #Htranslate
    8841373     cases (bindIO_inversion ??????? Htranslate) -Htranslate
    885      #cl_fundef * #Hfind_funct
     1374     * #cl_fundef #cl_fun_id * #Hfind_funct
    8861375     lapply (opt_to_io_Value ?????? Hfind_funct) -Hfind_funct #Hfind_funct
    8871376     cases (find_funct_inversion ???? Hfind_funct)
     
    8951384            cases (bindIO_inversion ??????? Htranslate) -Htranslate * *
    8961385            #lblock #loffset #ltrace *
    897             #Hexec_lvalue
    898             [ 1: (* empty trace *) @cthulhu (* TODO wip *)
    899             | 2: @cthulhu (* TODO wip *)
    900             ]
    901      | 3: @cthulhu ]
    902      (* TODO wip  *)
    903  (*     
     1386            whd in ⊢ ((???%) → (???%) → ?);
     1387            [ >Hlhs_eq #Hexec_lvalue
     1388              cut (ltrace = [])
     1389              [ lapply (res_to_io ????? Hexec_lvalue)
     1390                #H' whd in H':(??%?); cases (lookup ????) in H'; normalize nodelta
     1391                [ 2: #b #Heq destruct (Heq) @refl
     1392                | #H cases (bind_inversion ????? H) #H24 * #H27 #H28
     1393                  whd in H28:(???%); destruct (H28) @refl ]
     1394              ] #H destruct (H)
     1395            | #Hexec_lvalue ]
     1396     | 3: ]
    9041397     whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
    905        [ 1: >Hlhs_eq in Hexec_lvalue; #Hexec_lvalue %{1}
    906        | 2: (* Execute Cminor part: evaluate lhs, evaluate assign *)
    907             %{2} whd whd in ⊢ (??%?); normalize nodelta
    908             whd in match (eval_expr ???????);
    909             whd in match (m_bind ?????);
    910             lapply (Hsim_expr … Htranslate_ef … Hexpr_vars_present_ef … Hexec_func_ptr)
    911             -Hsim_expr * #cm_func_ptr_val * #Heval_func #Hvalue_eq_func
    912            
    913        | 3:
    914        ]
    915        (* execute Cminor part *)
    916        [ %{1} | %{2} | %{1} ]
    917        whd whd in ⊢ (??%?); normalize nodelta
    918        [ 1: generalize in match (proj2 (present ????) (expr_vars ???) (proj1 ???));
    919        | 2: generalize in match (proj2 (present ????) (expr_vars ???) (proj1 ???));
    920        | 3: generalize in match (proj2 True ??); ]
    921        #Hexpr_vars_present_ef'
    922        cases (eval_expr_sim … frame_data) #Hsim_expr #_
     1398     [ 1: %{1} whd whd in ⊢ (??%?); normalize nodelta
     1399     | 2: (* Execute Cminor part: evaluate lhs, evaluate assign *)
     1400          %{5} whd whd in ⊢ (??%?); normalize nodelta
     1401          whd in match (eval_expr ???????);
     1402          whd in match (m_bind ?????);
     1403          cut (expr_vars ASTptr cm_expr
     1404                  (λid:ident.λty:typ.present SymbolTag val cm_env id))
     1405          [ cases sInv * * * * * * * #_ #H #_ #_ #_ @H ] #Hexpr_vars_cut
     1406          lapply (translate_dest_MemDest_simulation … Htranslate_dest Hexec_lvalue)
     1407          try assumption try @refl
     1408          * #cm_val_tmp * #Heval_expr_tmp >Heval_expr_tmp #Hvalue_eq
     1409          normalize nodelta generalize in match (proj1 ???); #Htmp_var_present
     1410          cases (value_eq_ptr_inversion … Hvalue_eq) #cm_ptr * #Hcm_val_tmp #Hcm_ptr_translation
     1411          >Hcm_val_tmp
     1412          lapply (Htmp_vars_well_allocated … tmp_var Htmp_var_present (Tpointer (typeof lhs)) ? (Vptr cm_ptr) ?)
     1413          [ 2: @(alloc_tmp_in_genlist … (sym_eq ??? Heq_alloc_tmp) (sym_eq ??? Heq_alloc_tmp'))
     1414          | 1: normalize cases cm_ptr #b #o %3 ]
     1415          * #cm_mem_after_store * #Hstorev #Hnew_inj >Hstorev
     1416          whd in match (m_bind ?????); normalize nodelta
     1417          whd whd in ⊢ (??%?); normalize nodelta
     1418(*          cases (update_clight_cminor_data_cm … frame_ … Hnew_inj)
     1419          try assumption #frame_data'
     1420          * * * * * #Halloctype_eq_frame_data #Hcl_env_eq_frame_data #Hcm_env_eq_frame_data
     1421          #Hstackptr_eq_frame_data #Hcl_m_eq_frame_data #Hcm_m_eq_frame_data *)
     1422     | 3: %{1} whd whd in ⊢ (??%?); normalize nodelta
     1423     ]
     1424    (* execute Cminor part *)
     1425    [ 1: generalize in match (proj2 (present ????) (expr_vars ???) (proj1 ???));
     1426    | 2: generalize in match (proj2 (present ????) (expr_vars ???) (proj1 ???));
     1427    | 3: generalize in match (proj2 True ??); ]
     1428    #Hexpr_vars_present_ef'
     1429    [ 1,3:
     1430       cases (eval_expr_sim … INV' … Halloc_hyp … Hcl_env_hyp … Hinjection … Hmatching) #Hsim_expr #_
    9231431       cut (expr_vars (typ_of_type (typeof func)) ef
    924              (λid:ident.λty:typ.present SymbolTag val (cm_env cl_f cl_ge cm_ge INV' frame_data) id))
    925        [ 1,3,5: lapply Heq_ef_ef' lapply Hexpr_vars_ef lapply ef >Htyp_equality_ef
     1432             (λid:ident.λty:typ.present SymbolTag val cm_env id))
     1433       [ 1,3: lapply Heq_ef_ef' lapply Hexpr_vars_ef lapply ef >Htyp_equality_ef
    9261434                #ef #Hexpr_vars_ef @(jmeq_absorb ?????) #Heq destruct (Heq)
    9271435                @Hexpr_vars_present_ef' ]
    928        #Hexpr_vars_present_ef           
    929        (* use simulation lemma on expressions for function *)
     1436       #Hexpr_vars_present_ef
    9301437       lapply (Hsim_expr … Htranslate_ef … Hexpr_vars_present_ef … Hexec_func_ptr)
    9311438       -Hsim_expr * #cm_func_ptr_val * #Heval_func #Hvalue_eq_func
    932        cut (eval_expr cm_ge ASTptr ef'
    933              (cm_env cl_f cl_ge cm_ge INV' frame_data) Hexpr_vars_present_ef'
    934              (stackptr cl_f cl_ge cm_ge INV' frame_data)
    935              (cm_m cl_f cl_ge cm_ge INV' frame_data)
    936                =OK (trace×val) 〈func_trace,cm_func_ptr_val〉)
    937        [ 1,3,5:
     1439       cut (eval_expr cm_ge ASTptr ef' cm_env Hexpr_vars_present_ef'
     1440             stackptr cm_m = OK (trace×val) 〈func_trace,cm_func_ptr_val〉)
     1441       [ 1,3:
    9381442         lapply Heq_ef_ef' lapply Heval_func lapply Hexpr_vars_ef lapply Hexpr_vars_local_ef'
    9391443         lapply Hexpr_vars_present_ef lapply ef lapply Hexpr_vars_present_ef' lapply ef'
     
    9411445         @(jmeq_absorb ?????) #Heq destruct (Heq) @HE ]
    9421446       -Heval_func #Heval_func >Heval_func
    943        whd in match (m_bind ?????);
    944        lapply (trans_fn … INV' … Hfind_funct)
    945        * #tmp_u * #cminor_fundef * #Hglobals_fresh_for_tmp_u * #Hfundef_fresh_for_tmp_u *
    946        #Htranslate_fundef #Hfind_funct_cm
    947        lapply (value_eq_ptr_inversion … Hvalue_eq_func) * #cm_func_ptr * #Hcm_func_ptr
    948        whd in ⊢ ((??%?) → ?); cases func_ptr in Hfind_funct Hfind_funct_cm Hregion_is_code Hpoff_eq_zero;
    949        #cm_block #cm_off #Hfind_funct #Hfind_funct_cm #Hregion_is_code #Hpoff_eq_zero destruct (Hpoff_eq_zero)
    950        whd in ⊢ ((??%?) → ?); >(Em_fn_id … frame_data … cm_block Hregion_is_code)
    951        normalize nodelta cases cm_func_ptr in Hcm_func_ptr; #cm_block' #cm_off'
    952        #Hcm_func_ptr #Heq destruct (Hcm_func_ptr Heq) >addition_n_0
    953        >Hfind_funct_cm
    954        whd in match (opt_to_res ???); normalize nodelta
    955        cut (All (𝚺t:typ.CMexpr t)
    956               (λx:𝚺t:typ.expr t.(
    957                 match x with
    958                 [ mk_DPair ty e ⇒
    959                  expr_vars ty e
    960                    (λid:ident
    961                     .λty0:typ.present SymbolTag val (cm_env cl_f cl_ge cm_ge INV' frame_data) id)])) args)
    962        [ 1: cases sInv * * normalize nodelta * #_ #_ #Hall #_ #_ @Hall
    963        | 3: cases sInv * * * * * * * normalize nodelta * #_ #_ #Hall #_ #_ #_ @Hall
    964        | 5: cases sInv * * normalize nodelta * #_ #_ #Hall #_ #_ @Hall ]
    965        #Hall
    966        cases (eval_exprlist_simulation … frame_data ???? Hexec_arglist Hargs_spec Hall)
    967        #cm_values * #Hcm_exec_list #Hcl_cm_values_eq >Hcm_exec_list
    968        whd in match (m_bind ?????); normalize nodelta whd  (* TODO here bug in toCminor to be fixed before going on *) @conj
    969        [ 2,4,6: #Habsurd destruct (Habsurd) ]
    970        @conj try @refl
    971        generalize in match (proj1 True (expr_vars ???) (proj1 ???));
    972        * @(CMR_call … tmp_u) try assumption normalize nodelta
    973        (* a dependency somewhere prevents case analysis *)
    974        lapply Hfind_funct lapply Hfind_funct_cm lapply Htranslate_fundef lapply Hfundef_fresh_for_tmp_u
    975        cases cl_fundef
    976        [ 2: #H1 #H2 #H3 #H4 #H5 #H6 #H7 @I
    977        | 1: #H9 #H10 #H11 #H12 #H13 @conj try @conj try // ]
    978      | (* return something *)
    979        #lhs #Hdest
    980        cases (bind_inversion ????? Hdest) -Hdest #dest *
    981        inversion dest normalize nodelta
    982        [ (* register dest *) #var_id #var_ty #His_local @(jmeq_absorb ?????) #Hdest
    983          #Htranslate_dest whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
    984           generalize in match (conj ???);
    985      ]
    986    
    987          
    988          whd in match (proj1 ???); whd in match (proj2 ???);
    989          
    990          
    991          [ 2: cases sInv * * normalize nodelta * #_ #_ #Hall #_ #_ @Hall ]
    992          
    993          >Hfind_funct_cm
    994          (* case split away the invariants *)
    995          cases sInv * * normalize nodelta * * #Hexpr_vars_ef' #Hall_args_present
    996          whd in ⊢ (% → ?); * * normalize nodelta * #Heval_expr #Hvalue_eq
    997          >Heval_expr
    998          *
    999    
    1000 [ 1: (* Skip *)
    1001      #cm_s #cl_k #cm_k #cm_st #cl_f #cm_f #frame_data #rettyp #Hcont_rel
    1002      (* case analysis on continuation *)
    1003      inversion Hcont_rel
    1004      [ (* Kstop continuation *)
    1005        (* simplifying the goal using outcome of the inversion *)
    1006        #kcl_ge #kcm_ge #kINV #kcl_f #kcm_f #kframe_data #ktarget_type
    1007        @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
    1008        destruct (HA HB)
    1009        @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
    1010        destruct (HC HD HE)
    1011        @(jmeq_absorb ?????) #HF @(jmeq_absorb ?????) #HG @(jmeq_absorb ?????) #HH @(jmeq_absorb ?????) #HI
    1012        destruct (HF HG HH HI) #_
    1013        (* introduce everything *)
    1014        #fInv #sInv #kInv
    1015        #Htarget_type #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function
    1016        #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls
    1017        #flag * * * * #Hstmt_inv #Hlabels_translated #Htmps_preserved
    1018        #Hreturn_ok #Hlabel_wf
    1019        (* reduce statement translation function *)
    1020        whd in ⊢ ((??%?) → ?);
    1021        #Heq_translate
    1022        (* In this simple case, trivial translation *)
    1023        destruct (Heq_translate)
    1024        @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
    1025        destruct (HA HB)
    1026        @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
    1027        destruct (HC HD HE) #_
    1028        (* unfold the clight execution *)
    1029        #s2 #tr whd in ⊢ ((??%?) → ?);
    1030        inversion (fn_return kcl_f) normalize nodelta
    1031        normalize nodelta
    1032        [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
    1033        | #structname #fieldspec | #unionname #fieldspec | #id ]
    1034        #Hfn_return whd in ⊢ ((??%?) → ?); #Heq destruct (Heq)
    1035        %{1} whd @conj try @conj try @refl
    1036        [ 2: #Habsurd destruct (Habsurd) ]
    1037        %2{kcl_f}
    1038        [ %{ (alloc_type … kframe_data)
    1039             (stacksize … kframe_data)
    1040             (alloc_hyp … kframe_data)
    1041             (cl_env … kframe_data)
    1042             (cm_env … kframe_data)
    1043             (cl_env_hyp … kframe_data)
    1044             (free_list (cl_m … kframe_data) (blocks_of_env (cl_env … kframe_data)))
    1045             (free (cm_m … kframe_data) (stackptr … kframe_data))
    1046             (Em … kframe_data)
    1047             ? (* injection *)
    1048             (stackptr … kframe_data)
    1049             ? (* matching *)}
    1050          [ @(freelist_memory_inj_m1_m2 … (injection … kframe_data) (blocks_of_env (cl_env … kframe_data)) (stackptr … kframe_data))
    1051            [ 2,3: @refl
    1052            |
    1053  
    1054      @cthulhu
    1055     | (* KSeq continuation *)
    1056       #gcl_ge #kcm_ge #kINV #kcl_f #kcm_f #kframe_data #ktarget_type #kcl_s #kcm_s #kcl_k' #kcm_k'
    1057       #kstmt_univ #kstmt_univ' #klbl_univ #klbl_univ' #klbls #kflag
     1447    | 2: (* treat case 2 as special, since the type differs slightly *)
     1448       cases (eval_expr_sim … INV' … Halloc_hyp ? cm_env Hcl_env_hyp … Hnew_inj stackptr Hmatching)
     1449       #Hsim_expr #_
     1450       generalize in match (proj2 ???); #Hall_present
     1451       generalize in match (proj1 ???); #Hret_present
     1452       generalize in match (proj2 ???); #Hstore_inv
     1453       generalize in match (conj ????); #Hstmt_inv
     1454       cut (eval_expr cm_ge ? ef' cm_env ? stackptr cm_m =
     1455            (eval_expr cm_ge ASTptr ef' cm_env ? stackptr cm_m)) try assumption try @refl
     1456       #Heval_expr_rewrite >Heval_expr_rewrite -Heval_expr_rewrite
     1457       lapply (Hsim_expr … Htranslate_ef … (Vptr func_ptr) func_trace ??)       
     1458       try assumption
     1459       [ lapply Hexpr_vars_present_ef' lapply Heq_ef_ef' lapply Hexpr_vars_ef lapply Hexpr_vars_local_ef'
     1460         lapply ef >Htyp_equality_ef #ef #HA #HB @(jmeq_absorb ?????) #Heq destruct (Heq) #x @x ]
     1461       * #cm_func_ptr_val * #Heval_func_cm #Hvalue_eq_func
     1462       (* And some more shuffling types around to match the goal *)
     1463       cut (eval_expr cm_ge ? ef' cm_env Hexpr_vars_present_ef' stackptr cm_mem_after_store = OK ? 〈func_trace,cm_func_ptr_val〉)
     1464       [ lapply Heval_func_cm -Heval_func_cm
     1465         generalize in ⊢ ((??(?????%??)?) → ?);
     1466         lapply Heq_ef_ef' -Heq_ef_ef'
     1467         lapply Hexpr_vars_ef -Hexpr_vars_ef
     1468         lapply Hexpr_vars_local_ef' -Hexpr_vars_local_ef'
     1469         lapply Hexpr_vars_present_ef'
     1470         lapply ef >Htyp_equality_ef #ef0 #HA #HB #HC @(jmeq_absorb ?????)
     1471         #Heq destruct (Heq) #H1 #H2 @H2 ]
     1472       #Heval_cm_func >Heval_cm_func ]
     1473    whd in match (m_bind ?????);
     1474    lapply (trans_fn … INV' … Hfind_funct)
     1475    * #tmp_u * #cminor_fundef * #Hglobals_fresh_for_tmp_u * #Hfundef_fresh_for_tmp_u *
     1476    #Htranslate_fundef #Hfind_funct_cm
     1477    lapply (value_eq_ptr_inversion … Hvalue_eq_func) * #cm_func_ptr * #Hcm_func_ptr
     1478    whd in ⊢ ((??%?) → ?); cases func_ptr in Hfind_funct Hfind_funct_cm Hregion_is_code Hpoff_eq_zero;
     1479    #cm_block #cm_off #Hfind_funct #Hfind_funct_cm #Hregion_is_code #Hpoff_eq_zero destruct (Hpoff_eq_zero)
     1480    whd in ⊢ ((??%?) → ?);
     1481    [ 1,2: >(HEm_fn_id … cm_block Hregion_is_code)
     1482    | 3: >(HEm_fn_id … cm_block Hregion_is_code) ]
     1483    normalize nodelta cases cm_func_ptr in Hcm_func_ptr; #cm_block' #cm_off'
     1484    #Hcm_func_ptr #Heq destruct (Hcm_func_ptr Heq)
     1485    [ 1,2: >addition_n_0 >mk_offset_offv_id
     1486    | 3: ]
     1487    >(find_funct_to_find_funct_id ???? Hfind_funct_cm)
     1488    whd in match (opt_to_res ???); normalize nodelta
     1489    (* Again, isolate cases by type similarity *)
     1490    [ 1,2:
     1491      cut (All (𝚺t:typ.CMexpr t)
     1492            (λx:𝚺t:typ.expr t.(
     1493              match x with
     1494              [ mk_DPair ty e ⇒
     1495               expr_vars ty e
     1496                 (λid:ident
     1497                  .λty0:typ.present SymbolTag val cm_env id)])) cm_args)
     1498      [ 1: cases sInv * * normalize nodelta * #_ #_ #Hall #_ #_ @Hall
     1499      | 3: cases sInv * * normalize nodelta * #_ #_ #Hall #_ #_ @Hall ]
     1500      #Hall
     1501      cases (eval_exprlist_simulation …  Halloc_hyp Hcl_env_hyp Hinjection Hmatching ???? Hexec_arglist Hargs_spec Hall)
     1502      #cm_values * #Hcm_exec_list #Hcl_cm_values_eq >Hcm_exec_list
     1503    | 3:
     1504      (* Arrrgh *)
     1505      lapply (eval_exprlist_simulation …  Halloc_hyp Hcl_env_hyp Hnew_inj ????? Hexec_arglist Hargs_spec ?)
     1506      try assumption *
     1507      #cm_values * #Hcm_exec_list #Hcl_cm_values_eq >Hcm_exec_list
     1508    ]
     1509    whd in match (m_bind ?????); normalize nodelta whd @conj
     1510    [ 2,4,6: #Habsurd destruct (Habsurd) ]
     1511    @conj
     1512    [ 1,3,5: normalize try @refl
     1513             >append_nil >append_nil @refl ]
     1514    [ 1: generalize in match (proj1 ? (expr_vars ???) (proj1 ???)); #Hugly_pres
     1515    | 2: generalize in match (proj1 ? (expr_vars ???) (proj1 ???)); #Hugly_pres
     1516    | 3: ]
     1517(*    [ 3: >addition_n_0 ]*)
     1518    [ 1,2: (* no return or return to CM local variable *)
     1519           @(CMR_call_nostore … tmp_u) try assumption
     1520           [ 2,4: (* TODO: prove matching between CL and CM function ids *)
     1521                  @cthulhu
     1522           ]
     1523           lapply Hfind_funct
     1524           lapply Hfind_funct_cm
     1525           lapply Htranslate_fundef
     1526           lapply Hfundef_fresh_for_tmp_u
     1527           lapply Hassert_type_eq
     1528           lapply Htype_of_fundef
     1529           lapply Hlookup
     1530           cases cl_fundef
     1531           [ 2,4: #id #typel #ty #HA #HB #HC #HD #HE #HF #HG @I
     1532           | 1,3: #f #HA #HB #HC #HD #HE #HF #HG normalize nodelta
     1533                  @conj try @conj try @conj try assumption ]
     1534    | 3: (* type mismatch *)
     1535         @(CMR_call_store … tmp_u) try assumption
     1536         [ 2: (* TODO: prove matching between CL and CM function ids *)
     1537              @cthulhu ]
     1538         lapply Hfind_funct
     1539         lapply Htranslate_fundef
     1540         lapply Hfundef_fresh_for_tmp_u
     1541         lapply Hassert_type_eq
     1542         lapply Htype_of_fundef
     1543         lapply Hlookup
     1544         cases cl_fundef
     1545         [ 2: #id #typel #ty #HA #HB #HC #f #HD #HE @I ]
     1546         #f #HA #HB #HC #HD #HE #HF normalize nodelta @conj try @conj try @conj
     1547         try assumption
     1548    ]
     1549| 1: (* Skip *)
     1550    #cm_s #cl_k #cm_k #cm_st #cl_f #cm_f #rettyp
     1551    #alloc_type #cl_env #cl_m #cm_env #cm_m #stackptr #stacksize #Hcont_rel
     1552    (* case analysis on continuation *)
     1553    inversion Hcont_rel
     1554    [ (* Kstop continuation *)
     1555      (* simplifying the goal using outcome of the inversion *)
     1556      #kcl_ge #kcm_ge #kINV #kcl_f #kcm_f #ktarget_type #kcl_env #kcm_env
     1557      @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
     1558      destruct (HA HB)
     1559      @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
     1560      destruct (HC HD HE)
     1561      @(jmeq_absorb ?????) #HF @(jmeq_absorb ?????) #HG @(jmeq_absorb ?????) #HH
     1562      @(jmeq_absorb ?????) #HI @(jmeq_absorb ?????) #HJ
     1563      destruct (HF HG HH HI HJ) #_
     1564      (* introduce everything *)
     1565      #fInv #sInv #kInv
     1566      #Htarget_type #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function
     1567      #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls
     1568      #flag * * * * #Hstmt_inv #Hlabels_translated #Htmps_preserved
     1569      #Hreturn_ok #Hlabel_wf generalize in match (conj ????); #Hugly
     1570      (* reduce statement translation function *)
     1571      whd in ⊢ ((??%?) → ?);
     1572      #Heq_translate
     1573      (* In this simple case, trivial translation *)
     1574      destruct (Heq_translate)
     1575      #Em #Htmp_vars_well_allocated #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id
     1576      @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
     1577      destruct (HA HB)
     1578      @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
     1579      destruct (HC HD HE) #_
     1580      (* unfold the clight execution *)
     1581      #s2 #tr whd in ⊢ ((??%?) → ?);
     1582      inversion (fn_return kcl_f) normalize nodelta
     1583      [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
     1584      | #structname #fieldspec | #unionname #fieldspec | #id ]
     1585      #Hfn_return whd in ⊢ ((??%?) → ?); #Heq destruct (Heq)
     1586      %{1} whd @conj try @conj try @refl
     1587      [ 2: #Habsurd destruct (Habsurd) ]
     1588      @CMR_return
     1589    | #kcl_ge #kcm_ge #kINV #kcl_f #kcm_f #ktarget_type #kalloc_type #kcl_s #kcm_s
     1590      #kcl_env #kcm_env #kcl_k' #kcm_k' #kstmt_univ #kstmt_univ' #klbl_univ #klbl_univ' #klbls #kflag
    10581591      * * * * #kHstmt_inv #kHlabels_translated #kHtmps_preserved
    10591592      #kHreturn_ok #kHlabel_wf #kHeq_translate #kHcont_rel #_
     
    10621595      @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
    10631596      destruct (HC HD HE)
    1064       @(jmeq_absorb ?????) #HF
    1065      
    1066       #Heq_INV #Heq_cl_f #Heq_cm_f #Heq_frame #Heq_rettyp #Heq_cl_k #Heq_cm_k  #_
    1067       (* get rid of jmeqs and destruct *)
    1068       lapply (jmeq_to_eq ??? Heq_INV) -Heq_INV #Heq_INV
    1069       lapply (jmeq_to_eq ??? Heq_cl_f) -Heq_cl_f #Heq_cl_f
    1070       destruct (Heq_INV Heq_cl_f)
    1071       lapply (jmeq_to_eq ??? Heq_frame) -Heq_frame #Heq_frame
    1072       lapply (jmeq_to_eq ??? Heq_cm_f) -Heq_cm_f #Heq_cm_f
    1073       lapply (jmeq_to_eq ??? Heq_rettyp) -Heq_rettyp #Heq_rettypv
    1074       lapply (jmeq_to_eq ??? Heq_cm_k) -Heq_cm_k #Heq_cm_k
    1075       lapply (jmeq_to_eq ??? Heq_cl_k) -Heq_cl_k #Heq_cl_k
    1076       destruct (Heq_frame Heq_cl_k Heq_cm_k Heq_cm_f Heq_rettyp)   
     1597      @(jmeq_absorb ?????) #HF @(jmeq_absorb ?????) #HG @(jmeq_absorb ?????) #HH @(jmeq_absorb ?????) #HI
     1598      @(jmeq_absorb ?????) #HJ
     1599      destruct (HF HG HH HI HK) #_
    10771600      #fInv #sInv #kInv #Hktarget_type
    1078       #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function
     1601      #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function
     1602      #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls
     1603      #flag * * * * #Hstmt_inv #Hlabels_translated #Htmps_preserved
     1604      #Hreturn_ok #Hlabel_wf
     1605      generalize in match (conj ????); #Hugly
     1606      (* In this simple case, trivial translation *)
     1607      whd in ⊢ ((??%?) → ?); #Heq_translate destruct (Heq_translate)
     1608      #Em
     1609      #Htmp_vars_well_alloc #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id
     1610      @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
     1611      destruct (HA HB)
     1612      @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
     1613      destruct (HC HD HE) #_
     1614      #s2 #tr whd in ⊢ ((??%?) → ?); #Heq destruct (Heq)
     1615      %{1} whd @conj [ 2: #Habsurd destruct (Habsurd) ] @conj try @refl
     1616      (* close simulation *)
     1617      %1{kINV kHcont_rel ? ? Hfresh_globals Hfresh_function
     1618         Htranslate_function kstmt_univ kstmt_univ' klbl_univ klbl_univ' klbls kflag}
     1619      (* TODO wrap this up properly *)
     1620      try assumption
     1621      @cthulhu
     1622      (* TODO: lemma allowing to prove this from [Htmp_vars_well_alloc] + tmp_gen inclusion *)
     1623    | (* Kwhile continuation *)
     1624      #kcl_ge #kcm_ge #kINV #kcl_f #kcm_f #ktarget_type #kalloc_type #kcl_env #kcm_env
     1625      #kcl_k' #kcm_k' #ksz #ksg #kcl_cond_desc #kcl_body #kcm_cond #kcm_body
     1626      #kentry #kexit #kstmt_univ #kstmt_univ' #klbl_univ #klbl_univ' #klbl_univ''
     1627      #klbls #kHtranslate_inv #kHexpr_vars #kHtranslate_expr #kfInv
     1628      * * * * #kHentry_declared * * * *
     1629      * * * #kHcond_vars_declared #Hnoise #Hnoise' #Hnoise''
     1630      #kHcont_inv #kHmklabels #kHeq_translate
     1631      #kHfind_label #kHcont_rel #_
     1632      @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
     1633      destruct (HA HB)
     1634      @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
     1635      destruct (HC HD HE)
     1636      @(jmeq_absorb ?????) #HF @(jmeq_absorb ?????) #HG @(jmeq_absorb ?????) #HH
     1637      @(jmeq_absorb ?????) #HI @(jmeq_absorb ?????) #HJ
     1638      destruct (HF HG HH HI HJ) #_
     1639      #fInv #sInv * whd in ⊢ (% → ?); * *
     1640      whd in ⊢ (% → ?); * whd in ⊢ (% → ?); #Hlabel_defined * #kInv
     1641      #Heq_rettyp
     1642      #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function
    10791643      #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls
    10801644      #flag * * * * #Hstmt_inv #Hlabels_translated #Htmps_preserved
     
    10821646      (* reduce translation function and eliminate result *)
    10831647      (* In this simple case, trivial translation *)
    1084       whd in ⊢ ((??%?) → ?); #Heq_translate
    1085       destruct (Heq_translate)
    1086       #Heq_INV' #Heq_s1 #Heq_s1'
    1087       lapply (jmeq_to_eq ??? Heq_INV') -Heq_INV' #Heq_INV'
    1088       lapply (jmeq_to_eq ??? Heq_s1) -Heq_s1 #Heq_s1
    1089       lapply (jmeq_to_eq ??? Heq_s1') -Heq_s1' #Heq_s1' #_
    1090       (* unfold the clight execution *)
    1091       %{0}
    1092       whd in ⊢ (% → ?); #Hassert
    1093       cases (invert_assert ?? Hassert) -Hassert #Hclight_class
    1094       cases (andb_inversion … Hclight_class) -Hclight_class
    1095       #_ #Hnot_labelled whd in ⊢ (% → ?); #Heq destruct (Heq)
    1096       %{0} whd in ⊢ %; @conj try @refl
    1097       (* close simulation *)
    1098       %1{kINV kHcont_rel ? ? Hfresh_globals Hfresh_function
    1099          Htranslate_function kstmt_univ kstmt_univ' klbl_univ klbl_univ' klbls kflag}
    1100       [ 3: @kHeq_translate | assumption ]
    1101     | (* Kwhile continuation *)
    1102       #kINV #kcl_f #kcm_f #kframe_data #ktarget_type
    1103       #kcl_k' #kcm_k' #ksz #ksg #kcl_cond_desc #kcl_body #kcm_cond #kcm_body
    1104       #kentry #kexit #kstmt_univ #kstmt_univ' #klbl_univ #klbl_univ' #klbl_univ''
    1105       #klbls #kHtranslate_inv #kHexpr_vars #kHtranslate_expr #kfInv
    1106       * * * * #kHentry_declared * * * *
    1107       * * * #kHcond_vars_declared * * * *
    1108       * * * #kHbody_inv * * *
    1109       whd in ⊢ (% → ?); #kHentry_declared'
    1110       * * * * * * * * *
    1111       whd in ⊢ (% → ?); #kHexit_declared *
    1112       * * * *
    1113       #kHcont_inv #kHmklabels #kHeq_translate #kHfind_label #kHcont_rel #_
    1114       #Heq_INV #Heq_cl_f #Heq_cm_f #Heq_frame #Heq_rettyp #Heq_cm_k #Heq_cl_k
    1115       lapply (jmeq_to_eq ??? Heq_INV) -Heq_INV #Heq_INV
    1116       lapply (jmeq_to_eq ??? Heq_cl_f) -Heq_cl_f #Heq_cl_f
    1117       destruct (Heq_INV Heq_cl_f)     
    1118       lapply (jmeq_to_eq ??? Heq_cm_f) -Heq_cm_f #Heq_cm_f
    1119       lapply (jmeq_to_eq ??? Heq_frame) -Heq_frame #Heq_frame
    1120       lapply (jmeq_to_eq ??? Heq_rettyp) -Heq_rettyp #Heq_rettyp
    1121       lapply (jmeq_to_eq ??? Heq_cm_k) -Heq_cm_k #Heq_cm_k
    1122       lapply (jmeq_to_eq ??? Heq_cl_k) -Heq_cl_k #Heq_cl_k #_
    1123       destruct (Heq_cl_k Heq_cm_k Heq_cm_f Heq_frame Heq_rettyp)
    1124       (* introduce state relation contents *)
    1125       #fInv #sInv * whd in ⊢ (% → ?); * *
    1126       whd in ⊢ (% → ?); * whd in ⊢ (% → ?); #Hlabel_defined * #kInv
    1127       #Heq_rettyp
    1128       #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function
    1129       #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls
    1130       #flag * * * * #Hstmt_inv #Hlabels_translated #Htmps_preserved
    1131       #Hreturn_ok #Hlabel_wf
    1132       (* reduce translation function and eliminate result *)
    1133       (* In this simple case, trivial translation *)
    1134       whd in ⊢ ((??%?) → ?); #Heq_translate
    1135       destruct (Heq_translate)
    1136       #Heq_INV' #Heq_s1 #Heq_s1'
    1137       lapply (jmeq_to_eq ??? Heq_INV') -Heq_INV' #Heq_INV'
    1138       lapply (jmeq_to_eq ??? Heq_s1) -Heq_s1 #Heq_s1
    1139       lapply (jmeq_to_eq ??? Heq_s1') -Heq_s1' #Heq_s1' #_
    1140       (* unfold the clight execution *)
    1141       %{1} whd in ⊢ (% → ?); #Hawait
    1142       cases (await_value_bind_inv … Hawait) -Hawait
    1143       * #cl_val #cl_trace * #Hexec_cond #Hawait
    1144       cases (await_value_bind_inv … Hawait) -Hawait
    1145       #cond_outcome * #Hcond_outcome
    1146       cases (eval_expr_sim … kframe_data) #Hsim_expr #_
    1147       (* use simulation lemma on expressions *)
    1148       lapply (Hsim_expr … kHtranslate_expr … kHcond_vars_declared … Hexec_cond) -Hsim_expr
    1149       whd in match (typeof ?) in Hcond_outcome; cases cond_outcome in Hcond_outcome;
    1150       #Hcond_outcome lapply (exec_bool_of_val_inversion … Hcond_outcome)
    1151       * [ 2,4: * #ptr * #ty' * * #_ #Habsurd destruct (Habsurd) ]
    1152       * [ 2,4: * #ty' * * #_ #Habsurd destruct (Habsurd) ]
    1153       * #vsz * #vsg * #i * * #Hcl_val #Htype_eq destruct (Hcl_val Htype_eq)
    1154       normalize nodelta #Hi_eq
    1155       * #cm_val * #Hexec_cond_cm #Hvalue_eq #Hassert
    1156       cases (invert_assert … Hassert) -Hassert #Handb
    1157       cases (andb_inversion … Handb) -Handb #_ #HClight_not_labelled
    1158       whd in ⊢ (% → ?); #Heq destruct (Heq)
    1159       [ %{5} whd whd in ⊢ (??%?); normalize nodelta
    1160         >kHfind_label -kHfind_label normalize nodelta
    1161         whd in match (proj1 ???);
    1162         whd in match (proj2 ???);
    1163         whd whd in ⊢ (??%?); normalize nodelta
    1164         >Hexec_cond_cm normalize nodelta
    1165         whd in match (m_bind ?????);
    1166         >(value_eq_int_inversion … Hvalue_eq)
    1167         whd in match (eval_bool_of_val ?); normalize nodelta
    1168         <Hi_eq normalize nodelta
    1169         whd @conj [ normalize >append_nil try @refl ]
    1170         whd in match (proj1 ???);
    1171         whd in match (proj2 ???);
    1172         whd whd in ⊢ (??%?); normalize nodelta
    1173         %{??????? kframe_data ktarget_type Hcont_rel Heq_rettyp ??? Htranslate_function
    1174           ??????? kHeq_translate}
    1175       | %{6} whd whd in ⊢ (??%?); normalize nodelta
    1176         >kHfind_label -kHfind_label normalize nodelta
    1177         whd in match (proj1 ???);
    1178         whd in match (proj2 ???);
    1179         whd whd in ⊢ (??%?); normalize nodelta
    1180         >Hexec_cond_cm normalize nodelta
    1181         whd in match (m_bind ?????);
    1182         >(value_eq_int_inversion … Hvalue_eq)
    1183         whd in match (eval_bool_of_val ?); normalize nodelta
    1184         <Hi_eq normalize nodelta
    1185         whd @conj [ normalize >append_nil >append_nil try @refl ]
    1186         whd in match (proj1 ???);
    1187         whd in match (proj2 ???);
    1188         whd whd in ⊢ (??%?); normalize nodelta
    1189         %{??????? kframe_data ktarget_type kHcont_rel Heq_rettyp ??? Htranslate_function}
    1190         try assumption
    1191         [ @conj try @conj try @conj try @conj //
    1192         | @refl ]
    1193       ]
    1194   (*| TODO: other continuations *)
     1648      whd in ⊢ ((??%?) → ?); #Heq_translate destruct (Heq_translate)
     1649      #Em #Htmp_vars_well_allocated #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching
     1650      #HEm_fn_id
     1651      @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
     1652      destruct (HA HB)
     1653      @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
     1654      destruct (HC HD HE) #_ #s2 #tr
     1655      whd in ⊢ ((??%?) → ?); #Heq destruct (Heq)
     1656      generalize in match (conj ????); #Hnoise'''
     1657      lapply kHfind_label -kHfind_label
     1658      generalize in ⊢ ((??(????%????)?) → ?); #Hlabel_exists
     1659      generalize in ⊢ ((???(????%)) → ?); #Hmore_invariant
     1660      #kHfind_label
     1661      %{2} whd whd in ⊢ (??%?); normalize nodelta generalize in match (proj2 ???); #Hmore_noise
     1662      generalize in match (proj1 ???); #Hmore_noise'
     1663      >kHfind_label normalize nodelta
     1664      whd @conj try @conj try @refl
     1665      generalize in match (proj1 ???); #Hvars_present_in_ifthenelse
     1666      generalize in match (proj2 ???); #Hcont_inv'
     1667      [ 2: #Habsurd destruct (Habsurd) ]
     1668      (* go to a special simulation state for while loops *)
     1669      @CMR_while
    11951670    ]
    11961671| 2: (* Assign *)
    1197      #cm_s #cl_k #cm_k #cm_st #cl_f #cm_f #frame_data #rettyp #Hcont_rel
    1198      #fInv #sInv #kInv #Hrettyp #func_univ #Hfresh_globals #Hfresh_function
    1199      #Htranslate_function #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls #flag
    1200      * * * * #Hstmt_inv_cm #Huseless_hypothesis
    1201       #Htmps_preserved #Hreturn_ok #Hlabel_wf     
     1672     #cm_s #cl_k #cm_k #cm_st #cl_f #cm_f #rettyp
     1673     #alloc_type #cl_env #cl_m #cm_env #cm_m #stackptr #stacksize #Hcont_rel
     1674     (* introduce everything *)
     1675     #fInv #sInv #kInv #Htarget_type #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function
     1676     #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls
     1677     #flag * * * * #Hstmt_inv_cm #Hlabels_translated #Htmps_preserved
     1678     #Hreturn_ok #Hlabel_wf generalize in match (conj ????); #Hugly #Htranslate
     1679     #Em #Htmp_vars_well_allocated #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id
     1680     @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
     1681     destruct (HA HB)
     1682     @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE #_
     1683     destruct (HC HD HE)
     1684     lapply Htranslate -Htranslate
    12021685     (* case-split on lhs in order to reduce lvalue production in Cminor *)
    12031686     cases lhs #lhs_ed #lhs_ty
    1204      cases lhs_ed
    1205      (* intro expr contents *)
    1206      [ #sz #i | #var_id | #e1 | #e1 | #op #e1 |#op #e1 #e2 | #cast_ty #e1
    1207      | #cond #iftrue #iffalse | #e1 #e2 | #e1 #e2 | #sizeofty | #e1 #field | #cost #e1 ]
    1208      [ 2: #Htranslate_statement
     1687     cases (expr_is_Evar_id_dec lhs_ed)
     1688     [ 2: * #var_id #Hlhs_ed destruct (Hlhs_ed)
     1689          #Htranslate_statement
    12091690          cases (bind_inversion ????? Htranslate_statement)
    12101691          * #cm_rhs #Hexpr_vars_rhs * #Htranslate_rhs #Htranslate_statement'
    1211           cases (bind_inversion ????? Htranslate_statement')
     1692          cases (bind_inversion ????? Htranslate_statement') -Htranslate_statement'
    12121693          #lhs_dest * #Htranslate_lhs
    12131694          cases (bind2_eq_inversion ?????? Htranslate_lhs) -Htranslate_lhs
     
    12181699               #Hlookup_var_success whd in ⊢ ((???%) → ?); #Hlhs_dest_eq
    12191700               destruct (Hlhs_dest_eq) normalize nodelta
    1220                whd in match (proj1 ???); whd in match (proj2 ???);
     1701               generalize in match (conj ????); #Hinvariant
     1702               cases (type_eq_dec ??)
     1703               [ 2: #Hneq normalize nodelta whd in ⊢ ((??%%) → ?);
     1704                    #Habsurd destruct (Habsurd) ]
     1705               normalize nodelta whd in match (typeof ?); #Heq_cl_types
    12211706               whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
    1222                #Heq_INV #Heq_s1 #Heq_s1'
    1223                lapply (jmeq_to_eq ??? Heq_INV) -Heq_INV #Heq_INV
    1224                lapply (jmeq_to_eq ??? Heq_s1) -Heq_s1 #Heq_s1
    1225                lapply (jmeq_to_eq ??? Heq_s1') -Heq_s1' #Heq_s1'
    1226                destruct (Heq_INV Heq_s1 Heq_s1') #_
    1227                %{1} whd in ⊢ (% → ?); #Hawait
    1228                cases (await_value_bind_inv … Hawait) -Hawait
     1707               #s2 #tr whd in ⊢ ((??%?) → ?); #Hstep
     1708               cases (bindIO_inversion ??????? Hstep) -Hstep
    12291709               * * #cl_blo #cl_off #cl_tr * whd in ⊢ ((??%?) → ?);
    1230                #Hexec_lvalue
     1710               #Hexec_lvalue #Hstep
    12311711               lapply (res_to_io ????? Hexec_lvalue) -Hexec_lvalue #Hexec_lvalue
    1232                #Hawait
    1233                cases (await_value_bind_inv … Hawait) -Hawait
    1234                * #rhs_val #rhs_trace * #Hexec_rhs_trace #Hawait
    1235                cases (await_value_bind_inv … Hawait) -Hawait
    1236                #mem_after_store * #Hstore_value #Hawait
    1237                lapply (opt_to_io_Value ?????? Hstore_value) -Hstore_value #Hstore_value
    1238                -Htranslate_statement' -Htranslate_statement
    1239                cases (invert_assert … Hawait) -Hawait #Handb
    1240                cases (andb_inversion … Handb) -Handb #_ #HClight_not_labelled #Hawait               
    1241                (* TODO: use the memory injection to handle the store,
    1242                   use INV contents to match up CL global with CM one.
    1243                   Note to self: globals should be exactly matched in CL and CM,
    1244                   maybe memory_injection is not useful in this particular case,
    1245                   only in Stack and Local cases.
    1246                 * *)
    1247                @cthulhu
    1248           | 2: (* Stack *) #n @cthulhu
    1249           | 3: (* Local *) @cthulhu
     1712               cases (bindIO_inversion ??????? Hstep) -Hstep
     1713               * #cl_rhs_val #cl_trace * #Hexec_rhs #Hstep
     1714               cases (bindIO_inversion ??????? Hstep) -Hstep
     1715               #cl_mem_after_store_lhs * #Hstore
     1716               whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
     1717               lapply (opt_to_io_Value ?????? Hstore) -Hstore #Hstore
     1718               %{1} whd whd in ⊢ (??%?); normalize nodelta
     1719               generalize in match (proj1 ???); whd in ⊢ (% → ?); *
     1720               whd in match (eval_expr ???????);
     1721               whd in match (eval_constant ????);
     1722               whd in Hexec_lvalue:(??%?);
     1723               <(eq_sym … INV' var_id)
     1724               lapply (Hmatching … var_id)
     1725               cases (lookup ?? cl_env var_id) in Hexec_lvalue; normalize nodelta
     1726               [ 1: #Heq_find_sym cases (bind_inversion ????? Heq_find_sym) -Heq_find_sym
     1727                    #global_b * #Hopt_to_res lapply (opt_to_res_inversion ???? Hopt_to_res) -Hopt_to_res
     1728                    #Hfind_symbol >Hfind_symbol
     1729                    normalize nodelta
     1730                    whd in ⊢ ((???%) → ?); #Heq destruct (Heq) #Hembed_eq
     1731                    whd in match (m_bind ?????);
     1732                    cases (eval_expr_sim … Halloc_hyp … Hcl_env_hyp … Hinjection … Hmatching) #Hsim_expr #_
     1733                    lapply (Hsim_expr … Htranslate_rhs … (proj2 ?? (proj1 ?? (proj1 ?? sInv))) Hexec_rhs)
     1734                    * #cm_rhs_val generalize in match (proj2 ???);
     1735                    #Hexpr_vars_rhs * #Heval_expr_rhs #Hvalue_eq_rhs >Heval_expr_rhs
     1736                    whd in match (m_bind ?????); whd in Hstore:(??%?); whd in Hstore:(??%?);
     1737                    cases (store_value_of_type_success_by_value lhs_ty cl_m
     1738                                    cl_mem_after_store_lhs cl_blo zero_offset cl_rhs_val Hstore)
     1739                    #Haccess_mode #Hstorev
     1740                    lapply (storen_parallel_aux ??? Hinjection … Hvalue_eq_rhs … Hembed_eq ??? Hstorev)
     1741                    * #cm_mem_after_store_lhs * #Hstoren #Hinj whd in Hstoren:(??%?);
     1742                    whd in Hstoren:(??%?); whd in match (shift_offset ???);
     1743                    >sign_ext_same_size >addition_n_0
     1744                    whd in match (storev ????);
     1745                    lapply Hstoren whd in match (offset_plus ??);
     1746                    >addition_n_0 -Hstoren
     1747                    >Heq_cl_types #Hstoren >Hstoren
     1748                    whd in match (opt_to_res ???); normalize nodelta
     1749                    whd @conj try @conj try @refl
     1750                    [ 2: #Habsurd destruct (Habsurd) ]
     1751                    generalize in match (conj ????);
     1752                    #Hinv_vars
     1753                    @CMR_normal try assumption
     1754                    [ 2: @refl | 1,3,4: ]
     1755                    [ 1: (* TODO: lemma on preservation of well-allocatedness through stores *) @cthulhu
     1756                    | 2: (* TODO: lemma on preservation of memory matching through stores *) @cthulhu ]
     1757               | 2: #b #Heq destruct (Heq)
     1758                    lapply (opt_to_res_inversion ???? Hlookup_var_success) #Hlookup_aux
     1759                    >Hlookup_aux normalize nodelta @False_ind ]
     1760          | 2: (* Stack *)
     1761               #n #Hlookup_var_success
     1762               whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
     1763               normalize nodelta whd in ⊢ ((???%) → ?);
     1764               cases (type_eq_dec ??) normalize nodelta #Htype_eq
     1765               [ 2: #Habsurd destruct (Habsurd) ]
     1766               #Heq destruct (Heq) #s2 #tr #Hstep
     1767               cases (bindIO_inversion ??????? Hstep)
     1768               * * #cl_lvalue_block #cl_offset #cl_trace * #Hexec_lvalue
     1769               lapply (res_to_io ????? Hexec_lvalue) -Hexec_lvalue
     1770               whd in ⊢ ((??%?) → ?);
     1771               @(match lookup ?? cl_env var_id
     1772                 return λx. (lookup ?? cl_env var_id = x) → ?
     1773                 with
     1774                 [ None ⇒ λH. ?
     1775                 | Some cl_addr ⇒ λH. ?
     1776                 ] (refl ? (lookup ?? cl_env var_id)))
     1777               normalize nodelta
     1778               [ (* Contradiction: a stack-allocated variable was necessarily in the environment *)
     1779                 @cthulhu
     1780               | #Heq destruct (Heq)
     1781                 lapply (Hmatching var_id) >H normalize nodelta
     1782                 >(opt_to_res_inversion ???? Hlookup_var_success) normalize nodelta
     1783                 #Hembedding_to_stack #Hexec_cl_rhs
     1784                 cases (bindIO_inversion ??????? Hexec_cl_rhs) -Hexec_cl_rhs *
     1785                 #cl_rhs_result #cl_rhs_trace * #Hcl_exec_expr_rhs #Hcl_exec_store
     1786                 cases (bindIO_inversion ??????? Hcl_exec_store) -Hcl_exec_store #cl_mem_after_store
     1787                 * #Hstore_value_of_type lapply (opt_to_io_Value ?????? Hstore_value_of_type)
     1788                 -Hstore_value_of_type
     1789                 #Hstore_value_of_type
     1790                 whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
     1791                 %{1} whd whd in ⊢ (??%?); normalize nodelta
     1792                 whd in match (eval_expr ???????);
     1793                 whd in match (eval_constant ????);
     1794                 whd in match (m_bind ?????);
     1795                 cases (eval_expr_sim … Halloc_hyp … Hcl_env_hyp … Hinjection … Hmatching) #Hsim_expr #_
     1796                 lapply (Hsim_expr … Htranslate_rhs … (proj2 ?? (proj1 ?? (proj1 ?? sInv))) Hcl_exec_expr_rhs)
     1797                 * #cm_rhs_val generalize in match (proj2 ???);
     1798                 #Hexpr_vars_rhs * #Heval_expr_rhs #Hvalue_eq_rhs >Heval_expr_rhs
     1799                 normalize nodelta -Hsim_expr
     1800                 whd in match (shift_offset ???); >sign_ext_same_size
     1801                 >commutative_addition_n >addition_n_0
     1802                 whd in Hstore_value_of_type:(??%?);
     1803                 cases (store_value_of_type_success_by_value ? cl_m
     1804                                    cl_mem_after_store ?? cl_rhs_result Hstore_value_of_type)
     1805                 whd in match (typeof ?) in ⊢ ((??%%) → (??%?) → ?);
     1806                 #Haccess_mode #Hstorev -Hstore_value_of_type
     1807                 lapply (storen_parallel_aux ??? Hinjection … Hvalue_eq_rhs … Hembedding_to_stack ??? Hstorev)
     1808                 * #cm_mem_after_store_lhs * #Hstoren #Hinj whd in Hstoren:(??%?);
     1809                 >offset_plus_0 in Hstoren; #Hstorev'
     1810                 whd in match (storev ????);
     1811                 lapply Htype_eq whd in match (typeof ?) in ⊢ ((??%?) → ?); #Htype_eq'
     1812                 <Htype_eq' >Hstorev'
     1813                 whd in match (m_bind ?????); normalize nodelta
     1814                 whd @conj try @conj try @refl
     1815                 [ 2: #Habsurd destruct (Habsurd) ]
     1816                 @(CMR_normal … Halloc_hyp) try assumption
     1817                 [ 2: @refl | 1,3,4,5: ]
     1818                 [ 1: (* TODO: lemma on preservation of well-allocatedness through stores *) @cthulhu
     1819                 | 2: (* TODO: lemma on preservation of memory matching through stores *) @cthulhu ]
     1820               ]
     1821          | 3: (* Local *)
     1822               #Hlookup_var_success whd in ⊢ ((???%) → ?);
     1823               #Heq destruct (Heq) normalize nodelta -Htranslate_statement
     1824               #Htranslate
     1825               cases (bind_inversion ????? Htranslate) -Htranslate
     1826               * #cm_expr #Hexpr_vars * #Htyp_should_eq
     1827               whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
     1828               cases (typ_should_eq_inversion (typ_of_type (typeof rhs)) (typ_of_type type_of_var) … Htyp_should_eq)
     1829               -Htyp_should_eq #Htyp_eq lapply Hexpr_vars_rhs lapply Hexpr_vars
     1830               -Hlabel_wf -Hreturn_ok -Hlabels_translated -Hstmt_inv_cm lapply sInv               
     1831               lapply cm_expr -cm_expr <Htyp_eq #cm_expr #sInv #Hexpr_vars #Hexpr_vars'
     1832               @(jmeq_absorb ?????) #Heq destruct (Heq)
     1833               #s2 #tr whd in ⊢ ((??%?) → ?); #Hcl_exec
     1834               cases (bindIO_inversion ??????? Hcl_exec)
     1835               * * #cl_blo #cl_off #cl_trace *
     1836               whd in ⊢ ((???%) → ?);
     1837               #Hexec_lvalue lapply (res_to_io ????? Hexec_lvalue) -Hexec_lvalue
     1838               whd in ⊢ ((??%?) → ?);
     1839               @(match lookup ?? cl_env var_id
     1840                 return λx. (lookup ?? cl_env var_id = x) → ?
     1841                 with
     1842                 [ None ⇒ λH. ?
     1843                 | Some cl_addr ⇒ λH. ?
     1844                 ] (refl ? (lookup ?? cl_env var_id)))
     1845               normalize nodelta
     1846               [ (* Contradiction: a register-allocated variable was necessarily in the environment *)
     1847                 @cthulhu
     1848               | #Heq destruct (Heq)
     1849                 lapply (Hmatching var_id) >H normalize nodelta
     1850                 >(opt_to_res_inversion ???? Hlookup_var_success) normalize nodelta
     1851                 #Hpresent_in_local #Hexec_cl_rhs
     1852                 cases (bindIO_inversion ??????? Hexec_cl_rhs) -Hexec_cl_rhs *
     1853                 #cl_rhs_result #cl_rhs_trace * #Hcl_exec_expr_rhs #Hcl_exec_store
     1854                 cases (bindIO_inversion ??????? Hcl_exec_store) -Hcl_exec_store #cl_mem_after_store
     1855                 * #Hstore_value_of_type lapply (opt_to_io_Value ?????? Hstore_value_of_type)
     1856                 -Hstore_value_of_type #Hstore_value_of_type
     1857                 whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
     1858                 %{1} whd whd in ⊢ (??%?); normalize nodelta
     1859                 cases (eval_expr_sim … Halloc_hyp … Hcl_env_hyp … Hinjection … Hmatching) #Hsim_expr #_
     1860                 lapply (Hsim_expr … Htranslate_rhs … (proj2 ?? (proj1 ?? (proj1 ?? sInv))) Hcl_exec_expr_rhs)
     1861                 * #cm_rhs_val generalize in match (proj2 ???);
     1862                 #Hexpr_vars_rhs * #Heval_expr_rhs #Hvalue_eq_rhs >Heval_expr_rhs
     1863                 normalize nodelta -Hsim_expr whd @conj try @conj try @refl
     1864                 [ 2: #Habsurd destruct (Habsurd) ]
     1865                 generalize in match (proj1 ???); #Hpresent
     1866                 generalize in match (conj ????); #Hstmt_vars
     1867                 @(CMR_normal … Halloc_hyp) try assumption
     1868                 [ 3: @refl | *: ]
     1869                 [ (* Need a particular kind of continuation relation *) @cthulhu
     1870                 | (* Lemma on preservation of well-allocatedness through update_present *) @cthulhu
     1871                 | (* Memory injection when writing in clight only, and block not mapped *) @cthulhu
     1872                 | (* Memory matching through env update *) @cthulhu ]
     1873               ]
    12501874          ]
    1251      | *: (* memdest *) @cthulhu ]   *) 
     1875     | 1: #Hnot_evar #Htranslate_statement
     1876          cases (bind_inversion ????? Htranslate_statement) -Htranslate_statement
     1877          * #cm_rhs #Hexpr_vars_rhs * #Htranslate_rhs #Htranslate_statement'
     1878          cases (bind_inversion ????? Htranslate_statement') -Htranslate_statement' #dest
     1879          lapply (translate_dest_not_Evar_id alloc_type ? lhs_ty Hnot_evar)
     1880          #Htranslate_dest * #Htranslate_dest'
     1881          >Htranslate_dest' in Htranslate_dest; #Haux lapply (sym_eq ??? Haux) -Haux #Haux
     1882          cases (bind_inversion ????? Haux) -Haux
     1883          * #translated_dest #Hexpr_vars_dest * #Htranslate_addr
     1884          whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) normalize nodelta
     1885          cases (type_eq_dec ??)
     1886          [ 2: #Hneq normalize nodelta whd in ⊢ ((??%%) → ?);
     1887               #Habsurd destruct (Habsurd) ]
     1888          normalize nodelta whd in match (typeof ?); #Heq_cl_types
     1889          whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
     1890          #s2 #tr whd in ⊢ ((??%?) → ?); #Hstep
     1891          cases (bindIO_inversion ??????? Hstep) -Hstep
     1892          * * #cl_blo #cl_off #cl_tr * whd in ⊢ ((??%?) → ?);
     1893          #Hexec_lvalue #Hstep
     1894          lapply (translate_dest_MemDest_simulation …
     1895                     INV' ???????? Halloc_hyp Hcl_env_hyp Hinjection Hmatching ??????
     1896                     Htranslate_dest' Hexec_lvalue)
     1897          [ 1: @(proj1 ?? (proj1 ?? (proj1 ?? sInv))) ]
     1898          * #cm_val_dest * #Heval_cm_dest #Hvalue_eq_dest
     1899          %{1} whd whd in ⊢ (??%?); normalize nodelta
     1900          >Heval_cm_dest
     1901          whd in match (m_bind ?????);
     1902          cases (bindIO_inversion ??????? Hstep) -Hstep
     1903          * #val #trace * #Hexec_expr #Hstep
     1904          cases (bindIO_inversion ??????? Hstep) -Hstep
     1905          #cl_mem_after_store * #Hopt_store
     1906          whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
     1907          lapply (opt_to_io_Value ?????? Hopt_store) -Hopt_store
     1908          #Hstore_value_of_type whd in Hstore_value_of_type:(??%?);
     1909          cases (eval_expr_sim … Halloc_hyp … Hcl_env_hyp … Hinjection … Hmatching) #Hsim_expr #_
     1910          lapply (Hsim_expr … Htranslate_rhs … (proj2 ?? (proj1 ?? (proj1 ?? sInv))) Hexec_expr)
     1911          * #cm_rhs_val generalize in match (proj2 ???);
     1912          #Hexpr_vars_rhs * #Heval_expr_rhs #Hvalue_eq_rhs >Heval_expr_rhs
     1913          normalize nodelta -Hsim_expr
     1914          cases (store_value_of_type_success_by_value ? cl_m
     1915                                    cl_mem_after_store ?? val Hstore_value_of_type)
     1916          whd in match (typeof ?) in ⊢ ((??%%) → (??%?) → ?);
     1917          #Haccess_mode #Hstorev -Hstore_value_of_type
     1918          cases (value_eq_ptr_inversion … Hvalue_eq_dest) * #cm_blo #cm_off * #Hcm_val_dest destruct (Hcm_val_dest)
     1919          whd in ⊢ ((??%?) → ?); #Hembed
     1920          cases (some_inversion ????? Hembed) -Hembed
     1921          * #cm_blo' #cm_off' * #Hembed normalize nodelta #Heq destruct (Heq)
     1922          lapply (storen_parallel_aux ??? Hinjection … Hvalue_eq_rhs … Hembed ??? Hstorev)
     1923          * #cm_mem_after_store_lhs * #Hstoren #Hinj whd in Hstoren:(??%?);
     1924          whd in match (storev ????);
     1925          lapply Hstoren
     1926          (* make the types match *)
     1927          generalize in match (conj ????); #Hstmt_vars' >Heq_cl_types
     1928          #Hstoren >Hstoren
     1929          whd in match (m_bind ?????); normalize nodelta whd @conj try @conj try @refl
     1930          [ 2: #Habsurd destruct (Habsurd) ]
     1931          @(CMR_normal … Halloc_hyp) try assumption
     1932          [ 2: @refl | *: ]
     1933          [ 1: (* lemma on well_allocated after CL and CM parallel writes *) @cthulhu
     1934          | 2: (* memory matching *) @cthulhu ]
     1935     ]
     1936| *: @cthulhu ]
    12521937| *: @cthulhu
    12531938] qed.
    12541939
    12551940(* TODO: adapt the following to the new goal shape. *)
     1941(*
    12561942axiom clight_cminor_call_return :
    12571943  ∀INV:clight_cminor_inv.
     
    12801966  make_initial_state ?? clight_fullexec cl_program = OK ? s →
    12811967  make_initial_state ?? Cminor_fullexec cm_program = OK ? s' →
    1282   ∃INV. clight_cminor_rel INV s s'.
     1968  ∃INV. clight_cminor_rel INV s s'. *)
  • src/Clight/toCminorCorrectnessExpr.ma

    r2692 r2822  
    389389qed.
    390390
     391(* This record holds much of the translation invariant for expressions AND statements.
     392 * Hence its size. *)
     393(* Using a record was a bad idea. Especially when it appears as a parameter of some type,
     394 * and we have to update another part of the record. *)
     395(*
    391396record clight_cminor_data
    392   (f : function)
    393   (ge_cl : genv_t clight_fundef)
    394   (ge_cm : genv_t (fundef internal_function))
    395   (INV : clight_cminor_inv ge_cl ge_cm) : Type[0] ≝
     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  ≝
    396402{ alloc_type  : var_types;
    397403  stacksize   : ℕ;
     
    412418  (* Force embedding to compute identity on functions *)
    413419  Em_fn_id    : ∀b. block_region b = Code → Em b = Some ? 〈b, zero_offset〉
    414 }.
     420  (* Fresh variable ident generator *)
     421  (* tmp_gen     : tmpgen alloc_type; *)
     422  (* Temporary variables generated during conversion are well-allocated. *)
     423  (* TODO: isn't this ugly ? Should it be there ? *)
     424  (* tmp_vars_ok : ∀local_variable.
     425                ∀H:present ?? cm_env local_variable.
     426                ∀ty. Exists ? (λx. x = 〈local_variable, ty〉) (tmp_env … tmp_gen) →
     427                ∀v. val_typ v (typ_of_type ty) →
     428                ∃cm_m'. storev (typ_of_type ty) cm_m (lookup_present ?? cm_env local_variable H) v = Some ? cm_m' ∧
     429                        memory_inj Em cl_m cm_m' *)
     430}.*)
    415431
    416432(* -------------------------------------------------------------------- *)
     
    421437  ∀ge_cl : genv_t clight_fundef.
    422438  ∀ge_cm : genv_t (fundef internal_function).
    423   ∀cl_cm_inv  : clight_cminor_inv ge_cl ge_cm.
     439  ∀INV   : clight_cminor_inv ge_cl ge_cm.
    424440  (* current function (defines local environment) *)
    425441  ∀f          : function.
    426   ∀data       : clight_cminor_data f ge_cl ge_cm cl_cm_inv.
     442  ∀alloc_type  : var_types.
     443  ∀stacksize   : ℕ. 
     444  ∀alloc_hyp   : characterise_vars (globals ?? INV) f = 〈alloc_type, stacksize〉.
     445  (* environments *)
     446  ∀cl_env      : cl_env.
     447  ∀cm_env      : cm_env.
     448  (* Characterise clight environment. Needed to prove that some variable is either a parameter or a local.  *)
     449  ∀cl_env_hyp  : ∃m,m'. exec_alloc_variables empty_env m (fn_params f @ fn_vars f) = 〈cl_env,m'〉.
     450  (* CL and CM memories *)
     451  ∀cl_m        : mem.
     452  ∀cm_m        : mem.
     453  (* Memory injection and matching *)
     454  ∀Em          : embedding. (* using "E" clashes with something in jmeq *)
     455  ∀injection   : memory_inj Em cl_m cm_m.
     456  ∀stackptr    : block.
     457  ∀matching    : memory_matching Em ge_cl ge_cm cl_m cm_m cl_env cm_env INV stackptr alloc_type.
    427458  (* clight expr to cminor expr *)
    428459  (∀(e:expr).
    429460   ∀(e':CMexpr (typ_of_type (typeof e))).
    430461   ∀Hexpr_vars.
    431    translate_expr (alloc_type … data) e = OK ? («e', Hexpr_vars») →
     462   translate_expr alloc_type e = OK ? («e', Hexpr_vars») →
    432463   ∀cl_val,trace,Hyp_present.
    433    exec_expr ge_cl (cl_env … data) (cl_m … data) e = OK ? 〈cl_val, trace〉 →
    434    ∃cm_val. eval_expr ge_cm (typ_of_type (typeof e)) e' (cm_env … data) Hyp_present (stackptr … data) (cm_m … data) = OK ? 〈trace, cm_val〉 ∧
    435             value_eq (Em … data) cl_val cm_val) ∧
     464   exec_expr ge_cl cl_env cl_m e = OK ? 〈cl_val, trace〉 →
     465   ∃cm_val. eval_expr ge_cm (typ_of_type (typeof e)) e' cm_env Hyp_present stackptr cm_m = OK ? 〈trace, cm_val〉 ∧
     466            value_eq Em cl_val cm_val) ∧
    436467   (* clight /lvalue/ to cminor /expr/ *)
    437468  (∀ed,ty.
    438469   ∀(e':CMexpr ASTptr).
    439470   ∀Hexpr_vars.
    440    translate_addr (alloc_type … data) (Expr ed ty) = OK ? («e', Hexpr_vars») →
     471   translate_addr alloc_type (Expr ed ty) = OK ? («e', Hexpr_vars») →
    441472   ∀cl_blo,cl_off,trace,Hyp_present.
    442    exec_lvalue' ge_cl (cl_env … data) (cl_m … data) ed ty = OK ? 〈cl_blo, cl_off, trace〉 →
    443    ∃cm_val. eval_expr ge_cm ASTptr e' (cm_env … data) Hyp_present (stackptr … data) (cm_m … data) = OK ? 〈trace, cm_val〉 ∧
    444             value_eq (Em … data) (Vptr (mk_pointer cl_blo cl_off)) cm_val).
    445 #ge_cl #ge_cm #inv #f * #vars #stacksize #Hcharacterise #cl_env #cm_env #Hexec_alloc #cl_m #cm_m #E #Hinj #sp #Hlocal_matching #_
     473   exec_lvalue' ge_cl cl_env cl_m ed ty = OK ? 〈cl_blo, cl_off, trace〉 →
     474   ∃cm_val. eval_expr ge_cm ASTptr e' cm_env Hyp_present stackptr cm_m = OK ? 〈trace, cm_val〉 ∧
     475            value_eq Em (Vptr (mk_pointer cl_blo cl_off)) cm_val).
     476#ge_cl #ge_cm #inv #f #vars #stacksize #Hcharacterise #cl_env #cm_env #Hexec_alloc #cl_m #cm_m #E #Hinj #sp #Hlocal_matching
    446477@expr_lvalue_ind_combined
    447478[ 7: (* binary ops *)
Note: See TracChangeset for help on using the changeset viewer.