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
RefinedC
Commits
a8710147
Commit
a8710147
authored
Sep 16, 2021
by
Rodolphe Lepigre
Browse files
Generalize the [boolean] type.
parent
364c4ae1
Pipeline
#53829
passed with stage
in 31 minutes and 13 seconds
Changes
11
Pipelines
6
Hide whitespace changes
Inline
Side-by-side
examples/proofs/latch/latch_def.v
View file @
a8710147
...
...
@@ -12,9 +12,15 @@ Section type.
l
`
has_layout_loc
`
struct_latch
→
l
↦
LATCH_INIT
={
E
}=
∗
l
◁ₗ
{
Shr
}
P
@
latch
.
Proof
.
iIntros
(?
?)
"Hl"
.
iApply
ty_share
=>
//.
unshelve
iApply
(@
ty_ref
with
"[] Hl"
).
{
apply
_
.
}
{
apply
:
(
UntypedOp
struct_latch
).
}
{
apply
:
MCNone
.
}
{
solve_goal
.
}
{
done
.
}
rewrite
/
ty_own_val
/=.
repeat
iSplit
=>
//.
rewrite
/
ty_own_val
/=/
ty_own_val
/=.
iSplit
=>
//.
by
iExists
false
.
iIntros
(?
?)
"Hl"
.
iApply
ty_share
=>
//.
unshelve
iApply
(@
ty_ref
with
"[] Hl"
).
{
apply
_
.
}
{
apply
:
(
UntypedOp
struct_latch
).
}
{
apply
:
MCNone
.
}
{
solve_goal
.
}
{
done
.
}
rewrite
/
ty_own_val
/=.
repeat
iSplit
=>
//.
rewrite
/
ty_own_val
/=
/
ty_own_val
/=.
iSplit
=>
//.
iExists
false
.
iSplit
;
last
done
.
by
iExists
_
.
Qed
.
End
type
.
linux/casestudies/proofs/pgtable/pgtable_lemmas.v
View file @
a8710147
...
...
@@ -145,10 +145,6 @@ Ltac simpl_bool_hyp :=
assert
(
b
=
false
)
by
apply
negb_true_iff
;
clear
H
|
[
H
:
negb
?b
=
false
|-
_
]
=>
assert
(
b
=
true
)
by
apply
negb_false_iff
;
clear
H
|
[
H
:
0
=
Z_of_bool
?b
|-
_
]
=>
assert
(
b
=
false
)
by
(
by
apply
Z_of_bool_false
)
;
clear
H
|
[
H
:
0
≠
Z_of_bool
?b
|-
_
]
=>
assert
(
b
=
true
)
by
(
by
apply
Z_of_bool_true
)
;
clear
H
|
[
H
:
bf_cons
?a
1
(
Z_of_bool
?b
)
bf_nil
=
0
|-
_
]
=>
assert
(
b
=
false
)
by
(
by
apply
(
bf_cons_bool_singleton_false_iff
a
b
))
;
clear
H
|
[
H
:
bf_cons
?a
1
(
Z_of_bool
?b
)
bf_nil
≠
0
|-
_
]
=>
...
...
linux/pkvm/proofs/spinlock/spinlock_proof.v
View file @
a8710147
...
...
@@ -84,7 +84,7 @@ Section proofs.
-
(* #1 First loop (after the initial run), checking if we got the ticket. *)
destruct
s
.
+
repeat
liRStep
;
liShow
.
iIntros
"Hb"
.
repeat
liRStep
;
liShow
.
2
:
{
destruct
b
=>
//.
iFrame
.
}
repeat
liRStep
;
liShow
.
iDestruct
select
(
hyp_spinlock_t_invariant
_
_
_
)
as
(
owner
next
)
"([%%]&?&?&?&?&?&?)"
.
repeat
liRStep
;
liShow
.
liInst
Hevar
next
.
...
...
@@ -93,7 +93,7 @@ Section proofs.
liInst
Hevar
owner
.
liInst
Hevar0
next
.
repeat
liRStep
;
liShow
.
+
repeat
liRStep
;
liShow
.
iIntros
"Hb"
.
repeat
liRStep
;
liShow
.
2
:
{
destruct
b
=>
//.
iFrame
.
}
repeat
liRStep
;
liShow
.
iExists
(
Shr
,
tytrue
)
;
iSplitR
;
first
by
simpl
.
iDestruct
select
(
inv
_
_
)
as
"#Hinv"
.
iInv
"Hinv"
as
">Inv"
.
...
...
@@ -129,6 +129,7 @@ Section proofs.
iDestruct
select
(
p
at
{
_
}
ₗ
_
◁ᵥ
_
)%
I
as
"[_ ->]"
.
iApply
(
wp_cas_suc_int
with
"Hnext Hticket [$]"
).
{
cbv
.
lia
.
}
done
.
iNext
.
iIntros
"??"
.
iApply
(
"HΦ"
$!
_
(
t2mt
(
true
@
boolean
bool_it
))%
I
)
=>
//.
{
iExists
_
.
done
.
}
repeat
liRStep
;
liShow
.
rewrite
/
hyp_spinlock_t_invariant
.
repeat
liRStep
;
liShow
.
...
...
@@ -151,6 +152,7 @@ Section proofs.
iDestruct
select
(
p
at
{
_
}
ₗ
_
◁ᵥ
_
)%
I
as
"[_ ->]"
.
iApply
(
wp_cas_fail_int
with
"Hnext Hticket [$]"
).
{
cbv
.
lia
.
}
done
.
iNext
.
iIntros
"??"
.
iApply
(
"HΦ"
$!
_
(
t2mt
(
false
@
boolean
bool_it
))%
I
)
=>
//.
{
by
iExists
_
.
}
repeat
liRStep
;
liShow
.
rewrite
/
hyp_spinlock_t_invariant
.
repeat
liRStep
;
liShow
.
...
...
@@ -188,6 +190,7 @@ Section proofs.
iDestruct
select
(
p
at
{
_
}
ₗ
_
◁ᵥ
_
)%
I
as
"[_ ->]"
.
iApply
(
wp_cas_suc_int
with
"Hnext Hticket [$]"
).
{
cbv
.
lia
.
}
done
.
iNext
.
iIntros
"??"
.
iApply
(
"HΦ"
$!
_
(
t2mt
(
true
@
boolean
bool_it
))%
I
)
=>
//.
{
by
iExists
_
.
}
iRename
select
(
p
at
{
struct_hyp_spinlock
}
ₗ
"next"
◁ₗ
_
)%
I
into
"Hnext"
.
iDestruct
"Hrest"
as
"(Hfrag&Hr1&Hr2&Hcases)"
.
iDestruct
(
split_first_ticket
with
"Hr2"
)
as
"[Hticket Hr2]"
.
...
...
@@ -206,6 +209,7 @@ Section proofs.
iDestruct
select
(
p
at
{
_
}
ₗ
_
◁ᵥ
_
)%
I
as
"[_ ->]"
.
iApply
(
wp_cas_fail_int
with
"Hnext Hticket [$]"
).
{
cbv
.
lia
.
}
done
.
iNext
.
iIntros
"??"
.
iApply
(
"HΦ"
$!
_
(
t2mt
(
false
@
boolean
bool_it
))%
I
)
=>
//.
{
by
iExists
_
.
}
iRename
select
(
p
at
{
struct_hyp_spinlock
}
ₗ
_
◁ₗ
_
)%
I
into
"Hnext"
.
iMod
(
"Hclose_inv"
with
"[Howner Hnext Hrest]"
)
as
"_"
.
{
iNext
.
iExists
owner
,
next
.
iFrame
"Howner"
.
iFrame
"Hnext"
.
iFrame
"Hrest"
.
done
.
}
...
...
theories/lithium/simpl_instances.v
View file @
a8710147
...
...
@@ -210,6 +210,16 @@ Proof. split; destruct b; naive_solver. Qed.
Global
Instance
simpl_Z_to_bool_1
(
b
:
bool
)
:
SimplBothRel
(=)
1
(
Z_of_bool
b
)
(
b
=
true
).
Proof
.
split
;
destruct
b
;
naive_solver
.
Qed
.
(* Using a SimplBothRel does not work since [x ≠ y] (i.e., [not (x = y)]) does
not unify with [?R ?x ?y] (Coq's unification is too limited here). This can be
seen by applying [simpl_both_rel_inst2], which given the following error:
[Unable to unify "?Goal1 ?Goal2 ?Goal3" with "0 = Z_of_bool _b_ → False"] *)
(*Global Instance simpl_Z_to_bool_nonzero b: SimplBothRel (≠) 0 (Z_of_bool b) (b = true).*)
Global
Instance
simpl_Z_to_bool_nonzero_1
b
:
SimplBoth
(
Z_of_bool
b
≠
0
)
(
b
=
true
).
Proof
.
by
destruct
b
.
Qed
.
Global
Instance
simpl_Z_to_bool_nonzero_2
b
:
SimplBoth
(
0
≠
Z_of_bool
b
)
(
b
=
true
).
Proof
.
by
destruct
b
.
Qed
.
Global
Instance
simpl_add_eq_0
n
m
:
SimplBothRel
(=)
(
n
+
m
)%
nat
(
0
)%
nat
(
n
=
0
%
nat
∧
m
=
0
%
nat
).
Proof
.
split
;
naive_solver
lia
.
Qed
.
...
...
theories/typing/atomic_bool.v
View file @
a8710147
From
refinedc
.
typing
Require
Export
type
.
From
refinedc
.
typing
Require
Import
programs
int
.
From
refinedc
.
typing
Require
Import
programs
boolean
int
.
Set
Default
Proof
Using
"Type"
.
Definition
atomic_boolN
:
namespace
:
=
nroot
.@
"atomic_boolN"
.
...
...
@@ -52,7 +52,7 @@ Section atomic_bool.
iInv
"Hl"
as
"(%b&>Hb&?)"
"Hclose"
.
iApply
fupd_mask_intro
;
[
set_solver
|].
iIntros
"_"
.
rewrite
/
ty_own
/=.
iDestruct
"Hb"
as
"(%v&%&%&?)"
.
iExists
_
,
_
.
iFrame
.
iPureIntro
.
iDestruct
"Hb"
as
"(%v&%
n&%&%
&%&?)"
.
iExists
_
,
_
.
iFrame
.
iPureIntro
.
erewrite
val_to_Z_length
;
[|
done
].
lia
.
Qed
.
...
...
@@ -166,34 +166,35 @@ Section programs.
destruct
β
.
-
iDestruct
"Hl"
as
(
b
)
"[Hb Hif]"
.
destruct
(
decide
(
b
=
bexp
))
;
subst
.
+
iApply
(
wp_cas_suc_bool
with
"Hb Hlexp"
)
=>
//.
+
iApply
(
wp_cas_suc_bool
ean
with
"Hb Hlexp"
)
=>
//.
iIntros
"!# Hb Hexp"
.
iDestruct
"Hsub"
as
"[Hsub _]"
.
iDestruct
(
"Hsub"
with
"Hif"
)
as
"[Hif HT]"
.
iApply
"HΦ"
.
2
:
iApply
(
"HT"
with
"[Hb Hif] Hexp"
).
done
.
iExists
bnew
.
by
iFrame
.
+
iApply
(
wp_cas_fail_bool
with
"Hb Hlexp"
)
=>
//
.
iIntros
"!#
Hb Hexp"
.
iDestruct
"Hsub"
as
"[_ HT]"
.
iApply
"HΦ"
.
2
:
iApply
(
"HT"
with
"[Hb Hif]"
).
done
.
*
iExists
b
.
iFrame
.
*
by
destruct
b
,
bexp
.
iApply
"HΦ"
;
last
first
.
*
iApply
(
"HT"
with
"[Hb Hif] Hexp"
).
iExists
bnew
.
by
iFrame
.
*
by
iExists
_
.
+
iApply
(
wp_cas_fail_boolean
with
"
Hb H
l
exp"
)
=>
//
.
iIntros
"!# Hb Hexp"
.
iDestruct
"Hsub"
as
"[_ HT]"
.
iApply
"HΦ"
;
last
first
.
*
iApply
(
"HT"
with
"[Hb Hif]"
).
{
iExists
_
.
by
iFrame
.
}
by
destruct
b
,
bexp
.
*
by
iExists
_
.
-
iDestruct
"Hl"
as
(?)
"#Hinv"
.
iInv
"Hinv"
as
"Hb"
.
iDestruct
"Hb"
as
(
b
)
"[>Hmt Hif]"
.
destruct
(
decide
(
b
=
bexp
))
;
subst
.
+
iApply
(
wp_cas_suc_bool
with
"Hmt Hlexp"
)
=>
//.
+
iApply
(
wp_cas_suc_bool
ean
with
"Hmt Hlexp"
)
=>
//.
iIntros
"!# Hb Hexp"
.
iDestruct
"Hsub"
as
"[Hsub _]"
.
iDestruct
(
"Hsub"
with
"Hif"
)
as
"[Hif HT]"
.
iModIntro
.
iSplitL
"Hb Hif"
.
{
iExists
bnew
.
iFrame
.
}
iApply
"HΦ"
.
2
:
iApply
(
"HT"
with
"[] Hexp"
).
done
.
by
iSplit
.
+
iApply
(
wp_cas_fail_bool
with
"Hmt Hlexp"
)
=>
//.
iApply
"HΦ"
;
last
first
.
*
iApply
(
"HT"
with
"[] Hexp"
).
by
iSplit
.
*
by
iExists
_
.
+
iApply
(
wp_cas_fail_boolean
with
"Hmt Hlexp"
)
=>
//.
iIntros
"!# Hb Hexp"
.
iDestruct
"Hsub"
as
"[_ HT]"
.
iModIntro
.
iSplitL
"Hb Hif"
.
{
by
iExists
b
;
iFrame
;
rewrite
/
i2v
Hvnew
.
}
iApply
"HΦ"
.
2
:
iApply
(
"HT"
with
"[]"
).
done
.
*
by
iSplit
.
*
by
destruct
b
,
bexp
.
iApply
"HΦ"
;
last
first
.
*
iApply
(
"HT"
with
"[]"
)
;
first
by
iSplit
.
by
destruct
b
,
bexp
.
*
by
iExists
_
.
Qed
.
Global
Instance
type_cas_atomic_bool_inst
(
l
:
loc
)
β
it
PT
PF
(
lexp
:
loc
)
Pexp
vnew
Pnew
:
TypedCas
(
IntOp
it
)
l
(
l
◁ₗ
{
β
}
(
atomic_bool
it
PT
PF
))%
I
lexp
Pexp
vnew
Pnew
:
=
...
...
theories/typing/bitfield.v
View file @
a8710147
From
refinedc
.
lithium
Require
Import
simpl_classes
.
From
refinedc
.
lang
Require
Export
bitfield
.
From
refinedc
.
typing
Require
Import
programs
int
.
From
refinedc
.
typing
Require
Import
programs
boolean
int
.
From
refinedc
.
typing
Require
Export
type
.
Set
Default
Proof
Using
"Type"
.
...
...
@@ -256,7 +256,7 @@ Section programs.
{
rewrite
(
bool_decide_iff
_
(
bv
=
0
))
//.
rewrite
Hbv
(
bool_decide_iff
_
(
b
=
false
))
;
last
by
apply
bf_cons_bool_singleton_false_iff
.
by
destruct
b
.
}
iExists
_
.
by
iFrame
.
iExists
_
.
iFrame
.
iIntros
"(%n&%&%Heq)"
.
move
:
Heq
=>
/=
?.
subst
n
.
done
.
Qed
.
Global
Instance
type_bitfield_raw_is_false_inst
it
v1
v2
bv
:
TypedBinOpVal
v1
(
0
@
int
it
)%
I
v2
(
bv
@
bitfield_raw
it
)%
I
(
EqOp
i32
)
(
IntOp
it
)
(
IntOp
it
)
:
=
...
...
@@ -275,7 +275,7 @@ Section programs.
{
rewrite
(
bool_decide_iff
_
(
bv
≠
0
))
//.
rewrite
Hbv
(
bool_decide_iff
_
(
b
=
true
))
;
last
by
apply
bf_cons_bool_singleton_true_iff
.
by
destruct
b
.
}
iExists
_
.
by
iFrame
.
iExists
_
.
iFrame
.
iIntros
"(%n&%&%Heq)"
.
move
:
Heq
=>
/=
?.
subst
n
.
done
.
Qed
.
Global
Instance
type_bitfield_raw_is_true_inst
it
v1
v2
bv
:
TypedBinOpVal
v1
(
0
@
int
it
)%
I
v2
(
bv
@
bitfield_raw
it
)%
I
(
NeOp
i32
)
(
IntOp
it
)
(
IntOp
it
)
:
=
...
...
theories/typing/boolean.v
0 → 100644
View file @
a8710147
From
refinedc
.
typing
Require
Export
type
.
From
refinedc
.
typing
Require
Import
programs
.
Set
Default
Proof
Using
"Type"
.
(** A [Strict] boolean can only have value 0 (false) or 1 (true). A [Relaxed]
boolean can have any value: 0 means false, anything else means true. *)
Inductive
strictness
:
=
Strict
|
Relaxed
.
Definition
represents_boolean
(
stn
:
strictness
)
(
n
:
Z
)
(
b
:
bool
)
:
Prop
:
=
match
stn
with
|
Strict
=>
n
=
Z_of_bool
b
|
Relaxed
=>
bool_decide
(
n
≠
0
)
=
b
end
.
Lemma
represents_boolean_eq
(
stn
:
strictness
)
(
n
:
Z
)
(
b
:
bool
)
:
represents_boolean
stn
n
b
→
bool_decide
(
n
≠
0
)
=
b
.
Proof
.
destruct
stn
=>
//=.
move
=>
->.
by
destruct
b
.
Qed
.
Section
generic_boolean
.
Context
`
{!
typeG
Σ
}.
Program
Definition
generic_boolean_inner_type
(
stn
:
strictness
)
(
it
:
int_type
)
(
b
:
bool
)
:
type
:
=
{|
ty_own
β
l
:
=
∃
v
n
,
⌜
val_to_Z
v
it
=
Some
n
⌝
∗
⌜
represents_boolean
stn
n
b
⌝
∗
⌜
l
`
has_layout_loc
`
it
⌝
∗
l
↦
[
β
]
v
;
|}%
I
.
Next
Obligation
.
iIntros
(??????)
"(%v&%n&%&%&%&Hl)"
.
iExists
v
,
n
.
do
3
(
iSplitR
;
first
done
).
by
iApply
heap_mapsto_own_state_share
.
Qed
.
Program
Definition
generic_boolean
(
stn
:
strictness
)
(
it
:
int_type
)
:
rtype
:
=
{|
rty_type
:
=
bool
;
rty
:
=
generic_boolean_inner_type
stn
it
;
|}.
Global
Program
Instance
rmovable_generic_boolean
stn
it
:
RMovable
(
generic_boolean
stn
it
)
:
=
{|
rmovable
b
:
=
{|
ty_has_op_type
ot
mt
:
=
is_int_ot
ot
it
;
ty_own_val
v
:
=
∃
n
,
⌜
val_to_Z
v
it
=
Some
n
⌝
∗
⌜
represents_boolean
stn
n
b
⌝
;
|}
|}%
I
.
Next
Obligation
.
iIntros
(??????
->%
is_int_ot_layout
)
"(%&%&_&_&$&_)"
.
Qed
.
Next
Obligation
.
iIntros
(??????
->%
is_int_ot_layout
[?[
H
_
]])
"!%"
.
by
apply
val_to_Z_length
in
H
.
Qed
.
Next
Obligation
.
iIntros
(???????)
"(%v&%n&%&%&%&?)"
.
eauto
with
iFrame
.
Qed
.
Next
Obligation
.
iIntros
(??????
v
->%
is_int_ot_layout
?)
"Hl (%n&%&%)"
.
iExists
v
,
n
.
eauto
with
iFrame
.
Qed
.
Next
Obligation
.
iIntros
(????????).
apply
:
mem_cast_compat_int
;
[
naive_solver
|].
iPureIntro
;
naive_solver
.
Qed
.
Global
Program
Instance
generic_boolean_copyable
b
stn
it
:
Copyable
(
b
@
generic_boolean
stn
it
).
Next
Obligation
.
iIntros
(???????
->%
is_int_ot_layout
)
"(%v&%n&%&%&%&Hl)"
.
iMod
(
heap_mapsto_own_state_to_mt
with
"Hl"
)
as
(
q
)
"[_ Hl]"
=>
//.
iSplitR
;
first
done
.
iExists
q
,
v
.
iFrame
.
iModIntro
.
eauto
6
with
iFrame
.
Qed
.
Global
Instance
alloc_alive_generic_boolean
b
stn
it
β
:
AllocAlive
(
b
@
generic_boolean
stn
it
)
β
True
.
Proof
.
constructor
.
iIntros
(
l
?)
"(%&%&%&%&%&Hl)"
.
iApply
(
heap_mapsto_own_state_alloc
with
"Hl"
).
erewrite
val_to_Z_length
;
[|
done
].
have
:
=
bytes_per_int_gt_0
it
.
lia
.
Qed
.
Global
Instance
generic_boolean_timeless
l
b
stn
it
:
Timeless
(
l
◁ₗ
b
@
generic_boolean
stn
it
)%
I
.
Proof
.
apply
_
.
Qed
.
End
generic_boolean
.
Notation
"generic_boolean< stn , it >"
:
=
(
generic_boolean
stn
it
)
(
only
printing
,
format
"'generic_boolean<' stn ',' it '>'"
)
:
printing_sugar
.
Notation
boolean
:
=
(
generic_boolean
Strict
)
(
only
parsing
).
Notation
"boolean< it >"
:
=
(
boolean
it
)
(
only
printing
,
format
"'boolean<' it '>'"
)
:
printing_sugar
.
Section
programs
.
Context
`
{!
typeG
Σ
}.
Inductive
destruct_hint_if_bool
:
=
|
DestructHintIfBool
(
b
:
bool
).
Lemma
type_if_generic_boolean
stn
it
(
b
:
bool
)
v
T1
T2
:
destruct_hint
(
DHintDestruct
_
b
)
(
DestructHintIfBool
b
)
(
if
b
then
T1
else
T2
)
-
∗
typed_if
(
IntOp
it
)
v
(
v
◁ᵥ
b
@
generic_boolean
stn
it
)
T1
T2
.
Proof
.
unfold
destruct_hint
.
iIntros
"Hs (%n&%Hv&%Hb)"
.
rewrite
<-(
represents_boolean_eq
stn
n
b
)
;
last
done
.
eauto
with
iFrame
.
Qed
.
Global
Instance
type_if_generic_boolean_inst
stn
it
b
v
:
TypedIf
(
IntOp
it
)
v
(
v
◁ᵥ
b
@
generic_boolean
stn
it
)%
I
:
=
λ
T1
T2
,
i2p
(
type_if_generic_boolean
stn
it
b
v
T1
T2
).
Lemma
type_assert_generic_boolean
stn
it
(
b
:
bool
)
s
Q
fn
ls
R
v
:
(
⌜
b
⌝
∗
typed_stmt
s
fn
ls
R
Q
)
-
∗
typed_assert
(
IntOp
it
)
v
(
v
◁ᵥ
b
@
generic_boolean
stn
it
)
s
fn
ls
R
Q
.
Proof
.
iIntros
"[%H $] (%n&%&%Hb)"
.
destruct
b
;
last
by
exfalso
.
iExists
n
.
iSplit
;
first
done
.
iPureIntro
.
by
apply
represents_boolean_eq
,
bool_decide_eq_true
in
Hb
.
Qed
.
Global
Instance
type_assert_generic_boolean_inst
stn
it
b
v
:
TypedAssert
(
IntOp
it
)
v
(
v
◁ᵥ
b
@
generic_boolean
stn
it
)%
I
:
=
λ
s
fn
ls
R
Q
,
i2p
(
type_assert_generic_boolean
_
_
_
_
_
_
_
_
_
).
End
programs
.
Section
boolean
.
Context
`
{!
typeG
Σ
}.
Lemma
type_relop_boolean
it
v1
b1
v2
b2
T
b
op
:
match
op
with
|
EqOp
rit
=>
Some
(
eqb
b1
b2
,
rit
)
|
NeOp
rit
=>
Some
(
negb
(
eqb
b1
b2
),
rit
)
|
_
=>
None
end
=
Some
(
b
,
i32
)
→
T
(
i2v
(
Z_of_bool
b
)
i32
)
(
t2mt
(
b
@
boolean
i32
))
-
∗
typed_bin_op
v1
(
v1
◁ᵥ
b1
@
boolean
it
)
v2
(
v2
◁ᵥ
b2
@
boolean
it
)
op
(
IntOp
it
)
(
IntOp
it
)
T
.
Proof
.
iIntros
"%Hop HT (%n1&%Hv1&%Hb1) (%n2&%Hv2&%Hb2) %Φ HΦ"
.
have
[
v
Hv
]
:
=
val_of_Z_bool_is_Some
None
i32
b
.
iApply
(
wp_binop_det_pure
(
i2v
(
Z_of_bool
b
)
i32
)).
{
rewrite
/
i2v
Hv
/=.
destruct
op
,
b1
,
b2
;
simplify_eq
.
all
:
split
;
[
inversion
1
;
simplify_eq
/=
;
done
|
move
=>
->]
;
simplify_eq
/=.
all
:
econstructor
=>
//
;
by
case_bool_decide
.
}
iApply
"HΦ"
;
last
done
.
iExists
(
Z_of_bool
b
).
iSplit
;
[
by
destruct
b
|
done
].
Qed
.
Global
Program
Instance
type_eq_boolean_inst
it
v1
b1
v2
b2
:
TypedBinOpVal
v1
(
b1
@
(
boolean
it
))%
I
v2
(
b2
@
(
boolean
it
))%
I
(
EqOp
i32
)
(
IntOp
it
)
(
IntOp
it
)
:
=
λ
T
,
i2p
(
type_relop_boolean
it
v1
b1
v2
b2
T
(
eqb
b1
b2
)
_
_
).
Next
Obligation
.
done
.
Qed
.
Global
Program
Instance
type_ne_boolean_inst
it
v1
b1
v2
b2
:
TypedBinOpVal
v1
(
b1
@
(
boolean
it
))%
I
v2
(
b2
@
(
boolean
it
))%
I
(
NeOp
i32
)
(
IntOp
it
)
(
IntOp
it
)
:
=
λ
T
,
i2p
(
type_relop_boolean
it
v1
b1
v2
b2
T
(
negb
(
eqb
b1
b2
))
_
_
).
Next
Obligation
.
done
.
Qed
.
(* TODO: replace this with a typed_cas once it is refactored to take E as an argument. *)
Lemma
wp_cas_suc_boolean
it
b1
b2
bd
l1
l2
vd
Φ
E
:
(
bytes_per_int
it
≤
bytes_per_addr
)%
nat
→
b1
=
b2
→
l1
◁ₗ
b1
@
boolean
it
-
∗
l2
◁ₗ
b2
@
boolean
it
-
∗
vd
◁ᵥ
bd
@
boolean
it
-
∗
▷
(
l1
◁ₗ
bd
@
boolean
it
-
∗
l2
◁ₗ
b2
@
boolean
it
-
∗
Φ
(
val_of_bool
true
))
-
∗
wp
NotStuck
E
(
CAS
(
IntOp
it
)
(
Val
l1
)
(
Val
l2
)
(
Val
vd
))
Φ
.
Proof
.
iIntros
(?
->)
"(%v1&%n1&%&%&%&Hl1) (%v2&%n2&%&%&%&Hl2) (%n&%&%) HΦ/="
.
iApply
(
wp_cas_suc
with
"Hl1 Hl2"
)
=>
//.
{
by
apply
val_to_of_loc
.
}
{
by
apply
val_to_of_loc
.
}
{
by
eapply
val_to_Z_length
.
}
{
simpl
in
*.
by
simplify_eq
.
}
iIntros
"!# Hl1 Hl2"
.
iApply
(
"HΦ"
with
"[Hl1] [Hl2]"
)
;
iExists
_
,
_;
by
iFrame
.
Qed
.
Lemma
wp_cas_fail_boolean
it
b1
b2
bd
l1
l2
vd
Φ
E
:
(
bytes_per_int
it
≤
bytes_per_addr
)%
nat
→
b1
≠
b2
→
l1
◁ₗ
b1
@
boolean
it
-
∗
l2
◁ₗ
b2
@
boolean
it
-
∗
vd
◁ᵥ
bd
@
boolean
it
-
∗
▷
(
l1
◁ₗ
b1
@
boolean
it
-
∗
l2
◁ₗ
b1
@
boolean
it
-
∗
Φ
(
val_of_bool
false
))
-
∗
wp
NotStuck
E
(
CAS
(
IntOp
it
)
(
Val
l1
)
(
Val
l2
)
(
Val
vd
))
Φ
.
Proof
.
iIntros
(??)
"(%v1&%n1&%&%&%&Hl1) (%v2&%n2&%&%&%&Hl2) (%n&%&%) HΦ/="
.
iApply
(
wp_cas_fail
with
"Hl1 Hl2"
)
=>
//.
{
by
apply
val_to_of_loc
.
}
{
by
apply
val_to_of_loc
.
}
{
by
eapply
val_to_Z_length
.
}
{
simpl
in
*.
simplify_eq
.
by
destruct
b1
,
b2
.
}
iIntros
"!# Hl1 Hl2"
.
iApply
(
"HΦ"
with
"[Hl1] [Hl2]"
)
;
iExists
_
,
_;
by
iFrame
.
Qed
.
Lemma
type_val_boolean
b
T
:
(
T
(
t2mt
(
b
@
boolean
bool_it
)))
-
∗
typed_value
(
val_of_bool
b
)
T
.
Proof
.
iIntros
"HT"
.
iExists
_
.
iFrame
.
iExists
(
Z_of_bool
b
).
destruct
b
;
eauto
.
Qed
.
Global
Instance
type_val_boolean_inst
b
:
TypedValue
(
val_of_bool
b
)
:
=
λ
T
,
i2p
(
type_val_boolean
b
T
).
Lemma
type_cast_boolean
b
it1
it2
v
T
:
(
∀
v
,
T
v
(
t2mt
(
b
@
boolean
it2
)))
-
∗
typed_un_op
v
(
v
◁ᵥ
b
@
boolean
it1
)%
I
(
CastOp
(
IntOp
it2
))
(
IntOp
it1
)
T
.
Proof
.
iIntros
"HT (%n&%Hv&%Hb) %Φ HΦ"
.
move
:
Hb
=>
/=
?.
subst
n
.
have
[??]
:
=
val_of_Z_bool_is_Some
(
val_to_byte_prov
v
)
it2
b
.
iApply
wp_cast_int
=>
//.
iApply
(
"HΦ"
with
"[] HT"
)
=>
//.
iExists
_
.
iSplit
;
last
done
.
iPureIntro
.
by
eapply
val_to_of_Z
.
Qed
.
Global
Instance
type_cast_bool_inst
b
it1
it2
v
:
TypedUnOpVal
v
(
b
@
boolean
it1
)%
I
(
CastOp
(
IntOp
it2
))
(
IntOp
it1
)
:
=
λ
T
,
i2p
(
type_cast_boolean
b
it1
it2
v
T
).
End
boolean
.
Typeclasses
Opaque
generic_boolean_inner_type
.
Notation
"'if' p "
:
=
(
DestructHintIfBool
p
)
(
at
level
100
,
only
printing
).
theories/typing/int.v
View file @
a8710147
From
refinedc
.
typing
Require
Export
type
.
From
refinedc
.
typing
Require
Import
programs
.
From
refinedc
.
typing
Require
Import
programs
boolean
.
Set
Default
Proof
Using
"Type"
.
Section
int
.
...
...
@@ -81,40 +81,6 @@ End int.
(* Typeclasses Opaque int. *)
Notation
"int< it >"
:
=
(
int
it
)
(
only
printing
,
format
"'int<' it '>'"
)
:
printing_sugar
.
(* TODO: move this to an extra file? *)
Section
boolean
.
Context
`
{!
typeG
Σ
}.
(* Separate definition such that we can make it typeclasses opaque later. *)
Program
Definition
boolean_inner_type
(
it
:
int_type
)
(
b
:
bool
)
:
type
:
=
(
Z_of_bool
b
)
@
int
it
.
Program
Definition
boolean
(
it
:
int_type
)
:
rtype
:
=
{|
rty_type
:
=
bool
;
rty
:
=
boolean_inner_type
it
;
|}.
Global
Program
Instance
rmovable_boolean
it
:
RMovable
(
boolean
it
)
:
=
{|
rmovable
b
:
=
(
rmovable
(
int
it
))
(
Z_of_bool
b
)
;
|}.
Global
Program
Instance
boolean_copyable
x
it
:
Copyable
(
x
@
boolean
it
).
Next
Obligation
.
rewrite
/
with_refinement
/=/
boolean_inner_type
=>
???????.
by
apply
:
copy_shr_acc
.
Qed
.
Lemma
boolean_own_val_eq
v
b
it
:
(
v
◁ᵥ
b
@
boolean
it
)%
I
≡
⌜
val_to_Z
v
it
=
Some
(
Z_of_bool
b
)
⌝
%
I
.
Proof
.
done
.
Qed
.
Global
Instance
alloc_alive_bool
b
it
β
:
AllocAlive
(
b
@
boolean
it
)
β
True
.
Proof
.
apply
_
.
Qed
.
Global
Instance
boolean_timeless
l
b
it
:
Timeless
(
l
◁ₗ
b
@
boolean
it
)%
I
.
Proof
.
apply
_
.
Qed
.
End
boolean
.
Notation
"boolean< it >"
:
=
(
boolean
it
)
(
only
printing
,
format
"'boolean<' it '>'"
)
:
printing_sugar
.
Section
programs
.
Context
`
{!
typeG
Σ
}.
...
...
@@ -152,10 +118,10 @@ Section programs.
1
-
2
:
iPureIntro
;
by
apply
:
val_to_Z_in_range
.
have
[
v
Hv
]
:
=
val_of_Z_bool_is_Some
None
i32
b
.
iApply
(
wp_binop_det_pure
(
i2v
(
Z_of_bool
b
)
i32
)).
{
rewrite
/
i2v
Hv
/=.
split
;
last
(
move
=>
->
;
by
econstructor
).
{
rewrite
/
i2v
Hv
/=.
split
;
last
(
move
=>
->
;
by
econstructor
).
destruct
op
=>
//
;
inversion
1
;
by
simplify_eq
.
}
iIntros
"!>"
.
iApply
"HΦ"
=>
//.
by
destruct
b
.
iIntros
"!>"
.
iApply
"HΦ"
=>
//.
iExists
(
Z_of_bool
b
).
destruct
b
;
eauto
.
Qed
.
Global
Program
Instance
type_eq_int_int_inst
it
v1
n1
v2
n2
:
...
...
@@ -461,137 +427,52 @@ Section programs.
iIntros
"!# Hl1 Hl2"
.
iApply
(
"HΦ"
with
"[Hl1] [Hl2]"
)
;
iExists
_;
by
iFrame
.
Qed
.
(*** bool *)
Lemma
type_val_bool'
b
:
⊢
(
val_of_bool
b
)
◁ᵥ
(
b
@
boolean
bool_it
).
Proof
.
iIntros
.
by
destruct
b
.
Qed
.
Lemma
type_val_bool
b
T
:
(
T
(
t2mt
(
b
@
boolean
bool_it
)))
-
∗
typed_value
(
val_of_bool
b
)
T
.
Proof
.
iIntros
"HT"
.
iExists
_
.
iFrame
.
iApply
type_val_bool'
.
Qed
.
Global
Instance
type_val_bool_inst
b
:
TypedValue
(
val_of_bool
b
)
:
=
λ
T
,
i2p
(
type_val_bool
b
T
).
Inductive
destruct_hint_if_bool
:
=
|
DestructHintIfBool
(
b
:
bool
).
Lemma
type_relop_bool_bool
it
v1
b1
v2
b2
T
b
op
:
match
op
with
|
EqOp
rit
=>
Some
(
eqb
b1
b2
,
rit
)
|
NeOp
rit
=>
Some
(
negb
(
eqb
b1
b2
),
rit
)
|
_
=>
None
end
=
Some
(
b
,
i32
)
→
(
T
(
i2v
(
Z_of_bool
b
)
i32
)
(
t2mt
(
b
@
boolean
i32
)))
-
∗
typed_bin_op
v1
(
v1
◁ᵥ
b1
@
boolean
it
)
v2
(
v2
◁ᵥ
b2
@
boolean
it
)
op
(
IntOp
it
)
(
IntOp
it
)
T
.
Proof
.
iIntros
"%Hop HT %Hv1 %Hv2 %Φ HΦ"
.
have
[
v
Hv
]
:
=
val_of_Z_bool_is_Some
None
i32
b
.
iApply
(
wp_binop_det_pure
(
i2v
(
Z_of_bool
b
)
i32
)).
{
rewrite
/
i2v
Hv
/=.
destruct
op
,
b1
,
b2
;
simplify_eq
.
all
:
split
;
[
inversion
1
;
simplify_eq
/=
;
done
|
move
=>
->
]
;
simplify_eq
/=.
all
:
econstructor
=>
//
;
by
case_bool_decide
.
}
iApply
"HΦ"
;
last
done
.
iPureIntro
.
by
destruct
b
.
Qed
.
Global
Program
Instance
type_eq_bool_bool_inst
it
v1
b1
v2
b2
:
TypedBinOpVal
v1
(
b1
@
(
boolean
it
))%
I
v2
(
b2
@
(
boolean
it
))%
I
(
EqOp
i32
)
(
IntOp
it
)
(
IntOp
it
)
:
=
λ
T
,
i2p
(
type_relop_bool_bool
it
v1
b1
v2
b2
T
(
eqb
b1
b2
)
_
_
).
Next
Obligation
.
done
.
Qed
.
Global
Program
Instance
type_ne_bool_bool_inst
it
v1
b1
v2
b2
:
TypedBinOpVal
v1
(
b1
@
(
boolean
it
))%
I
v2
(
b2
@
(
boolean
it
))%
I
(
NeOp
i32
)
(
IntOp
it
)
(
IntOp
it
)
:
=
λ
T
,
i2p
(
type_relop_bool_bool
it
v1
b1
v2
b2
T
(
negb
(
eqb
b1
b2
))
_
_
).
Next
Obligation
.
done
.
Qed
.
Lemma
type_if_bool
it
(
b
:
bool
)
v
T1
T2
:
destruct_hint
(
DHintDestruct
_
b
)
(
DestructHintIfBool
b
)
(
if
b
then
T1
else
T2
)
-
∗
typed_if
(
IntOp
it
)
v
(
v
◁ᵥ
b
@
boolean
it
)
T1
T2
.
Proof
.
unfold
destruct_hint
.
iIntros
"Hs %Hb"
.
iExists
_
.
iSplit
;
first
done
.
by
destruct
b
.
Qed
.
Global
Instance
type_if_bool_inst
it
b
v
:
TypedIf
(
IntOp
it
)
v
(
v
◁ᵥ
b
@
boolean
it
)%
I
:
=
λ
T1
T2
,
i2p
(
type_if_bool
it
b
v
T1
T2
).
Lemma
type_assert_bool
it
(
b
:
bool
)
s
Q
fn
ls
R
v
:
(
⌜
b
⌝
∗
typed_stmt
s
fn
ls
R
Q
)
-
∗
typed_assert
(
IntOp
it
)
v
(
v
◁ᵥ
b
@
boolean
it
)
s
fn
ls
R
Q
.
Proof
.
iIntros
"[% Hs] %Hb"
.
iExists
_
.
iFrame
"Hs"
.
iSplit
;
first
done
.
by
destruct
b
.
Qed
.
Global
Instance
type_assert_bool_inst
it
b
v
:
TypedAssert
(
IntOp
it
)
v
(
v
◁ᵥ
b
@
boolean
it
)%
I
:
=
λ
s
fn
ls
R
Q
,
i2p
(
type_assert_bool
_
_
_
_
_
_
_
_
).
Lemma
type_cast_bool
b
it1
it2
v
T
: