Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Paolo G. Giarrusso
examples
Commits
85d365c5
Commit
85d365c5
authored
Jan 12, 2018
by
Aleš Bizjak
Browse files
Add second intro example file accompanying lecture notes.
parent
ece3f6fa
Changes
1
Hide whitespace changes
Inline
Sidebyside
theories/lecture_notes/coq_intro_example_2.v
0 → 100644
View file @
85d365c5
(* In this file we explain how to do prove the counter specifications from
Section 7.7 of the notes. This involves construction and manipulation of
resource algebras, the explanation of which is the focus of this file. We
assume the reader has experimented with coqintroexample1.v example, and
thus we do not explain the features we have explained therein already. *)
From
iris
.
program_logic
Require
Export
weakestpre
.
From
iris
.
base_logic
.
lib
Require
Export
invariants
.
From
iris
.
proofmode
Require
Import
tactics
.
From
iris
.
heap_lang
Require
Import
proofmode
.
From
iris
.
heap_lang
Require
Import
notation
lang
.
From
iris
.
heap_lang
.
lib
Require
Import
par
.
(* The counter module definition. *)
Definition
read
:
val
:
=
λ
:
"c"
,
!
"c"
.
Definition
incr
:
val
:
=
rec
:
"incr"
"c"
:
=
let
:
"n"
:
=
!
"c"
in
let
:
"m"
:
=
#
1
+
"n"
in
if
:
CAS
"c"
"n"
"m"
then
#()
else
"incr"
"c"
.
Definition
newCounter
:
val
:
=
λ
:
<>,
ref
#
0
.
Section
monotone_counter
.
(* For the first example we will only give the weaker specification, as we did
in the notes. In this specification we only know the lower bound on the
counter value, since the isCounter predicate is freely duplicable.
Before we start with the actual verification we will define the resource
algebra we shall be using. The Iris library contains all the ingredients
needed to compose this particular resource algebra from simpler components,
however to illustrate how to define our own we will define it from scratch.
In the subsequent section we show how to obtain an equivalent resource
algebra from the building blocks provided by the Iris Coq library.
*)
(* The carrier of our resource algebra is the set ℕ_{⊥,⊤} × ℕ. NBT (Natural
numbers with Top and Bottom) is the first component of this product. *)
Inductive
NBT
:
=
Bot
:
NBT
(* Bottom *)

Top
:
NBT
(* Top *)

NBT_incl
:
nat
→
NBT
.
(* Inclusion of natural numbers into our new type. *)
(* The carrier of our RA. *)
Definition
mcounterRAT
:
Type
:
=
NBT
*
nat
.
(* The notion of a resource algebra as used in Iris is more general than the one
currently described. It is called a cmra (standing roughly for complete
metric resource algebra). For most verification purposes it is not
important what that is. It is a stepindexed generalization of the resource
algebra we have described in Section 7. The main difference is that the
carrier is not simply a set, but comes equipped with a set of equivalence
relations indexed by natural numbers (the "stepindices").
The notion we have defined in Section 7 is that of a "discrete" CMRA. There
is special support in the library for such CMRAs, and that is why in the
remainder of this file we will often use, e.g., special lemmas for discrete
CMRAs.
*)
(*
To tell Coq we wish to use such a discrete CMRA we use the constructor leibnizC.
This takes a Coq type and makes it an instance of an OFE (a stepindexed generalization of sets).
This is not the place do describe Canonical Structures.
A very good introduction is available at https://hal.inria.fr/hal00816703v1/document
*)
Canonical
Structure
mcounterRAC
:
=
leibnizC
mcounterRAT
.
(* To make the type mcounterRAT into an RA we need an operation. This is
defined in the standard way, except we use the typeclass Op so we can reuse
a lot of the notation mechanism (we can write x ⋅ y for the operation), and
some other infrastucture and generic lemmas. *)
Instance
mcounterRAop
:
Op
mcounterRAT
:
=
λ
p
₁
p
₂
,
let
(
x
,
n
)
:
=
p
₁
in
let
(
y
,
m
)
:
=
p
₂
in
match
x
with
Bot
=>
(
y
,
max
n
m
)

