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
Iris
examples
Commits
cb8a3ba6
Commit
cb8a3ba6
authored
Nov 22, 2017
by
Ralf Jung
Browse files
port to savedPred
parent
15c2936d
Changes
2
Hide whitespace changes
Inline
Side-by-side
opam
View file @
cb8a3ba6
...
...
@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris_atomic"]
depends: [
"coq-iris" { (= "dev.2017-11-
18.1
") | (= "dev") }
"coq-iris" { (= "dev.2017-11-
22.0
") | (= "dev") }
]
theories/flat.v
View file @
cb8a3ba6
...
...
@@ -50,12 +50,12 @@ Definition reqR := prodR fracR (agreeR valC). (* request x should be kept same *
Definition
toks
:
Type
:
=
gname
*
gname
*
gname
*
gname
*
gname
.
(* a bunch of tokens to do state transition *)
Class
flatG
Σ
:
=
FlatG
{
req_G
:
>
inG
Σ
reqR
;
sp_G
:
>
saved
AnythingG
Σ
(
▶
(
ofe_funCF
val
idCF
))
sp_G
:
>
saved
PredG
Σ
val
}.
Definition
flat
Σ
:
gFunctors
:
=
#[
GFunctor
(
constRF
reqR
)
;
saved
Anything
Σ
(
▶
(
ofe_funCF
val
idCF
))
].
saved
Pred
Σ
val
].
Instance
subG_flat
Σ
{
Σ
}
:
subG
flat
Σ
Σ
→
flatG
Σ
.
Proof
.
intros
[?%
subG_inG
[?
_
]%
subG_inv
]%
subG_inv
.
split
;
apply
_
.
Qed
.
...
...
@@ -70,7 +70,7 @@ Section proof.
let
'
(
γ
x
,
γ
1
,
_
,
γ
4
,
γ
q
)
:
=
ts
in
(
∃
(
P
:
val
→
iProp
Σ
)
Q
,
own
γ
x
((
1
/
2
)%
Qp
,
to_agree
x
)
∗
P
x
∗
({{
R
∗
P
x
}}
f
x
{{
v
,
R
∗
Q
x
v
}})
∗
saved_
anything
_own
γ
q
(
Next
$
Q
x
)
∗
own
γ
1
(
Excl
())
∗
own
γ
4
(
Excl
()))%
I
.
saved_
pred
_own
γ
q
(
Q
x
)
∗
own
γ
1
(
Excl
())
∗
own
γ
4
(
Excl
()))%
I
.
Definition
received_s
(
ts
:
toks
)
(
x
:
val
)
γ
r
:
=
let
'
(
γ
x
,
_
,
_
,
γ
4
,
_
)
:
=
ts
in
...
...
@@ -79,7 +79,7 @@ Section proof.
Definition
finished_s
(
ts
:
toks
)
(
x
y
:
val
)
:
=
let
'
(
γ
x
,
γ
1
,
_
,
γ
4
,
γ
q
)
:
=
ts
in
(
∃
Q
:
val
→
val
→
iProp
Σ
,
own
γ
x
((
1
/
2
)%
Qp
,
to_agree
x
)
∗
saved_
anything
_own
γ
q
(
Next
$
Q
x
)
∗
own
γ
x
((
1
/
2
)%
Qp
,
to_agree
x
)
∗
saved_
pred
_own
γ
q
(
Q
x
)
∗
Q
x
y
∗
own
γ
1
(
Excl
())
∗
own
γ
4
(
Excl
()))%
I
.
Definition
p_inv
R
(
γ
m
γ
r
:
gname
)
(
ts
:
toks
)
(
p
:
loc
)
:
=
...
...
@@ -99,7 +99,7 @@ Section proof.
Definition
installed_recp
(
ts
:
toks
)
(
x
:
val
)
(
Q
:
val
→
iProp
Σ
)
:
=
let
'
(
γ
x
,
_
,
γ
3
,
_
,
γ
q
)
:
=
ts
in
(
own
γ
3
(
Excl
())
∗
own
γ
x
((
1
/
2
)%
Qp
,
to_agree
x
)
∗
saved_
anything_own
γ
q
(
Next
Q
)
)%
I
.
(
own
γ
3
(
Excl
())
∗
own
γ
x
((
1
/
2
)%
Qp
,
to_agree
x
)
∗
saved_
pred_own
γ
q
Q
)%
I
.
Lemma
install_spec
R
P
Q
(
f
x
:
val
)
(
γ
m
γ
r
:
gname
)
(
s
:
loc
)
:
{{{
inv
N
(
srv_bag
R
γ
m
γ
r
s
)
∗
P
∗
({{
R
∗
P
}}
f
x
{{
v
,
R
∗
Q
v
}})
}}}
...
...
@@ -113,7 +113,7 @@ Section proof.
iMod
(
own_alloc
(
Excl
()))
as
(
γ
3
)
"Ho3"
;
first
done
.
iMod
(
own_alloc
(
Excl
()))
as
(
γ
4
)
"Ho4"
;
first
done
.
iMod
(
own_alloc
(
1
%
Qp
,
to_agree
x
))
as
(
γ
x
)
"Hx"
;
first
done
.
iMod
(
saved_
anything_alloc
(
F
:
=(
▶
(
ofe_funCF
val
idCF
)))
(
Next
Q
)
)
as
(
γ
q
)
"#?"
.
iMod
(
saved_
pred_alloc
Q
)
as
(
γ
q
)
"#?"
.
iDestruct
(
own_update
with
"Hx"
)
as
">[Hx1 Hx2]"
;
first
by
apply
pair_l_frac_op_1'
.
iModIntro
.
wp_let
.
wp_bind
(
push
_
_
).
iMod
(
inv_alloc
N
_
(
p_inv
R
γ
m
γ
r
(
γ
x
,
γ
1
,
γ
3
,
γ
4
,
γ
q
)
p
)
...
...
@@ -181,7 +181,7 @@ Section proof.
Definition
own_
γ
3
(
ts
:
toks
)
:
=
let
'
(
_
,
_
,
γ
3
,
_
,
_
)
:
=
ts
in
own
γ
3
(
Excl
()).
Definition
finished_recp
(
ts
:
toks
)
(
x
y
:
val
)
:
=
let
'
(
γ
x
,
_
,
_
,
_
,
γ
q
)
:
=
ts
in
(
∃
Q
,
own
γ
x
((
1
/
2
)%
Qp
,
to_agree
x
)
∗
saved_
anything
_own
γ
q
(
Next
$
Q
x
)
∗
Q
x
y
)%
I
.
(
∃
Q
,
own
γ
x
((
1
/
2
)%
Qp
,
to_agree
x
)
∗
saved_
pred
_own
γ
q
(
Q
x
)
∗
Q
x
y
)%
I
.
Lemma
loop_iter_doOp_spec
R
(
γ
m
γ
r
:
gname
)
xs
:
∀
(
hd
:
loc
),
...
...
@@ -290,13 +290,8 @@ Section proof.
iNext
.
iIntros
(?
?)
"Hs"
.
iDestruct
"Hs"
as
(
Q'
)
"(Hx' & HoQ' & HQ')"
.
destruct
(
decide
(
x
=
a
))
as
[->|
Hneq
].
-
iDestruct
(
saved_anything_agree
with
"[$HoQ] [HoQ']"
)
as
"Heq"
;
first
by
iFrame
.
(* FIXME:
iDestruct (uPred.later_equivI with "Heq") as "Heq".
does the wrong thing. *)
rewrite
uPred
.
later_equivI
.
wp_let
.
iDestruct
(
uPred
.
ofe_funC_equivI
with
"Heq"
)
as
"Heq"
.
iSpecialize
(
"Heq"
$!
a0
).
by
iRewrite
-
"Heq"
in
"HQ'"
.
-
iDestruct
(
saved_pred_agree
_
_
_
a0
with
"[$HoQ] [HoQ']"
)
as
"Heq"
;
first
by
iFrame
.
wp_let
.
by
iRewrite
-
"Heq"
in
"HQ'"
.
-
iExFalso
.
iCombine
"Hx"
"Hx'"
as
"Hx"
.
iDestruct
(
own_valid
with
"Hx"
)
as
%[
_
H1
].
rewrite
//=
in
H1
.
...
...
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