The interpreter, in full

//! The admitted instruction subset.
//!
//! Encoding: eBPF / RFC 9669, because it is documented and has existing
//! assembler and compiler tooling. Semantics: ours, normatively. Stock
//! `clang -target bpf` output is not generally admissible: LLVM's BPF target
//! is 64-bit, while this VM deliberately rejects most 64-bit operations and
//! other parts of the full ISA. A restricted source/compiler contract remains
//! product work; the loader fails closed on output outside this subset.
//!
//! ## The admission rule
//!
//! > A construct is admitted only if its semantics can be stated in one line
//! > a reviewer checks by reading, and discharged by Kani as a property of
//! > this implementation.
//!
//! Everything failing that is **deleted from the subset rather than
//! defended**. We control the whole pipeline, so ambiguity can be made
//! unreachable instead of mitigated. What that costs, and why each is worth
//! it:
//!
//! | Deleted | Because |
//! |---|---|
//! | `div`, `mod` | divide-by-zero has three different answers across eBPF, C and RV32 |
//! | signed compares | bias into unsigned at the trust boundary instead |
//! | 64-bit values | the CVE-2021-3490 shape |
//! | `lddw`, `callx` | a computed call index defeats capability confinement |
//! | atomics | single-threaded machine |
//!
//! Backward jumps are admitted in the default policy because fuel bounds every
//! execution. Callers that need a program-length WCET bound can select the
//! optional `ForwardOnly` loader policy, which rejects them.

/// An eBPF instruction is 64 bits: opcode, dst/src nibbles, offset, imm.
#[derive(Clone, Copy, PartialEq, Eq)]
pub struct Insn {
    pub opcode: u8,
    /// Destination register, low nibble of the register byte.
    pub dst: u8,
    /// Source register, high nibble.
    pub src: u8,
    pub off: i16,
    pub imm: i32,
}

/// Registers. eBPF defines r0..r10; r10 is the read-only frame pointer.
pub const N_REGS: usize = 11;
/// The frame pointer register index.
pub const REG_FP: u8 = 10;

/// Instruction classes we admit, from the low three bits of the opcode.
pub const CLASS_LD: u8 = 0x00;
pub const CLASS_LDX: u8 = 0x01;
pub const CLASS_ST: u8 = 0x02;
pub const CLASS_STX: u8 = 0x03;
pub const CLASS_ALU: u8 = 0x04;
pub const CLASS_JMP: u8 = 0x05;
pub const CLASS_ALU64: u8 = 0x07;

/// ALU operations, from the top nibble.
pub const ALU_ADD: u8 = 0x00;
pub const ALU_SUB: u8 = 0x10;
pub const ALU_MUL: u8 = 0x20;
pub const ALU_OR: u8 = 0x40;
pub const ALU_AND: u8 = 0x50;
pub const ALU_LSH: u8 = 0x60;
pub const ALU_RSH: u8 = 0x70;
pub const ALU_NEG: u8 = 0x80;
pub const ALU_XOR: u8 = 0xa0;
pub const ALU_MOV: u8 = 0xb0;
pub const ALU_ARSH: u8 = 0xc0;

/// Jump operations. Unsigned only — signed compares are deleted, so a program
/// that wants a signed comparison must bias into unsigned before the trust
/// boundary, where the bias is visible and checkable.
pub const JMP_JA: u8 = 0x00;
pub const JMP_JEQ: u8 = 0x10;
pub const JMP_JGT: u8 = 0x20;
pub const JMP_JGE: u8 = 0x30;
pub const JMP_JSET: u8 = 0x40;
pub const JMP_JNE: u8 = 0x50;
pub const JMP_JLT: u8 = 0xa0;
pub const JMP_JLE: u8 = 0xb0;
pub const JMP_CALL: u8 = 0x80;
pub const JMP_EXIT: u8 = 0x90;

/// Source modifier: operand is the immediate (0) or a register (1).
pub const SRC_IMM: u8 = 0x00;
pub const SRC_REG: u8 = 0x08;

/// Memory access widths. 64-bit (`DW`) is absent by design.
pub const SIZE_W: u8 = 0x00;
pub const SIZE_H: u8 = 0x08;
pub const SIZE_B: u8 = 0x10;

/// Is this opcode in the admitted subset?
///
/// The whitelist is positive: an opcode is rejected unless it appears here.
/// A negative list would silently admit anything a future encoding adds.
pub const fn admitted(opcode: u8) -> bool {
    let class = opcode & 0x07;
    let op = opcode & 0xf0;
    let src = opcode & 0x08;
    match class {
        // 32-bit ALU only. CLASS_ALU64 is rejected wholesale: the subset is
        // 32-bit-valued, so a 64-bit operation has no meaning here.
        CLASS_ALU => matches!(
            op,
            ALU_ADD
                | ALU_SUB
                | ALU_MUL
                | ALU_OR
                | ALU_AND
                | ALU_LSH
                | ALU_RSH
                | ALU_NEG
                | ALU_XOR
                | ALU_MOV
                | ALU_ARSH
        ),
        CLASS_JMP => match op {
            JMP_JA => src == SRC_IMM,
            JMP_JEQ | JMP_JGT | JMP_JGE | JMP_JSET | JMP_JNE | JMP_JLT | JMP_JLE => true,
            // A call is admitted; the *target* is checked at load time against
            // the capability table and cannot be computed at run time.
            JMP_CALL => src == SRC_IMM,
            JMP_EXIT => true,
            _ => false,
        },
        CLASS_LDX | CLASS_ST | CLASS_STX => {
            matches!(opcode & 0x18, SIZE_W | SIZE_H | SIZE_B)
        }
        // CLASS_LD carries only `lddw` in practice, which is deleted.
        _ => false,
    }
}

/// Does this opcode transfer control backwards or out of line?
#[inline]
pub fn is_jump(opcode: u8) -> bool {
    opcode & 0x07 == CLASS_JMP
}

//! Load-time validation.
//!
//! The loader is **safety-critical software in its own right.** FAA Order
//! 8110.49 §7-6 is explicit that a tool which writes the modifiable region
//! must itself be qualified, and that its protective component carries the
//! system's highest assurance level. That cost is not currently in the
//! budget; recording it here is the first step to putting it there.
//!
//! Everything this establishes is a **syntactic property of the image**,
//! decided before the machine moves. Nothing here depends on the program's
//! behaviour, which is why it can be decided at all.

use crate::isa::*;
use crate::{MAX_INSNS, N_CAPS};

/// Why an image was rejected.
#[derive(Clone, Copy, PartialEq, Eq, Debug)]
pub enum Reject {
    Empty,
    TooLong {
        len: usize,
    },
    IllegalOpcode {
        at: usize,
    },
    /// A jump that does not move strictly forwards. Only reachable under
    /// [`Strictness::ForwardOnly`]; loops are admitted by default because
    /// fuel already bounds them.
    BackwardJump {
        at: usize,
        off: i16,
    },
    JumpOutOfRange {
        at: usize,
    },
    BadRegister {
        at: usize,
    },
    BadCapIndex {
        at: usize,
        idx: i32,
    },
    /// The last instruction must be `exit`, so falling off the end is
    /// impossible rather than merely unlikely.
    NoTrailingExit,
    /// Conservative sum of all forward-only instruction charges exceeds the
    /// target-specific allowance supplied by the scheduler.
    TickBudgetExceeded {
        required: u64,
        available: u32,
    },
}

/// A forward-only program admitted against one concrete timing model.
#[derive(Clone, Copy, PartialEq, Eq, Debug)]
pub struct Admission {
    pub instructions: u32,
    pub required_credits: u32,
    pub cost_model_version: u32,
}

impl Admission {
    /// The smallest budget that is sufficient under the admitted model.
    pub const fn execution_budget(self) -> crate::ExecutionBudget {
        crate::ExecutionBudget::new(
            crate::StepFuel::new(self.instructions),
            crate::TickCredits::new(self.required_credits),
        )
    }
}

/// Validate an image. Returns the **termination** bound, which is not the
/// same kind of number as target-specific tick credits.
///
/// How strictly to validate.
#[derive(Clone, Copy, PartialEq, Eq, Debug)]
pub enum Strictness {
    /// Loops admitted. Termination comes from fuel, which is what fuel is
    /// for. The dispatch loop stays bounded — by the fuel cap, which is
    /// *tighter* than the program length.
    Default,
    /// Reject backward jumps. Buys one thing: worst-case execution time is
    /// the program's own length rather than the fuel cap, so a short program
    /// can be budgeted as short. Costs loops entirely, and unrolling a
    /// six-element loop can eat 20-50% of the instruction budget.
    ForwardOnly,
}

