Module MutrecAproof
Require Import CoqlibC Maps Postorder.
Require Import AST Linking.
Require Import ValuesC Memory GlobalenvsC Events Smallstep.
Require Import Op Registers ClightC Renumber.
Require Import CtypesC CtypingC.
Require Import sflib.
Require Import IntegersC.
Require Import MutrecHeader.
Require Import MutrecA MutrecAspec.
Require Import Simulation.
Require Import Skeleton Mod ModSem SimMod SimModSemLift SimSymb SimMemLift AsmregsC MatchSimModSem.
Require SoundTop.
Require SimMemInjC SimMemInjInvC.
Require Import Clightdefs.
Require Import CtypesC.
Set Implicit Arguments.
Definition memoized_inv:
SimMemInjInv.memblk_invariant :=
SimMemInjInv.memblk_invarant_mk
(
fun mem =>
forall
chunk ofs ind
(
BOUND: 0 <=
ind < 1000)
(
INT:
chunk =
Mint32)
(
INDEX:
size_chunk Mint32 *
ind =
ofs),
exists i,
(<<
VINT:
mem chunk ofs =
Some (
Vint i)>>) /\
(<<
VAL:
forall (
NZERO:
i.(
Int.intval) <> 0),
(<<
MEMO:
i =
sum (
Int.repr ind)>>)>>))
(
fun chunk ofs p =>
exists ind,
(<<
CHUNK:
chunk =
Mint32>>) /\ (<<
BOUND: 0 <=
ind < 1000>>) /\
(<<
INDEX:
ofs =
size_chunk Mint32 *
ind>>) /\ (<<
WRITABLE:
p =
Writable>>)).
Local Instance SimMemMemoizedA:
SimMem.class :=
SimMemInjInvC.SimMemInjInv
SimMemInjInv.top_inv memoized_inv.
Definition symbol_memoized:
ident ->
Prop :=
eq _memoized.
Lemma memoized_inv_store_le i ind blk ofs m_tgt
(
sm0 sm1:
SimMemInjInv.t')
(
MWF:
SimMem.wf sm0)
(
INVAR:
sm0.(
SimMemInjInv.mem_inv_tgt)
blk)
(
SUM:
i =
sum (
Int.repr ind))
(
OFS:
ofs =
size_chunk Mint32 *
ind)
(
STR:
Mem.store Mint32 sm0.(
SimMemInjInv.minj).(
SimMemInj.tgt)
blk ofs (
Vint i) =
Some m_tgt)
(
MREL:
sm1 =
SimMemInjInv.mk
(
SimMemInjC.update
(
sm0.(
SimMemInjInv.minj))
(
sm0.(
SimMemInjInv.minj).(
SimMemInj.src))
m_tgt
(
sm0.(
SimMemInjInv.minj).(
SimMemInj.inj)))
sm0.(
SimMemInjInv.mem_inv_src)
sm0.(
SimMemInjInv.mem_inv_tgt))
:
(<<
MLE:
SimMem.le sm0 sm1>>) /\
(<<
MWF:
SimMem.wf sm1>>).
Proof.
Section SIMMODSEM.
Variable skenv_link:
SkEnv.t.
Variable sm_link:
SimMem.t.
Let md_src:
Mod.t := (
MutrecAspec.module).
Let md_tgt:
Mod.t := (
ClightC.module2 prog).
Hypothesis (
INCL:
SkEnv.includes skenv_link md_src.(
Mod.sk)).
Hypothesis (
WF:
SkEnv.wf skenv_link).
Let ge := (
SkEnv.project skenv_link md_src.(
Mod.sk)).
Let tge :=
Build_genv (
SkEnv.revive (
SkEnv.project skenv_link md_tgt.(
Mod.sk))
prog)
prog.(
prog_comp_env).
Definition msp:
ModSemPair.t :=
ModSemPair.mk (
md_src skenv_link) (
md_tgt skenv_link)
symbol_memoized sm_link.
Inductive match_states_internal:
nat ->
MutrecAspec.state ->
Clight.state ->
Prop :=
|
match_callstate_nonzero
idx i m_src m_tgt
fptr
(
RANGE: 0 <=
i.(
Int.intval) <
MAX)
(
FINDF:
Genv.find_funct (
Smallstep.globalenv (
modsem2 skenv_link prog))
fptr =
Some (
Internal func_f))
(
IDX: (
idx > 3)%
nat)
:
match_states_internal idx (
Callstate i m_src) (
Clight.Callstate fptr (
Tfunction
(
Tcons tint Tnil)
tint cc_default)
[
Vint i]
Kstop m_tgt)
|
match_returnstate
idx i m_src m_tgt
:
match_states_internal idx (
Returnstate i m_src) (
Clight.Returnstate (
Vint i)
Kstop m_tgt)
.
Inductive match_states (
sm_init:
SimMem.t)
(
idx:
nat) (
st_src0:
MutrecAspec.state) (
st_tgt0:
Clight.state) (
sm0:
SimMem.t):
Prop :=
|
match_states_intro
(
MATCHST:
match_states_internal idx st_src0 st_tgt0)
(
MCOMPATSRC:
st_src0.(
get_mem) =
sm0.(
SimMem.src))
(
MCOMPATTGT:
st_tgt0.(
ClightC.get_mem) =
sm0.(
SimMem.tgt))
(
MWF:
SimMem.wf sm0)
(
MLE:
SimMem.le sm_init sm0)
.
Lemma g_blk_exists
:
exists g_blk,
(<<
FINDG:
Genv.find_symbol
(
SkEnv.revive (
SkEnv.project skenv_link (
CSk.of_program signature_of_function prog))
prog)
g_id =
Some g_blk>>)
/\
(<<
FINDG:
Genv.find_funct_ptr
(
SkEnv.revive (
SkEnv.project skenv_link (
CSk.of_program signature_of_function prog))
prog)
g_blk =
None>>)
/\
(<<
FINDG:
exists skd,
Genv.find_funct_ptr skenv_link g_blk =
Some skd /\
Some (
signature_of_type (
Tcons tint Tnil)
tint cc_default) =
Sk.get_csig skd>>)
.
Proof.
Lemma match_states_lxsim
sm_init idx st_src0 st_tgt0 sm0
(
SIMSK:
SimSymb.sim_skenv
sm0 symbol_memoized
(
SkEnv.project skenv_link (
CSk.of_program signature_of_function prog))
(
SkEnv.project skenv_link (
CSk.of_program signature_of_function prog)))
(
MATCH:
match_states sm_init idx st_src0 st_tgt0 sm0)
:
<<
XSIM:
lxsimL (
md_src skenv_link) (
md_tgt skenv_link)
(
fun st =>
unit ->
exists su m_init,
SoundTop.sound_state su m_init st)
top3 (
fun _ _ =>
SimMem.le)
sm_init (
Ord.lift_idx lt_wf idx)
st_src0 st_tgt0 sm0>>
.
Proof.
revert_until tge.
pcofix CIH.
i.
pfold.
generalize g_blk_exists;
et.
i;
des.
inv MATCH;
subst.
ss.
inv MATCHST;
ss;
clarify.
-
destruct (
classic (
i =
Int.zero)).
+
clarify.
econs 2.
i.
esplits;
cycle 3.
{
ii.
esplits.
econs;
eauto.
econs;
ss;
eauto.
-
econs.
-
econs;
eauto.
econs.
-
ii.
ss.
des;
clarify.
-
econs. }
econs 2.
{
split.
-
econs 2.
+
ss.
econs 1.
+
econs 1.
+
ss.
-
eapply Ord.lift_idx_spec.
instantiate (1:=3%
nat).
nia. }
refl.
left.
pfold.
econs 1.
i;
des.
econs 2.
*
split;
cycle 1.
{
apply Ord.lift_idx_spec.
instantiate (1:=2%
nat).
nia. }
eapply plus_left with (
t1 :=
E0) (
t2 :=
E0);
ss.
{
econs;
eauto.
{
eapply modsem2_determinate;
eauto. }
econs;
eauto.
econs;
ss;
eauto;
try (
by repeat (
econs;
ss;
eauto)).
unfold _x.
unfold _t'1.
rr.
ii;
ss.
des;
ss;
clarify.
}
eapply star_left with (
t1 :=
E0) (
t2 :=
E0);
ss.
{
econs;
eauto.
{
eapply modsem2_determinate;
eauto. }
econs;
eauto.
}
eapply star_left with (
t1 :=
E0) (
t2 :=
E0);
ss.
{
econs;
eauto.
{
eapply modsem2_determinate;
eauto. }
econs;
eauto.
-
repeat econs;
et.
-
ss.
}
eapply star_left with (
t1 :=
E0) (
t2 :=
E0);
ss.
{
econs;
eauto.
{
eapply modsem2_determinate;
eauto. }
econs;
eauto.
-
repeat econs;
et.
-
ss.
-
ss.
}
apply star_refl.
*
refl.
*
right.
eapply CIH;
eauto.
econs;
ss;
eauto.
replace (
Int.repr 0)
with (
sum Int.zero).
{
econs;
eauto. }
{
rewrite sum_recurse.
des_ifs. }
+
destruct (
Genv.find_symbol
(
SkEnv.project skenv_link (
CSk.of_program signature_of_function prog))
_memoized)
eqn:
BLK;
cycle 1.
{
exfalso.
clear -
INCL BLK.
inversion INCL;
subst.
exploit DEFS;
eauto.
-
instantiate (2:=
_memoized).
ss.
-
i.
des.
exploit SkEnv.project_impl_spec.
eapply INCL.
i.
inv H.
ss.
exploit SYMBKEEP.
instantiate (1:=
_memoized).
ss.
i.
rr in H.
rewrite H in *.
clarify. }
inv MWF.
ss.
assert (
INVAR:
SimMemInjInv.mem_inv_tgt sm0 b).
{
inv SIMSK.
ss.
inv INJECT.
eapply INVCOMPAT;
eauto.
ss. }
hexploit SATTGT;
eauto.
intros SAT0.
exploit SAT0;
eauto.
i.
inv H0.
ss.
hexploit LOADVALS;
eauto.
i.
des.
destruct (
zeq (
Int.intval i0) 0).
{
econs 2.
i.
splits;
cycle 3.
{
i.
esplits.
econs;
ss;
eauto.
econs;
ss;
eauto.
-
econs.
-
econs;
eauto.
econs.
-
ii.
ss.
des;
clarify.
-
econs. }
econs 2.
{
split.
-
econs 2;
ss.
+
econs 2;
eauto.
clear -
H.
exploit Int.eq_false;
eauto.
i.
unfold Int.eq in *.
ss.
des_ifs.
+
econs;
eauto.
+
ss.
-
eapply Ord.lift_idx_spec.
eauto. }
refl.
left.
pfold.
econs.
i;
des.
econs 2;
eauto.
*
esplits;
cycle 1.
{
eapply Ord.lift_idx_spec.
eauto. }
eapply plus_left with (
t1 :=
E0) (
t2 :=
E0);
ss.
{
econs;
eauto.
{
eapply modsem2_determinate;
eauto. }
econs;
eauto.
econs;
ss;
eauto;
try (
by repeat (
econs;
ss;
eauto)).
unfold _x.
unfold _t'1.
rr.
ii;
ss.
des;
ss;
clarify.
}
eapply star_left with (
t1 :=
E0) (
t2 :=
E0);
ss.
{
econs;
eauto.
{
eapply modsem2_determinate;
eauto. }
econs;
eauto.
}
eapply star_left with (
t1 :=
E0) (
t2 :=
E0);
ss.
{
econs;
eauto.
{
eapply modsem2_determinate;
eauto. }
econs;
eauto.
-
repeat econs;
et.
-
ss.
rewrite Int.eq_false;
ss.
}
eapply star_left with (
t1 :=
E0) (
t2 :=
E0);
ss.
{
econs;
eauto.
{
eapply modsem2_determinate;
eauto. }
econs;
eauto.
}
eapply star_left with (
t1 :=
E0) (
t2 :=
E0);
ss.
{
econs;
eauto.
{
eapply modsem2_determinate;
eauto. }
econs;
eauto.
}
eapply star_left with (
t1 :=
E0) (
t2 :=
E0);
ss.
{
econs;
eauto.
{
eapply modsem2_determinate;
eauto. }
econs;
eauto;
swap 1 2.
-
econs.
+
ss.
econs.
econs;
ss.
*
econs.
{
eapply eval_Evar_global;
ss.
instantiate (1:=
b).
eauto. }
{
econs 2;
ss. }
*
econs;
ss.
*
ss.
+
econs 1;
ss.
psimpl.
replace (
Ptrofs.unsigned (
Ptrofs.mul (
Ptrofs.repr 4) (
Ptrofs.of_ints i)))
with (4 *
Int.intval i);
cycle 1.
{
unfold Ptrofs.mul.
ss.
destruct i.
ss.
unfold Ptrofs.of_ints.
ss.
unfold Int.signed.
ss.
des_ifs;
cycle 1;
unfold Int.half_modulus,
Int.modulus,
two_power_nat in *;
ss;
unfold MAX in *;
rewrite <-
Zdiv2_div in *;
ss.
{
lia. }
repeat rewrite Ptrofs.unsigned_repr.
auto.
all :
unfold Ptrofs.max_unsigned;
rewrite Ptrofs.modulus_power;
unfold Ptrofs.zwordsize,
Ptrofs.wordsize,
Wordsize_Ptrofs.wordsize;
des_ifs;
ss;
omega. }
eauto. }
eapply star_left with (
t1 :=
E0) (
t2 :=
E0);
ss.
{
econs;
eauto.
{
eapply modsem2_determinate;
eauto. }
econs;
eauto.
}
eapply star_left with (
t1 :=
E0) (
t2 :=
E0);
ss.
{
econs;
eauto.
{
eapply modsem2_determinate;
eauto. }
econs;
eauto.
}
eapply star_left with (
t1 :=
E0) (
t2 :=
E0);
ss.
{
econs;
eauto.
{
eapply modsem2_determinate;
eauto. }
ss.
econs;
eauto.
-
econs;
ss.
+
econs;
ss.
+
econs;
ss.
+
ss.
-
ss.
instantiate (1:=
true).
unfold Cop.bool_val.
ss.
unfold Int.eq.
unfold Val.of_bool.
destruct (
zeq (
Int.unsigned i0) (
Int.unsigned (
Int.repr 0)))
eqn:
EQ;
ss. }
eapply star_left with (
t1 :=
E0) (
t2 :=
E0);
ss.
{
econs;
eauto.
{
eapply modsem2_determinate;
eauto. }
econs;
eauto.
}
eapply star_left with (
t1 :=
E0) (
t2 :=
E0);
ss.
{
econs;
eauto.
{
eapply modsem2_determinate;
eauto. }
econs;
eauto.
}
eapply star_left with (
t1 :=
E0) (
t2 :=
E0);
ss.
{
econs;
eauto.
{
eapply modsem2_determinate;
eauto. }
econs;
eauto;
swap 1 2.
-
econs.
+
eapply eval_Evar_global;
ss.
et.
+
econs 2;
et.
-
unfold Cop.classify_fun.
ss.
-
repeat econs;
ss;
et.
}
eapply star_refl.
*
refl.
*
left.
pfold.
econs 3;
et.
{
econs;
eauto. }
{
econs.
econs;
eauto. }
ii;
des.
inv ATSRC.
ss;
clarify.
unfold Clight.fundef in *.
assert(
g_fptr =
g_blk).
{
unfold SkEnv.revive in FINDG.
rewrite Genv_map_defs_symb in *.
clarify. }
clarify.
eexists (
Args.mk _ [
Vint (
Int.sub i (
Int.repr 1))]
_).
exists sm0.
esplits;
ss;
eauto.
{
econs;
ss;
eauto.
instantiate (1:=
Vptr g_blk Ptrofs.zero).
inv SIMSK.
inv SIMSKENV.
inv INJECT.
ss.
econs.
eapply DOMAIN;
eauto.
exploit Genv.genv_symb_range.
unfold Genv.find_symbol in *.
eauto.
i.
ss.
ii.
exploit INVCOMPAT;
eauto.
i.
rewrite <-
H1 in H0.
ss.
rewrite Ptrofs.add_zero_l.
ss. }
{
refl. }
{
econs;
eauto. }
i.
inv AFTERSRC.
inv SIMRETV;
ss;
clarify.
hexploit Mem.valid_access_store.
{
instantiate (4:=
sm_ret.(
SimMemInjInv.minj).(
SimMemInj.tgt)).
inv MWF.
inv WF.
exploit SATTGT0;
eauto.
-
inv MLE0.
erewrite <-
MINVEQTGT.
eauto.
-
i.
inv H0.
hexploit PERMISSIONS0;
eauto.
ss.
esplits;
eauto. }
intros [
m_tgt STR].
exploit SimMemInjInvC.unlift_wf;
try apply MLE0;
eauto.
{
econs;
eauto. }
intros MLE1.
exploit memoized_inv_store_le;
eauto.
i.
des.
esplits.
{
econs;
eauto. }
{
apply MLE2.
}
left.
pfold.
econs;
eauto.
i;
des.
econs 2;
eauto.
{
esplits;
eauto;
cycle 1.
{
instantiate (1:= (
Ord.lift_idx lt_wf 14%
nat)).
eapply Ord.lift_idx_spec;
et. }
eapply plus_left with (
t1 :=
E0) (
t2 :=
E0);
ss.
{
econs;
eauto.
{
eapply modsem2_determinate;
eauto. }
econs;
eauto.
}
eapply star_left with (
t1 :=
E0) (
t2 :=
E0);
ss.
{
econs;
eauto.
{
eapply modsem2_determinate;
eauto. }
econs;
eauto.
}
eapply star_left with (
t1 :=
E0) (
t2 :=
E0);
ss.
{
econs;
eauto.
{
eapply modsem2_determinate;
eauto. }
econs;
eauto.
econs;
eauto.
-
econs;
eauto.
ss.
-
econs;
eauto.
ss.
-
inv RETV.
ss.
unfold typify.
des_ifs. }
eapply star_left with (
t1 :=
E0) (
t2 :=
E0);
ss.
{
econs;
eauto.
{
eapply modsem2_determinate;
eauto. }
econs;
eauto.
}
eapply star_left with (
t1 :=
E0) (
t2 :=
E0);
ss.
{
econs;
eauto.
{
eapply modsem2_determinate;
eauto. }
econs;
eauto.
-
econs;
eauto.
econs;
eauto.
+
econs;
eauto.
*
eapply eval_Evar_global;
ss.
instantiate (1:=
b).
ss.
*
ss.
econs 2;
eauto.
+
econs;
eauto.
ss.
+
econs;
eauto.
-
econs;
eauto.
ss.
-
ss.
-
ss.
psimpl.
econs;
ss;
eauto.
rpapply STR.
f_equal.
+
unfold Ptrofs.mul.
ss.
destruct i.
ss.
unfold Ptrofs.of_ints.
ss.
unfold Int.signed.
ss.
des_ifs;
cycle 1;
unfold Int.half_modulus,
Int.modulus,
two_power_nat in *;
ss;
unfold MAX in *;
rewrite <-
Zdiv2_div in *;
ss.
{
lia. }
repeat rewrite Ptrofs.unsigned_repr.
auto.
all :
unfold Ptrofs.max_unsigned;
rewrite Ptrofs.modulus_power;
unfold Ptrofs.zwordsize,
Ptrofs.wordsize,
Wordsize_Ptrofs.wordsize;
des_ifs;
ss;
omega.
+
f_equal.
rewrite Int.repr_unsigned.
rewrite sum_recurse with (
i :=
i).
des_ifs.
rewrite Z.eqb_eq in Heq.
exploit Int.eq_spec.
instantiate (1:=
i).
instantiate (1:=
Int.zero).
unfold Int.eq.
unfold Int.unsigned.
rewrite Heq.
des_ifs.
i.
subst i.
rewrite Int.sub_zero_r.
rewrite sum_recurse.
des_ifs. }
eapply star_left with (
t1 :=
E0) (
t2 :=
E0);
ss.
{
econs;
eauto.
{
eapply modsem2_determinate;
eauto. }
econs;
eauto.
}
eapply star_left with (
t1 :=
E0) (
t2 :=
E0);
ss.
{
econs;
eauto.
{
eapply modsem2_determinate;
eauto. }
econs;
eauto.
-
econs;
eauto.
ss.
-
econs;
eauto.
-
econs;
eauto. }
eapply star_refl.
}
{
refl. }
right.
eapply CIH.
{
eapply SimMemInjInvC.sim_skenv_inj_lepriv;
cycle 1;
eauto.
etrans;
eauto.
{
exploit (
SimMemLift.lift_priv sm0);
eauto.
ss. }
etrans;
eauto;
cycle 1.
{
hexploit SimMem.pub_priv;
try apply MLE2.
eauto. }
etrans;
eauto.
{
hexploit SimMem.pub_priv;
try apply MLE0;
eauto. }
hexploit SimMemLift.unlift_priv;
revgoals.
{
intro T.
ss.
eauto. }
{
eauto. }
{
eauto. }
{
exploit (
SimMemLift.lift_priv sm0);
eauto.
ss. }
{
econs;
eauto. } }
{
econs;
ss.
-
replace (
Int.add (
sum (
Int.sub i Int.one))
i)
with (
sum i);
cycle 1.
{
rewrite sum_recurse with (
i :=
i).
des_ifs.
rewrite Z.eqb_eq in Heq.
exploit Int.eq_spec.
instantiate (1:=
i).
instantiate (1:=
Int.zero).
unfold Int.eq.
unfold Int.unsigned.
rewrite Heq.
des_ifs.
i.
subst i.
rewrite Int.sub_zero_r.
rewrite sum_recurse.
des_ifs. }
econs 2.
-
etrans;
eauto.
etrans;
eauto.
eapply SimMemInjInvC.unlift_spec;
eauto.
econs;
eauto.
}
}
{
hexploit VAL;
eauto.
i.
des.
clarify.
econs 2.
i.
splits;
cycle 3.
{
i.
esplits.
econs;
ss;
eauto.
econs;
ss;
eauto.
-
econs.
-
econs;
eauto.
econs.
-
ii.
ss.
des;
clarify.
-
econs. }
econs 2.
{
split.
-
econs 2;
ss.
+
econs;
eauto.
+
econs;
eauto.
+
ss.
-
eapply Ord.lift_idx_spec.
eauto. }
refl.
left.
pfold.
econs.
i;
des.
econs 2;
eauto.
*
esplits;
cycle 1.
{
eapply Ord.lift_idx_spec.
eauto. }
eapply plus_left with (
t1 :=
E0) (
t2 :=
E0);
ss.
{
econs;
eauto.
{
eapply modsem2_determinate;
eauto. }
econs;
eauto.
econs;
ss;
eauto;
try (
by repeat (
econs;
ss;
eauto)).
unfold _x.
unfold _t'1.
rr.
ii;
ss.
des;
ss;
clarify.
}
eapply star_left with (
t1 :=
E0) (
t2 :=
E0);
ss.
{
econs;
eauto.
{
eapply modsem2_determinate;
eauto. }
econs;
eauto.
}
eapply star_left with (
t1 :=
E0) (
t2 :=
E0);
ss.
{
econs;
eauto.
{
eapply modsem2_determinate;
eauto. }
econs;
eauto.
-
repeat econs;
et.
-
ss.
rewrite Int.eq_false;
ss.
}
eapply star_left with (
t1 :=
E0) (
t2 :=
E0);
ss.
{
econs;
eauto.
{
eapply modsem2_determinate;
eauto. }
econs;
eauto.
}
eapply star_left with (
t1 :=
E0) (
t2 :=
E0);
ss.
{
econs;
eauto.
{
eapply modsem2_determinate;
eauto. }
econs;
eauto.
}
eapply star_left with (
t1 :=
E0) (
t2 :=
E0);
ss.
{
econs;
eauto.
{
eapply modsem2_determinate;
eauto. }
econs;
eauto;
swap 1 2.
-
econs.
+
ss.
econs.
econs;
ss.
*
econs.
{
eapply eval_Evar_global;
ss.
instantiate (1:=
b).
ss. }
{
econs 2;
ss. }
*
econs;
ss.
*
ss.
+
econs 1;
ss.
psimpl.
replace (
Ptrofs.unsigned (
Ptrofs.mul (
Ptrofs.repr 4) (
Ptrofs.of_ints i)))
with (4 *
Int.intval i);
cycle 1.
{
unfold Ptrofs.mul.
ss.
destruct i.
ss.
unfold Ptrofs.of_ints.
ss.
unfold Int.signed.
ss.
des_ifs;
cycle 1;
unfold Int.half_modulus,
Int.modulus,
two_power_nat in *;
ss;
unfold MAX in *;
rewrite <-
Zdiv2_div in *;
ss.
{
lia. }
repeat rewrite Ptrofs.unsigned_repr.
auto.
all :
unfold Ptrofs.max_unsigned;
rewrite Ptrofs.modulus_power;
unfold Ptrofs.zwordsize,
Ptrofs.wordsize,
Wordsize_Ptrofs.wordsize;
des_ifs;
ss;
omega. }
eauto. }
eapply star_left with (
t1 :=
E0) (
t2 :=
E0);
ss.
{
econs;
eauto.
{
eapply modsem2_determinate;
eauto. }
econs;
eauto.
}
eapply star_left with (
t1 :=
E0) (
t2 :=
E0);
ss.
{
econs;
eauto.
{
eapply modsem2_determinate;
eauto. }
econs;
eauto.
}
eapply star_left with (
t1 :=
E0) (
t2 :=
E0);
ss.
{
econs;
eauto.
{
eapply modsem2_determinate;
eauto. }
ss.
econs;
eauto.
-
econs;
ss.
+
econs;
ss.
+
econs;
ss.
+
ss.
-
ss.
instantiate (1:=
false).
unfold Cop.bool_val.
ss.
unfold Int.eq.
unfold Val.of_bool.
destruct (
zeq (
Int.unsigned (
sum (
Int.repr (
Int.intval i))))
(
Int.unsigned (
Int.repr 0)))
eqn:
EQ;
ss. }
eapply star_left with (
t1 :=
E0) (
t2 :=
E0);
ss.
{
econs;
eauto.
{
eapply modsem2_determinate;
eauto. }
econs;
eauto.
}
eapply star_left with (
t1 :=
E0) (
t2 :=
E0);
ss.
{
econs;
eauto.
{
eapply modsem2_determinate;
eauto. }
econs;
eauto.
-
econs;
ss.
-
econs.
-
ss. }
apply star_refl.
*
refl.
*
right.
eapply CIH;
eauto.
{
econs;
eauto.
-
ss.
replace (
Int.repr (
Int.intval i))
with i.
+
econs;
eauto.
+
symmetry.
eapply Int.eqm_repr_eq.
eapply Int.eqm_refl2.
ss.
-
econs;
eauto. }
}
-
econs 4;
ss;
eauto.
econs;
ss;
eauto.
Qed.
Theorem sim_modsem
:
ModSemPair.sim msp
.
Proof.
End SIMMODSEM.
Theorem sim_mod
:
ModPair.sim (
ModPair.mk (
MutrecAspec.module) (
ClightC.module2 prog)
symbol_memoized)
.
Proof.
econs;
ss.
-
econs;
ss.
+
i.
inv SS.
esplits;
ss;
eauto.
*
econs;
ss.
ii.
des.
econs.
{
ii.
ss.
des.
clarify.
econs;
ss.
-
ii.
eapply PERM;
eauto.
unfold MAX in *.
lia.
-
eapply Z.divide_factor_l. }
{
ss.
i.
clarify.
erewrite INIT;
ss;
eauto.
-
esplits;
eauto.
i.
rewrite sum_recurse.
des_ifs.
-
lia.
-
unfold MAX.
lia.
-
eapply Z.divide_factor_l. }
*
ii.
des;
clarify.
+
ii.
destruct H.
eapply in_prog_defmap in PROG.
ss.
unfold update_snd in PROG.
ss.
des;
clarify;
inv DROP;
ss.
des;
clarify.
-
ii.
ss.
inv SIMSKENVLINK.
inv SIMSKENV.
eapply sim_modsem;
eauto.
Qed.