_
=>
match
y
with
Bot
=>
(
x
,
max
n
m
)

_
=>
(
Top
,
max
n
m
)
end
end
.
(* The set of valid elements. Valid A is simply abbreviation for A → Prop,
i.e., for the set of subsets of A. Importantly Valid is a typeclass, and
thus we make our definition an instance of it. This will enable the Coq
typeclass search and various interactive proof mode tactics automatically
deal with many boring use cases. *)
Instance
mcounterRAValid
:
Valid
mcounterRAT
:
=
λ
x
,
match
x
with
(
Bot
,
_
)
=>
True

(
NBT_incl
x
,
m
)
=>
x
≥
m

_
=>
False
end
.
(* The core of the RA. PCore stands for "partial core", and is an abbreviation
for a partial function, which in Coq is encoded as a function from A →
option A. Again, PCore is a typeclass for better automation support, and
thus our definition is an instance. *)
Instance
mcounterRACore
:
PCore
mcounterRAT
:
=
λ
x
,
let
(
_
,
n
)
:
=
x
in
Some
(
Bot
,
n
).
(* We can then package these definitions up into an RA structure, used by the
Iris library. *)
(* We need these auxiliary lemmas in the proof below.
We need the type annotation to guide the type inference. *)
Lemma
mcounterRA_op_second
(
x
y
:
NBT
)
n
m
:
∃
z
,
((
x
,
n
)
:
mcounterRAT
)
⋅
(
y
,
m
)
=
(
z
,
max
n
m
).
Proof
.
destruct
x
as
[],
y
as
[]
;
eexists
;
unfold
op
,
mcounterRAop
;
simpl
;
auto
.
Qed
.
Lemma
mcounterRA_included_aux
x
y
(
n
m
:
nat
)
:
((
x
,
n
)
:
mcounterRAT
)
≼
(
y
,
m
)
→
(
n
≤
m
)%
nat
.
Proof
.
intros
[[
z
k
]
[=
H
]].
revert
H
.
destruct
(
mcounterRA_op_second
x
z
n
k
)
as
[?
>].
inversion
1
;
subst
;
auto
with
arith
.
Qed
.
Lemma
mcounterRA_included_frag
(
n
m
:
nat
)
:
((
Bot
,
n
)
:
mcounterRAT
)
≼
(
Bot
,
m
)
↔
(
n
≤
m
)%
nat
.
Proof
.
split
.

apply
mcounterRA_included_aux
.

intros
H
%
Max
.
max_r
;
exists
(
Bot
,
m
)
;
unfold
op
,
mcounterRAop
;
rewrite
H
;
auto
.
Qed
.
Lemma
mcounterRA_valid
x
(
n
:
nat
)
:
✓
((
NBT_incl
x
,
n
)
:
mcounterRAT
)
↔
(
n
≤
x
)%
nat
.
Proof
.
split
;
auto
.
Qed
.
(* An RAMixin is a structure which combines all the parts of an RA into one
Coq structure, together with all the properties that the operations and
functions satisfy. *)
Definition
mcounterRA_mixin
:
RAMixin
mcounterRAT
.
Proof
.
split
;
try
apply
_;
try
done
.
unfold
valid
,
op
,
mcounterRAop
,
mcounterRAValid
.
intros
?
?
cx
>
?
;
exists
cx
.
done
.
(* The operation is associative. *)

unfold
op
,
mcounterRAop
.
intros
[[]]
[[]]
[[]]
;
rewrite
!
Nat
.
max_assoc
;
reflexivity
.
(* The operation is commutative. *)

unfold
op
,
mcounterRAop
.
intros
[[]]
[[]]
;
rewrite
Nat
.
max_comm
;
reflexivity
.
(* Core axioms. *)

unfold
pcore
,
mcounterRACore
,
op
,
mcounterRAop
;
intros
[[]]
[[]]
[=>]
;
rewrite
Max
.
max_idempotent
;
auto
.

unfold
pcore
,
mcounterRACore
,
op
,
mcounterRAop
;
intros
[[]]
[[]]
[=>]
;
auto
.

