Module SepInvariant

From compcert Require Import common.Separation.
From compcert Require Import common.Values.
From compcert Require Import common.Memdata.
From compcert Require Import common.Memory.
From compcert Require Import common.Globalenvs.
From compcert Require common.Errors.
From compcert Require Import cfrontend.Ctypes.
From compcert Require Import cfrontend.Clight.
From compcert Require Import lib.Maps.
From compcert Require Import lib.Coqlib.
From compcert Require Import lib.Integers.

From Velus Require Import Common.
From Velus Require Import Common.CompCertLib.
From Velus Require Import Ident.
From Velus Require Import Environment.
From Velus Require Import VelusMemory.

From Coq Require Import List.
Import List.ListNotations.
From Coq Require Import ZArith.BinInt.

From Coq Require Import Program.Tactics.

From Velus Require Import ObcToClight.MoreSeparation.
From Velus Require Import ObcToClight.Generation.
From Velus Require Import ObcToClight.GenerationProperties.
From Velus Require Import ObcToClight.Interface.

Import Obc.Syn.
Import Obc.Sem.
Import Obc.Typ.

Open Scope list.
Open Scope sep_scope.
Open Scope Z.

Definition match_value (ov: option val) (v: val) : Prop :=
  match ov with
  | None => True
  | Some v' => v = v'
  end.

Definition match_var (ve: venv) (le: temp_env) (x: ident) : Prop :=
  match le ! x with
  | Some v => match_value (Env.find x ve) v
  | None => False
  end.