/// What validation establishes about how long a program can run.
///
/// The two cases are genuinely different kinds of number, and conflating them
/// is the footgun this type exists to prevent: under [`Strictness::ForwardOnly`]
/// the program provably finishes in a bounded number of steps *derived from the
/// program*; under [`Strictness::Default`] loops are admitted, so there is no
/// such syntactic bound and the fuel cap is the only limit. A caller that wants
/// a dispatch bound must ask for it explicitly via
/// [`Termination::step_fuel`],
/// which makes the constant-vs-derived choice visible at the call site rather
/// than hidden behind a bare `u32`.
#[derive(Clone, Copy, PartialEq, Eq, Debug)]
pub enum Termination {
    /// Forward-only: no instruction executes twice, so the program finishes in
    /// at most this many steps.
    Length(u32),
    /// Loops admitted: termination rests on fuel, not on the program's shape.
    FuelBounded,
}

impl Termination {
    /// Platform-independent dispatch bound: the derived length when that is a
    /// real bound, otherwise the global proof ceiling. Tick credits must be
    /// supplied separately by the scheduler.
    #[inline]
    pub fn step_fuel(self) -> crate::StepFuel {
        match self {
            Termination::Length(n) => crate::StepFuel::new(n),
            Termination::FuelBounded => crate::StepFuel::new(crate::MAX_STEP_FUEL),
        }
    }
}

/// Validate an image at the default strictness.
pub fn validate(insns: &[Insn]) -> Result<Termination, Reject> {
    validate_with(insns, Strictness::Default)
}

/// Admit a program for completion within one modelled control-tick allowance.
///
/// This deliberately requires [`Strictness::ForwardOnly`]. With no repeated
/// instruction, summing every instruction in the image is conservative even
/// across conditional paths (it may count mutually exclusive paths, but never
/// under-counts an executed path). Looping programs retain safe termination
/// through step fuel, but do not receive a completion-within-tick admission.
pub fn validate_for_tick(
    insns: &[Insn],
    costs: &crate::CostModel,
    available: crate::TickCredits,
) -> Result<Admission, Reject> {
    validate_with(insns, Strictness::ForwardOnly)?;
    let mut required = costs.run_overhead() as u64;
    for insn in insns {
        required += costs.charge(insn) as u64;
    }
    if required > available.get() as u64 {
        return Err(Reject::TickBudgetExceeded {
            required,
            available: available.get(),
        });
    }
    Ok(Admission {
        instructions: insns.len() as u32,
        required_credits: required as u32,
        cost_model_version: costs.version,
    })
}

/// Validate an image.
///
/// Returns a [`Termination`], not a bare number, because the two strictness
/// modes establish different kinds of bound. Under [`Strictness::ForwardOnly`]
/// it is `Length`, the program's own length, since no instruction executes
/// twice. Otherwise it is `FuelBounded`: a looping program's step count is not
/// a property of its length, and the fuel cap is the only bound.
pub fn validate_with(insns: &[Insn], strict: Strictness) -> Result<Termination, Reject> {
    if insns.is_empty() {
        return Err(Reject::Empty);
    }
    if insns.len() > MAX_INSNS {
        return Err(Reject::TooLong { len: insns.len() });
    }

    for (at, i) in insns.iter().enumerate() {
        if !admitted(i.opcode) {
            return Err(Reject::IllegalOpcode { at });
        }
        if i.dst as usize >= N_REGS || i.src as usize >= N_REGS {
            return Err(Reject::BadRegister { at });
        }

        if is_jump(i.opcode) {
            let op = i.opcode & 0xf0;
            match op {
                JMP_EXIT => {}
                JMP_CALL => {
                    // The capability index is an immediate and is checked
                    // here. Because `callx` is not in the subset, the program
                    // cannot compute an index, so the reachable effect set is
                    // fixed by this loop.
                    if i.imm < 0 || i.imm as usize >= N_CAPS {
                        return Err(Reject::BadCapIndex { at, idx: i.imm });
                    }
                }
                _ => {
                    if strict == Strictness::ForwardOnly && i.off <= 0 {
                        return Err(Reject::BackwardJump { at, off: i.off });
                    }
                    // The target must land inside the image either way. This
                    // is the check that keeps the pc in range; the direction
                    // is a separate question.
                    let target = (at as i64) + 1 + (i.off as i64);
                    if target < 0 || target >= insns.len() as i64 {
                        return Err(Reject::JumpOutOfRange { at });
                    }
                }
            }
        }
    }

    // Falling off the end would reach `PcOutOfRange`, which is safe but
    // uninformative. Requiring a trailing `exit` makes the program's
    // termination visible in the image rather than inferred from a halt.
    let last = insns[insns.len() - 1];
    if last.opcode & 0x07 != CLASS_JMP || last.opcode & 0xf0 != JMP_EXIT {
        return Err(Reject::NoTrailingExit);
    }

    // Under ForwardOnly no instruction executes twice, so the program cannot
    // take more steps than it has instructions. With loops admitted there is
    // no such bound and termination rests on fuel — `MAX_STEP_FUEL`, the number of
    // instructions a run may execute, which is what a program actually gets.
    Ok(match strict {
        Strictness::ForwardOnly => Termination::Length(insns.len() as u32),
        Strictness::Default => Termination::FuelBounded,
    })
}

//! Target-specific, versioned timing-credit tables.
//!
//! These constants do not turn observed cycle counts into WCET. They are kept
//! separate from the platform-independent VM semantics so their provenance and
//! maturity are visible at every use site.

use crate::CostModel;

/// Deployed-board admission model, version 2026-09-28.01.
///
/// Ordinary-class entries unchanged from the initial no-cache NEORV32 RTL
/// characterization (`evidence/simulation/2026-08-27-neorv32-rtl-fuel-costs-02`;
/// each value an observed class maximum × 1.25 rounded up to 16 cycles) —
/// the 2026-09-27 board rail (`evidence/runs/2026-09-27-ecp5-j4-001/`)
/// confirmed they hold on silicon (71.5–79.4% utilization, board within
/// 0.2–3.6% of the RTL model).
///
/// **Capability entries replaced with deployed-callee measurements**, as the
/// v1 doc below required: the stub entries under-charged the deployed
/// propose by 14.76× and the deployed seal by 57.9×. Sources
/// `evidence/runs/2026-09-27-ecp5-j4-001/` (propose 13,621 cycles/call through
/// the real monitor; sense 1,018) and the 2026-09-28 seal leg
/// (Ed25519 sign, 12,262,800 cycles/call). Same derivation convention:
/// observed maximum × 1.25, rounded up to 16 cycles.
///
/// Still provisional engineering characterization, not WCET; the seal entry
/// bounds one sign of a 32-byte message with the default-features crate
/// configuration (no precomputed basepoint table).
pub const PROVISIONAL_NEORV32_RTL_V1: CostModel = CostModel::new(
    2_026_092_801,
    416,             // fixed Vm::run overhead
    368,             // non-multiply ALU
    352,             // multiply
    [336, 368, 432], // load: byte, half, word
    [320, 368, 400], // store: byte, half, word
    448,             // branch/jump
    [1_280, 17_040, 15_328_512], // sense, propose, seal: deployed-callee bounds
    448,             // exit: conservative ordinary-class maximum, not isolated
    480,             // invalid path: conservative measured-class maximum
);

/// The v1 table as first characterized, retained for the record: its
/// capability entries were harness stubs, and the 2026-09-27 board rail
/// measured them 14.76x (propose) and 57.9x (seal) below the deployed
/// path. Superseded by the entries in `PROVISIONAL_NEORV32_RTL_V1` above;
/// kept so the finding stays reproducible against the table that exhibited it.
pub const PROVISIONAL_NEORV32_RTL_V0_STUB_CALLS: CostModel = CostModel::new(
    2_026_082_701,
    416,
    368,
    352,
    [336, 368, 432],
    [320, 368, 400],
    448,
    [480, 464, 480], // harness-stub call entries, superseded
    448,
    480,
);

