Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Iris
RefinedC
Commits
ef38ef58
Commit
ef38ef58
authored
Jul 12, 2021
by
Michael Sammler
Browse files
change ty_layout to ty_has_layout
parent
f7d127fd
Pipeline
#50380
passed with stage
in 16 minutes and 35 seconds
Changes
49
Pipelines
2
Hide whitespace changes
Inline
Sidebyside
examples/proofs/btree/generated_spec.v
View file @
ef38ef58
...
...
@@ 68,7 +68,6 @@ Section spec.
Global
Program
Instance
btree_t_rmovable
:
RMovable
btree_t
:
=
{
rmovable
patt__
:
=
movable_eq
_
_
(
btree_t_unfold
patt__
)
}.
Next
Obligation
.
solve_ty_layout_eq
.
Qed
.
Global
Instance
btree_t_simplify_hyp_place_inst_generated
l_
β
_
patt__
:
SimplifyHypPlace
l_
β
_
(
patt__
@
btree_t
)%
I
(
Some
100
%
N
)
:
=
...
...
examples/proofs/flags/generated_spec.v
View file @
ef38ef58
...
...
@@ 51,7 +51,6 @@ Section spec.
Global
Program
Instance
flags_rmovable
:
RMovable
flags
:
=
{
rmovable
patt__
:
=
movable_eq
_
_
(
flags_unfold
patt__
)
}.
Next
Obligation
.
solve_ty_layout_eq
.
Qed
.
Global
Instance
flags_simplify_hyp_place_inst_generated
l_
β
_
patt__
:
SimplifyHypPlace
l_
β
_
(
patt__
@
flags
)%
I
(
Some
100
%
N
)
:
=
...
...
examples/proofs/latch/generated_spec.v
View file @
ef38ef58
...
...
@@ 33,7 +33,6 @@ Section spec.
Global
Program
Instance
latch_rmovable
:
RMovable
latch
:
=
{
rmovable
patt__
:
=
movable_eq
_
_
(
latch_unfold
patt__
)
}.
Next
Obligation
.
solve_ty_layout_eq
.
Qed
.
Global
Instance
latch_simplify_hyp_place_inst_generated
l_
β
_
patt__
:
SimplifyHypPlace
l_
β
_
(
patt__
@
latch
)%
I
(
Some
100
%
N
)
:
=
...
...
examples/proofs/latch/latch_def.v
View file @
ef38ef58
...
...
@@ 13,7 +13,8 @@ Section type.
l
↦
LATCH_INIT
={
E
}=
∗
l
◁ₗ
{
Shr
}
P
@
latch
.
Proof
.
iIntros
(?
?)
"Hl"
.
iApply
ty_share
=>
//.
unshelve
iApply
(@
ty_ref
with
"[] Hl"
)
=>
//.
apply
_
.
done
.
iApply
ty_share
=>
//.
unshelve
iApply
(@
ty_ref
with
"[] Hl"
)
=>
//.
{
apply
_
.
}
{
solve_goal
.
}
rewrite
/
ty_own_val
/=.
repeat
iSplit
=>
//.
rewrite
/
ty_own_val
/=/
ty_own_val
/=.
iSplit
=>
//.
by
iExists
false
.
Qed
.
End
type
.
examples/proofs/lock/generated_spec.v
View file @
ef38ef58
...
...
@@ 73,7 +73,6 @@ Section spec.
Global
Program
Instance
lock_test_rmovable
:
RMovable
lock_test
:
=
{
rmovable
patt__
:
=
movable_eq
_
_
(
lock_test_unfold
patt__
)
}.
Next
Obligation
.
solve_ty_layout_eq
.
Qed
.
Global
Instance
lock_test_simplify_hyp_place_inst_generated
l_
β
_
patt__
:
SimplifyHypPlace
l_
β
_
(
patt__
@
lock_test
)%
I
(
Some
100
%
N
)
:
=
...
...
examples/proofs/malloc1/generated_spec.v
View file @
ef38ef58
...
...
@@ 39,7 +39,6 @@ Section spec.
Global
Program
Instance
freelist_t_rmovable
(
entry_size
:
nat
)
:
RMovable
(
freelist_t
entry_size
)
:
=
{
rmovable
patt__
:
=
movable_eq
_
_
(
freelist_t_unfold
entry_size
patt__
)
}.
Next
Obligation
.
solve_ty_layout_eq
.
Qed
.
Global
Instance
freelist_t_simplify_hyp_place_inst_generated
l_
β
_
(
entry_size
:
nat
)
patt__
:
SimplifyHypPlace
l_
β
_
(
patt__
@
freelist_t
entry_size
)%
I
(
Some
100
%
N
)
:
=
...
...
@@ 104,7 +103,6 @@ Section spec.
Global
Program
Instance
slab_rmovable
(
entry_size
:
nat
)
:
RMovable
(
slab
entry_size
)
:
=
{
rmovable
patt__
:
=
movable_eq
_
_
(
slab_unfold
entry_size
patt__
)
}.
Next
Obligation
.
solve_ty_layout_eq
.
Qed
.
Global
Instance
slab_simplify_hyp_place_inst_generated
l_
β
_
(
entry_size
:
nat
)
patt__
:
SimplifyHypPlace
l_
β
_
(
patt__
@
slab
entry_size
)%
I
(
Some
100
%
N
)
:
=
...
...
examples/proofs/mpool/generated_spec.v
View file @
ef38ef58
...
...
@@ 61,7 +61,6 @@ Section spec.
Global
Program
Instance
mpool_chunk_t_rmovable
(
entry_size
:
nat
)
:
RMovable
(
mpool_chunk_t
entry_size
)
:
=
{
rmovable
patt__
:
=
movable_eq
_
_
(
mpool_chunk_t_unfold
entry_size
patt__
)
}.
Next
Obligation
.
solve_ty_layout_eq
.
Qed
.
Global
Instance
mpool_chunk_t_simplify_hyp_place_inst_generated
l_
β
_
(
entry_size
:
nat
)
patt__
:
SimplifyHypPlace
l_
β
_
(
patt__
@
mpool_chunk_t
entry_size
)%
I
(
Some
100
%
N
)
:
=
...
...
@@ 112,7 +111,6 @@ Section spec.
Global
Program
Instance
mpool_entry_t_rmovable
(
entry_size
:
nat
)
:
RMovable
(
mpool_entry_t
entry_size
)
:
=
{
rmovable
patt__
:
=
movable_eq
_
_
(
mpool_entry_t_unfold
entry_size
patt__
)
}.
Next
Obligation
.
solve_ty_layout_eq
.
Qed
.
Global
Instance
mpool_entry_t_simplify_hyp_place_inst_generated
l_
β
_
(
entry_size
:
nat
)
patt__
:
SimplifyHypPlace
l_
β
_
(
patt__
@
mpool_entry_t
entry_size
)%
I
(
Some
100
%
N
)
:
=
...
...
@@ 197,7 +195,6 @@ Section spec.
Global
Program
Instance
mpool_rmovable
(
entry_size
:
nat
)
:
RMovable
(
mpool
entry_size
)
:
=
{
rmovable
patt__
:
=
movable_eq
_
_
(
mpool_unfold
entry_size
patt__
)
}.
Next
Obligation
.
solve_ty_layout_eq
.
Qed
.
Global
Instance
mpool_simplify_hyp_place_inst_generated
l_
β
_
(
entry_size
:
nat
)
patt__
:
SimplifyHypPlace
l_
β
_
(
patt__
@
mpool
entry_size
)%
I
(
Some
100
%
N
)
:
=
...
...
examples/proofs/mpool_simpl/generated_spec.v
View file @
ef38ef58
...
...
@@ 37,7 +37,6 @@ Section spec.
Global
Program
Instance
mpool_entry_rmovable
:
RMovable
mpool_entry
:
=
{
rmovable
patt__
:
=
movable_eq
_
_
(
mpool_entry_unfold
patt__
)
}.
Next
Obligation
.
solve_ty_layout_eq
.
Qed
.
Global
Instance
mpool_entry_simplify_hyp_place_inst_generated
l_
β
_
patt__
:
SimplifyHypPlace
l_
β
_
(
patt__
@
mpool_entry
)%
I
(
Some
100
%
N
)
:
=
...
...
@@ 82,7 +81,6 @@ Section spec.
Global
Program
Instance
mpool_rmovable
:
RMovable
mpool
:
=
{
rmovable
patt__
:
=
movable_eq
_
_
(
mpool_unfold
patt__
)
}.
Next
Obligation
.
solve_ty_layout_eq
.
Qed
.
Global
Instance
mpool_simplify_hyp_place_inst_generated
l_
β
_
patt__
:
SimplifyHypPlace
l_
β
_
(
patt__
@
mpool
)%
I
(
Some
100
%
N
)
:
=
...
...
examples/proofs/mutable_map/generated_spec.v
View file @
ef38ef58
...
...
@@ 48,19 +48,6 @@ Section spec.
Next
Obligation
.
done
.
Qed
.
Next
Obligation
.
by
case
;
eauto
.
Qed
.
Global
Program
Instance
movable_item_tunion_info
:
MovableTUnion
item_tunion_info
:
=
{
mti_movable
c
:
=
match
c
with

Empty
=>
_

Entry
key
ty
=>
_

Tombstone
key
=>
_
end
;
}.
Next
Obligation
.
simpl
.
apply
_
.
Defined
.
Next
Obligation
.
simpl
.
apply
_
.
Defined
.
Next
Obligation
.
simpl
.
apply
_
.
Defined
.
Next
Obligation
.
by
case
=>
/=
;
apply
_
.
Qed
.
Program
Definition
item
:
rtype
:
=
tunion
item_tunion_info
.
(* Definition of type [fixed_size_map]. *)
...
...
@@ 110,7 +97,6 @@ Section spec.
Global
Program
Instance
fixed_size_map_rmovable
:
RMovable
fixed_size_map
:
=
{
rmovable
patt__
:
=
movable_eq
_
_
(
fixed_size_map_unfold
patt__
)
}.
Next
Obligation
.
solve_ty_layout_eq
.
Qed
.
Global
Instance
fixed_size_map_simplify_hyp_place_inst_generated
l_
β
_
patt__
:
SimplifyHypPlace
l_
β
_
(
patt__
@
fixed_size_map
)%
I
(
Some
100
%
N
)
:
=
...
...
examples/proofs/paper_example_2_1/generated_spec.v
View file @
ef38ef58
...
...
@@ 48,7 +48,6 @@ Section spec.
Global
Program
Instance
mem_t_rmovable
:
RMovable
mem_t
:
=
{
rmovable
patt__
:
=
movable_eq
_
_
(
mem_t_unfold
patt__
)
}.
Next
Obligation
.
solve_ty_layout_eq
.
Qed
.
Global
Instance
mem_t_simplify_hyp_place_inst_generated
l_
β
_
patt__
:
SimplifyHypPlace
l_
β
_
(
patt__
@
mem_t
)%
I
(
Some
100
%
N
)
:
=
...
...
examples/proofs/paper_example_2_2/generated_spec.v
View file @
ef38ef58
...
...
@@ 58,7 +58,6 @@ Section spec.
Global
Program
Instance
chunks_t_rmovable
:
RMovable
chunks_t
:
=
{
rmovable
patt__
:
=
movable_eq
_
_
(
chunks_t_unfold
patt__
)
}.
Next
Obligation
.
solve_ty_layout_eq
.
Qed
.
Global
Instance
chunks_t_simplify_hyp_place_inst_generated
l_
β
_
patt__
:
SimplifyHypPlace
l_
β
_
(
patt__
@
chunks_t
)%
I
(
Some
100
%
N
)
:
=
...
...
examples/proofs/queue/generated_spec.v
View file @
ef38ef58
...
...
@@ 45,7 +45,6 @@ Section spec.
Global
Program
Instance
queue_elem_rmovable
(
cont
:
type
)
:
RMovable
(
queue_elem
cont
)
:
=
{
rmovable
patt__
:
=
movable_eq
_
_
(
queue_elem_unfold
cont
patt__
)
}.
Next
Obligation
.
solve_ty_layout_eq
.
Qed
.
Global
Instance
queue_elem_simplify_hyp_place_inst_generated
l_
β
_
(
cont
:
type
)
patt__
:
SimplifyHypPlace
l_
β
_
(
patt__
@
queue_elem
cont
)%
I
(
Some
100
%
N
)
:
=
...
...
@@ 96,7 +95,6 @@ Section spec.
Global
Program
Instance
queue_rmovable
:
RMovable
queue
:
=
{
rmovable
patt__
:
=
movable_eq
_
_
(
queue_unfold
patt__
)
}.
Next
Obligation
.
solve_ty_layout_eq
.
Qed
.
Global
Instance
queue_simplify_hyp_place_inst_generated
l_
β
_
patt__
:
SimplifyHypPlace
l_
β
_
(
patt__
@
queue
)%
I
(
Some
100
%
N
)
:
=
...
...
examples/proofs/reverse/generated_spec.v
View file @
ef38ef58
...
...
@@ 47,7 +47,6 @@ Section spec.
Global
Program
Instance
list_t_rmovable
:
RMovable
list_t
:
=
{
rmovable
patt__
:
=
movable_eq
_
_
(
list_t_unfold
patt__
)
}.
Next
Obligation
.
solve_ty_layout_eq
.
Qed
.
Global
Instance
list_t_simplify_hyp_place_inst_generated
l_
β
_
patt__
:
SimplifyHypPlace
l_
β
_
(
patt__
@
list_t
)%
I
(
Some
100
%
N
)
:
=
...
...
examples/proofs/simple_union/generated_spec.v
View file @
ef38ef58
...
...
@@ 54,19 +54,6 @@ Section spec.
Next
Obligation
.
done
.
Qed
.
Next
Obligation
.
by
case
;
eauto
.
Qed
.
Global
Program
Instance
movable_item_tunion_info
:
MovableTUnion
item_tunion_info
:
=
{
mti_movable
c
:
=
match
c
with

Empty
=>
_

Entry
key
ty
=>
_

Tombstone
key
=>
_
end
;
}.
Next
Obligation
.
simpl
.
apply
_
.
Defined
.
Next
Obligation
.
simpl
.
apply
_
.
Defined
.
Next
Obligation
.
simpl
.
apply
_
.
Defined
.
Next
Obligation
.
by
case
=>
/=
;
apply
_
.
Qed
.
Program
Definition
item
:
rtype
:
=
tunion
item_tunion_info
.
(* Type definitions. *)
...
...
examples/proofs/talk_demo2/generated_spec.v
View file @
ef38ef58
...
...
@@ 47,7 +47,6 @@ Section spec.
Global
Program
Instance
list_t_rmovable
:
RMovable
list_t
:
=
{
rmovable
patt__
:
=
movable_eq
_
_
(
list_t_unfold
patt__
)
}.
Next
Obligation
.
solve_ty_layout_eq
.
Qed
.
Global
Instance
list_t_simplify_hyp_place_inst_generated
l_
β
_
patt__
:
SimplifyHypPlace
l_
β
_
(
patt__
@
list_t
)%
I
(
Some
100
%
N
)
:
=
...
...
examples/proofs/talk_demo3/generated_spec.v
View file @
ef38ef58
...
...
@@ 51,7 +51,6 @@ Section spec.
Global
Program
Instance
list_t_rmovable
:
RMovable
list_t
:
=
{
rmovable
patt__
:
=
movable_eq
_
_
(
list_t_unfold
patt__
)
}.
Next
Obligation
.
solve_ty_layout_eq
.
Qed
.
Global
Instance
list_t_simplify_hyp_place_inst_generated
l_
β
_
patt__
:
SimplifyHypPlace
l_
β
_
(
patt__
@
list_t
)%
I
(
Some
100
%
N
)
:
=
...
...
frontend/coq_pp.ml
View file @
ef38ef58
...
...
@@ 883,7 +883,7 @@ let pp_spec : string > import list > inlined_code >
id
pp_params
params
(
pp_id_args
true
id
)
par_names
;
pp
" { rmovable patt__ := movable_eq _ _ (%s_unfold"
id
;
List
.
iter
(
fun
n
>
pp
" %s"
n
)
par_names
;
pp
" patt__) }.
@;Next Obligation. solve_ty_layout_eq. Qed.
\n
"
;
pp
" patt__) }.
\n
"
;
in
if
not
annot
.
st_immovable
then
pp_movable_instance
()
;
...
...
@@ 1037,21 +1037,6 @@ let pp_spec : string > import list > inlined_code >
pp
"}.@;"
;
pp
"Next Obligation. done. Qed.@;"
;
pp
"Next Obligation. by case; eauto. Qed.
\n
@;"
;
(* Movable instance. *)
pp
"Global Program Instance movable_%s_tunion_info : MovableTUnion \
%s_tunion_info := {@;"
id
id
;
pp
" mti_movable c :=@;"
;
pp
" match c with@;"
;
let
fn
(
_
,
(
c
,
args
)
,
_
)
=
pp
"  %s"
c
;
List
.
iter
(
fun
(
x
,_
)
>
pp
" %s"
x
)
args
;
pp
" => _@;"
in
List
.
iter
fn
union_cases
;
pp
" end;@;"
;
pp
"}.@;"
;
let
fn
_
=
pp
"Next Obligation. simpl. apply _. Defined.@;"
in
List
.
iter
fn
union_cases
;
pp
"Next Obligation. by case => /=; apply _. Qed.
\n
@;"
;
(* Actual definition of the type. *)
pp
"Program Definition %s : rtype := tunion %s_tunion_info."
id
id
in
...
...
linux/casestudies/proofs/page_alloc_find_buddy/generated_spec.v
View file @
ef38ef58
...
...
@@ 45,7 +45,6 @@ Section spec.
Global
Program
Instance
hyp_page_rmovable
:
RMovable
hyp_page
:
=
{
rmovable
patt__
:
=
movable_eq
_
_
(
hyp_page_unfold
patt__
)
}.
Next
Obligation
.
solve_ty_layout_eq
.
Qed
.
Global
Instance
hyp_page_simplify_hyp_place_inst_generated
l_
β
_
patt__
:
SimplifyHypPlace
l_
β
_
(
patt__
@
hyp_page
)%
I
(
Some
100
%
N
)
:
=
...
...
@@ 120,7 +119,6 @@ Section spec.
Global
Program
Instance
hyp_pool_rmovable
:
RMovable
hyp_pool
:
=
{
rmovable
patt__
:
=
movable_eq
_
_
(
hyp_pool_unfold
patt__
)
}.
Next
Obligation
.
solve_ty_layout_eq
.
Qed
.
Global
Instance
hyp_pool_simplify_hyp_place_inst_generated
l_
β
_
patt__
:
SimplifyHypPlace
l_
β
_
(
patt__
@
hyp_pool
)%
I
(
Some
100
%
N
)
:
=
...
...
linux/pkvm/proofs/early_alloc/generated_spec.v
View file @
ef38ef58
...
...
@@ 68,7 +68,6 @@ Section spec.
Global
Program
Instance
region_rmovable
:
RMovable
region
:
=
{
rmovable
patt__
:
=
movable_eq
_
_
(
region_unfold
patt__
)
}.
Next
Obligation
.
solve_ty_layout_eq
.
Qed
.
Global
Instance
region_simplify_hyp_place_inst_generated
l_
β
_
patt__
:
SimplifyHypPlace
l_
β
_
(
patt__
@
region
)%
I
(
Some
100
%
N
)
:
=
...
...
linux/pkvm/proofs/spinlock/spinlock_proof.v
View file @
ef38ef58
...
...
@@ 4,18 +4,6 @@ From refinedc.linux.pkvm.spinlock Require Import generated_spec.
From
refinedc
.
linux
.
pkvm
.
spinlock
Require
Import
spinlock_def
.
Set
Default
Proof
Using
"Type"
.
(* TODO: figure out if this is what we want and move to type.v *)
Theorem
ty_deref_full
`
{!
typeG
Σ
}
(
l
:
loc
)
(
ty
:
type
)
`
{!
Movable
ty
}
:
l
◁ₗ
ty

