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
Rice Wine
Iris
Commits
4b2916c4
Commit
4b2916c4
authored
Dec 06, 2016
by
Ralf Jung
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Add locking to value-scope notation for lambdas
parent
c24ee497
Changes
19
Hide whitespace changes
Inline
Side-by-side
Showing
19 changed files
with
45 additions
and
57 deletions
+45
-57
heap_lang/derived.v
heap_lang/derived.v
+6
-4
heap_lang/lib/assert.v
heap_lang/lib/assert.v
+0
-2
heap_lang/lib/barrier/barrier.v
heap_lang/lib/barrier/barrier.v
+0
-1
heap_lang/lib/barrier/proof.v
heap_lang/lib/barrier/proof.v
+0
-2
heap_lang/lib/counter.v
heap_lang/lib/counter.v
+9
-10
heap_lang/lib/par.v
heap_lang/lib/par.v
+0
-2
heap_lang/lib/spawn.v
heap_lang/lib/spawn.v
+0
-1
heap_lang/lib/spin_lock.v
heap_lang/lib/spin_lock.v
+0
-1
heap_lang/lib/ticket_lock.v
heap_lang/lib/ticket_lock.v
+8
-8
heap_lang/lifting.v
heap_lang/lifting.v
+0
-6
heap_lang/notation.v
heap_lang/notation.v
+5
-5
heap_lang/wp_tactics.v
heap_lang/wp_tactics.v
+17
-2
tests/barrier_client.v
tests/barrier_client.v
+0
-2
tests/counter.v
tests/counter.v
+0
-2
tests/heap_lang.v
tests/heap_lang.v
+0
-1
tests/joining_existentials.v
tests/joining_existentials.v
+0
-2
tests/list_reverse.v
tests/list_reverse.v
+0
-1
tests/one_shot.v
tests/one_shot.v
+0
-2
tests/tree_sum.v
tests/tree_sum.v
+0
-3
No files found.
heap_lang/derived.v
View file @
4b2916c4
...
...
@@ -17,15 +17,17 @@ Implicit Types P Q : iProp Σ.
Implicit
Types
Φ
:
val
→
iProp
Σ
.
(** Proof rules for the sugar *)
Lemma
wp_lam
E
x
ef
e
Φ
:
is_Some
(
to_val
e
)
→
Closed
(
x
:
b
:
[])
ef
→
▷
WP
subst'
x
e
ef
@
E
{{
Φ
}}
⊢
WP
App
(
Lam
x
ef
)
e
@
E
{{
Φ
}}.
Lemma
wp_lam
E
x
elam
e1
e2
Φ
:
e1
=
Lam
x
elam
→
is_Some
(
to_val
e2
)
→
Closed
(
x
:
b
:
[])
elam
→
▷
WP
subst'
x
e2
elam
@
E
{{
Φ
}}
⊢
WP
App
e1
e2
@
E
{{
Φ
}}.
Proof
.
intros
.
by
rewrite
-(
wp_rec
_
BAnon
)
//.
Qed
.
Lemma
wp_let
E
x
e1
e2
Φ
:
is_Some
(
to_val
e1
)
→
Closed
(
x
:
b
:
[])
e2
→
▷
WP
subst'
x
e1
e2
@
E
{{
Φ
}}
⊢
WP
Let
x
e1
e2
@
E
{{
Φ
}}.
Proof
.
apply
wp_lam
.
Qed
.
Proof
.
by
apply
wp_lam
.
Qed
.
Lemma
wp_seq
E
e1
e2
Φ
:
is_Some
(
to_val
e1
)
→
Closed
[]
e2
→
...
...
heap_lang/lib/assert.v
View file @
4b2916c4
...
...
@@ -14,5 +14,3 @@ Proof.
iIntros
"HΦ"
.
rewrite
/
assert
.
wp_let
.
wp_seq
.
iApply
(
wp_wand
with
"HΦ"
).
iIntros
(
v
)
"[% ?]"
;
subst
.
by
wp_if
.
Qed
.
Global
Opaque
assert
.
heap_lang/lib/barrier/barrier.v
View file @
4b2916c4
...
...
@@ -4,4 +4,3 @@ Definition newbarrier : val := λ: <>, ref #false.
Definition
signal
:
val
:
=
λ
:
"x"
,
"x"
<-
#
true
.
Definition
wait
:
val
:
=
rec
:
"wait"
"x"
:
=
if
:
!
"x"
then
#()
else
"wait"
"x"
.
Global
Opaque
newbarrier
signal
wait
.
heap_lang/lib/barrier/proof.v
View file @
4b2916c4
...
...
@@ -22,8 +22,6 @@ Section proof.
Context
`
{!
heapG
Σ
,
!
barrierG
Σ
}
(
N
:
namespace
).
Implicit
Types
I
:
gset
gname
.
Local
Transparent
newbarrier
signal
wait
.
Definition
ress
(
P
:
iProp
Σ
)
(
I
:
gset
gname
)
:
iProp
Σ
:
=
(
∃
Ψ
:
gname
→
iProp
Σ
,
▷
(
P
-
∗
[
∗
set
]
i
∈
I
,
Ψ
i
)
∗
[
∗
set
]
i
∈
I
,
saved_prop_own
i
(
Ψ
i
))%
I
.
...
...
heap_lang/lib/counter.v
View file @
4b2916c4
...
...
@@ -4,12 +4,11 @@ From iris.proofmode Require Import tactics.
From
iris
.
algebra
Require
Import
frac
auth
.
From
iris
.
heap_lang
Require
Import
proofmode
notation
.
Definition
newcounter
:
val
:
=
locked
(
λ
:
<>,
ref
#
0
)%
V
.
Definition
incr
:
val
:
=
locked
(
rec
:
"incr"
"l"
:
=
Definition
newcounter
:
val
:
=
λ
:
<>,
ref
#
0
.
Definition
incr
:
val
:
=
rec
:
"incr"
"l"
:
=
let
:
"n"
:
=
!
"l"
in
if
:
CAS
"l"
"n"
(#
1
+
"n"
)
then
#()
else
"incr"
"l"
)%
V
.
Definition
read
:
val
:
=
locked
(
λ
:
"l"
,
!
"l"
)%
V
.
if
:
CAS
"l"
"n"
(#
1
+
"n"
)
then
#()
else
"incr"
"l"
.
Definition
read
:
val
:
=
λ
:
"l"
,
!
"l"
.
(** Monotone counter *)
Class
mcounterG
Σ
:
=
MCounterG
{
mcounter_inG
:
>
inG
Σ
(
authR
mnatUR
)
}.
...
...
@@ -36,7 +35,7 @@ Section mono_proof.
heapN
⊥
N
→
{{{
heap_ctx
}}}
newcounter
#()
{{{
l
,
RET
#
l
;
mcounter
l
0
}}}.
Proof
.
iIntros
(?
Φ
)
"#Hh HΦ"
.
rewrite
-
wp_fupd
/
newcounter
-
lock
/=
.
wp_seq
.
wp_alloc
l
as
"Hl"
.
iIntros
(?
Φ
)
"#Hh HΦ"
.
rewrite
-
wp_fupd
/
newcounter
.
wp_seq
.
wp_alloc
l
as
"Hl"
.
iMod
(
own_alloc
(
●
(
O
:
mnat
)
⋅
◯
(
O
:
mnat
)))
as
(
γ
)
"[Hγ Hγ']"
;
first
done
.
iMod
(
inv_alloc
N
_
(
mcounter_inv
γ
l
)
with
"[Hl Hγ]"
).
{
iNext
.
iExists
0
%
nat
.
by
iFrame
.
}
...
...
@@ -72,7 +71,7 @@ Section mono_proof.
{{{
mcounter
l
j
}}}
read
#
l
{{{
i
,
RET
#
i
;
⌜
j
≤
i
⌝
%
nat
∧
mcounter
l
i
}}}.
Proof
.
iIntros
(
ϕ
)
"Hc HΦ"
.
iDestruct
"Hc"
as
(
γ
)
"(% & #? & #Hinv & Hγf)"
.
rewrite
/
read
-
lock
/=.
wp_let
.
iInv
N
as
(
c
)
">[Hγ Hl]"
"Hclose"
.
wp_load
.
rewrite
/
read
/=.
wp_let
.
iInv
N
as
(
c
)
">[Hγ Hl]"
"Hclose"
.
wp_load
.
iDestruct
(
own_valid_2
with
"Hγ Hγf"
)
as
%[?%
mnat_included
_
]%
auth_valid_discrete_2
.
iMod
(
own_update_2
with
"Hγ Hγf"
)
as
"[Hγ Hγf]"
.
...
...
@@ -113,7 +112,7 @@ Section contrib_spec.
{{{
heap_ctx
}}}
newcounter
#()
{{{
γ
l
,
RET
#
l
;
ccounter_ctx
γ
l
∗
ccounter
γ
1
0
}}}.
Proof
.
iIntros
(?
Φ
)
"#Hh HΦ"
.
rewrite
-
wp_fupd
/
newcounter
-
lock
/=.
wp_seq
.
wp_alloc
l
as
"Hl"
.
iIntros
(?
Φ
)
"#Hh HΦ"
.
rewrite
-
wp_fupd
/
newcounter
/=.
wp_seq
.
wp_alloc
l
as
"Hl"
.
iMod
(
own_alloc
(
●
(
Some
(
1
%
Qp
,
O
%
nat
))
⋅
◯
(
Some
(
1
%
Qp
,
0
%
nat
))))
as
(
γ
)
"[Hγ Hγ']"
;
first
done
.
iMod
(
inv_alloc
N
_
(
ccounter_inv
γ
l
)
with
"[Hl Hγ]"
).
...
...
@@ -147,7 +146,7 @@ Section contrib_spec.
{{{
c
,
RET
#
c
;
⌜
n
≤
c
⌝
%
nat
∧
ccounter
γ
q
n
}}}.
Proof
.
iIntros
(
Φ
)
"(#(%&?&?) & Hγf) HΦ"
.
rewrite
/
read
-
lock
/=.
wp_let
.
iInv
N
as
(
c
)
">[Hγ Hl]"
"Hclose"
.
wp_load
.
rewrite
/
read
/=.
wp_let
.
iInv
N
as
(
c
)
">[Hγ Hl]"
"Hclose"
.
wp_load
.
iDestruct
(
own_valid_2
with
"Hγ Hγf"
)
as
%[[?
?%
nat_included
]%
Some_pair_included_total_2
_
]%
auth_valid_discrete_2
.
iMod
(
"Hclose"
with
"[Hl Hγ]"
)
as
"_"
;
[
iNext
;
iExists
c
;
by
iFrame
|].
...
...
@@ -159,7 +158,7 @@ Section contrib_spec.
{{{
n
,
RET
#
n
;
ccounter
γ
1
n
}}}.
Proof
.
iIntros
(
Φ
)
"(#(%&?&?) & Hγf) HΦ"
.
rewrite
/
read
-
lock
/=.
wp_let
.
iInv
N
as
(
c
)
">[Hγ Hl]"
"Hclose"
.
wp_load
.
rewrite
/
read
/=.
wp_let
.
iInv
N
as
(
c
)
">[Hγ Hl]"
"Hclose"
.
wp_load
.
iDestruct
(
own_valid_2
with
"Hγ Hγf"
)
as
%[
Hn
_
]%
auth_valid_discrete_2
.
apply
(
Some_included_exclusive
_
)
in
Hn
as
[=
->]%
leibniz_equiv
;
last
done
.
iMod
(
"Hclose"
with
"[Hl Hγ]"
)
as
"_"
;
[
iNext
;
iExists
c
;
by
iFrame
|].
...
...
heap_lang/lib/par.v
View file @
4b2916c4
...
...
@@ -44,5 +44,3 @@ Proof.
iSplitL
"H1"
;
by
wp_let
.
Qed
.
End
proof
.
Global
Opaque
par
.
heap_lang/lib/spawn.v
View file @
4b2916c4
...
...
@@ -78,4 +78,3 @@ Qed.
End
proof
.
Typeclasses
Opaque
join_handle
.
Global
Opaque
spawn
join
.
heap_lang/lib/spin_lock.v
View file @
4b2916c4
...
...
@@ -89,7 +89,6 @@ Section proof.
End
proof
.
Typeclasses
Opaque
is_lock
locked
.
Global
Opaque
newlock
try_acquire
acquire
release
.
Definition
spin_lock
`
{!
heapG
Σ
,
!
lockG
Σ
}
:
lock
Σ
:
=
{|
lock
.
locked_exclusive
:
=
locked_exclusive
;
lock
.
newlock_spec
:
=
newlock_spec
;
...
...
heap_lang/lib/ticket_lock.v
View file @
4b2916c4
...
...
@@ -7,24 +7,24 @@ From iris.heap_lang.lib Require Export lock.
Import
uPred
.
Definition
wait_loop
:
val
:
=
ssreflect
.
locked
(
rec
:
"wait_loop"
"x"
"lk"
:
=
rec
:
"wait_loop"
"x"
"lk"
:
=
let
:
"o"
:
=
!(
Fst
"lk"
)
in
if
:
"x"
=
"o"
then
#()
(* my turn *)
else
"wait_loop"
"x"
"lk"
)%
V
.
else
"wait_loop"
"x"
"lk"
.
Definition
newlock
:
val
:
=
ssreflect
.
locked
(
λ
:
<>,
(
(* owner *)
ref
#
0
,
(* next *)
ref
#
0
)
)%
V
.
λ
:
<>,
(
(* owner *)
ref
#
0
,
(* next *)
ref
#
0
).
Definition
acquire
:
val
:
=
ssreflect
.
locked
(
rec
:
"acquire"
"lk"
:
=
rec
:
"acquire"
"lk"
:
=
let
:
"n"
:
=
!(
Snd
"lk"
)
in
if
:
CAS
(
Snd
"lk"
)
"n"
(
"n"
+
#
1
)
then
wait_loop
"n"
"lk"
else
"acquire"
"lk"
)%
V
.
else
"acquire"
"lk"
.
Definition
release
:
val
:
=
ssreflect
.
locked
(
λ
:
"lk"
,
(
Fst
"lk"
)
<-
!(
Fst
"lk"
)
+
#
1
)%
V
.
λ
:
"lk"
,
(
Fst
"lk"
)
<-
!(
Fst
"lk"
)
+
#
1
.
(** The CMRAs we need. *)
Class
tlockG
Σ
:
=
...
...
@@ -77,7 +77,7 @@ Section proof.
heapN
⊥
N
→
{{{
heap_ctx
∗
R
}}}
newlock
#()
{{{
lk
γ
,
RET
lk
;
is_lock
γ
lk
R
}}}.
Proof
.
iIntros
(
HN
Φ
)
"(#Hh & HR) HΦ"
.
rewrite
-
wp_fupd
/
newlock
.
unlock
.
iIntros
(
HN
Φ
)
"(#Hh & HR) HΦ"
.
rewrite
-
wp_fupd
/
newlock
.
wp_seq
.
wp_alloc
lo
as
"Hlo"
.
wp_alloc
ln
as
"Hln"
.
iMod
(
own_alloc
(
●
(
Excl'
0
%
nat
,
∅
)
⋅
◯
(
Excl'
0
%
nat
,
∅
)))
as
(
γ
)
"[Hγ Hγ']"
.
{
by
rewrite
-
auth_both_op
.
}
...
...
@@ -145,7 +145,7 @@ Section proof.
iIntros
(
Φ
)
"(Hl & Hγ & HR) HΦ"
.
iDestruct
"Hl"
as
(
lo
ln
)
"(% & #? & % & #?)"
;
subst
.
iDestruct
"Hγ"
as
(
o
)
"Hγo"
.
rewrite
/
release
.
unlock
.
wp_let
.
wp_proj
.
wp_proj
.
wp_bind
(!
_
)%
E
.
rewrite
/
release
.
wp_let
.
wp_proj
.
wp_proj
.
wp_bind
(!
_
)%
E
.
iInv
N
as
(
o'
n
)
"(>Hlo & >Hln & >Hauth & Haown)"
"Hclose"
.
wp_load
.
iDestruct
(
own_valid_2
with
"Hauth Hγo"
)
as
...
...
heap_lang/lifting.v
View file @
4b2916c4
...
...
@@ -111,12 +111,6 @@ Proof.
intros
;
inv_head_step
;
eauto
.
Qed
.
Lemma
wp_rec_locked
E
f
x
erec
e1
e2
Φ
`
{!
Closed
(
f
:
b
:
x
:
b
:
[])
erec
}
:
e1
=
of_val
$
locked
(
RecV
f
x
erec
)
→
is_Some
(
to_val
e2
)
→
▷
WP
subst'
x
e2
(
subst'
f
e1
erec
)
@
E
{{
Φ
}}
⊢
WP
App
e1
e2
@
E
{{
Φ
}}.
Proof
.
unlock
.
auto
using
wp_rec
.
Qed
.
Lemma
wp_un_op
E
op
e
v
v'
Φ
:
to_val
e
=
Some
v
→
un_op_eval
op
v
=
Some
v'
→
...
...
heap_lang/notation.v
View file @
4b2916c4
...
...
@@ -47,7 +47,7 @@ Notation "~ e" := (UnOp NegOp e%E) (at level 75, right associativity) : expr_sco
Notation
"e1 <- e2"
:
=
(
Store
e1
%
E
e2
%
E
)
(
at
level
80
)
:
expr_scope
.
Notation
"'rec:' f x := e"
:
=
(
Rec
f
%
bind
x
%
bind
e
%
E
)
(
at
level
102
,
f
at
level
1
,
x
at
level
1
,
e
at
level
200
)
:
expr_scope
.
Notation
"'rec:' f x := e"
:
=
(
RecV
f
%
bind
x
%
bind
e
%
E
)
Notation
"'rec:' f x := e"
:
=
(
locked
(
RecV
f
%
bind
x
%
bind
e
%
E
)
)
(
at
level
102
,
f
at
level
1
,
x
at
level
1
,
e
at
level
200
)
:
val_scope
.
Notation
"'if:' e1 'then' e2 'else' e3"
:
=
(
If
e1
%
E
e2
%
E
e3
%
E
)
(
at
level
200
,
e1
,
e2
,
e3
at
level
200
)
:
expr_scope
.
...
...
@@ -58,20 +58,20 @@ defined above. This is needed because App is now a coercion, and these
notations are otherwise not pretty printed back accordingly. *)
Notation
"'rec:' f x y := e"
:
=
(
Rec
f
%
bind
x
%
bind
(
Lam
y
%
bind
e
%
E
))
(
at
level
102
,
f
,
x
,
y
at
level
1
,
e
at
level
200
)
:
expr_scope
.
Notation
"'rec:' f x y := e"
:
=
(
RecV
f
%
bind
x
%
bind
(
Lam
y
%
bind
e
%
E
))
Notation
"'rec:' f x y := e"
:
=
(
locked
(
RecV
f
%
bind
x
%
bind
(
Lam
y
%
bind
e
%
E
))
)
(
at
level
102
,
f
,
x
,
y
at
level
1
,
e
at
level
200
)
:
val_scope
.
Notation
"'rec:' f x y .. z := e"
:
=
(
Rec
f
%
bind
x
%
bind
(
Lam
y
%
bind
..
(
Lam
z
%
bind
e
%
E
)
..))
(
at
level
102
,
f
,
x
,
y
,
z
at
level
1
,
e
at
level
200
)
:
expr_scope
.
Notation
"'rec:' f x y .. z := e"
:
=
(
RecV
f
%
bind
x
%
bind
(
Lam
y
%
bind
..
(
Lam
z
%
bind
e
%
E
)
..))
Notation
"'rec:' f x y .. z := e"
:
=
(
locked
(
RecV
f
%
bind
x
%
bind
(
Lam
y
%
bind
..
(
Lam
z
%
bind
e
%
E
)
..))
)
(
at
level
102
,
f
,
x
,
y
,
z
at
level
1
,
e
at
level
200
)
:
val_scope
.
Notation
"λ: x , e"
:
=
(
Lam
x
%
bind
e
%
E
)
(
at
level
102
,
x
at
level
1
,
e
at
level
200
)
:
expr_scope
.
Notation
"λ: x y .. z , e"
:
=
(
Lam
x
%
bind
(
Lam
y
%
bind
..
(
Lam
z
%
bind
e
%
E
)
..))
(
at
level
102
,
x
,
y
,
z
at
level
1
,
e
at
level
200
)
:
expr_scope
.
Notation
"λ: x , e"
:
=
(
LamV
x
%
bind
e
%
E
)
Notation
"λ: x , e"
:
=
(
locked
(
LamV
x
%
bind
e
%
E
)
)
(
at
level
102
,
x
at
level
1
,
e
at
level
200
)
:
val_scope
.
Notation
"λ: x y .. z , e"
:
=
(
LamV
x
%
bind
(
Lam
y
%
bind
..
(
Lam
z
%
bind
e
%
E
)
..
))
Notation
"λ: x y .. z , e"
:
=
(
locked
(
LamV
x
%
bind
(
Lam
y
%
bind
..
(
Lam
z
%
bind
e
%
E
)
..
))
)
(
at
level
102
,
x
,
y
,
z
at
level
1
,
e
at
level
200
)
:
val_scope
.
Notation
"'let:' x := e1 'in' e2"
:
=
(
Lam
x
%
bind
e2
%
E
e1
%
E
)
...
...
heap_lang/wp_tactics.v
View file @
4b2916c4
...
...
@@ -44,13 +44,28 @@ Tactic Notation "wp_value" :=
|
_
=>
fail
"wp_value: not a wp"
end
.
(* Applied to goals that are equalities of expressions. Will try to unlock the
LHS once if necessary, to get rid of the lock added by the syntactic sugar. *)
Ltac
wp_unlock
:
=
solve
[
reflexivity
|
(* If there are no locks, this is enough. *)
(* Otherwise, use unification to uncover the lock. *)
(* Step 1: Get the LHS into the form "of_val (locked v)" *)
let
v
:
=
fresh
"v"
in
evar
(
v
:
val
)
;
trans
(
of_val
(
locked
v
))
;
subst
v
;
first
reflexivity
;
(* Step 2: Remove the lock from the LHS. *)
etrans
;
first
solve
[
apply
(
f_equal
of_val
)
;
symmetry
;
apply
lock
]
;
(* Now things should be convertible. *)
reflexivity
].
Tactic
Notation
"wp_rec"
:
=
lazymatch
goal
with
|
|-
_
⊢
wp
?E
?e
?Q
=>
reshape_expr
e
ltac
:
(
fun
K
e'
=>
match
eval
hnf
in
e'
with
App
?e1
_
=>
(* hnf does not reduce through an of_val *)
(* match eval hnf in e1 with Rec _ _ _ => *)
wp_bind_core
K
;
etrans
;
[|
(
eapply
wp_rec
;
wp_
done
)
||
(
eapply
wp_rec_locked
;
wp_done
)
]
;
simpl_subst
;
wp_finish
wp_bind_core
K
;
etrans
;
[|
eapply
wp_rec
;
[
wp_
unlock
|
wp_done
..]
]
;
simpl_subst
;
wp_finish
(* end *)
end
)
||
fail
"wp_rec: cannot find 'Rec' in"
e
|
_
=>
fail
"wp_rec: not a 'wp'"
end
.
...
...
@@ -60,7 +75,7 @@ Tactic Notation "wp_lam" :=
|
|-
_
⊢
wp
?E
?e
?Q
=>
reshape_expr
e
ltac
:
(
fun
K
e'
=>
match
eval
hnf
in
e'
with
App
?e1
_
=>
(* match eval hnf in e1 with Rec BAnon _ _ => *)
wp_bind_core
K
;
etrans
;
[|
eapply
wp_lam
;
wp_done
]
;
simpl_subst
;
wp_finish
wp_bind_core
K
;
etrans
;
[|
eapply
wp_lam
;
[
wp_unlock
|
wp_done
..]
]
;
simpl_subst
;
wp_finish
(* end *)
end
)
||
fail
"wp_lam: cannot find 'Lam' in"
e
|
_
=>
fail
"wp_lam: not a 'wp'"
end
.
...
...
tests/barrier_client.v
View file @
4b2916c4
...
...
@@ -54,8 +54,6 @@ Section client.
Qed
.
End
client
.
Global
Opaque
worker
client
.
Section
ClosedProofs
.
Let
Σ
:
gFunctors
:
=
#[
heap
Σ
;
barrier
Σ
;
spawn
Σ
].
...
...
tests/counter.v
View file @
4b2916c4
...
...
@@ -136,5 +136,3 @@ Proof.
iModIntro
;
rewrite
/
C
;
eauto
10
with
omega
.
Qed
.
End
proof
.
Global
Opaque
newcounter
incr
read
.
tests/heap_lang.v
View file @
4b2916c4
...
...
@@ -37,7 +37,6 @@ Section LiftingTests.
Definition
Pred
:
val
:
=
λ
:
"x"
,
if
:
"x"
≤
#
0
then
-
FindPred
(-
"x"
+
#
2
)
#
0
else
FindPred
"x"
#
0
.
Global
Opaque
FindPred
Pred
.
Lemma
FindPred_spec
n1
n2
E
Φ
:
n1
<
n2
→
...
...
tests/joining_existentials.v
View file @
4b2916c4
...
...
@@ -97,5 +97,3 @@ Proof.
-
iIntros
(
_
v
)
"[_ H]"
.
iDestruct
(
Q_res_join
with
"H"
)
as
"?"
.
auto
.
Qed
.
End
proof
.
Global
Opaque
client
.
tests/list_reverse.v
View file @
4b2916c4
...
...
@@ -24,7 +24,6 @@ Definition rev : val :=
"l"
<-
(
"tmp1"
,
"acc"
)
;;
"rev"
"tmp2"
"hd"
end
.
Global
Opaque
rev
.
Lemma
rev_acc_wp
hd
acc
xs
ys
(
Φ
:
val
→
iProp
Σ
)
:
heap_ctx
∗
is_list
hd
xs
∗
is_list
acc
ys
∗
...
...
tests/one_shot.v
View file @
4b2916c4
...
...
@@ -96,5 +96,3 @@ Proof.
iApply
(
wp_wand
with
"Hf2"
).
by
iIntros
(
v
)
"#? !# _"
.
Qed
.
End
proof
.
Global
Opaque
one_shot_example
.
tests/tree_sum.v
View file @
4b2916c4
...
...
@@ -64,6 +64,3 @@ Proof.
rewrite
Z
.
add_0_r
.
iIntros
"Hl Ht"
.
wp_seq
.
wp_load
.
by
iApply
"HΦ"
.
Qed
.
Global
Opaque
sum_loop
sum'
.
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