Section Staterep.
  Variable ge : composite_env.

  Definition staterep_mems (cls: class) (me: menv) (b: block) (ofs: Z) '((x, ty): ident * type) :=
    match field_offset ge x (make_members cls) with
    | Errors.OK d =>
     contains_w (type_chunk ty) b (ofs + d) (match_value (find_val x me))
    | Errors.Error _ => sepfalse
    end.

  Fixpoint staterep
           (p: program) (clsnm: ident) (me: menv) (b: block) (ofs: Z): massert :=
    match p with
    | nil => sepfalse
    | cls :: p' =>
      if ident_eqb clsnm cls.(c_name)
      then
        sepall (staterep_mems cls me b ofs) cls.(c_mems)
        **
        sepall (fun '((i, c): ident * ident) =>
                  match field_offset ge i (make_members cls) with
                  | Errors.OK d =>
                    staterep p' c (instance_match i me) b (ofs + d)
                  | Errors.Error _ => sepfalse
                  end) cls.(c_objs)
      else staterep p' clsnm me b ofs
    end.

  Definition staterep_objs (p: program) (cls: class) (me: menv) (b: block) (ofs: Z) '((i, c): ident * ident) : massert :=
    match field_offset ge i (make_members cls) with
    | Errors.OK d =>
      staterep p c (instance_match i me) b (ofs + d)
    | Errors.Error _ => sepfalse
    end.

  Lemma staterep_objs_not_in:
    forall objs p cls me i me_i b ofs,
      ~ InMembers i objs ->
      sepall (staterep_objs p cls me b ofs) objs <-*->
      sepall (staterep_objs p cls (add_inst i me_i me) b ofs) objs.

  Lemma staterep_cons:
    forall cls prog clsnm me b ofs,
      clsnm = cls.(c_name) ->
      staterep (cls :: prog) clsnm me b ofs <-*->
      sepall (staterep_mems cls me b ofs) cls.(c_mems)
      ** sepall (staterep_objs prog cls me b ofs) cls.(c_objs).

  Lemma staterep_skip_cons:
    forall cls prog clsnm me b ofs,
      clsnm <> cls.(c_name) ->
      staterep (cls :: prog) clsnm me b ofs <-*-> staterep prog clsnm me b ofs.

  Lemma staterep_skip_app:
    forall clsnm prog oprog me b ofs,
      find_class clsnm oprog = None ->
      staterep (oprog ++ prog) clsnm me b ofs <-*-> staterep prog clsnm me b ofs.

  Remark staterep_skip:
    forall c clsnm prog prog' me b ofs,
      find_class clsnm prog = Some (c, prog') ->
      staterep prog clsnm me b ofs <-*->
      staterep (c :: prog') clsnm me b ofs.

  Lemma decidable_footprint_staterep:
    forall p clsnm me b ofs,
      decidable_footprint (staterep p clsnm me b ofs).

  Lemma footprint_perm_staterep:
    forall p clsnm me b ofs b' lo hi,
      footprint_perm_w (staterep p clsnm me b ofs) b' lo hi.

  Hint Resolve decidable_footprint_staterep footprint_perm_staterep.

End Staterep.


Section StructInBounds.
  Variable env : composite_env.
  Hypothesis env_consistent: composite_env_consistent env.

  Definition struct_in_bounds (min max ofs: Z) (flds: Ctypes.members) :=
    min <= ofs /\ ofs + sizeof_struct env 0 flds <= max.

  Lemma struct_in_bounds_sizeof:
    forall id co,
      env!id = Some co ->
      struct_in_bounds 0 (sizeof_struct env 0 (co_members co)) 0 (co_members co).

  Lemma struct_in_bounds_weaken:
    forall min' max' min max ofs flds,
      struct_in_bounds min max ofs flds ->
      min' <= min ->
      max <= max' ->
      struct_in_bounds min' max' ofs flds.

  Lemma struct_in_bounds_field:
    forall min max ofs flds id d,
      struct_in_bounds min max ofs flds ->
      field_offset env id flds = Errors.OK d ->
      min <= ofs + d <= max.

  Lemma struct_in_struct_in_bounds:
    forall min max ofs flds id sid d co a,
      struct_in_bounds min max ofs flds ->
      field_offset env id flds = Errors.OK d ->
      field_type id flds = Errors.OK (Tstruct sid a) ->
      env!sid = Some co ->
      co_su co = Struct ->
      struct_in_bounds min max (ofs + d) (co_members co).

End StructInBounds.

Section StateRepProperties.

  Variable prog: program.
  Variable gcenv: composite_env.

  Hypothesis gcenv_consistent: composite_env_consistent gcenv.

  Hypothesis make_members_co:
    forall clsnm cls prog',
      find_class clsnm prog = Some (cls, prog') ->
      (exists co, gcenv!clsnm = Some co
             /\ co_su co = Struct
             /\ co_members co = make_members cls
             /\ attr_alignas (co_attr co) = None
             /\ NoDupMembers (co_members co)
             /\ co.(co_sizeof) <= Ptrofs.max_unsigned).

  Lemma struct_in_struct_in_bounds':
    forall min max ofs clsid cls o c cls' prog' prog'',
      wt_program prog ->
      find_class clsid prog = Some (cls, prog') ->
      struct_in_bounds gcenv min max ofs (make_members cls) ->
      In (o, c) cls.(c_objs) ->
      find_class c prog' = Some (cls', prog'') ->
      exists d, field_offset gcenv o (make_members cls) = Errors.OK d
           /\ struct_in_bounds gcenv min max (ofs + d) (make_members cls').

  Hint Resolve Z.divide_trans.

  Lemma range_staterep:
    forall b clsnm,
      wt_program prog ->
      find_class clsnm prog <> None ->
      range_w b 0 (sizeof gcenv (type_of_inst clsnm)) -*>
      staterep gcenv prog clsnm mempty b 0.

  Lemma staterep_deref_mem:
    forall clsnm c prog prog' m me b ofs x ty d v P,
      find_class clsnm prog = Some (c, prog') ->
      m |= staterep gcenv prog clsnm me b ofs ** P ->
      In (x, ty) c.(c_mems) ->
      find_val x me = Some v ->
      field_offset gcenv x (make_members c) = Errors.OK d ->
      Clight.deref_loc (cltype ty) m b (Ptrofs.repr (ofs + d)) v.

  Lemma staterep_field_offset:
    forall m me c prog' cls prog b ofs x ty P,
      find_class c prog = Some (cls, prog') ->
      m |= staterep gcenv prog c me b ofs ** P ->
      In (x, ty) (c_mems cls) ->
      exists d, field_offset gcenv x (make_members cls) = Errors.OK d
           /\ 0 <= ofs + d <= Ptrofs.max_unsigned.

  Lemma staterep_extract:
    forall cid c prog' me b ofs m i c' P,
      wt_program prog ->
      find_class cid prog = Some (c, prog') ->
      (In (i, c') c.(c_objs)
       /\ m |= staterep gcenv prog cid me b ofs ** P)
      <-> exists objs objs' d,
          c.(c_objs) = objs ++ (i, c') :: objs'
          /\ field_offset gcenv i (make_members c) = Errors.OK d
          /\ m |= staterep gcenv prog c' (instance_match i me) b (ofs + d)
                  ** sepall (staterep_mems gcenv c me b ofs) c.(c_mems)
                  ** sepall (staterep_objs gcenv prog c me b ofs) (objs ++ objs')
                  ** P.

End StateRepProperties.

Section Fieldsrep.
  Variable ge : composite_env.
  Hypothesis ge_consistent : composite_env_consistent ge.

  Definition fieldrep (ve: venv) (flds: members) (b: block) '((x, ty) : ident * Ctypes.type) : massert :=
    match field_offset ge x flds, access_mode ty with
    | Errors.OK d, By_value chunk =>
      contains chunk b d (match_value (Env.find x ve))
    | _, _ => sepfalse
    end.

  Definition fieldsrep (ve: venv) (flds: members) (b: block) : massert :=
    sepall (fieldrep ve flds b) flds.

  Lemma fieldsrep_deref_mem:
    forall m ve flds b x ty d v P,
      m |= fieldsrep ve flds b ** P ->
      In (x, ty) flds ->
      Env.find x ve = Some v ->
      field_offset ge x flds = Errors.OK d ->
      Clight.deref_loc ty m b (Ptrofs.repr d) v.

  Lemma footprint_perm_fieldsrep:
    forall ve flds b b' lo hi,
      footprint_perm (fieldsrep ve flds b) b' lo hi.

  Lemma footprint_decidable_fieldsrep:
    forall ve flds b,
      decidable_footprint (fieldsrep ve flds b).

  Lemma fieldsrep_empty':
    forall flds b,
      NoDupMembers flds ->
      (forall x ty, In (x, ty) flds ->
               exists chunk, access_mode ty = By_value chunk
                        /\ (Memdata.align_chunk chunk | alignof ge ty)) ->
      sepall (field_range ge flds b 0) flds <-*-> fieldsrep vempty flds b.

  Lemma fieldsrep_empty:
    forall nm co b,
      ge!nm = Some co ->
      co_su co = Struct ->
      NoDupMembers (co_members co) ->
      (forall x ty, In (x, ty) (co_members co) ->
               exists chunk, access_mode ty = By_value chunk
                        /\ (Memdata.align_chunk chunk | alignof ge ty)) ->
      range b 0 (co_sizeof co) -*> fieldsrep vempty (co_members co) b.

  Lemma fieldsrep_any_empty:
    forall flds ve b,
      fieldsrep ve flds b -*> fieldsrep vempty flds b.

  Lemma fieldsrep_nodup:
    forall (xs: list (ident * type)) vs flds ve ob,
      NoDup (map fst xs ++ map fst flds) ->
      fieldsrep ve flds ob <-*-> fieldsrep (Env.adds (map fst xs) vs ve) flds ob.

  Lemma fieldsrep_findvars:
    forall ve xs vs b,
      Forall2 (fun x v => Env.find x ve = v) (map fst xs) vs ->
      fieldsrep ve xs b -*> fieldsrep (Env.adds_opt (map fst xs) vs vempty) xs b.

  Lemma fieldsrep_field_offset:
    forall m ve flds b P,
      m |= fieldsrep ve flds b ** P ->
      forall x ty,
        In (x, ty) flds ->
        exists d, field_offset ge x flds = Errors.OK d
             /\ 0 <= d <= Ptrofs.max_unsigned.

  Lemma fieldsrep_add:
    forall outb ve x v flds,
      ~ InMembers x flds ->
      fieldsrep ve flds outb -*>
      fieldsrep (Env.add x v ve) flds outb.

End Fieldsrep.

Hint Resolve footprint_perm_fieldsrep footprint_decidable_fieldsrep.

Section SubRep.

  Variable ge : composite_env.

  Definition fieldsrep_of (id: ident) (b: block): massert :=
    match ge ! id with
    | Some co =>
      fieldsrep ge vempty (co_members co) b
    | None => sepfalse
    end.

  Definition subrep_inst '((_, (b, t)): ident * (block * Ctypes.type)): massert :=
    match t with
    | Tstruct id _ => fieldsrep_of id b
    | _ => sepfalse
    end.

  Definition subrep_inst_env (e: Clight.env) '((x, t): ident * Ctypes.type): massert :=
    match e ! x with
    | Some (b, Tstruct id _ as t') =>
      if type_eq t t' then fieldsrep_of id b else sepfalse
    | _ => sepfalse
    end.

  Definition subrep (f: method) (e: Clight.env) : massert :=
    sepall (subrep_inst_env e)
           (make_out_vars (instance_methods f)).

  Lemma subrep_eqv:
    forall f e,
      Permutation.Permutation (make_out_vars (instance_methods f))
                              (map drop_block (PTree.elements e)) ->
      subrep f e <-*-> sepall subrep_inst (PTree.elements e).

  Definition range_inst '((_, (b, t)): ident * (block * Ctypes.type)) : massert :=
    range b 0 (Ctypes.sizeof ge t).

  Definition range_inst_env (e: Clight.env) (x: ident) : massert :=
    match e ! x with
    | Some (b, t) => range b 0 (Ctypes.sizeof ge t)
    | None => sepfalse
    end.

  Definition subrep_range (e: Clight.env) : massert :=
    sepall range_inst (PTree.elements e).

  Lemma subrep_range_eqv:
    forall e,
      subrep_range e <-*-> sepall (range_inst_env e) (map fst (PTree.elements e)).

  Remark decidable_footprint_subrep_inst:
    forall x, decidable_footprint (subrep_inst x).

  Lemma decidable_subrep:
    forall f e, decidable_footprint (subrep f e).

  Remark footprint_perm_subrep_inst:
    forall x b lo hi,
      footprint_perm (subrep_inst x) b lo hi.

  Remark disjoint_footprint_range_inst:
    forall l b lo hi,
      ~ InMembers b (map snd l) ->
      disjoint_footprint (range b lo hi) (sepall range_inst l).

  Hint Resolve decidable_footprint_subrep_inst decidable_subrep footprint_perm_subrep_inst.

  Lemma range_wand_equiv:
    forall e,
      composite_env_consistent ge ->
      Forall (wf_struct ge) (map drop_block (PTree.elements e)) ->
      NoDupMembers (map snd (PTree.elements e)) ->
      subrep_range e <-*->
      sepall subrep_inst (PTree.elements e)
      ** (sepall subrep_inst (PTree.elements e) -* subrep_range e).

  Lemma subrep_extract:
    forall f f' e m o c' P,
      M.MapsTo (o, f') c' (instance_methods f) ->
      m |= subrep f e ** P <->
      exists b co ws xs,
        e ! (prefix_out f' o) = Some (b, type_of_inst (prefix_fun f' c'))
        /\ ge ! (prefix_fun f' c') = Some co
        /\ make_out_vars (instance_methods f) = ws ++ (prefix_out f' o, type_of_inst (prefix_fun f' c')) :: xs
        /\ m |= fieldsrep ge vempty (co_members co) b
              ** sepall (subrep_inst_env e) (ws ++ xs)
              ** P.

End SubRep.

Lemma free_exists:
  forall ge e m P,
    let gcenv := Clight.genv_cenv ge in
    m |= subrep_range gcenv e ** P ->
    exists m',
      Mem.free_list m (blocks_of_env ge e) = Some m'
      /\ m' |= P.

Definition varsrep (f: method) (ve: venv) (le: temp_env) : massert :=
  pure (Forall (match_var ve le) (map fst (f.(m_in) ++ f.(m_vars)))).

Lemma varsrep_any_empty:
  forall f ve le,
    varsrep f ve le -*> varsrep f vempty le.

Lemma varsrep_corres_out:
  forall f ve le x t v,
    In (x, t) (m_out f) ->
    varsrep f ve le -*> varsrep f (Env.add x v ve) le.

Lemma varsrep_add:
  forall f ve le x v,
    varsrep f ve le -*> varsrep f (Env.add x v ve) (PTree.set x v le).

Lemma varsrep_add':
  forall f ve le x v y v',
    ~ InMembers y (m_in f ++ m_vars f) ->
    varsrep f ve le -*> varsrep f (Env.add x v ve) (PTree.set x v (PTree.set y v' le)).

Lemma varsrep_add'':
  forall f ve le x v y v',
    ~ InMembers y (m_in f ++ m_vars f) ->
    x <> y ->
    varsrep f (Env.add x v ve) le -*> varsrep f (Env.add x v ve) (PTree.set y v' le).

Lemma varsrep_add''':
  forall f ve le x v,
    ~ InMembers x (m_in f ++ m_vars f) ->
    varsrep f ve le -*> varsrep f ve (PTree.set x v le).

Definition var_ptr (b: block) : val :=
  Vptr b Ptrofs.zero.

Section MatchStates.

  Variable ge : composite_env.

  Definition outputrep
             (c: class) (f: method) (ve: venv) (le: temp_env)
             (outb_co: option (block * composite)) : massert :=
    case_out f
             sepemp
             (fun x _ => pure (match_var ve le x))
             (fun _ => match outb_co with
                    | Some (outb, outco) =>
                      pure (le ! (prefix obc2c out) = Some (var_ptr outb))
                      ** pure (ge ! (prefix_fun f.(m_name) c.(c_name)) = Some outco)
                      ** fieldsrep ge ve outco.(co_members) outb
                    | None => sepfalse
                    end).

  Lemma outputrep_add_prefix:
    forall c f ve le outb_co f' x v,
      atom f' ->
      outputrep c f ve le outb_co <-*-> outputrep c f ve (PTree.set (prefix_temp f' x) v le) outb_co.

  Lemma outputrep_nil:
    forall c f ve le outb_co,
      f.(m_out) = [] ->
      outputrep c f ve le outb_co <-*-> sepemp.

  Lemma outputrep_singleton:
    forall c f ve le m outb_co x t P,
      f.(m_out) = [(x, t)] ->
      (m |= outputrep c f ve le outb_co ** P <->
       m |= P /\ match_var ve le x).

  Lemma outputrep_notnil:
    forall c f ve le m outb_co P,
      (1 < length f.(m_out))%nat ->
      (m |= outputrep c f ve le outb_co ** P <->
       exists outb outco,
         outb_co = Some (outb, outco)
         /\ m |= fieldsrep ge ve outco.(co_members) outb ** P
         /\ le ! (prefix obc2c out) = Some (var_ptr outb)
         /\ ge ! (prefix_fun f.(m_name) c.(c_name)) = Some outco).

  Definition prefix_out_env (e: Clight.env) : Prop :=
    forall x b t,
      e ! x = Some (b, t) ->
      exists o f, x = prefix_out o f.

  Definition bounded_struct_of_class (c: class) (sofs: ptrofs) : Prop :=
    struct_in_bounds ge 0 Ptrofs.max_unsigned (Ptrofs.unsigned sofs) (make_members c).

  Lemma bounded_struct_of_class_ge0:
    forall c sofs,
      bounded_struct_of_class c sofs ->
      0 <= Ptrofs.unsigned sofs.
  Hint Resolve bounded_struct_of_class_ge0.

  Definition selfrep (p: program) (c: class) (me: menv) (le: Clight.temp_env) (sb: block) (sofs: ptrofs) : massert :=
    pure (le ! (prefix obc2c self) = Some (Vptr sb sofs))
    ** pure (bounded_struct_of_class c sofs)
    ** staterep ge p c.(c_name) me sb (Ptrofs.unsigned sofs).

  Lemma selfrep_conj:
    forall m p c me le sb sofs P,
      m |= selfrep p c me le sb sofs ** P
      <-> m |= staterep ge p c.(c_name) me sb (Ptrofs.unsigned sofs) ** P
        /\ le ! (prefix obc2c self) = Some (Vptr sb sofs)
        /\ bounded_struct_of_class c sofs.

  Definition outputsrep (f: method) (e: Clight.env) : massert :=
    pure (prefix_out_env e)
    ** subrep ge f e
    ** (subrep ge f e -* subrep_range ge e).

  Definition match_states
             (p: program) (c: class) (f: method) '((me, ve): menv * venv)
             '((e, le): Clight.env * Clight.temp_env)
             (sb: block) (sofs: ptrofs) (outb_co: option (block * composite)): massert :=
    pure (wt_state p me ve c (meth_vars f))
    ** selfrep p c me le sb sofs
    ** outputrep c f ve le outb_co
    ** outputsrep f e
    ** varsrep f ve le.

  Lemma match_states_conj:
    forall p c f me ve e le m sb sofs outb_co P,
      m |= match_states p c f (me, ve) (e, le) sb sofs outb_co ** P <->
      m |= staterep ge p c.(c_name) me sb (Ptrofs.unsigned sofs)
           ** outputrep c f ve le outb_co
           ** subrep ge f e
           ** (subrep ge f e -* subrep_range ge e)
           ** varsrep f ve le
           ** P
      /\ bounded_struct_of_class c sofs
      /\ wt_state p me ve c (meth_vars f)
      /\ le ! (prefix obc2c self)= Some (Vptr sb sofs)
      /\ prefix_out_env e.

  Lemma match_states_wt_state:
    forall p c f me ve e le m sb sofs outb_co P,
      m |= match_states p c f (me, ve) (e, le) sb sofs outb_co ** P ->
      wt_state p me ve c (meth_vars f).

  Section MatchStatesPreservation.


    Variable
      (prog : program)

      (ownerid : ident) (owner : class) (prog' : program)

      (callerid : ident) (caller : method)

      (me : menv) (ve : venv)

      (m : Mem.mem) (e : Clight.env) (le : temp_env)

      (sb : block) (sofs : ptrofs)

      (outb_co : option (block * composite))

      (P : massert).

    Hypothesis (Findcl : find_class ownerid prog = Some (owner, prog'))
               (Findmth : find_method callerid owner.(c_methods) = Some caller)
               (OutputMatch : forall outco , (1 < length (m_out caller))%nat ->
                                        ge ! (prefix_fun callerid ownerid) = Some outco ->
                                        map translate_param caller.(m_out) = outco.(co_members)).

    Variable (v : val) (x : ident) (ty : type).

    Hypothesis (WTv : wt_val v ty).

    Lemma outputrep_assign_gt1_mem:
      In (x, ty) caller.(m_out) ->
      (1 < length (m_out caller))%nat ->
      m |= outputrep owner caller ve le outb_co ** P ->
      exists m' b co d,
        outb_co = Some (b, co)
        /\ field_offset ge x (co_members co) = Errors.OK d
        /\ Clight.assign_loc ge (cltype ty) m b (Ptrofs.repr d) v m'
        /\ m' |= outputrep owner caller (Env.add x v ve) le outb_co ** P.

    Lemma outputrep_assign_singleton_mem:
      m_out caller = [(x, ty)] ->
      outputrep owner caller ve le outb_co -*>
      outputrep owner caller (Env.add x v ve) (PTree.set x v le) outb_co.

    Lemma outputrep_assign_var_mem:
      ~ InMembers x (m_out caller) ->
      In (x, ty) (meth_vars caller) ->
      m |= outputrep owner caller ve le outb_co ** P ->
      m |= outputrep owner caller (Env.add x v ve) (PTree.set x v le) outb_co ** P.

    Lemma match_states_assign_state_mem:
      m |= match_states prog owner caller (me, ve) (e, le) sb sofs outb_co
           ** P ->
      In (x, ty) owner.(c_mems) ->
      exists m' d,
        field_offset ge x (make_members owner) = Errors.OK d
        /\ Clight.assign_loc ge (cltype ty) m sb (Ptrofs.repr (Ptrofs.unsigned sofs + d)) v m'
        /\ m' |= match_states prog owner caller (add_val x v me, ve) (e, le) sb sofs outb_co
                ** P.

  End MatchStatesPreservation.

End MatchStates.


Section FunctionEntry.




  Remark bind_parameter_temps_exists:
    forall xs s ts o to ys vs sptr optr,
      s <> o ->
      NoDupMembers xs ->
      ~ InMembers s xs ->
      ~ InMembers o xs ->
      ~ InMembers s ys ->
      ~ InMembers o ys ->
      length xs = length vs ->
      exists le',
        bind_parameter_temps ((s, ts) :: (o, to) :: xs)
                             (sptr :: optr :: vs)
                             (create_undef_temps ys) = Some le'
        /\ Forall (match_var (Env.adds (map fst xs) vs vempty) le') (map fst (xs ++ ys)).

  Remark bind_parameter_temps_exists_noout:
    forall xs s ts ys vs sptr,
      NoDupMembers xs ->
      ~ InMembers s xs ->
      ~ InMembers s ys ->
      length xs = length vs ->
      exists le',
        bind_parameter_temps ((s, ts) :: xs)
                             (sptr :: vs)
                             (create_undef_temps ys) = Some le'
        /\ Forall (match_var (Env.adds (map fst xs) vs vempty) le') (map fst (xs ++ ys)).

  Remark alloc_mem_vars:
    forall ge vars e m e' m' P,
      let gcenv := Clight.genv_cenv ge in
      m |= P ->
      NoDupMembers vars ->
      Forall (fun xt => sizeof gcenv (snd xt) <= Ptrofs.max_unsigned) vars ->
      alloc_variables ge e m vars e' m' ->
      m' |= sepall (range_inst_env gcenv e') (var_names vars) ** P.

  Lemma alloc_result:
    forall ge f m P,
      let vars := instance_methods f in
      let gcenv := Clight.genv_cenv ge in
      composite_env_consistent ge ->
      Forall (fun xt => sizeof ge (snd xt) <= Ptrofs.max_unsigned /\ wf_struct gcenv xt)
             (make_out_vars vars) ->
      NoDupMembers (make_out_vars vars) ->
      m |= P ->
      exists e' m',
        alloc_variables ge empty_env m (make_out_vars vars) e' m'
        /\ prefix_out_env e'
        /\ m' |= subrep gcenv f e'
               ** (subrep gcenv f e' -* subrep_range gcenv e')
               ** P.


  Variable (main_node : ident)
           (prog : program)
           (tprog : Clight.program)
           (do_sync : bool)
           (all_public : bool).
  Let tge := Clight.globalenv tprog.
  Let gcenv := Clight.genv_cenv tge.

  Hypothesis (TRANSL : translate do_sync all_public main_node prog = Errors.OK tprog)
             (WT : wt_program prog).

  Lemma function_entry_match_states:
    forall cid c prog' fid f fd me vs,
      method_spec c f prog fd ->
      find_class cid prog = Some (c, prog') ->
      find_method fid c.(c_methods) = Some f ->
      wt_mem me prog c ->
      Forall2 (fun v xt => wt_val v (snd xt)) vs (m_in f) ->
      case_out f
               (forall m sb sofs P,
                   bounded_struct_of_class gcenv c sofs ->
                   m |= staterep gcenv prog cid me sb (Ptrofs.unsigned sofs) ** P ->
                   exists e_f le_f m_f,
                     function_entry2 tge fd (Vptr sb sofs :: vs) m e_f le_f m_f
                     /\ m_f |= match_states gcenv prog c f (me, Env.adds (map fst f.(m_in)) vs vempty) (e_f, le_f) sb sofs None
                              ** P)
               (fun _ _ =>
                  forall m sb sofs P,
                    bounded_struct_of_class gcenv c sofs ->
                    m |= staterep gcenv prog cid me sb (Ptrofs.unsigned sofs) ** P ->
                    exists e_f le_f m_f,
                      function_entry2 tge fd (Vptr sb sofs :: vs) m e_f le_f m_f
                      /\ m_f |= match_states gcenv prog c f (me, Env.adds (map fst f.(m_in)) vs vempty) (e_f, le_f) sb sofs None
                               ** P)
               (fun _ =>
                  forall m sb sofs instb instco P,
                   bounded_struct_of_class gcenv c sofs ->
                   m |= staterep gcenv prog cid me sb (Ptrofs.unsigned sofs)
                        ** fieldsrep gcenv vempty (co_members instco) instb
                        ** P ->
                   gcenv ! (prefix_fun fid cid) = Some instco ->
                   exists e_f le_f m_f,
                     function_entry2 tge fd (Vptr sb sofs :: var_ptr instb :: vs) m e_f le_f m_f
                     /\ m_f |= match_states gcenv prog c f (me, Env.adds (map fst f.(m_in)) vs vempty) (e_f, le_f) sb sofs
                                (Some (instb, instco))
                              ** P).

End FunctionEntry.

Section MainProgram.

  Variable (main_node : ident)
           (prog : program)
           (tprog : Clight.program)
           (do_sync : bool)
           (all_public : bool).
  Let tge := Clight.globalenv tprog.
  Let gcenv := Clight.genv_cenv tge.

  Hypothesis (TRANSL : translate do_sync all_public main_node prog = Errors.OK tprog)
             (WT : wt_program prog).

  Let out_step := prefix out step.
  Let t_out_step := type_of_inst (prefix_fun step main_node).

  Let main_step := main_step _ _ _ _ _ TRANSL.
  Let main_f := main_f _ _ _ _ _ TRANSL.

  Lemma main_with_output_structure:
    forall m P,
      (1 < length (m_out main_step))%nat ->
      m |= P ->
      exists m' step_b step_co,
        alloc_variables tge empty_env m (fn_vars main_f)
                        (PTree.set out_step (step_b, t_out_step) empty_env) m'
        /\ gcenv ! (prefix_fun step main_node) = Some step_co
        /\ m' |= fieldsrep gcenv vempty step_co.(co_members) step_b ** P.

  Lemma init_mem:
    exists m sb,
      Genv.init_mem tprog = Some m
      /\ Genv.find_symbol tge (prefix_glob (prefix self main_id)) = Some sb
      /\ m |= staterep gcenv prog main_node mempty sb Z0.

End MainProgram.

Hint Resolve match_states_wt_state bounded_struct_of_class_ge0.