feat(v2): add Kani + Miri verification harness

.github/workflows/tests.yaml

@@ -120,6 +120,38 @@ jobs:
           flags: v2
           fail_ci_if_error: false
 
+      # Miri (Tree Borrows) — UB + aliasing + provenance checks on the
+      # same integration tests above. Catches things the default cargo
+      # test run can't: `AccountView` copy-aliasing, `Slab::header_ptr`
+      # write provenance, `AccountCursor::next` strict-provenance walks.
+      # Caches the nightly toolchain and miri component to avoid a
+      # per-run rustup fetch (~200 MB).
+      - uses: actions/cache@v4
+        name: Cache rustup nightly + miri
+        with:
+          path: |
+            ~/.rustup/toolchains/
+            ~/.rustup/update-hashes/
+            ~/.rustup/settings.toml
+          key: rustup-miri-${{ runner.os }}-v2-${{ hashFiles('rust-toolchain*', '**/rust-toolchain*') }}
+          restore-keys: |
+            rustup-miri-${{ runner.os }}-v2-
+      - name: Install nightly + miri
+        run: |
+          rustup toolchain install nightly --component miri --profile minimal
+          cargo +nightly miri setup
+      - name: Miri (Tree Borrows) for anchor-lang-v2 + anchor-spl-v2
+        env:
+          MIRIFLAGS: '-Zmiri-tree-borrows'
+        run: cargo +nightly miri test -p anchor-lang-v2 -p anchor-spl-v2 --tests --features anchor-lang-v2/testing
+
+      # Kani harnesses live in-tree under `#[cfg(kani)]` and are runnable
+      # locally via `cargo kani -p anchor-lang-v2` / `-p anchor-spl-v2`,
+      # but are not wired into CI: kani-verifier 0.67.0 has an
+      # upstream-deterministic `.unwrap()` panic on CBMC `ERROR` status
+      # lines (kani#4519, fixed on main in #4540, not yet released).
+      # Re-enable once kani-verifier ≥ 0.68.0 ships on crates.io.
+
       # CLI: unit-test + build sanity only. No anchor-binary install,
       # no `anchor build`/`anchor test` flows, no tests/* integration.
       - run: cargo check -p anchor-cli

lang-v2/Cargo.toml

@@ -74,7 +74,7 @@ sha2 = "0.10"
 
 [lints.rust.unexpected_cfgs]
 level = "warn"
-check-cfg = ['cfg(target_os, values("solana"))']
+check-cfg = ['cfg(target_os, values("solana"))', 'cfg(kani)']
 
 # Integration tests that exercise `unsafe` paths via the `testing`
 # scaffold. Gated behind the `testing` feature so the mock types never
@@ -98,3 +98,23 @@ required-features = ["testing"]
 [[test]]
 name = "cursor_and_remaining_accounts"
 required-features = ["testing"]
+
+[[test]]
+name = "miri_account_view_aliasing"
+required-features = ["testing"]
+
+[[test]]
+name = "miri_cursor_walk"
+required-features = ["testing"]
+
+[[test]]
+name = "miri_slab_alignment"
+required-features = ["testing"]
+
+[[test]]
+name = "miri_slab_construction"
+required-features = ["testing"]
+
+[[test]]
+name = "miri_wrapper_accounts"
+required-features = ["testing"]

lang-v2/src/accounts/slab.rs

@@ -32,6 +32,24 @@ pub(super) fn cold_not_writable() -> ProgramError {
     ProgramError::InvalidAccountData
 }
 
+/// Capacity from live `data_len` / `items_offset` / `item_size`. Returns 0
+/// when `data_len < items_offset` to guard against underflow if an external
+/// `realloc_account` shrinks the buffer while a `Slab` is retained. Caller
+/// must ensure `item_size > 0` (`Slab` skips this for ZST items).
+///
+/// Factored out of `Slab::capacity` as a free `const fn` so the Kani proofs
+/// below (`capacity_never_underflows`, `capacity_fits_within_data_len_item_*`,
+/// `clamp_never_exceeds_capacity`) can reason about it in isolation from
+/// `Slab`'s generic plumbing.
+#[inline(always)]
+const fn capacity_for(data_len: usize, items_offset: usize, item_size: usize) -> usize {
+    if data_len < items_offset {
+        0
+    } else {
+        (data_len - items_offset) / item_size
+    }
+}
+
 /// `Account<H>` / `BorshAccount<H>` get `AccountInitialize` for free by
 /// running `H::SlabInit::create_and_initialize(...)` and then loading.
 impl<H, T> AccountInitialize for Slab<H, T>