//! # Endstop VM
//!
//! An interpreter for the admitted eBPF subset.
//!
//! Written rather than inherited. An earlier design took a published,
//! formally verified eBPF VM and dropped it: the proof covered a much larger
//! machine than this one executes, and it stopped at C rather than at machine
//! code.
//!
//! This is **not** the safety function. The envelope monitor is
//! (`endstop-monitor`), and under IEC 61508's limited/full-variability split
//! that distinction is what lets the program this executes be arbitrary code.
//! What the VM owes is narrower: that an untrusted program cannot escape its
//! memory, cannot fail to terminate, and cannot reach an effect outside the
//! capability table.
//!
//! ## Why this is verifiable at all
//!
//! **Step fuel bounds the dispatch loop**, and it is capped at
//! [`MAX_STEP_FUEL`], so
//! the trip count is a compile-time constant no matter what the program's
//! control flow does. The plan's objection — *"Kani cannot prove an
//! interpreter's dispatch loop safe for all executions"* — is about an
//! *unbounded* loop. A fuel-capped one is bounded by construction.
//!
//! An earlier draft claimed it was the deletion of backward jumps that made
//! this tractable. That was wrong twice over. The fuel cap is a *tighter*
//! bound than the program length would be, and more fundamentally **we are
//! not proving the program — we are proving this interpreter.** What shape
//! the untrusted program's control-flow graph has is its business; that we
//! handle any shape safely is ours. Loops are admitted.
//!
//! ## Status
//!
//! All seven properties discharged by bounded model checking (Kani): single-step
//! memory safety (V1), capability-index confinement (V2), jump-target containment
//! (V3), forward-only rejection (V3b), checked memory access (V4), and termination
//! under fuel (V5), plus precharge-before-capability ordering (V6). Each harness
//! in `proofs.rs` states its `unwind` bound. Those
//! bounds are shallow by design: the properties are structural, not depth-
//! sensitive -- V1 quantifies over a fully symbolic instruction from the VM's
//! concrete reset state, and the dispatch
//! loop is bounded by the fuel cap regardless of program length. The argument for
//! why shallow suffices is in the `proofs.rs` header.

#![cfg_attr(not(test), no_std)]
#![forbid(unsafe_code)]

pub mod costs;
pub mod isa;
pub mod loader;

#[cfg(kani)]
mod proofs;

#[cfg(test)]
mod tests;

/// Panic handler for the bare-metal artifact. Spinning is fail-closed: the
/// watchdog stops being fed, the deadman expires, and drive power is cut.
// Only for the bare-metal target. A host build links std, which brings
// its own handler, and two would be a duplicate lang item — which is how
// this was found: the plant crate depends on the monitor.
#[cfg(all(not(test), not(kani), target_os = "none"))]
#[panic_handler]
fn panic(_info: &core::panic::PanicInfo) -> ! {
    loop {
        core::hint::spin_loop();
    }
}

use isa::*;

/// Scratch memory available to a program, in bytes. Fixed at build time so
/// the bound is a constant the checker can use.
pub const MEM_LEN: usize = 512;
/// Maximum program length.
pub const MAX_INSNS: usize = 512;
/// Step fuel: the **ceiling** on how many instructions one run may execute, and
/// therefore the dispatch loop's bound.
///
/// This is what bounds the loop — not the program length. [`StepFuel::new`]
/// clamps the caller's request to this value, so the trip count is a
/// compile-time constant no matter what a caller supplies. The proofs use
/// smaller values and are independent of the constant's particular value.
///
/// **A ceiling is not a tick's allowance, and the two must not be conflated.**
/// The operating budget is whatever the caller hands to `run` beneath this
/// number, and callers differ on purpose:
///
/// - The red-team board hands out the full 1024, deliberately generous so an
///   attacker has room to build something sophisticated rather than being cut
///   short. A range that starves its attackers proves nothing.
/// - A real control tick also supplies target-specific [`TickCredits`]. The
///   interpreter reserves the complete instruction charge before execution.
///   The initial table is provisional NEORV32 RTL characterization; production
///   admission remains disabled until deployed capability paths are bounded
///   and an independent privileged deadline mechanism is integrated.
///
/// Historical instructions-per-period divisions are not admission limits:
/// instruction mix, capability implementations and shared monitor work all
/// affect the actual cycle budget.
pub const MAX_STEP_FUEL: u32 = 1024;
/// Capability slots. Three: read state, propose setpoint, request signature.
pub const N_CAPS: usize = 3;

/// Why execution stopped.
///
/// Every reason is a first-class outcome rather than an error code, because
/// the evidence record stores refusals with the same fidelity as permissions
/// and a refusal is the differentiated half of the product.
#[derive(Clone, Copy, PartialEq, Eq, Debug)]
pub enum Halt {
    /// `exit` reached. `r0` carries the program's result.
    Exit(u32),
    StepFuelExhausted,
    /// The target-specific conservative execution-credit budget could not pay
    /// for the next instruction. The instruction was not executed.
    TickCreditsExhausted,
    PcOutOfRange,
    IllegalOpcode,
    MemBounds,
    BadCapIndex,
    /// A write to the frame pointer, which is read-only.
    WriteToFp,
    /// A shift by 32 or more. Deleted rather than defined: C says undefined,
    /// RV32 says mask to 5 bits, eBPF says mask. One line is not available.
    ShiftOutOfRange,
}

/// What a capability call may do. The VM never performs an effect itself; it
/// hands an index and arguments to the trusted side, which constructs the
/// effect canonically. The program cannot compute the index — `callx` is not
/// in the subset — so the set of reachable effects is fixed at load time.
pub trait Caps {
    /// Invoke capability `idx` with the eBPF argument registers r1..r5.
    fn call(&mut self, idx: u32, args: [u32; 5]) -> u32;
}

/// Platform-independent bound on dispatched instructions.
///
/// Construction clamps the value to [`MAX_STEP_FUEL`], preserving the static
/// dispatch-loop bound even when a caller supplies an untrusted number.
#[derive(Clone, Copy, PartialEq, Eq, Debug)]
pub struct StepFuel(u32);

impl StepFuel {
    pub const fn new(steps: u32) -> Self {
        Self(if steps > MAX_STEP_FUEL {
            MAX_STEP_FUEL
        } else {
            steps
        })
    }

    pub const fn get(self) -> u32 {
        self.0
    }
}

/// Target-specific conservative work allowance. Credits are deliberately a
/// different type from [`StepFuel`]: a proof ceiling must not be passed where
/// a control-tick timing allowance is required.
#[derive(Clone, Copy, PartialEq, Eq, Debug)]
pub struct TickCredits(u32);

impl TickCredits {
    pub const fn new(credits: u32) -> Self {
        Self(credits)
    }

    pub const fn get(self) -> u32 {
        self.0
    }
}

/// Both independent limits required for one invocation.
#[derive(Clone, Copy, PartialEq, Eq, Debug)]
pub struct ExecutionBudget {
    pub step_fuel: StepFuel,
    pub tick_credits: TickCredits,
}

impl ExecutionBudget {
    pub const fn new(step_fuel: StepFuel, tick_credits: TickCredits) -> Self {
        Self {
            step_fuel,
            tick_credits,
        }
    }
}

/// Versioned conservative costs for one concrete target configuration.
///
/// Values are absolute charges for one dispatch, including common dispatch
/// overhead. Capability entries include the complete bounded callee cost. The
/// model is deterministic: charges depend only on the encoded instruction,
/// never on a host cycle counter or runtime operand values.
#[derive(Clone, Copy, PartialEq, Eq, Debug)]
pub struct CostModel {
    pub version: u32,
    run_overhead: u32,
    alu: u32,
    mul: u32,
    load: [u32; 3],
    store: [u32; 3],
    branch: u32,
    call: [u32; N_CAPS],
    exit: u32,
    invalid: u32,
}

impl CostModel {
    #[allow(clippy::too_many_arguments)]
    pub const fn new(
        version: u32,
        run_overhead: u32,
        alu: u32,
        mul: u32,
        load: [u32; 3],
        store: [u32; 3],
        branch: u32,
        call: [u32; N_CAPS],
        exit: u32,
        invalid: u32,
    ) -> Self {
        assert!(run_overhead > 0 && alu > 0 && mul > 0 && branch > 0 && exit > 0 && invalid > 0);
        assert!(load[0] > 0 && load[1] > 0 && load[2] > 0);
        assert!(store[0] > 0 && store[1] > 0 && store[2] > 0);
        assert!(call[0] > 0 && call[1] > 0 && call[2] > 0);
        Self {
            version,
            run_overhead,
            alu,
            mul,
            load,
            store,
            branch,
            call,
            exit,
            invalid,
        }
    }

    /// A model useful for functional tests and timing characterization. It is
    /// not a deployment timing model.
    pub const fn uniform(charge: u32) -> Self {
        assert!(charge > 0);
        Self::new(
            0,
            charge,
            charge,
            charge,
            [charge; 3],
            [charge; 3],
            charge,
            [charge; N_CAPS],
            charge,
            charge,
        )
    }

    pub const fn run_overhead(&self) -> u32 {
        self.run_overhead
    }

