hopper_native/

sysvar.rs

//! Sysvar access via direct syscalls.
//!
//! Provides zero-alloc, zero-deserialization access to Solana sysvars
//! by reading them directly into stack buffers via syscalls, including the
//! epoch schedule sysvar.

use crate::address::Address;
use crate::error::ProgramError;

// ── Clock ────────────────────────────────────────────────────────────

/// Clock sysvar data, read directly from the runtime.
#[repr(C)]
#[derive(Clone, Copy, Debug, Default)]
pub struct Clock {
    pub slot: u64,
    pub epoch_start_timestamp: i64,
    pub epoch: u64,
    pub leader_schedule_epoch: u64,
    pub unix_timestamp: i64,
}

/// Read the Clock sysvar.
#[inline]
pub fn get_clock() -> Result<Clock, ProgramError> {
    #[allow(unused_mut)]
    let mut clock = Clock::default();
    #[cfg(target_os = "solana")]
    {
        // The generic `sol_get_sysvar` read costs 110 CU for any image under
        // 2,500 bytes, the dedicated `sol_get_clock_sysvar` 100 plus the
        // 40-byte struct. The bincode image is five little-endian 8-byte
        // words in field order, exactly the `#[repr(C)]` layout
        // (`clock_reads_canonical_byte_image` pins it), so it is read
        // straight into the struct.
        // SAFETY: `Clock` is repr(C) with size 40, every bit pattern of its
        // integer fields is valid, and the view covers exactly the struct.
        let image = unsafe {
            core::slice::from_raw_parts_mut(
                &mut clock as *mut Clock as *mut u8,
                core::mem::size_of::<Clock>(),
            )
        };
        get_sysvar_into(&CLOCK_ID, 0, image)?;
    }
    Ok(clock)
}

impl Clock {
    /// Read the Clock sysvar.
    ///
    /// Method-style alias for [`get_clock`], matching the `Sysvar::get()`
    /// ergonomics other Solana frameworks expose (`Clock::get()`).
    #[inline]
    pub fn get() -> Result<Self, ProgramError> {
        get_clock()
    }
}

// ── Rent ─────────────────────────────────────────────────────────────

/// Rent sysvar data.
#[repr(C)]
#[derive(Clone, Copy, Debug, Default)]
pub struct Rent {
    pub lamports_per_byte_year: u64,
    pub exemption_threshold: f64,
    pub burn_percent: u8,
}

/// Lamports charged per byte of account storage per year.
///
/// This is the launch-era value baked into Solana's original rent config. It
/// is a historical snapshot of a runtime-owned parameter; Mainnet now carries
/// the effective per-byte rate directly in the live [`Rent`] sysvar.
/// Reaping-relevant decisions must read that sysvar (see
/// [`Rent::minimum_balance`]), not this constant.
pub const LAMPORTS_PER_BYTE_YEAR: u64 = 3_480;

/// Years of rent an account must prepay to be rent-exempt.
///
/// Launch-era snapshot of the runtime's `exemption_threshold`. SIMD-0194
/// deprecated the field and Mainnet now stores `1.0`, while the effective
/// per-byte rate carries the complete price. The field remains in the wire
/// layout for compatibility.
pub const EXEMPTION_THRESHOLD_YEARS: u64 = 2;

/// Fixed per-account storage overhead charged by the cluster.
pub const ACCOUNT_STORAGE_OVERHEAD: u64 = 128;

/// Minimum balance for rent exemption **assuming the launch-era rent
/// constants** ([`LAMPORTS_PER_BYTE_YEAR`], [`EXEMPTION_THRESHOLD_YEARS`],
/// [`ACCOUNT_STORAGE_OVERHEAD`]).
///
/// This is the fast, allocation-free, syscall-free path: pure `const`
/// integer arithmetic over hardcoded constants. It is exact **for a cluster
/// running that legacy config** and byte-matches [`Rent::minimum_balance`]
/// when the live sysvar carries those same constants.
///
/// # SAFETY-CRITICAL caveat, do NOT gate reaping on this
///
/// Because the constants are hardcoded, this function cannot see a rent
/// *reprice*. It can overcharge after a reduction or under-fund after a later
/// increase. Any code path that decides whether an account is safe from
/// reaping, topping an account up to exemption, or gating a resize on it,
/// must therefore use the live value.
///
/// For those paths read the live [`Rent`] sysvar and call
/// [`Rent::minimum_balance`] (see [`crate::batch::require_rent_exempt_with`]
/// and [`crate::batch::realloc_checked_with`]). Keep this const form only
/// where a fixed legacy snapshot is explicitly intended.
#[inline]
pub const fn rent_exempt_minimum(data_len: usize) -> u64 {
    (data_len as u64 + ACCOUNT_STORAGE_OVERHEAD)
        * LAMPORTS_PER_BYTE_YEAR
        * EXEMPTION_THRESHOLD_YEARS
}

/// Read the Rent sysvar.
#[inline]
pub fn get_rent() -> Result<Rent, ProgramError> {
    #[cfg(target_os = "solana")]
    {
        // 17-byte bincode image (u64 rate, f64 threshold, u8 burn percent)
        // at the same offsets as the first 17 bytes of the repr(C) struct,
        // written straight into uninitialized memory: zeroing the struct
        // first cost three stores the syscall then overwrote. The padding
        // after `burn_percent` stays uninitialized, as a `Copy` struct's
        // padding may. 110 CU through `sol_get_sysvar` instead of 124
        // through `sol_get_rent_sysvar`.
        let mut rent = core::mem::MaybeUninit::<Rent>::uninit();
        // SAFETY: `RENT_ID` is a 32-byte address and the destination is the
        // first `RENT_IMAGE_LEN` bytes of `rent` (the offsets are pinned
        // below); the syscall writes exactly that many bytes or none.
        let rc = unsafe {
            crate::syscalls::sol_get_sysvar(
                RENT_ID.as_array().as_ptr(),
                rent.as_mut_ptr() as *mut u8,
                0,
                RENT_IMAGE_LEN as u64,
            )
        };
        if rc != 0 {
            return Err(ProgramError::UnsupportedSysvar);
        }
        // SAFETY: the syscall succeeded, so it wrote all three fields (the
        // rate, the threshold, and the burn percent), every bit pattern of
        // which is valid; only padding is left uninitialized.
        Ok(unsafe { rent.assume_init() })
    }
    #[cfg(not(target_os = "solana"))]
    {
        Ok(Rent::default())
    }
}

/// Length of the Rent sysvar's account image: `u64 + f64 + u8`.
pub const RENT_IMAGE_LEN: usize = 17;

