From 5de7967868f99ded1c801af01c7dc75b45f6deb5 Mon Sep 17 00:00:00 2001 From: KAMIYO Date: Tue, 17 Feb 2026 03:22:20 +0100 Subject: [PATCH 1/2] feat: add solana AccountInfo generators for proofs --- library/kani_solana_agent/Cargo.toml | 14 ++ library/kani_solana_agent/README.md | 28 +++ library/kani_solana_agent/src/account.rs | 167 ++++++++++++++++++ library/kani_solana_agent/src/lib.rs | 8 + .../cargo-kani/solana-accountinfo/Cargo.toml | 13 ++ .../release_funds_conserves_lamports.expected | 1 + .../cargo-kani/solana-accountinfo/src/lib.rs | 110 ++++++++++++ ...elock_policy_matches_release_rule.expected | 1 + 8 files changed, 342 insertions(+) create mode 100644 library/kani_solana_agent/Cargo.toml create mode 100644 library/kani_solana_agent/README.md create mode 100644 library/kani_solana_agent/src/account.rs create mode 100644 library/kani_solana_agent/src/lib.rs create mode 100644 tests/cargo-kani/solana-accountinfo/Cargo.toml create mode 100644 tests/cargo-kani/solana-accountinfo/release_funds_conserves_lamports.expected create mode 100644 tests/cargo-kani/solana-accountinfo/src/lib.rs create mode 100644 tests/cargo-kani/solana-accountinfo/timelock_policy_matches_release_rule.expected diff --git a/library/kani_solana_agent/Cargo.toml b/library/kani_solana_agent/Cargo.toml new file mode 100644 index 000000000000..cdb6f16026c7 --- /dev/null +++ b/library/kani_solana_agent/Cargo.toml @@ -0,0 +1,14 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +[package] +name = "kani-solana-agent" +version = "0.1.0" +edition = "2021" +license = "MIT OR Apache-2.0" +publish = false + +[dependencies] +solana-program = "=3.0.0" + +[workspace] diff --git a/library/kani_solana_agent/README.md b/library/kani_solana_agent/README.md new file mode 100644 index 000000000000..80b65cc5f01c --- /dev/null +++ b/library/kani_solana_agent/README.md @@ -0,0 +1,28 @@ +# Solana AccountInfo Utilities for Kani Proofs + +This crate provides small helpers to reduce the boilerplate involved in writing Kani proof harnesses for code that uses Solana's `AccountInfo` API. + +Non-goals: +- Modeling Solana syscalls / runtime behavior +- Anchor-specific modeling +- Token program semantics + +The primary entry point is `any_account_info::(...)`, which constructs an `AccountInfo<'static>` backed by leaked allocations so it can be passed into program logic during verification. + +## Example + +```rust +#[cfg(kani)] +mod proofs { + use kani_solana_agent::{AccountConfig, any_account_info}; + + #[kani::proof] + fn can_build_accounts() { + let payer = any_account_info::<0>(AccountConfig::new().payer()); + let escrow = any_account_info::<128>(AccountConfig::new().writable()); + + kani::assert(payer.is_signer, "payer must be a signer"); + kani::assert(escrow.is_writable, "escrow must be writable"); + } +} +``` diff --git a/library/kani_solana_agent/src/account.rs b/library/kani_solana_agent/src/account.rs new file mode 100644 index 000000000000..e28a80287dd3 --- /dev/null +++ b/library/kani_solana_agent/src/account.rs @@ -0,0 +1,167 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +use solana_program::account_info::AccountInfo; +use solana_program::pubkey::Pubkey; +use solana_program::rent::Rent; +use std::cell::RefCell; +use std::ops::RangeInclusive; +use std::rc::Rc; + +#[derive(Clone, Debug)] +enum Lamports { + Any, + Exact(u64), + Range(RangeInclusive), +} + +#[derive(Clone, Debug)] +pub struct AccountConfig { + key: Option, + owner: Option, + lamports: Lamports, + rent_exempt: bool, + + pub is_signer: bool, + pub is_writable: bool, + pub executable: bool, + pub rent_epoch: u64, +} + +impl Default for AccountConfig { + fn default() -> Self { + Self { + key: None, + owner: None, + lamports: Lamports::Any, + rent_exempt: true, + is_signer: false, + is_writable: false, + executable: false, + rent_epoch: 0, + } + } +} + +impl AccountConfig { + pub fn new() -> Self { + Self::default() + } + + pub fn key(mut self, key: Pubkey) -> Self { + self.key = Some(key); + self + } + + pub fn owner(mut self, owner: Pubkey) -> Self { + self.owner = Some(owner); + self + } + + pub fn signer(mut self) -> Self { + self.is_signer = true; + self + } + + pub fn writable(mut self) -> Self { + self.is_writable = true; + self + } + + pub fn payer(mut self) -> Self { + self.is_signer = true; + self.is_writable = true; + self + } + + pub fn executable(mut self) -> Self { + self.executable = true; + self + } + + pub fn lamports(mut self, lamports: u64) -> Self { + self.lamports = Lamports::Exact(lamports); + self + } + + pub fn lamports_range(mut self, range: RangeInclusive) -> Self { + self.lamports = Lamports::Range(range); + self + } + + pub fn rent_exempt(mut self, enabled: bool) -> Self { + self.rent_exempt = enabled; + self + } + + pub fn rent_epoch(mut self, epoch: u64) -> Self { + self.rent_epoch = epoch; + self + } +} + +#[cfg(kani)] +fn any_pubkey() -> Pubkey { + Pubkey::new_from_array(kani::any()) +} + +#[cfg(not(kani))] +fn any_pubkey() -> Pubkey { + Pubkey::default() +} + +#[cfg(kani)] +fn pick_lamports(cfg: &AccountConfig) -> u64 { + let lamports = match &cfg.lamports { + Lamports::Any => kani::any(), + Lamports::Exact(v) => *v, + Lamports::Range(r) => { + let v: u64 = kani::any(); + kani::assume(r.contains(&v)); + v + } + }; + + if cfg.rent_exempt { + kani::assume(Rent::default().is_exempt(lamports, DATA_LEN)); + } + + lamports +} + +#[cfg(not(kani))] +fn pick_lamports(_cfg: &AccountConfig) -> u64 { + let _ = DATA_LEN; + 0 +} + +#[cfg(kani)] +pub fn any_account_info(cfg: AccountConfig) -> AccountInfo<'static> { + let key = cfg.key.unwrap_or_else(any_pubkey); + let owner = cfg.owner.unwrap_or_else(any_pubkey); + let lamports = pick_lamports::(&cfg); + + let key: &'static Pubkey = Box::leak(Box::new(key)); + let owner: &'static Pubkey = Box::leak(Box::new(owner)); + + let lamports: &'static mut u64 = Box::leak(Box::new(lamports)); + let data: &'static mut [u8; DATA_LEN] = Box::leak(Box::new(kani::any())); + let data: &'static mut [u8] = data; + + AccountInfo { + key, + is_signer: cfg.is_signer, + is_writable: cfg.is_writable, + lamports: Rc::new(RefCell::new(lamports)), + data: Rc::new(RefCell::new(data)), + owner, + executable: cfg.executable, + rent_epoch: cfg.rent_epoch, + } +} + +#[cfg(not(kani))] +pub fn any_account_info(_cfg: AccountConfig) -> AccountInfo<'static> { + let _ = DATA_LEN; + panic!("any_account_info is only available under `cargo kani` (cfg(kani))"); +} diff --git a/library/kani_solana_agent/src/lib.rs b/library/kani_solana_agent/src/lib.rs new file mode 100644 index 000000000000..a6122cdb6943 --- /dev/null +++ b/library/kani_solana_agent/src/lib.rs @@ -0,0 +1,8 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +pub mod account; + +pub use account::{AccountConfig, any_account_info}; +pub use solana_program::account_info::AccountInfo; +pub use solana_program::pubkey::Pubkey; diff --git a/tests/cargo-kani/solana-accountinfo/Cargo.toml b/tests/cargo-kani/solana-accountinfo/Cargo.toml new file mode 100644 index 000000000000..1439b2a47146 --- /dev/null +++ b/tests/cargo-kani/solana-accountinfo/Cargo.toml @@ -0,0 +1,13 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +[package] +name = "solana-accountinfo" +version = "0.1.0" +edition = "2018" + +[dependencies] +kani-solana-agent = { path = "../../../library/kani_solana_agent" } +solana-program = "=3.0.0" + +[workspace] diff --git a/tests/cargo-kani/solana-accountinfo/release_funds_conserves_lamports.expected b/tests/cargo-kani/solana-accountinfo/release_funds_conserves_lamports.expected new file mode 100644 index 000000000000..34c886c358cb --- /dev/null +++ b/tests/cargo-kani/solana-accountinfo/release_funds_conserves_lamports.expected @@ -0,0 +1 @@ +VERIFICATION:- SUCCESSFUL diff --git a/tests/cargo-kani/solana-accountinfo/src/lib.rs b/tests/cargo-kani/solana-accountinfo/src/lib.rs new file mode 100644 index 000000000000..1cdcfa3682eb --- /dev/null +++ b/tests/cargo-kani/solana-accountinfo/src/lib.rs @@ -0,0 +1,110 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +use kani_solana_agent::{AccountConfig, AccountInfo, any_account_info}; + +fn authorized(now: i64, expires_at: i64, agent: &AccountInfo<'_>, api: &AccountInfo<'_>) -> bool { + agent.is_signer || (api.is_signer && now >= expires_at) +} + +fn lamports(account: &AccountInfo<'_>) -> u64 { + **account.lamports.borrow() +} + +fn transfer(from: &AccountInfo<'_>, to: &AccountInfo<'_>, amount: u64) -> Result<(), ()> { + let mut from_lamports = from.lamports.borrow_mut(); + let Some(new_from) = (**from_lamports).checked_sub(amount) else { + return Err(()); + }; + **from_lamports = new_from; + drop(from_lamports); + + let mut to_lamports = to.lamports.borrow_mut(); + let Some(new_to) = (**to_lamports).checked_add(amount) else { + return Err(()); + }; + **to_lamports = new_to; + Ok(()) +} + +fn release_funds( + now: i64, + expires_at: i64, + agent: &AccountInfo<'_>, + api: &AccountInfo<'_>, + escrow: &AccountInfo<'_>, + payee: &AccountInfo<'_>, + amount: u64, +) -> Result<(), ()> { + if !authorized(now, expires_at, agent, api) { + return Err(()); + } + + transfer(escrow, payee, amount) +} + +#[cfg(kani)] +mod proofs { + use super::*; + + #[kani::proof] + fn timelock_policy_matches_release_rule() { + let now: i64 = kani::any(); + let expires_at: i64 = kani::any(); + + let mut agent = any_account_info::<0>(AccountConfig::new()); + let mut api = any_account_info::<0>(AccountConfig::new()); + agent.is_signer = kani::any(); + api.is_signer = kani::any(); + + let allowed = authorized(now, expires_at, &agent, &api); + + if now < expires_at { + kani::assert(allowed == agent.is_signer, "before expiry only agent can release"); + } else { + kani::assert( + allowed == (agent.is_signer || api.is_signer), + "after expiry agent or api can release", + ); + } + } + + #[kani::proof] + fn release_funds_conserves_lamports() { + let now: i64 = kani::any(); + let expires_at: i64 = kani::any(); + let amount: u64 = kani::any::() as u64; + + let mut agent = any_account_info::<0>(AccountConfig::new()); + let mut api = any_account_info::<0>(AccountConfig::new()); + agent.is_signer = kani::any(); + api.is_signer = kani::any(); + + let escrow = any_account_info::<0>( + AccountConfig::new().writable().lamports_range(0..=(u32::MAX as u64)), + ); + let payee = any_account_info::<0>( + AccountConfig::new().writable().lamports_range(0..=(u32::MAX as u64)), + ); + + let escrow_before = lamports(&escrow); + let payee_before = lamports(&payee); + kani::assume(escrow_before >= amount); + + let total_before = escrow_before as u128 + payee_before as u128; + + let res = release_funds(now, expires_at, &agent, &api, &escrow, &payee, amount); + let escrow_after = lamports(&escrow); + let payee_after = lamports(&payee); + + if res.is_ok() { + let total_after = escrow_after as u128 + payee_after as u128; + kani::assert(total_after == total_before, "release must conserve lamports"); + kani::assert(escrow_after + amount == escrow_before, "escrow must decrease by amount"); + kani::assert(payee_before + amount == payee_after, "payee must increase by amount"); + } else { + kani::assert(escrow_after == escrow_before, "failed release must not mutate"); + kani::assert(payee_after == payee_before, "failed release must not mutate"); + } + } +} diff --git a/tests/cargo-kani/solana-accountinfo/timelock_policy_matches_release_rule.expected b/tests/cargo-kani/solana-accountinfo/timelock_policy_matches_release_rule.expected new file mode 100644 index 000000000000..34c886c358cb --- /dev/null +++ b/tests/cargo-kani/solana-accountinfo/timelock_policy_matches_release_rule.expected @@ -0,0 +1 @@ +VERIFICATION:- SUCCESSFUL From aabb1d9ba26ed9f4ba6a2109af744fbc34dfa6db Mon Sep 17 00:00:00 2001 From: KAMIYO Date: Tue, 17 Feb 2026 10:27:11 +0100 Subject: [PATCH 2/2] feat: add lamport snapshot helpers --- library/kani_solana_agent/.gitignore | 1 + library/kani_solana_agent/Cargo.toml | 3 ++ library/kani_solana_agent/README.md | 11 ++++--- library/kani_solana_agent/src/account.rs | 32 +++++++++++-------- library/kani_solana_agent/src/invariants.rs | 31 ++++++++++++++++++ library/kani_solana_agent/src/lib.rs | 4 ++- .../cargo-kani/solana-accountinfo/Cargo.toml | 3 ++ .../cargo-kani/solana-accountinfo/src/lib.rs | 28 ++++++++-------- 8 files changed, 81 insertions(+), 32 deletions(-) create mode 100644 library/kani_solana_agent/.gitignore create mode 100644 library/kani_solana_agent/src/invariants.rs diff --git a/library/kani_solana_agent/.gitignore b/library/kani_solana_agent/.gitignore new file mode 100644 index 000000000000..2f7896d1d136 --- /dev/null +++ b/library/kani_solana_agent/.gitignore @@ -0,0 +1 @@ +target/ diff --git a/library/kani_solana_agent/Cargo.toml b/library/kani_solana_agent/Cargo.toml index cdb6f16026c7..4244703f8b37 100644 --- a/library/kani_solana_agent/Cargo.toml +++ b/library/kani_solana_agent/Cargo.toml @@ -11,4 +11,7 @@ publish = false [dependencies] solana-program = "=3.0.0" +[lints.rust] +unexpected_cfgs = { level = "warn", check-cfg = ["cfg(kani)"] } + [workspace] diff --git a/library/kani_solana_agent/README.md b/library/kani_solana_agent/README.md index 80b65cc5f01c..3df5990c841e 100644 --- a/library/kani_solana_agent/README.md +++ b/library/kani_solana_agent/README.md @@ -7,22 +7,25 @@ Non-goals: - Anchor-specific modeling - Token program semantics -The primary entry point is `any_account_info::(...)`, which constructs an `AccountInfo<'static>` backed by leaked allocations so it can be passed into program logic during verification. +The primary entry point is `any_account_info::(...)` (alias: `any_agent_account::(...)`), which constructs an `AccountInfo<'static>` backed by leaked allocations so it can be passed into program logic during verification. ## Example ```rust #[cfg(kani)] mod proofs { - use kani_solana_agent::{AccountConfig, any_account_info}; + use kani_solana_agent::{AccountConfig, LamportSnapshot, any_agent_account}; #[kani::proof] fn can_build_accounts() { - let payer = any_account_info::<0>(AccountConfig::new().payer()); - let escrow = any_account_info::<128>(AccountConfig::new().writable()); + let payer = any_agent_account::<0>(AccountConfig::new().payer()); + let escrow = any_agent_account::<128>(AccountConfig::new().writable()); kani::assert(payer.is_signer, "payer must be a signer"); kani::assert(escrow.is_writable, "escrow must be writable"); + + let before = LamportSnapshot::new(&[&payer, &escrow]); + before.assert_unchanged(&[&payer, &escrow], "snapshot must be stable without mutation"); } } ``` diff --git a/library/kani_solana_agent/src/account.rs b/library/kani_solana_agent/src/account.rs index e28a80287dd3..de2b494d5203 100644 --- a/library/kani_solana_agent/src/account.rs +++ b/library/kani_solana_agent/src/account.rs @@ -3,9 +3,13 @@ use solana_program::account_info::AccountInfo; use solana_program::pubkey::Pubkey; +use std::ops::RangeInclusive; + +#[cfg(kani)] use solana_program::rent::Rent; +#[cfg(kani)] use std::cell::RefCell; -use std::ops::RangeInclusive; +#[cfg(kani)] use std::rc::Rc; #[derive(Clone, Debug)] @@ -100,14 +104,13 @@ impl AccountConfig { } } -#[cfg(kani)] -fn any_pubkey() -> Pubkey { - Pubkey::new_from_array(kani::any()) +pub fn any_agent_account(cfg: AccountConfig) -> AccountInfo<'static> { + any_account_info::(cfg) } -#[cfg(not(kani))] +#[cfg(kani)] fn any_pubkey() -> Pubkey { - Pubkey::default() + Pubkey::new_from_array(kani::any()) } #[cfg(kani)] @@ -129,12 +132,6 @@ fn pick_lamports(cfg: &AccountConfig) -> u64 { lamports } -#[cfg(not(kani))] -fn pick_lamports(_cfg: &AccountConfig) -> u64 { - let _ = DATA_LEN; - 0 -} - #[cfg(kani)] pub fn any_account_info(cfg: AccountConfig) -> AccountInfo<'static> { let key = cfg.key.unwrap_or_else(any_pubkey); @@ -161,7 +158,16 @@ pub fn any_account_info(cfg: AccountConfig) -> AccountInf } #[cfg(not(kani))] -pub fn any_account_info(_cfg: AccountConfig) -> AccountInfo<'static> { +pub fn any_account_info(cfg: AccountConfig) -> AccountInfo<'static> { let _ = DATA_LEN; + match cfg.lamports { + Lamports::Any => {} + Lamports::Exact(v) => { + let _ = v; + } + Lamports::Range(r) => { + let _ = r; + } + } panic!("any_account_info is only available under `cargo kani` (cfg(kani))"); } diff --git a/library/kani_solana_agent/src/invariants.rs b/library/kani_solana_agent/src/invariants.rs new file mode 100644 index 000000000000..507c4448d349 --- /dev/null +++ b/library/kani_solana_agent/src/invariants.rs @@ -0,0 +1,31 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +use solana_program::account_info::AccountInfo; + +pub fn lamports(account: &AccountInfo<'_>) -> u64 { + **account.lamports.borrow() +} + +pub fn sum_lamports(accounts: &[&AccountInfo<'_>]) -> u128 { + accounts.iter().map(|a| lamports(a) as u128).sum() +} + +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub struct LamportSnapshot(pub u128); + +impl LamportSnapshot { + pub fn new(accounts: &[&AccountInfo<'_>]) -> Self { + Self(sum_lamports(accounts)) + } + + pub fn assert_unchanged(self, accounts: &[&AccountInfo<'_>], msg: &'static str) { + let after = sum_lamports(accounts); + + #[cfg(kani)] + kani::assert(after == self.0, msg); + + #[cfg(not(kani))] + assert!(after == self.0, "{msg}"); + } +} diff --git a/library/kani_solana_agent/src/lib.rs b/library/kani_solana_agent/src/lib.rs index a6122cdb6943..b3e7e5a5f9e2 100644 --- a/library/kani_solana_agent/src/lib.rs +++ b/library/kani_solana_agent/src/lib.rs @@ -2,7 +2,9 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT pub mod account; +pub mod invariants; -pub use account::{AccountConfig, any_account_info}; +pub use account::{AccountConfig, any_account_info, any_agent_account}; +pub use invariants::{LamportSnapshot, lamports, sum_lamports}; pub use solana_program::account_info::AccountInfo; pub use solana_program::pubkey::Pubkey; diff --git a/tests/cargo-kani/solana-accountinfo/Cargo.toml b/tests/cargo-kani/solana-accountinfo/Cargo.toml index 1439b2a47146..3fc60a445396 100644 --- a/tests/cargo-kani/solana-accountinfo/Cargo.toml +++ b/tests/cargo-kani/solana-accountinfo/Cargo.toml @@ -10,4 +10,7 @@ edition = "2018" kani-solana-agent = { path = "../../../library/kani_solana_agent" } solana-program = "=3.0.0" +[lints.rust] +unexpected_cfgs = { level = "warn", check-cfg = ["cfg(kani)"] } + [workspace] diff --git a/tests/cargo-kani/solana-accountinfo/src/lib.rs b/tests/cargo-kani/solana-accountinfo/src/lib.rs index 1cdcfa3682eb..787dc64480c4 100644 --- a/tests/cargo-kani/solana-accountinfo/src/lib.rs +++ b/tests/cargo-kani/solana-accountinfo/src/lib.rs @@ -1,16 +1,15 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -use kani_solana_agent::{AccountConfig, AccountInfo, any_account_info}; +#[cfg(kani)] +use kani_solana_agent::AccountInfo; +#[cfg(kani)] fn authorized(now: i64, expires_at: i64, agent: &AccountInfo<'_>, api: &AccountInfo<'_>) -> bool { agent.is_signer || (api.is_signer && now >= expires_at) } -fn lamports(account: &AccountInfo<'_>) -> u64 { - **account.lamports.borrow() -} - +#[cfg(kani)] fn transfer(from: &AccountInfo<'_>, to: &AccountInfo<'_>, amount: u64) -> Result<(), ()> { let mut from_lamports = from.lamports.borrow_mut(); let Some(new_from) = (**from_lamports).checked_sub(amount) else { @@ -27,6 +26,7 @@ fn transfer(from: &AccountInfo<'_>, to: &AccountInfo<'_>, amount: u64) -> Result Ok(()) } +#[cfg(kani)] fn release_funds( now: i64, expires_at: i64, @@ -46,14 +46,15 @@ fn release_funds( #[cfg(kani)] mod proofs { use super::*; + use kani_solana_agent::{AccountConfig, LamportSnapshot, any_agent_account, lamports}; #[kani::proof] fn timelock_policy_matches_release_rule() { let now: i64 = kani::any(); let expires_at: i64 = kani::any(); - let mut agent = any_account_info::<0>(AccountConfig::new()); - let mut api = any_account_info::<0>(AccountConfig::new()); + let mut agent = any_agent_account::<0>(AccountConfig::new()); + let mut api = any_agent_account::<0>(AccountConfig::new()); agent.is_signer = kani::any(); api.is_signer = kani::any(); @@ -75,15 +76,15 @@ mod proofs { let expires_at: i64 = kani::any(); let amount: u64 = kani::any::() as u64; - let mut agent = any_account_info::<0>(AccountConfig::new()); - let mut api = any_account_info::<0>(AccountConfig::new()); + let mut agent = any_agent_account::<0>(AccountConfig::new()); + let mut api = any_agent_account::<0>(AccountConfig::new()); agent.is_signer = kani::any(); api.is_signer = kani::any(); - let escrow = any_account_info::<0>( + let escrow = any_agent_account::<0>( AccountConfig::new().writable().lamports_range(0..=(u32::MAX as u64)), ); - let payee = any_account_info::<0>( + let payee = any_agent_account::<0>( AccountConfig::new().writable().lamports_range(0..=(u32::MAX as u64)), ); @@ -91,15 +92,14 @@ mod proofs { let payee_before = lamports(&payee); kani::assume(escrow_before >= amount); - let total_before = escrow_before as u128 + payee_before as u128; + let total_before = LamportSnapshot::new(&[&escrow, &payee]); let res = release_funds(now, expires_at, &agent, &api, &escrow, &payee, amount); let escrow_after = lamports(&escrow); let payee_after = lamports(&payee); if res.is_ok() { - let total_after = escrow_after as u128 + payee_after as u128; - kani::assert(total_after == total_before, "release must conserve lamports"); + total_before.assert_unchanged(&[&escrow, &payee], "release must conserve lamports"); kani::assert(escrow_after + amount == escrow_before, "escrow must decrease by amount"); kani::assert(payee_before + amount == payee_after, "payee must increase by amount"); } else {