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
Adam
Iris
Commits
2bc880b2
Commit
2bc880b2
authored
Mar 15, 2021
by
Ralf Jung
Browse files
move error into regular .v file
parent
59d18188
Changes
2
Hide whitespace changes
Inline
Side-by-side
_CoqProject
View file @
2bc880b2
...
...
@@ -166,6 +166,7 @@ iris_heap_lang/lib/increment.v
iris_heap_lang/lib/diverge.v
iris_heap_lang/lib/arith.v
iris_heap_lang/lib/array.v
iris_heap_lang/lib/one_shot.v
iris_deprecated/base_logic/auth.v
iris_deprecated/base_logic/sts.v
...
...
iris_heap_lang/lib/one_shot.v
0 → 100644
View file @
2bc880b2
From
iris
.
algebra
Require
Import
excl
agree
csum
.
From
iris
.
proofmode
Require
Import
tactics
.
From
iris
.
program_logic
Require
Export
weakestpre
.
From
iris
.
deprecated
.
program_logic
Require
Import
hoare
.
From
iris
.
heap_lang
Require
Export
lang
.
From
iris
.
heap_lang
Require
Import
assert
proofmode
notation
adequacy
.
From
iris
.
heap_lang
.
lib
Require
Import
par
.
Set
Default
Proof
Using
"Type"
.
(** This is the introductory example from the "Iris from the Ground Up" journal
paper. *)
Unset
Mangle
Names
.
Definition
one_shot_example
:
val
:
=
λ
:
<>,
let
:
"x"
:
=
ref
NONE
in
(
(* tryset *)
(
λ
:
"n"
,
CAS
"x"
NONE
(
SOME
"n"
)),
(* check *)
(
λ
:
<>,
let
:
"y"
:
=
!
"x"
in
λ
:
<>,
match
:
"y"
with
NONE
=>
#()
|
SOME
"n"
=>
match
:
!
"x"
with
NONE
=>
assert
:
#
false
|
SOME
"m"
=>
assert
:
"n"
=
"m"
end
end
)).
Definition
one_shotR
:
=
csumR
(
exclR
unitO
)
(
agreeR
ZO
).
Definition
Pending
:
one_shotR
:
=
Cinl
(
Excl
()).
Definition
Shot
(
n
:
Z
)
:
one_shotR
:
=
Cinr
(
to_agree
n
).
Class
one_shotG
Σ
:
=
{
one_shot_inG
:
>
inG
Σ
one_shotR
}.
Definition
one_shot
Σ
:
gFunctors
:
=
#[
GFunctor
one_shotR
].
Global
Instance
subG_one_shot
Σ
{
Σ
}
:
subG
one_shot
Σ
Σ
→
one_shotG
Σ
.
Proof
.
solve_inG
.
Qed
.
Section
proof
.
Local
Set
Default
Proof
Using
"Type*"
.
Context
`
{!
heapG
Σ
,
!
one_shotG
Σ
}.
Definition
one_shot_inv
(
γ
:
gname
)
(
l
:
loc
)
:
iProp
Σ
:
=
(
l
↦
NONEV
∗
own
γ
Pending
∨
∃
n
:
Z
,
l
↦
SOMEV
#
n
∗
own
γ
(
Shot
n
))%
I
.
Lemma
wp_one_shot
(
Φ
:
val
→
iProp
Σ
)
:
(
∀
f1
f2
:
val
,
(
∀
n
:
Z
,
□
WP
f1
#
n
{{
w
,
⌜
w
=
#
true
⌝
∨
⌜
w
=
#
false
⌝
}})
∗
□
WP
f2
#()
{{
g
,
□
WP
g
#()
{{
_
,
True
}}
}}
-
∗
Φ
(
f1
,
f2
)%
V
)
⊢
WP
one_shot_example
#()
{{
Φ
}}.
Proof
.
iIntros
"Hf /="
.
pose
proof
(
nroot
.@
"N"
)
as
N
.
wp_lam
.
wp_alloc
l
as
"Hl"
.
iMod
(
own_alloc
Pending
)
as
(
γ
)
"Hγ"
;
first
done
.
iMod
(
inv_alloc
N
_
(
one_shot_inv
γ
l
)
with
"[Hl Hγ]"
)
as
"#HN"
.
{
iNext
.
iLeft
.
by
iSplitL
"Hl"
.
}
wp_pures
.
iModIntro
.
iApply
"Hf"
;
iSplit
.
-
iIntros
(
n
)
"!>"
.
wp_lam
.
wp_pures
.
wp_bind
(
CmpXchg
_
_
_
).
iInv
N
as
">[[Hl Hγ]|H]"
;
last
iDestruct
"H"
as
(
m
)
"[Hl Hγ]"
.
+
iMod
(
own_update
with
"Hγ"
)
as
"Hγ"
.
{
by
apply
cmra_update_exclusive
with
(
y
:
=
Shot
n
).
}
wp_cmpxchg_suc
.
iModIntro
.
iSplitL
;
last
(
wp_pures
;
by
eauto
).
iNext
;
iRight
;
iExists
n
;
by
iFrame
.
+
wp_cmpxchg_fail
.
iModIntro
.
iSplitL
;
last
(
wp_pures
;
by
eauto
).
rewrite
/
one_shot_inv
;
eauto
10
.
-
iIntros
"!> /="
.
wp_lam
.
wp_bind
(!
_
)%
E
.
iInv
N
as
">Hγ"
.
iAssert
(
∃
v
,
l
↦
v
∗
((
⌜
v
=
NONEV
⌝
∗
own
γ
Pending
)
∨
∃
n
:
Z
,
⌜
v
=
SOMEV
#
n
⌝
∗
own
γ
(
Shot
n
)))%
I
with
"[Hγ]"
as
"Hv"
.
{
iDestruct
"Hγ"
as
"[[Hl Hγ]|Hl]"
;
last
iDestruct
"Hl"
as
(
m
)
"[Hl Hγ]"
.
+
iExists
NONEV
.
iFrame
.
eauto
.
+
iExists
(
SOMEV
#
m
).
iFrame
.
eauto
.
}
iDestruct
"Hv"
as
(
v
)
"[Hl Hv]"
.
wp_load
.
iAssert
(
one_shot_inv
γ
l
∗
(
⌜
v
=
NONEV
⌝
∨
∃
n
:
Z
,
⌜
v
=
SOMEV
#
n
⌝
∗
own
γ
(
Shot
n
)))%
I
with
"[Hl Hv]"
as
"[Hinv #Hv]"
.
{
iDestruct
"Hv"
as
"[[% ?]|Hv]"
;
last
iDestruct
"Hv"
as
(
m
)
"[% ?]"
;
subst
.
+
iSplit
.
iLeft
;
by
iSplitL
"Hl"
.
eauto
.
+
iSplit
.
iRight
;
iExists
m
;
by
iSplitL
"Hl"
.
eauto
.
}
iSplitL
"Hinv"
;
first
by
eauto
.
iModIntro
.
wp_pures
.
iIntros
"!> !>"
.
wp_lam
.
iDestruct
"Hv"
as
"[%|Hv]"
;
last
iDestruct
"Hv"
as
(
m
)
"[% Hγ']"
;
subst
;
wp_match
;
[
done
|].
wp_bind
(!
_
)%
E
.
iInv
N
as
"[[Hl >Hγ]|H]"
;
last
iDestruct
"H"
as
(
m'
)
"[Hl Hγ]"
.
{
by
iDestruct
(
own_valid_2
with
"Hγ Hγ'"
)
as
%?.
}
wp_load
.
iDestruct
(
own_valid_2
with
"Hγ Hγ'"
)
as
%?%
to_agree_op_inv_L
;
subst
.
iModIntro
.
iSplitL
"Hl"
.
{
iNext
;
iRight
;
by
eauto
.
}
wp_smart_apply
wp_assert
.
wp_pures
.
by
case_bool_decide
.
Qed
.
Lemma
ht_one_shot
(
Φ
:
val
→
iProp
Σ
)
:
⊢
{{
True
}}
one_shot_example
#()
{{
ff
,
(
∀
n
:
Z
,
{{
True
}}
Fst
ff
#
n
{{
w
,
⌜
w
=
#
true
⌝
∨
⌜
w
=
#
false
⌝
}})
∗
{{
True
}}
Snd
ff
#()
{{
g
,
{{
True
}}
g
#()
{{
_
,
True
}}
}}
}}.
Proof
.
iIntros
"!> _"
.
iApply
wp_one_shot
.
iIntros
(
f1
f2
)
"[#Hf1 #Hf2]"
;
iSplit
.
-
iIntros
(
n
)
"!> _"
.
wp_smart_apply
"Hf1"
.
-
iIntros
"!> _"
.
wp_smart_apply
(
wp_wand
with
"Hf2"
).
by
iIntros
(
v
)
"#? !> _"
.
Qed
.
End
proof
.
(* Have a client with a closed proof. *)
Definition
client
:
expr
:
=
let
:
"ff"
:
=
one_shot_example
#()
in
(
Fst
"ff"
#
5
|||
let
:
"check"
:
=
Snd
"ff"
#()
in
"check"
#()).
Section
client
.
Context
`
{!
heapG
Σ
,
!
one_shotG
Σ
,
!
spawnG
Σ
}.
Lemma
client_safe
:
⊢
WP
client
{{
_
,
True
}}.
Proof
using
Type
*.
rewrite
/
client
.
wp_apply
wp_one_shot
.
iIntros
(
f1
f2
)
"[#Hf1 #Hf2]"
.
wp_let
.
wp_smart_apply
wp_par
.
-
wp_smart_apply
"Hf1"
.
-
wp_proj
.
wp_bind
(
f2
_
)%
E
.
iApply
wp_wand
;
first
by
iExact
"Hf2"
.
iIntros
(
check
)
"Hcheck"
.
wp_pures
.
iApply
"Hcheck"
.
-
auto
.
Qed
.
End
client
.
(** Put together all library functors. *)
Definition
client
Σ
:
gFunctors
:
=
#[
heap
Σ
;
one_shot
Σ
;
spawn
Σ
].
(** This lemma implicitly shows that these functors are enough to meet
all library assumptions. *)
Lemma
client_adequate
σ
:
adequate
NotStuck
client
σ
(
λ
_
_
,
True
).
Proof
.
apply
(
heap_adequacy
client
Σ
)=>
?.
iIntros
"_"
.
iApply
client_safe
.
Qed
.
(* Since we check the output of the test files, this means
our test suite will fail if we ever accidentally add an axiom
to anything used by this proof. *)
Print
Assumptions
client_adequate
.
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