@@ -396,7 +414,11 @@ where
     /// account below the Slab's structural minimum).
     #[inline(always)]
     pub fn capacity(&self) -> usize {
-        self.view.data_len().saturating_sub(Self::ITEMS_OFFSET) / core::mem::size_of::<T>()
+        capacity_for(
+            self.view.data_len(),
+            Self::ITEMS_OFFSET,
+            core::mem::size_of::<T>(),
+        )
     }
 
     /// Live `len` clamped to current `capacity`. The stored `len` may
@@ -754,3 +776,92 @@ where
         H::__register_idl_deps(types);
     }
 }
+
+// Kani proofs for the `capacity_for` helper, which backs `Slab::capacity`
+// and therefore every slice-bounds computation in the tail-region
+// accessors (`as_slice`, `as_mut_slice`, push/pop/swap_remove). Proving
+// these invariants on the free function means any regression to the
+// production formula (e.g. replacing the `data_len < items_offset` guard
+// with a raw subtract) will break CBMC/Z3's proof obligations.
+#[cfg(kani)]
+mod kani_proofs {
+    use super::capacity_for;
+
+    // Generous bounds on the symbolic inputs — well above any realistic
+    // Slab account, but tight enough for CBMC/Z3 to converge.
+    const DATA_LEN_MAX: usize = 1 << 16;
+    const OFFSET_MAX: usize = 1024;
+    const ITEM_SIZE_MAX: usize = 1024;
+
+    // `capacity_for` never panics or wraps for any valid input.
+    #[kani::proof]
+    fn capacity_never_underflows() {
+        let data_len: usize = kani::any();
+        let items_offset: usize = kani::any();
+        let item_size: usize = kani::any();
+        kani::assume(item_size > 0);
+        kani::assume(data_len <= DATA_LEN_MAX);
+        kani::assume(items_offset <= OFFSET_MAX);
+        kani::assume(item_size <= ITEM_SIZE_MAX);
+        let _ = capacity_for(data_len, items_offset, item_size);
+    }
+
+    // Normal case: `items_offset + capacity * item_size <= data_len` —
+    // the invariant `as_slice`'s slice-bounds depends on.
+    //
+    // A single symbolic-`item_size` harness would be ideal, but the Linux
+    // Kani 0.67.0 bundle's CBMC aborts during bitvector encoding on
+    // symbolic `usize × usize` multiplication (macOS bundle is fine). The
+    // abort surfaces as an unparseable `ERROR` status that panics
+    // `kani-driver` before Z3 sees the goal, so `#[kani::solver(z3)]`
+    // can't rescue it. Splitting per-concrete `item_size` turns the
+    // multiplication into linear arithmetic CBMC dispatches trivially;
+    // the covered set spans every Pod width the codebase uses (u8 → u128,
+    // Pubkey = 32) plus powers of two up to 1024.
+    macro_rules! capacity_fits_within_data_len_for {
+        ($name:ident, $item_size:expr) => {
+            #[kani::proof]
+            fn $name() {
+                const ITEM_SIZE: usize = $item_size;
+                let data_len: usize = kani::any();
+                let items_offset: usize = kani::any();
+                kani::assume(data_len <= DATA_LEN_MAX);
+                kani::assume(items_offset <= OFFSET_MAX);
+                kani::assume(data_len >= items_offset);
+                let capacity = capacity_for(data_len, items_offset, ITEM_SIZE);
+                assert!(items_offset + capacity * ITEM_SIZE <= data_len);
+            }
+        };
+    }
+    capacity_fits_within_data_len_for!(capacity_fits_within_data_len_item_1, 1);
+    capacity_fits_within_data_len_for!(capacity_fits_within_data_len_item_2, 2);
+    capacity_fits_within_data_len_for!(capacity_fits_within_data_len_item_4, 4);
+    capacity_fits_within_data_len_for!(capacity_fits_within_data_len_item_8, 8);
+    capacity_fits_within_data_len_for!(capacity_fits_within_data_len_item_16, 16);
+    capacity_fits_within_data_len_for!(capacity_fits_within_data_len_item_32, 32);
+    capacity_fits_within_data_len_for!(capacity_fits_within_data_len_item_64, 64);
+    capacity_fits_within_data_len_for!(capacity_fits_within_data_len_item_128, 128);
+    capacity_fits_within_data_len_for!(capacity_fits_within_data_len_item_256, 256);
+    capacity_fits_within_data_len_for!(capacity_fits_within_data_len_item_512, 512);
+    capacity_fits_within_data_len_for!(capacity_fits_within_data_len_item_1024, 1024);
+
+    // The `.min(capacity)` clamp in `Slab::as_slice`'s `effective_len`
+    // never exceeds `capacity`, regardless of the raw stored `len` (which
+    // may exceed `capacity` when a retained Slab's buffer has been shrunk
+    // externally via `realloc_account`).
+    //
+    // Combined with `capacity_fits_within_data_len_for!(…)`:
+    //   `clamped_len ≤ capacity`
+    //   ∧  `items_offset + capacity * item_size ≤ data_len`
+    //   ⟹  `items_offset + clamped_len * item_size ≤ data_len`
+    // — the slice-bounds invariant that `as_slice` depends on.
+    #[kani::proof]
+    fn clamp_never_exceeds_capacity() {
+        let capacity: usize = kani::any();
+        let raw_len: usize = kani::any();
+        kani::assume(capacity <= DATA_LEN_MAX);
+        kani::assume(raw_len <= DATA_LEN_MAX);
+        let clamped_len = if raw_len < capacity { raw_len } else { capacity };
+        assert!(clamped_len <= capacity);
+    }
+}

