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
Iris
Commits
bdcfa356
Commit
bdcfa356
authored
Feb 27, 2016
by
Ralf Jung
Browse files
make auth_fsa consistent about const-valid vs uPred-valid
parent
e3c01577
Pipeline
#185
passed with stage
Changes
2
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
heap_lang/heap.v
View file @
bdcfa356
...
...
@@ -149,7 +149,7 @@ Section heap.
apply
wp_strip_pvs
,
(
auth_fsa
heap_inv
(
wp_fsa
(
Alloc
e
)))
with
N
heap_name
∅
;
simpl
;
eauto
with
I
.
rewrite
-
later_intro
.
apply
sep_mono_r
,
forall_intro
=>
h
;
apply
wand_intro_l
.
rewrite
-
assoc
left_id
discrete_valid
;
apply
const_elim_sep_l
=>
?.
rewrite
-
assoc
left_id
;
apply
const_elim_sep_l
=>
?.
rewrite
-(
wp_alloc_pst
_
(
of_heap
h
))
//.
apply
sep_mono_r
;
rewrite
HP
;
apply
later_mono
.
apply
forall_mono
=>
l
;
apply
wand_intro_l
.
...
...
@@ -172,7 +172,7 @@ Section heap.
apply
(
auth_fsa'
heap_inv
(
wp_fsa
_
)
id
)
with
N
heap_name
{[
l
:
=
Frac
q
(
DecAgree
v
)
]}
;
simpl
;
eauto
with
I
.
rewrite
HP
Φ
{
HP
Φ
}
;
apply
sep_mono_r
,
forall_intro
=>
h
;
apply
wand_intro_l
.
rewrite
-
assoc
discrete_valid
;
apply
const_elim_sep_l
=>
?.
rewrite
-
assoc
;
apply
const_elim_sep_l
=>
?.
rewrite
-(
wp_load_pst
_
(<[
l
:
=
v
]>(
of_heap
h
)))
?lookup_insert
//.
rewrite
const_equiv
//
left_id
.
rewrite
/
heap_inv
of_heap_singleton_op
//.
...
...
@@ -189,7 +189,7 @@ Section heap.
apply
(
auth_fsa'
heap_inv
(
wp_fsa
_
)
(
alter
(
λ
_
,
Frac
1
(
DecAgree
v
))
l
))
with
N
heap_name
{[
l
:
=
Frac
1
(
DecAgree
v'
)
]}
;
simpl
;
eauto
with
I
.
rewrite
HP
Φ
{
HP
Φ
}
;
apply
sep_mono_r
,
forall_intro
=>
h
;
apply
wand_intro_l
.
rewrite
-
assoc
discrete_valid
;
apply
const_elim_sep_l
=>
?.
rewrite
-
assoc
;
apply
const_elim_sep_l
=>
?.
rewrite
-(
wp_store_pst
_
(<[
l
:
=
v'
]>(
of_heap
h
)))
?lookup_insert
//.
rewrite
/
heap_inv
alter_singleton
insert_insert
!
of_heap_singleton_op
;
eauto
.
rewrite
const_equiv
;
last
naive_solver
.
...
...
@@ -206,7 +206,7 @@ Section heap.
apply
(
auth_fsa'
heap_inv
(
wp_fsa
_
)
id
)
with
N
heap_name
{[
l
:
=
Frac
q
(
DecAgree
v'
)
]}
;
simpl
;
eauto
10
with
I
.
rewrite
HP
Φ
{
HP
Φ
}
;
apply
sep_mono_r
,
forall_intro
=>
h
;
apply
wand_intro_l
.
rewrite
-
assoc
discrete_valid
;
apply
const_elim_sep_l
=>
?.
rewrite
-
assoc
;
apply
const_elim_sep_l
=>
?.
rewrite
-(
wp_cas_fail_pst
_
(<[
l
:
=
v'
]>(
of_heap
h
)))
?lookup_insert
//.
rewrite
const_equiv
//
left_id
.
rewrite
/
heap_inv
!
of_heap_singleton_op
//.
...
...
@@ -223,7 +223,7 @@ Section heap.
apply
(
auth_fsa'
heap_inv
(
wp_fsa
_
)
(
alter
(
λ
_
,
Frac
1
(
DecAgree
v2
))
l
))
with
N
heap_name
{[
l
:
=
Frac
1
(
DecAgree
v1
)
]}
;
simpl
;
eauto
10
with
I
.
rewrite
HP
Φ
{
HP
Φ
}
;
apply
sep_mono_r
,
forall_intro
=>
h
;
apply
wand_intro_l
.
rewrite
-
assoc
discrete_valid
;
apply
const_elim_sep_l
=>
?.
rewrite
-
assoc
;
apply
const_elim_sep_l
=>
?.
rewrite
-(
wp_cas_suc_pst
_
(<[
l
:
=
v1
]>(
of_heap
h
)))
//
;
last
by
rewrite
lookup_insert
.
rewrite
/
heap_inv
alter_singleton
insert_insert
!
of_heap_singleton_op
;
eauto
.
...
...
program_logic/auth.v
View file @
bdcfa356
...
...
@@ -101,15 +101,12 @@ Section auth.
Context
{
V
}
(
fsa
:
FSA
Λ
(
globalF
Σ
)
V
)
`
{!
FrameShiftAssertion
fsaV
fsa
}.
(* Notice how the user has to prove that `b⋅a'` is valid at all
step-indices. However, since A is timeless, that should not be
a restriction. *)
Lemma
auth_fsa
E
N
P
(
Ψ
:
V
→
iPropG
Λ
Σ
)
γ
a
:
fsaV
→
nclose
N
⊆
E
→
P
⊑
auth_ctx
γ
N
φ
→
P
⊑
(
▷
auth_own
γ
a
★
∀
a'
,
✓
(
a
⋅
a'
)
★
▷
φ
(
a
⋅
a'
)
-
★
■
✓
(
a
⋅
a'
)
★
▷
φ
(
a
⋅
a'
)
-
★
fsa
(
E
∖
nclose
N
)
(
λ
x
,
∃
L
Lv
(
Hup
:
LocalUpdate
Lv
L
),
■
(
Lv
a
∧
✓
(
L
a
⋅
a'
))
★
▷
φ
(
L
a
⋅
a'
)
★
(
auth_own
γ
(
L
a
)
-
★
Ψ
x
)))
→
...
...
@@ -124,7 +121,7 @@ Section auth.
apply
(
fsa_strip_pvs
fsa
).
apply
exist_elim
=>
a'
.
rewrite
(
forall_elim
a'
).
rewrite
[(
▷
_
★
_
)%
I
]
comm
.
eapply
wand_apply_r
;
first
(
by
eapply
(
wand_frame_l
(
own
γ
_
)))
;
last
first
.
{
rewrite
assoc
[(
_
★
own
_
_
)%
I
]
comm
-
assoc
.
done
.
}
{
rewrite
assoc
[(
_
★
own
_
_
)%
I
]
comm
-
assoc
discrete_valid
.
done
.
}
rewrite
fsa_frame_l
.
apply
(
fsa_mono_pvs
fsa
)=>
x
.
rewrite
sep_exist_l
;
apply
exist_elim
=>
L
.
...
...
@@ -141,7 +138,7 @@ Section auth.
nclose
N
⊆
E
→
P
⊑
auth_ctx
γ
N
φ
→
P
⊑
(
▷
auth_own
γ
a
★
(
∀
a'
,
✓
(
a
⋅
a'
)
★
▷
φ
(
a
⋅
a'
)
-
★
■
✓
(
a
⋅
a'
)
★
▷
φ
(
a
⋅
a'
)
-
★
fsa
(
E
∖
nclose
N
)
(
λ
x
,
■
(
Lv
a
∧
✓
(
L
a
⋅
a'
))
★
▷
φ
(
L
a
⋅
a'
)
★
(
auth_own
γ
(
L
a
)
-
★
Ψ
x
))))
→
...
...
Write
Preview
Supports
Markdown
0%
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!
Cancel
Please
register
or
sign in
to comment