Library Cminor_CompcertSemantics
Require Import compcert.Coqlib.
Require Import compcert.AST.
Require Import compcert.Integers.
Require Import compcert.Values.
Require Import compcert.Memory.
Require Import compcert.Events.
Require Import compcert.Globalenvs.
Require Import compcert.Cminor.
Require Import veric.sim.
Inductive CMin_core: Type :=
| CMin_State:
forall (f: function)
(s: stmt)
(k: cont)
(sp: val)
(e: env),
CMin_core
| CMin_Callstate:
forall (f: fundef)
(args: list val)
(k: cont),
CMin_core
| CMin_Returnstate:
forall (v: val)
(k: cont),
CMin_core.
Definition ToState (q:CMin_core) (m:mem): Cminor.state :=
match q with
CMin_State f s k sp e => State f s k sp e m
| CMin_Callstate f args k => Callstate f args k m
| CMin_Returnstate v k => Returnstate v k m
end.
Definition FromState (c: Cminor.state) : CMin_core * mem :=
match c with
State f s k sp e m => (CMin_State f s k sp e, m)
| Callstate f args k m => (CMin_Callstate f args k, m)
| Returnstate v k m => (CMin_Returnstate v k, m)
end.
Definition CMin_init_mem (ge:genv) (m:mem) d: Prop:=
Genv.alloc_variables ge Mem.empty d = Some m.
Definition CMin_make_initial_core (ge:genv) (v: val) (args:list val): option CMin_core :=
match v with
Vptr b i => if Int.eq_dec i Int.zero
then
match Genv.find_funct_ptr ge b with
None => None
| Some f => match funsig f with
{| sig_args := sargs; sig_res := sres |} =>
match sargs, sres with
nil, Some Tint => Some (CMin_Callstate f nil Kstop)
| _ , _ => None
end
end
end
else None
| _ => None
end.
Definition CMin_at_external (c: CMin_core) : option (external_function * signature * list val) :=
match c with
| CMin_State f s k sp e => None
| CMin_Callstate fd args k => match fd with
Internal f => None
| External ef => Some (ef, ef_sig ef, args)
end
| CMin_Returnstate v k => None
end.
Definition CMin_after_external (vret: option val) (c: CMin_core) : option CMin_core :=
match c with
CMin_Callstate fd args k =>
match fd with
Internal f => None
| External ef => match vret with
None => Some (CMin_Returnstate Vundef k)
| Some v => Some (CMin_Returnstate v k)
end
end
| _ => None
end.
Definition CMin_corestep (ge : genv) (q : CMin_core) (m : mem) (q' : CMin_core) (m' : mem) : Prop.
destruct q; destruct q'.
apply (exists t, Cminor.step ge (State f s k sp e m) t (State f0 s0 k0 sp0 e0 m')).
apply (exists t, Cminor.step ge (State f s k sp e m) t (Callstate f0 args k0 m')).
apply (exists t, Cminor.step ge (State f s k sp e m) t (Returnstate v k0 m')).
apply (exists t, Cminor.step ge (Callstate f args k m) t (State f0 s k0 sp e m')).
apply False.
apply False.
apply (exists t, Cminor.step ge (Returnstate v k m) t (State f s k0 sp e m')).
apply False.
apply False.
Defined.
Lemma CMin_corestep_not_at_external:
forall ge m q m' q', CMin_corestep ge q m q' m' -> CMin_at_external q = None.
Proof. intros.
unfold CMin_corestep in H.
destruct q; destruct q'; simpl in *; try reflexivity.
destruct H as [t Ht]. inversion Ht; subst. reflexivity.
contradiction.
contradiction.
Qed.
Definition CMin_safely_halted (ge:genv) (q : CMin_core): option int :=
match q with
CMin_Returnstate (Vint r) Kstop => Some r
| _ => None
end.
Lemma CMin_corestep_not_halted : forall ge m q m' q',
CMin_corestep ge q m q' m' -> CMin_safely_halted ge q = None.
Proof. intros.
unfold CMin_corestep in H.
destruct q; destruct q'; simpl in *; try reflexivity.
destruct H as [t Ht]. inversion Ht; subst.
destruct v; reflexivity.
contradiction.
contradiction.
Qed.
Lemma CMin_at_external_halted_excl :
forall ge q, CMin_at_external q = None \/ CMin_safely_halted ge q = None.
Proof. intros. destruct q; auto. Qed.
Definition CMin_core_sem : CoreSemantics genv CMin_core mem (list (ident * globvar unit)).
eapply @Build_CoreSemantics with (at_external:=CMin_at_external)(corestep:=CMin_corestep)
(safely_halted:=CMin_safely_halted).
apply CMin_init_mem.
apply CMin_make_initial_core.
apply CMin_after_external.
apply CMin_corestep_not_at_external.
apply CMin_corestep_not_halted.
apply CMin_at_external_halted_excl.
Defined.
Parameter Mem_free_deterministic: forall m sp f m1 m2,
Mem.free m sp 0 (fn_stackspace f) = Some m1 ->
Mem.free m sp 0 (fn_stackspace f) = Some m2 -> m1=m2.
Parameter eval_expr_deterministic: forall ge sp e m a v1 v2,
eval_expr ge sp e m a v1 ->
eval_expr ge sp e m a v2 -> v1=v2.
Parameter Mem_storev_deterministic: forall ch m a v m1 m2,
Mem.storev ch m a v = Some m1 -> Mem.storev ch m a v = Some m2 -> m1 = m2.
Lemma Cminor_step_fun: forall ge q q1 t1 (K1: Cminor.step ge q t1 q1) q2 t2 (K2:step ge q t2 q2), q1 = q2.
Proof. intros g1 q q1 t1 K1.
induction K1; intros.
inv K2; simpl in *; try contradiction. trivial.
inv K2; simpl in *; try contradiction. trivial.
inv K2; simpl in *; try contradiction. rewrite (Mem_free_deterministic _ _ _ _ _ H1 H11). trivial.
inv K2; simpl in *; try contradiction. rewrite (eval_expr_deterministic _ _ _ _ _ _ _ H H9). trivial.
inv K2; simpl in *; try contradiction.
rewrite (eval_expr_deterministic _ _ _ _ _ _ _ H H12) in *.
rewrite (eval_expr_deterministic _ _ _ _ _ _ _ H0 H13) in *.
rewrite (Mem_storev_deterministic _ _ _ _ _ _ H1 H14) in *. trivial.
Admitted.
Lemma CMin_corestep_fun: forall ge m q m1 q1 m2 q2,
CMin_corestep ge q m q1 m1 ->
CMin_corestep ge q m q2 m2 ->
(q1, m1) = (q2, m2).
Proof.
intros.
destruct q; destruct q1; destruct q2; try inv H; try inv H0;
try assert (X:= Cminor_step_fun _ _ _ _ H1 _ _ H); inv X; trivial.
Qed.
Lemma CMin_allowed_modifications :
forall ge q m q' m',
CMin_corestep ge q m q' m' ->
allowed_core_modification m m'.
Proof. intros. assert (NotAtExt:= CMin_corestep_not_at_external _ _ _ _ _ H).
destruct q; destruct q'; inv H.
inv H0; try apply allowed_core_modification_refl.
unfold Mem.storev in H15. destruct vaddr; try inv H15. eapply store_allowed_core_mod; eauto.
simpl in NotAtExt. assert (Pr:= external_call_spec ef). inv Pr.
split; intros.
eapply external_call_mem_forward; eauto.
split; intros. admit.
split; intros. admit. admit.
inv H0; try apply allowed_core_modification_refl. eapply free_allowed_core_mod; eassumption.
inv H0; try eapply free_allowed_core_mod; eassumption.
inv H0. eapply alloc_allowed_core_mod; eassumption.
inv H0; try apply allowed_core_modification_refl.
Qed.
Definition CMin_CompcertCoreSem : CompcertCoreSem genv CMin_core (list (ident * globvar unit)).
eapply @Build_CompcertCoreSem with (csem:=CMin_core_sem).
apply CMin_corestep_fun.
apply CMin_allowed_modifications.
Defined.
Lemma CMin_corestep_2_CompCertStep: forall (ge : genv) (q : CMin_core) (m : mem) (q' : CMin_core) (m' : mem) ,
CMin_corestep ge q m q' m' ->
exists t, step ge (ToState q m) t (ToState q' m').
Proof.
intros. destruct q; destruct q'; induction H; simpl; eauto.
Qed.
Lemma CompCertStep_CMin_corestep: forall (ge : genv) (q : CMin_core) (m : mem) (q' : CMin_core) (m' : mem) t,
step ge (ToState q m) t (ToState q' m') ->
CMin_at_external q = None ->
CMin_corestep ge q m q' m'.
Proof.
intros. destruct q; destruct q'; simpl in *; try eexists; try eassumption.
inv H.
inv H. inv H0.
inv H.
inv H.
Qed.
Lemma CompCertStep_CMin_corestep': forall (ge : genv) (q : CMin_core) (m : mem) c' t,
step ge (ToState q m) t c' ->
CMin_at_external q = None ->
CMin_corestep ge q m (fst (FromState c')) (snd (FromState c')).
Proof.
intros. destruct q; destruct c'; simpl in *; try eexists; try eassumption.
inv H.
inv H. inv H0.
inv H.
inv H.
Qed.
Lemma CMin_corestepSN_2_CompCertStepStar: forall (ge : genv) n (q : CMin_core) (m : mem) (q' : CMin_core) (m' : mem),
corestepN CMin_CompcertCoreSem ge n q m q' m' ->
exists t, Smallstep.star step ge (ToState q m) t (ToState q' m').
Proof.
intros ge n.
induction n; simpl; intros.
inv H. eexists. apply Smallstep.star_refl.
destruct H as [c2 [m2 [Step1 Steps]]].
destruct (IHn _ _ _ _ Steps) as [t Ht].
destruct (CMin_corestep_2_CompCertStep _ _ _ _ _ Step1) as [t1 Ht1].
eexists. econstructor. eassumption. eassumption.
reflexivity.
Qed.
Lemma CMin_corestepSN_2_CompCertStepPlus: forall (ge : genv) n (q : CMin_core) (m : mem) (q' : CMin_core) (m' : mem),
corestepN CMin_CompcertCoreSem ge (S n) q m q' m' ->
exists t, Smallstep.plus step ge (ToState q m) t (ToState q' m').
Proof.
intros.
destruct H as [c2 [m2 [H X]]].
destruct (CMin_corestep_2_CompCertStep _ _ _ _ _ H) as [t1 Ht1]. clear H.
destruct (CMin_corestepSN_2_CompCertStepStar _ _ _ _ _ _ X) as [t2 Ht2]. clear X.
eexists. econstructor. eassumption. eassumption. reflexivity.
Qed.
Lemma CMin_corestep_plus_2_CompCertStep_plus: forall (ge : genv) (q : CMin_core) (m : mem) (q' : CMin_core) (m' : mem) ,
corestep_plus CMin_CompcertCoreSem ge q m q' m' ->
exists t, Smallstep.plus step ge (ToState q m) t (ToState q' m').
Proof.
intros. destruct H as [n Hn].
eapply CMin_corestepSN_2_CompCertStepPlus. apply Hn.
Qed.
Lemma CMin_corestep_star_2_CompCertStep_star: forall (ge : genv) (q : CMin_core) (m : mem) (q' : CMin_core) (m' : mem) ,
corestep_star CMin_CompcertCoreSem ge q m q' m' ->
exists t, Smallstep.star step ge (ToState q m) t (ToState q' m').
Proof.
intros. destruct H as [n Hn].
eapply CMin_corestepSN_2_CompCertStepStar. apply Hn.
Qed.
Lemma CompCertStep_2_CMin_corestep: forall (ge : genv) (q : CMin_core) (m : mem) t c',
step ge (ToState q m) t c' ->
CMin_at_external q = None ->
exists q', exists m', c' = ToState q' m' /\ CMin_corestep ge q m q' m'.
Proof.
intros. destruct q; destruct c'; simpl in *.
exists (CMin_State f0 s0 k0 sp0 e0). exists m0; simpl. split. trivial. eexists. eassumption.
exists (CMin_Callstate f0 args k0). exists m0; simpl. split. trivial. eexists. eassumption.
exists (CMin_Returnstate v k0). exists m0; simpl. split. trivial. eexists. eassumption.
exists (CMin_State f0 s k0 sp e). exists m0; simpl. split. trivial. eexists. eassumption.
inv H.
inv H. inv H0.
exists (CMin_State f s k0 sp e). exists m0; simpl. split. trivial. eexists. eassumption.
inv H.
inv H.
Qed.
Lemma CMin_core2state_injective: forall q m q' m',
ToState q m = ToState q' m' -> q'=q /\ m'=m.
Proof. intros.
destruct q; destruct q'; simpl in *; inv H; split; trivial.
Qed.
Require Import compcert.AST.
Require Import compcert.Integers.
Require Import compcert.Values.
Require Import compcert.Memory.
Require Import compcert.Events.
Require Import compcert.Globalenvs.
Require Import compcert.Cminor.
Require Import veric.sim.
Inductive CMin_core: Type :=
| CMin_State:
forall (f: function)
(s: stmt)
(k: cont)
(sp: val)
(e: env),
CMin_core
| CMin_Callstate:
forall (f: fundef)
(args: list val)
(k: cont),
CMin_core
| CMin_Returnstate:
forall (v: val)
(k: cont),
CMin_core.
Definition ToState (q:CMin_core) (m:mem): Cminor.state :=
match q with
CMin_State f s k sp e => State f s k sp e m
| CMin_Callstate f args k => Callstate f args k m
| CMin_Returnstate v k => Returnstate v k m
end.
Definition FromState (c: Cminor.state) : CMin_core * mem :=
match c with
State f s k sp e m => (CMin_State f s k sp e, m)
| Callstate f args k m => (CMin_Callstate f args k, m)
| Returnstate v k m => (CMin_Returnstate v k, m)
end.
Definition CMin_init_mem (ge:genv) (m:mem) d: Prop:=
Genv.alloc_variables ge Mem.empty d = Some m.
Definition CMin_make_initial_core (ge:genv) (v: val) (args:list val): option CMin_core :=
match v with
Vptr b i => if Int.eq_dec i Int.zero
then
match Genv.find_funct_ptr ge b with
None => None
| Some f => match funsig f with
{| sig_args := sargs; sig_res := sres |} =>
match sargs, sres with
nil, Some Tint => Some (CMin_Callstate f nil Kstop)
| _ , _ => None
end
end
end
else None
| _ => None
end.
Definition CMin_at_external (c: CMin_core) : option (external_function * signature * list val) :=
match c with
| CMin_State f s k sp e => None
| CMin_Callstate fd args k => match fd with
Internal f => None
| External ef => Some (ef, ef_sig ef, args)
end
| CMin_Returnstate v k => None
end.
Definition CMin_after_external (vret: option val) (c: CMin_core) : option CMin_core :=
match c with
CMin_Callstate fd args k =>
match fd with
Internal f => None
| External ef => match vret with
None => Some (CMin_Returnstate Vundef k)
| Some v => Some (CMin_Returnstate v k)
end
end
| _ => None
end.
Definition CMin_corestep (ge : genv) (q : CMin_core) (m : mem) (q' : CMin_core) (m' : mem) : Prop.
destruct q; destruct q'.
apply (exists t, Cminor.step ge (State f s k sp e m) t (State f0 s0 k0 sp0 e0 m')).
apply (exists t, Cminor.step ge (State f s k sp e m) t (Callstate f0 args k0 m')).
apply (exists t, Cminor.step ge (State f s k sp e m) t (Returnstate v k0 m')).
apply (exists t, Cminor.step ge (Callstate f args k m) t (State f0 s k0 sp e m')).
apply False.
apply False.
apply (exists t, Cminor.step ge (Returnstate v k m) t (State f s k0 sp e m')).
apply False.
apply False.
Defined.
Lemma CMin_corestep_not_at_external:
forall ge m q m' q', CMin_corestep ge q m q' m' -> CMin_at_external q = None.
Proof. intros.
unfold CMin_corestep in H.
destruct q; destruct q'; simpl in *; try reflexivity.
destruct H as [t Ht]. inversion Ht; subst. reflexivity.
contradiction.
contradiction.
Qed.
Definition CMin_safely_halted (ge:genv) (q : CMin_core): option int :=
match q with
CMin_Returnstate (Vint r) Kstop => Some r
| _ => None
end.
Lemma CMin_corestep_not_halted : forall ge m q m' q',
CMin_corestep ge q m q' m' -> CMin_safely_halted ge q = None.
Proof. intros.
unfold CMin_corestep in H.
destruct q; destruct q'; simpl in *; try reflexivity.
destruct H as [t Ht]. inversion Ht; subst.
destruct v; reflexivity.
contradiction.
contradiction.
Qed.
Lemma CMin_at_external_halted_excl :
forall ge q, CMin_at_external q = None \/ CMin_safely_halted ge q = None.
Proof. intros. destruct q; auto. Qed.
Definition CMin_core_sem : CoreSemantics genv CMin_core mem (list (ident * globvar unit)).
eapply @Build_CoreSemantics with (at_external:=CMin_at_external)(corestep:=CMin_corestep)
(safely_halted:=CMin_safely_halted).
apply CMin_init_mem.
apply CMin_make_initial_core.
apply CMin_after_external.
apply CMin_corestep_not_at_external.
apply CMin_corestep_not_halted.
apply CMin_at_external_halted_excl.
Defined.
Parameter Mem_free_deterministic: forall m sp f m1 m2,
Mem.free m sp 0 (fn_stackspace f) = Some m1 ->
Mem.free m sp 0 (fn_stackspace f) = Some m2 -> m1=m2.
Parameter eval_expr_deterministic: forall ge sp e m a v1 v2,
eval_expr ge sp e m a v1 ->
eval_expr ge sp e m a v2 -> v1=v2.
Parameter Mem_storev_deterministic: forall ch m a v m1 m2,
Mem.storev ch m a v = Some m1 -> Mem.storev ch m a v = Some m2 -> m1 = m2.
Lemma Cminor_step_fun: forall ge q q1 t1 (K1: Cminor.step ge q t1 q1) q2 t2 (K2:step ge q t2 q2), q1 = q2.
Proof. intros g1 q q1 t1 K1.
induction K1; intros.
inv K2; simpl in *; try contradiction. trivial.
inv K2; simpl in *; try contradiction. trivial.
inv K2; simpl in *; try contradiction. rewrite (Mem_free_deterministic _ _ _ _ _ H1 H11). trivial.
inv K2; simpl in *; try contradiction. rewrite (eval_expr_deterministic _ _ _ _ _ _ _ H H9). trivial.
inv K2; simpl in *; try contradiction.
rewrite (eval_expr_deterministic _ _ _ _ _ _ _ H H12) in *.
rewrite (eval_expr_deterministic _ _ _ _ _ _ _ H0 H13) in *.
rewrite (Mem_storev_deterministic _ _ _ _ _ _ H1 H14) in *. trivial.
Admitted.
Lemma CMin_corestep_fun: forall ge m q m1 q1 m2 q2,
CMin_corestep ge q m q1 m1 ->
CMin_corestep ge q m q2 m2 ->
(q1, m1) = (q2, m2).
Proof.
intros.
destruct q; destruct q1; destruct q2; try inv H; try inv H0;
try assert (X:= Cminor_step_fun _ _ _ _ H1 _ _ H); inv X; trivial.
Qed.
Lemma CMin_allowed_modifications :
forall ge q m q' m',
CMin_corestep ge q m q' m' ->
allowed_core_modification m m'.
Proof. intros. assert (NotAtExt:= CMin_corestep_not_at_external _ _ _ _ _ H).
destruct q; destruct q'; inv H.
inv H0; try apply allowed_core_modification_refl.
unfold Mem.storev in H15. destruct vaddr; try inv H15. eapply store_allowed_core_mod; eauto.
simpl in NotAtExt. assert (Pr:= external_call_spec ef). inv Pr.
split; intros.
eapply external_call_mem_forward; eauto.
split; intros. admit.
split; intros. admit. admit.
inv H0; try apply allowed_core_modification_refl. eapply free_allowed_core_mod; eassumption.
inv H0; try eapply free_allowed_core_mod; eassumption.
inv H0. eapply alloc_allowed_core_mod; eassumption.
inv H0; try apply allowed_core_modification_refl.
Qed.
Definition CMin_CompcertCoreSem : CompcertCoreSem genv CMin_core (list (ident * globvar unit)).
eapply @Build_CompcertCoreSem with (csem:=CMin_core_sem).
apply CMin_corestep_fun.
apply CMin_allowed_modifications.
Defined.
Lemma CMin_corestep_2_CompCertStep: forall (ge : genv) (q : CMin_core) (m : mem) (q' : CMin_core) (m' : mem) ,
CMin_corestep ge q m q' m' ->
exists t, step ge (ToState q m) t (ToState q' m').
Proof.
intros. destruct q; destruct q'; induction H; simpl; eauto.
Qed.
Lemma CompCertStep_CMin_corestep: forall (ge : genv) (q : CMin_core) (m : mem) (q' : CMin_core) (m' : mem) t,
step ge (ToState q m) t (ToState q' m') ->
CMin_at_external q = None ->
CMin_corestep ge q m q' m'.
Proof.
intros. destruct q; destruct q'; simpl in *; try eexists; try eassumption.
inv H.
inv H. inv H0.
inv H.
inv H.
Qed.
Lemma CompCertStep_CMin_corestep': forall (ge : genv) (q : CMin_core) (m : mem) c' t,
step ge (ToState q m) t c' ->
CMin_at_external q = None ->
CMin_corestep ge q m (fst (FromState c')) (snd (FromState c')).
Proof.
intros. destruct q; destruct c'; simpl in *; try eexists; try eassumption.
inv H.
inv H. inv H0.
inv H.
inv H.
Qed.
Lemma CMin_corestepSN_2_CompCertStepStar: forall (ge : genv) n (q : CMin_core) (m : mem) (q' : CMin_core) (m' : mem),
corestepN CMin_CompcertCoreSem ge n q m q' m' ->
exists t, Smallstep.star step ge (ToState q m) t (ToState q' m').
Proof.
intros ge n.
induction n; simpl; intros.
inv H. eexists. apply Smallstep.star_refl.
destruct H as [c2 [m2 [Step1 Steps]]].
destruct (IHn _ _ _ _ Steps) as [t Ht].
destruct (CMin_corestep_2_CompCertStep _ _ _ _ _ Step1) as [t1 Ht1].
eexists. econstructor. eassumption. eassumption.
reflexivity.
Qed.
Lemma CMin_corestepSN_2_CompCertStepPlus: forall (ge : genv) n (q : CMin_core) (m : mem) (q' : CMin_core) (m' : mem),
corestepN CMin_CompcertCoreSem ge (S n) q m q' m' ->
exists t, Smallstep.plus step ge (ToState q m) t (ToState q' m').
Proof.
intros.
destruct H as [c2 [m2 [H X]]].
destruct (CMin_corestep_2_CompCertStep _ _ _ _ _ H) as [t1 Ht1]. clear H.
destruct (CMin_corestepSN_2_CompCertStepStar _ _ _ _ _ _ X) as [t2 Ht2]. clear X.
eexists. econstructor. eassumption. eassumption. reflexivity.
Qed.
Lemma CMin_corestep_plus_2_CompCertStep_plus: forall (ge : genv) (q : CMin_core) (m : mem) (q' : CMin_core) (m' : mem) ,
corestep_plus CMin_CompcertCoreSem ge q m q' m' ->
exists t, Smallstep.plus step ge (ToState q m) t (ToState q' m').
Proof.
intros. destruct H as [n Hn].
eapply CMin_corestepSN_2_CompCertStepPlus. apply Hn.
Qed.
Lemma CMin_corestep_star_2_CompCertStep_star: forall (ge : genv) (q : CMin_core) (m : mem) (q' : CMin_core) (m' : mem) ,
corestep_star CMin_CompcertCoreSem ge q m q' m' ->
exists t, Smallstep.star step ge (ToState q m) t (ToState q' m').
Proof.
intros. destruct H as [n Hn].
eapply CMin_corestepSN_2_CompCertStepStar. apply Hn.
Qed.
Lemma CompCertStep_2_CMin_corestep: forall (ge : genv) (q : CMin_core) (m : mem) t c',
step ge (ToState q m) t c' ->
CMin_at_external q = None ->
exists q', exists m', c' = ToState q' m' /\ CMin_corestep ge q m q' m'.
Proof.
intros. destruct q; destruct c'; simpl in *.
exists (CMin_State f0 s0 k0 sp0 e0). exists m0; simpl. split. trivial. eexists. eassumption.
exists (CMin_Callstate f0 args k0). exists m0; simpl. split. trivial. eexists. eassumption.
exists (CMin_Returnstate v k0). exists m0; simpl. split. trivial. eexists. eassumption.
exists (CMin_State f0 s k0 sp e). exists m0; simpl. split. trivial. eexists. eassumption.
inv H.
inv H. inv H0.
exists (CMin_State f s k0 sp e). exists m0; simpl. split. trivial. eexists. eassumption.
inv H.
inv H.
Qed.
Lemma CMin_core2state_injective: forall q m q' m',
ToState q m = ToState q' m' -> q'=q /\ m'=m.
Proof. intros.
destruct q; destruct q'; simpl in *; inv H; split; trivial.
Qed.