Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Rice Wine
Iris
Commits
eacb1c46
Commit
eacb1c46
authored
May 24, 2016
by
Robbert Krebbers
Browse files
Flip order of arguments of iAssert/iPvsAssert.
parent
65bfa071
Changes
5
Hide whitespace changes
Inline
Sidebyside
heap_lang/lib/barrier/proof.v
View file @
eacb1c46
...
@@ 110,7 +110,7 @@ Proof.
...
@@ 110,7 +110,7 @@ Proof.
iAssert
(
barrier_ctx
γ
'
l
P
)%
I
as
"#?"
.
iAssert
(
barrier_ctx
γ
'
l
P
)%
I
as
"#?"
.
{
rewrite
/
barrier_ctx
.
by
repeat
iSplit
.
}
{
rewrite
/
barrier_ctx
.
by
repeat
iSplit
.
}
iPvsAssert
(
sts_ownS
γ
'
(
i_states
γ
)
{[
Change
γ
]}
iPvsAssert
(
sts_ownS
γ
'
(
i_states
γ
)
{[
Change
γ
]}
★
sts_ownS
γ
'
low_states
{[
Send
]})%
I
as
"[Hr Hs]"
with
"[
]"
.
★
sts_ownS
γ
'
low_states
{[
Send
]})%
I
with
"[]"
as
"[Hr Hs
]"
.
{
iApply
sts_ownS_op
;
eauto
using
i_states_closed
,
low_states_closed
.
{
iApply
sts_ownS_op
;
eauto
using
i_states_closed
,
low_states_closed
.
+
set_solver
.
+
set_solver
.
+
iApply
(
sts_own_weaken
with
"Hγ'"
)
;
+
iApply
(
sts_own_weaken
with
"Hγ'"
)
;
...
@@ 148,7 +148,7 @@ Proof.
...
@@ 148,7 +148,7 @@ Proof.
iExists
(
State
Low
I
),
{[
Change
i
]}
;
iSplit
;
[
done

iSplitL
"Hl Hr"
].
iExists
(
State
Low
I
),
{[
Change
i
]}
;
iSplit
;
[
done

iSplitL
"Hl Hr"
].
{
iNext
.
rewrite
{
2
}/
barrier_inv
/=.
by
iFrame
"Hl"
.
}
{
iNext
.
rewrite
{
2
}/
barrier_inv
/=.
by
iFrame
"Hl"
.
}
iIntros
"Hγ"
.
iIntros
"Hγ"
.
iPvsAssert
(
sts_ownS
γ
(
i_states
i
)
{[
Change
i
]})%
I
as
"Hγ"
with
"[Hγ]"
.
iPvsAssert
(
sts_ownS
γ
(
i_states
i
)
{[
Change
i
]})%
I
with
"[Hγ]"
as
"Hγ"
.
{
iApply
(
sts_own_weaken
with
"Hγ"
)
;
eauto
using
i_states_closed
.
}
{
iApply
(
sts_own_weaken
with
"Hγ"
)
;
eauto
using
i_states_closed
.
}
wp_op
=>
?
;
simplify_eq
;
wp_if
.
iApply
(
"IH"
with
"Hγ [HQR] HΦ"
).
by
iNext
.
wp_op
=>
?
;
simplify_eq
;
wp_if
.
iApply
(
"IH"
with
"Hγ [HQR] HΦ"
).
by
iNext
.

(* a High state: the comparison succeeds, and we perform a transition and

(* a High state: the comparison succeeds, and we perform a transition and
...
@@ 157,7 +157,7 @@ Proof.
...
@@ 157,7 +157,7 @@ Proof.
iSplit
;
[
iPureIntro
;
by
eauto
using
wait_step
].
iSplit
;
[
iPureIntro
;
by
eauto
using
wait_step
].
iDestruct
"Hr"
as
{
Ψ
}
"[HΨ Hsp]"
.
iDestruct
"Hr"
as
{
Ψ
}
"[HΨ Hsp]"
.
iDestruct
(
big_sepS_delete
_
_
i
with
"Hsp"
)
as
"[#HΨi Hsp]"
;
first
done
.
iDestruct
(
big_sepS_delete
_
_
i
with
"Hsp"
)
as
"[#HΨi Hsp]"
;
first
done
.
iAssert
(
▷
Ψ
i
★
▷
Π★
{
set
(
I
∖
{[
i
]})}
Ψ
)%
I
as
"[HΨ
HΨ']"
with
"[HΨ]"
.
iAssert
(
▷
Ψ
i
★
▷
Π★
{
set
(
I
∖
{[
i
]})}
Ψ
)%
I
with
"[HΨ
]"
as
"[HΨ
HΨ'
]"
.
{
iNext
.
iApply
(
big_sepS_delete
_
_
i
)
;
first
done
.
by
iApply
"HΨ"
.
}
{
iNext
.
iApply
(
big_sepS_delete
_
_
i
)
;
first
done
.
by
iApply
"HΨ"
.
}
iSplitL
"HΨ' Hl Hsp"
;
[
iNext
].
iSplitL
"HΨ' Hl Hsp"
;
[
iNext
].
+
rewrite
{
2
}/
barrier_inv
/=
;
iFrame
"Hl"
.
+
rewrite
{
2
}/
barrier_inv
/=
;
iFrame
"Hl"
.
...
@@ 185,7 +185,7 @@ Proof.
...
@@ 185,7 +185,7 @@ Proof.
iApply
(
ress_split
_
_
_
Q
R1
R2
)
;
eauto
.
iFrame
"Hr HQR"
.
by
repeat
iSplit
.
iApply
(
ress_split
_
_
_
Q
R1
R2
)
;
eauto
.
iFrame
"Hr HQR"
.
by
repeat
iSplit
.

iIntros
"Hγ"
.

iIntros
"Hγ"
.
iPvsAssert
(
sts_ownS
γ
(
i_states
i1
)
{[
Change
i1
]}
iPvsAssert
(
sts_ownS
γ
(
i_states
i1
)
{[
Change
i1
]}
★
sts_ownS
γ
(
i_states
i2
)
{[
Change
i2
]})%
I
as
"[Hγ1 Hγ2]"
with
"[]"
.
★
sts_ownS
γ
(
i_states
i2
)
{[
Change
i2
]})%
I
with
"[]"
as
"[Hγ1 Hγ2]"
.
{
iApply
sts_ownS_op
;
eauto
using
i_states_closed
,
low_states_closed
.
{
iApply
sts_ownS_op
;
eauto
using
i_states_closed
,
low_states_closed
.
+
set_solver
.
+
set_solver
.
+
iApply
(
sts_own_weaken
with
"Hγ"
)
;
+
iApply
(
sts_own_weaken
with
"Hγ"
)
;
...
...
proofmode/pviewshifts.v
View file @
eacb1c46
...
@@ 186,7 +186,7 @@ Tactic Notation "iTimeless" constr(H) :=
...
@@ 186,7 +186,7 @@ Tactic Notation "iTimeless" constr(H) :=
Tactic
Notation
"iTimeless"
constr
(
H
)
"as"
constr
(
Hs
)
:
=
Tactic
Notation
"iTimeless"
constr
(
H
)
"as"
constr
(
Hs
)
:
=
iTimeless
H
;
iDestruct
H
as
Hs
.
iTimeless
H
;
iDestruct
H
as
Hs
.
Tactic
Notation
"iPvsAssert"
constr
(
Q
)
"
as
"
constr
(
pat
)
"with
"
constr
(
Hs
)
:
=
Tactic
Notation
"iPvsAssert"
constr
(
Q
)
"
with
"
constr
(
Hs
)
"as
"
constr
(
pat
)
:
=
let
H
:
=
iFresh
in
let
H
:
=
iFresh
in
let
Hs
:
=
spec_pat
.
parse_one
Hs
in
let
Hs
:
=
spec_pat
.
parse_one
Hs
in
lazymatch
Hs
with
lazymatch
Hs
with
...
@@ 200,4 +200,4 @@ Tactic Notation "iPvsAssert" constr(Q) "as" constr(pat) "with" constr(Hs) :=
...
@@ 200,4 +200,4 @@ Tactic Notation "iPvsAssert" constr(Q) "as" constr(pat) "with" constr(Hs) :=

?pat
=>
fail
"iPvsAssert: invalid pattern"
pat

?pat
=>
fail
"iPvsAssert: invalid pattern"
pat
end
.
end
.
Tactic
Notation
"iPvsAssert"
constr
(
Q
)
"as"
constr
(
pat
)
:
=
Tactic
Notation
"iPvsAssert"
constr
(
Q
)
"as"
constr
(
pat
)
:
=
iPvsAssert
Q
as
pat
with
"[]"
.
iPvsAssert
Q
with
"[]"
as
pat
.
proofmode/tactics.v
View file @
eacb1c46
...
@@ 699,7 +699,7 @@ Tactic Notation "iLöb" "{" ident(x1) ident(x2) ident(x3) ident(x4)
...
@@ 699,7 +699,7 @@ Tactic Notation "iLöb" "{" ident(x1) ident(x2) ident(x3) ident(x4)
ltac
:
(
iIntros
{
x1
x2
x3
x4
x5
x6
x7
x8
}).
ltac
:
(
iIntros
{
x1
x2
x3
x4
x5
x6
x7
x8
}).
(** * Assert *)
(** * Assert *)
Tactic
Notation
"iAssert"
constr
(
Q
)
"
as
"
constr
(
pat
)
"with
"
constr
(
Hs
)
:
=
Tactic
Notation
"iAssert"
constr
(
Q
)
"
with
"
constr
(
Hs
)
"as
"
constr
(
pat
)
:
=
let
H
:
=
iFresh
in
let
H
:
=
iFresh
in
let
Hs
:
=
spec_pat
.
parse
Hs
in
let
Hs
:
=
spec_pat
.
parse
Hs
in
lazymatch
Hs
with
lazymatch
Hs
with
...
@@ 716,7 +716,7 @@ Tactic Notation "iAssert" constr(Q) "as" constr(pat) "with" constr(Hs) :=
...
@@ 716,7 +716,7 @@ Tactic Notation "iAssert" constr(Q) "as" constr(pat) "with" constr(Hs) :=

?pat
=>
fail
"iAssert: invalid pattern"
pat

?pat
=>
fail
"iAssert: invalid pattern"
pat
end
.
end
.
Tactic
Notation
"iAssert"
constr
(
Q
)
"as"
constr
(
pat
)
:
=
Tactic
Notation
"iAssert"
constr
(
Q
)
"as"
constr
(
pat
)
:
=
iAssert
Q
as
pat
with
"[]"
.
iAssert
Q
with
"[]"
as
pat
.
(** * Rewrite *)
(** * Rewrite *)
Local
Ltac
iRewriteFindPred
:
=
Local
Ltac
iRewriteFindPred
:
=
...
...
tests/one_shot.v
View file @
eacb1c46
...
@@ 58,13 +58,13 @@ Proof.
...
@@ 58,13 +58,13 @@ Proof.
+
wp_cas_fail
.
iSplitL
.
iRight
;
iExists
m
;
by
iSplitL
"Hl"
.
by
iRight
.
+
wp_cas_fail
.
iSplitL
.
iRight
;
iExists
m
;
by
iSplitL
"Hl"
.
by
iRight
.

iIntros
"!"
.
wp_seq
.
wp_focus
(!
_
)%
E
.
iInv
>
N
as
"Hγ"
.

iIntros
"!"
.
wp_seq
.
wp_focus
(!
_
)%
E
.
iInv
>
N
as
"Hγ"
.
iAssert
(
∃
v
,
l
↦
v
★
((
v
=
InjLV
#
0
★
own
γ
OneShotPending
)
∨
iAssert
(
∃
v
,
l
↦
v
★
((
v
=
InjLV
#
0
★
own
γ
OneShotPending
)
∨
∃
n
:
Z
,
v
=
InjRV
#
n
★
own
γ
(
Shot
(
DecAgree
n
))))%
I
as
"Hv"
with
"[]"
.
∃
n
:
Z
,
v
=
InjRV
#
n
★
own
γ
(
Shot
(
DecAgree
n
))))%
I
with
"[]"
as
"Hv"
.
{
iDestruct
"Hγ"
as
"[[Hl Hγ]Hl]"
;
last
iDestruct
"Hl"
as
{
m
}
"[Hl Hγ]"
.
{
iDestruct
"Hγ"
as
"[[Hl Hγ]Hl]"
;
last
iDestruct
"Hl"
as
{
m
}
"[Hl Hγ]"
.
+
iExists
(
InjLV
#
0
).
iFrame
"Hl"
.
iLeft
;
by
iSplit
.
+
iExists
(
InjLV
#
0
).
iFrame
"Hl"
.
iLeft
;
by
iSplit
.
+
iExists
(
InjRV
#
m
).
iFrame
"Hl"
.
iRight
;
iExists
m
;
by
iSplit
.
}
+
iExists
(
InjRV
#
m
).
iFrame
"Hl"
.
iRight
;
iExists
m
;
by
iSplit
.
}
iDestruct
"Hv"
as
{
v
}
"[Hl Hv]"
.
wp_load
.
iDestruct
"Hv"
as
{
v
}
"[Hl Hv]"
.
wp_load
.
iAssert
(
one_shot_inv
γ
l
★
(
v
=
InjLV
#
0
∨
∃
n
:
Z
,
iAssert
(
one_shot_inv
γ
l
★
(
v
=
InjLV
#
0
∨
∃
n
:
Z
,
v
=
InjRV
#
n
★
own
γ
(
Shot
(
DecAgree
n
))))%
I
as
"[$ #Hv]"
with
"[
]"
.
v
=
InjRV
#
n
★
own
γ
(
Shot
(
DecAgree
n
))))%
I
with
"[]"
as
"[$ #Hv
]"
.
{
iDestruct
"Hv"
as
"[[% ?]Hv]"
;
last
iDestruct
"Hv"
as
{
m
}
"[% ?]"
;
subst
.
{
iDestruct
"Hv"
as
"[[% ?]Hv]"
;
last
iDestruct
"Hv"
as
{
m
}
"[% ?]"
;
subst
.
+
iSplit
.
iLeft
;
by
iSplitL
"Hl"
.
by
iLeft
.
+
iSplit
.
iLeft
;
by
iSplitL
"Hl"
.
by
iLeft
.
+
iSplit
.
iRight
;
iExists
m
;
by
iSplitL
"Hl"
.
iRight
;
iExists
m
;
by
iSplit
.
}
+
iSplit
.
iRight
;
iExists
m
;
by
iSplitL
"Hl"
.
iRight
;
iExists
m
;
by
iSplit
.
}
...
...
tests/proofmode.v
View file @
eacb1c46
...
@@ 26,7 +26,7 @@ Proof.
...
@@ 26,7 +26,7 @@ Proof.
iDestruct
"H1"
as
{
z1
z2
c
}
"(H1&_&#Hc)"
.
iDestruct
"H1"
as
{
z1
z2
c
}
"(H1&_&#Hc)"
.
iPoseProof
"Hc"
as
"foo"
.
iPoseProof
"Hc"
as
"foo"
.
iRevert
{
a
b
}
"Ha Hb"
.
iIntros
{
b
a
}
"Hb {foo} Ha"
.
iRevert
{
a
b
}
"Ha Hb"
.
iIntros
{
b
a
}
"Hb {foo} Ha"
.
iAssert
(
uPred_ownM
(
a
⋅
core
a
))
%
I
as
"[Ha #Hac]"
with
"[Ha
]"
.
iAssert
(
uPred_ownM
(
a
⋅
core
a
))
with
"[Ha]"
as
"[Ha #Hac
]"
.
{
by
rewrite
cmra_core_r
.
}
{
by
rewrite
cmra_core_r
.
}
iFrame
"Ha Hac"
.
iFrame
"Ha Hac"
.
iExists
(
S
j
+
z1
),
z2
.
iExists
(
S
j
+
z1
),
z2
.
...
...
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