Properties
The property!
operation is not actually a transition. Instead, it allows you to export
useful facts from the state-machine view of the world to thread-local reasoning in your
implementation.
For example, suppose your state machine has:
fields {
#[sharding(bool)]
pub waiting: bool,
#[sharding(variable)]
pub num_remaining: nat,
...
}
where num_remaining
corresponds to an atomic U32 counting the number of
threads that still need to perform an operation. You could represent this by
maintaining a state-machine level invariant that self.waiting ==> self.num_remaining > 0
. However, that fact is not available in your code by
default. Hence, if your code needs to prove, say, that when it decreases the
atomic U32, the value does not wrap around, you can establish this via a
property:
property! {
waiting_means_positive() {
assert(self.waiting ==> self.num_remaining > 0);
}
}
Verus will check that the invariant establishes this property, and then it will make
waiting_means_positive
available to the code as a lemma that can be invoked on the
state-machine’s Instance
.
You can also use a property!
to establish a proof-by-contradiction. Continuing the example
above, suppose you also maintain an invariant that num_remaining < 10
. In your implementation,
perhaps your code contains a function that receives a token tok
representing
num_remaining
but doesn’t know how large the contained value might be. To prove that the value
isn’t too large, you can use a property like this:
property! {
in_bounds() {
have num_remaining >= (10);
assert(false);
}
}
Again, Verus will check that the invariant establishes this property, and then
it will make in_bounds
available to the code as a lemma that can be invoked
on the state-machine’s Instance
. Invoking that lemma with a shared reference
to tok
will allow the code to conclude that the value in tok
must be less
than 10.
Finally, when working with storage strategies (e.g.,
storage_option or
storage_map), to obtain a shared permission to the
stored value, you can use the guard
operation inside a property. For
instance, if your state machine has:
fields {
#[sharding(bool)]
pub deposited: bool,
#[sharding(storage_option)]
pub perm: Option<Perm>,
...
}
then you can write a property like this:
property! {
get_perm_ref(x: Perm) {
have deposited >= (true);
guard perm >= (Some(x));
}
}
Verus will check that your invariant implies that perm
is Some
(e.g.,
perhaps your invariant says self.deposited ==> self.perm.is_some()
).
VerusSync will make get_perm_ref
available to the code as a lemma that can be
invoked on the state-machine’s Instance
. Invoking that lemma with a shared
reference to a token for deposited
and the ghost value of perm
will
produce a shared reference to the value in perm
.