3 stable releases
1.0.2 | Apr 12, 2023 |
---|---|
1.0.0 | Apr 11, 2023 |
#25 in #formal-verification
31 downloads per month
6KB
Formal Verification of the Solana Programs
Formal verification is the process of using a formal specification to verify the correctness of a system.
Invariants
Invariants are properties that should always be true. For example, the balance of a token account should never be negative. There are two types of invariants in the Solana programs: account invariants
and instruction invariants
.
Instruction Invariants
An instruction invariant specifies sufficient conditions for an instruction to succeed (or fail). These are specified as succeeds_if
or errors_if
macro annotations on the instruction handler.
succeeds_if
- The instruction should succeed if and only if the given condition is true.
#[succeeds_if(
ctx.user.balance > amount
)]
pub fn withdraw(ctx: Context<Withdraw>, amount: u64) {
// ...
}
errors_if
- The instruction should fail if and only if the given condition is true.
#[errors_if(
ctx.user.balance < amount
)]
pub fn withdraw(ctx: Context<Withdraw>, amount: u64) {
// ...
}
Account Invariants
The other type of invariant is an Account Invariant. This invariant describes some property of an account that should always hold. We use the invariant
macro to specify these invariants.
invariant
- The account invariant should hold if and only if the given condition is true.
#[account]
#[invariant(
self.balance >= 0
)]
struct User {
pub balance: i64,
}
Dependencies
~82KB