∗
∃
v
,
⌜
l
`
has_layout_loc
`
ty_layout
ty
⌝
∗
⌜
v
`
has_layout_val
`
ty_layout
ty
⌝
∗
l
↦
v
∗
v
◁ᵥ
ty
.
Proof
.
iIntros
"Hl"
.
iDestruct
(
ty_aligned
with
"Hl"
)
as
%?.
iDestruct
(
ty_deref
with
"Hl"
)
as
(
v
)
"[Hl Hv]"
.
iDestruct
(
ty_size_eq
with
"Hv"
)
as
%?.
iExists
v
.
eauto
with
iFrame
.
Qed
.
Section
proofs
.
Context
`
{!
typeG
Σ
}
`
{!
globalG
Σ
}
`
{!
lockG
Σ
}
`
{!
spinlockG
Σ
}.
...
...
@@ 85,9 +73,9 @@ Section proofs.
iInv
"Hinv"
as
">Inv"
"Hclose_inv"
.
iDestruct
"Inv"
as
(
owner
next
)
"(%&Howner&Hnext&Hrest)"
.
iApply
fupd_mask_intro
;
first
solve_ndisj
.
iIntros
"Hclose"
.
iDestruct
(
ty_aligned
with
"Hnext"
)
as
%?.
iDestruct
(
ty_deref
with
"Hnext"
)
as
(
v
)
"[Hl Hv]"
.
iDestruct
(
ty_size_eq
with
"Hv"
)
as
%?.
iDestruct
(
ty_aligned
with
"Hnext"
)
as
%?
;
[
done
]
.
iDestruct
(
ty_deref
with
"Hnext"
)
as
(
v
)
"[Hl Hv]"
;
[
done
]
.
iDestruct
(
ty_size_eq
with
"Hv"
)
as
%?
;
[
done
]
.
iExists
1
%
Qp
,
v
,
_
,
(
t2mt
(
next
@
int
u16
))%
I
.
repeat
liRStep
;
liShow
.
iSplit
;
first
by
iNext
.
iIntros
"!> Hl"
.
iMod
"Hclose"
as
"_"
.
iMod
(
"Hclose_inv"
with
"[Howner Hrest Hl Hv]"
)
as
"_"
.
...
...
@@ 116,9 +104,9 @@ Section proofs.
iInv
"Hinv"
as
">Inv"
"Hclose_inv"
.
iDestruct
"Inv"
as
(
owner
next
)
"(%&Howner&Hnext&Hrest)"
.
iApply
fupd_mask_intro
;
first
solve_ndisj
.
iIntros
"Hclose"
.
iDestruct
(
ty_aligned
with
"Hnext"
)
as
%?.
iDestruct
(
ty_deref
with
"Hnext"
)
as
(
v'
)
"[Hl Hv]"
.
iDestruct
(
ty_size_eq
with
"Hv"
)
as
%?.
iDestruct
(
ty_aligned
with
"Hnext"
)
as
%?
;
[
done
]
.
iDestruct
(
ty_deref
with
"Hnext"
)
as
(
v'
)
"[Hl Hv]"
;
[
done
]
.
iDestruct
(
ty_size_eq
with
"Hv"
)
as
%?
;
[
done
]
.
iExists
1
%
Qp
,
v'
,
_
,
(
t2mt
(
next
@
int
u16
))%
I
.
repeat
liRStep
;
liShow
.
iSplit
;
first
by
iNext
.
iIntros
"!> Hl"
.
iMod
"Hclose"
as
"_"
.
iMod
(
"Hclose_inv"
with
"[Howner Hrest Hl Hv]"
)
as
"_"
.
...
...
@@ 187,9 +175,9 @@ Section proofs.
iInv
"Hinv"
as
">Inv"
"Hclose_inv"
.
iDestruct
"Inv"
as
(
owner
next
)
"(%&Howner&Hnext&Hrest)"
.
iApply
fupd_mask_intro
;
first
solve_ndisj
.
iIntros
"Hclose"
.
iDestruct
(
ty_aligned
with
"Hnext"
)
as
%?.
iDestruct
(
ty_deref
with
"Hnext"
)
as
(
v'
)
"[Hl Hv]"
.
iDestruct
(
ty_size_eq
with
"Hv"
)
as
%?.
iDestruct
(
ty_aligned
with
"Hnext"
)
as
%?
;
[
done
]
.
iDestruct
(
ty_deref
with
"Hnext"
)
as
(
v'
)
"[Hl Hv]"
;
[
done
]
.
iDestruct
(
ty_size_eq
with
"Hv"
)
as
%?
;
[
done
]
.
iExists
1
%
Qp
,
v'
,
_
,
(
t2mt
(
next
@
int
u16
))%
I
.
repeat
liRStep
;
liShow
.
iSplit
;
first
by
iNext
.
iIntros
"!> Hl"
.
iMod
"Hclose"
as
"_"
.
iMod
(
"Hclose_inv"
with
"[Howner Hrest Hl Hv]"
)
as
"_"
.
...
...
@@ 263,9 +251,9 @@ Section proofs.
iInv
"Hinv"
as
">Inv"
"Hclose_inv"
.
iDestruct
"Inv"
as
(
owner
next
)
"([%%]&Howner&Hnext&Hrest)"
.
iApply
fupd_mask_intro
;
first
solve_ndisj
.
iIntros
"Hclose"
.
iDestruct
(
ty_aligned
with
"Howner"
)
as
%?.
iDestruct
(
ty_deref
with
"Howner"
)
as
(
w
)
"[Hl Hv]"
.
iDestruct
(
ty_size_eq
with
"Hv"
)
as
%?.
iDestruct
(
ty_aligned
with
"Howner"
)
as
%?
;
[
done
]
.
iDestruct
(
ty_deref
with
"Howner"
)
as
(
w
)
"[Hl Hv]"
;
[
done
]
.
iDestruct
(
ty_size_eq
with
"Hv"
)
as
%?
;
[
done
]
.
iExists
1
%
Qp
,
w
,
_
,
(
t2mt
(
owner
@
int
u16
))%
I
.
repeat
liRStep
;
liShow
.
iSplit
;
first
by
iNext
.
iIntros
"!> Hl"
.
destruct
(
decide
(
i
≠
owner
)).
...
...
@@ 283,7 +271,7 @@ Section proofs.
{
rewrite
/
ty_own_val
/=.
by
iDestruct
"Hv"
as
%
Hv
%
val_to_Z_in_range
.
}
iAssert
(
⌜
owner
<
next
⌝
)%
I
as
%?.
{
destruct
(
decide
(
owner
<
next
))
;
first
done
.
iExFalso
.
iDestruct
(
ty_size_eq
with
"Hv"
)
as
%?.
iDestruct
(
ty_size_eq
with
"Hv"
)
as
%?
;
[
done
]
.
iDestruct
(
ticket_not_NO_TICKET
with
"Hticket"
)
as
%
Howner
.
iApply
(
ticket_already_in_range
with
"[] Hr2 Hticket"
).
iPureIntro
.
clear
Q
.
apply
elem_of_seqZ
.
lia
.
}
...
...
@@ 352,9 +340,9 @@ Section proofs.
(* We have the token: we are the owner. *)
iDestruct
(
owner_auth_agree
with
"H● H◯"
)
as
%<.
(* We perform the read. *)
iDestruct
(
ty_aligned
with
"Howner"
)
as
%?.
iDestruct
(
ty_deref
with
"Howner"
)
as
(
v
)
"[Hl Hv]"
.
iDestruct
(
ty_size_eq
with
"Hv"
)
as
%?.
iDestruct
(
ty_aligned
with
"Howner"
)
as
%?
;
[
done
]
.
iDestruct
(
ty_deref
with
"Howner"
)
as
(
v
)
"[Hl Hv]"
;
[
done
]
.
iDestruct
(
ty_size_eq
with
"Hv"
)
as
%?
;
[
done
]
.
iExists
1
%
Qp
,
v
,
_
,
(
t2mt
(
owner
@
int
u16
))%
I
.
repeat
liRStep
;
liShow
.
iSplit
;
first
by
iNext
.
iIntros
"!> Hl"
.
(* We must close the invariant. *)
...
...
@@ 368,7 +356,7 @@ Section proofs.
+
(* We have the last ticket. The next owner will be 0, we update. *)
(* We must open the invariant again. *)
iExists
(
Shr
,
place
_
)
;
iSplitR
;
first
by
simpl
.
rewrite
/
typed_write_end
;
iIntros
"??"
.
rewrite
/
typed_write_end
;
iIntros
"?
_
?"
.
iInv
"Hinv"
as
">Inv"
"Hclose_inv"
.
iDestruct
"Inv"
as
(
owner'
next'
)
"([%%]&Howner&Hnext&H◯&Htk1&Htk2&Hcases)"
.
(* We have the token: we are the owner and our ticket is in [Hcases]. *)
...
...
@@ 381,12 +369,12 @@ Section proofs.
iApply
fupd_mask_intro
;
first
solve_ndisj
.
iIntros
"Hclose"
.
(* Learn that [next'] actually is [max_int u16]. *)
iAssert
⌜
next'
=
max_int
u16
⌝
%
I
as
%>.
{
iDestruct
(
ty_deref
with
"Hnext"
)
as
(
w
)
"[_ H]"
.
iDestruct
"H"
as
%
Hnext
.
{
iDestruct
(
ty_deref
with
"Hnext"
)
as
(
w
)
"[_ H]"
;
[
done
]
.
iDestruct
"H"
as
%
Hnext
.
iPureIntro
.
apply
val_to_Z_in_range
in
Hnext
as
[??].
lia
.
}
(* We perform the write and close the invariant. *)
iDestruct
(
ty_aligned
with
"Howner"
)
as
%?.
iDestruct
(
ty_deref
with
"Howner"
)
as
(
v'
)
"[Hl Hv]"
.
iDestruct
(
ty_size_eq
with
"Hv"
)
as
%?.
iDestruct
(
ty_aligned
with
"Howner"
)
as
%?
;
[
done
]
.
iDestruct
(
ty_deref
with
"Howner"
)
as
(
v'
)
"[Hl Hv]"
;
[
done
]
.
iDestruct
(
ty_size_eq
with
"Hv"
)
as
%?
;
[
done
]
.
iSplitL
"Hl"
.
{
iExists
_
.
by
iFrame
"Hl"
.
}
iIntros
"!> Hl"
.
iRename
select
(
_
◁ᵥ
0
@
int
u16
)%
I
into
"H0"
.
...
...
@@ 400,16 +388,17 @@ Section proofs.
(* We have all the tickets, let's combine them. *)
iAssert
(
ticket_range
id
0
(
LAST_TICKET
+
1
))
with
"[Htk1 Htk2 Hticket]"
as
"Htk"
.
{
iDestruct
(
ticket_range_insert_r
with
"Htk1 Hticket"
)
as
"Hr"
=>
//.
}
iExists
(
place
_
)
;
iSplitR
;
first
by
simpl
.
(* Run the automation up to the write to the [next] field, open invariant. *)
repeat
liRStep
;
liShow
.
iExists
(
Shr
,
place
_
)
;
iSplitR
;
first
by
simpl
.
rewrite
/
typed_write_end
;
iIntros
"?
?"
.
rewrite
/
typed_write_end
;
iIntros
"?
?
?"
.
iInv
"Hinv"
as
">Inv"
"Hclose_inv"
.
iDestruct
"Inv"
as
(
owner'
next''
)
"([%%]&Howner&Hnext&H◯&Htr1&Htr2&Hcases)"
.
(* We can get [owner' = 0] since we have all the tickets. *)
iAssert
⌜
owner'
=
0
⌝
%
I
as
%>.
{
destruct
(
decide
(
owner'
=
0
))
=>
//.
iExFalso
.
iDestruct
(
ty_deref
with
"Howner"
)
as
(?)
"[? Hv]"
.
iDestruct
(
ty_deref
with
"Howner"
)
as
(?)
"[? Hv]"
;
[
done
]
.
iDestruct
"Hv"
as
%
Howner
%
val_to_Z_in_range
.
destruct
Howner
as
[
Howner
?].
iDestruct
(
overlaping_ticket_ranges
with
"[] Htk Htr1"
)
as
"$"
.
...
...
@@ 428,9 +417,9 @@ Section proofs.
iExists
next''
.
iPureIntro
.
split
;
apply
elem_of_seqZ
;
lia
.
}
(* We perform the write and close the invariant. *)
iApply
fupd_mask_intro
;
first
solve_ndisj
.
iIntros
"Hclose"
.
iDestruct
(
ty_aligned
with
"Hnext"
)
as
%?.
iDestruct
(
ty_deref
with
"Hnext"
)
as
(
v''
)
"[Hl Hv]"
.
iDestruct
(
ty_size_eq
with
"Hv"
)
as
%?.
iDestruct
(
ty_aligned
with
"Hnext"
)
as
%?
;
[
done
]
.
iDestruct
(
ty_deref
with
"Hnext"
)
as
(
v''
)
"[Hl Hv]"
;
[
done
]
.
iDestruct
(
ty_size_eq
with
"Hv"
)
as
%?
;
[
done
]
.
iSplitL
"Hl"
.
{
iExists
_
.
by
iFrame
"Hl"
.
}
iIntros
"!> Hl"
.
iRename
select
(
ticket
◁ₗ
_
)%
I
into
"Hticket_var"
.
...
...
@@ 444,7 +433,7 @@ Section proofs.
+
(* We do not have the last ticket, we do not reset the queue. *)
(* We must open the invariant again. *)
iExists
(
Shr
,
place
_
)
;
iSplitR
;
first
by
simpl
.
rewrite
/
typed_read_end
;
iIntros
"? ?"
.
rewrite
/
typed_read_end
;
iIntros
"?
?
?"
.
iInv
"Hinv"
as
">Inv"
"Hclose_inv"
.
iDestruct
"Inv"
as
(
owner'
next'
)
"([% %]&Howner&Hnext&H◯&Htk1&Htk2&Hcases)"
.
(* We have the token: we are the owner and our ticket is in [Hcases]. *)
...
...
@@ 456,9 +445,9 @@ Section proofs.
iMod
(
owner_auth_update
_
_
_
_
(
owner
+
1
)
with
"H● H◯"
)
as
"[H● H◯]"
.
iApply
fupd_mask_intro
;
first
solve_ndisj
.
iIntros
"Hclose"
.
(* We perform the write and close the invariant. *)
iDestruct
(
ty_aligned
with
"Howner"
)
as
%?.
iDestruct
(
ty_deref
with
"Howner"
)
as
(
v'
)
"[Hl Hv]"
.
iDestruct
(
ty_size_eq
with
"Hv"
)
as
%?.
iDestruct
(
ty_aligned
with
"Howner"
)
as
%?
;
[
done
]
.
iDestruct
(
ty_deref
with
"Howner"
)
as
(
v'
)
"[Hl Hv]"
;
[
done
]
.
iDestruct
(
ty_size_eq
with
"Hv"
)
as
%?
;
[
done
]
.
iDestruct
"Hv"
as
%?%
val_to_Z_in_range
.
iSplitL
"Hl"
.
{
iExists
_
.
by
iFrame
"Hl"
.
}
iIntros
"!> Hl"
.
...
...
Prev
1
2
3
Next
Write
Preview
Supports
Markdown
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