const _: () = {
    assert!(core::mem::offset_of!(Rent, lamports_per_byte_year) == 0);
    assert!(core::mem::offset_of!(Rent, exemption_threshold) == 8);
    assert!(core::mem::offset_of!(Rent, burn_percent) == 16);
    assert!(core::mem::size_of::<Rent>() >= RENT_IMAGE_LEN);
};

impl Rent {
    /// Read the Rent sysvar.
    ///
    /// Method-style alias for [`get_rent`], matching the `Sysvar::get()`
    /// ergonomics other Solana frameworks expose (`Rent::get()`).
    #[inline]
    pub fn get() -> Result<Self, ProgramError> {
        get_rent()
    }

    /// Minimum lamports for rent exemption at `data_len`, computed from the
    /// **live sysvar** values, the correct source for reaping-relevant
    /// decisions after a rent reprice.
    ///
    /// This follows Solana's own `solana_rent::Rent::minimum_balance` for the
    /// two thresholds any cluster has stored, with no floating point at all:
    ///
    /// ```text
    /// integer_part = (ACCOUNT_STORAGE_OVERHEAD + data_len) * rate
    /// threshold 1.0 => integer_part
    /// threshold 2.0 => integer_part * 2
    /// otherwise     => integer_part * ceil(threshold)   (never below Solana's
    ///                  `(integer_part as f64 * threshold) as u64`)
    /// ```
    ///
    /// SIMD-0194 made `1.0` the live wire marker and moved the full price into
    /// the rate field; `2.0` is the launch-era value. Both are matched by bit
    /// pattern (see [`scale_by_exemption_threshold`]), so a program that reads
    /// the sysvar links no soft-float code. A threshold no cluster has ever
    /// used rounds up to whole years, which can only overfund.
    ///
    /// The integer product uses saturating ops purely as an overflow guard;
    /// for every loader-permitted `data_len` (`<= 10_485_760`) and realistic
    /// `lamports_per_byte_year` it never saturates, so the byte-match with the
    /// runtime is exact (proven in the Kani harnesses below).
    #[inline(always)]
    pub fn minimum_balance(&self, data_len: usize) -> u64 {
        // The same product Solana's `Rent::minimum_balance` computes, which
        // does not saturate either: the loader caps `data_len` at 10 MiB, so
        // the byte term is below 2^24 and the product below 2^64 for any
        // rate under 2^40 lamports per byte-year. `saturating_mul` here
        // linked and called the 128-bit `__multi3` helper (344 bytes, about
        // 50 CU) on every `init` (measured 2026-09-21).
        let bytes = data_len as u64;
        let integer_part = ACCOUNT_STORAGE_OVERHEAD
            .saturating_add(bytes)
            .wrapping_mul(self.lamports_per_byte_year);
        scale_by_exemption_threshold(integer_part, self.exemption_threshold.to_bits())
    }
}

pub use crate::arith::saturating_mul_u64;

/// Bit pattern of `1.0f64`, the SIMD-0194 live threshold marker.
const THRESHOLD_ONE_BITS: u64 = 0x3FF0_0000_0000_0000;
/// Bit pattern of `2.0f64`, the launch-era threshold.
const THRESHOLD_TWO_BITS: u64 = 0x4000_0000_0000_0000;

/// Apply the rent `exemption_threshold` (given as its IEEE-754 bit pattern)
/// to an integer lamport amount **without any floating-point instruction**.
///
/// sBPF has no FPU: every `f64` compare or multiply lowers to a soft-float
/// library call, and the launch-era formula's `(x as f64 * t) as u64`
/// fallback dragged `__muldf3`, `__floatundidf`, and `__fixunsdfdi` into
/// every program that read the Rent sysvar (measured 2026-09-21 on the
/// framework-comparison counter: 2,528 bytes of `.text` for a path no
/// cluster has ever taken). The two thresholds that have existed are
/// matched by bit pattern and are exact: `1.0`, the SIMD-0194 wire marker
/// every public cluster stores today, and the launch-era `2.0`. Any other
/// finite positive threshold is rounded **up** to a whole number of years
/// with integer arithmetic, which can only overfund, never underfund, so a
/// rent-exemption decision made through it stays safe. Saturates at
/// `u64::MAX` (an infinite threshold saturates too); a zero, negative, or
/// NaN threshold yields `0`, the same as the cast.
///
/// The two real thresholds are tested inline; the rounding path for any
/// other value is out of line and cold.
#[inline(always)]
pub fn scale_by_exemption_threshold(integer_part: u64, threshold_bits: u64) -> u64 {
    if threshold_bits == THRESHOLD_ONE_BITS {
        return integer_part;
    }
    if threshold_bits == THRESHOLD_TWO_BITS {
        return integer_part.saturating_mul(2);
    }
    scale_by_unusual_threshold(integer_part, threshold_bits)
}

#[cold]
#[inline(never)]
fn scale_by_unusual_threshold(integer_part: u64, threshold_bits: u64) -> u64 {
    saturating_mul_u64(integer_part, ceil_years(threshold_bits))
}

/// Ceiling of a double (given as bits) as a `u64`, saturating: the whole
/// number of years a non-standard threshold rounds up to. Zero, negative,
/// and NaN give `0`; anything in `(0, 1]` gives `1`; infinity saturates.
#[inline]
fn ceil_years(bits: u64) -> u64 {
    if bits >> 63 == 1 {
        return 0;
    }
    let exponent = ((bits >> 52) & 0x7FF) as i32;
    let mantissa = bits & ((1u64 << 52) - 1);
    if exponent == 0x7FF {
        return if mantissa == 0 { u64::MAX } else { 0 };
    }
    if exponent == 0 {
        // Zero, or a subnormal that still rounds up to one year.
        return if mantissa == 0 { 0 } else { 1 };
    }
    // value = 1.mantissa * 2^(exponent - 1023)
    let e = exponent - 1023;
    if e < 0 {
        return 1;
    }
    if e >= 64 {
        return u64::MAX;
    }
    let significand = (1u64 << 52) | mantissa;
    if e >= 52 {
        return significand << (e - 52);
    }
    let shift = (52 - e) as u32;
    let whole = significand >> shift;
    let fraction = significand & ((1u64 << shift) - 1);
    if fraction == 0 {
        whole
    } else {
        whole + 1
    }
}

// ── Epoch Schedule ───────────────────────────────────────────────────

