Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
10
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Open sidebar
Iris
Iris
Commits
37305156
Commit
37305156
authored
Feb 24, 2016
by
Robbert Krebbers
Browse files
Options
Browse Files
Download
Plain Diff
Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq
parents
c9ea799b
21419737
Pipeline
#144
passed with stage
Changes
4
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
Showing
4 changed files
with
28 additions
and
40 deletions
+28
-40
heap_lang/heap.v
heap_lang/heap.v
+5
-8
program_logic/auth.v
program_logic/auth.v
+5
-8
program_logic/saved_prop.v
program_logic/saved_prop.v
+6
-10
program_logic/sts.v
program_logic/sts.v
+12
-14
No files found.
heap_lang/heap.v
View file @
37305156
...
...
@@ -25,14 +25,11 @@ matching it against other forms of ownership. *)
Definition
heap_mapsto_def
`
{
heapG
Σ
}
(
l
:
loc
)
(
v
:
val
)
:
iPropG
heap_lang
Σ
:
=
auth_own
heap_name
{[
l
:
=
Excl
v
]}.
(* Perform sealing *)
Module
Type
HeapMapstoSig
.
Parameter
heap_mapsto
:
∀
`
{
heapG
Σ
}
(
l
:
loc
)
(
v
:
val
),
iPropG
heap_lang
Σ
.
Axiom
heap_mapsto_eq
:
@
heap_mapsto
=
@
heap_mapsto_def
.
End
HeapMapstoSig
.
Module
Export
HeapMapsto
:
HeapMapstoSig
.
Definition
heap_mapsto
:
=
@
heap_mapsto_def
.
Definition
heap_mapsto_eq
:
=
Logic
.
eq_refl
(@
heap_mapsto
).
End
HeapMapsto
.
Definition
heap_mapsto_aux
:
{
x
:
_
&
x
=
@
heap_mapsto_def
}.
exact
(
existT
_
Logic
.
eq_refl
).
Qed
.
Definition
heap_mapsto
:
=
projT1
heap_mapsto_aux
.
Definition
heap_mapsto_eq
:
@
heap_mapsto
=
@
heap_mapsto_def
:
=
projT2
heap_mapsto_aux
.
Arguments
heap_mapsto
{
_
_
}
_
_
.
Definition
heap_inv
`
{
i
:
heapG
Σ
}
(
h
:
heapRA
)
:
iPropG
heap_lang
Σ
:
=
ownP
(
of_heap
h
).
...
...
program_logic/auth.v
View file @
37305156
...
...
@@ -16,14 +16,11 @@ Proof. split; try apply _. apply: inGF_inG. Qed.
Definition
auth_own_def
`
{
authG
Λ
Σ
A
}
(
γ
:
gname
)
(
a
:
A
)
:
iPropG
Λ
Σ
:
=
own
γ
(
◯
a
).
(* Perform sealing *)
Module
Type
AuthOwnSig
.
Parameter
auth_own
:
∀
`
{
authG
Λ
Σ
A
}
(
γ
:
gname
)
(
a
:
A
),
iPropG
Λ
Σ
.
Axiom
auth_own_eq
:
@
auth_own
=
@
auth_own_def
.
End
AuthOwnSig
.
Module
Export
AuthOwn
:
AuthOwnSig
.
Definition
auth_own
:
=
@
auth_own_def
.
Definition
auth_own_eq
:
=
Logic
.
eq_refl
(@
auth_own
).
End
AuthOwn
.
Definition
auth_own_aux
:
{
x
:
_
&
x
=
@
auth_own_def
}.
exact
(
existT
_
Logic
.
eq_refl
).
Qed
.
Definition
auth_own
:
=
projT1
auth_own_aux
.
Definition
auth_own_eq
:
@
auth_own
=
@
auth_own_def
:
=
projT2
auth_own_aux
.
Arguments
auth_own
{
_
_
_
_
_
}
_
_
.
Definition
auth_inv
`
{
authG
Λ
Σ
A
}
(
γ
:
gname
)
(
φ
:
A
→
iPropG
Λ
Σ
)
:
iPropG
Λ
Σ
:
=
...
...
program_logic/saved_prop.v
View file @
37305156
...
...
@@ -11,16 +11,12 @@ Proof. apply: inGF_inG. Qed.
Definition
saved_prop_own_def
`
{
savedPropG
Λ
Σ
}
(
γ
:
gname
)
(
P
:
iPropG
Λ
Σ
)
:
iPropG
Λ
Σ
:
=
own
γ
(
to_agree
(
Next
(
iProp_unfold
P
))).
(* Perform sealing. *)
Module
Type
SavedPropOwnSig
.
Parameter
saved_prop_own
:
∀
`
{
savedPropG
Λ
Σ
}
(
γ
:
gname
)
(
P
:
iPropG
Λ
Σ
),
iPropG
Λ
Σ
.
Axiom
saved_prop_own_eq
:
@
saved_prop_own
=
@
saved_prop_own_def
.
End
SavedPropOwnSig
.
Module
Export
SavedPropOwn
:
SavedPropOwnSig
.
Definition
saved_prop_own
:
=
@
saved_prop_own_def
.
Definition
saved_prop_own_eq
:
=
Logic
.
eq_refl
(@
saved_prop_own
).
End
SavedPropOwn
.
(* Perform sealing *)
Definition
saved_prop_own_aux
:
{
x
:
_
&
x
=
@
saved_prop_own_def
}.
exact
(
existT
_
Logic
.
eq_refl
).
Qed
.
Definition
saved_prop_own
:
=
projT1
saved_prop_own_aux
.
Definition
saved_prop_own_eq
:
@
saved_prop_own
=
@
saved_prop_own_def
:
=
projT2
saved_prop_own_aux
.
Arguments
saved_prop_own
{
_
_
_
}
_
_
.
Instance
:
Params
(@
saved_prop_own
)
4
.
Section
saved_prop
.
...
...
program_logic/sts.v
View file @
37305156
...
...
@@ -16,24 +16,22 @@ Proof. split; try apply _. apply: inGF_inG. Qed.
Definition
sts_ownS_def
`
{
i
:
stsG
Λ
Σ
sts
}
(
γ
:
gname
)
(
S
:
sts
.
states
sts
)
(
T
:
sts
.
tokens
sts
)
:
iPropG
Λ
Σ
:
=
own
γ
(
sts_frag
S
T
).
(* Perform sealing. *)
Definition
sts_ownS_aux
:
{
x
:
_
&
x
=
@
sts_ownS_def
}.
exact
(
existT
_
Logic
.
eq_refl
).
Qed
.
Definition
sts_ownS
:
=
projT1
sts_ownS_aux
.
Definition
sts_ownS_eq
:
@
sts_ownS
=
@
sts_ownS_def
:
=
projT2
sts_ownS_aux
.
Arguments
sts_ownS
{
_
_
_
_
}
_
_
_
.
Definition
sts_own_def
`
{
i
:
stsG
Λ
Σ
sts
}
(
γ
:
gname
)
(
s
:
sts
.
state
sts
)
(
T
:
sts
.
tokens
sts
)
:
iPropG
Λ
Σ
:
=
own
γ
(
sts_frag_up
s
T
).
(* Perform sealing. *)
Module
Type
StsOwnSig
.
Parameter
sts_ownS
:
∀
`
{
i
:
stsG
Λ
Σ
sts
}
(
γ
:
gname
)
(
S
:
sts
.
states
sts
)
(
T
:
sts
.
tokens
sts
),
iPropG
Λ
Σ
.
Parameter
sts_own
:
∀
`
{
i
:
stsG
Λ
Σ
sts
}
(
γ
:
gname
)
(
s
:
sts
.
state
sts
)
(
T
:
sts
.
tokens
sts
),
iPropG
Λ
Σ
.
Axiom
sts_ownS_eq
:
@
sts_ownS
=
@
sts_ownS_def
.
Axiom
sts_own_eq
:
@
sts_own
=
@
sts_own_def
.
End
StsOwnSig
.
Module
Export
StsOwn
:
StsOwnSig
.
Definition
sts_ownS
:
=
@
sts_ownS_def
.
Definition
sts_own
:
=
@
sts_own_def
.
Definition
sts_ownS_eq
:
=
Logic
.
eq_refl
(@
sts_ownS_def
).
Definition
sts_own_eq
:
=
Logic
.
eq_refl
(@
sts_own_def
).
End
StsOwn
.
Definition
sts_own_aux
:
{
x
:
_
&
x
=
@
sts_own_def
}.
exact
(
existT
_
Logic
.
eq_refl
).
Qed
.
Definition
sts_own
:
=
projT1
sts_own_aux
.
Definition
sts_own_eq
:
@
sts_own
=
@
sts_own_def
:
=
projT2
sts_own_aux
.
Arguments
sts_own
{
_
_
_
_
}
_
_
_
.
Definition
sts_inv
`
{
i
:
stsG
Λ
Σ
sts
}
(
γ
:
gname
)
(
φ
:
sts
.
state
sts
→
iPropG
Λ
Σ
)
:
iPropG
Λ
Σ
:
=
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a 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