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
6e1d449c
Commit
6e1d449c
authored
Nov 01, 2018
by
Robbert Krebbers
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Bump Iris.
parent
c18dc76f
Changes
5
Hide whitespace changes
Inline
Side-by-side
Showing
5 changed files
with
18 additions
and
17 deletions
+18
-17
opam
opam
+1
-1
theories/logrel/F_mu/soundness.v
theories/logrel/F_mu/soundness.v
+1
-1
theories/logrel/F_mu_ref/rules.v
theories/logrel/F_mu_ref/rules.v
+5
-4
theories/logrel/F_mu_ref_conc/rules.v
theories/logrel/F_mu_ref_conc/rules.v
+10
-10
theories/logrel/stlc/soundness.v
theories/logrel/stlc/soundness.v
+1
-1
No files found.
opam
View file @
6e1d449c
...
...
@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris_examples"]
depends: [
"coq-iris" { (= "dev.2018-10-31.
0.6356ef0
3") | (= "dev") }
"coq-iris" { (= "dev.2018-10-31.
4.4a1eb8a
3") | (= "dev") }
"coq-autosubst" { = "dev.coq86" }
]
theories/logrel/F_mu/soundness.v
View file @
6e1d449c
...
...
@@ -11,7 +11,7 @@ Proof.
eapply
(
wp_adequacy
Σ
)
;
eauto
.
iIntros
(
Hinv
?).
iModIntro
.
iExists
(
λ
_
_
,
True
%
I
).
iSplit
=>
//.
rewrite
-(
empty_env_subst
e
).
set
(
H
Σ
:
=
IrisG
_
_
_
Hinv
(
λ
_
_
,
True
)%
I
).
set
(
H
Σ
:
=
IrisG
_
_
Hinv
(
λ
_
_
_
,
True
)%
I
(
λ
_
,
True
)%
I
).
iApply
(
wp_wand
with
"[]"
).
iApply
Hlog
;
eauto
.
by
iApply
interp_env_nil
.
auto
.
Qed
.
...
...
theories/logrel/F_mu_ref/rules.v
View file @
6e1d449c
...
...
@@ -14,7 +14,8 @@ Class heapG Σ := HeapG {
Instance
heapG_irisG
`
{
heapG
Σ
}
:
irisG
F_mu_ref_lang
Σ
:
=
{
iris_invG
:
=
heapG_invG
;
state_interp
σ
κ
s
:
=
gen_heap_ctx
σ
state_interp
σ
κ
s
_
:
=
gen_heap_ctx
σ
;
fork_post
_
:
=
True
%
I
;
}.
Global
Opaque
iris_invG
.
...
...
@@ -62,7 +63,7 @@ Section lang_rules.
Proof
.
iIntros
(<-
Φ
)
"_ HΦ"
.
iApply
wp_lift_atomic_head_step_no_fork
;
auto
.
iIntros
(
σ
1
??)
"Hσ !>"
;
iSplit
;
first
by
auto
.
iIntros
(
σ
1
??
?
)
"Hσ !>"
;
iSplit
;
first
by
auto
.
iNext
;
iIntros
(
v2
σ
2
efs
Hstep
)
;
inv_head_step
.
iMod
(@
gen_heap_alloc
with
"Hσ"
)
as
"[Hσ Hl]"
;
first
done
.
iModIntro
;
iSplit
=>
//.
iFrame
.
by
iApply
"HΦ"
.
...
...
@@ -72,7 +73,7 @@ Section lang_rules.
{{{
▷
l
↦
{
q
}
v
}}}
Load
(
Loc
l
)
@
E
{{{
RET
v
;
l
↦
{
q
}
v
}}}.
Proof
.
iIntros
(
Φ
)
">Hl HΦ"
.
iApply
wp_lift_atomic_head_step_no_fork
;
auto
.
iIntros
(
σ
1
??)
"Hσ !>"
.
iDestruct
(@
gen_heap_valid
with
"Hσ Hl"
)
as
%?.
iIntros
(
σ
1
??
?
)
"Hσ !>"
.
iDestruct
(@
gen_heap_valid
with
"Hσ Hl"
)
as
%?.
iSplit
;
first
by
eauto
.
iNext
;
iIntros
(
v2
σ
2
efs
Hstep
)
;
inv_head_step
.
iModIntro
;
iSplit
=>
//.
iFrame
.
by
iApply
"HΦ"
.
...
...
@@ -85,7 +86,7 @@ Section lang_rules.
Proof
.
iIntros
(<-%
of_to_val
Φ
)
">Hl HΦ"
.
iApply
wp_lift_atomic_head_step_no_fork
;
auto
.
iIntros
(
σ
1
??)
"Hσ !>"
.
iDestruct
(@
gen_heap_valid
with
"Hσ Hl"
)
as
%?.
iIntros
(
σ
1
??
?
)
"Hσ !>"
.
iDestruct
(@
gen_heap_valid
with
"Hσ Hl"
)
as
%?.
iSplit
;
first
by
eauto
.
iNext
;
iIntros
(
v2
σ
2
efs
Hstep
)
;
inv_head_step
.
iMod
(@
gen_heap_update
with
"Hσ Hl"
)
as
"[$ Hl]"
.
iModIntro
.
iSplit
=>//.
by
iApply
"HΦ"
.
...
...
theories/logrel/F_mu_ref_conc/rules.v
View file @
6e1d449c
...
...
@@ -16,7 +16,8 @@ Class heapIG Σ := HeapIG {
Instance
heapIG_irisG
`
{
heapIG
Σ
}
:
irisG
F_mu_ref_conc_lang
Σ
:
=
{
iris_invG
:
=
heapI_invG
;
state_interp
σ
κ
s
:
=
gen_heap_ctx
σ
state_interp
σ
κ
s
_
:
=
gen_heap_ctx
σ
;
fork_post
_
:
=
True
%
I
;
}.
Global
Opaque
iris_invG
.
...
...
@@ -57,7 +58,7 @@ Section lang_rules.
{{{
True
}}}
Alloc
e
@
E
{{{
l
,
RET
(
LocV
l
)
;
l
↦ᵢ
v
}}}.
Proof
.
iIntros
(<-
Φ
)
"_ HΦ"
.
iApply
wp_lift_atomic_head_step_no_fork
;
auto
.
iIntros
(
σ
1
??)
"Hσ !>"
;
iSplit
;
first
by
auto
.
iIntros
(
σ
1
??
?
)
"Hσ !>"
;
iSplit
;
first
by
auto
.
iNext
;
iIntros
(
v2
σ
2
efs
Hstep
)
;
inv_head_step
.
iMod
(@
gen_heap_alloc
with
"Hσ"
)
as
"[Hσ Hl]"
;
first
done
.
iModIntro
;
iSplit
=>
//.
iFrame
.
by
iApply
"HΦ"
.
...
...
@@ -67,7 +68,7 @@ Section lang_rules.
{{{
▷
l
↦ᵢ
{
q
}
v
}}}
Load
(
Loc
l
)
@
E
{{{
RET
v
;
l
↦ᵢ
{
q
}
v
}}}.
Proof
.
iIntros
(
Φ
)
">Hl HΦ"
.
iApply
wp_lift_atomic_head_step_no_fork
;
auto
.
iIntros
(
σ
1
??)
"Hσ !>"
.
iDestruct
(@
gen_heap_valid
with
"Hσ Hl"
)
as
%?.
iIntros
(
σ
1
??
?
)
"Hσ !>"
.
iDestruct
(@
gen_heap_valid
with
"Hσ Hl"
)
as
%?.
iSplit
;
first
by
eauto
.
iNext
;
iIntros
(
v2
σ
2
efs
Hstep
)
;
inv_head_step
.
iModIntro
;
iSplit
=>
//.
iFrame
.
by
iApply
"HΦ"
.
...
...
@@ -80,7 +81,7 @@ Section lang_rules.
Proof
.
iIntros
(<-
Φ
)
">Hl HΦ"
.
iApply
wp_lift_atomic_head_step_no_fork
;
auto
.
iIntros
(
σ
1
??)
"Hσ !>"
.
iDestruct
(@
gen_heap_valid
with
"Hσ Hl"
)
as
%?.
iIntros
(
σ
1
??
?
)
"Hσ !>"
.
iDestruct
(@
gen_heap_valid
with
"Hσ Hl"
)
as
%?.
iSplit
;
first
by
eauto
.
iNext
;
iIntros
(
v2
σ
2
efs
Hstep
)
;
inv_head_step
.
iMod
(@
gen_heap_update
with
"Hσ Hl"
)
as
"[$ Hl]"
.
iModIntro
.
iSplit
=>//.
by
iApply
"HΦ"
.
...
...
@@ -93,7 +94,7 @@ Section lang_rules.
Proof
.
iIntros
(<-
<-
?
Φ
)
">Hl HΦ"
.
iApply
wp_lift_atomic_head_step_no_fork
;
auto
.
iIntros
(
σ
1
??)
"Hσ !>"
.
iDestruct
(@
gen_heap_valid
with
"Hσ Hl"
)
as
%?.
iIntros
(
σ
1
??
?
)
"Hσ !>"
.
iDestruct
(@
gen_heap_valid
with
"Hσ Hl"
)
as
%?.
iSplit
;
first
by
eauto
.
iNext
;
iIntros
(
v2'
σ
2
efs
Hstep
)
;
inv_head_step
.
iModIntro
;
iSplit
=>
//.
iFrame
.
by
iApply
"HΦ"
.
...
...
@@ -106,7 +107,7 @@ Section lang_rules.
Proof
.
iIntros
(<-
<-
Φ
)
">Hl HΦ"
.
iApply
wp_lift_atomic_head_step_no_fork
;
auto
.
iIntros
(
σ
1
??)
"Hσ !>"
.
iDestruct
(@
gen_heap_valid
with
"Hσ Hl"
)
as
%?.
iIntros
(
σ
1
??
?
)
"Hσ !>"
.
iDestruct
(@
gen_heap_valid
with
"Hσ Hl"
)
as
%?.
iSplit
;
first
by
eauto
.
iNext
;
iIntros
(
v2'
σ
2
efs
Hstep
)
;
inv_head_step
.
iMod
(@
gen_heap_update
with
"Hσ Hl"
)
as
"[$ Hl]"
.
iModIntro
.
iSplit
=>//.
by
iApply
"HΦ"
.
...
...
@@ -115,10 +116,9 @@ Section lang_rules.
Lemma
wp_fork
E
e
Φ
:
▷
(|={
E
}=>
Φ
UnitV
)
∗
▷
WP
e
{{
_
,
True
}}
⊢
WP
Fork
e
@
E
{{
Φ
}}.
Proof
.
rewrite
-(
wp_lift_pure_det_head_step
(
Fork
e
)
Unit
[
e
])
//=
;
eauto
.
-
iIntros
"[H1 H2]"
;
iModIntro
;
iNext
;
iModIntro
;
iFrame
.
by
iApply
wp_value_fupd
.
-
intros
;
inv_head_step
;
eauto
.
iIntros
"[He HΦ]"
.
iApply
wp_lift_atomic_head_step
;
[
done
|].
iIntros
(
σ
1
κ
κ
s
n
)
"Hσ !>"
;
iSplit
;
first
by
eauto
.
iNext
;
iIntros
(
v2
σ
2
efs
Hstep
)
;
inv_head_step
.
by
iFrame
.
Qed
.
Local
Ltac
solve_exec_safe
:
=
intros
;
subst
;
do
3
eexists
;
econstructor
;
eauto
.
...
...
theories/logrel/stlc/soundness.v
View file @
6e1d449c
...
...
@@ -16,7 +16,7 @@ Proof.
cut
(
adequate
NotStuck
e
()
(
λ
_
_
,
True
))
;
first
(
intros
[
_
Hsafe
]
;
eauto
).
eapply
(
wp_adequacy
Σ
_
).
iIntros
(
Hinv
?).
iModIntro
.
iExists
(
λ
_
_
,
True
%
I
).
iSplit
=>//.
set
(
H
Σ
:
=
IrisG
_
_
_
Hinv
(
λ
_
_
,
True
)%
I
).
set
(
H
Σ
:
=
IrisG
_
_
Hinv
(
λ
_
_
_
,
True
)%
I
(
λ
_
,
True
)%
I
).
iApply
(
wp_wand
with
"[]"
).
by
iApply
wp_soundness
.
eauto
.
Qed
.
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