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
Rice Wine
Iris
Commits
60a43009
Commit
60a43009
authored
Mar 05, 2016
by
Ralf Jung
Browse files
rename Cas -> CAS; make BAnon notation work better
parent
30758ade
Changes
6
Hide whitespace changes
Inline
Side-by-side
heap_lang/heap.v
View file @
60a43009
...
...
@@ -200,7 +200,7 @@ Section heap.
to_val
e1
=
Some
v1
→
to_val
e2
=
Some
v2
→
v'
≠
v1
→
P
⊑
heap_ctx
N
→
nclose
N
⊆
E
→
P
⊑
(
▷
l
↦
{
q
}
v'
★
▷
(
l
↦
{
q
}
v'
-
★
Φ
(
LitV
(
LitBool
false
))))
→
P
⊑
#>
C
as
(
Loc
l
)
e1
e2
@
E
{{
Φ
}}.
P
⊑
#>
C
AS
(
Loc
l
)
e1
e2
@
E
{{
Φ
}}.
Proof
.
rewrite
/
heap_ctx
/
heap_inv
=>?????
HP
Φ
.
apply
(
auth_fsa'
heap_inv
(
wp_fsa
_
)
id
)
...
...
@@ -217,7 +217,7 @@ Section heap.
to_val
e1
=
Some
v1
→
to_val
e2
=
Some
v2
→
P
⊑
heap_ctx
N
→
nclose
N
⊆
E
→
P
⊑
(
▷
l
↦
v1
★
▷
(
l
↦
v2
-
★
Φ
(
LitV
(
LitBool
true
))))
→
P
⊑
#>
C
as
(
Loc
l
)
e1
e2
@
E
{{
Φ
}}.
P
⊑
#>
C
AS
(
Loc
l
)
e1
e2
@
E
{{
Φ
}}.
Proof
.
rewrite
/
heap_ctx
/
heap_inv
=>
????
HP
Φ
.
apply
(
auth_fsa'
heap_inv
(
wp_fsa
_
)
(
alter
(
λ
_
,
Frac
1
(
DecAgree
v2
))
l
))
...
...
heap_lang/lang.v
View file @
60a43009
...
...
@@ -84,7 +84,7 @@ Inductive expr (X : list string) :=
|
Alloc
(
e
:
expr
X
)
|
Load
(
e
:
expr
X
)
|
Store
(
e1
:
expr
X
)
(
e2
:
expr
X
)
|
C
as
(
e0
:
expr
X
)
(
e1
:
expr
X
)
(
e2
:
expr
X
).
|
C
AS
(
e0
:
expr
X
)
(
e1
:
expr
X
)
(
e2
:
expr
X
).
Bind
Scope
expr_scope
with
expr
.
Delimit
Scope
expr_scope
with
E
.
...
...
@@ -106,7 +106,7 @@ Arguments Loc {_} _.
Arguments
Alloc
{
_
}
_
%
E
.
Arguments
Load
{
_
}
_
%
E
.
Arguments
Store
{
_
}
_
%
E
_
%
E
.
Arguments
C
as
{
_
}
_
%
E
_
%
E
_
%
E
.
Arguments
C
AS
{
_
}
_
%
E
_
%
E
_
%
E
.
Inductive
val
:
=
|
RecV
(
f
x
:
binder
)
(
e
:
expr
(
f
:
b
:
x
:
b
:
[]))
...
...
@@ -192,9 +192,9 @@ Definition fill_item (Ki : ectx_item) (e : expr []) : expr [] :=
|
LoadCtx
=>
Load
e
|
StoreLCtx
e2
=>
Store
e
e2
|
StoreRCtx
v1
=>
Store
(
of_val
v1
)
e
|
CasLCtx
e1
e2
=>
C
as
e
e1
e2
|
CasMCtx
v0
e2
=>
C
as
(
of_val
v0
)
e
e2
|
CasRCtx
v0
v1
=>
C
as
(
of_val
v0
)
(
of_val
v1
)
e
|
CasLCtx
e1
e2
=>
C
AS
e
e1
e2
|
CasMCtx
v0
e2
=>
C
AS
(
of_val
v0
)
e
e2
|
CasRCtx
v0
v1
=>
C
AS
(
of_val
v0
)
(
of_val
v1
)
e
end
.
Definition
fill
(
K
:
ectx
)
(
e
:
expr
[])
:
expr
[]
:
=
fold_right
fill_item
e
K
.
...
...
@@ -224,7 +224,7 @@ Program Fixpoint wexpr {X Y} (H : X `included` Y) (e : expr X) : expr Y :=
|
Alloc
e
=>
Alloc
(
wexpr
H
e
)
|
Load
e
=>
Load
(
wexpr
H
e
)
|
Store
e1
e2
=>
Store
(
wexpr
H
e1
)
(
wexpr
H
e2
)
|
C
as
e0
e1
e2
=>
C
as
(
wexpr
H
e0
)
(
wexpr
H
e1
)
(
wexpr
H
e2
)
|
C
AS
e0
e1
e2
=>
C
AS
(
wexpr
H
e0
)
(
wexpr
H
e1
)
(
wexpr
H
e2
)
end
.
Solve
Obligations
with
set_solver
.
...
...
@@ -265,7 +265,7 @@ Program Fixpoint wsubst {X Y} (x : string) (es : expr [])
|
Alloc
e
=>
Alloc
(
wsubst
x
es
H
e
)
|
Load
e
=>
Load
(
wsubst
x
es
H
e
)
|
Store
e1
e2
=>
Store
(
wsubst
x
es
H
e1
)
(
wsubst
x
es
H
e2
)
|
C
as
e0
e1
e2
=>
C
as
(
wsubst
x
es
H
e0
)
(
wsubst
x
es
H
e1
)
(
wsubst
x
es
H
e2
)
|
C
AS
e0
e1
e2
=>
C
AS
(
wsubst
x
es
H
e0
)
(
wsubst
x
es
H
e1
)
(
wsubst
x
es
H
e2
)
end
.
Solve
Obligations
with
set_solver
.
...
...
@@ -333,11 +333,11 @@ Inductive head_step : expr [] → state → expr [] → state → option (expr [
|
CasFailS
l
e1
v1
e2
v2
vl
σ
:
to_val
e1
=
Some
v1
→
to_val
e2
=
Some
v2
→
σ
!!
l
=
Some
vl
→
vl
≠
v1
→
head_step
(
C
as
(
Loc
l
)
e1
e2
)
σ
(
Lit
$
LitBool
false
)
σ
None
head_step
(
C
AS
(
Loc
l
)
e1
e2
)
σ
(
Lit
$
LitBool
false
)
σ
None
|
CasSucS
l
e1
v1
e2
v2
σ
:
to_val
e1
=
Some
v1
→
to_val
e2
=
Some
v2
→
σ
!!
l
=
Some
v1
→
head_step
(
C
as
(
Loc
l
)
e1
e2
)
σ
(
Lit
$
LitBool
true
)
(<[
l
:
=
v2
]>
σ
)
None
.
head_step
(
C
AS
(
Loc
l
)
e1
e2
)
σ
(
Lit
$
LitBool
true
)
(<[
l
:
=
v2
]>
σ
)
None
.
(** Atomic expressions *)
Definition
atomic
(
e
:
expr
[])
:
Prop
:
=
...
...
@@ -345,7 +345,7 @@ Definition atomic (e: expr []) : Prop :=
|
Alloc
e
=>
is_Some
(
to_val
e
)
|
Load
e
=>
is_Some
(
to_val
e
)
|
Store
e1
e2
=>
is_Some
(
to_val
e1
)
∧
is_Some
(
to_val
e2
)
|
C
as
e0
e1
e2
=>
is_Some
(
to_val
e0
)
∧
is_Some
(
to_val
e1
)
∧
is_Some
(
to_val
e2
)
|
C
AS
e0
e1
e2
=>
is_Some
(
to_val
e0
)
∧
is_Some
(
to_val
e1
)
∧
is_Some
(
to_val
e2
)
(* Make "skip" atomic *)
|
App
(
Rec
_
_
(
Lit
_
))
(
Lit
_
)
=>
True
|
_
=>
False
...
...
@@ -545,7 +545,7 @@ Fixpoint expr_beq {X Y} (e : expr X) (e' : expr Y) : bool :=
|
BinOp
op
e1
e2
,
BinOp
op'
e1'
e2'
=>
bool_decide
(
op
=
op'
)
&&
expr_beq
e1
e1'
&&
expr_beq
e2
e2'
|
If
e0
e1
e2
,
If
e0'
e1'
e2'
|
Case
e0
e1
e2
,
Case
e0'
e1'
e2'
|
C
as
e0
e1
e2
,
C
as
e0'
e1'
e2'
=>
C
AS
e0
e1
e2
,
C
AS
e0'
e1'
e2'
=>
expr_beq
e0
e0'
&&
expr_beq
e1
e1'
&&
expr_beq
e2
e2'
|
Fst
e
,
Fst
e'
|
Snd
e
,
Snd
e'
|
InjL
e
,
InjL
e'
|
InjR
e
,
InjR
e'
|
Fork
e
,
Fork
e'
|
Alloc
e
,
Alloc
e'
|
Load
e
,
Load
e'
=>
expr_beq
e
e'
...
...
@@ -595,3 +595,6 @@ Qed.
Global
Instance
heap_lang_ctx_item
Ki
:
LanguageCtx
heap_lang
(
heap_lang
.
fill_item
Ki
).
Proof
.
change
(
LanguageCtx
heap_lang
(
heap_lang
.
fill
[
Ki
])).
apply
_
.
Qed
.
(* Prefer heap_lang names over language names. *)
Export
heap_lang
.
heap_lang/lifting.v
View file @
60a43009
...
...
@@ -3,7 +3,6 @@ From heap_lang Require Export lang.
From
program_logic
Require
Import
lifting
.
From
program_logic
Require
Import
ownership
.
(* for ownP *)
From
heap_lang
Require
Import
tactics
.
Export
heap_lang
.
(* Prefer heap_lang names over language names. *)
Import
uPred
.
Local
Hint
Extern
0
(
language
.
reducible
_
_
)
=>
do_step
ltac
:
(
eauto
2
).
...
...
@@ -58,7 +57,7 @@ Qed.
Lemma
wp_cas_fail_pst
E
σ
l
e1
v1
e2
v2
v'
Φ
:
to_val
e1
=
Some
v1
→
to_val
e2
=
Some
v2
→
σ
!!
l
=
Some
v'
→
v'
≠
v1
→
(
▷
ownP
σ
★
▷
(
ownP
σ
-
★
Φ
(
LitV
$
LitBool
false
)))
⊑
#>
C
as
(
Loc
l
)
e1
e2
@
E
{{
Φ
}}.
⊑
#>
C
AS
(
Loc
l
)
e1
e2
@
E
{{
Φ
}}.
Proof
.
intros
.
rewrite
-(
wp_lift_atomic_det_step
σ
(
LitV
$
LitBool
false
)
σ
None
)
?right_id
//
;
last
by
intros
;
inv_step
;
eauto
.
...
...
@@ -67,7 +66,7 @@ Qed.
Lemma
wp_cas_suc_pst
E
σ
l
e1
v1
e2
v2
Φ
:
to_val
e1
=
Some
v1
→
to_val
e2
=
Some
v2
→
σ
!!
l
=
Some
v1
→
(
▷
ownP
σ
★
▷
(
ownP
(<[
l
:
=
v2
]>
σ
)
-
★
Φ
(
LitV
$
LitBool
true
)))
⊑
#>
C
as
(
Loc
l
)
e1
e2
@
E
{{
Φ
}}.
⊑
#>
C
AS
(
Loc
l
)
e1
e2
@
E
{{
Φ
}}.
Proof
.
intros
.
rewrite
-(
wp_lift_atomic_det_step
σ
(
LitV
$
LitBool
true
)
(<[
l
:
=
v2
]>
σ
)
None
)
?right_id
//
;
last
by
intros
;
inv_step
;
eauto
.
...
...
heap_lang/notation.v
View file @
60a43009
From
heap_lang
Require
Export
derived
.
Export
heap_lang
.
Arguments
wp
{
_
_
}
_
_
%
E
_
.
Notation
"
||
e @ E {{ Φ } }"
:
=
(
wp
E
e
%
E
Φ
)
Notation
"
#>
e @ E {{ Φ } }"
:
=
(
wp
E
e
%
E
Φ
)
(
at
level
20
,
e
,
Φ
at
level
200
,
format
"
||
e @ E {{ Φ } }"
)
:
uPred_scope
.
Notation
"
||
e {{ Φ } }"
:
=
(
wp
⊤
e
%
E
Φ
)
format
"
#>
e @ E {{ Φ } }"
)
:
uPred_scope
.
Notation
"
#>
e {{ Φ } }"
:
=
(
wp
⊤
e
%
E
Φ
)
(
at
level
20
,
e
,
Φ
at
level
200
,
format
"
||
e {{ Φ } }"
)
:
uPred_scope
.
format
"
#>
e {{ Φ } }"
)
:
uPred_scope
.
Coercion
LitInt
:
Z
>->
base_lit
.
Coercion
LitBool
:
bool
>->
base_lit
.
...
...
@@ -15,6 +16,7 @@ Coercion of_val : val >-> expr.
Coercion
BNamed
:
string
>->
binder
.
Notation
"<>"
:
=
BAnon
:
binder_scope
.
Notation
"<>"
:
=
BAnon
:
expr_scope
.
(* No scope for the values, does not conflict and scope is often not inferred properly. *)
Notation
"# l"
:
=
(
LitV
l
%
Z
%
V
)
(
at
level
8
,
format
"# l"
).
...
...
@@ -33,6 +35,9 @@ Notation "( e1 , e2 , .. , en )" := (Pair .. (Pair e1 e2) .. en) : expr_scope.
Notation
"'match:' e0 'with' 'InjL' x1 => e1 | 'InjR' x2 => e2 'end'"
:
=
(
Match
e0
x1
e1
x2
e2
)
(
e0
,
x1
,
e1
,
x2
,
e2
at
level
200
)
:
expr_scope
.
Notation
"'match:' e0 'with' 'InjR' x1 => e1 | 'InjL' x2 => e2 'end'"
:
=
(
Match
e0
x2
e2
x1
e1
)
(
e0
,
x1
,
e1
,
x2
,
e2
at
level
200
)
:
expr_scope
.
Notation
"()"
:
=
LitUnit
:
val_scope
.
Notation
"! e"
:
=
(
Load
e
%
E
)
(
at
level
9
,
right
associativity
)
:
expr_scope
.
Notation
"'ref' e"
:
=
(
Alloc
e
%
E
)
...
...
heap_lang/substitution.v
View file @
60a43009
...
...
@@ -78,7 +78,7 @@ Global Instance do_wexpr_store e1 e2 e1r e2r :
W
e1
e1r
→
W
e2
e2r
→
W
(
Store
e1
e2
)
(
Store
e1r
e2r
).
Proof
.
by
intros
;
red
;
f_equal
/=.
Qed
.
Global
Instance
do_wexpr_cas
e0
e1
e2
e0r
e1r
e2r
:
W
e0
e0r
→
W
e1
e1r
→
W
e2
e2r
→
W
(
C
as
e0
e1
e2
)
(
C
as
e0r
e1r
e2r
).
W
e0
e0r
→
W
e1
e1r
→
W
e2
e2r
→
W
(
C
AS
e0
e1
e2
)
(
C
AS
e0r
e1r
e2r
).
Proof
.
by
intros
;
red
;
f_equal
/=.
Qed
.
End
do_wexpr
.
...
...
@@ -185,7 +185,7 @@ Global Instance do_wsubst_store e1 e2 e1r e2r :
Sub
e1
e1r
→
Sub
e2
e2r
→
Sub
(
Store
e1
e2
)
(
Store
e1r
e2r
).
Proof
.
by
intros
;
red
;
f_equal
/=.
Qed
.
Global
Instance
do_wsubst_cas
e0
e1
e2
e0r
e1r
e2r
:
Sub
e0
e0r
→
Sub
e1
e1r
→
Sub
e2
e2r
→
Sub
(
C
as
e0
e1
e2
)
(
C
as
e0r
e1r
e2r
).
Sub
e0
e0r
→
Sub
e1
e1r
→
Sub
e2
e2r
→
Sub
(
C
AS
e0
e1
e2
)
(
C
AS
e0r
e1r
e2r
).
Proof
.
by
intros
;
red
;
f_equal
/=.
Qed
.
End
wsubst
.
...
...
heap_lang/tactics.v
View file @
60a43009
...
...
@@ -66,10 +66,10 @@ Ltac reshape_expr e tac :=
|
Load
?e
=>
go
(
LoadCtx
::
K
)
e
|
Store
?e1
?e2
=>
reshape_val
e1
ltac
:
(
fun
v1
=>
go
(
StoreRCtx
v1
::
K
)
e2
)
|
Store
?e1
?e2
=>
go
(
StoreLCtx
e2
::
K
)
e1
|
C
as
?e0
?e1
?e2
=>
reshape_val
e0
ltac
:
(
fun
v0
=>
first
|
C
AS
?e0
?e1
?e2
=>
reshape_val
e0
ltac
:
(
fun
v0
=>
first
[
reshape_val
e1
ltac
:
(
fun
v1
=>
go
(
CasRCtx
v0
v1
::
K
)
e2
)
|
go
(
CasMCtx
v0
e2
::
K
)
e1
])
|
C
as
?e0
?e1
?e2
=>
go
(
CasLCtx
e1
e2
::
K
)
e0
|
C
AS
?e0
?e1
?e2
=>
go
(
CasLCtx
e1
e2
::
K
)
e0
end
in
go
(@
nil
ectx_item
)
e
.
(** The tactic [do_step tac] solves goals of the shape [reducible], [prim_step]
...
...
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