Changeset 2857


Ignore:
Timestamp:
Mar 12, 2013, 8:03:03 PM (4 years ago)
Author:
garnier
Message:

CL to CM: some invariants strengthened.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/toCminorCorrectness.ma

    r2850 r2857  
    409409#H1 #H2 @refl qed.
    410410
    411 
    412411(* relate Clight continuations and Cminor ones. *)
    413412inductive clight_cminor_cont_rel :
     
    423422  cl_cont →                                 (* CL cont *)
    424423  cm_cont →                                 (* CM cont *)
     424  stack →                                   (* CM stack *) 
    425425  Prop ≝
    426426(* Stop continuation*) 
     
    428428  ∀cl_ge, cm_ge, INV, cl_f, cm_f, target_type.
    429429  ∀cl_env, cm_env, alloc_type.
    430   clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type target_type Kstop Kend
     430  ∀cm_stack.
     431  cm_stack = SStop →
     432  clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type target_type Kstop Kend cm_stack
    431433
    432434(* Seq continuation *)
    433435| ClCm_cont_seq:
    434436  ∀cl_ge, cm_ge, INV, cl_f, cm_f, target_type.
     437  ∀stack.
    435438  ∀alloc_type.
    436439  ∀cl_s: statement.
     
    448451  (* ---- invariant on label existence ---- *)
    449452  lset_inclusion ? (labels_of cm_s) (labels_of (f_body cm_f)) →
    450   clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type target_type cl_k' cm_k'
    451   clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type target_type (ClKseq cl_s cl_k') (Kseq cm_s cm_k')
     453  clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type target_type cl_k' cm_k' stack
     454  clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type target_type (ClKseq cl_s cl_k') (Kseq cm_s cm_k') stack
    452455
    453456(* While continuation *) 
     
    455458  (* Inductive family parameters *)
    456459  ∀cl_ge, cm_ge, INV, cl_f, cm_f, target_type.
    457 
     460  ∀stack.
    458461  ∀alloc_type.
    459462  ∀cl_env.
     
    501504            (St_ifthenelse ?? cm_cond (St_seq cm_body (St_goto entry)) St_skip)
    502505            (St_label exit St_skip)), cm_k'〉, Hinv» →
    503   clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type target_type cl_k' cm_k'
     506  clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type target_type cl_k' cm_k' stack
    504507  clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type target_type (
    505508    Kwhile (Expr cl_cond_desc cl_ty) cl_body cl_k')
    506     (Kseq (St_goto entry) (Kseq (St_label exit St_skip) cm_k')).
     509    (Kseq (St_goto entry) (Kseq (St_label exit St_skip) cm_k')) stack.
     510(* TODO: Kcall *)
    507511
    508512(* TODO XXX *)
     
    532536inductive clight_cminor_rel : ∀cl_ge, cm_ge. clight_cminor_inv cl_ge cm_ge  → Clight_state → Cminor_state → Prop ≝
    533537| CMR_normal :
     538  (* Clight and Cminor global envs *)
    534539  ∀cl_ge, cm_ge.
    535540  (* Relates globals to globals and functions to functions. *)
    536541  ∀INV:  clight_cminor_inv cl_ge cm_ge. 
    537542  (* ---- Statements ---- *)
    538   ∀cl_s: statement.                                       (* Clight statement *) 
    539   ∀cm_s: stmt.                                            (* Cminor statement *)
     543  (* Clight statement *) 
     544  ∀cl_s: statement.
     545  (* Cminor statement *)
     546  ∀cm_s: stmt.                                           
    540547  (* ---- Continuations ---- *)
    541   ∀cl_k: cl_cont.                                      (* Clight continuation *)
    542   ∀cm_k: cm_cont.                                      (* Cminor continuation *)
    543   ∀cm_st: stack.                                              (* Cminor stack *) 
    544   ∀cl_f: function.                               (* Clight enclosing function *)
    545   ∀cm_f: internal_function.                             (* enclosing function *)
    546   ∀rettyp.                                     (* return type of the function *)
     548  (* Clight continuation *)
     549  ∀cl_k: cl_cont.
     550  (* Cminor continuation *) 
     551  ∀cm_k: cm_cont.
     552  (* Cminor stack *)
     553  ∀cm_st: stack.
     554  (* Clight enclosing function *)
     555  ∀cl_f: function.
     556  (* Cminor enclosing function *)
     557  ∀cm_f: internal_function.
     558  (* optional return type of the function *)
     559  ∀rettyp.
     560  (* mapping from variables to their Cminor alloc type *)                                 
    547561  ∀alloc_type.
     562  (* Clight env/mem *)
    548563  ∀cl_env, cl_m.
     564  (* Cminor env/mem *)
    549565  ∀cm_env, cm_m.
    550   ∀stackptr, stacksize. 
     566  (* Stack pointer (block containing Cminor locals), related size *)
     567  ∀stackptr, stacksize.
    551568  (* ---- Cminor invariants ---- *)
    552569  ∀fInv: stmt_inv cm_f cm_env (f_body cm_f).
     
    561578  translate_function func_univ (globals ?? INV) cl_f Hfresh_globals Hfresh_function = OK ? cm_f →
    562579  (* ---- relate Clight and Cminor statements ---- *)
     580  (* fresh var generators *)
    563581  ∀stmt_univ,stmt_univ' : tmpgen alloc_type.
     582  (* fresh label generators *)
    564583  ∀lbl_univ,lbl_univ'   : labgen.
     584  (* map old labels to new labels *)
    565585  ∀lbls                 : lenv.
     586  (* specify where to goto when encountering a continue or a break *)
    566587  ∀flag                 : convert_flag.
     588  (* Invariant on translation produced by [translate_statement] *)
    567589  ∀Htranslate_inv.
    568590  translate_statement alloc_type stmt_univ lbl_univ lbls flag rettyp cl_s = OK ? «〈stmt_univ',lbl_univ',cm_s〉, Htranslate_inv» →
     
    570592  lset_inclusion ? (labels_of cm_s) (labels_of (f_body cm_f)) →
    571593  (* ---- relate Clight continuation to Cminor continuation ---- *)
    572   clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type rettyp cl_k cm_k →
    573   (* ---- state invariants for memory and environments ---- *) 
     594  clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type rettyp cl_k cm_k cm_st →
     595  (* ---- state invariants for memory and environments ---- *)
     596  (* Embedding *)
    574597  ∀Em: embedding.
    575   tmp_vars_well_allocated alloc_type stmt_univ' cm_env cm_m cl_m Em →        (* locals are properly allocated *)
     598  (* locals are properly allocated *)
     599  tmp_vars_well_allocated alloc_type stmt_univ' cm_env cm_m cl_m Em →
     600  (* specify how alloc_type is built *)
     601  characterise_vars (globals ?? INV) cl_f = 〈alloc_type, stacksize〉 →
     602  (* spec. Clight env at alloc time *)
     603  (∃m,m'. exec_alloc_variables empty_env m (fn_params cl_f @ fn_vars cl_f) = 〈cl_env,m'〉) →
     604  (* memory injection *)
     605  memory_inj Em cl_m cm_m →
     606  (* map CL env to CM env *)
     607  memory_matching Em cl_ge cm_ge cl_m cm_m cl_env cm_env INV stackptr alloc_type →
     608  (* Force embedding to compute identity on functions *)
     609  (∀b. block_region b = Code → Em b = Some ? 〈b, zero_offset〉) →
     610  (* Make explicit the fact that locals in CL are mapped to a single CM block *)
     611  (∀b1.∀delta. Em b1=Some ? 〈stackptr,delta〉 →
     612               mem block b1 (blocks_of_env cl_env)) →
     613  clight_cminor_rel cl_ge cm_ge INV
     614    (ClState cl_f cl_s cl_k cl_env cl_m)
     615    (CmState cm_f cm_s cm_env fInv sInv cm_m stackptr cm_k kInv cm_st)
     616
     617| CMR_return :
     618  ∀cl_ge, cm_ge.
     619  ∀INV: clight_cminor_inv cl_ge cm_ge.
     620  ∀cl_f: function.                               (* Clight enclosing function *)
     621  ∀cm_f: internal_function.                             (* enclosing function *)
     622  ∀alloc_type.
     623  ∀cl_env, cl_m.
     624  ∀cm_env, cm_m.
     625  ∀cm_st: stack.                                              (* Cminor stack *)
     626  ∀stackptr, stacksize.
     627  ∀stmt_univ.
     628  ∀Em: embedding.
     629  tmp_vars_well_allocated alloc_type stmt_univ cm_env cm_m cl_m Em →        (* locals are properly allocated *)
    576630  characterise_vars (globals ?? INV) cl_f = 〈alloc_type, stacksize〉 →        (* specify how alloc_type is built *)
    577631  (∃m,m'. exec_alloc_variables empty_env m (fn_params cl_f @ fn_vars cl_f) = 〈cl_env,m'〉) → (* spec. Clight env *)
     
    579633  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 *)             
    580634  (∀b. block_region b = Code → Em b = Some ? 〈b, zero_offset〉) →             (* Force embedding to compute identity on functions *)
    581   clight_cminor_rel cl_ge cm_ge INV
    582     (ClState cl_f cl_s cl_k cl_env cl_m)
    583     (CmState cm_f cm_s cm_env fInv sInv cm_m stackptr cm_k kInv cm_st)
    584 
    585 | CMR_return :
    586   ∀cl_ge, cm_ge.
    587   ∀INV: clight_cminor_inv cl_ge cm_ge.
    588   (*  ∀frame_data: clight_cminor_data cl_f ?? INV.*)
    589   ∀cl_m, cm_m.
    590   ∀cm_st: stack.                                              (* Cminor stack *)
     635  (* Make explicit the fact that locals in CL are mapped to a single CM block *)
     636  (∀b1.∀delta. Em b1=Some ? 〈stackptr,delta〉 →
     637               mem block b1 (blocks_of_env cl_env)) → 
    591638  clight_cminor_rel cl_ge cm_ge INV
    592639    (ClReturnstate Vundef Kstop cl_m)
     
    597644 ∀cl_ge, cm_ge, cl_f, cm_f.
    598645 ∀INV: clight_cminor_inv cl_ge cm_ge.
    599  ∀alloc_type, cl_env, cl_m, cm_env, cm_m, stackptr.
     646 ∀alloc_type, cl_env, cl_m, cm_env, cm_m, cm_stack, stackptr.
    600647 (* TODO: put the actual invariants on memory and etc. here *)
    601648 ∀u: universe SymbolTag.
     
    611658    find_funct (fundef internal_function) cm_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? cm_fundef ∧
    612659    translate_fundef u (globals ?? INV) Hglobals_fresh cl_fundef Hfundef_fresh = OK ? cm_fundef ∧
    613     clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type rettyp cl_k cm_k
     660    clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type rettyp cl_k cm_k cm_stack
    614661 | CL_External name argtypes rettype ⇒
    615662   True
     
    622669 (* TODO: return_value_rel … INV frame_data cl_retval cm_retval →*)
    623670 (* TODO: add invariant All2 value_eq cl_args_values cm_args_values *)
    624  ∀cm_stack.
    625671 clight_cminor_rel cl_ge cm_ge INV
    626672  (ClCallstate cl_fun_id
     
    633679 ∀cl_ge, cm_ge, cl_f, cm_f.
    634680 ∀INV: clight_cminor_inv cl_ge cm_ge.
    635  ∀alloc_type, cl_env, cl_m, cm_env, cm_m, stackptr.
     681 ∀alloc_type, cl_env, cl_m, cm_env, cm_m, cm_stack, stackptr.
    636682 (* TODO: put the actual invariants on memory and etc. here *)
    637683 ∀u: universe SymbolTag.
     
    647693    find_funct (fundef internal_function) cm_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? cm_fundef ∧
    648694    translate_fundef u (globals ?? INV) Hglobals_fresh cl_fundef Hfundef_fresh = OK ? cm_fundef ∧
    649     clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type rettyp cl_k cm_k
     695    clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type rettyp cl_k cm_k cm_stack
    650696 | CL_External name argtypes rettype ⇒
    651697   True
     
    704750 translate_function func_univ (globals ?? INV) cl_f Hfresh_globals Hfresh_function = OK ? cm_f →
    705751 (* ---- relate continuations ---- *)
    706  clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type rettyp cl_k cm_k
     752 clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f cl_env cm_env alloc_type rettyp cl_k cm_k cm_stack
    707753 ∀stmt_univ,stmt_univ',lbl_univ,lbl_univ',lbl_univ'',lbls.
    708754 (* Invariants *)
     
    713759 memory_inj Em cl_m cm_m →                                                  (* memory injection *)
    714760 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 *)
    715  (∀b. block_region b = Code → Em b = Some ? 〈b, zero_offset〉) →             (* Force embedding to compute identity on functions *)
     761 (∀b. block_region b = Code → Em b = Some ? 〈b, zero_offset〉) →             (* Force embedding to compute identity on functions *)
     762 (* Make explicit the fact that locals in CL are mapped to a single CM block *)
     763 (∀b1.∀delta. Em b1=Some ? 〈stackptr,delta〉 →
     764              mem block b1 (blocks_of_env cl_env)) →
    716765 (* Expression translation and related hypotheses *)
    717766 ∀Hcond_tr.  (* invariant after converting conditional expr *)
     
    746795     (St_ifthenelse sz sg cm_cond (St_seq cm_body (St_goto entry_label)) St_skip)
    747796     (St_label exit_label St_skip)))
    748    cm_env fInv sInv cm_m stackptr cm_k kInv cm_stack)).
    749 
    750  
     797   cm_env fInv sInv cm_m stackptr cm_k kInv cm_stack)).
    751798
    752799definition clight_normal : Clight_state → bool ≝
     
    768815    (λg. Cminor_labelled)
    769816    (λg. Cminor_classify)
    770     (λx,y,H. an_identifier ? one).   (* XXX TODO *)
     817    (λx,y,H. an_identifier ? one). (* XXX TODO *)
    771818
    772819(* --------------------------------------------------------------------------- *)
     
    13991446       ]
    14001447  ]
    1401 ] qed. 
     1448] qed.
     1449
     1450axiom load_value_after_free_list_inversion :
     1451  ∀ty, m, blocks, b, o, v.
     1452  load_value_of_type ty (free_list m blocks) b o = Some ? v → 
     1453  load_value_of_type ty m b o = Some ? v.
    14021454
    14031455(* --------------------------------------------------------------------------- *)
     
    14131465   2. call and return steps are simulated by a call/return step plus [m] normal
    14141466      steps (to copy stack allocated parameters / results); and
    1415    3. lone cost label steps are simulates by a lone cost label step
     1467   3. lone cost label steps are simulated by a lone cost label step
    14161468   
    14171469   These should allow us to maintain enough structure to identify the Cminor
    14181470   subtrace corresponding to a measurable Clight subtrace.
    14191471 *)
     1472
     1473 
    14201474
    14211475lemma clight_cminor_normal :
     
    14421496| 7: #cond #body | 8: #init #cond #step #body | 9,10: | 11: #retval | 12: #cond #switchcases | 13: #lab #body
    14431497| 14: #lab | 15: #cost #body ]
     1498(*
     1499[ 11: (* Return case *)
     1500     #cm_s #cl_k #cm_k #cm_st #cl_f #cm_f #rettyp
     1501     #alloc_type #cl_env #cl_m #cm_env #cm_m #stackptr #stacksize
     1502     (* introduce everything *)
     1503     #fInv #sInv #kInv #Htarget_type #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function
     1504     #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls
     1505     #flag #Htrans_inv #Htranslate #Hlabel_inclusion #Hcont_rel
     1506     #Em #Htmp_vars_well_allocated #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id
     1507     @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
     1508     destruct (HA HB)
     1509     @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE #_
     1510     destruct (HC HD HE)
     1511     whd in Htranslate:(??%?);
     1512     cases retval in Htranslate; normalize nodelta
     1513     [ cases rettyp in Htrans_inv Hcont_rel;
     1514       [ 2: #opttyp normalize nodelta #Htrans_inv #_
     1515            #Habsurd destruct (Habsurd)
     1516       | 1: #Htrans_inv #Hcont_rel normalize nodelta #Heq destruct (Heq)
     1517            #s2 #tr whd in ⊢ ((??%?) → ?);
     1518            cases (fn_return cl_f)
     1519            [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
     1520            | #structname #fieldspec | #unionname #fieldspec | #id ]
     1521            normalize nodelta
     1522            [ 1:
     1523            | *: #Habsurd destruct (Habsurd) ]
     1524            whd in ⊢ ((??%?) → ?);
     1525            #Heq destruct (Heq)
     1526            %{1} whd @conj try @conj
     1527            [ 3: #Habsurd destruct (Habsurd)
     1528            | 1: @refl ]
     1529            @CMR_return
     1530*)     
    14441531[ 6: (* While *)
    14451532     #cm_s #cl_k #cm_k #cm_st #cl_f #cm_f #rettyp
     
    14571544     #Hcont_rel
    14581545     #Em #Htmp_vars_well_allocated #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id
     1546     #Hframe_spec
    14591547     @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
    14601548     destruct (HA HB)
     
    16051693     #Htmp_vars_well_allocated
    16061694     #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id
     1695     #Hframe_spec
    16071696     @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
    16081697     destruct (HA HB)
     
    18591948    [ (* Kstop continuation *)
    18601949      (* simplifying the goal using outcome of the inversion *)
    1861       #kcl_ge #kcm_ge #kINV #kcl_f #kcm_f #ktarget_type #kcl_env #kcm_env #kalloc_type
     1950      #kcl_ge #kcm_ge #kINV #kcl_f #kcm_f #ktarget_type #kcl_env #kcm_env #kalloc_type #kstack #Hkstack
    18621951      @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
    18631952      destruct (HA HB)
     
    18651954      destruct (HC HD HE)
    18661955      @(jmeq_absorb ?????) #HF @(jmeq_absorb ?????) #HG @(jmeq_absorb ?????) #HH
    1867       @(jmeq_absorb ?????) #HI @(jmeq_absorb ?????) #HJ @(jmeq_absorb ?????) #HK
    1868       destruct (HF HG HH HI HJ HK) #_
     1956      @(jmeq_absorb ?????) #HI @(jmeq_absorb ?????) #HJ @(jmeq_absorb ?????) #HK @(jmeq_absorb ?????) #HL
     1957      destruct (HF HG HH HI HJ HK HL) #_
    18691958      (* re-introduce everything *)
    18701959      #Hlabel_inclusion
     
    18761965      (* In this simple case, trivial translation *)
    18771966      destruct (Heq_translate)
    1878       #Em #Htmp_vars_well_allocated #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id
     1967      #Em #Htmp_vars_well_allocated #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id #Hframe_spec
    18791968      @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
    18801969      destruct (HA HB)
     
    18891978      %{1} whd @conj try @conj try @refl
    18901979      [ 2: #Habsurd destruct (Habsurd) ]
    1891       @CMR_return
     1980      (* Use the memory injection stuff to produce a new memory injection *)
     1981      cut (memory_inj Em (free_list cl_m (blocks_of_env kcl_env)) (free cm_m stackptr))
     1982      [ @(freelist_memory_inj_m1_m2 Em cl_m cm_m
     1983            (free_list cl_m (blocks_of_env kcl_env))
     1984            (free cm_m stackptr) Hinjection (blocks_of_env kcl_env) stackptr ? (refl ??) (refl ??))
     1985        assumption ]
     1986      #Hinjection'
     1987      @(CMR_return … Halloc_hyp Hcl_env_hyp … Hinjection') try assumption
     1988      [ 2: #b lapply (Hmatching b)
     1989           cases (lookup ?? kcl_env b) normalize nodelta
     1990           [ 1: #H @H
     1991           | 2: #b' cases (lookup ?? kalloc_type b) normalize nodelta
     1992             [ 1: #H @H
     1993             | 2: * #kalloc_type #ty normalize nodelta
     1994                  cases kalloc_type normalize nodelta try //
     1995                  #H #v #Hload_after_free @H
     1996                  @(load_value_after_free_list_inversion … Hload_after_free)
     1997             ]
     1998           ]
     1999      | 1: (* TODO: lemma *) @cthulhu
     2000      ] 
    18922001    | (* Kseq *)
    1893       #kcl_ge #kcm_ge #kINV #kcl_f #kcm_f #ktarget_type #kalloc_type #kcl_s #kcm_s
     2002      #kcl_ge #kcm_ge #kINV #kcl_f #kcm_f #ktarget_type #kstack #kalloc_type #kcl_s #kcm_s
    18942003      #kcl_env #kcm_env #kcl_k' #kcm_k' #kstmt_univ #kstmt_univ' #klbl_univ #klbl_univ' #klbls #kflag
    18952004      * * * * #kHstmt_inv #kHlabels_translated #kHtmps_preserved
     
    19002009      destruct (HC HD HE)
    19012010      @(jmeq_absorb ?????) #HF @(jmeq_absorb ?????) #HG @(jmeq_absorb ?????) #HH @(jmeq_absorb ?????) #HI
    1902       @(jmeq_absorb ?????) #HJ @(jmeq_absorb ?????) #HK
    1903       destruct (HF HG HH HI HJ HK) #_
     2011      @(jmeq_absorb ?????) #HJ @(jmeq_absorb ?????) #HK @(jmeq_absorb ?????) #HL
     2012      destruct (HF HG HH HI HJ HK HL) #_
    19042013      #Hlabel_inclusion
    19052014      #stmt_univ' #stmt_univ #fInv #sInv #kInv #Htarget_type #Hfresh_function #Hfresh_globals
     
    19082017      (* In this simple case, trivial translation *)
    19092018      #Heq_translate destruct (Heq_translate) #Em
    1910       #Htmp_vars_well_alloc #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id
     2019      #Htmp_vars_well_alloc #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id #Hframe_spec
    19112020      @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
    19122021      destruct (HA HB)
     
    19212030      (* TODO: lemma allowing to prove this from [Htmp_vars_well_alloc] + tmp_gen inclusion *)
    19222031    | (* Kwhile continuation *)
    1923       #kcl_ge #kcm_ge #kINV #kcl_f #kcm_f #ktarget_type #kalloc_type #kcl_env #kcm_env
     2032      #kcl_ge #kcm_ge #kINV #kcl_f #kcm_f #ktarget_type #kstack #kalloc_type #kcl_env #kcm_env
    19242033      #kcl_k' #kcm_k' #ksz #ksg #kcl_ty #kcl_cond_desc #kcl_body #kHeq_ty #kcm_cond #kcm_body
    19252034      #kentry #kexit #kstmt_univ #kstmt_univ' #klbl_univ #klbl_univ' #klbl_univ''
     
    19372046      @(jmeq_absorb ?????) #HF @(jmeq_absorb ?????) #HG @(jmeq_absorb ?????) #HH
    19382047      @(jmeq_absorb ?????) #HI @(jmeq_absorb ?????) #HJ @(jmeq_absorb ?????) #HK
    1939       destruct (HF HG HH HI HJ HK) #_
     2048      @(jmeq_absorb ?????) #HL
     2049      destruct (HF HG HH HI HJ HK HL) #_
    19402050      #Hlabel_inclusion
    19412051      #stmt_univ' #stmt_univ #fInv #sInv #kInv #Htarget_type #Hfresh_function #Hfresh_globals
     
    19462056      #Heq_translate destruct (Heq_translate)
    19472057      #Em #Htmp_vars_well_allocated #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching
    1948       #HEm_fn_id
     2058      #HEm_fn_id #Hframe_spec
    19492059      @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
    19502060      destruct (HA HB)
     
    19832093     #Hreturn_ok #Hlabel_wf generalize in match (conj ????); #Hugly #Htranslate
    19842094     #Hlabel_inclusion #Hcont_rel
    1985      #Em #Htmp_vars_well_allocated #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id
     2095     #Em #Htmp_vars_well_allocated #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id #Hframe_spec
    19862096     @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
    19872097     destruct (HA HB)
     
    22492359     #Hreturn_ok #Hlabel_wf generalize in match (conj ????); #Hugly #Htranslate #Hlabel_inclusion
    22502360     #Hcont_rel
    2251      #Em #Htmp_vars_well_allocated #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id
     2361     #Em #Htmp_vars_well_allocated #Halloc_hyp #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id #Hframe_spec
    22522362     @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
    22532363     destruct (HA HB)
     
    22732383| *: @cthulhu ]
    22742384| 2: (* Return state *)
    2275   @cthulhu
     2385  #cl_ge #cm_ge #INV' #cl_f #cm_f #alloc_type
     2386  #cl_env #cl_m #cm_env #c_m #cm_st #stackptr #stacksize
     2387  #stmt_univ #Em #Htmp_vars_wa #Hcharac #Hexec_alloc #Hinj #Hmatch #Hem_fn_id #Hframe
     2388  @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
     2389  destruct (HA HB)
     2390  @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
     2391  destruct (HC HD HE)
     2392  #_
     2393  whd in Hclight_normal:%;
     2394  @False_ind @Hclight_normal
    22762395| 3: (* Call state, nostore *)
    2277   @cthulhu
     2396  #cl_ge #cm_ge #cl_f #cm_f #INV' #alloc_types
     2397  #cl_env #cl_m #cm_env #cm_m #stackptr #u #cl_fundef #cm_fundef
     2398  #Hglobals_fresh #Hfundef_fresh #rettyp #Hrettyp #cl_k #cm_k #fblock
     2399  #Hcont_rel #cl_fun_id #cm_fun_id #Hfun_id_eq #cl_retval #cm_retval
     2400  #sInv #fInv #kInv #cl_argvals #cm_argvals #cm_stack
     2401  @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
     2402  destruct (HA HB)
     2403  @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
     2404  destruct (HC HD HE)
     2405  whd in Hclight_normal:%;
     2406  @False_ind @Hclight_normal
    22782407| 4: (* Call state, store *)
    2279   @cthulhu
     2408  #cl_ge #cm_ge #cl_f #cm_f #INV' #alloc_types
     2409  #cl_env #cl_m #cm_env #cm_m #cm_stack #stackptr #u #cl_fundef #cm_fundef
     2410  #Hglobals_fresh #Hfundef_fresh #rettyp #Hrettyp #cl_k #cm_k #fblock
     2411  #Hcont_rel #cl_fun_id #cm_fun_id #Hfun_id_eq
     2412  #cl_rettyp #cl_retval #cl_retrace #cm_retval #cl_lhs #cm_lhs
     2413  #Hinvariant_on_cm_lhs #Hexec_lvalue #Htranslate_dest #cm_ret_var
     2414  #sInv #fInv #kInv #cl_argvals #cm_argvals #cm_stack
     2415  @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
     2416  destruct (HA HB)
     2417  @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
     2418  destruct (HC HD HE)
     2419  whd in Hclight_normal:%;
     2420  @False_ind @Hclight_normal
    22802421| 5: (* Intermediary While state *)
    22812422     (* ---------------------------------------------------------------------- *)
     
    22872428#stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbl_univ'' #lbls
    22882429#Em #Htmp_vars_well_allocated #Halloc_hyp
    2289 #Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id #Hexpr_vars #Htranslate_expr
     2430#Hcl_env_hyp #Hinjection #Hmatching #HEm_fn_id #Hframe_spec #Hexpr_vars #Htranslate_expr
    22902431#Hentry_ex #Hexit_ex #Htranslate_inv #Hmk_labels #Htranslate_statement
    22912432#Hlabel_inclusion #Hlabel_exists #Hinv1 #Hinv2 #Hfind_label
     
    23632504] qed.
    23642505
     2506 
     2507lemma clight_cminor_call_return :
     2508  ∀g1, g2.
     2509  ∀INV:clight_cminor_inv g1 g2.
     2510  ∀s1,s1'.
     2511  clight_cminor_rel g1 g2 INV s1 s1' →
     2512  match Clight_classify s1 with
     2513  [ cl_call ⇒ true
     2514  | cl_return ⇒ true
     2515  | _ ⇒ false ] →
     2516  ∀s2,tr. step … (pcs_exec cl_pre) g1 s1 = Value … 〈tr, s2〉 →
     2517  ∃m. after_n_steps m ?? (pcs_exec cm_pre) g2 s1' (λs.cminor_normal s) (λtr',s2'.
     2518    tr = tr' ∧
     2519    clight_cminor_rel g1 g2 INV s2 s2' ∧
     2520      (m = 0 → lex_lt (measure_Clight s2) (measure_Clight s1))
     2521  ).
     2522#g1 #g2 #INV #s1 #s1' #Hstate_rel #Hclight_class
     2523inversion Hstate_rel
     2524[ 1: (* normal *)
     2525  #cl_ge #cm_ge #INV' #cl_s
     2526  #cm_s #cl_k #cm_k #cm_st #cl_f #cm_f #rettyp
     2527  #alloc_type #cl_env #cl_m #cm_env #cm_m #stackptr #stacksize
     2528  (* introduce everything *)
     2529  #fInv #sInv #kInv #Htarget_type #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function
     2530  #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls
     2531  #flag  #Htrans_inv #Htrans_stmt #Hincl #HA #HB #HC
     2532  #HE #HF #HG #HI #HJ #HK
     2533  @(jmeq_absorb ?????) #H1 @(jmeq_absorb ?????) #H2
     2534  destruct (H1 H2)
     2535  @(jmeq_absorb ?????) #H3 @(jmeq_absorb ?????) #H4 @(jmeq_absorb ?????) #H5
     2536  destruct (H3 H4 H5)
     2537  @False_ind @Hclight_class
     2538| 5:
     2539  #cl_ge #cm_ge #INV' #cl_s
     2540  #cm_s #cl_k #cm_k #cm_st #cl_f #cm_f #rettyp
     2541  #alloc_type #cl_k #cm_k #sz #sg #cl_ty #cl_cond_desc #cl_body #entry_lab #exit_lab
     2542  #cm_cond #cm_body #cm_stack #rettyp' #kInv
     2543  (* introduce everything *)
     2544  #fInv #sInv #kInv #Htarget_type #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function
     2545  #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls
     2546  #lbl1 #lbl2 #Em #Htmp_vars #Hcharac #Hexec #Hinj #Hmatching #Hem #Hframe #Hcond_tr
     2547  #Htransl #Hex1 #Hex2 #Htransinv #Hmklabs #Htranstmt #Hincl
     2548  #Hlabdecl #Hinv1 #Hinv2 #Hfindlab
     2549  @(jmeq_absorb ?????) #H1 @(jmeq_absorb ?????) #H2
     2550  destruct (H1 H2)
     2551  @(jmeq_absorb ?????) #H3 @(jmeq_absorb ?????) #H4 @(jmeq_absorb ?????) #H5
     2552  destruct (H3 H4 H5)
     2553  @False_ind @Hclight_class
     2554| *: @cthulhu
     2555] qed.
     2556
    23652557
    23662558(* TODO: adapt the following to the new goal shape. *)
    23672559(*
    2368 axiom clight_cminor_call_return :
    2369   ∀INV:clight_cminor_inv.
    2370   ∀s1,s1',s2,tr.
    2371   clight_cminor_rel INV s1 s1' →
    2372   match Clight_classify s1 with [ cl_call ⇒ true | cl_return ⇒ true | _ ⇒ false ] →
    2373   after_n_steps 1 … clight_exec (ge_cl INV) s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) →
    2374   ∃m. after_n_steps (S m) … Cminor_exec (ge_cm INV) s1' (λs.cminor_normal s) (λtr',s2'.
    2375     tr = tr' ∧
    2376     clight_cminor_rel INV s2 s2'
    2377   ).
    2378 
     2560 
    23792561axiom clight_cminor_cost :
    23802562  ∀INV:clight_cminor_inv.
Note: See TracChangeset for help on using the changeset viewer.