    /// Conservative charge for an encoded instruction.
    pub const fn charge(&self, i: &Insn) -> u32 {
        if !admitted(i.opcode) {
            return self.invalid;
        }
        let class = i.opcode & 0x07;
        let op = i.opcode & 0xf0;
        match class {
            CLASS_ALU => {
                if op == ALU_MUL {
                    self.mul
                } else {
                    self.alu
                }
            }
            CLASS_LDX => self.load[width_index(i.opcode)],
            CLASS_ST | CLASS_STX => self.store[width_index(i.opcode)],
            CLASS_JMP => {
                if op == JMP_CALL {
                    let idx = i.imm as u32;
                    if idx < N_CAPS as u32 {
                        self.call[idx as usize]
                    } else {
                        self.invalid
                    }
                } else if op == JMP_EXIT {
                    self.exit
                } else {
                    self.branch
                }
            }
            _ => self.invalid,
        }
    }
}

const fn width_index(opcode: u8) -> usize {
    match opcode & 0x18 {
        SIZE_B => 0,
        SIZE_H => 1,
        _ => 2,
    }
}

/// Accounting returned with every halt, including abnormal halts.
#[derive(Clone, Copy, PartialEq, Eq, Debug)]
pub struct RunOutcome {
    pub halt: Halt,
    pub steps_used: u32,
    pub credits_used: u32,
}

/// Explicitly non-deployment helpers for functional tests and cycle
/// characterization. Keeping these under a conspicuous module prevents a
/// unit-cost model from looking like the target's operational cost table.
pub mod characterization {
    use super::{CostModel, ExecutionBudget, StepFuel, TickCredits};

    pub const COSTS: CostModel = CostModel::uniform(1);

    pub const fn budget(steps: StepFuel) -> ExecutionBudget {
        ExecutionBudget::new(steps, TickCredits::new(u32::MAX))
    }
}

/// Machine state. No heap, no growth, no interior mutability.
pub struct Vm {
    regs: [u32; N_REGS],
    mem: [u8; MEM_LEN],
    step_fuel: u32,
    tick_credits: u32,
}

impl Default for Vm {
    fn default() -> Self {
        Self::new()
    }
}

impl Vm {
    pub const fn new() -> Self {
        Vm {
            regs: [0; N_REGS],
            mem: [0; MEM_LEN],
            step_fuel: 0,
            tick_credits: 0,
        }
    }

    /// Read a result register after a halt.
    #[inline]
    pub fn reg(&self, i: usize) -> u32 {
        if i < N_REGS {
            self.regs[i]
        } else {
            0
        }
    }

    /// Run a loaded program.
    ///
    /// `insns` must already have passed [`loader::validate`], which
    /// establishes the opcode whitelist, in-range jump targets and the
    /// capability index. The checks repeated here are belt-and-braces: they
    /// cost a comparison each and mean a loader bug cannot become a
    /// memory-safety bug.
    ///
    /// **Fuel is the termination argument.** It holds for any program,
    /// including one that loops forever, which is precisely what it is for.
    /// The safety of running out is established elsewhere and is mandatory:
    /// IR semantics §7 requires setpoints to be double-buffered and committed
    /// only on a clean `EXIT`, with every other halt degrading to STO/SS1
    /// rather than hold-last.
    pub fn run<C: Caps>(
        &mut self,
        insns: &[Insn],
        budget: ExecutionBudget,
        costs: &CostModel,
        caps: &mut C,
    ) -> RunOutcome {
        // Reset is part of the fixed invocation overhead. It happens even for
        // a configuration-error budget so stale registers from a prior run
        // cannot be mistaken for this invocation's result.
        self.regs = [0; N_REGS];
        self.regs[REG_FP as usize] = MEM_LEN as u32;
        self.step_fuel = budget.step_fuel.get();
        self.tick_credits = budget.tick_credits.get();
        let initial_steps = self.step_fuel;
        let initial_credits = self.tick_credits;
        if self.tick_credits < costs.run_overhead() {
            return RunOutcome {
                halt: Halt::TickCreditsExhausted,
                steps_used: 0,
                credits_used: 0,
            };
        }
        self.tick_credits -= costs.run_overhead();
        let mut pc: usize = 0;
        while self.step_fuel > 0 {
            if pc >= insns.len() {
                return self.outcome(Halt::PcOutOfRange, initial_steps, initial_credits);
            }
            let charge = costs.charge(&insns[pc]);
            if self.tick_credits < charge {
                return self.outcome(Halt::TickCreditsExhausted, initial_steps, initial_credits);
            }
            // Reserve both budgets before the instruction can mutate VM state
            // or enter a capability implementation.
            self.step_fuel -= 1;
            self.tick_credits -= charge;
            match self.step(&insns[pc], &mut pc, caps) {
                Some(h) => return self.outcome(h, initial_steps, initial_credits),
                None => {}
            }
        }
        // Fuel ran out. Per IR semantics §7 this must leave nothing
        // committed: setpoints are double-buffered and land only on a clean
        // EXIT, and any other halt degrades to STO/SS1 rather than
        // hold-last. That is what makes an attacker-timed abort safe, and it
        // is why admitting loops does not reintroduce the torn-state problem:
        // a program cut off mid-flight has committed nothing.
        self.outcome(Halt::StepFuelExhausted, initial_steps, initial_credits)
    }

    fn outcome(&self, halt: Halt, initial_steps: u32, initial_credits: u32) -> RunOutcome {
        RunOutcome {
            halt,
            steps_used: initial_steps - self.step_fuel,
            credits_used: initial_credits - self.tick_credits,
        }
    }

    /// One instruction. Returns `Some(halt)` to stop, `None` to continue.
    fn step<C: Caps>(&mut self, i: &Insn, pc: &mut usize, caps: &mut C) -> Option<Halt> {
        if !admitted(i.opcode) {
            return Some(Halt::IllegalOpcode);
        }
        let class = i.opcode & 0x07;
        let op = i.opcode & 0xf0;
        let src_is_reg = i.opcode & 0x08 == SRC_REG;

        let dst = i.dst as usize;
        let srcr = i.src as usize;
        if dst >= N_REGS || srcr >= N_REGS {
            return Some(Halt::IllegalOpcode);
        }

        match class {
            CLASS_ALU => {
                // r10 is the frame pointer and is read-only. Writing it would
                // let a program relocate its own stack view.
                if i.dst == REG_FP {
                    return Some(Halt::WriteToFp);
                }
                let a = self.regs[dst];
                let b = if src_is_reg {
                    self.regs[srcr]
                } else {
                    i.imm as u32
                };
                let v = match op {
                    ALU_ADD => a.wrapping_add(b),
                    ALU_SUB => a.wrapping_sub(b),
                    ALU_MUL => a.wrapping_mul(b),
                    ALU_OR => a | b,
                    ALU_AND => a & b,
                    ALU_XOR => a ^ b,
                    ALU_MOV => b,
                    ALU_NEG => (a as i32).wrapping_neg() as u32,
                    ALU_LSH | ALU_RSH | ALU_ARSH => {
                        // Shifts of 32 or more differ between C, RV32 and
                        // eBPF. Refuse instead of picking a winner.
                        if b >= 32 {
                            return Some(Halt::ShiftOutOfRange);
                        }
                        match op {
                            ALU_LSH => a << b,
                            ALU_RSH => a >> b,
                            _ => ((a as i32) >> b) as u32,
                        }
                    }
                    _ => return Some(Halt::IllegalOpcode),
                };
                self.regs[dst] = v;
                *pc += 1;
                None
            }
            CLASS_LDX => {
                if i.dst == REG_FP {
                    return Some(Halt::WriteToFp);
                }
                let addr = self.regs[srcr].wrapping_add(i.off as i32 as u32);
                match self.load(addr, i.opcode & 0x18) {
                    Ok(v) => {
                        self.regs[dst] = v;
                        *pc += 1;
                        None
                    }
                    Err(h) => Some(h),
                }
            }
            CLASS_ST | CLASS_STX => {
                let addr = self.regs[dst].wrapping_add(i.off as i32 as u32);
                let v = if class == CLASS_STX {
                    self.regs[srcr]
                } else {
                    i.imm as u32
                };
                match self.store(addr, v, i.opcode & 0x18) {
                    Ok(()) => {
                        *pc += 1;
                        None
                    }
                    Err(h) => Some(h),
                }
            }
            CLASS_JMP => {
                match op {
                    JMP_EXIT => return Some(Halt::Exit(self.regs[0])),
                    JMP_CALL => {
                        let idx = i.imm as u32;
                        if idx as usize >= N_CAPS {
                            return Some(Halt::BadCapIndex);
                        }
                        let args = [
                            self.regs[1],
                            self.regs[2],
                            self.regs[3],
                            self.regs[4],
                            self.regs[5],
                        ];
                        self.regs[0] = caps.call(idx, args);
                        *pc += 1;
                        return None;
                    }
                    _ => {}
                }
                let a = self.regs[dst];
                let b = if src_is_reg {
                    self.regs[srcr]
                } else {
                    i.imm as u32
                };
                let taken = match op {
                    JMP_JA => true,
                    JMP_JEQ => a == b,
                    JMP_JNE => a != b,
                    JMP_JGT => a > b,
                    JMP_JGE => a >= b,
                    JMP_JLT => a < b,
                    JMP_JLE => a <= b,
                    JMP_JSET => a & b != 0,
                    _ => return Some(Halt::IllegalOpcode),
                };
                if taken {
                    // Backward jumps are admitted; the pc must still land in
                    // range, re-checked here so a loader bug cannot become a
                    // memory-safety bug.
                    let t = (*pc as i64) + 1 + (i.off as i64);
                    if t < 0 {
                        return Some(Halt::PcOutOfRange);
                    }
                    *pc = t as usize;
                } else {
                    *pc += 1;
                }
                None
            }
            _ => Some(Halt::IllegalOpcode),
        }
    }

