Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
E
examples
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
0
Issues
0
List
Boards
Labels
Service Desk
Milestones
Merge Requests
0
Merge Requests
0
CI / CD
CI / CD
Pipelines
Jobs
Schedules
Operations
Operations
Incidents
Environments
Analytics
Analytics
CI / CD
Repository
Value Stream
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Jobs
Commits
Issue Boards
Open sidebar
Simon Spies
examples
Commits
c56b93ab
Commit
c56b93ab
authored
Sep 19, 2019
by
Simon Spies
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
refactor to use iris arrays more and move semantic invariants out
parent
8e68836b
Pipeline
#19778
canceled with stage
Changes
4
Pipelines
1
Expand all
Hide whitespace changes
Inline
Side-by-side
Showing
4 changed files
with
433 additions
and
425 deletions
+433
-425
_CoqProject
_CoqProject
+1
-0
theories/logrel_heaplang/lib/arrays.v
theories/logrel_heaplang/lib/arrays.v
+144
-326
theories/logrel_heaplang/lib/invariants.v
theories/logrel_heaplang/lib/invariants.v
+197
-0
theories/logrel_heaplang/lib/vectors.v
theories/logrel_heaplang/lib/vectors.v
+91
-99
No files found.
_CoqProject
View file @
c56b93ab
...
...
@@ -80,6 +80,7 @@ theories/logrel/F_mu_ref_conc/examples/fact.v
theories/logrel_heaplang/ltyping.v
theories/logrel_heaplang/ltyping_safety.v
theories/logrel_heaplang/lib/symbol_adt.v
theories/logrel_heaplang/lib/invariants.v
theories/logrel_heaplang/lib/arrays.v
theories/logrel_heaplang/lib/vectors.v
...
...
theories/logrel_heaplang/lib/arrays.v
View file @
c56b93ab
This diff is collapsed.
Click to expand it.
theories/logrel_heaplang/lib/invariants.v
0 → 100644
View file @
c56b93ab
(* TODO: merge this into iris *)
From
iris
.
base_logic
.
lib
Require
Export
fancy_updates
.
From
stdpp
Require
Export
namespaces
.
From
iris
.
base_logic
.
lib
Require
Import
wsat
.
From
iris
.
algebra
Require
Import
gmap
.
From
iris
.
proofmode
Require
Import
tactics
.
Set
Default
Proof
Using
"Type"
.
Import
uPred
.
Lemma
fresh_inv_name
(
E
:
gset
positive
)
N
:
∃
i
,
i
∉
E
∧
i
∈
(
↑
N
:
coPset
).
Proof
.
exists
(
coPpick
(
↑
N
∖
gset_to_coPset
E
)).
rewrite
-
elem_of_gset_to_coPset
(
comm
and
)
-
elem_of_difference
.
apply
coPpick_elem_of
=>
Hfin
.
eapply
nclose_infinite
,
(
difference_finite_inv
_
_
),
Hfin
.
apply
gset_to_coPset_finite
.
Qed
.
(** * Invariants *)
Section
inv
.
Context
`
{!
invG
Σ
}.
(** Internal backing store of invariants *)
Definition
internal_inv_def
(
N
:
namespace
)
(
P
:
iProp
Σ
)
:
iProp
Σ
:
=
(
∃
i
P'
,
⌜
i
∈
(
↑
N
:
coPset
)
⌝
∧
▷
□
(
P'
↔
P
)
∧
ownI
i
P'
)%
I
.
Definition
internal_inv_aux
:
seal
(@
internal_inv_def
).
by
eexists
.
Qed
.
Definition
internal_inv
:
=
internal_inv_aux
.(
unseal
).
Definition
internal_inv_eq
:
@
internal_inv
=
@
internal_inv_def
:
=
internal_inv_aux
.(
seal_eq
).
Typeclasses
Opaque
internal_inv
.
Global
Instance
internal_inv_persistent
N
P
:
Persistent
(
internal_inv
N
P
).
Proof
.
rewrite
internal_inv_eq
/
internal_inv
;
apply
_
.
Qed
.
Lemma
internal_inv_open
E
N
P
:
↑
N
⊆
E
→
internal_inv
N
P
={
E
,
E
∖↑
N
}=
∗
▷
P
∗
(
▷
P
={
E
∖↑
N
,
E
}=
∗
True
).
Proof
.
rewrite
internal_inv_eq
/
internal_inv_def
uPred_fupd_eq
/
uPred_fupd_def
.
iDestruct
1
as
(
i
P'
)
"(Hi & #HP' & #HiP)"
.
iDestruct
"Hi"
as
%
?%
elem_of_subseteq_singleton
.
rewrite
{
1
4
}(
union_difference_L
(
↑
N
)
E
)
//
ownE_op
;
last
set_solver
.
rewrite
{
1
5
}(
union_difference_L
{[
i
]}
(
↑
N
))
//
ownE_op
;
last
set_solver
.
iIntros
"(Hw & [HE $] & $) !> !>"
.
iDestruct
(
ownI_open
i
with
"[$Hw $HE $HiP]"
)
as
"($ & HP & HD)"
.
iDestruct
(
"HP'"
with
"HP"
)
as
"$"
.
iIntros
"HP [Hw $] !> !>"
.
iApply
(
ownI_close
_
P'
).
iFrame
"HD Hw HiP"
.
iApply
"HP'"
.
iFrame
.
Qed
.
Lemma
internal_inv_alloc
N
E
P
:
▷
P
={
E
}=
∗
internal_inv
N
P
.
Proof
.
rewrite
internal_inv_eq
/
internal_inv_def
uPred_fupd_eq
.
iIntros
"HP [Hw $]"
.
iMod
(
ownI_alloc
(
∈
(
↑
N
:
coPset
))
P
with
"[$HP $Hw]"
)
as
(
i
?)
"[$ ?]"
;
auto
using
fresh_inv_name
.
do
2
iModIntro
.
iExists
i
,
P
.
rewrite
-(
iff_refl
True
%
I
).
auto
.
Qed
.
Lemma
internal_inv_alloc_open
N
E
P
:
↑
N
⊆
E
→
(|={
E
,
E
∖↑
N
}=>
internal_inv
N
P
∗
(
▷
P
={
E
∖↑
N
,
E
}=
∗
True
))%
I
.
Proof
.
rewrite
internal_inv_eq
/
internal_inv_def
uPred_fupd_eq
.
iIntros
(
Sub
)
"[Hw HE]"
.
iMod
(
ownI_alloc_open
(
∈
(
↑
N
:
coPset
))
P
with
"Hw"
)
as
(
i
?)
"(Hw & #Hi & HD)"
;
auto
using
fresh_inv_name
.
iAssert
(
ownE
{[
i
]}
∗
ownE
(
↑
N
∖
{[
i
]})
∗
ownE
(
E
∖
↑
N
))%
I
with
"[HE]"
as
"(HEi & HEN\i & HE\N)"
.
{
rewrite
-
?ownE_op
;
[|
set_solver
..].
rewrite
assoc_L
-!
union_difference_L
//.
set_solver
.
}
do
2
iModIntro
.
iFrame
"HE\N"
.
iSplitL
"Hw HEi"
;
first
by
iApply
"Hw"
.
iSplitL
"Hi"
.
{
iExists
i
,
P
.
rewrite
-(
iff_refl
True
%
I
).
auto
.
}
iIntros
"HP [Hw HE\N]"
.
iDestruct
(
ownI_close
with
"[$Hw $Hi $HP $HD]"
)
as
"[$ HEi]"
.
do
2
iModIntro
.
iSplitL
;
[|
done
].
iCombine
"HEi HEN\i HE\N"
as
"HEN"
.
rewrite
-
?ownE_op
;
[|
set_solver
..].
rewrite
assoc_L
-!
union_difference_L
//
;
set_solver
.
Qed
.
(** Invariants API *)
Definition
inv_def
(
N
:
namespace
)
(
P
:
iProp
Σ
)
:
iProp
Σ
:
=
(
□
(
∀
E
,
⌜↑
N
⊆
E
⌝
→
|={
E
,
E
∖
↑
N
}=>
▷
P
∗
(
▷
P
={
E
∖
↑
N
,
E
}=
∗
True
)))%
I
.
Definition
inv_aux
:
seal
(@
inv_def
).
by
eexists
.
Qed
.
Definition
inv
:
=
inv_aux
.(
unseal
).
Definition
inv_eq
:
@
inv
=
@
inv_def
:
=
inv_aux
.(
seal_eq
).
Typeclasses
Opaque
inv
.
(** Properties about invariants *)
Global
Instance
inv_contractive
N
:
Contractive
(
inv
N
).
Proof
.
rewrite
inv_eq
.
solve_contractive
.
Qed
.
Global
Instance
inv_ne
N
:
NonExpansive
(
inv
N
).
Proof
.
apply
contractive_ne
,
_
.
Qed
.
Global
Instance
inv_proper
N
:
Proper
(
equiv
==>
equiv
)
(
inv
N
).
Proof
.
apply
ne_proper
,
_
.
Qed
.
Global
Instance
inv_persistent
M
P
:
Persistent
(
inv
M
P
).
Proof
.
rewrite
inv_eq
.
typeclasses
eauto
.
Qed
.
Lemma
inv_acc
N
P
Q
:
inv
N
P
-
∗
▷
□
(
P
-
∗
Q
∗
(
Q
-
∗
P
))
-
∗
inv
N
Q
.
Proof
.
iIntros
"#I #Acc"
.
rewrite
inv_eq
.
iModIntro
.
iIntros
(
E
H
).
iDestruct
(
"I"
$!
E
H
)
as
"#I'"
.
iApply
fupd_wand_r
.
iFrame
"I'"
.
iIntros
"(P & Hclose)"
.
iSpecialize
(
"Acc"
with
"P"
).
iDestruct
"Acc"
as
"[Q CB]"
.
iFrame
.
iIntros
"Q"
.
iApply
"Hclose"
.
now
iApply
"CB"
.
Qed
.
Lemma
inv_iff
N
P
Q
:
▷
□
(
P
↔
Q
)
-
∗
inv
N
P
-
∗
inv
N
Q
.
Proof
.
iIntros
"#HPQ #I"
.
iApply
(
inv_acc
with
"I"
).
iNext
.
iIntros
"!# P"
.
iSplitL
"P"
.
-
by
iApply
"HPQ"
.
-
iIntros
"Q"
.
by
iApply
"HPQ"
.
Qed
.
Lemma
inv_to_inv
M
P
:
internal_inv
M
P
-
∗
inv
M
P
.
Proof
.
iIntros
"#I"
.
rewrite
inv_eq
.
iIntros
(
E
H
).
iPoseProof
(
internal_inv_open
with
"I"
)
as
"H"
;
eauto
.
Qed
.
Lemma
inv_alloc
N
E
P
:
▷
P
={
E
}=
∗
inv
N
P
.
Proof
.
iIntros
"P"
.
iPoseProof
(
internal_inv_alloc
N
E
with
"P"
)
as
"I"
.
iApply
fupd_mono
;
last
eauto
.
iApply
inv_to_inv
.
Qed
.
Lemma
inv_alloc_open
N
E
P
:
↑
N
⊆
E
→
(|={
E
,
E
∖↑
N
}=>
inv
N
P
∗
(
▷
P
={
E
∖↑
N
,
E
}=
∗
True
))%
I
.
Proof
.
iIntros
(
H
).
iPoseProof
(
internal_inv_alloc_open
_
_
_
H
)
as
"H"
.
iApply
fupd_mono
;
last
eauto
.
iIntros
"[I H]"
;
iFrame
;
by
iApply
inv_to_inv
.
Qed
.
Lemma
inv_open
E
N
P
:
↑
N
⊆
E
→
inv
N
P
={
E
,
E
∖↑
N
}=
∗
▷
P
∗
(
▷
P
={
E
∖↑
N
,
E
}=
∗
True
).
Proof
.
rewrite
inv_eq
/
inv_def
;
iIntros
(
H
)
"#I"
.
by
iApply
"I"
.
Qed
.
Lemma
inv_open_strong
E
N
P
:
↑
N
⊆
E
→
inv
N
P
={
E
,
E
∖↑
N
}=
∗
▷
P
∗
∀
E'
,
▷
P
={
E'
,
↑
N
∪
E'
}=
∗
True
.
Proof
.
iIntros
(?)
"Hinv"
.
iPoseProof
(
inv_open
(
↑
N
)
N
P
with
"Hinv"
)
as
"H"
;
first
done
.
rewrite
difference_diag_L
.
iPoseProof
(
fupd_mask_frame_r
_
_
(
E
∖
↑
N
)
with
"H"
)
as
"H"
;
first
set_solver
.
rewrite
left_id_L
-
union_difference_L
//.
iMod
"H"
as
"[$ H]"
;
iModIntro
.
iIntros
(
E'
)
"HP"
.
iPoseProof
(
fupd_mask_frame_r
_
_
E'
with
"(H HP)"
)
as
"H"
;
first
set_solver
.
by
rewrite
left_id_L
.
Qed
.
Global
Instance
into_inv_inv
N
P
:
IntoInv
(
inv
N
P
)
N
:
=
{}.
Global
Instance
into_acc_inv
N
P
E
:
IntoAcc
(
X
:
=
unit
)
(
inv
N
P
)
(
↑
N
⊆
E
)
True
(
fupd
E
(
E
∖
↑
N
))
(
fupd
(
E
∖
↑
N
)
E
)
(
λ
_
:
(),
(
▷
P
)%
I
)
(
λ
_
:
(),
(
▷
P
)%
I
)
(
λ
_
:
(),
None
).
Proof
.
rewrite
inv_eq
/
IntoAcc
/
accessor
bi
.
exist_unit
.
iIntros
(?)
"#Hinv _"
.
iApply
"Hinv"
;
done
.
Qed
.
Lemma
inv_open_timeless
E
N
P
`
{!
Timeless
P
}
:
↑
N
⊆
E
→
inv
N
P
={
E
,
E
∖↑
N
}=
∗
P
∗
(
P
={
E
∖↑
N
,
E
}=
∗
True
).
Proof
.
iIntros
(?)
"Hinv"
.
iMod
(
inv_open
with
"Hinv"
)
as
"[>HP Hclose]"
;
auto
.
iIntros
"!> {$HP} HP"
.
iApply
"Hclose"
;
auto
.
Qed
.
(* Weakening of semantic invariants *)
Lemma
inv_proj_l
N
P
Q
:
inv
N
(
P
∗
Q
)
-
∗
inv
N
P
.
Proof
.
iIntros
"#I"
.
iApply
inv_acc
;
eauto
.
iNext
.
iIntros
"!# [$ Q] P"
;
iFrame
.
Qed
.
Lemma
inv_proj_r
N
P
Q
:
inv
N
(
P
∗
Q
)
-
∗
inv
N
Q
.
Proof
.
rewrite
(
bi
.
sep_comm
P
Q
).
eapply
inv_proj_l
.
Qed
.
Lemma
inv_split
N
P
Q
:
inv
N
(
P
∗
Q
)
-
∗
inv
N
P
∗
inv
N
Q
.
Proof
.
iIntros
"#H"
.
iPoseProof
(
inv_proj_l
with
"H"
)
as
"$"
.
iPoseProof
(
inv_proj_r
with
"H"
)
as
"$"
.
Qed
.
End
inv
.
theories/logrel_heaplang/lib/vectors.v
View file @
c56b93ab
From
iris
.
heap_lang
Require
Export
lifting
metatheory
.
From
iris
.
base_logic
.
lib
Require
Import
invariants
.
From
iris
.
heap_lang
Require
Import
notation
proofmode
.
From
iris_examples
.
logrel_heaplang
Require
Import
ltyping
ltyping_safety
.
From
iris
.
algebra
Require
Import
gmap
auth
agree
.
From
iris_examples
.
logrel_heaplang
.
lib
Require
Import
arrays
.
From
iris_examples
.
logrel_heaplang
.
lib
Require
Import
invariants
arrays
.
Set
Default
Proof
Using
"Type"
.
Section
Vectors
.
(* vec = ref array *)
(* vec = ref array *)
(* API *)
Definition
use
:
val
:
=
...
...
@@ -20,17 +16,15 @@ Set Default Proof Using "Type".
let
:
"b"
:
=
copy
"a"
(!
"a"
)
in
let
:
"v"
:
=
ref
"b"
in
"f"
#()
"v"
.
Definition
idx
:
val
:
=
λ
:
<>
"v"
"i"
,
if
:
((#-
1
)
<
"i"
)
&&
(
"i"
<
!(!
"v"
))
then
SOME
"i"
else
NONE
.
Definition
get
:
val
:
=
λ
:
<>
"v"
"i"
,
unsafe_get
(!
"v"
)
"i"
.
Definition
set
:
val
:
=
λ
:
<>
"v"
"i"
"x"
,
(
unsafe_set
(!
"v"
)
"i"
)
"x"
.
Definition
app
:
val
:
=
λ
:
<>
,
rec
:
"f"
"v"
"x"
:
=
let
:
"a"
:
=
!
"v"
in
...
...
@@ -39,28 +33,34 @@ Set Default Proof Using "Type".
if
:
CAS
"v"
"a"
"b"
then
#()
else
"f"
"v"
"x"
.
(* History *)
Definition
Hist
:
=
gmap
loc
nat
.
Definition
HistUR
:
=
gmapUR
loc
(
agreeR
(
leibnizO
nat
)).
Definition
hist
:
Hist
→
HistUR
:
=
fmap
(
λ
v
:
nat
,
to_agree
(
v
:
leibnizO
nat
)).
Implicit
Types
(
h
:
Hist
)
(
a
:
loc
).
Context
`
{!
heapG
Σ
,
!
inG
Σ
(
authR
mnatUR
),
(* maximum length *)
!
inG
Σ
(
authR
(
gmapUR
loc
(
agreeR
(
leibnizC
nat
)))
)
(* history *)
!
inG
Σ
(
authR
HistUR
)
(* history *)
}.
(* Maximum Length *)
Global
Instance
auth_mnat_persistent
(
n
:
mnat
)
γ
:
Persistent
(
own
γ
(
◯
n
)).
Proof
.
eapply
own_core_persistent
,
auth_frag_core_id
,
mnat_core_id
.
eapply
own_core_persistent
,
auth_frag_core_id
,
mnat_core_id
.
Qed
.
Lemma
auth_mnat_alloc
(
n
:
mnat
)
:
(|==>
∃
γ
,
own
γ
(
●
n
)
∗
own
γ
(
◯
n
))%
I
.
Proof
.
iMod
(
own_alloc
(
●
n
⋅
◯
n
))
as
(
γ
)
"[??]"
.
eapply
auth_both_valid_2
;
done
.
eauto
with
iFrame
.
eauto
with
iFrame
.
Qed
.
Lemma
auth_mnat_agree
γ
(
m
n
:
mnat
)
:
own
γ
(
●
m
)
-
∗
own
γ
(
◯
n
)
-
∗
⌜
n
<=
m
⌝
.
Proof
.
iIntros
"Hγ● Hγ◯"
.
iIntros
"Hγ● Hγ◯"
.
iDestruct
(
own_valid_2
with
"Hγ● Hγ◯"
)
as
"%"
.
eapply
auth_both_valid
in
H
as
[
H
_
].
iPureIntro
.
eapply
mnat_included
in
H
.
lia
.
...
...
@@ -79,64 +79,59 @@ Set Default Proof Using "Type".
Proof
.
intros
H
.
eapply
own_mono
.
eapply
(
auth_frag_mono
n
m
),
mnat_included
.
lia
.
Qed
.
Lemma
auth_mnat_update
γ
(
n
p
:
mnat
)
:
n
<=
p
->
own
γ
(
●
n
)
==
∗
own
γ
(
●
p
).
Proof
.
iIntros
(
H
)
"Hγ●"
.
iMod
(
auth_mnat_fork
with
"Hγ●"
)
as
"[Hγ● Hγ◯]"
;
eauto
.
iMod
(
auth_mnat_fork
with
"Hγ●"
)
as
"[Hγ● Hγ◯]"
;
eauto
.
iMod
(
own_update_2
_
_
_
(
●
p
⋅
◯
p
)
with
"Hγ● Hγ◯"
)
as
"[$ _]"
;
eauto
.
eapply
auth_update
,
mnat_local_update
;
lia
.
Qed
.
(* History *)
Definition
Hist
:
=
gmap
loc
nat
.
Definition
HistUR
:
=
gmapUR
loc
(
agreeR
(
leibnizC
nat
)).
Definition
hist
:
Hist
->
HistUR
:
=
fmap
(
λ
v
,
to_agree
(
v
:
leibnizC
nat
)).
Implicit
Types
(
h
:
Hist
)
(
a
:
loc
).
Section
hist
.
(** Conversion to hists and back *)
Lemma
hist_valid
h
:
✓
hist
h
.
Proof
.
intros
l
.
rewrite
lookup_fmap
.
by
case
(
h
!!
l
).
Qed
.
Lemma
lookup_hist_None
h
a
:
h
!!
a
=
None
→
hist
h
!!
a
=
None
.
Proof
.
by
rewrite
/
hist
lookup_fmap
=>
->.
Qed
.
Lemma
hist_singleton_included
h
a
m
:
{[
a
:
=
to_agree
m
]}
≼
hist
h
→
h
!!
a
=
Some
m
.
Proof
.
rewrite
singleton_included
=>
-[
a'
[]].
rewrite
/
hist
lookup_fmap
fmap_Some_equiv
=>
-[
m'
[->
H
]].
rewrite
H
.
rewrite
/
hist
lookup_fmap
fmap_Some_equiv
=>
-[
m'
[->
H
]].
rewrite
H
.
move
=>
/
Some_included_total
/
to_agree_included
/
leibniz_equiv_iff
->
//.
Qed
.
Lemma
hist_insert
h
a
m
:
hist
(<[
a
:
=
m
]>
h
)
=
<[
a
:
=
to_agree
(
m
:
leibniz
C
nat
)]>
(
hist
h
).
hist
(<[
a
:
=
m
]>
h
)
=
<[
a
:
=
to_agree
(
m
:
leibniz
O
nat
)]>
(
hist
h
).
Proof
.
by
rewrite
/
hist
fmap_insert
.
Qed
.
Lemma
hist_delete
a
h
:
hist
(
delete
a
h
)
=
delete
a
(
hist
h
).
Proof
.
by
rewrite
/
hist
fmap_delete
.
Qed
.
End
hist
.
Definition
hist_all
γ
h
:
iProp
Σ
:
=
(
own
γ
(
●
(
hist
h
)))%
I
.
Definition
hist_all
γ
h
:
iProp
Σ
:
=
(
own
γ
(
●
(
hist
h
)))%
I
.
Definition
hist_entry
γ
a
m
:
iProp
Σ
:
=
(
own
γ
(
◯
{[
a
:
=
to_agree
(
m
:
leibniz
C
nat
)]}))%
I
.
(
own
γ
(
◯
{[
a
:
=
to_agree
(
m
:
leibniz
O
nat
)]}))%
I
.
Global
Instance
hist_persistent
a
m
γ
:
Persistent
(
hist_entry
γ
a
m
).
Proof
.
eapply
_
.
Qed
.
Lemma
hist_alloc
:
(|==>
∃
γ
,
hist_all
γ
∅
)%
I
.
Proof
.
iMod
(
own_alloc
(
●
(
hist
∅
)))
as
(
γ
)
"H"
.
eapply
auth_auth_valid
,
hist_valid
.
eapply
auth_auth_valid
,
hist_valid
.
eauto
with
iFrame
.
Qed
.
Lemma
hist_update
γ
h
a
m
:
(
h
!!
a
=
None
)
->
hist_all
γ
h
==
∗
hist_all
γ
(<[
a
:
=
m
]>
h
)
∗
hist_entry
γ
a
m
.
...
...
@@ -156,7 +151,7 @@ Set Default Proof Using "Type".
f_equiv
.
rewrite
auth_frag_valid
/=.
rewrite
op_singleton
singleton_valid
.
by
intros
?%
agree_op_invL'
.
Qed
.
Lemma
hist_agree
γ
h
a
m
:
hist_all
γ
h
-
∗
hist_entry
γ
a
m
-
∗
⌜
h
!!
a
=
Some
m
⌝
.
Proof
.
...
...
@@ -167,11 +162,11 @@ Set Default Proof Using "Type".
Qed
.
Variable
(
N
:
namespace
).
Definition
Vec_inv
γ
1
γ
2
(
l
:
loc
)
:
iProp
Σ
:
=
(
∃
(
h
:
Hist
)
(
a
:
loc
)
(
m
:
mnat
),
l
↦
#
a
∗
...
...
@@ -185,18 +180,17 @@ Set Default Proof Using "Type".
Lemma
Vec_project_array
γ
1
γ
2
a
m
l
:
hist_entry
γ
2
a
m
-
∗
Vec
γ
1
γ
2
l
-
∗
I
nv
N
(
array
m
a
).
hist_entry
γ
2
a
m
-
∗
Vec
γ
1
γ
2
l
-
∗
i
nv
N
(
array
m
a
).
Proof
.
iIntros
"#E #V"
.
iPoseProof
(
inv_to_Inv
with
"V"
)
as
"Vec"
.
iApply
Inv_acc
;
eauto
.
iModIntro
.
iDestruct
1
as
(
h
b
n
)
"(Hl & Hγ1● & Hγ2● & Hγ2◯ & Hst)"
.
iIntros
"#E #V"
.
iApply
inv_acc
;
eauto
.
iNext
.
iModIntro
.
iDestruct
1
as
(
h
b
n
)
"(Hl & Hγ1● & Hγ2● & Hγ2◯ & Hst)"
.
iAssert
(
⌜
h
!!
a
=
Some
m
⌝
)%
I
with
"[Hγ2●]"
as
"#H"
.
{
iApply
(
hist_agree
with
"[Hγ2●]"
)
;
eauto
.
}
iAssert
((
array
m
a
∗
(
array
m
a
-
∗
[
∗
map
]
a
↦
m
∈
h
,
array
(
Z
.
of_nat
m
)
a
)))%
I
with
"[Hst]"
as
"(Ha & Hst)"
.
{
iDestruct
"H"
as
%
H1
.
now
iApply
(
big_sepM_lookup_acc
with
"Hst"
).
}
iFrame
.
iIntros
"Ha"
.
iFrame
.
iIntros
"Ha"
.
iExists
h
,
b
,
n
.
iFrame
.
now
iApply
"Hst"
.
Qed
.
...
...
@@ -204,31 +198,31 @@ Set Default Proof Using "Type".
(* Function Verification *)
Definition
ι
γ
1
γ
2
:
val
:
=
PairV
(#(
Z
.
pos
γ
1
))
(#(
Z
.
pos
γ
2
)).
Definition
β
γ
1
γ
2
:
lty
Σ
:
=
Lty
(
fun
v
=>
⌜
v
=
ι
γ
1
γ
2
⌝
)%
I
.
Definition
Index
(
S
:
lty
Σ
)
:
lty
Σ
:
=
Lty
(
fun
v
=>
(
□
∃
γ
1
γ
2
(
i
:
mnat
),
(
∀
v
,
S
v
∗
-
∗
β
γ
1
γ
2
v
)
∗
⌜
v
=
#
i
⌝
∗
Idx
γ
1
i
)%
I
).
Definition
Vector
(
S
:
lty
Σ
)
:
lty
Σ
:
=
Lty
(
fun
v
=>
(
□
∃
γ
1
γ
2
(
l
:
loc
),
(
∀
v
,
S
v
∗
-
∗
β
γ
1
γ
2
v
)
∗
⌜
v
=
#
l
⌝
∗
Vec
γ
1
γ
2
l
)%
I
).
Lemma
typing_use
:
∅
⊨
use
:
∀
T
,
Array
N
→
(
∀
S
,
Vector
S
→
T
)
→
T
.
Proof
.
unfold
use
.
iIntros
(
s
)
"!# #T /="
.
Proof
.
unfold
use
.
iIntros
(
s
)
"!# #T /="
.
iApply
wp_value
.
iIntros
(
S
)
"!#"
.
wp_pures
.
iIntros
(
S
)
"!#"
.
wp_pures
.
iIntros
(
v1
)
"!# #Array"
.
wp_pures
.
iIntros
(
v2
)
"!# #Cont"
.
wp_pures
.
iDestruct
"Array"
as
(
a
m
)
"[Array ->]"
.
wp_bind
(!
#
a
)%
E
.
iInv
"
Array"
as
"[Ha Hl]"
"Hclose"
.
wp_load
.
iMod
(
"Hclose"
with
"[$Ha $Hl]
"
)
as
"_"
.
iDestruct
"Array"
as
(
a
m
)
"[Array ->]"
.
wp_bind
(!
#
a
)%
E
.
iPoseProof
(
array_length_inv
with
"Array"
)
as
"L"
.
iInv
"
L"
as
"Ha"
"Hclose"
.
wp_load
.
iMod
(
"Hclose"
with
"Ha
"
)
as
"_"
.
iModIntro
.
wp_apply
(
copy_spec
)
;
eauto
with
lia
.
iIntros
(
b
)
"B"
.
wp_pures
.
wp_bind
(
ref
_
)%
E
.
wp_apply
wp_fupd
.
wp_alloc
l
as
"Hl"
.
iMod
(
auth_mnat_alloc
m
)
as
(
γ
1
)
"[Hγ1● _]"
.
iMod
(
hist_alloc
)
as
(
γ
2
)
"Hγ2●"
.
iMod
(
hist_update
γ
2
∅
b
m
with
"[Hγ2●]"
)
as
"[Hγ2● #Hγ2◯]"
;
eauto
.
iMod
(
hist_update
γ
2
∅
b
m
with
"[Hγ2●]"
)
as
"[Hγ2● #Hγ2◯]"
;
eauto
.
iMod
(
inv_alloc
N
_
(
Vec_inv
γ
1
γ
2
l
)
with
"[Hγ1● Hγ2● Hl B]"
)
as
"#I"
.
-
iNext
.
iExists
{[
b
:
=
m
]},
b
,
m
.
iFrame
.
iSplit
;
eauto
.
now
rewrite
big_sepM_singleton
.
...
...
@@ -239,14 +233,14 @@ Set Default Proof Using "Type".
Qed
.
Lemma
typing_idx
:
∅
⊨
idx
:
(
∀
S
,
Vector
S
→
lty_int
→
Option
(
Index
S
)).
Proof
.
unfold
idx
.
iIntros
(
s
)
"!# T /="
.
iApply
wp_value
.
iIntros
(
S
)
"!#"
.
wp_pures
.
iIntros
(
v1
)
"!# #Vec"
.
wp_pures
.
iIntros
(
v1
)
"!# #Vec"
.
wp_pures
.
iIntros
(
v2
)
"!# #Int"
.
wp_pures
.
iDestruct
"Vec"
as
(
γ
1
γ
2
l
)
"(EQ & -> & V)"
.
iDestruct
"Vec"
as
(
γ
1
γ
2
l
)
"(EQ & -> & V)"
.
iDestruct
"Int"
as
(
n
)
"->"
.
wp_pures
.
bool_decide
H
;
last
(
wp_pures
;
now
iLeft
).
wp_pures
.
wp_bind
(!
#
l
)%
E
.
iInv
"V"
as
(
h
a
m
)
"(H1 & H2 & H3 & #Ha & H4)"
"Hclose"
.
...
...
@@ -254,14 +248,15 @@ Set Default Proof Using "Type".
iMod
(
"Hclose"
with
"[H1 H2 H3 H4]"
)
as
"_"
.
iNext
;
iExists
h
,
a
,
m
;
iFrame
;
eauto
.
iModIntro
.
iPoseProof
(
Vec_project_array
with
"Ha V"
)
as
"I"
.
wp_bind
(!
_
)%
E
.
iInv
"I"
as
"[Hb Aa]"
"Hclose"
.
wp_load
.
iMod
(
"Hclose"
with
"[$Hb $Aa]"
)
as
"_"
.
iModIntro
.
wp_pures
.
wp_bind
(!
_
)%
E
.
iPoseProof
(
array_length_inv
with
"I"
)
as
"L"
.
iInv
"L"
as
"H"
"Hclose"
.
wp_load
.
iMod
(
"Hclose"
with
"H"
)
as
"_"
.
iModIntro
.
wp_pures
.
bool_decide
H'
;
last
(
wp_pures
;
now
iLeft
).
wp_pures
.
iRight
.
iExists
#
n
.
iSplit
;
eauto
.
destruct
(
Z_to_nat
n
)
as
[
k
->]
;
first
lia
.
iExists
γ
1
,
γ
2
,
k
.
iModIntro
.
repeat
iSplit
;
eauto
.
iApply
auth_mnat_previous
;
eauto
.
lia
.
iApply
auth_mnat_previous
;
eauto
.
lia
.
Qed
.
...
...
@@ -269,97 +264,94 @@ Set Default Proof Using "Type".
Proof
.
unfold
get
.
iIntros
(
s
)
"!# T /="
.
iApply
wp_value
.
iIntros
(
S
)
"!#"
.
wp_pures
.
iIntros
(
v1
)
"!# #Vec"
.
wp_pures
.
iIntros
(
v1
)
"!# #Vec"
.
wp_pures
.
iIntros
(
v2
)
"!# #Idx"
.
wp_pures
.
iDestruct
"Vec"
as
(
γ
1
γ
2
l
)
"(EQ & -> & V)"
.
iDestruct
"Vec"
as
(
γ
1
γ
2
l
)
"(EQ & -> & V)"
.
iDestruct
"Idx"
as
(
γ
1
'
γ
2
'
i
)
"(EQ' & -> & I)"
.
iAssert
(
β
γ
1
γ
2
(
ι
γ
1
'
γ
2
'
))%
I
as
"%"
.
{
iApply
"EQ"
.
iApply
"EQ'"
.
now
iPureIntro
.
}
injection
H
as
->
->.
injection
H
as
->
->.
wp_bind
(!
_
)%
E
.
iInv
"V"
as
(
h
a
m
)
"(H1 & H2 & H3 & #Ha & H4)"
"Hclose"
.
wp_load
.
iDestruct
(
auth_mnat_agree
with
"H2 I"
)
as
%
H
.
iMod
(
"Hclose"
with
"[H1 H2 H3 H4]"
)
as
"_"
.
iMod
(
"Hclose"
with
"[H1 H2 H3 H4]"
)
as
"_"
.
iNext
;
iExists
h
,
a
,
m
;
iFrame
;
eauto
.
iModIntro
.
wp_apply
(
unsafe_get_spec
)
;
eauto
.
iSplit
.
iApply
Vec_project_array
;
eauto
.
iPureIntro
;
lia
.
iApply
Vec_project_array
;
eauto
.
iPureIntro
;
lia
.
Qed
.
Lemma
typing_set
:
∅
⊨
set
:
(
∀
S
,
Vector
S
→
Index
S
→
lty_int
→
lty_unit
).
Proof
.
unfold
set
.
iIntros
(
s
)
"!# T /="
.
iApply
wp_value
.
iIntros
(
S
)
"!#"
.
wp_pures
.
iIntros
(
v1
)
"!# #Vec"
.
wp_pures
.
iIntros
(
v1
)
"!# #Vec"
.
wp_pures
.
iIntros
(
v2
)
"!# #Idx"
.
wp_pures
.
iIntros
(
v3
)
"!# #Int"
.
wp_pures
.
iDestruct
"Vec"
as
(
γ
1
γ
2
l
)
"(EQ & -> & V)"
.
iIntros
(
v3
)
"!# #Int"
.
wp_pures
.
iDestruct
"Vec"
as
(
γ
1
γ
2
l
)
"(EQ & -> & V)"
.
iDestruct
"Idx"
as
(
γ
1
'
γ
2
'
i
)
"(EQ' & -> & I)"
.
iDestruct
"Int"
as
(
n
)
"->"
.
iAssert
(
β
γ
1
γ
2
(
ι
γ
1
'
γ
2
'
))%
I
as
"%"
.
{
iApply
"EQ"
.
iApply
"EQ'"
.
now
iPureIntro
.
}
injection
H
as
->
->.
injection
H
as
->
->.
wp_bind
(!
_
)%
E
.
iInv
"V"
as
(
h
a
m
)
"(H1 & H2 & H3 & #Ha & H4)"
"Hclose"
.
wp_load
.
iDestruct
(
auth_mnat_agree
with
"H2 I"
)
as
%
H
.
iMod
(
"Hclose"
with
"[H1 H2 H3 H4]"
)
as
"_"
.
iMod
(
"Hclose"
with
"[H1 H2 H3 H4]"
)
as
"_"
.
iNext
;
iExists
h
,
a
,
m
;
iFrame
;
eauto
.
iModIntro
.
wp_apply
(
unsafe_set_spec
)
;
eauto
.
iSplit
.
iApply
Vec_project_array
;
eauto
.
iPureIntro
;
lia
.
iApply
Vec_project_array
;
eauto
.
iPureIntro
;
lia
.
Qed
.
Lemma
typing_app
:
∅
⊨
app
:
(
∀
S
,
Vector
S
→
lty_int
→
lty_unit
).
Proof
.
iIntros
(
s
)
"!# #T /="
.
unfold
app
.
unfold
app
.
iApply
wp_value
.
iIntros
(
S
)
"!#"
.
wp_pures
.
iIntros
(
v1
)
"!# #Vec"
.
wp_pures
.
iIntros
(
v1
)
"!# #Vec"
.
wp_pures
.
iIntros
(
v2
)
"!# #Int"
.
wp_pures
.
fold
app
.
iL
ö
b
as
"IH"
forall
(
v1
v2
)
"Vec Int"
.
iDestruct
"Vec"
as
(
γ
1
γ
2
l
)
"(EQ & -> & Vec)"
.
iDestruct
"Vec"
as
(
γ
1
γ
2
l
)
"(EQ & -> & Vec)"
.
iDestruct
"Int"
as
(
n
)
"->"
.
wp_bind
(!
#
l
)%
E
.
iInv
"Vec"
as
(
h
a
m
)
"(Hl & Hγ1● & Hγ2 & #Ha & Hst)"
"Hclose"
.
wp_load
.