/// Epoch schedule sysvar data.
///
/// Nobody wraps this at the native level. Useful for programs that
/// need to reason about epoch boundaries (staking, vesting, time locks).
#[repr(C)]
#[derive(Clone, Copy, Debug, Default)]
pub struct EpochSchedule {
    pub slots_per_epoch: u64,
    pub leader_schedule_slot_offset: u64,
    pub warmup: bool,
    pub first_normal_epoch: u64,
    pub first_normal_slot: u64,
}

// ABI lock: `sol_get_epoch_schedule_sysvar` memcpy's the runtime's
// `#[repr(C)]` `EpochSchedule` into this buffer. The canonical Agave
// definition (solana-sdk `epoch-schedule`) is `#[repr(C)]` with field
// order `slots_per_epoch, leader_schedule_slot_offset, warmup,
// first_normal_epoch, first_normal_slot`. The `bool` sits between two
// u64 fields, so the layout depends on `repr(C)` padding, any drift in
// field order or repr here silently misreads every field after `warmup`.
// These asserts fail the build if that ever happens.
const _: () = {
    assert!(core::mem::size_of::<EpochSchedule>() == 40);
    assert!(core::mem::align_of::<EpochSchedule>() == 8);
    assert!(core::mem::offset_of!(EpochSchedule, slots_per_epoch) == 0);
    assert!(core::mem::offset_of!(EpochSchedule, leader_schedule_slot_offset) == 8);
    assert!(core::mem::offset_of!(EpochSchedule, warmup) == 16);
    assert!(core::mem::offset_of!(EpochSchedule, first_normal_epoch) == 24);
    assert!(core::mem::offset_of!(EpochSchedule, first_normal_slot) == 32);
};

// The Clock sysvar is also memcpy'd from a `#[repr(C)]` runtime struct.
const _: () = {
    assert!(core::mem::size_of::<Clock>() == 40);
    assert!(core::mem::offset_of!(Clock, slot) == 0);
    assert!(core::mem::offset_of!(Clock, epoch_start_timestamp) == 8);
    assert!(core::mem::offset_of!(Clock, epoch) == 16);
    assert!(core::mem::offset_of!(Clock, leader_schedule_epoch) == 24);
    assert!(core::mem::offset_of!(Clock, unix_timestamp) == 32);
};

/// Read the EpochSchedule sysvar.
#[inline]
pub fn get_epoch_schedule() -> Result<EpochSchedule, ProgramError> {
    #[cfg(target_os = "solana")]
    {
        // 33-byte bincode image: two u64, one bool byte, two u64. The
        // repr(C) struct pads the bool to eight bytes, so the image is
        // decoded field by field. 110 CU through `sol_get_sysvar` instead
        // of 140 through the dedicated syscall.
        let mut image = [0u8; EPOCH_SCHEDULE_IMAGE_LEN];
        get_sysvar_into(&EPOCH_SCHEDULE_ID, 0, &mut image)?;
        Ok(decode_epoch_schedule(&image))
    }
    #[cfg(not(target_os = "solana"))]
    {
        Ok(EpochSchedule::default())
    }
}

/// Length of the EpochSchedule sysvar's account image.
pub const EPOCH_SCHEDULE_IMAGE_LEN: usize = 33;

/// Decode the EpochSchedule account image (`epoch_schedule_decodes_canonical_image`
/// pins the offsets).
#[inline]
pub fn decode_epoch_schedule(image: &[u8; EPOCH_SCHEDULE_IMAGE_LEN]) -> EpochSchedule {
    let rd8 = |o: usize| {
        u64::from_le_bytes([
            image[o],
            image[o + 1],
            image[o + 2],
            image[o + 3],
            image[o + 4],
            image[o + 5],
            image[o + 6],
            image[o + 7],
        ])
    };
    EpochSchedule {
        slots_per_epoch: rd8(0),
        leader_schedule_slot_offset: rd8(8),
        warmup: image[16] != 0,
        first_normal_epoch: rd8(17),
        first_normal_slot: rd8(25),
    }
}

impl EpochSchedule {
    /// Get the epoch for a given slot.
    #[inline]
    pub fn get_epoch(&self, slot: u64) -> u64 {
        if slot < self.first_normal_slot {
            // During warmup, epoch length doubles each epoch.
            // Initial epoch has 32 slots (MINIMUM_SLOTS_PER_EPOCH).
            if slot == 0 {
                return 0;
            }
            // log2(slot / 32) + 1, clamped.
            let mut epoch_len: u64 = 32; // MINIMUM_SLOTS_PER_EPOCH
            let mut epoch: u64 = 0;
            let mut slot_remaining = slot;
            while slot_remaining >= epoch_len {
                slot_remaining -= epoch_len;
                epoch += 1;
                epoch_len = epoch_len.saturating_mul(2);
            }
            epoch
        } else {
            let normal_slot_index = slot - self.first_normal_slot;
            self.first_normal_epoch + normal_slot_index / self.slots_per_epoch
        }
    }

    /// Get the first slot in the given epoch.
    #[inline]
    pub fn get_first_slot_in_epoch(&self, epoch: u64) -> u64 {
        if epoch <= self.first_normal_epoch {
            // Warmup: each epoch doubles in length starting from 32.
            if epoch == 0 {
                return 0;
            }
            // First slot = sum of all previous epoch lengths.
            // = 32 * (2^epoch - 1)
            let shift = epoch.min(63);
            32_u64.saturating_mul((1_u64 << shift).saturating_sub(1))
        } else {
            let normal_epoch_index = epoch - self.first_normal_epoch;
            self.first_normal_slot + normal_epoch_index * self.slots_per_epoch
        }
    }
}

// ── Well-known sysvar addresses ──────────────────────────────────────

/// Clock sysvar address.
pub const CLOCK_ID: Address = crate::address!("SysvarC1ock11111111111111111111111111111111");

/// Rent sysvar address.
pub const RENT_ID: Address = crate::address!("SysvarRent111111111111111111111111111111111");

/// Epoch schedule sysvar address.
pub const EPOCH_SCHEDULE_ID: Address =
    crate::address!("SysvarEpochSchedu1e111111111111111111111111");

/// SlotHashes sysvar address.
pub const SLOT_HASHES_ID: Address = crate::address!("SysvarS1otHashes111111111111111111111111111");

/// StakeHistory sysvar address.
pub const STAKE_HISTORY_ID: Address =
    crate::address!("SysvarStakeHistory1111111111111111111111111");

/// Instructions sysvar address (for instruction introspection).
pub const INSTRUCTIONS_ID: Address = crate::address!("Sysvar1nstructions1111111111111111111111111");