    /// Bounds-checked load. The check is on the *computed* address, after
    /// wrapping, so an offset cannot be used to wrap past the end.
    #[inline]
    fn load(&self, addr: u32, size: u8) -> Result<u32, Halt> {
        let n = match size {
            SIZE_B => 1usize,
            SIZE_H => 2,
            _ => 4,
        };
        let a = addr as usize;
        if a > MEM_LEN || MEM_LEN - a < n {
            return Err(Halt::MemBounds);
        }
        let mut v: u32 = 0;
        let mut k = 0;
        while k < n {
            v |= (self.mem[a + k] as u32) << (8 * k);
            k += 1;
        }
        Ok(v)
    }

    /// Bounds-checked store.
    #[inline]
    fn store(&mut self, addr: u32, val: u32, size: u8) -> Result<(), Halt> {
        let n = match size {
            SIZE_B => 1usize,
            SIZE_H => 2,
            _ => 4,
        };
        let a = addr as usize;
        if a > MEM_LEN || MEM_LEN - a < n {
            return Err(Halt::MemBounds);
        }
        let mut k = 0;
        while k < n {
            self.mem[a + k] = (val >> (8 * k)) as u8;
            k += 1;
        }
        Ok(())
    }
}

//! Kani harnesses for the VM.
//!
//! The claim the interpreter owes: an untrusted program cannot escape its
//! memory, cannot fail to terminate, and cannot reach an effect outside the
//! capability table. All seven harnesses discharge under bounded model checking;
//! each states its `unwind` bound below.
//!
//! The bounds are shallow -- one to three instructions, against a machine that
//! admits `MAX_INSNS`. This is deliberate, not the limitation the depth makes
//! it look like. The properties are structural rather than depth-sensitive: V1
//! quantifies over a fully symbolic instruction rather than over program
//! length, and V5's termination argument is that the dispatch loop's trip count
//! is bounded by the fuel constant, which holds whatever the program does. A
//! reader who finds `unwind(4)` and expected a 256-deep proof should read this
//! paragraph first: depth is not what these properties turn on.

use crate::isa::*;
use crate::loader::*;
use crate::*;

struct NoCaps;
impl Caps for NoCaps {
    fn call(&mut self, _idx: u32, _args: [u32; 5]) -> u32 {
        0
    }
}

const PROOF_COSTS: CostModel = CostModel::uniform(1);

fn proof_budget(steps: u32, credits: u32) -> ExecutionBudget {
    ExecutionBudget::new(StepFuel::new(steps), TickCredits::new(credits))
}

fn any_insn() -> Insn {
    Insn {
        opcode: kani::any(),
        dst: kani::any(),
        src: kani::any(),
        off: kani::any(),
        imm: kani::any(),
    }
}

/// **V1** — an arbitrary instruction cannot escape memory or panic.
///
/// A fully symbolic instruction from the VM's concrete reset state, one run.
/// If any opcode, register pair, offset or immediate can index out of bounds
/// or overflow from that state, this fails. It does not quantify over arbitrary
/// prior register or scratch-memory contents.
#[kani::proof]
#[kani::unwind(8)]
fn v1_single_step_is_memory_safe() {
    let insn = any_insn();
    let mut vm = Vm::new();
    let prog = [insn];
    // run() re-checks everything the loader established, so an unvalidated
    // program is a legitimate input here — that is the point of the
    // belt-and-braces checks.
    let _ = vm.run(&prog, proof_budget(4, 4), &PROOF_COSTS, &mut NoCaps);
    // No explicit assert, and that is the point: panic-freedom *is* the
    // memory-safety obligation here. An out-of-bounds index or an arithmetic
    // overflow panics in safe Rust, so Kani's implicit panic and overflow checks
    // failing would be exactly a memory-safety violation. Surviving a fully
    // symbolic instruction from the concrete reset state is the property.
}

/// **V2** — a validated program never reaches an out-of-table capability.
///
/// The loader checks the immediate; `callx` is absent so the index cannot be
/// computed. Together those fix the reachable effect set at load time.
#[kani::proof]
#[kani::unwind(4)]
fn v2_capability_index_is_bounded() {
    let imm: i32 = kani::any();
    let insn = Insn {
        opcode: CLASS_JMP | JMP_CALL,
        dst: 0,
        src: 0,
        off: 0,
        imm,
    };
    let prog = [
        insn,
        Insn {
            opcode: CLASS_JMP | JMP_EXIT,
            dst: 0,
            src: 0,
            off: 0,
            imm: 0,
        },
    ];
    if validate(&prog).is_ok() {
        assert!(imm >= 0 && (imm as usize) < N_CAPS);
    }
}

/// **V3** — a validated jump target is always inside the image.
///
/// This is the property that actually matters for memory safety, and it holds
/// at either strictness. An earlier version asserted forward-only control
/// flow; that was a restriction we have since dropped, because fuel bounds
/// termination and we are proving this interpreter rather than the program.
#[kani::proof]
#[kani::unwind(4)]
fn v3_validated_jump_target_is_in_range() {
    let a = any_insn();
    let exit = Insn {
        opcode: CLASS_JMP | JMP_EXIT,
        dst: 0,
        src: 0,
        off: 0,
        imm: 0,
    };
    let prog = [a, exit];
    if validate(&prog).is_ok() && is_jump(a.opcode) {
        let op = a.opcode & 0xf0;
        if op != JMP_EXIT && op != JMP_CALL {
            let target = 1i64 + a.off as i64;
            assert!(target >= 0 && target < prog.len() as i64);
        }
    }
}

/// **V3b** — `ForwardOnly` still means what it says, for callers who want
/// worst-case execution time to be the program's own length.
#[kani::proof]
#[kani::unwind(4)]
fn v3b_forward_only_mode_rejects_backward_jumps() {
    let a = any_insn();
    let exit = Insn {
        opcode: CLASS_JMP | JMP_EXIT,
        dst: 0,
        src: 0,
        off: 0,
        imm: 0,
    };
    let prog = [a, exit];
    if validate_with(&prog, Strictness::ForwardOnly).is_ok() && is_jump(a.opcode) {
        let op = a.opcode & 0xf0;
        if op != JMP_EXIT && op != JMP_CALL {
            assert!(a.off > 0);
        }
    }
}

/// **V5** — every program halts, including one that loops forever.
///
/// This is what replaces the syntactic termination argument. It holds for an
/// arbitrary instruction at an arbitrary offset, which is the point: the
/// program's control-flow graph is not our proof obligation, and it does not
/// have to be.
#[kani::proof]
#[kani::unwind(9)]
fn v5_any_program_halts() {
    let a = any_insn();
    let exit = Insn {
        opcode: CLASS_JMP | JMP_EXIT,
        dst: 0,
        src: 0,
        off: 0,
        imm: 0,
    };
    let prog = [a, exit];
    let mut vm = Vm::new();
    // Small fuel keeps the unwind tractable; the argument is independent of
    // the constant, since the loop decrements once per iteration.
    let h = vm.run(&prog, proof_budget(8, 8), &PROOF_COSTS, &mut NoCaps);
    // The claim is that the loop terminates in a defined halt: its trip count is
    // bounded by the fuel constant, so it cannot run forever. `unwind(9)` over
    // fuel 8 is what proves the bound; this asserts the run ends in a known halt
    // rather than diverging.
    assert!(matches!(
        h.halt,
        Halt::Exit(_)
            | Halt::StepFuelExhausted
            | Halt::TickCreditsExhausted
            | Halt::PcOutOfRange
            | Halt::IllegalOpcode
            | Halt::MemBounds
            | Halt::BadCapIndex
            | Halt::WriteToFp
            | Halt::ShiftOutOfRange
    ));
}

