Require Import Coqlib List Maps Integers.
Import ListNotations.
Require Import AST Linking Smallstep.
Require Import Globalenvs Values.
Require Import Op Registers Memory.
Require Import RTL RTLtyping.
Require Import CounterMeasures IPCFC.
Static specification
Definition gsr f :=
Pos.succ (
max_reg_function f).
Definition gsrv f :=
Pos.succ (
gsr f).
Definition rts f :=
Pos.succ (
gsrv f).
Definition tmp1 f :=
Pos.succ (
rts f).
Definition tmp2 f :=
Pos.succ (
tmp1 f).
Definition tmp3 f :=
Pos.succ (
tmp2 f).
Lemma transf_init_prot_entry:
forall id f f',
transf_function_init_prot id f =
Errors.OK f' ->
exists seq abort,
transf_init_prot id f =
Errors.OK seq
/\
spec_seq abort (
fn_code f') (
fn_entrypoint f')
seq CNoExit.
Proof.
Lemma transf_prot_entry protected:
forall id id' f f',
harden_name id =
Errors.OK id' ->
transf_function_prot protected id f =
Errors.OK f' ->
exists abort,
spec_seq abort (
fn_code f') (
fn_entrypoint f')
(
prot_prologue (
gsr f) (
gsrv f) (
rts f)
id')
(
COneExit (
fn_entrypoint f))
/\ (
fn_code f')!
abort =
Some (
Ibuiltin EF_cm_catch []
BR_none abort).
Proof.
Lemma transf_prot_spec protected:
forall id id' f f',
harden_name id =
Errors.OK id' ->
transf_function_prot protected id f =
Errors.OK f' ->
forall pc i,
(
fn_code f) !
pc =
Some i ->
exists abort res,
transf_partial_instr
transf_partial_nop_default transf_partial_op_default
transf_partial_load_default transf_partial_store_default
(
transf_call protected (
gsr f) (
gsrv f) (
tmp1 f))
(
fun _ _ _ =>
Errors.Error (
Errors.msg "IPCFC: tail calls are not allowed"))
transf_partial_builtin_default
transf_partial_cond_default transf_partial_jumptable_default
(
transf_return id' (
gsr f) (
gsrv f) (
rts f))
i =
Errors.OK res
/\
spec_seq abort (
fn_code f')
pc (
fst (
projT2 res)) (
snd (
projT2 res)).
Proof.
Additional lemmas
Lemma check_params_length:
forall params sig tt,
check_params params sig =
Errors.OK tt ->
length params =
length (
sig_args sig).
Proof.
Lemma check_params_norepet :
forall params sig tt,
check_params params sig =
Errors.OK tt ->
list_norepet params.
Proof.
Weaker match_prog
This ones passes linking !
Definition is_transf_function_prot (
p:
RTL.program)
id f f' :
Prop :=
exists prot,
(
forall id,
prot!.
id =
Some tt -> (
protected p)!.
id =
Some tt)
/\
transf_function_prot prot id f =
Errors.OK f'.
Inductive match_def (
p tp:
RTL.program) (
id:
qualident) :
Prop :=
|
match_def_none1 :
(
prog_defmap p)!.
id =
None ->
(
prog_defmap tp)!.
id =
None ->
match_def p tp id
|
match_def_none2 :
forall id' f f',
(
prog_defmap p)!.
id =
None ->
harden_name id' =
Errors.OK id ->
(
prog_defmap p)!.
id' =
Some (
Gfun (
Internal f)) ->
(
protected p)!.
id' =
Some tt ->
is_transf_function_prot p id' f f' ->
(
prog_defmap tp)!.
id =
Some (
Gfun (
Internal f')) ->
match_def p tp id
|
match_def_var :
forall v,
(
prog_defmap p)!.
id =
Some (
Gvar v) ->
(
prog_defmap tp)!.
id =
Some (
Gvar v) ->
match_def p tp id
|
match_def_unprot:
forall f,
(
protected p)!.
id =
None ->
(
prog_defmap p)!.
id =
Some (
Gfun f) ->
(
prog_defmap tp)!.
id =
Some (
Gfun f) ->
match_def p tp id
|
match_def_prot:
forall id' f f1 f2,
(
protected p)!.
id =
Some tt ->
harden_name id =
Errors.OK id' ->
(
prog_defmap p)!.
id =
Some (
Gfun (
Internal f)) ->
transf_function_init_prot id f =
Errors.OK f1 ->
(
prog_defmap tp)!.
id =
Some (
Gfun (
Internal f1)) ->
is_transf_function_prot p id f f2 ->
(
prog_defmap tp)!.
id' =
Some (
Gfun (
Internal f2)) ->
match_def p tp id.
Global Hint Constructors match_def :
ipcfc.
Global Hint Unfold is_transf_function_prot :
ipcfc.
Record match_prog (
p tp:
program) :
Prop := {
match_prog_main:
tp.(
prog_main) =
p.(
prog_main);
match_prog_public:
tp.(
prog_public) =
p.(
prog_public);
match_prog_public_in:
forall id,
In id (
prog_public p) ->
In id (
map fst (
prog_defs p));
match_prog_def:
forall id,
match_def p tp id;
match_prog_inv:
forall id id' tf,
harden_name id' =
Errors.OK id ->
(
prog_defmap tp)!.
id =
Some (
Gfun (
Internal tf)) ->
exists f, (
prog_defmap p)!.
id' =
Some (
Gfun (
Internal f));
match_prog_wt:
wt_program p;
match_prog_norepet1:
list_norepet (
prog_defs_names p);
match_prog_norepet2:
list_norepet (
prog_defs_names tp);
match_prog_npref:
forall id,
In id (
map fst (
prog_defs p)) -> ~
qualident_prefixed id ipcfc_pre;
}.
Lemma transf_program_match:
forall prog tprog,
transf_program prog =
Errors.OK tprog ->
match_prog prog tprog.
Proof.
intros *
TR.
apply transf_program_match in TR as [].
repeat split;
auto.
intros *.
specialize (
match_prog_def0 id).
inv match_prog_def0;
eauto with ipcfc.
Qed.
Properties of match_prog
Lemma of_succ_nat_pred_id :
forall p,
Pos.of_succ_nat (
Nat.pred (
Pos.to_nat p)) =
p.
Proof.
Lemma match_prog_var p tp (
TRANSL:
match_prog p tp) :
forall id v,
(
prog_defmap p)!.
id =
Some (
Gvar v) <->
(
prog_defmap tp)!.
id =
Some (
Gvar v).
Proof.
intros *.
specialize (
match_prog_def _ _
TRANSL id)
as DEF.
inv DEF;
split;
intros *
FIND;
try congruence.
Qed.
Lemma match_prog_qualident_is_prefix :
forall p tp id,
match_prog p tp ->
In id (
prog_defs_names tp) ->
~
In id (
prog_defs_names p) ->
qualident_prefixed id ipcfc_pre.
Proof.
Ltac qualident_not_prefix id :=
unfold prog_defmap in *;
repeat
(
match goal with
|
H:
harden_name _ =
Errors.OK id |- _ =>
eapply harden_name_qualident_prefix in H
|
H1:
QITree.get id (
QITree_Properties.of_list (
prog_defs ?
p)) =
Some _,
H2:
forall id,
In id (
map fst (
prog_defs ?
p)) -> _ |- _ =>
eapply H2;
eauto;
eapply in_map_iff;
do 2
esplit; [|
eauto using in_prog_defmap];
auto
end).
Section IPCFC.
Fact fold_max_ge :
forall xs x0,
Forall (
Pos.ge (
fold_left Pos.max xs x0))
xs.
Proof.
induction xs;
simpl;
constructor;
auto.
clear IHxs.
assert (
forall x,
fold_left Pos.max xs x >=
x)%
positive as GE.
{
induction xs;
intros;
simpl;
try lia.
specialize (
IHxs (
Pos.max x a0)).
lia. }
specialize (
GE (
Pos.max x0 a)).
lia.
Qed.
Variable p:
program.
Variable tp:
program.
Hypothesis TRANSL:
match_prog p tp.
Let ge :=
Genv.globalenv p.
Let tge :=
Genv.globalenv tp.
Static properties
Lemma match_prog_harden_name_inv :
forall id id' g,
harden_name id =
Errors.OK id' ->
(
prog_defmap tp)!.
id' =
Some g ->
exists f, (
prog_defmap p)!.
id =
Some (
Gfun (
Internal f)).
Proof.
intros *
HARD FIND.
inv TRANSL.
specialize (
match_prog_def0 id)
as D.
specialize (
match_prog_def0 id')
as D'.
inv D'.
-
congruence.
-
eapply harden_name_inj in HARD;
eauto;
subst.
eauto.
-
exfalso.
qualident_not_prefix id'.
-
exfalso.
qualident_not_prefix id'.
-
exfalso.
eapply harden_name_not_twice in HARD;
eauto.
Qed.
Lemma transf_init_prot_sig:
forall id f f',
transf_function_init_prot id f =
Errors.OK f' ->
fn_sig f' =
fn_sig f.
Proof.
Lemma transf_prot_sig protected:
forall id f f',
transf_function_prot protected id f =
Errors.OK f' ->
fn_sig f' =
transf_sig (
fn_sig f).
Proof.
Lemma transf_init_prot_params :
forall id f f',
transf_function_init_prot id f =
Errors.OK f' ->
fn_params f' =
fn_params f.
Proof.
Lemma transf_prot_params protected:
forall id f f',
transf_function_prot protected id f =
Errors.OK f' ->
fn_params f' = (
gsr f)::(
rts f)::
fn_params f.
Proof.
Fact transf_init_prot_stacksize :
forall id f f',
transf_function_init_prot id f =
Errors.OK f' ->
fn_stacksize f' =
size_chunk Mint32.
Proof.
Fact transf_prot_stacksize protected :
forall id f f',
transf_function_prot protected id f =
Errors.OK f' ->
fn_stacksize f' =
fn_stacksize f.
Proof.
Public symbols
Fact prog_public_iff :
forall id v,
Genv.find_symbol (
Genv.globalenv p)
id =
Some v ->
In id (
filter (
fun x1 :
QualIdent.t =>
in_dec QualIdent.eq x1 (
map fst (
prog_defs p))) (
prog_public p))
<->
In id (
prog_public p).
Proof.
Lemma public_symbol_preserved:
forall id,
Senv.public_symbol (
symbolenv (
semantics tp))
id =
Senv.public_symbol (
symbolenv (
semantics p))
id.
Proof.
Relating Genv.find_symbol operations in the unprotected and transformed program
Lemma transform_find_symbol_1:
forall id b,
Genv.find_symbol ge id =
Some b ->
exists b',
Genv.find_symbol tge id =
Some b'.
Proof.
Lemma find_funct_ptr_init_prot:
forall id b f,
Genv.find_symbol ge id =
Some b ->
Genv.find_funct_ptr ge b =
Some f ->
exists b',
Genv.find_symbol tge id =
Some b'
/\
match (
protected p)!.
id with
|
Some _ =>
exists f1 f2,
f =
Internal f1
/\
transf_function_init_prot id f1 =
Errors.OK f2
/\
Genv.find_funct_ptr tge b' =
Some (
Internal f2)
|
None =>
Genv.find_funct_ptr tge b' =
Some f
end.
Proof.
Lemma find_funct_ptr_prot :
forall id b f,
Genv.find_symbol ge id =
Some b ->
Genv.find_funct_ptr ge b =
Some f ->
match (
protected p)!.
id with
|
Some _ =>
exists id' b' f1 f2,
f =
Internal f1
/\
harden_name id =
Errors.OK id'
/\
is_transf_function_prot p id f1 f2
/\
Genv.find_symbol tge id' =
Some b'
/\
Genv.find_funct_ptr tge b' =
Some (
Internal f2)
|
None =>
True
end.
Proof.
Semantic correctness
Memory injection
Inductive match_gdef id :
globdef fundef unit ->
globdef fundef unit ->
Prop :=
|
match_gdef_var :
forall v,
match_gdef id (
Gvar v) (
Gvar v)
|
match_gdef_external :
forall f,
(
protected p)!.
id =
None ->
match_gdef id (
Gfun f) (
Gfun f)
|
match_gdef_prot :
forall id' f f' fc' b,
(
protected p)!.
id =
Some tt ->
harden_name id =
Errors.OK id' ->
transf_function_init_prot id f =
Errors.OK f' ->
is_transf_function_prot p id f fc' ->
Genv.find_symbol tge id' =
Some b ->
Genv.find_def tge b =
Some (
Gfun (
Internal fc')) ->
match_gdef id (
Gfun (
Internal f)) (
Gfun (
Internal f')).
Open Scope Z.
Record meminj_preserves_globals (
f:
meminj) :
Prop := {
symbols_inject_1:
forall id b b' delta,
f b =
Some(
b',
delta) ->
Genv.find_symbol ge id =
Some b ->
delta = 0 /\
Genv.find_symbol tge id =
Some b';
symbols_inject_2:
forall id b,
Genv.find_symbol ge id =
Some b ->
exists b',
Genv.find_symbol tge id =
Some b' /\
f b =
Some(
b', 0);
defs_inject:
forall id b b' delta gd,
Genv.find_symbol ge id =
Some b ->
Genv.find_def ge b =
Some gd ->
f b =
Some(
b',
delta) ->
exists gd',
Genv.find_symbol tge id =
Some b'
/\
Genv.find_def tge b' =
Some gd'
/\
match_gdef id gd gd'
/\
delta = 0;
defs_rev_inject:
forall id b b' delta gd,
Genv.find_symbol tge id =
Some b' ->
Genv.find_def tge b' =
Some gd ->
f b =
Some(
b',
delta) ->
exists gd',
Genv.find_def ge b =
Some gd'
/\
match_gdef id gd' gd
/\
delta = 0
}.
Lemma globals_symbols_inject:
forall j,
meminj_preserves_globals j ->
Events.symbols_inject j ge tge.
Proof.
Fact ptrofs_add_repr_zero :
forall x,
Ptrofs.add x (
Ptrofs.repr 0) =
x.
Proof.
Lemma symbol_address_inject :
forall j id ofs,
meminj_preserves_globals j ->
Val.inject j (
Genv.symbol_address ge id ofs) (
Genv.symbol_address tge id ofs).
Proof.
State relation
Definition match_regs (
fn :
function)
j (
rs rs' :
regset) :=
(
forall r, (
r <=
RTL.max_reg_function fn)%
positive ->
Val.inject j rs#
r rs'#
r).
Definition match_gsr gsr rs' m m' inj bgsr vgsr :=
rs' #
gsr =
Vptr bgsr Ptrofs.zero
/\
Mem.valid_access m' Mint32 bgsr 0
Writable
/\
Mem.load Mint32 m' bgsr 0 =
Some (
Vint vgsr)
/\ (
forall delta,
Events.loc_out_of_reach inj m bgsr delta).
match_stacks with latest call unprotected
Inductive match_stacks_unprot (
m m':
mem) (
j:
meminj):
list stackframe ->
list stackframe ->
block ->
block ->
Prop :=
|
match_stacks_unprot_nil:
forall bound bound',
meminj_preserves_globals j ->
Ple (
Genv.genv_next ge)
bound ->
Ple (
Genv.genv_next tge)
bound' ->
match_stacks_unprot m m' j [] []
bound bound'
|
match_stacks_unprot_cons1:
forall res f sp sp' pc rs rs' stk stk' bound bound'
(
STACKS:
match_stacks_unprot m m' j stk stk' sp sp')
(
SPINJ:
j sp =
Some (
sp', 0))
(
REGINJ:
match_regs f j rs rs')
(
BELOW:
Plt sp bound)
(
TBELOW:
Plt sp' bound'),
match_stacks_unprot m m' j
(
Stackframe res f (
Vptr sp Ptrofs.zero)
pc rs ::
stk)
(
Stackframe res f (
Vptr sp' Ptrofs.zero)
pc rs' ::
stk')
bound bound'
|
match_stacks_unprot_cons2:
forall res id id' f f' sp sp' pc rs rs' stk stk' bound bound' bgsr vgsr vgsr'
(
REG_OK : (
res <=
max_reg_function f)%
positive)
(
HARDEN:
harden_name id =
Errors.OK id')
(
TR:
is_transf_function_prot p id f f')
(
STACKS:
match_stacks_prot m m' j stk stk' sp sp' id' (
sig_res (
fn_sig f))
bgsr vgsr)
(
SPINJ:
j sp =
Some (
sp', 0))
(
REGINJ:
match_regs f j rs rs')
(
BELOW:
Plt sp bound)
(
TBELOW:
Plt sp' bound')
(
GSR:
match_gsr (
gsr f)
rs' m m' j bgsr vgsr')
(
GSRBELOW:
Plt bgsr bound')
(
GSRV:
rs' # (
gsrv f) =
Vint vgsr')
(
RTS:
rs' # (
rts f) =
Vint (
Int.xor vgsr vgsr')),
match_stacks_unprot m m' j
(
Stackframe res f (
Vptr sp Ptrofs.zero)
pc rs ::
stk)
(
Stackframe res f' (
Vptr sp' Ptrofs.zero)
pc rs' ::
stk')
bound bound'
match_stacks with latest call unprotected
with match_stacks_init_prot (
m m':
mem) (
j:
meminj):
list stackframe ->
list stackframe ->
block ->
block ->
Prop :=
|
match_stacks_init_prot_nil:
forall bound bound',
meminj_preserves_globals j ->
Ple (
Genv.genv_next ge)
bound ->
Ple (
Genv.genv_next tge)
bound' ->
match_stacks_init_prot m m' j [] []
bound bound'
|
match_stacks_unprot_init_prot:
forall bound bound' stk stk'
(
STACKS:
match_stacks_unprot m m' j stk stk' bound bound'),
match_stacks_init_prot m m' j stk stk' bound bound'
|
match_stacks_init_prot_cons2:
forall res id id' f f' sp sp' pc rs rs' stk stk' bound bound' bgsr vgsr vgsr'
(
REG_OK : (
res <=
max_reg_function f)%
positive)
(
HARDEN:
harden_name id =
Errors.OK id')
(
TR:
is_transf_function_prot p id f f')
(
STACKS:
match_stacks_prot m m' j stk stk' sp sp' id' (
sig_res (
fn_sig f))
bgsr vgsr)
(
SPINJ:
j sp =
Some(
sp', 0))
(
REGINJ:
match_regs f j rs rs')
(
BELOW:
Plt sp bound)
(
TBELOW:
Plt sp' bound')
(
GSR:
match_gsr (
gsr f)
rs' m m' j bgsr vgsr')
(
GSRBELOW:
Plt bgsr bound')
(
GSRV:
rs' # (
gsrv f) =
Vint vgsr')
(
RTS:
rs' # (
rts f) =
Vint (
Int.xor vgsr vgsr')),
match_stacks_init_prot m m' j (
Stackframe res f (
Vptr sp Ptrofs.zero)
pc rs ::
stk)
(
Stackframe res f' (
Vptr sp' Ptrofs.zero)
pc rs' ::
stk')
bound bound'
match_stacks with latest call protected
with match_stacks_prot (
m m':
mem) (
j:
meminj):
list stackframe ->
list stackframe ->
block ->
block ->
qualident ->
xtype ->
block ->
int ->
Prop :=
|
match_stacks_prot_both:
forall res id id' f f' sp sp' pc pc' rs rs' stk stk' bound bound' pcxor2 pccheck pcstore pcnop2 pcabort cid cid' rty bgsr vgsr vgsr'
(
REG_OK : (
res <=
max_reg_function f)%
positive)
(
HARDEN1:
harden_name cid =
Errors.OK cid')
(
TR:
is_transf_function_prot p cid f f')
(
HARDEN2:
harden_name id =
Errors.OK id')
(
STACKS:
match_stacks_prot m m' j stk stk' sp sp' cid' (
sig_res (
fn_sig f))
bgsr vgsr')
(
SPINJ:
j sp =
Some(
sp', 0))
(
REGINJ:
match_regs f j rs rs')
(
BELOW:
Plt sp bound)
(
TBELOW:
Plt sp' bound')
(
GSR:
rs' # (
gsr f) =
Vptr bgsr Ptrofs.zero)
(
GSRBELOW:
Plt bgsr bound')
(
GSRV:
rs' # (
gsrv f) =
Vint vgsr)
(
RTS:
rs' # (
rts f) =
Vint (
Int.xor vgsr' vgsr))
(
LOAD: (
fn_code f') !
pc' =
Some (
Iload TRAP Mint32 (
Aindexed' Int.zero) [
gsr f] (
tmp1 f)
pcxor2))
(
XOR2: (
fn_code f') !
pcxor2 =
Some (
Iop (
Oxorimm (
hash_exit_sig id')) [
tmp1 f] (
tmp1 f)
pccheck))
(
CHECK: (
fn_code f') !
pccheck =
Some (
Icond (
Ccomp Cne) [
tmp1 f;
gsrv f]
pcabort pcstore (
Some false)))
(
STORE: (
fn_code f') !
pcstore =
Some (
Istore Mint32 (
Aindexed' Int.zero) [
gsr f] (
gsrv f)
pcnop2))
(
NOP2: (
fn_code f') !
pcnop2 =
Some (
Inop pc)),
match_stacks_prot m m' j (
Stackframe res f (
Vptr sp Ptrofs.zero)
pc rs ::
stk)
(
Stackframe res f' (
Vptr sp' Ptrofs.zero)
pc' rs' ::
stk')
bound bound' id' rty bgsr vgsr
|
match_stacks_prot_right:
forall id id' f f' pc' rs' sp' stk stk' bound bound' pcxor2 pccheck pcstore pcret pcabort bgsr vgsr
(
HARDEN:
harden_name id =
Errors.OK id')
(
TR:
transf_function_init_prot id f =
Errors.OK f')
(
STACKS:
match_stacks_init_prot m m' j stk stk' bound sp')
(
TBELOW:
Plt sp' bound')
(
SPPERM:
Mem.range_perm m' sp' 0 (
fn_stacksize f')
Cur Freeable)
(
SPOUT:
forall off, 0 <=
off <
size_chunk Mint32 ->
Events.loc_out_of_reach j m sp' off)
(
GSR:
rs' # (
gsr f) =
Vptr bgsr Ptrofs.zero)
(
GSRABOVE:
Ple sp' bgsr)
(
GSRBELOW:
Plt bgsr bound')
(
GSRV:
rs' # (
gsrv f) =
Vint vgsr)
(
LOAD: (
fn_code f') !
pc' =
Some (
Iload TRAP Mint32 (
Aindexed' Int.zero) [
gsr f] (
tmp1 f)
pcxor2))
(
XOR2: (
fn_code f') !
pcxor2 =
Some (
Iop (
Oxorimm (
hash_exit_sig id')) [
tmp1 f] (
tmp1 f)
pccheck))
(
CHECK: (
fn_code f') !
pccheck =
Some (
Icond (
Ccomp Cne) [
tmp1 f;
gsrv f]
pcabort pcstore (
Some false)))
(
STORE: (
fn_code f') !
pcstore =
Some (
Istore Mint32 (
Aindexed' Int.zero) [
gsr f] (
gsrv f)
pcret))
(
RET: (
fn_code f') !
pcret =
Some (
Ireturn (
match sig_res (
fn_sig f)
with Xvoid =>
None | _ =>
Some (
tmp3 f)
end))),
match_stacks_prot m m' j stk
(
Stackframe (
tmp3 f)
f' (
Vptr sp' Ptrofs.zero)
pc' rs' ::
stk')
bound bound' id' (
sig_res (
fn_sig f))
bgsr vgsr.
Scheme match_stacks_unprot_ind2 :=
Induction for match_stacks_unprot Sort Prop
with match_stacks_init_prot_ind2 :=
Induction for match_stacks_init_prot Sort Prop
with match_stacks_prot_ind2 :=
Induction for match_stacks_prot Sort Prop.
Combined Scheme match_stacks_all_ind from
match_stacks_unprot_ind2,
match_stacks_init_prot_ind2,
match_stacks_prot_ind2.
Inductive match_states:
RTL.state ->
RTL.state ->
Prop :=
|
match_states_unprot:
forall stk stk' f sp sp' pc rs rs' m m' j
(
STACKS:
match_stacks_unprot m m' j stk stk' sp sp')
(
SPINJ:
j sp =
Some(
sp', 0))
(
BELOW:
Plt sp (
Mem.nextblock m))
(
TBELOW:
Plt sp' (
Mem.nextblock m'))
(
REGS:
match_regs f j rs rs')
(
MEMINJ:
Mem.inject j m m'),
match_states
(
State stk f (
Vptr sp Ptrofs.zero)
pc rs m)
(
State stk' f (
Vptr sp' Ptrofs.zero)
pc rs' m')
|
match_states_prot:
forall stk stk' id id' f f' sp sp' pc rs rs' m m' j bgsr vgsr vgsr'
(
STACKS:
match_stacks_prot m m' j stk stk' sp sp' id' (
sig_res (
fn_sig f))
bgsr vgsr')
(
HARDEN:
harden_name id =
Errors.OK id')
(
TR:
is_transf_function_prot p id f f')
(
SPINJ:
j sp =
Some(
sp', 0))
(
BELOW:
Plt sp (
Mem.nextblock m))
(
TBELOW:
Plt sp' (
Mem.nextblock m'))
(
REGS :
match_regs f j rs rs')
(
MEMINJ:
Mem.inject j m m')
(
GSR:
match_gsr (
gsr f)
rs' m m' j bgsr vgsr)
(
GSRV:
rs' # (
gsrv f) =
Vint vgsr)
(
RTS:
rs' # (
rts f) =
Vint (
Int.xor vgsr' vgsr)),
match_states (
State stk f (
Vptr sp Ptrofs.zero)
pc rs m)
(
State stk' f' (
Vptr sp' Ptrofs.zero)
pc rs' m')
|
match_callstates_unprot:
forall stk stk' f args args' m m' j
(
STACKS:
match_stacks_unprot m m' j stk stk' (
Mem.nextblock m) (
Mem.nextblock m'))
(
AINJ:
Val.inject_list j args args')
(
MEMINJ:
Mem.inject j m m'),
match_states (
Callstate stk f args m) (
Callstate stk' f args' m')
|
match_callstates_init_prot:
forall id id' f f' fc' stk stk' args args' m m' j
(
STACKS:
match_stacks_init_prot m m' j stk stk' (
Mem.nextblock m) (
Mem.nextblock m'))
(
HARD:
harden_name id =
Errors.OK id')
(
TR:
transf_function_init_prot id f =
Errors.OK f')
(
FIND:
forall rs,
find_function tge (
inr id)
rs =
Some (
Internal f'))
(
TR':
is_transf_function_prot p id f fc')
(
FIND':
forall rs,
find_function tge (
inr id')
rs =
Some (
Internal fc'))
(
AINJ:
Val.inject_list j args args')
(
MEMINJ:
Mem.inject j m m'),
match_states (
Callstate stk (
Internal f)
args m)
(
Callstate stk' (
Internal f')
args' m')
|
match_callstates_prot:
forall id id' f f' stk stk' args rs' arg1 arg2 args' m m' j bgsr vgsr
(
STACKS:
match_stacks_prot m m' j stk stk' (
Mem.nextblock m) (
Mem.nextblock m')
id' (
sig_res (
fn_sig f))
bgsr vgsr)
(
HARD:
harden_name id =
Errors.OK id')
(
TR:
is_transf_function_prot p id f f')
(
AINJ:
Val.inject_list j args rs' ##
args')
(
MEMINJ:
Mem.inject j m m')
(
GSR:
match_gsr arg1 rs' m m' j bgsr vgsr)
(
ARG2:
rs' #
arg2 =
Vint (
Int.xor vgsr (
hash_entry_sig id'))),
match_states (
Callstate stk (
Internal f)
args m)
(
Callstate stk' (
Internal f')
rs' ## (
arg1 ::
arg2 ::
args')
m')
|
match_return_unprot:
forall stk stk' v v' m m' j
(
STACKS:
match_stacks_unprot m m' j stk stk' (
Mem.nextblock m) (
Mem.nextblock m'))
(
VINJ:
Val.inject j v v')
(
MEMINJ:
Mem.inject j m m'),
match_states (
Returnstate stk v m) (
Returnstate stk' v' m')
|
match_return_init_prot:
forall stk stk' v v' m m' j
(
STACKS:
match_stacks_init_prot m m' j stk stk' (
Mem.nextblock m) (
Mem.nextblock m'))
(
VINJ:
Val.inject j v v')
(
MEMINJ:
Mem.inject j m m'),
match_states (
Returnstate stk v m) (
Returnstate stk' v' m')
|
match_return_prot:
forall stk stk' v v' m m' j cid bgsr vgsr rty
(
STACKS:
match_stacks_prot m m' j stk stk' (
Mem.nextblock m) (
Mem.nextblock m')
cid rty bgsr vgsr)
(
STKNNIL:
stk <> [])
(
WTV:
rty =
Xvoid ->
v =
Vundef)
(
VINJ:
Val.inject j v v')
(
MEMINJ:
Mem.inject j m m')
(
GSRPERM:
Mem.valid_access m' Mint32 bgsr 0
Writable)
(
GSRL:
Mem.load Mint32 m' bgsr 0 =
Some (
Vint (
Int.xor (
hash_exit_sig cid)
vgsr)))
(
GSROUT:
forall delta,
Events.loc_out_of_reach j m bgsr delta),
match_states (
Returnstate stk v m)
(
Returnstate stk' v' m').
Properties
Lemma match_regs_assign :
forall f j rs rs' res v v',
Val.inject j v v' ->
match_regs f j rs rs' ->
match_regs f j (
rs #
res <-
v) (
rs' #
res <-
v').
Proof.
Lemma match_regs_assign' :
forall f j rs rs' res v',
(
max_reg_function f <
res)%
positive ->
match_regs f j rs rs' ->
match_regs f j rs (
rs' #
res <-
v').
Proof.
intros *
MATCH LT ?
LE.
rewrite Regmap.gso;
auto.
lia.
Qed.
Hint Resolve match_regs_assign match_regs_assign' :
ipcfc.
Lemma match_regs_incr:
forall f j j' rs rs',
inject_incr j j' ->
match_regs f j rs rs' ->
match_regs f j' rs rs'.
Proof.
Lemma match_regs_undef:
forall fn j rs',
match_regs fn j (
Regmap.init Vundef)
rs'.
Proof.
intros;
red;
intros.
rewrite Regmap.gi.
auto.
Qed.
Lemma match_regs_init:
forall fn j params args args',
Val.inject_list j args args' ->
match_regs fn j (
init_regs args params) (
init_regs args' params).
Proof.
Fact match_regs_init_twice:
forall fn j params args args',
Val.inject_list j args args' ->
match_regs fn j (
init_regs args params)
(
init_regs (
init_regs args' params) ##
params params).
Proof.
Lemma match_regs_inject_list :
forall f j rs rs' args,
match_regs f j rs rs' ->
(
forall r,
In r args -> (
r <=
max_reg_function f)%
positive) ->
Val.inject_list j rs ##
args rs' ##
args.
Proof.
induction args; intros * MATCH MAX; simpl; constructor; auto with datatypes.
Qed.
Lemma match_gsr_assign :
forall gsr rs m m' j bgsr vgsr r v,
r <>
gsr ->
match_gsr gsr rs m m' j bgsr vgsr ->
match_gsr gsr (
rs #
r <-
v)
m m' j bgsr vgsr.
Proof.
intros *
NEQ (?&?&?&?).
repeat (
esplit;
eauto).
rewrite Regmap.gso;
auto.
Qed.
Lemma match_gsr_mem :
forall f rs m1 m1' m2 m2' j bgsr vgsr,
(
Mem.load Mint32 m2' bgsr 0 =
Mem.load Mint32 m1' bgsr 0) ->
(
forall b delta ofs kind perm,
j b =
Some (
bgsr,
delta) ->
Mem.perm m2 b ofs kind perm ->
Mem.perm m1 b ofs kind perm) ->
(
forall ofs kind perm, 0 <=
ofs <
size_chunk Mint32 ->
Events.loc_out_of_reach j m1 bgsr ofs ->
Mem.perm m1' bgsr ofs kind perm ->
Mem.perm m2' bgsr ofs kind perm) ->
match_gsr f rs m1 m1' j bgsr vgsr ->
match_gsr f rs m2 m2' j bgsr vgsr.
Proof.
intros *
LOADS PERMS PERMS' (?&(
PERM&?)&?&
JPERM).
split; [|
split; [|
split]];
eauto.
-
split;
auto using Z.divide_0_r.
intros ?
OFS.
eapply PERMS',
PERM;
eauto.
-
erewrite LOADS;
eauto.
-
intros ???
J' PERM'.
eapply JPERM;
eauto.
Qed.
Lemma match_gsr_external_call :
forall f rs m1 m1' m2 m2' j j' bgsr vgsr ef vargs vargs' vres vres' t,
Events.external_call ef ge vargs m1 t vres m2 ->
Events.external_call ef tge vargs' m1' t vres' m2' ->
Mem.inject j m1 m1' ->
Mem.unchanged_on (
Events.loc_unmapped j)
m1 m2 ->
Mem.unchanged_on (
Events.loc_out_of_reach j m1)
m1' m2' ->
inject_incr j j' ->
Events.inject_separated j j' m1 m1' ->
match_gsr f rs m1 m1' j bgsr vgsr ->
match_gsr f rs m2 m2' j' bgsr vgsr.
Proof.
Lemma match_gsr_incr' :
forall f rs m m' j j' bgsr vgsr,
inject_incr j j' ->
(
forall b delta,
j b =
None ->
j' b =
Some (
bgsr,
delta) -> ~
Mem.valid_block m b) ->
match_gsr f rs m m' j bgsr vgsr ->
match_gsr f rs m m' j' bgsr vgsr.
Proof.
intros *
INCR SEP (?&?&?&
JPERM).
repeat (
esplit;
eauto).
intros ???
J' PERM.
destruct (
j b0)
as [(?&?)|]
eqn:
J.
-
apply INCR in J as J''.
setoid_rewrite J' in J''.
inv J''.
eapply JPERM;
eauto.
-
eapply SEP in J' as NV1;
eauto using Mem.perm_valid_block.
Qed.
Corollary match_gsr_incr :
forall f rs m m' j j' bgsr vgsr,
inject_incr j j' ->
Events.inject_separated j j' m m' ->
match_gsr f rs m m' j bgsr vgsr ->
match_gsr f rs m m' j' bgsr vgsr.
Proof.
intros * INCR SEP GSR.
eapply match_gsr_incr'; eauto.
intros * J J'. eapply SEP in J' as (?&?); eauto.
Qed.
Lemma match_stacks_preserves_globals:
forall m m' j s ts bound tbound,
match_stacks_unprot m m' j s ts bound tbound
\/
match_stacks_init_prot m m' j s ts bound tbound
\/ (
exists cid rty bgsr vgsr,
match_stacks_prot m m' j s ts bound tbound rty cid bgsr vgsr) ->
meminj_preserves_globals j.
Proof.
Ltac extlia :=
unfold Mem.valid_block,
tmp3,
tmp2,
tmp1,
rts,
gsrv,
gsr in *;
Coqlib.extlia.
Lemma match_stacks_incr:
forall m m' j j',
inject_incr j j' ->
forall s ts bound tbound,
(
forall b1 b2 delta,
j b1 =
None ->
j' b1 =
Some(
b2,
delta) ->
Ple bound b1 /\
Ple tbound b2) ->
(
match_stacks_unprot m m' j s ts bound tbound ->
match_stacks_unprot m m' j' s ts bound tbound)
/\ (
match_stacks_init_prot m m' j s ts bound tbound ->
match_stacks_init_prot m m' j' s ts bound tbound)
/\ (
forall cid rty bgsr vgsr,
match_stacks_prot m m' j s ts bound tbound cid rty bgsr vgsr ->
match_stacks_prot m m' j' s ts bound tbound cid rty bgsr vgsr).
Proof.
intros *
INCR SEP.
assert (
(
forall s ts bound tbound,
match_stacks_unprot m m' j s ts bound tbound ->
(
forall b1 b2 delta,
j b1 =
None ->
j' b1 =
Some(
b2,
delta) ->
Ple bound b1 /\
Ple tbound b2) ->
match_stacks_unprot m m' j' s ts bound tbound)
/\ (
forall s ts bound tbound,
match_stacks_init_prot m m' j s ts bound tbound ->
(
forall b1 b2 delta,
j b1 =
None ->
j' b1 =
Some(
b2,
delta) ->
Ple bound b1 /\
Ple tbound b2) ->
match_stacks_init_prot m m' j' s ts bound tbound)
/\ (
forall s ts bound tbound cid rty bgsr vgsr,
match_stacks_prot m m' j s ts bound tbound cid rty bgsr vgsr ->
(
forall b1 b2 delta,
j b1 =
None ->
j' b1 =
Some(
b2,
delta) ->
Ple bound b1 /\
Ple tbound b2) ->
match_stacks_prot m m' j' s ts bound tbound cid rty bgsr vgsr)).
2:{
destruct H as (?&?&?).
intros;
auto. }
eapply match_stacks_all_ind.
-
intros *
GLOBALS LE1 LE2 IND.
constructor;
auto.
assert (
SAME:
forall b b' delta,
Plt b (
Genv.genv_next ge) \/
Plt b' (
Genv.genv_next tge) ->
j' b =
Some(
b',
delta) ->
j b =
Some(
b',
delta)).
{
intros *
LT J'.
destruct (
j b)
as [[
b1 delta1] | ]
eqn:
J.
-
apply INCR in J.
congruence.
-
exploit IND;
eauto.
intros (?&?);
extlia.
}
constructor;
intros.
+
exploit symbols_inject_1;
eauto.
apply SAME;
auto.
left.
eapply Genv.genv_symb_range;
eauto.
+
exploit symbols_inject_2;
eauto.
intros (
b' &
A &
B).
exists b';
auto.
+
eapply defs_inject;
eauto.
apply SAME;
auto.
left.
eapply Genv.genv_defs_range;
eauto.
+
eapply defs_rev_inject;
eauto.
apply SAME;
auto.
right.
eapply Genv.genv_defs_range;
eauto.
-
intros * ?
IND ????
JIMPL.
econstructor;
eauto 8
using match_regs_incr.
+
eapply IND;
intros.
edestruct JIMPL;
eauto 8
using Plt_Ple,
Plt_Ple_trans.
-
intros * ????
IND ????????
JIMPL.
econstructor;
eauto 8
using match_regs_incr.
+
eapply IND;
intros.
edestruct JIMPL;
eauto 8
using Plt_Ple,
Plt_Ple_trans.
+
eapply match_gsr_incr';
eauto.
intros *
J J'.
eapply JIMPL in J' as (?&?);
eauto.
extlia.
-
intros *
GLOBALS LE1 LE2 IND.
constructor;
auto.
assert (
SAME:
forall b b' delta,
Plt b (
Genv.genv_next ge) \/
Plt b' (
Genv.genv_next tge) ->
j' b =
Some(
b',
delta) ->
j b =
Some(
b',
delta)).
{
intros *
LT J'.
destruct (
j b)
as [[
b1 delta1] | ]
eqn:
J.
-
apply INCR in J.
congruence.
-
exploit IND;
eauto.
intros (?&?);
extlia.
}
constructor;
intros.
+
exploit symbols_inject_1;
eauto.
apply SAME;
auto.
left.
eapply Genv.genv_symb_range;
eauto.
+
exploit symbols_inject_2;
eauto.
intros (
b' &
A &
B).
exists b';
auto.
+
eapply defs_inject;
eauto.
apply SAME;
auto.
left.
eapply Genv.genv_defs_range;
eauto.
+
eapply defs_rev_inject;
eauto.
apply SAME;
auto.
right.
eapply Genv.genv_defs_range;
eauto.
-
intros.
econstructor;
eauto.
-
intros * ????
IND ????????
JIMPL.
eapply match_stacks_init_prot_cons2;
eauto 8
using match_regs_incr.
+
eapply IND;
intros.
edestruct JIMPL;
eauto 8
using Plt_Ple,
Plt_Ple_trans.
+
eapply match_gsr_incr';
eauto.
intros *
J J'.
eapply JIMPL in J' as (?&?);
eauto.
extlia.
-
intros * ?????
IND ?????????????
JIMPL.
eapply match_stacks_prot_both with (
cid:=
cid);
eauto 8
using match_regs_incr.
+
eapply IND;
intros.
edestruct JIMPL;
eauto 8
using Plt_Ple,
Plt_Ple_trans.
-
intros * ???
IND ????????????
JIMPL.
eapply match_stacks_prot_right;
eauto 8
using match_regs_incr.
+
eapply IND;
intros.
edestruct JIMPL;
eauto 8
using Plt_Ple,
Plt_Ple_trans.
+
intros ? ?
LT ??
J PERM.
destruct (
j b0)
as [(?&?)|]
eqn:
J'.
*
apply INCR in J' as J''.
rewrite J in J'';
inv J''.
eapply SPOUT;
eauto.
*
edestruct JIMPL;
eauto.
extlia.
Qed.
Lemma match_stacks_bound:
forall m m' j s ts bound tbound bound' tbound',
Ple bound bound' ->
Ple tbound tbound' ->
(
match_stacks_unprot m m' j s ts bound tbound ->
match_stacks_unprot m m' j s ts bound' tbound')
/\ (
match_stacks_init_prot m m' j s ts bound tbound ->
match_stacks_init_prot m m' j s ts bound' tbound')
/\ (
forall cid rty bgsr vgsr,
match_stacks_prot m m' j s ts bound tbound cid rty bgsr vgsr ->
match_stacks_prot m m' j s ts bound' tbound' cid rty bgsr vgsr).
Proof.
Definition match_perm_1 (
j:
meminj)
m1 m2 bound' :=
(
forall b size kind perm, (
forall b' delta,
j b =
Some (
b',
delta) ->
Plt b' bound') ->
Mem.perm m2 b size kind perm ->
Mem.perm m1 b size kind perm).
Definition match_perm_2 (
j:
meminj)
m1 m1' m2' bound' :=
(
forall b' ofs kind perm,
Plt b' bound' ->
Events.loc_out_of_reach j m1 b' ofs ->
Mem.perm m1' b' ofs kind perm ->
Mem.perm m2' b' ofs kind perm).
Hint Unfold match_perm_1 match_perm_2 :
ipcfc.
Lemma match_stacks_mem:
forall m1 m2 m1' m2' j,
(
forall s ts bound tbound,
match_stacks_unprot m1 m1' j s ts bound tbound ->
match_perm_1 j m1 m2 tbound ->
match_perm_2 j m1 m1' m2' tbound ->
(
forall b',
Plt b' tbound -> (
forall ofs,
Events.loc_out_of_reach j m1 b' ofs) ->
Mem.load Mint32 m2' b' 0 =
Mem.load Mint32 m1' b' 0) ->
match_stacks_unprot m2 m2' j s ts bound tbound)
/\ (
forall s ts bound tbound,
match_stacks_init_prot m1 m1' j s ts bound tbound ->
match_perm_1 j m1 m2 tbound ->
match_perm_2 j m1 m1' m2' tbound ->
(
forall b',
Plt b' tbound -> (
forall ofs,
Events.loc_out_of_reach j m1 b' ofs) ->
Mem.load Mint32 m2' b' 0 =
Mem.load Mint32 m1' b' 0) ->
match_stacks_init_prot m2 m2' j s ts bound tbound)
/\ (
forall s ts bound tbound cid rty bgsr vgsr,
match_stacks_prot m1 m1' j s ts bound tbound cid rty bgsr vgsr ->
match_perm_1 j m1 m2 tbound ->
match_perm_2 j m1 m1' m2' tbound ->
(
forall b',
Plt b' bgsr ->
Plt b' tbound -> (
forall ofs,
Events.loc_out_of_reach j m1 b' ofs) ->
Mem.load Mint32 m2' b' 0 =
Mem.load Mint32 m1' b' 0) ->
match_stacks_prot m2 m2' j s ts bound tbound cid rty bgsr vgsr).
Proof.
intros ?????.
eapply match_stacks_all_ind.
-
intros.
constructor;
eauto.
-
intros.
econstructor;
eauto 11
using Plt_trans with ipcfc.
-
intros * ?????????????
PERM1 PERM2 LOAD.
econstructor;
eauto 11
using Plt_trans with ipcfc.
eapply match_gsr_mem in GSR;
eauto with ipcfc.
+
intros.
destruct GSR as (?&?&?&?).
eapply LOAD;
eauto.
+
intros *
J.
eapply PERM1;
eauto.
intros *
J'.
rewrite J in J';
inv J'.
auto.
-
intros.
econstructor;
eauto.
-
intros.
econstructor;
eauto 9
using Plt_trans.
-
intros * ?????????????
PERM1 PERM2 LOAD.
eapply match_stacks_init_prot_cons2;
eauto 11
using Plt_trans with ipcfc.
eapply match_gsr_mem in GSR;
eauto.
+
intros.
destruct GSR as (?&?&?&?).
eapply LOAD;
eauto.
+
intros *
J.
eapply PERM1;
eauto.
intros *
J'.
rewrite J in J';
inv J'.
auto.
-
intros.
econstructor. 1,3:
eauto.
all:
eauto 11
using Plt_trans with ipcfc.
-
intros *
HARD1 TR MATCH IND LT SPPERM SPOUT GSR GSRABOVE GSRBELOW ??????
PERM1 PERM2 LOAD.
econstructor;
eauto.
+
eapply IND;
eauto using Plt_trans with ipcfc.
intros.
eapply LOAD;
eauto;
extlia.
+
intros ?
OFF.
erewrite transf_init_prot_stacksize in *;
eauto.
+
intros ? ?
LT ??
J PERM.
eapply SPOUT;
eauto.
eapply PERM1;
eauto.
intros *
J'.
rewrite J' in J.
now inv J.
Qed.
Lemma match_stacks_mem_external_call:
forall ef vargs t vres m1 m2 m1' m2' j s ts bound tbound,
Mem.inject j m1 m1' ->
Events.external_call ef ge vargs m1 t vres m2 ->
Mem.unchanged_on (
Events.loc_out_of_reach j m1)
m1' m2' ->
(
match_stacks_unprot m1 m1' j s ts bound tbound ->
match_stacks_unprot m2 m2' j s ts bound tbound)
/\ (
match_stacks_init_prot m1 m1' j s ts bound tbound ->
match_stacks_init_prot m2 m2' j s ts bound tbound)
/\ (
forall cid rty bgsr vgsr,
match_stacks_prot m1 m1' j s ts bound tbound cid rty bgsr vgsr ->
match_stacks_prot m2 m2' j s ts bound tbound cid rty bgsr vgsr).
Proof.
Definition match_stacks_preserves m m' j bound bound' m1 m1' j1 bound1 bound1' :=
forall stk stk',
(
match_stacks_unprot m m' j stk stk' bound bound' ->
match_stacks_unprot m1 m1' j1 stk stk' bound1 bound1')
/\ (
match_stacks_init_prot m m' j stk stk' bound bound' ->
match_stacks_init_prot m1 m1' j1 stk stk' bound1 bound1')
/\ (
forall cid rty bgsr vgsr,
match_stacks_prot m m' j stk stk' bound bound' cid rty bgsr vgsr ->
match_stacks_prot m1 m1' j1 stk stk' bound1 bound1' cid rty bgsr vgsr).
Lemma match_stacks_alloc :
forall m m' sp sp' size m1 m1' j j1,
Mem.alloc m 0
size = (
m1,
sp) ->
Mem.alloc m' 0
size = (
m1',
sp') ->
inject_incr j j1 ->
j1 sp =
Some (
sp', 0) ->
(
forall b,
b <>
sp ->
j1 b =
j b) ->
match_stacks_preserves m m' j (
Mem.nextblock m) (
Mem.nextblock m')
m1 m1' j1 sp sp'.
Proof.
Lemma match_stacks_free :
forall m m' sp sp' size m1 m1' j,
j sp =
Some (
sp', 0) ->
Plt sp (
Mem.nextblock m) ->
Plt sp' (
Mem.nextblock m') ->
Mem.free m sp 0
size =
Some m1 ->
Mem.free m' sp' 0
size =
Some m1' ->
match_stacks_preserves m m' j sp sp' m1 m1' j (
Mem.nextblock m1) (
Mem.nextblock m1').
Proof.
Initial state
Lemma init_mem_exists:
forall m,
Genv.init_mem p =
Some m ->
exists tm,
Genv.init_mem tp =
Some tm.
Proof.
Section INIT_MEM.
Variables m tm:
mem.
Hypothesis IM:
Genv.init_mem p =
Some m.
Hypothesis TIM:
Genv.init_mem tp =
Some tm.
Definition init_meminj :
meminj :=
fun b =>
match Genv.invert_symbol ge b with
|
Some id =>
match Genv.find_symbol tge id with
|
Some b' =>
Some (
b', 0)
|
None =>
None
end
|
None =>
None
end.
Remark init_meminj_eq:
forall id b b',
Genv.find_symbol ge id =
Some b ->
Genv.find_symbol tge id =
Some b' ->
init_meminj b =
Some(
b', 0).
Proof.
Remark init_meminj_invert:
forall b b' delta,
init_meminj b =
Some(
b',
delta) ->
delta = 0 /\
exists id,
Genv.find_symbol ge id =
Some b /\
Genv.find_symbol tge id =
Some b'.
Proof.
Lemma init_meminj_preserves_globals:
meminj_preserves_globals init_meminj.
Proof.
Lemma init_meminj_invert_strong:
forall b b' delta,
init_meminj b =
Some(
b',
delta) ->
delta = 0 /\
exists id gd gd',
Genv.find_symbol ge id =
Some b
/\
Genv.find_symbol tge id =
Some b'
/\
Genv.find_def ge b =
Some gd
/\
Genv.find_def tge b' =
Some gd'
/\
match_gdef id gd gd'.
Proof.
Lemma bytes_of_init_inject:
forall il,
list_forall2 (
memval_inject init_meminj)
(
Genv.bytes_of_init_data_list ge il)
(
Genv.bytes_of_init_data_list tge il).
Proof.
Lemma init_mem_inj_1:
Mem.mem_inj init_meminj m tm.
Proof.
Lemma init_mem_inj_2:
Mem.inject init_meminj m tm.
Proof.
End INIT_MEM.
Theorem init_mem_inject:
forall m,
Genv.init_mem p =
Some m ->
exists f tm,
Genv.init_mem tp =
Some tm /\
Mem.inject f m tm /\
meminj_preserves_globals f.
Proof.
Lemma transf_initial_states:
forall st1,
initial_state p st1 ->
exists st2,
initial_state tp st2 /\
match_states st1 st2.
Proof.
Final state
Lemma transf_final_states:
forall st1 st2 r,
match_states st1 st2 ->
final_state st1 r ->
final_state st2 r.
Proof.
intros * MATCH FINAL.
inv FINAL; inv MATCH; inv VINJ.
- inv STACKS. constructor.
- inv STACKS; [|inv STACKS0]; constructor.
-
congruence.
Qed.
Step
Lemma eval_builtin_arg_inject:
forall f rs sp m j rs' sp' m' a v,
Events.eval_builtin_arg ge (
fun r =>
rs#
r) (
Vptr sp Ptrofs.zero)
m a v ->
(
forall r,
In r (
params_of_builtin_arg a) -> (
r <=
max_reg_function f)%
positive) ->
j sp =
Some(
sp', 0) ->
meminj_preserves_globals j ->
match_regs f j rs rs' ->
Mem.inject j m m' ->
exists v',
Events.eval_builtin_arg tge (
fun r =>
rs'#
r) (
Vptr sp' Ptrofs.zero)
m' a v'
/\
Val.inject j v v'.
Proof.
Lemma eval_builtin_args_inject:
forall f rs sp m j rs' sp' m' al vl,
Events.eval_builtin_args ge (
fun r =>
rs#
r) (
Vptr sp Ptrofs.zero)
m al vl ->
(
forall r,
In r (
params_of_builtin_args al) -> (
r <=
max_reg_function f)%
positive) ->
j sp =
Some(
sp', 0) ->
meminj_preserves_globals j ->
match_regs f j rs rs' ->
Mem.inject j m m' ->
exists vl',
Events.eval_builtin_args tge (
fun r =>
rs'#
r) (
Vptr sp' Ptrofs.zero)
m' al vl'
/\
Val.inject_list j vl vl'.
Proof.
induction 1;
intros.
-
exists (@
nil val);
split;
constructor.
-
simpl in H5.
exploit eval_builtin_arg_inject;
eauto using in_or_app.
intros (
v1' &
A &
B).
destruct IHlist_forall2 as (
vl' &
C &
D);
eauto using in_or_app.
exists (
v1' ::
vl');
split;
constructor;
auto.
Qed.
Lemma eval_assert_arg_inject:
forall f rs sp m j rs' sp' m' a v,
eval_assert_arg ge (
Vptr sp Ptrofs.zero)
rs m a v ->
(
forall r,
In r (
params_of_assert_arg a) -> (
r <=
max_reg_function f)%
positive) ->
j sp =
Some(
sp', 0) ->
meminj_preserves_globals j ->
match_regs f j rs rs' ->
Mem.inject j m m' ->
exists v',
eval_assert_arg tge (
Vptr sp' Ptrofs.zero)
rs' m' a v'
/\
Val.inject j v v'.
Proof.
Lemma eval_assert_args_inject:
forall f rs sp m j rs' sp' m' al vl,
eval_assert_args ge (
Vptr sp Ptrofs.zero)
rs m al vl ->
(
forall r,
In r (
params_of_assert_args al) -> (
r <=
max_reg_function f)%
positive) ->
j sp =
Some(
sp', 0) ->
meminj_preserves_globals j ->
match_regs f j rs rs' ->
Mem.inject j m m' ->
exists vl',
eval_assert_args tge (
Vptr sp' Ptrofs.zero)
rs' m' al vl'
/\
Val.inject_list j vl vl'.
Proof.
induction 1;
intros.
-
exists (@
nil val);
split;
constructor.
-
simpl in H5.
exploit eval_assert_arg_inject;
eauto using in_or_app.
intros (
v1' &
A &
B).
destruct IHlist_forall2 as (
vl' &
C &
D);
eauto using in_or_app.
exists (
v1' ::
vl');
split;
constructor;
auto.
Qed.
Lemma init_regs_gss :
forall params args,
length args =
length params ->
list_norepet params ->
(
init_regs args params) ##
params =
args.
Proof.
induction params;
intros []
LEN NR;
simpl in *;
inv LEN;
inv NR.
-
reflexivity.
-
f_equal;
auto.
+
now rewrite Regmap.gss.
+
rewrite regs_gsso;
auto.
Qed.
Lemma protected_entry_step_simulation :
forall id id' f f' stk args rs' stk' m m1 arg1 arg2 args' m' inj bgsr vgsr,
harden_name id =
Errors.OK id' ->
is_transf_function_prot p id f f' ->
match_regs f inj (
init_regs args (
fn_params f)) (
init_regs rs' ##
args' (
fn_params f)) ->
match_stacks_prot m m' inj stk stk' (
Mem.nextblock m) (
Mem.nextblock m')
id' (
sig_res (
fn_sig f))
bgsr vgsr ->
Mem.inject inj m m' ->
match_gsr arg1 rs' m m' inj bgsr vgsr ->
rs'#
arg2 =
Vint (
Int.xor vgsr (
hash_entry_sig id')) ->
list_forall2 Val.has_argtype rs' ##
args' (
sig_args (
fn_sig f)) ->
Mem.alloc m 0 (
fn_stacksize f) = (
m1,
Mem.nextblock m) ->
exists s2' :
RTL.state,
plus step tge (
Callstate stk' (
Internal f')
rs' ## (
arg1 ::
arg2 ::
args')
m')
Events.E0 s2' /\
match_states
(
State stk f (
Vptr (
Mem.nextblock m)
Ptrofs.zero) (
fn_entrypoint f) (
init_regs args (
fn_params f))
m1)
s2'.
Proof.
intros *
HARDEN (
prot&
PROT&
TR)
REGS STACKS MINJ (
GSR&
GSRPERM&
GSRL&
GSROUT)
ARG2 ARGTYS ALLOC;
subst.
exploit transf_prot_params;
eauto.
intros PARAMS.
exploit Mem.alloc_parallel_inject;
eauto. 1,2:
apply Z.le_refl.
intros (
inj'&
m1'&?&
ALLOC'&
MINJ1&
INJINCR&
NEXT&
NNEXT).
eapply Mem.alloc_result in ALLOC' as ?;
subst.
edestruct (
Mem.valid_access_store m1' Mint32 bgsr)
as (
m2'&
STORE').
{
eapply Mem.valid_access_alloc_other;
eauto. }
assert (
Mem.valid_block m' bgsr)
as VALID.
{
eapply Mem.valid_access_valid_block,
Mem.valid_access_implies;
eauto using perm_any_N. }
assert (
Mem.inject inj' m1 m2')
as INJ'.
{
eapply Mem.store_outside_inject; [| |
eauto];
eauto.
intros *
INJ PERM LT.
destruct (
peq b' (
Mem.nextblock m));
subst.
*
rewrite NEXT in INJ.
inv INJ.
eapply Mem.fresh_block_alloc;
eauto.
*
rewrite NNEXT in INJ;
auto.
eapply GSROUT;
eauto.
instantiate (1:=
ofs'+
delta).
replace (
ofs' +
delta -
delta)
with ofs' by lia.
eauto using Mem.perm_cur_max,
Mem.perm_implies,
Mem.perm_alloc_4,
perm_any_N.
}
exploit transf_prot_entry;
eauto.
intros;
inv_seq.
do 2
esplit; [
plus_step 4;
try apply plus_one|].
-
constructor.
+
erewrite transf_prot_sig; [|
eauto];
simpl.
repeat constructor;
auto.
*
now rewrite GSR.
*
now rewrite ARG2.
+
erewrite transf_prot_stacksize;
eauto.
-
rewrite PARAMS.
eapply exec_Iload;
eauto.
econstructor;
simpl.
+
now rewrite Regmap.gss,
GSR.
+
simpl.
setoid_rewrite Mem.load_alloc_unchanged;
eauto.
-
eapply exec_Iop;
eauto.
simpl.
rewrite Regmap.gss, 2
Regmap.gso,
Regmap.gss,
ARG2;
simpl. 2,3:
extlia.
now rewrite <-
Int.xor_assoc,
Int.xor_idem,
Int.xor_zero_l.
-
eapply exec_Icond with (
b:=
false);
eauto.
simpl.
rewrite Regmap.gss.
simpl.
now rewrite Int.eq_true.
-
eapply exec_Istore;
eauto.
+
simpl.
rewrite 2
Regmap.gso,
Regmap.gss;
simpl;
auto;
try reflexivity.
1,2:
unfold gsrv;
lia.
+
rewrite Regmap.gss,
GSR;
simpl.
apply STORE'.
-
econstructor;
eauto with ipcfc.
+
eapply match_stacks_alloc in STACKS. 2-6:
eauto.
eapply match_stacks_mem.
eapply STACKS.
all:
eauto using Ple_refl,
Mem.perm_store_1 with ipcfc.
*
intros *
LT OUT.
erewrite Mem.load_store_other;
eauto.
left.
extlia.
+
erewrite Mem.nextblock_alloc with (
m2:=
m1);
eauto.
extlia.
+
erewrite Mem.nextblock_store with (
m2:=
m2'),
Mem.nextblock_alloc with (
m2:=
m1');
eauto.
extlia.
+
simpl.
repeat apply match_regs_assign'. 1-4:
extlia.
eapply match_regs_incr;
eauto.
+
split; [|
split; [|
split]];
eauto.
*
rewrite ?
Regmap.gso. 2-3:
extlia.
simpl.
rewrite Regmap.gss,
GSR;
eauto.
*
eapply Mem.store_valid_access_1,
Mem.valid_access_alloc_other;
eauto.
*
erewrite Mem.load_store_same;
eauto.
simpl;
eauto.
*
intros ???
INJ PERM.
destruct (
peq b0 (
Mem.nextblock m));
subst.
--
rewrite NEXT in INJ.
inv INJ.
apply Mem.alloc_result in ALLOC';
subst.
eapply Plt_strict,
VALID.
--
rewrite NNEXT in INJ;
eauto.
eapply GSROUT;
eauto.
instantiate (1:=
delta).
eauto using Mem.perm_cur_max,
Mem.perm_implies,
Mem.perm_alloc_4,
perm_any_N.
+
rewrite Regmap.gss;
auto.
+
simpl.
rewrite 3
Regmap.gso,
Regmap.gss;
eauto.
all:
extlia.
Qed.
Fact plus_match_trans :
forall s2 s1',
(
exists s2',
plus step tge s1' []
s2' /\
exists s3',
plus step tge s2' []
s3' /\
match_states s2 s3') ->
exists s2',
plus step tge s1' []
s2' /\
match_states s2 s2'.
Proof.
intros * (?&
PLUS1&?&
PLUS2&
MATCH).
do 2
esplit; [|
eauto].
eapply plus_trans;
eauto.
Qed.
Hint Resolve plus_one :
ipcfc.
Hint Constructors step :
ipcfc.
Hint Constructors match_stacks_unprot match_stacks_init_prot match_stacks_prot match_states :
ipcfc.
Hint Resolve symbol_address_inject Mem.valid_pointer_inject_val Mem.weak_valid_pointer_inject_val Mem.weak_valid_pointer_inject_no_overflow Mem.different_pointers_inject :
inject.
Hint Unfold transf_call transf_return :
rtlcm.
Overall simulation proof
Lemma step_simulation :
forall s1 s2 t s1',
wt_state s1 ->
step ge s1 t s1' ->
match_states s1 s2 ->
exists s2',
plus step tge s2 t s2' /\
match_states s1' s2'.
Proof.
intros *
WTST STEP *
MATCH;
inv MATCH.
-
assert (
meminj_preserves_globals j)
as PRES by eauto using match_stacks_preserves_globals.
inv STEP;
eauto 8
with ipcfc.
+
assert (
Val.inject_list j rs ##
args rs' ##
args)
as INJL.
{
eapply match_regs_inject_list;
eauto.
intros.
eapply max_reg_function_use;
eauto. }
eapply eval_operation_inj in H8 as (?&
OP&
INJ);
eauto with inject.
do 2
esplit; [
eapply plus_one|].
*
eapply exec_Iop;
eauto.
*
econstructor;
eauto with ipcfc.
+
assert (
Val.inject_list j rs ##
args rs' ##
args)
as INJL.
{
eapply match_regs_inject_list;
eauto.
intros.
eapply max_reg_function_use;
eauto. }
inv H8.
*
eapply eval_addressing_inj in EVAL as (?&
EVAL'&
INJ);
eauto using symbol_address_inject.
exploit Mem.loadv_inject;
eauto.
intros (?&
LOAD'&
INJ').
do 2
esplit; [
eapply plus_one|].
--
eapply exec_Iload;
eauto using has_loaded_normal.
--
econstructor;
eauto with ipcfc.
all:
rewrite Regmap.gso;
auto;
eapply max_reg_function_def in H7;
simpl;
eauto;
extlia.
*
destruct eval_addressing eqn:
EVAL in LOAD.
specialize (
LOAD _
eq_refl).
eapply eval_addressing_inj in EVAL as (? &
EVAL'' &
INJ);
eauto using symbol_address_inject.
rewrite ptrofs_add_repr_zero in EVAL''.
destruct (
Mem.loadv chunk m' x)
eqn:
LOAD';
auto.
all:
do 2
esplit; [
eapply plus_one,
exec_Iload|];
eauto using has_loaded_normal.
1,3,5:
econstructor;
eauto with ipcfc.
1,2:
eapply has_loaded_default;
eauto;
intros *
EVAL'.
--
rewrite EVAL'' in EVAL';
inv EVAL';
auto.
--
eapply eval_addressing_inj_none in EVAL;
eauto using symbol_address_inject.
rewrite ptrofs_add_repr_zero in EVAL.
congruence.
+
eapply eval_addressing_inj in H8 as (?&
EVAL'&
INJ);
eauto using symbol_address_inject.
2:{
eapply match_regs_inject_list;
eauto.
intros.
eapply max_reg_function_use;
eauto;
simpl;
auto. }
exploit Mem.storev_mapped_inject;
eauto.
1:{
eapply REGS.
eapply max_reg_function_use;
eauto.
simpl;
auto. }
intros (?&
STORE'&
MINJ').
do 2
esplit; [
eapply plus_one;
eauto|].
*
eapply exec_Istore;
eauto.
*
unfold Mem.storev in *.
destruct a,
x;
try congruence.
econstructor;
eauto with ipcfc.
--
eapply match_stacks_mem;
eauto using STACKS.
all:
eauto using Mem.perm_store_1,
Mem.perm_store_2 with ipcfc.
intros *
LT1 LOC.
erewrite Mem.load_store_other;
eauto.
left;
intros ?;
subst.
inv INJ.
eapply LOC;
eauto.
instantiate (1:=(
Ptrofs.unsigned i)+
delta);
replace ((
Ptrofs.unsigned i) +
delta -
delta)
with (
Ptrofs.unsigned i)
by lia.
eapply Mem.store_needs_Writable in H9;
eauto using Mem.perm_implies,
perm_order.
--
erewrite Mem.nextblock_store;
eauto.
--
erewrite Mem.nextblock_store;
eauto.
+
assert (
Val.inject_list j rs ##
args rs' ##
args)
as ARGS.
{
eapply match_regs_inject_list;
eauto.
intros.
eapply max_reg_function_use;
eauto.
destruct ros;
simpl;
auto. }
destruct ros. 2:
destruct ((
protected p)!.
q)
as [[]|]
eqn:
ISINTERNAL.
*{
assert (
Val.inject j rs #
r rs' #
r)
as INJ.
{
eapply REGS,
max_reg_function_use;
eauto.
simpl;
auto. }
simpl in *.
destruct (
rs #
r);
simpl in *;
try congruence.
destruct (
Ptrofs.eq_dec i Ptrofs.zero); [|
congruence];
subst.
unfold Genv.find_funct_ptr in *.
destruct (
Genv.find_def ge b)
as [[]|]
eqn:
DEF;
inv H8.
eapply Genv.find_def_inversion_symbol in DEF as SYMB;
eauto using match_prog_norepet1.
destruct SYMB as (
q&
SYMB).
inversion INJ as [| | | |?????
J EQ1 EQ2 R'|];
subst;
clear INJ.
rewrite Ptrofs.add_zero_l in R'.
eapply defs_inject in J as (?&
SYMB'&
DEF'&
MATCH&?);
eauto;
subst.
inversion MATCH as [|?
FIND1 FIND2|??????
HARDEN' TR' TRC' SYMB'' DEF''];
subst;
clear MATCH.
1,2:(
do 2
esplit; [
eapply plus_one,
exec_Icall|]).
1,5:
eauto.
1,4:(
simpl;
unfold Genv.find_funct,
Genv.find_funct_ptr;
rewrite <-
R';
destruct (
Ptrofs.eq_dec _ _); [
now rewrite DEF'|
exfalso;
apply n;
reflexivity]).
1,3:
simpl;
auto;
eapply transf_init_prot_sig;
eauto.
-
econstructor;
eauto.
econstructor;
eauto with ipcfc.
-
eapply match_callstates_init_prot;
eauto.
2,3:
intros;
simpl;
unfold Genv.find_funct_ptr.
+
eapply match_stacks_unprot_init_prot,
match_stacks_unprot_cons1;
eauto with ipcfc.
+
now rewrite SYMB',
DEF'.
+
now rewrite SYMB'',
DEF''.
}
*{
eapply protected_internal in ISINTERNAL as INPROGS.
destruct INPROGS as (?&
INPROGS).
simpl in *.
apply prog_defmap_norepet in INPROGS;
eauto using match_prog_norepet1.
assert (
fd =
Internal x);
subst.
{
apply Genv.find_def_symbol in INPROGS as (?&
SYMB&
DEF).
unfold ge,
Genv.find_funct_ptr in *.
rewrite SYMB,
DEF in H8.
congruence. }
edestruct (
match_prog_def _ _
TRANSL q)
as [| | | |?????
HARDEN' FIND1 TR1 FIND2 (?&
PROT2&
TR2)
FIND3];
try congruence.
rewrite FIND1 in INPROGS.
inv INPROGS.
eapply Genv.find_def_symbol in FIND2 as DEF.
destruct DEF as (?&
SYMB&
DEF).
eapply Genv.find_def_symbol in FIND3 as DEF'.
destruct DEF' as (?&
SYMB'&
DEF').
do 2
esplit; [
eapply plus_one|].
-
eapply exec_Icall.
eauto.
simpl.
+
unfold tge,
Genv.find_funct_ptr.
setoid_rewrite SYMB.
now setoid_rewrite DEF.
+
simpl.
erewrite transf_init_prot_sig;
eauto with ipcfc.
-
eapply match_callstates_init_prot;
eauto with ipcfc;
intros;
simpl;
unfold tge,
Genv.find_funct_ptr.
+
setoid_rewrite SYMB.
now setoid_rewrite DEF.
+
setoid_rewrite SYMB'.
now setoid_rewrite DEF'.
}
*{
simpl in *.
unfold Genv.find_funct_ptr in *.
destruct (
Genv.find_symbol ge q)
eqn:
SYMB; [|
inv H8].
destruct (
Genv.find_def ge b)
as [[|]|]
eqn:
DEF;
inv H8.
assert ((
prog_defmap p)!.
q=
Some (
Gfun fd))
as DEFMAP.
{
eapply Genv.find_def_symbol.
eauto. }
edestruct (
match_prog_def _ _
TRANSL q)
as [| | |??
FIND1 FIND2|];
try congruence.
rewrite FIND1 in DEFMAP;
inv DEFMAP.
apply Genv.find_def_symbol in FIND2 as (?&
SYMB'&
DEF').
do 2
esplit; [
eapply plus_one|].
+
eapply exec_Icall;
eauto.
simpl.
*
unfold tge,
Genv.find_funct_ptr.
setoid_rewrite SYMB'.
setoid_rewrite DEF'.
reflexivity.
+
eapply match_callstates_unprot;
eauto.
eapply match_stacks_unprot_cons1;
eauto with ipcfc.
}
+
assert (
Val.inject_list j rs ##
args rs' ##
args)
as ARGS.
{
eapply match_regs_inject_list;
eauto.
intros.
eapply max_reg_function_use;
eauto.
destruct ros;
simpl;
auto. }
exploit Mem.free_parallel_inject;
eauto.
intros (?&
FREE'&
INJ').
rewrite ?
Z.add_0_r in FREE'.
destruct ros. 2:
destruct ((
protected p)!.
q)
as [[]|]
eqn:
ISINTERNAL.
*{
assert (
Val.inject j rs #
r rs' #
r)
as INJ.
{
eapply REGS,
max_reg_function_use;
eauto.
simpl;
auto. }
simpl in *.
destruct (
rs #
r);
simpl in *;
try congruence.
destruct (
Ptrofs.eq_dec i Ptrofs.zero); [|
congruence];
subst.
unfold Genv.find_funct_ptr in *.
destruct (
Genv.find_def ge b)
as [[]|]
eqn:
DEF;
inv H8.
eapply Genv.find_def_inversion_symbol in DEF as SYMB;
eauto using match_prog_norepet1.
destruct SYMB as (
q&
SYMB).
inversion INJ as [| | | |?????
J EQ1 EQ2 R'|];
subst;
clear INJ.
rewrite Ptrofs.add_zero_l in R'.
eapply defs_inject in J as (?&
SYMB'&
DEF'&
MATCH&?);
eauto;
subst.
inversion MATCH as [|?
FIND1 FIND2|??????
HARDEN' TR' TRC' SYMB'' DEF''];
subst;
clear MATCH.
1,2:(
do 2
esplit; [
eapply plus_one,
exec_Itailcall|]).
1,6:
eauto.
1,5:(
simpl;
unfold Genv.find_funct,
Genv.find_funct_ptr;
rewrite <-
R';
destruct (
Ptrofs.eq_dec _ _); [
now rewrite DEF'|
exfalso;
apply n;
reflexivity]).
all:
eauto.
2:
simpl;
auto;
eapply transf_init_prot_sig;
eauto.
-
econstructor;
eauto.
eapply match_stacks_free;
eauto.
-
econstructor;
eauto;
intros;
simpl;
unfold Genv.find_funct_ptr.
+
constructor.
eapply match_stacks_free;
eauto.
+
setoid_rewrite SYMB'.
now setoid_rewrite DEF'.
+
setoid_rewrite SYMB''.
now setoid_rewrite DEF''.
}
*{
eapply protected_internal in ISINTERNAL as INPROGS.
destruct INPROGS as (?&
INPROGS).
simpl in *.
apply prog_defmap_norepet in INPROGS;
eauto using match_prog_norepet1.
assert (
fd =
Internal x0);
subst.
{
apply Genv.find_def_symbol in INPROGS as (?&
SYMB&
DEF).
unfold ge,
Genv.find_funct_ptr in *.
rewrite SYMB,
DEF in H8.
congruence. }
edestruct (
match_prog_def _ _
TRANSL q)
as [| | | |?????
HARDEN' FIND1 TR1 FIND2 TR2 FIND3];
try congruence.
rewrite FIND1 in INPROGS.
inv INPROGS.
eapply Genv.find_def_symbol in FIND2 as DEF.
destruct DEF as (?&
SYMB&
DEF).
eapply Genv.find_def_symbol in FIND3 as DEF'.
destruct DEF' as (?&
SYMB'&
DEF').
do 2
esplit; [
eapply plus_one|].
-
eapply exec_Itailcall.
eauto.
simpl.
+
unfold tge,
Genv.find_funct_ptr.
setoid_rewrite SYMB.
now setoid_rewrite DEF.
+
simpl.
erewrite transf_init_prot_sig;
eauto with ipcfc.
+
eauto.
-
econstructor;
eauto with ipcfc;
intros;
simpl;
unfold tge,
Genv.find_funct_ptr.
+
constructor;
auto.
eapply match_stacks_free;
eauto.
+
setoid_rewrite SYMB.
now setoid_rewrite DEF.
+
setoid_rewrite SYMB'.
now setoid_rewrite DEF'.
}
*{
simpl in *.
unfold Genv.find_funct_ptr in *.
destruct (
Genv.find_symbol ge q)
eqn:
SYMB; [|
inv H8].
destruct (
Genv.find_def ge b)
as [[|]|]
eqn:
DEF;
inv H8.
assert ((
prog_defmap p)!.
q=
Some (
Gfun fd))
as DEFMAP.
{
eapply Genv.find_def_symbol.
eauto. }
edestruct (
match_prog_def _ _
TRANSL q)
as [| | |??
FIND1 FIND2|];
try congruence.
rewrite FIND1 in DEFMAP;
inv DEFMAP.
apply Genv.find_def_symbol in FIND2 as (?&
SYMB'&
DEF').
do 2
esplit; [
eapply plus_one|].
+
eapply exec_Itailcall;
eauto.
simpl.
*
unfold tge,
Genv.find_funct_ptr.
setoid_rewrite SYMB'.
setoid_rewrite DEF'.
reflexivity.
+
eapply match_callstates_unprot;
eauto.
eapply match_stacks_free;
eauto.
}
+
exploit eval_builtin_args_inject;
eauto using match_stacks_preserves_globals.
1:{
intros.
eapply max_reg_function_use in H7;
eauto. }
intros (?&
EVAL'&
INJL).
eapply Events.external_call_mem_inject_gen in H9 as EXT';
eauto.
2:
eapply globals_symbols_inject,
match_stacks_preserves_globals;
eauto 8.
destruct EXT' as (
inj&?&?&
EXT'&
VINJ&
MINJ&
MUNC1&
MUNC2&
INCR&
EINJ);
eauto.
do 2
esplit; [
eapply plus_one,
exec_Ibuiltin;
eauto|].
eapply match_states_unprot with (
j:=
inj);
eauto with ipcfc.
*
eapply match_stacks_incr,
match_stacks_mem_external_call,
STACKS;
eauto.
--
intros.
exploit EINJ;
eauto.
intros [
P Q].
unfold Mem.valid_block in *;
extlia.
*
apply Events.external_call_nextblock in H9.
extlia.
*
apply Events.external_call_nextblock in EXT'.
extlia.
*
eapply match_regs_incr in REGS;
eauto.
destruct res;
simpl;
eauto using match_regs_assign.
+
do 2
esplit; [
eapply plus_one|].
*
eapply exec_Icond;
eauto.
eapply eval_condition_inject;
eauto.
eapply match_regs_inject_list;
eauto.
intros.
eapply max_reg_function_use;
eauto.
*
econstructor;
eauto with ipcfc.
+
assert (
Val.inject j (
rs #
arg) (
rs' #
arg))
as INJ.
{
apply REGS.
eapply max_reg_function_use;
eauto.
simpl;
auto. }
rewrite H8 in INJ.
inv INJ.
do 2
esplit; [
eapply plus_one;
eauto|].
*
eapply exec_Ijumptable;
eauto.
*
econstructor;
eauto with ipcfc.
+
exploit Mem.free_parallel_inject;
eauto.
intros (
m2'&
FREE'&
MEMINJ2).
rewrite ?
Z.add_0_r in FREE'.
do 2
esplit; [
eapply plus_one|];
eauto with ipcfc.
econstructor;
eauto.
*
eapply match_stacks_free;
eauto.
*
destruct or;
simpl;
auto.
eapply REGS,
max_reg_function_use;
eauto.
simpl;
auto.
+
do 2
esplit; [
eapply plus_one|].
*
eapply eval_assert_args_inject in H8 as (?&?&?);
eauto.
2:{
intros.
eapply max_reg_function_use;
eauto. }
eapply exec_Iassert;
eauto.
eapply eval_condition_inject;
eauto.
*
econstructor;
eauto with ipcfc.
-
destruct TR as (
prot&
PROT&
TR).
assert (
meminj_preserves_globals j)
as PRES by eauto 8
using match_stacks_preserves_globals.
inv STEP;
eapply transf_prot_spec in TR as SPEC;
eauto.
all:
simpl in SPEC;
destruct SPEC as (?&?&
EQ&?);
repeat pMonadInv;
simpl in *;
inv_seq.
+
do 2
esplit;
eauto with ipcfc.
+
assert (
Val.inject_list j rs ##
args rs' ##
args)
as INJL.
{
eapply match_regs_inject_list;
eauto.
intros.
eapply max_reg_function_use;
eauto. }
eapply eval_operation_inj in H8 as (?&
OP&
INJ);
eauto with inject.
do 2
esplit; [
eapply plus_one|].
*
eapply exec_Iop;
eauto.
*
econstructor;
eauto with ipcfc.
--
eapply match_gsr_assign;
eauto.
eapply max_reg_function_def in H7;
simpl;
eauto.
extlia.
--
rewrite Regmap.gso;
eauto.
eapply max_reg_function_def in H7;
simpl;
eauto.
extlia.
--
rewrite Regmap.gso;
eauto.
eapply max_reg_function_def in H7;
simpl;
eauto.
extlia.
+
assert (
forall v,
match_gsr (
gsr f)
rs' #
dst <-
v m m' j bgsr vgsr)
as GSR'.
{
intros.
eapply match_gsr_assign;
eauto.
eapply max_reg_function_def in H7;
simpl;
eauto.
unfold gsr in *.
extlia. }
assert (
Val.inject_list j rs ##
args rs' ##
args)
as INJL.
{
eapply match_regs_inject_list;
eauto.
intros.
eapply max_reg_function_use;
eauto. }
inv H8.
*
eapply eval_addressing_inj in EVAL as (?&
EVAL'&
INJ);
eauto using symbol_address_inject.
exploit Mem.loadv_inject;
eauto.
intros (?&
LOAD'&
INJ').
do 2
esplit; [
eapply plus_one|].
--
eapply exec_Iload;
eauto using has_loaded_normal.
--
econstructor;
eauto with ipcfc.
all:
rewrite Regmap.gso;
auto;
eapply max_reg_function_def in H7;
simpl;
eauto;
extlia.
*
destruct eval_addressing eqn:
EVAL in LOAD.
specialize (
LOAD _
eq_refl).
eapply eval_addressing_inj in EVAL as (? &
EVAL'' &
INJ);
eauto using symbol_address_inject.
rewrite ptrofs_add_repr_zero in EVAL''.
destruct (
Mem.loadv chunk m' x0)
eqn:
LOAD';
auto.
all:
do 2
esplit; [
eapply plus_one,
exec_Iload|];
eauto using has_loaded_normal.
1,3,5:
econstructor;
eauto with ipcfc.
1-6:
erewrite Regmap.gso;
eauto;
eapply max_reg_function_def in H7;
simpl;
eauto;
extlia.
1,2:
eapply has_loaded_default;
eauto;
intros *
EVAL'.
--
rewrite EVAL'' in EVAL';
inv EVAL';
auto.
--
eapply eval_addressing_inj_none in EVAL;
eauto using symbol_address_inject.
rewrite ptrofs_add_repr_zero in EVAL.
congruence.
+
eapply eval_addressing_inj in H8 as (?&
EVAL'&
INJ);
eauto using symbol_address_inject.
2:{
eapply match_regs_inject_list;
eauto.
intros.
eapply max_reg_function_use;
eauto;
simpl;
auto. }
exploit Mem.storev_mapped_inject;
eauto.
1:{
eapply REGS.
eapply max_reg_function_use;
eauto.
simpl;
auto. }
intros (?&
STORE'&
MINJ').
do 2
esplit; [
eapply plus_one;
eauto|].
*
eapply exec_Istore;
eauto.
*
unfold Mem.storev in *.
destruct a,
x0;
try congruence.
econstructor;
eauto with ipcfc.
--
eapply match_stacks_mem;
eauto using STACKS.
all:
eauto using Mem.perm_store_1,
Mem.perm_store_2 with ipcfc.
intros *
LT1 LT2 LOC.
erewrite Mem.load_store_other;
eauto.
left;
intros ?;
subst.
inv INJ.
eapply LOC;
eauto.
instantiate (1:=(
Ptrofs.unsigned i)+
delta);
replace ((
Ptrofs.unsigned i) +
delta -
delta)
with (
Ptrofs.unsigned i)
by lia.
eapply Mem.store_needs_Writable in H9;
eauto using Mem.perm_implies,
perm_order.
--
erewrite Mem.nextblock_store;
eauto.
--
erewrite Mem.nextblock_store;
eauto.
--
eapply match_gsr_mem,
GSR;
eauto using Mem.perm_store_1,
Mem.perm_store_2.
++
intros *.
erewrite Mem.load_store_other;
eauto.
left;
intros ?;
subst.
inv INJ.
destruct GSR as (?&_&_&
OUT).
eapply OUT;
eauto.
instantiate (1:=
Ptrofs.unsigned i +
delta).
replace (
Ptrofs.unsigned i+
delta-
delta)
with (
Ptrofs.unsigned i)
by lia.
eapply Mem.perm_implies;
eauto using Mem.store_needs_Writable,
perm_order.
+
assert (
Val.inject_list j rs ##
args rs' ##
args)
as ARGS.
{
eapply match_regs_inject_list;
eauto.
intros.
eapply max_reg_function_use;
eauto.
destruct ros;
simpl;
auto. }
destruct ros;
simpl in *. 2:
destruct (
prot!.
q)
as [[]|]
eqn:
ISINTERNAL.
all:
repeat pMonadInv;
inv_seq.
*{
assert (
Val.inject j rs #
r rs' #
r)
as INJ.
{
eapply REGS,
max_reg_function_use;
eauto.
simpl;
auto. }
simpl in *.
destruct (
rs #
r);
simpl in *;
try congruence.
destruct (
Ptrofs.eq_dec i Ptrofs.zero); [|
congruence];
subst.
unfold Genv.find_funct_ptr in *.
destruct (
Genv.find_def ge b)
as [[]|]
eqn:
DEF;
inv H8.
eapply Genv.find_def_inversion_symbol in DEF as SYMB;
eauto using match_prog_norepet1.
destruct SYMB as (
q&
SYMB).
inversion INJ as [| | | |?????
J EQ1 EQ2 R'|];
subst;
clear INJ.
rewrite Ptrofs.add_zero_l in R'.
eapply defs_inject in J as (?&
SYMB'&
DEF'&
MATCH&?);
eauto;
subst.
inversion MATCH as [|?
FIND1 FIND2|??????
HARDEN' TR' TRC' SYMB'' DEF''];
subst;
clear MATCH.
1,2:(
do 2
esplit; [
eapply plus_one,
exec_Icall|]).
1,5:
eauto.
1,4:(
simpl;
unfold Genv.find_funct,
Genv.find_funct_ptr;
rewrite <-
R';
destruct (
Ptrofs.eq_dec _ _); [
now rewrite DEF'|
exfalso;
apply n;
reflexivity]).
1,3:
simpl;
auto;
eapply transf_init_prot_sig;
eauto.
-
econstructor;
eauto.
econstructor;
eauto with ipcfc.
+
eapply max_reg_function_def;
eauto.
+
destruct GSR as (?&
PERM&?&?).
eapply Mem.valid_access_implies,
Mem.valid_access_valid_block in PERM;
eauto using perm_order.
-
eapply match_callstates_init_prot;
eauto.
2,3:
intros;
simpl;
unfold Genv.find_funct_ptr.
+
eapply match_stacks_init_prot_cons2 with (
id:=
id);
eauto with ipcfc.
*
eapply max_reg_function_def;
eauto.
*
destruct GSR as (?&_&
GSRL&_).
eapply Mem.load_valid_access,
Mem.valid_access_implies,
Mem.valid_access_valid_block in GSRL;
eauto using perm_order.
+
now rewrite SYMB',
DEF'.
+
now rewrite SYMB'',
DEF''.
}
*{
unfold transf_call' in *.
repeat pMonadInv.
inv_seq.
eapply PROT,
protected_internal in ISINTERNAL as INPROGS.
destruct INPROGS as (?&
INPROGS).
simpl in *.
apply prog_defmap_norepet in INPROGS;
eauto using match_prog_norepet1.
assert (
fd =
Internal x0);
subst.
{
apply Genv.find_def_symbol in INPROGS as (?&
SYMB&
DEF).
unfold ge,
Genv.find_funct_ptr in *.
rewrite SYMB,
DEF in H8.
congruence. }
edestruct (
match_prog_def _ _
TRANSL q)
as [| | | |?????
HARDEN' FIND1 TR1 FIND2 (?&
PROT2&
TR2)
FIND3];
try congruence.
rewrite FIND1 in INPROGS.
inv INPROGS.
eapply Genv.find_def_symbol in FIND3 as DEF.
destruct DEF as (?&
SYMB&
DEF).
rewrite HARDEN' in MON;
inv MON.
do 2
esplit; [
plus_step 2;
try eapply plus_one|].
-
eapply exec_Iassert;
eauto.
+
repeat econstructor.
simpl.
destruct GSR as (
REG&_&
LOAD&_).
rewrite REG;
simpl.
rewrite Ptrofs.add_zero.
apply LOAD.
+
rewrite GSRV.
simpl.
now rewrite Int.eq_true.
-
eapply exec_Iop;
eauto.
simpl.
rewrite GSRV.
simpl.
reflexivity.
-
eapply exec_Icall;
eauto;
simpl.
+
unfold tge,
Genv.find_funct_ptr.
setoid_rewrite SYMB.
now setoid_rewrite DEF.
+
simpl.
erewrite transf_prot_sig;
eauto with ipcfc.
-
eapply match_callstates_prot;
eauto with ipcfc.
+
eapply match_stacks_prot_both with (
cid:=
id) (
id:=
q);
eauto with ipcfc.
*
eapply max_reg_function_def;
eauto.
*
apply match_regs_assign',
REGS;
extlia.
*
eapply match_gsr_assign;
eauto;
extlia.
*
destruct GSR as (?&
PERM&?).
eapply Mem.valid_access_implies,
Mem.valid_access_valid_block in PERM;
eauto using perm_order.
*
rewrite Regmap.gso;
eauto.
all:
extlia.
*
rewrite Regmap.gso;
eauto.
all:
extlia.
+
eapply match_regs_inject_list.
*
eapply match_regs_assign',
REGS.
extlia.
*
intros *
INARGS.
eapply max_reg_function_use in H7;
eauto.
+
eapply match_gsr_assign,
GSR.
extlia.
+
rewrite Regmap.gss.
simpl.
eauto.
}
*{
simpl in *.
unfold Genv.find_funct_ptr in *.
destruct (
Genv.find_symbol ge q)
eqn:
SYMB; [|
inv H8].
destruct (
Genv.find_def ge b)
as [[|]|]
eqn:
DEF;
inv H8.
assert ((
prog_defmap p)!.
q=
Some (
Gfun fd))
as DEFMAP.
{
eapply Genv.find_def_symbol.
eauto. }
edestruct (
match_prog_def _ _
TRANSL q)
as [| | |??
FIND1 FIND2|??????
FIND1 TR1 FIND2 TR2 FIND3];
try congruence.
+
rewrite FIND1 in DEFMAP;
inv DEFMAP.
apply Genv.find_def_symbol in FIND2 as (?&
SYMB'&
DEF').
do 2
esplit; [
eapply plus_one|].
*
eapply exec_Icall;
eauto.
simpl.
unfold tge,
Genv.find_funct_ptr.
setoid_rewrite SYMB'.
setoid_rewrite DEF'.
reflexivity.
*
eapply match_callstates_unprot;
eauto.
eapply match_stacks_unprot_cons2 with (
id:=
id);
eauto with ipcfc.
--
eapply max_reg_function_def;
eauto.
--
destruct GSR as (?&_&
GSRL&_).
eapply Mem.load_valid_access,
Mem.valid_access_implies,
Mem.valid_access_valid_block in GSRL;
eauto using perm_order.
+
rewrite FIND1 in DEFMAP;
inv DEFMAP.
apply Genv.find_def_symbol in FIND2 as (?&
SYMB'&
DEF').
do 2
esplit; [
eapply plus_one|].
*
eapply exec_Icall.
eauto.
simpl.
--
unfold tge,
Genv.find_funct_ptr.
setoid_rewrite SYMB'.
setoid_rewrite DEF'.
reflexivity.
--
simpl.
erewrite transf_init_prot_sig;
eauto.
*
eapply match_callstates_init_prot;
eauto.
eapply match_stacks_unprot_init_prot,
match_stacks_unprot_cons2 with (
id:=
id);
eauto with ipcfc.
--
eapply max_reg_function_def;
eauto.
--
destruct GSR as (?&_&
GSRL&_).
eapply Mem.load_valid_access,
Mem.valid_access_implies,
Mem.valid_access_valid_block in GSRL;
eauto using perm_order.
--
intros;
simpl.
unfold tge,
Genv.find_funct_ptr.
setoid_rewrite SYMB'.
now setoid_rewrite DEF'.
--
intros;
simpl.
unfold tge,
Genv.find_funct_ptr.
eapply Genv.find_def_symbol in FIND3 as (?&
SYMB''&
DEF'').
setoid_rewrite SYMB''.
now setoid_rewrite DEF''.
}
+
exploit eval_builtin_args_inject;
eauto using match_stacks_preserves_globals.
1:{
intros.
eapply max_reg_function_use in H7;
eauto. }
intros (?&
EVAL'&
INJL).
eapply Events.external_call_mem_inject_gen in H9 as EXT';
eauto.
2:
eapply globals_symbols_inject,
match_stacks_preserves_globals;
eauto 8.
destruct EXT' as (
inj&?&?&
EXT'&
VINJ&
MINJ&
MUNC1&
MUNC2&
INCR&
EINJ);
eauto.
do 2
esplit; [
eapply plus_one,
exec_Ibuiltin;
eauto|].
eapply match_states_prot with (
j:=
inj);
eauto with ipcfc.
*
eapply match_stacks_incr,
match_stacks_mem_external_call,
STACKS;
eauto.
--
intros.
exploit EINJ;
eauto.
intros [
P Q].
unfold Mem.valid_block in *;
extlia.
*
apply Events.external_call_nextblock in H9.
extlia.
*
apply Events.external_call_nextblock in EXT'.
extlia.
*
eapply match_regs_incr in REGS;
eauto.
destruct res;
simpl;
eauto using match_regs_assign.
*
eapply match_gsr_external_call;
eauto.
destruct res;
simpl;
eauto.
eapply match_gsr_assign;
eauto.
eapply max_reg_function_def in H7;
simpl;
eauto.
unfold gsr;
extlia.
*
destruct res;
simpl;
eauto.
rewrite Regmap.gso;
auto;
eapply max_reg_function_def in H7;
simpl;
eauto;
extlia.
*
destruct res;
simpl;
eauto.
rewrite Regmap.gso;
auto;
eapply max_reg_function_def in H7;
simpl;
eauto;
extlia.
+
do 2
esplit; [
plus_step 1;
try apply plus_one|].
*
eapply exec_Icond;
eauto.
eapply eval_condition_inject;
eauto.
eapply match_regs_inject_list;
eauto.
intros.
eapply max_reg_function_use;
eauto.
*
instantiate (1:=
if b then _
else _).
destruct b;
eapply exec_Inop;
eauto.
*
destruct b;
econstructor;
eauto with ipcfc.
+
assert (
Val.inject j (
rs #
arg) (
rs' #
arg))
as INJ.
{
apply REGS.
eapply max_reg_function_use;
eauto.
simpl;
auto. }
rewrite H8 in INJ.
inv INJ.
do 2
esplit; [
eapply plus_one;
eauto|].
*
eapply exec_Ijumptable;
eauto.
*
econstructor;
eauto with ipcfc.
+
destruct GSR as (
GSR&
GSRPERM&?&
GSRINJ).
eapply Mem.valid_access_store in GSRPERM as STORE'.
destruct STORE' as (
m1'&
STORE').
assert (
Mem.inject j m m1')
as MEMINJ1.
{
eapply Mem.store_outside_inject;
eauto.
intros *
J PERM OFF.
eapply GSRINJ;
eauto.
instantiate (1:=
ofs'+
delta).
replace (
ofs' +
delta -
delta)
with ofs' by lia.
eauto using Mem.perm_max,
Mem.perm_implies,
perm_order. }
apply plus_match_trans.
exploit Mem.free_parallel_inject;
eauto.
intros (
m2'&
FREE'&
MEMINJ2).
rewrite ?
Z.add_0_r in FREE'.
do 2
esplit; [
eapply plus_three;
repeat rewrite Events.E0_right;
auto|].
*
eapply exec_Iop;
eauto.
reflexivity.
*
eapply exec_Iop;
eauto.
simpl.
rewrite Regmap.gss,
GSRV,
RTS;
simpl.
rewrite Int.xor_assoc with (
z:=
vgsr),
Int.xor_idem,
Int.xor_zero.
reflexivity.
*
eapply exec_Istore;
eauto;
simpl.
--
rewrite ?
Regmap.gso;
try extlia.
rewrite GSR;
simpl;
rewrite ?
Ptrofs.add_zero;
reflexivity.
--
rewrite Regmap.gss.
apply STORE'.
*
assert (
bgsr <>
sp')
as NEQ.
{
inv STACKS;
extlia. }
destruct stk.
{
inv STACKS.
assert (
Mem.valid_access m2' Mint32 bgsr 0
Writable)
as PERM2.
{
eapply Mem.valid_access_free_1;
eauto.
eapply Mem.store_valid_access_1;
eauto. }
eapply Mem.valid_access_store in PERM2 as STORE2'.
destruct STORE2' as (
m3'&
STORE2').
assert (
Mem.range_perm m3' sp'0 0 (
fn_stacksize f'0)
Cur Freeable)
as SPPERM'.
{
intros ?
OFF.
specialize (
SPPERM _
OFF).
eapply Mem.perm_store_1,
Mem.perm_free_1,
Mem.perm_store_1;
eauto.
left;
extlia.
}
eapply Mem.range_perm_free in SPPERM' as (
m4'&
FREE2').
assert (
Mem.inject j m'0 m4')
as MEMINJ3.
{
eapply Mem.free_right_inject; [|
eauto|].
2:{
intros *
J PERM OFF.
erewrite transf_init_prot_stacksize in OFF;
eauto.
eapply SPOUT;
eauto.
replace (
ofs +
delta -
delta)
with ofs by lia.
eapply Mem.perm_free_3;
eauto using Mem.perm_max,
Mem.perm_implies,
perm_order. }
eapply Mem.store_outside_inject;
eauto.
intros *
J PERM OFF.
eapply GSRINJ;
eauto.
instantiate (1:=
ofs'+
delta).
replace (
ofs' +
delta -
delta)
with ofs' by lia.
eapply Mem.perm_free_3;
eauto using Mem.perm_max,
Mem.perm_implies,
perm_order. }
do 2
esplit; [
plus_step 6;
try apply plus_one|].
-
eapply exec_Ireturn;
eauto.
rewrite ?
Z.add_0_r in FREE'.
erewrite transf_prot_stacksize;
eauto.
-
eapply exec_return;
eauto.
-
eapply exec_Iload;
eauto.
econstructor;
simpl.
+
rewrite Regmap.gso,
GSR0; [|
extlia].
simpl.
now rewrite ?
Ptrofs.add_zero.
+
simpl.
setoid_rewrite Mem.load_free.
setoid_rewrite Mem.load_store_same. 2:
eapply STORE'.
all:
eauto.
-
eapply exec_Iop;
eauto.
simpl.
rewrite Regmap.gss.
simpl.
now rewrite Int.xor_assoc,
Int.xor_idem,
Int.xor_zero.
-
eapply exec_Icond with (
b:=
false);
eauto.
simpl.
rewrite Regmap.gss, ?
Regmap.gso,
GSRV0;
try extlia.
simpl.
now rewrite Int.eq_true.
-
eapply exec_Istore;
eauto;
simpl.
+
rewrite ?
Regmap.gso,
GSR0;
try extlia.
simpl.
now rewrite ?
Ptrofs.add_zero.
+
simpl.
rewrite ?
Regmap.gso,
GSRV0;
try extlia.
apply STORE2'.
-
eapply exec_Ireturn;
eauto.
-
eapply match_return_init_prot;
eauto.
+
inv STACKS0; [|
inv STACKS];
repeat (
constructor;
eauto).
*
erewrite Mem.nextblock_free;
eauto.
extlia.
*
erewrite Mem.nextblock_free,
Mem.nextblock_store,
Mem.nextblock_free with (
m1:=
m1'),
Mem.nextblock_store with (
m1:=
m');
eauto.
extlia.
*
erewrite Mem.nextblock_free;
eauto.
extlia.
*
erewrite Mem.nextblock_free,
Mem.nextblock_store,
Mem.nextblock_free with (
m1:=
m1'),
Mem.nextblock_store with (
m1:=
m');
eauto.
extlia.
+
destruct or;
simpl;
auto.
eapply max_reg_function_use in H7 as LE;
simpl;
eauto.
inv WTST.
inv WT_STK.
replace (
sig_res (
fn_sig f0))
with Xint by congruence;
simpl.
rewrite 2
Regmap.gso,
Regmap.gss, 2
Regmap.gso;
try extlia.
apply REGS;
auto.
}
{
do 2
esplit; [
apply plus_one|].
-
eapply exec_Ireturn;
eauto.
erewrite transf_prot_stacksize;
eauto.
-
eapply match_return_prot;
eauto;
try congruence.
+
eapply match_stacks_bound,
match_stacks_mem;
eauto using STACKS.
*
erewrite Mem.nextblock_free;
eauto.
extlia.
*
erewrite Mem.nextblock_free,
Mem.nextblock_store;
eauto.
extlia.
*
eauto using Mem.perm_free_3 with ipcfc.
*
intros ????
LT OUT PERM.
eapply Mem.perm_free_1,
Mem.perm_store_1,
PERM;
eauto;
extlia.
*
intros *
LT OUT.
erewrite Mem.load_free,
Mem.load_store_other;
eauto. 1,2:
left;
extlia.
+
intros VOID.
inv WTST.
eapply wt_instrs in H7;
eauto.
inv H7;
simpl;
auto;
congruence.
+
destruct or;
simpl; [|
constructor].
eapply max_reg_function_use in H7; [|
simpl;
eauto].
rewrite ?
Regmap.gso.
eapply REGS.
all:
extlia.
+
eapply Mem.valid_access_free_1;
eauto using Mem.store_valid_access_1.
+
erewrite Mem.load_free,
Mem.load_store_same;
eauto.
rewrite Int.xor_commut.
reflexivity.
+
intros ???
J PERM.
eapply GSRINJ;
eauto using Mem.perm_free_3.
}
+
do 2
esplit; [
eapply plus_one|
eauto with ipcfc].
eapply exec_Inop;
eauto.
-
inv STEP.
+
exploit Mem.alloc_parallel_inject;
eauto using Z.le_refl.
intros (
j'&?&?&
ALLOC'&
INJ'&
INCR&
NEXT&
NNEXT).
do 2
esplit; [
apply plus_one;
econstructor;
eauto using Val.has_argtype_list_inject|].
econstructor;
eauto.
2,3:
erewrite Mem.nextblock_alloc;
eauto.
*
eapply match_stacks_alloc;
eauto.
*
eapply Mem.alloc_result in H6;
subst.
extlia.
*
eapply Mem.alloc_result in ALLOC';
subst.
extlia.
*
eapply match_regs_init;
eauto using val_inject_list_incr.
+
eapply Events.external_call_mem_inject_gen in H5 as EXT';
eauto.
2:
eapply globals_symbols_inject,
match_stacks_preserves_globals;
eauto.
destruct EXT' as (
inj&?&?&
EXT'&
VINJ&
MINJ&
MUNC1&
MUNC2&
INCR&
EINJ);
eauto.
do 2
esplit; [
apply plus_one;
econstructor;
eauto|].
eapply match_return_unprot;
eauto.
*
eapply match_stacks_bound,
match_stacks_incr with j,
match_stacks_mem_external_call,
STACKS;
eauto using Events.external_call_nextblock.
all:
try exact Xvoid;
try exact xH;
try exact Int.zero;
try exact (
exist _ [
xH]
eq_refl).
intros.
exploit EINJ;
eauto.
intros [
P Q].
unfold Mem.valid_block in *;
extlia.
-
inv STEP.
exploit transf_init_prot_entry;
eauto.
intros (?&?&?&?);
simpl in *.
unfold transf_init_prot,
transf_call' in *.
repeat pMonadInv.
inv_seq.
rewrite HARD in MON;
inv MON.
assert (
stk0 =
Mem.nextblock m)
by (
eapply Mem.alloc_result;
eauto);
subst.
edestruct (
Mem.alloc m' 0 (
Memdata.size_chunk Mint32))
as (
m1'&
nb1')
eqn:
ALLOC1.
assert (
Mem.valid_access m1' Mint32 nb1' 0
Writable)
as PERM1.
{
eapply Mem.valid_access_freeable_any,
Mem.valid_access_alloc_same;
eauto.
1,2:
lia.
apply Z.divide_0_r.
}
edestruct (
Mem.valid_access_store m1' Mint32 nb1' 0 (
Vint (
hash_entry_sig id)))
as (?&
MSTORE);
eauto.
assert (
forall delta,
Events.loc_out_of_reach j m nb1' delta)
as SPOUT.
{
intros ???
INJ PERM .
apply Mem.fresh_block_alloc in ALLOC1.
eapply ALLOC1,
Mem.perm_valid_block,
Mem.perm_inject;
eauto. }
exploit protected_entry_step_simulation. 1,2:
eauto.
all:
cycle -1.
intros (?&
STEPS&
MATCH).
do 2
esplit; [
plus_step 7;
try apply STEPS|];
eauto.
+
econstructor.
*
erewrite transf_init_prot_sig;
eauto using Val.has_argtype_list_inject.
*
erewrite transf_init_prot_stacksize;
eauto.
+
eapply exec_Iop;
eauto.
reflexivity.
+
eapply exec_Istore;
eauto.
reflexivity.
simpl.
rewrite ?
Regmap.gss,
Ptrofs.add_zero.
simpl.
rewrite Ptrofs.unsigned_zero.
apply MSTORE.
+
eapply exec_Iop;
eauto.
simpl.
reflexivity.
+
eapply exec_Iassert;
eauto.
*
repeat econstructor.
setoid_rewrite Regmap.gss.
simpl.
rewrite ?
Ptrofs.add_zero.
eapply Mem.load_store_same;
eauto.
*
simpl.
rewrite Regmap.gso,
Regmap.gss; [|
extlia].
now rewrite Int.eq_true.
+
eapply exec_Iop;
eauto.
simpl.
rewrite Regmap.gso,
Regmap.gss;
try extlia.
simpl.
reflexivity.
+
destruct TR' as (?&?&?).
eapply exec_Icall;
eauto;
simpl.
*
rewrite FIND';
eauto using (
init_regs [] []).
*
eauto using transf_prot_sig.
+
instantiate (1:=
j).
intros ?
LE.
erewrite map_ext_in with (
g:=
fun x => _ #
x).
2:{
intros ?
IN.
apply max_reg_function_params in IN;
unfold Ple in *.
rewrite 3
Regmap.gso.
reflexivity.
all:
unfold rts,
gsrv,
gsr;
lia. }
erewrite transf_init_prot_params with (
f':=
f');
eauto.
eapply match_regs_init_twice;
eauto.
+
apply Mem.alloc_result in ALLOC1 as ?;
subst.
econstructor;
eauto with ipcfc.
*
eapply match_stacks_mem;
eauto using STACKS,
Pos.le_refl,
Int.zero,
Mem.perm_store_1,
Mem.perm_alloc_1 with ipcfc.
--
intros *
LT OUT.
erewrite Mem.load_store_other,
Mem.load_alloc_unchanged;
eauto.
left.
extlia.
*
erewrite Mem.nextblock_store with (
m2:=
x);
eauto.
erewrite Mem.nextblock_alloc with (
m2:=
m1');
eauto using Plt_succ.
*
intros ?
OFS.
eapply Mem.perm_store_1,
Mem.perm_alloc_2;
eauto.
erewrite transf_init_prot_stacksize in OFS;
eauto.
*
rewrite 1
Regmap.gso,
Regmap.gss;
simpl;
auto;
extlia.
*
reflexivity.
*
erewrite Mem.nextblock_store with (
m2:=
x);
eauto.
erewrite Mem.nextblock_alloc with (
m2:=
m1');
eauto using Plt_succ.
*
rewrite 2
Regmap.gso,
Regmap.gss;
auto.
all:
extlia.
+
eapply Mem.store_outside_inject; [| |
eauto];
eauto using Mem.alloc_right_inject.
intros.
eapply SPOUT;
eauto.
instantiate (1:=
ofs'+
delta).
replace (
ofs'+
delta-
delta)
with ofs' by lia.
eauto using Mem.perm_cur_max,
Mem.perm_implies,
perm_order.
+
apply Mem.alloc_result in ALLOC1;
subst.
split; [|
split; [|
split]];
eauto.
*
rewrite 1
Regmap.gso,
Regmap.gss;
try extlia.
simpl.
now rewrite Ptrofs.add_zero.
*
eapply Mem.store_valid_access_1;
eauto.
*
apply Mem.load_store_same in MSTORE.
eauto.
+
now rewrite Regmap.gss.
+
rewrite ?
regs_gsso.
2-4:
intros IN;
eapply max_reg_function_params in IN;
extlia.
erewrite transf_init_prot_params;
eauto.
match goal with
|
H:
Val.has_argtype_list _ _ |- _ =>
eapply Val.has_argtype_list_inject in H; [|
eauto]
end.
erewrite init_regs_gss;
eauto using check_params_norepet.
erewrite check_params_length;
eauto using list_forall2_length.
+
auto.
-
inv STEP.
assert (
stk0 =
Mem.nextblock m)
by (
eapply Mem.alloc_result;
eauto);
subst.
eapply protected_entry_step_simulation;
eauto.
+
apply match_regs_init;
auto.
+
eapply Val.has_argtype_list_inject;
eauto.
-
inv STEP.
inv STACKS.
+
do 2
esplit; [
eapply plus_one,
exec_return|];
eauto with ipcfc.
+
do 2
esplit; [
eapply plus_one,
exec_return|].
econstructor;
eauto with ipcfc.
*
eapply match_gsr_assign;
eauto.
extlia.
*
rewrite Regmap.gso;
auto.
extlia.
*
rewrite Regmap.gso;
auto.
extlia.
-
inv STEP.
inv STACKS.
inv STACKS0.
+
do 2
esplit; [
eapply plus_one,
exec_return|];
eauto.
econstructor;
eauto using match_regs_assign.
+
do 2
esplit; [
eapply plus_one,
exec_return|];
eauto.
econstructor;
eauto using match_regs_assign.
*
eapply match_gsr_assign;
eauto.
extlia.
*
rewrite Regmap.gso;
try extlia;
eauto.
*
rewrite Regmap.gso;
try extlia;
eauto.
+
do 2
esplit; [
eapply plus_one,
exec_return|];
eauto.
econstructor;
eauto using match_regs_assign.
*
eapply match_gsr_assign;
eauto.
extlia.
*
rewrite Regmap.gso;
try extlia;
eauto.
*
rewrite Regmap.gso;
try extlia;
eauto.
-
inv STEP.
inv STACKS; [|
inv STACKS0; [
inv STACKS|]].
+
eapply Mem.valid_access_store in GSRPERM as STORE'.
destruct STORE' as (
m2'&
STORE').
do 2
esplit; [
plus_step 5;
try apply plus_one|].
*
econstructor;
eauto.
*
eapply exec_Iload;
eauto.
econstructor;
simpl.
--
rewrite Regmap.gso; [|
extlia].
rewrite GSR;
simpl.
now rewrite ?
Ptrofs.add_zero.
--
simpl.
eauto.
*
eapply exec_Iop;
eauto.
simpl.
rewrite Regmap.gss;
eauto.
*
eapply exec_Icond with (
b:=
false);
eauto.
simpl.
rewrite Regmap.gss, ?
Regmap.gso,
GSRV;
simpl;
try extlia.
now rewrite Int.xor_commut, <-
Int.xor_assoc,
Int.xor_idem,
Int.xor_zero_l,
Int.eq_true.
*
eapply exec_Istore;
eauto;
simpl.
--
rewrite ?
Regmap.gso;
try extlia.
rewrite GSR;
simpl.
now rewrite ?
Ptrofs.add_zero.
--
simpl.
rewrite ?
Regmap.gso;
try extlia.
rewrite GSRV.
apply STORE'.
*
eapply exec_Inop;
eauto.
*
eapply match_states_prot with (
id:=
cid0);
eauto.
--
eapply match_stacks_mem;
eauto using STACKS0,
Mem.perm_store_1 with ipcfc.
intros *
LT OUT.
erewrite Mem.load_store_other;
eauto.
left;
extlia.
--
erewrite Mem.nextblock_store;
eauto.
--
apply match_regs_assign',
match_regs_assign',
match_regs_assign;
eauto.
all:
extlia.
--
eapply Mem.store_outside_inject;
eauto.
intros *
J PERM BOUNDS.
eapply GSROUT;
eauto.
instantiate (1:=
ofs'+
delta).
replace (
ofs'+
delta-
delta)
with ofs' by lia;
auto.
eauto using Mem.perm_cur_max,
Mem.perm_implies,
perm_any_N.
--
eapply match_gsr_assign,
match_gsr_assign,
match_gsr_assign;
eauto;
try extlia.
split; [|
split; [|
split]];
eauto using Mem.store_valid_access_1.
erewrite Mem.load_store_same;
eauto.
simpl.
auto.
--
rewrite ?
Regmap.gso;
eauto;
extlia.
--
rewrite ?
Regmap.gso;
eauto;
extlia.
+
eapply Mem.valid_access_store in GSRPERM as STORE'.
destruct STORE' as (
m2'&
STORE').
assert (
Mem.range_perm m2' sp' 0 (
fn_stacksize f')
Cur Freeable)
as SPPERM'.
{
intros ?
OFF.
specialize (
SPPERM _
OFF);
eauto using Mem.perm_store_1. }
eapply Mem.range_perm_free in SPPERM' as (
m3'&
FREE').
assert (
Mem.inject j m m3')
as MEMINJ3.
{
eapply Mem.free_right_inject; [|
eauto|].
2:{
intros *
J PERM OFF.
erewrite transf_init_prot_stacksize in OFF;
eauto.
eapply SPOUT;
eauto.
replace (
ofs +
delta -
delta)
with ofs by lia.
eauto using Mem.perm_max,
Mem.perm_implies,
perm_order. }
eapply Mem.store_outside_inject;
eauto.
intros *
J PERM BOUNDS.
eapply GSROUT;
eauto.
instantiate (1:=
ofs'+
delta).
replace (
ofs'+
delta-
delta)
with ofs' by lia;
auto.
eauto using Mem.perm_cur_max,
Mem.perm_implies,
perm_any_N.
}
do 2
esplit; [
plus_step 6;
try apply plus_one|].
*
econstructor;
eauto.
*
eapply exec_Iload;
eauto.
econstructor;
simpl.
--
rewrite Regmap.gso; [|
extlia].
rewrite GSR;
simpl.
now rewrite ?
Ptrofs.add_zero.
--
simpl.
eauto.
*
eapply exec_Iop;
eauto.
simpl.
rewrite Regmap.gss.
simpl.
now rewrite Int.xor_commut with (
y:=
vgsr),
Int.xor_assoc,
Int.xor_idem,
Int.xor_zero.
*
eapply exec_Icond with (
b:=
false);
eauto.
simpl.
rewrite Regmap.gss, ?
Regmap.gso,
GSRV;
simpl;
try extlia.
now rewrite Int.eq_true.
*
eapply exec_Istore;
eauto;
simpl.
--
rewrite ?
Regmap.gso;
try extlia.
rewrite GSR;
simpl.
now rewrite ?
Ptrofs.add_zero.
--
simpl.
rewrite ?
Regmap.gso;
try extlia.
rewrite GSRV.
apply STORE'.
*
eapply exec_Ireturn;
eauto.
*
eapply exec_return.
*
eapply match_states_unprot;
eauto.
--
eapply match_stacks_mem;
eauto using STACKS0 with ipcfc.
++
intros ???????.
eapply Mem.perm_free_1,
Mem.perm_store_1;
eauto.
left.
extlia.
++
intros.
erewrite Mem.load_free,
Mem.load_store_other;
eauto;
left;
extlia.
--
erewrite Mem.nextblock_free,
Mem.nextblock_store;
eauto.
extlia.
--
apply match_regs_assign;
auto.
simpl.
destruct (
sig_res (
fn_sig f0))
eqn:
SIG;
simpl.
all:
try rewrite 2
Regmap.gso,
Regmap.gss;
auto;
try extlia.
now rewrite WTV.
+
eapply Mem.valid_access_store in GSRPERM as STORE'.
destruct STORE' as (
m2'&
STORE').
assert (
Mem.range_perm m2' sp' 0 (
fn_stacksize f')
Cur Freeable)
as SPPERM'.
{
intros ?
OFF.
specialize (
SPPERM _
OFF);
eauto using Mem.perm_store_1. }
eapply Mem.range_perm_free in SPPERM' as (
m3'&
FREE').
assert (
Mem.inject j m m3')
as MEMINJ3.
{
eapply Mem.free_right_inject; [|
eauto|].
2:{
intros *
J PERM OFF.
erewrite transf_init_prot_stacksize in OFF;
eauto.
eapply SPOUT;
eauto.
replace (
ofs +
delta -
delta)
with ofs by lia.
eauto using Mem.perm_max,
Mem.perm_implies,
perm_order. }
eapply Mem.store_outside_inject;
eauto.
intros *
J PERM BOUNDS.
eapply GSROUT;
eauto.
instantiate (1:=
ofs'+
delta).
replace (
ofs'+
delta-
delta)
with ofs' by lia;
auto.
eauto using Mem.perm_cur_max,
Mem.perm_implies,
perm_any_N.
}
do 2
esplit; [
plus_step 6;
try apply plus_one|].
*
econstructor;
eauto.
*
eapply exec_Iload;
eauto.
econstructor;
simpl.
--
rewrite Regmap.gso; [|
extlia].
rewrite GSR;
simpl.
now rewrite ?
Ptrofs.add_zero.
--
simpl.
eauto.
*
eapply exec_Iop;
eauto.
simpl.
rewrite Regmap.gss.
simpl.
now rewrite Int.xor_commut, <-
Int.xor_assoc,
Int.xor_idem,
Int.xor_zero_l.
*
eapply exec_Icond with (
b:=
false);
eauto.
simpl.
rewrite Regmap.gss, ?
Regmap.gso,
GSRV;
simpl;
try extlia.
now rewrite Int.eq_true.
*
eapply exec_Istore;
eauto;
simpl.
--
rewrite ?
Regmap.gso;
try extlia.
rewrite GSR;
simpl.
now rewrite ?
Ptrofs.add_zero.
--
simpl.
rewrite ?
Regmap.gso;
try extlia.
rewrite GSRV.
apply STORE'.
*
eapply exec_Ireturn;
eauto.
*
eapply exec_return.
*
eapply match_states_prot;
eauto.
--
eapply match_stacks_mem;
eauto using STACKS0 with ipcfc.
++
intros ???????.
eapply Mem.perm_free_1,
Mem.perm_store_1;
eauto.
left.
extlia.
++
intros.
erewrite Mem.load_free,
Mem.load_store_other;
eauto;
left;
extlia.
--
erewrite Mem.nextblock_free,
Mem.nextblock_store;
eauto.
extlia.
--
apply match_regs_assign;
auto.
simpl.
destruct (
sig_res (
fn_sig f0))
eqn:
SIG;
simpl.
all:
try rewrite 2
Regmap.gso,
Regmap.gss;
auto;
try extlia.
now rewrite WTV.
--
eapply match_gsr_assign; [
extlia|].
eapply match_gsr_mem in GSR0;
eauto.
++
intros *.
destruct GSR0 as (?&?&?&
OUT).
erewrite Mem.load_free,
Mem.load_store_other;
eauto;
left;
extlia.
++
intros *
OFS OUT PERM.
eapply Mem.perm_free_1,
Mem.perm_store_1;
eauto.
left.
extlia.
--
rewrite ?
Regmap.gso;
eauto;
extlia.
--
rewrite ?
Regmap.gso;
eauto;
extlia.
+
eapply Mem.valid_access_store in GSRPERM as STORE'.
destruct STORE' as (
m2'&
STORE').
assert (
Mem.range_perm m2' sp' 0 (
fn_stacksize f')
Cur Freeable)
as SPPERM'.
{
intros ?
OFF.
specialize (
SPPERM _
OFF);
eauto using Mem.perm_store_1. }
eapply Mem.range_perm_free in SPPERM' as (
m3'&
FREE').
assert (
Mem.inject j m m3')
as MEMINJ3.
{
eapply Mem.free_right_inject; [|
eauto|].
2:{
intros *
J PERM OFF.
erewrite transf_init_prot_stacksize in OFF;
eauto.
eapply SPOUT;
eauto.
replace (
ofs +
delta -
delta)
with ofs by lia.
eauto using Mem.perm_max,
Mem.perm_implies,
perm_order. }
eapply Mem.store_outside_inject;
eauto.
intros *
J PERM BOUNDS.
eapply GSROUT;
eauto.
instantiate (1:=
ofs'+
delta).
replace (
ofs'+
delta-
delta)
with ofs' by lia;
auto.
eauto using Mem.perm_cur_max,
Mem.perm_implies,
perm_any_N.
}
do 2
esplit; [
plus_step 6;
try apply plus_one|].
*
econstructor;
eauto.
*
eapply exec_Iload;
eauto.
econstructor;
simpl.
--
rewrite Regmap.gso; [|
extlia].
rewrite GSR;
simpl.
now rewrite ?
Ptrofs.add_zero.
--
simpl.
eauto.
*
eapply exec_Iop;
eauto.
simpl.
rewrite Regmap.gss.
simpl.
now rewrite Int.xor_commut, <-
Int.xor_assoc,
Int.xor_idem,
Int.xor_zero_l.
*
eapply exec_Icond with (
b:=
false);
eauto.
simpl.
rewrite Regmap.gss, ?
Regmap.gso,
GSRV;
simpl;
try extlia.
now rewrite Int.eq_true.
*
eapply exec_Istore;
eauto;
simpl.
--
rewrite ?
Regmap.gso;
try extlia.
rewrite GSR;
simpl.
now rewrite ?
Ptrofs.add_zero.
--
simpl.
rewrite ?
Regmap.gso;
try extlia.
rewrite GSRV.
apply STORE'.
*
eapply exec_Ireturn;
eauto.
*
eapply exec_return.
*
eapply match_states_prot;
eauto.
--
eapply match_stacks_mem;
eauto using STACKS with ipcfc.
++
intros ???????.
eapply Mem.perm_free_1,
Mem.perm_store_1;
eauto.
left.
extlia.
++
intros.
erewrite Mem.load_free,
Mem.load_store_other;
eauto;
left;
extlia.
--
erewrite Mem.nextblock_free,
Mem.nextblock_store;
eauto.
extlia.
--
apply match_regs_assign;
auto.
simpl.
destruct (
sig_res (
fn_sig f0))
eqn:
SIG;
simpl.
all:
try rewrite 2
Regmap.gso,
Regmap.gss;
auto;
try extlia.
now rewrite WTV.
--
eapply match_gsr_assign;
try extlia.
eapply match_gsr_mem in GSR0;
eauto.
++
intros *.
destruct GSR0 as (?&?&?&
OUT).
erewrite Mem.load_free,
Mem.load_store_other;
eauto;
left;
extlia.
++
intros *
OFS OUT PERM.
eapply Mem.perm_free_1,
Mem.perm_store_1;
eauto.
left.
extlia.
--
rewrite ?
Regmap.gso;
eauto;
extlia.
--
rewrite ?
Regmap.gso;
eauto;
extlia.
Qed.
Correctness theorem
Theorem transf_program_correct:
forward_simulation (
semantics p) (
semantics tp).
Proof.
End IPCFC.
Linking
Transparent Linker_def Linker_fundef Linker_vardef.
Ltac destruct_conjs :=
repeat
match goal with
|
x:(_ * _) |- _ =>
destruct x
end.
Ltac inv_equalities :=
destruct_conjs;
repeat
match goal with
|
H:(_, _) = (_, _) |- _ =>
inv H
|
H:
Some _ =
Some _ |- _ =>
inv H
|
H:
None =
Some _ |- _ =>
inv H
|
H:
Some _ =
None |- _ =>
inv H
end.
Ltac simpl_In :=
repeat
match goal with
|
H:
In _ (
map _ _) |- _ =>
apply in_map_iff in H as (?&?
F&
H);
destruct_conjs
|
H:
In _ (
map_filter _ _) |- _ =>
apply map_filter_In in H as (?&?
PRED&
H);
destruct_conjs
|
H:
In _ (
QITree.elements _) |- _ =>
apply QITree.elements_complete in H
|
H:(
QITree_Properties.of_list _)!._ =
Some _ |- _ =>
apply QITree_Properties.in_of_list in H
end.
Ltac solve_In :=
simpl_In;
repeat
match goal with
| |-
In _ (
map _ _) =>
apply in_map_iff;
do 2
esplit;
eauto with datatypes
| |-
In _ (
map_filter _ _) =>
apply map_filter_In;
do 2
esplit;
eauto with datatypes
| |-
In _ (
QITree.elements _) =>
apply QITree.elements_correct
| |- (
QITree_Properties.of_list _)!._ =
Some _ =>
apply QITree_Properties.of_list_norepet
end.
Fact of_list_unit :
forall l x,
In x l ->
(
QITree_Properties.of_list (
map (
fun x => (
x,
tt))
l))!.
x =
Some tt.
Proof.
Fact map_filter_norepet_fst A B C :
forall (
f: (
A *
B) ->
option (
A *
C))
l,
(
forall a1 b a2 c,
f (
a1,
b) =
Some (
a2,
c) ->
a2 =
a1) ->
list_norepet (
map fst l) ->
list_norepet (
map fst (
map_filter f l)).
Proof.
intros * F ND.
induction l as [|(?&?)]; simpl in *; auto.
inv ND.
destruct (f (a, b)) as [(?&?)|] eqn:EQ; simpl; [constructor|]; eauto.
apply F in EQ; subst.
contradict H1. simpl_In; subst. eapply F in H1; subst.
solve_In; auto.
Qed.
Lemma prog_defmap_protected_None :
forall prog id,
(
prog_defmap prog)!.
id =
None ->
(
protected prog)!.
id =
None.
Proof.
Global Instance TransfLinkIPCFC :
TransfLink IPCFCproof.match_prog.
Proof.
red;
intros *
LINK MATCH1 MATCH2.
assert (
forall id f,
(
prog_defmap p1)!.
id =
Some (
Gfun (
Internal f)) \/ (
prog_defmap p2)!.
id =
Some (
Gfun (
Internal f)) ->
(
QITree.combine link_prog_merge (
prog_defmap p1) (
prog_defmap p2))!.
id =
Some (
Gfun (
Internal f)))
as LINKINTERNAL.
{
apply link_prog_inv in LINK as (
MAIN&
EQ&?);
subst.
intros * [
FIND|
FIND];
rewrite QITree.gcombine,
FIND;
auto;
[
destruct ((
prog_defmap p2)!.
id)
eqn:
FIND2|
destruct ((
prog_defmap p1)!.
id)
eqn:
FIND2];
auto.
all:
edestruct EQ as (_&_&?&
LINK);
eauto.
simpl in *.
all:
destruct g as [[|[]]|];
inv LINK;
auto.
}
assert (
forall id,
(
protected p1)!.
id =
Some tt \/ (
protected p2)!.
id =
Some tt ->
(
protected p)!.
id =
Some tt)
as PROT.
{
apply link_prog_inv in LINK as (
MAIN&
EQ&?);
subst.
unfold protected;
simpl.
intros ? [
PROT|
PROT];
simpl_In;
cases_eq;
try congruence;
simpl_In;
inv_equalities.
1,2:
assert ((
QITree_Properties.of_list
(
map (
fun x :
qualident => (
x,
tt)) (
prog_public p1 ++
prog_public p2)))!.
id =
Some tt)
as FILTER.
1,3:(
apply of_list_unit;
auto with datatypes).
1,2:
eapply prog_defmap_norepet in PRED;
auto; [|
now (
inv MATCH1;
inv MATCH2)].
1,2:(
apply QITree_Properties.of_list_norepet,
map_filter_In).
1,3:(
eapply map_filter_norepet_fst,
QITree.elements_keys_norepet;
intros;
cases;
inv_equalities;
auto).
1,2:
do 2
esplit; [
apply QITree.elements_correct,
LINKINTERNAL;
eauto|];
simpl.
all:
rewrite FILTER,
EQ3;
auto.
}
assert (
forall id, (
protected p1)!.
id =
None -> (
protected p2)!.
id =
None -> (
protected p)!.
id =
None)
as NPROT.
{
apply link_prog_inv in LINK as (
MAIN&
EQ&?);
subst.
unfold protected;
simpl.
intros *
N1 N2.
rewrite <-
QITree_Properties.not_in_of_list in *.
intros IN.
simpl_In.
cases_eq;
inv_equalities;
simpl_In;
inv_equalities.
rewrite QITree.gcombine in PRED;
auto.
destruct ((
prog_defmap p1)!.
e)
as [[[]|]|]
eqn:
GET1, ((
prog_defmap p2)!.
e)
as [[[]|]|]
eqn:
GET2;
simpl in *;
cases_eq;
inv_equalities.
-
edestruct EQ as (
PUB1&
PUB2&_);
eauto.
eapply in_prog_defmap in GET1.
eapply N1.
solve_In;
simpl. 2:
rewrite of_list_unit,
EQ3;
auto.
auto.
-
apply in_app_iff in EQ2 as [|].
+
eapply in_prog_defmap in GET1.
eapply N1.
solve_In;
simpl. 2:
rewrite of_list_unit,
EQ3;
auto.
auto.
+
eapply match_prog_public_in in H;
eauto.
simpl_In;
simpl in *;
subst.
eapply prog_defmap_norepet in H; [
congruence|];
eauto using match_prog_norepet1.
-
edestruct EQ as (
PUB1&
PUB2&_);
eauto.
eapply in_prog_defmap in GET2.
eapply N2.
solve_In;
simpl. 2:
rewrite of_list_unit,
EQ3;
auto.
auto.
-
apply in_app_iff in EQ2 as [|].
+
eapply match_prog_public_in in H;
eauto.
simpl_In;
simpl in *;
subst.
eapply prog_defmap_norepet in H; [
congruence|];
eauto using match_prog_norepet1.
+
eapply in_prog_defmap in GET2.
eapply N2.
solve_In;
simpl. 2:
rewrite of_list_unit,
EQ3;
auto.
auto.
}
assert (
forall id f f',
is_transf_function_prot p1 id f f' \/
is_transf_function_prot p2 id f f' ->
is_transf_function_prot p id f f')
as LINKPROTECTED.
{
intros * [
ISC|
ISC];
destruct ISC as (?&
IN&?); (
do 2
esplit; [|
eauto]);
eauto. }
apply link_prog_inv in LINK as (
MAIN&
EQ&?);
subst.
inversion MATCH1.
inversion MATCH2.
setoid_rewrite link_prog_succeeds.
-
do 2
esplit;
eauto.
constructor;
simpl;
auto.
+
congruence.
+
intros *
IN.
apply in_app_iff in IN as [
IN|
IN];
[
apply match_prog_public_in0 in IN|
apply match_prog_public_in1 in IN];
simpl_In;
simpl in *;
subst.
1,2:
apply prog_defmap_norepet in IN;
auto.
1:
destruct ((
prog_defmap p2)!.
id)
eqn:
GET. 3:
destruct ((
prog_defmap p1)!.
id)
eqn:
GET.
all:
try (
edestruct EQ as (_&_&(?&
LINK)); [
now eauto|
now eauto|]).
all:(
solve_In;
simpl;
auto;
rewrite QITree.gcombine,
IN,
GET;
simpl;
eauto).
+
unfold prog_defmap.
simpl.
intros id.
specialize (
match_prog_def0 id).
specialize (
match_prog_def1 id).
destruct (
QITree.get id (
prog_defmap p1))
as [[[]|]|]
eqn:
GET1,
(
QITree.get id (
prog_defmap p2))
as [[[]|]|]
eqn:
GET2;
inv match_prog_def0;
inv match_prog_def1;
unfold prog_defmap in *;
try congruence.
all:
repeat
match goal with
|
H: _ \/ _ |- _ =>
destruct H
|
H: _ /\ _ |- _ =>
destruct H
|
H:
exists _, _ |- _ =>
destruct H
|
H1: ?
x = _,
H2: ?
x = _ |- _ =>
rewrite H1 in H2;
inv H2
|
H1:
harden_name _ =
Errors.OK ?
id,
H2:
harden_name _ =
Errors.OK ?
id |- _ =>
eapply harden_name_inj in H1;
eauto;
subst
end;
try congruence.
Ltac match_solve EQ :=
unfold prog_defmap;
simpl;
rewrite ?
QITree_Properties.of_list_elements, ?
QITree.gcombine;
repeat (
match goal with
|
H: _=
None |- _ =>
rewrite H
|
H: _ =
Some _ |- _ =>
rewrite H
end);
auto.
all:
try (
edestruct EQ as (?&?&?&
LINK);
eauto; [
idtac];
try now inv LINK).
all:
try now (
exfalso;
qualident_not_prefix id).
all:
repeat
(
match goal with
|
ef:
external_function |- _ =>
destruct ef;
inv LINK; [
idtac]
end).
*
eapply match_def_unprot;
repeat match_solve EQ.
*
eapply match_def_prot;
eauto;
repeat match_solve EQ.
destruct ((
QITree_Properties.of_list (
prog_defs tp2))!.
id')
eqn:
GET;
try reflexivity.
eapply match_prog_harden_name_inv in GET as (?&?);
eauto.
unfold prog_defmap in *;
congruence.
*
eapply match_def_unprot;
repeat match_solve EQ.
eapply NPROT;
eauto using prog_defmap_protected_None.
*
eapply match_def_prot;
eauto;
repeat match_solve EQ.
destruct ((
QITree_Properties.of_list (
prog_defs tp2))!.
id')
eqn:
GET;
try reflexivity.
eapply match_prog_harden_name_inv in GET as (?&?);
eauto.
unfold prog_defmap in *;
congruence.
*
eapply match_def_unprot;
repeat match_solve EQ.
*
eapply match_def_prot;
eauto;
repeat match_solve EQ.
destruct ((
QITree_Properties.of_list (
prog_defs tp1))!.
id')
eqn:
GET;
try reflexivity.
eapply match_prog_harden_name_inv in GET as (?&?);
eauto.
unfold prog_defmap in *;
congruence.
*
simpl in *.
destruct (
external_function_eq e e0)
eqn:
EXT;
inv LINK.
eapply match_def_unprot;
repeat match_solve EQ;
rewrite EXT;
eauto.
*
eapply match_def_unprot;
repeat match_solve EQ.
eapply NPROT;
eauto using prog_defmap_protected_None.
*
simpl in *.
destruct (
link_vardef v1 v2)
eqn:
LINKV;
inv LINK.
eapply match_def_var;
repeat match_solve EQ;
simpl;
now rewrite LINKV.
*
eapply match_def_var;
repeat match_solve EQ.
*
eapply match_def_unprot;
repeat match_solve EQ.
eapply NPROT;
eauto using prog_defmap_protected_None.
*
eapply match_def_prot;
eauto;
repeat match_solve EQ.
destruct ((
QITree_Properties.of_list (
prog_defs tp1))!.
id')
eqn:
GET;
try reflexivity.
eapply match_prog_harden_name_inv in GET as (?&?);
eauto.
unfold prog_defmap in *.
congruence.
*
eapply match_def_unprot;
repeat match_solve EQ.
eapply NPROT;
eauto using prog_defmap_protected_None.
*
eapply match_def_var;
repeat match_solve EQ.
*
eapply match_def_none1;
repeat match_solve EQ.
*
eapply match_def_none2;
eauto;
repeat match_solve EQ.
destruct ((
QITree_Properties.of_list (
prog_defs p1))!.
id')
eqn:
GET;
try reflexivity.
edestruct (
EQ id')
as (?&?&?&
LINK);
eauto.
setoid_rewrite LINK.
destruct g as [[|[]]|];
simpl in *;
inv LINK;
auto.
*
eapply match_def_none2;
eauto;
repeat match_solve EQ.
destruct ((
QITree_Properties.of_list (
prog_defs p2))!.
id')
eqn:
GET;
try reflexivity.
edestruct (
EQ id')
as (?&?&?&
LINK);
eauto.
setoid_rewrite LINK.
destruct g as [[|[]]|];
simpl in *;
inv LINK;
auto.
+
intros *
HARD FIND.
apply in_prog_defmap,
QITree.elements_complete in FIND;
simpl in *.
rewrite QITree.gcombine in FIND;
auto.
destruct
((
prog_defmap tp1)!.
id)
as [[|]|]
eqn:
FIND1,
((
prog_defmap tp2)!.
id)
as [[|]|]
eqn:
FIND2;
simpl in *;
try (
now inv FIND).
*
destruct f,
f0;
simpl in *;
inv FIND.
1,2:
destruct e;
inv H0.
--
eapply match_prog_inv0 in FIND1 as (
f&
FIND');
eauto 8
using prog_defmap_norepet,
QITree.elements_correct,
QITree.elements_keys_norepet.
--
eapply match_prog_inv1 in FIND2 as (
f&
FIND');
eauto 8
using prog_defmap_norepet,
QITree.elements_correct,
QITree.elements_keys_norepet.
--
destruct (
external_function_eq _ _);
simpl in *;
inv H0.
*
inv FIND.
eapply match_prog_inv0 in FIND1 as (
f&
FIND');
eauto 8
using prog_defmap_norepet,
QITree.elements_correct,
QITree.elements_keys_norepet.
*
cases;
inv FIND.
*
inv FIND.
eapply match_prog_inv1 in FIND2 as (
f&
FIND');
eauto 8
using prog_defmap_norepet,
QITree.elements_correct,
QITree.elements_keys_norepet.
+
intros ??
IN;
simpl in *.
apply QITree.elements_complete in IN.
rewrite QITree.gcombine in IN;
auto.
destruct ((
prog_defmap p1)!.
i)
as [|]
eqn:
P1,
((
prog_defmap p2)!.
i)
as [|]
eqn:
P2;
simpl in IN;
try congruence;
repeat
match goal with
|
H:
Some _ =
Some _ |- _ =>
inv H
|
H:(
prog_defmap _)!._ =
Some _ |- _ =>
apply in_prog_defmap in H
end;
eauto.
destruct g,
g0;
simpl in *;
try now inv IN.
*
destruct f0 as [|],
f1 as [|];
simpl in *;
try congruence.
1,2:
destruct e;
inv IN;
eauto.
destruct (
external_function_eq _ _);
inv IN;
eauto.
*
destruct (
link_vardef _ _);
inv IN.
+
unfold prog_defs_names.
simpl.
apply QITree.elements_keys_norepet.
+
unfold prog_defs_names.
simpl.
apply QITree.elements_keys_norepet.
+
intros *
IN.
apply in_map_iff in IN as ((?&?)&?&
IN);
subst.
apply QITree.elements_complete in IN.
rewrite QITree.gcombine in IN;
auto.
destruct (
QITree.get q (
prog_defmap p1))
eqn:
P1, (
QITree.get q (
prog_defmap p2))
eqn:
P2;
simpl in *;
try now (
inv IN).
all:
qualident_not_prefix q.
-
congruence.
-
intros *
EQ1 EQ2.
specialize (
match_prog_def0 id).
specialize (
match_prog_def1 id).
inv match_prog_def0;
inv match_prog_def1;
repeat
match goal with
|
H: _ \/ _ |- _ =>
destruct H
|
H: _ /\ _ |- _ =>
destruct H
|
H:
exists _, _ |- _ =>
destruct H
|
H1:
harden_name _ =
Errors.OK ?
id,
H2:
harden_name _ =
Errors.OK ?
id |- _ =>
eapply harden_name_inj in H1;
eauto;
subst
|
H1: ?
x = _,
H2: ?
x = _ |- _ =>
rewrite H1 in H2;
inv H2
|
H1:
QITree.get ?
id (
prog_defmap p1) =
Some _,
H2:
QITree.get ?
id (
prog_defmap p2) =
Some _ |- _ =>
specialize (
EQ id _ _
H1 H2)
as (?
P1&?
P2&?&?
LINK);
simpl in *;
try now inv LINK
|
H1:
harden_name _ =
Errors.OK ?
id |- _ =>
exfalso;
now (
qualident_not_prefix id)
end;
try congruence.
all:
repeat split;
auto;
try congruence.
+
destruct f as [|[]];
inv LINK;
intros LINK';
inv LINK'.
+
destruct f0 as [|[]];
inv LINK;
intros LINK';
inv LINK'.
Qed.