unfold
pcore
,
mcounterRACore
,
op
,
mcounterRAop
.
intros
[
x
n
]
[
y
m
]
cx
Hleq
%
mcounterRA_included_aux
[=<].
exists
(
Bot
,
m
)
;
split
;
first
auto
.
by
apply
mcounterRA_included_frag
.

(* Validity axiom: validity is downclosed with respect to the extension order. *)
intros
[[]].
+
reflexivity
.
+
unfold
op
,
mcounterRAop
;
intros
[[]]
[].
+
unfold
op
,
mcounterRAop
;
intros
[[]].
*
rewrite
!
mcounterRA_valid
.
eauto
with
arith
.
*
intros
[].
*
intros
[].
Qed
.
(* We finally wrap the type and the above mixin and make the structure
available for typeclass search. The discreteR is a wrapper for when our CMRA is
"discrete" as described above. *)
Canonical
Structure
mcounterRA
:
=
discreteR
mcounterRAT
mcounterRA_mixin
.
(* Some tactics and lemmas only apply for discrete CMRAs (what we called RAs).
To be able to use these we need to register our CMRA as a discrete one, to
make this information available to typeclass search. *)
Instance
mcounterRA_cmra_discrete
:
CmraDiscrete
mcounterRA
.
Proof
.
apply
discrete_cmra_discrete
.
Qed
.
(* A total CMRA (or RA) is the one where the core operation is a total
function, i.e., the core of every element is defined. Some properties and
lemmas only apply for such CMRAs, and so we register the fact that our CMRA
is of this form.
*)
Instance
mcounterRA_cmra_total
:
CmraTotal
mcounterRA
.
Proof
.
intros
[[]]
;
eauto
.
Qed
.
(* We define some abbreviation. We only define it as notation in this section
since the same notation is already defined for the general authoritative RA
construction in the Iris Coq library.
*)
Local
Notation
"◯ n"
:
=
((
Bot
,
n
%
nat
)
:
mcounterRA
)
(
at
level
20
).
Local
Notation
"● m"
:
=
((
NBT_incl
m
%
nat
,
0
%
nat
)
:
mcounterRA
)
(
at
level
20
).
(* We now prove the three properties we claim were required from the resource
algebra in Section 7.7.
*)
(* CoreId x states that the core of x is x, which is one of the properties we claimed for the
fragments. CoreId is a typeclass. *)
Instance
mcounterRA_frag_core
(
n
:
nat
)
:
CoreId
(
◯
n
).
Proof
.
rewrite
/
CoreId
;
reflexivity
.
Qed
.
Lemma
mcounterRA_valid_auth_frag
m
n
:
✓
(
●
m
⋅
◯
n
)
↔
(
n
≤
m
)%
nat
.
Proof
.
apply
mcounterRA_valid
.
Qed
.
Lemma
mcounterRA_update
m
n
:
((
●
m
⋅
◯
n
)
:
mcounterRA
)
~~>
(
●
(
1
+
m
)
⋅
◯
(
1
+
n
)).
Proof
.
(* Use the specialized definition of update, since our RA is a nice one. *)
apply
cmra_discrete_update
.
intros
[[]
k
].

rewrite
/
op
/
cmra_op
!
mcounterRA_valid
;
lia
.

intros
[].

