//! MODELED_ONLY CPU/timer/register witnesses; the retained three-member Table,
//! Context, Async and Completion owners are the real frozen implementations.
#![allow(dead_code)]
use os_k1060_queue::Backend as _;
use std::{
    cell::{Cell, RefCell},
    rc::Rc,
};
use turkos_os_runqueue_guest_services::{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;
        })
    });
}

#[test]
fn actual_three_members_cycle_fifo_without_duplicating_an_owner() {
    let (mut q, h, _, _) = queue();
    let inventory = ownership(&q);
    for i in 0..30 {
        assert_eq!(step(&mut q, false), h[i % 3]);
        assert_eq!(ownership(&q), inventory);
    }
    assert_eq!(
        h.iter()
            .map(|h| q.queue().record(*h).unwrap().slices)
            .sum::<u64>(),
        30
    );
}
#[test]
fn issuer_ordinal_and_actual_handle_are_private_and_checked() {
    let (mut b, h, _, _) = backend();
    let m = b.issue(h[0], 0).unwrap();
    assert!(matches!(
        b.issue(h[0], 1),
        Err(os_k1060_queue::Error::Duplicate)
    ));
    assert!(matches!(
        b.issue(h[1], 3),
        Err(os_k1060_queue::Error::Duplicate)
    ));
    let mut fake = OsK1060Member {
        identity: m.identity + 1,
        context: m.context,
        thread: m.thread,
        ordinal: m.ordinal,
        retired: false,
    };
    assert!(matches!(b.member(&fake), Err(os_k1060_queue::Error::Stale)));
    fake.identity = m.identity;
    fake.ordinal = 2;
    assert!(matches!(b.member(&fake), Err(os_k1060_queue::Error::Stale)));
    let (other, _, _, _) = backend();
    assert!(matches!(
        other.member(&m),
        Err(os_k1060_queue::Error::Stale)
    ));
    assert_eq!(b.members.iter().flatten().count(), 1);
}
#[test]
fn constructor_refusal_returns_the_same_three_real_owners() {
    let (bank, _, h, _) = model::setup(3);
    let bank = os_k1060_context::CompletionBank::new(bank).ok().unwrap();
    h.borrow_mut().cpu = 1;
    let (error, bank) = B::new(bank).err().unwrap();
    assert_eq!(error, os_k1060_queue::Error::Context);
    assert_eq!(bank.handoff().bank().snapshot().retained, 3);
    assert_eq!((h.borrow().pins, h.borrow().stack_pages), (3, 12));
}
#[test]
fn service_gate_precedes_every_actual_table_or_stack_observation() {
    let (mut b, h, hardware, _) = backend();
    let m = b.issue(h[0], 0).unwrap();
    for kind in 0..3 {
        let table = b.bank.handoff().bank().with_backend_observation(|d| {
            &d.inner.table as *const RefCell<os_k1060_thread::Table<model::saved::ThreadBackend, 3>>
        });
        let _exclusive = unsafe { &*table }.borrow_mut();
        {
            let mut hw = hardware.borrow_mut();
            hw.cpu = if kind == 0 { 1 } else { 0 };
            hw.daif = if kind == 1 { 0 } else { 0x3c0 };
            hw.in_irq = kind == 2;
        }
        assert!(matches!(
            b.bank.os_k1060_observe_member(h[0]),
            Err(os_k1060_context::Error::Context)
        ));
        assert!(matches!(b.member(&m), Err(os_k1060_queue::Error::Backend)));
        assert!(matches!(
            b.bank.os_k1060_capture(),
            Err(os_k1060_context::Error::Context)
        ));
    }
}
#[test]
fn before_depart_preserves_real_lookup_and_all_owner_bytes() {
    let (mut q, _, h, cpu) = queue();
    let before = q.queue().snapshot();
    let inv = ownership(&q);
    let t = q.select(os_k1060_queue::Disposition::Ready).unwrap();
    cpu.borrow_mut().depart_fail = Some(os_k1060_context::FailurePhase::BeforeSwitch);
    let t = match q.depart(t) {
        Err(os_k1060_queue::HandoffSelectionError::Before(_, t)) => t,
        _ => panic!("expected retained Before lookup"),
    };
    q.queue()
        .with_retained_observation(|p| assert!(p.unwrap().handoff.is_some()));
    cpu.borrow_mut().depart_fail = None;
    q.abort(t).ok().unwrap();
    assert_eq!(q.queue().snapshot(), before);
    assert_eq!(ownership(&q), inv);
    assert_eq!(h.borrow().releases, 0);
}
#[test]
fn after_depart_quarantines_real_prepared_and_three_stack_owners() {
    let (mut q, _, h, cpu) = queue();
    let inv = ownership(&q);
    let t = q.select(os_k1060_queue::Disposition::Ready).unwrap();
    cpu.borrow_mut().depart_fail = Some(os_k1060_context::FailurePhase::AfterSwitch);
    assert!(matches!(
        q.depart(t),
        Err(os_k1060_queue::HandoffSelectionError::Quarantined(_))
    ));
    assert!(q.quarantined());
    q.queue()
        .with_backend_observation(|b| assert!(b.bank.handoff().quarantined()));
    assert_eq!(ownership(&q), inv);
    assert_eq!(h.borrow().releases, 0);
}
#[test]
fn failed_abort_keeps_the_actual_prepared_token_inside_owned_backend() {
    let (mut q, _, h, _) = queue();
    let t = q.select(os_k1060_queue::Disposition::Ready).unwrap();
    h.borrow_mut().abort_fail = true;
    assert!(q.abort(t).is_err());
    q.queue().with_backend_observation(|b| {
        assert!(b.bank.handoff().quarantined());
        assert!(b.bank.handoff().bank().snapshot().retained_switch);
    });
    assert_eq!(ownership(&q), (3, 12, 3));
}
#[test]
fn real_sleeping_member_stays_off_fifo_with_actual_wait_retained() {
    let (mut q, h, _, _) = queue();
    assert_eq!(step(&mut q, false), h[0]);
    assert_eq!(step(&mut q, true), h[1]);
    q.queue().with_backend_observation(|b| {
        assert_eq!(
            b.member(&OsK1060Member {
                identity: b.identity,
                context: b.members[0].unwrap(),
                thread: q.queue().record(h[0]).unwrap().thread,
                ordinal: 0,
                retired: false,
            })
            .unwrap()
            .thread
            .state,
            os_k1060_thread::State::Sleeping
        )
    });
    assert!(
        !q.queue()
            .ready_order()
            .iter()
            .flatten()
            .any(|id| *id == h[0])
    );
    for _ in 0..4 {
        assert_ne!(step(&mut q, false), h[0]);
    }
    assert_eq!(ownership(&q), (3, 12, 3));
    q.queue().with_backend_observation(|b| {
        b.bank
            .handoff()
            .bank()
            .with_backend_observation(|d| assert!(d.inner.sleep_wait.is_some()))
    });
}
#[test]
fn completion_publishes_only_after_real_dead_and_bootstrap_landing() {
    let (mut q, _, h, _) = queue();
    step(&mut q, false);
    let c = capture(&q);
    let t = q.prepare_return(c).unwrap();
    let t = q.depart_return(t).ok().unwrap();
    assert_eq!(h.borrow().current, None);
    returned(&q);
    q.return_landed(t).ok().unwrap();
    assert_eq!(q.queue().snapshot().active, 0);
    assert_eq!(ownership(&q), (3, 12, 3));
    assert_eq!(h.borrow().releases, 0);
}
#[test]
fn failed_finish_retains_real_completion_prepared_and_old_queue_active() {
    let (mut q, _, h, _) = queue();
    step(&mut q, false);
    let before = q.queue().snapshot();
    let c = capture(&q);
    let t = q.prepare_return(c).unwrap();
    let t = q.depart_return(t).ok().unwrap();
    returned(&q);
    h.borrow_mut().finish_fail = true;
    assert!(q.return_landed(t).is_err());
    assert_eq!(q.queue().snapshot().active, before.active);
    q.queue()
        .with_backend_observation(|b| assert!(b.bank.with_return_observation(|p| p.is_some())));
    assert_eq!(ownership(&q), (3, 12, 3));
}
#[test]
fn failed_tick_is_retained_before_bounded_park() {
    let (mut b, h, hardware, cpu) = backend();
    let m = b.issue(h[0], 0).unwrap();
    let held = Rc::new(Cell::new(true));
    let t = Tick {
        issuer: Rc::as_ptr(&cpu),
        sequence: 1,
        observation: os_k1060_queue::TickObservation {
            cpu: 0,
            source: 30,
            sequence: 1,
            counter: 1,
            thread: m.thread,
            slice: 1,
        },
        held: held.clone(),
    };
    cpu.borrow_mut().tick_live = Some(1);
    hardware.borrow_mut().in_irq = true;
    assert!(std::panic::catch_unwind(std::panic::AssertUnwindSafe(|| b.consume_tick(t))).is_err());
    assert_eq!(b.failed_tick.as_ref().unwrap().sequence, 1);
    assert!(held.get());
    assert_eq!(cpu.borrow().tick_live, Some(1));
    assert_eq!(cpu.borrow().tick_consumed, 0);
}
#[test]
fn tick_observer_refuses_foreign_issuer_and_consumes_one_actual_receipt() {
    let (mut b, h, _, cpu) = backend();
    let m = b.issue(h[0], 0).unwrap();
    let held = Rc::new(Cell::new(true));
    let mut t = Tick {
        issuer: core::ptr::null(),
        sequence: 1,
        observation: os_k1060_queue::TickObservation {
            cpu: 0,
            source: 30,
            sequence: 1,
            counter: 1,
            thread: m.thread,
            slice: 1,
        },
        held: held.clone(),
    };
    cpu.borrow_mut().tick_live = Some(1);
    assert!(matches!(b.tick(&t), Err(os_k1060_queue::Error::Tick)));
    t.issuer = Rc::as_ptr(&cpu);
    assert_eq!(b.tick(&t).unwrap().sequence, 1);
    b.consume_tick(t);
    assert!(!held.get());
    assert_eq!(cpu.borrow().tick_consumed, 1);
}
#[test]
fn retirement_failure_returns_actual_member_and_never_returns_stack_pages() {
    let (mut b, h, hardware, _) = backend();
    let m = b.issue(h[0], 0).unwrap();
    hardware.borrow_mut().release_fail = true;
    let (error, m) = b.retire_member(m).err().unwrap();
    assert_eq!(error, os_k1060_queue::Error::Backend);
    assert_eq!(m.context, h[0]);
    assert_eq!(b.members[0], Some(h[0]));
    assert_eq!(
        (hardware.borrow().pins, hardware.borrow().stack_pages),
        (3, 12)
    );
}
#[test]
fn narrow_retirement_consumes_only_the_actual_withdrawn_member() {
    let (mut q, h, hardware, _) = queue();
    let id = q.queue().record(h[0]).unwrap().thread;
    q.queue().with_backend_observation(|b| {
        b.bank
            .handoff()
            .bank()
            .with_backend_observation(|d| d.inner.table.borrow_mut().cancel(id).unwrap())
    });
    let m = q.quiescent().unwrap().withdraw(h[0]).unwrap();
    q.quiescent()
        .unwrap()
        .os_k1060_retire_withdrawn(m)
        .ok()
        .unwrap();
    assert_eq!(ownership(&q), (2, 8, 2));
    assert_eq!(hardware.borrow().releases, 1);
    assert_eq!(q.queue().snapshot().members, 2);
    assert!(matches!(
        q.queue().record(h[0]),
        Err(os_k1060_queue::Error::Stale)
    ));
    q.queue().audit().unwrap();
}
#[test]
fn narrow_retirement_context_refusal_returns_the_exact_live_member() {
    let (mut q, h, hardware, _) = queue();
    let id = q.queue().record(h[0]).unwrap().thread;
    q.queue().with_backend_observation(|b| {
        b.bank
            .handoff()
            .bank()
            .with_backend_observation(|d| d.inner.table.borrow_mut().cancel(id).unwrap())
    });
    let m = q.quiescent().unwrap().withdraw(h[0]).unwrap();
    let context = m.context;
    hardware.borrow_mut().in_irq = true;
    let (error, m) = q
        .quiescent()
        .unwrap()
        .os_k1060_retire_withdrawn(m)
        .err()
        .unwrap();
    assert_eq!(error, os_k1060_queue::Error::Context);
    assert_eq!(m.context, context);
    assert_eq!(
        (hardware.borrow().pins, hardware.borrow().stack_pages),
        (3, 12)
    );
    hardware.borrow_mut().in_irq = false;
    q.quiescent()
        .unwrap()
        .os_k1060_retire_withdrawn(m)
        .ok()
        .unwrap();
    assert_eq!(ownership(&q), (2, 8, 2));
}
#[test]
fn actual_return_abort_preserves_fifo_epoch_and_retained_members() {
    let (mut q, _, hardware, _) = queue();
    step(&mut q, false);
    let before = q.queue().snapshot();
    let order = q.queue().ready_order();
    let c = capture(&q);
    let t = q.prepare_return(c).unwrap();
    q.abort_return(t).ok().unwrap();
    assert_eq!(q.queue().snapshot(), before);
    assert_eq!(q.queue().ready_order(), order);
    assert_eq!(ownership(&q), (3, 12, 3));
    assert_eq!(hardware.borrow().releases, 0);
}
#[test]
fn finish_exit_refuses_an_unobserved_real_completion_token() {
    let (mut q, _, _, _) = queue();
    step(&mut q, false);
    let c = capture(&q);
    let backend_offset = {
        let l = os_k1060_queue::os_k1060_return_layout::<B, 3>();
        (l[1] + l[6] + l[11]) as usize
    };
    // Controlled private adapter test derives the nested mutable subobject
    // from its original exclusive Queue pointer after all observations ended.
    let b = unsafe {
        &mut *((&mut q as *mut Q)
            .cast::<u8>()
            .add(backend_offset)
            .cast::<B>())
    };
    let context = b.members[0].unwrap();
    let o = b.bank.os_k1060_observe_member(context).unwrap();
    let m = OsK1060Member {
        identity: b.identity,
        context,
        thread: o.thread.id,
        ordinal: 0,
        retired: false,
    };
    let p = os_k1060_queue::QueueCompletionBackend::prepare_exit(b, &m, c).unwrap();
    let (error, p) = os_k1060_queue::QueueCompletionBackend::finish_exit(b, p)
        .err()
        .unwrap();
    assert_eq!(error, os_k1060_queue::Error::State);
    assert!(p.token.is_some());
    assert!(!p.observed);
    os_k1060_queue::QueueCompletionBackend::abort_exit(b, p)
        .ok()
        .unwrap();
    assert_eq!(ownership(&q), (3, 12, 3));
}
#[test]
fn successful_release_context_drift_quarantines_logical_member_without_fake_binding() {
    for drift in 1..=9 {
        let (mut q, h, hardware, cpu) = queue();
        let id = q.queue().record(h[0]).unwrap().thread;
        q.queue().with_backend_observation(|b| {
            b.bank
                .handoff()
                .bank()
                .with_backend_observation(|d| d.inner.table.borrow_mut().cancel(id).unwrap())
        });
        let m = q.quiescent().unwrap().withdraw(h[0]).unwrap();
        let context = m.context;
        cpu.borrow_mut().release_drift = drift;
        let (error, m) = q
            .quiescent()
            .unwrap()
            .os_k1060_retire_withdrawn(m)
            .err()
            .unwrap();
        assert_eq!(error, os_k1060_queue::Error::Quarantined);
        assert_eq!(m.context, context);
        assert!(m.retired);
        assert_eq!(
            (
                hardware.borrow().pins,
                hardware.borrow().stack_pages,
                hardware.borrow().releases
            ),
            (2, 8, 1)
        );
        assert!(q.queue().snapshot().faulted);
        q.queue().with_backend_observation(|b| {
            assert!(b.retirement_quarantined);
            assert_eq!(b.members[0], Some(context));
            assert_eq!(b.bank.handoff().bank().snapshot().retained, 2);
        });
        // Restoring modeled hardware cannot authorize queue/ordinal reuse.
        {
            let mut e = hardware.borrow_mut();
            e.cpu = 0;
            e.daif = 0x3c0;
            e.current = None;
            e.in_irq = false;
            e.critical = 0;
            e.safe = true;
            e.fp = true;
            e.sp = 0x90001000;
        }
        q.queue().with_backend_observation(|b| {
            b.bank
                .handoff()
                .bank()
                .with_backend_observation(|d| d.root.set(model::BOOTSTRAP_ROOT))
        });
        assert!(q.select(os_k1060_queue::Disposition::Ready).is_err());
        let b = q
            .queue()
            .with_backend_observation(|b| b as *const B as usize);
        assert_ne!(b, 0);
        assert_eq!(
            (hardware.borrow().pins, hardware.borrow().stack_pages),
            (2, 8)
        );
    }
}