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
Iris
Commits
24b6bc9c
Commit
24b6bc9c
authored
Oct 24, 2016
by
Ralf Jung
Committed by
Robbert Krebbers
Oct 27, 2016
Browse files
port a lot of our specs to texan triples
parent
3e2fda9e
Changes
5
Hide whitespace changes
Inline
Side-by-side
heap_lang/lib/counter.v
View file @
24b6bc9c
...
...
@@ -33,21 +33,21 @@ Section mono_proof.
Global
Instance
mcounter_persistent
l
n
:
PersistentP
(
mcounter
l
n
).
Proof
.
apply
_
.
Qed
.
Lemma
newcounter_mono_spec
(
R
:
iProp
Σ
)
Φ
:
Lemma
newcounter_mono_spec
(
R
:
iProp
Σ
)
:
heapN
⊥
N
→
heap_ctx
★
(
∀
l
,
mcounter
l
0
-
★
Φ
#
l
)
⊢
WP
newcounter
#()
{{
Φ
}}.
{{{
heap_ctx
}}}
newcounter
#()
{{{
l
;
#
l
,
mcounter
l
0
}
}}.
Proof
.
iIntros
(?)
"[#Hh HΦ]"
.
rewrite
/
newcounter
/=.
wp_seq
.
wp_alloc
l
as
"Hl"
.
iIntros
(?
Φ
)
"[#Hh HΦ]"
.
rewrite
/
newcounter
/=.
wp_seq
.
wp_alloc
l
as
"Hl"
.
iMod
(
own_alloc
(
●
(
O
:
mnat
)
⋅
◯
(
O
:
mnat
)))
as
(
γ
)
"[Hγ Hγ']"
;
first
done
.
iMod
(
inv_alloc
N
_
(
mcounter_inv
γ
l
)
with
"[Hl Hγ]"
).
{
iNext
.
iExists
0
%
nat
.
by
iFrame
.
}
iModIntro
.
iApply
"HΦ"
.
rewrite
/
mcounter
;
eauto
10
.
Qed
.
Lemma
inc_mono_spec
l
n
(
Φ
:
val
→
iProp
Σ
)
:
mcounter
l
n
★
(
mcounter
l
(
S
n
)
-
★
Φ
#())
⊢
WP
inc
#
l
{{
Φ
}}.
Lemma
inc_mono_spec
l
n
:
{{{
mcounter
l
n
}}}
inc
#
l
{{{
;
#(),
mcounter
l
(
S
n
)
}
}}.
Proof
.
iIntros
"[Hl HΦ]"
.
iL
ö
b
as
"IH"
.
wp_rec
.
iIntros
(
Φ
)
"[Hl HΦ]"
.
iL
ö
b
as
"IH"
.
wp_rec
.
iDestruct
"Hl"
as
(
γ
)
"(% & #? & #Hinv & Hγf)"
.
wp_bind
(!
_
)%
E
.
iInv
N
as
(
c
)
">[Hγ Hl]"
"Hclose"
.
wp_load
.
iMod
(
"Hclose"
with
"[Hl Hγ]"
)
as
"_"
;
[
iNext
;
iExists
c
;
by
iFrame
|].
...
...
@@ -69,18 +69,17 @@ Section mono_proof.
rewrite
{
3
}/
mcounter
;
eauto
10
.
Qed
.
Lemma
read_mono_spec
l
j
(
Φ
:
val
→
iProp
Σ
)
:
mcounter
l
j
★
(
∀
i
,
■
(
j
≤
i
)%
nat
→
mcounter
l
i
-
★
Φ
#
i
)
⊢
WP
read
#
l
{{
Φ
}}.
Lemma
read_mono_spec
l
j
:
{{{
mcounter
l
j
}}}
read
#
l
{{{
i
;
#
i
,
■
(
j
≤
i
)%
nat
∧
mcounter
l
i
}}}.
Proof
.
iIntros
"[Hc HΦ]"
.
iDestruct
"Hc"
as
(
γ
)
"(% & #? & #Hinv & Hγf)"
.
iIntros
(
ϕ
)
"[Hc HΦ]"
.
iDestruct
"Hc"
as
(
γ
)
"(% & #? & #Hinv & Hγf)"
.
rewrite
/
read
/=.
wp_let
.
iInv
N
as
(
c
)
">[Hγ Hl]"
"Hclose"
.
wp_load
.
iDestruct
(
own_valid_2
with
"[$Hγ $Hγf]"
)
as
%[?%
mnat_included
_
]%
auth_valid_discrete_2
.
iMod
(
own_update_2
with
"[$Hγ $Hγf]"
)
as
"[Hγ Hγf]"
.
{
apply
auth_update
,
(
mnat_local_update
_
_
c
)
;
auto
.
}
iMod
(
"Hclose"
with
"[Hl Hγ]"
)
as
"_"
;
[
iNext
;
iExists
c
;
by
iFrame
|].
iApply
(
"HΦ"
with
"[
%
]"
)
;
rewrite
/
mcounter
;
eauto
10
.
iApply
(
"HΦ"
with
"[
-
]"
)
.
rewrite
/
mcounter
;
eauto
10
.
Qed
.
End
mono_proof
.
...
...
@@ -110,12 +109,12 @@ Section contrib_spec.
ccounter
γ
(
q1
+
q2
)
(
n1
+
n2
)
⊣
⊢
ccounter
γ
q1
n1
★
ccounter
γ
q2
n2
.
Proof
.
by
rewrite
/
ccounter
-
own_op
-
auth_frag_op
.
Qed
.
Lemma
newcounter_contrib_spec
(
R
:
iProp
Σ
)
Φ
:
Lemma
newcounter_contrib_spec
(
R
:
iProp
Σ
)
:
heapN
⊥
N
→
heap_ctx
★
(
∀
γ
l
,
ccounter_ctx
γ
l
★
ccounter
γ
1
0
-
★
Φ
#
l
)
⊢
WP
newcounter
#()
{{
Φ
}}.
{{{
heap_ctx
}}}
newcounter
#(
)
{{{
γ
l
;
#
l
,
ccounter_ctx
γ
l
★
ccounter
γ
1
0
}
}}.
Proof
.
iIntros
(?)
"[#Hh HΦ]"
.
rewrite
/
newcounter
/=.
wp_seq
.
wp_alloc
l
as
"Hl"
.
iIntros
(?
Φ
)
"[#Hh HΦ]"
.
rewrite
/
newcounter
/=.
wp_seq
.
wp_alloc
l
as
"Hl"
.
iMod
(
own_alloc
(
●
(
Some
(
1
%
Qp
,
O
%
nat
))
⋅
◯
(
Some
(
1
%
Qp
,
0
%
nat
))))
as
(
γ
)
"[Hγ Hγ']"
;
first
done
.
iMod
(
inv_alloc
N
_
(
ccounter_inv
γ
l
)
with
"[Hl Hγ]"
).
...
...
@@ -123,11 +122,11 @@ Section contrib_spec.
iModIntro
.
iApply
"HΦ"
.
rewrite
/
ccounter_ctx
/
ccounter
;
eauto
10
.
Qed
.
Lemma
inc_contrib_spec
γ
l
q
n
(
Φ
:
val
→
iProp
Σ
)
:
ccounter_ctx
γ
l
★
ccounter
γ
q
n
★
(
ccounter
γ
q
(
S
n
)
-
★
Φ
#())
⊢
WP
inc
#
l
{{
Φ
}}.
Lemma
inc_contrib_spec
γ
l
q
n
:
{{{
ccounter_ctx
γ
l
★
ccounter
γ
q
n
}}}
inc
#
l
{{{
;
#(),
ccounter
γ
q
(
S
n
)
}
}}.
Proof
.
iIntros
"
(#(%&?&?) & Hγf & HΦ)"
.
iL
ö
b
as
"IH"
.
wp_rec
.
iIntros
(
Φ
)
"(
(#(%&?&?) & Hγf
)
& HΦ)"
.
iL
ö
b
as
"IH"
.
wp_rec
.
wp_bind
(!
_
)%
E
.
iInv
N
as
(
c
)
">[Hγ Hl]"
"Hclose"
.
wp_load
.
iMod
(
"Hclose"
with
"[Hl Hγ]"
)
as
"_"
;
[
iNext
;
iExists
c
;
by
iFrame
|].
iModIntro
.
wp_let
.
wp_op
.
...
...
@@ -144,24 +143,23 @@ Section contrib_spec.
iModIntro
.
wp_if
.
by
iApply
(
"IH"
with
"[Hγf] HΦ"
).
Qed
.
Lemma
read_contrib_spec
γ
l
q
n
(
Φ
:
val
→
iProp
Σ
)
:
ccounter_ctx
γ
l
★
ccounter
γ
q
n
★
(
∀
c
,
■
(
n
≤
c
)%
nat
→
ccounter
γ
q
n
-
★
Φ
#
c
)
⊢
WP
read
#
l
{{
Φ
}}.
Lemma
read_contrib_spec
γ
l
q
n
:
{{{
ccounter_ctx
γ
l
★
ccounter
γ
q
n
}}}
read
#
l
{{{
c
;
#
c
,
■
(
n
≤
c
)%
nat
∧
ccounter
γ
q
n
}}}.
Proof
.
iIntros
"
(#(%&?&?) & Hγf & HΦ)"
.
iIntros
(
Φ
)
"(
(#(%&?&?) & Hγf
)
& HΦ)"
.
rewrite
/
read
/=.
wp_let
.
iInv
N
as
(
c
)
">[Hγ Hl]"
"Hclose"
.
wp_load
.
iDestruct
(
own_valid_2
with
"[$Hγ $Hγf]"
)
as
%[[?
?%
nat_included
]%
Some_pair_included_total_2
_
]%
auth_valid_discrete_2
.
iMod
(
"Hclose"
with
"[Hl Hγ]"
)
as
"_"
;
[
iNext
;
iExists
c
;
by
iFrame
|].
iApply
(
"HΦ"
with
"[
%
]"
)
;
rewrite
/
ccounter
;
eauto
10
.
iApply
(
"HΦ"
with
"[
-
]"
)
;
rewrite
/
ccounter
;
eauto
10
.
Qed
.
Lemma
read_contrib_spec_1
γ
l
n
(
Φ
:
val
→
iProp
Σ
)
:
ccounter_ctx
γ
l
★
ccounter
γ
1
n
★
(
ccounter
γ
1
n
-
★
Φ
#
n
)
⊢
WP
read
#
l
{{
Φ
}}.
Lemma
read_contrib_spec_1
γ
l
n
:
{{{
ccounter_ctx
γ
l
★
ccounter
γ
1
n
}}}
read
#
l
{{{
n
;
#
n
,
ccounter
γ
1
n
}
}}.
Proof
.
iIntros
"
(#(%&?&?) & Hγf & HΦ)"
.
iIntros
(
Φ
)
"(
(#(%&?&?) & Hγf
)
& HΦ)"
.
rewrite
/
read
/=.
wp_let
.
iInv
N
as
(
c
)
">[Hγ Hl]"
"Hclose"
.
wp_load
.
iDestruct
(
own_valid_2
with
"[$Hγ $Hγf]"
)
as
%[
Hn
_
]%
auth_valid_discrete_2
.
apply
(
Some_included_exclusive
_
)
in
Hn
as
[=
->]%
leibniz_equiv
;
last
done
.
...
...
heap_lang/lib/lock.v
View file @
24b6bc9c
...
...
@@ -16,13 +16,13 @@ Structure lock Σ `{!heapG Σ} := Lock {
locked_timeless
γ
:
TimelessP
(
locked
γ
)
;
locked_exclusive
γ
:
locked
γ
★
locked
γ
⊢
False
;
(* -- operation specs -- *)
newlock_spec
N
(
R
:
iProp
Σ
)
Φ
:
newlock_spec
N
(
R
:
iProp
Σ
)
:
heapN
⊥
N
→
heap_ctx
★
R
★
(
∀
l
γ
,
is_lock
N
γ
l
R
-
★
Φ
l
)
⊢
WP
newlock
#()
{{
Φ
}}
;
acquire_spec
N
γ
lk
R
(
Φ
:
val
→
iProp
Σ
)
:
is_lock
N
γ
lk
R
★
(
locked
γ
-
★
R
-
★
Φ
#())
⊢
WP
acquire
lk
{{
Φ
}}
;
release_spec
N
γ
lk
R
(
Φ
:
val
→
iProp
Σ
)
:
is_lock
N
γ
lk
R
★
locked
γ
★
R
★
Φ
#()
⊢
WP
release
lk
{{
Φ
}}
{{{
heap_ctx
★
R
}}}
newlock
#()
{{{
l
k
γ
;
lk
,
is_lock
N
γ
l
k
R
}
}}
;
acquire_spec
N
γ
lk
R
:
{{{
is_lock
N
γ
lk
R
}}}
acquire
lk
{{{
;
#(),
locked
γ
★
R
}
}}
;
release_spec
N
γ
lk
R
:
{{{
is_lock
N
γ
lk
R
★
locked
γ
★
R
}}}
release
lk
{{
{
;
#(),
True
}
}}
}.
Arguments
newlock
{
_
_
}
_
.
...
...
heap_lang/lib/spawn.v
View file @
24b6bc9c
...
...
@@ -46,13 +46,12 @@ Global Instance join_handle_ne n l :
Proof
.
solve_proper
.
Qed
.
(** The main proofs. *)
Lemma
spawn_spec
(
Ψ
:
val
→
iProp
Σ
)
e
(
f
:
val
)
(
Φ
:
val
→
iProp
Σ
)
:
Lemma
spawn_spec
(
Ψ
:
val
→
iProp
Σ
)
e
(
f
:
val
)
:
to_val
e
=
Some
f
→
heapN
⊥
N
→
heap_ctx
★
WP
f
#()
{{
Ψ
}}
★
(
∀
l
,
join_handle
l
Ψ
-
★
Φ
#
l
)
⊢
WP
spawn
e
{{
Φ
}}.
{{{
heap_ctx
★
WP
f
#()
{{
Ψ
}}
}}}
spawn
e
{{{
l
;
#
l
,
join_handle
l
Ψ
}}}.
Proof
.
iIntros
(<-%
of_to_val
?)
"(#Hh & Hf & HΦ)"
.
rewrite
/
spawn
/=.
iIntros
(<-%
of_to_val
?
Φ
)
"(
(
#Hh & Hf
)
& HΦ)"
.
rewrite
/
spawn
/=.
wp_let
.
wp_alloc
l
as
"Hl"
.
wp_let
.
iMod
(
own_alloc
(
Excl
()))
as
(
γ
)
"Hγ"
;
first
done
.
iMod
(
inv_alloc
N
_
(
spawn_inv
γ
l
Ψ
)
with
"[Hl]"
)
as
"#?"
.
...
...
@@ -64,10 +63,10 @@ Proof.
wp_store
.
iApply
"Hclose"
.
iNext
.
iExists
(
SOMEV
v
).
iFrame
.
eauto
.
Qed
.
Lemma
join_spec
(
Ψ
:
val
→
iProp
Σ
)
l
(
Φ
:
val
→
iProp
Σ
)
:
join_handle
l
Ψ
★
(
∀
v
,
Ψ
v
-
★
Φ
v
)
⊢
WP
join
#
l
{{
Φ
}}.
Lemma
join_spec
(
Ψ
:
val
→
iProp
Σ
)
l
:
{{{
join_handle
l
Ψ
}}}
join
#
l
{{{
v
;
v
,
Ψ
v
}
}}.
Proof
.
rewrite
/
join_handle
;
iIntros
"[[% H] Hv]"
.
iDestruct
"H"
as
(
γ
)
"(#?&Hγ&#?)"
.
rewrite
/
join_handle
;
iIntros
(
Φ
)
"[[% H] Hv]"
.
iDestruct
"H"
as
(
γ
)
"(#?&Hγ&#?)"
.
iL
ö
b
as
"IH"
.
wp_rec
.
wp_bind
(!
_
)%
E
.
iInv
N
as
(
v
)
"[Hl Hinv]"
"Hclose"
.
wp_load
.
iDestruct
"Hinv"
as
"[%|Hinv]"
;
subst
.
-
iMod
(
"Hclose"
with
"[Hl]"
)
;
[
iNext
;
iExists
_;
iFrame
;
eauto
|].
...
...
heap_lang/lib/spin_lock.v
View file @
24b6bc9c
...
...
@@ -45,11 +45,11 @@ Section proof.
Global
Instance
locked_timeless
γ
:
TimelessP
(
locked
γ
).
Proof
.
apply
_
.
Qed
.
Lemma
newlock_spec
(
R
:
iProp
Σ
)
Φ
:
Lemma
newlock_spec
(
R
:
iProp
Σ
)
:
heapN
⊥
N
→
heap_ctx
★
R
★
(
∀
lk
γ
,
is_lock
γ
lk
R
-
★
Φ
lk
)
⊢
WP
newlock
#()
{{
Φ
}}.
{{{
heap_ctx
★
R
}}}
newlock
#()
{{{
lk
γ
;
lk
,
is_lock
γ
lk
R
}
}}.
Proof
.
iIntros
(?)
"
(
#Hh
& HR &
HΦ
)
"
.
rewrite
/
newlock
/=.
iIntros
(?
Φ
)
"
[[
#Hh
HR]
HΦ
]
"
.
rewrite
/
newlock
/=.
wp_seq
.
wp_alloc
l
as
"Hl"
.
iMod
(
own_alloc
(
Excl
()))
as
(
γ
)
"Hγ"
;
first
done
.
iMod
(
inv_alloc
N
_
(
lock_inv
γ
l
R
)
with
"[-HΦ]"
)
as
"#?"
.
...
...
@@ -70,22 +70,22 @@ Section proof.
iModIntro
.
iDestruct
"HΦ"
as
"[HΦ _]"
.
rewrite
/
locked
.
by
iApply
(
"HΦ"
with
"Hγ HR"
).
Qed
.
Lemma
acquire_spec
γ
lk
R
(
Φ
:
val
→
iProp
Σ
)
:
is_lock
γ
lk
R
★
(
locked
γ
-
★
R
-
★
Φ
#())
⊢
WP
acquire
lk
{{
Φ
}}.
Lemma
acquire_spec
γ
lk
R
:
{{{
is_lock
γ
lk
R
}}}
acquire
lk
{{{
;
#(),
locked
γ
★
R
}
}}.
Proof
.
iIntros
"[#Hl HΦ]"
.
iL
ö
b
as
"IH"
.
wp_rec
.
wp_bind
(
try_acquire
_
).
iIntros
(
Φ
)
"[#Hl HΦ]"
.
iL
ö
b
as
"IH"
.
wp_rec
.
wp_bind
(
try_acquire
_
).
iApply
try_acquire_spec
.
iFrame
"#"
.
iSplit
.
-
iIntros
"Hlked HR"
.
wp_if
.
iModIntro
.
iApply
(
"HΦ"
with
"Hlked HR"
)
.
-
iIntros
"Hlked HR"
.
wp_if
.
iModIntro
.
iApply
"HΦ"
;
iFrame
.
-
wp_if
.
iApply
(
"IH"
with
"HΦ"
).
Qed
.
Lemma
release_spec
γ
lk
R
(
Φ
:
val
→
iProp
Σ
)
:
is_lock
γ
lk
R
★
locked
γ
★
R
★
Φ
#()
⊢
WP
release
lk
{{
Φ
}}.
Lemma
release_spec
γ
lk
R
:
{{{
is_lock
γ
lk
R
★
locked
γ
★
R
}}}
release
lk
{{
{
;
#(),
True
}
}}.
Proof
.
iIntros
"
(Hlock & Hlocked & HR & HΦ)"
.
iIntros
(
Φ
)
"(
(Hlock & Hlocked & HR
)
& HΦ)"
.
iDestruct
"Hlock"
as
(
l
)
"(% & #? & % & #?)"
.
subst
.
rewrite
/
release
/=.
wp_let
.
iInv
N
as
(
b
)
"[Hl _]"
"Hclose"
.
wp_store
.
i
Frame
"HΦ"
.
iApply
"Hclose"
.
iNext
.
iExists
false
.
by
iFrame
.
wp_store
.
i
Apply
"HΦ"
.
iApply
"Hclose"
.
iNext
.
iExists
false
.
by
iFrame
.
Qed
.
End
proof
.
...
...
heap_lang/lib/ticket_lock.v
View file @
24b6bc9c
...
...
@@ -74,11 +74,11 @@ Section proof.
iCombine
"H1"
"H2"
as
"H"
.
iDestruct
(
own_valid
with
"H"
)
as
%[[]
_
].
Qed
.
Lemma
newlock_spec
(
R
:
iProp
Σ
)
Φ
:
Lemma
newlock_spec
(
R
:
iProp
Σ
)
:
heapN
⊥
N
→
heap_ctx
★
R
★
(
∀
lk
γ
,
is_lock
γ
lk
R
-
★
Φ
lk
)
⊢
WP
newlock
#()
{{
Φ
}}.
{{{
heap_ctx
★
R
}}}
newlock
#()
{{{
lk
γ
;
lk
,
is_lock
γ
lk
R
}
}}.
Proof
.
iIntros
(
HN
)
"(#Hh & HR & HΦ)"
.
rewrite
/
newlock
/=.
iIntros
(
HN
Φ
)
"(
(
#Hh & HR
)
& HΦ)"
.
rewrite
/
newlock
/=.
wp_seq
.
wp_alloc
lo
as
"Hlo"
.
wp_alloc
ln
as
"Hln"
.
iMod
(
own_alloc
(
●
(
Excl'
0
%
nat
,
∅
)
⋅
◯
(
Excl'
0
%
nat
,
∅
)))
as
(
γ
)
"[Hγ Hγ']"
.
{
by
rewrite
-
auth_both_op
.
}
...
...
@@ -89,7 +89,7 @@ Section proof.
Qed
.
Lemma
wait_loop_spec
γ
lk
x
R
(
Φ
:
val
→
iProp
Σ
)
:
issued
γ
lk
x
R
★
(
locked
γ
-
★
R
-
★
Φ
#())
⊢
WP
wait_loop
#
x
lk
{{
Φ
}}.
issued
γ
lk
x
R
★
(
locked
γ
★
R
-
★
Φ
#())
⊢
WP
wait_loop
#
x
lk
{{
Φ
}}.
Proof
.
iIntros
"[Hl HΦ]"
.
iDestruct
"Hl"
as
(
lo
ln
)
"(% & #? & % & #? & Ht)"
.
iL
ö
b
as
"IH"
.
wp_rec
.
subst
.
wp_let
.
wp_proj
.
wp_bind
(!
_
)%
E
.
...
...
@@ -100,7 +100,7 @@ Section proof.
{
iNext
.
iExists
o
,
n
.
iFrame
.
eauto
.
}
iModIntro
.
wp_let
.
wp_op
=>[
_
|[]]
//.
wp_if
.
iModIntro
.
iApply
(
"HΦ"
with
"[-
HR] HR
"
).
rewrite
/
locked
;
eauto
.
iApply
(
"HΦ"
with
"[-
]
"
).
rewrite
/
locked
.
iFrame
.
eauto
.
+
iDestruct
(
own_valid_2
with
"[$Ht $Haown]"
)
as
%
[
_
?%
gset_disj_valid_op
].
set_solver
.
-
iMod
(
"Hclose"
with
"[Hlo Hln Ha]"
).
...
...
@@ -109,10 +109,10 @@ Section proof.
wp_if
.
iApply
(
"IH"
with
"Ht"
).
by
iExact
"HΦ"
.
Qed
.
Lemma
acquire_spec
γ
lk
R
(
Φ
:
val
→
iProp
Σ
)
:
is_lock
γ
lk
R
★
(
locked
γ
-
★
R
-
★
Φ
#())
⊢
WP
acquire
lk
{{
Φ
}}.
Lemma
acquire_spec
γ
lk
R
:
{{{
is_lock
γ
lk
R
}}}
acquire
lk
{{{
;
#(),
locked
γ
★
R
}
}}.
Proof
.
iIntros
"[Hl HΦ]"
.
iDestruct
"Hl"
as
(
lo
ln
)
"(% & #? & % & #?)"
.
iIntros
(
ϕ
)
"[Hl HΦ]"
.
iDestruct
"Hl"
as
(
lo
ln
)
"(% & #? & % & #?)"
.
iL
ö
b
as
"IH"
.
wp_rec
.
wp_bind
(!
_
)%
E
.
subst
.
wp_proj
.
iInv
N
as
(
o
n
)
"[Hlo [Hln Ha]]"
"Hclose"
.
wp_load
.
iMod
(
"Hclose"
with
"[Hlo Hln Ha]"
)
as
"_"
.
...
...
@@ -139,10 +139,10 @@ Section proof.
iModIntro
.
wp_if
.
by
iApply
"IH"
.
Qed
.
Lemma
release_spec
γ
lk
R
(
Φ
:
val
→
iProp
Σ
)
:
is_lock
γ
lk
R
★
locked
γ
★
R
★
Φ
#()
⊢
WP
release
lk
{{
Φ
}}.
Lemma
release_spec
γ
lk
R
:
{{{
is_lock
γ
lk
R
★
locked
γ
★
R
}}}
release
lk
{{
{
;
#(),
True
}
}}.
Proof
.
iIntros
"
(Hl & Hγ & HR & HΦ)"
.
iIntros
(
Φ
)
"(
(Hl & Hγ & HR
)
& HΦ)"
.
iDestruct
"Hl"
as
(
lo
ln
)
"(% & #? & % & #?)"
;
subst
.
iDestruct
"Hγ"
as
(
o
)
"Hγo"
.
rewrite
/
release
.
wp_let
.
wp_proj
.
wp_proj
.
wp_bind
(!
_
)%
E
.
...
...
@@ -162,7 +162,7 @@ Section proof.
iMod
(
own_update_2
with
"[$Hauth $Hγo]"
)
as
"[Hauth Hγo]"
.
{
apply
auth_update
,
prod_local_update_1
.
by
apply
option_local_update
,
(
exclusive_local_update
_
(
Excl
(
S
o
))).
}
iMod
(
"Hclose"
with
"[Hlo Hln Hauth Haown Hγo HR]"
)
as
"_"
;
last
auto
.
iMod
(
"Hclose"
with
"[Hlo Hln Hauth Haown Hγo HR]"
)
as
"_"
;
last
by
iApply
"HΦ"
.
iNext
.
iExists
(
S
o
),
n'
.
rewrite
Nat2Z
.
inj_succ
-
Z
.
add_1_r
.
iFrame
.
iLeft
.
by
iFrame
.
Qed
.
...
...
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