intros
[].
Qed
.
(* We now need to tell Coq to use our RA as one of the RA's in the instantiation of Iris. *)
(* This is achieved via the subG constructor. All of this is boilerplate, so
the proofs are trivial, with the tactics provided by the library. *)
Class
mcounterG
Σ
:
=
MCounterG
{
mcounter_inG
:
>
inG
Σ
mcounterRA
}.
Definition
mcounter
Σ
:
gFunctors
:
=
#[
GFunctor
mcounterRA
].
Instance
subG_mcounter
Σ
{
Σ
}
:
subG
mcounter
Σ
Σ
→
mcounterG
Σ
.
Proof
.
solve_inG
.
Qed
.
(* We can now verify the programs. *)
(* We start off as in the previous example, with some boilerplate code. *)
Context
`
{!
heapG
Σ
,
!
mcounterG
Σ
}
(
N
:
namespace
).
Notation
iProp
:
=
(
iProp
Σ
).
(* The counter invariant as defined in the notes. The only difference is that
we are using the namespace N for the invariant, instead of existentially
quantifying the invariant name. *)
Definition
counter_inv
(
ℓ
:
loc
)
(
γ
:
gname
)
:
iProp
:
=
(
∃
(
m
:
nat
),
ℓ
↦
#
m
∗
own
γ
(
●
m
))%
I
.
(* the isCounter predicate as in the notes. *)
Definition
isCounter
(
ℓ
:
loc
)
(
n
:
nat
)
:
iProp
:
=
(
∃
γ
,
own
γ
(
◯
n
)
∗
inv
N
(
counter_inv
ℓ
γ
))%
I
.
(* isCounter is a persistent predicate. This is needed so we can share it among threads. *)
(* We first need an auxiliary lemma, which tells Coq that ownership of fragments is persistent.
This follows from the persistentlycore axiom of the logic.
Instead of proving this as a lemma we make it an instance of the Persistent class.
This way Coq will be able to infer automatically whenever it needs the fact
that ownership of fragments is persistent.
*)
Instance
ownFrac_persistent
γ
n
:
Persistent
(
own
γ
(
◯
n
)).
Proof
.
apply
own_core_persistent
,
_
.
Qed
.
(* Now the proof of the main counter predicate is simple: Coq's typeclass
search can automatically deduce that isCounter is persistent. It knows the
closure properties of persistent propositions, e.g., existential
quantification over a persistent predicate is persistent, and it knows that
invariants are persistent. The final part it needs is that own γ (◯ n) is
persistent, and we have just taught it that in the preceding lemma. *)
Instance
isCounter_persistent
ℓ
n
:
Persistent
(
isCounter
ℓ
n
).
Proof
.
apply
_
.
Qed
.
(* We can now perform the main proofs. They are not very different from the
proofs we have done previously. *)
Lemma
newCounter_spec
:
{{{
True
}}}
newCounter
#()
{{{
v
,
RET
#
v
;
isCounter
v
0
}}}.
Proof
.
iIntros
(
Φ
)
"_ HCont"
.
rewrite
/
newCounter

wp_fupd
.
(* See comment below for why we used wp_fupd. *)
wp_lam
.
(* We allocate ghost state using the rule/lemma own_alloc. Since the
conclusion of the rule is under a modality we wrap the application of
this lemma with the call to the iMod tactic, which takes care of the
bookkeeping, using the primitive rules of the modality.
In this case the tactic knows that ==> WP ... implies WP ... and thus removes it from the goal.
*)
iMod
(
own_alloc
(
●
0
⋅
◯
0
))
as
(
γ
)
"[HAuth HFrac]"
.

apply
mcounterRA_valid_auth_frag
;
auto
.
(* NOTE: We use the validity property of the RA we have constructed. *)

wp_alloc
ℓ
as
"Hpt"
.
(* We now allocate an invariant. For this it is crucial we have used the
wp_fupd lemma above to have the Φ under a modality. Otherwise we would
have been stuck here, since allocating an invariant is only possible
under the fancy update modality. *)
iMod
(
inv_alloc
N
_
(
counter_inv
ℓ
γ
)
with
"[Hpt HAuth]"
)
as
"HInv"
.
+
iExists
0
%
nat
;
iFrame
.
+
iApply
(
"HCont"
with
"[HFrac HInv]"
).
iExists
γ
;
iFrame
.
Qed
.
(* The read method specification. *)
Lemma
read_spec
ℓ
n
:
{{{
isCounter
ℓ
n
}}}
read
#
ℓ
{{{
m
,
RET
#
m
;
⌜
n
≤
m
⌝
%
nat
}}}.
Proof
.
iIntros
(
Φ
)
"HCounter HCont"
.
iDestruct
"HCounter"
as
(
γ
)
"[HOwnFrag HInv]"
.
rewrite
/
read
.
wp_lam
.
iInv
N
as
(
m
)
">[Hpt HOwnAuth]"
"HClose"
.
wp_load
.
(* NOTE: We use the validity property of the RA we have constructed. From the fact that we own
◯ n and ● m to conclude that n ≤ m. *)
iDestruct
(@
own_valid_2
_
_
_
γ
with
"HOwnAuth HOwnFrag"
)
as
%
H
%
mcounterRA_valid_auth_frag
.
iMod
(
"HClose"
with
"[Hpt HOwnAuth]"
)
as
"_"
.
{
iNext
;
iExists
m
;
iFrame
.
}
iModIntro
.
iApply
"HCont"
;
done
.
Qed
.
(* The read method specification. *)
Lemma
incr_spec
ℓ
n
:
{{{
isCounter
ℓ
n
}}}
incr
#
ℓ
{{{
RET
#()
;
isCounter
ℓ
(
1
+
n
)%
nat
}}}.
Proof
.
iIntros
(
Φ
)
"HCounter HCont"
.
iDestruct
"HCounter"
as
(
γ
)
"[HOwnFrag #HInv]"
.
iL
ö
b
as
"IH"
.
rewrite
/
incr
.
wp_lam
.
wp_bind
(!
_
)%
E
.
iInv
N
as
(
m
)
">[Hpt HOwnAuth]"
"HClose"
.
wp_load
.
iDestruct
(@
own_valid_2
_
_
_
γ
with
"HOwnAuth HOwnFrag"
)
as
%
H
%
mcounterRA_valid_auth_frag
.
iMod
(
"HClose"
with
"[Hpt HOwnAuth]"
)
as
"_"
.
{
iNext
;
iExists
m
;
iFrame
.
}
iModIntro
.
wp_lam
;
wp_op
;
wp_lam
.
wp_bind
(
CAS
_
_
_
)%
E
.
iInv
N
as
(
k
)
">[Hpt HOwnAuth]"
"HClose"
.
destruct
(
decide
(
k
=
m
))
;
subst
.
+
wp_cas_suc
.
(* If the CAS succeeds we need to update our ghost state. This is achieved using the own_update rule/lemma.
The arguments are the ghost name and the ghost resources x from which and to which we are updating.
Finally we need to give up own γ x to get ownership of the new resources.
We do this using the "with ..." syntax.
Again, the conclusion of the update rule is under the update modality,
and thus we wrap the application of the lemma with the iMod tactic. *)
iMod
(
own_update
γ
((
●
m
⋅
◯
n
)
:
mcounterRA
)
(
●
(
1
+
m
)
⋅
◯
(
1
+
n
))
with
"[HOwnFrag HOwnAuth]"
)
as
"[HOwnAuth HOwnFrag]"
.
{
apply
mcounterRA_update
.
}
(* We need the final property of the RA we proved above: the frame preserving update from (● m ⋅ ◯ n) to (● (1 + m) ⋅ ◯ (1 + n)). *)
{
rewrite
own_op
;
iFrame
.
}
iMod
(
"HClose"
with
"[Hpt HOwnAuth]"
)
as
"_"
.
{
iNext
;
iExists
(
1
+
m
)%
nat
.
rewrite
Nat2Z
.
inj_succ
Z
.
add_1_l
;
iFrame
.
}
iModIntro
;
wp_if
;
iApply
(
"HCont"
with
"[HInv HOwnFrag]"
).
iExists
γ
;
iFrame
"#"
;
iFrame
.
+
wp_cas_fail
;
first
intros
?
;
simplify_eq
.
iMod
(
"HClose"
with
"[Hpt HOwnAuth]"
)
as
"_"
.

iExists
k
;
iFrame
.

iModIntro
;
wp_if
.
iApply
(
"IH"
with
"HOwnFrag HCont"
)
;
iFrame
.
Qed
.
End
monotone_counter
.
(* In the preceding section we spent a lot of time defining our own resource
algebra and proving it satisfies all the needed properties. The same patterns
appear often in proof development, and thus the iris Coq library provides
several building blocks for constructing resource algebras.
In the following section we repeat the above specification, but with a
resource algebra constructed using these building blocks. We will see that
this will save us quite a bit of work.
As we stated in an exercise in the counter modules section of the lecture
notes, the resource algebra we constructed above is nothing but Auth(N_max).
Auth and N_max are both part of the iris Coq library. They are called authR
and mnatUR (standing for authoritative Resource algebra and max nat Unital
Resource algebra). *)
(* Auth is defined in iris.algebra.auth. *)
From
iris
.
algebra
Require
Import
auth
.
(* The following section is a generic update property of the authoritative construction.
In the Iris Coq library there are several update lemmas, using the concept of local updates
(notation x ~l~> y, and the definition is called local_update).
The two updates in the following section are the same as stated in the exercise in the notes.
*)
Section
auth_update
.
Context
{
U
:
ucmraT
}.
Lemma
auth_update_add
(
x
y
z
:
U
)
:
✓
(
x
⋅
z
)
→
●
x
⋅
◯
y
~~>
●
(
x
⋅
z
)
⋅
◯
(
y
⋅
z
).
Proof
.
intros
?.
(* auth_update is the generic update rule for the auth RA. It reduces a
frame preserving update to that of a local update. *)
apply
auth_update
.
intros
?
mz
?
Heq
.
split
.

apply
cmra_valid_validN
;
auto
.

simpl
in
*.
rewrite
Heq
.
destruct
mz
;
simpl
;
auto
.
rewrite

assoc
(
comm
_
_
z
)
assoc
//.
Qed
.
Lemma
auth_update_add'
(
x
y
z
w
:
U
)
:
✓
(
x
⋅
z
)
→
w
≼
z
→
●
x
⋅
◯
y
~~>
●
(
x
⋅
z
)
⋅
◯
(
y
⋅
w
).
Proof
.
(* The proof of this lemma uses the previous lemma, together with the fact
that ~~> is transitive, and the fact that we always have the frame
preserving update from a ⋅ b to a. This is proved in cmra_update_op_l in
the Coq library.
*)
intros
Hv
[?
He
].
etransitivity
.
apply
(
auth_update_add
x
y
z
Hv
).
rewrite
{
2
}
He
assoc
auth_frag_op
assoc
.
apply
cmra_update_op_l
.
Qed
.
End
auth_update
.
Section
monotone_counter'
.
(* We tell Coq that our Iris instantiation has the following resource
algebras. Note that the only diffference from above is that we use authR
mnatUR in place of the resource algebra mcounterRA we constructed above. *)
Class
mcounterG'
Σ
:
=
MCounterG'
{
mcounter_inG'
:
>
inG
Σ
(
authR
mnatUR
)}.
Definition
mcounter
Σ
'
:
gFunctors
:
=
#[
GFunctor
(
authR
mnatUR
)].
Instance
subG_mcounter
Σ
'
{
Σ
}
:
subG
mcounter
Σ
'
Σ
→
mcounterG'
Σ
.
Proof
.
solve_inG
.
Qed
.
(* We now prove the same three properties we claim were required from the resource
algebra in Section 7.7. *)
Instance
mcounterRA_frag_core'
(
n
:
mnatUR
)
:
CoreId
(
◯
n
).
Proof
.
apply
_
.
(* CoreID is a typeclass, so typeclass search can automatically deduce what
we want. Concretely, the proof follows by lemmas auth_frag_core_id and
mnat_core_id proved in the Iris Coq library. *)
Qed
.
Lemma
mcounterRA_valid_auth_frag'
(
m
n
:
mnatUR
)
:
✓
(
●
m
⋅
◯
n
)
↔
(
n
≤
m
)%
nat
.
Proof
.
(* Use a simplified definition of validity for when the underlying CMRA is discrete, i.e., an RA.
The general definition also involves the use of stepindices, which is not needed in our case. *)
rewrite
auth_valid_discrete_2
.
split
.

intros
[?
_
]
;
by
apply
mnat_included
.

intros
?%
mnat_included
;
done
.
Qed
.
Lemma
mcounterRA_update'
(
m
n
:
mnatUR
)
:
●
m
⋅
◯
n
~~>
●
(
S
m
:
mnatUR
)
⋅
◯
(
S
n
:
mnatUR
).
Proof
.
replace
(
S
m
)
with
(
m
⋅
(
S
m
))
;
last
auto
with
arith
.
replace
(
S
n
)
with
(
n
⋅
(
S
n
))
;
last
auto
with
arith
.
apply
cmra_update_valid0
;
intros
?%
cmra_discrete_valid
%
mcounterRA_valid_auth_frag'
.
apply
auth_update_add'
;
first
reflexivity
.
exists
(
S
m
)
;
symmetry
;
apply
max_r
;
auto
with
arith
.
Qed
.
(* We can now verify the programs. *)
(* We start off as in the previous example, with some boilerplate code. *)
Context
`
{!
heapG
Σ
,
!
mcounterG'
Σ
}
(
N
:
namespace
).
Notation
iProp
:
=
(
iProp
Σ
).
(* The rest of this section is exactly the same as the preceding one. We use
the properties of the RA we have proved above. *)
Definition
counter_inv'
(
ℓ
:
loc
)
(
γ
:
gname
)
:
iProp
:
=
(
∃
(
m
:
mnatUR
),
ℓ
↦
#
m
∗
own
γ
(
●
m
))%
I
.
Definition
isCounter'
(
ℓ
:
loc
)
(
n
:
mnatUR
)
:
iProp
:
=
(
∃
γ
,
own
γ
(
◯
n
)
∗
inv
N
(
counter_inv'
ℓ
γ
))%
I
.
Global
Instance
isCounter_persistent'
ℓ
n
:
Persistent
(
isCounter'
ℓ
n
).
Proof
.
apply
_
.
Qed
.
Lemma
newCounter_spec'
:
{{{
True
}}}
newCounter
#()
{{{
v
,
RET
#
v
;
isCounter'
v
0
%
nat
}}}.
Proof
.
iIntros
(
Φ
)
"_ HCont"
.
rewrite
/
newCounter