/// EpochRewards sysvar address (SIMD-0118).
pub const EPOCH_REWARDS_ID: Address =
    crate::address!("SysvarEpochRewards1111111111111111111111111");

// ── Generalized sysvar access (sol_get_sysvar) ──────────────────────

/// Copy `dst.len()` bytes starting at `offset` from the sysvar identified
/// by `sysvar_id` into `dst`.
///
/// This wraps the `sol_get_sysvar` syscall (SIMD-0127, active on every
/// public cluster), the cheapest read of any sysvar: 110 CU for an image
/// under 2,500 bytes, against 100 plus the struct size for the dedicated
/// getters. Every Hopper sysvar reader goes through it. Returns
/// `Err(UnsupportedSysvar)` on syscall failure (an unknown sysvar, or a
/// read past the sysvar's length).
#[inline]
pub fn get_sysvar_into(
    sysvar_id: &Address,
    offset: u64,
    dst: &mut [u8],
) -> Result<(), ProgramError> {
    #[cfg(target_os = "solana")]
    {
        // SAFETY: `sysvar_id` is a 32-byte address; `dst` is valid for its
        // own length; the syscall copies exactly `dst.len()` bytes or none.
        let rc = unsafe {
            crate::syscalls::sol_get_sysvar(
                sysvar_id.as_array().as_ptr(),
                dst.as_mut_ptr(),
                offset,
                dst.len() as u64,
            )
        };
        if rc != 0 {
            return Err(ProgramError::UnsupportedSysvar);
        }
    }
    #[cfg(not(target_os = "solana"))]
    {
        let _ = (sysvar_id, offset, dst);
    }
    Ok(())
}

/// The syscall's result for a read past the sysvar's length (Agave
/// `sysvar.rs`, `OFFSET_LENGTH_EXCEEDS_SYSVAR`); every other nonzero result
/// is a hard failure.
#[cfg(target_os = "solana")]
const OFFSET_LENGTH_EXCEEDS_SYSVAR: u64 = 1;

/// [`get_sysvar_into`] that reports a read past the sysvar's end as
/// `Ok(false)` instead of an error, so a caller can read an optimistic
/// prefix (a length word plus the first entry) in one syscall and fall
/// back only when the sysvar is shorter than that.
#[inline]
pub fn get_sysvar_prefix_at(
    sysvar_id: &Address,
    offset: u64,
    dst: &mut [u8],
) -> Result<bool, ProgramError> {
    #[cfg(target_os = "solana")]
    {
        // SAFETY: `sysvar_id` is a 32-byte address; `dst` is valid for its
        // own length; the syscall copies exactly `dst.len()` bytes or none.
        let rc = unsafe {
            crate::syscalls::sol_get_sysvar(
                sysvar_id.as_array().as_ptr(),
                dst.as_mut_ptr(),
                offset,
                dst.len() as u64,
            )
        };
        match rc {
            0 => Ok(true),
            OFFSET_LENGTH_EXCEEDS_SYSVAR => Ok(false),
            _ => Err(ProgramError::UnsupportedSysvar),
        }
    }
    #[cfg(not(target_os = "solana"))]
    {
        let _ = (sysvar_id, offset, dst);
        Ok(true)
    }
}

// ── Epoch stake (sol_get_epoch_stake, SIMD-0133) ────────────────────

/// Get the current-epoch activated stake of the vote account at `vote`.
#[inline]
pub fn get_epoch_stake(vote: &Address) -> u64 {
    #[cfg(target_os = "solana")]
    {
        // SAFETY: `vote` is a 32-byte address pointer the syscall reads.
        unsafe { crate::syscalls::sol_get_epoch_stake(vote.as_array().as_ptr()) }
    }
    #[cfg(not(target_os = "solana"))]
    {
        let _ = vote;
        0
    }
}

/// Get the cluster-wide total activated stake for the current epoch.
#[inline]
pub fn get_total_epoch_stake() -> u64 {
    #[cfg(target_os = "solana")]
    {
        // SAFETY: a null `vote_address` is the documented request for the
        // cluster total (SIMD-0133).
        unsafe { crate::syscalls::sol_get_epoch_stake(core::ptr::null()) }
    }
    #[cfg(not(target_os = "solana"))]
    {
        0
    }
}

// ── LastRestartSlot (SIMD-0047) ─────────────────────────────────────

/// LastRestartSlot sysvar address.
pub const LAST_RESTART_SLOT_ID: Address =
    crate::address!("SysvarLastRestartS1ot1111111111111111111111");

/// Read the slot of the last cluster restart (hard fork), or `0` if the
/// cluster has never been restarted.
///
/// This wraps the dedicated `sol_get_last_restart_slot` syscall
/// (SIMD-0047). Programs that must reason about whether state predates a
/// restart (oracle freshness, liveness windows) read it here instead of
/// passing the sysvar as an account.
#[inline]
pub fn get_last_restart_slot() -> Result<u64, ProgramError> {
    #[allow(unused_mut)]
    let mut slot: u64 = 0;
    #[cfg(target_os = "solana")]
    {
        // SAFETY: the syscall writes a single `u64` into the 8-byte buffer
        // `slot` points at; `slot` is a live stack local for the call.
        let rc =
            unsafe { crate::syscalls::sol_get_last_restart_slot(&mut slot as *mut u64 as *mut u8) };
        if rc != 0 {
            return Err(ProgramError::UnsupportedSysvar);
        }
    }
    Ok(slot)
}

// ── SlotHashes ──────────────────────────────────────────────────────

/// One `(slot, hash)` entry from the SlotHashes sysvar.
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub struct SlotHash {
    pub slot: u64,
    pub hash: [u8; 32],
}

/// Read the most recent `(slot, hash)` from the SlotHashes sysvar.
///
/// SlotHashes is a length-prefixed list ordered most-recent-first:
/// `u64 count` then `count` entries of `slot(u64) + hash([u8;32])`. This
/// reads the count and the first entry (48 bytes) in one `sol_get_sysvar`
/// call (110 CU) instead of materializing the 16 KiB sysvar; only when the
/// list is empty, so the sysvar is 8 bytes long and the read overruns it,
/// does a second call read the count. Returns `Ok(None)` when the list is
/// empty.
#[inline]
pub fn slot_hashes_latest() -> Result<Option<SlotHash>, ProgramError> {
    let mut prefix = [0u8; 48];
    if !get_sysvar_prefix_at(&SLOT_HASHES_ID, 0, &mut prefix)? {
        return empty_list_or_error(&SLOT_HASHES_ID);
    }
    let count = u64::from_le_bytes([
        prefix[0], prefix[1], prefix[2], prefix[3], prefix[4], prefix[5], prefix[6], prefix[7],
    ]);
    if count == 0 {
        return Ok(None);
    }
    let slot = u64::from_le_bytes([
        prefix[8], prefix[9], prefix[10], prefix[11], prefix[12], prefix[13], prefix[14],
        prefix[15],
    ]);
    let mut hash = [0u8; 32];
    hash.copy_from_slice(&prefix[16..48]);
    Ok(Some(SlotHash { slot, hash }))
}