/// **V4** — a load or store is in bounds or halts, never both.
#[kani::proof]
#[kani::unwind(8)]
fn v4_memory_access_is_checked() {
    let base: u32 = kani::any();
    let off: i16 = kani::any();
    let size: u8 = kani::any();
    kani::assume(matches!(size, SIZE_W | SIZE_H | SIZE_B));
    let prog = [
        Insn {
            opcode: CLASS_ALU | ALU_MOV | SRC_IMM,
            dst: 1,
            src: 0,
            off: 0,
            imm: base as i32,
        },
        Insn {
            opcode: CLASS_LDX | size,
            dst: 0,
            src: 1,
            off,
            imm: 0,
        },
        Insn {
            opcode: CLASS_JMP | JMP_EXIT,
            dst: 0,
            src: 0,
            off: 0,
            imm: 0,
        },
    ];
    let mut vm = Vm::new();
    // Either it completes or it reports MemBounds. It must not do anything
    // else, and must not panic.
    let h = vm.run(&prog, proof_budget(8, 8), &PROOF_COSTS, &mut NoCaps);
    assert!(matches!(
        h.halt,
        Halt::Exit(_) | Halt::MemBounds | Halt::WriteToFp
    ));
}

/// **V6** — an instruction is not executed unless its complete timing charge
/// has been reserved. The capability boundary is the externally observable
/// case: insufficient credits must leave the call count at zero.
#[kani::proof]
#[kani::unwind(3)]
fn v6_tick_charge_precedes_capability_effect() {
    struct CountingCaps {
        calls: u32,
    }
    impl Caps for CountingCaps {
        fn call(&mut self, _idx: u32, _args: [u32; 5]) -> u32 {
            self.calls += 1;
            0
        }
    }

    let prog = [
        Insn {
            opcode: CLASS_JMP | JMP_CALL,
            dst: 0,
            src: 0,
            off: 0,
            imm: 0,
        },
        Insn {
            opcode: CLASS_JMP | JMP_EXIT,
            dst: 0,
            src: 0,
            off: 0,
            imm: 0,
        },
    ];
    let costs = CostModel::new(1, 1, 1, 1, [1; 3], [1; 3], 1, [2; N_CAPS], 1, 1);
    let mut vm = Vm::new();
    let mut caps = CountingCaps { calls: 0 };
    let outcome = vm.run(&prog, proof_budget(2, 2), &costs, &mut caps);
    assert!(matches!(outcome.halt, Halt::TickCreditsExhausted));
    assert!(outcome.steps_used == 0 && outcome.credits_used == 1);
    assert!(caps.calls == 0);
}

//! Host tests for the VM. Unit tests rather than `tests/` because the crate
//! is `no_std` outside `cfg(test)` and ships a panic handler.

use crate::isa::*;
use crate::loader::*;
use crate::*;

struct NoCaps;
impl Caps for NoCaps {
    fn call(&mut self, _idx: u32, _args: [u32; 5]) -> u32 {
        0
    }
}
struct RecCaps(Vec<(u32, [u32; 5])>);
impl Caps for RecCaps {
    fn call(&mut self, idx: u32, args: [u32; 5]) -> u32 {
        self.0.push((idx, args));
        42
    }
}

fn i(opcode: u8, dst: u8, src: u8, off: i16, imm: i32) -> Insn {
    Insn {
        opcode,
        dst,
        src,
        off,
        imm,
    }
}
fn exit() -> Insn {
    i(CLASS_JMP | JMP_EXIT, 0, 0, 0, 0)
}
fn mov(d: u8, v: i32) -> Insn {
    i(CLASS_ALU | ALU_MOV | SRC_IMM, d, 0, 0, v)
}

const TEST_COSTS: CostModel = CostModel::uniform(1);

fn budget(steps: u32, credits: u32) -> ExecutionBudget {
    ExecutionBudget::new(StepFuel::new(steps), TickCredits::new(credits))
}

fn run(prog: &[Insn]) -> (Halt, Vm) {
    let steps = validate(prog).expect("program must validate").step_fuel();
    let mut vm = Vm::new();
    let outcome = vm.run(
        prog,
        ExecutionBudget::new(steps, TickCredits::new(MAX_STEP_FUEL)),
        &TEST_COSTS,
        &mut NoCaps,
    );
    (outcome.halt, vm)
}

#[test]
fn mov_and_exit() {
    let (h, vm) = run(&[mov(0, 7), exit()]);
    assert_eq!(h, Halt::Exit(7));
    assert_eq!(vm.reg(0), 7);
}

#[test]
fn arithmetic_wraps_rather_than_traps() {
    let p = [
        mov(0, -1),
        i(CLASS_ALU | ALU_ADD | SRC_IMM, 0, 0, 0, 1),
        exit(),
    ];
    assert_eq!(run(&p).0, Halt::Exit(0)); // 0xFFFF_FFFF + 1 wraps to 0
}

#[test]
fn forward_jump_skips() {
    let p = [
        mov(0, 1),
        i(CLASS_JMP | JMP_JA, 0, 0, 1, 0),
        mov(0, 99),
        exit(),
    ];
    assert_eq!(run(&p).0, Halt::Exit(1));
}

/// Loops are admitted by default. Fuel is what stops them, which is what
/// fuel is for.
#[test]
fn backward_jump_admitted_and_bounded_by_fuel() {
    // An unconditional infinite loop.
    let p = [mov(0, 1), i(CLASS_JMP | JMP_JA, 0, 0, -1, 0), exit()];
    assert!(validate(&p).is_ok(), "loops must load");
    let mut vm = Vm::new();
    assert_eq!(
        vm.run(&p, budget(32, 33), &TEST_COSTS, &mut NoCaps).halt,
        Halt::StepFuelExhausted
    );
}

/// A real counting loop -- the thing unrolling was costing us.
#[test]
fn counting_loop_runs_and_terminates() {
    // r0 = 0; r1 = 4; loop { r0 += 1; r1 -= 1; if r1 != 0 goto loop } exit
    let p = [
        mov(0, 0),
        mov(1, 4),
        i(CLASS_ALU | ALU_ADD | SRC_IMM, 0, 0, 0, 1),
        i(CLASS_ALU | ALU_SUB | SRC_IMM, 1, 0, 0, 1),
        i(CLASS_JMP | JMP_JNE | SRC_IMM, 1, 0, -3, 0),
        exit(),
    ];
    assert!(validate(&p).is_ok());
    let mut vm = Vm::new();
    assert_eq!(
        vm.run(&p, budget(64, 64), &TEST_COSTS, &mut NoCaps).halt,
        Halt::Exit(4)
    );
}

/// Forward-only remains available for programs that want their worst-case
/// execution time to be their own length rather than the fuel cap.
#[test]
fn forward_only_mode_still_rejects_backward_jumps() {
    let p = [mov(0, 1), i(CLASS_JMP | JMP_JA, 0, 0, -1, 0), exit()];
    assert!(matches!(
        validate_with(&p, Strictness::ForwardOnly),
        Err(Reject::BackwardJump { at: 1, off: -1 })
    ));
    assert_eq!(
        validate_with(&[mov(0, 1), exit()], Strictness::ForwardOnly),
        Ok(Termination::Length(2))
    );
}

#[test]
fn jump_past_the_end_rejected() {
    let p = [i(CLASS_JMP | JMP_JA, 0, 0, 50, 0), exit()];
    assert!(matches!(
        validate(&p),
        Err(Reject::JumpOutOfRange { at: 0 })
    ));
}

#[test]
fn missing_trailing_exit_rejected() {
    assert!(matches!(
        validate(&[mov(0, 1)]),
        Err(Reject::NoTrailingExit)
    ));
}

/// Deleted constructs must be rejected by the whitelist, not merely unhandled.
#[test]
fn deleted_constructs_are_rejected() {
    for opcode in [
        CLASS_ALU | 0x30,               // div
        CLASS_ALU | 0x90,               // mod
        CLASS_ALU64 | ALU_ADD,          // 64-bit ALU
        CLASS_LD,                       // lddw
        CLASS_JMP | JMP_CALL | SRC_REG, // callx
    ] {
        assert!(!admitted(opcode), "opcode {opcode:#04x} should be deleted");
        assert!(validate(&[i(opcode, 0, 0, 0, 0), exit()]).is_err());
    }
}

