// MODELED_ONLY CPU/timer/register witnesses; the retained three-member Table,
// Context, Async and Completion owners are the real frozen implementations.


use std::{
    cell::{Cell, RefCell},
    rc::Rc,
};
use turkos_os_k1080_wait_main::{context as os_k1060_context, runqueue as os_k1060_queue};
use turkos_os_threads::threads as os_k1060_thread;
#[path = "context-model.rs"]
mod model;
fn park() -> ! {
    panic!("bounded host park with actual retained owner");
}
include!("backend-under-test.rs");

#[unsafe(no_mangle)]
extern "C" fn __os_k1060_backend_identity() -> u64 {
    use std::sync::atomic::{AtomicU64, Ordering};
    static NEXT: AtomicU64 = AtomicU64::new(1);
    NEXT.try_update(Ordering::Relaxed, Ordering::Relaxed, |n| n.checked_add(1))
        .unwrap_or(0)
}
struct Tick {
    issuer: *const RefCell<model::Cpu>,
    sequence: u64,
    observation: os_k1060_queue::TickObservation,
    held: Rc<Cell<bool>>,
}
unsafe impl os_k1060_context::QueueServices for model::Device {
    type QueueTick = Tick;
    fn queue_capture(&self) -> Option<os_k1060_context::Capture> {
        self.inner.hardware.borrow().capture
    }
    fn queue_tick(
        &self,
        t: &Tick,
    ) -> Result<os_k1060_queue::TickObservation, os_k1060_queue::Error> {
        if t.issuer != Rc::as_ptr(&self.cpu)
            || self.cpu.borrow().tick_live != Some(t.sequence)
            || !t.held.get()
        {
            return Err(os_k1060_queue::Error::Tick);
        }
        Ok(t.observation)
    }
    fn queue_consume_tick(&mut self, t: Tick) {
        assert_eq!(self.cpu.borrow().tick_live, Some(t.sequence));
        self.cpu.borrow_mut().tick_live = None;
        self.cpu.borrow_mut().tick_consumed += 1;
        t.held.set(false);
    }
}
unsafe impl os_k1060_context::InactiveBackend for model::Device {
    fn cancel_inactive(&mut self, b: &Self::Binding) -> Result<(), os_k1060_context::Failure> {
        self.inner
            .table
            .borrow_mut()
            .cancel(b.id)
            .map_err(|_| os_k1060_context::Failure {
                error: os_k1060_context::Error::State,
                phase: os_k1060_context::FailurePhase::BeforeSwitch,
            })?;
        if self
            .inner
            .sleep_wait
            .as_ref()
            .is_some_and(|w| w.thread() == b.id)
        {
            self.inner.sleep_wait = None;
        }
        Ok(())
    }
}
type B = OsK1060QueueBackend<model::Device>;
type Q = os_k1060_queue::ReturnQueue<B, 3>;
type Setup = (
    B,
    Vec<os_k1060_context::Handle>,
    Rc<RefCell<model::saved::Hardware>>,
    Rc<RefCell<model::Cpu>>,
);
fn backend() -> Setup {
    let (bank, h, hardware, cpu) = model::setup(3);
    let bank = os_k1060_context::CompletionBank::new(bank).ok().unwrap();
    (B::new(bank).ok().unwrap(), h, hardware, cpu)
}
type QueueSetup = (
    Q,
    Vec<os_k1060_queue::Handle>,
    Rc<RefCell<model::saved::Hardware>>,
    Rc<RefCell<model::Cpu>>,
);
fn queue() -> QueueSetup {
    let (mut b, h, hardware, cpu) = backend();
    let members = h
        .iter()
        .enumerate()
        .map(|(i, h)| b.issue(*h, i).unwrap())
        .collect::<Vec<_>>();
    let mut q = os_k1060_queue::Queue::new(b).ok().unwrap();
    let ids = members
        .into_iter()
        .enumerate()
        .map(|(i, m)| {
            q.enqueue(
                m,
                if i == 1 {
                    os_k1060_queue::Class::Low
                } else {
                    os_k1060_queue::Class::Normal
                },
            )
            .ok()
            .unwrap()
        })
        .collect();
    (
        os_k1060_queue::ReturnQueue::new(os_k1060_queue::AsyncQueue::new(q).ok().unwrap())
            .ok()
            .unwrap(),
        ids,
        hardware,
        cpu,
    )
}
fn capture(q: &Q) -> os_k1060_context::Capture {
    q.queue().with_backend_observation(|b| {
        let d = b
            .bank
            .handoff()
            .bank()
            .with_backend_observation(|d| d.inner.hardware.clone());
        let id = d.borrow().current.unwrap();
        let h = b
            .members
            .iter()
            .flatten()
            .find(|h| b.bank.handoff().bank().record(**h).unwrap().thread == id)
            .copied()
            .unwrap();
        model::capture(b.bank.handoff(), h, &d, 73, false)
    })
}
fn step(q: &mut Q, sleep: bool) -> os_k1060_queue::Handle {
    if q.queue().snapshot().active != 0 {
        capture(q);
    }
    let t = q
        .select(if sleep {
            os_k1060_queue::Disposition::Sleeping
        } else {
            os_k1060_queue::Disposition::Ready
        })
        .unwrap();
    let t = q.depart(t).ok().unwrap();
    q.queue().with_retained_observation(|p| {
        q.queue().with_backend_observation(|b| {
            model::physical_step(b.bank.handoff(), p.unwrap().handoff.as_ref().unwrap())
        })
    });
    q.landed(t).ok().unwrap()
}
fn ownership(q: &Q) -> (usize, u64, usize) {
    q.queue().with_backend_observation(|b| {
        b.bank.handoff().bank().with_backend_observation(|d| {
            let h = d.inner.hardware.borrow();
            (h.pins, h.stack_pages, b.members.iter().flatten().count())
        })
    })
}
fn returned(q: &Q) {
    q.queue().with_backend_observation(|b| {
        b.bank.handoff().bank().with_backend_observation(|d| {
            let f = model::bootstrap();
            d.cpu.borrow_mut().registers = Some(f);
            d.inner.hardware.borrow_mut().sp = f.sp - 64;
        })
    });
}