/// The prefix read overran the sysvar: `Ok(None)` when its length word is
/// zero (an empty list), a failure otherwise.
#[inline]
fn empty_list_or_error<T>(sysvar_id: &Address) -> Result<Option<T>, ProgramError> {
    let mut count_buf = [0u8; 8];
    get_sysvar_into(sysvar_id, 0, &mut count_buf)?;
    if u64::from_le_bytes(count_buf) == 0 {
        Ok(None)
    } else {
        Err(ProgramError::UnsupportedSysvar)
    }
}

// ── StakeHistory ────────────────────────────────────────────────────

/// One epoch's stake-history entry.
#[derive(Clone, Copy, Debug, Default, PartialEq, Eq)]
pub struct StakeHistoryEntry {
    pub epoch: u64,
    pub effective: u64,
    pub activating: u64,
    pub deactivating: u64,
}

/// Read the most recent stake-history entry.
///
/// StakeHistory is a length-prefixed list ordered most-recent-first:
/// `u64 count` then entries of `epoch(u64) + effective(u64) +
/// activating(u64) + deactivating(u64)` (32 bytes each). The count and the
/// first entry are read in one `sol_get_sysvar` call; an empty history
/// (an 8-byte sysvar) falls back to a count read. Returns `Ok(None)` when
/// the history is empty.
#[inline]
pub fn stake_history_latest() -> Result<Option<StakeHistoryEntry>, ProgramError> {
    let mut prefix = [0u8; 40];
    if !get_sysvar_prefix_at(&STAKE_HISTORY_ID, 0, &mut prefix)? {
        return empty_list_or_error(&STAKE_HISTORY_ID);
    }
    let rd = |o: usize| {
        u64::from_le_bytes([
            prefix[o],
            prefix[o + 1],
            prefix[o + 2],
            prefix[o + 3],
            prefix[o + 4],
            prefix[o + 5],
            prefix[o + 6],
            prefix[o + 7],
        ])
    };
    if rd(0) == 0 {
        return Ok(None);
    }
    Ok(Some(StakeHistoryEntry {
        epoch: rd(8),
        effective: rd(16),
        activating: rd(24),
        deactivating: rd(32),
    }))
}

// ── EpochRewards (SIMD-0118) ────────────────────────────────────────

/// EpochRewards sysvar data (SIMD-0118).
///
/// Surfaces the partitioned-rewards distribution state for the current
/// epoch: how many lamports are being paid out, how far distribution has
/// progressed, and whether the rewards period is still active. Staking and
/// airdrop programs read it to gate behaviour during the distribution
/// window.
#[derive(Clone, Copy, Debug, Default, PartialEq, Eq)]
pub struct EpochRewards {
    /// First block height at which rewards distribution begins this epoch.
    pub distribution_starting_block_height: u64,
    /// Number of partitions the distribution is split across.
    pub num_partitions: u64,
    /// Blockhash of the parent of the epoch's first block.
    pub parent_blockhash: [u8; 32],
    /// Total rewards points calculated for the epoch.
    pub total_points: u128,
    /// Total rewards (lamports) calculated for the epoch.
    pub total_rewards: u64,
    /// Rewards (lamports) distributed so far this epoch.
    pub distributed_rewards: u64,
    /// Whether the rewards period (calculation + distribution) is active.
    pub active: bool,
}

/// Wire size of the bincode-serialized EpochRewards sysvar account data.
///
/// `8 + 8 + 32 + 16 + 8 + 8 + 1`. Unlike Clock/Rent/EpochSchedule (which
/// have dedicated syscalls that memcpy a `#[repr(C)]` struct), EpochRewards
/// is only reachable through `sol_get_sysvar`, which returns the sysvar
/// *account data* in bincode form: a flat little-endian field concatenation
/// with no padding. The decoder below mirrors that image byte-for-byte
/// rather than casting a `#[repr(C)]` struct (whose `u128` would force
/// 16-byte alignment and 96-byte size, reading past the 81-byte image).
const EPOCH_REWARDS_LEN: usize = 81;

#[inline]
fn decode_epoch_rewards(buf: &[u8; EPOCH_REWARDS_LEN]) -> EpochRewards {
    let rd8 = |o: usize| {
        u64::from_le_bytes([
            buf[o],
            buf[o + 1],
            buf[o + 2],
            buf[o + 3],
            buf[o + 4],
            buf[o + 5],
            buf[o + 6],
            buf[o + 7],
        ])
    };
    let mut parent_blockhash = [0u8; 32];
    parent_blockhash.copy_from_slice(&buf[16..48]);
    let mut points = [0u8; 16];
    points.copy_from_slice(&buf[48..64]);
    EpochRewards {
        distribution_starting_block_height: rd8(0),
        num_partitions: rd8(8),
        parent_blockhash,
        total_points: u128::from_le_bytes(points),
        total_rewards: rd8(64),
        distributed_rewards: rd8(72),
        active: buf[80] != 0,
    }
}

/// Read the EpochRewards sysvar (SIMD-0118).
///
/// Reads the bincode account-data image via `sol_get_sysvar` and decodes
/// it without alignment assumptions. Off-chain this returns the zeroed
/// default (`active = false`). Returns `Err(UnsupportedSysvar)` if the
/// syscall fails (e.g. the sysvar is unavailable on the cluster).
#[inline]
pub fn get_epoch_rewards() -> Result<EpochRewards, ProgramError> {
    let mut buf = [0u8; EPOCH_REWARDS_LEN];
    get_sysvar_into(&EPOCH_REWARDS_ID, 0, &mut buf)?;
    Ok(decode_epoch_rewards(&buf))
}

#[cfg(test)]
mod abi_tests {
    use super::*;