#[test]
fn memory_stays_in_bounds() {
    // Store then load at the top of scratch memory.
    let p = [
        mov(1, (MEM_LEN - 4) as i32),
        i(CLASS_ST | SIZE_W, 1, 0, 0, 0xAB),
        i(CLASS_LDX | SIZE_W, 0, 1, 0, 0),
        exit(),
    ];
    assert_eq!(run(&p).0, Halt::Exit(0xAB));
}

#[test]
fn out_of_bounds_access_halts() {
    let p = [
        mov(1, MEM_LEN as i32),
        i(CLASS_LDX | SIZE_W, 0, 1, 0, 0),
        exit(),
    ];
    assert_eq!(run(&p).0, Halt::MemBounds);
}

/// An offset must not be usable to wrap the address past the end.
#[test]
fn offset_cannot_wrap_past_the_end() {
    let p = [mov(1, 0), i(CLASS_LDX | SIZE_W, 0, 1, -4, 0), exit()];
    assert_eq!(run(&p).0, Halt::MemBounds);
}

#[test]
fn frame_pointer_is_read_only() {
    let p = [mov(REG_FP, 0), exit()];
    assert_eq!(run(&p).0, Halt::WriteToFp);
}

/// Shift semantics differ between C, RV32 and eBPF at 32 or more. Refusing is
/// the only answer that needs no arbitration.
#[test]
fn oversized_shift_halts_rather_than_choosing() {
    let p = [
        mov(0, 1),
        i(CLASS_ALU | ALU_LSH | SRC_IMM, 0, 0, 0, 32),
        exit(),
    ];
    assert_eq!(run(&p).0, Halt::ShiftOutOfRange);
}

#[test]
fn capability_call_reaches_the_trusted_side() {
    let p = [mov(1, 5), i(CLASS_JMP | JMP_CALL, 0, 0, 0, 1), exit()];
    let fuel = validate(&p).unwrap().step_fuel();
    let mut vm = Vm::new();
    let mut caps = RecCaps(Vec::new());
    assert_eq!(
        vm.run(
            &p,
            ExecutionBudget::new(fuel, TickCredits::new(MAX_STEP_FUEL)),
            &TEST_COSTS,
            &mut caps,
        )
        .halt,
        Halt::Exit(42)
    );
    assert_eq!(caps.0.len(), 1);
    assert_eq!(caps.0[0].0, 1);
    assert_eq!(caps.0[0].1[0], 5);
}

#[test]
fn capability_index_outside_the_table_rejected_at_load() {
    let p = [i(CLASS_JMP | JMP_CALL, 0, 0, 0, N_CAPS as i32), exit()];
    assert!(matches!(validate(&p), Err(Reject::BadCapIndex { .. })));
}

/// The two bounds are different numbers and must not be conflated: a program
/// can be well within its termination bound and still unaffordable this tick.
#[test]
fn termination_and_work_bounds_are_distinct() {
    let p = [mov(0, 1), mov(0, 2), mov(0, 3), exit()];
    // Default strictness admits loops, so the length is not a termination
    // bound and validate reports the fuel budget instead.
    assert_eq!(validate(&p), Ok(Termination::FuelBounded));
    // Under ForwardOnly the length *is* the bound.
    let term = validate_with(&p, Strictness::ForwardOnly)
        .unwrap()
        .step_fuel();
    assert_eq!(term.get(), 4);

    let mut vm = Vm::new();
    let outcome = vm.run(
        &p,
        ExecutionBudget::new(term, TickCredits::new(2)),
        &TEST_COSTS,
        &mut NoCaps,
    );
    assert_eq!(outcome.halt, Halt::TickCreditsExhausted);
    assert_eq!(outcome.steps_used, 1);
    assert_eq!(outcome.credits_used, 2);
}

/// Fuel bounds *work*. Termination rests on fuel too: loops are admitted, and
/// the fuel cap — not the program's shape — is the termination argument. (The
/// earlier "termination is syntactic" position was reversed; see `lib.rs`.)
#[test]
fn fuel_exhaustion_halts_cleanly() {
    let p = [mov(0, 1), mov(0, 2), mov(0, 3), exit()];
    let mut vm = Vm::new();
    assert_eq!(
        vm.run(&p, budget(2, 100), &TEST_COSTS, &mut NoCaps).halt,
        Halt::StepFuelExhausted
    );
}

/// Under ForwardOnly, termination is the program's own length.
#[test]
fn forward_only_terminates_within_its_length() {
    let progs: Vec<Vec<Insn>> = vec![
        vec![mov(0, 1), exit()],
        vec![
            i(CLASS_JMP | JMP_JEQ | SRC_IMM, 0, 0, 1, 0),
            mov(0, 9),
            exit(),
        ],
        vec![
            mov(0, 1),
            i(CLASS_JMP | JMP_JA, 0, 0, 1, 0),
            mov(0, 2),
            exit(),
        ],
    ];
    for p in progs {
        let fuel = validate_with(&p, Strictness::ForwardOnly)
            .unwrap()
            .step_fuel();
        assert_eq!(fuel.get(), p.len() as u32);
        let mut vm = Vm::new();
        let h = vm.run(
            &p,
            ExecutionBudget::new(fuel, TickCredits::new(p.len() as u32 + 1)),
            &TEST_COSTS,
            &mut NoCaps,
        );
        assert!(
            !matches!(h.halt, Halt::StepFuelExhausted),
            "needed more steps than instructions"
        );
    }
}

#[test]
fn weighted_credits_are_charged_by_instruction_class() {
    let costs = CostModel::new(7, 3, 2, 5, [3, 4, 6], [4, 5, 7], 3, [8, 11, 13], 1, 9);
    let p = [
        mov(0, 3),
        i(CLASS_ALU | ALU_MUL | SRC_IMM, 0, 0, 0, 2),
        i(CLASS_JMP | JMP_CALL, 0, 0, 0, 1),
        exit(),
    ];
    let mut vm = Vm::new();
    let mut caps = RecCaps(Vec::new());
    let outcome = vm.run(&p, budget(4, 22), &costs, &mut caps);
    assert_eq!(outcome.halt, Halt::Exit(42));
    assert_eq!(outcome.steps_used, 4);
    assert_eq!(outcome.credits_used, 22);
}

#[test]
fn unaffordable_capability_is_not_invoked() {
    let costs = CostModel::new(1, 1, 1, 1, [1; 3], [1; 3], 1, [5, 7, 9], 1, 1);
    let p = [i(CLASS_JMP | JMP_CALL, 0, 0, 0, 1), exit()];
    let mut vm = Vm::new();
    let mut caps = RecCaps(Vec::new());
    let outcome = vm.run(&p, budget(2, 7), &costs, &mut caps);
    assert_eq!(outcome.halt, Halt::TickCreditsExhausted);
    assert_eq!(outcome.steps_used, 0);
    assert_eq!(outcome.credits_used, 1);
    assert!(caps.0.is_empty());
}

#[test]
fn step_fuel_constructor_enforces_the_proof_ceiling() {
    assert_eq!(StepFuel::new(u32::MAX).get(), MAX_STEP_FUEL);
}

#[test]
fn forward_only_tick_admission_rejects_an_unaffordable_program() {
    let costs = CostModel::new(12, 2, 2, 5, [3, 4, 6], [4, 5, 7], 3, [8, 11, 13], 1, 9);
    let p = [
        mov(0, 1),
        i(CLASS_ALU | ALU_MUL | SRC_IMM, 0, 0, 0, 2),
        exit(),
    ];
    assert!(matches!(
        validate_for_tick(&p, &costs, TickCredits::new(9)),
        Err(Reject::TickBudgetExceeded {
            required: 10,
            available: 9
        })
    ));
    let admitted = validate_for_tick(&p, &costs, TickCredits::new(10)).unwrap();
    assert_eq!(admitted.instructions, 3);
    assert_eq!(admitted.required_credits, 10);
    assert_eq!(admitted.cost_model_version, 12);

    let mut vm = Vm::new();
    let outcome = vm.run(&p, admitted.execution_budget(), &costs, &mut NoCaps);
    assert_eq!(outcome.halt, Halt::Exit(2));
}

#[test]
fn looping_program_cannot_receive_tick_completion_admission() {
    let p = [i(CLASS_JMP | JMP_JA, 0, 0, -1, 0), exit()];
    assert!(matches!(
        validate_for_tick(&p, &TEST_COSTS, TickCredits::new(100)),
        Err(Reject::BackwardJump { .. })
    ));
}

