//! Mint creates no authority. The real kernel, with tables shrunk under
//! `cfg(kani)`, runs `mint` with arbitrary arguments in a small state
//! whose capabilities carry arbitrary rights. Afterwards every capability
//! to an object that already existed carries no more rights than some
//! capability to that object carried before.
//!
//! Only this harness is kept. The same check over delegate, delete,
//! revoke, create and kill either exceeded 12 GB in CBMC or tripped
//! modelling artifacts ("unreachable code" on safe `Option` matches that
//! an exhaustive host replay never reaches). Those operations are covered
//! by the syscall storm's global invariants (tests/storm.rs) and the
//! capability-tree model test (tests/captree_model.rs) instead.

use super::platform::KaniPlatform;
use crate::Kernel;
use domain::{capability::MAX_CAPS_PER_PROCESS, process::MAX_PROCESSES, resource::Resource};
use types::{
    address::PhysicalAddress,
    badge::Badge,
    bounded::{CapSlot, Priority},
    id::ProcessId,
    permission::PermissionSet,
    time::TimeSlice,
};

#[derive(Clone, Copy, PartialEq)]
struct Held {
    resource: Resource,
    perms: PermissionSet,
    badge: Badge,
}

type Snapshot = [[Option<Held>; MAX_CAPS_PER_PROCESS]; MAX_PROCESSES];

fn snapshot(k: &Kernel<KaniPlatform>) -> Snapshot {
    let mut s = [[None; MAX_CAPS_PER_PROCESS]; MAX_PROCESSES];
    for (p, row) in s.iter_mut().enumerate() {
        if let Ok(process) = k.processes.get(ProcessId::from_raw(p as u16)) {
            for (slot, cap) in process.capabilities().iter() {
                row[slot.value() as usize] = Some(Held {
                    resource: *cap.resource(),
                    perms: *cap.permissions(),
                    badge: cap.badge(),
                });
            }
        }
    }
    s
}

/// Whether `resource` named a live object before the operation.
fn existed(before: &Snapshot, resource: &Resource) -> bool {
    before
        .iter()
        .flatten()
        .flatten()
        .any(|h| h.resource == *resource)
}

/// Some capability before the operation already granted at least `h`.
fn justified(before: &Snapshot, h: &Held) -> bool {
    before.iter().flatten().flatten().any(|b| {
        b.resource == h.resource
            && h.perms.is_subset_of(&b.perms)
            && (b.badge == h.badge || b.badge.is_none())
    })
}

fn any_perms() -> PermissionSet {
    PermissionSet::from_bits(kani::any::<u8>() & 0b1111)
}

fn any_slot() -> CapSlot {
    CapSlot::new(kani::any::<u8>() % (CapSlot::MAX + 1)).unwrap()
}

/// Init and one more process, an endpoint, a notification, and caps with
/// arbitrary rights spread over both, including a cap to the other process.
fn small_world() -> Kernel<KaniPlatform> {
    let mut k = Kernel::new(KaniPlatform, PhysicalAddress::from_raw(0x8400_0000), 6);
    let (init, _) = k.boot(Priority::DEFAULT, TimeSlice::DEFAULT).unwrap();
    let b = k.create_process_internal().unwrap();
    k.spawn_thread_internal(b).unwrap();
    let ep = k.create_endpoint(init).unwrap();
    let n = k.create_notification(b).unwrap();
    k.grant_capability(init, Resource::Endpoint(ep), any_perms())
        .unwrap();
    k.grant_capability(init, Resource::Process(b), any_perms())
        .unwrap();
    k.grant_capability(b, Resource::Endpoint(ep), any_perms())
        .unwrap();
    k.grant_capability(b, Resource::Notification(n), any_perms())
        .unwrap();
    k
}

/// The caller is concrete: a symbolic pid turns every table lookup into a
/// symbolic index and blows CBMC's formula up past 30 GB.
#[kani::proof]
#[kani::unwind(8)]
fn mint_creates_no_authority() {
    let mut k = small_world();
    let (slot, badge, perms) = (any_slot(), Badge::new(kani::any()), any_perms());
    let before = snapshot(&k);
    let _ = k.mint(ProcessId::from_raw(0), slot, badge, perms);
    let after = snapshot(&k);
    for (p, row) in after.iter().enumerate() {
        for (s, held) in row.iter().enumerate() {
            let Some(h) = held else { continue };
            if before[p][s] == Some(*h) {
                continue; // untouched
            }
            if existed(&before, &h.resource) {
                assert!(justified(&before, h), "authority appeared from nowhere");
            }
        }
    }
}