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
Jonas Kastberg
iris
Commits
7527bd61
Commit
7527bd61
authored
Nov 03, 2016
by
Robbert Krebbers
Browse files
Rename "inc" of counter into "incr".
parent
3f678b90
Changes
2
Hide whitespace changes
Inline
Side-by-side
heap_lang/lib/counter.v
View file @
7527bd61
...
...
@@ -5,12 +5,12 @@ From iris.algebra Require Import frac auth.
From
iris
.
heap_lang
Require
Import
proofmode
notation
.
Definition
newcounter
:
val
:
=
λ
:
<>,
ref
#
0
.
Definition
inc
:
val
:
=
rec
:
"inc"
"l"
:
=
Definition
inc
r
:
val
:
=
rec
:
"inc
r
"
"l"
:
=
let
:
"n"
:
=
!
"l"
in
if
:
CAS
"l"
"n"
(#
1
+
"n"
)
then
#()
else
"inc"
"l"
.
if
:
CAS
"l"
"n"
(#
1
+
"n"
)
then
#()
else
"inc
r
"
"l"
.
Definition
read
:
val
:
=
λ
:
"l"
,
!
"l"
.
Global
Opaque
newcounter
inc
get
.
Global
Opaque
newcounter
inc
r
get
.
(** Monotone counter *)
Class
mcounterG
Σ
:
=
MCounterG
{
mcounter_inG
:
>
inG
Σ
(
authR
mnatUR
)
}.
...
...
@@ -44,8 +44,8 @@ Section mono_proof.
iModIntro
.
iApply
"HΦ"
.
rewrite
/
mcounter
;
eauto
10
.
Qed
.
Lemma
inc_mono_spec
l
n
:
{{{
mcounter
l
n
}}}
inc
#
l
{{{
RET
#()
;
mcounter
l
(
S
n
)
}}}.
Lemma
inc
r
_mono_spec
l
n
:
{{{
mcounter
l
n
}}}
inc
r
#
l
{{{
RET
#()
;
mcounter
l
(
S
n
)
}}}.
Proof
.
iIntros
(
Φ
)
"Hl HΦ"
.
iL
ö
b
as
"IH"
.
wp_rec
.
iDestruct
"Hl"
as
(
γ
)
"(% & #? & #Hinv & Hγf)"
.
...
...
@@ -122,8 +122,8 @@ Section contrib_spec.
iModIntro
.
iApply
"HΦ"
.
rewrite
/
ccounter_ctx
/
ccounter
;
eauto
10
.
Qed
.
Lemma
inc_contrib_spec
γ
l
q
n
:
{{{
ccounter_ctx
γ
l
∗
ccounter
γ
q
n
}}}
inc
#
l
Lemma
inc
r
_contrib_spec
γ
l
q
n
:
{{{
ccounter_ctx
γ
l
∗
ccounter
γ
q
n
}}}
inc
r
#
l
{{{
RET
#()
;
ccounter
γ
q
(
S
n
)
}}}.
Proof
.
iIntros
(
Φ
)
"(#(%&?&?) & Hγf) HΦ"
.
iL
ö
b
as
"IH"
.
wp_rec
.
...
...
tests/counter.v
View file @
7527bd61
...
...
@@ -11,12 +11,12 @@ From iris.heap_lang Require Import proofmode notation.
Import
uPred
.
Definition
newcounter
:
val
:
=
λ
:
<>,
ref
#
0
.
Definition
inc
:
val
:
=
rec
:
"inc"
"l"
:
=
Definition
inc
r
:
val
:
=
rec
:
"inc
r
"
"l"
:
=
let
:
"n"
:
=
!
"l"
in
if
:
CAS
"l"
"n"
(#
1
+
"n"
)
then
#()
else
"inc"
"l"
.
if
:
CAS
"l"
"n"
(#
1
+
"n"
)
then
#()
else
"inc
r
"
"l"
.
Definition
read
:
val
:
=
λ
:
"l"
,
!
"l"
.
Global
Opaque
newcounter
inc
read
.
Global
Opaque
newcounter
inc
r
read
.
(** The CMRA we need. *)
Inductive
M
:
=
Auth
:
nat
→
M
|
Frag
:
nat
→
M
|
Bot
.
...
...
@@ -103,8 +103,8 @@ Proof.
iModIntro
.
rewrite
/
C
;
eauto
10
.
Qed
.
Lemma
inc_spec
l
n
:
{{
C
l
n
}}
inc
#
l
{{
v
,
v
=
#()
∧
C
l
(
S
n
)
}}.
Lemma
inc
r
_spec
l
n
:
{{
C
l
n
}}
inc
r
#
l
{{
v
,
v
=
#()
∧
C
l
(
S
n
)
}}.
Proof
.
iIntros
"!# Hl /="
.
iL
ö
b
as
"IH"
.
wp_rec
.
iDestruct
"Hl"
as
(
N
γ
)
"(% & #Hh & #Hinv & Hγf)"
.
...
...
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