Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
10
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Open sidebar
Paolo G. Giarrusso
examples
Commits
e70f486e
Verified
Commit
e70f486e
authored
Mar 27, 2019
by
Rodolphe Lepigre
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Fix atomic snapshot example
parent
9fbc1013
Changes
2
Hide whitespace changes
Inline
Side-by-side
Showing
2 changed files
with
7 additions
and
7 deletions
+7
-7
opam
opam
+1
-1
theories/logatom/snapshot/atomic_snapshot.v
theories/logatom/snapshot/atomic_snapshot.v
+6
-6
No files found.
opam
View file @
e70f486e
...
...
@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris_examples"]
depends: [
"coq-iris" { (= "dev.2019-03-
14.3.2d1c8352
") | (= "dev") }
"coq-iris" { (= "dev.2019-03-
26.0.0495f119
") | (= "dev") }
"coq-autosubst" { = "dev.coq86" }
]
theories/logatom/snapshot/atomic_snapshot.v
View file @
e70f486e
...
...
@@ -365,10 +365,10 @@ Section atomic_snapshot.
wp_load
.
eauto
.
Qed
.
Definition
val_to_bool
(
v
:
option
val
)
:
bool
:
=
Definition
val_
list_
to_bool
(
v
:
list
val
)
:
bool
:
=
match
v
with
|
Some
(
LitV
(
LitBool
b
)
)
=>
b
|
_
=>
false
|
LitV
(
LitBool
b
)
::
_
=>
b
|
_
=>
false
end
.
Lemma
readPair_spec
γ
p
:
...
...
@@ -413,7 +413,7 @@ Section atomic_snapshot.
iMod
"AU"
as
(
xv
yv
)
"[Hpair Hclose]"
.
rewrite
/
pair_content
.
iDestruct
(
excl_sync
with
"Hp⚫ Hpair"
)
as
%[=
->
->].
destruct
(
val_to_bool
proph_val
)
eqn
:
Hproph
.
destruct
(
val_
list_
to_bool
proph_val
)
eqn
:
Hproph
.
-
(* prophecy value is predicting that timestamp has not changed, so we commit *)
(* committing AU *)
iMod
(
"Hclose"
with
"Hpair"
)
as
"HΦ"
.
...
...
@@ -443,7 +443,7 @@ Section atomic_snapshot.
}
wp_load
.
wp_let
.
wp_proj
.
wp_let
.
wp_proj
.
wp_op
.
case_bool_decide
;
wp_let
;
wp_apply
(
wp_resolve_proph
with
"Hpr"
)
;
iIntros
(->
)
;
wp_seq
;
wp_if
.
iIntros
(
vs'
)
"[Eq _]"
;
iDestruct
"Eq"
as
%
->
;
wp_seq
;
wp_if
.
+
inversion
H
;
subst
;
clear
H
.
wp_pures
.
assert
(
v_x2
=
v_y
)
as
->.
{
assert
(
v_x2
<=
v_y
)
as
vneq
.
{
...
...
@@ -479,7 +479,7 @@ Section atomic_snapshot.
}
wp_load
.
repeat
(
wp_let
;
wp_proj
).
wp_op
.
wp_let
.
wp_apply
(
wp_resolve_proph
with
"Hpr"
).
iIntros
(
Heq
).
subst
.
iIntros
(
vs'
)
"[Heq _]"
;
iDestruct
"Heq"
as
%->
.
case_bool_decide
.
+
inversion
H
;
subst
;
clear
H
.
inversion
Hproph
.
+
wp_seq
.
wp_if
.
iApply
"IH"
;
rewrite
/
is_pair
;
eauto
.
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a 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