#[test]
fn provisional_neorv32_table_is_wired_into_tick_admission() {
    let costs = crate::costs::PROVISIONAL_NEORV32_RTL_V1;
    let p = [mov(0, 1), exit()];
    // 416 fixed + 368 ALU + 448 exit.
    assert!(matches!(
        validate_for_tick(&p, &costs, TickCredits::new(1_231)),
        Err(Reject::TickBudgetExceeded {
            required: 1_232,
            available: 1_231
        })
    ));
    let admitted = validate_for_tick(&p, &costs, TickCredits::new(1_232)).unwrap();
    assert_eq!(admitted.required_credits, 1_232);
    assert_eq!(admitted.cost_model_version, 2_026_092_801);
}

//! Runs the interpreter on a real RV32 core model and reports what happened.
//!
//! Built for `riscv32imc-unknown-none-elf` and executed under
//! `qemu-system-riscv32 -machine virt`. That is the instruction set the gate
//! runs, exercised by a core model rather than by the host.
//!
//! **This is not the board.** It says the code executes correctly on the
//! architecture. It says nothing about timing, which needs the FPGA, and
//! nothing about the peripheral map, which is different on NEORV32.
//!
//! The library is `#![forbid(unsafe_code)]`. This crate is not: writing to a
//! UART and setting a stack pointer cannot be done without it, which is
//! exactly why they live out here instead of in there.

#![no_std]
#![no_main]

use endstop_vm::isa::{self, *};
use endstop_vm::loader::{validate, Reject};
use endstop_vm::{Caps, CostModel, ExecutionBudget, Halt, TickCredits, Vm, MAX_STEP_FUEL, MEM_LEN, N_CAPS};

const FUNCTIONAL_COSTS: CostModel = CostModel::uniform(1);


/// Local instruction constructor. The library keeps its own as a test helper
/// rather than public API, and a self-test is not a reason to widen that.
const fn i(opcode: u8, dst: u8, src: u8, off: i16, imm: i32) -> isa::Insn {
    isa::Insn { opcode, dst, src, off, imm }
}

// ------------------------------------------------------------------- entry

core::arch::global_asm!(
    ".section .text.entry",
    ".globl _start",
    "_start:",
    "  la sp, __stack_top",
    "  la t0, __bss_start",
    "  la t1, __bss_end",
    "1:",
    "  bgeu t0, t1, 2f",
    "  sw zero, 0(t0)",
    "  addi t0, t0, 4",
    "  j 1b",
    "2:",
    "  call main",
    "3:",
    "  j 3b",
);

// -------------------------------------------------------------- UART, exit

const UART: usize = 0x1000_0000;
const TEST_FINISHER: usize = 0x0010_0000;

fn putb(b: u8) {
    unsafe { core::ptr::write_volatile(UART as *mut u8, b) }
}

fn say(s: &str) {
    for b in s.bytes() {
        if b == b'\n' {
            putb(b'\r');
        }
        putb(b);
    }
}

fn num(mut n: u32) {
    if n == 0 {
        return putb(b'0');
    }
    let mut d = [0u8; 10];
    let mut i = 0;
    while n > 0 {
        d[i] = b'0' + (n % 10) as u8;
        n /= 10;
        i += 1;
    }
    while i > 0 {
        i -= 1;
        putb(d[i]);
    }
}

fn quit(failures: u32) -> ! {
    // The `virt` machine's SiFive test device. 0x5555 is pass; anything else
    // shifts the exit code into the upper bits.
    let code: u32 = if failures == 0 { 0x5555 } else { (failures << 16) | 0x3333 };
    unsafe { core::ptr::write_volatile(TEST_FINISHER as *mut u32, code) }
    loop {}
}

// No panic handler here on purpose. The library supplies one for
// `target_os = "none"`, and a second would be a duplicate lang item.

// ------------------------------------------------------------- the machine

const CAP_READ: u32 = 0;
const CAP_PROPOSE: u32 = 1;

struct Machine {
    current: u32,
    proposed: u32,
    calls: u32,
}

impl Caps for Machine {
    fn call(&mut self, idx: u32, args: [u32; 5]) -> u32 {
        self.calls += 1;
        match idx {
            CAP_READ => self.current,
            CAP_PROPOSE => {
                self.proposed = args[0];
                0
            }
            _ => 0,
        }
    }
}

fn machine() -> Machine {
    Machine { current: 100, proposed: 0, calls: 0 }
}

// ------------------------------------------------------------------ checks

fn check(failures: &mut u32, name: &str, ok: bool) {
    say(if ok { "  ok    " } else { "  FAIL  " });
    say(name);
    say("\n");
    if !ok {
        *failures += 1;
    }
}

#[no_mangle]
extern "C" fn main() -> ! {
    let mut bad = 0u32;

    say("\nendstop-vm on riscv32imc-unknown-none-elf, under qemu virt\n");
    say("----------------------------------------------------------\n");

    // A well-formed program loads, runs, reads state and proposes.
    let prog = [
        i(CLASS_JMP | JMP_CALL, 0, 0, 0, CAP_READ as i32),
        i(CLASS_ALU | ALU_ADD | SRC_IMM, 0, 0, 0, 7),
        // SRC_REG must be explicit: without it this is immediate mode and
        // the instruction means `r1 = 0`, which is how this test first failed.
        i(CLASS_ALU | ALU_MOV | SRC_REG, 1, 0, 0, 0),
        i(CLASS_JMP | JMP_CALL, 0, 0, 0, CAP_PROPOSE as i32),
        i(CLASS_JMP | JMP_EXIT, 0, 0, 0, 0),
    ];
    match validate(&prog) {
        Ok(bound) => {
            let mut vm = Vm::new();
            let mut m = machine();
            let halt = vm.run(
                &prog,
                ExecutionBudget::new(bound.step_fuel(), TickCredits::new(u32::MAX)),
                &FUNCTIONAL_COSTS,
                &mut m,
            ).halt;
            check(&mut bad, "a valid program loads and runs", matches!(halt, Halt::Exit(_)));
            check(&mut bad, "it read state and proposed 107", m.proposed == 107 && m.calls == 2);
        }
        Err(_) => {
            check(&mut bad, "a valid program loads and runs", false);
            check(&mut bad, "it read state and proposed 107", false);
        }
    }

    // An effect outside the table is not refused at run time. It does not load.
    let outside = [
        i(CLASS_JMP | JMP_CALL, 0, 0, 0, N_CAPS as i32),
        i(CLASS_JMP | JMP_EXIT, 0, 0, 0, 0),
    ];
    check(&mut bad, "capability 3 never loads",
          matches!(validate(&outside), Err(Reject::BadCapIndex { .. })));

    // A program that loops forever is cut off by fuel.
    let spin = [
        i(CLASS_JMP | JMP_JA, 0, 0, -1, 0),
        i(CLASS_JMP | JMP_EXIT, 0, 0, 0, 0),
    ];
    match validate(&spin) {
        Ok(f) => {
            let mut vm = Vm::new();
            let mut m = machine();
            check(&mut bad, "an infinite loop halts on fuel",
                  matches!(vm.run(
                      &spin,
                      ExecutionBudget::new(f.step_fuel(), TickCredits::new(u32::MAX)),
                      &FUNCTIONAL_COSTS,
                      &mut m,
                  ).halt, Halt::StepFuelExhausted));
        }
        Err(_) => check(&mut bad, "an infinite loop halts on fuel", false),
    }

    // A read past the region halts instead of returning data.
    let oob = [
        i(CLASS_ALU | ALU_MOV | SRC_IMM, 1, 0, 0, MEM_LEN as i32 + 64),
        i(CLASS_LDX | SIZE_W, 2, 1, 0, 0),
        i(CLASS_JMP | JMP_EXIT, 0, 0, 0, 0),
    ];
    match validate(&oob) {
        Ok(f) => {
            let mut vm = Vm::new();
            let mut m = machine();
            check(&mut bad, "a read past the region halts",
                  matches!(vm.run(
                      &oob,
                      ExecutionBudget::new(f.step_fuel(), TickCredits::new(u32::MAX)),
                      &FUNCTIONAL_COSTS,
                      &mut m,
                  ).halt, Halt::MemBounds));
        }
        Err(_) => check(&mut bad, "a read past the region halts", false),
    }

    say("----------------------------------------------------------\n");
    say("failures ");
    num(bad);
    say("\nfuel cap ");
    num(MAX_STEP_FUEL);
    say(", memory ");
    num(MEM_LEN as u32);
    say(" bytes, capabilities ");
    num(N_CAPS as u32);
    say("\n");

    quit(bad)
}