Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
Iris
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Wiki
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Build
Pipelines
Jobs
Pipeline schedules
Artifacts
Deploy
Releases
Package registry
Model registry
Operate
Terraform modules
Monitor
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
William Mansky
Iris
Commits
a983ad09
Commit
a983ad09
authored
9 years ago
by
Ralf Jung
Browse files
Options
Downloads
Patches
Plain Diff
turn STSs into a record
parent
48d0c51a
No related branches found
Branches containing commit
No related tags found
Tags containing commit
No related merge requests found
Changes
2
Hide whitespace changes
Inline
Side-by-side
Showing
2 changed files
algebra/sts.v
+94
-63
94 additions, 63 deletions
algebra/sts.v
program_logic/sts.v
+51
-54
51 additions, 54 deletions
program_logic/sts.v
with
145 additions
and
117 deletions
algebra/sts.v
+
94
−
63
View file @
a983ad09
...
...
@@ -5,31 +5,47 @@ Local Arguments valid _ _ !_ /.
Local
Arguments
op
_
_
!
_
!
_
/.
Local
Arguments
unit
_
_
!
_
/.
Inductive
sts
{
A
B
}
(
R
:
relation
A
)
(
tok
:
A
→
set
B
)
:=
|
auth
:
A
→
set
B
→
sts
R
tok
|
frag
:
set
A
→
set
B
→
sts
R
tok
.
Arguments
auth
{_
_
_
_}
_
_
.
Arguments
frag
{_
_
_
_}
_
_
.
Module
sts
.
Record
Sts
:=
{
state
:
Type
;
token
:
Type
;
trans
:
relation
state
;
tok
:
state
→
set
token
;
}
.
(* The type of bounds we can give to the state of an STS. This is the type
that we equip with an RA structure. *)
Inductive
bound
(
sts
:
Sts
)
:=
|
bound_auth
:
state
sts
→
set
(
token
sts
)
→
bound
sts
|
bound_frag
:
set
(
state
sts
)
→
set
(
token
sts
)
→
bound
sts
.
Arguments
bound_auth
{_}
_
_
.
Arguments
bound_frag
{_}
_
_
.
Section
sts_core
.
Context
{
A
B
:
Type
}
(
R
:
relation
A
)
(
tok
:
A
→
set
B
)
.
Context
(
sts
:
Sts
)
.
Infix
"≼"
:=
dra_included
.
Inductive
sts_equiv
:
Equiv
(
sts
R
tok
)
:=
|
auth_equiv
s
T1
T2
:
T1
≡
T2
→
auth
s
T1
≡
auth
s
T2
|
frag_equiv
S1
S2
T1
T2
:
T1
≡
T2
→
S1
≡
S2
→
frag
S1
T1
≡
frag
S2
T2
.
Global
Existing
Instance
sts_equiv
.
Inductive
step
:
relation
(
A
*
set
B
)
:=
Notation
state
:=
(
state
sts
)
.
Notation
token
:=
(
token
sts
)
.
Notation
trans
:=
(
trans
sts
)
.
Notation
tok
:=
(
tok
sts
)
.
Inductive
equiv
:
Equiv
(
bound
sts
)
:=
|
auth_equiv
s
T1
T2
:
T1
≡
T2
→
bound_auth
s
T1
≡
bound_auth
s
T2
|
frag_equiv
S1
S2
T1
T2
:
T1
≡
T2
→
S1
≡
S2
→
bound_frag
S1
T1
≡
bound_frag
S2
T2
.
Global
Existing
Instance
equiv
.
Inductive
step
:
relation
(
state
*
set
token
)
:=
|
Step
s1
s2
T1
T2
:
R
s1
s2
→
tok
s1
∩
T1
≡
∅
→
tok
s2
∩
T2
≡
∅
→
tok
s1
∪
T1
≡
tok
s2
∪
T2
→
step
(
s1
,
T1
)
(
s2
,
T2
)
.
trans
s1
s2
→
tok
s1
∩
T1
≡
∅
→
tok
s2
∩
T2
≡
∅
→
tok
s1
∪
T1
≡
tok
s2
∪
T2
→
step
(
s1
,
T1
)
(
s2
,
T2
)
.
Hint
Resolve
Step
.
Inductive
frame_step
(
T
:
set
B
)
(
s1
s2
:
A
)
:
Prop
:=
Inductive
frame_step
(
T
:
set
token
)
(
s1
s2
:
state
)
:
Prop
:=
|
Frame_step
T1
T2
:
T1
∩
(
tok
s1
∪
T
)
≡
∅
→
step
(
s1
,
T1
)
(
s2
,
T2
)
→
frame_step
T
s1
s2
.
Hint
Resolve
Frame_step
.
Record
closed
(
S
:
set
A
)
(
T
:
set
B
)
:
Prop
:=
Closed
{
Record
closed
(
S
:
set
state
)
(
T
:
set
token
)
:
Prop
:=
Closed
{
closed_ne
:
S
≢
∅
;
closed_disjoint
s
:
s
∈
S
→
tok
s
∩
T
≡
∅
;
closed_step
s1
s2
:
s1
∈
S
→
frame_step
T
s1
s2
→
s2
∈
S
...
...
@@ -37,40 +53,50 @@ Record closed (S : set A) (T : set B) : Prop := Closed {
Lemma
closed_steps
S
T
s1
s2
:
closed
S
T
→
s1
∈
S
→
rtc
(
frame_step
T
)
s1
s2
→
s2
∈
S
.
Proof
.
induction
3
;
eauto
using
closed_step
.
Qed
.
Global
Instance
sts_valid
:
Valid
(
sts
R
tok
)
:=
λ
x
,
match
x
with
auth
s
T
=>
tok
s
∩
T
≡
∅
|
frag
S'
T
=>
closed
S'
T
end
.
Definition
up
(
s
:
A
)
(
T
:
set
B
)
:
set
A
:=
mkSet
(
rtc
(
frame_step
T
)
s
)
.
Definition
up_set
(
S
:
set
A
)
(
T
:
set
B
)
:
set
A
:=
S
≫=
λ
s
,
up
s
T
.
Global
Instance
sts_unit
:
Unit
(
sts
R
tok
)
:=
λ
x
,
Global
Instance
valid
:
Valid
(
bound
sts
)
:=
λ
x
,
match
x
with
|
frag
S'
_
=>
frag
(
up_set
S'
∅
)
∅
|
auth
s
_
=>
frag
(
up
s
∅
)
∅
|
bound_auth
s
T
=>
tok
s
∩
T
≡
∅
|
bound_frag
S'
T
=>
closed
S'
T
end
.
Inductive
sts_disjoint
:
Disjoint
(
sts
R
tok
)
:=
Definition
up
(
s
:
state
)
(
T
:
set
token
)
:
set
state
:=
mkSet
(
rtc
(
frame_step
T
)
s
)
.
Definition
up_set
(
S
:
set
state
)
(
T
:
set
token
)
:
set
state
:=
S
≫=
λ
s
,
up
s
T
.
Global
Instance
unit
:
Unit
(
bound
sts
)
:=
λ
x
,
match
x
with
|
bound_frag
S'
_
=>
bound_frag
(
up_set
S'
∅
)
∅
|
bound_auth
s
_
=>
bound_frag
(
up
s
∅
)
∅
end
.
Inductive
disjoint
:
Disjoint
(
bound
sts
)
:=
|
frag_frag_disjoint
S1
S2
T1
T2
:
S1
∩
S2
≢
∅
→
T1
∩
T2
≡
∅
→
frag
S1
T1
⊥
frag
S2
T2
|
auth_frag_disjoint
s
S
T1
T2
:
s
∈
S
→
T1
∩
T2
≡
∅
→
auth
s
T1
⊥
frag
S
T2
|
frag_auth_disjoint
s
S
T1
T2
:
s
∈
S
→
T1
∩
T2
≡
∅
→
frag
S
T1
⊥
auth
s
T2
.
Global
Existing
Instance
sts_disjoint
.
Global
Instance
sts_op
:
Op
(
sts
R
tok
)
:=
λ
x1
x2
,
S1
∩
S2
≢
∅
→
T1
∩
T2
≡
∅
→
bound_frag
S1
T1
⊥
bound_frag
S2
T2
|
auth_frag_disjoint
s
S
T1
T2
:
s
∈
S
→
T1
∩
T2
≡
∅
→
bound_auth
s
T1
⊥
bound_frag
S
T2
|
frag_auth_disjoint
s
S
T1
T2
:
s
∈
S
→
T1
∩
T2
≡
∅
→
bound_frag
S
T1
⊥
bound_auth
s
T2
.
Global
Existing
Instance
disjoint
.
Global
Instance
op
:
Op
(
bound
sts
)
:=
λ
x1
x2
,
match
x1
,
x2
with
|
frag
S1
T1
,
frag
S2
T2
=>
frag
(
S1
∩
S2
)
(
T1
∪
T2
)
|
auth
s
T1
,
frag
_
T2
=>
auth
s
(
T1
∪
T2
)
|
frag
_
T1
,
auth
s
T2
=>
auth
s
(
T1
∪
T2
)
|
auth
s
T1
,
auth
_
T2
=>
auth
s
(
T1
∪
T2
)
(* never happens *)
|
bound_frag
S1
T1
,
bound_frag
S2
T2
=>
bound_frag
(
S1
∩
S2
)
(
T1
∪
T2
)
|
bound_auth
s
T1
,
bound_frag
_
T2
=>
bound_auth
s
(
T1
∪
T2
)
|
bound_frag
_
T1
,
bound_auth
s
T2
=>
bound_auth
s
(
T1
∪
T2
)
|
bound_auth
s
T1
,
bound_auth
_
T2
=>
bound_auth
s
(
T1
∪
T2
)
(* never happens *)
end
.
Global
Instance
sts_
minus
:
Minus
(
sts
R
tok
)
:=
λ
x1
x2
,
Global
Instance
minus
:
Minus
(
bound
sts
)
:=
λ
x1
x2
,
match
x1
,
x2
with
|
frag
S1
T1
,
frag
S2
T2
=>
frag
(
up_set
S1
(
T1
∖
T2
))
(
T1
∖
T2
)
|
auth
s
T1
,
frag
_
T2
=>
auth
s
(
T1
∖
T2
)
|
frag
_
T2
,
auth
s
T1
=>
auth
s
(
T1
∖
T2
)
(* never happens *)
|
auth
s
T1
,
auth
_
T2
=>
frag
(
up
s
(
T1
∖
T2
))
(
T1
∖
T2
)
|
bound_frag
S1
T1
,
bound_frag
S2
T2
=>
bound_frag
(
up_set
S1
(
T1
∖
T2
))
(
T1
∖
T2
)
|
bound_auth
s
T1
,
bound_frag
_
T2
=>
bound_auth
s
(
T1
∖
T2
)
|
bound_frag
_
T2
,
bound_auth
s
T1
=>
bound_auth
s
(
T1
∖
T2
)
(* never happens *)
|
bound_auth
s
T1
,
bound_auth
_
T2
=>
bound_frag
(
up
s
(
T1
∖
T2
))
(
T1
∖
T2
)
end
.
Hint
Extern
10
(
equiv
(
A
:=
set
_)
_
_)
=>
solve_elem_of
:
sts
.
Hint
Extern
10
(
¬
(
equiv
(
A
:=
set
_)
_
_))
=>
solve_elem_of
:
sts
.
Hint
Extern
10
(
base
.
equiv
(
A
:=
set
_)
_
_)
=>
solve_elem_of
:
sts
.
Hint
Extern
10
(
¬
(
base
.
equiv
(
A
:=
set
_)
_
_))
=>
solve_elem_of
:
sts
.
Hint
Extern
10
(_
∈
_)
=>
solve_elem_of
:
sts
.
Hint
Extern
10
(_
⊆
_)
=>
solve_elem_of
:
sts
.
Instance
:
Equivalence
((
≡
)
:
relation
(
sts
R
tok
))
.
Instance
:
Equivalence
((
≡
)
:
relation
(
bound
sts
))
.
Proof
.
split
.
*
by
intros
[];
constructor
.
...
...
@@ -145,7 +171,7 @@ Proof.
unfold
up_set
;
rewrite
elem_of_bind
;
intros
(
s'
&
Hstep
&
?)
.
induction
Hstep
;
eauto
using
closed_step
.
Qed
.
Global
Instance
sts_
dra
:
DRA
(
sts
R
tok
)
.
Global
Instance
dra
:
DRA
(
bound
sts
)
.
Proof
.
split
.
*
apply
_
.
...
...
@@ -211,36 +237,38 @@ Proof.
*
solve_elem_of
-
Hstep
Hs1
Hs2
.
Qed
.
End
sts_core
.
End
sts
.
Section
stsRA
.
Context
{
A
B
:
Type
}
(
R
:
relation
A
)
(
tok
:
A
→
set
B
)
.
Context
(
sts
:
Sts
)
.
Canonical
Structure
stsRA
:=
validityRA
(
sts
R
tok
)
.
Definition
sts_auth
(
s
:
A
)
(
T
:
set
B
)
:
stsRA
:=
to_validity
(
auth
s
T
)
.
Definition
sts_frag
(
S
:
set
A
)
(
T
:
set
B
)
:
stsRA
:=
to_validity
(
frag
S
T
)
.
Canonical
Structure
RA
:=
validityRA
(
bound
sts
)
.
Definition
auth
(
s
:
state
sts
)
(
T
:
set
(
token
sts
))
:
RA
:=
to_validity
(
bound_auth
s
T
)
.
Definition
frag
(
S
:
set
(
state
sts
))
(
T
:
set
(
token
sts
))
:
RA
:=
to_validity
(
bound_frag
S
T
)
.
Lemma
sts_
update_auth
s1
s2
T1
T2
:
st
s
.
step
R
tok
(
s1
,
T1
)
(
s2
,
T2
)
→
sts_
auth
s1
T1
~~>
sts_
auth
s2
T2
.
Lemma
update_auth
s1
s2
T1
T2
:
st
ep
sts
(
s1
,
T1
)
(
s2
,
T2
)
→
auth
s1
T1
~~>
auth
s2
T2
.
Proof
.
intros
?;
apply
validity_update
;
inversion
3
as
[|?
S
?
Tf
|];
subst
.
destruct
(
sts
.
step_closed
R
tok
s1
s2
T1
T2
S
Tf
)
as
(?
&
?
&
?);
auto
.
destruct
(
step_closed
sts
s1
s2
T1
T2
S
Tf
)
as
(?
&
?
&
?);
auto
.
repeat
(
done
||
constructor
)
.
Qed
.
Lemma
sts_update_frag
S1
S2
(
T
:
set
B
)
:
S1
⊆
S2
→
sts
.
closed
R
tok
S2
T
→
sts_
frag
S1
T
~~>
sts_
frag
S2
T
.
Lemma
sts_update_frag
S1
S2
(
T
:
set
(
token
sts
)
)
:
S1
⊆
S2
→
closed
sts
S2
T
→
frag
S1
T
~~>
frag
S2
T
.
Proof
.
move
=>
HS
Hcl
.
eapply
validity_update
;
inversion
3
as
[|?
S
?
Tf
|];
subst
.
-
split
;
first
done
.
constructor
;
last
done
.
solve_elem_of
.
-
split
;
first
done
.
constructor
;
solve_elem_of
.
Qed
.
Lemma
sts_frag_included
S1
S2
T1
T2
:
sts
.
closed
R
tok
S2
T2
→
sts_frag
S1
T1
≼
sts_frag
S2
T2
↔
(
sts
.
closed
R
tok
S1
T1
∧
∃
Tf
,
T2
≡
T1
∪
Tf
∧
T1
∩
Tf
≡
∅
∧
S2
≡
(
S1
∩
sts
.
up_set
R
tok
S2
Tf
))
.
Lemma
frag_included
S1
S2
T1
T2
:
closed
sts
S2
T2
→
frag
S1
T1
≼
frag
S2
T2
↔
(
closed
sts
S1
T1
∧
∃
Tf
,
T2
≡
T1
∪
Tf
∧
T1
∩
Tf
≡
∅
∧
S2
≡
(
S1
∩
up_set
sts
S2
Tf
))
.
Proof
.
move
=>
Hcl2
.
split
.
-
intros
[
xf
EQ
]
.
destruct
xf
as
[
xf
vf
Hvf
]
.
destruct
xf
as
[
Sf
Tf
|
Sf
Tf
]
.
...
...
@@ -258,23 +286,26 @@ Proof.
destruct
Hscl
as
[
s'
[
Hsup
Hs'
]]
.
eapply
sts
.
closed_steps
;
last
(
hnf
in
Hsup
;
eexact
Hsup
);
first
done
.
solve_elem_of
+
HS
Hs'
.
-
intros
(
Hcl1
&
Tf
&
Htk
&
Hf
&
Hs
)
.
exists
(
sts_frag
(
sts
.
up_set
R
tok
S2
Tf
)
Tf
)
.
-
intros
(
Hcl1
&
Tf
&
Htk
&
Hf
&
Hs
)
.
exists
(
frag
(
up_set
sts
S2
Tf
)
Tf
)
.
split
;
first
split
;
simpl
;[|
done
|]
.
+
intros
_
.
split_ands
;
first
done
.
*
apply
sts
.
closed_up_set
;
last
by
eapply
sts
.
closed_ne
.
move
=>
s
Hs2
.
move
:(
sts
.
closed_disjoint
_
_
_
_
Hcl2
_
Hs2
)
.
move
=>
s
Hs2
.
move
:(
closed_disjoint
sts
_
_
Hcl2
_
Hs2
)
.
solve_elem_of
+
Htk
.
*
constructor
;
last
done
.
rewrite
-
Hs
.
by
eapply
sts
.
closed_ne
.
+
intros
_
.
constructor
;
[
solve_elem_of
+
Htk
|
done
]
.
Qed
.
Lemma
sts_
frag_included'
S1
S2
T
:
sts
.
closed
R
tok
S2
T
→
sts
.
closed
R
tok
S1
T
→
S2
≡
(
S1
∩
sts
.
up_set
R
tok
S2
∅
)
→
sts_
frag
S1
T
≼
sts_
frag
S2
T
.
Lemma
frag_included'
S1
S2
T
:
closed
sts
S2
T
→
closed
sts
S1
T
→
S2
≡
(
S1
∩
sts
.
up_set
sts
S2
∅
)
→
frag
S1
T
≼
frag
S2
T
.
Proof
.
intros
.
apply
sts_
frag_included
;
first
done
.
intros
.
apply
frag_included
;
first
done
.
split
;
first
done
.
exists
∅.
split_ands
;
done
||
solve_elem_of
+.
Qed
.
End
stsRA
.
End
sts
.
This diff is collapsed.
Click to expand it.
program_logic/sts.v
+
51
−
54
View file @
a983ad09
...
...
@@ -12,65 +12,62 @@ Module sts.
like you would use "auth_ctx" etc. *)
Export
algebra
.
sts
.
sts
.
Record
Sts
{
A
B
}
:=
{
st
:
relation
A
;
tok
:
A
→
set
B
;
}
.
Arguments
Sts
:
clear
implicits
.
Class
InG
Λ
Σ
(
i
:
gid
)
{
A
B
}
(
sts
:
Sts
A
B
)
:=
{
inG
:>
ghost_ownership
.
InG
Λ
Σ
i
(
stsRA
sts
.(
st
)
sts
.(
tok
));
inh
:>
Inhabited
A
;
Class
InG
Λ
Σ
(
i
:
gid
)
(
sts
:
Sts
)
:=
{
inG
:>
ghost_ownership
.
InG
Λ
Σ
i
(
sts
.
RA
sts
);
inh
:>
Inhabited
(
state
sts
);
}
.
Section
definitions
.
Context
{
Λ
Σ
A
B
}
(
i
:
gid
)
(
sts
:
Sts
A
B
)
`{
!
InG
Λ
Σ
i
sts
}
(
γ
:
gname
)
.
Definition
inv
(
φ
:
A
→
iPropG
Λ
Σ
)
:
iPropG
Λ
Σ
:=
(
∃
s
,
own
i
γ
(
sts_
auth
sts
.(
st
)
sts
.(
tok
)
s
∅
)
★
φ
s
)
%
I
.
Definition
states
(
S
:
set
A
)
(
T
:
set
B
)
:
iPropG
Λ
Σ
:=
own
i
γ
(
sts_
frag
sts
.(
st
)
sts
.(
tok
)
S
T
)
%
I
.
Definition
state
(
s
:
A
)
(
T
:
set
B
)
:
iPropG
Λ
Σ
:=
states
(
up
sts
.(
st
)
sts
.(
tok
)
s
T
)
T
.
Definition
ctx
(
N
:
namespace
)
(
φ
:
A
→
iPropG
Λ
Σ
)
:
iPropG
Λ
Σ
:=
Context
{
Λ
Σ
}
(
i
:
gid
)
(
sts
:
Sts
)
`{
!
InG
Λ
Σ
i
sts
}
(
γ
:
gname
)
.
Definition
inv
(
φ
:
state
sts
→
iPropG
Λ
Σ
)
:
iPropG
Λ
Σ
:=
(
∃
s
,
own
i
γ
(
auth
sts
s
∅
)
★
φ
s
)
%
I
.
Definition
in_
states
(
S
:
set
(
state
sts
))
(
T
:
set
(
token
sts
)
)
:
iPropG
Λ
Σ
:=
own
i
γ
(
frag
sts
S
T
)
%
I
.
Definition
in_
state
(
s
:
state
sts
)
(
T
:
set
(
token
sts
)
)
:
iPropG
Λ
Σ
:=
in_
states
(
up
sts
s
T
)
T
.
Definition
ctx
(
N
:
namespace
)
(
φ
:
state
sts
→
iPropG
Λ
Σ
)
:
iPropG
Λ
Σ
:=
invariants
.
inv
N
(
inv
φ
)
.
End
definitions
.
Instance
:
Params
(
@
inv
)
8
.
Instance
:
Params
(
@
states
)
8
.
Instance
:
Params
(
@
ctx
)
9
.
Instance
:
Params
(
@
inv
)
6
.
Instance
:
Params
(
@
in_states
)
6
.
Instance
:
Params
(
@
in_state
)
6
.
Instance
:
Params
(
@
ctx
)
7
.
Section
sts
.
Context
{
Λ
Σ
A
B
}
(
i
:
gid
)
(
sts
:
Sts
A
B
)
`{
!
InG
Λ
Σ
StsI
sts
}
.
Context
(
φ
:
A
→
iPropG
Λ
Σ
)
.
Context
{
Λ
Σ
}
(
i
:
gid
)
(
sts
:
Sts
)
`{
!
InG
Λ
Σ
StsI
sts
}
.
Context
(
φ
:
state
sts
→
iPropG
Λ
Σ
)
.
Implicit
Types
N
:
namespace
.
Implicit
Types
P
Q
R
:
iPropG
Λ
Σ
.
Implicit
Types
γ
:
gname
.
(* The same rule as implication does *not* hold, as could be shown using
sts_frag_included. *)
Lemma
states_weaken
E
γ
S1
S2
T
:
S1
⊆
S2
→
closed
sts
.(
st
)
sts
.(
tok
)
S2
T
→
states
StsI
sts
γ
S1
T
⊑
pvs
E
E
(
states
StsI
sts
γ
S2
T
)
.
Lemma
in_
states_weaken
E
γ
S1
S2
T
:
S1
⊆
S2
→
closed
sts
S2
T
→
in_
states
StsI
sts
γ
S1
T
⊑
pvs
E
E
(
in_
states
StsI
sts
γ
S2
T
)
.
Proof
.
rewrite
/
states
=>
Hs
Hcl
.
apply
own_update
,
sts_update_frag
;
done
.
rewrite
/
in_
states
=>
Hs
Hcl
.
apply
own_update
,
sts_update_frag
;
done
.
Qed
.
Lemma
state_states
E
γ
s
S
T
:
s
∈
S
→
closed
sts
.(
st
)
sts
.(
tok
)
S
T
→
state
StsI
sts
γ
s
T
⊑
pvs
E
E
(
states
StsI
sts
γ
S
T
)
.
Lemma
in_
state_states
E
γ
s
S
T
:
s
∈
S
→
closed
sts
S
T
→
in_
state
StsI
sts
γ
s
T
⊑
pvs
E
E
(
in_
states
StsI
sts
γ
S
T
)
.
Proof
.
move
=>
Hs
Hcl
.
apply
states_weaken
;
last
done
.
move
=>
s'
Hup
.
eapply
closed_steps
in
Hcl
;
last
(
hnf
in
Hup
;
eexact
Hup
);
done
.
move
=>
Hs
Hcl
.
apply
in_
states_weaken
;
last
done
.
move
=>
s'
Hup
.
eapply
closed_steps
in
Hcl
;
last
(
hnf
in
Hup
;
eexact
Hup
);
done
.
Qed
.
Lemma
alloc
N
s
:
φ
s
⊑
pvs
N
N
(
∃
γ
,
ctx
StsI
sts
γ
N
φ
∧
state
StsI
sts
γ
s
(
set_all
∖
sts
.(
tok
)
s
))
.
φ
s
⊑
pvs
N
N
(
∃
γ
,
ctx
StsI
sts
γ
N
φ
∧
in_state
StsI
sts
γ
s
(
set_all
∖
sts
.(
tok
)
s
))
.
Proof
.
eapply
sep_elim_True_r
.
{
eapply
(
own_alloc
StsI
(
sts_
auth
sts
.(
st
)
sts
.(
tok
)
s
(
set_all
∖
sts
.(
tok
)
s
))
N
)
.
{
eapply
(
own_alloc
StsI
(
auth
sts
s
(
set_all
∖
sts
.(
tok
)
s
))
N
)
.
apply
discrete_valid
=>
/=.
solve_elem_of
.
}
rewrite
pvs_frame_l
.
apply
pvs_strip_pvs
.
rewrite
sep_exist_l
.
apply
exist_elim
=>
γ
.
rewrite
-
(
exist_intro
γ
)
.
transitivity
(
▷
inv
StsI
sts
γ
φ
★
state
StsI
sts
γ
s
(
set_all
∖
sts
.(
tok
)
s
))
%
I
.
transitivity
(
▷
inv
StsI
sts
γ
φ
★
in_state
StsI
sts
γ
s
(
set_all
∖
sts
.(
tok
)
s
))
%
I
.
{
rewrite
/
inv
-
later_intro
-
(
exist_intro
s
)
.
rewrite
[(_
★
φ
_)
%
I
]
comm
-
assoc
.
apply
sep_mono
;
first
done
.
rewrite
-
own_op
.
apply
equiv_spec
,
own_proper
.
...
...
@@ -85,16 +82,16 @@ Section sts.
Qed
.
Lemma
opened
E
γ
S
T
:
(
▷
inv
StsI
sts
γ
φ
★
states
StsI
sts
γ
S
T
)
⊑
pvs
E
E
(
∃
s
,
■
(
s
∈
S
)
★
▷
φ
s
★
own
StsI
γ
(
sts_
auth
sts
.(
st
)
sts
.(
tok
)
s
T
))
.
(
▷
inv
StsI
sts
γ
φ
★
in_
states
StsI
sts
γ
S
T
)
⊑
pvs
E
E
(
∃
s
,
■
(
s
∈
S
)
★
▷
φ
s
★
own
StsI
γ
(
auth
sts
s
T
))
.
Proof
.
rewrite
/
inv
/
states
.
rewrite
later_exist
sep_exist_r
.
apply
exist_elim
=>
s
.
rewrite
/
inv
/
in_
states
later_exist
sep_exist_r
.
apply
exist_elim
=>
s
.
rewrite
later_sep
pvs_timeless
!
pvs_frame_r
.
apply
pvs_mono
.
rewrite
-
(
exist_intro
s
)
.
rewrite
[(_
★
▷
φ
_)
%
I
]
comm
-!
assoc
-
own_op
-
[(
▷
φ
_
★
_)
%
I
]
comm
.
rewrite
own_valid_l
discrete_validI
.
rewrite
-!
assoc
.
apply
const_elim_sep_l
=>
-
[_
[
Hcl
Hdisj
]]
.
simpl
in
Hdisj
,
Hcl
.
inversion_clear
Hdisj
.
rewrite
const_equiv
//
left_id
.
rewrite
-!
assoc
.
apply
const_elim_sep_l
=>
-
[_
[
Hcl
Hdisj
]]
.
simpl
in
Hdisj
,
Hcl
.
inversion_clear
Hdisj
.
rewrite
const_equiv
//
left_id
.
rewrite
comm
.
apply
sep_mono
;
first
done
.
apply
equiv_spec
,
own_proper
.
split
;
first
split
;
simpl
.
-
intros
Hdisj
.
split_ands
;
first
by
solve_elem_of
+.
...
...
@@ -105,22 +102,22 @@ Section sts.
Qed
.
Lemma
closing
E
γ
s
T
s'
T'
:
step
sts
.(
st
)
sts
.(
tok
)
(
s
,
T
)
(
s'
,
T'
)
→
(
▷
φ
s'
★
own
StsI
γ
(
sts_
auth
sts
.(
st
)
sts
.(
tok
)
s
T
))
⊑
pvs
E
E
(
▷
inv
StsI
sts
γ
φ
★
state
StsI
sts
γ
s'
T'
)
.
step
sts
(
s
,
T
)
(
s'
,
T'
)
→
(
▷
φ
s'
★
own
StsI
γ
(
auth
sts
s
T
))
⊑
pvs
E
E
(
▷
inv
StsI
sts
γ
φ
★
in_
state
StsI
sts
γ
s'
T'
)
.
Proof
.
intros
Hstep
.
rewrite
/
inv
/
states
-
(
exist_intro
s'
)
.
intros
Hstep
.
rewrite
/
inv
/
in_
states
-
(
exist_intro
s'
)
.
rewrite
later_sep
[(_
★
▷
φ
_)
%
I
]
comm
-
assoc
.
rewrite
-
pvs_frame_l
.
apply
sep_mono
;
first
done
.
rewrite
-
later_intro
.
rewrite
own_valid_l
discrete_validI
.
apply
const_elim_sep_l
=>
Hval
.
simpl
in
Hval
.
transitivity
(
pvs
E
E
(
own
StsI
γ
(
sts_
auth
sts
.(
st
)
sts
.(
tok
)
s'
T'
)))
.
{
by
apply
own_update
,
sts
_
update_auth
.
}
rewrite
own_valid_l
discrete_validI
.
apply
const_elim_sep_l
=>
Hval
.
simpl
in
Hval
.
transitivity
(
pvs
E
E
(
own
StsI
γ
(
auth
sts
s'
T'
)))
.
{
by
apply
own_update
,
sts
.
update_auth
.
}
apply
pvs_mono
.
rewrite
-
own_op
.
apply
equiv_spec
,
own_proper
.
split
;
first
split
;
simpl
.
-
intros
_
.
set
Tf
:=
set_all
∖
sts
.(
tok
)
s
∖
T
.
assert
(
closed
(
st
sts
)
(
tok
sts
)
(
up
sts
.(
st
)
sts
.(
tok
)
s
Tf
)
Tf
)
.
assert
(
closed
sts
(
up
sts
s
Tf
)
Tf
)
.
{
apply
closed_up
.
rewrite
/
Tf
.
solve_elem_of
+.
}
eapply
step_closed
;
[
done
..|
|]
.
+
apply
elem_of_up
.
...
...
@@ -136,11 +133,11 @@ Section sts.
Lemma
states_fsa
E
N
P
(
Q
:
V
→
iPropG
Λ
Σ
)
γ
S
T
:
fsaV
→
nclose
N
⊆
E
→
P
⊑
ctx
StsI
sts
γ
N
φ
→
P
⊑
(
states
StsI
sts
γ
S
T
★
∀
s
,
P
⊑
(
in_
states
StsI
sts
γ
S
T
★
∀
s
,
■
(
s
∈
S
)
★
▷
φ
s
-★
fsa
(
E
∖
nclose
N
)
(
λ
x
,
∃
s'
T'
,
■
(
step
sts
.(
st
)
sts
.(
tok
)
(
s
,
T
)
(
s'
,
T'
))
★
▷
φ
s'
★
(
state
StsI
sts
γ
s'
T'
-★
Q
x
)))
→
■
(
step
sts
(
s
,
T
)
(
s'
,
T'
))
★
▷
φ
s'
★
(
in_
state
StsI
sts
γ
s'
T'
-★
Q
x
)))
→
P
⊑
fsa
E
Q
.
Proof
.
rewrite
/
ctx
=>?
HN
Hinv
Hinner
.
...
...
@@ -165,11 +162,11 @@ Section sts.
Lemma
state_fsa
E
N
P
(
Q
:
V
→
iPropG
Λ
Σ
)
γ
s0
T
:
fsaV
→
nclose
N
⊆
E
→
P
⊑
ctx
StsI
sts
γ
N
φ
→
P
⊑
(
state
StsI
sts
γ
s0
T
★
∀
s
,
■
(
s
∈
up
sts
.(
st
)
sts
.(
tok
)
s0
T
)
★
▷
φ
s
-★
P
⊑
(
in_
state
StsI
sts
γ
s0
T
★
∀
s
,
■
(
s
∈
up
sts
s0
T
)
★
▷
φ
s
-★
fsa
(
E
∖
nclose
N
)
(
λ
x
,
∃
s'
T'
,
■
(
step
sts
.(
st
)
sts
.(
tok
)
(
s
,
T
)
(
s'
,
T'
))
★
▷
φ
s'
★
(
state
StsI
sts
γ
s'
T'
-★
Q
x
)))
→
■
(
step
sts
(
s
,
T
)
(
s'
,
T'
))
★
▷
φ
s'
★
(
in_
state
StsI
sts
γ
s'
T'
-★
Q
x
)))
→
P
⊑
fsa
E
Q
.
Proof
.
rewrite
{
1
}
/
state
.
apply
states_fsa
.
...
...
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