// Host-only. The fixture runs the frozen Threads/AsyncBank implementations;
// physical_step models register observations and never claims CPU execution.
use std::vec::Vec;
include!("handoff_fixture.rs");
use std::cell::Cell;
use turkos_os_thread_wait::thread_wait as wait;
use turkos_os_threads::threads::{State as ThreadState, ThreadId};

#[derive(Default)]
struct Ledger {
    pins: Cell<usize>,
    retains: Cell<usize>,
    releases: Cell<usize>,
    resolves: Cell<usize>,
    fail_retain: Cell<bool>,
    fail_validate: Cell<bool>,
    fail_release: Cell<bool>,
    fail_resolve_thread: Cell<Option<ThreadId>>,
    clock_regression: Cell<bool>,
}
struct SourcePort {
    hardware: Rc<RefCell<saved::Hardware>>,
    observation: Rc<RefCell<wait::Observation>>,
}
unsafe impl wait::Producer for SourcePort {
    fn execution(&self) -> wait::Execution {
        execution(&self.hardware)
    }
    fn observe(&self) -> Result<wait::Observation, wait::Error> {
        Ok(*self.observation.borrow())
    }
}
fn execution(h: &Rc<RefCell<saved::Hardware>>) -> wait::Execution {
    let h = h.borrow();
    wait::Execution {
        cpu: h.cpu,
        irq_masked: h.daif & 128 != 0,
        in_irq: h.in_irq,
        current: h.current,
    }
}
struct Pins {
    thread: ThreadId,
    target: ThreadId,
    source: wait::Source,
}
struct WaitPrepared {
    token: Option<OwnedHandoff>,
    thread: ThreadId,
    target: ThreadId,
    closed: bool,
}
struct Driver {
    bank: AsyncBank<Device, 4>,
    handles: [Handle; 3],
    hardware: Rc<RefCell<saved::Hardware>>,
    observations: [Rc<RefCell<wait::Observation>>; 2],
    ledger: Rc<Ledger>,
    landing: Option<(Image, u64, ThreadId)>,
}
impl Driver {
    fn handle(&self, id: ThreadId) -> Result<Handle, wait::Error> {
        self.handles
            .iter()
            .copied()
            .find(|h| self.bank.bank().record(*h).is_ok_and(|r| r.thread == id))
            .ok_or(wait::Error::Stale)
    }
    fn state(&self, id: ThreadId) -> ThreadState {
        self.bank
            .bank()
            .with_backend_observation(|d| d.inner.table.borrow().record(id).unwrap().state)
    }
    fn landing(&self) {
        // No WaitSet or AsyncBank mutable loan exists here.
        self.bank
            .with_prepared_observation(|p| assert!(p.is_some()));
        let staged = self.bank.bank().with_backend_observation(|d| d.cpu.clone());
        assert!(self.bank.stage().is_some());
        // The bank's target image is exposed only with the retained nonce token
        // in departure helpers below, not manufactured by a requested Task.
        assert!(staged.borrow().departures > 0);
    }
}
unsafe impl wait::Backend for Driver {
    type Pins = Pins;
    type Prepared = WaitPrepared;
    type Capture = Capture;
    fn execution(&self) -> wait::Execution {
        execution(&self.hardware)
    }
    fn observe(&self, source: wait::Source) -> Result<wait::Observation, wait::Error> {
        let mut o = self
            .observations
            .iter()
            .find_map(|o| {
                let o = *o.borrow();
                (o.source == source).then_some(o)
            })
            .ok_or(wait::Error::Source)?;
        if self.ledger.clock_regression.get() {
            o.now = o.now.saturating_sub(1);
        }
        Ok(o)
    }
    fn retain(
        &mut self,
        thread: ThreadId,
        target: ThreadId,
        source: wait::Source,
    ) -> Result<Pins, wait::Error> {
        if self.ledger.fail_retain.get() {
            return Err(wait::Error::Backend);
        }
        assert_eq!(self.state(thread), ThreadState::Running);
        assert_eq!(self.state(target), ThreadState::Ready);
        self.observe(source)?;
        self.ledger.pins.set(self.ledger.pins.get() + 2);
        self.ledger.retains.set(self.ledger.retains.get() + 1);
        Ok(Pins {
            thread,
            target,
            source,
        })
    }
    fn validate(
        &self,
        p: &Pins,
        thread: ThreadId,
        target: ThreadId,
        source: wait::Source,
    ) -> Result<(), wait::Error> {
        if self.ledger.fail_validate.get() {
            return Err(wait::Error::Backend);
        }
        if (p.thread, p.target, p.source) != (thread, target, source) {
            return Err(wait::Error::Source);
        }
        if self.state(thread) == ThreadState::Dead || self.state(target) == ThreadState::Dead {
            return Err(wait::Error::State);
        }
        self.observe(source)?;
        Ok(())
    }
    fn stage(&mut self, p: &mut Pins, c: Capture) -> Result<WaitPrepared, wait::Error> {
        assert_eq!(self.state(p.thread), ThreadState::Running);
        let token = self
            .bank
            .sleep_to(self.handle(p.thread)?, self.handle(p.target)?, c)
            .map_err(|_| wait::Error::Backend)?;
        assert_eq!(self.state(p.thread), ThreadState::Running);
        self.landing = Some((
            self.bank.target_image(&token).unwrap(),
            token.nonce(),
            p.target,
        ));
        Ok(WaitPrepared {
            token: Some(token),
            thread: p.thread,
            target: p.target,
            closed: false,
        })
    }
    fn abort(&mut self, p: &mut WaitPrepared) -> Result<(), wait::Failure> {
        match self.bank.abort(p.token.take().unwrap()) {
            Ok(()) => {
                assert_eq!(self.state(p.thread), ThreadState::Running);
                p.closed = true;
                Ok(())
            }
            Err(HandoffFailure::Before(_, token)) => {
                p.token = Some(token);
                Err(wait::Failure {
                    error: wait::Error::Backend,
                    phase: wait::FailurePhase::Before,
                })
            }
            Err(HandoffFailure::Quarantined(_)) => Err(wait::Failure {
                error: wait::Error::Quarantined,
                phase: wait::FailurePhase::After,
            }),
        }
    }
    fn depart(&mut self, p: &mut WaitPrepared) -> Result<(), wait::Failure> {
        match self.bank.depart(p.token.take().unwrap()) {
            Ok(token) => {
                assert_eq!(self.state(p.thread), ThreadState::Sleeping);
                p.token = Some(token);
                Ok(())
            }
            Err(HandoffFailure::Before(_, token)) => {
                p.token = Some(token);
                Err(wait::Failure {
                    error: wait::Error::Backend,
                    phase: wait::FailurePhase::Before,
                })
            }
            Err(HandoffFailure::Quarantined(_)) => Err(wait::Failure {
                error: wait::Error::Quarantined,
                phase: wait::FailurePhase::After,
            }),
        }
    }
    fn landed(&mut self, p: &mut WaitPrepared) -> Result<(), wait::Failure> {
        match self.bank.landed(p.token.take().unwrap()) {
            Ok(()) => {
                assert_eq!(self.state(p.thread), ThreadState::Sleeping);
                assert_eq!(self.state(p.target), ThreadState::Running);
                Ok(())
            }
            Err(HandoffFailure::Before(_, token)) => {
                p.token = Some(token);
                Err(wait::Failure {
                    error: wait::Error::Backend,
                    phase: wait::FailurePhase::Before,
                })
            }
            Err(HandoffFailure::Quarantined(_)) => Err(wait::Failure {
                error: wait::Error::Quarantined,
                phase: wait::FailurePhase::After,
            }),
        }
    }
    fn resolve(
        &mut self,
        pins: &mut Pins,
        p: &mut WaitPrepared,
        _: wait::Outcome,
    ) -> Result<(), wait::Failure> {
        if self.ledger.fail_resolve_thread.get() == Some(p.thread) {
            return Err(wait::Failure {
                error: wait::Error::Backend,
                phase: wait::FailurePhase::Before,
            });
        }
        if p.closed || pins.thread != p.thread || self.state(p.thread) != ThreadState::Sleeping {
            return Err(wait::Failure {
                error: wait::Error::State,
                phase: wait::FailurePhase::Before,
            });
        }
        self.bank.bank().with_backend_observation(|d| {
            let token = d.waits.borrow_mut()[p.thread.slot()].take().unwrap();
            assert_eq!(token.thread(), p.thread);
            assert_eq!(d.inner.table.borrow_mut().wake(token).unwrap(), p.thread);
        });
        p.closed = true;
        self.ledger.resolves.set(self.ledger.resolves.get() + 1);
        Ok(())
    }
    fn release(
        &mut self,
        owned: wait::Retained<Pins, WaitPrepared>,
    ) -> Result<(), (wait::Error, wait::Retained<Pins, WaitPrepared>)> {
        if self.ledger.fail_release.get() {
            return Err((wait::Error::Backend, owned));
        }
        if owned
            .prepared
            .as_ref()
            .is_some_and(|p| !p.closed || p.token.is_some())
        {
            return Err((wait::Error::Pending, owned));
        }
        self.ledger.pins.set(self.ledger.pins.get() - 2);
        self.ledger.releases.set(self.ledger.releases.get() + 1);
        Ok(())
    }
}
struct System<const N: usize = 8> {
    waits: wait::WaitSet<Driver, N>,
    ingress: [wait::Ingress<SourcePort, 2>; 2],
    ids: [ThreadId; 3],
    handles: [Handle; 3],
    hardware: Rc<RefCell<saved::Hardware>>,
    cpu: Rc<RefCell<Cpu>>,
    observations: [Rc<RefCell<wait::Observation>>; 2],
    ledger: Rc<Ledger>,
}
fn system() -> System {
    let (mut bank, handles, hardware, cpu) = setup();
    let token = bank.start(handles[0]).unwrap();
    land(&mut bank, token);
    let ids = core::array::from_fn(|i| bank.bank().record(handles[i]).unwrap().thread);
    let observations = core::array::from_fn(|i| {
        Rc::new(RefCell::new(wait::Observation {
            source: wait::Source {
                channel: 0x108001 + i as u64,
                epoch: 1,
                owner: 0x1080,
            },
            sequence: 0,
            ready: false,
            now: 100,
        }))
    });
    let ingress = core::array::from_fn(|i| {
        wait::Ingress::new(SourcePort {
            hardware: hardware.clone(),
            observation: observations[i].clone(),
        })
        .ok()
        .unwrap()
    });
    let ledger = Rc::new(Ledger::default());
    let waits = wait::WaitSet::new(Driver {
        bank,
        handles,
        hardware: hardware.clone(),
        observations: observations.clone(),
        ledger: ledger.clone(),
        landing: None,
    })
    .ok()
    .unwrap();
    System {
        waits,
        ingress,
        ids,
        handles,
        hardware,
        cpu,
        observations,
        ledger,
    }
}
fn arm<const N: usize>(
    s: &mut System<N>,
    source: usize,
    target: usize,
    port: usize,
    deadline: Option<u64>,
) -> wait::WaitToken {
    let c = s
        .waits
        .with_backend_observation(|d| capture(&d.bank, s.handles[source], &s.hardware, 19, false));
    s.waits
        .arm(&s.ingress[port], s.ids[source], s.ids[target], c, deadline)
        .ok()
        .unwrap()
}
fn arrive<const N: usize>(s: &mut System<N>, transfer: wait::WaitTransfer) -> wait::WaitToken {
    s.waits.with_backend_observation(|d| {
        // The actual model CPU landing witness is recorded under an immutable
        // observer after the departure loan has ended.
        d.landing();
        // A Prepared's opaque nonce remains inside the bank. The target image
        // is read from the actual staged bank record for this model boundary.
    });
    // Source-bound fixture exposes the actual retained token only to this
    // dedicated host boundary through Driver's private observation below.
    let i = s
        .waits
        .records()
        .iter()
        .position(|r| r.phase == wait::Phase::Departed)
        .unwrap();
    let target = s.waits.records()[i].target.unwrap();
    s.waits.with_backend_observation(|d| {
        let (image, nonce, actual_target) = d.landing.unwrap();
        assert_eq!(actual_target, target);
        let actual = saved::Backend::expected(image);
        s.hardware.borrow_mut().sp = image.sp() - 64;
        s.hardware.borrow_mut().current = Some(target);
        let mut cpu = s.cpu.borrow_mut();
        cpu.nonce = nonce;
        cpu.registers = Some(actual);
    });
    s.waits.landed(transfer).ok().unwrap()
}