The interpreter, in full

//! The admitted instruction subset.
//!
//! Encoding: eBPF / RFC 9669, because LLVM has a BPF backend and we want the
//! model-emits-C, `clang -target bpf` pipeline for free. Semantics: ours,
//! normatively.
//!
//! ## 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 |
//! | **backward jumps** | makes termination syntactic — and makes *this file* verifiable |
//! | `lddw`, `callx` | a computed call index defeats capability confinement |
//! | atomics | single-threaded machine |
//!
//! Deleting backward jumps is the load-bearing one twice over. It turns
//! termination into a load-time check, and it bounds the dispatch loop, which
//! is what lets bounded model checking reach this code at all.

/// 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 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,
}

/// The two bounds a caller needs, kept apart because conflating them is easy
/// and the failure is silent.
#[derive(Clone, Copy, PartialEq, Eq, Debug)]
pub struct Bounds {
    /// Steps after which the program has provably finished: its own length,
    /// since forward-only jumps mean no instruction executes twice. This is
    /// the **termination** argument.
    pub termination: u32,
    /// Steps the tick can afford. A different question entirely — it is about
    /// the control period, not about the program — and it is the smaller of
    /// the two in any realistic configuration.
    pub work_budget: u32,
}

impl Bounds {
    /// The fuel to actually pass to [`crate::Vm::run`].
    ///
    /// A program may be shorter than the tick allows, in which case
    /// termination binds. A program may be longer, in which case the tick
    /// binds and the program is cut off mid-flight — which is safe, because
    /// an abort drives the safe state, but which the operator should see as
    /// a configuration error rather than normal operation.
    #[inline]
    pub fn fuel(&self) -> u32 {
        if self.termination < self.work_budget {
            self.termination
        } else {
            self.work_budget
        }
    }

    /// True when the tick budget, not the program, is what will stop it.
    /// Worth surfacing at load time: a program that cannot finish inside a
    /// tick will be aborted every tick, forever.
    #[inline]
    pub fn work_bound_binds(&self) -> bool {
        self.work_budget < self.termination
    }
}

/// Validate an image. Returns the **termination** bound, which is not the
/// same number as the tick's fuel budget — see [`Bounds`].
///
/// The order matters: length before anything indexed, opcodes before their
/// operands are interpreted, and jump targets last, since they depend on the
/// length already being known.
/// 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,
}

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

/// Validate an image.
///
/// Returns the **termination** bound. Under [`Strictness::ForwardOnly`] that
/// is the program length, since no instruction executes twice. Otherwise it
/// is the caller's fuel cap, because a looping program's step count is not a
/// property of its length.
pub fn validate_with(insns: &[Insn], strict: Strictness) -> Result<u32, 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 — the tick's budget,
    // `DEFAULT_FUEL`, which is what a program actually gets. The hard ceiling
    // `MAX_FUEL` sits above it and only limits a caller that asks for more.
    Ok(match strict {
        Strictness::ForwardOnly => insns.len() as u32,
        Strictness::Default => crate::DEFAULT_FUEL,
    })
}

//! # 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
//!
//! **Fuel bounds the dispatch loop**, and fuel is capped at [`MAX_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
//!
//! Implemented, undischarged. Until the harnesses pass, the honest
//! description is "a verification target that fits our tools".

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

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 = 256;
/// Hard ceiling on fuel, and therefore the dispatch loop's bound.
///
/// This is what bounds the loop — not the program length. `run` clamps any
/// requested fuel to this value, so the trip count is a compile-time constant
/// no matter what a caller passes, which is what keeps the dispatch loop
/// verifiable. It is the ceiling, not the operating budget: a tick hands out
/// [`DEFAULT_FUEL`], and only a caller that asks for more than that is limited
/// by this cap. The proofs assume small fuel and are independent of its value.
pub const MAX_FUEL: u32 = 4096;
/// The fuel a tick hands a program by default: enough to admit real loops,
/// well under the [`MAX_FUEL`] ceiling. This is the number that decides how
/// much work a program actually gets, and it is what the loader returns.
pub const DEFAULT_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),
    FuelExhausted,
    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;
}

