Solana Accounts

Most real Solana handlers take &[AccountInfo] and read/write account data. To verify them you need a way to produce nondeterministic accounts, read typed state out of them, and snapshot before/after. This page covers the account-handling helpers in cvlr-solana.

Producing nondet accounts

cvlr_deserialize_nondet_accounts

Spawn a fixed-size array of nondeterministic AccountInfos:

use cvlr::prelude::*;
use cvlr_solana::cvlr_deserialize_nondet_accounts;
use solana_program::account_info::{next_account_info, AccountInfo};

#[rule]
pub fn rule_deposit_smoke() {
    let acc_infos: [AccountInfo; 8] = cvlr_deserialize_nondet_accounts();
    let iter = &mut acc_infos.iter();
    let vault_info     = next_account_info(iter).unwrap();
    let user_info      = next_account_info(iter).unwrap();
    let token_program  = next_account_info(iter).unwrap();
    // ... rest of the harness ...
}

What you get:

  • An array of AccountInfos with internally-consistent memory layout — try_borrow_data, try_borrow_lamports, key, owner all work.

  • Each account’s data, lamports, key, and owner are independently havoced.

  • The array length is a compile-time constant. Pick the smallest size that matches your handler’s signature. Common values are 4, 8, 16.

Slicing to the right length

Many handlers take exactly N accounts. Allocate a generous array, then slice:

let acc_infos: [AccountInfo; 16] = cvlr_deserialize_nondet_accounts();
let used = &acc_infos[..5];   // pass `used` to the handler

This is convenient because you can keep the same array size across many rules and only slice differently per handler.

Pubkeys

use cvlr_solana::{cvlr_nondet_pubkey, cvlr_nondet_option_pubkey};
use solana_program::pubkey::Pubkey;

let program_id: Pubkey                  = cvlr_nondet_pubkey();
let optional:   Option<Pubkey>          = cvlr_nondet_option_pubkey();

Use cvlr_nondet_pubkey() rather than nondet::<Pubkey>() so the Prover treats it as an opaque 32-byte identifier rather than havocing 32 individual bytes (the latter is slower and produces a wider search space than necessary).

Reading typed state out of an account

POD types via bytemuck

If your account state is #[repr(C)] and Pod, you can borrow it directly from the account’s data buffer:

use bytemuck::{Pod, Zeroable};
use solana_program::account_info::AccountInfo;

#[repr(C)]
#[derive(Clone, Copy, Pod, Zeroable)]
pub struct Vault {
    pub tokens: u64,
    pub shares: u64,
    pub bump:   u8,
    _padding:   [u8; 7],
}

fn read_vault<'a>(info: &AccountInfo<'a>) -> &'a mut Vault {
    let data = info.try_borrow_mut_data().unwrap();
    bytemuck::from_bytes_mut(unsafe {
        // SAFETY: data borrow lives as long as the AccountInfo
        std::slice::from_raw_parts_mut(data.as_ptr() as *mut u8, data.len())
    })
}

In practice you’ll also want a value-only snapshot type for clog!:

pub struct VaultView {
    pub tokens: u64,
    pub shares: u64,
}

impl<'a> From<&AccountInfo<'a>> for VaultView {
    fn from(info: &AccountInfo) -> Self {
        let data = info.try_borrow_data().unwrap();
        let v: &Vault = bytemuck::from_bytes(&data[..core::mem::size_of::<Vault>()]);
        VaultView { tokens: v.tokens, shares: v.shares }
    }
}

Anchor accounts

Anchor wraps AccountInfo in typed Account<'info, T>, Signer<'info>, and Program<'info, T> handles. Building those wrappers from a havoced AccountInfo array needs a small set of project-local helpers — see Anchor for the helper set and a full Anchor harness example.

Account-loader-flavored helpers

Some projects use a trait-bound deserializer (often called something like FatAccountLoader). Where it exists, the verification harness mirrors the production loader pattern:

let loader = FatAccountLoader::<Vault>::try_from(&acc_infos[0]).unwrap();
let vault: &mut Vault = loader.load_mut().unwrap();

If the production code uses a custom loader, write a Nondet impl for the loaded type and reuse the production loader unchanged. The mock surface shrinks dramatically when you let the real deserialization paths execute on nondet bytes.

The clock and other sysvars

Some handlers branch on Clock::get(). To control the slot inside a rule, use cvlr-solana’s clock helpers:

use cvlr_solana::cvlr_advance_clock_slot;

cvlr_advance_clock_slot();             // moves the clock forward by a nondet amount
// run handler that reads Clock::get()
cvlr_advance_clock_slot();             // again, between two handler calls

For a full nondet Clock value:

use solana_program::clock::Clock;
let clock: Clock = cvlr::nondet::havoc::alloc_ref_havoced::<Clock>().clone();

(or implement Nondet for Clock once and reuse).

The pre/post snapshot pattern

Almost every account-touching rule has the same shape:

#[rule]
pub fn rule_deposit_preserves_solvency() {
    let acc_infos: [AccountInfo; 8] = cvlr_deserialize_nondet_accounts();
    let vault_info = &acc_infos[0];

    // 1. Read pre-state into a value snapshot.
    let pre: VaultView = vault_info.into();
    cvlr_assume!(pre.shares <= pre.tokens);    // protocol invariant

    // 2. Run the handler with nondet inputs.
    let amount: u64 = nondet();
    process_deposit(&acc_infos, amount).unwrap();

    // 3. Read post-state.
    let post: VaultView = vault_info.into();

    // 4. Log and assert.
    clog!(pre, post);
    cvlr_assert_le!(post.shares, post.tokens);
}

Steps 1, 3, 4 are entirely mechanical and look identical across rules. The Parametric Rules & Macros page shows how to factor them out so you only write the parts that vary.

Common pitfalls

  • Slice length mismatch. If your handler reads more accounts than you pass, it panics in next_account_info. Pick the array size to be at least as large as the largest handler in your rule set.

  • Forgetting to .unwrap() on the handler call. Without .unwrap(), the rule trivially succeeds even when the handler errors out — a common source of vacuous “passing” rules. Always either .unwrap() or cvlr_assume!(result.is_ok()) and assert on the post-state.

  • Sharing AccountInfos across rules unintentionally. Each #[rule] is a fresh universe; allocate accounts inside the rule, not in a static.

For Anchor-specific pitfalls (clone semantics on Accounts fields, Context bumps), see Anchor.

What’s next

  • Anchor — Anchor-specific helpers and end-to-end harnesses.

  • Parametric Rules & Macros — factor the snapshot pattern into reusable harnesses.

  • Methodology — how to scope rules so the Prover actually closes them.