Solana 程序的正式验证

正式验证是使用正式规范验证系统正确性的过程。

不变性

不变性是始终应该为真的属性。例如，代币账户的余额不应为负。Solana 程序中有两种类型的不变性：账户不变性 和 指令不变性。

指令不变性

指令不变性指定了指令成功（或失败）的充分条件。这些条件作为指令处理器的 succeeds_if 或 errors_if 宏注释来指定。

• succeeds_if - 如果给定条件为真，则指令应该成功。

#[succeeds_if(
    ctx.user.balance > amount
)]
pub fn withdraw(ctx: Context<Withdraw>, amount: u64) {
    // ...
}

• errors_if - 如果给定条件为真，则指令应该失败。

#[errors_if(
    ctx.user.balance < amount
)]
pub fn withdraw(ctx: Context<Withdraw>, amount: u64) {
    // ...
}

账户不变性

另一种类型的不变性是账户不变性。这种不变性描述了账户的一些始终存在的属性。我们使用 invariant 宏来指定这些不变性。

• invariant - 如果给定条件为真，则账户不变性应该成立。

#[account]
#[invariant(
    self.balance >= 0
)]
struct User {
    pub balance: i64,
}