Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
ReLoC
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Snippets
Build
Pipelines
Jobs
Pipeline schedules
Artifacts
Deploy
Releases
Model registry
Operate
Environments
Monitor
Incidents
Service Desk
Analyze
Value stream analytics
Contributor analytics
CI/CD analytics
Repository analytics
Model experiments
Help
Help
Support
GitLab documentation
Compare GitLab plans
Community forum
Contribute to GitLab
Provide feedback
Terms and privacy
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
Iris
ReLoC
Commits
d008408b
Commit
d008408b
authored
6 years ago
by
Dan Frumin
Browse files
Options
Downloads
Patches
Plain Diff
add the symbol ADT example
parent
e1c83937
No related branches found
No related tags found
No related merge requests found
Changes
3
Hide whitespace changes
Inline
Side-by-side
Showing
3 changed files
_CoqProject
+2
-1
2 additions, 1 deletion
_CoqProject
theories/examples/symbol.v
+390
-0
390 additions, 0 deletions
theories/examples/symbol.v
theories/lib/list.v
+101
-0
101 additions, 0 deletions
theories/lib/list.v
with
493 additions
and
1 deletion
_CoqProject
+
2
−
1
View file @
d008408b
...
@@ -31,8 +31,9 @@ theories/lib/lock.v
...
@@ -31,8 +31,9 @@ theories/lib/lock.v
theories/lib/counter.v
theories/lib/counter.v
theories/lib/Y.v
theories/lib/Y.v
theories/lib/assert.v
theories/lib/assert.v
theories/lib/list.v
theories/examples/bit.v
theories/examples/bit.v
theories/examples/or.v
theories/examples/or.v
theories/examples/generative.v
theories/examples/generative.v
theories/examples/symbol.v
This diff is collapsed.
Click to expand it.
theories/examples/symbol.v
0 → 100644
+
390
−
0
View file @
d008408b
(* ReLoC -- Relational logic for fine-grained concurrency *)
(** This is a generative ADT example from "State-Dependent
Represenation Independence" by A. Ahmed, D. Dreyer, A. Rossberg.
In this example we implement a symbol lookup table, where a symbol is
an abstract data type. Because the only way to obtain a symbol is to
insert something into the table, we can show that the dynamic check in
the lookup function in `symbol2` is redundant. *)
From
iris
.
proofmode
Require
Import
tactics
.
From
iris
.
algebra
Require
Import
auth
.
From
reloc
Require
Import
proofmode
.
From
reloc
.
lib
Require
Import
lock
list
.
From
reloc
.
typing
Require
Import
interp
soundness
.
(** * Symbol table *)
Definition
lty_symbol
`{
relocG
Σ
}
:
lty2
Σ
:=
∃
α
,
(
α
→
α
→
lty2_bool
)
(* equality check *)
×
(
lty2_int
→
α
)
(* insert *)
×
(
α
→
lty2_int
)
.
(* lookup *)
Definition
eqKey
:
val
:=
λ
:
"n"
"m"
,
"n"
=
"m"
.
Definition
symbol1
:
val
:=
λ
:
<>
,
let
:
"size"
:=
ref
#
0
in
let
:
"tbl"
:=
ref
NIL
in
let
:
"l"
:=
newlock
#
()
in
(
eqKey
,
λ
:
"s"
,
acquire
"l"
;;
let
:
"n"
:=
!
"size"
in
"size"
<-
"n"
+#
1
;;
"tbl"
<-
CONS
"s"
(
!
"tbl"
);;
release
"l"
;;
"n"
,
λ
:
"n"
,
nth
(
!
"tbl"
)
(
!
"size"
-
"n"
))
.
Definition
symbol2
:
val
:=
λ
:
<>
,
let
:
"size"
:=
ref
#
0
in
let
:
"tbl"
:=
ref
NIL
in
let
:
"l"
:=
newlock
#
()
in
(
eqKey
,
λ
:
"s"
,
acquire
"l"
;;
let
:
"n"
:=
!
"size"
in
"size"
<-
"n"
+#
1
;;
"tbl"
<-
CONS
"s"
(
!
"tbl"
);;
release
"l"
;;
"n"
,
λ
:
"n"
,
let
:
"m"
:=
!
"size"
in
if
:
"n"
≤
"m"
then
nth
(
!
"tbl"
)
(
!
"size"
-
"n"
)
else
#
0
)
.
(** * The actual refinement proof.
Requires monotonic state *)
Class
msizeG
Σ
:=
MSizeG
{
msize_inG
:>
inG
Σ
(
authR
mnatUR
)
}
.
Definition
msizeΣ
:
gFunctors
:=
#
[
GFunctor
(
authR
mnatUR
)]
.
Instance
subG_mcounterΣ
{
Σ
}
:
subG
msizeΣ
Σ
→
msizeG
Σ
.
Proof
.
solve_inG
.
Qed
.
Section
rules
.
Definition
sizeN
:=
relocN
.
@
"size"
.
Context
`{
!
relocG
Σ
,
!
msizeG
Σ
}
.
Context
(
γ
:
gname
)
.
Lemma
size_le
(
n
m
:
nat
)
:
own
γ
(
●
(
n
:
mnat
))
-∗
own
γ
(
◯
(
m
:
mnat
))
-∗
⌜
m
≤
n
⌝%
nat
.
Proof
.
iIntros
"Hn Hm"
.
by
iDestruct
(
own_valid_2
with
"Hn Hm"
)
as
%
[?
%
mnat_included
_]
%
auth_valid_discrete_2
.
Qed
.
Lemma
same_size
(
n
m
:
nat
)
:
own
γ
(
●
(
n
:
mnat
))
∗
own
γ
(
◯
(
m
:
mnat
))
==∗
own
γ
(
●
(
n
:
mnat
))
∗
own
γ
(
◯
(
n
:
mnat
))
.
Proof
.
iIntros
"[Hn Hm]"
.
iMod
(
own_update_2
γ
_
_
(
●
(
n
:
mnat
)
⋅
◯
(
n
:
mnat
))
with
"Hn Hm"
)
as
"[$ $]"
;
last
done
.
apply
auth_update
,
(
mnat_local_update
_
_
n
);
auto
.
Qed
.
Lemma
inc_size'
(
n
m
:
nat
)
:
own
γ
(
●
(
n
:
mnat
))
∗
own
γ
(
◯
(
m
:
mnat
))
==∗
own
γ
(
●
(
S
n
:
mnat
))
.
Proof
.
iIntros
"[Hn #Hm]"
.
iMod
(
own_update_2
γ
_
_
(
●
(
S
n
:
mnat
)
⋅
◯
(
S
n
:
mnat
))
with
"Hn Hm"
)
as
"[$ _]"
;
last
done
.
apply
auth_update
,
(
mnat_local_update
_
_
(
S
n
));
auto
.
Qed
.
Lemma
conjure_0
:
(|
==>
own
γ
(
◯
(
O
:
mnat
)))
%
I
.
Proof
.
by
apply
own_unit
.
Qed
.
Lemma
inc_size
(
n
:
nat
)
:
own
γ
(
●
(
n
:
mnat
))
==∗
own
γ
(
●
(
S
n
:
mnat
))
.
Proof
.
iIntros
"Hn"
.
iMod
(
conjure_0
)
as
"Hz"
.
iApply
inc_size'
;
by
iFrame
.
Qed
.
Definition
tableR
:
lty2
Σ
:=
Lty2
(
λ
v1
v2
,
(
∃
n
:
nat
,
⌜
v1
=
#
n
⌝
∗
⌜
v2
=
#
n
⌝
∗
own
γ
(
◯
(
n
:
mnat
))))
%
I
.
Definition
table_inv
(
size1
size2
tbl1
tbl2
:
loc
)
:
iProp
Σ
:=
(
∃
(
n
:
nat
)
(
ls
:
val
),
own
γ
(
●
(
n
:
mnat
))
∗
size1
↦
{
1
/
2
}
#
n
∗
size2
↦
ₛ
{
1
/
2
}
#
n
∗
tbl1
↦
{
1
/
2
}
ls
∗
tbl2
↦
ₛ
{
1
/
2
}
ls
∗
lty_list
lty2_int
ls
ls
)
%
I
.
Definition
lok_inv
(
size1
size2
tbl1
tbl2
l
:
loc
)
:
iProp
Σ
:=
(
∃
(
n
:
nat
)
(
ls
:
val
),
size1
↦
{
1
/
2
}
#
n
∗
size2
↦
ₛ
{
1
/
2
}
#
n
∗
tbl1
↦
{
1
/
2
}
ls
∗
tbl2
↦
ₛ
{
1
/
2
}
ls
∗
l
↦
ₛ
#
false
)
%
I
.
End
rules
.
Section
proof
.
Context
`{
!
relocG
Σ
,
!
msizeG
Σ
,
!
lockG
Σ
}
.
Lemma
eqKey_refinement
γ
:
REL
eqKey
<<
eqKey
:
tableR
γ
→
tableR
γ
→
lty2_bool
.
Proof
.
unlock
eqKey
.
iApply
refines_arrow_val
.
iAlways
.
iIntros
(
k1
k2
)
"/= #Hk"
.
iDestruct
"Hk"
as
(
n
)
"(% & % & #Hn)"
;
simplify_eq
.
rel_let_l
.
rel_let_r
.
rel_pure_l
.
rel_pure_r
.
iApply
refines_arrow_val
.
iAlways
.
iIntros
(
k1
k2
)
"/= #Hk"
.
iDestruct
"Hk"
as
(
m
)
"(% & % & #Hm)"
;
simplify_eq
.
rel_let_l
.
rel_let_r
.
rel_op_l
.
rel_op_r
.
rel_values
.
Qed
.
Lemma
lookup_refinement1
(
γ
:
gname
)
(
size1
size2
tbl1
tbl2
:
loc
)
:
inv
sizeN
(
table_inv
γ
size1
size2
tbl1
tbl2
)
-∗
REL
(
λ
:
"n"
,
(
nth
!
#
tbl1
)
(
!
#
size1
-
"n"
))
%
V
<<
(
λ
:
"n"
,
let
:
"m"
:=
!
#
size2
in
if
:
"n"
≤
"m"
then
(
nth
!
#
tbl2
)
(
!
#
size2
-
"n"
)
else
#
0
)
%
V
:
(
tableR
γ
→
lty2_int
)
.
Proof
.
iIntros
"#Hinv"
.
unlock
.
iApply
refines_arrow_val
.
iAlways
.
iIntros
(
k1
k2
)
"/= #Hk"
.
iDestruct
"Hk"
as
(
n
)
"(% & % & #Hn)"
;
simplify_eq
.
rel_let_l
.
rel_let_r
.
rel_load_l_atomic
.
iInv
sizeN
as
(
m
ls
)
"(Ha & Hs1' & Hs2' & Htbl1' & Htbl2' & #Hls)"
"Hcl"
.
iModIntro
.
iExists
_
.
iFrame
.
iNext
.
iIntros
"Hs1'"
.
rel_load_r
.
rel_pure_r
.
rel_pure_r
.
iDestruct
(
own_valid_2
with
"Ha Hn"
)
as
%
[?
%
mnat_included
_]
%
auth_valid_discrete_2
.
rel_op_l
.
rel_op_r
.
rewrite
bool_decide_true
;
last
lia
.
rel_pure_r
.
rel_load_r
.
rel_op_r
.
iMod
(
"Hcl"
with
"[Ha Hs1' Hs2' Htbl1' Htbl2' Hls]"
)
as
"_"
.
{
iNext
.
iExists
_,_
.
iFrame
.
repeat
iSplit
;
eauto
.
}
iClear
"Hls"
.
rel_load_l_atomic
.
iInv
sizeN
as
(
m'
ls'
)
"(Ha & Hs1' & >Hs2' & >Htbl1' & >Htbl2' & #Hls)"
"Hcl"
.
iModIntro
.
iExists
_
.
iFrame
.
iNext
.
iIntros
"Htbl1'"
.
rel_load_r
.
iMod
(
"Hcl"
with
"[Ha Hs1' Hs2' Htbl1' Htbl2' Hls]"
)
as
"_"
.
{
iNext
.
iExists
_,_
.
iFrame
.
repeat
iSplit
;
eauto
.
}
repeat
iApply
refines_app
.
-
iApply
nth_int_typed
.
-
rel_values
.
-
rel_values
.
Qed
.
Lemma
lookup_refinement2
(
γ
:
gname
)
(
size1
size2
tbl1
tbl2
:
loc
)
:
inv
sizeN
(
table_inv
γ
size1
size2
tbl1
tbl2
)
-∗
REL
(
λ
:
"n"
,
let
:
"m"
:=
!
#
size1
in
if
:
"n"
≤
"m"
then
(
nth
!
#
tbl1
)
(
!
#
size1
-
"n"
)
else
#
0
)
%
V
<<
(
λ
:
"n"
,
(
nth
!
#
tbl2
)
(
!
#
size2
-
"n"
))
%
V
:
(
tableR
γ
→
lty2_int
)
.
Proof
.
iIntros
"#Hinv"
.
unlock
.
iApply
refines_arrow_val
.
iAlways
.
iIntros
(
k1
k2
)
"#Hk /="
.
iDestruct
"Hk"
as
(
n
)
"(% & % & #Hn)"
;
simplify_eq
.
repeat
rel_pure_l
.
repeat
rel_pure_r
.
rel_load_l_atomic
.
iInv
sizeN
as
(
m
ls
)
"(Ha & Hs1' & >Hs2' & >Htbl1' & >Htbl2' & Hls)"
"Hcl"
.
iModIntro
.
iExists
_
.
iFrame
.
iNext
.
iIntros
"Hs1'"
.
iDestruct
(
own_valid_2
with
"Ha Hn"
)
as
%
[?
%
mnat_included
_]
%
auth_valid_discrete_2
.
iMod
(
"Hcl"
with
"[Ha Hs1' Hs2' Htbl1' Htbl2' Hls]"
)
as
"_"
.
{
iNext
.
iExists
_,_
.
by
iFrame
.
}
clear
ls
.
repeat
rel_pure_l
.
case_bool_decide
;
last
by
lia
.
rel_if_l
.
rel_load_l_atomic
.
iInv
sizeN
as
(
m'
ls
)
"(Ha & Hs1' & Hs2' & Htbl1' & Htbl2' & Hls)"
"Hcl"
.
iModIntro
.
iExists
_
.
iFrame
.
iNext
.
iIntros
"Hs1'"
.
rel_load_r
.
iMod
(
"Hcl"
with
"[Ha Hs1' Hs2' Htbl1' Htbl2' Hls]"
)
as
"_"
.
{
iNext
.
iExists
_,_
.
by
iFrame
.
}
rel_pure_l
.
rel_pure_r
.
rel_load_l_atomic
.
clear
ls
.
iInv
sizeN
as
(?
ls
)
"(Ha & Hs1' & Hs2' & Htbl1' & Htbl2' & #Hls)"
"Hcl"
.
iModIntro
.
iExists
_
.
iFrame
.
iNext
.
iIntros
"Htbl1'"
.
rel_load_r
.
iMod
(
"Hcl"
with
"[Ha Hs1' Hs2' Htbl1' Htbl2']"
)
as
"_"
.
{
iNext
.
iExists
_,_
.
by
iFrame
.
}
repeat
iApply
refines_app
.
-
iApply
nth_int_typed
.
-
rel_values
.
-
rel_values
.
Qed
.
Definition
symbolτ
:
type
:=
TExists
(
TProd
(
TProd
(
TArrow
(
TVar
0
)
(
TArrow
(
TVar
0
)
TBool
))
(
TArrow
TNat
(
TVar
0
)))
(
TArrow
(
TVar
0
)
TNat
))
%
nat
.
Lemma
refinement1
Δ
:
{
Δ
;
∅
}
⊨
symbol1
≤
log
≤
symbol2
:
TArrow
TUnit
symbolτ
.
Proof
.
unlock
symbol1
symbol2
.
iIntros
(
vs
)
"Hvs"
.
rewrite
fmap_empty
.
rewrite
env_ltyped2_empty_inv
.
iDestruct
"Hvs"
as
%->
.
rewrite
!
fmap_empty
!
subst_map_empty
.
iApply
refines_arrow_val
.
fold
interp
.
iAlways
.
iIntros
(?
?)
"[% %]"
;
simplify_eq
/=.
rel_let_l
.
rel_let_r
.
rel_alloc_l
size1
as
"[Hs1 Hs1']"
;
repeat
rel_pure_l
.
rel_alloc_r
size2
as
"[Hs2 Hs2']"
;
repeat
rel_pure_r
.
rel_alloc_l
tbl1
as
"[Htbl1 Htbl1']"
;
repeat
rel_pure_l
.
rel_alloc_r
tbl2
as
"[Htbl2 Htbl2']"
;
repeat
rel_pure_r
.
iMod
(
own_alloc
(
●
(
0
%
nat
:
mnat
)))
as
(
γ
)
"Ha"
;
first
done
.
iMod
(
inv_alloc
sizeN
_
(
table_inv
γ
size1
size2
tbl1
tbl2
)
with
"[Hs1 Hs2 Htbl1 Htbl2 Ha]"
)
as
"#Hinv"
.
{
iNext
.
iExists
_,_
.
iFrame
.
iApply
lty_list_nil
.
}
rel_apply_r
refines_newlock_r
.
iIntros
(
l2
)
"Hl2"
.
rel_pure_r
.
rel_pure_r
.
pose
(
N
:=(
relocN
.
@
"lock1"
))
.
rel_apply_l
(
refines_newlock_l
N
(
lok_inv
size1
size2
tbl1
tbl2
l2
)
%
I
with
"[Hs1' Hs2' Htbl1' Htbl2' Hl2]"
)
.
{
iExists
0
%
nat
,_
.
by
iFrame
.
}
iNext
.
iIntros
(
l1
γl
)
"#Hl1"
.
rel_pure_l
.
rel_pure_l
.
iApply
(
refines_exists
(
tableR
γ
))
.
repeat
iApply
refines_pair
.
(* Eq *)
-
iApply
eqKey_refinement
.
(* Insert *)
-
rel_pure_l
.
rel_pure_r
.
iApply
refines_arrow_val
.
iAlways
.
iIntros
(?
?)
.
iDestruct
1
as
(
n
)
"[% %]"
;
simplify_eq
/=.
repeat
rel_pure_l
.
repeat
rel_pure_r
.
rel_apply_l
(
refines_acquire_l
with
"Hl1"
)
.
iNext
.
iIntros
"Hlk Htbl"
.
repeat
rel_pure_l
.
iDestruct
"Htbl"
as
(
m
ls
)
"(Hs1 & Hs2 & Htbl1 & Htbl2 & Hl2)"
.
rel_load_l
.
repeat
rel_pure_l
.
rel_store_l_atomic
.
iInv
sizeN
as
(
m'
ls'
)
"(Ha & >Hs1' & >Hs2' & >Htbl1' & >Htbl2' & #Hls)"
"Hcl"
.
iDestruct
(
gen_heap
.
mapsto_agree
with
"Hs1 Hs1'"
)
as
%
Hm'
.
simplify_eq
/=.
iCombine
"Hs1 Hs1'"
as
"Hs1"
.
iDestruct
(
gen_heap
.
mapsto_agree
with
"Htbl1 Htbl1'"
)
as
%->
.
iModIntro
.
iExists
_
.
iFrame
.
iNext
.
iIntros
"[Hs1 Hs1']"
.
repeat
rel_pure_l
.
rel_apply_r
(
refines_acquire_r
with
"Hl2"
)
.
iIntros
"Hl2"
.
repeat
rel_pure_r
.
iDestruct
(
mapsto_half_combine
with
"Hs2 Hs2'"
)
as
"[% Hs2]"
;
simplify_eq
.
rel_load_r
.
repeat
rel_pure_r
.
rel_store_r
.
repeat
rel_pure_r
.
(* Before we close the lock, we need to gather some evidence *)
iMod
(
conjure_0
γ
)
as
"Hf"
.
iMod
(
same_size
with
"[$Ha $Hf]"
)
as
"[Ha #Hf]"
.
iMod
(
inc_size
with
"Ha"
)
as
"Ha"
.
iDestruct
"Hs2"
as
"[Hs2 Hs2']"
.
replace
(
m'
+
1
)
with
(
Z
.
of_nat
(
S
m'
));
last
lia
.
iMod
(
"Hcl"
with
"[Ha Hs1 Hs2 Htbl1 Htbl2]"
)
as
"_"
.
{
iNext
.
iExists
_,_
.
by
iFrame
.
}
rel_load_l
.
repeat
rel_pure_l
.
rel_store_l_atomic
.
iClear
"Hls"
.
iInv
sizeN
as
(
m
ls
)
"(Ha & >Hs1 & >Hs2 & >Htbl1 & >Htbl2 & #Hls)"
"Hcl"
.
iDestruct
(
gen_heap
.
mapsto_agree
with
"Htbl1 Htbl1'"
)
as
%->
.
iCombine
"Htbl1 Htbl1'"
as
"Htbl1"
.
iModIntro
.
iExists
_
.
iFrame
.
iNext
.
iIntros
"[Htbl1 Htbl1']"
.
repeat
rel_pure_l
.
repeat
rel_pure_r
.
rel_load_r
.
iDestruct
(
mapsto_half_combine
with
"Htbl2 Htbl2'"
)
as
"[% Htbl2]"
;
simplify_eq
.
repeat
rel_pure_r
.
rel_store_r
.
repeat
rel_pure_r
.
rel_apply_r
(
refines_release_r
with
"Hl2"
)
.
iIntros
"Hl2"
.
repeat
rel_pure_r
.
iDestruct
"Htbl2"
as
"[Htbl2 Htbl2']"
.
iMod
(
"Hcl"
with
"[Ha Hs1 Hs2 Htbl1 Htbl2]"
)
as
"_"
.
{
iNext
.
iExists
_,_
.
iFrame
.
iApply
lty_list_cons
;
eauto
.
}
rel_apply_l
(
refines_release_l
with
"Hl1 Hlk [-]"
);
auto
.
{
iExists
_,_
.
by
iFrame
.
}
iNext
.
do
2
rel_pure_l
.
rel_values
.
iExists
m'
.
eauto
.
(* Lookup *)
-
rel_pure_l
.
rel_pure_r
.
iPoseProof
(
lookup_refinement1
with
"Hinv"
)
as
"H"
.
unlock
.
iApply
"H"
.
(* TODO how to avoid this? *)
Qed
.
Lemma
refinement2
Δ
:
{
Δ
;
∅
}
⊨
symbol2
≤
log
≤
symbol1
:
TArrow
TUnit
symbolτ
.
Proof
.
unlock
symbol1
symbol2
.
iIntros
(
vs
)
"Hvs"
.
rewrite
fmap_empty
.
rewrite
env_ltyped2_empty_inv
.
iDestruct
"Hvs"
as
%->
.
rewrite
!
fmap_empty
!
subst_map_empty
.
iApply
refines_arrow_val
.
fold
interp
.
iAlways
.
iIntros
(?
?)
"[% %]"
;
simplify_eq
/=.
rel_let_l
.
rel_let_r
.
rel_alloc_l
size1
as
"[Hs1 Hs1']"
;
repeat
rel_pure_l
.
rel_alloc_r
size2
as
"[Hs2 Hs2']"
;
repeat
rel_pure_r
.
rel_alloc_l
tbl1
as
"[Htbl1 Htbl1']"
;
repeat
rel_pure_l
.
rel_alloc_r
tbl2
as
"[Htbl2 Htbl2']"
;
repeat
rel_pure_r
.
iMod
(
own_alloc
(
●
(
0
%
nat
:
mnat
)))
as
(
γ
)
"Ha"
;
first
done
.
iMod
(
inv_alloc
sizeN
_
(
table_inv
γ
size1
size2
tbl1
tbl2
)
with
"[Hs1 Hs2 Htbl1 Htbl2 Ha]"
)
as
"#Hinv"
.
{
iNext
.
iExists
_,_
.
iFrame
.
iApply
lty_list_nil
.
}
rel_apply_r
refines_newlock_r
.
iIntros
(
l2
)
"Hl2"
.
rel_pure_r
.
rel_pure_r
.
pose
(
N
:=(
relocN
.
@
"lock1"
))
.
rel_apply_l
(
refines_newlock_l
N
(
lok_inv
size1
size2
tbl1
tbl2
l2
)
%
I
with
"[Hs1' Hs2' Htbl1' Htbl2' Hl2]"
)
.
{
iExists
0
%
nat
,_
.
by
iFrame
.
}
iNext
.
iIntros
(
l1
γl
)
"#Hl1"
.
rel_pure_l
.
rel_pure_l
.
iApply
(
refines_exists
(
tableR
γ
))
.
repeat
iApply
refines_pair
.
(* Eq *)
-
iApply
eqKey_refinement
.
(* Insert *)
-
rel_pure_l
.
rel_pure_r
.
iApply
refines_arrow_val
.
iAlways
.
iIntros
(?
?)
.
iDestruct
1
as
(
n
)
"[% %]"
;
simplify_eq
/=.
repeat
rel_pure_l
.
repeat
rel_pure_r
.
rel_apply_l
(
refines_acquire_l
with
"Hl1"
)
.
iNext
.
iIntros
"Hlk Htbl"
.
repeat
rel_pure_l
.
iDestruct
"Htbl"
as
(
m
ls
)
"(Hs1 & Hs2 & Htbl1 & Htbl2 & Hl2)"
.
rel_load_l
.
repeat
rel_pure_l
.
rel_store_l_atomic
.
iInv
sizeN
as
(
m'
ls'
)
"(Ha & >Hs1' & >Hs2' & >Htbl1' & >Htbl2' & #Hls)"
"Hcl"
.
iDestruct
(
gen_heap
.
mapsto_agree
with
"Hs1 Hs1'"
)
as
%
Hm'
.
simplify_eq
/=.
iCombine
"Hs1 Hs1'"
as
"Hs1"
.
iDestruct
(
gen_heap
.
mapsto_agree
with
"Htbl1 Htbl1'"
)
as
%->
.
iModIntro
.
iExists
_
.
iFrame
.
iNext
.
iIntros
"[Hs1 Hs1']"
.
repeat
rel_pure_l
.
rel_apply_r
(
refines_acquire_r
with
"Hl2"
)
.
iIntros
"Hl2"
.
repeat
rel_pure_r
.
iDestruct
(
mapsto_half_combine
with
"Hs2 Hs2'"
)
as
"[% Hs2]"
;
simplify_eq
.
rel_load_r
.
repeat
rel_pure_r
.
rel_store_r
.
repeat
rel_pure_r
.
(* Before we close the lock, we need to gather some evidence *)
iMod
(
conjure_0
γ
)
as
"Hf"
.
iMod
(
same_size
with
"[$Ha $Hf]"
)
as
"[Ha #Hf]"
.
iMod
(
inc_size
with
"Ha"
)
as
"Ha"
.
iDestruct
"Hs2"
as
"[Hs2 Hs2']"
.
replace
(
m'
+
1
)
with
(
Z
.
of_nat
(
S
m'
));
last
lia
.
iMod
(
"Hcl"
with
"[Ha Hs1 Hs2 Htbl1 Htbl2]"
)
as
"_"
.
{
iNext
.
iExists
_,_
.
by
iFrame
.
}
rel_load_l
.
repeat
rel_pure_l
.
rel_store_l_atomic
.
iClear
"Hls"
.
iInv
sizeN
as
(
m
ls
)
"(Ha & >Hs1 & >Hs2 & >Htbl1 & >Htbl2 & #Hls)"
"Hcl"
.
iDestruct
(
gen_heap
.
mapsto_agree
with
"Htbl1 Htbl1'"
)
as
%->
.
iCombine
"Htbl1 Htbl1'"
as
"Htbl1"
.
iModIntro
.
iExists
_
.
iFrame
.
iNext
.
iIntros
"[Htbl1 Htbl1']"
.
repeat
rel_pure_l
.
repeat
rel_pure_r
.
rel_load_r
.
iDestruct
(
mapsto_half_combine
with
"Htbl2 Htbl2'"
)
as
"[% Htbl2]"
;
simplify_eq
.
repeat
rel_pure_r
.
rel_store_r
.
repeat
rel_pure_r
.
rel_apply_r
(
refines_release_r
with
"Hl2"
)
.
iIntros
"Hl2"
.
repeat
rel_pure_r
.
iDestruct
"Htbl2"
as
"[Htbl2 Htbl2']"
.
iMod
(
"Hcl"
with
"[Ha Hs1 Hs2 Htbl1 Htbl2]"
)
as
"_"
.
{
iNext
.
iExists
_,_
.
iFrame
.
iApply
lty_list_cons
;
eauto
.
}
rel_apply_l
(
refines_release_l
with
"Hl1 Hlk [-]"
);
auto
.
{
iExists
_,_
.
by
iFrame
.
}
iNext
.
do
2
rel_pure_l
.
rel_values
.
iExists
m'
.
eauto
.
(* Lookup *)
-
rel_pure_l
.
rel_pure_r
.
iPoseProof
(
lookup_refinement2
with
"Hinv"
)
as
"H"
.
unlock
.
iApply
"H"
.
(* TODO how to avoid this? *)
Qed
.
End
proof
.
This diff is collapsed.
Click to expand it.
theories/lib/list.v
0 → 100644
+
101
−
0
View file @
d008408b
(* ReLoC -- Relational logic for fine-grained concurrency *)
(** Lists, their semantics types, and operations on them *)
From
reloc
Require
Import
proofmode
.
From
reloc
.
typing
Require
Import
types
interp
.
Notation
CONS
h
t
:=
(
SOME
(
Pair
h
t
))
.
Notation
CONSV
h
t
:=
(
SOMEV
(
PairV
h
t
))
.
Notation
NIL
:=
NONE
.
Notation
NILV
:=
NONEV
.
Fixpoint
is_list
(
hd
:
val
)
(
xs
:
list
val
)
:
Prop
:=
match
xs
with
|
[]
=>
hd
=
NILV
|
x
::
xs
=>
∃
hd'
,
hd
=
CONSV
x
hd'
∧
is_list
hd'
xs
end
.
(* TODO: is it possible to do this without `Program Definition`? *)
(* TODO: notation for lty_sum *)
Program
Definition
lty_list
`{
relocG
Σ
}
(
A
:
lty2
Σ
)
:
lty2
Σ
:=
lty2_rec
(
λ
ne
B
,
lty2_sum
()
(
A
×
B
))
%
lty2
.
Next
Obligation
.
solve_proper
.
Qed
.
Definition
nth
:
val
:=
rec
:
"nth"
"l"
"n"
:=
match
:
rec_unfold
"l"
with
NONE
=>
#
0
|
SOME
"xs"
=>
if
:
"n"
=
#
0
then
Fst
"xs"
else
"nth"
(
Snd
"xs"
)
(
"n"
-
#
1
)
end
.
Lemma
lty_list_nil
`{
relocG
Σ
}
A
:
lty_list
A
NILV
NILV
.
Proof
.
unfold
lty_list
.
rewrite
lty_rec_unfold
/=.
unfold
lty2_rec1
,
lty2_car
.
(* TODO so much unfolding *)
simpl
.
iNext
.
iExists
_,_
.
iLeft
.
repeat
iSplit
;
eauto
.
Qed
.
Lemma
lty_list_cons
`{
relocG
Σ
}
(
A
:
lty2
Σ
)
v1
v2
ls1
ls2
:
A
v1
v2
-∗
lty_list
A
ls1
ls2
-∗
lty_list
A
(
CONSV
v1
ls1
)
(
CONSV
v2
ls2
)
.
Proof
.
iIntros
"#HA #Hls"
.
rewrite
{
2
}
/
lty_list
lty_rec_unfold
/=.
rewrite
/
lty2_rec1
{
3
}
/
lty2_car
.
iNext
.
simpl
.
iExists
_,
_
.
iRight
.
repeat
iSplit
;
eauto
.
rewrite
{
1
}
/
lty2_prod
/
lty2_car
/=.
iExists
_,_,_,_
.
repeat
iSplit
;
eauto
.
Qed
.
Lemma
refines_nth_l
`{
relocG
Σ
}
(
A
:
lty2
Σ
)
K
v
w
ls
(
n
:
nat
)
t
:
is_list
v
ls
→
ls
!!
n
=
Some
w
→
(
REL
fill
K
(
of_val
w
)
<<
t
:
A
)
-∗
REL
fill
K
(
nth
v
#
n
)
<<
t
:
A
.
Proof
.
iInduction
ls
as
[|
hd
tl
]
"IH"
forall
(
v
n
)
.
-
iIntros
(_
Hl
)
.
destruct
n
;
simplify_eq
/=.
-
iIntros
(
Hv
Hn
)
"Hl"
.
simpl
in
*.
destruct
Hv
as
(
hd'
&
->
&
Hv
)
.
rel_rec_l
.
repeat
rel_pure_l
.
rel_rec_l
.
repeat
rel_pure_l
.
destruct
n
as
[|
n'
]
.
+
rewrite
bool_decide_true
//.
repeat
rel_pure_l
.
simpl
in
Hn
.
by
simplify_eq
/=.
+
rewrite
bool_decide_false
//.
repeat
rel_pure_l
.
simpl
in
Hn
.
replace
((
S
n'
)
%
nat
-
1
)
%
Z
with
(
Z
.
of_nat
n'
);
last
by
lia
.
iApply
"IH"
;
eauto
.
Qed
.
Lemma
refines_nth_r
`{
relocG
Σ
}
(
A
:
lty2
Σ
)
K
v
w
ls
(
n
:
nat
)
e
:
is_list
v
ls
→
ls
!!
n
=
Some
w
→
(
REL
e
<<
fill
K
(
of_val
w
)
:
A
)
-∗
REL
e
<<
fill
K
(
nth
v
#
n
)
:
A
.
Proof
.
iInduction
ls
as
[|
hd
tl
]
"IH"
forall
(
v
n
)
.
-
iIntros
(_
Hl
)
.
destruct
n
;
simplify_eq
/=.
-
iIntros
(
Hv
Hn
)
"Hl"
.
simpl
in
*.
destruct
Hv
as
(
hd'
&
->
&
Hv
)
.
rel_rec_r
.
repeat
rel_pure_r
.
rel_rec_r
.
repeat
rel_pure_r
.
destruct
n
as
[|
n'
]
.
+
rewrite
bool_decide_true
//.
repeat
rel_pure_r
.
simpl
in
Hn
.
by
simplify_eq
/=.
+
rewrite
bool_decide_false
//.
repeat
rel_pure_r
.
simpl
in
Hn
.
replace
((
S
n'
)
%
nat
-
1
)
%
Z
with
(
Z
.
of_nat
n'
);
last
by
lia
.
iApply
"IH"
;
eauto
.
Qed
.
Lemma
nth_int_typed
`{
relocG
Σ
}
:
REL
nth
<<
nth
:
lty_list
lty2_int
→
lty2_int
→
lty2_int
.
Proof
.
admit
.
Admitted
.
This diff is collapsed.
Click to expand it.
Preview
0%
Loading
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!
Save comment
Cancel
Please
register
or
sign in
to comment