use super::{arbitrary_endpoint_cap, insert_cap};
use domain::capability::{Capability, CapabilityTable};
use domain::endpoint::Endpoint;
use domain::resource::Resource;
use types::generation::Generation;
use types::id::EndpointId;
use types::permission::{Permission, PermissionSet};

#[kani::proof]
fn revoke_invalidates_cap_slot() {
    let bits: u8 = kani::any();
    let ep_id: u16 = kani::any();
    kani::assume(ep_id < 256);

    let mut table = CapabilityTable::new();
    let slot = insert_cap(&mut table, arbitrary_endpoint_cap(bits, ep_id));

    assert!(table.get(slot).is_ok());
    table.remove(slot).unwrap();
    assert!(table.get(slot).is_err());
}

#[kani::proof]
fn revoke_does_not_affect_other_slots() {
    let bits_a: u8 = kani::any();
    let bits_b: u8 = kani::any();

    let cap_a = Capability::new(
        Resource::ProcessCreate,
        PermissionSet::from_bits(bits_a),
        Generation::initial(),
    );
    let cap_b = Capability::new(
        Resource::Endpoint(EndpointId::from_raw(0)),
        PermissionSet::from_bits(bits_b),
        Generation::initial(),
    );

    let mut table = CapabilityTable::new();
    let slot_a = insert_cap(&mut table, cap_a);
    let slot_b = insert_cap(&mut table, cap_b);

    table.remove(slot_a).unwrap();

    assert!(table.get(slot_a).is_err());
    assert!(table.get(slot_b).is_ok());
    assert!(*table.get(slot_b).unwrap().permissions() == PermissionSet::from_bits(bits_b));
}

#[kani::proof]
fn grant_cap_preserves_resource_identity() {
    let ep_id: u16 = kani::any();
    kani::assume(ep_id < 256);
    let bits: u8 = kani::any();

    let mut table = CapabilityTable::new();
    let slot = insert_cap(&mut table, arbitrary_endpoint_cap(bits, ep_id));

    let retrieved = table.get(slot).unwrap();
    match retrieved.resource() {
        Resource::Endpoint(id) => assert!(id.raw() == ep_id),
        _ => panic!("resource type changed"),
    }
}

#[kani::proof]
fn generation_revocation_invalidates_all_caps() {
    let bits: u8 = kani::any();
    let ep_id: u16 = kani::any();
    kani::assume(ep_id < 256);

    let mut endpoint = Endpoint::new(EndpointId::from_raw(ep_id));
    let original_gen = *endpoint.generation();

    let cap = Capability::new(
        Resource::Endpoint(EndpointId::from_raw(ep_id)),
        PermissionSet::from_bits(bits),
        original_gen,
    );

    let mut table = CapabilityTable::new();
    let slot = insert_cap(&mut table, cap);

    assert!(
        table
            .get(slot)
            .unwrap()
            .generation()
            .is_valid_against(&original_gen)
    );

    endpoint.revoke();
    let new_gen = *endpoint.generation();

    assert!(
        !table
            .get(slot)
            .unwrap()
            .generation()
            .is_valid_against(&new_gen)
    );
}

#[kani::proof]
fn cap_created_after_revoke_is_valid() {
    let ep_id: u16 = kani::any();
    kani::assume(ep_id < 256);
    let bits: u8 = kani::any();

    let mut endpoint = Endpoint::new(EndpointId::from_raw(ep_id));
    endpoint.revoke();
    let current_gen = *endpoint.generation();

    let cap = Capability::new(
        Resource::Endpoint(EndpointId::from_raw(ep_id)),
        PermissionSet::from_bits(bits),
        current_gen,
    );

    assert!(cap.generation().is_valid_against(&current_gen));
}

#[kani::proof]
fn multiple_revocations_invalidate_all_prior_caps() {
    let ep_id: u16 = kani::any();
    kani::assume(ep_id < 256);

    let mut endpoint = Endpoint::new(EndpointId::from_raw(ep_id));

    let gen0 = *endpoint.generation();
    let cap0 = Capability::new(
        Resource::Endpoint(EndpointId::from_raw(ep_id)),
        PermissionSet::empty().with(Permission::Read),
        gen0,
    );

    endpoint.revoke();
    let gen1 = *endpoint.generation();
    let cap1 = Capability::new(
        Resource::Endpoint(EndpointId::from_raw(ep_id)),
        PermissionSet::empty().with(Permission::Read),
        gen1,
    );

    endpoint.revoke();
    let gen2 = *endpoint.generation();

    assert!(!cap0.generation().is_valid_against(&gen2));
    assert!(!cap1.generation().is_valid_against(&gen2));
}