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
Dan Frumin
ReLoC-v1
Commits
d6237350
Commit
d6237350
authored
Sep 13, 2017
by
Dan Frumin
Browse files
[stack] Finish the stack module refinement
parent
a8c7557d
Changes
4
Hide whitespace changes
Inline
Side-by-side
_CoqProject
View file @
d6237350
...
...
@@ -33,6 +33,7 @@ theories/examples/stack/stack_rules.v
theories/examples/stack/CG_stack.v
theories/examples/stack/FG_stack.v
theories/examples/stack/refinement.v
theories/examples/stack/module_refinement.v
theories/examples/stack/mailbox.v
theories/examples/stack/helping.v
theories/tests/typetest.v
...
...
theories/examples/stack/module_refinement.v
View file @
d6237350
...
...
@@ -4,17 +4,17 @@ From iris_logrel.examples.stack Require Import
CG_stack
FG_stack
stack_rules
refinement
.
Section
Mod_refinement
.
Context
`
{
logrel
G
Σ
,
stack
G
Σ
}
.
Context
`
{
HLR
:
logrelG
Σ
}
.
Notation
D
:=
(
prodC
valC
valC
-
n
>
iProp
Σ
).
Implicit
Types
Δ
:
listC
D
.
Import
lang
.
Program
Definition
sint
`
{
logrelG
Σ
,
stackG
Σ
}
τ
i
:
prodC
valC
valC
-
n
>
iProp
Σ
:=
λ
ne
vv
,
(
∃
(
l
stk
stk
'
:
loc
),
⌜
(
vv
.2
)
=
(#
stk
'
,
#
l
)
%
V
⌝
∗
⌜
(
vv
.1
)
=
#
stk
⌝
∗
inv
stackN
(
sinv
τ
i
stk
stk
'
l
))
%
I
.
Next
Obligation
.
solve_proper
.
Qed
.
Program
Definition
sint
{
LG
:
logrelG
Σ
}
{
Z
:
stack
Pre
G
Σ
}
τ
i
:
prodC
valC
valC
-
n
>
iProp
Σ
:=
λ
ne
vv
,
(
∃
γ
(
l
stk
stk
'
:
loc
),
⌜
(
vv
.2
)
=
(#
stk
'
,
#
l
)
%
V
⌝
∗
⌜
(
vv
.1
)
=
#
stk
⌝
∗
inv
(
stackN
.
@
(
stk
,
stk
'
))
(
sinv
'
γ
τ
i
stk
stk
'
l
))
%
I
.
Solve
Obligation
s
with
solve_proper
.
Instance
sint_persistent
τ
i
vv
:
PersistentP
(
sint
τ
i
vv
).
Instance
sint_persistent
`
{
logrelG
Σ
,
stackPreG
Σ
}
τ
i
vv
:
PersistentP
(
sint
τ
i
vv
).
Proof
.
apply
_.
Qed
.
Lemma
interp_subst_up_2
Δ
1
Δ
2
τ
τ
i
:
...
...
@@ -60,7 +60,7 @@ Section Mod_refinement.
by
rewrite
-
interp_subst_2
.
Qed
.
Lemma
module_refinmen
e
t
Δ
Γ
:
Lemma
module_refin
e
ment
`
{
SPG
:
stackPreG
Σ
}
Δ
Γ
:
{
⊤
,
⊤
;
Δ
;
Γ
}
⊨
FG_stack
.
stackmod
≤
log
≤
CG_stack
.
stackmod
:
TForall
$
TExists
$
TProd
(
TProd
(
TArrow
TUnit
(
TVar
0
))
(
TArrow
(
TVar
0
)
(
TSum
TUnit
(
TVar
1
))))
...
...
@@ -79,13 +79,29 @@ Section Mod_refinement.
rel_seq_r
.
rel_alloc_l
as
istk
"Histk"
.
simpl
.
rel_alloc_l
as
stk
"Hstk"
.
rel_alloc_r
as
st
l
'
"Hstk'"
.
rel_alloc_r
as
st
k
'
"Hstk'"
.
rel_alloc_r
as
l
"Hl"
.
rel_vals
.
admit
.
rewrite
-
persistentP
.
iMod
(
own_alloc
(
●
(
∅
:
stackUR
)))
as
(
γ
)
"Hemp"
;
first
done
.
pose
(
SG
:=
StackG
Σ
_
γ
).
iAssert
(
prestack_owns
γ
∅
)
with
"[Hemp]"
as
"Hoe"
.
{
rewrite
/
prestack_owns
big_sepM_empty
fmap_empty
.
iFrame
"Hemp"
.
}
iMod
(
stack_owns_alloc
with
"[$Hoe $Histk]"
)
as
"[Hoe #Histk]"
.
iAssert
(
preStackLink
γ
τ
i
(#
istk
,
FoldV
(
InjLV
(
LitV
Unit
))))
with
"[Histk]"
as
"#HLK"
.
{
rewrite
preStackLink_unfold
.
iExists
_
,
_.
iSplitR
;
simpl
;
trivial
.
iFrame
"Histk"
.
iLeft
.
iSplit
;
trivial
.
}
iAssert
(
sinv
'
γ
τ
i
stk
stk
'
l
)
with
"[Hoe Hstk Hstk' HLK Hl]"
as
"Hinv"
.
{
iExists
_
,
_
,
_.
by
iFrame
.
}
iMod
(
inv_alloc
(
stackN
.
@
(
stk
,
stk
'
))
with
"[Hinv]"
)
as
"#Hinv"
.
{
iNext
.
iExact
"Hinv"
.
}
iModIntro
.
iExists
γ
,
l
,
stk
,
stk
'
.
eauto
.
-
iApply
bin_log_related_arrow_val
;
eauto
.
iAlways
.
iIntros
(
?
?
)
"#Hvv /="
.
iDestruct
"Hvv"
as
(
l
stk
stk
'
)
"(% & % & #Hinv)"
.
iDestruct
"Hvv"
as
(
γ
l
stk
stk
'
)
"(% & % & #Hinv)"
.
simplify_eq
/=
.
rel_let_l
.
rel_let_r
.
...
...
@@ -100,11 +116,15 @@ Section Mod_refinement.
replace
(
TSum
TUnit
(
TVar
1
))
with
(
TSum
TUnit
(
TVar
0
)).[
ren
(
+
1
)]
by
done
.
iApply
bin_log_weaken_2
.
by
iApply
FG_CG_pop_refinement
'
.
pose
(
SG
:=
StackG
Σ
_
γ
).
change
γ
with
stack_name
.
iApply
(
FG_CG_pop_refinement
'
(
stackN
.
@
(
stk
,
stk
'
))).
{
solve_ndisj
.
}
by
rewrite
sinv_unfold
.
-
iApply
bin_log_related_arrow_val
;
eauto
.
{
unlock
FG_push
.
done
.
}
iAlways
.
iIntros
(
?
?
)
"#Hvv /="
.
iDestruct
"Hvv"
as
(
l
stk
stk
'
)
"(% & % & #Hinv)"
.
iDestruct
"Hvv"
as
(
γ
l
stk
stk
'
)
"(% & % & #Hinv)"
.
simplify_eq
/=
.
rel_let_r
.
Transparent
FG_push
.
...
...
@@ -121,7 +141,22 @@ Section Mod_refinement.
with
((
CG_locked_push
$
/
LitV
stk
'
$
/
LitV
l
)
v
'
)
%
E
;
last
first
.
{
unlock
CG_locked_push
.
simpl_subst
/=
.
done
.
}
change
TUnit
with
(
TUnit
.[
ren
(
+
1
)]).
iApply
(
FG_CG_push_refinement
with
"Hinv Hτi"
).
Admitted
.
pose
(
SG
:=
StackG
Σ
_
γ
).
change
γ
with
stack_name
.
iApply
(
FG_CG_push_refinement
(
stackN
.
@
(
stk
,
stk
'
))
with
"[Hinv] Hτi"
).
{
solve_ndisj
.
}
by
rewrite
sinv_unfold
.
Qed
.
End
Mod_refinement
.
Theorem
module_ctx_refinement
:
∅
⊨
FG_stack
.
stackmod
≤
ctx
≤
CG_stack
.
stackmod
:
TForall
$
TExists
$
TProd
(
TProd
(
TArrow
TUnit
(
TVar
0
))
(
TArrow
(
TVar
0
)
(
TSum
TUnit
(
TVar
1
))))
(
TArrow
(
TVar
0
)
(
TArrow
(
TVar
1
)
TUnit
)).
Proof
.
set
(
Σ
:=
#[
logrel
Σ
;
GFunctor
(
authR
stackUR
)]).
eapply
(
logrel_ctxequiv
Σ
);
[
solve_closed
..
|
intros
].
apply
module_refinement
.
Qed
.
theories/examples/stack/refinement.v
View file @
d6237350
...
...
@@ -6,40 +6,52 @@ From iris_logrel.examples.stack Require Import
Definition
stackN
:
namespace
:=
nroot
.
@
"stack"
.
Section
Stack_refinement
.
Context
`
{
logrelG
Σ
,
stackG
Σ
}
.
Context
`
{
logrelG
Σ
}
.
Notation
D
:=
(
prodC
valC
valC
-
n
>
iProp
Σ
).
Implicit
Types
Δ
:
listC
D
.
Import
lang
.
Definition
sinv
τ
i
stk
stk
'
l
'
{
SH
:
stackG
Σ
}
:
iProp
Σ
:=
Definition
sinv
'
{
SPG
:
authG
Σ
stackUR
}
γ
τ
i
stk
stk
'
l
'
:
iProp
Σ
:=
(
∃
(
istk
:
loc
)
v
h
,
(
prestack_owns
γ
h
)
∗
stk
'
↦ₛ
v
∗
stk
↦ᵢ
(
FoldV
#
istk
)
∗
preStackLink
γ
τ
i
(#
istk
,
v
)
∗
l
'
↦ₛ
#
false
)
%
I
.
Context
`
{
stackG
Σ
}
.
Definition
sinv
τ
i
stk
stk
'
l
:
iProp
Σ
:=
(
∃
(
istk
:
loc
)
v
h
,
(
stack_owns
h
)
∗
stk
'
↦ₛ
v
∗
stk
↦ᵢ
(
FoldV
#
istk
)
∗
StackLink
τ
i
(#
istk
,
v
)
∗
l
'
↦ₛ
#
false
)
%
I
.
∗
l
↦ₛ
#
false
)
%
I
.
Lemma
sinv_unfold
τ
i
stk
stk
'
l
:
sinv
τ
i
stk
stk
'
l
=
sinv
'
stack_name
τ
i
stk
stk
'
l
.
Proof
.
reflexivity
.
Qed
.
Ltac
close_sinv
Hcl
asn
:=
iMod
(
Hcl
with
asn
)
as
"_"
;
[
iNext
;
rewrite
/
sinv
;
iExists
_
,
_
,
_
;
by
iFrame
|
];
try
iModIntro
.
Lemma
FG_CG_push_refinement
st
st
'
(
τ
i
:
D
)
(
v
v
'
:
val
)
l
{
τ
P
:
∀
ww
,
PersistentP
(
τ
i
ww
)
}
Γ
:
inv
stackN
(
sinv
τ
i
st
st
'
l
)
-
∗
τ
i
(
v
,
v
'
)
-
∗
Lemma
FG_CG_push_refinement
N
st
st
'
(
τ
i
:
D
)
(
v
v
'
:
val
)
l
{
τ
P
:
∀
ww
,
PersistentP
(
τ
i
ww
)
}
Γ
:
N
⊥
logrelN
→
inv
N
(
sinv
τ
i
st
st
'
l
)
-
∗
τ
i
(
v
,
v
'
)
-
∗
Γ
⊨
(
FG_push
$
/
(
LitV
(
Loc
st
)))
v
≤
log
≤
(
CG_locked_push
$
/
(
LitV
(
Loc
st
'
))
$
/
(
LitV
(
Loc
l
)))
v
'
:
TUnit
.
Proof
.
iIntros
"#Hinv #Hvv'"
(
Δ
).
iIntros
(
?
)
"#Hinv #Hvv'"
.
iIntros
(
Δ
).
Transparent
FG_push
.
unfold
FG_push
.
unlock
.
simpl_subst
/=
.
iL
ö
b
as
"IH"
.
rel_rec_l
.
rel_load_l_atomic
.
iInv
stack
N
as
(
istk
w
h
)
"[Hoe [>Hst' [Hst [HLK >Hl]]]]"
"Hclose"
.
iInv
N
as
(
istk
w
h
)
"[Hoe [>Hst' [Hst [HLK >Hl]]]]"
"Hclose"
.
iExists
(
FoldV
#
istk
).
iFrame
.
iModIntro
.
iNext
.
iIntros
"Hst"
.
close_sinv
"Hclose"
"[Hst Hoe Hst' Hl HLK]"
.
clear
w
h
.
rel_rec_l
.
rel_alloc_l
as
nstk
"Hnstk"
.
simpl
.
rel_cas_l_atomic
.
iInv
stack
N
as
(
istk
'
w
h
)
"[Hoe [>Hst' [Hst [HLK >Hl]]]]"
"Hclose"
.
iInv
N
as
(
istk
'
w
h
)
"[Hoe [>Hst' [Hst [HLK >Hl]]]]"
"Hclose"
.
iExists
(
FoldV
#
istk
'
).
iFrame
.
iModIntro
.
destruct
(
decide
(
istk
'
=
istk
))
as
[
e
|
nestk
];
subst
.
...
...
@@ -70,12 +82,13 @@ Section Stack_refinement.
by
iApply
"IH"
.
Qed
.
Lemma
FG_CG_pop_refinement
'
st
st
'
(
τ
i
:
D
)
l
{
τ
P
:
∀
ww
,
PersistentP
(
τ
i
ww
)
}
Δ
Γ
:
inv
stackN
(
sinv
τ
i
st
st
'
l
)
-
∗
Lemma
FG_CG_pop_refinement
'
N
st
st
'
(
τ
i
:
D
)
l
{
τ
P
:
∀
ww
,
PersistentP
(
τ
i
ww
)
}
Δ
Γ
:
N
⊥
logrelN
→
inv
N
(
sinv
τ
i
st
st
'
l
)
-
∗
{
⊤
,
⊤
;
τ
i
::
Δ
;
Γ
}
⊨
(
FG_pop
$
/
LitV
(
Loc
st
))
#()
≤
log
≤
(
CG_locked_pop
$
/
LitV
(
Loc
st
'
)
$
/
LitV
(
Loc
l
))
#()
:
TSum
TUnit
(
TVar
0
).
Proof
.
Transparent
CG_locked_pop
FG_pop
CG_pop
.
iIntros
"#Hinv"
.
iIntros
(
?
)
"#Hinv"
.
iL
ö
b
as
"IH"
.
rewrite
{
2
}/
FG_pop
.
unlock
.
simpl_subst
/=
.
...
...
@@ -91,7 +104,7 @@ replace ((rec: "pop" "st" <> :=
rel_rec_l
.
rel_load_l_atomic
.
iInv
stack
N
as
(
istk
v
h
)
"[Hoe [Hst' [Hst [#HLK Hl]]]]"
"Hclose"
.
iInv
N
as
(
istk
v
h
)
"[Hoe [Hst' [Hst [#HLK Hl]]]]"
"Hclose"
.
iExists
_.
iFrame
.
iModIntro
.
iNext
.
iIntros
"Hst /="
.
rel_rec_l
.
...
...
@@ -107,7 +120,7 @@ replace ((rec: "pop" "st" <> :=
iIntros
"Hst' Hl"
.
close_sinv
"Hclose"
"[Hoe Hst' Hst Hl HLK']"
.
clear
h
.
iClear
"HLK'"
.
rel_load_l_atomic
.
iInv
stack
N
as
(
istk
v
h
)
"[Hoe [Hst' [Hst [#HLK Hl]]]]"
"Hclose"
.
iInv
N
as
(
istk
v
h
)
"[Hoe [Hst' [Hst [#HLK Hl]]]]"
"Hclose"
.
iDestruct
(
stack_owns_later_open_close
with
"Hoe Histk"
)
as
"[Histk_i Hoe]"
.
iExists
_.
iFrame
"Histk_i"
.
iModIntro
.
iNext
.
iIntros
"Histk_i /="
.
...
...
@@ -123,7 +136,7 @@ replace ((rec: "pop" "st" <> :=
iDestruct
"HLK"
as
(
y1
z1
y2
z2
)
"(% & % & Hτ & HLK_tail)"
;
simplify_eq
/=
.
close_sinv
"Hclose"
"[Hoe Hst' Hst Hl HLK']"
.
clear
h
.
rel_load_l_atomic
.
iInv
stack
N
as
(
istk
v
h
)
"[Hoe [Hst' [Hst [HLK Hl]]]]"
"Hclose"
.
iInv
N
as
(
istk
v
h
)
"[Hoe [Hst' [Hst [HLK Hl]]]]"
"Hclose"
.
iDestruct
(
stack_owns_later_open_close
with
"Hoe Histk"
)
as
"[Histk_i Hoe]"
.
iExists
_.
iFrame
.
iModIntro
.
iNext
.
iIntros
"Histk_i /="
.
...
...
@@ -134,7 +147,7 @@ replace ((rec: "pop" "st" <> :=
do
2
(
rel_proj_l
;
rel_rec_l
).
close_sinv
"Hclose"
"[Hoe Hst' Hst Hl HLK]"
.
clear
h
istk
v
.
rel_cas_l_atomic
.
iInv
stack
N
as
(
istk
v
h
)
"[Hoe [Hst' [Hst [HLK2 Hl]]]]"
"Hclose"
.
iInv
N
as
(
istk
v
h
)
"[Hoe [Hst' [Hst [HLK2 Hl]]]]"
"Hclose"
.
iExists
_.
iFrame
.
iModIntro
.
destruct
(
decide
(
istk
=
istk2
))
as
[
?
|
NE
];
simplify_eq
/=
.
...
...
@@ -179,10 +192,11 @@ replace ((rec: "pop" "st" <> :=
{
unlock
FG_pop
CG_locked_pop
.
simpl_subst
/=
.
solve_closed
.
}
{
unlock
FG_pop
CG_locked_pop
.
simpl_subst
/=
.
solve_closed
.
}
iAlways
.
iIntros
(
?
?
)
"[% %]"
.
simplify_eq
/=
.
by
iApply
FG_CG_pop_refinement
'
.
iApply
(
FG_CG_pop_refinement
'
stackN
);
eauto
.
{
solve_ndisj
.
}
Qed
.
Lemma
FG_CG_iter_refinement
st
st
'
(
τ
i
:
D
)
l
Δ
{
τ
P
:
∀
ww
,
PersistentP
(
τ
i
ww
)
}
{
SH
:
stackG
Σ
}
Γ
:
Lemma
FG_CG_iter_refinement
st
st
'
(
τ
i
:
D
)
l
Δ
{
τ
P
:
∀
ww
,
PersistentP
(
τ
i
ww
)
}
Γ
:
inv
stackN
(
sinv
τ
i
st
st
'
l
)
-
∗
{
⊤
,
⊤
;
τ
i
::
Δ
;
Γ
}
⊨
FG_read_iter
$
/
LitV
(
Loc
st
)
≤
log
≤
CG_snap_iter
$
/
LitV
(
Loc
st
'
)
$
/
LitV
(
Loc
l
)
:
TArrow
(
TArrow
(
TVar
0
)
TUnit
)
TUnit
.
Proof
.
...
...
@@ -234,7 +248,7 @@ replace ((rec: "pop" "st" <> :=
rel_rec_r
.
rel_load_l_atomic
.
iInv
stackN
as
(
istk
v
h
)
"[Hoe [Hst' [Hst [#HLK Hl]]]]"
"Hclose"
.
iInv
stackN
as
(
istk
v
h
)
"[Hoe [Hst' [Hst [#HLK Hl]]]]"
"Hclose"
.
iDestruct
(
stack_owns_later_open_close
with
"Hoe Histk"
)
as
"[Histk_i Hoe]"
.
iExists
_.
iFrame
"Histk_i"
.
iModIntro
.
iNext
.
iIntros
"Histk_i /="
.
...
...
@@ -299,7 +313,7 @@ Section Full_refinement.
end
.
(
*
∀
α
.
(
α
→
Unit
)
*
(
Unit
→
Unit
+
α
)
*
((
α
→
Unit
)
→
Unit
)
*
)
Lemma
FG_CG_stack_refinement
`
{
stackPreG
Σ
,
logrelG
Σ
}
Δ
Γ
:
Lemma
FG_CG_stack_refinement
`
{
SPG
:
stackPreG
Σ
,
logrelG
Σ
}
Δ
Γ
:
{
⊤
,
⊤
;
Δ
;
Γ
}
⊨
FG_stack
≤
log
≤
CG_stack
:
TForall
(
TProd
(
TProd
(
TArrow
(
TVar
0
)
TUnit
)
(
TArrow
TUnit
(
TSum
TUnit
(
TVar
0
))))
...
...
@@ -330,10 +344,10 @@ Section Full_refinement.
iMod
(
own_alloc
(
●
(
∅
:
stackUR
)))
as
(
γ
)
"Hemp"
;
first
done
.
set
(
istkG
:=
StackG
_
_
γ
).
change
γ
with
(
@
stack_name
_
istkG
).
change
(
@
stack_pre_inG
_
H
)
with
(
@
stack_inG
_
istkG
).
clearbody
istkG
.
clear
γ
H1
.
change
(
@
stack_pre_inG
_
SPG
)
with
(
@
stack_inG
_
istkG
).
clearbody
istkG
.
clear
γ
SPG
.
iAssert
(
@
stack_owns
_
istkG
_
∅
)
with
"[Hemp]"
as
"Hoe"
.
{
rewrite
/
stack_owns
big_sepM_empty
fmap_empty
.
{
rewrite
/
stack_owns
/
prestack_owns
big_sepM_empty
fmap_empty
.
iFrame
"Hemp"
.
}
iMod
(
stack_owns_alloc
with
"[$Hoe $Histk]"
)
as
"[Hoe #Histk]"
.
iAssert
(
StackLink
τ
i
(#
istk
,
FoldV
(
InjLV
(
LitV
Unit
))))
with
"[Histk]"
as
"#HLK"
.
...
...
@@ -368,6 +382,7 @@ Section Full_refinement.
replace_r
((
CG_locked_push
$
/
LitV
(
Loc
st
'
)
$
/
LitV
(
Loc
l
))
v2
)
%
E
.
{
unlock
CG_locked_push
.
simpl_subst
/=
.
reflexivity
.
}
iApply
(
FG_CG_push_refinement
with
"Hinv Hτ"
).
{
solve_ndisj
.
}
-
replace_l
(
FG_pop
$
/
LitV
(
Loc
st
))
%
E
.
{
unlock
FG_pop
.
by
simpl_subst
/=
.
}
replace_r
(
CG_locked_pop
$
/
LitV
(
Loc
st
'
)
$
/
LitV
(
Loc
l
))
%
E
.
...
...
theories/examples/stack/stack_rules.v
View file @
d6237350
...
...
@@ -12,67 +12,72 @@ Class stackPreG Σ := StackPreG { stack_pre_inG :> authG Σ stackUR }.
Definition
stack
Σ
:
gFunctors
:=
#[
auth
Σ
stackUR
].
Instance
subG_stackPreG
{
Σ
}
:
subG
stack
Σ
Σ
→
stackPreG
Σ
.
Proof
.
solve_inG
.
Qed
.
(
*
Instance
stackG_stackPreG
{
Σ
}
:
stackG
Σ
→
stackPreG
Σ
.
*
)
(
*
Proof
.
intros
[
S
?
].
by
constructor
.
Qed
.
*
)
Definition
stack_mapsto
`
{
stackG
Σ
}
(
l
:
loc
)
(
v
:
val
)
:
iProp
Σ
:=
own
stack_name
(
◯
{
[
l
:=
to_agree
v
]
}
).
Definition
prestack_mapsto
`
{
authG
Σ
stackUR
}
(
γ
:
gname
)
(
l
:
loc
)
(
v
:
val
)
:
iProp
Σ
:=
own
γ
(
◯
{
[
l
:=
to_agree
v
]
}
).
Definition
stack_mapsto
`
{
stackG
Σ
}
l
v
:
iProp
Σ
:=
prestack_mapsto
stack_name
l
v
.
Notation
"l ↦ˢᵗᵏ v"
:=
(
stack_mapsto
l
v
)
(
at
level
20
)
:
uPred_scope
.
Section
Rules
.
Context
`
{
stackG
Σ
}
.
Section
Rules_pre
.
Context
`
{
authG
Σ
stackUR
}
.
Variable
(
γ
:
gname
).
Notation
D
:=
(
prodC
valC
valC
-
n
>
iProp
Σ
).
Notation
"l ↦ˢᵗᵏ v"
:=
(
prestack_mapsto
γ
l
v
)
(
at
level
20
)
:
uPred_scope
.
Global
Instance
stack_mapsto_persistent
l
v
:
PersistentP
(
l
↦ˢᵗᵏ
v
).
Proof
.
apply
_.
Qed
.
(
*
TODO
:
this
is
bad
*
)
Lemma
stack_mapstos_agree_uncurried
l
v
w
:
l
↦ˢᵗᵏ
v
∗
l
↦ˢᵗᵏ
w
⊢
⌜
v
=
w
⌝
.
Lemma
prestack_mapstos_agree_uncurried
l
v
w
:
l
↦ˢᵗᵏ
v
∗
l
↦ˢᵗᵏ
w
⊢
⌜
v
=
w
⌝
.
Proof
.
rewrite
-
own_op
-
auth_frag_op
op_singleton
.
change
(
own
stack_name
(
◯
{
[
l
:=
to_agree
v
⋅
to_agree
w
]
}
))
with
(
auth_own
stack_name
{
[
l
:=
to_agree
v
⋅
to_agree
w
]
}
).
change
(
own
γ
(
◯
{
[
l
:=
to_agree
v
⋅
to_agree
w
]
}
))
with
(
auth_own
γ
{
[
l
:=
to_agree
v
⋅
to_agree
w
]
}
).
rewrite
auth_own_valid
.
iIntros
"Hvalid"
.
iDestruct
"Hvalid"
as
%
Hvalid
.
rewrite
singleton_valid
in
Hvalid
*
.
intros
Hagree
.
by
rewrite
(
agree_op_inv
'
v
w
Hagree
).
Qed
.
Lemma
stack_mapstos_agree
l
v
w
:
l
↦ˢᵗᵏ
v
-
∗
l
↦ˢᵗᵏ
w
-
∗
⌜
v
=
w
⌝
.
Lemma
pre
stack_mapstos_agree
l
v
w
:
l
↦ˢᵗᵏ
v
-
∗
l
↦ˢᵗᵏ
w
-
∗
⌜
v
=
w
⌝
.
Proof
.
iIntros
"??"
.
iApply
stack_mapstos_agree_uncurried
.
by
iFrame
.
iApply
pre
stack_mapstos_agree_uncurried
.
by
iFrame
.
Qed
.
(
*
stacklink
Q
:=
{
((
Loc
l
),
nil
)
∣
l
↦ˢᵗᵏ
(
InjL
#())
}
∪
{
((
Loc
l
),
cons
y2
z2
)
∣
∃
y1
z1
,
l
↦ˢᵗᵏ
(
y1
,
z1
)
∗
(
y1
,
y2
)
∈
Q
∗
▷
stacklink
Q
(
z1
,
z2
)
}*
)
Program
Definition
StackLink_pre
(
Q
:
D
)
:
D
-
n
>
D
:=
λ
ne
P
v
,
Program
Definition
pre
StackLink_pre
(
Q
:
D
)
:
D
-
n
>
D
:=
λ
ne
P
v
,
(
∃
(
l
:
loc
)
w
,
⌜
v
.1
=
#
l
⌝
∗
l
↦ˢᵗᵏ
w
∗
((
⌜
w
=
InjLV
#()
⌝
∧
⌜
v
.2
=
FoldV
(
InjLV
#())
⌝
)
∨
(
∃
y1
z1
y2
z2
,
⌜
w
=
InjRV
(
PairV
y1
(
FoldV
z1
))
⌝
∗
⌜
v
.2
=
FoldV
(
InjRV
(
PairV
y2
z2
))
⌝
∗
Q
(
y1
,
y2
)
∗
▷
P
(
z1
,
z2
))))
%
I
.
Solve
Obligations
with
solve_proper
.
Global
Instance
StackLink_pre_contractive
Q
:
Contractive
(
StackLink_pre
Q
).
Global
Instance
StackLink_pre_contractive
Q
:
Contractive
(
pre
StackLink_pre
Q
).
Proof
.
solve_contractive
.
Qed
.
Definition
StackLink
(
Q
:
D
)
:
D
:=
fixpoint
(
StackLink_pre
Q
).
Definition
pre
StackLink
(
Q
:
D
)
:
D
:=
fixpoint
(
pre
StackLink_pre
Q
).
Lemma
StackLink_unfold
Q
v
:
StackLink
Q
v
≡
(
∃
(
l
:
loc
)
w
,
Lemma
pre
StackLink_unfold
Q
v
:
pre
StackLink
Q
v
≡
(
∃
(
l
:
loc
)
w
,
⌜
v
.1
=
#
l
⌝
∗
l
↦ˢᵗᵏ
w
∗
((
⌜
w
=
InjLV
#()
⌝
∧
⌜
v
.2
=
FoldV
(
InjLV
#())
⌝
)
∨
(
∃
y1
z1
y2
z2
,
⌜
w
=
InjRV
(
PairV
y1
(
FoldV
z1
))
⌝
∗
⌜
v
.2
=
FoldV
(
InjRV
(
PairV
y2
z2
))
⌝
∗
Q
(
y1
,
y2
)
∗
▷
StackLink
Q
(
z1
,
z2
))))
%
I
.
Proof
.
by
rewrite
{
1
}/
StackLink
fixpoint_unfold
.
Qed
.
∗
Q
(
y1
,
y2
)
∗
▷
pre
StackLink
Q
(
z1
,
z2
))))
%
I
.
Proof
.
by
rewrite
{
1
}/
pre
StackLink
fixpoint_unfold
.
Qed
.
Global
Opaque
StackLink
.
(
*
So
that
we
can
only
use
the
unfold
above
.
*
)
Global
Opaque
pre
StackLink
.
(
*
So
that
we
can
only
use
the
unfold
above
.
*
)
Global
Instance
StackLink_persistent
(
Q
:
D
)
v
`
{
∀
vw
,
PersistentP
(
Q
vw
)
}
:
PersistentP
(
StackLink
Q
v
).
Global
Instance
pre
StackLink_persistent
(
Q
:
D
)
v
`
{
∀
vw
,
PersistentP
(
Q
vw
)
}
:
PersistentP
(
pre
StackLink
Q
v
).
Proof
.
iIntros
"H"
.
iL
ö
b
as
"IH"
forall
(
v
).
rewrite
StackLink_unfold
.
iIntros
"H"
.
iL
ö
b
as
"IH"
forall
(
v
).
rewrite
pre
StackLink_unfold
.
iDestruct
"H"
as
(
l
w
)
"[% [#Hl [[% %]|Hr]]]"
;
subst
.
{
iExists
l
,
_
;
iAlways
;
eauto
.
}
iDestruct
"Hr"
as
(
y1
z1
y2
z2
)
"[% [% [#HQ Hrec]]]"
;
subst
.
...
...
@@ -87,14 +92,12 @@ Section Rules.
h
!!
i
=
None
→
●
h
~~>
●
(
<
[
i
:=
to_agree
v
]
>
h
)
⋅
◯
{
[
i
:=
to_agree
v
]
}
.
Proof
.
intros
.
by
apply
auth_update_alloc
,
alloc_singleton_local_update
.
Qed
.
Context
`
{
logrelG
Σ
}
.
Definition
stack_owns
(
h
:
gmap
loc
val
)
:
iProp
Σ
:=
(
own
stack_name
(
●
(
to_agree
<
$
>
h
:
stackUR
))
Definition
prestack_owns
`
{
logrelG
Σ
}
(
h
:
gmap
loc
val
)
:
iProp
Σ
:=
(
own
γ
(
●
(
to_agree
<
$
>
h
:
stackUR
))
∗
[
∗
map
]
l
↦
v
∈
h
,
l
↦ᵢ
v
)
%
I
.
Lemma
stack_owns_alloc
h
l
v
:
stack_owns
h
∗
l
↦ᵢ
v
==
∗
stack_owns
(
<
[
l
:=
v
]
>
h
)
∗
l
↦ˢᵗᵏ
v
.
Lemma
pre
stack_owns_alloc
`
{
logrelG
Σ
}
h
l
v
:
pre
stack_owns
h
∗
l
↦ᵢ
v
==
∗
pre
stack_owns
(
<
[
l
:=
v
]
>
h
)
∗
l
↦ˢᵗᵏ
v
.
Proof
.
iIntros
"[[Hown Hall] Hl]"
.
iDestruct
(
own_valid
with
"Hown"
)
as
%
Hvalid
.
...
...
@@ -107,14 +110,14 @@ Section Rules.
eapply
(
alloc_singleton_local_update
_
l
(
to_agree
v
)).
-
rewrite
lookup_fmap
Hhl
.
by
compute
.
-
by
compute
.
-
iModIntro
.
rewrite
/
stack_owns
.
rewrite
fmap_insert
.
-
iModIntro
.
rewrite
/
pre
stack_owns
.
rewrite
fmap_insert
.
iFrame
"Hown Hl'"
.
iApply
big_sepM_insert
;
eauto
.
by
iFrame
.
}
Qed
.
Lemma
stack_owns_open_close
h
l
v
:
stack_owns
h
-
∗
l
↦ˢᵗᵏ
v
-
∗
l
↦ᵢ
v
∗
(
l
↦ᵢ
v
-
∗
stack_owns
h
).
Lemma
pre
stack_owns_open_close
`
{
logrelG
Σ
}
h
l
v
:
pre
stack_owns
h
-
∗
l
↦ˢᵗᵏ
v
-
∗
l
↦ᵢ
v
∗
(
l
↦ᵢ
v
-
∗
pre
stack_owns
h
).
Proof
.
iIntros
"[Howns Hls] Hl"
.
iDestruct
(
own_valid_2
with
"Howns Hl"
)
...
...
@@ -125,10 +128,48 @@ Section Rules.
move
=>
[
v
'
[
Hl
Hav
]];
subst
.
apply
to_agree_included
in
Hav
'
;
setoid_subst
.
iDestruct
(
big_sepM_lookup_acc
with
"Hls"
)
as
"[$ Hclose]"
;
first
done
.
iIntros
"Hl'"
.
rewrite
/
stack_owns
.
iFrame
"Howns"
.
by
iApply
"Hclose"
.
iIntros
"Hl'"
.
rewrite
/
pre
stack_owns
.
iFrame
"Howns"
.
by
iApply
"Hclose"
.
Qed
.
Lemma
stack_owns_later_open_close
h
l
v
:
Lemma
prestack_owns_later_open_close
`
{
logrelG
Σ
}
h
l
v
:
▷
prestack_owns
h
-
∗
l
↦ˢᵗᵏ
v
-
∗
▷
(
l
↦ᵢ
v
∗
(
l
↦ᵢ
v
-
∗
prestack_owns
h
)).
Proof
.
iIntros
"H1 H2"
.
iNext
;
by
iApply
(
prestack_owns_open_close
with
"H1"
).
Qed
.
End
Rules_pre
.
Section
Rules
.
Context
`
{
stackG
Σ
}
.
Notation
D
:=
(
prodC
valC
valC
-
n
>
iProp
Σ
).
Definition
stack_owns
`
{
logrelG
Σ
}
:=
prestack_owns
stack_name
.
Lemma
stack_mapstos_agree
l
v
w
:
l
↦ˢᵗᵏ
v
-
∗
l
↦ˢᵗᵏ
w
-
∗
⌜
v
=
w
⌝
.
Proof
.
apply
prestack_mapstos_agree
.
Qed
.
Lemma
stack_owns_alloc
`
{
logrelG
Σ
}
h
l
v
:
stack_owns
h
∗
l
↦ᵢ
v
==
∗
stack_owns
(
<
[
l
:=
v
]
>
h
)
∗
l
↦ˢᵗᵏ
v
.
Proof
.
apply
prestack_owns_alloc
.
Qed
.
Lemma
stack_owns_open_close
`
{
logrelG
Σ
}
h
l
v
:
stack_owns
h
-
∗
l
↦ˢᵗᵏ
v
-
∗
l
↦ᵢ
v
∗
(
l
↦ᵢ
v
-
∗
stack_owns
h
).
Proof
.
apply
prestack_owns_open_close
.
Qed
.
Lemma
stack_owns_later_open_close
`
{
logrelG
Σ
}
h
l
v
:
▷
stack_owns
h
-
∗
l
↦ˢᵗᵏ
v
-
∗
▷
(
l
↦ᵢ
v
∗
(
l
↦ᵢ
v
-
∗
stack_owns
h
)).
Proof
.
iIntros
"H1 H2"
.
iNext
;
by
iApply
(
stack_owns_open_close
with
"H1"
).
Qed
.
Proof
.
apply
prestack_owns_later_open_close
.
Qed
.
Definition
StackLink
Q
v
:=
preStackLink
stack_name
Q
v
.
Lemma
StackLink_unfold
Q
v
:
StackLink
Q
v
≡
(
∃
(
l
:
loc
)
w
,
⌜
v
.1
=
#
l
⌝
∗
l
↦ˢᵗᵏ
w
∗
((
⌜
w
=
InjLV
#()
⌝
∧
⌜
v
.2
=
FoldV
(
InjLV
#())
⌝
)
∨
(
∃
y1
z1
y2
z2
,
⌜
w
=
InjRV
(
PairV
y1
(
FoldV
z1
))
⌝
∗
⌜
v
.2
=
FoldV
(
InjRV
(
PairV
y2
z2
))
⌝
∗
Q
(
y1
,
y2
)
∗
▷
StackLink
Q
(
z1
,
z2
))))
%
I
.
Proof
.
by
rewrite
/
StackLink
preStackLink_unfold
.
Qed
.
Global
Instance
StackLink_persistent
(
Q
:
D
)
v
`
{
∀
vw
,
PersistentP
(
Q
vw
)
}
:
PersistentP
(
StackLink
Q
v
).
Proof
.
apply
_.
Qed
.
Global
Opaque
StackLink
.
End
Rules
.
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