Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
R
ReLoC-v1
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
1
Issues
1
List
Boards
Labels
Service Desk
Milestones
Merge Requests
0
Merge Requests
0
CI / CD
CI / CD
Pipelines
Jobs
Schedules
Operations
Operations
Incidents
Environments
Analytics
Analytics
CI / CD
Repository
Value Stream
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Jobs
Commits
Issue Boards
Open sidebar
Dan Frumin
ReLoC-v1
Commits
3447371d
Commit
3447371d
authored
Apr 09, 2018
by
Dan Frumin
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Simplify some example proofs
parent
752493b6
Changes
4
Hide whitespace changes
Inline
Side-by-side
Showing
4 changed files
with
236 additions
and
140 deletions
+236
-140
theories/examples/counter.v
theories/examples/counter.v
+0
-1
theories/examples/generative.v
theories/examples/generative.v
+3
-0
theories/examples/or.v
theories/examples/or.v
+21
-22
theories/examples/symbol.v
theories/examples/symbol.v
+212
-117
No files found.
theories/examples/counter.v
View file @
3447371d
...
...
@@ -122,7 +122,6 @@ Section CG_Counter.
(
*
A
logically
atomic
specification
for
a
fine
-
grained
increment
with
a
baked
in
frame
.
*
)
(
*
Unfortunately
,
the
precondition
is
not
baked
in
the
rule
so
you
can
only
use
it
when
your
spatial
context
is
empty
*
)
Lemma
bin_log_FG_increment_logatomic
R
P
Γ
E
K
x
t
τ
:
P
-
∗
□
(
|={
⊤
,
E
}=>
∃
n
:
nat
,
x
↦ᵢ
#
n
∗
R
n
∗
...
...
theories/examples/generative.v
View file @
3447371d
...
...
@@ -7,6 +7,9 @@ From iris_logrel Require Import logrel examples.counter examples.lock prelude.bi
(
**
*
5.2
References
for
name
generation
*
)
(
*
∃
α
.
(
1
→
α
)
×
(
α
→
α
→
2
)
*
)
(
*
^
new
name
^
*
)
(
*
|
compare
names
for
equality
*
)
Definition
nameGenTy
:
type
:=
TExists
(
TProd
(
TArrow
TUnit
(
TVar
0
))
(
TArrow
(
TVar
0
)
(
TArrow
(
TVar
0
)
TBool
))).
...
...
theories/examples/or.v
View file @
3447371d
...
...
@@ -99,7 +99,7 @@ Section contents.
Definition
or_inv
x
:
iProp
Σ
:=
(
x
↦ᵢ
#
0
∨
x
↦ᵢ
#
1
)
%
I
.
Definition
orN
:=
nroot
.
@
"orN"
.
Ltac
close_
shoot
:=
iNext
;
(
iLeft
+
iRight
);
by
iFrame
.
Ltac
close_
inv
:=
iNext
;
(
iLeft
+
iRight
);
by
iFrame
.
Lemma
assign_safe
x
:
inv
orN
(
or_inv
x
)
...
...
@@ -107,7 +107,7 @@ Section contents.
Proof
.
iIntros
"#Hinv"
.
iNext
.
iInv
orN
as
">[Hx | Hx]"
"Hcl"
;
wp_store
;
(
iMod
(
"Hcl"
with
"[-]"
);
first
close_
shoot
);
eauto
.
(
iMod
(
"Hcl"
with
"[-]"
);
first
close_
inv
);
eauto
.
Qed
.
Lemma
bin_log_or_commute
Δ
Γ
(
v1
v1
'
v2
v2
'
:
val
)
:
...
...
@@ -116,13 +116,13 @@ Section contents.
{
Δ
;
Γ
}
⊨
or
v2
v1
≤
log
≤
or
v1
'
v2
'
:
TUnit
.
Proof
.
iIntros
"Hv1 Hv2"
.
unlock
or
.
repeat
rel_rec_r
.
repeat
rel_rec_l
.
unlock
or
;
simpl
.
repeat
rel_rec_r
.
repeat
rel_rec_l
.
rel_alloc_l
as
x
"Hx"
.
rel_alloc_r
as
y
"Hy"
.
repeat
rel_let_l
.
repeat
rel_let_r
.
rel_fork_r
as
j
"Hj"
.
rel_seq_r
.
iMod
(
inv_alloc
orN
_
(
or_inv
x
)
with
"[Hx]"
)
as
"#Hinv"
.
{
close_shoot
.
}
iMod
(
inv_alloc
orN
_
(
or_inv
x
)
with
"[Hx]"
)
as
"#Hinv"
;
first
close_inv
.
rel_fork_l
.
iModIntro
.
iSplitR
;
[
by
iApply
assign_safe
|
].
rel_seq_l
.
...
...
@@ -130,18 +130,17 @@ Section contents.
iInv
orN
as
">[Hx|Hx]"
"Hcl"
;
iExists
_
;
iFrame
;
iModIntro
;
iNext
;
iIntros
"Hx"
;
rel_op_l
;
rel_if_l
.
+
apply
bin_log_related_spec_ctx
.
iDestruct
1
as
(
ρ
1
)
"#Hρ1"
.
(
*
TODO
:
tp
tactics
should
be
aware
of
that
^
*
)
+
apply
bin_log_related_spec_ctx
;
iDestruct
1
as
(
ρ
1
)
"#Hρ1"
.
(
*
TODO
:
tp
tactics
should
be
aware
of
spec_ctx
*
)
tp_store
j
.
rel_load_r
.
repeat
(
rel_pure_r
_
).
iMod
(
"Hcl"
with
"[-Hv1 Hv2]"
);
first
close_
shoot
.
iMod
(
"Hcl"
with
"[-Hv1 Hv2]"
);
first
close_
inv
.
iApply
(
bin_log_related_app
with
"Hv2"
).
iApply
bin_log_related_unit
.
+
rel_load_r
.
repeat
(
rel_pure_r
_
).
iMod
(
"Hcl"
with
"[-Hv1 Hv2]"
);
first
close_
shoot
.
iMod
(
"Hcl"
with
"[-Hv1 Hv2]"
);
first
close_
inv
.
iApply
(
bin_log_related_app
with
"Hv1"
).
iApply
bin_log_related_unit
.
Qed
.
...
...
@@ -173,7 +172,7 @@ Section contents.
rel_alloc_l
as
x
"Hx"
.
repeat
rel_let_l
.
iMod
(
inv_alloc
orN
_
(
or_inv
x
)
%
I
with
"[Hx]"
)
as
"#Hinv"
.
{
close_
shoot
.
}
{
close_
inv
.
}
rel_fork_l
.
iModIntro
.
iSplitR
;
[
by
iApply
assign_safe
|
].
rel_seq_l
.
...
...
@@ -181,10 +180,10 @@ Section contents.
iInv
orN
as
">[Hx|Hx]"
"Hcl"
;
iExists
_
;
iFrame
;
iModIntro
;
iNext
;
iIntros
"Hx"
;
rel_op_l
;
rel_if_l
.
+
iMod
(
"Hcl"
with
"[-Hlog]"
);
first
close_
shoot
.
+
iMod
(
"Hcl"
with
"[-Hlog]"
);
first
close_
inv
.
iApply
(
bin_log_related_app
with
"Hlog"
).
iApply
bin_log_related_unit
.
+
iMod
(
"Hcl"
with
"[-Hlog]"
);
first
close_
shoot
.
+
iMod
(
"Hcl"
with
"[-Hlog]"
);
first
close_
inv
.
iApply
(
bin_log_related_app
with
"Hlog"
).
iApply
bin_log_related_unit
.
Qed
.
...
...
@@ -198,7 +197,7 @@ Section contents.
rel_alloc_l
as
x
"Hx"
.
repeat
rel_let_l
.
iMod
(
inv_alloc
orN
_
(
or_inv
x
)
%
I
with
"[Hx]"
)
as
"#Hinv"
.
{
close_
shoot
.
}
{
close_
inv
.
}
rel_fork_l
.
iModIntro
.
iSplitR
;
[
by
iApply
assign_safe
|
].
rel_seq_l
.
...
...
@@ -206,10 +205,10 @@ Section contents.
iInv
orN
as
">[Hx|Hx]"
"Hcl"
;
iExists
_
;
iFrame
;
iModIntro
;
iNext
;
iIntros
"Hx"
;
rel_op_l
;
rel_if_l
.
+
iMod
(
"Hcl"
with
"[-Hlog]"
);
first
close_
shoot
.
+
iMod
(
"Hcl"
with
"[-Hlog]"
);
first
close_
inv
.
iApply
(
bin_log_related_app
with
"Hlog"
).
iApply
bin_log_related_unit
.
+
iMod
(
"Hcl"
with
"[-Hlog]"
);
first
close_
shoot
.
+
iMod
(
"Hcl"
with
"[-Hlog]"
);
first
close_
inv
.
rel_apply_l
bot_l
.
Qed
.
...
...
@@ -236,7 +235,7 @@ Section contents.
repeat
rel_let_l
.
repeat
rel_let_r
.
rel_fork_r
as
j
"Hj"
.
rel_seq_r
.
iMod
(
inv_alloc
orN
_
(
or_inv
x
)
with
"[Hx]"
)
as
"#Hinv"
.
{
close_
shoot
.
}
{
close_
inv
.
}
rel_fork_l
.
iModIntro
.
iSplitR
;
[
by
iApply
assign_safe
|
].
rel_seq_l
.
...
...
@@ -250,14 +249,14 @@ Section contents.
rel_let_r
.
rel_fork_r
as
k
"Hk"
.
rel_seq_r
.
rel_load_r
.
repeat
(
rel_pure_r
_
).
iMod
(
"Hcl"
with
"[-Hv1 Hv2 Hv3]"
)
as
"_"
;
first
close_
shoot
.
iMod
(
"Hcl"
with
"[-Hv1 Hv2 Hv3]"
)
as
"_"
;
first
close_
inv
.
iApply
(
bin_log_related_app
with
"Hv1"
).
iApply
bin_log_related_unit
.
-
iMod
(
"Hcl"
with
"[-Hv1 Hv2 Hv3 Hy Hj]"
)
as
"_"
;
first
close_
shoot
.
-
iMod
(
"Hcl"
with
"[-Hv1 Hv2 Hv3 Hy Hj]"
)
as
"_"
;
first
close_
inv
.
rel_alloc_l
as
x
'
"Hx'"
.
rel_let_l
.
iClear
"Hinv"
.
iMod
(
inv_alloc
orN
_
(
or_inv
x
'
)
with
"[Hx']"
)
as
"#Hinv"
.
{
close_
shoot
.
}
{
close_
inv
.
}
rel_fork_l
.
iModIntro
.
iSplitR
;
[
by
iApply
assign_safe
|
].
apply
bin_log_related_spec_ctx
.
...
...
@@ -274,12 +273,12 @@ Section contents.
tp_store
k
.
rel_load_r
.
repeat
(
rel_pure_r
_
).
iMod
(
"Hcl"
with
"[-Hv1 Hv2 Hv3]"
)
as
"_"
;
first
close_
shoot
.
iMod
(
"Hcl"
with
"[-Hv1 Hv2 Hv3]"
)
as
"_"
;
first
close_
inv
.
iApply
(
bin_log_related_app
with
"Hv2"
).
iApply
bin_log_related_unit
.
+
tp_store
j
.
rel_load_r
;
repeat
(
rel_pure_r
_
).
iMod
(
"Hcl"
with
"[-Hv1 Hv2 Hv3]"
)
as
"_"
;
first
close_
shoot
.
iMod
(
"Hcl"
with
"[-Hv1 Hv2 Hv3]"
)
as
"_"
;
first
close_
inv
.
iApply
(
bin_log_related_app
with
"Hv3"
).
iApply
bin_log_related_unit
.
Qed
.
...
...
theories/examples/symbol.v
View file @
3447371d
...
...
@@ -18,55 +18,7 @@ Notation NileV := (FoldV NONEV).
Definition
LIST
τ
:=
TRec
(
TSum
TUnit
(
TProd
τ
.[
ren
(
+
1
)]
(
TVar
0
))).
Lemma
LIST_interp_nil
τ
`
{
logrelG
Σ
}
:
⟦
LIST
τ
⟧
[]
(
NileV
,
NileV
).
Proof
.
rewrite
/=
{
1
}
fixpoint_unfold
/=
.
iExists
(
_
,
_
).
iSplit
;
eauto
.
iNext
.
iLeft
.
iExists
(
_
,
_
).
eauto
.
Qed
.
Lemma
LIST_interp_cons
(
n
:
nat
)
ls1
ls2
`
{
logrelG
Σ
}
:
⟦
LIST
TNat
⟧
[]
(
ls1
,
ls2
)
-
∗
⟦
LIST
TNat
⟧
[]
(
ConseV
#
n
ls1
,
ConseV
#
n
ls2
).
Proof
.
iIntros
"#Hls"
.
rewrite
/=
{
2
}
fixpoint_unfold
/=
.
iExists
(
_
,
_
).
iSplit
;
eauto
.
iNext
.
iRight
.
iExists
(
_
,
_
).
iSplit
;
eauto
.
iExists
(
_
,
_
),
(
_
,
_
).
iSplit
;
eauto
.
Qed
.
Lemma
LIST_interp_weaken
`
{
logrelG
Σ
}
Δ
ls1
ls2
:
⟦
LIST
TNat
⟧
[]
(
ls1
,
ls2
)
-
∗
⟦
LIST
TNat
⟧
Δ
(
ls1
,
ls2
).
Proof
.
iRevert
(
ls1
ls2
).
iL
ö
b
as
"IH"
.
iIntros
(
ls1
ls2
)
"#Hls /="
.
rewrite
{
2
}
(
fixpoint_unfold
(
interp_rec1
(
interp_sum
interp_unit
(
interp_prod
interp_nat
(
ctx_lookup
0
)))
Δ
))
/=
.
rewrite
{
2
}
(
fixpoint_unfold
(
interp_rec1
(
interp_sum
interp_unit
(
interp_prod
interp_nat
(
ctx_lookup
0
)))
[]))
/=
.
iDestruct
"Hls"
as
([
?
?
])
"[% #Hls]"
.
iExists
(
_
,
_
).
iSplit
;
eauto
.
iNext
.
iDestruct
"Hls"
as
"[Hls | Hls]"
.
-
iLeft
;
eauto
.
-
iRight
.
iDestruct
"Hls"
as
([
?
?
])
"[% Hls]"
.
iExists
_.
iSplit
;
eauto
.
iDestruct
"Hls"
as
([
?
?
]
[
?
?
])
"[% [Hn #Hls]]"
.
iExists
_
,
_.
iSplit
;
eauto
.
iSplit
;
eauto
.
iAlways
.
by
iApply
"IH"
.
Qed
.
(
*
`nth
ls
n
`
diverges
if
`n
>=
length
ls
`
*
)
(
*
`nth
ls
n
`
loops
if
`n
>=
length
ls
`
*
)
Definition
nth
:
val
:=
rec
:
"nth"
"l"
"n"
:=
match:
Unfold
"l"
with
NONE
=>
bot
#()
...
...
@@ -128,46 +80,54 @@ Lemma eqKey_typed Γ :
typed
Γ
eqKey
(
TArrow
TNat
(
TArrow
TNat
TBool
)).
Proof
.
solve_typed
.
Qed
.
Hint
Resolve
eqKey_typed
:
typeable
.
Lemma
symbol1_typed
Γ
:
typed
Γ
symbol1
(
TArrow
TUnit
SYMBOL
).
Lemma
LIST_interp_nil
τ
`
{
logrelG
Σ
}
:
⟦
LIST
τ
⟧
[]
(
NileV
,
NileV
).
Proof
.
unfold
SYMBOL
.
solve_typed
.
econstructor
.
cbn
.
econstructor
;
cbn
.
2
:
solve_typed
.
econstructor
;
cbn
.
econstructor
;
cbn
.
econstructor
;
cbn
.
econstructor
;
cbn
.
2
:
solve_typed
.
econstructor
;
cbn
.
econstructor
;
cbn
.
econstructor
;
cbn
.
econstructor
;
cbn
.
apply
eqKey_typed
.
econstructor
;
cbn
.
2
:
solve_typed
.
all:
solve_typed
.
rewrite
/=
{
1
}
fixpoint_unfold
/=
.
iExists
(
_
,
_
).
iSplit
;
eauto
.
iNext
.
iLeft
.
iExists
(
_
,
_
).
eauto
.
Qed
.
Hint
Resolve
symbol1_typed
:
typeable
.
Lemma
symbol2_typed
Γ
:
typed
Γ
symbol2
(
TArrow
TUnit
SYMBOL
).
Lemma
LIST_interp_cons
(
n
:
nat
)
ls1
ls2
`
{
logrelG
Σ
}
:
⟦
LIST
TNat
⟧
[]
(
ls1
,
ls2
)
-
∗
⟦
LIST
TNat
⟧
[]
(
ConseV
#
n
ls1
,
ConseV
#
n
ls2
).
Proof
.
unfold
SYMBOL
.
solve_typed
.
econstructor
.
cbn
.
econstructor
;
cbn
.
2
:
solve_typed
.
econstructor
;
cbn
.
econstructor
;
cbn
.
econstructor
;
cbn
.
econstructor
;
cbn
.
2
:
solve_typed
.
econstructor
;
cbn
.
econstructor
;
cbn
.
econstructor
;
cbn
.
econstructor
;
cbn
.
apply
eqKey_typed
.
econstructor
;
cbn
.
2
:
solve_typed
.
all:
solve_typed
.
iIntros
"#Hls"
.
rewrite
/=
{
2
}
fixpoint_unfold
/=
.
iExists
(
_
,
_
).
iSplit
;
eauto
.
iNext
.
iRight
.
iExists
(
_
,
_
).
iSplit
;
eauto
.
iExists
(
_
,
_
),
(
_
,
_
).
iSplit
;
eauto
.
Qed
.
Lemma
LIST_interp_weaken
`
{
logrelG
Σ
}
Δ
ls1
ls2
:
⟦
LIST
TNat
⟧
[]
(
ls1
,
ls2
)
-
∗
⟦
LIST
TNat
⟧
Δ
(
ls1
,
ls2
).
Proof
.
iRevert
(
ls1
ls2
).
iL
ö
b
as
"IH"
.
iIntros
(
ls1
ls2
)
"#Hls /="
.
rewrite
{
2
}
(
fixpoint_unfold
(
interp_rec1
(
interp_sum
interp_unit
(
interp_prod
interp_nat
(
ctx_lookup
0
)))
Δ
))
/=
.
rewrite
{
2
}
(
fixpoint_unfold
(
interp_rec1
(
interp_sum
interp_unit
(
interp_prod
interp_nat
(
ctx_lookup
0
)))
[]))
/=
.
iDestruct
"Hls"
as
([
?
?
])
"[% #Hls]"
.
iExists
(
_
,
_
).
iSplit
;
eauto
.
iNext
.
iDestruct
"Hls"
as
"[Hls | Hls]"
.
-
iLeft
;
eauto
.
-
iRight
.
iDestruct
"Hls"
as
([
?
?
])
"[% Hls]"
.
iExists
_.
iSplit
;
eauto
.
iDestruct
"Hls"
as
([
?
?
]
[
?
?
])
"[% [Hn #Hls]]"
.
iExists
_
,
_.
iSplit
;
eauto
.
iSplit
;
eauto
.
iAlways
.
by
iApply
"IH"
.
Qed
.
Hint
Resolve
symbol2_typed
:
typeable
.
(
**
*
The
actual
refinement
proof
.
Requires
monotonic
state
*
)
...
...
@@ -264,8 +224,94 @@ Section proof.
iApply
bin_log_related_nat
.
Qed
.
Lemma
lookup_refinement1
(
γ
:
gname
)
(
size1
size2
tbl1
tbl2
:
loc
)
Δ
Γ
:
inv
sizeN
(
table_inv
γ
size1
size2
tbl1
tbl2
)
-
∗
{
(
tableR
γ
::
Δ
);
⤉Γ
}
⊨
(
λ
:
"n"
,
(
nth
!
#
tbl1
)
(
!
#
size1
-
"n"
))
≤
log
≤
(
λ
:
"n"
,
let:
"m"
:=
!
#
size2
in
if:
"n"
≤
"m"
then
(
nth
!
#
tbl2
)
(
!
#
size2
-
"n"
)
else
#
0
)
:
(
TVar
0
→
TNat
).
Proof
.
iIntros
"#Hinv"
.
iApply
bin_log_related_arrow_val
;
eauto
.
iAlways
.
iIntros
(
k1
k2
)
"/= #Hk"
.
iDestruct
"Hk"
as
(
n
)
"(% & % & #Hn)"
;
simplify_eq
.
rel_let_l
.
rel_let_r
.
rel_load_l_atomic
.
iInv
sizeN
as
(
m
ls
)
"(Ha & Hs1' & >Hs2' & >Htbl1' & >Htbl2' & #Hls)"
"Hcl"
.
iModIntro
.
iExists
_.
iFrame
.
iNext
.
iIntros
"Htbl1'"
.
Local
Opaque
interp
.
rel_load_r
.
rel_let_r
.
iDestruct
(
own_valid_2
with
"Ha Hn"
)
as
%
[
?%
mnat_included
_
]
%
auth_valid_discrete_2
.
rel_op_r
.
destruct
(
le_dec
n
m
);
last
by
exfalso
.
rel_if_r
.
rel_load_r
.
iMod
(
"Hcl"
with
"[Ha Hs1' Hs2' Htbl1' Htbl2' Hls]"
)
as
"_"
.
{
iNext
.
iExists
_
,
_.
by
iFrame
.
}
repeat
iApply
bin_log_related_app
.
+
iApply
binary_fundamental
;
eauto
with
typeable
.
+
rel_vals
.
by
iApply
LIST_interp_weaken
.
+
iClear
"Hls"
.
clear
ls
.
rel_load_l_atomic
.
iInv
sizeN
as
(
m
'
ls
)
"(Ha & Hs1' & Hs2' & Htbl1' & Htbl2' & #Hls)"
"Hcl"
.
iModIntro
.
iExists
_.
iFrame
.
iNext
.
iIntros
"Hs1'"
.
rel_load_r
.
iMod
(
"Hcl"
with
"[Ha Hs1' Hs2' Htbl1' Htbl2']"
)
as
"_"
.
{
iNext
.
iExists
_
,
_.
by
iFrame
.
}
iApply
bin_log_related_nat_binop
;
eauto
.
all:
iApply
bin_log_related_nat
.
Qed
.
Lemma
lookup_refinement2
(
γ
:
gname
)
(
size1
size2
tbl1
tbl2
:
loc
)
Δ
Γ
:
inv
sizeN
(
table_inv
γ
size1
size2
tbl1
tbl2
)
-
∗
{
(
tableR
γ
::
Δ
);
⤉Γ
}
⊨
(
λ
:
"n"
,
let:
"m"
:=
!
#
size1
in
if:
"n"
≤
"m"
then
(
nth
!
#
tbl1
)
(
!
#
size1
-
"n"
)
else
#
0
)
≤
log
≤
(
λ
:
"n"
,
(
nth
!
#
tbl2
)
(
!
#
size2
-
"n"
))
:
(
TVar
0
→
TNat
).
Proof
.
iIntros
"#Hinv"
.
iApply
bin_log_related_arrow_val
;
eauto
.
iAlways
.
iIntros
(
k1
k2
)
"#Hk /="
.
iDestruct
"Hk"
as
(
n
)
"(% & % & #Hn)"
;
simplify_eq
.
rel_let_l
.
rel_let_r
.
rel_load_l_atomic
.
iInv
sizeN
as
(
m
ls
)
"(Ha & Hs1' & >Hs2' & >Htbl1' & >Htbl2' & Hls)"
"Hcl"
.
iModIntro
.
iExists
_.
iFrame
.
iNext
.
iIntros
"Hs1'"
.
iDestruct
(
own_valid_2
with
"Ha Hn"
)
as
%
[
?%
mnat_included
_
]
%
auth_valid_discrete_2
.
iMod
(
"Hcl"
with
"[Ha Hs1' Hs2' Htbl1' Htbl2' Hls]"
)
as
"_"
.
{
iNext
.
iExists
_
,
_.
by
iFrame
.
}
clear
ls
.
rel_let_l
.
rel_op_l
.
destruct
(
le_dec
n
m
);
last
by
congruence
.
rel_if_l
.
repeat
iApply
bin_log_related_app
.
+
iApply
binary_fundamental
;
eauto
with
typeable
.
+
rel_load_l_atomic
.
iInv
sizeN
as
(
m
'
ls
)
"(Ha & Hs1' & Hs2' & Htbl1' & Htbl2' & #Hls)"
"Hcl"
.
iModIntro
.
iExists
_.
iFrame
.
iNext
.
iIntros
"Htbl1'"
.
rel_load_r
.
iMod
(
"Hcl"
with
"[Ha Hs1' Hs2' Htbl1' Htbl2']"
)
as
"_"
.
{
iNext
.
iExists
_
,
_.
by
iFrame
.
}
rel_vals
;
eauto
.
iModIntro
.
by
iApply
LIST_interp_weaken
.
+
iApply
bin_log_related_nat_binop
;
eauto
;
last
by
iApply
bin_log_related_nat
.
rel_load_l_atomic
.
iInv
sizeN
as
(
m
'
ls
)
"(Ha & Hs1' & Hs2' & Htbl1' & Htbl2' & Hls)"
"Hcl"
.
iModIntro
.
iExists
_.
iFrame
.
iNext
.
iIntros
"Hs1'"
.
rel_load_r
.
iMod
(
"Hcl"
with
"[Ha Hs1' Hs2' Htbl1' Htbl2' Hls]"
)
as
"_"
.
{
iNext
.
iExists
_
,
_.
by
iFrame
.
}
iApply
bin_log_related_nat
.
Qed
.
Lemma
refinement1
Δ
Γ
:
{
Δ
;
Γ
}
⊨
symbol
2
≤
log
≤
symbol1
:
TArrow
TUnit
SYMBOL
.
{
Δ
;
Γ
}
⊨
symbol
1
≤
log
≤
symbol2
:
TArrow
TUnit
SYMBOL
.
Proof
.
unlock
symbol1
symbol2
.
iApply
bin_log_related_arrow_val
;
eauto
.
...
...
@@ -345,41 +391,90 @@ Section proof.
rel_vals
.
iModIntro
.
iAlways
.
iExists
m
'
.
eauto
.
(
*
Lookup
*
)
-
by
iApply
lookup_refinement1
.
Qed
.
Lemma
refinement2
Δ
Γ
:
{
Δ
;
Γ
}
⊨
symbol2
≤
log
≤
symbol1
:
TArrow
TUnit
SYMBOL
.
Proof
.
unlock
symbol1
symbol2
.
iApply
bin_log_related_arrow_val
;
eauto
.
iAlways
.
iIntros
(
?
?
)
"[% %]"
;
simplify_eq
/=
.
rel_let_l
.
rel_let_r
.
rel_alloc_l
as
size1
"[Hs1 Hs1']"
;
rel_let_l
.
rel_alloc_r
as
size2
"[Hs2 Hs2']"
;
rel_let_r
.
rel_alloc_l
as
tbl1
"[Htbl1 Htbl1']"
;
rel_let_l
.
rel_alloc_r
as
tbl2
"[Htbl2 Htbl2']"
;
rel_let_r
.
iMod
(
own_alloc
(
●
(
0
:
mnat
)))
as
(
γ
)
"Ha"
;
first
done
.
iMod
(
inv_alloc
sizeN
_
(
table_inv
γ
size1
size2
tbl1
tbl2
)
with
"[Hs1 Hs2 Htbl1 Htbl2 Ha]"
)
as
"#Hinv"
.
{
iNext
.
iExists
_
,
_.
iFrame
.
iApply
LIST_interp_nil
.
}
rel_apply_r
bin_log_related_newlock_r
;
first
done
.
iIntros
(
l2
)
"Hl2"
.
rel_let_r
.
pose
(
N
:=
(
logrelN
.
@
"lock1"
)).
rel_apply_l
(
bin_log_related_newlock_l
N
(
lok_inv
size1
size2
tbl1
tbl2
l2
)
%
I
with
"[Hs1' Hs2' Htbl1' Htbl2' Hl2]"
).
{
iExists
0
,
_.
by
iFrame
.
}
iIntros
(
l1
γ
l
)
"#Hl1"
.
rel_let_l
.
iApply
(
bin_log_related_pack
(
tableR
γ
)).
repeat
iApply
bin_log_related_pair
.
(
*
Eq
*
)
-
iApply
eqKey_refinement
.
(
*
Insert
*
)
-
iApply
bin_log_related_arrow_val
;
eauto
.
iAlways
.
iIntros
(
k1
k2
)
"/= #Hk"
.
iDestruct
"Hk"
as
(
n
)
"(% & % & #Hn)"
;
simplify_eq
.
iAlways
.
iIntros
(
?
?
).
iDestruct
1
as
(
n
)
"[% %]"
;
simplify_eq
/=
.
rel_let_l
.
rel_let_r
.
rel_apply_l
(
bin_log_related_acquire_l
with
"Hl1"
);
auto
.
iIntros
"Hlk Htbl"
.
rel_let_l
.
iDestruct
"Htbl"
as
(
m
ls
)
"(Hs1 & Hs2 & Htbl1 & Htbl2 & Hl2)"
.
rel_load_l
.
rel_let_l
.
rel_op_l
.
rel_store_l_atomic
.
iInv
sizeN
as
(
m
'
ls
'
)
"(Ha & >Hs1' & >Hs2' & >Htbl1' & >Htbl2' & #Hls)"
"Hcl"
.
iDestruct
(
mapsto_half_combine
with
"Hs1 Hs1'"
)
as
"[% Hs1]"
;
simplify_eq
.
iDestruct
(
mapsto_half_combine
with
"Htbl1 Htbl1'"
)
as
"[% [Htbl1 Htbl1']]"
;
simplify_eq
.
iModIntro
.
iExists
_.
iFrame
.
iNext
.
iIntros
"[Hs1 Hs1']"
.
rel_let_l
.
rel_apply_r
(
bin_log_related_acquire_r
with
"Hl2"
);
first
solve_ndisj
.
iIntros
"Hl2"
.
rel_let_r
.
rel_load_l_atomic
.
iInv
sizeN
as
(
m
ls
)
"(Ha & Hs1' & >Hs2' & >Htbl1' & >Htbl2' & Hls)"
"Hcl"
.
iModIntro
.
iExists
_.
iFrame
.
iNext
.
iIntros
"Hs1'"
.
iDestruct
(
own_valid_2
with
"Ha Hn"
)
as
%
[
?%
mnat_included
_
]
%
auth_valid_discrete_2
.
iMod
(
"Hcl"
with
"[Ha Hs1' Hs2' Htbl1' Htbl2' Hls]"
)
as
"_"
.
iDestruct
(
threadpool
.
mapsto_half_combine
with
"Hs2 Hs2'"
)
as
"[% Hs2]"
;
simplify_eq
.
rel_load_r
.
repeat
(
rel_pure_r
_
).
rel_store_r
.
rel_let_r
.
(
*
Before
we
close
the
lock
,
we
need
to
gather
some
evidence
*
)
iMod
(
conjure_0
γ
)
as
"Hf"
.
iMod
(
same_size
with
"[$Ha $Hf]"
)
as
"[Ha #Hf]"
.
iMod
(
inc_size
with
"Ha"
)
as
"Ha"
.
iDestruct
"Hs2"
as
"[Hs2 Hs2']"
.
rewrite
Nat
.
add_1_r
.
iMod
(
"Hcl"
with
"[Ha Hs1 Hs2 Htbl1 Htbl2]"
)
as
"_"
.
{
iNext
.
iExists
_
,
_.
by
iFrame
.
}
clear
ls
.
rel_load_l
.
rel_store_l_atomic
.
iClear
"Hls"
.
iInv
sizeN
as
(
m
ls
)
"(Ha & >Hs1 & >Hs2 & >Htbl1 & >Htbl2 & #Hls)"
"Hcl"
.
iDestruct
(
mapsto_half_combine
with
"Htbl1 Htbl1'"
)
as
"[% Htbl1]"
;
simplify_eq
.
iModIntro
.
iExists
_.
iFrame
.
iNext
.
iIntros
"[Htbl1 Htbl1']"
.
rel_let_l
.
rel_op_l
.
destruct
(
le_dec
n
m
);
last
congruence
.
rel_if_l
.
repeat
iApply
bin_log_related_app
.
+
iApply
binary_fundamental
;
eauto
with
typeable
.
+
rel_load_l_atomic
.
iInv
sizeN
as
(
m
'
ls
)
"(Ha & Hs1' & Hs2' & Htbl1' & Htbl2' & #Hls)"
"Hcl"
.
iModIntro
.
iExists
_.
iFrame
.
iNext
.
iIntros
"Htbl1'"
.
rel_load_r
.
iMod
(
"Hcl"
with
"[Ha Hs1' Hs2' Htbl1' Htbl2']"
)
as
"_"
.
{
iNext
.
iExists
_
,
_.
by
iFrame
.
}
rel_vals
;
eauto
.
iModIntro
.
by
iApply
LIST_interp_weaken
.
+
iApply
bin_log_related_nat_binop
;
eauto
;
last
by
iApply
bin_log_related_nat
.
rel_load_l_atomic
.
iInv
sizeN
as
(
m
'
ls
)
"(Ha & Hs1' & Hs2' & Htbl1' & Htbl2' & Hls)"
"Hcl"
.
iModIntro
.
iExists
_.
iFrame
.
iNext
.
iIntros
"Hs1'"
.
rel_load_r
.
iMod
(
"Hcl"
with
"[Ha Hs1' Hs2' Htbl1' Htbl2' Hls]"
)
as
"_"
.
{
iNext
.
iExists
_
,
_.
by
iFrame
.
}
iApply
bin_log_related_nat
.
rel_load_r
.
iDestruct
(
threadpool
.
mapsto_half_combine
with
"Htbl2 Htbl2'"
)
as
"[% Htbl2]"
;
simplify_eq
.
rel_store_r
.
rel_let_r
.
rel_apply_r
(
bin_log_related_release_r
with
"Hl2"
);
first
solve_ndisj
.
iIntros
"Hl2"
.
rel_let_r
.
iDestruct
"Htbl2"
as
"[Htbl2 Htbl2']"
.
iMod
(
"Hcl"
with
"[Ha Hs1 Hs2 Htbl1 Htbl2]"
)
as
"_"
.
{
iNext
.
iExists
_
,
_.
iFrame
.
by
iApply
LIST_interp_cons
.
}
rel_apply_l
(
bin_log_related_release_l
with
"Hl1 Hlk [-]"
);
auto
.
{
iExists
_
,
_.
by
iFrame
.
}
rel_let_l
.
rel_vals
.
iModIntro
.
iAlways
.
iExists
m
'
.
eauto
.
(
*
Lookup
*
)
-
by
iApply
lookup_refinement2
.
Qed
.
End
proof
.
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a 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