lang-v2/src/cpi.rs

@@ -13,6 +13,33 @@ use {
 #[cfg(feature = "const-rent")]
 const MAX_SAFE_SPACE: u64 = (u64::MAX / DEFAULT_LAMPORTS_PER_BYTE) - ACCOUNT_STORAGE_OVERHEAD;
 
+/// System program `Transfer` instruction discriminant (variant index).
+/// Encoded as `u32 LE` in the first 4 bytes of the instruction data.
+#[cfg(feature = "account-resize")]
+const SYSTEM_TRANSFER_VARIANT: u8 = 2;
+
+// Pin the protocol-mandated discriminant at compile time. Without this,
+// the wire-format Kani harness below would still pass if someone edited
+// `SYSTEM_TRANSFER_VARIANT` (both sides of its byte-equality reference
+// the same constant).
+#[cfg(feature = "account-resize")]
+const _: () = assert!(SYSTEM_TRANSFER_VARIANT == 2);
+
+/// Encode a System program `Transfer` instruction body.
+///
+/// Extracted as a pure helper so the Kani harness in this module can verify
+/// the real encoder byte-for-byte against the documented wire format. The
+/// encoding is otherwise only reachable through `realloc_account`'s unsafe
+/// CPI path, which Kani cannot model (the CPI syscall is opaque to CBMC).
+#[cfg(feature = "account-resize")]
+#[inline]
+fn encode_system_transfer(lamports: u64) -> [u8; 12] {
+    let mut data = [0u8; 12];
+    data[0] = SYSTEM_TRANSFER_VARIANT;
+    data[4..12].copy_from_slice(&lamports.to_le_bytes());
+    data
+}
+
 /// Compute the rent-exempt minimum balance for an account of `space` bytes.
 ///
 /// Default path calls `Rent::get()` (picks up runtime formula changes).
@@ -477,14 +504,12 @@ pub fn realloc_account(
             // bytes — disjoint region, no aliasing. The unchecked path
             // bypasses pinocchio's borrow-flag check which would otherwise
             // reject the CPI while the RefMut is held.
+            let ix_data = encode_system_transfer(deficit);
             unsafe {
                 let cpi_accounts: [pinocchio::cpi::CpiAccount; 2] = [
                     pinocchio::cpi::CpiAccount::from(payer),
                     pinocchio::cpi::CpiAccount::from(&*account as &AccountView),
                 ];
-                let mut ix_data = [0u8; 12];
-                ix_data[0] = 2;
-                ix_data[4..12].copy_from_slice(&deficit.to_le_bytes());
                 let instruction = pinocchio::instruction::InstructionView {
                     program_id: &pinocchio_system::ID,
                     accounts: &[
@@ -534,3 +559,131 @@ pub fn realloc_account(
 
     Ok(())
 }
+
+#[cfg(all(test, feature = "const-rent"))]
+mod const_rent_tests {
+    use super::*;
+
+    // `space > MAX_SAFE_SPACE` must short-circuit to an error before the
+    // formula runs. Covered by unit test because the branch is boolean —
+    // a couple of boundary values suffice and Kani adds no value.
+    #[test]
+    fn rejects_oversized_space() {
+        assert!(rent_exempt_lamports(MAX_SAFE_SPACE as usize + 1).is_err());
+        assert!(rent_exempt_lamports(usize::MAX).is_err());
+    }
+
+    // Base case: space == 0 charges only the fixed storage overhead.
+    #[test]
+    fn zero_space_returns_overhead_only() {
+        assert_eq!(
+            rent_exempt_lamports(0).unwrap(),
+            ACCOUNT_STORAGE_OVERHEAD * DEFAULT_LAMPORTS_PER_BYTE,
+        );
+    }
+}
+
+// ---------------------------------------------------------------------------
+// Kani proofs — CPI helper invariants
+// ---------------------------------------------------------------------------
+
+#[cfg(all(kani, feature = "const-rent"))]
+mod kani_proofs_const_rent {
+    use super::*;
+
+    // For accepted inputs, the wrapping_mul does not actually wrap.
+    // The comment "Bounded by MAX_SAFE_SPACE → no overflow" is load-bearing.
+    #[kani::proof]
+    #[kani::solver(z3)]
+    fn accepted_inputs_do_not_overflow() {
+        let space: usize = kani::any();
+        kani::assume(space as u64 <= MAX_SAFE_SPACE);
+        // The wrapping_mul in the implementation must equal the checked_mul
+        // result (no overflow actually happened).
+        let sum = (ACCOUNT_STORAGE_OVERHEAD + space as u64);
+        let wrapping = sum.wrapping_mul(DEFAULT_LAMPORTS_PER_BYTE);
+        let checked = sum.checked_mul(DEFAULT_LAMPORTS_PER_BYTE);
+        assert!(checked == Some(wrapping));
+    }
+
+    // At the boundary space == MAX_SAFE_SPACE, the computed result
+    // fits in u64.
+    #[kani::proof]
+    #[kani::solver(z3)]
+    fn boundary_space_value_fits_u64() {
+        let result = rent_exempt_lamports(MAX_SAFE_SPACE as usize);
+        assert!(result.is_ok());
+    }
+
+    // Monotonicity: larger space ⇒ ≥ rent. (Logic invariant — required
+    // by any sensible fee schedule.)
+    #[kani::proof]
+    #[kani::solver(z3)]
+    fn rent_is_monotonic_in_space() {
+        let a: usize = kani::any();
+        let b: usize = kani::any();
+        kani::assume(a <= b);
+        kani::assume(b as u64 <= MAX_SAFE_SPACE);
+        let ra = rent_exempt_lamports(a).unwrap();
+        let rb = rent_exempt_lamports(b).unwrap();
+        assert!(ra <= rb);
+    }
+}
+
+#[cfg(kani)]
+mod kani_proofs_pda {
+    use super::*;
+
+    // Length-guard only. Proves that `try_find_program_address` rejects
+    // inputs with more than 16 seeds (Solana runtime cap). Does NOT
+    // verify PDA derivation correctness, bump-search behavior, or seed
+    // content handling — those live in the Solana runtime's own test
+    // suite and are exercised end-to-end by the litesvm tests.
+    #[kani::proof]
+    fn seventeen_seeds_rejected() {
+        let empty: &[u8] = &[];
+        let seeds: [&[u8]; 17] = [empty; 17];
+        let pid = Address::new_from_array([0u8; 32]);
+        assert!(try_find_program_address(&seeds, &pid).is_err());
+    }
+}
+
+// ---------------------------------------------------------------------------
+// Kani proofs — System program Transfer wire format byte-identity
+//
+// `realloc_account` hand-encodes a System Transfer instruction instead of
+// going through `pinocchio_system::instructions::Transfer` (to bypass the
+// borrow-flag check while a BorshAccount RefMut is live). This harness
+// verifies that the hand encoding matches the documented wire format:
+//   [variant u32 LE] [lamports u64 LE]
+// The `SYSTEM_TRANSFER_VARIANT` constant is shared with the production
+// encoder — if someone edits it, both sides move together.
+//
+// Allocate / Assign / CreateAccount go through pinocchio-system directly,
+// so their encoding lives outside anchor-v2 and isn't verified here.
+// ---------------------------------------------------------------------------
+
+#[cfg(all(kani, feature = "account-resize"))]
+mod kani_proofs_cpi_wire {
+    use super::{encode_system_transfer, SYSTEM_TRANSFER_VARIANT};
+
+    // Calls the real `encode_system_transfer` helper (the same one
+    // `realloc_account` uses) so a layout change in the encoder — moving a
+    // field, swapping endianness, truncating bytes — fails this harness.
+    // Paired with the `const _: () = assert!(SYSTEM_TRANSFER_VARIANT == 2)`
+    // guard near the constant definition, this proves both "the encoder
+    // produces the protocol format" and "the protocol constant is correct."
+    #[kani::proof]
+    fn anchor_transfer_encoding_matches_wire_format() {
+        let lamports: u64 = kani::any();
+
+        let anchor_encoded = encode_system_transfer(lamports);
+
+        // Documented wire format: [variant u32 LE] [lamports u64 LE].
+        let mut wire_format = [0u8; 12];
+        wire_format[0..4].copy_from_slice(&(SYSTEM_TRANSFER_VARIANT as u32).to_le_bytes());
+        wire_format[4..12].copy_from_slice(&lamports.to_le_bytes());
+
+        assert!(anchor_encoded == wire_format);
+    }
+}