wp_fupd
.
wp_lam
.
iMod
(
own_alloc
(
●
(
0
%
nat
:
mnatUR
)
⋅
◯
0
%
nat
))
as
(
γ
)
"[HAuth HFrac]"
.

apply
mcounterRA_valid_auth_frag'
;
auto
.

wp_alloc
ℓ
as
"Hpt"
.
iMod
(
inv_alloc
N
_
(
counter_inv'
ℓ
γ
)
with
"[Hpt HAuth]"
)
as
"HInv"
.
+
iExists
0
%
nat
;
iFrame
.
+
iApply
(
"HCont"
with
"[HFrac HInv]"
).
iExists
γ
;
iFrame
.
Qed
.
(* The read method specification. *)
Lemma
read_spec'
ℓ
n
:
{{{
isCounter'
ℓ
n
}}}
read
#
ℓ
{{{
m
,
RET
#
m
;
⌜
n
≤
m
⌝
%
nat
}}}.
Proof
.
iIntros
(
Φ
)
"HCounter HCont"
.
iDestruct
"HCounter"
as
(
γ
)
"[HOwnFrag HInv]"
.
rewrite
/
read
.
wp_lam
.
iInv
N
as
(
m
)
">[Hpt HOwnAuth]"
"HClose"
.
wp_load
.
iDestruct
(@
own_valid_2
_
_
_
γ
with
"HOwnAuth HOwnFrag"
)
as
%
H
%
mcounterRA_valid_auth_frag'
.
iMod
(
"HClose"
with
"[Hpt HOwnAuth]"
)
as
"_"
.
{
iNext
;
iExists
m
;
iFrame
.
}
iModIntro
.
iApply
"HCont"
;
done
.
Qed
.
(* The read method specification. *)
Lemma
incr_spec'
ℓ
n
:
{{{
isCounter'
ℓ
n
}}}
incr
#
ℓ
{{{
RET
#()
;
isCounter'
ℓ
(
1
+
n
)%
nat
}}}.
Proof
.
iIntros
(
Φ
)
"HCounter HCont"
.
iDestruct
"HCounter"
as
(
γ
)
"[HOwnFrag #HInv]"
.
iL
ö
b
as
"IH"
.
rewrite
/
incr
.
wp_lam
.
wp_bind
(!
_
)%
E
.
iInv
N
as
(
m
)
">[Hpt HOwnAuth]"
"HClose"
.
wp_load
.
iDestruct
(@
own_valid_2
_
_
_
γ
with
"HOwnAuth HOwnFrag"
)
as
%
H
%
mcounterRA_valid_auth_frag'
.
iMod
(
"HClose"
with
"[Hpt HOwnAuth]"
)
as
"_"
.
{
iNext
;
iExists
m
;
iFrame
.
}
iModIntro
.
wp_lam
;
wp_op
;
wp_lam
.
wp_bind
(
CAS
_
_
_
)%
E
.
iInv
N
as
(
k
)
">[Hpt HOwnAuth]"
"HClose"
.
destruct
(
decide
(
k
=
m
))
;
subst
.
+
wp_cas_suc
.
iMod
(
own_update
γ
((
●
m
⋅
◯
n
))
(
●
(
S
m
:
mnatUR
)
⋅
(
◯
S
n
))
with
"[HOwnFrag HOwnAuth]"
)
as
"[HOwnAuth HOwnFrag]"
.
{
apply
mcounterRA_update'
.
}
{
rewrite
own_op
;
iFrame
.
}
iMod
(
"HClose"
with
"[Hpt HOwnAuth]"
)
as
"_"
.
{
iNext
;
iExists
(
1
+
m
)%
nat
.
rewrite
Nat2Z
.
inj_succ
Z
.
add_1_l
;
iFrame
.
}
iModIntro
;
wp_if
;
iApply
(
"HCont"
with
"[HInv HOwnFrag]"
).
iExists
γ
;
iFrame
"#"
;
iFrame
.
+
wp_cas_fail
;
first
intros
?
;
simplify_eq
.
iMod
(
"HClose"
with
"[Hpt HOwnAuth]"
)
as
"_"
.

