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
Iris
gpfsl
Commits
c5fa30a1
Commit
c5fa30a1
authored
Oct 18, 2021
by
Jaehwang Jung
Committed by
Hai Dang
Oct 18, 2021
Browse files
Prove stack history spec for Treiber stack
parent
cbc347da
Changes
8
Expand all
Hide whitespace changes
Inline
Side-by-side
_CoqProject
View file @
c5fa30a1
...
...
@@ -12,6 +12,7 @@ theories/lang/tactics.v
# CMRAs
theories/algebra/mono_list.v
theories/algebra/mono_list_list.v
theories/algebra/lat_auth.v
theories/algebra/to_agree.v
theories/algebra/lattice_cmra.v
...
...
@@ -105,6 +106,10 @@ theories/examples/gset_disj.v
## Event
theories/examples/event/event.v
theories/examples/event/ghost.v
## Event History
theories/examples/history/history.v
theories/examples/history/ghost.v
theories/examples/history/spec.v
## Event Graph
theories/examples/graph/map_helper.v
theories/examples/graph/graph.v
...
...
@@ -130,12 +135,14 @@ theories/examples/stack/spec_na.v
theories/examples/stack/spec_per_elem.v
theories/examples/stack/event.v
theories/examples/stack/spec_graph.v
theories/examples/stack/spec_history.v
theories/examples/stack/code_na.v
theories/examples/stack/code_treiber.v
theories/examples/stack/code_elimination.v
theories/examples/stack/proof_na.v
theories/examples/stack/proof_treiber_gps.v
theories/examples/stack/proof_treiber_graph.v
theories/examples/stack/proof_treiber_history.v
theories/examples/stack/proof_mp_client.v
theories/examples/stack/proof_elim_graph.v
theories/examples/stack/proof_elim_graph_closed.v
...
...
theories/algebra/mono_list_list.v
0 → 100644
View file @
c5fa30a1
From
iris
.
algebra
Require
Export
auth
max_prefix_list
.
From
iris
.
algebra
Require
Import
updates
local_updates
proofmode_classes
.
From
iris
.
prelude
Require
Import
options
.
From
gpfsl
.
algebra
Require
Export
mono_list
.
(* TODO: upstream? *)
Lemma
map_relation_iff
`
{
∀
A
,
Lookup
K
A
(
M
A
)}
{
A
B
}
(
R1
R2
:
A
→
B
→
Prop
)
(
P1
P2
:
A
→
Prop
)
(
Q1
Q2
:
B
→
Prop
)
(
IffR
:
∀
a
b
,
R1
a
b
↔
R2
a
b
)
(
IffP
:
∀
a
,
P1
a
↔
P2
a
)
(
IffQ
:
∀
b
,
Q1
b
↔
Q2
b
)
(
m1
:
M
A
)
(
m2
:
M
B
)
:
map_relation
R1
P1
Q1
m1
m2
↔
map_relation
R2
P2
Q2
m1
m2
.
Proof
.
split
;
intros
REL
i
;
move
:
(
REL
i
)
;
destruct
(
m1
!!
i
),
(
m2
!!
i
)
;
simpl
;
naive_solver
.
Qed
.
(** List of [mono_listR] *)
Definition
max_prefix_list_list
(
A
:
Type
)
:
=
gmap
nat
(
max_prefix_list
A
).
Definition
max_prefix_list_listR
(
A
:
ofe
)
:
=
gmapR
nat
(
max_prefix_listUR
A
).
Definition
max_prefix_list_listUR
(
A
:
ofe
)
:
=
gmapUR
nat
(
max_prefix_listUR
A
).
Definition
to_max_prefix_list_list
{
A
}
(
l
:
list
(
list
A
))
:
max_prefix_list_list
A
:
=
to_max_prefix_list
<$>
map_seq
0
l
.
Global
Instance
:
Params
(@
to_max_prefix_list_list
)
1
:
=
{}.
Definition
prefixes
{
A
}
:
relation
(
list
(
list
A
))
:
=
map_included
prefix
.
Infix
"`prefixes_of`"
:
=
prefixes
(
at
level
70
)
:
stdpp_scope
.
Section
max_prefix_list_list
.
Context
{
A
:
ofe
}.
Implicit
Types
(
l
:
list
A
)
(
ll
:
list
(
list
A
)).
Global
Instance
to_max_prefix_list_list_ne
:
NonExpansive
(@
to_max_prefix_list_list
A
).
Proof
.
solve_proper
.
Qed
.
Global
Instance
to_max_prefix_list_list_proper
:
Proper
((
≡
)
==>
(
≡
))
(@
to_max_prefix_list_list
A
).
Proof
.
intros
???.
rewrite
/
to_max_prefix_list_list
!
fmap_map_seq
.
rewrite
map_seq_proper
;
[
done
|].
by
rewrite
(
list_fmap_proper
to_max_prefix_list
).
Qed
.
Global
Instance
to_max_prefix_list_list_dist_inj
n
:
Inj
(
dist
n
)
(
dist
n
)
(@
to_max_prefix_list_list
A
).
Proof
.
rewrite
/
to_max_prefix_list_list
.
intros
ll1
ll2
Hll
.
apply
list_dist_lookup
=>
i
.
move
:
(
Hll
i
).
rewrite
!
lookup_fmap
!
lookup_map_seq
Nat
.
sub_0_r
.
rewrite
!
option_guard_True
;
[|
lia
..].
case
El1
:
(
ll1
!!
i
)
=>
[
l1
|]
;
case
El2
:
(
ll2
!!
i
)
=>
[
l2
|]
;
inversion_clear
1
;
[|
done
].
f_equiv
.
by
apply
to_max_prefix_list_dist_inj
.
Qed
.
Global
Instance
to_max_prefix_list_list_inj
:
Inj
(
≡
)
(
≡
)
(@
to_max_prefix_list_list
A
).
Proof
.
intros
ll1
ll2
.
rewrite
!
equiv_dist
=>
?
n
.
by
apply
(
inj
to_max_prefix_list_list
).
Qed
.
Global
Instance
mono_list_lb_core_id
(
mll
:
max_prefix_list_list
A
)
:
CoreId
mll
:
=
_
.
Lemma
to_max_prefix_list_list_valid
ll
:
✓
to_max_prefix_list_list
ll
.
Proof
.
intros
i
.
rewrite
/
to_max_prefix_list_list
fmap_map_seq
lookup_map_seq
Nat
.
sub_0_r
list_lookup_fmap
.
rewrite
!
option_guard_True
;
[|
lia
..].
destruct
(
ll
!!
i
)
;
[|
done
].
simpl
.
apply
Some_valid
,
to_max_prefix_list_valid
.
Qed
.
Lemma
to_max_prefix_list_list_validN
n
ll
:
✓
{
n
}
to_max_prefix_list_list
ll
.
Proof
.
apply
cmra_valid_validN
,
to_max_prefix_list_list_valid
.
Qed
.
Lemma
to_max_prefix_list_list_op_l
ll1
ll2
:
ll1
`
prefixes_of
`
ll2
→
to_max_prefix_list_list
ll1
⋅
to_max_prefix_list_list
ll2
≡
to_max_prefix_list_list
ll2
.
Proof
.
rewrite
/
prefixes
/
map_included
/
map_relation
=>
H
i
.
rewrite
lookup_op
.
rewrite
/
to_max_prefix_list_list
!
fmap_map_seq
!
lookup_map_seq
Nat
.
sub_0_r
!
list_lookup_fmap
.
rewrite
!
option_guard_True
;
[|
lia
..].
move
:
(
H
i
).
case
El1
:
(
ll1
!!
i
)
=>
[
l1
|]
;
case
El2
:
(
ll2
!!
i
)
=>
[
l2
|]
;
inversion_clear
1
;
simplify_eq
/=.
-
rewrite
-
Some_op
.
rewrite
to_max_prefix_list_op_l
;
[
done
|
by
eexists
].
-
rewrite
left_id
//.
-
done
.
Qed
.
Lemma
to_max_prefix_list_list_op_r
ll1
ll2
:
ll1
`
prefixes_of
`
ll2
→
to_max_prefix_list_list
ll2
⋅
to_max_prefix_list_list
ll1
≡
to_max_prefix_list_list
ll2
.
Proof
.
rewrite
/
prefixes
/
map_included
/
map_relation
=>
H
i
.
rewrite
lookup_op
.
rewrite
/
to_max_prefix_list_list
!
fmap_map_seq
!
lookup_map_seq
Nat
.
sub_0_r
!
list_lookup_fmap
.
rewrite
!
option_guard_True
;
[|
lia
..].
move
:
(
H
i
).
case
El1
:
(
ll1
!!
i
)
=>
[
l1
|]
;
case
El2
:
(
ll2
!!
i
)
=>
[
l2
|]
;
inversion_clear
1
;
simplify_eq
/=.
-
rewrite
-
Some_op
.
rewrite
to_max_prefix_list_op_r
;
[
done
|
by
eexists
].
-
rewrite
right_id
//.
-
done
.
Qed
.
Lemma
max_prefix_list_list_included_includedN
(
mll1
mll2
:
max_prefix_list_list
A
)
:
mll1
≼
mll2
↔
∀
n
,
mll1
≼
{
n
}
mll2
.
Proof
.
split
;
[
intros
;
by
apply
:
cmra_included_includedN
|].
intros
Hincl
.
exists
mll2
.
apply
equiv_dist
=>
n
.
(* NOTE: [rewrite Hdist] fails. Maybe because it can't guess what [cmra] to
use for [cmra_op_ne]? But then how does [rewrite (Hdist i)] work?? *)
destruct
(
Hincl
n
)
as
[
mll
Hdist
].
intros
i
.
rewrite
lookup_op
(
Hdist
i
).
rewrite
lookup_op
assoc
-
core_id_dup
.
done
.
Qed
.
Local
Lemma
to_max_prefix_list_list_includedN_aux
n
ll1
ll2
:
to_max_prefix_list_list
ll1
≼
{
n
}
to_max_prefix_list_list
ll2
→
map_included
(
λ
l1
l2
,
l2
≡
{
n
}
≡
l1
++
drop
(
length
l1
)
l2
)
ll1
ll2
.
Proof
.
rewrite
lookup_includedN
=>
H
.
rewrite
/
map_included
/
map_relation
=>
i
.
move
:
{
H
}(
H
i
).
rewrite
/
to_max_prefix_list_list
!
fmap_map_seq
.
rewrite
option_includedN_total
=>
-[|].
-
move
=>/
lookup_map_seq_None
=>
-[|]
;
[
lia
|].
rewrite
fmap_length
/=.
move
=>/
lookup_ge_None_2
=>
->
/=.
by
case_match
.
-
move
=>
[?][?].
rewrite
!
lookup_map_seq_0
.
intros
((?
&
->
&
->)%
list_lookup_fmap_inv
&
(?
&
->
&
->)%
list_lookup_fmap_inv
&
?).
simpl
.
by
apply
max_prefix_list
.
to_max_prefix_list_includedN_aux
.
Qed
.
Lemma
to_max_prefix_list_list_includedN
n
ll1
ll2
:
to_max_prefix_list_list
ll1
≼
{
n
}
to_max_prefix_list_list
ll2
↔
map_included
(
λ
l1
l2
,
∃
l
,
l2
≡
{
n
}
≡
l1
++
l
)
ll1
ll2
.
Proof
.
split
.
-
intros
H
%
to_max_prefix_list_list_includedN_aux
i
.
move
:
{
H
}(
H
i
).
case
El1
:
(
ll1
!!
i
)
=>
[
l1
|]
;
case
El2
:
(
ll2
!!
i
)
=>
[
l2
|]
;
simpl
;
by
eauto
.
-
rewrite
lookup_includedN
=>
H
i
.
move
:
{
H
}(
H
i
).
rewrite
/
to_max_prefix_list_list
!
fmap_map_seq
!
lookup_map_seq_0
!
list_lookup_fmap
.
case
El1
:
(
ll1
!!
i
)
=>
[
l1
|]
;
case
El2
:
(
ll2
!!
i
)
=>
[
l2
|]
;
simpl
in
*
;
[|
done
|
|
done
]
;
intros
.
+
by
apply
Some_includedN_total
,
to_max_prefix_list_includedN
.
+
apply
option_includedN_total
.
by
left
.
Qed
.
Lemma
to_max_prefix_list_list_included
ll1
ll2
:
to_max_prefix_list_list
ll1
≼
to_max_prefix_list_list
ll2
↔
map_included
(
λ
l1
l2
,
∃
l
,
l2
≡
l1
++
l
)
ll1
ll2
.
Proof
.
split
.
-
intros
IN
i
.
have
{}
IN
:
∀
n
,
to_max_prefix_list_list
ll1
≼
{
n
}
to_max_prefix_list_list
ll2
.
{
intros
n
.
by
apply
:
cmra_included_includedN
.
(* NOTE: why does this work? *)
}
case
El1
:
(
ll1
!!
i
)
=>
[
l1
|]
;
case
El2
:
(
ll2
!!
i
)
=>
[
l2
|]
;
simpl
;
[
|
|
done
|
done
].
+
eexists
.
apply
equiv_dist
=>
n
.
specialize
(
IN
n
).
move
:
(
to_max_prefix_list_list_includedN_aux
n
ll1
ll2
IN
)
=>
INCL
.
move
:
(
INCL
i
).
rewrite
El1
El2
//.
+
move
:
{
IN
}(
IN
0
).
rewrite
lookup_includedN
=>
IN
.
move
:
{
IN
}(
IN
i
).
rewrite
/
to_max_prefix_list_list
!
fmap_map_seq
!
lookup_map_seq_0
!
list_lookup_fmap
.
rewrite
El1
El2
/=.
rewrite
option_includedN
.
naive_solver
.
-
rewrite
lookup_included
=>
IN
i
.
move
:
{
IN
}(
IN
i
).
rewrite
/
to_max_prefix_list_list
!
fmap_map_seq
!
lookup_map_seq_0
!
list_lookup_fmap
.
case
El1
:
(
ll1
!!
i
)
=>
[
l1
|]
;
case
El2
:
(
ll2
!!
i
)
=>
[
l2
|]
;
simpl
in
*
;
[
|
done
|
|
done
]
;
intros
.
+
by
apply
Some_included_total
,
to_max_prefix_list_included
.
+
apply
option_included_total
.
by
left
.
Qed
.
Lemma
to_max_prefix_list_list_included_L
`
{!
LeibnizEquiv
A
}
ll1
ll2
:
to_max_prefix_list_list
ll1
≼
to_max_prefix_list_list
ll2
↔
ll1
`
prefixes_of
`
ll2
.
Proof
.
rewrite
to_max_prefix_list_list_included
/
prefixes
/
prefix
.
rewrite
/
map_included
.
apply
map_relation_iff
;
naive_solver
.
Qed
.
Lemma
max_prefix_list_list_local_update
ll1
ll2
:
ll1
`
prefixes_of
`
ll2
→
(
to_max_prefix_list_list
ll1
,
to_max_prefix_list_list
ll1
)
~l
~>
(
to_max_prefix_list_list
ll2
,
to_max_prefix_list_list
ll2
).
Proof
.
intros
P
n
oll
V
EQ
.
simpl
in
*.
split
.
{
apply
to_max_prefix_list_list_validN
.
}
intros
i
.
move
:
{
P
}(
P
i
)
{
V
}(
V
i
)
{
EQ
}(
EQ
i
).
rewrite
!
lookup_opM
.
rewrite
/
to_max_prefix_list_list
!
fmap_map_seq
!
lookup_map_seq
Nat
.
sub_0_r
!
list_lookup_fmap
.
rewrite
!
option_guard_True
;
[|
lia
..].
destruct
oll
as
[
ll
|]
;
simpl
;
last
by
rewrite
!
right_id
.
destruct
(
ll
!!
i
)
as
[
l
|]
;
simpl
;
last
by
rewrite
!
right_id
.
destruct
(
ll1
!!
i
)
as
[
l1
|],
(
ll2
!!
i
)
as
[
l2
|]
;
simpl
;
[|
done
|
|
done
].
-
rewrite
-!
Some_op
.
intros
P
V
EQ
%
Some_dist_inj
.
f_equiv
.
move
:
(
max_prefix_list_local_update
l1
l2
P
n
(
Some
l
)).
naive_solver
.
-
rewrite
-!
Some_op
.
intros
_
_
EQ
.
symmetry
in
EQ
.
apply
dist_None
in
EQ
.
done
.
Qed
.
End
max_prefix_list_list
.
Definition
mono_list_listR
(
A
:
ofe
)
:
cmra
:
=
authR
(
max_prefix_list_listUR
A
).
Definition
mono_list_listUR
(
A
:
ofe
)
:
ucmra
:
=
authUR
(
max_prefix_list_listUR
A
).
Definition
mono_list_list_auth
{
A
:
ofe
}
(
l
:
list
(
list
A
))
:
mono_list_listR
A
:
=
●
(
to_max_prefix_list_list
l
)
⋅
◯
(
to_max_prefix_list_list
l
).
Definition
mono_list_list_lb
{
A
:
ofe
}
(
l
:
list
(
list
A
))
:
mono_list_listR
A
:
=
◯
(
to_max_prefix_list_list
l
).
Global
Instance
:
Params
(@
mono_list_list_auth
)
1
:
=
{}.
Global
Instance
:
Params
(@
mono_list_list_lb
)
1
:
=
{}.
Typeclasses
Opaque
mono_list_list_auth
mono_list_list_lb
.
Notation
"●MLL l"
:
=
(
mono_list_list_auth
l
)
(
at
level
20
).
Notation
"◯MLL l"
:
=
(
mono_list_list_lb
l
)
(
at
level
20
).
Section
mono_list_list
.
Context
{
A
:
ofe
}.
Implicit
Types
(
l
:
list
A
)
(
ll
:
list
(
list
A
)).
(** Setoid properties *)
Global
Instance
mono_list_list_auth_ne
:
NonExpansive
(@
mono_list_list_auth
A
).
Proof
.
solve_proper
.
Qed
.
Global
Instance
mono_list_list_auth_proper
:
Proper
((
≡
)
==>
(
≡
))
(@
mono_list_list_auth
A
).
Proof
.
solve_proper
.
Qed
.
Global
Instance
mono_list_list_lb_ne
:
NonExpansive
(@
mono_list_list_lb
A
).
Proof
.
solve_proper
.
Qed
.
Global
Instance
mono_list_list_lb_proper
:
Proper
((
≡
)
==>
(
≡
))
(@
mono_list_list_lb
A
).
Proof
.
solve_proper
.
Qed
.
Global
Instance
mono_list_list_lb_dist_inj
n
:
Inj
(
dist
n
)
(
dist
n
)
(@
mono_list_list_lb
A
).
Proof
.
rewrite
/
mono_list_list_lb
.
by
intros
??
?%(
inj
_
)%(
inj
_
).
Qed
.
Global
Instance
mono_list_list_lb_inj
:
Inj
(
≡
)
(
≡
)
(@
mono_list_list_lb
A
).
Proof
.
rewrite
/
mono_list_list_lb
.
by
intros
??
?%(
inj
_
)%(
inj
_
).
Qed
.
(** * Operation *)
Global
Instance
mono_list_list_lb_core_id
ll
:
CoreId
(
◯
MLL
ll
).
Proof
.
rewrite
/
mono_list_list_lb
.
apply
_
.
Qed
.
Lemma
mono_list_list_lb_op_l
ll1
ll2
:
ll1
`
prefixes_of
`
ll2
→
◯
MLL
ll1
⋅
◯
MLL
ll2
≡
◯
MLL
ll2
.
Proof
.
intros
?.
by
rewrite
/
mono_list_list_lb
-
auth_frag_op
to_max_prefix_list_list_op_l
.
Qed
.
Lemma
mono_list_list_lb_op_r
ll1
ll2
:
ll1
`
prefixes_of
`
ll2
→
◯
MLL
ll2
⋅
◯
MLL
ll1
≡
◯
MLL
ll2
.
Proof
.
intros
?.
by
rewrite
/
mono_list_list_lb
-
auth_frag_op
to_max_prefix_list_list_op_r
.
Qed
.
Lemma
mono_list_list_auth_lb_op
ll
:
●
MLL
ll
≡
●
MLL
ll
⋅
◯
MLL
ll
.
Proof
.
by
rewrite
/
mono_list_list_auth
/
mono_list_list_lb
-!
assoc
-
auth_frag_op
-
core_id_dup
.
Qed
.
Global
Instance
mono_list_list_lb_is_op
ll
:
IsOp'
(
◯
MLL
ll
)
(
◯
MLL
ll
)
(
◯
MLL
ll
).
Proof
.
by
rewrite
/
IsOp'
/
IsOp
-
core_id_dup
.
Qed
.
(** * Validity *)
Lemma
mono_list_list_auth_validN
n
ll
:
✓
{
n
}
(
●
MLL
ll
).
Proof
.
rewrite
/
mono_list_list_auth
auth_both_validN
.
naive_solver
apply
to_max_prefix_list_list_validN
.
Qed
.
Lemma
mono_list_list_auth_valid
ll
:
✓
(
●
MLL
ll
).
Proof
.
rewrite
/
mono_list_list_auth
auth_both_valid
.
naive_solver
apply
to_max_prefix_list_list_valid
.
Qed
.
Lemma
mono_list_list_both_validN
n
ll1
ll2
:
✓
{
n
}
(
●
MLL
ll1
⋅
◯
MLL
ll2
)
↔
map_included
(
λ
l1
l2
,
∃
l
,
l2
≡
{
n
}
≡
l1
++
l
)
ll2
ll1
.
Proof
.
rewrite
/
mono_list_list_auth
/
mono_list_list_lb
-
assoc
-
auth_frag_op
auth_both_validN
-
to_max_prefix_list_list_includedN
.
split
.
-
intros
[
Hincl
_
].
(* NOTE: Can't [etrans]. "not a declared transitive relation". *)
eapply
(@
transitivity
(
max_prefix_list_listR
A
)
_
(
cmra_includedN_trans
n
))
;
[
apply
cmra_includedN_r
|
done
].
-
intros
.
split
;
[|
by
apply
to_max_prefix_list_list_validN
].
rewrite
{
2
}(
core_id_dup
(
to_max_prefix_list_list
ll1
)).
by
f_equiv
.
Qed
.
Lemma
mono_list_list_both_valid
ll1
ll2
:
✓
(
●
MLL
ll1
⋅
◯
MLL
ll2
)
↔
map_included
(
λ
l1
l2
,
∃
l
,
l2
≡
l1
++
l
)
ll2
ll1
.
Proof
.
rewrite
/
mono_list_list_auth
/
mono_list_list_lb
-
assoc
-
auth_frag_op
auth_both_valid
-
max_prefix_list_list_included_includedN
-
to_max_prefix_list_list_included
.
split
.
-
intros
[
Hincl
_
].
(* NOTE: Can't [etrans]. "not a declared transitive relation". *)
eapply
(@
transitivity
(
max_prefix_list_listR
A
)
_
cmra_included_trans
)
;
[
apply
cmra_included_r
|
done
].
-
intros
.
split
;
[|
by
apply
to_max_prefix_list_list_valid
].
(* NOTE: can't infer cmra in [cmra_included_proper]? *)
(* rewrite {2}(core_id_dup (to_max_prefix_list_list ll1)). by f_equiv. *)
move
:
H
.
rewrite
!
lookup_included
=>
H
i
.
move
:
{
H
}(
H
i
).
rewrite
lookup_op
.
rewrite
/
to_max_prefix_list_list
!
fmap_map_seq
!
lookup_map_seq_0
!
list_lookup_fmap
.
destruct
(
ll1
!!
i
)
as
[
l1
|],
(
ll2
!!
i
)
as
[
l2
|]
;
simpl
;
[|
done
..].
move
=>
/
Some_included_total
H
.
rewrite
-
Some_op
Some_included_total
.
rewrite
{
2
}(
core_id_dup
(
to_max_prefix_list
l1
)).
by
f_equiv
.
Qed
.
Lemma
mono_list_list_both_valid_L
`
{!
LeibnizEquiv
A
}
ll1
ll2
:
✓
(
●
MLL
ll1
⋅
◯
MLL
ll2
)
↔
ll2
`
prefixes_of
`
ll1
.
Proof
.
rewrite
mono_list_list_both_valid
.
apply
map_relation_iff
;
[|
done
..].
rewrite
/
prefix
.
naive_solver
.
Qed
.
Lemma
mono_list_list_included
ll
:
◯
MLL
ll
≼
●
MLL
ll
.
Proof
.
apply
cmra_included_r
.
Qed
.
(** * Update *)
Lemma
mono_list_list_update
{
ll1
}
ll2
:
ll1
`
prefixes_of
`
ll2
→
●
MLL
ll1
~~>
●
MLL
ll2
.
Proof
.
intros
?.
by
apply
auth_update
,
max_prefix_list_list_local_update
.
Qed
.
End
mono_list_list
.
theories/examples/history/ghost.v
0 → 100644
View file @
c5fa30a1
From
iris
.
algebra
Require
Import
auth
gmap
.
From
iris
.
bi
Require
Import
fractional
.
From
iris
.
proofmode
Require
Import
tactics
.
From
iris
.
base_logic
.
lib
Require
Import
own
.
From
gpfsl
.
base_logic
Require
Import
vprop
.
From
gpfsl
.
examples
.
event
Require
Import
event
ghost
.
From
gpfsl
.
algebra
Require
Import
mono_list
.
From
gpfsl
.
examples
.
graph
Require
Import
ghost
.
From
gpfsl
.
examples
.
history
Require
Import
history
.
Require
Import
iris
.
prelude
.
options
.
(** CMRA for history *)
Notation
historyR
:
=
elistR
.
Definition
ghost_history_master
{
A
}
f
E
:
historyR
A
:
=
●
ML
{#
f
}
(
E
:
listO
(
leibnizO
_
)).
Definition
ghost_history_snap
{
A
}
E
:
historyR
A
:
=
◯
ML
(
E
:
listO
(
leibnizO
_
)).
Notation
history_gmaster
γ
g
f
E
:
=
(
own
γ
g
(
ghost_history_master
f
E
)).
Notation
history_gsnap
γ
g
E
:
=
(
own
γ
g
(
ghost_history_snap
E
)).
Notation
history_gsnapv
γ
g
E
:
=
(
⎡
history_gsnap
γ
g
E
⎤
%
I
:
vProp
_
).
Section
Graphs
.
Context
{
eventT
:
Type
}.
Context
{
Σ
:
gFunctors
}
`
{
egRG
:
inG
Σ
(
historyR
eventT
)}.
Notation
history
:
=
(
history
eventT
).
Notation
iProp
:
=
(
iProp
Σ
).
Notation
vProp
:
=
(
vProp
Σ
).
Implicit
Types
(
E
:
history
)
(
M
:
logView
).
Definition
history_master
γ
g
q
E
:
vProp
:
=
⎡
history_gmaster
γ
g
q
E
⎤
∗
⌜
history_wf
E
⌝
.
Definition
history_snap
γ
g
E
M
:
vProp
:
=
history_gsnapv
γ
g
E
∗
SeenLogview
E
M
.
#[
global
]
Instance
history_gmaster_timeless
γ
g
q
E
:
Timeless
(
history_gmaster
γ
g
q
E
)
:
=
_
.
#[
global
]
Instance
history_master_timeless
γ
g
f
E
:
Timeless
(
history_master
γ
g
f
E
)
:
=
_
.
#[
global
]
Instance
history_master_objective
γ
g
f
E
:
Objective
(
history_master
γ
g
f
E
)
:
=
_
.
#[
global
]
Instance
history_snap_timelesss
γ
g
E
M
:
Timeless
(
history_snap
γ
g
E
M
)
:
=
_
.
#[
global
]
Instance
history_snap_persistent
γ
g
E
M
:
Persistent
(
history_snap
γ
g
E
M
)
:
=
_
.
#[
global
]
Instance
history_snap_empty_objective
γ
g
E
:
Objective
(
history_snap
γ
g
E
∅
)
:
=
_
.
(** Ghost properties *)
(* Updates *)
Lemma
ghost_history_update
γ
E
E'
(
Le
:
E
⊑
E'
)
:
history_gmaster
γ
1
E
==
∗
history_gmaster
γ
1
E'
∗
history_gsnap
γ
E'
.
Proof
.
rewrite
-
own_op
.
apply
own_update
.
rewrite
-
mono_list_auth_lb_op
.
by
apply
mono_list_update
.
Qed
.
Lemma
ghost_history_fork
γ
f
E
E'
(
Le
:
E'
⊑
E
)
:
history_gmaster
γ
f
E
==
∗
history_gmaster
γ
f
E
∗
history_gsnap
γ
E'
.
Proof
.
rewrite
-
own_op
.
apply
own_update
.
rewrite
/
ghost_history_master
/
ghost_history_snap
.
rewrite
mono_list_auth_lb_op
.
rewrite
-(
assoc
_
(
●
ML
{#
f
}
_
))
mono_list_lb_op_r
;
[|
done
].
by
rewrite
-
mono_list_auth_lb_op
.
Qed
.
(* Alloc *)
Lemma
ghost_history_alloc
E
:
⊢
|==>
∃
γ
,
history_gmaster
γ
1
E
∗
history_gsnap
γ
E
.
Proof
.
iMod
(
own_alloc
(
ghost_history_master
1
E
))
as
(
γ
)
"Hm"
.
-
apply
mono_list_auth_valid
.
-
iExists
γ
.
by
iMod
(
ghost_history_update
with
"Hm"
)
as
"$"
.
Qed
.
(* Agreements *)
Lemma
ghost_history_master_agree
γ
f1
E1
f2
E2
:
history_gmaster
γ
f1
E1
-
∗
history_gmaster
γ
f2
E2
-
∗
⌜
E1
=
E2
⌝
.
Proof
.
iIntros
"o1 o2"
.
by
iDestruct
(
own_valid_2
with
"o1 o2"
)
as
%[
_
?%
leibniz_equiv
]%
mono_list_auth_frac_op_valid
.
Qed
.
Lemma
ghost_history_master_snap_included
γ
g
f
E
E'
:
history_gmaster
γ
g
f
E
-
∗
history_gsnap
γ
g
E'
-
∗
⌜
E'
⊑
E
⌝
.
Proof
.
iIntros
"oM oS"
.
by
iDestruct
(
own_valid_2
with
"oM oS"
)
as
%[
_
?]%
mono_list_both_dfrac_valid_L
.
Qed
.
(** Graph's Master-Snapshot properties *)
#[
global
]
Instance
history_master_fractional
γ
g
E
:
Fractional
(
λ
q
,
history_master
γ
g
q
E
).
Proof
.
intros
p
q
.
rewrite
/
history_master
.
iSplit
.
-
iIntros
"[E %]"
.
iFrame
"%"
.
rewrite
-
embed_sep
-
own_op
.
by
rewrite
-
mono_list_auth_frac_op
.
-
iIntros
"[[E1 _] [E2 $]]"
.
iCombine
"E1 E2"
as
"E"
.
by
rewrite
-
mono_list_auth_frac_op
.
Qed
.
#[
global
]
Instance
history_master_asfractional
γ
g
E
q
:
AsFractional
(
history_master
γ
g
q
E
)
(
λ
q
,
history_master
γ
g
q
E
)
q
.
Proof
.
constructor
;
[
done
|
apply
_
].
Qed
.
Lemma
history_master_update
γ
E
E'
:
E
⊑
E'
→
history_wf
E'
→
history_master
γ
1
E
==
∗
history_master
γ
1
E'
∗
history_gsnapv
γ
E'
.
Proof
.
iIntros
(
SE
EC
)
"[EM %]"
.
by
iMod
(
ghost_history_update
with
"EM"
)
as
"[$ $]"
.
Qed
.
Lemma
history_master_alloc_empty
:
⊢
|==>
∃
γ
,
history_master
γ
1
[]
∗
history_gsnapv
γ
[].
Proof
.
iMod
(
ghost_history_alloc
[])
as
(
γ
)
"[Em Es]"
.
iIntros
"!>"
.
iExists
γ
.
iFrame
.
by
iPureIntro
.
Qed
.
Lemma
history_master_wf
γ
g
f
E
:
history_master
γ
g
f
E
-
∗
⌜
history_wf
E
⌝
.
Proof
.
by
iIntros
"[? %]"
.
Qed
.
Lemma
history_master_agree
γ
g
f1
E1
f2
E2
:
history_master
γ
g
f1
E1
-
∗
history_master
γ
g
f2
E2
-
∗
⌜
E1
=
E2
⌝
.
Proof
.
iIntros
"[E1 _] [E2 _]"
.
by
iDestruct
(
ghost_history_master_agree
with
"E1 E2"
)
as
%?.
Qed
.
Lemma
history_master_snap
γ
g
f
E
:
history_master
γ
g
f
E
==
∗
history_master
γ
g
f
E
∗
history_snap
γ
g
E
∅
.
Proof
.
iIntros
"[E %EGc]"
.
iMod
(
ghost_history_fork
with
"E"
)
as
"[$ $]"
;
first
by
auto
.
iIntros
"!>"
.
iSplit
;
[
done
|].
by
rewrite
-
SeenLogview_empty
.
Qed
.
Lemma
history_master_snap_included'
γ
g
f
E
E'
M
V
V'
:
@{
V
}
history_master
γ
g
f
E
-
∗
@{
V'
}
history_snap
γ
g
E'
M
-
∗
⌜
E'
⊑
E
⌝
.
Proof
.
iIntros
"[E _] [Es _]"
.
rewrite
!
view_at_objective_iff
.
by
iDestruct
(
ghost_history_master_snap_included
with
"E Es"
)
as
%?.
Qed
.
Definition
history_master_snap_included
γ
g
f
E
E'
M
:
=
view_at_wand_lr
_
_
_
(
history_master_snap_included'
γ
g
f
E
E'
M
).
Definition
history_master_snap_included_2
γ
g
f
E
E'
M
:
=
view_at_wand_l
_
_
_
(
history_master_snap_included'
γ
g
f
E
E'
M
).
Lemma
history_snap_mono_marked
γ
g
E
M
E'
M'
(
In1
:
E'
⊑
E
)
:
history_snap
γ
g
E
M
-
∗
history_snap
γ
g
E'
M'
-
∗
history_snap
γ
g
E
M'
.
Proof
.
iIntros
"[$ PS1] [_ PS2]"
.
by
iApply
(
SeenLogview_map_mono
with
"PS2"
).
Qed
.
Lemma
history_snap_downclosed
γ
g
E
M
M'
:
M'
⊆
M
→
history_snap
γ
g
E
M
⊢
history_snap
γ
g
E
M'
.
Proof
.
iIntros
(
SubM'
)
"[$ SL]"
.
by
iApply
SeenLogview_downclosed
.
Qed
.
Lemma
history_snap_lookup
γ
g
E
M
e
dV
:
ge_view
<$>
E
!!
e
=
Some
dV
→
e
∈
M
→
history_snap
γ
g
E
M
-
∗
⊒
(
dV
.(
dv_comm
)).
Proof
.
intros
Eqe
Inm
.
constructor
=>
V''
/=.
iIntros
"[_ %InM']"
.
iPureIntro
.
specialize
(
InM'
_
Inm
)
as
([
e'
V'
]
&
Eq'
&
SubV'
).
simpl
in
SubV'
.
rewrite
Eq'
/=
in
Eqe
.
by
simplify_eq
.
Qed
.
(* Stupid lemma done at iRC11 level *)
Lemma
history_snap_empty
γ
g
:
history_gsnapv
γ
g
[]
-
∗
history_snap
γ
g
[]
∅
.
Proof
.
iIntros
"$"
.
by
rewrite
-
SeenLogview_empty
.
Qed
.
End
Graphs
.
Typeclasses
Opaque
history_master
.
Typeclasses
Opaque
graph_gmaster
.
theories/examples/history/history.v
0 → 100644
View file @
c5fa30a1
From
gpfsl
.
examples
Require
Import
sflib
.
From
iris
.
algebra
Require
Import
gmap
.
From
gpfsl
.
lang
Require
Import
lang
.
From
gpfsl
.
examples
.
event
Require
Import
event
.
Require
Import
iris
.
prelude
.
options
.
Notation
history
eventT
:
=
(
event_list
eventT
).
Section
history
.
Context
{
eventT
:
Type
}.
Implicit
Types
(
E
:
history
eventT
)
(
V
:
view
).
Record
history_wf
E
:
=
mkHistoryWf
{
(* logview includes the event itself *)
hwf_logview_event
: