//! Validate the root startup bundle from user mode.

export mod abi;

export mod sys;

/// Typed startup view used by the boot root package.

record Env: Copy {

    /// Root-owned resource bundle.

    argsPointer: *abi::BootInfo,

    /// Byte size of the bundle header.

    argsSize: u64,

    /// Installed Events capability.

    eventsHandle: u64,

    /// Shared event-ring address.

    eventsPointer: u64,

}

/// Check root identity, resource ordering, and image authority before returning.

@default unsafe fn main(env: *Env) {

    assert env.argsSize == @sizeOf(abi::BootInfo) as u64;

    let info = env.argsPointer;

    let handles = info.handles;

    let self = sys::queryDomain(abi::Handle(handles[0]));

    assert (self.id & 0xffffffff) == 0 and self.creator == self.id;

    assert handles[1] == env.eventsHandle and info.timebase > 0;

    let mut harts: u64 = 0;

    for hart in 0..8 { if (info.harts & (1 << hart as u64)) <> 0 { set harts += 1; } }

    assert handles.len as u64 == 2 + info.devices + info.interrupts + harts;

    for i in 0..info.devices as u32 {

        let device = sys::queryDevice(abi::Handle(handles[2 + i]));

        assert device.size > 0;

    }

    for i in 0..info.interrupts as u32 {

        let irq = sys::queryInterrupt(abi::Handle(handles[2 + info.devices as u32 + i]));

        assert irq.number == i + 1;

    }

    assert sys::queryDevice(info.clock).size == 8;

    assert sys::queryDevice(info.shutdown).size >= 4;

    assert (try! sys::queryImage(info.rootImage)).entry <> 0;

    assert (try! sys::queryImage(info.schedulerImage)).entry <> 0;

    let current = sys::currentContext();

    let first = 2 + info.devices as u32 + info.interrupts as u32;

    assert current.hart == 0 and current.budget == handles[first];

    assert (try! sys::queryBudget(abi::Handle(handles[first]))).hart == 0;

}