Function vec_checked_lookup

src/tcb/misc.rs:16–21

(
    vec: &Vec<RuntimeResult<HostFd>>,
    index: SboxFd,
)

#[pure]
#[requires(index < MAX_SBOX_FDS )]
pub fn vec_checked_lookup(
    vec: &Vec<RuntimeResult<HostFd>>,
    index: SboxFd,
) -> RuntimeResult<HostFd> {
    vec[index as usize]
}

// Once again, Prusti does not accept that this is pure
#[trusted]