    /// Reproduce the byte image the runtime memcpy's for EpochSchedule and
    /// confirm every field reads from the offset the syscall writes. This
    /// is the runtime counterpart to the compile-time offset asserts: it
    /// proves the read side, not just the struct shape.
    #[test]
    fn epoch_schedule_reads_canonical_byte_image() {
        // Devnet/mainnet default: 432_000 slots/epoch, no warmup.
        let mut buf = [0u8; 40];
        buf[0..8].copy_from_slice(&432_000u64.to_le_bytes()); // slots_per_epoch
        buf[8..16].copy_from_slice(&432_000u64.to_le_bytes()); // leader_schedule_slot_offset
        buf[16] = 0; // warmup = false
                     // bytes 17..24 are padding
        buf[24..32].copy_from_slice(&0u64.to_le_bytes()); // first_normal_epoch
        buf[32..40].copy_from_slice(&0u64.to_le_bytes()); // first_normal_slot

        // SAFETY: `EpochSchedule` is repr(C), size 40, and `buf` is 40 bytes
        // matching the canonical wire image asserted above.
        let sched: EpochSchedule = unsafe { core::ptr::read(buf.as_ptr() as *const EpochSchedule) };
        assert_eq!(sched.slots_per_epoch, 432_000);
        assert_eq!(sched.leader_schedule_slot_offset, 432_000);
        assert!(!sched.warmup);
        assert_eq!(sched.first_normal_epoch, 0);
        assert_eq!(sched.first_normal_slot, 0);
    }

    /// The Rent sysvar image is the first 17 bytes of the repr(C) struct:
    /// the offsets the const assertions pin, and the bytes `get_rent` reads
    /// straight into the struct on chain.
    #[test]
    fn rent_image_offsets() {
        let mut image = [0u8; RENT_IMAGE_LEN];
        image[0..8].copy_from_slice(&5_080u64.to_le_bytes());
        image[8..16].copy_from_slice(&1.0f64.to_bits().to_le_bytes());
        image[16] = 50;
        let mut rent = Rent::default();
        // SAFETY: the same prefix view `get_rent` uses on chain.
        let view = unsafe {
            core::slice::from_raw_parts_mut(&mut rent as *mut Rent as *mut u8, RENT_IMAGE_LEN)
        };
        view.copy_from_slice(&image);
        assert_eq!(rent.lamports_per_byte_year, 5_080);
        assert_eq!(rent.exemption_threshold.to_bits(), 1.0f64.to_bits());
        assert_eq!(rent.burn_percent, 50);
        assert_eq!(rent.minimum_balance(25), (128 + 25) * 5_080);
    }

    /// The EpochSchedule account image packs the bool at byte 16 with the
    /// last two words at 17 and 25, unlike the padded repr(C) struct.
    #[test]
    fn epoch_schedule_decodes_canonical_image() {
        let mut image = [0u8; EPOCH_SCHEDULE_IMAGE_LEN];
        image[0..8].copy_from_slice(&432_000u64.to_le_bytes());
        image[8..16].copy_from_slice(&432_000u64.to_le_bytes());
        image[16] = 1;
        image[17..25].copy_from_slice(&14u64.to_le_bytes());
        image[25..33].copy_from_slice(&524_256u64.to_le_bytes());
        let sched = decode_epoch_schedule(&image);
        assert_eq!(sched.slots_per_epoch, 432_000);
        assert_eq!(sched.leader_schedule_slot_offset, 432_000);
        assert!(sched.warmup);
        assert_eq!(sched.first_normal_epoch, 14);
        assert_eq!(sched.first_normal_slot, 524_256);
    }

    #[test]
    fn clock_reads_canonical_byte_image() {
        let mut buf = [0u8; 40];
        buf[0..8].copy_from_slice(&123u64.to_le_bytes()); // slot
        buf[8..16].copy_from_slice(&1_600_000_000i64.to_le_bytes()); // epoch_start_timestamp
        buf[16..24].copy_from_slice(&7u64.to_le_bytes()); // epoch
        buf[24..32].copy_from_slice(&8u64.to_le_bytes()); // leader_schedule_epoch
        buf[32..40].copy_from_slice(&1_600_000_500i64.to_le_bytes()); // unix_timestamp

        // SAFETY: `Clock` is repr(C), size 40, matching this 40-byte image.
        let clock: Clock = unsafe { core::ptr::read(buf.as_ptr() as *const Clock) };
        assert_eq!(clock.slot, 123);
        assert_eq!(clock.epoch_start_timestamp, 1_600_000_000);
        assert_eq!(clock.epoch, 7);
        assert_eq!(clock.leader_schedule_epoch, 8);
        assert_eq!(clock.unix_timestamp, 1_600_000_500);
    }

    /// Build the canonical bincode image for EpochRewards and confirm the
    /// decoder reads every field from the byte offset the runtime writes.
    /// This is the read-side proof for the no-dedicated-syscall sysvar.
    #[test]
    fn epoch_rewards_decodes_canonical_byte_image() {
        let mut buf = [0u8; EPOCH_REWARDS_LEN];
        buf[0..8].copy_from_slice(&100u64.to_le_bytes()); // distribution_starting_block_height
        buf[8..16].copy_from_slice(&8u64.to_le_bytes()); // num_partitions
        buf[16..48].copy_from_slice(&[7u8; 32]); // parent_blockhash
        buf[48..64].copy_from_slice(&123_456_789u128.to_le_bytes()); // total_points
        buf[64..72].copy_from_slice(&5_000_000u64.to_le_bytes()); // total_rewards
        buf[72..80].copy_from_slice(&1_250_000u64.to_le_bytes()); // distributed_rewards
        buf[80] = 1; // active = true

        let er = decode_epoch_rewards(&buf);
        assert_eq!(er.distribution_starting_block_height, 100);
        assert_eq!(er.num_partitions, 8);
        assert_eq!(er.parent_blockhash, [7u8; 32]);
        assert_eq!(er.total_points, 123_456_789);
        assert_eq!(er.total_rewards, 5_000_000);
        assert_eq!(er.distributed_rewards, 1_250_000);
        assert!(er.active);
    }

    #[test]
    fn epoch_rewards_off_chain_is_zeroed_default() {
        // Off-chain `get_sysvar_into` is a no-op, so the getter yields the
        // zeroed default with `active = false`.
        let er = get_epoch_rewards().unwrap();
        assert_eq!(er, EpochRewards::default());
        assert!(!er.active);
    }
}

#[cfg(test)]
mod rent_tests {
    use super::*;

    /// Loader bound on serialized account data (10 MiB), the largest
    /// `data_len` any rent calculation ever sees on-chain.
    const LOADER_MAX_DATA_LEN: usize = 10_485_760;