iExists
k
;
iFrame
.

iModIntro
;
wp_if
.
iApply
(
"IH"
with
"HOwnFrag HCont"
)
;
iFrame
.
Qed
.
End
monotone_counter'
.
(* Counter with contributions. *)
(* As a final example in this example file we give the more precise specification to the counter. *)
(* As explained in the lecture notes we need a different resource algebra: the
authoritative resource algebra on the product of the RA of fractions and the
RA of natural numbers, with an added unit.
The combination of the RA of fractions and the authoritative RA in this way
is fairly common, and so the Iris Coq library provides frac_authR (CM)RA. *)
From
iris
.
algebra
Require
Import
frac_auth
.
Section
ccounter
.
(* We start as we did before, telling Coq what we assume from the Iris instantiation. *)
(* Note that now we use natR as the underlying resource algebra. This is the
RA of natural numbers with addition as the operation. *)
Class
ccounterG
Σ
:
=
CCounterG
{
ccounter_inG
:
>
inG
Σ
(
frac_authR
natR
)
}.
Definition
ccounter
Σ
:
gFunctors
:
=
#[
GFunctor
(
frac_authR
natR
)].
Instance
subG_ccounter
Σ
{
Σ
}
:
subG
ccounter
Σ
Σ
→
ccounterG
Σ
.
Proof
.
solve_inG
.
Qed
.
(* The first thing we are going to prove are the properties of the resource
algebra, specialized to our use case. These are listed in the exercise in
the relevant section of the lecture notes. *)
(* We are using some new notation. The frac_auth library defines the notation
◯!{q} n to mean ◯ (q, n) as we used in the lecture notes. Further, ●! m
means ● (1, m) and ◯! n means ◯ (1, n). *)
Lemma
ccounterRA_valid
(
m
n
:
natR
)
(
q
:
frac
)
:
✓
(
●
!
m
⋅
◯
!{
q
}
n
)
→
(
n
≤
m
)%
nat
.
Proof
.
intros
?.
(* This property follows directly from the generic properties of the relevant RAs. *)
by
apply
nat_included
,
(
frac_auth_included_total
q
).
Qed
.
Lemma
ccounterRA_valid_full
(
m
n
:
natR
)
:
✓
(
●
!
m
⋅
◯
!
n
)
→
(
n
=
m
)%
nat
.
Proof
.
by
intros
?%
frac_auth_agree
.
Qed
.
Lemma
ccounterRA_update
(
m
n
:
natR
)
(
q
:
frac
)
:
(
●
!
m
⋅
◯
!{
q
}
n
)
~~>
(
●
!
(
S
m
)
⋅
◯
!{
q
}
(
S
n
)).