/// Machine state. No heap, no growth, no interior mutability.
pub struct Vm {
    regs: [u32; N_REGS],
    mem: [u8; MEM_LEN],
    fuel: 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],
            fuel: 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], fuel: u32, caps: &mut C) -> Halt {
        self.regs = [0; N_REGS];
        self.regs[REG_FP as usize] = MEM_LEN as u32;
        self.fuel = fuel;

        // Fuel is the termination argument and the loop bound. Capping it
        // here means the trip count is a compile-time constant regardless of
        // what the program's control flow does.
        if self.fuel > MAX_FUEL {
            self.fuel = MAX_FUEL;
        }
        let mut pc: usize = 0;
        while self.fuel > 0 {
            self.fuel -= 1;
            if pc >= insns.len() {
                return Halt::PcOutOfRange;
            }
            match self.step(&insns[pc], &mut pc, caps) {
                Some(h) => return h,
                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.
        Halt::FuelExhausted
    }

    /// 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. Until these discharge, the honest description is
//! "a verification target that fits our tools".

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
    }
}

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 against a symbolic machine, one step. If any
/// opcode, register pair, offset or immediate can index out of bounds or
/// overflow, this fails. This is the memory-safety obligation in its
/// strongest single-step form.
#[kani::proof]
#[kani::unwind(8)]
fn v1_single_step_is_memory_safe() {
    let insn = any_insn();
    let mut vm = Vm::new();
    let mut pc: usize = kani::any();
    kani::assume(pc < MAX_INSNS);
    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, 4, &mut NoCaps);
    let _ = pc;
}

/// **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, 8, &mut NoCaps);
    // Reaching any halt at all is the claim. It cannot run forever.
    let _ = h;
}

/// **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, 8, &mut NoCaps);
    assert!(matches!(h, Halt::Exit(_) | Halt::MemBounds | Halt::WriteToFp));
}

//! 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) }

fn run(prog: &[Insn]) -> (Halt, Vm) {
    let fuel = validate(prog).expect("program must validate");
    let mut vm = Vm::new();
    let h = vm.run(prog, fuel, &mut NoCaps);
    (h, 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, 32, &mut NoCaps), Halt::FuelExhausted);
}

/// 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, 64, &mut NoCaps), 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(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();
    let mut vm = Vm::new();
    let mut caps = RecCaps(Vec::new());
    assert_eq!(vm.run(&p, fuel, &mut caps), 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 tick's fuel budget instead. That budget
    // is DEFAULT_FUEL, which sits below the MAX_FUEL ceiling the run loop
    // clamps to.
    assert_eq!(validate(&p), Ok(DEFAULT_FUEL));
    assert!(DEFAULT_FUEL <= MAX_FUEL);
    // Under ForwardOnly the length *is* the bound.
    let term = validate_with(&p, Strictness::ForwardOnly).unwrap();
    assert_eq!(term, 4);

    // Tick can afford the whole program: termination binds.
    let roomy = Bounds { termination: term, work_budget: 144 };
    assert_eq!(roomy.fuel(), 4);
    assert!(!roomy.work_bound_binds());

    // Tick cannot: the work budget binds, and that is a configuration error
    // the operator should see rather than a normal abort.
    let tight = Bounds { termination: term, work_budget: 2 };
    assert_eq!(tight.fuel(), 2);
    assert!(tight.work_bound_binds());

    let mut vm = Vm::new();
    assert_eq!(vm.run(&p, tight.fuel(), &mut NoCaps), Halt::FuelExhausted);
}

/// Fuel bounds *work*, not termination — termination is already syntactic.
#[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, 2, &mut NoCaps), Halt::FuelExhausted);
}

/// 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();
        assert_eq!(fuel, p.len() as u32);
        let mut vm = Vm::new();
        let h = vm.run(&p, fuel, &mut NoCaps);
        assert!(!matches!(h, Halt::FuelExhausted), "needed more steps than instructions");
    }
}

//! 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, Halt, Vm, MAX_FUEL, MEM_LEN, N_CAPS};


/// 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(fuel) => {
            let mut vm = Vm::new();
            let mut m = machine();
            let halt = vm.run(&prog, fuel, &mut m);
            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, f, &mut m), Halt::FuelExhausted));
        }
        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, f, &mut m), Halt::MemBounds));
        }
        Err(_) => check(&mut bad, "a read past the region halts", false),
    }

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

    quit(bad)
}