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
08fc0696
Commit
08fc0696
authored
Nov 01, 2016
by
Ralf Jung
Browse files
update to latest iris (bb5e21f21)
parent
f8ce13c3
Changes
11
Hide whitespace changes
Inline
Side-by-side
Makefile.coq
View file @
08fc0696
...
...
@@ -2,7 +2,7 @@
## v # The Coq Proof Assistant ##
## <O___,, # INRIA - CNRS - LIX - LRI - PPS ##
## \VV/ # ##
## // # Makefile automagically generated by coq_makefile V8.5pl
2
##
## // # Makefile automagically generated by coq_makefile V8.5pl
3
##
#############################################################################
# WARNING
...
...
atomic.v
View file @
08fc0696
(* Logically atomic triple *)
From
iris
.
program_logic
Require
Export
hoare
weakestpre
pviewshifts
.
From
iris
.
base_logic
Require
Export
fancy_updates
.
From
iris
.
program_logic
Require
Export
hoare
weakestpre
.
From
iris
.
prelude
Require
Export
coPset
.
Import
uPred
.
Section
atomic
.
Context
`
{
irisG
Λ
Σ
}
(
A
:
Type
).
(* TODO RJ: IMHO it would make more sense to have the outer mask first, after all, that's what the shifts "starts" with. *)
(* TODO RJ: Don't define atomic_triple_base; everybody should only ever use atomic_triple anyway. *)
(* TODO RJ: We probably will want to make `A` an implicit parameter. *)
Definition
atomic_triple_base
(
α
:
A
→
iProp
Σ
)
(* atomic pre-condition *)
(
β
:
A
→
val
_
→
iProp
Σ
)
(* atomic post-condition *)
...
...
atomic_incr.v
View file @
08fc0696
From
iris
.
program_logic
Require
Export
weakestpre
wsat
.
From
iris
.
program_logic
Require
Export
weakestpre
.
From
iris
.
heap_lang
Require
Export
lang
proofmode
notation
.
From
iris_atomic
Require
Import
atomic
.
From
iris
.
proofmode
Require
Import
tactics
.
From
iris
.
prelude
Require
Import
coPset
.
From
iris
.
heap_lang
.
lib
Require
Import
par
.
Section
incr
.
Context
`
{!
heapG
Σ
}
(
N
:
namespace
).
...
...
@@ -34,26 +35,25 @@ Section incr.
iIntros
"!# HP"
.
wp_rec
.
wp_bind
(!
_
)%
E
.
i
Vs
(
"Hvs"
with
"HP"
)
as
(
x
)
"[Hl [Hvs' _]]"
.
i
Mod
(
"Hvs"
with
"HP"
)
as
(
x
)
"[Hl [Hvs' _]]"
.
wp_load
.
i
Vs
(
"Hvs'"
with
"Hl"
)
as
"HP"
.
i
Vs
Intro
.
wp_let
.
wp_bind
(
CAS
_
_
_
).
wp_op
.
i
Vs
(
"Hvs"
with
"HP"
)
as
(
x'
)
"[Hl Hvs']"
.
i
Mod
(
"Hvs'"
with
"Hl"
)
as
"HP"
.
i
Mod
Intro
.
wp_let
.
wp_bind
(
CAS
_
_
_
).
wp_op
.
i
Mod
(
"Hvs"
with
"HP"
)
as
(
x'
)
"[Hl Hvs']"
.
destruct
(
decide
(
x
=
x'
)).
-
subst
.
iDestruct
"Hvs'"
as
"[_ Hvs']"
.
iSpecialize
(
"Hvs'"
$!
#
x'
).
wp_cas_suc
.
i
Vs
(
"Hvs'"
with
"[Hl]"
)
as
"HQ"
;
first
by
iFrame
.
i
Vs
Intro
.
wp_if
.
i
Vs
Intro
.
by
iExists
x'
.
i
Mod
(
"Hvs'"
with
"[Hl]"
)
as
"HQ"
;
first
by
iFrame
.
i
Mod
Intro
.
wp_if
.
i
Mod
Intro
.
by
iExists
x'
.
-
iDestruct
"Hvs'"
as
"[Hvs' _]"
.
wp_cas_fail
.
i
Vs
(
"Hvs'"
with
"[Hl]"
)
as
"HP"
;
first
by
iFrame
.
i
Vs
Intro
.
wp_if
.
by
iApply
"IH"
.
i
Mod
(
"Hvs'"
with
"[Hl]"
)
as
"HP"
;
first
by
iFrame
.
i
Mod
Intro
.
wp_if
.
by
iApply
"IH"
.
Qed
.
End
incr
.
From
iris
.
heap_lang
.
lib
Require
Import
par
.
Section
user
.
Context
`
{!
heapG
Σ
,
!
spawnG
Σ
}
(
N
:
namespace
).
...
...
@@ -72,7 +72,7 @@ Section user.
rewrite
/
incr_2
.
wp_let
.
wp_alloc
l
as
"Hl"
.
i
Vs
(
inv_alloc
N
_
(
∃
x'
:
Z
,
l
↦
#
x'
)%
I
with
"[Hl]"
)
as
"#?"
;
first
eauto
.
i
Mod
(
inv_alloc
N
_
(
∃
x'
:
Z
,
l
↦
#
x'
)%
I
with
"[Hl]"
)
as
"#?"
;
first
eauto
.
wp_let
.
wp_bind
(
_
||
_
)%
E
.
iApply
(
wp_par
(
λ
_
,
True
%
I
)
(
λ
_
,
True
%
I
)).
...
...
@@ -85,14 +85,14 @@ Section user.
(* open the invariant *)
iInv
N
as
(
x'
)
">Hl'"
"Hclose"
.
(* mask magic *)
i
Vs
(
pvs
_intro_mask'
(
⊤
∖
nclose
N
)
heapN
)
as
"Hvs"
;
first
set_solver
.
i
Vs
Intro
.
iExists
x'
.
iFrame
"Hl'"
.
iSplit
.
i
Mod
(
fupd
_intro_mask'
(
⊤
∖
nclose
N
)
heapN
)
as
"Hvs"
;
first
set_solver
.
i
Mod
Intro
.
iExists
x'
.
iFrame
"Hl'"
.
iSplit
.
+
(* provide a way to rollback *)
iIntros
"Hl'"
.
i
Vs
"Hvs"
.
i
Vs
(
"Hclose"
with
"[Hl']"
)
;
eauto
.
i
Mod
"Hvs"
.
i
Mod
(
"Hclose"
with
"[Hl']"
)
;
eauto
.
+
(* provide a way to commit *)
iIntros
(
v
)
"[Heq Hl']"
.
i
Vs
"Hvs"
.
i
Vs
(
"Hclose"
with
"[Hl']"
)
;
eauto
.
i
Mod
"Hvs"
.
i
Mod
(
"Hclose"
with
"[Hl']"
)
;
eauto
.
-
iDestruct
"Hincr"
as
"#HIncr"
.
iSplitL
;
[|
iSplitL
]
;
try
(
iApply
wp_wand_r
;
iSplitL
;
[
by
iApply
"HIncr"
|
auto
]).
...
...
atomic_pcas.v
View file @
08fc0696
...
...
@@ -35,7 +35,7 @@ Section atomic_pair.
Lemma
pcas_seq_spec
:
seq_spec
N
pcas_seq
ϕ
α
β
⊤
.
Proof
.
iIntros
(
_
l
)
"!# _"
.
wp_seq
.
i
Vs
Intro
.
iPureIntro
.
iIntros
(
_
l
)
"!# _"
.
wp_seq
.
i
Mod
Intro
.
iPureIntro
.
iIntros
(
x
Φ
g
HN
)
"(#Hh & Hg & #Hα & HΦ)"
.
iDestruct
"Hg"
as
(
l1
l2
x1
x2
)
"(% & % & Hl1 & Hl2)"
.
iDestruct
"Hα"
as
(
a
b
)
"%"
.
...
...
atomic_sync.v
View file @
08fc0696
...
...
@@ -54,7 +54,7 @@ Section atomic_sync.
⊢
WP
(
sync
mk_syncer
)
f_seq
l
{{
f
,
∃
γ
,
gHalf
γ
g0
★
∀
x
,
□
atomic_triple'
α
β
Ei
⊤
f
x
γ
}}.
Proof
.
iIntros
(
g0
HN
Hseq
Hsync
)
"[#Hh Hϕ]"
.
i
Vs
(
own_alloc
(((
1
/
2
)%
Qp
,
DecAgree
g0
)
⋅
((
1
/
2
)%
Qp
,
DecAgree
g0
)))
as
(
γ
)
"[Hg1 Hg2]"
.
i
Mod
(
own_alloc
(((
1
/
2
)%
Qp
,
DecAgree
g0
)
⋅
((
1
/
2
)%
Qp
,
DecAgree
g0
)))
as
(
γ
)
"[Hg1 Hg2]"
.
{
by
rewrite
pair_op
dec_agree_idemp
.
}
repeat
wp_let
.
wp_bind
(
mk_syncer
_
).
iApply
(
Hsync
(
∃
g
:
A
,
ϕ
l
g
★
gHalf
γ
g
)%
I
)=>//.
iFrame
"Hh"
.
...
...
@@ -75,23 +75,23 @@ Section atomic_sync.
-
iApply
(
"Hsynced"
with
"[]"
)=>//.
iAlways
.
iIntros
"[HR HP]"
.
iDestruct
"HR"
as
(
g
)
"[Hϕ Hg1]"
.
(* we should view shift at this point *)
iDestruct
(
"Hvss"
with
"HP"
)
as
"Hvss'"
.
iApply
pvs
_wp
.
i
Vs
"Hvss'"
.
iDestruct
"Hvss'"
as
(?)
"[[Hg2 #Hα] [Hvs1 _]]"
.
iDestruct
(
"Hvss"
with
"HP"
)
as
"Hvss'"
.
iApply
fupd
_wp
.
i
Mod
"Hvss'"
.
iDestruct
"Hvss'"
as
(?)
"[[Hg2 #Hα] [Hvs1 _]]"
.
iDestruct
(
m_frag_agree
with
"[Hg1 Hg2]"
)
as
%
Heq
;
first
iFrame
.
subst
.
i
Vs
(
"Hvs1"
with
"[Hg2]"
)
as
"HP"
;
first
by
iFrame
.
i
Vs
Intro
.
iApply
H
=>//.
i
Mod
(
"Hvs1"
with
"[Hg2]"
)
as
"HP"
;
first
by
iFrame
.
i
Mod
Intro
.
iApply
H
=>//.
iFrame
"Hh Hϕ"
.
iSplitR
;
first
done
.
iIntros
(
ret
g'
)
"Hϕ' Hβ"
.
i
Vs
(
"Hvss"
with
"HP"
)
as
(
g''
)
"[[Hg'' _] [_ Hvs2]]"
.
i
Mod
(
"Hvss"
with
"HP"
)
as
(
g''
)
"[[Hg'' _] [_ Hvs2]]"
.
iSpecialize
(
"Hvs2"
$!
ret
).
iDestruct
(
m_frag_agree'
with
"[Hg'' Hg1]"
)
as
"[Hg %]"
;
first
iFrame
.
subst
.
rewrite
Qp_div_2
.
iAssert
(|=
r
=>
own
γ
(((
1
/
2
)%
Qp
,
DecAgree
g'
)
⋅
((
1
/
2
)%
Qp
,
DecAgree
g'
)))%
I
with
"[Hg]"
as
"
==
>[Hg1 Hg2]"
.
iAssert
(|==>
own
γ
(((
1
/
2
)%
Qp
,
DecAgree
g'
)
⋅
((
1
/
2
)%
Qp
,
DecAgree
g'
)))%
I
with
"[Hg]"
as
">[Hg1 Hg2]"
.
{
iApply
own_update
;
last
by
iAssumption
.
apply
cmra_update_exclusive
.
by
rewrite
pair_op
dec_agree_idemp
.
}
i
Vs
(
"Hvs2"
with
"[Hg1 Hβ]"
).
i
Mod
(
"Hvs2"
with
"[Hg1 Hβ]"
).
{
iExists
g'
.
iFrame
.
}
i
Vs
Intro
.
iSplitL
"Hg2 Hϕ'"
;
last
done
.
i
Mod
Intro
.
iSplitL
"Hg2 Hϕ'"
;
last
done
.
iExists
g'
.
by
iFrame
.
-
iIntros
(?)
"?"
.
by
iExists
g0
.
Qed
.
...
...
evmap.v
View file @
08fc0696
(* evmap.v -- generalized heap-like monoid composite *)
From
iris
.
program_logic
Require
Export
invariants
weakestpre
.
From
iris
.
base_logic
Require
Export
invariants
.
From
iris
.
program_logic
Require
Export
weakestpre
.
From
iris
.
algebra
Require
Export
auth
frac
gmap
dec_agree
.
From
iris
.
proofmode
Require
Import
tactics
.
...
...
@@ -58,7 +59,7 @@ Section evmapR.
(* Alloc a new mapsto *)
Lemma
evmap_alloc
γ
m
m
k
v
:
m
!!
k
=
None
→
own
γ
m
(
●
m
)
⊢
|=
r
=>
own
γ
m
(
●
(<[
k
:
=
((),
DecAgree
v
)
]>
m
)
⋅
◯
{[
k
:
=
((),
DecAgree
v
)
]}).
own
γ
m
(
●
m
)
⊢
|==>
own
γ
m
(
●
(<[
k
:
=
((),
DecAgree
v
)
]>
m
)
⋅
◯
{[
k
:
=
((),
DecAgree
v
)
]}).
Proof
.
iIntros
(?)
"Hm"
.
iDestruct
(
own_update
with
"Hm"
)
as
"?"
;
last
by
iAssumption
.
...
...
flat.v
View file @
08fc0696
(* Flat Combiner *)
From
iris
.
program_logic
Require
Export
weakestpre
saved_prop
.
From
iris
.
program_logic
Require
Export
weakestpre
.
From
iris
.
heap_lang
Require
Export
lang
.
From
iris
.
heap_lang
Require
Import
proofmode
notation
.
From
iris
.
heap_lang
.
lib
Require
Import
spin_lock
.
From
iris
.
algebra
Require
Import
auth
upred
frac
agree
excl
dec_agree
upred_big_op
gset
gmap
.
From
iris
.
algebra
Require
Import
auth
frac
agree
excl
dec_agree
gset
gmap
.
From
iris
.
base_logic
Require
Import
big_op
saved_prop
.
From
iris_atomic
Require
Import
misc
peritem
sync
evmap
.
Definition
doOp
:
val
:
=
...
...
@@ -145,12 +146,12 @@ Section proof.
Proof
.
iIntros
(
HN
)
"(#Hh & #? & Hpx & Hf & HΦ)"
.
wp_seq
.
wp_let
.
wp_let
.
wp_alloc
p
as
"Hl"
.
iApply
pvs
_wp
.
i
Vs
(
own_alloc
(
Excl
()))
as
(
γ
1
)
"Ho1"
;
first
done
.
i
Vs
(
own_alloc
(
Excl
()))
as
(
γ
3
)
"Ho3"
;
first
done
.
i
Vs
(
own_alloc
(
Excl
()))
as
(
γ
4
)
"Ho4"
;
first
done
.
i
Vs
(
own_alloc
(
1
%
Qp
,
DecAgree
x
))
as
(
γ
x
)
"Hx"
;
first
done
.
i
Vs
(
saved_prop_alloc
(
F
:
=(
cofe_funCF
val
idCF
))
(
Q
x
)%
I
)
as
(
γ
q
)
"#?"
.
iApply
fupd
_wp
.
i
Mod
(
own_alloc
(
Excl
()))
as
(
γ
1
)
"Ho1"
;
first
done
.
i
Mod
(
own_alloc
(
Excl
()))
as
(
γ
3
)
"Ho3"
;
first
done
.
i
Mod
(
own_alloc
(
Excl
()))
as
(
γ
4
)
"Ho4"
;
first
done
.
i
Mod
(
own_alloc
(
1
%
Qp
,
DecAgree
x
))
as
(
γ
x
)
"Hx"
;
first
done
.
i
Mod
(
saved_prop_alloc
(
F
:
=(
cofe_funCF
val
idCF
))
(
Q
x
)%
I
)
as
(
γ
q
)
"#?"
.
iInv
N
as
"[Hrs >Hm]"
"Hclose"
.
iDestruct
"Hm"
as
(
m
)
"[Hm HRm]"
.
destruct
(
m
!!
p
)
eqn
:
Heqn
.
...
...
@@ -158,19 +159,19 @@ Section proof.
iDestruct
(
big_sepM_delete
(
fun
p
_
=>
∃
v
:
val
,
p
↦
{
1
/
2
}
v
)%
I
m
with
"HRm"
)
as
"[Hp HRm]"
=>//.
iDestruct
"Hp"
as
(?)
"Hp"
.
iExFalso
.
iApply
bogus_heap
;
last
by
iFrame
"Hh Hl Hp"
.
auto
.
-
(* fresh name *)
iDestruct
(
evmap_alloc
_
_
_
m
p
(
γ
x
,
γ
1
,
γ
3
,
γ
4
,
γ
q
)
with
"[Hm]"
)
as
"
==
>[Hm1 #Hm2]"
=>//.
iDestruct
(
evmap_alloc
_
_
_
m
p
(
γ
x
,
γ
1
,
γ
3
,
γ
4
,
γ
q
)
with
"[Hm]"
)
as
">[Hm1 #Hm2]"
=>//.
iDestruct
"Hl"
as
"[Hl1 Hl2]"
.
i
Vs
(
"Hclose"
with
"[HRm Hm1 Hl1 Hrs]"
).
i
Mod
(
"Hclose"
with
"[HRm Hm1 Hl1 Hrs]"
).
+
iNext
.
iFrame
.
iExists
(<[
p
:
=
(
∅
,
DecAgree
(
γ
x
,
γ
1
,
γ
3
,
γ
4
,
γ
q
))]>
m
).
iFrame
.
iDestruct
(
big_sepM_insert
_
m
with
"[-]"
)
as
"H"
=>//.
iSplitL
"Hl1"
;
last
by
iAssumption
.
eauto
.
+
iDestruct
(
own_update
with
"Hx"
)
as
"
==
>[Hx1 Hx2]"
;
first
by
apply
pair_l_frac_op_1'
.
i
Vs
Intro
.
wp_let
.
wp_bind
((
push
_
)
_
).
+
iDestruct
(
own_update
with
"Hx"
)
as
">[Hx1 Hx2]"
;
first
by
apply
pair_l_frac_op_1'
.
i
Mod
Intro
.
wp_let
.
wp_bind
((
push
_
)
_
).
iApply
install_push_spec
=>//.
iFrame
"#"
.
rewrite
/
evm
/
installed_s
.
iFrame
.
iSplitL
"Hpx Hf"
.
{
iExists
P
,
Q
.
by
iFrame
.
}
iIntros
"Hhd"
.
wp_seq
.
i
Vs
Intro
.
iIntros
"Hhd"
.
wp_seq
.
i
Mod
Intro
.
iSpecialize
(
"HΦ"
$!
p
(
γ
x
,
γ
1
,
γ
3
,
γ
4
,
γ
q
)
with
"[-Hhd]"
)=>//.
{
rewrite
/
installed_recp
.
iFrame
.
iFrame
"#"
.
}
by
iApply
(
"HΦ"
with
"[]"
).
...
...
@@ -199,34 +200,34 @@ Section proof.
iDestruct
"Hp"
as
(
v'
)
"[>% [Hpinv' >Hahd]]"
.
inversion
H
.
subst
.
iDestruct
"Hpinv'"
as
(
ts
p''
)
"[>% [>#Hevm [Hp | [Hp | [Hp | Hp]]]]]"
;
subst
.
+
iDestruct
"Hp"
as
(
y
)
"(>Hp & Hs)"
.
wp_load
.
i
Vs
(
"Hclose"
with
"[-Hor HR Hev HΦ']"
).
wp_load
.
i
Mod
(
"Hclose"
with
"[-Hor HR Hev HΦ']"
).
{
iNext
.
iFrame
.
iExists
gxs
,
ghd
.
iFrame
"Hghd Hgxs"
.
iExists
m
.
iFrame
"Hom"
.
iDestruct
(
big_sepM_delete
_
m
with
"[-]"
)
as
"?"
=>//.
iFrame
.
iExists
#
p''
.
iSplitR
;
first
done
.
iExists
ts
,
p''
.
iSplitR
;
first
done
.
iFrame
"#"
.
iLeft
.
iExists
y
.
iFrame
.
}
i
Vs
Intro
.
wp_match
.
i
Vs
Intro
.
iApply
(
"HΦ'"
with
"[Hor HR]"
).
iFrame
.
i
Mod
Intro
.
wp_match
.
i
Mod
Intro
.
iApply
(
"HΦ'"
with
"[Hor HR]"
).
iFrame
.
+
iDestruct
"Hp"
as
(
f'
x'
)
"(Hp & Hs)"
.
wp_load
.
destruct
ts
as
[[[[
γ
x
γ
1
]
γ
3
]
γ
4
]
γ
q
].
iDestruct
"Hs"
as
(
P
Q
)
"(Hx & Hpx & Hf' & HoQ & Ho1 & Ho4)"
.
iAssert
(|=
r
=>
own
γ
x
(((
1
/
2
/
2
)%
Qp
,
DecAgree
x'
)
⋅
((
1
/
2
/
2
)%
Qp
,
DecAgree
x'
)))%
I
with
"[Hx]"
as
"
==
>[Hx1 Hx2]"
.
iAssert
(|==>
own
γ
x
(((
1
/
2
/
2
)%
Qp
,
DecAgree
x'
)
⋅
((
1
/
2
/
2
)%
Qp
,
DecAgree
x'
)))%
I
with
"[Hx]"
as
">[Hx1 Hx2]"
.
{
iDestruct
(
own_update
with
"Hx"
)
as
"?"
;
last
by
iAssumption
.
rewrite
-{
1
}(
Qp_div_2
(
1
/
2
)%
Qp
).
by
apply
pair_l_frac_op'
.
}
i
Vs
(
"Hclose"
with
"[-Hf' Ho1 Hx2 HR HoQ HΦ' Hpx]"
).
i
Mod
(
"Hclose"
with
"[-Hf' Ho1 Hx2 HR HoQ HΦ' Hpx]"
).
{
iNext
.
iFrame
.
iExists
gxs
,
ghd
.
iFrame
"Hghd Hgxs"
.
iExists
m
.
iFrame
"Hom"
.
iDestruct
(
big_sepM_delete
_
m
with
"[-]"
)
as
"?"
=>//.
simpl
.
iFrame
.
iExists
#
p''
.
iSplitR
;
auto
.
rewrite
/
allocated
.
iExists
(
γ
x
,
γ
1
,
γ
3
,
γ
4
,
γ
q
),
p''
.
iSplitR
;
auto
.
iFrame
"#"
.
iRight
.
iRight
.
iLeft
.
iExists
f'
,
x'
.
iFrame
.
}
i
Vs
Intro
.
wp_match
.
i
Mod
Intro
.
wp_match
.
wp_proj
.
wp_proj
.
wp_bind
(
f'
_
).
iApply
wp_wand_r
.
iSplitL
"Hpx Hf' HR"
.
{
iApply
"Hf'"
.
iFrame
.
}
iIntros
(
v
)
"[HR HQ]"
.
wp_value
.
i
Vs
Intro
.
iInv
N
as
"[Hs >Hm]"
"Hclose"
.
wp_value
.
i
Mod
Intro
.
iInv
N
as
"[Hs >Hm]"
"Hclose"
.
iDestruct
"Hs"
as
(
xs''
hd'''
)
"[>Hhd [>Hxs HRs]]"
.
iDestruct
"HRs"
as
(
m'
)
"[>Hom HRs]"
.
iDestruct
(
ev_map_witness
_
_
_
m'
with
"[Hevm Hom]"
)
as
%?
;
first
by
iFrame
.
...
...
@@ -251,7 +252,7 @@ Section proof.
rewrite
Qp_div_2
.
wp_store
.
(* now close the invariant *)
iDestruct
(
m_frag_agree'
with
"[Hx Hx2]"
)
as
"[Hx %]"
;
first
iFrame
.
subst
.
rewrite
Qp_div_2
.
i
Vs
(
"Hclose"
with
"[-HR Hor HΦ']"
).
subst
.
rewrite
Qp_div_2
.
i
Mod
(
"Hclose"
with
"[-HR Hor HΦ']"
).
{
iNext
.
iDestruct
"Hp"
as
"[Hp1 Hp2]"
.
iAssert
(
srv_tokm_inv
γ
m
)
with
"[Hp1 HRp Hom2]"
as
"HRp"
.
{
iExists
m2
.
iFrame
.
iApply
(
big_sepM_delete
_
m2
)=>//.
...
...
@@ -276,14 +277,14 @@ Section proof.
iApply
excl_falso
.
iFrame
.
+
destruct
ts
as
[[[[
γ
x
γ
1
]
γ
3
]
γ
4
]
γ
q
].
iDestruct
"Hp"
as
(
x'
y
)
"[Hp Hs]"
.
iDestruct
"Hs"
as
(
Q
)
"(>Hx & HoQ & HQxy & >Ho1 & >Ho4)"
.
wp_load
.
i
Vs
(
"Hclose"
with
"[-HΦ' HR Hor]"
).
wp_load
.
i
Mod
(
"Hclose"
with
"[-HΦ' HR Hor]"
).
{
iNext
.
iFrame
.
iExists
gxs
,
ghd
.
iFrame
"Hghd Hgxs"
.
iExists
m
.
iFrame
"Hom"
.
iDestruct
(
big_sepM_delete
_
m
with
"[-]"
)
as
"?"
=>//.
iFrame
.
iExists
#
p''
.
iSplitR
;
first
auto
.
iExists
(
γ
x
,
γ
1
,
γ
3
,
γ
4
,
γ
q
),
p''
.
iSplitR
;
auto
.
iFrame
"#"
.
iRight
.
iRight
.
iRight
.
iExists
x'
,
y
.
iFrame
.
iExists
Q
.
iFrame
.
}
i
Vs
Intro
.
wp_match
.
i
Mod
Intro
.
wp_match
.
iApply
"HΦ'"
.
iFrame
.
-
apply
to_of_val
.
-
iFrame
"#"
.
iFrame
.
iIntros
"[Hor HR]"
.
...
...
@@ -310,17 +311,17 @@ Section proof.
wp_if
.
wp_bind
(!
_
)%
E
.
iInv
N
as
"[H >Hm]"
"Hclose"
.
iDestruct
"H"
as
(
xs'
hd'
)
"[>Hs [>Hxs HRs]]"
.
wp_load
.
iDestruct
(
dup_is_list'
with
"[Hxs]"
)
as
"
==
>[Hxs1 Hxs2]"
;
first
by
iFrame
.
i
Vs
(
"Hclose"
with
"[Hs Hxs1 HRs Hm]"
).
wp_load
.
iDestruct
(
dup_is_list'
with
"[Hxs]"
)
as
">[Hxs1 Hxs2]"
;
first
by
iFrame
.
i
Mod
(
"Hclose"
with
"[Hs Hxs1 HRs Hm]"
).
{
iNext
.
iFrame
.
iExists
xs'
,
hd'
.
by
iFrame
.
}
i
Vs
Intro
.
wp_let
.
i
Mod
Intro
.
wp_let
.
wp_bind
(
iter
_
_
).
iApply
wp_wand_r
.
iSplitL
"HR Ho2 Hxs2"
.
{
iApply
(
loop_iter_doOp_spec
R
_
_
_
_
_
_
(
fun
v
=>
own
γ
r
(
Excl
())
★
R
★
v
=
#()))%
I
=>//.
iFrame
"#"
.
iFrame
.
iIntros
"? ?"
.
by
iFrame
.
}
iIntros
(
f'
)
"[Ho [HR %]]"
.
subst
.
wp_let
.
iApply
release_spec
.
iFrame
"#"
.
iFrame
.
iFrame
.
iNext
.
iIntros
.
done
.
Qed
.
Lemma
loop_spec
R
(
p
s
:
loc
)
(
lk
:
val
)
...
...
@@ -350,38 +351,38 @@ Section proof.
+
iDestruct
"Hp"
as
(?)
"(_ & _ & >Ho3')"
.
iApply
excl_falso
.
iFrame
.
+
iDestruct
"Hp"
as
(
f
x
)
"(>Hp & Hs')"
.
wp_load
.
i
Vs
(
"Hclose"
with
"[-Ho3 HΦ Hhd]"
).
wp_load
.
i
Mod
(
"Hclose"
with
"[-Ho3 HΦ Hhd]"
).
{
iNext
.
iFrame
.
iExists
xs
,
hd
.
iFrame
.
iExists
m
.
iFrame
.
iDestruct
(
big_sepM_delete
_
m
with
"[-]"
)
as
"?"
=>//.
iFrame
.
iExists
#
p
.
iSplitR
;
first
auto
.
iExists
(
γ
x
,
γ
1
,
γ
3
,
γ
4
,
γ
q
),
p
.
iSplitR
;
first
auto
.
iFrame
.
iRight
.
iLeft
.
iExists
f
,
x
.
iFrame
.
}
i
Vs
Intro
.
wp_match
.
i
Mod
Intro
.
wp_match
.
wp_bind
(
try_srv
_
_
).
iApply
try_srv_spec
=>//.
iFrame
"#"
.
wp_seq
.
iAssert
(
∃
hd
,
evs
γ
s
hd
#
p
)%
I
with
"[Hhd]"
as
"Hhd"
;
eauto
.
by
iApply
(
"IH"
with
"Ho3 Hhd"
).
+
iDestruct
"Hp"
as
(
f
x
)
"(Hp & Hx & Ho2 & Ho4)"
.
wp_load
.
i
Vs
(
"Hclose"
with
"[-Ho3 HΦ Hhd]"
).
i
Mod
(
"Hclose"
with
"[-Ho3 HΦ Hhd]"
).
{
iNext
.
iFrame
.
iExists
xs
,
hd
.
iFrame
.
iExists
m
.
iFrame
.
iDestruct
(
big_sepM_delete
_
m
with
"[-]"
)
as
"?"
=>//.
iFrame
.
iExists
#
p
.
iSplitR
;
auto
.
iExists
(
γ
x
,
γ
1
,
γ
3
,
γ
4
,
γ
q
),
p
.
iSplitR
;
first
auto
.
iFrame
.
iRight
.
iRight
.
iLeft
.
iExists
f
,
x
.
iFrame
.
}
i
Vs
Intro
.
wp_match
.
i
Mod
Intro
.
wp_match
.
wp_bind
(
try_srv
_
_
).
iApply
try_srv_spec
=>//.
iFrame
"#"
.
wp_seq
.
iAssert
(
∃
hd
,
evs
γ
s
hd
#
p
)%
I
with
"[Hhd]"
as
"Hhd"
;
eauto
.
by
iApply
(
"IH"
with
"Ho3 Hhd"
).
+
iDestruct
"Hp"
as
(
x
y
)
"[>Hp Hs']"
.
iDestruct
"Hs'"
as
(
Q
)
"(>Hx & HoQ & HQ & >Ho1 & >Ho4)"
.
wp_load
.
i
Vs
(
"Hclose"
with
"[-Ho4 HΦ Hx HoQ HQ]"
).
wp_load
.
i
Mod
(
"Hclose"
with
"[-Ho4 HΦ Hx HoQ HQ]"
).
{
iNext
.
iFrame
.
iExists
xs
,
hd
.
iFrame
.
iExists
m
.
iFrame
.
iDestruct
(
big_sepM_delete
_
m
with
"[-]"
)
as
"?"
=>//.
iFrame
.
iExists
#
p
.
iSplitR
;
auto
.
iExists
(
γ
x
,
γ
1
,
γ
3
,
γ
4
,
γ
q
),
p
.
iSplitR
;
first
auto
.
iFrame
.
iLeft
.
iExists
y
.
iFrame
.
}
i
Vs
Intro
.
wp_match
.
iApply
(
"HΦ"
with
"[-]"
).
iFrame
.
i
Mod
Intro
.
wp_match
.
iApply
(
"HΦ"
with
"[-]"
).
iFrame
.
iExists
Q
.
iFrame
.
-
iExFalso
.
iApply
(
map_agree_none'
_
_
_
m
)=>//.
iFrame
"Hom"
.
rewrite
/
ev
.
eauto
.
...
...
@@ -390,19 +391,19 @@ Section proof.
Lemma
mk_flat_spec
:
mk_syncer_spec
N
mk_flat
.
Proof
.
iIntros
(
R
Φ
HN
)
"(#Hh & HR & HΦ)"
.
i
Vs
(
own_alloc
(
Excl
()))
as
(
γ
r
)
"Ho2"
;
first
done
.
i
Vs
(
own_alloc
(
●
(
∅
:
tokmR
)
⋅
◯
∅
))
as
(
γ
m
)
"[Hm _]"
;
first
by
rewrite
-
auth_both_op
.
i
Mod
(
own_alloc
(
Excl
()))
as
(
γ
r
)
"Ho2"
;
first
done
.
i
Mod
(
own_alloc
(
●
(
∅
:
tokmR
)
⋅
◯
∅
))
as
(
γ
m
)
"[Hm _]"
;
first
by
rewrite
-
auth_both_op
.
iAssert
(
srv_tokm_inv
γ
m
)
with
"[Hm]"
as
"Hm"
;
first
eauto
.
{
iExists
∅
.
iFrame
.
by
rewrite
big_sepM_empty
.
}
wp_seq
.
wp_bind
(
newlock
_
).
iApply
(
newlock_spec
_
(
own
γ
r
(
Excl
())
★
R
))%
I
=>//.
iFrame
"Hh Ho2 HR"
.
iIntros
(
lk
γ
lk
)
"#Hlk"
.
iFrame
"Hh Ho2 HR"
.
iNext
.
iIntros
(
lk
γ
lk
)
"#Hlk"
.
wp_let
.
wp_bind
(
new_stack
_
).
iApply
(
new_stack_spec'
_
(
p_inv
_
γ
m
γ
r
))=>//.
iFrame
"Hh Hm"
.
iIntros
(
γ
s
)
"#Hss"
.
wp_let
.
i
Vs
Intro
.
iApply
"HΦ"
.
rewrite
/
synced
.
wp_let
.
i
Mod
Intro
.
iApply
"HΦ"
.
rewrite
/
synced
.
iAlways
.
iIntros
(
f
).
wp_let
.
i
Vs
Intro
.
iAlways
.
iIntros
(
f
).
wp_let
.
i
Mod
Intro
.
iAlways
.
iIntros
(
P
Q
x
)
"#Hf"
.
iIntros
"!# Hp"
.
wp_let
.
wp_bind
(
install
_
_
_
).
...
...
misc.v
View file @
08fc0696
...
...
@@ -2,9 +2,9 @@
From
iris
.
program_logic
Require
Export
weakestpre
.
From
iris
.
heap_lang
Require
Export
lang
proofmode
notation
.
From
iris
.
algebra
Require
Import
auth
frac
gmap
dec_agree
upred_big_op
.
From
iris
.
algebra
Require
Import
auth
frac
gmap
dec_agree
.
From
iris
.
prelude
Require
Import
countable
.
From
iris
.
program
_logic
Require
Import
auth
.
From
iris
.
base
_logic
Require
Import
big_op
auth
.
Import
uPred
.
Section
lemmas
.
...
...
peritem.v
View file @
08fc0696
From
iris
.
program_logic
Require
Export
weakestpre
.
From
iris
.
heap_lang
Require
Export
lang
.
From
iris
.
heap_lang
Require
Import
proofmode
notation
.
From
iris
.
algebra
Require
Import
frac
auth
upred
gmap
dec_agree
upred_big_op
csum
.
From
iris
.
algebra
Require
Import
frac
auth
gmap
dec_agree
csum
.
From
iris
.
base_logic
Require
Import
big_op
.
From
iris_atomic
Require
Export
treiber
misc
evmap
.
Section
defs
.
...
...
@@ -50,27 +51,27 @@ Section defs.
Proof
.
apply
_
.
Qed
.
Lemma
dup_is_list'
γ
:
∀
xs
hd
,
heap_ctx
★
is_list'
γ
hd
xs
⊢
|=
r
=>
is_list'
γ
hd
xs
★
is_list'
γ
hd
xs
.
heap_ctx
★
is_list'
γ
hd
xs
⊢
|==>
is_list'
γ
hd
xs
★
is_list'
γ
hd
xs
.
Proof
.
induction
xs
as
[|
y
xs'
IHxs'
].
-
iIntros
(
hd
)
"(#? & Hs)"
.
simpl
.
iDestruct
"Hs"
as
(
q
)
"[Hhd Hhd']"
.
iSplitL
"Hhd"
;
eauto
.
-
iIntros
(
hd
)
"(#? & Hs)"
.
simpl
.
iDestruct
"Hs"
as
(
hd'
q
)
"([Hhd Hhd'] & #Hev & Hs')"
.
iDestruct
(
IHxs'
with
"[Hs']"
)
as
"
==
>[Hs1 Hs2]"
;
first
by
iFrame
.
i
Vs
Intro
.
iSplitL
"Hhd Hs1"
;
iExists
hd'
,
(
q
/
2
)%
Qp
;
by
iFrame
.
iDestruct
(
IHxs'
with
"[Hs']"
)
as
">[Hs1 Hs2]"
;
first
by
iFrame
.
i
Mod
Intro
.
iSplitL
"Hhd Hs1"
;
iExists
hd'
,
(
q
/
2
)%
Qp
;
by
iFrame
.
Qed
.
Lemma
extract_is_list
γ
:
∀
xs
hd
,
heap_ctx
★
is_list'
γ
hd
xs
⊢
|=
r
=>
is_list'
γ
hd
xs
★
is_list
hd
xs
.
heap_ctx
★
is_list'
γ
hd
xs
⊢
|==>
is_list'
γ
hd
xs
★
is_list
hd
xs
.
Proof
.
induction
xs
as
[|
y
xs'
IHxs'
].
-
iIntros
(
hd
)
"(#? & Hs)"
.
simpl
.
iDestruct
"Hs"
as
(
q
)
"[Hhd Hhd']"
.
iSplitL
"Hhd"
;
eauto
.
-
iIntros
(
hd
)
"(#? & Hs)"
.
simpl
.
iDestruct
"Hs"
as
(
hd'
q
)
"([Hhd Hhd'] & Hev & Hs')"
.
iDestruct
(
IHxs'
with
"[Hs']"
)
as
"
==
>[Hs1 Hs2]"
;
first
by
iFrame
.
i
Vs
Intro
.
iSplitL
"Hhd Hs1 Hev"
;
iExists
hd'
,
(
q
/
2
)%
Qp
;
by
iFrame
.
iDestruct
(
IHxs'
with
"[Hs']"
)
as
">[Hs1 Hs2]"
;
first
by
iFrame
.
i
Mod
Intro
.
iSplitL
"Hhd Hs1 Hev"
;
iExists
hd'
,
(
q
/
2
)%
Qp
;
by
iFrame
.
Qed
.
Definition
f_spec
γ
(
xs
:
list
val
)
(
s
:
loc
)
(
f
:
val
)
(
Rf
RI
:
iProp
Σ
)
:
=
...
...
@@ -92,7 +93,7 @@ Lemma new_stack_spec' Φ RI:
⊢
WP
new_stack
#()
{{
Φ
}}.
Proof
.
iIntros
(
HN
)
"(#Hh & HR & HΦ)"
.
i
Vs
(
own_alloc
(
●
(
∅
:
evmapR
loc
val
unitR
)
⋅
◯
∅
))
as
(
γ
)
"[Hm Hm']"
.
i
Mod
(
own_alloc
(
●
(
∅
:
evmapR
loc
val
unitR
)
⋅
◯
∅
))
as
(
γ
)
"[Hm Hm']"
.
{
apply
auth_valid_discrete_2
.
done
.
}
wp_seq
.
wp_bind
(
ref
NONE
)%
E
.
wp_alloc
l
as
"Hl"
.
wp_alloc
s
as
"Hs"
.
...
...
@@ -100,7 +101,7 @@ Lemma new_stack_spec' Φ RI:
{
iFrame
.
iExists
[],
l
.
iFrame
.
simpl
.
iSplitL
"Hl"
.
-
eauto
.
-
iExists
∅
.
iSplitL
.
iFrame
.
by
iApply
(
big_sepM_empty
(
fun
hd
v
=>
perR
R
hd
v
)).
}
i
Vs
(
inv_alloc
N
_
((
∃
xs
:
list
val
,
is_stack'
R
γ
xs
s
)
★
RI
)%
I
with
"[-HΦ Hm']"
)
as
"#?"
;
first
eauto
.
i
Mod
(
inv_alloc
N
_
((
∃
xs
:
list
val
,
is_stack'
R
γ
xs
s
)
★
RI
)%
I
with
"[-HΦ Hm']"
)
as
"#?"
;
first
eauto
.
by
iApply
"HΦ"
.
Qed
.
...
...
@@ -114,10 +115,10 @@ Lemma new_stack_spec' Φ RI:
induction
xs
as
[|
x
xs'
IHxs'
].
-
simpl
.
iIntros
(
hd
f
f'
HN
?
?)
"(#Hh & #? & Hxs1 & HRf & HΦ)"
.
iDestruct
"Hxs1"
as
(
q
)
"Hhd"
.
wp_rec
.
wp_value
.
i
Vs
Intro
.
wp_let
.
wp_load
.
wp_match
.
by
iApply
"HΦ"
.
wp_rec
.
wp_value
.
i
Mod
Intro
.
wp_let
.
wp_load
.
wp_match
.
by
iApply
"HΦ"
.
-
simpl
.
iIntros
(
hd
f
f'
HN
Hf
?)
"(#Hh & #? & Hxs1 & HRf & HΦ)"
.
iDestruct
"Hxs1"
as
(
hd2
q
)
"(Hhd & Hev & Hhd2)"
.
wp_rec
.
wp_value
.
i
Vs
Intro
.
wp_let
.
wp_load
.
wp_match
.
wp_proj
.
wp_rec
.
wp_value
.
i
Mod
Intro
.
wp_let
.
wp_load
.
wp_match
.
wp_proj
.
wp_bind
(
f'
_
).
iApply
Hf
=>//.
iFrame
"#"
.
iSplitL
"Hev"
;
first
eauto
.
iFrame
.
iIntros
"HRf"
.
wp_seq
.
wp_proj
.
iApply
(
IHxs'
with
"[-]"
)=>//.
...
...
@@ -137,20 +138,20 @@ Lemma new_stack_spec' Φ RI:
(* open the invariant *)
iInv
N
as
"[IH1 ?]"
"Hclose"
.
iDestruct
"IH1"
as
(
xs
hd
)
"[>Hs [>Hxs HR]]"
.
iDestruct
(
extract_is_list
with
"[Hxs]"
)
as
"
==
>[Hxs Hxs']"
;
first
by
iFrame
.
iDestruct
(
extract_is_list
with
"[Hxs]"
)
as
">[Hxs Hxs']"
;
first
by
iFrame
.
iDestruct
(
dup_is_list
with
"[Hxs']"
)
as
"[Hxs'1 Hxs'2]"
;
first
by
iFrame
.
(* mask magic *)
i
Vs
(
pvs
_intro_mask'
(
⊤
∖
nclose
N
)
heapN
)
as
"Hvs"
;
first
set_solver
.
i
Vs
Intro
.
iExists
(
xs
,
hd
).
i
Mod
(
fupd
_intro_mask'
(
⊤
∖
nclose
N
)
heapN
)
as
"Hvs"
;
first
set_solver
.
i
Mod
Intro
.
iExists
(
xs
,
hd
).
iFrame
"Hs Hxs'1"
.
iSplit
.
+
(* provide a way to rollback *)
iIntros
"[Hs Hl']"
.
i
Vs
"Hvs"
.
i
Vs
(
"Hclose"
with
"[-Rx]"
)
;
last
done
.
i
Mod
"Hvs"
.
i
Mod
(
"Hclose"
with
"[-Rx]"
)
;
last
done
.
{
iNext
.
iFrame
.
iExists
xs
.
iExists
hd
.
by
iFrame
.
}
+
(* provide a way to commit *)
iIntros
(
v
)
"Hs"
.
iDestruct
"Hs"
as
(
hd'
)
"[% [Hs [[Hhd'1 Hhd'2] Hxs']]]"
.
subst
.
i
Vs
"Hvs"
.
i
Mod
"Hvs"
.
iDestruct
"HR"
as
(
m
)
"[>Hom HRm]"
.
destruct
(
m
!!
hd'
)
eqn
:
Heqn
.
*
iDestruct
(
big_sepM_delete_later
(
perR
R
)
m
with
"HRm"
)
as
"[Hx ?]"
=>//.
...
...
@@ -161,9 +162,9 @@ Lemma new_stack_spec' Φ RI:
iApply
(
bogus_heap
hd'
1
%
Qp
q
)
;
first
apply
Qp_not_plus_q_ge_1
.
iFrame
"#"
.
iFrame
.
*
iAssert
(
evs
γ
hd'
x
★
▷
(
allR
R
γ
))%
I
with
"
==
>[Rx Hom HRm Hhd'1]"
as
"[#Hox ?]"
.
with
">[Rx Hom HRm Hhd'1]"
as
"[#Hox ?]"
.
{
iDestruct
(
evmap_alloc
_
_
_
m
with
"[Hom]"
)
as
"
==
>[Hom Hox]"
=>//.
iDestruct
(
evmap_alloc
_
_
_
m
with
"[Hom]"
)
as
">[Hom Hox]"
=>//.
iDestruct
(
big_sepM_insert_later
(
perR
R
)
m
)
as
"H"
=>//.
iSplitL
"Hox"
.
{
rewrite
/
evs
/
ev
.
eauto
.
}
...
...
@@ -171,12 +172,12 @@ Lemma new_stack_spec' Φ RI:
iFrame
.
iApply
"H"
.
iFrame
.
iExists
x
.
iFrame
.
rewrite
/
allocated
.
iSplitR
"Hhd'1"
;
auto
.
}
i
Vs
(
"Hclose"
with
"[-]"
).
i
Mod
(
"Hclose"
with
"[-]"
).
{
iNext
.
iFrame
.
iExists
(
x
::
xs
).
iExists
hd'
.
iFrame
.
iExists
hd
,
(
1
/
2
)%
Qp
.
by
iFrame
.
}
i
Vs
Intro
.
iSplitL
;
last
auto
.
by
iExists
hd'
.
i
Mod
Intro
.
iSplitL
;
last
auto
.
by
iExists
hd'
.
-
iApply
wp_wand_r
.
iSplitL
"HRx Hpush"
.
+
by
iApply
"Hpush"
.
+
iIntros
(?)
"H"
.
iDestruct
"H"
as
(
_
)
"[? %]"
.
subst
.
...
...
simple_sync.v
View file @
08fc0696
...
...
@@ -26,18 +26,17 @@ Section syncer.
iIntros
(
R
Φ
HN
)
"(#Hh & HR & HΦ)"
.
wp_seq
.
wp_bind
(
newlock
_
).
iApply
newlock_spec
;
first
done
.
iSplitR
"HR HΦ"
;
first
done
.
iFrame
"HR"
.
iSplitL
"HR"
;
first
by
iFrame
.
iNext
.
iIntros
(
lk
γ
)
"#Hl"
.
wp_let
.
iApply
"HΦ"
.
iIntros
"!#"
.
iIntros
(
f
).
wp_let
.
i
Vs
Intro
.
iAlways
.
iIntros
(
f
).
wp_let
.
i
Mod
Intro
.
iAlways
.
iIntros
(
P
Q
x
)
"#Hf !# HP"
.
wp_let
.
wp_bind
(
acquire
_
).
iApply
acquire_spec
.
iSplit
;
first
done
.
iIntros
"Hlocked R"
.
wp_seq
.
wp_bind
(
f
_
).
iApply
acquire_spec
.
iSplit
;
first
done
.
iNext
.