Proof.
Proof.
Proof.
Proof.
Proof.
Proof.
Proof.
Proof.
Proof.
Proof.
Proof.
Proof.
Proof.
Proof.
Proof.
Proof.
Proof.
Proof.
Proof.
Proof.
Proof.
Proof.
Proof.
Proof.
unfold seq_correct.
intros.
unfold id_trans_asm in H.
monadInv H.
split;
auto.
eapply localize;
simpl.
exact asm_localize.
exact asm_lift.
intros.
destruct H.
eapply nodup_gd_init_genv_ident_exists;
eauto.
inv H0.
auto.
intros.
destruct H.
eapply nodup_gd_init_genv_ident_exists;
eauto.
inv H0.
auto.
split;
auto.
split;
auto.
intros ? ? ? ? ? ? ? ;
simpl in *.
inv H;
inv H0.
inv H3;
inv H2.
simpl in *.
subst.
rename bound0 into bound.
remember (
Genv.globalenv (
mkprogram (
cu_defs tu) (
cu_public tu) 1%
positive))
as ge0 eqn:
G0.
assert (
GEBOUND0 =
GEBOUND)
by apply Axioms.proof_irr.
subst GEBOUND0.
remember (
ge_extend ge0 bound GEBOUND)
as ge eqn:
G.
eapply (
Local_ldsim _ _ _ _ nat lt).
instantiate(1:=
MS ge).
econstructor;
eauto;
simpl;
try (
intros;
invMS;
destruct AGMU;
auto;
fail).
apply lt_wf.
constructor;
try tauto.
intros.
rewrite H in H0.
inversion H0.
subst b'.
simpl.
destruct (
Maps.PTree.get b (
Genv.genv_defs ge));
try constructor.
destruct g;
try constructor.
destruct v;
try constructor.
init*) {
intros.
unfold init_core,
fundef_init in *.
destruct (
Genv.find_symbol ge id);
try discriminate.
destruct (
Genv.find_funct_ptr ge b);
try discriminate.
destruct f;
try discriminate.
destruct (
wd_args argSrc (
sig_args (
fn_sig f)))
eqn:
WDARG;
try discriminate.
erewrite wd_args_inject;
eauto.
inversion H3.
clear H3.
subst score.
eexists.
split.
eauto.
intros sm tm INITSM INITTM MEMREL sm'
tm'
HLRELY.
exists 0%
nat.
assert (
argSrc =
argTgt).
{
revert argTgt MEMREL H1 H2.
clear.
induction argSrc;
intros;
inv H1;
inv H2;
auto.
f_equal;
auto.
inv H1;
auto;
try contradiction.
unfold Bset.inj_to_meminj in H.
destruct (
inj mu b1)
eqn:
INJ;
try discriminate.
inv H.
exploit inj_inject_id;
eauto.
unfold Bset.inj_to_meminj.
rewrite INJ.
eauto.
intro A;
inv A.
rewrite Ptrofs.add_zero.
auto. }
subst argTgt.
rename argSrc into args.
{
destruct HLRELY as [
HRELY LRELY INV].
constructor.
constructor;
auto.
assert (
Mem.extends sm tm).
{
generalize MEMREL H.
clear;
intros ?
GE_INIT_INJ.
destruct MEMREL.
eapply inject_implies_extends;
eauto.
intros.
unfold Mem.valid_block in H;
rewrite <-
dom_eq_src in H.
eapply Bset.inj_dom in H;
eauto.
destruct H as [
b'
A].
unfold Bset.inj_to_meminj.
rewrite A.
eauto.
inv GE_INIT_INJ.
rewrite mu_shared_src in dom_eq_src.
rewrite mu_shared_tgt in dom_eq_tgt.
assert (
forall b,
Plt b (
Mem.nextblock sm) <->
Plt b (
Mem.nextblock tm)).
{
intro.
rewrite <-
dom_eq_src, <-
dom_eq_tgt.
tauto. }
destruct (
Pos.lt_total (
Mem.nextblock sm) (
Mem.nextblock tm))
as [
LT | [
EQ |
LT]];
auto;
generalize H LT;
clear;
intros;
exfalso;
apply H in LT;
eapply Pos.lt_irrefl;
eauto. }
eapply extends_rely_extends;
eauto.
inv MEMREL;
eauto.
constructor;
auto.
Esimpl.
eresolvfp.
4:
apply MemClosures_local.reach_closed_unmapped_closed;
inv LRELY;
auto.
{
intros.
unfold Mem.valid_block.
destruct INITSM,
HRELY.
rewrite EQNEXT,<-
dom_match.
inv H.
simpl in *.
rewrite mu_shared_src in H3.
auto.
}
{
intros;
unfold Mem.valid_block;
destruct INITTM,
LRELY.
rewrite EQNEXT,<-
dom_match.
inv H;
simpl in *.
rewrite mu_shared_tgt in H3;
auto.
}
inversion H;
inversion MEMREL.
constructor;
auto.
unfold sep_inject.
intros.
unfold Bset.inj_to_meminj in *.
destruct (
Injections.inj mu b0)
eqn:?; [|
inv H3].
eapply Bset.inj_range'
in Heqo;[|
inv mu_inject;
eauto].
inv H3.
inv H4.
rewrite mu_shared_tgt, <-
mu_shared_src in Heqo.
eapply Bset.inj_dom in Heqo;
eauto.
destruct Heqo.
rewrite H3.
exploit inj_inject_id.
rewrite H3.
eauto.
intro C.
inv C;
auto.
}
}
step *) {
intros until Hm'.
right.
exists 0%
nat.
clear G0 G.
pose proof H0 as STEP0.
inv H0.
exec instr *) {
invMS;
intros;
simpl in *.
inversion MC.
subst rs0 lf0 Hm Lm Lcore.
eapply exec_instr_match in H4 as STEP;
eauto.
Hsimpl;
Esimpl;
eauto.
constructor.
econstructor;
eauto.
solv_rs.
eresolvfp.
unfold MS;
Esimpl;
eauto.
econstructor;
eauto;
eresolvfp.
eresolvfp.
eapply exec_instr_valid_block;
eauto.
eapply exec_instr_valid_block2;
eauto.
{
unfold exec_instr in *.
ex_match;
repeat solv_eq.
all:
unfold exec_load,
exec_store,
Mem.storev,
goto_label in *;
repeat ex_match;
repeat solv_eq;
try (
resvalid;
auto;
fail).
all :
try (
eapply eval_addrmode_lessdef with(
ge:=
ge)(
a:=
a)
in H5;
inv H5;
repeat solv_eq;
resvalid;
fail).
{
assert(
b1 =
b0).
Local Transparent Mem.alloc.
inv H9.
unfold Mem.alloc in *.
try congruence.
subst.
solv_eq.
solv_eq.
assert(
unmapped_closed mu m3 m0).
resvalid.
assert(
forall b :
block,
Bset.belongsto (
SharedSrc mu)
b ->
Mem.valid_block m3 b).
resvalid.
assert(
forall b :
block,
Bset.belongsto (
SharedTgt mu)
b ->
Mem.valid_block m0 b).
resvalid.
assert(
unmapped_closed mu m4 m1).
resvalid.
assert(
forall b :
block,
Bset.belongsto (
SharedSrc mu)
b ->
Mem.valid_block m4 b).
resvalid.
assert(
forall b :
block,
Bset.belongsto (
SharedTgt mu)
b ->
Mem.valid_block m1 b).
resvalid.
resvalid.
}
{
solv_rs.
resvalid.
}
}
}
{
invMS;
intros;
simpl in *.
inversion MC.
subst rs0 lf0 Hm'
Lm Lcore.
exploit (@
eval_builtin_args_lessdef _ ge (
fun r =>
rs#
r) (
fun r =>
rs'#
r));
eauto.
intros (
vargs' &
P &
Q).
exploit (
MemOpFP.eval_builtin_args_fp_lessdef _ ge (
fun r =>
rs#
r) (
fun r =>
rs'#
r));
eauto.
intros EVALFP.
exploit external_call_mem_extends;
eauto.
intros [
v' [
m'1 [
A [
B [
C D]]]]].
pose proof A as A'.
apply helpers.i64ext_effects in A'.
destruct A';
subst m'1 .
assert(
rs'
RSP =
rs RSP).
assert(
Val.lessdef (
rs RSP)(
rs'
RSP)).
solv_regset;
auto.
inv H;
auto.
rewrite H11 in *.
contradiction.
Esimpl;
auto.
constructor;
auto.
econstructor 2;
eauto.
solv_rs;
auto.
intro.
solv_rs.
rewrite H;
eauto.
rewrite H;
eauto.
eresolvfp.
unfold MS.
Esimpl;
eauto;
try resolvfp.
constructor;
eauto.
subst.
unfold nextinstr_nf.
solv_regset.
auto.
}
{
invMS;
intros;
simpl in *.
inv MC.
eapply extcall_arguments_match in H3 as ?;
eauto.
Hsimpl.
Esimpl;
eauto.
constructor.
econstructor 3;
eauto.
solv_rs.
eresolvfp.
unfold MS.
Esimpl;
eauto;
try eresolvfp;
try resvalid.
econstructor 3;
eauto.
}
{
invMS;
intros;
simpl in *.
inversion MC;
Hsimpl.
subst Lcore ef0 args0 rs0 lf0 Hm'
Lm.
eapply external_call_mem_extends in H4;
eauto.
Hsimpl.
apply helpers.i64ext_effects in H as ?;
Hsimpl;
subst.
Esimpl;
eauto.
constructor.
econstructor;
eauto.
solv_rs.
eapply helpers.i64ext_extcall_forall in H;
eauto.
eresolvfp.
unfold MS.
Esimpl;
eauto;
try eresolvfp;
try resvalid.
econstructor;
eauto.
solv_regset.
unfold set_pair.
ex_match;
solv_regset.
auto.
}
{
invMS.
intros.
inversion MC.
subst fb0 args tys0 retty0 Hm Lm Lcore.
eapply Mem.alloc_extends with(
lo2:=0)(
hi2:=(4*
z))
in H2 as ?;
eauto;
try omega.
Hsimpl.
assert((
MemOpFP.alloc_fp m 0 (4*
z))=(
MemOpFP.alloc_fp m' 0 (4*
z))).
revert H0;
clear.
intros.
unfold MemOpFP.alloc_fp,
FMemOpFP.uncheck_alloc_fp.
inv H0.
rewrite mext_next.
auto.
eapply store_args_mem_extends in H4 as ?;
eauto.
Hsimpl.
Esimpl;
eauto.
constructor.
econstructor;
eauto.
eresolvfp.
rewrite H5.
eresolvfp.
unfold MS.
rewrite H5.
assert(
forall b,
Bset.belongsto(
SharedSrc mu)
b ->
Mem.valid_block m1 b).
resvalid.
assert(
forall b,
Bset.belongsto(
SharedTgt mu)
b ->
Mem.valid_block x b).
resvalid.
Esimpl;
eauto;
try eresolvfp;
try resvalid.
constructor;
auto.
subst rs0.
solv_regset.
constructor.
intros.
apply H8 in H10;
eapply store_args_validity_preserve;
eauto.
intros.
apply H9 in H10.
eapply store_args_validity_preserve;
eauto.
assert(
unmapped_closed mu m1 x).
clear H8 H9.
resvalid.
revert H4 H6 H8 H9 H10 AGMU.
clear.
unfold store_args.
generalize 0.
revert Hm'
x0 m1 x tys.
induction args0.
intros.
simpl in *.
ex_match.
intros.
simpl in *.
ex_match.
all:
unfold store_stack,
Mach.store_stack,
Mem.storev in *;
ex_match.
all:
try(
assert(
unmapped_closed mu m0 m);[
resvalid|];
assert(
forall b,
Bset.belongsto (
SharedSrc mu)
b ->
Mem.valid_block m0 b);[
resvalid|];
assert(
forall b,
Bset.belongsto (
SharedTgt mu)
b ->
Mem.valid_block m b);[
resvalid|];
try (
eapply IHargs0 in H6;
eauto;
fail)).
assert(
unmapped_closed mu m2 m);[
resvalid|];
assert(
forall b,
Bset.belongsto (
SharedSrc mu)
b ->
Mem.valid_block m2 b);[
resvalid|];
assert(
forall b,
Bset.belongsto (
SharedTgt mu)
b ->
Mem.valid_block m b);[
resvalid|].
assert(
unmapped_closed mu m3 m0);[
resvalid|];
assert(
forall b,
Bset.belongsto (
SharedSrc mu)
b ->
Mem.valid_block m3 b);[
resvalid|];
assert(
forall b,
Bset.belongsto (
SharedTgt mu)
b ->
Mem.valid_block m0 b);[
resvalid|].
eapply IHargs0 in H6;
eauto.
}
{
invMS.
inv MC.
Esimpl;eauto.
constructor.
eapply exec_step_to_lock;eauto.
solv_rs.
eresolvfp.
unfold MS;Esimpl;eauto;try eresolvfp;try resvalid.
constructor;auto.
}
{
invMS.
inv MC.
assert(exists rs'' Lm',exec_locked_instr ge i0 rs'0 Lm = Next rs'' Lm' /\
FP.subset (exec_locked_instr_fp ge i0 rs'0 Lm) (exec_locked_instr_fp ge i0 rs Hm) /\ Mem.extends Hm' Lm' /\ match_regset rs' rs'').
{
unfold exec_locked_instr,exec_locked_instr_fp in *|-.
ex_match;try (solv_eq;fail).
eapply exec_load_fp_match in H4 as ?;eauto;eapply exec_load_match in H4 as ?;eauto;Hsimpl;Esimpl;eauto.
eapply Mem.loadv_extends in Hx0 as ?;eauto.
eapply Mem.storev_extends in Hx1 as ?;eauto.
Hsimpl.
eapply eval_addrmode_lessdef in H10 as ?.
inv H8. rewrite H12 in H,H0.
Esimpl;eauto.
unfold exec_locked_instr.
rewrite H,H0. eauto.
unfold exec_locked_instr_fp.
rewrite H12. apply FP.subset_refl. inv H4. auto.
inv H4. solv_regset.
rewrite <- H11 in H. inv H.
eapply Mem.storev_extends in Hx3 as ?;eauto;Hsimpl.
eapply eval_addrmode_lessdef in H10 as ?.
inv H6. rewrite H9 in H.
eapply Mem.loadv_extends in Hx0 as ?;eauto;Hsimpl.
unfold exec_locked_instr.
rewrite H,<-H9,H6.
assert(Val.cmpu_bool (Mem.valid_pointer Lm) Ceq x0 (rs'0 RAX) = Some true).
{
revert Hx1 H5 H10 H7.
clear.
intros.
assert(rs RAX <> Vundef).
intro. rewrite H in Hx1.
compute in Hx1. ex_match.
assert(Val.lessdef (rs RAX)(rs'0 RAX)).
solv_regset;auto.
inv H0;try congruence.
inv H7;[|inv Hx1].
unfold Val.cmpu_bool in *.
ex_match;try solv_rs;try solv_eq.
{
revert Hx4 Hx5 H5;clear;intros.
destruct (Mem.valid_pointer Hm b0 (Ptrofs.unsigned i)|| Mem.valid_pointer Hm b0 (Ptrofs.unsigned i - 1)) eqn:?;try discriminate.
simpl in Hx4.
pose Mem.valid_pointer_extends.
assert(forall m m' b i j,
Mem.valid_pointer m b i || Mem.valid_pointer m b j = true->
(forall b i ,Mem.valid_pointer m b i = true -> Mem.valid_pointer m' b i = true) ->
Mem.valid_pointer m' b i||Mem.valid_pointer m' b j = true).
clear.
intros.
destruct Mem.valid_pointer eqn:?;simpl in *;eauto with bool.
assert(forall b i,Mem.valid_pointer Hm b i = true->Mem.valid_pointer Lm b i = true).
intros;eauto.
eapply H in Heqb;eauto.
eapply H in Hx4;eauto. rewrite Heqb,Hx4 in Hx5. inv Hx5.
}
}
rewrite H8.
inv H4.
Esimpl;eauto;try resvalid;try solv_regset.
unfold exec_locked_instr_fp.
rewrite H9 in *.
repeat match goal with H: ?P = _|- context[match ?P with _ => _ end] => rewrite H end.
do 2 (eapply FP.subset_parallel_union;try apply FP.subset_refl).
{
revert Hx1 H5 H10 H7.
revert H8.
clear.
intros.
assert(rs RAX <> Vundef).
intro. rewrite H in Hx1.
compute in Hx1. ex_match.
assert(Val.lessdef (rs RAX)(rs'0 RAX)).
solv_regset;auto.
inv H0;try congruence.
inv H7;[|inv Hx1].
unfold Val.cmpu_bool,ValFP.cmpu_bool_fp_total in *.
ex_match;try solv_rs;try solv_eq.
apply FP.subset_refl.
assert(forall b i m m',
Mem.extends m m'->
FP.subset (MemOpFP.weak_valid_pointer_fp m' b i)(MemOpFP.weak_valid_pointer_fp m b i)).
clear.
intros.
unfold MemOpFP.weak_valid_pointer_fp.
ex_match;try apply FP.subset_refl.
unfold FMemOpFP.valid_pointer_fp.
constructor;try apply range_locset_expend1_subset;try apply Locs.subset_refl.
eapply Mem.valid_pointer_extends in H;eauto;congruence.
eapply FP.subset_parallel_union;eauto.
}
solv_eq.
rewrite <- H8 in *. simpl in H. congruence.
eapply Mem.loadv_extends in Hx0 as ?;eauto.
Hsimpl.
eapply eval_addrmode_lessdef in H10 as ?.
inv H6.
unfold exec_locked_instr,exec_locked_instr_fp.
rewrite H9 in *. rewrite H,Hx0.
assert(Val.cmpu_bool (Mem.valid_pointer Lm) Ceq x (rs'0 RAX) = Some false).
eapply cmpu_bool_some_eq;eauto.
rewrite H6,Hx1.
inv H4.
Esimpl;eauto;try resvalid;try solv_regset.
eapply FP.subset_parallel_union;eauto;try apply FP.subset_refl.
{
revert Hx1 H5 H10 H0.
revert H6.
clear.
intros.
assert(rs RAX <> Vundef).
intro. rewrite H in Hx1.
compute in Hx1. ex_match.
assert(Val.lessdef (rs RAX)(rs'0 RAX)).
solv_regset;auto.
inv H1;try congruence.
inv H0;[|inv Hx1].
unfold Val.cmpu_bool,ValFP.cmpu_bool_fp_total in *.
assert(forall b i m m',
Mem.extends m m'->
FP.subset (MemOpFP.weak_valid_pointer_fp m' b i)(MemOpFP.weak_valid_pointer_fp m b i)).
clear.
intros.
unfold MemOpFP.weak_valid_pointer_fp.
ex_match;try apply FP.subset_refl.
unfold FMemOpFP.valid_pointer_fp.
constructor;try apply range_locset_expend1_subset;try apply Locs.subset_refl.
eapply Mem.valid_pointer_extends in H;eauto;congruence.
ex_match;try solv_rs;try solv_eq;try apply FP.subset_refl.
eapply FP.subset_parallel_union;eauto.
}
rewrite <- H8 in H. inv H.
}
Hsimpl.
Esimpl;eauto.
constructor.
eapply exec_step_locked;eauto.
solv_rs.
resolvfp.
unfold MS.
Esimpl;eauto;try eresolvfp;try resvalid.
econstructor;eauto.
eapply exec_locked_instr_valid_block;eauto.
eapply exec_locked_instr_valid_block2;eauto.
{
unfold exec_locked_instr in *.
destruct i0 eqn:?;simpl in *;try congruence.
unfold exec_load in *;repeat ex_match;repeat solv_eq;try (resvalid;auto;fail).
{
ex_match.
inv H. inv H4.
unfold Mem.storev in *.
ex_match.
eapply eval_addrmode_lessdef in H10;eauto.
inv H10. rewrite<- H8 in Hx3. rewrite Hx3 in Hx4;inv Hx4.
resvalid.
rewrite <- H4 in Hx4. inv Hx4.
}
{
ex_match.
solv_eq.
unfold Mem.storev in *;ex_match.
eapply eval_addrmode_lessdef in H10;eauto.
inv H10. rewrite<- H9 in Hx1. rewrite Hx1 in Hx5;inv Hx5.
resvalid. solv_eq. inv H4. resvalid.
rewrite <- H8 in Hx5. inv Hx5.
pose proof cmpu_bool_some_eq.
exfalso.
eapply cmpu_bool_some_eq in Hx4 as ?.
rewrite Hx0 in H9.
congruence.
auto. auto.
revert H5 Hx3 Hx H10;clear;intros.
unfold Mem.loadv in *.
ex_match.
eapply eval_addrmode_lessdef in H10 as ?.
inv H. rewrite H2,Hx0 in Hx1. inv Hx1.
eapply Mem.load_extends in H5;eauto.
Hsimpl. solv_eq. auto.
rewrite <- H1 in Hx1. inv Hx1.
solv_eq.
inv H4.
eapply cmpu_bool_some_eq in Hx3 as ?.
rewrite H in Hx0. inv Hx0.
auto.
auto.
revert Hx Hx2 H5 H10. clear;intros.
unfold Mem.loadv in *;ex_match.
eapply eval_addrmode_lessdef in H10 as ?.
inv H. rewrite<- H2,Hx0 in Hx1. inv Hx1.
eapply Mem.load_extends in H5;eauto;Hsimpl;solv_eq;auto.
rewrite<- H1 in *;simpl in *;congruence.
}
}
} *) }
atext *) {
intros.
invMS.
inversion MC;
subst Hcore Lcore m m';
try discriminate.
unfold at_external in *.
ex_match.
inversion H0;
clear H0;
subst i0 sg0 args.
Esimpl;
eauto.
{
unfold LDSimDefs.arg_rel.
clear MC.
revert args'
AGMU H2 H8 ;
clear.
should be extracted as a lemma ...
induction argSrc;
intros args'
AGMU GARG LD.
simpl.
inv LD.
auto.
inv LD.
inv GARG.
constructor;
auto.
clear H3 H4 IHargSrc.
inv H1;
auto.
destruct v2;
auto.
simpl in H2.
eapply Bset.inj_dom in H2;
inv AGMU;
eauto.
destruct H2.
exploit proper_mu_inject_incr.
unfold Bset.inj_to_meminj;
rewrite H;
eauto.
intro.
inv H0.
econstructor.
unfold Bset.inj_to_meminj;
rewrite H.
eauto.
rewrite Ptrofs.add_zero;
auto. }
eapply MemClosures_local.unmapped_closed_reach_closed_preserved_by_extends;
inv AGMU;
eauto.
eapply extends_reach_closed_implies_inject;
inv AGMU;
eauto.
unfold MS.
Esimpl;
eauto;
try eresolvfp;
try resvalid.
{
unfold at_external in *. ex_match.
inversion H0;subst f sg argSrc.
Esimpl;eauto.
constructor.
eapply MemClosures_local.unmapped_closed_reach_closed_preserved_by_extends; inv AGMU; eauto.
eapply extends_reach_closed_implies_inject; inv AGMU; eauto.
unfold MS.
Esimpl;eauto;try eresolvfp;try resvalid.
Esimpl;eauto;try eresolvfp;try resvalid.
constructor.
eapply MemClosures_local.unmapped_closed_reach_closed_preserved_by_extends; inv AGMU; eauto.
eapply extends_reach_closed_implies_inject; inv AGMU; eauto.
unfold MS.
Esimpl;eauto;try eresolvfp;try resvalid.
}
*) }
aftext *) {
intros i mu Hcore Hm Lcore Lm oresSrc Hcore'
oresTgt MATCH GRES AFTEXT ORESREL.
simpl in *.
unfold after_external in *.
destruct Hcore;
try discriminate.
{
destruct f;
try discriminate.
assert(
Hcore' =
match oresSrc with
|
Some res => (
Core_State (
set_pair (
loc_external_result sg)
res rs) #
PC <- (
rs RA)
loader)
|
None => (
Core_State (
set_pair (
loc_external_result sg)
Vundef rs) #
PC <- (
rs RA)
loader)
end).
ex_match.
invMS.
inv MC.
exists (
match oresTgt with
|
Some res => (
Core_State (
set_pair (
loc_external_result sg)
res rs') #
PC <- (
rs'
RA)
loader)
|
None => (
Core_State (
set_pair (
loc_external_result sg)
Vundef rs') #
PC <- (
rs'
RA)
loader)
end).
Esimpl;
eauto.
ex_match;
inv ORESREL;
try discriminate;
try contradiction;
simpl in *;
eauto;
ex_match.
intros.
exists 1%
nat.
assert (
Mem.extends Hm'
Lm').
{
inv AGMU;
eapply extends_rely_extends;
eauto. }
assert (
unmapped_closed mu Hm'
Lm').
{
eapply reach_closed_unmapped_closed.
inv H.
inv H2.
auto. }
destruct oresSrc,
oresTgt;
try contradiction;
ex_match;
unfold MS;
Esimpl;
try eresolvfp;
try resvalid;
try(
econstructor;
eauto;
solv_regset;
unfold set_pair;
ex_match;
solv_regset;
simpl in ORESREL;
inv ORESREL;
auto;
inv AGMU;
apply proper_mu_inject_incr in H2;
unfold inject_id in H2;
inv H2;
rewrite MemInterpolant.ptrofs_add_0;
auto;
fail);
try(
inv H;
inv H2;
unfold Mem.valid_block;
rewrite EQNEXT;
auto;
fail);
try(
inv H;
inv H4;
unfold Mem.valid_block;
rewrite EQNEXT;
auto;
fail).
}
{
assert(Hcore' =
match locked with
| LOCK => (Core_LockState rs STEP loader)
| _ => (Core_State rs loader)
end).
ex_match.
invMS. inv MC.
exists (match locked with
| LOCK => (Core_LockState rs' STEP loader)
| _ => (Core_State rs' loader)
end).
Esimpl;eauto.
ex_match; inv ORESREL;try discriminate;try contradiction;simpl in *;eauto; ex_match.
intros. exists 1%nat.
assert (Mem.extends Hm' Lm').
{ inv AGMU; eapply extends_rely_extends; eauto. }
assert (unmapped_closed mu Hm' Lm').
{ eapply reach_closed_unmapped_closed. inv H. inv H3. auto. }
unfold MS.
Esimpl;eauto;try resolvfp;try resvalid;try(inv H; inv H3; unfold Mem.valid_block; rewrite EQNEXT; auto;fail);try(inv H; inv H4; unfold Mem.valid_block; rewrite EQNEXT;auto;fail).
ex_match;constructor;auto;try resolvfp;try resvalid.
}
*) }
halt *) {
intros.
simpl in *.
unfold halted in *.
destruct Hcore eqn:?;
try discriminate.
invMS.
inv MC.
destruct l;
try discriminate.
assert (
LDefs.Inv mu Hm Lm).
{
inv AGMU.
eapply extends_reach_closed_implies_inject;
eauto. }
assert (
reach_closed Lm (
Injections.SharedTgt mu)).
{
eapply unmapped_closed_reach_closed_preserved_by_injection';
eauto.
inv AGMU;
auto. }
destruct Val.cmp_bool eqn:?;[|
inv H0].
assert(
Val.cmp_bool Ceq (
rs'
PC)
Vzero =
Some b).
revert H4 Heqo;
clear;
intros.
unfold Val.cmp_bool in *;
simpl in *.
ex_match;
solv_rs;
auto.
rewrite H5.
ex_match.
{
Esimpl;
eauto.
inv H0.
unfold res_rel.
assert(
Val.lessdef (
r (
preg_of r0))(
rs' (
preg_of r0))).
solv_regset;
auto.
inv H0;
try constructor.
revert H2 AGMU;
clear;
intros ? [].
destruct (
r (
preg_of r0)).
all :
try constructor.
unfold inject_incr in proper_mu_inject_incr.
unfold inject_id in proper_mu_inject_incr.
simpl in H2.
apply proper_mu_inject in H2 as [].
unfold Bset.inj_to_meminj in proper_mu_inject_incr.
exploit proper_mu_inject_incr.
rewrite H.
eauto.
intro.
inv H0.
rewrite <-
Ptrofs.add_zero with(
x:=
i).
econstructor;
eauto.
unfold Bset.inj_to_meminj.
rewrite H.
eauto.
do 2
rewrite Ptrofs.add_zero;
auto.
}
{
Esimpl;
eauto.
inv H0.
unfold res_rel.
assert(
Val.lessdef (
Val.longofwords(
r (
preg_of rhi)) (
r (
preg_of rlo)))(
Val.longofwords (
rs' (
preg_of rhi)) (
rs' (
preg_of rlo)))).
solv_regset;
auto.
intros [] [] [] ;
auto;
congruence.
inv H0;
try constructor.
revert H2 AGMU;
clear;
intros ? [].
destruct ( (
Val.longofwords (
r (
preg_of rhi)) (
r (
preg_of rlo))))
eqn:?.
all :
try constructor.
unfold inject_incr in proper_mu_inject_incr.
unfold inject_id in proper_mu_inject_incr.
simpl in H2.
apply proper_mu_inject in H2 as [].
unfold Bset.inj_to_meminj in proper_mu_inject_incr.
exploit proper_mu_inject_incr.
rewrite H.
eauto.
intro.
inv H0.
rewrite <-
Ptrofs.add_zero with(
x:=
i).
econstructor;
eauto.
unfold Bset.inj_to_meminj.
rewrite H.
eauto.
do 2
rewrite Ptrofs.add_zero;
auto.
}
}
Unshelve.
eapply Genv.to_senv;
eauto.
apply Mem.empty.
apply O.
apply O.
apply O. *)Qed.