Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
FP
Stacked Borrows Coq
Commits
15c4ca51
Commit
15c4ca51
authored
Jul 08, 2019
by
Ralf Jung
Browse files
Merge branch 'master' of gitlab.mpi-sws.org:FP/stacked-borrows
parents
2a1adda1
c41ed90f
Changes
6
Hide whitespace changes
Inline
Side-by-side
theories/sim/instance.v
View file @
15c4ca51
...
...
@@ -93,6 +93,10 @@ Proof.
-
intros
[
VREL
?
].
subst
.
apply
vrel_eq
in
VREL
.
by
simplify_eq
.
Qed
.
Lemma
vrel_rrel
r
(
v1
v2
:
value
)
:
vrel
r
v1
v2
→
rrel
vrel
r
#
v1
#
v2
.
Proof
.
done
.
Qed
.
Lemma
rrel_mono
(
r1
r2
:
resUR
)
(
VAL
:
✓
r2
)
:
r1
≼
r2
→
∀
v1
v2
,
rrel
vrel
r1
v1
v2
→
rrel
vrel
r2
v1
v2
.
Proof
.
...
...
@@ -113,6 +117,10 @@ Proof.
have
Eq2
:=
to_of_result
e
.
rewrite
Eq1
/=
in
Eq2
.
by
simplify_eq
.
Qed
.
Lemma
list_Forall_result_value_2
(
vs
:
list
value
)
:
of_result
<
$
>
(
ValR
<
$
>
vs
)
=
Val
<
$
>
vs
.
Proof
.
by
rewrite
-
list_fmap_compose
.
Qed
.
Lemma
list_Forall_rrel_vrel
r
(
es
et
:
list
result
)
:
Forall2
(
rrel
vrel
r
)
es
et
→
Forall
(
λ
ei
:
expr
,
is_Some
(
to_value
ei
))
(
of_result
<
$
>
es
)
→
...
...
@@ -128,3 +136,50 @@ Proof.
by
rewrite
->
Forall2_fmap
in
RREL
.
Qed
.
Lemma
rrel_to_value
r
(
v1
:
value
)
e2
:
rrel
vrel
r
#
v1
e2
→
∃
(
v2
:
value
),
e2
=
v2
.
Proof
.
destruct
e2
;
[
|
done
].
by
eexists
.
Qed
.
Lemma
list_Forall_rrel_to_value
r
vs
et
:
Forall2
(
rrel
vrel
r
)
(
ValR
<
$
>
vs
)
et
→
∃
vt
,
et
=
ValR
<
$
>
vt
∧
Forall
(
λ
ei
:
expr
,
is_Some
(
to_value
ei
))
(
of_result
<
$
>
et
).
Proof
.
revert
vs
.
induction
et
as
[
|
e
et
IH
];
intros
vs
.
{
intros
Eq
%
Forall2_nil_inv_r
.
apply
fmap_nil_inv
in
Eq
.
subst
.
simpl
.
by
exists
[].
}
destruct
vs
as
[
|
v
vs
];
[
by
intros
Eq
%
Forall2_nil_inv_l
|
].
rewrite
!
fmap_cons
.
inversion
1
as
[
|????
RREL
REST
];
simplify_eq
.
apply
rrel_to_value
in
RREL
as
[
vt
?
].
apply
IH
in
REST
as
[
vts
[
?
?
]].
subst
e
et
.
exists
(
vt
::
vts
).
rewrite
fmap_cons
.
split
;
[
done
|
].
constructor
;
[
|
done
].
by
eexists
.
Qed
.
Lemma
list_Forall_rrel_vrel_2
r
(
es
et
:
list
result
)
:
Forall2
(
rrel
vrel
r
)
es
et
→
Forall
(
λ
ei
:
expr
,
is_Some
(
to_value
ei
))
(
of_result
<
$
>
es
)
→
∃
vs
vt
,
es
=
ValR
<
$
>
vs
∧
et
=
ValR
<
$
>
vt
∧
Forall
(
λ
ei
:
expr
,
is_Some
(
to_value
ei
))
(
of_result
<
$
>
et
)
∧
Forall2
(
vrel
r
)
vs
vt
.
Proof
.
intros
RREL
VRELs
.
have
VRELs
'
:=
VRELs
.
apply
list_Forall_to_value
in
VRELs
'
as
[
vs
Eqs
].
apply
list_Forall_result_value
in
Eqs
.
subst
es
.
destruct
(
list_Forall_rrel_to_value
_
_
_
RREL
)
as
[
vt
[
?
VRELt
]].
subst
.
destruct
(
list_Forall_rrel_vrel
_
_
_
RREL
VRELs
VRELt
)
as
(
vs
'
&
vt
'
&
Eq1
&
Eq2
&
?
).
by
exists
vs
'
,
vt
'
.
Qed
.
Lemma
list_Forall_rrel_vrel_3
r
(
vs
:
list
value
)
(
et
:
list
result
)
:
Forall2
(
rrel
vrel
r
)
(
ValR
<
$
>
vs
)
et
→
Forall
(
λ
ei
:
expr
,
is_Some
(
to_value
ei
))
(
Val
<
$
>
vs
)
→
∃
vt
,
et
=
ValR
<
$
>
vt
∧
Forall
(
λ
ei
:
expr
,
is_Some
(
to_value
ei
))
(
Val
<
$
>
vt
)
∧
Forall2
(
vrel
r
)
vs
vt
.
Proof
.
rewrite
-
list_Forall_result_value_2
.
intros
RREL
VRELs
.
destruct
(
list_Forall_rrel_vrel_2
_
_
_
RREL
VRELs
)
as
(
vs1
&
vt
&
Eqvs1
&
?
&
FA
&
?
).
subst
.
rewrite
list_Forall_result_value_2
in
FA
.
exists
vt
.
split
;
[
done
|
].
apply
Inj_instance_6
in
Eqvs1
;
[
by
subst
|
].
intros
??
.
by
inversion
1.
Qed
.
theories/sim/local.v
View file @
15c4ca51
...
...
@@ -54,15 +54,15 @@ Inductive _sim_local_body_step (r_f : A) (sim_local_body : SIM)
(
*
[
rv
]
justifies
the
arguments
*
)
(
VREL
:
Forall2
(
rrel
rv
)
vl_src
vl_tgt
)
(
*
and
after
the
call
our
context
can
continue
*
)
(
CONT
:
∀
r
'
r
_src
r
_tgt
σ
s
'
σ
t
'
(
*
For
any
new
resource
r
'
that
supports
the
returned
result
s
are
related
w
.
r
.
t
.
(
r
⋅
r
'
⋅
r_f
)
*
)
(
VRET
:
r
rel
r
'
r
_src
r
_tgt
)
(
CONT
:
∀
r
'
v
_src
v
_tgt
σ
s
'
σ
t
'
(
*
For
any
new
resource
r
'
that
supports
the
returned
value
s
are
related
w
.
r
.
t
.
r
'
*
)
(
VRET
:
v
rel
r
'
v
_src
v
_tgt
)
(
WSAT
:
wsat
(
r_f
⋅
(
rc
⋅
r
'
))
σ
s
'
σ
t
'
)
(
STACK
:
σ
t
.(
scs
)
=
σ
t
'
.(
scs
)),
∃
idx
'
,
sim_local_body
(
rc
⋅
r
'
)
idx
'
(
fill
Ks
(
of_result
r
_src
))
σ
s
'
(
fill
Kt
(
of_result
r
_tgt
))
σ
t
'
Φ
).
(
fill
Ks
(
Val
v
_src
))
σ
s
'
(
fill
Kt
(
Val
v
_tgt
))
σ
t
'
Φ
).
Record
sim_local_body_base
(
r_f
:
A
)
(
sim_local_body
:
SIM
)
(
r
:
A
)
(
idx
:
nat
)
es
σ
s
et
σ
t
Φ
:
Prop
:=
{
...
...
theories/sim/local_adequacy.v
View file @
15c4ca51
...
...
@@ -46,12 +46,12 @@ Inductive sim_local_frames:
our
local
resource
r
and
have
world
satisfaction
*
)
(
WSAT
'
:
wsat
(
r_f
⋅
(
frame
.(
rc
)
⋅
r
'
))
σ
_
src
'
σ
_
tgt
'
)
(
*
and
the
returned
values
are
related
w
.
r
.
t
.
(
r
⋅
r
'
⋅
r_f
)
*
)
(
VRET
:
rrel
vrel
r
'
v_src
v_tgt
)
(
VRET
:
vrel
r
'
v_src
v_tgt
)
(
CIDS
:
σ
_
tgt
'
.(
scs
)
=
frame
.(
callids
)),
∃
idx
'
,
sim_local_body
wsat
vrel
fns
fnt
(
frame
.(
rc
)
⋅
r
'
)
idx
'
(
fill
frame
.(
K_src
)
(
of_result
v_src
))
σ
_
src
'
(
fill
frame
.(
K_tgt
)
(
of_result
v_tgt
))
σ
_
tgt
'
(
fill
frame
.(
K_src
)
(
Val
v_src
))
σ
_
src
'
(
fill
frame
.(
K_tgt
)
(
Val
v_tgt
))
σ
_
tgt
'
(
λ
r
_
vs
σ
s
vt
σ
t
,
(
∃
c
,
σ
t
.(
scs
)
=
c
::
cids
∧
end_call_sat
r
c
)
∧
rrel
vrel
r
vs
vt
))
...
...
theories/sim/program.v
View file @
15c4ca51
...
...
@@ -30,7 +30,7 @@ Proof.
-
eapply
(
sim_body_step_over_call
_
_
init_res
ε
_
_
[]
[]);
[
done
|
..].
{
intros
fid
fn_src
.
specialize
(
FUNS
fid
fn_src
).
naive_solver
.
}
intros
.
simpl
.
exists
1
%
nat
.
apply
sim_body_result
.
apply
(
sim_body_result
_
_
_
_
(
ValR
vs
)
(
ValR
vt
))
.
intros
VALID
.
have
?:
rrel
vrel
(
init_res
⋅
r
'
)
vs
vt
.
{
eapply
rrel_mono
;
[
done
|
apply
cmra_included_r
|
exact
VRET
].
}
...
...
theories/sim/refl_pure_step.v
View file @
15c4ca51
...
...
@@ -9,21 +9,27 @@ Set Default Proof Using "Type".
(
**
Call
-
step
over
*
)
Lemma
sim_body_step_over_call
fs
ft
rc
rv
n
fid
v
ls
v
lt
σ
s
σ
t
Φ
(
V
REL
:
Forall2
(
vrel
rv
)
v
ls
v
lt
)
rc
rv
n
fid
r
ls
r
lt
σ
s
σ
t
Φ
(
R
REL
:
Forall2
(
rrel
vrel
rv
)
r
ls
r
lt
)
(
FUNS
:
sim_local_funs_lookup
fs
ft
)
:
(
∀
r
'
vs
vt
σ
s
'
σ
t
'
(
VRET
:
rrel
vrel
r
'
vs
vt
)
(
∀
r
'
vls
vlt
vs
vt
σ
s
'
σ
t
'
(
VRET
:
vrel
r
'
vs
vt
)
(
STACKS
:
σ
s
.(
scs
)
=
σ
s
'
.(
scs
))
(
STACKT
:
σ
t
.(
scs
)
=
σ
t
'
.(
scs
)),
∃
n
'
,
rc
⋅
r
'
⊨
{
n
'
,
fs
,
ft
}
(
of_result
vs
,
σ
s
'
)
≥
(
of_result
vt
,
σ
t
'
)
:
Φ
)
→
(
STACKT
:
σ
t
.(
scs
)
=
σ
t
'
.(
scs
))
(
Eqvls
:
rls
=
ValR
<
$
>
vls
)
(
Eqvlt
:
rlt
=
ValR
<
$
>
vlt
),
∃
n
'
,
rc
⋅
r
'
⊨
{
n
'
,
fs
,
ft
}
(
Val
vs
,
σ
s
'
)
≥
(
Val
vt
,
σ
t
'
)
:
Φ
)
→
rc
⋅
rv
⊨
{
n
,
fs
,
ft
}
(
Call
#[
ScFnPtr
fid
]
(
Val
<
$
>
v
ls
),
σ
s
)
≥
(
Call
#[
ScFnPtr
fid
]
(
Val
<
$
>
v
lt
),
σ
t
)
:
Φ
.
(
Call
#[
ScFnPtr
fid
]
(
of_result
<
$
>
r
ls
),
σ
s
)
≥
(
Call
#[
ScFnPtr
fid
]
(
of_result
<
$
>
r
lt
),
σ
t
)
:
Φ
.
Proof
.
intros
CONT
.
pfold
.
intros
NT
r_f
WSAT
.
edestruct
NT
as
[[]
|
[
e2
[
σ
2
RED
]]];
[
constructor
1
|
done
|
].
apply
tstep_call_inv
in
RED
;
last
first
.
{
apply
list_Forall_to_value
.
eauto
.
}
destruct
RED
as
(
xls
&
ebs
&
HCs
&
ebss
&
Eqfs
&
Eqss
&
?
&
?
).
subst
e2
σ
2.
apply
tstep_call_inv_result
in
RED
;
last
by
apply
list_Forall_to_of_result
.
destruct
RED
as
(
xls
&
ebs
&
HCs
&
ebss
&
Eqfs
&
Eqss
&
?
&
?
&
VALs
).
have
VALs
'
:=
VALs
.
apply
list_Forall_to_value
in
VALs
'
as
[
vls
Eqvls
].
subst
.
rewrite
Eqvls
.
rewrite
Eqvls
in
VALs
,
Eqss
.
apply
list_Forall_result_value
in
Eqvls
.
subst
rls
.
destruct
(
list_Forall_rrel_vrel_3
_
_
_
RREL
VALs
)
as
(
vlt
&
?
&
VALt
&
VREL
).
subst
rlt
.
destruct
(
FUNS
_
_
Eqfs
)
as
([
xlt
ebt
HCt
]
&
Eqft
&
Eql
).
simpl
in
Eql
.
destruct
(
subst_l_is_Some
xlt
(
Val
<
$
>
vlt
)
ebt
)
as
[
est
Eqst
].
...
...
@@ -31,15 +37,14 @@ Proof.
(
subst_l_is_Some_length
_
_
_
_
Eqss
)
fmap_length
//. }
split
;
[
|
done
|
].
{
right
.
exists
(
EndCall
(
InitCall
est
)),
σ
t
.
eapply
(
head_step_fill_tstep
_
[]).
econstructor
.
econstructor
;
try
done
.
apply
list_Forall_to_value
.
eauto
.
}
eapply
(
head_step_fill_tstep
_
[]).
econstructor
.
econstructor
;
try
done
;
rewrite
list_Forall_result_value_2
//
. }
eapply
(
sim_local_body_step_over_call
_
_
_
_
_
_
_
_
_
_
_
_
_
[]
[]
fid
(
ValR
<
$
>
vlt
)
(
ValR
<
$
>
vls
));
eauto
.
{
by
rewrite
of_result_list_expr
.
}
{
by
rewrite
of_result_list_expr
.
}
{
eapply
Forall2_fmap
,
Forall2_impl
;
eauto
.
}
intros
r
'
?
?
σ
s
'
σ
t
'
VR
WSAT
'
STACK
.
destruct
(
CONT
_
_
_
σ
s
'
σ
t
'
VR
)
as
[
n
'
?
];
[
|
done
|
exists
n
'
;
by
left
].
destruct
(
CONT
r
'
vls
vlt
v_src
v_tgt
σ
s
'
σ
t
'
)
as
[
n
'
?
];
[
by
apply
vrel_rrel
|
|
done
..
|
exists
n
'
;
by
left
].
destruct
WSAT
as
(
?&?&?&?&?&
SREL
&?
).
destruct
SREL
as
(
?&?&?
Eqcss
&?
).
destruct
WSAT
'
as
(
?&?&?&?&?&
SREL
'
&?
).
destruct
SREL
'
as
(
?&?&?
Eqcss
'
&?
).
by
rewrite
Eqcss
'
Eqcss
.
...
...
theories/sim/simple.v
View file @
15c4ca51
...
...
@@ -136,14 +136,16 @@ Qed.
(
*
[
Val
<
$
>
_
]
in
the
goal
makes
this
not
work
with
[
apply
],
but
we
'
d
need
tactic
support
for
anything
better
.
*
)
Lemma
sim_simple_call
n
'
v
ls
v
lt
rv
fs
ft
r
r
'
n
fid
css
cst
Φ
:
Lemma
sim_simple_call
n
'
r
ls
r
lt
rv
fs
ft
r
r
'
n
fid
css
cst
Φ
:
sim_local_funs_lookup
fs
ft
→
Forall2
(
vrel
rv
)
v
ls
v
lt
→
Forall2
(
rrel
vrel
rv
)
r
ls
r
lt
→
r
≡
r
'
⋅
rv
→
(
∀
rret
vs
vt
,
rrel
vrel
rret
vs
vt
→
r
'
⋅
rret
⊨ˢ
{
n
'
,
fs
,
ft
}
(
of_result
vs
,
css
)
≥
(
of_result
vt
,
cst
)
:
Φ
)
→
(
∀
rret
vs
vt
vls
vlt
,
rls
=
ValR
<
$
>
vls
→
rlt
=
ValR
<
$
>
vlt
→
vrel
rret
vs
vt
→
r
'
⋅
rret
⊨ˢ
{
n
'
,
fs
,
ft
}
(
Val
vs
,
css
)
≥
(
Val
vt
,
cst
)
:
Φ
)
→
r
⊨ˢ
{
n
,
fs
,
ft
}
(
Call
#[
ScFnPtr
fid
]
(
Val
<
$
>
v
ls
),
css
)
≥
(
Call
#[
ScFnPtr
fid
]
(
Val
<
$
>
v
lt
),
cst
)
:
Φ
.
(
Call
#[
ScFnPtr
fid
]
(
of_result
<
$
>
r
ls
),
css
)
≥
(
Call
#[
ScFnPtr
fid
]
(
of_result
<
$
>
r
lt
),
cst
)
:
Φ
.
Proof
.
intros
Hfns
Hrel
Hres
HH
σ
s
σ
t
<-<-
.
rewrite
Hres
.
apply:
sim_body_step_over_call
.
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment