//! Safety property tests for the unified-userspace VM.
//!
//! The load-bearing property of the new design: **`evaluate` never panics
//! on arbitrary inputs**. Every bytecode + userspace + inputs combination
//! either returns `Ok(EvalResult)` or `Err(RuntimeError)`. No panics, no
//! UB. This is the contract that lets us run untrusted MM-supplied
//! bytecode safely.

use proptest::prelude::*;

use quay_vm::vm::{evaluate, Inputs, TxContext};

proptest! {
    #![proptest_config(ProptestConfig::with_cases(1024))]

    /// Arbitrary bytecode + arbitrary userspace + arbitrary inputs. Verify
    /// no panic in any combination. Catches OOB reads, missed bounds
    /// checks, and any other invariant slip-up.
    #[test]
    fn evaluate_never_panics(
        bytecode in prop::collection::vec(any::<u8>(), 0..256),
        userspace_init in prop::collection::vec(any::<u8>(), 0..512),
        quotes in prop::collection::vec(any::<i32>(), 0..241),
        size in any::<u64>(),
        side in prop::sample::select(vec![0u8, 1]),
        current_slot in any::<u64>(),
        inventory_base in any::<u64>(),
        inventory_quote in any::<u64>(),
        current_unix_sec in any::<u64>(),
        base_decimals in any::<u8>(),
        quote_decimals in any::<u8>(),
        quotes_timestamp_ns in any::<u64>(),
        last_update_slot in any::<u64>(),
        ix_depth in any::<u8>(),
        tx_flags in any::<u64>(),
        entrypoint_program in any::<[u8; 32]>(),
        signers in prop::collection::vec(any::<[u8; 32]>(), 0..4),
    ) {
        let mut userspace = userspace_init;
        let inputs = Inputs {
            quotes: &quotes,
            userspace: &mut userspace,
            size, side,
            current_slot,
            inventory_base, inventory_quote,
            current_unix_sec,
            base_decimals, quote_decimals,
            quotes_timestamp_ns,
            last_update_slot,
            tx: TxContext {
                ix_depth,
                tx_flags,
                entrypoint_program,
                signers: &signers,
            },
        };
        // The point: `evaluate` returns a Result. We never panic. Either
        // arm is fine for this property.
        let _ = evaluate(&bytecode, inputs);
    }
}