    /// Transcription of Solana's `Rent::minimum_balance_unchecked`, including
    /// the SIMD-0194 `1.0` and legacy `2.0` integer fast paths.
    fn solana_reference_minimum_balance(data_len: usize, lpby: u64, threshold: f64) -> u64 {
        let bytes = data_len as u64;
        let integer_part = (ACCOUNT_STORAGE_OVERHEAD + bytes).saturating_mul(lpby);
        if threshold == 1.0 {
            integer_part
        } else if threshold == 2.0 {
            integer_part.saturating_mul(2)
        } else {
            (integer_part as f64 * threshold) as u64
        }
    }

    fn rent_with(lpby: u64, threshold: f64) -> Rent {
        Rent {
            lamports_per_byte_year: lpby,
            exemption_threshold: threshold,
            burn_percent: 0,
        }
    }

    /// The const fast-path must not overflow or panic at the data-length
    /// extremes the loader permits (0 and 10 MiB).
    #[test]
    fn const_rent_exempt_minimum_no_overflow_at_extremes() {
        assert_eq!(
            rent_exempt_minimum(0),
            ACCOUNT_STORAGE_OVERHEAD * LAMPORTS_PER_BYTE_YEAR * EXEMPTION_THRESHOLD_YEARS
        );
        let max = rent_exempt_minimum(LOADER_MAX_DATA_LEN);
        let expected = (LOADER_MAX_DATA_LEN as u64 + ACCOUNT_STORAGE_OVERHEAD)
            * LAMPORTS_PER_BYTE_YEAR
            * EXEMPTION_THRESHOLD_YEARS;
        assert_eq!(max, expected);
        // Sanity: comfortably inside u64.
        assert!(max < u64::MAX / 2);
    }

    /// The sysvar path must not overflow or panic even with a wildly
    /// repriced `lamports_per_byte_year` at the maximum data length: the
    /// saturating integer product keeps the arithmetic safe.
    #[test]
    fn sysvar_minimum_balance_no_overflow_at_extremes() {
        // Far past any realistic rate.
        let rent = rent_with(1u64 << 40, 2.0);
        let _ = rent.minimum_balance(LOADER_MAX_DATA_LEN);
        // data_len = 0 lower extreme.
        assert_eq!(
            rent.minimum_balance(0),
            solana_reference_minimum_balance(0, 1u64 << 40, 2.0)
        );
    }

    /// The const path and sysvar path agree at the launch-era snapshot.
    #[test]
    fn const_and_sysvar_agree_at_launch_snapshot() {
        let rent = rent_with(LAMPORTS_PER_BYTE_YEAR, EXEMPTION_THRESHOLD_YEARS as f64);
        for &dl in &[
            0usize,
            1,
            127,
            128,
            1024,
            10_240,
            1_000_000,
            LOADER_MAX_DATA_LEN,
        ] {
            assert_eq!(
                rent_exempt_minimum(dl),
                rent.minimum_balance(dl),
                "const vs sysvar mismatch at data_len={dl}"
            );
        }
    }

    /// The sysvar path must byte-match Solana's runtime formula across a
    /// range of data sizes, repriced per-byte costs, and fractional
    /// thresholds, including a `lamports_per_byte_year` past f64's 53-bit
    /// exact-integer range, where the old all-f64 form could drift.
    #[test]
    fn sysvar_minimum_balance_byte_matches_solana_reference() {
        let cases: &[(usize, u64, f64)] = &[
            (0, 6_333, 1.0),
            (167_829, 6_333, 1.0),
            (0, 3_480, 2.0),
            (165, 3_480, 2.0),
            (10_240, 3_480, 2.0),
            (1_000_000, 6_960, 2.0),  // hypothetical 2x reprice
            (500_000, 3_480, 3.0),    // whole-year non-default threshold
            (10_485_760, 3_480, 2.0), // max size
            // `lpby` just past f64's 2^53 exact-integer range, the case
            // that motivates the integer product + single f64 step (an
            // all-f64 formula would lose a lamport here). `data_len` is
            // kept small so the *integer* product stays inside u64: at
            // this `lpby`, (overhead + data_len) must be < ~2044 or the
            // product overflows u64 entirely (a regime Solana itself
            // never reaches, `lpby` is a fixed cluster constant).
            (1_024, 9_007_199_254_740_993, 2.0),
        ];
        for &(dl, lpby, threshold) in cases {
            let rent = rent_with(lpby, threshold);
            assert_eq!(
                rent.minimum_balance(dl),
                solana_reference_minimum_balance(dl, lpby, threshold),
                "sysvar minimum_balance != Solana reference at dl={dl}, lpby={lpby}, threshold={threshold}"
            );
        }
    }

    /// The float-free threshold scaling: exact for the two thresholds any
    /// cluster has stored, and for every other finite positive threshold a
    /// whole-year round-up that is never below the float cast the runtime
    /// historically used.
    #[test]
    fn saturating_mul_u64_matches_the_library_operator() {
        let samples = [
            0u64,
            1,
            2,
            3,
            128,
            153,
            3_480,
            5_080,
            6_333,
            10_485_888,
            u32::MAX as u64,
            u32::MAX as u64 + 1,
            1 << 40,
            u64::MAX / 3,
            u64::MAX / 2,
            u64::MAX / 2 + 1,
            u64::MAX - 1,
            u64::MAX,
        ];
        for &a in &samples {
            for &b in &samples {
                assert_eq!(saturating_mul_u64(a, b), a.saturating_mul(b), "{a} * {b}");
            }
        }
    }

