include "Clight/toCminor.ma".
include "Clight/CexecInd.ma".
include "common/Globalenvs.ma".
include "Clight/memoryInjections.ma".
include "Clight/abstract.ma".
include "Cminor/abstract.ma".

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


(* When we characterise the local Clight variables, those that are stack
   allocated are given disjoint regions of the stack. *)

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

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

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



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

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

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

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

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


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


(* This is the statement for expression simulation copied fro toCminorCorrectnessExpr.ma,
   for easier reference.
lemma eval_expr_sim :
  (* [cl_cm_inv] maps CL globals to CM globals, including functions *)
  ∀cl_cm_inv  : clight_cminor_inv.
  (* current function (defines local environment) *)
  ∀f          : function.
  (* [alloctype] maps variables to their allocation type (global, stack, register) *)
  ∀alloctype  : var_types.
  ∀stacksize  : ℕ.
  ∀alloc_hyp  : characterise_vars (globals cl_cm_inv) f = 〈alloctype, stacksize〉.
  (* environments *)
  ∀cl_env     : cl_env.
  ∀cm_env     : cm_env.
  (* Characterise clight environment. Needed to prove that some variable is either a parameter or a local.  *)
  ∀cl_env_hyp : ∃m,m'. exec_alloc_variables empty_env m (fn_params f @ fn_vars f) = 〈cl_env,m'〉.
  (* CL and CM memories *)
  ∀cl_m       : mem.
  ∀cm_m       : mem.
  (* memory injection and matching *)
  ∀embed      : embedding.
  ∀injection  : memory_inj embed cl_m cm_m.
  ∀stackptr   : block.
  ∀matching   : memory_matching embed cl_m cm_m cl_env cm_env cl_cm_inv stackptr alloctype.
  (* clight expr to cminor expr *)
  (∀(e:expr).
   ∀(e':CMexpr (typ_of_type (typeof e))).
   ∀Hexpr_vars.
   translate_expr alloctype e = OK ? («e', Hexpr_vars») →
   ∀cl_val,trace,Hyp_present.
   exec_expr (ge_cl … cl_cm_inv) cl_env cl_m e = OK ? 〈cl_val, trace〉 →
   ∃cm_val. eval_expr (ge_cm cl_cm_inv) (typ_of_type (typeof e)) e' cm_env Hyp_present stackptr cm_m = OK ? 〈trace, cm_val〉 ∧
            value_eq embed cl_val cm_val) ∧
   (* clight /lvalue/ to cminor /expr/ *)
  (∀ed,ty.
   ∀(e':CMexpr ASTptr).
   ∀Hexpr_vars.
   translate_addr alloctype (Expr ed ty) = OK ? («e', Hexpr_vars») →
   ∀cl_blo,cl_off,trace,Hyp_present.
   exec_lvalue' (ge_cl … cl_cm_inv) cl_env cl_m ed ty = OK ? 〈cl_blo, cl_off, trace〉 →
   ∃cm_val. eval_expr (ge_cm cl_cm_inv) ASTptr e' cm_env Hyp_present stackptr cm_m = OK ? 〈trace, cm_val〉 ∧
            value_eq embed (Vptr (mk_pointer cl_blo cl_off)) cm_val).   
*)




axiom clight_cminor_rel : clight_cminor_inv → Clight_state → Cminor_state → Prop.

(* Conjectured simulation results

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

definition clight_normal : Clight_state → bool ≝
λs. match Clight_classify s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ].

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

axiom clight_cminor_normal :
  ∀INV:clight_cminor_inv.
  ∀s1,s1',s2,tr.
  clight_cminor_rel INV s1 s1' →
  clight_normal s1 →
  ¬ Clight_labelled s1 →
  ∃n. after_n_steps (S n) … clight_exec (ge_cl INV) s1 (λs.clight_normal s ∧ ¬ Clight_labelled s) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) →
  ∃m. after_n_steps (S m) … Cminor_exec (ge_cm INV) s1' (λs.cminor_normal s) (λtr',s2'.
    tr = tr' ∧
    clight_cminor_rel INV s2 s2'
  ).

axiom clight_cminor_call_return :
  ∀INV:clight_cminor_inv.
  ∀s1,s1',s2,tr.
  clight_cminor_rel INV s1 s1' →
  match Clight_classify s1 with [ cl_call ⇒ true | cl_return ⇒ true | _ ⇒ false ] →
  after_n_steps 1 … clight_exec (ge_cl INV) s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) →
  ∃m. after_n_steps (S m) … Cminor_exec (ge_cm INV) s1' (λs.cminor_normal s) (λtr',s2'.
    tr = tr' ∧
    clight_cminor_rel INV s2 s2'
  ).

axiom clight_cminor_cost :
  ∀INV:clight_cminor_inv.
  ∀s1,s1',s2,tr.
  clight_cminor_rel INV s1 s1' →
  Clight_labelled s1 →
  after_n_steps 1 … clight_exec (ge_cl INV) s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) →
  after_n_steps 1 … Cminor_exec (ge_cm INV) s1' (λs.true) (λtr',s2'.
    tr = tr' ∧
    clight_cminor_rel INV s2 s2'
  ).