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
c
Commits
2ae8b292
Commit
2ae8b292
authored
Jun 18, 2019
by
Robbert Krebbers
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Bump Iris (C→O rename, lazy_tc).
parent
08d9e2b1
Pipeline
#17765
failed with stage
in 11 minutes and 13 seconds
Changes
5
Pipelines
3
Hide whitespace changes
Inline
Side-by-side
Showing
5 changed files
with
14 additions
and
14 deletions
+14
-14
opam
opam
+1
-1
theories/c_translation/proofmode.v
theories/c_translation/proofmode.v
+1
-1
theories/lib/flock.v
theories/lib/flock.v
+8
-8
theories/lib/locking_heap.v
theories/lib/locking_heap.v
+3
-3
theories/tests/store_strong.v
theories/tests/store_strong.v
+1
-1
No files found.
opam
View file @
2ae8b292
...
...
@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iris-c" ]
depends: [
"coq-iris" { (= "dev.2019-06-1
1.8.a51fa3cf
") | (= "dev") }
"coq-iris" { (= "dev.2019-06-1
8.2.e039d7c7
") | (= "dev") }
]
theories/c_translation/proofmode.v
View file @
2ae8b292
...
...
@@ -15,7 +15,7 @@ Ltac cwp_bind_core K :=
end
.
Tactic
Notation
"cwp_apply"
open_constr
(
lem
)
:
=
iPoseProofCore
lem
as
false
true
(
fun
H
=>
iPoseProofCore
lem
as
false
(
fun
H
=>
lazymatch
goal
with
|
|-
envs_entails
_
(
cwp
?e
?R
?Q
)
=>
reshape_expr
e
ltac
:
(
fun
K
e'
=>
...
...
theories/lib/flock.v
View file @
2ae8b292
...
...
@@ -7,7 +7,7 @@ From iris.bi.lib Require Import fractional.
Inductive
lockstate
:
=
|
Locked
|
Unlocked
.
Canonical
Structure
lockstate
C
:
=
leibniz
C
lockstate
.
Canonical
Structure
lockstate
O
:
=
leibniz
O
lockstate
.
Instance
lockstate_inhabited
:
Inhabited
lockstate
:
=
populate
Unlocked
.
...
...
@@ -68,7 +68,7 @@ Record lock_res_gname := {
flock_token1_name
:
gname
;
flock_token2_name
:
gname
;
}.
Canonical
Structure
lock_res_gname
C
:
=
leibniz
C
lock_res_gname
.
Canonical
Structure
lock_res_gname
O
:
=
leibniz
O
lock_res_gname
.
Instance
lock_res_gname_eq_dec
:
EqDecision
lock_res_gname
.
Proof
.
solve_decision
.
Defined
.
...
...
@@ -97,23 +97,23 @@ Defined.
*)
Class
flockG
Σ
:
=
FlockG
{
flock_stateG
:
>
inG
Σ
(
authR
(
optionUR
(
exclR
lockstate
C
)))
;
flock_stateG
:
>
inG
Σ
(
authR
(
optionUR
(
exclR
lockstate
O
)))
;
flock_lockG
:
>
lockG
Σ
;
flock_cinvG
:
>
cinvG
Σ
;
(* note the difference between the two RAs here ! *)
flock_props_active
:
>
inG
Σ
(
authR
(
optionUR
(
exclR
(
gmap
C
lock_res_gname
fracR
))))
;
(
optionUR
(
exclR
(
gmap
O
lock_res_gname
fracR
))))
;
flock_props
:
>
inG
Σ
(
authR
(
gmapUR
lock_res_gname
fracR
))
;
flock_tokens
:
>
inG
Σ
(
exclR
unit
C
)
;
flock_tokens
:
>
inG
Σ
(
exclR
unit
O
)
;
}.
Definition
flock
Σ
:
gFunctors
:
=
#[
GFunctor
(
authR
(
optionUR
(
exclR
lockstate
C
)))
#[
GFunctor
(
authR
(
optionUR
(
exclR
lockstate
O
)))
;
lock
Σ
;
cinv
Σ
;
GFunctor
(
authR
(
optionUR
(
exclR
(
gmap
C
lock_res_gname
frac
C
))))
;
GFunctor
(
authR
(
gmapUR
lock_res_gname
fracR
))%
C
F
].
;
GFunctor
(
authR
(
optionUR
(
exclR
(
gmap
O
lock_res_gname
frac
O
))))
;
GFunctor
(
authR
(
gmapUR
lock_res_gname
fracR
))%
O
F
].
Instance
subG_flock
Σ
Σ
:
subG
flock
Σ
Σ
→
flockG
Σ
.
Proof
.
solve_inG
.
Qed
.
...
...
theories/lib/locking_heap.v
View file @
2ae8b292
...
...
@@ -9,7 +9,7 @@ Local Open Scope nat_scope.
Inductive
lvl
:
=
|
LLvl
:
lvl
|
ULvl
:
lvl
.
Canonical
Structure
lvl
C
:
=
leibniz
C
lvl
.
Canonical
Structure
lvl
O
:
=
leibniz
O
lvl
.
Instance
lvl_EqDecision
:
EqDecision
lvl
.
Proof
.
solve_decision
.
Defined
.
...
...
@@ -82,9 +82,9 @@ Instance cloc_inhabited : Inhabited cloc | 0 :=
(* Auth (CLoc -> (Q * Level)) *)
Definition
locking_heapUR
:
ucmraT
:
=
gmapUR
cloc
(
prodR
(
prodR
fracR
lvlUR
)
(
agreeR
val
C
)).
gmapUR
cloc
(
prodR
(
prodR
fracR
lvlUR
)
(
agreeR
val
O
)).
Definition
heap_block_infoUR
:
ucmraT
:
=
gmapUR
loc
(
agreeR
(
prod
C
bool
C
nat
C
)).
gmapUR
loc
(
agreeR
(
prod
O
bool
O
nat
O
)).
(** The CMRA we need. *)
Class
locking_heapG
(
Σ
:
gFunctors
)
:
=
LHeapG
{
...
...
theories/tests/store_strong.v
View file @
2ae8b292
...
...
@@ -42,7 +42,7 @@ Definition test : val := λᶜ "l",
call
ᶜ
(
c_ret
storeme
)
(
c_ret
"l"
)
+
ᶜ
(
c_ret
"l"
=
ᶜ
♯
11
).
Section
test
.
Context
`
{
cmonadG
Σ
,
!
inG
Σ
(
authR
(
optionUR
(
exclR
bool
C
)))}.
Context
`
{
cmonadG
Σ
,
!
inG
Σ
(
authR
(
optionUR
(
exclR
bool
O
)))}.
(** Basic specification for `storeme' *)
Lemma
storeme_spec
R
cl
v
Φ
:
...
...
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