    #[test]
    fn threshold_scaling_is_float_free_and_never_underfunds() {
        fn reference(integer_part: u64, threshold: f64) -> u64 {
            (integer_part as f64 * threshold) as u64
        }
        let amounts: [u64; 8] = [
            0,
            1,
            7,
            128 * 3_480,
            890_880,
            1_740_445_440,
            1 << 40,
            1 << 52,
        ];
        let whole_thresholds: [f64; 4] = [1.0, 2.0, 3.0, 4.0];
        let fractional: [(f64, u64); 10] = [
            (0.5, 1),
            (1.5, 2),
            (2.5, 3),
            (0.25, 1),
            (0.75, 1),
            (1.1, 2),
            (1.7, 2),
            (0.3, 1),
            (2.9, 3),
            (3.33, 4),
        ];
        for &amount in &amounts {
            for &threshold in &whole_thresholds {
                assert_eq!(
                    scale_by_exemption_threshold(amount, threshold.to_bits()),
                    reference(amount, threshold),
                    "amount {amount} threshold {threshold}"
                );
            }
            for &(threshold, years) in &fractional {
                let ours = scale_by_exemption_threshold(amount, threshold.to_bits());
                assert_eq!(ours, amount.saturating_mul(years), "threshold {threshold}");
                assert!(
                    ours >= reference(amount, threshold),
                    "amount {amount} threshold {threshold}: {ours} underfunds"
                );
            }
            // Degenerate thresholds: zero, negative, and NaN yield 0 like the
            // cast; a subnormal rounds up to one year; infinity saturates.
            assert_eq!(scale_by_exemption_threshold(amount, 0.0f64.to_bits()), 0);
            assert_eq!(scale_by_exemption_threshold(amount, (-1.0f64).to_bits()), 0);
            assert_eq!(scale_by_exemption_threshold(amount, f64::NAN.to_bits()), 0);
            assert_eq!(
                scale_by_exemption_threshold(amount, f64::MIN_POSITIVE.to_bits() >> 1),
                amount
            );
            let saturated = if amount == 0 { 0 } else { u64::MAX };
            assert_eq!(
                scale_by_exemption_threshold(amount, f64::INFINITY.to_bits()),
                saturated
            );
        }
        // Huge thresholds saturate.
        let huge: f64 = (1u64 << 63) as f64;
        assert_eq!(scale_by_exemption_threshold(2, huge.to_bits()), u64::MAX);
        let astronomical: f64 = 1e300;
        assert_eq!(
            scale_by_exemption_threshold(1, astronomical.to_bits()),
            u64::MAX
        );
        let exactly_2_pow_60: f64 = (1u64 << 60) as f64;
        assert_eq!(
            scale_by_exemption_threshold(1, exactly_2_pow_60.to_bits()),
            1 << 60
        );
        assert_eq!(
            scale_by_exemption_threshold(u64::MAX, 1.0f64.to_bits()),
            u64::MAX
        );
        assert_eq!(
            scale_by_exemption_threshold(u64::MAX, 2.0f64.to_bits()),
            u64::MAX
        );
    }

    /// The correctness gap the safety work closes: after an UPWARD rent
    /// reprice the live sysvar demands strictly more than the const path,
    /// so gating reaping on the const would under-fund.
    #[test]
    fn repriced_sysvar_exceeds_const_underestimate() {
        let dl = 4_096;
        let const_min = rent_exempt_minimum(dl);
        // Cluster doubled the per-byte cost.
        let repriced = rent_with(LAMPORTS_PER_BYTE_YEAR * 2, EXEMPTION_THRESHOLD_YEARS as f64);
        let sysvar_min = repriced.minimum_balance(dl);
        assert!(
            sysvar_min > const_min,
            "expected repriced sysvar minimum ({sysvar_min}) > const minimum ({const_min})"
        );
        assert_eq!(sysvar_min, const_min * 2);
    }
}

// =====================================================================
// Kani proof harnesses for the rent arithmetic.
// =====================================================================
//
// These mirror the existing native Kani conventions (see
// `raw_input.rs::kani_proofs`): a `#[cfg(kani)]` module of `#[kani::proof]`
// harnesses over symbolic inputs bounded by the loader's limits, run by
// `cargo kani -p hopper-native`. They discharge the three safety claims the
// SAFETY-RENT work rests on:
//
//   (1) the const fast path cannot overflow for any loader-permitted
//       `data_len`;
//   (2) the sysvar path's integer product cannot overflow for any
//       loader-permitted `data_len` and any realistic (repriced)
//       `lamports_per_byte_year`, and its saturating ops never actually
//       saturate in that range (so the byte-match with the runtime is
//       exact); and
//   (3) the const and sysvar forms AGREE at the launch-era snapshot.
#[cfg(kani)]
mod kani_rent_proofs {
    use super::*;

    /// Loader bound on serialized account data (10 MiB).
    const LOADER_MAX_DATA_LEN: usize = 10_485_760;

    /// Generous upper bound on a repriced `lamports_per_byte_year`: 2^40 is
    /// ~1.1e12 and far past any realistic rent change,
    /// yet the integer product still provably cannot overflow u64.
    const MAX_LAMPORTS_PER_BYTE_YEAR: u64 = 1 << 40;

    /// The const path's integer arithmetic never overflows for any
    /// loader-permitted `data_len`, and the function returns exactly the
    /// checked value.
    #[kani::proof]
    fn const_rent_exempt_minimum_never_overflows() {
        let data_len: usize = kani::any();
        kani::assume(data_len <= LOADER_MAX_DATA_LEN);

        // Each `checked_*` doubles as the no-overflow proof for the `*`/`+`
        // in `rent_exempt_minimum`.
        let sum = (data_len as u64)
            .checked_add(ACCOUNT_STORAGE_OVERHEAD)
            .unwrap();
        let per_year = sum.checked_mul(LAMPORTS_PER_BYTE_YEAR).unwrap();
        let total = per_year.checked_mul(EXEMPTION_THRESHOLD_YEARS).unwrap();

        assert_eq!(rent_exempt_minimum(data_len), total);
    }

    /// The sysvar path's integer product never overflows for any
    /// loader-permitted `data_len` and any realistic `lamports_per_byte_year`,
    /// and its saturating ops equal the checked ops (never saturate) in that
    /// range.
    #[kani::proof]
    fn sysvar_minimum_balance_integer_part_never_overflows() {
        let data_len: usize = kani::any();
        let lpby: u64 = kani::any();
        kani::assume(data_len <= LOADER_MAX_DATA_LEN);
        kani::assume(lpby <= MAX_LAMPORTS_PER_BYTE_YEAR);

        let bytes = data_len as u64;
        let checked = ACCOUNT_STORAGE_OVERHEAD
            .checked_add(bytes)
            .and_then(|s| s.checked_mul(lpby));
        assert!(checked.is_some());

        let saturating = ACCOUNT_STORAGE_OVERHEAD
            .saturating_add(bytes)
            .saturating_mul(lpby);
        assert_eq!(saturating, checked.unwrap());
    }

    /// Const and sysvar forms agree at the launch-era snapshot.
    #[kani::proof]
    fn const_and_sysvar_agree_at_launch_snapshot() {
        let data_len: usize = kani::any();
        kani::assume(data_len <= LOADER_MAX_DATA_LEN);

        let rent = Rent {
            lamports_per_byte_year: LAMPORTS_PER_BYTE_YEAR,
            exemption_threshold: EXEMPTION_THRESHOLD_YEARS as f64,
            burn_percent: 0,
        };

        assert_eq!(
            rent_exempt_minimum(data_len),
            rent.minimum_balance(data_len)
        );
    }
}